35 open Hints_declaration
73 type register_set = { rs_empty : __; rs_singleton : (I8051.register -> __);
74 rs_fold : (__ -> (I8051.register -> __ -> __) -> __ ->
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 -> __) }
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 **)
89 let 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
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
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 **)
104 let 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
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
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 **)
119 let 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
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
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 **)
134 let 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
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
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 **)
149 let 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
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
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 **)
164 let 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
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
175 (** val rs_empty : register_set -> __ **)
176 let rec rs_empty xxx =
179 (** val rs_singleton : register_set -> I8051.register -> __ **)
180 let rec rs_singleton xxx =
184 register_set -> (I8051.register -> 'a1 -> 'a1) -> __ -> 'a1 -> 'a1 **)
185 let 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
190 Obj.magic yyy) __ x_18487 x_18488 x_18489
192 (** val rs_insert : register_set -> I8051.register -> __ -> __ **)
193 let rec rs_insert xxx =
196 (** val rs_exists : register_set -> I8051.register -> __ -> Bool.bool **)
197 let rec rs_exists xxx =
200 (** val rs_union : register_set -> __ -> __ -> __ **)
201 let rec rs_union xxx =
204 (** val rs_subset : register_set -> __ -> __ -> Bool.bool **)
205 let rec rs_subset xxx =
208 (** val rs_to_list : register_set -> __ -> I8051.register List.list **)
209 let rec rs_to_list xxx =
212 (** val rs_from_list : register_set -> I8051.register List.list -> __ **)
213 let rec rs_from_list xxx =
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 **)
222 let register_set_inv_rect_Type4 hterm h1 =
223 let hcut = register_set_rect_Type4 h1 hterm in hcut __
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 **)
231 let register_set_inv_rect_Type3 hterm h1 =
232 let hcut = register_set_rect_Type3 h1 hterm in hcut __
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 **)
240 let register_set_inv_rect_Type2 hterm h1 =
241 let hcut = register_set_rect_Type2 h1 hterm in hcut __
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 **)
249 let register_set_inv_rect_Type1 hterm h1 =
250 let hcut = register_set_rect_Type1 h1 hterm in hcut __
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 **)
258 let register_set_inv_rect_Type0 hterm h1 =
259 let hcut = register_set_rect_Type0 h1 hterm in hcut __
261 (** val register_set_jmdiscr : register_set -> register_set -> __ **)
262 let 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
268 Obj.magic (fun _ dH -> dH __ __ __ __ __ __ __ __ __ __)) y
270 (** val rs_list_set_empty : I8051.register List.list **)
271 let rs_list_set_empty =
274 (** val rs_list_set_singleton :
275 I8051.register -> I8051.register List.list **)
276 let rs_list_set_singleton r =
277 List.Cons (r, List.Nil)
279 (** val rs_list_set_fold :
280 (I8051.register -> 'a1 -> 'a1) -> I8051.register List.list -> 'a1 -> 'a1 **)
281 let rs_list_set_fold f l a =
284 (** val rs_list_set_insert :
285 I8051.register -> I8051.register List.list -> I8051.register List.list **)
286 let rs_list_set_insert r s =
287 match Util.member I8051.eq_Register r s with
288 | Bool.True -> List.Cons (r, s)
291 (** val rs_list_set_exists :
292 I8051.register -> I8051.register List.list -> Bool.bool **)
293 let rs_list_set_exists r s =
294 Util.member I8051.eq_Register r s
296 (** val rs_list_set_union :
297 I8051.register List.list -> I8051.register List.list -> I8051.register
299 let rs_list_set_union r s =
300 Util.nub_by I8051.eq_Register (List.append r s)
302 (** val rs_list_set_subset :
303 I8051.register List.list -> I8051.register List.list -> Bool.bool **)
304 let rs_list_set_subset r s =
305 Util.forall (fun x -> Util.member I8051.eq_Register x s) r
307 (** val rs_list_set_from_list :
308 I8051.register List.list -> I8051.register List.list **)
309 let rs_list_set_from_list r =
310 Util.nub_by I8051.eq_Register r
312 (** val register_list_set : register_set **)
313 let 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) }