examples/Unify.hs

   1 -- | A very simple finite-sized-term unification engine; used by GArrowTikZ
   2 module Unify(UVar, Unifier, Unifiable(..), mergeU, emptyUnifier, getU, uvarSupply, unify, resolve)
   3 --
   4 -- | Terminology: a value of type @t@ (for which an instance
   5 -- @Unifiable t@ exists) is "fully resolved" with respect to some
   6 -- value of type @Unifier t@ if no @UVar@ which occurs in the
   7 -- @t@-value is a key in the unifier map.
   8 --
   9 where
  10 import Prelude hiding (lookup)
  11 import Data.Map hiding (map)
  12 import Data.Tree
  13 import Data.List (nub)
  14 import Control.Monad.Error
  15
  16 -- | a unification variable
  17 newtype UVar = UVar Int
  18  deriving (Ord, Eq)
  19
  20 instance Show UVar where
  21  show (UVar v) = "u" ++ show v
  22
  23 -- | A unifier is a map from unification /variables/ to unification
  24 -- /values/ of type @t@.  Invariant: values of the map are always
  25 -- fully resolved with respect to the map.
  26 data Unifier t = Unifier (Map UVar t)
  27                | UnifierError String
  28
  29 -- | Resolves a unification variable according to a Unifier.
  30 getU :: Unifier t -> UVar -> Maybe t
  31 getU (Unifier      u) v = lookup v u
  32 getU (UnifierError e) v = error e
  33
  34 -- | An infinite supply of distinct unification variables.
  35 uvarSupply :: [UVar]
  36 uvarSupply = uvarSupply' 0
  37               where
  38                uvarSupply' n = (UVar n):(uvarSupply' $ n+1)
  39
  40 -- | The empty unifier.
  41 emptyUnifier :: Unifier t
  42 emptyUnifier =  Unifier empty
  43
  44 -- | Types for which we know how to do unification.
  45 class Show t => Unifiable t where
  46
  47   -- | Turns a @UVar@ into a @t@
  48   inject      :: UVar -> t
  49
  50   -- | Discern if a @t@ is a @UVar@.  Invariant: @(project (inject x) == x)@
  51   project     :: t -> Maybe UVar
  52
  53   -- | Instances must implement this; it is called by @(unify x y)@
  54   --   only when both @(project x)@ and @(project y)@ are @Nothing@
  55   unify'      :: t -> t -> Unifier t
  56
  57   -- | Returns a list of all @UVars@ occurring in @t@
  58   occurrences :: t -> [UVar]
  59
  60   -- | @(replace vrep trep t)@ returns a copy of @t@ in which all occurrences of @vrep@ have been replaced by @trep@
  61   replace     :: UVar -> t -> t -> t
  62
  63 -- | Returns a copy of the @t@ argument in which all @UVar@
  64 -- occurrences have been replaced by fully-resolved @t@ values.
  65 resolve :: Unifiable t => Unifier t -> t -> t
  66 resolve (UnifierError e) _ = error e
  67 resolve (Unifier m) t      = resolve' (toList m) t
  68  where
  69   resolve' []            t                         = t
  70   resolve' ((uv,v):rest) t | Just uvt <- project t = if uvt == uv
  71                                                      then v        -- we got this out of the unifier, so it must be fully resolved
  72                                                      else resolve' rest t
  73                            | otherwise             = resolve' rest (replace uv v t)
  74
  75 -- | Given two unifiables, find their most general unifier.
  76 unify :: Unifiable t => t -> t -> Unifier t
  77 unify v1 v2 | (Just v1') <- project v1, (Just v2') <- project v2, v1'==v2'  = emptyUnifier
  78 unify v1 v2 | (Just v1') <- project v1                                      = if  elem v1' (occurrences v2)
  79                                                                               then UnifierError "occurs check failed in Unify.unify"
  80                                                                               else Unifier $ insert v1' v2 empty
  81 unify v1 v2 | (Just v2') <- project v2                                      = unify v2 v1
  82 unify v1 v2 |  _         <- project v1,  _         <- project v2            = unify' v1 v2
  83
  84 -- | Merge two unifiers into a single unifier.
  85 mergeU :: Unifiable t => Unifier t -> Unifier t -> Unifier t
  86 mergeU ue@(UnifierError _) _  = ue
  87 mergeU    (Unifier      u) u' = foldr (\(k,v) -> \uacc -> mergeU' uacc k (resolve uacc v)) u' (toList u)
  88  where
  89   mergeU' ue@(UnifierError _) _ _                                              = ue
  90   mergeU'  u@(Unifier m) v1 v2 | member v1 m                                   = mergeU u $ unify (m ! v1) v2
  91                                | Just v2' <- project (resolve u v2), v2' == v1 = u
  92                                | elem v1 (occurrences v2)                      = UnifierError "occurs check failed in Unify.mergeU"
  93                                | otherwise                                     = Unifier $ insert v1 v2 m
  94
  95 -- | Enumerates the unification variables, sorted by occurs-check.
  96 sortU :: (Unifiable t, Eq t) => Unifier t -> [UVar]
  97 sortU u@(Unifier um)      = reverse $ nub $ concatMap (\k -> occurrences (um!k)) (keys um)
  98 sortU   (UnifierError ue) = error ue