From 417792b30223b5edd4a9194193c7f34514bd0fa3 Mon Sep 17 00:00:00 2001
From: Cosimo Oliboni <??>
Date: Thu, 3 Sep 2009 22:39:31 +0000
Subject: [PATCH]  freescale porting, work in progress

---
 .../ng_assembly/common/list_utility.ma        |   2 +-
 .../matita/contribs/ng_assembly/common/nat.ma | 114 ++++++++++++++++++
 .../contribs/ng_assembly/common/nat_to_num.ma |  14 +--
 .../contribs/ng_assembly/compiler/ast_type.ma |   8 +-
 .../ng_assembly/compiler/environment.ma       |  72 +++++++++++
 .../matita/contribs/ng_assembly/depends       |   1 +
 .../ng_assembly/freescale/load_write.ma       |  36 +++---
 .../freescale_tests/medium_tests.ma           |  16 +--
 .../freescale_tests/micro_tests.ma            |   5 +-
 .../matita/contribs/ng_assembly/num/word16.ma |   2 +-
 .../matita/contribs/ng_assembly/num/word32.ma |   2 +-
 11 files changed, 231 insertions(+), 41 deletions(-)
 create mode 100755 helm/software/matita/contribs/ng_assembly/compiler/environment.ma

diff --git a/helm/software/matita/contribs/ng_assembly/common/list_utility.ma b/helm/software/matita/contribs/ng_assembly/common/list_utility.ma
index ae40ba75d..ce118e74c 100755
--- a/helm/software/matita/contribs/ng_assembly/common/list_utility.ma
+++ b/helm/software/matita/contribs/ng_assembly/common/list_utility.ma
@@ -188,7 +188,7 @@ nlet rec abs_list (T:Type) (l:list T) on l ≝
 
 (* listlen *)
 nlet rec len_neList (T:Type) (nl:ne_list T) on nl ≝
- match nl with [ ne_nil _ ⇒ 1 | ne_cons _ t ⇒ S (len_neList T t) ].
+ match nl with [ ne_nil _ ⇒ (S O) | ne_cons _ t ⇒ S (len_neList T t) ].
 
 (* reverse *)
 nlet rec reverse_neList (T:Type) (nl:ne_list T) on nl ≝
diff --git a/helm/software/matita/contribs/ng_assembly/common/nat.ma b/helm/software/matita/contribs/ng_assembly/common/nat.ma
index 9188bef9e..12ca65afe 100755
--- a/helm/software/matita/contribs/ng_assembly/common/nat.ma
+++ b/helm/software/matita/contribs/ng_assembly/common/nat.ma
@@ -38,6 +38,107 @@ default "natural numbers" cic:/matita/common/nat/nat.ind.
 alias num (instance 0) = "natural number".
 *)
 
+ndefinition nat1 ≝ S O.
+ndefinition nat2 ≝ S nat1.
+ndefinition nat3 ≝ S nat2.
+ndefinition nat4 ≝ S nat3.
+ndefinition nat5 ≝ S nat4.
+ndefinition nat6 ≝ S nat5.
+ndefinition nat7 ≝ S nat6.
+ndefinition nat8 ≝ S nat7.
+ndefinition nat9 ≝ S nat8.
+ndefinition nat10 ≝ S nat9.
+ndefinition nat11 ≝ S nat10.
+ndefinition nat12 ≝ S nat11.
+ndefinition nat13 ≝ S nat12.
+ndefinition nat14 ≝ S nat13.
+ndefinition nat15 ≝ S nat14.
+ndefinition nat16 ≝ S nat15.
+ndefinition nat17 ≝ S nat16.
+ndefinition nat18 ≝ S nat17.
+ndefinition nat19 ≝ S nat18.
+ndefinition nat20 ≝ S nat19.
+ndefinition nat21 ≝ S nat20.
+ndefinition nat22 ≝ S nat21.
+ndefinition nat23 ≝ S nat22.
+ndefinition nat24 ≝ S nat23.
+ndefinition nat25 ≝ S nat24.
+ndefinition nat26 ≝ S nat25.
+ndefinition nat27 ≝ S nat26.
+ndefinition nat28 ≝ S nat27.
+ndefinition nat29 ≝ S nat28.
+ndefinition nat30 ≝ S nat29.
+ndefinition nat31 ≝ S nat30.
+ndefinition nat32 ≝ S nat31.
+ndefinition nat33 ≝ S nat32.
+ndefinition nat34 ≝ S nat33.
+ndefinition nat35 ≝ S nat34.
+ndefinition nat36 ≝ S nat35.
+ndefinition nat37 ≝ S nat36.
+ndefinition nat38 ≝ S nat37.
+ndefinition nat39 ≝ S nat38.
+ndefinition nat40 ≝ S nat39.
+ndefinition nat41 ≝ S nat40.
+ndefinition nat42 ≝ S nat41.
+ndefinition nat43 ≝ S nat42.
+ndefinition nat44 ≝ S nat43.
+ndefinition nat45 ≝ S nat44.
+ndefinition nat46 ≝ S nat45.
+ndefinition nat47 ≝ S nat46.
+ndefinition nat48 ≝ S nat47.
+ndefinition nat49 ≝ S nat48.
+ndefinition nat50 ≝ S nat49.
+ndefinition nat51 ≝ S nat50.
+ndefinition nat52 ≝ S nat51.
+ndefinition nat53 ≝ S nat52.
+ndefinition nat54 ≝ S nat53.
+ndefinition nat55 ≝ S nat54.
+ndefinition nat56 ≝ S nat55.
+ndefinition nat57 ≝ S nat56.
+ndefinition nat58 ≝ S nat57.
+ndefinition nat59 ≝ S nat58.
+ndefinition nat60 ≝ S nat59.
+ndefinition nat61 ≝ S nat60.
+ndefinition nat62 ≝ S nat61.
+ndefinition nat63 ≝ S nat62.
+ndefinition nat64 ≝ S nat63.
+ndefinition nat65 ≝ S nat64.
+ndefinition nat66 ≝ S nat65.
+ndefinition nat67 ≝ S nat66.
+ndefinition nat68 ≝ S nat67.
+ndefinition nat69 ≝ S nat68.
+ndefinition nat70 ≝ S nat69.
+ndefinition nat71 ≝ S nat70.
+ndefinition nat72 ≝ S nat71.
+ndefinition nat73 ≝ S nat72.
+ndefinition nat74 ≝ S nat73.
+ndefinition nat75 ≝ S nat74.
+ndefinition nat76 ≝ S nat75.
+ndefinition nat77 ≝ S nat76.
+ndefinition nat78 ≝ S nat77.
+ndefinition nat79 ≝ S nat78.
+ndefinition nat80 ≝ S nat79.
+ndefinition nat81 ≝ S nat80.
+ndefinition nat82 ≝ S nat81.
+ndefinition nat83 ≝ S nat82.
+ndefinition nat84 ≝ S nat83.
+ndefinition nat85 ≝ S nat84.
+ndefinition nat86 ≝ S nat85.
+ndefinition nat87 ≝ S nat86.
+ndefinition nat88 ≝ S nat87.
+ndefinition nat89 ≝ S nat88.
+ndefinition nat90 ≝ S nat89.
+ndefinition nat91 ≝ S nat90.
+ndefinition nat92 ≝ S nat91.
+ndefinition nat93 ≝ S nat92.
+ndefinition nat94 ≝ S nat93.
+ndefinition nat95 ≝ S nat94.
+ndefinition nat96 ≝ S nat95.
+ndefinition nat97 ≝ S nat96.
+ndefinition nat98 ≝ S nat97.
+ndefinition nat99 ≝ S nat98.
+ndefinition nat100 ≝ S nat99.
+
 nlet rec eq_nat (n1,n2:nat) on n1 ≝
  match n1 with
   [ O ⇒ match n2 with [ O ⇒ true | S _ ⇒ false ]
@@ -103,3 +204,16 @@ ndefinition div : nat → nat → nat ≝
  | (S p) ⇒ div_aux n n p]. 
 
 interpretation "natural divide" 'divide x y = (div x y).
+
+ndefinition pred ≝ λn.match n with [ O ⇒ O | S n ⇒ n ].
+
+ndefinition nat128 ≝ nat64 * nat2.
+ndefinition nat256 ≝ nat128 * nat2.
+ndefinition nat512 ≝ nat256 * nat2.
+ndefinition nat1024 ≝ nat512 * nat2.
+ndefinition nat2048 ≝ nat1024 * nat2.
+ndefinition nat4096 ≝ nat2048 * nat2.
+ndefinition nat8192 ≝ nat4096 * nat2.
+ndefinition nat16384 ≝ nat8192 * nat2.
+ndefinition nat32768 ≝ nat16384 * nat2.
+ndefinition nat65536 ≝ nat32768 * nat2.
diff --git a/helm/software/matita/contribs/ng_assembly/common/nat_to_num.ma b/helm/software/matita/contribs/ng_assembly/common/nat_to_num.ma
index 6ea1507af..e7665864f 100755
--- a/helm/software/matita/contribs/ng_assembly/common/nat_to_num.ma
+++ b/helm/software/matita/contribs/ng_assembly/common/nat_to_num.ma
@@ -29,7 +29,7 @@ include "num/word32.ma".
 
 nlet rec nat_of_qu_aux n (r:rec_quatern n) on r ≝
  match r with
-  [ qu_O ⇒ 0
+  [ qu_O ⇒ O
   | qu_S t n' ⇒ S (nat_of_qu_aux t n')
   ].
 
@@ -37,7 +37,7 @@ ndefinition nat_of_qu : quatern → nat ≝ λn.nat_of_qu_aux n (qu_to_recqu n).
 
 nlet rec nat_of_oct_aux n (r:rec_oct n) on r ≝
  match r with
-  [ oc_O ⇒ 0
+  [ oc_O ⇒ O
   | oc_S t n' ⇒ S (nat_of_oct_aux t n')
   ].
 
@@ -45,7 +45,7 @@ ndefinition nat_of_oct : oct → nat ≝ λn.nat_of_oct_aux n (oct_to_recoct n).
 
 nlet rec nat_of_ex_aux n (r:rec_exadecim n) on r ≝
  match r with
-  [ ex_O ⇒ 0
+  [ ex_O ⇒ O
   | ex_S t n' ⇒ S (nat_of_ex_aux t n')
   ].
 
@@ -53,7 +53,7 @@ ndefinition nat_of_ex : exadecim → nat ≝ λn.nat_of_ex_aux n (ex_to_recex n)
 
 nlet rec nat_of_bit_aux n (r:rec_bitrigesim n) on r ≝
  match r with
-  [ bi_O ⇒ 0
+  [ bi_O ⇒ O
   | bi_S t n' ⇒ S (nat_of_bit_aux t n')
   ].
 
@@ -61,7 +61,7 @@ ndefinition nat_of_bit : bitrigesim → nat ≝ λn.nat_of_bit_aux n (bit_to_rec
 
 nlet rec nat_of_b8_aux n (r:rec_byte8 n) on r ≝
  match r with
-  [ b8_O ⇒ 0
+  [ b8_O ⇒ O
   | b8_S t n' ⇒ S (nat_of_b8_aux t n')
   ].
 
@@ -69,10 +69,10 @@ ndefinition nat_of_b8 : byte8 → nat ≝ λn:byte8.nat_of_b8_aux n (b8_to_recb8
 
 nlet rec nat_of_w16_aux n (r:rec_word16 n) on r : nat ≝
  match r with
-  [ w16_O ⇒ 0
+  [ w16_O ⇒ O
   | w16_S t n' ⇒ S (nat_of_w16_aux t n')
   ].
 
 ndefinition nat_of_w16 : word16 → nat ≝ λn:word16.nat_of_w16_aux n (w16_to_recw16 n).
 
-ndefinition nat_of_w32 : word32 → nat ≝ λn:word32.(256*256*(nat_of_w16 (w32h n))) + (nat_of_w16 (w32l n)).
+ndefinition nat_of_w32 : word32 → nat ≝ λn:word32.(nat65536 * (nat_of_w16 (w32h n))) + (nat_of_w16 (w32l n)).
diff --git a/helm/software/matita/contribs/ng_assembly/compiler/ast_type.ma b/helm/software/matita/contribs/ng_assembly/compiler/ast_type.ma
index 8a3734104..93a66f913 100755
--- a/helm/software/matita/contribs/ng_assembly/compiler/ast_type.ma
+++ b/helm/software/matita/contribs/ng_assembly/compiler/ast_type.ma
@@ -123,14 +123,14 @@ ndefinition isntb_ast_base_type ≝
 
 ndefinition eval_size_base_type ≝
 λast:ast_base_type.match ast with
- [ AST_BASE_TYPE_BYTE8 ⇒ 1
- | AST_BASE_TYPE_WORD16 ⇒ 2
- | AST_BASE_TYPE_WORD32 ⇒ 4
+ [ AST_BASE_TYPE_BYTE8 ⇒ nat1
+ | AST_BASE_TYPE_WORD16 ⇒ nat2
+ | AST_BASE_TYPE_WORD32 ⇒ nat4
  ].
 
 nlet rec eval_size_type (ast:ast_type) on ast ≝
  match ast with
   [ AST_TYPE_BASE b ⇒ eval_size_base_type b
-  | AST_TYPE_ARRAY sub_ast dim ⇒ (dim+1)*(eval_size_type sub_ast)
+  | AST_TYPE_ARRAY sub_ast dim ⇒ (dim + nat1)*(eval_size_type sub_ast)
   | AST_TYPE_STRUCT nel_ast ⇒ fold_right_neList … (λt,x.(eval_size_type t)+x) O nel_ast
   ].
diff --git a/helm/software/matita/contribs/ng_assembly/compiler/environment.ma b/helm/software/matita/contribs/ng_assembly/compiler/environment.ma
new file mode 100755
index 000000000..73a2c8aa4
--- /dev/null
+++ b/helm/software/matita/contribs/ng_assembly/compiler/environment.ma
@@ -0,0 +1,72 @@
+(**************************************************************************)
+(*       ___                                                              *)
+(*      ||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                  *)
+(*                                                                        *)
+(**************************************************************************)
+
+(* ********************************************************************** *)
+(*                                                                        *)
+(* Sviluppato da:                                                         *)
+(*   Cosimo Oliboni, oliboni@cs.unibo.it                                  *)
+(*                                                                        *)
+(* ********************************************************************** *)
+
+include "common/string.ma".
+include "compiler/ast_type.ma".
+
+(* ***************** *)
+(* GESTIONE AMBIENTE *)
+(* ***************** *)
+
+(* elemento: name + const + type *)
+nrecord envDsc : Type ≝
+ {
+ nameDsc: aux_str_type;
+ constDsc: bool;
+ typeDsc: ast_type
+ }.
+
+(* ambiente globale: (ambiente base + ambienti annidati) *)
+ninductive env_list : nat → Type ≝
+  env_nil: list envDsc → env_list O
+| env_cons: ∀n.list envDsc → env_list n → env_list (S n).
+
+(* sto cercando di emulare "inversion e" *)
+nlemma inv_envList :
+ ∀n.∀e:env_list n.∀P:Prop.
+ (n = (match e with [ env_nil _ ⇒ O | env_cons n' _ _ ⇒ S n' ]) → P) → P.
+ #n; #e;
+ ncases e;
+ nnormalize;
+ ##[ ##1: #x; #P; #H;
+ ##| ##2: #x; #y; #z; #P; #H;
+ ##]
+ napply (H (refl_eq …)).
+nqed.
+
+ndefinition defined_envList ≝
+λd.λl:env_list d.match l with [ env_nil _ ⇒ False | env_cons _ _ _ ⇒ True ].
+
+(* bisogna dimostrare "defined_envList (S ...)"
+   impossibile anche cercando di usare l'emulazione di inversion
+*)
+ndefinition cut_first_envList_aux : Πd.env_list (S d) → env_list d ≝
+λd.λl:env_list (S d).
+  match l
+   return λX.λY:env_list X.defined_envList X Y → env_list (pred X)
+  with
+   [ env_nil h ⇒ λp:defined_envList O (env_nil h).False_rect_Type0 ? p
+   | env_cons n h t ⇒ λp:defined_envList (S n) (env_cons n h t).t
+   ] ?.
+ napply (inv_envList ? l …);
+ (* se apro l, a ritroso modifica il suo parametro destro d e non dimostro piu' nulla *)
+ (* io pensavo di ottenere per env_nil l'assurdo S d = O ... *)
+ ncases l;
diff --git a/helm/software/matita/contribs/ng_assembly/depends b/helm/software/matita/contribs/ng_assembly/depends
index 8e63f959c..9e633043e 100644
--- a/helm/software/matita/contribs/ng_assembly/depends
+++ b/helm/software/matita/contribs/ng_assembly/depends
@@ -28,6 +28,7 @@ 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
 num/word32_lemmas.ma num/word16_lemmas.ma num/word32.ma
 test_errori.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
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 28704ff34..addedf2e3 100755
--- a/helm/software/matita/contribs/ng_assembly/freescale/load_write.ma
+++ b/helm/software/matita/contribs/ng_assembly/freescale/load_write.ma
@@ -391,39 +391,39 @@ ndefinition mode_IMM2_load ≝
 λm:mcu_type.λt:memory_impl.λs:any_status m t.λcur_pc:word16.
  opt_map … (memory_filter_read m t s cur_pc)
   (λbh.opt_map … (memory_filter_read m t s (filtered_inc_w16 m t s cur_pc))
-   (λbl.Some ? (triple … s (mk_word16 bh bl) (filtered_plus_w16 m t s cur_pc 2)))).
+   (λbl.Some ? (triple … s (mk_word16 bh bl) (filtered_plus_w16 m t s cur_pc nat2)))).
 
 (* lettura da [byte [curpc]]: true=DIR1 loadb, false=DIR1 loadw *)
 ndefinition mode_DIR1_load ≝
 λbyteflag:bool.λm:mcu_type.λt:memory_impl.λs:any_status m t.λcur_pc:word16.
  opt_map … (memory_filter_read m t s cur_pc)
-  (λaddr.(aux_load m t byteflag) s 〈〈x0,x0〉:addr〉 cur_pc 1).
+  (λaddr.(aux_load m t byteflag) s 〈〈x0,x0〉:addr〉 cur_pc nat1).
 
 (* lettura da [byte [curpc]]: loadbit *)
 ndefinition mode_DIR1n_load ≝
 λm:mcu_type.λt:memory_impl.λs:any_status m t.λcur_pc:word16.λsub:oct.
  opt_map … (memory_filter_read m t s cur_pc)
-  (λaddr.loadbit_from m t  s 〈〈x0,x0〉:addr〉 sub cur_pc 1).
+  (λaddr.loadbit_from m t  s 〈〈x0,x0〉:addr〉 sub cur_pc nat1).
 
 (* scrittura su [byte [curpc]]: true=DIR1 writeb, false=DIR1 writew *)
 ndefinition mode_DIR1_write ≝
 λbyteflag:bool.λm:mcu_type.λt:memory_impl.λs:any_status m t.λcur_pc:word16.
 λwritebw:match byteflag with [ true ⇒ byte8 | false ⇒ word16 ].
  opt_map … (memory_filter_read m t s cur_pc)
-  (λaddr.(aux_write m t byteflag) s 〈〈x0,x0〉:addr〉 cur_pc 1 writebw).
+  (λaddr.(aux_write m t byteflag) s 〈〈x0,x0〉:addr〉 cur_pc nat1 writebw).
 
 (* scrittura su [byte [curpc]]: writebit *)
 ndefinition mode_DIR1n_write ≝
 λm:mcu_type.λt:memory_impl.λs:any_status m t.λcur_pc:word16.λsub:oct.λwriteb:bool.
  opt_map … (memory_filter_read m t s cur_pc)
-  (λaddr.writebit_to m t s 〈〈x0,x0〉:addr〉 sub cur_pc 1 writeb).
+  (λaddr.writebit_to m t s 〈〈x0,x0〉:addr〉 sub cur_pc nat1 writeb).
 
 (* lettura da [word [curpc]]: true=DIR2 loadb, false=DIR2 loadw *)
 ndefinition mode_DIR2_load ≝
 λbyteflag:bool.λm:mcu_type.λt:memory_impl.λs:any_status m t.λcur_pc:word16.
  opt_map … (memory_filter_read m t s cur_pc)
   (λaddrh.opt_map … (memory_filter_read m t s (filtered_inc_w16 m t s cur_pc))
-   (λaddrl.(aux_load m t byteflag) s 〈addrh:addrl〉 cur_pc 2)).
+   (λaddrl.(aux_load m t byteflag) s 〈addrh:addrl〉 cur_pc nat2)).
 
 (* scrittura su [word [curpc]]: true=DIR2 writeb, false=DIR2 writew *)
 ndefinition mode_DIR2_write ≝
@@ -431,7 +431,7 @@ ndefinition mode_DIR2_write ≝
 λwritebw:match byteflag with [ true ⇒ byte8 | false ⇒ word16 ].
  opt_map … (memory_filter_read m t s cur_pc)
   (λaddrh.opt_map … (memory_filter_read m t s (filtered_inc_w16 m t s cur_pc))
-   (λaddrl.(aux_write m t byteflag) s 〈addrh:addrl〉 cur_pc 2 writebw)).
+   (λaddrl.(aux_write m t byteflag) s 〈addrh:addrl〉 cur_pc nat2 writebw)).
 
 ndefinition get_IX ≝
 λm:mcu_type.λt:memory_impl.λs:any_status m t.
@@ -445,21 +445,21 @@ ndefinition get_IX ≝
 ndefinition mode_IX0_load ≝
 λbyteflag:bool.λm:mcu_type.λt:memory_impl.λs:any_status m t.λcur_pc:word16.
  opt_map … (get_IX m t s)
-  (λaddr.(aux_load m t byteflag) s addr cur_pc 0).
+  (λaddr.(aux_load m t byteflag) s addr cur_pc O).
 
 (* scrittura su [IX]: true=IX0 writeb, false=IX0 writew *)
 ndefinition mode_IX0_write ≝
 λbyteflag:bool.λm:mcu_type.λt:memory_impl.λs:any_status m t.λcur_pc:word16.
 λwritebw:match byteflag with [ true ⇒ byte8 | false ⇒ word16 ].
  opt_map … (get_IX m t s)
-  (λaddr.(aux_write m t byteflag) s addr cur_pc 0 writebw).
+  (λaddr.(aux_write m t byteflag) s addr cur_pc O writebw).
 
 (* lettura da [IX+byte [pc]]: true=IX1 loadb, false=IX1 loadw *)
 ndefinition mode_IX1_load ≝
 λbyteflag:bool.λm:mcu_type.λt:memory_impl.λs:any_status m t.λcur_pc:word16.
  opt_map … (get_IX m t s)
   (λaddr.opt_map … (memory_filter_read m t s cur_pc)
-   (λoffs.(aux_load m t byteflag) s (plus_w16_d_d addr 〈〈x0,x0〉:offs〉) cur_pc 1)).
+   (λoffs.(aux_load m t byteflag) s (plus_w16_d_d addr 〈〈x0,x0〉:offs〉) cur_pc nat1)).
 
 (* lettura da X+[byte curpc] *)
 ndefinition mode_IX1ADD_load ≝
@@ -474,7 +474,7 @@ ndefinition mode_IX1_write ≝
 λwritebw:match byteflag with [ true ⇒ byte8 | false ⇒ word16 ].
  opt_map … (get_IX m t s)
   (λaddr.opt_map … (memory_filter_read m t s cur_pc)
-   (λoffs.(aux_write m t byteflag) s (plus_w16_d_d addr 〈〈x0,x0〉:offs〉) cur_pc 1 writebw)).
+   (λoffs.(aux_write m t byteflag) s (plus_w16_d_d addr 〈〈x0,x0〉:offs〉) cur_pc nat1 writebw)).
 
 (* lettura da [IX+word [pc]]: true=IX2 loadb, false=IX2 loadw *)
 ndefinition mode_IX2_load ≝
@@ -482,7 +482,7 @@ ndefinition mode_IX2_load ≝
  opt_map … (get_IX m t s)
   (λaddr.opt_map … (memory_filter_read m t s cur_pc)
    (λoffsh.opt_map … (memory_filter_read m t s (filtered_inc_w16 m t s cur_pc))
-    (λoffsl.(aux_load m t byteflag) s (plus_w16_d_d addr 〈offsh:offsl〉) cur_pc 2))).
+    (λoffsl.(aux_load m t byteflag) s (plus_w16_d_d addr 〈offsh:offsl〉) cur_pc nat2))).
 
 (* lettura da X+[word curpc] *)
 ndefinition mode_IX2ADD_load ≝
@@ -490,7 +490,7 @@ ndefinition mode_IX2ADD_load ≝
  opt_map … (memory_filter_read m t s cur_pc)
   (λbh.opt_map … (memory_filter_read m t s (filtered_inc_w16 m t s cur_pc))
    (λbl.opt_map … (get_IX m t s)
-    (λaddr.Some ? (triple … s (plus_w16_d_d addr 〈bh:bl〉) (filtered_plus_w16 m t s cur_pc 2))))).
+    (λaddr.Some ? (triple … s (plus_w16_d_d addr 〈bh:bl〉) (filtered_plus_w16 m t s cur_pc nat2))))).
 
 (* scrittura su [IX+word [pc]]: true=IX2 writeb, false=IX2 writew *)
 ndefinition mode_IX2_write ≝
@@ -499,14 +499,14 @@ ndefinition mode_IX2_write ≝
  opt_map … (get_IX m t s)
   (λaddr.opt_map … (memory_filter_read m t s cur_pc)
    (λoffsh.opt_map … (memory_filter_read m t s (filtered_inc_w16 m t s cur_pc))
-    (λoffsl.(aux_write m t byteflag) s (plus_w16_d_d addr 〈offsh:offsl〉) cur_pc 2 writebw))).
+    (λoffsl.(aux_write m t byteflag) s (plus_w16_d_d addr 〈offsh:offsl〉) cur_pc nat2 writebw))).
 
 (* lettura da [SP+byte [pc]]: true=SP1 loadb, false=SP1 loadw *)
 ndefinition mode_SP1_load ≝
 λbyteflag:bool.λm:mcu_type.λt:memory_impl.λs:any_status m t.λcur_pc:word16.
  opt_map … (get_sp_reg m t s)
   (λaddr.opt_map … (memory_filter_read m t s cur_pc)
-   (λoffs.(aux_load m t byteflag) s (plus_w16_d_d addr 〈〈x0,x0〉:offs〉) cur_pc 1)).
+   (λoffs.(aux_load m t byteflag) s (plus_w16_d_d addr 〈〈x0,x0〉:offs〉) cur_pc nat1)).
 
 (* scrittura su [SP+byte [pc]]: true=SP1 writeb, false=SP1 writew *)
 ndefinition mode_SP1_write ≝
@@ -514,7 +514,7 @@ ndefinition mode_SP1_write ≝
 λwritebw:match byteflag with [ true ⇒ byte8 | false ⇒ word16 ].
  opt_map … (get_sp_reg m t s)
   (λaddr.opt_map … (memory_filter_read m t s cur_pc)
-   (λoffs.(aux_write m t byteflag) s (plus_w16_d_d addr 〈〈x0,x0〉:offs〉) cur_pc 1 writebw)).
+   (λoffs.(aux_write m t byteflag) s (plus_w16_d_d addr 〈〈x0,x0〉:offs〉) cur_pc nat1 writebw)).
 
 (* lettura da [SP+word [pc]]: true=SP2 loadb, false=SP2 loadw *)
 ndefinition mode_SP2_load ≝
@@ -522,7 +522,7 @@ ndefinition mode_SP2_load ≝
  opt_map … (get_sp_reg m t s)
   (λaddr.opt_map … (memory_filter_read m t s cur_pc)
    (λoffsh.opt_map … (memory_filter_read m t s (filtered_inc_w16 m t s cur_pc))
-    (λoffsl.(aux_load m t byteflag) s (plus_w16_d_d addr 〈offsh:offsl〉) cur_pc 2))).
+    (λoffsl.(aux_load m t byteflag) s (plus_w16_d_d addr 〈offsh:offsl〉) cur_pc nat2))).
 
 (* scrittura su [SP+word [pc]]: true=SP2 writeb, false=SP2 writew *)
 ndefinition mode_SP2_write ≝
@@ -531,7 +531,7 @@ ndefinition mode_SP2_write ≝
  opt_map … (get_sp_reg m t s)
   (λaddr.opt_map … (memory_filter_read m t s cur_pc)
    (λoffsh.opt_map … (memory_filter_read m t s (filtered_inc_w16 m t s cur_pc))
-    (λoffsl.(aux_write m t byteflag) s (plus_w16_d_d addr 〈offsh:offsl〉) cur_pc 2 writebw))).
+    (λoffsl.(aux_write m t byteflag) s (plus_w16_d_d addr 〈offsh:offsl〉) cur_pc nat2 writebw))).
 
 (* ************************************** *)
 (* raccordo di tutte le possibili letture *)
diff --git a/helm/software/matita/contribs/ng_assembly/freescale_tests/medium_tests.ma b/helm/software/matita/contribs/ng_assembly/freescale_tests/medium_tests.ma
index 0123dd885..68db649b5 100755
--- a/helm/software/matita/contribs/ng_assembly/freescale_tests/medium_tests.ma
+++ b/helm/software/matita/contribs/ng_assembly/freescale_tests/medium_tests.ma
@@ -157,7 +157,7 @@ nlemma dTest_HCS08_sReverse_dump_aux ≝
   (* parametri IN: t,H:X,strlen(string),string *)
   (TickOK ? (dTest_HCS08_sReverse_status t 〈x0,x0〉 〈〈x0,xD〉:〈x4,xB〉〉 (byte8_strlen string) string))
   (* tempo di esecuzione 42+79*n+5*(n>>9) *)
-  (42+(79*(len_list ? string))+(5*((len_list ? string)/512))) with
+  (nat42 + (nat79 * (len_list ? string))+(nat5 * ((len_list ? string) / nat512))) with
    [ TickERR s _ ⇒ None ?
    (* azzeramento tutta RAM tranne dati *)
    | TickSUSP s _ ⇒ None ? 
@@ -189,7 +189,7 @@ nlemma dTest_HCS08_sReverse_aux ≝
   (* parametri IN: t,H:X,strlen(string),string *)
   (TickOK ? (dTest_HCS08_sReverse_status t 〈x0,x0〉 〈〈x0,xD〉:〈x4,xB〉〉 (byte8_strlen string) string))
   (* tempo di esecuzione 42+79*n+5*(n>>9) *)
-  (42+(79*(len_list ? string))+(5*((len_list ? string)/512))) with
+  (nat42 + (nat79 * (len_list ? string))+(nat5 * ((len_list ? string) / nat512))) with
    [ TickERR s _ ⇒ None ?
    (* azzeramento tutta RAM tranne dati *)
    | TickSUSP s _ ⇒ None ? 
@@ -231,7 +231,7 @@ ndefinition sReverseCalc ≝
 λstring:list byte8.
  match execute HCS08 MEM_TREE
   (TickOK ? (dTest_HCS08_sReverse_status MEM_TREE 〈x0,x0〉 〈〈x0,xD〉:〈x4,xB〉〉 (byte8_strlen string) string))
-  (42+(79*(len_list ? string))+(5*((len_list ? string)/512))) with
+  (nat42 + (nat79 * (len_list ? string))+(nat5 * ((len_list ? string) / nat512))) with
    [ TickERR s _ ⇒ None ?
    | TickSUSP s _ ⇒ None ? 
    | TickOK s ⇒ Some ? (set_mem_desc HCS08 MEM_TREE s (load_from_source_at MEM_TREE (mem_desc HCS08 MEM_TREE s) dTest_zeros 〈〈x0,xD〉:〈x0,x0〉〉))
@@ -409,7 +409,7 @@ nlemma dTest_HCS08_cSort_aux ≝
   (* parametri IN: t,A,H:X,strlen(string),string *)
   (TickOK ? (dTest_HCS08_cSort_status t true 〈x0,x0〉 〈〈x0,xF〉:〈x4,xC〉〉 (byte8_strlen string) string))
   (* tempo di esecuzione 25700+150*n *)
-  ((257*100)+(150*(len_list ? string))) with
+  (((nat256 + nat1) * nat100)+((nat50 * nat3) * (len_list ? string))) with
    [ TickERR s _ ⇒ None ?
    (* azzeramento tutta RAM tranne dati *)
    | TickSUSP s _ ⇒ Some ? (set_mem_desc HCS08 t s (load_from_source_at t (mem_desc HCS08 t s) dTest_zeros 〈〈x0,xD〉:〈x0,x0〉〉))
@@ -434,7 +434,7 @@ ndefinition cSortCalc ≝
 λstring:list byte8.
  match execute HCS08 MEM_TREE
   (TickOK ? (dTest_HCS08_cSort_status MEM_TREE true 〈x0,x0〉 〈〈x0,xF〉:〈x4,xC〉〉 (byte8_strlen string) string))
-  ((257*100)+(150*(len_list ? string))) with
+  (((nat256 + nat1) * nat100)+((nat50 * nat3) * (len_list ? string))) with
    [ TickERR s _ ⇒ None ?
    | TickSUSP s _ ⇒ Some ? (set_mem_desc HCS08 MEM_TREE s (load_from_source_at MEM_TREE (mem_desc HCS08 MEM_TREE s) dTest_zeros 〈〈x0,xD〉:〈x0,x0〉〉))
    | TickOK s ⇒ None ?
@@ -803,7 +803,7 @@ nlet rec dTest_HCS08_gNum_execute1 (m:mcu_type) (t:memory_impl) (s:tick_result (
   | TickSUSP s' susp ⇒ TickSUSP ? s' susp
   | TickOK s' ⇒ match n with
    [ O ⇒ TickOK ? s'
-   | S n' ⇒ dTest_HCS08_gNum_execute1 m t (execute m t (TickOK ? s') (ntot+2)) n' ntot ]
+   | S n' ⇒ dTest_HCS08_gNum_execute1 m t (execute m t (TickOK ? s') (ntot + nat2)) n' ntot ]
   ].
 
 (* esecuzione execute k*(n+1)*(n+2) *)
@@ -813,7 +813,7 @@ nlet rec dTest_HCS08_gNum_execute2 (m:mcu_type) (t:memory_impl) (s:tick_result (
   | TickSUSP s' susp ⇒ TickSUSP ? s' susp
   | TickOK s' ⇒ match n with
    [ O ⇒ TickOK ? s'
-   | S n' ⇒ dTest_HCS08_gNum_execute2 m t (dTest_HCS08_gNum_execute1 m t (TickOK ? s') (ntot+1) ntot) n' ntot ]
+   | S n' ⇒ dTest_HCS08_gNum_execute2 m t (dTest_HCS08_gNum_execute1 m t (TickOK ? s') (ntot + nat1) ntot) n' ntot ]
   ].
 
 (* esecuzione execute k*n*(n+1)*(n+2) *)
@@ -832,7 +832,7 @@ ndefinition dTest_HCS08_gNum_execute4 ≝
  match s with
   [ TickERR s' error ⇒ TickERR ? s' error
   | TickSUSP s' susp ⇒ TickSUSP ? s' susp
-  | TickOK s' ⇒ execute m t (dTest_HCS08_gNum_execute3 m t (TickOK ? s') 11 ntot) 80
+  | TickOK s' ⇒ execute m t (dTest_HCS08_gNum_execute3 m t (TickOK ? s') nat11 ntot) nat80
   ].
 
 (* parametrizzazione dell'enunciato del teorema parziale *)
diff --git a/helm/software/matita/contribs/ng_assembly/freescale_tests/micro_tests.ma b/helm/software/matita/contribs/ng_assembly/freescale_tests/micro_tests.ma
index bc9615860..6918ba06b 100755
--- a/helm/software/matita/contribs/ng_assembly/freescale_tests/micro_tests.ma
+++ b/helm/software/matita/contribs/ng_assembly/freescale_tests/micro_tests.ma
@@ -120,7 +120,7 @@ ndefinition mTest_HCS08_ADC_status ≝
 (* dimostrazione senza svolgimento degli stati, immediata *)
 nlemma ok_mTest_HCS08_ADC_full :
  ∀t:memory_impl.
- execute HCS08 t (TickOK ? (mTest_HCS08_ADC_status t)) 28 =
+ execute HCS08 t (TickOK ? (mTest_HCS08_ADC_status t)) nat28 =
  (* NB: V,N,Z sono tornati false C e' tornato true *)
  TickOK ? (set_pc_reg HCS08 t (* nuovo PC *)
            (set_acc_8_low_reg HCS08 t (mTest_HCS08_ADC_status t) 〈x1,x6〉) (* nuovo A *)
@@ -189,6 +189,8 @@ nlemma ok_mTest_HCS08_ADC_full :
  napply refl_eq.
 nqed.
 
+(* -------------------------------------
+
 (* ********* *)
 (* HCS08 MOV *)
 (* ********* *)
@@ -785,3 +787,4 @@ lemma ok_mTest_bits_MEM_TREE_full :
  reflexivity.
 qed.
 *)
+*)
diff --git a/helm/software/matita/contribs/ng_assembly/num/word16.ma b/helm/software/matita/contribs/ng_assembly/num/word16.ma
index 1abaf0599..6c1b21865 100755
--- a/helm/software/matita/contribs/ng_assembly/num/word16.ma
+++ b/helm/software/matita/contribs/ng_assembly/num/word16.ma
@@ -224,7 +224,7 @@ ndefinition div_b8 ≝
 (* 3) ad ogni ciclo il divisore e il moltiplicatore vengono scalati di 1 a dx *)
 (* 4) il moltiplicatore e' la quantita' aggiunta al quoziente se il divisore *)
 (*    puo' essere sottratto al dividendo *) 
-  | false ⇒ div_b8_aux w (rol_w16_n 〈〈x0,x0〉:b〉 7) 〈x8,x0〉 〈x0,x0〉 7 ]].
+  | false ⇒ div_b8_aux w (rol_w16_n 〈〈x0,x0〉:b〉 nat7) 〈x8,x0〉 〈x0,x0〉 nat7 ]].
 
 (* operatore x in [inf,sup] *)
 ndefinition inrange_w16 ≝
diff --git a/helm/software/matita/contribs/ng_assembly/num/word32.ma b/helm/software/matita/contribs/ng_assembly/num/word32.ma
index 81c0af595..51bbf1ced 100755
--- a/helm/software/matita/contribs/ng_assembly/num/word32.ma
+++ b/helm/software/matita/contribs/ng_assembly/num/word32.ma
@@ -224,7 +224,7 @@ ndefinition div_w16 ≝
 (* 3) ad ogni ciclo il divisore e il moltiplicatore vengono scalati di 1 a dx *)
 (* 4) il moltiplicatore e' la quantita' aggiunta al quoziente se il divisore *)
 (*    puo' essere sottratto al dividendo *) 
-  | false ⇒ div_w16_aux w (rol_w32_n 〈〈〈x0,x0〉:〈x0,x0〉〉.b〉 15) 〈〈x8,x0〉:〈x0,x0〉〉 〈〈x0,x0〉:〈x0,x0〉〉 15 ]].
+  | 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] *)
 ndefinition inrange_w32 ≝
-- 
2.39.2