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 **)
142 let rec aSM_universe_rect_Type4 h_mk_ASM_universe x_588 =
143 let { id_univ = id_univ0; current_funct = current_funct0; ident_map =
144 ident_map0; label_map = label_map0; fresh_cost_label =
145 fresh_cost_label0 } = x_588
147 h_mk_ASM_universe id_univ0 current_funct0 ident_map0 label_map0
150 (** val aSM_universe_rect_Type5 :
151 (Identifiers.universe -> AST.ident -> ASM.identifier
152 Identifiers.identifier_map -> ASM.identifier Identifiers.identifier_map
153 Identifiers.identifier_map -> Positive.pos -> 'a1) -> aSM_universe -> 'a1 **)
154 let rec aSM_universe_rect_Type5 h_mk_ASM_universe x_590 =
155 let { id_univ = id_univ0; current_funct = current_funct0; ident_map =
156 ident_map0; label_map = label_map0; fresh_cost_label =
157 fresh_cost_label0 } = x_590
159 h_mk_ASM_universe id_univ0 current_funct0 ident_map0 label_map0
162 (** val aSM_universe_rect_Type3 :
163 (Identifiers.universe -> AST.ident -> ASM.identifier
164 Identifiers.identifier_map -> ASM.identifier Identifiers.identifier_map
165 Identifiers.identifier_map -> Positive.pos -> 'a1) -> aSM_universe -> 'a1 **)
166 let rec aSM_universe_rect_Type3 h_mk_ASM_universe x_592 =
167 let { id_univ = id_univ0; current_funct = current_funct0; ident_map =
168 ident_map0; label_map = label_map0; fresh_cost_label =
169 fresh_cost_label0 } = x_592
171 h_mk_ASM_universe id_univ0 current_funct0 ident_map0 label_map0
174 (** val aSM_universe_rect_Type2 :
175 (Identifiers.universe -> AST.ident -> ASM.identifier
176 Identifiers.identifier_map -> ASM.identifier Identifiers.identifier_map
177 Identifiers.identifier_map -> Positive.pos -> 'a1) -> aSM_universe -> 'a1 **)
178 let rec aSM_universe_rect_Type2 h_mk_ASM_universe x_594 =
179 let { id_univ = id_univ0; current_funct = current_funct0; ident_map =
180 ident_map0; label_map = label_map0; fresh_cost_label =
181 fresh_cost_label0 } = x_594
183 h_mk_ASM_universe id_univ0 current_funct0 ident_map0 label_map0
186 (** val aSM_universe_rect_Type1 :
187 (Identifiers.universe -> AST.ident -> ASM.identifier
188 Identifiers.identifier_map -> ASM.identifier Identifiers.identifier_map
189 Identifiers.identifier_map -> Positive.pos -> 'a1) -> aSM_universe -> 'a1 **)
190 let rec aSM_universe_rect_Type1 h_mk_ASM_universe x_596 =
191 let { id_univ = id_univ0; current_funct = current_funct0; ident_map =
192 ident_map0; label_map = label_map0; fresh_cost_label =
193 fresh_cost_label0 } = x_596
195 h_mk_ASM_universe id_univ0 current_funct0 ident_map0 label_map0
198 (** val aSM_universe_rect_Type0 :
199 (Identifiers.universe -> AST.ident -> ASM.identifier
200 Identifiers.identifier_map -> ASM.identifier Identifiers.identifier_map
201 Identifiers.identifier_map -> Positive.pos -> 'a1) -> aSM_universe -> 'a1 **)
202 let rec aSM_universe_rect_Type0 h_mk_ASM_universe x_598 =
203 let { id_univ = id_univ0; current_funct = current_funct0; ident_map =
204 ident_map0; label_map = label_map0; fresh_cost_label =
205 fresh_cost_label0 } = x_598
207 h_mk_ASM_universe id_univ0 current_funct0 ident_map0 label_map0
210 (** val id_univ : aSM_universe -> Identifiers.universe **)
211 let rec id_univ xxx =
214 (** val current_funct : aSM_universe -> AST.ident **)
215 let rec current_funct xxx =
219 aSM_universe -> ASM.identifier Identifiers.identifier_map **)
220 let rec ident_map xxx =
224 aSM_universe -> ASM.identifier Identifiers.identifier_map
225 Identifiers.identifier_map **)
226 let rec label_map xxx =
229 (** val fresh_cost_label : aSM_universe -> Positive.pos **)
230 let rec fresh_cost_label xxx =
233 (** val aSM_universe_inv_rect_Type4 :
234 aSM_universe -> (Identifiers.universe -> AST.ident -> ASM.identifier
235 Identifiers.identifier_map -> ASM.identifier Identifiers.identifier_map
236 Identifiers.identifier_map -> Positive.pos -> __ -> 'a1) -> 'a1 **)
237 let aSM_universe_inv_rect_Type4 hterm h1 =
238 let hcut = aSM_universe_rect_Type4 h1 hterm in hcut __
240 (** val aSM_universe_inv_rect_Type3 :
241 aSM_universe -> (Identifiers.universe -> AST.ident -> ASM.identifier
242 Identifiers.identifier_map -> ASM.identifier Identifiers.identifier_map
243 Identifiers.identifier_map -> Positive.pos -> __ -> 'a1) -> 'a1 **)
244 let aSM_universe_inv_rect_Type3 hterm h1 =
245 let hcut = aSM_universe_rect_Type3 h1 hterm in hcut __
247 (** val aSM_universe_inv_rect_Type2 :
248 aSM_universe -> (Identifiers.universe -> AST.ident -> ASM.identifier
249 Identifiers.identifier_map -> ASM.identifier Identifiers.identifier_map
250 Identifiers.identifier_map -> Positive.pos -> __ -> 'a1) -> 'a1 **)
251 let aSM_universe_inv_rect_Type2 hterm h1 =
252 let hcut = aSM_universe_rect_Type2 h1 hterm in hcut __
254 (** val aSM_universe_inv_rect_Type1 :
255 aSM_universe -> (Identifiers.universe -> AST.ident -> ASM.identifier
256 Identifiers.identifier_map -> ASM.identifier Identifiers.identifier_map
257 Identifiers.identifier_map -> Positive.pos -> __ -> 'a1) -> 'a1 **)
258 let aSM_universe_inv_rect_Type1 hterm h1 =
259 let hcut = aSM_universe_rect_Type1 h1 hterm in hcut __
261 (** val aSM_universe_inv_rect_Type0 :
262 aSM_universe -> (Identifiers.universe -> AST.ident -> ASM.identifier
263 Identifiers.identifier_map -> ASM.identifier Identifiers.identifier_map
264 Identifiers.identifier_map -> Positive.pos -> __ -> 'a1) -> 'a1 **)
265 let aSM_universe_inv_rect_Type0 hterm h1 =
266 let hcut = aSM_universe_rect_Type0 h1 hterm in hcut __
268 (** val aSM_universe_discr : aSM_universe -> aSM_universe -> __ **)
269 let aSM_universe_discr x y =
270 Logic.eq_rect_Type2 x
271 (let { id_univ = a0; current_funct = a1; ident_map = a2; label_map = a3;
272 fresh_cost_label = a4 } = x
274 Obj.magic (fun _ dH -> dH __ __ __ __ __)) y
276 (** val aSM_universe_jmdiscr : aSM_universe -> aSM_universe -> __ **)
277 let aSM_universe_jmdiscr x y =
278 Logic.eq_rect_Type2 x
279 (let { id_univ = a0; current_funct = a1; ident_map = a2; label_map = a3;
280 fresh_cost_label = a4 } = x
282 Obj.magic (fun _ dH -> dH __ __ __ __ __)) y
284 (** val report_cost :
285 CostLabel.costlabel -> Types.unit0 Monad.smax_def__o__monad **)
288 let clw = Identifiers.word_of_identifier PreIdentifiers.CostTag cl in
289 (match Positive.leb u.fresh_cost_label clw with
291 { Types.fst = { id_univ = u.id_univ; current_funct = u.current_funct;
292 ident_map = u.ident_map; label_map = u.label_map; fresh_cost_label =
293 (Positive.succ clw) }; Types.snd = Types.It }
294 | Bool.False -> { Types.fst = u; Types.snd = Types.It }))
296 (** val identifier_of_label :
297 Graphs.label -> ASM.identifier Monad.smax_def__o__monad **)
298 let identifier_of_label l =
300 let current = u.current_funct in
302 Identifiers.lookup_def PreIdentifiers.SymbolTag u.label_map current
303 (Identifiers.empty_map PreIdentifiers.LabelTag)
305 let { Types.fst = eta2825; Types.snd = lmap0 } =
306 match Identifiers.lookup PreIdentifiers.LabelTag lmap l with
308 let { Types.fst = id; Types.snd = univ } =
309 Identifiers.fresh PreIdentifiers.ASMTag u.id_univ
311 { Types.fst = { Types.fst = id; Types.snd = univ }; Types.snd =
312 (Identifiers.add PreIdentifiers.LabelTag lmap l id) }
314 { Types.fst = { Types.fst = id; Types.snd = u.id_univ }; Types.snd =
317 let { Types.fst = id; Types.snd = univ } = eta2825 in
318 { Types.fst = { id_univ = univ; current_funct = current; ident_map =
319 u.ident_map; label_map =
320 (Identifiers.add PreIdentifiers.SymbolTag u.label_map current lmap0);
321 fresh_cost_label = u.fresh_cost_label }; Types.snd = id })
323 (** val identifier_of_ident :
324 AST.ident -> ASM.identifier Monad.smax_def__o__monad **)
325 let identifier_of_ident i =
327 let imap = u.ident_map in
329 match Identifiers.lookup PreIdentifiers.SymbolTag imap i with
331 let { Types.fst = id; Types.snd = univ } =
332 Identifiers.fresh PreIdentifiers.ASMTag u.id_univ
334 { Types.fst = { Types.fst = id; Types.snd = univ }; Types.snd =
335 (Identifiers.add PreIdentifiers.SymbolTag imap i id) }
337 { Types.fst = { Types.fst = id; Types.snd = u.id_univ }; Types.snd =
340 let id = res.Types.fst.Types.fst in
341 let univ = res.Types.fst.Types.snd in
342 let imap0 = res.Types.snd in
343 { Types.fst = { id_univ = univ; current_funct = u.current_funct;
344 ident_map = imap0; label_map = u.label_map; fresh_cost_label =
345 u.fresh_cost_label }; Types.snd = id })
347 (** val new_ASM_universe : Joint.joint_program -> aSM_universe **)
348 let new_ASM_universe p =
349 { id_univ = Positive.One; current_funct = Positive.One; ident_map =
350 (Identifiers.empty_map PreIdentifiers.SymbolTag); label_map =
351 (Identifiers.empty_map PreIdentifiers.SymbolTag); fresh_cost_label =
354 (** val start_funct_translation :
355 AST.ident List.list -> AST.ident List.list -> (AST.ident,
356 Joint.joint_function) Types.prod -> Types.unit0 Monad.smax_def__o__monad **)
357 let start_funct_translation g functs id_f =
358 Obj.magic (fun u -> { Types.fst = { id_univ = u.id_univ; current_funct =
359 id_f.Types.fst; ident_map = u.ident_map; label_map = u.label_map;
360 fresh_cost_label = u.fresh_cost_label }; Types.snd = Types.It })
362 (** val aSM_fresh : ASM.identifier Monad.smax_def__o__monad **)
365 let { Types.fst = id; Types.snd = univ } =
366 Identifiers.fresh PreIdentifiers.ASMTag u.id_univ
368 { Types.fst = { id_univ = univ; current_funct = u.current_funct;
369 ident_map = u.ident_map; label_map = u.label_map; fresh_cost_label =
370 u.fresh_cost_label }; Types.snd = id })
372 (** val register_address : I8051.register -> ASM.subaddressing_mode **)
373 let register_address r =
375 | I8051.Register00 ->
376 (fun _ -> ASM.REGISTER (Vector.VCons ((Nat.S (Nat.S Nat.O)), Bool.False,
377 (Vector.VCons ((Nat.S Nat.O), Bool.False, (Vector.VCons (Nat.O,
378 Bool.False, Vector.VEmpty)))))))
379 | I8051.Register01 ->
380 (fun _ -> ASM.REGISTER (Vector.VCons ((Nat.S (Nat.S Nat.O)), Bool.False,
381 (Vector.VCons ((Nat.S Nat.O), Bool.False, (Vector.VCons (Nat.O,
382 Bool.True, Vector.VEmpty)))))))
383 | I8051.Register02 ->
384 (fun _ -> ASM.REGISTER (Vector.VCons ((Nat.S (Nat.S Nat.O)), Bool.False,
385 (Vector.VCons ((Nat.S Nat.O), Bool.True, (Vector.VCons (Nat.O,
386 Bool.False, Vector.VEmpty)))))))
387 | I8051.Register03 ->
388 (fun _ -> ASM.REGISTER (Vector.VCons ((Nat.S (Nat.S Nat.O)), Bool.False,
389 (Vector.VCons ((Nat.S Nat.O), Bool.True, (Vector.VCons (Nat.O,
390 Bool.True, Vector.VEmpty)))))))
391 | I8051.Register04 ->
392 (fun _ -> ASM.REGISTER (Vector.VCons ((Nat.S (Nat.S Nat.O)), Bool.True,
393 (Vector.VCons ((Nat.S Nat.O), Bool.False, (Vector.VCons (Nat.O,
394 Bool.False, Vector.VEmpty)))))))
395 | I8051.Register05 ->
396 (fun _ -> ASM.REGISTER (Vector.VCons ((Nat.S (Nat.S Nat.O)), Bool.True,
397 (Vector.VCons ((Nat.S Nat.O), Bool.False, (Vector.VCons (Nat.O,
398 Bool.True, Vector.VEmpty)))))))
399 | I8051.Register06 ->
400 (fun _ -> ASM.REGISTER (Vector.VCons ((Nat.S (Nat.S Nat.O)), Bool.True,
401 (Vector.VCons ((Nat.S Nat.O), Bool.True, (Vector.VCons (Nat.O,
402 Bool.False, Vector.VEmpty)))))))
403 | I8051.Register07 ->
404 (fun _ -> ASM.REGISTER (Vector.VCons ((Nat.S (Nat.S Nat.O)), Bool.True,
405 (Vector.VCons ((Nat.S Nat.O), Bool.True, (Vector.VCons (Nat.O,
406 Bool.True, Vector.VEmpty)))))))
407 | I8051.Register10 ->
409 (Arithmetic.bitvector_of_nat (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
410 (Nat.S (Nat.S Nat.O)))))))) (I8051.nat_of_register r)))
411 | I8051.Register11 ->
413 (Arithmetic.bitvector_of_nat (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
414 (Nat.S (Nat.S Nat.O)))))))) (I8051.nat_of_register r)))
415 | I8051.Register12 ->
417 (Arithmetic.bitvector_of_nat (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
418 (Nat.S (Nat.S Nat.O)))))))) (I8051.nat_of_register r)))
419 | I8051.Register13 ->
421 (Arithmetic.bitvector_of_nat (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
422 (Nat.S (Nat.S Nat.O)))))))) (I8051.nat_of_register r)))
423 | I8051.Register14 ->
425 (Arithmetic.bitvector_of_nat (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
426 (Nat.S (Nat.S Nat.O)))))))) (I8051.nat_of_register r)))
427 | I8051.Register15 ->
429 (Arithmetic.bitvector_of_nat (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
430 (Nat.S (Nat.S Nat.O)))))))) (I8051.nat_of_register r)))
431 | I8051.Register16 ->
433 (Arithmetic.bitvector_of_nat (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
434 (Nat.S (Nat.S Nat.O)))))))) (I8051.nat_of_register r)))
435 | I8051.Register17 ->
437 (Arithmetic.bitvector_of_nat (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
438 (Nat.S (Nat.S Nat.O)))))))) (I8051.nat_of_register r)))
439 | I8051.Register20 ->
441 (Arithmetic.bitvector_of_nat (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
442 (Nat.S (Nat.S Nat.O)))))))) (I8051.nat_of_register r)))
443 | I8051.Register21 ->
445 (Arithmetic.bitvector_of_nat (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
446 (Nat.S (Nat.S Nat.O)))))))) (I8051.nat_of_register r)))
447 | I8051.Register22 ->
449 (Arithmetic.bitvector_of_nat (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
450 (Nat.S (Nat.S Nat.O)))))))) (I8051.nat_of_register r)))
451 | I8051.Register23 ->
453 (Arithmetic.bitvector_of_nat (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
454 (Nat.S (Nat.S Nat.O)))))))) (I8051.nat_of_register r)))
455 | I8051.Register24 ->
457 (Arithmetic.bitvector_of_nat (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
458 (Nat.S (Nat.S Nat.O)))))))) (I8051.nat_of_register r)))
459 | I8051.Register25 ->
461 (Arithmetic.bitvector_of_nat (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
462 (Nat.S (Nat.S Nat.O)))))))) (I8051.nat_of_register r)))
463 | I8051.Register26 ->
465 (Arithmetic.bitvector_of_nat (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
466 (Nat.S (Nat.S Nat.O)))))))) (I8051.nat_of_register r)))
467 | I8051.Register27 ->
469 (Arithmetic.bitvector_of_nat (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
470 (Nat.S (Nat.S Nat.O)))))))) (I8051.nat_of_register r)))
471 | I8051.Register30 ->
473 (Arithmetic.bitvector_of_nat (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
474 (Nat.S (Nat.S Nat.O)))))))) (I8051.nat_of_register r)))
475 | I8051.Register31 ->
477 (Arithmetic.bitvector_of_nat (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
478 (Nat.S (Nat.S Nat.O)))))))) (I8051.nat_of_register r)))
479 | I8051.Register32 ->
481 (Arithmetic.bitvector_of_nat (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
482 (Nat.S (Nat.S Nat.O)))))))) (I8051.nat_of_register r)))
483 | I8051.Register33 ->
485 (Arithmetic.bitvector_of_nat (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
486 (Nat.S (Nat.S Nat.O)))))))) (I8051.nat_of_register r)))
487 | I8051.Register34 ->
489 (Arithmetic.bitvector_of_nat (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
490 (Nat.S (Nat.S Nat.O)))))))) (I8051.nat_of_register r)))
491 | I8051.Register35 ->
493 (Arithmetic.bitvector_of_nat (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
494 (Nat.S (Nat.S Nat.O)))))))) (I8051.nat_of_register r)))
495 | I8051.Register36 ->
497 (Arithmetic.bitvector_of_nat (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
498 (Nat.S (Nat.S Nat.O)))))))) (I8051.nat_of_register r)))
499 | I8051.Register37 ->
501 (Arithmetic.bitvector_of_nat (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
502 (Nat.S (Nat.S Nat.O)))))))) (I8051.nat_of_register r)))
503 | I8051.RegisterA -> (fun _ -> ASM.ACC_A)
506 (Arithmetic.bitvector_of_nat (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
507 (Nat.S (Nat.S Nat.O)))))))) (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
508 (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
509 (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
510 (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
511 (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
512 (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
513 (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
514 (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
515 (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
516 (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
517 (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
518 (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
519 (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
520 (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
521 (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
522 (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
523 (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
524 (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
525 (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
526 (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
527 (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
528 (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
529 (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
530 (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
531 (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
532 (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
533 (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
535 Nat.O))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))
536 | I8051.RegisterDPL ->
538 (Arithmetic.bitvector_of_nat (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
539 (Nat.S (Nat.S Nat.O)))))))) (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
540 (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
541 (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
542 (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
543 (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
544 (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
545 (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
546 (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
547 (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
548 (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
549 (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
550 (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
551 (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
552 (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
553 (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
554 Nat.O))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))
555 | I8051.RegisterDPH ->
557 (Arithmetic.bitvector_of_nat (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
558 (Nat.S (Nat.S Nat.O)))))))) (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
559 (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
560 (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
561 (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
562 (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
563 (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
564 (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
565 (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
566 (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
567 (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
568 (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
569 (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
570 (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
571 (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
572 (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
573 Nat.O)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))
574 | I8051.RegisterCarry ->
576 (Arithmetic.bitvector_of_nat (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
577 (Nat.S (Nat.S Nat.O)))))))) (I8051.nat_of_register r)))) __
579 (** val vector_cast :
580 Nat.nat -> Nat.nat -> 'a1 -> 'a1 Vector.vector -> 'a1 Vector.vector **)
581 let vector_cast n m dflt v =
582 Util.if_then_else_safe (Nat.leb n m) (fun _ ->
583 Vector.append (Nat.minus m n) n (Vector.replicate (Nat.minus m n) dflt) v)
584 (fun _ -> (Vector.vsplit (Nat.minus n m) m v).Types.snd)
586 (** val arg_address : Joint.hdw_argument -> ASM.subaddressing_mode **)
587 let arg_address = function
590 ASM.subaddressing_modeel__o__mk_subaddressing_mode (Nat.S (Nat.S Nat.O))
591 (Nat.S (Nat.S (Nat.S Nat.O))) (Vector.VCons ((Nat.S (Nat.S Nat.O)),
592 ASM.Acc_a, (Vector.VCons ((Nat.S Nat.O), ASM.Direct, (Vector.VCons
593 (Nat.O, ASM.Registr, Vector.VEmpty)))))) (Vector.VCons ((Nat.S (Nat.S
594 (Nat.S Nat.O))), ASM.Acc_a, (Vector.VCons ((Nat.S (Nat.S Nat.O)),
595 ASM.Direct, (Vector.VCons ((Nat.S Nat.O), ASM.Registr, (Vector.VCons
596 (Nat.O, ASM.Data, Vector.VEmpty)))))))) (register_address r)
599 | Joint.Imm v -> let x = ASM.DATA v in x
601 type lin_statement = Joint.joint_statement LabelledObjects.labelled_obj
603 (** val data_of_int : BitVector.byte -> ASM.addressing_mode **)
607 (** val data16_of_int : Nat.nat -> ASM.addressing_mode **)
608 let data16_of_int bv =
610 (Arithmetic.bitvector_of_nat (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
611 (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
612 Nat.O)))))))))))))))) bv)
614 (** val accumulator_address : ASM.addressing_mode **)
615 let accumulator_address =
617 (Arithmetic.bitvector_of_nat (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
618 (Nat.S (Nat.S Nat.O)))))))) (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
619 (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
620 (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
621 (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
622 (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
623 (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
624 (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
625 (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
626 (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
627 (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
628 (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
629 (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
630 (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
631 (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
632 (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
633 (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
634 (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
635 (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
636 (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
637 (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
638 (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
639 (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
640 (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
641 Nat.O)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))
643 (** val asm_other_bit : ASM.addressing_mode **)
645 ASM.BIT_ADDR Joint.zero_byte
647 (** val one_word : BitVector.word **)
649 Vector.append (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
650 (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))))))))))))
652 (BitVector.zero (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
653 (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))))))))))))))
654 (Vector.VCons (Nat.O, Bool.True, Vector.VEmpty))
656 (** val translate_statements :
657 AST.ident List.list -> Joint.joint_statement -> ASM.pseudo_instruction
658 Monad.smax_def__o__monad **)
659 let translate_statements globals = function
660 | Joint.Sequential (instr, x) ->
662 | Joint.COST_LABEL lbl ->
663 Monad.m_bind0 (Monad.smax_def State.state_monad) (report_cost lbl)
665 Monad.m_return0 (Monad.smax_def State.state_monad) (ASM.Cost lbl))
666 | Joint.CALL (f, x0, x1) ->
669 Monad.m_bind0 (Monad.smax_def State.state_monad)
670 (identifier_of_ident id) (fun id' ->
671 Monad.m_return0 (Monad.smax_def State.state_monad) (ASM.Call
672 (ASM.toASM_ident PreIdentifiers.ASMTag id')))
674 Monad.m_return0 (Monad.smax_def State.state_monad) (ASM.Instruction
675 (ASM.JMP ASM.ACC_DPTR)))
676 | Joint.COND (x0, lbl) ->
677 Monad.m_bind0 (Monad.smax_def State.state_monad)
678 (identifier_of_label lbl) (fun l ->
679 Monad.m_return0 (Monad.smax_def State.state_monad) (ASM.Instruction
681 | Joint.Step_seq instr' ->
683 | Joint.COMMENT comment ->
684 Monad.m_return0 (Monad.smax_def State.state_monad) (ASM.Comment
687 Monad.m_return0 (Monad.smax_def State.state_monad)
688 (match Obj.magic regs with
689 | Joint_LTL_LIN.From_acc (reg, x0) ->
690 (match ASM.subaddressing_modeel (Nat.S (Nat.S Nat.O))
691 (Vector.VCons ((Nat.S (Nat.S Nat.O)), ASM.Acc_a,
692 (Vector.VCons ((Nat.S Nat.O), ASM.Direct, (Vector.VCons
693 (Nat.O, ASM.Registr, Vector.VEmpty))))))
694 (register_address reg) with
696 (fun _ -> ASM.Instruction (ASM.MOV (Types.Inl (Types.Inl
697 (Types.Inl (Types.Inr { Types.fst = (ASM.DIRECT d);
698 Types.snd = ASM.ACC_A }))))))
699 | ASM.INDIRECT x1 -> (fun _ -> assert false (* absurd case *))
700 | ASM.EXT_INDIRECT x1 ->
701 (fun _ -> assert false (* absurd case *))
703 (fun _ -> ASM.Instruction (ASM.MOV (Types.Inl (Types.Inl
704 (Types.Inl (Types.Inl (Types.Inr { Types.fst =
705 (ASM.REGISTER r); Types.snd = ASM.ACC_A })))))))
706 | ASM.ACC_A -> (fun _ -> ASM.Instruction ASM.NOP)
707 | ASM.ACC_B -> (fun _ -> assert false (* absurd case *))
708 | ASM.DPTR -> (fun _ -> assert false (* absurd case *))
709 | ASM.DATA x1 -> (fun _ -> assert false (* absurd case *))
710 | ASM.DATA16 x1 -> (fun _ -> assert false (* absurd case *))
711 | ASM.ACC_DPTR -> (fun _ -> assert false (* absurd case *))
712 | ASM.ACC_PC -> (fun _ -> assert false (* absurd case *))
713 | ASM.EXT_INDIRECT_DPTR ->
714 (fun _ -> assert false (* absurd case *))
715 | ASM.INDIRECT_DPTR ->
716 (fun _ -> assert false (* absurd case *))
717 | ASM.CARRY -> (fun _ -> assert false (* absurd case *))
718 | ASM.BIT_ADDR x1 -> (fun _ -> assert false (* absurd case *))
719 | ASM.N_BIT_ADDR x1 ->
720 (fun _ -> assert false (* absurd case *))
721 | ASM.RELATIVE x1 -> (fun _ -> assert false (* absurd case *))
722 | ASM.ADDR11 x1 -> (fun _ -> assert false (* absurd case *))
723 | ASM.ADDR16 x1 -> (fun _ -> assert false (* absurd case *)))
725 | Joint_LTL_LIN.To_acc (x0, reg) ->
726 (match ASM.subaddressing_modeel (Nat.S (Nat.S Nat.O))
727 (Vector.VCons ((Nat.S (Nat.S Nat.O)), ASM.Acc_a,
728 (Vector.VCons ((Nat.S Nat.O), ASM.Direct, (Vector.VCons
729 (Nat.O, ASM.Registr, Vector.VEmpty))))))
730 (register_address reg) with
732 (fun _ -> ASM.Instruction (ASM.MOV (Types.Inl (Types.Inl
733 (Types.Inl (Types.Inl (Types.Inl { Types.fst = ASM.ACC_A;
734 Types.snd = (ASM.DIRECT d) })))))))
735 | ASM.INDIRECT x1 -> (fun _ -> assert false (* absurd case *))
736 | ASM.EXT_INDIRECT x1 ->
737 (fun _ -> assert false (* absurd case *))
739 (fun _ -> ASM.Instruction (ASM.MOV (Types.Inl (Types.Inl
740 (Types.Inl (Types.Inl (Types.Inl { Types.fst = ASM.ACC_A;
741 Types.snd = (ASM.REGISTER r) })))))))
742 | ASM.ACC_A -> (fun _ -> ASM.Instruction ASM.NOP)
743 | ASM.ACC_B -> (fun _ -> assert false (* absurd case *))
744 | ASM.DPTR -> (fun _ -> assert false (* absurd case *))
745 | ASM.DATA x1 -> (fun _ -> assert false (* absurd case *))
746 | ASM.DATA16 x1 -> (fun _ -> assert false (* absurd case *))
747 | ASM.ACC_DPTR -> (fun _ -> assert false (* absurd case *))
748 | ASM.ACC_PC -> (fun _ -> assert false (* absurd case *))
749 | ASM.EXT_INDIRECT_DPTR ->
750 (fun _ -> assert false (* absurd case *))
751 | ASM.INDIRECT_DPTR ->
752 (fun _ -> assert false (* absurd case *))
753 | ASM.CARRY -> (fun _ -> assert false (* absurd case *))
754 | ASM.BIT_ADDR x1 -> (fun _ -> assert false (* absurd case *))
755 | ASM.N_BIT_ADDR x1 ->
756 (fun _ -> assert false (* absurd case *))
757 | ASM.RELATIVE x1 -> (fun _ -> assert false (* absurd case *))
758 | ASM.ADDR11 x1 -> (fun _ -> assert false (* absurd case *))
759 | ASM.ADDR16 x1 -> (fun _ -> assert false (* absurd case *)))
761 | Joint_LTL_LIN.Int_to_reg (reg, b) ->
762 (match ASM.subaddressing_modeel (Nat.S (Nat.S Nat.O))
763 (Vector.VCons ((Nat.S (Nat.S Nat.O)), ASM.Acc_a,
764 (Vector.VCons ((Nat.S Nat.O), ASM.Direct, (Vector.VCons
765 (Nat.O, ASM.Registr, Vector.VEmpty))))))
766 (register_address reg) with
768 (fun _ -> ASM.Instruction (ASM.MOV (Types.Inl (Types.Inl
769 (Types.Inl (Types.Inr { Types.fst = (ASM.DIRECT d);
770 Types.snd = (ASM.DATA b) }))))))
771 | ASM.INDIRECT x0 -> (fun _ -> assert false (* absurd case *))
772 | ASM.EXT_INDIRECT x0 ->
773 (fun _ -> assert false (* absurd case *))
775 (fun _ -> ASM.Instruction (ASM.MOV (Types.Inl (Types.Inl
776 (Types.Inl (Types.Inl (Types.Inr { Types.fst =
777 (ASM.REGISTER r); Types.snd = (ASM.DATA b) })))))))
780 match BitVector.eq_bv (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
781 (Nat.S (Nat.S (Nat.S Nat.O))))))))
782 (BitVector.zero (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
783 (Nat.S (Nat.S (Nat.S Nat.O))))))))) b with
784 | Bool.True -> ASM.Instruction (ASM.CLR ASM.ACC_A)
786 ASM.Instruction (ASM.MOV (Types.Inl (Types.Inl (Types.Inl
787 (Types.Inl (Types.Inl { Types.fst = ASM.ACC_A;
788 Types.snd = (ASM.DATA b) })))))))
789 | ASM.ACC_B -> (fun _ -> assert false (* absurd case *))
790 | ASM.DPTR -> (fun _ -> assert false (* absurd case *))
791 | ASM.DATA x0 -> (fun _ -> assert false (* absurd case *))
792 | ASM.DATA16 x0 -> (fun _ -> assert false (* absurd case *))
793 | ASM.ACC_DPTR -> (fun _ -> assert false (* absurd case *))
794 | ASM.ACC_PC -> (fun _ -> assert false (* absurd case *))
795 | ASM.EXT_INDIRECT_DPTR ->
796 (fun _ -> assert false (* absurd case *))
797 | ASM.INDIRECT_DPTR ->
798 (fun _ -> assert false (* absurd case *))
799 | ASM.CARRY -> (fun _ -> assert false (* absurd case *))
800 | ASM.BIT_ADDR x0 -> (fun _ -> assert false (* absurd case *))
801 | ASM.N_BIT_ADDR x0 ->
802 (fun _ -> assert false (* absurd case *))
803 | ASM.RELATIVE x0 -> (fun _ -> assert false (* absurd case *))
804 | ASM.ADDR11 x0 -> (fun _ -> assert false (* absurd case *))
805 | ASM.ADDR16 x0 -> (fun _ -> assert false (* absurd case *)))
807 | Joint_LTL_LIN.Int_to_acc (x0, b) ->
808 (match BitVector.eq_bv (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
809 (Nat.S (Nat.S Nat.O))))))))
810 (BitVector.zero (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
811 (Nat.S (Nat.S (Nat.S Nat.O))))))))) b with
812 | Bool.True -> ASM.Instruction (ASM.CLR ASM.ACC_A)
814 ASM.Instruction (ASM.MOV (Types.Inl (Types.Inl (Types.Inl
815 (Types.Inl (Types.Inl { Types.fst = ASM.ACC_A; Types.snd =
816 (ASM.DATA b) }))))))))
818 Monad.m_return0 (Monad.smax_def State.state_monad) (ASM.Instruction
819 (ASM.POP accumulator_address))
821 Monad.m_return0 (Monad.smax_def State.state_monad) (ASM.Instruction
822 (ASM.PUSH accumulator_address))
823 | Joint.ADDRESS (id, off, x0, x1) ->
824 Monad.m_bind0 (Monad.smax_def State.state_monad)
825 (identifier_of_ident id) (fun id0 ->
826 Monad.m_return0 (Monad.smax_def State.state_monad) (ASM.Mov
827 ((Types.Inl ASM.DPTR), id0, off)))
828 | Joint.OPACCS (accs, x0, x1, x2, x3) ->
829 Monad.m_return0 (Monad.smax_def State.state_monad)
832 ASM.Instruction (ASM.MUL (ASM.ACC_A, ASM.ACC_B))
833 | BackEndOps.DivuModu ->
834 ASM.Instruction (ASM.DIV (ASM.ACC_A, ASM.ACC_B)))
835 | Joint.OP1 (op1, x0, x1) ->
836 Monad.m_return0 (Monad.smax_def State.state_monad)
838 | BackEndOps.Cmpl -> ASM.Instruction (ASM.CPL ASM.ACC_A)
839 | BackEndOps.Inc -> ASM.Instruction (ASM.INC ASM.ACC_A)
840 | BackEndOps.Rl -> ASM.Instruction (ASM.RL ASM.ACC_A))
841 | Joint.OP2 (op2, x0, x1, reg) ->
842 Monad.m_return0 (Monad.smax_def State.state_monad)
843 ((match ASM.subaddressing_modeel (Nat.S (Nat.S (Nat.S Nat.O)))
844 (Vector.VCons ((Nat.S (Nat.S (Nat.S Nat.O))), ASM.Acc_a,
845 (Vector.VCons ((Nat.S (Nat.S Nat.O)), ASM.Direct,
846 (Vector.VCons ((Nat.S Nat.O), ASM.Registr, (Vector.VCons
847 (Nat.O, ASM.Data, Vector.VEmpty))))))))
848 (arg_address (Obj.magic reg)) with
853 ASM.Instruction (ASM.ADD (ASM.ACC_A, (ASM.DIRECT d)))
855 ASM.Instruction (ASM.ADDC (ASM.ACC_A, (ASM.DIRECT d)))
857 ASM.Instruction (ASM.SUBB (ASM.ACC_A, (ASM.DIRECT d)))
859 ASM.Instruction (ASM.ANL (Types.Inl (Types.Inl
860 { Types.fst = ASM.ACC_A; Types.snd = (ASM.DIRECT d) })))
862 ASM.Instruction (ASM.ORL (Types.Inl (Types.Inl
863 { Types.fst = ASM.ACC_A; Types.snd = (ASM.DIRECT d) })))
865 ASM.Instruction (ASM.XRL (Types.Inl { Types.fst =
866 ASM.ACC_A; Types.snd = (ASM.DIRECT d) })))
867 | ASM.INDIRECT x2 -> (fun _ -> assert false (* absurd case *))
868 | ASM.EXT_INDIRECT x2 ->
869 (fun _ -> assert false (* absurd case *))
874 ASM.Instruction (ASM.ADD (ASM.ACC_A, (ASM.REGISTER r)))
876 ASM.Instruction (ASM.ADDC (ASM.ACC_A, (ASM.REGISTER r)))
878 ASM.Instruction (ASM.SUBB (ASM.ACC_A, (ASM.REGISTER r)))
880 ASM.Instruction (ASM.ANL (Types.Inl (Types.Inl
881 { Types.fst = ASM.ACC_A; Types.snd = (ASM.REGISTER
884 ASM.Instruction (ASM.ORL (Types.Inl (Types.Inl
885 { Types.fst = ASM.ACC_A; Types.snd = (ASM.REGISTER
888 ASM.Instruction (ASM.XRL (Types.Inl { Types.fst =
889 ASM.ACC_A; Types.snd = (ASM.REGISTER r) })))
894 ASM.Instruction (ASM.ADD (ASM.ACC_A, accumulator_address))
896 ASM.Instruction (ASM.ADDC (ASM.ACC_A, accumulator_address))
898 ASM.Instruction (ASM.SUBB (ASM.ACC_A, accumulator_address))
899 | BackEndOps.And -> ASM.Instruction ASM.NOP
900 | BackEndOps.Or -> ASM.Instruction ASM.NOP
901 | BackEndOps.Xor -> ASM.Instruction (ASM.CLR ASM.ACC_A))
902 | ASM.ACC_B -> (fun _ -> assert false (* absurd case *))
903 | ASM.DPTR -> (fun _ -> assert false (* absurd case *))
908 ASM.Instruction (ASM.ADD (ASM.ACC_A, (ASM.DATA b)))
910 ASM.Instruction (ASM.ADDC (ASM.ACC_A, (ASM.DATA b)))
912 ASM.Instruction (ASM.SUBB (ASM.ACC_A, (ASM.DATA b)))
914 ASM.Instruction (ASM.ANL (Types.Inl (Types.Inl
915 { Types.fst = ASM.ACC_A; Types.snd = (ASM.DATA b) })))
917 ASM.Instruction (ASM.ORL (Types.Inl (Types.Inl
918 { Types.fst = ASM.ACC_A; Types.snd = (ASM.DATA b) })))
920 ASM.Instruction (ASM.XRL (Types.Inl { Types.fst =
921 ASM.ACC_A; Types.snd = (ASM.DATA b) })))
922 | ASM.DATA16 x2 -> (fun _ -> assert false (* absurd case *))
923 | ASM.ACC_DPTR -> (fun _ -> assert false (* absurd case *))
924 | ASM.ACC_PC -> (fun _ -> assert false (* absurd case *))
925 | ASM.EXT_INDIRECT_DPTR ->
926 (fun _ -> assert false (* absurd case *))
927 | ASM.INDIRECT_DPTR -> (fun _ -> assert false (* absurd case *))
928 | ASM.CARRY -> (fun _ -> assert false (* absurd case *))
929 | ASM.BIT_ADDR x2 -> (fun _ -> assert false (* absurd case *))
930 | ASM.N_BIT_ADDR x2 -> (fun _ -> assert false (* absurd case *))
931 | ASM.RELATIVE x2 -> (fun _ -> assert false (* absurd case *))
932 | ASM.ADDR11 x2 -> (fun _ -> assert false (* absurd case *))
933 | ASM.ADDR16 x2 -> (fun _ -> assert false (* absurd case *))) __)
934 | Joint.CLEAR_CARRY ->
935 Monad.m_return0 (Monad.smax_def State.state_monad) (ASM.Instruction
938 Monad.m_return0 (Monad.smax_def State.state_monad) (ASM.Instruction
939 (ASM.SETB ASM.CARRY))
940 | Joint.LOAD (x0, x1, x2) ->
941 Monad.m_return0 (Monad.smax_def State.state_monad) (ASM.Instruction
942 (ASM.MOVX (Types.Inl { Types.fst = ASM.ACC_A; Types.snd =
943 ASM.EXT_INDIRECT_DPTR })))
944 | Joint.STORE (x0, x1, x2) ->
945 Monad.m_return0 (Monad.smax_def State.state_monad) (ASM.Instruction
946 (ASM.MOVX (Types.Inr { Types.fst = ASM.EXT_INDIRECT_DPTR;
947 Types.snd = ASM.ACC_A })))
948 | Joint.Extension_seq ext ->
949 (match Obj.magic ext with
950 | Joint_LTL_LIN.SAVE_CARRY ->
951 Monad.m_return0 (Monad.smax_def State.state_monad)
952 (ASM.Instruction (ASM.MOV (Types.Inr { Types.fst =
953 asm_other_bit; Types.snd = ASM.CARRY })))
954 | Joint_LTL_LIN.RESTORE_CARRY ->
955 Monad.m_return0 (Monad.smax_def State.state_monad)
956 (ASM.Instruction (ASM.MOV (Types.Inl (Types.Inr { Types.fst =
957 ASM.CARRY; Types.snd = asm_other_bit }))))
958 | Joint_LTL_LIN.LOW_ADDRESS lbl ->
959 Monad.m_bind0 (Monad.smax_def State.state_monad)
960 (identifier_of_label lbl) (fun lbl' ->
961 Monad.m_return0 (Monad.smax_def State.state_monad) (ASM.Mov
962 ((Types.Inr { Types.fst = (register_address I8051.RegisterA);
963 Types.snd = ASM.LOW }), lbl', one_word)))
964 | Joint_LTL_LIN.HIGH_ADDRESS lbl ->
965 Monad.m_bind0 (Monad.smax_def State.state_monad)
966 (identifier_of_label lbl) (fun lbl' ->
967 Monad.m_return0 (Monad.smax_def State.state_monad) (ASM.Mov
968 ((Types.Inr { Types.fst = (register_address I8051.RegisterA);
969 Types.snd = ASM.HIGH }), lbl', one_word))))))
970 | Joint.Final instr ->
973 Monad.m_bind0 (Monad.smax_def State.state_monad)
974 (identifier_of_label lbl) (fun lbl' ->
975 Monad.m_return0 (Monad.smax_def State.state_monad) (ASM.Jmp
976 (ASM.toASM_ident PreIdentifiers.ASMTag lbl')))
978 Monad.m_return0 (Monad.smax_def State.state_monad) (ASM.Instruction
980 | Joint.TAILCALL (x, x0) -> assert false (* absurd case *))
981 | Joint.FCOND (x0, lbl_true, lbl_false) ->
982 Monad.m_bind0 (Monad.smax_def State.state_monad)
983 (identifier_of_label lbl_true) (fun l1 ->
984 Monad.m_bind0 (Monad.smax_def State.state_monad)
985 (identifier_of_label lbl_false) (fun l2 ->
986 Monad.m_return0 (Monad.smax_def State.state_monad) (ASM.Jnz (ASM.ACC_A,
989 (** val build_translated_statement :
990 AST.ident List.list -> lin_statement -> __ **)
991 let build_translated_statement globals statement =
992 Monad.m_bind0 (Monad.smax_def State.state_monad)
993 (translate_statements globals statement.Types.snd) (fun stmt ->
994 match statement.Types.fst with
996 Monad.m_return0 (Monad.smax_def State.state_monad) { Types.fst =
997 Types.None; Types.snd = stmt }
999 Monad.m_bind0 (Monad.smax_def State.state_monad)
1000 (identifier_of_label lbl) (fun lbl' ->
1001 Monad.m_return0 (Monad.smax_def State.state_monad) { Types.fst =
1002 (Types.Some lbl'); Types.snd = stmt }))
1004 (** val translate_code :
1005 AST.ident List.list -> lin_statement List.list -> __ **)
1006 let translate_code globals code =
1007 Monad.m_list_map (Monad.smax_def State.state_monad)
1008 (build_translated_statement globals) code
1010 (** val translate_fun_def :
1011 AST.ident List.list -> AST.ident List.list -> (AST.ident,
1012 Joint.joint_function) Types.prod -> __ **)
1013 let translate_fun_def globals functions id_def =
1014 Monad.m_bind0 (Monad.smax_def State.state_monad)
1015 (start_funct_translation globals functions id_def) (fun x ->
1016 match id_def.Types.snd with
1017 | AST.Internal int ->
1018 let code = (Types.pi1 int).Joint.joint_if_code in
1019 Monad.m_bind0 (Monad.smax_def State.state_monad)
1020 (identifier_of_ident id_def.Types.fst) (fun id ->
1021 Monad.m_bind0 (Monad.smax_def State.state_monad)
1022 (translate_code (List.append functions globals) (Obj.magic code))
1026 Monad.m_return0 (Monad.smax_def State.state_monad) (List.Cons
1027 ({ Types.fst = (Types.Some id); Types.snd = (ASM.Instruction
1028 ASM.RET) }, List.Nil))
1029 | List.Cons (hd, tl) ->
1030 (match hd.Types.fst with
1032 Monad.m_return0 (Monad.smax_def State.state_monad) (List.Cons
1033 ({ Types.fst = (Types.Some id); Types.snd = hd.Types.snd },
1036 Monad.m_return0 (Monad.smax_def State.state_monad) (List.Cons
1037 ({ Types.fst = (Types.Some id); Types.snd = (ASM.Instruction
1038 ASM.NOP) }, (List.Cons (hd, tl)))))))
1039 | AST.External x0 ->
1040 Monad.m_return0 (Monad.smax_def State.state_monad) List.Nil)
1042 type init_mutable = { virtual_dptr : (ASM.identifier, Z.z) Types.prod;
1043 actual_dptr : (ASM.identifier, Z.z) Types.prod;
1044 built_code : ASM.labelled_instruction List.list
1046 built_preamble : (ASM.identifier, BitVector.word)
1047 Types.prod List.list }
1049 (** val init_mutable_rect_Type4 :
1050 ((ASM.identifier, Z.z) Types.prod -> (ASM.identifier, Z.z) Types.prod ->
1051 ASM.labelled_instruction List.list List.list -> (ASM.identifier,
1052 BitVector.word) Types.prod List.list -> 'a1) -> init_mutable -> 'a1 **)
1053 let rec init_mutable_rect_Type4 h_mk_init_mutable x_614 =
1054 let { virtual_dptr = virtual_dptr0; actual_dptr = actual_dptr0;
1055 built_code = built_code0; built_preamble = built_preamble0 } = x_614
1057 h_mk_init_mutable virtual_dptr0 actual_dptr0 built_code0 built_preamble0
1059 (** val init_mutable_rect_Type5 :
1060 ((ASM.identifier, Z.z) Types.prod -> (ASM.identifier, Z.z) Types.prod ->
1061 ASM.labelled_instruction List.list List.list -> (ASM.identifier,
1062 BitVector.word) Types.prod List.list -> 'a1) -> init_mutable -> 'a1 **)
1063 let rec init_mutable_rect_Type5 h_mk_init_mutable x_616 =
1064 let { virtual_dptr = virtual_dptr0; actual_dptr = actual_dptr0;
1065 built_code = built_code0; built_preamble = built_preamble0 } = x_616
1067 h_mk_init_mutable virtual_dptr0 actual_dptr0 built_code0 built_preamble0
1069 (** val init_mutable_rect_Type3 :
1070 ((ASM.identifier, Z.z) Types.prod -> (ASM.identifier, Z.z) Types.prod ->
1071 ASM.labelled_instruction List.list List.list -> (ASM.identifier,
1072 BitVector.word) Types.prod List.list -> 'a1) -> init_mutable -> 'a1 **)
1073 let rec init_mutable_rect_Type3 h_mk_init_mutable x_618 =
1074 let { virtual_dptr = virtual_dptr0; actual_dptr = actual_dptr0;
1075 built_code = built_code0; built_preamble = built_preamble0 } = x_618
1077 h_mk_init_mutable virtual_dptr0 actual_dptr0 built_code0 built_preamble0
1079 (** val init_mutable_rect_Type2 :
1080 ((ASM.identifier, Z.z) Types.prod -> (ASM.identifier, Z.z) Types.prod ->
1081 ASM.labelled_instruction List.list List.list -> (ASM.identifier,
1082 BitVector.word) Types.prod List.list -> 'a1) -> init_mutable -> 'a1 **)
1083 let rec init_mutable_rect_Type2 h_mk_init_mutable x_620 =
1084 let { virtual_dptr = virtual_dptr0; actual_dptr = actual_dptr0;
1085 built_code = built_code0; built_preamble = built_preamble0 } = x_620
1087 h_mk_init_mutable virtual_dptr0 actual_dptr0 built_code0 built_preamble0
1089 (** val init_mutable_rect_Type1 :
1090 ((ASM.identifier, Z.z) Types.prod -> (ASM.identifier, Z.z) Types.prod ->
1091 ASM.labelled_instruction List.list List.list -> (ASM.identifier,
1092 BitVector.word) Types.prod List.list -> 'a1) -> init_mutable -> 'a1 **)
1093 let rec init_mutable_rect_Type1 h_mk_init_mutable x_622 =
1094 let { virtual_dptr = virtual_dptr0; actual_dptr = actual_dptr0;
1095 built_code = built_code0; built_preamble = built_preamble0 } = x_622
1097 h_mk_init_mutable virtual_dptr0 actual_dptr0 built_code0 built_preamble0
1099 (** val init_mutable_rect_Type0 :
1100 ((ASM.identifier, Z.z) Types.prod -> (ASM.identifier, Z.z) Types.prod ->
1101 ASM.labelled_instruction List.list List.list -> (ASM.identifier,
1102 BitVector.word) Types.prod List.list -> 'a1) -> init_mutable -> 'a1 **)
1103 let rec init_mutable_rect_Type0 h_mk_init_mutable x_624 =
1104 let { virtual_dptr = virtual_dptr0; actual_dptr = actual_dptr0;
1105 built_code = built_code0; built_preamble = built_preamble0 } = x_624
1107 h_mk_init_mutable virtual_dptr0 actual_dptr0 built_code0 built_preamble0
1109 (** val virtual_dptr : init_mutable -> (ASM.identifier, Z.z) Types.prod **)
1110 let rec virtual_dptr xxx =
1113 (** val actual_dptr : init_mutable -> (ASM.identifier, Z.z) Types.prod **)
1114 let rec actual_dptr xxx =
1117 (** val built_code :
1118 init_mutable -> ASM.labelled_instruction List.list List.list **)
1119 let rec built_code xxx =
1122 (** val built_preamble :
1123 init_mutable -> (ASM.identifier, BitVector.word) Types.prod List.list **)
1124 let rec built_preamble xxx =
1127 (** val init_mutable_inv_rect_Type4 :
1128 init_mutable -> ((ASM.identifier, Z.z) Types.prod -> (ASM.identifier,
1129 Z.z) Types.prod -> ASM.labelled_instruction List.list List.list ->
1130 (ASM.identifier, BitVector.word) Types.prod List.list -> __ -> 'a1) ->
1132 let init_mutable_inv_rect_Type4 hterm h1 =
1133 let hcut = init_mutable_rect_Type4 h1 hterm in hcut __
1135 (** val init_mutable_inv_rect_Type3 :
1136 init_mutable -> ((ASM.identifier, Z.z) Types.prod -> (ASM.identifier,
1137 Z.z) Types.prod -> ASM.labelled_instruction List.list List.list ->
1138 (ASM.identifier, BitVector.word) Types.prod List.list -> __ -> 'a1) ->
1140 let init_mutable_inv_rect_Type3 hterm h1 =
1141 let hcut = init_mutable_rect_Type3 h1 hterm in hcut __
1143 (** val init_mutable_inv_rect_Type2 :
1144 init_mutable -> ((ASM.identifier, Z.z) Types.prod -> (ASM.identifier,
1145 Z.z) Types.prod -> ASM.labelled_instruction List.list List.list ->
1146 (ASM.identifier, BitVector.word) Types.prod List.list -> __ -> 'a1) ->
1148 let init_mutable_inv_rect_Type2 hterm h1 =
1149 let hcut = init_mutable_rect_Type2 h1 hterm in hcut __
1151 (** val init_mutable_inv_rect_Type1 :
1152 init_mutable -> ((ASM.identifier, Z.z) Types.prod -> (ASM.identifier,
1153 Z.z) Types.prod -> ASM.labelled_instruction List.list List.list ->
1154 (ASM.identifier, BitVector.word) Types.prod List.list -> __ -> 'a1) ->
1156 let init_mutable_inv_rect_Type1 hterm h1 =
1157 let hcut = init_mutable_rect_Type1 h1 hterm in hcut __
1159 (** val init_mutable_inv_rect_Type0 :
1160 init_mutable -> ((ASM.identifier, Z.z) Types.prod -> (ASM.identifier,
1161 Z.z) Types.prod -> ASM.labelled_instruction List.list List.list ->
1162 (ASM.identifier, BitVector.word) Types.prod List.list -> __ -> 'a1) ->
1164 let init_mutable_inv_rect_Type0 hterm h1 =
1165 let hcut = init_mutable_rect_Type0 h1 hterm in hcut __
1167 (** val init_mutable_discr : init_mutable -> init_mutable -> __ **)
1168 let init_mutable_discr x y =
1169 Logic.eq_rect_Type2 x
1170 (let { virtual_dptr = a0; actual_dptr = a1; built_code = a2;
1171 built_preamble = a3 } = x
1173 Obj.magic (fun _ dH -> dH __ __ __ __)) y
1175 (** val init_mutable_jmdiscr : init_mutable -> init_mutable -> __ **)
1176 let init_mutable_jmdiscr x y =
1177 Logic.eq_rect_Type2 x
1178 (let { virtual_dptr = a0; actual_dptr = a1; built_code = a2;
1179 built_preamble = a3 } = x
1181 Obj.magic (fun _ dH -> dH __ __ __ __)) y
1183 (** val store_byte_or_Identifier :
1184 (BitVector.byte, (ASM.word_side, ASM.identifier) Types.prod) Types.sum ->
1185 init_mutable -> init_mutable **)
1186 let store_byte_or_Identifier by mut =
1187 let { virtual_dptr = virt; actual_dptr = act; built_code = acc1;
1188 built_preamble = acc2 } = mut
1191 match Identifiers.eq_identifier PreIdentifiers.ASMTag virt.Types.fst
1194 let off = Z.zminus virt.Types.snd act.Types.snd in
1195 (match Z.eqZb off Z.OZ with
1196 | Bool.True -> List.Nil
1198 (match Z.eqZb off (Z.z_of_nat (Nat.S Nat.O)) with
1200 List.Cons ({ Types.fst = Types.None; Types.snd = (ASM.Instruction
1201 (ASM.INC ASM.DPTR)) }, List.Nil)
1203 List.Cons ({ Types.fst = Types.None; Types.snd = (ASM.Mov
1204 ((Types.Inl ASM.DPTR), virt.Types.fst,
1205 (BitVectorZ.bitvector_of_Z (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1206 (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1207 (Nat.S (Nat.S (Nat.S Nat.O)))))))))))))))) virt.Types.snd))) },
1210 List.Cons ({ Types.fst = Types.None; Types.snd = (ASM.Mov ((Types.Inl
1211 ASM.DPTR), virt.Types.fst,
1212 (BitVectorZ.bitvector_of_Z (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1213 (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1214 (Nat.S Nat.O)))))))))))))))) virt.Types.snd))) }, List.Nil)
1219 { Types.fst = Types.None; Types.snd = (ASM.Instruction (ASM.MOV
1220 (Types.Inl (Types.Inl (Types.Inl (Types.Inl (Types.Inl { Types.fst =
1221 ASM.ACC_A; Types.snd = (ASM.DATA by0) }))))))) }
1222 | Types.Inr si_id ->
1223 { Types.fst = Types.None; Types.snd = (ASM.Mov ((Types.Inr
1224 { Types.fst = ASM.ACC_A; Types.snd = si_id.Types.fst }),
1226 (BitVector.zero (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1227 (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1228 Nat.O))))))))))))))))))) }
1230 { virtual_dptr = { Types.fst = virt.Types.fst; Types.snd =
1231 (Z.zsucc virt.Types.snd) }; actual_dptr = virt; built_code = (List.Cons
1232 ((List.append pre (List.Cons (post, (List.Cons ({ Types.fst = Types.None;
1233 Types.snd = (ASM.Instruction (ASM.MOVX (Types.Inr { Types.fst =
1234 ASM.EXT_INDIRECT_DPTR; Types.snd = ASM.ACC_A }))) }, List.Nil))))),
1235 acc1)); built_preamble = acc2 }
1237 (** val do_store_init_data :
1238 init_mutable Monad.smax_def__o__monad -> AST.init_data -> init_mutable
1239 Monad.smax_def__o__monad **)
1240 let do_store_init_data m_mut data =
1241 Monad.m_bind0 (Monad.smax_def State.state_monad) m_mut (fun mut ->
1242 let store_byte = fun by -> store_byte_or_Identifier (Types.Inl by) in
1243 let store_Identifier = fun side id ->
1244 store_byte_or_Identifier (Types.Inr { Types.fst = side; Types.snd =
1248 | AST.Init_int8 n ->
1249 Monad.m_return0 (Monad.smax_def State.state_monad) (store_byte n mut)
1250 | AST.Init_int16 n ->
1251 let { Types.fst = by0; Types.snd = by1 } =
1252 Vector.vsplit (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1253 (Nat.S Nat.O)))))))) (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1254 (Nat.S (Nat.S Nat.O)))))))) n
1256 Monad.m_return0 (Monad.smax_def State.state_monad)
1257 (store_byte by1 (store_byte by0 mut))
1258 | AST.Init_int32 n ->
1259 let { Types.fst = by0; Types.snd = n0 } =
1260 Vector.vsplit (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1261 (Nat.S Nat.O)))))))) (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1262 (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1263 (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1264 Nat.O)))))))))))))))))))))))) n
1266 let { Types.fst = by1; Types.snd = n1 } =
1267 Vector.vsplit (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1268 (Nat.S Nat.O)))))))) (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1269 (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1270 (Nat.S Nat.O)))))))))))))))) n0
1272 let { Types.fst = by2; Types.snd = by3 } =
1273 Vector.vsplit (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1274 (Nat.S Nat.O)))))))) (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1275 (Nat.S (Nat.S Nat.O)))))))) n1
1277 Monad.m_return0 (Monad.smax_def State.state_monad)
1279 (store_byte by2 (store_byte by1 (store_byte by0 mut))))
1280 | AST.Init_space n ->
1281 let { Types.fst = virt_id; Types.snd = virt_off } = mut.virtual_dptr
1283 Monad.m_return0 (Monad.smax_def State.state_monad) { virtual_dptr =
1284 { Types.fst = virt_id; Types.snd =
1285 (Z.zplus (Z.z_of_nat n) virt_off) }; actual_dptr = mut.actual_dptr;
1286 built_code = mut.built_code; built_preamble = mut.built_preamble }
1289 BitVector.zero (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1290 (Nat.S Nat.O))))))))
1292 Monad.m_return0 (Monad.smax_def State.state_monad)
1293 (store_byte z (store_byte z mut))
1294 | AST.Init_addrof (symb, ofs) ->
1295 Monad.m_bind0 (Monad.smax_def State.state_monad)
1296 (identifier_of_ident symb) (fun id ->
1297 Monad.m_return0 (Monad.smax_def State.state_monad)
1298 (store_Identifier ASM.HIGH id (store_Identifier ASM.LOW id mut)))))
1300 (** val do_store_global :
1301 init_mutable Monad.smax_def__o__monad -> ((AST.ident, AST.region)
1302 Types.prod, AST.init_data List.list) Types.prod -> init_mutable
1303 Monad.smax_def__o__monad **)
1304 let do_store_global m_mut id_reg_data =
1305 Monad.m_bind0 (Monad.smax_def State.state_monad) m_mut (fun mut ->
1306 let { Types.fst = eta2842; Types.snd = data } = id_reg_data in
1307 let { Types.fst = id; Types.snd = reg } = eta2842 in
1308 Monad.m_bind0 (Monad.smax_def State.state_monad) (identifier_of_ident id)
1310 let mut0 = { virtual_dptr = { Types.fst = id0; Types.snd = Z.OZ };
1311 actual_dptr = mut.actual_dptr; built_code = mut.built_code;
1312 built_preamble = (List.Cons ({ Types.fst = id0; Types.snd =
1313 (Arithmetic.bitvector_of_nat (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1314 (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1315 (Nat.S (Nat.S Nat.O))))))))))))))))
1316 (Globalenvs.size_init_data_list data)) }, mut.built_preamble)) }
1318 Util.foldl do_store_init_data
1319 (Monad.m_return0 (Monad.smax_def State.state_monad) mut0) data))
1321 (** val reversed_flatten_aux :
1322 'a1 List.list -> 'a1 List.list List.list -> 'a1 List.list **)
1323 let rec reversed_flatten_aux acc = function
1325 | List.Cons (hd, tl) -> reversed_flatten_aux (List.append hd acc) tl
1327 (** val translate_premain :
1328 LIN.lin_program -> ASM.identifier -> (ASM.labelled_instruction List.list,
1329 (ASM.identifier, BitVector.word) Types.prod List.list) Types.prod
1330 Monad.smax_def__o__monad **)
1331 let translate_premain p exit_label =
1332 Monad.m_bind0 (Monad.smax_def State.state_monad)
1333 (identifier_of_ident p.Joint.joint_prog.AST.prog_main) (fun main ->
1334 Monad.m_bind0 (Monad.smax_def State.state_monad) State.state_get
1336 let dummy_dptr = { Types.fst = Positive.One; Types.snd =
1337 (Z.zopp (Z.z_of_nat (Nat.S Nat.O))) }
1339 let mut = { virtual_dptr = dummy_dptr; actual_dptr = dummy_dptr;
1340 built_code = List.Nil; built_preamble = List.Nil }
1342 Monad.m_bind0 (Monad.smax_def State.state_monad)
1343 (Util.foldl do_store_global
1344 (Monad.m_return0 (Monad.smax_def State.state_monad) mut)
1345 p.Joint.joint_prog.AST.prog_vars) (fun globals_init ->
1346 let { Types.fst = sph; Types.snd = spl } =
1347 Vector.vsplit (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1348 (Nat.S Nat.O)))))))) (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1349 (Nat.S (Nat.S Nat.O))))))))
1350 (BitVectorZ.bitvector_of_Z
1351 (Nat.plus (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1352 (Nat.S Nat.O)))))))) (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1353 (Nat.S (Nat.S (Nat.S Nat.O)))))))))
1356 (Joint.globals_stacksize
1357 (Joint.lin_params_to_params LIN.lIN) p)))))
1359 let init_isp = ASM.DATA
1360 (Vector.append (Nat.S (Nat.S Nat.O))
1361 (Nat.plus (Nat.S (Nat.S Nat.O)) (Nat.S (Nat.S (Nat.S (Nat.S
1362 Nat.O))))) (BitVector.zero (Nat.S (Nat.S Nat.O)))
1363 (Vector.append (Nat.S (Nat.S Nat.O)) (Nat.S (Nat.S (Nat.S (Nat.S
1364 Nat.O)))) (Vector.VCons ((Nat.S Nat.O), Bool.True,
1365 (Vector.VCons (Nat.O, Bool.False, Vector.VEmpty))))
1366 (BitVector.maximum (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))))
1368 let isp_direct = ASM.DIRECT
1369 (Vector.append (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1370 Nat.O))))))) (Nat.S Nat.O) (Vector.VCons ((Nat.S (Nat.S (Nat.S
1371 (Nat.S (Nat.S (Nat.S Nat.O)))))), Bool.True,
1372 (BitVector.zero (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1373 Nat.O))))))))) (Vector.VCons (Nat.O, Bool.True,
1376 let reg_spl = ASM.REGISTER (Vector.VCons ((Nat.S (Nat.S Nat.O)),
1377 Bool.True, (Vector.VCons ((Nat.S Nat.O), Bool.True, (Vector.VCons
1378 (Nat.O, Bool.False, Vector.VEmpty))))))
1380 let reg_sph = ASM.REGISTER (Vector.VCons ((Nat.S (Nat.S Nat.O)),
1381 Bool.True, (Vector.VCons ((Nat.S Nat.O), Bool.True, (Vector.VCons
1382 (Nat.O, Bool.True, Vector.VEmpty))))))
1384 Monad.m_return0 (Monad.smax_def State.state_monad) { Types.fst =
1385 (List.append (List.Cons ({ Types.fst = Types.None; Types.snd =
1386 (ASM.Cost p.Joint.init_cost_label) }, (List.Cons ({ Types.fst =
1387 Types.None; Types.snd = (ASM.Instruction (ASM.MOV (Types.Inl
1388 (Types.Inl (Types.Inl (Types.Inr { Types.fst = isp_direct;
1389 Types.snd = init_isp })))))) }, (List.Cons ({ Types.fst =
1390 Types.None; Types.snd = (ASM.Instruction (ASM.MOV (Types.Inl
1391 (Types.Inl (Types.Inl (Types.Inl (Types.Inr { Types.fst =
1392 reg_spl; Types.snd = (ASM.DATA spl) }))))))) }, (List.Cons
1393 ({ Types.fst = Types.None; Types.snd = (ASM.Instruction (ASM.MOV
1394 (Types.Inl (Types.Inl (Types.Inl (Types.Inl (Types.Inr
1395 { Types.fst = reg_sph; Types.snd = (ASM.DATA sph) }))))))) },
1398 (reversed_flatten_aux List.Nil globals_init.built_code)
1399 (List.Cons ({ Types.fst = Types.None; Types.snd = (ASM.Call
1400 main) }, (List.Cons ({ Types.fst = (Types.Some exit_label);
1401 Types.snd = (ASM.Cost u.fresh_cost_label) }, (List.Cons
1402 ({ Types.fst = Types.None; Types.snd = (ASM.Jmp exit_label) },
1403 List.Nil)))))))); Types.snd = globals_init.built_preamble })))
1405 (** val get_symboltable :
1406 (ASM.identifier, AST.ident) Types.prod List.list Monad.smax_def__o__monad **)
1407 let get_symboltable =
1409 let imap = u.ident_map in
1410 let f = fun iold inew x -> List.Cons ({ Types.fst = inew; Types.snd =
1413 { Types.fst = u; Types.snd =
1414 (Identifiers.foldi PreIdentifiers.SymbolTag f imap List.Nil) })
1416 (** val lin_to_asm :
1417 LIN.lin_program -> ASM.pseudo_assembly_program Types.option **)
1419 State.state_run (new_ASM_universe p)
1420 (let add_translation = fun acc id_def ->
1421 Monad.m_bind0 (Monad.smax_def State.state_monad)
1422 (translate_fun_def p.Joint.jp_functions
1423 (List.map (fun x -> x.Types.fst.Types.fst)
1424 p.Joint.joint_prog.AST.prog_vars) id_def) (fun code ->
1425 Monad.m_bind0 (Monad.smax_def State.state_monad) acc (fun acc0 ->
1426 Monad.m_return0 (Monad.smax_def State.state_monad)
1427 (List.append code acc0)))
1429 Monad.m_bind0 (Monad.smax_def State.state_monad) aSM_fresh
1431 Monad.m_bind0 (Monad.smax_def State.state_monad)
1432 (Util.foldl add_translation
1433 (Monad.m_return0 (Monad.smax_def State.state_monad) List.Nil)
1434 p.Joint.joint_prog.AST.prog_funct) (fun code ->
1435 Monad.m_bind0 (Monad.smax_def State.state_monad) get_symboltable
1437 Monad.m_bind2 (Monad.smax_def State.state_monad)
1438 (translate_premain p exit_label) (fun init preamble ->
1439 Monad.m_return0 (Monad.smax_def State.state_monad)
1440 (let code0 = List.append init code in
1441 Monad.m_bind0 (Monad.max_def Option.option)
1442 (Obj.magic (ASM.code_size_opt code0)) (fun _ ->
1443 Monad.m_return0 (Monad.max_def Option.option)
1444 { ASM.preamble = preamble; ASM.code = code0;
1445 ASM.renamed_symbols = symboltable; ASM.final_label =