From: Cosimo Oliboni <??>
Date: Wed, 29 Jul 2009 16:30:44 +0000 (+0000)
Subject:  freescale porting, work in progress
X-Git-Tag: make_still_working~3597
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=842e243be954d67360788d08701289f3237c2699;p=helm.git

 freescale porting, work in progress
---

diff --git a/helm/software/matita/contribs/ng_assembly/freescale/load_write.ma b/helm/software/matita/contribs/ng_assembly/freescale/load_write.ma
index 5bfd406b5..766be3772 100755
--- a/helm/software/matita/contribs/ng_assembly/freescale/load_write.ma
+++ b/helm/software/matita/contribs/ng_assembly/freescale/load_write.ma
@@ -116,11 +116,11 @@ ndefinition RS08_memory_filter_read_bit ≝
 ndefinition memory_filter_read ≝
 λm:mcu_type.λt:memory_impl.match m return λm:mcu_type.any_status m t → word16 → option byte8 with
  [ HC05 ⇒ λs:any_status HC05 t.λaddr:word16.
-  mem_read t (get_mem_desc ? t s) (get_chk_desc ? t s) addr
+  mem_read t (mem_desc ? t s) (chk_desc ? t s) addr
  | HC08 ⇒ λs:any_status HC08 t.λaddr:word16.
-  mem_read t (get_mem_desc ? t s) (get_chk_desc ? t s) addr
+  mem_read t (mem_desc ? t s) (chk_desc ? t s) addr
  | HCS08 ⇒ λs:any_status HCS08 t.λaddr:word16.
-  mem_read t (get_mem_desc ? t s) (get_chk_desc ? t s) addr
+  mem_read t (mem_desc ? t s) (chk_desc ? t s) addr
  | RS08 ⇒ λs:any_status RS08 t.λaddr:word16.
   RS08_memory_filter_read t s addr
  ].
@@ -128,11 +128,11 @@ ndefinition memory_filter_read ≝
 ndefinition memory_filter_read_bit ≝
 λm:mcu_type.λt:memory_impl.match m return λm:mcu_type.any_status m t → word16 → oct → option bool with
  [ HC05 ⇒ λs:any_status HC05 t.λaddr:word16.λsub:oct.
-  mem_read_bit t (get_mem_desc ? t s) (get_chk_desc ? t s) addr sub
+  mem_read_bit t (mem_desc ? t s) (chk_desc ? t s) addr sub
  | HC08 ⇒ λs:any_status HC08 t.λaddr:word16.λsub:oct.
-  mem_read_bit t (get_mem_desc ? t s) (get_chk_desc ? t s) addr sub
+  mem_read_bit t (mem_desc ? t s) (chk_desc ? t s) addr sub
  | HCS08 ⇒ λs:any_status HCS08 t.λaddr:word16.λsub:oct.
-  mem_read_bit t (get_mem_desc ? t s) (get_chk_desc ? t s) addr sub
+  mem_read_bit t (mem_desc ? t s) (chk_desc ? t s) addr sub
  | RS08 ⇒ λs:any_status RS08 t.λaddr:word16.λsub:oct.
   RS08_memory_filter_read_bit t s addr sub
  ].
@@ -217,13 +217,13 @@ ndefinition memory_filter_write ≝
 λm:mcu_type.λt:memory_impl.match m
  return λm:mcu_type.any_status m t → word16 → byte8 → option (any_status m t) with
  [ HC05 ⇒ λs:any_status HC05 t.λaddr:word16.λval:byte8.
-  opt_map ?? (mem_update t (get_mem_desc ? t s) (get_chk_desc ? t s) addr val)
+  opt_map ?? (mem_update t (mem_desc ? t s) (chk_desc ? t s) addr val)
    (λmem.Some ? (set_mem_desc ? t s mem)) 
  | HC08 ⇒ λs:any_status HC08 t.λaddr:word16.λval:byte8.
-  opt_map ?? (mem_update t (get_mem_desc ? t s) (get_chk_desc ? t s) addr val)
+  opt_map ?? (mem_update t (mem_desc ? t s) (chk_desc ? t s) addr val)
    (λmem.Some ? (set_mem_desc ? t s mem))
  | HCS08 ⇒ λs:any_status HCS08 t.λaddr:word16.λval:byte8.
-  opt_map ?? (mem_update t (get_mem_desc ? t s) (get_chk_desc ? t s) addr val)
+  opt_map ?? (mem_update t (mem_desc ? t s) (chk_desc ? t s) addr val)
    (λmem.Some ? (set_mem_desc ? t s mem)) 
  | RS08 ⇒ λs:any_status RS08 t.λaddr:word16.λval:byte8.
   RS08_memory_filter_write t s addr val
@@ -233,13 +233,13 @@ ndefinition memory_filter_write_bit ≝
 λm:mcu_type.λt:memory_impl.match m
  return λm:mcu_type.any_status m t → word16 → oct → bool → option (any_status m t) with
  [ HC05 ⇒ λs:any_status HC05 t.λaddr:word16.λsub:oct.λval:bool.
-  opt_map ?? (mem_update_bit t (get_mem_desc ? t s) (get_chk_desc ? t s) addr sub val)
+  opt_map ?? (mem_update_bit t (mem_desc ? t s) (chk_desc ? t s) addr sub val)
    (λmem.Some ? (set_mem_desc ? t s mem)) 
  | HC08 ⇒ λs:any_status HC08 t.λaddr:word16.λsub:oct.λval:bool.
-  opt_map ?? (mem_update_bit t (get_mem_desc ? t s) (get_chk_desc ? t s) addr sub val)
+  opt_map ?? (mem_update_bit t (mem_desc ? t s) (chk_desc ? t s) addr sub val)
    (λmem.Some ? (set_mem_desc ? t s mem))
  | HCS08 ⇒ λs:any_status HCS08 t.λaddr:word16.λsub:oct.λval:bool.
-  opt_map ?? (mem_update_bit t (get_mem_desc ? t s) (get_chk_desc ? t s) addr sub val)
+  opt_map ?? (mem_update_bit t (mem_desc ? t s) (chk_desc ? t s) addr sub val)
    (λmem.Some ? (set_mem_desc ? t s mem)) 
  | RS08 ⇒ λs:any_status RS08 t.λaddr:word16.λsub:oct.λval:bool.
   RS08_memory_filter_write_bit t s addr sub val
diff --git a/helm/software/matita/contribs/ng_assembly/freescale/multivm.ma b/helm/software/matita/contribs/ng_assembly/freescale/multivm.ma
index fc374d9ab..e0277386c 100755
--- a/helm/software/matita/contribs/ng_assembly/freescale/multivm.ma
+++ b/helm/software/matita/contribs/ng_assembly/freescale/multivm.ma
@@ -1268,7 +1268,7 @@ ndefinition tick_execute ≝
 
 ndefinition tick ≝
 λm:mcu_type.λt:memory_impl.λs:any_status m t.
- let opt_info ≝ get_clk_desc m t s in
+ let opt_info ≝ clk_desc m t s in
  match opt_info with
   (* e' il momento del fetch *)
   [ None ⇒ match fetch m t s with
diff --git a/helm/software/matita/contribs/ng_assembly/freescale/status.ma b/helm/software/matita/contribs/ng_assembly/freescale/status.ma
index e6d42deed..6a0f81887 100755
--- a/helm/software/matita/contribs/ng_assembly/freescale/status.ma
+++ b/helm/software/matita/contribs/ng_assembly/freescale/status.ma
@@ -165,7 +165,6 @@ nrecord any_status (mcu:mcu_type) (t:memory_impl): Type ≝
  clk_desc : option (Prod5T byte8 (any_opcode mcu) (instr_mode) byte8 word16)
  }.
 
-
 (* evitare di mostrare la memoria/descrittore che impalla il visualizzatore *)
 notation > "{hvbox('Alu' ≝ alu ; break 'Clk' ≝ clk)}" non associative with precedence 80 
  for @{ 'mk_any_status $alu $mem $chk $clk }.
@@ -362,20 +361,6 @@ ndefinition get_irq_flag ≝
  | RS08 ⇒ λalu.None ? ]
  (alu m t s).
 
-(* DESCRITTORI ESTERNI ALLA ALU *)
-
-(* getter della ALU, esiste sempre *)
-ndefinition get_alu ≝ λm:mcu_type.λt:memory_impl.λs:any_status m t.alu m t s.
-
-(* getter della memoria, esiste sempre *)
-ndefinition get_mem_desc ≝ λm:mcu_type.λt:memory_impl.λs:any_status m t.mem_desc m t s.
-
-(* getter del descrittore, esiste sempre *)
-ndefinition get_chk_desc ≝ λm:mcu_type.λt:memory_impl.λs:any_status m t.chk_desc m t s.
-
-(* getter del clik, esiste sempre *)
-ndefinition get_clk_desc ≝ λm:mcu_type.λt:memory_impl.λs:any_status m t.clk_desc m t s.
-
 (* ***************************** *)
 (* SETTER SPECIFICI FORTI/DEBOLI *)
 (* ***************************** *)
@@ -397,23 +382,23 @@ ndefinition aux_set_typing_opt ≝ λx:Type.λm:mcu_type.option
 (* setter forte della ALU *)
 ndefinition set_alu ≝
 λm:mcu_type.λt:memory_impl.λs:any_status m t.λalu'.
- mk_any_status m t alu' (get_mem_desc m t s) (get_chk_desc m t s) (get_clk_desc m t s).
+ mk_any_status m t alu' (mem_desc m t s) (chk_desc m t s) (clk_desc m t s).
 
 (* setter forte della memoria *)
 ndefinition set_mem_desc ≝
 λm:mcu_type.λt:memory_impl.λs:any_status m t.λmem':aux_mem_type t.
- mk_any_status m t (get_alu m t s) mem' (get_chk_desc m t s) (get_clk_desc m t s).
+ mk_any_status m t (alu m t s) mem' (chk_desc m t s) (clk_desc m t s).
 
 (* setter forte del descrittore *)
 ndefinition set_chk_desc ≝
 λm:mcu_type.λt:memory_impl.λs:any_status m t.λchk':aux_chk_type t.
- mk_any_status m t (get_alu m t s) (get_mem_desc m t s) chk' (get_clk_desc m t s).
+ mk_any_status m t (alu m t s) (mem_desc m t s) chk' (clk_desc m t s).
 
 (* setter forte del clik *)
 ndefinition set_clk_desc ≝
 λm:mcu_type.λt:memory_impl.λs:any_status m t.
 λclk':option (Prod5T byte8 (any_opcode m) (instr_mode) byte8 word16).
- mk_any_status m t (get_alu m t s) (get_mem_desc m t s) (get_chk_desc m t s) clk'.
+ mk_any_status m t (alu m t s) (mem_desc m t s) (chk_desc m t s) clk'.
 
 (* REGISTRO A *)