source: extracted/eRTL.ml @ 2717

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

Extracted code for the whole compiler.
The space cost model is not there yet.

I have fixed by hand the few extraction problems
(i.e. composed coercions not extracted and type
definitions with wrong syntax).

I have also changed all axioms to be implemented
so that they do not fail at initialization time.

File size: 8.1 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_17821 -> h_PSD x_17821
115| HDW x_17822 -> h_HDW x_17822
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_17826 -> h_PSD x_17826
121| HDW x_17827 -> h_HDW x_17827
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_17831 -> h_PSD x_17831
127| HDW x_17832 -> h_HDW x_17832
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_17836 -> h_PSD x_17836
133| HDW x_17837 -> h_HDW x_17837
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_17841 -> h_PSD x_17841
139| HDW x_17842 -> h_HDW x_17842
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_17846 -> h_PSD x_17846
145| HDW x_17847 -> h_HDW x_17847
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 psd_argument_move_src : Joint.psd_argument -> move_src **)
198let psd_argument_move_src = function
199| Joint.Reg r -> Joint.Reg (PSD r)
200| Joint.Imm b -> Joint.Imm b
201
202type ertl_seq =
203| Ertl_new_frame
204| Ertl_del_frame
205| Ertl_frame_size of Registers.register
206
207(** val ertl_seq_rect_Type4 :
208    'a1 -> 'a1 -> (Registers.register -> 'a1) -> ertl_seq -> 'a1 **)
209let rec ertl_seq_rect_Type4 h_ertl_new_frame h_ertl_del_frame h_ertl_frame_size = function
210| Ertl_new_frame -> h_ertl_new_frame
211| Ertl_del_frame -> h_ertl_del_frame
212| Ertl_frame_size x_17886 -> h_ertl_frame_size x_17886
213
214(** val ertl_seq_rect_Type5 :
215    'a1 -> 'a1 -> (Registers.register -> 'a1) -> ertl_seq -> 'a1 **)
216let rec ertl_seq_rect_Type5 h_ertl_new_frame h_ertl_del_frame h_ertl_frame_size = function
217| Ertl_new_frame -> h_ertl_new_frame
218| Ertl_del_frame -> h_ertl_del_frame
219| Ertl_frame_size x_17891 -> h_ertl_frame_size x_17891
220
221(** val ertl_seq_rect_Type3 :
222    'a1 -> 'a1 -> (Registers.register -> 'a1) -> ertl_seq -> 'a1 **)
223let rec ertl_seq_rect_Type3 h_ertl_new_frame h_ertl_del_frame h_ertl_frame_size = function
224| Ertl_new_frame -> h_ertl_new_frame
225| Ertl_del_frame -> h_ertl_del_frame
226| Ertl_frame_size x_17896 -> h_ertl_frame_size x_17896
227
228(** val ertl_seq_rect_Type2 :
229    'a1 -> 'a1 -> (Registers.register -> 'a1) -> ertl_seq -> 'a1 **)
230let rec ertl_seq_rect_Type2 h_ertl_new_frame h_ertl_del_frame h_ertl_frame_size = function
231| Ertl_new_frame -> h_ertl_new_frame
232| Ertl_del_frame -> h_ertl_del_frame
233| Ertl_frame_size x_17901 -> h_ertl_frame_size x_17901
234
235(** val ertl_seq_rect_Type1 :
236    'a1 -> 'a1 -> (Registers.register -> 'a1) -> ertl_seq -> 'a1 **)
237let rec ertl_seq_rect_Type1 h_ertl_new_frame h_ertl_del_frame h_ertl_frame_size = function
238| Ertl_new_frame -> h_ertl_new_frame
239| Ertl_del_frame -> h_ertl_del_frame
240| Ertl_frame_size x_17906 -> h_ertl_frame_size x_17906
241
242(** val ertl_seq_rect_Type0 :
243    'a1 -> 'a1 -> (Registers.register -> 'a1) -> ertl_seq -> 'a1 **)
244let rec ertl_seq_rect_Type0 h_ertl_new_frame h_ertl_del_frame h_ertl_frame_size = function
245| Ertl_new_frame -> h_ertl_new_frame
246| Ertl_del_frame -> h_ertl_del_frame
247| Ertl_frame_size x_17911 -> h_ertl_frame_size x_17911
248
249(** val ertl_seq_inv_rect_Type4 :
250    ertl_seq -> (__ -> 'a1) -> (__ -> 'a1) -> (Registers.register -> __ ->
251    'a1) -> 'a1 **)
252let ertl_seq_inv_rect_Type4 hterm h1 h2 h3 =
253  let hcut = ertl_seq_rect_Type4 h1 h2 h3 hterm in hcut __
254
255(** val ertl_seq_inv_rect_Type3 :
256    ertl_seq -> (__ -> 'a1) -> (__ -> 'a1) -> (Registers.register -> __ ->
257    'a1) -> 'a1 **)
258let ertl_seq_inv_rect_Type3 hterm h1 h2 h3 =
259  let hcut = ertl_seq_rect_Type3 h1 h2 h3 hterm in hcut __
260
261(** val ertl_seq_inv_rect_Type2 :
262    ertl_seq -> (__ -> 'a1) -> (__ -> 'a1) -> (Registers.register -> __ ->
263    'a1) -> 'a1 **)
264let ertl_seq_inv_rect_Type2 hterm h1 h2 h3 =
265  let hcut = ertl_seq_rect_Type2 h1 h2 h3 hterm in hcut __
266
267(** val ertl_seq_inv_rect_Type1 :
268    ertl_seq -> (__ -> 'a1) -> (__ -> 'a1) -> (Registers.register -> __ ->
269    'a1) -> 'a1 **)
270let ertl_seq_inv_rect_Type1 hterm h1 h2 h3 =
271  let hcut = ertl_seq_rect_Type1 h1 h2 h3 hterm in hcut __
272
273(** val ertl_seq_inv_rect_Type0 :
274    ertl_seq -> (__ -> 'a1) -> (__ -> 'a1) -> (Registers.register -> __ ->
275    'a1) -> 'a1 **)
276let ertl_seq_inv_rect_Type0 hterm h1 h2 h3 =
277  let hcut = ertl_seq_rect_Type0 h1 h2 h3 hterm in hcut __
278
279(** val ertl_seq_discr : ertl_seq -> ertl_seq -> __ **)
280let ertl_seq_discr x y =
281  Logic.eq_rect_Type2 x
282    (match x with
283     | Ertl_new_frame -> Obj.magic (fun _ dH -> dH)
284     | Ertl_del_frame -> Obj.magic (fun _ dH -> dH)
285     | Ertl_frame_size a0 -> Obj.magic (fun _ dH -> dH __)) y
286
287(** val ertl_seq_jmdiscr : ertl_seq -> ertl_seq -> __ **)
288let ertl_seq_jmdiscr x y =
289  Logic.eq_rect_Type2 x
290    (match x with
291     | Ertl_new_frame -> Obj.magic (fun _ dH -> dH)
292     | Ertl_del_frame -> Obj.magic (fun _ dH -> dH)
293     | Ertl_frame_size a0 -> Obj.magic (fun _ dH -> dH __)) y
294
295(** val eRTL_uns : Joint.unserialized_params **)
296let eRTL_uns =
297  { Joint.ext_seq_labels = (fun x -> List.Nil); Joint.has_tailcalls =
298    Bool.False }
299
300(** val eRTL : Joint.graph_params **)
301let eRTL =
302  eRTL_uns
303
304type ertl_program = Joint.joint_program
305
306(** val ertl_seq_joint : AST.ident List.list -> __ -> Joint.joint_seq **)
307let ertl_seq_joint =
308  Obj.magic (fun _ x -> Joint.Extension_seq x)
309
310let byte_to_ertl_snd_argument__o__psd_argument_to_move_src _ = assert false
Note: See TracBrowser for help on using the repository browser.