Changeset 2924


Ignore:
Timestamp:
Mar 21, 2013, 8:39:00 AM (4 years ago)
Author:
campbell
Message:

Make calls to a known identifier actually use a direct call.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/Cminor/toRTLabs.ma

    r2601 r2924  
    580580λfx. stmt_P (stmt_inv fx).
    581581
    582 (* Trick to avoid multiplying the proof obligations for the non-Id cases. *)
    583 definition expr_is_Id : ∀t. expr t → option ident ≝
     582(* Trick to avoid multiplying the proof obligations for the non-constant ident cases. *)
     583definition expr_is_cst_ident : ∀t. expr t → option ident ≝
    584584λt,e. match e with
    585 [ Id _ id ⇒ Some ? id
     585[ Cst _ c ⇒
     586  match c with
     587  [ Oaddrsymbol id n ⇒
     588    match n with [ O ⇒ Some ? id | _ ⇒ None ? ]
     589  | _ ⇒ None ?
     590  ]
    586591| _ ⇒ None ?
    587592].
     
    738743    let ❬f, args_regs❭ ≝ choose_regs ? args f (π2 (si_vars ?? (π1 Env))) in
    739744    let f ≝
    740       match expr_is_Id ? e with
     745      match expr_is_cst_ident ? e with
    741746      [ Some id ⇒ add_fresh_to_graph … (St_call_id id args_regs return_opt_reg) f ??
    742747      | None ⇒
Note: See TracChangeset for help on using the changeset viewer.