the next generation of the in-browser educational proof assistant
chore: run ./node_modules/.bin/rescript-tools migrate-all .
+212
-198
+4
-2
src/AxiomSet.res
+4
-2
src/AxiomSet.res
···
54
54
<div
55
55
className={"axiom-set axiom-set-"->String.concat(
56
56
String.make(props.imports.ruleStyle->Option.getOr(Hybrid)),
57
-
)}>
57
+
)}
58
+
>
58
59
{Dict.toArray(props.content)
59
60
->Array.mapWithIndex(((n, r), i) =>
60
61
<RuleView
61
62
rule={r}
62
63
scope={[]}
63
64
key={String.make(i)}
64
-
style={props.imports.ruleStyle->Option.getOr(Hybrid)}>
65
+
style={props.imports.ruleStyle->Option.getOr(Hybrid)}
66
+
>
65
67
{React.string(n)}
66
68
</RuleView>
67
69
)
+28
-28
src/HOTerm.res
+28
-28
src/HOTerm.res
···
102
102
| Ok(newIdx) =>
103
103
let new = newIdx + from
104
104
if new < 0 {
105
-
raise(Err("mapbind: negative index"))
105
+
throw(Err("mapbind: negative index"))
106
106
}
107
107
Var({
108
108
idx: new,
···
132
132
let upshift = (term: t, amount: int, ~from: int=0) => mapbind(term, idx => idx + amount, ~from)
133
133
let downshift = (term: t, amount: int, ~from: int=1) => {
134
134
if amount > from {
135
-
raise(Err("downshift amount must be less than from"))
135
+
throw(Err("downshift amount must be less than from"))
136
136
}
137
137
mapbind(term, idx => idx - amount, ~from)
138
138
}
···
333
333
let rec proj = (subst: subst, term: t, ~gen: option<gen>): subst => {
334
334
switch strip(devar(subst, term)) {
335
335
| (Lam({name: _, body}), args) if args->Array.length == 0 => proj(subst, body, ~gen)
336
-
| (Unallowed, _args) => raise(UnifyFail("unallowed"))
336
+
| (Unallowed, _args) => throw(UnifyFail("unallowed"))
337
337
| (Symbol(_) | Var(_), args) => Array.reduce(args, subst, (acc, a) => proj(acc, a, ~gen))
338
338
| (Schematic({schematic}), args) => {
339
339
assert(!substHas(subst, schematic))
340
340
if gen->Option.isNone {
341
-
raise(UnifyFail("no gen provided"))
341
+
throw(UnifyFail("no gen provided"))
342
342
}
343
343
let h = Schematic({schematic: fresh(Option.getExn(gen))})
344
344
subst->substAdd(
···
358
358
),
359
359
)
360
360
}
361
-
| _ => raise(UnifyFail("not a symbol, var or schematic"))
361
+
| _ => throw(UnifyFail("not a symbol, var or schematic"))
362
362
}
363
363
}
364
364
let flexflex = (
···
370
370
~gen: option<gen>,
371
371
): subst => {
372
372
if gen->Option.isNone {
373
-
raise(UnifyFail("no gen provided"))
373
+
throw(UnifyFail("no gen provided"))
374
374
}
375
375
if sa == sb {
376
376
if xs->Array.length != ys->Array.length {
377
-
raise(UnifyFail("flexible schematics have different number of arguments"))
377
+
throw(UnifyFail("flexible schematics have different number of arguments"))
378
378
}
379
379
let len = xs->Array.length
380
380
let h = Schematic({schematic: fresh(Option.getExn(gen))})
···
396
396
}
397
397
let flexrigid = (sa: schematic, xs: array<t>, b: t, subst: subst, ~gen: option<gen>): subst => {
398
398
if occ(sa, subst, b) {
399
-
raise(UnifyFail("flexible schematic occurs in rigid term"))
399
+
throw(UnifyFail("flexible schematic occurs in rigid term"))
400
400
}
401
401
// pattern unification
402
402
// let u = b->mapbind0(bind => idx2(xs, bind))
···
412
412
if na == nb {
413
413
subst
414
414
} else {
415
-
raise(UnifyFail("symbols do not match"))
415
+
throw(UnifyFail("symbols do not match"))
416
416
}
417
417
| (Var({idx: ia}), Var({idx: ib})) =>
418
418
if ia == ib {
419
419
subst
420
420
} else {
421
-
raise(UnifyFail("variables do not match"))
421
+
throw(UnifyFail("variables do not match"))
422
422
}
423
423
| (Schematic({schematic: sa}), Schematic({schematic: sb})) if sa == sb => subst
424
424
| (Lam({name: _, body: ba}), Lam({name: _, body: bb})) => unifyTerm(ba, bb, subst, ~gen)
···
435
435
| ((a, xs), (b, ys)) =>
436
436
switch (a, b) {
437
437
| (Symbol(_) | Var(_), Symbol(_) | Var(_)) => rigidrigid(a, xs, b, ys, subst, ~gen)
438
-
| _ => raise(UnifyFail("no rules match"))
438
+
| _ => throw(UnifyFail("no rules match"))
439
439
}
440
440
}
441
441
}
442
442
and unifyArray = (xs: array<t>, ys: array<t>, subst: subst, ~gen: option<gen>): subst => {
443
443
if xs->Array.length != ys->Array.length {
444
-
raise(UnifyFail("arrays have different lengths"))
444
+
throw(UnifyFail("arrays have different lengths"))
445
445
}
446
446
Belt.Array.zip(xs, ys)->Belt.Array.reduce(subst, (acc, (x, y)) => unifyTerm(x, y, acc, ~gen))
447
447
}
···
454
454
~gen: option<gen>,
455
455
): subst => {
456
456
if !equivalent(a, b) {
457
-
raise(UnifyFail("rigid terms do not match"))
457
+
throw(UnifyFail("rigid terms do not match"))
458
458
}
459
459
if xs->Array.length != ys->Array.length {
460
-
raise(UnifyFail("rigid terms have different number of arguments"))
460
+
throw(UnifyFail("rigid terms have different number of arguments"))
461
461
}
462
462
unifyArray(xs, ys, subst, ~gen)
463
463
}
···
571
571
| "\\" => {
572
572
let re = RegExp.fromStringWithFlags(varRegexpString, ~flags="y")
573
573
switch re->RegExp.exec(str) {
574
-
| None => raise(ParseError("invalid variable"))
574
+
| None => throw(ParseError("invalid variable"))
575
575
| Some(res) =>
576
576
switch RegExp.Result.matches(res) {
577
577
| [n] => (
578
578
VarT(n->Int.fromString->Option.getExn),
579
579
String.sliceToEnd(str, ~start=RegExp.lastIndex(re)),
580
580
)
581
-
| _ => raise(ParseError("invalid variable"))
581
+
| _ => throw(ParseError("invalid variable"))
582
582
}
583
583
}
584
584
}
585
585
| "?" => {
586
586
let re = RegExp.fromStringWithFlags(schematicRegexpString, ~flags="y")
587
587
switch re->RegExp.exec(str) {
588
-
| None => raise(ParseError("invalid schematic"))
588
+
| None => throw(ParseError("invalid schematic"))
589
589
| Some(res) =>
590
590
switch RegExp.Result.matches(res) {
591
591
| [n] => (
592
592
SchematicT(n->Int.fromString->Option.getExn),
593
593
String.sliceToEnd(str, ~start=RegExp.lastIndex(re)),
594
594
)
595
-
| _ => raise(ParseError("invalid schematic"))
595
+
| _ => throw(ParseError("invalid schematic"))
596
596
}
597
597
}
598
598
}
599
599
| "@" =>
600
600
let re = RegExp.fromStringWithFlags(symbolRegexpString, ~flags="y")
601
601
switch re->RegExp.exec(rest()) {
602
-
| None => raise(ParseError("invalid symbol"))
602
+
| None => throw(ParseError("invalid symbol"))
603
603
| Some(res) =>
604
604
switch RegExp.Result.matches(res) {
605
605
| [n] => (ConsT(n), String.sliceToEnd(rest(), ~start=RegExp.lastIndex(re)))
606
-
| _ => raise(ParseError("invalid symbol"))
606
+
| _ => throw(ParseError("invalid symbol"))
607
607
}
608
608
}
609
609
| _ => {
···
612
612
| Some(res) =>
613
613
switch RegExp.Result.matches(res) {
614
614
| [n] => (NameT(n), String.sliceToEnd(str, ~start=RegExp.lastIndex(reName)))
615
-
| _ => raise(ParseError("invalid symbol"))
615
+
| _ => throw(ParseError("invalid symbol"))
616
616
}
617
617
| None =>
618
618
let re = RegExp.fromStringWithFlags(symbolRegexpString, ~flags="y")
619
619
switch re->RegExp.exec(str) {
620
-
| None => raise(ParseError("invalid symbol"))
620
+
| None => throw(ParseError("invalid symbol"))
621
621
| Some(res) =>
622
622
switch RegExp.Result.matches(res) {
623
623
| [n] => (AtomT(n), String.sliceToEnd(str, ~start=RegExp.lastIndex(re)))
624
-
| _ => raise(ParseError("invalid symbol"))
624
+
| _ => throw(ParseError("invalid symbol"))
625
625
}
626
626
}
627
627
}
···
651
651
let (tail, rest3) = parseSimple("("->String.concat(rest2))
652
652
switch tail {
653
653
| ListS({xs}) => (ListS({xs: Array.concat([head], xs)}), rest3)
654
-
| _ => raise(Unreachable("bug"))
654
+
| _ => throw(Unreachable("bug"))
655
655
}
656
656
}
657
657
}
658
658
}
659
-
| RParen => raise(ParseError("unexpected right parenthesis"))
659
+
| RParen => throw(ParseError("unexpected right parenthesis"))
660
660
| VarT(idx) => (VarS({idx: idx}), rest)
661
661
| SchematicT(schematic) => (SchematicS({schematic: schematic}), rest)
662
662
| AtomT(name) => (AtomS({name, constructor: false}), rest)
···
665
665
let (result, rest1) = parseSimple(rest)
666
666
(LambdaS({name, body: result}), rest1)
667
667
}
668
-
| EOF => raise(ParseError("unexpected end of file"))
668
+
| EOF => throw(ParseError("unexpected end of file"))
669
669
}
670
670
}
671
671
type env = Map.t<string, int>
···
696
696
| ListS({xs}) => {
697
697
let ts = xs->Array.map(x => parseAll(x, ~env, ~gen?))
698
698
if ts->Array.length == 0 {
699
-
raise(ParseError("empty list"))
699
+
throw(ParseError("empty list"))
700
700
} else {
701
701
ts
702
702
->Array.sliceToEnd(~start=1)
···
719
719
seen(g, schematic)
720
720
Schematic({schematic: schematic})
721
721
}
722
-
| None => raise(ParseError("Schematics not allowed here"))
722
+
| None => throw(ParseError("Schematics not allowed here"))
723
723
}
724
724
| LambdaS({name, body}) =>
725
725
Lam({
+6
-4
src/InductiveSet.res
+6
-4
src/InductiveSet.res
···
88
88
let (conclusionHead, conclusionArgs) = HOTerm.strip(constructorRule.conclusion)
89
89
let typeIndex = switch conclusionHead {
90
90
| Symbol({name}) => findFormerIndex(name, Array.length(conclusionArgs))
91
-
| _ => raise(Unreachable("Constructor conclusion must have a Symbol head"))
91
+
| _ => throw(Unreachable("Constructor conclusion must have a Symbol head"))
92
92
}
93
93
94
94
{
···
187
187
let (_head, args) = HOTerm.strip(predicateRule.conclusion)
188
188
let predicateArg = switch args[0] {
189
189
| Some(arg) => arg
190
-
| None => raise(Unreachable("Predicate conclusion must have one argument"))
190
+
| None => throw(Unreachable("Predicate conclusion must have one argument"))
191
191
}
192
192
193
193
let equalityPremise = {
···
276
276
<div
277
277
className={"axiom-set axiom-set-"->String.concat(
278
278
String.make(props.imports.ruleStyle->Option.getOr(Hybrid)),
279
-
)}>
279
+
)}
280
+
>
280
281
{Dict.toArray(props.content->Dict.copy->Dict.assign(derived(props.content)))
281
282
->Array.mapWithIndex(((n, r), i) =>
282
283
<RuleView
283
284
rule={r}
284
285
scope={[]}
285
286
key={String.make(i)}
286
-
style={props.imports.ruleStyle->Option.getOr(Hybrid)}>
287
+
style={props.imports.ruleStyle->Option.getOr(Hybrid)}
288
+
>
287
289
{React.string(n)}
288
290
</RuleView>
289
291
)
+3
-3
src/Method.res
+3
-3
src/Method.res
···
112
112
Array.push(subgoals, sg)
113
113
cur := String.trim(rest)
114
114
}
115
-
| Error(e) => raise(InternalParseError(e))
115
+
| Error(e) => throw(InternalParseError(e))
116
116
}
117
117
}
118
118
if cur.contents->String.get(0) == Some("}") {
···
276
276
Array.push(subgoals, sg)
277
277
cur := String.trim(rest)
278
278
}
279
-
| Error(e) => raise(InternalParseError(e))
279
+
| Error(e) => throw(InternalParseError(e))
280
280
}
281
281
}
282
282
if cur.contents->String.get(0) == Some("}") {
···
614
614
615
615
try {
616
616
switch subparser(cur.contents, ~scope, ~gen) {
617
-
| Error(e) => raise(InternalParseError(e))
617
+
| Error(e) => throw(InternalParseError(e))
618
618
| Ok((subgoal, rest2)) => {
619
619
cur := String.trim(rest2)
620
620
+145
-139
src/MethodView.res
+145
-139
src/MethodView.res
···
37
37
"gen": Term.gen,
38
38
"onChange": ('a, Judgment.subst) => unit,
39
39
}
40
-
let make = (subRender: srProps<'a> => React.element) => props => {
41
-
<div>
42
-
<b> {React.string("by ")} </b>
43
-
{React.string(props.method.ruleName)}
44
-
<ul>
45
-
{props.method.subgoals
46
-
->Array.mapWithIndex((sg, i) => {
47
-
<li key={String.make(i)}>
48
-
{React.createElement(
49
-
subRender,
50
-
{
51
-
"proof": sg,
52
-
"scope": props.scope,
53
-
"ruleStyle": props.ruleStyle,
54
-
"gen": props.gen,
55
-
"onChange": (newa, subst: Judgment.subst) =>
56
-
props.onChange(props.method->Method.updateAtKey(i, _ => newa), subst),
57
-
},
58
-
)}
59
-
</li>
60
-
})
61
-
->React.array}
62
-
</ul>
63
-
</div>
64
-
}
40
+
let make = (subRender: srProps<'a> => React.element) =>
41
+
props => {
42
+
<div>
43
+
<b> {React.string("by ")} </b>
44
+
{React.string(props.method.ruleName)}
45
+
<ul>
46
+
{props.method.subgoals
47
+
->Array.mapWithIndex((sg, i) => {
48
+
<li key={String.make(i)}>
49
+
{React.createElement(
50
+
subRender,
51
+
{
52
+
"proof": sg,
53
+
"scope": props.scope,
54
+
"ruleStyle": props.ruleStyle,
55
+
"gen": props.gen,
56
+
"onChange": (newa, subst: Judgment.subst) =>
57
+
props.onChange(props.method->Method.updateAtKey(i, _ => newa), subst),
58
+
},
59
+
)}
60
+
</li>
61
+
})
62
+
->React.array}
63
+
</ul>
64
+
</div>
65
+
}
65
66
}
66
67
67
68
module EliminationView = (Term: TERM, Judgment: JUDGMENT with module Term := Term) => {
···
80
81
"gen": Term.gen,
81
82
"onChange": ('a, Judgment.subst) => unit,
82
83
}
83
-
let make = (subRender: srProps<'a> => React.element) => props => {
84
-
<div>
85
-
<b> {React.string("elim ")} </b>
86
-
{React.string(`${props.method.ruleName} ${props.method.elimName}`)}
87
-
<ul>
88
-
{props.method.subgoals
89
-
->Array.mapWithIndex((sg, i) => {
90
-
<li key={String.make(i)}>
91
-
{React.createElement(
92
-
subRender,
93
-
{
94
-
"proof": sg,
95
-
"scope": props.scope,
96
-
"ruleStyle": props.ruleStyle,
97
-
"gen": props.gen,
98
-
"onChange": (newa, subst: Judgment.subst) =>
99
-
props.onChange(props.method->Method.updateAtKey(i, _ => newa), subst),
100
-
},
101
-
)}
102
-
</li>
103
-
})
104
-
->React.array}
105
-
</ul>
106
-
</div>
107
-
}
84
+
let make = (subRender: srProps<'a> => React.element) =>
85
+
props => {
86
+
<div>
87
+
<b> {React.string("elim ")} </b>
88
+
{React.string(`${props.method.ruleName} ${props.method.elimName}`)}
89
+
<ul>
90
+
{props.method.subgoals
91
+
->Array.mapWithIndex((sg, i) => {
92
+
<li key={String.make(i)}>
93
+
{React.createElement(
94
+
subRender,
95
+
{
96
+
"proof": sg,
97
+
"scope": props.scope,
98
+
"ruleStyle": props.ruleStyle,
99
+
"gen": props.gen,
100
+
"onChange": (newa, subst: Judgment.subst) =>
101
+
props.onChange(props.method->Method.updateAtKey(i, _ => newa), subst),
102
+
},
103
+
)}
104
+
</li>
105
+
})
106
+
->React.array}
107
+
</ul>
108
+
</div>
109
+
}
108
110
}
109
111
110
112
module LemmaView = (
···
128
130
"onChange": ('a, Judgment.subst) => unit,
129
131
}
130
132
module RuleView = RuleView.Make(Term, Judgment, JudgmentView)
131
-
let make = (subRender: srProps<'a> => React.element) => props => {
132
-
<div>
133
-
<b> {React.string("have ")} </b>
134
-
<RuleView rule={props.method.rule} scope={props.scope} style={props.ruleStyle}>
135
-
{React.null}
136
-
</RuleView>
137
-
{React.createElement(
138
-
subRender,
139
-
{
140
-
"proof": props.method.proof,
141
-
"scope": props.scope,
142
-
"ruleStyle": props.ruleStyle,
143
-
"gen": props.gen,
144
-
"onChange": (proof, subst) => {props.onChange({...props.method, proof}, subst)},
145
-
},
146
-
)}
147
-
{React.createElement(
148
-
subRender,
149
-
{
150
-
"proof": props.method.show,
151
-
"scope": props.scope,
152
-
"ruleStyle": props.ruleStyle,
153
-
"gen": props.gen,
154
-
"onChange": (show, subst) => {props.onChange({...props.method, show}, subst)},
155
-
},
156
-
)}
157
-
</div>
158
-
}
133
+
let make = (subRender: srProps<'a> => React.element) =>
134
+
props => {
135
+
<div>
136
+
<b> {React.string("have ")} </b>
137
+
<RuleView rule={props.method.rule} scope={props.scope} style={props.ruleStyle}>
138
+
{React.null}
139
+
</RuleView>
140
+
{React.createElement(
141
+
subRender,
142
+
{
143
+
"proof": props.method.proof,
144
+
"scope": props.scope,
145
+
"ruleStyle": props.ruleStyle,
146
+
"gen": props.gen,
147
+
"onChange": (proof, subst) => {props.onChange({...props.method, proof}, subst)},
148
+
},
149
+
)}
150
+
{React.createElement(
151
+
subRender,
152
+
{
153
+
"proof": props.method.show,
154
+
"scope": props.scope,
155
+
"ruleStyle": props.ruleStyle,
156
+
"gen": props.gen,
157
+
"onChange": (show, subst) => {props.onChange({...props.method, show}, subst)},
158
+
},
159
+
)}
160
+
</div>
161
+
}
159
162
}
160
163
161
164
module RewriteView = (
···
176
179
"gen": HOTerm.gen,
177
180
"onChange": ('a, Judgment.subst) => unit,
178
181
}
179
-
let make = (subRender: srProps<'a> => React.element) => props => {
180
-
<div>
181
-
<b> {React.string("rewrite ")} </b>
182
-
{React.string(props.method.equalityName)}
183
-
<ul>
184
-
<li>
185
-
{React.createElement(
186
-
subRender,
187
-
{
188
-
"proof": props.method.subgoal,
189
-
"scope": props.scope,
190
-
"ruleStyle": props.ruleStyle,
191
-
"gen": props.gen,
192
-
"onChange": (subgoal, subst: Judgment.subst) =>
193
-
props.onChange({...props.method, subgoal}, subst),
194
-
},
195
-
)}
196
-
</li>
197
-
</ul>
198
-
</div>
199
-
}
182
+
let make = (subRender: srProps<'a> => React.element) =>
183
+
props => {
184
+
<div>
185
+
<b> {React.string("rewrite ")} </b>
186
+
{React.string(props.method.equalityName)}
187
+
<ul>
188
+
<li>
189
+
{React.createElement(
190
+
subRender,
191
+
{
192
+
"proof": props.method.subgoal,
193
+
"scope": props.scope,
194
+
"ruleStyle": props.ruleStyle,
195
+
"gen": props.gen,
196
+
"onChange": (subgoal, subst: Judgment.subst) =>
197
+
props.onChange({...props.method, subgoal}, subst),
198
+
},
199
+
)}
200
+
</li>
201
+
</ul>
202
+
</div>
203
+
}
200
204
}
201
205
202
206
module RewriteReverseView = (
···
217
221
"gen": HOTerm.gen,
218
222
"onChange": ('a, Judgment.subst) => unit,
219
223
}
220
-
let make = (subRender: srProps<'a> => React.element) => props => {
221
-
<div>
222
-
<b> {React.string("rewrite_reverse ")} </b>
223
-
{React.string(props.method.equalityName)}
224
-
<ul>
225
-
<li>
226
-
{React.createElement(
227
-
subRender,
228
-
{
229
-
"proof": props.method.subgoal,
230
-
"scope": props.scope,
231
-
"ruleStyle": props.ruleStyle,
232
-
"gen": props.gen,
233
-
"onChange": (subgoal, subst: Judgment.subst) =>
234
-
props.onChange({...props.method, subgoal}, subst),
235
-
},
236
-
)}
237
-
</li>
238
-
</ul>
239
-
</div>
240
-
}
224
+
let make = (subRender: srProps<'a> => React.element) =>
225
+
props => {
226
+
<div>
227
+
<b> {React.string("rewrite_reverse ")} </b>
228
+
{React.string(props.method.equalityName)}
229
+
<ul>
230
+
<li>
231
+
{React.createElement(
232
+
subRender,
233
+
{
234
+
"proof": props.method.subgoal,
235
+
"scope": props.scope,
236
+
"ruleStyle": props.ruleStyle,
237
+
"gen": props.gen,
238
+
"onChange": (subgoal, subst: Judgment.subst) =>
239
+
props.onChange({...props.method, subgoal}, subst),
240
+
},
241
+
)}
242
+
</li>
243
+
</ul>
244
+
</div>
245
+
}
241
246
}
242
247
243
248
module CombineMethodView = (
···
258
263
onChange: (Method.t<'a>, Judgment.subst) => unit,
259
264
}
260
265
type srProps<'a> = Method1View.srProps<'a>
261
-
let make = (subrender: srProps<'a> => React.element) => props => {
262
-
switch props.method {
263
-
| First(m) =>
264
-
Method1View.make(subrender)({
265
-
method: m,
266
-
scope: props.scope,
267
-
ruleStyle: props.ruleStyle,
268
-
gen: props.gen,
269
-
onChange: (n, s) => props.onChange(First(n), s),
270
-
})
271
-
| Second(m) =>
272
-
Method2View.make(subrender)({
273
-
method: m,
274
-
scope: props.scope,
275
-
ruleStyle: props.ruleStyle,
276
-
gen: props.gen,
277
-
onChange: (n, s) => props.onChange(Second(n), s),
278
-
})
266
+
let make = (subrender: srProps<'a> => React.element) =>
267
+
props => {
268
+
switch props.method {
269
+
| First(m) =>
270
+
Method1View.make(subrender)({
271
+
method: m,
272
+
scope: props.scope,
273
+
ruleStyle: props.ruleStyle,
274
+
gen: props.gen,
275
+
onChange: (n, s) => props.onChange(First(n), s),
276
+
})
277
+
| Second(m) =>
278
+
Method2View.make(subrender)({
279
+
method: m,
280
+
scope: props.scope,
281
+
ruleStyle: props.ruleStyle,
282
+
gen: props.gen,
283
+
onChange: (n, s) => props.onChange(Second(n), s),
284
+
})
285
+
}
279
286
}
280
-
}
281
287
}
+2
-1
src/ProofView.res
+2
-1
src/ProofView.res
+2
-2
src/Rule.res
+2
-2
src/Rule.res
···
103
103
cur := rest
104
104
premises->Array.push(p)
105
105
}
106
-
| Error(_) => raise(InternalParseError("expected turnstile or premise"))
106
+
| Error(_) => throw(InternalParseError("expected turnstile or premise"))
107
107
}
108
108
}
109
109
if cur.contents->String.trim->String.get(0) == Some("]") {
···
162
162
cur := rest
163
163
premises->Array.push(p)
164
164
}
165
-
| Error(e) => raise(InternalParseError(e))
165
+
| Error(e) => throw(InternalParseError(e))
166
166
}
167
167
}
168
168
let (ruleName, rest) = it.contents->Result.getExn
+2
-1
src/RuleView.res
+2
-1
src/RuleView.res
+4
-4
src/SExp.res
+4
-4
src/SExp.res
···
324
324
seen(g, num)
325
325
Some(Schematic({schematic: num, allowed: bits}))
326
326
}
327
-
| None => raise(ParseError("Schematics not allowed here"))
327
+
| None => throw(ParseError("Schematics not allowed here"))
328
328
}
329
-
| _ => raise(ParseError("Expected closing parenthesis"))
329
+
| _ => throw(ParseError("Expected closing parenthesis"))
330
330
}
331
331
}
332
-
| _ => raise(ParseError("Expected opening parenthesis"))
332
+
| _ => throw(ParseError("Expected opening parenthesis"))
333
333
}
334
334
}
335
335
| Some(LParen) => {
···
344
344
}
345
345
switch lex() {
346
346
| Some(RParen) => Some(Compound({subexps: bits}))
347
-
| _ => raise(ParseError("Expected closing parenthesis"))
347
+
| _ => throw(ParseError("Expected closing parenthesis"))
348
348
}
349
349
}
350
350
| _ => None
+4
-2
src/StringAxiomSet.res
+4
-2
src/StringAxiomSet.res
···
135
135
<div
136
136
className={"axiom-set axiom-set-"->String.concat(
137
137
String.make(props.imports.ruleStyle->Option.getOr(Hybrid)),
138
-
)}>
138
+
)}
139
+
>
139
140
{content
140
141
->Dict.toArray
141
142
->Array.mapWithIndex(((n, r), i) =>
···
143
144
rule={r}
144
145
scope={[]}
145
146
key={String.make(i)}
146
-
style={props.imports.ruleStyle->Option.getOr(Hybrid)}>
147
+
style={props.imports.ruleStyle->Option.getOr(Hybrid)}
148
+
>
147
149
{React.string(n)}
148
150
</RuleView>
149
151
)
+9
-9
src/StringTerm.res
+9
-9
src/StringTerm.res
···
350
350
}
351
351
352
352
let parseMeta = (str: string) => {
353
-
let re = %re("/^([^\s.\[\]()]+)\./y")
353
+
let re = /^([^\s.\[\]()]+)\./y
354
354
switch re->RegExp.exec(str->String.trim) {
355
355
| None => Error("not a meta name")
356
356
| Some(res) =>
···
416
416
let execRe = re => execRe(re, String.sliceToEnd(str, ~start=pos.contents))
417
417
let stringLit = () => {
418
418
let identRegex = RegExp.fromString(`^${Util.identRegexStr}`)
419
-
let symbolRegex = %re(`/^([!@#\$%\^~&*_+\-={};':|,.<>\/?]+)/`)
420
-
let numberRegex = %re(`/^(\d+)/`)
419
+
let symbolRegex = /^([!@#\$%\^~&*_+\-={};':|,.<>\/?]+)/
420
+
let numberRegex = /^(\d+)/
421
421
switch execRe(identRegex)
422
422
->Option.orElse(execRe(symbolRegex))
423
423
->Option.orElse(execRe(numberRegex)) {
···
427
427
}
428
428
}
429
429
let escaped = () => {
430
-
let escapedRegex = %re(`/\\([\$\?\\\"])/`)
430
+
let escapedRegex = /\\([\$\?\\\"])/
431
431
switch execRe(escapedRegex) {
432
432
| Some([char], l) => add(String(char), ~nAdvance=l)
433
433
| Some(_) => error("regex escaped error")
···
436
436
}
437
437
let readInt = s => Int.fromString(s)->Option.getExn
438
438
let schema = () => {
439
-
let schemaRegex = %re("/\?(\d+)\(((?:\d+\s*)*)\)/")
439
+
let schemaRegex = /\?(\d+)\(((?:\d+\s*)*)\)/
440
440
switch execRe(schemaRegex) {
441
441
| Some([idStr, allowedStr], l) => {
442
442
let schematic = readInt(idStr)
443
443
let allowed =
444
444
allowedStr
445
445
->String.trim
446
-
->String.splitByRegExp(%re("/\s+/"))
446
+
->String.splitByRegExp(/\s+/)
447
447
->Array.keepSome
448
448
->Array.filter(s => s != "")
449
449
->Array.map(readInt)
···
454
454
}
455
455
}
456
456
let var = () => {
457
-
let varLitRegex = %re("/^\$\\(\d+)/")
458
-
let varScopeRegex = %re("/^\$([a-zA-Z]\w*)/")
457
+
let varLitRegex = /^\$\\(\d+)/
458
+
let varScopeRegex = /^\$([a-zA-Z]\w*)/
459
459
switch execRe(varLitRegex) {
460
460
| Some([match], l) => add(Var({idx: readInt(match)}), ~nAdvance=l)
461
461
| Some(_) => error("var lit regex error")
···
473
473
}
474
474
475
475
// consume leading whitespace + open quote
476
-
switch execRe(%re(`/^\s*"/`)) {
476
+
switch execRe(/^\s*"/) {
477
477
| Some(_, l) => pos := l
478
478
| None => error("expected open quote")
479
479
}
+1
-1
src/Util.res
+1
-1
src/Util.res
+2
-2
tests/TestUtil.res
+2
-2
tests/TestUtil.res
···
64
64
| Ok((term, "")) => term
65
65
| Ok((_, rest)) => {
66
66
t->fail(~msg="parse incomplete: " ++ rest)
67
-
raise(Unreachable(""))
67
+
throw(Unreachable(""))
68
68
}
69
69
| Error(msg) => {
70
70
t->fail(~msg="parse failed: " ++ msg)
71
-
raise(Unreachable(""))
71
+
throw(Unreachable(""))
72
72
}
73
73
}
74
74
}