Changeset 2498 for src/ASM/Fetch.ma


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/Fetch.ma

    r2264 r2498  
    3939definition label_map ≝ identifier_map ASMTag ℕ.
    4040
     41definition costlabel_map ≝ BitVectorTrie costlabel 16. 
     42
    4143(* The function that creates the label-to-address map *)
    4244definition create_label_cost_map0: ∀program:list labelled_instruction.
    43   (Σlabels_costs:label_map × (BitVectorTrie costlabel 16). (* Both on ppcs *)
     45  (Σlabels_costs:label_map × costlabel_map. (* Both on ppcs *)
    4446    let labels ≝ \fst labels_costs in
    4547    (∀l.occurs_exactly_once ?? l program →
     
    5052  λprogram.
    5153  \fst (pi1 ?? (foldl_strong (option Identifier × pseudo_instruction)
    52   (λprefix.Σlabels_costs_ppc:label_map × (BitVectorTrie costlabel 16) × ℕ.
     54  (λprefix.Σlabels_costs_ppc:label_map × costlabel_map × ℕ.
    5355    let 〈labels,costs,ppc〉 ≝ labels_costs_ppc in
    5456    ppc = |prefix| ∧
     
    107109(* The function that creates the label-to-address map *)
    108110definition create_label_cost_map: ∀program:list labelled_instruction.
    109   label_map × (BitVectorTrie costlabel 16)
     111  label_map × costlabel_map
    110112    λprogram.
    111113      pi1 … (create_label_cost_map0 program).
     
    167169(***** Object-code *******)
    168170
     171definition object_code ≝ list Byte.
     172
    169173definition bitvector_max_nat ≝
    170174  λlength: nat.
     
    182186
    183187definition load_code_memory0:
    184  ∀program: list Byte. Σres: BitVectorTrie Byte 16.
     188 ∀program: object_code. Σres: BitVectorTrie Byte 16.
    185189  let program_size ≝ |program| in
    186190   program_size ≤ 2^16 →
     
    220224qed.
    221225
    222 definition load_code_memory: list Byte → BitVectorTrie Byte 16 ≝
     226definition load_code_memory: object_code → BitVectorTrie Byte 16 ≝
    223227 λprogram.load_code_memory0 program.
    224228
    225229lemma load_code_memory_ok:
    226  ∀program: list Byte.
     230 ∀program: object_code.
    227231  let program_size ≝ |program| in
    228232   program_size ≤ 2^16 →
Note: See TracChangeset for help on using the changeset viewer.