diff options
Diffstat (limited to 'Logic.icl')
| -rw-r--r-- | Logic.icl | 92 |
1 files changed, 89 insertions, 3 deletions
@@ -1,6 +1,6 @@ implementation module Logic -import StdEnv +import StdEnv, StringUtils isBool :: Expr -> Bool isBool (B _) = True @@ -41,6 +41,15 @@ isEquiv :: Expr -> Bool isEquiv (App2 _ Equiv _) = True isEquiv _ = False +apply1 :: Op1 Bool -> Bool +apply1 Not b = not b + +apply2 :: Bool Op2 Bool -> Bool +apply2 x And y = x && y +apply2 x Or y = x || y +apply2 x Impl y = y || not x +apply2 x Equiv y = x == y + instance toString Op1 where toString Not = "~" @@ -54,8 +63,7 @@ where instance toString Expr where - toString (B True) = toString 1 - toString (B False) = toString 0 + toString (B b) = toString b toString (Atom a) = toString a toString (App1 op e) | needs_parentheses (App1 op e) = toString op +++ "(" +++ toString e +++ ")" @@ -97,3 +105,81 @@ binds_stronger Impl _ = True binds_stronger _ Impl = False binds_stronger Equiv Equiv = True +all_atoms :: Expr -> [AtomName] +all_atoms (Atom a) = [a] +all_atoms (B _) = [] +all_atoms (App1 _ e) = all_atoms e +all_atoms (App2 e1 _ e2) = removeDup (all_atoms e1 ++ all_atoms e2) + +all_atom_options :: Expr -> [[AtomOption]] +all_atom_options e = [opt \\ opt <- all_options (all_atoms e) []] +where + all_options :: [AtomName] [AtomOption] -> [[AtomOption]] + all_options [] opts = [opts] + all_options [a:as] opts = all_options as (opts ++ [(a,False)]) ++ all_options as (opts ++ [(a,True)]) + +substitute :: AtomOption Expr -> Expr +substitute (a,b) (Atom a`) +| a == a` = B b +| otherwise = Atom a` +substitute (a,b) (App1 op e) = App1 op (substitute (a,b) e) +substitute (a,b) (App2 e1 op e2) = App2 (substitute (a,b) e1) op (substitute (a,b) e2) +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] +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 + + + + + + + + + + + + + + + + + + + + + + + + |