Changeset 1104 for Deliverables/D3.3/id-lookup-branch

Timestamp:

Aug 10, 2011, 5:17:55 PM (10 years ago)

Author:

campbell

Message:

A little more tidying.

Location:

Deliverables/D3.3/id-lookup-branch

Files:

• Cminor/syntax.ma (modified) (1 diff)
• Cminor/toRTLabs.ma (modified) (5 diffs)
• common/Identifiers.ma (modified) (1 diff)

Deliverables/D3.3/id-lookup-branch/Cminor/syntax.ma

@@ -4 +4 @@
 include "utilities/lists.ma".
 include "utilities/option.ma".
-
-definition present : ∀tag,A. identifier_map tag A → identifier tag → Prop ≝
-λtag,A,m,i. lookup … m i ≠ None ?.
 
 (* TODO: consider making the typing stricter. *)

Deliverables/D3.3/id-lookup-branch/Cminor/toRTLabs.ma

@@ -79 +79 @@
 ] qed.
 
-definition lookup' : ∀e:env. ∀id. present ?? e id → register ≝
-λe,id. match lookup ?? e id return λx. x ≠ None ? → ? with [ Some r ⇒ λ_. r | None ⇒ λH.⊥ ].
-cases H #H'  cases (H' (refl ??)) qed.
-
-definition lookup_label : ∀e:label_env. ∀id. present ?? e id → label ≝
-λe,id. match lookup ?? e id return λx. x ≠ None ? → ? with [ Some r ⇒ λ_. r | None ⇒ λH.⊥ ].
-cases H #H'  cases (H' (refl ??)) qed.
-
+definition lookup_reg : ∀e:env. ∀id. present ?? e id → register ≝ lookup_present ??.
+definition lookup_label : ∀e:label_env. ∀id. present ?? e id → label ≝ lookup_present ??.
 
 (* Add a statement to the graph, *without* updating the entry label. *)
@@ -135 +129 @@
 λenv,ty,e,f.
   match e return λty,e. expr_vars ty e (present ?? env) → register × internal_function with
-  [ Id _ i ⇒ λEnv. 〈lookup' env i Env, f〉
+  [ Id _ i ⇒ λEnv. 〈lookup_reg env i Env, f〉
   | _ ⇒ λ_.fresh_reg f ty
   ].
@@ -179 +173 @@
 match e return λty,e.expr_vars ty e (present ?? env) → internal_function with
 [ Id _ i ⇒ λEnv.
-    let r ≝ lookup' env i Env in
+    let r ≝ lookup_reg env i Env in
     match register_eq r dst with
     [ inl _ ⇒ f
@@ -239 +233 @@
 [ St_skip ⇒ λ_. OK ? f
 | St_assign _ x e ⇒ λEnv.
-    let dst ≝ lookup' env x (π1 (π1 Env)) in
+    let dst ≝ lookup_reg env x (π1 (π1 Env)) in
     OK ? (add_expr env ? e (π2 (π1 Env)) dst f)
 | St_store _ _ q e1 e2 ⇒ λEnv.
@@ -251 +245 @@
       match return_opt_id return λo. ? → ? with
       [ None ⇒ λ_. None ?
-      | Some id ⇒ λEnv. Some ? (lookup' env id ?)
+      | Some id ⇒ λEnv. Some ? (lookup_reg env id ?)
       ] Env in
     let 〈args_regs, f〉 as Eregs ≝ choose_regs env args f (π2 (π1 Env)) in

Deliverables/D3.3/id-lookup-branch/common/Identifiers.ma

@@ -147 +147 @@
   [ an_id_map m' ⇒ fold A B ? (λbv. f (an_identifier ? bv)) m' b ].
 
+(* A predicate that an identifier is in a map, and a failure-avoiding lookup
+   using it. *)
+
+definition present : ∀tag,A. identifier_map tag A → identifier tag → Prop ≝
+λtag,A,m,i. lookup … m i ≠ None ?.
+
+definition lookup_present : ∀tag,A. ∀m:identifier_map tag A. ∀id. present ?? m id → A ≝
+λtag,A,m,id. match lookup ?? m id return λx. x ≠ None ? → ? with [ Some a ⇒ λ_. a | None ⇒ λH.⊥ ].
+cases H #H'  cases (H' (refl ??)) qed.
+
+
 (* Sets *)