Ignore:
Timestamp:
Apr 4, 2011, 5:13:10 PM (9 years ago)
Author:
campbell
Message:

Use lower case names for identifiers for consistency with CompCert? derived code
and to prevent confusion with the back-end equivalents until they're all merged.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/common/Identifiers.ma

    r737 r738  
    55include "common/Errors.ma".
    66
    7 (* Identifiers and their generators are tagged to differentiate them, and to
     7(* identifiers and their generators are tagged to differentiate them, and to
    88   provide extra type checking. *)
    99
    10 inductive Identifier (tag:String) : Type[0] ≝
    11   an_identifier : Word → Identifier tag.
     10inductive identifier (tag:String) : Type[0] ≝
     11  an_identifier : Word → identifier tag.
    1212 
    13 record Universe (tag:String) : Type[0] ≝
     13record universe (tag:String) : Type[0] ≝
    1414  { next_identifier : Word }.
    1515
    1616
    17 definition new_universe : ∀tag:String. Universe tag ≝
    18   λtag. mk_Universe tag (zero ?).
     17definition new_universe : ∀tag:String. universe tag ≝
     18  λtag. mk_universe tag (zero ?).
    1919 
    20 definition fresh : ∀tag. Universe tag → res (Identifier tag × (Universe tag)) ≝
     20definition fresh : ∀tag. universe tag → res (identifier tag × (universe tag)) ≝
    2121λtag,g.
    2222  let 〈gen, carries〉 ≝ add_with_carries ? (next_identifier ? g) (zero ?) true in
    2323    if get_index_v ?? carries 0 ? then Error ? else
    24       OK ? 〈an_identifier tag (next_identifier ? g), mk_Universe tag gen〉.
     24      OK ? 〈an_identifier tag (next_identifier ? g), mk_universe tag gen〉.
    2525// qed.
    2626
    27 definition identifier_eq : ∀tag:String. ∀x,y:Identifier tag. (x=y) + (x≠y).
     27definition identifier_eq : ∀tag:String. ∀x,y:identifier tag. (x=y) + (x≠y).
    2828#tag * #x * #y lapply (refl ? (eq_bv ? x y)) cases (eq_bv ? x y) in ⊢ (???% → %)
    2929#E [ % | %2 ]
     
    3232qed.
    3333
    34 definition identifier_of_nat : ∀tag:String. nat → Identifier tag ≝
     34definition identifier_of_nat : ∀tag:String. nat → identifier tag ≝
    3535  λtag,n. an_identifier tag (bitvector_of_nat ? n).
    3636
     
    4040include "ASM/BitVectorTrie.ma".
    4141
    42 inductive IdentifierMap (tag:String) (A:Type[0]) : Type[0] ≝ an_id_map : BitVectorTrie A 16 → IdentifierMap tag A.
    43 definition empty_map : ∀tag:String. ∀A. IdentifierMap tag A ≝
     42inductive identifier_map (tag:String) (A:Type[0]) : Type[0] ≝ an_id_map : BitVectorTrie A 16 → identifier_map tag A.
     43definition empty_map : ∀tag:String. ∀A. identifier_map tag A ≝
    4444  λtag,A. an_id_map tag A (Stub A 16).
    4545
    46 definition lookup : ∀tag,A. IdentifierMap tag A → Identifier tag → option A ≝
     46definition lookup : ∀tag,A. identifier_map tag A → identifier tag → option A ≝
    4747  λtag,A,m,l. lookup_opt A 16 (match l with [ an_identifier l' ⇒ l' ])
    4848                              (match m with [ an_id_map m' ⇒ m' ]).
    4949
    50 definition add : ∀tag,A. IdentifierMap tag A → Identifier tag → A → IdentifierMap tag A ≝
     50definition add : ∀tag,A. identifier_map tag A → identifier tag → A → identifier_map tag A ≝
    5151λtag,A,m,l,a. an_id_map tag A (insert A 16 (match l with [ an_identifier l' ⇒ l' ]) a
    5252                                           (match m with [ an_id_map m' ⇒ m' ])).
Note: See TracChangeset for help on using the changeset viewer.