...

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 10b82528d13d6aa903eb81bad50e287d353764bc..b86e307f238e66c476a72bce74004c4f9a07cb73 100755 (executable)
--- a/helm/software/matita/contribs/ng_assembly2/emulator/opcodes/pseudo.ma
+++ b/helm/software/matita/contribs/ng_assembly2/emulator/opcodes/pseudo.ma
@@ -73,18 +73,42 @@ ndefinition aux_im_type ≝
 
 ndefinition aux_table_type ≝ λmcu:mcu_type.Prod4T (aux_pseudo_type mcu) (aux_im_type mcu) byte8_or_word16 byte8.
 
-ndefinition pseudo_is_comparable ≝
-λmcu:mcu_type.match mcu with
- [ HC05 ⇒ Freescalepseudo_is_comparable
- | HC08 ⇒ Freescalepseudo_is_comparable
- | HCS08 ⇒ Freescalepseudo_is_comparable
- | RS08 ⇒ Freescalepseudo_is_comparable
- | IP2022 ⇒ IP2022pseudo_is_comparable
- ].
+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.
+       
 
 (* come suggerire di unificare?
    carr (pseudo_is_comparable M) = aux_pseudo_type M *)
 
+unification hint 0 ≔  MCU:mcu_type ⊢
+   carr (pseudo_is_comparable MCU) ≡ aux_pseudo_type MCU.
+
 (* 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 ≝
  match l with