the next generation of the in-browser educational proof assistant
remove (some of) atom debjruijn sub partiality
+41
-30
+3
-3
src/SExp.res
+3
-3
src/SExp.res
···
15
15
| _ => Error("constant symbol parse error")
16
16
}
17
17
let substitute = (name, _) => name
18
-
let lowerVar = _ => ""
19
-
let lowerSchematic = (_, _) => ""
18
+
let lowerVar = _ => None
19
+
let lowerSchematic = (_, _) => None
20
20
let ghost = ""
21
-
let substDeBruijn = (name, _, ~from as _=?) => name
21
+
let substDeBruijn = (name, _, ~from as _=?, ~to as _) => name
22
22
let unifiesWithAnything = _ => false
23
23
let upshift = (t, _, ~from as _=?) => t
24
24
}
+13
-8
src/SExpFunc.res
+13
-8
src/SExpFunc.res
···
7
7
let substitute: (t, subst) => t
8
8
let upshift: (t, int, ~from: int=?) => t
9
9
// used for when trying to substitute a variable of the wrong type
10
-
let lowerVar: int => t
11
-
let lowerSchematic: (int, array<int>) => t
10
+
let lowerVar: int => option<t>
11
+
let lowerSchematic: (int, array<int>) => option<t>
12
12
let ghost: t
13
-
let substDeBruijn: (t, array<t>, ~from: int=?) => t
13
+
let substDeBruijn: (t, Map.t<int, t>, ~from: int=?, ~to: int) => t
14
14
let unifiesWithAnything: t => bool
15
15
}
16
16
···
155
155
}
156
156
let unify = (a: t, b: t, ~gen as _=?) => unifyTerm(a, b)
157
157
158
-
let rec lower = (term: t): Atom.t =>
158
+
let rec lower = (term: t): option<Atom.t> =>
159
159
switch term {
160
-
| Atom(s) => s
160
+
| Atom(s) => Some(s)
161
161
| Var({idx}) => Atom.lowerVar(idx)
162
162
| Schematic({schematic, allowed}) => Atom.lowerSchematic(schematic, allowed)
163
163
| Compound({subexps: [e1]}) => lower(e1)
164
-
| _ => Atom.ghost
164
+
| _ => None
165
165
}
166
166
let rec substDeBruijn = (term: t, substs: array<t>, ~from: int=0) =>
167
167
switch term {
168
168
| Atom(s) => {
169
-
let symbolSubsts = substs->Array.map(lower)
170
-
Atom(Atom.substDeBruijn(s, symbolSubsts, ~from))
169
+
let symbolSubsts =
170
+
substs
171
+
->Array.mapWithIndex((t, i) => lower(t)->Option.map(a => (i, a)))
172
+
->Array.keepSome
173
+
->Map.fromArray
174
+
175
+
Atom(Atom.substDeBruijn(s, symbolSubsts, ~from, ~to=Array.length(substs)))
171
176
}
172
177
173
178
| Compound({subexps}) =>
+8
-9
src/StringAtom.res
+8
-9
src/StringAtom.res
···
274
274
}
275
275
276
276
// law: unify(a,b) == [{}] iff equivalent(a,b)
277
-
let equivalent: (t, t) => bool = (s, t) => s == t
278
-
let substDeBruijn = (string: t, substs: array<t>, ~from: int=0) => {
277
+
let substDeBruijn = (string: t, substs: Map.t<int, t>, ~from: int=0, ~to: int) => {
279
278
Array.flatMap(string, piece =>
280
279
switch piece {
281
280
| String(_) => [piece]
282
281
| Var({idx: var}) =>
283
282
if var < from {
284
283
[piece]
285
-
} else if var - from < Array.length(substs) && var - from >= 0 {
286
-
Option.getUnsafe(substs[var - from])
284
+
} else if var - from < to {
285
+
Map.get(substs, var - from)->Option.getOr([piece])
287
286
} else {
288
-
[Var({idx: var - Array.length(substs)})]
287
+
[Var({idx: var - to})]
289
288
}
290
289
| Schematic({schematic, allowed}) => [
291
290
Schematic({
292
291
schematic,
293
292
allowed: Array.filterMap(allowed, i =>
294
-
if i < from + Array.length(substs) {
293
+
if i < from + to {
295
294
None
296
295
} else {
297
-
Some(i - (from + Array.length(substs)))
296
+
Some(i - (from + to))
298
297
}
299
298
),
300
299
}),
···
503
502
acc.contents->Result.map(r => (r, str->String.sliceToEnd(~start=pos.contents)))
504
503
}
505
504
506
-
let lowerSchematic = (schematic, allowed) => [Schematic({schematic, allowed})]
507
-
let lowerVar = idx => [Var({idx: idx})]
505
+
let lowerSchematic = (schematic, allowed) => Some([Schematic({schematic, allowed})])
506
+
let lowerVar = idx => Some([Var({idx: idx})])
508
507
let ghost = [Ghost]
509
508
let unifiesWithAnything = t =>
510
509
t->Array.every(p =>
+17
-10
src/StringSExp.res
+17
-10
src/StringSExp.res
···
42
42
| StringS(s) => StringS(s->StringAtom.upshift(amount, ~from?))
43
43
| ConstS(s) => ConstS(s)
44
44
}
45
-
let lowerVar = idx => StringS([StringAtom.Var({idx: idx})])
46
-
let lowerSchematic = (schematic, allowed) => StringS([StringAtom.Schematic({schematic, allowed})])
45
+
let lowerVar = idx => Some(StringS([StringAtom.Var({idx: idx})]))
46
+
let lowerSchematic = (schematic, allowed) => Some(
47
+
StringS([StringAtom.Schematic({schematic, allowed})]),
48
+
)
47
49
let ghost = StringS([StringAtom.Ghost])
48
-
let substDeBruijn = (s, substs: array<t>, ~from=?) =>
50
+
let substDeBruijn = (s, substs: Map.t<int, t>, ~from=?, ~to: int) =>
49
51
switch s {
50
52
| StringS(s) => {
51
-
let stringSubs = substs->Array.map(v =>
52
-
switch v {
53
-
| StringS(s) => s
54
-
| _ => [StringAtom.String("AYAYAYSLKDJFLSKDJ")]
55
-
}
56
-
)
57
-
StringS(StringAtom.substDeBruijn(s, stringSubs, ~from?))
53
+
let stringSubs =
54
+
substs
55
+
->Map.entries
56
+
->Iterator.toArrayWithMapper(((i, v)) =>
57
+
switch v {
58
+
| StringS(s) => Some((i, s))
59
+
| _ => None
60
+
}
61
+
)
62
+
->Array.keepSome
63
+
->Map.fromArray
64
+
StringS(StringAtom.substDeBruijn(s, stringSubs, ~from?, ~to))
58
65
}
59
66
| ConstS(s) => ConstS(s)
60
67
}