X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2Fcontribs%2Fng_assembly%2Ffreescale%2Ftranslation.ma;fp=helm%2Fsoftware%2Fmatita%2Fcontribs%2Fng_assembly%2Ffreescale%2Ftranslation.ma;h=0474e6e9bf88bf508d912f50e792202c477f1e22;hb=c70ecb50a457d251ef1cd61960a641d491febed7;hp=0000000000000000000000000000000000000000;hpb=3819ff5482f28f3bb9be822513c7bd73c47a46e0;p=helm.git

diff --git a/helm/software/matita/contribs/ng_assembly/freescale/translation.ma b/helm/software/matita/contribs/ng_assembly/freescale/translation.ma
new file mode 100755
index 000000000..0474e6e9b
--- /dev/null
+++ b/helm/software/matita/contribs/ng_assembly/freescale/translation.ma
@@ -0,0 +1,249 @@
+(**************************************************************************)
+(*       ___                                                              *)
+(*      ||M||                                                             *)
+(*      ||A||       A project by Andrea Asperti                           *)
+(*      ||T||                                                             *)
+(*      ||I||       Developers:                                           *)
+(*      ||T||         The HELM team.                                      *)
+(*      ||A||         http://helm.cs.unibo.it                             *)
+(*      \   /                                                             *)
+(*       \ /        This file is distributed under the terms of the       *)
+(*        v         GNU General Public License Version 2                  *)
+(*                                                                        *)
+(**************************************************************************)
+
+(* ********************************************************************** *)
+(*                          Progetto FreeScale                            *)
+(*                                                                        *)
+(*   Sviluppato da: Cosimo Oliboni, oliboni@cs.unibo.it                   *)
+(*     Cosimo Oliboni, oliboni@cs.unibo.it                                *)
+(*                                                                        *)
+(* ********************************************************************** *)
+
+include "freescale/table_HC05.ma".
+include "freescale/table_HC08.ma".
+include "freescale/table_HCS08.ma".
+include "freescale/table_RS08.ma".
+include "common/option.ma".
+
+(* ***************************** *)
+(* TRADUZIONE ESADECIMALE → INFO *)
+(* ***************************** *)
+
+(* accesso alla tabella della ALU prescelta *)
+ndefinition opcode_table ≝
+λm:mcu_type.
+ match m
+  return λm:mcu_type.list (Prod4T (any_opcode m) instr_mode byte8_or_word16 byte8)
+ with
+  [ HC05  ⇒ opcode_table_HC05
+  | HC08  ⇒ opcode_table_HC08
+  | HCS08 ⇒ opcode_table_HCS08
+  | RS08  ⇒ opcode_table_RS08
+ ].
+
+(* traduzione mcu+esadecimale → info *)
+(* NB: la ricerca per byte non matcha con una word con lo stesso byte superiore uguale *)
+(* NB: per matchare una word (precode+code) bisogna passare una word *)
+(* NB: il risultato e' sempre un'opzione, NON esiste un dummy opcode tipo UNKNOWN/ILLEGAL *)
+nlet rec full_info_of_word16_aux (m:mcu_type) (borw:byte8_or_word16)
+                                (param:list (Prod4T (any_opcode m) instr_mode byte8_or_word16 byte8)) on param ≝
+ match param with
+  [ nil ⇒ None ?
+  | cons hd tl ⇒
+   match thd4T … hd with
+    [ Byte b ⇒ match borw with
+     [ Byte borw' ⇒ match eq_b8 borw' b with
+      [ true ⇒ Some ? hd
+      | false ⇒ full_info_of_word16_aux m borw tl ]
+     | Word _ ⇒ full_info_of_word16_aux m borw tl ]
+    | Word w ⇒ match borw with
+     [ Byte _ ⇒ full_info_of_word16_aux m borw tl
+     | Word borw' ⇒ match eq_w16 borw' w with
+      [ true ⇒ Some ? hd
+      | false ⇒ full_info_of_word16_aux m borw tl ]            
+    ]]].
+
+ndefinition full_info_of_word16 ≝
+λm:mcu_type.λborw:byte8_or_word16.
+full_info_of_word16_aux m borw (opcode_table m).
+
+(* ******************************************************* *)
+(* TRADUZIONE MCU+OPCODE+MODALITA'+ARGOMENTI → ESADECIMALE *)
+(* ******************************************************* *)
+
+(* introduzione di un tipo byte8 dipendente dall'mcu_type (phantom type) *)
+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.
+
+(* introduzione di un tipo dipendente (dalla modalita') per gli argomenti *)
+ninductive MA_check : instr_mode → Type ≝
+  maINH              : MA_check MODE_INH
+| maINHA             : MA_check MODE_INHA
+| maINHX             : MA_check MODE_INHX
+| maINHH             : MA_check MODE_INHH
+| maINHX0ADD         : MA_check MODE_INHX0ADD
+| maINHX1ADD         : byte8 → MA_check MODE_INHX1ADD
+| maINHX2ADD         : word16 → MA_check MODE_INHX2ADD
+| maIMM1             : byte8  → MA_check MODE_IMM1
+| maIMM1EXT          : byte8  → MA_check MODE_IMM1EXT
+| maIMM2             : word16 → MA_check MODE_IMM2
+| maDIR1             : byte8  → MA_check MODE_DIR1
+| maDIR2             : word16 → MA_check MODE_DIR2
+| maIX0              : MA_check MODE_IX0
+| maIX1              : byte8  → MA_check MODE_IX1
+| maIX2              : word16 → MA_check MODE_IX2
+| maSP1              : byte8  → MA_check MODE_SP1
+| maSP2              : word16 → MA_check MODE_SP2
+| maDIR1_to_DIR1     : byte8 → byte8 → MA_check MODE_DIR1_to_DIR1
+| maIMM1_to_DIR1     : byte8 → byte8 → MA_check MODE_IMM1_to_DIR1
+| maIX0p_to_DIR1     : byte8 → MA_check MODE_IX0p_to_DIR1
+| maDIR1_to_IX0p     : byte8 → MA_check MODE_DIR1_to_IX0p
+| maINHA_and_IMM1    : byte8 → MA_check MODE_INHA_and_IMM1
+| maINHX_and_IMM1    : byte8 → MA_check MODE_INHX_and_IMM1
+| maIMM1_and_IMM1    : byte8 → byte8 → MA_check MODE_IMM1_and_IMM1
+| maDIR1_and_IMM1    : byte8 → byte8 → MA_check MODE_DIR1_and_IMM1
+| maIX0_and_IMM1     : byte8 → MA_check MODE_IX0_and_IMM1
+| maIX0p_and_IMM1    : byte8 → MA_check MODE_IX0p_and_IMM1
+| maIX1_and_IMM1     : byte8 → byte8 → MA_check MODE_IX1_and_IMM1
+| maIX1p_and_IMM1    : byte8 → byte8 → MA_check MODE_IX1p_and_IMM1
+| maSP1_and_IMM1     : byte8 → byte8 → MA_check MODE_SP1_and_IMM1
+| maDIRn             : ∀n.byte8 → MA_check (MODE_DIRn n)
+| maDIRn_and_IMM1    : ∀n.byte8 → byte8 → MA_check (MODE_DIRn_and_IMM1 n)
+| maTNY              : ∀e.MA_check (MODE_TNY e)
+| maSRT              : ∀t.MA_check (MODE_SRT 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 ≝
+λm:mcu_type.λi:instr_mode.λargs:MA_check i.
+ match args with
+  (* inherent: legale se nessun operando *) 
+  [ maINH    ⇒ nil ? 
+  | maINHA   ⇒ nil ? 
+  | maINHX   ⇒ nil ? 
+  | maINHH   ⇒ nil ?
+  (* inherent address: legale se nessun operando/1 byte/1 word *)
+  | maINHX0ADD ⇒ nil ?
+  | maINHX1ADD b ⇒ [ TByte m b ]
+  | maINHX2ADD w ⇒ [ TByte m (w16h w); TByte m (w16l w) ]    
+  (* _0/1/2: legale se nessun operando/1 byte/1 word *)
+  | maIMM1 b ⇒ [ TByte m b ]
+  | maIMM1EXT b ⇒ [ TByte m b ]
+  | maIMM2 w ⇒ [ TByte m (w16h w); TByte m (w16l w) ]
+  | maDIR1 b ⇒ [ TByte m b ]
+  | maDIR2 w ⇒ [ TByte m (w16h w); TByte m (w16l w) ]
+  | maIX0    ⇒ nil ?
+  | maIX1 b  ⇒ [ TByte m b ]
+  | maIX2 w  ⇒ [ TByte m (w16h w); TByte m (w16l w) ]
+  | maSP1 b  ⇒ [ TByte m b ]
+  | maSP2 w  ⇒ [ TByte m (w16h w); TByte m (w16l w) ]
+  (* movimento: legale se 2 operandi byte *)
+  | maDIR1_to_DIR1 b1 b2  ⇒ [ TByte m b1 ; TByte m b2 ]
+  | maIMM1_to_DIR1 b1 b2  ⇒ [ TByte m b1 ; TByte m b2 ]
+  | maIX0p_to_DIR1 b      ⇒ [ TByte m b]
+  | maDIR1_to_IX0p b      ⇒ [ TByte m b]
+  (* cbeq/dbnz: legale se 1/2 operandi byte *)
+  | maINHA_and_IMM1 b     ⇒ [ TByte m b]
+  | maINHX_and_IMM1 b     ⇒ [ TByte m b]
+  | maIMM1_and_IMM1 b1 b2 ⇒ [ TByte m b1 ; TByte m b2 ]
+  | maDIR1_and_IMM1 b1 b2 ⇒ [ TByte m b1 ; TByte m b2 ]
+  | maIX0_and_IMM1  b     ⇒ [ TByte m b]
+  | maIX0p_and_IMM1 b     ⇒ [ TByte m b]
+  | maIX1_and_IMM1  b1 b2 ⇒ [ TByte m b1 ; TByte m b2 ]
+  | maIX1p_and_IMM1 b1 b2 ⇒ [ TByte m b1 ; TByte m b2 ]
+  | maSP1_and_IMM1  b1 b2 ⇒ [ TByte m b1 ; TByte m b2 ]
+  (* DIRn: legale se 1 operando byte *)
+  | maDIRn _ b ⇒ [ TByte m b]
+  (* DIRn_and_IMM1: legale se 2 operandi byte *)
+  | maDIRn_and_IMM1 _ b1 b2 ⇒ [ TByte m b1 ; TByte m b2 ]
+  (* TNY: legale se nessun operando *)
+  | maTNY _ ⇒ nil ?
+  (* SRT: legale se nessun operando *)
+  | maSRT _ ⇒ nil ?
+  ].
+
+(* trasformatore finale: mcu+opcode+instr_mode+args → list (t_byte8 m) *)
+nlet rec bytes_of_pseudo_instr_mode_param_aux (m:mcu_type) (o:any_opcode m) (i:instr_mode) (p:MA_check 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_im i (snd4T … hd)) with
+   [ true ⇒ match thd4T … hd with 
+    [ Byte isab ⇒ 
+     Some ? ([ (TByte m isab) ]@(args_picker m i p))
+    | Word isaw ⇒
+     Some ? ([ (TByte m (w16h isaw)) ; (TByte m (w16l isaw)) ]@(args_picker m i p))
+    ]
+   | false ⇒ bytes_of_pseudo_instr_mode_param_aux m o i p tl ]].
+
+ndefinition bytes_of_pseudo_instr_mode_param ≝
+λm:mcu_type.λo:any_opcode m.λi:instr_mode.λp:MA_check i.
+bytes_of_pseudo_instr_mode_param_aux m o i p (opcode_table m).
+
+(* ****************************** *)
+(* APPROCCIO COMPILAZIONE AL VOLO *)
+(* ****************************** *)
+
+(* ausiliario di compile *)
+ndefinition defined_option ≝
+ λT:Type.λo:option T.
+  match o with
+   [ None ⇒ False
+   | Some _ ⇒ True
+   ].
+
+(* compila solo se l'intera istruzione+modalita'+argomenti ha riscontro nelle tabelle *)
+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 ?.defined_option ? res → ?
+ with
+  [ None ⇒ λp:defined_option ? (None ?).False_rect_Type0 ? p
+  | Some x ⇒ λp:defined_option ? (Some ? x).x
+  ].
+
+(* detipatore del compilato: (t_byte8 m) → byte8 *)
+nlet rec source_to_byte8_HC05_aux (p1:list (t_byte8 HC05)) (p2:list byte8) ≝
+ match p1 with
+  [ nil ⇒ p2
+  | cons hd tl ⇒ match hd with [ TByte b ⇒ source_to_byte8_HC05_aux tl (p2@[b]) ]
+  ].
+
+nlet rec source_to_byte8_HC08_aux (p1:list (t_byte8 HC08)) (p2:list byte8) ≝
+ match p1 with
+  [ nil ⇒ p2
+  | cons hd tl ⇒ match hd with [ TByte b ⇒ source_to_byte8_HC08_aux tl (p2@[b]) ]
+  ].
+
+nlet rec source_to_byte8_HCS08_aux (p1:list (t_byte8 HCS08)) (p2:list byte8) ≝
+ match p1 with
+  [ nil ⇒ p2
+  | cons hd tl ⇒ match hd with [ TByte b ⇒ source_to_byte8_HCS08_aux tl (p2@[b]) ]
+  ].
+
+nlet rec source_to_byte8_RS08_aux (p1:list (t_byte8 RS08)) (p2:list byte8) ≝
+ match p1 with
+  [ nil ⇒ p2
+  | cons hd tl ⇒ match hd with [ TByte b ⇒ source_to_byte8_RS08_aux tl (p2@[b]) ]
+  ].
+
+ndefinition source_to_byte8 ≝
+λm:mcu_type.
+ match m
+  return λm:mcu_type.list (t_byte8 m) → list byte8
+ with
+  [ HC05 ⇒ λl:list (t_byte8 HC05).source_to_byte8_HC05_aux l []
+  | HC08 ⇒ λl:list (t_byte8 HC08).source_to_byte8_HC08_aux l []
+  | HCS08 ⇒ λl:list (t_byte8 HCS08).source_to_byte8_HCS08_aux l []
+  | RS08 ⇒ λl:list (t_byte8 RS08).source_to_byte8_RS08_aux l []
+  ].