the next generation of the in-browser educational proof assistant
renames
+26
-31
+21
-22
src/AtomDef.res
+21
-22
src/AtomDef.res
···
1
1
// type level stuff to enable well-typed coercions
2
-
type typeTag<_> = ..
2
+
type atomTag<_> = ..
3
3
type rec eq<_, _> = Refl: eq<'a, 'a>
4
4
5
5
module type ATOM = {
6
6
type t
7
7
type subst = Map.t<int, t>
8
-
let tagEq: typeTag<'a> => option<eq<t, 'a>>
9
-
let tag: typeTag<t>
8
+
type atomTag<_> += Tag: atomTag<t>
9
+
let tagEq: atomTag<'a> => option<eq<t, 'a>>
10
10
let unify: (t, t, ~gen: ref<int>=?) => Seq.t<subst>
11
11
let prettyPrint: (t, ~scope: array<string>) => string
12
12
let parse: (string, ~scope: array<string>, ~gen: ref<int>=?) => result<(t, string), string>
···
19
19
let concrete: t => bool
20
20
}
21
21
22
-
type rec existsValue = ExistsValue(typeTag<'a>, 'a): existsValue
22
+
type rec hValue = HValue(atomTag<'a>, 'a): hValue
23
23
module type COERCIBLE_ATOM = {
24
24
include ATOM
25
-
let liftForeign: existsValue => option<t>
26
-
let unwrap: t => existsValue
25
+
let liftHValue: hValue => option<t>
26
+
let getHValue: t => hValue
27
27
}
28
28
29
29
// coercion<t> represents a coercion from some type 'a to t,
30
30
// along with a function that effectively checks whether its argument is
31
-
// an instance of the coerced type. see usage in MakeCoercible.liftForeign
31
+
// an instance of the coerced type. see usage in MakeCoercible.liftHValue
32
32
type rec coercion<_> =
33
-
Coercion({tagEq: 'c. typeTag<'c> => option<eq<'a, 'c>>, coerce: 'a => option<'b>}): coercion<'b>
33
+
Coercion({tagEq: 'c. atomTag<'c> => option<eq<'a, 'c>>, coerce: 'a => option<'b>}): coercion<'b>
34
34
module MakeCoercible = (
35
35
Atom: ATOM,
36
36
Coercions: {
···
38
38
},
39
39
): (COERCIBLE_ATOM with type t = Atom.t) => {
40
40
include Atom
41
-
let liftForeign = (ExistsValue(tag, val)) =>
41
+
let liftHValue = (HValue(tag, val)) =>
42
42
Array.findMap(Coercions.coercions, (Coercion(c)) =>
43
43
switch c.tagEq(tag) {
44
44
| Some(Refl) => c.coerce(val)
45
45
| None => None
46
46
}
47
47
)
48
-
let unwrap = t => ExistsValue(Atom.tag, t)
48
+
let getHValue = t => HValue(Atom.Tag, t)
49
49
}
50
50
51
51
exception MatchCombineAtomBoth
···
59
59
// should not be parsed or otherwise appear organically
60
60
| Both(option<Left.t>, option<Right.t>)
61
61
// likewise, strictly for Atom <-> Atom coercions
62
-
// occurs only when passed from some upper part of the tree
63
-
| Foreign(existsValue)
62
+
// occurs only when passed from some sibling part of the tree
63
+
| Foreign(hValue)
64
64
include COERCIBLE_ATOM with type t = base
65
65
let match: (t, Left.t => 'a, Right.t => 'a) => 'a
66
66
} => {
···
68
68
| Left(Left.t)
69
69
| Right(Right.t)
70
70
| Both(option<Left.t>, option<Right.t>)
71
-
| Foreign(existsValue)
71
+
| Foreign(hValue)
72
72
type t = base
73
73
type subst = Map.t<int, t>
74
74
type gen = ref<int>
75
-
type typeTag<_> += Tag: typeTag<t>
76
-
let tag = Tag
77
-
let tagEq = (type a, tag: typeTag<a>): option<eq<t, a>> =>
75
+
type atomTag<_> += Tag: atomTag<t>
76
+
let tagEq = (type a, tag: atomTag<a>): option<eq<t, a>> =>
78
77
switch tag {
79
78
| Tag => Some(Refl)
80
79
| _ => None
81
80
}
82
-
let liftForeign = v => Some(Foreign(v))
81
+
let liftHValue = v => Some(Foreign(v))
83
82
let match = (t, leftBranch: Left.t => 'a, rightBranch: Right.t => 'a): 'a =>
84
83
switch t {
85
84
| Left(s) => leftBranch(s)
···
87
86
| Both(_) => throw(MatchCombineAtomBoth)
88
87
| Foreign(_) => throw(MatchCombineAtomForeign)
89
88
}
90
-
let unwrap = t => t->match(Left.unwrap, Right.unwrap)
89
+
let getHValue = t => t->match(Left.getHValue, Right.getHValue)
91
90
let parse = (s, ~scope, ~gen: option<gen>=?) => {
92
91
Left.parse(s, ~scope, ~gen?)
93
92
->Result.map(((r, rest)) => (Left(r), rest))
···
109
108
switch t {
110
109
| Left(s) => Some(s)
111
110
| Both(os, _) => os
112
-
| Right(s) => s->Right.unwrap->Left.liftForeign
113
-
| Foreign(v) => Left.liftForeign(v)
111
+
| Right(s) => s->Right.getHValue->Left.liftHValue
112
+
| Foreign(v) => Left.liftHValue(v)
114
113
}
115
114
let coerceToRight = (t): option<Right.t> =>
116
115
switch t {
117
116
| Right(s) => Some(s)
118
117
| Both(_, os) => os
119
-
| Left(s) => s->Left.unwrap->Right.liftForeign
120
-
| Foreign(v) => Right.liftForeign(v)
118
+
| Left(s) => s->Left.getHValue->Right.liftHValue
119
+
| Foreign(v) => Right.liftHValue(v)
121
120
}
122
121
let substitute = (s, subst: subst) => {
123
122
s->match(
+3
-6
src/StringA.res
+3
-6
src/StringA.res
···
15
15
open AtomDef
16
16
type t = t
17
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>> =>
18
+
type atomTag<_> += Tag: atomTag<t>
19
+
let tagEq = (type a, tag: atomTag<a>): option<eq<t, a>> =>
21
20
switch tag {
22
21
| Tag => Some(Refl)
23
22
| _ => None
···
290
289
switch Option.getUnsafe(substs[var - from]) {
291
290
| Some(v) => v
292
291
| None =>
293
-
throw(
294
-
SExp.SubstNotCompatible(`index ${Int.toString(var - from)} not of sort string`),
295
-
)
292
+
throw(SExp.SubstNotCompatible(`index ${Int.toString(var - from)} not of sort string`))
296
293
}
297
294
} else {
298
295
[Var({idx: var - to})]
+2
-3
src/Symbolic.res
+2
-3
src/Symbolic.res
···
3
3
open AtomDef
4
4
type t = string
5
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>> =>
6
+
type atomTag<_> += Tag: atomTag<t>
7
+
let tagEq = (type a, tag: atomTag<a>): option<eq<t, a>> =>
9
8
switch tag {
10
9
| Tag => Some(Refl)
11
10
| _ => None