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=94d254bf2fe709a1fddf082bc63200ba8e154c3c;hb=03ebff6c48be2253ad32b3b57f4e1d2b02acda86;hp=8ef0d523407dd0ca5c889ec7f9f4e4f43eee474f;hpb=dc74ed7c4af1aa9b90fc5d2f0a86bd7825696e71;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 index 8ef0d5234..94d254bf2 100755 --- a/helm/software/matita/contribs/ng_assembly/freescale/translation.ma +++ b/helm/software/matita/contribs/ng_assembly/freescale/translation.ma @@ -76,21 +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 ]); @@ -137,114 +122,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 ≝ @@ -329,10 +206,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 *)