viewcvs.cgi/types/sortedList.ml

module Make(X : Custom.T) = struct
  include Custom.List(X)
  let rec check = function
    | x::(y::_ as tl) -> X.check x; assert (X.compare x y < 0); check tl
    | [x] -> X.check x;
    | _ -> ()

  type elem = X.t

  let rec equal l1 l2 =
    (l1 == l2) ||
    match (l1,l2) with
      | x1::l1, x2::l2 -> (X.equal x1 x2) && (equal l1 l2)
      | _ -> false

  let rec hash accu = function
    | [] -> 1 + accu
    | x::l -> hash (17 * accu + X.hash x) l

  let hash l = hash 1 l

  let rec compare l1 l2 =
    if l1 == l2 then 0 
    else match (l1,l2) with
      | x1::l1, x2::l2 -> 
          let c = X.compare x1 x2 in if c <> 0 then c 
          else compare l1 l2
      | [],_ -> -1
      | _ -> 1


  let iter = List.iter

  let filter = List.filter
  let exists = List.exists
  let fold = List.fold_left


  external get: t -> elem list = "%identity"
  let singleton x = [ x ]

  let pick = function x::_ -> Some x | _ -> None 
  let length = List.length

  let empty = []
  let is_empty l = l = []

let rec disjoint l1 l2 =
  if l1 == l2 then l1 == [] else
  match (l1,l2) with
    | (t1::q1, t2::q2) -> 
        let c = X.compare t1 t2 in
        if c < 0 then disjoint q1 l2
        else if c > 0 then disjoint l1 q2
        else false
    | _ -> true
        
let rec cup l1 l2 =
  if l1 == l2 then l1 else
  match (l1,l2) with
    | (t1::q1, t2::q2) ->
        let c = X.compare t1 t2 in
        if c = 0 then t1::(cup q1 q2)
        else if c < 0 then t1::(cup q1 l2)
        else t2::(cup l1 q2)
    | ([],l2) -> l2
    | (l1,[]) -> l1

let add x l = cup [x] l
        
let rec split l1 l2 =
  match (l1,l2) with
    | (t1::q1, t2::q2) ->
        let c = X.compare t1 t2 in
        if c = 0 then       let (l1,i,l2) = split q1 q2 in (l1,t1::i,l2)
        else if c < 0 then  let (l1,i,l2) = split q1 l2 in (t1::l1,i,l2)
        else                let (l1,i,l2) = split l1 q2 in (l1,i,t2::l2)
    | _ -> (l1,[],l2)
        
        
let rec diff l1 l2 =
  if l1 == l2 then [] else
  match (l1,l2) with
    | (t1::q1, t2::q2) ->
        let c = X.compare t1 t2 in
        if c = 0 then diff q1 q2
        else if c < 0 then t1::(diff q1 l2)
        else diff l1 q2
    | _ -> l1

let remove x l = diff l [x]

let rec cap l1 l2 =
  if l1 == l2 then l1 else
  match (l1,l2) with
    | (t1::q1, t2::q2) ->
        let c = X.compare t1 t2 in
        if c = 0 then t1::(cap q1 q2)
        else if c < 0 then cap q1 l2
        else cap l1 q2
    | _ -> []

        
let rec subset l1 l2 =
  (l1 == l2) ||
  match (l1,l2) with
    | (t1::q1, t2::q2) ->
        let c = X.compare t1 t2 in
        if c = 0 then (
(* inlined: subset q1 q2 *)
          (q1 == q2) || match (q1,q2) with
            | (t1::qq1, t2::qq2) ->
                let c = X.compare t1 t2 in
                if c = 0 then subset qq1 qq2
                else if c < 0 then false
                else subset q1 qq2
            | [],_ -> true | _ -> false
        )
        else if c < 0 then false
        else subset l1 q2
    | [],_ -> true | _ -> false
        
        
let from_list l = 
  let rec initlist = function
    | [] -> []
    | e::rest -> [e] :: initlist rest in
  let rec merge2 = function
    | l1::l2::rest -> cup l1 l2 :: merge2 rest
    | x -> x in
  let rec mergeall = function
    | [] -> []
    | [l] -> l
    | llist -> mergeall (merge2 llist) in
  mergeall (initlist l)
    
let map f l =
  from_list (List.map f l)

(* The order of elements might have changed since serialization *)
  let deserialize f = from_list (deserialize f)


let rec mem l x =
  match l with
    | [] -> false
    | t::q -> 
        let c = X.compare x t in
        (c = 0) || ((c > 0) && (mem q x))

module Map = struct
  type 'a map = (X.t * 'a) list
  external get: 'a map -> (elem * 'a) list = "%identity"
  let empty = []
  let is_empty l = l = []
  let singleton x y = [ (x,y) ]

  let rec iter f = function
    | (_,y)::l -> f y; iter f l
    | [] -> ()

  let rec filter f = function
    | ((x,y) as c)::l -> if f x y then c::(filter f l) else filter f l
    | [] -> []

  let rec assoc_remove_aux v r = function
    | ((x,y) as a)::l ->
        let c = X.compare x v in
        if c = 0 then (r := Some y; l) 
        else if c < 0 then a :: (assoc_remove_aux v r l)
        else raise Not_found
    | [] -> raise Not_found

  let assoc_remove v l =
    let r = ref None in
    let l = assoc_remove_aux v r l in
    match !r with Some x -> (x,l) | _ -> assert false

(* TODO: is is faster to raise exception Not_found and return
   original list ? *)
  let rec remove v = function
    | (((x,y) as a)::rem) as l->
        let c = X.compare x v in
        if c = 0 then rem
        else if c < 0 then a :: (remove v rem)
        else l
    | [] -> []

  let rec merge f l1 l2 =
    match (l1,l2) with
      | ((x1,y1) as t1)::q1, ((x2,y2) as t2)::q2 ->
          let c = X.compare x1 x2 in
          if c = 0 then (x1,(f y1 y2))::(merge f q1 q2)
          else if c < 0 then t1::(merge f q1 l2)
          else t2::(merge f l1 q2)
      | ([],l2) -> l2
      | (l1,[]) -> l1

  let rec cap f l1 l2 =
    match (l1,l2) with
      | ((x1,y1) as t1)::q1, ((x2,y2) as t2)::q2 ->
          let c = X.compare x1 x2 in
          if c = 0 then (x1,(f y1 y2))::(cap f q1 q2)
          else if c < 0 then cap f q1 l2
          else cap f l1 q2
      | _ -> []

  let rec sub f l1 l2 =
    match (l1,l2) with
      | ((x1,y1) as t1)::q1, ((x2,y2) as t2)::q2 ->
          let c = X.compare x1 x2 in
          if c = 0 then (x1,(f y1 y2))::(sub f q1 q2)
          else if c < 0 then t1::(sub f q1 l2)
          else sub f l1 q2
      | (l1,_) -> l1

  let merge_elem x l1 l2 = merge (fun _ _ -> x) l1 l2
                             (* TODO: optimize this ? *)

  let rec union_disj l1 l2 =
    match (l1,l2) with
      | ((x1,y1) as t1)::q1, ((x2,y2) as t2)::q2 ->
          let c = X.compare x1 x2 in
          if c = 0 then failwith "SortedList.Map.union_disj"
          else if c < 0 then t1::(union_disj q1 l2)
          else t2::(union_disj l1 q2)
      | ([],l2) -> l2
      | (l1,[]) -> l1

  let rec diff l1 l2 =
    match (l1,l2) with
      | (((x1,y1) as t1)::q1, x2::q2) ->
          let c = X.compare x1 x2 in
          if c = 0 then diff q1 q2
          else if c < 0 then t1::(diff q1 l2)
          else diff l1 q2
      | _ -> l1

  let from_list f l = 
    let rec initlist = function
      | [] -> []
      | e::rest -> [e] :: initlist rest in
    let rec merge2 = function
      | l1::l2::rest -> merge f l1 l2 :: merge2 rest
      | x -> x in
    let rec mergeall = function
      | [] -> []
      | [l] -> l
      | llist -> mergeall (merge2 llist) in
    mergeall (initlist l)

  let from_list_disj l = 
    let rec initlist = function
      | [] -> []
      | e::rest -> [e] :: initlist rest in
    let rec merge2 = function
      | l1::l2::rest -> union_disj l1 l2 :: merge2 rest
      | x -> x in
    let rec mergeall = function
      | [] -> []
      | [l] -> l
      | llist -> mergeall (merge2 llist) in
    mergeall (initlist l)

  let rec map_from_slist f = function
    | x::l -> (x,f x)::(map_from_slist f l)
    | [] -> []
    
  let rec collide f l1 l2 =
    match (l1,l2) with
      | (_,y1)::l1, (_,y2)::l2 -> f y1 y2; collide f l1 l2
      | [],[] -> ()
      | _ -> assert false

  let rec map f = function
    | (x,y)::l -> (x, f y)::(map f l)
    | [] -> []

  let rec mapi f = function
    | (x,y)::l -> (x, f x y)::(mapi f l)
    | [] -> []

  let rec mapi_to_list f = function
    | (x,y)::l -> (f x y) ::(mapi_to_list f l)
    | [] -> []

  let rec constant y = function
    | x::l -> (x,y)::(constant y l)
    | [] -> []

  let rec num i = function [] -> [] | h::t -> (h,i)::(num (i+1) t)

  let rec map_to_list f = function
    | (x,y)::l -> (f y)::(map_to_list f l)
    | [] -> []

  let rec assoc v = function
    | (x,y)::l ->
        let c = X.compare x v in
        if c = 0 then y 
        else if c < 0 then assoc v l
        else raise Not_found
    | [] -> raise Not_found

  let rec assoc_present v = function
    | [(_,y)] -> y
    | (x,y)::l ->
        let c = X.compare x v in
        if c = 0 then y else assoc_present v l
    | [] -> assert false

  let rec compare f l1 l2 =
    if l1 == l2 then 0 
    else match (l1,l2) with
      | (x1,y1)::l1, (x2,y2)::l2 ->
          let c = X.compare x1 x2 in if c <> 0 then c
          else let c = f y1 y2 in if c <> 0 then c
          else compare f l1 l2
      | [],_ -> -1
      | _,[] -> 1

  let rec hash f = function
    | [] -> 1
    | (x,y)::l -> X.hash x + 17 * (f y) + 257 * (hash f l)

  let rec equal f l1 l2  =
    (l1 == l2) ||
    match (l1,l2) with
      | (x1,y1)::l1, (x2,y2)::l2 ->
          (X.equal x1 x2) && (f y1 y2) && (equal f l1 l2)
      | _ -> false


  let serialize f t l =
    Serialize.Put.list (Serialize.Put.pair X.serialize f) t l
  let deserialize f t =
    from_list_disj 
        (Serialize.Get.list (Serialize.Get.pair X.deserialize f) t)

  let rec check f = function
    | (x,a)::((y,b)::_ as tl) -> 
        X.check x; f a;
        assert (X.compare x y < 0); check f tl
    | [x,a] -> X.check x; f a
    | _ -> ()
    
end


  module MakeMap(Y : Custom.T) = struct
    type t = Y.t Map.map
        (* Note: need to eta expand these definitions, because
           of the compilation of the recursive module definitions
           in types.ml... *)
    let hash x = Map.hash Y.hash x
    let compare x y = Map.compare Y.compare x y
    let equal x y = Map.equal Y.equal x y 

    let check l = Map.check Y.check l
    let dump ppf _ = Format.fprintf ppf "<SortedList.MakeMap>"

    let serialize t l =
      Serialize.Put.list (Serialize.Put.pair X.serialize Y.serialize) t l

    let deserialize t =
      Map.from_list_disj 
        (Serialize.Get.list (Serialize.Get.pair X.deserialize Y.deserialize) t)
  end


end

module type FiniteCofinite = sig
  type elem
  type s = private Finite of elem list | Cofinite of elem list
  include Custom.T with type t = s

  val empty: t
  val any: t
  val atom: elem -> t
  val cup: t -> t -> t
  val cap: t -> t -> t
  val diff: t -> t -> t
  val neg: t -> t
  val contains: elem -> t -> bool
  val disjoint: t -> t -> bool
  val is_empty: t -> bool
end

module FiniteCofinite(X : Custom.T) = struct
  type elem = X.t
  module SList = Make(X)
  type s = Finite of SList.t | Cofinite of SList.t
  type t = s

  let hash = function
    | Finite l -> SList.hash l
    | Cofinite l -> 17 * SList.hash l + 1

  let compare l1 l2 =
    match (l1,l2) with
      | Finite l1, Finite l2 
      | Cofinite l1, Cofinite l2 -> SList.compare l1 l2
      | Finite _, Cofinite _ -> -1
      | _ -> 1

  let equal l1 l2 = compare l1 l2 = 0

  let serialize t = function
    | Finite s -> Serialize.Put.bool t true; SList.serialize t s
    | Cofinite s -> Serialize.Put.bool t false; SList.serialize t s

   let deserialize t = 
    if Serialize.Get.bool t
    then Finite (SList.deserialize t)
    else Cofinite (SList.deserialize t)

   let check = function
    | Finite s | Cofinite s -> SList.check s

  let dump ppf = function
    | Finite s -> Format.fprintf ppf "Finite[%a]" SList.dump s
    | Cofinite s -> Format.fprintf ppf "Cofinite[%a]" SList.dump s


  let empty = Finite []
  let any = Cofinite []
  let atom x = Finite [x]

  let cup s t =
    match (s,t) with
      | (Finite s, Finite t) -> Finite (SList.cup s t)
      | (Finite s, Cofinite t) -> Cofinite (SList.diff t s)
      | (Cofinite s, Finite t) -> Cofinite (SList.diff s t)
      | (Cofinite s, Cofinite t) -> Cofinite (SList.cap s t)

  let cap s t =
    match (s,t) with
      | (Finite s, Finite t) -> Finite (SList.cap s t)
      | (Finite s, Cofinite t) -> Finite (SList.diff s t)
      | (Cofinite s, Finite t) -> Finite (SList.diff t s)
      | (Cofinite s, Cofinite t) -> Cofinite (SList.cup s t)

  let diff s t =
    match (s,t) with
      | (Finite s, Cofinite t) -> Finite (SList.cap s t)
      | (Finite s, Finite t) -> Finite (SList.diff s t)
      | (Cofinite s, Cofinite t) -> Finite (SList.diff t s)
      | (Cofinite s, Finite t) -> Cofinite (SList.cup s t)

  let neg = function
      | Finite s -> Cofinite s
      | Cofinite s -> Finite s
        
  let contains x = function
    | Finite s -> SList.mem s x
    | Cofinite s -> not (SList.mem s x)
        
  let disjoint s t =
    match (s,t) with
      | (Finite s, Finite t) -> SList.disjoint s t
      | (Finite s, Cofinite t) -> SList.subset s t
      | (Cofinite s, Finite t) -> SList.subset t s
      | (Cofinite s, Cofinite t) -> false

  let is_empty = function Finite [] -> true | _ -> false
end

module FiniteCofiniteMap(X : Custom.T)(SymbolSet : FiniteCofinite) =
struct
  include Custom.Dummy

  module T0 = Make(X)
  module TMap = T0.MakeMap(SymbolSet)
  module T = T0.Map
  type t = Finite of TMap.t | Cofinite of TMap.t

  let get = function
    | Finite l -> `Finite (T.get l)
    | Cofinite l -> `Cofinite (T.get l)
    
  let check = function
    | Finite l | Cofinite l -> TMap.check l
                   
  let dump ppf = function
    | Finite s -> Format.fprintf ppf "Finite[%a]" TMap.dump s
    | Cofinite s -> Format.fprintf ppf "Cofinite[%a]" TMap.dump s
        
  let serialize t = function
    | Finite s -> Serialize.Put.bool t true; TMap.serialize t s
    | Cofinite s -> Serialize.Put.bool t false; TMap.serialize t s
        
  let deserialize t = 
    if Serialize.Get.bool t
    then Finite (TMap.deserialize t)
    else Cofinite (TMap.deserialize t)
      

  let empty = Finite T.empty
  let any   = Cofinite T.empty
  let any_in_ns ns = Finite (T.singleton ns SymbolSet.any)
                       
  let finite l =
    let l = 
      T.filter 
        (fun _ x -> match x with SymbolSet.Finite [] -> false | _ -> true)
        l in
    Finite l
      
  let cofinite l =
    let l = 
      T.filter 
        (fun _ x -> match x with SymbolSet.Cofinite [] -> false | _ -> true)
        l in
    Cofinite l
      
      
  let atom (ns,x) = Finite (T.singleton ns (SymbolSet.atom x))
                      
  let cup s t =
    match (s,t) with
      | (Finite s, Finite t) -> finite (T.merge SymbolSet.cup s t)
      | (Finite s, Cofinite t) -> cofinite (T.sub SymbolSet.diff t s)
      | (Cofinite s, Finite t) -> cofinite (T.sub SymbolSet.diff s t)
      | (Cofinite s, Cofinite t) -> cofinite (T.cap SymbolSet.cap s t)
          
  let cap s t =
    match (s,t) with
      | (Finite s, Finite t) -> finite (T.cap SymbolSet.cap s t)
      | (Finite s, Cofinite t) -> finite (T.sub SymbolSet.diff s t)
      | (Cofinite s, Finite t) -> finite (T.sub SymbolSet.diff t s)
      | (Cofinite s, Cofinite t) -> cofinite (T.merge SymbolSet.cup s t)
          
  let diff s t =
    match (s,t) with
      | (Finite s, Cofinite t) -> finite (T.cap SymbolSet.cap s t)
      | (Finite s, Finite t) -> finite (T.sub SymbolSet.diff s t)
      | (Cofinite s, Cofinite t) -> finite (T.sub SymbolSet.diff t s)
      | (Cofinite s, Finite t) -> cofinite (T.merge SymbolSet.cup s t)
          
  let is_empty = function
    | Finite l -> T.is_empty l
    | _ -> false  

  let hash = function
    | Finite l -> 1 + 17 * (TMap.hash l)
    | Cofinite l -> 2 +  17 * (TMap.hash l)
        
  let compare l1 l2 =
    match (l1,l2) with
      | Finite l1, Finite l2 
      | Cofinite l1, Cofinite l2 -> TMap.compare l1 l2
      | Finite _, Cofinite _ -> -1
      | _ -> 1
          
  let equal t1 t2 = 
    compare t1 t2 = 0

  let symbol_set ns = function
    | Finite s ->
        (try T.assoc ns s with Not_found -> SymbolSet.empty)
    | Cofinite s ->
        (try SymbolSet.neg (T.assoc ns s) with Not_found -> SymbolSet.any)

  let contains (ns,x) = function
    | Finite s -> 
        (try SymbolSet.contains x (T.assoc ns s) with Not_found -> false)
    | Cofinite s -> 
        (try not (SymbolSet.contains x (T.assoc ns s)) with Not_found -> true)
        
  let disjoint s t = 
    is_empty (cap t s) (* TODO: OPT *)

end
1	module Make(X : Custom.T) = struct
2	include Custom.List(X)
3	let rec check = function
4	\| x::(y::_ as tl) -> X.check x; assert (X.compare x y < 0); check tl
5	\| [x] -> X.check x;
6	\| _ -> ()
7
8	type elem = X.t
9
10	let rec equal l1 l2 =
11	(l1 == l2) \|\|
12	match (l1,l2) with
13	\| x1::l1, x2::l2 -> (X.equal x1 x2) && (equal l1 l2)
14	\| _ -> false
15
16	let rec hash accu = function
17	\| [] -> 1 + accu
18	\| x::l -> hash (17 * accu + X.hash x) l
19
20	let hash l = hash 1 l
21
22	let rec compare l1 l2 =
23	if l1 == l2 then 0
24	else match (l1,l2) with
25	\| x1::l1, x2::l2 ->
26	let c = X.compare x1 x2 in if c <> 0 then c
27	else compare l1 l2
28	\| [],_ -> -1
29	\| _ -> 1
30
31
32	let iter = List.iter
33
34	let filter = List.filter
35	let exists = List.exists
36	let fold = List.fold_left
37
38
39	external get: t -> elem list = "%identity"
40	let singleton x = [ x ]
41
42	let pick = function x::_ -> Some x \| _ -> None
43	let length = List.length
44
45	let empty = []
46	let is_empty l = l = []
47
48	let rec disjoint l1 l2 =
49	if l1 == l2 then l1 == [] else
50	match (l1,l2) with
51	\| (t1::q1, t2::q2) ->
52	let c = X.compare t1 t2 in
53	if c < 0 then disjoint q1 l2
54	else if c > 0 then disjoint l1 q2
55	else false
56	\| _ -> true
57
58	let rec cup l1 l2 =
59	if l1 == l2 then l1 else
60	match (l1,l2) with
61	\| (t1::q1, t2::q2) ->
62	let c = X.compare t1 t2 in
63	if c = 0 then t1::(cup q1 q2)
64	else if c < 0 then t1::(cup q1 l2)
65	else t2::(cup l1 q2)
66	\| ([],l2) -> l2
67	\| (l1,[]) -> l1
68
69	let add x l = cup [x] l
70
71	let rec split l1 l2 =
72	match (l1,l2) with
73	\| (t1::q1, t2::q2) ->
74	let c = X.compare t1 t2 in
75	if c = 0 then let (l1,i,l2) = split q1 q2 in (l1,t1::i,l2)
76	else if c < 0 then let (l1,i,l2) = split q1 l2 in (t1::l1,i,l2)
77	else let (l1,i,l2) = split l1 q2 in (l1,i,t2::l2)
78	\| _ -> (l1,[],l2)
79
80
81	let rec diff l1 l2 =
82	if l1 == l2 then [] else
83	match (l1,l2) with
84	\| (t1::q1, t2::q2) ->
85	let c = X.compare t1 t2 in
86	if c = 0 then diff q1 q2
87	else if c < 0 then t1::(diff q1 l2)
88	else diff l1 q2
89	\| _ -> l1
90
91	let remove x l = diff l [x]
92
93	let rec cap l1 l2 =
94	if l1 == l2 then l1 else
95	match (l1,l2) with
96	\| (t1::q1, t2::q2) ->
97	let c = X.compare t1 t2 in
98	if c = 0 then t1::(cap q1 q2)
99	else if c < 0 then cap q1 l2
100	else cap l1 q2
101	\| _ -> []
102
103
104	let rec subset l1 l2 =
105	(l1 == l2) \|\|
106	match (l1,l2) with
107	\| (t1::q1, t2::q2) ->
108	let c = X.compare t1 t2 in
109	if c = 0 then (
110	(* inlined: subset q1 q2 *)
111	(q1 == q2) \|\| match (q1,q2) with
112	\| (t1::qq1, t2::qq2) ->
113	let c = X.compare t1 t2 in
114	if c = 0 then subset qq1 qq2
115	else if c < 0 then false
116	else subset q1 qq2
117	\| [],_ -> true \| _ -> false
118	)
119	else if c < 0 then false
120	else subset l1 q2
121	\| [],_ -> true \| _ -> false
122
123
124
125	let from_list l =
126	let rec initlist = function
127	\| [] -> []
128	\| e::rest -> [e] :: initlist rest in
129	let rec merge2 = function
130	\| l1::l2::rest -> cup l1 l2 :: merge2 rest
131	\| x -> x in
132	let rec mergeall = function
133	\| [] -> []
134	\| [l] -> l
135	\| llist -> mergeall (merge2 llist) in
136	mergeall (initlist l)
137
138	let map f l =
139	from_list (List.map f l)
140
141	(* The order of elements might have changed since serialization *)
142	let deserialize f = from_list (deserialize f)
143
144
145	let rec mem l x =
146	match l with
147	\| [] -> false
148	\| t::q ->
149	let c = X.compare x t in
150	(c = 0) \|\| ((c > 0) && (mem q x))
151
152	module Map = struct
153	type 'a map = (X.t * 'a) list
154	external get: 'a map -> (elem * 'a) list = "%identity"
155	let empty = []
156	let is_empty l = l = []
157	let singleton x y = [ (x,y) ]
158
159	let rec iter f = function
160	\| (_,y)::l -> f y; iter f l
161	\| [] -> ()
162
163	let rec filter f = function
164	\| ((x,y) as c)::l -> if f x y then c::(filter f l) else filter f l
165	\| [] -> []
166
167	let rec assoc_remove_aux v r = function
168	\| ((x,y) as a)::l ->
169	let c = X.compare x v in
170	if c = 0 then (r := Some y; l)
171	else if c < 0 then a :: (assoc_remove_aux v r l)
172	else raise Not_found
173	\| [] -> raise Not_found
174
175	let assoc_remove v l =
176	let r = ref None in
177	let l = assoc_remove_aux v r l in
178	match !r with Some x -> (x,l) \| _ -> assert false
179
180	(* TODO: is is faster to raise exception Not_found and return
181	original list ? *)
182	let rec remove v = function
183	\| (((x,y) as a)::rem) as l->
184	let c = X.compare x v in
185	if c = 0 then rem
186	else if c < 0 then a :: (remove v rem)
187	else l
188	\| [] -> []
189
190	let rec merge f l1 l2 =
191	match (l1,l2) with
192	\| ((x1,y1) as t1)::q1, ((x2,y2) as t2)::q2 ->
193	let c = X.compare x1 x2 in
194	if c = 0 then (x1,(f y1 y2))::(merge f q1 q2)
195	else if c < 0 then t1::(merge f q1 l2)
196	else t2::(merge f l1 q2)
197	\| ([],l2) -> l2
198	\| (l1,[]) -> l1
199
200	let rec cap f l1 l2 =
201	match (l1,l2) with
202	\| ((x1,y1) as t1)::q1, ((x2,y2) as t2)::q2 ->
203	let c = X.compare x1 x2 in
204	if c = 0 then (x1,(f y1 y2))::(cap f q1 q2)
205	else if c < 0 then cap f q1 l2
206	else cap f l1 q2
207	\| _ -> []
208
209	let rec sub f l1 l2 =
210	match (l1,l2) with
211	\| ((x1,y1) as t1)::q1, ((x2,y2) as t2)::q2 ->
212	let c = X.compare x1 x2 in
213	if c = 0 then (x1,(f y1 y2))::(sub f q1 q2)
214	else if c < 0 then t1::(sub f q1 l2)
215	else sub f l1 q2
216	\| (l1,_) -> l1
217
218	let merge_elem x l1 l2 = merge (fun _ _ -> x) l1 l2
219	(* TODO: optimize this ? *)
220
221	let rec union_disj l1 l2 =
222	match (l1,l2) with
223	\| ((x1,y1) as t1)::q1, ((x2,y2) as t2)::q2 ->
224	let c = X.compare x1 x2 in
225	if c = 0 then failwith "SortedList.Map.union_disj"
226	else if c < 0 then t1::(union_disj q1 l2)
227	else t2::(union_disj l1 q2)
228	\| ([],l2) -> l2
229	\| (l1,[]) -> l1
230
231	let rec diff l1 l2 =
232	match (l1,l2) with
233	\| (((x1,y1) as t1)::q1, x2::q2) ->
234	let c = X.compare x1 x2 in
235	if c = 0 then diff q1 q2
236	else if c < 0 then t1::(diff q1 l2)
237	else diff l1 q2
238	\| _ -> l1
239
240	let from_list f l =
241	let rec initlist = function
242	\| [] -> []
243	\| e::rest -> [e] :: initlist rest in
244	let rec merge2 = function
245	\| l1::l2::rest -> merge f l1 l2 :: merge2 rest
246	\| x -> x in
247	let rec mergeall = function
248	\| [] -> []
249	\| [l] -> l
250	\| llist -> mergeall (merge2 llist) in
251	mergeall (initlist l)
252
253	let from_list_disj l =
254	let rec initlist = function
255	\| [] -> []
256	\| e::rest -> [e] :: initlist rest in
257	let rec merge2 = function
258	\| l1::l2::rest -> union_disj l1 l2 :: merge2 rest
259	\| x -> x in
260	let rec mergeall = function
261	\| [] -> []
262	\| [l] -> l
263	\| llist -> mergeall (merge2 llist) in
264	mergeall (initlist l)
265
266	let rec map_from_slist f = function
267	\| x::l -> (x,f x)::(map_from_slist f l)
268	\| [] -> []
269
270	let rec collide f l1 l2 =
271	match (l1,l2) with
272	\| (_,y1)::l1, (_,y2)::l2 -> f y1 y2; collide f l1 l2
273	\| [],[] -> ()
274	\| _ -> assert false
275
276	let rec map f = function
277	\| (x,y)::l -> (x, f y)::(map f l)
278	\| [] -> []
279
280	let rec mapi f = function
281	\| (x,y)::l -> (x, f x y)::(mapi f l)
282	\| [] -> []
283
284	let rec mapi_to_list f = function
285	\| (x,y)::l -> (f x y) ::(mapi_to_list f l)
286	\| [] -> []
287
288	let rec constant y = function
289	\| x::l -> (x,y)::(constant y l)
290	\| [] -> []
291
292	let rec num i = function [] -> [] \| h::t -> (h,i)::(num (i+1) t)
293
294	let rec map_to_list f = function
295	\| (x,y)::l -> (f y)::(map_to_list f l)
296	\| [] -> []
297
298	let rec assoc v = function
299	\| (x,y)::l ->
300	let c = X.compare x v in
301	if c = 0 then y
302	else if c < 0 then assoc v l
303	else raise Not_found
304	\| [] -> raise Not_found
305
306	let rec assoc_present v = function
307	\| [(_,y)] -> y
308	\| (x,y)::l ->
309	let c = X.compare x v in
310	if c = 0 then y else assoc_present v l
311	\| [] -> assert false
312
313	let rec compare f l1 l2 =
314	if l1 == l2 then 0
315	else match (l1,l2) with
316	\| (x1,y1)::l1, (x2,y2)::l2 ->
317	let c = X.compare x1 x2 in if c <> 0 then c
318	else let c = f y1 y2 in if c <> 0 then c
319	else compare f l1 l2
320	\| [],_ -> -1
321	\| _,[] -> 1
322
323	let rec hash f = function
324	\| [] -> 1
325	\| (x,y)::l -> X.hash x + 17 * (f y) + 257 * (hash f l)
326
327	let rec equal f l1 l2 =
328	(l1 == l2) \|\|
329	match (l1,l2) with
330	\| (x1,y1)::l1, (x2,y2)::l2 ->
331	(X.equal x1 x2) && (f y1 y2) && (equal f l1 l2)
332	\| _ -> false
333
334
335	let serialize f t l =
336	Serialize.Put.list (Serialize.Put.pair X.serialize f) t l
337	let deserialize f t =
338	from_list_disj
339	(Serialize.Get.list (Serialize.Get.pair X.deserialize f) t)
340
341	let rec check f = function
342	\| (x,a)::((y,b)::_ as tl) ->
343	X.check x; f a;
344	assert (X.compare x y < 0); check f tl
345	\| [x,a] -> X.check x; f a
346	\| _ -> ()
347
348	end
349
350
351	module MakeMap(Y : Custom.T) = struct
352	type t = Y.t Map.map
353	(* Note: need to eta expand these definitions, because
354	of the compilation of the recursive module definitions
355	in types.ml... *)
356	let hash x = Map.hash Y.hash x
357	let compare x y = Map.compare Y.compare x y
358	let equal x y = Map.equal Y.equal x y
359
360	let check l = Map.check Y.check l
361	let dump ppf _ = Format.fprintf ppf "<SortedList.MakeMap>"
362
363	let serialize t l =
364	Serialize.Put.list (Serialize.Put.pair X.serialize Y.serialize) t l
365
366	let deserialize t =
367	Map.from_list_disj
368	(Serialize.Get.list (Serialize.Get.pair X.deserialize Y.deserialize) t)
369	end
370
371
372
373	end
374
375	module type FiniteCofinite = sig
376	type elem
377	type s = private Finite of elem list \| Cofinite of elem list
378	include Custom.T with type t = s
379
380	val empty: t
381	val any: t
382	val atom: elem -> t
383	val cup: t -> t -> t
384	val cap: t -> t -> t
385	val diff: t -> t -> t
386	val neg: t -> t
387	val contains: elem -> t -> bool
388	val disjoint: t -> t -> bool
389	val is_empty: t -> bool
390	end
391
392	module FiniteCofinite(X : Custom.T) = struct
393	type elem = X.t
394	module SList = Make(X)
395	type s = Finite of SList.t \| Cofinite of SList.t
396	type t = s
397
398	let hash = function
399	\| Finite l -> SList.hash l
400	\| Cofinite l -> 17 * SList.hash l + 1
401
402	let compare l1 l2 =
403	match (l1,l2) with
404	\| Finite l1, Finite l2
405	\| Cofinite l1, Cofinite l2 -> SList.compare l1 l2
406	\| Finite _, Cofinite _ -> -1
407	\| _ -> 1
408
409	let equal l1 l2 = compare l1 l2 = 0
410
411	let serialize t = function
412	\| Finite s -> Serialize.Put.bool t true; SList.serialize t s
413	\| Cofinite s -> Serialize.Put.bool t false; SList.serialize t s
414
415	let deserialize t =
416	if Serialize.Get.bool t
417	then Finite (SList.deserialize t)
418	else Cofinite (SList.deserialize t)
419
420	let check = function
421	\| Finite s \| Cofinite s -> SList.check s
422
423	let dump ppf = function
424	\| Finite s -> Format.fprintf ppf "Finite[%a]" SList.dump s
425	\| Cofinite s -> Format.fprintf ppf "Cofinite[%a]" SList.dump s
426
427
428	let empty = Finite []
429	let any = Cofinite []
430	let atom x = Finite [x]
431
432	let cup s t =
433	match (s,t) with
434	\| (Finite s, Finite t) -> Finite (SList.cup s t)
435	\| (Finite s, Cofinite t) -> Cofinite (SList.diff t s)
436	\| (Cofinite s, Finite t) -> Cofinite (SList.diff s t)
437	\| (Cofinite s, Cofinite t) -> Cofinite (SList.cap s t)
438
439	let cap s t =
440	match (s,t) with
441	\| (Finite s, Finite t) -> Finite (SList.cap s t)
442	\| (Finite s, Cofinite t) -> Finite (SList.diff s t)
443	\| (Cofinite s, Finite t) -> Finite (SList.diff t s)
444	\| (Cofinite s, Cofinite t) -> Cofinite (SList.cup s t)
445
446	let diff s t =
447	match (s,t) with
448	\| (Finite s, Cofinite t) -> Finite (SList.cap s t)
449	\| (Finite s, Finite t) -> Finite (SList.diff s t)
450	\| (Cofinite s, Cofinite t) -> Finite (SList.diff t s)
451	\| (Cofinite s, Finite t) -> Cofinite (SList.cup s t)
452
453	let neg = function
454	\| Finite s -> Cofinite s
455	\| Cofinite s -> Finite s
456
457	let contains x = function
458	\| Finite s -> SList.mem s x
459	\| Cofinite s -> not (SList.mem s x)
460
461	let disjoint s t =
462	match (s,t) with
463	\| (Finite s, Finite t) -> SList.disjoint s t
464	\| (Finite s, Cofinite t) -> SList.subset s t
465	\| (Cofinite s, Finite t) -> SList.subset t s
466	\| (Cofinite s, Cofinite t) -> false
467
468	let is_empty = function Finite [] -> true \| _ -> false
469	end
470
471	module FiniteCofiniteMap(X : Custom.T)(SymbolSet : FiniteCofinite) =
472	struct
473	include Custom.Dummy
474
475	module T0 = Make(X)
476	module TMap = T0.MakeMap(SymbolSet)
477	module T = T0.Map
478	type t = Finite of TMap.t \| Cofinite of TMap.t
479
480	let get = function
481	\| Finite l -> `Finite (T.get l)
482	\| Cofinite l -> `Cofinite (T.get l)
483
484	let check = function
485	\| Finite l \| Cofinite l -> TMap.check l
486
487	let dump ppf = function
488	\| Finite s -> Format.fprintf ppf "Finite[%a]" TMap.dump s
489	\| Cofinite s -> Format.fprintf ppf "Cofinite[%a]" TMap.dump s
490
491	let serialize t = function
492	\| Finite s -> Serialize.Put.bool t true; TMap.serialize t s
493	\| Cofinite s -> Serialize.Put.bool t false; TMap.serialize t s
494
495	let deserialize t =
496	if Serialize.Get.bool t
497	then Finite (TMap.deserialize t)
498	else Cofinite (TMap.deserialize t)
499
500
501
502	let empty = Finite T.empty
503	let any = Cofinite T.empty
504	let any_in_ns ns = Finite (T.singleton ns SymbolSet.any)
505
506	let finite l =
507	let l =
508	T.filter
509	(fun _ x -> match x with SymbolSet.Finite [] -> false \| _ -> true)
510	l in
511	Finite l
512
513	let cofinite l =
514	let l =
515	T.filter
516	(fun _ x -> match x with SymbolSet.Cofinite [] -> false \| _ -> true)
517	l in
518	Cofinite l
519
520
521	let atom (ns,x) = Finite (T.singleton ns (SymbolSet.atom x))
522
523	let cup s t =
524	match (s,t) with
525	\| (Finite s, Finite t) -> finite (T.merge SymbolSet.cup s t)
526	\| (Finite s, Cofinite t) -> cofinite (T.sub SymbolSet.diff t s)
527	\| (Cofinite s, Finite t) -> cofinite (T.sub SymbolSet.diff s t)
528	\| (Cofinite s, Cofinite t) -> cofinite (T.cap SymbolSet.cap s t)
529
530	let cap s t =
531	match (s,t) with
532	\| (Finite s, Finite t) -> finite (T.cap SymbolSet.cap s t)
533	\| (Finite s, Cofinite t) -> finite (T.sub SymbolSet.diff s t)
534	\| (Cofinite s, Finite t) -> finite (T.sub SymbolSet.diff t s)
535	\| (Cofinite s, Cofinite t) -> cofinite (T.merge SymbolSet.cup s t)
536
537	let diff s t =
538	match (s,t) with
539	\| (Finite s, Cofinite t) -> finite (T.cap SymbolSet.cap s t)
540	\| (Finite s, Finite t) -> finite (T.sub SymbolSet.diff s t)
541	\| (Cofinite s, Cofinite t) -> finite (T.sub SymbolSet.diff t s)
542	\| (Cofinite s, Finite t) -> cofinite (T.merge SymbolSet.cup s t)
543
544	let is_empty = function
545	\| Finite l -> T.is_empty l
546	\| _ -> false
547
548	let hash = function
549	\| Finite l -> 1 + 17 * (TMap.hash l)
550	\| Cofinite l -> 2 + 17 * (TMap.hash l)
551
552	let compare l1 l2 =
553	match (l1,l2) with
554	\| Finite l1, Finite l2
555	\| Cofinite l1, Cofinite l2 -> TMap.compare l1 l2
556	\| Finite _, Cofinite _ -> -1
557	\| _ -> 1
558
559	let equal t1 t2 =
560	compare t1 t2 = 0
561
562	let symbol_set ns = function
563	\| Finite s ->
564	(try T.assoc ns s with Not_found -> SymbolSet.empty)
565	\| Cofinite s ->
566	(try SymbolSet.neg (T.assoc ns s) with Not_found -> SymbolSet.any)
567
568	let contains (ns,x) = function
569	\| Finite s ->
570	(try SymbolSet.contains x (T.assoc ns s) with Not_found -> false)
571	\| Cofinite s ->
572	(try not (SymbolSet.contains x (T.assoc ns s)) with Not_found -> true)
573
574	let disjoint s t =
575	is_empty (cap t s) (* TODO: OPT *)
576
577	end