freescale porting, work in progress

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

diff --git a/helm/software/matita/contribs/ng_assembly/freescale/translation.ma b/helm/software/matita/contribs/ng_assembly/freescale/translation.ma
index 9b327ac1fe1961f76c39671cd9f695bc623b4859..0996948942bad7c8c8cd7b4809456eaa72acc96b 100755 (executable)
--- a/helm/software/matita/contribs/ng_assembly/freescale/translation.ma
+++ b/helm/software/matita/contribs/ng_assembly/freescale/translation.ma
@@ -15,8 +15,8 @@
 (* ********************************************************************** *)
 (*                          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                                          *)
 (*                                                                        *)
 (* ********************************************************************** *)
 
@@ -24,7 +24,7 @@ include "freescale/table_HC05.ma".
 include "freescale/table_HC08.ma".
 include "freescale/table_HCS08.ma".
 include "freescale/table_RS08.ma".
-include "freescale/option.ma".
+include "common/option.ma".
 
 (* ***************************** *)
 (* TRADUZIONE ESADECIMALE → INFO *)
@@ -76,13 +76,11 @@ full_info_of_word16_aux m borw (opcode_table m).
 ninductive t_byte8 (m:mcu_type) : Type ≝
  TByte : byte8 → t_byte8 m.
 
-nlemma tbyte8_destruct : ∀m,b1,b2.TByte m b1 = TByte m b2 → b1 = b2.
- #m; #b1; #b2; #H;
- nchange with (match TByte m b2 with [ TByte a ⇒ b1 = a ]);
- nrewrite < H;
- nnormalize;
- napply refl_eq.
-nqed.
+ndefinition eq_tbyte8 ≝
+λm.λtb1,tb2:t_byte8 m.
+ match tb1 with
+  [ TByte b1 ⇒ match tb2 with
+   [ TByte b2 ⇒ eq_b8 b1 b2 ]].
 
 (* introduzione di un tipo dipendente (dalla modalita') per gli argomenti *)
 ninductive MA_check : instr_mode → Type ≝
@@ -177,7 +175,7 @@ nlet rec bytes_of_pseudo_instr_mode_param_aux (m:mcu_type) (o:any_opcode m) (i:i
                                              (param:list (Prod4T (any_opcode m) instr_mode byte8_or_word16 byte8)) on param ≝
  match param with
  [ nil ⇒ None ? | cons hd tl ⇒
-  match (eq_anyop m o (fst4T … hd)) ⊗ (eq_instrmode i (snd4T … hd)) with
+  match (eq_anyop m o (fst4T … hd)) ⊗ (eq_im i (snd4T … hd)) with
    [ true ⇒ match thd4T … hd with 
     [ Byte isab ⇒ 
      Some ? ([ (TByte m isab) ]@(args_picker m i p))