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)))