atp-haskell 1.7 → 1.8

raw patch · 11 files changed

+199/−151 lines, 11 filesdep +applicative-extrasPVP ok

version bump matches the API change (PVP)

Dependencies added: applicative-extras

API changes (from Hackage documentation)

Files

• atp-haskell.cabal +3/−1
• src/Data/Logic/ATP/Apply.hs +8/−5
• src/Data/Logic/ATP/Equate.hs +21/−22
• src/Data/Logic/ATP/Lib.hs +1/−19
• src/Data/Logic/ATP/LitWrapper.hs +43/−0
• src/Data/Logic/ATP/Meson.hs +9/−9
• src/Data/Logic/ATP/Prop.hs +48/−46
• src/Data/Logic/ATP/Resolution.hs +16/−16
• src/Data/Logic/ATP/Tableaux.hs +18/−16
• src/Data/Logic/ATP/Term.hs +5/−0
• src/Data/Logic/ATP/Unif.hs +27/−17

@@ -1,5 +1,5 @@ Name:             atp-haskell-Version:          1.7+Version:          1.8 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@@ -22,6 +22,7 @@  Library   Build-Depends:+    applicative-extras,     base >= 4.8 && < 5,     containers,     HUnit,@@ -42,6 +43,7 @@     Data.Logic.ATP.Equate     --     Data.Logic.ATP.Lit+    Data.Logic.ATP.LitWrapper     Data.Logic.ATP.Prop     Data.Logic.ATP.PropExamples     Data.Logic.ATP.DefCNF

@@ -50,13 +50,15 @@ -- an 'IsAtom'. class (Eq predicate, Ord predicate, Show predicate, IsString predicate, Pretty predicate) => IsPredicate predicate +-- | The result of applying a predicate to some terms is an atomic+-- formula whose type is an instance of 'HasApply'. class (IsAtom atom, IsPredicate (PredOf atom), IsTerm (TermOf atom)) => HasApply atom where     type PredOf atom     type TermOf atom     applyPredicate :: PredOf atom -> [(TermOf atom)] -> atom-    foldApply' :: (atom -> r) -> (PredOf atom -> [(TermOf atom)] -> r) -> atom -> r-    overterms :: ((TermOf atom) -> r -> r) -> r -> atom -> r-    onterms :: ((TermOf atom) -> (TermOf atom)) -> atom -> atom+    foldApply' :: (atom -> r) -> (PredOf atom -> [TermOf atom] -> r) -> atom -> r+    overterms :: (TermOf atom -> r -> r) -> r -> atom -> r+    onterms :: (TermOf atom -> TermOf atom) -> atom -> atom  -- | The set of functions in an atom. atomFuncs :: (HasApply atom, function ~ FunOf (TermOf atom)) => atom -> Set (function, Arity)@@ -89,8 +91,9 @@ ontermsApply f = foldApply (\p ts -> applyPredicate p (map f ts))  -- | Zip two atoms if they are similar-zipApplys :: (JustApply atom, term ~ TermOf atom, predicate ~ PredOf atom) =>-                 (predicate -> [(term, term)] -> Maybe r) -> atom -> atom -> Maybe r+zipApplys :: (JustApply atom1, term ~ TermOf atom1, predicate ~ PredOf atom1,+              JustApply atom2, term ~ TermOf atom2, predicate ~ PredOf atom2) =>+             (predicate -> [(term, term)] -> Maybe r) -> atom1 -> atom2 -> Maybe r zipApplys f atom1 atom2 =     foldApply f' atom1     where

@@ -1,4 +1,4 @@--- | ATOM with the Equate predicate+-- | ATOM with a distinguished Equate predicate.  {-# LANGUAGE DeriveDataTypeable #-} {-# LANGUAGE FlexibleContexts #-}@@ -16,7 +16,6 @@     ( HasEquate(equate, foldEquate)     , (.=.)     , zipEquates-    , isEquate     , prettyEquate     , overtermsEq     , ontermsEq@@ -39,22 +38,24 @@ import Prelude hiding (pred) import Text.PrettyPrint.HughesPJClass (maybeParens, Pretty(pPrintPrec), PrettyLevel) --- | Atoms that support equality must have HasEquate instance+-- | Atoms that support equality must be an instance of HasEquate class HasApply atom => HasEquate atom where     equate :: TermOf atom -> TermOf atom -> atom+    -- ^ Create an equate predicate     foldEquate :: (TermOf atom -> TermOf atom -> r) -> (PredOf atom -> [TermOf atom] -> r) -> atom -> r+    -- ^ Analyze whether a predicate is an equate or a regular apply. --- | Build an equality formula from two terms.+-- | Combine 'equate' and 'atomic' to build a formula from two terms. (.=.) :: (IsFormula formula, HasEquate atom, atom ~ AtomOf formula) => TermOf atom -> TermOf atom -> formula a .=. b = atomic (equate a b) infix 6 .=.  -- | Zip two atoms that support equality-zipEquates :: HasEquate atom =>-              (TermOf atom -> TermOf atom ->-               TermOf atom -> TermOf atom -> Maybe r)-           -> (PredOf atom -> [(TermOf atom, TermOf atom)] -> Maybe r)-           -> atom -> atom -> Maybe r+zipEquates :: (HasEquate atom1, HasEquate atom2, PredOf atom1 ~ PredOf atom2) =>+              (TermOf atom1 -> TermOf atom1 ->+               TermOf atom2 -> TermOf atom2 -> Maybe r)+           -> (PredOf atom1 -> [(TermOf atom1, TermOf atom2)] -> Maybe r)+           -> atom1 -> atom2 -> Maybe r zipEquates eq ap atom1 atom2 =     foldEquate eq' ap' atom1     where@@ -63,32 +64,30 @@       ap'' p1 ts1 p2 ts2 | p1 == p2 && length ts1 == length ts2 = ap p1 (zip ts1 ts2)       ap'' _ _ _ _ = Nothing -isEquate :: HasEquate atom => atom -> Bool-isEquate = foldEquate (\_ _ -> True) (\_ _ -> False)---- | Format the infix equality predicate applied to two terms.-prettyEquate :: IsTerm term => PrettyLevel -> Rational -> term -> term -> Doc-prettyEquate l p t1 t2 =-    maybeParens (p > atomPrec) $ pPrintPrec l atomPrec t1 <> text "=" <> pPrintPrec l atomPrec t2+-- | Convert between HasEquate atom types.+convertEquate :: (HasEquate atom1, HasEquate atom2) =>+                 (PredOf atom1 -> PredOf atom2) -> (TermOf atom1 -> TermOf atom2) -> atom1 -> atom2+convertEquate cp ct = foldEquate (\t1 t2 -> equate (ct t1) (ct t2)) (\p1 ts1 -> applyPredicate (cp p1) (map ct ts1)) --- | Implementation of 'overterms' for 'HasApply' types.+-- | Implementation of 'overterms' for 'HasEquate' types. overtermsEq :: HasEquate atom => ((TermOf atom) -> r -> r) -> r -> atom -> r overtermsEq f r0 = foldEquate (\t1 t2 -> f t2 (f t1 r0)) (\_ ts -> foldr f r0 ts) --- | Implementation of 'onterms' for 'HasApply' types.+-- | Implementation of 'onterms' for 'HasEquate' types. ontermsEq :: HasEquate atom => ((TermOf atom) -> (TermOf atom)) -> atom -> atom ontermsEq f = foldEquate (\t1 t2 -> equate (f t1) (f t2)) (\p ts -> applyPredicate p (map f ts)) --- | Implementation of Show for HasEquate types+-- | Implementation of Show for 'HasEquate' types showApplyAndEquate :: (HasEquate atom, Show (TermOf atom)) => atom -> String showApplyAndEquate atom = foldEquate showEquate showApply atom  showEquate :: Show term => term -> term -> String showEquate t1 t2 = "(" ++ show t1 ++ ") .=. (" ++ show t2 ++ ")" -convertEquate :: (HasEquate atom1, HasEquate atom2) =>-                 (PredOf atom1 -> PredOf atom2) -> (TermOf atom1 -> TermOf atom2) -> atom1 -> atom2-convertEquate cp ct = foldEquate (\t1 t2 -> equate (ct t1) (ct t2)) (\p1 ts1 -> applyPredicate (cp p1) (map ct ts1))+-- | Format the infix equality predicate applied to two terms.+prettyEquate :: IsTerm term => PrettyLevel -> Rational -> term -> term -> Doc+prettyEquate l p t1 t2 =+    maybeParens (p > atomPrec) $ pPrintPrec l atomPrec t1 <> text "=" <> pPrintPrec l atomPrec t2  precedenceEquate :: HasEquate atom => atom -> Precedence precedenceEquate = foldEquate (\_ _ -> eqPrec) (\_ _ -> pAppPrec)

@@ -54,7 +54,7 @@     , testLib     ) where -import Control.Applicative (Alternative(empty, (<|>)))+import Control.Applicative.Error (Failing(..)) import Control.Concurrent (forkIO, killThread, newEmptyMVar, putMVar, takeMVar, threadDelay) import Control.Monad.RWS (evalRWS, runRWS, RWS) import Data.Data (Data)@@ -77,25 +77,7 @@  -- | An error idiom.  Rather like the error monad, but collect all -- errors together-data Failing a = Success a | Failure [ErrorMsg] deriving Show type ErrorMsg = String--instance Functor Failing where-  fmap _ (Failure fs) = Failure fs-  fmap f (Success a) = Success (f a)--instance Applicative Failing where-   pure = Success-   Failure msgs <*> Failure msgs' = Failure (msgs ++ msgs')-   Success _ <*> Failure msgs' = Failure msgs'-   Failure msgs' <*> Success _ = Failure msgs'-   Success f <*> Success x = Success (f x)--instance Alternative Failing where-  empty                       = Failure []-  (Success x) <|> _           = Success x-  _           <|> (Success y) = Success y-  (Failure x) <|> (Failure y) = Failure (x ++ y)  failing :: ([String] -> b) -> (a -> b) -> Failing a -> b failing f _ (Failure errs) = f errs

@@ -0,0 +1,43 @@+{-# LANGUAGE FlexibleContexts, ScopedTypeVariables, TypeFamilies, UndecidableInstances #-}+module Data.Logic.ATP.LitWrapper+    ( JL(unJL)+    ) where++import Data.Logic.ATP.Formulas+import Data.Logic.ATP.Lit+import Data.Logic.ATP.Pretty++-- | Wrapper type to make an IsLiteral value that happens to also be+-- JustLiteral.  The JL constructor is not exported, JL values can be+-- built using 'convertToLiteral'.+newtype JL a = JL {unJL :: a}++instance Pretty a => Pretty (JL a) where+    pPrint (JL x) = pPrint x++instance HasFixity a => HasFixity (JL a) where+    precedence = precedence . unJL+    associativity = associativity . unJL++instance IsLiteral a => IsFormula (JL a) where+    type AtomOf (JL a) = AtomOf a+    asBool (JL x) = asBool x+    true = JL (true :: a)+    false = JL (false :: a)+    atomic = JL . atomic+    overatoms f (JL x) r0 = overatomsLiteral' {-(\y r -> f (JL y) r)-} f x r0+    onatoms f (JL x) = JL (onatoms f x)++instance (IsFormula (JL a), IsLiteral a) => JustLiteral (JL a)++instance (IsFormula (JL a), IsLiteral a) => IsLiteral (JL a) where+    naiveNegate (JL x) = JL (naiveNegate x)+    foldNegation n i (JL x) = foldNegation (n . JL) (i . JL) x+    foldLiteral' ho ne tf at (JL x) = foldLiteral' (ho . JL) (ne . JL) tf at x++-- | Unsafe local version of overatomsLiteral - assumes lit is a JustLiteral.+overatomsLiteral' :: IsLiteral lit => (AtomOf lit -> r -> r) -> lit -> r -> r+overatomsLiteral' f fm r0 =+        foldLiteral' undefined ne (const r0) (flip f r0) fm+        where+          ne fm' = overatomsLiteral' f fm' r0

@@ -176,7 +176,7 @@ -- -------------------------------------------------------------------------  mexpand1 :: (JustLiteral lit, Ord lit,-             HasApply atom, IsTerm term, Unify atom v term,+             HasApply atom, IsTerm term, Unify 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 v term, Ord fof,+              (IsFirstOrder fof, Unify 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 (VarOf fof) (TermOf (atom)), Ord fof, HasSkolem function, Monad m,+          (IsFirstOrder fof, Unify 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 v term, IsTerm term,+equal :: (JustLiteral lit, HasApply atom, Unify 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 v term,+mexpand2 :: (JustLiteral lit, Ord lit, HasApply atom, IsTerm term, Unify 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 v term, IsTerm term,+mexpands :: (JustLiteral lit, Ord lit, HasApply atom, Unify 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 v term, Ord fof+              Unify 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 v term, Ord fof,+          (IsFirstOrder fof, Unify 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 v term, HasSkolem function, Monad m, Ord fof,+meson :: (IsFirstOrder fof, Unify 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

@@ -18,10 +18,10 @@ {-# LANGUAGE UndecidableInstances #-}  module Data.Logic.ATP.Prop-    ( -- * binary operations-      BinOp(..), binop+    (     -- * Propositional formulas-    , IsPropositional((.|.), (.&.), (.<=>.), (.=>.), foldPropositional', foldCombination)+      IsPropositional((.|.), (.&.), (.<=>.), (.=>.), foldPropositional', foldCombination)+    , BinOp(..), binop     , (⇒), (==>), (⊃), (→)     , (⇔), (<=>), (↔), (<==>)     , (∧), (·)@@ -103,49 +103,6 @@ import Text.PrettyPrint.HughesPJClass (maybeParens, PrettyLevel, vcat) import Test.HUnit --- | Implication synonyms.  Note that if the -XUnicodeSyntax option is--- turned on the operator ⇒ can not be declared/used as a function ---- it becomes a reserved special character used in type signatures.-(⇒), (⊃), (==>), (→) :: IsPropositional formula => formula -> formula -> formula-(⇒) = (.=>.)-(⊃) = (.=>.)-(==>) = (.=>.)-(→) = (.=>.)-infixr 3 .=>., ⇒, ⊃, ==>, →---- | If-and-only-if synonyms-(<=>), (<==>), (⇔), (↔) :: IsPropositional formula => formula -> formula -> formula-(<=>) = (.<=>.)-(<==>) = (.<=>.)-(⇔) = (.<=>.)-(↔) = (.<=>.)-infixl 2 .<=>., <=>, <==>, ⇔, ↔---- | And/conjunction synonyms-(∧), (·) :: IsPropositional formula => formula -> formula -> formula-(∧) = (.&.)-(·) = (.&.)-infixl 5 .&., ∧, ·---- | Or/disjunction synonyms-(∨) :: IsPropositional formula => formula -> formula -> formula-(∨) = (.|.)-infixl 4 .|., ∨--data BinOp-    = (:<=>:)-    | (:=>:)-    | (:&:)-    | (:|:)-    deriving (Eq, Ord, Data, Typeable, Show, Enum, Bounded)---- | Combine formulas with a 'BinOp'.-binop :: IsPropositional formula => formula -> BinOp -> formula -> formula-binop f1 (:<=>:) f2 = f1 .<=>. f2-binop f1 (:=>:) f2 = f1 .=>. f2-binop f1 (:&:) f2 = f1 .&. f2-binop f1 (:|:) f2 = f1 .|. f2- -- |A type class for propositional logic.  If the type we are writing -- an instance for is a zero-order (aka propositional) logic type -- there will generally by a type or a type parameter corresponding to@@ -183,6 +140,35 @@                     -> (formula -> formula -> r) -- equivalence                     -> formula -> r +-- | Implication synonyms.  Note that if the -XUnicodeSyntax option is+-- turned on the operator ⇒ can not be declared/used as a function -+-- it becomes a reserved special character used in type signatures.+(⇒), (⊃), (==>), (→) :: IsPropositional formula => formula -> formula -> formula+(⇒) = (.=>.)+(⊃) = (.=>.)+(==>) = (.=>.)+(→) = (.=>.)+infixr 3 .=>., ⇒, ⊃, ==>, →++-- | If-and-only-if synonyms+(<=>), (<==>), (⇔), (↔) :: IsPropositional formula => formula -> formula -> formula+(<=>) = (.<=>.)+(<==>) = (.<=>.)+(⇔) = (.<=>.)+(↔) = (.<=>.)+infixl 2 .<=>., <=>, <==>, ⇔, ↔++-- | And/conjunction synonyms+(∧), (·) :: IsPropositional formula => formula -> formula -> formula+(∧) = (.&.)+(·) = (.&.)+infixl 5 .&., ∧, ·++-- | Or/disjunction synonyms+(∨) :: IsPropositional formula => formula -> formula -> formula+(∨) = (.|.)+infixl 4 .|., ∨+ -- | Deconstruct a 'JustPropositional' formula. foldPropositional :: JustPropositional pf =>                      (pf -> BinOp -> pf -> r) -- ^ fold on a binary operation formula@@ -191,6 +177,22 @@                   -> (AtomOf pf -> r)         -- ^ fold on an atomic formula                   -> pf -> r foldPropositional = foldPropositional' (error "JustPropositional failure")++-- | This type is used to construct the first argument of 'foldPropositional'.+data BinOp+    = (:<=>:)+    | (:=>:)+    | (:&:)+    | (:|:)+    deriving (Eq, Ord, Data, Typeable, Show, Enum, Bounded)++-- | Combine formulas with a 'BinOp', for use building the first+-- argument of 'foldPropositional'.+binop :: IsPropositional formula => formula -> BinOp -> formula -> formula+binop f1 (:<=>:) f2 = f1 .<=>. f2+binop f1 (:=>:) f2 = f1 .=>. f2+binop f1 (:&:) f2 = f1 .&. f2+binop f1 (:|:) f2 = f1 .|. f2  -- | Combine two 'JustPropositional' formulas if they are similar. zipPropositional :: (JustPropositional pf1, JustPropositional pf2) =>

@@ -68,7 +68,7 @@  -- | MGU of a set of literals. mgu :: forall lit atom term v.-       (IsLiteral lit, HasApply atom, Unify atom v term, IsTerm term,+       (JustLiteral lit, HasApply atom, Unify 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 :: (IsLiteral lit, IsTerm term, HasApply atom, Unify atom v term,+unifiable :: (JustLiteral lit, IsTerm term, HasApply atom, Unify 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 v term, IsTerm term,+resolvents :: (JustLiteral lit, Ord lit, HasApply atom, Unify 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 v term, IsTerm term,+resolve_clauses :: (JustLiteral lit, Ord lit, HasApply atom, Unify 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 v term,+resloop1 :: (JustLiteral lit, Ord lit, HasApply atom, IsTerm term, Unify 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 v term,+                     Unify 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 v term, Ord fof, HasSkolem function, Monad m,+               (IsFirstOrder fof, Unify 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 v term, Match (atom, atom) v term, HasSkolem function, Monad m, Ord fof,+               (IsFirstOrder fof, Unify 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 v term, Match (atom, atom) v term,+                     Unify 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 v term, Match (atom, atom) v term,+             Unify 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 v term, Match (atom, atom) v term, HasSkolem function, Monad m, Ord fof, Pretty fof,+               (IsFirstOrder fof, Unify 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 v term, Match (atom, atom) v term, Ord fof, Pretty fof,+                    (IsFirstOrder fof, Unify 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 v term,+             Match (atom, atom) v term, Unify 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 v term,+presolve_clauses :: (JustLiteral lit, Ord lit, HasApply atom, IsTerm term, Unify 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 v term, Match (atom, atom) v term, HasSkolem function, Monad m, Ord fof,+               (IsFirstOrder fof, Unify 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 v term,+                     Unify atom atom,                      Match (atom, atom) v term,                      Ord fof, Pretty fof) => fof -> Failing Bool pure_resolution3 fm =

@@ -30,7 +30,8 @@ import Data.Logic.ATP.Formulas (atomic, IsFormula(asBool, AtomOf), onatoms, overatoms) import Data.Logic.ATP.Herbrand (davisputnam) import Data.Logic.ATP.Lib ((|=>), allpairs, deepen, Depth(Depth), distrib, evalRS, Failing(Success, Failure), failing, settryfind, tryfindM)-import Data.Logic.ATP.Lit ((.~.), IsLiteral, JustLiteral, LFormula, positive)+import Data.Logic.ATP.Lit ((.~.), convertToLiteral, IsLiteral, JustLiteral, LFormula, positive)+import Data.Logic.ATP.LitWrapper (JL) import Data.Logic.ATP.Pretty (assertEqual', Pretty(pPrint), prettyShow, text) import Data.Logic.ATP.Prop ( (.&.), (.=>.), (.<=>.), (.|.), BinOp((:&:), (:|:)), PFormula, simpdnf) import Data.Logic.ATP.Quantified (exists, foldQuantified, for_all, Quant((:!:)))@@ -44,13 +45,13 @@ import Test.HUnit hiding (State)  -- | Unify complementary literals.-unify_complements :: (IsLiteral lit, HasApply atom, Unify atom v term,-                      atom ~ AtomOf lit, term ~ TermOf atom, v ~ TVarOf term) =>-                     lit -> lit -> StateT (Map v term) Failing ()+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) =>+                     lit1 -> lit2 -> StateT (Map v term) Failing () unify_complements p q = unify_literals p ((.~.) q)  -- | Unify and refute a set of disjuncts.-unify_refute :: (IsLiteral lit, Ord lit, HasApply atom, Unify atom v term, IsTerm term,+unify_refute :: (JustLiteral lit, Ord lit, HasApply atom, Unify atom atom, IsTerm term,                  atom ~ AtomOf lit, term ~ TermOf atom, v ~ TVarOf term) =>                 Set (Set lit) -> Map v term -> Failing (Map v term) unify_refute djs env =@@ -64,7 +65,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 v term,+                (JustLiteral lit, Ord lit, HasApply atom, Unify 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 =@@ -77,7 +78,7 @@       newvar k = vt (fromString ("_" ++ show (n * length fvs + k)))  prawitz :: forall formula atom term function v.-           (IsFirstOrder formula, Ord formula, Unify atom v term, HasSkolem function, Show formula,+           (IsFirstOrder formula, Ord formula, Unify atom atom, HasSkolem function, Show formula,             atom ~ AtomOf formula, term ~ TermOf atom, function ~ FunOf term,             v ~ TVarOf term, v ~ SVarOf function) =>            formula -> Int@@ -106,7 +107,7 @@ -- Comparison of number of ground instances. -- ------------------------------------------------------------------------- -compare :: (IsFirstOrder formula, Ord formula, Unify atom v term, HasSkolem function, Show formula,+compare :: (IsFirstOrder formula, Ord formula, Unify atom atom, HasSkolem function, Show formula,             atom ~ AtomOf formula, term ~ TermOf atom, function ~ FunOf term,             v ~ TVarOf term, v ~ SVarOf function) =>            formula -> (Int, Int)@@ -174,13 +175,13 @@  -- | More standard tableau procedure, effectively doing DNF incrementally.  (p. 177) tableau :: forall formula atom term v function.-           (IsFirstOrder formula, Unify atom v term,+           (IsFirstOrder formula, Unify 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 =     go (fms, [], n0) (return . Success) (K 0, Map.empty)     where-      go :: ([formula], [formula], Depth)+      go :: ([formula], [JL formula], Depth)          -> ((K, Map v term) -> RWS () () () (Failing (K, Map v term)))          -> (K, Map v term)          -> RWS () () () (Failing (K, Map v term))@@ -203,20 +204,21 @@              go2 :: formula -> [formula] -> RWS () () () (Failing (K, Map v term))             go2 fm' unexp' =-                tryfindM (tryLit fm') lits >>=-                failing (\_ -> go (unexp', fm' : lits, n) cont (k, env))+                let (fm'' :: JL formula) = convertToLiteral (error "expected JustLiteral") id fm' in+                tryfindM (tryLit fm'') lits >>=+                failing (\_ -> go (unexp', fm'' : lits, n) cont (k, env))                         (return . Success)-            tryLit :: formula -> formula -> RWS () () () (Failing (K, Map v term))+            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 v term,+tabrefute :: (IsFirstOrder formula, Unify 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 v term, Pretty formula, HasSkolem function,+tab :: (IsFirstOrder formula, Unify 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)@@ -283,7 +285,7 @@ -- Try to split up the initial formula first; often a big improvement. -- ------------------------------------------------------------------------- splittab :: forall formula atom term v function.-            (IsFirstOrder formula, Unify atom v term, Ord formula, Pretty formula, HasSkolem function,+            (IsFirstOrder formula, Unify 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)]

@@ -1,3 +1,8 @@+-- | A Term is a expression representing a domain element.  It is+-- composed of variables which can be bound to domain elements, or+-- functions which can be applied to terms to yield other domain+-- elements.+ {-# LANGUAGE DeriveDataTypeable #-} {-# LANGUAGE FlexibleContexts #-} {-# LANGUAGE FlexibleInstances #-}

@@ -24,36 +24,38 @@ import Control.Monad.State -- (evalStateT, runStateT, State, StateT, get) import Data.Bool (bool) import Data.List as List (map)-import Data.Logic.ATP.Apply (HasApply(TermOf), JustApply, zipApplys)+import Data.Logic.ATP.Apply (HasApply(TermOf, PredOf), JustApply, zipApplys) import Data.Logic.ATP.Equate (HasEquate, zipEquates) import Data.Logic.ATP.FOL (tsubst) import Data.Logic.ATP.Formulas (IsFormula(AtomOf)) import Data.Logic.ATP.Lib (Failing(Success, Failure))-import Data.Logic.ATP.Lit (IsLiteral, zipLiterals')+import Data.Logic.ATP.Lit (IsLiteral, JustLiteral, zipLiterals') import Data.Logic.ATP.Skolem (SkAtom, SkTerm)-import Data.Logic.ATP.Term (IsTerm(..), V)+import Data.Logic.ATP.Term (IsTerm(..)) import Data.Map.Strict as Map import Data.Maybe (fromMaybe)-import Data.Sequence (Seq, viewl, ViewL(EmptyL, (:<)))+-- import Data.Sequence (Seq, viewl, ViewL(EmptyL, (:<))) import Test.HUnit hiding (State)  -- | Main unification procedure.-class Unify a v term where-    unify :: a -> a -> StateT (Map v term) Failing ()+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 v term => Unify [a] v term where+{-+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 v term => Unify (Seq a) v term where+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"+-}  unify_terms :: (IsTerm term, v ~ TVarOf term) => [(term,term)] -> StateT (Map v term) Failing () unify_terms = mapM_ (uncurry unify_term_pair)@@ -103,10 +105,14 @@ unify_and_apply eqs =     fullunify eqs >>= \i -> return $ List.map (\ (t1, t2) -> (tsubst i t1, tsubst i t2)) eqs --- | Unify literals-unify_literals :: (IsLiteral lit, HasApply atom, Unify atom v term,-                   atom ~ AtomOf lit, term ~ TermOf atom, v ~ TVarOf term) =>-                  lit -> lit -> StateT (Map v term) Failing ()+-- | Unify literals, perhaps of different types, but sharing term and+-- variable type.  Note that only one needs to be 'JustLiteral', if+-- the unification succeeds the other must have been too, if it fails,+-- 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) =>+                  lit1 -> lit2 -> StateT (Map v term) Failing () unify_literals f1 f2 =     fromMaybe (fail "Can't unify literals") (zipLiterals' ho ne tf at f1 f2)     where@@ -115,13 +121,17 @@       tf p q = if p == q then Just (unify_terms []) else Nothing       at a1 a2 = Just (unify a1 a2) -unify_atoms :: (JustApply atom, term ~ TermOf atom, v ~ TVarOf term) =>-               (atom, atom) -> StateT (Map v term) Failing ()+unify_atoms :: (JustApply atom1, term ~ TermOf atom1,+                JustApply atom2, term ~ TermOf atom2,+                v ~ TVarOf term, PredOf atom1 ~ PredOf atom2) =>+               (atom1, atom2) -> StateT (Map v term) Failing () unify_atoms (a1, a2) =     maybe (fail "unify_atoms") id (zipApplys (\_ tpairs -> Just (unify_terms tpairs)) a1 a2) -unify_atoms_eq :: (HasEquate atom, term ~ TermOf atom, v ~ TVarOf term) =>-                  atom -> atom -> StateT (Map v term) Failing ()+unify_atoms_eq :: (HasEquate atom1, term ~ TermOf atom1,+                   HasEquate atom2, term ~ TermOf atom2,+                   PredOf atom1 ~ PredOf atom2, v ~ TVarOf term) =>+                  atom1 -> atom2 -> StateT (Map v term) Failing () unify_atoms_eq a1 a2 =     maybe (fail "unify_atoms") id (zipEquates (\l1 r1 l2 r2 -> Just (unify_terms [(l1, l2), (r1, r2)]))                                               (\_ tpairs -> Just (unify_terms tpairs))@@ -133,7 +143,7 @@ --        where --          app (t1, t2) = fullunify eqs >>= \i -> return $ (tsubst i t1, tsubst i t2) -instance Unify SkAtom V SkTerm where+instance Unify SkAtom SkAtom where     unify = unify_atoms_eq  test01, test02, test03, test04 :: Test