Changeset 2335


Ignore:
Timestamp:
Sep 20, 2012, 6:57:34 PM (7 years ago)
Author:
campbell
Message:

Deal with goto labels in RTLabs to Cminor by fixing up goto statements
after the main translation to avoid generating extra skips in awkward
locations.

Location:
src
Files:
3 edited

Legend:

Unmodified
Added
Removed
  • src/Cminor/toRTLabs.ma

    r2319 r2335  
    55
    66definition env ≝ identifier_map SymbolTag (register × typ).
    7 definition label_env ≝ identifier_map Label label.
    87definition populate_env : env → universe RegisterTag → list (ident × typ) → list (register×typ) × env × (universe RegisterTag) ≝
    98λen,gen. foldr ??
     
    132131] qed.
    133132
    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 in
    138    let 〈r,gen'〉 ≝ fresh … gen in
    139      〈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 ls
    145 [ #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 destruct
    153   #l *
    154   [ #El <El whd >lookup_add_hit % #Er destruct
    155   | #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 ls
    163 [ #lbls #u #lbls' #u' #E #l #H %2 whd in E:(??%?); destruct @H
    164 | #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 destruct
    171   #l #H cases (identifier_eq ? l h)
    172   [ #El %1 %1 @El
    173   | #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 
    180133(* Check that the domain of one graph is included in another, for monotonicity
    181134   properties.  Note that we don't say anything about the statements. *)
    182135definition graph_included : graph statement → graph statement → Prop ≝
    183 λg1,g2. ∀l. present ?? g1 l → present ?? g2 l.
     136extends_domain ??.
    184137
    185138lemma graph_inc_trans : ∀g1,g2,g3.
    186139  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
     141qed.
     142
    193143
    194144(* Some data structures for the transformation that remain fixed throughout. *)
    195145record fixed : Type[0] ≝ {
    196   fx_lenv   : label_env;
     146  fx_gotos  : identifier_set Label;
    197147  fx_env    : env;
    198148  fx_rettyp : option typ
     
    202152λty,env.
    203153  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
     160record 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}.
    204165
    205166(* I'd use a single parametrised definition along with internal_function, but
     
    214175; pf_stacksize : nat
    215176; 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'
    217180; pf_typed     : graph_typed (pf_locals @ pf_params) pf_graph
    218181; pf_entry     : Σl:label. present ?? pf_graph l
     
    223186  λfx,f. env_has (pf_locals fx f @ pf_params fx f).
    224187
     188(* TODO: move or use another definition if there's already one *)
     189definition 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
     192lemma 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/
     197qed.
     198
    225199record fn_contains (fx:fixed) (f1:partial_fn fx) (f2:partial_fn fx) : Prop ≝
    226200{ fn_con_graph : graph_included (pf_graph … f1) (pf_graph … f2)
    227201; 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)
    228203}.
    229204
     
    233208[ @(graph_inc_trans … (fn_con_graph … H1) (fn_con_graph … H2))
    234209| #r #ty #H @(fn_con_env … H2) @(fn_con_env … H1) @H
     210| @(extends_dom_trans … (fn_con_labels … H1) (fn_con_labels … H2))
    235211] qed.
    236212
     
    248224lemma add_statement_inv : ∀fx,l,s.∀f.
    249225  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).
    251227#fx #l #s #f #p
    252228#l' #s' #H cases (identifier_eq … l l')
    253229[ #E >E in H; >lookup_add_hit #E' <(?:s = s') [2:destruct //]
    254   @(labels_P_mp … p) #l0 #H %1 @lookup_add_oblivious @H
     230  @(labels_P_mp … p) #l0 #H @lookup_add_oblivious @H
    255231| #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
    257233  | >lookup_add_miss in H; /2/
    258234  ]
     
    279255  mk_partial_fn fx (pf_labgen … f) (pf_reggen … f)
    280256                (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, ?» ?
    282259                «pf_entry … f, ?» «pf_exit … f, ?».
    283260[ @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)
    284264| @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/ ]
    287267] qed.
    288268
     
    295275  mk_partial_fn fx (pf_labgen … f) (pf_reggen … f)
    296276                (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) ????
    298278                «l, ?» «pf_exit … f, ?».
    299279[ @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)
    300283| @forall_nodes_add //
    301284| whd >lookup_add_hit % #E destruct
    302285| @lookup_add_oblivious @(pi2 … (pf_exit … f))
    303 | % [ #l' @lookup_add_oblivious | // ]
     286| % [ #l' @lookup_add_oblivious | // | cases (pf_labels fx f) /2/ ]
    304287] qed.
    305288
     
    315298    (mk_partial_fn fx g (pf_reggen … f)
    316299                   (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') ????
    318301                   «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/ ]
    320304| @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 ]
    354307| @forall_nodes_add //
    355308| whd >lookup_add_hit % #E destruct
     
    385338    «mk_partial_fn fx
    386339       (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), ?»
    388341  in
    389342    ❬f' , ?(*«r, ?»*)❭.
     
    392345| #i #t #r1 #H #L %2 @(pf_envok … f … L)
    393346| 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 | // ]
    395348] qed.
    396349
     
    437390]  qed.
    438391
    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 
    445392lemma choose_regs_length : ∀fx,es,f,p,f',rs.
    446393  choose_regs fx es f p = ❬f',rs❭ → |es| = length … rs.
     
    452399  present ?? (pf_graph … f) l →
    453400  present ?? (pf_graph … f') l.
    454 #fx #f #f' #l * #H1 #H2 @H1 qed.
     401#fx #f #f' #l * #H1 #H2 #H3 @H1 qed.
    455402
    456403(* Some definitions for the add_stmt function later, which we introduce now so
     
    460407   up in the graph. *)
    461408definition 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.
    464410
    465411record add_stmt_inv (fx:fixed) (s:stmt) (f:partial_fn fx) (f':partial_fn fx) : Prop ≝
     
    609555λt,s. match s with [ St_return oe ⇒ rettyp_match t oe | _ ⇒ True ].
    610556
     557(* Invariants about Cminor statements that we'll need *)
     558
    611559record stmt_inv (fx:fixed) (s:stmt) : Prop ≝ {
    612560  si_vars : stmt_vars (Env_has (fx_env fx)) s;
    613   si_labels : stmt_labels (present ?? (fx_lenv fx)) s;
     561  si_labels : stmt_labels (present ?? (fx_gotos fx)) s;
    614562  si_return : return_ok (fx_rettyp fx) s
    615563}.
     
    630578alias id "R_return" = "cic:/matita/cerco/RTLabs/syntax/statement.con(0,11,0)".
    631579
    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' #p
    635 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} @refl
    639   ]
    640 | * #lx #E whd in ⊢ (??%? → ?); cases p >E #q whd in ⊢ (??%? → ?); #E' >E' @refl
    641 ] 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 
    653580lemma empty_Cminor_labels_added : ∀fx,s,f'.
    654581  labels_of s = [ ] → Cminor_labels_added fx s f'.
     
    667594  Cminor_labels_added … s f'.
    668595#fx #s #f #f' #INC #ADDED
    669 #l #E cases (ADDED l E) #l' * #L #P
    670 %{l'} % [ @L | @(present_included … P) @INC ]
     596#l #E
     597@(fn_con_labels … INC l (ADDED l E))
    671598qed.
    672599
     
    676603  Cminor_labels_added fx s f'.
    677604#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
    680606qed.
    681607
     
    684610  Cminor_labels_added … s f →
    685611  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)
    689613qed.
    690614
     
    716640    ]
    717641  ].
    718 [ @mk_add_stmt_inv /2/
     642[ @mk_add_stmt_inv /2 by refl, empty_Cminor_labels_added, fn_con_sig/
    719643| inversion H #A #B #C destruct
    720644| @mk_add_stmt_inv
     
    728652] qed.
    729653
     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
     657definition 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
     674definition 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. *)
    730705
    731706let 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' ≝
     
    773748| St_label l s' ⇒ λEnv.
    774749    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, ?»
    777751| 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 ?, ?»
    780753| St_cost l s' ⇒ λEnv.
    781754    let f ≝ add_stmt … s' (π2 Env) f in
     
    826799| #l whd % [2: @(pi2 ?? r) | skip ]
    827800| #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 ]
    831806        ]
    832807| @(si_labels … (π1 Env))
    833 | #l1 #H whd %2 @lookup_label_lpresent
    834 | @(si_labels … (π1 Env))
    835808| @(equal_Cminor_labels_added ?? s') [ @refl | @Cminor_labels_sig @(stmt_labels_added ???? (pi2 … f)) ]
     809] qed.
     810
     811
     812
     813definition 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.
     817fold_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| %
    836824] qed.
    837825
     
    851839let locals ≝ \fst locals_reggen in
    852840let 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
     841let 〈l,labgen〉 ≝ fresh … labgen0 in
     842let fixed ≝ mk_fixed (set_of_list … (labels_of (f_body f))) env (f_return f) in
    856843let emptyfn ≝
    857844  mk_partial_fn fixed
     
    865852    (add ?? (empty_map …) l St_return)
    866853    ?
     854    (mk_goto_map ?? (empty_map …) ??)
     855    «empty_map …, ?»
    867856    ?
    868857    l
    869858    l in
    870859let f ≝ add_stmt fixed (f_body f) ? emptyfn in
     860let f ≝ patch_gotos … f ? in
    871861  mk_internal_function
    872862    (pf_labgen … f)
     
    877867    (pf_stacksize … f)
    878868    (pf_graph … f)
    879     ?
     869    (pf_closed … f)
    880870    (pf_typed … f)
    881871    (pf_entry … f)
    882872    (pf_exit … f)
    883873  .
    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))
    895880| -emptyfn @(stmt_P_mp … (f_inv f))
    896881  #s * #V #L #R %
     
    905890    ]
    906891  | @(stmt_labels_mp … L)
    907     #l #H @(populates_label_env … (sym_eq … El)) @H
     892    #l #H whd in match fixed; @in_set_of_list assumption
    908893  | cases s in R ⊢ %; //
    909894  ]
     
    923908  | whd in ⊢ (??%? → ?); #E' destruct (E')
    924909  ]
     910| #id #l #E normalize in E; destruct
     911| #id normalize * #H cases (H (refl ??))
     912| #l #l' normalize #E destruct
    925913| #l #s #LOOKUP cases (lookup_add_cases ??????? LOOKUP)
    926914  [ * #E1 #E2 >E2 @I
    927915  | whd in ⊢ (??%? → ?); #E' destruct (E')
    928916  ]
    929 | 6,7: whd >lookup_add_hit % #E destruct
     917| 9,10: whd >lookup_add_hit % #E destruct
    930918| % @refl
    931919]
  • src/common/Identifiers.ma

    r2314 r2335  
    334334  [ an_id_map m' ⇒ fold A B (λbv. f (an_identifier ? bv)) m' b ].
    335335
     336(* An informative, dependently-typed, fold. *)
     337
     338definition 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
    336347(* A predicate that an identifier is in a map, and a failure-avoiding lookup
    337348   and update using it. *)
     
    518529whd >lookup_add_miss //
    519530qed.
     531
     532(* Extending the domain of a map (without necessarily preserving contents). *)
     533
     534definition 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
     537lemma 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.
    520540
    521541
     
    10181038
    10191039
    1020 
     1040(* Transforming a list into a set. *)
     1041
     1042definition set_of_list : ∀tag. list (identifier tag) → identifier_set tag ≝
     1043λtag,l. foldl ?? (λs,id. add_set tag s id) ∅ l.
     1044
     1045lemma 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
     1056lemma 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
     1068lemma 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 ??);
     1072cut (¬present ?? ∅ id) [ /3/ ]
     1073generalize in match ∅;
     1074elim 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  
    567567] qed.
    568568
    569 
     569(* An "informative" dependently typed fold *)
     570
     571let 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 ≝
     578match 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 % ]
     586qed.
     587
     588definition 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.