Folly 0.2.0.0 → 0.2.0.1

raw patch · 10 files changed

+85/−88 lines, 10 filesPVP: major bump suggested

API removals or changes: PVP suggests a major version bump

API changes (from Hackage documentation)

Files

• Folly.cabal +1/−1
• src/Folly/Clause.hs +12/−7
• src/Folly/Formula.hs +5/−1
• src/Folly/Lexer.hs +2/−2
• src/Folly/Parser.hs +4/−4
• src/Folly/Resolution.hs +23/−14
• src/Folly/Utils.hs +4/−25
• src/Main.hs +2/−2
• test/Folly/LexerTests.hs +20/−20
• test/Folly/ParserTests.hs +12/−12

@@ -2,7 +2,7 @@ --  see http://haskell.org/cabal/users-guide/  name:                Folly-version:             0.2.0.0+version:             0.2.0.1 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

@@ -15,6 +15,11 @@ data Clause = Clause (Set Formula) Justification            deriving (Show) +data Justification+  = Given+  | Resolved Clause Clause Unifier Unifier+    deriving (Eq, Ord, Show)+ instance Eq Clause where   (==) (Clause cs1 _) (Clause cs2 _) = cs1 == cs2 @@ -26,11 +31,6 @@  empty = Clause S.empty Given -data Justification-  = Given-  | Resolved Clause Clause Unifier Unifier-    deriving (Eq, Ord, Show)- applySub :: Unifier -> Clause -> Clause applySub u c@(Clause lits j) =   Clause (S.map (\lit -> applyToTerms lit (applyUnifier u)) lits) j@@ -88,10 +88,15 @@  showTrace c = showTraceRec 0 c -showTraceRec n c@(Clause cs Given) = (ind n) ++ "GIVEN " ++ show cs+showTraceRec n c@(Clause cs Given) = (ind n) ++ "GIVEN " ++ showLits cs showTraceRec n c@(Clause cs (Resolved a b u _)) =-  (ind n) ++ show cs ++ "\t" ++ show u ++ "\n" +++  (ind n) ++ showLits cs ++ "  " ++ show u ++ "\n" ++   showTraceRec (n+1) a ++ "\n" ++   showTraceRec (n+1) b  ind n = L.concat $ L.replicate n "  "++showLits ls = "{" ++ (L.concat $ L.intersperse " " $ L.map show lits) ++ "}"+  where+    lits = S.toList ls+    n = L.length lits

@@ -5,6 +5,7 @@   appendVarName, collectVars,   var, func, constant,   te, fa, pr, con, dis, neg, imp, bic, t, f,+  (/\), (\/),   vars, freeVars, isAtom, stripNegations,   generalize, subFormula,   applyToTerms,@@ -86,7 +87,7 @@ showFormula T = "True" showFormula F = "False" showFormula (P predName args) = predName ++ "[" ++ (concat $ intersperse ", " $ L.map showTerm args)  ++ "]"---showFormula (N (P name args)) = "~" ++ show (P name args)+showFormula (N (P name args)) = "~" ++ show (P name args) showFormula (N f) = "~(" ++ show f ++ ")" showFormula (B op f1 f2) = "(" ++ show f1 ++ " " ++ op ++ " "  ++ show f2 ++ ")" showFormula (Q q t f) = "(" ++ q ++ " "  ++ show t ++ " . " ++ show f ++ ")"@@ -120,6 +121,9 @@ neg f = N f t = T f = F++(/\) = con+(\/) = dis  vars :: Formula -> Set Term vars T = S.empty

@@ -57,8 +57,8 @@  lexer :: String -> Error [Token] lexer str = case parse parseToks "LEXER" str of-  Left err -> Failed $ show err-  Right toks -> Succeeded $ toks+  Left err -> Left $ show err+  Right toks -> Right toks  parseToks = endBy parseTok spaces 

@@ -14,8 +14,8 @@  parseTheorem :: [Token] -> Error Theorem parseTheorem toks = case parse parseTheoremToks "PARSER" toks of-  Left err -> Failed $ show err-  Right thm -> Succeeded thm+  Left err -> Left $ show err+  Right thm -> Right thm  parseTheoremToks = do   axioms <- parseHypothesis@@ -34,8 +34,8 @@  parseFormula :: [Token] -> Error (Formula) parseFormula toks = case parse parseForm "PARSER" toks of-  Left err -> Failed $ show err-  Right formula -> Succeeded formula+  Left err -> Left $ show err+  Right formula -> Right formula  parseForm = buildExpressionParser table parseFactor 

@@ -4,6 +4,7 @@                         maxClause) where  import Data.List as L+import Data.Maybe import Data.Set as S  import Folly.Clause as C@@ -11,7 +12,10 @@ import Folly.Theorem  isValid :: Theorem -> Bool-isValid t = isValid' maxClause standardSkolem t+isValid t =+  case isValid' maxClause standardSkolem t of+   Just _ -> True+   Nothing -> False  maxClause cs = S.findMax cs @@ -23,24 +27,29 @@    isValid' :: (Set Clause -> Clause) -> -- Clause selection             (Theorem -> Set Clause) -> -- Preprocessor-            Theorem -> Bool+            Theorem -> Maybe Clause isValid' s p t =   case S.size clauses == 0 of-   True -> False-   False -> not $ resolve s (S.singleton (s clauses)) (S.delete (s clauses) clauses)+   True -> Nothing+   False ->+     case S.member C.empty clauses of+      True -> S.lookupGE C.empty clauses+      False -> resolve s (S.singleton (s clauses)) (S.delete (s clauses) clauses)   where     clauses = p t -resolve :: (Set Clause -> Clause) -> Set Clause -> Set Clause -> Bool-resolve s axioms cls = case S.member C.empty axioms ||-                            S.member C.empty cls of-  True -> False-  False -> case S.size cls == 0 of-    True -> True-    False ->-      let c = s cls-          newClauses = genNewClauses c axioms in-       resolve s (S.insert c axioms) (S.delete c $ S.union newClauses cls)+resolve :: (Set Clause -> Clause) -> Set Clause -> Set Clause -> Maybe Clause+resolve s axioms cls =+  case S.member C.empty cls of+   True -> S.lookupGE C.empty cls+   False -> case S.size cls == 0 of+     True -> Nothing+     False ->+       let c = s cls+           newClauses = genNewClauses c axioms+           nextAxioms = S.insert c axioms+           nextCls = S.delete c $ S.union newClauses cls in+        resolve s nextAxioms nextCls  genNewClauses c cls =   S.fold S.union S.empty $ S.map (\x -> S.union (resolvedClauses c x) (resolvedClauses x c)) (S.delete c cls)

@@ -1,32 +1,11 @@ module Folly.Utils(   Name,-  Error(..), extractValue) where+  Error, extractValue) where  type Name = String -data Error a =-  Succeeded a |-  Failed String-  deriving (Show)--instance Applicative Error where-  pure = Succeeded-  (Succeeded f) <*> (Succeeded x) = Succeeded (f x)-  (Failed m) <*> _ = Failed m--instance Functor Error where-  fmap f (Succeeded a) = Succeeded (f a)-  fmap _ (Failed m) = Failed m--instance Monad Error where-  return a = Succeeded a-  (Succeeded a) >>= f = f a-  (Failed errMsg) >>= f = (Failed errMsg)--instance Eq a => Eq (Error a) where-  (==) (Succeeded v1) (Succeeded v2) = v1 == v2-  (==) _ _ = False+type Error a = Either String a  extractValue :: Error a -> a-extractValue (Succeeded val) = val-extractValue (Failed errMsg) = error $ "Computation Failed: " ++ errMsg+extractValue (Right val) = val+extractValue (Left errMsg) = error $ "Computation Failed: " ++ errMsg

@@ -17,8 +17,8 @@   thmString <- hGetContents fHandle   let thm = processTheoremFile thmString   case thm of-    Failed errMsg -> putStrLn errMsg-    Succeeded t -> do+    Left errMsg -> putStrLn errMsg+    Right t -> do       putStr $ show t       case isValid t of         True -> putStrLn "\n\nIs Valid"

@@ -8,23 +8,23 @@   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 "]"])]+  [("nooo", Right $ [testVar "nooo"]),+   ("(", Right $ [testSep "("]),+   (")", Right $ [testSep ")"]),+   ("[", Right $ [testSep "["]),+   ("]", Right $ [testSep "]"]),+   (",", Right $ [testSep ","]),+   (".", Right $ [testSep "."]),+   ("|", Right $ [testOp "|"]),+   ("&", Right $ [testOp "&"]),+   ("~", Right $ [testOp "~"]),+   ("->", Right $ [testOp "->"]),+   ("<->", Right $ [testOp "<->"]),+   ("E", Right $ [testQuant "E"]),+   ("Q", Right $ [testQuant "Q"]),+   ("=", Right $ [testPred "="]),+   ("Ever", Right $ [testPred "Ever"]),+   ("Quacks", Right $ [testPred "Quacks"]),+   ("N#%_Man", Right $ [testPred "N#%_Man"]),+   ("n#2@", Right $ [testVar "n#2@"]),+   ("V z . E k. F[z] -> G[k]", Right $ [testPred "V", testVar "z", testSep ".", testPred "E", testVar "k", testSep ".", testPred "F", testSep "[", testVar "z", testSep "]", testOp "->", testPred "G", testSep "[", testVar "k", testSep "]"])]

@@ -11,15 +11,15 @@  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"])))]+  [("Dog[ a ]", Right $ pr "Dog" [var "a"]),+   ("~Super[ k, kill(a, b)]", Right $ neg (pr "Super" [var "k", func "kill" [var "a", var "b"]])),+   ("Dog[x] & Owns[John, x]", Right $ con (pr "Dog" [var "x"]) (pr "Owns" [constant "John", var "x"])),+   ("Dog [x] & (Owns[John, x] | Not[Cat, John])", Right $ con (pr "Dog" [var "x"]) (dis (pr "Owns" [constant "John", var "x"]) (pr "Not" [constant "Cat", constant "John"]))),+   ("Ex[p] | ~Ex[x]", Right $ dis (pr "Ex" [var "p"]) (neg (pr "Ex" [var "x"]))),+   ("Ex[p] -> ~Ex[x]", Right $ imp (pr "Ex" [var "p"]) (neg (pr "Ex" [var "x"]))),+   ("Ex[p] <-> ~Vx[x]", Right $ bic (pr "Ex" [var "p"]) (neg (pr "Vx" [var "x"]))),+   ("V x . U#12[x]", Right $ fa (var "x") (pr "U#12" [var "x"])),+   ("E y . K[f(l, y, No)]", Right $ te (var "y") (pr "K" [func "f" [var "l", var "y", constant "No"]])),+   ("V z . E k. F[z] -> G[k]", Right $ fa (var "z") (te (var "k") (imp (pr "F" [var "z"]) (pr "G" [var "k"])))),+   ("E y. K[y] -> V x. Z[x, y]", Right $ te (var "y") (imp (pr "K" [var "y"]) (fa (var "x") (pr "Z" [var "x", var "y"])))),+   ("E y. K[y] -> Z[x, y]", Right $ te (var "y") (imp (pr "K" [var "y"]) (pr "Z" [var "x", var "y"])))]