Changeset 738 for src

Timestamp:

Apr 4, 2011, 5:13:10 PM (10 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:

• Clight/AST.ma (modified) (1 diff)
• RTLabs/RTLabs-syntax.ma (modified) (1 diff)
• RTLabs/import.ma (modified) (3 diffs)
• common/CostLabel.ma (modified) (1 diff)
• common/Graphs.ma (modified) (1 diff)
• common/Identifiers.ma (modified) (3 diffs)
• common/Registers.ma (modified) (1 diff)

src/Clight/AST.ma

@@ -32 +32 @@
 axiom SymbolTag : String.
 
-definition ident ≝ Identifier SymbolTag.
+definition ident ≝ identifier SymbolTag.
 
 definition ident_eq : ∀x,y:ident. (x=y) + (x≠y) ≝ identifier_eq ?.

src/RTLabs/RTLabs-syntax.ma

@@ -59 +59 @@
 
 record internal_function : Type[0] ≝
-{ f_labgen    : Universe LabelTag
-; f_reggen    : Universe RegisterTag
+{ f_labgen    : universe LabelTag
+; f_reggen    : universe RegisterTag
 ; f_sig       : signature
 ; f_result    : registers

src/RTLabs/import.ma

@@ -2 +2 @@
 include "RTLabs/RTLabs-sem.ma".
 
-let rec n_idents (n:nat) (tag:String) (g:Universe tag) : res (Vector (Identifier tag) n × (Universe tag)) ≝
+let rec n_idents (n:nat) (tag:String) (g:universe tag) : res (Vector (identifier tag) n × (universe tag)) ≝
 match n with
 [ O ⇒ OK ? 〈[[ ]], g〉
@@ -29 +29 @@
 
 definition make_registers : 
-  (nat → option register) → pre_registers → Universe RegisterTag →
-  res ((nat → option register) × (Universe RegisterTag) × registers) ≝
+  (nat → option register) → pre_registers → universe RegisterTag →
+  res ((nat → option register) × (universe RegisterTag) × registers) ≝
 λm,rs0,g.
 match rs0 with [ dp n rs ⇒
@@ -46 +46 @@
 
 definition make_registers_list :
-  (nat → option register) → list pre_registers → Universe RegisterTag →
-  res ((nat → option register) × (Universe RegisterTag) × (list registers)) ≝
+  (nat → option register) → list pre_registers → universe RegisterTag →
+  res ((nat → option register) × (universe RegisterTag) × (list registers)) ≝
 λm,lrs,g.
 foldr ?? (λrs,acc. do 〈acc',l〉 ← acc;

src/common/CostLabel.ma

@@ -3 +3 @@
 axiom CostTag : String.
 
-definition costlabel ≝ Identifier CostTag.
+definition costlabel ≝ identifier CostTag.
 
 (* For use in importing programs in intermediate languages. *)

src/common/Graphs.ma

@@ -6 +6 @@
 axiom LabelTag : String.
 
-definition label ≝ Identifier LabelTag.
+definition label ≝ identifier LabelTag.
 
 definition label_eq : ∀x,y:label. (x=y) + (x≠y) ≝ identifier_eq ?.
 
 
-definition graph : Type[0] → Type[0] ≝ IdentifierMap LabelTag.
+definition graph : Type[0] → Type[0] ≝ identifier_map LabelTag.

src/common/Identifiers.ma

@@ -5 +5 @@
 include "common/Errors.ma".
 
-(* Identifiers and their generators are tagged to differentiate them, and to
+(* identifiers and their generators are tagged to differentiate them, and to
    provide extra type checking. *)
 
-inductive Identifier (tag:String) : Type[0] ≝
-  an_identifier : Word → Identifier tag.
+inductive identifier (tag:String) : Type[0] ≝
+  an_identifier : Word → identifier tag.
   
-record Universe (tag:String) : Type[0] ≝
+record universe (tag:String) : Type[0] ≝
   { next_identifier : Word }.
 
 
-definition new_universe : ∀tag:String. Universe tag ≝
-  λtag. mk_Universe tag (zero ?).
+definition new_universe : ∀tag:String. universe tag ≝
+  λtag. mk_universe tag (zero ?).
   
-definition fresh : ∀tag. Universe tag → res (Identifier tag × (Universe tag)) ≝
+definition fresh : ∀tag. universe tag → res (identifier tag × (universe tag)) ≝
 λtag,g.
   let 〈gen, carries〉 ≝ add_with_carries ? (next_identifier ? g) (zero ?) true in
     if get_index_v ?? carries 0 ? then Error ? else
-      OK ? 〈an_identifier tag (next_identifier ? g), mk_Universe tag gen〉.
+      OK ? 〈an_identifier tag (next_identifier ? g), mk_universe tag gen〉.
 // qed.
 
-definition identifier_eq : ∀tag:String. ∀x,y:Identifier tag. (x=y) + (x≠y).
+definition identifier_eq : ∀tag:String. ∀x,y:identifier tag. (x=y) + (x≠y).
 #tag * #x * #y lapply (refl ? (eq_bv ? x y)) cases (eq_bv ? x y) in ⊢ (???% → %)
 #E [ % | %2 ]
@@ -32 +32 @@
 qed.
 
-definition identifier_of_nat : ∀tag:String. nat → Identifier tag ≝
+definition identifier_of_nat : ∀tag:String. nat → identifier tag ≝
   λtag,n. an_identifier tag (bitvector_of_nat ? n).
 
@@ -40 +40 @@
 include "ASM/BitVectorTrie.ma".
 
-inductive IdentifierMap (tag:String) (A:Type[0]) : Type[0] ≝ an_id_map : BitVectorTrie A 16 → IdentifierMap tag A.
-definition empty_map : ∀tag:String. ∀A. IdentifierMap tag A ≝
+inductive identifier_map (tag:String) (A:Type[0]) : Type[0] ≝ an_id_map : BitVectorTrie A 16 → identifier_map tag A.
+definition empty_map : ∀tag:String. ∀A. identifier_map tag A ≝
   λtag,A. an_id_map tag A (Stub A 16).
 
-definition lookup : ∀tag,A. IdentifierMap tag A → Identifier tag → option A ≝
+definition lookup : ∀tag,A. identifier_map tag A → identifier tag → option A ≝
   λtag,A,m,l. lookup_opt A 16 (match l with [ an_identifier l' ⇒ l' ])
                               (match m with [ an_id_map m' ⇒ m' ]).
 
-definition add : ∀tag,A. IdentifierMap tag A → Identifier tag → A → IdentifierMap tag A ≝
+definition add : ∀tag,A. identifier_map tag A → identifier tag → A → identifier_map tag A ≝
 λtag,A,m,l,a. an_id_map tag A (insert A 16 (match l with [ an_identifier l' ⇒ l' ]) a
                                            (match m with [ an_id_map m' ⇒ m' ])).

src/common/Registers.ma

@@ -9 +9 @@
 axiom RegisterTag : String.
 
-definition register ≝ Identifier RegisterTag.
+definition register ≝ identifier RegisterTag.
 
 definition register_eq : ∀x,y:register. (x=y) + (x≠y) ≝ identifier_eq ?.
 
-definition register_env ≝ IdentifierMap RegisterTag.
+definition register_env ≝ identifier_map RegisterTag.