Changeset 2516 for src/ASM/Interpret2.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/Interpret2.ma

    r2498 r2516  
    3838
    3939(*CSC: move this definition elsewhere *)
    40 definition object_code: Type[0] ≝ list Byte × costlabel_map.
     40definition object_code: Type[0] ≝ list Byte × (BitVectorTrie costlabel 16).
    4141
    42 definition make_global: object_code → costlabel_map ≝ \snd.
     42definition make_global: object_code → BitVectorTrie costlabel 16 ≝ \snd.
    4343
    4444definition execute_1_instruction:
    45  costlabel_map → Status → IO io_out io_in (trace × Status) ≝
     45 BitVectorTrie costlabel 16 → 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: costlabel_map → Status → option int.
     53axiom is_final: BitVectorTrie costlabel 16 → Status → option int.
    5454
    5555definition exec: trans_system io_out io_in ≝
Note: See TracChangeset for help on using the changeset viewer.