the next generation of the in-browser educational proof assistant
restore original judgment signature
+193
-205
+1
src/HOTerm.res
+1
src/HOTerm.res
+1
src/HOTerm.resi
+1
src/HOTerm.resi
+1
-3
src/HOTermJView.resi
+1
-3
src/HOTermJView.resi
+13
-17
src/HOTermMethod.res
+13
-17
src/HOTermMethod.res
···
2
2
open Method
3
3
4
4
module MakeRewriteHOTerm = (
5
-
Judgment: JUDGMENT with module Term := HOTerm and type subst = HOTerm.subst and type t = HOTerm.t,
5
+
Judgment: JUDGMENT with module Term := HOTerm and type t = HOTerm.t,
6
6
Config: {
7
7
let keyword: string
8
8
let reversed: bool
···
43
43
44
44
type t<'a> = {
45
45
equalityName: string,
46
-
instantiation: array<Judgment.substCodom>,
46
+
instantiation: array<Term.t>,
47
47
subgoal: 'a,
48
48
}
49
49
···
57
57
}
58
58
}
59
59
60
-
let substitute = (it: t<'a>, subst: Judgment.subst) => {
60
+
let substitute = (it: t<'a>, subst: Term.subst) => {
61
61
{
62
62
equalityName: it.equalityName,
63
-
instantiation: it.instantiation->Array.map(t => t->Judgment.substituteSubstCodom(subst)),
63
+
instantiation: it.instantiation->Array.map(t => t->Judgment.substitute(subst)),
64
64
subgoal: it.subgoal,
65
65
}
66
66
}
···
72
72
~subprinter: ('a, ~scope: array<HOTerm.meta>, ~indentation: int=?) => string,
73
73
) => {
74
74
let ind = String.repeat(" ", indentation)
75
-
let args = it.instantiation->Array.map(t => Judgment.prettyPrintSubstCodom(t, ~scope))
75
+
let args = it.instantiation->Array.map(t => Term.prettyPrint(t, ~scope))
76
76
let argsStr = if Array.length(args) > 0 {
77
77
" " ++ Array.join(args, " ")
78
78
} else {
···
98
98
let instantiation = []
99
99
let it = ref(Error(""))
100
100
while {
101
-
it := Judgment.parseSubstCodom(cur.contents, ~scope, ~gen)
101
+
it := Term.parse(cur.contents, ~scope, ~gen)
102
102
it.contents->Result.isOk
103
103
} {
104
104
let (val, rest) = it.contents->Result.getExn
···
157
157
}
158
158
159
159
let apply = (ctx: Context.t, j: Judgment.t, gen: HOTerm.gen, f: Rule.t => 'a) => {
160
-
let ret: Dict.t<(t<'a>, Judgment.subst)> = Dict.make()
160
+
let ret: Dict.t<(t<'a>, Term.subst)> = Dict.make()
161
161
162
162
ctx
163
163
->Context.facts
···
246
246
}
247
247
248
248
module Rewrite = (
249
-
Judgment: JUDGMENT with module Term := HOTerm and type subst = HOTerm.subst and type t = HOTerm.t,
249
+
Judgment: JUDGMENT with module Term := HOTerm and type t = HOTerm.t,
250
250
) => MakeRewriteHOTerm(
251
251
Judgment,
252
252
{
···
256
256
)
257
257
258
258
module RewriteReverse = (
259
-
Judgment: JUDGMENT with module Term := HOTerm and type subst = HOTerm.subst and type t = HOTerm.t,
259
+
Judgment: JUDGMENT with module Term := HOTerm and type t = HOTerm.t,
260
260
) => MakeRewriteHOTerm(
261
261
Judgment,
262
262
{
···
265
265
},
266
266
)
267
267
268
-
module ConstructorNeq = (
269
-
Judgment: JUDGMENT with module Term := HOTerm and type subst = HOTerm.subst and type t = HOTerm.t,
270
-
) => {
268
+
module ConstructorNeq = (Judgment: JUDGMENT with module Term := HOTerm and type t = HOTerm.t) => {
271
269
module Term = HOTerm
272
270
module Rule = Rule.Make(HOTerm, Judgment)
273
271
module Context = Context(HOTerm, Judgment)
···
321
319
322
320
let map = (it: t<'a>, _f: 'a => 'b): t<'b> => it
323
321
324
-
let substitute = (it: t<'a>, _subst: Judgment.subst) => it
322
+
let substitute = (it: t<'a>, _subst: Term.subst) => it
325
323
326
324
let prettyPrint = (_it: t<'a>, ~scope as _, ~indentation=0, ~subprinter as _) =>
327
325
String.repeat(" ", indentation)->String.concat("constructor_neq")
···
353
351
}
354
352
}
355
353
356
-
module ConstructorInj = (
357
-
Judgment: JUDGMENT with module Term := HOTerm and type subst = HOTerm.subst and type t = HOTerm.t,
358
-
) => {
354
+
module ConstructorInj = (Judgment: JUDGMENT with module Term := HOTerm and type t = HOTerm.t) => {
359
355
module Rule = Rule.Make(HOTerm, Judgment)
360
356
module Context = Context(HOTerm, Judgment)
361
357
···
370
366
371
367
let map = (it: t<'a>, _f: 'a => 'b): t<'b> => it
372
368
373
-
let substitute = (it: t<'a>, _subst: Judgment.subst) => it
369
+
let substitute = (it: t<'a>, _subst: HOTerm.subst) => it
374
370
375
371
let prettyPrint = (it: t<'a>, ~scope as _, ~indentation=0, ~subprinter as _) =>
376
372
String.repeat(" ", indentation)->String.concat(
+15
-15
src/Method.res
+15
-15
src/Method.res
···
16
16
module Context: module type of Context(Term, Judgment)
17
17
type t<'a>
18
18
let keywords: array<string>
19
-
let substitute: (t<'a>, Judgment.subst) => t<'a>
19
+
let substitute: (t<'a>, Term.subst) => t<'a>
20
20
let check: (t<'a>, Context.t, Judgment.t, ('a, Rule.t) => 'b) => result<t<'b>, string>
21
-
let apply: (Context.t, Judgment.t, Term.gen, Rule.t => 'a) => Dict.t<(t<'a>, Judgment.subst)>
21
+
let apply: (Context.t, Judgment.t, Term.gen, Rule.t => 'a) => Dict.t<(t<'a>, Term.subst)>
22
22
let map: (t<'a>, 'a => 'b) => t<'b>
23
23
let parse: (
24
24
string,
···
43
43
module Context = Context(Term, Judgment)
44
44
type t<'a> = {
45
45
ruleName: string,
46
-
instantiation: array<Judgment.substCodom>,
46
+
instantiation: array<Term.t>,
47
47
subgoals: array<'a>,
48
48
}
49
49
let map = (it: t<'a>, f) => {
···
53
53
subgoals: it.subgoals->Array.map(f),
54
54
}
55
55
}
56
-
let substitute = (it: t<'a>, subst: Judgment.subst) => {
56
+
let substitute = (it: t<'a>, subst: Term.subst) => {
57
57
{
58
58
ruleName: it.ruleName,
59
-
instantiation: it.instantiation->Array.map(t => t->Judgment.substituteSubstCodom(subst)),
59
+
instantiation: it.instantiation->Array.map(t => t->Term.substitute(subst)),
60
60
subgoals: it.subgoals,
61
61
}
62
62
}
···
68
68
~indentation=0,
69
69
~subprinter: ('a, ~scope: array<Term.meta>, ~indentation: int=?) => string,
70
70
) => {
71
-
let args = it.instantiation->Array.map(t => Judgment.prettyPrintSubstCodom(t, ~scope))
71
+
let args = it.instantiation->Array.map(t => Term.prettyPrint(t, ~scope))
72
72
"by ("
73
73
->String.concat(Array.join([it.ruleName]->Array.concat(args), " "))
74
74
->String.concat(") {")
···
95
95
let instantiation = []
96
96
let it = ref(Error(""))
97
97
while {
98
-
it := Judgment.parseSubstCodom(cur.contents, ~scope, ~gen)
98
+
it := Term.parse(cur.contents, ~scope, ~gen)
99
99
it.contents->Result.isOk
100
100
} {
101
101
let (val, rest) = it.contents->Result.getExn
···
147
147
->Array.filterMap(((key, rule)) => {
148
148
let insts = rule->Rule.genSchemaInsts(gen, ~scope=ctx.fixes)
149
149
let res = rule->Rule.instantiate(insts)
150
-
let ghostSubs = Judgment.unify(Judgment.ghostJudgment, res.conclusion)
150
+
let ghostSubs = Judgment.unify(Judgment.ghostTerm, res.conclusion)
151
151
if ghostSubs->Seq.head->Option.isNone {
152
152
Some((key, res, insts))
153
153
} else {
···
212
212
type t<'a> = {
213
213
ruleName: string,
214
214
elimName: string,
215
-
instantiation: array<Judgment.substCodom>,
215
+
instantiation: array<Term.t>,
216
216
subgoals: array<'a>,
217
217
}
218
218
exception InternalParseError(string)
···
229
229
""
230
230
}
231
231
let instantiation = Array.join(
232
-
it.instantiation->Array.map(t => Judgment.prettyPrintSubstCodom(t, ~scope)),
232
+
it.instantiation->Array.map(t => Term.prettyPrint(t, ~scope)),
233
233
" ",
234
234
)
235
235
let subgoalsStr =
···
248
248
}
249
249
}
250
250
251
-
let substitute = (it: t<'a>, subst: Judgment.subst) => {
251
+
let substitute = (it: t<'a>, subst: Term.subst) => {
252
252
{
253
253
ruleName: it.ruleName,
254
254
elimName: it.elimName,
255
-
instantiation: it.instantiation->Array.map(t => t->Judgment.substituteSubstCodom(subst)),
255
+
instantiation: it.instantiation->Array.map(t => t->Term.substitute(subst)),
256
256
subgoals: it.subgoals,
257
257
}
258
258
}
···
270
270
let instantiation = []
271
271
let it = ref(Error(""))
272
272
while {
273
-
it := Judgment.parseSubstCodom(cur.contents, ~scope, ~gen)
273
+
it := Term.parse(cur.contents, ~scope, ~gen)
274
274
it.contents->Result.isOk
275
275
} {
276
276
let (val, rest) = it.contents->Result.getExn
···
394
394
instantiation: ruleInsts,
395
395
subgoals: rule.premises->Array.sliceToEnd(~start=1)->Array.map(f),
396
396
}
397
-
let subst = Judgment.mergeSubsts(elimSub, ruleSub)
397
+
let subst = Term.mergeSubsts(elimSub, ruleSub)
398
398
ret->Dict.set(`elim ${ruleName} with ${elimName}`, (new, subst))
399
399
},
400
400
)
···
421
421
show: f(it.show),
422
422
}
423
423
}
424
-
let substitute = (it: t<'a>, subst: Judgment.subst) => {
424
+
let substitute = (it: t<'a>, subst: Term.subst) => {
425
425
{
426
426
rule: it.rule->Rule.substitute(subst),
427
427
proof: it.proof,
+25
-27
src/MethodView.res
+25
-27
src/MethodView.res
···
10
10
scope: array<Term.meta>,
11
11
ruleStyle: RuleView.style,
12
12
gen: Term.gen,
13
-
onChange: (Method.t<'a>, Judgment.subst) => unit,
13
+
onChange: (Method.t<'a>, Term.subst) => unit,
14
14
}
15
15
type srProps<'a> = {
16
16
"proof": 'a,
17
17
"scope": array<Term.meta>,
18
18
"ruleStyle": RuleView.style,
19
19
"gen": Term.gen,
20
-
"onChange": ('a, Judgment.subst) => unit,
20
+
"onChange": ('a, Term.subst) => unit,
21
21
}
22
22
let make: (srProps<'a> => React.element) => props<'a> => React.element
23
23
}
···
29
29
scope: array<Term.meta>,
30
30
ruleStyle: RuleView.style,
31
31
gen: Term.gen,
32
-
onChange: (Method.t<'a>, Judgment.subst) => unit,
32
+
onChange: (Method.t<'a>, Term.subst) => unit,
33
33
}
34
34
type srProps<'a> = {
35
35
"proof": 'a,
36
36
"scope": array<Term.meta>,
37
37
"ruleStyle": RuleView.style,
38
38
"gen": Term.gen,
39
-
"onChange": ('a, Judgment.subst) => unit,
39
+
"onChange": ('a, Term.subst) => unit,
40
40
}
41
41
let make = (subRender: srProps<'a> => React.element) =>
42
42
props => {
···
54
54
"scope": props.scope,
55
55
"ruleStyle": props.ruleStyle,
56
56
"gen": props.gen,
57
-
"onChange": (newa, subst: Judgment.subst) =>
57
+
"onChange": (newa, subst: Term.subst) =>
58
58
props.onChange(props.method->Method.updateAtKey(i, _ => newa), subst),
59
59
},
60
60
)}
···
73
73
scope: array<Term.meta>,
74
74
ruleStyle: RuleView.style,
75
75
gen: Term.gen,
76
-
onChange: (Method.t<'a>, Judgment.subst) => unit,
76
+
onChange: (Method.t<'a>, Term.subst) => unit,
77
77
}
78
78
type srProps<'a> = {
79
79
"proof": 'a,
80
80
"scope": array<Term.meta>,
81
81
"ruleStyle": RuleView.style,
82
82
"gen": Term.gen,
83
-
"onChange": ('a, Judgment.subst) => unit,
83
+
"onChange": ('a, Term.subst) => unit,
84
84
}
85
85
let make = (subRender: srProps<'a> => React.element) =>
86
86
props => {
···
98
98
"scope": props.scope,
99
99
"ruleStyle": props.ruleStyle,
100
100
"gen": props.gen,
101
-
"onChange": (newa, subst: Judgment.subst) =>
101
+
"onChange": (newa, subst: Term.subst) =>
102
102
props.onChange(props.method->Method.updateAtKey(i, _ => newa), subst),
103
103
},
104
104
)}
···
121
121
scope: array<Term.meta>,
122
122
ruleStyle: RuleView.style,
123
123
gen: Term.gen,
124
-
onChange: (Method.t<'a>, Judgment.subst) => unit,
124
+
onChange: (Method.t<'a>, Term.subst) => unit,
125
125
}
126
126
type srProps<'a> = {
127
127
"proof": 'a,
128
128
"scope": array<Term.meta>,
129
129
"ruleStyle": RuleView.style,
130
130
"gen": Term.gen,
131
-
"onChange": ('a, Judgment.subst) => unit,
131
+
"onChange": ('a, Term.subst) => unit,
132
132
}
133
133
module RuleView = RuleView.Make(Term, Judgment, JudgmentView)
134
134
let make = (subRender: srProps<'a> => React.element) =>
···
162
162
}
163
163
}
164
164
165
-
module RewriteView = (
166
-
Judgment: JUDGMENT with module Term := HOTerm and type subst = HOTerm.subst and type t = HOTerm.t,
167
-
) => {
165
+
module RewriteView = (Judgment: JUDGMENT with module Term := HOTerm and type t = HOTerm.t) => {
168
166
module Method = Rewrite(Judgment)
169
167
type props<'a> = {
170
168
method: Method.t<'a>,
171
169
scope: array<HOTerm.meta>,
172
170
ruleStyle: RuleView.style,
173
171
gen: HOTerm.gen,
174
-
onChange: (Method.t<'a>, Judgment.subst) => unit,
172
+
onChange: (Method.t<'a>, HOTerm.subst) => unit,
175
173
}
176
174
type srProps<'a> = {
177
175
"proof": 'a,
178
176
"scope": array<HOTerm.meta>,
179
177
"ruleStyle": RuleView.style,
180
178
"gen": HOTerm.gen,
181
-
"onChange": ('a, Judgment.subst) => unit,
179
+
"onChange": ('a, HOTerm.subst) => unit,
182
180
}
183
181
let make = (subRender: srProps<'a> => React.element) =>
184
182
props => {
···
194
192
"scope": props.scope,
195
193
"ruleStyle": props.ruleStyle,
196
194
"gen": props.gen,
197
-
"onChange": (subgoal, subst: Judgment.subst) =>
195
+
"onChange": (subgoal, subst: HOTerm.subst) =>
198
196
props.onChange({...props.method, subgoal}, subst),
199
197
},
200
198
)}
···
205
203
}
206
204
207
205
module RewriteReverseView = (
208
-
Judgment: JUDGMENT with module Term := HOTerm and type subst = HOTerm.subst and type t = HOTerm.t,
206
+
Judgment: JUDGMENT with module Term := HOTerm and type t = HOTerm.t,
209
207
) => {
210
208
module Method = RewriteReverse(Judgment)
211
209
type props<'a> = {
···
213
211
scope: array<HOTerm.meta>,
214
212
ruleStyle: RuleView.style,
215
213
gen: HOTerm.gen,
216
-
onChange: (Method.t<'a>, Judgment.subst) => unit,
214
+
onChange: (Method.t<'a>, HOTerm.subst) => unit,
217
215
}
218
216
type srProps<'a> = {
219
217
"proof": 'a,
220
218
"scope": array<HOTerm.meta>,
221
219
"ruleStyle": RuleView.style,
222
220
"gen": HOTerm.gen,
223
-
"onChange": ('a, Judgment.subst) => unit,
221
+
"onChange": ('a, HOTerm.subst) => unit,
224
222
}
225
223
let make = (subRender: srProps<'a> => React.element) =>
226
224
props => {
···
236
234
"scope": props.scope,
237
235
"ruleStyle": props.ruleStyle,
238
236
"gen": props.gen,
239
-
"onChange": (subgoal, subst: Judgment.subst) =>
237
+
"onChange": (subgoal, subst: HOTerm.subst) =>
240
238
props.onChange({...props.method, subgoal}, subst),
241
239
},
242
240
)}
···
247
245
}
248
246
249
247
module ConstructorNeqView = (
250
-
Judgment: JUDGMENT with module Term := HOTerm and type subst = HOTerm.subst and type t = HOTerm.t,
248
+
Judgment: JUDGMENT with module Term := HOTerm and type t = HOTerm.t,
251
249
) => {
252
250
module Method = ConstructorNeq(Judgment)
253
251
type props<'a> = {
···
255
253
scope: array<HOTerm.meta>,
256
254
ruleStyle: RuleView.style,
257
255
gen: HOTerm.gen,
258
-
onChange: (Method.t<'a>, Judgment.subst) => unit,
256
+
onChange: (Method.t<'a>, HOTerm.subst) => unit,
259
257
}
260
258
type srProps<'a> = {
261
259
"proof": 'a,
262
260
"scope": array<HOTerm.meta>,
263
261
"ruleStyle": RuleView.style,
264
262
"gen": HOTerm.gen,
265
-
"onChange": ('a, Judgment.subst) => unit,
263
+
"onChange": ('a, HOTerm.subst) => unit,
266
264
}
267
265
let make = (_subRender: srProps<'a> => React.element) =>
268
266
_props => {
···
273
271
}
274
272
275
273
module ConstructorInjView = (
276
-
Judgment: JUDGMENT with module Term := HOTerm and type subst = HOTerm.subst and type t = HOTerm.t,
274
+
Judgment: JUDGMENT with module Term := HOTerm and type t = HOTerm.t,
277
275
) => {
278
276
module Method = ConstructorInj(Judgment)
279
277
type props<'a> = {
···
281
279
scope: array<HOTerm.meta>,
282
280
ruleStyle: RuleView.style,
283
281
gen: HOTerm.gen,
284
-
onChange: (Method.t<'a>, Judgment.subst) => unit,
282
+
onChange: (Method.t<'a>, HOTerm.subst) => unit,
285
283
}
286
284
type srProps<'a> = {
287
285
"proof": 'a,
288
286
"scope": array<HOTerm.meta>,
289
287
"ruleStyle": RuleView.style,
290
288
"gen": HOTerm.gen,
291
-
"onChange": ('a, Judgment.subst) => unit,
289
+
"onChange": ('a, HOTerm.subst) => unit,
292
290
}
293
291
let make = (_subRender: srProps<'a> => React.element) =>
294
292
props => {
···
317
315
scope: array<Term.meta>,
318
316
ruleStyle: RuleView.style,
319
317
gen: Term.gen,
320
-
onChange: (Method.t<'a>, Judgment.subst) => unit,
318
+
onChange: (Method.t<'a>, Term.subst) => unit,
321
319
}
322
320
type srProps<'a> = Method1View.srProps<'a>
323
321
let make = (subrender: srProps<'a> => React.element) =>
+3
-3
src/Proof.res
+3
-3
src/Proof.res
···
24
24
| ProofError({raw: t, rule: Rule.t, msg: string})
25
25
and checked_option_method =
26
26
| Do(Method.t<checked>)
27
-
| Goal(Term.gen => Dict.t<(Method.t<checked>, Judgment.subst)>)
27
+
| Goal(Term.gen => Dict.t<(Method.t<checked>, Term.subst)>)
28
28
let parseKeyword = input => {
29
29
Method.keywords
30
30
->Array.concat(["?"])
31
31
->Array.find(kw => String.trim(input)->String.startsWith(kw))
32
32
}
33
-
let rec substitute = (prf: t, subst: Judgment.subst) => {
33
+
let rec substitute = (prf: t, subst: Term.subst) => {
34
34
fixes: prf.fixes,
35
35
assumptions: prf.assumptions,
36
36
method: prf.method->Option.map(m =>
···
191
191
}
192
192
} // result<checked,string>
193
193
194
-
let substituteChecked = (prf: checked, ctx: Context.t, subst: Judgment.subst) => {
194
+
let substituteChecked = (prf: checked, ctx: Context.t, subst: Term.subst) => {
195
195
switch prf {
196
196
| Checked(prf) =>
197
197
check(ctx, Checked(prf)->uncheck->substitute(subst), prf.rule->Rule.substitute(subst))
+27
-17
src/ProofView.res
+27
-17
src/ProofView.res
···
19
19
scope: array<Term.meta>,
20
20
ruleStyle: RuleView.style,
21
21
gen: Term.gen,
22
-
onChange: (Proof.checked, Judgment.subst) => unit,
22
+
onChange: (Proof.checked, Term.subst) => unit,
23
23
}
24
24
module RuleView = RuleView.Make(Term, Judgment, JudgmentView)
25
25
@react.componentWithProps
26
26
let rec make = (props: props) => {
27
27
let {sidebarRef} = React.useContext(SidebarContext.context)
28
28
let (isFocused, setFocused) = React.useState(() => false)
29
-
29
+
30
30
let onBlur = e => {
31
-
let leavingProof = ReactEvent.Focus.relatedTarget(e)
31
+
let leavingProof =
32
+
ReactEvent.Focus.relatedTarget(e)
32
33
->Option.flatMap(el => el->closest(".sidebar")->Nullable.toOption)
33
34
->Option.isNone
34
35
if leavingProof {
···
53
54
| Goal(options) =>
54
55
let portal = switch sidebarRef.current->Nullable.toOption {
55
56
| None => React.null
56
-
| Some(node) => Portal.createPortal(<> {
57
-
options(props.gen)
57
+
| Some(node) =>
58
+
Portal.createPortal(
59
+
<>
60
+
{options(props.gen)
58
61
->Dict.toArray
59
62
->Array.map(((str, (opt, subst))) => {
60
-
<button tabIndex=0 onBlur
63
+
<button
64
+
tabIndex=0
65
+
onBlur
61
66
key=str
62
67
onClick={_ =>
63
68
props.onChange(
···
68
73
{React.string(str)}
69
74
</button>
70
75
})
71
-
->React.array }
72
-
</>, node)
76
+
->React.array}
77
+
</>,
78
+
node,
79
+
)
73
80
}
74
-
<div className="proof-goal" tabIndex=0
81
+
<div
82
+
className="proof-goal"
83
+
tabIndex=0
75
84
onBlur
76
85
onFocus={e => {
77
86
setFocused(_ => true)
78
87
ReactEvent.Focus.stopPropagation(e)
79
-
}}>
80
-
{if (isFocused) {
81
-
<>
82
-
<span className="button-icon button-icon-blue typcn typcn-location" />
83
-
{portal}
84
-
</>
85
-
} else {
86
-
<span className="button-icon button-icon-blue typcn typcn-location-outline" />
88
+
}}
89
+
>
90
+
{if isFocused {
91
+
<>
92
+
<span className="button-icon button-icon-blue typcn typcn-location" />
93
+
{portal}
94
+
</>
95
+
} else {
96
+
<span className="button-icon button-icon-blue typcn typcn-location-outline" />
87
97
}}
88
98
</div>
89
99
| Do(method) =>
+8
-9
src/Rule.res
+8
-9
src/Rule.res
···
5
5
let vinculumRES = "^\s*\\n\\s*[-—][-—][\\-—]+[ \t]*([^()|\\s\\-—][^()\\s]*)?"
6
6
module Make = (Term: TERM, Judgment: JUDGMENT with module Term := Term) => {
7
7
type rec t = {vars: array<Term.meta>, premises: array<t>, conclusion: Judgment.t}
8
-
let rec substitute = (rule: t, subst: Judgment.subst) => {
9
-
let subst' =
10
-
subst->Judgment.mapSubst(v => v->Judgment.upshiftSubstCodom(Array.length(rule.vars)))
8
+
let rec substitute = (rule: t, subst: Term.subst) => {
9
+
let subst' = subst->Term.mapSubst(v => v->Term.upshift(Array.length(rule.vars)))
11
10
{
12
11
vars: rule.vars,
13
12
premises: rule.premises->Array.map(premise => premise->substitute(subst')),
14
13
conclusion: rule.conclusion->Judgment.substitute(subst')->Judgment.reduce,
15
14
}
16
15
}
17
-
let rec substDeBruijn = (rule: t, substs: array<Judgment.substCodom>, ~from: int=0) => {
16
+
let rec substDeBruijn = (rule: t, substs: array<Term.t>, ~from: int=0) => {
18
17
let len = Array.length(rule.vars)
19
-
let substs' = substs->Array.map(v => v->Judgment.upshiftSubstCodom(len, ~from))
18
+
let substs' = substs->Array.map(v => v->Term.upshift(len, ~from))
20
19
{
21
20
vars: rule.vars,
22
21
premises: rule.premises->Array.map(premise =>
···
36
35
}
37
36
}
38
37
type bare = {premises: array<t>, conclusion: Judgment.t}
39
-
let substituteBare = (rule: bare, subst: Judgment.subst) => {
38
+
let substituteBare = (rule: bare, subst: Term.subst) => {
40
39
{
41
40
premises: rule.premises->Array.map(premise => premise->substitute(subst)),
42
41
conclusion: rule.conclusion->Judgment.substitute(subst)->Judgment.reduce,
43
42
}
44
43
}
45
-
let instantiate = (rule: t, terms: array<Judgment.substCodom>) => {
44
+
let instantiate = (rule: t, terms: array<Term.t>) => {
46
45
assert(Array.length(terms) == Array.length(rule.vars))
47
46
let terms' = [...terms]
48
47
Array.reverse(terms')
···
51
50
conclusion: rule.conclusion->Judgment.substDeBruijn(terms')->Judgment.reduce,
52
51
}
53
52
}
54
-
let genSchemaInsts = (rule: t, gen: Term.gen, ~scope: array<Judgment.meta>) => {
55
-
rule.vars->Array.map(m => Judgment.placeSubstCodom(gen->Term.fresh(~replacing=m), ~scope))
53
+
let genSchemaInsts = (rule: t, gen: Term.gen, ~scope: array<Term.meta>) => {
54
+
rule.vars->Array.map(m => Term.place(gen->Term.fresh(~replacing=m), ~scope))
56
55
}
57
56
let parseRuleName = str => {
58
57
let re = RegExp.fromStringWithFlags(ruleNamePattern, ~flags="y")
-3
src/SExp.res
-3
src/SExp.res
+18
-7
src/SExp.resi
+18
-7
src/SExp.resi
···
1
-
// TODO: i only added the with type t = string later.
2
-
// may remove need for helpers down bottom
3
-
module ConstSymbol: SExpFunc.SYMBOL with type t = string
1
+
// NOTE: ideally we want something like:
2
+
// include module type of SExpFunc.Make(ConstSymbol)
3
+
// this doesn't work because reasons. can come back to revisit
4
+
// but i honestly suspect this is a rescript compiler bug.
5
+
6
+
module Symbol: SExpFunc.SYMBOL with type t = string
7
+
type rec t =
8
+
| Symbol(Symbol.t)
9
+
| Compound({subexps: array<t>})
10
+
| Var({idx: int})
11
+
| Schematic({schematic: int, allowed: array<int>})
12
+
| Ghost
4
13
5
-
include module type of SExpFunc.Make(ConstSymbol)
6
-
let symbol: string => t
7
-
let pSymbol: string => ConstSymbol.t
8
-
let getSymbol: ConstSymbol.t => string
14
+
include Signatures.TERM
15
+
with type t := t
16
+
and type meta = string
17
+
and type schematic = int
18
+
and type subst = Map.t<int, t>
19
+
let mapTerms: (t, t => t) => t
+5
-1
src/SExpFunc.res
+5
-1
src/SExpFunc.res
···
18
18
})
19
19
20
20
module Make = (Symbol: SYMBOL): {
21
+
module Symbol: SYMBOL with type t = Symbol.t
22
+
21
23
type rec t =
22
24
| Symbol(Symbol.t)
23
25
| Compound({subexps: array<t>})
24
26
| Var({idx: int})
25
27
| Schematic({schematic: int, allowed: array<int>})
26
28
| Ghost
27
-
module Symbol: SYMBOL with type t := Symbol.t
29
+
28
30
include Signatures.TERM
29
31
with type t := t
30
32
and type meta = string
31
33
and type schematic = int
32
34
and type subst = Map.t<int, t>
35
+
let mapTerms: (t, t => t) => t
33
36
} => {
34
37
type rec t =
35
38
| Symbol(Symbol.t)
···
423
426
}
424
427
425
428
let ghostTerm = Ghost
429
+
let mapTerms = (t, f) => f(t)
426
430
}
+1
-3
src/SExpJView.resi
+1
-3
src/SExpJView.resi
+3
-3
src/SExpView.res
+3
-3
src/SExpView.res
···
1
-
module ConstSymbol = SExp.ConstSymbol
2
-
module ConstSymbolView: SExpViewFunc.SYMBOL_VIEW with module Symbol := SExp.ConstSymbol = {
3
-
type props = {name: ConstSymbol.t, scope: array<string>}
1
+
module ConstSymbol = SExp.Symbol
2
+
module ConstSymbolView: SExpViewFunc.SYMBOL_VIEW with module Symbol := SExp.Symbol = {
3
+
type props = {name: string, scope: array<string>}
4
4
let make = (props: props) => React.string(props.name)
5
5
}
6
6
+1
-1
src/SExpView.resi
+1
-1
src/SExpView.resi
+14
-1
src/SExpViewFunc.res
+14
-1
src/SExpViewFunc.res
···
7
7
module Make = (
8
8
Symbol: SExpFunc.SYMBOL,
9
9
SymbolView: SYMBOL_VIEW with module Symbol := Symbol,
10
-
SExp: module type of SExpFunc.Make(Symbol),
10
+
SExp: {
11
+
type rec t =
12
+
| Symbol(Symbol.t)
13
+
| Compound({subexps: array<t>})
14
+
| Var({idx: int})
15
+
| Schematic({schematic: int, allowed: array<int>})
16
+
| Ghost
17
+
include Signatures.TERM
18
+
with type t := t
19
+
and type meta = string
20
+
and type schematic = int
21
+
and type subst = Map.t<int, t>
22
+
let mapTerms: (t, t => t) => t
23
+
},
11
24
): {
12
25
include Signatures.TERM_VIEW with module Term := SExp
13
26
} => {
+25
-42
src/Scratch.res
+25
-42
src/Scratch.res
···
1
-
module HOTermJ = TermAsJudgment.HOTermJ
2
-
module StringSExpJ = TermAsJudgment.StringSExpJ
3
-
4
-
module AxiomS = Editable.TextArea(AxiomSet.Make(HOTerm, HOTermJ, HOTermJView))
5
-
module InductiveS = Editable.TextArea(InductiveSet.Make(HOTerm, HOTermJ, HOTermJView))
1
+
module AxiomS = Editable.TextArea(AxiomSet.Make(HOTerm, HOTerm, HOTermJView))
2
+
module InductiveS = Editable.TextArea(InductiveSet.Make(HOTerm, HOTerm, HOTermJView))
6
3
7
4
module EqualityViews = MethodView.CombineMethodView(
8
5
HOTerm,
9
-
HOTermJ,
10
-
MethodView.RewriteView(HOTermJ),
11
-
MethodView.RewriteReverseView(HOTermJ),
6
+
HOTerm,
7
+
MethodView.RewriteView(HOTerm),
8
+
MethodView.RewriteReverseView(HOTerm),
12
9
)
13
10
module ConstructorEqualityViews = MethodView.CombineMethodView(
14
11
HOTerm,
15
-
HOTermJ,
12
+
HOTerm,
16
13
EqualityViews,
17
-
MethodView.ConstructorNeqView(HOTermJ),
14
+
MethodView.ConstructorNeqView(HOTerm),
18
15
)
19
16
module RewritesView = MethodView.CombineMethodView(
20
17
HOTerm,
21
-
HOTermJ,
18
+
HOTerm,
22
19
ConstructorEqualityViews,
23
-
MethodView.ConstructorInjView(HOTermJ),
20
+
MethodView.ConstructorInjView(HOTerm),
24
21
)
25
22
module DerivationsOrLemmasView = MethodView.CombineMethodView(
26
23
HOTerm,
27
-
HOTermJ,
24
+
HOTerm,
28
25
MethodView.CombineMethodView(
29
26
HOTerm,
30
-
HOTermJ,
31
-
MethodView.DerivationView(HOTerm, HOTermJ),
32
-
MethodView.LemmaView(HOTerm, HOTermJ, HOTermJView),
27
+
HOTerm,
28
+
MethodView.DerivationView(HOTerm, HOTerm),
29
+
MethodView.LemmaView(HOTerm, HOTerm, HOTermJView),
33
30
),
34
-
MethodView.EliminationView(HOTerm, HOTermJ),
31
+
MethodView.EliminationView(HOTerm, HOTerm),
35
32
)
36
-
module DLRView = MethodView.CombineMethodView(
33
+
module DLRView = MethodView.CombineMethodView(HOTerm, HOTerm, DerivationsOrLemmasView, RewritesView)
34
+
module DLREView = MethodView.CombineMethodView(
37
35
HOTerm,
38
-
HOTermJ,
39
-
DerivationsOrLemmasView,
40
-
RewritesView,
41
-
)
42
-
module DLREView = MethodView.CombineMethodView(
43
36
HOTerm,
44
-
HOTermJ,
45
37
DLRView,
46
-
MethodView.EliminationView(HOTerm, HOTermJ),
38
+
MethodView.EliminationView(HOTerm, HOTerm),
47
39
)
48
40
49
41
// Temporarily use DLRView (without Elimination) due to HOTerm unification bug
50
-
module TheoremS = Editable.TextArea(Theorem.Make(HOTerm, HOTermJ, HOTermJView, DLRView))
51
-
module ConfS = ConfigBlock.Make(HOTerm, HOTermJ)
42
+
module TheoremS = Editable.TextArea(Theorem.Make(HOTerm, HOTerm, HOTermJView, DLRView))
43
+
module ConfS = ConfigBlock.Make(HOTerm, HOTerm)
52
44
53
45
module AxiomStr = Editable.TextArea(StringAxiomSet)
54
46
module DerivationsOrLemmasStrView = MethodView.CombineMethodView(
55
47
StringSExp,
56
-
StringSExpJ,
57
-
MethodView.DerivationView(StringSExp, StringSExpJ),
58
-
MethodView.LemmaView(
59
-
StringSExp,
60
-
StringSExpJ,
61
-
StringTermJView,
62
-
),
48
+
StringSExp,
49
+
MethodView.DerivationView(StringSExp, StringSExp),
50
+
MethodView.LemmaView(StringSExp, StringSExp, StringTermJView),
63
51
)
64
52
module DLEStrView = MethodView.CombineMethodView(
65
53
StringSExp,
66
-
StringSExpJ,
54
+
StringSExp,
67
55
DerivationsOrLemmasStrView,
68
-
MethodView.EliminationView(StringSExp, StringSExpJ),
56
+
MethodView.EliminationView(StringSExp, StringSExp),
69
57
)
70
58
module TheoremStr = Editable.TextArea(
71
-
Theorem.Make(
72
-
StringSExp,
73
-
StringSExpJ,
74
-
StringTermJView,
75
-
DLEStrView,
76
-
),
59
+
Theorem.Make(StringSExp, StringSExp, StringTermJView, DLEStrView),
77
60
)
+5
-19
src/Signatures.res
+5
-19
src/Signatures.res
···
30
30
module type JUDGMENT = {
31
31
module Term: TERM
32
32
type t
33
-
type subst
34
-
type substCodom
35
-
type schematic = Term.schematic
36
-
type meta = Term.meta
37
-
let mapSubst: (subst, substCodom => substCodom) => subst
38
-
let mergeSubsts: (subst, subst) => subst
39
-
let substitute: (t, subst) => t
40
-
let substituteSubstCodom: (substCodom, subst) => substCodom
33
+
let substitute: (t, Term.subst) => t
41
34
let equivalent: (t, t) => bool
42
-
let unify: (t, t, ~gen: Term.gen=?) => Seq.t<subst>
43
-
let substDeBruijn: (t, array<substCodom>, ~from: int=?) => t
35
+
let unify: (t, t, ~gen: Term.gen=?) => Seq.t<Term.subst>
36
+
let substDeBruijn: (t, array<Term.t>, ~from: int=?) => t
44
37
let reduce: t => t
45
38
let upshift: (t, int, ~from: int=?) => t
46
-
let upshiftSubstCodom: (substCodom, int, ~from: int=?) => substCodom
47
-
let placeSubstCodom: (schematic, ~scope: array<meta>) => substCodom
48
39
// Map a function over all terms in the judgment
40
+
// NOTE(josh): we should return to whether this is necessary.
49
41
let mapTerms: (t, Term.t => Term.t) => t
50
42
let parse: (string, ~scope: array<Term.meta>, ~gen: Term.gen=?) => result<(t, string), string>
51
-
let parseSubstCodom: (
52
-
string,
53
-
~scope: array<Term.meta>,
54
-
~gen: Term.gen=?,
55
-
) => result<(substCodom, string), string>
56
43
let prettyPrint: (t, ~scope: array<Term.meta>) => string
57
-
let prettyPrintSubstCodom: (substCodom, ~scope: array<Term.meta>) => string
58
-
let ghostJudgment: t
44
+
let ghostTerm: t
59
45
}
60
46
61
47
module type TERM_VIEW = {
+1
-1
src/StringAxiomSet.res
+1
-1
src/StringAxiomSet.res
+4
-4
src/StringSExp.res
+4
-4
src/StringSExp.res
···
1
-
type stringSymbol = StringS(StringTerm.t) | ConstS(SExp.ConstSymbol.t)
1
+
type stringSymbol = StringS(StringTerm.t) | ConstS(SExp.Symbol.t)
2
2
3
3
module StringSymbol: SExpFunc.SYMBOL with type t = stringSymbol = {
4
4
type t = stringSymbol
···
8
8
StringTerm.parse(s, ~scope, ~gen?)
9
9
->Result.map(((r, rest)) => (StringS(r), rest))
10
10
->Util.Result.or(() =>
11
-
SExp.ConstSymbol.parse(s, ~scope, ~gen?)->Result.map(((r, rest)) => (ConstS(r), rest))
11
+
SExp.Symbol.parse(s, ~scope, ~gen?)->Result.map(((r, rest)) => (ConstS(r), rest))
12
12
)
13
13
}
14
14
let prettyPrint = (s, ~scope) =>
15
15
switch s {
16
16
| StringS(s) => StringTerm.prettyPrint(s, ~scope)
17
-
| ConstS(s) => SExp.ConstSymbol.prettyPrint(s, ~scope)
17
+
| ConstS(s) => SExp.Symbol.prettyPrint(s, ~scope)
18
18
}
19
19
let unify = (s1, s2) =>
20
20
switch (s1, s2) {
21
21
| (StringS(s1), StringS(s2)) =>
22
22
StringTerm.unify(s1, s2)->Seq.map(subst => subst->Util.mapMapValues(v => StringS(v)))
23
23
| (ConstS(s1), ConstS(s2)) =>
24
-
SExp.ConstSymbol.unify(s1, s2)->Seq.map(subst => subst->Util.mapMapValues(v => ConstS(v)))
24
+
SExp.Symbol.unify(s1, s2)->Seq.map(subst => subst->Util.mapMapValues(v => ConstS(v)))
25
25
| (_, _) => Seq.empty
26
26
}
27
27
let substitute = (s, subst: subst) =>
+16
-2
src/StringSExp.resi
+16
-2
src/StringSExp.resi
···
1
-
type stringSymbol = StringS(StringTerm.t) | ConstS(SExp.ConstSymbol.t)
1
+
type stringSymbol = StringS(StringTerm.t) | ConstS(SExp.Symbol.t)
2
2
module StringSymbol: SExpFunc.SYMBOL with type t = stringSymbol
3
3
4
-
include module type of SExpFunc.Make(StringSymbol)
4
+
type rec t =
5
+
| Symbol(StringSymbol.t)
6
+
| Compound({subexps: array<t>})
7
+
| Var({idx: int})
8
+
| Schematic({schematic: int, allowed: array<int>})
9
+
| Ghost
10
+
11
+
include Signatures.TERM
12
+
with type t := t
13
+
and type meta = string
14
+
and type schematic = int
15
+
and type subst = Map.t<int, t>
16
+
17
+
module Symbol: SExpFunc.SYMBOL with type t := StringSymbol.t
18
+
let mapTerms: (t, t => t) => t
+1
-3
src/StringTermJView.resi
+1
-3
src/StringTermJView.resi
-19
src/TermAsJudgment.res
-19
src/TermAsJudgment.res
···
1
-
open Signatures
2
-
3
-
module Make = (Term: TERM): (
4
-
JUDGMENT with module Term := Term and type t = Term.t and type subst = Term.subst
5
-
) => {
6
-
include Term
7
-
type substCodom = Term.t
8
-
let prettyPrintSubstCodom = Term.prettyPrint
9
-
let parseSubstCodom = Term.parse
10
-
let placeSubstCodom = Term.place
11
-
let upshiftSubstCodom = Term.upshift
12
-
let substituteSubstCodom = Term.substitute
13
-
let mapTerms = (t: Term.t, f: Term.t => Term.t): Term.t => f(t)
14
-
let ghostJudgment = Term.ghostTerm
15
-
}
16
-
17
-
module SExpJ = Make(SExp)
18
-
module HOTermJ = Make(HOTerm)
19
-
module StringSExpJ = Make(StringSExp)
+5
-5
tests/SExpTest.res
+5
-5
tests/SExpTest.res
···
4
4
module Util = TestUtil.MakeTerm(SExp)
5
5
6
6
zoraBlock("parse symbol", t => {
7
-
t->block("single char", t => t->Util.testParse("x", symbol("x")))
8
-
t->block("multi char", t => t->Util.testParse("xyz", symbol("xyz")))
9
-
t->block("judgement terminal", t => t->Util.testParse("a]", symbol("a"), ~expectRemaining="]"))
7
+
t->block("single char", t => t->Util.testParse("x", Symbol("x")))
8
+
t->block("multi char", t => t->Util.testParse("xyz", Symbol("xyz")))
9
+
t->block("judgement terminal", t => t->Util.testParse("a]", Symbol("a"), ~expectRemaining="]"))
10
10
})
11
11
12
12
zoraBlock("parse var", t => {
···
27
27
28
28
zoraBlock("parse compound", t => {
29
29
t->block("unit", t => t->Util.testParse("()", Compound({subexps: []})))
30
-
t->block("single", t => t->Util.testParse("(a)", Compound({subexps: [symbol("a")]})))
30
+
t->block("single", t => t->Util.testParse("(a)", Compound({subexps: [Symbol("a")]})))
31
31
t->block("multiple", t => {
32
32
t->Util.testParse(
33
33
"(a \\1 ?1())",
34
34
Compound({
35
-
subexps: [symbol("a"), Var({idx: 1}), Schematic({schematic: 1, allowed: []})],
35
+
subexps: [Symbol("a"), Var({idx: 1}), Schematic({schematic: 1, allowed: []})],
36
36
}),
37
37
)
38
38
})