diff options
| -rw-r--r-- | Logic.dcl | 38 | ||||
| -rw-r--r-- | Logic.icl | 101 | ||||
| -rw-r--r-- | LogicParser.icl | 18 |
3 files changed, 157 insertions, 0 deletions
diff --git a/Logic.dcl b/Logic.dcl new file mode 100644 index 0000000..767990f --- /dev/null +++ b/Logic.dcl @@ -0,0 +1,38 @@ +definition module Logic + +import StdEnv + +// Expressions +:: Expr = B Bool // A constant + | Atom AtomName // An atomic expression + | App1 Op1 Expr // Applying an Op1 on an expression + | App2 Expr Op2 Expr // Applying an Op2 on two expressions + +// Operators with one argument +:: Op1 = Not // logical not + +// Operators with two arguments +:: Op2 = And // logical and; left-associative + | Or // logical or; right-associative + | Impl // material implication; right-associative + | Equiv // equivalence; right-associative + +// All Chars may be used, but typically only [a-zA-Z] are used +:: AtomName :== Char + +isBool :: Expr -> Bool +isAtom :: Expr -> Bool +isApp1 :: Expr -> Bool +isApp2 :: Expr -> Bool +isApp :: Expr -> Bool + +isNot :: Expr -> Bool +isAnd :: Expr -> Bool +isOr :: Expr -> Bool +isImpl :: Expr -> Bool +isEquiv :: Expr -> Bool + +instance toString Op1 +instance toString Op2 +instance toString Expr + diff --git a/Logic.icl b/Logic.icl new file mode 100644 index 0000000..0276305 --- /dev/null +++ b/Logic.icl @@ -0,0 +1,101 @@ +implementation module Logic + +import StdEnv + +isBool :: Expr -> Bool +isBool (B _) = True +isBool _ = False + +isAtom :: Expr -> Bool +isAtom (Atom _) = True +isAtom _ = False + +isApp1 :: Expr -> Bool +isApp1 (App1 _ _) = True +isApp1 _ = False + +isApp2 :: Expr -> Bool +isApp2 (App2 _ _ _) = True +isApp2 _ = False + +isApp :: Expr -> Bool +isApp e = isApp1 e || isApp2 e + +isNot :: Expr -> Bool +isNot (App1 Not _) = True +isNot _ = False + +isAnd :: Expr -> Bool +isAnd (App2 _ And _) = True +isAnd _ = False + +isOr :: Expr -> Bool +isOr (App2 _ Or _) = True +isOr _ = False + +isImpl :: Expr -> Bool +isImpl (App2 _ Impl _) = True +isImpl _ = False + +isEquiv :: Expr -> Bool +isEquiv (App2 _ Equiv _) = True +isEquiv _ = False + +instance toString Op1 +where + toString Not = "~" + +instance toString Op2 +where + toString And = "&" + toString Or = "|" + toString Impl = "->" + toString Equiv = "<->" + +instance toString Expr +where + toString (B True) = toString 1 + toString (B False) = toString 0 + toString (Atom a) = toString a + toString (App1 op e) + | needs_parentheses (App1 op e) = toString op +++ "(" +++ toString e +++ ")" + | otherwise = toString op +++ toString e + toString (App2 e1 op e2) = e1` +++ " " +++ toString op +++ " " +++ e2` + where + e1` + | needs_parentheses_left (App2 e1 op e2) = "(" +++ toString e1 +++ ")" + | otherwise = toString e1 + e2` + | needs_parentheses_right (App2 e1 op e2) = "(" +++ toString e2 +++ ")" + | otherwise = toString e2 + +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 + +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 + +needs_parentheses_right :: Expr -> Bool +needs_parentheses_right (App2 _ _ (B _)) = False +needs_parentheses_right (App2 _ _ (Atom _)) = False +needs_parentheses_right (App2 _ _ (App1 Not _)) = False +needs_parentheses_right (App2 _ op1 (App2 _ op2 _)) = binds_stronger op1 op2 + +// Associativity rules +binds_stronger :: Op2 Op2 -> Bool +binds_stronger And _ = True // And is left-associative +binds_stronger _ And = False +binds_stronger Or Or = False // All others are right-associative +binds_stronger Or _ = True +binds_stronger _ Or = False +binds_stronger Impl Impl = False +binds_stronger Impl _ = True +binds_stronger _ Impl = False +binds_stronger Equiv Equiv = False + diff --git a/LogicParser.icl b/LogicParser.icl new file mode 100644 index 0000000..ef81237 --- /dev/null +++ b/LogicParser.icl @@ -0,0 +1,18 @@ +module LogicParser + +import Logic + +e1 = Atom 'p' +e2 = Atom 'q' +e3 = App1 Not e1 +e4 = App2 e1 And e2 +e5 = App2 e3 Or e2 +e6 = App2 e3 Impl e3 +e7 = App2 e4 Equiv e5 + +e8 = App2 (App2 (Atom 'p') And (Atom 'q')) Impl (Atom 'q') +e9 = App2 (Atom 'p') And (App2 (Atom 'q') Impl (Atom 'q')) + +exprs = [e1,e2,e3,e4,e5,e6,e7,e8,e9] + +Start = map toString exprs |