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