FirstOrderTheory 0.1.0.4 → 0.1.0.6

raw patch · 3 files changed

+40/−2 lines, 3 filesdep +ProperPVP: minor bump suggested

API additions: PVP suggests at least a minor version bump

Dependencies added: Proper

API changes (from Hackage documentation)

Files

• FirstOrderTheory.cabal +2/−2
• src/FirstOrderTheory/Syntax.hs +37/−0
• src/FirstOrderTheory/Theory.hs +1/−0

@@ -2,7 +2,7 @@ -- documentation, see http://haskell.org/cabal/users-guide/  name:                FirstOrderTheory-version:             0.1.0.4+version:             0.1.0.6 synopsis:            Grammar and typeclass for first order theories description:         Grammar and typeclass for first order theories license:             BSD3@@ -17,5 +17,5 @@ library   exposed-modules:     FirstOrderTheory.Theory, FirstOrderTheory.Utils, FirstOrderTheory.Syntax   -- other-modules:       -  build-depends:       base ==4.6.*, containers+  build-depends:       base ==4.6.*, containers, Proper   hs-source-dirs:      src

@@ -1,13 +1,46 @@ module FirstOrderTheory.Syntax(   Literal, Atom, Term,+  NNFFormula, nnfLit, nnfCon, nnfDis,+  toPropositionalCNF,+  negateLit,   atomArgs, predicateName, isFunctionWithName,   isNeg, getAtom, varName, intVal, funcArgs,   lit, nLit, atom, func, var, intConst) where  import Data.List as L +import Proper.CNF+import Proper.Formula+ import FirstOrderTheory.Utils +-- |A quantifier free formla in negation normal form+data NNFFormula+  = Con NNFFormula NNFFormula+  | Dis NNFFormula NNFFormula+  | LF Literal+    deriving (Eq, Ord, Show)++-- |Returns a NNF Formula consisting of only the input literal+nnfLit :: Literal -> NNFFormula+nnfLit l = LF l++-- |Returns the conjunction of two NNF formulas+nnfCon l r = Con l r++-- |Return the disjunction of two NNF formulas+nnfDis l r = Dis l r++-- | Convert NNFFormula to propositional formula in+-- conjunctive normal form+toPropositionalCNF :: NNFFormula -> CNF Literal+toPropositionalCNF formula = toCNF $ toProperFormula formula++toProperFormula :: NNFFormula -> Formula Literal+toProperFormula (LF l) = val l+toProperFormula (Con l r) = con (toProperFormula l) (toProperFormula r)+toProperFormula (Dis l r) = dis (toProperFormula l) (toProperFormula l)+ data Literal   = Lit Atom   | Neg Atom@@ -21,6 +54,10 @@ isNeg :: Literal -> Bool isNeg (Neg _) = True isNeg _ = False++-- |Return the negation of the input literal+negateLit (Lit a) = Neg a+negateLit (Neg a) = Lit a  -- |Returns the atomic formula of the given literal getAtom :: Literal -> Atom

@@ -2,6 +2,7 @@   FirstOrderTheory(..),   PredicateDecl,   FunctionDecl,+  nnfLit, nnfCon, nnfDis,   predicateDecl,   functionDecl) where