Skip to content

Commit 1639113

Browse files
jkingdondigama0
jkingdon
and
digama0
authored
Test disjoint (#58)
* Add disjoint1.mm test This is a simple test for enforcing disjoint variable constraints. * Add disjoint2.mm test This ends up testing various different kinds of checks. Most notably it does have some nesting in the test data which hopefully helps check that the verifier is recursing into nested syntaxes. * Add disjoint3.mm test This is for the case in which the check fails because the theorem being proved has two variables and does not have a needed disjoint variable constraint between them. * Add stillgood to disjoint2.mm This has fewer disjoint constraints than good but still enough to be allowable. Co-authored-by: Mario Carneiro <[email protected]> Co-authored-by: Mario Carneiro <[email protected]>
1 parent f1ff4b8 commit 1639113

File tree

9 files changed

+243
-0
lines changed

9 files changed

+243
-0
lines changed

‎tests/disjoint1.expected‎

Lines changed: 19 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,19 @@
1+
MM> READ "disjoint1.mm"
2+
Reading source file "disjoint1.mm"... 140 bytes
3+
140 bytes were read into the source buffer.
4+
The source has 9 statements; 1 are $a and 1 are $p.
5+
No errors were found. However, proofs were not checked. Type VERIFY PROOF *
6+
if you want to check them.
7+
MM> Continuous scrolling is now in effect.
8+
MM> 0 10% 20% 30% 40% 50% 60% 70% 80% 90% 100%
9+
..................................................
10+
?Error on line 10 of file "disjoint1.mm" at statement 9, label "bad", type
11+
"$p":
12+
xf xf ax-1 $.
13+
^^^^
14+
There is a disjoint variable ($d) violation at proof step 3. Assertion "ax-1"
15+
requires that variables "x" and "y" be disjoint. But "x" was substituted with
16+
"x" and "y" was substituted with "x". These substitutions have variable "x" in
17+
common.
18+
19+
All proofs in the database were verified.

‎tests/disjoint1.in‎

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1 @@
1+
verify proof *

‎tests/disjoint1.mm‎

Lines changed: 10 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,10 @@
1+
$c var formula |- $.
2+
$v x y $.
3+
xf $f formula x $.
4+
yf $f formula y $.
5+
${
6+
$d x y $.
7+
ax-1 $a |- x y $.
8+
$}
9+
bad $p |- x x $=
10+
xf xf ax-1 $.

‎tests/disjoint2.expected‎

Lines changed: 138 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,138 @@
1+
MM> READ "disjoint2.mm"
2+
Reading source file "disjoint2.mm"... 754 bytes
3+
754 bytes were read into the source buffer.
4+
The source has 33 statements; 2 are $a and 6 are $p.
5+
No errors were found. However, proofs were not checked. Type VERIFY PROOF *
6+
if you want to check them.
7+
MM> Continuous scrolling is now in effect.
8+
MM> 0 10% 20% 30% 40% 50% 60% 70% 80% 90% 100%
9+
..................
10+
?Error on line 15 of file "disjoint2.mm" at statement 12, label "verybad", type
11+
"$p":
12+
xf yf combo zf xf combo ax-1 $.
13+
^^^^
14+
There is a disjoint variable ($d) violation at proof step 7. Assertion "ax-1"
15+
requires that variables "x" and "y" be disjoint. But "x" was substituted with
16+
"( x y )" and "y" was substituted with "( z x )".
17+
Variables "x" and "z" do not have a disjoint variable requirement in the
18+
assertion being proved, "verybad".
19+
20+
?Error on line 15 of file "disjoint2.mm" at statement 12, label "verybad", type
21+
"$p":
22+
xf yf combo zf xf combo ax-1 $.
23+
^^^^
24+
There is a disjoint variable ($d) violation at proof step 7. Assertion "ax-1"
25+
requires that variables "x" and "y" be disjoint. But "x" was substituted with
26+
"( x y )" and "y" was substituted with "( z x )". These substitutions have
27+
variable "x" in common.
28+
29+
?Error on line 15 of file "disjoint2.mm" at statement 12, label "verybad", type
30+
"$p":
31+
xf yf combo zf xf combo ax-1 $.
32+
^^^^
33+
There is a disjoint variable ($d) violation at proof step 7. Assertion "ax-1"
34+
requires that variables "x" and "y" be disjoint. But "x" was substituted with
35+
"( x y )" and "y" was substituted with "( z x )".
36+
Variables "y" and "z" do not have a disjoint variable requirement in the
37+
assertion being proved, "verybad".
38+
39+
?Error on line 15 of file "disjoint2.mm" at statement 12, label "verybad", type
40+
"$p":
41+
xf yf combo zf xf combo ax-1 $.
42+
^^^^
43+
There is a disjoint variable ($d) violation at proof step 7. Assertion "ax-1"
44+
requires that variables "x" and "y" be disjoint. But "x" was substituted with
45+
"( x y )" and "y" was substituted with "( z x )".
46+
Variables "x" and "y" do not have a disjoint variable requirement in the
47+
assertion being proved, "verybad".
48+
....
49+
?Error on line 20 of file "disjoint2.mm" at statement 15, label "stillbad",
50+
type "$p":
51+
xf yf combo zf xf combo ax-1 $.
52+
^^^^
53+
There is a disjoint variable ($d) violation at proof step 7. Assertion "ax-1"
54+
requires that variables "x" and "y" be disjoint. But "x" was substituted with
55+
"( x y )" and "y" was substituted with "( z x )". These substitutions have
56+
variable "x" in common.
57+
...
58+
?Error on line 24 of file "disjoint2.mm" at statement 17, label "semigood",
59+
type "$p":
60+
xf yf combo zf wf combo ax-1 $.
61+
^^^^
62+
There is a disjoint variable ($d) violation at proof step 7. Assertion "ax-1"
63+
requires that variables "x" and "y" be disjoint. But "x" was substituted with
64+
"( x y )" and "y" was substituted with "( z w )".
65+
Variables "x" and "z" do not have a disjoint variable requirement in the
66+
assertion being proved, "semigood".
67+
68+
?Error on line 24 of file "disjoint2.mm" at statement 17, label "semigood",
69+
type "$p":
70+
xf yf combo zf wf combo ax-1 $.
71+
^^^^
72+
There is a disjoint variable ($d) violation at proof step 7. Assertion "ax-1"
73+
requires that variables "x" and "y" be disjoint. But "x" was substituted with
74+
"( x y )" and "y" was substituted with "( z w )".
75+
Variables "w" and "x" do not have a disjoint variable requirement in the
76+
assertion being proved, "semigood".
77+
78+
?Error on line 24 of file "disjoint2.mm" at statement 17, label "semigood",
79+
type "$p":
80+
xf yf combo zf wf combo ax-1 $.
81+
^^^^
82+
There is a disjoint variable ($d) violation at proof step 7. Assertion "ax-1"
83+
requires that variables "x" and "y" be disjoint. But "x" was substituted with
84+
"( x y )" and "y" was substituted with "( z w )".
85+
Variables "y" and "z" do not have a disjoint variable requirement in the
86+
assertion being proved, "semigood".
87+
88+
?Error on line 24 of file "disjoint2.mm" at statement 17, label "semigood",
89+
type "$p":
90+
xf yf combo zf wf combo ax-1 $.
91+
^^^^
92+
There is a disjoint variable ($d) violation at proof step 7. Assertion "ax-1"
93+
requires that variables "x" and "y" be disjoint. But "x" was substituted with
94+
"( x y )" and "y" was substituted with "( z w )".
95+
Variables "w" and "y" do not have a disjoint variable requirement in the
96+
assertion being proved, "semigood".
97+
......
98+
?Error on line 30 of file "disjoint2.mm" at statement 21, label "almostgood",
99+
type "$p":
100+
xf yf combo zf wf combo ax-1 $.
101+
^^^^
102+
There is a disjoint variable ($d) violation at proof step 7. Assertion "ax-1"
103+
requires that variables "x" and "y" be disjoint. But "x" was substituted with
104+
"( x y )" and "y" was substituted with "( z w )".
105+
Variables "x" and "z" do not have a disjoint variable requirement in the
106+
assertion being proved, "almostgood".
107+
108+
?Error on line 30 of file "disjoint2.mm" at statement 21, label "almostgood",
109+
type "$p":
110+
xf yf combo zf wf combo ax-1 $.
111+
^^^^
112+
There is a disjoint variable ($d) violation at proof step 7. Assertion "ax-1"
113+
requires that variables "x" and "y" be disjoint. But "x" was substituted with
114+
"( x y )" and "y" was substituted with "( z w )".
115+
Variables "w" and "x" do not have a disjoint variable requirement in the
116+
assertion being proved, "almostgood".
117+
118+
?Error on line 30 of file "disjoint2.mm" at statement 21, label "almostgood",
119+
type "$p":
120+
xf yf combo zf wf combo ax-1 $.
121+
^^^^
122+
There is a disjoint variable ($d) violation at proof step 7. Assertion "ax-1"
123+
requires that variables "x" and "y" be disjoint. But "x" was substituted with
124+
"( x y )" and "y" was substituted with "( z w )".
125+
Variables "y" and "z" do not have a disjoint variable requirement in the
126+
assertion being proved, "almostgood".
127+
128+
?Error on line 30 of file "disjoint2.mm" at statement 21, label "almostgood",
129+
type "$p":
130+
xf yf combo zf wf combo ax-1 $.
131+
^^^^
132+
There is a disjoint variable ($d) violation at proof step 7. Assertion "ax-1"
133+
requires that variables "x" and "y" be disjoint. But "x" was substituted with
134+
"( x y )" and "y" was substituted with "( z w )".
135+
Variables "w" and "y" do not have a disjoint variable requirement in the
136+
assertion being proved, "almostgood".
137+
...................
138+
All proofs in the database were verified.

‎tests/disjoint2.in‎

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1 @@
1+
verify proof *

‎tests/disjoint2.mm‎

Lines changed: 43 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,43 @@
1+
$c formula |- ( ) $.
2+
3+
$v x y z w $.
4+
xf $f formula x $.
5+
yf $f formula y $.
6+
zf $f formula z $.
7+
wf $f formula w $.
8+
combo $a formula ( x y ) $.
9+
${
10+
$d x y $.
11+
ax-1 $a |- ( x y ) $.
12+
$}
13+
14+
verybad $p |- ( ( x y ) ( z x ) ) $=
15+
xf yf combo zf xf combo ax-1 $.
16+
17+
${
18+
$d x y z $.
19+
stillbad $p |- ( ( x y ) ( z x ) ) $=
20+
xf yf combo zf xf combo ax-1 $.
21+
$}
22+
23+
semigood $p |- ( ( x y ) ( z w ) ) $=
24+
xf yf combo zf wf combo ax-1 $.
25+
26+
${
27+
$d x y $.
28+
$d z w $.
29+
almostgood $p |- ( ( x y ) ( z w ) ) $=
30+
xf yf combo zf wf combo ax-1 $.
31+
$}
32+
33+
${
34+
$d x y z w $.
35+
good $p |- ( ( x y ) ( z w ) ) $=
36+
xf yf combo zf wf combo ax-1 $.
37+
$}
38+
39+
${
40+
$d x z $. $d x w $. $d y z $. $d y w $.
41+
stillgood $p |- ( ( x y ) ( z w ) ) $=
42+
xf yf combo zf wf combo ax-1 $.
43+
$}

‎tests/disjoint3.expected‎

Lines changed: 20 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,20 @@
1+
MM> READ "disjoint3.mm"
2+
Reading source file "disjoint3.mm"... 140 bytes
3+
140 bytes were read into the source buffer.
4+
The source has 9 statements; 1 are $a and 1 are $p.
5+
No errors were found. However, proofs were not checked. Type VERIFY PROOF *
6+
if you want to check them.
7+
MM> Continuous scrolling is now in effect.
8+
MM> 0 10% 20% 30% 40% 50% 60% 70% 80% 90% 100%
9+
..................................................
10+
?Error on line 10 of file "disjoint3.mm" at statement 9, label "bad", type
11+
"$p":
12+
xf yf ax-1 $.
13+
^^^^
14+
There is a disjoint variable ($d) violation at proof step 3. Assertion "ax-1"
15+
requires that variables "x" and "y" be disjoint. But "x" was substituted with
16+
"x" and "y" was substituted with "y".
17+
Variables "x" and "y" do not have a disjoint variable requirement in the
18+
assertion being proved, "bad".
19+
20+
All proofs in the database were verified.

‎tests/disjoint3.in‎

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1 @@
1+
verify proof *

‎tests/disjoint3.mm‎

Lines changed: 10 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,10 @@
1+
$c var formula |- $.
2+
$v x y $.
3+
xf $f formula x $.
4+
yf $f formula y $.
5+
${
6+
$d x y $.
7+
ax-1 $a |- x y $.
8+
$}
9+
bad $p |- x y $=
10+
xf yf ax-1 $.

0 commit comments

Comments
 (0)