Changeset 797 for src/Clight/Csyntax.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/Clight/Csyntax.ma

    r747 r797  
    517517Open Local Scope string_scope.
    518518*)
     519axiom UnknownField : String.
     520
    519521let rec field_offset_rec (id: ident) (fld: fieldlist) (pos: nat)
    520522                              on fld : res nat ≝
    521523  match fld with
    522   [ Fnil ⇒ Error ? (*MSG "Unknown field " :: CTX id :: nil*)
     524  [ Fnil ⇒ Error ? [MSG UnknownField (*"Unknown field "*); CTX ? id]
    523525  | Fcons id' t fld' ⇒
    524526      match ident_eq id id' with
     
    533535let rec field_type (id: ident) (fld: fieldlist) on fld : res type :=
    534536  match fld with
    535   [ Fnil ⇒ Error ? (*MSG "Unknown field " :: CTX id :: nil*)
     537  [ Fnil ⇒ Error ? [MSG UnknownField (*"Unknown field "*); CTX ? id]
    536538  | Fcons id' t fld' ⇒ match ident_eq id id' with [ inl _ ⇒ OK ? t | inr _ ⇒ field_type id fld']
    537539  ].
Note: See TracChangeset for help on using the changeset viewer.