Ignore:
Timestamp:
Dec 2, 2012, 5:45:36 PM (7 years ago)
Author:
mckinna
Message:

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

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/ASM/ASMCostsSplit.ma

    r2508 r2516  
    55
    66let rec traverse_code_internal
    7   (code_memory: BitVectorTrie Byte 16) (cost_labels: costlabel_map)
     7  (code_memory: BitVectorTrie Byte 16) (cost_labels: BitVectorTrie costlabel 16)
    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: costlabel_map.
     281  ∀cost_labels: BitVectorTrie costlabel 16.
    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: costlabel_map.
     291  λcost_labels: BitVectorTrie costlabel 16.
    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: costlabel_map.
     320  λcost_labels: BitVectorTrie costlabel 16.
    321321  λcost_labels_injective:
    322322    ∀pc, pc',l.
     
    327327      traverse_code code_memory cost_labels cost_labels_injective.
    328328
    329 (* JHM: moved to Fetch.ma *)
    330 (* definition object_code ≝ list Byte. *)
    331 (* definition costlabel_map ≝ BitVectorTrie costlabel 16.   *)
    332 
    333329(* use of this defn in ASM/CostsProof.ma is ill-typed *)
    334330definition ASM_cost_map :
    335   ∀p: object_code × costlabel_map.
     331  ∀p: (list Byte) × (BitVectorTrie costlabel 16).
    336332  let code_memory ≝ load_code_memory (\fst p) in
    337333  let a_s ≝ ASM_abstract_status code_memory (\snd p) in
Note: See TracChangeset for help on using the changeset viewer.