the next generation of the in-browser educational proof assistant
convert SExp lowerings to coercions
+27
-29
+11
-16
src/AtomDef.res
+11
-16
src/AtomDef.res
···
12
12
let parse: (string, ~scope: array<string>, ~gen: ref<int>=?) => result<(t, string), string>
13
13
let substitute: (t, subst) => t
14
14
let upshift: (t, int, ~from: int=?) => t
15
-
// used for when trying to substitute a variable of the wrong type
16
-
let lowerVar: int => option<t>
17
-
let lowerSchematic: (int, array<int>) => option<t>
18
15
let substDeBruijn: (t, array<option<t>>, ~from: int=?) => t
19
16
let concrete: t => bool
20
17
}
···
25
22
let liftHValue: hValue => option<t>
26
23
let getHValue: t => hValue
27
24
}
25
+
26
+
type loweredSExp = Var({idx: int}) | Schematic({schematic: int, allowed: array<int>})
27
+
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
+
}
28
33
29
34
// coercion<t> represents a coercion from some type 'a to t,
30
35
// along with a function that effectively checks whether its argument is
···
55
60
type rec base =
56
61
| Left(Left.t)
57
62
| Right(Right.t)
58
-
// used strictly for SExp -> Atom coercions
59
-
// should not be parsed or otherwise appear organically
60
-
| Both(option<Left.t>, option<Right.t>)
61
-
// likewise, strictly for Atom <-> Atom coercions
62
-
// occurs only when passed from some sibling part of the tree
63
+
// strictly for coercions
64
+
// occurs when passed from some relative in the tree
65
+
// or when SExp values are lowered into loweredSExp
63
66
| Foreign(hValue)
64
67
include COERCIBLE_ATOM with type t = base
65
68
let match: (t, Left.t => 'a, Right.t => 'a) => 'a
···
67
70
type rec base =
68
71
| Left(Left.t)
69
72
| Right(Right.t)
70
-
| Both(option<Left.t>, option<Right.t>)
71
73
| Foreign(hValue)
72
74
type t = base
73
75
type subst = Map.t<int, t>
···
83
85
switch t {
84
86
| Left(s) => leftBranch(s)
85
87
| Right(s) => rightBranch(s)
86
-
| Both(_) => throw(MatchCombineAtomBoth)
87
88
| Foreign(_) => throw(MatchCombineAtomForeign)
88
89
}
89
90
let getHValue = t => t->match(Left.getHValue, Right.getHValue)
···
107
108
let coerceToLeft = (t): option<Left.t> =>
108
109
switch t {
109
110
| Left(s) => Some(s)
110
-
| Both(os, _) => os
111
111
| Right(s) => s->Right.getHValue->Left.liftHValue
112
112
| Foreign(v) => Left.liftHValue(v)
113
113
}
114
114
let coerceToRight = (t): option<Right.t> =>
115
115
switch t {
116
116
| Right(s) => Some(s)
117
-
| Both(_, os) => os
118
117
| Left(s) => s->Left.getHValue->Right.liftHValue
119
118
| Foreign(v) => Right.liftHValue(v)
120
119
}
···
135
134
left => Left(left->Left.upshift(amount, ~from?)),
136
135
right => Right(right->Right.upshift(amount, ~from?)),
137
136
)
138
-
let lowerVar = idx => Some(Both(Left.lowerVar(idx), Right.lowerVar(idx)))
139
-
let lowerSchematic = (schematic, allowed) => Some(
140
-
Both(Left.lowerSchematic(schematic, allowed), Right.lowerSchematic(schematic, allowed)),
141
-
)
142
137
let substDeBruijn = (s, substs: array<option<t>>, ~from=?) =>
143
138
s->match(
144
139
left => {
+8
src/Coercible.res
+8
src/Coercible.res
···
8
8
tagEq: Symbolic.Atom.tagEq,
9
9
coerce: s => Some([StringA.String(s)]),
10
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
+
}),
11
19
]
12
20
},
13
21
)
+4
-3
src/SExp.res
+4
-3
src/SExp.res
···
7
7
let cmp = Pervasives.compare
8
8
})
9
9
10
-
module Make = (Atom: ATOM): {
10
+
module Make = (Atom: AtomDef.COERCIBLE_ATOM): {
11
11
type rec t =
12
12
| Atom(Atom.t)
13
13
| Compound({subexps: array<t>})
···
150
150
let rec lower = (term: t): option<Atom.t> =>
151
151
switch term {
152
152
| Atom(s) => Some(s)
153
-
| Var({idx}) => Atom.lowerVar(idx)
154
-
| Schematic({schematic, allowed}) => Atom.lowerSchematic(schematic, allowed)
153
+
| Var({idx}) => Atom.liftHValue(HValue(AtomDef.SExpTag, AtomDef.Var({idx: idx})))
154
+
| Schematic({schematic, allowed}) =>
155
+
Atom.liftHValue(HValue(AtomDef.SExpTag, AtomDef.Schematic({schematic, allowed})))
155
156
| Compound({subexps: [e1]}) => lower(e1)
156
157
| _ => None
157
158
}
+1
-1
src/SExpView.res
+1
-1
src/SExpView.res
+2
-6
src/StringA.res
+2
-6
src/StringA.res
···
12
12
type schematic = int
13
13
14
14
module Atom = {
15
-
open AtomDef
16
15
type t = t
17
16
type subst = Map.t<schematic, t>
18
-
type atomTag<_> += Tag: atomTag<t>
19
-
let tagEq = (type a, tag: atomTag<a>): option<eq<t, a>> =>
17
+
type AtomDef.atomTag<_> += Tag: AtomDef.atomTag<t>
18
+
let tagEq = (type a, tag: AtomDef.atomTag<a>): option<AtomDef.eq<t, a>> =>
20
19
switch tag {
21
20
| Tag => Some(Refl)
22
21
| _ => None
···
461
460
462
461
acc.contents->Result.map(r => (r, str->String.sliceToEnd(~start=pos.contents)))
463
462
}
464
-
465
-
let lowerSchematic = (schematic, allowed) => Some([Schematic({schematic, allowed})])
466
-
let lowerVar = idx => Some([Var({idx: idx})])
467
463
let concrete = t =>
468
464
t->Array.every(p =>
469
465
switch p {
-2
src/Symbolic.res
-2
src/Symbolic.res
···
23
23
| _ => Error("constant symbol parse error")
24
24
}
25
25
let substitute = (name, _) => name
26
-
let lowerVar = _ => None
27
-
let lowerSchematic = (_, _) => None
28
26
let substDeBruijn = (name, _, ~from as _=?) => name
29
27
let concrete = _ => false
30
28
let upshift = (t, _, ~from as _=?) => t