the next generation of the in-browser educational proof assistant
remove ghost, tidy
+12
-74
-1
src/HOTerm.res
-1
src/HOTerm.res
-1
src/SExp.res
-1
src/SExp.res
-7
src/SExpFunc.res
-7
src/SExpFunc.res
···
9
9
// used for when trying to substitute a variable of the wrong type
10
10
let lowerVar: int => option<t>
11
11
let lowerSchematic: (int, array<int>) => option<t>
12
-
let ghost: t
13
12
let substDeBruijn: (t, Map.t<int, t>, ~from: int=?, ~to: int) => t
14
13
let concrete: t => bool
15
14
}
···
25
24
| Compound({subexps: array<t>})
26
25
| Var({idx: int})
27
26
| Schematic({schematic: int, allowed: array<int>})
28
-
| Ghost
29
27
30
28
include Signatures.TERM
31
29
with type t := t
···
39
37
| Compound({subexps: array<t>})
40
38
| Var({idx: int})
41
39
| Schematic({schematic: int, allowed: array<int>})
42
-
| Ghost
43
40
module Atom = Atom
44
41
type meta = string
45
42
type schematic = int
···
194
191
}
195
192
),
196
193
})
197
-
| Ghost => Ghost
198
194
}
199
195
let rec upshift = (term: t, amount: int, ~from: int=0) =>
200
196
switch term {
···
219
215
}
220
216
),
221
217
})
222
-
| Ghost => Ghost
223
218
}
224
219
let place = (x: int, ~scope: array<string>) => Schematic({
225
220
schematic: x,
···
261
256
"("
262
257
->String.concat(Array.join(subexps->Array.map(e => prettyPrint(e, ~scope)), " "))
263
258
->String.concat(")")
264
-
| Ghost => "§SExp.Ghost"
265
259
}
266
260
267
261
let prettyPrintSubst = (sub, ~scope) =>
···
430
424
}
431
425
}
432
426
433
-
let ghostTerm = Ghost
434
427
let rec concrete = t =>
435
428
switch t {
436
429
| Schematic(_) => true
-1
src/SExpViewFunc.res
-1
src/SExpViewFunc.res
-2
src/Signatures.res
-2
src/Signatures.res
···
24
24
let parseMeta: string => result<(meta, string), string>
25
25
let prettyPrint: (t, ~scope: array<meta>) => string
26
26
let prettyPrintMeta: meta => string
27
-
let ghostTerm: t
28
27
let concrete: t => bool
29
28
}
30
29
···
41
40
let mapTerms: (t, Term.t => Term.t) => t
42
41
let parse: (string, ~scope: array<Term.meta>, ~gen: Term.gen=?) => result<(t, string), string>
43
42
let prettyPrint: (t, ~scope: array<Term.meta>) => string
44
-
let ghostTerm: t
45
43
// will unifying t with a term give meaningful substitutions?
46
44
let concrete: t => bool
47
45
}
+1
-44
src/StringAtom.res
+1
-44
src/StringAtom.res
···
7
7
| String(string)
8
8
| Var({idx: int})
9
9
| Schematic({schematic: int, allowed: array<int>})
10
-
| Ghost
11
10
type t = array<piece>
12
11
type meta = string
13
12
type schematic = int
14
13
type subst = Map.t<schematic, t>
15
-
let mapSubst = Util.mapMapValues
16
-
let substEqual = Util.mapEqual
17
-
let makeSubst = () => Map.make()
18
-
let mergeSubsts = Util.mapUnion
19
14
20
15
let substitute = (term: t, subst: subst) =>
21
16
Array.flatMap(term, piece => {
···
43
38
let maxSchematicCount = (term: t) => {
44
39
schematicsCountsIn(term)->Belt.Map.Int.maximum->Option.map(Pair.second)->Option.getOr(0)
45
40
}
46
-
let reduce = t => t
47
41
let freeVarsIn = (term: t): Belt.Set.t<int, IntCmp.identity> =>
48
42
Array.map(term, piece => {
49
43
switch piece {
···
177
171
| None => searchSub(schematic, allowed, Eps)
178
172
| Some(p) =>
179
173
switch p {
180
-
| String(_) | Ghost =>
174
+
| String(_) =>
181
175
Array.concat(
182
176
searchSub(schematic, allowed, PieceLitSub(p)),
183
177
searchSub(schematic, allowed, Eps),
···
298
292
),
299
293
}),
300
294
]
301
-
| Ghost => [Ghost]
302
295
}
303
296
)
304
297
}
···
326
319
}
327
320
),
328
321
})
329
-
| Ghost => Ghost
330
322
}
331
323
})
332
324
333
-
let place = (x: int, ~scope: array<string>) => [
334
-
Schematic({
335
-
schematic: x,
336
-
allowed: Array.fromInitializer(~length=Array.length(scope), i => i),
337
-
}),
338
-
]
339
-
340
325
type gen = ref<int>
341
-
let seen = (g: gen, s: int) => {
342
-
if s >= g.contents {
343
-
g := s + 1
344
-
}
345
-
}
346
-
let fresh = (g: gen, ~replacing as _=?) => {
347
-
let v = g.contents
348
-
g := g.contents + 1
349
-
v
350
-
}
351
-
let makeGen = () => {
352
-
ref(0)
353
-
}
354
326
355
-
let parseMeta = (str: string) => {
356
-
let re = /^([^\s.\[\]()]+)\./y
357
-
switch re->RegExp.exec(str->String.trim) {
358
-
| None => Error("not a meta name")
359
-
| Some(res) =>
360
-
switch RegExp.Result.matches(res) {
361
-
| [n] => Ok(n, String.sliceToEnd(str->String.trim, ~start=RegExp.lastIndex(re)))
362
-
| _ => Error("impossible happened")
363
-
}
364
-
}
365
-
}
366
327
let prettyPrintVar = (idx: int, scope: array<string>) =>
367
328
"$" ++
368
329
switch scope[idx] {
···
381
342
->Array.join(" ")
382
343
`?${Int.toString(schematic)}(${allowedStr})`
383
344
}
384
-
| Ghost => "§String.Ghost"
385
345
}
386
346
})->Array.join(" ")}"`
387
-
let prettyPrintMeta = (str: string) => `${str}.`
388
-
let prettyPrintSubst = (sub, ~scope) => Util.prettyPrintMap(sub, ~showV=t => prettyPrint(t, ~scope))
389
347
390
348
type remaining = string
391
349
type errorMessage = string
···
504
462
505
463
let lowerSchematic = (schematic, allowed) => Some([Schematic({schematic, allowed})])
506
464
let lowerVar = idx => Some([Var({idx: idx})])
507
-
let ghost = [Ghost]
508
465
let concrete = t =>
509
466
t->Array.every(p =>
510
467
switch p {
-1
src/StringAtom.resi
-1
src/StringAtom.resi
-1
src/StringAtomView.res
-1
src/StringAtomView.res
+11
-7
src/StringSExp.res
+11
-7
src/StringSExp.res
···
29
29
let substitute = (s, subst: subst) =>
30
30
switch s {
31
31
| StringS(s) => {
32
-
let stringSubs = subst->Util.mapMapValues(v =>
33
-
switch v {
34
-
| StringS(s) => s
35
-
| _ => [StringAtom.Ghost]
36
-
}
37
-
)
32
+
let stringSubs =
33
+
subst
34
+
->Map.entries
35
+
->Iterator.toArrayWithMapper(((i, v)) =>
36
+
switch v {
37
+
| StringS(s) => Some((i, s))
38
+
| _ => None
39
+
}
40
+
)
41
+
->Array.keepSome
42
+
->Map.fromArray
38
43
StringS(StringAtom.substitute(s, stringSubs))
39
44
}
40
45
| ConstS(s) => ConstS(s)
···
48
53
let lowerSchematic = (schematic, allowed) => Some(
49
54
StringS([StringAtom.Schematic({schematic, allowed})]),
50
55
)
51
-
let ghost = StringS([StringAtom.Ghost])
52
56
let substDeBruijn = (s, substs: Map.t<int, t>, ~from=?, ~to: int) =>
53
57
switch s {
54
58
| StringS(s) => {
-4
tests/SExpTest.res
-4
tests/SExpTest.res
-5
tests/StringTermTest.res
-5
tests/StringTermTest.res
···
50
50
let b = parse(`"b"`)
51
51
let x = parse(`"?1()"`)
52
52
let y = parse(`"?2()"`)
53
-
t->block("ghost", t => {
54
-
t->UnifyUtil.testUnifyFail(a, StringAtom.ghost)
55
-
t->UnifyUtil.testUnify(x, StringAtom.ghost)
56
-
t->UnifyUtil.testUnify([x, y, x]->Array.flat, StringAtom.ghost)
57
-
})
58
53
t->block("schematics on at most one side", t => {
59
54
t->UnifyUtil.testUnify(a, a, ~expect=[Map.make()])
60
55
t->UnifyUtil.testUnify(x, a, ~expect=[Map.fromArray([(1, a)])])