(* *************************************************************)
(*                                                             *)
(*             The Compcert verified compiler                  *)
(*                                                             *)
(*           Sylvain Boulmé     Grenoble-INP, VERIMAG          *)
(*           Justus Fasse       UGA, VERIMAG                   *)
(*           Xavier Leroy       INRIA Paris-Rocquencourt       *)
(*           David Monniaux     CNRS, VERIMAG                  *)
(*           Cyril Six          Kalray                         *)
(*                                                             *)
(*  Copyright Kalray. Copyright VERIMAG. All rights reserved.  *)
(*  This file is distributed under the terms of the INRIA      *)
(*  Non-Commercial License Agreement.                          *)
(*                                                             *)
(* *************************************************************)

Require Import Recdef Coqlib Zwf Zbits.
Require Import Errors AST Integers Floats Op.
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 (see kvx/Asm.v and kvx/Asmgen.v) *)

Module Asmblock_TRANSF.
(* STUB *)

Definition transf_function (f: Asmblock.function) : res Asm.function :=
  Error (msg "Asmgen not yet implmented").

Definition transf_fundef (f: Asmblock.fundef) : res Asm.fundef :=
  transf_partial_fundef transf_function f.

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.