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 s1 s2, 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 s1 s2, 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
 305 instance infer [a] | infer a where
 306     infer _ = undef
 307
 308 Mapmap :: (a->b) ('Map'.Map k a) -> ('Map'.Map k b)
 309 Mapmap _ 'Map'.Tip = 'Map'.Tip
 310 Mapmap f ('Map'.Bin sz k v ml mr) = 'Map'.Bin sz k (f v)
 311                                         (Mapmap f ml)
 312                                         (Mapmap f mr)
 313
 314 instance toString Scheme where
 315     toString (Forall x t) =
 316         concat ["Forall ": map ((+++) "\n") x] +++ toString t
 317
 318 instance toString Gamma where
 319     toString mp =
 320         concat [concat [k, ": ", toString v, "\n"]\\(k, v)<-'Map'.toList mp]
 321
 322 instance toString SemError where
 323     toString (SanityError p e) = concat [toString p,
 324         "SemError: SanityError: ", e]
 325     toString se = "SemError: "
 326
 327 instance MonadTrans (StateT (Gamma, [TVar])) where
 328     liftT m = StateT \s-> m >>= \a-> return (a, s)
 329
 330 //// ------------------------
 331 //// First step: Inference
 332 //// ------------------------//
 333
 334 //unify :: Type Type -> Infer ()
 335 //unify t1 t2 = tell [(t1, t2)]//
 336
 337 //fresh :: Infer Type
 338 //fresh = (gets id) >>= \vars-> (put $ tail vars) >>| (pure $ IdType $ head vars)//
 339
 340 //op2Type :: Op2 -> Infer Type
 341 //op2Type op
 342 //| elem op [BiPlus, BiMinus, BiTimes, BiDivide, BiMod]
 343 //      = pure (IntType ->> IntType ->> IntType)
 344 //| elem op [BiEquals, BiUnEqual]
 345 //      = fresh >>= \t1-> fresh >>= \t2-> pure (t1 ->> t2 ->> BoolType)
 346 //| elem op [BiLesser, BiGreater, BiLesserEq, BiGreaterEq]
 347 //      = pure (IntType ->> IntType ->> BoolType)
 348 //| elem op [BiAnd, BiOr]
 349 //      = pure (BoolType ->> BoolType ->> BoolType)
 350 //| op == BiCons
 351 //      = fresh >>= \t1-> pure (t1 ->> ListType t1 ->> ListType t1)//
 352
 353 //op1Type :: Op1 -> Infer Type
 354 //op1Type UnNegation = pure $ (BoolType ->> BoolType)
 355 //op1Type UnMinus = pure $ (IntType ->> IntType)//
 356
 357 ////instantiate :: Scheme -> Infer Type
 358 ////instantiate (Forall as t) = mapM (const fresh) as//
 359
 360 //lookupEnv :: String -> Infer Type
 361 //lookupEnv ident = asks ('Map'.get ident)
 362 //      >>= \m->case m of
 363 //              Nothing = liftT $ Left $ UndeclaredVariableError zero ident
 364 //              Just (Forall as t) = pure t //instantiate ???//
 365
 366 //class infer a :: a -> Infer Type
 367 //instance infer Expr where
 368 //      infer (VarExpr _ (VarDef ident fs)) = lookupEnv ident
 369 //    infer (Op2Expr _ e1 op e2) =
 370 //        infer e1 >>= \t1 ->
 371 //        infer e2 >>= \t2 ->
 372 //        fresh >>= \frsh ->
 373 //        let given = t1 ->> (t2 ->> frsh) in
 374 //        op2Type op >>= \expected ->
 375 //        unify expected given >>|
 376 //        return frsh
 377 //      infer (Op1Expr _ op e) =
 378 //        infer e >>= \t1 ->
 379 //        fresh >>= \frsh ->
 380 //        let given = t1 ->> frsh in
 381 //        op1Type op >>= \expected ->
 382 //        unify expected given >>|
 383 //        pure frsh
 384 //      infer (IntExpr _ _) = pure IntType
 385 //      infer (CharExpr _ _) = pure CharType
 386 //      infer (BoolExpr _ _) = pure BoolType
 387 //      infer (FunExpr _ f args sels) =  //todo, iets met field selectors
 388 //        lookupEnv f >>= \expected ->
 389 //        fresh >>= \frsh ->
 390 //        mapM infer args >>= \argTypes ->
 391 //        let given = foldr (->>) frsh argTypes in
 392 //        unify expected given >>|
 393 //        pure frsh
 394 //      infer (EmptyListExpr _) = ListType <$> fresh
 395 //      infer (TupleExpr _ (e1, e2)) =
 396 //              infer e1 >>= \et1->infer e2 >>= \et2->pure $ TupleType (et1, et2)//
 397
 398 ////:: VarDef = VarDef String [FieldSelector]
 399 ////:: FieldSelector = FieldHd | FieldTl | FieldFst | FieldSnd
 400 ////:: Op1 = UnNegation | UnMinus
 401 ////:: Op2 = BiPlus | BiMinus | BiTimes | BiDivide | BiMod | BiEquals | BiLesser |
 402 ////    BiGreater | BiLesserEq | BiGreaterEq | BiUnEqual | BiAnd | BiOr | BiCons
 403 ////:: FunDecl = FunDecl Pos String [String] (Maybe Type) [VarDecl] [Stmt]
 404 ////:: FunCall = FunCall String [Expr]
 405 ////:: Stmt
 406 ////    = IfStmt Expr [Stmt] [Stmt]
 407 ////    | WhileStmt Expr [Stmt]
 408 ////    | AssStmt VarDef Expr
 409 ////    | FunStmt FunCall
 410 ////    | ReturnStmt (Maybe Expr)
 411 ////:: Pos = {line :: Int, col :: Int}
 412 ////:: AST = AST [VarDecl] [FunDecl]
 413 ////:: VarDecl = VarDecl Pos Type String Expr
 414 ////:: Type
 415 ////    = TupleType (Type, Type)
 416 ////    | ListType Type
 417 ////    | IdType String
 418 ////    | IntType
 419 ////    | BoolType
 420 ////    | CharType
 421 ////    | VarType
 422 ////    | VoidType
 423 ////    | (->>) infixl 7 Type Type