boolean.ml 4.33 KB
Newer Older
1 2 3 4
(* Optimization ideas:
    -    (A|B) & (C|D) = A | (B & (C|D))    if A <= C
*)

5 6
module type S =
sig
7 8
  include Custom.T
  type elem
9

10
  external get: t -> (elem list * elem list) list = "%identity"
11

12 13 14 15 16 17
  val empty : t
  val full  : t
  val cup   : t -> t -> t
  val cap   : t -> t -> t
  val diff  : t -> t -> t
  val atom  : elem -> t
18

19 20
  val map : (elem -> elem) -> t -> t
  val iter: (elem -> unit) -> t -> unit
21 22
  val compute: empty:'d -> full:'c -> cup:('d -> 'c -> 'd) 
    -> cap:('c -> 'b -> 'c) -> diff:('c -> 'b -> 'c) ->
23 24
    atom:(elem -> 'b) -> t -> 'd
  val compute_bool: (elem -> t) -> t -> t
25
    
26
  val print: string -> (Format.formatter -> elem -> unit) -> t ->
27 28
    (Format.formatter -> unit) list
    
29
  val trivially_disjoint : t -> t -> bool    
30 31
end

32 33 34 35 36 37
module Make(X : Custom.T) = struct
  type elem = X.t
  module SList = SortedList.Make(X)
  include SortedList.Make(Custom.Pair(SList)(SList))


38

39 40

let empty = [ ]
41
let full  = [ [],[] ]
42

43
let atom x = [ [x],[] ]
44

45
let may_remove (p1,n1) (p2,n2) =
46
(*  false *)
47
  (SList.subset p2 p1) && (SList.subset n2 n1)
48

49 50 51 52
(* in some cases, it is faster to avoid may_remove...
   investigate this... *)


53 54
let cup t s = 
  if t == s then t
55 56 57 58 59 60
  else match (t,s) with
    | [],s -> s
    | t,[] -> t
    | [ [], [] ], _ | _, [ [], [] ] -> full
    | _ ->
	let s=
61 62
	  filter 
	    (fun (p,n) -> not (exists (may_remove (p,n)) t)) s in
63
	let t=
64 65 66
	  filter 
	    (fun (p,n) -> not (exists (may_remove (p,n)) s)) t in 
	cup s t
67

68
(*
69
let clean accu t =
70 71 72 73 74
  let rec aux accu = function
    | (p,n) :: rem ->
	if (List.exists (may_remove (p,n)) accu)
	  || (List.exists (may_remove (p,n)) rem)
	then aux accu rem
75 76
	else aux ((p,n)::accu) rem 
    | [] -> accu
77
  in
78
  from_list (aux accu t)
79
*)
80 81 82

    

83 84 85 86 87 88 89 90 91
let rec fold2_aux f a x = function
  | [] -> x
  | h :: t -> fold2_aux f a (f x a h) t

let rec fold2 f x l1 l2 =
  match l1 with
    | [] -> x
    | h :: t -> fold2 f (fold2_aux f h x l2) t l2

92 93 94 95 96 97 98 99 100 101
let rec should_add x = function
  | [] -> true
  | y::rem -> if may_remove x y then false else should_add x rem

let rec clean_add accu x = function
  | [] -> accu
  | y::rem -> 
      if may_remove y x then clean_add accu x rem 
      else clean_add (y::accu) x rem

102 103 104 105 106 107
let cap s t =
  if s == t then s
  else if s == full then t
  else if t == full then s
  else if (s == empty) || (t == empty) then empty
  else
108
    let (lines1,common,lines2) = split s t in
109
    let rec aux lines (p1,n1) (p2,n2) =
110 111 112 113
        if (SList.disjoint p1 n2) && (SList.disjoint p2 n1)
        then 
	  let x = (SList.cup p1 p2, SList.cup n1 n2) in
	  if should_add x lines then clean_add [x] x lines else lines
114
	else lines
115
    in
116 117
    from_list 
      (fold2 aux (get common) (get lines1) (get lines2))
118 119

let diff c1 c2 =
120
  if (c2 == full) || (c1 == c2) then empty
121 122
  else if (c1 == empty) || (c2 == empty) then c1
  else
123
    let c1 = diff c1 c2 in
124
    let line (p,n) =
125 126
      let acc = SList.fold (fun acc a -> ([], [a]) :: acc) [] p in
      let acc = SList.fold (fun acc a -> ([a], []) :: acc) acc n in
127
      from_list acc
128
    in
129
    fold (fun c1 l -> cap c1 (line l)) c1 c2
130 131 132 133 134 135


let rec map f t =
  let lines =
    List.fold_left
      (fun lines (p,n) ->
136 137
	 let p = SList.map f p and n = SList.map f n in
	 if (SList.disjoint p n) then (p,n) :: lines else lines)
138 139 140
      []
      t
  in
141
  from_list lines
142

143
let iter f t =
144
  iter (fun (p,n) -> SList.iter f p; SList.iter f n) t
145

146 147 148 149 150 151
let compute ~empty ~full ~cup ~cap ~diff ~atom t =
  let line (p,n) =
    List.fold_left (fun accu x -> diff accu (atom x)) (
      List.fold_left (fun accu x -> cap accu (atom x)) full p
    ) n in
  List.fold_left (fun accu l -> cup accu (line l)) empty t
152
  
153 154 155
let compute_bool f = 
  compute ~empty ~full ~cup ~cap ~diff ~atom:f

156 157 158 159 160 161 162 163

let print any f =
  List.map 
    (function 
	 (p1::p,n) -> 
	   (fun ppf ->
	      Format.fprintf ppf "@[%a" f p1;
	      List.iter (fun x -> Format.fprintf ppf " &@ %a" f x) p;
164
	      List.iter (fun x -> Format.fprintf ppf " \\@ %a" f x) n;
165 166 167 168 169
	      Format.fprintf ppf "@]";
	   )
       | ([],[]) -> 
	   (fun ppf -> Format.fprintf ppf "%s" any)
       | ([],[n]) ->
170
	   (fun ppf -> Format.fprintf ppf "@[%s \\ %a@]" any f n)
171 172 173
       | ([],n1::n) ->
	   (fun ppf -> 
              Format.fprintf ppf "@[%s" any;
174
	      List.iter (fun x -> Format.fprintf ppf " \\@ %a" f x) n;
175 176 177 178
	      Format.fprintf ppf "@]";
	   )
    )

179 180
let trivially_disjoint a b = cap a b = []

181
  external get: t -> (elem list * elem list) list = "%identity"
182

183 184
end