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