Changeset 2971
- Timestamp:
- Mar 27, 2013, 11:41:51 AM (8 years ago)
- File:
-
- 1 edited
Legend:
- Unmodified
- Added
- Removed
-
src/Cminor/toRTLabs.ma
r2936 r2971 636 636 637 637 (* Return statements need a little careful treatment to avoid errors using the 638 invariant about the return type. *) 638 invariant about the return type. Note that there is one unique return 639 statement at the function's exit. *) 639 640 640 641 definition add_return : ∀fx,opt_e. ∀f:partial_fn fx. ∀Env:stmts_inv fx (St_return opt_e). … … 642 643 λfx,opt_e,f. 643 644 let f0 ≝ f in 644 let f ≝ add_fresh_to_graph … (λ_. R_return) f ??in645 let f ≝ change_entry … f (pf_exit … f) (pi2 ???) in 645 646 match opt_e return λo. stmts_inv ? (St_return o) → Σf':partial_fn fx.add_stmt_inv … (St_return o) f0 f' with 646 647 [ None ⇒ λEnv. «pi1 … f, ?» … … 667 668 | @(si_vars … (π1 Env)) 668 669 | inversion H [ #E destruct ] #ty' #e' #E1 #E2 #_ destruct @Hr 669 | #l #H @I670 | #l //671 670 ] qed. 672 671
Note: See TracChangeset
for help on using the changeset viewer.