source: Deliverables/D4.1/Matita/Interpret.ma @ 330

include "Status.ma".
include "Fetch.ma".
include "Cartesian.ma".
include "Arithmetic.ma".
include "List.ma".

ndefinition execute_1: Status → Status ≝
  λs.
    let 〈 instr_pc, ticks 〉 ≝ fetch (code_memory s) (program_counter s) in
    let 〈 instr, pc 〉 ≝ 〈 first … instr_pc, second … instr_pc 〉 in
    let s ≝ set_clock s (clock s + ticks) in
    let s ≝ set_program_counter s pc in
    let s ≝
      match instr with
        [ ADD addr1 addr2 ⇒
            match addr1 return λx. bool_to_Prop (is_in … [[ acc_a ]] x) → ? with
              [ ACC_A ⇒ λacc_a: True.
                match addr2 return λx. bool_to_Prop (is_in … [[ register;
                                                                direct;
                                                                indirect;
                                                                data ]] x) → ? with
                  [ REGISTER r ⇒ λregister: True.
                    let 〈result, flags〉 ≝ add_8_with_carry (get_arg_8 s false ACC_A)
                                                           (get_arg_8 s false (REGISTER r)) false in
                    let cy_flag ≝ get_index ? flags Z in
                    let ac_flag ≝ get_index ? flags one in
                    let ov_flag ≝ get_index ? flags two in
                    let s ≝ set_arg_8 s ACC_A result in
                      set_flags s cy_flag (Just? ac_flag) ov_flag
                  | DIRECT d ⇒ λdirect: True. ?
                  | INDIRECT i ⇒ λindirect: True. ?
                  | DATA d ⇒ λdata: True. ?
                  | _ ⇒ λother: False. ?
                  ] (subaddressing_modein … addr2)
            | _ ⇒ λother: False. ?
            ] (subaddressing_modein … addr1)
        | _ ⇒ s
        ]
    in
      s.