Changeset 2516 for src/ASM/Fetch.ma


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

    r2498 r2516  
    3939definition label_map ≝ identifier_map ASMTag ℕ.
    4040
    41 definition costlabel_map ≝ BitVectorTrie costlabel 16. 
    42 
    4341(* The function that creates the label-to-address map *)
    4442definition create_label_cost_map0: ∀program:list labelled_instruction.
    45   (Σlabels_costs:label_map × costlabel_map. (* Both on ppcs *)
     43  (Σlabels_costs:label_map × (BitVectorTrie costlabel 16). (* Both on ppcs *)
    4644    let labels ≝ \fst labels_costs in
    4745    (∀l.occurs_exactly_once ?? l program →
     
    5250  λprogram.
    5351  \fst (pi1 ?? (foldl_strong (option Identifier × pseudo_instruction)
    54   (λprefix.Σlabels_costs_ppc:label_map × costlabel_map × ℕ.
     52  (λprefix.Σlabels_costs_ppc:label_map × (BitVectorTrie costlabel 16) × ℕ.
    5553    let 〈labels,costs,ppc〉 ≝ labels_costs_ppc in
    5654    ppc = |prefix| ∧
     
    109107(* The function that creates the label-to-address map *)
    110108definition create_label_cost_map: ∀program:list labelled_instruction.
    111   label_map × costlabel_map
     109  label_map × (BitVectorTrie costlabel 16)
    112110    λprogram.
    113111      pi1 … (create_label_cost_map0 program).
     
    169167(***** Object-code *******)
    170168
    171 definition object_code ≝ list Byte.
    172 
    173169definition bitvector_max_nat ≝
    174170  λlength: nat.
     
    186182
    187183definition load_code_memory0:
    188  ∀program: object_code. Σres: BitVectorTrie Byte 16.
     184 ∀program: list Byte. Σres: BitVectorTrie Byte 16.
    189185  let program_size ≝ |program| in
    190186   program_size ≤ 2^16 →
     
    224220qed.
    225221
    226 definition load_code_memory: object_code → BitVectorTrie Byte 16 ≝
     222definition load_code_memory: list Byte → BitVectorTrie Byte 16 ≝
    227223 λprogram.load_code_memory0 program.
    228224
    229225lemma load_code_memory_ok:
    230  ∀program: object_code.
     226 ∀program: list Byte.
    231227  let program_size ≝ |program| in
    232228   program_size ≤ 2^16 →
Note: See TracChangeset for help on using the changeset viewer.