diff options
| -rw-r--r-- | Logic.icl | 430 | ||||
| -rw-r--r-- | LogicParser.icl | 19 | ||||
| -rw-r--r-- | LogicTest.icl | 2 | ||||
| -rw-r--r-- | README.md | 131 |
4 files changed, 310 insertions, 272 deletions
@@ -52,7 +52,7 @@ isAnd :: Expr -> Bool isAnd (App2 _ And _) = True isAnd _ = False -isOr :: Expr -> Bool +isOr :: Expr -> Bool isOr (App2 _ Or _) = True isOr _ = False @@ -75,118 +75,118 @@ apply2 x Equiv y = x == y instance == OutputOption where - (==) Plain Plain = True - (==) Html Html = True - (==) LaTeX LaTeX = True - (==) _ _ = False + (==) Plain Plain = True + (==) Html Html = True + (==) LaTeX LaTeX = True + (==) _ _ = False instance show Bool where - show LaTeX True = "\\top" - show LaTeX False = "\\bot" - show _ b = toString b + show LaTeX True = "\\top" + show LaTeX False = "\\bot" + show _ b = toString b instance show Char where - show LaTeX c = " " +++ toString c - show _ c = toString c + show LaTeX c = " " +++ toString c + show _ c = toString c instance show Op1 where - show Plain Not = "~" - show Html Not = "¬" - show LaTeX Not = "\\neg" + show Plain Not = "~" + show Html Not = "¬" + show LaTeX Not = "\\neg" instance show Op2 where - show Plain And = "&" - show Plain Or = "|" - show Plain Impl = "->" - show Plain Equiv = "<->" - show Html And = "∧" - show Html Or = "∨" - show Html Impl = "→" - show Html Equiv = "↔" - show LaTeX And = "\\land" - show LaTeX Or = "\\lor" - show LaTeX Impl = "\\rightarrow" - show LaTeX Equiv = "\\leftrightarrow" + show Plain And = "&" + show Plain Or = "|" + show Plain Impl = "->" + show Plain Equiv = "<->" + show Html And = "∧" + show Html Or = "∨" + show Html Impl = "→" + show Html Equiv = "↔" + show LaTeX And = "\\land" + show LaTeX Or = "\\lor" + show LaTeX Impl = "\\rightarrow" + show LaTeX Equiv = "\\leftrightarrow" instance show Expr where - show opt (B b) = show opt b - show opt (Atom a) = show opt a - show opt (App1 op (App2 x y z)) = show opt op +++ "(" +++ show opt (App2 x y z) +++ ")" - show opt (App1 op e) = show opt op +++ show opt e - show opt (App2 e1 op e2) = if needs_l "(" "" +++ - show opt e1 +++ - if needs_l ")" "" +++ - " " +++ show opt op +++ " " +++ - if needs_r "(" "" +++ - show opt e2 +++ - if needs_r ")" "" - where - needs_l = needs_parentheses_left (App2 e1 op e2) - needs_r = needs_parentheses_right (App2 e1 op e2) + show opt (B b) = show opt b + show opt (Atom a) = show opt a + show opt (App1 op (App2 x y z)) = show opt op +++ "(" +++ show opt (App2 x y z) +++ ")" + show opt (App1 op e) = show opt op +++ show opt e + show opt (App2 e1 op e2) = if needs_l "(" "" +++ + show opt e1 +++ + if needs_l ")" "" +++ + " " +++ show opt op +++ " " +++ + if needs_r "(" "" +++ + show opt e2 +++ + if needs_r ")" "" + where + needs_l = needs_parentheses_left (App2 e1 op e2) + needs_r = needs_parentheses_right (App2 e1 op e2) instance == Op1 where - (==) Not Not = True + (==) Not Not = True instance < Op1 where - (<) Not Not = False + (<) Not Not = False instance == Op2 where - (==) And And = True - (==) Or Or = True - (==) Impl Impl = True - (==) Equiv Equiv = True - (==) _ _ = False + (==) And And = True + (==) Or Or = True + (==) Impl Impl = True + (==) Equiv Equiv = True + (==) _ _ = False instance < Op2 where - (<) op1 op2 - | op1 == op2 = False - | otherwise = comp op1 op2 - where - comp And And = False - comp And _ = True - comp _ And = False - comp Or Or = False - comp Or _ = True - comp _ Or = False - comp Impl Impl = False - comp Impl _ = True - comp Equiv Equiv = False + (<) op1 op2 + | op1 == op2 = False + | otherwise = comp op1 op2 + where + comp And And = False + comp And _ = True + comp _ And = False + comp Or Or = False + comp Or _ = True + comp _ Or = False + comp Impl Impl = False + comp Impl _ = True + comp Equiv Equiv = False instance == Expr where - (==) (B b1) (B b2) = b1 == b2 - (==) (Atom a1) (Atom a2) = a1 == a2 - (==) (App1 op e) (App1 op` e`) = op == op` && e == e` - (==) (App2 e1 op e2) (App2 e1` op` e2`) = e1 == e1` && op == op` && e2 == e2` - (==) _ _ = False + (==) (B b1) (B b2) = b1 == b2 + (==) (Atom a1) (Atom a2) = a1 == a2 + (==) (App1 op e) (App1 op` e`) = op == op` && e == e` + (==) (App2 e1 op e2) (App2 e1` op` e2`) = e1 == e1` && op == op` && e2 == e2` + (==) _ _ = False instance < Expr where - (<) e1 e2 - | e1 == e2 = False - | otherwise = comp e1 e2 - where - comp (B False) _ = True - comp _ (B False) = False - comp (B _) _ = True - comp _ (B _) = False - comp (Atom a) (Atom b) = a < b - comp (Atom _) _ = True - comp _ (Atom _) = False - comp (App1 Not e) (App1 Not e`) = e < e` - comp e1 e2 - | isMember e1 (subexprs e2) = True - | isMember e2 (subexprs e1) = False - | otherwise = strlen (show Plain e1) < strlen (show Plain e2) + (<) e1 e2 + | e1 == e2 = False + | otherwise = comp e1 e2 + where + comp (B False) _ = True + comp _ (B False) = False + comp (B _) _ = True + comp _ (B _) = False + comp (Atom a) (Atom b) = a < b + comp (Atom _) _ = True + comp _ (Atom _) = False + comp (App1 Not e) (App1 Not e`) = e < e` + comp e1 e2 + | isMember e1 (subexprs e2) = True + | isMember e2 (subexprs e1) = False + | otherwise = strlen (show Plain e1) < strlen (show Plain e2) // Does a the argument of a unary operator need parentheses? needs_parentheses :: Expr -> Bool @@ -211,9 +211,9 @@ needs_parentheses_right (App2 _ op1 (App2 _ op2 _)) = not (binds_stronger op2 op // Associativity rules binds_stronger :: Op2 Op2 -> Bool -binds_stronger _ And = False // And is left-associative +binds_stronger _ And = False // And is left-associative binds_stronger And _ = True -binds_stronger Or _ = True // The rest is right-associative +binds_stronger Or _ = True // The rest is right-associative binds_stronger _ Or = False binds_stronger Impl _ = True binds_stronger _ Impl = False @@ -228,10 +228,10 @@ all_atoms (App2 e1 _ e2) = removeDup (all_atoms e1 ++ all_atoms e2) all_atom_options :: Expr -> [[AtomOption]] all_atom_options e = removeDup [opt \\ opt <- all_opts (sort (all_atoms e)) []] where - all_opts :: [AtomName] [AtomOption] -> [[AtomOption]] - all_opts [] opts = [opts] - all_opts [a:as] opts - = all_opts as (opts ++ [(a,False)]) ++ all_opts as (opts ++ [(a,True)]) + all_opts :: [AtomName] [AtomOption] -> [[AtomOption]] + all_opts [] opts = [opts] + all_opts [a:as] opts + = all_opts as (opts ++ [(a,False)]) ++ all_opts as (opts ++ [(a,True)]) substitute :: AtomOption Expr -> Expr substitute (a,b) (Atom a`) @@ -269,143 +269,145 @@ truthtable :: Expr -> TruthTable truthtable e = {exprs = sorted_subexprs e ++ [e], options = all_atom_options e} truthtable_n :: [Expr] -> TruthTable -truthtable_n es = {exprs = sort (removeDup (flatten ([[e:subexprs e] \\ e <- es]))), options = removeDup (flatten (map all_atom_options es))} +truthtable_n es = {exprs = sort (removeDup (flatten ([[e:subexprs e] \\ e <- es]))), options = removeSubOptions (flatten (map all_atom_options es))} +where + removeSubOptions :: [[AtomOption]] -> [[AtomOption]] + removeSubOptions opts = filter (\this -> not (any (\that -> all (flip isMember that) this) (removeMember this opts))) opts compute :: TruthTable -> FilledTruthTable // Fill in a truthtable compute table=:{exprs,options} = {table=table, values=values} where - values = [[toMaybeBool val \\ val <- map (eval o substitute_all options`) exprs] \\ options` <- options] - toMaybeBool [] = Nothing - toMaybeBool [b:bs] = Just b + values = [map (toMaybeBool o eval o substitute_all options`) exprs \\ options` <- options] + toMaybeBool [] = Nothing + toMaybeBool [b:_] = Just b instance show FilledTruthTable where - show :: OutputOption FilledTruthTable -> String - show opt t=:{table=table=:{exprs,options},values} - = begin +++ - head_b +++ - join head_s [pad_right (showOrNot head_i) header len \\ header <- map (show opt) exprs & len <- padlens] +++ - head_e +++ - line_b +++ - join line_s [foldr (+++) "" (repeatn len (showOrNot line_i)) \\ len <- padlens] +++ - line_e +++ - foldr (+++) "" [row_b +++ join row_s [pad_right (showOrNot row_i) (showOrNot v) len \\ v <- r & len <- padlens] +++ row_e \\ r <- values] +++ - end - where - padlens = map ((\l . maxList (map strlen [l,show opt True,show opt False])) o (show opt)) exprs - // Ideally, we would some kind of DOM writer for Html, but for this project this is sufficient (although not very readable) - (begin,end) = gen - gen - | opt == Plain = ("","") - | opt == Html = ("<table>", "</tbody></table>") - | opt == LaTeX = ("\\begin{tabular}{" +++ join "|" (repeatn (length exprs) "c") +++ "}", "\\end{tabular}") - (head_b,head_e,head_s,head_i) = head - head - | opt == Html = ("<thead><tr><th>", "</th></tr></thead><tbody>", "</th><th>", Nothing) - | otherwise = row - (row_b,row_e,row_s,row_i) = row - row - | opt == Plain = (" ", " \n", " | ", Just ' ') - | opt == Html = ("<tr><td>", "</td></tr>", "</td><td>", Nothing) - | opt == LaTeX = ("$", "$\\\\", "$&$", Nothing) - (line_b,line_e,line_s,line_i) = line - line - | opt == Plain = ("-", "-\n", "-+-", Just '-') - | opt == Html = ("", "", "", Nothing) - | opt == LaTeX = ("\\hline", "", "", Nothing) - showOrNot :: (Maybe a) -> String | show a - showOrNot Nothing = "" - showOrNot (Just a) = show opt a - -NOT :== '~' -AND :== '&' -OR :== '|' -IMPL :== '>' + show :: OutputOption FilledTruthTable -> String + show opt t=:{table=table=:{exprs,options},values} + = begin +++ + head_b +++ + join head_s [pad_right (showOrNot head_i) header len \\ header <- map (show opt) exprs & len <- padlens] +++ + head_e +++ + line_b +++ + join line_s [foldr (+++) "" (repeatn len (showOrNot line_i)) \\ len <- padlens] +++ + line_e +++ + foldr (+++) "" [row_b +++ join row_s [pad_right (showOrNot row_i) (showOrNot v) len \\ v <- r & len <- padlens] +++ row_e \\ r <- values] +++ + end + where + padlens = map ((\l . maxList (map strlen [l,show opt True,show opt False])) o (show opt)) exprs + // Ideally, we would some kind of DOM writer for Html, but for this project this is sufficient (although not very readable) + (begin,end) = gen + gen + | opt == Plain = ("","") + | opt == Html = ("<table>", "</tbody></table>") + | opt == LaTeX = ("\\begin{tabular}{" +++ join "|" (repeatn (length exprs) "c") +++ "}", "\\end{tabular}") + (head_b,head_e,head_s,head_i) = head + head + | opt == Html = ("<thead><tr><th>", "</th></tr></thead><tbody>", "</th><th>", Nothing) + | otherwise = row + (row_b,row_e,row_s,row_i) = row + row + | opt == Plain = (" ", " \n", " | ", Just ' ') + | opt == Html = ("<tr><td>", "</td></tr>", "</td><td>", Nothing) + | opt == LaTeX = ("$", "$\\\\", "$&$", Nothing) + (line_b,line_e,line_s,line_i) = line + line + | opt == Plain = ("-", "-\n", "-+-", Just '-') + | opt == Html = ("", "", "", Nothing) + | opt == LaTeX = ("\\hline", "", "", Nothing) + showOrNot :: (Maybe a) -> String | show a + showOrNot Nothing = "" + showOrNot (Just a) = show opt a + +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 (show Plain) 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 (" +++ show Plain c +++ ") with too few expressions on the stack:\n" +++ join "," (map (show Plain) 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 - + // 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 (show Plain) 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 (" +++ show Plain c +++ ") with too few expressions on the stack:\n" +++ join "," (map (show Plain) 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 index ab99abf..46ac605 100644 --- a/LogicParser.icl +++ b/LogicParser.icl @@ -30,15 +30,14 @@ Start | length (removeDup (foldr (++) [] (map all_atoms exprs))) > 8 = abort "You don't need more than 8 atomic expressions." | otherwise = show outputoption (compute (if extended truthtable_n simple_truthtable_n exprs)) where - argc = size argv - 1 - argv = getCommandLine + argc = size argv - 1 + argv = getCommandLine - exprs = map parse (filter (\s . s.[0] <> '-') [argv.[n] \\ n <- [1..argc]]) - - extended = hasArg "-e" - outputoption - | hasArg "-html" = Html - | hasArg "-latex" = LaTeX - | otherwise = Plain - hasArg arg = or [arg == argv.[n] \\ n <- [0..argc]] + exprs = map parse (filter (\s . s.[0] <> '-') [argv.[n] \\ n <- [1..argc]]) + extended = hasArg "-e" + outputoption + | hasArg "-html" = Html + | hasArg "-latex" = LaTeX + | otherwise = Plain + hasArg arg = or [arg == argv.[n] \\ n <- [0..argc]] diff --git a/LogicTest.icl b/LogicTest.icl index 6c13eb7..4113673 100644 --- a/LogicTest.icl +++ b/LogicTest.icl @@ -55,5 +55,5 @@ exprs_assoc = [e10,e11,e12,e13,e14,e15,e16,e17] //Start = map toString exprs_rand //Start = map toString exprs_assoc -Start = show Plain (compute (truthtable e15)) +Start = /*show Plain (compute*/ (truthtable_n [e1, e4])//) @@ -3,39 +3,49 @@ Logic toolbox in [Clean](http://wiki.clean.cs.ru.nl/Clean). Features include: * Straightforward types for (atomic) expressions, operators and truth tables - * `show` (`toString`-like) instances for all types that take care of associativity + * `show` (`toString`-like) instances for all types that take care of + associativity * Substituting atomic expressions for constants * Evaluating expressions without atomic expressions * Generating truth tables for expressions, possibly with intermediate steps * Displaying truth tables * Parsing strings to expressions - * A web frontend to access the Clean program through, so only server-side installation is necessary + * A web frontend to access the Clean program through, so only server-side + installation is necessary * Different output options (Plain / ASCII art, HTML, LaTeX) Read further for examples. ### Demo -A demo of the web frontend may be found on https://demo.camilstaps.nl/CleanLogic. +A demo of the web frontend may be found on +https://demo.camilstaps.nl/CleanLogic. ### License -This program and the example are distributed under the MIT license. For more details, see the LICENSE file. +This program and the example are distributed under the MIT license. For more +details, see the LICENSE file. ## Installation -Set `CLEAN_HOME` to your Clean installation directory. To install the parser and the example program: +Set `CLEAN_HOME` to your Clean installation directory. To install the parser +and the example program: - clm -I $CLEAN_HOME/lib/StdLib -I $CLEAN_HOME/lib/ArgEnv LogicParser -o LogicParser - clm -I $CLEAN_HOME/lib/StdLib -I $CLEAN_HOME/lib/ArgEnv LogicTest -o LogicTest +``` +make +``` ## Types ### Operators -There is one unary operator (`Op1`): `Not`. It binds stronger than all other operators. +There is one unary operator (`Op1`): `Not`. It binds stronger than all other +operators. -There are four binary operators (`Op2`). In order of descending precedence: `And`, `Or`, `Impl` and `Equiv`. `And` is considered left-associative; all others are considered right-associative. Associativity is only important in `toString` functions. `Expr` itself is an unambiguous recursive type. +There are four binary operators (`Op2`). In order of descending precedence: +`And`, `Or`, `Impl` and `Equiv`. `And` is considered left-associative; all +others are considered right-associative. Associativity is only important in +`toString` functions. `Expr` itself is an unambiguous recursive type. The operators are represented as: @@ -47,7 +57,9 @@ The operators are represented as: ### Expressions -Expressions are constants (`B Bool`), atomic expressions (`Atom Char`), or applications of operators on other expressions (`App1 Op1 Expr` or `App2 Expr Op2 Expr`). +Expressions are constants (`B Bool`), atomic expressions (`Atom Char`), or +applications of operators on other expressions (`App1 Op1 Expr` or `App2 Expr +Op2 Expr`). ### Examples @@ -77,19 +89,30 @@ Expressions are constants (`B Bool`), atomic expressions (`Atom Char`), or appli ## Substitution -You can substitute all occurences of `Atom a` in an `Expr e` by a `Bool b` with `substitute (a,b) e`. This yields a new `Expr`, in which all occurences have been replaced by the contstant `B b`. +You can substitute all occurrences of `Atom a` in an `Expr e` by a `Bool b` +with `substitute (a,b) e`. This yields a new `Expr`, in which all occurrences +have been replaced by the constant `B b`. -An alternative is `substitute_all`, which takes a list of tuples `(a :: AtomName, b :: Bool)` and substitutes all atomnames with the corresponding booleans. +An alternative is `substitute_all`, which takes a list of tuples `(a :: +AtomName, b :: Bool)` and substitutes all atomnames with the corresponding +booleans. ## Evaluation -An expression `e` **without atomic expressions** may be evaluated to its result by calling `eval e`. This yields the empty list `[]` if `e` *did* have atomic expressions, or a singleton `[b :: Bool]` with the result of the evaluation. +An expression `e` **without atomic expressions** may be evaluated to its result +by calling `eval e`. This yields the empty list `[]` if `e` *did* have atomic +expressions, or a singleton `[b :: Bool]` with the result of the evaluation. ## Truth tables -A `TruthTable` has a list of expressions `exprs` and a list of `options`, which has the type `[[(AtomName,Bool)]]` and describes all the options the truth table should list. +A `TruthTable` has a list of expressions `exprs` and a list of `options`, which +has the type `[[(AtomName,Bool)]]` and describes all the options the truth +table should list. -A simple truth table of an expression `e` contains only the atomic expressions in `e` and `e` itself. It may be built with `simple_truthtable e`. A more complex truth table lists all `e`'s subexpressions. In either table, the expressions are roughly sorted by complexity. +A simple truth table of an expression `e` contains only the atomic expressions +in `e` and `e` itself. It may be built with `simple_truthtable e`. A more +complex truth table lists all `e`'s subexpressions. In either table, the +expressions are roughly sorted by complexity. A truth table `table` can be shown with `toString table`. @@ -123,50 +146,64 @@ The `truthtable` of `e15`: ## Parsing -The `parse` function may be used to read an expression from a String. The following rules are used: +The `parse` function may be used to read an expression from a String. The +following rules are used: * Spaces are ignored. - * All latin letters (`[a-zA-Z]`) are considered atomic expressions + * All Latin letters (`[a-zA-Z]`) are considered atomic expressions * Operators are expected in their representation described above * True and False are expected as `1` and `0`, respectively * Unknown characters will throw an error -A usage example is found in `LogicParser.icl`. This file, once compiled, reads the command line arguments and shows their truth tables: - - $./LogicParser -b -nt -e "~~(((A | (A -> B)) -> B) -> B)" - A | B | A -> B | A | (A -> B) | A | (A -> B) -> B | (A | (A -> B) -> B) -> B | ~((A | (A -> B) -> B) -> B) | ~~((A | (A -> B) -> B) -> B) - -------+-------+--------+--------------+-------------------+--------------------------+-----------------------------+------------------------------ - False | False | True | True | False | True | False | True - False | True | True | True | True | True | False | True - True | False | False | True | False | True | False | True - True | True | True | True | True | True | False | True - -Here, `-b` and `-nt` are common Clean options to disable outputting basic values for constructors, and disable outputting execution times, respectively. - -The option `-e` tells the parser to show the extended truth table. With this option, only the first formula is considered. Without `-e`, multiple formulas may be given (possibly with different atomic expressions), and all will be evaluated in one table: - - $./LogicParser -b -nt "~~(((A | (A -> B)) -> B) -> B)" "A & B" - A | B | ~~((A | (A -> B) -> B) -> B) | A & B - -------+-------+------------------------------+------- - False | False | True | False - False | True | True | False - True | False | True | False - True | True | True | True - False | False | True | False - False | True | True | False - True | False | True | False - True | True | True | True - -The parsers also recognises `-html` and `-latex` and will output an HTML or LaTeX table if these arguments are present. +A usage example is found in `LogicParser.icl`. This file, once compiled, reads +the command line arguments and shows their truth tables: + +``` +$./LogicParser -e "~~(((A | (A -> B)) -> B) -> B)" + A | B | A -> B | A | (A -> B) | A | (A -> B) -> B | (A | (A -> B) -> B) -> B | ~((A | (A -> B) -> B) -> B) | ~~((A | (A -> B) -> B) -> B) +-------+-------+--------+--------------+-------------------+--------------------------+-----------------------------+------------------------------ + False | False | True | True | False | True | False | True + False | True | True | True | True | True | False | True + True | False | False | True | False | True | False | True + True | True | True | True | True | True | False | True +``` + +The option `-e` tells the parser to show the extended truth table. With this +option, only the first formula is considered. Without `-e`, multiple formulas +may be given (possibly with different atomic expressions), and all will be +evaluated in one table: + +``` +$./LogicParser -b -nt "~~(((A | (A -> B)) -> B) -> B)" "A & B" + A | B | ~~((A | (A -> B) -> B) -> B) | A & B +-------+-------+------------------------------+------- + False | False | True | False + False | True | True | False + True | False | True | False + True | True | True | True + False | False | True | False + False | True | True | False + True | False | True | False + True | True | True | True +``` + +The parsers also recognises `-html` and `-latex` and will output an HTML or +LaTeX table if these arguments are present. ## Web frontend -There is a simple web frontend in PHP and a basic HTML template which allows one to connect to the Clean application through his browser. The files for this are `index.html` and `request.php`, and a demo may be found on https://demo.camilstaps.nl/CleanLogic. For this to work, the `exec()` function should be enabled in your PHP configuration. +There is a simple web frontend in PHP and a basic HTML template which allows +one to connect to the Clean application through his browser. The files for this +are `index.html` and `request.php`, and a demo may be found on +https://demo.camilstaps.nl/CleanLogic. For this to work, the `exec()` function +should be enabled in your PHP configuration. ## Future ideas - * Different `toString` formats for booleans: `0` and `1` or `T` and `F` instead of `True` and `False` + * 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 * Add support for multi-letter atomic expressions - * Would it be easier / neater / more intuitive to get rid of `Op1` and `Op2` and use `Not`, `And`, etc. as type constructors of `Expr`? + * Would it be easier / neater / more intuitive to get rid of `Op1` and `Op2` + and use `Not`, `And`, etc. as type constructors of `Expr`? |