the next generation of the in-browser educational proof assistant
less dummy tests
+167
-7
+80
-4
tests/SExpTest.mjs
+80
-4
tests/SExpTest.mjs
···
1
1
// Generated by ReScript, PLEASE EDIT WITH CARE
2
2
3
+
import * as SExp from "../src/SExp.mjs";
3
4
import * as Test from "rescript-test/src/Test.mjs";
5
+
import * as TestUtil from "./TestUtil.mjs";
4
6
5
7
function intEqual(message, a, b) {
6
8
Test.assertion(message, "Int equals", (function (a, b) {
···
8
10
}), a, b);
9
11
}
10
12
11
-
Test.test("add", (function () {
12
-
intEqual(undefined, 2, 2);
13
-
intEqual("1 + 2 === 3", 3, 3);
13
+
var Util = TestUtil.MakeTerm(SExp);
14
+
15
+
Test.test("parse symbol", (function () {
16
+
Util.testParse("x", {
17
+
TAG: "Symbol",
18
+
name: "x"
19
+
}, undefined);
20
+
Util.testParse("xyz", {
21
+
TAG: "Symbol",
22
+
name: "xyz"
23
+
}, undefined);
24
+
}));
25
+
26
+
Test.test("parse var", (function () {
27
+
Util.testParse("\\1", {
28
+
TAG: "Var",
29
+
idx: 1
30
+
}, undefined);
31
+
Util.testParse("\\234", {
32
+
TAG: "Var",
33
+
idx: 234
34
+
}, undefined);
35
+
}));
36
+
37
+
Test.test("parse schematic", (function () {
38
+
Util.testParse("?1()", {
39
+
TAG: "Schematic",
40
+
schematic: 1,
41
+
allowed: []
42
+
}, undefined);
43
+
Util.testParse("?1(\\1)", {
44
+
TAG: "Schematic",
45
+
schematic: 1,
46
+
allowed: [1]
47
+
}, undefined);
48
+
Util.testParse("?1(\\1 \\23 \\4)", {
49
+
TAG: "Schematic",
50
+
schematic: 1,
51
+
allowed: [
52
+
1,
53
+
23,
54
+
4
55
+
]
56
+
}, undefined);
57
+
}));
58
+
59
+
Test.test("parse compound", (function () {
60
+
Util.testParse("()", {
61
+
TAG: "Compound",
62
+
subexps: []
63
+
}, undefined);
64
+
Util.testParse("(a)", {
65
+
TAG: "Compound",
66
+
subexps: [{
67
+
TAG: "Symbol",
68
+
name: "a"
69
+
}]
70
+
}, undefined);
71
+
Util.testParse("(a \\1 ?1())", {
72
+
TAG: "Compound",
73
+
subexps: [
74
+
{
75
+
TAG: "Symbol",
76
+
name: "a"
77
+
},
78
+
{
79
+
TAG: "Var",
80
+
idx: 1
81
+
},
82
+
{
83
+
TAG: "Schematic",
84
+
schematic: 1,
85
+
allowed: []
86
+
}
87
+
]
88
+
}, undefined);
14
89
}));
15
90
16
91
export {
17
92
intEqual ,
93
+
Util ,
18
94
}
19
-
/* Not a pure module */
95
+
/* Util Not a pure module */
+28
-3
tests/SExpTest.res
+28
-3
tests/SExpTest.res
···
1
1
open Test
2
+
open SExp
2
3
3
4
let intEqual = (~message=?, a: int, b: int) =>
4
5
assertion(~message?, ~operator="Int equals", (a, b) => a === b, a, b)
5
6
6
-
test("add", () => {
7
-
intEqual(1 + 1, 2)
8
-
intEqual(~message="1 + 2 === 3", 1 + 2, 3)
7
+
module Util = TestUtil.MakeTerm(SExp)
8
+
9
+
test("parse symbol", () => {
10
+
Util.testParse("x", Symbol({name: "x"}))
11
+
Util.testParse("xyz", Symbol({name: "xyz"}))
12
+
})
13
+
14
+
test("parse var", () => {
15
+
Util.testParse("\\1", Var({idx: 1}))
16
+
Util.testParse("\\234", Var({idx: 234}))
17
+
})
18
+
19
+
test("parse schematic", () => {
20
+
Util.testParse("?1()", Schematic({schematic: 1, allowed: []}))
21
+
Util.testParse("?1(\\1)", Schematic({schematic: 1, allowed: [1]}))
22
+
Util.testParse("?1(\\1 \\23 \\4)", Schematic({schematic: 1, allowed: [1, 23, 4]}))
23
+
})
24
+
25
+
test("parse compound", () => {
26
+
Util.testParse("()", Compound({subexps: []}))
27
+
Util.testParse("(a)", Compound({subexps: [Symbol({name: "a"})]}))
28
+
Util.testParse(
29
+
"(a \\1 ?1())",
30
+
Compound({
31
+
subexps: [Symbol({name: "a"}), Var({idx: 1}), Schematic({schematic: 1, allowed: []})],
32
+
}),
33
+
)
9
34
})
+37
tests/TestUtil.mjs
+37
tests/TestUtil.mjs
···
1
+
// Generated by ReScript, PLEASE EDIT WITH CARE
2
+
3
+
import * as Test from "rescript-test/src/Test.mjs";
4
+
import * as Caml_option from "rescript/lib/es6/caml_option.js";
5
+
import * as Core__Option from "@rescript/core/src/Core__Option.mjs";
6
+
7
+
function assertEqual(a, b, message) {
8
+
Test.assertion(message, undefined, (function (a, b) {
9
+
return a === b;
10
+
}), a, b);
11
+
}
12
+
13
+
function MakeTerm(Term) {
14
+
var termEquivalent = function (t1, t2, message) {
15
+
Test.assertion(message, undefined, Term.equivalent, t1, t2);
16
+
};
17
+
var testParse = function (input, t2, message) {
18
+
var res = Term.parse(input, [], Caml_option.some(Term.makeGen()));
19
+
if (res.TAG !== "Ok") {
20
+
return Test.fail("parse failed: " + res._0, undefined);
21
+
}
22
+
var res$1 = res._0;
23
+
assertEqual(res$1[1], "", input + " input consumed");
24
+
var message$1 = Core__Option.getOr(message, input + " equals expectation");
25
+
termEquivalent(res$1[0], t2, message$1);
26
+
};
27
+
return {
28
+
termEquivalent: termEquivalent,
29
+
testParse: testParse
30
+
};
31
+
}
32
+
33
+
export {
34
+
assertEqual ,
35
+
MakeTerm ,
36
+
}
37
+
/* Test Not a pure module */
+22
tests/TestUtil.res
+22
tests/TestUtil.res
···
1
+
open Signatures
2
+
open Test
3
+
4
+
let assertEqual = (a, b, ~message=?) => assertion((a, b) => a === b, a, b, ~message?)
5
+
6
+
module MakeTerm = (Term: TERM) => {
7
+
let termEquivalent = (t1: Term.t, t2: Term.t, ~message=?) => {
8
+
assertion(Term.equivalent, t1, t2, ~message?)
9
+
}
10
+
let testParse = (input: string, t2: Term.t, ~message=?) => {
11
+
let res = Term.parse(input, ~scope=[], ~gen=Term.makeGen())
12
+
// i'm sure this could be handled better, but it works
13
+
switch res {
14
+
| Ok(res) => {
15
+
assertEqual(res->snd, "", ~message=input ++ " input consumed")
16
+
let message = message->Option.getOr(input ++ " equals expectation")
17
+
termEquivalent(res->fst, t2, ~message)
18
+
}
19
+
| Error(msg) => fail(~message="parse failed: " ++ msg, ())
20
+
}
21
+
}
22
+
}