forked from
liamoc.net/holbert-ng
the next generation of the in-browser educational proof assistant
HOTerm atom fixes
the diff is unfortunately really noisy because functorising certain
stuff has really confused the algorithm.
three main things:
- lowering atoms where needed in substitutions (which requires
collecting `allowed` indices via `strip`)
- small bug fix in pattern match in `unifyTerm`
- functorising the other HOTerm stuff
on functorising: i chose _not_ to destructively constrain `Atom`
so that the `Atom` arg doesn't need to be passed around everywhere. not
sure if that's best practice, happy to add it back as a destructive
constraint if preferred.
currently, substitution is still broken in the UI. i expect that there's
a place a `reduce` needs to be added, just not sure where.
+299
-277
+31
index.html
+31
index.html
···
307
307
-------- sucnatt
308
308
(natt x (S n))
309
309
</hol-inductive>
310
+
<hol-inductive id="index.html/mexp-hol" deps="index.html/myconfig">
311
+
---- M-Empty
312
+
(M "")
313
+
s.
314
+
(M "$s")
315
+
-------- M-Surround
316
+
(M "( $s )")
317
+
s1.s2.
318
+
(M "$s1")
319
+
(M "$s2")
320
+
--------- M-Juxtapose
321
+
(M "$s1 $s2")
322
+
s.
323
+
(L "$s")
324
+
-------- N-Surr
325
+
(N "( $s )")
326
+
327
+
---- L-Empty
328
+
(L "")
329
+
s1.s2.
330
+
(N "$s1")
331
+
(L "$s2")
332
+
--------- L-Juxtapose
333
+
(L "$s1 $s2")
334
+
</hol-inductive>
335
+
<hol-proof id="index.html/lexp-n-hol" deps="index.html/myconfig index.html/mexp-hol">
336
+
s. (N "$s")
337
+
--------N-L
338
+
(L "$s")
339
+
s. sn |- ?
340
+
</hol-proof>
310
341
<hol-comp id="index.html/baz" deps="index.html/myconfig">
311
342
x.y.
312
343
(/\ x y)
+46
-67
src/HOTerm.res
+46
-67
src/HOTerm.res
···
3
3
let cmp = Pervasives.compare
4
4
})
5
5
6
-
module type ATOM = AtomDef.ATOM
7
-
8
-
module DefaultAtom = {
9
-
module Base = AtomBase.Make({
10
-
type t = string
11
-
})
12
-
type t = string
13
-
type subst = Map.t<int, string>
14
-
let unify = (a, b, ~gen as _=?) =>
15
-
if a == b {
16
-
Seq.once(Map.make())
17
-
} else {
18
-
Seq.empty
19
-
}
20
-
let prettyPrint = (name, ~scope as _: array<string>) => name
21
-
let symbolRegexpString = "^([^\\s()]+)"
22
-
let parse = (str0, ~scope as _: array<string>, ~gen as _=?) => {
23
-
let str = str0->String.trimStart
24
-
let re = RegExp.fromStringWithFlags(symbolRegexpString, ~flags="y")
25
-
switch re->RegExp.exec(str) {
26
-
| None => Error("invalid symbol")
27
-
| Some(res) =>
28
-
switch RegExp.Result.matches(res) {
29
-
| [name] => Ok((name, String.sliceToEnd(str, ~start=RegExp.lastIndex(re))))
30
-
| _ => Error("invalid symbol")
31
-
}
32
-
}
33
-
}
34
-
let substitute = (name, _) => name
35
-
let substDeBruijn = (name, _, ~from as _=?) => name
36
-
let concrete = _ => true
37
-
let upshift = (t, _, ~from as _=?) => t
38
-
let coerce = _ => None
39
-
let reduce = t => t
40
-
}
41
-
42
-
module Make = (Atom: AtomDef.ATOM): {
6
+
module type S = {
7
+
module Atom: AtomDef.ATOM_CHOICE
43
8
type rec t =
44
9
| Symbol({name: Atom.t, constructor: bool})
45
10
| Var({idx: int})
···
64
29
let unifyTerm: (t, t, subst, ~gen: option<gen>) => Seq.t<subst>
65
30
let reduceSubst: subst => subst
66
31
let rewrite: (t, t, t, ~subst: subst, ~gen: option<gen>) => (subst, t)
67
-
} => {
32
+
let isEqualityAtom: Atom.t => bool
33
+
}
34
+
35
+
module Make = (Atom: AtomDef.ATOM_CHOICE): (S with module Atom = Atom) => {
36
+
module Atom = Atom
68
37
type rec t =
69
38
| Symbol({name: Atom.t, constructor: bool})
70
39
| Var({idx: int})
···
245
214
assert(subst->Belt.Map.Int.has(schematic) == false)
246
215
subst->Belt.Map.Int.set(schematic, term)
247
216
}
217
+
let rec strip = (term: t): (t, array<t>) => {
218
+
switch term {
219
+
| App({func, arg}) =>
220
+
let (peeledFunc, peeledArgs) = strip(func)
221
+
(peeledFunc, Array.concat(peeledArgs, [arg]))
222
+
| _ => (term, [])
223
+
}
224
+
}
225
+
let lower = (term: t): option<Atom.t> =>
226
+
switch term {
227
+
| Symbol(s) => Some(s.name)
228
+
| Var({idx}) => Atom.coerce(AtomBase.VarBase.wrap(Var({idx: idx})))
229
+
| _ =>
230
+
switch strip(term) {
231
+
| (Schematic({schematic}), ts) =>
232
+
ts
233
+
->Array.map(t =>
234
+
switch t {
235
+
| Var({idx}) => Some(idx)
236
+
| _ => None
237
+
}
238
+
)
239
+
->Util.Option.sequence
240
+
->Option.flatMap(allowed =>
241
+
Atom.coerce(AtomBase.VarBase.wrap(Schematic({schematic, allowed})))
242
+
)
243
+
| _ => None
244
+
}
245
+
}
248
246
let rec substitute = (term: t, subst: subst) =>
249
247
switch term {
250
248
| Schematic({schematic, _}) =>
···
264
262
arg: substitute(arg, subst),
265
263
})
266
264
| Symbol({name, constructor}) => {
267
-
let symbolSubst = subst->Belt.Map.Int.reduce(Map.make(), (acc, k, v) => {
268
-
switch v {
269
-
| Symbol({name}) => {
270
-
acc->Map.set(k, name)
271
-
acc
272
-
}
273
-
| _ => acc
274
-
}
265
+
let symbolSubst = Map.make()
266
+
subst->Belt.Map.Int.forEach((k, v) => {
267
+
lower(v)->Option.map(v => Map.set(symbolSubst, k, v))->ignore
275
268
})
276
269
Symbol({name: Atom.substitute(name, symbolSubst), constructor})
277
270
}
···
282
275
switch term {
283
276
| Symbol({name, constructor}) =>
284
277
Symbol({
285
-
name: Atom.substDeBruijn(
286
-
name,
287
-
substs->Array.map(t =>
288
-
switch t {
289
-
| Symbol({name}) => Some(name)
290
-
| _ => None
291
-
}
292
-
),
293
-
~from,
294
-
),
278
+
name: Atom.substDeBruijn(name, substs->Array.map(lower), ~from),
295
279
constructor,
296
280
})
297
281
| Var({idx: var}) =>
···
400
384
let lam = (is: array<t>, g: t, js: array<t>): t => {
401
385
lams(is->Array.length, app(g, js->Array.map(j => idx1'(is, j))))
402
386
}
403
-
let rec strip = (term: t): (t, array<t>) => {
404
-
switch term {
405
-
| App({func, arg}) =>
406
-
let (peeledFunc, peeledArgs) = strip(func)
407
-
(peeledFunc, Array.concat(peeledArgs, [arg]))
408
-
| _ => (term, [])
409
-
}
410
-
}
411
387
let rec devar = (subst: subst, term: t): t => {
412
388
let (func, args) = strip(term)
413
389
switch func {
···
570
546
}
571
547
| ((a, xs), (b, ys)) =>
572
548
switch (a, b) {
573
-
| (Symbol(_) | Var(_), Symbol(_) | Var(_)) =>
549
+
| (Symbol(_), Symbol(_)) | (Var(_), Var(_)) =>
574
550
unifyTerm(a, b, subst, ~gen)->Seq.flatMap(subst => unifyArray(xs, ys, subst, ~gen))
575
551
| _ => Seq.empty
576
552
}
···
630
606
Array.fromInitializer(~length=Array.length(scope), i => Var({idx: i})),
631
607
)
632
608
609
+
let isEqualityAtom = (AtomBase.AnyValue(tag, v): Atom.t): bool =>
610
+
switch tag {
611
+
| Symbolic.Base.Tag => v == "="
612
+
| _ => false
613
+
}
633
614
let prettyPrintVar = (idx: int, scope: array<string>) =>
634
615
switch scope[idx] {
635
616
| Some(n) if Array.indexOf(scope, n) == idx => n
···
874
855
}
875
856
let mapTerms = (t, f) => f(t)
876
857
}
877
-
878
-
include Make(DefaultAtom)
+4
-30
src/HOTerm.resi
+4
-30
src/HOTerm.resi
···
1
-
module type ATOM = AtomDef.ATOM
2
-
3
-
module Make: (Atom: AtomDef.ATOM) =>
4
-
{
1
+
module type S = {
2
+
module Atom: AtomDef.ATOM_CHOICE
5
3
type rec t =
6
4
| Symbol({name: Atom.t, constructor: bool})
7
5
| Var({idx: int})
···
26
24
let unifyTerm: (t, t, subst, ~gen: option<gen>) => Seq.t<subst>
27
25
let reduceSubst: subst => subst
28
26
let rewrite: (t, t, t, ~subst: subst, ~gen: option<gen>) => (subst, t)
27
+
let isEqualityAtom: Atom.t => bool
29
28
}
30
29
31
-
type rec t =
32
-
| Symbol({name: string, constructor: bool})
33
-
| Var({idx: int})
34
-
| Schematic({schematic: int})
35
-
| Lam({name: string, body: t})
36
-
| App({func: t, arg: t})
37
-
// Unallowed is used internally in unify, where Nipkow 1993 uses Var(-infinity)
38
-
| Unallowed
39
-
40
-
include Signatures.TERM
41
-
with type t := t
42
-
and type meta = string
43
-
and type schematic = int
44
-
and type subst = Belt.Map.Int.t<t>
45
-
46
-
let emptySubst: subst
47
-
let strip: t => (t, array<t>)
48
-
let app: (t, array<t>) => t
49
-
let mkvars: int => array<t>
50
-
let mapTerms: (t, t => t) => t
51
-
// exposed for testing purposes
52
-
exception UnifyFail(string)
53
-
let substAdd: (subst, schematic, t) => subst
54
-
let unifyTerm: (t, t, subst, ~gen: option<gen>) => Seq.t<subst>
55
-
let reduceSubst: subst => subst
56
-
let rewrite: (t, t, t, ~subst: subst, ~gen: option<gen>) => (subst, t)
30
+
module Make: (Atom: AtomDef.ATOM_CHOICE) => (S with module Atom = Atom)
-6
src/HOTermJView.res
-6
src/HOTermJView.res
-1
src/HOTermJView.resi
-1
src/HOTermJView.resi
···
1
-
include Signatures.JUDGMENT_VIEW with module Term := HOTerm and module Judgment := HOTerm
+24
-10
src/HOTermMethod.res
+24
-10
src/HOTermMethod.res
···
2
2
open Method
3
3
4
4
module MakeRewriteHOTerm = (
5
+
HOTerm: HOTerm.S,
5
6
Judgment: JUDGMENT with module Term := HOTerm and type t = HOTerm.t,
6
7
Config: {
7
8
let keyword: string
···
16
17
let extractEqualityTermsFromJudgment = (judgment: Judgment.t): option<(HOTerm.t, HOTerm.t)> => {
17
18
let term: HOTerm.t = judgment
18
19
switch HOTerm.strip(term) {
19
-
| (HOTerm.Symbol({name: "="}), args) if Array.length(args) == 2 =>
20
+
| (HOTerm.Symbol({name}), args) if HOTerm.isEqualityAtom(name) && Array.length(args) == 2 =>
20
21
Some((args->Array.getUnsafe(0), args->Array.getUnsafe(1)))
21
22
| _ => None
22
23
}
···
247
248
}
248
249
249
250
module Rewrite = (
251
+
HOTerm: HOTerm.S,
250
252
Judgment: JUDGMENT with module Term := HOTerm and type t = HOTerm.t,
251
253
) => MakeRewriteHOTerm(
254
+
HOTerm,
252
255
Judgment,
253
256
{
254
257
let keyword = "rewrite"
···
257
260
)
258
261
259
262
module RewriteReverse = (
263
+
HOTerm: HOTerm.S,
260
264
Judgment: JUDGMENT with module Term := HOTerm and type t = HOTerm.t,
261
265
) => MakeRewriteHOTerm(
266
+
HOTerm,
262
267
Judgment,
263
268
{
264
269
let keyword = "rewrite_reverse"
···
266
271
},
267
272
)
268
273
269
-
module ConstructorNeq = (Judgment: JUDGMENT with module Term := HOTerm and type t = HOTerm.t) => {
274
+
module ConstructorNeq = (
275
+
HOTerm: HOTerm.S,
276
+
Judgment: JUDGMENT with module Term := HOTerm and type t = HOTerm.t,
277
+
) => {
270
278
module Term = HOTerm
271
279
module Rule = Rule.Make(HOTerm, Judgment)
272
280
module Context = Context(HOTerm, Judgment)
···
278
286
let constructorHead = (term: HOTerm.t): option<constructorHead> => {
279
287
let (head, args) = HOTerm.strip(term)
280
288
switch head {
281
-
| HOTerm.Symbol({name, constructor: true}) => Some({name, args})
289
+
| HOTerm.Symbol({name: AtomBase.AnyValue(Symbolic.Base.Tag, name), constructor: true}) =>
290
+
Some({name, args})
282
291
| _ => None
283
292
}
284
293
}
···
291
300
)> => {
292
301
let (head, args) = HOTerm.strip(term)
293
302
switch head {
294
-
| HOTerm.Symbol({name: "="}) if Array.length(args) == 2 =>
303
+
| HOTerm.Symbol({name: AtomBase.AnyValue(Symbolic.Base.Tag, "=")}) if Array.length(args) == 2 =>
295
304
switch (
296
305
constructorHead(args->Array.getUnsafe(0)),
297
306
constructorHead(args->Array.getUnsafe(1)),
···
309
318
| Some((lhs, rhs)) => Some({lhs, rhs, negated: false})
310
319
| None =>
311
320
switch HOTerm.strip(reduced) {
312
-
| (HOTerm.Symbol({name: "not"}), [inner]) =>
321
+
| (HOTerm.Symbol({name: AtomBase.AnyValue(Symbolic.Base.Tag, "not")}), [inner]) =>
313
322
extractConstructorEqualityFrom(inner)->Option.map(((lhs, rhs)) => {lhs, rhs, negated: true})
314
323
| _ => None
315
324
}
···
352
361
}
353
362
}
354
363
355
-
module ConstructorInj = (Judgment: JUDGMENT with module Term := HOTerm and type t = HOTerm.t) => {
364
+
module ConstructorInj = (
365
+
HOTerm: HOTerm.S,
366
+
Judgment: JUDGMENT with module Term := HOTerm and type t = HOTerm.t,
367
+
) => {
356
368
module Rule = Rule.Make(HOTerm, Judgment)
357
369
module Context = Context(HOTerm, Judgment)
358
370
module Results = MethodResults(HOTerm)
···
416
428
let (lHead, lArgs) = args->Array.getUnsafe(0)->HOTerm.strip
417
429
let (rHead, rArgs) = args->Array.getUnsafe(1)->HOTerm.strip
418
430
switch (lHead, rHead) {
419
-
| (HOTerm.Symbol({name: ln, constructor: true}), HOTerm.Symbol({name: rn, constructor: true}))
420
-
if ln == rn && lArgs->Array.length == rArgs->Array.length =>
431
+
| (
432
+
HOTerm.Symbol({name: AtomBase.AnyValue(Symbolic.Base.Tag, ln), constructor: true}),
433
+
HOTerm.Symbol({name: AtomBase.AnyValue(Symbolic.Base.Tag, rn), constructor: true}),
434
+
) if ln == rn && lArgs->Array.length == rArgs->Array.length =>
421
435
Some((ln, lArgs, rArgs))
422
436
| _ => None
423
437
}
···
427
441
let apply = (ctx: Context.t, j: Judgment.t, _gen: HOTerm.gen, _f: Rule.t => 'a) => {
428
442
let ret = Dict.make()
429
443
switch j->Judgment.reduce->HOTerm.strip {
430
-
| (HOTerm.Symbol({name: "="}), [lhs, rhs]) =>
444
+
| (HOTerm.Symbol({name}), [lhs, rhs]) if HOTerm.isEqualityAtom(name) =>
431
445
ctx
432
446
->Context.facts
433
447
->Dict.forEachWithKey((fact, name) => {
···
452
466
let check = (it: t<'a>, ctx: Context.t, goal: Judgment.t, _f: ('a, Rule.t) => 'b) => {
453
467
switch (ctx->Context.facts->Dict.get(it.source), goal->Judgment.reduce->HOTerm.strip) {
454
468
| (None, _) => Error(`Cannot find equality '${it.source}'`)
455
-
| (Some(fact), (HOTerm.Symbol({name: "="}), [lhs, rhs])) =>
469
+
| (Some(fact), (HOTerm.Symbol({name}), [lhs, rhs])) if HOTerm.isEqualityAtom(name) =>
456
470
switch extractConstructorEquality(fact.conclusion) {
457
471
| None => Error(`'${it.source}' is not a constructor equality`)
458
472
| Some((_cName, lArgs, rArgs)) =>
+80
-74
src/HOTermView.res
+80
-74
src/HOTermView.res
···
1
1
open Util
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)}
2
+
module Make = (
3
+
Atom: AtomDef.ATOM_CHOICE,
4
+
AtomView: AtomDef.ATOM_VIEW with module Atom := Atom,
5
+
HOTerm: HOTerm.S with module Atom := Atom,
6
+
) => {
7
+
type idx_props = {idx: int, scope: array<string>}
8
+
let viewVar = (props: idx_props) =>
9
+
switch props.scope[props.idx] {
10
+
| Some(n) if Array.indexOf(props.scope, n) == props.idx =>
11
+
<span className="term-metavar"> {React.string(n)} </span>
12
+
| _ =>
13
+
<span className="term-metavar-unnamed">
14
+
{React.string("\\")}
15
+
{React.int(props.idx)}
16
+
</span>
17
+
}
18
+
19
+
let makeMeta = (str: string) =>
20
+
<span className="rule-binder">
21
+
{React.string(str)}
22
+
{React.string(".")}
11
23
</span>
12
-
}
13
24
14
-
let makeMeta = (str: string) =>
15
-
<span className="rule-binder">
16
-
{React.string(str)}
17
-
{React.string(".")}
18
-
</span>
25
+
let parenthesise = f =>
26
+
[
27
+
<span className="symbol" key={"-1"}> {React.string("(")} </span>,
28
+
...f,
29
+
<span className="symbol" key={"-2"}> {React.string(")")} </span>,
30
+
]
19
31
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 =>
28
-
a->Array.flatMapWithIndex((e, i) =>
29
-
if i == 0 {
30
-
[e]
31
-
} else {
32
-
[React.string(" "), e]
33
-
}
34
-
)
35
-
type props1 = {term: HOTerm.t, scope: array<string>, brackets: bool}
36
-
@react.componentWithProps
37
-
let rec make1 = ({term, scope, brackets}) =>
38
-
switch term {
39
-
| Var({idx}) => viewVar({idx, scope})
40
-
| Symbol({name: s}) => <span className="term-const"> {React.string(s)} </span>
41
-
| Schematic({schematic: s}) =>
42
-
<span className="term-schematic">
43
-
{React.string("?")}
44
-
{React.int(s)}
45
-
</span>
46
-
| App(_) =>
47
-
switch HOTerm.strip(term) {
48
-
| (Symbol({name: "="}), args) if Array.length(args) == 2 =>
49
-
<span className="term-equality">
50
-
{React.createElement(make1, {term: args->Array.getUnsafe(0), scope, brackets: true})}
51
-
{React.string("=")}
52
-
{React.createElement(make1, {term: args->Array.getUnsafe(1), scope, brackets: true})}
53
-
</span>
54
-
| (func, args) =>
55
-
let xs = Array.concat([func], args)
56
-
let a =
57
-
<span className="term-app">
58
-
{xs
59
-
->Array.mapWithIndex((t, i) =>
60
-
React.createElement(make1, withKey({term: t, scope, brackets: true}, i))
61
-
)
62
-
->intersperse
63
-
->React.array}
64
-
</span>
65
-
if brackets {
66
-
[a]->parenthesise->React.array
32
+
let intersperse = a =>
33
+
a->Array.flatMapWithIndex((e, i) =>
34
+
if i == 0 {
35
+
[e]
67
36
} else {
68
-
a
37
+
[React.string(" "), e]
69
38
}
70
-
}
71
-
| Lam({name, body}) => {
72
-
let newScope = Array.concat([name], scope)
73
-
<span className="term-lambda">
74
-
{React.string(name)}
75
-
{React.createElement(make1, {term: body, scope: newScope, brackets: false})}
39
+
)
40
+
type props1 = {term: HOTerm.t, scope: array<string>, brackets: bool}
41
+
@react.componentWithProps
42
+
let rec make1 = ({term, scope, brackets}) =>
43
+
switch term {
44
+
| Var({idx}) => viewVar({idx, scope})
45
+
| Symbol({name: s}) => <span className="term-const"> {AtomView.make({atom: s, scope})} </span>
46
+
| Schematic({schematic: s}) =>
47
+
<span className="term-schematic">
48
+
{React.string("?")}
49
+
{React.int(s)}
76
50
</span>
51
+
| App(_) =>
52
+
switch HOTerm.strip(term) {
53
+
| (Symbol({name: s}), args) if HOTerm.isEqualityAtom(s) && Array.length(args) == 2 =>
54
+
<span className="term-equality">
55
+
{React.createElement(make1, {term: args->Array.getUnsafe(0), scope, brackets: true})}
56
+
{React.string("=")}
57
+
{React.createElement(make1, {term: args->Array.getUnsafe(1), scope, brackets: true})}
58
+
</span>
59
+
| (func, args) =>
60
+
let xs = Array.concat([func], args)
61
+
let a =
62
+
<span className="term-app">
63
+
{xs
64
+
->Array.mapWithIndex((t, i) =>
65
+
React.createElement(make1, withKey({term: t, scope, brackets: true}, i))
66
+
)
67
+
->intersperse
68
+
->React.array}
69
+
</span>
70
+
if brackets {
71
+
[a]->parenthesise->React.array
72
+
} else {
73
+
a
74
+
}
75
+
}
76
+
| Lam({name, body}) => {
77
+
let newScope = Array.concat([name], scope)
78
+
<span className="term-lambda">
79
+
{React.string(name)}
80
+
{React.createElement(make1, {term: body, scope: newScope, brackets: false})}
81
+
</span>
82
+
}
83
+
| Unallowed => <p> {React.string("Internal error: unallowed")} </p>
77
84
}
78
-
| Unallowed => <p> {React.string("Internal error: unallowed")} </p>
79
-
}
80
-
type props = {term: HOTerm.t, scope: array<string>}
81
-
@react.componentWithProps
82
-
let make = ({term, scope}) => make1({term, scope, brackets: false})
85
+
type props = {term: HOTerm.t, scope: array<string>}
86
+
@react.componentWithProps
87
+
let make = ({term, scope}) => make1({term, scope, brackets: false})
88
+
}
+5
-1
src/HOTermView.resi
+5
-1
src/HOTermView.resi
+15
-9
src/InductiveSet.res
+15
-9
src/InductiveSet.res
···
3
3
4
4
// InductiveSet is specific to HOTerm to allow pattern matching on term structure
5
5
module Make = (
6
-
Term: TERM with type t = HOTerm.t and type meta = string,
7
-
Judgment: JUDGMENT with module Term := Term and type t = HOTerm.t,
6
+
Term: HOTerm.S,
7
+
Judgment: JUDGMENT with module Term := Term and type t = Term.t,
8
8
JudgmentView: JUDGMENT_VIEW with module Term := Term and module Judgment := Judgment,
9
9
) => {
10
+
module HOTerm = Term
10
11
module Rule = Rule.Make(Term, Judgment)
11
12
module RuleView = RuleView.Make(Term, Judgment, JudgmentView)
12
13
module Ports = Ports(Term, Judgment)
···
31
32
let extractPredicateSignature = (rule: Rule.t): option<(string, int)> => {
32
33
let (head, args) = HOTerm.strip(rule.conclusion)
33
34
switch head {
34
-
| Symbol({name}) => Some((name, Array.length(args)))
35
+
| Symbol({name: AtomBase.AnyValue(Symbolic.Base.Tag, name)}) => Some((name, Array.length(args)))
35
36
| _ => None
36
37
}
37
38
}
···
64
65
let generateInductiveHypothesis = (premise: Rule.t, offset: int): option<Rule.t> => {
65
66
let (head, args) = HOTerm.strip(premise.conclusion)
66
67
switch head {
67
-
| Symbol({name}) =>
68
+
| Symbol({name: AtomBase.AnyValue(Symbolic.Base.Tag, name)}) =>
68
69
let formerIndex = findFormerIndex(name, Array.length(args))
69
70
Some({
70
71
Rule.vars: premise.vars,
···
87
88
88
89
let (conclusionHead, conclusionArgs) = HOTerm.strip(constructorRule.conclusion)
89
90
let typeIndex = switch conclusionHead {
90
-
| Symbol({name}) => findFormerIndex(name, Array.length(conclusionArgs))
91
+
| Symbol({name: AtomBase.AnyValue(Symbolic.Base.Tag, name)}) =>
92
+
findFormerIndex(name, Array.length(conclusionArgs))
91
93
| _ => throw(Util.Unreachable("Constructor conclusion must have a Symbol head"))
92
94
}
93
95
···
110
112
{
111
113
Rule.vars: [],
112
114
premises: [],
113
-
conclusion: HOTerm.app(HOTerm.Symbol({name: str, constructor: false}), makeVarArgs(i)),
115
+
conclusion: HOTerm.app(
116
+
HOTerm.Symbol({name: AtomBase.AnyValue(Symbolic.Base.Tag, str), constructor: false}),
117
+
makeVarArgs(i),
118
+
),
114
119
},
115
120
...subgoals,
116
121
],
···
126
131
let extractInductiveType = (premise: Rule.t): option<(string, int)> => {
127
132
let (head, args) = HOTerm.strip(premise.conclusion)
128
133
switch head {
129
-
| Symbol({name}) => Some((name, Array.length(args)))
134
+
| Symbol({name: AtomBase.AnyValue(Symbolic.Base.Tag, name), constructor: false}) =>
135
+
Some((name, Array.length(args)))
130
136
| _ => None
131
137
}
132
138
}
···
192
198
Rule.vars: [],
193
199
premises: [],
194
200
conclusion: HOTerm.app(
195
-
HOTerm.Symbol({name: "=", constructor: false}),
201
+
HOTerm.Symbol({name: AtomBase.AnyValue(Symbolic.Base.Tag, "="), constructor: false}),
196
202
[HOTerm.Var({idx: offset + idx}), arg],
197
203
),
198
204
}
···
214
220
Rule.vars: [],
215
221
premises: [],
216
222
conclusion: HOTerm.app(
217
-
HOTerm.Symbol({name: str, constructor: false}),
223
+
HOTerm.Symbol({name: Symbolic.Base.wrap(str), constructor: false}),
218
224
makeVarArgs(arity),
219
225
),
220
226
},
+11
-5
src/MethodView.res
+11
-5
src/MethodView.res
···
162
162
}
163
163
}
164
164
165
-
module RewriteView = (Judgment: JUDGMENT with module Term := HOTerm and type t = HOTerm.t) => {
166
-
module Method = Rewrite(Judgment)
165
+
module RewriteView = (
166
+
HOTerm: HOTerm.S,
167
+
Judgment: JUDGMENT with module Term := HOTerm and type t = HOTerm.t,
168
+
) => {
169
+
module Method = Rewrite(HOTerm, Judgment)
167
170
type props<'a> = {
168
171
method: Method.t<'a>,
169
172
scope: array<HOTerm.meta>,
···
203
206
}
204
207
205
208
module RewriteReverseView = (
209
+
HOTerm: HOTerm.S,
206
210
Judgment: JUDGMENT with module Term := HOTerm and type t = HOTerm.t,
207
211
) => {
208
-
module Method = RewriteReverse(Judgment)
212
+
module Method = RewriteReverse(HOTerm, Judgment)
209
213
type props<'a> = {
210
214
method: Method.t<'a>,
211
215
scope: array<HOTerm.meta>,
···
245
249
}
246
250
247
251
module ConstructorNeqView = (
252
+
HOTerm: HOTerm.S,
248
253
Judgment: JUDGMENT with module Term := HOTerm and type t = HOTerm.t,
249
254
) => {
250
-
module Method = ConstructorNeq(Judgment)
255
+
module Method = ConstructorNeq(HOTerm, Judgment)
251
256
type props<'a> = {
252
257
method: Method.t<'a>,
253
258
scope: array<HOTerm.meta>,
···
271
276
}
272
277
273
278
module ConstructorInjView = (
279
+
HOTerm: HOTerm.S,
274
280
Judgment: JUDGMENT with module Term := HOTerm and type t = HOTerm.t,
275
281
) => {
276
-
module Method = ConstructorInj(Judgment)
282
+
module Method = ConstructorInj(HOTerm, Judgment)
277
283
type props<'a> = {
278
284
method: Method.t<'a>,
279
285
scope: array<HOTerm.meta>,
+33
-28
src/Scratch.res
+33
-28
src/Scratch.res
···
1
+
module Symbol = AtomDef.MakeAtomChoiceAndView(
2
+
Symbolic.Atom,
3
+
Symbolic.AtomView,
4
+
AtomDef.EmptyAtomChoice,
5
+
AtomDef.EmptyAtomChoiceView,
6
+
)
7
+
module StringSymbol = AtomDef.MakeAtomChoiceAndView(
8
+
StringA.Atom,
9
+
StringA.AtomView,
10
+
Symbol.Atom,
11
+
Symbol.AtomView,
12
+
)
13
+
module StringNatSymbol = AtomDef.MakeAtomChoiceAndView(
14
+
AssocComm.Nat.Atom,
15
+
AssocComm.Nat.AtomView,
16
+
StringSymbol.Atom,
17
+
StringSymbol.AtomView,
18
+
)
19
+
module Final = AtomDef.MakeAtomChoiceAndView(
20
+
Preludic.Atom,
21
+
Preludic.AtomView,
22
+
StringNatSymbol.Atom,
23
+
StringNatSymbol.AtomView,
24
+
)
25
+
26
+
module HOTerm = HOTerm.Make(StringSymbol.Atom)
27
+
module HOTermView = HOTermView.Make(StringSymbol.Atom, StringSymbol.AtomView, HOTerm)
28
+
29
+
module HOTermJView = TermViewAsJudgmentView.Make(HOTerm, HOTerm, HOTermView)
1
30
module AxiomS = Editable.TextArea(AxiomSet.Make(HOTerm, HOTerm, HOTermJView))
2
31
module InductiveS = Editable.TextArea(InductiveSet.Make(HOTerm, HOTerm, HOTermJView))
3
32
4
33
module EqualityViews = MethodView.CombineMethodView(
5
34
HOTerm,
6
35
HOTerm,
7
-
MethodView.RewriteView(HOTerm),
8
-
MethodView.RewriteReverseView(HOTerm),
36
+
MethodView.RewriteView(HOTerm, HOTerm),
37
+
MethodView.RewriteReverseView(HOTerm, HOTerm),
9
38
)
10
39
module ConstructorEqualityViews = MethodView.CombineMethodView(
11
40
HOTerm,
12
41
HOTerm,
13
42
EqualityViews,
14
-
MethodView.ConstructorNeqView(HOTerm),
43
+
MethodView.ConstructorNeqView(HOTerm, HOTerm),
15
44
)
16
45
module RewritesView = MethodView.CombineMethodView(
17
46
HOTerm,
18
47
HOTerm,
19
48
ConstructorEqualityViews,
20
-
MethodView.ConstructorInjView(HOTerm),
49
+
MethodView.ConstructorInjView(HOTerm, HOTerm),
21
50
)
22
51
module DerivationsOrLemmasView = MethodView.CombineMethodView(
23
52
HOTerm,
···
42
71
module TheoremS = Editable.TextArea(Theorem.Make(HOTerm, HOTerm, HOTermJView, DLRView))
43
72
module ConfS = ConfigBlock.Make(HOTerm, HOTerm)
44
73
45
-
module Symbol = AtomDef.MakeAtomChoiceAndView(
46
-
Symbolic.Atom,
47
-
Symbolic.AtomView,
48
-
AtomDef.EmptyAtomChoice,
49
-
AtomDef.EmptyAtomChoiceView,
50
-
)
51
-
module StringSymbol = AtomDef.MakeAtomChoiceAndView(
52
-
StringA.Atom,
53
-
StringA.AtomView,
54
-
Symbol.Atom,
55
-
Symbol.AtomView,
56
-
)
57
-
module StringNatSymbol = AtomDef.MakeAtomChoiceAndView(
58
-
AssocComm.Nat.Atom,
59
-
AssocComm.Nat.AtomView,
60
-
StringSymbol.Atom,
61
-
StringSymbol.AtomView,
62
-
)
63
-
module Final = AtomDef.MakeAtomChoiceAndView(
64
-
Preludic.Atom,
65
-
Preludic.AtomView,
66
-
StringNatSymbol.Atom,
67
-
StringNatSymbol.AtomView,
68
-
)
69
74
module StringSExp = SExp.Make(Final.Atom)
70
75
module TermView = SExpView.Make(Final.Atom, Final.AtomView, StringSExp)
71
76
module StringSExpJView = TermViewAsJudgmentView.Make(StringSExp, StringSExp, TermView)
+8
src/Util.res
+8
src/Util.res
+40
-44
tests/HOTermTest.res
+40
-44
tests/HOTermTest.res
···
1
1
open Zora
2
-
open HOTerm
3
-
4
-
module Util = TestUtil.MakeTerm(HOTerm)
5
2
6
3
module Symbol = AtomDef.MakeAtomChoiceAndView(
7
4
Symbolic.Atom,
···
9
6
AtomDef.EmptyAtomChoice,
10
7
AtomDef.EmptyAtomChoiceView,
11
8
)
9
+
module RegularHOTerm = HOTerm.Make(Symbol.Atom)
10
+
module Util = TestUtil.MakeTerm(RegularHOTerm)
12
11
module StringSymbol = AtomDef.MakeAtomChoiceAndView(
13
12
StringA.Atom,
14
13
StringA.AtomView,
···
27
26
})
28
27
29
28
let testUnify0 = (t: Zora.t, at: string, bt: string, ~subst=?, ~msg=?, ~reduce=false) => {
30
-
let gen = HOTerm.makeGen()
31
-
let (a, _) = HOTerm.parse(at, ~scope=[], ~gen)->Result.getExn
32
-
let (b, _) = HOTerm.parse(bt, ~scope=[], ~gen)->Result.getExn
29
+
let gen = RegularHOTerm.makeGen()
30
+
let (a, _) = RegularHOTerm.parse(at, ~scope=[], ~gen)->Result.getExn
31
+
let (b, _) = RegularHOTerm.parse(bt, ~scope=[], ~gen)->Result.getExn
33
32
try {
34
-
let res0 = HOTerm.unifyTerm(a, b, HOTerm.emptySubst, ~gen=Some(gen))->Seq.head->Option.getExn
33
+
let res0 =
34
+
RegularHOTerm.unifyTerm(a, b, RegularHOTerm.emptySubst, ~gen=Some(gen))
35
+
->Seq.head
36
+
->Option.getExn
35
37
let res = if reduce {
36
-
HOTerm.reduceSubst(res0)
38
+
RegularHOTerm.reduceSubst(res0)
37
39
} else {
38
40
res0
39
41
}
···
58
60
})
59
61
}
60
62
} catch {
61
-
| HOTerm.UnifyFail(failed) =>
63
+
| RegularHOTerm.UnifyFail(failed) =>
62
64
t->fail(
63
65
~msg="unification failed: " ++
64
66
TestUtil.stringifyExn(a) ++
···
73
75
testUnify0(t, at, bt, ~subst?, ~msg?, ~reduce)
74
76
testUnify0(t, bt, at, ~subst?, ~msg?, ~reduce)
75
77
}
78
+
let s = s => RegularHOTerm.Symbol({name: Symbolic.Base.wrap(s), constructor: false})
76
79
zoraBlock("parse symbol", t => {
77
-
t->block("single char", t => t->Util.testParse("x", Symbol({name: "x", constructor: false})))
78
-
t->block("multi char", t => t->Util.testParse("xyz", Symbol({name: "xyz", constructor: false})))
80
+
t->block("single char", t => t->Util.testParse("x", s("x")))
81
+
t->block("multi char", t => t->Util.testParse("xyz", s("xyz")))
79
82
})
80
83
81
84
zoraBlock("parse var", t => {
···
93
96
t->Util.testParse(
94
97
"(a b)",
95
98
App({
96
-
func: Symbol({name: "a", constructor: false}),
97
-
arg: Symbol({name: "b", constructor: false}),
99
+
func: s("a"),
100
+
arg: s("b"),
98
101
}),
99
102
)
100
103
})
···
103
106
"(a b c)",
104
107
App({
105
108
func: App({
106
-
func: Symbol({name: "a", constructor: false}),
107
-
arg: Symbol({name: "b", constructor: false}),
109
+
func: s("a"),
110
+
arg: s("b"),
108
111
}),
109
-
arg: Symbol({name: "c", constructor: false}),
112
+
arg: s("c"),
110
113
}),
111
114
)
112
115
})
···
114
117
t->Util.testParse(
115
118
"(a \\1 ?1)",
116
119
App({
117
-
func: App({func: Symbol({name: "a", constructor: false}), arg: Var({idx: 1})}),
120
+
func: App({func: s("a"), arg: Var({idx: 1})}),
118
121
arg: Schematic({schematic: 1}),
119
122
}),
120
123
)
···
148
151
)
149
152
})
150
153
t->block("constructor", t => {
151
-
t->Util.testParse("@cons", Symbol({name: "cons", constructor: true}))
154
+
t->Util.testParse("@cons", Symbol({name: Symbolic.Base.wrap("cons"), constructor: true}))
152
155
})
153
156
// TODO: test if remaining strings are returned correctly
154
157
})
···
190
193
)
191
194
})
192
195
t->block("unify string atom", t => {
193
-
let parse = input => t->StringUtil.parse(input)
196
+
let parse = (input, ~scope=[]) => t->StringUtil.parse(input, ~scope)
194
197
let emptySubst = StringHOTerm.emptySubst
195
198
let substAdd = StringHOTerm.substAdd
196
199
t->equal(
···
198
201
Some(emptySubst->substAdd(0, wrapString([String("b")]))),
199
202
)
200
203
t->equal(
204
+
StringHOTerm.unify(parse(`(L "$s")`, ~scope=["s"]), parse(`(L "?0(0) ?1(0)")`))->Seq.toArray,
205
+
[
206
+
emptySubst->substAdd(0, wrapString([]))->substAdd(1, wrapString([Var({idx: 0})])),
207
+
emptySubst->substAdd(0, wrapString([Var({idx: 0})]))->substAdd(1, wrapString([])),
208
+
],
209
+
)
210
+
t->equal(
201
211
StringHOTerm.unify(parse(`(P "?1() a" "?1()")`), parse(`(P "a ?1()" "a")`))->Seq.head,
202
212
Some(emptySubst->substAdd(1, wrapString([String("a")]))),
203
213
)
···
215
225
216
226
zoraBlock("unify test", t => {
217
227
let testUnifyFail = Util.testUnifyFailString
228
+
open RegularHOTerm
218
229
t->block("symbols", t => {
219
230
let x = "x"
220
231
let y = "y"
···
233
244
t->block("flex-rigid", t => {
234
245
let x = "?0"
235
246
let y = "y"
236
-
t->testUnify(x, y, ~subst=emptySubst->substAdd(0, Symbol({name: "y", constructor: false})))
247
+
t->testUnify(x, y, ~subst=RegularHOTerm.emptySubst->RegularHOTerm.substAdd(0, s("y")))
237
248
})
238
249
t->block("flex-rigid2", t => {
239
250
let x = "(x. ?0 x)"
···
247
258
0,
248
259
Lam({
249
260
name: "x",
250
-
body: App({func: Symbol({name: "y", constructor: false}), arg: Var({idx: 0})}),
261
+
body: App({func: s("y"), arg: Var({idx: 0})}),
251
262
}),
252
263
),
253
264
)
254
-
t->testUnify(
255
-
x,
256
-
y,
257
-
~reduce=true,
258
-
~subst=emptySubst->substAdd(0, Symbol({name: "y", constructor: false})),
259
-
)
265
+
t->testUnify(x, y, ~reduce=true, ~subst=emptySubst->substAdd(0, s("y")))
260
266
})
261
267
t->block("flex-rigid3", t => {
262
268
let x = "(?0 \\10)"
263
269
let y = "(fst \\10)"
264
-
t->testUnify(
265
-
x,
266
-
y,
267
-
~reduce=true,
268
-
~subst=emptySubst->substAdd(0, Symbol({name: "fst", constructor: false})),
269
-
)
270
+
t->testUnify(x, y, ~reduce=true, ~subst=emptySubst->substAdd(0, s("fst")))
270
271
})
271
272
t->block("flex-rigid", t => {
272
273
let x = "(?0 \\10)"
···
279
280
Lam({
280
281
name: "x",
281
282
body: App({
282
-
func: Symbol({name: "r", constructor: false}),
283
-
arg: App({func: Symbol({name: "fst", constructor: false}), arg: Var({idx: 0})}),
283
+
func: s("r"),
284
+
arg: App({func: s("fst"), arg: Var({idx: 0})}),
284
285
}),
285
286
}),
286
287
),
···
294
295
y,
295
296
~subst=emptySubst->substAdd(
296
297
0,
297
-
HOTerm.parse("(x. (r (fst x)))", ~scope=[])->Result.getExn->Pair.first,
298
+
RegularHOTerm.parse("(x. (r (fst x)))", ~scope=[])->Result.getExn->Pair.first,
298
299
),
299
300
)
300
301
})
···
306
307
y,
307
308
~subst=emptySubst->substAdd(
308
309
1,
309
-
HOTerm.parse("(x. x. (r (q \\0 \\1)))", ~scope=[])->Result.getExn->Pair.first,
310
+
RegularHOTerm.parse("(x. x. (r (q \\0 \\1)))", ~scope=[])->Result.getExn->Pair.first,
310
311
),
311
312
)
312
313
})
···
318
319
y,
319
320
~subst=emptySubst->substAdd(
320
321
1,
321
-
HOTerm.parse("(x. x. (r (q (snd \\0) \\1)))", ~scope=[])->Result.getExn->Pair.first,
322
+
RegularHOTerm.parse("(x. x. (r (q (snd \\0) \\1)))", ~scope=[])->Result.getExn->Pair.first,
322
323
),
323
324
)
324
325
})
···
357
358
t->testUnifyFail(a, b)
358
359
})
359
360
t->block("eta", t => {
360
-
t->testUnify(
361
-
"(x. ?0 x)",
362
-
"a",
363
-
~reduce=true,
364
-
~subst=emptySubst->substAdd(0, Symbol({name: "a", constructor: false})),
365
-
)
361
+
t->testUnify("(x. ?0 x)", "a", ~reduce=true, ~subst=emptySubst->substAdd(0, s("a")))
366
362
})
367
363
t->block("divergent", _t => {
368
364
let _divergent = "((x. x x) (x. x x))"
+2
-2
tests/TestUtil.res
+2
-2
tests/TestUtil.res
···
205
205
| Error(msg) => t->fail(~msg="parse failed: " ++ msg)
206
206
}
207
207
}
208
-
let parse = (t: Zora.t, input: string): Term.t => {
209
-
let res = Term.parse(input, ~scope=[], ~gen=Term.makeGen())
208
+
let parse = (t: Zora.t, input: string, ~scope=[]): Term.t => {
209
+
let res = Term.parse(input, ~scope, ~gen=Term.makeGen())
210
210
switch res {
211
211
| Ok((term, "")) => term
212
212
| Ok((_, rest)) => {