viewcvs.cgi/types/normal.ml

module type S =
sig
  type t

  val any: t
  val empty: t
  val cup: t -> t -> t
  val cap: t -> t -> t
  val diff: t -> t -> t
  val is_empty: t -> bool
end

type 'a bool = ('a list * 'a list) list

module Make(X1 : S)(X2 : S) =
struct
  type t = (X1.t * X2.t) list

(* Possible optimizations:
   - check whether t1 or t2 is empty initially
   - check s1 = t1 (structural equility)
*)
  let rec add root t1 t2 = function
    | [] -> (t1,t2) :: root
    | (s1,s2) :: rem ->
        let i = X1.cap t1 s1 in
        if X1.is_empty i then add ((s1,s2)::root) t1 t2 rem
        else (
          let root = (i, X2.cup t2 s2) :: root in
          let k = X1.diff s1 t1 in
          let root = if not (X1.is_empty k) then (k, s2) :: root else root in
          let j = X1.diff t1 s1 in
          if not (X1.is_empty j) then add root j t2 rem else root
        )

  let normal x =
    List.fold_left (fun accu (t1,t2) -> add [] t1 t2 accu) [] x

  let rec bigcap_aux t1 t2 = function
    | (s1,s2)::rem -> bigcap_aux (X1.cap t1 s1) (X2.cap t2 s2) rem
    | [] -> (t1,t2)
  let bigcap = bigcap_aux X1.any X2.any

(* optimize: one knows that the t1 are pairwise disjoint ... *)
  let line accu (p,n) =
    let (d1,d2) = bigcap p in
    if not ((X1.is_empty d1) || (X2.is_empty d2)) then
      (let resid = ref X1.empty in
       let accu = List.fold_left
         (fun accu (t1,t2) ->
            let i = X1.cap d1 t1 in
            if not (X1.is_empty i) then
              (resid := X1.cup !resid t1;
               let t2 = X2.diff d2 t2 in
               if not (X2.is_empty t2) then add [] i t2 accu else accu
              ) else accu
         ) accu (normal n) in
       let d1 = X1.diff d1 !resid in
       if not (X1.is_empty d1) then add [] d1 d2 accu else accu)
    else accu
      
  let boolean_normal x =
    List.fold_left line [] x

  let boolean x =
    List.fold_left (fun accu x -> (line [] x) @ accu) [] x

  let pi1 =
    List.fold_left (fun accu (t1,t2) -> X1.cup accu t1) X1.empty

  let pi2 =
    List.fold_left (fun accu (t1,t2) -> X2.cup accu t2) X2.empty

  let pi2_restricted restr = 
    List.fold_left (fun accu (t1,t2) -> 
                      if X1.is_empty (X1.cap t1 restr) then accu 
                      else X2.cup accu t2) X2.empty
end

1	module type S =
2	sig
3	type t
4
5	val any: t
6	val empty: t
7	val cup: t -> t -> t
8	val cap: t -> t -> t
9	val diff: t -> t -> t
10	val is_empty: t -> bool
11	end
12
13	type 'a bool = ('a list * 'a list) list
14
15	module Make(X1 : S)(X2 : S) =
16	struct
17	type t = (X1.t * X2.t) list
18
19	(* Possible optimizations:
20	- check whether t1 or t2 is empty initially
21	- check s1 = t1 (structural equility)
22	*)
23	let rec add root t1 t2 = function
24	\| [] -> (t1,t2) :: root
25	\| (s1,s2) :: rem ->
26	let i = X1.cap t1 s1 in
27	if X1.is_empty i then add ((s1,s2)::root) t1 t2 rem
28	else (
29	let root = (i, X2.cup t2 s2) :: root in
30	let k = X1.diff s1 t1 in
31	let root = if not (X1.is_empty k) then (k, s2) :: root else root in
32	let j = X1.diff t1 s1 in
33	if not (X1.is_empty j) then add root j t2 rem else root
34	)
35
36	let normal x =
37	List.fold_left (fun accu (t1,t2) -> add [] t1 t2 accu) [] x
38
39	let rec bigcap_aux t1 t2 = function
40	\| (s1,s2)::rem -> bigcap_aux (X1.cap t1 s1) (X2.cap t2 s2) rem
41	\| [] -> (t1,t2)
42	let bigcap = bigcap_aux X1.any X2.any
43
44	(* optimize: one knows that the t1 are pairwise disjoint ... *)
45	let line accu (p,n) =
46	let (d1,d2) = bigcap p in
47	if not ((X1.is_empty d1) \|\| (X2.is_empty d2)) then
48	(let resid = ref X1.empty in
49	let accu = List.fold_left
50	(fun accu (t1,t2) ->
51	let i = X1.cap d1 t1 in
52	if not (X1.is_empty i) then
53	(resid := X1.cup !resid t1;
54	let t2 = X2.diff d2 t2 in
55	if not (X2.is_empty t2) then add [] i t2 accu else accu
56	) else accu
57	) accu (normal n) in
58	let d1 = X1.diff d1 !resid in
59	if not (X1.is_empty d1) then add [] d1 d2 accu else accu)
60	else accu
61
62	let boolean_normal x =
63	List.fold_left line [] x
64
65	let boolean x =
66	List.fold_left (fun accu x -> (line [] x) @ accu) [] x
67
68	let pi1 =
69	List.fold_left (fun accu (t1,t2) -> X1.cup accu t1) X1.empty
70
71	let pi2 =
72	List.fold_left (fun accu (t1,t2) -> X2.cup accu t2) X2.empty
73
74	let pi2_restricted restr =
75	List.fold_left (fun accu (t1,t2) ->
76	if X1.is_empty (X1.cap t1 restr) then accu
77	else X2.cup accu t2) X2.empty
78	end
79