diff options
Diffstat (limited to 'Logic.icl')
| -rw-r--r-- | Logic.icl | 119 |
1 files changed, 102 insertions, 17 deletions
@@ -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 + |