Changeset 1316 for src/common

Timestamp:

Oct 7, 2011, 12:26:39 PM (10 years ago)

Author:

campbell

Message:

Merge in id-lookup-branch to trunk.

Location:

src

Files:

• . (modified) (1 prop)
• common/Errors.ma (modified) (4 diffs)
• common/Identifiers.ma (modified) (3 diffs)

src/common/Errors.ma

@@ -18 +18 @@
 include "basics/list.ma".
 include "common/PreIdentifiers.ma".
+include "utilities/lists.ma".
+include "utilities/deppair.ma".
 
 (* * Error reporting and the error monad. *)
@@ -87 +89 @@
 notation "'ret' e" non associative with precedence 45 for @{'ret ${e}}.*)
 
+(* Dependent pair version. *)
+notation > "vbox('do' « ident v , ident p » ← e; break e')" with precedence 40
+  for @{ bind ?? ${e} (λ${fresh x}.match ${fresh x} with [ dp ${ident v} ${ident p} ⇒ ${e'} ]) }.
+
 (*
 (** The [do] notation, inspired by Haskell's, keeps the code readable. *)
@@ -127 +133 @@
   | cons hd tl ⇒ do hd' ← f hd; do tl' ← mmap ?? f tl; OK ? (hd'::tl')
   ].
+
+(* And mmap coupled with proofs. *)
+
+let rec mmap_sigma (A,B:Type[0]) (P:B → Prop) (f:A → res (Σx:B.P x)) (l:list A) on l : res (Σl':list B.All B P l') ≝
+match l with
+[ nil ⇒ OK ? «nil B, ?»
+| cons h t ⇒ 
+    do h' ← f h;
+    do t' ← mmap_sigma A B P f t;
+    OK ? «cons B h' t', ?»
+].
+whd // %
+[ @(use_sig B P)
+| cases t' #l' #p @p
+] qed.
 
 (*
@@ -239 +260 @@
 qed.
 
+(* A variation of bind and its notation that provides an equality proof for
+   later use. *)
+
+definition bind_eq ≝ λA,B:Type[0]. λf: res A. λg: ∀a:A. f = OK ? a → res B.
+  match f return λx. f = x → ? with
+  [ OK x ⇒ g x
+  | Error msg ⇒ λ_. Error ? msg
+  ] (refl ? f).
+
+notation > "vbox('do' ident v 'as' ident E ← e; break e')" with precedence 40 for @{ bind_eq ?? ${e} (λ${ident v}.λ${ident E}.${e'})}.
+
 definition res_to_opt : ∀A:Type[0]. res A → option A ≝
  λA.λv. match v with [ Error _ ⇒ None ? | OK v ⇒ Some … v].
+

src/common/Identifiers.ma

@@ -3 +3 @@
 include "ASM/Arithmetic.ma".
 include "common/Errors.ma".
+include "utilities/option.ma".
 
 (* identifiers and their generators are tagged to differentiate them, and to
@@ -122 +123 @@
 ] qed.
 
+lemma lookup_add_cases : ∀tag,A,m,i,j,a,v.
+  lookup tag A (add tag A m i a) j = Some ? v →
+  (i=j ∧ v = a) ∨ lookup tag A m j = Some ? v.
+#tag #A #m #i #j #a #v
+cases (identifier_eq ? i j)
+[ #E >E >lookup_add_hit #H %1 destruct % //
+| #NE >lookup_add_miss /2/ @eq_identifier_elim /2/
+] qed. 
+
 (* Extract every identifier, value pair from the map. *)
 definition elements : ∀tag,A. identifier_map tag A → list (identifier tag × A) ≝
@@ -147 +157 @@
   [ 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
+   and update 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.
+
+definition update_present : ∀tag,A. ∀m:identifier_map tag A. ∀id. present ?? m id → A → identifier_map tag A ≝
+λtag,A,m,l,p,a.
+  let l' ≝ match l with [ an_identifier l' ⇒ l' ] in
+  let m' ≝ match m with [ an_id_map m' ⇒ m' ] in
+  let u' ≝ update A 16 l' a m' in
+  match u' return λx. update ????? = x → ? with
+  [ None ⇒ λE.⊥
+  | Some m' ⇒ λ_. an_id_map tag A m'
+  ] (refl ? u').
+whd in p; whd in p:(?(??%?)) E:(??(???%?%)?);
+cases l in p E; cases m; -l' -m' #m' #l' whd in ⊢ (?(??(???%%)?) → ??(???%?%)? → ?)
+#NL #U cases NL #H @H @(update_fail … U)
+qed.
+
+lemma update_still_present : ∀tag,A,m,id,a,id'.
+  ∀H:present tag A m id.
+  ∀H':present tag A m id'.
+  present tag A (update_present tag A m id' H' a) id.
+#tag #A * #m * #id #a * #id' #H #H'
+whd whd in ⊢ (?(??(???(%??????)?)?)) normalize nodelta
+cases (identifier_eq ? (an_identifier tag id) (an_identifier tag id'))
+[ #E >E @refute_none_by_refl #m' #U whd in ⊢ (?(??%?)) >(update_lookup_opt_same ?????? U)
+  % #E' destruct
+| #NE @refute_none_by_refl #m' #U whd in ⊢ (?(??%?)) whd in ⊢ (?(??(???%%)?))
+  <(update_lookup_opt_other ?????? U id) [ @H | % #E cases NE >E #H @H @refl ]
+] qed.
+
 (* Sets *)