Changeset 2252 for src/Cminor
- Timestamp:
- Jul 24, 2012, 7:40:21 PM (9 years ago)
- Location:
- src/Cminor
- Files:
-
- 3 edited
Legend:
- Unmodified
- Added
- Removed
-
src/Cminor/initialisation.ma
r2251 r2252 38 38 ] 39 39 ]. 40 % / 2/40 % /3/ 41 41 cases init in p; [ 7: | 8: #a #b | *: #a ] #p normalize in p; 42 destruct;/ 3/42 destruct;/4 by stmt_labels_mp, conj/ 43 43 qed. 44 44 … … 50 50 〈off + (size_init_data datum), St_seq (init_datum id r datum off) s〉) 51 51 〈0, mk_Sig ? (λx.stmt_inv x) St_skip ?〉 init). 52 [ % / 2/52 [ % /3/ 53 53 | elim init 54 [ % /2/ 55 | #h #t #IH whd in ⊢ (?(???%)); @breakup_pair whd in ⊢ (?%); 56 % [ % [ % /2/ | @(pi2 … (init_datum …)) ] | @IH ] 54 [ % /3/ 55 | #h #t #IH whd in ⊢ (?(???%)); @breakup_pair 56 % 57 [ /3/ 58 | % [ @(pi2 … (init_datum …)) | @IH ] 59 ] 57 60 ] qed. 58 61 59 62 definition init_vars : list (ident × region × (list init_data)) → Σs:stmt. stmt_inv s ≝ 60 63 λvars. foldr ? (Σs:stmt. stmt_inv s) 61 (λvar,s. mk_Sig ? (λx.stmt_inv x ) (St_seq s (init_var (\fst (\fst var)) (\snd (\fst var)) (\snd var))) ?) (mk_Sig ? (λx.stmt_inv x ) St_skip (conj ?? (conj ?? I I) I)) vars. 62 % [ % [ % /2/ | @(pi2 … s) ] | @(pi2 … (init_var …)) ] 63 qed. 64 (λvar,s. mk_Sig ? (λx.stmt_inv x ) (St_seq s (init_var (\fst (\fst var)) (\snd (\fst var)) (\snd var))) ?) (mk_Sig ? (λx.stmt_inv x ) St_skip ?) vars. 65 [ % [ /3/ | % [ @(pi2 … s) | @(pi2 … (init_var …)) ] ] 66 | /4/ 67 ] qed. 64 68 65 69 lemma no_labels : ∀s. stmt_inv s → labels_of s = [ ]. 66 70 #s elim s // 67 [ #s1 #s2 #IH1 #IH2 * * * * #_ #_ #_#H1 #H2 whd in ⊢ (??%?);71 [ #s1 #s2 #IH1 #IH2 * #_ * #H1 #H2 whd in ⊢ (??%?); 68 72 >(IH1 H1) >(IH2 H2) @refl 69 | #sz #sg #e #s1 #s2 #IH1 #IH2 * * * #_ #_#H1 #H2 whd in ⊢ (??%?);73 | #sz #sg #e #s1 #s2 #IH1 #IH2 * #_ * #H1 #H2 whd in ⊢ (??%?); 70 74 >(IH1 H1) >(IH2 H2) @refl 71 75 | #l #s #IH * * * #_ * 72 | #l #s #IH * * #_#_ #H @(IH H)76 | #l #s #IH * #_ #H @(IH H) 73 77 ] qed. 74 78 … … 95 99 | inr _ ⇒ 〈id',f'〉 ]) ]. 96 100 % 97 [ % [ % // | 98 @(stmt_P_mp … H) #s * * #V #L #R % 99 [ @(stmt_vars_mp … V) #i #t * 100 | @(stmt_labels_mp … L) #l * 101 | cases s in R ⊢ %; // #x * 101 [ % // 102 | % 103 [ @(stmt_P_mp … H) #s * * #V #L #R % 104 [ @(stmt_vars_mp … V) #i #t * 105 | @(stmt_labels_mp … L) #l * 106 | cases s in R ⊢ %; // #x * 107 ] 108 | whd in match (labels_of ?); >(no_labels … H) @(f_inv f) 102 109 ] 103 ]104 | whd in match (labels_of ?); >(no_labels … H) @(f_inv f)105 110 ] qed. 106 111 -
src/Cminor/syntax.ma
r2251 r2252 51 51 | St_cost : costlabel → stmt → stmt. 52 52 53 (* Apply a predicate to every statement. Be careful with grouping so that the 54 local application is the first conjunct, and substatements the second. *) 55 53 56 let rec stmt_P (P:stmt → Prop) (s:stmt) on s : Prop ≝ 54 57 match s with 55 [ St_seq s1 s2 ⇒ P s ∧ stmt_P P s1 ∧ stmt_P P s256 | St_ifthenelse _ _ _ s1 s2 ⇒ P s ∧ stmt_P P s1 ∧ stmt_P P s258 [ St_seq s1 s2 ⇒ P s ∧ (stmt_P P s1 ∧ stmt_P P s2) 59 | St_ifthenelse _ _ _ s1 s2 ⇒ P s ∧ (stmt_P P s1 ∧ stmt_P P s2) 57 60 | St_label _ s' ⇒ P s ∧ stmt_P P s' 58 61 | St_cost _ s' ⇒ P s ∧ stmt_P P s' 59 | _ ⇒ P s 62 | _ ⇒ P s ∧ True 60 63 ]. 61 64 62 65 lemma stmt_P_P : ∀P,s. stmt_P P s → P s. 63 #P * normalize /2/ 64 [ #s1 #s2 * * /2/ 65 | #sz #sg #e #s1 #s2 * * /2/ 66 | *: #i #s normalize * /2/ 67 ] qed. 66 #P * normalize * /3 by proj1/ 67 qed. 68 68 69 69 (* Assert a predicate on every variable or parameter identifier. *) … … 91 91 92 92 lemma stmt_P_mp : ∀P,Q. (∀s. P s → Q s) → ∀s. stmt_P P s → stmt_P Q s. 93 #P #Q #H #s elim s /2/ 94 [ #s1 #s2 #H1 #H2 normalize * * /4/ 95 | #sz #sg #e #s1 #s2 #H1 #H2 * * /5/ 96 | #l #s #H * /5/ 97 | #l #s #H * /5/ 98 ] qed. 93 #P #Q #H #s elim s /6 by proj1, proj2, conj/ 94 qed. 99 95 100 96 lemma stmt_vars_mp : ∀P,Q. (∀i,t. P i t → Q i t) → ∀s. stmt_vars P s → stmt_vars Q s. -
src/Cminor/toRTLabs.ma
r2251 r2252 192 192 λe,g. forall_nodes ? (labels_P (λl. present ?? g l ∨ lpresent e l)) g. 193 193 194 (* Some data structures for the transformation that remain fixed throughout. *) 195 record fixed : Type[0] ≝ { 196 fx_lenv : label_env; 197 fx_env : env; 198 fx_rettyp : option typ 199 }. 200 201 definition resultok : option typ → list (register × typ) → Type[0] ≝ 202 λty,env. 203 match ty with [ Some t ⇒ Σr:register. env_has env r t | _ ⇒ True ]. 204 194 205 (* I'd use a single parametrised definition along with internal_function, but 195 206 it's a pain without implicit parameters. *) 196 record partial_fn ( lenv:label_env) (env:env) : Type[0] ≝207 record partial_fn (fx:fixed) : Type[0] ≝ 197 208 { pf_labgen : universe LabelTag 198 209 ; pf_reggen : universe RegisterTag 199 210 ; pf_params : list (register × typ) 200 211 ; pf_locals : list (register × typ) 201 ; pf_result : option (Σrt:register × typ. env_has (pf_locals @ pf_params) (\fst rt) (\snd rt))202 ; pf_envok : ∀id,ty,r,H. lookup_reg envid ty H = r → env_has (pf_locals @ pf_params) r ty212 ; pf_result : resultok (fx_rettyp … fx) (pf_locals @ pf_params) 213 ; pf_envok : ∀id,ty,r,H. lookup_reg (fx_env … fx) id ty H = r → env_has (pf_locals @ pf_params) r ty 203 214 ; pf_stacksize : nat 204 215 ; pf_graph : graph statement 205 ; pf_closed : partially_closed lenvpf_graph216 ; pf_closed : partially_closed (fx_lenv … fx) pf_graph 206 217 ; pf_typed : graph_typed (pf_locals @ pf_params) pf_graph 207 218 ; pf_entry : Σl:label. present ?? pf_graph l … … 210 221 211 222 definition fn_env_has ≝ 212 λ le,env,f. env_has (pf_locals le env f @ pf_params le envf).213 214 record fn_contains ( le:label_env) (env:env) (f1:partial_fn le env) (f2:partial_fn le env) : Prop ≝223 λfx,f. env_has (pf_locals fx f @ pf_params fx f). 224 225 record fn_contains (fx:fixed) (f1:partial_fn fx) (f2:partial_fn fx) : Prop ≝ 215 226 { fn_con_graph : graph_included (pf_graph … f1) (pf_graph … f2) 216 ; fn_con_env : ∀r,ty. fn_env_has le env f1 r ty → fn_env_has le envf2 r ty227 ; fn_con_env : ∀r,ty. fn_env_has … f1 r ty → fn_env_has … f2 r ty 217 228 }. 218 229 219 lemma fn_con_trans : ∀ le,env,f1,f2,f3.220 fn_contains le env f1 f2 → fn_contains le env f2 f3 → fn_contains le envf1 f3.221 # le #env#f1 #f2 #f3 #H1 #H2 %230 lemma fn_con_trans : ∀fx,f1,f2,f3. 231 fn_contains fx f1 f2 → fn_contains … f2 f3 → fn_contains … f1 f3. 232 #fx #f1 #f2 #f3 #H1 #H2 % 222 233 [ @(graph_inc_trans … (fn_con_graph … H1) (fn_con_graph … H2)) 223 234 | #r #ty #H @(fn_con_env … H2) @(fn_con_env … H1) @H 224 235 ] qed. 225 236 226 lemma fn_con_refl : ∀ label_env,env,f.227 fn_contains label_env envf f.228 # le #env#f % #l // qed.229 230 lemma fn_con_sig : ∀ label_env,env,f,f0.231 ∀f':Σf':partial_fn label_env env. fn_contains … f0 f'.232 fn_contains label_env envf f0 →233 fn_contains label_env envf f'.234 # le #env#f #f0 * #f' #H1 #H2 @(fn_con_trans … H2 H1)235 qed. 236 237 lemma add_statement_inv : ∀ le,env,l,s.∀f.238 labels_present (pf_graph le envf) s →239 partially_closed le(add … (pf_graph … f) l s).240 # le #env#l #s #f #p237 lemma fn_con_refl : ∀fx,f. 238 fn_contains fx f f. 239 #fx #f % #l // qed. 240 241 lemma fn_con_sig : ∀fx,f,f0. 242 ∀f':Σf':partial_fn fx. fn_contains … f0 f'. 243 fn_contains fx f f0 → 244 fn_contains fx f f'. 245 #fx #f #f0 * #f' #H1 #H2 @(fn_con_trans … H2 H1) 246 qed. 247 248 lemma add_statement_inv : ∀fx,l,s.∀f. 249 labels_present (pf_graph fx f) s → 250 partially_closed (fx_lenv … fx) (add … (pf_graph … f) l s). 251 #fx #l #s #f #p 241 252 #l' #s' #H cases (identifier_eq … l l') 242 253 [ #E >E in H; >lookup_add_hit #E' <(?:s = s') [2:destruct //] … … 249 260 250 261 definition statement_typed_in ≝ 251 λ le,env,f,s. statement_typed (pf_locals le env f @ pf_params le envf) s.262 λfx,f,s. statement_typed (pf_locals fx f @ pf_params fx f) s. 252 263 253 264 lemma forall_nodes_add : ∀A,P,l,a,g. … … 261 272 262 273 (* Add a statement to the graph, *without* updating the entry label. *) 263 definition fill_in_statement : ∀ le,env. label → ∀s:statement. ∀f:partial_fn le env.274 definition fill_in_statement : ∀fx. label → ∀s:statement. ∀f:partial_fn fx. 264 275 labels_present (pf_graph … f) s → 265 statement_typed_in le envf s →266 Σf':partial_fn le env. fn_contains … f f' ≝267 λ le,env,l,s,f,p,tp.268 mk_partial_fn le env(pf_labgen … f) (pf_reggen … f)276 statement_typed_in … f s → 277 Σf':partial_fn fx. fn_contains … f f' ≝ 278 λfx,l,s,f,p,tp. 279 mk_partial_fn fx (pf_labgen … f) (pf_reggen … f) 269 280 (pf_params … f) (pf_locals … f) (pf_result … f) (pf_envok … f) 270 281 (pf_stacksize … f) (add ?? (pf_graph … f) l s) ? ? … … 277 288 278 289 (* Add a statement to the graph, making it the entry label. *) 279 definition add_to_graph : ∀ le,env. label → ∀s:statement. ∀f:partial_fn le env.290 definition add_to_graph : ∀fx. label → ∀s:statement. ∀f:partial_fn fx. 280 291 labels_present (pf_graph … f) s → 281 292 statement_typed_in … f s → 282 Σf':partial_fn le env. fn_contains … f f' ≝283 λ le,env,l,s,f,p,tl.284 mk_partial_fn le env(pf_labgen … f) (pf_reggen … f)293 Σf':partial_fn fx. fn_contains … f f' ≝ 294 λfx,l,s,f,p,tl. 295 mk_partial_fn fx (pf_labgen … f) (pf_reggen … f) 285 296 (pf_params … f) (pf_locals … f) (pf_result … f) (pf_envok … f) 286 297 (pf_stacksize … f) (add ?? (pf_graph … f) l s) ? ? … … 295 306 (* Add a statement with a fresh label to the start of the function. The 296 307 statement is parametrised by the *next* instruction's label. *) 297 definition add_fresh_to_graph : ∀ le,env. ∀s:(label → statement). ∀f:partial_fn le env.308 definition add_fresh_to_graph : ∀fx. ∀s:(label → statement). ∀f:partial_fn fx. 298 309 (∀l. present ?? (pf_graph … f) l → labels_present (pf_graph … f) (s l)) → 299 310 (∀l. statement_typed_in … f (s l)) → 300 Σf':partial_fn le env. fn_contains … f f' ≝301 λ le,env,s,f,p,tp.311 Σf':partial_fn fx. fn_contains … f f' ≝ 312 λfx,s,f,p,tp. 302 313 let 〈l,g〉 ≝ fresh … (pf_labgen … f) in 303 314 let s' ≝ s (pf_entry … f) in 304 (mk_partial_fn le envg (pf_reggen … f)315 (mk_partial_fn fx g (pf_reggen … f) 305 316 (pf_params … f) (pf_locals … f) (pf_result … f) (pf_envok … f) 306 317 (pf_stacksize … f) (add ?? (pf_graph … f) l s') ? ? … … 315 326 (* Variants for labels which are (goto) labels *) 316 327 317 lemma add_statement_inv' : ∀ le,env,l,s.∀f.318 labels_P (λl. present ?? (pf_graph le env f) l ∨ lpresent lel) s →319 partially_closed le(add … (pf_graph … f) l s).320 # le #env#l #s #f #p328 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 321 332 #l' #s' #H cases (identifier_eq … l l') 322 333 [ #E >E in H; >lookup_add_hit #E' <(?:s = s') [2:destruct //] … … 328 339 ] qed. 329 340 330 definition add_fresh_to_graph' : ∀ le,env. ∀s:(label → statement). ∀f:partial_fn le env.331 (∀l. present ?? (pf_graph … f) l → labels_P (λl.present ?? (pf_graph … f) l ∨ lpresent lel) (s l)) →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)) → 332 343 (∀l. statement_typed_in … f (s l)) → 333 Σf':partial_fn le env. fn_contains … f f' ≝334 λ le,env,s,f,p,tp.344 Σf':partial_fn fx. fn_contains … f f' ≝ 345 λfx,s,f,p,tp. 335 346 let 〈l,g〉 ≝ fresh … (pf_labgen … f) in 336 347 let s' ≝ s (pf_entry … f) in 337 (mk_partial_fn le envg (pf_reggen … f)348 (mk_partial_fn fx g (pf_reggen … f) 338 349 (pf_params … f) (pf_locals … f) (pf_result … f) (pf_envok … f) 339 350 (pf_stacksize … f) (add ?? (pf_graph … f) l s') ? ? … … 362 373 (* A little more nesting in the result type than I'd like, but it keeps the 363 374 function closely paired with the proof that it contains f. *) 364 definition fresh_reg : ∀ le,env. ∀f:partial_fn le env. ∀ty:typ.365 𝚺f':(Σf':partial_fn le env. fn_contains … f f'). (Σr:register. fn_env_has le envf' r ty) ≝366 λ le,env,f,ty.375 definition fresh_reg : ∀fx. ∀f:partial_fn fx. ∀ty:typ. 376 𝚺f':(Σf':partial_fn fx. fn_contains … f f'). (Σr:register. fn_env_has … f' r ty) ≝ 377 λfx,f,ty. 367 378 let 〈r,g〉 ≝ fresh … (pf_reggen … f) in 368 379 let f' ≝ 369 «mk_partial_fn le env 370 (pf_labgen … f) g (pf_params … f) (〈r,ty〉::(pf_locals … f)) 371 (match pf_result … f with [ None ⇒ None ? | Some rt ⇒ Some ? «pi1 … rt, ?»]) ? 380 «mk_partial_fn fx 381 (pf_labgen … f) g (pf_params … f) (〈r,ty〉::(pf_locals … f)) ? ? 372 382 (pf_stacksize … f) (pf_graph … f) (pf_closed … f) ? (pf_entry … f) (pf_exit … f), ?» 373 383 in … … 376 386 | #l #s #L @stmt_extend_typ_env @(pf_typed … L) 377 387 | #i #t #r1 #H #L %2 @(pf_envok … f … L) 378 | %2 @(pi2 … rt)388 | lapply (pf_result fx f) cases (fx_rettyp fx) // #t * #r' #H %{r'} @extend_typ_env // 379 389 | % [ #l // | #r' #ty' #H @extend_typ_env @H ] 380 390 ] qed. … … 382 392 axiom UnknownVariable : String. 383 393 384 definition choose_reg : ∀ le. ∀env:env.∀ty.∀e:expr ty. ∀f:partial_fn le env. expr_vars ty e (Env_has env) →385 𝚺f':(Σf':partial_fn le env. fn_contains … f f'). (Σr:register. fn_env_has le envf' r ty) ≝386 λ le,env,ty,e,f.387 match e return λty,e. expr_vars ty e (Env_has env) → 𝚺f':(Σf':partial_fn le env. fn_contains … f f'). (Σr:register. fn_env_has le envf' r ty) with388 [ Id t i ⇒ λEnv. ❬«f, ?», «lookup_reg envi t Env, ?»❭389 | _ ⇒ λ_.fresh_reg le envf ?394 definition choose_reg : ∀fx.∀ty.∀e:expr ty. ∀f:partial_fn fx. expr_vars ty e (Env_has (fx_env fx)) → 395 𝚺f':(Σf':partial_fn fx. fn_contains … f f'). (Σr:register. fn_env_has … f' r ty) ≝ 396 λfx,ty,e,f. 397 match e return λty,e. expr_vars ty e (Env_has (fx_env fx)) → 𝚺f':(Σf':partial_fn fx. fn_contains … f f'). (Σr:register. fn_env_has … f' r ty) with 398 [ Id t i ⇒ λEnv. ❬«f, ?», «lookup_reg (fx_env fx) i t Env, ?»❭ 399 | _ ⇒ λ_.fresh_reg … f ? 390 400 ]. 391 401 [ % // … … 404 414 λA,P,x. match x with [ mk_DPair a _ ⇒ a]. 405 415 406 definition choose_regs : ∀ le. ∀env:env. ∀es:list (𝚺t:typ.expr t).407 ∀f:partial_fn le env. All ? (exprtyp_present env) es →408 𝚺f':(Σf':partial_fn le env. fn_contains … f f'). (Σrs:list register. All2 ?? (λr,e. fn_env_has le envf' r (eject' typ expr e)) rs es) ≝409 λ le,env,es,f,Env.410 foldr_all' (𝚺t:typ.expr t) ? (λes. 𝚺f':(Σf':partial_fn le env. fn_contains … f f'). (Σrs:list register. All2 ?? (λr,e. fn_env_has le envf' r (eject' typ expr e)) rs es))416 definition choose_regs : ∀fx. ∀es:list (𝚺t:typ.expr t). 417 ∀f:partial_fn fx. All ? (exprtyp_present (fx_env fx)) es → 418 𝚺f':(Σf':partial_fn fx. fn_contains … f f'). (Σrs:list register. All2 ?? (λr,e. fn_env_has … f' r (eject' typ expr e)) rs es) ≝ 419 λfx,es,f,Env. 420 foldr_all' (𝚺t:typ.expr t) ? (λes. 𝚺f':(Σf':partial_fn fx. fn_contains … f f'). (Σrs:list register. All2 ?? (λr,e. fn_env_has … f' r (eject' typ expr e)) rs es)) 411 421 (λe,p,tl,acc. 412 match acc return λ_.𝚺f':(Σf':partial_fn le env. fn_contains … f f'). (Σrs:list register. All2 ?? (λr,e. fn_env_has le envf' r (eject' typ expr e)) rs (e::tl)) with [ mk_DPair f1 rs ⇒413 match e return λe.exprtyp_present env e → 𝚺f':(Σf':partial_fn le env. fn_contains … f f'). (Σrs:list register. All2 ?? (λr,e. fn_env_has le envf' r (eject' typ expr e)) rs (e::tl)) with [ mk_DPair t e ⇒ λp.414 match choose_reg le env t e (pi1 … f1) ? return λ_.𝚺f':(Σf':partial_fn le env. fn_contains … f f'). (Σrs:list register. All2 ?? (λr,e. fn_env_has le envf' r (eject' typ expr e)) rs (❬t,e❭::tl)) with [ mk_DPair f' r ⇒422 match acc return λ_.𝚺f':(Σf':partial_fn fx. fn_contains … f f'). (Σrs:list register. All2 ?? (λr,e. fn_env_has … f' r (eject' typ expr e)) rs (e::tl)) with [ mk_DPair f1 rs ⇒ 423 match e return λe.exprtyp_present (fx_env fx) e → 𝚺f':(Σf':partial_fn fx. fn_contains … f f'). (Σrs:list register. All2 ?? (λr,e. fn_env_has … f' r (eject' typ expr e)) rs (e::tl)) with [ mk_DPair t e ⇒ λp. 424 match choose_reg fx t e (pi1 … f1) ? return λ_.𝚺f':(Σf':partial_fn fx. fn_contains … f f'). (Σrs:list register. All2 ?? (λr,e. fn_env_has … f' r (eject' typ expr e)) rs (❬t,e❭::tl)) with [ mk_DPair f' r ⇒ 415 425 ❬«pi1 … f', ?»,«(pi1 … r)::(pi1 … rs), ?»❭ 416 426 ] … … 419 429 [ @p 420 430 | cases r #r' #Hr' cases rs #rs' #Hrs' 421 % [ whd in ⊢ (?? ?%%%); @Hr' | @(All2_mp … Hrs') #r1 * #t1 #e1 #H1 @(fn_con_env … f1) [ @(pi2 … f') | @H1 ] ]431 % [ whd in ⊢ (??%%%); @Hr' | @(All2_mp … Hrs') #r1 * #t1 #e1 #H1 @(fn_con_env … f1) [ @(pi2 … f') | @H1 ] ] 422 432 | @fn_con_trans [ 3: @(pi2 … f') | skip | @(pi2 … f1) ] 423 433 | @fn_con_refl … … 430 440 431 441 432 lemma choose_regs_length : ∀ le,env,es,f,p,f',rs.433 choose_regs le enves f p = ❬f',rs❭ → |es| = length … rs.434 # le #env#es #f #p #f' * #rs #H #_ @sym_eq @(All2_length … H)435 qed. 436 437 lemma present_included : ∀ le,env,f,f',l.438 fn_contains le envf f' →442 lemma choose_regs_length : ∀fx,es,f,p,f',rs. 443 choose_regs fx es f p = ❬f',rs❭ → |es| = length … rs. 444 #fx #es #f #p #f' * #rs #H #_ @sym_eq @(All2_length … H) 445 qed. 446 447 lemma present_included : ∀fx,f,f',l. 448 fn_contains fx f f' → 439 449 present ?? (pf_graph … f) l → 440 450 present ?? (pf_graph … f') l. 441 # le #env#f #f' #l * #H1 #H2 @H1 qed.451 #fx #f #f' #l * #H1 #H2 @H1 qed. 442 452 443 453 (* Some definitions for the add_stmt function later, which we introduce now so … … 446 456 (* We need to show that the graph only grows, and that Cminor labels will end 447 457 up in the graph. *) 448 definition Cminor_labels_added ≝ λ le,env,s,f'.458 definition Cminor_labels_added ≝ λfx,s,f'. 449 459 ∀l. Exists ? (λl'.l=l') (labels_of s) → 450 ∃l'. lookup ?? le l = Some ? l' ∧ present ?? (pf_graph le envf') l'.451 452 record add_stmt_inv ( le:label_env) (env:env) (s:stmt) (f:partial_fn le env) (f':partial_fn le env) : Prop ≝460 ∃l'. lookup ?? (fx_lenv fx) l = Some ? l' ∧ present ?? (pf_graph fx f') l'. 461 462 record add_stmt_inv (fx:fixed) (s:stmt) (f:partial_fn fx) (f':partial_fn fx) : Prop ≝ 453 463 { stmt_graph_con : fn_contains … f f' 454 464 ; stmt_labels_added : Cminor_labels_added … s f' … … 458 468 459 469 (* A datatype saying how we intend to prove a step. *) 460 inductive fn_con_because ( le:label_env) (env:env) : partial_fn le env→ Type[0] ≝461 | fn_con_eq : ∀f. fn_con_because le envf462 | fn_con_sig : ∀f1,f2:partial_fn le env. fn_contains … f1 f2 →463 ∀f3:(Σf3:partial_fn le env.fn_contains … f2 f3). fn_con_because le envf3464 | fn_con_addinv : ∀f1,f2:partial_fn le env. fn_contains … f1 f2 →465 ∀s.∀f3:(Σf3:partial_fn le env.add_stmt_inv … s f2 f3). fn_con_because le envf3470 inductive fn_con_because (fx:fixed) : partial_fn fx → Type[0] ≝ 471 | fn_con_eq : ∀f. fn_con_because fx f 472 | fn_con_sig : ∀f1,f2:partial_fn fx. fn_contains … f1 f2 → 473 ∀f3:(Σf3:partial_fn fx.fn_contains … f2 f3). fn_con_because fx f3 474 | fn_con_addinv : ∀f1,f2:partial_fn fx. fn_contains … f1 f2 → 475 ∀s.∀f3:(Σf3:partial_fn fx.add_stmt_inv … s f2 f3). fn_con_because fx f3 466 476 . 467 477 468 478 (* Extract the starting function for a step. *) 469 let rec fn_con_because_left le env f0 (b:fn_con_because ?? f0) on b : partial_fn le env≝479 let rec fn_con_because_left fx f0 (b:fn_con_because ? f0) on b : partial_fn fx ≝ 470 480 match b with [ fn_con_eq f ⇒ f | fn_con_sig f _ _ _ ⇒ f | fn_con_addinv f _ _ _ _ ⇒ f ]. 471 481 … … 475 485 have reached the desired starting point. *) 476 486 477 unification hint 0 ≔ le:label_env, env:env, f:partial_fn le env, dummy:True;487 unification hint 0 ≔ fx:fixed, f:partial_fn fx, dummy:True; 478 488 f' ≟ f, 479 b ≟ fn_con_eq le envf489 b ≟ fn_con_eq fx f 480 490 ⊢ 481 fn_contains le env f f' ≡ fn_contains le env (fn_con_because_left le envf' b) f'491 fn_contains fx f f' ≡ fn_contains fx (fn_con_because_left fx f' b) f' 482 492 . 483 493 484 unification hint 1 ≔ le:label_env, env:env, f1:partial_fn le env, f2:partial_fn le env, H12 : fn_contains le env f1 f2, f3:(Σf3:partial_fn le env. fn_contains le envf2 f3);485 b ≟ fn_con_sig le envf1 f2 H12 f3494 unification hint 1 ≔ fx:fixed, f1:partial_fn fx, f2:partial_fn fx, H12 : fn_contains fx f1 f2, f3:(Σf3:partial_fn fx. fn_contains fx f2 f3); 495 b ≟ fn_con_sig fx f1 f2 H12 f3 486 496 ⊢ 487 fn_contains le env f1 f3 ≡ fn_contains le env (fn_con_because_left le envf3 b) f3497 fn_contains fx f1 f3 ≡ fn_contains fx (fn_con_because_left fx f3 b) f3 488 498 . 489 499 490 unification hint 1 ≔ le:label_env, env:env, f1:partial_fn le env, f2:partial_fn le env, H12 : fn_contains le env f1 f2, s:stmt, f3:(Σf3:partial_fn le env. add_stmt_inv le envs f2 f3);491 b ≟ fn_con_addinv le envf1 f2 H12 s f3500 unification hint 1 ≔ fx:fixed, f1:partial_fn fx, f2:partial_fn fx, H12 : fn_contains fx f1 f2, s:stmt, f3:(Σf3:partial_fn fx. add_stmt_inv fx s f2 f3); 501 b ≟ fn_con_addinv fx f1 f2 H12 s f3 492 502 ⊢ 493 fn_contains le env f1 f3 ≡ fn_contains le env (fn_con_because_left le envf3 b) f3503 fn_contains fx f1 f3 ≡ fn_contains fx (fn_con_because_left fx f3 b) f3 494 504 . 495 505 496 506 (* A lemma to perform a step of the proof. We can repeat this to do the whole 497 507 proof. *) 498 lemma fn_contains_step : ∀ le,env,f. ∀b:fn_con_because le envf. fn_contains … (fn_con_because_left … f b) f.499 # le #env#f *508 lemma fn_contains_step : ∀fx,f. ∀b:fn_con_because fx f. fn_contains … (fn_con_because_left … f b) f. 509 #fx #f * 500 510 [ #f @fn_con_refl 501 511 | #f1 #f2 #H12 * #f3 #H23 @(fn_con_trans … H12 H23) … … 505 515 axiom BadCminorProgram : String. 506 516 507 let rec add_expr ( le:label_env) (env:env) (ty:typ) (e:expr ty)508 (Env:expr_vars ty e (Env_has env)) (f:partial_fn le env)517 let rec add_expr (fx:fixed) (ty:typ) (e:expr ty) 518 (Env:expr_vars ty e (Env_has (fx_env fx))) (f:partial_fn fx) 509 519 (dst:Σdst. fn_env_has … f dst ty) 510 on e: Σf':partial_fn le env. fn_contains … f f' ≝511 match e return λty,e.expr_vars ty e (Env_has env) → (Σdst. fn_env_has … f dst ty) → Σf':partial_fn le env. fn_contains … f f' with520 on e: Σf':partial_fn fx. fn_contains … f f' ≝ 521 match e return λty,e.expr_vars ty e (Env_has ?) → (Σdst. fn_env_has … f dst ty) → Σf':partial_fn fx. fn_contains … f f' with 512 522 [ Id t i ⇒ λEnv,dst. 513 let r ≝ lookup_reg envi t Env in523 let r ≝ lookup_reg (fx_env fx) i t Env in 514 524 match register_eq r dst with 515 525 [ inl _ ⇒ «f, ?» … … 520 530 let ❬f,r❭ ≝ choose_reg … e' f Env in 521 531 let f ≝ add_fresh_to_graph … (St_op1 t' t op dst r) f ?? in 522 let f ≝ add_expr … env? e' Env f «r, ?» in532 let f ≝ add_expr … ? e' Env f «r, ?» in 523 533 «pi1 … f, ?» 524 534 | Op2 _ _ _ op e1 e2 ⇒ λEnv,dst. … … 526 536 let ❬f,r2❭ ≝ choose_reg … e2 f (proj2 … Env) in 527 537 let f ≝ add_fresh_to_graph … (St_op2 ??? op dst r1 r2) f ?? in 528 let f ≝ add_expr … env? e2 (proj2 … Env) f «r2, ?» in529 let f ≝ add_expr … env? e1 (proj1 … Env) f «r1, ?» in538 let f ≝ add_expr … ? e2 (proj2 … Env) f «r2, ?» in 539 let f ≝ add_expr … ? e1 (proj1 … Env) f «r1, ?» in 530 540 «pi1 … f, ?» 531 541 | Mem t e' ⇒ λEnv,dst. 532 542 let ❬f,r❭ ≝ choose_reg … e' f Env in 533 543 let f ≝ add_fresh_to_graph … (St_load t r dst) f ?? in 534 let f ≝ add_expr … env? e' Env f «r,?» in544 let f ≝ add_expr … ? e' Env f «r,?» in 535 545 «pi1 … f, ?» 536 546 | Cond _ _ _ e' e1 e2 ⇒ λEnv,dst. 537 547 let resume_at ≝ pf_entry … f in 538 let f ≝ add_expr … env? e2 (proj2 … Env) f dst in548 let f ≝ add_expr … ? e2 (proj2 … Env) f dst in 539 549 let lfalse ≝ pf_entry … f in 540 550 let f ≝ add_fresh_to_graph … (λ_.St_skip resume_at) f ?? in 541 let f ≝ add_expr … env? e1 (proj2 … (proj1 … Env)) f «dst, ?» in551 let f ≝ add_expr … ? e1 (proj2 … (proj1 … Env)) f «dst, ?» in 542 552 let ❬f,r❭ ≝ choose_reg … e' f ? in 543 553 let f ≝ add_fresh_to_graph … (λltrue. St_cond r ltrue lfalse) f ?? in 544 let f ≝ add_expr … env? e' (proj1 … (proj1 … Env)) f «r, ?» in554 let f ≝ add_expr … ? e' (proj1 … (proj1 … Env)) f «r, ?» in 545 555 «pi1 … f, ?» 546 556 | Ecost _ l e' ⇒ λEnv,dst. 547 let f ≝ add_expr … env? e' Env f dst in557 let f ≝ add_expr … ? e' Env f dst in 548 558 let f ≝ add_fresh_to_graph … (St_cost l) f ?? in 549 559 «f, ?» … … 560 570 | @(fn_con_env … (pi2 ?? r1)) repeat @fn_contains_step @I 561 571 | @(fn_con_env … (pi2 ?? r2)) repeat @fn_contains_step @I 562 | #l % [ % [ @(fn_con_env ???????(pi2 ?? r1)) | @(pi2 ?? r2) ] | @(fn_con_env … (pi2 ?? dst)) ] repeat @fn_contains_step @I572 | #l % [ % [ @(fn_con_env … (pi2 ?? r1)) | @(pi2 ?? r2) ] | @(fn_con_env … (pi2 ?? dst)) ] repeat @fn_contains_step @I 563 573 | #l #H whd % [ @H | @(fn_con_graph … (pi2 ?? lfalse)) repeat @fn_contains_step @I ] 564 574 | @(π1 (π1 Env)) … … 567 577 ] qed. 568 578 569 let rec add_exprs ( le:label_env) (env:env) (es:list (𝚺t:typ.expr t)) (Env:All ? (exprtyp_present env) es)570 (dsts:list register) (pf:length … es = length … dsts) (f:partial_fn le env)571 (Hdsts:All2 ?? (λr,e. fn_env_has le env f r (eject' typ expr e)) dsts es) on es: Σf':partial_fn le env. fn_contains le envf f' ≝579 let rec add_exprs (fx:fixed) (es:list (𝚺t:typ.expr t)) (Env:All ? (exprtyp_present (fx_env fx)) es) 580 (dsts:list register) (pf:length … es = length … dsts) (f:partial_fn fx) 581 (Hdsts:All2 ?? (λr,e. fn_env_has … f r (eject' typ expr e)) dsts es) on es: Σf':partial_fn fx. fn_contains … f f' ≝ 572 582 match es return λes.All ?? es → All2 ???? es → |es|=|dsts| → ? with 573 [ nil ⇒ λ_.λ_. match dsts return λx. ?=|x| → Σf':partial_fn le env. fn_contains le envf f' with [ nil ⇒ λ_. «f, ?» | cons _ _ ⇒ λpf.⊥ ]583 [ nil ⇒ λ_.λ_. match dsts return λx. ?=|x| → Σf':partial_fn fx. fn_contains … f f' with [ nil ⇒ λ_. «f, ?» | cons _ _ ⇒ λpf.⊥ ] 574 584 | cons e et ⇒ λEnv. 575 match dsts return λx. All2 ?? (λr,e. fn_env_has le envf r (eject' typ expr e)) x (e::et) → ?=|x| → ? with585 match dsts return λx. All2 ?? (λr,e. fn_env_has … f r (eject' typ expr e)) x (e::et) → ?=|x| → ? with 576 586 [ nil ⇒ λ_.λpf.⊥ 577 587 | cons r rt ⇒ λHdsts,pf. 578 let f' ≝ add_exprs ? envet ? rt ? f ? in579 match e return λe.exprtyp_present ? e → fn_env_has le envf r (eject' typ expr e) → ? with [ mk_DPair ty e ⇒ λEnv,Hr.580 let f'' ≝ add_expr ? envty e ? f' r in588 let f' ≝ add_exprs … et ? rt ? f ? in 589 match e return λe.exprtyp_present ? e → fn_env_has … f r (eject' typ expr e) → ? with [ mk_DPair ty e ⇒ λEnv,Hr. 590 let f'' ≝ add_expr … ty e ? f' r in 581 591 «pi1 … f'', ?» 582 592 ] (proj1 ?? Env) (π1 Hdsts) … … 595 605 axiom ReturnMismatch : String. 596 606 597 definition stmt_inv : env → label_env → stmt → Prop ≝ 598 λenv,lenv. stmt_P (λs. stmt_vars (Env_has env) s ∧ stmt_labels (present ?? lenv) s). 607 definition return_ok ≝ 608 λt,s. match s with [ St_return oe ⇒ rettyp_match t oe | _ ⇒ True ]. 609 610 record stmt_inv (fx:fixed) (s:stmt) : Prop ≝ { 611 si_vars : stmt_vars (Env_has (fx_env fx)) s; 612 si_labels : stmt_labels (present ?? (fx_lenv fx)) s; 613 si_return : return_ok (fx_rettyp fx) s 614 }. 615 616 definition stmts_inv : fixed → stmt → Prop ≝ 617 λfx. stmt_P (stmt_inv fx). 599 618 600 619 (* Trick to avoid multiplying the proof obligations for the non-Id cases. *) … … 631 650 qed. 632 651 633 lemma empty_Cminor_labels_added : ∀ le,env,s,f'.634 labels_of s = [ ] → Cminor_labels_added le envs f'.635 # le #env#s #f' #E whd >E #l *;636 qed. 637 638 lemma equal_Cminor_labels_added : ∀ le,env,s,s',f.652 lemma empty_Cminor_labels_added : ∀fx,s,f'. 653 labels_of s = [ ] → Cminor_labels_added fx s f'. 654 #fx #s #f' #E whd >E #l *; 655 qed. 656 657 lemma equal_Cminor_labels_added : ∀fx,s,s',f. 639 658 labels_of s = labels_of s' → Cminor_labels_added … s' f → 640 Cminor_labels_added le envs f.641 # le #env#s #s' #f #E whd in ⊢ (% → %); > E #H @H642 qed. 643 644 lemma Cminor_labels_con : ∀ le,env,s,f,f'.645 fn_contains le envf f' →659 Cminor_labels_added fx s f. 660 #fx #s #s' #f #E whd in ⊢ (% → %); > E #H @H 661 qed. 662 663 lemma Cminor_labels_con : ∀fx,s,f,f'. 664 fn_contains fx f f' → 646 665 Cminor_labels_added … s f → 647 666 Cminor_labels_added … s f'. 648 # le #env#s #f #f' #INC #ADDED667 #fx #s #f #f' #INC #ADDED 649 668 #l #E cases (ADDED l E) #l' * #L #P 650 669 %{l'} % [ @L | @(present_included … P) @INC ] 651 670 qed. 652 671 653 lemma Cminor_labels_inv : ∀ le,env,s,s',f.654 ∀f':Σf':partial_fn le env. add_stmt_inv le envs' f f'.655 Cminor_labels_added le envs f →656 Cminor_labels_added le envs f'.657 # le #env#s #s' #f * #f' * #H1 #H2 #H3672 lemma Cminor_labels_inv : ∀fx,s,s',f. 673 ∀f':Σf':partial_fn fx. add_stmt_inv fx s' f f'. 674 Cminor_labels_added fx s f → 675 Cminor_labels_added fx s f'. 676 #fx #s #s' #f * #f' * #H1 #H2 #H3 658 677 #l #E cases (H3 l E) #l' * #L #P 659 678 %{l'} % [ @L | @(present_included … P) @H1 ] 660 679 qed. 661 680 662 lemma Cminor_labels_sig : ∀ le,env,s,f.663 ∀f':Σf':partial_fn le env. fn_contains … f f'.681 lemma Cminor_labels_sig : ∀fx,s,f. 682 ∀f':Σf':partial_fn fx. fn_contains … f f'. 664 683 Cminor_labels_added … s f → 665 684 Cminor_labels_added … s f'. 666 # le #env#s #f * #f' #H1 #H2685 #fx #s #f * #f' #H1 #H2 667 686 #l #E cases (H2 l E) #l' * #L #P 668 687 %{l'} % [ @L | @(present_included … P) @H1 ] 669 688 qed. 670 689 671 let rec add_stmt (env:env) (label_env:label_env) (s:stmt) (Env:stmt_inv env label_env s) (f:partial_fn label_env env) on s : res (Σf':partial_fn label_env env. add_stmt_inv label_env env s f f') ≝ 672 match s return λs.stmt_inv env label_env s → res (Σf':partial_fn label_env env. add_stmt_inv … s f f') with 690 discriminator option. 691 discriminator DPair. 692 693 (* Return statements need a little careful treatment to avoid errors using the 694 invariant about the return type. *) 695 696 definition add_return : ∀fx,opt_e. ∀f:partial_fn fx. ∀Env:stmts_inv fx (St_return opt_e). 697 Σf':partial_fn fx. add_stmt_inv fx (St_return opt_e) f f' ≝ 698 λfx,opt_e,f. 699 let f0 ≝ f in 700 let f ≝ add_fresh_to_graph … (λ_. R_return) f ?? in 701 match opt_e return λo. stmts_inv ? (St_return o) → Σf':partial_fn fx.add_stmt_inv … (St_return o) f0 f' with 702 [ None ⇒ λEnv. «pi1 … f, ?» 703 | Some et ⇒ 704 match et return λe.stmts_inv fx (St_return (Some ? e)) → Σf':partial_fn fx.add_stmt_inv … (St_return (Some ? e)) f0 f' with 705 [ mk_DPair ty e ⇒ λEnv. 706 match fx_rettyp fx return λX. rettyp_match X ? → match X with [ Some t ⇒ Σr:register. env_has ?? t | None ⇒ ? ] → ? with 707 [ None ⇒ λH. ⊥ 708 | Some t ⇒ λH,R. 709 match R with 710 [ mk_Sig r Hr ⇒ 711 let f ≝ add_expr fx ty e ? f «r, ?» in 712 «pi1 … f, ?» 713 ] 714 ] (si_return … (π1 Env)) (pf_result fx f) 715 ] 716 ]. 717 [ @mk_add_stmt_inv /2/ 718 | inversion H #A #B #C destruct 719 | @mk_add_stmt_inv 720 [ repeat @fn_contains_step @I 721 | @empty_Cminor_labels_added // 722 ] 723 | @(si_vars … (π1 Env)) 724 | inversion H [ #E destruct ] #ty' #e' #E1 #E2 #_ destruct @Hr 725 | #l #H @I 726 | #l // 727 ] qed. 728 729 730 let rec add_stmt (fx:fixed) (s:stmt) (Env:stmts_inv fx s) (f:partial_fn fx) on s : res (Σf':partial_fn fx. add_stmt_inv fx s f f') ≝ 731 match s return λs.stmts_inv fx s → res (Σf':partial_fn fx. add_stmt_inv … s f f') with 673 732 [ St_skip ⇒ λ_. OK ? «f, ?» 674 733 | St_assign t x e ⇒ λEnv. 675 let dst ≝ lookup_reg env x t (π1 (π1 Env)) in676 OK ? «pi1 … (add_expr ? env ? e (π2 (π1 Env)) f dst), ?»734 let dst ≝ lookup_reg (fx_env fx) x t (π1 (si_vars … (π1 Env))) in 735 OK ? «pi1 … (add_expr … e (π2 (si_vars … (π1 Env))) f dst), ?» 677 736 | St_store t e1 e2 ⇒ λEnv. 678 let ❬f, val_reg❭ ≝ choose_reg … e2 f (π2 ( π1 Env)) in679 let ❬f, addr_reg❭ ≝ choose_reg … e1 f (π1 ( π1 Env)) in737 let ❬f, val_reg❭ ≝ choose_reg … e2 f (π2 (si_vars … (π1 Env))) in 738 let ❬f, addr_reg❭ ≝ choose_reg … e1 f (π1 (si_vars … (π1 Env))) in 680 739 let f ≝ add_fresh_to_graph … (St_store t addr_reg val_reg) f ?? in 681 let f ≝ add_expr ? env ? e1 (π1 (π1 Env)) f «addr_reg, ?» in682 OK ? «pi1 … (add_expr ? env ? e2 (π2 (π1 Env)) f «val_reg, ?»), ?»740 let f ≝ add_expr … e1 (π1 (si_vars … (π1 Env))) f «addr_reg, ?» in 741 OK ? «pi1 … (add_expr … ? e2 (π2 (si_vars … (π1 Env))) f «val_reg, ?»), ?» 683 742 | St_call return_opt_id e args ⇒ λEnv. 684 743 let return_opt_reg ≝ 685 744 match return_opt_id return λo. ? → ? with 686 745 [ None ⇒ λ_. None ? 687 | Some idty ⇒ λEnv. Some ? (lookup_reg env(\fst idty) (\snd idty) ?)746 | Some idty ⇒ λEnv. Some ? (lookup_reg (fx_env fx) (\fst idty) (\snd idty) ?) 688 747 ] Env in 689 let ❬f, args_regs❭ ≝ choose_regs ? env args f (π2 (π1 Env)) in748 let ❬f, args_regs❭ ≝ choose_regs ? args f (π2 (si_vars ?? (π1 Env))) in 690 749 let f ≝ 691 750 match expr_is_Id ? e with 692 751 [ Some id ⇒ add_fresh_to_graph … (St_call_id id args_regs return_opt_reg) f ?? 693 752 | None ⇒ 694 let ❬f, fnr❭ ≝ choose_reg … e f (π2 (π1 ( π1 Env))) in753 let ❬f, fnr❭ ≝ choose_reg … e f (π2 (π1 (si_vars … (π1 Env)))) in 695 754 let f ≝ add_fresh_to_graph … (St_call_ptr fnr args_regs return_opt_reg) f ?? in 696 «pi1 … (add_expr ? env ? e (π2 (π1 (π1 Env))) f «fnr, ?»), ?»755 «pi1 … (add_expr … ? e (π2 (π1 (si_vars … (π1 Env)))) f «fnr, ?»), ?» 697 756 ] in 698 OK ? «pi1 … (add_exprs ? env args (π2 (π1 Env)) args_regs ? f ?), ?»757 OK ? «pi1 … (add_exprs … args (π2 (si_vars … (π1 Env))) args_regs ? f ?), ?» 699 758 (* 700 759 | St_tailcall e args ⇒ λEnv. … … 711 770 *) 712 771 | St_seq s1 s2 ⇒ λEnv. 713 do f2 ← add_stmt env label_envs2 ? f;714 do f1 ← add_stmt env label_envs1 ? f2;772 do f2 ← add_stmt … s2 ? f; 773 do f1 ← add_stmt … s1 ? f2; 715 774 OK ? «pi1 … f1, ?» 716 775 | St_ifthenelse _ _ e s1 s2 ⇒ λEnv. 717 776 let l_next ≝ pf_entry … f in 718 do f2 ← add_stmt env label_env s2 (π2 Env) f;777 do f2 ← add_stmt … s2 (π2 (π2 Env)) f; 719 778 let l2 ≝ pf_entry … f2 in 720 779 let f ≝ add_fresh_to_graph … (λ_. R_skip l_next) f2 ?? in 721 do f1 ← add_stmt env label_env s1 (π2 (π1Env)) f;722 let ❬f,r❭ ≝ choose_reg … e f1 ( π1 (π1 (π1 Env))) in780 do f1 ← add_stmt … s1 (π1 (π2 Env)) f; 781 let ❬f,r❭ ≝ choose_reg … e f1 (si_vars … (π1 Env)) in 723 782 let f ≝ add_fresh_to_graph … (λl1. St_cond r l1 l2) f ?? in 724 OK ? «pi1 … (add_expr ? env ? e (π1 (π1 (π1 Env))) f «r, ?»), ?» 725 | St_return opt_e ⇒ let f0 ≝ f in 783 OK ? «pi1 … (add_expr … ? e (si_vars … (π1 Env)) f «r, ?»), ?» 784 | St_return opt_e ⇒ λEnv. OK ? (add_return fx opt_e f Env) 785 (*let f0 ≝ f in 726 786 let f ≝ add_fresh_to_graph … (λ_. R_return) f ?? in 727 match opt_e return λo. stmt_inv ? ? (St_return o) → res (Σf':partial_fn label_env env.add_stmt_inv … (St_return o) f0 f') with787 match opt_e return λo. stmt_inv ? (St_return o) → res (Σf':partial_fn fx.add_stmt_inv … (St_return o) f0 f') with 728 788 [ None ⇒ λEnv. OK ? «pi1 … f, ?» 729 789 | Some e ⇒ 730 match pf_result… f with790 match fx_rettyp … f with 731 791 [ None ⇒ λEnv. Error ? (msg ReturnMismatch) 732 792 | Some r ⇒ 733 match e return λe.stmt_inv env label_env (St_return (Some ? e)) → res (Σf':partial_fn label_env env.add_stmt_inv … (St_return (Some ? e)) f0 f') with793 match e return λe.stmt_inv fx (St_return (Some ? e)) → res (Σf':partial_fn fx.add_stmt_inv … (St_return (Some ? e)) f0 f') with 734 794 [ mk_DPair ty e ⇒ λEnv. 735 795 match typ_eq (\snd r) ty with 736 [ inl E ⇒ let f ≝ add_expr label_env envty e ? f «\fst r, ? E (* XXX E goes missing if I don't use it! *)» in796 [ inl E ⇒ let f ≝ add_expr … ty e ? f «\fst r, ? E (* XXX E goes missing if I don't use it! *)» in 737 797 OK ? «pi1 … f, ?» 738 798 | inr _ ⇒ Error ? (msg ReturnMismatch) … … 740 800 ] 741 801 ] 742 ] 802 ]*) 743 803 | St_label l s' ⇒ λEnv. 744 do f ← add_stmt env label_envs' (π2 Env) f;745 let l' ≝ lookup_label label_envl ? in804 do f ← add_stmt … s' (π2 Env) f; 805 let l' ≝ lookup_label (fx_lenv fx) l ? in 746 806 OK ? «pi1 … (add_to_graph … l' (R_skip (pf_entry … f)) f ??), ?» 747 807 | St_goto l ⇒ λEnv. 748 let l' ≝ lookup_label label_envl ? in808 let l' ≝ lookup_label (fx_lenv fx) l ? in 749 809 OK ? «pi1 … (add_fresh_to_graph' … (λ_.R_skip l') f ??), ?» 750 810 | St_cost l s' ⇒ λEnv. 751 do f ← add_stmt env label_envs' (π2 Env) f;811 do f ← add_stmt … s' (π2 Env) f; 752 812 OK ? «pi1 … (add_fresh_to_graph … (St_cost l) f ??), ?» 753 813 ] Env. 754 try @(π1 Env)755 814 try @(π2 Env) 756 try @(π1 (π 1Env))757 try @(π2 (π 1Env))815 try @(π1 (π2 Env)) 816 try @(π2 (π2 Env)) 758 817 try @mk_add_stmt_inv 759 818 try (repeat @fn_contains_step @I) … … 762 821 try (#l #H @H) 763 822 try (#l @I) 764 [ @(pf_envok … (π1 ( π1 Env))) @refl823 [ @(pf_envok … (π1 (si_vars … (π1 Env)))) @refl 765 824 | @(fn_con_env … (pi2 ?? val_reg)) repeat @fn_contains_step @I 766 825 | @(fn_con_env … (pi2 ?? addr_reg)) repeat @fn_contains_step @I … … 768 827 | @sym_eq @(All2_length … (pi2 ?? args_regs)) 769 828 | @(fn_con_env … (pi2 ?? fnr)) repeat @fn_contains_step @I 770 | @(π1 (π1 ( π1 Env)))829 | @(π1 (π1 (si_vars … (π1 Env)))) 771 830 | #l #H cases (Exists_append … H) 772 [ #H1 @(stmt_labels_added ???? ?(pi2 ?? f1) ? H1)773 | #H2 @(Cminor_labels_inv … H2) @(stmt_labels_added ???? ?(pi2 ?? f2))831 [ #H1 @(stmt_labels_added ???? (pi2 ?? f1) ? H1) 832 | #H2 @(Cminor_labels_inv … H2) @(stmt_labels_added ???? (pi2 ?? f2)) 774 833 ] 775 834 | #l #H @(fn_con_graph … (pi2 ?? l_next)) repeat @fn_contains_step @I 776 835 | #l #H cases (Exists_append … H) 777 [ #H1 @(Cminor_labels_sig … H1) @Cminor_labels_sig @Cminor_labels_sig @(stmt_labels_added ???? ?(pi2 ?? f1))778 | #H2 @(Cminor_labels_sig … H2) @Cminor_labels_sig @Cminor_labels_sig @Cminor_labels_inv @Cminor_labels_sig @(stmt_labels_added ???? ?(pi2 ?? f2))836 [ #H1 @(Cminor_labels_sig … H1) @Cminor_labels_sig @Cminor_labels_sig @(stmt_labels_added ???? (pi2 ?? f1)) 837 | #H2 @(Cminor_labels_sig … H2) @Cminor_labels_sig @Cminor_labels_sig @Cminor_labels_inv @Cminor_labels_sig @(stmt_labels_added ???? (pi2 ?? f2)) 779 838 ] 780 839 | @(fn_con_env … (pi2 ?? r)) repeat @fn_contains_step @I 781 840 | #l #H % [ @H | @(fn_con_graph … (pi2 ?? l2)) repeat @fn_contains_step @I ] 782 | #_ (* see above *) <E @(pi2 ?? r)841 | @(si_labels … (π1 Env)) 783 842 | @(pi2 … (pf_entry …)) 784 843 | #l1 * [ #E >E %{l'} % [ @lookup_label_rev' | whd >lookup_add_hit % #E' destruct (E') ] 785 | @Cminor_labels_sig @(stmt_labels_added ???? ?(pi2 … f))844 | @Cminor_labels_sig @(stmt_labels_added ???? (pi2 … f)) 786 845 ] 787 846 | #l1 #H whd %2 @lookup_label_lpresent 788 | @(equal_Cminor_labels_added ??? s') [ @refl | @Cminor_labels_sig @(stmt_labels_added ????? (pi2 … f)) ] 847 | @(si_labels … (π1 Env)) 848 | @(equal_Cminor_labels_added ?? s') [ @refl | @Cminor_labels_sig @(stmt_labels_added ???? (pi2 … f)) ] 789 849 ] qed. 790 850 … … 797 857 let 〈locals0, env, reggen2〉 as E2 ≝ populate_env env1 reggen1 (f_vars f) in 798 858 let ❬locals_reggen, result❭ as E3 ≝ 799 match f_return f return λ _.𝚺lr. option (Σrt. env_has ((\fst lr)@params) (\fst rt) (\snd rt)) with800 [ None ⇒ ❬〈locals0, reggen2〉, None ?❭859 match f_return f return λt.𝚺lr. resultok t ((\fst lr)@params) with 860 [ None ⇒ ❬〈locals0, reggen2〉, I❭ 801 861 | Some ty ⇒ 802 862 let 〈r,gen〉 ≝ fresh … reggen2 in 803 mk_DPair ? (λlr. option (Σrt. env_has ((\fst lr)@params) (\fst rt) (\snd rt))) 〈〈r,ty〉::locals0, gen〉 (Some ? «〈r,ty〉, ?»)] in863 mk_DPair ? (λlr.Σr. env_has ((\fst lr)@params) r ty) 〈〈r,ty〉::locals0, gen〉 «r, ?» ] in 804 864 let locals ≝ \fst locals_reggen in 805 865 let reggen ≝ \snd locals_reggen in 806 866 let 〈label_env, labgen1〉 as El ≝ populate_label_env (empty_map …) labgen0 cminor_labels in 807 867 let 〈l,labgen〉 ≝ fresh … labgen1 in 868 let fixed ≝ mk_fixed label_env env (f_return f) in 808 869 let emptyfn ≝ 809 mk_partial_fn 810 label_env 811 env 870 mk_partial_fn fixed 812 871 labgen 813 872 reggen … … 822 881 l 823 882 l in 824 do f ← add_stmt env label_env(f_body f) ? emptyfn;883 do f ← add_stmt fixed (f_body f) ? emptyfn; 825 884 OK ? (mk_internal_function 826 885 (pf_labgen … f) 827 886 (pf_reggen … f) 828 (match pf_result … f with [ None ⇒ None ? | Some rt ⇒ Some ? (pi1 … rt) ])887 (match fx_rettyp fixed return λt. match t with [ Some t ⇒ Σr:register. env_has ? r t | _ ⇒ True ] → ? with [ None ⇒ λ_. None ? | Some t ⇒ λR. Some ? 〈(pi1 … R),t〉 ] (pf_result … f)) 829 888 (pf_params … f) 830 889 (pf_locals … f) … … 849 908 | @(stmt_labels_mp … L) 850 909 #l #H @(populates_label_env … (sym_eq … El)) @H 910 | cases s in R ⊢ %; // 851 911 ] 852 912 | #l #s #E @(labels_P_mp … (pf_closed … f l s E)) … … 864 924 [ * #H1 #L1 cases (populate_env_list … (sym_eq … E1) … H1 L1) 865 925 [ * * | normalize @Exists_append_r ] 866 | cases (f_return f) in E3; 867 [ whd in ⊢ (??%% → ?); #E3 whd in match locals; destruct 926 | (* gave up with cases (f_return f) in result E3; *) 927 @(match f_return f return λx.∀R:resultok x ((\fst locals_reggen)@params). ❬locals_reggen,R❭ = match x with [None ⇒ ?|Some _ ⇒ ?] → ? with [ None ⇒ λres1.? | Some rty ⇒ λres1.?] result E3) 928 [ whd in ⊢ (??%% → ?); #E3' whd in match locals; destruct 868 929 @Exists_append_l 869 | #rt cases (fresh ? reggen2) #rr #ru whd in ⊢ (??%% → ?); #E3whd in match locals; destruct930 | cases (fresh ? reggen2) #rr #ru whd in ⊢ (??%% → ?); #E3' whd in match locals; destruct 870 931 #H' @Exists_append_l %2 @H' 871 932 ]
Note: See TracChangeset
for help on using the changeset viewer.