From a6501e81dc2cae2025841cefd502c220e01cd5d8 Mon Sep 17 00:00:00 2001 From: Cosimo Oliboni Date: Fri, 22 Jan 2010 01:30:42 +0000 Subject: [PATCH] freescale porting --- .../matita/contribs/ng_assembly/depends | 12 +- .../ng_assembly/freescale/memory_struct.ma | 624 ----------------- .../ng_assembly/freescale/memory_trees.ma | 227 ------ .../contribs/ng_assembly/freescale/status.ma | 2 +- .../{freescale => memory}/memory_abs.ma | 116 +-- .../{freescale => memory}/memory_bits.ma | 160 ++--- .../{freescale => memory}/memory_func.ma | 36 +- .../ng_assembly/memory/memory_struct.ma | 659 ++++++++++++++++++ .../ng_assembly/memory/memory_trees.ma | 148 ++++ .../matita/contribs/ng_assembly/num/byte8.ma | 7 +- .../contribs/ng_assembly/num/exadecim.ma | 7 +- .../matita/contribs/ng_assembly/num/word16.ma | 7 +- .../matita/contribs/ng_assembly/num/word32.ma | 7 +- .../contribs/ng_assembly/universe/universe.ma | 37 +- 14 files changed, 984 insertions(+), 1065 deletions(-) delete mode 100755 helm/software/matita/contribs/ng_assembly/freescale/memory_struct.ma delete mode 100755 helm/software/matita/contribs/ng_assembly/freescale/memory_trees.ma rename helm/software/matita/contribs/ng_assembly/{freescale => memory}/memory_abs.ma (64%) rename helm/software/matita/contribs/ng_assembly/{freescale => memory}/memory_bits.ma (55%) rename helm/software/matita/contribs/ng_assembly/{freescale => memory}/memory_func.ma (67%) create mode 100755 helm/software/matita/contribs/ng_assembly/memory/memory_struct.ma create mode 100755 helm/software/matita/contribs/ng_assembly/memory/memory_trees.ma diff --git a/helm/software/matita/contribs/ng_assembly/depends b/helm/software/matita/contribs/ng_assembly/depends index a897995c2..fcdbc839b 100644 --- a/helm/software/matita/contribs/ng_assembly/depends +++ b/helm/software/matita/contribs/ng_assembly/depends @@ -1,6 +1,5 @@ freescale/multivm_lemmas.ma common/nat_lemmas.ma freescale/multivm.ma -freescale/status.ma freescale/memory_abs.ma freescale/opcode_base.ma -freescale/memory_bits.ma freescale/memory_trees.ma +freescale/status.ma freescale/opcode_base.ma memory/memory_abs.ma common/prod_lemmas.ma common/prod.ma num/bool_lemmas.ma num/bool.ma common/theory.ma freescale_tests/micro_tests10.ma freescale/multivm.ma freescale/status_lemmas.ma freescale_tests/micro_tests_tools.ma @@ -14,12 +13,12 @@ common/string_lemmas.ma common/ascii_lemmas.ma common/list_utility_lemmas.ma com common/nat.ma num/bool.ma compiler/ast_type_lemmas.ma common/list_utility_lemmas.ma compiler/ast_type.ma freescale_tests/micro_tests3.ma freescale/multivm.ma freescale/status_lemmas.ma freescale_tests/micro_tests_tools.ma +memory/memory_bits.ma memory/memory_trees.ma num/quatern.ma num/bool.ma num/exadecim.ma common/nat.ma common/prod.ma num/bool.ma num/oct.ma num/quatern.ma freescale/table_HC05_tests.ma freescale/opcode.ma freescale/table_HC05.ma num/bitrigesim_lemmas.ma num/bitrigesim.ma num/bool_lemmas.ma num/byte8.ma num/bitrigesim.ma num/exadecim.ma -freescale/memory_func.ma common/list.ma common/option.ma freescale/memory_struct.ma num/word16.ma freescale/load_write.ma freescale/model.ma freescale/translation.ma freescale_tests/micro_tests4bis.ma freescale/multivm.ma freescale/status_lemmas.ma freescale_tests/micro_tests_tools.ma freescale/table_RS08.ma common/list.ma freescale/opcode_base.ma @@ -29,14 +28,13 @@ common/list_utility_lemmas.ma common/list_lemmas.ma common/list_utility.ma freescale/table_RS08_tests.ma freescale/opcode.ma freescale/table_RS08.ma freescale/translation.ma common/option.ma freescale/table_HC05.ma freescale/table_HC08.ma freescale/table_HCS08.ma freescale/table_RS08.ma freescale/translation_lemmas.ma freescale/translation.ma num/byte8_lemmas.ma -freescale/memory_abs.ma freescale/memory_bits.ma freescale/memory_func.ma freescale/memory_trees.ma +memory/memory_func.ma common/list.ma common/option.ma memory/memory_struct.ma num/word32.ma num/word32_lemmas.ma num/word16_lemmas.ma num/word32.ma freescale_tests/micro_tests9.ma common/nat_to_num.ma freescale/multivm.ma freescale/status_lemmas.ma freescale_tests/micro_tests_tools.ma test_errori.ma freescale_tests/micro_tests2.ma freescale/multivm.ma freescale/status_lemmas.ma freescale_tests/micro_tests_tools.ma compiler/environment.ma common/string.ma compiler/ast_type.ma common/ascii_lemmas.ma common/ascii.ma num/bool_lemmas.ma -freescale/memory_struct.ma num/byte8.ma num/oct.ma freescale/model.ma freescale/status.ma freescale/table_HC05.ma common/list.ma freescale/opcode_base.ma common/string.ma common/ascii.ma common/list_utility.ma @@ -44,16 +42,18 @@ common/theory.ma compiler/ast_type.ma common/list_utility.ma num/word16.ma num/byte8.ma freescale_tests/micro_tests5.ma freescale/multivm.ma freescale/status_lemmas.ma freescale_tests/micro_tests_tools.ma -freescale/memory_trees.ma common/list.ma common/option.ma freescale/memory_struct.ma num/word16.ma common/prod.ma num/bool.ma num/exadecim_lemmas.ma num/bool_lemmas.ma num/exadecim.ma num/word16_lemmas.ma num/byte8_lemmas.ma num/word16.ma +memory/memory_trees.ma common/list.ma common/option.ma memory/memory_struct.ma num/word32.ma freescale_tests/medium_tests.ma common/list_utility.ma common/nat_to_num.ma freescale_tests/medium_tests_tools.ma num/bool_lemmas.ma num/bool.ma freescale/opcode_base_lemmas1.ma freescale/opcode_base_lemmas_instrmode.ma freescale/opcode_base_lemmas_opcode.ma num/word16_lemmas.ma freescale/table_HC08.ma common/list.ma freescale/opcode_base.ma +memory/memory_struct.ma num/byte8.ma num/oct.ma num/oct_lemmas.ma num/bool_lemmas.ma num/oct.ma freescale/table_HCS08.ma common/list.ma freescale/opcode_base.ma +memory/memory_abs.ma memory/memory_bits.ma memory/memory_func.ma memory/memory_trees.ma num/word32.ma num/word16.ma common/ascii.ma num/bool.ma freescale_tests/micro_tests8.ma freescale/multivm.ma freescale/status_lemmas.ma freescale_tests/micro_tests_tools.ma diff --git a/helm/software/matita/contribs/ng_assembly/freescale/memory_struct.ma b/helm/software/matita/contribs/ng_assembly/freescale/memory_struct.ma deleted file mode 100755 index 4fc65abeb..000000000 --- a/helm/software/matita/contribs/ng_assembly/freescale/memory_struct.ma +++ /dev/null @@ -1,624 +0,0 @@ -(**************************************************************************) -(* ___ *) -(* ||M|| *) -(* ||A|| A project by Andrea Asperti *) -(* ||T|| *) -(* ||I|| Developers: *) -(* ||T|| The HELM team. *) -(* ||A|| http://helm.cs.unibo.it *) -(* \ / *) -(* \ / This file is distributed under the terms of the *) -(* v GNU General Public License Version 2 *) -(* *) -(**************************************************************************) - -(* ********************************************************************** *) -(* Progetto FreeScale *) -(* *) -(* Sviluppato da: Ing. Cosimo Oliboni, oliboni@cs.unibo.it *) -(* Ultima modifica: 05/08/2009 *) -(* *) -(* ********************************************************************** *) - -include "num/oct.ma". -include "num/byte8.ma". - -(* **************************** *) -(* TIPI PER I MODULI DI MEMORIA *) -(* **************************** *) - -(* tipi di memoria:RAM/ROM/non installata *) -ninductive memory_type : Type ≝ - MEM_READ_ONLY: memory_type -| MEM_READ_WRITE: memory_type -| MEM_OUT_OF_BOUND: memory_type. - -(* **************** *) -(* TIPO ARRAY DA 16 *) -(* **************** *) - -(* definizione di un array omogeneo di dimensione 16 *) -ninductive Array16T (T:Type) : Type ≝ -array_16T : T → T → T → T → T → T → T → T → - T → T → T → T → T → T → T → T → - Array16T T. - -(* abbiamo gia' gli esadecimali come tipo induttivo quindi: *) -(* posso definire un getter a matrice sull'array *) -ndefinition getn_array16T ≝ -λn:exadecim.λT:Type.λp:Array16T T. - match p with - [ array_16T e00 e01 e02 e03 e04 e05 e06 e07 e08 e09 e10 e11 e12 e13 e14 e15 ⇒ - match n with - [ x0 ⇒ e00 | x1 ⇒ e01 | x2 ⇒ e02 | x3 ⇒ e03 | x4 ⇒ e04 | x5 ⇒ e05 | x6 ⇒ e06 | x7 ⇒ e07 - | x8 ⇒ e08 | x9 ⇒ e09 | xA ⇒ e10 | xB ⇒ e11 | xC ⇒ e12 | xD ⇒ e13 | xE ⇒ e14 | xF ⇒ e15 - ]]. - -(* abbiamo gia' gli esadecimali come tipo induttivo quindi: *) -(* posso definire un setter a matrice sull'array *) -ndefinition setn_array16T ≝ -λn:exadecim.λT:Type.λp:Array16T T.λv:T. - match p with - [ array_16T e00 e01 e02 e03 e04 e05 e06 e07 e08 e09 e10 e11 e12 e13 e14 e15 ⇒ - match n with - [ x0 ⇒ array_16T T v e01 e02 e03 e04 e05 e06 e07 e08 e09 e10 e11 e12 e13 e14 e15 - | x1 ⇒ array_16T T e00 v e02 e03 e04 e05 e06 e07 e08 e09 e10 e11 e12 e13 e14 e15 - | x2 ⇒ array_16T T e00 e01 v e03 e04 e05 e06 e07 e08 e09 e10 e11 e12 e13 e14 e15 - | x3 ⇒ array_16T T e00 e01 e02 v e04 e05 e06 e07 e08 e09 e10 e11 e12 e13 e14 e15 - | x4 ⇒ array_16T T e00 e01 e02 e03 v e05 e06 e07 e08 e09 e10 e11 e12 e13 e14 e15 - | x5 ⇒ array_16T T e00 e01 e02 e03 e04 v e06 e07 e08 e09 e10 e11 e12 e13 e14 e15 - | x6 ⇒ array_16T T e00 e01 e02 e03 e04 e05 v e07 e08 e09 e10 e11 e12 e13 e14 e15 - | x7 ⇒ array_16T T e00 e01 e02 e03 e04 e05 e06 v e08 e09 e10 e11 e12 e13 e14 e15 - | x8 ⇒ array_16T T e00 e01 e02 e03 e04 e05 e06 e07 v e09 e10 e11 e12 e13 e14 e15 - | x9 ⇒ array_16T T e00 e01 e02 e03 e04 e05 e06 e07 e08 v e10 e11 e12 e13 e14 e15 - | xA ⇒ array_16T T e00 e01 e02 e03 e04 e05 e06 e07 e08 e09 v e11 e12 e13 e14 e15 - | xB ⇒ array_16T T e00 e01 e02 e03 e04 e05 e06 e07 e08 e09 e10 v e12 e13 e14 e15 - | xC ⇒ array_16T T e00 e01 e02 e03 e04 e05 e06 e07 e08 e09 e10 e11 v e13 e14 e15 - | xD ⇒ array_16T T e00 e01 e02 e03 e04 e05 e06 e07 e08 e09 e10 e11 e12 v e14 e15 - | xE ⇒ array_16T T e00 e01 e02 e03 e04 e05 e06 e07 e08 e09 e10 e11 e12 e13 v e15 - | xF ⇒ array_16T T e00 e01 e02 e03 e04 e05 e06 e07 e08 e09 e10 e11 e12 e13 e14 v - ]]. - -(* abbiamo gia' gli esadecimali come tipo induttivo quindi: *) -(* posso definire un setter multiplo [m,n] a matrice sull'array *) -ndefinition setmn_array16T ≝ -λm,n:exadecim.λT:Type.λp:Array16T T.λv:T. - match p with - [ array_16T e00 e01 e02 e03 e04 e05 e06 e07 e08 e09 e10 e11 e12 e13 e14 e15 ⇒ - match m with - [ x0 ⇒ match n with - [ x0 ⇒ array_16T T v e01 e02 e03 e04 e05 e06 e07 e08 e09 e10 e11 e12 e13 e14 e15 - | x1 ⇒ array_16T T v v e02 e03 e04 e05 e06 e07 e08 e09 e10 e11 e12 e13 e14 e15 - | x2 ⇒ array_16T T v v v e03 e04 e05 e06 e07 e08 e09 e10 e11 e12 e13 e14 e15 - | x3 ⇒ array_16T T v v v v e04 e05 e06 e07 e08 e09 e10 e11 e12 e13 e14 e15 - | x4 ⇒ array_16T T v v v v v e05 e06 e07 e08 e09 e10 e11 e12 e13 e14 e15 - | x5 ⇒ array_16T T v v v v v v e06 e07 e08 e09 e10 e11 e12 e13 e14 e15 - | x6 ⇒ array_16T T v v v v v v v e07 e08 e09 e10 e11 e12 e13 e14 e15 - | x7 ⇒ array_16T T v v v v v v v v e08 e09 e10 e11 e12 e13 e14 e15 - | x8 ⇒ array_16T T v v v v v v v v v e09 e10 e11 e12 e13 e14 e15 - | x9 ⇒ array_16T T v v v v v v v v v v e10 e11 e12 e13 e14 e15 - | xA ⇒ array_16T T v v v v v v v v v v v e11 e12 e13 e14 e15 - | xB ⇒ array_16T T v v v v v v v v v v v v e12 e13 e14 e15 - | xC ⇒ array_16T T v v v v v v v v v v v v v e13 e14 e15 - | xD ⇒ array_16T T v v v v v v v v v v v v v v e14 e15 - | xE ⇒ array_16T T v v v v v v v v v v v v v v v e15 - | xF ⇒ array_16T T v v v v v v v v v v v v v v v v ] - | x1 ⇒ match n with - [ x0 ⇒ p - | x1 ⇒ array_16T T e00 v e02 e03 e04 e05 e06 e07 e08 e09 e10 e11 e12 e13 e14 e15 - | x2 ⇒ array_16T T e00 v v e03 e04 e05 e06 e07 e08 e09 e10 e11 e12 e13 e14 e15 - | x3 ⇒ array_16T T e00 v v v e04 e05 e06 e07 e08 e09 e10 e11 e12 e13 e14 e15 - | x4 ⇒ array_16T T e00 v v v v e05 e06 e07 e08 e09 e10 e11 e12 e13 e14 e15 - | x5 ⇒ array_16T T e00 v v v v v e06 e07 e08 e09 e10 e11 e12 e13 e14 e15 - | x6 ⇒ array_16T T e00 v v v v v v e07 e08 e09 e10 e11 e12 e13 e14 e15 - | x7 ⇒ array_16T T e00 v v v v v v v e08 e09 e10 e11 e12 e13 e14 e15 - | x8 ⇒ array_16T T e00 v v v v v v v v e09 e10 e11 e12 e13 e14 e15 - | x9 ⇒ array_16T T e00 v v v v v v v v v e10 e11 e12 e13 e14 e15 - | xA ⇒ array_16T T e00 v v v v v v v v v v e11 e12 e13 e14 e15 - | xB ⇒ array_16T T e00 v v v v v v v v v v v e12 e13 e14 e15 - | xC ⇒ array_16T T e00 v v v v v v v v v v v v e13 e14 e15 - | xD ⇒ array_16T T e00 v v v v v v v v v v v v v e14 e15 - | xE ⇒ array_16T T e00 v v v v v v v v v v v v v v e15 - | xF ⇒ array_16T T e00 v v v v v v v v v v v v v v v ] - | x2 ⇒ match n with - [ x0 ⇒ p | x1 ⇒ p - | x2 ⇒ array_16T T e00 e01 v e03 e04 e05 e06 e07 e08 e09 e10 e11 e12 e13 e14 e15 - | x3 ⇒ array_16T T e00 e01 v v e04 e05 e06 e07 e08 e09 e10 e11 e12 e13 e14 e15 - | x4 ⇒ array_16T T e00 e01 v v v e05 e06 e07 e08 e09 e10 e11 e12 e13 e14 e15 - | x5 ⇒ array_16T T e00 e01 v v v v e06 e07 e08 e09 e10 e11 e12 e13 e14 e15 - | x6 ⇒ array_16T T e00 e01 v v v v v e07 e08 e09 e10 e11 e12 e13 e14 e15 - | x7 ⇒ array_16T T e00 e01 v v v v v v e08 e09 e10 e11 e12 e13 e14 e15 - | x8 ⇒ array_16T T e00 e01 v v v v v v v e09 e10 e11 e12 e13 e14 e15 - | x9 ⇒ array_16T T e00 e01 v v v v v v v v e10 e11 e12 e13 e14 e15 - | xA ⇒ array_16T T e00 e01 v v v v v v v v v e11 e12 e13 e14 e15 - | xB ⇒ array_16T T e00 e01 v v v v v v v v v v e12 e13 e14 e15 - | xC ⇒ array_16T T e00 e01 v v v v v v v v v v v e13 e14 e15 - | xD ⇒ array_16T T e00 e01 v v v v v v v v v v v v e14 e15 - | xE ⇒ array_16T T e00 e01 v v v v v v v v v v v v v e15 - | xF ⇒ array_16T T e00 e01 v v v v v v v v v v v v v v ] - | x3 ⇒ match n with - [ x0 ⇒ p | x1 ⇒ p | x2 ⇒ p - | x3 ⇒ array_16T T e00 e01 e02 v e04 e05 e06 e07 e08 e09 e10 e11 e12 e13 e14 e15 - | x4 ⇒ array_16T T e00 e01 e02 v v e05 e06 e07 e08 e09 e10 e11 e12 e13 e14 e15 - | x5 ⇒ array_16T T e00 e01 e02 v v v e06 e07 e08 e09 e10 e11 e12 e13 e14 e15 - | x6 ⇒ array_16T T e00 e01 e02 v v v v e07 e08 e09 e10 e11 e12 e13 e14 e15 - | x7 ⇒ array_16T T e00 e01 e02 v v v v v e08 e09 e10 e11 e12 e13 e14 e15 - | x8 ⇒ array_16T T e00 e01 e02 v v v v v v e09 e10 e11 e12 e13 e14 e15 - | x9 ⇒ array_16T T e00 e01 e02 v v v v v v v e10 e11 e12 e13 e14 e15 - | xA ⇒ array_16T T e00 e01 e02 v v v v v v v v e11 e12 e13 e14 e15 - | xB ⇒ array_16T T e00 e01 e02 v v v v v v v v v e12 e13 e14 e15 - | xC ⇒ array_16T T e00 e01 e02 v v v v v v v v v v e13 e14 e15 - | xD ⇒ array_16T T e00 e01 e02 v v v v v v v v v v v e14 e15 - | xE ⇒ array_16T T e00 e01 e02 v v v v v v v v v v v v e15 - | xF ⇒ array_16T T e00 e01 e02 v v v v v v v v v v v v v ] - | x4 ⇒ match n with - [ x0 ⇒ p | x1 ⇒ p | x2 ⇒ p | x3 ⇒ p - | x4 ⇒ array_16T T e00 e01 e02 e03 v e05 e06 e07 e08 e09 e10 e11 e12 e13 e14 e15 - | x5 ⇒ array_16T T e00 e01 e02 e03 v v e06 e07 e08 e09 e10 e11 e12 e13 e14 e15 - | x6 ⇒ array_16T T e00 e01 e02 e03 v v v e07 e08 e09 e10 e11 e12 e13 e14 e15 - | x7 ⇒ array_16T T e00 e01 e02 e03 v v v v e08 e09 e10 e11 e12 e13 e14 e15 - | x8 ⇒ array_16T T e00 e01 e02 e03 v v v v v e09 e10 e11 e12 e13 e14 e15 - | x9 ⇒ array_16T T e00 e01 e02 e03 v v v v v v e10 e11 e12 e13 e14 e15 - | xA ⇒ array_16T T e00 e01 e02 e03 v v v v v v v e11 e12 e13 e14 e15 - | xB ⇒ array_16T T e00 e01 e02 e03 v v v v v v v v e12 e13 e14 e15 - | xC ⇒ array_16T T e00 e01 e02 e03 v v v v v v v v v e13 e14 e15 - | xD ⇒ array_16T T e00 e01 e02 e03 v v v v v v v v v v e14 e15 - | xE ⇒ array_16T T e00 e01 e02 e03 v v v v v v v v v v v e15 - | xF ⇒ array_16T T e00 e01 e02 e03 v v v v v v v v v v v v ] - | x5 ⇒ match n with - [ x0 ⇒ p | x1 ⇒ p | x2 ⇒ p | x3 ⇒ p | x4 ⇒ p - | x5 ⇒ array_16T T e00 e01 e02 e03 e04 v e06 e07 e08 e09 e10 e11 e12 e13 e14 e15 - | x6 ⇒ array_16T T e00 e01 e02 e03 e04 v v e07 e08 e09 e10 e11 e12 e13 e14 e15 - | x7 ⇒ array_16T T e00 e01 e02 e03 e04 v v v e08 e09 e10 e11 e12 e13 e14 e15 - | x8 ⇒ array_16T T e00 e01 e02 e03 e04 v v v v e09 e10 e11 e12 e13 e14 e15 - | x9 ⇒ array_16T T e00 e01 e02 e03 e04 v v v v v e10 e11 e12 e13 e14 e15 - | xA ⇒ array_16T T e00 e01 e02 e03 e04 v v v v v v e11 e12 e13 e14 e15 - | xB ⇒ array_16T T e00 e01 e02 e03 e04 v v v v v v v e12 e13 e14 e15 - | xC ⇒ array_16T T e00 e01 e02 e03 e04 v v v v v v v v e13 e14 e15 - | xD ⇒ array_16T T e00 e01 e02 e03 e04 v v v v v v v v v e14 e15 - | xE ⇒ array_16T T e00 e01 e02 e03 e04 v v v v v v v v v v e15 - | xF ⇒ array_16T T e00 e01 e02 e03 e04 v v v v v v v v v v v ] - | x6 ⇒ match n with - [ x0 ⇒ p | x1 ⇒ p | x2 ⇒ p | x3 ⇒ p | x4 ⇒ p | x5 ⇒ p - | x6 ⇒ array_16T T e00 e01 e02 e03 e04 e05 v e07 e08 e09 e10 e11 e12 e13 e14 e15 - | x7 ⇒ array_16T T e00 e01 e02 e03 e04 e05 v v e08 e09 e10 e11 e12 e13 e14 e15 - | x8 ⇒ array_16T T e00 e01 e02 e03 e04 e05 v v v e09 e10 e11 e12 e13 e14 e15 - | x9 ⇒ array_16T T e00 e01 e02 e03 e04 e05 v v v v e10 e11 e12 e13 e14 e15 - | xA ⇒ array_16T T e00 e01 e02 e03 e04 e05 v v v v v e11 e12 e13 e14 e15 - | xB ⇒ array_16T T e00 e01 e02 e03 e04 e05 v v v v v v e12 e13 e14 e15 - | xC ⇒ array_16T T e00 e01 e02 e03 e04 e05 v v v v v v v e13 e14 e15 - | xD ⇒ array_16T T e00 e01 e02 e03 e04 e05 v v v v v v v v e14 e15 - | xE ⇒ array_16T T e00 e01 e02 e03 e04 e05 v v v v v v v v v e15 - | xF ⇒ array_16T T e00 e01 e02 e03 e04 e05 v v v v v v v v v v ] - | x7 ⇒ match n with - [ x0 ⇒ p | x1 ⇒ p | x2 ⇒ p | x3 ⇒ p | x4 ⇒ p | x5 ⇒ p | x6 ⇒ p - | x7 ⇒ array_16T T e00 e01 e02 e03 e04 e05 e06 v e08 e09 e10 e11 e12 e13 e14 e15 - | x8 ⇒ array_16T T e00 e01 e02 e03 e04 e05 e06 v v e09 e10 e11 e12 e13 e14 e15 - | x9 ⇒ array_16T T e00 e01 e02 e03 e04 e05 e06 v v v e10 e11 e12 e13 e14 e15 - | xA ⇒ array_16T T e00 e01 e02 e03 e04 e05 e06 v v v v e11 e12 e13 e14 e15 - | xB ⇒ array_16T T e00 e01 e02 e03 e04 e05 e06 v v v v v e12 e13 e14 e15 - | xC ⇒ array_16T T e00 e01 e02 e03 e04 e05 e06 v v v v v v e13 e14 e15 - | xD ⇒ array_16T T e00 e01 e02 e03 e04 e05 e06 v v v v v v v e14 e15 - | xE ⇒ array_16T T e00 e01 e02 e03 e04 e05 e06 v v v v v v v v e15 - | xF ⇒ array_16T T e00 e01 e02 e03 e04 e05 e06 v v v v v v v v v ] - | x8 ⇒ match n with - [ x0 ⇒ p | x1 ⇒ p | x2 ⇒ p | x3 ⇒ p | x4 ⇒ p | x5 ⇒ p | x6 ⇒ p | x7 ⇒ p - | x8 ⇒ array_16T T e00 e01 e02 e03 e04 e05 e06 e07 v e09 e10 e11 e12 e13 e14 e15 - | x9 ⇒ array_16T T e00 e01 e02 e03 e04 e05 e06 e07 v v e10 e11 e12 e13 e14 e15 - | xA ⇒ array_16T T e00 e01 e02 e03 e04 e05 e06 e07 v v v e11 e12 e13 e14 e15 - | xB ⇒ array_16T T e00 e01 e02 e03 e04 e05 e06 e07 v v v v e12 e13 e14 e15 - | xC ⇒ array_16T T e00 e01 e02 e03 e04 e05 e06 e07 v v v v v e13 e14 e15 - | xD ⇒ array_16T T e00 e01 e02 e03 e04 e05 e06 e07 v v v v v v e14 e15 - | xE ⇒ array_16T T e00 e01 e02 e03 e04 e05 e06 e07 v v v v v v v e15 - | xF ⇒ array_16T T e00 e01 e02 e03 e04 e05 e06 e07 v v v v v v v v ] - | x9 ⇒ match n with - [ x0 ⇒ p | x1 ⇒ p | x2 ⇒ p | x3 ⇒ p | x4 ⇒ p | x5 ⇒ p | x6 ⇒ p | x7 ⇒ p - | x8 ⇒ p - | x9 ⇒ array_16T T e00 e01 e02 e03 e04 e05 e06 e07 e08 v e10 e11 e12 e13 e14 e15 - | xA ⇒ array_16T T e00 e01 e02 e03 e04 e05 e06 e07 e08 v v e11 e12 e13 e14 e15 - | xB ⇒ array_16T T e00 e01 e02 e03 e04 e05 e06 e07 e08 v v v e12 e13 e14 e15 - | xC ⇒ array_16T T e00 e01 e02 e03 e04 e05 e06 e07 e08 v v v v e13 e14 e15 - | xD ⇒ array_16T T e00 e01 e02 e03 e04 e05 e06 e07 e08 v v v v v e14 e15 - | xE ⇒ array_16T T e00 e01 e02 e03 e04 e05 e06 e07 e08 v v v v v v e15 - | xF ⇒ array_16T T e00 e01 e02 e03 e04 e05 e06 e07 e08 v v v v v v v ] - | xA ⇒ match n with - [ x0 ⇒ p | x1 ⇒ p | x2 ⇒ p | x3 ⇒ p | x4 ⇒ p | x5 ⇒ p | x6 ⇒ p | x7 ⇒ p - | x8 ⇒ p | x9 ⇒ p - | xA ⇒ array_16T T e00 e01 e02 e03 e04 e05 e06 e07 e08 e09 v e11 e12 e13 e14 e15 - | xB ⇒ array_16T T e00 e01 e02 e03 e04 e05 e06 e07 e08 e09 v v e12 e13 e14 e15 - | xC ⇒ array_16T T e00 e01 e02 e03 e04 e05 e06 e07 e08 e09 v v v e13 e14 e15 - | xD ⇒ array_16T T e00 e01 e02 e03 e04 e05 e06 e07 e08 e09 v v v v e14 e15 - | xE ⇒ array_16T T e00 e01 e02 e03 e04 e05 e06 e07 e08 e09 v v v v v e15 - | xF ⇒ array_16T T e00 e01 e02 e03 e04 e05 e06 e07 e08 e09 v v v v v v ] - | xB ⇒ match n with - [ x0 ⇒ p | x1 ⇒ p | x2 ⇒ p | x3 ⇒ p | x4 ⇒ p | x5 ⇒ p | x6 ⇒ p | x7 ⇒ p - | x8 ⇒ p | x9 ⇒ p | xA ⇒ p - | xB ⇒ array_16T T e00 e01 e02 e03 e04 e05 e06 e07 e08 e09 e10 v e12 e13 e14 e15 - | xC ⇒ array_16T T e00 e01 e02 e03 e04 e05 e06 e07 e08 e09 e10 v v e13 e14 e15 - | xD ⇒ array_16T T e00 e01 e02 e03 e04 e05 e06 e07 e08 e09 e10 v v v e14 e15 - | xE ⇒ array_16T T e00 e01 e02 e03 e04 e05 e06 e07 e08 e09 e10 v v v v e15 - | xF ⇒ array_16T T e00 e01 e02 e03 e04 e05 e06 e07 e08 e09 e10 v v v v v ] - | xC ⇒ match n with - [ x0 ⇒ p | x1 ⇒ p | x2 ⇒ p | x3 ⇒ p | x4 ⇒ p | x5 ⇒ p | x6 ⇒ p | x7 ⇒ p - | x8 ⇒ p | x9 ⇒ p | xA ⇒ p | xB ⇒ p - | xC ⇒ array_16T T e00 e01 e02 e03 e04 e05 e06 e07 e08 e09 e10 e11 v e13 e14 e15 - | xD ⇒ array_16T T e00 e01 e02 e03 e04 e05 e06 e07 e08 e09 e10 e11 v v e14 e15 - | xE ⇒ array_16T T e00 e01 e02 e03 e04 e05 e06 e07 e08 e09 e10 e11 v v v e15 - | xF ⇒ array_16T T e00 e01 e02 e03 e04 e05 e06 e07 e08 e09 e10 e11 v v v v ] - | xD ⇒ match n with - [ x0 ⇒ p | x1 ⇒ p | x2 ⇒ p | x3 ⇒ p | x4 ⇒ p | x5 ⇒ p | x6 ⇒ p | x7 ⇒ p - | x8 ⇒ p | x9 ⇒ p | xA ⇒ p | xB ⇒ p | xC ⇒ p - | xD ⇒ array_16T T e00 e01 e02 e03 e04 e05 e06 e07 e08 e09 e10 e11 e12 v e14 e15 - | xE ⇒ array_16T T e00 e01 e02 e03 e04 e05 e06 e07 e08 e09 e10 e11 e12 v v e15 - | xF ⇒ array_16T T e00 e01 e02 e03 e04 e05 e06 e07 e08 e09 e10 e11 e12 v v v ] - | xE ⇒ match n with - [ x0 ⇒ p | x1 ⇒ p | x2 ⇒ p | x3 ⇒ p | x4 ⇒ p | x5 ⇒ p | x6 ⇒ p | x7 ⇒ p - | x8 ⇒ p | x9 ⇒ p | xA ⇒ p | xB ⇒ p | xC ⇒ p | xD ⇒ p - | xE ⇒ array_16T T e00 e01 e02 e03 e04 e05 e06 e07 e08 e09 e10 e11 e12 e13 v e15 - | xF ⇒ array_16T T e00 e01 e02 e03 e04 e05 e06 e07 e08 e09 e10 e11 e12 e13 v v ] - | xF ⇒ match n with - [ x0 ⇒ p | x1 ⇒ p | x2 ⇒ p | x3 ⇒ p | x4 ⇒ p | x5 ⇒ p | x6 ⇒ p | x7 ⇒ p - | x8 ⇒ p | x9 ⇒ p | xA ⇒ p | xB ⇒ p | xC ⇒ p | xD ⇒ p | xE ⇒ p - | xF ⇒ array_16T T e00 e01 e02 e03 e04 e05 e06 e07 e08 e09 e10 e11 e12 e13 e14 v ] - ]]. - -(* abbiamo gia' gli esadecimali come tipo induttivo quindi: *) -(* posso definire un setter composto [m+1,n-1] a matrice sull'array *) -(* NB: obbiettivo evitare l'overflow *) -ndefinition setmn_array16T_succ_pred ≝ -λm,n:exadecim.λT:Type.λp:Array16T T.λv:T. - match lt_ex m xF with - [ true ⇒ match gt_ex n x0 with - [ true ⇒ setmn_array16T (succ_ex m) (pred_ex n) T p v - | false ⇒ p - ] - | false ⇒ p - ]. - -(* abbiamo gia' gli esadecimali come tipo induttivo quindi: *) -(* posso definire un setter composto [m+1,F] a matrice sull'array *) -(* NB: obbiettivo evitare l'overflow *) -ndefinition setmn_array16T_succ ≝ -λm:exadecim.λT:Type.λp:Array16T T.λv:T. - match lt_ex m xF with - [ true ⇒ setmn_array16T (succ_ex m) xF T p v - | false ⇒ p - ]. - -(* abbiamo gia' gli esadecimali come tipo induttivo quindi: *) -(* posso definire un setter composto [0,n-1] a matrice sull'array *) -(* NB: obbiettivo evitare l'overflow *) -ndefinition setmn_array16T_pred ≝ -λn:exadecim.λT:Type.λp:Array16T T.λv:T. - match gt_ex n x0 with - [ true ⇒ setmn_array16T x0 (pred_ex n) T p v - | false ⇒ p - ]. - -(* ************************** *) -(* TIPO BYTE COME INSIEME BIT *) -(* ************************** *) - -(* definizione di un byte come 8 bit *) -ninductive Array8T (T:Type) : Type ≝ -array_8T : T → T → T → T → T → T → T → T → - Array8T T. - -(* abbiamo gia' gli ottali come tipo induttivo quindi: *) -(* posso definire un getter a matrice sull'array *) -ndefinition getn_array8T ≝ -λn:oct.λT:Type.λp:Array8T T. - match p with - [ array_8T e07 e06 e05 e04 e03 e02 e01 e00 ⇒ - match n with - [ o0 ⇒ e00 | o1 ⇒ e01 | o2 ⇒ e02 | o3 ⇒ e03 | o4 ⇒ e04 | o5 ⇒ e05 | o6 ⇒ e06 | o7 ⇒ e07 ]]. - -(* abbiamo gia' gli ottali come tipo induttivo quindi: *) -(* posso definire un setter a matrice sull'array *) -ndefinition setn_array8T ≝ -λn:oct.λT:Type.λp:Array8T T.λv:T. - match p with - [ array_8T e07 e06 e05 e04 e03 e02 e01 e00 ⇒ - match n with - [ o0 ⇒ array_8T T e07 e06 e05 e04 e03 e02 e01 v - | o1 ⇒ array_8T T e07 e06 e05 e04 e03 e02 v e00 - | o2 ⇒ array_8T T e07 e06 e05 e04 e03 v e01 e00 - | o3 ⇒ array_8T T e07 e06 e05 e04 v e02 e01 e00 - | o4 ⇒ array_8T T e07 e06 e05 v e03 e02 e01 e00 - | o5 ⇒ array_8T T e07 e06 v e04 e03 e02 e01 e00 - | o6 ⇒ array_8T T e07 v e05 e04 e03 e02 e01 e00 - | o7 ⇒ array_8T T v e06 e05 e04 e03 e02 e01 e00 - ]]. - -(* lettura byte *) -ndefinition byte8_of_bits ≝ -λp:Array8T bool. - match p with - [ array_8T e07 e06 e05 e04 e03 e02 e01 e00 ⇒ - mk_byte8 - (or_ex (match e07 with [ true ⇒ x8 | false ⇒ x0 ]) - (or_ex (match e06 with [ true ⇒ x4 | false ⇒ x0 ]) - (or_ex (match e05 with [ true ⇒ x2 | false ⇒ x0 ]) - (match e04 with [ true ⇒ x1 | false ⇒ x0 ])))) - (or_ex (match e03 with [ true ⇒ x8 | false ⇒ x0 ]) - (or_ex (match e02 with [ true ⇒ x4 | false ⇒ x0 ]) - (or_ex (match e01 with [ true ⇒ x2 | false ⇒ x0 ]) - (match e00 with [ true ⇒ x1 | false ⇒ x0 ])))) ]. - -(* scrittura byte *) -ndefinition bits_of_byte8 ≝ -λp:byte8. - match b8h p with - [ x0 ⇒ match b8l p with - [ x0 ⇒ array_8T bool false false false false false false false false - | x1 ⇒ array_8T bool false false false false false false false true - | x2 ⇒ array_8T bool false false false false false false true false - | x3 ⇒ array_8T bool false false false false false false true true - | x4 ⇒ array_8T bool false false false false false true false false - | x5 ⇒ array_8T bool false false false false false true false true - | x6 ⇒ array_8T bool false false false false false true true false - | x7 ⇒ array_8T bool false false false false false true true true - | x8 ⇒ array_8T bool false false false false true false false false - | x9 ⇒ array_8T bool false false false false true false false true - | xA ⇒ array_8T bool false false false false true false true false - | xB ⇒ array_8T bool false false false false true false true true - | xC ⇒ array_8T bool false false false false true true false false - | xD ⇒ array_8T bool false false false false true true false true - | xE ⇒ array_8T bool false false false false true true true false - | xF ⇒ array_8T bool false false false false true true true true ] - | x1 ⇒ match b8l p with - [ x0 ⇒ array_8T bool false false false true false false false false - | x1 ⇒ array_8T bool false false false true false false false true - | x2 ⇒ array_8T bool false false false true false false true false - | x3 ⇒ array_8T bool false false false true false false true true - | x4 ⇒ array_8T bool false false false true false true false false - | x5 ⇒ array_8T bool false false false true false true false true - | x6 ⇒ array_8T bool false false false true false true true false - | x7 ⇒ array_8T bool false false false true false true true true - | x8 ⇒ array_8T bool false false false true true false false false - | x9 ⇒ array_8T bool false false false true true false false true - | xA ⇒ array_8T bool false false false true true false true false - | xB ⇒ array_8T bool false false false true true false true true - | xC ⇒ array_8T bool false false false true true true false false - | xD ⇒ array_8T bool false false false true true true false true - | xE ⇒ array_8T bool false false false true true true true false - | xF ⇒ array_8T bool false false false true true true true true ] - | x2 ⇒ match b8l p with - [ x0 ⇒ array_8T bool false false true false false false false false - | x1 ⇒ array_8T bool false false true false false false false true - | x2 ⇒ array_8T bool false false true false false false true false - | x3 ⇒ array_8T bool false false true false false false true true - | x4 ⇒ array_8T bool false false true false false true false false - | x5 ⇒ array_8T bool false false true false false true false true - | x6 ⇒ array_8T bool false false true false false true true false - | x7 ⇒ array_8T bool false false true false false true true true - | x8 ⇒ array_8T bool false false true false true false false false - | x9 ⇒ array_8T bool false false true false true false false true - | xA ⇒ array_8T bool false false true false true false true false - | xB ⇒ array_8T bool false false true false true false true true - | xC ⇒ array_8T bool false false true false true true false false - | xD ⇒ array_8T bool false false true false true true false true - | xE ⇒ array_8T bool false false true false true true true false - | xF ⇒ array_8T bool false false true false true true true true ] - | x3 ⇒ match b8l p with - [ x0 ⇒ array_8T bool false false true true false false false false - | x1 ⇒ array_8T bool false false true true false false false true - | x2 ⇒ array_8T bool false false true true false false true false - | x3 ⇒ array_8T bool false false true true false false true true - | x4 ⇒ array_8T bool false false true true false true false false - | x5 ⇒ array_8T bool false false true true false true false true - | x6 ⇒ array_8T bool false false true true false true true false - | x7 ⇒ array_8T bool false false true true false true true true - | x8 ⇒ array_8T bool false false true true true false false false - | x9 ⇒ array_8T bool false false true true true false false true - | xA ⇒ array_8T bool false false true true true false true false - | xB ⇒ array_8T bool false false true true true false true true - | xC ⇒ array_8T bool false false true true true true false false - | xD ⇒ array_8T bool false false true true true true false true - | xE ⇒ array_8T bool false false true true true true true false - | xF ⇒ array_8T bool false false true true true true true true ] - | x4 ⇒ match b8l p with - [ x0 ⇒ array_8T bool false true false false false false false false - | x1 ⇒ array_8T bool false true false false false false false true - | x2 ⇒ array_8T bool false true false false false false true false - | x3 ⇒ array_8T bool false true false false false false true true - | x4 ⇒ array_8T bool false true false false false true false false - | x5 ⇒ array_8T bool false true false false false true false true - | x6 ⇒ array_8T bool false true false false false true true false - | x7 ⇒ array_8T bool false true false false false true true true - | x8 ⇒ array_8T bool false true false false true false false false - | x9 ⇒ array_8T bool false true false false true false false true - | xA ⇒ array_8T bool false true false false true false true false - | xB ⇒ array_8T bool false true false false true false true true - | xC ⇒ array_8T bool false true false false true true false false - | xD ⇒ array_8T bool false true false false true true false true - | xE ⇒ array_8T bool false true false false true true true false - | xF ⇒ array_8T bool false true false false true true true true ] - | x5 ⇒ match b8l p with - [ x0 ⇒ array_8T bool false true false true false false false false - | x1 ⇒ array_8T bool false true false true false false false true - | x2 ⇒ array_8T bool false true false true false false true false - | x3 ⇒ array_8T bool false true false true false false true true - | x4 ⇒ array_8T bool false true false true false true false false - | x5 ⇒ array_8T bool false true false true false true false true - | x6 ⇒ array_8T bool false true false true false true true false - | x7 ⇒ array_8T bool false true false true false true true true - | x8 ⇒ array_8T bool false true false true true false false false - | x9 ⇒ array_8T bool false true false true true false false true - | xA ⇒ array_8T bool false true false true true false true false - | xB ⇒ array_8T bool false true false true true false true true - | xC ⇒ array_8T bool false true false true true true false false - | xD ⇒ array_8T bool false true false true true true false true - | xE ⇒ array_8T bool false true false true true true true false - | xF ⇒ array_8T bool false true false true true true true true ] - | x6 ⇒ match b8l p with - [ x0 ⇒ array_8T bool false true true false false false false false - | x1 ⇒ array_8T bool false true true false false false false true - | x2 ⇒ array_8T bool false true true false false false true false - | x3 ⇒ array_8T bool false true true false false false true true - | x4 ⇒ array_8T bool false true true false false true false false - | x5 ⇒ array_8T bool false true true false false true false true - | x6 ⇒ array_8T bool false true true false false true true false - | x7 ⇒ array_8T bool false true true false false true true true - | x8 ⇒ array_8T bool false true true false true false false false - | x9 ⇒ array_8T bool false true true false true false false true - | xA ⇒ array_8T bool false true true false true false true false - | xB ⇒ array_8T bool false true true false true false true true - | xC ⇒ array_8T bool false true true false true true false false - | xD ⇒ array_8T bool false true true false true true false true - | xE ⇒ array_8T bool false true true false true true true false - | xF ⇒ array_8T bool false true true false true true true true ] - | x7 ⇒ match b8l p with - [ x0 ⇒ array_8T bool false true true true false false false false - | x1 ⇒ array_8T bool false true true true false false false true - | x2 ⇒ array_8T bool false true true true false false true false - | x3 ⇒ array_8T bool false true true true false false true true - | x4 ⇒ array_8T bool false true true true false true false false - | x5 ⇒ array_8T bool false true true true false true false true - | x6 ⇒ array_8T bool false true true true false true true false - | x7 ⇒ array_8T bool false true true true false true true true - | x8 ⇒ array_8T bool false true true true true false false false - | x9 ⇒ array_8T bool false true true true true false false true - | xA ⇒ array_8T bool false true true true true false true false - | xB ⇒ array_8T bool false true true true true false true true - | xC ⇒ array_8T bool false true true true true true false false - | xD ⇒ array_8T bool false true true true true true false true - | xE ⇒ array_8T bool false true true true true true true false - | xF ⇒ array_8T bool false true true true true true true true ] - | x8 ⇒ match b8l p with - [ x0 ⇒ array_8T bool true false false false false false false false - | x1 ⇒ array_8T bool true false false false false false false true - | x2 ⇒ array_8T bool true false false false false false true false - | x3 ⇒ array_8T bool true false false false false false true true - | x4 ⇒ array_8T bool true false false false false true false false - | x5 ⇒ array_8T bool true false false false false true false true - | x6 ⇒ array_8T bool true false false false false true true false - | x7 ⇒ array_8T bool true false false false false true true true - | x8 ⇒ array_8T bool true false false false true false false false - | x9 ⇒ array_8T bool true false false false true false false true - | xA ⇒ array_8T bool true false false false true false true false - | xB ⇒ array_8T bool true false false false true false true true - | xC ⇒ array_8T bool true false false false true true false false - | xD ⇒ array_8T bool true false false false true true false true - | xE ⇒ array_8T bool true false false false true true true false - | xF ⇒ array_8T bool true false false false true true true true ] - | x9 ⇒ match b8l p with - [ x0 ⇒ array_8T bool true false false true false false false false - | x1 ⇒ array_8T bool true false false true false false false true - | x2 ⇒ array_8T bool true false false true false false true false - | x3 ⇒ array_8T bool true false false true false false true true - | x4 ⇒ array_8T bool true false false true false true false false - | x5 ⇒ array_8T bool true false false true false true false true - | x6 ⇒ array_8T bool true false false true false true true false - | x7 ⇒ array_8T bool true false false true false true true true - | x8 ⇒ array_8T bool true false false true true false false false - | x9 ⇒ array_8T bool true false false true true false false true - | xA ⇒ array_8T bool true false false true true false true false - | xB ⇒ array_8T bool true false false true true false true true - | xC ⇒ array_8T bool true false false true true true false false - | xD ⇒ array_8T bool true false false true true true false true - | xE ⇒ array_8T bool true false false true true true true false - | xF ⇒ array_8T bool true false false true true true true true ] - | xA ⇒ match b8l p with - [ x0 ⇒ array_8T bool true false true false false false false false - | x1 ⇒ array_8T bool true false true false false false false true - | x2 ⇒ array_8T bool true false true false false false true false - | x3 ⇒ array_8T bool true false true false false false true true - | x4 ⇒ array_8T bool true false true false false true false false - | x5 ⇒ array_8T bool true false true false false true false true - | x6 ⇒ array_8T bool true false true false false true true false - | x7 ⇒ array_8T bool true false true false false true true true - | x8 ⇒ array_8T bool true false true false true false false false - | x9 ⇒ array_8T bool true false true false true false false true - | xA ⇒ array_8T bool true false true false true false true false - | xB ⇒ array_8T bool true false true false true false true true - | xC ⇒ array_8T bool true false true false true true false false - | xD ⇒ array_8T bool true false true false true true false true - | xE ⇒ array_8T bool true false true false true true true false - | xF ⇒ array_8T bool true false true false true true true true ] - | xB ⇒ match b8l p with - [ x0 ⇒ array_8T bool true false true true false false false false - | x1 ⇒ array_8T bool true false true true false false false true - | x2 ⇒ array_8T bool true false true true false false true false - | x3 ⇒ array_8T bool true false true true false false true true - | x4 ⇒ array_8T bool true false true true false true false false - | x5 ⇒ array_8T bool true false true true false true false true - | x6 ⇒ array_8T bool true false true true false true true false - | x7 ⇒ array_8T bool true false true true false true true true - | x8 ⇒ array_8T bool true false true true true false false false - | x9 ⇒ array_8T bool true false true true true false false true - | xA ⇒ array_8T bool true false true true true false true false - | xB ⇒ array_8T bool true false true true true false true true - | xC ⇒ array_8T bool true false true true true true false false - | xD ⇒ array_8T bool true false true true true true false true - | xE ⇒ array_8T bool true false true true true true true false - | xF ⇒ array_8T bool true false true true true true true true ] - | xC ⇒ match b8l p with - [ x0 ⇒ array_8T bool true true false false false false false false - | x1 ⇒ array_8T bool true true false false false false false true - | x2 ⇒ array_8T bool true true false false false false true false - | x3 ⇒ array_8T bool true true false false false false true true - | x4 ⇒ array_8T bool true true false false false true false false - | x5 ⇒ array_8T bool true true false false false true false true - | x6 ⇒ array_8T bool true true false false false true true false - | x7 ⇒ array_8T bool true true false false false true true true - | x8 ⇒ array_8T bool true true false false true false false false - | x9 ⇒ array_8T bool true true false false true false false true - | xA ⇒ array_8T bool true true false false true false true false - | xB ⇒ array_8T bool true true false false true false true true - | xC ⇒ array_8T bool true true false false true true false false - | xD ⇒ array_8T bool true true false false true true false true - | xE ⇒ array_8T bool true true false false true true true false - | xF ⇒ array_8T bool true true false false true true true true ] - | xD ⇒ match b8l p with - [ x0 ⇒ array_8T bool true true false true false false false false - | x1 ⇒ array_8T bool true true false true false false false true - | x2 ⇒ array_8T bool true true false true false false true false - | x3 ⇒ array_8T bool true true false true false false true true - | x4 ⇒ array_8T bool true true false true false true false false - | x5 ⇒ array_8T bool true true false true false true false true - | x6 ⇒ array_8T bool true true false true false true true false - | x7 ⇒ array_8T bool true true false true false true true true - | x8 ⇒ array_8T bool true true false true true false false false - | x9 ⇒ array_8T bool true true false true true false false true - | xA ⇒ array_8T bool true true false true true false true false - | xB ⇒ array_8T bool true true false true true false true true - | xC ⇒ array_8T bool true true false true true true false false - | xD ⇒ array_8T bool true true false true true true false true - | xE ⇒ array_8T bool true true false true true true true false - | xF ⇒ array_8T bool true true false true true true true true ] - | xE ⇒ match b8l p with - [ x0 ⇒ array_8T bool true true true false false false false false - | x1 ⇒ array_8T bool true true true false false false false true - | x2 ⇒ array_8T bool true true true false false false true false - | x3 ⇒ array_8T bool true true true false false false true true - | x4 ⇒ array_8T bool true true true false false true false false - | x5 ⇒ array_8T bool true true true false false true false true - | x6 ⇒ array_8T bool true true true false false true true false - | x7 ⇒ array_8T bool true true true false false true true true - | x8 ⇒ array_8T bool true true true false true false false false - | x9 ⇒ array_8T bool true true true false true false false true - | xA ⇒ array_8T bool true true true false true false true false - | xB ⇒ array_8T bool true true true false true false true true - | xC ⇒ array_8T bool true true true false true true false false - | xD ⇒ array_8T bool true true true false true true false true - | xE ⇒ array_8T bool true true true false true true true false - | xF ⇒ array_8T bool true true true false true true true true ] - | xF ⇒ match b8l p with - [ x0 ⇒ array_8T bool true true true true false false false false - | x1 ⇒ array_8T bool true true true true false false false true - | x2 ⇒ array_8T bool true true true true false false true false - | x3 ⇒ array_8T bool true true true true false false true true - | x4 ⇒ array_8T bool true true true true false true false false - | x5 ⇒ array_8T bool true true true true false true false true - | x6 ⇒ array_8T bool true true true true false true true false - | x7 ⇒ array_8T bool true true true true false true true true - | x8 ⇒ array_8T bool true true true true true false false false - | x9 ⇒ array_8T bool true true true true true false false true - | xA ⇒ array_8T bool true true true true true false true false - | xB ⇒ array_8T bool true true true true true false true true - | xC ⇒ array_8T bool true true true true true true false false - | xD ⇒ array_8T bool true true true true true true false true - | xE ⇒ array_8T bool true true true true true true true false - | xF ⇒ array_8T bool true true true true true true true true ] - ]. diff --git a/helm/software/matita/contribs/ng_assembly/freescale/memory_trees.ma b/helm/software/matita/contribs/ng_assembly/freescale/memory_trees.ma deleted file mode 100755 index e1e338b81..000000000 --- a/helm/software/matita/contribs/ng_assembly/freescale/memory_trees.ma +++ /dev/null @@ -1,227 +0,0 @@ -(**************************************************************************) -(* ___ *) -(* ||M|| *) -(* ||A|| A project by Andrea Asperti *) -(* ||T|| *) -(* ||I|| Developers: *) -(* ||T|| The HELM team. *) -(* ||A|| http://helm.cs.unibo.it *) -(* \ / *) -(* \ / This file is distributed under the terms of the *) -(* v GNU General Public License Version 2 *) -(* *) -(**************************************************************************) - -(* ********************************************************************** *) -(* Progetto FreeScale *) -(* *) -(* Sviluppato da: Ing. Cosimo Oliboni, oliboni@cs.unibo.it *) -(* Ultima modifica: 05/08/2009 *) -(* *) -(* ********************************************************************** *) - -include "freescale/memory_struct.ma". -include "num/word16.ma". -include "common/option.ma". -include "common/list.ma". - -(* ********************* *) -(* MEMORIA E DESCRITTORE *) -(* ********************* *) - -(* tutta la memoria non installata *) -ndefinition mt_out_of_bound_memory ≝ -let lev4 ≝ array_16T ? - MEM_OUT_OF_BOUND MEM_OUT_OF_BOUND MEM_OUT_OF_BOUND MEM_OUT_OF_BOUND - MEM_OUT_OF_BOUND MEM_OUT_OF_BOUND MEM_OUT_OF_BOUND MEM_OUT_OF_BOUND - MEM_OUT_OF_BOUND MEM_OUT_OF_BOUND MEM_OUT_OF_BOUND MEM_OUT_OF_BOUND - MEM_OUT_OF_BOUND MEM_OUT_OF_BOUND MEM_OUT_OF_BOUND MEM_OUT_OF_BOUND - in -let lev3 ≝ array_16T ? - lev4 lev4 lev4 lev4 lev4 lev4 lev4 lev4 - lev4 lev4 lev4 lev4 lev4 lev4 lev4 lev4 - in -let lev2 ≝ array_16T ? - lev3 lev3 lev3 lev3 lev3 lev3 lev3 lev3 - lev3 lev3 lev3 lev3 lev3 lev3 lev3 lev3 - in -let lev1 ≝ array_16T ? - lev2 lev2 lev2 lev2 lev2 lev2 lev2 lev2 - lev2 lev2 lev2 lev2 lev2 lev2 lev2 lev2 - in -lev1. - -(* tutta la memoria a 0 *) -ndefinition mt_zero_memory ≝ -let lev4 ≝ array_16T ? - (mk_byte8 x0 x0) (mk_byte8 x0 x0) (mk_byte8 x0 x0) (mk_byte8 x0 x0) - (mk_byte8 x0 x0) (mk_byte8 x0 x0) (mk_byte8 x0 x0) (mk_byte8 x0 x0) - (mk_byte8 x0 x0) (mk_byte8 x0 x0) (mk_byte8 x0 x0) (mk_byte8 x0 x0) - (mk_byte8 x0 x0) (mk_byte8 x0 x0) (mk_byte8 x0 x0) (mk_byte8 x0 x0) - in -let lev3 ≝ array_16T ? - lev4 lev4 lev4 lev4 lev4 lev4 lev4 lev4 - lev4 lev4 lev4 lev4 lev4 lev4 lev4 lev4 - in -let lev2 ≝ array_16T ? - lev3 lev3 lev3 lev3 lev3 lev3 lev3 lev3 - lev3 lev3 lev3 lev3 lev3 lev3 lev3 lev3 - in -let lev1 ≝ array_16T ? - lev2 lev2 lev2 lev2 lev2 lev2 lev2 lev2 - lev2 lev2 lev2 lev2 lev2 lev2 lev2 lev2 - in -lev1. - -(* visita di un albero da 64KB di elementi: ln16(65536)=4 passaggi *) -ndefinition mt_visit ≝ -λT:Type.λdata:Array16T (Array16T (Array16T (Array16T T))).λaddr:word16. - match addr with - [ mk_word16 wh wl ⇒ - getn_array16T (b8l wl) ? - (getn_array16T (b8h wl) ? - (getn_array16T (b8l wh) ? - (getn_array16T (b8h wh) ? data))) ]. - -(* scrittura di un elemento in un albero da 64KB *) -ndefinition mt_update ≝ -λT:Type.λdata:Array16T (Array16T (Array16T (Array16T T))).λaddr:word16.λv:T. - match addr with - [ mk_word16 wh wl ⇒ - let lev2 ≝ getn_array16T (b8h wh) ? data in - let lev3 ≝ getn_array16T (b8l wh) ? lev2 in - let lev4 ≝ getn_array16T (b8h wl) ? lev3 in - setn_array16T (b8h wh) ? data - (setn_array16T (b8l wh) ? lev2 - (setn_array16T (b8h wl) ? lev3 - (setn_array16T (b8l wl) T lev4 v))) ]. - -(* scrittura di un range in un albero da 64KB *) -ndefinition mt_update_ranged ≝ -λT:Type.λdata:Array16T (Array16T (Array16T (Array16T T))).λi,s:word16.λv:T. - (* ok i≤s *) - match le_w16 i s with - [ true ⇒ - match i with - [ mk_word16 ih il ⇒ - match s with - [ mk_word16 sh sl ⇒ - let aux_4 ≝ Array16T T in - let aux_3 ≝ Array16T (Array16T T) in - let aux_2 ≝ Array16T (Array16T (Array16T T)) in - - let ilev2 ≝ getn_array16T (b8h ih) aux_2 data in - let ilev3 ≝ getn_array16T (b8l ih) aux_3 ilev2 in - let ilev4 ≝ getn_array16T (b8h il) aux_4 ilev3 in - - let slev2 ≝ getn_array16T (b8h sh) aux_2 data in - let slev3 ≝ getn_array16T (b8l sh) aux_3 slev2 in - let slev4 ≝ getn_array16T (b8h sl) aux_4 slev3 in - - let vlev4 ≝ array_16T T v v v v v v v v v v v v v v v v in - let vlev3 ≝ array_16T aux_4 vlev4 vlev4 vlev4 vlev4 vlev4 vlev4 vlev4 vlev4 - vlev4 vlev4 vlev4 vlev4 vlev4 vlev4 vlev4 vlev4 in - let vlev2 ≝ array_16T aux_3 vlev3 vlev3 vlev3 vlev3 vlev3 vlev3 vlev3 vlev3 - vlev3 vlev3 vlev3 vlev3 vlev3 vlev3 vlev3 vlev3 in - - match eq_ex (b8h ih) (b8h sh) with - [ true ⇒ match eq_ex (b8l ih) (b8l sh) with - [ true ⇒ match eq_ex (b8h il) (b8h sl) with - (* caso 0x...(X) a 0x...(Y) *) - [ true ⇒ setn_array16T (b8h ih) aux_2 data - (setn_array16T (b8l ih) aux_3 ilev2 - (setn_array16T (b8h il) aux_4 ilev3 - (* cambio a partire da livello 4 *) - (setmn_array16T (b8l il) (b8l sl) T ilev4 v))) (* ...X,...Y *) - (* caso 0x..(X1)(X2) a 0x..(Y1)(Y2) *) - | false ⇒ setn_array16T (b8h ih) aux_2 data - (setn_array16T (b8l ih) aux_3 ilev2 - (* cambio a partire da livello 3 *) - (setn_array16T (b8h sl) aux_4 (* ..(Y1)0,..(Y1)(Y2) *) - (setmn_array16T_succ_pred (b8h il) (b8h sl) aux_4 (* ..(X1+1).,..(Y1-1). *) - (setn_array16T (b8h il) aux_4 ilev3 - (setmn_array16T (b8l il) xF T ilev4 v)) (* ..(X1)(X2),..(X1)F *) - vlev4) - (setmn_array16T x0 (b8l sl) T slev4 v))) ] - (* caso 0x.(X1)(X2)(X3) a 0x..(Y1)(Y2)(Y3) *) - | false ⇒ setn_array16T (b8h ih) aux_2 data - (* cambio a partire da livello 2 *) - (setn_array16T (b8l sh) aux_3 - (setmn_array16T_succ_pred (b8l ih) (b8l sh) aux_3 (* .(X1+1)..,.(Y1-1).. *) - (setn_array16T (b8l ih) aux_3 ilev2 - (setmn_array16T_succ (b8h il) aux_4 (* .(X1)(X2+1).,.(X1)F. *) - (setn_array16T (b8h il) aux_4 ilev3 - (setmn_array16T (b8l il) xF T ilev4 v)) (* .(X1)(X2)(X3),.(X1)(X2)F *) - vlev4)) - vlev3) - (setmn_array16T_pred (b8h sl) aux_4 (* .(Y1)0.,.(Y1)(Y2-1). *) - (setn_array16T (b8h sl) aux_4 slev3 - (setmn_array16T x0 (b8l sl) T slev4 v)) (* .(Y1)(Y2)0,.(Y1)(Y2)(Y3) *) - vlev4)) - ] - (* caso 0x(X1)(X2)(X3)(X4) a 0x(Y1)(Y2)(Y3)(Y4) *) - | false ⇒ setn_array16T (b8h sh) aux_2 - (setmn_array16T_succ_pred (b8h ih) (b8h sh) aux_2 (* (X+1)...,(Y-1)... *) - (setn_array16T (b8h ih) aux_2 data - (setmn_array16T_succ (b8l ih) aux_3 (* (X1)(X2+1)..,(X1)F.. *) - (setn_array16T (b8l ih) aux_3 ilev2 - (setmn_array16T_succ (b8h il) aux_4 (* (X1)(X2)(X3+1).,(X1)(X2)F. *) - (setn_array16T (b8h il) aux_4 ilev3 - (setmn_array16T (b8l il) xF T ilev4 v)) (* (X1)(X2)(X3)(X4),(X1)(X2)(X3)F *) - vlev4)) - vlev3)) - vlev2) - (setmn_array16T_pred (b8l sh) aux_3 (* (Y1)0..,(Y1)(Y2-1).. *) - (setn_array16T (b8l sh) aux_3 slev2 - (setmn_array16T_pred (b8h sl) aux_4 (* (Y1)(Y2)0.,(Y1)(Y2)(Y3-1). *) - (setn_array16T (b8h sl) aux_4 slev3 - (setmn_array16T x0 (b8l sl) T slev4 v)) (* (Y1)(Y2)(Y3)0,(Y1)(Y2)(Y3)(Y4) *) - vlev4)) - vlev3) ]]] - (* no i>s *) - | false ⇒ data - ]. - -ndefinition mt_chk_get ≝ -λchk:Array16T (Array16T (Array16T (Array16T memory_type))).λaddr:word16. - match mt_visit ? chk addr with - [ MEM_READ_ONLY ⇒ array_8T ? MEM_READ_ONLY MEM_READ_ONLY MEM_READ_ONLY MEM_READ_ONLY MEM_READ_ONLY MEM_READ_ONLY MEM_READ_ONLY MEM_READ_ONLY - | MEM_READ_WRITE ⇒ array_8T ? MEM_READ_WRITE MEM_READ_WRITE MEM_READ_WRITE MEM_READ_WRITE MEM_READ_WRITE MEM_READ_WRITE MEM_READ_WRITE MEM_READ_WRITE - | MEM_OUT_OF_BOUND ⇒ array_8T ? MEM_OUT_OF_BOUND MEM_OUT_OF_BOUND MEM_OUT_OF_BOUND MEM_OUT_OF_BOUND MEM_OUT_OF_BOUND MEM_OUT_OF_BOUND MEM_OUT_OF_BOUND MEM_OUT_OF_BOUND - ]. - -(* scrivi controllando il tipo di memoria *) -ndefinition mt_mem_update ≝ -λmem:Array16T (Array16T (Array16T (Array16T byte8))). -λchk:Array8T memory_type. -λaddr:word16.λv:byte8. - match getn_array8T o0 ? chk with - (* ROM? ok, ma il valore viene perso *) - [ MEM_READ_ONLY ⇒ Some ? mem - (* RAM? ok *) - | MEM_READ_WRITE ⇒ Some ? (mt_update ? mem addr v) - (* NON INSTALLATA? no *) - | MEM_OUT_OF_BOUND ⇒ None ? ]. - -(* leggi controllando il tipo di memoria *) -ndefinition mt_mem_read ≝ -λmem:Array16T (Array16T (Array16T (Array16T byte8))). -λchk:Array16T (Array16T (Array16T (Array16T memory_type))). -λaddr:word16. - match mt_visit ? chk addr with - [ MEM_READ_ONLY ⇒ Some ? (mt_visit ? mem addr) - | MEM_READ_WRITE ⇒ Some ? (mt_visit ? mem addr) - | MEM_OUT_OF_BOUND ⇒ None ? ]. - -(* ************************** *) -(* CARICAMENTO PROGRAMMA/DATI *) -(* ************************** *) - -(* carica a paratire da addr, overflow se si supera 0xFFFF... *) -nlet rec mt_load_from_source_at (old_mem:Array16T (Array16T (Array16T (Array16T byte8)))) - (src:list byte8) (addr:word16) on src ≝ - match src with - (* fine di source: carica da old_mem *) - [ nil ⇒ old_mem - | cons hd tl ⇒ mt_load_from_source_at (mt_update ? old_mem addr hd) tl (plus_w16_d_d addr 〈〈x0,x0〉:〈x0,x1〉〉) - ]. diff --git a/helm/software/matita/contribs/ng_assembly/freescale/status.ma b/helm/software/matita/contribs/ng_assembly/freescale/status.ma index 1354861e2..9eba21d29 100755 --- a/helm/software/matita/contribs/ng_assembly/freescale/status.ma +++ b/helm/software/matita/contribs/ng_assembly/freescale/status.ma @@ -20,7 +20,7 @@ (* *) (* ********************************************************************** *) -include "freescale/memory_abs.ma". +include "memory/memory_abs.ma". include "freescale/opcode_base.ma". (* *********************************** *) diff --git a/helm/software/matita/contribs/ng_assembly/freescale/memory_abs.ma b/helm/software/matita/contribs/ng_assembly/memory/memory_abs.ma similarity index 64% rename from helm/software/matita/contribs/ng_assembly/freescale/memory_abs.ma rename to helm/software/matita/contribs/ng_assembly/memory/memory_abs.ma index 736f4aaea..a9988c492 100755 --- a/helm/software/matita/contribs/ng_assembly/freescale/memory_abs.ma +++ b/helm/software/matita/contribs/ng_assembly/memory/memory_abs.ma @@ -16,13 +16,13 @@ (* Progetto FreeScale *) (* *) (* Sviluppato da: Ing. Cosimo Oliboni, oliboni@cs.unibo.it *) -(* Ultima modifica: 05/08/2009 *) +(* Sviluppo: 2008-2010 *) (* *) (* ********************************************************************** *) -include "freescale/memory_func.ma". -include "freescale/memory_trees.ma". -include "freescale/memory_bits.ma". +include "memory/memory_func.ma". +include "memory/memory_trees.ma". +include "memory/memory_bits.ma". (* ********************************************* *) (* ASTRAZIONE DALL'IMPLEMENTAZIONE DELLA MEMORIA *) @@ -37,17 +37,17 @@ ninductive memory_impl : Type ≝ (* ausiliario per il tipo della memoria *) ndefinition aux_mem_type ≝ λt:memory_impl.match t with - [ MEM_FUNC ⇒ word16 → byte8 - | MEM_TREE ⇒ Array16T (Array16T (Array16T (Array16T byte8))) - | MEM_BITS ⇒ Array16T (Array16T (Array16T (Array16T (Array8T bool)))) + [ MEM_FUNC ⇒ word32 → byte8 + | MEM_TREE ⇒ aux_32B_type byte8 + | MEM_BITS ⇒ aux_32B_type (Array8T bool) ]. (* ausiliario per il tipo del checker *) ndefinition aux_chk_type ≝ λt:memory_impl.match t with - [ MEM_FUNC ⇒ word16 → memory_type - | MEM_TREE ⇒ Array16T (Array16T (Array16T (Array16T memory_type))) - | MEM_BITS ⇒ Array16T (Array16T (Array16T (Array16T (Array8T memory_type)))) + [ MEM_FUNC ⇒ word32 → memory_type + | MEM_TREE ⇒ aux_32B_type memory_type + | MEM_BITS ⇒ aux_32B_type (Array8T memory_type) ]. (* unificazione di out_of_bound_memory *) @@ -76,35 +76,46 @@ ndefinition zero_memory ≝ ndefinition mem_read_abs ≝ λt:memory_impl. match t - return λt.aux_mem_type t → word16 → byte8 + return λt.aux_mem_type t → word32 → byte8 with [ MEM_FUNC ⇒ λm:aux_mem_type MEM_FUNC. - λaddr:word16. + λaddr:word32. m addr | MEM_TREE ⇒ λm:aux_mem_type MEM_TREE. - λaddr:word16. - mt_visit byte8 m addr + λaddr:word32. + mt_visit ? m addr | MEM_BITS ⇒ λm:aux_mem_type MEM_BITS. - λaddr:word16. - byte8_of_bits (mt_visit (Array8T bool) m addr) + λaddr:word32. + byte8_of_bits (mt_visit ? m addr) ]. (* unificazione del chk *) ndefinition chk_get ≝ -λt:memory_impl.λc:aux_chk_type t.λaddr:word16. +λt:memory_impl. match t - return λt.aux_chk_type t → word16 → Array8T memory_type + return λt.aux_chk_type t → word32 → Array8T memory_type with - [ MEM_FUNC ⇒ mf_chk_get - | MEM_TREE ⇒ mt_chk_get - | MEM_BITS ⇒ mb_chk_get - ] c addr. + [ MEM_FUNC ⇒ λc:aux_chk_type MEM_FUNC.λaddr:word32. + match c addr with + [ MEM_READ_ONLY ⇒ mk_Array8T ? MEM_READ_ONLY MEM_READ_ONLY MEM_READ_ONLY MEM_READ_ONLY MEM_READ_ONLY MEM_READ_ONLY MEM_READ_ONLY MEM_READ_ONLY + | MEM_READ_WRITE ⇒ mk_Array8T ? MEM_READ_WRITE MEM_READ_WRITE MEM_READ_WRITE MEM_READ_WRITE MEM_READ_WRITE MEM_READ_WRITE MEM_READ_WRITE MEM_READ_WRITE + | MEM_OUT_OF_BOUND ⇒ mk_Array8T ? MEM_OUT_OF_BOUND MEM_OUT_OF_BOUND MEM_OUT_OF_BOUND MEM_OUT_OF_BOUND MEM_OUT_OF_BOUND MEM_OUT_OF_BOUND MEM_OUT_OF_BOUND MEM_OUT_OF_BOUND + ] + | MEM_TREE ⇒ λc:aux_chk_type MEM_TREE.λaddr:word32. + match mt_visit ? c addr with + [ MEM_READ_ONLY ⇒ mk_Array8T ? MEM_READ_ONLY MEM_READ_ONLY MEM_READ_ONLY MEM_READ_ONLY MEM_READ_ONLY MEM_READ_ONLY MEM_READ_ONLY MEM_READ_ONLY + | MEM_READ_WRITE ⇒ mk_Array8T ? MEM_READ_WRITE MEM_READ_WRITE MEM_READ_WRITE MEM_READ_WRITE MEM_READ_WRITE MEM_READ_WRITE MEM_READ_WRITE MEM_READ_WRITE + | MEM_OUT_OF_BOUND ⇒ mk_Array8T ? MEM_OUT_OF_BOUND MEM_OUT_OF_BOUND MEM_OUT_OF_BOUND MEM_OUT_OF_BOUND MEM_OUT_OF_BOUND MEM_OUT_OF_BOUND MEM_OUT_OF_BOUND MEM_OUT_OF_BOUND + ] + | MEM_BITS ⇒ λc:aux_chk_type MEM_BITS.λaddr:word32. + mt_visit ? c addr + ]. (* unificazione della lettura con chk: mem_read mem chk addr *) ndefinition mem_read ≝ -λt:memory_impl.λm:aux_mem_type t.λc:aux_chk_type t.λaddr:word16. +λt:memory_impl.λm:aux_mem_type t.λc:aux_chk_type t.λaddr:word32. match t - return λt.aux_mem_type t → aux_chk_type t → word16 → option byte8 + return λt.aux_mem_type t → aux_chk_type t → word32 → option byte8 with [ MEM_FUNC ⇒ mf_mem_read | MEM_TREE ⇒ mt_mem_read @@ -115,61 +126,59 @@ ndefinition mem_read ≝ ndefinition mem_read_bit ≝ λt:memory_impl. match t - return λt.aux_mem_type t → aux_chk_type t → word16 → oct → option bool + return λt.aux_mem_type t → aux_chk_type t → word32 → oct → option bool with [ MEM_FUNC ⇒ λm:aux_mem_type MEM_FUNC. λc:aux_chk_type MEM_FUNC. - λaddr:word16. + λaddr:word32. λo:oct. opt_map … (mf_mem_read m c addr) (λb.Some ? (getn_array8T o bool (bits_of_byte8 b))) | MEM_TREE ⇒ λm:aux_mem_type MEM_TREE. λc:aux_chk_type MEM_TREE. - λaddr:word16. + λaddr:word32. λo:oct. opt_map … (mt_mem_read m c addr) (λb.Some ? (getn_array8T o bool (bits_of_byte8 b))) | MEM_BITS ⇒ λm:aux_mem_type MEM_BITS. λc:aux_chk_type MEM_BITS. - λaddr:word16. + λaddr:word32. λo:oct. mb_mem_read_bit m c addr o ]. (* unificazione della scrittura con chk: mem_update mem chk addr val *) ndefinition mem_update ≝ -λt:memory_impl.λm:aux_mem_type t.λc:aux_chk_type t.λaddr:word16.λv:byte8. +λt:memory_impl.λm:aux_mem_type t.λc:aux_chk_type t.λaddr:word32.λv:byte8. match t - return λt.aux_mem_type t → Array8T memory_type → word16 → byte8 → option (aux_mem_type t) + return λt.aux_mem_type t → aux_chk_type t → word32 → byte8 → option (aux_mem_type t) with [ MEM_FUNC ⇒ mf_mem_update | MEM_TREE ⇒ mt_mem_update | MEM_BITS ⇒ mb_mem_update - ] m (chk_get t c addr) addr v. + ] m c addr v. (* unificazione della scrittura di bit con chk: mem_update mem chk addr sub val *) ndefinition mem_update_bit ≝ λt:memory_impl. match t - return λt.aux_mem_type t → aux_chk_type t → word16 → oct → bool → option (aux_mem_type t) + return λt.aux_mem_type t → aux_chk_type t → word32 → oct → bool → option (aux_mem_type t) with [ MEM_FUNC ⇒ λm:aux_mem_type MEM_FUNC. λc:aux_chk_type MEM_FUNC. - λaddr:word16. + λaddr:word32. λo:oct. λv:bool. - opt_map … (mf_mem_read m c addr) - (λb.mf_mem_update m (chk_get MEM_FUNC c addr) addr (byte8_of_bits (setn_array8T o bool (bits_of_byte8 b) v))) + mf_mem_update m c addr (byte8_of_bits (setn_array8T o bool (bits_of_byte8 (m addr)) v)) | MEM_TREE ⇒ λm:aux_mem_type MEM_TREE. λc:aux_chk_type MEM_TREE. - λaddr:word16. + λaddr:word32. λo:oct. λv:bool. - opt_map … (mt_mem_read m c addr) - (λb.mt_mem_update m (chk_get MEM_TREE c addr) addr (byte8_of_bits (setn_array8T o bool (bits_of_byte8 b) v))) + mt_mem_update m c addr (byte8_of_bits (setn_array8T o bool (bits_of_byte8 (mt_visit ? m addr)) v)) | MEM_BITS ⇒ λm:aux_mem_type MEM_BITS. λc:aux_chk_type MEM_BITS. - λaddr:word16. + λaddr:word32. λo:oct. λv:bool. mb_mem_update_bit m c addr o v @@ -177,9 +186,9 @@ ndefinition mem_update_bit ≝ (* unificazione del caricamento: load_from_source_at old_mem source addr *) ndefinition load_from_source_at ≝ -λt:memory_impl.λm:aux_mem_type t.λl:list byte8.λaddr:word16. +λt:memory_impl.λm:aux_mem_type t.λl:list byte8.λaddr:word32. match t - return λt.aux_mem_type t → list byte8 → word16 → aux_mem_type t + return λt.aux_mem_type t → list byte8 → word32 → aux_mem_type t with [ MEM_FUNC ⇒ mf_load_from_source_at | MEM_TREE ⇒ mt_load_from_source_at @@ -190,20 +199,23 @@ ndefinition load_from_source_at ≝ ndefinition check_update_ranged ≝ λt:memory_impl. match t - return λt.aux_chk_type t → word16 → word16 → memory_type → aux_chk_type t + return λt.aux_chk_type t → word32 → word16 → memory_type → aux_chk_type t with [ MEM_FUNC ⇒ λc:aux_chk_type MEM_FUNC. - λinf,sup:word16. + λaddr:word32. + λrange:word16. λv:memory_type. - mf_check_update_ranged c inf sup v + mf_check_update_ranged c addr range v | MEM_TREE ⇒ λc:aux_chk_type MEM_TREE. - λinf,sup:word16. + λaddr:word32. + λrange:word16. λv:memory_type. - mt_update_ranged memory_type c inf sup v + mt_update_ranged ? c addr ? (w16_to_recw16 range) v | MEM_BITS ⇒ λc:aux_chk_type MEM_BITS. - λinf,sup:word16. + λaddr:word32. + λrange:word16. λv:memory_type. - mt_update_ranged (Array8T memory_type) c inf sup (array_8T memory_type v v v v v v v v) + mt_update_ranged ? c addr ? (w16_to_recw16 range) (mk_Array8T ? v v v v v v v v) ]. (* unificazione dell'impostazione dei bit: chk_update_bit chk addr sub v *) @@ -211,20 +223,20 @@ ndefinition check_update_ranged ≝ ndefinition check_update_bit ≝ λt:memory_impl. match t - return λt.aux_chk_type t → word16 → oct → memory_type → aux_chk_type t + return λt.aux_chk_type t → word32 → oct → memory_type → aux_chk_type t with [ MEM_FUNC ⇒ λc:aux_chk_type MEM_FUNC. - λaddr:word16. + λaddr:word32. λo:oct. λv:memory_type. c | MEM_TREE ⇒ λc:aux_chk_type MEM_TREE. - λaddr:word16. + λaddr:word32. λo:oct. λv:memory_type. c | MEM_BITS ⇒ λc:aux_chk_type MEM_BITS. - λaddr:word16. + λaddr:word32. λo:oct. λv:memory_type. mb_chk_update_bit c addr o v diff --git a/helm/software/matita/contribs/ng_assembly/freescale/memory_bits.ma b/helm/software/matita/contribs/ng_assembly/memory/memory_bits.ma similarity index 55% rename from helm/software/matita/contribs/ng_assembly/freescale/memory_bits.ma rename to helm/software/matita/contribs/ng_assembly/memory/memory_bits.ma index c49be931a..396ad9a07 100755 --- a/helm/software/matita/contribs/ng_assembly/freescale/memory_bits.ma +++ b/helm/software/matita/contribs/ng_assembly/memory/memory_bits.ma @@ -16,11 +16,11 @@ (* Progetto FreeScale *) (* *) (* Sviluppato da: Ing. Cosimo Oliboni, oliboni@cs.unibo.it *) -(* Ultima modifica: 05/08/2009 *) +(* Sviluppo: 2008-2010 *) (* *) (* ********************************************************************** *) -include "freescale/memory_trees.ma". +include "memory/memory_trees.ma". (* ********************* *) (* MEMORIA E DESCRITTORE *) @@ -28,124 +28,63 @@ include "freescale/memory_trees.ma". (* tutta la memoria non installata *) ndefinition mb_out_of_bound_memory ≝ -let base ≝ array_8T memory_type MEM_OUT_OF_BOUND MEM_OUT_OF_BOUND MEM_OUT_OF_BOUND MEM_OUT_OF_BOUND - MEM_OUT_OF_BOUND MEM_OUT_OF_BOUND MEM_OUT_OF_BOUND MEM_OUT_OF_BOUND in -let lev4 ≝ array_16T ? - base base base base base base base base - base base base base base base base base - in -let lev3 ≝ array_16T ? - lev4 lev4 lev4 lev4 lev4 lev4 lev4 lev4 - lev4 lev4 lev4 lev4 lev4 lev4 lev4 lev4 - in -let lev2 ≝ array_16T ? - lev3 lev3 lev3 lev3 lev3 lev3 lev3 lev3 - lev3 lev3 lev3 lev3 lev3 lev3 lev3 lev3 - in -let lev1 ≝ array_16T ? - lev2 lev2 lev2 lev2 lev2 lev2 lev2 lev2 - lev2 lev2 lev2 lev2 lev2 lev2 lev2 lev2 - in -lev1. + aux_32B_filler ? + (mk_Array8T ? MEM_OUT_OF_BOUND MEM_OUT_OF_BOUND MEM_OUT_OF_BOUND MEM_OUT_OF_BOUND + MEM_OUT_OF_BOUND MEM_OUT_OF_BOUND MEM_OUT_OF_BOUND MEM_OUT_OF_BOUND). (* tutta la memoria a 0 *) ndefinition mb_zero_memory ≝ -let base ≝ array_8T bool false false false false false false false false in -let lev4 ≝ array_16T ? - base base base base base base base base - base base base base base base base base - in -let lev3 ≝ array_16T ? - lev4 lev4 lev4 lev4 lev4 lev4 lev4 lev4 - lev4 lev4 lev4 lev4 lev4 lev4 lev4 lev4 - in -let lev2 ≝ array_16T ? - lev3 lev3 lev3 lev3 lev3 lev3 lev3 lev3 - lev3 lev3 lev3 lev3 lev3 lev3 lev3 lev3 - in -let lev1 ≝ array_16T ? - lev2 lev2 lev2 lev2 lev2 lev2 lev2 lev2 - lev2 lev2 lev2 lev2 lev2 lev2 lev2 lev2 - in -lev1. + aux_32B_filler ? (mk_Array8T ? false false false false false false false false). (* scrivi bit controllando il tipo di memoria *) ndefinition mb_mem_update_bit ≝ -λmem:Array16T (Array16T (Array16T (Array16T (Array8T bool)))). -λchk:Array16T (Array16T (Array16T (Array16T (Array8T memory_type)))). -λaddr:word16.λsub:oct.λv:bool. - match getn_array8T sub memory_type (mt_visit (Array8T memory_type) chk addr) with +λmem:aux_32B_type (Array8T bool). +λchk:aux_32B_type (Array8T memory_type). +λaddr:word32.λsub:oct.λv:bool. + match getn_array8T sub ? (mt_visit ? chk addr) with (* ROM? ok, ma il valore viene perso *) [ MEM_READ_ONLY ⇒ Some ? mem (* RAM? ok *) - | MEM_READ_WRITE ⇒ Some ? (mt_update (Array8T bool) mem addr (setn_array8T sub bool (mt_visit (Array8T bool) mem addr) v)) + | MEM_READ_WRITE ⇒ Some ? (mt_update ? mem addr (setn_array8T sub ? (mt_visit ? mem addr) v)) (* NON INSTALLATA? no *) | MEM_OUT_OF_BOUND ⇒ None ? ]. -(* scrivi tipo di bit *) -ndefinition mb_chk_update_bit ≝ -λchk:Array16T (Array16T (Array16T (Array16T (Array8T memory_type)))). -λaddr:word16.λsub:oct.λv:memory_type. - mt_update (Array8T memory_type) chk addr (setn_array8T sub memory_type (mt_visit (Array8T memory_type) chk addr) v). - -(* leggi bit controllando il tipo di memoria *) -ndefinition mb_mem_read_bit ≝ -λmem:Array16T (Array16T (Array16T (Array16T (Array8T bool)))). -λchk:Array16T (Array16T (Array16T (Array16T (Array8T memory_type)))). -λaddr:word16.λsub:oct. - match getn_array8T sub memory_type (mt_visit (Array8T memory_type) chk addr) with - (* ROM? ok, ma il valore viene perso *) - [ MEM_READ_ONLY ⇒ Some ? (getn_array8T sub bool (mt_visit (Array8T bool) mem addr)) - (* RAM? ok *) - | MEM_READ_WRITE ⇒ Some ? (getn_array8T sub bool (mt_visit (Array8T bool) mem addr)) - (* NON INSTALLATA? no *) - | MEM_OUT_OF_BOUND ⇒ None ? ]. - -ndefinition mb_chk_get ≝ -λchk:Array16T (Array16T (Array16T (Array16T (Array8T memory_type)))).λaddr:word16. -let c ≝ mt_visit (Array8T memory_type) chk addr in -array_8T ? (getn_array8T o7 ? c) (getn_array8T o6 ? c) - (getn_array8T o5 ? c) (getn_array8T o4 ? c) - (getn_array8T o3 ? c) (getn_array8T o2 ? c) - (getn_array8T o1 ? c) (getn_array8T o0 ? c). - -(* scrivi controllando il tipo di memoria *) -(* NB: devono esistere tutti i bit *) ndefinition mb_mem_update ≝ -λmem:Array16T (Array16T (Array16T (Array16T (Array8T bool)))). -λchk:Array8T memory_type. -λaddr:word16.λv:byte8. +λmem:aux_32B_type (Array8T bool). +λchk:aux_32B_type (Array8T memory_type). +λaddr:word32.λv:byte8. let old_value ≝ mt_visit (Array8T bool) mem addr in let new_value ≝ bits_of_byte8 v in -let newbit0 ≝ match getn_array8T o0 memory_type chk with +let memtypes ≝ mt_visit (Array8T memory_type) chk addr in +let newbit0 ≝ match getn_array8T o0 memory_type memtypes with [ MEM_READ_ONLY ⇒ Some bool (getn_array8T o0 bool old_value) | MEM_READ_WRITE ⇒ Some bool (getn_array8T o0 bool new_value) | MEM_OUT_OF_BOUND ⇒ None bool ] in -let newbit1 ≝ match getn_array8T o1 memory_type chk with +let newbit1 ≝ match getn_array8T o1 memory_type memtypes with [ MEM_READ_ONLY ⇒ Some bool (getn_array8T o1 bool old_value) | MEM_READ_WRITE ⇒ Some bool (getn_array8T o1 bool new_value) | MEM_OUT_OF_BOUND ⇒ None bool ] in -let newbit2 ≝ match getn_array8T o2 memory_type chk with +let newbit2 ≝ match getn_array8T o2 memory_type memtypes with [ MEM_READ_ONLY ⇒ Some bool (getn_array8T o2 bool old_value) | MEM_READ_WRITE ⇒ Some bool (getn_array8T o2 bool new_value) | MEM_OUT_OF_BOUND ⇒ None bool ] in -let newbit3 ≝ match getn_array8T o3 memory_type chk with +let newbit3 ≝ match getn_array8T o3 memory_type memtypes with [ MEM_READ_ONLY ⇒ Some bool (getn_array8T o3 bool old_value) | MEM_READ_WRITE ⇒ Some bool (getn_array8T o3 bool new_value) | MEM_OUT_OF_BOUND ⇒ None bool ] in -let newbit4 ≝ match getn_array8T o4 memory_type chk with +let newbit4 ≝ match getn_array8T o4 memory_type memtypes with [ MEM_READ_ONLY ⇒ Some bool (getn_array8T o4 bool old_value) | MEM_READ_WRITE ⇒ Some bool (getn_array8T o4 bool new_value) | MEM_OUT_OF_BOUND ⇒ None bool ] in -let newbit5 ≝ match getn_array8T o5 memory_type chk with +let newbit5 ≝ match getn_array8T o5 memory_type memtypes with [ MEM_READ_ONLY ⇒ Some bool (getn_array8T o5 bool old_value) | MEM_READ_WRITE ⇒ Some bool (getn_array8T o5 bool new_value) | MEM_OUT_OF_BOUND ⇒ None bool ] in -let newbit6 ≝ match getn_array8T o6 memory_type chk with +let newbit6 ≝ match getn_array8T o6 memory_type memtypes with [ MEM_READ_ONLY ⇒ Some bool (getn_array8T o6 bool old_value) | MEM_READ_WRITE ⇒ Some bool (getn_array8T o6 bool new_value) | MEM_OUT_OF_BOUND ⇒ None bool ] in -let newbit7 ≝ match getn_array8T o7 memory_type chk with +let newbit7 ≝ match getn_array8T o7 memory_type memtypes 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 @@ -157,45 +96,64 @@ let newbit7 ≝ match getn_array8T o7 memory_type chk with (λ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)))))))))). + (λnb7.Some ? (mt_update ? mem addr (mk_Array8T bool nb7 nb6 nb5 nb4 nb3 nb2 nb1 nb0)))))))))). + +(* scrivi tipo di bit *) +ndefinition mb_chk_update_bit ≝ +λchk:aux_32B_type (Array8T memory_type). +λaddr:word32.λsub:oct.λv:memory_type. + mt_update ? chk addr (setn_array8T sub ? (mt_visit ? chk addr) v). + +(* leggi bit controllando il tipo di memoria *) +ndefinition mb_mem_read_bit ≝ +λmem:aux_32B_type (Array8T bool). +λchk:aux_32B_type (Array8T memory_type). +λaddr:word32.λsub:oct. + match getn_array8T sub ? (mt_visit ? chk addr) with + (* ROM? ok, ma il valore viene perso *) + [ MEM_READ_ONLY ⇒ Some ? (getn_array8T sub ? (mt_visit ? mem addr)) + (* RAM? ok *) + | MEM_READ_WRITE ⇒ Some ? (getn_array8T sub ? (mt_visit ? mem addr)) + (* NON INSTALLATA? no *) + | MEM_OUT_OF_BOUND ⇒ None ? ]. (* leggi controllando il tipo di memoria *) (* NB: devono esistere tutti i bit *) ndefinition mb_mem_read ≝ -λmem:Array16T (Array16T (Array16T (Array16T (Array8T bool)))). -λchk:Array16T (Array16T (Array16T (Array16T (Array8T memory_type)))). -λaddr:word16. -let bit_types ≝ mt_visit (Array8T memory_type) chk addr in +λmem:aux_32B_type (Array8T bool). +λchk:aux_32B_type (Array8T memory_type). +λaddr:word32. let value ≝ mt_visit (Array8T bool) mem addr in -let newbit0 ≝ match getn_array8T o0 memory_type bit_types with +let memtypes ≝ mt_visit (Array8T memory_type) chk addr in +let newbit0 ≝ match getn_array8T o0 memory_type memtypes with [ MEM_READ_ONLY ⇒ Some bool (getn_array8T o0 bool value) | MEM_READ_WRITE ⇒ Some bool (getn_array8T o0 bool value) | MEM_OUT_OF_BOUND ⇒ None bool ] in -let newbit1 ≝ match getn_array8T o1 memory_type bit_types with +let newbit1 ≝ match getn_array8T o1 memory_type memtypes with [ MEM_READ_ONLY ⇒ Some bool (getn_array8T o1 bool value) | MEM_READ_WRITE ⇒ Some bool (getn_array8T o1 bool value) | MEM_OUT_OF_BOUND ⇒ None bool ] in -let newbit2 ≝ match getn_array8T o2 memory_type bit_types with +let newbit2 ≝ match getn_array8T o2 memory_type memtypes with [ MEM_READ_ONLY ⇒ Some bool (getn_array8T o2 bool value) | MEM_READ_WRITE ⇒ Some bool (getn_array8T o2 bool value) | MEM_OUT_OF_BOUND ⇒ None bool ] in -let newbit3 ≝ match getn_array8T o3 memory_type bit_types with +let newbit3 ≝ match getn_array8T o3 memory_type memtypes with [ MEM_READ_ONLY ⇒ Some bool (getn_array8T o3 bool value) | MEM_READ_WRITE ⇒ Some bool (getn_array8T o3 bool value) | MEM_OUT_OF_BOUND ⇒ None bool ] in -let newbit4 ≝ match getn_array8T o4 memory_type bit_types with +let newbit4 ≝ match getn_array8T o4 memory_type memtypes with [ MEM_READ_ONLY ⇒ Some bool (getn_array8T o4 bool value) | MEM_READ_WRITE ⇒ Some bool (getn_array8T o4 bool value) | MEM_OUT_OF_BOUND ⇒ None bool ] in -let newbit5 ≝ match getn_array8T o5 memory_type bit_types with +let newbit5 ≝ match getn_array8T o5 memory_type memtypes with [ MEM_READ_ONLY ⇒ Some bool (getn_array8T o5 bool value) | MEM_READ_WRITE ⇒ Some bool (getn_array8T o5 bool value) | MEM_OUT_OF_BOUND ⇒ None bool ] in -let newbit6 ≝ match getn_array8T o6 memory_type bit_types with +let newbit6 ≝ match getn_array8T o6 memory_type memtypes with [ MEM_READ_ONLY ⇒ Some bool (getn_array8T o6 bool value) | MEM_READ_WRITE ⇒ Some bool (getn_array8T o6 bool value) | MEM_OUT_OF_BOUND ⇒ None bool ] in -let newbit7 ≝ match getn_array8T o7 memory_type bit_types with +let newbit7 ≝ match getn_array8T o7 memory_type memtypes 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 @@ -207,17 +165,17 @@ let newbit7 ≝ match getn_array8T o7 memory_type bit_types with (λ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)))))))))). + (λnb7.Some ? (byte8_of_bits (mk_Array8T bool nb7 nb6 nb5 nb4 nb3 nb2 nb1 nb0)))))))))). (* ************************** *) (* CARICAMENTO PROGRAMMA/DATI *) (* ************************** *) (* carica a paratire da addr, scartando source (pescando da old_mem) se si supera 0xFFFF... *) -nlet rec mb_load_from_source_at (old_mem:Array16T (Array16T (Array16T (Array16T (Array8T bool))))) - (src:list byte8) (addr:word16) on src ≝ +nlet rec mb_load_from_source_at (old_mem:aux_32B_type (Array8T bool)) + (src:list byte8) (addr:word32) on src ≝ match src with (* fine di source: carica da old_mem *) [ nil ⇒ old_mem - | cons hd tl ⇒ mb_load_from_source_at (mt_update ? old_mem addr (bits_of_byte8 hd)) tl (plus_w16_d_d addr 〈〈x0,x0〉:〈x0,x1〉〉) + | cons hd tl ⇒ mb_load_from_source_at (mt_update ? old_mem addr (bits_of_byte8 hd)) tl (succ_w32 addr) ]. diff --git a/helm/software/matita/contribs/ng_assembly/freescale/memory_func.ma b/helm/software/matita/contribs/ng_assembly/memory/memory_func.ma similarity index 67% rename from helm/software/matita/contribs/ng_assembly/freescale/memory_func.ma rename to helm/software/matita/contribs/ng_assembly/memory/memory_func.ma index 831c75a1a..96c2ee742 100755 --- a/helm/software/matita/contribs/ng_assembly/freescale/memory_func.ma +++ b/helm/software/matita/contribs/ng_assembly/memory/memory_func.ma @@ -16,12 +16,12 @@ (* Progetto FreeScale *) (* *) (* Sviluppato da: Ing. Cosimo Oliboni, oliboni@cs.unibo.it *) -(* Ultima modifica: 05/08/2009 *) +(* Sviluppo: 2008-2010 *) (* *) (* ********************************************************************** *) -include "freescale/memory_struct.ma". -include "num/word16.ma". +include "memory/memory_struct.ma". +include "num/word32.ma". include "common/option.ma". include "common/list.ma". @@ -31,39 +31,31 @@ include "common/list.ma". (* (mf_check_update_ranged chk inf sup mode) = setta tipo memoria *) ndefinition mf_check_update_ranged ≝ -λf:word16 → memory_type.λinf.λsup.λv. - λx.match inrange_w16 x inf sup with +λf:word32 → memory_type.λaddr:word32.λrange:word16.λv. + λx.match inrange_w32 x addr (plus_w32_d_d addr 〈〈〈x0,x0〉:〈x0,x0〉〉.range〉) with [ true ⇒ v | false ⇒ f x ]. (* tutta la memoria non installata *) -ndefinition mf_out_of_bound_memory ≝ λ_:word16.MEM_OUT_OF_BOUND. - -ndefinition mf_chk_get ≝ -λc:word16 → memory_type.λa:word16. - match c a with - [ MEM_READ_ONLY ⇒ array_8T ? MEM_READ_ONLY MEM_READ_ONLY MEM_READ_ONLY MEM_READ_ONLY MEM_READ_ONLY MEM_READ_ONLY MEM_READ_ONLY MEM_READ_ONLY - | MEM_READ_WRITE ⇒ array_8T ? MEM_READ_WRITE MEM_READ_WRITE MEM_READ_WRITE MEM_READ_WRITE MEM_READ_WRITE MEM_READ_WRITE MEM_READ_WRITE MEM_READ_WRITE - | MEM_OUT_OF_BOUND ⇒ array_8T ? MEM_OUT_OF_BOUND MEM_OUT_OF_BOUND MEM_OUT_OF_BOUND MEM_OUT_OF_BOUND MEM_OUT_OF_BOUND MEM_OUT_OF_BOUND MEM_OUT_OF_BOUND MEM_OUT_OF_BOUND - ]. +ndefinition mf_out_of_bound_memory ≝ λ_:word32.MEM_OUT_OF_BOUND. (* (mf_mem_update mem checked addr val) = scrivi controllando il tipo di memoria *) ndefinition mf_mem_update ≝ -λf:word16 → byte8.λc:Array8T memory_type.λa:word16.λv:byte8. - match getn_array8T o0 ? c with +λf:word32 → byte8.λc:word32 → memory_type.λa:word32.λv:byte8. + match c a with (* ROM? ok, ma il valore viene perso *) [ MEM_READ_ONLY ⇒ Some ? f (* RAM? ok *) - | MEM_READ_WRITE ⇒ Some ? (λx.match eq_w16 x a with [ true ⇒ v | false ⇒ f x ]) + | MEM_READ_WRITE ⇒ Some ? (λx.match eq_w32 x a with [ true ⇒ v | false ⇒ f x ]) (* NON INSTALLATA? no *) | MEM_OUT_OF_BOUND ⇒ None ? ]. (* tutta la memoria a 0 *) -ndefinition mf_zero_memory ≝ λ_:word16.〈x0,x0〉. +ndefinition mf_zero_memory ≝ λ_:word32.〈x0,x0〉. (* (mf_mem_read mem check addr) = leggi controllando il tipo di memoria *) ndefinition mf_mem_read ≝ -λf:word16 → byte8.λc:word16 → memory_type.λa. +λf:word32 → byte8.λc:word32 → memory_type.λa. match c a with [ MEM_READ_ONLY ⇒ Some ? (f a) | MEM_READ_WRITE ⇒ Some ? (f a) @@ -74,14 +66,14 @@ ndefinition mf_mem_read ≝ (* ************************** *) (* carica a paratire da addr, overflow se si supera 0xFFFF... *) -nlet rec mf_load_from_source_at (old_mem:word16 → byte8) (src:list byte8) (addr:word16) on src ≝ +nlet rec mf_load_from_source_at (old_mem:word32 → byte8) (src:list byte8) (addr:word32) on src ≝ match src with (* fine di source: carica da old_mem *) [ nil ⇒ old_mem - | cons hd tl ⇒ λx:word16.match eq_w16 addr x with + | cons hd tl ⇒ λx:word32.match eq_w32 addr x with (* la locazione corrisponde al punto corrente di source *) [ true ⇒ hd (* la locazione e' piu' avanti? ricorsione *) - | false ⇒ (mf_load_from_source_at old_mem tl (plus_w16_d_d addr 〈〈x0,x0〉:〈x0,x1〉〉)) x + | false ⇒ (mf_load_from_source_at old_mem tl (plus_w32_d_d addr 〈〈〈x0,x0〉:〈x0,x0〉〉.〈〈x0,x0〉:〈x0,x1〉〉〉)) x ] ]. diff --git a/helm/software/matita/contribs/ng_assembly/memory/memory_struct.ma b/helm/software/matita/contribs/ng_assembly/memory/memory_struct.ma new file mode 100755 index 000000000..0e023b5a1 --- /dev/null +++ b/helm/software/matita/contribs/ng_assembly/memory/memory_struct.ma @@ -0,0 +1,659 @@ +(**************************************************************************) +(* ___ *) +(* ||M|| *) +(* ||A|| A project by Andrea Asperti *) +(* ||T|| *) +(* ||I|| Developers: *) +(* ||T|| The HELM team. *) +(* ||A|| http://helm.cs.unibo.it *) +(* \ / *) +(* \ / This file is distributed under the terms of the *) +(* v GNU General Public License Version 2 *) +(* *) +(**************************************************************************) + +(* ********************************************************************** *) +(* Progetto FreeScale *) +(* *) +(* Sviluppato da: Ing. Cosimo Oliboni, oliboni@cs.unibo.it *) +(* Sviluppo: 2008-2010 *) +(* *) +(* ********************************************************************** *) + +include "num/oct.ma". +include "num/byte8.ma". + +(* **************************** *) +(* TIPI PER I MODULI DI MEMORIA *) +(* **************************** *) + +(* tipi di memoria:RAM/ROM/non installata *) +ninductive memory_type : Type ≝ + MEM_READ_ONLY: memory_type +| MEM_READ_WRITE: memory_type +| MEM_OUT_OF_BOUND: memory_type. + +(* **************** *) +(* TIPO ARRAY DA 16 *) +(* **************** *) + +(* definizione di un array omogeneo di dimensione 16 *) +nrecord Array16T (T:Type) : Type ≝ +{ a16_1 : T ; a16_2 : T ; a16_3 : T ; a16_4 : T +; a16_5 : T ; a16_6 : T ; a16_7 : T ; a16_8 : T +; a16_9 : T ; a16_10 : T ; a16_11 : T ; a16_12 : T +; a16_13 : T ; a16_14 : T ; a16_15 : T ; a16_16 : T }. + +(* abbiamo gia' gli esadecimali come tipo induttivo quindi: *) +(* posso definire un getter a matrice sull'array *) + +ndefinition getn_array16T ≝ +λn:exadecim.λT:Type.λp:Array16T T. + match n return λn.(Array16T T) → T with + [ x0 ⇒ a16_1 T | x1 ⇒ a16_2 T | x2 ⇒ a16_3 T | x3 ⇒ a16_4 T + | x4 ⇒ a16_5 T | x5 ⇒ a16_6 T | x6 ⇒ a16_7 T | x7 ⇒ a16_8 T + | x8 ⇒ a16_9 T | x9 ⇒ a16_10 T | xA ⇒ a16_11 T | xB ⇒ a16_12 T + | xC ⇒ a16_13 T | xD ⇒ a16_14 T | xE ⇒ a16_15 T | xF ⇒ a16_16 T + ] p. + +(* abbiamo gia' gli esadecimali come tipo induttivo quindi: *) +(* posso definire un setter a matrice sull'array *) +ndefinition setn_array16T ≝ +λn:exadecim.λT:Type.λp:Array16T T.λv:T. +let e00 ≝ (a16_1 T p) in +let e01 ≝ (a16_2 T p) in +let e02 ≝ (a16_3 T p) in +let e03 ≝ (a16_4 T p) in +let e04 ≝ (a16_5 T p) in +let e05 ≝ (a16_6 T p) in +let e06 ≝ (a16_7 T p) in +let e07 ≝ (a16_8 T p) in +let e08 ≝ (a16_9 T p) in +let e09 ≝ (a16_10 T p) in +let e10 ≝ (a16_11 T p) in +let e11 ≝ (a16_12 T p) in +let e12 ≝ (a16_13 T p) in +let e13 ≝ (a16_14 T p) in +let e14 ≝ (a16_15 T p) in +let e15 ≝ (a16_16 T p) in + match n with + [ x0 ⇒ mk_Array16T T v e01 e02 e03 e04 e05 e06 e07 e08 e09 e10 e11 e12 e13 e14 e15 + | x1 ⇒ mk_Array16T T e00 v e02 e03 e04 e05 e06 e07 e08 e09 e10 e11 e12 e13 e14 e15 + | x2 ⇒ mk_Array16T T e00 e01 v e03 e04 e05 e06 e07 e08 e09 e10 e11 e12 e13 e14 e15 + | x3 ⇒ mk_Array16T T e00 e01 e02 v e04 e05 e06 e07 e08 e09 e10 e11 e12 e13 e14 e15 + | x4 ⇒ mk_Array16T T e00 e01 e02 e03 v e05 e06 e07 e08 e09 e10 e11 e12 e13 e14 e15 + | x5 ⇒ mk_Array16T T e00 e01 e02 e03 e04 v e06 e07 e08 e09 e10 e11 e12 e13 e14 e15 + | x6 ⇒ mk_Array16T T e00 e01 e02 e03 e04 e05 v e07 e08 e09 e10 e11 e12 e13 e14 e15 + | x7 ⇒ mk_Array16T T e00 e01 e02 e03 e04 e05 e06 v e08 e09 e10 e11 e12 e13 e14 e15 + | x8 ⇒ mk_Array16T T e00 e01 e02 e03 e04 e05 e06 e07 v e09 e10 e11 e12 e13 e14 e15 + | x9 ⇒ mk_Array16T T e00 e01 e02 e03 e04 e05 e06 e07 e08 v e10 e11 e12 e13 e14 e15 + | xA ⇒ mk_Array16T T e00 e01 e02 e03 e04 e05 e06 e07 e08 e09 v e11 e12 e13 e14 e15 + | xB ⇒ mk_Array16T T e00 e01 e02 e03 e04 e05 e06 e07 e08 e09 e10 v e12 e13 e14 e15 + | xC ⇒ mk_Array16T T e00 e01 e02 e03 e04 e05 e06 e07 e08 e09 e10 e11 v e13 e14 e15 + | xD ⇒ mk_Array16T T e00 e01 e02 e03 e04 e05 e06 e07 e08 e09 e10 e11 e12 v e14 e15 + | xE ⇒ mk_Array16T T e00 e01 e02 e03 e04 e05 e06 e07 e08 e09 e10 e11 e12 e13 v e15 + | xF ⇒ mk_Array16T T e00 e01 e02 e03 e04 e05 e06 e07 e08 e09 e10 e11 e12 e13 e14 v + ]. + +(* abbiamo gia' gli esadecimali come tipo induttivo quindi: *) +(* posso definire un setter multiplo [m,n] a matrice sull'array *) +(* m ≤ n *) +ndefinition setmn_array16T ≝ +λm,n:exadecim.λT:Type.λp:Array16T T.λv:T. +let e00 ≝ (a16_1 T p) in +let e01 ≝ (a16_2 T p) in +let e02 ≝ (a16_3 T p) in +let e03 ≝ (a16_4 T p) in +let e04 ≝ (a16_5 T p) in +let e05 ≝ (a16_6 T p) in +let e06 ≝ (a16_7 T p) in +let e07 ≝ (a16_8 T p) in +let e08 ≝ (a16_9 T p) in +let e09 ≝ (a16_10 T p) in +let e10 ≝ (a16_11 T p) in +let e11 ≝ (a16_12 T p) in +let e12 ≝ (a16_13 T p) in +let e13 ≝ (a16_14 T p) in +let e14 ≝ (a16_15 T p) in +let e15 ≝ (a16_16 T p) in + match m with + [ x0 ⇒ match n with + [ x0 ⇒ mk_Array16T T v e01 e02 e03 e04 e05 e06 e07 e08 e09 e10 e11 e12 e13 e14 e15 + | x1 ⇒ mk_Array16T T v v e02 e03 e04 e05 e06 e07 e08 e09 e10 e11 e12 e13 e14 e15 + | x2 ⇒ mk_Array16T T v v v e03 e04 e05 e06 e07 e08 e09 e10 e11 e12 e13 e14 e15 + | x3 ⇒ mk_Array16T T v v v v e04 e05 e06 e07 e08 e09 e10 e11 e12 e13 e14 e15 + | x4 ⇒ mk_Array16T T v v v v v e05 e06 e07 e08 e09 e10 e11 e12 e13 e14 e15 + | x5 ⇒ mk_Array16T T v v v v v v e06 e07 e08 e09 e10 e11 e12 e13 e14 e15 + | x6 ⇒ mk_Array16T T v v v v v v v e07 e08 e09 e10 e11 e12 e13 e14 e15 + | x7 ⇒ mk_Array16T T v v v v v v v v e08 e09 e10 e11 e12 e13 e14 e15 + | x8 ⇒ mk_Array16T T v v v v v v v v v e09 e10 e11 e12 e13 e14 e15 + | x9 ⇒ mk_Array16T T v v v v v v v v v v e10 e11 e12 e13 e14 e15 + | xA ⇒ mk_Array16T T v v v v v v v v v v v e11 e12 e13 e14 e15 + | xB ⇒ mk_Array16T T v v v v v v v v v v v v e12 e13 e14 e15 + | xC ⇒ mk_Array16T T v v v v v v v v v v v v v e13 e14 e15 + | xD ⇒ mk_Array16T T v v v v v v v v v v v v v v e14 e15 + | xE ⇒ mk_Array16T T v v v v v v v v v v v v v v v e15 + | xF ⇒ mk_Array16T T v v v v v v v v v v v v v v v v ] + | x1 ⇒ match n with + [ x0 ⇒ p + | x1 ⇒ mk_Array16T T e00 v e02 e03 e04 e05 e06 e07 e08 e09 e10 e11 e12 e13 e14 e15 + | x2 ⇒ mk_Array16T T e00 v v e03 e04 e05 e06 e07 e08 e09 e10 e11 e12 e13 e14 e15 + | x3 ⇒ mk_Array16T T e00 v v v e04 e05 e06 e07 e08 e09 e10 e11 e12 e13 e14 e15 + | x4 ⇒ mk_Array16T T e00 v v v v e05 e06 e07 e08 e09 e10 e11 e12 e13 e14 e15 + | x5 ⇒ mk_Array16T T e00 v v v v v e06 e07 e08 e09 e10 e11 e12 e13 e14 e15 + | x6 ⇒ mk_Array16T T e00 v v v v v v e07 e08 e09 e10 e11 e12 e13 e14 e15 + | x7 ⇒ mk_Array16T T e00 v v v v v v v e08 e09 e10 e11 e12 e13 e14 e15 + | x8 ⇒ mk_Array16T T e00 v v v v v v v v e09 e10 e11 e12 e13 e14 e15 + | x9 ⇒ mk_Array16T T e00 v v v v v v v v v e10 e11 e12 e13 e14 e15 + | xA ⇒ mk_Array16T T e00 v v v v v v v v v v e11 e12 e13 e14 e15 + | xB ⇒ mk_Array16T T e00 v v v v v v v v v v v e12 e13 e14 e15 + | xC ⇒ mk_Array16T T e00 v v v v v v v v v v v v e13 e14 e15 + | xD ⇒ mk_Array16T T e00 v v v v v v v v v v v v v e14 e15 + | xE ⇒ mk_Array16T T e00 v v v v v v v v v v v v v v e15 + | xF ⇒ mk_Array16T T e00 v v v v v v v v v v v v v v v ] + | x2 ⇒ match n with + [ x0 ⇒ p | x1 ⇒ p + | x2 ⇒ mk_Array16T T e00 e01 v e03 e04 e05 e06 e07 e08 e09 e10 e11 e12 e13 e14 e15 + | x3 ⇒ mk_Array16T T e00 e01 v v e04 e05 e06 e07 e08 e09 e10 e11 e12 e13 e14 e15 + | x4 ⇒ mk_Array16T T e00 e01 v v v e05 e06 e07 e08 e09 e10 e11 e12 e13 e14 e15 + | x5 ⇒ mk_Array16T T e00 e01 v v v v e06 e07 e08 e09 e10 e11 e12 e13 e14 e15 + | x6 ⇒ mk_Array16T T e00 e01 v v v v v e07 e08 e09 e10 e11 e12 e13 e14 e15 + | x7 ⇒ mk_Array16T T e00 e01 v v v v v v e08 e09 e10 e11 e12 e13 e14 e15 + | x8 ⇒ mk_Array16T T e00 e01 v v v v v v v e09 e10 e11 e12 e13 e14 e15 + | x9 ⇒ mk_Array16T T e00 e01 v v v v v v v v e10 e11 e12 e13 e14 e15 + | xA ⇒ mk_Array16T T e00 e01 v v v v v v v v v e11 e12 e13 e14 e15 + | xB ⇒ mk_Array16T T e00 e01 v v v v v v v v v v e12 e13 e14 e15 + | xC ⇒ mk_Array16T T e00 e01 v v v v v v v v v v v e13 e14 e15 + | xD ⇒ mk_Array16T T e00 e01 v v v v v v v v v v v v e14 e15 + | xE ⇒ mk_Array16T T e00 e01 v v v v v v v v v v v v v e15 + | xF ⇒ mk_Array16T T e00 e01 v v v v v v v v v v v v v v ] + | x3 ⇒ match n with + [ x0 ⇒ p | x1 ⇒ p | x2 ⇒ p + | x3 ⇒ mk_Array16T T e00 e01 e02 v e04 e05 e06 e07 e08 e09 e10 e11 e12 e13 e14 e15 + | x4 ⇒ mk_Array16T T e00 e01 e02 v v e05 e06 e07 e08 e09 e10 e11 e12 e13 e14 e15 + | x5 ⇒ mk_Array16T T e00 e01 e02 v v v e06 e07 e08 e09 e10 e11 e12 e13 e14 e15 + | x6 ⇒ mk_Array16T T e00 e01 e02 v v v v e07 e08 e09 e10 e11 e12 e13 e14 e15 + | x7 ⇒ mk_Array16T T e00 e01 e02 v v v v v e08 e09 e10 e11 e12 e13 e14 e15 + | x8 ⇒ mk_Array16T T e00 e01 e02 v v v v v v e09 e10 e11 e12 e13 e14 e15 + | x9 ⇒ mk_Array16T T e00 e01 e02 v v v v v v v e10 e11 e12 e13 e14 e15 + | xA ⇒ mk_Array16T T e00 e01 e02 v v v v v v v v e11 e12 e13 e14 e15 + | xB ⇒ mk_Array16T T e00 e01 e02 v v v v v v v v v e12 e13 e14 e15 + | xC ⇒ mk_Array16T T e00 e01 e02 v v v v v v v v v v e13 e14 e15 + | xD ⇒ mk_Array16T T e00 e01 e02 v v v v v v v v v v v e14 e15 + | xE ⇒ mk_Array16T T e00 e01 e02 v v v v v v v v v v v v e15 + | xF ⇒ mk_Array16T T e00 e01 e02 v v v v v v v v v v v v v ] + | x4 ⇒ match n with + [ x0 ⇒ p | x1 ⇒ p | x2 ⇒ p | x3 ⇒ p + | x4 ⇒ mk_Array16T T e00 e01 e02 e03 v e05 e06 e07 e08 e09 e10 e11 e12 e13 e14 e15 + | x5 ⇒ mk_Array16T T e00 e01 e02 e03 v v e06 e07 e08 e09 e10 e11 e12 e13 e14 e15 + | x6 ⇒ mk_Array16T T e00 e01 e02 e03 v v v e07 e08 e09 e10 e11 e12 e13 e14 e15 + | x7 ⇒ mk_Array16T T e00 e01 e02 e03 v v v v e08 e09 e10 e11 e12 e13 e14 e15 + | x8 ⇒ mk_Array16T T e00 e01 e02 e03 v v v v v e09 e10 e11 e12 e13 e14 e15 + | x9 ⇒ mk_Array16T T e00 e01 e02 e03 v v v v v v e10 e11 e12 e13 e14 e15 + | xA ⇒ mk_Array16T T e00 e01 e02 e03 v v v v v v v e11 e12 e13 e14 e15 + | xB ⇒ mk_Array16T T e00 e01 e02 e03 v v v v v v v v e12 e13 e14 e15 + | xC ⇒ mk_Array16T T e00 e01 e02 e03 v v v v v v v v v e13 e14 e15 + | xD ⇒ mk_Array16T T e00 e01 e02 e03 v v v v v v v v v v e14 e15 + | xE ⇒ mk_Array16T T e00 e01 e02 e03 v v v v v v v v v v v e15 + | xF ⇒ mk_Array16T T e00 e01 e02 e03 v v v v v v v v v v v v ] + | x5 ⇒ match n with + [ x0 ⇒ p | x1 ⇒ p | x2 ⇒ p | x3 ⇒ p | x4 ⇒ p + | x5 ⇒ mk_Array16T T e00 e01 e02 e03 e04 v e06 e07 e08 e09 e10 e11 e12 e13 e14 e15 + | x6 ⇒ mk_Array16T T e00 e01 e02 e03 e04 v v e07 e08 e09 e10 e11 e12 e13 e14 e15 + | x7 ⇒ mk_Array16T T e00 e01 e02 e03 e04 v v v e08 e09 e10 e11 e12 e13 e14 e15 + | x8 ⇒ mk_Array16T T e00 e01 e02 e03 e04 v v v v e09 e10 e11 e12 e13 e14 e15 + | x9 ⇒ mk_Array16T T e00 e01 e02 e03 e04 v v v v v e10 e11 e12 e13 e14 e15 + | xA ⇒ mk_Array16T T e00 e01 e02 e03 e04 v v v v v v e11 e12 e13 e14 e15 + | xB ⇒ mk_Array16T T e00 e01 e02 e03 e04 v v v v v v v e12 e13 e14 e15 + | xC ⇒ mk_Array16T T e00 e01 e02 e03 e04 v v v v v v v v e13 e14 e15 + | xD ⇒ mk_Array16T T e00 e01 e02 e03 e04 v v v v v v v v v e14 e15 + | xE ⇒ mk_Array16T T e00 e01 e02 e03 e04 v v v v v v v v v v e15 + | xF ⇒ mk_Array16T T e00 e01 e02 e03 e04 v v v v v v v v v v v ] + | x6 ⇒ match n with + [ x0 ⇒ p | x1 ⇒ p | x2 ⇒ p | x3 ⇒ p | x4 ⇒ p | x5 ⇒ p + | x6 ⇒ mk_Array16T T e00 e01 e02 e03 e04 e05 v e07 e08 e09 e10 e11 e12 e13 e14 e15 + | x7 ⇒ mk_Array16T T e00 e01 e02 e03 e04 e05 v v e08 e09 e10 e11 e12 e13 e14 e15 + | x8 ⇒ mk_Array16T T e00 e01 e02 e03 e04 e05 v v v e09 e10 e11 e12 e13 e14 e15 + | x9 ⇒ mk_Array16T T e00 e01 e02 e03 e04 e05 v v v v e10 e11 e12 e13 e14 e15 + | xA ⇒ mk_Array16T T e00 e01 e02 e03 e04 e05 v v v v v e11 e12 e13 e14 e15 + | xB ⇒ mk_Array16T T e00 e01 e02 e03 e04 e05 v v v v v v e12 e13 e14 e15 + | xC ⇒ mk_Array16T T e00 e01 e02 e03 e04 e05 v v v v v v v e13 e14 e15 + | xD ⇒ mk_Array16T T e00 e01 e02 e03 e04 e05 v v v v v v v v e14 e15 + | xE ⇒ mk_Array16T T e00 e01 e02 e03 e04 e05 v v v v v v v v v e15 + | xF ⇒ mk_Array16T T e00 e01 e02 e03 e04 e05 v v v v v v v v v v ] + | x7 ⇒ match n with + [ x0 ⇒ p | x1 ⇒ p | x2 ⇒ p | x3 ⇒ p | x4 ⇒ p | x5 ⇒ p | x6 ⇒ p + | x7 ⇒ mk_Array16T T e00 e01 e02 e03 e04 e05 e06 v e08 e09 e10 e11 e12 e13 e14 e15 + | x8 ⇒ mk_Array16T T e00 e01 e02 e03 e04 e05 e06 v v e09 e10 e11 e12 e13 e14 e15 + | x9 ⇒ mk_Array16T T e00 e01 e02 e03 e04 e05 e06 v v v e10 e11 e12 e13 e14 e15 + | xA ⇒ mk_Array16T T e00 e01 e02 e03 e04 e05 e06 v v v v e11 e12 e13 e14 e15 + | xB ⇒ mk_Array16T T e00 e01 e02 e03 e04 e05 e06 v v v v v e12 e13 e14 e15 + | xC ⇒ mk_Array16T T e00 e01 e02 e03 e04 e05 e06 v v v v v v e13 e14 e15 + | xD ⇒ mk_Array16T T e00 e01 e02 e03 e04 e05 e06 v v v v v v v e14 e15 + | xE ⇒ mk_Array16T T e00 e01 e02 e03 e04 e05 e06 v v v v v v v v e15 + | xF ⇒ mk_Array16T T e00 e01 e02 e03 e04 e05 e06 v v v v v v v v v ] + | x8 ⇒ match n with + [ x0 ⇒ p | x1 ⇒ p | x2 ⇒ p | x3 ⇒ p | x4 ⇒ p | x5 ⇒ p | x6 ⇒ p | x7 ⇒ p + | x8 ⇒ mk_Array16T T e00 e01 e02 e03 e04 e05 e06 e07 v e09 e10 e11 e12 e13 e14 e15 + | x9 ⇒ mk_Array16T T e00 e01 e02 e03 e04 e05 e06 e07 v v e10 e11 e12 e13 e14 e15 + | xA ⇒ mk_Array16T T e00 e01 e02 e03 e04 e05 e06 e07 v v v e11 e12 e13 e14 e15 + | xB ⇒ mk_Array16T T e00 e01 e02 e03 e04 e05 e06 e07 v v v v e12 e13 e14 e15 + | xC ⇒ mk_Array16T T e00 e01 e02 e03 e04 e05 e06 e07 v v v v v e13 e14 e15 + | xD ⇒ mk_Array16T T e00 e01 e02 e03 e04 e05 e06 e07 v v v v v v e14 e15 + | xE ⇒ mk_Array16T T e00 e01 e02 e03 e04 e05 e06 e07 v v v v v v v e15 + | xF ⇒ mk_Array16T T e00 e01 e02 e03 e04 e05 e06 e07 v v v v v v v v ] + | x9 ⇒ match n with + [ x0 ⇒ p | x1 ⇒ p | x2 ⇒ p | x3 ⇒ p | x4 ⇒ p | x5 ⇒ p | x6 ⇒ p | x7 ⇒ p + | x8 ⇒ p + | x9 ⇒ mk_Array16T T e00 e01 e02 e03 e04 e05 e06 e07 e08 v e10 e11 e12 e13 e14 e15 + | xA ⇒ mk_Array16T T e00 e01 e02 e03 e04 e05 e06 e07 e08 v v e11 e12 e13 e14 e15 + | xB ⇒ mk_Array16T T e00 e01 e02 e03 e04 e05 e06 e07 e08 v v v e12 e13 e14 e15 + | xC ⇒ mk_Array16T T e00 e01 e02 e03 e04 e05 e06 e07 e08 v v v v e13 e14 e15 + | xD ⇒ mk_Array16T T e00 e01 e02 e03 e04 e05 e06 e07 e08 v v v v v e14 e15 + | xE ⇒ mk_Array16T T e00 e01 e02 e03 e04 e05 e06 e07 e08 v v v v v v e15 + | xF ⇒ mk_Array16T T e00 e01 e02 e03 e04 e05 e06 e07 e08 v v v v v v v ] + | xA ⇒ match n with + [ x0 ⇒ p | x1 ⇒ p | x2 ⇒ p | x3 ⇒ p | x4 ⇒ p | x5 ⇒ p | x6 ⇒ p | x7 ⇒ p + | x8 ⇒ p | x9 ⇒ p + | xA ⇒ mk_Array16T T e00 e01 e02 e03 e04 e05 e06 e07 e08 e09 v e11 e12 e13 e14 e15 + | xB ⇒ mk_Array16T T e00 e01 e02 e03 e04 e05 e06 e07 e08 e09 v v e12 e13 e14 e15 + | xC ⇒ mk_Array16T T e00 e01 e02 e03 e04 e05 e06 e07 e08 e09 v v v e13 e14 e15 + | xD ⇒ mk_Array16T T e00 e01 e02 e03 e04 e05 e06 e07 e08 e09 v v v v e14 e15 + | xE ⇒ mk_Array16T T e00 e01 e02 e03 e04 e05 e06 e07 e08 e09 v v v v v e15 + | xF ⇒ mk_Array16T T e00 e01 e02 e03 e04 e05 e06 e07 e08 e09 v v v v v v ] + | xB ⇒ match n with + [ x0 ⇒ p | x1 ⇒ p | x2 ⇒ p | x3 ⇒ p | x4 ⇒ p | x5 ⇒ p | x6 ⇒ p | x7 ⇒ p + | x8 ⇒ p | x9 ⇒ p | xA ⇒ p + | xB ⇒ mk_Array16T T e00 e01 e02 e03 e04 e05 e06 e07 e08 e09 e10 v e12 e13 e14 e15 + | xC ⇒ mk_Array16T T e00 e01 e02 e03 e04 e05 e06 e07 e08 e09 e10 v v e13 e14 e15 + | xD ⇒ mk_Array16T T e00 e01 e02 e03 e04 e05 e06 e07 e08 e09 e10 v v v e14 e15 + | xE ⇒ mk_Array16T T e00 e01 e02 e03 e04 e05 e06 e07 e08 e09 e10 v v v v e15 + | xF ⇒ mk_Array16T T e00 e01 e02 e03 e04 e05 e06 e07 e08 e09 e10 v v v v v ] + | xC ⇒ match n with + [ x0 ⇒ p | x1 ⇒ p | x2 ⇒ p | x3 ⇒ p | x4 ⇒ p | x5 ⇒ p | x6 ⇒ p | x7 ⇒ p + | x8 ⇒ p | x9 ⇒ p | xA ⇒ p | xB ⇒ p + | xC ⇒ mk_Array16T T e00 e01 e02 e03 e04 e05 e06 e07 e08 e09 e10 e11 v e13 e14 e15 + | xD ⇒ mk_Array16T T e00 e01 e02 e03 e04 e05 e06 e07 e08 e09 e10 e11 v v e14 e15 + | xE ⇒ mk_Array16T T e00 e01 e02 e03 e04 e05 e06 e07 e08 e09 e10 e11 v v v e15 + | xF ⇒ mk_Array16T T e00 e01 e02 e03 e04 e05 e06 e07 e08 e09 e10 e11 v v v v ] + | xD ⇒ match n with + [ x0 ⇒ p | x1 ⇒ p | x2 ⇒ p | x3 ⇒ p | x4 ⇒ p | x5 ⇒ p | x6 ⇒ p | x7 ⇒ p + | x8 ⇒ p | x9 ⇒ p | xA ⇒ p | xB ⇒ p | xC ⇒ p + | xD ⇒ mk_Array16T T e00 e01 e02 e03 e04 e05 e06 e07 e08 e09 e10 e11 e12 v e14 e15 + | xE ⇒ mk_Array16T T e00 e01 e02 e03 e04 e05 e06 e07 e08 e09 e10 e11 e12 v v e15 + | xF ⇒ mk_Array16T T e00 e01 e02 e03 e04 e05 e06 e07 e08 e09 e10 e11 e12 v v v ] + | xE ⇒ match n with + [ x0 ⇒ p | x1 ⇒ p | x2 ⇒ p | x3 ⇒ p | x4 ⇒ p | x5 ⇒ p | x6 ⇒ p | x7 ⇒ p + | x8 ⇒ p | x9 ⇒ p | xA ⇒ p | xB ⇒ p | xC ⇒ p | xD ⇒ p + | xE ⇒ mk_Array16T T e00 e01 e02 e03 e04 e05 e06 e07 e08 e09 e10 e11 e12 e13 v e15 + | xF ⇒ mk_Array16T T e00 e01 e02 e03 e04 e05 e06 e07 e08 e09 e10 e11 e12 e13 v v ] + | xF ⇒ match n with + [ x0 ⇒ p | x1 ⇒ p | x2 ⇒ p | x3 ⇒ p | x4 ⇒ p | x5 ⇒ p | x6 ⇒ p | x7 ⇒ p + | x8 ⇒ p | x9 ⇒ p | xA ⇒ p | xB ⇒ p | xC ⇒ p | xD ⇒ p | xE ⇒ p + | xF ⇒ mk_Array16T T e00 e01 e02 e03 e04 e05 e06 e07 e08 e09 e10 e11 e12 e13 e14 v ] + ]. + +(* abbiamo gia' gli esadecimali come tipo induttivo quindi: *) +(* posso definire un setter composto [m+1,n-1] a matrice sull'array *) +(* NB: obbiettivo evitare l'overflow *) +ndefinition setmn_array16T_succ_pred ≝ +λm,n:exadecim.λT:Type.λp:Array16T T.λv:T. + match lt_ex m xF with + [ true ⇒ match gt_ex n x0 with + [ true ⇒ setmn_array16T (succ_ex m) (pred_ex n) T p v + | false ⇒ p + ] + | false ⇒ p + ]. + +(* abbiamo gia' gli esadecimali come tipo induttivo quindi: *) +(* posso definire un setter composto [m+1,F] a matrice sull'array *) +(* NB: obbiettivo evitare l'overflow *) +ndefinition setmn_array16T_succ ≝ +λm:exadecim.λT:Type.λp:Array16T T.λv:T. + match lt_ex m xF with + [ true ⇒ setmn_array16T (succ_ex m) xF T p v + | false ⇒ p + ]. + +(* abbiamo gia' gli esadecimali come tipo induttivo quindi: *) +(* posso definire un setter composto [0,n-1] a matrice sull'array *) +(* NB: obbiettivo evitare l'overflow *) +ndefinition setmn_array16T_pred ≝ +λn:exadecim.λT:Type.λp:Array16T T.λv:T. + match gt_ex n x0 with + [ true ⇒ setmn_array16T x0 (pred_ex n) T p v + | false ⇒ p + ]. + +(* ************************** *) +(* TIPO BYTE COME INSIEME BIT *) +(* ************************** *) + +(* definizione di un byte come 8 bit *) +nrecord Array8T (T:Type) : Type ≝ +{ a8_1 : T ; a8_2 : T ; a8_3 : T ; a8_4 : T +; a8_5 : T ; a8_6 : T ; a8_7 : T ; a8_8 : T }. + +(* abbiamo gia' gli ottali come tipo induttivo quindi: *) +(* posso definire un getter a matrice sull'array *) +ndefinition getn_array8T ≝ +λn:oct.λT:Type.λp:Array8T T. + match n return λn.(Array8T T) → T with + [ o0 ⇒ a8_1 T | o1 ⇒ a8_2 T | o2 ⇒ a8_3 T | o3 ⇒ a8_4 T + | o4 ⇒ a8_5 T | o5 ⇒ a8_6 T | o6 ⇒ a8_7 T | o7 ⇒ a8_8 T + ] p. + +(* abbiamo gia' gli ottali come tipo induttivo quindi: *) +(* posso definire un setter a matrice sull'array *) +ndefinition setn_array8T ≝ +λn:oct.λT:Type.λp:Array8T T.λv:T. +let e00 ≝ (a8_1 T p) in +let e01 ≝ (a8_2 T p) in +let e02 ≝ (a8_3 T p) in +let e03 ≝ (a8_4 T p) in +let e04 ≝ (a8_5 T p) in +let e05 ≝ (a8_6 T p) in +let e06 ≝ (a8_7 T p) in +let e07 ≝ (a8_8 T p) in + match n with + [ o0 ⇒ mk_Array8T T e07 e06 e05 e04 e03 e02 e01 v + | o1 ⇒ mk_Array8T T e07 e06 e05 e04 e03 e02 v e00 + | o2 ⇒ mk_Array8T T e07 e06 e05 e04 e03 v e01 e00 + | o3 ⇒ mk_Array8T T e07 e06 e05 e04 v e02 e01 e00 + | o4 ⇒ mk_Array8T T e07 e06 e05 v e03 e02 e01 e00 + | o5 ⇒ mk_Array8T T e07 e06 v e04 e03 e02 e01 e00 + | o6 ⇒ mk_Array8T T e07 v e05 e04 e03 e02 e01 e00 + | o7 ⇒ mk_Array8T T v e06 e05 e04 e03 e02 e01 e00 + ]. + +(* lettura byte *) +ndefinition byte8_of_bits ≝ +λp:Array8T bool. + mk_byte8 + (or_ex (match a8_8 ? p with [ true ⇒ x8 | false ⇒ x0 ]) + (or_ex (match a8_7 ? p with [ true ⇒ x4 | false ⇒ x0 ]) + (or_ex (match a8_6 ? p with [ true ⇒ x2 | false ⇒ x0 ]) + (match a8_5 ? p with [ true ⇒ x1 | false ⇒ x0 ])))) + (or_ex (match a8_4 ? p with [ true ⇒ x8 | false ⇒ x0 ]) + (or_ex (match a8_3 ? p with [ true ⇒ x4 | false ⇒ x0 ]) + (or_ex (match a8_2 ? p with [ true ⇒ x2 | false ⇒ x0 ]) + (match a8_1 ? p with [ true ⇒ x1 | false ⇒ x0 ])))). + +(* scrittura byte *) +ndefinition bits_of_byte8 ≝ +λp:byte8. + match b8h p with + [ x0 ⇒ match b8l p with + [ x0 ⇒ mk_Array8T bool false false false false false false false false + | x1 ⇒ mk_Array8T bool false false false false false false false true + | x2 ⇒ mk_Array8T bool false false false false false false true false + | x3 ⇒ mk_Array8T bool false false false false false false true true + | x4 ⇒ mk_Array8T bool false false false false false true false false + | x5 ⇒ mk_Array8T bool false false false false false true false true + | x6 ⇒ mk_Array8T bool false false false false false true true false + | x7 ⇒ mk_Array8T bool false false false false false true true true + | x8 ⇒ mk_Array8T bool false false false false true false false false + | x9 ⇒ mk_Array8T bool false false false false true false false true + | xA ⇒ mk_Array8T bool false false false false true false true false + | xB ⇒ mk_Array8T bool false false false false true false true true + | xC ⇒ mk_Array8T bool false false false false true true false false + | xD ⇒ mk_Array8T bool false false false false true true false true + | xE ⇒ mk_Array8T bool false false false false true true true false + | xF ⇒ mk_Array8T bool false false false false true true true true ] + | x1 ⇒ match b8l p with + [ x0 ⇒ mk_Array8T bool false false false true false false false false + | x1 ⇒ mk_Array8T bool false false false true false false false true + | x2 ⇒ mk_Array8T bool false false false true false false true false + | x3 ⇒ mk_Array8T bool false false false true false false true true + | x4 ⇒ mk_Array8T bool false false false true false true false false + | x5 ⇒ mk_Array8T bool false false false true false true false true + | x6 ⇒ mk_Array8T bool false false false true false true true false + | x7 ⇒ mk_Array8T bool false false false true false true true true + | x8 ⇒ mk_Array8T bool false false false true true false false false + | x9 ⇒ mk_Array8T bool false false false true true false false true + | xA ⇒ mk_Array8T bool false false false true true false true false + | xB ⇒ mk_Array8T bool false false false true true false true true + | xC ⇒ mk_Array8T bool false false false true true true false false + | xD ⇒ mk_Array8T bool false false false true true true false true + | xE ⇒ mk_Array8T bool false false false true true true true false + | xF ⇒ mk_Array8T bool false false false true true true true true ] + | x2 ⇒ match b8l p with + [ x0 ⇒ mk_Array8T bool false false true false false false false false + | x1 ⇒ mk_Array8T bool false false true false false false false true + | x2 ⇒ mk_Array8T bool false false true false false false true false + | x3 ⇒ mk_Array8T bool false false true false false false true true + | x4 ⇒ mk_Array8T bool false false true false false true false false + | x5 ⇒ mk_Array8T bool false false true false false true false true + | x6 ⇒ mk_Array8T bool false false true false false true true false + | x7 ⇒ mk_Array8T bool false false true false false true true true + | x8 ⇒ mk_Array8T bool false false true false true false false false + | x9 ⇒ mk_Array8T bool false false true false true false false true + | xA ⇒ mk_Array8T bool false false true false true false true false + | xB ⇒ mk_Array8T bool false false true false true false true true + | xC ⇒ mk_Array8T bool false false true false true true false false + | xD ⇒ mk_Array8T bool false false true false true true false true + | xE ⇒ mk_Array8T bool false false true false true true true false + | xF ⇒ mk_Array8T bool false false true false true true true true ] + | x3 ⇒ match b8l p with + [ x0 ⇒ mk_Array8T bool false false true true false false false false + | x1 ⇒ mk_Array8T bool false false true true false false false true + | x2 ⇒ mk_Array8T bool false false true true false false true false + | x3 ⇒ mk_Array8T bool false false true true false false true true + | x4 ⇒ mk_Array8T bool false false true true false true false false + | x5 ⇒ mk_Array8T bool false false true true false true false true + | x6 ⇒ mk_Array8T bool false false true true false true true false + | x7 ⇒ mk_Array8T bool false false true true false true true true + | x8 ⇒ mk_Array8T bool false false true true true false false false + | x9 ⇒ mk_Array8T bool false false true true true false false true + | xA ⇒ mk_Array8T bool false false true true true false true false + | xB ⇒ mk_Array8T bool false false true true true false true true + | xC ⇒ mk_Array8T bool false false true true true true false false + | xD ⇒ mk_Array8T bool false false true true true true false true + | xE ⇒ mk_Array8T bool false false true true true true true false + | xF ⇒ mk_Array8T bool false false true true true true true true ] + | x4 ⇒ match b8l p with + [ x0 ⇒ mk_Array8T bool false true false false false false false false + | x1 ⇒ mk_Array8T bool false true false false false false false true + | x2 ⇒ mk_Array8T bool false true false false false false true false + | x3 ⇒ mk_Array8T bool false true false false false false true true + | x4 ⇒ mk_Array8T bool false true false false false true false false + | x5 ⇒ mk_Array8T bool false true false false false true false true + | x6 ⇒ mk_Array8T bool false true false false false true true false + | x7 ⇒ mk_Array8T bool false true false false false true true true + | x8 ⇒ mk_Array8T bool false true false false true false false false + | x9 ⇒ mk_Array8T bool false true false false true false false true + | xA ⇒ mk_Array8T bool false true false false true false true false + | xB ⇒ mk_Array8T bool false true false false true false true true + | xC ⇒ mk_Array8T bool false true false false true true false false + | xD ⇒ mk_Array8T bool false true false false true true false true + | xE ⇒ mk_Array8T bool false true false false true true true false + | xF ⇒ mk_Array8T bool false true false false true true true true ] + | x5 ⇒ match b8l p with + [ x0 ⇒ mk_Array8T bool false true false true false false false false + | x1 ⇒ mk_Array8T bool false true false true false false false true + | x2 ⇒ mk_Array8T bool false true false true false false true false + | x3 ⇒ mk_Array8T bool false true false true false false true true + | x4 ⇒ mk_Array8T bool false true false true false true false false + | x5 ⇒ mk_Array8T bool false true false true false true false true + | x6 ⇒ mk_Array8T bool false true false true false true true false + | x7 ⇒ mk_Array8T bool false true false true false true true true + | x8 ⇒ mk_Array8T bool false true false true true false false false + | x9 ⇒ mk_Array8T bool false true false true true false false true + | xA ⇒ mk_Array8T bool false true false true true false true false + | xB ⇒ mk_Array8T bool false true false true true false true true + | xC ⇒ mk_Array8T bool false true false true true true false false + | xD ⇒ mk_Array8T bool false true false true true true false true + | xE ⇒ mk_Array8T bool false true false true true true true false + | xF ⇒ mk_Array8T bool false true false true true true true true ] + | x6 ⇒ match b8l p with + [ x0 ⇒ mk_Array8T bool false true true false false false false false + | x1 ⇒ mk_Array8T bool false true true false false false false true + | x2 ⇒ mk_Array8T bool false true true false false false true false + | x3 ⇒ mk_Array8T bool false true true false false false true true + | x4 ⇒ mk_Array8T bool false true true false false true false false + | x5 ⇒ mk_Array8T bool false true true false false true false true + | x6 ⇒ mk_Array8T bool false true true false false true true false + | x7 ⇒ mk_Array8T bool false true true false false true true true + | x8 ⇒ mk_Array8T bool false true true false true false false false + | x9 ⇒ mk_Array8T bool false true true false true false false true + | xA ⇒ mk_Array8T bool false true true false true false true false + | xB ⇒ mk_Array8T bool false true true false true false true true + | xC ⇒ mk_Array8T bool false true true false true true false false + | xD ⇒ mk_Array8T bool false true true false true true false true + | xE ⇒ mk_Array8T bool false true true false true true true false + | xF ⇒ mk_Array8T bool false true true false true true true true ] + | x7 ⇒ match b8l p with + [ x0 ⇒ mk_Array8T bool false true true true false false false false + | x1 ⇒ mk_Array8T bool false true true true false false false true + | x2 ⇒ mk_Array8T bool false true true true false false true false + | x3 ⇒ mk_Array8T bool false true true true false false true true + | x4 ⇒ mk_Array8T bool false true true true false true false false + | x5 ⇒ mk_Array8T bool false true true true false true false true + | x6 ⇒ mk_Array8T bool false true true true false true true false + | x7 ⇒ mk_Array8T bool false true true true false true true true + | x8 ⇒ mk_Array8T bool false true true true true false false false + | x9 ⇒ mk_Array8T bool false true true true true false false true + | xA ⇒ mk_Array8T bool false true true true true false true false + | xB ⇒ mk_Array8T bool false true true true true false true true + | xC ⇒ mk_Array8T bool false true true true true true false false + | xD ⇒ mk_Array8T bool false true true true true true false true + | xE ⇒ mk_Array8T bool false true true true true true true false + | xF ⇒ mk_Array8T bool false true true true true true true true ] + | x8 ⇒ match b8l p with + [ x0 ⇒ mk_Array8T bool true false false false false false false false + | x1 ⇒ mk_Array8T bool true false false false false false false true + | x2 ⇒ mk_Array8T bool true false false false false false true false + | x3 ⇒ mk_Array8T bool true false false false false false true true + | x4 ⇒ mk_Array8T bool true false false false false true false false + | x5 ⇒ mk_Array8T bool true false false false false true false true + | x6 ⇒ mk_Array8T bool true false false false false true true false + | x7 ⇒ mk_Array8T bool true false false false false true true true + | x8 ⇒ mk_Array8T bool true false false false true false false false + | x9 ⇒ mk_Array8T bool true false false false true false false true + | xA ⇒ mk_Array8T bool true false false false true false true false + | xB ⇒ mk_Array8T bool true false false false true false true true + | xC ⇒ mk_Array8T bool true false false false true true false false + | xD ⇒ mk_Array8T bool true false false false true true false true + | xE ⇒ mk_Array8T bool true false false false true true true false + | xF ⇒ mk_Array8T bool true false false false true true true true ] + | x9 ⇒ match b8l p with + [ x0 ⇒ mk_Array8T bool true false false true false false false false + | x1 ⇒ mk_Array8T bool true false false true false false false true + | x2 ⇒ mk_Array8T bool true false false true false false true false + | x3 ⇒ mk_Array8T bool true false false true false false true true + | x4 ⇒ mk_Array8T bool true false false true false true false false + | x5 ⇒ mk_Array8T bool true false false true false true false true + | x6 ⇒ mk_Array8T bool true false false true false true true false + | x7 ⇒ mk_Array8T bool true false false true false true true true + | x8 ⇒ mk_Array8T bool true false false true true false false false + | x9 ⇒ mk_Array8T bool true false false true true false false true + | xA ⇒ mk_Array8T bool true false false true true false true false + | xB ⇒ mk_Array8T bool true false false true true false true true + | xC ⇒ mk_Array8T bool true false false true true true false false + | xD ⇒ mk_Array8T bool true false false true true true false true + | xE ⇒ mk_Array8T bool true false false true true true true false + | xF ⇒ mk_Array8T bool true false false true true true true true ] + | xA ⇒ match b8l p with + [ x0 ⇒ mk_Array8T bool true false true false false false false false + | x1 ⇒ mk_Array8T bool true false true false false false false true + | x2 ⇒ mk_Array8T bool true false true false false false true false + | x3 ⇒ mk_Array8T bool true false true false false false true true + | x4 ⇒ mk_Array8T bool true false true false false true false false + | x5 ⇒ mk_Array8T bool true false true false false true false true + | x6 ⇒ mk_Array8T bool true false true false false true true false + | x7 ⇒ mk_Array8T bool true false true false false true true true + | x8 ⇒ mk_Array8T bool true false true false true false false false + | x9 ⇒ mk_Array8T bool true false true false true false false true + | xA ⇒ mk_Array8T bool true false true false true false true false + | xB ⇒ mk_Array8T bool true false true false true false true true + | xC ⇒ mk_Array8T bool true false true false true true false false + | xD ⇒ mk_Array8T bool true false true false true true false true + | xE ⇒ mk_Array8T bool true false true false true true true false + | xF ⇒ mk_Array8T bool true false true false true true true true ] + | xB ⇒ match b8l p with + [ x0 ⇒ mk_Array8T bool true false true true false false false false + | x1 ⇒ mk_Array8T bool true false true true false false false true + | x2 ⇒ mk_Array8T bool true false true true false false true false + | x3 ⇒ mk_Array8T bool true false true true false false true true + | x4 ⇒ mk_Array8T bool true false true true false true false false + | x5 ⇒ mk_Array8T bool true false true true false true false true + | x6 ⇒ mk_Array8T bool true false true true false true true false + | x7 ⇒ mk_Array8T bool true false true true false true true true + | x8 ⇒ mk_Array8T bool true false true true true false false false + | x9 ⇒ mk_Array8T bool true false true true true false false true + | xA ⇒ mk_Array8T bool true false true true true false true false + | xB ⇒ mk_Array8T bool true false true true true false true true + | xC ⇒ mk_Array8T bool true false true true true true false false + | xD ⇒ mk_Array8T bool true false true true true true false true + | xE ⇒ mk_Array8T bool true false true true true true true false + | xF ⇒ mk_Array8T bool true false true true true true true true ] + | xC ⇒ match b8l p with + [ x0 ⇒ mk_Array8T bool true true false false false false false false + | x1 ⇒ mk_Array8T bool true true false false false false false true + | x2 ⇒ mk_Array8T bool true true false false false false true false + | x3 ⇒ mk_Array8T bool true true false false false false true true + | x4 ⇒ mk_Array8T bool true true false false false true false false + | x5 ⇒ mk_Array8T bool true true false false false true false true + | x6 ⇒ mk_Array8T bool true true false false false true true false + | x7 ⇒ mk_Array8T bool true true false false false true true true + | x8 ⇒ mk_Array8T bool true true false false true false false false + | x9 ⇒ mk_Array8T bool true true false false true false false true + | xA ⇒ mk_Array8T bool true true false false true false true false + | xB ⇒ mk_Array8T bool true true false false true false true true + | xC ⇒ mk_Array8T bool true true false false true true false false + | xD ⇒ mk_Array8T bool true true false false true true false true + | xE ⇒ mk_Array8T bool true true false false true true true false + | xF ⇒ mk_Array8T bool true true false false true true true true ] + | xD ⇒ match b8l p with + [ x0 ⇒ mk_Array8T bool true true false true false false false false + | x1 ⇒ mk_Array8T bool true true false true false false false true + | x2 ⇒ mk_Array8T bool true true false true false false true false + | x3 ⇒ mk_Array8T bool true true false true false false true true + | x4 ⇒ mk_Array8T bool true true false true false true false false + | x5 ⇒ mk_Array8T bool true true false true false true false true + | x6 ⇒ mk_Array8T bool true true false true false true true false + | x7 ⇒ mk_Array8T bool true true false true false true true true + | x8 ⇒ mk_Array8T bool true true false true true false false false + | x9 ⇒ mk_Array8T bool true true false true true false false true + | xA ⇒ mk_Array8T bool true true false true true false true false + | xB ⇒ mk_Array8T bool true true false true true false true true + | xC ⇒ mk_Array8T bool true true false true true true false false + | xD ⇒ mk_Array8T bool true true false true true true false true + | xE ⇒ mk_Array8T bool true true false true true true true false + | xF ⇒ mk_Array8T bool true true false true true true true true ] + | xE ⇒ match b8l p with + [ x0 ⇒ mk_Array8T bool true true true false false false false false + | x1 ⇒ mk_Array8T bool true true true false false false false true + | x2 ⇒ mk_Array8T bool true true true false false false true false + | x3 ⇒ mk_Array8T bool true true true false false false true true + | x4 ⇒ mk_Array8T bool true true true false false true false false + | x5 ⇒ mk_Array8T bool true true true false false true false true + | x6 ⇒ mk_Array8T bool true true true false false true true false + | x7 ⇒ mk_Array8T bool true true true false false true true true + | x8 ⇒ mk_Array8T bool true true true false true false false false + | x9 ⇒ mk_Array8T bool true true true false true false false true + | xA ⇒ mk_Array8T bool true true true false true false true false + | xB ⇒ mk_Array8T bool true true true false true false true true + | xC ⇒ mk_Array8T bool true true true false true true false false + | xD ⇒ mk_Array8T bool true true true false true true false true + | xE ⇒ mk_Array8T bool true true true false true true true false + | xF ⇒ mk_Array8T bool true true true false true true true true ] + | xF ⇒ match b8l p with + [ x0 ⇒ mk_Array8T bool true true true true false false false false + | x1 ⇒ mk_Array8T bool true true true true false false false true + | x2 ⇒ mk_Array8T bool true true true true false false true false + | x3 ⇒ mk_Array8T bool true true true true false false true true + | x4 ⇒ mk_Array8T bool true true true true false true false false + | x5 ⇒ mk_Array8T bool true true true true false true false true + | x6 ⇒ mk_Array8T bool true true true true false true true false + | x7 ⇒ mk_Array8T bool true true true true false true true true + | x8 ⇒ mk_Array8T bool true true true true true false false false + | x9 ⇒ mk_Array8T bool true true true true true false false true + | xA ⇒ mk_Array8T bool true true true true true false true false + | xB ⇒ mk_Array8T bool true true true true true false true true + | xC ⇒ mk_Array8T bool true true true true true true false false + | xD ⇒ mk_Array8T bool true true true true true true false true + | xE ⇒ mk_Array8T bool true true true true true true true false + | xF ⇒ mk_Array8T bool true true true true true true true true ] + ]. diff --git a/helm/software/matita/contribs/ng_assembly/memory/memory_trees.ma b/helm/software/matita/contribs/ng_assembly/memory/memory_trees.ma new file mode 100755 index 000000000..b2f2a0d35 --- /dev/null +++ b/helm/software/matita/contribs/ng_assembly/memory/memory_trees.ma @@ -0,0 +1,148 @@ +(**************************************************************************) +(* ___ *) +(* ||M|| *) +(* ||A|| A project by Andrea Asperti *) +(* ||T|| *) +(* ||I|| Developers: *) +(* ||T|| The HELM team. *) +(* ||A|| http://helm.cs.unibo.it *) +(* \ / *) +(* \ / This file is distributed under the terms of the *) +(* v GNU General Public License Version 2 *) +(* *) +(**************************************************************************) + +(* ********************************************************************** *) +(* Progetto FreeScale *) +(* *) +(* Sviluppato da: Ing. Cosimo Oliboni, oliboni@cs.unibo.it *) +(* Sviluppo: 2008-2010 *) +(* *) +(* ********************************************************************** *) + +include "memory/memory_struct.ma". +include "num/word32.ma". +include "common/option.ma". +include "common/list.ma". + +(* ********************* *) +(* MEMORIA E DESCRITTORE *) +(* ********************* *) + +ndefinition aux_32B_filler ≝ +λT:Type.λel:T. +let lev8 ≝ mk_Array16T T el el el el el el el el el el el el el el el el in +let lev7 ≝ mk_Array16T ? + lev8 lev8 lev8 lev8 lev8 lev8 lev8 lev8 + lev8 lev8 lev8 lev8 lev8 lev8 lev8 lev8 + in +let lev6 ≝ mk_Array16T ? + lev7 lev7 lev7 lev7 lev7 lev7 lev7 lev7 + lev7 lev7 lev7 lev7 lev7 lev7 lev7 lev7 + in +let lev5 ≝ mk_Array16T ? + lev6 lev6 lev6 lev6 lev6 lev6 lev6 lev6 + lev6 lev6 lev6 lev6 lev6 lev6 lev6 lev6 + in +let lev4 ≝ mk_Array16T ? + lev5 lev5 lev5 lev5 lev5 lev5 lev5 lev5 + lev5 lev5 lev5 lev5 lev5 lev5 lev5 lev5 + in +let lev3 ≝ mk_Array16T ? + lev4 lev4 lev4 lev4 lev4 lev4 lev4 lev4 + lev4 lev4 lev4 lev4 lev4 lev4 lev4 lev4 + in +let lev2 ≝ mk_Array16T ? + lev3 lev3 lev3 lev3 lev3 lev3 lev3 lev3 + lev3 lev3 lev3 lev3 lev3 lev3 lev3 lev3 + in +let lev1 ≝ mk_Array16T ? + lev2 lev2 lev2 lev2 lev2 lev2 lev2 lev2 + lev2 lev2 lev2 lev2 lev2 lev2 lev2 lev2 + in +lev1. + +ndefinition aux_32B_type ≝ +λT:Type.Array16T (Array16T (Array16T (Array16T (Array16T (Array16T (Array16T (Array16T T))))))). + +(* tutta la memoria non installata *) +ndefinition mt_out_of_bound_memory ≝ aux_32B_filler ? MEM_OUT_OF_BOUND. + +(* tutta la memoria a 0 *) +ndefinition mt_zero_memory ≝ aux_32B_filler ? 〈x0,x0〉. + +(* visita di un albero da 4GB di elementi: ln16(4GB)=8 passaggi *) +ndefinition mt_visit ≝ +λT:Type.λdata:aux_32B_type T.λaddr:word32. + getn_array16T (b8l (w16l (w32l addr))) ? + (getn_array16T (b8h (w16l (w32l addr))) ? + (getn_array16T (b8l (w16h (w32l addr))) ? + (getn_array16T (b8h (w16h (w32l addr))) ? + (getn_array16T (b8l (w16l (w32h addr))) ? + (getn_array16T (b8h (w16l (w32h addr))) ? + (getn_array16T (b8l (w16h (w32h addr))) ? + (getn_array16T (b8h (w16h (w32h addr))) ? data))))))). + +(* scrittura di un elemento in un albero da 4GB *) +ndefinition mt_update ≝ +λT:Type.λdata:aux_32B_type T.λaddr:word32.λv:T. + let lev2 ≝ getn_array16T (b8h (w16h (w32h addr))) ? data in + let lev3 ≝ getn_array16T (b8l (w16h (w32h addr))) ? lev2 in + let lev4 ≝ getn_array16T (b8h (w16l (w32h addr))) ? lev3 in + let lev5 ≝ getn_array16T (b8l (w16l (w32h addr))) ? lev4 in + let lev6 ≝ getn_array16T (b8h (w16h (w32l addr))) ? lev5 in + let lev7 ≝ getn_array16T (b8l (w16h (w32l addr))) ? lev6 in + let lev8 ≝ getn_array16T (b8h (w16l (w32l addr))) ? lev7 in + + setn_array16T (b8h (w16h (w32h addr))) ? data + (setn_array16T (b8l (w16h (w32h addr))) ? lev2 + (setn_array16T (b8h (w16l (w32h addr))) ? lev3 + (setn_array16T (b8l (w16l (w32h addr))) ? lev4 + (setn_array16T (b8h (w16h (w32l addr))) ? lev5 + (setn_array16T (b8l (w16h (w32l addr))) ? lev6 + (setn_array16T (b8h (w16l (w32l addr))) ? lev7 + (setn_array16T (b8l (w16l (w32l addr))) T lev8 v))))))). + +(* scrittura di un range (max 64KB) in un albero da 4GB *) +nlet rec mt_update_ranged (T:Type) (data:aux_32B_type T) (addr:word32) (w:word16) (rw:rec_word16 w) (v:T) on rw ≝ + match rw with + [ w16_O ⇒ data + | w16_S w' rw' ⇒ mt_update_ranged T (mt_update T data addr v) + (succ_w32 addr) w' rw' v + ]. + +(* scrivi controllando il tipo di memoria *) +ndefinition mt_mem_update ≝ +λmem:aux_32B_type byte8. +λchk:aux_32B_type memory_type. +λaddr:word32.λv:byte8. + match mt_visit ? chk addr with + (* ROM? ok, ma il valore viene perso *) + [ MEM_READ_ONLY ⇒ Some ? mem + (* RAM? ok *) + | MEM_READ_WRITE ⇒ Some ? (mt_update ? mem addr v) + (* NON INSTALLATA? no *) + | MEM_OUT_OF_BOUND ⇒ None ? ]. + +(* leggi controllando il tipo di memoria *) +ndefinition mt_mem_read ≝ +λmem:aux_32B_type byte8. +λchk:aux_32B_type memory_type. +λaddr:word32. + match mt_visit ? chk addr with + [ MEM_READ_ONLY ⇒ Some ? (mt_visit ? mem addr) + | MEM_READ_WRITE ⇒ Some ? (mt_visit ? mem addr) + | MEM_OUT_OF_BOUND ⇒ None ? ]. + +(* ************************** *) +(* CARICAMENTO PROGRAMMA/DATI *) +(* ************************** *) + +(* carica a paratire da addr, overflow se si supera 0xFFFF... *) +nlet rec mt_load_from_source_at (old_mem:aux_32B_type byte8) + (src:list byte8) (addr:word32) on src ≝ + match src with + (* fine di source: carica da old_mem *) + [ nil ⇒ old_mem + | cons hd tl ⇒ mt_load_from_source_at (mt_update ? old_mem addr hd) tl (succ_w32 addr) + ]. diff --git a/helm/software/matita/contribs/ng_assembly/num/byte8.ma b/helm/software/matita/contribs/ng_assembly/num/byte8.ma index e899a6989..d759181ce 100755 --- a/helm/software/matita/contribs/ng_assembly/num/byte8.ma +++ b/helm/software/matita/contribs/ng_assembly/num/byte8.ma @@ -306,9 +306,12 @@ ndefinition daa_b8 ≝ pair … X'' true ]. -(* operatore x in [inf,sup] *) +(* operatore x in [inf,sup] o in sup],[inf *) ndefinition inrange_b8 ≝ -λx,inf,sup:byte8.(le_b8 inf x) ⊗ (le_b8 x sup). +λx,inf,sup:byte8. + match le_b8 inf sup with + [ true ⇒ and_bool | false ⇒ or_bool ] + (le_b8 inf x) (le_b8 x sup). (* iteratore sui byte *) ndefinition forall_b8 ≝ diff --git a/helm/software/matita/contribs/ng_assembly/num/exadecim.ma b/helm/software/matita/contribs/ng_assembly/num/exadecim.ma index f4728367f..e75c80bd6 100755 --- a/helm/software/matita/contribs/ng_assembly/num/exadecim.ma +++ b/helm/software/matita/contribs/ng_assembly/num/exadecim.ma @@ -1378,9 +1378,12 @@ ndefinition compl_ex ≝ | x8 ⇒ x8 | x9 ⇒ x7 | xA ⇒ x6 | xB ⇒ x5 | xC ⇒ x4 | xD ⇒ x3 | xE ⇒ x2 | xF ⇒ x1 ]. -(* operatore x in [inf,sup] *) +(* operatore x in [inf,sup] o in sup],[inf *) ndefinition inrange_ex ≝ -λx,inf,sup:exadecim.(le_ex inf x) ⊗ (le_ex x sup). +λx,inf,sup:exadecim. + match le_ex inf sup with + [ true ⇒ and_bool | false ⇒ or_bool ] + (le_ex inf x) (le_ex x sup). (* iteratore sugli esadecimali *) ndefinition forall_ex ≝ λP. diff --git a/helm/software/matita/contribs/ng_assembly/num/word16.ma b/helm/software/matita/contribs/ng_assembly/num/word16.ma index 2ae8fc5fd..e89e64f3d 100755 --- a/helm/software/matita/contribs/ng_assembly/num/word16.ma +++ b/helm/software/matita/contribs/ng_assembly/num/word16.ma @@ -233,9 +233,12 @@ ndefinition div_b8 ≝ (* puo' essere sottratto al dividendo *) | false ⇒ div_b8_aux w (rol_w16_n 〈〈x0,x0〉:b〉 nat7) 〈x8,x0〉 〈x0,x0〉 nat7 ]]. -(* operatore x in [inf,sup] *) +(* operatore x in [inf,sup] o in sup],[inf *) ndefinition inrange_w16 ≝ -λx,inf,sup:word16.(le_w16 inf x) ⊗ (le_w16 x sup). +λx,inf,sup:word16. + match le_w16 inf sup with + [ true ⇒ and_bool | false ⇒ or_bool ] + (le_w16 inf x) (le_w16 x sup). (* iteratore sulle word *) ndefinition forall_w16 ≝ diff --git a/helm/software/matita/contribs/ng_assembly/num/word32.ma b/helm/software/matita/contribs/ng_assembly/num/word32.ma index 416ad623f..bc81cac17 100755 --- a/helm/software/matita/contribs/ng_assembly/num/word32.ma +++ b/helm/software/matita/contribs/ng_assembly/num/word32.ma @@ -233,9 +233,12 @@ ndefinition div_w16 ≝ (* puo' essere sottratto al dividendo *) | false ⇒ div_w16_aux w (rol_w32_n 〈〈〈x0,x0〉:〈x0,x0〉〉.b〉 nat15) 〈〈x8,x0〉:〈x0,x0〉〉 〈〈x0,x0〉:〈x0,x0〉〉 nat15 ]]. -(* operatore x in [inf,sup] *) +(* operatore x in [inf,sup] o in sup],[inf *) ndefinition inrange_w32 ≝ -λx,inf,sup:word32.(le_w32 inf x) ⊗ (le_w32 x sup). +λx,inf,sup:word32. + match le_w32 inf sup with + [ true ⇒ and_bool | false ⇒ or_bool ] + (le_w32 inf x) (le_w32 x sup). (* iteratore sulle word *) ndefinition forall_w32 ≝ diff --git a/helm/software/matita/contribs/ng_assembly/universe/universe.ma b/helm/software/matita/contribs/ng_assembly/universe/universe.ma index 21fd84675..0db667a0f 100755 --- a/helm/software/matita/contribs/ng_assembly/universe/universe.ma +++ b/helm/software/matita/contribs/ng_assembly/universe/universe.ma @@ -16,7 +16,7 @@ (* Progetto FreeScale *) (* *) (* Sviluppato da: Ing. Cosimo Oliboni, oliboni@cs.unibo.it *) -(* Ultima modifica: 05/08/2009 *) +(* Sviluppo: 2008-2010 *) (* *) (* ********************************************************************** *) @@ -104,24 +104,13 @@ nlemma neqSUN_to_neq : ∀l.∀x,y:S_UN l.eq_SUN l x y = false → x ≠ y. nqed. (* eqxx_to_eq universale *) -(* serve l'assioma di equivalenza sulle dimostrazioni *) - -naxiom eqSUN_to_eq_aux : ∀l,e.∀dim1,dim2:((member_natList e l) = true).S_EL l e dim1 = S_EL l e dim2. -(* mi dice matita/logic/equality/eq.ind not found che e' vero perche' uso il mio... - #l; #e; #dim1; #dim2; - nauto library; -*) +(* !!! evidente ma come si fa? *) +naxiom eqSUN_to_eq_aux : ∀l,x,y.((getelem l x) = (getelem l y)) → x = y. nlemma eqSUN_to_eq : ∀l.∀x,y:S_UN l.eq_SUN l x y = true → x = y. - #l; #x; nelim x; - #u1; #dim1; - #y; nelim y; - #u2; #dim2; - nchange with ((eq_nat u1 u2 = true) → ?); - #H; - nrewrite > (eqnat_to_eq u1 u2 H) in dim1:(%) ⊢ %; - #dim1; - napply eqSUN_to_eq_aux. + #l; #x; #y; + nchange with ((eq_nat (getelem ? x) (getelem ? y) = true) → x = y); + #H; napply (eqSUN_to_eq_aux l x y (eqnat_to_eq … H)). nqed. (* neq_to_neqxx universale *) @@ -200,13 +189,13 @@ nlet rec farg2 (T:Type) (l,lfix:ne_list nat) on l ≝ (* esempio0: universo ottale *) ndefinition oct0 ≝ O. -ndefinition oct1 ≝ S O. -ndefinition oct2 ≝ S (S O). -ndefinition oct3 ≝ S (S (S O)). -ndefinition oct4 ≝ S (S (S (S O))). -ndefinition oct5 ≝ S (S (S (S (S O)))). -ndefinition oct6 ≝ S (S (S (S (S (S O))))). -ndefinition oct7 ≝ S (S (S (S (S (S (S O)))))). +ndefinition oct1 ≝ nat1. +ndefinition oct2 ≝ nat2. +ndefinition oct3 ≝ nat3. +ndefinition oct4 ≝ nat4. +ndefinition oct5 ≝ nat5. +ndefinition oct6 ≝ nat6. +ndefinition oct7 ≝ nat7. ndefinition oct_UN ≝ « oct0 ; oct1 ; oct2 ; oct3 ; oct4 ; oct5 ; oct6 £ oct7 ». -- 2.39.2