Changeset 1104 for Deliverables/D3.3/idlookupbranch/Cminor/toRTLabs.ma
 Timestamp:
 Aug 10, 2011, 5:17:55 PM (10 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

Deliverables/D3.3/idlookupbranch/Cminor/toRTLabs.ma
r1102 r1104 79 79 ] qed. 80 80 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 81 definition lookup_reg : ∀e:env. ∀id. present ?? e id → register ≝ lookup_present ??. 82 definition lookup_label : ∀e:label_env. ∀id. present ?? e id → label ≝ lookup_present ??. 89 83 90 84 (* Add a statement to the graph, *without* updating the entry label. *) … … 135 129 λenv,ty,e,f. 136 130 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〉 138 132  _ ⇒ λ_.fresh_reg f ty 139 133 ]. … … 179 173 match e return λty,e.expr_vars ty e (present ?? env) → internal_function with 180 174 [ Id _ i ⇒ λEnv. 181 let r ≝ lookup 'env i Env in175 let r ≝ lookup_reg env i Env in 182 176 match register_eq r dst with 183 177 [ inl _ ⇒ f … … 239 233 [ St_skip ⇒ λ_. OK ? f 240 234  St_assign _ x e ⇒ λEnv. 241 let dst ≝ lookup 'env x (π1 (π1 Env)) in235 let dst ≝ lookup_reg env x (π1 (π1 Env)) in 242 236 OK ? (add_expr env ? e (π2 (π1 Env)) dst f) 243 237  St_store _ _ q e1 e2 ⇒ λEnv. … … 251 245 match return_opt_id return λo. ? → ? with 252 246 [ None ⇒ λ_. None ? 253  Some id ⇒ λEnv. Some ? (lookup 'env id ?)247  Some id ⇒ λEnv. Some ? (lookup_reg env id ?) 254 248 ] Env in 255 249 let 〈args_regs, f〉 as Eregs ≝ choose_regs env args f (π2 (π1 Env)) in
Note: See TracChangeset
for help on using the changeset viewer.