import Control.Monad => qualified join
import Control.Monad.State
import Control.Monad.Trans
+import Control.Monad.Writer
import Data.Either
import Data.Func
import Data.List
+import Data.Tuple
import Data.Map => qualified put, union, difference, find, updateAt
import Data.Maybe
-import Data.Tuple
import Text
-import ast
+import ast, scc
+
+import StdDebug
-check :: [Function] -> Either [String] (Expression, Scheme)
-check fs
- # dups = filter (\x->length x > 1) (groupBy (\(Function i _ _) (Function j _ _)->i == j) fs)
+check :: ![Either TypeDef Function] -> Either [String] (Expression, [([Char], Scheme)])
+check tdfs
+ # dups = filter (\x->length x > 1) (groupBy (\(Function i _ _) (Function j _ _)->i == j) functions)
| length dups > 0 = Left ["Duplicate functions: ":[toString n\\[(Function n _ _):_]<-dups]]
- = case partition (\a->a=:(Function ['start'] _ _)) fs of
+ = case partition (\a->a=:(Function ['start'] _ _)) functions of
([], _) = Left ["No start function defined"]
- ([Function _ [] e], fs)
-// = (\x->(e, x)) <$> runInfer (infer preamble (makeExpression fs e))
- = pure (makeExpression fs e, undef)
- ([Function _ _ _], _) = Left ["Start cannot have arguments"]
-
-
-:: Node a :== (a, [a])
-:: SCCState a =
- { index :: Int
- , stack :: [a]
- , map :: Map a (Int, Int, Bool)
- , sccs :: [[a]]
- }
-
-import StdDebug
-import Text.GenPrint
-scc :: [Node a] -> [[a]] | Eq, Ord a
-scc nodes = (foldr scc` {index=0,stack=[],map=newMap,sccs=[]} nodes).sccs
+ ([Function _ [] e:_], fs)
+ # e = makeExpression fs e
+ = tuple e <$> runInfer (infer (fromList (conses ++ builtin)) e)
+ ([Function _ _ _:_], _) = Left ["Start cannot have arguments"]
where
-// scc` :: (Node a) (SCCState a) -> SCCState a | Eq, Ord a
- scc` (v, suc) s = maybe (strongconnect s (v, suc)) (\_->s) $ get v s.map
-
-// strongconnect :: (SCCState a) (Node a)-> SCCState a | Eq, Ord a
- strongconnect s (v, suc)
- # s = flip (foldr processSucc) suc
- { s
- & map = 'Data.Map'.put v (s.index, s.index, True) s.map
- , stack = [v:s.stack]
- , index = s.index + 1
- }
- # (Just (iv, lv, lo)) = get v s.map
- | iv == lv
- # (scc, [sl:stack]) = span ((<>) v) s.stack
- # scc = scc ++ [sl]
- = { s
- & sccs = [scc:s.sccs]
- , stack= stack
- , map = foldr (\w m->'Data.Map'.put w (appThd3 (\_->False) $ fromJust (get w m)) m) s.map scc
- }
- = s
- where
-// processSucc :: a (SCCState a) -> SCCState a | Eq, Ord a
- processSucc w s = case get w s.map of
- Nothing
- # s = strongconnect s $ hd [l\\l=:(n, _)<-nodes | n == w]
- # (Just (iw, lw, ow)) = get w s.map
- # (Just (iv, lv, ov)) = get v s.map
- = {s & map='Data.Map'.put v (iv, min lv lw, ov) s.map}
- Just (iw, lw, True)
- # (Just (iv, lv, ov)) = get v s.map
- = {s & map='Data.Map'.put v (iv, min iw lv, ov) s.map}
- Just _ = s
+ functions = rights tdfs
+ conses = flatten $ map (\(TypeDef n t cs)->
+ let cons = Forall t o foldr (-->) (foldl TApp (TVar n) (map TVar t))
+ in map (appSnd cons) cs) $ lefts tdfs
+ builtin =
+ [(['_if'], Forall [['a']] $ TBool --> TVar ['a'] --> TVar ['a'] --> TVar ['a'])
+ ,(['_eq'], Forall [] $ TInt --> TInt --> TBool)
+ ,(['_mul'], Forall [] $ TInt --> TInt --> TInt)
+ ,(['_add'], Forall [] $ TInt --> TInt --> TInt)
+ ,(['_sub'], Forall [] $ TInt --> TInt --> TInt)
+ ,(['_div'], Forall [] $ TInt --> TInt --> TInt)
+ ]
makeExpression :: [Function] Expression -> Expression
-makeExpression fs start
- = mkExpr $ scc [(l, vars e [])\\(l, e)<-nicefuns]
+makeExpression fs start = foldr mkExpr start $ scc $ map (appSnd vars) nicefuns
where
- mkExpr :: [[[Char]]] -> Expression
- mkExpr t = trace_n (printToString t) start
+ mkExpr :: [[Char]] -> (Expression -> Expression)
+ mkExpr scc = Let [(l, e)\\(l, e)<-nicefuns, s<-scc | s == l]
+
+ nicefuns :: [([Char], Expression)]
nicefuns = [(l, foldr ((o) o Lambda) id i e)\\(Function l i e)<-fs]
- vars :: Expression [[Char]] -> [[Char]]
- vars (Var v=:[m:_]) c
- | m <> '_' = [v:c]
- vars (App l r) c = vars l $ vars r c
- vars (Lambda l e) c = [v\\v<-vars e c | v <> l]
- vars (Let ns e) c = vars e c // TODO
- vars _ c = c
+ vars :: Expression -> [[Char]]
+ vars (Var v) = [v]
+ vars (App l r) = vars l ++ vars r
+ vars (Lambda l e) = flt l e
+ vars (Let ns e) = flatten [[v\\v<-vars e | not (isMember v (map fst ns))]:map (uncurry flt) ns]
+ vars _ = []
+
+ flt i e = [v\\v<-vars e | v <> i]
instance toString Scheme where
toString (Forall [] t) = toString t
toString (Forall as t) = concat ["A.", join " " (map toString as), ": ", toString t]
-instance toString Type where
- toString (TVar a) = toString a
- toString TInt = "Int"
- toString TBool = "Bool"
- toString (a --> b) = concat ["(", toString a, ") -> ", toString b]
-
:: TypeEnv :== Map [Char] Scheme
-preamble :: TypeEnv
-preamble = fromList
- [(['_if'], Forall [['_ift']]
- $ TBool --> TVar ['_ift'] --> TVar ['_ift'] --> TVar ['_ift'])
- ,(['_eq'], Forall [['_eq']] $ TInt --> TInt --> TBool)
- ,(['_mul'], Forall [['_mul']] $ TInt --> TInt --> TInt)
- ,(['_add'], Forall [['_add']] $ TInt --> TInt --> TInt)
- ,(['_sub'], Forall [['_sub']] $ TInt --> TInt --> TInt)
- ]
:: Subst :== Map [Char] Type
-:: Infer a :== StateT [Int] (Either [String]) a
-runInfer :: (Infer (Subst, Type)) -> Either [String] Scheme
-runInfer i = uncurry ((o) (generalize newMap) o apply)
- <$> evalStateT i [0..]
+:: Infer a :== StateT [Int] (WriterT [([Char], Scheme)] (Either [String])) a
+
+runInfer :: (Infer (Subst, Type)) -> Either [String] [([Char], Scheme)]
+runInfer i = case runWriterT (evalStateT i [0..]) of
+ Left e = Left e
+ Right ((s, t), w) = pure [(['start'], generalize newMap (apply s t)):w]
fresh :: Infer Type
fresh = getState >>= \[s:ss]->put ss >>| pure (TVar (['v':[c\\c<-:toString s]]))
instance Substitutable Type where
apply s t=:(TVar v) = fromMaybe t (get v s)
apply s (t1 --> t2) = apply s t1 --> apply s t2
+ apply s (TApp t1 t2) = TApp (apply s t1) (apply s t2)
apply _ x = x
ftv (TVar v) = [v]
ftv (t1 --> t2) = on union ftv t1 t2
+ ftv (TApp t1 t2) = on union ftv t1 t2
ftv _ = []
instance Substitutable Scheme where
occursCheck :: [Char] -> (a -> Bool) | Substitutable a
occursCheck a = isMember a o ftv
+err :: [String] -> Infer a
+err e = liftT (liftT (Left e))
+
unify :: Type Type -> Infer Subst
unify (l --> r) (l` --> r`)
= unify l l`
unify (TVar a) (TVar t)
| a == t = pure newMap
unify (TVar a) t
- | occursCheck a t = liftT (Left ["Infinite type: ", toString a, " to ", toString t])
+ | occursCheck a t = err ["Infinite type: ", toString a, " to ", toString t]
= pure (singleton a t)
unify t (TVar a) = unify (TVar a) t
unify TInt TInt = pure newMap
unify TBool TBool = pure newMap
-unify t1 t2 = liftT (Left ["Cannot unify: ", toString t1, " with ", toString t2])
+unify (TApp l r) (TApp l` r`)
+ = unify l l`
+ >>= \s1->on unify (apply s1) r r`
+ >>= \s2->pure (s1 oo s2)
+unify t1 t2 = err ["Cannot unify: ", toString t1, " with ", toString t2]
+
+unifyl :: [Type] -> Infer Subst
+unifyl [t1,t2:ts] = unify t1 t2 >>= \s->unifyl (map (apply s) [t2:ts])
+unifyl _ = pure newMap
instantiate :: Scheme -> Infer Type
instantiate (Forall as t)
infer :: TypeEnv Expression -> Infer (Subst, Type)
infer env (Lit (Int _)) = pure (newMap, TInt)
infer env (Lit (Bool _)) = pure (newMap, TBool)
-infer env (Var x) = case get x env of
- Nothing = liftT (Left ["Unbound variable: ", toString x])
- Just s = (\x->(newMap, x)) <$> instantiate s
+infer env (Var x) = maybe (err ["Unbound variable: ", toString x])
+ (\s->tuple newMap <$> instantiate s) $ get x env
infer env (App e1 e2)
= fresh
>>= \tv-> infer env e1
>>= \(s1, t1)->infer (apply s1 env) e2
>>= \(s2, t2)->unify (apply s2 t1) (t2 --> tv)
- >>= \s3-> pure (s1 oo s2 oo s3, apply s3 tv)
+ >>= \s3-> pure (s3 oo s2 oo s1, apply s3 tv)
infer env (Lambda x b)
= fresh
>>= \tv-> infer ('Data.Map'.put x (Forall [] tv) env) b
>>= \(s1, t1)->pure (s1, apply s1 tv --> t1)
+//Non recursion
//infer env (Let [(x, e1)] e2)
// = infer env e1
// >>= \(s1, t1)->infer ('Data.Map'.put x (generalize (apply s1 env) t1) env) e2
+// >>= \(s2, t2)->liftT (tell [(x, Forall [] t1)])
+// >>| pure (s1 oo s2, t2)
+//Single recursion
+//infer env (Let [(x, e1)] e2)
+// = fresh
+// >>= \tv-> let env` = 'Data.Map'.put x (Forall [] tv) env
+// in infer env` e1
+// >>= \(s1,t1)-> infer ('Data.Map'.put x (generalize (apply s1 env`) t1) env`) e2
// >>= \(s2, t2)->pure (s1 oo s2, t2)
-infer env (Let [(x, e1)] e2)
- = fresh
- >>= \tv-> let env` = 'Data.Map'.put x (Forall [] tv) env
- in infer env` e1
- >>= \(s1,t1)-> unify t1 tv
- >>= \t->infer ('Data.Map'.put x (generalize (apply s1 env`) t1) env`) e2
- >>= \(s2, t2)->pure (s1 oo s2, t2)
-//infer env (Let xs e2)
-// # (ns, bs) = unzip xs
-// = sequence [fresh\\_<-ns]
-// >>= \tvs-> let env` = foldr (uncurry putenv) env (zip2 ns tvs)
-// in unzip <$> sequence (map infer env`) bs
-// >>= \(ss,ts)-> let s = foldr (oo) newMap ss
-// in //unify t1 tv
-// >>= \t->infer ('Data.Map'.put x (generalize (apply s1 env`) t1) env`) e2
-// >>= \(s2, t2)->pure (s1 oo s2, t2)
-where
- putenv :: [Char] -> (Type TypeEnv -> TypeEnv)
- putenv k = 'Data.Map'.put k o Forall []
-
-unifyl :: [Type] -> Infer Subst
-unifyl [t1,t2:ts] = unify t1 t2 >>= \s->unifyl [t2:map (apply s) ts]
-unifyl _ = pure newMap
+//Multiple recursion
+infer env (Let xs e2)
+ # (ns, bs) = unzip xs
+ = sequence [fresh\\_<-ns]
+ >>= \tvs-> let env` = foldr (\(k, v)->'Data.Map'.put k (Forall [] v)) env (zip2 ns tvs)
+ in unzip <$> sequence (map (infer env`) bs)
+ >>= \(ss,ts)-> unifyl ts
+ >>= \s-> liftT (tell [(n, generalize (apply s env`) t)\\t<-ts & n<-ns])
+ >>| let env`` = foldr (\(n, s, t) m->'Data.Map'.put n (generalize (apply s env`) t) m) env` (zip3 ns ss ts)
+ in infer env`` e2
+ >>= \(s2, t2)->pure (s oo s2, t2)
repositories / minfp.git / blobdiff