Changeset 1316 for src/common/Errors.ma
 Timestamp:
 Oct 7, 2011, 12:26:39 PM (9 years ago)
 Location:
 src
 Files:

 2 edited
Legend:
 Unmodified
 Added
 Removed

src

Property
svn:mergeinfo
set to
/Deliverables/D3.3/idlookupbranch merged eligible

Property
svn:mergeinfo
set to

src/common/Errors.ma
r1214 r1316 18 18 include "basics/list.ma". 19 19 include "common/PreIdentifiers.ma". 20 include "utilities/lists.ma". 21 include "utilities/deppair.ma". 20 22 21 23 (* * Error reporting and the error monad. *) … … 87 89 notation "'ret' e" non associative with precedence 45 for @{'ret ${e}}.*) 88 90 91 (* Dependent pair version. *) 92 notation > "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 89 95 (* 90 96 (** 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') 128 134 ]. 135 136 (* And mmap coupled with proofs. *) 137 138 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') ≝ 139 match 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 ]. 146 whd // % 147 [ @(use_sig B P) 148  cases t' #l' #p @p 149 ] qed. 129 150 130 151 (* … … 239 260 qed. 240 261 262 (* A variation of bind and its notation that provides an equality proof for 263 later use. *) 264 265 definition 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 271 notation > "vbox('do' ident v 'as' ident E ← e; break e')" with precedence 40 for @{ bind_eq ?? ${e} (λ${ident v}.λ${ident E}.${e'})}. 272 241 273 definition res_to_opt : ∀A:Type[0]. res A → option A ≝ 242 274 λA.λv. match v with [ Error _ ⇒ None ?  OK v ⇒ Some … v]. 275
Note: See TracChangeset
for help on using the changeset viewer.