source: driver/extracted/positiveMap.ml @ 3106

Last change on this file since 3106 was 3043, checked in by sacerdot, 7 years ago

New major extraction that should have solved all remaining issues.
As tests/PROBLEMI shows, we still have some bugs with:

a) initialization of global data (regression)
b) function pointers call

File size: 12.7 KB
Line 
1open Preamble
2
3open Hints_declaration
4
5open Core_notation
6
7open Pts
8
9open Logic
10
11open Types
12
13open Bool
14
15open Relations
16
17open Nat
18
19open Positive
20
21open Div_and_mod
22
23open Jmeq
24
25open Russell
26
27open List
28
29open Util
30
31open Setoids
32
33open Monad
34
35open Option
36
37type 'a positive_map =
38| Pm_leaf
39| Pm_node of 'a Types.option * 'a positive_map * 'a positive_map
40
41(** val positive_map_rect_Type4 :
42    'a2 -> ('a1 Types.option -> 'a1 positive_map -> 'a1 positive_map -> 'a2
43    -> 'a2 -> 'a2) -> 'a1 positive_map -> 'a2 **)
44let rec positive_map_rect_Type4 h_pm_leaf h_pm_node = function
45| Pm_leaf -> h_pm_leaf
46| Pm_node (x_3300, x_3299, x_3298) ->
47  h_pm_node x_3300 x_3299 x_3298
48    (positive_map_rect_Type4 h_pm_leaf h_pm_node x_3299)
49    (positive_map_rect_Type4 h_pm_leaf h_pm_node x_3298)
50
51(** val positive_map_rect_Type3 :
52    'a2 -> ('a1 Types.option -> 'a1 positive_map -> 'a1 positive_map -> 'a2
53    -> 'a2 -> 'a2) -> 'a1 positive_map -> 'a2 **)
54let rec positive_map_rect_Type3 h_pm_leaf h_pm_node = function
55| Pm_leaf -> h_pm_leaf
56| Pm_node (x_3312, x_3311, x_3310) ->
57  h_pm_node x_3312 x_3311 x_3310
58    (positive_map_rect_Type3 h_pm_leaf h_pm_node x_3311)
59    (positive_map_rect_Type3 h_pm_leaf h_pm_node x_3310)
60
61(** val positive_map_rect_Type2 :
62    'a2 -> ('a1 Types.option -> 'a1 positive_map -> 'a1 positive_map -> 'a2
63    -> 'a2 -> 'a2) -> 'a1 positive_map -> 'a2 **)
64let rec positive_map_rect_Type2 h_pm_leaf h_pm_node = function
65| Pm_leaf -> h_pm_leaf
66| Pm_node (x_3318, x_3317, x_3316) ->
67  h_pm_node x_3318 x_3317 x_3316
68    (positive_map_rect_Type2 h_pm_leaf h_pm_node x_3317)
69    (positive_map_rect_Type2 h_pm_leaf h_pm_node x_3316)
70
71(** val positive_map_rect_Type1 :
72    'a2 -> ('a1 Types.option -> 'a1 positive_map -> 'a1 positive_map -> 'a2
73    -> 'a2 -> 'a2) -> 'a1 positive_map -> 'a2 **)
74let rec positive_map_rect_Type1 h_pm_leaf h_pm_node = function
75| Pm_leaf -> h_pm_leaf
76| Pm_node (x_3324, x_3323, x_3322) ->
77  h_pm_node x_3324 x_3323 x_3322
78    (positive_map_rect_Type1 h_pm_leaf h_pm_node x_3323)
79    (positive_map_rect_Type1 h_pm_leaf h_pm_node x_3322)
80
81(** val positive_map_rect_Type0 :
82    'a2 -> ('a1 Types.option -> 'a1 positive_map -> 'a1 positive_map -> 'a2
83    -> 'a2 -> 'a2) -> 'a1 positive_map -> 'a2 **)
84let rec positive_map_rect_Type0 h_pm_leaf h_pm_node = function
85| Pm_leaf -> h_pm_leaf
86| Pm_node (x_3330, x_3329, x_3328) ->
87  h_pm_node x_3330 x_3329 x_3328
88    (positive_map_rect_Type0 h_pm_leaf h_pm_node x_3329)
89    (positive_map_rect_Type0 h_pm_leaf h_pm_node x_3328)
90
91(** val positive_map_inv_rect_Type4 :
92    'a1 positive_map -> (__ -> 'a2) -> ('a1 Types.option -> 'a1 positive_map
93    -> 'a1 positive_map -> (__ -> 'a2) -> (__ -> 'a2) -> __ -> 'a2) -> 'a2 **)
94let positive_map_inv_rect_Type4 hterm h1 h2 =
95  let hcut = positive_map_rect_Type4 h1 h2 hterm in hcut __
96
97(** val positive_map_inv_rect_Type3 :
98    'a1 positive_map -> (__ -> 'a2) -> ('a1 Types.option -> 'a1 positive_map
99    -> 'a1 positive_map -> (__ -> 'a2) -> (__ -> 'a2) -> __ -> 'a2) -> 'a2 **)
100let positive_map_inv_rect_Type3 hterm h1 h2 =
101  let hcut = positive_map_rect_Type3 h1 h2 hterm in hcut __
102
103(** val positive_map_inv_rect_Type2 :
104    'a1 positive_map -> (__ -> 'a2) -> ('a1 Types.option -> 'a1 positive_map
105    -> 'a1 positive_map -> (__ -> 'a2) -> (__ -> 'a2) -> __ -> 'a2) -> 'a2 **)
106let positive_map_inv_rect_Type2 hterm h1 h2 =
107  let hcut = positive_map_rect_Type2 h1 h2 hterm in hcut __
108
109(** val positive_map_inv_rect_Type1 :
110    'a1 positive_map -> (__ -> 'a2) -> ('a1 Types.option -> 'a1 positive_map
111    -> 'a1 positive_map -> (__ -> 'a2) -> (__ -> 'a2) -> __ -> 'a2) -> 'a2 **)
112let positive_map_inv_rect_Type1 hterm h1 h2 =
113  let hcut = positive_map_rect_Type1 h1 h2 hterm in hcut __
114
115(** val positive_map_inv_rect_Type0 :
116    'a1 positive_map -> (__ -> 'a2) -> ('a1 Types.option -> 'a1 positive_map
117    -> 'a1 positive_map -> (__ -> 'a2) -> (__ -> 'a2) -> __ -> 'a2) -> 'a2 **)
118let positive_map_inv_rect_Type0 hterm h1 h2 =
119  let hcut = positive_map_rect_Type0 h1 h2 hterm in hcut __
120
121(** val positive_map_discr : 'a1 positive_map -> 'a1 positive_map -> __ **)
122let positive_map_discr x y =
123  Logic.eq_rect_Type2 x
124    (match x with
125     | Pm_leaf -> Obj.magic (fun _ dH -> dH)
126     | Pm_node (a0, a10, a2) -> Obj.magic (fun _ dH -> dH __ __ __)) y
127
128(** val positive_map_jmdiscr : 'a1 positive_map -> 'a1 positive_map -> __ **)
129let positive_map_jmdiscr x y =
130  Logic.eq_rect_Type2 x
131    (match x with
132     | Pm_leaf -> Obj.magic (fun _ dH -> dH)
133     | Pm_node (a0, a10, a2) -> Obj.magic (fun _ dH -> dH __ __ __)) y
134
135(** val lookup_opt : Positive.pos -> 'a1 positive_map -> 'a1 Types.option **)
136let rec lookup_opt b = function
137| Pm_leaf -> Types.None
138| Pm_node (a, l, r) ->
139  (match b with
140   | Positive.One -> a
141   | Positive.P1 tl -> lookup_opt tl r
142   | Positive.P0 tl -> lookup_opt tl l)
143
144(** val lookup : Positive.pos -> 'a1 positive_map -> 'a1 -> 'a1 **)
145let lookup b t x =
146  match lookup_opt b t with
147  | Types.None -> x
148  | Types.Some r -> r
149
150(** val pm_set :
151    Positive.pos -> 'a1 Types.option -> 'a1 positive_map -> 'a1 positive_map **)
152let rec pm_set b a t =
153  match b with
154  | Positive.One ->
155    (match t with
156     | Pm_leaf -> Pm_node (a, Pm_leaf, Pm_leaf)
157     | Pm_node (x, l, r) -> Pm_node (a, l, r))
158  | Positive.P1 tl ->
159    (match t with
160     | Pm_leaf -> Pm_node (Types.None, Pm_leaf, (pm_set tl a Pm_leaf))
161     | Pm_node (x, l, r) -> Pm_node (x, l, (pm_set tl a r)))
162  | Positive.P0 tl ->
163    (match t with
164     | Pm_leaf -> Pm_node (Types.None, (pm_set tl a Pm_leaf), Pm_leaf)
165     | Pm_node (x, l, r) -> Pm_node (x, (pm_set tl a l), r))
166
167(** val insert :
168    Positive.pos -> 'a1 -> 'a1 positive_map -> 'a1 positive_map **)
169let insert p a =
170  pm_set p (Types.Some a)
171
172(** val update :
173    Positive.pos -> 'a1 -> 'a1 positive_map -> 'a1 positive_map Types.option **)
174let rec update b a t =
175  match b with
176  | Positive.One ->
177    (match t with
178     | Pm_leaf -> Types.None
179     | Pm_node (x, l, r) ->
180       Types.option_map (fun x0 -> Pm_node ((Types.Some a), l, r)) x)
181  | Positive.P1 tl ->
182    (match t with
183     | Pm_leaf -> Types.None
184     | Pm_node (x, l, r) ->
185       Types.option_map (fun r0 -> Pm_node (x, l, r0)) (update tl a r))
186  | Positive.P0 tl ->
187    (match t with
188     | Pm_leaf -> Types.None
189     | Pm_node (x, l, r) ->
190       Types.option_map (fun l0 -> Pm_node (x, l0, r)) (update tl a l))
191
192(** val fold :
193    (Positive.pos -> 'a1 -> 'a2 -> 'a2) -> 'a1 positive_map -> 'a2 -> 'a2 **)
194let rec fold f t b =
195  match t with
196  | Pm_leaf -> b
197  | Pm_node (a, l, r) ->
198    let b0 =
199      match a with
200      | Types.None -> b
201      | Types.Some a0 -> f Positive.One a0 b
202    in
203    let b1 = fold (fun x -> f (Positive.P0 x)) l b0 in
204    fold (fun x -> f (Positive.P1 x)) r b1
205
206(** val domain_of_pm : 'a1 positive_map -> Types.unit0 positive_map **)
207let domain_of_pm t =
208  fold (fun p a b -> insert p Types.It b) t Pm_leaf
209
210(** val is_none : 'a1 Types.option -> Bool.bool **)
211let is_none = function
212| Types.None -> Bool.True
213| Types.Some x -> Bool.False
214
215(** val is_pm_leaf : 'a1 positive_map -> Bool.bool **)
216let is_pm_leaf = function
217| Pm_leaf -> Bool.True
218| Pm_node (x, x0, x1) -> Bool.False
219
220(** val map_opt :
221    ('a1 -> 'a2 Types.option) -> 'a1 positive_map -> 'a2 positive_map **)
222let rec map_opt f = function
223| Pm_leaf -> Pm_leaf
224| Pm_node (a, l, r) ->
225  let a' =
226    Monad.m_bind0 (Monad.max_def Option.option) (Obj.magic a) (fun x ->
227      Obj.magic f x)
228  in
229  let l' = map_opt f l in
230  let r' = map_opt f r in
231  (match Bool.andb (Bool.andb (is_none (Obj.magic a')) (is_pm_leaf l'))
232           (is_pm_leaf r') with
233   | Bool.True -> Pm_leaf
234   | Bool.False -> Pm_node ((Obj.magic a'), l', r'))
235
236(** val map : ('a1 -> 'a2) -> 'a1 positive_map -> 'a2 positive_map **)
237let map f =
238  map_opt (fun x -> Types.Some (f x))
239
240(** val merge :
241    ('a1 Types.option -> 'a2 Types.option -> 'a3 Types.option) -> 'a1
242    positive_map -> 'a2 positive_map -> 'a3 positive_map **)
243let rec merge choice a b =
244  match a with
245  | Pm_leaf -> map_opt (fun x -> choice Types.None (Types.Some x)) b
246  | Pm_node (o, l, r) ->
247    (match b with
248     | Pm_leaf -> map_opt (fun x -> choice (Types.Some x) Types.None) a
249     | Pm_node (o', l', r') ->
250       let o'' = choice o o' in
251       let l'' = merge choice l l' in
252       let r'' = merge choice r r' in
253       (match Bool.andb (Bool.andb (is_none o'') (is_pm_leaf l''))
254                (is_pm_leaf r'') with
255        | Bool.True -> Pm_leaf
256        | Bool.False -> Pm_node (o'', l'', r'')))
257
258(** val domain_size : 'a1 positive_map -> Nat.nat **)
259let rec domain_size = function
260| Pm_leaf -> Nat.O
261| Pm_node (a, l, r) ->
262  Nat.plus
263    (Nat.plus
264      (match a with
265       | Types.None -> Nat.O
266       | Types.Some x -> Nat.S Nat.O) (domain_size l)) (domain_size r)
267
268(** val pm_all_aux :
269    'a1 positive_map -> 'a1 positive_map -> (Positive.pos -> Positive.pos) ->
270    (Positive.pos -> 'a1 -> __ -> Bool.bool) -> Bool.bool **)
271let rec pm_all_aux m t pre x =
272  (match t with
273   | Pm_leaf -> (fun _ x0 -> Bool.True)
274   | Pm_node (a, l, r) ->
275     (fun _ f ->
276       Bool.andb
277         (Bool.andb (pm_all_aux m l (fun x0 -> pre (Positive.P0 x0)) f)
278           ((match a with
279             | Types.None -> (fun _ -> Bool.True)
280             | Types.Some a' -> (fun _ -> f (pre Positive.One) a' __)) __))
281         (pm_all_aux m r (fun x0 -> pre (Positive.P1 x0)) f))) __ x
282
283(** val pm_all :
284    'a1 positive_map -> (Positive.pos -> 'a1 -> __ -> Bool.bool) -> Bool.bool **)
285let pm_all m f =
286  pm_all_aux m m (fun x -> x) f
287
288(** val pm_choose :
289    'a1 positive_map -> ((Positive.pos, 'a1) Types.prod, 'a1 positive_map)
290    Types.prod Types.option **)
291let rec pm_choose = function
292| Pm_leaf -> Types.None
293| Pm_node (a, l, r) ->
294  (match pm_choose l with
295   | Types.None ->
296     (match pm_choose r with
297      | Types.None ->
298        (match a with
299         | Types.None -> Types.None
300         | Types.Some a0 ->
301           Types.Some { Types.fst = { Types.fst = Positive.One; Types.snd =
302             a0 }; Types.snd = Pm_leaf })
303      | Types.Some x ->
304        Types.Some { Types.fst = { Types.fst = (Positive.P1
305          x.Types.fst.Types.fst); Types.snd = x.Types.fst.Types.snd };
306          Types.snd = (Pm_node (a, l, x.Types.snd)) })
307   | Types.Some x ->
308     Types.Some { Types.fst = { Types.fst = (Positive.P0
309       x.Types.fst.Types.fst); Types.snd = x.Types.fst.Types.snd };
310       Types.snd = (Pm_node (a, x.Types.snd, r)) })
311
312(** val pm_try_remove :
313    Positive.pos -> 'a1 positive_map -> ('a1, 'a1 positive_map) Types.prod
314    Types.option **)
315let rec pm_try_remove b t =
316  match b with
317  | Positive.One ->
318    (match t with
319     | Pm_leaf -> Types.None
320     | Pm_node (x, l, r) ->
321       Types.option_map (fun x0 -> { Types.fst = x0; Types.snd = (Pm_node
322         (Types.None, l, r)) }) x)
323  | Positive.P1 tl ->
324    (match t with
325     | Pm_leaf -> Types.None
326     | Pm_node (x, l, r) ->
327       Types.option_map (fun xr -> { Types.fst = xr.Types.fst; Types.snd =
328         (Pm_node (x, l, xr.Types.snd)) }) (pm_try_remove tl r))
329  | Positive.P0 tl ->
330    (match t with
331     | Pm_leaf -> Types.None
332     | Pm_node (x, l, r) ->
333       Types.option_map (fun xl -> { Types.fst = xl.Types.fst; Types.snd =
334         (Pm_node (x, xl.Types.snd, r)) }) (pm_try_remove tl l))
335
336(** val pm_fold_inf_aux :
337    'a1 positive_map -> (Positive.pos -> 'a1 -> __ -> 'a2 -> 'a2) -> 'a1
338    positive_map -> (Positive.pos -> Positive.pos) -> 'a2 -> 'a2 **)
339let rec pm_fold_inf_aux t f t' pre b =
340  (match t' with
341   | Pm_leaf -> (fun _ -> b)
342   | Pm_node (a, l, r) ->
343     (fun _ ->
344       let b0 =
345         (match a with
346          | Types.None -> (fun _ -> b)
347          | Types.Some a0 -> (fun _ -> f (pre Positive.One) a0 __ b)) __
348       in
349       let b1 = pm_fold_inf_aux t f l (fun x -> pre (Positive.P0 x)) b0 in
350       pm_fold_inf_aux t f r (fun x -> pre (Positive.P1 x)) b1)) __
351
352(** val pm_fold_inf :
353    'a1 positive_map -> (Positive.pos -> 'a1 -> __ -> 'a2 -> 'a2) -> 'a2 ->
354    'a2 **)
355let pm_fold_inf t f b =
356  pm_fold_inf_aux t f t (fun x -> x) b
357
358(** val pm_find_aux :
359    (Positive.pos -> Positive.pos) -> 'a1 positive_map -> (Positive.pos ->
360    'a1 -> Bool.bool) -> (Positive.pos, 'a1) Types.prod Types.option **)
361let rec pm_find_aux pre t p =
362  match t with
363  | Pm_leaf -> Types.None
364  | Pm_node (a, l, r) ->
365    let x =
366      match a with
367      | Types.None -> Types.None
368      | Types.Some a0 ->
369        (match p (pre Positive.One) a0 with
370         | Bool.True ->
371           Types.Some { Types.fst = (pre Positive.One); Types.snd = a0 }
372         | Bool.False -> Types.None)
373    in
374    (match x with
375     | Types.None ->
376       (match pm_find_aux (fun x0 -> pre (Positive.P0 x0)) l p with
377        | Types.None -> pm_find_aux (fun x0 -> pre (Positive.P1 x0)) r p
378        | Types.Some y -> Types.Some y)
379     | Types.Some x0 -> Types.Some x0)
380
381(** val pm_find :
382    'a1 positive_map -> (Positive.pos -> 'a1 -> Bool.bool) -> (Positive.pos,
383    'a1) Types.prod Types.option **)
384let pm_find x x0 =
385  pm_find_aux (fun x1 -> x1) x x0
386
Note: See TracBrowser for help on using the repository browser.