include "Clight/label.ma".
include "Clight/SimplifyCasts.ma".
include "Clight/switchRemoval.ma".
include "Clight/toCminor.ma".
include "Cminor/initialisation.ma".
include "Cminor/toRTLabs.ma".

definition front_end : clight_program → res (costlabel × clight_program × RTLabs_program) ≝
λp.
  let p ≝ program_switch_removal p in
  let 〈p',init_cost〉 ≝ clight_label p in
  let p ≝ simplify_program p' in
  ! p ← clight_to_cminor p;
  let p ≝ cminor_to_rtlabs init_cost p in
  return 〈init_cost,p',p〉.

include "RTLabs/RTLabsToRTL.ma". 
include "RTL/RTLToERTL.ma".
include "ERTL/ERTLToLTL.ma".
(*
include "LTL/LTLToLIN.ma".
include "LIN/LINToASM.ma".
*) include "ASM/ASM.ma". include "LIN/LIN.ma".
   axiom ltl_to_lin: ltl_program → lin_program.
   axiom lin_to_asm: lin_program → pseudo_assembly_program.

(* these are already defined in utilities/fixpoint.ma and ERTL/Interference.ma
axiom the_fixpoint : fixpoint.
axiom build : ∀valuation. coloured_graph valuation.
*)

definition back_end : RTLabs_program → pseudo_assembly_program ≝
λp.
  let p ≝ rtlabs_to_rtl p in
  let p ≝ rtl_to_ertl p in
  let p ≝ ertl_to_ltl p in  (* TODO: abstract over colouring *)
  let p ≝ ltl_to_lin p in
          lin_to_asm p.

(* JHM: minimum needed for assembler axiom to typecheck *)
(* JHM: moved from ASMCostsSplit.ma                     *)
(* JHM: should move elsewhere in ASM/                   *)
definition object_code ≝ list Byte. 
definition costlabel_map ≝ BitVectorTrie costlabel 16. 

axiom assembler : pseudo_assembly_program → res (object_code × costlabel_map). 

(* include "ASM/Policy.ma".

definition assembler : pseudo_assembly_program → res (object_code × costlabel_map) ≝
λp.
  let 〈preamble, list_instr〉 ≝ p in
  (* TODO: fail if p is too large. *)
  let p' ≝ 〈preamble, list_instr〉 in
  ! sigma_pol ← opt_to_res ? (msg Jump_expansion_failed) (jump_expansion' p');
  let sigma ≝ λppc. \fst (sigma_pol ppc) in
  let pol ≝ λppc. \snd (sigma_pol ppc) in
  OK ? (assembly p sigma pol).
cases daemon
qed.
*)

include "ASM/ASMCosts.ma". 

definition lift_cost_map_back_to_front :
  ∀clight, code_memory, lbls.
    let abstat ≝ ASM_abstract_status code_memory lbls in 
   (∀l. (as_cost_labelled abstat l) + ¬(as_cost_labelled abstat l)) →
  as_cost_map abstat → clight_cost_map clight ≝ 
  λclight,code_memory,lbls,dec,k,asm_cost_map.
  lift_sigma_map_id … 0 (* labels not present in out code get 0 *)
    dec k asm_cost_map.

include "ASM/ASMCostsSplit.ma". 

definition compile : clight_program →
  res (object_code × costlabel_map × (𝚺labelled:clight_program. clight_cost_map labelled)) ≝ 
λp.
  ! 〈init_cost,p',p〉 ← front_end p;
  let p ≝ back_end p in
    ! p ← assembler p;
  let k ≝ ASM_cost_map p ? in
  let k' ≝ lift_cost_map_back_to_front
    p'
    (load_code_memory (\fst p))
    (\snd p)
    ? k
    in
  return 〈p, ❬p', k'❭〉.
  cases daemon
  qed.