the next generation of the in-browser educational proof assistant
simplify coercions
+29
-80
+8
-43
src/AtomDef.res
+8
-43
src/AtomDef.res
···
1
1
// type level stuff to enable well-typed coercions
2
2
type atomTag<_> = ..
3
-
type rec eq<_, _> = Refl: eq<'a, 'a>
4
3
5
4
module type ATOM = {
6
5
type t
7
6
type subst = Map.t<int, t>
8
7
type atomTag<_> += Tag: atomTag<t>
9
-
let tagEq: atomTag<'a> => option<eq<t, 'a>>
10
8
let unify: (t, t, ~gen: ref<int>=?) => Seq.t<subst>
11
9
let prettyPrint: (t, ~scope: array<string>) => string
12
10
let parse: (string, ~scope: array<string>, ~gen: ref<int>=?) => result<(t, string), string>
···
19
17
type rec hValue = HValue(atomTag<'a>, 'a): hValue
20
18
module type COERCIBLE_ATOM = {
21
19
include ATOM
22
-
let liftHValue: hValue => option<t>
23
-
let getHValue: t => hValue
20
+
let coerce: hValue => option<t>
24
21
}
25
22
26
23
type loweredSExp = Var({idx: int}) | Schematic({schematic: int, allowed: array<int>})
27
24
type atomTag<_> += SExpTag: atomTag<loweredSExp>
28
-
let tagEqSExp = (type a, tag: atomTag<a>): option<eq<loweredSExp, a>> =>
29
-
switch tag {
30
-
| SExpTag => Some(Refl)
31
-
| _ => None
32
-
}
33
25
34
-
// coercion<t> represents a coercion from some type 'a to t,
35
-
// along with a function that effectively checks whether its argument is
36
-
// an instance of the coerced type. see usage in MakeCoercible.liftHValue
37
-
type rec coercion<_> =
38
-
Coercion({tagEq: 'c. atomTag<'c> => option<eq<'a, 'c>>, coerce: 'a => option<'b>}): coercion<'b>
39
-
module MakeCoercible = (
40
-
Atom: ATOM,
41
-
Coercions: {
42
-
let coercions: array<coercion<Atom.t>>
43
-
},
44
-
): (COERCIBLE_ATOM with type t = Atom.t) => {
45
-
include Atom
46
-
let liftHValue = (HValue(tag, val)) =>
47
-
Array.findMap(Coercions.coercions, (Coercion(c)) =>
48
-
switch c.tagEq(tag) {
49
-
| Some(Refl) => c.coerce(val)
50
-
| None => None
51
-
}
52
-
)
53
-
let getHValue = t => HValue(Atom.Tag, t)
54
-
}
55
-
56
-
exception MatchCombineAtomBoth
57
26
exception MatchCombineAtomForeign
58
27
59
28
module CombineAtom = (Left: COERCIBLE_ATOM, Right: COERCIBLE_ATOM): {
···
75
44
type subst = Map.t<int, t>
76
45
type gen = ref<int>
77
46
type atomTag<_> += Tag: atomTag<t>
78
-
let tagEq = (type a, tag: atomTag<a>): option<eq<t, a>> =>
79
-
switch tag {
80
-
| Tag => Some(Refl)
81
-
| _ => None
82
-
}
83
-
let liftHValue = v => Some(Foreign(v))
47
+
let coerce = v => Some(Foreign(v))
84
48
let match = (t, leftBranch: Left.t => 'a, rightBranch: Right.t => 'a): 'a =>
85
49
switch t {
86
50
| Left(s) => leftBranch(s)
87
51
| Right(s) => rightBranch(s)
88
52
| Foreign(_) => throw(MatchCombineAtomForeign)
89
53
}
90
-
let getHValue = t => t->match(Left.getHValue, Right.getHValue)
54
+
let wrapLeft = left => HValue(Left.Tag, left)
55
+
let wrapRight = right => HValue(Right.Tag, right)
91
56
let parse = (s, ~scope, ~gen: option<gen>=?) => {
92
57
Left.parse(s, ~scope, ~gen?)
93
58
->Result.map(((r, rest)) => (Left(r), rest))
···
108
73
let coerceToLeft = (t): option<Left.t> =>
109
74
switch t {
110
75
| Left(s) => Some(s)
111
-
| Right(s) => s->Right.getHValue->Left.liftHValue
112
-
| Foreign(v) => Left.liftHValue(v)
76
+
| Right(s) => s->wrapRight->Left.coerce
77
+
| Foreign(v) => Left.coerce(v)
113
78
}
114
79
let coerceToRight = (t): option<Right.t> =>
115
80
switch t {
116
81
| Right(s) => Some(s)
117
-
| Left(s) => s->Left.getHValue->Right.liftHValue
118
-
| Foreign(v) => Right.liftHValue(v)
82
+
| Left(s) => s->wrapLeft->Right.coerce
83
+
| Foreign(v) => Right.coerce(v)
119
84
}
120
85
let substitute = (s, subst: subst) => {
121
86
s->match(
+19
-25
src/Coercible.res
+19
-25
src/Coercible.res
···
1
1
open AtomDef
2
2
3
-
module StringA = MakeCoercible(
4
-
StringA.Atom,
5
-
{
6
-
let coercions = [
7
-
Coercion({
8
-
tagEq: Symbolic.Atom.tagEq,
9
-
coerce: s => Some([StringA.String(s)]),
10
-
}),
11
-
Coercion({
12
-
tagEq: tagEqSExp,
13
-
coerce: t =>
14
-
switch t {
15
-
| Var({idx}) => Some([StringA.Var({idx: idx})])
16
-
| Schematic({schematic, allowed}) => Some([StringA.Schematic({schematic, allowed})])
17
-
},
18
-
}),
19
-
]
20
-
},
21
-
)
3
+
module StringA: COERCIBLE_ATOM with type t = StringA.t = {
4
+
include StringA.Atom
5
+
let coerce = (HValue(tag, a)) =>
6
+
switch tag {
7
+
| Symbolic.Atom.Tag => Some([StringA.String(a)])
8
+
| AtomDef.SExpTag =>
9
+
Some([
10
+
switch a {
11
+
| Var({idx}) => StringA.Var({idx: idx})
12
+
| Schematic({schematic, allowed}) => StringA.Schematic({schematic, allowed})
13
+
},
14
+
])
15
+
| _ => None
16
+
}
17
+
}
22
18
23
-
module Symbolic = MakeCoercible(
24
-
Symbolic.Atom,
25
-
{
26
-
let coercions = []
27
-
},
28
-
)
19
+
module Symbolic: COERCIBLE_ATOM with type t = Symbolic.Atom.t = {
20
+
include Symbolic.Atom
21
+
let coerce = _ => None
22
+
}
+2
-2
src/SExp.res
+2
-2
src/SExp.res
···
150
150
let rec lower = (term: t): option<Atom.t> =>
151
151
switch term {
152
152
| Atom(s) => Some(s)
153
-
| Var({idx}) => Atom.liftHValue(HValue(AtomDef.SExpTag, AtomDef.Var({idx: idx})))
153
+
| Var({idx}) => Atom.coerce(HValue(AtomDef.SExpTag, AtomDef.Var({idx: idx})))
154
154
| Schematic({schematic, allowed}) =>
155
-
Atom.liftHValue(HValue(AtomDef.SExpTag, AtomDef.Schematic({schematic, allowed})))
155
+
Atom.coerce(HValue(AtomDef.SExpTag, AtomDef.Schematic({schematic, allowed})))
156
156
| Compound({subexps: [e1]}) => lower(e1)
157
157
| _ => None
158
158
}
-5
src/StringA.res
-5
src/StringA.res
···
15
15
type t = t
16
16
type subst = Map.t<schematic, t>
17
17
type AtomDef.atomTag<_> += Tag: AtomDef.atomTag<t>
18
-
let tagEq = (type a, tag: AtomDef.atomTag<a>): option<AtomDef.eq<t, a>> =>
19
-
switch tag {
20
-
| Tag => Some(Refl)
21
-
| _ => None
22
-
}
23
18
let substitute = (term: t, subst: subst) =>
24
19
Array.flatMap(term, piece => {
25
20
switch piece {
-5
src/Symbolic.res
-5
src/Symbolic.res
···
4
4
type t = string
5
5
type subst = Map.t<int, string>
6
6
type atomTag<_> += Tag: atomTag<t>
7
-
let tagEq = (type a, tag: atomTag<a>): option<eq<t, a>> =>
8
-
switch tag {
9
-
| Tag => Some(Refl)
10
-
| _ => None
11
-
}
12
7
let unify = (a, b, ~gen as _=?) =>
13
8
if a == b {
14
9
Seq.once(Map.make())