the next generation of the in-browser educational proof assistant
clean ATOM/BASE_ATOM signature
Before, we had this ATOM/COERCIBLE_ATOM split to solve circular
references, where COERCIBLE_ATOM was a thin wrapper around ATOM to
introduce coercions. The idea was that one might want to opt-out
entirely from the coercion system and which requires having a complete ATOM
definition without any of the extra stuff that coercions introduce. In
practice, that idea was already very leaky, with hard-coded requirements
that atoms be coercible already in place that would be hard to remove.
And besides, one can always opt out of coercions on their own types by
declaring `coerce = _ => None`, and on some predefined type by writing a
wrapper with such a definition.
This change flips the previous architecture so that the full ATOM
signature includes coercions and a thin BASE_ATOM module which includes a type definition,
a tag, and a way to wrap a value into an `anyValue`
(also, I renamed `hValue` to `anyValue` for clarity).
This should be the last substantial change to the signature of ATOM.
authored by
Josh Brown
and committed by
Tangled
3974f644
0d7282eb
+70
-56
+32
-16
src/AtomDef.res
+32
-16
src/AtomDef.res
···
1
1
// type level stuff to enable well-typed coercions
2
2
type atomTag<_> = ..
3
+
type rec hValue = HValue(atomTag<'a>, 'a): hValue
3
4
4
-
module type ATOM = {
5
+
// to allow circular coercions, we declare base types
6
+
// separately from relevant implementation
7
+
module type BASE_ATOM = {
5
8
type t
6
-
type subst = Map.t<int, t>
7
9
type atomTag<_> += Tag: atomTag<t>
10
+
let wrap: t => hValue
11
+
}
12
+
13
+
module MakeBaseAtom = (
14
+
T: {
15
+
type t
16
+
},
17
+
): (BASE_ATOM with type t = T.t) => {
18
+
type t = T.t
19
+
type atomTag<_> += Tag: atomTag<t>
20
+
let wrap = t => HValue(Tag, t)
21
+
}
22
+
23
+
module type ATOM = {
24
+
module BaseAtom: BASE_ATOM
25
+
type t = BaseAtom.t
26
+
type subst = Map.t<int, t>
8
27
let unify: (t, t, ~gen: ref<int>=?) => Seq.t<subst>
9
28
let prettyPrint: (t, ~scope: array<string>) => string
10
29
let parse: (string, ~scope: array<string>, ~gen: ref<int>=?) => result<(t, string), string>
···
12
31
let upshift: (t, int, ~from: int=?) => t
13
32
let substDeBruijn: (t, array<option<t>>, ~from: int=?) => t
14
33
let concrete: t => bool
15
-
}
16
-
17
-
type rec hValue = HValue(atomTag<'a>, 'a): hValue
18
-
module type COERCIBLE_ATOM = {
19
-
include ATOM
20
34
let coerce: hValue => option<t>
21
35
let wrap: t => hValue
22
36
}
···
26
40
27
41
exception MatchCombineAtomForeign
28
42
29
-
module CombineAtom = (Left: COERCIBLE_ATOM, Right: COERCIBLE_ATOM): {
30
-
type rec base =
43
+
module CombineAtom = (Left: ATOM, Right: ATOM): {
44
+
type base =
31
45
| Left(Left.t)
32
46
| Right(Right.t)
33
47
// strictly for coercions
34
48
// occurs when passed from some relative in the tree
35
49
// or when SExp values are lowered into loweredSExp
36
50
| Foreign(hValue)
37
-
include COERCIBLE_ATOM with type t = base
51
+
include ATOM with type BaseAtom.t = base
38
52
let match: (t, Left.t => 'a, Right.t => 'a) => 'a
39
53
} => {
40
54
type rec base =
41
55
| Left(Left.t)
42
56
| Right(Right.t)
43
57
| Foreign(hValue)
44
-
type t = base
58
+
module BaseAtom = MakeBaseAtom({
59
+
type t = base
60
+
})
61
+
type t = BaseAtom.t
45
62
type subst = Map.t<int, t>
46
63
type gen = ref<int>
47
-
type atomTag<_> += Tag: atomTag<t>
48
64
let coerce = v => Some(Foreign(v))
49
65
let match = (t, leftBranch: Left.t => 'a, rightBranch: Right.t => 'a): 'a =>
50
66
switch t {
···
125
141
}
126
142
127
143
module MakeAtomView = (
128
-
Left: COERCIBLE_ATOM,
144
+
Left: ATOM,
129
145
LeftView: ATOM_VIEW with module Atom := Left,
130
-
Right: COERCIBLE_ATOM,
146
+
Right: ATOM,
131
147
RightView: ATOM_VIEW with module Atom := Right,
132
148
Combined: module type of CombineAtom(Left, Right),
133
149
): {
···
142
158
}
143
159
144
160
module MakeAtomAndView = (
145
-
Left: COERCIBLE_ATOM,
161
+
Left: ATOM,
146
162
LeftView: ATOM_VIEW with module Atom := Left,
147
-
Right: COERCIBLE_ATOM,
163
+
Right: ATOM,
148
164
RightView: ATOM_VIEW with module Atom := Right,
149
165
) => {
150
166
module Atom = CombineAtom(Left, Right)
-24
src/Coercible.res
-24
src/Coercible.res
···
1
-
open AtomDef
2
-
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
-
let wrap = a => HValue(StringA.Atom.Tag, a)
18
-
}
19
-
20
-
module Symbolic: COERCIBLE_ATOM with type t = Symbolic.Atom.t = {
21
-
include Symbolic.Atom
22
-
let coerce = _ => None
23
-
let wrap = a => HValue(Symbolic.Atom.Tag, a)
24
-
}
+1
-1
src/SExp.res
+1
-1
src/SExp.res
+1
-1
src/SExpView.res
+1
-1
src/SExpView.res
+2
-2
src/Scratch.res
+2
-2
src/Scratch.res
···
43
43
module ConfS = ConfigBlock.Make(HOTerm, HOTerm)
44
44
45
45
module StringSymbol = AtomDef.MakeAtomAndView(
46
-
Coercible.StringA,
46
+
StringA.Atom,
47
47
StringA.AtomView,
48
-
Coercible.Symbolic,
48
+
Symbolic.Atom,
49
49
Symbolic.AtomView,
50
50
)
51
51
module StringSExp = SExp.Make(StringSymbol.Atom)
+18
-1
src/StringA.res
+18
-1
src/StringA.res
···
11
11
type meta = string
12
12
type schematic = int
13
13
14
+
module BaseAtom = AtomDef.MakeBaseAtom({
15
+
type t = t
16
+
})
17
+
14
18
module Atom = {
19
+
module BaseAtom = BaseAtom
15
20
type t = t
16
21
type subst = Map.t<schematic, t>
17
-
type AtomDef.atomTag<_> += Tag: AtomDef.atomTag<t>
18
22
let substitute = (term: t, subst: subst) =>
19
23
Array.flatMap(term, piece => {
20
24
switch piece {
···
462
466
| _ => false
463
467
}
464
468
)
469
+
let coerce = (AtomDef.HValue(tag, a)) =>
470
+
switch tag {
471
+
| Symbolic.BaseAtom.Tag => Some([String(a)])
472
+
| AtomDef.SExpTag =>
473
+
Some([
474
+
switch a {
475
+
| Var({idx}) => Var({idx: idx})
476
+
| Schematic({schematic, allowed}) => Schematic({schematic, allowed})
477
+
},
478
+
])
479
+
| _ => None
480
+
}
481
+
let wrap = a => AtomDef.HValue(BaseAtom.Tag, a)
465
482
}
466
483
467
484
module AtomView = {
+2
-1
src/StringA.resi
+2
-1
src/StringA.resi
···
4
4
| Schematic({schematic: int, allowed: array<int>})
5
5
type t = array<piece>
6
6
7
-
module Atom: AtomDef.ATOM with type t = t
7
+
module BaseAtom: AtomDef.BASE_ATOM with type t = t
8
+
module Atom: AtomDef.ATOM with module BaseAtom = BaseAtom
8
9
module AtomView: AtomDef.ATOM_VIEW with module Atom := Atom
+2
-2
src/StringAxiomSet.res
+2
-2
src/StringAxiomSet.res
+7
-3
src/Symbolic.res
+7
-3
src/Symbolic.res
···
1
-
type t = string
1
+
module BaseAtom = AtomDef.MakeBaseAtom({
2
+
type t = string
3
+
})
4
+
2
5
module Atom = {
3
-
open AtomDef
6
+
module BaseAtom = BaseAtom
4
7
type t = string
5
8
type subst = Map.t<int, string>
6
-
type atomTag<_> += Tag: atomTag<t>
7
9
let unify = (a, b, ~gen as _=?) =>
8
10
if a == b {
9
11
Seq.once(Map.make())
···
21
23
let substDeBruijn = (name, _, ~from as _=?) => name
22
24
let concrete = _ => false
23
25
let upshift = (t, _, ~from as _=?) => t
26
+
let coerce = _ => None
27
+
let wrap = a => AtomDef.HValue(BaseAtom.Tag, a)
24
28
}
25
29
26
30
module AtomView = {
+2
-2
src/Symbolic.resi
+2
-2
src/Symbolic.resi
+2
-2
tests/RuleTest.res
+2
-2
tests/RuleTest.res
···
33
33
34
34
zoraBlock("string terms", t => {
35
35
module StringSymbol = AtomDef.MakeAtomAndView(
36
-
Coercible.StringA,
36
+
StringA.Atom,
37
37
StringA.AtomView,
38
-
Coercible.Symbolic,
38
+
Symbolic.Atom,
39
39
Symbolic.AtomView,
40
40
)
41
41
module StringSExp = SExp.Make(StringSymbol.Atom)