the next generation of the in-browser educational proof assistant
rename string term -> string atom
+274
-120
+2
-2
src/SExp.res
+2
-2
src/SExp.res
···
1
1
module SymbolAtom: SExpFunc.ATOM with type t = string = {
2
2
type t = string
3
3
type subst = Map.t<int, string>
4
-
let unify = (a, b) =>
4
+
let unify = (a, b, ~gen as _=?) =>
5
5
if a == b {
6
6
Seq.once(Map.make())
7
7
} else {
···
18
18
let lowerVar = _ => ""
19
19
let lowerSchematic = (_, _) => ""
20
20
let ghost = ""
21
-
let substDeBruijn = (name, _, ~from as _) => name
21
+
let substDeBruijn = (name, _, ~from as _=?) => name
22
22
let unifiesWithAnything = _ => false
23
23
let upshift = (t, _, ~from as _=?) => t
24
24
}
+2
-2
src/SExpFunc.res
+2
-2
src/SExpFunc.res
···
1
1
module type ATOM = {
2
2
type t
3
3
type subst = Map.t<int, t>
4
-
let unify: (t, t) => Seq.t<subst>
4
+
let unify: (t, t, ~gen: ref<int>=?) => Seq.t<subst>
5
5
let prettyPrint: (t, ~scope: array<string>) => string
6
6
let parse: (string, ~scope: array<string>, ~gen: ref<int>=?) => result<(t, string), string>
7
7
let substitute: (t, subst) => t
···
10
10
let lowerVar: int => t
11
11
let lowerSchematic: (int, array<int>) => t
12
12
let ghost: t
13
-
let substDeBruijn: (t, array<t>, ~from: int) => t
13
+
let substDeBruijn: (t, array<t>, ~from: int=?) => t
14
14
let unifiesWithAnything: t => bool
15
15
}
16
16
+2
-2
src/Scratch.res
+2
-2
src/Scratch.res
···
47
47
StringSExp,
48
48
StringSExp,
49
49
MethodView.DerivationView(StringSExp, StringSExp),
50
-
MethodView.LemmaView(StringSExp, StringSExp, StringTermJView),
50
+
MethodView.LemmaView(StringSExp, StringSExp, StringSExpJView),
51
51
)
52
52
module DLEStrView = MethodView.CombineMethodView(
53
53
StringSExp,
···
56
56
MethodView.EliminationView(StringSExp, StringSExp),
57
57
)
58
58
module TheoremStr = Editable.TextArea(
59
-
Theorem.Make(StringSExp, StringSExp, StringTermJView, DLEStrView),
59
+
Theorem.Make(StringSExp, StringSExp, StringSExpJView, DLEStrView),
60
60
)
+10
src/StringAtom.resi
+10
src/StringAtom.resi
+1
src/StringAtomView.resi
+1
src/StringAtomView.resi
···
1
+
include SExpViewFunc.ATOM_VIEW with module Atom := StringAtom
+6
-6
src/StringAxiomSet.res
+6
-6
src/StringAxiomSet.res
···
2
2
3
3
module Term = StringSExp
4
4
module Judgment = StringSExp
5
-
module JudgmentView = StringTermJView
5
+
module JudgmentView = StringSExpJView
6
6
7
7
module Rule = Rule.Make(Term, Judgment)
8
8
module RuleView = RuleView.Make(Term, Judgment, JudgmentView)
···
38
38
}
39
39
40
40
open StringSExp
41
-
let destructure = (r: Judgment.t): (StringTerm.t, string) =>
41
+
let destructure = (r: Judgment.t): (StringAtom.t, string) =>
42
42
switch r {
43
43
| Compound({subexps: [Atom(StringS(s)), Atom(ConstS(name))]}) => (s, name)
44
44
| _ => throw(Util.Unreachable("expected valid induction rule"))
45
45
}
46
-
let destructureOpt = (r: Judgment.t): option<(StringTerm.t, string)> =>
46
+
let destructureOpt = (r: Judgment.t): option<(StringAtom.t, string)> =>
47
47
switch r {
48
48
| Compound({subexps: [Atom(StringS(s)), Atom(ConstS(name))]}) => Some((s, name))
49
49
| _ => None
···
88
88
let xIdx = vars->Array.findIndex(i => i == x)
89
89
let aIdx = vars->Array.findIndex(i => i == a)
90
90
let bIdx = vars->Array.findIndex(i => i == b)
91
-
let surround = (t: StringTerm.t, aIdx: int, bIdx: int) => {
92
-
Array.concat(Array.concat([StringTerm.Var({idx: aIdx})], t), [StringTerm.Var({idx: bIdx})])
91
+
let surround = (t: StringAtom.t, aIdx: int, bIdx: int) => {
92
+
Array.concat(Array.concat([StringAtom.Var({idx: aIdx})], t), [StringAtom.Var({idx: bIdx})])
93
93
}
94
94
let lookupGroup = (name: string): option<int> =>
95
95
mentionedGroups->Array.findIndexOpt(g => name == g.name)
···
128
128
mentionedGroups->Array.flatMap(g => g.rules->Array.map(r => replaceJudgeRHS(r, 0))),
129
129
),
130
130
conclusion: structure(
131
-
surround([StringTerm.Var({idx: xIdx})], aIdx, bIdx)->StringS->Atom,
131
+
surround([StringAtom.Var({idx: xIdx})], aIdx, bIdx)->StringS->Atom,
132
132
Var({idx: 0}),
133
133
), // TODO: clean here
134
134
}
+19
-19
src/StringSExp.res
+19
-19
src/StringSExp.res
···
1
-
type stringAtom = StringS(StringTerm.t) | ConstS(SExp.Atom.t)
1
+
type stringSExpAtom = StringS(StringAtom.t) | ConstS(SExp.Atom.t)
2
2
3
-
module StringAtom: SExpFunc.ATOM with type t = stringAtom = {
4
-
type t = stringAtom
3
+
module StringSExpAtom: SExpFunc.ATOM with type t = stringSExpAtom = {
4
+
type t = stringSExpAtom
5
5
type subst = Map.t<int, t>
6
6
type gen = ref<int>
7
7
let parse = (s, ~scope, ~gen: option<gen>=?) => {
8
-
StringTerm.parse(s, ~scope, ~gen?)
8
+
StringAtom.parse(s, ~scope, ~gen?)
9
9
->Result.map(((r, rest)) => (StringS(r), rest))
10
10
->Util.Result.or(() =>
11
11
SExp.Atom.parse(s, ~scope, ~gen?)->Result.map(((r, rest)) => (ConstS(r), rest))
···
13
13
}
14
14
let prettyPrint = (s, ~scope) =>
15
15
switch s {
16
-
| StringS(s) => StringTerm.prettyPrint(s, ~scope)
16
+
| StringS(s) => StringAtom.prettyPrint(s, ~scope)
17
17
| ConstS(s) => SExp.Atom.prettyPrint(s, ~scope)
18
18
}
19
-
let unify = (s1, s2) =>
19
+
let unify = (s1, s2, ~gen=?) =>
20
20
switch (s1, s2) {
21
21
| (StringS(s1), StringS(s2)) =>
22
-
StringTerm.unify(s1, s2)->Seq.map(subst => subst->Util.mapMapValues(v => StringS(v)))
22
+
StringAtom.unify(s1, s2, ~gen?)->Seq.map(subst => subst->Util.mapMapValues(v => StringS(v)))
23
23
| (ConstS(s1), ConstS(s2)) =>
24
-
SExp.Atom.unify(s1, s2)->Seq.map(subst => subst->Util.mapMapValues(v => ConstS(v)))
24
+
SExp.Atom.unify(s1, s2, ~gen?)->Seq.map(subst => subst->Util.mapMapValues(v => ConstS(v)))
25
25
| (_, _) => Seq.empty
26
26
}
27
27
let substitute = (s, subst: subst) =>
···
30
30
let stringSubs = subst->Util.mapMapValues(v =>
31
31
switch v {
32
32
| StringS(s) => s
33
-
| _ => [StringTerm.Ghost]
33
+
| _ => [StringAtom.Ghost]
34
34
}
35
35
)
36
-
StringS(StringTerm.substitute(s, stringSubs))
36
+
StringS(StringAtom.substitute(s, stringSubs))
37
37
}
38
38
| ConstS(s) => ConstS(s)
39
39
}
40
40
let upshift = (s, amount: int, ~from=?) =>
41
41
switch s {
42
-
| StringS(s) => StringS(s->StringTerm.upshift(amount, ~from?))
42
+
| StringS(s) => StringS(s->StringAtom.upshift(amount, ~from?))
43
43
| ConstS(s) => ConstS(s)
44
44
}
45
-
let lowerVar = idx => StringS([StringTerm.Var({idx: idx})])
46
-
let lowerSchematic = (schematic, allowed) => StringS([StringTerm.Schematic({schematic, allowed})])
47
-
let ghost = StringS([StringTerm.Ghost])
48
-
let substDeBruijn = (s, substs: array<t>, ~from) =>
45
+
let lowerVar = idx => StringS([StringAtom.Var({idx: idx})])
46
+
let lowerSchematic = (schematic, allowed) => StringS([StringAtom.Schematic({schematic, allowed})])
47
+
let ghost = StringS([StringAtom.Ghost])
48
+
let substDeBruijn = (s, substs: array<t>, ~from=?) =>
49
49
switch s {
50
50
| StringS(s) => {
51
51
let stringSubs = substs->Array.map(v =>
52
52
switch v {
53
53
| StringS(s) => s
54
-
| _ => [StringTerm.String("AYAYAYSLKDJFLSKDJ")]
54
+
| _ => [StringAtom.String("AYAYAYSLKDJFLSKDJ")]
55
55
}
56
56
)
57
-
StringS(StringTerm.substDeBruijn(s, stringSubs, ~from))
57
+
StringS(StringAtom.substDeBruijn(s, stringSubs, ~from?))
58
58
}
59
59
| ConstS(s) => ConstS(s)
60
60
}
61
61
let unifiesWithAnything = s =>
62
62
switch s {
63
-
| StringS(s) => StringTerm.unifiesWithAnything(s)
63
+
| StringS(s) => StringAtom.unifiesWithAnything(s)
64
64
| ConstS(_) => false
65
65
}
66
66
}
67
67
68
-
include SExpFunc.Make(StringAtom)
68
+
include SExpFunc.Make(StringSExpAtom)
+4
-4
src/StringSExp.resi
+4
-4
src/StringSExp.resi
···
1
-
type stringAtom = StringS(StringTerm.t) | ConstS(SExp.Atom.t)
2
-
module StringAtom: SExpFunc.ATOM with type t = stringAtom
1
+
type stringSExpAtom = StringS(StringAtom.t) | ConstS(SExp.Atom.t)
2
+
module StringSExpAtom: SExpFunc.ATOM with type t = stringSExpAtom
3
3
4
4
type rec t =
5
-
| Atom(StringAtom.t)
5
+
| Atom(StringSExpAtom.t)
6
6
| Compound({subexps: array<t>})
7
7
| Var({idx: int})
8
8
| Schematic({schematic: int, allowed: array<int>})
···
14
14
and type schematic = int
15
15
and type subst = Map.t<int, t>
16
16
17
-
module Atom: SExpFunc.ATOM with type t := StringAtom.t
17
+
module Atom: SExpFunc.ATOM with type t := StringSExpAtom.t
18
18
let mapTerms: (t, t => t) => t
+17
src/StringSExpJView.res
+17
src/StringSExpJView.res
···
1
+
module StringAtomView: SExpViewFunc.ATOM_VIEW with module Atom := StringSExp.StringSExpAtom = {
2
+
type props = {name: StringSExp.StringSExpAtom.t, scope: array<string>}
3
+
let make = ({name, scope}: props) =>
4
+
switch name {
5
+
| StringSExp.StringS(name) => <StringAtomView name scope />
6
+
| StringSExp.ConstS(name) => <SExpView.ConstAtomView name scope />
7
+
}
8
+
}
9
+
10
+
module View = SExpViewFunc.Make(StringSExp.StringSExpAtom, StringAtomView, StringSExp)
11
+
12
+
module TermView = View
13
+
type props = {
14
+
judgment: StringSExp.t,
15
+
scope: array<string>,
16
+
}
17
+
let make = ({judgment, scope}) => View.make({term: judgment, scope})
+3
-1
src/StringTerm.res
src/StringAtom.res
+3
-1
src/StringTerm.res
src/StringAtom.res
···
503
503
acc.contents->Result.map(r => (r, str->String.sliceToEnd(~start=pos.contents)))
504
504
}
505
505
506
-
let ghostTerm = [Ghost]
506
+
let lowerSchematic = (schematic, allowed) => [Schematic({schematic, allowed})]
507
+
let lowerVar = idx => [Var({idx: idx})]
508
+
let ghost = [Ghost]
507
509
let unifiesWithAnything = t =>
508
510
t->Array.every(p =>
509
511
switch p {
-15
src/StringTerm.resi
-15
src/StringTerm.resi
···
1
-
type rec piece =
2
-
| String(string)
3
-
| Var({idx: int})
4
-
| Schematic({schematic: int, allowed: array<int>})
5
-
| Ghost
6
-
type t = array<piece>
7
-
type subst = Map.t<int, t>
8
-
type gen = ref<int>
9
-
10
-
include Signatures.TERM
11
-
with type t := t
12
-
and type meta = string
13
-
and type schematic = int
14
-
and type subst := subst
15
-
and type gen := gen
-17
src/StringTermJView.res
-17
src/StringTermJView.res
···
1
-
module StringAtomView: SExpViewFunc.ATOM_VIEW with module Atom := StringSExp.StringAtom = {
2
-
type props = {name: StringSExp.StringAtom.t, scope: array<string>}
3
-
let make = ({name, scope}: props) =>
4
-
switch name {
5
-
| StringSExp.StringS(term) => <StringTermView term scope />
6
-
| StringSExp.ConstS(name) => <SExpView.ConstAtomView name scope />
7
-
}
8
-
}
9
-
10
-
module View = SExpViewFunc.Make(StringSExp.StringAtom, StringAtomView, StringSExp)
11
-
12
-
module TermView = View
13
-
type props = {
14
-
judgment: StringSExp.t,
15
-
scope: array<string>,
16
-
}
17
-
let make = ({judgment, scope}) => View.make({term: judgment, scope})
src/StringTermJView.resi
src/StringSExpJView.resi
src/StringTermJView.resi
src/StringSExpJView.resi
+4
-4
src/StringTermView.res
src/StringAtomView.res
+4
-4
src/StringTermView.res
src/StringAtomView.res
···
1
-
type props = {term: StringTerm.t, scope: array<string>}
1
+
type props = {name: StringAtom.t, scope: array<string>}
2
2
type idx_props = {idx: int, scope: array<string>}
3
3
let viewVar = (props: idx_props) =>
4
4
switch props.scope[props.idx] {
···
28
28
29
29
module Piece = {
30
30
@react.component
31
-
let make = (~piece: StringTerm.piece, ~scope) =>
31
+
let make = (~piece: StringAtom.piece, ~scope) =>
32
32
switch piece {
33
33
| Var({idx}) => viewVar({idx, scope})
34
34
| String(s) => <span className="term-const"> {React.string(s)} </span>
···
51
51
}
52
52
53
53
@react.componentWithProps
54
-
let make = ({term, scope}) =>
54
+
let make = ({name, scope}) =>
55
55
<span className="term-compound">
56
56
{React.string("\"")}
57
-
{term
57
+
{name
58
58
->Array.mapWithIndex((piece, i) => {
59
59
let key = Int.toString(i)
60
60
<Piece piece scope key />
-1
src/StringTermView.resi
-1
src/StringTermView.resi
···
1
-
include Signatures.TERM_VIEW with module Term := StringTerm
+4
-4
tests/RuleTest.res
+4
-4
tests/RuleTest.res
···
42
42
// vars: [],
43
43
// premises: [],
44
44
// conclusion: StringSExp.Compound(
45
-
// [StringTerm.Var({idx: 0})],
46
-
// SExp.pAtom("p")->StringTermJudgment.ConstS->StringSExp.Atom,
45
+
// [StringAtom.Var({idx: 0})],
46
+
// SExp.pAtom("p")->StringAtomJudgment.ConstS->StringSExp.Atom,
47
47
// ),
48
48
// },
49
49
// ],
50
50
// conclusion: (
51
-
// [StringTerm.String("("), StringTerm.Var({idx: 0}), StringTerm.String(")")],
52
-
// SExp.pAtom("p")->StringTermJudgment.ConstS->StringSExp.Atom,
51
+
// [StringAtom.String("("), StringAtom.Var({idx: 0}), StringAtom.String(")")],
52
+
// SExp.pAtom("p")->StringAtomJudgment.ConstS->StringSExp.Atom,
53
53
// ),
54
54
// },
55
55
// )
+52
-43
tests/StringTermTest.res
+52
-43
tests/StringTermTest.res
···
1
1
open Zora
2
-
open StringTerm
3
2
4
-
module Util = TestUtil.MakeTerm(StringTerm)
3
+
module Util = TestUtil.MakeAtomTester(StringAtom)
4
+
module ParseUtil = Util.ParseTester
5
5
6
6
zoraBlock("parse", t => {
7
-
t->block("empty", t => t->Util.testParse(`""`, []))
7
+
t->block("empty", t => t->ParseUtil.testParse(`""`, []))
8
8
t->block("string literal", t => {
9
-
t->Util.testParse(`"x"`, [String("x")])
10
-
t->Util.testParse(`"xyz123"`, [String("xyz123")])
11
-
t->Util.testParse(`"123y"`, [String("123"), String("y")])
12
-
t->Util.testParse(`"\\"\\$\\?\\\\"`, [String("\""), String("$"), String("?"), String("\\")])
13
-
t->Util.testParse(
9
+
t->ParseUtil.testParse(`"x"`, [String("x")])
10
+
t->ParseUtil.testParse(`"xyz123"`, [String("xyz123")])
11
+
t->ParseUtil.testParse(`"123y"`, [String("123"), String("y")])
12
+
t->ParseUtil.testParse(
13
+
`"\\"\\$\\?\\\\"`,
14
+
[String("\""), String("$"), String("?"), String("\\")],
15
+
)
16
+
t->ParseUtil.testParse(
14
17
`"y(135ab!!)"`,
15
18
[String("y"), String("("), String("135"), String("ab"), String("!!"), String(")")],
16
19
)
17
-
t->Util.testParseFail(`foo`)
18
-
t->Util.testParseFail(`a b" c`)
20
+
t->ParseUtil.testParseFail(`foo`)
21
+
t->ParseUtil.testParseFail(`a b" c`)
19
22
})
20
23
t->block("variables", t => {
21
-
t->Util.testParse(`"$\\1"`, [Var({idx: 1})])
22
-
t->Util.testParse(`"$\\10"`, [Var({idx: 10})])
23
-
t->Util.testParse(`"$x"`, ~scope=["x"], [Var({idx: 0})])
24
-
t->Util.testParse(`"?1()"`, [Schematic({schematic: 1, allowed: []})])
25
-
t->Util.testParseFail(`"?1"`)
26
-
t->Util.testParse(`"?10()"`, [Schematic({schematic: 10, allowed: []})])
27
-
t->Util.testParse(`"?1(1 23 4)"`, [Schematic({schematic: 1, allowed: [1, 23, 4]})])
24
+
t->ParseUtil.testParse(`"$\\1"`, [Var({idx: 1})])
25
+
t->ParseUtil.testParse(`"$\\10"`, [Var({idx: 10})])
26
+
t->ParseUtil.testParse(`"$x"`, ~scope=["x"], [Var({idx: 0})])
27
+
t->ParseUtil.testParse(`"?1()"`, [Schematic({schematic: 1, allowed: []})])
28
+
t->ParseUtil.testParseFail(`"?1"`)
29
+
t->ParseUtil.testParse(`"?10()"`, [Schematic({schematic: 10, allowed: []})])
30
+
t->ParseUtil.testParse(`"?1(1 23 4)"`, [Schematic({schematic: 1, allowed: [1, 23, 4]})])
28
31
})
29
32
t->block("concat", t => {
30
-
t->Util.testParse(`"x y"`, [String("x"), String("y")])
31
-
t->Util.testParse(`"x y"`, [String("x"), String("y")])
32
-
t->Util.testParse(
33
+
t->ParseUtil.testParse(`"x y"`, [String("x"), String("y")])
34
+
t->ParseUtil.testParse(`"x y"`, [String("x"), String("y")])
35
+
t->ParseUtil.testParse(
33
36
`"x ?1(1 2 3) $\\1 $y"`,
34
37
~scope=["y"],
35
38
[String("x"), Schematic({schematic: 1, allowed: [1, 2, 3]}), Var({idx: 1}), Var({idx: 0})],
···
38
41
})
39
42
40
43
let parse = (input: string) =>
41
-
StringTerm.parse(input, ~scope=[], ~gen=StringTerm.makeGen())->Result.getExn->Pair.first
44
+
StringAtom.parse(input, ~scope=[], ~gen=Util.ParseWrapper.makeGen())->Result.getExn->Pair.first
45
+
46
+
module UnifyUtil = Util.UnifyTester
42
47
43
48
zoraBlock("unify", t => {
44
49
let a = parse(`"a"`)
···
46
51
let x = parse(`"?1()"`)
47
52
let y = parse(`"?2()"`)
48
53
t->block("ghost", t => {
49
-
t->Util.testUnifyFail(a, StringTerm.ghostTerm)
50
-
t->Util.testUnify(x, StringTerm.ghostTerm)
51
-
t->Util.testUnify([x, y, x]->Array.flat, StringTerm.ghostTerm)
54
+
t->UnifyUtil.testUnifyFail(a, StringAtom.ghost)
55
+
t->UnifyUtil.testUnify(x, StringAtom.ghost)
56
+
t->UnifyUtil.testUnify([x, y, x]->Array.flat, StringAtom.ghost)
52
57
})
53
58
t->block("schematics on at most one side", t => {
54
-
t->Util.testUnify(a, a, ~expect=[Map.make()])
55
-
t->Util.testUnify(x, a, ~expect=[Map.fromArray([(1, a)])])
56
-
t->Util.testUnify(a, x, ~expect=[Map.fromArray([(1, a)])])
59
+
t->UnifyUtil.testUnify(a, a, ~expect=[Map.make()])
60
+
t->UnifyUtil.testUnify(x, a, ~expect=[Map.fromArray([(1, a)])])
61
+
t->UnifyUtil.testUnify(a, x, ~expect=[Map.fromArray([(1, a)])])
57
62
58
63
let xy = parse(`"?1() ?2()"`)
59
64
let ab = parse(`"a b"`)
60
-
t->Util.testUnify(x, ab, ~expect=[Map.fromArray([(1, ab)])])
61
-
t->Util.testUnify(
65
+
t->UnifyUtil.testUnify(x, ab, ~expect=[Map.fromArray([(1, ab)])])
66
+
t->UnifyUtil.testUnify(
62
67
xy,
63
68
ab,
64
69
~expect=[
···
68
73
],
69
74
)
70
75
71
-
t->Util.testUnify(parse(`"?1() b ?2()"`), ab, ~expect=[Map.fromArray([(1, a), (2, [])])])
72
-
t->Util.testUnify(
76
+
t->UnifyUtil.testUnify(parse(`"?1() b ?2()"`), ab, ~expect=[Map.fromArray([(1, a), (2, [])])])
77
+
t->UnifyUtil.testUnify(
73
78
parse(`"?1() ?2() b"`),
74
79
ab,
75
80
~expect=[Map.fromArray([(1, []), (2, a)]), Map.fromArray([(1, a), (2, [])])],
76
81
)
77
-
t->Util.testUnify(
82
+
t->UnifyUtil.testUnify(
78
83
parse(`"a ?1() ?2()"`),
79
84
ab,
80
85
~expect=[Map.fromArray([(1, []), (2, b)]), Map.fromArray([(1, b), (2, [])])],
81
86
)
82
87
83
88
let xax = parse(`"?1() a ?1()"`)
84
-
t->Util.testUnify(xax, parse(`"a"`), ~expect=[Map.fromArray([(1, [])])])
85
-
t->Util.testUnify(xax, parse(`"a a a"`), ~expect=[Map.fromArray([(1, a)])])
86
-
t->Util.testUnify(xax, parse(`"a b a a b"`), ~expect=[Map.fromArray([(1, parse(`"a b"`))])])
89
+
t->UnifyUtil.testUnify(xax, parse(`"a"`), ~expect=[Map.fromArray([(1, [])])])
90
+
t->UnifyUtil.testUnify(xax, parse(`"a a a"`), ~expect=[Map.fromArray([(1, a)])])
91
+
t->UnifyUtil.testUnify(
92
+
xax,
93
+
parse(`"a b a a b"`),
94
+
~expect=[Map.fromArray([(1, parse(`"a b"`))])],
95
+
)
87
96
})
88
97
89
98
t->block("schematics appearing at most twice", t => {
90
-
t->Util.testUnify(x, x, ~expect=[Map.fromArray([(1, [])])])
91
-
t->Util.testUnify(x, y, ~expect=[Map.fromArray([(1, []), (2, [])])])
99
+
t->UnifyUtil.testUnify(x, x, ~expect=[Map.fromArray([(1, [])])])
100
+
t->UnifyUtil.testUnify(x, y, ~expect=[Map.fromArray([(1, []), (2, [])])])
92
101
93
-
t->Util.testUnify(a, parse(`"?1() a"`), ~expect=[Map.fromArray([(1, [])])])
94
-
t->Util.testUnify(
102
+
t->UnifyUtil.testUnify(a, parse(`"?1() a"`), ~expect=[Map.fromArray([(1, [])])])
103
+
t->UnifyUtil.testUnify(
95
104
parse(`"?1() a"`),
96
105
parse(`"a ?1()"`),
97
106
~expect=[
···
102
111
Map.fromArray([(1, parse(`"a a a a"`))]),
103
112
],
104
113
)
105
-
t->Util.testUnify(
114
+
t->UnifyUtil.testUnify(
106
115
parse(`"a ?1()"`),
107
116
parse(`"?2() b`),
108
117
~expect=[Map.fromArray([(1, b), (2, a)])],
109
118
)
110
-
t->Util.testUnify(
119
+
t->UnifyUtil.testUnify(
111
120
parse(`"a ?1() a"`),
112
121
parse(`"?2() b a"`),
113
122
~expect=[Map.fromArray([(1, b), (2, a)])],
114
123
)
115
-
t->Util.testUnify(
124
+
t->UnifyUtil.testUnify(
116
125
parse(`"b ?1() a"`),
117
126
parse(`"?2() a ?1()"`),
118
127
~expect=[Map.fromArray([(1, a), (2, b)]), Map.fromArray([(1, []), (2, b)])],
119
128
)
120
-
t->Util.testUnify(
129
+
t->UnifyUtil.testUnify(
121
130
parse(`"a b ?1() c ?2()"`),
122
131
parse(`"?2() c ?1() b a"`),
123
132
~expect=[Map.fromArray([(1, a), (2, parse(`"a b a"`))])],
+148
tests/TestUtil.res
+148
tests/TestUtil.res
···
3
3
4
4
let stringifyExn = (t: 'a) => JSON.stringifyAny(t, ~space=2)->Option.getExn
5
5
6
+
module type CAN_PARSE = {
7
+
type t
8
+
type meta
9
+
type gen
10
+
let parse: (string, ~scope: array<meta>, ~gen: gen=?) => result<(t, string), string>
11
+
let prettyPrint: (t, ~scope: array<meta>) => string
12
+
let makeGen: unit => gen
13
+
}
14
+
15
+
module MakeParseTester = (Subj: CAN_PARSE) => {
16
+
let testParse = (
17
+
t: Zora.t,
18
+
input: string,
19
+
expect: Subj.t,
20
+
~scope=[],
21
+
~msg=?,
22
+
~expectRemaining=?,
23
+
) => {
24
+
let res = Subj.parse(input, ~scope, ~gen=Subj.makeGen())
25
+
switch res {
26
+
| Ok((parsed, parsedRemaining)) => {
27
+
t->equal(
28
+
parsedRemaining,
29
+
expectRemaining->Option.getOr(""),
30
+
~msg=input ++ " input consumed",
31
+
)
32
+
// NOTE: we're checking for equality here, not equivalency
33
+
// error messages are better this way
34
+
t->equal(parsed, expect, ~msg?)
35
+
}
36
+
| Error(msg) => t->fail(~msg="parse failed: " ++ msg)
37
+
}
38
+
}
39
+
let testParseFail = (t: Zora.t, input: string, ~scope=[]) => {
40
+
let res = Subj.parse(input, ~scope, ~gen=Subj.makeGen())
41
+
switch res {
42
+
| Ok((p, remaining)) =>
43
+
t->fail(
44
+
~msg=`parse intended to fail, but succeeded: ${Subj.prettyPrint(
45
+
p,
46
+
~scope,
47
+
)}\nremaining: ${remaining}`,
48
+
)
49
+
| Error(_) => t->ok(true)
50
+
}
51
+
}
52
+
let testParsePrettyPrint = (t: Zora.t, input, expected, ~scope=[]) => {
53
+
let res = Subj.parse(input, ~scope=[], ~gen=Subj.makeGen())
54
+
55
+
switch res {
56
+
| Ok(res) => {
57
+
let result = Subj.prettyPrint(res->Pair.first, ~scope)
58
+
t->equal(result, expected, ~msg="prettyPrint output matches expected")
59
+
}
60
+
| Error(msg) => t->fail(~msg="parse failed: " ++ msg)
61
+
}
62
+
}
63
+
let parse = (t: Zora.t, input: string): Subj.t => {
64
+
let res = Subj.parse(input, ~scope=[], ~gen=Subj.makeGen())
65
+
switch res {
66
+
| Ok((term, "")) => term
67
+
| Ok((_, rest)) => {
68
+
t->fail(~msg="parse incomplete: " ++ rest)
69
+
throw(Util.Unreachable(""))
70
+
}
71
+
| Error(msg) => {
72
+
t->fail(~msg="parse failed: " ++ msg)
73
+
throw(Util.Unreachable(""))
74
+
}
75
+
}
76
+
}
77
+
}
78
+
79
+
module type CAN_UNIFY = {
80
+
type t
81
+
type subst
82
+
type gen
83
+
type meta
84
+
let unify: (t, t, ~gen: gen=?) => Seq.t<subst>
85
+
let substEqual: (subst, subst) => bool
86
+
let prettyPrintSubst: (subst, ~scope: array<meta>) => string
87
+
}
88
+
89
+
module MakeUnifyTester = (Subj: CAN_UNIFY) => {
90
+
let testUnify = (
91
+
t: Zora.t,
92
+
t1: Subj.t,
93
+
t2: Subj.t,
94
+
~expect: option<array<Subj.subst>>=?,
95
+
~msg=?,
96
+
) => {
97
+
let res = Subj.unify(t1, t2)->Seq.take(10)
98
+
switch expect {
99
+
| Some(expect) => {
100
+
let expect = Seq.fromArray(expect)
101
+
let noMatches =
102
+
expect
103
+
->Seq.filter(sub1 => Seq.find(res, sub2 => Subj.substEqual(sub1, sub2))->Option.isNone)
104
+
->Seq.map(t => Subj.prettyPrintSubst(t, ~scope=[]))
105
+
->Seq.toArray
106
+
let msg =
107
+
msg->Option.getOr("each substitution in `expect` should have a match in solutions")
108
+
t->equal(noMatches, [], ~msg)
109
+
}
110
+
| None => {
111
+
let msg = msg->Option.getOr("expect non-nil substitution sequence")
112
+
t->ok(res->Seq.head->Option.isSome, ~msg)
113
+
}
114
+
}
115
+
}
116
+
117
+
let testUnifyFail = (t: Zora.t, a: Subj.t, b: Subj.t, ~msg=?) => {
118
+
let res = Subj.unify(a, b)
119
+
if res->Seq.length != 0 {
120
+
t->fail(~msg="unification succeeded: " ++ stringifyExn(a) ++ " and " ++ stringifyExn(b))
121
+
} else {
122
+
t->ok(true, ~msg=msg->Option.getOr("unification failed"))
123
+
}
124
+
}
125
+
}
126
+
127
+
module MakeAtomTester = (Atom: SExpFunc.ATOM) => {
128
+
module ParseWrapper: CAN_PARSE
129
+
with type t = Atom.t
130
+
and type meta = string
131
+
and type gen = ref<int> = {
132
+
include Atom
133
+
type gen = ref<int>
134
+
type meta = string
135
+
let makeGen = () => ref(0)
136
+
}
137
+
module ParseTester = MakeParseTester(ParseWrapper)
138
+
module UnifyWrapper: CAN_UNIFY
139
+
with type t = Atom.t
140
+
and type meta = string
141
+
and type gen = ref<int>
142
+
and type subst = Atom.subst = {
143
+
include Atom
144
+
type meta = string
145
+
type gen = ref<int>
146
+
let prettyPrintSubst = (sub, ~scope) =>
147
+
Util.prettyPrintMap(sub, ~showV=t => prettyPrint(t, ~scope))
148
+
let substEqual = Util.mapEqual
149
+
}
150
+
module UnifyTester = MakeUnifyTester(UnifyWrapper)
151
+
}
152
+
153
+
// TODO: modularise in the same way as AtomTester
6
154
module MakeTerm = (Term: TERM) => {
7
155
let termEquivalent = (t: Zora.t, t1: Term.t, t2: Term.t, ~msg=?) => {
8
156
t->ok(