Changeset 2182
 Timestamp:
 Jul 13, 2012, 11:20:36 AM (6 years ago)
 Location:
 src
 Files:

 3 added
 4 edited
Legend:
 Unmodified
 Added
 Removed

src/ERTL/liveness_paolo.ma
r2174 r2182 3 3 include "utilities/adt/set_adt.ma". 4 4 include "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 with10 [ sequential seq l ⇒11 (match seq with12 [ COND _ lbl_true ⇒ [ lbl_true ]13  _ ⇒ [ ]14 ]) @ [ l ]15  final fin ⇒16 match fin with17 [ GOTO l ⇒ [ l ]18  _ ⇒ [ ]19 ]20 ].21 5 22 6 definition register_lattice : property_lattice ≝ … … 268 252 [ None ⇒ rl_bottom 269 253  Some stmt ⇒ 270 \fold[rl_join,rl_bottom]_{successor ∈ stmt_ successors … stmt}254 \fold[rl_join,rl_bottom]_{successor ∈ stmt_labels … stmt} 271 255 (livebefore globals int_fun successor liveafter) 272 256 ]. 
src/common/Identifiers.ma
r2155 r2182 216 216 λtag,A,m,l,d. match lookup tag A m l with [ None ⇒ d  Some x ⇒ x]. 217 217 218 let rec member tag A (m:identifier_map tag A) (l:identifier tag) on m : bool ≝ 218 definition member ≝ 219 λtag,A.λm:identifier_map tag A.λl:identifier tag. 219 220 match lookup tag A m l with [ None ⇒ false  _ ⇒ true ]. 221 222 interpretation "identifier map membership" 'mem a b = (member ?? b a). 223 224 definition lookup_safe : ∀tag,A.∀m : identifier_map tag A.∀i.i∈m → A ≝ 225 λtag,A,m,i. 226 match lookup … m i return λx.match x in option return λ_.bool with [ _ ⇒ ?] → ? with 227 [ Some x ⇒ λ_.x 228  None ⇒ λprf.⊥ 229 ]. @prf qed. 230 231 lemma 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); 233 whd in match lookup_safe; normalize nodelta 234 cases (lookup ????) normalize nodelta [*] // qed. 220 235 221 236 (* Always adds the identifier to the map. *) … … 472 487 λtag,i. add_set tag (empty_set tag) i. 473 488 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 with477 [ None ⇒ false478  Some _ ⇒ true479 ].480 481 489 let rec union_set (tag:String) A B (s:identifier_map tag A) (s':identifier_map tag B) on s : identifier_set tag ≝ 482 490 an_id_map tag unit (merge … (λo,o'.match o with [Some _ ⇒ Some ? it  None ⇒ !_ o'; return it]) … … 497 505 interpretation "empty identifier set" 'empty = (empty_set ?). 498 506 interpretation "singleton identifier set" 'singl a = (add_set ? (empty_set ?) a). 499 interpretation "identifier set membership" 'mem a b = (mem_set ?? b a).500 507 interpretation "identifier map difference" 'setminus a b = (minus_set ??? a b). 501 508 … … 720 727 qed. 721 728 722 lemma mem_set_empty : ∀tag .∀i: identifier tag. i∈∅= false.723 #tag * #i normalize %729 lemma mem_set_empty : ∀tag,A.∀i: identifier tag. i∈empty_map tag A = false. 730 #tag #A * #i normalize % 724 731 qed. 725 732 
src/joint/Joint_paolo.ma
r2162 r2182 233 233 λp,globals,c,pt.match stmt_at p globals c pt with [Some _ ⇒ true  None ⇒ false]. 234 234 235 interpretation "code membership" 'mem p c = (code_has_point ?? c p). 235 (* interpretation "code membership" 'mem p c = (code_has_point ?? c p). *) 236 236 237 237 definition point_in_code ≝ λp,globals,code.Σpt.bool_to_Prop (code_has_point p globals code pt). … … 372 372 373 373 lemma 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). 375 375 #lp #globals #code elim code 376 376 [ #pt % … … 410 410 411 411 lemma 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. 414 413 415 414 lemma 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. 418 416 419 417 definition stmt_forall_succ ≝ λp,globals.λP : succ p → Prop. … … 428 426 λglobals,p,code,pt,s. 429 427 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. 431 429 432 430 definition code_closed : ∀p : params.∀globals. 
src/joint/TranslateUtils_paolo.ma
r2162 r2182 161 161 ] in 162 162 foldi … f (joint_if_code … def) empty. 163 (* 163 164 164 (* translation without register allocation *) 165 165 definition graph_translate : 166 166 ∀src_g_pars,dst_g_pars : graph_params. 167 167 ∀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)) →175 168 (* initialized function definition with empty graph *) 176 169 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)) → 177 175 (* source function *) 178 176 joint_internal_function … src_g_pars → 179 177 (* destination function *) 180 178 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. 182 180 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 ≝ 184 182 λlbl,stmt,def. 185 183 match stmt with 186 184 [ 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 193 188 ] 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: (* sideeffect 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 857 191 (* 858 192 let rec add_translates
Note: See TracChangeset
for help on using the changeset viewer.