forked from
liamoc.net/holbert-ng
the next generation of the in-browser educational proof assistant
functorise StringAxiomSet
With the definition of a choice of atom now admitting a homogeneous
representation, we no longer need to make assumptions about the order
arguments are applied to CombineAtom in StringAxiomSet, so can make it a
functor.
authored by
Josh Brown
and committed by
Tangled
8665730b
33564d98
+205
-223
+4
-4
src/AtomDef.res
+4
-4
src/AtomDef.res
···
1
1
// type level stuff to enable well-typed coercions
2
2
type atomTag<_> = ..
3
-
type rec anyValue = HValue(atomTag<'a>, 'a): anyValue
3
+
type rec anyValue = AnyValue(atomTag<'a>, 'a): anyValue
4
4
5
5
// to allow circular coercions, we declare base types
6
6
// separately from relevant implementation
···
17
17
): (BASE_ATOM with type t = T.t) => {
18
18
type t = T.t
19
19
type atomTag<_> += Tag: atomTag<t>
20
-
let wrap = t => HValue(Tag, t)
20
+
let wrap = t => AnyValue(Tag, t)
21
21
}
22
22
23
23
module type ATOM = {
···
85
85
type gen = ref<int>
86
86
let getOrElse = Util.Option.getOrElse
87
87
let coerce = v => Some(v)
88
-
let onHead = (HValue(tag, val), f: Head.t => 'a): option<'a> =>
88
+
let onHead = (AnyValue(tag, val), f: Head.t => 'a): option<'a> =>
89
89
switch tag {
90
90
| Head.BaseAtom.Tag => Some(f(val))
91
91
| _ => None
···
101
101
->getOrElse(() => Tail.prettyPrint(atom, ~scope))
102
102
103
103
let unify = (a1, a2, ~gen=?) => {
104
-
let (HValue(tag1, val1), HValue(tag2, val2)) = (a1, a2)
104
+
let (AnyValue(tag1, val1), AnyValue(tag2, val2)) = (a1, a2)
105
105
switch (tag1, tag2) {
106
106
| (Head.BaseAtom.Tag, Head.BaseAtom.Tag) =>
107
107
Head.unify(val1, val2)->Seq.map(subst => subst->Util.mapMapValues(HeadBase.wrap))
+2
-2
src/SExp.res
+2
-2
src/SExp.res
···
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(AnyValue(AtomDef.SExpTag, AtomDef.Var({idx: idx})))
154
154
| Schematic({schematic, allowed}) =>
155
-
Atom.coerce(HValue(AtomDef.SExpTag, AtomDef.Schematic({schematic, allowed})))
155
+
Atom.coerce(AnyValue(AtomDef.SExpTag, AtomDef.Schematic({schematic, allowed})))
156
156
| Compound({subexps: [e1]}) => lower(e1)
157
157
| _ => None
158
158
}
+3
-1
src/Scratch.res
+3
-1
src/Scratch.res
···
57
57
module StringSExp = SExp.Make(StringSymbol.Atom)
58
58
module TermView = SExpView.Make(StringSymbol.Atom, StringSymbol.AtomView, StringSExp)
59
59
module StringSExpJView = TermViewAsJudgmentView.Make(StringSExp, StringSExp, TermView)
60
-
module AxiomStr = Editable.TextArea(StringAxiomSet)
60
+
module AxiomStr = Editable.TextArea(
61
+
StringAxiomSet.Make(StringSymbol.Atom, StringSExp, StringSExpJView),
62
+
)
61
63
62
64
module DerivationsOrLemmasStrView = MethodView.CombineMethodView(
63
65
StringSExp,
+1
-1
src/StringA.res
+1
-1
src/StringA.res
+192
-212
src/StringAxiomSet.res
+192
-212
src/StringAxiomSet.res
···
1
1
open Component
2
2
open! Util
3
3
4
-
module Symbol = AtomDef.MakeAtomAndView(
5
-
Symbolic.Atom,
6
-
Symbolic.AtomView,
7
-
AtomDef.NilAtomList,
8
-
AtomDef.NilAtomListView,
9
-
)
10
-
module StringSymbol = AtomDef.MakeAtomAndView(
11
-
StringA.Atom,
12
-
StringA.AtomView,
13
-
Symbol.Atom,
14
-
Symbol.AtomView,
15
-
)
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
+
}
16
16
17
-
module StringSExp = SExp.Make(StringSymbol.Atom)
18
-
module TermView = SExpView.Make(StringSymbol.Atom, StringSymbol.AtomView, StringSExp)
19
-
module JudgmentView = TermViewAsJudgmentView.Make(StringSExp, StringSExp, TermView)
17
+
type props = {
18
+
content: state,
19
+
imports: Ports.t,
20
+
onChange: (state, ~exports: Ports.t=?) => unit,
21
+
}
20
22
21
-
module Rule = Rule.Make(StringSExp, StringSExp)
22
-
module RuleView = RuleView.Make(StringSExp, StringSExp, JudgmentView)
23
-
module Ports = Ports(StringSExp, StringSExp)
24
-
type state = {
25
-
raw: dict<Rule.t>,
26
-
derived: dict<Rule.t>,
27
-
}
23
+
type judgeGroup = {
24
+
name: string,
25
+
rules: array<Rule.t>,
26
+
}
28
27
29
-
type props = {
30
-
content: state,
31
-
imports: Ports.t,
32
-
onChange: (state, ~exports: Ports.t=?) => unit,
33
-
}
34
-
35
-
type judgeGroup = {
36
-
name: string,
37
-
rules: array<Rule.t>,
38
-
}
39
-
40
-
module Set = Belt.Set.String
41
-
let varsInRule = (rule: Rule.t) => {
42
-
rule.premises->Array.reduce(Set.fromArray(rule.vars), (s, r) =>
43
-
s->Set.union(Set.fromArray(r.vars))
44
-
)
45
-
}
46
-
47
-
let getSExpName = (t: StringSExp.t): option<string> =>
48
-
switch t {
49
-
| Atom(name) => Some(name->StringSymbol.Atom.prettyPrint(~scope=[]))
50
-
| _ => 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
+
)
51
33
}
52
34
53
-
let destructureOpt = (r: StringSExp.t): option<(StringA.Atom.t, string)> =>
54
-
switch r {
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))
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
+
}
58
42
| _ => None
59
43
}
60
-
| _ => None
61
-
}
62
-
exception InvalidStringInductionPattern
63
-
let destructure = (r: StringSExp.t): (StringA.Atom.t, string) =>
64
-
destructureOpt(r)->Option.getOrElse(() => throw(InvalidStringInductionPattern))
65
-
let structure = (lhs: StringSExp.t, rhs: StringSExp.t): StringSExp.t => Compound({
66
-
subexps: [lhs, rhs],
67
-
})
68
-
let findMentionedRuleGroups = (group: judgeGroup, allGroups: array<judgeGroup>): array<
69
-
judgeGroup,
70
-
> => {
71
-
let allGroupNames = allGroups->Array.map(g => g.name)
72
-
let groupNames: array<string> = Array.concat(
73
-
[group.name],
74
-
group.rules
75
-
->Array.flatMap(r =>
76
-
r.premises
77
-
->Array.filterMap(p => p.conclusion->destructureOpt->Option.map(Pair.second))
78
-
->Array.filter(name => allGroupNames->Array.find(name' => name' == name)->Option.isSome)
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,
79
65
)
80
-
->Set.fromArray
81
-
->Set.remove(group.name)
82
-
->Set.toArray,
83
-
)
84
-
groupNames->Array.map(name => allGroups->Array.find(g => g.name == name))->Array.keepSome
85
-
}
66
+
groupNames->Array.map(name => allGroups->Array.find(g => g.name == name))->Array.keepSome
67
+
}
86
68
87
-
let derive = (group: judgeGroup, mentionedGroups: array<judgeGroup>): Rule.t => {
88
-
let allVars =
89
-
mentionedGroups
90
-
->Array.flatMap(g => g.rules)
91
-
->Array.reduce(Set.empty, (s, r) => s->Set.union(varsInRule(r)))
92
-
let rec genVar = (base: string) => {
93
-
if allVars->Set.has(base) {
94
-
genVar(`${base}'`)
95
-
} else {
96
-
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})])
97
89
}
98
-
}
99
-
let ps = mentionedGroups->Array.map(g => genVar(`P${g.name}`))
100
-
let (b, x, a) = (genVar("b"), genVar("x"), genVar("a"))
101
-
let vars = Array.concat(ps, [b, x, a])
102
-
let xIdx = vars->Array.findIndex(i => i == x)
103
-
let aIdx = vars->Array.findIndex(i => i == a)
104
-
let bIdx = vars->Array.findIndex(i => i == b)
105
-
let surround = (t: StringA.Atom.t, aIdx: int, bIdx: int) => {
106
-
Array.concat(Array.concat([StringA.Var({idx: aIdx})], t), [StringA.Var({idx: bIdx})])
107
-
}
108
-
let lookupGroup = (name: string): option<int> =>
109
-
mentionedGroups->Array.findIndexOpt(g => name == g.name)
110
-
let rec replaceJudgeRHS = (rule: Rule.t, baseIdx: int): Rule.t => {
111
-
let baseIdx = baseIdx + Array.length(rule.vars)
112
-
let (s, name) = destructure(rule.conclusion)
113
-
let inductionHyps =
114
-
rule.premises
115
-
->Array.filter(r =>
116
-
r.conclusion
117
-
->destructureOpt
118
-
->Option.flatMap(conclusion => conclusion->Pair.second->lookupGroup)
119
-
->Option.isSome
120
-
)
121
-
->Array.map(r => replaceJudgeRHS(r, baseIdx))
122
-
let pIdx = lookupGroup(name)->Option.getExn
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
+
}
113
+
}
123
114
{
124
-
vars: rule.vars,
125
-
premises: rule.premises->Array.concat(inductionHyps),
126
-
conclusion: structure(
127
-
Atom(AtomDef.HValue(StringA.BaseAtom.Tag, surround(s, aIdx + baseIdx, bIdx + baseIdx))),
128
-
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))),
129
125
),
126
+
conclusion: structure(
127
+
Atom(surround([Var({idx: xIdx})], aIdx, bIdx)->StringA.BaseAtom.wrap),
128
+
Var({idx: 0}),
129
+
), // TODO: clean here
130
130
}
131
131
}
132
-
{
133
-
vars,
134
-
premises: Array.concat(
135
-
[
136
-
{
137
-
Rule.vars: [],
138
-
premises: [],
139
-
conclusion: structure(
140
-
Var({idx: xIdx}),
141
-
Atom(AtomDef.HValue(Symbolic.BaseAtom.Tag, group.name)),
142
-
),
143
-
},
144
-
],
145
-
mentionedGroups->Array.flatMap(g => g.rules->Array.map(r => replaceJudgeRHS(r, 0))),
146
-
),
147
-
conclusion: structure(
148
-
Atom(HValue(StringA.BaseAtom.Tag, surround([StringA.Var({idx: xIdx})], aIdx, bIdx))),
149
-
Var({idx: 0}),
150
-
), // TODO: clean here
151
-
}
152
-
}
153
132
154
-
let deserialise = (str: string, ~imports as _: Ports.t) => {
155
-
let getBase = (str: string) => {
156
-
let cur = ref(str)
157
-
let go = ref(true)
158
-
let results = Dict.make()
159
-
let ret = ref(Error("impossible"))
160
-
while go.contents {
161
-
switch Rule.parseTopLevel(cur.contents, ~scope=[]) {
162
-
| Ok((t, n), rest) =>
163
-
if n->String.trim == "" {
164
-
go := false
165
-
ret := Error("Rule given with no name")
166
-
} else {
167
-
Dict.set(results, n, t)
168
-
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 == "" {
169
143
go := false
170
-
ret := Ok(results)
144
+
ret := Error("Rule given with no name")
171
145
} else {
172
-
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
+
}
153
+
}
154
+
| Error(e) => {
155
+
go := false
156
+
ret := Error(e)
173
157
}
174
158
}
175
-
| Error(e) => {
176
-
go := false
177
-
ret := Error(e)
178
-
}
179
159
}
160
+
ret.contents
180
161
}
181
-
ret.contents
182
-
}
183
-
getBase(str)->Result.map(raw => {
184
-
let grouped: dict<array<Rule.t>> = Dict.make()
185
-
raw->Dict.forEach(rule =>
186
-
switch rule.conclusion->destructureOpt {
187
-
| Some((_, name)) =>
188
-
switch grouped->Dict.get(name) {
189
-
| None => grouped->Dict.set(name, [rule])
190
-
| 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
+
| _ => ()
191
172
}
192
-
| _ => ()
193
-
}
194
-
)
195
-
let allGroups = grouped->Dict.toArray->Array.map(((name, rules)) => {name, rules})
196
-
let derived: Dict.t<Rule.t> = Dict.make()
197
-
allGroups->Array.forEach(group => {
198
-
// NOTE: this can clash with other names. is this an issue?
199
-
derived->Dict.set(`${group.name}_induct`, derive(group, [group]))
200
-
let mentionedGroups = findMentionedRuleGroups(group, allGroups)
201
-
if mentionedGroups->Array.length > 1 {
202
-
derived->Dict.set(`${group.name}_mutualInduct`, derive(group, mentionedGroups))
203
-
}
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})
204
185
})
205
-
({raw, derived}, {Ports.facts: raw->Dict.copy->Dict.assign(derived), ruleStyle: None})
206
-
})
207
-
}
186
+
}
208
187
209
-
let serialise = (state: state) => {
210
-
state.raw
211
-
->Dict.toArray
212
-
->Array.map(((k, r)) => r->Rule.prettyPrintTopLevel(~name=k))
213
-
->Array.join("\n")
214
-
}
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
+
}
215
194
216
-
let make = props => {
217
-
let makeRules = content =>
218
-
<div
219
-
className={"axiom-set axiom-set-"->String.concat(
220
-
String.make(props.imports.ruleStyle->Option.getOr(Hybrid)),
221
-
)}
222
-
>
223
-
{content
224
-
->Dict.toArray
225
-
->Array.mapWithIndex(((n, r), i) =>
226
-
<RuleView
227
-
rule={r}
228
-
scope={[]}
229
-
key={String.make(i)}
230
-
style={props.imports.ruleStyle->Option.getOr(Hybrid)}
231
-
>
232
-
{React.string(n)}
233
-
</RuleView>
234
-
)
235
-
->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)}
236
220
</div>
237
-
<div>
238
-
{makeRules(props.content.raw)}
239
-
<p> {React.string("derived")} </p>
240
-
{makeRules(props.content.derived)}
241
-
</div>
221
+
}
242
222
}
+1
-1
src/Symbolic.res
+1
-1
src/Symbolic.res
+2
-2
tests/RuleTest.res
+2
-2
tests/RuleTest.res
···
45
45
Symbol.AtomView,
46
46
)
47
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))
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))
50
50
module T = MakeTest(StringSExp, StringSExp)
51
51
t->T.testParseInner(
52
52
`[s1. ("$s1" p) |- ("($s1)" p)]`,