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

Timestamp:

Nov 25, 2010, 12:48:34 PM (10 years ago)

Author:

mulligan

Message:

Moved definitions around so related are grouped together.

File:

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

Deliverables/D4.1/Matita/Status.ma

@@ -410 +410 @@
     nrepeat (napply (less_than_or_equal_monotone ? ?)).
     napply (less_than_or_equal_zero).
+nqed.
+
+ndefinition set_flags ≝
+  λs: Status.
+  λcy: Bit.
+  λac: Maybe Bit.
+  λov: Bit.
+    let 〈 nu, nl 〉 ≝ split … four four (get_8051_sfr s SFR_PSW) in
+    let old_cy ≝ get_index … nu Z ? in
+    let old_ac ≝ get_index … nu one ? in
+    let old_fo ≝ get_index … nu two ? in
+    let old_rs1 ≝ get_index … nu three ? in
+    let old_rs0 ≝ get_index … nl Z ? in
+    let old_ov ≝ get_index … nl one ? in
+    let old_ud ≝ get_index … nl two ? in
+    let old_p ≝ get_index … nl three ? in
+    let new_ac ≝ match ac with [ Nothing ⇒ old_ac | Just j ⇒ j ] in
+    let new_psw ≝ [[ old_cy ; new_ac ; old_fo ; old_rs1 ;
+                     old_rs0 ; old_ov ; old_ud ; old_p ]] in
+      set_8051_sfr s SFR_PSW new_psw.
+    ##[##1,2,3,4,5,6,7,8:
+        nnormalize;
+        nrepeat (napply less_than_or_equal_monotone);
+        napply (less_than_or_equal_zero);
+    ##]
 nqed.
 
@@ -600 +625 @@
       set_low_internal_ram s new_low_internal_ram.
       
-ndefinition set_flags ≝
-  λs: Status.
-  λcy: Bit.
-  λac: Maybe Bit.
-  λov: Bit.
-    let 〈 nu, nl 〉 ≝ split … four four (get_8051_sfr s SFR_PSW) in
-    let old_cy ≝ get_index … nu Z ? in
-    let old_ac ≝ get_index … nu one ? in
-    let old_fo ≝ get_index … nu two ? in
-    let old_rs1 ≝ get_index … nu three ? in
-    let old_rs0 ≝ get_index … nl Z ? in
-    let old_ov ≝ get_index … nl one ? in
-    let old_ud ≝ get_index … nl two ? in
-    let old_p ≝ get_index … nl three ? in
-    let new_ac ≝ match ac with [ Nothing ⇒ old_ac | Just j ⇒ j ] in
-    let new_psw ≝ [[ old_cy ; new_ac ; old_fo ; old_rs1 ;
-                     old_rs0 ; old_ov ; old_ud ; old_p ]] in
-      set_8051_sfr s SFR_PSW new_psw.
-    ##[##1,2,3,4,5,6,7,8:
-        nnormalize;
-        nrepeat (napply less_than_or_equal_monotone);
-        napply (less_than_or_equal_zero);
-    ##]
-nqed.
-      
 ndefinition read_at_stack_pointer ≝
   λs: Status.