99 open Hints_declaration
121 type registers_move =
122 | From_acc of I8051.register * Types.unit0
123 | To_acc of Types.unit0 * I8051.register
124 | Int_to_reg of I8051.register * BitVector.byte
125 | Int_to_acc of Types.unit0 * BitVector.byte
127 (** val registers_move_rect_Type4 :
128 (I8051.register -> Types.unit0 -> 'a1) -> (Types.unit0 -> I8051.register
129 -> 'a1) -> (I8051.register -> BitVector.byte -> 'a1) -> (Types.unit0 ->
130 BitVector.byte -> 'a1) -> registers_move -> 'a1 **)
131 let rec registers_move_rect_Type4 h_from_acc h_to_acc h_int_to_reg h_int_to_acc = function
132 | From_acc (x_18638, x_18637) -> h_from_acc x_18638 x_18637
133 | To_acc (x_18640, x_18639) -> h_to_acc x_18640 x_18639
134 | Int_to_reg (x_18642, x_18641) -> h_int_to_reg x_18642 x_18641
135 | Int_to_acc (x_18644, x_18643) -> h_int_to_acc x_18644 x_18643
137 (** val registers_move_rect_Type5 :
138 (I8051.register -> Types.unit0 -> 'a1) -> (Types.unit0 -> I8051.register
139 -> 'a1) -> (I8051.register -> BitVector.byte -> 'a1) -> (Types.unit0 ->
140 BitVector.byte -> 'a1) -> registers_move -> 'a1 **)
141 let rec registers_move_rect_Type5 h_from_acc h_to_acc h_int_to_reg h_int_to_acc = function
142 | From_acc (x_18651, x_18650) -> h_from_acc x_18651 x_18650
143 | To_acc (x_18653, x_18652) -> h_to_acc x_18653 x_18652
144 | Int_to_reg (x_18655, x_18654) -> h_int_to_reg x_18655 x_18654
145 | Int_to_acc (x_18657, x_18656) -> h_int_to_acc x_18657 x_18656
147 (** val registers_move_rect_Type3 :
148 (I8051.register -> Types.unit0 -> 'a1) -> (Types.unit0 -> I8051.register
149 -> 'a1) -> (I8051.register -> BitVector.byte -> 'a1) -> (Types.unit0 ->
150 BitVector.byte -> 'a1) -> registers_move -> 'a1 **)
151 let rec registers_move_rect_Type3 h_from_acc h_to_acc h_int_to_reg h_int_to_acc = function
152 | From_acc (x_18664, x_18663) -> h_from_acc x_18664 x_18663
153 | To_acc (x_18666, x_18665) -> h_to_acc x_18666 x_18665
154 | Int_to_reg (x_18668, x_18667) -> h_int_to_reg x_18668 x_18667
155 | Int_to_acc (x_18670, x_18669) -> h_int_to_acc x_18670 x_18669
157 (** val registers_move_rect_Type2 :
158 (I8051.register -> Types.unit0 -> 'a1) -> (Types.unit0 -> I8051.register
159 -> 'a1) -> (I8051.register -> BitVector.byte -> 'a1) -> (Types.unit0 ->
160 BitVector.byte -> 'a1) -> registers_move -> 'a1 **)
161 let rec registers_move_rect_Type2 h_from_acc h_to_acc h_int_to_reg h_int_to_acc = function
162 | From_acc (x_18677, x_18676) -> h_from_acc x_18677 x_18676
163 | To_acc (x_18679, x_18678) -> h_to_acc x_18679 x_18678
164 | Int_to_reg (x_18681, x_18680) -> h_int_to_reg x_18681 x_18680
165 | Int_to_acc (x_18683, x_18682) -> h_int_to_acc x_18683 x_18682
167 (** val registers_move_rect_Type1 :
168 (I8051.register -> Types.unit0 -> 'a1) -> (Types.unit0 -> I8051.register
169 -> 'a1) -> (I8051.register -> BitVector.byte -> 'a1) -> (Types.unit0 ->
170 BitVector.byte -> 'a1) -> registers_move -> 'a1 **)
171 let rec registers_move_rect_Type1 h_from_acc h_to_acc h_int_to_reg h_int_to_acc = function
172 | From_acc (x_18690, x_18689) -> h_from_acc x_18690 x_18689
173 | To_acc (x_18692, x_18691) -> h_to_acc x_18692 x_18691
174 | Int_to_reg (x_18694, x_18693) -> h_int_to_reg x_18694 x_18693
175 | Int_to_acc (x_18696, x_18695) -> h_int_to_acc x_18696 x_18695
177 (** val registers_move_rect_Type0 :
178 (I8051.register -> Types.unit0 -> 'a1) -> (Types.unit0 -> I8051.register
179 -> 'a1) -> (I8051.register -> BitVector.byte -> 'a1) -> (Types.unit0 ->
180 BitVector.byte -> 'a1) -> registers_move -> 'a1 **)
181 let rec registers_move_rect_Type0 h_from_acc h_to_acc h_int_to_reg h_int_to_acc = function
182 | From_acc (x_18703, x_18702) -> h_from_acc x_18703 x_18702
183 | To_acc (x_18705, x_18704) -> h_to_acc x_18705 x_18704
184 | Int_to_reg (x_18707, x_18706) -> h_int_to_reg x_18707 x_18706
185 | Int_to_acc (x_18709, x_18708) -> h_int_to_acc x_18709 x_18708
187 (** val registers_move_inv_rect_Type4 :
188 registers_move -> (I8051.register -> Types.unit0 -> __ -> 'a1) ->
189 (Types.unit0 -> I8051.register -> __ -> 'a1) -> (I8051.register ->
190 BitVector.byte -> __ -> 'a1) -> (Types.unit0 -> BitVector.byte -> __ ->
192 let registers_move_inv_rect_Type4 hterm h1 h2 h3 h4 =
193 let hcut = registers_move_rect_Type4 h1 h2 h3 h4 hterm in hcut __
195 (** val registers_move_inv_rect_Type3 :
196 registers_move -> (I8051.register -> Types.unit0 -> __ -> 'a1) ->
197 (Types.unit0 -> I8051.register -> __ -> 'a1) -> (I8051.register ->
198 BitVector.byte -> __ -> 'a1) -> (Types.unit0 -> BitVector.byte -> __ ->
200 let registers_move_inv_rect_Type3 hterm h1 h2 h3 h4 =
201 let hcut = registers_move_rect_Type3 h1 h2 h3 h4 hterm in hcut __
203 (** val registers_move_inv_rect_Type2 :
204 registers_move -> (I8051.register -> Types.unit0 -> __ -> 'a1) ->
205 (Types.unit0 -> I8051.register -> __ -> 'a1) -> (I8051.register ->
206 BitVector.byte -> __ -> 'a1) -> (Types.unit0 -> BitVector.byte -> __ ->
208 let registers_move_inv_rect_Type2 hterm h1 h2 h3 h4 =
209 let hcut = registers_move_rect_Type2 h1 h2 h3 h4 hterm in hcut __
211 (** val registers_move_inv_rect_Type1 :
212 registers_move -> (I8051.register -> Types.unit0 -> __ -> 'a1) ->
213 (Types.unit0 -> I8051.register -> __ -> 'a1) -> (I8051.register ->
214 BitVector.byte -> __ -> 'a1) -> (Types.unit0 -> BitVector.byte -> __ ->
216 let registers_move_inv_rect_Type1 hterm h1 h2 h3 h4 =
217 let hcut = registers_move_rect_Type1 h1 h2 h3 h4 hterm in hcut __
219 (** val registers_move_inv_rect_Type0 :
220 registers_move -> (I8051.register -> Types.unit0 -> __ -> 'a1) ->
221 (Types.unit0 -> I8051.register -> __ -> 'a1) -> (I8051.register ->
222 BitVector.byte -> __ -> 'a1) -> (Types.unit0 -> BitVector.byte -> __ ->
224 let registers_move_inv_rect_Type0 hterm h1 h2 h3 h4 =
225 let hcut = registers_move_rect_Type0 h1 h2 h3 h4 hterm in hcut __
227 (** val registers_move_discr : registers_move -> registers_move -> __ **)
228 let registers_move_discr x y =
229 Logic.eq_rect_Type2 x
231 | From_acc (a0, a1) -> Obj.magic (fun _ dH -> dH __ __)
232 | To_acc (a0, a1) -> Obj.magic (fun _ dH -> dH __ __)
233 | Int_to_reg (a0, a1) -> Obj.magic (fun _ dH -> dH __ __)
234 | Int_to_acc (a0, a1) -> Obj.magic (fun _ dH -> dH __ __)) y
236 (** val registers_move_jmdiscr : registers_move -> registers_move -> __ **)
237 let registers_move_jmdiscr x y =
238 Logic.eq_rect_Type2 x
240 | From_acc (a0, a1) -> Obj.magic (fun _ dH -> dH __ __)
241 | To_acc (a0, a1) -> Obj.magic (fun _ dH -> dH __ __)
242 | Int_to_reg (a0, a1) -> Obj.magic (fun _ dH -> dH __ __)
243 | Int_to_acc (a0, a1) -> Obj.magic (fun _ dH -> dH __ __)) y
248 | LOW_ADDRESS of Graphs.label
249 | HIGH_ADDRESS of Graphs.label
251 (** val ltl_lin_seq_rect_Type4 :
252 'a1 -> 'a1 -> (Graphs.label -> 'a1) -> (Graphs.label -> 'a1) ->
253 ltl_lin_seq -> 'a1 **)
254 let rec ltl_lin_seq_rect_Type4 h_SAVE_CARRY h_RESTORE_CARRY h_LOW_ADDRESS h_HIGH_ADDRESS = function
255 | SAVE_CARRY -> h_SAVE_CARRY
256 | RESTORE_CARRY -> h_RESTORE_CARRY
257 | LOW_ADDRESS x_18800 -> h_LOW_ADDRESS x_18800
258 | HIGH_ADDRESS x_18801 -> h_HIGH_ADDRESS x_18801
260 (** val ltl_lin_seq_rect_Type5 :
261 'a1 -> 'a1 -> (Graphs.label -> 'a1) -> (Graphs.label -> 'a1) ->
262 ltl_lin_seq -> 'a1 **)
263 let rec ltl_lin_seq_rect_Type5 h_SAVE_CARRY h_RESTORE_CARRY h_LOW_ADDRESS h_HIGH_ADDRESS = function
264 | SAVE_CARRY -> h_SAVE_CARRY
265 | RESTORE_CARRY -> h_RESTORE_CARRY
266 | LOW_ADDRESS x_18807 -> h_LOW_ADDRESS x_18807
267 | HIGH_ADDRESS x_18808 -> h_HIGH_ADDRESS x_18808
269 (** val ltl_lin_seq_rect_Type3 :
270 'a1 -> 'a1 -> (Graphs.label -> 'a1) -> (Graphs.label -> 'a1) ->
271 ltl_lin_seq -> 'a1 **)
272 let rec ltl_lin_seq_rect_Type3 h_SAVE_CARRY h_RESTORE_CARRY h_LOW_ADDRESS h_HIGH_ADDRESS = function
273 | SAVE_CARRY -> h_SAVE_CARRY
274 | RESTORE_CARRY -> h_RESTORE_CARRY
275 | LOW_ADDRESS x_18814 -> h_LOW_ADDRESS x_18814
276 | HIGH_ADDRESS x_18815 -> h_HIGH_ADDRESS x_18815
278 (** val ltl_lin_seq_rect_Type2 :
279 'a1 -> 'a1 -> (Graphs.label -> 'a1) -> (Graphs.label -> 'a1) ->
280 ltl_lin_seq -> 'a1 **)
281 let rec ltl_lin_seq_rect_Type2 h_SAVE_CARRY h_RESTORE_CARRY h_LOW_ADDRESS h_HIGH_ADDRESS = function
282 | SAVE_CARRY -> h_SAVE_CARRY
283 | RESTORE_CARRY -> h_RESTORE_CARRY
284 | LOW_ADDRESS x_18821 -> h_LOW_ADDRESS x_18821
285 | HIGH_ADDRESS x_18822 -> h_HIGH_ADDRESS x_18822
287 (** val ltl_lin_seq_rect_Type1 :
288 'a1 -> 'a1 -> (Graphs.label -> 'a1) -> (Graphs.label -> 'a1) ->
289 ltl_lin_seq -> 'a1 **)
290 let rec ltl_lin_seq_rect_Type1 h_SAVE_CARRY h_RESTORE_CARRY h_LOW_ADDRESS h_HIGH_ADDRESS = function
291 | SAVE_CARRY -> h_SAVE_CARRY
292 | RESTORE_CARRY -> h_RESTORE_CARRY
293 | LOW_ADDRESS x_18828 -> h_LOW_ADDRESS x_18828
294 | HIGH_ADDRESS x_18829 -> h_HIGH_ADDRESS x_18829
296 (** val ltl_lin_seq_rect_Type0 :
297 'a1 -> 'a1 -> (Graphs.label -> 'a1) -> (Graphs.label -> 'a1) ->
298 ltl_lin_seq -> 'a1 **)
299 let rec ltl_lin_seq_rect_Type0 h_SAVE_CARRY h_RESTORE_CARRY h_LOW_ADDRESS h_HIGH_ADDRESS = function
300 | SAVE_CARRY -> h_SAVE_CARRY
301 | RESTORE_CARRY -> h_RESTORE_CARRY
302 | LOW_ADDRESS x_18835 -> h_LOW_ADDRESS x_18835
303 | HIGH_ADDRESS x_18836 -> h_HIGH_ADDRESS x_18836
305 (** val ltl_lin_seq_inv_rect_Type4 :
306 ltl_lin_seq -> (__ -> 'a1) -> (__ -> 'a1) -> (Graphs.label -> __ -> 'a1)
307 -> (Graphs.label -> __ -> 'a1) -> 'a1 **)
308 let ltl_lin_seq_inv_rect_Type4 hterm h1 h2 h3 h4 =
309 let hcut = ltl_lin_seq_rect_Type4 h1 h2 h3 h4 hterm in hcut __
311 (** val ltl_lin_seq_inv_rect_Type3 :
312 ltl_lin_seq -> (__ -> 'a1) -> (__ -> 'a1) -> (Graphs.label -> __ -> 'a1)
313 -> (Graphs.label -> __ -> 'a1) -> 'a1 **)
314 let ltl_lin_seq_inv_rect_Type3 hterm h1 h2 h3 h4 =
315 let hcut = ltl_lin_seq_rect_Type3 h1 h2 h3 h4 hterm in hcut __
317 (** val ltl_lin_seq_inv_rect_Type2 :
318 ltl_lin_seq -> (__ -> 'a1) -> (__ -> 'a1) -> (Graphs.label -> __ -> 'a1)
319 -> (Graphs.label -> __ -> 'a1) -> 'a1 **)
320 let ltl_lin_seq_inv_rect_Type2 hterm h1 h2 h3 h4 =
321 let hcut = ltl_lin_seq_rect_Type2 h1 h2 h3 h4 hterm in hcut __
323 (** val ltl_lin_seq_inv_rect_Type1 :
324 ltl_lin_seq -> (__ -> 'a1) -> (__ -> 'a1) -> (Graphs.label -> __ -> 'a1)
325 -> (Graphs.label -> __ -> 'a1) -> 'a1 **)
326 let ltl_lin_seq_inv_rect_Type1 hterm h1 h2 h3 h4 =
327 let hcut = ltl_lin_seq_rect_Type1 h1 h2 h3 h4 hterm in hcut __
329 (** val ltl_lin_seq_inv_rect_Type0 :
330 ltl_lin_seq -> (__ -> 'a1) -> (__ -> 'a1) -> (Graphs.label -> __ -> 'a1)
331 -> (Graphs.label -> __ -> 'a1) -> 'a1 **)
332 let ltl_lin_seq_inv_rect_Type0 hterm h1 h2 h3 h4 =
333 let hcut = ltl_lin_seq_rect_Type0 h1 h2 h3 h4 hterm in hcut __
335 (** val ltl_lin_seq_discr : ltl_lin_seq -> ltl_lin_seq -> __ **)
336 let ltl_lin_seq_discr x y =
337 Logic.eq_rect_Type2 x
339 | SAVE_CARRY -> Obj.magic (fun _ dH -> dH)
340 | RESTORE_CARRY -> Obj.magic (fun _ dH -> dH)
341 | LOW_ADDRESS a0 -> Obj.magic (fun _ dH -> dH __)
342 | HIGH_ADDRESS a0 -> Obj.magic (fun _ dH -> dH __)) y
344 (** val ltl_lin_seq_jmdiscr : ltl_lin_seq -> ltl_lin_seq -> __ **)
345 let ltl_lin_seq_jmdiscr x y =
346 Logic.eq_rect_Type2 x
348 | SAVE_CARRY -> Obj.magic (fun _ dH -> dH)
349 | RESTORE_CARRY -> Obj.magic (fun _ dH -> dH)
350 | LOW_ADDRESS a0 -> Obj.magic (fun _ dH -> dH __)
351 | HIGH_ADDRESS a0 -> Obj.magic (fun _ dH -> dH __)) y
353 (** val ltl_lin_seq_labels : ltl_lin_seq -> Graphs.label List.list **)
354 let ltl_lin_seq_labels = function
355 | SAVE_CARRY -> List.Nil
356 | RESTORE_CARRY -> List.Nil
357 | LOW_ADDRESS lbl -> List.Cons (lbl, List.Nil)
358 | HIGH_ADDRESS lbl -> List.Cons (lbl, List.Nil)
360 (** val lTL_LIN_uns : Joint.unserialized_params **)
362 { Joint.ext_seq_labels = (Obj.magic ltl_lin_seq_labels);
363 Joint.has_tailcalls = Bool.False }
365 (** val lTL_LIN_functs : Joint.get_pseudo_reg_functs **)
367 { Joint.acc_a_regs = (fun x -> List.Nil); Joint.acc_b_regs = (fun x ->
368 List.Nil); Joint.acc_a_args = (fun x -> List.Nil); Joint.acc_b_args =
369 (fun x -> List.Nil); Joint.dpl_regs = (fun x -> List.Nil);
370 Joint.dph_regs = (fun x -> List.Nil); Joint.dpl_args = (fun x ->
371 List.Nil); Joint.dph_args = (fun x -> List.Nil); Joint.snd_args =
372 (fun x -> List.Nil); Joint.pair_move_regs = (fun x -> List.Nil);
373 Joint.f_call_args = (fun x -> List.Nil); Joint.f_call_dest = (fun x ->
374 List.Nil); Joint.ext_seq_regs = (fun x -> List.Nil); Joint.params_regs =
375 (fun x -> List.Nil) }
377 (** val lTL_LIN : Joint.uns_params **)
379 { Joint.u_pars = lTL_LIN_uns; Joint.functs = lTL_LIN_functs }