Ignore:
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.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/common/Identifiers.ma

    r2335 r2415  
    345345  [ an_id_map m' ⇒ λf,b. pm_fold_inf A B m' (λbv,a,H. f (an_identifier ? bv) a H) b ].
    346346
     347(* Find one element of a map that satisfies a predicate *)
     348definition find : ∀tag,A. identifier_map tag A → (identifier tag → A → bool) →
     349  option (identifier tag × A) ≝
     350λtag,A,m,p.
     351  match m with [ an_id_map m' ⇒
     352    option_map … (λx. 〈an_identifier tag (\fst x), \snd x〉)
     353      (pm_find … m' (λid. p (an_identifier tag id))) ].
     354
     355lemma find_lookup : ∀tag,A,m,p,id,a.
     356  find tag A m p = Some ? 〈id,a〉 →
     357  lookup … m id = Some ? a.
     358#tag #A * #m #p * #id #a #FIND
     359@(pm_find_lookup A (λid. p (an_identifier tag id)) id a m)
     360whd in FIND:(??%?); cases (pm_find ???) in FIND ⊢ %;
     361[ normalize #E destruct
     362| * #id' #a' normalize #E destruct %
     363] qed.
     364
     365lemma find_predicate : ∀tag,A,m,p,id,a.
     366  find tag A m p = Some ? 〈id,a〉 →
     367  p id a.
     368#tag #A * #m #p * #id #a #FIND whd in FIND:(??%?);
     369@(pm_find_predicate A m (λid. p (an_identifier tag id)) id a)
     370cases (pm_find ???) in FIND ⊢ %;
     371[ normalize #E destruct
     372| * #id' #a' normalize #E destruct %
     373] qed.
     374
    347375(* A predicate that an identifier is in a map, and a failure-avoiding lookup
    348376   and update using it. *)
Note: See TracChangeset for help on using the changeset viewer.