Ignore:
Timestamp:
Nov 29, 2010, 1:42:00 PM (9 years ago)
Author:
mulligan
Message:

Commit to restore deleted file.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • Deliverables/D4.1/Matita/Interpret.ma

    r328 r329  
     1include "Status.ma".
     2include "Fetch.ma".
     3include "Cartesian.ma".
     4include "Arithmetic.ma".
     5include "List.ma".
     6
     7ndefinition execute_1: Status → Status ≝
     8  λs.
     9    let 〈 instr_pc, ticks 〉 ≝ fetch (code_memory s) (program_counter s) in
     10    let 〈 instr, pc 〉 ≝ 〈 first … instr_pc, second … instr_pc 〉 in
     11    let s ≝ set_clock s (clock s + ticks) in
     12    let s ≝ set_program_counter s pc in
     13    let s ≝
     14      match instr with
     15        [ ADD addr1 addr2 ⇒
     16            match addr1 return λx. bool_to_Prop (is_in … [[ acc_a ]] x) → ? with
     17              [ ACC_A ⇒ λacc_a: True.
     18                match addr2 return λx. bool_to_Prop (is_in … [[ register;
     19                                                                direct;
     20                                                                indirect;
     21                                                                data ]] x) → ? with
     22                  [ REGISTER r ⇒ λregister: True.
     23                    let 〈result, flags〉 ≝ add_8_with_carry (get_arg_8 s false ACC_A)
     24                                                           (get_arg_8 s false (REGISTER r)) false in
     25                    let cy_flag ≝ get_index ? flags Z in
     26                    let ac_flag ≝ get_index ? flags one in
     27                    let ov_flag ≝ get_index ? flags two in
     28                    let s ≝ set_arg_8 s ACC_A result in
     29                      set_flags s cy_flag (Just? ac_flag) ov_flag
     30                  | DIRECT d ⇒ λdirect: True. ?
     31                  | INDIRECT i ⇒ λindirect: True. ?
     32                  | DATA d ⇒ λdata: True. ?
     33                  | _ ⇒ λother: False. ?
     34                  ] (subaddressing_modein … addr2)
     35            | _ ⇒ λother: False. ?
     36            ] (subaddressing_modein … addr1)
     37        | _ ⇒ s
     38        ]
     39    in
     40      s.
     41   
     42   
Note: See TracChangeset for help on using the changeset viewer.