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 sem :: AST -> Either [SemError] AST
  52 sem (AST fd) = case foldM (const $ hasNoDups fd) () fd
  53                         >>| foldM (const isNiceMain) () fd
  54                         >>| hasMain fd
  55                     >>| evalStateT (type fd) (zero, variableStream) of
  56         Left e = Left [e]
  57     Right (_,fds) = Right (AST fds)
  58 where
  59                 hasNoDups :: [FunDecl] FunDecl -> Either SemError ()
  60                 hasNoDups fds (FunDecl p n _ _ _ _)
  61                 # mbs = map (\(FunDecl p` n` _ _ _ _)->if (n == n`) (Just p`) Nothing) fds
  62                 = case catMaybes mbs of
  63                         [] = Left $ SanityError p "HUH THIS SHOULDN'T HAPPEN"
  64                         [x] = pure ()
  65                         [_:x] = Left $ SanityError p (concat
  66                                 [n, " multiply defined at ", toString p])
  67
  68                 hasMain :: [FunDecl] -> Either SemError ()
  69                 hasMain [(FunDecl _ "main" _ _ _ _):fd] = pure ()
  70                 hasMain [_:fd] = hasMain fd
  71                 hasMain [] = Left $ SanityError zero "no main function defined"
  72
  73                 isNiceMain :: FunDecl -> Either SemError ()
  74                 isNiceMain (FunDecl p "main" as mt _ _) = case (as, mt) of
  75                         ([_:_], _) = Left $ SanityError p "main must have arity 0"
  76                         ([], t) = (case t of
  77                                 Nothing = pure ()
  78                                 Just VoidType = pure ()
  79                                 _ = Left $ SanityError p "main has to return Void")
  80                 isNiceMain _ = pure ()
  81
  82 class Typeable a where
  83     ftv :: a -> [TVar]
  84     subst :: Substitution a -> a
  85
  86 instance Typeable Scheme where
  87     ftv (Forall bound t) = difference (ftv t) bound
  88     subst s (Forall bound t) = Forall bound $ subst s_ t
  89         where s_ = 'Map'.filterWithKey (\k _ -> not (elem k bound)) s
  90
  91 instance Typeable [a] | Typeable a where
  92     ftv types   = foldr (\t ts-> ftv t ++ ts) [] types
  93     subst s ts  = map (\t->subst s t) ts
  94
  95 instance Typeable Type where
  96     ftv (TupleType (t1, t2))    = ftv t1 ++ ftv t2
  97     ftv (ListType t)            = ftv t
  98     ftv (IdType tvar)           = [tvar]
  99     ftv (t1 ->> t2)             = ftv t1 ++ ftv t2
 100     ftv _                       = []
 101     subst s (TupleType (t1, t2))= TupleType (subst s t1, subst s t2)
 102     subst s (ListType t1)       = ListType (subst s t1)
 103     subst s (t1 ->> t2)         = (subst s t1) ->> (subst s t2)
 104     subst s t1=:(IdType tvar)   = 'Map'.findWithDefault t1 tvar s
 105     subst s t                   = t
 106
 107 instance Typeable Gamma where
 108     ftv gamma       = concatMap id $ map ftv ('Map'.elems gamma)
 109     subst s gamma   = Mapmap (subst s) gamma
 110
 111 extend :: String Scheme Gamma -> Gamma
 112 extend k t g = 'Map'.put k t g
 113
 114 //// ------------------------
 115 //// algorithm U, Unification
 116 //// ------------------------
 117 instance zero Substitution where zero = 'Map'.newMap
 118
 119 compose :: Substitution Substitution -> Substitution
 120 compose s1 s2 = 'Map'.union (Mapmap (subst s1) s2) s1
 121 //Note: just like function compositon compose does snd first
 122
 123 occurs :: TVar a -> Bool | Typeable a
 124 occurs tvar a = elem tvar (ftv a)
 125
 126 unify :: Type Type -> Either SemError Substitution
 127 unify t1 t2=:(IdType tv)    | t1 == (IdType tv) = Right zero
 128                             | occurs tv t1 = Left $ InfiniteTypeError zero t1
 129                             | otherwise = Right $ 'Map'.singleton tv t1
 130 unify t1=:(IdType tv) t2 = unify t2 t1
 131 unify (ta1->>ta2) (tb1->>tb2) = unify ta1 tb1 >>= \s1->
 132                                 unify ta2 tb2 >>= \s2->
 133                                 Right $ compose s1 s2
 134 unify (TupleType (ta1,ta2)) (TupleType (tb1,tb2)) = unify ta1 tb1 >>= \s1->
 135                                                     unify ta2 tb2 >>= \s2->
 136                                                     Right $ compose s1 s2
 137 unify (ListType t1) (ListType t2) = unify t1 t2
 138 unify t1 t2 | t1 == t2  = Right zero
 139             | otherwise = Left $ UnifyError zero t1 t2
 140
 141 //// ------------------------
 142 //// Algorithm M, Inference and Solving
 143 //// ------------------------
 144 gamma :: Typing Gamma
 145 gamma = gets fst
 146 putGamma :: Gamma -> Typing ()
 147 putGamma g = modify (appFst $ const g) >>| pure ()
 148 changeGamma :: (Gamma -> Gamma) -> Typing Gamma
 149 changeGamma f = modify (appFst f) >>| gamma
 150 withGamma :: (Gamma -> a) -> Typing a
 151 withGamma f = f <$> gamma
 152 fresh :: Typing Type
 153 fresh = gets snd >>= \vars->
 154         modify (appSnd $ const $ tail vars) >>|
 155         pure (IdType (head vars))
 156
 157 lift :: (Either SemError a) -> Typing a
 158 lift (Left e) = liftT $ Left e
 159 lift (Right v) = pure v
 160
 161 //instantiate maps a schemes type variables to variables with fresh names
 162 //and drops the quantification: i.e. forall a,b.a->[b] becomes c->[d]
 163 instantiate :: Scheme -> Typing Type
 164 instantiate (Forall bound t) =
 165     mapM (const fresh) bound >>= \newVars->
 166     let s = 'Map'.fromList (zip (bound,newVars)) in
 167     pure (subst s t)
 168
 169 //generalize quentifies all free type variables in a type which are not
 170 //in the gamma
 171 generalize :: Type -> Typing Scheme
 172 generalize t = gamma >>= \g-> pure $ Forall (difference (ftv t) (ftv g)) t
 173
 174 lookup :: String -> Typing Type
 175 lookup "isEmpty" = ListType <$> fresh
 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 = pure (zero, VoidType)
 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)