Folly 0.1.4.3 → 0.1.4.4
raw patch · 6 files changed
+342/−3 lines, 6 files
Files
- Folly.cabal +3/−3
- test/Folly/FormulaTests.hs +201/−0
- test/Folly/LexerTests.hs +30/−0
- test/Folly/ParserTests.hs +25/−0
- test/Folly/ResolutionTests.hs +41/−0
- test/Folly/UnificationTests.hs +42/−0
Folly.cabal view
@@ -2,7 +2,7 @@ -- see http://haskell.org/cabal/users-guide/ name: Folly-version: 0.1.4.3+version: 0.1.4.4 synopsis: A first order logic library in Haskell description: An implementation of first order logic in Haskell that includes a library of modules for incorporating first@@ -26,12 +26,12 @@ executable Folly main-is: Main.hs- -- other-modules: + other-modules: build-depends: base < 6, containers, parsec hs-source-dirs: src executable Folly-tests main-is: Main.hs- -- other-modules: + other-modules: Folly.FormulaTests, Folly.LexerTests, Folly.ParserTests, Folly.ResolutionTests, Folly.UnificationTests build-depends: base < 6, HUnit, containers, parsec hs-source-dirs: test, src
+ test/Folly/FormulaTests.hs view
@@ -0,0 +1,201 @@+module Folly.FormulaTests(allFormulaTests) where++import Data.Map as M+import Data.Set as S+import Folly.Formula+import Folly.TestUtils++allFormulaTests = do+ testFVT+ testVars+ testFreeVars+ testGeneralize+ testSubTerm+ testSubFormula+ testToPNF+ testToPNFPullQuants+ testSkolemize+ testToClausalForm+ +testFVT =+ testFunction fvt fvtCases++fvtCases :: [(Term, Set Term)]+fvtCases =+ [(var "a", S.fromList [var "a"]),+ (func "+" [(var "x"), (var "y")], S.fromList [(var "x"), (var "y")]),+ (func "*" [(var "x"), (func "-" [(var "y"), (var "z")])],+ S.fromList [var "x", var "y", var "z"]),+ (constant "1", S.empty)]+ +testVars =+ testFunction vars varsCases++varsCases :: [(Formula, Set Term)]+varsCases =+ [(t, S.empty),+ (f, S.empty),+ (pr "<" [(var "a"), (var "b")], S.fromList [(var "a"), (var "b")]),+ (imp (pr ">" [(var "c")]) (pr "<" [(var "d"), (var "e")]),+ S.fromList [(var "c"), (var "d"), (var "e")]),+ (neg (pr "isReal" [(var "i")]), S.fromList [(var "i")]),+ (te (var "x") (pr "=" [(var "k"), (var "j")]),+ S.fromList [(var "x"), (var "k"), (var "j")])]+ +testFreeVars =+ testFunction freeVars freeVarCases++freeVarCases :: [(Formula, Set Term)]+freeVarCases =+ [(t, S.empty),+ (f, S.empty),+ (pr "<" [(var "a"), (var "b")], S.fromList [(var "a"), (var "b")]),+ (imp (pr ">" [(var "c")]) (pr "<" [(var "d"), (var "e")]),+ S.fromList [(var "c"), (var "d"), (var "e")]),+ (neg (pr "isReal" [(var "i")]), S.fromList [(var "i")]),+ (te (var "x") (pr "=" [(var "x")]), S.empty)]++testGeneralize =+ testFunction generalize generalizeCases++generalizeCases :: [(Formula, Formula)]+generalizeCases =+ [(t, t),+ (f, f),+ (pr "!" [var "x"], (fa (var "x") (pr "!" [var "x"]))),+ (fa (var "y") (pr "is" [var "x", var "y"]),+ fa (var "x") (fa (var "y") (pr "is" [var "x", var "y"]))),+ (te (var "k") (pr "no" [var "l", var "k", var "s"]),+ (fa (var "s") (fa (var "l") (te (var "k") (pr "no" [var "l", var "k", var "s"])))))]+ +testSubTerm =+ testFunction (subTerm testSub) subTermCases++testSub :: Map Term Term+testSub = M.fromList+ [(var "x", func "+" [var "a", var "b"]),+ (var "k", func "*" [var "c", var "d"])]++subTermCases :: [(Term, Term)]+subTermCases =+ [(constant "o", constant "o"),+ (var "x", func "+" [var "a", var "b"]),+ (func "su" [var "x", var "l"],+ func "su" [func "+" [var "a", var "b"], var "l"]),+ (func "op" [func "op" [var "k", var "x"]],+ func "op" [func "op"+ [func "*" [var "c", var "d"],+ func "+" [var "a", var "b"]]])]+ +testSubFormula =+ testFunction (subFormula testFormSub) subFormulaCases++testFormSub = M.fromList+ [(var "x", var "a"), (var "y", var "l")]++subFormulaCases :: [(Formula, Formula)]+subFormulaCases =+ [(t, t),+ (f, f),+ (pr "a" [var "x"], pr "a" [var "a"]),+ (imp (pr "xo" [var "x"]) (pr "d" [var "y"]),+ imp (pr "xo" [var "a"]) (pr "d" [var "l"])),+ (neg (pr "isX" [var "x"]), neg (pr "isX" [var "a"])),+ (fa (var "q") (pr "isK" [var "x", constant "p"]),+ fa (var "q") (pr "isK" [var "a", constant "p"])),+ (te (var "a") (pr "gotcha" [var "x", var "a"]),+ te (var "a'") (pr "gotcha" [var "a", var "a'"])),+ (fa (var "a") (te (var "a'") (pr "=" [var "x", var "a'"])),+ fa (var "a'") (te (var "a''") (pr "=" [var "a", var "a''"])))]+ +testToPNF =+ testFunction toPNF pnfCases++pnfCases :: [(Formula, Formula)]+pnfCases =+ [(t, t),+ (f, f),+ (imp (pr "a" [var "z"]) (pr "b" [var "z"]),+ dis (neg (pr "a" [var "z"])) (pr "b" [var "z"])),+ (bic (pr "d" [var "z"]) (pr "o" [var "k"]),+ con (dis (neg (pr "d" [var "z"])) (pr "o" [var "k"]))+ (dis (neg (pr "o" [var "k"])) (pr "d" [var "z"]))),+ (fa (var "x") (pr "d" [var "k", var "l"]),+ pr "d" [var "k", var "l"]),+ (fa (var "x") (te (var "d") (pr "i" [var "x", var "y"])),+ fa (var "x") (pr "i" [var "x", var "y"])),+ (neg (con (pr "a" [var "d"]) (pr "k" [var "l"])),+ dis (neg (pr "a" [var "d"])) (neg (pr "k" [var "l"]))),+ (neg (neg (dis (pr "a" [var "z"]) (pr "d" [var "k"]))),+ dis (pr "a" [var "z"]) (pr "d" [var "k"])),+ (neg (con (dis (pr "d" [var "x"]) (pr "e" [var "p"])) (pr "p" [var "w"])),+ dis (con (neg (pr "d" [var "x"])) (neg (pr "e" [var "p"]))) (neg (pr "p" [var "w"]))),+ (neg (fa (var "x") (pr "e" [var "x"])), te (var "x") (neg (pr "e" [var "x"]))),+ (neg (te (var "i") (pr "ds" [var "i"])), fa (var "i") (neg (pr "ds" [var "i"]))),+ (neg (con t f), t),+ (neg (neg (pr "d" [var "k"])), pr "d" [var "k"]),+ (dis f t, t),+ (dis f f, f),+ (con f t, f),+ (con t f, f),+ (con t t, t),+ (neg (neg (neg (pr "d" [var "o"]))), neg (pr "d" [var "o"])),+ (dis (neg (con (pr "Dog" [var "x"]) (pr "Owns" [var "y", var "x"]))) (pr "LovesAnimals" [var "y"]), (dis (dis (neg (pr "Dog" [var "x"])) (neg (pr "Owns" [var "y", var "x"]))) (pr "LovesAnimals" [var "y"])))]+ +testToPNFPullQuants =+ testFunction toPNF pullQuantsCases++pullQuantsCases :: [(Formula, Formula)]+pullQuantsCases =+ [(con (fa (var "x") (pr "d" [var "x"])) (fa (var "y") (pr "k" [var "y"])),+ fa (var "x") (con (pr "d" [var "x"]) (pr "k" [var "x"]))),+ (dis (te (var "k") (pr "d" [var "k"])) (te (var "j") (pr "i" [var "j"])),+ te (var "k") (dis (pr "d" [var "k"]) (pr "i" [var "k"]))),+ (dis (fa (var "k") (pr "d" [var "k"])) (pr "j" [var "k"]),+ fa (var "k'") (dis (pr "d" [var "k'"]) (pr "j" [var "k"]))),+ (dis (pr "d" [var "l"]) (fa (var "k") (pr "lj" [var "k"])),+ fa (var "k") (dis (pr "d" [var "l"]) (pr "lj" [var "k"]))),+ (dis (te (var "k") (pr "d" [var "k"])) (pr "j" [var "k"]),+ te (var "k'") (dis (pr "d" [var "k'"]) (pr "j" [var "k"]))),+ (dis (pr "d" [var "l"]) (te (var "k") (pr "lj" [var "k"])),+ te (var "k") (dis (pr "d" [var "l"]) (pr "lj" [var "k"]))),+ (con (fa (var "k") (pr "d" [var "k"])) (pr "j" [var "k"]),+ fa (var "k'") (con (pr "d" [var "k'"]) (pr "j" [var "k"]))),+ (con (pr "d" [var "l"]) (fa (var "k") (pr "lj" [var "k"])),+ fa (var "k") (con (pr "d" [var "l"]) (pr "lj" [var "k"]))),+ (con (te (var "k") (pr "d" [var "k"])) (pr "j" [var "k"]),+ te (var "k'") (con (pr "d" [var "k'"]) (pr "j" [var "k"]))),+ (con (pr "d" [var "l"]) (te (var "k") (pr "lj" [var "k"])),+ te (var "k") (con (pr "d" [var "l"]) (pr "lj" [var "k"]))),+ (con (con (fa (var "x") (pr "d" [var "x"])) (pr "i" [var "x"])) (pr "d" [var "k"]),+ fa (var "x'") (con (con (pr "d" [var "x'"]) (pr "i" [var "x"])) (pr "d" [var "k"])))]+ +testSkolemize =+ testFunction toSkolemForm skolemizeCases++skolemizeCases :: [(Formula, Formula)]+skolemizeCases =+ [(pr "d" [var "a"], pr "d" [var "a"]),+ (te (var "x") (pr "d" [var "x"]), pr "d" [skf 0 []]),+ (te (var "x") (fa (var "y") (pr "d" [var "x", var "y"])),+ fa (var "y") (pr "d" [skf 0 [], var "y"])),+ (fa (var "k") (te (var "l") (te (var "m") (pr "i" [var "l", var "m", var "k"]))),+ fa (var "k") (pr "i" [skf 0 [var "k"], skf 1 [var "k"], var "k"])),+ (fa (var "a") (te (var "b") (fa (var "c") (pr "l" [var "b", var "c", var "a"]))),+ fa (var "a") (fa (var "c") (pr "l" [skf 0 [var "a"], var "c", var "a"]))),+ (fa (var "a") (fa (var "b") (te (var "c") (pr "l" [var "a", var "c", var "b"]))),+ fa (var "a") (fa (var "b") (pr "l" [var "a", skf 0 [var "b", var "a"], var "b"])))]++testToClausalForm =+ testFunction toClausalForm clausalFormCases++clausalFormCases :: [(Formula, [[Formula]])]+clausalFormCases =+ [(pr "d" [var "no"], [[pr "d" [var "no"]]]),+ (fa (var "x") (con (pr "a" [var "x"]) (pr "d" [constant "P"])),+ [[pr "a" [var "x"]], [pr "d" [constant "P"]]]),+ (dis (pr "a" [var "x"]) (pr "d" [var "c"]), [[pr "a" [var "x"], pr "d" [var "c"]]]),+ (bic (pr "P" [var "x"]) (con (pr "Q" [var "y"]) (pr "R" [var "z"])),+ [[neg (pr "P" [var "x"]), pr "Q" [var "y"]],+ [neg (pr "P" [var "x"]), pr "R" [var "z"]],+ [neg (pr "Q" [var "y"]), neg (pr "R" [var "z"]), pr "P" [var "x"]]])]
+ test/Folly/LexerTests.hs view
@@ -0,0 +1,30 @@+module Folly.LexerTests(allLexerTests) where++import Folly.Lexer+import Folly.TestUtils+import Folly.Utils++allLexerTests = do+ testFunction lexer lexerCases++lexerCases =+ [("nooo", Succeeded $ [testVar "nooo"]),+ ("(", Succeeded $ [testSep "("]),+ (")", Succeeded $ [testSep ")"]),+ ("[", Succeeded $ [testSep "["]),+ ("]", Succeeded $ [testSep "]"]),+ (",", Succeeded $ [testSep ","]),+ (".", Succeeded $ [testSep "."]),+ ("|", Succeeded $ [testOp "|"]),+ ("&", Succeeded $ [testOp "&"]),+ ("~", Succeeded $ [testOp "~"]),+ ("->", Succeeded $ [testOp "->"]),+ ("<->", Succeeded $ [testOp "<->"]),+ ("E", Succeeded $ [testQuant "E"]),+ ("Q", Succeeded $ [testQuant "Q"]),+ ("=", Succeeded $ [testPred "="]),+ ("Ever", Succeeded $ [testPred "Ever"]),+ ("Quacks", Succeeded $ [testPred "Quacks"]),+ ("N#%_Man", Succeeded $ [testPred "N#%_Man"]),+ ("n#2@", Succeeded $ [testVar "n#2@"]),+ ("V z . E k. F[z] -> G[k]", Succeeded $ [testPred "V", testVar "z", testSep ".", testPred "E", testVar "k", testSep ".", testPred "F", testSep "[", testVar "z", testSep "]", testOp "->", testPred "G", testSep "[", testVar "k", testSep "]"])]
+ test/Folly/ParserTests.hs view
@@ -0,0 +1,25 @@+module Folly.ParserTests(allParserTests) where++import Folly.Formula+import Folly.Lexer+import Folly.Parser+import Folly.TestUtils+import Folly.Utils++allParserTests = do+ testFunction (\x -> ((>>=) x parseFormula)) (map (\ (x, y) -> (lexer x, y)) parseFormulaCases)++parseFormulaCases :: [(String, Error Formula)]+parseFormulaCases =+ [("Dog[ a ]", Succeeded $ pr "Dog" [var "a"]),+ ("~Super[ k, kill(a, b)]", Succeeded $ neg (pr "Super" [var "k", func "kill" [var "a", var "b"]])),+ ("Dog[x] & Owns[John, x]", Succeeded $ con (pr "Dog" [var "x"]) (pr "Owns" [constant "John", var "x"])),+ ("Dog [x] & (Owns[John, x] | Not[Cat, John])", Succeeded $ con (pr "Dog" [var "x"]) (dis (pr "Owns" [constant "John", var "x"]) (pr "Not" [constant "Cat", constant "John"]))),+ ("Ex[p] | ~Ex[x]", Succeeded $ dis (pr "Ex" [var "p"]) (neg (pr "Ex" [var "x"]))),+ ("Ex[p] -> ~Ex[x]", Succeeded $ imp (pr "Ex" [var "p"]) (neg (pr "Ex" [var "x"]))),+ ("Ex[p] <-> ~Vx[x]", Succeeded $ bic (pr "Ex" [var "p"]) (neg (pr "Vx" [var "x"]))),+ ("V x . U#12[x]", Succeeded $ fa (var "x") (pr "U#12" [var "x"])),+ ("E y . K[f(l, y, No)]", Succeeded $ te (var "y") (pr "K" [func "f" [var "l", var "y", constant "No"]])),+ ("V z . E k. F[z] -> G[k]", Succeeded $ fa (var "z") (te (var "k") (imp (pr "F" [var "z"]) (pr "G" [var "k"])))),+ ("E y. K[y] -> V x. Z[x, y]", Succeeded $ te (var "y") (imp (pr "K" [var "y"]) (fa (var "x") (pr "Z" [var "x", var "y"])))),+ ("E y. K[y] -> Z[x, y]", Succeeded $ te (var "y") (imp (pr "K" [var "y"]) (pr "Z" [var "x", var "y"])))]
+ test/Folly/ResolutionTests.hs view
@@ -0,0 +1,41 @@+module Folly.ResolutionTests(allResolutionTests) where++import Folly.Formula+import Folly.Resolution+import Folly.Theorem+import Folly.TestUtils++allResolutionTests = do+ testIsValid++testIsValid =+ testFunction isValid isValidTestCases++isValidTestCases :: [(Theorem, Bool)]+isValidTestCases =+ [(theorem [] (fa (var "a") (dis (pr "d" [var "a"]) (neg (pr "d" [var "a"])))), True),+ (theorem [] (pr "d" [var "k"]), False),+ (theorem [pr "Dog" [var "x"]] (pr "Dog" [var "x"]), True),+ (theorem+ [(fa (var "d") (imp (pr "Dog" [var "d"]) (pr "Loves" [constant "John", var "d"]))),+ (pr "Dog" [constant "Fido"])]+ (pr "Loves" [constant "John", constant "Fido"]), True),+ (theorem+ [(fa (var "p") (imp (te (var "d") (con (pr "Dog" [var "d"]) (pr "Owns" [var "p", var "d"]))) (pr "LovesAnimals" [var "p"]))),+ (imp (pr "LovesAnimals" [var "x"]) (fa (var "a") (neg (pr "Kills" [var "x", var "a"])))),+ (pr "Owns" [constant "John", constant "Fido"]),+ (pr "Dog" [constant "Fido"])]+ (fa (var "a") (neg (pr "Kills" [constant "John", var "a"]))), True),+ (theorem groupWithEquals (imp (con (con (con (pr "=" [func "*" [var "x", var "y"], constant "1"]) (pr "=" [func "*" [var "y", var "x"], constant "1"])) (pr "=" [func "*" [var "x", var "z"], constant "1"])) (pr "=" [func "*" [var "z", var "x"], constant "1"])) (pr "=" [var "y", var "z"])), True),+ (theorem groupWithEquals (imp (fa (var "x") (con (pr "=" [func "*" [var "x", var "z"], constant "1"]) (pr "=" [func "*" [var "z", var "x"], constant "1"]))) (pr "=" [var "z", constant "1"])), True)]++equalityAxioms :: [Formula]+equalityAxioms =+ [(fa (var "x") (pr "=" [var "x", var "x"])),+ (fa (var "x") (fa (var "y") (imp (pr "=" [var "x", var "y"]) (pr "=" [var "y", var "x"])))),+ (fa (var "x") (fa (var "y") (fa (var "z") (imp (con (pr "=" [var "x", var "y"]) (pr "=" [var "y", var "z"])) (pr "=" [var "x", var "z"])))))]++groupWithEquals =+ [(fa (var "x") (te (var "y") (con (pr "=" [func "*" [var "x", var "y"], constant "1"]) (pr "=" [func "*" [var "y", var "x"], constant "1"])))),+ (fa (var "x") (fa (var "y") (fa (var "z") (pr "=" [func "*" [var "x", func "*" [var "y", var "z"]], func "*" [func "*" [var "x", var "y"], var "z"]])))),+ (fa (var "x") (con (pr "=" [func "*" [var "x", constant "1"], var "x"]) (pr "=" [func "*" [constant "1", var "x"], constant "x"])))] ++ equalityAxioms
+ test/Folly/UnificationTests.hs view
@@ -0,0 +1,42 @@+module Folly.UnificationTests(allUnificationTests) where++import Folly.Formula+import Folly.TestUtils+import Folly.Unification++allUnificationTests = do+ testApplyUnifier+ testMostGeneralUnifier++simpleUnifier = unifier [(var "d", constant "Fido"),+ (var "n", constant "OOH-KILLEM"),+ (var "k", func "x" [(var "y")]),+ (var "y", var "n"),+ (var "q", var "uio")]++testApplyUnifier =+ testFunction (applyUnifier simpleUnifier) applyUnifierCases++applyUnifierCases =+ [(var "should-not-change", var "should-not-change"),+ (var "q", var "uio"),+ (var "d", constant "Fido"),+ (var "k", func "x" [constant "OOH-KILLEM"]),+ (func "nest" [var "k"], func "nest" [func "x" [constant "OOH-KILLEM"]])]++testMostGeneralUnifier =+ testFunction mostGeneralUnifier mguTestCases++mguTestCases =+ [([(var "x", var "x")], Just $ unifier []),+ ([(var "x", var "y")], Just $ unifier [(var "x", var "y")]),+ ([(var "x", var "z"), (constant "p", constant "dsf")], Nothing),+ ([(var "x", func "d" [constant "x", func "k" [var "x"]])], Nothing),+ ([(var "x", var "y"), (var "x", var "x"), (var "x", constant "K")],+ Just $ unifier [(var "x", var "y"), (var "y", constant "K")]),+ ([(func "g" [var "x2"], var "x1"),+ (func "f" [var "x1", func "h" [var "x1"], var "x2"],+ func "f" [func "g" [var "x3"], var "x4", var "x3"])],+ Just $ unifier [(var "x2", var "x3"),+ (var "x1", func "g" [var "x2"]),+ (var "x4", func "h" [func "g" [var "x3"]])])]