X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;ds=inline;f=helm%2Fsoftware%2Fmatita%2Flibrary%2Ffreescale%2Fopcode.ma;h=62199d7d354142d8d35fcb3d816351e423a2ec2c;hb=7abdf2f1764ba67a48f0829f7a9813ce7426b0c6;hp=e14ea9001edeee6a04c7e09ebdb2c2896366d40f;hpb=09e3a050664b07c961a92bf16245a7345346f964;p=helm.git

diff --git a/helm/software/matita/library/freescale/opcode.ma b/helm/software/matita/library/freescale/opcode.ma
index e14ea9001..62199d7d3 100644
--- a/helm/software/matita/library/freescale/opcode.ma
+++ b/helm/software/matita/library/freescale/opcode.ma
@@ -371,56 +371,64 @@ definition eqim ≝
 (* ********************************************* *)
 
 (* su tutta la lista quante volte compare il byte *)
-let rec get_byte_count (m:mcu_type) (b:byte8) (c:nat)
+definition get_byte_count := \lambda m:mcu_type.
+let rec get_byte_count  (b:byte8) (c:nat)
  (l:list (Prod4T (any_opcode m) instr_mode byte8_or_word16 byte8)) on l ≝
  match l with
   [ nil ⇒ c
   | cons hd tl ⇒ match thd4T ???? hd with
    [ Byte b' ⇒ match eq_b8 b b' with
-    [ true ⇒ get_byte_count m b (S c) tl
-    | false ⇒ get_byte_count m b c tl
+    [ true ⇒ get_byte_count b (S c) tl
+    | false ⇒ get_byte_count b c tl
     ]
-   | Word _ ⇒ get_byte_count m b c tl
+   | Word _ ⇒ get_byte_count b c tl
    ]
-  ].
+  ]
+in get_byte_count.
 
 (* su tutta la lista quante volte compare la word (0x9E+byte) *)
-let rec get_word_count (m:mcu_type) (b:byte8) (c:nat)
+definition get_word_count := \lambda m:mcu_type.
+let rec get_word_count (b:byte8) (c:nat)
  (l:list (Prod4T (any_opcode m) instr_mode byte8_or_word16 byte8)) on l ≝
  match l with
   [ nil ⇒ c
   | cons hd tl ⇒ match thd4T ???? hd with
-   [ Byte _ ⇒ get_word_count m b c tl
+   [ Byte _ ⇒ get_word_count b c tl
    | Word w ⇒ match eq_w16 〈〈x9,xE〉:b〉 w with
-    [ true ⇒ get_word_count m b (S c) tl
-    | false ⇒ get_word_count m b c tl
+    [ true ⇒ get_word_count b (S c) tl
+    | false ⇒ get_word_count b c tl
     ]
    ]
-  ].
+  ]
+in get_word_count.
 
 (* su tutta la lista quante volte compare lo pseudocodice *)
-let rec get_pseudo_count (m:mcu_type) (o:opcode) (c:nat)
+definition get_pseudo_count := \lambda m:mcu_type.
+let rec get_pseudo_count  (o:opcode) (c:nat)
  (l:list (Prod4T (any_opcode m) instr_mode byte8_or_word16 byte8)) on l ≝
  match l with
   [ nil ⇒ c
   | cons hd tl ⇒ match fst4T ???? hd with
    [ anyOP o' ⇒ match eqop m (anyOP m o) (anyOP m o') with
-    [ true ⇒ get_pseudo_count m o (S c) tl
-    | false ⇒ get_pseudo_count m o c tl
+    [ true ⇒ get_pseudo_count o (S c) tl
+    | false ⇒ get_pseudo_count o c tl
     ]
    ]
-  ].
+  ]
+in get_pseudo_count.
 
 (* su tutta la lista quante volte compare la modalita' *)
-let rec get_mode_count (m:mcu_type) (i:instr_mode) (c:nat)
+definition get_mode_count := \lambda m:mcu_type.
+let rec get_mode_count  (i:instr_mode) (c:nat)
  (l:list (Prod4T (any_opcode m) instr_mode byte8_or_word16 byte8)) on l ≝
  match l with
   [ nil ⇒ c
   | cons hd tl ⇒ match eqim (snd4T ???? hd) i with
-   [ true ⇒ get_mode_count m i (S c) tl
-   | false ⇒ get_mode_count m i c tl
+   [ true ⇒ get_mode_count i (S c) tl
+   | false ⇒ get_mode_count i c tl
    ]
-  ].
+  ]
+  in get_mode_count.
 
 (* b e' non implementato? *)
 let rec test_not_impl_byte (b:byte8) (l:list byte8) on l ≝
@@ -453,17 +461,19 @@ let rec test_not_impl_mode (i:instr_mode) (l:list instr_mode) on l ≝
   ].
 
 (* su tutta la lista quante volte compare la coppia opcode,instr_mode *)
-let rec get_OpIm_count (m:mcu_type) (o:any_opcode m) (i:instr_mode) (c:nat)
+definition get_OpIm_count := \lambda  m:mcu_type.
+let rec get_OpIm_count  (o:any_opcode m) (i:instr_mode) (c:nat)
  (l:list (Prod4T (any_opcode m) instr_mode byte8_or_word16 byte8)) on l ≝
  match l with
   [ nil ⇒ c
   | cons hd tl ⇒
    match (eqop m o (fst4T ???? hd)) ⊗
          (eqim i (snd4T ???? hd)) with
-    [ true ⇒ get_OpIm_count m o i (S c) tl
-    | false ⇒ get_OpIm_count m o i c tl
+    [ true ⇒ get_OpIm_count o i (S c) tl
+    | false ⇒ get_OpIm_count o i c tl
     ] 
-  ].
+  ]
+  in get_OpIm_count.
 
 (* iteratore sugli opcode *)
 definition forall_opcode ≝ λP.