Changeset 797 for src/common/Errors.ma


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.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • 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.
Note: See TracChangeset for help on using the changeset viewer.