Changeset 1949 for src/common/Errors.ma


Ignore:
Timestamp:
May 15, 2012, 5:51:25 PM (8 years ago)
Author:
tranquil
Message:
  • lemma trace rel to eq flatten trace
  • some more properties of generic monad relations and predicates
  • removed 'iff notation from extralib as already there
File:
1 edited

Legend:

Unmodified
Added
Removed

  • src/common/Errors.ma

    r1882 r1949  
    66include "utilities/monad.ma".
    77include "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.
    838
    849(* * Error reporting and the error monad. *)
    … …  
    13156
    13257include "hints_declaration.ma".
     58alias symbol "hint_decl" (instance 1) = "hint_decl_Type1".
    13359unification hint 0 ≔ X;
    13460N ≟ max_def Res
Note: See TracChangeset for help on using the changeset viewer.