the next generation of the in-browser educational proof assistant
adjust atom substDeBruijn sig
+22
-26
+4
-10
src/SExpFunc.res
+4
-10
src/SExpFunc.res
···
1
+
exception SubstNotCompatible(string)
2
+
1
3
module type ATOM = {
2
4
type t
3
5
type subst = Map.t<int, t>
···
9
11
// used for when trying to substitute a variable of the wrong type
10
12
let lowerVar: int => option<t>
11
13
let lowerSchematic: (int, array<int>) => option<t>
12
-
let substDeBruijn: (t, Map.t<int, t>, ~from: int=?, ~to: int) => t
14
+
let substDeBruijn: (t, array<option<t>>, ~from: int=?) => t
13
15
let concrete: t => bool
14
16
}
15
17
···
160
162
}
161
163
let rec substDeBruijn = (term: t, substs: array<t>, ~from: int=0) =>
162
164
switch term {
163
-
| Atom(s) => {
164
-
let symbolSubsts =
165
-
substs
166
-
->Array.mapWithIndex((t, i) => lower(t)->Option.map(a => (i, a)))
167
-
->Array.keepSome
168
-
->Map.fromArray
169
-
170
-
Atom(Atom.substDeBruijn(s, symbolSubsts, ~from, ~to=Array.length(substs)))
171
-
}
165
+
| Atom(s) => Atom(Atom.substDeBruijn(s, Array.map(substs, lower), ~from))
172
166
173
167
| Compound({subexps}) =>
174
168
Compound({subexps: Array.map(subexps, x => substDeBruijn(x, substs, ~from))})
+9
-2
src/StringA.res
+9
-2
src/StringA.res
···
270
270
}
271
271
272
272
// law: unify(a,b) == [{}] iff equivalent(a,b)
273
-
let substDeBruijn = (string: t, substs: Map.t<int, t>, ~from: int=0, ~to: int) => {
273
+
let substDeBruijn = (string: t, substs: array<option<t>>, ~from: int=0) => {
274
+
let to = Array.length(substs)
274
275
Array.flatMap(string, piece =>
275
276
switch piece {
276
277
| String(_) => [piece]
···
278
279
if var < from {
279
280
[piece]
280
281
} else if var - from < to {
281
-
Map.get(substs, var - from)->Option.getOr([piece])
282
+
switch Option.getUnsafe(substs[var - from]) {
283
+
| Some(v) => v
284
+
| None =>
285
+
throw(
286
+
SExpFunc.SubstNotCompatible(`index ${Int.toString(var - from)} not of sort string`),
287
+
)
288
+
}
282
289
} else {
283
290
[Var({idx: var - to})]
284
291
}
+8
-13
src/StringSymbol.res
+8
-13
src/StringSymbol.res
···
51
51
let lowerSchematic = (schematic, allowed) => Some(
52
52
StringS([StringA.Schematic({schematic, allowed})]),
53
53
)
54
-
let substDeBruijn = (s, substs: Map.t<int, t>, ~from=?, ~to: int) =>
54
+
let substDeBruijn = (s, substs: array<option<t>>, ~from=?) =>
55
55
switch s {
56
56
| StringS(s) => {
57
-
let stringSubs =
58
-
substs
59
-
->Map.entries
60
-
->Iterator.toArrayWithMapper(((i, v)) =>
61
-
switch v {
62
-
| StringS(s) => Some((i, s))
63
-
| _ => None
64
-
}
65
-
)
66
-
->Array.keepSome
67
-
->Map.fromArray
68
-
StringS(StringA.Atom.substDeBruijn(s, stringSubs, ~from?, ~to))
57
+
let stringSubs = substs->Array.map(s =>
58
+
switch s {
59
+
| Some(StringS(s)) => Some(s)
60
+
| _ => None
61
+
}
62
+
)
63
+
StringS(StringA.Atom.substDeBruijn(s, stringSubs, ~from?))
69
64
}
70
65
| ConstS(s) => ConstS(s)
71
66
}
+1
-1
src/Symbolic.res
+1
-1
src/Symbolic.res
···
18
18
let substitute = (name, _) => name
19
19
let lowerVar = _ => None
20
20
let lowerSchematic = (_, _) => None
21
-
let substDeBruijn = (name, _, ~from as _=?, ~to as _) => name
21
+
let substDeBruijn = (name, _, ~from as _=?) => name
22
22
let concrete = _ => false
23
23
let upshift = (t, _, ~from as _=?) => t
24
24
}