Changeset 271 for Deliverables/D4.1/Matita/Assembly.ma
 Timestamp:
 Nov 24, 2010, 1:00:41 AM (11 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

Deliverables/D4.1/Matita/Assembly.ma
r269 r271 1 1 include "ASM.ma". 2 2 3 (* 4 ndefinition from_addressing_mode_tag ≝ 5 λT:Type[0].λt:addressing_mode_tag. 6 match t with 7 [ direct ⇒ Byte → T 8  indirect ⇒ Bit → T 9  ext_indirect ⇒ Bit → T 10  register ⇒ Bit → Bit → Bit → T 11  acc_a ⇒ T 12  acc_b ⇒ T 13  dptr ⇒ T 14  data ⇒ Byte → T 15  data16 ⇒ Word → T 16  acc_dptr ⇒ T 17  acc_pc ⇒ T 18  ext_indirect_dptr ⇒ T 19  indirect_dptr ⇒ T 20  carry ⇒ T 21  bit_addr ⇒ Bit → T 22  n_bit_addr ⇒ Bit → T 23  relative ⇒ Byte → T 24  addr11 ⇒ Word11 → T 25  addr16 ⇒ Word → T ]. 26 *) 27 (* 28 nlet rec elim_addr (T:addressing_mode → Type[0]) n l on l 29 : subaddressing_mode n l → Type[0] ≝ 30 match l 31 return λm.λl:Vector addressing_mode_tag m. 32 ∀proof:m = S n. 33 subaddressing_mode n (match proof with [refl ⇒ l]) → Type[0] with 34 [ Empty ⇒ λK.λ_.Nat 35  Cons o he tl ⇒ λK.λv.Nat(* 36 match o 37 return λy.∀p:S y = S n. 38 subaddressing_mode y 39 (v⌈Vector addressing_mode_tag (S y) ↦ Vector addressing_mode_tag (S n)⌉) 40 → Type[0] 41 with 42 [ Z ⇒ λK.λv.(? : Type[0]) 43  S p ⇒ λK.λv.(? : Type[0]) 44 ]*) 45 ] (?: S n = S n). 46 ##[##1: @ 47  ndestruct 48 ##7: // 49  normalize; 50 51 nlet rec elim_addr n (v: Vector addressing_mode_tag (S n)) on v 52 : subaddressing_mode n v Type[0] 53 ≝ 54 match v return λx.λ_.x = S n. Type[0] with 55 [ Empty ⇒ λK.⊥ 56  Cons o he tl ⇒ λK. 57 match o with 58 [ Z ⇒ 59  S m ⇒ 60 ] 61 ] (? : S n = S n). 62 *) 63 64 notation "hvbox('let' 〈ident x,ident y〉 ≝ t 'in' s)" 65 with precedence 10 66 for @{ match $t with [ mk_Cartesian ${ident x} ${ident y} ⇒ $s ] }. 67 68 ncheck (let 〈x,z〉 ≝ 〈Z,Z〉 in 〈x,z〉). 69 3 70 ndefinition assembly1 ≝ 4 λ i.match i with71 λA.λi: preinstruction A.match i with 5 72 [ ACALL addr ⇒ 6 let w ≝ 7 match addr with [ mk_subaddressing_mode addr1 proof1 ⇒ 8 match addr1 return λx.∀proof: bool_to_Prop (is_in ?? x).? with 9 [ ADDR11 w ⇒ λ_.w  _ ⇒ λK.⊥ ] proof1] in 10 match split ?? (S (S (S (S (S (S (S (S Z)))))))) w with 11 [ mk_Cartesian v1 v2 ⇒ 12 v1 @ [[true; false; false; false; true]] @ v2 ] 13  _ ⇒ ? ]. 14 ##[##28,29,30,31,32,33,34,35,36,37,38,39,40,41,42,43,44,45: napply K; 15 ####47: 16 17 let (a10,a9,a8,b1) = from_word11 w in 18 [mk_byte_from_bits ((a10,a9,a8,true),(false,false,false,true)); b1] 19  `ADD (`A,`REG (r1,r2,r3)) > 20 [mk_byte_from_bits ((false,false,true,false),(true,r1,r2,r3))] 21  `ADD (`A, `DIRECT b1) > 22 [mk_byte_from_bits ((false,false,true,false),(false,true,false,true)); b1] 23  `ADD (`A, `INDIRECT i1) > 24 [mk_byte_from_bits ((false,false,true,false),(false,true,true,i1))] 25  `ADD (`A, `DATA b1) > 26 [mk_byte_from_bits ((false,false,true,false),(false,true,false,false)); b1] 73 match addr return λx. bool_to_Prop (is_in ? [[addr11]] x) → ? with 74 [ ADDR11 w ⇒ λ_. 75 let 〈v1,v2〉 ≝ split ? (S (S (S (S (S (S (S (S Z)))))))) (S (S (S Z))) w in 76 [ (v1 @ [[true; false; false; false; true]]) ; v2 ] 77  _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr) 78  ADD addr1 addr2 ⇒ 79 match addr2 return λx. bool_to_Prop (is_in ? [[register;direct;indirect;data]] x) → ? with 80 [ REGISTER r1 r2 r3 ⇒ λ_.[ ([[false;false;true;false;true;r1;r2;r2]]) ] 81  DIRECT b1 ⇒ λ_.[ ([[false;false;true;false;false;true;false;true]]); b1 ] 82  INDIRECT i1 ⇒ λ_. [ ([[false;false;true;false;false;true;true;i1]]) ] 83  DATA b1 ⇒ λ_. [ ([[false;false;true;false;false;true;false;false]]) ; b1 ] 84  _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr2) 85  _ ⇒ [ ([[false;false;false;false;false;false;false;false]]) ]]. 86 87 27 88  `ADDC (`A, `REG(r1,r2,r3)) > 28 89 [mk_byte_from_bits ((false,false,true,true),(true,r1,r2,r3))]
Note: See TracChangeset
for help on using the changeset viewer.