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
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
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
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
+++ /dev/null
-(**************************************************************************)
-(* ___ *)
-(* ||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_func.ma".
-include "freescale/memory_trees.ma".
-include "freescale/memory_bits.ma".
-
-(* ********************************************* *)
-(* ASTRAZIONE DALL'IMPLEMENTAZIONE DELLA MEMORIA *)
-(* ********************************************* *)
-
-(* tipi di implementazione della memoria *)
-ninductive memory_impl : Type ≝
- MEM_FUNC: memory_impl
-| MEM_TREE: memory_impl
-| MEM_BITS: memory_impl.
-
-(* 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))))
- ].
-
-(* 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))))
- ].
-
-(* unificazione di out_of_bound_memory *)
-ndefinition out_of_bound_memory ≝
-λt:memory_impl.
- match t
- return λt.aux_chk_type t
- with
- [ MEM_FUNC ⇒ mf_out_of_bound_memory
- | MEM_TREE ⇒ mt_out_of_bound_memory
- | MEM_BITS ⇒ mb_out_of_bound_memory
- ].
-
-(* unificazione di zero_memory *)
-ndefinition zero_memory ≝
-λt:memory_impl.
- match t
- return λt.aux_mem_type t
- with
- [ MEM_FUNC ⇒ mf_zero_memory
- | MEM_TREE ⇒ mt_zero_memory
- | MEM_BITS ⇒ mb_zero_memory
- ].
-
-(* unificazione della lettura senza chk: mem_read_abs mem addr *)
-ndefinition mem_read_abs ≝
-λt:memory_impl.
- match t
- return λt.aux_mem_type t → word16 → byte8
- with
- [ MEM_FUNC ⇒ λm:aux_mem_type MEM_FUNC.
- λaddr:word16.
- m addr
- | MEM_TREE ⇒ λm:aux_mem_type MEM_TREE.
- λaddr:word16.
- mt_visit byte8 m addr
- | MEM_BITS ⇒ λm:aux_mem_type MEM_BITS.
- λaddr:word16.
- byte8_of_bits (mt_visit (Array8T bool) m addr)
- ].
-
-(* unificazione del chk *)
-ndefinition chk_get ≝
-λt:memory_impl.λc:aux_chk_type t.λaddr:word16.
- match t
- return λt.aux_chk_type t → word16 → Array8T memory_type
- with
- [ MEM_FUNC ⇒ mf_chk_get
- | MEM_TREE ⇒ mt_chk_get
- | MEM_BITS ⇒ mb_chk_get
- ] 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.
- match t
- return λt.aux_mem_type t → aux_chk_type t → word16 → option byte8
- with
- [ MEM_FUNC ⇒ mf_mem_read
- | MEM_TREE ⇒ mt_mem_read
- | MEM_BITS ⇒ mb_mem_read
- ] m c addr.
-
-(* unificazione della lettura di bit con chk: mem_read mem chk addr sub *)
-ndefinition mem_read_bit ≝
-λt:memory_impl.
- match t
- return λt.aux_mem_type t → aux_chk_type t → word16 → oct → option bool
- with
- [ MEM_FUNC ⇒ λm:aux_mem_type MEM_FUNC.
- λc:aux_chk_type MEM_FUNC.
- λaddr:word16.
- λ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.
- λ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.
- λ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.
- match t
- return λt.aux_mem_type t → Array8T memory_type → word16 → 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.
-
-(* 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)
- with
- [ MEM_FUNC ⇒ λm:aux_mem_type MEM_FUNC.
- λc:aux_chk_type MEM_FUNC.
- λaddr:word16.
- λ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)))
- | MEM_TREE ⇒ λm:aux_mem_type MEM_TREE.
- λc:aux_chk_type MEM_TREE.
- λaddr:word16.
- λ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)))
- | MEM_BITS ⇒ λm:aux_mem_type MEM_BITS.
- λc:aux_chk_type MEM_BITS.
- λaddr:word16.
- λo:oct.
- λv:bool.
- mb_mem_update_bit m c addr o v
- ].
-
-(* 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.
- match t
- return λt.aux_mem_type t → list byte8 → word16 → aux_mem_type t
- with
- [ MEM_FUNC ⇒ mf_load_from_source_at
- | MEM_TREE ⇒ mt_load_from_source_at
- | MEM_BITS ⇒ mb_load_from_source_at
- ] m l addr.
-
-(* unificazione dell'impostazione della memoria: chk_update_ranged chk inf sup v *)
-ndefinition check_update_ranged ≝
-λt:memory_impl.
- match t
- return λt.aux_chk_type t → word16 → word16 → memory_type → aux_chk_type t
- with
- [ MEM_FUNC ⇒ λc:aux_chk_type MEM_FUNC.
- λinf,sup:word16.
- λv:memory_type.
- mf_check_update_ranged c inf sup v
- | MEM_TREE ⇒ λc:aux_chk_type MEM_TREE.
- λinf,sup:word16.
- λv:memory_type.
- mt_update_ranged memory_type c inf sup v
- | MEM_BITS ⇒ λc:aux_chk_type MEM_BITS.
- λinf,sup: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)
- ].
-
-(* unificazione dell'impostazione dei bit: chk_update_bit chk addr sub v *)
-(* NB: dove non esiste la granularita' del bit, lascio inalterato *)
-ndefinition check_update_bit ≝
-λt:memory_impl.
- match t
- return λt.aux_chk_type t → word16 → oct → memory_type → aux_chk_type t
- with
- [ MEM_FUNC ⇒ λc:aux_chk_type MEM_FUNC.
- λaddr:word16.
- λo:oct.
- λv:memory_type.
- c
- | MEM_TREE ⇒ λc:aux_chk_type MEM_TREE.
- λaddr:word16.
- λo:oct.
- λv:memory_type.
- c
- | MEM_BITS ⇒ λc:aux_chk_type MEM_BITS.
- λaddr:word16.
- λo:oct.
- λv:memory_type.
- mb_chk_update_bit c addr o v
- ].
+++ /dev/null
-(**************************************************************************)
-(* ___ *)
-(* ||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_trees.ma".
-
-(* ********************* *)
-(* MEMORIA E DESCRITTORE *)
-(* ********************* *)
-
-(* 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.
-
-(* 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.
-
-(* 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
- (* 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))
- (* 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.
-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
- [ 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
- [ 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
- [ 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
- [ 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
- [ 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
- [ 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
- [ 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
- [ MEM_READ_ONLY ⇒ Some bool (getn_array8T o7 bool old_value)
- | MEM_READ_WRITE ⇒ Some bool (getn_array8T o7 bool new_value)
- | MEM_OUT_OF_BOUND ⇒ None bool ] in
- opt_map … newbit0
- (λnb0.opt_map … newbit1
- (λnb1.opt_map … newbit2
- (λnb2.opt_map … newbit3
- (λnb3.opt_map … newbit4
- (λnb4.opt_map … newbit5
- (λnb5.opt_map … newbit6
- (λnb6.opt_map … newbit7
- (λnb7.Some ? (mt_update (Array8T bool) mem addr (array_8T bool nb7 nb6 nb5 nb4 nb3 nb2 nb1 nb0)))))))))).
-
-(* leggi controllando il tipo di memoria *)
-(* 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
-let value ≝ mt_visit (Array8T bool) mem addr in
-let newbit0 ≝ match getn_array8T o0 memory_type bit_types 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
- [ 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
- [ 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
- [ 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
- [ 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
- [ 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
- [ 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
- [ MEM_READ_ONLY ⇒ Some bool (getn_array8T o7 bool value)
- | MEM_READ_WRITE ⇒ Some bool (getn_array8T o7 bool value)
- | MEM_OUT_OF_BOUND ⇒ None bool ] in
- opt_map … newbit0
- (λnb0.opt_map … newbit1
- (λnb1.opt_map … newbit2
- (λnb2.opt_map … newbit3
- (λnb3.opt_map … newbit4
- (λnb4.opt_map … newbit5
- (λnb5.opt_map … newbit6
- (λnb6.opt_map … newbit7
- (λnb7.Some ? (byte8_of_bits (array_8T 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 ≝
- 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〉〉)
- ].
+++ /dev/null
-(**************************************************************************)
-(* ___ *)
-(* ||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 *)
-(* ********************* *)
-
-(* (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
- [ 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
- ].
-
-(* (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
- (* 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 ])
- (* NON INSTALLATA? no *)
- | MEM_OUT_OF_BOUND ⇒ None ? ].
-
-(* tutta la memoria a 0 *)
-ndefinition mf_zero_memory ≝ λ_:word16.〈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.
- match c a with
- [ MEM_READ_ONLY ⇒ Some ? (f a)
- | MEM_READ_WRITE ⇒ Some ? (f a)
- | MEM_OUT_OF_BOUND ⇒ None ? ].
-
-(* ************************** *)
-(* CARICAMENTO PROGRAMMA/DATI *)
-(* ************************** *)
-
-(* 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 ≝
- match src with
- (* fine di source: carica da old_mem *)
- [ nil ⇒ old_mem
- | cons hd tl ⇒ λx:word16.match eq_w16 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
- ]
- ].
+++ /dev/null
-(**************************************************************************)
-(* ___ *)
-(* ||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 ]
- ].
+++ /dev/null
-(**************************************************************************)
-(* ___ *)
-(* ||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〉〉)
- ].
(* *)
(* ********************************************************************** *)
-include "freescale/memory_abs.ma".
+include "memory/memory_abs.ma".
include "freescale/opcode_base.ma".
(* *********************************** *)
--- /dev/null
+(**************************************************************************)
+(* ___ *)
+(* ||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_func.ma".
+include "memory/memory_trees.ma".
+include "memory/memory_bits.ma".
+
+(* ********************************************* *)
+(* ASTRAZIONE DALL'IMPLEMENTAZIONE DELLA MEMORIA *)
+(* ********************************************* *)
+
+(* tipi di implementazione della memoria *)
+ninductive memory_impl : Type ≝
+ MEM_FUNC: memory_impl
+| MEM_TREE: memory_impl
+| MEM_BITS: memory_impl.
+
+(* ausiliario per il tipo della memoria *)
+ndefinition aux_mem_type ≝
+λt:memory_impl.match t with
+ [ 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 ⇒ word32 → memory_type
+ | MEM_TREE ⇒ aux_32B_type memory_type
+ | MEM_BITS ⇒ aux_32B_type (Array8T memory_type)
+ ].
+
+(* unificazione di out_of_bound_memory *)
+ndefinition out_of_bound_memory ≝
+λt:memory_impl.
+ match t
+ return λt.aux_chk_type t
+ with
+ [ MEM_FUNC ⇒ mf_out_of_bound_memory
+ | MEM_TREE ⇒ mt_out_of_bound_memory
+ | MEM_BITS ⇒ mb_out_of_bound_memory
+ ].
+
+(* unificazione di zero_memory *)
+ndefinition zero_memory ≝
+λt:memory_impl.
+ match t
+ return λt.aux_mem_type t
+ with
+ [ MEM_FUNC ⇒ mf_zero_memory
+ | MEM_TREE ⇒ mt_zero_memory
+ | MEM_BITS ⇒ mb_zero_memory
+ ].
+
+(* unificazione della lettura senza chk: mem_read_abs mem addr *)
+ndefinition mem_read_abs ≝
+λt:memory_impl.
+ match t
+ return λt.aux_mem_type t → word32 → byte8
+ with
+ [ MEM_FUNC ⇒ λm:aux_mem_type MEM_FUNC.
+ λaddr:word32.
+ m addr
+ | MEM_TREE ⇒ λm:aux_mem_type MEM_TREE.
+ λaddr:word32.
+ mt_visit ? m addr
+ | MEM_BITS ⇒ λm:aux_mem_type MEM_BITS.
+ λaddr:word32.
+ byte8_of_bits (mt_visit ? m addr)
+ ].
+
+(* unificazione del chk *)
+ndefinition chk_get ≝
+λt:memory_impl.
+ match t
+ return λt.aux_chk_type t → word32 → Array8T memory_type
+ with
+ [ 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:word32.
+ match t
+ return λt.aux_mem_type t → aux_chk_type t → word32 → option byte8
+ with
+ [ MEM_FUNC ⇒ mf_mem_read
+ | MEM_TREE ⇒ mt_mem_read
+ | MEM_BITS ⇒ mb_mem_read
+ ] m c addr.
+
+(* unificazione della lettura di bit con chk: mem_read mem chk addr sub *)
+ndefinition mem_read_bit ≝
+λt:memory_impl.
+ match t
+ 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: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: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: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:word32.λv:byte8.
+ match 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 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 → word32 → oct → bool → option (aux_mem_type t)
+ with
+ [ MEM_FUNC ⇒ λm:aux_mem_type MEM_FUNC.
+ λc:aux_chk_type MEM_FUNC.
+ λaddr:word32.
+ λo:oct.
+ λv:bool.
+ 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:word32.
+ λo:oct.
+ λv:bool.
+ 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:word32.
+ λo:oct.
+ λv:bool.
+ mb_mem_update_bit m c addr o v
+ ].
+
+(* 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:word32.
+ match 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
+ | MEM_BITS ⇒ mb_load_from_source_at
+ ] m l addr.
+
+(* unificazione dell'impostazione della memoria: chk_update_ranged chk inf sup v *)
+ndefinition check_update_ranged ≝
+λt:memory_impl.
+ match t
+ return λt.aux_chk_type t → word32 → word16 → memory_type → aux_chk_type t
+ with
+ [ MEM_FUNC ⇒ λc:aux_chk_type MEM_FUNC.
+ λaddr:word32.
+ λrange:word16.
+ λv:memory_type.
+ mf_check_update_ranged c addr range v
+ | MEM_TREE ⇒ λc:aux_chk_type MEM_TREE.
+ λaddr:word32.
+ λrange:word16.
+ λv:memory_type.
+ mt_update_ranged ? c addr ? (w16_to_recw16 range) v
+ | MEM_BITS ⇒ λc:aux_chk_type MEM_BITS.
+ λaddr:word32.
+ λrange:word16.
+ λv:memory_type.
+ 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 *)
+(* NB: dove non esiste la granularita' del bit, lascio inalterato *)
+ndefinition check_update_bit ≝
+λt:memory_impl.
+ match 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:word32.
+ λo:oct.
+ λv:memory_type.
+ c
+ | MEM_TREE ⇒ λc:aux_chk_type MEM_TREE.
+ λaddr:word32.
+ λo:oct.
+ λv:memory_type.
+ c
+ | MEM_BITS ⇒ λc:aux_chk_type MEM_BITS.
+ λaddr:word32.
+ λo:oct.
+ λv:memory_type.
+ mb_chk_update_bit c addr o v
+ ].
--- /dev/null
+(**************************************************************************)
+(* ___ *)
+(* ||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_trees.ma".
+
+(* ********************* *)
+(* MEMORIA E DESCRITTORE *)
+(* ********************* *)
+
+(* tutta la memoria non installata *)
+ndefinition mb_out_of_bound_memory ≝
+ 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 ≝
+ 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: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 ? mem addr (setn_array8T sub ? (mt_visit ? mem addr) v))
+ (* NON INSTALLATA? no *)
+ | MEM_OUT_OF_BOUND ⇒ None ? ].
+
+ndefinition mb_mem_update ≝
+λ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 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 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 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 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 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 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 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 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
+ opt_map … newbit0
+ (λnb0.opt_map … newbit1
+ (λnb1.opt_map … newbit2
+ (λnb2.opt_map … newbit3
+ (λnb3.opt_map … newbit4
+ (λnb4.opt_map … newbit5
+ (λnb5.opt_map … newbit6
+ (λnb6.opt_map … newbit7
+ (λnb7.Some ? (mt_update ? 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:aux_32B_type (Array8T bool).
+λchk:aux_32B_type (Array8T memory_type).
+λaddr:word32.
+let value ≝ mt_visit (Array8T bool) mem addr in
+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 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 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 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 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 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 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 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
+ opt_map … newbit0
+ (λnb0.opt_map … newbit1
+ (λnb1.opt_map … newbit2
+ (λnb2.opt_map … newbit3
+ (λnb3.opt_map … newbit4
+ (λnb4.opt_map … newbit5
+ (λnb5.opt_map … newbit6
+ (λnb6.opt_map … newbit7
+ (λnb7.Some ? (byte8_of_bits (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: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 (succ_w32 addr)
+ ].
--- /dev/null
+(**************************************************************************)
+(* ___ *)
+(* ||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 *)
+(* ********************* *)
+
+(* (mf_check_update_ranged chk inf sup mode) = setta tipo memoria *)
+ndefinition mf_check_update_ranged ≝
+λ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 ≝ λ_:word32.MEM_OUT_OF_BOUND.
+
+(* (mf_mem_update mem checked addr val) = scrivi controllando il tipo di memoria *)
+ndefinition mf_mem_update ≝
+λ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_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 ≝ λ_:word32.〈x0,x0〉.
+
+(* (mf_mem_read mem check addr) = leggi controllando il tipo di memoria *)
+ndefinition mf_mem_read ≝
+λf:word32 → byte8.λc:word32 → memory_type.λa.
+ match c a with
+ [ MEM_READ_ONLY ⇒ Some ? (f a)
+ | MEM_READ_WRITE ⇒ Some ? (f a)
+ | MEM_OUT_OF_BOUND ⇒ None ? ].
+
+(* ************************** *)
+(* CARICAMENTO PROGRAMMA/DATI *)
+(* ************************** *)
+
+(* carica a paratire da addr, overflow se si supera 0xFFFF... *)
+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: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_w32_d_d addr 〈〈〈x0,x0〉:〈x0,x0〉〉.〈〈x0,x0〉:〈x0,x1〉〉〉)) x
+ ]
+ ].
--- /dev/null
+(**************************************************************************)
+(* ___ *)
+(* ||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 ]
+ ].
--- /dev/null
+(**************************************************************************)
+(* ___ *)
+(* ||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)
+ ].
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 ≝
| 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.
(* 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 ≝
(* 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 ≝
(* Progetto FreeScale *)
(* *)
(* Sviluppato da: Ing. Cosimo Oliboni, oliboni@cs.unibo.it *)
-(* Ultima modifica: 05/08/2009 *)
+(* Sviluppo: 2008-2010 *)
(* *)
(* ********************************************************************** *)
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 *)
(* 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 ».
projects / helm.git / commitdiff