1 files changed, 12 insertions, 1 deletions
diff --git a/mppa_k1c/Asmgen.v b/mppa_k1c/Asmgen.v
index 7b753506..15892818 100644
--- a/mppa_k1c/Asmgen.v
+++ b/mppa_k1c/Asmgen.v
@@ -23,4 +23,15 @@ Local Open Scope error_monad_scope.
 Definition transf_program (p: Mach.program) : res Asm.program :=
   let mbp := Machblockgen.transf_program p in
   do abp <- Asmblockgen.transf_program mbp;
-  OK (Asm.transf_program abp).
-\ No newline at end of file
+  OK (Asm.transf_program abp).
+
+Definition transf_function (f: Mach.function) : res function :=
+  let mbf := Machblockgen.transf_function f in
+  do abf <- Asmblockgen.transf_function mbf;
+  OK (Asm.transf_function abf).
+
+Definition transl_code (f: Mach.function) (l: Mach.code) : res (list instruction) :=
+  let mbf := Machblockgen.transf_function f in
+  let mbc := Machblockgen.trans_code l in
+  do abc <- transl_blocks mbf mbc;
+  OK (unfold abc).
+\ No newline at end of file