X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2Flibrary%2Ffreescale%2Fopcode.ma;h=62199d7d354142d8d35fcb3d816351e423a2ec2c;hb=8ef11a4b981e6da3d60f353386b17f7692dc0ecd;hp=27a49f1208b3c427424dcbe2805c690332c0d07e;hpb=5806e0aa438ae85f09c93c93ba9f53d9663d7420;p=helm.git

diff --git a/helm/software/matita/library/freescale/opcode.ma b/helm/software/matita/library/freescale/opcode.ma
index 27a49f120..62199d7d3 100644
--- a/helm/software/matita/library/freescale/opcode.ma
+++ b/helm/software/matita/library/freescale/opcode.ma
@@ -24,9 +24,6 @@
 (*                    data ultima modifica 15/11/2007                     *)
 (* ********************************************************************** *)
 
-set "baseuri" "cic:/matita/freescale/opcode/".
-
-(*include "/media/VIRTUOSO/freescale/aux_bases.ma".*)
 include "freescale/aux_bases.ma".
 
 (* ********************************************** *)
@@ -374,55 +371,109 @@ 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 *)
+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 o (S c) tl
+    | false ⇒ get_pseudo_count o c tl
+    ]
+   ]
+  ]
+in get_pseudo_count.
+
+(* su tutta la lista quante volte compare la modalita' *)
+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 i (S c) tl
+   | false ⇒ get_mode_count i c tl
+   ]
+  ]
+  in get_mode_count.
 
 (* b e' non implementato? *)
-let rec test_not_impl (b:byte8) (l:list byte8) on l ≝
+let rec test_not_impl_byte (b:byte8) (l:list byte8) on l ≝
  match l with
   [ nil ⇒ false
   | cons hd tl ⇒ match eq_b8 b hd with
    [ true ⇒ true
-   | false ⇒ test_not_impl b tl
+   | false ⇒ test_not_impl_byte b tl
+   ]
+  ].
+
+(* o e' non implementato? *)
+let rec test_not_impl_pseudo (o:opcode) (l:list opcode) on l ≝
+ match l with
+  [ nil ⇒ false
+  | cons hd tl ⇒ match eqop HC05 (anyOP HC05 o) (anyOP HC05 hd) with
+   [ true ⇒ true
+   | false ⇒ test_not_impl_pseudo o tl
+   ]
+  ].
+
+(* i e' non implementato? *)
+let rec test_not_impl_mode (i:instr_mode) (l:list instr_mode) on l ≝
+ match l with
+  [ nil ⇒ false
+  | cons hd tl ⇒ match eqim i hd with
+   [ true ⇒ true
+   | false ⇒ test_not_impl_mode i tl
    ]
   ].
 
 (* 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.