source: driver/extracted/lINToASM.mli @ 3106

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

New extraction.
File size: 10.1 KB
Line 
1open Preamble
2
3open Deqsets
4
5open Setoids
6
7open Monad
8
9open Option
10
11open Extranat
12
13open Vector
14
15open Div_and_mod
16
17open Jmeq
18
19open Russell
20
21open List
22
23open Util
24
25open FoldStuff
26
27open Bool
28
29open Relations
30
31open Nat
32
33open BitVector
34
35open Hints_declaration
36
37open Core_notation
38
39open Pts
40
41open Logic
42
43open Types
44
45open BitVectorTrie
46
47open BitVectorTrieSet
48
49open State
50
51open String
52
53open Exp
54
55open Arithmetic
56
57open Integers
58
59open AST
60
61open LabelledObjects
62
63open Proper
64
65open PositiveMap
66
67open ErrorMessages
68
69open PreIdentifiers
70
71open Errors
72
73open Extralib
74
75open Lists
76
77open Positive
78
79open Identifiers
80
81open CostLabel
82
83open ASM
84
85open Extra_bool
86
87open Coqlib
88
89open Values
90
91open FrontEndVal
92
93open GenMem
94
95open FrontEndMem
96
97open Globalenvs
98
99open Sets
100
101open Listb
102
103open Graphs
104
105open I8051
106
107open Order
108
109open Registers
110
111open Hide
112
113open Division
114
115open Z
116
117open BitVectorZ
118
119open Pointers
120
121open ByteValues
122
123open BackEndOps
124
125open Joint
126
127open Joint_LTL_LIN
128
129open LIN
130
131type aSM_universe = { id_univ : Identifiers.universe;
132                      current_funct : AST.ident;
133                      ident_map : ASM.identifier Identifiers.identifier_map;
134                      label_map : ASM.identifier Identifiers.identifier_map
135                                  Identifiers.identifier_map;
136                      fresh_cost_label : Positive.pos }
137
138val aSM_universe_rect_Type4 :
139  (Identifiers.universe -> AST.ident -> ASM.identifier
140  Identifiers.identifier_map -> ASM.identifier Identifiers.identifier_map
141  Identifiers.identifier_map -> Positive.pos -> 'a1) -> aSM_universe -> 'a1
142
143val aSM_universe_rect_Type5 :
144  (Identifiers.universe -> AST.ident -> ASM.identifier
145  Identifiers.identifier_map -> ASM.identifier Identifiers.identifier_map
146  Identifiers.identifier_map -> Positive.pos -> 'a1) -> aSM_universe -> 'a1
147
148val aSM_universe_rect_Type3 :
149  (Identifiers.universe -> AST.ident -> ASM.identifier
150  Identifiers.identifier_map -> ASM.identifier Identifiers.identifier_map
151  Identifiers.identifier_map -> Positive.pos -> 'a1) -> aSM_universe -> 'a1
152
153val aSM_universe_rect_Type2 :
154  (Identifiers.universe -> AST.ident -> ASM.identifier
155  Identifiers.identifier_map -> ASM.identifier Identifiers.identifier_map
156  Identifiers.identifier_map -> Positive.pos -> 'a1) -> aSM_universe -> 'a1
157
158val aSM_universe_rect_Type1 :
159  (Identifiers.universe -> AST.ident -> ASM.identifier
160  Identifiers.identifier_map -> ASM.identifier Identifiers.identifier_map
161  Identifiers.identifier_map -> Positive.pos -> 'a1) -> aSM_universe -> 'a1
162
163val aSM_universe_rect_Type0 :
164  (Identifiers.universe -> AST.ident -> ASM.identifier
165  Identifiers.identifier_map -> ASM.identifier Identifiers.identifier_map
166  Identifiers.identifier_map -> Positive.pos -> 'a1) -> aSM_universe -> 'a1
167
168val id_univ : aSM_universe -> Identifiers.universe
169
170val current_funct : aSM_universe -> AST.ident
171
172val ident_map : aSM_universe -> ASM.identifier Identifiers.identifier_map
173
174val label_map :
175  aSM_universe -> ASM.identifier Identifiers.identifier_map
176  Identifiers.identifier_map
177
178val fresh_cost_label : aSM_universe -> Positive.pos
179
180val aSM_universe_inv_rect_Type4 :
181  aSM_universe -> (Identifiers.universe -> AST.ident -> ASM.identifier
182  Identifiers.identifier_map -> ASM.identifier Identifiers.identifier_map
183  Identifiers.identifier_map -> Positive.pos -> __ -> 'a1) -> 'a1
184
185val aSM_universe_inv_rect_Type3 :
186  aSM_universe -> (Identifiers.universe -> AST.ident -> ASM.identifier
187  Identifiers.identifier_map -> ASM.identifier Identifiers.identifier_map
188  Identifiers.identifier_map -> Positive.pos -> __ -> 'a1) -> 'a1
189
190val aSM_universe_inv_rect_Type2 :
191  aSM_universe -> (Identifiers.universe -> AST.ident -> ASM.identifier
192  Identifiers.identifier_map -> ASM.identifier Identifiers.identifier_map
193  Identifiers.identifier_map -> Positive.pos -> __ -> 'a1) -> 'a1
194
195val aSM_universe_inv_rect_Type1 :
196  aSM_universe -> (Identifiers.universe -> AST.ident -> ASM.identifier
197  Identifiers.identifier_map -> ASM.identifier Identifiers.identifier_map
198  Identifiers.identifier_map -> Positive.pos -> __ -> 'a1) -> 'a1
199
200val aSM_universe_inv_rect_Type0 :
201  aSM_universe -> (Identifiers.universe -> AST.ident -> ASM.identifier
202  Identifiers.identifier_map -> ASM.identifier Identifiers.identifier_map
203  Identifiers.identifier_map -> Positive.pos -> __ -> 'a1) -> 'a1
204
205val aSM_universe_discr : aSM_universe -> aSM_universe -> __
206
207val aSM_universe_jmdiscr : aSM_universe -> aSM_universe -> __
208
209val report_cost : CostLabel.costlabel -> Types.unit0 Monad.smax_def__o__monad
210
211val identifier_of_label :
212  Graphs.label -> ASM.identifier Monad.smax_def__o__monad
213
214val identifier_of_ident :
215  AST.ident -> ASM.identifier Monad.smax_def__o__monad
216
217val new_ASM_universe : Joint.joint_program -> aSM_universe
218
219val start_funct_translation :
220  AST.ident List.list -> AST.ident List.list -> (AST.ident,
221  Joint.joint_function) Types.prod -> Types.unit0 Monad.smax_def__o__monad
222
223val aSM_fresh : ASM.identifier Monad.smax_def__o__monad
224
225val register_address : I8051.register -> ASM.subaddressing_mode
226
227val vector_cast :
228  Nat.nat -> Nat.nat -> 'a1 -> 'a1 Vector.vector -> 'a1 Vector.vector
229
230val arg_address : Joint.hdw_argument -> ASM.subaddressing_mode
231
232type lin_statement = Joint.joint_statement LabelledObjects.labelled_obj
233
234val data_of_int : BitVector.byte -> ASM.addressing_mode
235
236val data16_of_int : Nat.nat -> ASM.addressing_mode
237
238val accumulator_address : ASM.addressing_mode
239
240val asm_other_bit : ASM.addressing_mode
241
242val one_word : BitVector.word
243
244val translate_statements :
245  AST.ident List.list -> Joint.joint_statement -> ASM.pseudo_instruction
246  Monad.smax_def__o__monad
247
248val build_translated_statement : AST.ident List.list -> lin_statement -> __
249
250val translate_code : AST.ident List.list -> lin_statement List.list -> __
251
252val translate_fun_def :
253  AST.ident List.list -> AST.ident List.list -> (AST.ident,
254  Joint.joint_function) Types.prod -> __
255
256type init_mutable = { virtual_dptr : (ASM.identifier, Z.z) Types.prod;
257                      actual_dptr : (ASM.identifier, Z.z) Types.prod;
258                      built_code : ASM.labelled_instruction List.list
259                                   List.list;
260                      built_preamble : (ASM.identifier, BitVector.word)
261                                       Types.prod List.list }
262
263val init_mutable_rect_Type4 :
264  ((ASM.identifier, Z.z) Types.prod -> (ASM.identifier, Z.z) Types.prod ->
265  ASM.labelled_instruction List.list List.list -> (ASM.identifier,
266  BitVector.word) Types.prod List.list -> 'a1) -> init_mutable -> 'a1
267
268val init_mutable_rect_Type5 :
269  ((ASM.identifier, Z.z) Types.prod -> (ASM.identifier, Z.z) Types.prod ->
270  ASM.labelled_instruction List.list List.list -> (ASM.identifier,
271  BitVector.word) Types.prod List.list -> 'a1) -> init_mutable -> 'a1
272
273val init_mutable_rect_Type3 :
274  ((ASM.identifier, Z.z) Types.prod -> (ASM.identifier, Z.z) Types.prod ->
275  ASM.labelled_instruction List.list List.list -> (ASM.identifier,
276  BitVector.word) Types.prod List.list -> 'a1) -> init_mutable -> 'a1
277
278val init_mutable_rect_Type2 :
279  ((ASM.identifier, Z.z) Types.prod -> (ASM.identifier, Z.z) Types.prod ->
280  ASM.labelled_instruction List.list List.list -> (ASM.identifier,
281  BitVector.word) Types.prod List.list -> 'a1) -> init_mutable -> 'a1
282
283val init_mutable_rect_Type1 :
284  ((ASM.identifier, Z.z) Types.prod -> (ASM.identifier, Z.z) Types.prod ->
285  ASM.labelled_instruction List.list List.list -> (ASM.identifier,
286  BitVector.word) Types.prod List.list -> 'a1) -> init_mutable -> 'a1
287
288val init_mutable_rect_Type0 :
289  ((ASM.identifier, Z.z) Types.prod -> (ASM.identifier, Z.z) Types.prod ->
290  ASM.labelled_instruction List.list List.list -> (ASM.identifier,
291  BitVector.word) Types.prod List.list -> 'a1) -> init_mutable -> 'a1
292
293val virtual_dptr : init_mutable -> (ASM.identifier, Z.z) Types.prod
294
295val actual_dptr : init_mutable -> (ASM.identifier, Z.z) Types.prod
296
297val built_code : init_mutable -> ASM.labelled_instruction List.list List.list
298
299val built_preamble :
300  init_mutable -> (ASM.identifier, BitVector.word) Types.prod List.list
301
302val init_mutable_inv_rect_Type4 :
303  init_mutable -> ((ASM.identifier, Z.z) Types.prod -> (ASM.identifier, Z.z)
304  Types.prod -> ASM.labelled_instruction List.list List.list ->
305  (ASM.identifier, BitVector.word) Types.prod List.list -> __ -> 'a1) -> 'a1
306
307val init_mutable_inv_rect_Type3 :
308  init_mutable -> ((ASM.identifier, Z.z) Types.prod -> (ASM.identifier, Z.z)
309  Types.prod -> ASM.labelled_instruction List.list List.list ->
310  (ASM.identifier, BitVector.word) Types.prod List.list -> __ -> 'a1) -> 'a1
311
312val init_mutable_inv_rect_Type2 :
313  init_mutable -> ((ASM.identifier, Z.z) Types.prod -> (ASM.identifier, Z.z)
314  Types.prod -> ASM.labelled_instruction List.list List.list ->
315  (ASM.identifier, BitVector.word) Types.prod List.list -> __ -> 'a1) -> 'a1
316
317val init_mutable_inv_rect_Type1 :
318  init_mutable -> ((ASM.identifier, Z.z) Types.prod -> (ASM.identifier, Z.z)
319  Types.prod -> ASM.labelled_instruction List.list List.list ->
320  (ASM.identifier, BitVector.word) Types.prod List.list -> __ -> 'a1) -> 'a1
321
322val init_mutable_inv_rect_Type0 :
323  init_mutable -> ((ASM.identifier, Z.z) Types.prod -> (ASM.identifier, Z.z)
324  Types.prod -> ASM.labelled_instruction List.list List.list ->
325  (ASM.identifier, BitVector.word) Types.prod List.list -> __ -> 'a1) -> 'a1
326
327val init_mutable_discr : init_mutable -> init_mutable -> __
328
329val init_mutable_jmdiscr : init_mutable -> init_mutable -> __
330
331val store_byte_or_Identifier :
332  (BitVector.byte, (ASM.word_side, ASM.identifier) Types.prod) Types.sum ->
333  init_mutable -> init_mutable
334
335val do_store_init_data :
336  init_mutable Monad.smax_def__o__monad -> AST.init_data -> init_mutable
337  Monad.smax_def__o__monad
338
339val do_store_global :
340  init_mutable Monad.smax_def__o__monad -> ((AST.ident, AST.region)
341  Types.prod, AST.init_data List.list) Types.prod -> init_mutable
342  Monad.smax_def__o__monad
343
344val reversed_flatten_aux :
345  'a1 List.list -> 'a1 List.list List.list -> 'a1 List.list
346
347val translate_premain :
348  LIN.lin_program -> ASM.identifier -> (ASM.labelled_instruction List.list,
349  (ASM.identifier, BitVector.word) Types.prod List.list) Types.prod
350  Monad.smax_def__o__monad
351
352val get_symboltable :
353  (ASM.identifier, AST.ident) Types.prod List.list Monad.smax_def__o__monad
354
355val lin_to_asm : LIN.lin_program -> ASM.pseudo_assembly_program Types.option
356
Note: See TracBrowser for help on using the repository browser.