sem.icl

   1 implementation module sem
   2
   3 import qualified Data.Map as Map
   4
   5 from Data.Func import $
   6 from StdFunc import o, flip, const, id
   7
   8 import Control.Monad
   9 import Control.Monad.Trans
  10 import Control.Monad.State
  11 import Data.Either
  12 import Data.Maybe
  13 import Data.Monoid
  14 import Data.List
  15 import Data.Functor
  16 import Data.Tuple
  17
  18 import StdString
  19 import StdTuple
  20 import StdList
  21 import StdMisc
  22 import StdEnum
  23 import GenEq
  24
  25 from Text import class Text(concat), instance Text String
  26
  27 import AST
  28
  29
  30 :: Scheme = Forall [TVar] Type
  31 :: Gamma :== 'Map'.Map String Scheme //map from Variables! to types
  32 :: Typing a :== StateT (Gamma, [TVar]) (Either SemError) a
  33 :: Substitution :== 'Map'.Map TVar Type
  34 :: Constraints :== [(Type, Type)]
  35 :: SemError
  36         = ParseError Pos String
  37         | UnifyError Pos Type Type
  38     | InfiniteTypeError Pos Type
  39     | FieldSelectorError Pos Type FieldSelector
  40         | OperatorError Pos Op2 Type
  41     | UndeclaredVariableError Pos String
  42     | ArgumentMisMatchError Pos String
  43         | SanityError Pos String
  44         | Error String
  45
  46 instance zero Gamma where
  47         zero = 'Map'.newMap
  48
  49 variableStream :: [TVar]
  50 variableStream = map toString [1..]
  51
  52 sem :: AST -> Either [SemError] AST
  53 sem (AST fd) = case foldM (const $ hasNoDups fd) () fd
  54                         >>| foldM (const isNiceMain) () fd
  55                         >>| hasMain fd
  56                     >>| evalStateT (type fd) (zero, variableStream) of
  57         Left e = Left [e]
  58     Right fds = Right (AST fds)
  59 where
  60                 hasNoDups :: [FunDecl] FunDecl -> Either SemError ()
  61                 hasNoDups fds (FunDecl p n _ _ _ _)
  62                 # mbs = map (\(FunDecl p` n` _ _ _ _)->if (n == n`) (Just p`) Nothing) fds
  63                 = case catMaybes mbs of
  64                         [] = Left $ SanityError p "HUH THIS SHOULDN'T HAPPEN"
  65                         [x] = pure ()
  66                         [_:x] = Left $ SanityError p (concat
  67                                 [n, " multiply defined at ", toString p])
  68
  69                 hasMain :: [FunDecl] -> Either SemError ()
  70                 hasMain [(FunDecl _ "main" _ _ _ _):fd] = pure ()
  71                 hasMain [_:fd] = hasMain fd
  72                 hasMain [] = Left $ SanityError zero "no main function defined"
  73
  74                 isNiceMain :: FunDecl -> Either SemError ()
  75                 isNiceMain (FunDecl p "main" as mt _ _) = case (as, mt) of
  76                         ([_:_], _) = Left $ SanityError p "main must have arity 0"
  77                         ([], t) = (case t of
  78                                 Nothing = pure ()
  79                                 Just VoidType = pure ()
  80                                 _ = Left $ SanityError p "main has to return Void")
  81                 isNiceMain _ = pure ()
  82
  83 class Typeable a where
  84     ftv :: a -> [TVar]
  85     subst :: Substitution a -> a
  86
  87 instance Typeable Scheme where
  88     ftv (Forall bound t) = difference (ftv t) bound
  89     subst s (Forall bound t) = Forall bound $ subst s_ t
  90         where s_ = 'Map'.filterWithKey (\k _ -> not (elem k bound)) s
  91
  92 instance Typeable [a] | Typeable a where
  93     ftv types   = foldr (\t ts-> ftv t ++ ts) [] types
  94     subst s ts  = map (\t->subst s t) ts
  95
  96 instance Typeable Type where
  97     ftv (TupleType (t1, t2))    = ftv t1 ++ ftv t2
  98     ftv (ListType t)            = ftv t
  99     ftv (IdType tvar)           = [tvar]
 100     ftv (t1 ->> t2)             = ftv t1 ++ ftv t2
 101     ftv _                       = []
 102     subst s (TupleType (t1, t2))= TupleType (subst s t1, subst s t2)
 103     subst s (ListType t1)       = ListType (subst s t1)
 104     subst s (t1 ->> t2)         = (subst s t1) ->> (subst s t2)
 105     subst s t1=:(IdType tvar)   = 'Map'.findWithDefault t1 tvar s
 106     subst s t                   = t
 107
 108 instance Typeable Gamma where
 109     ftv gamma       = concatMap id $ map ftv ('Map'.elems gamma)
 110     subst s gamma   = Mapmap (subst s) gamma
 111
 112 extend :: String Scheme Gamma -> Gamma
 113 extend k t g = 'Map'.put k t g
 114
 115 //// ------------------------
 116 //// algorithm U, Unification
 117 //// ------------------------
 118 instance zero Substitution where zero = 'Map'.newMap
 119
 120 compose :: Substitution Substitution -> Substitution
 121 compose s1 s2 = 'Map'.union (Mapmap (subst s1) s2) s1
 122 //Note: just like function compositon compose does snd first
 123
 124 occurs :: TVar a -> Bool | Typeable a
 125 occurs tvar a = elem tvar (ftv a)
 126
 127 unify :: Type Type -> Either SemError Substitution
 128 unify t1 t2=:(IdType tv)    | t1 == (IdType tv) = Right zero
 129                             | occurs tv t1 = Left $ InfiniteTypeError zero t1
 130                             | otherwise = Right $ 'Map'.singleton tv t1
 131 unify t1=:(IdType tv) t2 = unify t2 t1
 132 unify (ta1->>ta2) (tb1->>tb2) = unify ta1 tb1 >>= \s1->
 133                                 unify ta2 tb2 >>= \s2->
 134                                 Right $ compose s1 s2
 135 unify (TupleType (ta1,ta2)) (TupleType (tb1,tb2)) = unify ta1 tb1 >>= \s1->
 136                                                     unify ta2 tb2 >>= \s2->
 137                                                     Right $ compose s1 s2
 138 unify (ListType t1) (ListType t2) = unify t1 t2
 139 unify t1 t2 | t1 == t2  = Right zero
 140             | otherwise = Left $ UnifyError zero t1 t2
 141
 142 //// ------------------------
 143 //// Algorithm M, Inference and Solving
 144 //// ------------------------
 145 gamma :: Typing Gamma
 146 gamma = gets fst
 147 putGamma :: Gamma -> Typing ()
 148 putGamma g = modify (appFst $ const g) >>| pure ()
 149 changeGamma :: (Gamma -> Gamma) -> Typing Gamma
 150 changeGamma f = modify (appFst f) >>| gamma
 151 withGamma :: (Gamma -> a) -> Typing a
 152 withGamma f = f <$> gamma
 153 fresh :: Typing Type
 154 fresh = gets snd >>= \vars->
 155         modify (appSnd $ const $ tail vars) >>|
 156         pure (IdType (head vars))
 157
 158 lift :: (Either SemError a) -> Typing a
 159 lift (Left e) = liftT $ Left e
 160 lift (Right v) = pure v
 161
 162 //instantiate maps a schemes type variables to variables with fresh names
 163 //and drops the quantification: i.e. forall a,b.a->[b] becomes c->[d]
 164 instantiate :: Scheme -> Typing Type
 165 instantiate (Forall bound t) =
 166     mapM (const fresh) bound >>= \newVars->
 167     let s = 'Map'.fromList (zip (bound,newVars)) in
 168     pure (subst s t)
 169
 170 //generalize quentifies all free type variables in a type which are not
 171 //in the gamma
 172 generalize :: Type -> Typing Scheme
 173 generalize t = gamma >>= \g-> pure $ Forall (difference (ftv t) (ftv g)) t
 174
 175 lookup :: String -> Typing Type
 176 lookup k = gamma >>= \g-> case 'Map'.member k g of
 177     False = liftT (Left $ UndeclaredVariableError zero k)
 178     True = instantiate $ 'Map'.find k g
 179
 180 //The inference class
 181 //When tying it all together we will treat the program is a big
 182 //let x=e1 in let y=e2 in ....
 183 class infer a :: a -> Typing (Substitution, Type)
 184
 185 ////---- Inference for Expressions ----
 186
 187 instance infer Expr where
 188  infer e = case e of
 189     VarExpr _ (VarDef k fs) = (\t->(zero,t)) <$> lookup k
 190     //instantiate is key for the let polymorphism!
 191     //TODO: field selectors
 192
 193     Op2Expr _ e1 op e2 =
 194         infer e1 >>= \(s1, t1) ->
 195         infer e2 >>= \(s2, t2) ->
 196         fresh >>= \tv ->
 197         let given = t1 ->> t2 ->> tv in
 198         op2Type op >>= \expected ->
 199         lift (unify expected given) >>= \s3 ->
 200         pure ((compose s3 $ compose s2 s1), subst s3 tv)
 201
 202     Op1Expr _ op e1 =
 203         infer e1 >>= \(s1, t1) ->
 204         fresh >>= \tv ->
 205         let given = t1 ->> tv in
 206         op1Type op >>= \expected ->
 207         lift (unify expected given) >>= \s2 ->
 208         pure (compose s2 s1, subst s2 tv)
 209
 210     EmptyListExpr _ = (\tv->(zero,tv)) <$> fresh
 211
 212     TupleExpr _ (e1, e2) =
 213         infer e1 >>= \(s1, t1) ->
 214         infer e2 >>= \(s2, t2) ->
 215         pure (compose s2 s1, TupleType (t1,t2))
 216
 217     FunExpr _ f args fs = //todo: fieldselectors
 218         lookup f >>= \expected ->
 219         let accST = (\(s,ts) e->infer e >>= \(s_,et)->pure (compose s_ s,ts++[et])) in
 220         foldM accST (zero,[]) args >>= \(s1, argTs)->
 221         fresh >>= \tv->
 222         let given = foldr (->>) tv argTs in
 223         lift (unify expected given) >>= \s2->
 224         pure (compose s2 s1, subst s2 tv)
 225
 226     IntExpr _ _ = pure $ (zero, IntType)
 227     BoolExpr _ _ = pure $ (zero, BoolType)
 228     CharExpr _ _ = pure $ (zero, CharType)
 229
 230
 231 op2Type :: Op2 -> Typing Type
 232 op2Type op
 233 | elem op [BiPlus, BiMinus, BiTimes, BiDivide, BiMod]
 234   = pure (IntType ->> IntType ->> IntType)
 235 | elem op [BiEquals, BiUnEqual]
 236   = fresh >>= \t1-> fresh >>= \t2-> pure (t1 ->> t2 ->> BoolType)
 237 | elem op [BiLesser, BiGreater, BiLesserEq, BiGreaterEq]
 238   = pure (IntType ->> IntType ->> BoolType)
 239 | elem op [BiAnd, BiOr]
 240   = pure (BoolType ->> BoolType ->> BoolType)
 241 | op == BiCons
 242   = fresh >>= \t1-> pure (t1 ->> ListType t1 ->> ListType t1)
 243
 244 op1Type :: Op1 -> Typing Type
 245 op1Type UnNegation = pure $ (BoolType ->> BoolType)
 246 op1Type UnMinus = pure $ (IntType ->> IntType)
 247
 248 ////----- Inference for Statements -----
 249 applySubst :: Substitution -> Typing Gamma
 250 applySubst s = changeGamma (subst s)
 251
 252 instance infer Stmt where
 253  infer s = case s of
 254     IfStmt e th el =
 255         infer e >>= \(s1, et)->
 256         lift (unify et BoolType) >>= \s2 ->
 257         applySubst (compose s2 s1) >>|
 258         infer th >>= \(s3, tht)->
 259         applySubst s3 >>|
 260         infer el >>= \(s4, elt)->
 261         applySubst s4 >>|
 262         lift (unify tht elt) >>= \s5->
 263         pure (compose s5 $ compose s4 $ compose s3 $ compose s2 s1, subst s5 tht)
 264
 265     WhileStmt e wh =
 266         infer e >>= \(s1, et)->
 267         lift (unify et BoolType) >>= \s2 ->
 268         applySubst (compose s2 s1) >>|
 269         infer wh >>= \(s3, wht)->
 270         pure (compose s3 $ compose s2 s1, subst s3 wht)
 271
 272     AssStmt (VarDef k fs) e =
 273         infer e >>= \(s1, et)->
 274         applySubst s1 >>|
 275         changeGamma (extend k (Forall [] et)) >>| //todo: fieldselectors
 276         pure (s1, VoidType)
 277
 278     FunStmt f es = undef //what is this?
 279
 280     ReturnStmt Nothing = pure (zero, VoidType)
 281     ReturnStmt (Just e) = infer e
 282
 283 //The type of a list of statements is either an encountered
 284 //return, or VoidType
 285 instance infer [a] | infer a where
 286     infer []        = pure (zero, VoidType)
 287     infer [stmt:ss] =
 288         infer stmt >>= \(s1, t1) ->
 289         applySubst s1 >>|
 290         infer ss >>= \(s2, t2) ->
 291         applySubst s2 >>|
 292         case t1 of
 293             VoidType = pure (compose s2 s1, t2)
 294             _ = case t2 of
 295                 VoidType = pure (compose s2 s1, t1)
 296                 _ = lift (unify t1 t2) >>= \s3 ->
 297                     pure (compose s3 $ compose s2 s1, t1)
 298
 299 //the type class inferes the type of an AST element (VarDecl or FunDecl)
 300 //and adds it to the AST element
 301 class type a :: a -> Typing a
 302
 303 instance type VarDecl where
 304     type (VarDecl p expected k e) =
 305         infer e >>= \(s1, given) ->
 306         applySubst s1 >>|
 307         case expected of
 308             Nothing = pure zero
 309             Just expected_ = lift (unify expected_ given)
 310         >>= \s2->
 311         applySubst s2 >>|
 312         let vtype = subst (compose s2 s1) given in
 313         generalize vtype >>= \t ->
 314         changeGamma (extend k t) >>|
 315         pure (VarDecl p (Just vtype) k e)
 316
 317 instance type FunDecl where
 318     type (FunDecl p f args expected vds stmts) =
 319         introduce f >>|
 320         mapM introduce args >>= \argTs->
 321         type vds >>= \tVds->
 322         infer stmts >>= \(s1, result)->
 323         let given = foldr (->>) result argTs in
 324         applySubst s1 >>|
 325         (case expected of
 326             Nothing = pure zero
 327             Just expected_ = lift (unify expected_ given))
 328         >>= \s2 ->
 329         let ftype = subst (compose s2 s1) given in
 330         generalize ftype >>= \t->
 331         changeGamma (extend f t) >>|
 332         pure (FunDecl p f args (Just ftype) tVds stmts)
 333
 334 instance toString (Maybe a) | toString a where
 335     toString Nothing = "Nothing"
 336     toString (Just e) = concat ["Just ", toString e]
 337
 338 instance type [a] | type a where
 339     type dcls = mapM type dcls
 340
 341 introduce :: String -> Typing Type
 342 introduce k =
 343     fresh >>= \tv ->
 344     changeGamma (extend k (Forall [] tv)) >>|
 345     pure tv
 346
 347 instance toString Scheme where
 348     toString (Forall x t) =
 349         concat ["Forall ": intersperse "," x] +++ concat [". ", toString t];
 350
 351 instance toString Gamma where
 352     toString mp =
 353         concat [concat [k, ": ", toString v, "\n"]\\(k, v)<-'Map'.toList mp]
 354
 355 instance toString Substitution where
 356     toString subs =
 357         concat [concat [k, ": ", toString t, "\n"]\\(k, t)<-'Map'.toList subs]
 358
 359 instance toString SemError where
 360     toString (SanityError p e) = concat [toString p,
 361         "SemError: SanityError: ", e]
 362     toString (ParseError p s) = concat [toString p,
 363         "ParseError: ", s]
 364     toString (UnifyError p t1 t2) = concat [toString p,
 365         "Can not unify types, expected|given:\n", toString t1,
 366         "\n", toString t2]
 367     toString (InfiniteTypeError p t) = concat [toString p,
 368         "Infinite type: ", toString t]
 369     toString (FieldSelectorError p t fs) = concat [toString p,
 370         "Can not run fieldselector '", toString fs, "' on type: ",
 371         toString t]
 372     toString (OperatorError p op t) = concat [toString p,
 373         "Operator error, operator '", toString op, "' can not be",
 374         "used on type: ", toString t]
 375     toString (UndeclaredVariableError p k) = concat [toString p,
 376         "Undeclared identifier: ", k]
 377     toString (ArgumentMisMatchError p str) = concat [toString p,
 378         "Argument mismatch: ", str]
 379     toString (Error e) = concat ["Unknown error during semantical",
 380         "analysis: ", e]
 381
 382 instance MonadTrans (StateT (Gamma, [TVar])) where
 383     liftT m = StateT \s-> m >>= \a-> return (a, s)
 384
 385 Mapmap :: (a->b) ('Map'.Map k a) -> ('Map'.Map k b)
 386 Mapmap _ 'Map'.Tip = 'Map'.Tip
 387 Mapmap f ('Map'.Bin sz k v ml mr) = 'Map'.Bin sz k (f v)
 388                                         (Mapmap f ml)
 389                                         (Mapmap f mr)