Changeset 2498 for src/ASM/Interpret2.ma


Ignore:
Timestamp:
Nov 27, 2012, 6:01:50 PM (8 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/Interpret2.ma

    r1996 r2498  
    3838
    3939(*CSC: move this definition elsewhere *)
    40 definition object_code: Type[0] ≝ list Byte × (BitVectorTrie costlabel 16).
     40definition object_code: Type[0] ≝ list Byte × costlabel_map.
    4141
    42 definition make_global: object_code → BitVectorTrie costlabel 16 ≝ \snd.
     42definition make_global: object_code → costlabel_map ≝ \snd.
    4343
    4444definition execute_1_instruction:
    45  BitVectorTrie costlabel 16 → Status → IO io_out io_in (trace × Status) ≝
     45 costlabel_map → Status → IO io_out io_in (trace × Status) ≝
    4646λcosts,s.
    4747 let 〈instr_pc,ticks〉 ≝ fetch (code_memory … s) (program_counter … s) in
     
    5151 | Some cst ⇒ ret … 〈Echarge cst, execute_1 s〉 ].
    5252
    53 axiom is_final: BitVectorTrie costlabel 16 → Status → option int.
     53axiom is_final: costlabel_map → Status → option int.
    5454
    5555definition exec: trans_system io_out io_in ≝
Note: See TracChangeset for help on using the changeset viewer.