logic-classes 1.4.4 → 1.4.5

raw patch · 7 files changed

+36/−10 lines, 7 files

Files

• Data/Logic/Classes/Literal.hs +1/−0
• Data/Logic/Harrison/Lib.hs +27/−3
• Data/Logic/Harrison/Normal.hs +1/−2
• Data/Logic/Harrison/Resolution.hs +2/−2
• Data/Logic/Harrison/Unif.hs +2/−1
• Data/Logic/Tests/Harrison/Unif.hs +2/−1
• logic-classes.cabal +1/−1

@@ -18,6 +18,7 @@ import Data.Logic.Classes.Pretty (HasFixity(..), Fixity(..), FixityDirection(..)) import qualified Data.Logic.Classes.Propositional as P import Data.Logic.Classes.Negate+import Data.Logic.Harrison.Lib ({- instance Monad Failing -}) import Text.PrettyPrint (Doc, (<>), text, parens, nest)  -- |Literals are the building blocks of the clause and implicative normal

@@ -1,7 +1,8 @@-{-# LANGUAGE RankNTypes #-}+{-# LANGUAGE DeriveDataTypeable, RankNTypes, StandaloneDeriving #-} {-# OPTIONS_GHC -Wall -fno-warn-unused-binds #-} module Data.Logic.Harrison.Lib-    ( tests+    ( failing+    , tests     , setAny     , setAll     -- , itlist2@@ -34,11 +35,34 @@     , (∅)     ) where -import Control.Applicative.Error (Failing(..), failing)+import Control.Applicative.Error (Failing(..), ErrorMsg)+import Data.Generics import qualified Data.Map as Map import Data.Maybe import qualified Data.Set as Set import Test.HUnit (Test(TestCase, TestList, TestLabel), assertEqual)++-- | Case analysis for the 'Failing' type, from unpublished changes to +-- the applicative-extras packages.  If the value is @'Failure'@, apply +-- the first function to @[ErrorMsg]@; if it is @'Success' a@, apply +-- the second function to @a@.+failing :: ([ErrorMsg] -> b) -> (a -> b) -> Failing a -> b+failing f _ (Failure errs) = f errs+failing _ f (Success a)    = f a+ +instance Monad Failing where+  return = Success+  m >>= f =+      case m of+        (Failure errs) -> (Failure errs)+        (Success a) -> f a+  fail errMsg = Failure [errMsg]+  +deriving instance Typeable1 Failing+deriving instance Data a => Data (Failing a)+deriving instance Read a => Read (Failing a)+deriving instance Eq a => Eq (Failing a)+deriving instance Ord a => Ord (Failing a)  (∅) :: Set.Set a (∅) = Set.empty

@@ -9,14 +9,13 @@     , simpcnf'     ) where -import Control.Applicative.Error (failing) import Data.Logic.Classes.Combine (Combination(..), BinOp(..)) import Data.Logic.Classes.Constants (Constants(..)) import Data.Logic.Classes.FirstOrder (FirstOrderFormula(..)) import Data.Logic.Classes.Formula (Formula(atomic)) import Data.Logic.Classes.Literal (Literal, fromFirstOrder) import Data.Logic.Classes.Negate (Negatable, negated, (.~.))-import Data.Logic.Harrison.Lib (setAny, allpairs)+import Data.Logic.Harrison.Lib (setAny, allpairs, failing) import Data.Logic.Harrison.Skolem (nnf) import qualified Data.Set.Extra as Set import Prelude hiding (negate)

@@ -8,7 +8,7 @@     , matchAtomsEq     ) where -import Control.Applicative.Error (Failing(..), failing)+import Control.Applicative.Error (Failing(..)) import Data.Logic.Classes.Atom (Atom(match)) import Data.Logic.Classes.Combine (Combination(..)) import Data.Logic.Classes.Equals (AtomEq, zipAtomsEq)@@ -20,7 +20,7 @@ import Data.Logic.Classes.Variable (Variable(prefix)) import Data.Logic.Harrison.FOL (subst, fv, generalize, list_disj, list_conj) import Data.Logic.Harrison.Lib (settryfind, allpairs, allsubsets, setAny, setAll,-                                allnonemptysubsets, (|->), apply, defined)+                                allnonemptysubsets, (|->), apply, defined, failing) import Data.Logic.Harrison.Normal (simpdnf, simpcnf, trivial) import Data.Logic.Harrison.Skolem (pnf, SkolemT, askolemize, specialize) import Data.Logic.Harrison.Tableaux (unify_literals)

@@ -6,8 +6,9 @@     , unifyAndApply     ) where -import Control.Applicative.Error (Failing(..), failing)+import Control.Applicative.Error (Failing(..)) import Data.Logic.Classes.Term (Term(..), tsubst)+import Data.Logic.Harrison.Lib (failing) import qualified Data.Map as Map {- (* ========================================================================= *)

@@ -4,8 +4,9 @@     ( tests     ) where -import Control.Applicative.Error (Failing(..), failing)+import Control.Applicative.Error (Failing(..)) import Data.Logic.Classes.Term (Term(fApp, vt), tsubst)+import Data.Logic.Harrison.Lib (failing) import Data.Logic.Harrison.Unif (fullUnify) import Data.Logic.Tests.HUnit () import Data.Logic.Types.Harrison.FOL (TermType)

@@ -1,5 +1,5 @@ Name:             logic-classes-Version:          1.4.4+Version:          1.4.5 Synopsis:         Framework for propositional and first order logic, theorem proving Description:      Package to support Propositional and First Order Logic.  It includes classes                   representing the different types of formulas and terms, some instances of