source: extracted/eRTL.ml @ 2867

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

New extraction after indianess bug fixes by Paolo.

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