35 open Hints_declaration
131 type 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 }
138 val 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
143 val 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
148 val 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
153 val 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
158 val 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
163 val 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
168 val id_univ : aSM_universe -> Identifiers.universe
170 val current_funct : aSM_universe -> AST.ident
172 val ident_map : aSM_universe -> ASM.identifier Identifiers.identifier_map
175 aSM_universe -> ASM.identifier Identifiers.identifier_map
176 Identifiers.identifier_map
178 val fresh_cost_label : aSM_universe -> Positive.pos
180 val 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
185 val 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
190 val 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
195 val 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
200 val 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
205 val aSM_universe_discr : aSM_universe -> aSM_universe -> __
207 val aSM_universe_jmdiscr : aSM_universe -> aSM_universe -> __
209 val report_cost : CostLabel.costlabel -> Types.unit0 Monad.smax_def__o__monad
211 val identifier_of_label :
212 Graphs.label -> ASM.identifier Monad.smax_def__o__monad
214 val identifier_of_ident :
215 AST.ident -> ASM.identifier Monad.smax_def__o__monad
217 val new_ASM_universe : Joint.joint_program -> aSM_universe
219 val 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
223 val aSM_fresh : ASM.identifier Monad.smax_def__o__monad
225 val register_address : I8051.register -> ASM.subaddressing_mode
228 Nat.nat -> Nat.nat -> 'a1 -> 'a1 Vector.vector -> 'a1 Vector.vector
230 val arg_address : Joint.hdw_argument -> ASM.subaddressing_mode
232 type lin_statement = Joint.joint_statement LabelledObjects.labelled_obj
234 val data_of_int : BitVector.byte -> ASM.addressing_mode
236 val data16_of_int : Nat.nat -> ASM.addressing_mode
238 val accumulator_address : ASM.addressing_mode
240 val asm_other_bit : ASM.addressing_mode
242 val one_word : BitVector.word
244 val translate_statements :
245 AST.ident List.list -> Joint.joint_statement -> ASM.pseudo_instruction
246 Monad.smax_def__o__monad
248 val build_translated_statement : AST.ident List.list -> lin_statement -> __
250 val translate_code : AST.ident List.list -> lin_statement List.list -> __
252 val translate_fun_def :
253 AST.ident List.list -> AST.ident List.list -> (AST.ident,
254 Joint.joint_function) Types.prod -> __
256 type 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
260 built_preamble : (ASM.identifier, BitVector.word)
261 Types.prod List.list }
263 val 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
268 val 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
273 val 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
278 val 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
283 val 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
288 val 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
293 val virtual_dptr : init_mutable -> (ASM.identifier, Z.z) Types.prod
295 val actual_dptr : init_mutable -> (ASM.identifier, Z.z) Types.prod
297 val built_code : init_mutable -> ASM.labelled_instruction List.list List.list
300 init_mutable -> (ASM.identifier, BitVector.word) Types.prod List.list
302 val 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
307 val 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
312 val 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
317 val 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
322 val 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
327 val init_mutable_discr : init_mutable -> init_mutable -> __
329 val init_mutable_jmdiscr : init_mutable -> init_mutable -> __
331 val store_byte_or_Identifier :
332 (BitVector.byte, (ASM.word_side, ASM.identifier) Types.prod) Types.sum ->
333 init_mutable -> init_mutable
335 val do_store_init_data :
336 init_mutable Monad.smax_def__o__monad -> AST.init_data -> init_mutable
337 Monad.smax_def__o__monad
339 val 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
344 val reversed_flatten_aux :
345 'a1 List.list -> 'a1 List.list List.list -> 'a1 List.list
347 val 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
352 val get_symboltable :
353 (ASM.identifier, AST.ident) Types.prod List.list Monad.smax_def__o__monad
355 val lin_to_asm : LIN.lin_program -> ASM.pseudo_assembly_program Types.option