1 files changed, 101 insertions, 0 deletions
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
+