import AST
-
:: Scheme = Forall [TVar] Type
:: Gamma :== 'Map'.Map String Scheme //map from Variables! to types
:: Typing a :== StateT (Gamma, [TVar]) (Either SemError) a
variableStream :: [TVar]
variableStream = map toString [1..]
+defaultGamma :: Gamma //includes all default functions
+defaultGamma = extend "print" (Forall ["a"] ((IdType "a") ->> VoidType))
+ $ extend "isEmpty" (Forall ["a"] ((ListType (IdType "a")) ->> BoolType))
+ $ extend "read" (Forall [] (FuncType CharType))
+ zero
+
sem :: AST -> Either [SemError] AST
sem (AST fd) = case foldM (const $ hasNoDups fd) () fd
>>| foldM (const isNiceMain) () fd
>>| hasMain fd
- >>| evalStateT (type fd) (zero, variableStream) of
+ >>| evalStateT (type fd) (defaultGamma, variableStream) of
Left e = Left [e]
- Right fds = Right (AST fds)
+ Right (_,fds) = Right (AST fds)
where
hasNoDups :: [FunDecl] FunDecl -> Either SemError ()
hasNoDups fds (FunDecl p n _ _ _ _)
ftv (TupleType (t1, t2)) = ftv t1 ++ ftv t2
ftv (ListType t) = ftv t
ftv (IdType tvar) = [tvar]
+ ftv (FuncType t) = ftv t
ftv (t1 ->> t2) = ftv t1 ++ ftv t2
ftv _ = []
subst s (TupleType (t1, t2))= TupleType (subst s t1, subst s t2)
subst s (ListType t1) = ListType (subst s t1)
+ subst s (FuncType t) = FuncType (subst s t)
subst s (t1 ->> t2) = (subst s t1) ->> (subst s t2)
subst s t1=:(IdType tvar) = 'Map'.findWithDefault t1 tvar s
subst s t = t
unify ta2 tb2 >>= \s2->
Right $ compose s1 s2
unify (ListType t1) (ListType t2) = unify t1 t2
+unify (FuncType t1) (FuncType t2) = unify t1 t2
unify t1 t2 | t1 == t2 = Right zero
| otherwise = Left $ UnifyError zero t1 t2
instance infer Expr where
infer e = case e of
- VarExpr _ (VarDef k fs) = (\t->(zero,t)) <$> lookup k
- //instantiate is key for the let polymorphism!
- //TODO: field selectors
+ VarExpr _ (VarDef k fs) = lookup k >>= \t ->
+ foldM foldFieldSelectors t fs >>= \finalT ->
+ pure (zero, finalT)
Op2Expr _ e1 op e2 =
infer e1 >>= \(s1, t1) ->
lookup f >>= \expected ->
let accST = (\(s,ts) e->infer e >>= \(s_,et)->pure (compose s_ s,ts++[et])) in
foldM accST (zero,[]) args >>= \(s1, argTs)->
- fresh >>= \tv->
- let given = foldr (->>) tv argTs in
- lift (unify expected given) >>= \s2->
- pure (compose s2 s1, subst s2 tv)
+ fresh >>= \tv->case expected of
+ FuncType t = pure (s1, t)
+ _ = (let given = foldr (->>) tv argTs in
+ lift (unify expected given) >>= \s2->
+ let fReturnType = subst s2 tv in
+ foldM foldFieldSelectors fReturnType fs >>= \returnType ->
+ pure (compose s2 s1, returnType))
IntExpr _ _ = pure $ (zero, IntType)
BoolExpr _ _ = pure $ (zero, BoolType)
CharExpr _ _ = pure $ (zero, CharType)
+foldFieldSelectors :: Type FieldSelector -> Typing Type
+foldFieldSelectors (ListType t) (FieldHd) = pure t
+foldFieldSelectors t=:(ListType _) (FieldTl) = pure t
+foldFieldSelectors (TupleType (t1, _)) (FieldFst) = pure t1
+foldFieldSelectors (TupleType (_, t2)) (FieldSnd) = pure t2
+foldFieldSelectors t fs = liftT $ Left $ FieldSelectorError zero t fs
op2Type :: Op2 -> Typing Type
op2Type op
pure (compose s3 $ compose s2 s1, subst s3 wht)
AssStmt (VarDef k fs) e =
- infer e >>= \(s1, et)->
- applySubst s1 >>|
- changeGamma (extend k (Forall [] et)) >>| //todo: fieldselectors
- pure (s1, VoidType)
+ lookup k >>= \expected ->
+ infer e >>= \(s1, given)->
+ foldM reverseFs given (reverse fs) >>= \varType->
+ lift (unify expected varType) >>= \s2->
+ let s = compose s2 s1 in
+ applySubst s >>|
+ changeGamma (extend k (Forall [] (subst s varType))) >>|
+ pure (s, VoidType)
- FunStmt f es = undef //what is this?
+ FunStmt f es _ = pure (zero, VoidType)
ReturnStmt Nothing = pure (zero, VoidType)
ReturnStmt (Just e) = infer e
+reverseFs :: Type FieldSelector -> Typing Type
+reverseFs t FieldHd = pure $ ListType t
+reverseFs t FieldTl = pure $ ListType t
+reverseFs t FieldFst = fresh >>= \tv -> pure $ TupleType (t, tv)
+reverseFs t FieldSnd = fresh >>= \tv -> pure $ TupleType (tv, t)
+
//The type of a list of statements is either an encountered
//return, or VoidType
instance infer [a] | infer a where
//the type class inferes the type of an AST element (VarDecl or FunDecl)
//and adds it to the AST element
-class type a :: a -> Typing a
+class type a :: a -> Typing (Substitution, a)
instance type VarDecl where
type (VarDecl p expected k e) =
let vtype = subst (compose s2 s1) given in
generalize vtype >>= \t ->
changeGamma (extend k t) >>|
- pure (VarDecl p (Just vtype) k e)
+ pure (compose s2 s1, VarDecl p (Just vtype) k e)
instance type FunDecl where
type (FunDecl p f args expected vds stmts) =
+ gamma >>= \outerScope-> //functions are infered in their own scopde
introduce f >>|
mapM introduce args >>= \argTs->
- type vds >>= \tVds->
- infer stmts >>= \(s1, result)->
- let given = foldr (->>) result argTs in
+ type vds >>= \(s1, tVds)->
+ applySubst s1 >>|
+ infer stmts >>= \(s2, result)->
applySubst s1 >>|
+ let argTs_ = map (subst $ compose s2 s1) argTs in
+ //abort (concat $ intersperse "\n" $ map toString argTs_) >>|
+ let given = foldr (->>) result argTs_ in
(case expected of
Nothing = pure zero
Just expected_ = lift (unify expected_ given))
- >>= \s2 ->
- let ftype = subst (compose s2 s1) given in
+ >>= \s3 ->
+ let ftype = subst (compose s3 $ compose s2 s1) given in
generalize ftype >>= \t->
+ putGamma outerScope >>|
changeGamma (extend f t) >>|
- pure (FunDecl p f args (Just ftype) tVds stmts)
-
-instance toString (Maybe a) | toString a where
- toString Nothing = "Nothing"
- toString (Just e) = concat ["Just ", toString e]
+ pure (compose s3 $ compose s2 s1, FunDecl p f args (Just ftype) tVds stmts)
instance type [a] | type a where
- type dcls = mapM type dcls
+ type [] = pure (zero, [])
+ type [v:vs] =
+ type v >>= \(s1, v_)->
+ applySubst s1 >>|
+ type vs >>= \(s2, vs_)->
+ applySubst (compose s2 s1) >>|
+ pure (compose s2 s1, [v_:vs_])
introduce :: String -> Typing Type
introduce k =
toString (Error e) = concat ["Unknown error during semantical",
"analysis: ", e]
+instance toString (Maybe a) | toString a where
+ toString Nothing = "Nothing"
+ toString (Just e) = concat ["Just ", toString e]
+
instance MonadTrans (StateT (Gamma, [TVar])) where
liftT m = StateT \s-> m >>= \a-> return (a, s)
repositories / cc1516.git / blobdiff