source: extracted/set_adt.ml @ 2717

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

Extracted code for the whole compiler.
The space cost model is not there yet.

I have fixed by hand the few extraction problems
(i.e. composed coercions not extracted and type
definitions with wrong syntax).

I have also changed all axioms to be implemented
so that they do not fail at initialization time.

File size: 6.5 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 List
20
21open Div_and_mod
22
23open Jmeq
24
25open Russell
26
27open Util
28
29type 'x set (* AXIOM TO BE REALIZED *)
30
31type 'elt_type set0 =
32| Empty
33| Node of Nat.nat * 'elt_type set0 * 'elt_type * 'elt_type set0
34
35(** val set_rect_Type4 :
36    'a2 -> (Nat.nat -> 'a1 set0 -> 'a1 -> 'a1 set0 -> 'a2 -> 'a2 -> 'a2) ->
37    'a1 set0 -> 'a2 **)
38let rec set_rect_Type4 h_empty h_node = function
39| Empty -> h_empty
40| Node (x_18359, x_18358, x_18357, x_18356) ->
41  h_node x_18359 x_18358 x_18357 x_18356
42    (set_rect_Type4 h_empty h_node x_18358)
43    (set_rect_Type4 h_empty h_node x_18356)
44
45(** val set_rect_Type3 :
46    'a2 -> (Nat.nat -> 'a1 set0 -> 'a1 -> 'a1 set0 -> 'a2 -> 'a2 -> 'a2) ->
47    'a1 set0 -> 'a2 **)
48let rec set_rect_Type3 h_empty h_node = function
49| Empty -> h_empty
50| Node (x_18373, x_18372, x_18371, x_18370) ->
51  h_node x_18373 x_18372 x_18371 x_18370
52    (set_rect_Type3 h_empty h_node x_18372)
53    (set_rect_Type3 h_empty h_node x_18370)
54
55(** val set_rect_Type2 :
56    'a2 -> (Nat.nat -> 'a1 set0 -> 'a1 -> 'a1 set0 -> 'a2 -> 'a2 -> 'a2) ->
57    'a1 set0 -> 'a2 **)
58let rec set_rect_Type2 h_empty h_node = function
59| Empty -> h_empty
60| Node (x_18380, x_18379, x_18378, x_18377) ->
61  h_node x_18380 x_18379 x_18378 x_18377
62    (set_rect_Type2 h_empty h_node x_18379)
63    (set_rect_Type2 h_empty h_node x_18377)
64
65(** val set_rect_Type1 :
66    'a2 -> (Nat.nat -> 'a1 set0 -> 'a1 -> 'a1 set0 -> 'a2 -> 'a2 -> 'a2) ->
67    'a1 set0 -> 'a2 **)
68let rec set_rect_Type1 h_empty h_node = function
69| Empty -> h_empty
70| Node (x_18387, x_18386, x_18385, x_18384) ->
71  h_node x_18387 x_18386 x_18385 x_18384
72    (set_rect_Type1 h_empty h_node x_18386)
73    (set_rect_Type1 h_empty h_node x_18384)
74
75(** val set_rect_Type0 :
76    'a2 -> (Nat.nat -> 'a1 set0 -> 'a1 -> 'a1 set0 -> 'a2 -> 'a2 -> 'a2) ->
77    'a1 set0 -> 'a2 **)
78let rec set_rect_Type0 h_empty h_node = function
79| Empty -> h_empty
80| Node (x_18394, x_18393, x_18392, x_18391) ->
81  h_node x_18394 x_18393 x_18392 x_18391
82    (set_rect_Type0 h_empty h_node x_18393)
83    (set_rect_Type0 h_empty h_node x_18391)
84
85(** val set_inv_rect_Type4 :
86    'a1 set0 -> (__ -> 'a2) -> (Nat.nat -> 'a1 set0 -> 'a1 -> 'a1 set0 -> (__
87    -> 'a2) -> (__ -> 'a2) -> __ -> 'a2) -> 'a2 **)
88let set_inv_rect_Type4 hterm h1 h2 =
89  let hcut = set_rect_Type4 h1 h2 hterm in hcut __
90
91(** val set_inv_rect_Type3 :
92    'a1 set0 -> (__ -> 'a2) -> (Nat.nat -> 'a1 set0 -> 'a1 -> 'a1 set0 -> (__
93    -> 'a2) -> (__ -> 'a2) -> __ -> 'a2) -> 'a2 **)
94let set_inv_rect_Type3 hterm h1 h2 =
95  let hcut = set_rect_Type3 h1 h2 hterm in hcut __
96
97(** val set_inv_rect_Type2 :
98    'a1 set0 -> (__ -> 'a2) -> (Nat.nat -> 'a1 set0 -> 'a1 -> 'a1 set0 -> (__
99    -> 'a2) -> (__ -> 'a2) -> __ -> 'a2) -> 'a2 **)
100let set_inv_rect_Type2 hterm h1 h2 =
101  let hcut = set_rect_Type2 h1 h2 hterm in hcut __
102
103(** val set_inv_rect_Type1 :
104    'a1 set0 -> (__ -> 'a2) -> (Nat.nat -> 'a1 set0 -> 'a1 -> 'a1 set0 -> (__
105    -> 'a2) -> (__ -> 'a2) -> __ -> 'a2) -> 'a2 **)
106let set_inv_rect_Type1 hterm h1 h2 =
107  let hcut = set_rect_Type1 h1 h2 hterm in hcut __
108
109(** val set_inv_rect_Type0 :
110    'a1 set0 -> (__ -> 'a2) -> (Nat.nat -> 'a1 set0 -> 'a1 -> 'a1 set0 -> (__
111    -> 'a2) -> (__ -> 'a2) -> __ -> 'a2) -> 'a2 **)
112let set_inv_rect_Type0 hterm h1 h2 =
113  let hcut = set_rect_Type0 h1 h2 hterm in hcut __
114
115(** val set_discr : 'a1 set0 -> 'a1 set0 -> __ **)
116let set_discr x y =
117  Logic.eq_rect_Type2 x
118    (match x with
119     | Empty -> Obj.magic (fun _ dH -> dH)
120     | Node (a0, a10, a2, a3) -> Obj.magic (fun _ dH -> dH __ __ __ __)) y
121
122(** val set_jmdiscr : 'a1 set0 -> 'a1 set0 -> __ **)
123let set_jmdiscr x y =
124  Logic.eq_rect_Type2 x
125    (match x with
126     | Empty -> Obj.magic (fun _ dH -> dH)
127     | Node (a0, a10, a2, a3) -> Obj.magic (fun _ dH -> dH __ __ __ __)) y
128
129(** val set_empty : 'a1 set0 **)
130let set_empty =
131  failwith "AXIOM TO BE REALIZED"
132
133(** val set_size : 'a1 set0 -> Nat.nat **)
134let set_size _ =
135  failwith "AXIOM TO BE REALIZED"
136
137(** val set_to_list : 'a1 set0 -> 'a1 List.list **)
138let set_to_list _ =
139  failwith "AXIOM TO BE REALIZED"
140
141(** val set_insert : 'a1 -> 'a1 set0 -> 'a1 set0 **)
142let set_insert _ =
143  failwith "AXIOM TO BE REALIZED"
144
145(** val set_remove : 'a1 -> 'a1 set0 -> 'a1 set0 **)
146let set_remove _ =
147  failwith "AXIOM TO BE REALIZED"
148
149(** val set_member :
150    ('a1 -> 'a1 -> Bool.bool) -> 'a1 -> 'a1 set0 -> Bool.bool **)
151let set_member _ =
152  failwith "AXIOM TO BE REALIZED"
153
154(** val set_forall : ('a1 -> Bool.bool) -> 'a1 set0 -> Bool.bool **)
155let set_forall _ =
156  failwith "AXIOM TO BE REALIZED"
157
158(** val set_exists : ('a1 -> Bool.bool) -> 'a1 set0 -> Bool.bool **)
159let set_exists _ =
160  failwith "AXIOM TO BE REALIZED"
161
162(** val set_filter : ('a1 -> Bool.bool) -> 'a1 set0 -> 'a1 set0 **)
163let set_filter _ =
164  failwith "AXIOM TO BE REALIZED"
165
166(** val set_map : ('a1 -> 'a2) -> 'a1 set0 -> 'a2 set0 **)
167let set_map _ =
168  failwith "AXIOM TO BE REALIZED"
169
170(** val set_fold : ('a1 -> 'a2 -> 'a2) -> 'a1 set0 -> 'a2 -> 'a2 **)
171let set_fold _ =
172  failwith "AXIOM TO BE REALIZED"
173
174(** val set_equal :
175    ('a1 -> 'a1 -> Bool.bool) -> 'a1 set0 -> 'a1 set0 -> Bool.bool **)
176let set_equal _ =
177  failwith "AXIOM TO BE REALIZED"
178
179(** val set_diff : 'a1 set0 -> 'a1 set0 -> 'a1 set0 **)
180let set_diff _ =
181  failwith "AXIOM TO BE REALIZED"
182
183(** val set_is_empty : 'a1 set0 -> Bool.bool **)
184let set_is_empty set1 =
185  Util.eq_nat (set_size set1) Nat.O
186
187(** val set_singleton : 'a1 -> 'a1 set0 **)
188let set_singleton elt =
189  set_insert elt set_empty
190
191(** val set_from_list : 'a1 List.list -> 'a1 set0 **)
192let set_from_list the_list =
193  List.foldr set_insert set_empty the_list
194
195(** val set_split :
196    ('a1 -> Bool.bool) -> 'a1 set0 -> ('a1 set0, 'a1 set0) Types.prod **)
197let set_split pred0 the_set =
198  let left = set_filter pred0 the_set in
199  let npred = fun x -> Bool.notb (pred0 x) in
200  let right = set_filter npred the_set in
201  { Types.fst = left; Types.snd = right }
202
203(** val set_subset :
204    ('a1 -> 'a1 -> Bool.bool) -> 'a1 set0 -> 'a1 set0 -> Bool.bool **)
205let set_subset eq left right =
206  set_forall (fun elt -> set_member eq elt right) left
207
208(** val set_subseteq :
209    ('a1 -> 'a1 -> Bool.bool) -> 'a1 set0 -> 'a1 set0 -> Bool.bool **)
210let set_subseteq eq left right =
211  Bool.andb (set_equal eq left right) (set_subset eq left right)
212
213(** val set_union : 'a1 set0 -> 'a1 set0 -> 'a1 set0 **)
214let set_union left right =
215  set_fold set_insert left right
216
217(** val set_intersection :
218    ('a1 -> 'a1 -> Bool.bool) -> 'a1 set0 -> 'a1 set0 -> 'a1 set0 **)
219let set_intersection eq left right =
220  set_filter (fun elt -> set_member eq elt right) left
221
Note: See TracBrowser for help on using the repository browser.