add "sanity" target to Makefile
[coq-hetmet.git] / 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