Changeset 2971


Ignore:
Timestamp:
Mar 27, 2013, 11:41:51 AM (4 years ago)
Author:
campbell
Message:

Single RTLabs return statement.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/Cminor/toRTLabs.ma

    r2936 r2971  
    636636
    637637(* 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. *)
    639640
    640641definition add_return : ∀fx,opt_e. ∀f:partial_fn fx. ∀Env:stmts_inv fx (St_return opt_e).
     
    642643λfx,opt_e,f.
    643644  let f0 ≝ f in
    644   let f ≝ add_fresh_to_graph … (λ_. R_return) f ?? in
     645  let f ≝ change_entry … f (pf_exit … f) (pi2 ???) in
    645646  match opt_e return λo. stmts_inv ? (St_return o) → Σf':partial_fn fx.add_stmt_inv … (St_return o) f0 f' with
    646647  [ None ⇒ λEnv. «pi1 … f, ?»
     
    667668| @(si_vars … (π1 Env))
    668669| inversion H [ #E destruct ] #ty' #e' #E1 #E2 #_ destruct @Hr
    669 | #l #H @I
    670 | #l //
    671670] qed.
    672671
Note: See TracChangeset for help on using the changeset viewer.