the next generation of the in-browser educational proof assistant
add checks for substitution failure
+30
-6
+10
-2
src/SExpFunc.res
+10
-2
src/SExpFunc.res
···
144
144
unifyTerm(x, y)->Seq.flatMap(s1 =>
145
145
a
146
146
->Array.sliceToEnd(~start=1)
147
-
->Array.map(((t1, t2)) => (substitute(t1, s1), substitute(t2, s1)))
147
+
->Array.filterMap(((t1, t2)) =>
148
+
try {Some((substitute(t1, s1), substitute(t2, s1)))} catch {
149
+
| SubstNotCompatible(_) => None
150
+
}
151
+
)
148
152
->unifyArray
149
-
->Seq.map(s2 => combineSubst(s1, s2))
153
+
->Seq.filterMap(s2 =>
154
+
try {Some(combineSubst(s1, s2))} catch {
155
+
| SubstNotCompatible(_) => None
156
+
}
157
+
)
150
158
)
151
159
}
152
160
}
+20
-4
src/Theorem.res
+20
-4
src/Theorem.res
···
14
14
open RuleView
15
15
module RuleView = RuleView.Make(Term, Judgment, JudgmentView)
16
16
module Ports = Ports(Term, Judgment)
17
-
type state = {name: string, rule: Rule.t, proof: Proof.t, gen: Term.gen}
17
+
type state = {
18
+
name: string,
19
+
rule: Rule.t,
20
+
proof: Proof.t,
21
+
gen: Term.gen,
22
+
substFailed: option<string>,
23
+
}
18
24
type props = {
19
25
content: state,
20
26
imports: Ports.t,
···
39
45
Error("Trailing input: "->String.concat(s'))
40
46
| Ok((proof, _)) =>
41
47
Ok((
42
-
{name, rule, proof, gen},
48
+
{name, rule, proof, gen, substFailed: None},
43
49
{Ports.facts: Dict.fromArray([(name, rule)]), ruleStyle: None},
44
50
))
45
51
}
···
51
57
let checked = Proof.check(ctx, props.content.proof, props.content.rule)
52
58
let sidebarRef = React.useRef(Nullable.null)
53
59
let proofChanged = (proof, subst) => {
60
+
let proof = Proof.uncheck(proof)->Proof.substitute(subst)
54
61
props.onChange(
55
-
{...props.content, proof: Proof.uncheck(proof)->Proof.substitute(subst)},
62
+
try {
63
+
Proof.check(ctx, proof, props.content.rule)->ignore
64
+
{...props.content, proof, substFailed: None}
65
+
} catch {
66
+
| SExpFunc.SubstNotCompatible(s) => {...props.content, substFailed: Some(s)}
67
+
},
56
68
~exports={
57
69
Ports.facts: Dict.fromArray([(props.content.name, props.content.rule)]),
58
70
ruleStyle: None,
59
71
},
60
72
)
61
73
}
62
-
74
+
63
75
<SidebarContext sidebarRef>
64
76
<h3> {React.string("Theorem")} </h3>
65
77
<RuleView rule={props.content.rule} scope={[]} style={ruleStyle}>
···
69
81
<ProofView
70
82
ruleStyle={ruleStyle} scope={[]} proof=checked gen={props.content.gen} onChange=proofChanged
71
83
/>
84
+
{switch props.content.substFailed {
85
+
| Some(msg) => React.string(msg)
86
+
| None => React.null
87
+
}}
72
88
<div className="sidebar" ref={ReactDOM.Ref.domRef(sidebarRef)} />
73
89
</SidebarContext>
74
90
}