WeberLogic (empty) → 0.1.0.0
raw patch · 7 files changed
+610/−0 lines, 7 filesdep +basedep +parsecsetup-changed
Dependencies added: base, parsec
Files
- LICENSE +30/−0
- README.md +63/−0
- Setup.hs +2/−0
- WeberLogic.cabal +33/−0
- WeberLogic.lhs +65/−0
- WeberLogic/Actions.lhs +269/−0
- WeberLogic/Parser.lhs +148/−0
+ LICENSE view
@@ -0,0 +1,30 @@+Copyright (c) 2014, Cameron Brandon White++All rights reserved.++Redistribution and use in source and binary forms, with or without+modification, are permitted provided that the following conditions are met:++ * Redistributions of source code must retain the above copyright+ notice, this list of conditions and the following disclaimer.++ * Redistributions in binary form must reproduce the above+ copyright notice, this list of conditions and the following+ disclaimer in the documentation and/or other materials provided+ with the distribution.++ * Neither the name of Cameron Brandon White nor the names of other+ contributors may be used to endorse or promote products derived+ from this software without specific prior written permission.++THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS+"AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT+LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR+A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT+OWNER OR CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL,+SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT+LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE,+DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY+THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT+(INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE+OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.
+ README.md view
@@ -0,0 +1,63 @@+HsSymMath+=========++Interactive mathematical languages written in haskell++## Logic.hs ##++Formal logic parser ++### Command line ###++Currently the command line will take a logical expression as an argument and print out its corresponding truth table.++```+$ ./Logic+Enter Command+> TruthTable: a&b+c->~a&b+'a' 'b' 'c' | (((a&b)+c)->(~a&b))+True True True | False+True True False | False+True False True | False+True False False | True +False True True | True +False True False | True +False False True | False+False False False | True ++Enter Command+> ToNand: a&b->c +(((((a|b)|(a|b))|((a|b)|(a|b)))|(((a|b)|(a|b))|((a|b)|(a|b))))|(c|c))++Enter Command+> ToNor: a&b->c+(((((a/a)/(b/b))/((a/a)/(b/b)))/c)/((((a/a)/(b/b))/((a/a)/(b/b)))/c))+```++### Code ###++```haskell+> And (Atom 'a') (Not (Atom 'b'))+(a&~b)++> truthTable $ And (Atom 'a') (Not (Atom 'b'))+'a' 'b' | (a&~b)+True True | False+True False | True +False True | False+False False | False++> toNand $ And (Atom 'a') (Not (Atom 'b'))+((a|(b|b))|(a|(b|b)))++> toNor $ And (Atom 'a') (Not (Atom 'b'))+((a/a)/((b/b)/(b/b)))++> let exp = And (Atom 'a') (Not (Atom 'b'))+> exp == toNand exp+True+> exp == toNor exp+True+> exp == toNor (toNand exp)+True+```
+ Setup.hs view
@@ -0,0 +1,2 @@+import Distribution.Simple+main = defaultMain
+ WeberLogic.cabal view
@@ -0,0 +1,33 @@+-- Initial WeberLogic.cabal generated by cabal init. For further +-- documentation, see http://haskell.org/cabal/users-guide/++name: WeberLogic+version: 0.1.0.0+synopsis: Logic interpreter+description: Logic interpreter+homepage: https://github.com/cameronbwhite/WeberLogic+license: BSD3+license-file: LICENSE+author: Cameron Brandon White+maintainer: cameronbwhite90@gmail.com+-- copyright: +category: Math+build-type: Simple+extra-source-files: README.md+cabal-version: >=1.10++library+ exposed-modules: WeberLogic.Actions, WeberLogic.Parser+ -- other-modules: + -- other-extensions: + build-depends: base >=4.6 && <4.7, parsec >=3.1 && <3.2+ -- hs-source-dirs: + default-language: Haskell2010++executable WeberLogic+ main-is: WeberLogic.lhs+ -- other-modules: + -- other-extensions: + build-depends: base >=4.6 && <4.7, parsec >=3.1 && <3.2+ -- hs-source-dirs: + default-language: Haskell2010
+ WeberLogic.lhs view
@@ -0,0 +1,65 @@+> module WeberLogic where++> import System.Environment+> import System.IO (hFlush, stdout)+> import Text.Parsec (parse)++> import WeberLogic.Parser+> import WeberLogic.Actions++> data Command = TruthTable LogicExp+> | TruthTree [LogicExp]+> | IsArgConsistent [LogicExp]+> | ToNand LogicExp+> | ToNor LogicExp+> | Error String++> main :: IO()+> main = do+> args <- getArgs+> reader++> reader :: IO ()+> reader = do+> putStrLn "Enter Command"+> putStr "> "+> hFlush stdout+> line <- getLine +> runCommand $ readCommand line+> reader++> readCommand :: String -> Command+> readCommand input = case words input of +> ("truthTable:":arguments) -> +> case parse parseExp "truthtable" $ unwords arguments of +> Right val -> TruthTable val+> Left val -> Error $ show val+> ("truthTree:":arguments) ->+> case parse parseArg "truthTree" $ unwords arguments of +> Right val -> TruthTree val+> Left val -> Error $ show val+> ("toNand:":arguments) ->+> case parse parseExp "toNand" $ unwords arguments of +> Right val -> ToNand val+> Left val -> Error $ show val+> ("toNor:":arguments) ->+> case parse parseExp "toNor" $ unwords arguments of +> Right val -> ToNor val+> Left val -> Error $ show val+> ("isArgConsistent:":arguments) ->+> case parse parseArg "isArgConsistent" $ unwords arguments of +> Right val -> IsArgConsistent val+> Left val -> Error $ show val+> _ -> Error input++> runCommand :: Command -> IO()+> runCommand cmd = +> case cmd of+> TruthTable exp -> mapM_ putStrLn $ truthTableStrs exp+> TruthTree exps -> truthTree exps'+> where exps' = (take (length exps - 1) exps) ++ [Not (last exps)]+> IsArgConsistent exps -> putStrLn $ show $ not $ isConsistent exps'+> where exps' = (take (length exps - 1) exps) ++ [Not (last exps)]+> ToNand exp -> putStrLn $ show $ toNand exp+> ToNor exp -> putStrLn $ show $ toNor exp+> Error err -> putStrLn err
+ WeberLogic/Actions.lhs view
@@ -0,0 +1,269 @@+> module WeberLogic.Actions (+> toNand, toNor, truthTree,+> and, or, implies, iff, nand, nor, isConsistent,+> truthTableStrs, truthTableValues) +> where++> import Prelude hiding (and, or)+> import Text.Printf+> import Data.List (union)++> import WeberLogic.Parser++> instance Show Letter where+> show exp =+> case exp of+> Name a -> [a]+> Variable a -> [a]++> instance Eq Letter where+> (==) exp1 exp2 =+> case (exp1, exp2) of+> (Name a, Name b) -> a == b+> (Variable a, Variable b) -> a == b+> (_, _) -> False ++> instance Show LogicExp where+> show exp =+> case exp of+> Not a -> printf "~%s" (show a)+> Or a b -> printf "(%s+%s)" (show a) (show b)+> Xor a b -> printf "(%s⊕%s)" (show a) (show b)+> And a b -> printf "(%s&%s)" (show a) (show b)+> Implies a b -> printf "(%s->%s)" (show a) (show b)+> Iff a b -> printf "(%s<->%s)" (show a) (show b)+> Nand a b -> printf "(%s|%s)" (show a) (show b)+> Nor a b -> printf "(%s/%s)" (show a) (show b)+> Predicate a bs -> printf "%c%s" a $ concatMap (show) bs+ +> instance Eq LogicExp where+> (==) exp1 exp2 =+> case (exp1, exp2) of+> (Predicate a as, Predicate b bs) -> a == b && as == bs+> (Not a, Not b) -> a == b+> (Or a b, Or c d) -> a == c && b == d+> (Xor a b, Xor c d) -> a == c && b == d+> (And a b, And c d) -> a == c && b == d+> (Implies a b, Implies c d) -> a == c && b == d+> (Iff a b, Iff c d) -> a == c && b == d+> (Nand a b, Nand c d) -> a == c && b == d+> (Nor a b, Nor c d) -> a == c && b == d+> (_, _) -> False++ +> lmap :: (LogicExp -> LogicExp) -> LogicExp -> LogicExp+> lmap f exp =+> case exp of +> Not a -> f $ Not (lmap f a)+> Or a b -> f $ Or (lmap f a) (lmap f b)+> And a b -> f $ And (lmap f a) (lmap f b)+> Xor a b -> f $ Xor (lmap f a) (lmap f b)+> Implies a b -> f $ Implies (lmap f a) (lmap f b)+> Iff a b -> f $ Iff (lmap f a) (lmap f b)+> Nand a b -> f $ Nand (lmap f a) (lmap f b)+> Nor a b -> f $ Nor (lmap f a) (lmap f b)+> Predicate a bs -> f exp + +> toNand :: LogicExp -> LogicExp+> toNand exp = lmap (toNand') exp+> where toNand' e = case e of+> Not a -> a `Nand` a+> Or a b -> (a `Nand` a) `Nand` (b `Nand` b)+> And a b -> (a `Nand` b) `Nand` (a `Nand` b)+> Nand a b -> a `Nand` b+> Nor a b -> ((a `Nand` a) `Nand` (b `Nand` b)) `Nand` +> ((a `Nand` a) `Nand` (b `Nand` b))+> Implies a b -> toNand $ Or (toNand $ Not a) b+> Iff a b -> toNand $ (a `Implies` b) `And` (b `Implies` a)+> _ -> e+ +> toNor :: LogicExp -> LogicExp+> toNor exp = lmap (toNor') exp+> where toNor' e = case e of+> Not a -> a `Nor` a+> Or a b -> (a `Nor` b) `Nor` (a `Nor` b)+> And a b -> (a `Nor` a) `Nor` (b `Nor` b)+> Nor a b -> a `Nor` b+> Nand a b -> ((a `Nor` a) `Nor` (b `Nor` b)) `Nor` +> ((a `Nor` a) `Nor` (b `Nor` b))+> Implies a b -> toNor $ Or (toNor $ Not a) b+> Iff a b -> toNor $ (a `Implies` b) `And` (b `Implies` a)+> _ -> e+ + +> decompose :: [LogicExp] -> [[LogicExp]]+> decompose es = decompose' es []+ +> decompose' :: [LogicExp] -> [LogicExp] -> [[LogicExp]]+> decompose' exps as +> | null exps = [as]+> | otherwise = let (e:es) = exps+> in case e of+> Predicate _ _ -> decompose' es (e:as)+> Not(Predicate _ _) -> decompose' es (e:as)+> And x y -> decompose' (x:y:es) as +> Or x y -> (decompose' (x:es) as) ++ (decompose' (y:es) as)+> Implies x y -> (decompose' ((Not x):es) as) ++ (decompose' (y:es) as)+> Iff x y -> decompose' (Or (And x y) (And (Not x) (Not y)):es) as+> Not(And x y) -> (decompose' ((Not x):es) as) ++ (decompose' ((Not y):es) as)+> Not(Or x y) -> decompose' ((Not x):(Not y):es) as +> Not(Implies x y) -> decompose' ((And x (Not y)):es) as+> Not(Iff x y) -> decompose' (Or (And x y) (And (Not x) (Not y)):es) as+ +> isConsistent :: [LogicExp] -> Bool+> isConsistent es = isConsistent' es []+ +> isConsistent' :: [LogicExp] -> [LogicExp] -> Bool+> isConsistent' exps as +> | null exps = True+> | otherwise = let (e:es) = exps+> in case e of+> Predicate _ _ -> if elem (Not e) as then False else isConsistent' es (e:as)+> Not(Predicate x xs) -> if elem (Predicate x xs) as then False else isConsistent' es (e:as)+> And x y -> isConsistent' (x:y:es) as +> Or x y -> (isConsistent' (x:es) as) || (isConsistent' (y:es) as)+> Implies x y -> (isConsistent' ((Not x):es) as) || (isConsistent' (y:es) as)+> Iff x y -> isConsistent' (Or (And x y) (And (Not x) (Not y)):es) as+> Not(And x y) -> (isConsistent' ((Not x):es) as) || (isConsistent' ((Not y):es) as)+> Not(Or x y) -> isConsistent' ((Not x):(Not y):es) as +> Not(Implies x y) -> isConsistent' ((And x (Not y)):es) as+> Not(Iff x y) -> isConsistent' (Or (And x y) (And (Not x) (Not y)):es) as+ +> truthTree :: [LogicExp] -> IO()+> truthTree es = do +> printf "%s\n" $ show es +> truthTree' es [] 0+ +> truthTree' :: [LogicExp] -> [LogicExp] -> Int -> IO()+> truthTree' exps as indent = do+> if null exps +> then print "Open" indent+> else let (e:es) = exps+> in do +> print (show e) indent+> case e of+> Predicate x xs -> if elem (Not e) as +> then print "Closed" indent+> else truthTree' es (e:as) indent+> +> Not(Predicate x xs) -> if elem (Predicate x xs) as +> then print "Closed" indent+> else truthTree' es (e:as) indent+> +> Not(Not x) -> truthTree' (x:es) as indent+> +> And x y -> truthTree' (x:y:es) as indent+> +> Or x y -> do +> truthTree' (x:es) as (indent+1)+> truthTree' (y:es) as (indent+1)+> +> Implies x y -> let z = Or (Not x) (y)+> in truthTree' (z:es) as indent+> +> Iff x y -> let z = Or (And x y) (And (Not x) (Not y)) +> in truthTree' (z:es) as indent+> +> Not(And x y) -> let z = Or (Not x) (Not y) +> in truthTree' (z:es) as indent+> +> Not(Or x y) -> let z = And (Not x) (Not y) +> in truthTree' (z:es) as indent+> +> Not(Implies x y) -> let z = Or (Not x) y+> in truthTree' (z:es) as indent+> +> Not(Iff x y) -> let z = Or (And x y) (And (Not x) (Not y))+> in truthTree' (z:es) as indent+> +> where print str indent = printf "%s%s\n" (replicate (indent*2) ' ') str+ +> evalutateBinary :: (Bool -> Bool -> Bool) -> LogicExp -> LogicExp -> +> [(LogicExp, Bool)] -> Bool+> evalutateBinary operator exp1 exp2 xs = exp1' `operator` exp2'+> where exp1' = evaluate exp1 xs;+> exp2' = evaluate exp2 xs+ +> evaluate :: LogicExp -> [(LogicExp, Bool)] -> Bool+> evaluate exp xs =+> case exp of +> Predicate a as -> if exp == c then v else evaluate exp xs'+> where ((c,v):xs') = xs+> Not a -> not $ evaluate a xs+> And a b -> evalutateBinary and a b xs+> Or a b -> evalutateBinary or a b xs+> Xor a b -> evalutateBinary xor a b xs+> Nand a b -> evalutateBinary nand a b xs+> Nor a b -> evalutateBinary nor a b xs+> Implies a b -> evalutateBinary implies a b xs+> Iff a b -> evalutateBinary iff a b xs+ +> and :: Bool -> Bool -> Bool+> and True True = True+> and _ _ = False+ +> or :: Bool -> Bool -> Bool+> or True _ = True+> or _ True = True+> or _ _ = False+ +> implies :: Bool -> Bool -> Bool+> implies True False = False+> implies _ _ = True+ +> iff :: Bool -> Bool -> Bool+> iff True True = True+> iff False False = True+> iff _ _ = False+ +> xor :: Bool -> Bool -> Bool+> xor False False = False+> xor True True = False+> xor _ _ = True+ +> nand :: Bool -> Bool -> Bool+> nand x y = not (x `and` y)+ +> nor :: Bool -> Bool -> Bool+> nor x y = not (x `or` y)+ +> truthTableStrs :: LogicExp -> [String]+> truthTableStrs exp = +> let (predicates, values, results) = truthTableValues exp +> header_lhs = concatMap (printf "%-5s " . show) predicates+> header_rhs = printf "| %-5s" $ show exp +> header = header_lhs ++ header_rhs+> rows_lhs = map (concatMap (printf "%-5s " . show)) values+> rows_rhs = map (printf "| %-5s" . show) results+> rows = zipWith (++) rows_lhs rows_rhs+> in header : rows++> truthTableValues :: LogicExp -> ([LogicExp], [[Bool]], [Bool])+> truthTableValues exp = +> let (_, _, preds) = getBasics exp+> pred_values = map (zip preds) (perm (length preds) [True, False])+> values = map (map (snd)) pred_values+> results = map (evaluate exp) pred_values+> in (preds, values, results)+ +> perm i xs | i > 0 = [ x:ys | x <- xs, ys <- perm (i-1) xs]+> | otherwise = [[]]+ +> -- ([Names], [Variables], [Predicates])+> getBasics :: LogicExp -> ([Letter], [Letter], [LogicExp])+> getBasics exp = +> case exp of +> Predicate a bs -> foldl sumTuples ([], [], [exp]) $ map toTuple bs+> where toTuple p = case p of+> Name a -> ([p], [], [])+> Variable a -> ([], [p], [])+> Not a -> getBasics a+> Nor a b -> sumTuples (getBasics a) (getBasics b)+> Nand a b -> sumTuples (getBasics a) (getBasics b)+> And a b -> sumTuples (getBasics a) (getBasics b)+> Or a b -> sumTuples (getBasics a) (getBasics b)+> Xor a b -> sumTuples (getBasics a) (getBasics b)+> Iff a b -> sumTuples (getBasics a) (getBasics b)+> Implies a b -> sumTuples (getBasics a) (getBasics b)+> where sumTuples (xs1, xs2, xs3) (ys1, ys2, ys3) = +> ((xs1 `union` ys1), (xs2 `union` ys2), (xs3 `union` ys3))
+ WeberLogic/Parser.lhs view
@@ -0,0 +1,148 @@+> module WeberLogic.Parser (+> Letter(Name, Variable), +> LogicExp(+> Not, Or, Xor, And, Implies, Iff, Nand, Nor, Predicate, Universal,+> Existential),+> parseExp, parseArg) +> where ++> import Prelude hiding (and, or)+> import Data.List (union)+> import Text.Printf+> import Text.Parsec as Parsec+> import Text.Parsec hiding (Error)+> import Text.Parsec.String+> import Text.Parsec.Expr+> import Text.Parsec.Token+> import Text.Parsec.Language+> import qualified Data.List as List++> data Letter+> = Name Char+> | Variable Char++> data LogicExp+> = Not LogicExp+> | Or LogicExp LogicExp+> | Xor LogicExp LogicExp+> | And LogicExp LogicExp+> | Implies LogicExp LogicExp+> | Iff LogicExp LogicExp+> | Nand LogicExp LogicExp+> | Nor LogicExp LogicExp+> | Predicate Char [Letter]+> | Universal Letter LogicExp+> | Existential LogicExp++> parseExp :: Parser LogicExp+> parseExp = do x <- parseExp1+> eof+> return x++> parseExp1 :: Parser LogicExp+> parseExp1 = try $ do+> x <- parseExp2+> x' <- parseExp1' x+> return x'++> parseExp1' :: LogicExp -> Parser LogicExp+> parseExp1' x = try $ do+> string "<->"+> y <- parseExp2+> return $ Iff x y+> <|> do+> return x++> parseExp2 :: Parser LogicExp+> parseExp2 = try $ do+> x <- parseExp3+> x' <- parseExp2' x+> return x'++> parseExp2' :: LogicExp -> Parser LogicExp+> parseExp2' x = try $ do+> string "->"+> y <- parseExp2+> return $ Implies x y+> <|> do+> return x+ +> parseExp3 :: Parser LogicExp+> parseExp3 = try $ do +> lhs <- parseExp4+> rhs <- parseExp3' lhs+> return rhs+> <|> do +> lhs <- parseExp4+> return lhs+ + +> parseOperator3 :: (LogicExp -> LogicExp -> LogicExp) -> +> String -> LogicExp -> Parser (LogicExp)+> parseOperator3 connective symbol lhs+> = try $ do+> string symbol+> rhs <- parseExp4+> exp2 <- parseExp3' $ connective lhs rhs+> return exp2+ +> parseExp3' :: LogicExp -> Parser (LogicExp)+> parseExp3' lhs = parseOperator3 And "&" lhs+> <|> parseOperator3 Or "+" lhs+> <|> parseOperator3 Nand "|" lhs+> <|> parseOperator3 Nor "/" lhs+> <|> parseOperator3 Xor "⊕" lhs+> <|> do+> return lhs+ +> parseExp4 :: Parser LogicExp+> parseExp4 = try $ do+> string "~"+> x <- parseExp4+> return $ Not x+> <|> (try $ do+> p <- upper+> xs <- parsePredicateLetters+> return $ Predicate p xs)+> <|> do+> char '('+> x <- parseExp1+> char ')'+> return $ x+ +> parsePredicateLetters :: Parser ([Letter])+> parsePredicateLetters+> = try $ do+> x <- oneOf "abcefghijklmnopqrst"+> xs <- parsePredicateLetters +> return ((Name x):xs)+> <|> (try $ do+> x <- oneOf "uvwxyz"+> xs <- parsePredicateLetters +> return ((Variable x):xs))+> <|> do+> return []++> parseArg :: Parser [LogicExp]+> parseArg = try $ do+> xs <- parseArg'+> return xs+> <|> do +> x <- parseExp1+> spaces+> xs <- parseArg'+> return $ x : xs++> parseArg' :: Parser [LogicExp]+> parseArg' = try $ do+> string "|-"+> spaces+> x <- parseExp1+> return [x]+> <|> do +> char ','+> spaces+> x <- parseExp1+> spaces+> xs <- parseArg'+> return $ x : xs