From: Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Date: Thu, 4 Feb 2010 13:31:41 +0000 (+0000)
Subject: ...
X-Git-Tag: make_still_working~3055
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=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 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