atp-haskell 1.14 → 1.14.1

raw patch · 3 files changed

+22/−6 lines, 3 files

Files

• atp-haskell.cabal +4/−2
• src/Data/Logic/ATP/Prop.hs +17/−3
• src/Data/Logic/ATP/Quantified.hs +1/−1

@@ -1,5 +1,5 @@ Name:             atp-haskell-Version:          1.14+Version:          1.14.1 Synopsis:         Translation from Ocaml to Haskell of John Harrison's ATP code Description:      This package is a liberal translation from OCaml to Haskell of                   the automated theorem prover written in OCaml in@@ -15,13 +15,14 @@ Cabal-version:    >= 1.9 Build-Type:       Simple Extra-Source-Files: tests/Extra.hs, .travis.yml, .ghci-Tested-With:      GHC == 7.10.3, GHC == 7.11.*+Tested-With:      GHC == 7.10.3, GHC == 7.11.*, GHC == 8.6.5  Source-Repository head   type: git   location: https://github.com/seereason/atp-haskell  Library+  Default-Language: Haskell2010   Build-Depends:     applicative-extras,     base >= 4.8 && < 5,@@ -91,6 +92,7 @@     -- Data.Logic.ATP.Limitations  Test-Suite atp-haskell-tests+  Default-Language: Haskell2010   Type: exitcode-stdio-1.0   Hs-Source-Dirs: tests   Main-Is: Main.hs

@@ -1087,8 +1087,8 @@ simpcnf ca fm =     foldPropositional (\_ _ _ -> go) (\_ -> go) tf (\_ -> go) fm     where-      tf False = Set.empty-      tf True = singleton Set.empty+      tf False = singleton Set.empty+      tf True = Set.empty       go = let cjs = Set.filter (not . trivial) (purecnf ca fm) in            Set.filter (\c -> not (setAny (\c' -> Set.isProperSubsetOf c' c) cjs)) cjs @@ -1103,9 +1103,22 @@ test35 = TestCase $ assertEqual "cnf (p. 61)" expected input     where input = (prettyShow (cnf' fm), tautology (Iff fm (cnf' fm)))           expected = ("(p∨q)∧(p∨r)∧(¬p∨¬r)", True)+          fm :: PFormula Prop           fm = (p .|. q .&. r) .&. (((.~.)p) .|. ((.~.)r))           [p, q, r] = [Atom (P "p"), Atom (P "q"), Atom (P "r")] +test36, test37 :: Test+test36 = TestCase $ assertEqual "cnf (trivial case: False)" expected input+    where input = (prettyShow (cnf' fm), tautology (Iff fm (cnf' fm)))+          expected = ("⊥", True)+          fm :: PFormula Prop+          fm = F+test37 = TestCase $ assertEqual "cnf (trivial case: True)" expected input+    where input = (prettyShow (cnf' fm), tautology (Iff fm (cnf' fm)))+          expected = ("⊤", True)+          fm :: PFormula Prop+          fm = T+ testProp :: Test testProp = TestLabel "Prop" $            TestList [test00, test01, test02, test03, test04, {-test05,-}@@ -1114,4 +1127,5 @@                      test16, test17, test18, test19, test20,                      test21, test22, test23, test24, test25,                      test26, test27, test28, test29, test30,-                     test31, test32, test33, test34, test35]+                     test31, test32, test33, test34, test35,+                     test36, test37]

@@ -89,7 +89,7 @@       co _ (:<=>:) _ = iffPrec       ne _ = notPrec       tf _ = leafPrec-      at = precedence+      at = (precedence :: Num a => AtomOf formula -> a)  associativityQuantified :: forall formula. IsQuantified formula => formula -> Associativity associativityQuantified = foldQuantified qu co ne tf at