include "joint/Joint_paolo.ma".
include "joint/blocks.ma".

(* general type of functions generating fresh things *)
(* type T is the syntactic type of the generated things *)
(* (sig for RTLabs registers, unit in others ) *)
definition freshT ≝ λg.λpars : params.state_monad (joint_internal_function … g pars).

definition rtl_ertl_fresh_reg: 
 ∀inst_pars,funct_pars,globals.
  freshT globals (rtl_ertl_params inst_pars funct_pars) register ≝
  λinst_pars,var_pars,globals,def.
    let 〈r, runiverse〉 ≝ fresh … (joint_if_runiverse … def) in
    〈set_locals ?? (set_runiverse ?? def runiverse)(r::joint_if_locals ?? def), r〉.

include alias "basics/lists/list.ma".
let rec rtl_ertl_fresh_regs inst_pars funct_pars globals (n : ℕ) on n :
  freshT globals (rtl_ertl_params inst_pars funct_pars)
    (Σl : list register. |l| = n) ≝
  let ret_type ≝ (Σl : list register. |l| = n) in
  match n  return λx.x = n → freshT … ret_type with
  [ O ⇒ λeq'.return (mk_Sig … [ ] ?)
  | S n' ⇒ λeq'.
    ! regs' ← rtl_ertl_fresh_regs inst_pars funct_pars globals n';
    ! reg ← rtl_ertl_fresh_reg inst_pars funct_pars globals;
    return (mk_Sig … (reg :: regs') ?)
  ](refl …). <eq' normalize [//] elim regs' #l #eql >eql //
  qed.

definition fresh_label:
 ∀g_pars,globals.freshT globals g_pars label ≝
  λg_pars,globals,def.
    let 〈r,luniverse〉 ≝ fresh … (joint_if_luniverse … def) in
     〈set_luniverse … def luniverse, r〉.

(* insert into a graph a block of instructions *)
let rec adds_graph_list
  (g_pars: graph_params)
  (globals: list ident)
  (insts: list (joint_seq g_pars globals))
  (src : label)
  (def: joint_internal_function … g_pars) on insts 
  : (joint_internal_function … g_pars) × label ≝
  match insts with
  [ nil ⇒ 〈def, src〉
  | cons instr others ⇒
    let 〈def, mid〉 ≝ fresh_label … def in
    let def ≝ add_graph … src (sequential … instr mid) def in
    adds_graph_list g_pars globals others mid def
  ].

definition adds_graph :
  ∀g_pars : graph_params.
  ∀globals: list ident.
  ∀b : seq_block g_pars globals (joint_step g_pars globals) +
       seq_block g_pars globals (joint_fin_step g_pars).
  label → if is_inl … b then label else unit →
  joint_internal_function … g_pars → joint_internal_function … g_pars ≝
  λg_pars,globals,insts,src.
  match insts return λx.if is_inl … x then ? else ? → ? → ? with
  [ inl b ⇒ λdst,def.
    let 〈def, mid〉 ≝ adds_graph_list … (\fst b) src def in
    add_graph … mid (sequential … (\snd b) dst) def
  | inr b ⇒ λdst,def.
    let 〈def, mid〉 ≝ adds_graph_list … (\fst b) src def in
    add_graph … mid (final … (\snd b)) def
  ].

definition b_adds_graph :
  ∀g_pars: graph_params.
  ∀globals: list ident.
  (* fresh register creation *)
  freshT globals g_pars (localsT … g_pars) →
  ∀b : bind_seq_block g_pars globals (joint_step g_pars globals) +
       bind_seq_block g_pars globals (joint_fin_step g_pars).
  label → if is_inl … b then label else unit →
  joint_internal_function globals g_pars →
  joint_internal_function globals g_pars ≝
  λg_pars,globals,fresh_r,insts,src.
  match insts return λx.if is_inl … x then ? else ? → ? → ? with
  [ inl b ⇒ λdst,def.
    let 〈def, stmts〉 ≝ bcompile ??? fresh_r b def in
    adds_graph … (inl … stmts) src dst def
  | inr b ⇒ λdst,def.
    let 〈def, stmts〉 ≝ bcompile ??? fresh_r b def in
    adds_graph … (inr … stmts) src dst def
  ].

(* translation with inline fresh register allocation *)
definition b_graph_translate :
  ∀src_g_pars,dst_g_pars : graph_params.
  ∀globals: list ident.
  (* fresh register creation *)
  freshT globals dst_g_pars (localsT dst_g_pars) →
  (* initialized function definition with empty graph *)
  joint_internal_function globals dst_g_pars →
  (* functions dictating the translation *)
  (label → joint_step src_g_pars globals →
    bind_seq_block dst_g_pars globals (joint_step dst_g_pars globals)) →
  (label → joint_fin_step src_g_pars →
    bind_seq_block dst_g_pars globals (joint_fin_step dst_g_pars)) →
  (* source function *)
  joint_internal_function globals src_g_pars →
  (* destination function *)
  joint_internal_function globals dst_g_pars ≝
  λsrc_g_pars,dst_g_pars,globals,fresh_reg,empty,trans_step,trans_fin_step,def.
  let f : label → joint_statement (src_g_pars : params) globals →
    joint_internal_function globals dst_g_pars → joint_internal_function globals dst_g_pars ≝ 
    λlbl,stmt,def.
    match stmt with
    [ sequential inst next ⇒
      b_adds_graph … fresh_reg (inl … (trans_step lbl inst)) lbl next def
    | final inst ⇒
      b_adds_graph … fresh_reg (inr … (trans_fin_step lbl inst)) lbl it def
    ] in
  foldi … f (joint_if_code … def) empty.
(*  
(* translation without register allocation *)
definition graph_translate :
  ∀src_g_pars,dst_g_pars : graph_params.
  ∀globals: list ident.
  (* function dictating the translation *)
  (label → joint_step src_g_pars globals →
    list (joint_step dst_g_pars globals)) →
  (label → ext_fin_stmt src_g_pars →
    (list (joint_step dst_g_pars globals))
    ×
    (joint_statement dst_g_pars globals)) →
  (* initialized function definition with empty graph *)
  joint_internal_function … dst_g_pars →
  (* source function *)
  joint_internal_function … src_g_pars →
  (* destination function *)
  joint_internal_function … dst_g_pars ≝ 
  λsrc_g_pars,dst_g_pars,globals,trans,trans',empty,def.
  let f : label → joint_statement (src_g_pars : params) globals →
    joint_internal_function … dst_g_pars → joint_internal_function … dst_g_pars ≝ 
    λlbl,stmt,def.
    match stmt with
    [ sequential inst next ⇒
      adds_graph dst_g_pars globals (trans lbl inst) lbl next def
    | GOTO next ⇒ add_graph … lbl (GOTO … next) def
    | RETURN ⇒ add_graph … lbl (RETURN …) def
    | extension_fin c ⇒ let 〈l, fin〉 ≝ trans' lbl c in
      let 〈def, tmp_lbl〉 ≝ fresh_label … def in
      adds_graph … l lbl tmp_lbl (add_graph … tmp_lbl fin def)
    ] in
  foldi ??? f (joint_if_code ?? def) empty.
*)
(*
definition graph_to_lin_statement :
  ∀p : unserialized_params.∀globals.
  joint_statement (mk_graph_params p) globals → joint_statement (mk_lin_params p) globals ≝
  λp,globals,stmt.match stmt with
  [ sequential c _ ⇒ sequential … c it
  | final c ⇒
    final ?? match c return λx.joint_fin_step (mk_lin_params p) globals with
    [ GOTO l ⇒ GOTO … l
    | RETURN ⇒ RETURN …
    | extension_fin c ⇒ extension_fin ?? c
    ]
  ].

lemma graph_to_lin_labels :
  ∀p : unserialized_params.∀globals,s.
  stmt_labels … (graph_to_lin_statement p globals s) =
  stmt_explicit_labels … s.
#p#globals * [//] * //
qed.

(* in order to make the coercion from lists to sets to work, one needs these hints *)
unification hint 0 ≔ ;
X ≟ identifier LabelTag
⊢
list label ≡ list X.

unification hint 0 ≔ ;
X ≟ identifier RegisterTag
⊢
list register ≡ list X.

   
definition hide_prf : ∀P : Prop.P → P ≝ λP,prf.prf.
definition hide_Prop : Prop → Prop ≝ λP.P.

interpretation "hide proof" 'hide p = (hide_prf ? p).
interpretation "hide Prop" 'hide p = (hide_Prop p).

(* discard all elements failing test, return first element succeeding it *)
(* and the rest of the list, if any. *)
let rec chop A (test : A → bool) (l : list A) on l : option (A × (list A)) ≝
  match l with
  [ nil ⇒ None ?
  | cons x l' ⇒ if test x then return 〈x, l'〉 else chop A test l'
  ].

lemma chop_hit : ∀A,f,l,pr. chop A f l = Some ? pr →
  let x ≝ \fst pr in
  let post ≝ \snd pr in
  ∃pre.All ? (λx.Not (bool_to_Prop (f x))) pre ∧ l = pre @ x :: post ∧ bool_to_Prop (f x).
#A#f#l elim l
[ normalize * #x #post #EQ destruct
| #y #l' #Hi * #x #post
  normalize elim (true_or_false_Prop (f y)) #fy >fy normalize
  #EQ
  [ destruct >fy %{[ ]} /3 by refl, conj, I/
  | elim (Hi … EQ) #pre ** #prefalse #chopd #fx
    %{(y :: pre)} %[%[%{fy prefalse}| >chopd %]|@fx]
  ]
]
qed.

lemma chop_miss : ∀A,f,l. chop A f l = None ? → All A (λx.Not (bool_to_Prop (f x))) l.
#A#f#l elim l
[ normalize #_ %
| #y #l' #Hi normalize
  elim (true_or_false_Prop (f y)) #fy >fy normalize
  #EQ
  [ destruct
  | /3 by conj, nmk/
  ]
]
qed.

unification hint 0 ≔ p, globals;
lp ≟ lin_params_to_params p,
sp ≟ stmt_pars lp,
js ≟ joint_statement sp globals,
lo ≟ labelled_obj LabelTag js
(*----------------------------*)⊢
list lo ≡ codeT lp globals.


definition graph_visit_ret_type ≝ λp,globals.λg : codeT (mk_graph_params p) globals.
  λentry : label.
  (Σ〈visited'   : identifier_map LabelTag ℕ,
   required'  : identifier_set LabelTag,
   generated' : codeT (mk_lin_params p) globals〉.'hide (
      And (And (And (lookup ?? visited' entry = Some ? 0) (required' ⊆ visited'))
        (code_forall_labels … (λl.bool_to_Prop (l∈required')) generated'))
        (∀l,n.lookup ?? visited' l = Some ? n →
          And (code_has_label … (rev ? generated') l)
            (∃s.And (And
              (lookup … g l = Some ? s)
              (nth_opt … n (rev … generated') = Some ? 〈Some ? l, graph_to_lin_statement … s〉))
              (opt_All ?
                (λnext.Or (lookup … visited' next = Some ? (S n))
                  (nth_opt … (S n) (rev … generated') = Some ? 〈None ?, GOTO … next〉))
                (stmt_implicit_label … s)))))).
                
unification hint 0 ≔ tag ⊢ identifier_set tag ≡ identifier_map tag unit.

let rec graph_visit
  (p : unserialized_params)
  (globals: list ident)
  (g : codeT (mk_graph_params p) globals)
  (* = graph (joint_statement (mk_graph_params p) globals *)
  (required: identifier_set LabelTag)
  (visited: identifier_map LabelTag ℕ) (* the reversed index of labels in the new code *)
  (generated: codeT (mk_lin_params p) globals)
  (* ≝ list ((option label)×(joint_statement (mk_lin_params p) globals)) *)
  (visiting: list label)
  (gen_length : ℕ)
  (n: nat)
  (entry : label)
  (g_prf : code_closed … g)
  (required_prf1 : ∀i.i∈required → Or (In ? visiting i) (bool_to_Prop (i ∈ visited)))
  (required_prf2 : code_forall_labels … (λl.bool_to_Prop (l ∈ required)) generated)
  (generated_prf1 : ∀l,n.lookup … visited l = Some ? n → hide_Prop (
    And (code_has_label … (rev ? generated) l)
    (∃s.And (And
      (lookup … g l = Some ? s)
      (nth_opt ? n (rev … generated) = Some ? 〈Some ? l, graph_to_lin_statement … s〉))
      (opt_All ? (λnext.match lookup … visited next with
                     [ Some n' ⇒ Or (n' = S n) (nth_opt ? (S n) (rev ? generated) = Some ? 〈None ?, GOTO … next〉)
                     | None ⇒ And (nth_opt ? 0 visiting = Some ? next) (S n = gen_length) ]) (stmt_implicit_label … s)))))
  (generated_prf2 : ∀l.lookup … visited l = None ? → does_not_occur … l (rev ? generated))
  (visiting_prf : All … (λl.lookup … g l ≠ None ?) visiting)
  (gen_length_prf : gen_length = length ? generated)
  (entry_prf : Or (And (And (visiting = [entry]) (gen_length = 0)) (Not (bool_to_Prop (entry∈visited))))
                  (lookup … visited entry = Some ? 0))
  (n_prf : le (id_map_size … g) (plus n (id_map_size … visited)))
  on n
  : graph_visit_ret_type … g entry ≝
  match chop ? (λx.¬x∈visited) visiting
  return λx.chop ? (λx.¬x∈visited) visiting = x → graph_visit_ret_type … g entry with
  [ None ⇒ λeq_chop.
    let H ≝ chop_miss … eq_chop in
    mk_Sig … 〈visited, required, generated〉 ?
  | Some pr ⇒ λeq_chop.
    let vis_hd ≝ \fst pr in
    let vis_tl ≝ \snd pr in
    let H ≝ chop_hit ???? eq_chop in
    match n return λx.x = n → graph_visit_ret_type … g entry with
    [ O ⇒ λeq_n.⊥
    | S n' ⇒ λeq_n.
      (* add the label to the visited ones *)
      let visited' ≝ add … visited vis_hd gen_length in
      (* take l's statement *)
      let statement ≝ opt_safe … (lookup ?? g vis_hd) (hide_prf ? ?) in  
      (* translate it to its linear version *)
      let translated_statement ≝ graph_to_lin_statement p globals statement in
      (* add the translated statement to the code (which will be reversed later) *)
      let generated' ≝ 〈Some … vis_hd, translated_statement〉 :: generated in
      let required' ≝ stmt_explicit_labels … statement ∪ required in
      (* put successors in the visiting worklist *)
      let visiting' ≝ stmt_labels … statement @ vis_tl in
      (* finally, check the implicit successor *)
      (* if it has been already visited, we need to add a GOTO *)
      let add_req_gen ≝ match stmt_implicit_label … statement with
        [ Some next ⇒
          if next ∈ visited' then 〈1, {(next)}, [〈None label, GOTO … next〉]〉 else 〈0, ∅, [ ]〉
        | None ⇒ 〈0, ∅, [ ]〉
        ] in
      graph_visit ???
        (\snd (\fst add_req_gen) ∪ required')
        visited'
        (\snd add_req_gen @ generated')
        visiting'
        (\fst (\fst add_req_gen) + S(gen_length))
        n' entry g_prf ????????
    ] (refl …)
  ] (refl …).
whd
[ (* base case, visiting is all visited *)
  %[
    %[
      %[
        elim entry_prf
        [ ** #eq_visiting #gen_length_O #entry_vis >eq_visiting in H; * >entry_vis
          * #ABS elim (ABS I)
        | //
        ]
      | #l #l_req
        elim (required_prf1 … l_req) #G
        [ lapply (All_In … H G) #H >(notb_false ? H) %
        | assumption
        ]
      ]
    | assumption
    ]
   | #l #n #H elim (generated_prf1 … H)
      #H1 * #s ** #H2 #H3 #H4
      % [assumption] %{s} %
      [% assumption
      | @(opt_All_mp … H4) -l #l
        lapply (in_map_domain … visited l)
        elim (true_or_false (l∈visited)) #l_vis >l_vis
        normalize nodelta [ * #n' ] #EQlookup >EQlookup
        normalize nodelta *
        [ #EQn' % >EQn' %
        | #H %2{H}
        | #H' lapply (All_nth … H … H') >l_vis * #ABS elim (ABS I)
        ]
      ]
    ]
|*: (* unpack H in all other cases *) elim H #pre ** #H1 #H2 #H3 ]
(* first, close goals where add_gen_req plays no role *)
[10: (* vis_hd is in g *) @(All_split … visiting_prf … H2)
|1: (* n = 0 absrud *)
  @(absurd … n_prf)
  @lt_to_not_le
  <eq_n
  lapply (add_size … visited vis_hd 0 (* dummy value *))
  >(notb_true … H3)
  whd in match (if ? then ? else ?);
  whd in match (? + ?);
  whd in match (lt ? ?);
  #EQ <EQ @subset_card @add_subset
  [ @(All_split ? (λx.bool_to_Prop (x∈g)) ????? H2) @(All_mp … visiting_prf)
    #a elim g #gm whd in ⊢ (?→?%); #H >(opt_to_opt_safe … H) %
  | #l #H lapply (mem_map_domain … H) -H #H lapply(opt_to_opt_safe … H)
    generalize in match (opt_safe ???); #n #l_is_n
    elim (generated_prf1 … l_is_n) #_ * #s ** #s_in_g #_ #_ lapply s_in_g -s_in_g
    elim g #mg  whd in ⊢ (?→?%); #H >H whd %
  ]
|6:
  @All_append
  [ @(g_prf … vis_hd) <opt_to_opt_safe %
  | >H2 in visiting_prf;
    #H' lapply (All_append_r … H') -H' * #_ //
  ]
|8:
  %2 elim entry_prf
  [ ** >H2 cases pre
    [2: #x' #pre' #ABS normalize in ABS; destruct(ABS)
      cases pre' in e0; [2: #x'' #pre''] #ABS' normalize in ABS'; destruct(ABS')
    |1: #EQ normalize in EQ; destruct(EQ) #eq_gen_length #_
      >lookup_add_hit >eq_gen_length %
    ]
  | #lookup_entry cut (entry ≠ vis_hd)
    [ % whd in match vis_hd; #entry_vis_hd <entry_vis_hd in H3; #entry_vis
      lapply (in_map_domain … visited entry) >(notb_true … entry_vis)
      normalize nodelta >lookup_entry #ABS destruct(ABS)]
    #entry_not_vis_hd >(lookup_add_miss ?????? entry_not_vis_hd) assumption
  ]
|9:
  >commutative_plus
  >add_size >(notb_true … H3) normalize nodelta
  whd in match (? + ?);
  >commutative_plus
  change with (? ≤ S(?) + ?)
  >eq_n assumption
|*: (* where add_gen_req does matter, expand the three possible cases *)
  lapply (refl … add_req_gen)
  whd in ⊢ (???%→?);
  lapply (refl … (stmt_implicit_label … statement))
  (* BUG *)
  [ generalize in match (stmt_implicit_label … statement) in ⊢ (???%→%);
  | generalize in match (stmt_implicit_label … statement) in ⊢ (???%→%);
  | generalize in match (stmt_implicit_label … statement) in ⊢ (???%→%);
  | generalize in match (stmt_implicit_label … statement) in ⊢ (???%→%);
  | generalize in match (stmt_implicit_label … statement) in ⊢ (???%→%);
  ]
  *[2,4,6,8,10: #next]
  #EQimpl
  whd in ⊢ (???%→?);
  [1,2,3,4,5: elim (true_or_false_Prop … (next∈visited')) #next_vis >next_vis
    whd in ⊢ (???%→?);]
  #EQ_req_gen >EQ_req_gen
  (* these are the cases, reordering them *)
  [1,2,11: | 3,4,12: | 5,6,13: | 7,8,14: |9,10,15: ]
  [1,2,3: #i >mem_set_union
    [ #H elim (orb_Prop_true … H) -H
      [ #H >(mem_set_singl_to_eq … H) %2{next_vis}]
    |*: >mem_set_empty whd in match (false ∨ ?);
    ]
    >mem_set_union
    #H elim(orb_Prop_true … H) -H
    [1,3,5: (* i is an explicit successor *)
      #i_succ
      (* if it's visited it's ok *)
      elim(true_or_false_Prop (i ∈visited')) #i_vis >i_vis
      [1,3,5: %2 %
      |*: %
        @Exists_append_l
        whd in match (stmt_labels ???);
        @Exists_append_r
        @mem_list_as_set
        @i_succ
      ]
    |2,4,6: (* i was already required *)
      #i_req
      elim (required_prf1 … i_req)
      [1,3,5: >H2 #H elim (Exists_append … H) -H
        [1,3,5: (* i in preamble → i∈visited *)
          #i_pre %2 >mem_set_add @orb_Prop_r
          lapply (All_In … H1 i_pre)
          #H >(notb_false … H) %
        |*: *
          [1,3,5: (* i is vis_hd *)
            #eq_i >eq_i %2 @mem_set_add_id
          |*: (* i in vis_tl → i∈visiting' *)
            #i_post % @Exists_append_r assumption
          ]
        ]
      |*: #i_vis %2 >mem_set_add @orb_Prop_r assumption
      ]
    ]
  |4,5,6:
    [% [ whd % [ >mem_set_union >mem_set_add_id % | %]]]
    whd in match (? @ ?); %
    [1,3,5:
      whd
      >graph_to_lin_labels
      change with (All ?? (stmt_explicit_labels ?? statement))
      whd in match required';
      generalize in match (stmt_explicit_labels … statement);
      #l @list_as_set_All
      #i >mem_set_union >mem_set_union
      #i_l @orb_Prop_r @orb_Prop_l @i_l
    |*: @(All_mp … required_prf2)
      * #l_opt #s @All_mp
      #l #l_req >mem_set_union @orb_Prop_r
      >mem_set_union @orb_Prop_r @l_req
    ]
  |7,8,9:
    #i whd in match visited';
    @(eq_identifier_elim … i vis_hd)
    [1,3,5: #EQi >EQi #pos
      >lookup_add_hit #EQpos cut (gen_length = pos)
        [1,3,5: (* BUG: -graph_visit *) -visited destruct(EQpos) %]
        -EQpos #EQpos <EQpos -pos
      %
      [1,3,5: whd in match (rev ? ?);
        >rev_append_def
        whd
        [ change with (? @ ([?] @ [?])) in match (? @ [? ; ?]);
          <associative_append >occurs_exactly_once_None]
        >occurs_exactly_once_Some_eq >eq_identifier_refl
        normalize nodelta
        @generated_prf2
        lapply (in_map_domain … visited vis_hd)
        >(notb_true … H3) normalize nodelta //
      |*: %{statement}
        %
        [1,3,5: %
          [1,3,5:
           change with (? = Some ? (opt_safe ???))
           @opt_safe_elim #s //
          |*: whd in match (rev ? ?);
            >rev_append_def
            [ change with (? @ ([?] @ [?])) in match (? @ [? ; ?]);
              <associative_append @nth_opt_append_hit_l ]
            >nth_opt_append_r
            >rev_length
            <gen_length_prf
            [1,3,5: <minus_n_n] %
          ]
        |*: >EQimpl whd [3: %]
          >mem_set_add in next_vis;
          @eq_identifier_elim
          [1,3: #EQnext >EQnext * [2: #ABS elim(ABS I)]
            >lookup_add_hit
          |*: #NEQ >(lookup_add_miss … visited … NEQ)
            whd in match (false ∨ ?);
            #next_vis lapply(in_map_domain … visited next) >next_vis
            whd in ⊢ (% → ?); [ * #s ]
            #EQlookup >EQlookup
          ] whd
          [1,2: %2
            >rev_append >nth_opt_append_r
            >rev_length whd in match generated';
            whd in match (|? :: ?|); <gen_length_prf
            [1,3: <minus_n_n ] %
          |*: % [2: %] @nth_opt_append_hit_l whd in match (stmt_labels … statement);
            >EQimpl %
          ]
        ]
      ]
    |*:
      #NEQ #n_i >(lookup_add_miss … visited … NEQ)
      #Hlookup elim (generated_prf1 … Hlookup)
      #G1 * #s ** #G2 #G3 #G4
      %
      [1,3,5: whd in match (rev ??);
        >rev_append_def whd
        [ change with (? @ ([?] @ [?])) in match (? @ [? ; ?]);
          <associative_append >occurs_exactly_once_None]
        >occurs_exactly_once_Some_eq
        >eq_identifier_false
        [2,4,6: % #ABS >ABS in NEQ; * #ABS' @ABS' %]
        normalize nodelta
        assumption
      |*: %{s}
        %
        [1,3,5: %
          [1,3,5: assumption
          |*: whd in match (rev ??); >rev_append_def
            [ change with (? @ ([?] @ [?])) in match (? @ [? ; ?]);
              <associative_append @nth_opt_append_hit_l ]
            @nth_opt_append_hit_l assumption
          ]
        |*: @(opt_All_mp … G4)
          #x
          @(eq_identifier_elim … x vis_hd) #Heq
          [1,3,5: >Heq 
            lapply (in_map_domain … visited vis_hd)
            >(notb_true … H3)
           normalize nodelta #EQlookup >EQlookup normalize nodelta
           * #nth_opt_visiting #gen_length_eq
           >lookup_add_hit normalize nodelta %
           >gen_length_eq %
          |*: >(lookup_add_miss ?????? Heq)
            lapply (in_map_domain … visited x)
            elim (true_or_false_Prop (x∈visited)) #x_vis >x_vis normalize nodelta
            [1,3,5: * #n'] #EQlookupx >EQlookupx normalize nodelta *
            [1,3,5: #G %{G}
            |2,4,6: #G %2 whd in match (rev ??); >rev_append_def
              [ change with (? @ ([?] @ [?])) in match (? @ [? ; ?]);
              <associative_append @nth_opt_append_hit_l ]
              @nth_opt_append_hit_l assumption
            |*: #G elim(absurd ?? Heq)
              (* BUG (but useless): -required -g -generated *)
               >H2 in G; #G
              lapply (refl … (nth_opt ? 0 pre))
              (* BUG *)
              [generalize in ⊢ (???%→?);
              |generalize in ⊢ (???%→?);
              |generalize in ⊢ (???%→?);
              ] *
              [1,3,5: #G' >(nth_opt_append_miss_l … G') in G;
                change with (Some ? vis_hd = ? → ?)
                #EQvis_hd' destruct(EQvis_hd') %
              |*: #lbl'' #G' >(nth_opt_append_hit_l ? pre ??? G') in G;
                #EQlbl'' destruct(EQlbl'') lapply (All_nth … H1 … G')
                >x_vis * #ABS elim (ABS I)
              ]
            ]
          ]
        ]
      ]
    ]
  |10,11,12:
    #i whd in match visited';
    lapply (in_map_domain … visited' i)
    >mem_set_add
    elim (true_or_false_Prop (eq_identifier … vis_hd i)) #i_vis_hd
    >eq_identifier_sym >i_vis_hd
    [2,4,6: elim(true_or_false (i∈visited)) #i_vis >i_vis]
    [1,3,5,7,8,9: change with ((∃_.?) → ?); * #n #EQlook >EQlook #ABS destruct(ABS)]
    #_ #EQlookup >lookup_add_miss in EQlookup;
    [2,4,6: % #ABS >ABS in i_vis_hd; >eq_identifier_refl *]
    #EQlookup
    [1,2,3: @EQlookup %]
    whd in match (rev ??); >rev_append_def
    [ change with (? @ ([?] @ [?])) in match (? @ [? ; ?]);
              <associative_append >does_not_occur_None]
    >(does_not_occur_Some ?????? (i_vis_hd))
    @generated_prf2 assumption
  |13,14,15:
    whd in match generated'; normalize <gen_length_prf %
  ]
]
qed.

(* CSC: The branch compression (aka tunneling) optimization is not implemented
   in Matita *)
definition branch_compress 
  ≝ λp: graph_params.λglobals.λg:codeT p globals.
    λentry : Σl.code_has_label … g l.g.
  
lemma branch_compress_closed : ∀p,globals,g,l.code_closed ?? g →
  code_closed … (branch_compress p globals g l).
#p#globals#g#l#H @H qed.

lemma branch_compress_has_entry : ∀p,globals,g,l.
  code_has_label … (branch_compress p globals g l) l.
#p#globals#g*#l#l_prf @l_prf qed.

definition filter_labels ≝ λtag,A.λtest : identifier tag → bool.λc : list (labelled_obj tag A).
  map ??
    (λs. let 〈l_opt,x〉 ≝ s in
      〈! l ← l_opt ; if test l then return l else None ?, x〉) c.
      
lemma does_not_occur_filter_labels :
  ∀tag,A,test,id,c.
    does_not_occur ?? id (filter_labels tag A test c) =
      (does_not_occur ?? id c ∨ ¬ test id).
#tag #A #test #id #c elim c
[ //
| ** [2: #lbl] #s #tl #IH
  whd in match (filter_labels ????); normalize nodelta
  whd in match (does_not_occur ????) in ⊢ (??%%);
  [2: @IH]
  normalize in match (! l ← ? ; ?); >IH
  @(eq_identifier_elim ?? lbl id) #Heq [<Heq]
  elim (test lbl) normalize nodelta
  change with (eq_identifier ???) in match (instruction_matches_identifier ????);
  [1,2: >eq_identifier_refl [2: >commutative_orb] normalize %
  |*: >(eq_identifier_false ??? Heq) normalize nodelta %
  ]
]
qed.

lemma occurs_exactly_once_filter_labels :
  ∀tag,A,test,id,c.
    occurs_exactly_once ?? id (filter_labels tag A test c) =
      (occurs_exactly_once ?? id c ∧ test id).
#tag #A #test #id #c elim c
[ //
| ** [2: #lbl] #s #tl #IH
  whd in match (filter_labels ????); normalize nodelta
  whd in match (occurs_exactly_once ????) in ⊢ (??%%);
  [2: @IH]
  normalize in match (! l ← ? ; ?); >IH
  >does_not_occur_filter_labels
  @(eq_identifier_elim ?? lbl id) #Heq [<Heq]
  elim (test lbl) normalize nodelta
  change with (eq_identifier ???) in match (instruction_matches_identifier ????);
  [1,2: >eq_identifier_refl >commutative_andb [ >(commutative_andb ? true) >commutative_orb | >(commutative_andb ? false)] normalize %
  |*: >(eq_identifier_false ??? Heq) normalize nodelta %
  ]
]
qed.

lemma nth_opt_filter_labels : ∀tag,A,test,instrs,n.
  nth_opt ? n (filter_labels tag A test instrs) =
  ! 〈lopt, s〉 ← nth_opt ? n instrs ;
  return 〈 ! lbl ← lopt; if test lbl then return lbl else None ?, s〉.
#tag #A #test #instrs elim instrs
[ * [2: #n'] %
| * #lopt #s #tl #IH * [2: #n']
  whd in match (filter_labels ????); normalize nodelta
  whd in match (nth_opt ???) in ⊢ (??%%); [>IH] %
]
qed.

definition linearize_code:
 ∀p : unserialized_params.∀globals.
  ∀g : codeT (mk_graph_params p) globals.code_closed … g →
  ∀entry : (Σl. code_has_label … g l).
    (Σc : codeT (mk_lin_params p) globals.
      code_closed … c ∧
      ∃ sigma : identifier_map LabelTag ℕ.
      lookup … sigma entry = Some ? 0 ∧
      ∀l,n.lookup … sigma l = Some ? n →
        ∃s. lookup … g l = Some ? s ∧
          opt_Exists ?
            (λls.let 〈lopt, ts〉 ≝ ls in
              opt_All ? (eq ? l) lopt ∧
              ts = graph_to_lin_statement … s ∧
              opt_All ?
                (λnext.Or (lookup … sigma next = Some ? (S n))
                (nth_opt … (S n) c = Some ? 〈None ?, GOTO … next〉))
                (stmt_implicit_label … s)) (nth_opt … n c))
≝
 λp,globals,g,g_prf,entry_sig.
    let g ≝ branch_compress (mk_graph_params p) ? g entry_sig in
    let g_prf ≝ branch_compress_closed … g entry_sig g_prf in
    let entry_sig' ≝ mk_Sig ?? entry_sig (branch_compress_has_entry … g entry_sig) in
    match graph_visit p globals g ∅ (empty_map …) [ ] [entry_sig] 0 (|g|)
      (entry_sig) g_prf ????????
    with
    [ mk_Sig triple H ⇒ 
      let sigma ≝ \fst (\fst triple) in
      let required ≝ \snd (\fst triple) in
      let crev ≝ \snd triple in
      let lbld_code ≝ rev ? crev in
      mk_Sig ?? (filter_labels … (λl.l∈required) lbld_code) ? ].
[ (* done later *)
| #i >mem_set_empty *
| %
|#l #n normalize in ⊢ (%→?); #ABS destruct(ABS)
| #l #_ %
| % [2: %] @(pi2 … entry_sig')
| %
| % % [% %] cases (pi1 … entry_sig) normalize #_ % //
| >commutative_plus change with (? ≤ |g|) %
]
lapply (refl … triple)
generalize in match triple in ⊢ (???%→%); **
#visited #required #generated #EQtriple
>EQtriple in H ⊢ %; normalize nodelta ***
#entry_O #req_vis #labels_in_req #sigma_prop
% >EQtriple
[ (* code closed *)
  @All_map
  [2: @All_rev
    @(All_mp … labels_in_req) #ls #H @H
  |1: (* side-effect close *)
  |3: * #lopt #s @All_mp
    #lbl #lbl_req whd in match (code_has_label ????);
    >occurs_exactly_once_filter_labels
    @andb_Prop [2: assumption]
    lapply (in_map_domain … visited lbl)
    >(req_vis … lbl_req) * #n #eq_lookup
    elim (sigma_prop ?? eq_lookup) #H #_ @H
  ]
]
%{visited} % [assumption]
#lbl #n #eq_lookup elim (sigma_prop ?? eq_lookup)
#lbl_in_gen * #stmt ** #stmt_in_g #nth_opt_is_stmt #succ_is_in
% [2: % [ assumption ] |]
>nth_opt_filter_labels in ⊢ (???%);
>nth_opt_is_stmt
whd in match (! 〈lopt, s〉 ← Some ??; ?);
whd
whd in match (! lbl0 ← Some ??; ?);
% [ % [ elim (lbl ∈ required) ] % ]
whd
lapply (refl … (stmt_implicit_label … stmt))
generalize in match (stmt_implicit_label … stmt) in ⊢ (???%→%); * [2: #next]
#eq_impl_lbl normalize nodelta [2: %]
>eq_impl_lbl in succ_is_in; whd in match (opt_All ???); * #H
[ %{H}
| %2 >nth_opt_filter_labels >H
  whd in match (! 〈lopt, s〉 ← ?; ?);
  whd in match (! lbl0 ← ?; ?);
  %
]
qed.

definition graph_linearize :
  ∀p : unserialized_params.
  ∀globals. ∀fin : joint_closed_internal_function globals (mk_graph_params p).
    Σfout : joint_closed_internal_function globals (mk_lin_params p).
      ∃sigma : identifier_map LabelTag ℕ. 
        let g ≝ joint_if_code ?? (pi1 … fin) in
        let c ≝ joint_if_code ?? (pi1 … fout) in
        let entry ≝ joint_if_entry ?? (pi1 … fin) in
         lookup … sigma entry = Some ? 0 ∧
          ∀l,n.lookup … sigma l = Some ? n →
            ∃s. lookup … g l = Some ? s ∧
              opt_Exists ?
                (λls.let 〈lopt, ts〉 ≝ ls in
                  opt_All ? (eq ? l) lopt ∧
                  ts = graph_to_lin_statement … s ∧
                  opt_All ?
                    (λnext.Or (lookup … sigma next = Some ? (S n))
                    (nth_opt … (S n) c = Some ? 〈None ?, GOTO … next〉))
                    (stmt_implicit_label … s)) (nth_opt … n c) ≝
  λp,globals,f_sig.
  mk_Sig ?? (match f_sig with
  [ mk_Sig f f_prf ⇒  
  mk_joint_internal_function globals (mk_lin_params p)
   (joint_if_luniverse ?? f) (joint_if_runiverse ?? f)
   (joint_if_result ?? f) (joint_if_params ?? f) (joint_if_locals ?? f)
   (joint_if_stacksize ?? f)
   (linearize_code p globals (joint_if_code … f) f_prf (joint_if_entry … f))
   (mk_Sig ?? it I) (mk_Sig ?? it I)
  ]) ?.
elim f_sig
normalize nodelta #f_in #f_in_prf
elim (linearize_code ?????)
#f_out * #f_out_closed #H assumption
qed. 
*)  

      
(* 
let rec add_translates
  (pars1: params1) (globals: list ident)
  (translate_list: list ?) (start_lbl: label) (dest_lbl: label) 
  (def: joint_internal_function … (graph_params pars1 globals))
    on translate_list ≝
  match translate_list with
  [ nil ⇒ add_graph … start_lbl (GOTO … dest_lbl) def
  | cons trans translate_list ⇒
    match translate_list with
    [ nil ⇒ trans start_lbl dest_lbl def
    | _ ⇒
      let 〈tmp_lbl, def〉 ≝ fresh_label … def in
      let def ≝ trans start_lbl tmp_lbl def in
        add_translates pars1 globals translate_list tmp_lbl dest_lbl def]].

definition adds_graph ≝
 λpars1:params1.λglobals. λstmt_list: list (label → joint_statement (graph_params_ pars1) globals).
  add_translates … (map ?? (λf,start_lbl,dest_lbl. add_graph pars1 ? start_lbl (f dest_lbl)) stmt_list).
  *)