Changeset 1316 for src/Cminor/toRTLabs.ma
 Timestamp:
 Oct 7, 2011, 12:26:39 PM (9 years ago)
 Location:
 src
 Files:

 2 edited
Legend:
 Unmodified
 Added
 Removed

src

Property
svn:mergeinfo
set to
/Deliverables/D3.3/idlookupbranch merged eligible

Property
svn:mergeinfo
set to

src/Cminor/toRTLabs.ma
r1224 r1316 3 3 include "Cminor/syntax.ma". 4 4 include "RTLabs/syntax.ma". 5 include "utilities/pair.ma". 6 include "utilities/deppair.ma". 5 7 6 8 definition env ≝ identifier_map SymbolTag register. 7 definition label_env ≝ identifier_map SymbolTaglabel.9 definition label_env ≝ identifier_map Label label. 8 10 definition populate_env : env → universe RegisterTag → list (ident × typ) → list (register×typ) × env × (universe RegisterTag) ≝ 9 11 λen,gen. foldr ?? … … 14 16 〈〈r,ty〉::rs, add ?? en id r, gen'〉) 〈[ ], en, gen〉. 15 17 16 definition populate_label_env : label_env → universe LabelTag → list ident → label_env × (universe LabelTag) ≝ 18 lemma populates_env : ∀l,e,u,l',e',u'. 19 populate_env e u l = 〈l',e',u'〉 → 20 ∀i. Exists ? (λx.\fst x = i) l → 21 present ?? e' i. 22 #l elim l 23 [ #e #u #l' #e' #u' #E whd in E:(??%?); #i destruct (E) * 24  * #id #t #tl #IH #e #u #l' #e' #u' #E #i whd in E:(??%?) ⊢ (% → ?); 25 * [ whd in ⊢ (??%? → ?) #E1 <E1 26 generalize in E:(??(match % with [ _ ⇒ ? ])?) ⊢ ? * * #x #y #z 27 whd in ⊢ (??%? → ?) elim (fresh RegisterTag z) #r #gen' #E 28 whd in E:(??%?); 29 >(?:e' = add ?? y id r) [ 2: destruct (E) @refl ] (* XXX workaround because destruct overnormalises *) 30 whd >lookup_add_hit % #A destruct 31  #H change in E:(??(match % with [ _ ⇒ ? ])?) with (populate_env e u tl) 32 lapply (refl ? (populate_env e u tl)) 33 cases (populate_env e u tl) in (*E:%*) ⊢ (???% → ?) (* XXX if I do this directly it rewrites both sides of the equality *) 34 * #rs #e1 #u1 #E1 >E1 in E; whd in ⊢ (??%? → ?) cases (fresh RegisterTag u1) #r #u'' 35 whd in ⊢ (??%? → ?) #E 36 >(?:e' = add ?? e1 id r) [ 2: destruct (E) @refl ] (* XXX workaround because destruct overnormalises *) 37 @lookup_add_oblivious 38 @(IH … E1 ? H) 39 ] 40 ] qed. 41 42 lemma populate_extends : ∀l,e,u,l',e',u'. 43 populate_env e u l = 〈l',e',u'〉 → 44 ∀i. present ?? e i → present ?? e' i. 45 #l elim l 46 [ #e #u #l' #e' #u' #E whd in E:(??%?); destruct // 47  * #id #t #tl #IH #e #u #l' #e' #u' #E whd in E:(??%?); 48 change in E:(??(match % with [ _ ⇒ ?])?) with (populate_env e u tl) 49 lapply (refl ? (populate_env e u tl)) 50 cases (populate_env e u tl) in (*E:%*) ⊢ (???% → ?) * #l0 #e0 #u0 #E0 51 >E0 in E; whd in ⊢ (??%? → ?) cases (fresh RegisterTag u0) #i1 #u1 #E 52 whd in E:(??%?) 53 >(?:e' = add ?? e0 id i1) [ 2: destruct (E) @refl ] 54 #i #H @lookup_add_oblivious @(IH … E0) @H 55 ] qed. 56 57 definition populate_label_env : label_env → universe LabelTag → list (identifier Label) → label_env × (universe LabelTag) ≝ 17 58 λen,gen. foldr ?? 18 59 (λid,engen. … … 21 62 〈add ?? en id r, gen'〉) 〈en, gen〉. 22 63 23 lemma lookup_sigma : ∀tag,A,m. ∀i:(Σl:identifier tag. lookup tag A m l ≠ None ?). 24 lookup tag A m i ≠ None ?. 25 #tag #A #m * #i #H @H 26 qed. 64 lemma populates_label_env : ∀ls,lbls,u,lbls',u'. 65 populate_label_env lbls u ls = 〈lbls',u'〉 → 66 ∀l. Exists ? (λl'.l' = l) ls → present ?? lbls' l. 67 #ls elim ls 68 [ #lbls #u #lbls' #u' #E #l * 69  #h #t #IH #lbls #u #lbls' #u' whd in ⊢ (??%? → ?) 70 change in ⊢ (??match % with [ _ ⇒ ? ]? → ?) with (populate_label_env ???) 71 lapply (refl ? (populate_label_env lbls u t)) 72 cases (populate_label_env lbls u t) in ⊢ (???% → %) 73 #lbls1 #u1 #E1 whd in ⊢ (??%? → ?) cases (fresh ? u1) #r #gen' whd in ⊢ (??%? → ?) 74 #E >(?:lbls' = add ?? lbls1 h r) [ 2: destruct (E) @refl ] 75 #l * 76 [ #El <El whd >lookup_add_hit % #Er destruct 77  #H @lookup_add_oblivious @(IH … E1 ? H) 78 ] 79 ] qed. 80 81 lemma label_env_contents : ∀ls,lbls,u,lbls',u'. 82 populate_label_env lbls u ls = 〈lbls',u'〉 → 83 ∀l. present ?? lbls' l → Exists ? (λl'.l = l') ls ∨ present ?? lbls l. 84 #ls elim ls 85 [ #lbls #u #lbls' #u' #E #l #H %2 whd in E:(??%?); destruct @H 86  #h #t #IH #lbls #u #lbls' #u' whd in ⊢ (??%? → ?) 87 change in ⊢ (??match % with [ _ ⇒ ? ]? → ?) with (populate_label_env ???) 88 lapply (refl ? (populate_label_env lbls u t)) 89 cases (populate_label_env lbls u t) in ⊢ (???% → %) 90 #lbls1 #u1 #E1 whd in ⊢ (??%? → ?) cases (fresh ? u1) #r #gen' whd in ⊢ (??%? → ?) 91 #E >(?:lbls' = add ?? lbls1 h r) [ 2: destruct (E) @refl ] 92 #l #H cases (identifier_eq ? l h) 93 [ #El %1 %1 @El 94  #NE cases (IH … E1 l ?) 95 [ #H' %1 %2 @H'  #H' %2 @H'  whd in H >lookup_add_miss in H // @eq_identifier_elim // #E cases NE /2/ ] 96 ] 97 ] qed. 98 99 definition lookup_reg : ∀e:env. ∀id. present ?? e id → register ≝ lookup_present ??. 100 definition lookup_label : ∀e:label_env. ∀id. present ?? e id → label ≝ lookup_present ??. 101 102 (* Check that the domain of one graph is included in another, for monotonicity 103 properties. Note that we don't say anything about the statements. *) 104 definition graph_included : graph statement → graph statement → Prop ≝ 105 λg1,g2. ∀l. present ?? g1 l → present ?? g2 l. 106 107 lemma graph_inc_trans : ∀g1,g2,g3. 108 graph_included g1 g2 → graph_included g2 g3 → graph_included g1 g3. 109 #g1 #g2 #g3 #H1 #H2 #l #P1 @H2 @H1 @P1 qed. 110 111 definition lpresent ≝ λlbls:label_env. λl. ∃l'. lookup ?? lbls l' = Some ? l. 112 113 definition partially_closed : label_env → graph statement → Prop ≝ 114 λe,g. ∀l,s. lookup ?? g l = Some ? s → labels_P (λl. present ?? g l ∨ lpresent e l) s. 115 116 (* I'd use a single parametrised definition along with internal_function, but 117 it's a pain without implicit parameters. *) 118 record partial_fn (lenv:label_env) : Type[0] ≝ 119 { pf_labgen : universe LabelTag 120 ; pf_reggen : universe RegisterTag 121 ; pf_result : option (register × typ) 122 ; pf_params : list (register × typ) 123 ; pf_locals : list (register × typ) 124 ; pf_stacksize : nat 125 ; pf_graph : graph statement 126 ; pf_closed : partially_closed lenv pf_graph 127 ; pf_entry : Σl:label. present ?? pf_graph l 128 ; pf_exit : Σl:label. present ?? pf_graph l 129 }. 130 131 inductive fn_graph_included (le:label_env) (f1:partial_fn le) (f2:partial_fn le) : Prop ≝ 132  fn_graph_inc : graph_included (pf_graph ? f1) (pf_graph ? f2) → fn_graph_included le f1 f2. 133 134 lemma fn_graph_inc_trans : ∀le,f1,f2,f3. 135 fn_graph_included le f1 f2 → fn_graph_included le f2 f3 → fn_graph_included le f1 f3. 136 #le #f1 #f2 #f3 * #H1 * #H2 % @(graph_inc_trans … H1 H2) qed. 137 138 lemma fn_graph_included_refl : ∀label_env,f. 139 fn_graph_included label_env f f. 140 #le #f % #l #H @H qed. 141 142 lemma fn_graph_included_sig : ∀label_env,f,f0. 143 ∀f':Σf':partial_fn label_env. fn_graph_included ? f0 f'. 144 fn_graph_included label_env f f0 → 145 fn_graph_included label_env f f'. 146 #le #f #f0 * #f' #H1 #H2 @(fn_graph_inc_trans … H2 H1) 147 qed. 148 149 lemma add_statement_inv : ∀le,l,s.∀f. 150 labels_present (pf_graph le f) s → 151 partially_closed le (add … (pf_graph ? f) l s). 152 #le #l #s #f #p 153 #l' #s' #H cases (identifier_eq … l l') 154 [ #E >E in H >lookup_add_hit #E' <(?:s = s') [2:destruct //] 155 @(labels_P_mp … p) #l0 #H %1 @lookup_add_oblivious @H 156  #NE @(labels_P_mp … (pf_closed ? f l' s' ?)) 157 [ #lx * [ #H %1 @lookup_add_oblivious @H  #H %2 @H ] 158  >lookup_add_miss in H // @eq_identifier_elim // #E cases NE /2/ 159 ] 160 ] qed. 27 161 28 162 (* Add a statement to the graph, *without* updating the entry label. *) 29 definition fill_in_statement : label → statement → internal_function → internal_function ≝ 30 λl,s,f. 31 mk_internal_function (f_labgen f) (f_reggen f) 32 (f_result f) (f_params f) (f_locals f) 33 (f_stacksize f) (add ?? (f_graph f) l s) 34 (dp ?? (f_entry f) ?) (dp ?? (f_exit f) ?). 35 @lookup_add_oblivious @lookup_sigma 36 qed. 163 definition fill_in_statement : ∀le. label → ∀s:statement. ∀f:partial_fn le. labels_present (pf_graph ? f) s → Σf':partial_fn le. fn_graph_included le f f' ≝ 164 λle,l,s,f,p. 165 mk_partial_fn le (pf_labgen ? f) (pf_reggen ? f) 166 (pf_result ? f) (pf_params ? f) (pf_locals ? f) 167 (pf_stacksize ? f) (add ?? (pf_graph ? f) l s) ? 168 «pf_entry ? f, ?» «pf_exit ? f, ?». 169 [ @add_statement_inv @p 170  2,3: @lookup_add_oblivious @use_sig 171  % #l' @lookup_add_oblivious 172 ] qed. 37 173 38 174 (* Add a statement to the graph, making it the entry label. *) 39 definition add_to_graph : label → statement → internal_function → internal_function ≝ 40 λl,s,f. 41 mk_internal_function (f_labgen f) (f_reggen f) 42 (f_result f) (f_params f) (f_locals f) 43 (f_stacksize f) (add ?? (f_graph f) l s) 44 (dp ?? l ?) (dp ?? (f_exit f) ?). 45 [ >lookup_add_hit % #E destruct 46  @lookup_add_oblivious @lookup_sigma 175 definition add_to_graph : ∀le. label → ∀s:statement. ∀f:partial_fn le. labels_present (pf_graph ? f) s → Σf':partial_fn le. fn_graph_included le f f' ≝ 176 λle,l,s,f,p. 177 mk_partial_fn le (pf_labgen ? f) (pf_reggen ? f) 178 (pf_result ? f) (pf_params ? f) (pf_locals ? f) 179 (pf_stacksize ? f) (add ?? (pf_graph ? f) l s) ? 180 «l, ?» «pf_exit ? f, ?». 181 [ @add_statement_inv @p 182  whd >lookup_add_hit % #E destruct 183  @lookup_add_oblivious @use_sig 184  % #l' @lookup_add_oblivious 47 185 ] qed. 48 186 49 187 (* Add a statement with a fresh label to the start of the function. The 50 188 statement is parametrised by the *next* instruction's label. *) 51 definition add_fresh_to_graph : (label → statement) → internal_function → internal_function ≝ 52 λs,f. 53 let 〈l,g〉 ≝ fresh … (f_labgen f) in 54 let s' ≝ s (f_entry f) in 55 (mk_internal_function g (f_reggen f) 56 (f_result f) (f_params f) (f_locals f) 57 (f_stacksize f) (add ?? (f_graph f) l s') 58 (dp ?? l ?) (dp ?? (f_exit f) ?)). 59 [ >lookup_add_hit % #E destruct 60  @lookup_add_oblivious @lookup_sigma 61 ] qed. 62 63 definition fresh_reg : internal_function → typ → register × internal_function ≝ 64 λf,ty. 65 let 〈r,g〉 ≝ fresh … (f_reggen f) in 66 〈r, mk_internal_function (f_labgen f) g 67 (f_result f) (f_params f) (〈r,ty〉::(f_locals f)) 68 (f_stacksize f) (f_graph f) (f_entry f) (f_exit f)〉. 189 definition add_fresh_to_graph : ∀le. ∀s:(label → statement). ∀f:partial_fn le. (∀l. present ?? (pf_graph ? f) l → labels_present (pf_graph ? f) (s l)) → Σf':partial_fn le. fn_graph_included le f f' ≝ 190 λle,s,f,p. 191 let 〈l,g〉 ≝ fresh … (pf_labgen ? f) in 192 let s' ≝ s (pf_entry ? f) in 193 (mk_partial_fn le g (pf_reggen ? f) 194 (pf_result ? f) (pf_params ? f) (pf_locals ? f) 195 (pf_stacksize ? f) (add ?? (pf_graph ? f) l s') ? 196 «l, ?» «pf_exit ? f, ?»). 197 [ % #l' @lookup_add_oblivious 198  @add_statement_inv @p @use_sig 199  whd >lookup_add_hit % #E destruct 200  @lookup_add_oblivious @use_sig 201 ] qed. 202 203 (* Variants for labels which are (goto) labels *) 204 205 lemma add_statement_inv' : ∀le,l,s.∀f. 206 labels_P (λl. present ?? (pf_graph le f) l ∨ lpresent le l) s → 207 partially_closed le (add … (pf_graph ? f) l s). 208 #le #l #s #f #p 209 #l' #s' #H cases (identifier_eq … l l') 210 [ #E >E in H >lookup_add_hit #E' <(?:s = s') [2:destruct //] 211 @(labels_P_mp … p) #l0 * [ #H %1 @lookup_add_oblivious @H  #H %2 @H ] 212  #NE @(labels_P_mp … (pf_closed ? f l' s' ?)) 213 [ #lx * [ #H %1 @lookup_add_oblivious @H  #H %2 @H ] 214  >lookup_add_miss in H // @eq_identifier_elim // #E cases NE /2/ 215 ] 216 ] qed. 217 218 definition add_fresh_to_graph' : ∀le. ∀s:(label → statement). ∀f:partial_fn le. (∀l. present ?? (pf_graph ? f) l → labels_P (λl.present ?? (pf_graph ? f) l ∨ lpresent le l) (s l)) → Σf':partial_fn le. fn_graph_included le f f' ≝ 219 λle,s,f,p. 220 let 〈l,g〉 ≝ fresh … (pf_labgen ? f) in 221 let s' ≝ s (pf_entry ? f) in 222 (mk_partial_fn le g (pf_reggen ? f) 223 (pf_result ? f) (pf_params ? f) (pf_locals ? f) 224 (pf_stacksize ? f) (add ?? (pf_graph ? f) l s') ? 225 «l, ?» «pf_exit ? f, ?»). 226 [ % #l' @lookup_add_oblivious 227  @add_statement_inv' @p @use_sig 228  whd >lookup_add_hit % #E destruct 229  @lookup_add_oblivious @use_sig 230 ] qed. 231 232 definition fresh_reg : ∀le. ∀f:partial_fn le. typ → register × (Σf':partial_fn le. fn_graph_included le f f') ≝ 233 λle,f,ty. 234 let 〈r,g〉 ≝ fresh … (pf_reggen ? f) in 235 〈r, «mk_partial_fn le (pf_labgen ? f) g 236 (pf_result ? f) (pf_params ? f) (〈r,ty〉::(pf_locals ? f)) 237 (pf_stacksize ? f) (pf_graph ? f) (pf_closed ? f) (pf_entry ? f) (pf_exit ? f), ?»〉. 238 % #l // qed. 69 239 70 240 axiom UnknownVariable : String. 71 241 72 definition choose_reg : env → ∀ty.expr ty → internal_function → res (register × internal_function) ≝ 73 λenv,ty,e,f. 74 match e with 75 [ Id _ i ⇒ 76 do r ← opt_to_res … [MSG UnknownVariable; CTX ? i] (lookup … env i); 77 OK ? 〈r, f〉 78  _ ⇒ 79 OK ? (fresh_reg f ty) 242 definition choose_reg : ∀le. ∀env:env.∀ty.∀e:expr ty. ∀f:partial_fn le. expr_vars ty e (present ?? env) → register × (Σf':partial_fn le. fn_graph_included le f f') ≝ 243 λle,env,ty,e,f. 244 match e return λty,e. expr_vars ty e (present ?? env) → register × (Σf':partial_fn le. fn_graph_included le f f') with 245 [ Id _ i ⇒ λEnv. 〈lookup_reg env i Env, «f, ?»〉 246  _ ⇒ λ_.fresh_reg le f ty 80 247 ]. 81 82 definition choose_regs : env → list (Σt:typ.expr t) → internal_function → res (list register × internal_function) ≝ 83 λenv,es,f. 84 foldr (Σt:typ.expr t) ? 85 (λe,acc. do 〈rs,f〉 ← acc; 86 do 〈r,f'〉 ← match e with [ dp t e ⇒ choose_reg env t e f ]; 87 OK ? 〈r::rs,f'〉) (OK ? 〈[ ], f〉) es. 248 % // qed. 249 250 let rec foldr_all (A,B:Type[0]) (P:A → Prop) (f:∀a:A. P a → B → B) (b:B) (l:list A) (H:All ? P l) on l :B ≝ 251 match l return λx.All ? P x → B with [ nil ⇒ λ_. b  cons a l ⇒ λH. f a (proj1 … H) (foldr_all A B P f b l (proj2 … H))] H. 252 253 definition exprtyp_present ≝ λenv:env.λe:Σt:typ.expr t.match e with [ dp ty e ⇒ expr_vars ty e (present ?? env) ]. 254 255 definition choose_regs : ∀le. ∀env:env. ∀es:list (Σt:typ.expr t). 256 ∀f:partial_fn le. All ? (exprtyp_present env) es → 257 list register × (Σf':partial_fn le. fn_graph_included le f f') ≝ 258 λle,env,es,f,Env. 259 foldr_all (Σt:typ.expr t) ?? 260 (λe,p,acc. let 〈rs,f〉 ≝ acc in 261 let 〈r,f'〉 ≝ match e return λe.? → ? with [ dp t e ⇒ λp.choose_reg le env t e (eject … f) ? ] p in 262 〈r::rs,«eject … f', ?»〉) 〈[ ], «f, ?»〉 es Env. 263 [ @p 264  @fn_graph_inc_trans [ 3: @(use_sig ?? f')  skip  @(use_sig ?? f) ] 265  % // 266 ] qed. 267 268 lemma extract_pair : ∀A,B,C,D. ∀u:A×B. ∀Q:A → B → C×D. ∀x,y. 269 ((let 〈a,b〉 ≝ u in Q a b) = 〈x,y〉) → 270 ∃a,b. 〈a,b〉 = u ∧ Q a b = 〈x,y〉. 271 #A #B #C #D * #a #b #Q #x #y normalize #E1 %{a} %{b} % try @refl @E1 qed. 272 273 274 lemma choose_regs_length : ∀le,env,es,f,p,rs,f'. 275 choose_regs le env es f p = 〈rs,f'〉 → es = rs. 276 #le #env #es #f elim es 277 [ #p #rs #f normalize #E destruct @refl 278  * #ty #e #t #IH #p #rs #f' whd in ⊢ (??%? → ??%?) #E 279 cases (extract_pair ???????? E) #rs' * #f'' * #E1 #E2 E; 280 cases (extract_pair ???????? E2) #r * #f3 * #E3 #E4 E2; 281 destruct (E4) skip (E1 E3) @eq_f @IH 282 [ @(proj2 … p) 283  3: @sym_eq @E1 284  2: skip 285 ] 286 ] qed. 287 288 lemma present_inc : ∀le,f,l. 289 ∀f':Σf':partial_fn le. fn_graph_included le f f'. 290 present ?? (pf_graph le f) l → 291 present ?? (pf_graph le f') l. 292 #le #f #l * #f' * #H1 #H2 @H1 @H2 qed. 88 293 89 294 axiom BadCminorProgram : String. 90 295 91 let rec add_expr ( env:env) (ty:typ) (e:expr ty) (dst:register) (f:internal_function) on e: res internal_function≝92 match e with93 [ Id _ i ⇒ 94 do r ← opt_to_res … [MSG UnknownVariable; CTX ? i] (lookup ?? env i);296 let rec add_expr (le:label_env) (env:env) (ty:typ) (e:expr ty) (Env:expr_vars ty e (present ?? env)) (dst:register) (f:partial_fn le) on e: Σf':partial_fn le. fn_graph_included le f f' ≝ 297 match e return λty,e.expr_vars ty e (present ?? env) → Σf':partial_fn le. fn_graph_included le f f' with 298 [ Id _ i ⇒ λEnv. 299 let r ≝ lookup_reg env i Env in 95 300 match register_eq r dst with 96 [ inl _ ⇒ OK ? f97  inr _ ⇒ OK ? (add_fresh_to_graph (St_op1 Oid dst r) f)301 [ inl _ ⇒ «f, ?» 302  inr _ ⇒ «eject … (add_fresh_to_graph ? (St_op1 Oid dst r) f ?), ?» 98 303 ] 99  Cst _ c ⇒ OK ? (add_fresh_to_graph (St_const dst c) f) 100  Op1 _ _ op e' ⇒ 101 do 〈r,f〉 ← choose_reg env ? e' f; 102 let f ≝ add_fresh_to_graph (St_op1 op dst r) f in 103 add_expr env ? e' r f 104  Op2 _ _ _ op e1 e2 ⇒ 105 do 〈r1,f〉 ← choose_reg env ? e1 f; 106 do 〈r2,f〉 ← choose_reg env ? e2 f; 107 let f ≝ add_fresh_to_graph (St_op2 op dst r1 r2) f in 108 do f ← add_expr env ? e2 r2 f; 109 add_expr env ? e1 r1 f 110  Mem _ _ q e' ⇒ 111 do 〈r,f〉 ← choose_reg env ? e' f; 112 let f ≝ add_fresh_to_graph (St_load q r dst) f in 113 add_expr env ? e' r f 114  Cond _ _ _ e' e1 e2 ⇒ 115 let resume_at ≝ f_entry f in 116 do f ← add_expr env ? e2 dst f; 117 let lfalse ≝ f_entry f in 118 let f ≝ add_fresh_to_graph (λ_.St_skip resume_at) f in 119 do f ← add_expr env ? e1 dst f; 120 do 〈r,f〉 ← choose_reg env ? e' f; 121 let f ≝ add_fresh_to_graph (λltrue. St_cond r ltrue lfalse) f in 122 add_expr env ? e' r f 123  Ecost _ l e' ⇒ 124 do f ← add_expr env ? e' dst f; 125 OK ? (add_fresh_to_graph (St_cost l) f) 126 ]. 127 128 (* This shouldn't occur; maybe use vectors? *) 129 axiom WrongNumberOfArguments : String. 130 131 let rec add_exprs (env:env) (es:list (Σt:typ.expr t)) (dsts:list register) (f:internal_function) on es: res internal_function ≝ 132 match es with 133 [ nil ⇒ match dsts with [ nil ⇒ OK ? f  cons _ _ ⇒ Error ? (msg WrongNumberOfArguments) ] 134  cons e et ⇒ 135 match dsts with 136 [ nil ⇒ Error ? (msg WrongNumberOfArguments) 137  cons r rt ⇒ 138 do f ← add_exprs env et rt f; 139 match e with [ dp ty e ⇒ add_expr env ty e r f ] 304  Cst _ c ⇒ λ_. «add_fresh_to_graph ? (St_const dst c) f ?, ?» 305  Op1 _ _ op e' ⇒ λEnv. 306 let 〈r,f〉 ≝ choose_reg ? env ? e' f Env in 307 let f ≝ add_fresh_to_graph ? (St_op1 op dst r) f ? in 308 let f ≝ add_expr ? env ? e' Env r f in 309 «eject … f, ?» 310  Op2 _ _ _ op e1 e2 ⇒ λEnv. 311 let 〈r1,f〉 ≝ choose_reg ? env ? e1 f (proj1 … Env) in 312 let 〈r2,f〉 ≝ choose_reg ? env ? e2 f (proj2 … Env) in 313 let f ≝ add_fresh_to_graph ? (St_op2 op dst r1 r2) f ? in 314 let f ≝ add_expr ? env ? e2 (proj2 … Env) r2 f in 315 let f ≝ add_expr ? env ? e1 (proj1 … Env) r1 f in 316 «eject … f, ?» 317  Mem _ _ q e' ⇒ λEnv. 318 let 〈r,f〉 ≝ choose_reg ? env ? e' f Env in 319 let f ≝ add_fresh_to_graph ? (St_load q r dst) f ? in 320 let f ≝ add_expr ? env ? e' Env r f in 321 «eject … f, ?» 322  Cond _ _ _ e' e1 e2 ⇒ λEnv. 323 let resume_at ≝ pf_entry ? f in 324 let f ≝ add_expr ? env ? e2 (proj2 … Env) dst f in 325 let lfalse ≝ pf_entry ? f in 326 let f ≝ add_fresh_to_graph ? (λ_.St_skip resume_at) f ? in 327 let f ≝ add_expr ? env ? e1 (proj2 … (proj1 … Env)) dst f in 328 let 〈r,f〉 as E ≝ choose_reg ? env ? e' f (proj1 … (proj1 … Env)) in 329 let f ≝ add_fresh_to_graph ? (λltrue. St_cond r ltrue lfalse) f ? in 330 let f ≝ add_expr ? env ? e' (proj1 … (proj1 … Env)) r f in 331 «eject … f, ?» 332  Ecost _ l e' ⇒ λEnv. 333 let f ≝ add_expr ? env ? e' Env dst f in 334 let f ≝ add_fresh_to_graph ? (St_cost l) f ? in 335 «f, ?» 336 ] Env. 337 (* For new labels, we need to step back through the definitions of f until we 338 hit the point that it was added. *) 339 try @fn_graph_included_refl 340 try (#l #H @H) 341 [ 7: #l #H whd % [ @H  342 @present_inc 343 @present_inc 344 @present_inc 345 @(use_sig ? (present ???)) ] 346  8: #l #H 347 @present_inc 348 @(use_sig ? (present ???)) 349 (* For the monotonicity properties, we just keep going back until we're at the 350 start. The repeat tactical helps here. *) 351  *: repeat @fn_graph_included_sig @fn_graph_included_refl 352 ] qed. 353 354 let rec add_exprs (le:label_env) (env:env) (es:list (Σt:typ.expr t)) (Env:All ? (exprtyp_present env) es) 355 (dsts:list register) (pf:es=dsts) (f:partial_fn le) on es: Σf':partial_fn le. fn_graph_included le f f' ≝ 356 match es return λes.All ?? es → es=dsts → ? with 357 [ nil ⇒ λ_. match dsts return λx. ?=x → Σf':partial_fn le. fn_graph_included le f f' with [ nil ⇒ λ_. «f, ?»  cons _ _ ⇒ λpf.⊥ ] 358  cons e et ⇒ λEnv. 359 match dsts return λx. ?=x → ? with 360 [ nil ⇒ λpf.⊥ 361  cons r rt ⇒ λpf. 362 let f ≝ add_exprs ? env et ? rt ? f in 363 match e return λe.exprtyp_present ? e → ? with [ dp ty e ⇒ λEnv. 364 let f ≝ add_expr ? env ty e ? r f in 365 «eject … f, ?» ] (proj1 ?? Env) 140 366 ] 141 ]. 367 ] Env pf. 368 [ // 369  2,3: normalize in pf; destruct 370  @fn_graph_included_sig @fn_graph_included_sig @fn_graph_included_refl 371  @Env 372  @(proj2 … Env) 373  normalize in pf; destruct @e0 ] qed. 142 374 143 375 axiom UnknownLabel : String. 144 376 axiom ReturnMismatch : String. 145 377 146 let rec add_stmt (env:env) (label_env:label_env) (s:stmt) (exits:list label) (f:internal_function) on s : res internal_function ≝ 147 match s with 148 [ St_skip ⇒ OK ? f 149  St_assign _ x e ⇒ 150 do dst ← opt_to_res … [MSG UnknownVariable; CTX ? x] (lookup ?? env x); 151 add_expr env ? e dst f 152  St_store _ _ q e1 e2 ⇒ 153 do 〈val_reg, f〉 ← choose_reg env ? e2 f; 154 do 〈addr_reg, f〉 ← choose_reg env ? e1 f; 155 let f ≝ add_fresh_to_graph (St_store q addr_reg val_reg) f in 156 do f ← add_expr env ? e1 addr_reg f; 157 add_expr env ? e2 val_reg f 158  St_call return_opt_id e args ⇒ 159 do return_opt_reg ← 160 match return_opt_id with 161 [ None ⇒ OK ? (None ?) 162  Some id ⇒ do r ← opt_to_res … [MSG UnknownVariable; CTX ? id] (lookup ?? env id); OK ? (Some ? r) 163 ]; 164 do 〈args_regs, f〉 ← choose_regs env args f; 165 do f ← 166 match e with 167 [ Id _ id ⇒ OK ? (add_fresh_to_graph (St_call_id id args_regs return_opt_reg) f) 168  _ ⇒ 169 do 〈fnr, f〉 ← choose_reg env ? e f; 170 let f ≝ add_fresh_to_graph (St_call_ptr fnr args_regs return_opt_reg) f in 171 add_expr env ? e fnr f 172 ]; 173 add_exprs env args args_regs f 174  St_tailcall e args ⇒ 175 do 〈args_regs, f〉 ← choose_regs env args f; 176 do f ← 177 match e with 178 [ Id _ id ⇒ OK ? (add_fresh_to_graph (λ_. St_tailcall_id id args_regs) f) 179  _ ⇒ 180 do 〈fnr, f〉 ← choose_reg env ? e f; 181 let f ≝ add_fresh_to_graph (λ_. St_tailcall_ptr fnr args_regs) f in 182 add_expr env ? e fnr f 183 ]; 184 add_exprs env args args_regs f 185  St_seq s1 s2 ⇒ 186 do f ← add_stmt env label_env s2 exits f; 187 add_stmt env label_env s1 exits f 188  St_ifthenelse _ _ e s1 s2 ⇒ 189 let l_next ≝ f_entry f in 190 do f ← add_stmt env label_env s2 exits f; 191 let l2 ≝ f_entry f in 192 let f ≝ add_fresh_to_graph ? (* XXX: fails, but works if applied afterwards: λ_. St_skip l_next*) f in 193 do f ← add_stmt env label_env s1 exits f; 194 do 〈r,f〉 ← choose_reg env ? e f; 195 let f ≝ add_fresh_to_graph (λl1. St_cond r l1 l2) f in 196 add_expr env ? e r f 197  St_loop s ⇒ 198 let f ≝ add_fresh_to_graph ? f in (* dummy statement, fill in afterwards *) 199 let l_loop ≝ f_entry f in 200 do f ← add_stmt env label_env s exits f; 201 OK ? (fill_in_statement l_loop (* XXX another odd failure: St_skip (f_entry f)*)? f) 202  St_block s ⇒ 203 add_stmt env label_env s ((f_entry f)::exits) f 204  St_exit n ⇒ 205 do l ← opt_to_res … (msg BadCminorProgram) (nth_opt ? n exits); 206 OK ? (add_fresh_to_graph (* XXX another: λ_. St_skip l*)? f) 207  St_switch sz sg e tab n ⇒ 208 do 〈r,f〉 ← choose_reg env ? e f; 209 do l_default ← opt_to_res … (msg BadCminorProgram) (nth_opt ? n exits); 210 let f ≝ add_fresh_to_graph (* XXX grrrr: λ_. St_skip l_default*)? f in 211 do f ← foldr ?? (λcs,f. 378 definition stmt_inv : env → label_env → stmt → Prop ≝ 379 λenv,lenv. stmt_P (λs. stmt_vars (present ?? env) s ∧ stmt_labels (present ?? lenv) s). 380 381 (* Trick to avoid multiplying the proof obligations for the nonId cases. *) 382 definition expr_is_Id : ∀t. expr t → option ident ≝ 383 λt,e. match e with 384 [ Id _ id ⇒ Some ? id 385  _ ⇒ None ? 386 ]. 387 388 (* XXX Work around odd disambiguation errors. *) 389 alias id "R_skip" = "cic:/matita/cerco/RTLabs/syntax/statement.con(0,1,0)". 390 alias id "R_return" = "cic:/matita/cerco/RTLabs/syntax/statement.con(0,14,0)". 391 392 definition nth_sig : ∀A. ∀P:A → Prop. errmsg → (Σl:list A. All A P l) → nat → res (Σa:A. P a) ≝ 393 λA,P,m,l,n. 394 match nth_opt A n l return λx.(∀_.x = ? → ?) → ? with 395 [ None ⇒ λ_. Error ? m 396  Some a ⇒ λH'. OK ? «a, ?» 397 ] (All_nth A P n l (use_sig … l)). 398 @H' @refl qed. 399 400 lemma lookup_label_rev : ∀lenv,l,l',p. 401 lookup_label lenv l p = l' → lookup ?? lenv l = Some ? l'. 402 #lenv #l #l' #p 403 cut (∃lx. lookup ?? lenv l = Some ? lx) 404 [ whd in p; cases (lookup ?? lenv l) in p ⊢ % 405 [ * #H cases (H (refl ??)) 406  #lx #_ %{lx} @refl 407 ] 408  * #lx #E whd in ⊢ (??%? → ?) cases p >E #q whd in ⊢ (??%? → ?) #E' >E' @refl 409 ] qed. 410 411 lemma lookup_label_rev' : ∀lenv,l,p. 412 lookup ?? lenv l = Some ? (lookup_label lenv l p). 413 #lenv #l #p @lookup_label_rev [ @p  @refl ] 414 qed. 415 416 lemma lookup_label_lpresent : ∀lenv,l,p. 417 lpresent lenv (lookup_label lenv l p). 418 #le #l #p whd %{l} @lookup_label_rev' 419 qed. 420 421 (* We need to show that the graph only grows, and that Cminor labels will end 422 up in the graph. *) 423 definition Cminor_labels_added ≝ λle,s,f'. 424 ∀l. Exists ? (λl'.l=l') (labels_of s) → 425 ∃l'. lookup ?? le l = Some ? l' ∧ present ?? (pf_graph le f') l'. 426 427 record add_stmt_inv (le:label_env) (s:stmt) (f:partial_fn le) (f':partial_fn le) : Prop ≝ 428 { stmt_graph_inc : fn_graph_included ? f f' 429 ; stmt_labels_added : Cminor_labels_added le s f' 430 }. 431 432 lemma empty_Cminor_labels_added : ∀le,s,f'. 433 labels_of s = [ ] → Cminor_labels_added le s f'. 434 #le #s #f' #E whd >E #l *; 435 qed. 436 437 lemma equal_Cminor_labels_added : ∀le,s,s',f. 438 labels_of s = labels_of s' → Cminor_labels_added le s' f → 439 Cminor_labels_added le s f. 440 #le #s #s' #f #E whd in ⊢ (% → %) > E #H @H 441 qed. 442 443 lemma fn_graph_included_inv : ∀label_env,s,f,f0. 444 ∀f':Σf':partial_fn label_env. add_stmt_inv label_env s f0 f'. 445 fn_graph_included label_env f f0 → 446 fn_graph_included label_env f f'. 447 #label_env #s #f #f0 * #f' * #H1 #H2 #H3 448 @(fn_graph_inc_trans … H3 H1) 449 qed. 450 451 lemma present_inc' : ∀le,s,f,l. 452 ∀f':(Σf':partial_fn le. add_stmt_inv le s f f'). 453 present ?? (pf_graph le f) l → 454 present ?? (pf_graph le f') l. 455 #le #s #f #l * #f' * * #H1 #H2 #H3 456 @H1 @H3 457 qed. 458 459 lemma Cminor_labels_inv : ∀le,s,s',f. 460 ∀f':Σf':partial_fn le. add_stmt_inv le s' f f'. 461 Cminor_labels_added le s f → 462 Cminor_labels_added le s f'. 463 #le #s #s' #f * #f' * #H1 #H2 #H3 464 #l #E cases (H3 l E) #l' * #L #P 465 %{l'} % [ @L  @present_inc' @P ] 466 qed. 467 468 lemma Cminor_labels_sig : ∀le,s,f. 469 ∀f':Σf':partial_fn le. fn_graph_included le f f'. 470 Cminor_labels_added le s f → 471 Cminor_labels_added le s f'. 472 #le #s #f * #f' #H1 #H2 473 #l #E cases (H2 l E) #l' * #L #P 474 %{l'} % [ @L  @present_inc @P ] 475 qed. 476 477 let rec add_stmt (env:env) (label_env:label_env) (s:stmt) (Env:stmt_inv env label_env s) (f:partial_fn label_env) (exits:Σls:list label. All ? (present ?? (pf_graph ? f)) ls) on s : res (Σf':partial_fn label_env. add_stmt_inv label_env s f f') ≝ 478 match s return λs.stmt_inv env label_env s → res (Σf':partial_fn label_env. add_stmt_inv ? s f f') with 479 [ St_skip ⇒ λ_. OK ? «f, ?» 480  St_assign _ x e ⇒ λEnv. 481 let dst ≝ lookup_reg env x (π1 (π1 Env)) in 482 OK ? «eject … (add_expr ? env ? e (π2 (π1 Env)) dst f), ?» 483  St_store _ _ q e1 e2 ⇒ λEnv. 484 let 〈val_reg, f〉 ≝ choose_reg ? env ? e2 f (π2 (π1 Env)) in 485 let 〈addr_reg, f〉 ≝ choose_reg ? env ? e1 f (π1 (π1 Env)) in 486 let f ≝ add_fresh_to_graph ? (St_store q addr_reg val_reg) f ? in 487 let f ≝ add_expr ? env ? e1 (π1 (π1 Env)) addr_reg f in 488 OK ? «eject … (add_expr ? env ? e2 (π2 (π1 Env)) val_reg f), ?» 489  St_call return_opt_id e args ⇒ λEnv. 490 let return_opt_reg ≝ 491 match return_opt_id return λo. ? → ? with 492 [ None ⇒ λ_. None ? 493  Some id ⇒ λEnv. Some ? (lookup_reg env id ?) 494 ] Env in 495 let 〈args_regs, f〉 as Eregs ≝ choose_regs ? env args f (π2 (π1 Env)) in 496 let f ≝ 497 match expr_is_Id ? e with 498 [ Some id ⇒ add_fresh_to_graph ? (St_call_id id args_regs return_opt_reg) f ? 499  None ⇒ 500 let 〈fnr, f〉 ≝ choose_reg ? env ? e f (π2 (π1 (π1 Env))) in 501 let f ≝ add_fresh_to_graph ? (St_call_ptr fnr args_regs return_opt_reg) f ? in 502 «eject … (add_expr ? env ? e (π2 (π1 (π1 Env))) fnr f), ?» 503 ] in 504 OK ? «eject … (add_exprs ? env args (π2 (π1 Env)) args_regs ? f), ?» 505  St_tailcall e args ⇒ λEnv. 506 let 〈args_regs, f〉 as Eregs ≝ choose_regs ? env args f (π2 (π1 Env)) in 507 let f ≝ 508 match expr_is_Id ? e with 509 [ Some id ⇒ add_fresh_to_graph ? (λ_. St_tailcall_id id args_regs) f ? 510  None ⇒ 511 let 〈fnr, f〉 ≝ choose_reg ? env ? e f (π1 (π1 Env)) in 512 let f ≝ add_fresh_to_graph ? (λ_. St_tailcall_ptr fnr args_regs) f ? in 513 «eject … (add_expr ? env ? e (π1 (π1 Env)) fnr f), ?» 514 ] in 515 OK ? «eject … (add_exprs ? env args (π2 (π1 Env)) args_regs ? f), ?» 516  St_seq s1 s2 ⇒ λEnv. 517 do f2 ← add_stmt env label_env s2 ? f «exits, ?»; 518 do f1 ← add_stmt env label_env s1 ? f2 «exits, ?»; 519 OK ? «eject … f1, ?» 520  St_ifthenelse _ _ e s1 s2 ⇒ λEnv. 521 let l_next ≝ pf_entry ? f in 522 do f2 ← add_stmt env label_env s2 (π2 Env) f «exits, ?»; 523 let l2 ≝ pf_entry ? f2 in 524 let f ≝ add_fresh_to_graph ? (λ_. R_skip l_next) f2 ? in 525 do f1 ← add_stmt env label_env s1 (π2 (π1 Env)) f «exits, ?»; 526 let 〈r,f〉 ≝ choose_reg ? env ? e f1 (π1 (π1 (π1 Env))) in 527 let f ≝ add_fresh_to_graph ? (λl1. St_cond r l1 l2) f ? in 528 OK ? «eject … (add_expr ? env ? e (π1 (π1 (π1 Env))) r f), ?» 529  St_loop s ⇒ λEnv. 530 let f ≝ add_fresh_to_graph ? R_skip f ? in (* dummy statement, fill in afterwards *) 531 let l_loop ≝ pf_entry ? f in 532 do f ← add_stmt env label_env s (π2 Env) f «exits, ?»; 533 OK ? «eject … (fill_in_statement ? l_loop (R_skip (pf_entry ? f)) f ?), ?» 534  St_block s ⇒ λEnv. 535 do f ← add_stmt env label_env s (π2 Env) f («pf_entry ? f::exits, ?»); 536 OK ? «eject … f, ?» 537  St_exit n ⇒ λEnv. 538 do l ← nth_sig ?? (msg BadCminorProgram) exits n; 539 OK ? «eject … (add_fresh_to_graph ? (λ_. R_skip l) f ?), ?» 540  St_switch sz sg e tab n ⇒ λEnv. 541 let 〈r,f〉 ≝ choose_reg ? env ? e f ? in 542 do l_default ← nth_sig ?? (msg BadCminorProgram) exits n; 543 let f ≝ add_fresh_to_graph ? (λ_. R_skip l_default) f ? in 544 do f ← foldr ? (res (Σf':partial_fn ?. ?)) (λcs,f. 212 545 do f ← f; 213 546 let 〈i,n〉 ≝ cs in 214 547 let 〈cr,f〉 ≝ fresh_reg … f (ASTint sz sg) in 215 548 let 〈br,f〉 ≝ fresh_reg … f (ASTint I8 Unsigned) in 216 do l_case ← opt_to_res … (msg BadCminorProgram) (nth_opt ? n exits); 217 let f ≝ add_fresh_to_graph (St_cond br l_case) f in 218 let f ≝ add_fresh_to_graph (St_op2 (Ocmpu Ceq) (* signed? *) br r cr) f in 219 OK ? (add_fresh_to_graph (St_const cr (Ointconst ? i)) f)) (OK ? f) tab; 220 add_expr env ? e r f 221  St_return opt_e ⇒ 222 let f ≝ add_fresh_to_graph (λ_. St_return) f in 223 match opt_e with 224 [ None ⇒ OK ? f 225  Some e ⇒ 226 match f_result f with 227 [ None ⇒ Error ? (msg ReturnMismatch) 228  Some r ⇒ match e with [ dp ty e ⇒ add_expr env ? e (\fst r) f ] 549 do l_case ← nth_sig ?? (msg BadCminorProgram) exits n; 550 let f ≝ add_fresh_to_graph ? (St_cond br l_case) f ? in 551 let f ≝ add_fresh_to_graph ? (St_op2 (Ocmpu Ceq) (* signed? *) br r cr) f ? in 552 let f ≝ add_fresh_to_graph ? (St_const cr (Ointconst ? i)) f ? in 553 OK ? «eject … f, ?») (OK ? f) tab; 554 OK ? «eject … (add_expr ? env ? e (π1 Env) r f), ?» 555  St_return opt_e ⇒ let f0 ≝ f in 556 let f ≝ add_fresh_to_graph ? (λ_. R_return) f ? in 557 match opt_e return λo. stmt_inv ?? (St_return o) → res (Σf':partial_fn label_env.add_stmt_inv ? (St_return o) f0 f') with 558 [ None ⇒ λEnv. OK ? «eject … f, ?» 559  Some e ⇒ 560 match pf_result ? f with 561 [ None ⇒ λEnv. Error ? (msg ReturnMismatch) 562  Some r ⇒ 563 match e return λe.stmt_inv env label_env (St_return (Some ? e)) → res (Σf':partial_fn label_env.add_stmt_inv label_env (St_return (Some ? e)) f0 f') with 564 [ dp ty e ⇒ λEnv. let f ≝ add_expr label_env env ty e ? (\fst r) f in 565 OK ? «eject … f, ?» ] 229 566 ] 230 567 ] 231  St_label l s' ⇒ 232 do f ← add_stmt env label_env s' exits f; 233 do l' ← opt_to_res … [MSG UnknownLabel; CTX ? l] (lookup ?? label_env l); 234 OK ? (add_to_graph l' (* XXX again: St_skip (f_entry f)*)? f) 235  St_goto l ⇒ 236 do l' ← opt_to_res … [MSG UnknownLabel; CTX ? l] (lookup ?? label_env l); 237 OK ? (add_fresh_to_graph (* XXX again: λ_.St_skip l'*)? f) 238  St_cost l s' ⇒ 239 do f ← add_stmt env label_env s' exits f; 240 OK ? (add_fresh_to_graph (St_cost l) f) 241 ]. 242 [ @(λ_. St_skip l_next) 243  @(St_skip (f_entry f)) 244  @St_skip 245  @(λ_. St_skip l) 246  @(λ_. St_skip l_default) 247  @(St_skip (f_entry f)) 248  @(λ_.St_skip l') 249 ] qed. 250 251 (* Get labels from a Cminor statement. *) 252 let rec labels_of (s:stmt) : list ident ≝ 253 match s with 254 [ St_seq s1 s2 ⇒ (labels_of s1) @ (labels_of s2) 255  St_ifthenelse _ _ _ s1 s2 ⇒ (labels_of s1) @ (labels_of s2) 256  St_loop s ⇒ labels_of s 257  St_block s ⇒ labels_of s 258  St_label l s ⇒ l::(labels_of s) 259  St_cost _ s ⇒ labels_of s 260  _ ⇒ [ ] 261 ]. 568  St_label l s' ⇒ λEnv. 569 do f ← add_stmt env label_env s' (π2 Env) f exits; 570 let l' ≝ lookup_label label_env l ? in 571 OK ? «eject … (add_to_graph ? l' (R_skip (pf_entry ? f)) f ?), ?» 572  St_goto l ⇒ λEnv. 573 let l' ≝ lookup_label label_env l ? in 574 OK ? «eject … (add_fresh_to_graph' ? (λ_.R_skip l') f ?), ?» 575  St_cost l s' ⇒ λEnv. 576 do f ← add_stmt env label_env s' (π2 Env) f exits; 577 OK ? «eject … (add_fresh_to_graph ? (St_cost l) f ?), ?» 578 ] Env. 579 try @(π1 Env) 580 try @(π2 Env) 581 try @(π1 (π1 Env)) 582 try @(π2 (π1 Env)) 583 try @mk_add_stmt_inv 584 try (@empty_Cminor_labels_added @refl) 585 try (@(All_mp … (use_sig ?? exits))) 586 try @fn_graph_included_refl 587 try (repeat @fn_graph_included_inv repeat @fn_graph_included_sig @fn_graph_included_refl) 588 try (#l #H @I) 589 try (#l #H @H) 590 [ f @(choose_regs_length … (sym_eq … Eregs)) 591  @fn_graph_included_sig @fn_graph_included_sig @fn_graph_included_sig @fn_graph_included_refl 592  whd in Env @(π1 (π1 (π1 Env))) 593  f @(choose_regs_length … (sym_eq … Eregs)) 594  @fn_graph_included_sig @fn_graph_included_sig @fn_graph_included_sig @fn_graph_included_refl 595  #l #H cases (Exists_append … H) 596 [ #H1 @(stmt_labels_added ???? (use_sig ?? f1) ? H1) 597  #H2 @(Cminor_labels_inv … H2) @(stmt_labels_added ???? (use_sig ?? f2)) 598 ] 599  #l #H @present_inc' @H 600  #l #H @present_inc' @use_sig 601  @fn_graph_included_sig @fn_graph_included_sig @fn_graph_included_sig @fn_graph_included_inv @fn_graph_included_sig @fn_graph_included_inv @fn_graph_included_refl 602  #l #H cases (Exists_append … H) 603 [ #H1 @(Cminor_labels_sig … H1) @Cminor_labels_sig @Cminor_labels_sig @(stmt_labels_added ???? (use_sig ?? f1)) 604  #H2 @(Cminor_labels_sig … H2) @Cminor_labels_sig @Cminor_labels_sig @Cminor_labels_inv @Cminor_labels_sig @(stmt_labels_added ???? (use_sig ?? f2)) 605 ] 606  #l #H % [ @H  @present_inc @present_inc' @present_inc @(use_sig ?? (pf_entry ? f2)) ] 607  #l #H @present_inc @present_inc' @H 608  #l #H @present_inc @H 609  @(use_sig ?? (pf_entry ??)) 610  @fn_graph_included_sig @fn_graph_included_inv @fn_graph_included_sig @fn_graph_included_refl 611  @Cminor_labels_sig @(equal_Cminor_labels_added ?? s) [ @refl  @(stmt_labels_added ???? (use_sig ? (add_stmt_inv ???) ?)) ] 612  % [ @use_sig  @(use_sig ?? exits) ] 613  @(equal_Cminor_labels_added ?? s) [ @refl  @(stmt_labels_added ???? (use_sig ? (add_stmt_inv ???) ?)) ] 614  #l #H @use_sig 615  #l #H @present_inc @use_sig 616  #l #H % [ @present_inc @present_inc @present_inc @present_inc @use_sig  @H ] 617  @fn_graph_included_sig @fn_graph_included_sig @fn_graph_included_sig @fn_graph_included_sig @fn_graph_included_sig @fn_graph_included_sig @fn_graph_included_refl 618  @use_sig 619  @fn_graph_included_sig @fn_graph_included_inv @fn_graph_included_refl 620  #l1 * [ #E >E %{l'} % [ @lookup_label_rev'  whd >lookup_add_hit % #E' destruct (E') ] 621 @Cminor_labels_sig @(stmt_labels_added ???? (use_sig ? (add_stmt_inv ???) ?)) 622 ] 623  #l1 #H whd %2 @lookup_label_lpresent 624  @fn_graph_included_sig @fn_graph_included_inv @fn_graph_included_refl 625  @(equal_Cminor_labels_added ?? s') [ @refl  @Cminor_labels_sig @(stmt_labels_added ???? (use_sig ? (add_stmt_inv ???) ?)) ] 626 ] qed. 627 628 (* 629 definition mk_fn : ∀le. partial_fn le → internal_function ≝ 630 λle, f. 631 mk_internal_function 632 (pf_labgen ? f) 633 (pf_reggen ? f) 634 (pf_result ? f) 635 (pf_params ? f) 636 (pf_locals ? f) 637 (pf_stacksize ? f) 638 (pf_graph ? f) 639 ? 640 (pf_entry ? f) 641 (pf_exit ? f). 642 #l #s #E @(labels_P_mp … (pf_closed ? f l s E)) 643 #l' * [ //  #H 644 *) 262 645 263 646 definition c2ra_function (*: internal_function → internal_function*) ≝ … … 266 649 let reggen0 ≝ new_universe RegisterTag in 267 650 let cminor_labels ≝ labels_of (f_body f) in 268 let 〈params, env1, reggen1〉 ≝ populate_env (empty_map …) reggen0 (f_params f) in269 let 〈locals0, env, reggen2〉 ≝ populate_env env1 reggen1 (f_vars f) in651 let 〈params, env1, reggen1〉 as E1 ≝ populate_env (empty_map …) reggen0 (f_params f) in 652 let 〈locals0, env, reggen2〉 as E2 ≝ populate_env env1 reggen1 (f_vars f) in 270 653 let 〈result, locals, reggen〉 ≝ 271 654 match f_return f with … … 274 657 let 〈r,gen〉 ≝ fresh … reggen2 in 275 658 〈Some ? 〈r,ty〉, 〈r,ty〉::locals0, gen〉 ] in 276 let 〈label_env, labgen1〉 ≝ populate_label_env (empty_map …) labgen0 cminor_labels in659 let 〈label_env, labgen1〉 as El ≝ populate_label_env (empty_map …) labgen0 cminor_labels in 277 660 let 〈l,labgen〉 ≝ fresh … labgen1 in 278 661 let emptyfn ≝ 279 mk_internal_function 662 mk_partial_fn 663 label_env 280 664 labgen 281 665 reggen … … 285 669 (f_stacksize f) 286 670 (add ?? (empty_map …) l St_return) 671 ? 287 672 l 288 673 l in 289 do f ← add_stmt env label_env (f_body f) [ ] emptyfn; 290 do u1 ← check_universe_ok ? (f_labgen f); 291 do u2 ← check_universe_ok ? (f_reggen f); 292 OK ? f 293 . 294 >lookup_add_hit % #E destruct 674 do f ← add_stmt env label_env (f_body f) ? emptyfn [ ]; 675 do u1 ← check_universe_ok ? (pf_labgen ? f); 676 do u2 ← check_universe_ok ? (pf_reggen ? f); 677 OK ? (mk_internal_function 678 (pf_labgen ? f) 679 (pf_reggen ? f) 680 (pf_result ? f) 681 (pf_params ? f) 682 (pf_locals ? f) 683 (pf_stacksize ? f) 684 (pf_graph ? f) 685 ? 686 (pf_entry ? f) 687 (pf_exit ? f) 688 ). 689 [ @I 690  emptyfn @(stmt_P_mp … (f_inv f)) 691 #s * #V #L % 692 [ @(stmt_vars_mp … V) 693 #i #H cases (Exists_append … H) 694 [ #H1 @(populate_extends ?????? (sym_eq … E2)) 695 @(populates_env … (sym_eq … E1)) @H1 696  #H1 @(populates_env … (sym_eq … E2)) @H1 697 ] 698  @(stmt_labels_mp … L) 699 #l #H @(populates_label_env … (sym_eq … El)) @H 700 ] 701  #l #s #E @(labels_P_mp … (pf_closed ? f l s E)) 702 #l' * [ //  * #l #H cases f #f' * #L #P cases (P l ?) 703 [ #lx >H * #Ex >(?:lx = l') [ 2: destruct (Ex) @refl ] 704 #P' @P' 705  cases (label_env_contents … (sym_eq ??? El) l ?) 706 [ #H @H 707  whd in ⊢ (% → ?) whd in ⊢ (?(??%?) → ?) * #H cases (H (refl ??)) 708  whd >H % #E' destruct (E') 709 ] 710 ] 711 ] 712  #l1 #s #LOOKUP cases (lookup_add_cases ??????? LOOKUP) 713 [ * #E1 #E2 >E2 @I 714  whd in ⊢ (??%? → ?) #E' destruct (E') 715 ] 716  *: whd >lookup_add_hit % #E destruct 717 ] 295 718 qed. 296 719
Note: See TracChangeset
for help on using the changeset viewer.