diff options
| -rw-r--r-- | Logic.dcl | 12 | ||||
| -rw-r--r-- | Logic.icl | 109 | ||||
| -rw-r--r-- | LogicTest.icl | 8 |
3 files changed, 107 insertions, 22 deletions
@@ -40,6 +40,14 @@ isEquiv :: Expr -> Bool instance toString Op1 instance toString Op2 instance toString Expr +instance toString TruthTable + +instance == Op1 +instance < Op1 +instance == Op2 +instance < Op2 +instance == Expr +instance < Expr // To sort by unrigorous 'complexity'; e.g. in truthtables binds_stronger :: Op2 Op2 -> Bool // True iff arg1 stronger binds than arg2 @@ -50,5 +58,7 @@ substitute :: AtomOption Expr -> Expr // Substitute all atomic expressions substitute_all :: [AtomOption] Expr -> Expr // Same, for multiple options eval :: Expr -> [Bool] // Evaluate to a simpler form -instance toString TruthTable +subexprs :: Expr -> [Expr] // Subexpressions of an expression +sorted_subexprs :: (Expr -> [Expr]) // Similar, but roughly sorted by complexity +truthtable :: Expr -> TruthTable // Truthtable from an expression @@ -77,6 +77,88 @@ where | needs_parentheses_right (App2 e1 op e2) = "(" +++ toString e2 +++ ")" | otherwise = toString e2 +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 +++ + 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 (+++) "" (map toString padlens) + where + row_b = " " + row_e = " \n" + row_s = " | " + line_b = "-" + line_e = "-\n" + line_s = "-+-" + padlens = map ((max 5) o strlen o toString) exprs + toStringOrEmpty :: [Bool] -> String + toStringOrEmpty [] = "" + toStringOrEmpty [b:bs] = toString b + +instance == Op1 +where + (==) Not Not = True + +instance < Op1 +where + (<) Not Not = False // this doesn't make much sense, but whatever + +instance == Op2 +where + (==) 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 + +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 + +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 _ 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` + needs_parentheses :: Expr -> Bool needs_parentheses (App1 Not (B _)) = False needs_parentheses (App1 Not (Atom _)) = False @@ -141,26 +223,17 @@ eval (App1 op e) = [apply1 op e` \\ e` <- eval e] eval (App2 e1 op e2) = [apply2 e1` op e2` \\ e1` <- eval e1 & e2` <- eval e2] eval _ = [] -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 +++ - 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 (+++) "" (map toString padlens) - where - row_b = " " - row_e = " \n" - row_s = " | " - line_b = "-" - line_e = "-\n" - line_s = "-+-" - padlens = map ((max 5) o strlen o toString) exprs - toStringOrEmpty :: [Bool] -> String - toStringOrEmpty [] = "" - toStringOrEmpty [b:bs] = toString b +subexprs :: Expr -> [Expr] +subexprs (B _) = [] +subexprs (Atom _) = [] +subexprs (App1 op e) = removeDup (subexprs e ++ [e]) +subexprs (App2 e1 op e2) = removeDup (subexprs e1 ++ subexprs e2 ++ [e1,e2]) +sorted_subexprs :: (Expr -> [Expr]) +sorted_subexprs = sort o subexprs +truthtable :: Expr -> TruthTable +truthtable e = {exprs = sorted_subexprs e ++ [e], options = all_atom_options e} diff --git a/LogicTest.icl b/LogicTest.icl index 4122b92..7f6f214 100644 --- a/LogicTest.icl +++ b/LogicTest.icl @@ -1,6 +1,6 @@ module LogicTest -import Logic +import Logic, StringUtils // Some random examples e1 = Atom 'p' @@ -35,6 +35,8 @@ exprs_assoc = [e10,e11,e12,e13,e14,e15,e16,e17] //Start = substitute ('q',True) e8 table = { exprs = exprs_rand ++ exprs_assoc, - options = all_atom_options e4 } + options = all_atom_options e10 } -Start = toString table +//Start = join ", " (map toString [e17 : subexprs e17]) + +Start = toString (truthtable (App2 e9 And e7)) |