the next generation of the in-browser educational proof assistant
switch to zora
+146
-128
+4
-2
package.json
+4
-2
package.json
···
12
12
"res:clean": "rescript clean",
13
13
"res:dev": "rescript -w",
14
14
"res:format": "rescript format -all",
15
-
"test": "retest tests/*.mjs"
15
+
"test": "onchange --initial '{tests,src}/*.mjs' -- pta 'tests/*.mjs'"
16
16
},
17
17
"dependencies": {
18
18
"@rescript/react": "^0.13.1",
···
21
21
"rescript": "^11.1.4"
22
22
},
23
23
"devDependencies": {
24
+
"@dusty-phillips/rescript-zora": "^5.0.1",
24
25
"@eslint/js": "^9.25.0",
25
26
"@rescript/core": "^1.6.1",
26
27
"@rescript/std": "^11.1.4",
···
31
32
"eslint-plugin-react-hooks": "^5.2.0",
32
33
"eslint-plugin-react-refresh": "^0.4.19",
33
34
"globals": "^16.0.0",
34
-
"rescript-test": "^7.0.1",
35
+
"onchange": "^7.1.0",
36
+
"pta": "^1.3.0",
35
37
"typescript": "~5.8.3",
36
38
"typescript-eslint": "^8.30.1",
37
39
"vite": "^6.3.5"
+1
-1
rescript.json
+1
-1
rescript.json
+89
-76
tests/SExpTest.mjs
+89
-76
tests/SExpTest.mjs
···
1
1
// Generated by ReScript, PLEASE EDIT WITH CARE
2
2
3
3
import * as SExp from "../src/SExp.mjs";
4
-
import * as Test from "rescript-test/src/Test.mjs";
4
+
import * as Zora from "zora";
5
5
import * as TestUtil from "./TestUtil.mjs";
6
6
7
-
function intEqual(message, a, b) {
8
-
Test.assertion(message, "Int equals", (function (a, b) {
9
-
return a === b;
10
-
}), a, b);
11
-
}
12
-
13
7
var Util = TestUtil.MakeTerm(SExp);
14
8
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);
9
+
Zora.test("parse symbol", (function (t) {
10
+
t.test("single char", (function (t) {
11
+
Util.testParse(t, "x", {
12
+
TAG: "Symbol",
13
+
name: "x"
14
+
}, undefined);
15
+
}));
16
+
t.test("multi char", (function (t) {
17
+
Util.testParse(t, "xyz", {
18
+
TAG: "Symbol",
19
+
name: "xyz"
20
+
}, undefined);
21
+
}));
24
22
}));
25
23
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);
24
+
Zora.test("parse var", (function (t) {
25
+
t.test("single digit", (function (t) {
26
+
Util.testParse(t, "\\1", {
27
+
TAG: "Var",
28
+
idx: 1
29
+
}, undefined);
30
+
}));
31
+
t.test("multi digit", (function (t) {
32
+
Util.testParse(t, "\\234", {
33
+
TAG: "Var",
34
+
idx: 234
35
+
}, undefined);
36
+
}));
35
37
}));
36
38
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);
39
+
Zora.test("parse schematic", (function (t) {
40
+
t.test("empty allowed", (function (t) {
41
+
Util.testParse(t, "?1()", {
42
+
TAG: "Schematic",
43
+
schematic: 1,
44
+
allowed: []
45
+
}, undefined);
46
+
}));
47
+
t.test("one allowed", (function (t) {
48
+
Util.testParse(t, "?1(\\1)", {
49
+
TAG: "Schematic",
50
+
schematic: 1,
51
+
allowed: [1]
52
+
}, undefined);
53
+
}));
54
+
t.test("multiple allowed", (function (t) {
55
+
Util.testParse(t, "?1(\\1 \\23 \\4)", {
56
+
TAG: "Schematic",
57
+
schematic: 1,
58
+
allowed: [
59
+
1,
60
+
2,
61
+
4
62
+
]
63
+
}, undefined);
64
+
}));
57
65
}));
58
66
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);
67
+
Zora.test("parse compound", (function (t) {
68
+
t.test("unit", (function (t) {
69
+
Util.testParse(t, "()", {
70
+
TAG: "Compound",
71
+
subexps: []
72
+
}, undefined);
73
+
}));
74
+
t.test("single", (function (t) {
75
+
Util.testParse(t, "(a)", {
76
+
TAG: "Compound",
77
+
subexps: [{
78
+
TAG: "Symbol",
79
+
name: "a"
80
+
}]
81
+
}, undefined);
82
+
}));
83
+
t.test("multiple", (function (t) {
84
+
Util.testParse(t, "(a \\1 ?1())", {
85
+
TAG: "Compound",
86
+
subexps: [
87
+
{
88
+
TAG: "Symbol",
89
+
name: "a"
90
+
},
91
+
{
92
+
TAG: "Var",
93
+
idx: 1
94
+
},
95
+
{
96
+
TAG: "Schematic",
97
+
schematic: 1,
98
+
allowed: []
99
+
}
100
+
]
101
+
}, undefined);
102
+
}));
89
103
}));
90
104
91
105
export {
92
-
intEqual ,
93
106
Util ,
94
107
}
95
108
/* Util Not a pure module */
+26
-23
tests/SExpTest.res
+26
-23
tests/SExpTest.res
···
1
-
open Test
1
+
open Zora
2
2
open SExp
3
3
4
-
let intEqual = (~message=?, a: int, b: int) =>
5
-
assertion(~message?, ~operator="Int equals", (a, b) => a === b, a, b)
6
-
7
4
module Util = TestUtil.MakeTerm(SExp)
8
5
9
-
test("parse symbol", () => {
10
-
Util.testParse("x", Symbol({name: "x"}))
11
-
Util.testParse("xyz", Symbol({name: "xyz"}))
6
+
zoraBlock("parse symbol", t => {
7
+
t->block("single char", t => t->Util.testParse("x", Symbol({name: "x"})))
8
+
t->block("multi char", t => t->Util.testParse("xyz", Symbol({name: "xyz"})))
12
9
})
13
10
14
-
test("parse var", () => {
15
-
Util.testParse("\\1", Var({idx: 1}))
16
-
Util.testParse("\\234", Var({idx: 234}))
11
+
zoraBlock("parse var", t => {
12
+
t->block("single digit", t => t->Util.testParse("\\1", Var({idx: 1})))
13
+
t->block("multi digit", t => t->Util.testParse("\\234", Var({idx: 234})))
17
14
})
18
15
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]}))
16
+
zoraBlock("parse schematic", t => {
17
+
t->block("empty allowed", t => t->Util.testParse("?1()", Schematic({schematic: 1, allowed: []})))
18
+
t->block("one allowed", t =>
19
+
t->Util.testParse("?1(\\1)", Schematic({schematic: 1, allowed: [1]}))
20
+
)
21
+
t->block("multiple allowed", t =>
22
+
t->Util.testParse("?1(\\1 \\23 \\4)", Schematic({schematic: 1, allowed: [1, 2, 4]}))
23
+
)
23
24
})
24
25
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
-
)
26
+
zoraBlock("parse compound", t => {
27
+
t->block("unit", t => t->Util.testParse("()", Compound({subexps: []})))
28
+
t->block("single", t => t->Util.testParse("(a)", Compound({subexps: [Symbol({name: "a"})]})))
29
+
t->block("multiple", t => {
30
+
t->Util.testParse(
31
+
"(a \\1 ?1())",
32
+
Compound({
33
+
subexps: [Symbol({name: "a"}), Var({idx: 1}), Schematic({schematic: 1, allowed: []})],
34
+
}),
35
+
)
36
+
})
34
37
})
+13
-16
tests/TestUtil.mjs
+13
-16
tests/TestUtil.mjs
···
1
1
// Generated by ReScript, PLEASE EDIT WITH CARE
2
2
3
-
import * as Test from "rescript-test/src/Test.mjs";
4
3
import * as Caml_option from "rescript/lib/es6/caml_option.js";
5
4
import * as Core__Option from "@rescript/core/src/Core__Option.mjs";
6
5
7
-
function assertEqual(a, b, message) {
8
-
Test.assertion(message, undefined, (function (a, b) {
9
-
return a === b;
10
-
}), a, b);
6
+
function stringifyExn(t) {
7
+
return Core__Option.getExn(JSON.stringify(t, undefined, 2), undefined);
11
8
}
12
9
13
10
function MakeTerm(Term) {
14
-
var termEquivalent = function (t1, t2, message) {
15
-
Test.assertion(message, undefined, Term.equivalent, t1, t2);
11
+
var termEquivalent = function (t, t1, t2, msg) {
12
+
t.ok(Term.equivalent(t1, t2), Core__Option.getOr(msg, stringifyExn(t1) + " equivalent to " + stringifyExn(t2)));
16
13
};
17
-
var testParse = function (input, t2, message) {
14
+
var testParse = function (t, input, t2, msg) {
18
15
var res = Term.parse(input, [], Caml_option.some(Term.makeGen()));
19
-
if (res.TAG !== "Ok") {
20
-
return Test.fail("parse failed: " + res._0, undefined);
16
+
if (res.TAG === "Ok") {
17
+
var res$1 = res._0;
18
+
t.equal(res$1[1], "", input + " input consumed");
19
+
t.equal(res$1[0], t2, msg !== undefined ? Caml_option.valFromOption(msg) : undefined);
20
+
return ;
21
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);
22
+
t.fail("parse failed: " + res._0);
26
23
};
27
24
return {
28
25
termEquivalent: termEquivalent,
···
31
28
}
32
29
33
30
export {
34
-
assertEqual ,
31
+
stringifyExn ,
35
32
MakeTerm ,
36
33
}
37
-
/* Test Not a pure module */
34
+
/* No side effect */
+13
-10
tests/TestUtil.res
+13
-10
tests/TestUtil.res
···
1
1
open Signatures
2
-
open Test
2
+
open Zora
3
3
4
-
let assertEqual = (a, b, ~message=?) => assertion((a, b) => a === b, a, b, ~message?)
4
+
let stringifyExn = (t: 'a) => JSON.stringifyAny(t, ~space=2)->Option.getExn
5
5
6
6
module MakeTerm = (Term: TERM) => {
7
-
let termEquivalent = (t1: Term.t, t2: Term.t, ~message=?) => {
8
-
assertion(Term.equivalent, t1, t2, ~message?)
7
+
let termEquivalent = (t: Zora.t, t1: Term.t, t2: Term.t, ~msg=?) => {
8
+
t->ok(
9
+
Term.equivalent(t1, t2),
10
+
~msg=msg->Option.getOr(`${stringifyExn(t1)} equivalent to ${stringifyExn(t2)}`),
11
+
)
9
12
}
10
-
let testParse = (input: string, t2: Term.t, ~message=?) => {
13
+
let testParse = (t: Zora.t, input: string, t2: Term.t, ~msg=?) => {
11
14
let res = Term.parse(input, ~scope=[], ~gen=Term.makeGen())
12
-
// i'm sure this could be handled better, but it works
13
15
switch res {
14
16
| 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)
17
+
t->equal(res->snd, "", ~msg=input ++ " input consumed")
18
+
// NOTE: we're checking for equality here, not equivalency
19
+
// error messages are better this way
20
+
t->equal(res->fst, t2, ~msg?)
18
21
}
19
-
| Error(msg) => fail(~message="parse failed: " ++ msg, ())
22
+
| Error(msg) => t->fail(~msg="parse failed: " ++ msg)
20
23
}
21
24
}
22
25
}