packages feed

logic-classes 1.4.8 → 1.5

raw patch · 14 files changed

+61/−369 lines, 14 files

Files

Data/Logic/Classes/Apply.hs view
@@ -1,4 +1,5 @@-{-# LANGUAGE FlexibleContexts, FlexibleInstances, FunctionalDependencies, MultiParamTypeClasses, TypeFamilies, UndecidableInstances #-}+{-# LANGUAGE FlexibleContexts, FlexibleInstances, FunctionalDependencies, MultiParamTypeClasses,+             RankNTypes, ScopedTypeVariables, TypeFamilies, UndecidableInstances #-} {-# OPTIONS -fno-warn-missing-signatures #-} -- | The Apply class represents a type of atom the only supports predicate application. module Data.Logic.Classes.Apply@@ -11,11 +12,13 @@     , prettyApply     , varApply     , substApply+    , pApp, pApp0, pApp1, pApp2, pApp3, pApp4, pApp5, pApp6, pApp7     ) where  import Data.Data (Data) import Data.Logic.Classes.Arity import Data.Logic.Classes.Constants+import Data.Logic.Classes.Formula (Formula(atomic)) import Data.Logic.Classes.Pretty (Pretty) import Data.Logic.Classes.Term (Term, showTerm, prettyTerm, fvt, tsubst) import Data.List (intercalate, intersperse)@@ -62,7 +65,7 @@               (\ x -> if x then "true" else "false")  prettyApply :: (Apply atom p term, Term term v f) => (v -> Doc) -> (p -> Doc) -> (f -> Doc) -> Int -> atom -> Doc-prettyApply pv pp pf prec atom =+prettyApply pv pp pf _prec atom =     foldApply (\ p ts ->                    pp p <> case ts of                              [] -> empty@@ -83,3 +86,24 @@     freeVariables = varApply     substitute = substApply -}++pApp :: forall formula atom term p. (Formula formula atom, Apply atom p term) => p -> [term] -> formula+pApp p ts = atomic (apply p ts :: atom)++-- | Versions of pApp specialized for different argument counts.+pApp0 :: forall formula atom term p. (Formula formula atom, Apply atom p term) => p -> formula+pApp0 p = atomic (apply0 p :: atom)+pApp1 :: forall formula atom term p. (Formula formula atom, Apply atom p term) => p -> term -> formula+pApp1 p a = atomic (apply1 p a :: atom)+pApp2 :: forall formula atom term p. (Formula formula atom, Apply atom p term) => p -> term -> term -> formula+pApp2 p a b = atomic (apply2 p a b :: atom)+pApp3 :: forall formula atom term p. (Formula formula atom, Apply atom p term) => p -> term -> term -> term -> formula+pApp3 p a b c = atomic (apply3 p a b c :: atom)+pApp4 :: forall formula atom term p. (Formula formula atom, Apply atom p term) => p -> term -> term -> term -> term -> formula+pApp4 p a b c d = atomic (apply4 p a b c d :: atom)+pApp5 :: forall formula atom term p. (Formula formula atom, Apply atom p term) => p -> term -> term -> term -> term -> term -> formula+pApp5 p a b c d e = atomic (apply5 p a b c d e :: atom)+pApp6 :: forall formula atom term p. (Formula formula atom, Apply atom p term) => p -> term -> term -> term -> term -> term -> term -> formula+pApp6 p a b c d e f = atomic (apply6 p a b c d e f :: atom)+pApp7 :: forall formula atom term p. (Formula formula atom, Apply atom p term) => p -> term -> term -> term -> term -> term -> term -> term -> formula+pApp7 p a b c d e f g = atomic (apply7 p a b c d e f g :: atom)
Data/Logic/Classes/Equals.hs view
@@ -34,7 +34,7 @@ import Text.PrettyPrint (Doc, (<>), (<+>), text, empty, parens, hcat, nest)  -- | Its not safe to make Atom a superclass of AtomEq, because the Atom methods will fail on AtomEq instances.-class Predicate p => AtomEq atom p term | atom -> p term, term -> atom p where+class Predicate p => AtomEq atom p term | atom -> term, atom -> p where     foldAtomEq :: (p -> [term] -> r) -> (Bool -> r) -> (term -> term -> r) -> atom -> r     equals :: term -> term -> atom     applyEq' :: p -> [term] -> atom@@ -110,7 +110,7 @@ pApp7 :: (FirstOrderFormula formula atom v, AtomEq atom p term) => p -> term -> term -> term -> term -> term -> term -> term -> formula pApp7 p a b c d e f g = atomic (apply7 p a b c d e f g) -showFirstOrderFormulaEq :: (FirstOrderFormula fof atom v, AtomEq atom p term, Show term, Show v, Show p) => fof -> String+showFirstOrderFormulaEq :: forall fof atom v p term. (FirstOrderFormula fof atom v, AtomEq atom p term, Show term, Show v, Show p) => fof -> String showFirstOrderFormulaEq fm =     fst (sfo fm)     where
Data/Logic/Classes/FirstOrder.hs view
@@ -4,15 +4,6 @@     ( FirstOrderFormula(..)     , Quant(..)     , zipFirstOrder-    , pApp-    , pApp0-    , pApp1-    , pApp2-    , pApp3-    , pApp4-    , pApp5-    , pApp6-    , pApp7     , for_all'     , exists'     , quant@@ -37,7 +28,6 @@     ) where  import Data.Generics (Data, Typeable)-import Data.Logic.Classes.Apply (Apply(..), apply, apply0, apply1, apply2, apply3, apply4, apply5, apply6, apply7) import Data.Logic.Classes.Constants import Data.Logic.Classes.Combine import Data.Logic.Classes.Formula (Formula(atomic))@@ -101,27 +91,6 @@ -- class, but it would add additional complexity with unclear -- benefits. data Quant = Forall | Exists deriving (Eq,Ord,Show,Read,Data,Typeable,Enum,Bounded)--pApp :: forall formula atom term v p. (FirstOrderFormula formula atom v, Apply atom p term) => p -> [term] -> formula-pApp p ts = atomic (apply p ts :: atom)---- | Versions of pApp specialized for different argument counts.-pApp0 :: forall formula atom term v p. (FirstOrderFormula formula atom v, Apply atom p term) => p -> formula-pApp0 p = atomic (apply0 p :: atom)-pApp1 :: forall formula atom term v p. (FirstOrderFormula formula atom v, Apply atom p term) => p -> term -> formula-pApp1 p a = atomic (apply1 p a :: atom)-pApp2 :: forall formula atom term v p. (FirstOrderFormula formula atom v, Apply atom p term) => p -> term -> term -> formula-pApp2 p a b = atomic (apply2 p a b :: atom)-pApp3 :: forall formula atom term v p. (FirstOrderFormula formula atom v, Apply atom p term) => p -> term -> term -> term -> formula-pApp3 p a b c = atomic (apply3 p a b c :: atom)-pApp4 :: forall formula atom term v p. (FirstOrderFormula formula atom v, Apply atom p term) => p -> term -> term -> term -> term -> formula-pApp4 p a b c d = atomic (apply4 p a b c d :: atom)-pApp5 :: forall formula atom term v p. (FirstOrderFormula formula atom v, Apply atom p term) => p -> term -> term -> term -> term -> term -> formula-pApp5 p a b c d e = atomic (apply5 p a b c d e :: atom)-pApp6 :: forall formula atom term v p. (FirstOrderFormula formula atom v, Apply atom p term) => p -> term -> term -> term -> term -> term -> term -> formula-pApp6 p a b c d e f = atomic (apply6 p a b c d e f :: atom)-pApp7 :: forall formula atom term v p. (FirstOrderFormula formula atom v, Apply atom p term) => p -> term -> term -> term -> term -> term -> term -> term -> formula-pApp7 p a b c d e f g = atomic (apply7 p a b c d e f g :: atom)  -- |for_all with a list of variables, for backwards compatibility. for_all' :: FirstOrderFormula formula atom v => [v] -> formula -> formula
Data/Logic/Classes/Formula.hs view
@@ -1,9 +1,9 @@-{-# LANGUAGE MultiParamTypeClasses #-}+{-# LANGUAGE FunctionalDependencies, MultiParamTypeClasses #-} module Data.Logic.Classes.Formula     ( Formula(atomic, foldAtoms, mapAtoms)     ) where -class Formula formula atom where+class Formula formula atom | formula -> atom where     atomic :: atom -> formula     foldAtoms :: Formula formula atom => (r -> atom -> r) -> r -> formula -> r     mapAtoms :: Formula formula atom => (atom -> formula) -> formula -> formula
Data/Logic/Classes/Literal.hs view
@@ -8,13 +8,11 @@     , foldAtomsLiteral     ) where -import Data.Logic.Classes.Combine (Combination(..)) import Data.Logic.Classes.Constants import Data.Logic.Classes.Formula (Formula(atomic)) import Data.Logic.Classes.Pretty (HasFixity(..), Fixity(..), FixityDirection(..)) import qualified Data.Logic.Classes.Propositional as P import Data.Logic.Classes.Negate-import Data.Logic.Failing (Failing(..)) import Text.PrettyPrint (Doc, (<>), text, parens, nest)  -- |Literals are the building blocks of the clause and implicative normal
Data/Logic/Harrison/DefCNF.hs view
@@ -89,8 +89,8 @@   let (deflist {- :: [pf]-}) = Map.elems defs in   Set.unions (simpcnf fm'' : map simpcnf deflist) -defcnf1 :: forall pf lit atom. (PropositionalFormula pf atom, Literal lit atom, NumAtom atom, Ord lit) => pf -> pf-defcnf1 fm = cnf (mk_defcnf maincnf fm :: Set.Set (Set.Set lit))+defcnf1 :: forall pf lit atom. (PropositionalFormula pf atom, Literal lit atom, NumAtom atom, Ord lit) => lit -> atom -> pf -> pf+defcnf1 _ _ fm = cnf (mk_defcnf maincnf fm :: Set.Set (Set.Set lit))   -- ------------------------------------------------------------------------- @@ -134,8 +134,8 @@ defcnfs :: (PropositionalFormula pf atom, Literal lit atom, NumAtom atom, Ord lit) => pf -> Set.Set (Set.Set lit) defcnfs fm = mk_defcnf andcnf fm -defcnf2 :: forall pf lit atom.(PropositionalFormula pf atom, Literal lit atom, NumAtom atom, Ord lit) => pf -> pf-defcnf2 fm = cnf (defcnfs fm :: Set.Set (Set.Set lit))+defcnf2 :: forall pf lit atom.(PropositionalFormula pf atom, Literal lit atom, NumAtom atom, Ord lit) => lit -> atom -> pf -> pf+defcnf2 _ _ fm = cnf (defcnfs fm :: Set.Set (Set.Set lit))  -- -------------------------------------------------------------------------  -- Examples.                                                                 @@ -156,5 +156,5 @@       co (BinOp p (:&:) q) = subcnf andcnf3 (.&.) p q trip       co _ = maincnf trip -defcnf3 :: forall pf lit atom. (PropositionalFormula pf atom, Literal lit atom, NumAtom atom, Ord lit) => pf -> pf-defcnf3 fm = cnf (mk_defcnf andcnf3 fm :: Set.Set (Set.Set lit))+defcnf3 :: forall pf lit atom. (PropositionalFormula pf atom, Literal lit atom, NumAtom atom, Ord lit) => lit -> atom -> pf -> pf+defcnf3 _ _ fm = cnf (mk_defcnf andcnf3 fm :: Set.Set (Set.Set lit))
Data/Logic/Harrison/Herbrand.hs view
@@ -134,8 +134,8 @@             Atom atom term v,             IsString f,             Ord pf) =>-           (atom -> Set.Set (f, Int)) -> fof -> Failing Int-gilmore fa fm =+           pf -> (atom -> Set.Set (f, Int)) -> fof -> Failing Int+gilmore _ fa fm =   let sfm = runSkolem (skolemize id ((.~.)(generalize fm))) :: pf in   let fvs = Set.toList (foldAtoms (\ s (a :: atom) -> Set.union s (freeVariables a)) Set.empty sfm)       (consts,funcs) = herbfuns fa sfm in@@ -224,8 +224,8 @@                 Atom atom term v,                 IsString f,                 Ord lit) =>-               (atom -> Set.Set (f, Int)) -> fof -> Failing Int-davisputnam fa fm =+               lit -> (atom -> Set.Set (f, Int)) -> fof -> Failing Int+davisputnam _ fa fm =   let (sfm :: lit) = runSkolem (skolemize id ((.~.)(generalize fm))) in   let fvs = Set.toList (foldAtoms (\ s (a :: atom) -> Set.union (freeVariables a) s) Set.empty sfm)       (consts,funcs) = herbfuns fa sfm in@@ -284,8 +284,8 @@                  Term term v f,                  Atom atom term v,                  IsString f) =>-                (atom -> Set.Set (f, Int)) -> fof -> Failing Int-davisputnam' fa fm =+                lit -> pf -> (atom -> Set.Set (f, Int)) -> fof -> Failing Int+davisputnam' _ _ fa fm =     let (sfm :: pf) = runSkolem (skolemize id ((.~.)(generalize fm))) in     let fvs = Set.toList (foldAtoms (\ s (a :: atom) -> Set.union (freeVariables a) s) Set.empty sfm)         (consts,funcs) = herbfuns fa sfm in
Data/Logic/Harrison/Tableaux.hs view
@@ -1,4 +1,4 @@-{-# LANGUAGE NoMonomorphismRestriction, OverloadedStrings, RankNTypes, ScopedTypeVariables #-}+{-# LANGUAGE CPP, NoMonomorphismRestriction, OverloadedStrings, RankNTypes, ScopedTypeVariables #-} {-# OPTIONS_GHC -Wall #-} module Data.Logic.Harrison.Tableaux     ( unify_literals@@ -112,6 +112,7 @@       substitute' = C.substitute  -- prawitz :: forall fof atom v. (FirstOrderFormula fof atom v, Ord fof) => fof -> Int+#if 0 prawitz :: forall fof atom term v f lit pf.            (FirstOrderFormula fof atom v,             PropositionalFormula pf atom,@@ -126,6 +127,7 @@       dnf = simpdnf pf :: Set.Set (Set.Set lit)       fvs = foldAtoms (\ s (a :: atom) -> Set.union (C.freeVariables a) s) Set.empty pf :: Set.Set v       pf = runSkolem (skolemize id ((.~.)(generalize fm))) :: pf+#endif  -- -------------------------------------------------------------------------  -- Examples.
− Data/Logic/Instances/Chiou.hs 
@@ -1,307 +0,0 @@-{-# LANGUAGE DeriveDataTypeable, FlexibleContexts, FlexibleInstances, MultiParamTypeClasses,-             RankNTypes, TypeSynonymInstances, UndecidableInstances #-}-{-# OPTIONS -Wall -Wwarn -fno-warn-orphans -fno-warn-missing-signatures #-}-module Data.Logic.Instances.Chiou-    ( Sentence(..)-    , CTerm(..)-    , Connective(..)-    , Quantifier(..)-    , ConjunctiveNormalForm(..)-    , NormalSentence(..)-    , NormalTerm(..)-    , toSentence-    , fromSentence-    ) where--import Data.Generics (Data, Typeable)-import Data.Logic.Classes.Apply (Apply(..), Predicate)-import Data.Logic.Classes.Atom (Atom)-import Data.Logic.Classes.Combine (Combinable(..), BinOp(..), Combination(..))-import Data.Logic.Classes.Constants (Constants(..), asBool, true, false)-import Data.Logic.Classes.Equals (AtomEq(..), (.=.))-import Data.Logic.Classes.FirstOrder (FirstOrderFormula(..), Quant(..), quant', pApp, prettyFirstOrder, fixityFirstOrder, foldAtomsFirstOrder, mapAtomsFirstOrder)-import Data.Logic.Classes.Formula (Formula(..))-import Data.Logic.Classes.Negate (Negatable(..), (.~.))-import Data.Logic.Classes.Pretty (Pretty(pretty), HasFixity(..))-import Data.Logic.Classes.Term (Term(..), Function)-import Data.Logic.Classes.Variable (Variable)-import qualified Data.Logic.Classes.FirstOrder as L-import Data.Logic.Classes.Propositional (PropositionalFormula(..))-import Data.Logic.Classes.Skolem (Skolem(..))-import Data.String (IsString(..))--data Sentence v p f-    = Connective (Sentence v p f) Connective (Sentence v p f)-    | Quantifier Quantifier [v] (Sentence v p f)-    | Not (Sentence v p f)-    | Predicate p [CTerm v f]-    | Equal (CTerm v f) (CTerm v f)-    deriving (Eq, Ord, Data, Typeable)--data CTerm v f-    = Function f [CTerm v f]-    | Variable v-    deriving (Eq, Ord, Data, Typeable)--data Connective-    = Imply-    | Equiv-    | And-    | Or-    deriving (Eq, Ord, Show, Data, Typeable)--data Quantifier-    = ForAll-    | ExistsCh-    deriving (Eq, Ord, Show, Data, Typeable)--instance Negatable (Sentence v p f) where-    negatePrivate = Not-    foldNegation normal inverted (Not x) = foldNegation inverted normal x-    foldNegation normal _ x = normal x--instance (Constants p, Eq (Sentence v p f)) => Constants (Sentence v p f) where-    fromBool x = Predicate (fromBool x) []-    asBool x-        | fromBool True == x = Just True-        | fromBool False == x = Just False-        | True = Nothing--instance ({- Constants (Sentence v p f), -} Ord v, Ord p, Ord f) => Combinable (Sentence v p f) where-    x .<=>. y = Connective x Equiv y-    x .=>.  y = Connective x Imply y-    x .|.   y = Connective x Or y-    x .&.   y = Connective x And y--instance (Predicate p, Function f v) => Formula (Sentence v p f) (Sentence v p f) where-    atomic (Connective _ _ _) = error "Logic.Instances.Chiou.atomic: unexpected"-    atomic (Quantifier _ _ _) = error "Logic.Instances.Chiou.atomic: unexpected"-    atomic (Not _) = error "Logic.Instances.Chiou.atomic: unexpected"-    atomic x@(Predicate _ _) = x-    atomic x@(Equal _ _) = x-    foldAtoms = foldAtomsFirstOrder-    mapAtoms = mapAtomsFirstOrder--instance (Formula (Sentence v p f) (Sentence v p f), Variable v, Predicate p, Function f v, Combinable (Sentence v p f)) =>-         PropositionalFormula (Sentence v p f) (Sentence v p f) where-    foldPropositional co tf at formula =-        case formula of-          Not x -> co ((:~:) x)-          Quantifier _ _ _ -> error "Logic.Instance.Chiou.foldF0: unexpected"-          Connective f1 Imply f2 -> co (BinOp f1 (:=>:) f2)-          Connective f1 Equiv f2 -> co (BinOp f1 (:<=>:) f2)-          Connective f1 And f2 -> co (BinOp f1 (:&:) f2)-          Connective f1 Or f2 -> co (BinOp f1 (:|:) f2)-          Predicate p ts -> maybe (at (Predicate p ts)) tf (asBool p)-          Equal t1 t2 -> at (Equal t1 t2)--data AtomicFunction v-    = AtomicFunction String-    -- This is redundant with the SkolemFunction and SkolemConstant-    -- constructors in the Chiou Term type.-    | AtomicSkolemFunction v-    deriving (Eq, Show)--instance IsString (AtomicFunction v) where-    fromString = AtomicFunction--instance Variable v => Skolem (AtomicFunction v) v where-    toSkolem = AtomicSkolemFunction-    isSkolem (AtomicSkolemFunction _) = True-    isSkolem _ = False---- The Atom type is not cleanly distinguished from the Sentence type, so we need an Atom instance for Sentence.-instance (Variable v, Predicate p, Function f v) => Apply (Sentence v p f) p (CTerm v f) where-    foldApply ap tf (Predicate p ts) = maybe (ap p ts) tf (asBool p)-    foldApply _ _ _ = error "Data.Logic.Instances.Chiou: Invalid atom"-    apply' = Predicate--instance Predicate p => AtomEq (Sentence v p f) p (CTerm v f) where-    foldAtomEq ap tf _ (Predicate p ts) = if p == true then tf True else if p == false then tf False else ap p ts-    foldAtomEq _ _ eq (Equal t1 t2) = eq t1 t2-    foldAtomEq _ _ _ _ = error "Data.Logic.Instances.Chiou: Invalid atom"-    equals = Equal-    applyEq' = Predicate--instance (FirstOrderFormula (Sentence v p f) (Sentence v p f) v, Variable v, Predicate p, Function f v) => Pretty (Sentence v p f) where-    pretty = prettyFirstOrder (\ _ a -> pretty a) pretty 0--instance (Formula (Sentence v p f) (Sentence v p f), Predicate p, Function f v, Variable v) => HasFixity (Sentence v p f) where-    fixity = fixityFirstOrder--instance (Formula (Sentence v p f) (Sentence v p f),-          Variable v, Predicate p, Function f v) =>-          FirstOrderFormula (Sentence v p f) (Sentence v p f) v where-    for_all v x = Quantifier ForAll [v] x-    exists v x = Quantifier ExistsCh [v] x-    foldFirstOrder qu co tf at f =-        case f of-          Not x -> co ((:~:) x)-          Quantifier op (v:vs) f' ->-              let op' = case op of-                          ForAll -> Forall-                          ExistsCh -> Exists in-              -- Use Logic.quant' here instead of the constructor-              -- Quantifier so as not to create quantifications with-              -- empty variable lists.-              qu op' v (quant' op' vs f')-          Quantifier _ [] f' -> foldFirstOrder qu co tf at f'-          Connective f1 Imply f2 -> co (BinOp f1 (:=>:) f2)-          Connective f1 Equiv f2 -> co (BinOp f1 (:<=>:) f2)-          Connective f1 And f2 -> co (BinOp f1 (:&:) f2)-          Connective f1 Or f2 -> co (BinOp f1 (:|:) f2)-          Predicate _ _ -> at f-          Equal _ _ -> at f-{--    zipFirstOrder qu co tf at f1 f2 =-        case (f1, f2) of-          (Not f1', Not f2') -> co ((:~:) f1') ((:~:) f2')-          (Quantifier op1 (v1:vs1) f1', Quantifier op2 (v2:vs2) f2') ->-              if op1 == op2-              then let op' = case op1 of-                               ForAll -> Forall-                               ExistsCh -> Exists in-                   qu op' v1 (Quantifier op1 vs1 f1') Forall v2 (Quantifier op2 vs2 f2')-              else Nothing-          (Quantifier q1 [] f1', Quantifier q2 [] f2') ->-              if q1 == q2 then zipFirstOrder qu co tf at f1' f2' else Nothing-          (Connective l1 op1 r1, Connective l2 op2 r2) ->-              case (op1, op2) of-                (And, And) -> co (BinOp l1 (:&:) r1) (BinOp l2 (:&:) r2)-                (Or, Or) -> co (BinOp l1 (:|:) r1) (BinOp l2 (:|:) r2)-                (Imply, Imply) -> co (BinOp l1 (:=>:) r1) (BinOp l2 (:=>:) r2)-                (Equiv, Equiv) -> co (BinOp l1 (:<=>:) r1) (BinOp l2 (:<=>:) r2)-                _ -> Nothing-          (Equal _ _, Equal _ _) -> at f1 f2-          (Predicate _ _, Predicate _ _) -> at f1 f2-          _ -> Nothing--}--instance (Variable v, Function f v) => Term (CTerm v f) v f where-    foldTerm v fn t =-        case t of-          Variable x -> v x-          Function f ts -> fn f ts-    zipTerms  v f t1 t2 =-        case (t1, t2) of-          (Variable v1, Variable v2) -> v v1 v2-          (Function f1 ts1, Function f2 ts2) -> f f1 ts1 f2 ts2-          _ -> Nothing-    vt = Variable-    fApp f ts = Function f ts--data ConjunctiveNormalForm v p f =-    CNF [Sentence v p f]-    deriving (Eq)--data NormalSentence v p f-    = NFNot (NormalSentence v p f)-    | NFPredicate p [NormalTerm v f]-    | NFEqual (NormalTerm v f) (NormalTerm v f)-    deriving (Eq, Ord, Data, Typeable)---- We need a distinct type here because of the functional dependencies--- in class FirstOrderFormula.-data NormalTerm v f-    = NormalFunction f [NormalTerm v f]-    | NormalVariable v-    deriving (Eq, Ord, Data, Typeable)--instance (Constants p, Eq (NormalSentence v p f)) => Constants (NormalSentence v p f) where-    fromBool x = NFPredicate (fromBool x) []-    asBool x-        | fromBool True == x = Just True-        | fromBool False == x = Just False-        | True = Nothing--instance Negatable (NormalSentence v p f) where-    negatePrivate = NFNot-    foldNegation normal inverted (NFNot x) = foldNegation inverted normal x-    foldNegation normal _ x = normal x--{--instance (Arity p, Constants p, Combinable (NormalSentence v p f)) => Pred p (NormalTerm v f) (NormalSentence v p f) where-    pApp0 x = NFPredicate x []-    pApp1 x a = NFPredicate x [a]-    pApp2 x a b = NFPredicate x [a,b]-    pApp3 x a b c = NFPredicate x [a,b,c]-    pApp4 x a b c d = NFPredicate x [a,b,c,d]-    pApp5 x a b c d e = NFPredicate x [a,b,c,d,e]-    pApp6 x a b c d e f = NFPredicate x [a,b,c,d,e,f]-    pApp7 x a b c d e f g = NFPredicate x [a,b,c,d,e,f,g]-    x .=. y = NFEqual x y-    x .!=. y = NFNot (NFEqual x y)--}--instance (Formula (NormalSentence v p f) (NormalSentence v p f),-          Variable v, Predicate p, Function f v, Combinable (NormalSentence v p f)) => Pretty (NormalSentence v p f) where-    pretty = prettyFirstOrder (\ _ a -> pretty a) pretty 0--instance (Predicate p, Function f v, Combinable (NormalSentence v p f)) => Formula (NormalSentence v p f) (NormalSentence v p f) where-    atomic x@(NFPredicate _ _) = x-    atomic x@(NFEqual _ _) = x-    atomic _ = error "Chiou: atomic"-    foldAtoms = foldAtomsFirstOrder-    mapAtoms = mapAtomsFirstOrder--instance (Formula (NormalSentence v p f) (NormalSentence v p f), Combinable (NormalSentence v p f), Term (NormalTerm v f) v f,-          Variable v, Predicate p, Function f v) => FirstOrderFormula (NormalSentence v p f) (NormalSentence v p f) v where-    for_all _ _ = error "FirstOrderFormula NormalSentence"-    exists _ _ = error "FirstOrderFormula NormalSentence"-    foldFirstOrder _ co tf at f =-        case f of-          NFNot x -> co ((:~:) x)-          NFEqual _ _ -> at f-          NFPredicate p _ -> maybe (at f) tf (asBool p)-{--    zipFirstOrder _ co tf at f1 f2 =-        case (f1, f2) of-          (NFNot f1', NFNot f2') -> co ((:~:) f1') ((:~:) f2')-          (NFEqual _ _, NFEqual _ _) -> at f1 f2-          (NFPredicate _ _, NFPredicate _ _) -> at f1 f2-          _ -> Nothing--}--instance (Formula (NormalSentence v p f) (NormalSentence v p f),-          Combinable (NormalSentence v p f), Predicate p, Function f v, Variable v) => HasFixity (NormalSentence v p f) where-    fixity = fixityFirstOrder--instance (Variable v, Function f v) => Term (NormalTerm v f) v f where-    vt = NormalVariable-    fApp = NormalFunction-    foldTerm v f t =-            case t of-              NormalVariable x -> v x-              NormalFunction x ts -> f x ts-    zipTerms v fn t1 t2 =-        case (t1, t2) of-          (NormalVariable x1, NormalVariable x2) -> v x1 x2-          (NormalFunction f1 ts1, NormalFunction f2 ts2) -> fn f1 ts1 f2 ts2-          _ -> Nothing--toSentence :: (FirstOrderFormula (Sentence v p f) (Sentence v p f) v, Atom (Sentence v p f) (CTerm v f) v, Function f v, Variable v, Predicate p) =>-              NormalSentence v p f -> Sentence v p f-toSentence (NFNot s) = (.~.) (toSentence s)-toSentence (NFEqual t1 t2) = toTerm t1 .=. toTerm t2-toSentence (NFPredicate p ts) = pApp p (map toTerm ts)--toTerm :: (Variable v, Function f v) => NormalTerm v f -> CTerm v f-toTerm (NormalFunction f ts) = fApp f (map toTerm ts)-toTerm (NormalVariable v) = vt v--fromSentence :: forall v p f. (FirstOrderFormula (Sentence v p f) (Sentence v p f) v, Predicate p) =>-                Sentence v p f -> NormalSentence v p f-fromSentence = foldFirstOrder -                 (\ _ _ _ -> error "fromSentence 1")-                 (\ cm ->-                      case cm of-                        ((:~:) f) -> NFNot (fromSentence f)-                        _ -> error "fromSentence 2")-                 (\ x -> NFPredicate (fromBool x) [])-                 (foldAtomEq (\ p ts -> NFPredicate p (map fromTerm ts))-                             (\ x -> NFPredicate (fromBool x) [])-                             (\ t1 t2 -> NFEqual (fromTerm t1) (fromTerm t2)))--fromTerm :: CTerm v f -> NormalTerm v f-fromTerm (Function f ts) = NormalFunction f (map fromTerm ts)-fromTerm (Variable v) = NormalVariable v
Data/Logic/Tests/Data.hs view
@@ -1,5 +1,5 @@ {-# LANGUAGE DeriveDataTypeable, FlexibleContexts, MonoLocalBinds, NoMonomorphismRestriction, OverloadedStrings, RankNTypes, ScopedTypeVariables, TypeFamilies  #-}-{-# OPTIONS -fno-warn-name-shadowing -fno-warn-missing-signatures #-}+{-# OPTIONS -fno-warn-name-shadowing #-} module Data.Logic.Tests.Data     ( tests     , allFormulas@@ -920,9 +920,7 @@                (String, [TestFormula formula atom v]) -> (String, [formula]) kbKnowledge kb = (fst (kb :: (String, [TestFormula formula atom v])), map formula (snd kb)) -proofs :: forall formula atom term v p f. (formula ~ TFormula, atom ~ TAtom, v ~ V,-                                           FirstOrderFormula formula atom v, AtomEq atom p term, Term term v f, Ord formula, IsString v, IsString p, IsString f) =>-          [TestProof formula term v]+proofs :: forall term v f. (Term term v f, IsString v, Ord v) => [TestProof TFormula term v] proofs =     let -- dog = pApp "Dog" :: [term] -> formula         -- cat = pApp "Cat" :: [term] -> formula
Data/Logic/Tests/Harrison/FOL.hs view
@@ -13,6 +13,7 @@ import Control.Applicative ((<$>), (<*>)) import Control.Applicative.Error (Failing(..)) import Control.Monad (filterM)+import Data.Logic.Classes.Apply (pApp) import Data.Logic.Classes.Combine (Combinable(..), Combination(..), BinOp(..)) import Data.Logic.Classes.Constants (false) import Data.Logic.Classes.Equals (AtomEq(..), (.=.))@@ -90,7 +91,7 @@ -- -------------------------------------------------------------------------   example2 :: Formula FOL-example2 = C.pApp "<" [fApp "+" [vt "x", vt "y"], vt "z"]+example2 = pApp "<" [fApp "+" [vt "x", vt "y"], vt "z"] -- example2 = Atom (R "<" [Fn "+" [Var "x", Var "y"], Var "z"])  -- ------------------------------------------------------------------------- @@ -98,8 +99,8 @@ -- -------------------------------------------------------------------------   example3 :: Formula FOL-example3 = (for_all "x" (C.pApp "<" [vt "x", fApp "2" []] .=>.-                         C.pApp "<=" [fApp "*" [fApp "2" [], vt "x"], fApp "3" []])) .|. false+example3 = (for_all "x" (pApp "<" [vt "x", fApp "2" []] .=>.+                         pApp "<=" [fApp "*" [fApp "2" [], vt "x"], fApp "3" []])) .|. false example4 :: TermType example4 = fApp "*" [fApp "2" [], vt "x"]
Data/Logic/Tests/Harrison/Prop.hs view
@@ -8,7 +8,6 @@ import Data.Logic.Classes.Constants (true, false) import Data.Logic.Classes.Formula (atomic) import Data.Logic.Classes.Negate ((.~.), (¬))-import Data.Logic.Classes.Propositional import Data.Logic.Harrison.Lib ((|=>)) import Data.Logic.Harrison.Prop (eval, atoms, truthTable, tautology, pSubst, psimplify,                                  nnf, dnf', rawdnf, dual, purednf, trivial, cnf')
changelog view
@@ -1,3 +1,11 @@+haskell-logic-classes (1.5) unstable; urgency=low++  * Move the pApp* functions from Data.Logic.Classes.FirstOrder to+    Data.Logic.Classes.Apply, and let them work with any formula,+    not just first order.++ -- David Fox <dsf@seereason.com>  Sat, 29 Mar 2014 07:57:37 -0700+ haskell-logic-classes (1.4.8) unstable; urgency=low    * Make changelog visible in hackage.
logic-classes.cabal view
@@ -1,5 +1,5 @@ Name:             logic-classes-Version:          1.4.8+Version:          1.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@@ -53,7 +53,7 @@                    Data.Logic.Harrison.Skolem                    Data.Logic.Harrison.Tableaux                    Data.Logic.Harrison.Unif-                   Data.Logic.Instances.Chiou+                   -- Data.Logic.Instances.Chiou                    Data.Logic.Instances.PropLogic                    Data.Logic.Instances.SatSolver                    -- Data.Logic.Instances.TPTP