the next generation of the in-browser educational proof assistant
introduce foreign to lazily evaluate conversion
+40
-58
+40
-58
src/AtomDef.res
+40
-58
src/AtomDef.res
···
19
19
let concrete: t => bool
20
20
}
21
21
22
-
// coercion<t> represents a coercion from some type 'a to t
23
-
type rec coercion<_> =
24
-
Coercion({tagEq: 'c. typeTag<'c> => option<eq<'a, 'c>>, coerce: 'a => option<'b>}): coercion<'b>
25
22
type rec existsValue = ExistsValue(typeTag<'a>, 'a): existsValue
26
23
module type COERCIBLE_ATOM = {
27
24
include ATOM
28
-
let coercions: array<coercion<t>>
25
+
let liftForeign: existsValue => option<t>
29
26
let unwrap: t => existsValue
30
27
}
31
28
29
+
// coercion<t> represents a coercion from some type 'a to t,
30
+
// along with a function that effectively checks whether its argument is
31
+
// an instance of the coerced type. see usage in MakeCoercible.liftForeign
32
+
type rec coercion<_> =
33
+
Coercion({tagEq: 'c. typeTag<'c> => option<eq<'a, 'c>>, coerce: 'a => option<'b>}): coercion<'b>
32
34
module MakeCoercible = (
33
35
Atom: ATOM,
34
36
Coercions: {
···
36
38
},
37
39
): (COERCIBLE_ATOM with type t = Atom.t) => {
38
40
include Atom
39
-
let coercions = Coercions.coercions
41
+
let liftForeign = (ExistsValue(tag, val)) =>
42
+
Array.findMap(Coercions.coercions, (Coercion(c)) =>
43
+
switch c.tagEq(tag) {
44
+
| Some(Refl) => c.coerce(val)
45
+
| None => None
46
+
}
47
+
)
40
48
let unwrap = t => ExistsValue(Atom.tag, t)
41
49
}
42
50
43
51
exception MatchCombineAtomBoth
52
+
exception MatchCombineAtomForeign
44
53
45
54
module CombineAtom = (Left: COERCIBLE_ATOM, Right: COERCIBLE_ATOM): {
46
-
type base =
55
+
type rec base =
47
56
| Left(Left.t)
48
57
| Right(Right.t)
49
58
// used strictly for SExp -> Atom coercions
50
59
// should not be parsed or otherwise appear organically
51
60
| Both(option<Left.t>, option<Right.t>)
61
+
// likewise, strictly for Atom <-> Atom coercions
62
+
// occurs only when passed from some upper part of the tree
63
+
| Foreign(existsValue)
52
64
include COERCIBLE_ATOM with type t = base
53
65
let match: (t, Left.t => 'a, Right.t => 'a) => 'a
54
66
} => {
55
-
type base =
67
+
type rec base =
56
68
| Left(Left.t)
57
69
| Right(Right.t)
58
70
| Both(option<Left.t>, option<Right.t>)
71
+
| Foreign(existsValue)
59
72
type t = base
60
73
type subst = Map.t<int, t>
61
74
type gen = ref<int>
···
66
79
| Tag => Some(Refl)
67
80
| _ => None
68
81
}
69
-
let coercions = {
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
-
}))
78
-
Array.concat(left, right)
79
-
}
82
+
let liftForeign = v => Some(Foreign(v))
80
83
let match = (t, leftBranch: Left.t => 'a, rightBranch: Right.t => 'a): 'a =>
81
84
switch t {
82
85
| Left(s) => leftBranch(s)
83
86
| Right(s) => rightBranch(s)
84
87
| Both(_) => throw(MatchCombineAtomBoth)
88
+
| Foreign(_) => throw(MatchCombineAtomForeign)
85
89
}
86
90
let unwrap = t => t->match(Left.unwrap, Right.unwrap)
87
91
let parse = (s, ~scope, ~gen: option<gen>=?) => {
···
101
105
Right.unify(s1, s2, ~gen?)->Seq.map(subst => subst->Util.mapMapValues(v => Right(v)))
102
106
| (_, _) => Seq.empty
103
107
}
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
-
| None => None
110
-
}
111
-
)
112
-
}
113
-
let coerceRight = (right: Right.t): option<Left.t> => {
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)
118
-
| None => None
119
-
}
120
-
)
121
-
}
108
+
let coerceToLeft = (t): option<Left.t> =>
109
+
switch t {
110
+
| Left(s) => Some(s)
111
+
| Both(os, _) => os
112
+
| Right(s) => s->Right.unwrap->Left.liftForeign
113
+
| Foreign(v) => Left.liftForeign(v)
114
+
}
115
+
let coerceToRight = (t): option<Right.t> =>
116
+
switch t {
117
+
| Right(s) => Some(s)
118
+
| Both(_, os) => os
119
+
| Left(s) => s->Left.unwrap->Right.liftForeign
120
+
| Foreign(v) => Right.liftForeign(v)
121
+
}
122
122
let substitute = (s, subst: subst) => {
123
123
s->match(
124
124
left => {
125
-
let leftSubs =
126
-
subst->Util.Map.filterMap((_, v) => v->match(left => Some(left), coerceRight))
125
+
let leftSubs = subst->Util.Map.filterMap((_, v) => coerceToLeft(v))
127
126
Left(Left.substitute(left, leftSubs))
128
127
},
129
128
right => {
130
-
let rightSubs =
131
-
subst->Util.Map.filterMap((_, v) => v->match(coerceLeft, right => Some(right)))
129
+
let rightSubs = subst->Util.Map.filterMap((_, v) => coerceToRight(v))
132
130
Right(Right.substitute(right, rightSubs))
133
131
},
134
132
)
···
145
143
let substDeBruijn = (s, substs: array<option<t>>, ~from=?) =>
146
144
s->match(
147
145
left => {
148
-
let leftSubs = substs->Array.map(o =>
149
-
o->Option.flatMap(s =>
150
-
switch s {
151
-
| Left(s) => Some(s)
152
-
| Both(os, _) => os
153
-
| Right(s) => coerceRight(s)
154
-
}
155
-
)
156
-
)
146
+
let leftSubs = substs->Array.map(o => o->Option.flatMap(coerceToLeft))
157
147
Left(Left.substDeBruijn(left, leftSubs, ~from?))
158
148
},
159
149
right => {
160
-
let rightSubs = substs->Array.map(o =>
161
-
o->Option.flatMap(s =>
162
-
switch s {
163
-
| Right(s) => Some(s)
164
-
| Both(_, os) => os
165
-
| Left(s) => coerceLeft(s)
166
-
}
167
-
)
168
-
)
150
+
let rightSubs = substs->Array.map(o => o->Option.flatMap(coerceToRight))
169
151
Right(Right.substDeBruijn(right, rightSubs, ~from?))
170
152
},
171
153
)