Changeset 264 for Deliverables
 Timestamp:
 Nov 23, 2010, 5:05:07 PM (9 years ago)
 Location:
 Deliverables/D4.1/Matita
 Files:

 1 added
 4 edited
Legend:
 Unmodified
 Added
 Removed

Deliverables/D4.1/Matita/ASM.ma
r262 r264 1 include "Universes.ma".2 include "Plogic/equality.ma".3 1 include "Either.ma". 4 include "BitVector.ma".5 2 include "BitVectorTrie.ma". 3 include "String.ma". 6 4 7 5 interpretation "Cartesian" 'product A B = (Cartesian A B). … … 178 176  NOP: preinstruction A. 179 177 178 ndefinition instruction ≝ preinstruction [[relative]]. 180 179 181 ndefinition xxx: jump Nat. 182 napply (DJNZ ? (REGISTER [true] [true] [true]) Z). 183 napply I; 184 nqed. 180 ninductive labelled_instruction: Type[0] ≝ 181 Instruction: instruction → labelled_instruction 182  Cost: String → labelled_instruction 183  Jmp: String → labelled_instruction 184  Call: String → labelled_instruction 185  Mov: [[dptr]] × String → labelled_instruction 186  WithLabel: preinstruction String → labelled_instruction. 185 187 186 n axiom bar: addressing_mode → Nat.188 ndefinition preamble ≝ List (String × Nat). 187 189 188 ndefinition barj ≝ 189 λA.λf:A → Nat.λJ:Jump A. 190 match J with 191 [ DJNZ arg1 arg2 ⇒ f arg2 + bar arg1 192  _ ⇒ (Z: Nat)]. 193 194 ndefinition PreInstruction ≝ λA: Type[0]. Jump A. 195 196 ndefinition Instruction ≝ PreInstruction [rel]. 197 198 nrecord Sigma (A: Type[0]) (T: A → Type[0]) : Type[0] ≝ { 199 elem:> A; 200 witness: T elem 201 }. 202 203 interpretation "Sigma" 'sigma T = (Sigma ? T). 204 205 naxiom daemon: False. 206 207 naxiom decode_register: Vector Bool (S (S (S Z))) → [reg]. 208 naxiom decode_direct: Vector Bool (S (S (S Z))) → [direct]. 209 210 ndefinition decode_tbl0: List ((Σn.Vector Bool n) × (Vector Bool (S (S (S Z))) → Instruction)) 211 ≝ 212 [mk_Cartesian ?? 213 (mk_Sigma ? (λn.Vector Bool n) ? [ false; false; true; false; true]) 214 (λl. 215 ADD ? (mk_subaddressing_mode ? [acc] ACCUMULATORA ?) 216 (mk_subaddressing_mode ? ? (decode_register l) ?)); 217 mk_Cartesian ?? 218 (mk_Sigma ? (λn.Vector Bool n) ? [ false; false; true; false; true]) 219 (λl. 220 ADD ? (mk_subaddressing_mode ? [acc] ACCUMULATORA ?) 221 (mk_subaddressing_mode ? ? (decode_direct l) ?)) ]. 222 ncases daemon. 223 nqed. 224 225 226 naxiom decode_register: List Bool → [reg]. 227 naxiom decode_direct: List Bool → [direct]. 228 229 ndefinition decode_tbl0: List (List Bool × (List Bool → Instruction)) 230 ≝ 231 [mk_Cartesian ?? 232 [ false; false; true; false; true] 233 (λl. 234 ADD ? (mk_subaddressing_mode ? [acc] ACCUMULATORA ?) 235 (mk_subaddressing_mode ? ? (decode_register l) ?)); 236 mk_Cartesian ?? 237 [ false; false; true; false; true] 238 (λl. 239 ADD ? (mk_subaddressing_mode ? [acc] ACCUMULATORA ?) 240 (mk_subaddressing_mode ? ? (decode_direct l) ?)) ]. 241 ncases daemon. 242 nqed. 243 244 245 ndefinition decode_tbl1: 246 List (List Bool × Σaddr:all_types. [addr] → Instruction) 247 ≝ 248 [mk_Cartesian ?? 249 [ false; false; true; false; true] 250 (mk_Sigma ? (λaddr:all_types. [addr] → Instruction) 251 reg 252 (λa. 253 ADD ? (mk_subaddressing_mode ? [acc] ACCUMULATORA ?) 254 (mk_subaddressing_mode ? ? a ?))) ]. 255 ncases daemon. 256 nqed. 257 258 ndefinition decode_tbl2: 259 List (List Bool × Σaddr:all_types. [addr] → Instruction) 260 ≝ 261 [mk_Cartesian ?? 262 [ false; false; true; false; false; true; false; true] 263 (mk_Sigma ? (λaddr:all_types. [addr] → Instruction) 264 direct 265 (λa. 266 ADD ? (mk_subaddressing_mode ? [acc] ACCUMULATORA ?) 267 (mk_subaddressing_mode ? ? a ?))) ]. 268 ncases daemon. 269 nqed. 270 271 ndefinition decode_tbl ≝ decode_tbl1 @ decode_tbl2. 272 273 decode_addr_mode; ∀addr:all_types. List Bool → [addr]. 274 275 decode ≝ 276 λl:List Bit. 277 List.iter 278 (fun l0 addr mk_f → 279 match split_prefix l l0 with 280 [ None ⇒ ... 281  Some r ⇒ mk_f (decode_addr_mode r) ] 282 283 ) decode_tbl 284 285 encode ≝ 286 287 ndefinition decode_tbl: 288 List (List Bool × Σaddr:all_types. [addr] → Instruction) 289 ≝ 290 [mk_Cartesian ?? 291 [ False; False; True; False; True] 292 (mk_Sigma all_types (λaddr:all_types. [addr] → Instruction) 293 reg 294 (λa:subaddressing_mode ? [reg]. 295 ADD ? (mk_subaddressing_mode ? [acc] ACCUMULATORA ?) 296 (mk_subaddressing_mode ? ? a ?))); 297 mk_Cartesian ?? 298 [ False; False; True; False; False; True; False; True] 299 (mk_Sigma all_types (λaddr:all_types. [addr] → Instruction) 300 direct 301 (λa:subaddressing_mode ? [direct]. 302 ADD ? (mk_subaddressing_mode ? [acc] ACCUMULATORA ?) 303 (mk_subaddressing_mode ? ? a ?))) 304 ]. 305 nnormalize; 306 307 ]. 190 ndefinition assembly_program ≝ preamble × (List labelled_instruction). 
Deliverables/D4.1/Matita/Char.ma
r249 r264 1 1 include "Universes.ma". 2 2 3 (* 3 4 ninductive Char: Type[0] ≝ 4 5 a: Char … … 54 55  Y: Char 55 56  Z: Char. 57 *) 
Deliverables/D4.1/Matita/String.ma
r249 r264 2 2 include "List.ma". 3 3 4 ndefinition String ≝ List Char. 4 (*ndefinition String ≝ List Char.*) 5 naxiom String: Type[0]. 
Deliverables/D4.1/Matita/depends
r261 r264 1 Arithmetic.ma BitVector.ma Bool.ma Connectives.ma Exponential.ma List.ma Nat.ma Plogic/equality.ma Universes.ma 1 2 Exponential.ma Connectives.ma Equality.ma Nat.ma 2 Arithmetic.ma BitVector.ma Bool.ma Connectives.ma Exponential.ma List.ma Nat.ma Plogic/equality.ma Universes.ma3 3 BitVectorTrie.ma BitVector.ma Bool.ma Maybe.ma 4 4 Cartesian.ma Universes.ma 5 Universes.ma6 5 Maybe.ma Bool.ma Plogic/equality.ma Universes.ma 7 6 Either.ma Bool.ma Maybe.ma Universes.ma 8 ASM.ma BitVector.ma BitVectorTrie.ma Either.ma Plogic/equality.ma Universes.ma 7 Universes.ma 8 ASM.ma BitVectorTrie.ma Either.ma String.ma 9 Vector.ma Cartesian.ma List.ma Maybe.ma Nat.ma Plogic/equality.ma Universes.ma Util.ma 9 10 Char.ma Universes.ma 10 Vector.ma Cartesian.ma List.ma Maybe.ma Nat.ma Plogic/equality.ma Universes.ma Util.ma11 11 Connectives.ma Plogic/equality.ma 12 12 Bool.ma Universes.ma 13 Assembly.ma ASM.ma 13 14 List.ma Bool.ma Nat.ma Plogic/equality.ma Universes.ma Util.ma 14 15 Util.ma Nat.ma 15 16 Interpret.ma Arithmetic.ma BitVectorTrie.ma 16 String.ma Char.ma List.ma17 17 BitVector.ma Bool.ma List.ma Nat.ma Universes.ma Vector.ma 18 18 Compare.ma Universes.ma 19 String.ma Char.ma List.ma 19 20 Plogic/equality.ma Universes.ma 20 21 Nat.ma Bool.ma Cartesian.ma Connectives.ma
Note: See TracChangeset
for help on using the changeset viewer.