atp-haskell 1.8 → 1.9

raw patch · 6 files changed

+71/−67 lines, 6 filesPVP ok

version bump matches the API change (PVP)

API changes (from Hackage documentation)

Files

• atp-haskell.cabal +1/−1
• src/Data/Logic/ATP/Meson.hs +10/−10
• src/Data/Logic/ATP/Pretty.hs +5/−2
• src/Data/Logic/ATP/Resolution.hs +17/−17
• src/Data/Logic/ATP/Tableaux.hs +15/−12
• src/Data/Logic/ATP/Unif.hs +23/−25

@@ -1,5 +1,5 @@ Name:             atp-haskell-Version:          1.8+Version:          1.9 Synopsis:         Translation from Ocaml to Haskell of John Harrison's ATP code Description:      This package is a liberal translation from OCaml to Haskell of                   the automated theorem prover written in OCaml in

@@ -33,7 +33,7 @@ import Data.Logic.ATP.Skolem (askolemize, Formula, HasSkolem(SVarOf), pnf, runSkolem, SkolemT, simpdnf', specialize, toSkolem) import Data.Logic.ATP.Tableaux (K(K), tab) import Data.Logic.ATP.Term (fApp, IsTerm(FunOf, TVarOf), vt)-import Data.Logic.ATP.Unif (Unify, unify_literals)+import Data.Logic.ATP.Unif (Unify(UTermOf), unify_literals) import Data.Map.Strict as Map import Data.Set as Set import Test.HUnit@@ -176,7 +176,7 @@ -- -------------------------------------------------------------------------  mexpand1 :: (JustLiteral lit, Ord lit,-             HasApply atom, IsTerm term, Unify atom atom,+             HasApply atom, IsTerm term, Unify (atom, atom), term ~ UTermOf (atom, atom),              atom ~ AtomOf lit, term ~ TermOf atom, v ~ TVarOf term) =>            Set (PrologRule lit)         -> Set lit@@ -206,7 +206,7 @@ -- -------------------------------------------------------------------------  puremeson1 :: forall fof atom term v function.-              (IsFirstOrder fof, Unify atom atom, Ord fof,+              (IsFirstOrder fof, Unify (atom, atom), term ~ UTermOf (atom, atom), Ord fof,                atom ~ AtomOf fof, term ~ TermOf atom, function ~ FunOf term,                v ~ VarOf fof, v ~ TVarOf term) =>               Maybe Depth -> fof -> Failing Depth@@ -219,7 +219,7 @@       (cls :: Set (Set (LFormula atom))) = simpcnf id (specialize id (pnf fm) :: PFormula atom)  meson1 :: forall m fof atom predicate term function v.-          (IsFirstOrder fof, Unify atom atom, Ord fof, HasSkolem function, Monad m,+          (IsFirstOrder fof, Unify (atom, atom), term ~ UTermOf (atom, atom), Ord fof, HasSkolem function, Monad m,            atom ~ AtomOf fof, term ~ TermOf atom, predicate ~ PredOf atom, function ~ FunOf term, v ~ VarOf fof, v ~ SVarOf function) =>           Maybe Depth -> fof -> SkolemT m function (Set (Failing Depth)) meson1 maxdl fm =@@ -230,7 +230,7 @@ -- With repetition checking and divide-and-conquer search. -- ------------------------------------------------------------------------- -equal :: (JustLiteral lit, HasApply atom, Unify atom atom, IsTerm term,+equal :: (JustLiteral lit, HasApply atom, Unify (atom, atom), term ~ UTermOf (atom, atom), IsTerm term,           atom ~ AtomOf lit, term ~ TermOf atom, v ~ TVarOf term) =>          Map v term -> lit -> lit -> Bool equal env fm1 fm2 =@@ -257,7 +257,7 @@                                    (e1,n2+r1,k1))                  (env,n1,k) -mexpand2 :: (JustLiteral lit, Ord lit, HasApply atom, IsTerm term, Unify atom atom,+mexpand2 :: (JustLiteral lit, Ord lit, HasApply atom, IsTerm term, Unify (atom, atom), term ~ UTermOf (atom, atom),              atom ~ AtomOf lit, term ~ TermOf atom, v ~ TVarOf term) =>            Set (PrologRule lit)         -> Set lit@@ -284,7 +284,7 @@             mexpand2' = mexpands rules (Set.insert g ancestors) asm cont             (Prolog asm c, k') = renamerule k rule -mexpands :: (JustLiteral lit, Ord lit, HasApply atom, Unify atom atom, IsTerm term,+mexpands :: (JustLiteral lit, Ord lit, HasApply atom, Unify (atom, atom), term ~ UTermOf (atom, atom), IsTerm term,              atom ~ AtomOf lit, term ~ TermOf atom, v ~ TVarOf term) =>             Set (PrologRule lit)          -> Set lit@@ -317,7 +317,7 @@ puremeson2 :: forall fof atom term v.              (atom ~ AtomOf fof, term ~ TermOf atom, v ~ VarOf fof, v ~ TVarOf term,               IsFirstOrder fof,-              Unify atom atom, Ord fof+              Unify (atom, atom), term ~ UTermOf (atom, atom), Ord fof              ) => Maybe Depth -> fof -> Failing Depth puremeson2 maxdl fm =     snd <$> deepen f (Depth 0) maxdl@@ -328,7 +328,7 @@       (cls :: Set (Set (LFormula atom))) = simpcnf id (specialize id (pnf fm) :: PFormula atom)  meson2 :: forall m fof atom term function v.-          (IsFirstOrder fof, Unify atom atom, Ord fof,+          (IsFirstOrder fof, Unify (atom, atom), term ~ UTermOf (atom, atom), Ord fof,            HasSkolem function, Monad m,            atom ~ AtomOf fof, term ~ TermOf atom, function ~ FunOf term, v ~ VarOf fof, v ~ SVarOf function) =>           Maybe Depth -> fof -> SkolemT m function (Set (Failing Depth))@@ -336,7 +336,7 @@     askolemize ((.~.)(generalize fm)) >>=     return . Set.map (puremeson2 maxdl . list_conj) . (simpdnf' :: fof -> Set (Set fof)) -meson :: (IsFirstOrder fof, Unify atom atom, HasSkolem function, Monad m, Ord fof,+meson :: (IsFirstOrder fof, Unify (atom, atom), term ~ UTermOf (atom, atom), HasSkolem function, Monad m, Ord fof,           atom ~ AtomOf fof, term ~ TermOf atom, function ~ FunOf term, v ~ VarOf fof, v ~ SVarOf function) =>          Maybe Depth -> fof -> SkolemT m function (Set (Failing Depth)) meson = meson2

@@ -9,7 +9,6 @@ {-# LANGUAGE TemplateHaskell #-} {-# LANGUAGE TypeSynonymInstances #-} {-# OPTIONS_GHC -fno-warn-orphans #-}-{-# OPTIONS_GHC -ddump-splices #-}  module Data.Logic.ATP.Pretty     ( (<>)@@ -105,7 +104,11 @@     pPrint = pPrint . Map.toList  -- | Version of assertEqual that uses the pretty printer instead of show.-assertEqual' :: (?loc :: CallStack, Eq a, Pretty a) =>+assertEqual' :: (+#ifndef ghcjs_HOST_OS+                 ?loc :: CallStack,+#endif+                 Eq a, Pretty a) =>                 String -- ^ The message prefix              -> a      -- ^ The expected value              -> a      -- ^ The actual value

@@ -40,7 +40,7 @@ import Data.Logic.ATP.Skolem (askolemize, Formula, Function(Skolem), HasSkolem(SVarOf), pnf,                               runSkolem, simpdnf', SkAtom, skolemize, SkolemT, specialize, SkTerm) import Data.Logic.ATP.Term (fApp, foldTerm, IsTerm(FunOf, TVarOf), prefix, V, vt)-import Data.Logic.ATP.Unif (solve, Unify, unify_literals)+import Data.Logic.ATP.Unif (solve, Unify(UTermOf), unify_literals) import Data.Map.Strict as Map import Data.Maybe (fromMaybe) import Data.Set as Set@@ -68,7 +68,7 @@  -- | MGU of a set of literals. mgu :: forall lit atom term v.-       (JustLiteral lit, HasApply atom, Unify atom atom, IsTerm term,+       (JustLiteral lit, HasApply atom, Unify (atom, atom), term ~ UTermOf (atom, atom), IsTerm term,         atom ~ AtomOf lit, term ~ TermOf atom, v ~ TVarOf term) =>        Set lit -> StateT (Map v term) Failing (Map v term) mgu l =@@ -79,7 +79,7 @@             _ -> solve <$> get       _ -> solve <$> get -unifiable :: (JustLiteral lit, IsTerm term, HasApply atom, Unify atom atom,+unifiable :: (JustLiteral lit, IsTerm term, HasApply atom, Unify (atom, atom), term ~ UTermOf (atom, atom),               atom ~ AtomOf lit, term ~ TermOf atom, v ~ TVarOf term) =>              lit -> lit -> Bool unifiable p q = failing (const False) (const True) (execStateT (unify_literals p q) Map.empty)@@ -100,7 +100,7 @@ -- General resolution rule, incorporating factoring as in Robinson's paper. -- ------------------------------------------------------------------------- -resolvents :: (JustLiteral lit, Ord lit, HasApply atom, Unify atom atom, IsTerm term,+resolvents :: (JustLiteral lit, Ord lit, HasApply atom, Unify (atom, atom), term ~ UTermOf (atom, atom), IsTerm term,                atom ~ AtomOf lit, term ~ TermOf atom, v ~ TVarOf term) =>               Set lit -> Set lit -> lit -> Set lit -> Set lit resolvents cl1 cl2 p acc =@@ -117,7 +117,7 @@       -- ps2 :: Set fof       ps2 = Set.filter (unifiable ((.~.) p)) cl2 -resolve_clauses :: (JustLiteral lit, Ord lit, HasApply atom, Unify atom atom, IsTerm term,+resolve_clauses :: (JustLiteral lit, Ord lit, HasApply atom, Unify (atom, atom), term ~ UTermOf (atom, atom), IsTerm term,                     atom ~ AtomOf lit, term ~ TermOf atom, v ~ TVarOf term) =>                    Set lit -> Set lit -> Set lit resolve_clauses cls1 cls2 =@@ -129,7 +129,7 @@ -- Basic "Argonne" loop. -- ------------------------------------------------------------------------- -resloop1 :: (JustLiteral lit, Ord lit, HasApply atom, IsTerm term, Unify atom atom,+resloop1 :: (JustLiteral lit, Ord lit, HasApply atom, IsTerm term, Unify (atom, atom), term ~ UTermOf (atom, atom),              atom ~ AtomOf lit, term ~ TermOf atom, v ~ TVarOf term) =>             Set (Set lit) -> Set (Set lit) -> Failing Bool resloop1 used unused =@@ -145,13 +145,13 @@ pure_resolution1 :: forall fof atom term v.                     (atom ~ AtomOf fof, term ~ TermOf atom, v ~ TVarOf term,                      IsFirstOrder fof,-                     Unify atom atom,+                     Unify (atom, atom), term ~ UTermOf (atom, atom),                      Ord fof, Pretty fof                     ) => fof -> Failing Bool pure_resolution1 fm = resloop1 Set.empty (simpcnf id (specialize id (pnf fm) :: PFormula atom) :: Set (Set (LFormula atom)))  resolution1 :: forall m fof atom term v function.-               (IsFirstOrder fof, Unify atom atom, Ord fof, HasSkolem function, Monad m,+               (IsFirstOrder fof, Unify (atom, atom), term ~ UTermOf (atom, atom), Ord fof, HasSkolem function, Monad m,                 atom ~ AtomOf fof, term ~ TermOf atom, function ~ FunOf term, v ~ TVarOf term, v ~ SVarOf function) =>                fof -> SkolemT m function (Set (Failing Bool)) resolution1 fm = askolemize ((.~.)(generalize fm)) >>= return . Set.map (pure_resolution1 . list_conj) . (simpdnf' :: fof -> Set (Set fof))@@ -220,7 +220,7 @@  -- | With deletion of tautologies and bi-subsumption with "unused". resolution2 :: forall fof atom term v function m.-               (IsFirstOrder fof, Unify atom atom, Match (atom, atom) v term, HasSkolem function, Monad m, Ord fof,+               (IsFirstOrder fof, Unify (atom, atom), term ~ UTermOf (atom, atom), Match (atom, atom) v term, HasSkolem function, Monad m, Ord fof,                 atom ~ AtomOf fof, term ~ TermOf atom, function ~ FunOf term, v ~ TVarOf term, v ~ SVarOf function) =>                fof -> SkolemT m function (Set (Failing Bool)) resolution2 fm = askolemize ((.~.) (generalize fm)) >>= return . Set.map (pure_resolution2 . list_conj) . (simpdnf' :: fof -> Set (Set fof))@@ -228,13 +228,13 @@ pure_resolution2 :: forall fof atom term v.                     (IsFirstOrder fof, Ord fof, Pretty fof,                      HasApply atom, IsTerm term,-                     Unify atom atom, Match (atom, atom) v term,+                     Unify (atom, atom), term ~ UTermOf (atom, atom), Match (atom, atom) v term,                      atom ~ AtomOf fof, term ~ TermOf atom, v ~ TVarOf term) =>                     fof -> Failing Bool pure_resolution2 fm = resloop2 Set.empty (simpcnf id (specialize id (pnf fm) :: PFormula atom) :: Set (Set (LFormula atom)))  resloop2 :: (JustLiteral lit, Ord lit, HasApply atom, IsTerm term,-             Unify atom atom, Match (atom, atom) v term,+             Unify (atom, atom), term ~ UTermOf (atom, atom), Match (atom, atom) v term,              atom ~ AtomOf lit, term ~ TermOf atom, v ~ TVarOf term) =>             Set (Set lit) -> Set (Set lit) -> Failing Bool resloop2 used unused =@@ -295,20 +295,20 @@  -- | Positive (P1) resolution. presolution :: forall fof atom term v function m.-               (IsFirstOrder fof, Unify atom atom, Match (atom, atom) v term, HasSkolem function, Monad m, Ord fof, Pretty fof,+               (IsFirstOrder fof, Unify (atom, atom), term ~ UTermOf (atom, atom), Match (atom, atom) v term, HasSkolem function, Monad m, Ord fof, Pretty fof,                 atom ~ AtomOf fof, term ~ TermOf atom, function ~ FunOf term, v ~ VarOf fof, v ~ SVarOf function) =>                fof -> SkolemT m function (Set (Failing Bool)) presolution fm =     askolemize ((.~.) (generalize fm)) >>= return . Set.map (pure_presolution . list_conj) . (simpdnf' :: fof -> Set (Set fof))  pure_presolution :: forall fof atom term v.-                    (IsFirstOrder fof, Unify atom atom, Match (atom, atom) v term, Ord fof, Pretty fof,+                    (IsFirstOrder fof, Unify (atom, atom), term ~ UTermOf (atom, atom), Match (atom, atom) v term, Ord fof, Pretty fof,                      atom ~ AtomOf fof, term ~ TermOf atom, v ~ VarOf fof, v ~ TVarOf term) =>                     fof -> Failing Bool pure_presolution fm = presloop Set.empty (simpcnf id (specialize id (pnf fm :: fof) ::  PFormula atom) :: Set (Set (LFormula atom)))  presloop :: (JustLiteral lit, Ord lit, HasApply atom, IsTerm term,-             Match (atom, atom) v term, Unify atom atom,+             Match (atom, atom) v term, Unify (atom, atom), term ~ UTermOf (atom, atom),              atom ~ AtomOf lit, term ~ TermOf atom, v ~ TVarOf term) =>             Set (Set lit) -> Set (Set lit) -> Failing Bool presloop used unused =@@ -323,7 +323,7 @@           then Success True           else presloop used' (Set.fold (incorporate cl) ros news) -presolve_clauses :: (JustLiteral lit, Ord lit, HasApply atom, IsTerm term, Unify atom atom,+presolve_clauses :: (JustLiteral lit, Ord lit, HasApply atom, IsTerm term, Unify (atom, atom), term ~ UTermOf (atom, atom),                      atom ~ AtomOf lit, term ~ TermOf atom, v ~ TVarOf term) =>                     Set lit -> Set lit -> Set lit presolve_clauses cls1 cls2 =@@ -333,7 +333,7 @@  -- | Introduce a set-of-support restriction. resolution3 :: forall fof atom term v function m.-               (IsFirstOrder fof, Unify atom atom, Match (atom, atom) v term, HasSkolem function, Monad m, Ord fof,+               (IsFirstOrder fof, Unify (atom, atom), term ~ UTermOf (atom, atom), Match (atom, atom) v term, HasSkolem function, Monad m, Ord fof,                 atom ~ AtomOf fof, term ~ TermOf atom, function ~ FunOf term, v ~ VarOf fof, v ~ SVarOf function) =>                fof -> SkolemT m function (Set (Failing Bool)) resolution3 fm =@@ -342,7 +342,7 @@ pure_resolution3 :: forall fof atom term v.                     (atom ~ AtomOf fof, term ~ TermOf atom, v ~ VarOf fof, v ~ TVarOf term,                      IsFirstOrder fof,-                     Unify atom atom,+                     Unify (atom, atom), term ~ UTermOf (atom, atom),                      Match (atom, atom) v term,                      Ord fof, Pretty fof) => fof -> Failing Bool pure_resolution3 fm =

@@ -37,7 +37,7 @@ import Data.Logic.ATP.Quantified (exists, foldQuantified, for_all, Quant((:!:))) import Data.Logic.ATP.Skolem (askolemize, Formula, HasSkolem(SVarOf, toSkolem), runSkolem, simpdnf', skolemize, SkTerm) import Data.Logic.ATP.Term (fApp, IsTerm(TVarOf, FunOf), vt)-import Data.Logic.ATP.Unif (Unify, unify_literals)+import Data.Logic.ATP.Unif (Unify(UTermOf), unify_literals) import Data.Map.Strict as Map import Data.Set as Set import Data.String (IsString(..))@@ -45,14 +45,17 @@ import Test.HUnit hiding (State)  -- | Unify complementary literals.-unify_complements :: (IsLiteral lit1, JustLiteral lit2, HasApply atom1, HasApply atom2, Unify atom1 atom2,-                      atom1 ~ AtomOf lit1, atom2 ~ AtomOf lit2, term ~ TermOf atom1, term ~ TermOf atom2, v ~ TVarOf term) =>+unify_complements :: (IsLiteral lit1, JustLiteral lit2, HasApply atom1, HasApply atom2,+                      Unify (atom1, atom2), term ~ UTermOf (atom1, atom2), v ~ TVarOf term,+                      atom1 ~ AtomOf lit1, term ~ TermOf atom1,+                      atom2 ~ AtomOf lit2, term ~ TermOf atom2) =>                      lit1 -> lit2 -> StateT (Map v term) Failing () unify_complements p q = unify_literals p ((.~.) q)  -- | Unify and refute a set of disjuncts.-unify_refute :: (JustLiteral lit, Ord lit, HasApply atom, Unify atom atom, IsTerm term,-                 atom ~ AtomOf lit, term ~ TermOf atom, v ~ TVarOf term) =>+unify_refute :: (JustLiteral lit, Ord lit, HasApply atom, IsTerm term,+                 Unify (atom, atom), term ~ UTermOf (atom, atom), v ~ TVarOf term,+                 atom ~ AtomOf lit, term ~ TermOf atom) =>                 Set (Set lit) -> Map v term -> Failing (Map v term) unify_refute djs env =     case Set.minView djs of@@ -65,7 +68,7 @@  -- | Hence a Prawitz-like procedure (using unification on DNF). prawitz_loop :: forall lit atom v term.-                (JustLiteral lit, Ord lit, HasApply atom, Unify atom atom,+                (JustLiteral lit, Ord lit, HasApply atom, Unify (atom, atom), term ~ UTermOf (atom, atom),                  atom ~ AtomOf lit, term ~ TermOf atom, v ~ TVarOf term) =>                 Set (Set lit) -> [v] -> Set (Set lit) -> Int -> (Map v term, Int) prawitz_loop djs0 fvs djs n =@@ -78,7 +81,7 @@       newvar k = vt (fromString ("_" ++ show (n * length fvs + k)))  prawitz :: forall formula atom term function v.-           (IsFirstOrder formula, Ord formula, Unify atom atom, HasSkolem function, Show formula,+           (IsFirstOrder formula, Ord formula, Unify (atom, atom), term ~ UTermOf (atom, atom), HasSkolem function, Show formula,             atom ~ AtomOf formula, term ~ TermOf atom, function ~ FunOf term,             v ~ TVarOf term, v ~ SVarOf function) =>            formula -> Int@@ -107,7 +110,7 @@ -- Comparison of number of ground instances. -- ------------------------------------------------------------------------- -compare :: (IsFirstOrder formula, Ord formula, Unify atom atom, HasSkolem function, Show formula,+compare :: (IsFirstOrder formula, Ord formula, Unify (atom, atom), term ~ UTermOf (atom, atom), HasSkolem function, Show formula,             atom ~ AtomOf formula, term ~ TermOf atom, function ~ FunOf term,             v ~ TVarOf term, v ~ SVarOf function) =>            formula -> (Int, Int)@@ -175,7 +178,7 @@  -- | More standard tableau procedure, effectively doing DNF incrementally.  (p. 177) tableau :: forall formula atom term v function.-           (IsFirstOrder formula, Unify atom atom,+           (IsFirstOrder formula, Unify (atom, atom), term ~ UTermOf (atom, atom),             atom ~ AtomOf formula, term ~ TermOf atom, function ~ FunOf term, v ~ TVarOf term) =>            [formula] -> Depth -> RWS () () () (Failing (K, Map v term)) tableau fms n0 =@@ -211,14 +214,14 @@             tryLit :: JL formula -> JL formula -> RWS () () () (Failing (K, Map v term))             tryLit fm' l = failing (return . Failure) (\env' -> cont (k, env')) (execStateT (unify_complements fm' l) env) -tabrefute :: (IsFirstOrder formula, Unify atom atom,+tabrefute :: (IsFirstOrder formula, Unify (atom, atom), term ~ UTermOf (atom, atom),               atom ~ AtomOf formula, term ~ TermOf atom, v ~ TVarOf term) =>              Maybe Depth -> [formula] -> Failing ((K, Map v term), Depth) tabrefute limit fms =     let r = deepen (\n -> (,n) <$> evalRS (tableau fms n) () ()) (Depth 0) limit in     failing Failure (Success . fst) r -tab :: (IsFirstOrder formula, Unify atom atom, Pretty formula, HasSkolem function,+tab :: (IsFirstOrder formula, Unify (atom, atom), term ~ UTermOf (atom, atom), Pretty formula, HasSkolem function,         atom ~ AtomOf formula, term ~ TermOf atom, function ~ FunOf term,         v ~ TVarOf term, v ~ SVarOf function) =>        Maybe Depth -> formula -> Failing ((K, Map v term), Depth)@@ -285,7 +288,7 @@ -- Try to split up the initial formula first; often a big improvement. -- ------------------------------------------------------------------------- splittab :: forall formula atom term v function.-            (IsFirstOrder formula, Unify atom atom, Ord formula, Pretty formula, HasSkolem function,+            (IsFirstOrder formula, Unify (atom, atom), term ~ UTermOf (atom, atom), Ord formula, Pretty formula, HasSkolem function,              atom ~ AtomOf formula, term ~ TermOf atom, function ~ FunOf term,              v ~ TVarOf term, v ~ SVarOf function) =>             formula -> [Failing ((K, Map v term), Depth)]

@@ -3,6 +3,7 @@ -- Copyright (c) 2003-2007, John Harrison. (See "LICENSE.txt" for details.)  {-# OPTIONS -Wall #-}+{-# LANGUAGE FlexibleContexts #-} {-# LANGUAGE FlexibleInstances #-} {-# LANGUAGE MultiParamTypeClasses #-} {-# LANGUAGE OverloadedStrings #-}@@ -10,7 +11,7 @@ {-# LANGUAGE TypeFamilies #-}  module Data.Logic.ATP.Unif-    ( Unify(unify)+    ( Unify(unify, UTermOf)     , unify_terms     , unify_literals     , unify_atoms@@ -31,31 +32,27 @@ import Data.Logic.ATP.Lib (Failing(Success, Failure)) import Data.Logic.ATP.Lit (IsLiteral, JustLiteral, zipLiterals') import Data.Logic.ATP.Skolem (SkAtom, SkTerm)-import Data.Logic.ATP.Term (IsTerm(..))+import Data.Logic.ATP.Term (IsTerm(..), IsVariable) import Data.Map.Strict as Map import Data.Maybe (fromMaybe) -- import Data.Sequence (Seq, viewl, ViewL(EmptyL, (:<))) import Test.HUnit hiding (State) --- | Main unification procedure.-class TermOf a ~ TermOf b => Unify a b where-    unify :: a -> b -> StateT (Map (TVarOf (TermOf a)) (TermOf a)) Failing ()-    -- ^ Unify the two elements of a pair, collecting variable-    -- assignments in the state.--{--instance Unify a b => Unify [a] [b] where-    unify [] [] = return ()-    unify (x : xs) (y : ys) = unify x y >> unify xs ys-    unify _ _ = fail "unify - list length mismatch"--instance Unify a b => Unify (Seq a) (Seq b) where-    unify xs ys =-        case (viewl xs, viewl ys) of-          (EmptyL, EmptyL) -> return ()-          (x :< xs', y :< ys') -> unify x y >> unify xs' ys'-          _ -> fail "unify - Seq list length mismatch"--}+-- | Main unification procedure.  The result of unification is a+-- mapping of variables to terms, so although we can unify two+-- dissimilar types, they must at least have the same term type (which+-- means the variable type will also match.)  The result of unifying+-- the two arguments is added to the state, while failure is signalled+-- in the Failing monad.+--+-- One might think that Unify should take two type parameters, the+-- types of two values to be unified, but there are instances where a+-- single type contains both - for example, in template-haskell we+-- want to unify a and b in a predicate such as this: @(AppT (AppT+-- EqualityT a) b)@.+class (IsTerm (UTermOf a), IsVariable (TVarOf (UTermOf a))) => Unify a where+    type UTermOf a+    unify :: a -> StateT (Map (TVarOf (UTermOf a)) (UTermOf a)) Failing ()  unify_terms :: (IsTerm term, v ~ TVarOf term) => [(term,term)] -> StateT (Map v term) Failing () unify_terms = mapM_ (uncurry unify_term_pair)@@ -111,7 +108,7 @@ -- who cares. unify_literals :: (IsLiteral lit1, HasApply atom1, atom1 ~ AtomOf lit1, term ~ TermOf atom1,                    JustLiteral lit2, HasApply atom2, atom2 ~ AtomOf lit2, term ~ TermOf atom2,-                   Unify atom1 atom2, v ~ TVarOf term) =>+                   Unify (atom1, atom2), term ~ UTermOf (atom1, atom2), v ~ TVarOf term) =>                   lit1 -> lit2 -> StateT (Map v term) Failing () unify_literals f1 f2 =     fromMaybe (fail "Can't unify literals") (zipLiterals' ho ne tf at f1 f2)@@ -119,7 +116,7 @@       ho _ _ = Nothing       ne p q = Just $ unify_literals p q       tf p q = if p == q then Just (unify_terms []) else Nothing-      at a1 a2 = Just (unify a1 a2)+      at a1 a2 = Just (unify (a1, a2))  unify_atoms :: (JustApply atom1, term ~ TermOf atom1,                 JustApply atom2, term ~ TermOf atom2,@@ -143,8 +140,9 @@ --        where --          app (t1, t2) = fullunify eqs >>= \i -> return $ (tsubst i t1, tsubst i t2) -instance Unify SkAtom SkAtom where-    unify = unify_atoms_eq+instance Unify (SkAtom, SkAtom) where+    type UTermOf (SkAtom, SkAtom) = TermOf SkAtom+    unify = uncurry unify_atoms_eq  test01, test02, test03, test04 :: Test test01 = TestCase (assertEqual "Unify test 1"