the next generation of the in-browser educational proof assistant
checkpoint
+213
-120
+1
-1
index.html
+1
-1
index.html
+168
src/AtomDef.res
+168
src/AtomDef.res
···
1
+
// type level stuff to enable well-typed coercions
2
+
type typeTag<_> = ..
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
+
7
+
module type ATOM = {
8
+
type t
9
+
type subst = Map.t<int, t>
10
+
let tagEq: typeTag<'a> => option<eq<t, 'a>>
11
+
let tag: typeTag<t>
12
+
let unify: (t, t, ~gen: ref<int>=?) => Seq.t<subst>
13
+
let prettyPrint: (t, ~scope: array<string>) => string
14
+
let parse: (string, ~scope: array<string>, ~gen: ref<int>=?) => result<(t, string), string>
15
+
let substitute: (t, subst) => t
16
+
let upshift: (t, int, ~from: int=?) => t
17
+
// used for when trying to substitute a variable of the wrong type
18
+
let lowerVar: int => option<t>
19
+
let lowerSchematic: (int, array<int>) => option<t>
20
+
let substDeBruijn: (t, array<option<t>>, ~from: int=?) => t
21
+
let concrete: t => bool
22
+
}
23
+
24
+
module type COERCIBLE_ATOM = {
25
+
include ATOM
26
+
let coercions: array<coercion<t>>
27
+
}
28
+
29
+
module MakeCoercible = (
30
+
Atom: ATOM,
31
+
Coercions: {
32
+
let coercions: array<coercion<Atom.t>>
33
+
},
34
+
): (COERCIBLE_ATOM with type t = Atom.t) => {
35
+
include Atom
36
+
let coercions = Coercions.coercions
37
+
}
38
+
39
+
exception RawVarOrSchematic
40
+
module CombineAtom = (Left: COERCIBLE_ATOM, Right: COERCIBLE_ATOM): {
41
+
type base =
42
+
| Left(Left.t)
43
+
| Right(Right.t)
44
+
// neither of the below should appear organically. they're purely so we can lower
45
+
// substitutions to both Left.t and Right.t
46
+
| Var({idx: int})
47
+
| Schematic({schematic: int, allowed: array<int>})
48
+
include COERCIBLE_ATOM with type t = base
49
+
let match: (t, Left.t => 'a, Right.t => 'a) => 'a
50
+
} => {
51
+
type base =
52
+
| Left(Left.t)
53
+
| Right(Right.t)
54
+
| Var({idx: int})
55
+
| Schematic({schematic: int, allowed: array<int>})
56
+
type t = base
57
+
type subst = Map.t<int, t>
58
+
type gen = ref<int>
59
+
type typeTag<_> += Tag: typeTag<t>
60
+
let tag = Tag
61
+
let tagEq = (type a, tag: typeTag<a>): option<eq<t, a>> =>
62
+
switch tag {
63
+
| Tag => Some(Refl)
64
+
| _ => None
65
+
}
66
+
let coercions = {
67
+
let left =
68
+
Left.coercions->Array.map((Coercion((tag, f))) => Coercion((
69
+
tag,
70
+
x => f(x)->Option.map(v => Left(v)),
71
+
)))
72
+
let right =
73
+
Right.coercions->Array.map((Coercion((tag, f))) => Coercion((
74
+
tag,
75
+
x => f(x)->Option.map(v => Right(v)),
76
+
)))
77
+
Array.concat(left, right)
78
+
}
79
+
let match = (t, leftBranch: Left.t => 'a, rightBranch: Right.t => 'a): 'a =>
80
+
switch t {
81
+
| Left(s) => leftBranch(s)
82
+
| Right(s) => rightBranch(s)
83
+
| _ => throw(RawVarOrSchematic)
84
+
}
85
+
let parse = (s, ~scope, ~gen: option<gen>=?) => {
86
+
Left.parse(s, ~scope, ~gen?)
87
+
->Result.map(((r, rest)) => (Left(r), rest))
88
+
->Util.Result.or(() =>
89
+
Right.parse(s, ~scope, ~gen?)->Result.map(((r, rest)) => (Right(r), rest))
90
+
)
91
+
}
92
+
let prettyPrint = (s, ~scope) =>
93
+
s->match(left => Left.prettyPrint(left, ~scope), right => Right.prettyPrint(right, ~scope))
94
+
let unify = (s1, s2, ~gen=?) =>
95
+
switch (s1, s2) {
96
+
| (Left(s1), Left(s2)) =>
97
+
Left.unify(s1, s2, ~gen?)->Seq.map(subst => subst->Util.mapMapValues(v => Left(v)))
98
+
| (Right(s1), Right(s2)) =>
99
+
Right.unify(s1, s2, ~gen?)->Seq.map(subst => subst->Util.mapMapValues(v => Right(v)))
100
+
| (_, _) => Seq.empty
101
+
}
102
+
let coerceLeft = (left: Left.t): option<Right.t> =>
103
+
Array.findMap(Right.coercions, (Coercion((tag, f))) =>
104
+
switch Left.tagEq(tag) {
105
+
| Some(Refl) => f(left)
106
+
| None => None
107
+
}
108
+
)
109
+
let coerceRight = (right: Right.t): option<Left.t> => {
110
+
Array.findMap(Left.coercions, (Coercion((tag, f))) =>
111
+
switch Right.tagEq(tag) {
112
+
| Some(Refl) => f(right)
113
+
| None => None
114
+
}
115
+
)
116
+
}
117
+
let substitute = (s, subst: subst) => {
118
+
s->match(
119
+
left => {
120
+
let leftSubs =
121
+
subst->Util.Map.filterMap((_, v) => v->match(left => Some(left), coerceRight))
122
+
Left(Left.substitute(left, leftSubs))
123
+
},
124
+
right => {
125
+
let rightSubs =
126
+
subst->Util.Map.filterMap((_, v) => v->match(coerceLeft, right => Some(right)))
127
+
Right(Right.substitute(right, rightSubs))
128
+
},
129
+
)
130
+
}
131
+
let upshift = (s, amount: int, ~from=?) =>
132
+
s->match(
133
+
left => Left(left->Left.upshift(amount, ~from?)),
134
+
right => Right(right->Right.upshift(amount, ~from?)),
135
+
)
136
+
let lowerVar = idx => Some(Var({idx: idx}))
137
+
let lowerSchematic = (schematic, allowed) => Some(Schematic({schematic, allowed}))
138
+
let substDeBruijn = (s, substs: array<option<t>>, ~from=?) =>
139
+
s->match(
140
+
left => {
141
+
let leftSubs = substs->Array.map(o =>
142
+
o->Option.flatMap(s =>
143
+
switch s {
144
+
| Left(s) => Some(s)
145
+
| Var({idx}) => Left.lowerVar(idx)
146
+
| Schematic({schematic, allowed}) => Left.lowerSchematic(schematic, allowed)
147
+
| Right(s) => coerceRight(s)
148
+
}
149
+
)
150
+
)
151
+
Left(Left.substDeBruijn(left, leftSubs, ~from?))
152
+
},
153
+
right => {
154
+
let rightSubs = substs->Array.map(o =>
155
+
o->Option.flatMap(s =>
156
+
switch s {
157
+
| Right(s) => Some(s)
158
+
| Var({idx}) => Right.lowerVar(idx)
159
+
| Schematic({schematic, allowed}) => Right.lowerSchematic(schematic, allowed)
160
+
| Left(s) => coerceLeft(s)
161
+
}
162
+
)
163
+
)
164
+
Right(Right.substDeBruijn(right, rightSubs, ~from?))
165
+
},
166
+
)
167
+
let concrete = s => s->match(Left.concrete, Right.concrete)
168
+
}
+15
src/Coercible.res
+15
src/Coercible.res
+6
-93
src/CombinedAtom.res
+6
-93
src/CombinedAtom.res
···
1
1
module type ATOM = SExpFunc.ATOM
2
2
exception RawVarOrSchematic
3
3
4
-
module MakeAtom = (Left: ATOM, Right: ATOM): {
4
+
module MakeAtom = (Left: AtomDef.COERCIBLE_ATOM, Right: AtomDef.COERCIBLE_ATOM): {
5
5
type base =
6
6
| Left(Left.t)
7
7
| Right(Right.t)
···
11
11
| Schematic({schematic: int, allowed: array<int>})
12
12
include ATOM with type t = base
13
13
let match: (t, Left.t => 'a, Right.t => 'a) => 'a
14
-
} => {
15
-
type base =
16
-
| Left(Left.t)
17
-
| Right(Right.t)
18
-
| Var({idx: int})
19
-
| Schematic({schematic: int, allowed: array<int>})
20
-
type t = base
21
-
type subst = Map.t<int, t>
22
-
type gen = ref<int>
23
-
let match = (t, leftBranch: Left.t => 'a, rightBranch: Right.t => 'a): 'a =>
24
-
switch t {
25
-
| Left(s) => leftBranch(s)
26
-
| Right(s) => rightBranch(s)
27
-
| _ => throw(RawVarOrSchematic)
28
-
}
29
-
let parse = (s, ~scope, ~gen: option<gen>=?) => {
30
-
Left.parse(s, ~scope, ~gen?)
31
-
->Result.map(((r, rest)) => (Left(r), rest))
32
-
->Util.Result.or(() =>
33
-
Right.parse(s, ~scope, ~gen?)->Result.map(((r, rest)) => (Right(r), rest))
34
-
)
35
-
}
36
-
let prettyPrint = (s, ~scope) =>
37
-
s->match(left => Left.prettyPrint(left, ~scope), right => Right.prettyPrint(right, ~scope))
38
-
let unify = (s1, s2, ~gen=?) =>
39
-
switch (s1, s2) {
40
-
| (Left(s1), Left(s2)) =>
41
-
Left.unify(s1, s2, ~gen?)->Seq.map(subst => subst->Util.mapMapValues(v => Left(v)))
42
-
| (Right(s1), Right(s2)) =>
43
-
Right.unify(s1, s2, ~gen?)->Seq.map(subst => subst->Util.mapMapValues(v => Right(v)))
44
-
| (_, _) => Seq.empty
45
-
}
46
-
let substitute = (s, subst: subst) => {
47
-
s->match(
48
-
left => {
49
-
let leftSubs = subst->Util.Map.filterMap((_, v) =>
50
-
switch v {
51
-
| Left(s) => Some(s)
52
-
| _ => None
53
-
}
54
-
)
55
-
Left(Left.substitute(left, leftSubs))
56
-
},
57
-
right => {
58
-
let rightSubs = subst->Util.Map.filterMap((_, v) =>
59
-
switch v {
60
-
| Right(s) => Some(s)
61
-
| _ => None
62
-
}
63
-
)
64
-
Right(Right.substitute(right, rightSubs))
65
-
},
66
-
)
67
-
}
68
-
let upshift = (s, amount: int, ~from=?) =>
69
-
s->match(
70
-
left => Left(left->Left.upshift(amount, ~from?)),
71
-
right => Right(right->Right.upshift(amount, ~from?)),
72
-
)
73
-
let lowerVar = idx => Some(Var({idx: idx}))
74
-
let lowerSchematic = (schematic, allowed) => Some(Schematic({schematic, allowed}))
75
-
let substDeBruijn = (s, substs: array<option<t>>, ~from=?) =>
76
-
s->match(
77
-
left => {
78
-
let leftSubs = substs->Array.map(s =>
79
-
switch s {
80
-
| Some(Left(s)) => Some(s)
81
-
| Some(Var({idx})) => Left.lowerVar(idx)
82
-
| Some(Schematic({schematic, allowed})) => Left.lowerSchematic(schematic, allowed)
83
-
| _ => None
84
-
}
85
-
)
86
-
Left(Left.substDeBruijn(left, leftSubs, ~from?))
87
-
},
88
-
right => {
89
-
let rightSubs = substs->Array.map(s =>
90
-
switch s {
91
-
| Some(Right(s)) => Some(s)
92
-
| Some(Var({idx})) => Right.lowerVar(idx)
93
-
| Some(Schematic({schematic, allowed})) => Right.lowerSchematic(schematic, allowed)
94
-
| _ => None
95
-
}
96
-
)
97
-
Right(Right.substDeBruijn(right, rightSubs, ~from?))
98
-
},
99
-
)
100
-
let concrete = s => s->match(Left.concrete, Right.concrete)
101
-
}
14
+
} => AtomDef.CombineAtom(Left, Right)
102
15
103
16
module type ATOM_VIEW = SExpViewFunc.ATOM_VIEW
104
17
module MakeAtomView = (
105
-
Left: ATOM,
18
+
Left: AtomDef.COERCIBLE_ATOM,
106
19
LeftView: ATOM_VIEW with module Atom := Left,
107
-
Right: ATOM,
20
+
Right: AtomDef.COERCIBLE_ATOM,
108
21
RightView: ATOM_VIEW with module Atom := Right,
109
22
Combined: module type of MakeAtom(Left, Right),
110
23
): {
···
119
32
}
120
33
121
34
module MakeAtomAndView = (
122
-
Left: ATOM,
35
+
Left: AtomDef.COERCIBLE_ATOM,
123
36
LeftView: ATOM_VIEW with module Atom := Left,
124
-
Right: ATOM,
37
+
Right: AtomDef.COERCIBLE_ATOM,
125
38
RightView: ATOM_VIEW with module Atom := Right,
126
39
) => {
127
40
module Atom = MakeAtom(Left, Right)
+1
-14
src/SExpFunc.res
+1
-14
src/SExpFunc.res
···
1
1
exception SubstNotCompatible(string)
2
2
3
-
module type ATOM = {
4
-
type t
5
-
type subst = Map.t<int, t>
6
-
let unify: (t, t, ~gen: ref<int>=?) => Seq.t<subst>
7
-
let prettyPrint: (t, ~scope: array<string>) => string
8
-
let parse: (string, ~scope: array<string>, ~gen: ref<int>=?) => result<(t, string), string>
9
-
let substitute: (t, subst) => t
10
-
let upshift: (t, int, ~from: int=?) => t
11
-
// used for when trying to substitute a variable of the wrong type
12
-
let lowerVar: int => option<t>
13
-
let lowerSchematic: (int, array<int>) => option<t>
14
-
let substDeBruijn: (t, array<option<t>>, ~from: int=?) => t
15
-
let concrete: t => bool
16
-
}
3
+
module type ATOM = AtomDef.ATOM
17
4
18
5
module IntCmp = Belt.Id.MakeComparable({
19
6
type t = int
+2
-2
src/Scratch.res
+2
-2
src/Scratch.res
···
43
43
module ConfS = ConfigBlock.Make(HOTerm, HOTerm)
44
44
45
45
module StringSymbol = CombinedAtom.MakeAtomAndView(
46
-
StringA.Atom,
46
+
Coercible.StringA,
47
47
StringA.AtomView,
48
-
Symbolic.Atom,
48
+
Coercible.Symbolic,
49
49
Symbolic.AtomView,
50
50
)
51
51
module StringSExp = SExpFunc.Make(StringSymbol.Atom)
+8
-6
src/StringA.res
+8
-6
src/StringA.res
···
12
12
type schematic = int
13
13
14
14
module Atom = {
15
+
open AtomDef
15
16
type t = t
16
17
type subst = Map.t<schematic, t>
18
+
type typeTag<_> += Tag: typeTag<t>
19
+
let tag = Tag
20
+
let tagEq = (type a, tag: typeTag<a>): option<eq<t, a>> =>
21
+
switch tag {
22
+
| Tag => Some(Refl)
23
+
| _ => None
24
+
}
17
25
let substitute = (term: t, subst: subst) =>
18
26
Array.flatMap(term, piece => {
19
27
switch piece {
···
481
489
{React.int(props.idx)}
482
490
</span>
483
491
}
484
-
485
-
let makeMeta = (str: string) =>
486
-
<span className="rule-binder">
487
-
{React.string(str)}
488
-
{React.string(".")}
489
-
</span>
490
492
491
493
let parenthesise = f =>
492
494
[
+1
-1
src/StringA.resi
+1
-1
src/StringA.resi
+2
-2
src/StringAxiomSet.res
+2
-2
src/StringAxiomSet.res
+8
src/Symbolic.res
+8
src/Symbolic.res
···
1
1
type t = string
2
2
module Atom = {
3
+
open AtomDef
3
4
type t = string
4
5
type subst = Map.t<int, string>
6
+
type typeTag<_> += Tag: typeTag<t>
7
+
let tag = Tag
8
+
let tagEq = (type a, tag: typeTag<a>): option<eq<t, a>> =>
9
+
switch tag {
10
+
| Tag => Some(Refl)
11
+
| _ => None
12
+
}
5
13
let unify = (a, b, ~gen as _=?) =>
6
14
if a == b {
7
15
Seq.once(Map.make())