Changeset 1102 for Deliverables/D3.3/idlookupbranch/common
 Timestamp:
 Aug 4, 2011, 1:55:53 PM (9 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

Deliverables/D3.3/idlookupbranch/common/Errors.ma
r797 r1102 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 (* … … 214 235 #A #m #P #e elim e; /2/; 215 236 qed. 237 238 (* A variation of bind and its notation that provides an equality proof for 239 later use. *) 240 241 definition bind_eq ≝ λA,B:Type[0]. λf: res A. λg: ∀a:A. f = OK ? a → res B. 242 match f return λx. f = x → ? with 243 [ OK x ⇒ g x 244  Error msg ⇒ λ_. Error ? msg 245 ] (refl ? f). 246 247 notation > "vbox('do' ident v 'as' ident E ← e; break e')" with precedence 40 for @{ bind_eq ?? ${e} (λ${ident v}.λ${ident E}.${e'})}. 248
Note: See TracChangeset
for help on using the changeset viewer.