(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
(* Interpret.ma: Operational semantics for the 8051/8052 processor.           *)
(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)

(* include "ASM.ma". *)
include "Arithmetic.ma".
include "BitVectorTrie.ma".

ninductive SFR8051: Type[0] ≝
  SFR_SP: SFR8051
| SFR_DPL: SFR8051
| SFR_DPH: SFR8051
| SFR_PCON: SFR8051
| SFR_TCON: SFR8051
| SFR_TMOD: SFR8051
| SFR_TL0: SFR8051
| SFR_TL1: SFR8051
| SFR_TH0: SFR8051
| SFR_TH1: SFR8051
| SFR_P1: SFR8051
| SFR_SCON: SFR8051
| SFR_SBUF: SFR8051
| SFR_IE: SFR8051
| SFR_P3: SFR8051
| SFR_IP: SFR8051
| SFR_PSW: SFR8051
| SFR_ACC_A: SFR8051
| SFR_ACC_B: SFR8051.

ndefinition sfr_8051_index ≝
  λs: SFR8051.
    match s with
      [ SFR_SP ⇒ Z
      | SFR_DPL ⇒ S Z
      | SFR_DPH ⇒ two
      | SFR_PCON ⇒ three
      | SFR_TCON ⇒ four
      | SFR_TMOD ⇒ five
      | SFR_TL0 ⇒ six
      | SFR_TL1 ⇒ seven
      | SFR_TH0 ⇒ eight
      | SFR_TH1 ⇒ nine
      | SFR_P1 ⇒ ten
      | SFR_SCON ⇒ eleven
      | SFR_SBUF ⇒ twelve
      | SFR_IE ⇒ thirteen
      | SFR_P3 ⇒ fourteen
      | SFR_IP ⇒ fifteen
      | SFR_PSW ⇒ sixteen
      | SFR_ACC_A ⇒ seventeen
      | SFR_ACC_B ⇒ eighteen
      ].
      
ninductive SFR8052: Type[0] ≝
   SFR_T2CON: SFR8052
|  SFR_RCAP2L: SFR8052
|  SFR_RCAP2H: SFR8052
|  SFR_TL2: SFR8052
|  SFR_TH2: SFR8052.

ndefinition sfr_8052_index ≝
  λs: SFR8052.
    match s with
      [ SFR_T2CON ⇒ Z
      | SFR_RCAP2L ⇒ S Z
      | SFR_RCAP2H ⇒ two
      | SFR_TL2 ⇒ three
      | SFR_TH2 ⇒ four 
      ].

(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
(* Processor status.                                                          *)
(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
nrecord Status: Type[0] ≝
{
  code_memory: BitVectorTrie Byte sixteen;
  low_internal_ram: BitVectorTrie Byte seven;
  high_internal_ram: BitVectorTrie Byte seven;
  external_ram: BitVectorTrie Byte sixteen;
 
  program_counter: Word;
  
  special_function_registers_8051: Vector Byte nineteen;
  special_function_registers_8052: Vector Byte five
}.

alias id "replicate" = "cic:/matita/Cerco/Vector/replicate.fix(0,1,1)".

ndefinition set_8051_sfr ≝
  λs: Status.
  λi: SFR8051.
  λb: Byte.
    let index ≝ sfr_8051_status i in
    let 

ndefinition initialise_status ≝
  let status ≝ mk_Status (Stub Byte sixteen)
                         (Stub Byte seven)
                         (Stub Byte seven)
                         (Stub Byte sixteen)
                         (zero sixteen)
                         (replicate Byte nineteen (zero eight))
                         (replicate Byte five (zero eight)) in
  status.