Library mcertikos.layerlib.LAsmgen

This file provides the compiler from CompCertX AsmX (in fact, syntactically, from CompCert Asm) to the LAsm instructions.

Require AST.

Require Asm.
Require LAsm.

Definition transf_code: ∀ (c: Asm.code), LAsm.code :=
  List.map LAsm.asm_instruction.

Definition transf_function (f: Asm.function): LAsm.function :=
  {|
    LAsm.fn_sig := Asm.fn_sig f ;
    LAsm.fn_code := transf_code (Asm.fn_code f )
  |}.

Definition transf_fundef := AST.transf_fundef transf_function.

Definition transf_program:
  Asm.program → LAsm.program
:= AST.transform_program transf_fundef.