include "LTL/LTL.ma".
include "LIN/LIN.ma".
include "utilities/BitVectorTrieSet.ma".
include "utilities/lists.ma".

definition translate_statement: ∀globals. ltl_statement globals → lin_statement globals ≝
  λglobals: list ident.
  λs: ltl_statement globals.
  match s with
  [ joint_st_return ⇒ joint_st_return …
  | joint_st_sequential instr lbl ⇒ joint_st_sequential … instr it
  | joint_st_goto l ⇒ joint_st_goto … l
  | joint_st_extension ext ⇒ joint_st_extension lin_params … ext
  ].

(* Invariant: l has not been visited yet the very first time the
   function is called and in the true branch of a conditional call.
   This avoid useless gotos.
   
   Note: the OCaml code contains some useful explanatory comments. *)
let rec visit
  (globals: list ident) (g: label → option (ltl_statement globals))
  (required: BitVectorTrieSet 16) (visited: BitVectorTrieSet 16)
  (generated: list ((option label) × (lin_statement globals))) (l: label) (n: nat)
    on n: BitVectorTrieSet 16 × (list ((option label) × (lin_statement globals))) ≝
  match n with
  [ O ⇒ ⊥ (* CSC: Case to be made impossible; use dummy value? *)
  | S n' ⇒
    if set_member … (word_of_identifier … l) visited then
     〈set_insert ? (word_of_identifier ? l) required, 〈None …, joint_st_goto … globals l〉 :: generated〉
    else
     let visited' ≝ set_insert ? (word_of_identifier ? l) visited in
     match g (an_identifier LabelTag (word_of_identifier … l)) with
     [ None ⇒ ⊥ (* Case to be made impossible with more dependent types *)
     | Some statement ⇒
       let translated_statement ≝ translate_statement globals statement in
       let generated' ≝ 〈Some … l, translated_statement〉 :: generated in
       match statement with
       [ joint_st_sequential instr l2 ⇒
         match instr with
         [ joint_instr_cond acc_a_reg l1 ⇒
            let 〈required', generated''〉 ≝
             visit globals g required visited' generated' l2 n' in
            let required'' ≝ set_insert ? (word_of_identifier ? l1) required' in
             if set_member … (word_of_identifier … l1) visited' then
               〈required', generated''〉
             else
               visit globals g required'' visited' generated'' l1 n'
         | _ ⇒ visit globals g required visited' generated' l2 n']
     | joint_st_return ⇒ 〈required, generated'〉
     | joint_st_goto l2 ⇒ visit globals g required visited' generated' l2 n'
     | joint_st_extension ext ⇒ ⊥ ]]].
[3: @ext
|1,2: @daemon (*CSC: impossible cases, use more dependent types *) ]
qed.

(* CSC: The branch compression (aka tunneling) optimization is not implemented
   in Matita *)
definition branch_compress ≝ λglobals.λa:label → option (ltl_statement globals).a.

definition translate_graph:
 ∀globals. label → nat →
  (label → option (ltl_statement globals)) → (label → option (lin_statement globals))
≝
 λglobals,entry,labels_upper_bound,g.
  let g ≝ branch_compress ? g in
  let visited ≝ set_empty ? in
  let required ≝ set_insert ? (word_of_identifier … entry) (set_empty ?) in
  let 〈required', translated〉 ≝ visit globals g required visited [ ] entry labels_upper_bound in
  let reversed ≝ rev ? translated in
  let final ≝
   map ??
    (λs. let 〈l,x〉 ≝ s in
      match l with
       [ None ⇒ 〈None …,x〉
       | Some l ⇒
          〈if set_member … (word_of_identifier … l) required' then Some ? l else None ?,
           x〉])
    reversed in
  λl.
   find ?? (λs. let 〈l',x〉 ≝ s in
    match l' with [ None ⇒ None … | Some l'' ⇒ if eq_identifier … l l'' then Some … x else None ?]) final.

definition translate_int_fun:
 ∀globals.
  joint_internal_function ltl_params globals →
   joint_internal_function lin_params globals
≝
 λglobals,f.
  mk_joint_internal_function lin_params globals
   (joint_if_luniverse ?? f) (joint_if_runiverse ?? f) it it it (joint_if_stacksize ?? f)
    (translate_graph globals (joint_if_entry ?? f) (nat_of_bitvector … (next_identifier … (joint_if_luniverse … f)))
     (joint_if_lookup ?? f))
    ??.
cases daemon (*CSC: XXXXXXXXX Dead code produced *)
qed.

definition ltl_to_lin : ltl_program → lin_program ≝
 λp. transform_program … p (transf_fundef … (translate_int_fun …)).