Changeset 1316 for src/common


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

Merge in id-lookup-branch to trunk.

Location:
src
Files:
3 edited

Legend:

Unmodified
Added
Removed
  • src

  • src/common/Errors.ma

    r1214 r1316  
    1818include "basics/list.ma".
    1919include "common/PreIdentifiers.ma".
     20include "utilities/lists.ma".
     21include "utilities/deppair.ma".
    2022
    2123(* * Error reporting and the error monad. *)
     
    8789notation "'ret' e" non associative with precedence 45 for @{'ret ${e}}.*)
    8890
     91(* Dependent pair version. *)
     92notation > "vbox('do' « ident v , ident p » ← e; break e')" with precedence 40
     93  for @{ bind ?? ${e} (λ${fresh x}.match ${fresh x} with [ dp ${ident v} ${ident p} ⇒ ${e'} ]) }.
     94
    8995(*
    9096(** The [do] notation, inspired by Haskell's, keeps the code readable. *)
     
    127133  | cons hd tl ⇒ do hd' ← f hd; do tl' ← mmap ?? f tl; OK ? (hd'::tl')
    128134  ].
     135
     136(* And mmap coupled with proofs. *)
     137
     138let 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') ≝
     139match l with
     140[ nil ⇒ OK ? «nil B, ?»
     141| cons h t ⇒
     142    do h' ← f h;
     143    do t' ← mmap_sigma A B P f t;
     144    OK ? «cons B h' t', ?»
     145].
     146whd // %
     147[ @(use_sig B P)
     148| cases t' #l' #p @p
     149] qed.
    129150
    130151(*
     
    239260qed.
    240261
     262(* A variation of bind and its notation that provides an equality proof for
     263   later use. *)
     264
     265definition bind_eq ≝ λA,B:Type[0]. λf: res A. λg: ∀a:A. f = OK ? a → res B.
     266  match f return λx. f = x → ? with
     267  [ OK x ⇒ g x
     268  | Error msg ⇒ λ_. Error ? msg
     269  ] (refl ? f).
     270
     271notation > "vbox('do' ident v 'as' ident E ← e; break e')" with precedence 40 for @{ bind_eq ?? ${e} (λ${ident v}.λ${ident E}.${e'})}.
     272
    241273definition res_to_opt : ∀A:Type[0]. res A → option A ≝
    242274 λA.λv. match v with [ Error _ ⇒ None ? | OK v ⇒ Some … v].
     275
  • 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.