the next generation of the in-browser educational proof assistant
chore: solve warnings
+24
-23
+3
-3
rescript.json
+3
-3
rescript.json
···
9
9
"in-source": true
10
10
},
11
11
"suffix": ".mjs",
12
-
"bs-dependencies": [
12
+
"dependencies": [
13
13
"@rescript/core",
14
14
"@rescript/react",
15
15
"@jmagaram/rescript-seq"
16
16
],
17
-
"bs-dev-dependencies": ["@dusty-phillips/rescript-zora"],
18
-
"bsc-flags": ["-open RescriptCore"],
17
+
"dev-dependencies": ["@dusty-phillips/rescript-zora"],
18
+
"compiler-flags": ["-open RescriptCore"],
19
19
"jsx": { "version": 4 }
20
20
}
+3
-3
src/StringAxiomSet.res
+3
-3
src/StringAxiomSet.res
···
49
49
let (aIdx, bIdx, pIdx) = (aIdx + n, bIdx + n, pIdx + n)
50
50
let inductionHyps =
51
51
rule.premises
52
-
->Array.filter(r => r.conclusion->snd == Symbol({name: name}))
52
+
->Array.filter(r => r.conclusion->Pair.second == Symbol({name: name}))
53
53
->Array.map(r => replaceJudgeRHS(r, aIdx, bIdx, pIdx))
54
54
{
55
55
vars: rule.vars,
56
56
premises: rule.premises->Array.concat(inductionHyps),
57
-
conclusion: (surround(rule.conclusion->fst, aIdx, bIdx), Var({idx: pIdx})),
57
+
conclusion: (surround(rule.conclusion->Pair.first, aIdx, bIdx), Var({idx: pIdx})),
58
58
}
59
59
}
60
60
{
···
105
105
getBase(str)->Result.map(raw => {
106
106
let grouped: dict<array<Rule.t>> = Dict.make()
107
107
raw->Dict.forEach(rule =>
108
-
switch rule.conclusion->snd {
108
+
switch rule.conclusion->Pair.second {
109
109
| Symbol({name: a}) =>
110
110
switch grouped->Dict.get(a) {
111
111
| None => grouped->Dict.set(a, [rule])
+1
-1
src/StringTerm.res
+1
-1
src/StringTerm.res
···
40
40
}
41
41
)
42
42
let maxSchematicCount = (term: t) => {
43
-
schematicsCountsIn(term)->Belt.Map.Int.maximum->Option.map(snd)->Option.getOr(0)
43
+
schematicsCountsIn(term)->Belt.Map.Int.maximum->Option.map(Pair.second)->Option.getOr(0)
44
44
}
45
45
let reduce = t => t
46
46
let freeVarsIn = (term: t): Belt.Set.t<int, IntCmp.identity> =>
+9
-9
tests/HOTermTest.res
+9
-9
tests/HOTermTest.res
···
224
224
y,
225
225
~subst=emptySubst->substAdd(
226
226
0,
227
-
HOTerm.parse("(x. (r (fst x)))", ~scope=[])->Result.getExn->fst,
227
+
HOTerm.parse("(x. (r (fst x)))", ~scope=[])->Result.getExn->Pair.first,
228
228
),
229
229
)
230
230
})
···
236
236
y,
237
237
~subst=emptySubst->substAdd(
238
238
1,
239
-
HOTerm.parse("(x. x. (r (q \\0 \\1)))", ~scope=[])->Result.getExn->fst,
239
+
HOTerm.parse("(x. x. (r (q \\0 \\1)))", ~scope=[])->Result.getExn->Pair.first,
240
240
),
241
241
)
242
242
})
···
248
248
y,
249
249
~subst=emptySubst->substAdd(
250
250
1,
251
-
HOTerm.parse("(x. x. (r (q (snd \\0) \\1)))", ~scope=[])->Result.getExn->fst,
251
+
HOTerm.parse("(x. x. (r (q (snd \\0) \\1)))", ~scope=[])->Result.getExn->Pair.first,
252
252
),
253
253
)
254
254
})
···
294
294
~subst=emptySubst->substAdd(0, Symbol({name: "a", constructor: false})),
295
295
)
296
296
})
297
-
t->block("divergent", t => {
298
-
let divergent = "((x. x x) (x. x x))"
299
-
let a = "((x. ?0 x) (x. x x))"
297
+
t->block("divergent", _t => {
298
+
let _divergent = "((x. x x) (x. x x))"
299
+
let _a = "((x. ?0 x) (x. x x))"
300
300
// we don't care
301
301
// t->Util.testNotUnify(a, divergent)
302
302
})
···
343
343
t->Util.testUnifyFail(a, b)
344
344
t->testUnify(c, b, ~subst=emptySubst->substAdd(6, t->Util.parse("(x. S \\0)")))
345
345
})
346
-
t->block("tests from induction examples", t => {
347
-
let r = "((?0 \\0) (?1 \\0))"
348
-
let g = "(f \\0)"
346
+
t->block("tests from induction examples", _t => {
347
+
let _r = "((?0 \\0) (?1 \\0))"
348
+
let _g = "(f \\0)"
349
349
// what it's currently doing:
350
350
// 0 := (x. y. f x)
351
351
// 1 := doesn't matter
+4
-4
tests/RuleTest.res
+4
-4
tests/RuleTest.res
···
7
7
let res = RuleInst.parseInner(input, ~scope, ~gen=Term.makeGen())
8
8
switch res {
9
9
| Ok(res) => {
10
-
t->equal(res->snd, "", ~msg=input ++ " input consumed")
11
-
t->equal(res->fst, expect, ~msg?)
10
+
t->equal(res->Pair.second, "", ~msg=input ++ " input consumed")
11
+
t->equal(res->Pair.first, expect, ~msg?)
12
12
}
13
13
| Error(msg) => t->fail(~msg="parse failed: " ++ msg)
14
14
}
···
23
23
let res = RuleInst.parseTopLevel(input, ~scope, ~gen=Term.makeGen())
24
24
switch res {
25
25
| Ok(res) => {
26
-
t->equal(res->snd, "", ~msg=input ++ " input consumed")
27
-
t->equal(res->fst, expect, ~msg?)
26
+
t->equal(res->Pair.second, "", ~msg=input ++ " input consumed")
27
+
t->equal(res->Pair.first, expect, ~msg?)
28
28
}
29
29
| Error(msg) => t->fail(~msg="parse failed: " ++ msg)
30
30
}
+2
-1
tests/SExpTest.res
+2
-1
tests/SExpTest.res
···
40
40
})
41
41
})
42
42
43
-
let parse = (input: string) => SExp.parse(input, ~scope=[], ~gen=SExp.makeGen())->Result.getExn->fst
43
+
let parse = (input: string) =>
44
+
SExp.parse(input, ~scope=[], ~gen=SExp.makeGen())->Result.getExn->Pair.first
44
45
45
46
zoraBlock("unify var", t => {
46
47
let x = parse("x")
+1
-1
tests/StringTermTest.res
+1
-1
tests/StringTermTest.res
···
38
38
})
39
39
40
40
let parse = (input: string) =>
41
-
StringTerm.parse(input, ~scope=[], ~gen=StringTerm.makeGen())->Result.getExn->fst
41
+
StringTerm.parse(input, ~scope=[], ~gen=StringTerm.makeGen())->Result.getExn->Pair.first
42
42
43
43
zoraBlock("unify", t => {
44
44
let a = parse(`"a"`)
+1
-1
tests/TestUtil.res
+1
-1
tests/TestUtil.res
···
52
52
53
53
switch res {
54
54
| Ok(res) => {
55
-
let result = Term.prettyPrint(res->fst, ~scope)
55
+
let result = Term.prettyPrint(res->Pair.first, ~scope)
56
56
t->equal(result, expected, ~msg="prettyPrint output matches expected")
57
57
}
58
58
| Error(msg) => t->fail(~msg="parse failed: " ++ msg)