diff options
| -rw-r--r-- | Logic.dcl | 10 | ||||
| -rw-r--r-- | Logic.icl | 119 | ||||
| -rw-r--r-- | LogicParser.icl | 34 | ||||
| -rw-r--r-- | README.md | 2 | ||||
| -rw-r--r-- | StringUtils.dcl | 11 | ||||
| -rw-r--r-- | StringUtils.icl | 22 |
6 files changed, 166 insertions, 32 deletions
@@ -65,12 +65,12 @@ instance toString Op2 instance toString Expr instance toString TruthTable -instance == Op1 -instance < Op1 +instance == Op1 +instance < Op1 // Maybe useful later if more unary operators are added instance == Op2 -instance < Op2 +instance < Op2 // To sort by precedence instance == Expr -instance < Expr // To sort by unrigorous 'complexity'; e.g. in truthtables +instance < Expr // To sort by unrigorous 'complexity'; e.g. in truthtables binds_stronger :: Op2 Op2 -> Bool // True iff arg1 stronger binds than arg2 @@ -87,3 +87,5 @@ sorted_subexprs :: (Expr -> [Expr]) // Similar, but roughly sorted by co simple_truthtable :: Expr -> TruthTable // Simple truthtable: only the atomic expression and the expression itself truthtable :: Expr -> TruthTable // Truthtable from an expression +parse :: String -> Expr // Parse a string into an expression + @@ -103,9 +103,9 @@ where instance toString TruthTable where toString t=:{exprs,options} - = row_b +++ join row_s [pad_right head len \\ head <- map toString exprs & len <- padlens] +++ row_e +++ + = row_b +++ join row_s [pad_right ' ' head len \\ head <- map toString exprs & len <- padlens] +++ row_e +++ line_b +++ join line_s [toString (repeatn len '-') \\ len <- padlens] +++ line_e +++ - foldr (+++) "" [row_b +++ join row_s [pad_right (toStringOrEmpty val) len \\ val <- map (eval o substitute_all options`) exprs & len <- padlens] +++ row_e \\ options` <- options] + foldr (+++) "" [row_b +++ join row_s [pad_right ' ' (toStringOrEmpty val) len \\ val <- map (eval o substitute_all options`) exprs & len <- padlens] +++ row_e \\ options` <- options] where row_b = " " // Row / Line begin, end, separator row_e = " \n" @@ -171,28 +171,27 @@ where comp (Atom a) (Atom b) = a < b comp (Atom _) _ = True comp _ (Atom _) = False - comp (App1 _ e) (App1 _ e`) = e < e` - comp (App1 _ _) _ = True - comp _ (App1 _ _) = False - comp (App2 e1 op e2) (App2 e1` op` e2`) - | e1 < e1` = True - | e1` < e1 = False - | e2 < e2` = True - | e2` < e2 = False - | otherwise = op < op` + comp (App1 Not e) (App1 Not e`) = e < e` + comp e1 e2 + | isMember e1 (subexprs e2) = True + | isMember e2 (subexprs e1) = False + | otherwise = strlen (toString e1) < strlen (toString e2) +// Does a the argument of a unary operator need parentheses? needs_parentheses :: Expr -> Bool needs_parentheses (App1 Not (B _)) = False needs_parentheses (App1 Not (Atom _)) = False needs_parentheses (App1 Not (App1 Not _)) = False needs_parentheses _ = True +// Does the first argument of a binary operator need parentheses? needs_parentheses_left :: Expr -> Bool needs_parentheses_left (App2 (B _) _ _) = False needs_parentheses_left (App2 (Atom _) _ _) = False needs_parentheses_left (App2 (App1 Not _) _ _) = False needs_parentheses_left (App2 (App2 _ op1 _) op2 _) = binds_stronger op2 op1 +// Does the second argument of a binary operator need parentheses? needs_parentheses_right :: Expr -> Bool needs_parentheses_right (App2 _ _ (B _)) = False needs_parentheses_right (App2 _ _ (Atom _)) = False @@ -233,12 +232,6 @@ substitute _ e = e substitute_all :: [AtomOption] Expr -> Expr substitute_all opts e = foldr substitute e opts -contains_atoms :: Expr -> Bool -contains_atoms (B _) = False -contains_atoms (Atom _) = True -contains_atoms (App1 _ e) = contains_atoms e -contains_atoms (App2 e1 _ e2) = contains_atoms e1 || contains_atoms e2 - eval :: Expr -> [Bool] eval (B b) = [b] eval (App1 op e) = [apply1 op e` \\ e` <- eval e] @@ -260,3 +253,95 @@ simple_truthtable e = {exprs = [Atom a \\ a <- all_atoms e] ++ [e], options = al truthtable :: Expr -> TruthTable truthtable e = {exprs = sorted_subexprs e ++ [e], options = all_atom_options e} +NOT :== '~' +AND :== '&' +OR :== '|' +IMPL :== '>' +EQUIV :== '=' + +parse :: String -> Expr +parse s = parse_stack (shunting_yard (prep s) [] []) +where + // Make sure every token is ONE character by replacing <-> and -> + // Remove whitespace + prep :: String -> [Char] + prep s + # s = repl "<->" EQUIV s + # s = repl "->" IMPL s + # cs = fromString s + # cs = removeAll ' ' cs + = cs + where + removeAll c cs + | isMember c cs = removeAll c (removeMember c cs) + | otherwise = cs + + // The shunting yard algorithm for propositional logic; see https://en.wikipedia.org/wiki/Shunting-yard_algorithm + shunting_yard :: [Char] [Char] [Char] -> [Char] + shunting_yard [] output [] = output + shunting_yard [] output ['(':_] = abort "Mismatched parentheses" + shunting_yard [] output [')':_] = abort "Mismatched parentheses" + shunting_yard [] output [op:operators] = shunting_yard [] (output ++ [op]) operators + shunting_yard ['(':input] output operators = shunting_yard input output ['(':operators] + shunting_yard [')':input] output ['(':operators] = shunting_yard input output operators + shunting_yard [')':input] output [op:operators] = shunting_yard [')':input] (output ++ [op]) operators + shunting_yard [NOT:input] output operators = shunting_yard input output [NOT:operators] + shunting_yard [AND:input] output operators + | not (isEmpty operators) && (hd operators == NOT || hd operators == AND) = shunting_yard [AND:input] (output ++ [hd operators]) (tl operators) + | otherwise = shunting_yard input output [AND:operators] + shunting_yard [OR:input] output operators + | not (isEmpty operators) && (hd operators == NOT || hd operators == AND) = shunting_yard [OR:input] (output ++ [hd operators]) (tl operators) + | otherwise = shunting_yard input output [OR:operators] + shunting_yard [IMPL:input] output operators + | not (isEmpty operators) && (hd operators == NOT || hd operators == AND || hd operators == OR) = shunting_yard [IMPL:input] (output ++ [hd operators]) (tl operators) + | otherwise = shunting_yard input output [IMPL:operators] + shunting_yard [EQUIV:input] output operators + | not (isEmpty operators) && (hd operators == NOT || hd operators == AND || hd operators == OR || hd operators == IMPL) = shunting_yard [EQUIV:input] (output ++ [hd operators]) (tl operators) + | otherwise = shunting_yard input output [EQUIV:operators] + shunting_yard [ip:input] output operators + | cIsAtom [ip] || cIsBool [ip] = shunting_yard input (output ++ [ip]) operators + | otherwise = abort ("Unknown character " +++ toString ip) + + // Parse the outcome of the shunting yard algorithm into one expression + parse_stack :: [Char] -> Expr + parse_stack [] = abort "Cannot parse: empty input" + parse_stack cs = parse_stack` cs [] + where + parse_stack` :: [Char] [Expr] -> Expr + parse_stack` [] [e] = e + parse_stack` [] [] = abort "Cannot parse: not enough expressoins on the stack" + parse_stack` [] es = abort ("Cannot parse: too many expressions on the stack:\n" +++ join "\n" (map toString es) +++ "\n") + parse_stack` [AND:st] [e1:[e2:es]] = parse_stack` st [App2 e2 And e1:es] + parse_stack` [OR:st] [e1:[e2:es]] = parse_stack` st [App2 e2 Or e1:es] + parse_stack` [IMPL:st] [e1:[e2:es]] = parse_stack` st [App2 e2 Impl e1:es] + parse_stack` [EQUIV:st] [e1:[e2:es]] = parse_stack` st [App2 e2 Equiv e1:es] + parse_stack` [NOT:st] [e:es] = parse_stack` st [App1 Not e:es] + parse_stack` [c:st] es + | cIsAtom [c] = parse_stack` st [Atom (cToAtom [c]) : es] + | cIsBool [c] = parse_stack` st [B (cToBool [c]) : es] + parse_stack` [c:st] es = abort ("Cannot parse: tried to perform an operation (" +++ toString c +++ ") with too few expressions on the stack:\n" +++ join "," (map toString es) +++ "\n") + + cIsOp :: [Char] -> Bool + cIsOp ['~'] = True + cIsOp ['&'] = True + cIsOp ['|'] = True + cIsOp ['->'] = True + cIsOp ['<->'] = True + cIsOp _ = False + + cIsAtom :: [Char] -> Bool + cIsAtom [c] = 'a' <= c && c <= 'z' || 'A' <= c && c <= 'Z' + cIsAtom _ = False + + cToAtom :: [Char] -> AtomName + cToAtom [c:cs] = c + + cIsBool :: [Char] -> Bool + cIsBool ['1'] = True + cIsBool ['0'] = True + cIsBool _ = False + + cToBool :: [Char] -> Bool + cToBool ['1'] = True + cToBool _ = False + diff --git a/LogicParser.icl b/LogicParser.icl new file mode 100644 index 0000000..b25b0e5 --- /dev/null +++ b/LogicParser.icl @@ -0,0 +1,34 @@ +/** + * The MIT License (MIT) + * + * Copyright (c) 2015 Camil Staps + * + * Permission is hereby granted, free of charge, to any person obtaining a copy + * of this software and associated documentation files (the "Software"), to deal + * in the Software without restriction, including without limitation the rights + * to use, copy, modify, merge, publish, distribute, sublicense, and/or sell + * copies of the Software, and to permit persons to whom the Software is + * furnished to do so, subject to the following conditions: + * + * The above copyright notice and this permission notice shall be included in all + * copies or substantial portions of the Software. + * + * THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR + * IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY, + * FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL THE + * AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER + * LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, + * OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE + * SOFTWARE. + */ +module LogicParser + +import StdEnv, StdMaybe, ArgEnv, Logic + +Start +| argc <> 1 = abort ("Usage: " +++ argv.[0] +++ " -b -nt <string>\n") +| otherwise = toString (truthtable (parse argv.[1])) +where + argc = size argv - 1 + argv = getCommandLine + @@ -97,7 +97,7 @@ The `truthtable` of `e15`: ## Future ideas - * Different `toString` formats for operators: HTML (`¬`), UTF-8 (¬) + * Different `toString` formats for operators: HTML (`¬`), UTF-8 (¬), LaTeX (`\neg`) * Different `toString` formats for booleans: `0` and `1` or `T` and `F` instead of `True` and `False` * Simplifying expressions with atomic expressions as far as possible * Testing equivalence or impliance of expressions with atomic expressions diff --git a/StringUtils.dcl b/StringUtils.dcl index e7255fb..5593c4c 100644 --- a/StringUtils.dcl +++ b/StringUtils.dcl @@ -25,10 +25,13 @@ definition module StringUtils import StdEnv -strlen :: String -> Int +strlen :: String -> Int // Length of a String -pad_right :: String Int -> String -pad_left :: String Int -> String +pad_right :: Char String Int -> String // Pad a String with Chars up to a length +pad_left :: Char String Int -> String // Similar, but pad on the left -join :: String [String] -> String +join :: String [String] -> String // Join a [String] with a String glue + +// Replace every occurence of @a in @c with @b +repl :: a b c -> String | toString a & toString b & toString c diff --git a/StringUtils.icl b/StringUtils.icl index e2b7c3e..811b3d2 100644 --- a/StringUtils.icl +++ b/StringUtils.icl @@ -31,18 +31,28 @@ where s` :: [Char] s` = fromString s -pad_right :: String Int -> String -pad_right s l +pad_right :: Char String Int -> String +pad_right c s l | strlen s >= l = s -| otherwise = s +++ toString (repeatn (l - strlen s) ' ') +| otherwise = s +++ toString (repeatn (l - strlen s) c) -pad_left :: String Int -> String -pad_left s l +pad_left :: Char String Int -> String +pad_left c s l | strlen s >= l = s -| otherwise = toString (repeatn (l - strlen s) ' ') +++ s +| otherwise = toString (repeatn (l - strlen s) c) +++ s join :: String [String] -> String join glue [] = "" join glue [s] = s join glue [s:ss] = s +++ glue +++ join glue ss +repl :: a b c -> String | toString a & toString b & toString c +repl needle replment haystack +| strlen needle` > strlen haystack` = haystack` +| needle` == haystack` % (0,strlen needle` - 1) = replment` +++ repl needle` replment` (haystack` % (strlen needle`, strlen haystack` - 1)) +| otherwise = (haystack` % (0,0)) +++ repl needle` replment` (haystack` % (1, strlen haystack` - 1)) +where + needle` = toString needle + replment` = toString replment + haystack` = toString haystack + |