X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2Fcontribs%2Fng_assembly%2Ffreescale%2Fmemory_bits.ma;h=93dcfa53f7f0fa5ff44e14b8eff618044ee71e6f;hb=dc7e826399162e2fde3ddf1f02d5530d6cd11205;hp=2b0b736245ce7c4990a8a462e0c2a541a7627704;hpb=9f580d9bf8f6ba6950b252f587166e95bc8fb1a8;p=helm.git diff --git a/helm/software/matita/contribs/ng_assembly/freescale/memory_bits.ma b/helm/software/matita/contribs/ng_assembly/freescale/memory_bits.ma index 2b0b73624..93dcfa53f 100755 --- a/helm/software/matita/contribs/ng_assembly/freescale/memory_bits.ma +++ b/helm/software/matita/contribs/ng_assembly/freescale/memory_bits.ma @@ -13,15 +13,11 @@ (**************************************************************************) (* ********************************************************************** *) -(* Progetto FreeScale *) +(* Progetto FreeScale *) (* *) -(* Sviluppato da: *) -(* Cosimo Oliboni, oliboni@cs.unibo.it *) +(* Sviluppato da: Ing. Cosimo Oliboni, oliboni@cs.unibo.it *) +(* Ultima modifica: 05/08/2009 *) (* *) -(* Questo materiale fa parte della tesi: *) -(* "Formalizzazione Interattiva dei Microcontroller a 8bit FreeScale" *) -(* *) -(* data ultima modifica 15/11/2007 *) (* ********************************************************************** *) include "freescale/memory_trees.ma". @@ -153,14 +149,14 @@ let newbit7 ≝ match getn_array8T o7 memory_type chk with [ MEM_READ_ONLY ⇒ Some bool (getn_array8T o7 bool old_value) | MEM_READ_WRITE ⇒ Some bool (getn_array8T o7 bool new_value) | MEM_OUT_OF_BOUND ⇒ None bool ] in - opt_map ?? newbit0 - (λnb0.opt_map ?? newbit1 - (λnb1.opt_map ?? newbit2 - (λnb2.opt_map ?? newbit3 - (λnb3.opt_map ?? newbit4 - (λnb4.opt_map ?? newbit5 - (λnb5.opt_map ?? newbit6 - (λnb6.opt_map ?? newbit7 + opt_map … newbit0 + (λnb0.opt_map … newbit1 + (λnb1.opt_map … newbit2 + (λnb2.opt_map … newbit3 + (λnb3.opt_map … newbit4 + (λnb4.opt_map … newbit5 + (λnb5.opt_map … newbit6 + (λnb6.opt_map … newbit7 (λnb7.Some ? (mt_update (Array8T bool) mem addr (array_8T bool nb7 nb6 nb5 nb4 nb3 nb2 nb1 nb0)))))))))). (* leggi controllando il tipo di memoria *) @@ -203,14 +199,14 @@ let newbit7 ≝ match getn_array8T o7 memory_type bit_types with [ MEM_READ_ONLY ⇒ Some bool (getn_array8T o7 bool value) | MEM_READ_WRITE ⇒ Some bool (getn_array8T o7 bool value) | MEM_OUT_OF_BOUND ⇒ None bool ] in - opt_map ?? newbit0 - (λnb0.opt_map ?? newbit1 - (λnb1.opt_map ?? newbit2 - (λnb2.opt_map ?? newbit3 - (λnb3.opt_map ?? newbit4 - (λnb4.opt_map ?? newbit5 - (λnb5.opt_map ?? newbit6 - (λnb6.opt_map ?? newbit7 + opt_map … newbit0 + (λnb0.opt_map … newbit1 + (λnb1.opt_map … newbit2 + (λnb2.opt_map … newbit3 + (λnb3.opt_map … newbit4 + (λnb4.opt_map … newbit5 + (λnb5.opt_map … newbit6 + (λnb6.opt_map … newbit7 (λnb7.Some ? (byte8_of_bits (array_8T bool nb7 nb6 nb5 nb4 nb3 nb2 nb1 nb0)))))))))). (* ************************** *)