Source

ocaml-lib / intreln.ml

Full commit
  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
 67
 68
 69
 70
 71
 72
 73
 74
 75
 76
 77
 78
 79
 80
 81
 82
 83
 84
 85
 86
 87
 88
 89
 90
 91
 92
 93
 94
 95
 96
 97
 98
 99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
244
245
246
247
248
249
250
251
252
253
254
255
256
257
258
259
260
261
262
263
264
265
266
267
268
269
270
271
272
273
274
275
276
277
278
279
280
281
282
283
284
285
286
287
288
289
290
291
292
293
294
295
296
297
298
299
300
301
302
303
304
305
306
307
308
309
310
311
312
313
314
315
316
317
318
319
320
321
322
323
324
325
326
327
328
329
330
331
332
333
334
335
336
337
338
339
340
341
342
343
344
345
346
347
348
349
350
351
352
353
354
355
356
357
358
359
360
361
362
363
364
365
366
367
368
369
370
371
372
373
374
375
376
377
378
379
380
381
382
383
384
385
386
387
388
389
390
391
392
393
394
395
396
397
398
399
400
401
402
403
404
405
406
407
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

module Mask =
  struct
    type t = bool list
    let dim bs = List.length bs
    let size bs = List.fold_left (fun res b -> if b then res + 1 else res) 0 bs
  end

module type T =
  sig
    type t
    exception Invalid_dimension
    val dim : t -> int
    val empty : int -> t
    val is_empty : t -> bool
    val cardinal : t -> int
    val mem : int list -> t -> bool
    val singleton : int list -> t
    val add : int list -> t -> t
    val remove : int list -> t -> t
    val union : t -> t -> t
    val inter : t -> t -> t
    val diff : t -> t -> t
    val union_r : t list -> t
    val inter_r : t list -> t
    val fold : ('a -> int list -> 'a) -> 'a -> t -> 'a
    val fold_mu : (string * int) list -> string list -> ('a -> (string * int) list -> 'a) -> 'a -> t -> 'a
    val fold_restr : (string * int) list -> string list -> ('a -> (string * int) list -> 'a) -> 'a -> t -> 'a
    val filter_restr : (string * int) list -> string list -> ((string * int) list -> bool) -> t -> t
    val iter : (int list -> unit) -> t -> unit

    val project : Mask.t -> t -> t
    val group_by : Mask.t -> t -> t
    val restriction : int -> ?filter:(int list -> t -> bool) -> t -> t
	(* restriction k (int^(n-k) -> t_k -> bool) t_n -> t_(n-k) *)
    val extension : int -> (int list -> t) -> t -> t
	(* extension k (int^n -> t_k) -> t_n -> t_(n+k) *)

    val memory_size : t -> int
  end

module Intmap : T =
  struct
    module M = Intmap.M

    type t = {dim : int; data : Obj.t}

    exception Invalid_dimension
	
    (* utilities *)

    type obj = R0 of bool | R1 of unit M.t | Rn of int * Obj.t M.t
	
    let repr = function
      | R0 b -> if b then Obj.repr () else Obj.repr M.empty
      | R1 s -> Obj.repr s
      | Rn (_,m) -> Obj.repr m
	    
    let obj n d =
      if n = 0 then R0 (d = Obj.repr ())
      else if n = 1 then R1 (Obj.obj d : unit M.t)
      else Rn (n, (Obj.obj d : Obj.t M.t))
	  
    let split xs = List.hd xs, List.tl xs

    (* public interface *)

    let dim r = r.dim
	
    let rec empty n =
      {dim = n; data = repr (empty_obj n)}
    and empty_obj n =
      if n = 0 then R0 false
      else if n = 1 then R1 M.empty
      else Rn (n,M.empty)
	  
    let rec is_empty r = is_empty_obj (obj r.dim r.data) (*r.data = Obj.repr M.empty*)
    and is_empty_obj = function
      | R0 b -> not b
      | R1 s -> M.is_empty s
      | Rn (n,m) -> M.is_empty m
	
    let rec cardinal r = Common.prof "Intreln.cardinal" (fun () ->
      cardinal_obj (obj r.dim r.data))
    and cardinal_obj = function
      | R0 b -> if b then 1 else 0
      | R1 s -> M.cardinal s
      | Rn (n, m) -> M.fold (fun res x d1 -> res + cardinal_obj (obj (n-1) d1)) 0 m
	    
    let rec mem xs r = Common.prof "Intreln.mem" (fun () ->
      if List.length xs = r.dim
      then mem_obj xs (obj r.dim r.data)
      else raise Invalid_dimension)
    and mem_obj xs = function
      | R0 b -> b
      | R1 s -> M.mem (List.hd xs) s
      | Rn (n, m) ->
	  let x, xs1 = split xs in
	  try mem_obj xs1 (obj (n-1) (M.get x m))
	  with Not_found -> false

    let rec singleton xs = Common.prof "Intreln.singleton" (fun () ->
      let n = List.length xs in
      {dim = n; data = repr (singleton_obj n xs)})
    and singleton_obj n = function
      | [] -> R0 true
      | [x] -> R1 (M.singleton x)
      | x::xs1 -> Rn (n, M.set x (repr (singleton_obj (n-1) xs1)) M.empty)
	      
    let rec add xs r = Common.prof "Intreln.add" (fun () ->
      if List.length xs = r.dim
      then {r with data = repr (add_obj xs (obj r.dim r.data))}
      else raise Invalid_dimension)
    and add_obj xs = function
      | R0 _ -> R0 true
      | R1 s -> R1 (M.add (List.hd xs) s)
      | Rn (n,m) ->
	  let n1 = n-1 in
	  let x, xs1 = split xs in
	  let d1 = try obj n1 (M.get x m) with Not_found -> empty_obj n1 in
	  Rn (n, M.set x (repr (add_obj xs1 d1)) m)

    let rec remove xs r = Common.prof "Intreln.remove" (fun () ->
      if List.length xs = r.dim
      then {r with data = repr (remove_obj xs (obj r.dim r.data))}
      else raise Invalid_dimension)
    and remove_obj xs = function
      | R0 _ -> R0 false
      | R1 s -> R1 (M.remove (List.hd xs) s)
      | Rn (n,m) ->
	  let x, xs1 = split xs in
	  try
	    let d1' = remove_obj xs1 (obj (n-1) (M.get x m)) in
	    if is_empty_obj d1'
	    then Rn (n, M.remove x m)
	    else Rn (n, M.set x (repr d1') m)
	  with Not_found ->
	    Rn (n,m)

    let rec union r1 r2 = Common.prof "Intreln.union" (fun () ->
      if r1.dim = r2.dim
      then {dim = r1.dim; data = repr (union_obj (obj r1.dim r1.data) (obj r2.dim r2.data))}
      else raise Invalid_dimension)
    and union_obj d1 d2 =
      match d1, d2 with
      | R0 b1, R0 b2 -> R0 (b1 || b2)
      | R1 s1, R1 s2 -> R1 (M.domain_union s1 s2)
      | Rn (n,m1), Rn (_,m2) ->
	  let n1 = n-1 in
	  Rn (n,
	      M.map_union
		(fun x d1_opt d2_opt ->
		  match d1_opt, d2_opt with
		  | None, None -> None
		  | Some _, None -> d1_opt
		  | None, Some _ -> d2_opt
		  | Some d1, Some d2 -> Some (repr (union_obj (obj n1 d1) (obj n1 d2))))
		m1 m2)
      | _, _ -> assert false

    let rec inter r1 r2 = Common.prof "Intreln.inter" (fun () ->
      if r1.dim = r2.dim
      then {dim = r1.dim; data = repr (inter_obj (obj r1.dim r1.data) (obj r2.dim r2.data))}
      else raise Invalid_dimension)
    and inter_obj d1 d2 =
      match d1, d2 with
      | R0 b1, R0 b2 -> R0 (b1 && b2)
      | R1 s1, R1 s2 -> R1 (M.domain_inter s1 s2)
      | Rn (n,m1), Rn (_,m2) ->
	  let n1 = n-1 in
	  Rn (n,
	      M.map_inter
		(fun x d1 d2 ->
		  let d = inter_obj (obj n1 d1) (obj n1 d2) in
		  if is_empty_obj d
		  then None
		  else Some (repr d))
		m1 m2)
      | _, _ -> assert false

    let rec diff r1 r2 = Common.prof "Intreln.diff" (fun () ->
      if r1.dim = r2.dim
      then {dim = r1.dim; data = repr (diff_obj (obj r1.dim r1.data) (obj r2.dim r2.data))}
      else raise Invalid_dimension)
    and diff_obj d1 d2 =
      match d1, d2 with
      | R0 b1, R0 b2 -> R0 (b1 && not b2)
      | R1 s1, R1 s2 -> R1 (M.domain_diff s1 s2)
      | Rn (n,m1), Rn (_,m2) ->
	  let n1 = n-1 in
	  Rn (n,
	      M.map_diff
		(fun x d1 d2_opt ->
		  match d2_opt with
		  | None -> Some d1
		  | Some d2 ->
		      let d = diff_obj (obj n1 d1) (obj n1 d2) in
		      if is_empty_obj d
		      then None
		      else Some (repr d))
		m1 m2)
      | _, _ -> assert false

    let union_r = function
      | [] -> invalid_arg "Intreln.Intmap.union_r: empty list of relations"
      | r::rs -> List.fold_left union r rs

    let inter_r = function
      | [] -> invalid_arg "Intreln.Intmap.inter_r : empty list of relations"
      | r::rs -> List.fold_left inter r rs

    let rec fold f init r = Common.prof "Intreln.fold" (fun () ->
      fold_obj f init [] (obj r.dim r.data))
    and fold_obj f acc xs = function
      | R0 b -> if b then f acc [] else acc
      | R1 s -> M.fold (fun res x _ -> f res (List.rev (x::xs))) acc s
      | Rn (n,m) ->
	  let n1 = n-1 in
	  M.fold
	    (fun res x d1 ->
	      fold_obj f res (x::xs) (obj n1 d1))
	    acc m

    let rec fold_mu mu vs f init r = Common.prof "Intreln.fold_mu" (fun () ->
         (* "" variables must be ignored in generated mappings *)
      let rec aux = function ""::l -> aux l | l -> l in
      let vs_prefix = List.rev (aux (List.rev vs)) in
      fold_mu_obj f init mu vs_prefix (obj r.dim r.data))
    and fold_mu_obj f acc mu vs = function
      | R0 b ->
	  if b then f acc mu else acc
      | R1 s ->
	  ( match vs with
	  | [] -> f acc mu
	  | v::_ ->
	      (try
		let x = List.assoc v mu in
		if M.mem x s
		then f acc mu
		else acc
	      with Not_found ->
		M.fold
		  (fun res x _ ->
		    let mu' = if v="" then mu else (v,x)::mu in
		    f res mu')
		  acc s))
      | Rn (n,m) ->
	  let n1 = n-1 in
	  ( match vs with
	  | [] -> f acc mu
	  | v::vs1 ->
	      (try
		let x = List.assoc v mu in
		try
		  let d1 = M.get x m in
		  fold_mu_obj f acc mu vs1 (obj n1 d1)
		with Not_found ->
		  acc
	      with Not_found ->
		M.fold
		  (fun res x d1 ->
		    let mu' = if v="" then mu else (v,x)::mu in
		    fold_mu_obj f res mu' vs1 (obj n1 d1))
		  acc m))

    let rec project ps r = Common.prof "Intreln.project" (fun () ->
      if Mask.dim ps = r.dim
      then
	if Mask.size ps = r.dim
	then r
	else{dim = Mask.size ps;
	     data = repr (project_obj ps (obj r.dim r.data))}
      else raise Invalid_dimension)
    and project_obj ps = function
      | R0 b -> R0 b
      | R1 s ->
	  if List.hd ps
	  then R1 s
	  else R0 (not (M.is_empty s))
      | Rn (n,m) ->
	  let n1 = n-1 in
	  let p, ps1 = split ps in
	  let n' = Mask.size ps in
	  if p
	  then 
	    if n' = 1
	    then R1 (M.domain m)
	    else Rn (n', M.map (fun x d1 -> Some (repr (project_obj ps1 (obj n1 d1)))) m)
	  else
	    let n1' = Mask.size ps1 in
	    if n1' = 0
	    then R0 (not (M.is_empty m))
	    else M.fold (fun res x d1 -> union_obj res (project_obj ps1 (obj n1 d1))) (empty_obj n1') m

    let rec fold_restr mu vs f init r = Common.prof "Intreln.fold_restr" (fun () ->
         (* "" variables must be ignored in generated mappings *)
      let r' = project (List.map ((<>) "") vs) r in (* done to avoid doublons when folding *)
      let vs' = List.filter ((<>) "") vs in
      fold_restr_obj f init mu vs' (obj r'.dim r'.data))
    and fold_restr_obj f acc mu vs = function
      | R0 b -> if b then f acc mu else acc
      | R1 s ->
	  let v = List.hd vs in
	  (try
	    let x = List.assoc v mu in
	    if M.mem x s
	    then f acc mu
	    else acc
	  with Not_found ->
	    M.fold (fun res x _ -> f res ((v,x)::mu)) acc s)
      | Rn (n,m) ->
	  let n1 = n-1 in
	  let v = List.hd vs in
	  (try
	    let x = List.assoc v mu in
	    try
	      let d1 = M.get x m in
	      fold_restr_obj f acc mu (List.tl vs) (obj n1 d1)
	    with Not_found ->
	      acc
	  with Not_found ->
	    M.fold
	      (fun res x d1 ->
		fold_restr_obj f res ((v,x)::mu) (List.tl vs) (obj n1 d1))
	      acc m)

    let rec filter_restr mu vs f r = Common.prof "Intreln.filter_restr" (fun () ->
         (* "" variables must be ignored in generated mappings *)
      let r' = project (List.map ((<>) "") vs) r in (* done to avoid doublons when folding *)
      let vs' = List.filter ((<>) "") vs in
      {dim = List.length vs'; data = repr (filter_restr_obj f mu vs' (obj r'.dim r'.data))})
    and filter_restr_obj f mu vs = function
      | R0 b -> R0 (b && f mu)
      | R1 s ->
	  let v = List.hd vs in
	  (try
	    let x = List.assoc v mu in
	    if M.mem x s && f mu
	    then R1 s
	    else R1 M.empty
	  with Not_found ->
	    R1 (M.domain ~filter:(fun x _ -> f ((v,x)::mu)) s))
      | Rn (n,m) ->
	  let n1 = n-1 in
	  let v = List.hd vs in
	  (try
	    let x = List.assoc v mu in
	    try
	      let d1 = M.get x m in
	      let d1' = filter_restr_obj f mu (List.tl vs) (obj n1 d1) in
	      if is_empty_obj d1'
	      then Rn (n, M.remove x m)
	      else Rn (n, M.set x (repr d1') m)
	    with Not_found ->
	      Rn (n, m)
	  with Not_found ->
	    Rn (n,
		M.map
		  (fun x d1 ->
		    let d1' = filter_restr_obj f ((v,x)::mu) (List.tl vs) (obj n1 d1) in
		    if is_empty_obj d1'
		    then None
		    else Some (repr d1'))
		  m))

    let rec iter f r = Common.prof "Intreln.iter" (fun () ->
      iter_obj f [] (obj r.dim r.data))
    and iter_obj f xs = function
      | R0 b -> if b then f [] else ()
      | R1 s -> M.iter (fun x _ -> f (List.rev (x::xs))) s
      | Rn (n,m) ->
	  let n1 = n-1 in
	  M.iter
	    (fun x d1 ->
	      iter_obj f (x::xs) (obj n1 d1))
	    m


    let rec group_by ps r =
      if Mask.dim ps = r.dim
      then {dim = Mask.size ps;
	    data = repr (group_by_obj ps [] (obj r.dim r.data))}
      else raise Invalid_dimension
    and group_by_obj ps xs = function
      | R0 b ->
	  if b
	  then singleton_obj (List.length xs) (List.rev xs)
	  else R0 false
      | R1 s ->
	  if xs = []
	  then R1 s
	  else
	    let k = List.length xs in
	    if List.hd ps
	    then
	      let xs' = List.rev xs in
	      Rn (1+k, M.map (fun x _ -> Some (repr (singleton_obj k xs'))) s)
	    else
	      let k' = 1 + k in
	      M.fold (fun res x _ -> union_obj res (singleton_obj k' (List.rev (x::xs)))) (empty_obj k') s
      | Rn (n,m) ->
	  let n1 = n-1 in
	  let k = List.length xs in
	  let p, ps1 = split ps in
	  if p
	  then Rn (n+k, M.map (fun x d1 -> Some (repr (group_by_obj ps1 xs (obj n1 d1)))) m)
	  else M.fold (fun res x d1 -> union_obj res (group_by_obj ps1 (x::xs) (obj n1 d1))) (empty_obj (n+k)) m

    let rec restriction k ?(filter = fun xs r_k -> true) r =
      if k >= 0 && k <= r.dim
      then {dim = r.dim - k; data = repr (restriction_obj k filter [] (obj r.dim r.data))}
      else raise Invalid_dimension
    and restriction_obj k f xs = function
      | R0 b ->
	  if b
	  then R0 (f (List.rev xs) {dim=0; data=Obj.repr ()})
	  else R0 false
      | R1 s ->
	  if k = 1 then R0 (f (List.rev xs) {dim=1; data=Obj.repr s})
	  else (* k = 0 *)
	    R1 (M.domain ~filter:(fun x d1 -> f (List.rev (x::xs)) {dim=0; data=Obj.repr ()}) s)
      | Rn (n,m) ->
	  if k = n then R0 (f (List.rev xs) {dim=n; data=Obj.repr m})
	  else if k+1 = n then R1 (M.domain ~filter:(fun x d1 -> f (List.rev (x::xs)) {dim=k; data=d1}) m)
	  else
	    let n1 = n-1 in
	    Rn (n-k, M.map (fun x d1 -> Some (repr (restriction_obj k f (x::xs) (obj n1 d1)))) m)

    let rec extension k f r =
      if k >= 0
      then {dim = r.dim + k; data = repr (extension_obj k f [] (obj r.dim r.data))}
      else raise Invalid_dimension
    and extension_obj k f xs = function
      | R0 b ->
	  if b
	  then
	    let r_k = f xs in
	    if r_k.dim <> k then raise Invalid_dimension;
	    if is_empty r_k
	    then empty_obj k
	    else obj r_k.dim r_k.data
	  else empty_obj k
      | R1 s ->
	  if k = 0
	  then R1 (M.domain
		     ~filter:(fun x _ -> 
		       let r_k = f (List.rev (x::xs)) in
		       if r_k.dim <> k then raise Invalid_dimension;
		       not (is_empty r_k))
		     s)
	  else Rn (1+k,
		   M.map
		     (fun x _ ->
		       let r_k = f (List.rev (x::xs)) in
		       if r_k.dim <> k then raise Invalid_dimension;
		       if is_empty r_k
		       then None
		       else Some r_k.data)
		     s)
      | Rn (n,m) ->
	  let n1 = n-1 in
	  Rn (n + k,
	      M.map
		(fun x d1 ->
		  let d1_k = extension_obj k f (x::xs) (obj n1 d1) in
		  if is_empty_obj d1_k
		  then None
		  else Some (repr d1_k))
		m)

    let rec memory_size r =
      3 (* reference + tag + dim *)
	+ memory_size_obj (obj r.dim r.data)
    and memory_size_obj = function
      | R0 _ -> 1
      | R1 s -> M.memory_size s
      | Rn (n,m) -> M.memory_size ~f:(fun d1 -> memory_size_obj (obj (n-1) d1)) m

  end