Changeset 329 for Deliverables/D4.1/Matita/Status.ma

Timestamp:

Nov 29, 2010, 1:42:00 PM (10 years ago)

Author:

mulligan

Message:

Commit to restore deleted file.

File:

• Deliverables/D4.1/Matita/Status.ma (modified) (22 diffs)

Deliverables/D4.1/Matita/Status.ma

@@ -98 +98 @@
   
   p1_latch: Byte;
-  p3_latch: Byte
+  p3_latch: Byte;
+  
+  clock: Time
 }.
 
@@ -108 +110 @@
   ∀i: SFR8052.
     sfr_8052_index i < five.
+    
+ndefinition set_clock ≝ 
+  λs: Status.
+  λt: Time.
+    let old_code_memory ≝ code_memory s in
+    let old_low_internal_ram ≝ low_internal_ram s in
+    let old_high_internal_ram ≝ high_internal_ram s in
+    let old_external_ram ≝ external_ram s in
+    let old_program_counter ≝ program_counter s in
+    let old_special_function_registers_8051 ≝ special_function_registers_8051 s in
+    let old_special_function_registers_8052 ≝ special_function_registers_8052 s in
+    let old_p1_latch ≝ p1_latch s in    
+    let old_p3_latch ≝ p3_latch s in
+      mk_Status old_code_memory
+                old_low_internal_ram
+                old_high_internal_ram
+                old_external_ram
+                old_program_counter
+                old_special_function_registers_8051
+                old_special_function_registers_8052
+                old_p1_latch
+                old_p3_latch
+                t.
     
 ndefinition set_p1_latch ≝
@@ -120 +145 @@
     let old_special_function_registers_8052 ≝ special_function_registers_8052 s in
     let old_p3_latch ≝ p3_latch s in
+    let old_clock ≝ clock s in
       mk_Status old_code_memory
                 old_low_internal_ram
@@ -128 +154 @@
                 old_special_function_registers_8052
                 b
-                old_p3_latch.
+                old_p3_latch
+                old_clock.
 
 ndefinition set_p3_latch ≝
@@ -141 +168 @@
     let old_special_function_registers_8052 ≝ special_function_registers_8052 s in
     let old_p1_latch ≝ p1_latch s in
+    let old_clock ≝ clock s in
       mk_Status old_code_memory
                 old_low_internal_ram
@@ -149 +177 @@
                 old_special_function_registers_8052
                 old_p1_latch
-                b.
+                b
+                old_clock.
 
 ndefinition get_8051_sfr ≝
@@ -185 +214 @@
     let old_p1_latch ≝ p1_latch s in
     let old_p3_latch ≝ p3_latch s in
+    let old_clock ≝ clock s in
       mk_Status old_code_memory
                 old_low_internal_ram
@@ -193 +223 @@
                 old_special_function_registers_8052
                 old_p1_latch
-                old_p3_latch.
+                old_p3_latch
+                old_clock.
     napply (sfr8051_index_nineteen i).
 nqed.
@@ -213 +244 @@
     let old_p1_latch ≝ p1_latch s in
     let old_p3_latch ≝ p3_latch s in
+    let old_clock ≝ clock s in
       mk_Status old_code_memory
                 old_low_internal_ram
@@ -221 +253 @@
                 new_special_function_registers_8052
                 old_p1_latch
-                old_p3_latch.
+                old_p3_latch
+                old_clock.
     napply (sfr8052_index_five i).
 nqed.
@@ -236 +269 @@
     let old_p1_latch ≝ p1_latch s in
     let old_p3_latch ≝ p3_latch s in
+    let old_clock ≝ clock s in
       mk_Status old_code_memory
                 old_low_internal_ram
@@ -244 +278 @@
                 old_special_function_registers_8052
                 old_p1_latch
-                old_p3_latch.
+                old_p3_latch
+                old_clock.
                 
 ndefinition set_code_memory ≝
@@ -257 +292 @@
     let old_p1_latch ≝ p1_latch s in
     let old_p3_latch ≝ p3_latch s in
+    let old_clock ≝ clock s in
       mk_Status r
                 old_low_internal_ram
@@ -265 +301 @@
                 old_special_function_registers_8052
                 old_p1_latch
-                old_p3_latch.
+                old_p3_latch
+                old_clock.
                 
 ndefinition set_low_internal_ram ≝
@@ -278 +315 @@
     let old_p1_latch ≝ p1_latch s in
     let old_p3_latch ≝ p3_latch s in
+    let old_clock ≝ clock s in
       mk_Status old_code_memory
                 r
@@ -286 +324 @@
                 old_special_function_registers_8052
                 old_p1_latch
-                old_p3_latch.
+                old_p3_latch
+                old_clock.
                 
 ndefinition set_high_internal_ram ≝
@@ -300 +339 @@
     let old_p1_latch ≝ p1_latch s in
     let old_p3_latch ≝ p3_latch s in
+    let old_clock ≝ clock s in
       mk_Status old_code_memory
                 old_low_internal_ram
@@ -308 +348 @@
                 old_special_function_registers_8052
                 old_p1_latch
-                old_p3_latch.
+                old_p3_latch
+                old_clock.
                 
 ndefinition set_external_ram ≝
@@ -321 +362 @@
     let old_p1_latch ≝ p1_latch s in
     let old_p3_latch ≝ p3_latch s in
+    let old_clock ≝ clock s in
       mk_Status old_code_memory
                 old_low_internal_ram
@@ -329 +371 @@
                 old_special_function_registers_8052
                 old_p1_latch
-                old_p3_latch.
+                old_p3_latch
+                old_clock.
                 
 naxiom less_than_or_equal_monotone:
@@ -467 +510 @@
                          (replicate Byte five (zero eight))     (* 8052 SFR. *)
                          (zero eight)                           (* P1 latch. *)
-                         (zero eight) in                        (* P3 latch. *)
-  set_program_counter status (bitvector_of_nat sixteen seven).
+                         (zero eight)                           (* P3 latch. *)
+                         Z                                      (* Clock.    *)
+  in
+    set_program_counter status (bitvector_of_nat sixteen seven).
   
 naxiom not_implemented: False.
@@ -650 +695 @@
       set_low_internal_ram s new_low_internal_ram.
       
+alias id "get_index" = "cic:/matita/ng/BitVector/get_index.def(3)".
 ndefinition read_at_stack_pointer ≝
   λs: Status.