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
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
|
implementation module Logic
import StdEnv, StringUtils
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
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 = "~"
instance toString Op2
where
toString And = "&"
toString Or = "|"
toString Impl = "->"
toString Equiv = "<->"
instance toString Expr
where
toString (B b) = toString b
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
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]
where
row_b = " " // Row / Line begin, end, separator
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
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
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
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 _ = []
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}
|
