include "Clight/label.ma".
include "Clight/SimplifyCasts.ma".
include "Clight/switchRemoval.ma".
include "Clight/toCminor.ma".
include "Cminor/toRTLabs.ma".
include "RTLabs/CostCheck.ma".
include "RTLabs/CostInj.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
  if check_cost_program p then
    if check_program_cost_injectivity p then
      (return 〈init_cost,p',p〉)
    else
      (Error ? (msg RepeatedCostLabel))
  else
    (Error ? (msg BadCostLabelling)).

include "RTLabs/RTLabsToRTL.ma". 
include "RTL/RTLToERTL.ma".
include "ERTL/ERTLToERTLptr.ma".
include "ERTLptr/ERTLptrToLTL.ma".
include "LTL/LTLToLIN.ma".
include "LIN/LINToASM.ma".

axiom compute_fixpoint : fixpoint_computer.
axiom colour_graph : coloured_graph_computer.

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_ertlptr p in
  let p ≝ ertlptr_to_ltl compute_fixpoint colour_graph p in (* TODO: abstract over colouring *)
  let p ≝ ltl_to_lin p in
          lin_to_asm p.

include "ASM/Policy.ma".
(* Equivalent to the inclusion of ASM/Policy.ma, waiting for that slow
   file to compile
  include "ASM/PolicyStep.ma".
  axiom jump_expansion': ∀program:preamble × (Σl:list labelled_instruction.lt (S (|l|)) 2^16 ∧ is_well_labelled_p l).
 option (Σsigma_policy:(Word → Word) × (Word → bool).
   let 〈sigma,policy〉≝ sigma_policy in
   sigma_policy_specification 〈\fst program,\snd program〉 sigma policy). *)
   
definition assembler : pseudo_assembly_program → res labelled_object_code ≝
λp.
(*  ! list_instr_ok ← opt_to_res ? (msg AssemblyTooLarge) ?(*(program_ok_opt ? list_instr)*); *)
  ! 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).

include "ASM/ASMCosts.ma". 

(*CSC: move the next definitions, e.g. in BitVectorTrie *)
definition in_codomain: ∀A:Type[0].∀n:nat. BitVectorTrie A n → A → Prop ≝
 λA,n,m,a. ∃k:BitVector n. lookup_opt … k m = Some … a.

definition strong_decidable: Prop → Type[0] ≝
 λP:Prop. P + ¬ P.

lemma strong_decidable_in_codomain:
 ∀A:DeqSet.∀n:nat.∀m: BitVectorTrie A n.∀a:A.
  strong_decidable (in_codomain A n m a).
 #A #n #m elim m
 [ normalize #a' #a inversion (a' == a) #H
   [ %1 %{(VEmpty …)} >(\P H) %
   | %2 % * #_ #EQ destruct lapply (\Pf H) /2/ ]
 | -n #n #L #R #Hl #Hr #a
   cases (Hl a) -Hl [#K %1 cases K #k #H %{(false:::k)} <H % ] #Hl
   cases (Hr a) -Hr [#K %1 cases K #k #H %{(true:::k)}  <H % ] #Hr
   %2 % * #k cases (BitVector_Sn … k) ** #tl #EQ >EQ whd in ⊢ (??%? → ?);
   normalize nodelta whd in match (tail ???); #abs [ cases Hr | cases Hl ] /3/
 | #n #A %2 % * #x normalize #abs destruct ]
qed.

(* can now move this defn to ASM/ASMCosts.ma *)
definition lift_cost_map_back_to_front :
  ∀clight, code_memory, lbls.
    let abstat ≝ ASM_abstract_status code_memory lbls in 
  as_cost_map abstat → clight_cost_map clight ≝ 
  λclight,code_memory,lbls,k,asm_cost_map.
  lift_sigma_map_id … 0 (* labels not present in out code get 0 *)
    (strong_decidable_in_codomain …) k asm_cost_map.

include "ASM/ASMCostsSplit.ma". 

definition compile : clight_program →
  res (labelled_object_code × (𝚺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 (oc p)) (costlabels p) k in
  return 〈p, ❬p', k'❭〉.