the next generation of the in-browser educational proof assistant
reorganise
+55
-65
+40
-4
src/AtomDef.res
+40
-4
src/AtomDef.res
···
1
1
// type level stuff to enable well-typed coercions
2
2
type typeTag<_> = ..
3
3
type rec eq<_, _> = Refl: eq<'a, 'a>
4
-
// coercion<t> represents a coercion from some type 'a to t
5
-
type rec coercion<_> = Coercion(typeTag<'a>, 'a => option<'b>): coercion<'b>
6
4
7
5
module type ATOM = {
8
6
type t
···
21
19
let concrete: t => bool
22
20
}
23
21
22
+
// coercion<t> represents a coercion from some type 'a to t
23
+
type rec coercion<_> = Coercion(typeTag<'a>, 'a => option<'b>): coercion<'b>
24
24
module type COERCIBLE_ATOM = {
25
25
include ATOM
26
26
let coercions: array<coercion<t>>
···
36
36
let coercions = Coercions.coercions
37
37
}
38
38
39
-
exception RawVarOrSchematic
39
+
exception MatchCombineAtomVar
40
+
exception MatchCombineAtomSchematic
41
+
40
42
module CombineAtom = (Left: COERCIBLE_ATOM, Right: COERCIBLE_ATOM): {
41
43
type base =
42
44
| Left(Left.t)
···
80
82
switch t {
81
83
| Left(s) => leftBranch(s)
82
84
| Right(s) => rightBranch(s)
83
-
| _ => throw(RawVarOrSchematic)
85
+
| Var(_) => throw(MatchCombineAtomVar)
86
+
| Schematic(_) => throw(MatchCombineAtomSchematic)
84
87
}
85
88
let parse = (s, ~scope, ~gen: option<gen>=?) => {
86
89
Left.parse(s, ~scope, ~gen?)
···
166
169
)
167
170
let concrete = s => s->match(Left.concrete, Right.concrete)
168
171
}
172
+
173
+
module type ATOM_VIEW = {
174
+
module Atom: ATOM
175
+
type props = {name: Atom.t, scope: array<string>}
176
+
let make: props => React.element
177
+
}
178
+
179
+
module MakeAtomView = (
180
+
Left: COERCIBLE_ATOM,
181
+
LeftView: ATOM_VIEW with module Atom := Left,
182
+
Right: COERCIBLE_ATOM,
183
+
RightView: ATOM_VIEW with module Atom := Right,
184
+
Combined: module type of CombineAtom(Left, Right),
185
+
): {
186
+
include ATOM_VIEW with module Atom := Combined
187
+
} => {
188
+
type props = {name: Combined.t, scope: array<string>}
189
+
let make = ({name, scope}: props) =>
190
+
name->Combined.match(
191
+
left => <LeftView name={left} scope />,
192
+
right => <RightView name={right} scope />,
193
+
)
194
+
}
195
+
196
+
module MakeAtomAndView = (
197
+
Left: COERCIBLE_ATOM,
198
+
LeftView: ATOM_VIEW with module Atom := Left,
199
+
Right: COERCIBLE_ATOM,
200
+
RightView: ATOM_VIEW with module Atom := Right,
201
+
) => {
202
+
module Atom = CombineAtom(Left, Right)
203
+
module AtomView = MakeAtomView(Left, LeftView, Right, RightView, Atom)
204
+
}
-42
src/CombinedAtom.res
-42
src/CombinedAtom.res
···
1
-
module type ATOM = SExpFunc.ATOM
2
-
exception RawVarOrSchematic
3
-
4
-
module MakeAtom = (Left: AtomDef.COERCIBLE_ATOM, Right: AtomDef.COERCIBLE_ATOM): {
5
-
type base =
6
-
| Left(Left.t)
7
-
| Right(Right.t)
8
-
// neither of the below should appear organically. they're purely so we can lower
9
-
// substitutions to both Left.t and Right.t
10
-
| Var({idx: int})
11
-
| Schematic({schematic: int, allowed: array<int>})
12
-
include ATOM with type t = base
13
-
let match: (t, Left.t => 'a, Right.t => 'a) => 'a
14
-
} => AtomDef.CombineAtom(Left, Right)
15
-
16
-
module type ATOM_VIEW = SExpViewFunc.ATOM_VIEW
17
-
module MakeAtomView = (
18
-
Left: AtomDef.COERCIBLE_ATOM,
19
-
LeftView: ATOM_VIEW with module Atom := Left,
20
-
Right: AtomDef.COERCIBLE_ATOM,
21
-
RightView: ATOM_VIEW with module Atom := Right,
22
-
Combined: module type of MakeAtom(Left, Right),
23
-
): {
24
-
include ATOM_VIEW with module Atom := Combined
25
-
} => {
26
-
type props = {name: Combined.t, scope: array<string>}
27
-
let make = ({name, scope}: props) =>
28
-
name->Combined.match(
29
-
left => <LeftView name={left} scope />,
30
-
right => <RightView name={right} scope />,
31
-
)
32
-
}
33
-
34
-
module MakeAtomAndView = (
35
-
Left: AtomDef.COERCIBLE_ATOM,
36
-
LeftView: ATOM_VIEW with module Atom := Left,
37
-
Right: AtomDef.COERCIBLE_ATOM,
38
-
RightView: ATOM_VIEW with module Atom := Right,
39
-
) => {
40
-
module Atom = MakeAtom(Left, Right)
41
-
module AtomView = MakeAtomView(Left, LeftView, Right, RightView, Atom)
42
-
}
src/SExpFunc.res
src/SExp.res
src/SExpFunc.res
src/SExp.res
+3
-7
src/SExpViewFunc.res
src/SExpView.res
+3
-7
src/SExpViewFunc.res
src/SExpView.res
···
1
-
module type ATOM_VIEW = {
2
-
module Atom: SExpFunc.ATOM
3
-
type props = {name: Atom.t, scope: array<string>}
4
-
let make: props => React.element
5
-
}
1
+
module type ATOM_VIEW = AtomDef.ATOM_VIEW
6
2
7
3
module Make = (
8
-
Atom: SExpFunc.ATOM,
4
+
Atom: AtomDef.ATOM,
9
5
AtomView: ATOM_VIEW with module Atom := Atom,
10
-
SExp: module type of SExpFunc.Make(Atom),
6
+
SExp: module type of SExp.Make(Atom),
11
7
): {
12
8
include Signatures.TERM_VIEW with module Term := SExp
13
9
} => {
+3
-3
src/Scratch.res
+3
-3
src/Scratch.res
···
42
42
module TheoremS = Editable.TextArea(Theorem.Make(HOTerm, HOTerm, HOTermJView, DLRView))
43
43
module ConfS = ConfigBlock.Make(HOTerm, HOTerm)
44
44
45
-
module StringSymbol = CombinedAtom.MakeAtomAndView(
45
+
module StringSymbol = AtomDef.MakeAtomAndView(
46
46
Coercible.StringA,
47
47
StringA.AtomView,
48
48
Coercible.Symbolic,
49
49
Symbolic.AtomView,
50
50
)
51
-
module StringSExp = SExpFunc.Make(StringSymbol.Atom)
52
-
module TermView = SExpViewFunc.Make(StringSymbol.Atom, StringSymbol.AtomView, StringSExp)
51
+
module StringSExp = SExp.Make(StringSymbol.Atom)
52
+
module TermView = SExpView.Make(StringSymbol.Atom, StringSymbol.AtomView, StringSExp)
53
53
module StringSExpJView = TermViewAsJudgmentView.Make(StringSExp, StringSExp, TermView)
54
54
module AxiomStr = Editable.TextArea(StringAxiomSet)
55
55
+1
-1
src/StringA.res
+1
-1
src/StringA.res
+1
-1
src/StringA.resi
+1
-1
src/StringA.resi
+3
-3
src/StringAxiomSet.res
+3
-3
src/StringAxiomSet.res
···
1
1
open Component
2
2
3
-
module StringSymbol = CombinedAtom.MakeAtomAndView(
3
+
module StringSymbol = AtomDef.MakeAtomAndView(
4
4
Coercible.StringA,
5
5
StringA.AtomView,
6
6
Coercible.Symbolic,
7
7
Symbolic.AtomView,
8
8
)
9
-
module StringSExp = SExpFunc.Make(StringSymbol.Atom)
10
-
module TermView = SExpViewFunc.Make(StringSymbol.Atom, StringSymbol.AtomView, StringSExp)
9
+
module StringSExp = SExp.Make(StringSymbol.Atom)
10
+
module TermView = SExpView.Make(StringSymbol.Atom, StringSymbol.AtomView, StringSExp)
11
11
module JudgmentView = TermViewAsJudgmentView.Make(StringSExp, StringSExp, TermView)
12
12
13
13
module Rule = Rule.Make(StringSExp, StringSExp)
+1
-1
src/Symbolic.resi
+1
-1
src/Symbolic.resi
+1
-1
src/Theorem.res
+1
-1
src/Theorem.res
···
63
63
Proof.check(ctx, proof, props.content.rule)->ignore
64
64
{...props.content, proof, substFailed: None}
65
65
} catch {
66
-
| SExpFunc.SubstNotCompatible(s) => {...props.content, substFailed: Some(s)}
66
+
| SExp.SubstNotCompatible(s) => {...props.content, substFailed: Some(s)}
67
67
},
68
68
~exports={
69
69
Ports.facts: Dict.fromArray([(props.content.name, props.content.rule)]),
+1
-1
tests/SExpTest.res
+1
-1
tests/SExpTest.res