Error is now a wrapper for either instead of its own ADT

Author: dillonhuff

GroupTheoryExample.txt

@@ -11,4 +11,5 @@ V x. E y. Eq[times(x, y), One]
 Inverse[x, y] <-> Eq[times(x, y), One] & Eq[times(y, x), One]
 
 CONCLUSION:
+
 Inverse[x, y] & Inverse[x, z] -> Eq[y, z]

src/Folly/Lexer.hs

@@ -57,8 +57,8 @@ tokEqual t1 t2 = name t1 == name t2
 
 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
 

src/Folly/Parser.hs

@@ -14,8 +14,8 @@ import Folly.Utils
 
 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 @@ parseHypothesis = do
 
 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
 

src/Folly/Resolution.hs

@@ -4,6 +4,7 @@ module Folly.Resolution(isValid,
                         maxClause) where
 
 import Data.List as L
+import Data.Maybe
 import Data.Set as S
 
 import Folly.Clause as C
@@ -40,13 +41,15 @@ isValid' s p t =
 resolve :: (Set Clause -> Clause) -> Set Clause -> Set Clause -> Maybe Clause
 resolve s axioms cls =
   case S.member C.empty cls of
-  True -> lookupGE C.empty cls
-  False -> case S.size cls == 0 of
-    True -> Nothing
-    False ->
-      let c = s cls
-          newClauses = genNewClauses c axioms in
-       resolve s (S.insert c axioms) (S.delete c $ S.union newClauses cls)
+   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)

src/Folly/Utils.hs

@@ -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

src/Main.hs

@@ -17,8 +17,8 @@ main = do
   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"

test/Folly/LexerTests.hs

@@ -8,23 +8,23 @@ 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 "]"])]
+  [("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 "]"])]

test/Folly/ParserTests.hs

@@ -11,15 +11,15 @@ allParserTests = do
 
 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"])))]