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

axiom LTLTag: String.

definition translate_statement: ∀globals. LTLStatement globals → PreLINStatement globals ≝
  λglobals: list Identifier.
  λs: LTLStatement globals.
    match s with
    [ Joint_St_Return ⇒ Joint_St_Return ? globals
    | Joint_St_Sequential instr _ ⇒ Joint_St_Sequential ? globals instr it
    | Joint_St_Goto lbl ⇒ Joint_St_Goto ? globals lbl
    ].
    
definition require: Identifier → BitVectorTrieSet 16 → BitVectorTrieSet 16 ≝
  λl: Identifier.
  λg: BitVectorTrieSet 16.
    set_insert ? l g.
    
definition mark: Identifier → BitVectorTrieSet 16 → BitVectorTrieSet 16 ≝
  λl: Identifier.
  λg: BitVectorTrieSet 16.
    set_insert ? l g.
    
definition marked: Identifier → BitVectorTrieSet 16 → bool ≝
  λl: Identifier.
  λg: BitVectorTrieSet 16.
    set_member ? l g.
    
definition graph_lookup ≝
  λglobals.
  λl: Identifier.
  λg: LTLStatementGraph globals.
    lookup LabelTag (LTLStatement globals) g (an_identifier LabelTag l).
    
definition fetch: ∀globals: list Identifier. Identifier → LTLStatementGraph globals → option (LTLStatement globals) ≝
  λglobals: list Identifier.
  λl: Identifier.
  λg: LTLStatementGraph globals.
    graph_lookup globals l g.

definition foo ≝
  λl2, visited, required, globals, generated, g, n.
  λvisit:
  ∀globals: list Identifier.
  ∀g: LTLStatementGraph globals.
  ∀required: BitVectorTrieSet 16.
  ∀visited: BitVectorTrieSet 16.
  ∀generated: list (PreLINStatement globals).
  ∀l: Identifier.
  ∀n: nat.
    BitVectorTrieSet 16 × (list (PreLINStatement globals)).
  if marked l2 visited then
    〈require l2 required, (Joint_St_Goto ? globals l2) :: generated〉
  else
   visit globals g required visited generated l2 n.

let rec visit (globals: list Identifier) (g: LTLStatementGraph globals)
              (required: BitVectorTrieSet 16) (visited: BitVectorTrieSet 16)
              (generated: list (PreLINStatement globals)) (l: Identifier) (n: nat) on n: BitVectorTrieSet 16 × (list (PreLINStatement 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_CondAcc 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_Goto lbl ⇒
        let required' ≝
          if marked lbl visited' then
            require lbl required
          else
            required in
        if marked lbl visited' then
          〈required', (Joint_St_Goto ? globals lbl) :: generated''〉
        else
          visit globals g required' visited' generated'' lbl n'
      | Joint_St_Return ⇒ 〈required, generated''〉 (* dpm: correct? *)
      ]
    ]
  ].

(*
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.
*)