Changeset 267 for Deliverables/D4.1/Matita

Timestamp:

Nov 23, 2010, 5:42:20 PM (10 years ago)

Author:

mulligan

Message:

Renamed Interpret to Status.

File:

• Deliverables/D4.1/Matita/Status.ma (moved) (moved from Deliverables/D4.1/Matita/Interpret.ma) (2 diffs)

Deliverables/D4.1/Matita/Status.ma

@@ -85 +85 @@
 }.
 
-ncheck special_function_registers_8051.
-
 naxiom sfr8051_index_nineteen:
   ∀i: SFR8051.
@@ -218 +216 @@
                 old_special_function_registers_8052.
                 
+naxiom less_than_or_equal_monotone:
+  ∀m, n: Nat.
+    m ≤ n → S m ≤ S n.
+    
+alias id "get_index" = "cic:/matita/ng/Vector/get_index.fix(0,3,2)".
+                
 ndefinition get_cy_flag ≝
   λs: Status.
     let sfr ≝ special_function_registers_8051 s in
-    let psw ≝ get_index … (sfr_8051_index SFR_PSW) s ? in
-      get_index … Z psw ?.
+    let psw ≝ get_index Byte nineteen sfr (sfr_8051_index SFR_PSW) ? in
+      get_index Bool eight psw Z ?.
+    nnormalize.
+    napply (less_than_or_equal_monotone ? ?).
+    napply (less_than_or_equal_zero).
+    nrepeat (napply (less_than_or_equal_monotone ? ?)).
+    napply (less_than_or_equal_zero).
+nqed.
+
+ndefinition get_ac_flag ≝
+  λs: Status.
+    let sfr ≝ special_function_registers_8051 s in
+    let psw ≝ get_index Byte nineteen sfr (sfr_8051_index SFR_PSW) ? in
+      get_index Bool eight psw (S Z) ?.
+    nnormalize.
+    nrepeat (napply (less_than_or_equal_monotone ? ?)).
+    napply (less_than_or_equal_zero).
+    nrepeat (napply (less_than_or_equal_monotone ? ?)).
+    napply (less_than_or_equal_zero).
+nqed.
+
+ndefinition get_fo_flag ≝
+  λs: Status.
+    let sfr ≝ special_function_registers_8051 s in
+    let psw ≝ get_index Byte nineteen sfr (sfr_8051_index SFR_PSW) ? in
+      get_index Bool eight psw two ?.
+    nnormalize.
+    nrepeat (napply (less_than_or_equal_monotone ? ?)).
+    napply (less_than_or_equal_zero).
+    nrepeat (napply (less_than_or_equal_monotone ? ?)).
+    napply (less_than_or_equal_zero).
+nqed.
+
+ndefinition get_rs1_flag ≝
+  λs: Status.
+    let sfr ≝ special_function_registers_8051 s in
+    let psw ≝ get_index Byte nineteen sfr (sfr_8051_index SFR_PSW) ? in
+      get_index Bool eight psw three ?.
+    nnormalize.
+    nrepeat (napply (less_than_or_equal_monotone ? ?)).
+    napply (less_than_or_equal_zero).
+    nrepeat (napply (less_than_or_equal_monotone ? ?)).
+    napply (less_than_or_equal_zero).
+nqed.
+
+ndefinition get_rs0_flag ≝
+  λs: Status.
+    let sfr ≝ special_function_registers_8051 s in
+    let psw ≝ get_index Byte nineteen sfr (sfr_8051_index SFR_PSW) ? in
+      get_index Bool eight psw four ?.
+    nnormalize.
+    nrepeat (napply (less_than_or_equal_monotone ? ?)).
+    napply (less_than_or_equal_zero).
+    nrepeat (napply (less_than_or_equal_monotone ? ?)).
+    napply (less_than_or_equal_zero).
+nqed.
+
+ndefinition get_ov_flag ≝
+  λs: Status.
+    let sfr ≝ special_function_registers_8051 s in
+    let psw ≝ get_index Byte nineteen sfr (sfr_8051_index SFR_PSW) ? in
+      get_index Bool eight psw five ?.
+    nnormalize.
+    nrepeat (napply (less_than_or_equal_monotone ? ?)).
+    napply (less_than_or_equal_zero).
+    nrepeat (napply (less_than_or_equal_monotone ? ?)).
+    napply (less_than_or_equal_zero).
+nqed.
+
+ndefinition get_ud_flag ≝
+  λs: Status.
+    let sfr ≝ special_function_registers_8051 s in
+    let psw ≝ get_index Byte nineteen sfr (sfr_8051_index SFR_PSW) ? in
+      get_index Bool eight psw six ?.
+    nnormalize.
+    nrepeat (napply (less_than_or_equal_monotone ? ?)).
+    napply (less_than_or_equal_zero).
+    nrepeat (napply (less_than_or_equal_monotone ? ?)).
+    napply (less_than_or_equal_zero).
+nqed.
+
+ndefinition get_p_flag ≝
+  λs: Status.
+    let sfr ≝ special_function_registers_8051 s in
+    let psw ≝ get_index Byte nineteen sfr (sfr_8051_index SFR_PSW) ? in
+      get_index Bool eight psw seven ?.
+    nnormalize.
+    nrepeat (napply (less_than_or_equal_monotone ? ?)).
+    napply (less_than_or_equal_zero).
+    nrepeat (napply (less_than_or_equal_monotone ? ?)).
+    napply (less_than_or_equal_zero).
+nqed.
                 
 ndefinition set_high_internal_ram ≝