diff options
Diffstat (limited to 'Logic.icl')
| -rw-r--r-- | Logic.icl | 430 |
1 files changed, 216 insertions, 214 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 |