+++ /dev/null
-(**************************************************************************)
-(* ___ *)
-(* ||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 "freescale/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_instrmode 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 []
- ].
projects / helm.git / blobdiff