[646] | 1 | include "Search.ma". |
---|
[644] | 2 | include "Interpret.ma". |
---|
| 3 | include "Assembly.ma". |
---|
| 4 | |
---|
[664] | 5 | ndefinition steps ≝ twenty_four. |
---|
[644] | 6 | |
---|
| 7 | ndefinition testmem ≝ assembly_unlabelled_program test. |
---|
| 8 | ndefinition teststatus ≝ |
---|
| 9 | match testmem with |
---|
| 10 | [ Nothing ⇒ Nothing … |
---|
| 11 | | Just testmem ⇒ Just … (load (first … testmem) initialise_status)]. |
---|
| 12 | ndefinition testfinal ≝ |
---|
| 13 | match teststatus with |
---|
| 14 | [ Nothing ⇒ Nothing … |
---|
| 15 | | Just teststatus ⇒ Just … (execute steps teststatus)]. |
---|
| 16 | |
---|
| 17 | notation "'STATUS'" with precedence 90 for @{ 'status }. |
---|
| 18 | interpretation "status" 'status = (mk_Status ??????????). |
---|
| 19 | |
---|
| 20 | nlet rec execute_trace (n: Nat) (s: Status) on n: List ? ≝ |
---|
| 21 | match n with |
---|
| 22 | [ Z ⇒ [] |
---|
| 23 | | S o ⇒ |
---|
| 24 | first … (first … (fetch (code_memory s) (program_counter s))) :: execute_trace o (execute_1 s) |
---|
| 25 | ]. |
---|
| 26 | |
---|
| 27 | ndefinition testtrace ≝ |
---|
| 28 | match teststatus with |
---|
| 29 | [ Nothing ⇒ Nothing … |
---|
| 30 | | Just teststatus ⇒ Just … (execute_trace steps teststatus)]. |
---|
| 31 | |
---|
| 32 | interpretation "left" 'left x = (Left ?? x). |
---|
| 33 | interpretation "right" 'right x = (Right ?? x). |
---|
| 34 | |
---|
| 35 | notation < "'L' x" with precedence 70 for @{ 'left $x }. |
---|
| 36 | notation < "'R' x" with precedence 70 for @{ 'right $x }. |
---|
| 37 | |
---|
| 38 | notation < "𝟘" with precedence 90 for @{ 'zero }. |
---|
| 39 | notation < "𝟙" with precedence 90 for @{ 'one }. |
---|
| 40 | notation < "𝟚" with precedence 90 for @{ 'two }. |
---|
| 41 | notation < "𝟛" with precedence 90 for @{ 'three }. |
---|
| 42 | notation < "𝟜" with precedence 90 for @{ 'four }. |
---|
| 43 | notation < "𝟝" with precedence 90 for @{ 'five }. |
---|
| 44 | notation < "𝟞" with precedence 90 for @{ 'six }. |
---|
| 45 | notation < "𝟟" with precedence 90 for @{ 'seven }. |
---|
| 46 | notation < "𝟠" with precedence 90 for @{ 'eight }. |
---|
| 47 | notation < "𝟡" with precedence 90 for @{ 'nine }. |
---|
| 48 | notation < "𝔸" with precedence 90 for @{ 'a }. |
---|
| 49 | notation < "𝔹" with precedence 90 for @{ 'b }. |
---|
| 50 | notation < "∁" with precedence 90 for @{ 'c }. |
---|
| 51 | notation < "𝔻" with precedence 90 for @{ 'd }. |
---|
| 52 | notation < "𝔼" with precedence 90 for @{ 'e }. |
---|
| 53 | notation < "𝔽" with precedence 90 for @{ 'f }. |
---|
| 54 | |
---|
| 55 | |
---|
| 56 | interpretation "zero" 'zero = (VCons ?? false (VCons ?? false (VCons ?? false (VCons ?? false (VEmpty ?))))). |
---|
| 57 | interpretation "one" 'one = (VCons ?? false (VCons ?? false (VCons ?? false (VCons ?? true (VEmpty ?))))). |
---|
| 58 | interpretation "two" 'two = (VCons ?? false (VCons ?? false (VCons ?? true (VCons ?? false (VEmpty ?))))). |
---|
| 59 | interpretation "three" 'three = (VCons ?? false (VCons ?? false (VCons ?? true (VCons ?? true (VEmpty ?))))). |
---|
| 60 | interpretation "four" 'four = (VCons ?? false (VCons ?? true (VCons ?? false (VCons ?? false (VEmpty ?))))). |
---|
| 61 | interpretation "five" 'five = (VCons ?? false (VCons ?? true (VCons ?? false (VCons ?? true (VEmpty ?))))). |
---|
| 62 | interpretation "six" 'six = (VCons ?? false (VCons ?? true (VCons ?? true (VCons ?? false (VEmpty ?))))). |
---|
| 63 | interpretation "seven" 'seven = (VCons ?? false (VCons ?? true (VCons ?? true (VCons ?? true (VEmpty ?))))). |
---|
| 64 | interpretation "eight" 'eight = (VCons ?? true (VCons ?? false (VCons ?? false (VCons ?? false (VEmpty ?))))). |
---|
| 65 | interpretation "nine" 'nine = (VCons ?? true (VCons ?? false (VCons ?? false (VCons ?? true (VEmpty ?))))). |
---|
| 66 | interpretation "A" 'a = (VCons ?? true (VCons ?? false (VCons ?? true (VCons ?? false (VEmpty ?))))). |
---|
| 67 | interpretation "B" 'b = (VCons ?? true (VCons ?? false (VCons ?? true (VCons ?? true (VEmpty ?))))). |
---|
| 68 | interpretation "C" 'c = (VCons ?? true (VCons ?? true (VCons ?? false (VCons ?? false (VEmpty ?))))). |
---|
| 69 | interpretation "D" 'd = (VCons ?? true (VCons ?? true (VCons ?? false (VCons ?? true (VEmpty ?))))). |
---|
| 70 | interpretation "E" 'e = (VCons ?? true (VCons ?? true (VCons ?? true (VCons ?? false (VEmpty ?))))). |
---|
| 71 | interpretation "F" 'f = (VCons ?? true (VCons ?? true (VCons ?? true (VCons ?? true (VEmpty ?))))). |
---|
| 72 | |
---|
| 73 | notation < "𝟘l" with precedence 90 for @{ 'zero4 $l }. |
---|
| 74 | notation < "𝟙l" with precedence 90 for @{ 'one4 $l }. |
---|
| 75 | notation < "𝟚l" with precedence 90 for @{ 'two4 $l }. |
---|
| 76 | notation < "𝟛l" with precedence 90 for @{ 'three4 $l }. |
---|
| 77 | notation < "𝟜l" with precedence 90 for @{ 'four4 $l }. |
---|
| 78 | notation < "𝟝l" with precedence 90 for @{ 'five4 $l }. |
---|
| 79 | notation < "𝟞l" with precedence 90 for @{ 'six4 $l }. |
---|
| 80 | notation < "𝟟l" with precedence 90 for @{ 'seven4 $l }. |
---|
| 81 | notation < "𝟠l" with precedence 90 for @{ 'eight4 $l }. |
---|
| 82 | notation < "𝟡l" with precedence 90 for @{ 'nine4 $l }. |
---|
| 83 | notation < "𝔸l" with precedence 90 for @{ 'a4 $l }. |
---|
| 84 | notation < "𝔹l" with precedence 90 for @{ 'b4 $l }. |
---|
| 85 | notation < "∁l" with precedence 90 for @{ 'c4 $l }. |
---|
| 86 | notation < "𝔻l" with precedence 90 for @{ 'd4 $l }. |
---|
| 87 | notation < "𝔼l" with precedence 90 for @{ 'e4 $l }. |
---|
| 88 | notation < "𝔽l" with precedence 90 for @{ 'f4 $l }. |
---|
| 89 | |
---|
| 90 | interpretation "zero4" 'zero4 l = (VCons ?? false (VCons ?? false (VCons ?? false (VCons ? (S (S (S (S Z)))) false l)))). |
---|
| 91 | interpretation "one4" 'one4 l = (VCons ?? false (VCons ?? false (VCons ?? false (VCons ? (S (S (S (S Z)))) true l)))). |
---|
| 92 | interpretation "two4" 'two4 l = (VCons ?? false (VCons ?? false (VCons ?? true (VCons ? (S (S (S (S Z)))) false l)))). |
---|
| 93 | interpretation "three4" 'three4 l = (VCons ?? false (VCons ?? false (VCons ?? true (VCons ? (S (S (S (S Z)))) true l)))). |
---|
| 94 | interpretation "four4" 'four4 l = (VCons ?? false (VCons ?? true (VCons ?? false (VCons ? (S (S (S (S Z)))) false l)))). |
---|
| 95 | interpretation "five4" 'five4 l = (VCons ?? false (VCons ?? true (VCons ?? false (VCons ? (S (S (S (S Z)))) true l)))). |
---|
| 96 | interpretation "six4" 'six4 l = (VCons ?? false (VCons ?? true (VCons ?? true (VCons ? (S (S (S (S Z)))) false l)))). |
---|
| 97 | interpretation "seven4" 'seven4 l = (VCons ?? false (VCons ?? true (VCons ?? true (VCons ? (S (S (S (S Z)))) true l)))). |
---|
| 98 | interpretation "eight4" 'eight4 l = (VCons ?? true (VCons ?? false (VCons ?? false (VCons ? (S (S (S (S Z)))) false l)))). |
---|
| 99 | interpretation "nine4" 'nine4 l = (VCons ?? true (VCons ?? false (VCons ?? false (VCons ? (S (S (S (S Z)))) true l)))). |
---|
| 100 | interpretation "A4" 'a4 l = (VCons ?? true (VCons ?? false (VCons ?? true (VCons ? (S (S (S (S Z)))) false l)))). |
---|
| 101 | interpretation "B4" 'b4 l = (VCons ?? true (VCons ?? false (VCons ?? true (VCons ? (S (S (S (S Z)))) true l)))). |
---|
| 102 | interpretation "C4" 'c4 l = (VCons ?? true (VCons ?? true (VCons ?? false (VCons ? (S (S (S (S Z)))) false l)))). |
---|
| 103 | interpretation "D4" 'd4 l = (VCons ?? true (VCons ?? true (VCons ?? false (VCons ? (S (S (S (S Z)))) true l)))). |
---|
| 104 | interpretation "E4" 'e4 l = (VCons ?? true (VCons ?? true (VCons ?? true (VCons ? (S (S (S (S Z)))) false l)))). |
---|
| 105 | interpretation "F4" 'f4 l = (VCons ?? true (VCons ?? true (VCons ?? true (VCons ? (S (S (S (S Z)))) true l)))). |
---|
| 106 | |
---|
| 107 | interpretation "zero8" 'zero4 l = (VCons ?? false (VCons ?? false (VCons ?? false (VCons ? (S (S (S (S (S (S (S (S Z)))))))) false l)))). |
---|
| 108 | interpretation "one8" 'one4 l = (VCons ?? false (VCons ?? false (VCons ?? false (VCons ? (S (S (S (S (S (S (S (S Z)))))))) true l)))). |
---|
| 109 | interpretation "two8" 'two4 l = (VCons ?? false (VCons ?? false (VCons ?? true (VCons ? (S (S (S (S (S (S (S (S Z)))))))) false l)))). |
---|
| 110 | interpretation "three8" 'three4 l = (VCons ?? false (VCons ?? false (VCons ?? true (VCons ? (S (S (S (S (S (S (S (S Z)))))))) true l)))). |
---|
| 111 | interpretation "four8" 'four4 l = (VCons ?? false (VCons ?? true (VCons ?? false (VCons ? (S (S (S (S (S (S (S (S Z)))))))) false l)))). |
---|
| 112 | interpretation "five8" 'five4 l = (VCons ?? false (VCons ?? true (VCons ?? false (VCons ? (S (S (S (S (S (S (S (S Z)))))))) true l)))). |
---|
| 113 | interpretation "six8" 'six4 l = (VCons ?? false (VCons ?? true (VCons ?? true (VCons ? (S (S (S (S (S (S (S (S Z)))))))) false l)))). |
---|
| 114 | interpretation "seven8" 'seven4 l = (VCons ?? false (VCons ?? true (VCons ?? true (VCons ? (S (S (S (S (S (S (S (S Z)))))))) true l)))). |
---|
| 115 | interpretation "eight8" 'eight4 l = (VCons ?? true (VCons ?? false (VCons ?? false (VCons ? (S (S (S (S (S (S (S (S Z)))))))) false l)))). |
---|
| 116 | interpretation "nine8" 'nine4 l = (VCons ?? true (VCons ?? false (VCons ?? false (VCons ? (S (S (S (S (S (S (S (S Z)))))))) true l)))). |
---|
| 117 | interpretation "A8" 'a4 l = (VCons ?? true (VCons ?? false (VCons ?? true (VCons ? (S (S (S (S (S (S (S (S Z)))))))) false l)))). |
---|
| 118 | interpretation "B8" 'b4 l = (VCons ?? true (VCons ?? false (VCons ?? true (VCons ? (S (S (S (S (S (S (S (S Z)))))))) true l)))). |
---|
| 119 | interpretation "C8" 'c4 l = (VCons ?? true (VCons ?? true (VCons ?? false (VCons ? (S (S (S (S (S (S (S (S Z)))))))) false l)))). |
---|
| 120 | interpretation "D8" 'd4 l = (VCons ?? true (VCons ?? true (VCons ?? false (VCons ? (S (S (S (S (S (S (S (S Z)))))))) true l)))). |
---|
| 121 | interpretation "E8" 'e4 l = (VCons ?? true (VCons ?? true (VCons ?? true (VCons ? (S (S (S (S (S (S (S (S Z)))))))) false l)))). |
---|
| 122 | interpretation "F8" 'f4 l = (VCons ?? true (VCons ?? true (VCons ?? true (VCons ? (S (S (S (S (S (S (S (S Z)))))))) true l)))). |
---|
| 123 | |
---|
| 124 | 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)))). |
---|
| 125 | 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)))). |
---|
| 126 | 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)))). |
---|
| 127 | 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)))). |
---|
| 128 | 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)))). |
---|
| 129 | 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)))). |
---|
| 130 | 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)))). |
---|
| 131 | 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)))). |
---|
| 132 | 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)))). |
---|
| 133 | 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)))). |
---|
| 134 | 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)))). |
---|
| 135 | 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)))). |
---|
| 136 | 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)))). |
---|
| 137 | 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)))). |
---|
| 138 | 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)))). |
---|
| 139 | 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)))). |
---|
| 140 | |
---|
| 141 | notation < "…" with precedence 90 for @{ 'hide }. |
---|
| 142 | interpretation "[[relative]]" 'hide = (VCons ?? relative (VEmpty ?)). |
---|
| 143 | |
---|
| 144 | nlemma do_test: testtrace = testtrace. |
---|
| 145 | nnormalize in ⊢ (??%?); (* STOP HERE TO SEE THE TRACE *) |
---|
| 146 | nnormalize; |
---|
| 147 | @. |
---|
| 148 | nqed. |
---|