File: boolean.mli

package info (click to toggle)
cduce 0.4.1-1
  • links: PTS
  • area: main
  • in suites: etch, etch-m68k
  • size: 2,836 kB
  • ctags: 3,143
  • sloc: ml: 20,402; xml: 5,376; makefile: 411; sh: 45
file content (39 lines) | stat: -rw-r--r-- 1,156 bytes parent folder | download | duplicates (6)
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
(* Implementation of boolean combination in disjunctive normal form (dnf).
   A dnf is a disjunction of lines, each line consisting of a 
   conjunction of atoms and negations of atoms.

   A line is coded as a pair (p,n) where p collects atoms and n
   the negated atoms. p and n are disjoint and sorted lists without duplicates
   (w.r.t Pervasives.compare).

   A dnf is coded as a sorted list of lines without duplicated
   (w.r.t Pervasives.compare).
*)

module Make(X : Custom.T) :
sig
  include Custom.T
  type elem = X.t

  external get: t -> (X.t list * X.t list) list = "%identity"

  val empty : t
  val full  : t
  val cup   : t -> t -> t
  val cap   : t -> t -> t
  val diff  : t -> t -> t
  val atom  : X.t -> t

  val map : (X.t -> X.t) -> t -> t
  val iter: (X.t -> unit) -> t -> unit
  val compute: empty:'d -> full:'c -> cup:('d -> 'c -> 'd) 
    -> cap:('c -> 'b -> 'c) -> diff:('c -> 'b -> 'c) ->
    atom:(X.t -> 'b) -> t -> 'd
  val compute_bool: (X.t -> t) -> t -> t
    
  val print: string -> (Format.formatter -> X.t -> unit) -> t ->
    (Format.formatter -> unit) list
    
    
  val trivially_disjoint : t -> t -> bool    
end