diff --git a/COPYING b/COPYING new file mode 100644 --- /dev/null +++ b/COPYING @@ -0,0 +1,34 @@ +This package was cabalized by David Fox + on June 18, 2010. + +Copyright (c) 2010, 2011, 2012, David Fox + +All rights reserved. + +Redistribution and use in source and binary forms, with or without +modification, are permitted provided that the following conditions are +met: + + * Redistributions of source code must retain the above copyright + notice, this list of conditions and the following disclaimer. + + * Redistributions in binary form must reproduce the above + copyright notice, this list of conditions and the following + disclaimer in the documentation and/or other materials provided + with the distribution. + + * The names of contributors may not be used to endorse or promote + products derived from this software without specific prior + written permission. + +THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS +"AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT +LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR +A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT +OWNER OR CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, +SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT +LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE, +DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY +THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT +(INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE +OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE. diff --git a/Data/Logic/Classes/Equals.hs b/Data/Logic/Classes/Equals.hs --- a/Data/Logic/Classes/Equals.hs +++ b/Data/Logic/Classes/Equals.hs @@ -49,7 +49,7 @@ -- | A way to represent any predicate's name. Frequently the equality -- predicate has no standalone representation in the p type, it is -- just a constructor in the atom type, or even the formula type. -data PredicateName p = Named p Int | Equals deriving (Eq, Ord, Show) +data Ord p => PredicateName p = Named p Int | Equals deriving (Eq, Ord, Show) instance (Pretty p, Ord p) => Pretty (PredicateName p) where pretty Equals = text "=" 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 @@ -44,7 +44,6 @@ import Data.Logic.Classes.Variable (Variable) import Data.SafeCopy (base, deriveSafeCopy) import qualified Data.Set as Set -import Happstack.Data (deriveNewData) import Text.PrettyPrint (Doc, (<>), (<+>), text, parens, nest) -- |The 'FirstOrderFormula' type class. Minimal implementation: @@ -302,6 +301,3 @@ atom_union f fm = overatoms (\ h t -> Set.union (f h) t) fm Set.empty $(deriveSafeCopy 1 'base ''Quant) - -$(deriveNewData [''Quant]) - diff --git a/Data/Logic/Classes/Propositional.hs b/Data/Logic/Classes/Propositional.hs --- a/Data/Logic/Classes/Propositional.hs +++ b/Data/Logic/Classes/Propositional.hs @@ -35,7 +35,6 @@ import Data.Logic.Classes.Pretty (Pretty, HasFixity(fixity), Fixity(Fixity), FixityDirection(..)) import Data.SafeCopy (base, deriveSafeCopy) import qualified Data.Set.Extra as Set -import Happstack.Data (deriveNewData) import Text.PrettyPrint (Doc, text, (<>)) -- |A type class for propositional logic. If the type we are writing @@ -332,5 +331,3 @@ $(deriveSafeCopy 1 'base ''BinOp) $(deriveSafeCopy 1 'base ''Combination) - -$(deriveNewData [''BinOp, ''Combination]) diff --git a/Data/Logic/Harrison/Herbrand.hs b/Data/Logic/Harrison/Herbrand.hs --- a/Data/Logic/Harrison/Herbrand.hs +++ b/Data/Logic/Harrison/Herbrand.hs @@ -1,16 +1,14 @@ -{-# LANGUAGE OverloadedStrings, RankNTypes, ScopedTypeVariables, TypeFamilies #-} +{-# LANGUAGE RankNTypes, ScopedTypeVariables #-} module Data.Logic.Harrison.Herbrand where import Control.Applicative.Error (Failing(..)) import Data.Logic.Classes.Atom (Atom(substitute, freeVariables)) -import Data.Logic.Classes.Combine ((.=>.)) -import Data.Logic.Classes.Equals (pApp, funcsAtomEq) -import Data.Logic.Classes.FirstOrder (FirstOrderFormula(exists, for_all)) +import Data.Logic.Classes.FirstOrder (FirstOrderFormula) import Data.Logic.Classes.Formula (Formula(..)) import Data.Logic.Classes.Literal (Literal) import Data.Logic.Classes.Negate ((.~.)) import Data.Logic.Classes.Propositional (PropositionalFormula) -import Data.Logic.Classes.Term (Term, fApp, vt) +import Data.Logic.Classes.Term (Term, fApp) import Data.Logic.Harrison.DP (dpll) import Data.Logic.Harrison.FOL (generalize) import Data.Logic.Harrison.Lib (distrib', allpairs) @@ -20,7 +18,6 @@ import qualified Data.Map as Map import qualified Data.Set as Set import Data.String (IsString(..)) -import Test.HUnit (Test(..), assertEqual) -- ========================================================================= -- Relation between FOL and propositonal logic; Herbrand theorem. @@ -136,8 +133,7 @@ Term term v f, Atom atom term v, IsString f, - Ord pf, - pf ~ fof) => + Ord pf) => (atom -> Set.Set (f, Int)) -> fof -> Failing Int gilmore fa fm = let sfm = runSkolem (skolemize id ((.~.)(generalize fm))) :: pf in @@ -149,8 +145,12 @@ -- ------------------------------------------------------------------------- -- First example and a little tracing. -- ------------------------------------------------------------------------- - {- +test01 = + let fm = exists "x" (for_all "y" (pApp "p" [vt "x"] .=>. pApp "p" [vt "y"])) + sfm = skolemize ((.~.) fm) in + TestList [TestCase (assertEqual "gilmore 1" 2 (gilmore fm))] + START_INTERACTIVE;; gilmore < P(y)>>;; diff --git a/Data/Logic/KnowledgeBase.hs b/Data/Logic/KnowledgeBase.hs --- a/Data/Logic/KnowledgeBase.hs +++ b/Data/Logic/KnowledgeBase.hs @@ -40,7 +40,6 @@ import Data.Logic.Resolution (prove, SetOfSupport, getSetOfSupport) import Data.SafeCopy (deriveSafeCopy, base) import qualified Data.Set.Extra as S -import Happstack.Data (Default(defaultValue), deriveNewDataNoDefault) import Prelude hiding (negate) type SentenceCount = Int @@ -104,11 +103,6 @@ deriving (Data, Typeable, Eq, Ord, Show) $(deriveSafeCopy 1 'base ''ProofResult) - -$(deriveNewDataNoDefault [''ProofResult]) - -instance Default ProofResult where - defaultValue = Invalid data Proof lit = Proof {proofResult :: ProofResult, proof :: S.Set (ImplicativeForm lit)} deriving (Data, Typeable, Eq, Ord) diff --git a/Data/Logic/Normal/Implicative.hs b/Data/Logic/Normal/Implicative.hs --- a/Data/Logic/Normal/Implicative.hs +++ b/Data/Logic/Normal/Implicative.hs @@ -52,7 +52,7 @@ -- formula has the form @a & b & c .=>. d | e | f@, where a thru f are -- literals. One more restriction that is not implied by the type is -- that no literal can appear in both the pos set and the neg set. -data ImplicativeForm lit = +data (Negatable lit, Ord lit) => ImplicativeForm lit = INF {neg :: Set.Set lit, pos :: Set.Set lit} deriving (Eq, Ord, Data, Typeable, Show) 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 (formula ~ TFormula, atom ~ TAtom, v ~ V) => 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 (FirstOrderFormula formula atom v, formula ~ TFormula, atom ~ TAtom, v ~ V) => Expected formula atom v = FirstOrderFormula formula | SimplifiedForm formula | NegationNormalForm formula diff --git a/Data/Logic/Tests/Harrison/Common.hs b/Data/Logic/Tests/Harrison/Common.hs --- a/Data/Logic/Tests/Harrison/Common.hs +++ b/Data/Logic/Tests/Harrison/Common.hs @@ -4,7 +4,7 @@ import Data.Logic.Types.Harrison.Equal (FOLEQ(..)) import Data.Logic.Types.Harrison.Formulas.FirstOrder (Formula(..)) --- deriving instance Show FOLEQ --- deriving instance Show (Formula FOLEQ) +deriving instance Show FOLEQ +deriving instance Show (Formula FOLEQ) diff --git a/Data/Logic/Types/FirstOrder.hs b/Data/Logic/Types/FirstOrder.hs --- a/Data/Logic/Types/FirstOrder.hs +++ b/Data/Logic/Types/FirstOrder.hs @@ -29,7 +29,6 @@ import Data.Logic.Resolution (isRenameOfAtomEq, getSubstAtomEq) import Data.SafeCopy (SafeCopy, base, deriveSafeCopy, extension, MigrateFrom(..)) import Data.Typeable (Typeable) -import Happstack.Data (deriveNewData) -- | The range of a formula is {True, False} when it has no free variables. data Formula v p f @@ -201,8 +200,6 @@ $(deriveSafeCopy 1 'base ''PTerm) $(deriveSafeCopy 1 'base ''Formula) $(deriveSafeCopy 2 'extension ''Predicate) - -$(deriveNewData [''PTerm, ''Formula, ''Predicate]) -- Migration -- diff --git a/Data/Logic/Types/FirstOrderPublic.hs b/Data/Logic/Types/FirstOrderPublic.hs --- a/Data/Logic/Types/FirstOrderPublic.hs +++ b/Data/Logic/Types/FirstOrderPublic.hs @@ -27,7 +27,6 @@ import Data.SafeCopy (base, deriveSafeCopy) import Data.Set (Set) import Data.Typeable (Typeable) -import Happstack.Data (deriveNewData) -- |Convert between the public and internal representations. class Bijection p i where @@ -115,5 +114,3 @@ pretty formula = prettyFirstOrder (\ _prec a -> pretty a) pretty 0 formula $(deriveSafeCopy 1 'base ''Formula) - -$(deriveNewData [''Formula]) 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.1 +Version: 1.4.2 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 @@ -8,6 +8,7 @@ resolution-based theorem prover for any instance of FirstOrderFormula. Homepage: http://src.seereason.com/logic-classes License: BSD3 +License-File: COPYING Author: David Fox Maintainer: SeeReason Partners Bug-Reports: http://bugzilla.seereason.com/ @@ -69,13 +70,13 @@ Data.Logic.Types.Harrison.Formulas.Propositional Data.Logic.Types.Harrison.Prop Data.Logic.Types.Propositional - Build-Depends: applicative-extras, base >= 4.3 && < 5, containers, fgl, happstack-data, HUnit, incremental-sat-solver, + Build-Depends: applicative-extras, base >= 4.3 && < 5, containers, fgl, HUnit, incremental-sat-solver, mtl, syb-with-class, text, PropLogic, pretty, safecopy, set-extra, syb, template-haskell Executable tests GHC-Options: -Wall -O2 Main-Is: Data/Logic/Tests/Main.hs - Build-Depends: applicative-extras, base, containers, happstack-data, HUnit, incremental-sat-solver, mtl, + Build-Depends: applicative-extras, base, containers, HUnit, incremental-sat-solver, mtl, pretty, PropLogic, safecopy, set-extra, syb, template-haskell Other-Modules: Data.Logic.Tests.Chiou0 Data.Logic.Tests.Common