freescale porting, work in progress

[helm.git] / helm / software / matita / contribs / ng_assembly / freescale / load_write.ma

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 5bfd406b5296052c5ca36c161a0f683706f6648a..766be3772c7c876851c37ab2f80d59200fbfb79b 100755 (executable)
--- 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