Ignore:
Timestamp:
Oct 7, 2011, 12:26:39 PM (9 years ago)
Author:
campbell
Message:

Merge in id-lookup-branch to trunk.

Location:
src
Files:
2 edited

Legend:

Unmodified
Added
Removed
  • src

  • src/common/Identifiers.ma

    r1092 r1316  
    33include "ASM/Arithmetic.ma".
    44include "common/Errors.ma".
     5include "utilities/option.ma".
    56
    67(* identifiers and their generators are tagged to differentiate them, and to
     
    122123] qed.
    123124
     125lemma lookup_add_cases : ∀tag,A,m,i,j,a,v.
     126  lookup tag A (add tag A m i a) j = Some ? v →
     127  (i=j ∧ v = a) ∨ lookup tag A m j = Some ? v.
     128#tag #A #m #i #j #a #v
     129cases (identifier_eq ? i j)
     130[ #E >E >lookup_add_hit #H %1 destruct % //
     131| #NE >lookup_add_miss /2/ @eq_identifier_elim /2/
     132] qed.
     133
    124134(* Extract every identifier, value pair from the map. *)
    125135definition elements : ∀tag,A. identifier_map tag A → list (identifier tag × A) ≝
     
    147157  [ an_id_map m' ⇒ fold A B ? (λbv. f (an_identifier ? bv)) m' b ].
    148158
     159(* A predicate that an identifier is in a map, and a failure-avoiding lookup
     160   and update using it. *)
     161
     162definition present : ∀tag,A. identifier_map tag A → identifier tag → Prop ≝
     163λtag,A,m,i. lookup … m i ≠ None ?.
     164
     165definition lookup_present : ∀tag,A. ∀m:identifier_map tag A. ∀id. present ?? m id → A ≝
     166λtag,A,m,id. match lookup ?? m id return λx. x ≠ None ? → ? with [ Some a ⇒ λ_. a | None ⇒ λH.⊥ ].
     167cases H #H'  cases (H' (refl ??)) qed.
     168
     169definition update_present : ∀tag,A. ∀m:identifier_map tag A. ∀id. present ?? m id → A → identifier_map tag A ≝
     170λtag,A,m,l,p,a.
     171  let l' ≝ match l with [ an_identifier l' ⇒ l' ] in
     172  let m' ≝ match m with [ an_id_map m' ⇒ m' ] in
     173  let u' ≝ update A 16 l' a m' in
     174  match u' return λx. update ????? = x → ? with
     175  [ None ⇒ λE.⊥
     176  | Some m' ⇒ λ_. an_id_map tag A m'
     177  ] (refl ? u').
     178whd in p; whd in p:(?(??%?)) E:(??(???%?%)?);
     179cases l in p E; cases m; -l' -m' #m' #l' whd in ⊢ (?(??(???%%)?) → ??(???%?%)? → ?)
     180#NL #U cases NL #H @H @(update_fail … U)
     181qed.
     182
     183lemma update_still_present : ∀tag,A,m,id,a,id'.
     184  ∀H:present tag A m id.
     185  ∀H':present tag A m id'.
     186  present tag A (update_present tag A m id' H' a) id.
     187#tag #A * #m * #id #a * #id' #H #H'
     188whd whd in ⊢ (?(??(???(%??????)?)?)) normalize nodelta
     189cases (identifier_eq ? (an_identifier tag id) (an_identifier tag id'))
     190[ #E >E @refute_none_by_refl #m' #U whd in ⊢ (?(??%?)) >(update_lookup_opt_same ?????? U)
     191  % #E' destruct
     192| #NE @refute_none_by_refl #m' #U whd in ⊢ (?(??%?)) whd in ⊢ (?(??(???%%)?))
     193  <(update_lookup_opt_other ?????? U id) [ @H | % #E cases NE >E #H @H @refl ]
     194] qed.
     195
    149196(* Sets *)
    150197
Note: See TracChangeset for help on using the changeset viewer.