restauring Coq compilation with STUBS

1 files changed, 15 insertions, 2 deletions

diff --git a/aarch64/Asmgen.v b/aarch64/Asmgen.v
index f81f37d6..b0fec14b 100644
--- a/aarch64/Asmgen.v
+++ b/aarch64/Asmgen.v
@@ -16,11 +16,16 @@
 
 Require Import Recdef Coqlib Zwf Zbits.
 Require Import Errors AST Integers Floats Op.
-Require Import Locations Asmblock Asm.
+Require Import Locations Compopts.
+Require Import Mach Asm Asmblock Asmblockgen Machblockgen PseudoAsmblock PseudoAsmblockproof.
+
+
+Local Open Scope error_monad_scope.
 
 (** * Translation from Asmblock to assembly language 
-      Inspired from the KVX backend. *)
+      Inspired from the KVX backend (see kvx/Asm.v and kvx/Asmgen.v) *)
 
+Module Asmblock_TRANSF.
 (* STUB *)
 
 Definition transf_function (f: Asmblock.function) : res Asm.function :=
@@ -31,3 +36,11 @@ Definition transf_fundef (f: Asmblock.fundef) : res Asm.fundef :=
 
 Definition transf_program (p: Asmblock.program) : res Asm.program :=
   transform_partial_program transf_fundef p.
+
+End Asmblock_TRANSF.
+
+Definition transf_program (p: Mach.program) : res Asm.program :=
+  let mbp := Machblockgen.transf_program p in
+  do mbp' <- PseudoAsmblockproof.transf_program mbp;
+  do abp <- Asmblockgen.transf_program mbp';
+  Asmblock_TRANSF.transf_program abp.