(* Front-end related includes *)
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".

(* Back-end related includes *)
include "RTLabs/RTLabsToRTL.ma". 
include "RTL/RTLToERTL.ma".
include "ERTL/ERTLToERTLptr.ma".
include "ERTLptr/ERTLptrToLTL.ma".
include "LTL/LTLToLIN.ma". 
include "LIN/LINToASM.ma".

(* List of all passes whose outputs can be observed *)
inductive pass : Type[0] ≝
   clight_pass: pass
 | clight_switch_removed_pass: pass
 | clight_label_pass: pass
 | clight_simplified_pass: pass
 | cminor_pass: pass
 | rtlabs_pass: pass
 | rtl_separate_pass: pass
 | rtl_uniq_pass: pass
 | ertl_pass: pass
 | ertlptr_pass: pass
 | ltl_pass: pass
 | lin_pass: pass
 | assembly_pass: pass
 | object_code_pass: pass.

definition with_stack_model : Type[0] → Type[0] ≝
 λA:Type[0].A × (ident → option ℕ).

definition syntax_of_pass : pass → Type[0] ≝
 λpass.
  match pass with
  [ clight_pass ⇒ clight_program
  | clight_switch_removed_pass ⇒ clight_program
  | clight_label_pass ⇒ clight_program
  | clight_simplified_pass ⇒ clight_program
  | cminor_pass ⇒ Cminor_program
  | rtlabs_pass ⇒ RTLabs_program
  | rtl_separate_pass ⇒ with_stack_model rtl_program
  | rtl_uniq_pass ⇒ with_stack_model rtl_program
  | ertl_pass ⇒ with_stack_model ertl_program
  | ertlptr_pass ⇒ with_stack_model ertlptr_program
  | ltl_pass ⇒ with_stack_model ltl_program
  | lin_pass ⇒ with_stack_model lin_program
  | assembly_pass ⇒
     pseudo_assembly_program × (Word → Word) × (Word → bool)
  | object_code_pass ⇒ labelled_object_code ].

definition observe_pass ≝ ∀pass. syntax_of_pass pass → unit.

(* The compiler front-end *)
definition front_end :
 observe_pass → clight_program → res (costlabel × clight_program × RTLabs_program) ≝
λobserve,p.
  let i ≝ observe clight_pass p in
  let p ≝ program_switch_removal p in
  let i ≝ observe clight_switch_removed_pass p in
  let 〈p',init_cost〉 ≝ clight_label p in
  let i ≝ observe clight_label_pass p' in
  let p ≝ simplify_program p' in
  let i ≝ observe clight_simplified_pass p in
  ! p ← clight_to_cminor p;
  let i ≝ observe cminor_pass p in
  let p ≝ cminor_to_rtlabs p in
  let i ≝ observe rtlabs_pass 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)).

(* The compiler back-end *)
include "ERTLptr/uses.ma".  (* Included by the untrusted code *)
axiom compute_fixpoint : fixpoint_computer.
axiom colour_graph : coloured_graph_computer.

include "common/AssocList.ma".

(* Inefficient, replace with Trie lookup *)
definition lookup_stack_cost ≝
 λP,p,id.
  assoc_list_lookup ?? id (eq_identifier …) (stack_cost P p).

definition back_end :
 observe_pass → costlabel → RTLabs_program →
  res (pseudo_assembly_program × stack_cost_model × nat) ≝
λobserve,init_cost,p.
  let p ≝ rtlabs_to_rtl init_cost p in
  let st ≝ lookup_stack_cost … p in
  let i ≝ observe rtl_separate_pass 〈p,st〉 in
  let i ≝ observe rtl_uniq_pass 〈p,st〉 in
  let p ≝ rtl_to_ertl p in
  let st ≝ lookup_stack_cost … p in  
  let i ≝ observe ertl_pass 〈p,st〉 in
  let p ≝ ertl_to_ertlptr p in
  let st ≝ lookup_stack_cost … p in  
  let i ≝ observe ertlptr_pass 〈p,st〉 in
  let 〈p,stack_cost,max_stack〉 ≝ ertlptr_to_ltl compute_fixpoint colour_graph p in
  (* The two stack models are the same *)
  let st ≝ lookup_stack_cost … p in
  let i ≝ observe ltl_pass 〈p,st〉 in
  let st ≝ lookup_stack_cost … p in
  let p ≝ ltl_to_lin p in
  let st ≝ lookup_stack_cost … p in
  let i ≝ observe lin_pass 〈p,st〉 in
   ! p ← opt_to_res ? (msg AssemblyTooLarge) (lin_to_asm p) ;
   return 〈p,stack_cost,max_stack〉.

(* The assembler *)
include "ASM/Policy.ma".

definition assembler :
 observe_pass → pseudo_assembly_program → res labelled_object_code ≝
λobserve,p.
  ! 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
  let i ≝ observe assembly_pass 〈p,sigma,pol〉 in
  let p ≝ assembly p sigma pol in
  let i ≝ observe object_code_pass p in
  OK ? p.

(* Cost lifting *)
include "ASM/ASMCosts.ma". 

definition lift_cost_map_back_to_front :
  ∀clight, oc.
    let abstat ≝ OC_abstract_status oc in 
  as_cost_map abstat → clight_cost_map clight ≝ 
  λclight,oc,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.

(* Cost model computation *)
include "ASM/ASMCostsSplit.ma".

record compiler_output : Type[0] ≝
 { c_labelled_object_code: labelled_object_code
 ; c_stack_cost: stack_cost_model
 ; c_max_stack: nat
 ; c_labelled_clight: clight_program
 ; c_clight_cost_map: clight_cost_map c_labelled_clight
 }.

definition compile : observe_pass → clight_program → res compiler_output ≝ 
λobserve,p.
  ! 〈init_cost,p',p〉 ← front_end observe p;
  ! 〈p,stack_cost,max_stack〉 ← back_end observe init_cost p;
  ! p ← assembler observe p;
  let k ≝ ASM_cost_map p in
  let k' ≝
   lift_cost_map_back_to_front p' p k in
  return mk_compiler_output p stack_cost max_stack p' k'.