+++ /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: Cosimo Oliboni, oliboni@cs.unibo.it *)
-(* Cosimo Oliboni, oliboni@cs.unibo.it *)
-(* *)
-(* ********************************************************************** *)
-
-include "freescale/oct.ma".
-include "freescale/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 ]
- ].
projects / helm.git / blobdiff