X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2Fcontribs%2Fng_assembly2%2Femulator%2Fopcodes%2Fpseudo.ma;h=4c5e3afe8a45999872115b57d2f64ea156730094;hb=67303bc29318bd94a31903a92a2127697c5de84e;hp=b86e307f238e66c476a72bce74004c4f9a07cb73;hpb=3e758134d629980e9bf018a913404b98eccc514c;p=helm.git

diff --git a/helm/software/matita/contribs/ng_assembly2/emulator/opcodes/pseudo.ma b/helm/software/matita/contribs/ng_assembly2/emulator/opcodes/pseudo.ma
index b86e307f2..4c5e3afe8 100755
--- a/helm/software/matita/contribs/ng_assembly2/emulator/opcodes/pseudo.ma
+++ b/helm/software/matita/contribs/ng_assembly2/emulator/opcodes/pseudo.ma
@@ -58,6 +58,40 @@ ndefinition aux_pseudo_type ≝
  | IP2022 ⇒ IP2022_pseudo
  ].
 
+ndefinition pseudo_is_comparable: mcu_type → comparable.
+ #mcu; @ (aux_pseudo_type mcu)
+  ##[ nelim mcu;
+      ##[ ##1,2,3,4: napply (zeroc Freescalepseudo_is_comparable)
+      ##| ##5: napply (zeroc IP2022pseudo_is_comparable) ##]
+  ##| nelim mcu;
+      ##[ ##1,2,3,4: napply (forallc Freescalepseudo_is_comparable)
+      ##| ##5:  napply (forallc IP2022pseudo_is_comparable) ##]
+  ##| nelim mcu;
+      ##[ ##1,2,3,4: napply (eqc Freescalepseudo_is_comparable)
+      ##| ##5: napply (eqc IP2022pseudo_is_comparable) ##]
+  ##| nelim mcu;
+      ##[ ##1,2,3,4: napply (eqc_to_eq Freescalepseudo_is_comparable)
+      ##| ##5: napply (eqc_to_eq IP2022pseudo_is_comparable) ##]
+  ##| nelim mcu;
+      ##[ ##1,2,3,4: napply (eq_to_eqc Freescalepseudo_is_comparable)
+      ##| ##5: napply (eq_to_eqc IP2022pseudo_is_comparable) ##]
+  ##| nelim mcu;
+      ##[ ##1,2,3,4: napply (neqc_to_neq Freescalepseudo_is_comparable)
+      ##| ##5: napply (neqc_to_neq IP2022pseudo_is_comparable) ##]
+  ##| nelim mcu;
+      ##[ ##1,2,3,4: napply (neq_to_neqc Freescalepseudo_is_comparable)
+      ##| ##5: napply (neq_to_neqc IP2022pseudo_is_comparable) ##]
+  ##| nelim mcu;
+      ##[ ##1,2,3,4: napply (decidable_c Freescalepseudo_is_comparable)
+      ##| ##5: napply (decidable_c IP2022pseudo_is_comparable) ##]
+  ##| nelim mcu;
+      ##[ ##1,2,3,4: napply (symmetric_eqc Freescalepseudo_is_comparable)
+      ##| ##5: napply (symmetric_eqc IP2022pseudo_is_comparable) ##]
+  ##]
+nqed.
+
+unification hint 0 ≔ M:mcu_type ⊢ carr (pseudo_is_comparable M) ≡ aux_pseudo_type M.
+
 ndefinition aux_im_type ≝
 λmcu:mcu_type.match mcu with
  [ HC05 ⇒ Freescale_instr_mode
@@ -67,47 +101,71 @@ ndefinition aux_im_type ≝
  | IP2022 ⇒ IP2022_instr_mode
  ].
 
+ndefinition im_is_comparable: mcu_type → comparable.
+ #mcu; @ (aux_im_type mcu)
+  ##[ nelim mcu;
+      ##[ ##1,2,3,4: napply (zeroc Freescaleim_is_comparable)
+      ##| ##5: napply (zeroc IP2022im_is_comparable) ##]
+  ##| nelim mcu;
+      ##[ ##1,2,3,4: napply (forallc Freescaleim_is_comparable)
+      ##| ##5:  napply (forallc IP2022im_is_comparable) ##]
+  ##| nelim mcu;
+      ##[ ##1,2,3,4: napply (eqc Freescaleim_is_comparable)
+      ##| ##5: napply (eqc IP2022im_is_comparable) ##]
+  ##| nelim mcu;
+      ##[ ##1,2,3,4: napply (eqc_to_eq Freescaleim_is_comparable)
+      ##| ##5: napply (eqc_to_eq IP2022im_is_comparable) ##]
+  ##| nelim mcu;
+      ##[ ##1,2,3,4: napply (eq_to_eqc Freescaleim_is_comparable)
+      ##| ##5: napply (eq_to_eqc IP2022im_is_comparable) ##]
+  ##| nelim mcu;
+      ##[ ##1,2,3,4: napply (neqc_to_neq Freescaleim_is_comparable)
+      ##| ##5: napply (neqc_to_neq IP2022im_is_comparable) ##]
+  ##| nelim mcu;
+      ##[ ##1,2,3,4: napply (neq_to_neqc Freescaleim_is_comparable)
+      ##| ##5: napply (neq_to_neqc IP2022im_is_comparable) ##]
+  ##| nelim mcu;
+      ##[ ##1,2,3,4: napply (decidable_c Freescaleim_is_comparable)
+      ##| ##5: napply (decidable_c IP2022im_is_comparable) ##]
+  ##| nelim mcu;
+      ##[ ##1,2,3,4: napply (symmetric_eqc Freescaleim_is_comparable)
+      ##| ##5: napply (symmetric_eqc IP2022im_is_comparable) ##]
+  ##]
+nqed.
+
+unification hint 0 ≔ M:mcu_type ⊢ carr (im_is_comparable M) ≡ aux_im_type M.
+
 (* ********************************************* *)
 (* STRUMENTI PER LE DIMOSTRAZIONI DI CORRETTEZZA *)
 (* ********************************************* *)
 
-ndefinition aux_table_type ≝ λmcu:mcu_type.Prod4T (aux_pseudo_type mcu) (aux_im_type mcu) byte8_or_word16 byte8.
-
-naxiom daemon: False.
-
-ndefinition pseudo_is_comparable: mcu_type → comparable.
- #mcu; 
- @ (aux_pseudo_type mcu)
-  ##[ napply (match mcu return λmcu. aux_pseudo_type mcu with
-        [ HC05 ⇒ zeroc Freescalepseudo_is_comparable
-        | HC08 ⇒ zeroc Freescalepseudo_is_comparable
-        | HCS08 ⇒ zeroc Freescalepseudo_is_comparable
-        | RS08 ⇒ zeroc Freescalepseudo_is_comparable
-        | IP2022 ⇒ zeroc IP2022pseudo_is_comparable
-        ])
-    | napply (match mcu return λmcu. (aux_pseudo_type mcu → bool) → bool with
-        [ HC05 ⇒ forallc Freescalepseudo_is_comparable
-        | HC08 ⇒ forallc Freescalepseudo_is_comparable
-        | HCS08 ⇒ forallc Freescalepseudo_is_comparable
-        | RS08 ⇒ forallc Freescalepseudo_is_comparable
-        | IP2022 ⇒ forallc IP2022pseudo_is_comparable
-        ])
-     | napply (match mcu return λmcu. aux_pseudo_type mcu → aux_pseudo_type mcu → bool with
-        [ HC05 ⇒ eqc Freescalepseudo_is_comparable
-        | HC08 ⇒ eqc Freescalepseudo_is_comparable
-        | HCS08 ⇒ eqc Freescalepseudo_is_comparable
-        | RS08 ⇒ eqc Freescalepseudo_is_comparable
-        | IP2022 ⇒ eqc IP2022pseudo_is_comparable
-        ])
-     |##*: ncases daemon ]
-nqed.
-       
+ndefinition aux_table_type ≝ λmcu:mcu_type.Prod4T (aux_pseudo_type mcu) (aux_im_type mcu) byte8_or_word16 nat.
 
-(* come suggerire di unificare?
-   carr (pseudo_is_comparable M) = aux_pseudo_type M *)
+(* su tutta la lista quante volte compare il byte *)
+nlet rec get_byte_count (m:mcu_type) (b:byte8) (c:word16) (l:list (aux_table_type m)) on l ≝
+ match l with
+  [ nil ⇒ c
+  | cons hd tl ⇒ match thd4T … hd with
+   [ Byte b' ⇒ match eqc ? b b' with
+    [ true ⇒ get_byte_count m b (succc ? c) tl
+    | false ⇒ get_byte_count m b c tl
+    ]
+   | Word _ ⇒ get_byte_count m b c tl
+   ]
+  ].
 
-unification hint 0 ≔  MCU:mcu_type ⊢
-   carr (pseudo_is_comparable MCU) ≡ aux_pseudo_type MCU.
+(* su tutta la lista quante volte compare la word *)
+nlet rec get_word_count (m:mcu_type) (w:word16) (c:word16) (l:list (aux_table_type m)) on l ≝
+ match l with
+  [ nil ⇒ c
+  | cons hd tl ⇒ match thd4T … hd with
+   [ Byte _ ⇒ get_word_count m w c tl
+   | Word w' ⇒ match eqc ? w w' with
+    [ true ⇒ get_word_count m w (succc ? c) tl
+    | false ⇒ get_word_count m w c tl
+    ]
+   ]
+  ].
 
 (* su tutta la lista quante volte compare lo pseudocodice *)
 nlet rec get_pseudo_count (m:mcu_type) (o:aux_pseudo_type m) (c:word16) (l:list (aux_table_type m)) on l ≝
@@ -118,3 +176,55 @@ nlet rec get_pseudo_count (m:mcu_type) (o:aux_pseudo_type m) (c:word16) (l:list
    | 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:aux_im_type m) (c:word16) (l:list (aux_table_type m)) on l ≝
+ match l with
+  [ nil ⇒ c
+  | cons hd tl ⇒ match eqc ? i (snd4T … hd) with
+   [ true ⇒ get_mode_count m i (succc ? c) tl
+   | false ⇒ get_mode_count m i c tl
+   ]
+  ].
+
+(* b e' non implementato? *)
+nlet rec test_not_impl_byte (b:byte8) (l:list byte8) on l ≝
+ match l with
+  [ nil ⇒ false
+  | cons hd tl ⇒ match eqc ? b hd with
+   [ true ⇒ true
+   | false ⇒ test_not_impl_byte b tl
+   ]
+  ].
+
+(* su tutta la lista quante volte compare la coppia pseudo,instr_mode *)
+nlet rec get_PsIm_count (m:mcu_type) (o:aux_pseudo_type m) (i:aux_im_type m) (c:word16) (l:list (aux_table_type m)) on l ≝
+ match l with
+  [ nil ⇒ c
+  | cons hd tl ⇒
+   match (eqc ? o (fst4T … hd)) ⊗
+         (eqc ? i (snd4T … hd)) with
+    [ true ⇒ get_PsIm_count m o i (succc ? c) tl
+    | false ⇒ get_PsIm_count m o i c tl
+    ] 
+  ].
+
+(* o e' non implementato? *)
+nlet rec test_not_impl_pseudo (m:mcu_type) (o:aux_pseudo_type m) (l:list (aux_pseudo_type m)) on l ≝
+ match l with
+  [ nil ⇒ false
+  | cons hd tl ⇒ match eqc ? o hd with
+   [ true ⇒ true
+   | false ⇒ test_not_impl_pseudo m o tl
+   ]
+  ].
+
+(* i e' non implementato? *)
+nlet rec test_not_impl_mode (m:mcu_type) (i:aux_im_type m) (l:list (aux_im_type m)) on l ≝
+ match l with
+  [ nil ⇒ false
+  | cons hd tl ⇒ match eqc ? i hd with
+   [ true ⇒ true
+   | false ⇒ test_not_impl_mode m i tl
+   ]
+  ].