toString (Let ns r) = concat
[ "let\n"
, concat [concat ["\t", toString n, " = ", toString v, "\n"]\\(n, v)<-ns]
- , " in\n", toString r]
+ , "in\n", toString r]
toString _ = abort "toString Expression not implemented"
instance toString Value where
preamble = fromList
[(['_if'], Forall [['_ift']]
$ TBool --> TVar ['_ift'] --> TVar ['_ift'] --> TVar ['_ift'])
- ,(['_eq'], Forall [['_eq']] $ TInt --> TInt --> TBool)
+ ,(['_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
+:: Subst :== Map [Char] Type
:: Infer a :== StateT [Int] (Either [String]) a
runInfer :: (Infer (Subst, Type)) -> Either [String] Scheme
fresh :: Infer Type
fresh = getState >>= \[s:ss]->put ss >>| pure (TVar (['v':[c\\c<-:toString s]]))
-(oo) infixr 9 :: Subst Subst -> Subst
+(oo) infixl 9 :: Subst Subst -> Subst
(oo) s1 s2 = 'Data.Map'.union (apply s1 <$> s2) s1
class Substitutable a where
= fresh
>>= \tv-> infer ('Data.Map'.put x (Forall [] tv) env) b
>>= \(s1, t1)->pure (s1, apply s1 tv --> t1)
-//infer env (Let x e1 e2)
+//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)->pure (s1 oo s2, t2)
infer env (Let [(x, e1)] e2)
= fresh
- >>= \tv-> infer ('Data.Map'.put x (Forall [] tv) env) e1
- >>= \(s1, t1)->infer ('Data.Map'.put x (generalize (apply s1 env) t1) env) e2
+ >>= \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)