source: Deliverables/D4.1/Matita/DoTest.ma @ 374

Last change on this file since 374 was 374, checked in by sacerdot, 9 years ago

1) notation for cast fixed
2) ambiguity reduced: Empty => VEmpty, Cons => VCons
3) DoTest? modified to pretty-print the execution trace.

This should make debugging easier.

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