Changeset 865 for src

Timestamp:

May 31, 2011, 11:45:21 AM (10 years ago)

Author:

sacerdot

Message:

Renaming.

Location:

src/ASM

Files:

• AssemblyProof.ma (modified) (3 diffs)
• Interpret.ma (modified) (2 diffs)

src/ASM/AssemblyProof.ma

@@ -362 +362 @@
  match l with
   [ nil ⇒ true
-  | cons hd tl ⇒ notb (address_of_word_labels_internal id hd) ∧ does_not_occur id tl].
+  | cons hd tl ⇒ notb (instruction_matches_identifier id hd) ∧ does_not_occur id tl].
 
 lemma does_not_occur_None:
@@ -376 +376 @@
   [ nil ⇒ false
   | cons hd tl ⇒
-     if address_of_word_labels_internal id hd then
+     if instruction_matches_identifier id hd then
       does_not_occur id tl
      else
@@ -393 +393 @@
 lemma index_of_internal_None: ∀i,id,instr_list,n.
  occurs_exactly_once id (instr_list@[〈None …,i〉]) →
-  index_of_internal ? (address_of_word_labels_internal id) instr_list n =
-   index_of_internal ? (address_of_word_labels_internal id) (instr_list@[〈None …,i〉]) n.
+  index_of_internal ? (instruction_matches_identifier id) instr_list n =
+   index_of_internal ? (instruction_matches_identifier id) (instr_list@[〈None …,i〉]) n.
  #i #id #instr_list elim instr_list
   [ #n #abs whd in abs; cases abs
   | #hd #tl #IH #n whd in ⊢ (% → ??%%); whd in ⊢ (match % with [_ ⇒ ? | _ ⇒ ?] → ?)
-    cases (address_of_word_labels_internal id hd) whd in ⊢ (match % with [_ ⇒ ? | _ ⇒ ?] → ??%%)
+    cases (instruction_matches_identifier id hd) whd in ⊢ (match % with [_ ⇒ ? | _ ⇒ ?] → ??%%)
     [ #H %
     | #H @IH whd in H; cases (occurs_exactly_once ??) in H ⊢ %

src/ASM/Interpret.ma

@@ -642 +642 @@
     index_of_internal A eq l 0.
 
-definition address_of_word_labels_internal ≝
+definition instruction_matches_identifier ≝
   λy: Identifier.
   λx: labelled_instruction.
@@ -653 +653 @@
   λcode_mem.
   λid: Identifier.
-    bitvector_of_nat 16 (index_of ? (address_of_word_labels_internal id) code_mem).
+    bitvector_of_nat 16 (index_of ? (instruction_matches_identifier id) code_mem).
 
 definition address_of_word_labels ≝