From 3e758134d629980e9bf018a913404b98eccc514c Mon Sep 17 00:00:00 2001
From: Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Date: Thu, 4 Feb 2010 13:31:41 +0000
Subject: [PATCH] ...

---
 .../ng_assembly2/emulator/opcodes/pseudo.ma   | 40 +++++++++++++++----
 1 file changed, 32 insertions(+), 8 deletions(-)

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 10b82528d..b86e307f2 100755
--- 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
-- 
2.39.2