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