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