source: driver/extracted/registerSet.ml @ 3106

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

New extraction

File size: 11.6 KB
Line 
1open Preamble
2
3open Exp
4
5open Setoids
6
7open Monad
8
9open Option
10
11open Extranat
12
13open Vector
14
15open Div_and_mod
16
17open Russell
18
19open Types
20
21open List
22
23open Util
24
25open FoldStuff
26
27open BitVector
28
29open Arithmetic
30
31open Jmeq
32
33open Bool
34
35open Hints_declaration
36
37open Core_notation
38
39open Pts
40
41open Logic
42
43open Relations
44
45open Nat
46
47open I8051
48
49open Order
50
51open Proper
52
53open PositiveMap
54
55open Deqsets
56
57open ErrorMessages
58
59open PreIdentifiers
60
61open Errors
62
63open Extralib
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_18453 =
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_18453
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_18455 =
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_18455
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_18457 =
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_18457
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_18459 =
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_18459
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_18461 =
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_18461
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_18463 =
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_18463
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_18487 x_18488 x_18489 =
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_18487 x_18488 x_18489
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.