the next generation of the in-browser educational proof assistant
move to list-based combine atom functor rather than sum tree
This significantly tidies the representation of a choice of atom
by folding the previous `Left, Right, and Foreign` constructors into
a single `anyValue`.
authored by
Josh Brown
and committed by
Tangled
33564d98
3974f644
+161
-126
+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
},
+99
-96
src/AtomDef.res
+99
-96
src/AtomDef.res
···
1
1
// type level stuff to enable well-typed coercions
2
2
type atomTag<_> = ..
3
-
type rec hValue = HValue(atomTag<'a>, 'a): hValue
3
+
type rec anyValue = HValue(atomTag<'a>, 'a): anyValue
4
4
5
5
// to allow circular coercions, we declare base types
6
6
// separately from relevant implementation
7
7
module type BASE_ATOM = {
8
8
type t
9
9
type atomTag<_> += Tag: atomTag<t>
10
-
let wrap: t => hValue
10
+
let wrap: t => anyValue
11
11
}
12
12
13
13
module MakeBaseAtom = (
···
31
31
let upshift: (t, int, ~from: int=?) => t
32
32
let substDeBruijn: (t, array<option<t>>, ~from: int=?) => t
33
33
let concrete: t => bool
34
-
let coerce: hValue => option<t>
35
-
let wrap: t => hValue
34
+
let coerce: anyValue => option<t>
36
35
}
37
36
38
37
type loweredSExp = Var({idx: int}) | Schematic({schematic: int, allowed: array<int>})
39
38
type atomTag<_> += SExpTag: atomTag<loweredSExp>
40
39
41
-
exception MatchCombineAtomForeign
40
+
exception AtomExpected
41
+
42
+
module AtomListBase = MakeBaseAtom({
43
+
type t = anyValue
44
+
})
45
+
46
+
module type ATOM_LIST = {
47
+
module HeadBase: BASE_ATOM
48
+
include ATOM with module BaseAtom = AtomListBase
49
+
let onHead: (t, HeadBase.t => 'a) => option<'a>
50
+
}
42
51
43
-
module CombineAtom = (Left: ATOM, Right: ATOM): {
44
-
type base =
45
-
| Left(Left.t)
46
-
| Right(Right.t)
47
-
// strictly for coercions
48
-
// occurs when passed from some relative in the tree
49
-
// or when SExp values are lowered into loweredSExp
50
-
| Foreign(hValue)
51
-
include ATOM with type BaseAtom.t = base
52
-
let match: (t, Left.t => 'a, Right.t => 'a) => 'a
53
-
} => {
54
-
type rec base =
55
-
| Left(Left.t)
56
-
| Right(Right.t)
57
-
| Foreign(hValue)
58
-
module BaseAtom = MakeBaseAtom({
59
-
type t = base
52
+
module NilAtomList: ATOM_LIST = {
53
+
module HeadBase = MakeBaseAtom({
54
+
// empty
55
+
type t = {.}
60
56
})
57
+
module BaseAtom = AtomListBase
58
+
type t = BaseAtom.t
59
+
type subst = Map.t<int, t>
60
+
let parse = (_, ~scope as _, ~gen as _=?) => Error("expected atom")
61
+
// ideally we could check that the tags
62
+
// in each argument are the same before returning Seq.empty, otherwise throw
63
+
// but building up a type-level witness to tag equality is not easy with the
64
+
// extensible variant stuff
65
+
let unify = (_, _, ~gen as _=?) => Seq.empty
66
+
// this should probably throw too, but will be more
67
+
// informative to have it appear wherever it's called from
68
+
let prettyPrint = (_, ~scope as _) => "NIL (THIS IS AN ERROR!)"
69
+
let onHead = (_, _) => throw(AtomExpected)
70
+
let coerce = _ => throw(AtomExpected)
71
+
let substitute = (_, _) => throw(AtomExpected)
72
+
let upshift = (_, _, ~from as _=?) => throw(AtomExpected)
73
+
let substDeBruijn = (_, _, ~from as _=?) => throw(AtomExpected)
74
+
let concrete = _ => throw(AtomExpected)
75
+
}
76
+
77
+
module CombineAtom = (Head: ATOM, Tail: ATOM_LIST): (
78
+
ATOM_LIST with module HeadBase = Head.BaseAtom
79
+
) => {
80
+
module HeadBase = Head.BaseAtom
81
+
module Tail = Tail
82
+
module BaseAtom = AtomListBase
61
83
type t = BaseAtom.t
62
84
type subst = Map.t<int, t>
63
85
type gen = ref<int>
64
-
let coerce = v => Some(Foreign(v))
65
-
let match = (t, leftBranch: Left.t => 'a, rightBranch: Right.t => 'a): 'a =>
66
-
switch t {
67
-
| Left(s) => leftBranch(s)
68
-
| Right(s) => rightBranch(s)
69
-
| Foreign(_) => throw(MatchCombineAtomForeign)
70
-
}
71
-
let wrap = t =>
72
-
switch t {
73
-
| Left(s) => Left.wrap(s)
74
-
| Right(s) => Right.wrap(s)
75
-
| Foreign(val) => val
86
+
let getOrElse = Util.Option.getOrElse
87
+
let coerce = v => Some(v)
88
+
let onHead = (HValue(tag, val), f: Head.t => 'a): option<'a> =>
89
+
switch tag {
90
+
| Head.BaseAtom.Tag => Some(f(val))
91
+
| _ => None
76
92
}
77
93
let parse = (s, ~scope, ~gen: option<gen>=?) => {
78
-
Left.parse(s, ~scope, ~gen?)
79
-
->Result.map(((r, rest)) => (Left(r), rest))
80
-
->Util.Result.or(() =>
81
-
Right.parse(s, ~scope, ~gen?)->Result.map(((r, rest)) => (Right(r), rest))
82
-
)
94
+
Head.parse(s, ~scope, ~gen?)
95
+
->Result.map(((r, rest)) => (HeadBase.wrap(r), rest))
96
+
->Util.Result.or(() => Tail.parse(s, ~scope, ~gen?))
83
97
}
84
-
let prettyPrint = (s, ~scope) =>
85
-
s->match(left => Left.prettyPrint(left, ~scope), right => Right.prettyPrint(right, ~scope))
86
-
let unify = (s1, s2, ~gen=?) =>
87
-
switch (s1, s2) {
88
-
| (Left(s1), Left(s2)) =>
89
-
Left.unify(s1, s2, ~gen?)->Seq.map(subst => subst->Util.mapMapValues(v => Left(v)))
90
-
| (Right(s1), Right(s2)) =>
91
-
Right.unify(s1, s2, ~gen?)->Seq.map(subst => subst->Util.mapMapValues(v => Right(v)))
92
-
| (_, _) => Seq.empty
98
+
let prettyPrint = (atom, ~scope) =>
99
+
atom
100
+
->onHead(val => Head.prettyPrint(val, ~scope))
101
+
->getOrElse(() => Tail.prettyPrint(atom, ~scope))
102
+
103
+
let unify = (a1, a2, ~gen=?) => {
104
+
let (HValue(tag1, val1), HValue(tag2, val2)) = (a1, a2)
105
+
switch (tag1, tag2) {
106
+
| (Head.BaseAtom.Tag, Head.BaseAtom.Tag) =>
107
+
Head.unify(val1, val2)->Seq.map(subst => subst->Util.mapMapValues(HeadBase.wrap))
108
+
| (_, _) => Tail.unify(a1, a2, ~gen?)
93
109
}
94
-
let coerceToLeft = (t): option<Left.t> =>
95
-
switch t {
96
-
| Left(s) => Some(s)
97
-
| Right(s) => Right.wrap(s)->Left.coerce
98
-
| Foreign(v) => Left.coerce(v)
99
-
}
100
-
let coerceToRight = (t): option<Right.t> =>
101
-
switch t {
102
-
| Right(s) => Some(s)
103
-
| Left(s) => Left.wrap(s)->Right.coerce
104
-
| Foreign(v) => Right.coerce(v)
105
-
}
106
-
let substitute = (s, subst: subst) => {
107
-
s->match(
108
-
left => {
109
-
let leftSubs = subst->Util.Map.filterMap((_, v) => coerceToLeft(v))
110
-
Left(Left.substitute(left, leftSubs))
111
-
},
112
-
right => {
113
-
let rightSubs = subst->Util.Map.filterMap((_, v) => coerceToRight(v))
114
-
Right(Right.substitute(right, rightSubs))
115
-
},
116
-
)
117
110
}
118
-
let upshift = (s, amount: int, ~from=?) =>
119
-
s->match(
120
-
left => Left(left->Left.upshift(amount, ~from?)),
121
-
right => Right(right->Right.upshift(amount, ~from?)),
122
-
)
123
-
let substDeBruijn = (s, substs: array<option<t>>, ~from=?) =>
124
-
s->match(
125
-
left => {
126
-
let leftSubs = substs->Array.map(o => o->Option.flatMap(coerceToLeft))
127
-
Left(Left.substDeBruijn(left, leftSubs, ~from?))
128
-
},
129
-
right => {
130
-
let rightSubs = substs->Array.map(o => o->Option.flatMap(coerceToRight))
131
-
Right(Right.substDeBruijn(right, rightSubs, ~from?))
132
-
},
111
+
let coerceToHead = (atom): option<Head.t> =>
112
+
atom->onHead(val => Some(val))->getOrElse(() => Head.coerce(atom))
113
+
let substitute = (atom, subst: subst) =>
114
+
atom
115
+
->onHead(val => {
116
+
let leftSubs = subst->Util.Map.filterMap((_, v) => coerceToHead(v))
117
+
Head.substitute(val, leftSubs)->HeadBase.wrap
118
+
})
119
+
->getOrElse(() => Tail.substitute(atom, subst))
120
+
121
+
let upshift = (atom, amount: int, ~from=?) =>
122
+
atom
123
+
->onHead(val => Head.upshift(val, amount, ~from?)->HeadBase.wrap)
124
+
->getOrElse(() => Tail.upshift(atom, amount, ~from?))
125
+
let substDeBruijn = (atom, substs: array<option<t>>, ~from=?) =>
126
+
atom
127
+
->onHead(val =>
128
+
Head.substDeBruijn(
129
+
val,
130
+
substs->Array.map(o => o->Option.flatMap(coerceToHead)),
131
+
~from?,
132
+
)->HeadBase.wrap
133
133
)
134
-
let concrete = s => s->match(Left.concrete, Right.concrete)
134
+
->getOrElse(() => Tail.substDeBruijn(atom, substs, ~from?))
135
+
let concrete = atom => atom->onHead(Head.concrete)->getOrElse(() => Tail.concrete(atom))
135
136
}
136
137
137
138
module type ATOM_VIEW = {
···
140
141
let make: props => React.element
141
142
}
142
143
144
+
module NilAtomListView: ATOM_VIEW with module Atom := NilAtomList = {
145
+
type props = {name: NilAtomList.t, scope: array<string>}
146
+
let make = _ => throw(AtomExpected)
147
+
}
148
+
143
149
module MakeAtomView = (
144
150
Left: ATOM,
145
151
LeftView: ATOM_VIEW with module Atom := Left,
146
-
Right: ATOM,
152
+
Right: ATOM_LIST,
147
153
RightView: ATOM_VIEW with module Atom := Right,
148
154
Combined: module type of CombineAtom(Left, Right),
149
-
): {
150
-
include ATOM_VIEW with module Atom := Combined
151
-
} => {
155
+
): (ATOM_VIEW with module Atom := Combined) => {
152
156
type props = {name: Combined.t, scope: array<string>}
153
157
let make = ({name, scope}: props) =>
154
-
name->Combined.match(
155
-
left => <LeftView name={left} scope />,
156
-
right => <RightView name={right} scope />,
157
-
)
158
+
name
159
+
->Combined.onHead(left => <LeftView name={left} scope />)
160
+
->Util.Option.getOrElse(() => <RightView name scope />)
158
161
}
159
162
160
163
module MakeAtomAndView = (
161
164
Left: ATOM,
162
165
LeftView: ATOM_VIEW with module Atom := Left,
163
-
Right: ATOM,
166
+
Right: ATOM_LIST,
164
167
RightView: ATOM_VIEW with module Atom := Right,
165
168
) => {
166
169
module Atom = CombineAtom(Left, Right)
+1
-1
src/RuleView.res
+1
-1
src/RuleView.res
+8
-2
src/Scratch.res
+8
-2
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
52
StringA.Atom,
47
53
StringA.AtomView,
48
-
Symbolic.Atom,
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)
-1
src/StringA.res
-1
src/StringA.res
+26
-13
src/StringAxiomSet.res
+26
-13
src/StringAxiomSet.res
···
1
1
open Component
2
+
open! Util
2
3
4
+
module Symbol = AtomDef.MakeAtomAndView(
5
+
Symbolic.Atom,
6
+
Symbolic.AtomView,
7
+
AtomDef.NilAtomList,
8
+
AtomDef.NilAtomListView,
9
+
)
3
10
module StringSymbol = AtomDef.MakeAtomAndView(
4
11
StringA.Atom,
5
12
StringA.AtomView,
6
-
Symbolic.Atom,
7
-
Symbolic.AtomView,
13
+
Symbol.Atom,
14
+
Symbol.AtomView,
8
15
)
16
+
9
17
module StringSExp = SExp.Make(StringSymbol.Atom)
10
18
module TermView = SExpView.Make(StringSymbol.Atom, StringSymbol.AtomView, StringSExp)
11
19
module JudgmentView = TermViewAsJudgmentView.Make(StringSExp, StringSExp, TermView)
···
42
50
| _ => None
43
51
}
44
52
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"))
49
-
}
50
53
let destructureOpt = (r: StringSExp.t): option<(StringA.Atom.t, string)> =>
51
54
switch r {
52
-
| Compound({subexps: [Atom(Left(s)), Atom(Right(name))]}) => Some((s, name))
55
+
| Compound({subexps: [Atom(AtomDef.HValue(tag1, s)), Atom(AtomDef.HValue(tag2, name))]}) =>
56
+
switch (tag1, tag2) {
57
+
| (StringA.BaseAtom.Tag, Symbolic.BaseAtom.Tag) => Some((s, name))
58
+
| _ => None
59
+
}
53
60
| _ => None
54
61
}
62
+
exception InvalidStringInductionPattern
63
+
let destructure = (r: StringSExp.t): (StringA.Atom.t, string) =>
64
+
destructureOpt(r)->Option.getOrElse(() => throw(InvalidStringInductionPattern))
55
65
let structure = (lhs: StringSExp.t, rhs: StringSExp.t): StringSExp.t => Compound({
56
66
subexps: [lhs, rhs],
57
67
})
···
114
124
vars: rule.vars,
115
125
premises: rule.premises->Array.concat(inductionHyps),
116
126
conclusion: structure(
117
-
surround(s, aIdx + baseIdx, bIdx + baseIdx)->Left->Atom,
127
+
Atom(AtomDef.HValue(StringA.BaseAtom.Tag, surround(s, aIdx + baseIdx, bIdx + baseIdx))),
118
128
Var({idx: pIdx + baseIdx}),
119
129
),
120
130
}
···
126
136
{
127
137
Rule.vars: [],
128
138
premises: [],
129
-
conclusion: structure(Var({idx: xIdx}), Atom(Right(group.name))),
139
+
conclusion: structure(
140
+
Var({idx: xIdx}),
141
+
Atom(AtomDef.HValue(Symbolic.BaseAtom.Tag, group.name)),
142
+
),
130
143
},
131
144
],
132
145
mentionedGroups->Array.flatMap(g => g.rules->Array.map(r => replaceJudgeRHS(r, 0))),
133
146
),
134
147
conclusion: structure(
135
-
surround([StringA.Var({idx: xIdx})], aIdx, bIdx)->Left->Atom,
148
+
Atom(HValue(StringA.BaseAtom.Tag, surround([StringA.Var({idx: xIdx})], aIdx, bIdx))),
136
149
Var({idx: 0}),
137
150
), // TODO: clean here
138
151
}
···
170
183
getBase(str)->Result.map(raw => {
171
184
let grouped: dict<array<Rule.t>> = Dict.make()
172
185
raw->Dict.forEach(rule =>
173
-
switch rule.conclusion {
174
-
| Compound({subexps: [Atom(Left(_)), Atom(Right(name))]}) =>
186
+
switch rule.conclusion->destructureOpt {
187
+
| Some((_, name)) =>
175
188
switch grouped->Dict.get(name) {
176
189
| None => grouped->Dict.set(name, [rule])
177
190
| Some(rs) => rs->Array.push(rule)
+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
+
}
+13
-10
tests/RuleTest.res
+13
-10
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
42
StringA.Atom,
37
43
StringA.AtomView,
38
-
Symbolic.Atom,
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.HValue(StringA.BaseAtom.Tag, s))
49
+
let wrapSymbol = (s): StringSExp.t => Atom(HValue(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
},