helm/software/matita/contribs/ng_assembly/freescale/translation.ma

   1 (**************************************************************************)
   2 (*       ___                                                              *)
   3 (*      ||M||                                                             *)
   4 (*      ||A||       A project by Andrea Asperti                           *)
   5 (*      ||T||                                                             *)
   6 (*      ||I||       Developers:                                           *)
   7 (*      ||T||         The HELM team.                                      *)
   8 (*      ||A||         http://helm.cs.unibo.it                             *)
   9 (*      \   /                                                             *)
  10 (*       \ /        This file is distributed under the terms of the       *)
  11 (*        v         GNU General Public License Version 2                  *)
  12 (*                                                                        *)
  13 (**************************************************************************)
  14
  15 (* ********************************************************************** *)
  16 (*                           Progetto FreeScale                           *)
  17 (*                                                                        *)
  18 (* Sviluppato da:                                                         *)
  19 (*   Cosimo Oliboni, oliboni@cs.unibo.it                                  *)
  20 (*                                                                        *)
  21 (* Questo materiale fa parte della tesi:                                  *)
  22 (*   "Formalizzazione Interattiva dei Microcontroller a 8bit FreeScale"   *)
  23 (*                                                                        *)
  24 (*                    data ultima modifica 15/11/2007                     *)
  25 (* ********************************************************************** *)
  26
  27 include "freescale/table_HC05.ma".
  28 include "freescale/table_HC08.ma".
  29 include "freescale/table_HCS08.ma".
  30 include "freescale/table_RS08.ma".
  31 include "freescale/option.ma".
  32
  33 (* ***************************** *)
  34 (* TRADUZIONE ESADECIMALE → INFO *)
  35 (* ***************************** *)
  36
  37 (* accesso alla tabella della ALU prescelta *)
  38 ndefinition opcode_table ≝
  39 λm:mcu_type.
  40  match m
  41   return λm:mcu_type.list (Prod4T (any_opcode m) instr_mode byte8_or_word16 byte8)
  42  with
  43   [ HC05  ⇒ opcode_table_HC05
  44   | HC08  ⇒ opcode_table_HC08
  45   | HCS08 ⇒ opcode_table_HCS08
  46   | RS08  ⇒ opcode_table_RS08
  47  ].
  48
  49 (* traduzione mcu+esadecimale → info *)
  50 (* NB: la ricerca per byte non matcha con una word con lo stesso byte superiore uguale *)
  51 (* NB: per matchare una word (precode+code) bisogna passare una word *)
  52 (* NB: il risultato e' sempre un'opzione, NON esiste un dummy opcode tipo UNKNOWN/ILLEGAL *)
  53 nlet rec full_info_of_word16_aux (m:mcu_type) (borw:byte8_or_word16)
  54                                 (param:list (Prod4T (any_opcode m) instr_mode byte8_or_word16 byte8)) on param ≝
  55  match param with
  56   [ nil ⇒ None ?
  57   | cons hd tl ⇒
  58    match thd4T ???? hd with
  59     [ Byte b ⇒ match borw with
  60      [ Byte borw' ⇒ match eq_b8 borw' b with
  61       [ true ⇒ Some ? hd
  62       | false ⇒ full_info_of_word16_aux m borw tl ]
  63      | Word _ ⇒ full_info_of_word16_aux m borw tl ]
  64     | Word w ⇒ match borw with
  65      [ Byte _ ⇒ full_info_of_word16_aux m borw tl
  66      | Word borw' ⇒ match eq_w16 borw' w with
  67       [ true ⇒ Some ? hd
  68       | false ⇒ full_info_of_word16_aux m borw tl ]
  69     ]]].
  70
  71 ndefinition full_info_of_word16 ≝
  72 λm:mcu_type.λborw:byte8_or_word16.
  73 full_info_of_word16_aux m borw (opcode_table m).
  74
  75 (* ******************************************************* *)
  76 (* TRADUZIONE MCU+OPCODE+MODALITA'+ARGOMENTI → ESADECIMALE *)
  77 (* ******************************************************* *)
  78
  79 (* introduzione di un tipo byte8 dipendente dall'mcu_type (phantom type) *)
  80 ninductive t_byte8 (m:mcu_type) : Type ≝
  81  TByte : byte8 → t_byte8 m.
  82
  83 ndefinition t_byte8_ind
  84  : Πm:mcu_type.ΠP:t_byte8 m → Prop.(Πb:byte8.P (TByte m b)) → Πt:t_byte8 m.P t ≝
  85 λm:mcu_type.λP:t_byte8 m → Prop.λf:Πb:byte8.P (TByte m b).λt:t_byte8 m.
  86  match t with [ TByte (b:byte8) ⇒ f b ].
  87
  88 ndefinition t_byte8_rec
  89  : Πm:mcu_type.ΠP:t_byte8 m → Set.(Πb:byte8.P (TByte m b)) → Πt:t_byte8 m.P t ≝
  90 λm:mcu_type.λP:t_byte8 m → Set.λf:Πb:byte8.P (TByte m b).λt:t_byte8 m.
  91  match t with [ TByte (b:byte8) ⇒ f b ].
  92
  93 ndefinition t_byte8_rect
  94  : Πm:mcu_type.ΠP:t_byte8 m → Type.(Πb:byte8.P (TByte m b)) → Πt:t_byte8 m.P t ≝
  95 λm:mcu_type.λP:t_byte8 m → Type.λf:Πb:byte8.P (TByte m b).λt:t_byte8 m.
  96  match t with [ TByte (b:byte8) ⇒ f b ].
  97
  98 nlemma tbyte8_destruct : ∀m,b1,b2.TByte m b1 = TByte m b2 → b1 = b2.
  99  #m; #b1; #b2; #H;
 100  nchange with (match TByte m b2 with [ TByte a ⇒ b1 = a ]);
 101  nrewrite < H;
 102  nnormalize;
 103  napply (refl_eq ??).
 104 nqed.
 105
 106 (* introduzione di un tipo dipendente (dalla modalita') per gli argomenti *)
 107 ninductive MA_check : instr_mode → Type ≝
 108   maINH              : MA_check MODE_INH
 109 | maINHA             : MA_check MODE_INHA
 110 | maINHX             : MA_check MODE_INHX
 111 | maINHH             : MA_check MODE_INHH
 112 | maINHX0ADD         : MA_check MODE_INHX0ADD
 113 | maINHX1ADD         : byte8 → MA_check MODE_INHX1ADD
 114 | maINHX2ADD         : word16 → MA_check MODE_INHX2ADD
 115 | maIMM1             : byte8  → MA_check MODE_IMM1
 116 | maIMM1EXT          : byte8  → MA_check MODE_IMM1EXT
 117 | maIMM2             : word16 → MA_check MODE_IMM2
 118 | maDIR1             : byte8  → MA_check MODE_DIR1
 119 | maDIR2             : word16 → MA_check MODE_DIR2
 120 | maIX0              : MA_check MODE_IX0
 121 | maIX1              : byte8  → MA_check MODE_IX1
 122 | maIX2              : word16 → MA_check MODE_IX2
 123 | maSP1              : byte8  → MA_check MODE_SP1
 124 | maSP2              : word16 → MA_check MODE_SP2
 125 | maDIR1_to_DIR1     : byte8 → byte8 → MA_check MODE_DIR1_to_DIR1
 126 | maIMM1_to_DIR1     : byte8 → byte8 → MA_check MODE_IMM1_to_DIR1
 127 | maIX0p_to_DIR1     : byte8 → MA_check MODE_IX0p_to_DIR1
 128 | maDIR1_to_IX0p     : byte8 → MA_check MODE_DIR1_to_IX0p
 129 | maINHA_and_IMM1    : byte8 → MA_check MODE_INHA_and_IMM1
 130 | maINHX_and_IMM1    : byte8 → MA_check MODE_INHX_and_IMM1
 131 | maIMM1_and_IMM1    : byte8 → byte8 → MA_check MODE_IMM1_and_IMM1
 132 | maDIR1_and_IMM1    : byte8 → byte8 → MA_check MODE_DIR1_and_IMM1
 133 | maIX0_and_IMM1     : byte8 → MA_check MODE_IX0_and_IMM1
 134 | maIX0p_and_IMM1    : byte8 → MA_check MODE_IX0p_and_IMM1
 135 | maIX1_and_IMM1     : byte8 → byte8 → MA_check MODE_IX1_and_IMM1
 136 | maIX1p_and_IMM1    : byte8 → byte8 → MA_check MODE_IX1p_and_IMM1
 137 | maSP1_and_IMM1     : byte8 → byte8 → MA_check MODE_SP1_and_IMM1
 138 | maDIRn             : ∀n.byte8 → MA_check (MODE_DIRn n)
 139 | maDIRn_and_IMM1    : ∀n.byte8 → byte8 → MA_check (MODE_DIRn_and_IMM1 n)
 140 | maTNY              : ∀e.MA_check (MODE_TNY e)
 141 | maSRT              : ∀t.MA_check (MODE_SRT t)
 142 .
 143
 144 ndefinition instr_mode_ind
 145  : Πi:instr_mode.ΠP:Πj.MA_check j → Prop.
 146    P ? maINH → P ? maINHA → P ? maINHX → P ? maINHH → P ? maINHX0ADD → (Πb.P ? (maINHX1ADD b)) →
 147    (Πw.P ? (maINHX2ADD w)) → (Πb.P ? (maIMM1 b)) → (Πb.P ? (maIMM1EXT b)) → (Πw.P ? (maIMM2 w)) →
 148    (Πb.P ? (maDIR1 b)) → (Πw.P ? (maDIR2 w)) → P ? maIX0 → (Πb.P ? (maIX1 b)) → (Πw.P ? (maIX2 w)) →
 149    (Πb.P ? (maSP1 b)) → (Πw.P ? (maSP2 w)) → (Πb1,b2.P ? (maDIR1_to_DIR1 b1 b2)) →
 150    (Πb1,b2.P ? (maIMM1_to_DIR1 b1 b2)) → (Πb.P ? (maIX0p_to_DIR1 b)) → (Πb.P ? (maDIR1_to_IX0p b)) →
 151    (Πb.P ? (maINHA_and_IMM1 b)) → (Πb.P ? (maINHX_and_IMM1 b)) → (Πb1,b2.P ? (maIMM1_and_IMM1 b1 b2)) →
 152    (Πb1,b2.P ? (maDIR1_and_IMM1 b1 b2)) → (Πb.P ? (maIX0_and_IMM1 b)) → (Πb.P ? (maIX0p_and_IMM1 b)) →
 153    (Πb1,b2.P ? (maIX1_and_IMM1 b1 b2)) → (Πb1,b2.P ? (maIX1p_and_IMM1 b1 b2)) → (Πb1,b2.P ? (maSP1_and_IMM1 b1 b2)) →
 154    (Πn,b.P ? ((maDIRn n) b)) → (Πn,b1,b2.P ? ((maDIRn_and_IMM1 n) b1 b2)) → (Πe.P ? (maTNY e)) → (Πt.P ? (maSRT t)) →
 155    Πma:MA_check i.P i ma ≝
 156 λi:instr_mode.λP:Πj.MA_check j → Prop.
 157 λp:P ? maINH.λp1:P ? maINHA.λp2:P ? maINHX.λp3:P ? maINHH.λp4:P ? maINHX0ADD.
 158 λf:Πb.P ? (maINHX1ADD b).λf1:Πw.P ? (maINHX2ADD w).λf2:Πb.P ? (maIMM1 b).λf3:Πb.P ? (maIMM1EXT b).
 159 λf4:Πw.P ? (maIMM2 w).λf5:Πb.P ? (maDIR1 b).λf6:Πw.P ? (maDIR2 w).λp5:P ? maIX0.
 160 λf7:Πb.P ? (maIX1 b).λf8:Πw.P ? (maIX2 w).λf9:Πb.P ? (maSP1 b).λf10:Πw.P ? (maSP2 w).
 161 λf11:Πb1,b2.P ? (maDIR1_to_DIR1 b1 b2).λf12:Πb1,b2.P ? (maIMM1_to_DIR1 b1 b2).
 162 λf13:Πb.P ? (maIX0p_to_DIR1 b).λf14:Πb.P ? (maDIR1_to_IX0p b).λf15:Πb.P ? (maINHA_and_IMM1 b).
 163 λf16:Πb.P ? (maINHX_and_IMM1 b).λf17:Πb1,b2.P ? (maIMM1_and_IMM1 b1 b2).
 164 λf18:Πb1,b2.P ? (maDIR1_and_IMM1 b1 b2).λf19:Πb.P ? (maIX0_and_IMM1 b).
 165 λf20:Πb.P ? (maIX0p_and_IMM1 b).λf21:Πb1,b2.P ? (maIX1_and_IMM1 b1 b2).
 166 λf22:Πb1,b2.P ? (maIX1p_and_IMM1 b1 b2).λf23:Πb1,b2.P ? (maSP1_and_IMM1 b1 b2).
 167 λf24:Πn,b.P ? ((maDIRn n) b).λf25:Πn,b1,b2.P ? ((maDIRn_and_IMM1 n) b1 b2).
 168 λf26:Πe.P ? (maTNY e).λf27:Πt.P ? (maSRT t).λma:MA_check i.
 169  match ma with
 170   [ maINH ⇒ p | maINHA ⇒ p1 | maINHX ⇒ p2 | maINHH ⇒ p3 | maINHX0ADD ⇒ p4
 171   | maINHX1ADD b ⇒ f b | maINHX2ADD w ⇒ f1 w | maIMM1 b ⇒ f2 b | maIMM1EXT b ⇒ f3 b
 172   | maIMM2 w ⇒ f4 w | maDIR1 b ⇒ f5 b | maDIR2 w ⇒ f6 w | maIX0 ⇒ p5 | maIX1 b ⇒ f7 b
 173   | maIX2 w ⇒ f8 w | maSP1 b ⇒ f9 b | maSP2 w ⇒ f10 w | maDIR1_to_DIR1 b1 b2 ⇒ f11 b1 b2
 174   | maIMM1_to_DIR1 b1 b2 ⇒ f12 b1 b2 | maIX0p_to_DIR1 b ⇒ f13 b | maDIR1_to_IX0p b ⇒ f14 b
 175   | maINHA_and_IMM1 b ⇒ f15 b | maINHX_and_IMM1 b ⇒ f16 b | maIMM1_and_IMM1 b1 b2 ⇒ f17 b1 b2
 176   | maDIR1_and_IMM1 b1 b2 ⇒ f18 b1 b2 | maIX0_and_IMM1 b ⇒ f19 b | maIX0p_and_IMM1 b ⇒ f20 b
 177   | maIX1_and_IMM1 b1 b2 ⇒ f21 b1 b2 | maIX1p_and_IMM1 b1 b2 ⇒ f22 b1 b2 | maSP1_and_IMM1 b1 b2 ⇒ f23 b1 b2
 178   | maDIRn n b ⇒ f24 n b | maDIRn_and_IMM1 n b1 b2 ⇒ f25 n b1 b2 | maTNY e ⇒ f26 e | maSRT t ⇒ f27 t ].
 179
 180 ndefinition instr_mode_rec
 181  : Πi:instr_mode.ΠP:Πj.MA_check j → Set.
 182    P ? maINH → P ? maINHA → P ? maINHX → P ? maINHH → P ? maINHX0ADD → (Πb.P ? (maINHX1ADD b)) →
 183    (Πw.P ? (maINHX2ADD w)) → (Πb.P ? (maIMM1 b)) → (Πb.P ? (maIMM1EXT b)) → (Πw.P ? (maIMM2 w)) →
 184    (Πb.P ? (maDIR1 b)) → (Πw.P ? (maDIR2 w)) → P ? maIX0 → (Πb.P ? (maIX1 b)) → (Πw.P ? (maIX2 w)) →
 185    (Πb.P ? (maSP1 b)) → (Πw.P ? (maSP2 w)) → (Πb1,b2.P ? (maDIR1_to_DIR1 b1 b2)) →
 186    (Πb1,b2.P ? (maIMM1_to_DIR1 b1 b2)) → (Πb.P ? (maIX0p_to_DIR1 b)) → (Πb.P ? (maDIR1_to_IX0p b)) →
 187    (Πb.P ? (maINHA_and_IMM1 b)) → (Πb.P ? (maINHX_and_IMM1 b)) → (Πb1,b2.P ? (maIMM1_and_IMM1 b1 b2)) →
 188    (Πb1,b2.P ? (maDIR1_and_IMM1 b1 b2)) → (Πb.P ? (maIX0_and_IMM1 b)) → (Πb.P ? (maIX0p_and_IMM1 b)) →
 189    (Πb1,b2.P ? (maIX1_and_IMM1 b1 b2)) → (Πb1,b2.P ? (maIX1p_and_IMM1 b1 b2)) → (Πb1,b2.P ? (maSP1_and_IMM1 b1 b2)) →
 190    (Πn,b.P ? ((maDIRn n) b)) → (Πn,b1,b2.P ? ((maDIRn_and_IMM1 n) b1 b2)) → (Πe.P ? (maTNY e)) → (Πt.P ? (maSRT t)) →
 191    Πma:MA_check i.P i ma ≝
 192 λi:instr_mode.λP:Πj.MA_check j → Set.
 193 λp:P ? maINH.λp1:P ? maINHA.λp2:P ? maINHX.λp3:P ? maINHH.λp4:P ? maINHX0ADD.
 194 λf:Πb.P ? (maINHX1ADD b).λf1:Πw.P ? (maINHX2ADD w).λf2:Πb.P ? (maIMM1 b).λf3:Πb.P ? (maIMM1EXT b).
 195 λf4:Πw.P ? (maIMM2 w).λf5:Πb.P ? (maDIR1 b).λf6:Πw.P ? (maDIR2 w).λp5:P ? maIX0.
 196 λf7:Πb.P ? (maIX1 b).λf8:Πw.P ? (maIX2 w).λf9:Πb.P ? (maSP1 b).λf10:Πw.P ? (maSP2 w).
 197 λf11:Πb1,b2.P ? (maDIR1_to_DIR1 b1 b2).λf12:Πb1,b2.P ? (maIMM1_to_DIR1 b1 b2).
 198 λf13:Πb.P ? (maIX0p_to_DIR1 b).λf14:Πb.P ? (maDIR1_to_IX0p b).λf15:Πb.P ? (maINHA_and_IMM1 b).
 199 λf16:Πb.P ? (maINHX_and_IMM1 b).λf17:Πb1,b2.P ? (maIMM1_and_IMM1 b1 b2).
 200 λf18:Πb1,b2.P ? (maDIR1_and_IMM1 b1 b2).λf19:Πb.P ? (maIX0_and_IMM1 b).
 201 λf20:Πb.P ? (maIX0p_and_IMM1 b).λf21:Πb1,b2.P ? (maIX1_and_IMM1 b1 b2).
 202 λf22:Πb1,b2.P ? (maIX1p_and_IMM1 b1 b2).λf23:Πb1,b2.P ? (maSP1_and_IMM1 b1 b2).
 203 λf24:Πn,b.P ? ((maDIRn n) b).λf25:Πn,b1,b2.P ? ((maDIRn_and_IMM1 n) b1 b2).
 204 λf26:Πe.P ? (maTNY e).λf27:Πt.P ? (maSRT t).λma:MA_check i.
 205  match ma with
 206   [ maINH ⇒ p | maINHA ⇒ p1 | maINHX ⇒ p2 | maINHH ⇒ p3 | maINHX0ADD ⇒ p4
 207   | maINHX1ADD b ⇒ f b | maINHX2ADD w ⇒ f1 w | maIMM1 b ⇒ f2 b | maIMM1EXT b ⇒ f3 b
 208   | maIMM2 w ⇒ f4 w | maDIR1 b ⇒ f5 b | maDIR2 w ⇒ f6 w | maIX0 ⇒ p5 | maIX1 b ⇒ f7 b
 209   | maIX2 w ⇒ f8 w | maSP1 b ⇒ f9 b | maSP2 w ⇒ f10 w | maDIR1_to_DIR1 b1 b2 ⇒ f11 b1 b2
 210   | maIMM1_to_DIR1 b1 b2 ⇒ f12 b1 b2 | maIX0p_to_DIR1 b ⇒ f13 b | maDIR1_to_IX0p b ⇒ f14 b
 211   | maINHA_and_IMM1 b ⇒ f15 b | maINHX_and_IMM1 b ⇒ f16 b | maIMM1_and_IMM1 b1 b2 ⇒ f17 b1 b2
 212   | maDIR1_and_IMM1 b1 b2 ⇒ f18 b1 b2 | maIX0_and_IMM1 b ⇒ f19 b | maIX0p_and_IMM1 b ⇒ f20 b
 213   | maIX1_and_IMM1 b1 b2 ⇒ f21 b1 b2 | maIX1p_and_IMM1 b1 b2 ⇒ f22 b1 b2 | maSP1_and_IMM1 b1 b2 ⇒ f23 b1 b2
 214   | maDIRn n b ⇒ f24 n b | maDIRn_and_IMM1 n b1 b2 ⇒ f25 n b1 b2 | maTNY e ⇒ f26 e | maSRT t ⇒ f27 t ].
 215
 216 ndefinition instr_mode_rect
 217  : Πi:instr_mode.ΠP:Πj.MA_check j → Type.
 218    P ? maINH → P ? maINHA → P ? maINHX → P ? maINHH → P ? maINHX0ADD → (Πb.P ? (maINHX1ADD b)) →
 219    (Πw.P ? (maINHX2ADD w)) → (Πb.P ? (maIMM1 b)) → (Πb.P ? (maIMM1EXT b)) → (Πw.P ? (maIMM2 w)) →
 220    (Πb.P ? (maDIR1 b)) → (Πw.P ? (maDIR2 w)) → P ? maIX0 → (Πb.P ? (maIX1 b)) → (Πw.P ? (maIX2 w)) →
 221    (Πb.P ? (maSP1 b)) → (Πw.P ? (maSP2 w)) → (Πb1,b2.P ? (maDIR1_to_DIR1 b1 b2)) →
 222    (Πb1,b2.P ? (maIMM1_to_DIR1 b1 b2)) → (Πb.P ? (maIX0p_to_DIR1 b)) → (Πb.P ? (maDIR1_to_IX0p b)) →
 223    (Πb.P ? (maINHA_and_IMM1 b)) → (Πb.P ? (maINHX_and_IMM1 b)) → (Πb1,b2.P ? (maIMM1_and_IMM1 b1 b2)) →
 224    (Πb1,b2.P ? (maDIR1_and_IMM1 b1 b2)) → (Πb.P ? (maIX0_and_IMM1 b)) → (Πb.P ? (maIX0p_and_IMM1 b)) →
 225    (Πb1,b2.P ? (maIX1_and_IMM1 b1 b2)) → (Πb1,b2.P ? (maIX1p_and_IMM1 b1 b2)) → (Πb1,b2.P ? (maSP1_and_IMM1 b1 b2)) →
 226    (Πn,b.P ? ((maDIRn n) b)) → (Πn,b1,b2.P ? ((maDIRn_and_IMM1 n) b1 b2)) → (Πe.P ? (maTNY e)) → (Πt.P ? (maSRT t)) →
 227    Πma:MA_check i.P i ma ≝
 228 λi:instr_mode.λP:Πj.MA_check j → Type.
 229 λp:P ? maINH.λp1:P ? maINHA.λp2:P ? maINHX.λp3:P ? maINHH.λp4:P ? maINHX0ADD.
 230 λf:Πb.P ? (maINHX1ADD b).λf1:Πw.P ? (maINHX2ADD w).λf2:Πb.P ? (maIMM1 b).λf3:Πb.P ? (maIMM1EXT b).
 231 λf4:Πw.P ? (maIMM2 w).λf5:Πb.P ? (maDIR1 b).λf6:Πw.P ? (maDIR2 w).λp5:P ? maIX0.
 232 λf7:Πb.P ? (maIX1 b).λf8:Πw.P ? (maIX2 w).λf9:Πb.P ? (maSP1 b).λf10:Πw.P ? (maSP2 w).
 233 λf11:Πb1,b2.P ? (maDIR1_to_DIR1 b1 b2).λf12:Πb1,b2.P ? (maIMM1_to_DIR1 b1 b2).
 234 λf13:Πb.P ? (maIX0p_to_DIR1 b).λf14:Πb.P ? (maDIR1_to_IX0p b).λf15:Πb.P ? (maINHA_and_IMM1 b).
 235 λf16:Πb.P ? (maINHX_and_IMM1 b).λf17:Πb1,b2.P ? (maIMM1_and_IMM1 b1 b2).
 236 λf18:Πb1,b2.P ? (maDIR1_and_IMM1 b1 b2).λf19:Πb.P ? (maIX0_and_IMM1 b).
 237 λf20:Πb.P ? (maIX0p_and_IMM1 b).λf21:Πb1,b2.P ? (maIX1_and_IMM1 b1 b2).
 238 λf22:Πb1,b2.P ? (maIX1p_and_IMM1 b1 b2).λf23:Πb1,b2.P ? (maSP1_and_IMM1 b1 b2).
 239 λf24:Πn,b.P ? ((maDIRn n) b).λf25:Πn,b1,b2.P ? ((maDIRn_and_IMM1 n) b1 b2).
 240 λf26:Πe.P ? (maTNY e).λf27:Πt.P ? (maSRT t).λma:MA_check i.
 241  match ma with
 242   [ maINH ⇒ p | maINHA ⇒ p1 | maINHX ⇒ p2 | maINHH ⇒ p3 | maINHX0ADD ⇒ p4
 243   | maINHX1ADD b ⇒ f b | maINHX2ADD w ⇒ f1 w | maIMM1 b ⇒ f2 b | maIMM1EXT b ⇒ f3 b
 244   | maIMM2 w ⇒ f4 w | maDIR1 b ⇒ f5 b | maDIR2 w ⇒ f6 w | maIX0 ⇒ p5 | maIX1 b ⇒ f7 b
 245   | maIX2 w ⇒ f8 w | maSP1 b ⇒ f9 b | maSP2 w ⇒ f10 w | maDIR1_to_DIR1 b1 b2 ⇒ f11 b1 b2
 246   | maIMM1_to_DIR1 b1 b2 ⇒ f12 b1 b2 | maIX0p_to_DIR1 b ⇒ f13 b | maDIR1_to_IX0p b ⇒ f14 b
 247   | maINHA_and_IMM1 b ⇒ f15 b | maINHX_and_IMM1 b ⇒ f16 b | maIMM1_and_IMM1 b1 b2 ⇒ f17 b1 b2
 248   | maDIR1_and_IMM1 b1 b2 ⇒ f18 b1 b2 | maIX0_and_IMM1 b ⇒ f19 b | maIX0p_and_IMM1 b ⇒ f20 b
 249   | maIX1_and_IMM1 b1 b2 ⇒ f21 b1 b2 | maIX1p_and_IMM1 b1 b2 ⇒ f22 b1 b2 | maSP1_and_IMM1 b1 b2 ⇒ f23 b1 b2
 250   | maDIRn n b ⇒ f24 n b | maDIRn_and_IMM1 n b1 b2 ⇒ f25 n b1 b2 | maTNY e ⇒ f26 e | maSRT t ⇒ f27 t ].
 251
 252 (* picker: trasforma l'argomento necessario in input a bytes_of_pseudo_instr_mode_param:
 253    MA_check i → list (t_byte8 m) *)
 254 ndefinition args_picker ≝
 255 λm:mcu_type.λi:instr_mode.λargs:MA_check i.
 256  match args with
 257   (* inherent: legale se nessun operando *)
 258   [ maINH    ⇒ nil ?
 259   | maINHA   ⇒ nil ?
 260   | maINHX   ⇒ nil ?
 261   | maINHH   ⇒ nil ?
 262   (* inherent address: legale se nessun operando/1 byte/1 word *)
 263   | maINHX0ADD ⇒ nil ?
 264   | maINHX1ADD b ⇒ [ TByte m b ]
 265   | maINHX2ADD w ⇒ [ TByte m (w16h w); TByte m (w16l w) ]
 266   (* _0/1/2: legale se nessun operando/1 byte/1 word *)
 267   | maIMM1 b ⇒ [ TByte m b ]
 268   | maIMM1EXT b ⇒ [ TByte m b ]
 269   | maIMM2 w ⇒ [ TByte m (w16h w); TByte m (w16l w) ]
 270   | maDIR1 b ⇒ [ TByte m b ]
 271   | maDIR2 w ⇒ [ TByte m (w16h w); TByte m (w16l w) ]
 272   | maIX0    ⇒ nil ?
 273   | maIX1 b  ⇒ [ TByte m b ]
 274   | maIX2 w  ⇒ [ TByte m (w16h w); TByte m (w16l w) ]
 275   | maSP1 b  ⇒ [ TByte m b ]
 276   | maSP2 w  ⇒ [ TByte m (w16h w); TByte m (w16l w) ]
 277   (* movimento: legale se 2 operandi byte *)
 278   | maDIR1_to_DIR1 b1 b2  ⇒ [ TByte m b1 ; TByte m b2 ]
 279   | maIMM1_to_DIR1 b1 b2  ⇒ [ TByte m b1 ; TByte m b2 ]
 280   | maIX0p_to_DIR1 b      ⇒ [ TByte m b]
 281   | maDIR1_to_IX0p b      ⇒ [ TByte m b]
 282   (* cbeq/dbnz: legale se 1/2 operandi byte *)
 283   | maINHA_and_IMM1 b     ⇒ [ TByte m b]
 284   | maINHX_and_IMM1 b     ⇒ [ TByte m b]
 285   | maIMM1_and_IMM1 b1 b2 ⇒ [ TByte m b1 ; TByte m b2 ]
 286   | maDIR1_and_IMM1 b1 b2 ⇒ [ TByte m b1 ; TByte m b2 ]
 287   | maIX0_and_IMM1  b     ⇒ [ TByte m b]
 288   | maIX0p_and_IMM1 b     ⇒ [ TByte m b]
 289   | maIX1_and_IMM1  b1 b2 ⇒ [ TByte m b1 ; TByte m b2 ]
 290   | maIX1p_and_IMM1 b1 b2 ⇒ [ TByte m b1 ; TByte m b2 ]
 291   | maSP1_and_IMM1  b1 b2 ⇒ [ TByte m b1 ; TByte m b2 ]
 292   (* DIRn: legale se 1 operando byte *)
 293   | maDIRn _ b ⇒ [ TByte m b]
 294   (* DIRn_and_IMM1: legale se 2 operandi byte *)
 295   | maDIRn_and_IMM1 _ b1 b2 ⇒ [ TByte m b1 ; TByte m b2 ]
 296   (* TNY: legale se nessun operando *)
 297   | maTNY _ ⇒ nil ?
 298   (* SRT: legale se nessun operando *)
 299   | maSRT _ ⇒ nil ?
 300   ].
 301
 302 (* trasformatore finale: mcu+opcode+instr_mode+args → list (t_byte8 m) *)
 303 nlet rec bytes_of_pseudo_instr_mode_param_aux (m:mcu_type) (o:any_opcode m) (i:instr_mode) (p:MA_check i)
 304                                              (param:list (Prod4T (any_opcode m) instr_mode byte8_or_word16 byte8)) on param ≝
 305  match param with
 306  [ nil ⇒ None ? | cons hd tl ⇒
 307   match (eq_anyop m o (fst4T ???? hd)) ⊗ (eq_instrmode i (snd4T ???? hd)) with
 308    [ true ⇒ match thd4T ???? hd with
 309     [ Byte isab ⇒
 310      Some ? ([ (TByte m isab) ]@(args_picker m i p))
 311     | Word isaw ⇒
 312      Some ? ([ (TByte m (w16h isaw)) ; (TByte m (w16l isaw)) ]@(args_picker m i p))
 313     ]
 314    | false ⇒ bytes_of_pseudo_instr_mode_param_aux m o i p tl ]].
 315
 316 ndefinition bytes_of_pseudo_instr_mode_param ≝
 317 λm:mcu_type.λo:any_opcode m.λi:instr_mode.λp:MA_check i.
 318 bytes_of_pseudo_instr_mode_param_aux m o i p (opcode_table m).
 319
 320 (* ****************************** *)
 321 (* APPROCCIO COMPILAZIONE AL VOLO *)
 322 (* ****************************** *)
 323
 324 (* ausiliario di compile *)
 325 ndefinition defined_option ≝
 326  λT:Type.λo:option T.
 327   match o with
 328    [ None ⇒ False
 329    | Some _ ⇒ True
 330    ].
 331
 332 (* compila solo se l'intera istruzione+modalita'+argomenti ha riscontro nelle tabelle *)
 333 ndefinition compile ≝
 334 λmcu:mcu_type.λi:instr_mode.λop:opcode.λarg:MA_check i.
 335  match bytes_of_pseudo_instr_mode_param mcu (anyOP mcu op) i arg
 336   return λres:option (list (t_byte8 mcu)).defined_option (list (t_byte8 mcu)) res → (list (t_byte8 mcu))
 337  with
 338   [ None ⇒ λp:defined_option (list (t_byte8 mcu)) (None ?).False_rect ? p
 339   | Some x ⇒ λp:defined_option (list (t_byte8 mcu)) (Some ? x).x
 340   ].
 341
 342 (* detipatore del compilato: (t_byte8 m) → byte8 *)
 343 nlet rec source_to_byte8_HC05_aux (p1:list (t_byte8 HC05)) (p2:list byte8) ≝
 344  match p1 with
 345   [ nil ⇒ p2
 346   | cons hd tl ⇒ match hd with [ TByte b ⇒ source_to_byte8_HC05_aux tl (p2@[b]) ]
 347   ].
 348
 349 nlet rec source_to_byte8_HC08_aux (p1:list (t_byte8 HC08)) (p2:list byte8) ≝
 350  match p1 with
 351   [ nil ⇒ p2
 352   | cons hd tl ⇒ match hd with [ TByte b ⇒ source_to_byte8_HC08_aux tl (p2@[b]) ]
 353   ].
 354
 355 nlet rec source_to_byte8_HCS08_aux (p1:list (t_byte8 HCS08)) (p2:list byte8) ≝
 356  match p1 with
 357   [ nil ⇒ p2
 358   | cons hd tl ⇒ match hd with [ TByte b ⇒ source_to_byte8_HCS08_aux tl (p2@[b]) ]
 359   ].
 360
 361 nlet rec source_to_byte8_RS08_aux (p1:list (t_byte8 RS08)) (p2:list byte8) ≝
 362  match p1 with
 363   [ nil ⇒ p2
 364   | cons hd tl ⇒ match hd with [ TByte b ⇒ source_to_byte8_RS08_aux tl (p2@[b]) ]
 365   ].
 366
 367 ndefinition source_to_byte8 ≝
 368 λm:mcu_type.
 369  match m
 370   return λm:mcu_type.list (t_byte8 m) → list byte8
 371  with
 372   [ HC05 ⇒ λl:list (t_byte8 HC05).source_to_byte8_HC05_aux l []
 373   | HC08 ⇒ λl:list (t_byte8 HC08).source_to_byte8_HC08_aux l []
 374   | HCS08 ⇒ λl:list (t_byte8 HCS08).source_to_byte8_HCS08_aux l []
 375   | RS08 ⇒ λl:list (t_byte8 RS08).source_to_byte8_RS08_aux l []
 376   ].