Changeset 374 for Deliverables/D4.1/Matita/DoTest.ma
 Timestamp:
 Dec 5, 2010, 11:54:59 PM (11 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

Deliverables/D4.1/Matita/DoTest.ma
r372 r374 5 5 ndefinition testmem ≝ assembly test. 6 6 ndefinition teststatus ≝ load testmem initialise_status. 7 ndefinition testfinal ≝ execute (four * two_hundred_and_fifty_six) teststatus.7 ndefinition testfinal ≝ execute four (*(four * two_hundred_and_fifty_six)*) teststatus. 8 8 9 9 notation "'STATUS'" with precedence 90 for @{ 'status }. 10 10 interpretation "status" 'status = (mk_Status ??????????). 11 11 12 (* 13 nlemma xoo: testfinal = testfinal. 14 nnormalize in ⊢ (??%?); @; 15 nqed. 16 *) 12 nlet rec execute_trace (n: Nat) (s: Status) on n: List ? ≝ 13 match n with 14 [ Z ⇒ [] 15  S o ⇒ 16 first … (first … (fetch (code_memory s) (program_counter s))) :: execute_trace o (execute_1 s) 17 ]. 17 18 18 (* 19 nlemma test: 20 (let status ≝ 21 load 22 (assembly [LJMP … (ADDR16 [[false;false;false;false;false;false;false;false;false;false;false;false;true;false;false;false]])]) 23 initialise_status 24 in 25 fetch (code_memory status) (program_counter status) 26 ) = ?. 27 ##[ nnormalize in ⊢ (??%?); 28 *) 19 interpretation "left" 'left x = (Left ?? x). 20 interpretation "right" 'right x = (Right ?? x). 29 21 30 (* 31 nlemma xoo: 32 (let testfinal ≝ testfinal in 33 first … (first … (fetch (code_memory testfinal) (program_counter testfinal)))) = 34 first … (first … (fetch (code_memory testfinal) (program_counter testfinal))). 35 nnormalize in ⊢ (??%?); 36 nqed. 22 notation < "'L' x" with precedence 70 for @{ 'left $x }. 23 notation < "'R' x" with precedence 70 for @{ 'right $x }. 37 24 38 ndefinition is_JZ ≝ 39 λi: instruction.match i with 40 [ Jump arg ⇒ 41 match arg with 42 [ JZ arg ⇒ 43 match arg with 44 [ RELATIVE arg ⇒ arg 45  _ ⇒ zero eight ] 46  _ ⇒ zero eight ] 47  _ ⇒ zero eight ]. 25 notation < "𝟘" with precedence 90 for @{ 'zero }. 26 notation < "𝟙" with precedence 90 for @{ 'one }. 27 notation < "𝟚" with precedence 90 for @{ 'two }. 28 notation < "𝟛" with precedence 90 for @{ 'three }. 29 notation < "𝟜" with precedence 90 for @{ 'four }. 30 notation < "𝟝" with precedence 90 for @{ 'five }. 31 notation < "𝟞" with precedence 90 for @{ 'six }. 32 notation < "𝟟" with precedence 90 for @{ 'seven }. 33 notation < "𝟠" with precedence 90 for @{ 'eight }. 34 notation < "𝟡" with precedence 90 for @{ 'nine }. 35 notation < "𝔸" with precedence 90 for @{ 'a }. 36 notation < "𝔹" with precedence 90 for @{ 'b }. 37 notation < "∁" with precedence 90 for @{ 'c }. 38 notation < "𝔻" with precedence 90 for @{ 'd }. 39 notation < "𝔼" with precedence 90 for @{ 'e }. 40 notation < "𝔽" with precedence 90 for @{ 'f }. 41 42 43 interpretation "zero" 'zero = (VCons ?? false (VCons ?? false (VCons ?? false (VCons ?? false (VEmpty ?))))). 44 interpretation "one" 'one = (VCons ?? false (VCons ?? false (VCons ?? false (VCons ?? true (VEmpty ?))))). 45 interpretation "two" 'two = (VCons ?? false (VCons ?? false (VCons ?? true (VCons ?? false (VEmpty ?))))). 46 interpretation "three" 'three = (VCons ?? false (VCons ?? false (VCons ?? true (VCons ?? true (VEmpty ?))))). 47 interpretation "four" 'four = (VCons ?? false (VCons ?? true (VCons ?? false (VCons ?? false (VEmpty ?))))). 48 interpretation "five" 'five = (VCons ?? false (VCons ?? true (VCons ?? false (VCons ?? true (VEmpty ?))))). 49 interpretation "six" 'six = (VCons ?? false (VCons ?? true (VCons ?? true (VCons ?? false (VEmpty ?))))). 50 interpretation "seven" 'seven = (VCons ?? false (VCons ?? true (VCons ?? true (VCons ?? true (VEmpty ?))))). 51 interpretation "eight" 'eight = (VCons ?? true (VCons ?? false (VCons ?? false (VCons ?? false (VEmpty ?))))). 52 interpretation "nine" 'nine = (VCons ?? true (VCons ?? false (VCons ?? false (VCons ?? true (VEmpty ?))))). 53 interpretation "A" 'a = (VCons ?? true (VCons ?? false (VCons ?? true (VCons ?? false (VEmpty ?))))). 54 interpretation "B" 'b = (VCons ?? true (VCons ?? false (VCons ?? true (VCons ?? true (VEmpty ?))))). 55 interpretation "C" 'c = (VCons ?? true (VCons ?? true (VCons ?? false (VCons ?? false (VEmpty ?))))). 56 interpretation "D" 'd = (VCons ?? true (VCons ?? true (VCons ?? false (VCons ?? true (VEmpty ?))))). 57 interpretation "E" 'e = (VCons ?? true (VCons ?? true (VCons ?? true (VCons ?? false (VEmpty ?))))). 58 interpretation "F" 'f = (VCons ?? true (VCons ?? true (VCons ?? true (VCons ?? true (VEmpty ?))))). 59 60 notation < "𝟘l" with precedence 90 for @{ 'zero4 $l }. 61 notation < "𝟙l" with precedence 90 for @{ 'one4 $l }. 62 notation < "𝟚l" with precedence 90 for @{ 'two4 $l }. 63 notation < "𝟛l" with precedence 90 for @{ 'three4 $l }. 64 notation < "𝟜l" with precedence 90 for @{ 'four4 $l }. 65 notation < "𝟝l" with precedence 90 for @{ 'five4 $l }. 66 notation < "𝟞l" with precedence 90 for @{ 'six4 $l }. 67 notation < "𝟟l" with precedence 90 for @{ 'seven4 $l }. 68 notation < "𝟠l" with precedence 90 for @{ 'eight4 $l }. 69 notation < "𝟡l" with precedence 90 for @{ 'nine4 $l }. 70 notation < "𝔸l" with precedence 90 for @{ 'a4 $l }. 71 notation < "𝔹l" with precedence 90 for @{ 'b4 $l }. 72 notation < "∁l" with precedence 90 for @{ 'c4 $l }. 73 notation < "𝔻l" with precedence 90 for @{ 'd4 $l }. 74 notation < "𝔼l" with precedence 90 for @{ 'e4 $l }. 75 notation < "𝔽l" with precedence 90 for @{ 'f4 $l }. 76 77 interpretation "zero4" 'zero4 l = (VCons ?? false (VCons ?? false (VCons ?? false (VCons ? (S (S (S (S Z)))) false l)))). 78 interpretation "one4" 'one4 l = (VCons ?? false (VCons ?? false (VCons ?? false (VCons ? (S (S (S (S Z)))) true l)))). 79 interpretation "two4" 'two4 l = (VCons ?? false (VCons ?? false (VCons ?? true (VCons ? (S (S (S (S Z)))) false l)))). 80 interpretation "three4" 'three4 l = (VCons ?? false (VCons ?? false (VCons ?? true (VCons ? (S (S (S (S Z)))) true l)))). 81 interpretation "four4" 'four4 l = (VCons ?? false (VCons ?? true (VCons ?? false (VCons ? (S (S (S (S Z)))) false l)))). 82 interpretation "five4" 'five4 l = (VCons ?? false (VCons ?? true (VCons ?? false (VCons ? (S (S (S (S Z)))) true l)))). 83 interpretation "six4" 'six4 l = (VCons ?? false (VCons ?? true (VCons ?? true (VCons ? (S (S (S (S Z)))) false l)))). 84 interpretation "seven4" 'seven4 l = (VCons ?? false (VCons ?? true (VCons ?? true (VCons ? (S (S (S (S Z)))) true l)))). 85 interpretation "eight4" 'eight4 l = (VCons ?? true (VCons ?? false (VCons ?? false (VCons ? (S (S (S (S Z)))) false l)))). 86 interpretation "nine4" 'nine4 l = (VCons ?? true (VCons ?? false (VCons ?? false (VCons ? (S (S (S (S Z)))) true l)))). 87 interpretation "A4" 'a4 l = (VCons ?? true (VCons ?? false (VCons ?? true (VCons ? (S (S (S (S Z)))) false l)))). 88 interpretation "B4" 'b4 l = (VCons ?? true (VCons ?? false (VCons ?? true (VCons ? (S (S (S (S Z)))) true l)))). 89 interpretation "C4" 'c4 l = (VCons ?? true (VCons ?? true (VCons ?? false (VCons ? (S (S (S (S Z)))) false l)))). 90 interpretation "D4" 'd4 l = (VCons ?? true (VCons ?? true (VCons ?? false (VCons ? (S (S (S (S Z)))) true l)))). 91 interpretation "E4" 'e4 l = (VCons ?? true (VCons ?? true (VCons ?? true (VCons ? (S (S (S (S Z)))) false l)))). 92 interpretation "F4" 'f4 l = (VCons ?? true (VCons ?? true (VCons ?? true (VCons ? (S (S (S (S Z)))) true l)))). 93 94 interpretation "zero8" 'zero4 l = (VCons ?? false (VCons ?? false (VCons ?? false (VCons ? (S (S (S (S (S (S (S (S Z)))))))) false l)))). 95 interpretation "one8" 'one4 l = (VCons ?? false (VCons ?? false (VCons ?? false (VCons ? (S (S (S (S (S (S (S (S Z)))))))) true l)))). 96 interpretation "two8" 'two4 l = (VCons ?? false (VCons ?? false (VCons ?? true (VCons ? (S (S (S (S (S (S (S (S Z)))))))) false l)))). 97 interpretation "three8" 'three4 l = (VCons ?? false (VCons ?? false (VCons ?? true (VCons ? (S (S (S (S (S (S (S (S Z)))))))) true l)))). 98 interpretation "four8" 'four4 l = (VCons ?? false (VCons ?? true (VCons ?? false (VCons ? (S (S (S (S (S (S (S (S Z)))))))) false l)))). 99 interpretation "five8" 'five4 l = (VCons ?? false (VCons ?? true (VCons ?? false (VCons ? (S (S (S (S (S (S (S (S Z)))))))) true l)))). 100 interpretation "six8" 'six4 l = (VCons ?? false (VCons ?? true (VCons ?? true (VCons ? (S (S (S (S (S (S (S (S Z)))))))) false l)))). 101 interpretation "seven8" 'seven4 l = (VCons ?? false (VCons ?? true (VCons ?? true (VCons ? (S (S (S (S (S (S (S (S Z)))))))) true l)))). 102 interpretation "eight8" 'eight4 l = (VCons ?? true (VCons ?? false (VCons ?? false (VCons ? (S (S (S (S (S (S (S (S Z)))))))) false l)))). 103 interpretation "nine8" 'nine4 l = (VCons ?? true (VCons ?? false (VCons ?? false (VCons ? (S (S (S (S (S (S (S (S Z)))))))) true l)))). 104 interpretation "A8" 'a4 l = (VCons ?? true (VCons ?? false (VCons ?? true (VCons ? (S (S (S (S (S (S (S (S Z)))))))) false l)))). 105 interpretation "B8" 'b4 l = (VCons ?? true (VCons ?? false (VCons ?? true (VCons ? (S (S (S (S (S (S (S (S Z)))))))) true l)))). 106 interpretation "C8" 'c4 l = (VCons ?? true (VCons ?? true (VCons ?? false (VCons ? (S (S (S (S (S (S (S (S Z)))))))) false l)))). 107 interpretation "D8" 'd4 l = (VCons ?? true (VCons ?? true (VCons ?? false (VCons ? (S (S (S (S (S (S (S (S Z)))))))) true l)))). 108 interpretation "E8" 'e4 l = (VCons ?? true (VCons ?? true (VCons ?? true (VCons ? (S (S (S (S (S (S (S (S Z)))))))) false l)))). 109 interpretation "F8" 'f4 l = (VCons ?? true (VCons ?? true (VCons ?? true (VCons ? (S (S (S (S (S (S (S (S Z)))))))) true l)))). 110 111 interpretation "zero16" 'zero4 l = (VCons ?? false (VCons ?? false (VCons ?? false (VCons ? (S (S (S (S (S (S (S (S (S (S (S (S Z)))))))))))) false l)))). 112 interpretation "one16" 'one4 l = (VCons ?? false (VCons ?? false (VCons ?? false (VCons ? (S (S (S (S (S (S (S (S (S (S (S (S Z)))))))))))) true l)))). 113 interpretation "two16" 'two4 l = (VCons ?? false (VCons ?? false (VCons ?? true (VCons ? (S (S (S (S (S (S (S (S (S (S (S (S Z)))))))))))) false l)))). 114 interpretation "three16" 'three4 l = (VCons ?? false (VCons ?? false (VCons ?? true (VCons ? (S (S (S (S (S (S (S (S (S (S (S (S Z)))))))))))) true l)))). 115 interpretation "four16" 'four4 l = (VCons ?? false (VCons ?? true (VCons ?? false (VCons ? (S (S (S (S (S (S (S (S (S (S (S (S Z)))))))))))) false l)))). 116 interpretation "five16" 'five4 l = (VCons ?? false (VCons ?? true (VCons ?? false (VCons ? (S (S (S (S (S (S (S (S (S (S (S (S Z)))))))))))) true l)))). 117 interpretation "six16" 'six4 l = (VCons ?? false (VCons ?? true (VCons ?? true (VCons ? (S (S (S (S (S (S (S (S (S (S (S (S Z)))))))))))) false l)))). 118 interpretation "seven16" 'seven4 l = (VCons ?? false (VCons ?? true (VCons ?? true (VCons ? (S (S (S (S (S (S (S (S (S (S (S (S Z)))))))))))) true l)))). 119 interpretation "eight16" 'eight4 l = (VCons ?? true (VCons ?? false (VCons ?? false (VCons ? (S (S (S (S (S (S (S (S (S (S (S (S Z)))))))))))) false l)))). 120 interpretation "nine16" 'nine4 l = (VCons ?? true (VCons ?? false (VCons ?? false (VCons ? (S (S (S (S (S (S (S (S (S (S (S (S Z)))))))))))) true l)))). 121 interpretation "A16" 'a4 l = (VCons ?? true (VCons ?? false (VCons ?? true (VCons ? (S (S (S (S (S (S (S (S (S (S (S (S Z)))))))))))) false l)))). 122 interpretation "B16" 'b4 l = (VCons ?? true (VCons ?? false (VCons ?? true (VCons ? (S (S (S (S (S (S (S (S (S (S (S (S Z)))))))))))) true l)))). 123 interpretation "C16" 'c4 l = (VCons ?? true (VCons ?? true (VCons ?? false (VCons ? (S (S (S (S (S (S (S (S (S (S (S (S Z)))))))))))) false l)))). 124 interpretation "D16" 'd4 l = (VCons ?? true (VCons ?? true (VCons ?? false (VCons ? (S (S (S (S (S (S (S (S (S (S (S (S Z)))))))))))) true l)))). 125 interpretation "E16" 'e4 l = (VCons ?? true (VCons ?? true (VCons ?? true (VCons ? (S (S (S (S (S (S (S (S (S (S (S (S Z)))))))))))) false l)))). 126 interpretation "F16" 'f4 l = (VCons ?? true (VCons ?? true (VCons ?? true (VCons ? (S (S (S (S (S (S (S (S (S (S (S (S Z)))))))))))) true l)))). 127 128 notation < "…" with precedence 90 for @{ 'hide }. 129 interpretation "[[relative]]" 'hide = (VCons ?? relative (VEmpty ?)). 48 130 49 131 nlemma xoo: 50 (let testfinal ≝ testfinal in 51 is_JZ 52 (first … (first … (fetch (code_memory testfinal) (program_counter testfinal)))) 53 ) 54 = zero eight. 132 execute_trace one_hundred_and_twenty_eight teststatus = 133 execute_trace four teststatus. 55 134 nnormalize in ⊢ (??%?); 56 57 *) 58 135 (* nnormalize in ⊢ (???%); 136 @. 137 nqed. 59 138 60 139 nlemma xoo: program_counter testfinal = program_counter testfinal. … … 63 142 @. 64 143 nqed. 144 *)
Note: See TracChangeset
for help on using the changeset viewer.