package exenum

  1. Overview
  2. Docs

Source file exen.ml

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
open Parts
open Convenience

(******************************************************************)
(*                  ENUMERATIONS                                  *)
(******************************************************************)

(* An enumeration *)
type 'a t = {
    (* Number of elements. None means infinity. *)
    cardinal : Z.t option ;
    
    (* Number of parts. None means infinity. *)
    n_parts  : int option ;

    (* An extensible array of parts, in order to compute parts lazily. *)
    parts : ('a part) ExtArray.t ;
    
    (* Function used to create a new part when necessary. *)
    new_part : (int -> 'a part) ;

    (* A title, mostly for debugging. *)
    title : string Lazy.t ;
  }

let cardinal exen = exen.cardinal

(******************************************************************)
(*             ACCESSING ENUMERATIONS                             *)
(******************************************************************)

(* Check that the required part index exists in the given enumeration. *)
let check_array_index index exen =
  match exen.n_parts with
  | None -> true
  | Some n -> index < n

(* Get (possibly by forcing evaluation) the part corresponding to the given index. *)
let get_part exen array_index =

  if check_array_index array_index exen then
    let part = ExtArray.get exen.parts array_index in

    let part =
      if part == uninitialized_part then
	begin
	  (* This cell is uninitialized. Set it first. *)
	  let newcell = exen.new_part array_index in
	  ExtArray.set exen.parts array_index newcell ;
	  newcell
	end  
      else
	part
    in

    part

  else
      empty_part

(* Find in which part of an enumearation an index holds. *)
let rec get_in_parts exen value_index array_index =

  let part = get_part exen array_index in

  (* Is the index in range of this part ? *)
  if part.p_cardinal <= value_index then
    (* No. Go to next part. *)
    get_in_parts exen (value_index -- part.p_cardinal) (array_index + 1)
  else
    (* OK. Get the value in this part. *)
    part.compute value_index

(* Gets a value, given an absolute index. *)
let get exen index =
  begin match exen.cardinal with
  | None -> ()
  | Some max -> 
      if max <= index then 
	failwith (Printf.sprintf "Exenum.get: index is out of bounds : %s / %s" (sob index) (sob (max -- bigone)))
  end ;
  
  get_in_parts exen index 0

(******************************************************************)
(*              BUILDING SIMPLE ENUMERATIONS                      *)
(******************************************************************)

(* An enumeration from a single part. *)
let from_single_part title a_part =
  let parts = ExtArray.create 1 empty_part in
  ExtArray.set parts 0 a_part ;  

  { cardinal = Some (a_part.p_cardinal) ;
    n_parts  = Some 1 ;
    parts ;
    (* This enumeration is finite. We should never need to create a new cell. *)
    new_part = (fun _ -> assert false) ;
    title }

(* An enumeration from a list of values. *)
let from_list ?(name="unnamed") values = from_single_part (lazy name) (part_from_list values)


(******************************************************************)
(*           ALGEBRAIC OPERATIONS ON ENUMERATIONS                 *)
(******************************************************************)

(* Pay *)
let pay l_exen =

  let parts = ExtArray.create 1 uninitialized_part in
  ExtArray.set parts 0 empty_part ;

  (* On the first call to new_part, we will check that the argument function is indeed infinite. *)
  let is_infinite = lazy
      ((Lazy.force l_exen).cardinal = None)
  in

  let new_part array_index =
    assert (array_index > 0) ;
    assert (Lazy.force is_infinite) ;
    get_part (Lazy.force l_exen) (array_index - 1)
  in

  { cardinal = None ;
    n_parts = None ;
    parts ;
    new_part ;
    title = lazy ("pay (...)") }

(* Maps an enumeration *)
let map exen f = 

  let parts = ExtArray.create 1 uninitialized_part in

  let new_part array_index =
    let part = get_part exen array_index in
    map_part f part
  in

  { cardinal = exen.cardinal ;
    n_parts = exen.n_parts ;
    parts ;
    new_part ;
    title = lazy ("map (" ^ Lazy.force exen.title ^ ")") }


(* Finite sub-enumeration *)
let sub ~max exen =

  let newcardinal =
    match exen.cardinal with
    | None -> Some max
    | Some bound -> 
	if max <= bound then Some max
	else Some bound
  in

  { exen with cardinal = newcardinal }

(*** DISJOINT UNION ***)

(* Compute the possibly infinite sum of cardinals. *)
let rec sum_cardinals acu = function
  | [] -> Some acu
  | exen :: exens ->
      begin match exen.cardinal with
      | None -> None (* Infinite *)
      | Some n -> sum_cardinals (acu ++ n) exens
      end

(* max, taking account of infinity (None) *)
let infmax a b =
  match (a,b) with
  | (None, _) | (_, None) -> None
  | (Some x, Some y) -> Some (max x y)

(* Returns the maximal number of parts of these enumerations. *)
let max_parts exens = myfold exens (Some 0) (fun acu exen -> infmax acu exen.n_parts)

(* Disjoint union of enumerations. *)
let union exens =
  let cardinal = sum_cardinals bigzero exens in  
  let parts = ExtArray.create 1 uninitialized_part in
  let new_part array_index = union_parts (List.map (fun ex -> get_part ex array_index) exens) in

  { cardinal ;
    n_parts = max_parts exens ;
    parts ;
    new_part ;
    title = lazy ("union (" ^ (sep (fun e -> Lazy.force e.title) ", " exens) ^ ")") }


(*** CARTESIAN PRODUCT ***)

(* Compute the possibly infinite product of cardinals. 
 * If one of them is empty, the result is empty. *)
let rec prod_cardinals acu = function
  | [] -> acu
  | exen :: exens ->
      begin match (exen.cardinal, acu) with
      | None, _ -> prod_cardinals None exens
      | (Some z,_) when z = bigzero -> Some bigzero
      | Some _, None -> prod_cardinals None exens
      | Some n, Some k -> prod_cardinals (Some (n ** k)) exens
      end

(* Find all vectors that reach the given max depth. 
 * Input: the expected (max) depth. 
 *        the vector of maximal indexes reachable by each coordinate.
 *          (these maximal indexes are guaranteed to be <= max depth). *)

(* Algorithm: brut force enumeration of all tuples.
 * An optimization, though: we know if the max depth has been reached in the current temporary vector,
 * and we know at which position is the 'last chance' of reaching the max depth. *)

(* For efficiency, rev_max is the reversed list of max_indexes. 
 * flag indicates if max depth has been reached in the current temporary vector. 
 * acu is the list of all vectors. 
 * pos is the current position in the reversed max_indexes list. *)
let rec find_vectors_aux last_chance depth flag acu temp_vect pos rev_max = 

  match rev_max with
  (* This vector is finished. Add it to the accumulator. *)
  | [] ->
      assert flag ; (* The maximal depth must have been reached. *)
      temp_vect :: acu

  | current_vup :: others ->

      let (vlow, vup) =
	(* Particular case: if this is the last chance and flag is false. *)
	if (not flag) && pos = last_chance then
	  begin
	    assert (current_vup = depth) ;
	    (depth, depth)
	  end

	else (0, current_vup)
      in

      (* Iterate over all these values. *)
      let racu = ref acu in
      
      for current_index = vlow to vup do
	racu := find_vectors_aux last_chance depth (flag || current_index = depth) !racu (current_index :: temp_vect) (pos+1) others ;
      done ;

      (* Finished. *)
      !racu

      
let find_vectors depth rev_max_indexes = 
 
  (* Find the position of the last chance. *)
  let (_, last_chance) = myfold rev_max_indexes (0, (-1)) 
      begin fun (current_pos, last) v -> if v = depth then (current_pos+1, current_pos) else (current_pos+1, last) end
  in
  assert (last_chance >= 0) ; (* The maximal depth must be reachable. We never try to build a part that cannot be built. *)

  find_vectors_aux last_chance depth false [] [] 0 rev_max_indexes

(* Maps a vector to a rev_list of parts. *)
let vector_to_part_list exens vector = 
  (try myrevmap2 exens vector get_part with _ -> assert false)

(* Creates a new part with depth array_index corresponding to the cartesian product of the given enumerations. *)
let prod_parts array_index exens =
  (* This part is the union of cartesian products of PARTS, at least one of them being at the given depth. *)

  (* Def: a 'vector' is a vector of indexes. Each index corresponds to an enumeration. 
   * The length of the vector = the length of the list 'exens'. *)

  assert (exens <> []) ;

  (* Get the rev_vectors of maximal part indexes, but never further than array_index. *)
  let max_revindexes = myrevmap exens
      begin fun ex ->
	match ex.n_parts with
	| None -> array_index (* Infinite *)
	| Some n -> min (n-1) array_index
      end
  in

  (* List all vectors that satisfy the current depth (i.e. at least one index is the expected array_index). *)
  let all_vectors = find_vectors array_index max_revindexes in

  assert (all_vectors <> []) ;
  
  (* Map these vectors to part lists. *)
  let all_rev_parts = List.rev_map (vector_to_part_list exens) all_vectors in

  (* Map each part list to a product part. 
   * product_parts reverses the tuples. *)
  let all_prod_parts = List.rev_map product_parts all_rev_parts in

  (* Get the union *)
  union_parts all_prod_parts

(* Cartesian product. *)
let product exens =
  
  let cardinal = prod_cardinals (Some bigone) exens in
  let parts = ExtArray.create 1 uninitialized_part in

  { cardinal ;
    n_parts = max_parts exens ;
    parts ;
    new_part = (fun array_index -> prod_parts array_index exens) ;
    title = lazy ("product (" ^ (sep (fun e -> Lazy.force e.title) ", " exens) ^ ")") }

OCaml

Innovation. Community. Security.