1 module Infer (inferTerm) where 2 3 import List(nub) 4 5 import MyList (minus) 6 import Type (TVarId, TConId, MonoType (..), PolyType (All), 7 arrow, freeTVarMono) 8 import Term (VarId, Term (Var, Abs, App, Let)) 9 import Substitution (Sub, applySub, lookupSub, makeSub) 10 import Environment (Env, lookupEnv, extendLocal, extendGlobal, 11 domEnv, freeTVarEnv) 12 import InferMonad (Infer, thenI, returnI, guardI, getSubI, 13 freshI, freshesI, unifyI, substituteI) 14 import MaybeM 15 16 specialiseI :: PolyType -> Infer MonoType 17 specialiseI (All xxs tt) = freshesI (length xxs) `thenI` (\yys -> 18 returnI (applySubs xxs yys tt)) 19 applySubs :: [TVarId] -> [MonoType] -> MonoType -> MonoType 20 applySubs xxs yys tt = applySub (makeSub (zip xxs yys)) tt 21 generaliseI :: Env -> MonoType -> Infer PolyType 22 generaliseI aa tt = getSubI `thenI` (\s -> 23 let aaVars = nub (freeTVarSubEnv s aa) in 24 let ttVars = nub (freeTVarMono tt) in 25 let xxs = ttVars `minus` aaVars in 26 returnI (All xxs tt) 27 ) 28 freeTVarSubEnv :: Sub -> Env -> [TVarId] 29 freeTVarSubEnv s aa = concat (map (freeTVarMono . lookupSub s) 30 (freeTVarEnv aa)) 31 inferTerm :: Env -> Term -> Infer MonoType 32 inferTerm aa (Var x) = 33 (x `elem` domEnv aa) `guardI` ( 34 let ss = lookupEnv aa x in 35 specialiseI ss `thenI` (\tt -> 36 substituteI tt `thenI` (\uu -> 37 returnI uu))) 38 inferTerm aa (Abs x v) = 39 freshI `thenI` (\xx -> 40 inferTerm (extendLocal aa x xx) v `thenI` (\vv -> 41 substituteI xx `thenI` (\uu -> 42 returnI (uu `arrow` vv)))) 43 inferTerm aa (App t u) = 44 inferTerm aa t `thenI` (\tt -> 45 inferTerm aa u `thenI` (\uu -> 46 freshI `thenI` (\xx -> 47 unifyI tt (uu `arrow` xx) `thenI` (\() -> 48 substituteI xx `thenI` (\vv -> 49 returnI vv))))) 50 inferTerm aa (Let x u v) = 51 inferTerm aa u `thenI` (\uu -> 52 generaliseI aa uu `thenI` (\ss -> 53 inferTerm (extendGlobal aa x ss) v `thenI` (\vv -> 54 returnI vv)))