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 [] (IntType ->> (ListType 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 "isEmpty" = ListType <$> fresh
 182 lookup k = gamma >>= \g-> case 'Map'.member k g of
 183     False = liftT (Left $ UndeclaredVariableError zero k)
 184     True = instantiate $ 'Map'.find k g
 185
 186 //The inference class
 187 //When tying it all together we will treat the program is a big
 188 //let x=e1 in let y=e2 in ....
 189 class infer a :: a -> Typing (Substitution, Type)
 190
 191 ////---- Inference for Expressions ----
 192
 193 instance infer Expr where
 194  infer e = case e of
 195     VarExpr _ (VarDef k fs) = (\t->(zero,t)) <$> lookup k
 196     //instantiate is key for the let polymorphism!
 197     //TODO: field selectors
 198
 199     Op2Expr _ e1 op e2 =
 200         infer e1 >>= \(s1, t1) ->
 201         infer e2 >>= \(s2, t2) ->
 202         fresh >>= \tv ->
 203         let given = t1 ->> t2 ->> tv in
 204         op2Type op >>= \expected ->
 205         lift (unify expected given) >>= \s3 ->
 206         pure ((compose s3 $ compose s2 s1), subst s3 tv)
 207
 208     Op1Expr _ op e1 =
 209         infer e1 >>= \(s1, t1) ->
 210         fresh >>= \tv ->
 211         let given = t1 ->> tv in
 212         op1Type op >>= \expected ->
 213         lift (unify expected given) >>= \s2 ->
 214         pure (compose s2 s1, subst s2 tv)
 215
 216     EmptyListExpr _ = (\tv->(zero,tv)) <$> fresh
 217
 218     TupleExpr _ (e1, e2) =
 219         infer e1 >>= \(s1, t1) ->
 220         infer e2 >>= \(s2, t2) ->
 221         pure (compose s2 s1, TupleType (t1,t2))
 222
 223     FunExpr _ f args fs = //todo: fieldselectors
 224         lookup f >>= \expected ->
 225         let accST = (\(s,ts) e->infer e >>= \(s_,et)->pure (compose s_ s,ts++[et])) in
 226         foldM accST (zero,[]) args >>= \(s1, argTs)->
 227         fresh >>= \tv->
 228         let given = foldr (->>) tv argTs in
 229         lift (unify expected given) >>= \s2->
 230         pure (compose s2 s1, subst s2 tv)
 231
 232     IntExpr _ _ = pure $ (zero, IntType)
 233     BoolExpr _ _ = pure $ (zero, BoolType)
 234     CharExpr _ _ = pure $ (zero, CharType)
 235
 236
 237 op2Type :: Op2 -> Typing Type
 238 op2Type op
 239 | elem op [BiPlus, BiMinus, BiTimes, BiDivide, BiMod]
 240   = pure (IntType ->> IntType ->> IntType)
 241 | elem op [BiEquals, BiUnEqual]
 242   = fresh >>= \t1-> fresh >>= \t2-> pure (t1 ->> t2 ->> BoolType)
 243 | elem op [BiLesser, BiGreater, BiLesserEq, BiGreaterEq]
 244   = pure (IntType ->> IntType ->> BoolType)
 245 | elem op [BiAnd, BiOr]
 246   = pure (BoolType ->> BoolType ->> BoolType)
 247 | op == BiCons
 248   = fresh >>= \t1-> pure (t1 ->> ListType t1 ->> ListType t1)
 249
 250 op1Type :: Op1 -> Typing Type
 251 op1Type UnNegation = pure $ (BoolType ->> BoolType)
 252 op1Type UnMinus = pure $ (IntType ->> IntType)
 253
 254 ////----- Inference for Statements -----
 255 applySubst :: Substitution -> Typing Gamma
 256 applySubst s = changeGamma (subst s)
 257
 258 instance infer Stmt where
 259  infer s = case s of
 260     IfStmt e th el =
 261         infer e >>= \(s1, et)->
 262         lift (unify et BoolType) >>= \s2 ->
 263         applySubst (compose s2 s1) >>|
 264         infer th >>= \(s3, tht)->
 265         applySubst s3 >>|
 266         infer el >>= \(s4, elt)->
 267         applySubst s4 >>|
 268         lift (unify tht elt) >>= \s5->
 269         pure (compose s5 $ compose s4 $ compose s3 $ compose s2 s1, subst s5 tht)
 270
 271     WhileStmt e wh =
 272         infer e >>= \(s1, et)->
 273         lift (unify et BoolType) >>= \s2 ->
 274         applySubst (compose s2 s1) >>|
 275         infer wh >>= \(s3, wht)->
 276         pure (compose s3 $ compose s2 s1, subst s3 wht)
 277
 278     AssStmt (VarDef k fs) e =
 279         lookup k >>= \expected ->
 280         infer e >>= \(s1, given)->
 281         lift (unify expected given) >>= \s2->
 282         let s = compose s2 s1 in
 283         applySubst s >>|
 284         changeGamma (extend k (Forall [] given)) >>| //todo: fieldselectors
 285         pure (s, VoidType)
 286
 287     FunStmt f es _ = pure (zero, VoidType)
 288
 289     ReturnStmt Nothing = pure (zero, VoidType)
 290     ReturnStmt (Just e) = infer e
 291
 292 //The type of a list of statements is either an encountered
 293 //return, or VoidType
 294 instance infer [a] | infer a where
 295     infer []        = pure (zero, VoidType)
 296     infer [stmt:ss] =
 297         infer stmt >>= \(s1, t1) ->
 298         applySubst s1 >>|
 299         infer ss >>= \(s2, t2) ->
 300         applySubst s2 >>|
 301         case t1 of
 302             VoidType = pure (compose s2 s1, t2)
 303             _ = case t2 of
 304                 VoidType = pure (compose s2 s1, t1)
 305                 _ = lift (unify t1 t2) >>= \s3 ->
 306                     pure (compose s3 $ compose s2 s1, t1)
 307
 308 //the type class inferes the type of an AST element (VarDecl or FunDecl)
 309 //and adds it to the AST element
 310 class type a :: a -> Typing (Substitution, a)
 311
 312 instance type VarDecl where
 313     type (VarDecl p expected k e) =
 314         infer e >>= \(s1, given) ->
 315         applySubst s1 >>|
 316         case expected of
 317             Nothing = pure zero
 318             Just expected_ = lift (unify expected_ given)
 319         >>= \s2->
 320         applySubst s2 >>|
 321         let vtype = subst (compose s2 s1) given in
 322         generalize vtype >>= \t ->
 323         changeGamma (extend k t) >>|
 324         pure (compose s2 s1, VarDecl p (Just vtype) k e)
 325
 326 instance type FunDecl where
 327     type (FunDecl p f args expected vds stmts) =
 328         gamma >>= \outerScope-> //functions are infered in their own scopde
 329         introduce f >>|
 330         mapM introduce args >>= \argTs->
 331         type vds >>= \(s1, tVds)->
 332         applySubst s1 >>|
 333         infer stmts >>= \(s2, result)->
 334         applySubst s1 >>|
 335         let argTs_ = map (subst $ compose s2 s1) argTs in
 336         //abort (concat $ intersperse "\n" $ map toString argTs_) >>|
 337         let given = foldr (->>) result argTs_ in
 338         (case expected of
 339             Nothing = pure zero
 340             Just expected_ = lift (unify expected_ given))
 341         >>= \s3 ->
 342         let ftype = subst (compose s3 $ compose s2 s1) given in
 343         generalize ftype >>= \t->
 344         putGamma outerScope >>|
 345         changeGamma (extend f t) >>|
 346         pure (compose s3 $ compose s2 s1, FunDecl p f args (Just ftype) tVds stmts)
 347
 348 instance type [a] | type a where
 349     type []     = pure (zero, [])
 350     type [v:vs] =
 351         type v >>= \(s1, v_)->
 352         applySubst s1 >>|
 353         type vs >>= \(s2, vs_)->
 354         applySubst (compose s2 s1) >>|
 355         pure (compose s2 s1, [v_:vs_])
 356
 357 introduce :: String -> Typing Type
 358 introduce k =
 359     fresh >>= \tv ->
 360     changeGamma (extend k (Forall [] tv)) >>|
 361     pure tv
 362
 363 instance toString Scheme where
 364     toString (Forall x t) =
 365         concat ["Forall ": intersperse "," x] +++ concat [". ", toString t];
 366
 367 instance toString Gamma where
 368     toString mp =
 369         concat [concat [k, ": ", toString v, "\n"]\\(k, v)<-'Map'.toList mp]
 370
 371 instance toString Substitution where
 372     toString subs =
 373         concat [concat [k, ": ", toString t, "\n"]\\(k, t)<-'Map'.toList subs]
 374
 375 instance toString SemError where
 376     toString (SanityError p e) = concat [toString p,
 377         "SemError: SanityError: ", e]
 378     toString (ParseError p s) = concat [toString p,
 379         "ParseError: ", s]
 380     toString (UnifyError p t1 t2) = concat [toString p,
 381         "Can not unify types, expected|given:\n", toString t1,
 382         "\n", toString t2]
 383     toString (InfiniteTypeError p t) = concat [toString p,
 384         "Infinite type: ", toString t]
 385     toString (FieldSelectorError p t fs) = concat [toString p,
 386         "Can not run fieldselector '", toString fs, "' on type: ",
 387         toString t]
 388     toString (OperatorError p op t) = concat [toString p,
 389         "Operator error, operator '", toString op, "' can not be",
 390         "used on type: ", toString t]
 391     toString (UndeclaredVariableError p k) = concat [toString p,
 392         "Undeclared identifier: ", k]
 393     toString (ArgumentMisMatchError p str) = concat [toString p,
 394         "Argument mismatch: ", str]
 395     toString (Error e) = concat ["Unknown error during semantical",
 396         "analysis: ", e]
 397
 398 instance toString (Maybe a) | toString a where
 399     toString Nothing = "Nothing"
 400     toString (Just e) = concat ["Just ", toString e]
 401
 402 instance MonadTrans (StateT (Gamma, [TVar])) where
 403     liftT m = StateT \s-> m >>= \a-> return (a, s)
 404
 405 Mapmap :: (a->b) ('Map'.Map k a) -> ('Map'.Map k b)
 406 Mapmap _ 'Map'.Tip = 'Map'.Tip
 407 Mapmap f ('Map'.Bin sz k v ml mr) = 'Map'.Bin sz k (f v)
 408                                         (Mapmap f ml)
 409                                         (Mapmap f mr)