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

Commit to restore deleted file.

File:
1 edited

Legend:

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

    r317 r329  
    9898 
    9999  p1_latch: Byte;
    100   p3_latch: Byte
     100  p3_latch: Byte;
     101 
     102  clock: Time
    101103}.
    102104
     
    108110  ∀i: SFR8052.
    109111    sfr_8052_index i < five.
     112   
     113ndefinition set_clock ≝
     114  λs: Status.
     115  λt: Time.
     116    let old_code_memory ≝ code_memory s in
     117    let old_low_internal_ram ≝ low_internal_ram s in
     118    let old_high_internal_ram ≝ high_internal_ram s in
     119    let old_external_ram ≝ external_ram s in
     120    let old_program_counter ≝ program_counter s in
     121    let old_special_function_registers_8051 ≝ special_function_registers_8051 s in
     122    let old_special_function_registers_8052 ≝ special_function_registers_8052 s in
     123    let old_p1_latch ≝ p1_latch s in   
     124    let old_p3_latch ≝ p3_latch s in
     125      mk_Status old_code_memory
     126                old_low_internal_ram
     127                old_high_internal_ram
     128                old_external_ram
     129                old_program_counter
     130                old_special_function_registers_8051
     131                old_special_function_registers_8052
     132                old_p1_latch
     133                old_p3_latch
     134                t.
    110135   
    111136ndefinition set_p1_latch ≝
     
    120145    let old_special_function_registers_8052 ≝ special_function_registers_8052 s in
    121146    let old_p3_latch ≝ p3_latch s in
     147    let old_clock ≝ clock s in
    122148      mk_Status old_code_memory
    123149                old_low_internal_ram
     
    128154                old_special_function_registers_8052
    129155                b
    130                 old_p3_latch.
     156                old_p3_latch
     157                old_clock.
    131158
    132159ndefinition set_p3_latch ≝
     
    141168    let old_special_function_registers_8052 ≝ special_function_registers_8052 s in
    142169    let old_p1_latch ≝ p1_latch s in
     170    let old_clock ≝ clock s in
    143171      mk_Status old_code_memory
    144172                old_low_internal_ram
     
    149177                old_special_function_registers_8052
    150178                old_p1_latch
    151                 b.
     179                b
     180                old_clock.
    152181
    153182ndefinition get_8051_sfr ≝
     
    185214    let old_p1_latch ≝ p1_latch s in
    186215    let old_p3_latch ≝ p3_latch s in
     216    let old_clock ≝ clock s in
    187217      mk_Status old_code_memory
    188218                old_low_internal_ram
     
    193223                old_special_function_registers_8052
    194224                old_p1_latch
    195                 old_p3_latch.
     225                old_p3_latch
     226                old_clock.
    196227    napply (sfr8051_index_nineteen i).
    197228nqed.
     
    213244    let old_p1_latch ≝ p1_latch s in
    214245    let old_p3_latch ≝ p3_latch s in
     246    let old_clock ≝ clock s in
    215247      mk_Status old_code_memory
    216248                old_low_internal_ram
     
    221253                new_special_function_registers_8052
    222254                old_p1_latch
    223                 old_p3_latch.
     255                old_p3_latch
     256                old_clock.
    224257    napply (sfr8052_index_five i).
    225258nqed.
     
    236269    let old_p1_latch ≝ p1_latch s in
    237270    let old_p3_latch ≝ p3_latch s in
     271    let old_clock ≝ clock s in
    238272      mk_Status old_code_memory
    239273                old_low_internal_ram
     
    244278                old_special_function_registers_8052
    245279                old_p1_latch
    246                 old_p3_latch.
     280                old_p3_latch
     281                old_clock.
    247282               
    248283ndefinition set_code_memory ≝
     
    257292    let old_p1_latch ≝ p1_latch s in
    258293    let old_p3_latch ≝ p3_latch s in
     294    let old_clock ≝ clock s in
    259295      mk_Status r
    260296                old_low_internal_ram
     
    265301                old_special_function_registers_8052
    266302                old_p1_latch
    267                 old_p3_latch.
     303                old_p3_latch
     304                old_clock.
    268305               
    269306ndefinition set_low_internal_ram ≝
     
    278315    let old_p1_latch ≝ p1_latch s in
    279316    let old_p3_latch ≝ p3_latch s in
     317    let old_clock ≝ clock s in
    280318      mk_Status old_code_memory
    281319                r
     
    286324                old_special_function_registers_8052
    287325                old_p1_latch
    288                 old_p3_latch.
     326                old_p3_latch
     327                old_clock.
    289328               
    290329ndefinition set_high_internal_ram ≝
     
    300339    let old_p1_latch ≝ p1_latch s in
    301340    let old_p3_latch ≝ p3_latch s in
     341    let old_clock ≝ clock s in
    302342      mk_Status old_code_memory
    303343                old_low_internal_ram
     
    308348                old_special_function_registers_8052
    309349                old_p1_latch
    310                 old_p3_latch.
     350                old_p3_latch
     351                old_clock.
    311352               
    312353ndefinition set_external_ram ≝
     
    321362    let old_p1_latch ≝ p1_latch s in
    322363    let old_p3_latch ≝ p3_latch s in
     364    let old_clock ≝ clock s in
    323365      mk_Status old_code_memory
    324366                old_low_internal_ram
     
    329371                old_special_function_registers_8052
    330372                old_p1_latch
    331                 old_p3_latch.
     373                old_p3_latch
     374                old_clock.
    332375               
    333376naxiom less_than_or_equal_monotone:
     
    467510                         (replicate Byte five (zero eight))     (* 8052 SFR. *)
    468511                         (zero eight)                           (* P1 latch. *)
    469                          (zero eight) in                        (* P3 latch. *)
    470   set_program_counter status (bitvector_of_nat sixteen seven).
     512                         (zero eight)                           (* P3 latch. *)
     513                         Z                                      (* Clock.    *)
     514  in
     515    set_program_counter status (bitvector_of_nat sixteen seven).
    471516 
    472517naxiom not_implemented: False.
     
    650695      set_low_internal_ram s new_low_internal_ram.
    651696     
     697alias id "get_index" = "cic:/matita/ng/BitVector/get_index.def(3)".
    652698ndefinition read_at_stack_pointer ≝
    653699  λs: Status.
Note: See TracChangeset for help on using the changeset viewer.