diff --git a/Data/Logic/Classes/FirstOrder.hs b/Data/Logic/Classes/FirstOrder.hs --- a/Data/Logic/Classes/FirstOrder.hs +++ b/Data/Logic/Classes/FirstOrder.hs @@ -32,6 +32,8 @@ , onatoms , overatoms , atom_union + , fromFirstOrder + , fromLiteral ) where import Data.Generics (Data, Typeable) @@ -39,9 +41,12 @@ import Data.Logic.Classes.Constants import Data.Logic.Classes.Combine import Data.Logic.Classes.Formula (Formula(atomic)) +import Data.Logic.Classes.Literal (Literal, foldLiteral) +import Data.Logic.Classes.Negate ((.~.)) import Data.Logic.Classes.Pretty (Pretty(pretty), HasFixity(..), Fixity(..), FixityDirection(..)) import qualified Data.Logic.Classes.Propositional as P import Data.Logic.Classes.Variable (Variable) +import Data.Logic.Failing (Failing(..)) import Data.SafeCopy (base, deriveSafeCopy) import qualified Data.Set as Set import Text.PrettyPrint (Doc, (<>), (<+>), text, parens, nest) @@ -299,5 +304,22 @@ atom_union :: forall formula atom v a. (FirstOrderFormula formula atom v, Ord a) => (atom -> Set.Set a) -> formula -> Set.Set a atom_union f fm = overatoms (\ h t -> Set.union (f h) t) fm Set.empty + +-- |Just like Logic.FirstOrder.convertFOF except it rejects anything +-- with a construct unsupported in a normal logic formula, +-- i.e. quantifiers and formula combinators other than negation. +fromFirstOrder :: forall formula atom v lit atom2. + (Formula lit atom2, FirstOrderFormula formula atom v, Literal lit atom2) => + (atom -> atom2) -> formula -> Failing lit +fromFirstOrder ca formula = + foldFirstOrder (\ _ _ _ -> Failure ["fromFirstOrder"]) co (Success . fromBool) (Success . atomic . ca) formula + where + co :: Combination formula -> Failing lit + co ((:~:) f) = fromFirstOrder ca f >>= return . (.~.) + co _ = Failure ["fromFirstOrder"] + +fromLiteral :: forall lit atom v fof atom2. (Literal lit atom, FirstOrderFormula fof atom2 v) => + (atom -> atom2) -> lit -> fof +fromLiteral ca lit = foldLiteral (\ p -> (.~.) (fromLiteral ca p)) fromBool (atomic . ca) lit $(deriveSafeCopy 1 'base ''Quant) diff --git a/Data/Logic/Classes/Literal.hs b/Data/Logic/Classes/Literal.hs --- a/Data/Logic/Classes/Literal.hs +++ b/Data/Logic/Classes/Literal.hs @@ -3,8 +3,6 @@ module Data.Logic.Classes.Literal ( Literal(..) , zipLiterals - , fromFirstOrder - , fromLiteral , toPropositional , prettyLit , foldAtomsLiteral @@ -12,7 +10,6 @@ import Data.Logic.Classes.Combine (Combination(..)) import Data.Logic.Classes.Constants -import qualified Data.Logic.Classes.FirstOrder as FOF import Data.Logic.Classes.Formula (Formula(atomic)) import Data.Logic.Classes.Pretty (HasFixity(..), Fixity(..), FixityDirection(..)) import qualified Data.Logic.Classes.Propositional as P @@ -46,23 +43,6 @@ co _ = error "instance Literal FirstOrderFormula" atomic = Data.Logic.Classes.FirstOrder.atomic -} - --- |Just like Logic.FirstOrder.convertFOF except it rejects anything --- with a construct unsupported in a normal logic formula, --- i.e. quantifiers and formula combinators other than negation. -fromFirstOrder :: forall formula atom v lit atom2. - (Formula lit atom2, FOF.FirstOrderFormula formula atom v, Literal lit atom2) => - (atom -> atom2) -> formula -> Failing lit -fromFirstOrder ca formula = - FOF.foldFirstOrder (\ _ _ _ -> Failure ["fromFirstOrder"]) co (Success . fromBool) (Success . atomic . ca) formula - where - co :: Combination formula -> Failing lit - co ((:~:) f) = fromFirstOrder ca f >>= return . (.~.) - co _ = Failure ["fromFirstOrder"] - -fromLiteral :: forall lit atom v fof atom2. (Literal lit atom, FOF.FirstOrderFormula fof atom2 v) => - (atom -> atom2) -> lit -> fof -fromLiteral ca lit = foldLiteral (\ p -> (.~.) (fromLiteral ca p)) fromBool (atomic . ca) lit toPropositional :: forall lit atom pf atom2. (Literal lit atom, P.PropositionalFormula pf atom2) => (atom -> atom2) -> lit -> pf diff --git a/Data/Logic/Harrison/Normal.hs b/Data/Logic/Harrison/Normal.hs --- a/Data/Logic/Harrison/Normal.hs +++ b/Data/Logic/Harrison/Normal.hs @@ -11,9 +11,9 @@ import Data.Logic.Classes.Combine (Combination(..), BinOp(..)) import Data.Logic.Classes.Constants (Constants(..)) -import Data.Logic.Classes.FirstOrder (FirstOrderFormula(..)) +import Data.Logic.Classes.FirstOrder (FirstOrderFormula(..), fromFirstOrder) import Data.Logic.Classes.Formula (Formula(atomic)) -import Data.Logic.Classes.Literal (Literal, fromFirstOrder) +import Data.Logic.Classes.Literal (Literal) import Data.Logic.Classes.Negate (Negatable, negated, (.~.)) import Data.Logic.Failing (failing) import Data.Logic.Harrison.Lib (setAny, allpairs) diff --git a/Data/Logic/Tests/Common.hs b/Data/Logic/Tests/Common.hs --- a/Data/Logic/Tests/Common.hs +++ b/Data/Logic/Tests/Common.hs @@ -177,7 +177,7 @@ instance Eq Doc where a == b = show a == show b -data (formula ~ TFormula, atom ~ TAtom, v ~ V) => TestFormula formula atom v +data TestFormula formula atom v = TestFormula { formula :: formula , name :: String @@ -185,7 +185,7 @@ } -- deriving (Data, Typeable) -- |Some values that we might expect after transforming the formula. -data (FirstOrderFormula formula atom v, formula ~ TFormula, atom ~ TAtom, v ~ V) => Expected formula atom v +data Expected formula atom v = FirstOrderFormula formula | SimplifiedForm formula | NegationNormalForm formula diff --git a/Setup.hs b/Setup.hs --- a/Setup.hs +++ b/Setup.hs @@ -6,10 +6,12 @@ import Distribution.Simple.LocalBuildInfo (LocalBuildInfo(buildDir)) import Distribution.Simple.Program import System.Cmd +import System.Directory (copyFile) import System.Exit main :: IO () -main = defaultMainWithHooks simpleUserHooks { +main = copyFile "debian/changelog" "changelog" >> + defaultMainWithHooks simpleUserHooks { postBuild = \ _ _ _ lbi -> runTestScript lbi , runTests = \ _ _ _ lbi -> runTestScript lbi } diff --git a/changelog b/changelog new file mode 100644 --- /dev/null +++ b/changelog @@ -0,0 +1,484 @@ +haskell-logic-classes (1.4.8) unstable; urgency=low + + * Make changelog visible in hackage. + + -- David Fox Tue, 15 Oct 2013 07:48:21 -0700 + +haskell-logic-classes (1.4.7) unstable; urgency=low + + * Copy the two modules from the incremental-sat-solver package + (version 0.1.7) into logic-classes with a changed export list + so our SatSolver instance can access the data types. + + -- David Fox Sun, 06 Jan 2013 17:44:04 -0800 + +haskell-logic-classes (1.4.6) unstable; urgency=low + + * Get rid of some deprecated datatype contexts. + * Fix bug in hackage build. + + -- David Fox Wed, 20 Jun 2012 10:40:49 -0700 + +haskell-logic-classes (1.4.5) unstable; urgency=low + + * Build with stock applicative-extras package. + + -- David Fox Wed, 18 Apr 2012 07:41:30 -0700 + +haskell-logic-classes (1.4) unstable; urgency=low + + * Overhaul of the pretty printing, add Pretty class. + * Fixes to get precedence behavior to match Harrison + * Rename class Formula -> Atom (still need to add f parameter) + * Sort out tangled type parameters (but still need to switch to type + families.) + * Add HasFixity class, to go with Pretty class. Get precedence to + mostly work. + * Add Davis-Putnam and some Herbrand support. + * askolemize should not specialize, only skolemize removes quantifiers. + * Fix bad implementation of atomic method in PropositionalFormula for + Data.Logic.Types.FirstOrder type. + * Added an argument function to skolemize and skolemNormalForm to convert + the atom type of the original formula to that of the result. This means + it can convert to any PropositionalFormula type while skolemizing. + + -- David Fox Tue, 17 Jan 2012 21:00:28 -0800 + +haskell-logic-classes (1.3) unstable; urgency=low + + * Clean up the superclasses + + -- David Fox Fri, 13 Jan 2012 08:45:55 -0800 + +haskell-logic-classes (1.2) unstable; urgency=low + + * Add a Pretty class to pretty print formulas and friends. + + -- David Fox Tue, 10 Jan 2012 06:28:40 -0800 + +haskell-logic-classes (1.1) unstable; urgency=low + + * Use the Formula class to abstract out the two different types of Atom + functionality (with and without equality.) + + -- David Fox Mon, 09 Jan 2012 10:45:09 -0800 + +haskell-logic-classes (1.0.2) unstable; urgency=low + + * Two important fixes in the old version of simpcnf. + + -- David Fox Fri, 06 Jan 2012 05:37:12 -0800 + +haskell-logic-classes (1.0.1) unstable; urgency=low + + * Fixes for ghc 7.4. + + -- David Fox Tue, 03 Jan 2012 12:43:44 -0800 + +haskell-logic-classes (1.0.0) unstable; urgency=low + + * Rewrite. + + -- David Fox Wed, 21 Dec 2011 09:12:48 -0800 + +haskell-logic-classes (0.49) unstable; urgency=low + + * Fix a bug in the unification algorithm. Unification should fail if + we try to unify a variable with itself. + + -- David Fox Mon, 05 Dec 2011 17:02:49 -0800 + +haskell-logic-classes (0.48) unstable; urgency=low + + * Add missing test modules. + + -- David Fox Sun, 04 Dec 2011 18:29:25 -0800 + +haskell-logic-classes (0.47) unstable; urgency=low + + * Move some orphan ProofResult instances here from ontology.y + + -- David Fox Fri, 02 Dec 2011 11:41:33 -0800 + +haskell-logic-classes (0.46) unstable; urgency=low + + * Limit the recursion depth of the prover to 100. + + -- David Fox Tue, 29 Nov 2011 15:05:39 -0800 + +haskell-logic-classes (0.45) unstable; urgency=low + + * Modify the superclasses of the Ord instance of Formula in + Data.Logic.Types.FirstOrderPublic. It was causing a loop + when the PropLogic satisfiable function ran. + + -- David Fox Fri, 14 Oct 2011 10:15:50 -0700 + +haskell-logic-classes (0.44) unstable; urgency=low + + * Major re-organization of modules. + + -- David Fox Sun, 09 Oct 2011 17:31:36 -0700 + +haskell-logic (0.43) unstable; urgency=low + + * Move Propositional modules into Data.Logic.Propositional. + * Add a Native instance for PropositionalFormula. + * Add a Normal in the Propositional directory + * Add clauseNormalForm and disjunctiveNormalForm for Propositional + * Add clauseNormalFormAlt which is an alternate implementation of + clauseNormalForm, I'm not sure if it gives results that are actually + different or just look different, but it makes cabal-debian work. + + -- David Fox Thu, 29 Sep 2011 05:56:41 -0700 + +haskell-logic (0.42) unstable; urgency=low + + * Derive the show instance for ImplicativeNormalForm rather than + making a custom one. + + -- David Fox Fri, 23 Sep 2011 16:43:09 -0700 + +haskell-logic (0.41) unstable; urgency=low + + * Add field accessors to Proof type. + * Finish show implementation for Proof + + -- David Fox Mon, 08 Aug 2011 08:32:56 -0700 + +haskell-logic (0.40) unstable; urgency=low + + * Remove NoProof constructor from Proof type - we only need this in + the augumented Proof' type in the ontology package. + * Add prettyProof and prettyINF to Data.Logic.Pretty. + + -- David Fox Sat, 06 Aug 2011 06:28:20 -0700 + +haskell-logic (0.39) unstable; urgency=low + + * Move Proof type from ontology to logic. + + -- David Fox Thu, 04 Aug 2011 07:13:00 -0700 + +haskell-logic (0.38) unstable; urgency=low + + * Remove the triple of function parameters for converting formulas to + literals, these were all invariably id. + + -- David Fox Tue, 02 Aug 2011 07:34:54 -0700 + +haskell-logic (0.37) unstable; urgency=low + + * Add an Ord instance to ProofResult so we can insert proofs into sets. + + -- David Fox Mon, 01 Aug 2011 09:51:59 -0700 + +haskell-logic (0.36) unstable; urgency=low + + * Move module Test.Types to Data.Logic.Test and export so that clients + of this package can use the definitions to create test cases. + + -- David Fox Sun, 24 Jul 2011 10:45:50 -0700 + +haskell-logic (0.35) unstable; urgency=low + + * Remove the Pretty class. Pretty printing of a type is application + specific, so the type class doesn't make sense. Instead add function + parameters to prettyForm et. al. to convert the primitive types to + Doc. + + -- David Fox Fri, 22 Jul 2011 09:01:45 -0700 + +haskell-logic (0.34) unstable; urgency=low + + * Allow .=. literals in the Native instance. This required a fix to the + resolution prover so that it never did substitutions based on an + equality predicate which had the same lhs and rhs. + + -- David Fox Thu, 21 Jul 2011 22:30:14 -0700 + +haskell-logic (0.33) unstable; urgency=low + + * Move the modules into the Data heirarchy. + + -- David Fox Sun, 17 Jul 2011 07:29:49 -0700 + +haskell-logic (0.32) unstable; urgency=low + + * Add a Pred class to describe predicate application + * Split pretty printing and show into a module. + + -- David Fox Sat, 16 Jul 2011 15:24:43 -0700 + +haskell-logic (0.31) unstable; urgency=low + + * Create a second instance of FirstOrderFormula in the module + Logic.Instances.Public, with Eq and Ord instances that use + the normal form to detect formulas that are equivalent under + identity transforms. + * Export the Bijection class which converts between the public + and internal formula types. + + -- David Fox Wed, 06 Jul 2011 12:46:45 -0700 + +haskell-logic (0.30) unstable; urgency=low + + * Simplify the parameters of the ImplicativeNormalForm type in the + native instance, move it to Logic.Normal and eliminate the + ImplicativeNormalFormula class. + * Don't require all formula and term types to be instances of Ord, + we can just specify it in the functions that need it. + + -- David Fox Sat, 02 Jul 2011 09:20:57 -0700 + +haskell-logic (0.29) unstable; urgency=low + + * Ported to safe-copy + + -- Jeremy Shaw Fri, 17 Jun 2011 11:18:32 -0500 + +haskell-logic (0.28) unstable; urgency=low + + * Switch the order of some constructors so that defaultValue of + Formula gives us a simpler value. + + -- David Fox Sun, 01 May 2011 11:36:12 -0700 + +haskell-logic (0.27) unstable; urgency=low + + * Moved JSON instances back to seereason. + + -- David Fox Wed, 13 Apr 2011 20:53:42 -0700 + +haskell-logic (0.26) unstable; urgency=low + + * Add JSON instances. + + -- David Fox Mon, 04 Apr 2011 07:21:25 -0600 + +haskell-logic (0.25) unstable; urgency=low + + * Disable the (unused) Logic-TPTP instance, it is blocking the + ghc7 build. + + -- David Fox Sat, 30 Oct 2010 10:35:35 -0700 + +haskell-logic (0.24) unstable; urgency=low + + * Add a missing paren in the pretty printing and show instances. + + -- David Fox Wed, 20 Oct 2010 21:17:34 -0700 + +haskell-logic (0.23) unstable; urgency=low + + * Add a "one" method to the Variable class which returns any instance of + the class, preferably some general purpose variable name like "x". + + -- David Fox Wed, 06 Oct 2010 12:28:38 -0700 + +haskell-logic (0.22) unstable; urgency=low + + * Instead of making variables instances of Enum and having non-working + fromEnum and toEnum methods, create a class Var with only a "next" + method. + * Add an Arity class and make it a super class of the predicate types. + * Replace the pApp method with pApp0, pApp1, pApp2 ... pApp7, add a + pApp function that checks the predicate arity and dispatches to the + correct method, or throws an error. + * Add withUnivQuant to look at the list of universally quantified + variables wrapped around a formula. + + -- David Fox Fri, 03 Sep 2010 12:36:25 -0700 + +haskell-logic (0.21.2) unstable; urgency=low + + * Fix a bug in fromFirstOrder + * Add Logic.Set.cartesianProduct, use to implement allpairs + * Add purednf and implement purecnf in terms of purednf. + + -- David Fox Mon, 30 Aug 2010 15:44:10 -0700 + +haskell-logic (0.21) unstable; urgency=low + + * Rename the *Logic classes -> *Formula + * Split a NormalFormula class out of FirstOrderFormula, use it as + the result of the clauseNormalForm and implicativeNormalForm + functions. + + -- David Fox Sun, 29 Aug 2010 14:27:34 -0700 + +haskell-logic (0.20) unstable; urgency=low + + * Reduce the number of arguments to foldF to three, one for quantifiers, + one for combining formulas, one for predicates. + * Add a Predicate type for a temporary representation of a predicate and + its arguments, this is the type now passed to foldF. + + -- David Fox Mon, 23 Aug 2010 22:14:22 -0700 + +haskell-logic (0.19) unstable; urgency=low + + * Extensive work on polymorphic version of Resolution prover and test cases. + * Emergency check-in due to dying disk. + * Implement skolemization and cnf algorithms from Harrison book. + + -- David Fox Tue, 17 Aug 2010 14:55:39 -0700 + +haskell-logic (0.18) unstable; urgency=low + + * Remove the Predicate and Proposition synonyms for Formula, they + seem likely to confuse. + + -- David Fox Wed, 28 Jul 2010 09:30:41 -0700 + +haskell-logic (0.17) unstable; urgency=low + + * Make all the normal form code polymorphic. + + -- David Fox Mon, 26 Jul 2010 08:05:24 -0700 + +haskell-logic (0.16) unstable; urgency=low + + * Move important super classes from the individual functions to the type + class FirstOrderLogic: Eq p, Boolean p, Eq f, Skolem f. + * Implement a default method for .!=. + * Remove two "quick simplifications" from Logic.NormalForm.distributeDisjuncts + because they assume Eq formula, which isn't really well defined. Can these + make any difference anyway once we reach CNF? + * Rename convertPred -> convertFOF to match class name change. + + -- David Fox Sat, 10 Jul 2010 22:25:18 -0700 + +haskell-logic (0.15) unstable; urgency=low + + * Rename PredicateLogic -> FirstOrderLogic + * Add a Logic.Prover module with a function to load a knowledgebase. + + -- David Fox Thu, 08 Jul 2010 16:00:35 -0700 + +haskell-logic (0.14) unstable; urgency=low + + * Fix skolem handling. Use a Skolem class to convert between Ints + and skolem functions, and a HasSkolem class to obtain numbers for + skolem functions from a monad. + * Integrate Chiou Prover package into this one. We need to mix + pieces of the two. + + -- David Fox Thu, 08 Jul 2010 12:47:23 -0700 + +haskell-logic (0.13) unstable; urgency=low + + * Implement polymorphic version of implicativeNormalForm. + + -- David Fox Tue, 06 Jul 2010 22:39:55 -0700 + +haskell-logic (0.12) unstable; urgency=low + + * Parameterize the variable type v in the PredicateLogic class and + the Formula type in the Parameterized instance. + * Reduce the number of functional dependencies in the PredicateLogic + class, this allows us to create two instances that use the same + types for any of v, p, or f. + + -- David Fox Tue, 06 Jul 2010 17:52:37 -0700 + +haskell-logic (0.11) unstable; urgency=low + + * Modify the Skolem class so it uses a monad to generate new names + for skolem functions. This corresponds to the technique used + by what is now our only working example of a first order logic + theorem prover, the new Chiou package. + + -- David Fox Mon, 05 Jul 2010 12:46:08 -0700 + +haskell-logic (0.10) unstable; urgency=low + + * Add an instance for the Charles Chiou first order logic prover. + + -- David Fox Mon, 05 Jul 2010 09:03:04 -0700 + +haskell-logic (0.9) unstable; urgency=low + + * Add a Logic.Satisfiable module, containing functions theorem, + inconsistant, and invalid. + + -- David Fox Fri, 02 Jul 2010 11:34:38 -0700 + +haskell-logic (0.8) unstable; urgency=low + + * Modify skolemize so it leaves the universal quantifiers on its + result, and add a function removeUniversal to remove them. We + envision having a use for those quantifiers some time soon. + * Use standard names for the various normal forms, move Logic.CNF + to Logic.NormalForm. + + -- David Fox Wed, 30 Jun 2010 18:28:00 -0700 + +haskell-logic (0.7) unstable; urgency=low + + * Change the order of substitution function arguments from (new, old) + to (old, new), to match the notation generally used in textbooks. + + -- David Fox Wed, 30 Jun 2010 08:58:54 -0700 + +haskell-logic (0.6.1) unstable; urgency=low + + * Fix a bug in substituteTerm and re-implement skolemize. + + -- David Fox Wed, 30 Jun 2010 06:43:50 -0700 + +haskell-logic (0.6) unstable; urgency=low + + * Split a Logic class out of PropositionalLogic and make it the ancestor + of PropositionalLogic and PredicateLogic. This way we can eliminate + the horrible atom parameter from the PredicateLogic type. + * Add a Skolem v f class to encapsulate conversion of variables to + skolem functions. + + -- David Fox Mon, 28 Jun 2010 06:34:43 -0700 + +haskell-logic (0.5.1) unstable; urgency=low + + * Rename variables in the moveQuantifiersOut operation of cnf to + avoid collisions later. + * Add an Enum instance for the V type so we can find fresh variables, + and new functions for finding the quantified variables and all the + variables in a formula. + + -- David Fox Sun, 27 Jun 2010 07:00:49 -0700 + +haskell-logic (0.5) unstable; urgency=low + + * Export distributeDisjuncts + + -- David Fox Fri, 25 Jun 2010 14:13:44 -0700 + +haskell-logic (0.4) unstable; urgency=low + + * Add documentation + * Remove the normalize function + * Remove the AtomicWord type (use the equivalent in Logic-TPTP.) + * Make some derived methods into functions. + + -- David Fox Fri, 25 Jun 2010 09:32:22 -0700 + +haskell-logic (0.3) unstable; urgency=low + + * Eliminate the use of the unicode characters for for_all and + exists, they make the amd64 version of haddock crash. + + -- David Fox Thu, 24 Jun 2010 13:46:42 -0700 + +haskell-logic (0.2) unstable; urgency=low + + * Add an Ord instance to AtomicFormula to satisfy the requirements + of the satisfiable function in PropLogic. + + -- David Fox Thu, 24 Jun 2010 10:08:42 -0700 + +haskell-logic (0.1) unstable; urgency=low + + * Debianization generated by cabal-debian + + -- David Fox Wed, 23 Jun 2010 14:19:18 -0700 + diff --git a/logic-classes.cabal b/logic-classes.cabal --- a/logic-classes.cabal +++ b/logic-classes.cabal @@ -1,5 +1,5 @@ Name: logic-classes -Version: 1.4.7 +Version: 1.4.8 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 @@ -15,6 +15,7 @@ Category: Logic, Theorem Provers Cabal-version: >= 1.9 Build-Type: Simple +Extra-Source-Files: changelog Library GHC-options: -Wall -O2