the next generation of the in-browser educational proof assistant
coercions b/w atoms rather than intermediaries
+42
-35
+36
-34
src/AtomDef.res
+36
-34
src/AtomDef.res
···
20
20
}
21
21
22
22
// coercion<t> represents a coercion from some type 'a to t
23
-
type rec coercion<_> = Coercion(typeTag<'a>, 'a => option<'b>): coercion<'b>
23
+
type rec coercion<_> =
24
+
Coercion({tagEq: 'c. typeTag<'c> => option<eq<'a, 'c>>, coerce: 'a => option<'b>}): coercion<'b>
25
+
type rec existsValue = ExistsValue(typeTag<'a>, 'a): existsValue
24
26
module type COERCIBLE_ATOM = {
25
27
include ATOM
26
28
let coercions: array<coercion<t>>
29
+
let unwrap: t => existsValue
27
30
}
28
31
29
32
module MakeCoercible = (
···
34
37
): (COERCIBLE_ATOM with type t = Atom.t) => {
35
38
include Atom
36
39
let coercions = Coercions.coercions
40
+
let unwrap = t => ExistsValue(Atom.tag, t)
37
41
}
38
42
39
-
exception MatchCombineAtomVar
40
-
exception MatchCombineAtomSchematic
43
+
exception MatchCombineAtomBoth
41
44
42
45
module CombineAtom = (Left: COERCIBLE_ATOM, Right: COERCIBLE_ATOM): {
43
46
type base =
44
47
| Left(Left.t)
45
48
| Right(Right.t)
46
-
// neither of the below should appear organically. they're purely so we can lower
47
-
// substitutions to both Left.t and Right.t
48
-
| Var({idx: int})
49
-
| Schematic({schematic: int, allowed: array<int>})
49
+
// used strictly for SExp -> Atom coercions
50
+
// should not be parsed or otherwise appear organically
51
+
| Both(option<Left.t>, option<Right.t>)
50
52
include COERCIBLE_ATOM with type t = base
51
53
let match: (t, Left.t => 'a, Right.t => 'a) => 'a
52
54
} => {
53
55
type base =
54
56
| Left(Left.t)
55
57
| Right(Right.t)
56
-
| Var({idx: int})
57
-
| Schematic({schematic: int, allowed: array<int>})
58
+
| Both(option<Left.t>, option<Right.t>)
58
59
type t = base
59
60
type subst = Map.t<int, t>
60
61
type gen = ref<int>
···
66
67
| _ => None
67
68
}
68
69
let coercions = {
69
-
let left =
70
-
Left.coercions->Array.map((Coercion((tag, f))) => Coercion((
71
-
tag,
72
-
x => f(x)->Option.map(v => Left(v)),
73
-
)))
74
-
let right =
75
-
Right.coercions->Array.map((Coercion((tag, f))) => Coercion((
76
-
tag,
77
-
x => f(x)->Option.map(v => Right(v)),
78
-
)))
70
+
let left = Left.coercions->Array.map((Coercion(c)) => Coercion({
71
+
...c,
72
+
coerce: x => c.coerce(x)->Option.map(v => Left(v)),
73
+
}))
74
+
let right = Right.coercions->Array.map((Coercion(c)) => Coercion({
75
+
...c,
76
+
coerce: x => c.coerce(x)->Option.map(v => Right(v)),
77
+
}))
79
78
Array.concat(left, right)
80
79
}
81
80
let match = (t, leftBranch: Left.t => 'a, rightBranch: Right.t => 'a): 'a =>
82
81
switch t {
83
82
| Left(s) => leftBranch(s)
84
83
| Right(s) => rightBranch(s)
85
-
| Var(_) => throw(MatchCombineAtomVar)
86
-
| Schematic(_) => throw(MatchCombineAtomSchematic)
84
+
| Both(_) => throw(MatchCombineAtomBoth)
87
85
}
86
+
let unwrap = t => t->match(Left.unwrap, Right.unwrap)
88
87
let parse = (s, ~scope, ~gen: option<gen>=?) => {
89
88
Left.parse(s, ~scope, ~gen?)
90
89
->Result.map(((r, rest)) => (Left(r), rest))
···
102
101
Right.unify(s1, s2, ~gen?)->Seq.map(subst => subst->Util.mapMapValues(v => Right(v)))
103
102
| (_, _) => Seq.empty
104
103
}
105
-
let coerceLeft = (left: Left.t): option<Right.t> =>
106
-
Array.findMap(Right.coercions, (Coercion((tag, f))) =>
107
-
switch Left.tagEq(tag) {
108
-
| Some(Refl) => f(left)
104
+
let coerceLeft = (left: Left.t): option<Right.t> => {
105
+
let ExistsValue(srcTag, srcVal) = Left.unwrap(left)
106
+
Array.findMap(Right.coercions, (Coercion(c)) =>
107
+
switch c.tagEq(srcTag) {
108
+
| Some(Refl) => c.coerce(srcVal)
109
109
| None => None
110
110
}
111
111
)
112
+
}
112
113
let coerceRight = (right: Right.t): option<Left.t> => {
113
-
Array.findMap(Left.coercions, (Coercion((tag, f))) =>
114
-
switch Right.tagEq(tag) {
115
-
| Some(Refl) => f(right)
114
+
let ExistsValue(srcTag, srcVal) = Right.unwrap(right)
115
+
Array.findMap(Left.coercions, (Coercion(c)) =>
116
+
switch c.tagEq(srcTag) {
117
+
| Some(Refl) => c.coerce(srcVal)
116
118
| None => None
117
119
}
118
120
)
···
136
138
left => Left(left->Left.upshift(amount, ~from?)),
137
139
right => Right(right->Right.upshift(amount, ~from?)),
138
140
)
139
-
let lowerVar = idx => Some(Var({idx: idx}))
140
-
let lowerSchematic = (schematic, allowed) => Some(Schematic({schematic, allowed}))
141
+
let lowerVar = idx => Some(Both(Left.lowerVar(idx), Right.lowerVar(idx)))
142
+
let lowerSchematic = (schematic, allowed) => Some(
143
+
Both(Left.lowerSchematic(schematic, allowed), Right.lowerSchematic(schematic, allowed)),
144
+
)
141
145
let substDeBruijn = (s, substs: array<option<t>>, ~from=?) =>
142
146
s->match(
143
147
left => {
···
145
149
o->Option.flatMap(s =>
146
150
switch s {
147
151
| Left(s) => Some(s)
148
-
| Var({idx}) => Left.lowerVar(idx)
149
-
| Schematic({schematic, allowed}) => Left.lowerSchematic(schematic, allowed)
152
+
| Both(os, _) => os
150
153
| Right(s) => coerceRight(s)
151
154
}
152
155
)
···
158
161
o->Option.flatMap(s =>
159
162
switch s {
160
163
| Right(s) => Some(s)
161
-
| Var({idx}) => Right.lowerVar(idx)
162
-
| Schematic({schematic, allowed}) => Right.lowerSchematic(schematic, allowed)
164
+
| Both(_, os) => os
163
165
| Left(s) => coerceLeft(s)
164
166
}
165
167
)
+6
-1
src/Coercible.res
+6
-1
src/Coercible.res