source: extracted/eRTL.ml @ 2746

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

Latest version of the compiler, extracted with the latest version of Matita.
Some files still need some manual patching to avoid an extraction bug
(see PROBLEMS file).

File size: 21.7 KB
Line 
1open Preamble
2
3open String
4
5open Sets
6
7open Listb
8
9open LabelledObjects
10
11open Graphs
12
13open I8051
14
15open Order
16
17open Registers
18
19open BitVectorTrie
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 Setoids
40
41open Monad
42
43open Option
44
45open Lists
46
47open Identifiers
48
49open Integers
50
51open AST
52
53open Division
54
55open Exp
56
57open Arithmetic
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_20901 -> h_PSD x_20901
115| HDW x_20902 -> h_HDW x_20902
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_20906 -> h_PSD x_20906
121| HDW x_20907 -> h_HDW x_20907
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_20911 -> h_PSD x_20911
127| HDW x_20912 -> h_HDW x_20912
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_20916 -> h_PSD x_20916
133| HDW x_20917 -> h_HDW x_20917
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_20921 -> h_PSD x_20921
139| HDW x_20922 -> h_HDW x_20922
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_20926 -> h_PSD x_20926
145| HDW x_20927 -> h_HDW x_20927
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_20966 -> h_ertl_frame_size x_20966
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_20971 -> h_ertl_frame_size x_20971
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_20976 -> h_ertl_frame_size x_20976
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_20981 -> h_ertl_frame_size x_20981
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_20986 -> h_ertl_frame_size x_20986
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_20991 -> h_ertl_frame_size x_20991
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 eRTL : Joint.graph_params **)
429let eRTL =
430  eRTL_uns
431
432type ertl_program = Joint.joint_program
433
434(** val dpi1__o__reg_to_ertl_snd_argument__o__inject :
435    (Registers.register, 'a1) Types.dPair -> Joint.psd_argument Types.sig0 **)
436let dpi1__o__reg_to_ertl_snd_argument__o__inject x2 =
437  Joint.psd_argument_from_reg x2.Types.dpi1
438
439(** val dpi1__o__reg_to_ertl_snd_argument__o__psd_argument_to_move_src__o__inject :
440    (Registers.register, 'a1) Types.dPair -> move_src Types.sig0 **)
441let dpi1__o__reg_to_ertl_snd_argument__o__psd_argument_to_move_src__o__inject x2 =
442  psd_argument_to_move_src__o__inject
443    (Joint.psd_argument_from_reg x2.Types.dpi1)
444
445(** val dpi1__o__reg_to_ertl_snd_argument__o__psd_argument_to_move_src :
446    (Registers.register, 'a1) Types.dPair -> move_src **)
447let dpi1__o__reg_to_ertl_snd_argument__o__psd_argument_to_move_src x1 =
448  psd_argument_move_src (Joint.psd_argument_from_reg x1.Types.dpi1)
449
450(** val eject__o__reg_to_ertl_snd_argument__o__inject :
451    Registers.register Types.sig0 -> Joint.psd_argument Types.sig0 **)
452let eject__o__reg_to_ertl_snd_argument__o__inject x2 =
453  Joint.psd_argument_from_reg (Types.pi1 x2)
454
455(** val eject__o__reg_to_ertl_snd_argument__o__psd_argument_to_move_src__o__inject :
456    Registers.register Types.sig0 -> move_src Types.sig0 **)
457let eject__o__reg_to_ertl_snd_argument__o__psd_argument_to_move_src__o__inject x2 =
458  psd_argument_to_move_src__o__inject
459    (Joint.psd_argument_from_reg (Types.pi1 x2))
460
461(** val eject__o__reg_to_ertl_snd_argument__o__psd_argument_to_move_src :
462    Registers.register Types.sig0 -> move_src **)
463let eject__o__reg_to_ertl_snd_argument__o__psd_argument_to_move_src x1 =
464  psd_argument_move_src (Joint.psd_argument_from_reg (Types.pi1 x1))
465
466(** val reg_to_ertl_snd_argument__o__psd_argument_to_move_src :
467    Registers.register -> move_src **)
468let reg_to_ertl_snd_argument__o__psd_argument_to_move_src x0 =
469  psd_argument_move_src (Joint.psd_argument_from_reg x0)
470
471(** val reg_to_ertl_snd_argument__o__psd_argument_to_move_src__o__inject :
472    Registers.register -> move_src Types.sig0 **)
473let reg_to_ertl_snd_argument__o__psd_argument_to_move_src__o__inject x1 =
474  psd_argument_to_move_src__o__inject (Joint.psd_argument_from_reg x1)
475
476(** val reg_to_ertl_snd_argument__o__inject :
477    Registers.register -> Joint.psd_argument Types.sig0 **)
478let reg_to_ertl_snd_argument__o__inject x1 =
479  Joint.psd_argument_from_reg x1
480
481(** val dpi1__o__reg_to_ertl_snd_argument :
482    (Registers.register, 'a1) Types.dPair -> Joint.psd_argument **)
483let dpi1__o__reg_to_ertl_snd_argument x1 =
484  Joint.psd_argument_from_reg x1.Types.dpi1
485
486(** val eject__o__reg_to_ertl_snd_argument :
487    Registers.register Types.sig0 -> Joint.psd_argument **)
488let eject__o__reg_to_ertl_snd_argument x1 =
489  Joint.psd_argument_from_reg (Types.pi1 x1)
490
491(** val dpi1__o__byte_to_ertl_snd_argument__o__inject :
492    (BitVector.byte, 'a1) Types.dPair -> Joint.psd_argument Types.sig0 **)
493let dpi1__o__byte_to_ertl_snd_argument__o__inject x2 =
494  Joint.psd_argument_from_byte x2.Types.dpi1
495
496(** val dpi1__o__byte_to_ertl_snd_argument__o__psd_argument_to_move_src__o__inject :
497    (BitVector.byte, 'a1) Types.dPair -> move_src Types.sig0 **)
498let dpi1__o__byte_to_ertl_snd_argument__o__psd_argument_to_move_src__o__inject x2 =
499  psd_argument_to_move_src__o__inject
500    (Joint.psd_argument_from_byte x2.Types.dpi1)
501
502(** val dpi1__o__byte_to_ertl_snd_argument__o__psd_argument_to_move_src :
503    (BitVector.byte, 'a1) Types.dPair -> move_src **)
504let dpi1__o__byte_to_ertl_snd_argument__o__psd_argument_to_move_src x1 =
505  psd_argument_move_src (Joint.psd_argument_from_byte x1.Types.dpi1)
506
507(** val eject__o__byte_to_ertl_snd_argument__o__inject :
508    BitVector.byte Types.sig0 -> Joint.psd_argument Types.sig0 **)
509let eject__o__byte_to_ertl_snd_argument__o__inject x2 =
510  Joint.psd_argument_from_byte (Types.pi1 x2)
511
512(** val eject__o__byte_to_ertl_snd_argument__o__psd_argument_to_move_src__o__inject :
513    BitVector.byte Types.sig0 -> move_src Types.sig0 **)
514let eject__o__byte_to_ertl_snd_argument__o__psd_argument_to_move_src__o__inject x2 =
515  psd_argument_to_move_src__o__inject
516    (Joint.psd_argument_from_byte (Types.pi1 x2))
517
518(** val eject__o__byte_to_ertl_snd_argument__o__psd_argument_to_move_src :
519    BitVector.byte Types.sig0 -> move_src **)
520let eject__o__byte_to_ertl_snd_argument__o__psd_argument_to_move_src x1 =
521  psd_argument_move_src (Joint.psd_argument_from_byte (Types.pi1 x1))
522
523(** val byte_to_ertl_snd_argument__o__psd_argument_to_move_src :
524    BitVector.byte -> move_src **)
525let byte_to_ertl_snd_argument__o__psd_argument_to_move_src x0 =
526  psd_argument_move_src (Joint.psd_argument_from_byte x0)
527
528(** val byte_to_ertl_snd_argument__o__psd_argument_to_move_src__o__inject :
529    BitVector.byte -> move_src Types.sig0 **)
530let byte_to_ertl_snd_argument__o__psd_argument_to_move_src__o__inject x1 =
531  psd_argument_to_move_src__o__inject (Joint.psd_argument_from_byte x1)
532
533(** val byte_to_ertl_snd_argument__o__inject :
534    BitVector.byte -> Joint.psd_argument Types.sig0 **)
535let byte_to_ertl_snd_argument__o__inject x1 =
536  Joint.psd_argument_from_byte x1
537
538(** val dpi1__o__byte_to_ertl_snd_argument :
539    (BitVector.byte, 'a1) Types.dPair -> Joint.psd_argument **)
540let dpi1__o__byte_to_ertl_snd_argument x1 =
541  Joint.psd_argument_from_byte x1.Types.dpi1
542
543(** val eject__o__byte_to_ertl_snd_argument :
544    BitVector.byte Types.sig0 -> Joint.psd_argument **)
545let eject__o__byte_to_ertl_snd_argument x1 =
546  Joint.psd_argument_from_byte (Types.pi1 x1)
547
548(** val ertl_seq_joint : AST.ident List.list -> __ -> Joint.joint_seq **)
549let ertl_seq_joint =
550  Obj.magic (fun _ x -> Joint.Extension_seq x)
551
552(** val dpi1__o__ertl_seq_to_joint_seq__o__inject :
553    AST.ident List.list -> (__, 'a1) Types.dPair -> Joint.joint_seq
554    Types.sig0 **)
555let dpi1__o__ertl_seq_to_joint_seq__o__inject x1 x2 =
556  ertl_seq_joint x1 x2.Types.dpi1
557
558(** val dpi1__o__ertl_seq_to_joint_seq__o__seq_to_step__o__inject :
559    AST.ident List.list -> (__, 'a1) Types.dPair -> Joint.joint_step
560    Types.sig0 **)
561let dpi1__o__ertl_seq_to_joint_seq__o__seq_to_step__o__inject x1 x2 =
562  Joint.seq_to_step__o__inject
563    (Joint.gp_to_p__o__stmt_pars__o__uns_pars eRTL) x1
564    (ertl_seq_joint x1 x2.Types.dpi1)
565
566(** val dpi1__o__ertl_seq_to_joint_seq__o__seq_to_step :
567    AST.ident List.list -> (__, 'a1) Types.dPair -> Joint.joint_step **)
568let dpi1__o__ertl_seq_to_joint_seq__o__seq_to_step x1 x2 =
569  Joint.Step_seq (ertl_seq_joint x1 x2.Types.dpi1)
570
571(** val eject__o__ertl_seq_to_joint_seq__o__inject :
572    AST.ident List.list -> __ Types.sig0 -> Joint.joint_seq Types.sig0 **)
573let eject__o__ertl_seq_to_joint_seq__o__inject x1 x2 =
574  ertl_seq_joint x1 (Types.pi1 x2)
575
576(** val eject__o__ertl_seq_to_joint_seq__o__seq_to_step__o__inject :
577    AST.ident List.list -> __ Types.sig0 -> Joint.joint_step Types.sig0 **)
578let eject__o__ertl_seq_to_joint_seq__o__seq_to_step__o__inject x1 x2 =
579  Joint.seq_to_step__o__inject
580    (Joint.gp_to_p__o__stmt_pars__o__uns_pars eRTL) x1
581    (ertl_seq_joint x1 (Types.pi1 x2))
582
583(** val eject__o__ertl_seq_to_joint_seq__o__seq_to_step :
584    AST.ident List.list -> __ Types.sig0 -> Joint.joint_step **)
585let eject__o__ertl_seq_to_joint_seq__o__seq_to_step x1 x2 =
586  Joint.Step_seq (ertl_seq_joint x1 (Types.pi1 x2))
587
588(** val ertl_seq_to_joint_seq__o__seq_to_step :
589    AST.ident List.list -> __ -> Joint.joint_step **)
590let ertl_seq_to_joint_seq__o__seq_to_step x0 x1 =
591  Joint.Step_seq (ertl_seq_joint x0 x1)
592
593(** val ertl_seq_to_joint_seq__o__seq_to_step__o__inject :
594    AST.ident List.list -> __ -> Joint.joint_step Types.sig0 **)
595let ertl_seq_to_joint_seq__o__seq_to_step__o__inject x0 x1 =
596  Joint.seq_to_step__o__inject
597    (Joint.gp_to_p__o__stmt_pars__o__uns_pars eRTL) x0 (ertl_seq_joint x0 x1)
598
599(** val ertl_seq_to_joint_seq__o__inject :
600    AST.ident List.list -> __ -> Joint.joint_seq Types.sig0 **)
601let ertl_seq_to_joint_seq__o__inject x0 x1 =
602  ertl_seq_joint x0 x1
603
604(** val dpi1__o__ertl_seq_to_joint_seq :
605    AST.ident List.list -> (__, 'a1) Types.dPair -> Joint.joint_seq **)
606let dpi1__o__ertl_seq_to_joint_seq x1 x2 =
607  ertl_seq_joint x1 x2.Types.dpi1
608
609(** val eject__o__ertl_seq_to_joint_seq :
610    AST.ident List.list -> __ Types.sig0 -> Joint.joint_seq **)
611let eject__o__ertl_seq_to_joint_seq x1 x2 =
612  ertl_seq_joint x1 (Types.pi1 x2)
613
Note: See TracBrowser for help on using the repository browser.