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/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  ].
Note: See TracChangeset for help on using the changeset viewer.