Changeset 2516 for src/ASM/ASMCostsSplit.ma

Timestamp:

Dec 2, 2012, 5:45:36 PM (8 years ago)

Author:

mckinna

Message:

removed typedefs; restored older versions; moved typedefs to compiler.ma
AssemblyProofSplit? *still* doesn't typecheck: disambiguation errors!

File:

• src/ASM/ASMCostsSplit.ma (modified) (5 diffs)

src/ASM/ASMCostsSplit.ma

@@ -5 +5 @@
 
 let rec traverse_code_internal
-  (code_memory: BitVectorTrie Byte 16) (cost_labels: costlabel_map)
+  (code_memory: BitVectorTrie Byte 16) (cost_labels: BitVectorTrie costlabel 16)
     (program_counter: Word) (program_size: nat)
       (program_size_invariant: program_size = 0 ∨ nat_of_bitvector … program_counter + program_size = 2^16)
@@ -279 +279 @@
 definition traverse_code:
   ∀code_memory: BitVectorTrie Byte 16.
-  ∀cost_labels: costlabel_map.
+  ∀cost_labels: BitVectorTrie costlabel 16.
   ∀cost_labels_injective:
     ∀pc, pc',l.
@@ -289 +289 @@
           pi1 … (block_cost code_memory pc cost_labels) = lookup_present … k_pres) ≝
   λcode_memory: BitVectorTrie Byte 16.
-  λcost_labels: costlabel_map.
+  λcost_labels: BitVectorTrie costlabel 16.
   λcost_labels_injective.
     pi1 ? ? (traverse_code_internal code_memory cost_labels (zero …) (2^16) ?).
@@ -318 +318 @@
 definition compute_costs ≝
   λprogram: list Byte.
-  λcost_labels: costlabel_map.
+  λcost_labels: BitVectorTrie costlabel 16.
   λcost_labels_injective:
     ∀pc, pc',l.
@@ -327 +327 @@
       traverse_code code_memory cost_labels cost_labels_injective.
 
-(* JHM: moved to Fetch.ma *)
-(* definition object_code ≝ list Byte. *)
-(* definition costlabel_map ≝ BitVectorTrie costlabel 16.   *)
-
 (* use of this defn in ASM/CostsProof.ma is ill-typed *)
 definition ASM_cost_map :
-  ∀p: object_code × costlabel_map.
+  ∀p: (list Byte) × (BitVectorTrie costlabel 16).
   let code_memory ≝ load_code_memory (\fst p) in
   let a_s ≝ ASM_abstract_status code_memory (\snd p) in