examples/Unify.hs

   1 -- | A very simple unification engine; used by GArrowTikZ
   2 module Unify(UVar, Unifier, Unifiable(..), mergeU, emptyUnifier, getU, uvarSupply, unify, resolve, occurs)
   3 where
   4 import Prelude hiding (lookup)
   5 import Data.Map hiding (map)
   6 import Data.Tree
   7 import Data.List (nub)
   8 import Control.Monad.Error
   9
  10 -- TO DO: propagate occurs-check errors through the Unifier instead of using Prelude.error
  11
  12 -- | a unification variable
  13 newtype UVar = UVar Int
  14  deriving (Ord, Eq)
  15
  16 instance Show UVar where
  17  show (UVar v) = "u" ++ show v
  18
  19 -- | A unifier is a map from unification /variables/ to unification /values/ of type @t@.
  20 data Unifier t = Unifier (Map UVar t)
  21
  22 -- | Resolves a unification variable according to a Unifier (not recursively).
  23 getU :: Unifier t -> UVar -> Maybe t
  24 getU (Unifier u) v = lookup v u
  25
  26 -- | An infinite supply of distinct unification variables.
  27 uvarSupply :: [UVar]
  28 uvarSupply = uvarSupply' 0
  29               where
  30                uvarSupply' n = (UVar n):(uvarSupply' $ n+1)
  31
  32 -- | The empty unifier.
  33 emptyUnifier :: Unifier t
  34 emptyUnifier =  Unifier empty
  35
  36 -- | Types for which we know how to do unification.
  37 class Unifiable t where
  38
  39   -- | Turns a @UVar@ into a @t@
  40   inject      :: UVar -> t
  41
  42   -- | Discern if a @t@ is a @UVar@.  Invariant: @(project (inject x) == x)@
  43   project     :: t -> Maybe UVar
  44
  45   -- | Instances must implement this; it is called by @(unify x y)@
  46   --   only when both @(project x)@ and @(project y)@ are @Nothing@
  47   unify'  :: t -> t -> Unifier t
  48
  49   -- | Returns a list of all @UVars@ occurring in @t@; duplicates are okay and resolution should not be performed.
  50   occurrences :: t -> [UVar]
  51
  52 -- | Returns a list of all UVars occurring anywhere in t and any UVars which
  53 --   occur in values unified therewith.
  54 resolve :: Unifiable t => Unifier t -> UVar -> [UVar]
  55 resolve (Unifier u) v | member v u = v:(concatMap (resolve (Unifier u)) $ occurrences $ u ! v)
  56                       | otherwise  = [v]
  57
  58 -- | The occurs check.
  59 occurs :: Unifiable t => Unifier t -> UVar -> t -> Bool
  60 occurs u v x = elem v $ concatMap (resolve u) (occurrences x)
  61
  62 -- | Given two unifiables, find their most general unifier.
  63 unify :: Unifiable t => t -> t -> Unifier t
  64 unify v1 v2 | (Just v1') <- project v1, (Just v2') <- project v2, v1'==v2'                   = emptyUnifier
  65 unify v1 v2 | (Just v1') <- project v1 = if  occurs emptyUnifier v1' v2
  66                                          then error "occurs check failed"
  67                                          else Unifier $ insert v1' v2 empty
  68 unify v1 v2 | (Just v2') <- project v2 = unify v2 v1
  69 unify v1 v2 |  _         <- project v1,  _         <- project v2                             = unify' v1 v2
  70
  71 -- | Merge two unifiers into a single unifier.
  72 mergeU :: Unifiable t => Unifier t -> Unifier t -> Unifier t
  73 mergeU (Unifier u) u' = foldr (\(k,v) -> \uacc -> mergeU' uacc k v) u' (toList u)
  74  where
  75   mergeU' u@(Unifier m) v1 v2 | member v1 m    = mergeU u $ unify (m ! v1) v2
  76                               | occurs u v1 v2 = error "occurs check failed"
  77                               | otherwise      = Unifier $ insert v1 v2 m
  78
  79 -- | Enumerates the unification variables, sorted by occurs-check.
  80 sortU :: (Unifiable t, Eq t) => Unifier t -> [UVar]
  81 sortU u@(Unifier um) = reverse $ nub $ concatMap (resolve u) (keys um)
  82
  83