Changeset 2182 for src/joint

Timestamp:

Jul 13, 2012, 11:20:36 AM (8 years ago)

Author:

tranquil

Message:

updated linearisation pass

Location:

src/joint

Files:

• Joint_paolo.ma (modified) (4 diffs)
• TranslateUtils_paolo.ma (modified) (1 diff)
• linearise.ma (added)

src/joint/Joint_paolo.ma

@@ -233 +233 @@
   λp,globals,c,pt.match stmt_at p globals c pt with [Some _ ⇒ true | None ⇒ false].
 
-interpretation "code membership" 'mem p c = (code_has_point ?? c p).
+(* interpretation "code membership" 'mem p c = (code_has_point ?? c p). *)
 
 definition point_in_code ≝ λp,globals,code.Σpt.bool_to_Prop (code_has_point p globals code pt).
@@ -372 +372 @@
   
 lemma lin_code_has_point : ∀lp : lin_params.∀globals.∀code:codeT lp globals.
-  ∀pt.pt ∈ code = leb (S pt) (|code|).
+  ∀pt.code_has_point … code pt = leb (S pt) (|code|).
 #lp #globals #code elim code
 [ #pt %
@@ -410 +410 @@
 
 lemma graph_code_has_point : ∀gp : graph_params.∀globals.∀code:codeT gp globals.
-  ∀pt.code_has_point … code pt = mem_set … code pt.
-#gp#globals*#m*#i % qed.
+  ∀pt.code_has_point … code pt = (pt ∈ code). // qed.
 
 lemma graph_code_has_label : ∀gp : graph_params.∀globals.∀code:codeT gp globals.
-  ∀lbl.code_has_label … code lbl = mem_set … code lbl.
-#gp #globals * #m * #i % qed.
+  ∀lbl.code_has_label … code lbl = (lbl ∈ code). // qed.
 
 definition stmt_forall_succ ≝ λp,globals.λP : succ p → Prop.
@@ -428 +426 @@
 λglobals,p,code,pt,s.
   All ? (λl.bool_to_Prop (code_has_label ?? code l)) (stmt_explicit_labels … s) ∧
-  stmt_forall_succ … (λn.bool_to_Prop (point_of_succ ? pt n ∈ code)) s.
+  stmt_forall_succ … (λn.bool_to_Prop (code_has_point … code (point_of_succ ? pt n))) s.
 
 definition code_closed : ∀p : params.∀globals.

src/joint/TranslateUtils_paolo.ma

@@ -161 +161 @@
     ] 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 →
+  (* functions dictating the translation *)
+  (label → joint_step src_g_pars globals →
+    seq_block dst_g_pars globals (joint_step dst_g_pars globals)) →
+  (label → joint_fin_step src_g_pars →
+    seq_block dst_g_pars globals (joint_fin_step 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.
+  λsrc_g_pars,dst_g_pars,globals,empty,trans_step,trans_fin_step,def.
   let f : label → joint_statement (src_g_pars : params) globals →
-    joint_internal_function … dst_g_pars → joint_internal_function … dst_g_pars ≝ 
+    joint_internal_function globals dst_g_pars → joint_internal_function globals 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)
+      adds_graph … (inl … (trans_step lbl inst)) lbl next def
+    | final inst ⇒
+      adds_graph … (inr … (trans_fin_step lbl inst)) lbl it 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. 
-*)  
-
-      
+  foldi … f (joint_if_code … def) empty.
+
 (* 
 let rec add_translates