include "LTL/LTL.ma".
include "LIN/LIN.ma".
include "utilities/BitVectorTrieSet.ma".
include alias "common/Graphs.ma".

definition translate_statement: ∀globals. ltl_statement globals → pre_lin_statement globals ≝
  λglobals: list ident.
  λs: ltl_statement globals.
  match s with
  [ RETURN ⇒ RETURN ??
  | sequential instr lbl ⇒ sequential … instr it
  | GOTO l ⇒ GOTO lin_params_ globals l
  ].

(* 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: identifier_set LabelTag) (visited: identifier_set LabelTag)
  (generated: list (lin_statement globals)) (l: label) (n: nat)
    on n: identifier_set LabelTag × (list (lin_statement globals)) ≝
  match n with
  [ O ⇒ ⊥ (* CSC: Case to be made impossible; use dummy value? *)
  | S n' ⇒
    if mem_set … visited l then
     〈add_set ? required l, 〈None …, GOTO … globals l〉 :: generated〉
    else
     let visited' ≝ add_set ? visited l in
     match g 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
       [ sequential instr l2 ⇒
         match instr with
         [ COND acc_a_reg l1 ⇒
            let 〈required', generated''〉 ≝
             visit globals g required visited' generated' l2 n' in
            let required'' ≝ add_set ? required' l1 in
             if mem_set … visited' l1 then
               〈required', generated''〉
             else
               visit globals g required'' visited' generated'' l1 n'
         | _ ⇒ visit globals g required visited' generated' l2 n']
     | RETURN ⇒ 〈required, generated'〉
     | GOTO l2 ⇒ visit globals g required visited' generated' l2 n']]].
[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)) → codeT … (lin_params globals)
≝
 λglobals,entry,labels_upper_bound,g.
  let g ≝ branch_compress ? g in
  let visited ≝ ∅ in
  let required ≝ { (entry) } in
  let 〈required', translated〉 ≝ visit globals g required visited [ ] entry labels_upper_bound in
  let reversed ≝ rev ? translated in
   map ??
    (λs. let 〈l,x〉 ≝ s in
      match l with
       [ None ⇒ 〈None …,x〉
       | Some l ⇒
          〈if mem_set … required' l then Some ? l else None ?,
           x〉])
    reversed.

definition translate_int_fun:
 ∀globals.
  joint_internal_function … (ltl_params globals) →
   joint_internal_function … (lin_params globals)
≝
 λglobals,f.
  mk_joint_internal_function globals (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_pos … (next_identifier … (joint_if_luniverse … f)))
     (lookup ?? (joint_if_code … 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 …)).