Ignore:
Timestamp:
Nov 27, 2012, 6:01:50 PM (7 years ago)
Author:
mckinna
Message:

Refactor:
Typedefs object_code and costlabel_map lifted out from ASMCostsSplit.ma
Dependencies simplified.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/ASM/ASMCostsSplit.ma

    r2475 r2498  
    55
    66let rec traverse_code_internal
    7   (code_memory: BitVectorTrie Byte 16) (cost_labels: BitVectorTrie costlabel 16)
     7  (code_memory: BitVectorTrie Byte 16) (cost_labels: costlabel_map)
    88    (program_counter: Word) (program_size: nat)
    99      (program_size_invariant: program_size = 0 ∨ nat_of_bitvector … program_counter + program_size = 2^16)
     
    279279definition traverse_code:
    280280  ∀code_memory: BitVectorTrie Byte 16.
    281   ∀cost_labels: BitVectorTrie costlabel 16.
     281  ∀cost_labels: costlabel_map.
    282282  ∀cost_labels_injective:
    283283    ∀pc, pc',l.
     
    289289          pi1 … (block_cost code_memory pc cost_labels) = lookup_present … k_pres) ≝
    290290  λcode_memory: BitVectorTrie Byte 16.
    291   λcost_labels: BitVectorTrie costlabel 16.
     291  λcost_labels: costlabel_map.
    292292  λcost_labels_injective.
    293293    pi1 ? ? (traverse_code_internal code_memory cost_labels (zero …) (2^16) ?).
     
    318318definition compute_costs ≝
    319319  λprogram: list Byte.
    320   λcost_labels: BitVectorTrie costlabel 16.
     320  λcost_labels: costlabel_map.
    321321  λcost_labels_injective:
    322322    ∀pc, pc',l.
     
    327327      traverse_code code_memory cost_labels cost_labels_injective.
    328328
    329 definition object_code ≝ list Byte.
    330 definition costlabel_map ≝ BitVectorTrie costlabel 16.     
     329(* definition object_code ≝ list Byte. *)
    331330
     331(* use of this defn in ASM/CostsProof.ma is ill-typed *)
    332332definition ASM_cost_map :
    333333  ∀p.let code_memory ≝ load_code_memory (\fst p) in
Note: See TracChangeset for help on using the changeset viewer.