1 module Substitution   (Sub, applySub, lookupSub, emptySub, extendSub,
    2                        makeSub, thenSub, domSub, unifySub)
    3                       where
    4 
    5 import Type           (TVarId, TConId, MonoType (TVar, TCon), freeTVarMono)
    6 import FiniteMap      (FM, emptyFM, lookupElseFM, makeFM, extendFM,
    7                        thenFM, mapFM, domFM, ranFM)
    8 import MaybeM         (Maybe, thenM, returnM, failM, guardM)
    9 data  Sub  =  MkSub (FM TVarId MonoType)
   10 rep                           ::  Sub -> FM TVarId MonoType
   11 rep (MkSub f)                 =   f
   12 applySub                      ::  Sub -> MonoType -> MonoType
   13 applySub s (TVar x)           =   lookupSub s x
   14 applySub s (TCon k ts)        =   TCon k (map (applySub s) ts)
   15 lookupSub                     ::  Sub -> TVarId -> MonoType
   16 lookupSub s x                 =   lookupElseFM (TVar x) (rep s) x
   17 unitSub                       ::  TVarId -> MonoType -> Sub
   18 unitSub x t                   =   MkSub (makeFM [(x,t)])
   19 emptySub                      ::  Sub
   20 emptySub                      =   MkSub emptyFM
   21 makeSub                       ::  [(TVarId, MonoType)] -> Sub
   22 makeSub xts                   =   MkSub (makeFM xts)
   23 extendSub                     ::  Sub -> TVarId -> MonoType -> Sub
   24 extendSub s x t               =   s `thenSub` unitSub x (applySub s t)
   25 thenSub                       ::  Sub -> Sub -> Sub
   26 r `thenSub` s                 =   MkSub (mapFM (applySub s) (rep r) `thenFM` rep s)
   27 domSub                        ::  Sub -> [TVarId]
   28 domSub s                      =   domFM (rep s)
   29 unifySub                              =  unify
   30 unify                                 :: MonoType -> MonoType -> Sub -> Maybe Sub
   31 unify (TVar x) u s                    =  unifyTVar x u s
   32 unify t (TVar y) s                    =  unifyTVar y t s
   33 unify (TCon j ts) (TCon k us) s       =  (j == k) `guardM` unifies ts us s
   34 unifies                               :: [MonoType] -> [MonoType] -> Sub -> Maybe Sub
   35 unifies [] [] s                       =  returnM s
   36 unifies (t:ts) (u:us) s               =  unify t u s `thenM` (\s' -> unifies ts us s')
   37 unifyTVar                             :: TVarId -> MonoType -> Sub -> Maybe Sub
   38 unifyTVar x t s | x `elem` domSub s     =  unify (lookupSub s x) t s
   39                 | TVar x == t         =  returnM s
   40                 | x `elem` freeVars t   =  failM
   41                 | otherwise           =  returnM (extendSub s x t)    
   42 freeVars                              =  freeTVarMono