NaturalDeductionContext: more permutation proofs

[coq-hetmet.git] / examples / Unify.hs

diff --git a/examples/Unify.hs b/examples/Unify.hs
index 41dcad8..34761ea 100644 (file)
--- a/examples/Unify.hs
+++ b/examples/Unify.hs
@@ -13,8 +13,6 @@ import Data.Tree
 import Data.List (nub)
 import Control.Monad.Error
 
--- TO DO: propagate occurs-check errors through the Unifier instead of using Prelude.error
-
 -- | a unification variable
 newtype UVar = UVar Int
  deriving (Ord, Eq)
@@ -26,10 +24,12 @@ instance Show UVar where
 -- /values/ of type @t@.  Invariant: values of the map are always
 -- fully resolved with respect to the map.
 data Unifier t = Unifier (Map UVar t)
+               | UnifierError String
 
 -- | Resolves a unification variable according to a Unifier.
 getU :: Unifier t -> UVar -> Maybe t
-getU (Unifier u) v = lookup v u
+getU (Unifier      u) v = lookup v u
+getU (UnifierError e) v = error e
 
 -- | An infinite supply of distinct unification variables.
 uvarSupply :: [UVar]
@@ -63,7 +63,8 @@ class Show t => Unifiable t where
 -- | Returns a copy of the @t@ argument in which all @UVar@
 -- occurrences have been replaced by fully-resolved @t@ values.
 resolve :: Unifiable t => Unifier t -> t -> t
-resolve (Unifier m) t = resolve' (toList m) t
+resolve (UnifierError e) _ = error e
+resolve (Unifier m) t      = resolve' (toList m) t
  where
   resolve' []            t                         = t
   resolve' ((uv,v):rest) t | Just uvt <- project t = if uvt == uv
@@ -73,22 +74,25 @@ resolve (Unifier m) t = resolve' (toList m) t
 
 -- | Given two unifiables, find their most general unifier.
 unify :: Unifiable t => t -> t -> Unifier t
-unify v1 v2 | (Just v1') <- project v1, (Just v2') <- project v2, v1'==v2'    = emptyUnifier
-unify v1 v2 | (Just v1') <- project v1                                        = if  elem v1' (occurrences v2)
-                                                                                then error "occurs check failed in Unify.unify"
-                                                                                else Unifier $ insert v1' v2 empty
-unify v1 v2 | (Just v2') <- project v2                                        = unify v2 v1
-unify v1 v2 |  _         <- project v1,  _         <- project v2              = unify' v1 v2
+unify v1 v2 | (Just v1') <- project v1, (Just v2') <- project v2, v1'==v2'  = emptyUnifier
+unify v1 v2 | (Just v1') <- project v1                                      = if  elem v1' (occurrences v2)
+                                                                              then UnifierError "occurs check failed in Unify.unify"
+                                                                              else Unifier $ insert v1' v2 empty
+unify v1 v2 | (Just v2') <- project v2                                      = unify v2 v1
+unify v1 v2 |  _         <- project v1,  _         <- project v2            = unify' v1 v2
 
 -- | Merge two unifiers into a single unifier.
 mergeU :: Unifiable t => Unifier t -> Unifier t -> Unifier t
-mergeU (Unifier u) u' = foldr (\(k,v) -> \uacc -> mergeU' uacc k (resolve uacc v)) u' (toList u)
+mergeU ue@(UnifierError _) _  = ue
+mergeU    (Unifier      u) u' = foldr (\(k,v) -> \uacc -> mergeU' uacc k (resolve uacc v)) u' (toList u)
  where
-  mergeU' u@(Unifier m) v1 v2 | member v1 m                                   = mergeU u $ unify (m ! v1) v2
-                              | Just v2' <- project (resolve u v2), v2' == v1 = u
-                              | elem v1 (occurrences v2)                      = error "occurs check failed in Unify.mergeU"
-                              | otherwise                                     = Unifier $ insert v1 v2 m
+  mergeU' ue@(UnifierError _) _ _                                              = ue
+  mergeU'  u@(Unifier m) v1 v2 | member v1 m                                   = mergeU u $ unify (m ! v1) v2
+                               | Just v2' <- project (resolve u v2), v2' == v1 = u
+                               | elem v1 (occurrences v2)                      = UnifierError "occurs check failed in Unify.mergeU"
+                               | otherwise                                     = Unifier $ insert v1 v2 m
                                                            
 -- | Enumerates the unification variables, sorted by occurs-check.
 sortU :: (Unifiable t, Eq t) => Unifier t -> [UVar]
-sortU u@(Unifier um) = reverse $ nub $ concatMap (\k -> occurrences (um!k)) (keys um)
+sortU u@(Unifier um)      = reverse $ nub $ concatMap (\k -> occurrences (um!k)) (keys um)
+sortU   (UnifierError ue) = error ue