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