Changeset 1882 for src/common/Errors.ma
 Timestamp:
 Apr 6, 2012, 8:02:10 PM (9 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

src/common/Errors.ma
r1647 r1882 1 (* *********************************************************************)2 (* *)3 (* The Compcert verified compiler *)4 (* *)5 (* Xavier Leroy, INRIA ParisRocquencourt *)6 (* *)7 (* Copyright Institut National de Recherche en Informatique et en *)8 (* Automatique. All rights reserved. This file is distributed *)9 (* under the terms of the GNU General Public License as published by *)10 (* the Free Software Foundation, either version 2 of the License, or *)11 (* (at your option) any later version. This file is also distributed *)12 (* under the terms of the INRIA NonCommercial License Agreement. *)13 (* *)14 (* *********************************************************************)15 16 1 include "basics/types.ma". 17 2 include "basics/logic.ma". … … 20 5 include "basics/russell.ma". 21 6 include "utilities/monad.ma". 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 X 13  success : X → except E X. 14 15 definition Except ≝ λE.MakeMonadProps 16 (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 @H 24 ] 25 qed. 26 27 unification hint 0 ≔ E,X; 28 O ≟ Except E, N ≟ max_def O 29 (**) ⊢ 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 with 34 [ success x ⇒ x 35  raise e ⇒ f e 36 ]. 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 with 53 [ success y ⇒ λ_.y 54  _ ⇒ λ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 with 76 [ 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. 22 83 23 84 (* * Error reporting and the error monad. *) … … 42 103 The return value is either [OK res] to indicate success, 43 104 or [Error msg] to indicate failure. *) 105 106 (* Paolo: not using except for backward compatbility 107 (would break Error ? msg) *) 44 108 45 109 inductive res (A: Type[0]) : Type[0] ≝ … … 56 120 (* bind *) 57 121 (λX,Y,m,f. match m with [ OK x ⇒ f x  Error msg ⇒ Error ? msg]) 58 ??? .122 ????. 59 123 // 60 124 [(* bind_ret *) … … 62 126 (* bind_bind *) 63 127 #X#Y#Z*normalize // 128  normalize #X #Y * normalize /2/ 64 129 ] 65 130 qed. … … 67 132 include "hints_declaration.ma". 68 133 unification hint 0 ≔ X; 69 N ≟ max_def Res , M ≟ m_def N134 N ≟ max_def Res 70 135 (**) ⊢ 71 res X ≡ monad MX136 res X ≡ monad N X 72 137 . 73 138 … … 267 332 definition bind2 ≝ m_bind2 Res. 268 333 definition bind3 ≝ m_bind3 Res. 269 definition mmap ≝ m_ mmap Res.270 definition mmap_sigma ≝ m_ mmap_sigma Res.334 definition mmap ≝ m_list_map Res. 335 definition mmap_sigma ≝ m_list_map_sigma Res.
Note: See TracChangeset
for help on using the changeset viewer.