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 Ord p => PredicateName p = Named p Int | Equals deriving (Eq, Ord, Show) +data 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/Harrison/Herbrand.hs b/Data/Logic/Harrison/Herbrand.hs --- a/Data/Logic/Harrison/Herbrand.hs +++ b/Data/Logic/Harrison/Herbrand.hs @@ -1,14 +1,16 @@ -{-# LANGUAGE RankNTypes, ScopedTypeVariables #-} +{-# LANGUAGE OverloadedStrings, RankNTypes, ScopedTypeVariables, TypeFamilies #-} module Data.Logic.Harrison.Herbrand where import Control.Applicative.Error (Failing(..)) import Data.Logic.Classes.Atom (Atom(substitute, freeVariables)) -import Data.Logic.Classes.FirstOrder (FirstOrderFormula) +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.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) +import Data.Logic.Classes.Term (Term, fApp, vt) import Data.Logic.Harrison.DP (dpll) import Data.Logic.Harrison.FOL (generalize) import Data.Logic.Harrison.Lib (distrib', allpairs) @@ -18,6 +20,7 @@ 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. @@ -133,7 +136,8 @@ Term term v f, Atom atom term v, IsString f, - Ord pf) => + Ord pf, + pf ~ fof) => (atom -> Set.Set (f, Int)) -> fof -> Failing Int gilmore fa fm = let sfm = runSkolem (skolemize id ((.~.)(generalize fm))) :: pf in @@ -145,12 +149,8 @@ -- ------------------------------------------------------------------------- -- 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/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 (Negatable lit, Ord lit) => ImplicativeForm lit = +data 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/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 +Version: 1.4.1 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 @@ -12,7 +12,7 @@ Maintainer: SeeReason Partners Bug-Reports: http://bugzilla.seereason.com/ Category: Logic, Theorem Provers -Cabal-version: >= 1.6 +Cabal-version: >= 1.9 Build-Type: Simple Library @@ -69,13 +69,14 @@ 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, incremental-sat-solver, + Build-Depends: applicative-extras, base >= 4.3 && < 5, containers, fgl, happstack-data, 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: HUnit + Build-Depends: applicative-extras, base, containers, happstack-data, HUnit, incremental-sat-solver, mtl, + pretty, PropLogic, safecopy, set-extra, syb, template-haskell Other-Modules: Data.Logic.Tests.Chiou0 Data.Logic.Tests.Common Data.Logic.Tests.Data