the next generation of the in-browser educational proof assistant
Merge pull request #26 from joshcbrown/atom-subst-cleaning
Tidy ATOM signature and substitution semantics
authored by
Liam O'Connor
and committed by
GitHub
dacd4ade
83f78cff
+73
-32
+21
index.html
+21
index.html
···
657
657
|- ?
658
658
659
659
</hol-string-proof>
660
+
<hol-string id="index.html/string-silliness" deps="index.html/myconfig">
661
+
a.
662
+
-------------- eq-refl
663
+
(Eq a a)
664
+
665
+
a. b. (Eq a b)
666
+
-------------- eq-sym
667
+
(Eq b a)
668
+
669
+
a. b. c. (Eq a b) (Eq "$b" c)
670
+
-------------- eq-trans-weird
671
+
(Eq a c)
672
+
673
+
-------------- eq-a-comp
674
+
(Eq "a" (Foo Bar))
675
+
</hol-string>
676
+
<hol-string-proof id="index.html/string-silliness-trip" deps="index.html/myconfig index.html/string-silliness">
677
+
------------- eq-a-c
678
+
(Eq "a" "a")
679
+
|- ?
680
+
</hol-string-proof>
660
681
<script type="module" src="./src/testcomponent.tsx"></script>
661
682
</body>
662
683
</html>
+14
-12
src/SExpFunc.res
+14
-12
src/SExpFunc.res
···
1
+
exception SubstNotCompatible(string)
2
+
1
3
module type ATOM = {
2
4
type t
3
5
type subst = Map.t<int, t>
···
9
11
// used for when trying to substitute a variable of the wrong type
10
12
let lowerVar: int => option<t>
11
13
let lowerSchematic: (int, array<int>) => option<t>
12
-
let substDeBruijn: (t, Map.t<int, t>, ~from: int=?, ~to: int) => t
14
+
let substDeBruijn: (t, array<option<t>>, ~from: int=?) => t
13
15
let concrete: t => bool
14
16
}
15
17
···
142
144
unifyTerm(x, y)->Seq.flatMap(s1 =>
143
145
a
144
146
->Array.sliceToEnd(~start=1)
145
-
->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
+
)
146
152
->unifyArray
147
-
->Seq.map(s2 => combineSubst(s1, s2))
153
+
->Seq.filterMap(s2 =>
154
+
try {Some(combineSubst(s1, s2))} catch {
155
+
| SubstNotCompatible(_) => None
156
+
}
157
+
)
148
158
)
149
159
}
150
160
}
···
160
170
}
161
171
let rec substDeBruijn = (term: t, substs: array<t>, ~from: int=0) =>
162
172
switch term {
163
-
| Atom(s) => {
164
-
let symbolSubsts =
165
-
substs
166
-
->Array.mapWithIndex((t, i) => lower(t)->Option.map(a => (i, a)))
167
-
->Array.keepSome
168
-
->Map.fromArray
169
-
170
-
Atom(Atom.substDeBruijn(s, symbolSubsts, ~from, ~to=Array.length(substs)))
171
-
}
173
+
| Atom(s) => Atom(Atom.substDeBruijn(s, Array.map(substs, lower), ~from))
172
174
173
175
| Compound({subexps}) =>
174
176
Compound({subexps: Array.map(subexps, x => substDeBruijn(x, substs, ~from))})
+9
-2
src/StringA.res
+9
-2
src/StringA.res
···
270
270
}
271
271
272
272
// law: unify(a,b) == [{}] iff equivalent(a,b)
273
-
let substDeBruijn = (string: t, substs: Map.t<int, t>, ~from: int=0, ~to: int) => {
273
+
let substDeBruijn = (string: t, substs: array<option<t>>, ~from: int=0) => {
274
+
let to = Array.length(substs)
274
275
Array.flatMap(string, piece =>
275
276
switch piece {
276
277
| String(_) => [piece]
···
278
279
if var < from {
279
280
[piece]
280
281
} else if var - from < to {
281
-
Map.get(substs, var - from)->Option.getOr([piece])
282
+
switch Option.getUnsafe(substs[var - from]) {
283
+
| Some(v) => v
284
+
| None =>
285
+
throw(
286
+
SExpFunc.SubstNotCompatible(`index ${Int.toString(var - from)} not of sort string`),
287
+
)
288
+
}
282
289
} else {
283
290
[Var({idx: var - to})]
284
291
}
+8
-13
src/StringSymbol.res
+8
-13
src/StringSymbol.res
···
51
51
let lowerSchematic = (schematic, allowed) => Some(
52
52
StringS([StringA.Schematic({schematic, allowed})]),
53
53
)
54
-
let substDeBruijn = (s, substs: Map.t<int, t>, ~from=?, ~to: int) =>
54
+
let substDeBruijn = (s, substs: array<option<t>>, ~from=?) =>
55
55
switch s {
56
56
| StringS(s) => {
57
-
let stringSubs =
58
-
substs
59
-
->Map.entries
60
-
->Iterator.toArrayWithMapper(((i, v)) =>
61
-
switch v {
62
-
| StringS(s) => Some((i, s))
63
-
| _ => None
64
-
}
65
-
)
66
-
->Array.keepSome
67
-
->Map.fromArray
68
-
StringS(StringA.Atom.substDeBruijn(s, stringSubs, ~from?, ~to))
57
+
let stringSubs = substs->Array.map(s =>
58
+
switch s {
59
+
| Some(StringS(s)) => Some(s)
60
+
| _ => None
61
+
}
62
+
)
63
+
StringS(StringA.Atom.substDeBruijn(s, stringSubs, ~from?))
69
64
}
70
65
| ConstS(s) => ConstS(s)
71
66
}
+1
-1
src/Symbolic.res
+1
-1
src/Symbolic.res
···
18
18
let substitute = (name, _) => name
19
19
let lowerVar = _ => None
20
20
let lowerSchematic = (_, _) => None
21
-
let substDeBruijn = (name, _, ~from as _=?, ~to as _) => name
21
+
let substDeBruijn = (name, _, ~from as _=?) => name
22
22
let concrete = _ => false
23
23
let upshift = (t, _, ~from as _=?) => t
24
24
}
+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
}