source: extracted/registerSet.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: 11.6 KB
Line 
1open Preamble
2
3open Exp
4
5open Extranat
6
7open Vector
8
9open Div_and_mod
10
11open Russell
12
13open Types
14
15open List
16
17open Util
18
19open FoldStuff
20
21open BitVector
22
23open Arithmetic
24
25open Jmeq
26
27open Bool
28
29open Hints_declaration
30
31open Core_notation
32
33open Pts
34
35open Logic
36
37open Relations
38
39open Nat
40
41open I8051
42
43open Order
44
45open Proper
46
47open PositiveMap
48
49open Deqsets
50
51open ErrorMessages
52
53open PreIdentifiers
54
55open Errors
56
57open Extralib
58
59open Setoids
60
61open Monad
62
63open Option
64
65open Lists
66
67open Positive
68
69open Identifiers
70
71open Registers
72
73type register_set = { rs_empty : __; rs_singleton : (I8051.register -> __);
74                      rs_fold : (__ -> (I8051.register -> __ -> __) -> __ ->
75                                __ -> __);
76                      rs_insert : (I8051.register -> __ -> __);
77                      rs_exists : (I8051.register -> __ -> Bool.bool);
78                      rs_union : (__ -> __ -> __);
79                      rs_subset : (__ -> __ -> Bool.bool);
80                      rs_to_list : (__ -> I8051.register List.list);
81                      rs_from_list : (I8051.register List.list -> __) }
82
83(** val register_set_rect_Type4 :
84    (__ -> __ -> (I8051.register -> __) -> (__ -> (I8051.register -> __ ->
85    __) -> __ -> __ -> __) -> (I8051.register -> __ -> __) -> (I8051.register
86    -> __ -> Bool.bool) -> (__ -> __ -> __) -> (__ -> __ -> Bool.bool) -> (__
87    -> I8051.register List.list) -> (I8051.register List.list -> __) -> 'a1)
88    -> register_set -> 'a1 **)
89let rec register_set_rect_Type4 h_mk_register_set x_17775 =
90  let { rs_empty = rs_empty0; rs_singleton = rs_singleton0; rs_fold =
91    rs_fold0; rs_insert = rs_insert0; rs_exists = rs_exists0; rs_union =
92    rs_union0; rs_subset = rs_subset0; rs_to_list = rs_to_list0;
93    rs_from_list = rs_from_list0 } = x_17775
94  in
95  h_mk_register_set __ rs_empty0 rs_singleton0 rs_fold0 rs_insert0 rs_exists0
96    rs_union0 rs_subset0 rs_to_list0 rs_from_list0
97
98(** val register_set_rect_Type5 :
99    (__ -> __ -> (I8051.register -> __) -> (__ -> (I8051.register -> __ ->
100    __) -> __ -> __ -> __) -> (I8051.register -> __ -> __) -> (I8051.register
101    -> __ -> Bool.bool) -> (__ -> __ -> __) -> (__ -> __ -> Bool.bool) -> (__
102    -> I8051.register List.list) -> (I8051.register List.list -> __) -> 'a1)
103    -> register_set -> 'a1 **)
104let rec register_set_rect_Type5 h_mk_register_set x_17777 =
105  let { rs_empty = rs_empty0; rs_singleton = rs_singleton0; rs_fold =
106    rs_fold0; rs_insert = rs_insert0; rs_exists = rs_exists0; rs_union =
107    rs_union0; rs_subset = rs_subset0; rs_to_list = rs_to_list0;
108    rs_from_list = rs_from_list0 } = x_17777
109  in
110  h_mk_register_set __ rs_empty0 rs_singleton0 rs_fold0 rs_insert0 rs_exists0
111    rs_union0 rs_subset0 rs_to_list0 rs_from_list0
112
113(** val register_set_rect_Type3 :
114    (__ -> __ -> (I8051.register -> __) -> (__ -> (I8051.register -> __ ->
115    __) -> __ -> __ -> __) -> (I8051.register -> __ -> __) -> (I8051.register
116    -> __ -> Bool.bool) -> (__ -> __ -> __) -> (__ -> __ -> Bool.bool) -> (__
117    -> I8051.register List.list) -> (I8051.register List.list -> __) -> 'a1)
118    -> register_set -> 'a1 **)
119let rec register_set_rect_Type3 h_mk_register_set x_17779 =
120  let { rs_empty = rs_empty0; rs_singleton = rs_singleton0; rs_fold =
121    rs_fold0; rs_insert = rs_insert0; rs_exists = rs_exists0; rs_union =
122    rs_union0; rs_subset = rs_subset0; rs_to_list = rs_to_list0;
123    rs_from_list = rs_from_list0 } = x_17779
124  in
125  h_mk_register_set __ rs_empty0 rs_singleton0 rs_fold0 rs_insert0 rs_exists0
126    rs_union0 rs_subset0 rs_to_list0 rs_from_list0
127
128(** val register_set_rect_Type2 :
129    (__ -> __ -> (I8051.register -> __) -> (__ -> (I8051.register -> __ ->
130    __) -> __ -> __ -> __) -> (I8051.register -> __ -> __) -> (I8051.register
131    -> __ -> Bool.bool) -> (__ -> __ -> __) -> (__ -> __ -> Bool.bool) -> (__
132    -> I8051.register List.list) -> (I8051.register List.list -> __) -> 'a1)
133    -> register_set -> 'a1 **)
134let rec register_set_rect_Type2 h_mk_register_set x_17781 =
135  let { rs_empty = rs_empty0; rs_singleton = rs_singleton0; rs_fold =
136    rs_fold0; rs_insert = rs_insert0; rs_exists = rs_exists0; rs_union =
137    rs_union0; rs_subset = rs_subset0; rs_to_list = rs_to_list0;
138    rs_from_list = rs_from_list0 } = x_17781
139  in
140  h_mk_register_set __ rs_empty0 rs_singleton0 rs_fold0 rs_insert0 rs_exists0
141    rs_union0 rs_subset0 rs_to_list0 rs_from_list0
142
143(** val register_set_rect_Type1 :
144    (__ -> __ -> (I8051.register -> __) -> (__ -> (I8051.register -> __ ->
145    __) -> __ -> __ -> __) -> (I8051.register -> __ -> __) -> (I8051.register
146    -> __ -> Bool.bool) -> (__ -> __ -> __) -> (__ -> __ -> Bool.bool) -> (__
147    -> I8051.register List.list) -> (I8051.register List.list -> __) -> 'a1)
148    -> register_set -> 'a1 **)
149let rec register_set_rect_Type1 h_mk_register_set x_17783 =
150  let { rs_empty = rs_empty0; rs_singleton = rs_singleton0; rs_fold =
151    rs_fold0; rs_insert = rs_insert0; rs_exists = rs_exists0; rs_union =
152    rs_union0; rs_subset = rs_subset0; rs_to_list = rs_to_list0;
153    rs_from_list = rs_from_list0 } = x_17783
154  in
155  h_mk_register_set __ rs_empty0 rs_singleton0 rs_fold0 rs_insert0 rs_exists0
156    rs_union0 rs_subset0 rs_to_list0 rs_from_list0
157
158(** val register_set_rect_Type0 :
159    (__ -> __ -> (I8051.register -> __) -> (__ -> (I8051.register -> __ ->
160    __) -> __ -> __ -> __) -> (I8051.register -> __ -> __) -> (I8051.register
161    -> __ -> Bool.bool) -> (__ -> __ -> __) -> (__ -> __ -> Bool.bool) -> (__
162    -> I8051.register List.list) -> (I8051.register List.list -> __) -> 'a1)
163    -> register_set -> 'a1 **)
164let rec register_set_rect_Type0 h_mk_register_set x_17785 =
165  let { rs_empty = rs_empty0; rs_singleton = rs_singleton0; rs_fold =
166    rs_fold0; rs_insert = rs_insert0; rs_exists = rs_exists0; rs_union =
167    rs_union0; rs_subset = rs_subset0; rs_to_list = rs_to_list0;
168    rs_from_list = rs_from_list0 } = x_17785
169  in
170  h_mk_register_set __ rs_empty0 rs_singleton0 rs_fold0 rs_insert0 rs_exists0
171    rs_union0 rs_subset0 rs_to_list0 rs_from_list0
172
173type rs_set = __
174
175(** val rs_empty : register_set -> __ **)
176let rec rs_empty xxx =
177  xxx.rs_empty
178
179(** val rs_singleton : register_set -> I8051.register -> __ **)
180let rec rs_singleton xxx =
181  xxx.rs_singleton
182
183(** val rs_fold0 :
184    register_set -> (I8051.register -> 'a1 -> 'a1) -> __ -> 'a1 -> 'a1 **)
185let rec rs_fold0 xxx x_17809 x_17810 x_17811 =
186  (let { rs_empty = x0; rs_singleton = x1; rs_fold = yyy; rs_insert = x2;
187     rs_exists = x3; rs_union = x4; rs_subset = x5; rs_to_list = x6;
188     rs_from_list = x7 } = xxx
189   in
190  Obj.magic yyy) __ x_17809 x_17810 x_17811
191
192(** val rs_insert : register_set -> I8051.register -> __ -> __ **)
193let rec rs_insert xxx =
194  xxx.rs_insert
195
196(** val rs_exists : register_set -> I8051.register -> __ -> Bool.bool **)
197let rec rs_exists xxx =
198  xxx.rs_exists
199
200(** val rs_union : register_set -> __ -> __ -> __ **)
201let rec rs_union xxx =
202  xxx.rs_union
203
204(** val rs_subset : register_set -> __ -> __ -> Bool.bool **)
205let rec rs_subset xxx =
206  xxx.rs_subset
207
208(** val rs_to_list : register_set -> __ -> I8051.register List.list **)
209let rec rs_to_list xxx =
210  xxx.rs_to_list
211
212(** val rs_from_list : register_set -> I8051.register List.list -> __ **)
213let rec rs_from_list xxx =
214  xxx.rs_from_list
215
216(** val register_set_inv_rect_Type4 :
217    register_set -> (__ -> __ -> (I8051.register -> __) -> (__ ->
218    (I8051.register -> __ -> __) -> __ -> __ -> __) -> (I8051.register -> __
219    -> __) -> (I8051.register -> __ -> Bool.bool) -> (__ -> __ -> __) -> (__
220    -> __ -> Bool.bool) -> (__ -> I8051.register List.list) ->
221    (I8051.register List.list -> __) -> __ -> 'a1) -> 'a1 **)
222let register_set_inv_rect_Type4 hterm h1 =
223  let hcut = register_set_rect_Type4 h1 hterm in hcut __
224
225(** val register_set_inv_rect_Type3 :
226    register_set -> (__ -> __ -> (I8051.register -> __) -> (__ ->
227    (I8051.register -> __ -> __) -> __ -> __ -> __) -> (I8051.register -> __
228    -> __) -> (I8051.register -> __ -> Bool.bool) -> (__ -> __ -> __) -> (__
229    -> __ -> Bool.bool) -> (__ -> I8051.register List.list) ->
230    (I8051.register List.list -> __) -> __ -> 'a1) -> 'a1 **)
231let register_set_inv_rect_Type3 hterm h1 =
232  let hcut = register_set_rect_Type3 h1 hterm in hcut __
233
234(** val register_set_inv_rect_Type2 :
235    register_set -> (__ -> __ -> (I8051.register -> __) -> (__ ->
236    (I8051.register -> __ -> __) -> __ -> __ -> __) -> (I8051.register -> __
237    -> __) -> (I8051.register -> __ -> Bool.bool) -> (__ -> __ -> __) -> (__
238    -> __ -> Bool.bool) -> (__ -> I8051.register List.list) ->
239    (I8051.register List.list -> __) -> __ -> 'a1) -> 'a1 **)
240let register_set_inv_rect_Type2 hterm h1 =
241  let hcut = register_set_rect_Type2 h1 hterm in hcut __
242
243(** val register_set_inv_rect_Type1 :
244    register_set -> (__ -> __ -> (I8051.register -> __) -> (__ ->
245    (I8051.register -> __ -> __) -> __ -> __ -> __) -> (I8051.register -> __
246    -> __) -> (I8051.register -> __ -> Bool.bool) -> (__ -> __ -> __) -> (__
247    -> __ -> Bool.bool) -> (__ -> I8051.register List.list) ->
248    (I8051.register List.list -> __) -> __ -> 'a1) -> 'a1 **)
249let register_set_inv_rect_Type1 hterm h1 =
250  let hcut = register_set_rect_Type1 h1 hterm in hcut __
251
252(** val register_set_inv_rect_Type0 :
253    register_set -> (__ -> __ -> (I8051.register -> __) -> (__ ->
254    (I8051.register -> __ -> __) -> __ -> __ -> __) -> (I8051.register -> __
255    -> __) -> (I8051.register -> __ -> Bool.bool) -> (__ -> __ -> __) -> (__
256    -> __ -> Bool.bool) -> (__ -> I8051.register List.list) ->
257    (I8051.register List.list -> __) -> __ -> 'a1) -> 'a1 **)
258let register_set_inv_rect_Type0 hterm h1 =
259  let hcut = register_set_rect_Type0 h1 hterm in hcut __
260
261(** val register_set_jmdiscr : register_set -> register_set -> __ **)
262let register_set_jmdiscr x y =
263  Logic.eq_rect_Type2 x
264    (let { rs_empty = a1; rs_singleton = a2; rs_fold = a3; rs_insert = a4;
265       rs_exists = a5; rs_union = a6; rs_subset = a7; rs_to_list = a8;
266       rs_from_list = a9 } = x
267     in
268    Obj.magic (fun _ dH -> dH __ __ __ __ __ __ __ __ __ __)) y
269
270(** val rs_list_set_empty : I8051.register List.list **)
271let rs_list_set_empty =
272  List.Nil
273
274(** val rs_list_set_singleton :
275    I8051.register -> I8051.register List.list **)
276let rs_list_set_singleton r =
277  List.Cons (r, List.Nil)
278
279(** val rs_list_set_fold :
280    (I8051.register -> 'a1 -> 'a1) -> I8051.register List.list -> 'a1 -> 'a1 **)
281let rs_list_set_fold f l a =
282  List.foldr f a l
283
284(** val rs_list_set_insert :
285    I8051.register -> I8051.register List.list -> I8051.register List.list **)
286let rs_list_set_insert r s =
287  match Util.member I8051.eq_Register r s with
288  | Bool.True -> List.Cons (r, s)
289  | Bool.False -> s
290
291(** val rs_list_set_exists :
292    I8051.register -> I8051.register List.list -> Bool.bool **)
293let rs_list_set_exists r s =
294  Util.member I8051.eq_Register r s
295
296(** val rs_list_set_union :
297    I8051.register List.list -> I8051.register List.list -> I8051.register
298    List.list **)
299let rs_list_set_union r s =
300  Util.nub_by I8051.eq_Register (List.append r s)
301
302(** val rs_list_set_subset :
303    I8051.register List.list -> I8051.register List.list -> Bool.bool **)
304let rs_list_set_subset r s =
305  Util.forall (fun x -> Util.member I8051.eq_Register x s) r
306
307(** val rs_list_set_from_list :
308    I8051.register List.list -> I8051.register List.list **)
309let rs_list_set_from_list r =
310  Util.nub_by I8051.eq_Register r
311
312(** val register_list_set : register_set **)
313let register_list_set =
314  { rs_empty = (Obj.magic rs_list_set_empty); rs_singleton =
315    (Obj.magic rs_list_set_singleton); rs_fold =
316    (Obj.magic (fun _ -> rs_list_set_fold)); rs_insert =
317    (Obj.magic rs_list_set_insert); rs_exists =
318    (Obj.magic rs_list_set_exists); rs_union = (Obj.magic rs_list_set_union);
319    rs_subset = (Obj.magic rs_list_set_subset); rs_to_list = (fun x ->
320    Obj.magic x); rs_from_list = (Obj.magic rs_list_set_from_list) }
321
Note: See TracBrowser for help on using the repository browser.