sortedList.ml 16 KB
Newer Older
1
2
3
4
5
6
7
8
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
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30

  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

31

32
33
34
35
36
37
38
  let iter = List.iter

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


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

  let pick = function x::_ -> Some x | _ -> None 
43
  let choose = function x::_ -> x | _ -> raise Not_found
44
45
46
47
48
  let length = List.length

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

49
let rec disjoint l1 l2 =
50
  if l1 == l2 then l1 == [] else
51
52
  match (l1,l2) with
    | (t1::q1, t2::q2) -> 
53
	let c = X.compare t1 t2 in
54
55
56
57
58
59
	if c < 0 then disjoint q1 l2
	else if c > 0 then disjoint l1 q2
	else false
    | _ -> true
	
let rec cup l1 l2 =
60
  if l1 == l2 then l1 else
61
62
  match (l1,l2) with
    | (t1::q1, t2::q2) ->
63
	let c = X.compare t1 t2 in
64
65
66
67
68
69
70
71
72
73
74
	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) ->
75
	let c = X.compare t1 t2 in
76
77
78
79
80
81
82
	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 =
83
  if l1 == l2 then [] else
84
85
  match (l1,l2) with
    | (t1::q1, t2::q2) ->
86
	let c = X.compare t1 t2 in
87
88
89
90
91
	if c = 0 then diff q1 q2
	else if c < 0 then t1::(diff q1 l2)
	else diff l1 q2
    | _ -> l1

92
93
let remove x l = diff l [x]

94
let rec cap l1 l2 =
95
  if l1 == l2 then l1 else
96
97
  match (l1,l2) with
    | (t1::q1, t2::q2) ->
98
	let c = X.compare t1 t2 in
99
100
101
102
103
104
105
	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 =
106
  (l1 == l2) ||
107
108
  match (l1,l2) with
    | (t1::q1, t2::q2) ->
109
	let c = X.compare t1 t2 in
110
111
112
113
114
115
116
117
118
119
	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
	)
120
121
	else if c < 0 then false
	else subset l1 q2
122
    | [],_ -> true | _ -> false
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
	
	
	
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)

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


146
147
148
149
let rec mem l x =
  match l with
    | [] -> false
    | t::q -> 
150
        let c = X.compare x t in
151
152
        (c = 0) || ((c > 0) && (mem q x))

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

160
  let length = List.length
161
162
  let domain l = List.map fst l

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

167
168
169
170
  let rec iteri f = function
    | (x,y)::l -> f x y; iteri f l
    | [] -> ()

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

175
176
177
  let rec assoc_remove_aux v r = function
    | ((x,y) as a)::l ->
	let c = X.compare x v in
178
	if c = 0 then (r := Some y; l) 
179
180
181
182
183
	else if c < 0 then a :: (assoc_remove_aux v r l)
	else raise Not_found
    | [] -> raise Not_found

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

188
189
190
191
192
193
194
195
196
197
(* 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
    | [] -> []

198
199
200
201
202
203
204
205
206
207
  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

208
209
210
211
212
213
214
215
216
217
  let rec combine f1 f2 f12 l1 l2 =
    match (l1,l2) with
      | (x1,y1)::q1, (x2,y2)::q2 ->
          let c = X.compare x1 x2 in
          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

218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
  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

236
237
238
239
240
241
242
243
244
245
246
247
248
249
250
251
252
253
254
255
256
257
  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

258
259
260
261
262
263
264
265
266
  let rec restrict l1 l2 =
    match (l1,l2) with
      | (((x1,y1) as t1)::q1, x2::q2) ->
          let c = X.compare x1 x2 in
          if c = 0 then t1::(restrict q1 q2)
          else if c < 0 then restrict q1 l2
          else restrict l1 q2
      | _ -> []

267
268
269
270
271
272
273
274
275
276
277
278
279
  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)

280
281
282
283
284
285
286
287
288
289
290
291
292
  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)

293
294
295
296
297
298
299
300
301
302
  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

303
304
305
306
307
308
309
  let rec may_collide f exn l1 l2 =
    match (l1,l2) with
      | (x1,y1)::l1, (x2,y2)::l2 when X.compare x1 x2 = 0 ->
	  f y1 y2; may_collide f exn l1 l2
      | [], [] -> ()
      | _ -> raise exn

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

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

318
319
320
321
322
323
324
325
326
327
328
329
330
331
332
333
334
335
336
337
338
339
  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

340
341
342
343
344
345
346
  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

347
348
349
350
351
352
353
354
355
356
  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

357
358
359
  let rec hash f = function
    | [] -> 1
    | (x,y)::l -> X.hash x + 17 * (f y) + 257 * (hash f l)
360
361
362
363
364
365
366
367

  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

368
369
370
371
372
373

  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)
374
375
376
377
378
379
380

  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
    | _ -> ()
381
    
382
383
end

384

385
386
387
388
389
390
391
392
  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 
393

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

397
398
399
400
401
402
    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)
403
  end
404
405
406



407
end
408

409
410
411
412
413
414
415
416
417
418
419
420
421
422
423
424
425
426
427
428
429
430
431
432
433
434
435
436
437
438
439
440
441
442
443
444
445
446
447
448
449
450
451
452
453
454
455
456
457
458
459
460
461
462
463
464
465
466
467
468
469
470
471
472
473
474
475
476
477
478
479
480
481
482
483
484
485
486
487
488
489
490
491
492
493
494
495
496
497
498
499
500
501
502
503
504
505
506
507
508
509
510
511
512
513
514
515
516
517
518
519
520
521
522
523
524
525
526
527
528
529
530
531
532
533
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
563
564
565
566
567
568
569
570
571
572
573
574
575
576
577
578
579
580
581
582
583
584
585
586
587
588
589
590
591
592
593
594
595
596
597
598
599
600
601
602
603
604
605
606
607
608
609
610
611
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