Changeset 1104 for Deliverables/D3.3/id-lookup-branch
- Timestamp:
- Aug 10, 2011, 5:17:55 PM (10 years ago)
- 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 4 4 include "utilities/lists.ma". 5 5 include "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 ?.9 6 10 7 (* TODO: consider making the typing stricter. *) -
Deliverables/D3.3/id-lookup-branch/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 -
Deliverables/D3.3/id-lookup-branch/common/Identifiers.ma
r1093 r1104 147 147 [ an_id_map m' ⇒ fold A B ? (λbv. f (an_identifier ? bv)) m' b ]. 148 148 149 (* A predicate that an identifier is in a map, and a failure-avoiding lookup 150 using it. *) 151 152 definition present : ∀tag,A. identifier_map tag A → identifier tag → Prop ≝ 153 λtag,A,m,i. lookup … m i ≠ None ?. 154 155 definition 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.⊥ ]. 157 cases H #H' cases (H' (refl ??)) qed. 158 159 149 160 (* Sets *) 150 161
Note: See TracChangeset
for help on using the changeset viewer.