the next generation of the in-browser educational proof assistant
tidy further
+686
-699
+6
-2
src/SExp.res
src/Symbolic.res
+6
-2
src/SExp.res
src/Symbolic.res
···
1
-
module SymbolAtom: SExpFunc.ATOM with type t = string = {
1
+
type t = string
2
+
module Atom = {
2
3
type t = string
3
4
type subst = Map.t<int, string>
4
5
let unify = (a, b, ~gen as _=?) =>
···
22
23
let upshift = (t, _, ~from as _=?) => t
23
24
}
24
25
25
-
include SExpFunc.Make(SymbolAtom)
26
+
module AtomView = {
27
+
type props = {name: string, scope: array<string>}
28
+
let make = (props: props) => React.string(props.name)
29
+
}
-3
src/SExp.resi
-3
src/SExp.resi
-7
src/SExpJView.res
-7
src/SExpJView.res
-4
src/SExpJView.resi
-4
src/SExpJView.resi
-6
src/SExpView.res
-6
src/SExpView.res
-3
src/SExpView.resi
-3
src/SExpView.resi
+4
src/Scratch.res
+4
src/Scratch.res
···
42
42
module TheoremS = Editable.TextArea(Theorem.Make(HOTerm, HOTerm, HOTermJView, DLRView))
43
43
module ConfS = ConfigBlock.Make(HOTerm, HOTerm)
44
44
45
+
module StringSExp = SExpFunc.Make(StringSymbol.Atom)
46
+
module TermView = SExpViewFunc.Make(StringSymbol.Atom, StringSymbol.AtomView, StringSExp)
47
+
module StringSExpJView = TermViewAsJudgmentView.Make(StringSExp, StringSExp, TermView)
45
48
module AxiomStr = Editable.TextArea(StringAxiomSet)
49
+
46
50
module DerivationsOrLemmasStrView = MethodView.CombineMethodView(
47
51
StringSExp,
48
52
StringSExp,
+1
-1
src/Signatures.res
+1
-1
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
+
// will unifying t with a term give meaningful substitutions?
27
28
let concrete: t => bool
28
29
}
29
30
···
40
41
let mapTerms: (t, Term.t => Term.t) => t
41
42
let parse: (string, ~scope: array<Term.meta>, ~gen: Term.gen=?) => result<(t, string), string>
42
43
let prettyPrint: (t, ~scope: array<Term.meta>) => string
43
-
// will unifying t with a term give meaningful substitutions?
44
44
let concrete: t => bool
45
45
}
46
46
+541
src/StringA.res
+541
src/StringA.res
···
1
+
module IntCmp = Belt.Id.MakeComparable({
2
+
type t = int
3
+
let cmp = Pervasives.compare
4
+
})
5
+
6
+
type piece =
7
+
| String(string)
8
+
| Var({idx: int})
9
+
| Schematic({schematic: int, allowed: array<int>})
10
+
type t = array<piece>
11
+
type meta = string
12
+
type schematic = int
13
+
14
+
module Atom = {
15
+
type t = t
16
+
type subst = Map.t<schematic, t>
17
+
let substitute = (term: t, subst: subst) =>
18
+
Array.flatMap(term, piece => {
19
+
switch piece {
20
+
| Schematic({schematic, _}) =>
21
+
switch Map.get(subst, schematic) {
22
+
| None => [piece]
23
+
| Some(found) => found
24
+
}
25
+
| _ => [piece]
26
+
}
27
+
})
28
+
let schematicsCountsIn: t => Belt.Map.Int.t<int> = (term: t) =>
29
+
Array.reduce(term, Belt.Map.Int.empty, (m, p) =>
30
+
switch p {
31
+
| Schematic({schematic, _}) =>
32
+
m->Belt.Map.Int.update(schematic, o =>
33
+
o
34
+
->Option.map(v => v + 1)
35
+
->Option.orElse(Some(1))
36
+
)
37
+
| _ => m
38
+
}
39
+
)
40
+
let maxSchematicCount = (term: t) => {
41
+
schematicsCountsIn(term)->Belt.Map.Int.maximum->Option.map(Pair.second)->Option.getOr(0)
42
+
}
43
+
let freeVarsIn = (term: t): Belt.Set.t<int, IntCmp.identity> =>
44
+
Array.map(term, piece => {
45
+
switch piece {
46
+
| Var({idx}) => Belt.Set.make(~id=module(IntCmp))->Belt.Set.add(idx)
47
+
| _ => Belt.Set.make(~id=module(IntCmp))
48
+
}
49
+
})->Array.reduce(Belt.Set.make(~id=module(IntCmp)), (s1, s2) => Belt.Set.union(s1, s2))
50
+
51
+
let combineSubst = (s: subst, t: subst) => {
52
+
let nu = Map.make()
53
+
Map.entries(s)->Iterator.forEach(opt =>
54
+
switch opt {
55
+
| None => ()
56
+
| Some((key, term)) => nu->Map.set(key, term->substitute(t))
57
+
}
58
+
)
59
+
Map.entries(t)->Iterator.forEach(opt =>
60
+
switch opt {
61
+
| None => ()
62
+
| Some((key, term)) => nu->Map.set(key, term->substitute(s))
63
+
}
64
+
)
65
+
nu
66
+
}
67
+
68
+
let emptySubst: subst = Map.make()
69
+
let singletonSubst: (int, t) => subst = (schematic, term) => {
70
+
let s = Map.make()
71
+
s->Map.set(schematic, term)
72
+
s
73
+
}
74
+
75
+
let uncons = (xs: array<'a>): ('a, array<'a>) => {
76
+
switch xs {
77
+
| [] => Error("expected nonempty array")->Result.getExn
78
+
| _ => (xs[0]->Option.getExn, Array.sliceToEnd(xs, ~start=1))
79
+
}
80
+
}
81
+
82
+
type graphSub = Eps | PieceLitSub(piece) | SchemaSub(int, array<int>)
83
+
let unify = (s: array<piece>, t: array<piece>, ~gen as _=?): Seq.t<subst> => {
84
+
let match = (p1: piece, p2: piece) => {
85
+
switch (p1, p2) {
86
+
| (String(na), String(nb)) if na == nb => true
87
+
| (Var({idx: ia}), Var({idx: ib})) if ia == ib => true
88
+
| (_, _) => false
89
+
}
90
+
}
91
+
92
+
let rec oneSide = (s, t) => {
93
+
switch (s, t) {
94
+
| ([], []) => [emptySubst]
95
+
| ([], _) => []
96
+
| (_, _) => {
97
+
let (s1, ss) = uncons(s)
98
+
switch s1 {
99
+
| Schematic({schematic, allowed}) =>
100
+
Belt.Array.range(0, Array.length(t))
101
+
->Array.map(i => {
102
+
let subTerm = Array.slice(t, ~start=0, ~end=i)
103
+
let freeVars = freeVarsIn(subTerm)
104
+
let allowedVars = Belt.Set.fromArray(allowed, ~id=module(IntCmp))
105
+
if Belt.Set.subset(freeVars, allowedVars) {
106
+
let s1 = singletonSubst(schematic, subTerm)
107
+
oneSide(
108
+
substitute(ss, s1),
109
+
Array.sliceToEnd(t, ~start=i)->substitute(s1),
110
+
)->Array.map(s2 => combineSubst(s1, s2))
111
+
} else {
112
+
[]
113
+
}
114
+
})
115
+
->Array.flat
116
+
| _ =>
117
+
switch t {
118
+
| [] => []
119
+
| _ => {
120
+
let (t1, ts) = uncons(t)
121
+
if match(s1, t1) {
122
+
oneSide(ss, ts)
123
+
} else {
124
+
[]
125
+
}
126
+
}
127
+
}
128
+
}
129
+
}
130
+
}
131
+
}
132
+
133
+
let pigPug = (s, t) => {
134
+
let search = (targetCycles: int): (array<subst>, bool) => {
135
+
let moreSolsMightExist = ref(false)
136
+
// seen is an assoc list
137
+
let rec inner = (s, t, cycle: int, seen: array<((t, t), int)>): array<
138
+
array<(int, graphSub)>,
139
+
> => {
140
+
let (newSeen, thisCycle) = switch seen->Array.findIndexOpt(((e, _)) => e == (s, t)) {
141
+
| Some(i) => {
142
+
let (_, thisCycle) = seen[i]->Option.getExn
143
+
let newSeen = seen->Array.mapWithIndex((e, j) => i == j ? ((s, t), cycle + 1) : e)
144
+
(newSeen, thisCycle)
145
+
}
146
+
147
+
| None => (Array.concat([((s, t), 1)], seen), 0)
148
+
}
149
+
let cycle = max(thisCycle, cycle)
150
+
let searchSub = (schematic: int, allowed: array<int>, edge: graphSub): array<
151
+
array<(int, graphSub)>,
152
+
> => {
153
+
let piece = Schematic({schematic, allowed})
154
+
let sub = switch edge {
155
+
| Eps => singletonSubst(schematic, [])
156
+
| PieceLitSub(p) => singletonSubst(schematic, [p, piece])
157
+
| SchemaSub(s2, a2) =>
158
+
singletonSubst(schematic, [Schematic({schematic: s2, allowed: a2}), piece])
159
+
}
160
+
inner(substitute(s, sub), substitute(t, sub), cycle, newSeen)->Array.map(path =>
161
+
Array.concat(path, [(schematic, edge)])
162
+
)
163
+
}
164
+
if cycle > targetCycles {
165
+
moreSolsMightExist := true
166
+
[]
167
+
} else {
168
+
switch (s[0], t[0]) {
169
+
| (None, None) => cycle == targetCycles ? [[]] : []
170
+
| (Some(Schematic({schematic, allowed})), other)
171
+
| (other, Some(Schematic({schematic, allowed}))) =>
172
+
switch other {
173
+
| None => searchSub(schematic, allowed, Eps)
174
+
| Some(p) =>
175
+
switch p {
176
+
| String(_) =>
177
+
Array.concat(
178
+
searchSub(schematic, allowed, PieceLitSub(p)),
179
+
searchSub(schematic, allowed, Eps),
180
+
)
181
+
| Schematic({schematic: s2, allowed: a2}) =>
182
+
if schematic == s2 {
183
+
inner(
184
+
s->Array.sliceToEnd(~start=1),
185
+
t->Array.sliceToEnd(~start=1),
186
+
cycle,
187
+
newSeen,
188
+
)
189
+
} else {
190
+
Array.concat(
191
+
searchSub(schematic, allowed, Eps),
192
+
searchSub(schematic, allowed, SchemaSub(s2, a2)),
193
+
)
194
+
}
195
+
| Var({idx}) =>
196
+
if Belt.Set.Int.fromArray(allowed)->Belt.Set.Int.has(idx) {
197
+
Array.concat(
198
+
searchSub(schematic, allowed, PieceLitSub(p)),
199
+
searchSub(schematic, allowed, Eps),
200
+
)
201
+
} else {
202
+
searchSub(schematic, allowed, Eps)
203
+
}
204
+
}
205
+
}
206
+
| (p1, p2) if p1 == p2 =>
207
+
inner(s->Array.sliceToEnd(~start=1), t->Array.sliceToEnd(~start=1), cycle, newSeen)
208
+
| _ => []
209
+
}
210
+
}
211
+
}
212
+
let paths = inner(s, t, 0, [])
213
+
let substs = paths->Array.map(path => {
214
+
let sub = Map.make()
215
+
path->Array.forEach(((schem, edge)) => {
216
+
Map.set(
217
+
sub,
218
+
schem,
219
+
switch edge {
220
+
| Eps => []
221
+
| PieceLitSub(p) => Array.concat(Map.get(sub, schem)->Option.getOr([]), [p])
222
+
| SchemaSub(s2, _) =>
223
+
Array.concat(
224
+
Map.get(sub, schem)->Option.getOr([]),
225
+
Map.get(sub, s2)->Option.getOr([]),
226
+
)
227
+
},
228
+
)
229
+
})
230
+
sub
231
+
})
232
+
let substsSorted = substs->Array.toSorted((s1, s2) => {
233
+
let substLength = s =>
234
+
s
235
+
->Util.mapMapValues(Array.length)
236
+
->Map.values
237
+
->Iterator.toArray
238
+
->Array.reduce(0, (acc, v) => acc + v)
239
+
let (s1Length, s2Length) = (substLength(s1), substLength(s2))
240
+
s1Length < s2Length
241
+
? Ordering.less
242
+
: s2Length < s1Length
243
+
? Ordering.greater
244
+
: Ordering.equal
245
+
})
246
+
(substsSorted, moreSolsMightExist.contents)
247
+
}
248
+
Seq.unfold((0, true), ((c, moreSolsMightExist)) => {
249
+
if moreSolsMightExist {
250
+
let (substs, moreSolsMightExist) = search(c)
251
+
Some(substs->Seq.fromArray, (c + 1, moreSolsMightExist))
252
+
} else {
253
+
None
254
+
}
255
+
})->Seq.flatten
256
+
}
257
+
258
+
// naive: assume schematics appear in at most one side
259
+
let maxCountS = maxSchematicCount(s)
260
+
let maxCountT = maxSchematicCount(t)
261
+
if maxCountS == 0 {
262
+
Seq.fromArray(oneSide(t, s))
263
+
} else if maxCountT == 0 {
264
+
Seq.fromArray(oneSide(s, t))
265
+
} else if max(maxCountS, maxCountT) <= 2 {
266
+
pigPug(s, t)
267
+
} else {
268
+
Seq.fromArray([])
269
+
}
270
+
}
271
+
272
+
// law: unify(a,b) == [{}] iff equivalent(a,b)
273
+
let substDeBruijn = (string: t, substs: Map.t<int, t>, ~from: int=0, ~to: int) => {
274
+
Array.flatMap(string, piece =>
275
+
switch piece {
276
+
| String(_) => [piece]
277
+
| Var({idx: var}) =>
278
+
if var < from {
279
+
[piece]
280
+
} else if var - from < to {
281
+
Map.get(substs, var - from)->Option.getOr([piece])
282
+
} else {
283
+
[Var({idx: var - to})]
284
+
}
285
+
| Schematic({schematic, allowed}) => [
286
+
Schematic({
287
+
schematic,
288
+
allowed: Array.filterMap(allowed, i =>
289
+
if i < from + to {
290
+
None
291
+
} else {
292
+
Some(i - (from + to))
293
+
}
294
+
),
295
+
}),
296
+
]
297
+
}
298
+
)
299
+
}
300
+
301
+
let upshift = (term: t, amount: int, ~from: int=0) =>
302
+
Array.map(term, piece => {
303
+
switch piece {
304
+
| String(_) => piece
305
+
| Var({idx}) =>
306
+
Var({
307
+
idx: if idx >= from {
308
+
idx + amount
309
+
} else {
310
+
idx
311
+
},
312
+
})
313
+
| Schematic({schematic, allowed}) =>
314
+
Schematic({
315
+
schematic,
316
+
allowed: Array.map(allowed, i =>
317
+
if i >= from {
318
+
i + amount
319
+
} else {
320
+
i
321
+
}
322
+
),
323
+
})
324
+
}
325
+
})
326
+
327
+
type gen = ref<int>
328
+
329
+
let prettyPrintVar = (idx: int, scope: array<string>) =>
330
+
"$" ++
331
+
switch scope[idx] {
332
+
| Some(n) if Array.indexOf(scope, n) == idx => n
333
+
| _ => "\\"->String.concat(String.make(idx))
334
+
}
335
+
let prettyPrint = (term: t, ~scope: array<string>) =>
336
+
`"${Array.map(term, piece => {
337
+
switch piece {
338
+
| String(str) => str
339
+
| Var({idx}) => prettyPrintVar(idx, scope)
340
+
| Schematic({schematic, allowed}) => {
341
+
let allowedStr =
342
+
allowed
343
+
->Array.map(idx => prettyPrintVar(idx, scope))
344
+
->Array.join(" ")
345
+
`?${Int.toString(schematic)}(${allowedStr})`
346
+
}
347
+
}
348
+
})->Array.join(" ")}"`
349
+
350
+
type remaining = string
351
+
type errorMessage = string
352
+
type ident = string
353
+
let parse: (string, ~scope: array<meta>, ~gen: gen=?) => result<(t, remaining), errorMessage> = (
354
+
str: string,
355
+
~scope: array<ident>,
356
+
~gen as _=?,
357
+
) => {
358
+
let pos = ref(0)
359
+
let seenCloseString = ref(false)
360
+
let acc = ref(Ok([]))
361
+
362
+
let error = (msg: errorMessage) => {
363
+
let codeAroundLoc = String.slice(str, ~start=pos.contents, ~end=pos.contents + 5)
364
+
acc := Error(`problem here: ${codeAroundLoc}...: ${msg}`)
365
+
}
366
+
367
+
let execRe = Util.execRe
368
+
let advance = n => {
369
+
pos := pos.contents + n
370
+
}
371
+
let advance1 = () => advance(1)
372
+
let add = (token, ~nAdvance=?) => {
373
+
acc.contents
374
+
->Result.map(acc => {
375
+
Array.push(acc, token)
376
+
})
377
+
->ignore
378
+
Option.map(nAdvance, advance)->ignore
379
+
}
380
+
let execRe = re => execRe(re, String.sliceToEnd(str, ~start=pos.contents))
381
+
let stringLit = () => {
382
+
let identRegex = RegExp.fromString(`^${Util.identRegexStr}`)
383
+
let symbolRegex = /^([!@#\$%\^~&*_+\-={};':|,.<>\/?]+)/
384
+
let numberRegex = /^(\d+)/
385
+
switch execRe(identRegex)
386
+
->Option.orElse(execRe(symbolRegex))
387
+
->Option.orElse(execRe(numberRegex)) {
388
+
| Some([match], l) => add(String(match), ~nAdvance=l)
389
+
| Some(_) => error("regex string lit error")
390
+
| None => error("expected string")
391
+
}
392
+
}
393
+
let escaped = () => {
394
+
let escapedRegex = /\\([\$\?\\\"])/
395
+
switch execRe(escapedRegex) {
396
+
| Some([char], l) => add(String(char), ~nAdvance=l)
397
+
| Some(_) => error("regex escaped error")
398
+
| None => error("expected valid escaped character")
399
+
}
400
+
}
401
+
let readInt = s => Int.fromString(s)->Option.getExn
402
+
let schema = () => {
403
+
let schemaRegex = /\?(\d+)\(((?:\d+\s*)*)\)/
404
+
switch execRe(schemaRegex) {
405
+
| Some([idStr, allowedStr], l) => {
406
+
let schematic = readInt(idStr)
407
+
let allowed =
408
+
allowedStr
409
+
->String.trim
410
+
->String.splitByRegExp(/\s+/)
411
+
->Array.keepSome
412
+
->Array.filter(s => s != "")
413
+
->Array.map(readInt)
414
+
add(Schematic({schematic, allowed}), ~nAdvance=l)
415
+
}
416
+
| Some(_) => error("schema lit regex error")
417
+
| None => error("expected schematic literal")
418
+
}
419
+
}
420
+
let var = () => {
421
+
let varLitRegex = /^\$\\(\d+)/
422
+
let varScopeRegex = /^\$([a-zA-Z]\w*)/
423
+
switch execRe(varLitRegex) {
424
+
| Some([match], l) => add(Var({idx: readInt(match)}), ~nAdvance=l)
425
+
| Some(_) => error("var lit regex error")
426
+
| None =>
427
+
switch execRe(varScopeRegex) {
428
+
| Some([ident], l) =>
429
+
switch Array.indexOfOpt(scope, ident) {
430
+
| Some(idx) => add(Var({idx: idx}), ~nAdvance=l)
431
+
| None => error("expected variable in scope")
432
+
}
433
+
| Some(_) => error("var regex error")
434
+
| None => error("expected var")
435
+
}
436
+
}
437
+
}
438
+
439
+
// consume leading whitespace + open quote
440
+
switch execRe(/^\s*"/) {
441
+
| Some(_, l) => pos := l
442
+
| None => error("expected open quote")
443
+
}
444
+
while (
445
+
pos.contents < String.length(str) && Result.isOk(acc.contents) && !seenCloseString.contents
446
+
) {
447
+
let c = String.get(str, pos.contents)->Option.getExn
448
+
switch c {
449
+
| "\"" => {
450
+
advance1()
451
+
seenCloseString := true
452
+
}
453
+
| "$" => var()
454
+
| "?" => schema()
455
+
| " " | "\t" | "\r" | "\n" => advance1()
456
+
| ")" | "(" | "[" | "]" => add(String(c), ~nAdvance=1)
457
+
| "\\" => escaped()
458
+
| _ => stringLit()
459
+
}
460
+
}
461
+
462
+
acc.contents->Result.map(r => (r, str->String.sliceToEnd(~start=pos.contents)))
463
+
}
464
+
465
+
let lowerSchematic = (schematic, allowed) => Some([Schematic({schematic, allowed})])
466
+
let lowerVar = idx => Some([Var({idx: idx})])
467
+
let concrete = t =>
468
+
t->Array.every(p =>
469
+
switch p {
470
+
| Schematic(_) => true
471
+
| _ => false
472
+
}
473
+
)
474
+
}
475
+
476
+
module AtomView = {
477
+
type props = {name: t, scope: array<string>}
478
+
type idx_props = {idx: int, scope: array<string>}
479
+
let viewVar = (props: idx_props) =>
480
+
switch props.scope[props.idx] {
481
+
| Some(n) if Array.indexOf(props.scope, n) == props.idx =>
482
+
<span className="term-metavar"> {React.string(n)} </span>
483
+
| _ =>
484
+
<span className="term-metavar-unnamed">
485
+
{React.string("\\")}
486
+
{React.int(props.idx)}
487
+
</span>
488
+
}
489
+
490
+
let makeMeta = (str: string) =>
491
+
<span className="rule-binder">
492
+
{React.string(str)}
493
+
{React.string(".")}
494
+
</span>
495
+
496
+
let parenthesise = f =>
497
+
[
498
+
<span className="symbol" key={"-1"}> {React.string("(")} </span>,
499
+
...f,
500
+
<span className="symbol" key={"-2"}> {React.string(")")} </span>,
501
+
]
502
+
503
+
let intersperse = a => Util.intersperse(a, ~with=React.string(" "))
504
+
505
+
module Piece = {
506
+
@react.component
507
+
let make = (~piece: piece, ~scope) =>
508
+
switch piece {
509
+
| Var({idx}) => viewVar({idx, scope})
510
+
| String(s) => <span className="term-const"> {React.string(s)} </span>
511
+
| Schematic({schematic: s, allowed: vs}) =>
512
+
<span className="term-schematic">
513
+
{React.string("?")}
514
+
{React.int(s)}
515
+
<span className="term-schematic-telescope">
516
+
{vs
517
+
->Array.mapWithIndex((v, i) =>
518
+
React.createElement(viewVar, Util.withKey({idx: v, scope}, i))
519
+
)
520
+
->intersperse
521
+
->parenthesise
522
+
->React.array}
523
+
</span>
524
+
</span>
525
+
}
526
+
}
527
+
528
+
@react.componentWithProps
529
+
let make = ({name, scope}) =>
530
+
<span className="term-compound">
531
+
{React.string("\"")}
532
+
{name
533
+
->Array.mapWithIndex((piece, i) => {
534
+
let key = Int.toString(i)
535
+
<Piece piece scope key />
536
+
})
537
+
->intersperse
538
+
->React.array}
539
+
{React.string("\"")}
540
+
</span>
541
+
}
+8
src/StringA.resi
+8
src/StringA.resi
-471
src/StringAtom.res
-471
src/StringAtom.res
···
1
-
module IntCmp = Belt.Id.MakeComparable({
2
-
type t = int
3
-
let cmp = Pervasives.compare
4
-
})
5
-
6
-
type piece =
7
-
| String(string)
8
-
| Var({idx: int})
9
-
| Schematic({schematic: int, allowed: array<int>})
10
-
type t = array<piece>
11
-
type meta = string
12
-
type schematic = int
13
-
type subst = Map.t<schematic, t>
14
-
15
-
let substitute = (term: t, subst: subst) =>
16
-
Array.flatMap(term, piece => {
17
-
switch piece {
18
-
| Schematic({schematic, _}) =>
19
-
switch Map.get(subst, schematic) {
20
-
| None => [piece]
21
-
| Some(found) => found
22
-
}
23
-
| _ => [piece]
24
-
}
25
-
})
26
-
let schematicsCountsIn: t => Belt.Map.Int.t<int> = (term: t) =>
27
-
Array.reduce(term, Belt.Map.Int.empty, (m, p) =>
28
-
switch p {
29
-
| Schematic({schematic, _}) =>
30
-
m->Belt.Map.Int.update(schematic, o =>
31
-
o
32
-
->Option.map(v => v + 1)
33
-
->Option.orElse(Some(1))
34
-
)
35
-
| _ => m
36
-
}
37
-
)
38
-
let maxSchematicCount = (term: t) => {
39
-
schematicsCountsIn(term)->Belt.Map.Int.maximum->Option.map(Pair.second)->Option.getOr(0)
40
-
}
41
-
let freeVarsIn = (term: t): Belt.Set.t<int, IntCmp.identity> =>
42
-
Array.map(term, piece => {
43
-
switch piece {
44
-
| Var({idx}) => Belt.Set.make(~id=module(IntCmp))->Belt.Set.add(idx)
45
-
| _ => Belt.Set.make(~id=module(IntCmp))
46
-
}
47
-
})->Array.reduce(Belt.Set.make(~id=module(IntCmp)), (s1, s2) => Belt.Set.union(s1, s2))
48
-
49
-
let combineSubst = (s: subst, t: subst) => {
50
-
let nu = Map.make()
51
-
Map.entries(s)->Iterator.forEach(opt =>
52
-
switch opt {
53
-
| None => ()
54
-
| Some((key, term)) => nu->Map.set(key, term->substitute(t))
55
-
}
56
-
)
57
-
Map.entries(t)->Iterator.forEach(opt =>
58
-
switch opt {
59
-
| None => ()
60
-
| Some((key, term)) => nu->Map.set(key, term->substitute(s))
61
-
}
62
-
)
63
-
nu
64
-
}
65
-
66
-
let emptySubst: subst = Map.make()
67
-
let singletonSubst: (int, t) => subst = (schematic, term) => {
68
-
let s = Map.make()
69
-
s->Map.set(schematic, term)
70
-
s
71
-
}
72
-
73
-
let uncons = (xs: array<'a>): ('a, array<'a>) => {
74
-
switch xs {
75
-
| [] => Error("expected nonempty array")->Result.getExn
76
-
| _ => (xs[0]->Option.getExn, Array.sliceToEnd(xs, ~start=1))
77
-
}
78
-
}
79
-
80
-
type graphSub = Eps | PieceLitSub(piece) | SchemaSub(int, array<int>)
81
-
let unify = (s: array<piece>, t: array<piece>, ~gen as _=?): Seq.t<subst> => {
82
-
let match = (p1: piece, p2: piece) => {
83
-
switch (p1, p2) {
84
-
| (String(na), String(nb)) if na == nb => true
85
-
| (Var({idx: ia}), Var({idx: ib})) if ia == ib => true
86
-
| (_, _) => false
87
-
}
88
-
}
89
-
90
-
let rec oneSide = (s, t) => {
91
-
switch (s, t) {
92
-
| ([], []) => [emptySubst]
93
-
| ([], _) => []
94
-
| (_, _) => {
95
-
let (s1, ss) = uncons(s)
96
-
switch s1 {
97
-
| Schematic({schematic, allowed}) =>
98
-
Belt.Array.range(0, Array.length(t))
99
-
->Array.map(i => {
100
-
let subTerm = Array.slice(t, ~start=0, ~end=i)
101
-
let freeVars = freeVarsIn(subTerm)
102
-
let allowedVars = Belt.Set.fromArray(allowed, ~id=module(IntCmp))
103
-
if Belt.Set.subset(freeVars, allowedVars) {
104
-
let s1 = singletonSubst(schematic, subTerm)
105
-
oneSide(
106
-
substitute(ss, s1),
107
-
Array.sliceToEnd(t, ~start=i)->substitute(s1),
108
-
)->Array.map(s2 => combineSubst(s1, s2))
109
-
} else {
110
-
[]
111
-
}
112
-
})
113
-
->Array.flat
114
-
| _ =>
115
-
switch t {
116
-
| [] => []
117
-
| _ => {
118
-
let (t1, ts) = uncons(t)
119
-
if match(s1, t1) {
120
-
oneSide(ss, ts)
121
-
} else {
122
-
[]
123
-
}
124
-
}
125
-
}
126
-
}
127
-
}
128
-
}
129
-
}
130
-
131
-
let pigPug = (s, t) => {
132
-
let search = (targetCycles: int): (array<subst>, bool) => {
133
-
let moreSolsMightExist = ref(false)
134
-
// seen is an assoc list
135
-
let rec inner = (s, t, cycle: int, seen: array<((t, t), int)>): array<
136
-
array<(int, graphSub)>,
137
-
> => {
138
-
let (newSeen, thisCycle) = switch seen->Array.findIndexOpt(((e, _)) => e == (s, t)) {
139
-
| Some(i) => {
140
-
let (_, thisCycle) = seen[i]->Option.getExn
141
-
let newSeen = seen->Array.mapWithIndex((e, j) => i == j ? ((s, t), cycle + 1) : e)
142
-
(newSeen, thisCycle)
143
-
}
144
-
145
-
| None => (Array.concat([((s, t), 1)], seen), 0)
146
-
}
147
-
let cycle = max(thisCycle, cycle)
148
-
let searchSub = (schematic: int, allowed: array<int>, edge: graphSub): array<
149
-
array<(int, graphSub)>,
150
-
> => {
151
-
let piece = Schematic({schematic, allowed})
152
-
let sub = switch edge {
153
-
| Eps => singletonSubst(schematic, [])
154
-
| PieceLitSub(p) => singletonSubst(schematic, [p, piece])
155
-
| SchemaSub(s2, a2) =>
156
-
singletonSubst(schematic, [Schematic({schematic: s2, allowed: a2}), piece])
157
-
}
158
-
inner(substitute(s, sub), substitute(t, sub), cycle, newSeen)->Array.map(path =>
159
-
Array.concat(path, [(schematic, edge)])
160
-
)
161
-
}
162
-
if cycle > targetCycles {
163
-
moreSolsMightExist := true
164
-
[]
165
-
} else {
166
-
switch (s[0], t[0]) {
167
-
| (None, None) => cycle == targetCycles ? [[]] : []
168
-
| (Some(Schematic({schematic, allowed})), other)
169
-
| (other, Some(Schematic({schematic, allowed}))) =>
170
-
switch other {
171
-
| None => searchSub(schematic, allowed, Eps)
172
-
| Some(p) =>
173
-
switch p {
174
-
| String(_) =>
175
-
Array.concat(
176
-
searchSub(schematic, allowed, PieceLitSub(p)),
177
-
searchSub(schematic, allowed, Eps),
178
-
)
179
-
| Schematic({schematic: s2, allowed: a2}) =>
180
-
if schematic == s2 {
181
-
inner(
182
-
s->Array.sliceToEnd(~start=1),
183
-
t->Array.sliceToEnd(~start=1),
184
-
cycle,
185
-
newSeen,
186
-
)
187
-
} else {
188
-
Array.concat(
189
-
searchSub(schematic, allowed, Eps),
190
-
searchSub(schematic, allowed, SchemaSub(s2, a2)),
191
-
)
192
-
}
193
-
| Var({idx}) =>
194
-
if Belt.Set.Int.fromArray(allowed)->Belt.Set.Int.has(idx) {
195
-
Array.concat(
196
-
searchSub(schematic, allowed, PieceLitSub(p)),
197
-
searchSub(schematic, allowed, Eps),
198
-
)
199
-
} else {
200
-
searchSub(schematic, allowed, Eps)
201
-
}
202
-
}
203
-
}
204
-
| (p1, p2) if p1 == p2 =>
205
-
inner(s->Array.sliceToEnd(~start=1), t->Array.sliceToEnd(~start=1), cycle, newSeen)
206
-
| _ => []
207
-
}
208
-
}
209
-
}
210
-
let paths = inner(s, t, 0, [])
211
-
let substs = paths->Array.map(path => {
212
-
let sub = Map.make()
213
-
path->Array.forEach(((schem, edge)) => {
214
-
Map.set(
215
-
sub,
216
-
schem,
217
-
switch edge {
218
-
| Eps => []
219
-
| PieceLitSub(p) => Array.concat(Map.get(sub, schem)->Option.getOr([]), [p])
220
-
| SchemaSub(s2, _) =>
221
-
Array.concat(
222
-
Map.get(sub, schem)->Option.getOr([]),
223
-
Map.get(sub, s2)->Option.getOr([]),
224
-
)
225
-
},
226
-
)
227
-
})
228
-
sub
229
-
})
230
-
let substsSorted = substs->Array.toSorted((s1, s2) => {
231
-
let substLength = s =>
232
-
s
233
-
->Util.mapMapValues(Array.length)
234
-
->Map.values
235
-
->Iterator.toArray
236
-
->Array.reduce(0, (acc, v) => acc + v)
237
-
let (s1Length, s2Length) = (substLength(s1), substLength(s2))
238
-
s1Length < s2Length
239
-
? Ordering.less
240
-
: s2Length < s1Length
241
-
? Ordering.greater
242
-
: Ordering.equal
243
-
})
244
-
(substsSorted, moreSolsMightExist.contents)
245
-
}
246
-
Seq.unfold((0, true), ((c, moreSolsMightExist)) => {
247
-
if moreSolsMightExist {
248
-
let (substs, moreSolsMightExist) = search(c)
249
-
Some(substs->Seq.fromArray, (c + 1, moreSolsMightExist))
250
-
} else {
251
-
None
252
-
}
253
-
})->Seq.flatten
254
-
}
255
-
256
-
// naive: assume schematics appear in at most one side
257
-
let maxCountS = maxSchematicCount(s)
258
-
let maxCountT = maxSchematicCount(t)
259
-
if maxCountS == 0 {
260
-
Seq.fromArray(oneSide(t, s))
261
-
} else if maxCountT == 0 {
262
-
Seq.fromArray(oneSide(s, t))
263
-
} else if max(maxCountS, maxCountT) <= 2 {
264
-
pigPug(s, t)
265
-
} else {
266
-
Seq.fromArray([])
267
-
}
268
-
}
269
-
270
-
// law: unify(a,b) == [{}] iff equivalent(a,b)
271
-
let substDeBruijn = (string: t, substs: Map.t<int, t>, ~from: int=0, ~to: int) => {
272
-
Array.flatMap(string, piece =>
273
-
switch piece {
274
-
| String(_) => [piece]
275
-
| Var({idx: var}) =>
276
-
if var < from {
277
-
[piece]
278
-
} else if var - from < to {
279
-
Map.get(substs, var - from)->Option.getOr([piece])
280
-
} else {
281
-
[Var({idx: var - to})]
282
-
}
283
-
| Schematic({schematic, allowed}) => [
284
-
Schematic({
285
-
schematic,
286
-
allowed: Array.filterMap(allowed, i =>
287
-
if i < from + to {
288
-
None
289
-
} else {
290
-
Some(i - (from + to))
291
-
}
292
-
),
293
-
}),
294
-
]
295
-
}
296
-
)
297
-
}
298
-
299
-
let upshift = (term: t, amount: int, ~from: int=0) =>
300
-
Array.map(term, piece => {
301
-
switch piece {
302
-
| String(_) => piece
303
-
| Var({idx}) =>
304
-
Var({
305
-
idx: if idx >= from {
306
-
idx + amount
307
-
} else {
308
-
idx
309
-
},
310
-
})
311
-
| Schematic({schematic, allowed}) =>
312
-
Schematic({
313
-
schematic,
314
-
allowed: Array.map(allowed, i =>
315
-
if i >= from {
316
-
i + amount
317
-
} else {
318
-
i
319
-
}
320
-
),
321
-
})
322
-
}
323
-
})
324
-
325
-
type gen = ref<int>
326
-
327
-
let prettyPrintVar = (idx: int, scope: array<string>) =>
328
-
"$" ++
329
-
switch scope[idx] {
330
-
| Some(n) if Array.indexOf(scope, n) == idx => n
331
-
| _ => "\\"->String.concat(String.make(idx))
332
-
}
333
-
let prettyPrint = (term: t, ~scope: array<string>) =>
334
-
`"${Array.map(term, piece => {
335
-
switch piece {
336
-
| String(str) => str
337
-
| Var({idx}) => prettyPrintVar(idx, scope)
338
-
| Schematic({schematic, allowed}) => {
339
-
let allowedStr =
340
-
allowed
341
-
->Array.map(idx => prettyPrintVar(idx, scope))
342
-
->Array.join(" ")
343
-
`?${Int.toString(schematic)}(${allowedStr})`
344
-
}
345
-
}
346
-
})->Array.join(" ")}"`
347
-
348
-
type remaining = string
349
-
type errorMessage = string
350
-
type ident = string
351
-
let parse: (string, ~scope: array<meta>, ~gen: gen=?) => result<(t, remaining), errorMessage> = (
352
-
str: string,
353
-
~scope: array<ident>,
354
-
~gen as _=?,
355
-
) => {
356
-
let pos = ref(0)
357
-
let seenCloseString = ref(false)
358
-
let acc = ref(Ok([]))
359
-
360
-
let error = (msg: errorMessage) => {
361
-
let codeAroundLoc = String.slice(str, ~start=pos.contents, ~end=pos.contents + 5)
362
-
acc := Error(`problem here: ${codeAroundLoc}...: ${msg}`)
363
-
}
364
-
365
-
let execRe = Util.execRe
366
-
let advance = n => {
367
-
pos := pos.contents + n
368
-
}
369
-
let advance1 = () => advance(1)
370
-
let add = (token, ~nAdvance=?) => {
371
-
acc.contents
372
-
->Result.map(acc => {
373
-
Array.push(acc, token)
374
-
})
375
-
->ignore
376
-
Option.map(nAdvance, advance)->ignore
377
-
}
378
-
let execRe = re => execRe(re, String.sliceToEnd(str, ~start=pos.contents))
379
-
let stringLit = () => {
380
-
let identRegex = RegExp.fromString(`^${Util.identRegexStr}`)
381
-
let symbolRegex = /^([!@#\$%\^~&*_+\-={};':|,.<>\/?]+)/
382
-
let numberRegex = /^(\d+)/
383
-
switch execRe(identRegex)
384
-
->Option.orElse(execRe(symbolRegex))
385
-
->Option.orElse(execRe(numberRegex)) {
386
-
| Some([match], l) => add(String(match), ~nAdvance=l)
387
-
| Some(_) => error("regex string lit error")
388
-
| None => error("expected string")
389
-
}
390
-
}
391
-
let escaped = () => {
392
-
let escapedRegex = /\\([\$\?\\\"])/
393
-
switch execRe(escapedRegex) {
394
-
| Some([char], l) => add(String(char), ~nAdvance=l)
395
-
| Some(_) => error("regex escaped error")
396
-
| None => error("expected valid escaped character")
397
-
}
398
-
}
399
-
let readInt = s => Int.fromString(s)->Option.getExn
400
-
let schema = () => {
401
-
let schemaRegex = /\?(\d+)\(((?:\d+\s*)*)\)/
402
-
switch execRe(schemaRegex) {
403
-
| Some([idStr, allowedStr], l) => {
404
-
let schematic = readInt(idStr)
405
-
let allowed =
406
-
allowedStr
407
-
->String.trim
408
-
->String.splitByRegExp(/\s+/)
409
-
->Array.keepSome
410
-
->Array.filter(s => s != "")
411
-
->Array.map(readInt)
412
-
add(Schematic({schematic, allowed}), ~nAdvance=l)
413
-
}
414
-
| Some(_) => error("schema lit regex error")
415
-
| None => error("expected schematic literal")
416
-
}
417
-
}
418
-
let var = () => {
419
-
let varLitRegex = /^\$\\(\d+)/
420
-
let varScopeRegex = /^\$([a-zA-Z]\w*)/
421
-
switch execRe(varLitRegex) {
422
-
| Some([match], l) => add(Var({idx: readInt(match)}), ~nAdvance=l)
423
-
| Some(_) => error("var lit regex error")
424
-
| None =>
425
-
switch execRe(varScopeRegex) {
426
-
| Some([ident], l) =>
427
-
switch Array.indexOfOpt(scope, ident) {
428
-
| Some(idx) => add(Var({idx: idx}), ~nAdvance=l)
429
-
| None => error("expected variable in scope")
430
-
}
431
-
| Some(_) => error("var regex error")
432
-
| None => error("expected var")
433
-
}
434
-
}
435
-
}
436
-
437
-
// consume leading whitespace + open quote
438
-
switch execRe(/^\s*"/) {
439
-
| Some(_, l) => pos := l
440
-
| None => error("expected open quote")
441
-
}
442
-
while (
443
-
pos.contents < String.length(str) && Result.isOk(acc.contents) && !seenCloseString.contents
444
-
) {
445
-
let c = String.get(str, pos.contents)->Option.getExn
446
-
switch c {
447
-
| "\"" => {
448
-
advance1()
449
-
seenCloseString := true
450
-
}
451
-
| "$" => var()
452
-
| "?" => schema()
453
-
| " " | "\t" | "\r" | "\n" => advance1()
454
-
| ")" | "(" | "[" | "]" => add(String(c), ~nAdvance=1)
455
-
| "\\" => escaped()
456
-
| _ => stringLit()
457
-
}
458
-
}
459
-
460
-
acc.contents->Result.map(r => (r, str->String.sliceToEnd(~start=pos.contents)))
461
-
}
462
-
463
-
let lowerSchematic = (schematic, allowed) => Some([Schematic({schematic, allowed})])
464
-
let lowerVar = idx => Some([Var({idx: idx})])
465
-
let concrete = t =>
466
-
t->Array.every(p =>
467
-
switch p {
468
-
| Schematic(_) => true
469
-
| _ => false
470
-
}
471
-
)
-9
src/StringAtom.resi
-9
src/StringAtom.resi
-64
src/StringAtomView.res
-64
src/StringAtomView.res
···
1
-
type props = {name: StringAtom.t, scope: array<string>}
2
-
type idx_props = {idx: int, scope: array<string>}
3
-
let viewVar = (props: idx_props) =>
4
-
switch props.scope[props.idx] {
5
-
| Some(n) if Array.indexOf(props.scope, n) == props.idx =>
6
-
<span className="term-metavar"> {React.string(n)} </span>
7
-
| _ =>
8
-
<span className="term-metavar-unnamed">
9
-
{React.string("\\")}
10
-
{React.int(props.idx)}
11
-
</span>
12
-
}
13
-
14
-
let makeMeta = (str: string) =>
15
-
<span className="rule-binder">
16
-
{React.string(str)}
17
-
{React.string(".")}
18
-
</span>
19
-
20
-
let parenthesise = f =>
21
-
[
22
-
<span className="symbol" key={"-1"}> {React.string("(")} </span>,
23
-
...f,
24
-
<span className="symbol" key={"-2"}> {React.string(")")} </span>,
25
-
]
26
-
27
-
let intersperse = a => Util.intersperse(a, ~with=React.string(" "))
28
-
29
-
module Piece = {
30
-
@react.component
31
-
let make = (~piece: StringAtom.piece, ~scope) =>
32
-
switch piece {
33
-
| Var({idx}) => viewVar({idx, scope})
34
-
| String(s) => <span className="term-const"> {React.string(s)} </span>
35
-
| Schematic({schematic: s, allowed: vs}) =>
36
-
<span className="term-schematic">
37
-
{React.string("?")}
38
-
{React.int(s)}
39
-
<span className="term-schematic-telescope">
40
-
{vs
41
-
->Array.mapWithIndex((v, i) =>
42
-
React.createElement(viewVar, Util.withKey({idx: v, scope}, i))
43
-
)
44
-
->intersperse
45
-
->parenthesise
46
-
->React.array}
47
-
</span>
48
-
</span>
49
-
}
50
-
}
51
-
52
-
@react.componentWithProps
53
-
let make = ({name, scope}) =>
54
-
<span className="term-compound">
55
-
{React.string("\"")}
56
-
{name
57
-
->Array.mapWithIndex((piece, i) => {
58
-
let key = Int.toString(i)
59
-
<Piece piece scope key />
60
-
})
61
-
->intersperse
62
-
->React.array}
63
-
{React.string("\"")}
64
-
</span>
-1
src/StringAtomView.resi
-1
src/StringAtomView.resi
···
1
-
include SExpViewFunc.ATOM_VIEW with module Atom := StringAtom
+14
-16
src/StringAxiomSet.res
+14
-16
src/StringAxiomSet.res
···
1
1
open Component
2
2
3
-
module Term = StringSExp
4
-
module Judgment = StringSExp
5
-
module JudgmentView = StringSExpJView
3
+
module StringSExp = SExpFunc.Make(StringSymbol.Atom)
4
+
module TermView = SExpViewFunc.Make(StringSymbol.Atom, StringSymbol.AtomView, StringSExp)
5
+
module JudgmentView = TermViewAsJudgmentView.Make(StringSExp, StringSExp, TermView)
6
6
7
-
module Rule = Rule.Make(Term, Judgment)
8
-
module RuleView = RuleView.Make(Term, Judgment, JudgmentView)
9
-
module Ports = Ports(Term, Judgment)
7
+
module Rule = Rule.Make(StringSExp, StringSExp)
8
+
module RuleView = RuleView.Make(StringSExp, StringSExp, JudgmentView)
9
+
module Ports = Ports(StringSExp, StringSExp)
10
10
type state = {
11
11
raw: dict<Rule.t>,
12
12
derived: dict<Rule.t>,
···
24
24
}
25
25
26
26
module Set = Belt.Set.String
27
-
module SExp = StringSExp
28
27
let varsInRule = (rule: Rule.t) => {
29
28
rule.premises->Array.reduce(Set.fromArray(rule.vars), (s, r) =>
30
29
s->Set.union(Set.fromArray(r.vars))
31
30
)
32
31
}
33
32
34
-
let getSExpName = (t: SExp.t): option<string> =>
33
+
let getSExpName = (t: StringSExp.t): option<string> =>
35
34
switch t {
36
-
| Atom(name) => Some(name->SExp.StringSExpAtom.prettyPrint(~scope=[]))
35
+
| Atom(name) => Some(name->StringSymbol.Atom.prettyPrint(~scope=[]))
37
36
| _ => None
38
37
}
39
38
40
-
open StringSExp
41
-
let destructure = (r: Judgment.t): (StringAtom.t, string) =>
39
+
let destructure = (r: StringSExp.t): (StringA.Atom.t, string) =>
42
40
switch r {
43
41
| Compound({subexps: [Atom(StringS(s)), Atom(ConstS(name))]}) => (s, name)
44
42
| _ => throw(Util.Unreachable("expected valid induction rule"))
45
43
}
46
-
let destructureOpt = (r: Judgment.t): option<(StringAtom.t, string)> =>
44
+
let destructureOpt = (r: StringSExp.t): option<(StringA.Atom.t, string)> =>
47
45
switch r {
48
46
| Compound({subexps: [Atom(StringS(s)), Atom(ConstS(name))]}) => Some((s, name))
49
47
| _ => None
50
48
}
51
-
let structure = (lhs: StringSExp.t, rhs: StringSExp.t): Judgment.t => Compound({
49
+
let structure = (lhs: StringSExp.t, rhs: StringSExp.t): StringSExp.t => Compound({
52
50
subexps: [lhs, rhs],
53
51
})
54
52
let findMentionedRuleGroups = (group: judgeGroup, allGroups: array<judgeGroup>): array<
···
88
86
let xIdx = vars->Array.findIndex(i => i == x)
89
87
let aIdx = vars->Array.findIndex(i => i == a)
90
88
let bIdx = vars->Array.findIndex(i => i == b)
91
-
let surround = (t: StringAtom.t, aIdx: int, bIdx: int) => {
92
-
Array.concat(Array.concat([StringAtom.Var({idx: aIdx})], t), [StringAtom.Var({idx: bIdx})])
89
+
let surround = (t: StringA.Atom.t, aIdx: int, bIdx: int) => {
90
+
Array.concat(Array.concat([StringA.Var({idx: aIdx})], t), [StringA.Var({idx: bIdx})])
93
91
}
94
92
let lookupGroup = (name: string): option<int> =>
95
93
mentionedGroups->Array.findIndexOpt(g => name == g.name)
···
128
126
mentionedGroups->Array.flatMap(g => g.rules->Array.map(r => replaceJudgeRHS(r, 0))),
129
127
),
130
128
conclusion: structure(
131
-
surround([StringAtom.Var({idx: xIdx})], aIdx, bIdx)->StringS->Atom,
129
+
surround([StringA.Var({idx: xIdx})], aIdx, bIdx)->StringS->Atom,
132
130
Var({idx: 0}),
133
131
), // TODO: clean here
134
132
}
-81
src/StringSExp.res
-81
src/StringSExp.res
···
1
-
type stringSExpAtom = StringS(StringAtom.t) | ConstS(string)
2
-
3
-
module StringSExpAtom: SExpFunc.ATOM with type t = stringSExpAtom = {
4
-
type t = stringSExpAtom
5
-
type subst = Map.t<int, t>
6
-
type gen = ref<int>
7
-
let parse = (s, ~scope, ~gen: option<gen>=?) => {
8
-
StringAtom.parse(s, ~scope, ~gen?)
9
-
->Result.map(((r, rest)) => (StringS(r), rest))
10
-
->Util.Result.or(() =>
11
-
SExp.SymbolAtom.parse(s, ~scope, ~gen?)->Result.map(((r, rest)) => (ConstS(r), rest))
12
-
)
13
-
}
14
-
let prettyPrint = (s, ~scope) =>
15
-
switch s {
16
-
| StringS(s) => StringAtom.prettyPrint(s, ~scope)
17
-
| ConstS(s) => SExp.SymbolAtom.prettyPrint(s, ~scope)
18
-
}
19
-
let unify = (s1, s2, ~gen=?) =>
20
-
switch (s1, s2) {
21
-
| (StringS(s1), StringS(s2)) =>
22
-
StringAtom.unify(s1, s2, ~gen?)->Seq.map(subst => subst->Util.mapMapValues(v => StringS(v)))
23
-
| (ConstS(s1), ConstS(s2)) =>
24
-
SExp.SymbolAtom.unify(s1, s2, ~gen?)->Seq.map(subst =>
25
-
subst->Util.mapMapValues(v => ConstS(v))
26
-
)
27
-
| (_, _) => Seq.empty
28
-
}
29
-
let substitute = (s, subst: subst) =>
30
-
switch s {
31
-
| StringS(s) => {
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
43
-
StringS(StringAtom.substitute(s, stringSubs))
44
-
}
45
-
| ConstS(s) => ConstS(s)
46
-
}
47
-
let upshift = (s, amount: int, ~from=?) =>
48
-
switch s {
49
-
| StringS(s) => StringS(s->StringAtom.upshift(amount, ~from?))
50
-
| ConstS(s) => ConstS(s)
51
-
}
52
-
let lowerVar = idx => Some(StringS([StringAtom.Var({idx: idx})]))
53
-
let lowerSchematic = (schematic, allowed) => Some(
54
-
StringS([StringAtom.Schematic({schematic, allowed})]),
55
-
)
56
-
let substDeBruijn = (s, substs: Map.t<int, t>, ~from=?, ~to: int) =>
57
-
switch s {
58
-
| StringS(s) => {
59
-
let stringSubs =
60
-
substs
61
-
->Map.entries
62
-
->Iterator.toArrayWithMapper(((i, v)) =>
63
-
switch v {
64
-
| StringS(s) => Some((i, s))
65
-
| _ => None
66
-
}
67
-
)
68
-
->Array.keepSome
69
-
->Map.fromArray
70
-
StringS(StringAtom.substDeBruijn(s, stringSubs, ~from?, ~to))
71
-
}
72
-
| ConstS(s) => ConstS(s)
73
-
}
74
-
let concrete = s =>
75
-
switch s {
76
-
| StringS(s) => StringAtom.concrete(s)
77
-
| ConstS(_) => false
78
-
}
79
-
}
80
-
81
-
include SExpFunc.Make(StringSExpAtom)
-4
src/StringSExp.resi
-4
src/StringSExp.resi
-18
src/StringSExpJView.res
-18
src/StringSExpJView.res
···
1
-
module StringAtomView: SExpViewFunc.ATOM_VIEW with module Atom := StringSExp.StringSExpAtom = {
2
-
type props = {name: StringSExp.StringSExpAtom.t, scope: array<string>}
3
-
let make = ({name, scope}: props) =>
4
-
switch name {
5
-
| StringSExp.StringS(name) => <StringAtomView name scope />
6
-
| StringSExp.ConstS(name) => <SExpView.SymbolAtomView name scope />
7
-
}
8
-
}
9
-
10
-
module StringSExpJ = StringSExp
11
-
module View = SExpViewFunc.Make(StringSExp.StringSExpAtom, StringAtomView, StringSExp)
12
-
13
-
module TermView = View
14
-
type props = {
15
-
judgment: StringSExp.t,
16
-
scope: array<string>,
17
-
}
18
-
let make = ({judgment, scope}) => View.make({term: judgment, scope})
-3
src/StringSExpJView.resi
-3
src/StringSExpJView.resi
+86
src/StringSymbol.res
+86
src/StringSymbol.res
···
1
+
type t = StringS(StringA.Atom.t) | ConstS(string)
2
+
3
+
module Atom: SExpFunc.ATOM with type t = t = {
4
+
type t = t
5
+
type subst = Map.t<int, t>
6
+
type gen = ref<int>
7
+
let parse = (s, ~scope, ~gen: option<gen>=?) => {
8
+
StringA.Atom.parse(s, ~scope, ~gen?)
9
+
->Result.map(((r, rest)) => (StringS(r), rest))
10
+
->Util.Result.or(() =>
11
+
Symbolic.Atom.parse(s, ~scope, ~gen?)->Result.map(((r, rest)) => (ConstS(r), rest))
12
+
)
13
+
}
14
+
let prettyPrint = (s, ~scope) =>
15
+
switch s {
16
+
| StringS(s) => StringA.Atom.prettyPrint(s, ~scope)
17
+
| ConstS(s) => Symbolic.Atom.prettyPrint(s, ~scope)
18
+
}
19
+
let unify = (s1, s2, ~gen=?) =>
20
+
switch (s1, s2) {
21
+
| (StringS(s1), StringS(s2)) =>
22
+
StringA.Atom.unify(s1, s2, ~gen?)->Seq.map(subst => subst->Util.mapMapValues(v => StringS(v)))
23
+
| (ConstS(s1), ConstS(s2)) =>
24
+
Symbolic.Atom.unify(s1, s2, ~gen?)->Seq.map(subst => subst->Util.mapMapValues(v => ConstS(v)))
25
+
| (_, _) => Seq.empty
26
+
}
27
+
let substitute = (s, subst: subst) =>
28
+
switch s {
29
+
| StringS(s) => {
30
+
let stringSubs =
31
+
subst
32
+
->Map.entries
33
+
->Iterator.toArrayWithMapper(((i, v)) =>
34
+
switch v {
35
+
| StringS(s) => Some((i, s))
36
+
| _ => None
37
+
}
38
+
)
39
+
->Array.keepSome
40
+
->Map.fromArray
41
+
StringS(StringA.Atom.substitute(s, stringSubs))
42
+
}
43
+
| ConstS(s) => ConstS(s)
44
+
}
45
+
let upshift = (s, amount: int, ~from=?) =>
46
+
switch s {
47
+
| StringS(s) => StringS(s->StringA.Atom.upshift(amount, ~from?))
48
+
| ConstS(s) => ConstS(s)
49
+
}
50
+
let lowerVar = idx => Some(StringS([StringA.Var({idx: idx})]))
51
+
let lowerSchematic = (schematic, allowed) => Some(
52
+
StringS([StringA.Schematic({schematic, allowed})]),
53
+
)
54
+
let substDeBruijn = (s, substs: Map.t<int, t>, ~from=?, ~to: int) =>
55
+
switch s {
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))
69
+
}
70
+
| ConstS(s) => ConstS(s)
71
+
}
72
+
let concrete = s =>
73
+
switch s {
74
+
| StringS(s) => StringA.Atom.concrete(s)
75
+
| ConstS(_) => false
76
+
}
77
+
}
78
+
79
+
module AtomView: SExpViewFunc.ATOM_VIEW with module Atom := Atom = {
80
+
type props = {name: Atom.t, scope: array<string>}
81
+
let make = ({name, scope}: props) =>
82
+
switch name {
83
+
| StringS(name) => <StringA.AtomView name scope />
84
+
| ConstS(name) => <Symbolic.AtomView name scope />
85
+
}
86
+
}
+3
src/StringSymbol.resi
+3
src/StringSymbol.resi
+3
src/Symbolic.resi
+3
src/Symbolic.resi
+12
src/TermViewAsJudgmentView.res
+12
src/TermViewAsJudgmentView.res
···
1
+
module Make = (
2
+
Term: Signatures.TERM,
3
+
Judgment: Signatures.JUDGMENT with module Term := Term and type t = Term.t,
4
+
TermView: Signatures.TERM_VIEW with module Term := Term,
5
+
): (Signatures.JUDGMENT_VIEW with module Term := Term and module Judgment := Judgment) => {
6
+
module TermView = TermView
7
+
type props = {
8
+
judgment: Judgment.t,
9
+
scope: array<Term.meta>,
10
+
}
11
+
let make = ({judgment, scope}) => TermView.make({term: judgment, scope})
12
+
}
+4
-4
tests/RuleTest.res
+4
-4
tests/RuleTest.res
···
42
42
// vars: [],
43
43
// premises: [],
44
44
// conclusion: StringSExp.Compound(
45
-
// [StringAtom.Var({idx: 0})],
46
-
// SExp.pAtom("p")->StringAtomJudgment.ConstS->StringSExp.Atom,
45
+
// [StringA.Atom.Var({idx: 0})],
46
+
// SExp.pAtom("p")->StringA.AtomJudgment.ConstS->StringSymbolic.Atom,
47
47
// ),
48
48
// },
49
49
// ],
50
50
// conclusion: (
51
-
// [StringAtom.String("("), StringAtom.Var({idx: 0}), StringAtom.String(")")],
52
-
// SExp.pAtom("p")->StringAtomJudgment.ConstS->StringSExp.Atom,
51
+
// [StringA.Atom.String("("), StringA.Atom.Var({idx: 0}), StringA.Atom.String(")")],
52
+
// SExp.pAtom("p")->StringA.AtomJudgment.ConstS->StringSymbolic.Atom,
53
53
// ),
54
54
// },
55
55
// )
+2
tests/SExpTest.res
+2
tests/SExpTest.res
+2
-2
tests/StringTermTest.res
+2
-2
tests/StringTermTest.res
···
1
1
open Zora
2
2
3
-
module Util = TestUtil.MakeAtomTester(StringAtom)
3
+
module Util = TestUtil.MakeAtomTester(StringA.Atom)
4
4
module ParseUtil = Util.ParseTester
5
5
6
6
zoraBlock("parse", t => {
···
41
41
})
42
42
43
43
let parse = (input: string) =>
44
-
StringAtom.parse(input, ~scope=[], ~gen=Util.ParseWrapper.makeGen())->Result.getExn->Pair.first
44
+
StringA.Atom.parse(input, ~scope=[], ~gen=Util.ParseWrapper.makeGen())->Result.getExn->Pair.first
45
45
46
46
module UnifyUtil = Util.UnifyTester
47
47