Changeset 256 for Deliverables/D4.1/Matita/ASM.ma
 Timestamp:
 Nov 22, 2010, 7:25:53 PM (10 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

Deliverables/D4.1/Matita/ASM.ma
r249 r256 3 3 include "Either.ma". 4 4 include "BitVector.ma". 5 include "String.ma". 6 7 ninductive Direct: Type[0] ≝ 8 DIRECT: Byte → Direct. 9 ninductive Indirect: Type[0] ≝ 10 INDIRECT: Bit → Indirect. 11 ninductive ExtIndirect: Type[0] ≝ 12 EXTINDIRECT: Bit → ExtIndirect. 13 ninductive Register: Type[0] ≝ 14 REGISTER: Bit → Bit → Bit → Register. 15 ninductive AccumulatorA: Type[0] ≝ 16 ACCUMULATORA: AccumulatorA. 17 ninductive AccumulatorB: Type[0] ≝ 18 ACCUMULATORB: AccumulatorB. 19 ninductive DPointer: Type[0] ≝ 20 DPOINTER: DPointer. 21 ninductive Data: Type[0] ≝ 22 DATA: Byte → Data. 23 ninductive Data16: Type[0] ≝ 24 DATA16: Word → Data16. 25 ninductive AccumulatorDPointer: Type[0] ≝ 26 ACCUMULATORDPOINTER: AccumulatorDPointer. 27 ninductive AccumulatorProgramCounter: Type[0] ≝ 28 ACCUMULATORPROGRAMCOUNTER: AccumulatorProgramCounter. 29 ninductive ExternalIndirectDPointer: Type[0] ≝ 30 EXTERNALINDIRECTDPOINTER: ExternalIndirectDPointer. 31 ninductive IndirectDPointer: Type[0] ≝ 32 INDIRECTDPOINTER: IndirectDPointer. 33 ninductive Carry: Type[0] ≝ 34 CARRY: Carry. 35 ninductive BitAddress: Type[0] ≝ 36 BIT: Bit → BitAddress. 37 ninductive ComplementBitAddress: Type[0] ≝ 38 COMPLEMENTBITADDRESS: Bit → ComplementBitAddress. 39 ninductive Relative: Type[0] ≝ 40 RELATIVE: Byte → Relative. 41 ninductive Address11: Type[0] ≝ 42 ADDRESS11: Word11 → Address11. 43 ninductive Address16: Type[0] ≝ 44 ADDRESS16: Word → Address16. 45 46 ninductive Union2 (A: Type[0]) (B: Type[0]): Type[0] ≝ 47 U2: A → B → Union2 A B. 48 49 ninductive Union3 (A: Type[0]) (B: Type[0]) (C: Type[0]): Type[0] ≝ 50 U3: A → B → C → Union3 A B C. 51 52 ninductive Union6 (A: Type[0]) (B: Type[0]) 53 (C: Type[0]) (D: Type[0]) 54 (E: Type[0]) (F: Type[0]): Type[0] ≝ 55 U6: A → B → C → D → E → F → Union6 A B C D E F. 5 include "BitVectorTrie.ma". 6 7 ninductive all_types : Type[0] ≝ 8 reg: all_types  direct: all_types  indirect:all_types  data:all_types 9  acc: all_types  rel: all_types. 10 11 interpretation "Cartesian" 'product A B = (Cartesian A B). 12 interpretation "Either" 'plus A B = (Either A B). 13 14 ninductive addressing_mode: Type[0] ≝ 15 DIRECT: Byte → addressing_mode 16  INDIRECT: Bit → addressing_mode 17  EXTINDIRECT: Bit → addressing_mode 18  REGISTER: Bit → Bit → Bit → addressing_mode 19  ACCUMULATORA: addressing_mode 20  ACCUMULATORB: addressing_mode 21  DPOINTER: addressing_mode 22  DATA: Byte → addressing_mode 23  DATA16: Word → addressing_mode 24  ACCUMULATORDPOINTER: addressing_mode 25  ACCUMULATORPROGRAMCOUNTER: addressing_mode 26  EXTERNALINDIRECTDPOINTER: addressing_mode 27  INDIRECTDPOINTER: addressing_mode 28  CARRY: addressing_mode 29  BIT: Bit → addressing_mode 30  COMPLEMENTBITADDRESS: Bit → addressing_mode 31  RELATIVE: Byte → addressing_mode 32  ADDRESS11: Word11 → addressing_mode 33  ADDRESS16: Word → addressing_mode. 34 35 (* to avoid expansion... *) 36 nlet rec is_a (d:all_types) (A:addressing_mode) on d ≝ 37 match d with 38 [ reg ⇒ match A with [ REGISTER _ _ _ ⇒ True  _ ⇒ False ] 39  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 49 [ Empty ⇒ λK.⊥ 50  Cons m he (tl: Vector all_types m) ⇒ λ_. 51 match m return λz.m = z → Bool with 52 [ Z ⇒ λ_.is_a he A 53  S p ⇒ λK.is_a he A ∨ is_in p (? tl) A] (?: m=m)] (?: S n = S n). 54 ##[##4: #x; ncases K; napply x ] 55 //; ndestruct. 56 nqed. 57 58 nrecord subaddressing_mode (n) (l: Vector all_types (S n)) : Type[0] ≝ 59 { subaddressing_modeel:> addressing_mode; 60 subaddressing_modein: 61 match is_in ? l subaddressing_modeel with [ True ⇒ (? : Prop)  False ⇒ (? : Prop) ] 62 }. 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 (* 70 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 *) 56 75 57 76 ninductive Jump (A: Type[0]): Type[0] ≝ … … 63 82  JZ: A → Jump A 64 83  JNZ: A → Jump A 65  CJNE: (Cartesian (Union2 (Cartesian AccumulatorA (Either Direct Data)) (Cartesian (Either Register Indirect) Data)) A) → Jump A 66  DJNZ: Cartesian (Either Register Direct) A → Jump A. 67 68 ndefinition Preamble ≝ List (Cartesian String Nat). 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)). 90 napply I; 91 nqed. 92 93 naxiom bar: addressing_mode → Nat. 94 95 ndefinition barj ≝ 96 λA.λf:A → Nat.λJ:Jump A. 97 match J with 98 [ DJNZ arg1 arg2 ⇒ f arg2 + bar arg1 99  _ ⇒ (Z: Nat)]. 100 101 ndefinition PreInstruction ≝ λA: Type[0]. Jump A. 102 103 ndefinition Instruction ≝ PreInstruction [rel]. 104 105 nrecord Sigma (A: Type[0]) (T: A → Type[0]) : Type[0] ≝ { 106 elem:> A; 107 witness: T elem 108 }. 109 110 interpretation "Sigma" 'sigma T = (Sigma ? T). 111 112 ndefinition true: Bool ≝ True. 113 ndefinition false: Bool ≝ False. 114 naxiom daemon: False. 115 116 naxiom decode_register: Vector Bool (S (S (S Z))) → [reg]. 117 naxiom decode_direct: Vector Bool (S (S (S Z))) → [direct]. 118 119 ndefinition decode_tbl0: List ((Σn.Vector Bool n) × (Vector Bool (S (S (S Z))) → Instruction)) 120 ≝ 121 [mk_Cartesian ?? 122 (mk_Sigma ? (λn.Vector Bool n) ? [ false; false; true; false; true]) 123 (λl. 124 ADD ? (mk_subaddressing_mode ? [acc] ACCUMULATORA ?) 125 (mk_subaddressing_mode ? ? (decode_register l) ?)); 126 mk_Cartesian ?? 127 (mk_Sigma ? (λn.Vector Bool n) ? [ false; false; true; false; true]) 128 (λl. 129 ADD ? (mk_subaddressing_mode ? [acc] ACCUMULATORA ?) 130 (mk_subaddressing_mode ? ? (decode_direct l) ?)) ]. 131 ncases daemon. 132 nqed. 133 134 135 naxiom decode_register: List Bool → [reg]. 136 naxiom decode_direct: List Bool → [direct]. 137 138 ndefinition decode_tbl0: List (List Bool × (List Bool → Instruction)) 139 ≝ 140 [mk_Cartesian ?? 141 [ false; false; true; false; true] 142 (λl. 143 ADD ? (mk_subaddressing_mode ? [acc] ACCUMULATORA ?) 144 (mk_subaddressing_mode ? ? (decode_register l) ?)); 145 mk_Cartesian ?? 146 [ false; false; true; false; true] 147 (λl. 148 ADD ? (mk_subaddressing_mode ? [acc] ACCUMULATORA ?) 149 (mk_subaddressing_mode ? ? (decode_direct l) ?)) ]. 150 ncases daemon. 151 nqed. 152 153 154 ndefinition decode_tbl1: 155 List (List Bool × Σaddr:all_types. [addr] → Instruction) 156 ≝ 157 [mk_Cartesian ?? 158 [ false; false; true; false; true] 159 (mk_Sigma ? (λaddr:all_types. [addr] → Instruction) 160 reg 161 (λa. 162 ADD ? (mk_subaddressing_mode ? [acc] ACCUMULATORA ?) 163 (mk_subaddressing_mode ? ? a ?))) ]. 164 ncases daemon. 165 nqed. 166 167 ndefinition decode_tbl2: 168 List (List Bool × Σaddr:all_types. [addr] → Instruction) 169 ≝ 170 [mk_Cartesian ?? 171 [ false; false; true; false; false; true; false; true] 172 (mk_Sigma ? (λaddr:all_types. [addr] → Instruction) 173 direct 174 (λa. 175 ADD ? (mk_subaddressing_mode ? [acc] ACCUMULATORA ?) 176 (mk_subaddressing_mode ? ? a ?))) ]. 177 ncases daemon. 178 nqed. 179 180 ndefinition decode_tbl ≝ decode_tbl1 @ decode_tbl2. 181 182 decode_addr_mode; ∀addr:all_types. List Bool → [addr]. 183 184 decode ≝ 185 λl:List Bit. 186 List.iter 187 (fun l0 addr mk_f → 188 match split_prefix l l0 with 189 [ None ⇒ ... 190  Some r ⇒ mk_f (decode_addr_mode r) ] 191 192 ) decode_tbl 193 194 encode ≝ 195 196 ndefinition decode_tbl: 197 List (List Bool × Σaddr:all_types. [addr] → Instruction) 198 ≝ 199 [mk_Cartesian ?? 200 [ False; False; True; False; True] 201 (mk_Sigma all_types (λaddr:all_types. [addr] → Instruction) 202 reg 203 (λa:subaddressing_mode ? [reg]. 204 ADD ? (mk_subaddressing_mode ? [acc] ACCUMULATORA ?) 205 (mk_subaddressing_mode ? ? a ?))); 206 mk_Cartesian ?? 207 [ False; False; True; False; False; True; False; True] 208 (mk_Sigma all_types (λaddr:all_types. [addr] → Instruction) 209 direct 210 (λa:subaddressing_mode ? [direct]. 211 ADD ? (mk_subaddressing_mode ? [acc] ACCUMULATORA ?) 212 (mk_subaddressing_mode ? ? a ?))) 213 ]. 214 nnormalize; 215 216 ].
Note: See TracChangeset
for help on using the changeset viewer.