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