Changeset 1949 for src/common/Errors.ma
 Timestamp:
 May 15, 2012, 5:51:25 PM (8 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

src/common/Errors.ma
r1882 r1949 6 6 include "utilities/monad.ma". 7 7 include "utilities/option.ma". 8 9 (* first, generic exception monad *)10 11 inductive except (E : Type[0]) (X : Type[0]) : Type[0] ≝12  raise : E → except E X13  success : X → except E X.14 15 definition Except ≝ λE.MakeMonadProps16 (except E)17 (success E)18 (λX,Y,m,f.match m with [raise e ⇒ raise … e  success x ⇒ f x])19 ????.20 //21 [ #X * #x %22  #X#Y#Z * #x#f#g %23  #X#Y normalize * #x #f #g #H // normalize @H24 ]25 qed.26 27 unification hint 0 ≔ E,X;28 O ≟ Except E, N ≟ max_def O29 (**) ⊢30 except E X ≡ monad N X.31 32 definition try_catch : ∀E,X.except E X → (E → X) → X ≝33 λE,X,m,f.match m with34 [ success x ⇒ x35  raise e ⇒ f e36 ].37 38 interpretation "exception try catch" 'trycatch e f = (try_catch ?? e f).39 40 definition except_elim : ∀E,X.∀m : except E X.∀P : ? → Prop.41 (∀x.m = success ?? x → P (success ?? x)) →42 (∀e.m = raise ?? e → P (raise ?? e)) →43 P m.44 #E #X * /2/45 qed.46 47 definition except_success ≝ λE,X.λm : except E X.48 match m with [success _ ⇒ True  _ ⇒ False].49 50 definition except_safe ≝51 λE,X.λm : except E X.52 match m return λx.except_success ?? x → X with53 [ success y ⇒ λ_.y54  _ ⇒ λprf.match prf in False with []55 ].56 57 definition Except_P ≝ λE.λP_e : E → Prop.mk_MonadPred (Except E)58 (λX,P,m. Try ! x ← m ; return P x catch e ⇒ P_e e) ???.59 [ //60  #X#Y #P1 #P2 * #x normalize /2/61  #X #P #Q #H * #y normalize /2/62 ]63 qed.64 65 definition except_P ≝ λE,P_e.m_pred … (Except_P E P_e).66 67 definition except_All : ∀E,X.(X → Prop) → except E X → Prop ≝68 λE : Type[0].except_P E (λe.True).69 70 definition except_Exists : ∀E,X.(X → Prop) → except E X → Prop ≝71 λE : Type[0].except_P E (λe.False).72 73 definition except_rel ≝ λE,F.λrel_e : E → F → Prop.mk_MonadRel (Except E) (Except F)74 (λX,Y,rel,m,n.75 match m with76 [ success x ⇒ match n with [success y ⇒ rel x y  _ ⇒ False]77  raise e ⇒ match n with [raise f ⇒ rel_e e f  _ ⇒ False]78 ]) ???.79 [ //80 *: #X#Y[#Z#W] #rel1 #rel2 [2: #H] * #x * #y normalize /2/ *81 ]82 qed.83 8 84 9 (* * Error reporting and the error monad. *) … … 131 56 132 57 include "hints_declaration.ma". 58 alias symbol "hint_decl" (instance 1) = "hint_decl_Type1". 133 59 unification hint 0 ≔ X; 134 60 N ≟ max_def Res
Note: See TracChangeset
for help on using the changeset viewer.