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 eac7385d5ff58bf51c41a66cddc520c4aeba8d03..b7fc76f7a51da4b39297f959dec7daeae1ab3282 100755 (executable)
--- a/helm/software/matita/contribs/ng_assembly/freescale/translation.ma
+++ b/helm/software/matita/contribs/ng_assembly/freescale/translation.ma
@@ -13,22 +13,18 @@
 (**************************************************************************)
 
 (* ********************************************************************** *)
-(*                           Progetto FreeScale                           *)
+(*                          Progetto FreeScale                            *)
 (*                                                                        *)
-(* Sviluppato da:                                                         *)
-(*   Cosimo Oliboni, oliboni@cs.unibo.it                                  *)
+(*   Sviluppato da: Ing. Cosimo Oliboni, oliboni@cs.unibo.it              *)
+(*   Ultima modifica: 05/08/2009                                          *)
 (*                                                                        *)
-(* Questo materiale fa parte della tesi:                                  *)
-(*   "Formalizzazione Interattiva dei Microcontroller a 8bit FreeScale"   *)
-(*                                                                        *)
-(*                    data ultima modifica 15/11/2007                     *)
 (* ********************************************************************** *)
 
 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 *)
@@ -55,7 +51,7 @@ nlet rec full_info_of_word16_aux (m:mcu_type) (borw:byte8_or_word16)
  match param with
   [ nil ⇒ None ?
   | cons hd tl ⇒
-   match thd4T ???? hd with
+   match thd4T … hd with
     [ Byte b ⇒ match borw with
      [ Byte borw' ⇒ match eq_b8 borw' b with
       [ true ⇒ Some ? hd
@@ -80,29 +76,6 @@ full_info_of_word16_aux m borw (opcode_table m).
 ninductive t_byte8 (m:mcu_type) : Type ≝
  TByte : byte8 → t_byte8 m.
 
-ndefinition t_byte8_ind
- : Πm:mcu_type.ΠP:t_byte8 m → Prop.(Πb:byte8.P (TByte m b)) → Πt:t_byte8 m.P t ≝
-λm:mcu_type.λP:t_byte8 m → Prop.λf:Πb:byte8.P (TByte m b).λt:t_byte8 m.
- match t with [ TByte (b:byte8) ⇒ f b ].
-
-ndefinition t_byte8_rec
- : Πm:mcu_type.ΠP:t_byte8 m → Set.(Πb:byte8.P (TByte m b)) → Πt:t_byte8 m.P t ≝
-λm:mcu_type.λP:t_byte8 m → Set.λf:Πb:byte8.P (TByte m b).λt:t_byte8 m.
- match t with [ TByte (b:byte8) ⇒ f b ].
-
-ndefinition t_byte8_rect
- : Πm:mcu_type.ΠP:t_byte8 m → Type.(Πb:byte8.P (TByte m b)) → Πt:t_byte8 m.P t ≝
-λm:mcu_type.λP:t_byte8 m → Type.λf:Πb:byte8.P (TByte m b).λt:t_byte8 m.
- match t with [ TByte (b:byte8) ⇒ f b ].
-
-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.
-
 (* introduzione di un tipo dipendente (dalla modalita') per gli argomenti *)
 ninductive MA_check : instr_mode → Type ≝
   maINH              : MA_check MODE_INH
@@ -141,114 +114,6 @@ ninductive MA_check : instr_mode → Type ≝
 | maSRT              : ∀t.MA_check (MODE_SRT t)
 .
 
-ndefinition instr_mode_ind
- : Πi:instr_mode.ΠP:Πj.MA_check j → Prop.
-   P ? maINH → P ? maINHA → P ? maINHX → P ? maINHH → P ? maINHX0ADD → (Πb.P ? (maINHX1ADD b)) →
-   (Πw.P ? (maINHX2ADD w)) → (Πb.P ? (maIMM1 b)) → (Πb.P ? (maIMM1EXT b)) → (Πw.P ? (maIMM2 w)) →
-   (Πb.P ? (maDIR1 b)) → (Πw.P ? (maDIR2 w)) → P ? maIX0 → (Πb.P ? (maIX1 b)) → (Πw.P ? (maIX2 w)) →
-   (Πb.P ? (maSP1 b)) → (Πw.P ? (maSP2 w)) → (Πb1,b2.P ? (maDIR1_to_DIR1 b1 b2)) →
-   (Πb1,b2.P ? (maIMM1_to_DIR1 b1 b2)) → (Πb.P ? (maIX0p_to_DIR1 b)) → (Πb.P ? (maDIR1_to_IX0p b)) →
-   (Πb.P ? (maINHA_and_IMM1 b)) → (Πb.P ? (maINHX_and_IMM1 b)) → (Πb1,b2.P ? (maIMM1_and_IMM1 b1 b2)) →
-   (Πb1,b2.P ? (maDIR1_and_IMM1 b1 b2)) → (Πb.P ? (maIX0_and_IMM1 b)) → (Πb.P ? (maIX0p_and_IMM1 b)) →
-   (Πb1,b2.P ? (maIX1_and_IMM1 b1 b2)) → (Πb1,b2.P ? (maIX1p_and_IMM1 b1 b2)) → (Πb1,b2.P ? (maSP1_and_IMM1 b1 b2)) →
-   (Πn,b.P ? ((maDIRn n) b)) → (Πn,b1,b2.P ? ((maDIRn_and_IMM1 n) b1 b2)) → (Πe.P ? (maTNY e)) → (Πt.P ? (maSRT t)) →
-   Πma:MA_check i.P i ma ≝
-λi:instr_mode.λP:Πj.MA_check j → Prop.
-λp:P ? maINH.λp1:P ? maINHA.λp2:P ? maINHX.λp3:P ? maINHH.λp4:P ? maINHX0ADD.
-λf:Πb.P ? (maINHX1ADD b).λf1:Πw.P ? (maINHX2ADD w).λf2:Πb.P ? (maIMM1 b).λf3:Πb.P ? (maIMM1EXT b).
-λf4:Πw.P ? (maIMM2 w).λf5:Πb.P ? (maDIR1 b).λf6:Πw.P ? (maDIR2 w).λp5:P ? maIX0.
-λf7:Πb.P ? (maIX1 b).λf8:Πw.P ? (maIX2 w).λf9:Πb.P ? (maSP1 b).λf10:Πw.P ? (maSP2 w).
-λf11:Πb1,b2.P ? (maDIR1_to_DIR1 b1 b2).λf12:Πb1,b2.P ? (maIMM1_to_DIR1 b1 b2).
-λf13:Πb.P ? (maIX0p_to_DIR1 b).λf14:Πb.P ? (maDIR1_to_IX0p b).λf15:Πb.P ? (maINHA_and_IMM1 b).
-λf16:Πb.P ? (maINHX_and_IMM1 b).λf17:Πb1,b2.P ? (maIMM1_and_IMM1 b1 b2).
-λf18:Πb1,b2.P ? (maDIR1_and_IMM1 b1 b2).λf19:Πb.P ? (maIX0_and_IMM1 b).
-λf20:Πb.P ? (maIX0p_and_IMM1 b).λf21:Πb1,b2.P ? (maIX1_and_IMM1 b1 b2).
-λf22:Πb1,b2.P ? (maIX1p_and_IMM1 b1 b2).λf23:Πb1,b2.P ? (maSP1_and_IMM1 b1 b2).
-λf24:Πn,b.P ? ((maDIRn n) b).λf25:Πn,b1,b2.P ? ((maDIRn_and_IMM1 n) b1 b2).
-λf26:Πe.P ? (maTNY e).λf27:Πt.P ? (maSRT t).λma:MA_check i.
- match ma with
-  [ maINH ⇒ p | maINHA ⇒ p1 | maINHX ⇒ p2 | maINHH ⇒ p3 | maINHX0ADD ⇒ p4
-  | maINHX1ADD b ⇒ f b | maINHX2ADD w ⇒ f1 w | maIMM1 b ⇒ f2 b | maIMM1EXT b ⇒ f3 b
-  | maIMM2 w ⇒ f4 w | maDIR1 b ⇒ f5 b | maDIR2 w ⇒ f6 w | maIX0 ⇒ p5 | maIX1 b ⇒ f7 b
-  | maIX2 w ⇒ f8 w | maSP1 b ⇒ f9 b | maSP2 w ⇒ f10 w | maDIR1_to_DIR1 b1 b2 ⇒ f11 b1 b2
-  | maIMM1_to_DIR1 b1 b2 ⇒ f12 b1 b2 | maIX0p_to_DIR1 b ⇒ f13 b | maDIR1_to_IX0p b ⇒ f14 b
-  | maINHA_and_IMM1 b ⇒ f15 b | maINHX_and_IMM1 b ⇒ f16 b | maIMM1_and_IMM1 b1 b2 ⇒ f17 b1 b2
-  | maDIR1_and_IMM1 b1 b2 ⇒ f18 b1 b2 | maIX0_and_IMM1 b ⇒ f19 b | maIX0p_and_IMM1 b ⇒ f20 b
-  | maIX1_and_IMM1 b1 b2 ⇒ f21 b1 b2 | maIX1p_and_IMM1 b1 b2 ⇒ f22 b1 b2 | maSP1_and_IMM1 b1 b2 ⇒ f23 b1 b2
-  | maDIRn n b ⇒ f24 n b | maDIRn_and_IMM1 n b1 b2 ⇒ f25 n b1 b2 | maTNY e ⇒ f26 e | maSRT t ⇒ f27 t ].
-
-ndefinition instr_mode_rec
- : Πi:instr_mode.ΠP:Πj.MA_check j → Set.
-   P ? maINH → P ? maINHA → P ? maINHX → P ? maINHH → P ? maINHX0ADD → (Πb.P ? (maINHX1ADD b)) →
-   (Πw.P ? (maINHX2ADD w)) → (Πb.P ? (maIMM1 b)) → (Πb.P ? (maIMM1EXT b)) → (Πw.P ? (maIMM2 w)) →
-   (Πb.P ? (maDIR1 b)) → (Πw.P ? (maDIR2 w)) → P ? maIX0 → (Πb.P ? (maIX1 b)) → (Πw.P ? (maIX2 w)) →
-   (Πb.P ? (maSP1 b)) → (Πw.P ? (maSP2 w)) → (Πb1,b2.P ? (maDIR1_to_DIR1 b1 b2)) →
-   (Πb1,b2.P ? (maIMM1_to_DIR1 b1 b2)) → (Πb.P ? (maIX0p_to_DIR1 b)) → (Πb.P ? (maDIR1_to_IX0p b)) →
-   (Πb.P ? (maINHA_and_IMM1 b)) → (Πb.P ? (maINHX_and_IMM1 b)) → (Πb1,b2.P ? (maIMM1_and_IMM1 b1 b2)) →
-   (Πb1,b2.P ? (maDIR1_and_IMM1 b1 b2)) → (Πb.P ? (maIX0_and_IMM1 b)) → (Πb.P ? (maIX0p_and_IMM1 b)) →
-   (Πb1,b2.P ? (maIX1_and_IMM1 b1 b2)) → (Πb1,b2.P ? (maIX1p_and_IMM1 b1 b2)) → (Πb1,b2.P ? (maSP1_and_IMM1 b1 b2)) →
-   (Πn,b.P ? ((maDIRn n) b)) → (Πn,b1,b2.P ? ((maDIRn_and_IMM1 n) b1 b2)) → (Πe.P ? (maTNY e)) → (Πt.P ? (maSRT t)) →
-   Πma:MA_check i.P i ma ≝
-λi:instr_mode.λP:Πj.MA_check j → Set.
-λp:P ? maINH.λp1:P ? maINHA.λp2:P ? maINHX.λp3:P ? maINHH.λp4:P ? maINHX0ADD.
-λf:Πb.P ? (maINHX1ADD b).λf1:Πw.P ? (maINHX2ADD w).λf2:Πb.P ? (maIMM1 b).λf3:Πb.P ? (maIMM1EXT b).
-λf4:Πw.P ? (maIMM2 w).λf5:Πb.P ? (maDIR1 b).λf6:Πw.P ? (maDIR2 w).λp5:P ? maIX0.
-λf7:Πb.P ? (maIX1 b).λf8:Πw.P ? (maIX2 w).λf9:Πb.P ? (maSP1 b).λf10:Πw.P ? (maSP2 w).
-λf11:Πb1,b2.P ? (maDIR1_to_DIR1 b1 b2).λf12:Πb1,b2.P ? (maIMM1_to_DIR1 b1 b2).
-λf13:Πb.P ? (maIX0p_to_DIR1 b).λf14:Πb.P ? (maDIR1_to_IX0p b).λf15:Πb.P ? (maINHA_and_IMM1 b).
-λf16:Πb.P ? (maINHX_and_IMM1 b).λf17:Πb1,b2.P ? (maIMM1_and_IMM1 b1 b2).
-λf18:Πb1,b2.P ? (maDIR1_and_IMM1 b1 b2).λf19:Πb.P ? (maIX0_and_IMM1 b).
-λf20:Πb.P ? (maIX0p_and_IMM1 b).λf21:Πb1,b2.P ? (maIX1_and_IMM1 b1 b2).
-λf22:Πb1,b2.P ? (maIX1p_and_IMM1 b1 b2).λf23:Πb1,b2.P ? (maSP1_and_IMM1 b1 b2).
-λf24:Πn,b.P ? ((maDIRn n) b).λf25:Πn,b1,b2.P ? ((maDIRn_and_IMM1 n) b1 b2).
-λf26:Πe.P ? (maTNY e).λf27:Πt.P ? (maSRT t).λma:MA_check i.
- match ma with
-  [ maINH ⇒ p | maINHA ⇒ p1 | maINHX ⇒ p2 | maINHH ⇒ p3 | maINHX0ADD ⇒ p4
-  | maINHX1ADD b ⇒ f b | maINHX2ADD w ⇒ f1 w | maIMM1 b ⇒ f2 b | maIMM1EXT b ⇒ f3 b
-  | maIMM2 w ⇒ f4 w | maDIR1 b ⇒ f5 b | maDIR2 w ⇒ f6 w | maIX0 ⇒ p5 | maIX1 b ⇒ f7 b
-  | maIX2 w ⇒ f8 w | maSP1 b ⇒ f9 b | maSP2 w ⇒ f10 w | maDIR1_to_DIR1 b1 b2 ⇒ f11 b1 b2
-  | maIMM1_to_DIR1 b1 b2 ⇒ f12 b1 b2 | maIX0p_to_DIR1 b ⇒ f13 b | maDIR1_to_IX0p b ⇒ f14 b
-  | maINHA_and_IMM1 b ⇒ f15 b | maINHX_and_IMM1 b ⇒ f16 b | maIMM1_and_IMM1 b1 b2 ⇒ f17 b1 b2
-  | maDIR1_and_IMM1 b1 b2 ⇒ f18 b1 b2 | maIX0_and_IMM1 b ⇒ f19 b | maIX0p_and_IMM1 b ⇒ f20 b
-  | maIX1_and_IMM1 b1 b2 ⇒ f21 b1 b2 | maIX1p_and_IMM1 b1 b2 ⇒ f22 b1 b2 | maSP1_and_IMM1 b1 b2 ⇒ f23 b1 b2
-  | maDIRn n b ⇒ f24 n b | maDIRn_and_IMM1 n b1 b2 ⇒ f25 n b1 b2 | maTNY e ⇒ f26 e | maSRT t ⇒ f27 t ].
-
-ndefinition instr_mode_rect
- : Πi:instr_mode.ΠP:Πj.MA_check j → Type.
-   P ? maINH → P ? maINHA → P ? maINHX → P ? maINHH → P ? maINHX0ADD → (Πb.P ? (maINHX1ADD b)) →
-   (Πw.P ? (maINHX2ADD w)) → (Πb.P ? (maIMM1 b)) → (Πb.P ? (maIMM1EXT b)) → (Πw.P ? (maIMM2 w)) →
-   (Πb.P ? (maDIR1 b)) → (Πw.P ? (maDIR2 w)) → P ? maIX0 → (Πb.P ? (maIX1 b)) → (Πw.P ? (maIX2 w)) →
-   (Πb.P ? (maSP1 b)) → (Πw.P ? (maSP2 w)) → (Πb1,b2.P ? (maDIR1_to_DIR1 b1 b2)) →
-   (Πb1,b2.P ? (maIMM1_to_DIR1 b1 b2)) → (Πb.P ? (maIX0p_to_DIR1 b)) → (Πb.P ? (maDIR1_to_IX0p b)) →
-   (Πb.P ? (maINHA_and_IMM1 b)) → (Πb.P ? (maINHX_and_IMM1 b)) → (Πb1,b2.P ? (maIMM1_and_IMM1 b1 b2)) →
-   (Πb1,b2.P ? (maDIR1_and_IMM1 b1 b2)) → (Πb.P ? (maIX0_and_IMM1 b)) → (Πb.P ? (maIX0p_and_IMM1 b)) →
-   (Πb1,b2.P ? (maIX1_and_IMM1 b1 b2)) → (Πb1,b2.P ? (maIX1p_and_IMM1 b1 b2)) → (Πb1,b2.P ? (maSP1_and_IMM1 b1 b2)) →
-   (Πn,b.P ? ((maDIRn n) b)) → (Πn,b1,b2.P ? ((maDIRn_and_IMM1 n) b1 b2)) → (Πe.P ? (maTNY e)) → (Πt.P ? (maSRT t)) →
-   Πma:MA_check i.P i ma ≝
-λi:instr_mode.λP:Πj.MA_check j → Type.
-λp:P ? maINH.λp1:P ? maINHA.λp2:P ? maINHX.λp3:P ? maINHH.λp4:P ? maINHX0ADD.
-λf:Πb.P ? (maINHX1ADD b).λf1:Πw.P ? (maINHX2ADD w).λf2:Πb.P ? (maIMM1 b).λf3:Πb.P ? (maIMM1EXT b).
-λf4:Πw.P ? (maIMM2 w).λf5:Πb.P ? (maDIR1 b).λf6:Πw.P ? (maDIR2 w).λp5:P ? maIX0.
-λf7:Πb.P ? (maIX1 b).λf8:Πw.P ? (maIX2 w).λf9:Πb.P ? (maSP1 b).λf10:Πw.P ? (maSP2 w).
-λf11:Πb1,b2.P ? (maDIR1_to_DIR1 b1 b2).λf12:Πb1,b2.P ? (maIMM1_to_DIR1 b1 b2).
-λf13:Πb.P ? (maIX0p_to_DIR1 b).λf14:Πb.P ? (maDIR1_to_IX0p b).λf15:Πb.P ? (maINHA_and_IMM1 b).
-λf16:Πb.P ? (maINHX_and_IMM1 b).λf17:Πb1,b2.P ? (maIMM1_and_IMM1 b1 b2).
-λf18:Πb1,b2.P ? (maDIR1_and_IMM1 b1 b2).λf19:Πb.P ? (maIX0_and_IMM1 b).
-λf20:Πb.P ? (maIX0p_and_IMM1 b).λf21:Πb1,b2.P ? (maIX1_and_IMM1 b1 b2).
-λf22:Πb1,b2.P ? (maIX1p_and_IMM1 b1 b2).λf23:Πb1,b2.P ? (maSP1_and_IMM1 b1 b2).
-λf24:Πn,b.P ? ((maDIRn n) b).λf25:Πn,b1,b2.P ? ((maDIRn_and_IMM1 n) b1 b2).
-λf26:Πe.P ? (maTNY e).λf27:Πt.P ? (maSRT t).λma:MA_check i.
- match ma with
-  [ maINH ⇒ p | maINHA ⇒ p1 | maINHX ⇒ p2 | maINHH ⇒ p3 | maINHX0ADD ⇒ p4
-  | maINHX1ADD b ⇒ f b | maINHX2ADD w ⇒ f1 w | maIMM1 b ⇒ f2 b | maIMM1EXT b ⇒ f3 b
-  | maIMM2 w ⇒ f4 w | maDIR1 b ⇒ f5 b | maDIR2 w ⇒ f6 w | maIX0 ⇒ p5 | maIX1 b ⇒ f7 b
-  | maIX2 w ⇒ f8 w | maSP1 b ⇒ f9 b | maSP2 w ⇒ f10 w | maDIR1_to_DIR1 b1 b2 ⇒ f11 b1 b2
-  | maIMM1_to_DIR1 b1 b2 ⇒ f12 b1 b2 | maIX0p_to_DIR1 b ⇒ f13 b | maDIR1_to_IX0p b ⇒ f14 b
-  | maINHA_and_IMM1 b ⇒ f15 b | maINHX_and_IMM1 b ⇒ f16 b | maIMM1_and_IMM1 b1 b2 ⇒ f17 b1 b2
-  | maDIR1_and_IMM1 b1 b2 ⇒ f18 b1 b2 | maIX0_and_IMM1 b ⇒ f19 b | maIX0p_and_IMM1 b ⇒ f20 b
-  | maIX1_and_IMM1 b1 b2 ⇒ f21 b1 b2 | maIX1p_and_IMM1 b1 b2 ⇒ f22 b1 b2 | maSP1_and_IMM1 b1 b2 ⇒ f23 b1 b2
-  | maDIRn n b ⇒ f24 n b | maDIRn_and_IMM1 n b1 b2 ⇒ f25 n b1 b2 | maTNY e ⇒ f26 e | maSRT t ⇒ f27 t ].
-
 (* picker: trasforma l'argomento necessario in input a bytes_of_pseudo_instr_mode_param:
    MA_check i → list (t_byte8 m) *)
 ndefinition args_picker ≝
@@ -304,8 +169,8 @@ 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
-   [ true ⇒ match thd4T ???? 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))
     | Word isaw ⇒
@@ -333,10 +198,10 @@ ndefinition defined_option ≝
 ndefinition compile ≝
 λmcu:mcu_type.λi:instr_mode.λop:opcode.λarg:MA_check i.
  match bytes_of_pseudo_instr_mode_param mcu (anyOP mcu op) i arg
-  return λres:option (list (t_byte8 mcu)).defined_option (list (t_byte8 mcu)) res → (list (t_byte8 mcu))
+  return λres:option ?.defined_option ? res → ?
  with
-  [ None ⇒ λp:defined_option (list (t_byte8 mcu)) (None ?).False_rect ? p
-  | Some x ⇒ λp:defined_option (list (t_byte8 mcu)) (Some ? x).x
+  [ None ⇒ λp:defined_option ? (None ?).False_rect_Type0 ? p
+  | Some x ⇒ λp:defined_option ? (Some ? x).x
   ].
 
 (* detipatore del compilato: (t_byte8 m) → byte8 *)