Changeset 1104


Ignore:
Timestamp:
Aug 10, 2011, 5:17:55 PM (8 years ago)
Author:
campbell
Message:

A little more tidying.

Location:
Deliverables/D3.3/id-lookup-branch
Files:
3 edited

Legend:

Unmodified
Added
Removed
  • Deliverables/D3.3/id-lookup-branch/Cminor/syntax.ma

    r1097 r1104  
    44include "utilities/lists.ma".
    55include "utilities/option.ma".
    6 
    7 definition present : ∀tag,A. identifier_map tag A → identifier tag → Prop ≝
    8 λtag,A,m,i. lookup … m i ≠ None ?.
    96
    107(* TODO: consider making the typing stricter. *)
  • Deliverables/D3.3/id-lookup-branch/Cminor/toRTLabs.ma

    r1102 r1104  
    7979] qed.
    8080
    81 definition lookup' : ∀e:env. ∀id. present ?? e id → register ≝
    82 λe,id. match lookup ?? e id return λx. x ≠ None ? → ? with [ Some r ⇒ λ_. r | None ⇒ λH.⊥ ].
    83 cases H #H'  cases (H' (refl ??)) qed.
    84 
    85 definition lookup_label : ∀e:label_env. ∀id. present ?? e id → label ≝
    86 λe,id. match lookup ?? e id return λx. x ≠ None ? → ? with [ Some r ⇒ λ_. r | None ⇒ λH.⊥ ].
    87 cases H #H'  cases (H' (refl ??)) qed.
    88 
     81definition lookup_reg : ∀e:env. ∀id. present ?? e id → register ≝ lookup_present ??.
     82definition lookup_label : ∀e:label_env. ∀id. present ?? e id → label ≝ lookup_present ??.
    8983
    9084(* Add a statement to the graph, *without* updating the entry label. *)
     
    135129λenv,ty,e,f.
    136130  match e return λty,e. expr_vars ty e (present ?? env) → register × internal_function with
    137   [ Id _ i ⇒ λEnv. 〈lookup' env i Env, f〉
     131  [ Id _ i ⇒ λEnv. 〈lookup_reg env i Env, f〉
    138132  | _ ⇒ λ_.fresh_reg f ty
    139133  ].
     
    179173match e return λty,e.expr_vars ty e (present ?? env) → internal_function with
    180174[ Id _ i ⇒ λEnv.
    181     let r ≝ lookup' env i Env in
     175    let r ≝ lookup_reg env i Env in
    182176    match register_eq r dst with
    183177    [ inl _ ⇒ f
     
    239233[ St_skip ⇒ λ_. OK ? f
    240234| St_assign _ x e ⇒ λEnv.
    241     let dst ≝ lookup' env x (π1 (π1 Env)) in
     235    let dst ≝ lookup_reg env x (π1 (π1 Env)) in
    242236    OK ? (add_expr env ? e (π2 (π1 Env)) dst f)
    243237| St_store _ _ q e1 e2 ⇒ λEnv.
     
    251245      match return_opt_id return λo. ? → ? with
    252246      [ None ⇒ λ_. None ?
    253       | Some id ⇒ λEnv. Some ? (lookup' env id ?)
     247      | Some id ⇒ λEnv. Some ? (lookup_reg env id ?)
    254248      ] Env in
    255249    let 〈args_regs, f〉 as Eregs ≝ choose_regs env args f (π2 (π1 Env)) in
  • Deliverables/D3.3/id-lookup-branch/common/Identifiers.ma

    r1093 r1104  
    147147  [ an_id_map m' ⇒ fold A B ? (λbv. f (an_identifier ? bv)) m' b ].
    148148
     149(* A predicate that an identifier is in a map, and a failure-avoiding lookup
     150   using it. *)
     151
     152definition present : ∀tag,A. identifier_map tag A → identifier tag → Prop ≝
     153λtag,A,m,i. lookup … m i ≠ None ?.
     154
     155definition lookup_present : ∀tag,A. ∀m:identifier_map tag A. ∀id. present ?? m id → A ≝
     156λtag,A,m,id. match lookup ?? m id return λx. x ≠ None ? → ? with [ Some a ⇒ λ_. a | None ⇒ λH.⊥ ].
     157cases H #H'  cases (H' (refl ??)) qed.
     158
     159
    149160(* Sets *)
    150161
Note: See TracChangeset for help on using the changeset viewer.