source: extracted/eRTL.ml @ 2951

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

New extraction. Novely: a pre-main is used in the back-end. Initialization
of global data is performed in LINToASM.

Note: the cost-emission of the initialization costlabel in the front-end is
virtual, but not performed in the traces I generate and print. To be fixed
(how?)

File size: 25.1 KB
Line 
1open Preamble
2
3open Extra_bool
4
5open Coqlib
6
7open Values
8
9open FrontEndVal
10
11open GenMem
12
13open FrontEndMem
14
15open Globalenvs
16
17open String
18
19open Sets
20
21open Listb
22
23open LabelledObjects
24
25open BitVectorTrie
26
27open Graphs
28
29open I8051
30
31open Order
32
33open Registers
34
35open CostLabel
36
37open Hide
38
39open Proper
40
41open PositiveMap
42
43open Deqsets
44
45open ErrorMessages
46
47open PreIdentifiers
48
49open Errors
50
51open Extralib
52
53open Lists
54
55open Identifiers
56
57open Integers
58
59open AST
60
61open Division
62
63open Exp
64
65open Arithmetic
66
67open Setoids
68
69open Monad
70
71open Option
72
73open Extranat
74
75open Vector
76
77open Div_and_mod
78
79open Jmeq
80
81open Russell
82
83open List
84
85open Util
86
87open FoldStuff
88
89open BitVector
90
91open Types
92
93open Bool
94
95open Relations
96
97open Nat
98
99open Hints_declaration
100
101open Core_notation
102
103open Pts
104
105open Logic
106
107open Positive
108
109open Z
110
111open BitVectorZ
112
113open Pointers
114
115open ByteValues
116
117open BackEndOps
118
119open Joint
120
121type move_dst =
122| PSD of Registers.register
123| HDW of I8051.register
124
125(** val move_dst_rect_Type4 :
126    (Registers.register -> 'a1) -> (I8051.register -> 'a1) -> move_dst -> 'a1 **)
127let rec move_dst_rect_Type4 h_PSD h_HDW = function
128| PSD x_18520 -> h_PSD x_18520
129| HDW x_18521 -> h_HDW x_18521
130
131(** val move_dst_rect_Type5 :
132    (Registers.register -> 'a1) -> (I8051.register -> 'a1) -> move_dst -> 'a1 **)
133let rec move_dst_rect_Type5 h_PSD h_HDW = function
134| PSD x_18525 -> h_PSD x_18525
135| HDW x_18526 -> h_HDW x_18526
136
137(** val move_dst_rect_Type3 :
138    (Registers.register -> 'a1) -> (I8051.register -> 'a1) -> move_dst -> 'a1 **)
139let rec move_dst_rect_Type3 h_PSD h_HDW = function
140| PSD x_18530 -> h_PSD x_18530
141| HDW x_18531 -> h_HDW x_18531
142
143(** val move_dst_rect_Type2 :
144    (Registers.register -> 'a1) -> (I8051.register -> 'a1) -> move_dst -> 'a1 **)
145let rec move_dst_rect_Type2 h_PSD h_HDW = function
146| PSD x_18535 -> h_PSD x_18535
147| HDW x_18536 -> h_HDW x_18536
148
149(** val move_dst_rect_Type1 :
150    (Registers.register -> 'a1) -> (I8051.register -> 'a1) -> move_dst -> 'a1 **)
151let rec move_dst_rect_Type1 h_PSD h_HDW = function
152| PSD x_18540 -> h_PSD x_18540
153| HDW x_18541 -> h_HDW x_18541
154
155(** val move_dst_rect_Type0 :
156    (Registers.register -> 'a1) -> (I8051.register -> 'a1) -> move_dst -> 'a1 **)
157let rec move_dst_rect_Type0 h_PSD h_HDW = function
158| PSD x_18545 -> h_PSD x_18545
159| HDW x_18546 -> h_HDW x_18546
160
161(** val move_dst_inv_rect_Type4 :
162    move_dst -> (Registers.register -> __ -> 'a1) -> (I8051.register -> __ ->
163    'a1) -> 'a1 **)
164let move_dst_inv_rect_Type4 hterm h1 h2 =
165  let hcut = move_dst_rect_Type4 h1 h2 hterm in hcut __
166
167(** val move_dst_inv_rect_Type3 :
168    move_dst -> (Registers.register -> __ -> 'a1) -> (I8051.register -> __ ->
169    'a1) -> 'a1 **)
170let move_dst_inv_rect_Type3 hterm h1 h2 =
171  let hcut = move_dst_rect_Type3 h1 h2 hterm in hcut __
172
173(** val move_dst_inv_rect_Type2 :
174    move_dst -> (Registers.register -> __ -> 'a1) -> (I8051.register -> __ ->
175    'a1) -> 'a1 **)
176let move_dst_inv_rect_Type2 hterm h1 h2 =
177  let hcut = move_dst_rect_Type2 h1 h2 hterm in hcut __
178
179(** val move_dst_inv_rect_Type1 :
180    move_dst -> (Registers.register -> __ -> 'a1) -> (I8051.register -> __ ->
181    'a1) -> 'a1 **)
182let move_dst_inv_rect_Type1 hterm h1 h2 =
183  let hcut = move_dst_rect_Type1 h1 h2 hterm in hcut __
184
185(** val move_dst_inv_rect_Type0 :
186    move_dst -> (Registers.register -> __ -> 'a1) -> (I8051.register -> __ ->
187    'a1) -> 'a1 **)
188let move_dst_inv_rect_Type0 hterm h1 h2 =
189  let hcut = move_dst_rect_Type0 h1 h2 hterm in hcut __
190
191(** val move_dst_discr : move_dst -> move_dst -> __ **)
192let move_dst_discr x y =
193  Logic.eq_rect_Type2 x
194    (match x with
195     | PSD a0 -> Obj.magic (fun _ dH -> dH __)
196     | HDW a0 -> Obj.magic (fun _ dH -> dH __)) y
197
198(** val move_dst_jmdiscr : move_dst -> move_dst -> __ **)
199let move_dst_jmdiscr x y =
200  Logic.eq_rect_Type2 x
201    (match x with
202     | PSD a0 -> Obj.magic (fun _ dH -> dH __)
203     | HDW a0 -> Obj.magic (fun _ dH -> dH __)) y
204
205type move_src = move_dst Joint.argument
206
207(** val move_src_from_dst : move_dst -> move_src **)
208let move_src_from_dst x =
209  Joint.Reg x
210
211(** val dpi1__o__move_dst_to_src__o__inject :
212    (move_dst, 'a1) Types.dPair -> move_src Types.sig0 **)
213let dpi1__o__move_dst_to_src__o__inject x2 =
214  move_src_from_dst x2.Types.dpi1
215
216(** val eject__o__move_dst_to_src__o__inject :
217    move_dst Types.sig0 -> move_src Types.sig0 **)
218let eject__o__move_dst_to_src__o__inject x2 =
219  move_src_from_dst (Types.pi1 x2)
220
221(** val move_dst_to_src__o__inject : move_dst -> move_src Types.sig0 **)
222let move_dst_to_src__o__inject x1 =
223  move_src_from_dst x1
224
225(** val dpi1__o__move_dst_to_src :
226    (move_dst, 'a1) Types.dPair -> move_src **)
227let dpi1__o__move_dst_to_src x1 =
228  move_src_from_dst x1.Types.dpi1
229
230(** val eject__o__move_dst_to_src : move_dst Types.sig0 -> move_src **)
231let eject__o__move_dst_to_src x1 =
232  move_src_from_dst (Types.pi1 x1)
233
234(** val psd_argument_move_src : Joint.psd_argument -> move_src **)
235let psd_argument_move_src = function
236| Joint.Reg r -> Joint.Reg (PSD r)
237| Joint.Imm b -> Joint.Imm b
238
239(** val byte_to_psd_argument__o__psd_argument_to_move_src__o__inject :
240    BitVector.byte -> move_src Types.sig0 **)
241let byte_to_psd_argument__o__psd_argument_to_move_src__o__inject x0 =
242  psd_argument_move_src (Joint.psd_argument_from_byte x0)
243
244(** val dpi1__o__byte_to_hdw_argument__o__psd_argument_to_move_src__o__inject :
245    (BitVector.byte, 'a1) Types.dPair -> move_src Types.sig0 **)
246let dpi1__o__byte_to_hdw_argument__o__psd_argument_to_move_src__o__inject x2 =
247  psd_argument_move_src (Joint.dpi1__o__byte_to_hdw_argument x2)
248
249(** val dpi1__o__byte_to_psd_argument__o__psd_argument_to_move_src__o__inject :
250    (BitVector.byte, 'a1) Types.dPair -> move_src Types.sig0 **)
251let dpi1__o__byte_to_psd_argument__o__psd_argument_to_move_src__o__inject x2 =
252  psd_argument_move_src (Joint.dpi1__o__byte_to_psd_argument x2)
253
254(** val dpi1__o__reg_to_psd_argument__o__psd_argument_to_move_src__o__inject :
255    (Registers.register, 'a1) Types.dPair -> move_src Types.sig0 **)
256let dpi1__o__reg_to_psd_argument__o__psd_argument_to_move_src__o__inject x2 =
257  psd_argument_move_src (Joint.dpi1__o__reg_to_psd_argument x2)
258
259(** val eject__o__byte_to_hdw_argument__o__psd_argument_to_move_src__o__inject :
260    BitVector.byte Types.sig0 -> move_src Types.sig0 **)
261let eject__o__byte_to_hdw_argument__o__psd_argument_to_move_src__o__inject x2 =
262  psd_argument_move_src (Joint.eject__o__byte_to_hdw_argument x2)
263
264(** val eject__o__byte_to_psd_argument__o__psd_argument_to_move_src__o__inject :
265    BitVector.byte Types.sig0 -> move_src Types.sig0 **)
266let eject__o__byte_to_psd_argument__o__psd_argument_to_move_src__o__inject x2 =
267  psd_argument_move_src (Joint.eject__o__byte_to_psd_argument x2)
268
269(** val eject__o__reg_to_psd_argument__o__psd_argument_to_move_src__o__inject :
270    Registers.register Types.sig0 -> move_src Types.sig0 **)
271let eject__o__reg_to_psd_argument__o__psd_argument_to_move_src__o__inject x2 =
272  psd_argument_move_src (Joint.eject__o__reg_to_psd_argument x2)
273
274(** val reg_to_psd_argument__o__psd_argument_to_move_src__o__inject :
275    Registers.register -> move_src Types.sig0 **)
276let reg_to_psd_argument__o__psd_argument_to_move_src__o__inject x0 =
277  psd_argument_move_src (Joint.psd_argument_from_reg x0)
278
279(** val dpi1__o__psd_argument_to_move_src__o__inject :
280    (Joint.psd_argument, 'a1) Types.dPair -> move_src Types.sig0 **)
281let dpi1__o__psd_argument_to_move_src__o__inject x2 =
282  psd_argument_move_src x2.Types.dpi1
283
284(** val eject__o__psd_argument_to_move_src__o__inject :
285    Joint.psd_argument Types.sig0 -> move_src Types.sig0 **)
286let eject__o__psd_argument_to_move_src__o__inject x2 =
287  psd_argument_move_src (Types.pi1 x2)
288
289(** val psd_argument_to_move_src__o__inject :
290    Joint.psd_argument -> move_src Types.sig0 **)
291let psd_argument_to_move_src__o__inject x1 =
292  psd_argument_move_src x1
293
294(** val byte_to_psd_argument__o__psd_argument_to_move_src :
295    BitVector.byte -> move_src **)
296let byte_to_psd_argument__o__psd_argument_to_move_src x0 =
297  psd_argument_move_src (Joint.psd_argument_from_byte x0)
298
299(** val dpi1__o__byte_to_hdw_argument__o__psd_argument_to_move_src :
300    (BitVector.byte, 'a1) Types.dPair -> move_src **)
301let dpi1__o__byte_to_hdw_argument__o__psd_argument_to_move_src x1 =
302  psd_argument_move_src (Joint.dpi1__o__byte_to_hdw_argument x1)
303
304(** val dpi1__o__byte_to_psd_argument__o__psd_argument_to_move_src :
305    (BitVector.byte, 'a1) Types.dPair -> move_src **)
306let dpi1__o__byte_to_psd_argument__o__psd_argument_to_move_src x1 =
307  psd_argument_move_src (Joint.dpi1__o__byte_to_psd_argument x1)
308
309(** val dpi1__o__reg_to_psd_argument__o__psd_argument_to_move_src :
310    (Registers.register, 'a1) Types.dPair -> move_src **)
311let dpi1__o__reg_to_psd_argument__o__psd_argument_to_move_src x1 =
312  psd_argument_move_src (Joint.dpi1__o__reg_to_psd_argument x1)
313
314(** val eject__o__byte_to_hdw_argument__o__psd_argument_to_move_src :
315    BitVector.byte Types.sig0 -> move_src **)
316let eject__o__byte_to_hdw_argument__o__psd_argument_to_move_src x1 =
317  psd_argument_move_src (Joint.eject__o__byte_to_hdw_argument x1)
318
319(** val eject__o__byte_to_psd_argument__o__psd_argument_to_move_src :
320    BitVector.byte Types.sig0 -> move_src **)
321let eject__o__byte_to_psd_argument__o__psd_argument_to_move_src x1 =
322  psd_argument_move_src (Joint.eject__o__byte_to_psd_argument x1)
323
324(** val eject__o__reg_to_psd_argument__o__psd_argument_to_move_src :
325    Registers.register Types.sig0 -> move_src **)
326let eject__o__reg_to_psd_argument__o__psd_argument_to_move_src x1 =
327  psd_argument_move_src (Joint.eject__o__reg_to_psd_argument x1)
328
329(** val reg_to_psd_argument__o__psd_argument_to_move_src :
330    Registers.register -> move_src **)
331let reg_to_psd_argument__o__psd_argument_to_move_src x0 =
332  psd_argument_move_src (Joint.psd_argument_from_reg x0)
333
334(** val dpi1__o__psd_argument_to_move_src :
335    (Joint.psd_argument, 'a1) Types.dPair -> move_src **)
336let dpi1__o__psd_argument_to_move_src x1 =
337  psd_argument_move_src x1.Types.dpi1
338
339(** val eject__o__psd_argument_to_move_src :
340    Joint.psd_argument Types.sig0 -> move_src **)
341let eject__o__psd_argument_to_move_src x1 =
342  psd_argument_move_src (Types.pi1 x1)
343
344type ertl_seq =
345| Ertl_new_frame
346| Ertl_del_frame
347| Ertl_frame_size of Registers.register
348
349(** val ertl_seq_rect_Type4 :
350    'a1 -> 'a1 -> (Registers.register -> 'a1) -> ertl_seq -> 'a1 **)
351let rec ertl_seq_rect_Type4 h_ertl_new_frame h_ertl_del_frame h_ertl_frame_size = function
352| Ertl_new_frame -> h_ertl_new_frame
353| Ertl_del_frame -> h_ertl_del_frame
354| Ertl_frame_size x_18585 -> h_ertl_frame_size x_18585
355
356(** val ertl_seq_rect_Type5 :
357    'a1 -> 'a1 -> (Registers.register -> 'a1) -> ertl_seq -> 'a1 **)
358let rec ertl_seq_rect_Type5 h_ertl_new_frame h_ertl_del_frame h_ertl_frame_size = function
359| Ertl_new_frame -> h_ertl_new_frame
360| Ertl_del_frame -> h_ertl_del_frame
361| Ertl_frame_size x_18590 -> h_ertl_frame_size x_18590
362
363(** val ertl_seq_rect_Type3 :
364    'a1 -> 'a1 -> (Registers.register -> 'a1) -> ertl_seq -> 'a1 **)
365let rec ertl_seq_rect_Type3 h_ertl_new_frame h_ertl_del_frame h_ertl_frame_size = function
366| Ertl_new_frame -> h_ertl_new_frame
367| Ertl_del_frame -> h_ertl_del_frame
368| Ertl_frame_size x_18595 -> h_ertl_frame_size x_18595
369
370(** val ertl_seq_rect_Type2 :
371    'a1 -> 'a1 -> (Registers.register -> 'a1) -> ertl_seq -> 'a1 **)
372let rec ertl_seq_rect_Type2 h_ertl_new_frame h_ertl_del_frame h_ertl_frame_size = function
373| Ertl_new_frame -> h_ertl_new_frame
374| Ertl_del_frame -> h_ertl_del_frame
375| Ertl_frame_size x_18600 -> h_ertl_frame_size x_18600
376
377(** val ertl_seq_rect_Type1 :
378    'a1 -> 'a1 -> (Registers.register -> 'a1) -> ertl_seq -> 'a1 **)
379let rec ertl_seq_rect_Type1 h_ertl_new_frame h_ertl_del_frame h_ertl_frame_size = function
380| Ertl_new_frame -> h_ertl_new_frame
381| Ertl_del_frame -> h_ertl_del_frame
382| Ertl_frame_size x_18605 -> h_ertl_frame_size x_18605
383
384(** val ertl_seq_rect_Type0 :
385    'a1 -> 'a1 -> (Registers.register -> 'a1) -> ertl_seq -> 'a1 **)
386let rec ertl_seq_rect_Type0 h_ertl_new_frame h_ertl_del_frame h_ertl_frame_size = function
387| Ertl_new_frame -> h_ertl_new_frame
388| Ertl_del_frame -> h_ertl_del_frame
389| Ertl_frame_size x_18610 -> h_ertl_frame_size x_18610
390
391(** val ertl_seq_inv_rect_Type4 :
392    ertl_seq -> (__ -> 'a1) -> (__ -> 'a1) -> (Registers.register -> __ ->
393    'a1) -> 'a1 **)
394let ertl_seq_inv_rect_Type4 hterm h1 h2 h3 =
395  let hcut = ertl_seq_rect_Type4 h1 h2 h3 hterm in hcut __
396
397(** val ertl_seq_inv_rect_Type3 :
398    ertl_seq -> (__ -> 'a1) -> (__ -> 'a1) -> (Registers.register -> __ ->
399    'a1) -> 'a1 **)
400let ertl_seq_inv_rect_Type3 hterm h1 h2 h3 =
401  let hcut = ertl_seq_rect_Type3 h1 h2 h3 hterm in hcut __
402
403(** val ertl_seq_inv_rect_Type2 :
404    ertl_seq -> (__ -> 'a1) -> (__ -> 'a1) -> (Registers.register -> __ ->
405    'a1) -> 'a1 **)
406let ertl_seq_inv_rect_Type2 hterm h1 h2 h3 =
407  let hcut = ertl_seq_rect_Type2 h1 h2 h3 hterm in hcut __
408
409(** val ertl_seq_inv_rect_Type1 :
410    ertl_seq -> (__ -> 'a1) -> (__ -> 'a1) -> (Registers.register -> __ ->
411    'a1) -> 'a1 **)
412let ertl_seq_inv_rect_Type1 hterm h1 h2 h3 =
413  let hcut = ertl_seq_rect_Type1 h1 h2 h3 hterm in hcut __
414
415(** val ertl_seq_inv_rect_Type0 :
416    ertl_seq -> (__ -> 'a1) -> (__ -> 'a1) -> (Registers.register -> __ ->
417    'a1) -> 'a1 **)
418let ertl_seq_inv_rect_Type0 hterm h1 h2 h3 =
419  let hcut = ertl_seq_rect_Type0 h1 h2 h3 hterm in hcut __
420
421(** val ertl_seq_discr : ertl_seq -> ertl_seq -> __ **)
422let ertl_seq_discr x y =
423  Logic.eq_rect_Type2 x
424    (match x with
425     | Ertl_new_frame -> Obj.magic (fun _ dH -> dH)
426     | Ertl_del_frame -> Obj.magic (fun _ dH -> dH)
427     | Ertl_frame_size a0 -> Obj.magic (fun _ dH -> dH __)) y
428
429(** val ertl_seq_jmdiscr : ertl_seq -> ertl_seq -> __ **)
430let ertl_seq_jmdiscr x y =
431  Logic.eq_rect_Type2 x
432    (match x with
433     | Ertl_new_frame -> Obj.magic (fun _ dH -> dH)
434     | Ertl_del_frame -> Obj.magic (fun _ dH -> dH)
435     | Ertl_frame_size a0 -> Obj.magic (fun _ dH -> dH __)) y
436
437(** val eRTL_uns : Joint.unserialized_params **)
438let eRTL_uns =
439  { Joint.ext_seq_labels = (fun x -> List.Nil); Joint.has_tailcalls =
440    Bool.False }
441
442(** val regs_from_move_dst : move_dst -> Registers.register List.list **)
443let regs_from_move_dst = function
444| PSD r -> List.Cons (r, List.Nil)
445| HDW x -> List.Nil
446
447(** val regs_from_move_src : move_src -> Registers.register List.list **)
448let regs_from_move_src = function
449| Joint.Reg r ->
450  (match r with
451   | PSD r1 -> List.Cons (r1, List.Nil)
452   | HDW x -> List.Nil)
453| Joint.Imm x -> List.Nil
454
455(** val ertl_ext_seq_regs : ertl_seq -> Registers.register List.list **)
456let ertl_ext_seq_regs = function
457| Ertl_new_frame -> List.Nil
458| Ertl_del_frame -> List.Nil
459| Ertl_frame_size r -> List.Cons (r, List.Nil)
460
461(** val eRTL_functs : Joint.get_pseudo_reg_functs **)
462let eRTL_functs =
463  { Joint.acc_a_regs = (fun r -> List.Cons ((Obj.magic r), List.Nil));
464    Joint.acc_b_regs = (fun r -> List.Cons ((Obj.magic r), List.Nil));
465    Joint.acc_a_args = (fun arg ->
466    match Obj.magic arg with
467    | Joint.Reg r -> List.Cons (r, List.Nil)
468    | Joint.Imm x -> List.Nil); Joint.acc_b_args = (fun arg ->
469    match Obj.magic arg with
470    | Joint.Reg r -> List.Cons (r, List.Nil)
471    | Joint.Imm x -> List.Nil); Joint.dpl_regs = (fun r -> List.Cons
472    ((Obj.magic r), List.Nil)); Joint.dph_regs = (fun r -> List.Cons
473    ((Obj.magic r), List.Nil)); Joint.dpl_args = (fun arg ->
474    match Obj.magic arg with
475    | Joint.Reg r -> List.Cons (r, List.Nil)
476    | Joint.Imm x -> List.Nil); Joint.dph_args = (fun arg ->
477    match Obj.magic arg with
478    | Joint.Reg r -> List.Cons (r, List.Nil)
479    | Joint.Imm x -> List.Nil); Joint.snd_args = (fun arg ->
480    match Obj.magic arg with
481    | Joint.Reg r -> List.Cons (r, List.Nil)
482    | Joint.Imm x -> List.Nil); Joint.pair_move_regs = (fun x ->
483    List.append (regs_from_move_dst (Obj.magic x).Types.fst)
484      (regs_from_move_src (Obj.magic x).Types.snd)); Joint.f_call_args =
485    (fun x -> List.Nil); Joint.f_call_dest = (fun x -> List.Nil);
486    Joint.ext_seq_regs = (Obj.magic ertl_ext_seq_regs); Joint.params_regs =
487    (fun x -> List.Nil) }
488
489(** val eRTL : Joint.graph_params **)
490let eRTL =
491  { Joint.u_pars = eRTL_uns; Joint.functs = eRTL_functs }
492
493type ertl_program = Joint.joint_program
494
495(** val dpi1__o__reg_to_ertl_snd_argument__o__inject :
496    (Registers.register, 'a1) Types.dPair -> Joint.psd_argument Types.sig0 **)
497let dpi1__o__reg_to_ertl_snd_argument__o__inject x2 =
498  Joint.psd_argument_from_reg x2.Types.dpi1
499
500(** val dpi1__o__reg_to_ertl_snd_argument__o__psd_argument_to_move_src__o__inject :
501    (Registers.register, 'a1) Types.dPair -> move_src Types.sig0 **)
502let dpi1__o__reg_to_ertl_snd_argument__o__psd_argument_to_move_src__o__inject x2 =
503  psd_argument_to_move_src__o__inject
504    (Joint.psd_argument_from_reg x2.Types.dpi1)
505
506(** val dpi1__o__reg_to_ertl_snd_argument__o__psd_argument_to_move_src :
507    (Registers.register, 'a1) Types.dPair -> move_src **)
508let dpi1__o__reg_to_ertl_snd_argument__o__psd_argument_to_move_src x1 =
509  psd_argument_move_src (Joint.psd_argument_from_reg x1.Types.dpi1)
510
511(** val eject__o__reg_to_ertl_snd_argument__o__inject :
512    Registers.register Types.sig0 -> Joint.psd_argument Types.sig0 **)
513let eject__o__reg_to_ertl_snd_argument__o__inject x2 =
514  Joint.psd_argument_from_reg (Types.pi1 x2)
515
516(** val eject__o__reg_to_ertl_snd_argument__o__psd_argument_to_move_src__o__inject :
517    Registers.register Types.sig0 -> move_src Types.sig0 **)
518let eject__o__reg_to_ertl_snd_argument__o__psd_argument_to_move_src__o__inject x2 =
519  psd_argument_to_move_src__o__inject
520    (Joint.psd_argument_from_reg (Types.pi1 x2))
521
522(** val eject__o__reg_to_ertl_snd_argument__o__psd_argument_to_move_src :
523    Registers.register Types.sig0 -> move_src **)
524let eject__o__reg_to_ertl_snd_argument__o__psd_argument_to_move_src x1 =
525  psd_argument_move_src (Joint.psd_argument_from_reg (Types.pi1 x1))
526
527(** val reg_to_ertl_snd_argument__o__psd_argument_to_move_src :
528    Registers.register -> move_src **)
529let reg_to_ertl_snd_argument__o__psd_argument_to_move_src x0 =
530  psd_argument_move_src (Joint.psd_argument_from_reg x0)
531
532(** val reg_to_ertl_snd_argument__o__psd_argument_to_move_src__o__inject :
533    Registers.register -> move_src Types.sig0 **)
534let reg_to_ertl_snd_argument__o__psd_argument_to_move_src__o__inject x1 =
535  psd_argument_to_move_src__o__inject (Joint.psd_argument_from_reg x1)
536
537(** val reg_to_ertl_snd_argument__o__inject :
538    Registers.register -> Joint.psd_argument Types.sig0 **)
539let reg_to_ertl_snd_argument__o__inject x1 =
540  Joint.psd_argument_from_reg x1
541
542(** val dpi1__o__reg_to_ertl_snd_argument :
543    (Registers.register, 'a1) Types.dPair -> Joint.psd_argument **)
544let dpi1__o__reg_to_ertl_snd_argument x1 =
545  Joint.psd_argument_from_reg x1.Types.dpi1
546
547(** val eject__o__reg_to_ertl_snd_argument :
548    Registers.register Types.sig0 -> Joint.psd_argument **)
549let eject__o__reg_to_ertl_snd_argument x1 =
550  Joint.psd_argument_from_reg (Types.pi1 x1)
551
552(** val dpi1__o__byte_to_ertl_snd_argument__o__inject :
553    (BitVector.byte, 'a1) Types.dPair -> Joint.psd_argument Types.sig0 **)
554let dpi1__o__byte_to_ertl_snd_argument__o__inject x2 =
555  Joint.psd_argument_from_byte x2.Types.dpi1
556
557(** val dpi1__o__byte_to_ertl_snd_argument__o__psd_argument_to_move_src__o__inject :
558    (BitVector.byte, 'a1) Types.dPair -> move_src Types.sig0 **)
559let dpi1__o__byte_to_ertl_snd_argument__o__psd_argument_to_move_src__o__inject x2 =
560  psd_argument_to_move_src__o__inject
561    (Joint.psd_argument_from_byte x2.Types.dpi1)
562
563(** val dpi1__o__byte_to_ertl_snd_argument__o__psd_argument_to_move_src :
564    (BitVector.byte, 'a1) Types.dPair -> move_src **)
565let dpi1__o__byte_to_ertl_snd_argument__o__psd_argument_to_move_src x1 =
566  psd_argument_move_src (Joint.psd_argument_from_byte x1.Types.dpi1)
567
568(** val eject__o__byte_to_ertl_snd_argument__o__inject :
569    BitVector.byte Types.sig0 -> Joint.psd_argument Types.sig0 **)
570let eject__o__byte_to_ertl_snd_argument__o__inject x2 =
571  Joint.psd_argument_from_byte (Types.pi1 x2)
572
573(** val eject__o__byte_to_ertl_snd_argument__o__psd_argument_to_move_src__o__inject :
574    BitVector.byte Types.sig0 -> move_src Types.sig0 **)
575let eject__o__byte_to_ertl_snd_argument__o__psd_argument_to_move_src__o__inject x2 =
576  psd_argument_to_move_src__o__inject
577    (Joint.psd_argument_from_byte (Types.pi1 x2))
578
579(** val eject__o__byte_to_ertl_snd_argument__o__psd_argument_to_move_src :
580    BitVector.byte Types.sig0 -> move_src **)
581let eject__o__byte_to_ertl_snd_argument__o__psd_argument_to_move_src x1 =
582  psd_argument_move_src (Joint.psd_argument_from_byte (Types.pi1 x1))
583
584(** val byte_to_ertl_snd_argument__o__psd_argument_to_move_src :
585    BitVector.byte -> move_src **)
586let byte_to_ertl_snd_argument__o__psd_argument_to_move_src x0 =
587  psd_argument_move_src (Joint.psd_argument_from_byte x0)
588
589(** val byte_to_ertl_snd_argument__o__psd_argument_to_move_src__o__inject :
590    BitVector.byte -> move_src Types.sig0 **)
591let byte_to_ertl_snd_argument__o__psd_argument_to_move_src__o__inject x1 =
592  psd_argument_to_move_src__o__inject (Joint.psd_argument_from_byte x1)
593
594(** val byte_to_ertl_snd_argument__o__inject :
595    BitVector.byte -> Joint.psd_argument Types.sig0 **)
596let byte_to_ertl_snd_argument__o__inject x1 =
597  Joint.psd_argument_from_byte x1
598
599(** val dpi1__o__byte_to_ertl_snd_argument :
600    (BitVector.byte, 'a1) Types.dPair -> Joint.psd_argument **)
601let dpi1__o__byte_to_ertl_snd_argument x1 =
602  Joint.psd_argument_from_byte x1.Types.dpi1
603
604(** val eject__o__byte_to_ertl_snd_argument :
605    BitVector.byte Types.sig0 -> Joint.psd_argument **)
606let eject__o__byte_to_ertl_snd_argument x1 =
607  Joint.psd_argument_from_byte (Types.pi1 x1)
608
609(** val ertl_seq_joint : AST.ident List.list -> __ -> Joint.joint_seq **)
610let ertl_seq_joint =
611  Obj.magic (fun _ x -> Joint.Extension_seq x)
612
613(** val dpi1__o__ertl_seq_to_joint_seq__o__inject :
614    AST.ident List.list -> (__, 'a1) Types.dPair -> Joint.joint_seq
615    Types.sig0 **)
616let dpi1__o__ertl_seq_to_joint_seq__o__inject x1 x2 =
617  ertl_seq_joint x1 x2.Types.dpi1
618
619(** val dpi1__o__ertl_seq_to_joint_seq__o__seq_to_step__o__inject :
620    AST.ident List.list -> (__, 'a1) Types.dPair -> Joint.joint_step
621    Types.sig0 **)
622let dpi1__o__ertl_seq_to_joint_seq__o__seq_to_step__o__inject x1 x2 =
623  Joint.seq_to_step__o__inject
624    (Joint.gp_to_p__o__stmt_pars__o__uns_pars__o__u_pars eRTL) x1
625    (ertl_seq_joint x1 x2.Types.dpi1)
626
627(** val dpi1__o__ertl_seq_to_joint_seq__o__seq_to_step :
628    AST.ident List.list -> (__, 'a1) Types.dPair -> Joint.joint_step **)
629let dpi1__o__ertl_seq_to_joint_seq__o__seq_to_step x1 x2 =
630  Joint.Step_seq (ertl_seq_joint x1 x2.Types.dpi1)
631
632(** val eject__o__ertl_seq_to_joint_seq__o__inject :
633    AST.ident List.list -> __ Types.sig0 -> Joint.joint_seq Types.sig0 **)
634let eject__o__ertl_seq_to_joint_seq__o__inject x1 x2 =
635  ertl_seq_joint x1 (Types.pi1 x2)
636
637(** val eject__o__ertl_seq_to_joint_seq__o__seq_to_step__o__inject :
638    AST.ident List.list -> __ Types.sig0 -> Joint.joint_step Types.sig0 **)
639let eject__o__ertl_seq_to_joint_seq__o__seq_to_step__o__inject x1 x2 =
640  Joint.seq_to_step__o__inject
641    (Joint.gp_to_p__o__stmt_pars__o__uns_pars__o__u_pars eRTL) x1
642    (ertl_seq_joint x1 (Types.pi1 x2))
643
644(** val eject__o__ertl_seq_to_joint_seq__o__seq_to_step :
645    AST.ident List.list -> __ Types.sig0 -> Joint.joint_step **)
646let eject__o__ertl_seq_to_joint_seq__o__seq_to_step x1 x2 =
647  Joint.Step_seq (ertl_seq_joint x1 (Types.pi1 x2))
648
649(** val ertl_seq_to_joint_seq__o__seq_to_step :
650    AST.ident List.list -> __ -> Joint.joint_step **)
651let ertl_seq_to_joint_seq__o__seq_to_step x0 x1 =
652  Joint.Step_seq (ertl_seq_joint x0 x1)
653
654(** val ertl_seq_to_joint_seq__o__seq_to_step__o__inject :
655    AST.ident List.list -> __ -> Joint.joint_step Types.sig0 **)
656let ertl_seq_to_joint_seq__o__seq_to_step__o__inject x0 x1 =
657  Joint.seq_to_step__o__inject
658    (Joint.gp_to_p__o__stmt_pars__o__uns_pars__o__u_pars eRTL) x0
659    (ertl_seq_joint x0 x1)
660
661(** val ertl_seq_to_joint_seq__o__inject :
662    AST.ident List.list -> __ -> Joint.joint_seq Types.sig0 **)
663let ertl_seq_to_joint_seq__o__inject x0 x1 =
664  ertl_seq_joint x0 x1
665
666(** val dpi1__o__ertl_seq_to_joint_seq :
667    AST.ident List.list -> (__, 'a1) Types.dPair -> Joint.joint_seq **)
668let dpi1__o__ertl_seq_to_joint_seq x1 x2 =
669  ertl_seq_joint x1 x2.Types.dpi1
670
671(** val eject__o__ertl_seq_to_joint_seq :
672    AST.ident List.list -> __ Types.sig0 -> Joint.joint_seq **)
673let eject__o__ertl_seq_to_joint_seq x1 x2 =
674  ertl_seq_joint x1 (Types.pi1 x2)
675
676(** val eRTL_premain :
677    ertl_program -> Joint.joint_closed_internal_function **)
678let eRTL_premain p =
679  let l1 = Positive.One in
680  let l2 = Positive.P0 Positive.One in
681  let l3 = Positive.P1 Positive.One in
682  let res = { Joint.joint_if_luniverse = (Positive.P0 (Positive.P0
683    Positive.One)); Joint.joint_if_runiverse = Positive.One;
684    Joint.joint_if_result = (Obj.magic Types.It); Joint.joint_if_params =
685    (Obj.magic (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))));
686    Joint.joint_if_stacksize = Nat.O; Joint.joint_if_local_stacksize = Nat.O;
687    Joint.joint_if_code =
688    (Obj.magic (Identifiers.empty_map PreIdentifiers.LabelTag));
689    Joint.joint_if_entry = (Obj.magic l1) }
690  in
691  let res0 =
692    Joint.add_graph eRTL (AST.prog_var_names p.Joint.joint_prog) l1
693      (Joint.Sequential ((Joint.COST_LABEL p.Joint.init_cost_label),
694      (Obj.magic l2))) res
695  in
696  let res1 =
697    Joint.add_graph eRTL (AST.prog_var_names p.Joint.joint_prog) l2
698      (Joint.Sequential ((Joint.CALL ((Types.Inl
699      p.Joint.joint_prog.AST.prog_main),
700      (Obj.magic (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))),
701      (Obj.magic Types.It))), (Obj.magic l3))) res0
702  in
703  let res2 =
704    Joint.add_graph eRTL (AST.prog_var_names p.Joint.joint_prog) l3
705      (Joint.Final (Joint.GOTO l3)) res1
706  in
707  res2
708
Note: See TracBrowser for help on using the repository browser.