Changeset 2335
 Timestamp:
 Sep 20, 2012, 6:57:34 PM (7 years ago)
 Location:
 src
 Files:

 3 edited
Legend:
 Unmodified
 Added
 Removed

src/Cminor/toRTLabs.ma
r2319 r2335 5 5 6 6 definition env ≝ identifier_map SymbolTag (register × typ). 7 definition label_env ≝ identifier_map Label label.8 7 definition populate_env : env → universe RegisterTag → list (ident × typ) → list (register×typ) × env × (universe RegisterTag) ≝ 9 8 λen,gen. foldr ?? … … 132 131 ] qed. 133 132 134 definition populate_label_env : label_env → universe LabelTag → list (identifier Label) → label_env × (universe LabelTag) ≝135 λen,gen. foldr ??136 (λid,engen.137 let 〈en,gen〉 ≝ engen in138 let 〈r,gen'〉 ≝ fresh … gen in139 〈add ?? en id r, gen'〉) 〈en, gen〉.140 141 lemma populates_label_env : ∀ls,lbls,u,lbls',u'.142 populate_label_env lbls u ls = 〈lbls',u'〉 →143 ∀l. Exists ? (λl'.l' = l) ls → present ?? lbls' l.144 #ls elim ls145 [ #lbls #u #lbls' #u' #E #l *146  #h #t #IH #lbls #u #lbls' #u' whd in ⊢ (??%? → ?);147 change with (populate_label_env ???) in ⊢ (??match % with [ _ ⇒ ? ]? → ?);148 lapply (refl ? (populate_label_env lbls u t))149 cases (populate_label_env lbls u t) in ⊢ (???% → %);150 #lbls1 #u1 #E1 whd in ⊢ (??%? → ?);151 cases (fresh LabelTag u1) #lf #uf whd in ⊢ (??%? → ?);152 #E destruct153 #l *154 [ #El <El whd >lookup_add_hit % #Er destruct155  #H @lookup_add_oblivious @(IH … E1 ? H)156 ]157 ] qed.158 159 lemma label_env_contents : ∀ls,lbls,u,lbls',u'.160 populate_label_env lbls u ls = 〈lbls',u'〉 →161 ∀l. present ?? lbls' l → Exists ? (λl'.l = l') ls ∨ present ?? lbls l.162 #ls elim ls163 [ #lbls #u #lbls' #u' #E #l #H %2 whd in E:(??%?); destruct @H164  #h #t #IH #lbls #u #lbls' #u' whd in ⊢ (??%? → ?);165 change with (populate_label_env ???) in ⊢ (??match % with [ _ ⇒ ? ]? → ?);166 lapply (refl ? (populate_label_env lbls u t))167 cases (populate_label_env lbls u t) in ⊢ (???% → %);168 #lbls1 #u1 #E1 whd in ⊢ (??%? → ?);169 cases (fresh ? u1) #fi #fu whd in ⊢ (??%? → ?);170 #E destruct171 #l #H cases (identifier_eq ? l h)172 [ #El %1 %1 @El173  #NE cases (IH … E1 l ?)174 [ #H' %1 %2 @H'  #H' %2 @H'  whd in H; >lookup_add_miss in H; // ]175 ]176 ] qed.177 178 definition lookup_label : ∀e:label_env. ∀id. present ?? e id → label ≝ lookup_present ??.179 180 133 (* Check that the domain of one graph is included in another, for monotonicity 181 134 properties. Note that we don't say anything about the statements. *) 182 135 definition graph_included : graph statement → graph statement → Prop ≝ 183 λg1,g2. ∀l. present ?? g1 l → present ?? g2 l.136 extends_domain ??. 184 137 185 138 lemma graph_inc_trans : ∀g1,g2,g3. 186 139 graph_included g1 g2 → graph_included g2 g3 → graph_included g1 g3. 187 #g1 #g2 #g3 #H1 #H2 #l #P1 @H2 @H1 @P1 qed. 188 189 definition lpresent ≝ λlbls:label_env. λl. ∃l'. lookup ?? lbls l' = Some ? l. 190 191 definition partially_closed : label_env → graph statement → Prop ≝ 192 λe,g. forall_nodes ? (labels_P (λl. present ?? g l ∨ lpresent e l)) g. 140 @extends_dom_trans 141 qed. 142 193 143 194 144 (* Some data structures for the transformation that remain fixed throughout. *) 195 145 record fixed : Type[0] ≝ { 196 fx_ lenv : label_env;146 fx_gotos : identifier_set Label; 197 147 fx_env : env; 198 148 fx_rettyp : option typ … … 202 152 λty,env. 203 153 match ty with [ Some t ⇒ Σr:register. env_has env r t  _ ⇒ True ]. 154 155 (* We put in dummy statements for gotos, then change them afterwards once we 156 know their true destinations. So first we need a mapping between the dummy 157 CFG nodes and the Cminor destination. (We'll also keep a mapping of goto 158 labels to their RTLabs statements.) *) 159 160 record goto_map (fx:fixed) (g:graph statement) : Type[0] ≝ { 161 gm_map :> identifier_map LabelTag (identifier Label); 162 gm_dom : ∀id. present ?? gm_map id → present ?? g id; 163 gm_img : ∀id,l. lookup … gm_map id = Some ? l → present ?? (fx_gotos fx) l 164 }. 204 165 205 166 (* I'd use a single parametrised definition along with internal_function, but … … 214 175 ; pf_stacksize : nat 215 176 ; pf_graph : graph statement 216 ; pf_closed : partially_closed (fx_lenv … fx) pf_graph 177 ; pf_closed : graph_closed pf_graph 178 ; pf_gotos : goto_map fx pf_graph 179 ; pf_labels : Σm:identifier_map Label (identifier LabelTag). ∀l,l'. lookup … m l = Some ? l' → present ?? pf_graph l' 217 180 ; pf_typed : graph_typed (pf_locals @ pf_params) pf_graph 218 181 ; pf_entry : Σl:label. present ?? pf_graph l … … 223 186 λfx,f. env_has (pf_locals fx f @ pf_params fx f). 224 187 188 (* TODO: move or use another definition if there's already one *) 189 definition map_extends : ∀tag,A. identifier_map tag A → identifier_map tag A → Prop ≝ 190 λtag,A,m1,m2. ∀id,a. lookup tag A m1 id = Some A a → lookup tag A m2 id = Some A a. 191 192 lemma map_extends_trans : ∀tag,A,m1,m2,m3. 193 map_extends tag A m1 m2 → 194 map_extends tag A m2 m3 → 195 map_extends tag A m1 m3. 196 /3/ 197 qed. 198 225 199 record fn_contains (fx:fixed) (f1:partial_fn fx) (f2:partial_fn fx) : Prop ≝ 226 200 { fn_con_graph : graph_included (pf_graph … f1) (pf_graph … f2) 227 201 ; fn_con_env : ∀r,ty. fn_env_has … f1 r ty → fn_env_has … f2 r ty 202 ; fn_con_labels : extends_domain … (pf_labels … f1) (pf_labels … f2) 228 203 }. 229 204 … … 233 208 [ @(graph_inc_trans … (fn_con_graph … H1) (fn_con_graph … H2)) 234 209  #r #ty #H @(fn_con_env … H2) @(fn_con_env … H1) @H 210  @(extends_dom_trans … (fn_con_labels … H1) (fn_con_labels … H2)) 235 211 ] qed. 236 212 … … 248 224 lemma add_statement_inv : ∀fx,l,s.∀f. 249 225 labels_present (pf_graph fx f) s → 250 partially_closed (fx_lenv … fx)(add … (pf_graph … f) l s).226 graph_closed (add … (pf_graph … f) l s). 251 227 #fx #l #s #f #p 252 228 #l' #s' #H cases (identifier_eq … l l') 253 229 [ #E >E in H; >lookup_add_hit #E' <(?:s = s') [2:destruct //] 254 @(labels_P_mp … p) #l0 #H %1@lookup_add_oblivious @H230 @(labels_P_mp … p) #l0 #H @lookup_add_oblivious @H 255 231  #NE @(labels_P_mp … (pf_closed … f l' s' ?)) 256 [ #lx * [ #H %1 @lookup_add_oblivious @H  #H %2 @H ]232 [ #lx #H @lookup_add_oblivious @H 257 233  >lookup_add_miss in H; /2/ 258 234 ] … … 279 255 mk_partial_fn fx (pf_labgen … f) (pf_reggen … f) 280 256 (pf_params … f) (pf_locals … f) (pf_result … f) (pf_envok … f) 281 (pf_stacksize … f) (add ?? (pf_graph … f) l s) ? ? 257 (pf_stacksize … f) (add ?? (pf_graph … f) l s) ? 258 (mk_goto_map … (pf_gotos … f) ??) «pf_labels … f, ?» ? 282 259 «pf_entry … f, ?» «pf_exit … f, ?». 283 260 [ @add_statement_inv @p 261  @gm_img 262  #id #PR @lookup_add_oblivious @(gm_dom … PR) 263  #l1 #l2 #L @lookup_add_oblivious @(pi2 … (pf_labels … f) … L) 284 264  @forall_nodes_add // 285  3,4: @lookup_add_oblivious [ @(pi2 … (pf_entry … f))  @(pi2 … (pf_exit … f)) ]286  % [ #l' @lookup_add_oblivious  // ]265  6,7: @lookup_add_oblivious [ @(pi2 … (pf_entry … f))  @(pi2 … (pf_exit … f)) ] 266  % [ #l' @lookup_add_oblivious  //  cases (pf_labels fx f) /2/ ] 287 267 ] qed. 288 268 … … 295 275 mk_partial_fn fx (pf_labgen … f) (pf_reggen … f) 296 276 (pf_params … f) (pf_locals … f) (pf_result … f) (pf_envok … f) 297 (pf_stacksize … f) (add ?? (pf_graph … f) l s) ? 277 (pf_stacksize … f) (add ?? (pf_graph … f) l s) ???? 298 278 «l, ?» «pf_exit … f, ?». 299 279 [ @add_statement_inv @p 280  cases (pf_gotos … f) #m #dom #img % 281 [ @m  #id #P @lookup_add_oblivious @dom @P  @img ] 282  cases (pf_labels … f) #m #PR %{m} #l1 #l2 #L @lookup_add_oblivious @(PR … L) 300 283  @forall_nodes_add // 301 284  whd >lookup_add_hit % #E destruct 302 285  @lookup_add_oblivious @(pi2 … (pf_exit … f)) 303  % [ #l' @lookup_add_oblivious  // ]286  % [ #l' @lookup_add_oblivious  //  cases (pf_labels fx f) /2/ ] 304 287 ] qed. 305 288 … … 315 298 (mk_partial_fn fx g (pf_reggen … f) 316 299 (pf_params … f) (pf_locals … f) (pf_result … f) (pf_envok … f) 317 (pf_stacksize … f) (add ?? (pf_graph … f) l s') ? 300 (pf_stacksize … f) (add ?? (pf_graph … f) l s') ???? 318 301 «l, ?» «pf_exit … f, ?»). 319 [ % [ #l' @lookup_add_oblivious  // ] 302 [ 4: cases (pf_labels … f) #m #PR %{m} #l1 #l2 #L @lookup_add_oblivious @(PR … L) 303  % [ #l' @lookup_add_oblivious  //  cases (pf_labels fx f) /2/ ] 320 304  @add_statement_inv @p @(pi2 … (pf_entry …)) 321  @forall_nodes_add // 322  whd >lookup_add_hit % #E destruct 323  @lookup_add_oblivious @(pi2 … (pf_exit …)) 324 ] qed. 325 326 (* Variants for labels which are (goto) labels *) 327 328 lemma add_statement_inv' : ∀fx,l,s.∀f. 329 labels_P (λl. present ?? (pf_graph fx f) l ∨ lpresent (fx_lenv … fx) l) s → 330 partially_closed (fx_lenv … fx) (add … (pf_graph … f) l s). 331 #fx #l #s #f #p 332 #l' #s' #H cases (identifier_eq … l l') 333 [ #E >E in H; >lookup_add_hit #E' <(?:s = s') [2:destruct //] 334 @(labels_P_mp … p) #l0 * [ #H %1 @lookup_add_oblivious @H  #H %2 @H ] 335  #NE @(labels_P_mp … (pf_closed … f l' s' ?)) 336 [ #lx * [ #H %1 @lookup_add_oblivious @H  #H %2 @H ] 337  >lookup_add_miss in H; /2/ 338 ] 339 ] qed. 340 341 definition add_fresh_to_graph' : ∀fx. ∀s:(label → statement). ∀f:partial_fn fx. 342 (∀l. present ?? (pf_graph … f) l → labels_P (λl.present ?? (pf_graph … f) l ∨ lpresent (fx_lenv … fx) l) (s l)) → 343 (∀l. statement_typed_in … f (s l)) → 344 Σf':partial_fn fx. fn_contains … f f' ≝ 345 λfx,s,f,p,tp. 346 let 〈l,g〉 ≝ fresh … (pf_labgen … f) in 347 let s' ≝ s (pf_entry … f) in 348 (mk_partial_fn fx g (pf_reggen … f) 349 (pf_params … f) (pf_locals … f) (pf_result … f) (pf_envok … f) 350 (pf_stacksize … f) (add ?? (pf_graph … f) l s') ? ? 351 «l, ?» «pf_exit … f, ?»). 352 [ % [ #l' @lookup_add_oblivious  // ] 353  @add_statement_inv' @p @(pi2 … (pf_entry …)) 305  cases (pf_gotos … f) #m #dom #img % 306 [ @m  #id #P @lookup_add_oblivious @dom @P  @img ] 354 307  @forall_nodes_add // 355 308  whd >lookup_add_hit % #E destruct … … 385 338 «mk_partial_fn fx 386 339 (pf_labgen … f) g (pf_params … f) (〈r,ty〉::(pf_locals … f)) ? ? 387 (pf_stacksize … f) (pf_graph … f) (pf_closed … f) ? (pf_entry … f) (pf_exit … f), ?»340 (pf_stacksize … f) (pf_graph … f) (pf_closed … f) (pf_gotos … f) (pf_labels … f) ? (pf_entry … f) (pf_exit … f), ?» 388 341 in 389 342 ❬f' , ?(*«r, ?»*)❭. … … 392 345  #i #t #r1 #H #L %2 @(pf_envok … f … L) 393 346  lapply (pf_result fx f) cases (fx_rettyp fx) // #t * #r' #H %{r'} @extend_typ_env // 394  % [ #l //  #r' #ty' #H @extend_typ_env @H ]347  % [ #l //  #r' #ty' #H @extend_typ_env @H  // ] 395 348 ] qed. 396 349 … … 437 390 ] qed. 438 391 439 lemma extract_pair : ∀A,B,C,D. ∀u:A×B. ∀Q:A → B → C×D. ∀x,y.440 ((let 〈a,b〉 ≝ u in Q a b) = 〈x,y〉) →441 ∃a,b. 〈a,b〉 = u ∧ Q a b = 〈x,y〉.442 #A #B #C #D * #a #b #Q #x #y normalize #E1 %{a} %{b} % try @refl @E1 qed.443 444 445 392 lemma choose_regs_length : ∀fx,es,f,p,f',rs. 446 393 choose_regs fx es f p = ❬f',rs❭ → es = length … rs. … … 452 399 present ?? (pf_graph … f) l → 453 400 present ?? (pf_graph … f') l. 454 #fx #f #f' #l * #H1 #H2 @H1 qed.401 #fx #f #f' #l * #H1 #H2 #H3 @H1 qed. 455 402 456 403 (* Some definitions for the add_stmt function later, which we introduce now so … … 460 407 up in the graph. *) 461 408 definition Cminor_labels_added ≝ λfx,s,f'. 462 ∀l. Exists ? (λl'.l=l') (labels_of s) → 463 ∃l'. lookup ?? (fx_lenv fx) l = Some ? l' ∧ present ?? (pf_graph fx f') l'. 409 ∀l. Exists ? (λl'.l=l') (labels_of s) → present ?? (pf_labels fx f') l. 464 410 465 411 record add_stmt_inv (fx:fixed) (s:stmt) (f:partial_fn fx) (f':partial_fn fx) : Prop ≝ … … 609 555 λt,s. match s with [ St_return oe ⇒ rettyp_match t oe  _ ⇒ True ]. 610 556 557 (* Invariants about Cminor statements that we'll need *) 558 611 559 record stmt_inv (fx:fixed) (s:stmt) : Prop ≝ { 612 560 si_vars : stmt_vars (Env_has (fx_env fx)) s; 613 si_labels : stmt_labels (present ?? (fx_ lenvfx)) s;561 si_labels : stmt_labels (present ?? (fx_gotos fx)) s; 614 562 si_return : return_ok (fx_rettyp fx) s 615 563 }. … … 630 578 alias id "R_return" = "cic:/matita/cerco/RTLabs/syntax/statement.con(0,11,0)". 631 579 632 lemma lookup_label_rev : ∀lenv,l,l',p.633 lookup_label lenv l p = l' → lookup ?? lenv l = Some ? l'.634 #lenv #l #l' #p635 cut (∃lx. lookup ?? lenv l = Some ? lx)636 [ whd in p; cases (lookup ?? lenv l) in p ⊢ %;637 [ * #H cases (H (refl ??))638  #lx #_ %{lx} @refl639 ]640  * #lx #E whd in ⊢ (??%? → ?); cases p >E #q whd in ⊢ (??%? → ?); #E' >E' @refl641 ] qed.642 643 lemma lookup_label_rev' : ∀lenv,l,p.644 lookup ?? lenv l = Some ? (lookup_label lenv l p).645 #lenv #l #p @lookup_label_rev [ @p  @refl ]646 qed.647 648 lemma lookup_label_lpresent : ∀lenv,l,p.649 lpresent lenv (lookup_label lenv l p).650 #le #l #p whd %{l} @lookup_label_rev'651 qed.652 653 580 lemma empty_Cminor_labels_added : ∀fx,s,f'. 654 581 labels_of s = [ ] → Cminor_labels_added fx s f'. … … 667 594 Cminor_labels_added … s f'. 668 595 #fx #s #f #f' #INC #ADDED 669 #l #E cases (ADDED l E) #l' * #L #P670 %{l'} % [ @L  @(present_included … P) @INC ] 596 #l #E 597 @(fn_con_labels … INC l (ADDED l E)) 671 598 qed. 672 599 … … 676 603 Cminor_labels_added fx s f'. 677 604 #fx #s #s' #f * #f' * #H1 #H2 #H3 678 #l #E cases (H3 l E) #l' * #L #P 679 %{l'} % [ @L  @(present_included … P) @H1 ] 605 @(Cminor_labels_con … H1) assumption 680 606 qed. 681 607 … … 684 610 Cminor_labels_added … s f → 685 611 Cminor_labels_added … s f'. 686 #fx #s #f * #f' #H1 #H2 687 #l #E cases (H2 l E) #l' * #L #P 688 %{l'} % [ @L  @(present_included … P) @H1 ] 612 #fx #s #f * #f' #H1 @(Cminor_labels_con … H1) 689 613 qed. 690 614 … … 716 640 ] 717 641 ]. 718 [ @mk_add_stmt_inv /2 /642 [ @mk_add_stmt_inv /2 by refl, empty_Cminor_labels_added, fn_con_sig/ 719 643  inversion H #A #B #C destruct 720 644  @mk_add_stmt_inv … … 728 652 ] qed. 729 653 654 (* Record the mapping for a Cminor goto label so that we can put it in the skips 655 for the goto statements later. *) 656 657 definition record_goto_label : ∀fx. partial_fn fx → identifier Label → partial_fn fx ≝ 658 λfx,f,l. mk_partial_fn fx 659 (pf_labgen … f) (pf_reggen … f) (pf_params … f) (pf_locals … f) 660 (pf_result … f) (pf_envok … f) (pf_stacksize … f) (pf_graph … f) 661 (pf_closed … f) (pf_gotos … f) «add … (pf_labels … f) l (pf_entry … f), ?» 662 (pf_typed … f) (pf_entry … f) (pf_exit … f). 663 #l1 #l2 cases (identifier_eq … l2 (pf_entry … f)) 664 [ #E destruct #L @(pi2 … (pf_entry … f)) 665  #NE cases (identifier_eq … l l1) 666 [ #E destruct >lookup_add_hit #E destruct /2/ 667  #NE' >lookup_add_miss [ @(pi2 … (pf_labels … f))  /2/ ] 668 ] 669 ] qed. 670 671 (* Add a dummy statement for each goto so that we can put the real destination 672 in at the end once we've recorded them all. *) 673 674 definition add_goto_dummy : ∀fx. ∀f:partial_fn fx. ∀l. present … (fx_gotos fx) l → Σf':partial_fn fx. fn_contains … f f' ≝ 675 λfx,f,dest,PR. 676 let 〈l,g〉 ≝ fresh … (pf_labgen … f) in 677 (mk_partial_fn fx g (pf_reggen … f) 678 (pf_params … f) (pf_locals … f) (pf_result … f) (pf_envok … f) 679 (pf_stacksize … f) (add ?? (pf_graph … f) l St_return) ? 680 (mk_goto_map … (add … (pf_gotos … f) l dest) ??) 681 «pf_labels … f, ?» ? 682 «l, ?» «pf_exit … f, ?»). 683 [ % [ #l' @lookup_add_oblivious  //  cases (pf_labels fx f) /2/ ] 684  @add_statement_inv @I 685  #l1 #l2 cases (identifier_eq … l1 l) 686 [ #E destruct >lookup_add_hit #E destruct @PR 687  #NE >lookup_add_miss [ @(gm_img … (pf_gotos … f))  // ] 688 ] 689  #id cases (identifier_eq … id l) 690 [ #E destruct // 691  #NE whd in ⊢ (% → %); >lookup_add_miss [ >lookup_add_miss [ @(gm_dom … (pf_gotos … f))  // ]  // ] 692 ] 693  cases (pf_labels … f) #m #PR #l1 #l2 #L @lookup_add_oblivious @(PR … L) 694  @forall_nodes_add // 695  whd >lookup_add_hit % #E destruct 696  @lookup_add_oblivious @(pi2 … (pf_exit …)) 697 ] qed. 698 699 (* It's important for correctness that recursive calls to add_stmt happen in 700 reverse order. This is because Cminor and Clight programs allow goto labels 701 to occur multiple times, but only use the first one to appear in the 702 function. It would be nice to rule these programs out entirely, but that 703 means establishing and maintaining another invariant on Cminor programs, 704 which I'd like to avoid. *) 730 705 731 706 let rec add_stmt (fx:fixed) (s:stmt) (Env:stmts_inv fx s) (f:partial_fn fx) on s : Σf':partial_fn fx. add_stmt_inv fx s f f' ≝ … … 773 748  St_label l s' ⇒ λEnv. 774 749 let f ≝ add_stmt … s' (π2 Env) f in 775 let l' ≝ lookup_label (fx_lenv fx) l ? in 776 «pi1 … (add_to_graph … l' (R_skip (pf_entry … f)) f ??), ?» 750 «record_goto_label … f l, ?» 777 751  St_goto l ⇒ λEnv. 778 let l' ≝ lookup_label (fx_lenv fx) l ? in 779 «pi1 … (add_fresh_to_graph' … (λ_.R_skip l') f ??), ?» 752 «add_goto_dummy … f l ?, ?» 780 753  St_cost l s' ⇒ λEnv. 781 754 let f ≝ add_stmt … s' (π2 Env) f in … … 826 799  #l whd % [2: @(pi2 ?? r)  skip ] 827 800  #l #H @(fn_con_graph … (pi2 ?? l_next)) repeat @fn_contains_step @I 828  @(pi2 … (pf_entry …)) 829  #l1 * [ #E >E %{l'} % [ @lookup_label_rev'  whd >lookup_add_hit % #E' destruct (E') ] 830  @Cminor_labels_sig @(stmt_labels_added ???? (pi2 … f)) 801  cases (pi2 … f) * #INC #ENV #LBLE #LBLA % 802 [ @INC  @ENV  @(extends_dom_trans … LBLE) #l1 #PR whd in ⊢ (???%?); @lookup_add_oblivious @PR ] 803  #l1 * [ #E >E // 804  @(Cminor_labels_con … (stmt_labels_added ???? (pi2 … f))) 805 % [ //  //  #x #PR @lookup_add_oblivious @PR ] 831 806 ] 832 807  @(si_labels … (π1 Env)) 833  #l1 #H whd %2 @lookup_label_lpresent834  @(si_labels … (π1 Env))835 808  @(equal_Cminor_labels_added ?? s') [ @refl  @Cminor_labels_sig @(stmt_labels_added ???? (pi2 … f)) ] 809 ] qed. 810 811 812 813 definition patch_gotos : ∀fx. ∀f:partial_fn fx. 814 (∀l,l'. lookup ?? (pf_gotos … f) l = Some ? l' → present ?? (pf_labels … f) l') → 815 Σf':partial_fn fx. ∀l. present ?? (pf_labels … f) l → present ?? (pf_labels … f') l ≝ 816 λfx,f,PR. 817 fold_inf ? (Σf':partial_fn fx. ∀l. present ?? (pf_labels … f) l → present ?? (pf_labels … f') l) ? (pf_gotos … f) 818 (λl,l',H,f'. «fill_in_statement fx l (St_skip (lookup_present ?? (pf_labels … f') l' ?)) f' ??, ?») 819 «f, λx,H.H». 820 [ #l #PR' @(pi2 … f') @PR' 821  @(pi2 … f') @(PR … H) 822  @(pi2 … (pf_labels … f')) [ @l'  @lookup_lookup_present ] 823  % 836 824 ] qed. 837 825 … … 851 839 let locals ≝ \fst locals_reggen in 852 840 let reggen ≝ \snd locals_reggen in 853 let 〈label_env, labgen1〉 as El ≝ populate_label_env (empty_map …) labgen0 cminor_labels in 854 let 〈l,labgen〉 ≝ fresh … labgen1 in 855 let fixed ≝ mk_fixed label_env env (f_return f) in 841 let 〈l,labgen〉 ≝ fresh … labgen0 in 842 let fixed ≝ mk_fixed (set_of_list … (labels_of (f_body f))) env (f_return f) in 856 843 let emptyfn ≝ 857 844 mk_partial_fn fixed … … 865 852 (add ?? (empty_map …) l St_return) 866 853 ? 854 (mk_goto_map ?? (empty_map …) ??) 855 «empty_map …, ?» 867 856 ? 868 857 l 869 858 l in 870 859 let f ≝ add_stmt fixed (f_body f) ? emptyfn in 860 let f ≝ patch_gotos … f ? in 871 861 mk_internal_function 872 862 (pf_labgen … f) … … 877 867 (pf_stacksize … f) 878 868 (pf_graph … f) 879 ?869 (pf_closed … f) 880 870 (pf_typed … f) 881 871 (pf_entry … f) 882 872 (pf_exit … f) 883 873 . 884 [ #l #s #E @(labels_P_mp … (pf_closed … f l s E)) 885 #l' * [ //  * #l #H cases f #f' * #L #P cases (P l ?) 886 [ #lx >H * #Ex >(?:lx = l') [ 2: destruct (Ex) @refl ] 887 #P' @P' 888  cases (label_env_contents … (sym_eq ??? El) l ?) 889 [ #H @H 890  whd in ⊢ (% → ?); whd in ⊢ (?(??%?) → ?); * #H cases (H (refl ??)) 891  whd >H % #E' destruct (E') 892 ] 893 ] 894 ] 874 [ #l1 #l2 #L 875 lapply (gm_img … (pf_gotos … f) … L) 876 whd in match fixed; 877 #PR 878 lapply (in_set_of_list' … PR) 879 @(stmt_labels_added … (pi2 … f)) 895 880  emptyfn @(stmt_P_mp … (f_inv f)) 896 881 #s * #V #L #R % … … 905 890 ] 906 891  @(stmt_labels_mp … L) 907 #l #H @(populates_label_env … (sym_eq … El)) @H892 #l #H whd in match fixed; @in_set_of_list assumption 908 893  cases s in R ⊢ %; // 909 894 ] … … 923 908  whd in ⊢ (??%? → ?); #E' destruct (E') 924 909 ] 910  #id #l #E normalize in E; destruct 911  #id normalize * #H cases (H (refl ??)) 912  #l #l' normalize #E destruct 925 913  #l #s #LOOKUP cases (lookup_add_cases ??????? LOOKUP) 926 914 [ * #E1 #E2 >E2 @I 927 915  whd in ⊢ (??%? → ?); #E' destruct (E') 928 916 ] 929  6,7: whd >lookup_add_hit % #E destruct917  9,10: whd >lookup_add_hit % #E destruct 930 918  % @refl 931 919 ] 
src/common/Identifiers.ma
r2314 r2335 334 334 [ an_id_map m' ⇒ fold A B (λbv. f (an_identifier ? bv)) m' b ]. 335 335 336 (* An informative, dependentlytyped, fold. *) 337 338 definition fold_inf: 339 ∀A, B: Type[0]. 340 ∀tag: String. 341 ∀m:identifier_map tag A. 342 (∀id:identifier tag. ∀a:A. lookup … m id = Some A a → B → B) → B → B ≝ 343 λA,B,tag,m. 344 match m return λm. (∀id:identifier tag. ∀a:A. lookup … m id = Some A a → B → B) → B → B with 345 [ an_id_map m' ⇒ λf,b. pm_fold_inf A B m' (λbv,a,H. f (an_identifier ? bv) a H) b ]. 346 336 347 (* A predicate that an identifier is in a map, and a failureavoiding lookup 337 348 and update using it. *) … … 518 529 whd >lookup_add_miss // 519 530 qed. 531 532 (* Extending the domain of a map (without necessarily preserving contents). *) 533 534 definition extends_domain : ∀tag,A. identifier_map tag A → identifier_map tag A → Prop ≝ 535 λtag,A,m1,m2. ∀l. present ?? m1 l → present ?? m2 l. 536 537 lemma extends_dom_trans : ∀tag,A,m1,m2,m3. 538 extends_domain tag A m1 m2 → extends_domain tag A m2 m3 → extends_domain tag A m1 m3. 539 #tag #A #m1 #m2 #m3 #H1 #H2 #l #P1 @H2 @H1 @P1 qed. 520 540 521 541 … … 1018 1038 1019 1039 1020 1040 (* Transforming a list into a set. *) 1041 1042 definition set_of_list : ∀tag. list (identifier tag) → identifier_set tag ≝ 1043 λtag,l. foldl ?? (λs,id. add_set tag s id) ∅ l. 1044 1045 lemma fold_add_set_monotone : ∀tag,l,s,id. 1046 present tag unit s id → 1047 present tag unit (foldl ?? (λs,id. add_set tag s id) s l) id. 1048 #tag #l elim l 1049 [ // 1050  #h #t #IH #s #id #PR 1051 whd in ⊢ (???%?); @IH 1052 @lookup_add_oblivious 1053 @PR 1054 ] qed. 1055 1056 lemma in_set_of_list : ∀tag,l,id. 1057 Exists ? (λid'. id' = id) l → 1058 present ?? (set_of_list tag l) id. 1059 #tag #l #id whd in match (set_of_list ??); generalize in match ∅; elim l 1060 [ #s * 1061  #id' #tl #IH #s * 1062 [ #E whd in ⊢ (???%?); destruct 1063 @fold_add_set_monotone // 1064  @IH 1065 ] 1066 ] qed. 1067 1068 lemma in_set_of_list' : ∀tag,l,id. 1069 present ?? (set_of_list tag l) id → 1070 Exists ? (λid'. id = id') l. 1071 #tag #l #id whd in match (set_of_list ??); 1072 cut (¬present ?? ∅ id) [ /3/ ] 1073 generalize in match ∅; 1074 elim l 1075 [ #s #F #T @⊥ @(absurd … T F) 1076  #id' #tl #IH #s #F #PR whd in PR:(???%?); 1077 cases (identifier_eq … id id') 1078 [ #E destruct /2/ 1079  #NE %2 @(IH … PR) 1080 @(not_to_not … F) /2/ 1081 ] 1082 ] qed. 1083 1084 1085 
src/common/PositiveMap.ma
r2307 r2335 567 567 ] qed. 568 568 569 569 (* An "informative" dependently typed fold *) 570 571 let rec pm_fold_inf_aux 572 (A, B: Type[0]) 573 (t: positive_map A) 574 (f: ∀p:Pos. ∀a:A. lookup_opt … p t = Some A a → B → B) 575 (t': positive_map A) 576 (pre: Pos → Pos) 577 (b: B) on t': (∀p. lookup_opt … p t' = lookup_opt … (pre p) t) → B ≝ 578 match t' return λt'. (∀p. lookup_opt A p t' = lookup_opt A (pre p) t) → B with 579 [ pm_leaf ⇒ λ_. b 580  pm_node a l r ⇒ λH. 581 let b ≝ match a return λa. lookup_opt A one (pm_node A a ??) = ? → B with [ None ⇒ λ_.b  Some a ⇒ λH. f (pre one) a ? b ] (H one) in 582 let b ≝ pm_fold_inf_aux A B t f l (λx. pre (p0 x)) b ? in 583 pm_fold_inf_aux A B t f r (λx. pre (p1 x)) b ? 584 ]. 585 [ #p @(H (p1 p))  #p @(H (p0 p))  <H % ] 586 qed. 587 588 definition pm_fold_inf : ∀A, B: Type[0]. ∀t: positive_map A. 589 ∀f: (∀p:Pos. ∀a:A. lookup_opt … p t = Some A a → B → B). B → B ≝ 590 λA,B,t,f,b. pm_fold_inf_aux A B t f t (λx.x) b (λp. refl ??). 591
Note: See TracChangeset
for help on using the changeset viewer.