reworked freescale stuff to put \m as a left parameter

[helm.git] / helm / software / matita / library / freescale / opcode.ma

diff --git a/helm/software/matita/library/freescale/opcode.ma b/helm/software/matita/library/freescale/opcode.ma
index e14ea9001edeee6a04c7e09ebdb2c2896366d40f..62199d7d354142d8d35fcb3d816351e423a2ec2c 100644 (file)
--- 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.