blob: 5d5fc261a9008840c1909fd08dd0dd1f3bb401bc (
plain) (
blame)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
|
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 _)) = not (binds_stronger op2 op1)
// Associativity rules
binds_stronger :: Op2 Op2 -> Bool
binds_stronger _ And = False // And is left-associative
binds_stronger And _ = True
binds_stronger Or _ = True // The rest is right-associative
binds_stronger _ Or = False
binds_stronger Impl _ = True
binds_stronger _ Impl = False
binds_stronger Equiv Equiv = True
|
