(* data ultima modifica 15/11/2007 *)
(* ********************************************************************** *)
-set "baseuri" "cic:/matita/freescale/opcode/".
-
-(*include "/media/VIRTUOSO/freescale/aux_bases.ma".*)
include "freescale/aux_bases.ma".
(* ********************************************** *)
(* ********************************************* *)
(* 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.