Changeset 262 for Deliverables/D4.1
 Timestamp:
 Nov 23, 2010, 4:39:31 PM (10 years ago)
 Location:
 Deliverables/D4.1/Matita
 Files:

 3 edited
Legend:
 Unmodified
 Added
 Removed

Deliverables/D4.1/Matita/ASM.ma
r260 r262 5 5 include "BitVectorTrie.ma". 6 6 7 ninductive all_types : Type[0] ≝8 reg: all_types  direct: all_types  indirect:all_types  data:all_types9  acc: all_types  rel: all_types.10 11 7 interpretation "Cartesian" 'product A B = (Cartesian A B). 12 interpretation "Either" 'plus A B = (Either A B). 8 notation "hvbox(a break ⊎ b)" 9 left associative with precedence 50 10 for @{ 'disjoint_union $a $b }. 11 interpretation "Either" 'disjoint_union A B = (Either A B). 12 interpretation "Bool" 'or a b = (inclusive_disjunction a b). 13 13 14 14 ninductive addressing_mode: Type[0] ≝ 15 15 DIRECT: Byte → addressing_mode 16 16  INDIRECT: Bit → addressing_mode 17  EXT INDIRECT: Bit → addressing_mode17  EXT_INDIRECT: Bit → addressing_mode 18 18  REGISTER: Bit → Bit → Bit → addressing_mode 19  ACC UMULATORA: addressing_mode20  ACC UMULATORB: addressing_mode21  DP OINTER: addressing_mode19  ACC_A: addressing_mode 20  ACC_B: addressing_mode 21  DPTR: addressing_mode 22 22  DATA: Byte → addressing_mode 23 23  DATA16: Word → addressing_mode 24  ACC UMULATORDPOINTER: addressing_mode25  ACC UMULATORPROGRAMCOUNTER: addressing_mode26  EXT ERNALINDIRECTDPOINTER: addressing_mode27  INDIRECT DPOINTER: addressing_mode24  ACC_DPTR: addressing_mode 25  ACC_PC: addressing_mode 26  EXT_INDIRECT_DPTR: addressing_mode 27  INDIRECT_DPTR: addressing_mode 28 28  CARRY: addressing_mode 29  BIT : Bit → addressing_mode30  COMPLEMENTBITADDRESS: Bit → addressing_mode29  BIT_ADDR: Bit → addressing_mode 30  N_BIT_ADDR: Bit → addressing_mode 31 31  RELATIVE: Byte → addressing_mode 32  ADDRESS11: Word11 → addressing_mode 33  ADDRESS16: Word → addressing_mode. 32  ADDR11: Word11 → addressing_mode 33  ADDR16: Word → addressing_mode. 34 35 ninductive addressing_mode_tag : Type[0] ≝ 36 direct: addressing_mode_tag 37  indirect: addressing_mode_tag 38  ext_indirect: addressing_mode_tag 39  register: addressing_mode_tag 40  acc_a: addressing_mode_tag 41  acc_b: addressing_mode_tag 42  dptr: addressing_mode_tag 43  data: addressing_mode_tag 44  data16: addressing_mode_tag 45  acc_dptr: addressing_mode_tag 46  acc_pc: addressing_mode_tag 47  ext_indirect_dptr: addressing_mode_tag 48  indirect_dptr: addressing_mode_tag 49  carry: addressing_mode_tag 50  bit_addr: addressing_mode_tag 51  n_bit_addr: addressing_mode_tag 52  relative: addressing_mode_tag 53  addr11: addressing_mode_tag 54  addr16: addressing_mode_tag. 34 55 35 56 (* to avoid expansion... *) 36 nlet rec is_a (d:a ll_types) (A:addressing_mode) on d ≝57 nlet rec is_a (d:addressing_mode_tag) (A:addressing_mode) on d ≝ 37 58 match d with 38 [ reg ⇒ match A with [ REGISTER _ _ _ ⇒ true  _ ⇒ false ] 59 [ direct ⇒ match A with [ DIRECT _ ⇒ true  _ ⇒ false ] 60  indirect ⇒ match A with [ INDIRECT _ ⇒ true  _ ⇒ false ] 61  ext_indirect ⇒ match A with [ EXT_INDIRECT _ ⇒ true  _ ⇒ false ] 62  register ⇒ match A with [ REGISTER _ _ _ ⇒ true  _ ⇒ false ] 63  acc_a ⇒ match A with [ ACC_A ⇒ true  _ ⇒ false ] 64  acc_b ⇒ match A with [ ACC_B ⇒ true  _ ⇒ false ] 65  dptr ⇒ match A with [ DPTR ⇒ true  _ ⇒ false ] 39 66  data ⇒ match A with [ DATA _ ⇒ true  _ ⇒ false ] 40  rel ⇒ match A with [ RELATIVE _ ⇒ true  _ ⇒ false ] 41  acc ⇒ match A with [ ACCUMULATORA ⇒ true  _ ⇒ false ] 42  direct ⇒ match A with [ DIRECT _ ⇒ true  _ ⇒ false ] 43  indirect ⇒ match A with [ INDIRECT _ ⇒ true  _ ⇒ false ]]. 44 45 interpretation "Bool" 'or a b = (inclusive_disjunction a b). 46 47 nlet rec is_in n (l: Vector all_types (S n)) (A:addressing_mode) on l : Bool ≝ 48 match l return λm.λ_:Vector all_types m .∀K:m=S n.Bool with 67  data16 ⇒ match A with [ DATA16 _ ⇒ true  _ ⇒ false ] 68  acc_dptr ⇒ match A with [ ACC_DPTR ⇒ true  _ ⇒ false ] 69  acc_pc ⇒ match A with [ ACC_PC ⇒ true  _ ⇒ false ] 70  ext_indirect_dptr ⇒ match A with [ EXT_INDIRECT_DPTR ⇒ true  _ ⇒ false ] 71  indirect_dptr ⇒ match A with [ INDIRECT_DPTR ⇒ true  _ ⇒ false ] 72  carry ⇒ match A with [ CARRY ⇒ true  _ ⇒ false ] 73  bit_addr ⇒ match A with [ BIT_ADDR _ ⇒ true  _ ⇒ false ] 74  n_bit_addr ⇒ match A with [ N_BIT_ADDR _ ⇒ true  _ ⇒ false ] 75  relative ⇒ match A with [ RELATIVE _ ⇒ true  _ ⇒ false ] 76  addr11 ⇒ match A with [ ADDR11 _ ⇒ true  _ ⇒ false ] 77  addr16 ⇒ match A with [ ADDR16 _ ⇒ true  _ ⇒ false ]]. 78 79 nlet rec is_in n (l: Vector addressing_mode_tag (S n)) (A:addressing_mode) on l : Bool ≝ 80 match l return λm.λ_:Vector addressing_mode_tag m .∀K:m=S n.Bool with 49 81 [ Empty ⇒ λK.⊥ 50  Cons m he (tl: Vector a ll_typesm) ⇒ λ_.82  Cons m he (tl: Vector addressing_mode_tag m) ⇒ λ_. 51 83 match m return λz.m = z → Bool with 52 84 [ Z ⇒ λ_.is_a he A 53 85  S p ⇒ λK.is_a he A ∨ is_in p (? tl) A] (?: m=m)] (?: S n = S n). 86 (* CSC: cast not working here: why? *) 54 87 ##[##4: #x; ncases K; napply x ] 55 88 //; ndestruct. 56 89 nqed. 57 90 58 nrecord subaddressing_mode (n) (l: Vector all_types (S n)) : Type[0] ≝ 91 ndefinition bool_to_Prop ≝ 92 λb. match b with [ true ⇒ True  false ⇒ False ]. 93 94 nrecord subaddressing_mode (n) (l: Vector addressing_mode_tag (S n)) : Type[0] ≝ 59 95 { subaddressing_modeel:> addressing_mode; 60 subaddressing_modein: 61 match is_in ? l subaddressing_modeel with [ true ⇒ (? : Prop)  false ⇒ (? : Prop) ] 96 subaddressing_modein: bool_to_Prop (is_in ? l subaddressing_modeel) 62 97 }. 63 ##[ napply True  napply False ] 64 nqed. 65 66 ncoercion subaddressing_mode : ∀n.∀l:Vector all_types (S n).Type[0] 67 ≝ subaddressing_mode on _l: Vector all_types (S ?) to Type[0]. 68 69 (* 98 99 ncoercion subaddressing_mode : ∀n.∀l:Vector addressing_mode_tag (S n).Type[0] 100 ≝ subaddressing_mode on _l: Vector addressing_mode_tag (S ?) to Type[0]. 101 70 102 ncoercion mk_subaddressing_mode : 71 ∀n.∀l:Vector all_types (S n).∀a:addressing_mode. 72 ∀p:?(*match is_in ? l a return λ_.Prop with [True ⇒ True  False ⇒ False]*).subaddressing_mode n l 73 ≝ mk_subaddressing_mode on _a:addressing_mode to subaddressing_mode ? ?. 74 *) 75 76 ninductive Jump (A: Type[0]): Type[0] ≝ 77 JC: A → Jump A 78  JNC: A → Jump A 79  JB: Bit → A → Jump A 80  JNB: Bit → A → Jump A 81  JBC: Bit → A → Jump A 82  JZ: A → Jump A 83  JNZ: A → Jump A 84  CJNE: (([acc] × [direct; data]) + [reg; indirect] × [data]) → A → Jump A 85  DJNZ: [reg ; direct] → A → Jump A 86  ADD: [acc] → [reg; direct; indirect; data] → Jump A. 87 88 ndefinition xxx: Jump Nat. 89 napply (DJNZ ? (mk_subaddressing_mode ?? (REGISTER [true] [true] [true]) ?) (Z: Nat)). 103 ∀n.∀l:Vector addressing_mode_tag (S n).∀a:addressing_mode. 104 ∀p:bool_to_Prop (is_in ? l a).subaddressing_mode n l 105 ≝ mk_subaddressing_mode on a:addressing_mode to subaddressing_mode ? ?. 106 107 ninductive jump (A: Type[0]): Type[0] ≝ 108 JC: A → jump A 109  JNC: A → jump A 110  JB: Bit → A → jump A 111  JNB: Bit → A → jump A 112  JBC: Bit → A → jump A 113  JZ: A → jump A 114  JNZ: A → jump A 115  CJNE: 116 [[acc_a]] × [[direct; data]] ⊎ 117 [[register; indirect]] × [[data]] → A → jump A 118  DJNZ: [[register ; direct]] → A → jump A. 119 120 ninductive preinstruction (A: Type[0]) : Type[0] ≝ 121 ADD: [[acc_a]] × [[ register ; direct ; indirect ; data ]] > preinstruction A 122  ADDC: [[acc_a]] × [[ register ; direct ; indirect ; data ]] > preinstruction A 123  SUBB: [[acc_a]] × [[ register ; direct ; indirect ; data ]] > preinstruction A 124  INC: [[ acc_a ; register ; direct ; indirect ; dptr ]] > preinstruction A 125  DEC: [[ acc_a ; register ; direct ; indirect ]] > preinstruction A 126  MUL: [[acc_a]] × [[acc_b]] > preinstruction A 127  DIV: [[acc_a]] × [[acc_b]] > preinstruction A 128  DA: [[acc_a]] > preinstruction A 129 130 (* logical operations *) 131  ANL: 132 [[acc_a]] × [[ register ; direct ; indirect ; data ]] ⊎ 133 [[direct]] × [[ acc_a ; data ]] ⊎ 134 [[carry]] × [[ bit_addr ; n_bit_addr]] > preinstruction A 135  ORL: 136 [[acc_a]] × [[ register ; data ; direct ; indirect ]] ⊎ 137 [[direct]] × [[ acc_a ; data ]] ⊎ 138 [[carry]] × [[ bit_addr ; n_bit_addr]] > preinstruction A 139  XRL: 140 [[acc_a]] × [[ data ; register ; direct ; indirect ]] ⊎ 141 [[direct]] × [[ acc_a ; data ]] > preinstruction A 142  CLR: [[ acc_a ; carry ; bit_addr ]] > preinstruction A 143  CPL: [[ acc_a ; carry ; bit_addr ]] > preinstruction A 144  RL: [[acc_a]] > preinstruction A 145  RLC: [[acc_a]] > preinstruction A 146  RR: [[acc_a]] > preinstruction A 147  RRC: [[acc_a]] > preinstruction A 148  SWAP: [[acc_a]] > preinstruction A 149 150 (* data transfer *) 151  MOV: 152 [[acc_a]] × [[ register ; direct ; indirect ; data ]] ⊎ 153 [[ register ; indirect ]] × [[ acc_a ; direct ; data ]] ⊎ 154 [[direct]] × [[ acc_a ; register ; direct ; indirect ; data ]] ⊎ 155 [[dptr]] × [[data16]] ⊎ 156 [[carry]] × [[bit_addr]] ⊎ 157 [[bit_addr]] × [[carry]] > preinstruction A 158  MOVC: [[acc_a]] × [[ acc_dptr ; acc_pc ]] > preinstruction A 159  MOVX: 160 [[acc_a]] × [[ ext_indirect ; ext_indirect_dptr ]] ⊎ 161 [[ ext_indirect ; ext_indirect_dptr ]] × [[acc_a]] > preinstruction A 162  SETB: [[ carry ; bit_addr ]] > preinstruction A 163  PUSH: [[direct]] > preinstruction A 164  POP: [[direct]] > preinstruction A 165  XCH: [[acc_a]] × [[ register ; direct ; indirect ]] > preinstruction A 166  XCHD: [[acc_a]] × [[indirect]] > preinstruction A 167 168 (* program branching *) 169  Jump: jump A → preinstruction A 170  ACALL: [[addr11]] > preinstruction A 171  LCALL: [[addr16]] > preinstruction A 172  RET: preinstruction A 173  RETI: preinstruction A 174  AJMP: [[addr11]] > preinstruction A 175  LJMP: [[addr16]] > preinstruction A 176  SJMP: [[relative]] > preinstruction A 177  JMP: [[indirect_dptr]] > preinstruction A 178  NOP: preinstruction A. 179 180 181 ndefinition xxx: jump Nat. 182 napply (DJNZ ? (REGISTER [true] [true] [true]) Z). 90 183 napply I; 91 184 nqed. 
Deliverables/D4.1/Matita/BitVector.ma
r260 r262 41 41 λb: BitVector n. 42 42 λm: Nat. 43 set_index Bool n b m.43 set_index_weak Bool n b m. 44 44 45 45 ndefinition drop ≝ 
Deliverables/D4.1/Matita/Vector.ma
r261 r262 26 26 (* ===================================== *) 27 27 28 interpretation "Vector nil" 'nil = (Empty ?). 28 notation "[[ list0 x sep ; ]]" 29 non associative with precedence 90 30 for ${fold right @'vnil rec acc @{'vcons $x $acc}}. 31 32 interpretation "Vector vnil" 'vnil = (Empty ?). 33 interpretation "Vector vcons" 'vcons hd tl = (Cons ? ? hd tl). 29 34 interpretation "Vector cons" 'cons hd tl = (Cons ? ? hd tl). 30 31 notation "hvbox (v break !! n)"32 non associative with precedence 9033 for @{ 'get_index $v $n }.34 35 35 36 (* ===================================== *) … … 81 82 82 83 interpretation "Vector get_index" 'get_index v n = (get_index ? ? v n). 83 84 85 (* 84 86 nlet rec set_index (A: Type[0]) (n: Nat) (v: Vector A n) (m: Nat) (a: A) (lt: m < n) on m: Vector A n ≝ 85 87 (match m with … … 98 100 nassumption. 99 101 nqed. 102 *) 100 103 101 104 nlet rec set_index_weak (A: Type[0]) (n: Nat) … … 224 227 ]. 225 228 226 notation "v break @ q"227 right associative with precedence 47228 for @{ 'append $v $q }.229 230 229 interpretation "Vector append" 'append hd tl = (append ? ? hd tl). 231 230
Note: See TracChangeset
for help on using the changeset viewer.