infer el >>= \(s4, elt)->
applySubst s4 >>|
lift (unify tht elt) >>= \s5->
- pure (compose s5 $ compose s4 $ compose s3 $ compose s1 s2, subst s5 tht)
+ pure (compose s5 $ compose s4 $ compose s3 $ compose s2 s1, subst s5 tht)
WhileStmt e wh =
infer e >>= \(s1, et)->
lift (unify et BoolType) >>= \s2 ->
applySubst (compose s2 s1) >>|
infer wh >>= \(s3, wht)->
- pure (compose s3 $ compose s1 s2, subst s3 wht)
+ pure (compose s3 $ compose s2 s1, subst s3 wht)
AssStmt (VarDef k fs) e =
infer e >>= \(s1, et)->
ReturnStmt Nothing = pure (zero, VoidType)
ReturnStmt (Just e) = infer e
-
+//The type of a list of statements is either an encountered
+//return, or VoidType
instance infer [a] | infer a where
- infer _ = undef
+ infer [] = pure (zero, VoidType)
+ infer [stmt:ss] =
+ infer stmt >>= \(s1, t1) ->
+ infer ss >>= \(s2, t2) ->
+ case t1 of
+ VoidType = pure (compose s2 s1, t2)
+ _ = case t2 of
+ VoidType = pure (compose s2 s1, t1)
+ _ = lift (unify t1 t2) >>= \s3 ->
+ pure (compose s3 $ compose s2 s1, t1)
+
+//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
+
+instance type VarDecl where
+ type (VarDecl p expected k e) =
+ infer e >>= \(s, given) ->
+ applySubst s >>|
+ case expected of
+ Nothing = pure zero
+ Just expected_ = lift (unify expected_ given)
+ >>|
+ generalize given >>= \t ->
+ changeGamma (extend k t) >>|
+ pure (VarDecl p (Just given) k e)
+
+instance type FunDecl where
+ type (FunDecl p f args expected vds stmts) =
+ type vds >>= \tVds->
+ infer stmts >>= \(s, given)->
+ applySubst s >>|
+ (case expected of
+ Nothing = pure zero
+ Just expected_ = lift (unify expected_ given))
+ >>|
+ generalize given >>= \t->
+ changeGamma (extend f t) >>|
+ pure (FunDecl p f args (Just given) tVds stmts)
+
+instance type [a] | type a where
+ type dcls = mapM type dcls
+
-Mapmap :: (a->b) ('Map'.Map k a) -> ('Map'.Map k b)
-Mapmap _ 'Map'.Tip = 'Map'.Tip
-Mapmap f ('Map'.Bin sz k v ml mr) = 'Map'.Bin sz k (f v)
- (Mapmap f ml)
- (Mapmap f mr)
instance toString Scheme where
toString (Forall x t) =
instance MonadTrans (StateT (Gamma, [TVar])) where
liftT m = StateT \s-> m >>= \a-> return (a, s)
+Mapmap :: (a->b) ('Map'.Map k a) -> ('Map'.Map k b)
+Mapmap _ 'Map'.Tip = 'Map'.Tip
+Mapmap f ('Map'.Bin sz k v ml mr) = 'Map'.Bin sz k (f v)
+ (Mapmap f ml)
+ (Mapmap f mr)
+
//// ------------------------
//// First step: Inference
//// ------------------------//