Changeset 1640 for src/common/Errors.ma
 Timestamp:
 Jan 11, 2012, 5:41:45 PM (8 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

src/common/Errors.ma
r1626 r1640 19 19 include "common/PreIdentifiers.ma". 20 20 include "basics/russell.ma". 21 include "utilities/monad.ma". 21 22 22 23 (* * Error reporting and the error monad. *) … … 48 49 (*Implicit Arguments Error [A].*) 49 50 50 (* * To automate the propagation of errors, we use a monadic style 51 with the following [bind] operation. *) 52 53 definition bind ≝ λA,B:Type[0]. λf: res A. λg: A → res B. 54 match f with 55 [ OK x ⇒ g x 56  Error msg ⇒ Error ? msg 57 ]. 58 59 definition bind2 ≝ λA,B,C: Type[0]. λf: res (A × B). λg: A → B → res C. 60 match f with 61 [ OK v ⇒ g (fst … v) (snd … v) 62  Error msg => Error ? msg 63 ]. 64 65 definition bind3 ≝ λA,B,C,D: Type[0]. λf: res (A × B × C). λg: A → B → C → res D. 66 match f with 67 [ OK v ⇒ g (fst … (fst … v)) (snd … (fst … v)) (snd … v) 68  Error msg => Error ? msg 69 ]. 70 71 (* Not sure what level to use *) 72 notation > "vbox('do' ident v ← e; break e')" with precedence 40 for @{'bind ${e} (λ${ident v}.${e'})}. 73 notation > "vbox('do' ident v : ty ← e; break e')" with precedence 40 for @{'bind ${e} (λ${ident v} : ${ty}.${e'})}. 74 notation < "vbox('do' \nbsp ident v ← e; break e')" with precedence 40 for @{'bind ${e} (λ${ident v}.${e'})}. 75 notation < "vbox('do' \nbsp ident v : ty ← e; break e')" with precedence 40 for @{'bind ${e} (λ${ident v} : ${ty}.${e'})}. 76 interpretation "error monad bind" 'bind e f = (bind ?? e f). 77 notation > "vbox('do' 〈ident v1, ident v2〉 ← e; break e')" with precedence 40 for @{'bind2 ${e} (λ${ident v1}.λ${ident v2}.${e'})}. 78 notation > "vbox('do' 〈ident v1 : ty1, ident v2 : ty2〉 ← e; break e')" with precedence 40 for @{'bind2 ${e} (λ${ident v1} : ${ty1}.λ${ident v2} : ${ty2}.${e'})}. 79 notation < "vbox('do' \nbsp 〈ident v1, ident v2〉 ← e; break e')" with precedence 40 for @{'bind2 ${e} (λ${ident v1}.λ${ident v2}.${e'})}. 80 notation < "vbox('do' \nbsp 〈ident v1 : ty1, ident v2 : ty2〉 ← e; break e')" with precedence 40 for @{'bind2 ${e} (λ${ident v1} : ${ty1}.λ${ident v2} : ${ty2}.${e'})}. 81 interpretation "error monad Prod bind" 'bind2 e f = (bind2 ??? e f). 82 notation > "vbox('do' 〈ident v1, ident v2, ident v3〉 ← e; break e')" with precedence 40 for @{'bind3 ${e} (λ${ident v1}.λ${ident v2}.λ${ident v3}.${e'})}. 83 notation > "vbox('do' 〈ident v1 : ty1, ident v2 : ty2, ident v3 : ty3〉 ← e; break e')" with precedence 40 for @{'bind3 ${e} (λ${ident v1} : ${ty1}.λ${ident v2} : ${ty2}.λ${ident v3} : ${ty3}.${e'})}. 84 notation < "vbox('do' \nbsp 〈ident v1, ident v2, ident v3〉 ← e; break e')" with precedence 40 for @{'bind3 ${e} (λ${ident v1}.λ${ident v2}.λ${ident v3}.${e'})}. 85 notation < "vbox('do' \nbsp 〈ident v1 : ty1, ident v2 : ty2, ident v3 : ty3〉 ← e; break e')" with precedence 40 for @{'bind3 ${e} (λ${ident v1} : ${ty1}.λ${ident v2} : ${ty2}.λ${ident v3} : ${ty3}.${e'})}. 86 interpretation "error monad triple bind" 'bind3 e f = (bind3 ???? e f). 87 (*interpretation "error monad ret" 'ret e = (ret ? e). 88 notation "'ret' e" non associative with precedence 45 for @{'ret ${e}}.*) 89 90 (* Dependent pair version. *) 51 definition Res : Monad ≝ MakeMonad (mk_MonadDefinition 52 (* the monad *) 53 res 54 (* return *) 55 (λX.OK X) 56 (* bind *) 57 (λX,Y,m,f. match m with [ OK x ⇒ f x  Error msg ⇒ Error ? msg]) 58 ???). 59 // 60 [(* bind_bind *) 61 #X#Y#Z*normalize // 62 (* bind_ret *) 63 #X*normalize // 64 ] 65 qed. 66 67 include "hints_declaration.ma". 68 unification hint 0 ≔ X; 69 M ≟ m_def Res 70 (**) ⊢ 71 res X ≡ monad M X 72 . 73 74 (*(* Dependent pair version. *) 91 75 notation > "vbox('do' « ident v , ident p » ← e; break e')" with precedence 40 92 76 for @{ bind ?? ${e} (λ${fresh x}.match ${fresh x} with [ mk_Sig ${ident v} ${ident p} ⇒ ${e'} ]) }. … … 110 94 111 95 notation > "vbox('do' «ident v1, ident v2, ident H» ← e; break e')" with precedence 40 for @{'sigbind2 ${e} (λ${ident v1}.λ${ident v2}.λ${ident H}.${e'})}. 112 interpretation "error monad sig Prod bind" 'sigbind2 e f = (sigbind2 ???? e f). 113 114 (* 115 (** The [do] notation, inspired by Haskell's, keeps the code readable. *) 116 117 Notation "'do' X < A ; B" := (bind A (fun X => B)) 118 (at level 200, X ident, A at level 100, B at level 200) 119 : error_monad_scope. 120 121 Notation "'do' ( X , Y ) < A ; B" := (bind2 A (fun X Y => B)) 122 (at level 200, X ident, Y ident, A at level 100, B at level 200) 123 : error_monad_scope. 124 *) 125 lemma bind_inversion: 96 interpretation "error monad sig Prod bind" 'sigbind2 e f = (sigbind2 ???? e f).*) 97 98 lemma res_bind_inversion: 126 99 ∀A,B: Type[0]. ∀f: res A. ∀g: A → res B. ∀y: B. 127 bind ?? f g = OK ? y→128 ∃x. f = OK ? x ∧ g x = OK ? y.129 #A #B #f #g #y cases f ;130 [ #a #e %{a} whd in e:(??%?); /2/;131  #m #H whd in H:(??%?); destruct (H);100 (f »= g = return y) → 101 ∃x. (f = return x) ∧ (g x = return y). 102 #A #B #f #g #y cases f normalize 103 [ #a #e %{a} /2 by conj/ 104  #m #H destruct (H) 132 105 ] qed. 133 106 134 107 lemma bind2_inversion: 135 108 ∀A,B,C: Type[0]. ∀f: res (A×B). ∀g: A → B → res C. ∀z: C. 136 bind2 ??? f g = OK ?z →137 ∃x. ∃y. f = OK ? 〈x, y〉 ∧ g x y = OK ?z.138 #A #B #C #f #g #z cases f ;139 [ #ab cases ab; #a #b #e %{a} %{b} whd in e:(??%?); /2/;140  #m #H whd in H:(??%?); destruct109 m_bind2 ???? f g = return z → 110 ∃x. ∃y. f = return 〈x, y〉 ∧ g x y = return z. 111 #A #B #C #f #g #z cases f normalize 112 [ * #a #b normalize #e %{a} %{b} /2 by conj/ 113  #m #H destruct (H) 141 114 ] qed. 142 115 143 116 (* 144 Open Local Scope error_monad_scope. 145 146 (** This is the familiar monadic map iterator. *) 147 *) 148 149 let rec mmap (A, B: Type[0]) (f: A → res B) (l: list A) on l : res (list B) ≝ 150 match l with 151 [ nil ⇒ OK ? [] 152  cons hd tl ⇒ do hd' ← f hd; do tl' ← mmap ?? f tl; OK ? (hd'::tl') 153 ]. 154 155 (* And mmap coupled with proofs. *) 156 157 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') ≝ 158 match l with 159 [ nil ⇒ OK ? «nil B, ?» 160  cons h t ⇒ 161 do h' ← f h; 162 do t' ← mmap_sigma A B P f t; 163 OK ? «cons B h' t', ?» 164 ]. 165 whd // % 166 [ @(pi2 … h') 167  cases t' #l' #p @p 168 ] qed. 117 Open Local Scope error_monad_scope.*) 169 118 170 119 (* … … 189 138 [ nil ⇒ x 190 139  cons hd tl ⇒ 191 dox ← x ;140 ! x ← x ; 192 141 mfold_left_i_aux A B f (f i x hd) (S i) tl 193 142 ]. … … 213 162 [ nil ⇒ Error ? (msg WrongLength) 214 163  cons hd' tl' ⇒ 215 doaccu ← accu;164 ! accu ← accu; 216 165 mfold_left2 … f (f accu hd hd') tl tl' 217 166 ] … … 301 250 ] (refl ? f). 302 251 303 notation > "vbox(' do' ident v 'as' ident E ← e; break e')" with precedence 40 for @{ bind_eq ?? ${e} (λ${ident v}.λ${ident E}.${e'})}.252 notation > "vbox('!' ident v 'as' ident E ← e; break e')" with precedence 40 for @{ bind_eq ?? ${e} (λ${ident v}.λ${ident E}.${e'})}. 304 253 305 254 definition bind2_eq ≝ λA,B,C:Type[0]. λf: res (A×B). λg: ∀a:A.∀b:B. f = OK ? 〈a,b〉 → res C. … … 309 258 ] (refl ? f). 310 259 311 notation > "vbox(' do' 〈ident v1, ident v2〉 'as' ident E ← e; break e')" with precedence 40 for @{ bind2_eq ??? ${e} (λ${ident v1}.λ${ident v2}.λ${ident E}.${e'})}.260 notation > "vbox('!' 〈ident v1, ident v2〉 'as' ident E ← e; break e')" with precedence 40 for @{ bind2_eq ??? ${e} (λ${ident v1}.λ${ident v2}.λ${ident E}.${e'})}. 312 261 313 262 definition res_to_opt : ∀A:Type[0]. res A → option A ≝
Note: See TracChangeset
for help on using the changeset viewer.