(* ********************************************* *)
(* 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 ≝
].
(* 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.