sortedList.ml 19.3 KB
Newer Older
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 56 57 58 59 60 61 62 63 64 65 66
module type S =
sig
  module Elem : Custom.T
  include Custom.T with type t = private Elem.t list
  external get: t -> Elem.t list = "%identity"

  val singleton: Elem.t -> t
  val iter: (Elem.t -> unit) -> t -> unit
  val filter: (Elem.t -> bool) -> t -> t
  val exists: (Elem.t -> bool) -> t -> bool
  val fold: ('a -> Elem.t -> 'a) -> 'a -> t -> 'a
  val pick: t -> Elem.t option
  val choose: t -> Elem.t
  val length: t -> int

  val empty: t
  val is_empty: t -> bool
  val from_list : Elem.t list -> t
  val add: Elem.t -> t -> t
  val remove: Elem.t -> t -> t
  val disjoint: t -> t -> bool
  val cup: t -> t -> t
  val split: t -> t -> t * t * t
    (* split l1 l2 = (l1 \ l2, l1 & l2, l2 \ l1) *)
  val cap:  t -> t -> t
  val diff: t -> t -> t
  val subset: t -> t -> bool
  val map: (Elem.t -> Elem.t) -> t -> t
  val mem: t -> Elem.t -> bool

  module Map: sig
    type 'a map
    external get: 'a map -> (Elem.t * 'a) list = "%identity"
    val add: Elem.t -> 'a -> 'a map -> 'a map
    val mem: Elem.t -> 'a map -> bool
    val length: 'a map -> int
    val domain: 'a map -> t
    val restrict: 'a map -> t -> 'a map
    val empty: 'a map
    val fold: (Elem.t -> 'a -> 'b -> 'b) -> 'a map -> 'b -> 'b
    val iter: ('a -> unit) -> 'a map -> unit
    val iteri: (Elem.t -> 'a -> unit) -> 'a map -> unit
    val filter: (Elem.t -> 'a -> bool) -> 'a map -> 'a map
    val is_empty: 'a map -> bool
    val singleton: Elem.t -> 'a -> 'a map
    val assoc_remove: Elem.t -> 'a map -> 'a * 'a map
    val remove:  Elem.t -> 'a map -> 'a map
    val merge: ('a -> 'a -> 'a ) -> 'a map -> 'a map -> 'a map
    val combine: ('a -> 'c) -> ('b -> 'c) -> ('a -> 'b -> 'c) ->
      'a map -> 'b map -> 'c map
    val cap: ('a -> 'a -> 'a ) -> 'a map -> 'a map -> 'a map
    val sub: ('a -> 'a -> 'a ) -> 'a map -> 'a map -> 'a map

    val merge_elem: 'a -> 'a map -> 'a map -> 'a map
    val union_disj: 'a map -> 'a map -> 'a map
    val diff: 'a map -> t -> 'a map
    val from_list: ('a -> 'a -> 'a ) -> (Elem.t * 'a) list -> 'a map
    val from_list_disj: (Elem.t * 'a) list -> 'a map

    val map_from_slist: (Elem.t -> 'a) -> t -> 'a map
    val collide: ('a -> 'b -> unit) -> 'a map -> 'b map -> unit
    val may_collide: ('a -> 'b -> unit) -> exn -> 'a map -> 'b map -> unit
    val map: ('a -> 'b) -> 'a map -> 'b map
    val mapi: (Elem.t -> 'a -> 'b) -> 'a map -> 'b map
    val constant: 'a -> t -> 'a map
    val num: int -> t -> int map
67
    val init : (Elem.t -> 'a) -> t -> 'a map
68 69 70 71 72 73 74 75 76 77 78 79 80
    val map_to_list: ('a -> 'b) -> 'a map -> 'b list
    val mapi_to_list: (Elem.t -> 'a -> 'b) -> 'a map -> 'b list
    val assoc: Elem.t -> 'a map -> 'a
    val assoc_present:  Elem.t -> 'a map -> 'a
    val compare: ('a -> 'a -> int) -> 'a map -> 'a map -> int
    val hash: ('a -> int) -> 'a map -> int
    val equal: ('a -> 'a -> bool) -> 'a map -> 'a map -> bool
  end
  module MakeMap(Y : Custom.T) : sig
    include Custom.T with type t = Y.t Map.map
  end
end

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

88 89 90
  let rec equal l1 l2 =
    (l1 == l2) ||
    match (l1,l2) with
91
      | x1::l1, x2::l2 -> (Elem.equal x1 x2) && (equal l1 l2)
92 93 94 95
      | _ -> false

  let rec hash accu = function
    | [] -> 1 + accu
96
    | x::l -> hash (17 * accu + Elem.hash x) l
97 98 99 100

  let hash l = hash 1 l

  let rec compare l1 l2 =
101
    if l1 == l2 then 0
102
    else match (l1,l2) with
103
      | x1::l1, x2::l2 ->
104
	  let c = Elem.compare x1 x2 in if c <> 0 then c
105 106 107 108
	  else compare l1 l2
      | [],_ -> -1
      | _ -> 1

109

110 111 112 113 114 115
  let iter = List.iter

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

116
  external get: t -> Elem.t list = "%identity"
117 118
  let singleton x = [ x ]

119
  let pick = function x::_ -> Some x | _ -> None
120
  let choose = function x::_ -> x | _ -> raise Not_found
121 122 123 124 125
  let length = List.length

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

126 127
  let rec disjoint l1 l2 =
    if l1 == l2 then l1 == [] else
128
    match (l1,l2) with
129
      | (t1::q1, t2::q2) ->
130
        let c = Elem.compare t1 t2 in
131 132 133 134
        if c < 0 then disjoint q1 l2
        else if c > 0 then disjoint l1 q2
        else false
      | _ -> true
135

136 137
  let rec cup l1 l2 =
    if l1 == l2 then l1 else
138
    match (l1,l2) with
139
      | (t1::q1, t2::q2) ->
140
        let c = Elem.compare t1 t2 in
141 142 143
        if c = 0 then t1::(cup q1 q2)
        else if c < 0 then t1::(cup q1 l2)
        else t2::(cup l1 q2)
144 145 146
      | ([],l2) -> l2
      | (l1,[]) -> l1

147
  let add x l = cup [x] l
148

149 150 151
  let rec split l1 l2 =
    match (l1,l2) with
      | (t1::q1, t2::q2) ->
152
        let c = Elem.compare t1 t2 in
153 154 155 156
        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)
157 158


159
  let rec diff l1 l2 =
160
    if l1 == l2 then [] else
161
    match (l1,l2) with
162
      | (t1::q1, t2::q2) ->
163
        let c = Elem.compare t1 t2 in
164 165 166
        if c = 0 then diff q1 q2
        else if c < 0 then t1::(diff q1 l2)
        else diff l1 q2
167 168
      | _ -> l1

169 170 171 172
  let remove x l = diff l [x]

  let rec cap l1 l2 =
    if l1 == l2 then l1 else
173
    match (l1,l2) with
174
      | (t1::q1, t2::q2) ->
175
        let c = Elem.compare t1 t2 in
176 177 178
        if c = 0 then t1::(cap q1 q2)
        else if c < 0 then cap q1 l2
        else cap l1 q2
179 180
      | _ -> []

181

182 183 184 185
  let rec subset l1 l2 =
    (l1 == l2) ||
    match (l1,l2) with
      | (t1::q1, t2::q2) ->
186
        let c = Elem.compare t1 t2 in
187 188 189 190
        if c = 0 then (
  (* inlined: subset q1 q2 *)
          (q1 == q2) || match (q1,q2) with
            | (t1::qq1, t2::qq2) ->
191
              let c = Elem.compare t1 t2 in
192 193 194 195 196 197 198 199
              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
200 201

  let from_list l =
202 203 204 205
    let rec initlist = function
      | [] -> []
      | e::rest -> [e] :: initlist rest in
    let rec merge2 = function
206
      | l1::l2::rest -> cup l1 l2 :: merge2 rest
207 208 209 210 211 212
      | x -> x in
    let rec mergeall = function
      | [] -> []
      | [l] -> l
      | llist -> mergeall (merge2 llist) in
    mergeall (initlist l)
213

214 215 216 217 218 219
  let map f l =
    from_list (List.map f l)

  let rec mem l x =
    match l with
      | [] -> false
220
      | t::q ->
221
          let c = Elem.compare x t in
222 223 224
          (c = 0) || ((c > 0) && (mem q x))

  module Map = struct
225 226
    type 'a map = (Elem.t * 'a) list
    external get: 'a map -> (Elem.t * 'a) list = "%identity"
227 228 229 230 231 232 233 234 235 236 237 238 239 240 241 242 243 244 245 246
    let empty = []
    let is_empty l = l = []
    let singleton x y = [ (x,y) ]

    let fold f l acc = List.fold_left (fun tacc (k,v) -> f k v tacc) acc l

    let length = List.length
    let domain l = List.map fst l

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

    let rec iteri f = function
      | (x,y)::l -> f x y; iteri 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
      | [] -> []
247

248 249
    let rec assoc_remove_aux v r = function
      | ((x,y) as a)::l ->
250
        let c = Elem.compare x v in
251
        if c = 0 then (r := Some y; l)
252 253 254 255 256 257 258 259 260
        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

Pietro Abate's avatar
Pietro Abate committed
261
  (* TODO: is it faster to raise exception Not_found and return
262 263 264
     original list ? *)
    let rec remove v = function
      | (((x,y) as a)::rem) as l->
265
        let c = Elem.compare x v in
266 267 268
        if c = 0 then rem
        else if c < 0 then a :: (remove v rem)
        else l
269
      | [] -> []
270 271 272 273

    let rec merge f l1 l2 =
      match (l1,l2) with
        | ((x1,y1) as t1)::q1, ((x2,y2) as t2)::q2 ->
274
            let c = Elem.compare x1 x2 in
275 276 277 278 279 280 281 282 283
            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 combine f1 f2 f12 l1 l2 =
      match (l1,l2) with
        | (x1,y1)::q1, (x2,y2)::q2 ->
284
            let c = Elem.compare x1 x2 in
285 286 287 288 289 290 291 292 293
            if c = 0 then (x1,(f12 y1 y2))::(combine f1 f2 f12 q1 q2)
            else if c < 0 then (x1,f1 y1)::(combine f1 f2 f12 q1 l2)
            else (x2, f2 y2)::(combine f1 f2 f12 l1 q2)
        | [], l2 -> List.map (fun (x2,y2) -> (x2,f2 y2)) l2
        | l1, [] -> List.map (fun (x1,y1) -> (x1,f1 y1)) l1

    let rec cap f l1 l2 =
      match (l1,l2) with
        | (x1,y1)::q1, (x2,y2)::q2 ->
294
            let c = Elem.compare x1 x2 in
295 296 297 298 299 300 301 302
            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)::q2 ->
303
            let c = Elem.compare x1 x2 in
304 305 306 307 308 309 310 311 312 313 314
            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 ->
315
            let c = Elem.compare x1 x2 in
316 317 318 319 320 321 322 323
            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 add x v = union_disj [(x,v)]

324 325 326
    let rec mem x l =
      match l with
        | [] -> false
327
        | (t,_)::q ->
328
            let c = Elem.compare x t in
329
            (c = 0) || ((c > 0) && (mem x q))
330 331 332 333

    let rec diff l1 l2 =
      match (l1,l2) with
        | (((x1,y1) as t1)::q1, x2::q2) ->
334
            let c = Elem.compare x1 x2 in
335 336 337 338 339 340 341 342
            if c = 0 then diff q1 q2
            else if c < 0 then t1::(diff q1 l2)
            else diff l1 q2
        | _ -> l1

    let rec restrict l1 l2 =
      match (l1,l2) with
        | (((x1,y1) as t1)::q1, x2::q2) ->
343
            let c = Elem.compare x1 x2 in
344 345 346 347 348
            if c = 0 then t1::(restrict q1 q2)
            else if c < 0 then restrict q1 l2
            else restrict l1 q2
        | _ -> []

349
    let from_list f l =
350 351 352 353 354 355 356 357 358 359 360 361
      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)

362
    let from_list_disj l =
363 364 365 366 367 368 369 370 371 372 373 374 375 376 377
      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)
      | [] -> []
378

379 380 381 382 383 384 385 386
    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 may_collide f exn l1 l2 =
      match (l1,l2) with
387
        | (x1,y1)::l1, (x2,y2)::l2 when Elem.compare x1 x2 = 0 ->
388 389 390 391 392 393
          f y1 y2; may_collide f exn l1 l2
        | [], [] -> ()
        | _ -> raise exn

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

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

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

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

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

410 411 412 413
    let rec init f = function
           [] -> []
      | x :: l -> (x, f x) :: (init f l)

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

418 419
    let rec assoc v = function
      | (x,y)::l ->
420
        let c = Elem.compare x v in
421
        if c = 0 then y
422 423 424 425 426 427 428
        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 ->
429
        let c = Elem.compare x v in
430 431 432 433
        if c = 0 then y else assoc_present v l
      | [] -> assert false

    let rec compare f l1 l2 =
434
      if l1 == l2 then 0
435 436
      else match (l1,l2) with
        | (x1,y1)::l1, (x2,y2)::l2 ->
437
          let c = Elem.compare x1 x2 in if c <> 0 then c
438 439 440 441 442 443 444
          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
445
      | (x,y)::l -> Elem.hash x + 17 * (f y) + 257 * (hash f l)
446 447 448 449 450

    let rec equal f l1 l2  =
      (l1 == l2) ||
      match (l1,l2) with
        | (x1,y1)::l1, (x2,y2)::l2 ->
451
          (Elem.equal x1 x2) && (f y1 y2) && (equal f l1 l2)
452 453 454 455
        | _ -> false


    let rec check f = function
456
      | (x,a)::((y,b)::_ as tl) ->
457 458 459
        Elem.check x; f a;
        assert (Elem.compare x y < 0); check f tl
      | [x,a] -> Elem.check x; f a
460
      | _ -> ()
461 462

  end (* Map *)
463

464

465 466 467 468 469 470 471
  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
472
    let equal x y = Map.equal Y.equal x y
473

474
    let check l = Map.check Y.check l
475
    let dump ppf l =
476
      List.iter (fun (x,y) ->
477
		   Format.fprintf ppf "(%a->%a)" Elem.dump x Y.dump y) l
478

479
  end
480

481
end (* Make(X : Custom.T) *)
482

483 484


485 486 487 488 489 490 491 492 493 494 495 496 497 498 499
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
500
  val sample: t -> elem option
501 502 503 504 505 506 507 508 509 510 511 512 513 514
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
515
      | Finite l1, Finite l2
516 517 518 519 520 521 522 523 524 525 526 527 528
      | Cofinite l1, Cofinite l2 -> SList.compare l1 l2
      | Finite _, Cofinite _ -> -1
      | _ -> 1

  let equal l1 l2 = compare l1 l2 = 0

   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

529 530 531 532 533
  let sample = function
    | Finite (x::_) -> Some x
    | Finite [] -> raise Not_found
    | Cofinite _ -> None

534 535 536 537 538 539 540 541 542 543 544 545 546 547 548 549 550 551 552 553 554 555 556 557 558 559 560 561 562

  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
563

564 565 566
  let contains x = function
    | Finite s -> SList.mem s x
    | Cofinite s -> not (SList.mem s x)
567

568 569 570 571 572 573 574 575 576 577 578 579 580 581 582 583 584 585 586
  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

587 588
  let sample = function
    | Cofinite _ -> None
589
    | Finite l -> (match T.get l with
590 591 592
		     | [] -> raise Not_found
		     | (x,y)::_ -> Some (x, SymbolSet.sample y))

593 594 595
  let get = function
    | Finite l -> `Finite (T.get l)
    | Cofinite l -> `Cofinite (T.get l)
596

597 598
  let check = function
    | Finite l | Cofinite l -> TMap.check l
599

600 601 602
  let dump ppf = function
    | Finite s -> Format.fprintf ppf "Finite[%a]" TMap.dump s
    | Cofinite s -> Format.fprintf ppf "Cofinite[%a]" TMap.dump s
603

604 605 606
  let empty = Finite T.empty
  let any   = Cofinite T.empty
  let any_in_ns ns = Finite (T.singleton ns SymbolSet.any)
607

608
  let finite l =
609 610
    let l =
      T.filter
611 612 613
	(fun _ x -> match x with SymbolSet.Finite [] -> false | _ -> true)
	l in
    Finite l
614

615
  let cofinite l =
616 617
    let l =
      T.filter
618
	(fun _ x -> match x with SymbolSet.Finite [] -> false | _ -> true)
619 620
	l in
    Cofinite l
621 622


623
  let atom (ns,x) = Finite (T.singleton ns (SymbolSet.atom x))
624

625 626 627 628 629 630
  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)
631

632 633 634 635 636 637
  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)
638

639 640 641 642 643 644
  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)
645

646 647
  let is_empty = function
    | Finite l -> T.is_empty l
648
    | _ -> false
649 650 651 652

  let hash = function
    | Finite l -> 1 + 17 * (TMap.hash l)
    | Cofinite l -> 2 +  17 * (TMap.hash l)
653

654 655
  let compare l1 l2 =
    match (l1,l2) with
656
      | Finite l1, Finite l2
657 658 659
      | Cofinite l1, Cofinite l2 -> TMap.compare l1 l2
      | Finite _, Cofinite _ -> -1
      | _ -> 1
660 661

  let equal t1 t2 =
662 663 664 665 666 667 668 669 670
    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
671
    | Finite s ->
672
	(try SymbolSet.contains x (T.assoc ns s) with Not_found -> false)
673
    | Cofinite s ->
674
	(try not (SymbolSet.contains x (T.assoc ns s)) with Not_found -> true)
675 676

  let disjoint s t =
677 678 679
    is_empty (cap t s) (* TODO: OPT *)

end