Changeset 738


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.

Location:
src
Files:
7 edited

Legend:

Unmodified
Added
Removed
  • src/Clight/AST.ma

    r737 r738  
    3232axiom SymbolTag : String.
    3333
    34 definition ident ≝ Identifier SymbolTag.
     34definition ident ≝ identifier SymbolTag.
    3535
    3636definition ident_eq : ∀x,y:ident. (x=y) + (x≠y) ≝ identifier_eq ?.
  • src/RTLabs/RTLabs-syntax.ma

    r736 r738  
    5959
    6060record internal_function : Type[0] ≝
    61 { f_labgen    : Universe LabelTag
    62 ; f_reggen    : Universe RegisterTag
     61{ f_labgen    : universe LabelTag
     62; f_reggen    : universe RegisterTag
    6363; f_sig       : signature
    6464; f_result    : registers
  • src/RTLabs/import.ma

    r736 r738  
    22include "RTLabs/RTLabs-sem.ma".
    33
    4 let rec n_idents (n:nat) (tag:String) (g:Universe tag) : res (Vector (Identifier tag) n × (Universe tag)) ≝
     4let rec n_idents (n:nat) (tag:String) (g:universe tag) : res (Vector (identifier tag) n × (universe tag)) ≝
    55match n with
    66[ O ⇒ OK ? 〈[[ ]], g〉
     
    2929
    3030definition make_registers :
    31   (nat → option register) → pre_registers → Universe RegisterTag →
    32   res ((nat → option register) × (Universe RegisterTag) × registers) ≝
     31  (nat → option register) → pre_registers → universe RegisterTag →
     32  res ((nat → option register) × (universe RegisterTag) × registers) ≝
    3333λm,rs0,g.
    3434match rs0 with [ dp n rs ⇒
     
    4646
    4747definition make_registers_list :
    48   (nat → option register) → list pre_registers → Universe RegisterTag →
    49   res ((nat → option register) × (Universe RegisterTag) × (list registers)) ≝
     48  (nat → option register) → list pre_registers → universe RegisterTag →
     49  res ((nat → option register) × (universe RegisterTag) × (list registers)) ≝
    5050λm,lrs,g.
    5151foldr ?? (λrs,acc. do 〈acc',l〉 ← acc;
  • src/common/CostLabel.ma

    r737 r738  
    33axiom CostTag : String.
    44
    5 definition costlabel ≝ Identifier CostTag.
     5definition costlabel ≝ identifier CostTag.
    66
    77(* For use in importing programs in intermediate languages. *)
  • src/common/Graphs.ma

    r736 r738  
    66axiom LabelTag : String.
    77
    8 definition label ≝ Identifier LabelTag.
     8definition label ≝ identifier LabelTag.
    99
    1010definition label_eq : ∀x,y:label. (x=y) + (x≠y) ≝ identifier_eq ?.
    1111
    1212
    13 definition graph : Type[0] → Type[0] ≝ IdentifierMap LabelTag.
     13definition graph : Type[0] → Type[0] ≝ identifier_map LabelTag.
  • 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' ])).
  • src/common/Registers.ma

    r736 r738  
    99axiom RegisterTag : String.
    1010
    11 definition register ≝ Identifier RegisterTag.
     11definition register ≝ identifier RegisterTag.
    1212
    1313definition register_eq : ∀x,y:register. (x=y) + (x≠y) ≝ identifier_eq ?.
    1414
    15 definition register_env ≝ IdentifierMap RegisterTag.
     15definition register_env ≝ identifier_map RegisterTag.
Note: See TracChangeset for help on using the changeset viewer.