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