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
|
structure Wff : WFF =
struct
datatype wff = FALSE | TRUE | VAR of string
| AND of wff * wff
| OR of wff * wff
| NOT of wff
fun simplify e =
Generic.rewrite(
let include "wff.sig"
fun wff (NOT FALSE) = TRUE
| wff (NOT TRUE) = FALSE
| wff (NOT(NOT x)) = x
| wff (AND(TRUE,x)) = x
| wff (AND(x,TRUE)) = x
| wff (AND(FALSE,x)) = FALSE
| wff (AND(x,FALSE)) = FALSE
| wff (OR(TRUE,x)) = TRUE
| wff (OR(x,TRUE)) = TRUE
| wff (OR(FALSE,x)) = x
| wff (OR(x,FALSE)) = x
in rewrite'wff e
end
)
fun countNots e =
let val count = ref 0
in Generic.app(
let include "wff.sig"
fun wff (NOT _) = count := !count + 1
| wff _ = ()
in app'wff e;
!count
end
)
end
fun countNots2 e =
Generic.fold(
let include "wff.sig"
fun wff (NOT _, n) = n+1
| wff (_, n) = n
in fold'wff(e, 0)
end
)
fun allVars e =
Generic.fold(
let include "wff.sig"
fun wff (VAR v, vs) = v::vs | wff (_, vs) = vs
in fold'wff(e, [])
end)
end
|