the next generation of the in-browser educational proof assistant
Merge branch 'main' of tangled.org:liamoc.net/holbert-ng
+478
-425
+1
-1
package.json
+1
-1
package.json
···
12
12
"res:clean": "rescript clean",
13
13
"res:dev": "rescript watch",
14
14
"res:format": "rescript format",
15
-
"test": "npm run res:build && pta 'tests/*.mjs'",
15
+
"test": "pta 'tests/*.mjs'",
16
16
"test-watch": "onchange --initial '{tests,src}/*.mjs' -- pta 'tests/*.mjs'",
17
17
"prepare": "husky"
18
18
},
+125
-104
src/AtomDef.res
+125
-104
src/AtomDef.res
···
1
1
// type level stuff to enable well-typed coercions
2
2
type atomTag<_> = ..
3
+
type rec anyValue = AnyValue(atomTag<'a>, 'a): anyValue
4
+
5
+
// to allow circular coercions, we declare base types
6
+
// separately from relevant implementation
7
+
module type BASE_ATOM = {
8
+
type t
9
+
type atomTag<_> += Tag: atomTag<t>
10
+
let wrap: t => anyValue
11
+
}
12
+
13
+
module MakeBaseAtom = (
14
+
T: {
15
+
type t
16
+
},
17
+
): (BASE_ATOM with type t = T.t) => {
18
+
type t = T.t
19
+
type atomTag<_> += Tag: atomTag<t>
20
+
let wrap = t => AnyValue(Tag, t)
21
+
}
3
22
4
23
module type ATOM = {
5
-
type t
24
+
module BaseAtom: BASE_ATOM
25
+
type t = BaseAtom.t
6
26
type subst = Map.t<int, t>
7
-
type atomTag<_> += Tag: atomTag<t>
8
27
let unify: (t, t, ~gen: ref<int>=?) => Seq.t<subst>
9
28
let prettyPrint: (t, ~scope: array<string>) => string
10
29
let parse: (string, ~scope: array<string>, ~gen: ref<int>=?) => result<(t, string), string>
···
12
31
let upshift: (t, int, ~from: int=?) => t
13
32
let substDeBruijn: (t, array<option<t>>, ~from: int=?) => t
14
33
let concrete: t => bool
34
+
let coerce: anyValue => option<t>
15
35
}
16
36
17
-
type rec hValue = HValue(atomTag<'a>, 'a): hValue
18
-
module type COERCIBLE_ATOM = {
19
-
include ATOM
20
-
let coerce: hValue => option<t>
21
-
let wrap: t => hValue
37
+
type varBase = Var({idx: int}) | Schematic({schematic: int, allowed: array<int>})
38
+
module VarBase = MakeBaseAtom({
39
+
type t = varBase
40
+
})
41
+
42
+
exception AtomExpected
43
+
44
+
module AtomListBase = MakeBaseAtom({
45
+
type t = anyValue
46
+
})
47
+
48
+
module type ATOM_LIST = {
49
+
module HeadBase: BASE_ATOM
50
+
include ATOM with module BaseAtom = AtomListBase
51
+
let onHead: (t, HeadBase.t => 'a) => option<'a>
22
52
}
23
53
24
-
type loweredSExp = Var({idx: int}) | Schematic({schematic: int, allowed: array<int>})
25
-
type atomTag<_> += SExpTag: atomTag<loweredSExp>
54
+
module NilAtomList: ATOM_LIST = {
55
+
module HeadBase = MakeBaseAtom({
56
+
// empty
57
+
type t = {.}
58
+
})
59
+
module BaseAtom = AtomListBase
60
+
type t = BaseAtom.t
61
+
type subst = Map.t<int, t>
62
+
let parse = (_, ~scope as _, ~gen as _=?) => Error("expected atom")
63
+
// ideally we could check that the tags
64
+
// in each argument are the same before returning Seq.empty, otherwise throw
65
+
// but building up a type-level witness to tag equality is not easy with the
66
+
// extensible variant stuff
67
+
let unify = (_, _, ~gen as _=?) => Seq.empty
68
+
// this should probably throw too, but will be more
69
+
// informative to have it appear wherever it's called from
70
+
let prettyPrint = (_, ~scope as _) => "NIL (THIS IS AN ERROR!)"
71
+
let onHead = (_, _) => throw(AtomExpected)
72
+
let coerce = _ => throw(AtomExpected)
73
+
let substitute = (_, _) => throw(AtomExpected)
74
+
let upshift = (_, _, ~from as _=?) => throw(AtomExpected)
75
+
let substDeBruijn = (_, _, ~from as _=?) => throw(AtomExpected)
76
+
let concrete = _ => throw(AtomExpected)
77
+
}
26
78
27
-
exception MatchCombineAtomForeign
28
-
29
-
module CombineAtom = (Left: COERCIBLE_ATOM, Right: COERCIBLE_ATOM): {
30
-
type rec base =
31
-
| Left(Left.t)
32
-
| Right(Right.t)
33
-
// strictly for coercions
34
-
// occurs when passed from some relative in the tree
35
-
// or when SExp values are lowered into loweredSExp
36
-
| Foreign(hValue)
37
-
include COERCIBLE_ATOM with type t = base
38
-
let match: (t, Left.t => 'a, Right.t => 'a) => 'a
39
-
} => {
40
-
type rec base =
41
-
| Left(Left.t)
42
-
| Right(Right.t)
43
-
| Foreign(hValue)
44
-
type t = base
79
+
module CombineAtom = (Head: ATOM, Tail: ATOM_LIST): (
80
+
ATOM_LIST with module HeadBase = Head.BaseAtom
81
+
) => {
82
+
module HeadBase = Head.BaseAtom
83
+
module Tail = Tail
84
+
module BaseAtom = AtomListBase
85
+
type t = BaseAtom.t
45
86
type subst = Map.t<int, t>
46
87
type gen = ref<int>
47
-
type atomTag<_> += Tag: atomTag<t>
48
-
let coerce = v => Some(Foreign(v))
49
-
let match = (t, leftBranch: Left.t => 'a, rightBranch: Right.t => 'a): 'a =>
50
-
switch t {
51
-
| Left(s) => leftBranch(s)
52
-
| Right(s) => rightBranch(s)
53
-
| Foreign(_) => throw(MatchCombineAtomForeign)
54
-
}
55
-
let wrap = t =>
56
-
switch t {
57
-
| Left(s) => Left.wrap(s)
58
-
| Right(s) => Right.wrap(s)
59
-
| Foreign(val) => val
88
+
let getOrElse = Util.Option.getOrElse
89
+
let coerce = v => Some(v)
90
+
let onHead = (AnyValue(tag, val), f: Head.t => 'a): option<'a> =>
91
+
switch tag {
92
+
| Head.BaseAtom.Tag => Some(f(val))
93
+
| _ => None
60
94
}
61
95
let parse = (s, ~scope, ~gen: option<gen>=?) => {
62
-
Left.parse(s, ~scope, ~gen?)
63
-
->Result.map(((r, rest)) => (Left(r), rest))
64
-
->Util.Result.or(() =>
65
-
Right.parse(s, ~scope, ~gen?)->Result.map(((r, rest)) => (Right(r), rest))
66
-
)
96
+
Head.parse(s, ~scope, ~gen?)
97
+
->Result.map(((r, rest)) => (HeadBase.wrap(r), rest))
98
+
->Util.Result.or(() => Tail.parse(s, ~scope, ~gen?))
67
99
}
68
-
let prettyPrint = (s, ~scope) =>
69
-
s->match(left => Left.prettyPrint(left, ~scope), right => Right.prettyPrint(right, ~scope))
70
-
let unify = (s1, s2, ~gen=?) =>
71
-
switch (s1, s2) {
72
-
| (Left(s1), Left(s2)) =>
73
-
Left.unify(s1, s2, ~gen?)->Seq.map(subst => subst->Util.mapMapValues(v => Left(v)))
74
-
| (Right(s1), Right(s2)) =>
75
-
Right.unify(s1, s2, ~gen?)->Seq.map(subst => subst->Util.mapMapValues(v => Right(v)))
76
-
| (_, _) => Seq.empty
100
+
let prettyPrint = (atom, ~scope) =>
101
+
atom
102
+
->onHead(val => Head.prettyPrint(val, ~scope))
103
+
->getOrElse(() => Tail.prettyPrint(atom, ~scope))
104
+
105
+
let unify = (a1, a2, ~gen=?) => {
106
+
let (AnyValue(tag1, val1), AnyValue(tag2, val2)) = (a1, a2)
107
+
switch (tag1, tag2) {
108
+
| (Head.BaseAtom.Tag, Head.BaseAtom.Tag) =>
109
+
Head.unify(val1, val2)->Seq.map(subst => subst->Util.mapMapValues(HeadBase.wrap))
110
+
| (_, _) => Tail.unify(a1, a2, ~gen?)
77
111
}
78
-
let coerceToLeft = (t): option<Left.t> =>
79
-
switch t {
80
-
| Left(s) => Some(s)
81
-
| Right(s) => Right.wrap(s)->Left.coerce
82
-
| Foreign(v) => Left.coerce(v)
83
-
}
84
-
let coerceToRight = (t): option<Right.t> =>
85
-
switch t {
86
-
| Right(s) => Some(s)
87
-
| Left(s) => Left.wrap(s)->Right.coerce
88
-
| Foreign(v) => Right.coerce(v)
89
-
}
90
-
let substitute = (s, subst: subst) => {
91
-
s->match(
92
-
left => {
93
-
let leftSubs = subst->Util.Map.filterMap((_, v) => coerceToLeft(v))
94
-
Left(Left.substitute(left, leftSubs))
95
-
},
96
-
right => {
97
-
let rightSubs = subst->Util.Map.filterMap((_, v) => coerceToRight(v))
98
-
Right(Right.substitute(right, rightSubs))
99
-
},
100
-
)
101
112
}
102
-
let upshift = (s, amount: int, ~from=?) =>
103
-
s->match(
104
-
left => Left(left->Left.upshift(amount, ~from?)),
105
-
right => Right(right->Right.upshift(amount, ~from?)),
106
-
)
107
-
let substDeBruijn = (s, substs: array<option<t>>, ~from=?) =>
108
-
s->match(
109
-
left => {
110
-
let leftSubs = substs->Array.map(o => o->Option.flatMap(coerceToLeft))
111
-
Left(Left.substDeBruijn(left, leftSubs, ~from?))
112
-
},
113
-
right => {
114
-
let rightSubs = substs->Array.map(o => o->Option.flatMap(coerceToRight))
115
-
Right(Right.substDeBruijn(right, rightSubs, ~from?))
116
-
},
113
+
let coerceToHead = (atom): option<Head.t> =>
114
+
atom->onHead(val => Some(val))->getOrElse(() => Head.coerce(atom))
115
+
let substitute = (atom, subst: subst) =>
116
+
atom
117
+
->onHead(val => {
118
+
let leftSubs = subst->Util.Map.filterMap((_, v) => coerceToHead(v))
119
+
Head.substitute(val, leftSubs)->HeadBase.wrap
120
+
})
121
+
->getOrElse(() => Tail.substitute(atom, subst))
122
+
123
+
let upshift = (atom, amount: int, ~from=?) =>
124
+
atom
125
+
->onHead(val => Head.upshift(val, amount, ~from?)->HeadBase.wrap)
126
+
->getOrElse(() => Tail.upshift(atom, amount, ~from?))
127
+
let substDeBruijn = (atom, substs: array<option<t>>, ~from=?) =>
128
+
atom
129
+
->onHead(val =>
130
+
Head.substDeBruijn(
131
+
val,
132
+
substs->Array.map(o => o->Option.flatMap(coerceToHead)),
133
+
~from?,
134
+
)->HeadBase.wrap
117
135
)
118
-
let concrete = s => s->match(Left.concrete, Right.concrete)
136
+
->getOrElse(() => Tail.substDeBruijn(atom, substs, ~from?))
137
+
let concrete = atom => atom->onHead(Head.concrete)->getOrElse(() => Tail.concrete(atom))
119
138
}
120
139
121
140
module type ATOM_VIEW = {
···
124
143
let make: props => React.element
125
144
}
126
145
146
+
module NilAtomListView: ATOM_VIEW with module Atom := NilAtomList = {
147
+
type props = {name: NilAtomList.t, scope: array<string>}
148
+
let make = _ => throw(AtomExpected)
149
+
}
150
+
127
151
module MakeAtomView = (
128
-
Left: COERCIBLE_ATOM,
152
+
Left: ATOM,
129
153
LeftView: ATOM_VIEW with module Atom := Left,
130
-
Right: COERCIBLE_ATOM,
154
+
Right: ATOM_LIST,
131
155
RightView: ATOM_VIEW with module Atom := Right,
132
156
Combined: module type of CombineAtom(Left, Right),
133
-
): {
134
-
include ATOM_VIEW with module Atom := Combined
135
-
} => {
157
+
): (ATOM_VIEW with module Atom := Combined) => {
136
158
type props = {name: Combined.t, scope: array<string>}
137
159
let make = ({name, scope}: props) =>
138
-
name->Combined.match(
139
-
left => <LeftView name={left} scope />,
140
-
right => <RightView name={right} scope />,
141
-
)
160
+
name
161
+
->Combined.onHead(left => <LeftView name={left} scope />)
162
+
->Util.Option.getOrElse(() => <RightView name scope />)
142
163
}
143
164
144
165
module MakeAtomAndView = (
145
-
Left: COERCIBLE_ATOM,
166
+
Left: ATOM,
146
167
LeftView: ATOM_VIEW with module Atom := Left,
147
-
Right: COERCIBLE_ATOM,
168
+
Right: ATOM_LIST,
148
169
RightView: ATOM_VIEW with module Atom := Right,
149
170
) => {
150
171
module Atom = CombineAtom(Left, Right)
-24
src/Coercible.res
-24
src/Coercible.res
···
1
-
open AtomDef
2
-
3
-
module StringA: COERCIBLE_ATOM with type t = StringA.t = {
4
-
include StringA.Atom
5
-
let coerce = (HValue(tag, a)) =>
6
-
switch tag {
7
-
| Symbolic.Atom.Tag => Some([StringA.String(a)])
8
-
| AtomDef.SExpTag =>
9
-
Some([
10
-
switch a {
11
-
| Var({idx}) => StringA.Var({idx: idx})
12
-
| Schematic({schematic, allowed}) => StringA.Schematic({schematic, allowed})
13
-
},
14
-
])
15
-
| _ => None
16
-
}
17
-
let wrap = a => HValue(StringA.Atom.Tag, a)
18
-
}
19
-
20
-
module Symbolic: COERCIBLE_ATOM with type t = Symbolic.Atom.t = {
21
-
include Symbolic.Atom
22
-
let coerce = _ => None
23
-
let wrap = a => HValue(Symbolic.Atom.Tag, a)
24
-
}
+2
-2
src/HOTerm.res
+2
-2
src/HOTerm.res
+78
-57
src/Method.res
+78
-57
src/Method.res
···
9
9
let facts = t => t.localFacts->Dict.copy->Dict.assign(t.globalFacts)
10
10
}
11
11
12
-
module MethodResults = (Term : TERM) => {
13
-
12
+
module MethodResults = (Term: TERM) => {
14
13
// Currently all three options produce a button
15
14
// with both Group and Delay producing sub-menus
16
15
// I may change Group in future to just present
17
16
// a boxed group of buttons without nesting it in sub-menus.
18
17
// So use Delay() if sub-menus is what you actually want.
19
-
type rec t<'a> = Action(string, 'a, Term.subst)
20
-
| Delay(string, () => array<t<'a>>)
21
-
| Group(string, array<t<'a>>)
22
-
23
-
24
-
25
-
let rec map = (x: t<'a>, f: 'a => 'b ) =>
18
+
type rec t<'a> =
19
+
| Action(string, 'a, Term.subst)
20
+
| Delay(string, unit => array<t<'a>>)
21
+
| Group(string, array<t<'a>>)
22
+
23
+
let rec map = (x: t<'a>, f: 'a => 'b) =>
26
24
switch x {
27
-
| Action(str, a, sub) => Action(str,f(a), sub)
28
-
| Delay(str, g) => Delay(str, () => g(())->Array.map(x => x->map(f)))
25
+
| Action(str, a, sub) => Action(str, f(a), sub)
26
+
| Delay(str, g) => Delay(str, () => g()->Array.map(x => x->map(f)))
29
27
| Group(str, gs) => Group(str, gs->Array.map(x => x->map(f)))
30
28
}
31
-
}
32
-
33
-
29
+
}
34
30
35
31
module type PROOF_METHOD = {
36
32
module Term: TERM
···
165
161
}
166
162
}
167
163
let apply = (ctx: Context.t, j: Judgment.t, gen: Term.gen, f: Rule.t => 'a) => {
168
-
let ret = Dict.make()
169
164
ctx
170
165
->Context.facts
171
166
->Dict.toArray
···
173
168
let insts = rule->Rule.genSchemaInsts(gen, ~scope=ctx.fixes)
174
169
let res = rule->Rule.instantiate(insts)
175
170
if !Judgment.concrete(res.conclusion) {
176
-
Some((key, res, insts))
171
+
None
177
172
} else {
178
-
None
179
-
}
180
-
})
181
-
->Array.forEach(((key, res, insts)) => {
182
-
let substs = Judgment.unify(res.conclusion, j, ~gen)
183
-
substs
184
-
->Seq.take(seqSizeLimit)
185
-
->Seq.forEach(subst => {
173
+
let substs = Judgment.unify(res.conclusion, j, ~gen)->Seq.take(seqSizeLimit)->Seq.toArray
186
174
let new = {
187
175
ruleName: key,
188
176
instantiation: insts,
189
177
subgoals: res.premises->Array.map(f),
190
178
}
191
-
ret->Dict.set("intro " ++ key, (new, subst))
192
-
})
179
+
switch substs {
180
+
| [] => None
181
+
| [subst] => Some(Results.Action(`intro ${key}`, new, subst))
182
+
| _ =>
183
+
Some(
184
+
Delay(
185
+
`intro ${key}`,
186
+
() =>
187
+
substs->Array.map(subst => {
188
+
let s =
189
+
rule.vars
190
+
->Belt.Array.reverse
191
+
->Belt.Array.zip(insts->Array.map(t => t->Term.substitute(subst)))
192
+
->Array.map(
193
+
((v, x)) => {
194
+
let metaS = Term.prettyPrintMeta(v)
195
+
// not very clean, but don't particularly want to
196
+
// pollute TERM with another method for printing bare meta
197
+
let metaWithoutDot =
198
+
metaS->String.slice(~start=0, ~end=String.length(metaS) - 1)
199
+
`${metaWithoutDot} |-> ${Term.prettyPrint(x, ~scope=ctx.fixes)}`
200
+
},
201
+
)
202
+
->Array.join(", ")
203
+
Results.Action(s, new, subst)
204
+
}),
205
+
),
206
+
)
207
+
}
208
+
}
193
209
})
194
-
ret->Dict.toArray->Array.map(((key, (new, subst))) => Results.Action(key,new,subst))
195
210
}
196
211
let check = (it: t<'a>, ctx: Context.t, j: Judgment.t, f: ('a, Rule.t) => 'b) => {
197
212
switch ctx->Context.facts->Dict.get(it.ruleName) {
···
400
415
->Dict.toArray
401
416
->Array.filter(((_, r)) => r.premises->Array.length == 0 && r.vars->Array.length == 0)
402
417
possibleElims->Array.map(((elimName, elim)) => {
403
-
Results.Delay("elim " + elimName,() => {
404
-
let subtree = []
405
-
possibleRules->Array.forEach(((ruleName, rule)) => {
406
-
let ruleInsts = rule->Rule.genSchemaInsts(gen, ~scope=ctx.fixes)
407
-
let rule' = rule->Rule.instantiate(ruleInsts)
408
-
Judgment.unify((rule'.premises[0]->Option.getExn).conclusion, elim.conclusion, ~gen)
409
-
->Seq.take(seqSizeLimit)
410
-
->Seq.forEach(
411
-
elimSub => {
412
-
let rule'' = rule'->Rule.substituteBare(elimSub)
413
-
Judgment.unify(rule''.conclusion, j, ~gen)
414
-
->Seq.take(seqSizeLimit)
415
-
->Seq.forEach(
416
-
ruleSub => {
417
-
let new = {
418
-
ruleName,
419
-
elimName,
420
-
instantiation: ruleInsts,
421
-
subgoals: rule.premises->Array.sliceToEnd(~start=1)->Array.map(f),
422
-
}
423
-
let subst = Term.mergeSubsts(elimSub, ruleSub)
424
-
subtree->Array.push(Results.Action("with " ++ ruleName, new, subst))
425
-
},
426
-
)
427
-
},
428
-
)
429
-
})
430
-
subtree
431
-
})
418
+
Results.Delay(
419
+
"elim " + elimName,
420
+
() => {
421
+
let subtree = []
422
+
possibleRules->Array.forEach(((ruleName, rule)) => {
423
+
let ruleInsts = rule->Rule.genSchemaInsts(gen, ~scope=ctx.fixes)
424
+
let rule' = rule->Rule.instantiate(ruleInsts)
425
+
Judgment.unify((rule'.premises[0]->Option.getExn).conclusion, elim.conclusion, ~gen)
426
+
->Seq.take(seqSizeLimit)
427
+
->Seq.forEach(
428
+
elimSub => {
429
+
let rule'' = rule'->Rule.substituteBare(elimSub)
430
+
Judgment.unify(rule''.conclusion, j, ~gen)
431
+
->Seq.take(seqSizeLimit)
432
+
->Seq.forEach(
433
+
ruleSub => {
434
+
let new = {
435
+
ruleName,
436
+
elimName,
437
+
instantiation: ruleInsts,
438
+
subgoals: rule.premises->Array.sliceToEnd(~start=1)->Array.map(f),
439
+
}
440
+
let subst = Term.mergeSubsts(elimSub, ruleSub)
441
+
subtree->Array.push(Results.Action("with " ++ ruleName, new, subst))
442
+
},
443
+
)
444
+
},
445
+
)
446
+
})
447
+
subtree
448
+
},
449
+
)
432
450
})
433
451
}
434
452
}
···
517
535
let keywords = Array.concat(Method1.keywords, Method2.keywords)
518
536
let apply = (ctx: Context.t, j: Judgment.t, gen: Term.gen, f: Rule.t => 'a) => {
519
537
let d1 = Method1.apply(ctx, j, gen, f)->Array.map(me => me->Results.map(m => First(m)))
520
-
Array.pushMany(d1,Method2.apply(ctx, j, gen, f)->Array.map(me => me->Results.map(m => Second(m))))
538
+
Array.pushMany(
539
+
d1,
540
+
Method2.apply(ctx, j, gen, f)->Array.map(me => me->Results.map(m => Second(m))),
541
+
)
521
542
d1
522
543
}
523
544
let check = (it, ctx, j, f) =>
+1
-1
src/RuleView.res
+1
-1
src/RuleView.res
+5
-5
src/SExp.res
+5
-5
src/SExp.res
···
7
7
let cmp = Pervasives.compare
8
8
})
9
9
10
-
module Make = (Atom: AtomDef.COERCIBLE_ATOM): {
10
+
module Make = (Atom: AtomDef.ATOM): {
11
11
type rec t =
12
12
| Atom(Atom.t)
13
13
| Compound({subexps: array<t>})
···
150
150
let rec lower = (term: t): option<Atom.t> =>
151
151
switch term {
152
152
| Atom(s) => Some(s)
153
-
| Var({idx}) => Atom.coerce(HValue(AtomDef.SExpTag, AtomDef.Var({idx: idx})))
153
+
| Var({idx}) => Atom.coerce(AtomDef.VarBase.wrap(Var({idx: idx})))
154
154
| Schematic({schematic, allowed}) =>
155
-
Atom.coerce(HValue(AtomDef.SExpTag, AtomDef.Schematic({schematic, allowed})))
155
+
Atom.coerce(AtomDef.VarBase.wrap(Schematic({schematic, allowed})))
156
156
| Compound({subexps: [e1]}) => lower(e1)
157
157
| _ => None
158
158
}
···
311
311
312
312
let rec concrete = t =>
313
313
switch t {
314
-
| Schematic(_) => true
314
+
| Schematic(_) => false
315
315
| Atom(s) => Atom.concrete(s)
316
-
| Compound({subexps}) => subexps->Array.every(concrete)
316
+
| Compound({subexps}) => subexps->Array.some(concrete)
317
317
| _ => false
318
318
}
319
319
let mapTerms = (t, f) => f(t)
+1
-1
src/SExpView.res
+1
-1
src/SExpView.res
+12
-4
src/Scratch.res
+12
-4
src/Scratch.res
···
42
42
module TheoremS = Editable.TextArea(Theorem.Make(HOTerm, HOTerm, HOTermJView, DLRView))
43
43
module ConfS = ConfigBlock.Make(HOTerm, HOTerm)
44
44
45
+
module Symbol = AtomDef.MakeAtomAndView(
46
+
Symbolic.Atom,
47
+
Symbolic.AtomView,
48
+
AtomDef.NilAtomList,
49
+
AtomDef.NilAtomListView,
50
+
)
45
51
module StringSymbol = AtomDef.MakeAtomAndView(
46
-
Coercible.StringA,
52
+
StringA.Atom,
47
53
StringA.AtomView,
48
-
Coercible.Symbolic,
49
-
Symbolic.AtomView,
54
+
Symbol.Atom,
55
+
Symbol.AtomView,
50
56
)
51
57
module StringSExp = SExp.Make(StringSymbol.Atom)
52
58
module TermView = SExpView.Make(StringSymbol.Atom, StringSymbol.AtomView, StringSExp)
53
59
module StringSExpJView = TermViewAsJudgmentView.Make(StringSExp, StringSExp, TermView)
54
-
module AxiomStr = Editable.TextArea(StringAxiomSet)
60
+
module AxiomStr = Editable.TextArea(
61
+
StringAxiomSet.Make(StringSymbol.Atom, StringSExp, StringSExpJView),
62
+
)
55
63
56
64
module DerivationsOrLemmasStrView = MethodView.CombineMethodView(
57
65
StringSExp,
+19
-3
src/StringA.res
+19
-3
src/StringA.res
···
11
11
type meta = string
12
12
type schematic = int
13
13
14
+
module BaseAtom = AtomDef.MakeBaseAtom({
15
+
type t = t
16
+
})
17
+
14
18
module Atom = {
19
+
module BaseAtom = BaseAtom
15
20
type t = t
16
21
type subst = Map.t<schematic, t>
17
-
type AtomDef.atomTag<_> += Tag: AtomDef.atomTag<t>
18
22
let substitute = (term: t, subst: subst) =>
19
23
Array.flatMap(term, piece => {
20
24
switch piece {
···
458
462
let concrete = t =>
459
463
t->Array.every(p =>
460
464
switch p {
461
-
| Schematic(_) => true
462
-
| _ => false
465
+
| Schematic(_) => false
466
+
| _ => true
463
467
}
464
468
)
469
+
let coerce = (AtomDef.AnyValue(tag, a)) =>
470
+
switch tag {
471
+
| Symbolic.BaseAtom.Tag => Some([String(a)])
472
+
| AtomDef.VarBase.Tag =>
473
+
Some([
474
+
switch a {
475
+
| Var({idx}) => Var({idx: idx})
476
+
| Schematic({schematic, allowed}) => Schematic({schematic, allowed})
477
+
},
478
+
])
479
+
| _ => None
480
+
}
465
481
}
466
482
467
483
module AtomView = {
+2
-1
src/StringA.resi
+2
-1
src/StringA.resi
···
4
4
| Schematic({schematic: int, allowed: array<int>})
5
5
type t = array<piece>
6
6
7
-
module Atom: AtomDef.ATOM with type t = t
7
+
module BaseAtom: AtomDef.BASE_ATOM with type t = t
8
+
module Atom: AtomDef.ATOM with module BaseAtom = BaseAtom
8
9
module AtomView: AtomDef.ATOM_VIEW with module Atom := Atom
+195
-202
src/StringAxiomSet.res
+195
-202
src/StringAxiomSet.res
···
1
1
open Component
2
+
open! Util
2
3
3
-
module StringSymbol = AtomDef.MakeAtomAndView(
4
-
Coercible.StringA,
5
-
StringA.AtomView,
6
-
Coercible.Symbolic,
7
-
Symbolic.AtomView,
8
-
)
9
-
module StringSExp = SExp.Make(StringSymbol.Atom)
10
-
module TermView = SExpView.Make(StringSymbol.Atom, StringSymbol.AtomView, StringSExp)
11
-
module JudgmentView = TermViewAsJudgmentView.Make(StringSExp, StringSExp, TermView)
12
-
13
-
module Rule = Rule.Make(StringSExp, StringSExp)
14
-
module RuleView = RuleView.Make(StringSExp, StringSExp, JudgmentView)
15
-
module Ports = Ports(StringSExp, StringSExp)
16
-
type state = {
17
-
raw: dict<Rule.t>,
18
-
derived: dict<Rule.t>,
19
-
}
20
-
21
-
type props = {
22
-
content: state,
23
-
imports: Ports.t,
24
-
onChange: (state, ~exports: Ports.t=?) => unit,
25
-
}
4
+
module Make = (
5
+
Atom: AtomDef.ATOM_LIST,
6
+
Term: module type of SExp.Make(Atom),
7
+
JudgmentView: Signatures.JUDGMENT_VIEW with module Term := Term and module Judgment := Term,
8
+
) => {
9
+
module Rule = Rule.Make(Term, Term)
10
+
module RuleView = RuleView.Make(Term, Term, JudgmentView)
11
+
module Ports = Ports(Term, Term)
12
+
type state = {
13
+
raw: dict<Rule.t>,
14
+
derived: dict<Rule.t>,
15
+
}
26
16
27
-
type judgeGroup = {
28
-
name: string,
29
-
rules: array<Rule.t>,
30
-
}
17
+
type props = {
18
+
content: state,
19
+
imports: Ports.t,
20
+
onChange: (state, ~exports: Ports.t=?) => unit,
21
+
}
31
22
32
-
module Set = Belt.Set.String
33
-
let varsInRule = (rule: Rule.t) => {
34
-
rule.premises->Array.reduce(Set.fromArray(rule.vars), (s, r) =>
35
-
s->Set.union(Set.fromArray(r.vars))
36
-
)
37
-
}
23
+
type judgeGroup = {
24
+
name: string,
25
+
rules: array<Rule.t>,
26
+
}
38
27
39
-
let getSExpName = (t: StringSExp.t): option<string> =>
40
-
switch t {
41
-
| Atom(name) => Some(name->StringSymbol.Atom.prettyPrint(~scope=[]))
42
-
| _ => None
28
+
module Set = Belt.Set.String
29
+
let varsInRule = (rule: Rule.t) => {
30
+
rule.premises->Array.reduce(Set.fromArray(rule.vars), (s, r) =>
31
+
s->Set.union(Set.fromArray(r.vars))
32
+
)
43
33
}
44
34
45
-
let destructure = (r: StringSExp.t): (StringA.Atom.t, string) =>
46
-
switch r {
47
-
| Compound({subexps: [Atom(Left(s)), Atom(Right(name))]}) => (s, name)
48
-
| _ => throw(Util.Unreachable("expected valid induction rule"))
35
+
let destructureOpt = (r: Term.t): option<(StringA.Atom.t, Symbolic.Atom.t)> =>
36
+
switch r {
37
+
| Compound({subexps: [Atom(AtomDef.AnyValue(tag1, s)), Atom(AtomDef.AnyValue(tag2, name))]}) =>
38
+
switch (tag1, tag2) {
39
+
| (StringA.BaseAtom.Tag, Symbolic.BaseAtom.Tag) => Some((s, name))
40
+
| _ => None
41
+
}
42
+
| _ => None
43
+
}
44
+
exception InvalidStringInductionPattern
45
+
let destructure = (r: Term.t): (StringA.Atom.t, string) =>
46
+
destructureOpt(r)->Option.getOrElse(() => throw(InvalidStringInductionPattern))
47
+
let structure = (lhs: Term.t, rhs: Term.t): Term.t => Compound({
48
+
subexps: [lhs, rhs],
49
+
})
50
+
let findMentionedRuleGroups = (group: judgeGroup, allGroups: array<judgeGroup>): array<
51
+
judgeGroup,
52
+
> => {
53
+
let allGroupNames = allGroups->Array.map(g => g.name)
54
+
let groupNames: array<string> = Array.concat(
55
+
[group.name],
56
+
group.rules
57
+
->Array.flatMap(r =>
58
+
r.premises
59
+
->Array.filterMap(p => p.conclusion->destructureOpt->Option.map(Pair.second))
60
+
->Array.filter(name => allGroupNames->Array.find(name' => name' == name)->Option.isSome)
61
+
)
62
+
->Set.fromArray
63
+
->Set.remove(group.name)
64
+
->Set.toArray,
65
+
)
66
+
groupNames->Array.map(name => allGroups->Array.find(g => g.name == name))->Array.keepSome
49
67
}
50
-
let destructureOpt = (r: StringSExp.t): option<(StringA.Atom.t, string)> =>
51
-
switch r {
52
-
| Compound({subexps: [Atom(Left(s)), Atom(Right(name))]}) => Some((s, name))
53
-
| _ => None
54
-
}
55
-
let structure = (lhs: StringSExp.t, rhs: StringSExp.t): StringSExp.t => Compound({
56
-
subexps: [lhs, rhs],
57
-
})
58
-
let findMentionedRuleGroups = (group: judgeGroup, allGroups: array<judgeGroup>): array<
59
-
judgeGroup,
60
-
> => {
61
-
let allGroupNames = allGroups->Array.map(g => g.name)
62
-
let groupNames: array<string> = Array.concat(
63
-
[group.name],
64
-
group.rules
65
-
->Array.flatMap(r =>
66
-
r.premises
67
-
->Array.filterMap(p => p.conclusion->destructureOpt->Option.map(Pair.second))
68
-
->Array.filter(name => allGroupNames->Array.find(name' => name' == name)->Option.isSome)
69
-
)
70
-
->Set.fromArray
71
-
->Set.remove(group.name)
72
-
->Set.toArray,
73
-
)
74
-
groupNames->Array.map(name => allGroups->Array.find(g => g.name == name))->Array.keepSome
75
-
}
76
68
77
-
let derive = (group: judgeGroup, mentionedGroups: array<judgeGroup>): Rule.t => {
78
-
let allVars =
79
-
mentionedGroups
80
-
->Array.flatMap(g => g.rules)
81
-
->Array.reduce(Set.empty, (s, r) => s->Set.union(varsInRule(r)))
82
-
let rec genVar = (base: string) => {
83
-
if allVars->Set.has(base) {
84
-
genVar(`${base}'`)
85
-
} else {
86
-
base
69
+
let derive = (group: judgeGroup, mentionedGroups: array<judgeGroup>): Rule.t => {
70
+
let allVars =
71
+
mentionedGroups
72
+
->Array.flatMap(g => g.rules)
73
+
->Array.reduce(Set.empty, (s, r) => s->Set.union(varsInRule(r)))
74
+
let rec genVar = (base: string) => {
75
+
if allVars->Set.has(base) {
76
+
genVar(`${base}'`)
77
+
} else {
78
+
base
79
+
}
80
+
}
81
+
let ps = mentionedGroups->Array.map(g => genVar(`P${g.name}`))
82
+
let (b, x, a) = (genVar("b"), genVar("x"), genVar("a"))
83
+
let vars = Array.concat(ps, [b, x, a])
84
+
let xIdx = vars->Array.findIndex(i => i == x)
85
+
let aIdx = vars->Array.findIndex(i => i == a)
86
+
let bIdx = vars->Array.findIndex(i => i == b)
87
+
let surround = (t: StringA.Atom.t, aIdx: int, bIdx: int) => {
88
+
Array.concat(Array.concat([StringA.Var({idx: aIdx})], t), [StringA.Var({idx: bIdx})])
89
+
}
90
+
let lookupGroup = (name: string): option<int> =>
91
+
mentionedGroups->Array.findIndexOpt(g => name == g.name)
92
+
let rec replaceJudgeRHS = (rule: Rule.t, baseIdx: int): Rule.t => {
93
+
let baseIdx = baseIdx + Array.length(rule.vars)
94
+
let (s, name) = destructure(rule.conclusion)
95
+
let inductionHyps =
96
+
rule.premises
97
+
->Array.filter(r =>
98
+
r.conclusion
99
+
->destructureOpt
100
+
->Option.flatMap(conclusion => conclusion->Pair.second->lookupGroup)
101
+
->Option.isSome
102
+
)
103
+
->Array.map(r => replaceJudgeRHS(r, baseIdx))
104
+
let pIdx = lookupGroup(name)->Option.getExn
105
+
{
106
+
vars: rule.vars,
107
+
premises: rule.premises->Array.concat(inductionHyps),
108
+
conclusion: structure(
109
+
Atom(surround(s, aIdx + baseIdx, bIdx + baseIdx)->StringA.BaseAtom.wrap),
110
+
Var({idx: pIdx + baseIdx}),
111
+
),
112
+
}
87
113
}
88
-
}
89
-
let ps = mentionedGroups->Array.map(g => genVar(`P${g.name}`))
90
-
let (b, x, a) = (genVar("b"), genVar("x"), genVar("a"))
91
-
let vars = Array.concat(ps, [b, x, a])
92
-
let xIdx = vars->Array.findIndex(i => i == x)
93
-
let aIdx = vars->Array.findIndex(i => i == a)
94
-
let bIdx = vars->Array.findIndex(i => i == b)
95
-
let surround = (t: StringA.Atom.t, aIdx: int, bIdx: int) => {
96
-
Array.concat(Array.concat([StringA.Var({idx: aIdx})], t), [StringA.Var({idx: bIdx})])
97
-
}
98
-
let lookupGroup = (name: string): option<int> =>
99
-
mentionedGroups->Array.findIndexOpt(g => name == g.name)
100
-
let rec replaceJudgeRHS = (rule: Rule.t, baseIdx: int): Rule.t => {
101
-
let baseIdx = baseIdx + Array.length(rule.vars)
102
-
let (s, name) = destructure(rule.conclusion)
103
-
let inductionHyps =
104
-
rule.premises
105
-
->Array.filter(r =>
106
-
r.conclusion
107
-
->destructureOpt
108
-
->Option.flatMap(conclusion => conclusion->Pair.second->lookupGroup)
109
-
->Option.isSome
110
-
)
111
-
->Array.map(r => replaceJudgeRHS(r, baseIdx))
112
-
let pIdx = lookupGroup(name)->Option.getExn
113
114
{
114
-
vars: rule.vars,
115
-
premises: rule.premises->Array.concat(inductionHyps),
116
-
conclusion: structure(
117
-
surround(s, aIdx + baseIdx, bIdx + baseIdx)->Left->Atom,
118
-
Var({idx: pIdx + baseIdx}),
115
+
vars,
116
+
premises: Array.concat(
117
+
[
118
+
{
119
+
Rule.vars: [],
120
+
premises: [],
121
+
conclusion: structure(Var({idx: xIdx}), Atom(group.name->Symbolic.BaseAtom.wrap)),
122
+
},
123
+
],
124
+
mentionedGroups->Array.flatMap(g => g.rules->Array.map(r => replaceJudgeRHS(r, 0))),
119
125
),
126
+
conclusion: structure(
127
+
Atom(surround([Var({idx: xIdx})], aIdx, bIdx)->StringA.BaseAtom.wrap),
128
+
Var({idx: 0}),
129
+
), // TODO: clean here
120
130
}
121
131
}
122
-
{
123
-
vars,
124
-
premises: Array.concat(
125
-
[
126
-
{
127
-
Rule.vars: [],
128
-
premises: [],
129
-
conclusion: structure(Var({idx: xIdx}), Atom(Right(group.name))),
130
-
},
131
-
],
132
-
mentionedGroups->Array.flatMap(g => g.rules->Array.map(r => replaceJudgeRHS(r, 0))),
133
-
),
134
-
conclusion: structure(
135
-
surround([StringA.Var({idx: xIdx})], aIdx, bIdx)->Left->Atom,
136
-
Var({idx: 0}),
137
-
), // TODO: clean here
138
-
}
139
-
}
140
132
141
-
let deserialise = (str: string, ~imports as _: Ports.t) => {
142
-
let getBase = (str: string) => {
143
-
let cur = ref(str)
144
-
let go = ref(true)
145
-
let results = Dict.make()
146
-
let ret = ref(Error("impossible"))
147
-
while go.contents {
148
-
switch Rule.parseTopLevel(cur.contents, ~scope=[]) {
149
-
| Ok((t, n), rest) =>
150
-
if n->String.trim == "" {
151
-
go := false
152
-
ret := Error("Rule given with no name")
153
-
} else {
154
-
Dict.set(results, n, t)
155
-
if rest->String.trim == "" {
133
+
let deserialise = (str: string, ~imports as _: Ports.t) => {
134
+
let getBase = (str: string) => {
135
+
let cur = ref(str)
136
+
let go = ref(true)
137
+
let results = Dict.make()
138
+
let ret = ref(Error("impossible"))
139
+
while go.contents {
140
+
switch Rule.parseTopLevel(cur.contents, ~scope=[]) {
141
+
| Ok((t, n), rest) =>
142
+
if n->String.trim == "" {
156
143
go := false
157
-
ret := Ok(results)
144
+
ret := Error("Rule given with no name")
158
145
} else {
159
-
cur := rest
146
+
Dict.set(results, n, t)
147
+
if rest->String.trim == "" {
148
+
go := false
149
+
ret := Ok(results)
150
+
} else {
151
+
cur := rest
152
+
}
160
153
}
161
-
}
162
-
| Error(e) => {
163
-
go := false
164
-
ret := Error(e)
154
+
| Error(e) => {
155
+
go := false
156
+
ret := Error(e)
157
+
}
165
158
}
166
159
}
160
+
ret.contents
167
161
}
168
-
ret.contents
169
-
}
170
-
getBase(str)->Result.map(raw => {
171
-
let grouped: dict<array<Rule.t>> = Dict.make()
172
-
raw->Dict.forEach(rule =>
173
-
switch rule.conclusion {
174
-
| Compound({subexps: [Atom(Left(_)), Atom(Right(name))]}) =>
175
-
switch grouped->Dict.get(name) {
176
-
| None => grouped->Dict.set(name, [rule])
177
-
| Some(rs) => rs->Array.push(rule)
162
+
getBase(str)->Result.map(raw => {
163
+
let grouped: dict<array<Rule.t>> = Dict.make()
164
+
raw->Dict.forEach(rule =>
165
+
switch rule.conclusion->destructureOpt {
166
+
| Some((_, name)) =>
167
+
switch grouped->Dict.get(name) {
168
+
| None => grouped->Dict.set(name, [rule])
169
+
| Some(rs) => rs->Array.push(rule)
170
+
}
171
+
| _ => ()
178
172
}
179
-
| _ => ()
180
-
}
181
-
)
182
-
let allGroups = grouped->Dict.toArray->Array.map(((name, rules)) => {name, rules})
183
-
let derived: Dict.t<Rule.t> = Dict.make()
184
-
allGroups->Array.forEach(group => {
185
-
// NOTE: this can clash with other names. is this an issue?
186
-
derived->Dict.set(`${group.name}_induct`, derive(group, [group]))
187
-
let mentionedGroups = findMentionedRuleGroups(group, allGroups)
188
-
if mentionedGroups->Array.length > 1 {
189
-
derived->Dict.set(`${group.name}_mutualInduct`, derive(group, mentionedGroups))
190
-
}
173
+
)
174
+
let allGroups = grouped->Dict.toArray->Array.map(((name, rules)) => {name, rules})
175
+
let derived: Dict.t<Rule.t> = Dict.make()
176
+
allGroups->Array.forEach(group => {
177
+
// NOTE: this can clash with other names. is this an issue?
178
+
derived->Dict.set(`${group.name}_induct`, derive(group, [group]))
179
+
let mentionedGroups = findMentionedRuleGroups(group, allGroups)
180
+
if mentionedGroups->Array.length > 1 {
181
+
derived->Dict.set(`${group.name}_mutualInduct`, derive(group, mentionedGroups))
182
+
}
183
+
})
184
+
({raw, derived}, {Ports.facts: raw->Dict.copy->Dict.assign(derived), ruleStyle: None})
191
185
})
192
-
({raw, derived}, {Ports.facts: raw->Dict.copy->Dict.assign(derived), ruleStyle: None})
193
-
})
194
-
}
186
+
}
195
187
196
-
let serialise = (state: state) => {
197
-
state.raw
198
-
->Dict.toArray
199
-
->Array.map(((k, r)) => r->Rule.prettyPrintTopLevel(~name=k))
200
-
->Array.join("\n")
201
-
}
188
+
let serialise = (state: state) => {
189
+
state.raw
190
+
->Dict.toArray
191
+
->Array.map(((k, r)) => r->Rule.prettyPrintTopLevel(~name=k))
192
+
->Array.join("\n")
193
+
}
202
194
203
-
let make = props => {
204
-
let makeRules = content =>
205
-
<div
206
-
className={"axiom-set axiom-set-"->String.concat(
207
-
String.make(props.imports.ruleStyle->Option.getOr(Hybrid)),
208
-
)}
209
-
>
210
-
{content
211
-
->Dict.toArray
212
-
->Array.mapWithIndex(((n, r), i) =>
213
-
<RuleView
214
-
rule={r}
215
-
scope={[]}
216
-
key={String.make(i)}
217
-
style={props.imports.ruleStyle->Option.getOr(Hybrid)}
218
-
>
219
-
{React.string(n)}
220
-
</RuleView>
221
-
)
222
-
->React.array}
195
+
let make = props => {
196
+
let makeRules = content =>
197
+
<div
198
+
className={"axiom-set axiom-set-"->String.concat(
199
+
String.make(props.imports.ruleStyle->Option.getOr(Hybrid)),
200
+
)}
201
+
>
202
+
{content
203
+
->Dict.toArray
204
+
->Array.mapWithIndex(((n, r), i) =>
205
+
<RuleView
206
+
rule={r}
207
+
scope={[]}
208
+
key={String.make(i)}
209
+
style={props.imports.ruleStyle->Option.getOr(Hybrid)}
210
+
>
211
+
{React.string(n)}
212
+
</RuleView>
213
+
)
214
+
->React.array}
215
+
</div>
216
+
<div>
217
+
{makeRules(props.content.raw)}
218
+
<p> {React.string("derived")} </p>
219
+
{makeRules(props.content.derived)}
223
220
</div>
224
-
<div>
225
-
{makeRules(props.content.raw)}
226
-
<p> {React.string("derived")} </p>
227
-
{makeRules(props.content.derived)}
228
-
</div>
221
+
}
229
222
}
+7
-4
src/Symbolic.res
+7
-4
src/Symbolic.res
···
1
-
type t = string
1
+
module BaseAtom = AtomDef.MakeBaseAtom({
2
+
type t = string
3
+
})
4
+
2
5
module Atom = {
3
-
open AtomDef
6
+
module BaseAtom = BaseAtom
4
7
type t = string
5
8
type subst = Map.t<int, string>
6
-
type atomTag<_> += Tag: atomTag<t>
7
9
let unify = (a, b, ~gen as _=?) =>
8
10
if a == b {
9
11
Seq.once(Map.make())
···
19
21
}
20
22
let substitute = (name, _) => name
21
23
let substDeBruijn = (name, _, ~from as _=?) => name
22
-
let concrete = _ => false
24
+
let concrete = _ => true
23
25
let upshift = (t, _, ~from as _=?) => t
26
+
let coerce = _ => None
24
27
}
25
28
26
29
module AtomView = {
+2
-2
src/Symbolic.resi
+2
-2
src/Symbolic.resi
+13
-2
src/Util.res
+13
-2
src/Util.res
···
143
143
}
144
144
145
145
module Result = {
146
-
let ok = (r: result<'a, 'b>): option<'a> =>
146
+
include Result
147
+
type t<'a, 'b> = result<'a, 'b>
148
+
let ok = (r: t<'a, 'b>): option<'a> =>
147
149
switch r {
148
150
| Ok(a) => Some(a)
149
151
| Error(_) => None
150
152
}
151
-
let or = (r1: result<'a, 'b>, r2: unit => result<'a, 'b>): result<'a, 'b> =>
153
+
let or = (r1: t<'a, 'b>, r2: unit => t<'a, 'b>): t<'a, 'b> =>
152
154
switch r1 {
153
155
| Ok(_) => r1
154
156
| Error(_) => r2()
155
157
}
156
158
}
159
+
160
+
module Option = {
161
+
include Option
162
+
let getOrElse = (t, f): 'a =>
163
+
switch t {
164
+
| Some(a) => a
165
+
| None => f()
166
+
}
167
+
}
+14
-11
tests/RuleTest.res
+14
-11
tests/RuleTest.res
···
32
32
}
33
33
34
34
zoraBlock("string terms", t => {
35
+
module Symbol = AtomDef.MakeAtomAndView(
36
+
Symbolic.Atom,
37
+
Symbolic.AtomView,
38
+
AtomDef.NilAtomList,
39
+
AtomDef.NilAtomListView,
40
+
)
35
41
module StringSymbol = AtomDef.MakeAtomAndView(
36
-
Coercible.StringA,
42
+
StringA.Atom,
37
43
StringA.AtomView,
38
-
Coercible.Symbolic,
39
-
Symbolic.AtomView,
44
+
Symbol.Atom,
45
+
Symbol.AtomView,
40
46
)
41
47
module StringSExp = SExp.Make(StringSymbol.Atom)
48
+
let wrapString = (s): StringSExp.t => Atom(AtomDef.AnyValue(StringA.BaseAtom.Tag, s))
49
+
let wrapSymbol = (s): StringSExp.t => Atom(AnyValue(Symbolic.BaseAtom.Tag, s))
42
50
module T = MakeTest(StringSExp, StringSExp)
43
51
t->T.testParseInner(
44
52
`[s1. ("$s1" p) |- ("($s1)" p)]`,
···
49
57
vars: [],
50
58
premises: [],
51
59
conclusion: StringSExp.Compound({
52
-
subexps: [
53
-
[StringA.Var({idx: 0})]->StringSymbol.Atom.Left->StringSExp.Atom,
54
-
"p"->StringSymbol.Atom.Right->StringSExp.Atom,
55
-
],
60
+
subexps: [wrapString([StringA.Var({idx: 0})]), wrapSymbol("p")],
56
61
}),
57
62
},
58
63
],
59
64
conclusion: StringSExp.Compound({
60
65
subexps: [
61
-
[StringA.String("("), StringA.Var({idx: 0}), StringA.String(")")]
62
-
->StringSymbol.Atom.Left
63
-
->StringSExp.Atom,
64
-
"p"->StringSymbol.Atom.Right->StringSExp.Atom,
66
+
wrapString([StringA.String("("), StringA.Var({idx: 0}), StringA.String(")")]),
67
+
wrapSymbol("p"),
65
68
],
66
69
}),
67
70
},