Changeset 797 for src/common/IO.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/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;
Note: See TracChangeset for help on using the changeset viewer.