Changeset 797 for src/common


Ignore:
Timestamp:
May 13, 2011, 1:10:23 PM (9 years ago)
Author:
campbell
Message:

Add error messages wherever the error monad is used.
Sticks to CompCert? style strings+identifiers for the moment.
Use axioms for strings as we currently have no representation or literals
for them - still *very* useful for animation in the proof assistant.

Location:
src/common
Files:
1 added
8 edited

Legend:

Unmodified
Added
Removed
  • src/common/Animation.ma

    r731 r797  
    1010λo,ev.
    1111match io_in_typ o return λt. res (eventval_type t) with
    12 [ ASTint ⇒ match ev with [ EVint i ⇒ OK ? i | _ ⇒ Error ? ]
    13 | ASTfloat ⇒ match ev with [ EVfloat f ⇒ OK ? f | _ ⇒ Error ? ]
    14 | ASTptr _ ⇒ Error ?
     12[ ASTint ⇒ match ev with [ EVint i ⇒ OK ? i | _ ⇒ Error ? (msg IllTypedEvent) ]
     13| ASTfloat ⇒ match ev with [ EVfloat f ⇒ OK ? f | _ ⇒ Error ? (msg IllTypedEvent) ]
     14| ASTptr _ ⇒ Error ? (msg IllTypedEvent)
    1515].
    1616
     
    2020| input_exhausted : trace → snapshot state.
    2121
     22axiom StoppedMidIO : String.
     23
    2224let rec up_to_nth_step (n:nat) (ex:execstep io_out io_in) (input:list eventval) (e:execution (state ?? ex) io_out io_in) (t:trace) : res (snapshot (state ?? ex)) ≝
    2325match n with
    2426[ O ⇒ match e with [ e_step tr s _ ⇒ OK ? (running ? (t⧺tr) s)
    2527                   | e_stop tr r m ⇒ OK ? (finished ? (t⧺tr) r m)
    26                    | _ ⇒ Error ? ]
     28                   | e_interact o k ⇒ Error ? (msg StoppedMidIO)
     29                   | e_wrong m ⇒ Error ? m ]
    2730| S m ⇒ match e with [ e_step tr s e' ⇒ up_to_nth_step m ex input e' (t⧺tr)
    2831                     | e_stop tr r m ⇒ OK ? (finished ? (t⧺tr) r m)
     
    3336                                       up_to_nth_step m ex tl (k i) t
    3437                         ]
    35                      | e_wrong ⇒ Error ?
     38                     | e_wrong m ⇒ Error ? m
    3639                     ]
    3740].
  • src/common/Errors.ma

    r764 r797  
    1717include "basics/logic.ma".
    1818include "basics/list.ma".
     19include "common/PreIdentifiers.ma".
    1920
    2021(* * Error reporting and the error monad. *)
    21 (*
    22 (** * Representation of error messages. *)
    23 
    24 (** Compile-time errors produce an error message, represented in Coq
     22
     23(* * * Representation of error messages. *)
     24
     25(* * Compile-time errors produce an error message, represented in Coq
    2526  as a list of either substrings or positive numbers encoding
    2627  a source-level identifier (see module AST). *)
    2728
    28 Inductive errcode: Type :=
    29   | MSG: string -> errcode
    30   | CTX: positive -> errcode.
    31 
    32 Definition errmsg: Type := list errcode.
    33 
    34 Definition msg (s: string) : errmsg := MSG s :: nil.
    35 *)
     29inductive errcode: Type[0] :=
     30  | MSG: String → errcode
     31  | CTX: ∀tag:String. identifier tag → errcode.
     32
     33definition errmsg: Type[0] ≝ list errcode.
     34
     35definition msg : String → errmsg ≝ λs. [MSG s].
     36
    3637(* * * The error monad *)
    3738
     
    4243inductive res (A: Type[0]) : Type[0] ≝
    4344| OK: A → res A
    44 | Error: (* FIXME errmsg →*) res A.
     45| Error: errmsg → res A.
    4546
    4647(*Implicit Arguments Error [A].*)
     
    5253  match f with
    5354  [ OK x ⇒ g x
    54   | Error (*msg*) ⇒ Error ? (*msg*)
     55  | Error msg ⇒ Error ? msg
    5556  ].
    5657
     
    5859  match f with
    5960  [ OK v ⇒ match v with [ pair x y ⇒ g x y ]
    60   | Error (*msg*) => Error ? (*msg*)
     61  | Error msg => Error ? msg
    6162  ].
    6263
     
    6465  match f with
    6566  [ OK v ⇒ match v with [ pair xy z ⇒ match xy with [ pair x y ⇒ g x y z ] ]
    66   | Error (*msg*) => Error ? (*msg*)
     67  | Error msg => Error ? msg
    6768  ].
    6869 
     
    103104#A #B #f #g #y cases f;
    104105[ #a #e %{a} whd in e:(??%?); /2/;
    105 | #H whd in H:(??%?); destruct (H);
     106| #m #H whd in H:(??%?); destruct (H);
    106107] qed.
    107108
     
    112113#A #B #C #f #g #z cases f;
    113114[ #ab cases ab; #a #b #e %{a} %{b} whd in e:(??%?); /2/;
    114 | #H whd in H:(??%?); destruct
     115| #m #H whd in H:(??%?); destruct
    115116] qed.
    116117
     
    207208
    208209
    209 definition opt_to_res ≝ λA.λv:option A. match v with [ None ⇒ Error A | Some v ⇒ OK A v ].
    210 lemma opt_OK: ∀A,P,e.
     210definition opt_to_res ≝ λA.λmsg.λv:option A. match v with [ None ⇒ Error A msg | Some v ⇒ OK A v ].
     211lemma opt_OK: ∀A,m,P,e.
    211212  (∀v. e = Some ? v → P v) →
    212   match opt_to_res A e with [ Error ⇒ True | OK v ⇒ P v ].
    213 #A #P #e elim e; /2/;
     213  match opt_to_res A m e with [ Error _ ⇒ True | OK v ⇒ P v ].
     214#A #m #P #e elim e; /2/;
    214215qed.
  • src/common/Globalenvs.ma

    r758 r797  
    483483(* init *)
    484484
     485axiom InitDataStoreFailed : String.
     486
    485487definition add_globals : ∀F,V:Type[0].
    486488       genv F × mem → list (ident × (list init_data) × region × V) →
     
    495497        match alloc_init_data st init r with [ pair st' b ⇒
    496498          let g' ≝ add_symbol ? id b g in
    497           do st'' ← opt_to_res ? (store_init_data_list F g' st' b OZ init);
     499          do st'' ← opt_to_res ? (msg InitDataStoreFailed) (store_init_data_list F g' st' b OZ init);
    498500            OK ? 〈g', st''〉
    499501        ] ] ] ])
  • src/common/IO.ma

    r731 r797  
    2020#ty cases ty; normalize; // * *; qed.
    2121
     22axiom IllTypedEvent : String.
     23
    2224definition convert_eventval : ∀ev:eventval. ∀ty:typ. res val ≝
    2325λev,ty.
    2426match ty with
    25 [ ASTint ⇒ match ev with [ EVint i ⇒ OK ? (Vint i) | _ ⇒ Error ? ]
    26 | ASTfloat ⇒ match ev with [ EVfloat f ⇒ OK ? (Vfloat f) | _ ⇒ Error ? ]
    27 | _ ⇒ Error ?
     27[ ASTint ⇒ match ev with [ EVint i ⇒ OK ? (Vint i) | _ ⇒ Error ? (msg IllTypedEvent)]
     28| ASTfloat ⇒ match ev with [ EVfloat f ⇒ OK ? (Vfloat f) | _ ⇒ Error ? (msg IllTypedEvent)]
     29| _ ⇒ Error ? (msg IllTypedEvent)
    2830].
    2931
     
    3133λv,ty.
    3234match ty with
    33 [ ASTint ⇒ match v with [ Vint i ⇒ OK ? (EVint i) | _ ⇒ Error ? ]
    34 | ASTfloat ⇒ match v with [ Vfloat f ⇒ OK ? (EVfloat f) | _ ⇒ Error ? ]
    35 | _ ⇒ Error ?
     35[ ASTint ⇒ match v with [ Vint i ⇒ OK ? (EVint i) | _ ⇒ Error ? (msg IllTypedEvent) ]
     36| ASTfloat ⇒ match v with [ Vfloat f ⇒ OK ? (EVfloat f) | _ ⇒ Error ? (msg IllTypedEvent) ]
     37| _ ⇒ Error ? (msg IllTypedEvent)
    3638].
    3739
    3840let rec check_eventval_list (vs: list val) (tys: list typ) : res (list eventval) ≝
    3941match vs with
    40 [ nil ⇒ match tys with [ nil ⇒ OK ? (nil ?) | _ ⇒ Error ? ]
     42[ nil ⇒ match tys with [ nil ⇒ OK ? (nil ?) | _ ⇒ Error ? (msg IllTypedEvent) ]
    4143| cons v vt ⇒
    4244  match tys with
    43   [ nil ⇒ Error ?
     45  [ nil ⇒ Error ? (msg IllTypedEvent)
    4446  | cons ty tyt ⇒
    4547    do ev ← check_eventval' v ty;
  • src/common/IOMonad.ma

    r700 r797  
    77| Interact : ∀o:output. (input o → IO output input T) → IO output input T
    88| Value : T → IO output input T
    9 | Wrong : IO output input T.
     9| Wrong : errmsg → IO output input T.
    1010
    1111let rec bindIO (O:Type[0]) (I:O → Type[0]) (T,T':Type[0]) (v:IO O I T) (f:T → IO O I T') on v : IO O I T' ≝
     
    1313[ Interact out k ⇒ (Interact ??? out (λres. bindIO O I T T' (k res) f))
    1414| Value v' ⇒ (f v')
    15 | Wrong ⇒ Wrong O I T'
     15| Wrong m ⇒ Wrong O I T' m
    1616].
    1717
     
    2020[ Interact out k ⇒ (Interact ??? out (λres. bindIO2 ?? T1 T2 T' (k res) f))
    2121| Value v' ⇒ match v' with [ pair v1 v2 ⇒ f v1 v2 ]
    22 | Wrong ⇒ Wrong ?? T'
     22| Wrong m ⇒ Wrong ?? T' m
    2323].
    2424
    2525definition err_to_io : ∀O,I,T. res T → IO O I T ≝
    26 λO,I,T,v. match v with [ OK v' ⇒ Value O I T v' | Error ⇒ Wrong O I T ].
     26λO,I,T,v. match v with [ OK v' ⇒ Value O I T v' | Error m ⇒ Wrong O I T m ].
    2727coercion err_to_io : ∀O,I,A.∀c:res A.IO O I A ≝ err_to_io on _c:res ? to IO ???.
    2828definition err_to_io_sig : ∀O,I,T.∀P:T → Prop. res (Sig T P) → IO O I (Sig T P) ≝
    29 λO,I,T,P,v. match v with [ OK v' ⇒ Value O I (Sig T P) v' | Error ⇒ Wrong O I (Sig T P) ].
     29λO,I,T,P,v. match v with [ OK v' ⇒ Value O I (Sig T P) v' | Error m ⇒ Wrong O I (Sig T P) m ].
    3030(*coercion err_to_io_sig : ∀O,I,A.∀P:A → Prop.∀c:res (Sig A P).IO O I (Sig A P) ≝ err_to_io_sig on _c:res (Sig ??) to IO ?? (Sig ??).*)
    3131
     
    4545let rec P_io O I (A:Type[0]) (P:A → Prop) (v:IO O I A) on v : Prop ≝
    4646match v return λ_.Prop with
    47 [ Wrong ⇒ True
     47[ Wrong _ ⇒ True
    4848| Value z ⇒ P z
    4949| Interact out k ⇒ ∀v'.P_io O I A P (k v')
     
    5252let rec P_io' O I (A:Type[0]) (P:A → Prop) (v:IO O I A) on v : Prop ≝
    5353match v return λ_.Prop with
    54 [ Wrong ⇒ False
     54[ Wrong _ ⇒ False
    5555| Value z ⇒ P z
    5656| Interact out k ⇒ ∀v'.P_io' O I A P (k v')
     
    6565let rec io_inject_0 O I (A:Type[0]) (P:A → Prop) (a:IO O I A) (p:P_io O I A P a) on a : IO O I (Sig A P) ≝
    6666(match a return λa'.P_io O I A P a' → ? with
    67  [ Wrong ⇒ λ_. Wrong O I ?
     67 [ Wrong m ⇒ λ_. Wrong O I ? m
    6868 | Value c ⇒ λp'. Value ??? (dp A P c p')
    6969 | Interact out k ⇒ λp'. Interact ??? out (λv. io_inject_0 O I A P (k v) (p' v))
     
    8080let rec io_eject O I (A:Type[0]) (P: A → Prop) (a:IO O I (Sig A P)) on a : IO O I A ≝
    8181match a with
    82 [ Wrong ⇒ Wrong ???
     82[ Wrong m ⇒ Wrong ??? m
    8383| Value b ⇒ match b with [ dp w p ⇒ Value ??? w]
    8484| Interact out k ⇒ Interact ??? out (λv. io_eject ?? A P (k v))
     
    9191  on _c:IO ?? (Sig ? ?) to IO ???.
    9292
    93 definition opt_to_io : ∀O,I,T.option T → IO O I T ≝
    94 λO,I,T,v. match v with [ None ⇒ Wrong ?? T | Some v' ⇒ Value ??? v' ].
    95 coercion opt_to_io : ∀O,I,T.∀v:option T. IO O I T ≝ opt_to_io on _v:option ? to IO ???.
     93definition opt_to_io : ∀O,I,T.errmsg → option T → IO O I T ≝
     94λO,I,T,m,v. match v with [ None ⇒ Wrong ?? T m | Some v' ⇒ Value ??? v' ].
    9695
    9796lemma sig_bindIO_OK: ∀O,I,A,B. ∀P:A → Prop. ∀P':B → Prop. ∀e:IO O I (Sig A P). ∀f:Sig A P → IO O I B.
     
    113112] qed.
    114113
    115 lemma opt_bindIO_OK: ∀O,I,A,B. ∀P:B → Prop. ∀e:option A. ∀f: A → IO O I B.
     114lemma opt_bindIO_OK: ∀O,I,A,B,m. ∀P:B → Prop. ∀e:option A. ∀f: A → IO O I B.
    116115  (∀v:A. e = Some A v → P_io O I ? P (f v)) →
    117   P_io O I ? P (bindIO O I A B e f).
    118 #I #O #A #B #P #e elim e; //; #v #f #H @H //;
     116  P_io O I ? P (bindIO O I A B (opt_to_io ??? m e) f).
     117#I #O #A #B #m #P #e elim e; //; #v #f #H @H //;
    119118qed.
    120119
    121 lemma opt_bindIO2_OK: ∀O,I,A,B,C. ∀P:C → Prop. ∀e:option (A×B). ∀f: A → B → IO O I C.
     120lemma opt_bindIO2_OK: ∀O,I,A,B,C,m. ∀P:C → Prop. ∀e:option (A×B). ∀f: A → B → IO O I C.
    122121  (∀vA:A.∀vB:B. e = Some (A×B) 〈vA,vB〉 → P_io O I ? P (f vA vB)) →
    123   P_io O I ? P (bindIO2 O I A B C e f).
    124 #I #O #A #B #C #P #e elim e; //; #v cases v; #vA #vB #f #H @H //;
     122  P_io O I ? P (bindIO2 O I A B C (opt_to_io ??? m e) f).
     123#I #O #A #B #C #m #P #e elim e; //; #v cases v; #vA #vB #f #H @H //;
    125124qed.
    126125
     
    185184    @ext @IH
    186185| #v @refl
    187 | @refl
     186| #m @refl
    188187] qed.
    189188
  • src/common/Identifiers.ma

    r782 r797  
    88   provide extra type checking. *)
    99
     10(* in common/PreIdentifiers.ma, via Errors.ma.
    1011inductive identifier (tag:String) : Type[0] ≝
    1112  an_identifier : Word → identifier tag.
    12  
     13*)
     14
    1315record universe (tag:String) : Type[0] ≝
    1416  { next_identifier : Word }.
     
    1719definition new_universe : ∀tag:String. universe tag ≝
    1820  λtag. mk_universe tag (zero ?).
    19  
     21
     22axiom OutOfIdentifiers : String.
     23
    2024definition fresh : ∀tag. universe tag → res (identifier tag × (universe tag)) ≝
    2125λtag,g.
    2226  let 〈gen, carries〉 ≝ add_with_carries ? (next_identifier ? g) (zero ?) true in
    23     if get_index_v ?? carries 0 ? then Error ? else
     27    if get_index_v ?? carries 0 ? then Error ? (msg OutOfIdentifiers) else
    2428      OK ? 〈an_identifier tag (next_identifier ? g), mk_universe tag gen〉.
    2529// qed.
     
    7478                                           (match m with [ an_id_map m' ⇒ m' ])).
    7579
     80axiom MissingId : String.
     81
    7682(* Only updates an existing entry; fails with an error otherwise. *)
    7783definition update : ∀tag,A. identifier_map tag A → identifier tag → A → res (identifier_map tag A) ≝
     
    7985  match update A 16 (match l with [ an_identifier l' ⇒ l' ]) a
    8086                    (match m with [ an_id_map m' ⇒ m' ]) with
    81   [ None ⇒ Error ? (* missing identifier *)
     87  [ None ⇒ Error ? ([MSG MissingId; CTX tag l]) (* missing identifier *)
    8288  | Some m' ⇒ OK ? (an_id_map tag A m')
    8389  ].
  • src/common/SmallstepExec.ma

    r751 r797  
    3737| e_stop : trace → int → mem → execution state output input
    3838| e_step : trace → state → execution state output input → execution state output input
    39 | e_wrong : execution state output input
     39| e_wrong : errmsg → execution state output input
    4040| e_interact : ∀o:output. (input o → execution state output input) → execution state output input.
    4141
     
    4949                       : execution ??? ≝
    5050match s with
    51 [ Wrong ⇒ e_wrong ???
     51[ Wrong m ⇒ e_wrong ??? m
    5252| Value v ⇒ match v with [ pair t s' ⇒
    5353    match is_final ?? exec s' with
     
    6060 e = match e with [ e_stop tr r m ⇒ e_stop ??? tr r m
    6161 | e_step tr s e ⇒ e_step ??? tr s e
    62  | e_wrong ⇒ e_wrong ??? | e_interact o k ⇒ e_interact ??? o k ].
     62 | e_wrong m ⇒ e_wrong ??? m | e_interact o k ⇒ e_interact ??? o k ].
    6363#o #i #s #e cases e; //; qed.
    6464
    6565axiom exec_inf_aux_unfold: ∀o,i,exec,ge,s. exec_inf_aux o i exec ge s =
    6666match s with
    67 [ Wrong ⇒ e_wrong ???
     67[ Wrong m ⇒ e_wrong ??? m
    6868| Value v ⇒ match v with [ pair t s' ⇒
    6969    match is_final ?? exec s' with
     
    9191  match make_initial_state ?? fx p with
    9292  [ OK gs ⇒ exec_inf_aux ?? fx (\fst gs) (Value … 〈E0,\snd gs〉)
    93   | _ ⇒ e_wrong ???
     93  | Error m ⇒ e_wrong ??? m
    9494  ].
    9595
  • src/common/Values.ma

    r751 r797  
    156156
    157157notation > "vbox('do' _ ← e; break e')" with precedence 40 for @{'bind ${e} (λ_.${e'})}.
    158 
     158(*
    159159let rec assert_nat_eq (m,n:nat) : res (m = n) ≝
    160160match m return λx.res (x = n) with
     
    212212].
    213213   
    214 
     214*)
    215215(*
    216216(** The module [Val] defines a number of arithmetic and logical operations
     
    266266      ∀r. bool_of_val (Vnull r) true.
    267267
     268axiom ValueNotABoolean : String.
     269
    268270definition eval_bool_of_val : val → res bool ≝
    269271λv. match v with
     
    271273| Vnull _ ⇒ OK ? false
    272274| Vptr _ _ _ _ ⇒ OK ? true
    273 | _ ⇒ Error ?
     275| _ ⇒ Error ? (msg ValueNotABoolean)
    274276].
    275277
Note: See TracChangeset for help on using the changeset viewer.