1 -- | A very simple finite-sized-term unification engine; used by GArrowTikZ
2 module Unify(UVar, Unifier, Unifiable(..), mergeU, emptyUnifier, getU, uvarSupply, unify, resolve)
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.
10 import Prelude hiding (lookup)
11 import Data.Map hiding (map)
13 import Data.List (nub)
14 import Control.Monad.Error
16 -- | a unification variable
17 newtype UVar = UVar Int
20 instance Show UVar where
21 show (UVar v) = "u" ++ show v
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)
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
34 -- | An infinite supply of distinct unification variables.
36 uvarSupply = uvarSupply' 0
38 uvarSupply' n = (UVar n):(uvarSupply' $ n+1)
40 -- | The empty unifier.
41 emptyUnifier :: Unifier t
42 emptyUnifier = Unifier empty
44 -- | Types for which we know how to do unification.
45 class Show t => Unifiable t where
47 -- | Turns a @UVar@ into a @t@
50 -- | Discern if a @t@ is a @UVar@. Invariant: @(project (inject x) == x)@
51 project :: t -> Maybe UVar
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
57 -- | Returns a list of all @UVars@ occurring in @t@
58 occurrences :: t -> [UVar]
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
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
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
73 | otherwise = resolve' rest (replace uv v t)
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
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)
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
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