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
|
(* WARNING: This file is generated using 'rwgen wff.gsml' *)
(*#line 1.2 "wff.gsml"*)
structure Wff : WFF = struct
(*#line 4.4 "wff.gsml"*)
datatype wff =
FALSE
| TRUE
| VAR of string
| AND of (wff * wff)
| OR of (wff * wff)
| NOT of wff
(*#line 9.4 "wff.gsml"*)
fun simplify e =
let fun rewrite'wff redex =
(case redex of
FALSE => redex
| TRUE => redex
| VAR string => redex
| AND(wff1, wff2) =>
(case (rewrite'wff wff1, rewrite'wff wff2) of
(TRUE, x) => x
| (x, TRUE) => x
| (FALSE, x) => FALSE
| (x, FALSE) => FALSE
| arg => AND arg
)
| OR(wff1, wff2) =>
(case (rewrite'wff wff1, rewrite'wff wff2) of
(TRUE, x) => TRUE
| (x, TRUE) => TRUE
| (FALSE, x) => x
| (x, FALSE) => x
| arg => OR arg
)
| NOT wff =>
(case rewrite'wff wff of
FALSE => TRUE
| TRUE => FALSE
| NOT x => x
| arg => NOT arg
)
)
in rewrite'wff e
end
(*#line 27.4 "wff.gsml"*)
fun countNots e =
let
(*#line 28.8 "wff.gsml"*)
val count = ref 0
in
let fun app'wff redex =
let val _ =
(case redex of
FALSE => ()
| TRUE => ()
| VAR string => ()
| AND(wff1, wff2) =>
( app'wff wff1;
app'wff wff2 )
| OR(wff1, wff2) =>
( app'wff wff1;
app'wff wff2 )
| NOT wff => app'wff wff
)
in
(case redex of
NOT _ => count := (( ! count) + 1)
| _ => ()
)
end
in app'wff e;
! count
end
end
(*#line 39.4 "wff.gsml"*)
fun countNots2 e =
let fun fold'wff (redex, foldArg) =
let val foldArg =
(case redex of
FALSE => foldArg
| TRUE => foldArg
| VAR string => foldArg
| AND(wff1, wff2) => fold'wff (wff2, fold'wff (wff1, foldArg))
| OR(wff1, wff2) => fold'wff (wff2, fold'wff (wff1, foldArg))
| NOT wff => fold'wff (wff, foldArg)
)
in
(case (redex, foldArg) of
(NOT _, n) => n + 1
| (_, n) => n
)
end
in fold'wff (e, 0)
end
(*#line 48.4 "wff.gsml"*)
fun allVars e =
let fun fold'wff (redex, foldArg) =
let val foldArg =
(case redex of
FALSE => foldArg
| TRUE => foldArg
| VAR string => foldArg
| AND(wff1, wff2) => fold'wff (wff2, fold'wff (wff1, foldArg))
| OR(wff1, wff2) => fold'wff (wff2, fold'wff (wff1, foldArg))
| NOT wff => fold'wff (wff, foldArg)
)
in
(case (redex, foldArg) of
(VAR v, vs) => v :: vs
| (_, vs) => vs
)
end
in fold'wff (e, [])
end
end
|
