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