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

axiom LTLTag: String.

definition translate_statement: ∀globals. ltl_statement globals → pre_lin_statement globals ≝
  λglobals: list ident.
  λs: ltl_statement globals.
  match s with
  [ joint_st_return ⇒ joint_st_return lin_params globals
  | joint_st_sequential instr lbl ⇒ joint_st_sequential lin_params globals instr lbl
  | joint_st_goto l ⇒ joint_st_goto lin_params globals l
  | joint_st_extension ext ⇒ joint_st_extension lin_params globals ext
  ].
    
definition require: label → BitVectorTrieSet 16 → BitVectorTrieSet 16 ≝
  λl: label.
  λg: BitVectorTrieSet 16.
    set_insert ? (word_of_identifier ? l) g.
    
definition mark: label → BitVectorTrieSet 16 → BitVectorTrieSet 16 ≝
  λl: label.
  λg: BitVectorTrieSet 16.
    set_insert ? (word_of_identifier ? l) g.
    
definition marked: label → BitVectorTrieSet 16 → bool ≝
  λl: label.
  λg: BitVectorTrieSet 16.
    set_member ? (word_of_identifier ? l) g.
    
(* alias id "lookupn" = "cic:/matita/cerco/common/Identifiers/lookup.def(3)". *)
    
definition graph_lookup ≝
  λglobals: list ident.
  λl: label.
  λgr: ltl_statement_graph globals.
    lookup LabelTag ? gr (an_identifier LabelTag (word_of_identifier ? l)).
    
definition fetch: ∀globals: list ident. label → ltl_statement_graph globals → option (ltl_statement globals) ≝
  λglobals: list ident.
  λl: label.
  λg: ltl_statement_graph globals.
    graph_lookup globals l g.

definition foo ≝
  λl2, visited, required, globals, generated, g, n.
  λvisit:
  ∀globals: list ident.
  ∀g: ltl_statement_graph globals.
  ∀required: BitVectorTrieSet 16.
  ∀visited: BitVectorTrieSet 16.
  ∀generated: list (pre_lin_statement globals).
  ∀l: label.
  ∀n: nat.
    BitVectorTrieSet 16 × (list (pre_lin_statement globals)).
  if marked l2 visited then
    〈require l2 required, (joint_st_goto … globals l2) :: generated〉
  else
   visit globals g required visited generated l2 n.

(* XXX: look at this.  way too complicated to understand whether it is correct,
   in my opinion.
*)
let rec visit
  (globals: list ident) (g: ltl_statement_graph globals)
  (required: BitVectorTrieSet 16) (visited: BitVectorTrieSet 16)
  (generated: list (pre_lin_statement globals)) (l: label) (n: nat)
    on n: BitVectorTrieSet 16 × (list (pre_lin_statement globals)) ≝
  match n with
  [ O ⇒ 〈required, generated〉
  | S n' ⇒
    let visited' ≝ mark l visited in
    match fetch globals l g with
    [ None ⇒ 〈required, generated〉 (* dpm: correct? *)
    | Some statement ⇒
      let translated_statement ≝ translate_statement globals statement in
      let generated'' ≝ translated_statement :: generated in
      match statement with
      [ joint_st_sequential instr l2 ⇒
        match instr with
        [ joint_instr_cond acc_a_reg l1 ⇒
              let required' ≝
                if marked l2 visited' then
                  require l2 required
                else
                  required in
              let 〈required', generated''〉 ≝
               foo l2 visited' required' globals generated'' g n' visit (*
                if marked l2 visited' then
                  〈required', (Joint_St_Goto ? globals l2) :: generated''〉
                else
                  visit globals g required' visited' generated'' l2 n'*) in
              let required'' ≝ require l1 required' in
                if ¬(marked l1 visited') then
                  visit globals g required'' visited' generated'' l1 n'
                else
                  〈required', generated''〉
          | _ ⇒
            let required' ≝
              if marked l2 visited' then
                require l2 required
              else
                required in
            if marked l2 visited' then
              〈required', joint_st_goto … globals l2 :: generated''〉
            else
              visit globals g required' visited' generated'' l2 n'
          ]
    | joint_st_return ⇒ 〈required, generated''〉 (* dpm: correct? *)
    | joint_st_goto l ⇒
      let required' ≝
        if marked l visited' then
         require l required
        else
         required
      in
        if marked l visited' then
          〈required', joint_st_goto … globals l :: generated''〉
        else
          visit globals g required' visited' generated'' l n'
    | joint_st_extension ext ⇒ 〈required, generated〉
    ]
  ]
].

(*
definition translate_graph ≝
  λglobals: list Identifier.
  λg: LTLStatementGraph globals.
  λentry: Identifier.
    let visited ≝ set_empty ? in
    let required ≝ set_insert ? entry (set_empty ?) in
    let 〈required', translated〉 ≝ visit globals g required visited [ ] entry in
    let reversed ≝ rev ? translated in
      filter (λs: PreLINStatement globals. ?) reversed.
*)