From 7b60729bcdcdd820ae78e32a68b59e56e11f1c02 Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Wed, 22 Jul 2009 16:46:04 +0000 Subject: [PATCH] Elimination principles are now processed in O(1) again --- .../contribs/ng_assembly/compiler/ast_type.ma | 10 +++++----- .../ng_assembly/freescale/aux_bases.ma | 8 ++++---- .../ng_assembly/freescale/memory_abs.ma | 4 ++-- .../ng_assembly/freescale/memory_struct.ma | 12 +++++------ .../ng_assembly/freescale/opcode_base.ma | 20 +++++++++---------- .../contribs/ng_assembly/freescale/status.ma | 12 +++++------ .../ng_assembly/freescale/translation.ma | 8 ++++---- .../contribs/ng_assembly/utility/ascii.ma | 4 ++-- 8 files changed, 39 insertions(+), 39 deletions(-) diff --git a/helm/software/matita/contribs/ng_assembly/compiler/ast_type.ma b/helm/software/matita/contribs/ng_assembly/compiler/ast_type.ma index 8f6de6f47..d972fe0ba 100755 --- a/helm/software/matita/contribs/ng_assembly/compiler/ast_type.ma +++ b/helm/software/matita/contribs/ng_assembly/compiler/ast_type.ma @@ -33,7 +33,7 @@ ninductive ast_base_type : Type ≝ | AST_BASE_TYPE_WORD16: ast_base_type | AST_BASE_TYPE_WORD32: ast_base_type. -ndefinition ast_base_type_ind +(*ndefinition ast_base_type_ind : ΠP:ast_base_type → Prop.P AST_BASE_TYPE_BYTE8 → P AST_BASE_TYPE_WORD16 → P AST_BASE_TYPE_WORD32 → Πa:ast_base_type.P a ≝ λP:ast_base_type → Prop.λp:P AST_BASE_TYPE_BYTE8.λp1:P AST_BASE_TYPE_WORD16.λp2:P AST_BASE_TYPE_WORD32. @@ -53,7 +53,7 @@ ndefinition ast_base_type_rect λP:ast_base_type → Type.λp:P AST_BASE_TYPE_BYTE8.λp1:P AST_BASE_TYPE_WORD16.λp2:P AST_BASE_TYPE_WORD32. λa:ast_base_type. match a with [ AST_BASE_TYPE_BYTE8 ⇒ p | AST_BASE_TYPE_WORD16 ⇒ p1 | AST_BASE_TYPE_WORD32 ⇒ p2 ]. - +*) ninductive ast_type : Type ≝ AST_TYPE_BASE: ast_base_type → ast_type | AST_TYPE_ARRAY: ast_type → nat → ast_type @@ -69,7 +69,7 @@ nlet rec ast_type_ind_aux (P:ast_type → Prop) | ne_cons h t ⇒ f1 h t (f2 h) (ast_type_ind_aux P f f1 f2 t) ]. -nlet rec ast_type_ind (P:ast_type → Prop) +(*nlet rec ast_type_ind (P:ast_type → Prop) (f:Πb.P (AST_TYPE_BASE b)) (f1:Πt,n.P t → P (AST_TYPE_ARRAY t n)) (f2:Πt.P t → P (AST_TYPE_STRUCT (ne_nil ? t))) @@ -84,7 +84,7 @@ nlet rec ast_type_ind (P:ast_type → Prop) ] ]. -nlet rec ast_type_rec_aux (P:ast_type → Set) +nlet rec ast_type_rec_aux (P:ast_type → Type[0]) (f:Πt.P t → P (AST_TYPE_STRUCT (ne_nil ? t))) (f1:Πh,t.P h → P (AST_TYPE_STRUCT t) → P (AST_TYPE_STRUCT (ne_cons ? h t))) (f2:Πt.P t) @@ -133,7 +133,7 @@ nlet rec ast_type_rect (P:ast_type → Type) | ne_cons h t ⇒ f3 h t (ast_type_rect P f f1 f2 f3 h) (ast_type_rect_aux P f2 f3 (ast_type_rect P f f1 f2 f3) t) ] ]. - +*) ndefinition eq_ast_base_type ≝ λt1,t2:ast_base_type.match t1 with [ AST_BASE_TYPE_BYTE8 ⇒ match t2 with diff --git a/helm/software/matita/contribs/ng_assembly/freescale/aux_bases.ma b/helm/software/matita/contribs/ng_assembly/freescale/aux_bases.ma index a4707a5d5..58898142d 100755 --- a/helm/software/matita/contribs/ng_assembly/freescale/aux_bases.ma +++ b/helm/software/matita/contribs/ng_assembly/freescale/aux_bases.ma @@ -37,7 +37,7 @@ ninductive oct : Type ≝ | o6: oct | o7: oct. -ndefinition oct_ind : +(*ndefinition oct_ind : ΠP:oct → Prop.P o0 → P o1 → P o2 → P o3 → P o4 → P o5 → P o6 → P o7 → Πn:oct.P n ≝ λP:oct → Prop. λp:P o0.λp1:P o1.λp2:P o2.λp3:P o3.λp4:P o4.λp5:P o5.λp6:P o6.λp7:P o7.λn:oct. @@ -57,7 +57,7 @@ ndefinition oct_rect : λp:P o0.λp1:P o1.λp2:P o2.λp3:P o3.λp4:P o4.λp5:P o5.λp6:P o6.λp7:P o7.λn:oct. match n with [ o0 ⇒ p | o1 ⇒ p1 | o2 ⇒ p2 | o3 ⇒ p3 | o4 ⇒ p4 | o5 ⇒ p5 | o6 ⇒ p6 | o7 ⇒ p7 ]. - +*) (* operatore = *) ndefinition eq_oct ≝ λn1,n2:oct. @@ -136,7 +136,7 @@ ninductive bitrigesim : Type ≝ | t1E: bitrigesim | t1F: bitrigesim. -ndefinition bitrigesim_ind : +(*ndefinition bitrigesim_ind : ΠP:bitrigesim → Prop.P t00 → P t01 → P t02 → P t03 → P t04 → P t05 → P t06 → P t07 → P t08 → P t09 → P t0A → P t0B → P t0C → P t0D → P t0E → P t0F → P t10 → P t11 → P t12 → P t13 → P t14 → P t15 → P t16 → P t17 → @@ -183,7 +183,7 @@ ndefinition bitrigesim_rect : | t08 ⇒ p8 | t09 ⇒ p9 | t0A ⇒ p10 | t0B ⇒ p11 | t0C ⇒ p12 | t0D ⇒ p13 | t0E ⇒ p14 | t0F ⇒ p15 | t10 ⇒ p16 | t11 ⇒ p17 | t12 ⇒ p18 | t13 ⇒ p19 | t14 ⇒ p20 | t15 ⇒ p21 | t16 ⇒ p22 | t17 ⇒ p23 | t18 ⇒ p24 | t19 ⇒ p25 | t1A ⇒ p26 | t1B ⇒ p27 | t1C ⇒ p28 | t1D ⇒ p29 | t1E ⇒ p30 | t1F ⇒ p31 ]. - +*) (* operatore = *) ndefinition eq_bitrig ≝ λt1,t2:bitrigesim. diff --git a/helm/software/matita/contribs/ng_assembly/freescale/memory_abs.ma b/helm/software/matita/contribs/ng_assembly/freescale/memory_abs.ma index a93e38947..8e9f08c05 100755 --- a/helm/software/matita/contribs/ng_assembly/freescale/memory_abs.ma +++ b/helm/software/matita/contribs/ng_assembly/freescale/memory_abs.ma @@ -34,7 +34,7 @@ ninductive memory_impl : Type ≝ | MEM_TREE: memory_impl | MEM_BITS: memory_impl. -ndefinition memory_impl_ind : ΠP:memory_impl → Prop.P MEM_FUNC → P MEM_TREE → P MEM_BITS → Πm:memory_impl.P m ≝ +(*ndefinition memory_impl_ind : ΠP:memory_impl → Prop.P MEM_FUNC → P MEM_TREE → P MEM_BITS → Πm:memory_impl.P m ≝ λP:memory_impl → Prop.λp:P MEM_FUNC.λp1:P MEM_TREE.λp2:P MEM_BITS.λm:memory_impl. match m with [ MEM_FUNC ⇒ p | MEM_TREE ⇒ p1 | MEM_BITS ⇒ p2 ]. @@ -44,7 +44,7 @@ ndefinition memory_impl_rec : ΠP:memory_impl → Set.P MEM_FUNC → P MEM_TREE ndefinition memory_impl_rect : ΠP:memory_impl → Type.P MEM_FUNC → P MEM_TREE → P MEM_BITS → Πm:memory_impl.P m ≝ λP:memory_impl → Type.λp:P MEM_FUNC.λp1:P MEM_TREE.λp2:P MEM_BITS.λm:memory_impl. - match m with [ MEM_FUNC ⇒ p | MEM_TREE ⇒ p1 | MEM_BITS ⇒ p2 ]. + match m with [ MEM_FUNC ⇒ p | MEM_TREE ⇒ p1 | MEM_BITS ⇒ p2 ].*) (* ausiliario per il tipo della memoria *) ndefinition aux_mem_type ≝ diff --git a/helm/software/matita/contribs/ng_assembly/freescale/memory_struct.ma b/helm/software/matita/contribs/ng_assembly/freescale/memory_struct.ma index d256fefd8..0ba7735af 100755 --- a/helm/software/matita/contribs/ng_assembly/freescale/memory_struct.ma +++ b/helm/software/matita/contribs/ng_assembly/freescale/memory_struct.ma @@ -33,7 +33,7 @@ ninductive memory_type : Type ≝ | MEM_READ_WRITE: memory_type | MEM_OUT_OF_BOUND: memory_type. -ndefinition memory_type_ind : ΠP:memory_type → Prop.P MEM_READ_ONLY → P MEM_READ_WRITE → P MEM_OUT_OF_BOUND → Πm:memory_type.P m ≝ +(*ndefinition memory_type_ind : ΠP:memory_type → Prop.P MEM_READ_ONLY → P MEM_READ_WRITE → P MEM_OUT_OF_BOUND → Πm:memory_type.P m ≝ λP:memory_type → Prop.λp:P MEM_READ_ONLY.λp1:P MEM_READ_WRITE.λp2:P MEM_OUT_OF_BOUND.λm:memory_type. match m with [ MEM_READ_ONLY ⇒ p | MEM_READ_WRITE ⇒ p1 | MEM_OUT_OF_BOUND ⇒ p2 ]. @@ -44,7 +44,7 @@ ndefinition memory_type_rec : ΠP:memory_type → Set.P MEM_READ_ONLY → P MEM_ ndefinition memory_type_rect : ΠP:memory_type → Type.P MEM_READ_ONLY → P MEM_READ_WRITE → P MEM_OUT_OF_BOUND → Πm:memory_type.P m ≝ λP:memory_type → Type.λp:P MEM_READ_ONLY.λp1:P MEM_READ_WRITE.λp2:P MEM_OUT_OF_BOUND.λm:memory_type. match m with [ MEM_READ_ONLY ⇒ p | MEM_READ_WRITE ⇒ p1 | MEM_OUT_OF_BOUND ⇒ p2 ]. - +*) (* **************** *) (* TIPO ARRAY DA 16 *) (* **************** *) @@ -55,7 +55,7 @@ array_16T : T → T → T → T → T → T → T → T → T → T → T → T → T → T → T → T → Array16T T. -ndefinition Array16T_ind +(*ndefinition Array16T_ind : ΠT:Type.ΠP:Array16T T → Prop. (Πt,t1,t2,t3,t4,t5,t6,t7,t8,t9,t10,t11,t12,t13,t14,t15.P (array_16T T t t1 t2 t3 t4 t5 t6 t7 t8 t9 t10 t11 t12 t13 t14 t15)) → Πa:Array16T T.P a ≝ λT:Type.λP:Array16T T → Prop. @@ -75,7 +75,7 @@ ndefinition Array16T_rect λT:Type.λP:Array16T T → Type. λf:Πt,t1,t2,t3,t4,t5,t6,t7,t8,t9,t10,t11,t12,t13,t14,t15.P (array_16T T t t1 t2 t3 t4 t5 t6 t7 t8 t9 t10 t11 t12 t13 t14 t15).λa:Array16T T. match a with [ array_16T t t1 t2 t3 t4 t5 t6 t7 t8 t9 t10 t11 t12 t13 t14 t15 ⇒ f t t1 t2 t3 t4 t5 t6 t7 t8 t9 t10 t11 t12 t13 t14 t15 ]. - +*) (* abbiamo gia' gli esadecimali come tipo induttivo quindi: *) (* posso definire un getter a matrice sull'array *) ndefinition getn_array16T ≝ @@ -337,7 +337,7 @@ ninductive Array8T (T:Type) : Type ≝ array_8T : T → T → T → T → T → T → T → T → Array8T T. -ndefinition Array8T_ind +(*ndefinition Array8T_ind : ΠT:Type.ΠP:Array8T T → Prop. (Πt,t1,t2,t3,t4,t5,t6,t7.P (array_8T T t t1 t2 t3 t4 t5 t6 t7)) → Πa:Array8T T.P a ≝ λT:Type.λP:Array8T T → Prop. @@ -357,7 +357,7 @@ ndefinition Array8T_rect λT:Type.λP:Array8T T → Type. λf:Πt,t1,t2,t3,t4,t5,t6,t7.P (array_8T T t t1 t2 t3 t4 t5 t6 t7).λa:Array8T T. match a with [ array_8T t t1 t2 t3 t4 t5 t6 t7 ⇒ f t t1 t2 t3 t4 t5 t6 t7 ]. - +*) (* abbiamo gia' gli ottali come tipo induttivo quindi: *) (* posso definire un getter a matrice sull'array *) ndefinition getn_array8T ≝ diff --git a/helm/software/matita/contribs/ng_assembly/freescale/opcode_base.ma b/helm/software/matita/contribs/ng_assembly/freescale/opcode_base.ma index 85879bf4a..41de61f29 100755 --- a/helm/software/matita/contribs/ng_assembly/freescale/opcode_base.ma +++ b/helm/software/matita/contribs/ng_assembly/freescale/opcode_base.ma @@ -35,7 +35,7 @@ ninductive mcu_type: Type ≝ | HCS08 : mcu_type | RS08 : mcu_type. -ndefinition mcu_type_ind : ΠP:mcu_type → Prop.P HC05 → P HC08 → P HCS08 → P RS08 → Πm:mcu_type.P m ≝ +(*ndefinition mcu_type_ind : ΠP:mcu_type → Prop.P HC05 → P HC08 → P HCS08 → P RS08 → Πm:mcu_type.P m ≝ λP:mcu_type → Prop.λp:P HC05.λp1:P HC08.λp2:P HCS08.λp3:P RS08.λm:mcu_type. match m with [ HC05 ⇒ p | HC08 ⇒ p1 | HCS08 ⇒ p2 | RS08 ⇒ p3 ]. @@ -45,7 +45,7 @@ ndefinition mcu_type_rec : ΠP:mcu_type → Set.P HC05 → P HC08 → P HCS08 ndefinition mcu_type_rect : ΠP:mcu_type → Type.P HC05 → P HC08 → P HCS08 → P RS08 → Πm:mcu_type.P m ≝ λP:mcu_type → Type.λp:P HC05.λp1:P HC08.λp2:P HCS08.λp3:P RS08.λm:mcu_type. - match m with [ HC05 ⇒ p | HC08 ⇒ p1 | HCS08 ⇒ p2 | RS08 ⇒ p3 ]. + match m with [ HC05 ⇒ p | HC08 ⇒ p1 | HCS08 ⇒ p2 | RS08 ⇒ p3 ].*) ndefinition eq_mcutype ≝ λm1,m2:mcu_type. @@ -136,7 +136,7 @@ ninductive instr_mode: Type ≝ | MODE_SRT : bitrigesim → instr_mode . -ndefinition instr_mode_ind +(*ndefinition instr_mode_ind : ΠP:instr_mode → Prop. P MODE_INH → P MODE_INHA → P MODE_INHX → P MODE_INHH → P MODE_INHX0ADD → P MODE_INHX1ADD → P MODE_INHX2ADD → P MODE_IMM1 → P MODE_IMM1EXT → P MODE_IMM2 → P MODE_DIR1 → P MODE_DIR2 → @@ -227,7 +227,7 @@ ndefinition instr_mode_rect | MODE_DIR1_and_IMM1 ⇒ p24 | MODE_IX0_and_IMM1 ⇒ p25 | MODE_IX0p_and_IMM1 ⇒ p26 | MODE_IX1_and_IMM1 ⇒ p27 | MODE_IX1p_and_IMM1 ⇒ p28 | MODE_SP1_and_IMM1 ⇒ p29 | MODE_DIRn (d:oct) ⇒ f d | MODE_DIRn_and_IMM1 (d:oct) ⇒ f1 d | MODE_TNY (d:exadecim) ⇒ f2 d - | MODE_SRT (d:bitrigesim) ⇒ f3 d ]. + | MODE_SRT (d:bitrigesim) ⇒ f3 d ].*) ndefinition eq_instrmode ≝ λi1,i2:instr_mode. @@ -363,7 +363,7 @@ ninductive opcode: Type ≝ | WAIT : opcode (* !!wait mode!! *) . -ndefinition opcode_ind +(*ndefinition opcode_ind : ΠP:opcode → Prop. P ADC → P ADD → P AIS → P AIX → P AND → P ASL → P ASR → P BCC → P BCLRn → P BCS → P BEQ → P BGE → P BGND → P BGT → P BHCC → P BHCS → P BHI → P BIH → P BIL → P BIT → P BLE → P BLS → @@ -472,7 +472,7 @@ ndefinition opcode_rect | PULH ⇒ p65 | PULX ⇒ p66 | ROL ⇒ p67 | ROR ⇒ p68 | RSP ⇒ p69 | RTI ⇒ p70 | RTS ⇒ p71 | SBC ⇒ p72 | SEC ⇒ p73 | SEI ⇒ p74 | SHA ⇒ p75 | SLA ⇒ p76 | STA ⇒ p77 | STHX ⇒ p78 | STOP ⇒ p79 | STX ⇒ p80 | SUB ⇒ p81 | SWI ⇒ p82 | TAP ⇒ p83 | TAX ⇒ p84 | TPA ⇒ p85 | TST ⇒ p86 | TSX ⇒ p87 | TXA ⇒ p88 - | TXS ⇒ p89 | WAIT ⇒ p90 ]. + | TXS ⇒ p89 | WAIT ⇒ p90 ].*) ndefinition eq_op ≝ λop1,op2:opcode. @@ -529,7 +529,7 @@ ndefinition eq_op ≝ ninductive any_opcode (m:mcu_type) : Type ≝ anyOP : opcode → any_opcode m. -ndefinition any_opcode_ind +(*ndefinition any_opcode_ind : Πm:mcu_type.ΠP:any_opcode m → Prop.(Πo:opcode.P (anyOP m o)) → Πa:any_opcode m.P a ≝ λm:mcu_type.λP:any_opcode m → Prop.λf:Πo:opcode.P (anyOP m o).λa:any_opcode m. match a with [ anyOP (o:opcode) ⇒ f o ]. @@ -542,7 +542,7 @@ ndefinition any_opcode_rec ndefinition any_opcode_rect : Πm:mcu_type.ΠP:any_opcode m → Type.(Πo:opcode.P (anyOP m o)) → Πa:any_opcode m.P a ≝ λm:mcu_type.λP:any_opcode m → Type.λf:Πo:opcode.P (anyOP m o).λa:any_opcode m. - match a with [ anyOP (o:opcode) ⇒ f o ]. + match a with [ anyOP (o:opcode) ⇒ f o ].*) ndefinition eq_anyop ≝ λm:mcu_type.λop1,op2:any_opcode m. @@ -555,7 +555,7 @@ ninductive byte8_or_word16 : Type ≝ Byte: byte8 → byte8_or_word16 | Word: word16 → byte8_or_word16. -ndefinition byte8_or_word16_ind +(*ndefinition byte8_or_word16_ind : ΠP:byte8_or_word16 → Prop.(Πb:byte8.P (Byte b)) → (Πw:word16.P (Word w)) → Πb:byte8_or_word16.P b ≝ λP:byte8_or_word16 → Prop.λf:Πb:byte8.P (Byte b).λf1:Πw:word16.P (Word w).λb:byte8_or_word16. match b with [ Byte (b1:byte8) ⇒ f b1 | Word (w:word16) ⇒ f1 w ]. @@ -568,7 +568,7 @@ ndefinition byte8_or_word16_rec ndefinition byte8_or_word16_rect : ΠP:byte8_or_word16 → Type.(Πb:byte8.P (Byte b)) → (Πw:word16.P (Word w)) → Πb:byte8_or_word16.P b ≝ λP:byte8_or_word16 → Type.λf:Πb:byte8.P (Byte b).λf1:Πw:word16.P (Word w).λb:byte8_or_word16. - match b with [ Byte (b1:byte8) ⇒ f b1 | Word (w:word16) ⇒ f1 w ]. + match b with [ Byte (b1:byte8) ⇒ f b1 | Word (w:word16) ⇒ f1 w ].*) ndefinition eq_b8w16 ≝ λbw1,bw2:byte8_or_word16. diff --git a/helm/software/matita/contribs/ng_assembly/freescale/status.ma b/helm/software/matita/contribs/ng_assembly/freescale/status.ma index add19cb99..a92c4a6e0 100755 --- a/helm/software/matita/contribs/ng_assembly/freescale/status.ma +++ b/helm/software/matita/contribs/ng_assembly/freescale/status.ma @@ -64,7 +64,7 @@ nrecord alu_HC05: Type ≝ irq_flag_HC05 : bool }. -ndefinition alu_HC05_ind : +(*ndefinition alu_HC05_ind : ΠP:alu_HC05 → Prop.(Πb,b1,w,w1,w2,w3,w4,b2,b3,b4,b5,b6,b7.P (mk_alu_HC05 b b1 w w1 w2 w3 w4 b2 b3 b4 b5 b6 b7)) → Πa:alu_HC05.P a ≝ λP:alu_HC05 → Prop.λf:Πb,b1,w,w1,w2,w3,w4,b2,b3,b4,b5,b6,b7.P (mk_alu_HC05 b b1 w w1 w2 w3 w4 b2 b3 b4 b5 b6 b7).λa:alu_HC05. match a with [ mk_alu_HC05 b b1 w w1 w2 w3 w4 b2 b3 b4 b5 b6 b7 ⇒ f b b1 w w1 w2 w3 w4 b2 b3 b4 b5 b6 b7 ]. @@ -92,7 +92,7 @@ ndefinition n_flag_HC05 ≝ λalu.match alu with [ mk_alu_HC05 _ _ _ _ _ _ _ _ ndefinition z_flag_HC05 ≝ λalu.match alu with [ mk_alu_HC05 _ _ _ _ _ _ _ _ _ _ x _ _ ⇒ x ]. ndefinition c_flag_HC05 ≝ λalu.match alu with [ mk_alu_HC05 _ _ _ _ _ _ _ _ _ _ _ x _ ⇒ x ]. ndefinition irq_flag_HC05 ≝ λalu.match alu with [ mk_alu_HC05 _ _ _ _ _ _ _ _ _ _ _ _ x ⇒ x ]. - +*) notation "{hvbox('A_Reg' ≝ acclow ; break 'X_Reg' ≝ indxlow ; break 'Sp_Reg' ≝ sp ; break 'Sp_Mask' ≝ spm ; break 'Sp_Fix' ≝ spf ; break 'Pc_Reg' ≝ pc ; break 'Pc_Mask' ≝ pcm ; break 'H_Flag' ≝ hfl ; break 'I_Flag' ≝ ifl ; break 'N_Flag' ≝ nfl ; break 'Z_Flag' ≝ zfl ; break 'C_Flag' ≝ cfl ; break 'IRQ_Flag' ≝ irqfl)}" non associative with precedence 80 for @{ 'mk_alu_HC05 $acclow $indxlow $sp $spm $spf $pc $pcm $hfl $ifl $nfl $zfl $cfl $irqfl }. @@ -130,7 +130,7 @@ nrecord alu_HC08: Type ≝ irq_flag_HC08 : bool }. -ndefinition alu_HC08_ind : +(*ndefinition alu_HC08_ind : ΠP:alu_HC08 → Prop.(Πb,b1,b2,w,w1,b3,b4,b5,b6,b7,b8,b9.P (mk_alu_HC08 b b1 b2 w w1 b3 b4 b5 b6 b7 b8 b9)) → Πa:alu_HC08.P a ≝ λP:alu_HC08 → Prop.λf:Πb,b1,b2,w,w1,b3,b4,b5,b6,b7,b8,b9.P (mk_alu_HC08 b b1 b2 w w1 b3 b4 b5 b6 b7 b8 b9).λa:alu_HC08. match a with [ mk_alu_HC08 b b1 b2 w w1 b3 b4 b5 b6 b7 b8 b9 ⇒ f b b1 b2 w w1 b3 b4 b5 b6 b7 b8 b9 ]. @@ -157,7 +157,7 @@ ndefinition n_flag_HC08 ≝ λalu.match alu with [ mk_alu_HC08 _ _ _ _ _ _ _ _ ndefinition z_flag_HC08 ≝ λalu.match alu with [ mk_alu_HC08 _ _ _ _ _ _ _ _ _ x _ _ ⇒ x ]. ndefinition c_flag_HC08 ≝ λalu.match alu with [ mk_alu_HC08 _ _ _ _ _ _ _ _ _ _ x _ ⇒ x ]. ndefinition irq_flag_HC08 ≝ λalu.match alu with [ mk_alu_HC08 _ _ _ _ _ _ _ _ _ _ _ x ⇒ x ]. - +*) notation "{hvbox('A_Reg' ≝ acclow ; break 'X_Reg' ≝ indxlow ; break 'H_Reg' ≝ indxhigh ; break 'Sp_Reg' ≝ sp ; break 'Pc_Reg' ≝ pc ; break 'V_Flag' ≝ vfl ; break 'H_Flag' ≝ hfl ; break 'I_Flag' ≝ ifl ; break 'N_Flag' ≝ nfl ; break 'Z_Flag' ≝ zfl ; break 'C_Flag' ≝ cfl ; break 'IRQ_Flag' ≝ irqfl)}" non associative with precedence 80 for @{ 'mk_alu_HC08 $acclow $indxlow $indxhigh $sp $pc $vfl $hfl $ifl $nfl $zfl $cfl $irqfl }. @@ -200,7 +200,7 @@ nrecord alu_RS08: Type ≝ c_flag_RS08 : bool }. -ndefinition alu_RS08_ind : +(*ndefinition alu_RS08_ind : ΠP:alu_RS08 → Prop.(Πb,w,w1,w2,b1,b2,b3,b4.P (mk_alu_RS08 b w w1 w2 b1 b2 b3 b4)) → Πa:alu_RS08.P a ≝ λP:alu_RS08 → Prop.λf:Πb,w,w1,w2,b1,b2,b3,b4.P (mk_alu_RS08 b w w1 w2 b1 b2 b3 b4).λa:alu_RS08. match a with [ mk_alu_RS08 b w w1 w2 b1 b2 b3 b4 ⇒ f b w w1 w2 b1 b2 b3 b4 ]. @@ -223,7 +223,7 @@ ndefinition x_map_RS08 ≝ λalu.match alu with [ mk_alu_RS08 _ _ _ _ x _ _ _ ndefinition ps_map_RS08 ≝ λalu.match alu with [ mk_alu_RS08 _ _ _ _ _ x _ _ ⇒ x ]. ndefinition z_flag_RS08 ≝ λalu.match alu with [ mk_alu_RS08 _ _ _ _ _ _ x _ ⇒ x ]. ndefinition c_flag_RS08 ≝ λalu.match alu with [ mk_alu_RS08 _ _ _ _ _ _ _ x ⇒ x ]. - +*) notation "{hvbox('A_Reg' ≝ acclow ; break 'Pc_Reg' ≝ pc ; break 'Pc_Mask' ≝ pcm ; break 'Spc_Reg' ≝ spc ; break 'X_Map' ≝ xm ; break 'Ps_Map' ≝ psm ; break 'Z_Flag' ≝ zfl ; break 'C_Flag' ≝ cfl)}" non associative with precedence 80 for @{ 'mk_alu_RS08 $acclow $pc $pcm $spc $xm $psm $zfl $cfl }. diff --git a/helm/software/matita/contribs/ng_assembly/freescale/translation.ma b/helm/software/matita/contribs/ng_assembly/freescale/translation.ma index 7cb39cd91..8ef0d5234 100755 --- a/helm/software/matita/contribs/ng_assembly/freescale/translation.ma +++ b/helm/software/matita/contribs/ng_assembly/freescale/translation.ma @@ -76,7 +76,7 @@ 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 +(*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 ]. @@ -89,7 +89,7 @@ ndefinition t_byte8_rec 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 ]. + 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; @@ -173,7 +173,7 @@ ndefinition instr_mode_ind | 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 +(*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)) → @@ -244,7 +244,7 @@ ndefinition instr_mode_rect | 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 ≝ diff --git a/helm/software/matita/contribs/ng_assembly/utility/ascii.ma b/helm/software/matita/contribs/ng_assembly/utility/ascii.ma index 35894f570..38d2e7f53 100755 --- a/helm/software/matita/contribs/ng_assembly/utility/ascii.ma +++ b/helm/software/matita/contribs/ng_assembly/utility/ascii.ma @@ -98,7 +98,7 @@ ninductive ascii : Type ≝ | ch_y: ascii | ch_z: ascii. -ndefinition ascii_ind +(*ndefinition ascii_ind : ΠP:ascii → Prop. P ch_0 → P ch_1 → P ch_2 → P ch_3 → P ch_4 → P ch_5 → P ch_6 → P ch_7 → P ch_8 → P ch_9 → P ch__ → P ch_A → P ch_B → P ch_C → P ch_D → P ch_E → P ch_F → P ch_G → P ch_H → P ch_I → P ch_J → P ch_K → @@ -149,7 +149,7 @@ ndefinition ascii_rect | ch_d ⇒ p40 | ch_e ⇒ p41 | ch_f ⇒ p42 | ch_g ⇒ p43 | ch_h ⇒ p44 | ch_i ⇒ p45 | ch_j ⇒ p46 | ch_k ⇒ p47 | ch_l ⇒ p48 | ch_m ⇒ p49 | ch_n ⇒ p50 | ch_o ⇒ p51 | ch_p ⇒ p52 | ch_q ⇒ p53 | ch_r ⇒ p54 | ch_s ⇒ p55 | ch_t ⇒ p56 | ch_u ⇒ p57 | ch_v ⇒ p58 | ch_w ⇒ p59 | ch_x ⇒ p60 | ch_y ⇒ p61 | ch_z ⇒ p62 ]. - +*) (* confronto fra ascii *) ndefinition eq_ascii ≝ λc,c':ascii.match c with -- 2.39.2