Changeset 2182


Ignore:
Timestamp:
Jul 13, 2012, 11:20:36 AM (5 years ago)
Author:
tranquil
Message:

updated linearisation pass

Location:
src
Files:
3 added
4 edited

Legend:

Unmodified
Added
Removed
  • src/ERTL/liveness_paolo.ma

    r2174 r2182  
    33include "utilities/adt/set_adt.ma".
    44include "utilities/fixpoints.ma".
    5 
    6 (* maybe move? *)
    7 definition stmt_successors :
    8   ∀p : graph_params.∀globals.joint_statement p globals → list label ≝
    9   λp,g,s.match s with
    10   [ sequential seq l ⇒
    11     (match seq with
    12      [ COND _ lbl_true ⇒ [ lbl_true ]
    13      | _ ⇒ [ ]
    14      ]) @ [ l ]
    15   | final fin ⇒
    16     match fin with
    17     [ GOTO l ⇒ [ l ]
    18     | _ ⇒ [ ]
    19     ]
    20   ].
    215
    226definition register_lattice : property_lattice ≝
     
    268252  [ None      ⇒ rl_bottom
    269253  | Some stmt ⇒
    270     \fold[rl_join,rl_bottom]_{successor ∈ stmt_successors … stmt}
     254    \fold[rl_join,rl_bottom]_{successor ∈ stmt_labels … stmt}
    271255      (livebefore globals int_fun successor liveafter)
    272256  ].
  • src/common/Identifiers.ma

    r2155 r2182  
    216216λtag,A,m,l,d. match lookup tag A m l with [ None ⇒ d | Some x ⇒ x].
    217217
    218 let rec member tag A (m:identifier_map tag A) (l:identifier tag) on m : bool ≝
     218definition member ≝
     219  λtag,A.λm:identifier_map tag A.λl:identifier tag.
    219220  match lookup tag A m l with [ None ⇒ false | _ ⇒ true ].
     221
     222interpretation "identifier map membership" 'mem a b = (member ?? b a).
     223
     224definition lookup_safe : ∀tag,A.∀m : identifier_map tag A.∀i.i∈m → A ≝
     225λtag,A,m,i.
     226match lookup … m i return λx.match x in option return λ_.bool with [ _ ⇒ ?] → ? with
     227[ Some x ⇒ λ_.x
     228| None ⇒ λprf.⊥
     229]. @prf qed.
     230
     231lemma lookup_eq_safe : ∀tag,A,m,i,prf.lookup tag A m i = Some ? (lookup_safe tag A m i prf).
     232#tag #A #m #i whd in match (i∈m);
     233whd in match lookup_safe; normalize nodelta
     234cases (lookup ????) normalize nodelta [*] // qed.
    220235
    221236(* Always adds the identifier to the map. *)
     
    472487λtag,i. add_set tag (empty_set tag) i.
    473488
    474 (* mem set is generalised to all maps *)
    475 let rec mem_set (tag:String) A (s:identifier_map tag A) (i:identifier tag) on s : bool ≝
    476   match lookup … s i with
    477   [ None ⇒ false
    478   | Some _ ⇒ true
    479   ].
    480  
    481489let rec union_set (tag:String) A B (s:identifier_map tag A) (s':identifier_map tag B) on s : identifier_set tag ≝
    482490  an_id_map tag unit (merge … (λo,o'.match o with [Some _ ⇒ Some ? it | None ⇒ !_ o'; return it])
     
    497505interpretation "empty identifier set" 'empty = (empty_set ?).
    498506interpretation "singleton identifier set" 'singl a = (add_set ? (empty_set ?) a).
    499 interpretation "identifier set membership" 'mem a b = (mem_set ?? b a).
    500507interpretation "identifier map difference" 'setminus a b = (minus_set ??? a b).
    501508
     
    720727qed.
    721728
    722 lemma mem_set_empty : ∀tag.∀i: identifier tag. i∈∅ = false.
    723 #tag * #i normalize %
     729lemma mem_set_empty : ∀tag,A.∀i: identifier tag. i∈empty_map tag A = false.
     730#tag #A * #i normalize %
    724731qed.
    725732
  • src/joint/Joint_paolo.ma

    r2162 r2182  
    233233  λp,globals,c,pt.match stmt_at p globals c pt with [Some _ ⇒ true | None ⇒ false].
    234234
    235 interpretation "code membership" 'mem p c = (code_has_point ?? c p).
     235(* interpretation "code membership" 'mem p c = (code_has_point ?? c p). *)
    236236
    237237definition point_in_code ≝ λp,globals,code.Σpt.bool_to_Prop (code_has_point p globals code pt).
     
    372372 
    373373lemma lin_code_has_point : ∀lp : lin_params.∀globals.∀code:codeT lp globals.
    374   ∀pt.pt ∈ code = leb (S pt) (|code|).
     374  ∀pt.code_has_point … code pt = leb (S pt) (|code|).
    375375#lp #globals #code elim code
    376376[ #pt %
     
    410410
    411411lemma graph_code_has_point : ∀gp : graph_params.∀globals.∀code:codeT gp globals.
    412   ∀pt.code_has_point … code pt = mem_set … code pt.
    413 #gp#globals*#m*#i % qed.
     412  ∀pt.code_has_point … code pt = (pt ∈ code). // qed.
    414413
    415414lemma graph_code_has_label : ∀gp : graph_params.∀globals.∀code:codeT gp globals.
    416   ∀lbl.code_has_label … code lbl = mem_set … code lbl.
    417 #gp #globals * #m * #i % qed.
     415  ∀lbl.code_has_label … code lbl = (lbl ∈ code). // qed.
    418416
    419417definition stmt_forall_succ ≝ λp,globals.λP : succ p → Prop.
     
    428426λglobals,p,code,pt,s.
    429427  All ? (λl.bool_to_Prop (code_has_label ?? code l)) (stmt_explicit_labels … s) ∧
    430   stmt_forall_succ … (λn.bool_to_Prop (point_of_succ ? pt n ∈ code)) s.
     428  stmt_forall_succ … (λn.bool_to_Prop (code_has_point … code (point_of_succ ? pt n))) s.
    431429
    432430definition code_closed : ∀p : params.∀globals.
  • src/joint/TranslateUtils_paolo.ma

    r2162 r2182  
    161161    ] in
    162162  foldi … f (joint_if_code … def) empty.
    163 (* 
     163
    164164(* translation without register allocation *)
    165165definition graph_translate :
    166166  ∀src_g_pars,dst_g_pars : graph_params.
    167167  ∀globals: list ident.
    168   (* function dictating the translation *)
    169   (label → joint_step src_g_pars globals →
    170     list (joint_step dst_g_pars globals)) →
    171   (label → ext_fin_stmt src_g_pars →
    172     (list (joint_step dst_g_pars globals))
    173     ×
    174     (joint_statement dst_g_pars globals)) →
    175168  (* initialized function definition with empty graph *)
    176169  joint_internal_function … dst_g_pars →
     170  (* functions dictating the translation *)
     171  (label → joint_step src_g_pars globals →
     172    seq_block dst_g_pars globals (joint_step dst_g_pars globals)) →
     173  (label → joint_fin_step src_g_pars →
     174    seq_block dst_g_pars globals (joint_fin_step dst_g_pars)) →
    177175  (* source function *)
    178176  joint_internal_function … src_g_pars →
    179177  (* destination function *)
    180178  joint_internal_function … dst_g_pars ≝
    181   λsrc_g_pars,dst_g_pars,globals,trans,trans',empty,def.
     179  λsrc_g_pars,dst_g_pars,globals,empty,trans_step,trans_fin_step,def.
    182180  let f : label → joint_statement (src_g_pars : params) globals →
    183     joint_internal_function … dst_g_pars → joint_internal_function … dst_g_pars ≝
     181    joint_internal_function globals dst_g_pars → joint_internal_function globals dst_g_pars ≝
    184182    λlbl,stmt,def.
    185183    match stmt with
    186184    [ sequential inst next ⇒
    187       adds_graph dst_g_pars globals (trans lbl inst) lbl next def
    188     | GOTO next ⇒ add_graph … lbl (GOTO … next) def
    189     | RETURN ⇒ add_graph … lbl (RETURN …) def
    190     | extension_fin c ⇒ let 〈l, fin〉 ≝ trans' lbl c in
    191       let 〈def, tmp_lbl〉 ≝ fresh_label … def in
    192       adds_graph … l lbl tmp_lbl (add_graph … tmp_lbl fin def)
     185      adds_graph … (inl … (trans_step lbl inst)) lbl next def
     186    | final inst ⇒
     187      adds_graph … (inr … (trans_fin_step lbl inst)) lbl it def
    193188    ] in
    194   foldi ??? f (joint_if_code ?? def) empty.
    195 *)
    196 (*
    197 definition graph_to_lin_statement :
    198   ∀p : unserialized_params.∀globals.
    199   joint_statement (mk_graph_params p) globals → joint_statement (mk_lin_params p) globals ≝
    200   λp,globals,stmt.match stmt with
    201   [ sequential c _ ⇒ sequential … c it
    202   | final c ⇒
    203     final ?? match c return λx.joint_fin_step (mk_lin_params p) globals with
    204     [ GOTO l ⇒ GOTO … l
    205     | RETURN ⇒ RETURN …
    206     | extension_fin c ⇒ extension_fin ?? c
    207     ]
    208   ].
    209 
    210 lemma graph_to_lin_labels :
    211   ∀p : unserialized_params.∀globals,s.
    212   stmt_labels … (graph_to_lin_statement p globals s) =
    213   stmt_explicit_labels … s.
    214 #p#globals * [//] * //
    215 qed.
    216 
    217 (* in order to make the coercion from lists to sets to work, one needs these hints *)
    218 unification hint 0 ≔ ;
    219 X ≟ identifier LabelTag
    220 
    221 list label ≡ list X.
    222 
    223 unification hint 0 ≔ ;
    224 X ≟ identifier RegisterTag
    225 
    226 list register ≡ list X.
    227 
    228    
    229 definition hide_prf : ∀P : Prop.P → P ≝ λP,prf.prf.
    230 definition hide_Prop : Prop → Prop ≝ λP.P.
    231 
    232 interpretation "hide proof" 'hide p = (hide_prf ? p).
    233 interpretation "hide Prop" 'hide p = (hide_Prop p).
    234 
    235 (* discard all elements failing test, return first element succeeding it *)
    236 (* and the rest of the list, if any. *)
    237 let rec chop A (test : A → bool) (l : list A) on l : option (A × (list A)) ≝
    238   match l with
    239   [ nil ⇒ None ?
    240   | cons x l' ⇒ if test x then return 〈x, l'〉 else chop A test l'
    241   ].
    242 
    243 lemma chop_hit : ∀A,f,l,pr. chop A f l = Some ? pr →
    244   let x ≝ \fst pr in
    245   let post ≝ \snd pr in
    246   ∃pre.All ? (λx.Not (bool_to_Prop (f x))) pre ∧ l = pre @ x :: post ∧ bool_to_Prop (f x).
    247 #A#f#l elim l
    248 [ normalize * #x #post #EQ destruct
    249 | #y #l' #Hi * #x #post
    250   normalize elim (true_or_false_Prop (f y)) #fy >fy normalize
    251   #EQ
    252   [ destruct >fy %{[ ]} /3 by refl, conj, I/
    253   | elim (Hi … EQ) #pre ** #prefalse #chopd #fx
    254     %{(y :: pre)} %[%[%{fy prefalse}| >chopd %]|@fx]
    255   ]
    256 ]
    257 qed.
    258 
    259 lemma chop_miss : ∀A,f,l. chop A f l = None ? → All A (λx.Not (bool_to_Prop (f x))) l.
    260 #A#f#l elim l
    261 [ normalize #_ %
    262 | #y #l' #Hi normalize
    263   elim (true_or_false_Prop (f y)) #fy >fy normalize
    264   #EQ
    265   [ destruct
    266   | /3 by conj, nmk/
    267   ]
    268 ]
    269 qed.
    270 
    271 unification hint 0 ≔ p, globals;
    272 lp ≟ lin_params_to_params p,
    273 sp ≟ stmt_pars lp,
    274 js ≟ joint_statement sp globals,
    275 lo ≟ labelled_obj LabelTag js
    276 (*----------------------------*)⊢
    277 list lo ≡ codeT lp globals.
    278 
    279 
    280 definition graph_visit_ret_type ≝ λp,globals.λg : codeT (mk_graph_params p) globals.
    281   λentry : label.
    282   (Σ〈visited'   : identifier_map LabelTag ℕ,
    283    required'  : identifier_set LabelTag,
    284    generated' : codeT (mk_lin_params p) globals〉.'hide (
    285       And (And (And (lookup ?? visited' entry = Some ? 0) (required' ⊆ visited'))
    286         (code_forall_labels … (λl.bool_to_Prop (l∈required')) generated'))
    287         (∀l,n.lookup ?? visited' l = Some ? n →
    288           And (code_has_label … (rev ? generated') l)
    289             (∃s.And (And
    290               (lookup … g l = Some ? s)
    291               (nth_opt … n (rev … generated') = Some ? 〈Some ? l, graph_to_lin_statement … s〉))
    292               (opt_All ?
    293                 (λnext.Or (lookup … visited' next = Some ? (S n))
    294                   (nth_opt … (S n) (rev … generated') = Some ? 〈None ?, GOTO … next〉))
    295                 (stmt_implicit_label … s)))))).
    296                
    297 unification hint 0 ≔ tag ⊢ identifier_set tag ≡ identifier_map tag unit.
    298 
    299 let rec graph_visit
    300   (p : unserialized_params)
    301   (globals: list ident)
    302   (g : codeT (mk_graph_params p) globals)
    303   (* = graph (joint_statement (mk_graph_params p) globals *)
    304   (required: identifier_set LabelTag)
    305   (visited: identifier_map LabelTag ℕ) (* the reversed index of labels in the new code *)
    306   (generated: codeT (mk_lin_params p) globals)
    307   (* ≝ list ((option label)×(joint_statement (mk_lin_params p) globals)) *)
    308   (visiting: list label)
    309   (gen_length : ℕ)
    310   (n: nat)
    311   (entry : label)
    312   (g_prf : code_closed … g)
    313   (required_prf1 : ∀i.i∈required → Or (In ? visiting i) (bool_to_Prop (i ∈ visited)))
    314   (required_prf2 : code_forall_labels … (λl.bool_to_Prop (l ∈ required)) generated)
    315   (generated_prf1 : ∀l,n.lookup … visited l = Some ? n → hide_Prop (
    316     And (code_has_label … (rev ? generated) l)
    317     (∃s.And (And
    318       (lookup … g l = Some ? s)
    319       (nth_opt ? n (rev … generated) = Some ? 〈Some ? l, graph_to_lin_statement … s〉))
    320       (opt_All ? (λnext.match lookup … visited next with
    321                      [ Some n' ⇒ Or (n' = S n) (nth_opt ? (S n) (rev ? generated) = Some ? 〈None ?, GOTO … next〉)
    322                      | None ⇒ And (nth_opt ? 0 visiting = Some ? next) (S n = gen_length) ]) (stmt_implicit_label … s)))))
    323   (generated_prf2 : ∀l.lookup … visited l = None ? → does_not_occur … l (rev ? generated))
    324   (visiting_prf : All … (λl.lookup … g l ≠ None ?) visiting)
    325   (gen_length_prf : gen_length = length ? generated)
    326   (entry_prf : Or (And (And (visiting = [entry]) (gen_length = 0)) (Not (bool_to_Prop (entry∈visited))))
    327                   (lookup … visited entry = Some ? 0))
    328   (n_prf : le (id_map_size … g) (plus n (id_map_size … visited)))
    329   on n
    330   : graph_visit_ret_type … g entry ≝
    331   match chop ? (λx.¬x∈visited) visiting
    332   return λx.chop ? (λx.¬x∈visited) visiting = x → graph_visit_ret_type … g entry with
    333   [ None ⇒ λeq_chop.
    334     let H ≝ chop_miss … eq_chop in
    335     mk_Sig … 〈visited, required, generated〉 ?
    336   | Some pr ⇒ λeq_chop.
    337     let vis_hd ≝ \fst pr in
    338     let vis_tl ≝ \snd pr in
    339     let H ≝ chop_hit ???? eq_chop in
    340     match n return λx.x = n → graph_visit_ret_type … g entry with
    341     [ O ⇒ λeq_n.⊥
    342     | S n' ⇒ λeq_n.
    343       (* add the label to the visited ones *)
    344       let visited' ≝ add … visited vis_hd gen_length in
    345       (* take l's statement *)
    346       let statement ≝ opt_safe … (lookup ?? g vis_hd) (hide_prf ? ?) in 
    347       (* translate it to its linear version *)
    348       let translated_statement ≝ graph_to_lin_statement p globals statement in
    349       (* add the translated statement to the code (which will be reversed later) *)
    350       let generated' ≝ 〈Some … vis_hd, translated_statement〉 :: generated in
    351       let required' ≝ stmt_explicit_labels … statement ∪ required in
    352       (* put successors in the visiting worklist *)
    353       let visiting' ≝ stmt_labels … statement @ vis_tl in
    354       (* finally, check the implicit successor *)
    355       (* if it has been already visited, we need to add a GOTO *)
    356       let add_req_gen ≝ match stmt_implicit_label … statement with
    357         [ Some next ⇒
    358           if next ∈ visited' then 〈1, {(next)}, [〈None label, GOTO … next〉]〉 else 〈0, ∅, [ ]〉
    359         | None ⇒ 〈0, ∅, [ ]〉
    360         ] in
    361       graph_visit ???
    362         (\snd (\fst add_req_gen) ∪ required')
    363         visited'
    364         (\snd add_req_gen @ generated')
    365         visiting'
    366         (\fst (\fst add_req_gen) + S(gen_length))
    367         n' entry g_prf ????????
    368     ] (refl …)
    369   ] (refl …).
    370 whd
    371 [ (* base case, visiting is all visited *)
    372   %[
    373     %[
    374       %[
    375         elim entry_prf
    376         [ ** #eq_visiting #gen_length_O #entry_vis >eq_visiting in H; * >entry_vis
    377           * #ABS elim (ABS I)
    378         | //
    379         ]
    380       | #l #l_req
    381         elim (required_prf1 … l_req) #G
    382         [ lapply (All_In … H G) #H >(notb_false ? H) %
    383         | assumption
    384         ]
    385       ]
    386     | assumption
    387     ]
    388    | #l #n #H elim (generated_prf1 … H)
    389       #H1 * #s ** #H2 #H3 #H4
    390       % [assumption] %{s} %
    391       [% assumption
    392       | @(opt_All_mp … H4) -l #l
    393         lapply (in_map_domain … visited l)
    394         elim (true_or_false (l∈visited)) #l_vis >l_vis
    395         normalize nodelta [ * #n' ] #EQlookup >EQlookup
    396         normalize nodelta *
    397         [ #EQn' % >EQn' %
    398         | #H %2{H}
    399         | #H' lapply (All_nth … H … H') >l_vis * #ABS elim (ABS I)
    400         ]
    401       ]
    402     ]
    403 |*: (* unpack H in all other cases *) elim H #pre ** #H1 #H2 #H3 ]
    404 (* first, close goals where add_gen_req plays no role *)
    405 [10: (* vis_hd is in g *) @(All_split … visiting_prf … H2)
    406 |1: (* n = 0 absrud *)
    407   @(absurd … n_prf)
    408   @lt_to_not_le
    409   <eq_n
    410   lapply (add_size … visited vis_hd 0 (* dummy value *))
    411   >(notb_true … H3)
    412   whd in match (if ? then ? else ?);
    413   whd in match (? + ?);
    414   whd in match (lt ? ?);
    415   #EQ <EQ @subset_card @add_subset
    416   [ @(All_split ? (λx.bool_to_Prop (x∈g)) ????? H2) @(All_mp … visiting_prf)
    417     #a elim g #gm whd in ⊢ (?→?%); #H >(opt_to_opt_safe … H) %
    418   | #l #H lapply (mem_map_domain … H) -H #H lapply(opt_to_opt_safe … H)
    419     generalize in match (opt_safe ???); #n #l_is_n
    420     elim (generated_prf1 … l_is_n) #_ * #s ** #s_in_g #_ #_ lapply s_in_g -s_in_g
    421     elim g #mg  whd in ⊢ (?→?%); #H >H whd %
    422   ]
    423 |6:
    424   @All_append
    425   [ @(g_prf … vis_hd) <opt_to_opt_safe %
    426   | >H2 in visiting_prf;
    427     #H' lapply (All_append_r … H') -H' * #_ //
    428   ]
    429 |8:
    430   %2 elim entry_prf
    431   [ ** >H2 cases pre
    432     [2: #x' #pre' #ABS normalize in ABS; destruct(ABS)
    433       cases pre' in e0; [2: #x'' #pre''] #ABS' normalize in ABS'; destruct(ABS')
    434     |1: #EQ normalize in EQ; destruct(EQ) #eq_gen_length #_
    435       >lookup_add_hit >eq_gen_length %
    436     ]
    437   | #lookup_entry cut (entry ≠ vis_hd)
    438     [ % whd in match vis_hd; #entry_vis_hd <entry_vis_hd in H3; #entry_vis
    439       lapply (in_map_domain … visited entry) >(notb_true … entry_vis)
    440       normalize nodelta >lookup_entry #ABS destruct(ABS)]
    441     #entry_not_vis_hd >(lookup_add_miss ?????? entry_not_vis_hd) assumption
    442   ]
    443 |9:
    444   >commutative_plus
    445   >add_size >(notb_true … H3) normalize nodelta
    446   whd in match (? + ?);
    447   >commutative_plus
    448   change with (? ≤ S(?) + ?)
    449   >eq_n assumption
    450 |*: (* where add_gen_req does matter, expand the three possible cases *)
    451   lapply (refl … add_req_gen)
    452   whd in ⊢ (???%→?);
    453   lapply (refl … (stmt_implicit_label … statement))
    454   (* BUG *)
    455   [ generalize in match (stmt_implicit_label … statement) in ⊢ (???%→%);
    456   | generalize in match (stmt_implicit_label … statement) in ⊢ (???%→%);
    457   | generalize in match (stmt_implicit_label … statement) in ⊢ (???%→%);
    458   | generalize in match (stmt_implicit_label … statement) in ⊢ (???%→%);
    459   | generalize in match (stmt_implicit_label … statement) in ⊢ (???%→%);
    460   ]
    461   *[2,4,6,8,10: #next]
    462   #EQimpl
    463   whd in ⊢ (???%→?);
    464   [1,2,3,4,5: elim (true_or_false_Prop … (next∈visited')) #next_vis >next_vis
    465     whd in ⊢ (???%→?);]
    466   #EQ_req_gen >EQ_req_gen
    467   (* these are the cases, reordering them *)
    468   [1,2,11: | 3,4,12: | 5,6,13: | 7,8,14: |9,10,15: ]
    469   [1,2,3: #i >mem_set_union
    470     [ #H elim (orb_Prop_true … H) -H
    471       [ #H >(mem_set_singl_to_eq … H) %2{next_vis}]
    472     |*: >mem_set_empty whd in match (false ∨ ?);
    473     ]
    474     >mem_set_union
    475     #H elim(orb_Prop_true … H) -H
    476     [1,3,5: (* i is an explicit successor *)
    477       #i_succ
    478       (* if it's visited it's ok *)
    479       elim(true_or_false_Prop (i ∈visited')) #i_vis >i_vis
    480       [1,3,5: %2 %
    481       |*: %
    482         @Exists_append_l
    483         whd in match (stmt_labels ???);
    484         @Exists_append_r
    485         @mem_list_as_set
    486         @i_succ
    487       ]
    488     |2,4,6: (* i was already required *)
    489       #i_req
    490       elim (required_prf1 … i_req)
    491       [1,3,5: >H2 #H elim (Exists_append … H) -H
    492         [1,3,5: (* i in preamble → i∈visited *)
    493           #i_pre %2 >mem_set_add @orb_Prop_r
    494           lapply (All_In … H1 i_pre)
    495           #H >(notb_false … H) %
    496         |*: *
    497           [1,3,5: (* i is vis_hd *)
    498             #eq_i >eq_i %2 @mem_set_add_id
    499           |*: (* i in vis_tl → i∈visiting' *)
    500             #i_post % @Exists_append_r assumption
    501           ]
    502         ]
    503       |*: #i_vis %2 >mem_set_add @orb_Prop_r assumption
    504       ]
    505     ]
    506   |4,5,6:
    507     [% [ whd % [ >mem_set_union >mem_set_add_id % | %]]]
    508     whd in match (? @ ?); %
    509     [1,3,5:
    510       whd
    511       >graph_to_lin_labels
    512       change with (All ?? (stmt_explicit_labels ?? statement))
    513       whd in match required';
    514       generalize in match (stmt_explicit_labels … statement);
    515       #l @list_as_set_All
    516       #i >mem_set_union >mem_set_union
    517       #i_l @orb_Prop_r @orb_Prop_l @i_l
    518     |*: @(All_mp … required_prf2)
    519       * #l_opt #s @All_mp
    520       #l #l_req >mem_set_union @orb_Prop_r
    521       >mem_set_union @orb_Prop_r @l_req
    522     ]
    523   |7,8,9:
    524     #i whd in match visited';
    525     @(eq_identifier_elim … i vis_hd)
    526     [1,3,5: #EQi >EQi #pos
    527       >lookup_add_hit #EQpos cut (gen_length = pos)
    528         [1,3,5: (* BUG: -graph_visit *) -visited destruct(EQpos) %]
    529         -EQpos #EQpos <EQpos -pos
    530       %
    531       [1,3,5: whd in match (rev ? ?);
    532         >rev_append_def
    533         whd
    534         [ change with (? @ ([?] @ [?])) in match (? @ [? ; ?]);
    535           <associative_append >occurs_exactly_once_None]
    536         >occurs_exactly_once_Some_eq >eq_identifier_refl
    537         normalize nodelta
    538         @generated_prf2
    539         lapply (in_map_domain … visited vis_hd)
    540         >(notb_true … H3) normalize nodelta //
    541       |*: %{statement}
    542         %
    543         [1,3,5: %
    544           [1,3,5:
    545            change with (? = Some ? (opt_safe ???))
    546            @opt_safe_elim #s //
    547           |*: whd in match (rev ? ?);
    548             >rev_append_def
    549             [ change with (? @ ([?] @ [?])) in match (? @ [? ; ?]);
    550               <associative_append @nth_opt_append_hit_l ]
    551             >nth_opt_append_r
    552             >rev_length
    553             <gen_length_prf
    554             [1,3,5: <minus_n_n] %
    555           ]
    556         |*: >EQimpl whd [3: %]
    557           >mem_set_add in next_vis;
    558           @eq_identifier_elim
    559           [1,3: #EQnext >EQnext * [2: #ABS elim(ABS I)]
    560             >lookup_add_hit
    561           |*: #NEQ >(lookup_add_miss … visited … NEQ)
    562             whd in match (false ∨ ?);
    563             #next_vis lapply(in_map_domain … visited next) >next_vis
    564             whd in ⊢ (% → ?); [ * #s ]
    565             #EQlookup >EQlookup
    566           ] whd
    567           [1,2: %2
    568             >rev_append >nth_opt_append_r
    569             >rev_length whd in match generated';
    570             whd in match (|? :: ?|); <gen_length_prf
    571             [1,3: <minus_n_n ] %
    572           |*: % [2: %] @nth_opt_append_hit_l whd in match (stmt_labels … statement);
    573             >EQimpl %
    574           ]
    575         ]
    576       ]
    577     |*:
    578       #NEQ #n_i >(lookup_add_miss … visited … NEQ)
    579       #Hlookup elim (generated_prf1 … Hlookup)
    580       #G1 * #s ** #G2 #G3 #G4
    581       %
    582       [1,3,5: whd in match (rev ??);
    583         >rev_append_def whd
    584         [ change with (? @ ([?] @ [?])) in match (? @ [? ; ?]);
    585           <associative_append >occurs_exactly_once_None]
    586         >occurs_exactly_once_Some_eq
    587         >eq_identifier_false
    588         [2,4,6: % #ABS >ABS in NEQ; * #ABS' @ABS' %]
    589         normalize nodelta
    590         assumption
    591       |*: %{s}
    592         %
    593         [1,3,5: %
    594           [1,3,5: assumption
    595           |*: whd in match (rev ??); >rev_append_def
    596             [ change with (? @ ([?] @ [?])) in match (? @ [? ; ?]);
    597               <associative_append @nth_opt_append_hit_l ]
    598             @nth_opt_append_hit_l assumption
    599           ]
    600         |*: @(opt_All_mp … G4)
    601           #x
    602           @(eq_identifier_elim … x vis_hd) #Heq
    603           [1,3,5: >Heq
    604             lapply (in_map_domain … visited vis_hd)
    605             >(notb_true … H3)
    606            normalize nodelta #EQlookup >EQlookup normalize nodelta
    607            * #nth_opt_visiting #gen_length_eq
    608            >lookup_add_hit normalize nodelta %
    609            >gen_length_eq %
    610           |*: >(lookup_add_miss ?????? Heq)
    611             lapply (in_map_domain … visited x)
    612             elim (true_or_false_Prop (x∈visited)) #x_vis >x_vis normalize nodelta
    613             [1,3,5: * #n'] #EQlookupx >EQlookupx normalize nodelta *
    614             [1,3,5: #G %{G}
    615             |2,4,6: #G %2 whd in match (rev ??); >rev_append_def
    616               [ change with (? @ ([?] @ [?])) in match (? @ [? ; ?]);
    617               <associative_append @nth_opt_append_hit_l ]
    618               @nth_opt_append_hit_l assumption
    619             |*: #G elim(absurd ?? Heq)
    620               (* BUG (but useless): -required -g -generated *)
    621                >H2 in G; #G
    622               lapply (refl … (nth_opt ? 0 pre))
    623               (* BUG *)
    624               [generalize in ⊢ (???%→?);
    625               |generalize in ⊢ (???%→?);
    626               |generalize in ⊢ (???%→?);
    627               ] *
    628               [1,3,5: #G' >(nth_opt_append_miss_l … G') in G;
    629                 change with (Some ? vis_hd = ? → ?)
    630                 #EQvis_hd' destruct(EQvis_hd') %
    631               |*: #lbl'' #G' >(nth_opt_append_hit_l ? pre ??? G') in G;
    632                 #EQlbl'' destruct(EQlbl'') lapply (All_nth … H1 … G')
    633                 >x_vis * #ABS elim (ABS I)
    634               ]
    635             ]
    636           ]
    637         ]
    638       ]
    639     ]
    640   |10,11,12:
    641     #i whd in match visited';
    642     lapply (in_map_domain … visited' i)
    643     >mem_set_add
    644     elim (true_or_false_Prop (eq_identifier … vis_hd i)) #i_vis_hd
    645     >eq_identifier_sym >i_vis_hd
    646     [2,4,6: elim(true_or_false (i∈visited)) #i_vis >i_vis]
    647     [1,3,5,7,8,9: change with ((∃_.?) → ?); * #n #EQlook >EQlook #ABS destruct(ABS)]
    648     #_ #EQlookup >lookup_add_miss in EQlookup;
    649     [2,4,6: % #ABS >ABS in i_vis_hd; >eq_identifier_refl *]
    650     #EQlookup
    651     [1,2,3: @EQlookup %]
    652     whd in match (rev ??); >rev_append_def
    653     [ change with (? @ ([?] @ [?])) in match (? @ [? ; ?]);
    654               <associative_append >does_not_occur_None]
    655     >(does_not_occur_Some ?????? (i_vis_hd))
    656     @generated_prf2 assumption
    657   |13,14,15:
    658     whd in match generated'; normalize <gen_length_prf %
    659   ]
    660 ]
    661 qed.
    662 
    663 (* CSC: The branch compression (aka tunneling) optimization is not implemented
    664    in Matita *)
    665 definition branch_compress
    666   ≝ λp: graph_params.λglobals.λg:codeT p globals.
    667     λentry : Σl.code_has_label … g l.g.
    668  
    669 lemma branch_compress_closed : ∀p,globals,g,l.code_closed ?? g →
    670   code_closed … (branch_compress p globals g l).
    671 #p#globals#g#l#H @H qed.
    672 
    673 lemma branch_compress_has_entry : ∀p,globals,g,l.
    674   code_has_label … (branch_compress p globals g l) l.
    675 #p#globals#g*#l#l_prf @l_prf qed.
    676 
    677 definition filter_labels ≝ λtag,A.λtest : identifier tag → bool.λc : list (labelled_obj tag A).
    678   map ??
    679     (λs. let 〈l_opt,x〉 ≝ s in
    680       〈! l ← l_opt ; if test l then return l else None ?, x〉) c.
    681      
    682 lemma does_not_occur_filter_labels :
    683   ∀tag,A,test,id,c.
    684     does_not_occur ?? id (filter_labels tag A test c) =
    685       (does_not_occur ?? id c ∨ ¬ test id).
    686 #tag #A #test #id #c elim c
    687 [ //
    688 | ** [2: #lbl] #s #tl #IH
    689   whd in match (filter_labels ????); normalize nodelta
    690   whd in match (does_not_occur ????) in ⊢ (??%%);
    691   [2: @IH]
    692   normalize in match (! l ← ? ; ?); >IH
    693   @(eq_identifier_elim ?? lbl id) #Heq [<Heq]
    694   elim (test lbl) normalize nodelta
    695   change with (eq_identifier ???) in match (instruction_matches_identifier ????);
    696   [1,2: >eq_identifier_refl [2: >commutative_orb] normalize %
    697   |*: >(eq_identifier_false ??? Heq) normalize nodelta %
    698   ]
    699 ]
    700 qed.
    701 
    702 lemma occurs_exactly_once_filter_labels :
    703   ∀tag,A,test,id,c.
    704     occurs_exactly_once ?? id (filter_labels tag A test c) =
    705       (occurs_exactly_once ?? id c ∧ test id).
    706 #tag #A #test #id #c elim c
    707 [ //
    708 | ** [2: #lbl] #s #tl #IH
    709   whd in match (filter_labels ????); normalize nodelta
    710   whd in match (occurs_exactly_once ????) in ⊢ (??%%);
    711   [2: @IH]
    712   normalize in match (! l ← ? ; ?); >IH
    713   >does_not_occur_filter_labels
    714   @(eq_identifier_elim ?? lbl id) #Heq [<Heq]
    715   elim (test lbl) normalize nodelta
    716   change with (eq_identifier ???) in match (instruction_matches_identifier ????);
    717   [1,2: >eq_identifier_refl >commutative_andb [ >(commutative_andb ? true) >commutative_orb | >(commutative_andb ? false)] normalize %
    718   |*: >(eq_identifier_false ??? Heq) normalize nodelta %
    719   ]
    720 ]
    721 qed.
    722 
    723 lemma nth_opt_filter_labels : ∀tag,A,test,instrs,n.
    724   nth_opt ? n (filter_labels tag A test instrs) =
    725   ! 〈lopt, s〉 ← nth_opt ? n instrs ;
    726   return 〈 ! lbl ← lopt; if test lbl then return lbl else None ?, s〉.
    727 #tag #A #test #instrs elim instrs
    728 [ * [2: #n'] %
    729 | * #lopt #s #tl #IH * [2: #n']
    730   whd in match (filter_labels ????); normalize nodelta
    731   whd in match (nth_opt ???) in ⊢ (??%%); [>IH] %
    732 ]
    733 qed.
    734 
    735 definition linearize_code:
    736  ∀p : unserialized_params.∀globals.
    737   ∀g : codeT (mk_graph_params p) globals.code_closed … g →
    738   ∀entry : (Σl. code_has_label … g l).
    739     (Σc : codeT (mk_lin_params p) globals.
    740       code_closed … c ∧
    741       ∃ sigma : identifier_map LabelTag ℕ.
    742       lookup … sigma entry = Some ? 0 ∧
    743       ∀l,n.lookup … sigma l = Some ? n →
    744         ∃s. lookup … g l = Some ? s ∧
    745           opt_Exists ?
    746             (λls.let 〈lopt, ts〉 ≝ ls in
    747               opt_All ? (eq ? l) lopt ∧
    748               ts = graph_to_lin_statement … s ∧
    749               opt_All ?
    750                 (λnext.Or (lookup … sigma next = Some ? (S n))
    751                 (nth_opt … (S n) c = Some ? 〈None ?, GOTO … next〉))
    752                 (stmt_implicit_label … s)) (nth_opt … n c))
    753 
    754  λp,globals,g,g_prf,entry_sig.
    755     let g ≝ branch_compress (mk_graph_params p) ? g entry_sig in
    756     let g_prf ≝ branch_compress_closed … g entry_sig g_prf in
    757     let entry_sig' ≝ mk_Sig ?? entry_sig (branch_compress_has_entry … g entry_sig) in
    758     match graph_visit p globals g ∅ (empty_map …) [ ] [entry_sig] 0 (|g|)
    759       (entry_sig) g_prf ????????
    760     with
    761     [ mk_Sig triple H ⇒
    762       let sigma ≝ \fst (\fst triple) in
    763       let required ≝ \snd (\fst triple) in
    764       let crev ≝ \snd triple in
    765       let lbld_code ≝ rev ? crev in
    766       mk_Sig ?? (filter_labels … (λl.l∈required) lbld_code) ? ].
    767 [ (* done later *)
    768 | #i >mem_set_empty *
    769 | %
    770 |#l #n normalize in ⊢ (%→?); #ABS destruct(ABS)
    771 | #l #_ %
    772 | % [2: %] @(pi2 … entry_sig')
    773 | %
    774 | % % [% %] cases (pi1 … entry_sig) normalize #_ % //
    775 | >commutative_plus change with (? ≤ |g|) %
    776 ]
    777 lapply (refl … triple)
    778 generalize in match triple in ⊢ (???%→%); **
    779 #visited #required #generated #EQtriple
    780 >EQtriple in H ⊢ %; normalize nodelta ***
    781 #entry_O #req_vis #labels_in_req #sigma_prop
    782 % >EQtriple
    783 [ (* code closed *)
    784   @All_map
    785   [2: @All_rev
    786     @(All_mp … labels_in_req) #ls #H @H
    787   |1: (* side-effect close *)
    788   |3: * #lopt #s @All_mp
    789     #lbl #lbl_req whd in match (code_has_label ????);
    790     >occurs_exactly_once_filter_labels
    791     @andb_Prop [2: assumption]
    792     lapply (in_map_domain … visited lbl)
    793     >(req_vis … lbl_req) * #n #eq_lookup
    794     elim (sigma_prop ?? eq_lookup) #H #_ @H
    795   ]
    796 ]
    797 %{visited} % [assumption]
    798 #lbl #n #eq_lookup elim (sigma_prop ?? eq_lookup)
    799 #lbl_in_gen * #stmt ** #stmt_in_g #nth_opt_is_stmt #succ_is_in
    800 % [2: % [ assumption ] |]
    801 >nth_opt_filter_labels in ⊢ (???%);
    802 >nth_opt_is_stmt
    803 whd in match (! 〈lopt, s〉 ← Some ??; ?);
    804 whd
    805 whd in match (! lbl0 ← Some ??; ?);
    806 % [ % [ elim (lbl ∈ required) ] % ]
    807 whd
    808 lapply (refl … (stmt_implicit_label … stmt))
    809 generalize in match (stmt_implicit_label … stmt) in ⊢ (???%→%); * [2: #next]
    810 #eq_impl_lbl normalize nodelta [2: %]
    811 >eq_impl_lbl in succ_is_in; whd in match (opt_All ???); * #H
    812 [ %{H}
    813 | %2 >nth_opt_filter_labels >H
    814   whd in match (! 〈lopt, s〉 ← ?; ?);
    815   whd in match (! lbl0 ← ?; ?);
    816   %
    817 ]
    818 qed.
    819 
    820 definition graph_linearize :
    821   ∀p : unserialized_params.
    822   ∀globals. ∀fin : joint_closed_internal_function globals (mk_graph_params p).
    823     Σfout : joint_closed_internal_function globals (mk_lin_params p).
    824       ∃sigma : identifier_map LabelTag ℕ.
    825         let g ≝ joint_if_code ?? (pi1 … fin) in
    826         let c ≝ joint_if_code ?? (pi1 … fout) in
    827         let entry ≝ joint_if_entry ?? (pi1 … fin) in
    828          lookup … sigma entry = Some ? 0 ∧
    829           ∀l,n.lookup … sigma l = Some ? n →
    830             ∃s. lookup … g l = Some ? s ∧
    831               opt_Exists ?
    832                 (λls.let 〈lopt, ts〉 ≝ ls in
    833                   opt_All ? (eq ? l) lopt ∧
    834                   ts = graph_to_lin_statement … s ∧
    835                   opt_All ?
    836                     (λnext.Or (lookup … sigma next = Some ? (S n))
    837                     (nth_opt … (S n) c = Some ? 〈None ?, GOTO … next〉))
    838                     (stmt_implicit_label … s)) (nth_opt … n c) ≝
    839   λp,globals,f_sig.
    840   mk_Sig ?? (match f_sig with
    841   [ mk_Sig f f_prf ⇒ 
    842   mk_joint_internal_function globals (mk_lin_params p)
    843    (joint_if_luniverse ?? f) (joint_if_runiverse ?? f)
    844    (joint_if_result ?? f) (joint_if_params ?? f) (joint_if_locals ?? f)
    845    (joint_if_stacksize ?? f)
    846    (linearize_code p globals (joint_if_code … f) f_prf (joint_if_entry … f))
    847    (mk_Sig ?? it I) (mk_Sig ?? it I)
    848   ]) ?.
    849 elim f_sig
    850 normalize nodelta #f_in #f_in_prf
    851 elim (linearize_code ?????)
    852 #f_out * #f_out_closed #H assumption
    853 qed.
    854 *) 
    855 
    856      
     189  foldi … f (joint_if_code … def) empty.
     190
    857191(*
    858192let rec add_translates
Note: See TracChangeset for help on using the changeset viewer.