Changeset 487 for Deliverables/D3.1/Csemantics/Errors.ma
 Timestamp:
 Feb 9, 2011, 11:49:17 AM (9 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

Deliverables/D3.1/Csemantics/Errors.ma
r485 r487 14 14 (* *********************************************************************) 15 15 16 include "datatypes/pairs.ma". 17 include "Plogic/equality.ma". 18 include "Plogic/connectives.ma". 19 include "datatypes/sums.ma". 16 include "basics/types.ma". 17 include "basics/logic.ma". 20 18 21 19 (* * Error reporting and the error monad. *) … … 41 39 or [Error msg] to indicate failure. *) 42 40 43 ninductive res (A: Type) : Type≝41 inductive res (A: Type[0]) : Type[0] ≝ 44 42  OK: A → res A 45 43  Error: (* FIXME errmsg →*) res A. … … 50 48 with the following [bind] operation. *) 51 49 52 ndefinition bind ≝ λA,B:Type. λf: res A. λg: A → res B.50 definition bind ≝ λA,B:Type[0]. λf: res A. λg: A → res B. 53 51 match f with 54 52 [ OK x ⇒ g x … … 56 54 ]. 57 55 58 ndefinition bind2 ≝ λA,B,C: Type. λf: res (A × B). λg: A → B → res C.56 definition bind2 ≝ λA,B,C: Type[0]. λf: res (A × B). λg: A → B → res C. 59 57 match f with 60 [ OK v ⇒ match v with [ mk_pair x y ⇒ g x y ]58 [ OK v ⇒ match v with [ pair x y ⇒ g x y ] 61 59  Error (*msg*) => Error ? (*msg*) 62 60 ]. … … 72 70 notation < "vbox('do' \nbsp 〈ident v1, ident v2〉 ← e; break e')" with precedence 40 for @{'bind2 ${e} (λ${ident v1}.λ${ident v2}.${e'})}. 73 71 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'})}. 74 interpretation "error monad pairbind" 'bind2 e f = (bind2 ??? e f).72 interpretation "error monad Prod bind" 'bind2 e f = (bind2 ??? e f). 75 73 (*interpretation "error monad ret" 'ret e = (ret ? e). 76 74 notation "'ret' e" non associative with precedence 45 for @{'ret ${e}}.*) … … 87 85 : error_monad_scope. 88 86 *) 89 nremarkbind_inversion:90 ∀A,B: Type . ∀f: res A. ∀g: A → res B. ∀y: B.87 lemma bind_inversion: 88 ∀A,B: Type[0]. ∀f: res A. ∀g: A → res B. ∀y: B. 91 89 bind ?? f g = OK ? y → 92 90 ∃x. f = OK ? x ∧ g x = OK ? y. 93 #A B f g y; ncases f;94 ##[ #a e; @a; nwhd in e:(??%?); /2/;95 ## #H; nwhd in H:(??%?); ndestruct (H);96 ##] nqed.97 98 nremarkbind2_inversion:99 ∀A,B,C: Type . ∀f: res (A×B). ∀g: A → B → res C. ∀z: C.91 #A #B #f #g #y cases f; 92 [ #a #e %{a} whd in e:(??%?); /2/; 93  #H whd in H:(??%?); destruct (H); 94 ] qed. 95 96 lemma bind2_inversion: 97 ∀A,B,C: Type[0]. ∀f: res (A×B). ∀g: A → B → res C. ∀z: C. 100 98 bind2 ??? f g = OK ? z → 101 99 ∃x. ∃y. f = OK ? 〈x, y〉 ∧ g x y = OK ? z. 102 #A B C f g z; ncases f;103 ##[ #ab; ncases ab; #a b e; @a; @b; nwhd in e:(??%?); /2/;104 ## #H; nwhd in H:(??%?); ndestruct105 ##] nqed.100 #A #B #C #f #g #z cases f; 101 [ #ab cases ab; #a #b #e %{a} %{b} whd in e:(??%?); /2/; 102  #H whd in H:(??%?); destruct 103 ] qed. 106 104 107 105 (* … … 195 193 196 194 197 ndefinition opt_to_res ≝ λA.λv:option A. match v with [ None ⇒ Error A  Some v ⇒ OK A v ].198 nlemma opt_OK: ∀A,P,e.195 definition opt_to_res ≝ λA.λv:option A. match v with [ None ⇒ Error A  Some v ⇒ OK A v ]. 196 lemma opt_OK: ∀A,P,e. 199 197 (∀v. e = Some ? v → P v) → 200 198 match opt_to_res A e with [ Error ⇒ True  OK v ⇒ P v ]. 201 #A P e; nelim e; /2/;202 nqed.199 #A #P #e elim e; /2/; 200 qed.
Note: See TracChangeset
for help on using the changeset viewer.