source: extracted/eRTL.mli @ 2743

Last change on this file since 2743 was 2743, checked in by sacerdot, 8 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: 10.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
111val move_dst_rect_Type4 :
112  (Registers.register -> 'a1) -> (I8051.register -> 'a1) -> move_dst -> 'a1
113
114val move_dst_rect_Type5 :
115  (Registers.register -> 'a1) -> (I8051.register -> 'a1) -> move_dst -> 'a1
116
117val move_dst_rect_Type3 :
118  (Registers.register -> 'a1) -> (I8051.register -> 'a1) -> move_dst -> 'a1
119
120val move_dst_rect_Type2 :
121  (Registers.register -> 'a1) -> (I8051.register -> 'a1) -> move_dst -> 'a1
122
123val move_dst_rect_Type1 :
124  (Registers.register -> 'a1) -> (I8051.register -> 'a1) -> move_dst -> 'a1
125
126val move_dst_rect_Type0 :
127  (Registers.register -> 'a1) -> (I8051.register -> 'a1) -> move_dst -> 'a1
128
129val move_dst_inv_rect_Type4 :
130  move_dst -> (Registers.register -> __ -> 'a1) -> (I8051.register -> __ ->
131  'a1) -> 'a1
132
133val move_dst_inv_rect_Type3 :
134  move_dst -> (Registers.register -> __ -> 'a1) -> (I8051.register -> __ ->
135  'a1) -> 'a1
136
137val move_dst_inv_rect_Type2 :
138  move_dst -> (Registers.register -> __ -> 'a1) -> (I8051.register -> __ ->
139  'a1) -> 'a1
140
141val move_dst_inv_rect_Type1 :
142  move_dst -> (Registers.register -> __ -> 'a1) -> (I8051.register -> __ ->
143  'a1) -> 'a1
144
145val move_dst_inv_rect_Type0 :
146  move_dst -> (Registers.register -> __ -> 'a1) -> (I8051.register -> __ ->
147  'a1) -> 'a1
148
149val move_dst_discr : move_dst -> move_dst -> __
150
151val move_dst_jmdiscr : move_dst -> move_dst -> __
152
153type move_src = move_dst Joint.argument
154
155val move_src_from_dst : move_dst -> move_src
156
157val dpi1__o__move_dst_to_src__o__inject :
158  (move_dst, 'a1) Types.dPair -> move_src Types.sig0
159
160val eject__o__move_dst_to_src__o__inject :
161  move_dst Types.sig0 -> move_src Types.sig0
162
163val move_dst_to_src__o__inject : move_dst -> move_src Types.sig0
164
165val dpi1__o__move_dst_to_src : (move_dst, 'a1) Types.dPair -> move_src
166
167val eject__o__move_dst_to_src : move_dst Types.sig0 -> move_src
168
169val psd_argument_move_src : Joint.psd_argument -> move_src
170
171val byte_to_psd_argument__o__psd_argument_to_move_src__o__inject :
172  BitVector.byte -> move_src Types.sig0
173
174val dpi1__o__byte_to_hdw_argument__o__psd_argument_to_move_src__o__inject :
175  (BitVector.byte, 'a1) Types.dPair -> move_src Types.sig0
176
177val dpi1__o__byte_to_psd_argument__o__psd_argument_to_move_src__o__inject :
178  (BitVector.byte, 'a1) Types.dPair -> move_src Types.sig0
179
180val dpi1__o__reg_to_psd_argument__o__psd_argument_to_move_src__o__inject :
181  (Registers.register, 'a1) Types.dPair -> move_src Types.sig0
182
183val eject__o__byte_to_hdw_argument__o__psd_argument_to_move_src__o__inject :
184  BitVector.byte Types.sig0 -> move_src Types.sig0
185
186val eject__o__byte_to_psd_argument__o__psd_argument_to_move_src__o__inject :
187  BitVector.byte Types.sig0 -> move_src Types.sig0
188
189val eject__o__reg_to_psd_argument__o__psd_argument_to_move_src__o__inject :
190  Registers.register Types.sig0 -> move_src Types.sig0
191
192val reg_to_psd_argument__o__psd_argument_to_move_src__o__inject :
193  Registers.register -> move_src Types.sig0
194
195val dpi1__o__psd_argument_to_move_src__o__inject :
196  (Joint.psd_argument, 'a1) Types.dPair -> move_src Types.sig0
197
198val eject__o__psd_argument_to_move_src__o__inject :
199  Joint.psd_argument Types.sig0 -> move_src Types.sig0
200
201val psd_argument_to_move_src__o__inject :
202  Joint.psd_argument -> move_src Types.sig0
203
204val byte_to_psd_argument__o__psd_argument_to_move_src :
205  BitVector.byte -> move_src
206
207val dpi1__o__byte_to_hdw_argument__o__psd_argument_to_move_src :
208  (BitVector.byte, 'a1) Types.dPair -> move_src
209
210val dpi1__o__byte_to_psd_argument__o__psd_argument_to_move_src :
211  (BitVector.byte, 'a1) Types.dPair -> move_src
212
213val dpi1__o__reg_to_psd_argument__o__psd_argument_to_move_src :
214  (Registers.register, 'a1) Types.dPair -> move_src
215
216val eject__o__byte_to_hdw_argument__o__psd_argument_to_move_src :
217  BitVector.byte Types.sig0 -> move_src
218
219val eject__o__byte_to_psd_argument__o__psd_argument_to_move_src :
220  BitVector.byte Types.sig0 -> move_src
221
222val eject__o__reg_to_psd_argument__o__psd_argument_to_move_src :
223  Registers.register Types.sig0 -> move_src
224
225val reg_to_psd_argument__o__psd_argument_to_move_src :
226  Registers.register -> move_src
227
228val dpi1__o__psd_argument_to_move_src :
229  (Joint.psd_argument, 'a1) Types.dPair -> move_src
230
231val eject__o__psd_argument_to_move_src :
232  Joint.psd_argument Types.sig0 -> move_src
233
234type ertl_seq =
235| Ertl_new_frame
236| Ertl_del_frame
237| Ertl_frame_size of Registers.register
238
239val ertl_seq_rect_Type4 :
240  'a1 -> 'a1 -> (Registers.register -> 'a1) -> ertl_seq -> 'a1
241
242val ertl_seq_rect_Type5 :
243  'a1 -> 'a1 -> (Registers.register -> 'a1) -> ertl_seq -> 'a1
244
245val ertl_seq_rect_Type3 :
246  'a1 -> 'a1 -> (Registers.register -> 'a1) -> ertl_seq -> 'a1
247
248val ertl_seq_rect_Type2 :
249  'a1 -> 'a1 -> (Registers.register -> 'a1) -> ertl_seq -> 'a1
250
251val ertl_seq_rect_Type1 :
252  'a1 -> 'a1 -> (Registers.register -> 'a1) -> ertl_seq -> 'a1
253
254val ertl_seq_rect_Type0 :
255  'a1 -> 'a1 -> (Registers.register -> 'a1) -> ertl_seq -> 'a1
256
257val ertl_seq_inv_rect_Type4 :
258  ertl_seq -> (__ -> 'a1) -> (__ -> 'a1) -> (Registers.register -> __ -> 'a1)
259  -> 'a1
260
261val ertl_seq_inv_rect_Type3 :
262  ertl_seq -> (__ -> 'a1) -> (__ -> 'a1) -> (Registers.register -> __ -> 'a1)
263  -> 'a1
264
265val ertl_seq_inv_rect_Type2 :
266  ertl_seq -> (__ -> 'a1) -> (__ -> 'a1) -> (Registers.register -> __ -> 'a1)
267  -> 'a1
268
269val ertl_seq_inv_rect_Type1 :
270  ertl_seq -> (__ -> 'a1) -> (__ -> 'a1) -> (Registers.register -> __ -> 'a1)
271  -> 'a1
272
273val ertl_seq_inv_rect_Type0 :
274  ertl_seq -> (__ -> 'a1) -> (__ -> 'a1) -> (Registers.register -> __ -> 'a1)
275  -> 'a1
276
277val ertl_seq_discr : ertl_seq -> ertl_seq -> __
278
279val ertl_seq_jmdiscr : ertl_seq -> ertl_seq -> __
280
281val eRTL_uns : Joint.unserialized_params
282
283val eRTL : Joint.graph_params
284
285type ertl_program = Joint.joint_program
286
287val dpi1__o__reg_to_ertl_snd_argument__o__inject :
288  (Registers.register, 'a1) Types.dPair -> Joint.psd_argument Types.sig0
289
290val dpi1__o__reg_to_ertl_snd_argument__o__psd_argument_to_move_src__o__inject :
291  (Registers.register, 'a1) Types.dPair -> move_src Types.sig0
292
293val dpi1__o__reg_to_ertl_snd_argument__o__psd_argument_to_move_src :
294  (Registers.register, 'a1) Types.dPair -> move_src
295
296val eject__o__reg_to_ertl_snd_argument__o__inject :
297  Registers.register Types.sig0 -> Joint.psd_argument Types.sig0
298
299val eject__o__reg_to_ertl_snd_argument__o__psd_argument_to_move_src__o__inject :
300  Registers.register Types.sig0 -> move_src Types.sig0
301
302val eject__o__reg_to_ertl_snd_argument__o__psd_argument_to_move_src :
303  Registers.register Types.sig0 -> move_src
304
305val reg_to_ertl_snd_argument__o__psd_argument_to_move_src :
306  Registers.register -> move_src
307
308val reg_to_ertl_snd_argument__o__psd_argument_to_move_src__o__inject :
309  Registers.register -> move_src Types.sig0
310
311val reg_to_ertl_snd_argument__o__inject :
312  Registers.register -> Joint.psd_argument Types.sig0
313
314val dpi1__o__reg_to_ertl_snd_argument :
315  (Registers.register, 'a1) Types.dPair -> Joint.psd_argument
316
317val eject__o__reg_to_ertl_snd_argument :
318  Registers.register Types.sig0 -> Joint.psd_argument
319
320val dpi1__o__byte_to_ertl_snd_argument__o__inject :
321  (BitVector.byte, 'a1) Types.dPair -> Joint.psd_argument Types.sig0
322
323val dpi1__o__byte_to_ertl_snd_argument__o__psd_argument_to_move_src__o__inject :
324  (BitVector.byte, 'a1) Types.dPair -> move_src Types.sig0
325
326val dpi1__o__byte_to_ertl_snd_argument__o__psd_argument_to_move_src :
327  (BitVector.byte, 'a1) Types.dPair -> move_src
328
329val eject__o__byte_to_ertl_snd_argument__o__inject :
330  BitVector.byte Types.sig0 -> Joint.psd_argument Types.sig0
331
332val eject__o__byte_to_ertl_snd_argument__o__psd_argument_to_move_src__o__inject :
333  BitVector.byte Types.sig0 -> move_src Types.sig0
334
335val eject__o__byte_to_ertl_snd_argument__o__psd_argument_to_move_src :
336  BitVector.byte Types.sig0 -> move_src
337
338val byte_to_ertl_snd_argument__o__psd_argument_to_move_src :
339  BitVector.byte -> move_src
340
341val byte_to_ertl_snd_argument__o__psd_argument_to_move_src__o__inject :
342  BitVector.byte -> move_src Types.sig0
343
344val byte_to_ertl_snd_argument__o__inject :
345  BitVector.byte -> Joint.psd_argument Types.sig0
346
347val dpi1__o__byte_to_ertl_snd_argument :
348  (BitVector.byte, 'a1) Types.dPair -> Joint.psd_argument
349
350val eject__o__byte_to_ertl_snd_argument :
351  BitVector.byte Types.sig0 -> Joint.psd_argument
352
353val ertl_seq_joint : AST.ident List.list -> __ -> Joint.joint_seq
354
355val dpi1__o__ertl_seq_to_joint_seq__o__inject :
356  AST.ident List.list -> (__, 'a1) Types.dPair -> Joint.joint_seq Types.sig0
357
358val dpi1__o__ertl_seq_to_joint_seq__o__seq_to_step__o__inject :
359  AST.ident List.list -> (__, 'a1) Types.dPair -> Joint.joint_step Types.sig0
360
361val dpi1__o__ertl_seq_to_joint_seq__o__seq_to_step :
362  AST.ident List.list -> (__, 'a1) Types.dPair -> Joint.joint_step
363
364val eject__o__ertl_seq_to_joint_seq__o__inject :
365  AST.ident List.list -> __ Types.sig0 -> Joint.joint_seq Types.sig0
366
367val eject__o__ertl_seq_to_joint_seq__o__seq_to_step__o__inject :
368  AST.ident List.list -> __ Types.sig0 -> Joint.joint_step Types.sig0
369
370val eject__o__ertl_seq_to_joint_seq__o__seq_to_step :
371  AST.ident List.list -> __ Types.sig0 -> Joint.joint_step
372
373val ertl_seq_to_joint_seq__o__seq_to_step :
374  AST.ident List.list -> __ -> Joint.joint_step
375
376val ertl_seq_to_joint_seq__o__seq_to_step__o__inject :
377  AST.ident List.list -> __ -> Joint.joint_step Types.sig0
378
379val ertl_seq_to_joint_seq__o__inject :
380  AST.ident List.list -> __ -> Joint.joint_seq Types.sig0
381
382val dpi1__o__ertl_seq_to_joint_seq :
383  AST.ident List.list -> (__, 'a1) Types.dPair -> Joint.joint_seq
384
385val eject__o__ertl_seq_to_joint_seq :
386  AST.ident List.list -> __ Types.sig0 -> Joint.joint_seq
387
Note: See TracBrowser for help on using the repository browser.