X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2Fcontribs%2Fng_assembly%2Ffreescale%2Fmemory_func.ma;fp=helm%2Fsoftware%2Fmatita%2Fcontribs%2Fng_assembly%2Ffreescale%2Fmemory_func.ma;h=0000000000000000000000000000000000000000;hb=ce3886fa05ff0a2fbd4d7b6cf68225d90686eafe;hp=8ab90d06f8632ead2e0146e8fdcf222ff28ece2d;hpb=17c6ac2888a1f30aee059f5cf6b8872bb4f3ab61;p=helm.git

diff --git a/helm/software/matita/contribs/ng_assembly/freescale/memory_func.ma b/helm/software/matita/contribs/ng_assembly/freescale/memory_func.ma
deleted file mode 100755
index 8ab90d06f..000000000
--- a/helm/software/matita/contribs/ng_assembly/freescale/memory_func.ma
+++ /dev/null
@@ -1,91 +0,0 @@
-(**************************************************************************)
-(*       ___                                                              *)
-(*      ||M||                                                             *)
-(*      ||A||       A project by Andrea Asperti                           *)
-(*      ||T||                                                             *)
-(*      ||I||       Developers:                                           *)
-(*      ||T||         The HELM team.                                      *)
-(*      ||A||         http://helm.cs.unibo.it                             *)
-(*      \   /                                                             *)
-(*       \ /        This file is distributed under the terms of the       *)
-(*        v         GNU General Public License Version 2                  *)
-(*                                                                        *)
-(**************************************************************************)
-
-(* ********************************************************************** *)
-(*                          Progetto FreeScale                            *)
-(*                                                                        *)
-(*   Sviluppato da: Cosimo Oliboni, oliboni@cs.unibo.it                   *)
-(*     Cosimo Oliboni, oliboni@cs.unibo.it                                *)
-(*                                                                        *)
-(* ********************************************************************** *)
-
-include "freescale/memory_struct.ma".
-include "freescale/word16.ma".
-include "freescale/option.ma".
-include "freescale/theory.ma".
-
-(* ********************* *)
-(* MEMORIA E DESCRITTORE *)
-(* ********************* *)
-
-(* (mf_check_update_ranged chk inf sup mode) = setta tipo memoria *)
-ndefinition mf_check_update_ranged ≝
-λf:word16 → memory_type.λi.λs.λv.
- λx.match in_range x i s 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, scartando source (pescando da old_mem) se si supera 0xFFFF... *)
-nlet rec mf_load_from_source_at (old_mem:word16 → byte8) (source:list byte8) (addr:word16) on source ≝
-match source with
- (* fine di source: carica da old_mem *)
- [ nil ⇒ old_mem
- | cons hd tl ⇒ λx:word16.match lt_w16 x addr with
-  (* e' prima di source: carica da old_mem *)
-  [ true ⇒ old_mem x
-  | false ⇒ match eq_w16 x addr 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
-   ]
-  ]
- ].