freescale porting, work in progress

[helm.git] / helm / software / matita / contribs / ng_assembly / freescale / opcode.ma

diff --git a/helm/software/matita/contribs/ng_assembly/freescale/opcode.ma b/helm/software/matita/contribs/ng_assembly/freescale/opcode.ma
index 34b5c43af8aaa2a5bc8e2e326c1a9dd8012e0dee..aeaaa8aef47021ad982067357e6f552f3a771334 100755 (executable)
--- a/helm/software/matita/contribs/ng_assembly/freescale/opcode.ma
+++ b/helm/software/matita/contribs/ng_assembly/freescale/opcode.ma
@@ -15,25 +15,26 @@
 (* ********************************************************************** *)
 (*                          Progetto FreeScale                            *)
 (*                                                                        *)
-(*   Sviluppato da: Cosimo Oliboni, oliboni@cs.unibo.it                   *)
-(*     Cosimo Oliboni, oliboni@cs.unibo.it                                *)
+(*   Sviluppato da: Ing. Cosimo Oliboni, oliboni@cs.unibo.it              *)
+(*   Ultima modifica: 05/08/2009                                          *)
 (*                                                                        *)
 (* ********************************************************************** *)
 
 include "freescale/opcode_base.ma".
+include "common/list.ma".
 
 (* ********************************************* *)
 (* STRUMENTI PER LE DIMOSTRAZIONI DI CORRETTEZZA *)
 (* ********************************************* *)
 
 (* su tutta la lista quante volte compare il byte *)
-nlet rec get_byte_count (m:mcu_type) (b:byte8) (c:nat)
+nlet rec get_byte_count (m:mcu_type) (b:byte8) (c:word16)
  (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
+  | cons hd tl ⇒ match thd4T … hd with
    [ Byte b' ⇒ match eq_b8 b b' with
-    [ true ⇒ get_byte_count m b (S c) tl
+    [ true ⇒ get_byte_count m b (succ_w16 c) tl
     | false ⇒ get_byte_count m b c tl
     ]
    | Word _ ⇒ get_byte_count m b c tl
@@ -41,39 +42,39 @@ nlet rec get_byte_count (m:mcu_type) (b:byte8) (c:nat)
   ].
 
 (* su tutta la lista quante volte compare la word (0x9E+byte) *)
-nlet rec get_word_count (m:mcu_type) (b:byte8) (c:nat)
+nlet rec get_word_count (m:mcu_type) (b:byte8) (c:word16)
  (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
+  | cons hd tl ⇒ match thd4T … hd with
    [ Byte _ ⇒ get_word_count m b c tl
    | Word w ⇒ match eq_w16 〈〈x9,xE〉:b〉 w with
-    [ true ⇒ get_word_count m b (S c) tl
+    [ true ⇒ get_word_count m b (succ_w16 c) tl
     | false ⇒ get_word_count m b c tl
     ]
    ]
   ].
 
 (* su tutta la lista quante volte compare lo pseudocodice *)
-nlet rec get_pseudo_count (m:mcu_type) (o:opcode) (c:nat)
+nlet rec get_pseudo_count (m:mcu_type) (o:opcode) (c:word16)
  (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
+  | cons hd tl ⇒ match fst4T … hd with
    [ anyOP o' ⇒ match eq_op o o' with
-    [ true ⇒ get_pseudo_count m o (S c) tl
+    [ true ⇒ get_pseudo_count m o (succ_w16 c) tl
     | false ⇒ get_pseudo_count m o c tl
     ]
    ]
   ].
 
 (* su tutta la lista quante volte compare la modalita' *)
-nlet rec get_mode_count (m:mcu_type) (i:instr_mode) (c:nat)
+nlet rec get_mode_count (m:mcu_type) (i:instr_mode) (c:word16)
  (l:list (Prod4T (any_opcode m) instr_mode byte8_or_word16 byte8)) on l ≝
  match l with
   [ nil ⇒ c
-  | cons hd tl ⇒ match eq_instrmode (snd4T ???? hd) i with
-   [ true ⇒ get_mode_count m i (S c) tl
+  | cons hd tl ⇒ match eq_im (snd4T … hd) i with
+   [ true ⇒ get_mode_count m i (succ_w16 c) tl
    | false ⇒ get_mode_count m i c tl
    ]
   ].
@@ -102,27 +103,27 @@ nlet rec test_not_impl_pseudo (o:opcode) (l:list opcode) on l ≝
 nlet rec test_not_impl_mode (i:instr_mode) (l:list instr_mode) on l ≝
  match l with
   [ nil ⇒ false
-  | cons hd tl ⇒ match eq_instrmode i hd with
+  | cons hd tl ⇒ match eq_im i hd with
    [ true ⇒ true
    | false ⇒ test_not_impl_mode i tl
    ]
   ].
 
 (* su tutta la lista quante volte compare la coppia opcode,instr_mode *)
-nlet rec get_OpIm_count (m:mcu_type) (o:any_opcode m) (i:instr_mode) (c:nat)
+nlet rec get_OpIm_count (m:mcu_type) (o:any_opcode m) (i:instr_mode) (c:word16)
  (l:list (Prod4T (any_opcode m) instr_mode byte8_or_word16 byte8)) on l ≝
  match l with
   [ nil ⇒ c
   | cons hd tl ⇒
-   match (eq_anyop m o (fst4T ???? hd)) ⊗
-         (eq_instrmode i (snd4T ???? hd)) with
-    [ true ⇒ get_OpIm_count m o i (S c) tl
+   match (eq_anyop m o (fst4T … hd)) ⊗
+         (eq_im i (snd4T … hd)) with
+    [ true ⇒ get_OpIm_count m o i (succ_w16 c) tl
     | false ⇒ get_OpIm_count m o i c tl
     ] 
   ].
 
 (* iteratore sugli opcode *)
-ndefinition forall_opcode ≝ λP.
+ndefinition forall_op ≝ λP.
  P ADC    ⊗ P ADD    ⊗ P AIS    ⊗ P AIX    ⊗ P AND    ⊗ P ASL    ⊗ P ASR    ⊗ P BCC    ⊗
  P BCLRn  ⊗ P BCS    ⊗ P BEQ    ⊗ P BGE    ⊗ P BGND   ⊗ P BGT    ⊗ P BHCC   ⊗ P BHCS   ⊗
  P BHI    ⊗ P BIH    ⊗ P BIL    ⊗ P BIT    ⊗ P BLE    ⊗ P BLS    ⊗ P BLT    ⊗ P BMC    ⊗
@@ -137,7 +138,7 @@ ndefinition forall_opcode ≝ λP.
  P TXA    ⊗ P TXS    ⊗ P WAIT.
 
 (* iteratore sulle modalita' *)
-ndefinition forall_instr_mode ≝ λP.
+ndefinition forall_im ≝ λP.
   P MODE_INH
 ⊗ P MODE_INHA
 ⊗ P MODE_INHX
@@ -175,5 +176,5 @@ ndefinition forall_instr_mode ≝ λP.
 
 ⊗ forall_oct (λo. P (MODE_DIRn o))
 ⊗ forall_oct (λo. P (MODE_DIRn_and_IMM1 o))
-⊗ forall_exadecim (λe. P (MODE_TNY e))
-⊗ forall_bitrigesim (λt. P (MODE_SRT t)).
+⊗ forall_ex (λe. P (MODE_TNY e))
+⊗ forall_bit (λt. P (MODE_SRT t)).