source: Deliverables/D4.1/Demo-March-2011/matita/DoTest.ma @ 664

Last change on this file since 664 was 664, checked in by mulligan, 9 years ago

Changed output of Intel HEX files so we no longer have those gargantuan blocks of zeroes at the end.

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