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