tuples
[minfp.git] / check.icl
1 implementation module check
2
3 import StdEnv
4
5 import Control.Monad => qualified join
6 import Control.Monad.State
7 import Control.Monad.Trans
8 import Control.Monad.Writer
9 import Data.Either
10 import Data.Func
11 import Data.List
12 import Data.Tuple
13 import Data.Map => qualified put, union, difference, find, updateAt
14 import Data.Maybe
15 import Text
16
17 import ast, scc
18
19 check :: [Function] -> Either [String] (Expression, [([Char], Scheme)])
20 check fs
21 # dups = filter (\x->length x > 1) (groupBy (\(Function i _ _) (Function j _ _)->i == j) fs)
22 | length dups > 0 = Left ["Duplicate functions: ":[toString n\\[(Function n _ _):_]<-dups]]
23 = case partition (\a->a=:(Function ['start'] _ _)) fs of
24 ([], _) = Left ["No start function defined"]
25 ([Function _ [] e:_], fs)
26 # e = makeExpression fs e
27 = (\x->(e, x)) <$> runInfer (infer (fromList builtin) e)
28 ([Function _ _ _:_], _) = Left ["Start cannot have arguments"]
29 where
30 builtin =
31 [(['_if'], Forall [['a']] $ TBool --> TVar ['a'] --> TVar ['a'] --> TVar ['a'])
32 ,(['_fst'], Forall [['a'], ['b']] $ TTuple (TVar ['a']) (TVar ['b']) --> TVar ['a'])
33 ,(['_snd'], Forall [['a'], ['b']] $ TTuple (TVar ['a']) (TVar ['b']) --> TVar ['b'])
34 ,(['_eq'], Forall [] $ TInt --> TInt --> TBool)
35 ,(['_mul'], Forall [] $ TInt --> TInt --> TInt)
36 ,(['_add'], Forall [] $ TInt --> TInt --> TInt)
37 ,(['_sub'], Forall [] $ TInt --> TInt --> TInt)
38 ,(['_div'], Forall [] $ TInt --> TInt --> TInt)
39 ]
40
41 makeExpression :: [Function] Expression -> Expression
42 makeExpression fs start = foldr mkExpr start $ scc $ map (appSnd vars) nicefuns
43 where
44 mkExpr :: [[Char]] -> (Expression -> Expression)
45 mkExpr scc = Let [(l, e)\\(l, e)<-nicefuns, s<-scc | s == l]
46
47 nicefuns :: [([Char], Expression)]
48 nicefuns = [(l, foldr ((o) o Lambda) id i e)\\(Function l i e)<-fs]
49
50 vars :: Expression -> [[Char]]
51 vars (Var v) = [v]
52 vars (App l r) = vars l ++ vars r
53 vars (Lambda l e) = flt l e
54 vars (Let ns e) = flatten [[v\\v<-vars e | not (isMember v (map fst ns))]:map (uncurry flt) ns]
55 vars _ = []
56
57 flt i e = [v\\v<-vars e | v <> i]
58
59 instance toString Scheme where
60 toString (Forall [] t) = toString t
61 toString (Forall as t) = concat ["A.", join " " (map toString as), ": ", toString t]
62
63 instance toString Type where
64 toString (TVar a) = toString a
65 toString (TTuple a b) = concat ["(", toString a, ",", toString b, ")"]
66 toString TInt = "Int"
67 toString TBool = "Bool"
68 toString (a --> b) = concat ["(", toString a, " -> ", toString b, ")"]
69
70 :: TypeEnv :== Map [Char] Scheme
71 :: Subst :== Map [Char] Type
72
73 :: Infer a :== StateT [Int] (WriterT [([Char], Scheme)] (Either [String])) a
74
75 runInfer :: (Infer (Subst, Type)) -> Either [String] [([Char], Scheme)]
76 runInfer i = case runWriterT (evalStateT i [0..]) of
77 Left e = Left e
78 Right ((s, t), w) = pure [(['start'], generalize newMap (apply s t)):w]
79
80 fresh :: Infer Type
81 fresh = getState >>= \[s:ss]->put ss >>| pure (TVar (['v':[c\\c<-:toString s]]))
82
83 (oo) infixl 9 :: Subst Subst -> Subst
84 (oo) s1 s2 = 'Data.Map'.union (apply s1 <$> s2) s1
85
86 class Substitutable a where
87 apply :: Subst a -> a
88 ftv :: a -> [[Char]]
89
90 instance Substitutable Type where
91 apply s t=:(TVar v) = fromMaybe t (get v s)
92 apply s (t1 --> t2) = apply s t1 --> apply s t2
93 apply _ x = x
94
95 ftv (TVar v) = [v]
96 ftv (t1 --> t2) = on union ftv t1 t2
97 ftv _ = []
98
99 instance Substitutable Scheme where
100 apply s (Forall as t) = Forall as $ apply (foldr del s as) t
101 ftv (Forall as t) = difference (ftv t) (removeDup as)
102
103 instance Substitutable TypeEnv where
104 apply s env = apply s <$> env
105 ftv env = ftv (elems env)
106
107 instance Substitutable [a] | Substitutable a where
108 apply s l = apply s <$> l
109 ftv t = foldr (union o ftv) [] t
110
111 occursCheck :: [Char] -> (a -> Bool) | Substitutable a
112 occursCheck a = isMember a o ftv
113
114 err :: [String] -> Infer a
115 err e = liftT (liftT (Left e))
116
117 unify :: Type Type -> Infer Subst
118 unify (l --> r) (l` --> r`)
119 = unify l l`
120 >>= \s1->on unify (apply s1) r r`
121 >>= \s2->pure (s1 oo s2)
122 unify (TVar a) (TVar t)
123 | a == t = pure newMap
124 unify (TVar a) t
125 | occursCheck a t = err ["Infinite type: ", toString a, " to ", toString t]
126 = pure (singleton a t)
127 unify t (TVar a) = unify (TVar a) t
128 unify TInt TInt = pure newMap
129 unify TBool TBool = pure newMap
130 unify (TTuple l r) (TTuple l` r`)
131 = unify l l`
132 >>= \s1->on unify (apply s1) r r`
133 >>= \s2->pure (s1 oo s2)
134 unify t1 t2 = err ["Cannot unify: ", toString t1, " with ", toString t2]
135
136 unifyl :: [Type] -> Infer Subst
137 unifyl [t1,t2:ts] = unify t1 t2 >>= \s->unifyl (map (apply s) [t2:ts])
138 unifyl _ = pure newMap
139
140 instantiate :: Scheme -> Infer Type
141 instantiate (Forall as t)
142 = sequence [fresh\\_<-as]
143 >>= \as`->pure (apply (fromList $ zip2 as as`) t)
144
145 generalize :: TypeEnv Type -> Scheme
146 generalize env t = Forall (difference (ftv t) (ftv env)) t
147
148 infer :: TypeEnv Expression -> Infer (Subst, Type)
149 infer env (Lit (Int _)) = pure (newMap, TInt)
150 infer env (Lit (Bool _)) = pure (newMap, TBool)
151 infer env (Var x) = maybe (err ["Unbound variable: ", toString x])
152 (\s->tuple newMap <$> instantiate s) $ get x env
153 infer env (App e1 e2)
154 = fresh
155 >>= \tv-> infer env e1
156 >>= \(s1, t1)->infer (apply s1 env) e2
157 >>= \(s2, t2)->unify (apply s2 t1) (t2 --> tv)
158 >>= \s3-> pure (s3 oo s2 oo s1, apply s3 tv)
159 infer env (Tuple a b)
160 = infer env a
161 >>= \(s1, t1)->infer env b
162 >>= \(s2, t2)->pure (s1 oo s2, TTuple t1 t2)
163 infer env (Lambda x b)
164 = fresh
165 >>= \tv-> infer ('Data.Map'.put x (Forall [] tv) env) b
166 >>= \(s1, t1)->pure (s1, apply s1 tv --> t1)
167 //Non recursion
168 //infer env (Let [(x, e1)] e2)
169 // = infer env e1
170 // >>= \(s1, t1)->infer ('Data.Map'.put x (generalize (apply s1 env) t1) env) e2
171 // >>= \(s2, t2)->liftT (tell [(x, Forall [] t1)])
172 // >>| pure (s1 oo s2, t2)
173 //Single recursion
174 //infer env (Let [(x, e1)] e2)
175 // = fresh
176 // >>= \tv-> let env` = 'Data.Map'.put x (Forall [] tv) env
177 // in infer env` e1
178 // >>= \(s1,t1)-> infer ('Data.Map'.put x (generalize (apply s1 env`) t1) env`) e2
179 // >>= \(s2, t2)->pure (s1 oo s2, t2)
180 //Multiple recursion
181 infer env (Let xs e2)
182 # (ns, bs) = unzip xs
183 = sequence [fresh\\_<-ns]
184 >>= \tvs-> let env` = foldr (\(k, v)->'Data.Map'.put k (Forall [] v)) env (zip2 ns tvs)
185 in unzip <$> sequence (map (infer env`) bs)
186 >>= \(ss,ts)-> unifyl ts
187 >>= \s-> liftT (tell [(n, generalize (apply s env`) t)\\t<-ts & n<-ns])
188 >>| let env`` = foldr (\(n, s, t) m->'Data.Map'.put n (generalize (apply s env`) t) m) env` (zip3 ns ss ts)
189 in infer env`` e2
190 >>= \(s2, t2)->pure (s oo s2, t2)