Changeset 2415

Timestamp:

Oct 23, 2012, 3:57:02 PM (7 years ago)

Author:

campbell

Message:

Add the ability to map blocks to symbols in preparation for stack space.

Location:

src/common

Files:

• Globalenvs.ma (modified) (2 diffs)
• Identifiers.ma (modified) (1 diff)
• PositiveMap.ma (modified) (1 diff)

src/common/Globalenvs.ma

@@ -228 +228 @@
 
 
+(* Turn a memory block into the original symbol. *)
+definition symbol_for_block: ∀F:Type[0]. genv_t F → block → option ident ≝
+λF,genv,b.
+  option_map ?? (fst ??) (find … (symbols … genv) (λid,b'. eq_block b b')).
+
+
 lemma find_funct_find_funct_ptr : ∀F,ge,v,f.
   find_funct F ge v = Some F f →
@@ -312 +318 @@
 #A #B #P #fnOK #fns #fns' #p @(proj2 … (pre_matching_fns_get_same_blocks … p)) @fnOK
 qed.
+
+lemma symbol_of_block_rev : ∀F,genv,b,id.
+  symbol_for_block F genv b = Some ? id →
+  find_symbol F genv id = Some ? b.
+#F #genv #b #id #H whd in H:(??%?);
+@(find_lookup … (λid,b'. eq_block b b'))
+lapply (find_predicate … (symbols … genv) (λid,b'. eq_block b b'))
+cases (find ????) in H ⊢ %;
+[ normalize #E destruct
+| * #id' #b' normalize in ⊢ (% → ?); #E destruct
+  #H lapply (H … (refl ??))
+  @eq_block_elim
+  [ #E destruct //
+  | #_ *
+  ]
+] qed.
 
 (*

src/common/Identifiers.ma

@@ -345 +345 @@
   [ an_id_map m' ⇒ λf,b. pm_fold_inf A B m' (λbv,a,H. f (an_identifier ? bv) a H) b ].
 
+(* Find one element of a map that satisfies a predicate *)
+definition find : ∀tag,A. identifier_map tag A → (identifier tag → A → bool) →
+  option (identifier tag × A) ≝
+λtag,A,m,p.
+  match m with [ an_id_map m' ⇒
+    option_map … (λx. 〈an_identifier tag (\fst x), \snd x〉)
+      (pm_find … m' (λid. p (an_identifier tag id))) ].
+
+lemma find_lookup : ∀tag,A,m,p,id,a.
+  find tag A m p = Some ? 〈id,a〉 →
+  lookup … m id = Some ? a.
+#tag #A * #m #p * #id #a #FIND
+@(pm_find_lookup A (λid. p (an_identifier tag id)) id a m)
+whd in FIND:(??%?); cases (pm_find ???) in FIND ⊢ %;
+[ normalize #E destruct
+| * #id' #a' normalize #E destruct %
+] qed.
+
+lemma find_predicate : ∀tag,A,m,p,id,a.
+  find tag A m p = Some ? 〈id,a〉 →
+  p id a.
+#tag #A * #m #p * #id #a #FIND whd in FIND:(??%?);
+@(pm_find_predicate A m (λid. p (an_identifier tag id)) id a)
+cases (pm_find ???) in FIND ⊢ %;
+[ normalize #E destruct
+| * #id' #a' normalize #E destruct %
+] qed.
+
 (* A predicate that an identifier is in a map, and a failure-avoiding lookup
    and update using it. *)

src/common/PositiveMap.ma

@@ -590 +590 @@
   λA,B,t,f,b. pm_fold_inf_aux A B t f t (λx.x) b (λp. refl ??).
 
+(* Find an entry in the map matching the given predicate *)
+
+let rec pm_find_aux (pre: Pos → Pos) (A:Type[0]) (t: positive_map A) (p:Pos → A → bool) on t : option (Pos × A) ≝
+match t with
+[ pm_leaf ⇒ None ?
+| pm_node a l r ⇒
+  let x ≝ match a with
+  [ Some a ⇒ if p (pre one) a then Some ? 〈pre one, a〉 else None ?
+  | None ⇒ None ?
+  ] in
+  match x with
+  [ Some x ⇒ Some ? x
+  | None ⇒ 
+    match pm_find_aux (λx. pre (p0 x)) A l p with
+    [ None ⇒ pm_find_aux (λx. pre (p1 x)) A r p
+    | Some y ⇒ Some ? y
+    ]
+  ]
+].
+
+definition pm_find : ∀A:Type[0]. positive_map A → (Pos → A → bool) → option (Pos × A) ≝
+  pm_find_aux (λx.x).
+
+lemma pm_find_aux_pre : ∀A,t,pre,p,q,a.
+  pm_find_aux pre A t p = Some ? 〈q,a〉 →
+  ∃q'. q = pre q'.
+#A #t elim t
+[ normalize #pre #p #q #a #E destruct
+| * [2:#a] #l #r #IHl #IHr #pre #p #q #a' normalize
+  [ cases (p (pre one) a) normalize [ #E destruct /2/ ] ]
+  lapply (IHl (λx. pre (p0 x)) p)
+  cases (pm_find_aux ?? l ?)
+  [ 1,3: #_ normalize
+    lapply (IHr (λx. pre (p1 x)) p)
+    cases (pm_find_aux ?? r ?)
+    [ 1,3: #_ #E destruct
+    | *: * #q' #a'' #H #E destruct cases (H ?? (refl ??)) #q'' #E destruct /2/
+    ]
+  | *: * #q' #a'' #H normalize #E destruct cases (H ?? (refl ??)) #q'' #E destruct /2/
+  ]
+] qed.
+
+(* XXX: Hmm... destruct doesn't work properly with this, not sure why *)
+lemma option_pair_f_eq : ∀A,B:Type[0].∀a,a',b,b'. ∀f:A → A.
+  (∀a,a'. f a = f a' → a = a') →
+  Some (A×B) 〈f a,b〉 = Some ? 〈f a',b'〉 →
+  a = a' ∧ b = b'.
+#A #B #a #a' #b #b' #f #EXT #E
+cut (f a = f a') [ destruct (E) destruct (e0) @e2 (* WTF? *) ]
+#E' >(EXT … E') in E ⊢ %; #E destruct /2/
+qed.
+
+lemma pm_find_lookup : ∀A,p,q,a,t.
+  pm_find A t p = Some ? 〈q,a〉 →
+  lookup_opt A q t = Some ? a.
+#A #p #q #a normalize #t
+change with ((λx.x) q) in match q in ⊢ (% → ?);
+cut (∀y,z:Pos. (λx.x) y = (λx.x) z → y = z) //
+generalize in match q; -q generalize in match (λx.x);
+elim t
+[ #pre #q #_  normalize #E destruct
+| * [2:#a'] #l #r #IHl #IHr #pre #q #PRE
+  normalize [ cases (p (pre one) a') normalize [ #E cases (option_pair_f_eq … pre PRE E) #E1 #E2 destruct normalize % ] ]
+  lapply (IHl (λx.pre (p0 x)))
+  lapply (pm_find_aux_pre A l (λx.pre (p0 x)) p)
+  cases (pm_find_aux ?? l ?)
+  [ 1,3: #_ #_ normalize
+    lapply (IHr (λx.pre (p1 x)))
+    lapply (pm_find_aux_pre A r (λx.pre (p1 x)) p)
+    cases (pm_find_aux ?? r ?)
+    [ 1,3: #_ #_ #E destruct
+    | *: * #q' #a' #H1 #H2 #E destruct cases (H1 ?? (refl ??)) #q'' #E lapply (PRE … E) #E' destruct
+         whd in ⊢ (??%?); @H2 //
+         #y #z #E lapply (PRE … E) #E' destruct //
+    ]
+  | *: * #q' #a' #H1 #H2 normalize #E destruct cases (H1 ?? (refl ??)) #q'' #E lapply (PRE … E) #E' destruct
+         whd in ⊢ (??%?); @H2 //
+         #y #z #E lapply (PRE … E) #E' destruct //
+  ]
+] qed.
+
+lemma pm_find_predicate : ∀A,t,p,q,a.
+  pm_find A t p = Some ? 〈q,a〉 →
+  p q a.
+#A #t #p normalize #q
+change with ((λx.x) q) in match q; generalize in match q; -q generalize in match (λx.x);
+elim t
+[ normalize #pre #q #a #E destruct
+| * [2:#a'] #l #r #IHl #IHr #pre #q #a normalize
+  [ lapply (refl ? (p (pre one) a')) cases (p (pre one) a') in ⊢ (???% → %);
+    [ #E normalize #E'
+      cut (pre one = pre q) [ destruct (E') destruct (e0) @e2 (* XXX ! *) ]
+      #E'' <E'' in E' ⊢ %; #E' destruct >E %
+    | #_ normalize
+    ]
+  ]
+  lapply (IHl (λx.pre (p0 x)))
+  lapply (pm_find_aux_pre A l (λx.pre (p0 x)) p)
+  cases (pm_find_aux ?? l ?)
+  [ 1,3: #_ #_ normalize
+    lapply (IHr (λx.pre (p1 x)))
+    lapply (pm_find_aux_pre A r (λx.pre (p1 x)) p)
+    cases (pm_find_aux ?? r ?)
+    [ 1,3: #_ #_ #E destruct
+    | *: * #q' #a' #H1 #H2 #E destruct cases (H1 … (refl ??)) #q'' #E >E @H2 >E %
+    ]
+  | *: * #q' #a' #H1 #H2 normalize #E destruct cases (H1 … (refl ??)) #q'' #E >E @H2 >E %
+  ]
+] qed.