1 -- | A very simple unification engine; used by GArrowTikZ
2 module Unify(UVar, Unifier, Unifiable(..), mergeU, emptyUnifier, getU, uvarSupply, unify, resolve, occurs)
4 import Prelude hiding (lookup)
5 import Data.Map hiding (map)
8 import Control.Monad.Error
10 -- TO DO: propagate occurs-check errors through the Unifier instead of using Prelude.error
12 -- | a unification variable
13 newtype UVar = UVar Int
16 instance Show UVar where
17 show (UVar v) = "u" ++ show v
19 -- | A unifier is a map from unification /variables/ to unification /values/ of type @t@.
20 data Unifier t = Unifier (Map UVar t)
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
26 -- | An infinite supply of distinct unification variables.
28 uvarSupply = uvarSupply' 0
30 uvarSupply' n = (UVar n):(uvarSupply' $ n+1)
32 -- | The empty unifier.
33 emptyUnifier :: Unifier t
34 emptyUnifier = Unifier empty
36 -- | Types for which we know how to do unification.
37 class Unifiable t where
39 -- | Turns a @UVar@ into a @t@
42 -- | Discern if a @t@ is a @UVar@. Invariant: @(project (inject x) == x)@
43 project :: t -> Maybe UVar
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
49 -- | Returns a list of all @UVars@ occurring in @t@; duplicates are okay and resolution should not be performed.
50 occurrences :: t -> [UVar]
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)
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)
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
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)
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
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)