Changeset 1882 for src/common/Errors.ma


Ignore:
Timestamp:
Apr 6, 2012, 8:02:10 PM (9 years ago)
Author:
tranquil
Message:

big update, alas incomplete:
joint changed a bit, and all BE languages need to be updated
started development of blocks to aid preservation results, but still incomplete
if it breaks too many things, feel free to roll back

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 Paris-Rocquencourt                     *)
    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 Non-Commercial License Agreement.     *)
    13 (*                                                                     *)
    14 (* *********************************************************************)
    15 
    161include "basics/types.ma".
    172include "basics/logic.ma".
     
    205include "basics/russell.ma".
    216include "utilities/monad.ma".
     7include "utilities/option.ma".
     8
     9(* first, generic exception monad *)
     10
     11inductive except (E : Type[0]) (X : Type[0]) : Type[0] ≝
     12  | raise : E → except E X
     13  | success : X → except E X.
     14
     15definition 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]
     25qed.
     26
     27unification hint 0 ≔ E,X;
     28O ≟ Except E, N ≟ max_def O
     29(*--------------------------------------*) ⊢
     30except E X ≡ monad N X.
     31
     32definition 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
     38interpretation "exception try catch" 'trycatch e f = (try_catch ?? e f).
     39
     40definition 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/
     45qed.
     46
     47definition except_success ≝ λE,X.λm : except E X.
     48  match m with [success _ ⇒ True | _ ⇒ False].
     49
     50definition 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
     57definition 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]
     63qed.
     64
     65definition except_P ≝ λE,P_e.m_pred … (Except_P E P_e).
     66
     67definition except_All : ∀E,X.(X → Prop) → except E X → Prop ≝
     68  λE : Type[0].except_P E (λe.True).
     69
     70definition except_Exists : ∀E,X.(X → Prop) → except E X → Prop ≝
     71  λE : Type[0].except_P E (λe.False).
     72
     73definition 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]
     82qed.
    2283
    2384(* * Error reporting and the error monad. *)
     
    42103  The return value is either [OK res] to indicate success,
    43104  or [Error msg] to indicate failure. *)
     105
     106(* Paolo: not using except for backward compatbility
     107  (would break Error ? msg) *)
    44108
    45109inductive res (A: Type[0]) : Type[0] ≝
     
    56120  (* bind *)
    57121  (λX,Y,m,f. match m with [ OK x ⇒ f x | Error msg ⇒ Error ? msg])
    58   ???.
     122  ????.
    59123//
    60124[(* bind_ret *)
     
    62126|(* bind_bind *)
    63127 #X#Y#Z*normalize //
     128| normalize #X #Y * normalize /2/
    64129]
    65130qed.
     
    67132include "hints_declaration.ma".
    68133unification hint 0 ≔ X;
    69 N ≟ max_def Res, M ≟ m_def N
     134N ≟ max_def Res
    70135(*---------------*) ⊢
    71 res X ≡ monad M X
     136res X ≡ monad N X
    72137.
    73138
     
    267332definition bind2 ≝ m_bind2 Res.
    268333definition bind3 ≝ m_bind3 Res.
    269 definition mmap ≝ m_mmap Res.
    270 definition mmap_sigma ≝ m_mmap_sigma Res.
     334definition mmap ≝ m_list_map Res.
     335definition mmap_sigma ≝ m_list_map_sigma Res.
Note: See TracChangeset for help on using the changeset viewer.