File: wff.gsml

package info (click to toggle)
mlton 20210117%2Bdfsg-3
  • links: PTS, VCS
  • area: main
  • in suites: sid
  • size: 58,464 kB
  • sloc: ansic: 27,682; sh: 4,455; asm: 3,569; lisp: 2,879; makefile: 2,347; perl: 1,169; python: 191; pascal: 68; javascript: 7
file content (55 lines) | stat: -rw-r--r-- 1,340 bytes parent folder | download | duplicates (5)
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