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         lookup k >>= \expected ->
 274         infer e >>= \(s1, given)->
 275         lift (unify expected given) >>= \s2->
 276         let s = compose s2 s1 in
 277         applySubst s >>|
 278         changeGamma (extend k (Forall [] given)) >>| //todo: fieldselectors
 279         pure (s, VoidType)
 280
 281     FunStmt f es = undef //what is this?
 282
 283     ReturnStmt Nothing = pure (zero, VoidType)
 284     ReturnStmt (Just e) = infer e
 285
 286 //The type of a list of statements is either an encountered
 287 //return, or VoidType
 288 instance infer [a] | infer a where
 289     infer []        = pure (zero, VoidType)
 290     infer [stmt:ss] =
 291         infer stmt >>= \(s1, t1) ->
 292         applySubst s1 >>|
 293         infer ss >>= \(s2, t2) ->
 294         applySubst s2 >>|
 295         case t1 of
 296             VoidType = pure (compose s2 s1, t2)
 297             _ = case t2 of
 298                 VoidType = pure (compose s2 s1, t1)
 299                 _ = lift (unify t1 t2) >>= \s3 ->
 300                     pure (compose s3 $ compose s2 s1, t1)
 301
 302 //the type class inferes the type of an AST element (VarDecl or FunDecl)
 303 //and adds it to the AST element
 304 class type a :: a -> Typing (Substitution, a)
 305
 306 instance type VarDecl where
 307     type (VarDecl p expected k e) =
 308         infer e >>= \(s1, given) ->
 309         applySubst s1 >>|
 310         case expected of
 311             Nothing = pure zero
 312             Just expected_ = lift (unify expected_ given)
 313         >>= \s2->
 314         applySubst s2 >>|
 315         let vtype = subst (compose s2 s1) given in
 316         generalize vtype >>= \t ->
 317         changeGamma (extend k t) >>|
 318         pure (compose s2 s1, VarDecl p (Just vtype) k e)
 319
 320 instance type FunDecl where
 321     type (FunDecl p f args expected vds stmts) =
 322         gamma >>= \outerScope-> //functions are infered in their own scopde
 323         introduce f >>|
 324         mapM introduce args >>= \argTs->
 325         type vds >>= \(s1, tVds)->
 326         applySubst s1 >>|
 327         infer stmts >>= \(s2, result)->
 328         applySubst s1 >>|
 329         let argTs_ = map (subst $ compose s2 s1) argTs in
 330         //abort (concat $ intersperse "\n" $ map toString argTs_) >>|
 331         let given = foldr (->>) result argTs_ in
 332         (case expected of
 333             Nothing = pure zero
 334             Just expected_ = lift (unify expected_ given))
 335         >>= \s3 ->
 336         let ftype = subst (compose s3 $ compose s2 s1) given in
 337         generalize ftype >>= \t->
 338         putGamma outerScope >>|
 339         changeGamma (extend f t) >>|
 340         pure (compose s3 $ compose s2 s1, FunDecl p f args (Just ftype) tVds stmts)
 341
 342 instance type [a] | type a where
 343     type []     = pure (zero, [])
 344     type [v:vs] =
 345         type v >>= \(s1, v_)->
 346         applySubst s1 >>|
 347         type vs >>= \(s2, vs_)->
 348         applySubst (compose s2 s1) >>|
 349         pure (compose s2 s1, [v_:vs_])
 350
 351 introduce :: String -> Typing Type
 352 introduce k =
 353     fresh >>= \tv ->
 354     changeGamma (extend k (Forall [] tv)) >>|
 355     pure tv
 356
 357 instance toString Scheme where
 358     toString (Forall x t) =
 359         concat ["Forall ": intersperse "," x] +++ concat [". ", toString t];
 360
 361 instance toString Gamma where
 362     toString mp =
 363         concat [concat [k, ": ", toString v, "\n"]\\(k, v)<-'Map'.toList mp]
 364
 365 instance toString Substitution where
 366     toString subs =
 367         concat [concat [k, ": ", toString t, "\n"]\\(k, t)<-'Map'.toList subs]
 368
 369 instance toString SemError where
 370     toString (SanityError p e) = concat [toString p,
 371         "SemError: SanityError: ", e]
 372     toString (ParseError p s) = concat [toString p,
 373         "ParseError: ", s]
 374     toString (UnifyError p t1 t2) = concat [toString p,
 375         "Can not unify types, expected|given:\n", toString t1,
 376         "\n", toString t2]
 377     toString (InfiniteTypeError p t) = concat [toString p,
 378         "Infinite type: ", toString t]
 379     toString (FieldSelectorError p t fs) = concat [toString p,
 380         "Can not run fieldselector '", toString fs, "' on type: ",
 381         toString t]
 382     toString (OperatorError p op t) = concat [toString p,
 383         "Operator error, operator '", toString op, "' can not be",
 384         "used on type: ", toString t]
 385     toString (UndeclaredVariableError p k) = concat [toString p,
 386         "Undeclared identifier: ", k]
 387     toString (ArgumentMisMatchError p str) = concat [toString p,
 388         "Argument mismatch: ", str]
 389     toString (Error e) = concat ["Unknown error during semantical",
 390         "analysis: ", e]
 391
 392 instance toString (Maybe a) | toString a where
 393     toString Nothing = "Nothing"
 394     toString (Just e) = concat ["Just ", toString e]
 395
 396 instance MonadTrans (StateT (Gamma, [TVar])) where
 397     liftT m = StateT \s-> m >>= \a-> return (a, s)
 398
 399 Mapmap :: (a->b) ('Map'.Map k a) -> ('Map'.Map k b)
 400 Mapmap _ 'Map'.Tip = 'Map'.Tip
 401 Mapmap f ('Map'.Bin sz k v ml mr) = 'Map'.Bin sz k (f v)
 402                                         (Mapmap f ml)
 403                                         (Mapmap f mr)