Changeset 1478


Ignore:
Timestamp:
Nov 1, 2011, 9:39:49 PM (8 years ago)
Author:
sacerdot
Message:

Almost completed (up to is_finals).

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/ASM/Interpret2.ma

    r1476 r1478  
    4141definition make_global: object_code → BitVectorTrie Identifier 16 ≝ \snd.
    4242
    43 axiom execute_1_instruction:
    44  BitVectorTrie Identifier 16 → Status → IO io_out io_in (trace × Status).
     43definition execute_1_instruction:
     44 BitVectorTrie Identifier 16 → Status → IO io_out io_in (trace × Status) ≝
     45λcosts,s.
     46 let 〈instr_pc,ticks〉 ≝ fetch (code_memory … s) (program_counter … s) in
     47 let 〈instr,pc〉 ≝ instr_pc in
     48 let s ≝ execute_1 s in
     49 match lookup_opt … pc costs with
     50 [ None ⇒ ret … 〈E0, s〉
     51 | Some cst ⇒ ret … 〈Echarge (an_identifier … cst), s〉 ].
    4552
    4653axiom is_final: BitVectorTrie Identifier 16 → Status → option int.
Note: See TracChangeset for help on using the changeset viewer.