Changeset 1055


Ignore:
Timestamp:
Jul 5, 2011, 12:15:12 PM (8 years ago)
Author:
mulligan
Message:

changes to how identifiers are generated

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/common/Identifiers.ma

    r1053 r1055  
    1414
    1515record universe (tag:String) : Type[0] ≝
    16   { next_identifier : Word }.
    17 
     16{
     17  next_identifier : Word;
     18  counter_overflow: bool
     19}.
    1820
    1921definition new_universe : ∀tag:String. universe tag ≝
    20   λtag. mk_universe tag (zero ?).
     22  λtag. mk_universe tag (zero ?) false.
    2123
    22 axiom OutOfIdentifiers : String.
    23 
    24 definition fresh : ∀tag. universe tag → res (identifier tag × (universe tag)) ≝
    25 λtag,g.
    26   let 〈gen, carries〉 ≝ add_with_carries ? (next_identifier ? g) (zero ?) true in
    27     if get_index_v ?? carries 0 ? then Error ? (msg OutOfIdentifiers) else
    28       OK ? 〈an_identifier tag (next_identifier ? g), mk_universe tag gen〉.
    29 // qed.
     24definition fresh ≝
     25  λtag.
     26  λuniv: universe tag.
     27  let 〈gen, carries〉 ≝ add_with_carries ? (next_identifier ? univ) (zero ?) true in
     28    if get_index_v … carries 0 ? then
     29      〈an_identifier tag (next_identifier ? univ), mk_universe tag gen true〉
     30    else
     31      〈an_identifier tag (next_identifier ? univ), mk_universe tag gen false〉.
     32  //
     33qed.
    3034
    3135definition eq_identifier ≝
Note: See TracChangeset for help on using the changeset viewer.