Changeset 1515 for src/ASM/Interpret2.ma


Ignore:
Timestamp:
Nov 18, 2011, 1:03:14 PM (8 years ago)
Author:
campbell
Message:

Add type of maps on positive binary numbers, and use them for identifers.

Also:

  • fix interpretation for - on positives
  • move eq_nat_dec to a more appropriate place
  • split out costs from other identifiers in ASM
  • use identifier abstractions in back-end
File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/ASM/Interpret2.ma

    r1478 r1515  
    2323 let s ≝ execute_1_pseudo_instruction ticks_of s in
    2424 match instr with
    25  [ Cost cst ⇒ ret … 〈Echarge (an_identifier … cst), s〉
     25 [ Cost cst ⇒ ret … 〈Echarge cst, s〉
    2626 | _ ⇒ ret ? 〈E0, s〉 ].
    2727
     
    3737
    3838(*CSC: move this definition elsewhere *)
    39 definition object_code: Type[0] ≝ list Byte × (BitVectorTrie Identifier 16).
     39definition object_code: Type[0] ≝ list Byte × (BitVectorTrie costlabel 16).
    4040
    41 definition make_global: object_code → BitVectorTrie Identifier 16 ≝ \snd.
     41definition make_global: object_code → BitVectorTrie costlabel 16 ≝ \snd.
    4242
    4343definition execute_1_instruction:
    44  BitVectorTrie Identifier 16 → Status → IO io_out io_in (trace × Status) ≝
     44 BitVectorTrie costlabel 16 → Status → IO io_out io_in (trace × Status) ≝
    4545λcosts,s.
    4646 let 〈instr_pc,ticks〉 ≝ fetch (code_memory … s) (program_counter … s) in
     
    4949 match lookup_opt … pc costs with
    5050 [ None ⇒ ret … 〈E0, s〉
    51  | Some cst ⇒ ret … 〈Echarge (an_identifier … cst), s〉 ].
     51 | Some cst ⇒ ret … 〈Echarge cst, s〉 ].
    5252
    53 axiom is_final: BitVectorTrie Identifier 16 → 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.