Changeset 1316 for src/common/Errors.ma


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/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
Note: See TracChangeset for help on using the changeset viewer.