the next generation of the in-browser educational proof assistant
Merge pull request #23 from joshcbrown/intro-rule-filter
Add ghost term to filter for useful introduction rules
authored by
Liam O'Connor
and committed by
GitHub
e40b6b3a
0a6acbae
+124
-54
+2
src/HOTerm.res
+2
src/HOTerm.res
+11
-1
src/Method.res
+11
-1
src/Method.res
···
139
139
}
140
140
let apply = (ctx: Context.t, j: Judgment.t, gen: Term.gen, f: Rule.t => 'a) => {
141
141
let ret = Dict.make()
142
-
ctx.facts->Dict.forEachWithKey((rule, key) => {
142
+
ctx.facts
143
+
->Dict.toArray
144
+
->Array.filterMap(((key, rule)) => {
143
145
let insts = rule->Rule.genSchemaInsts(gen, ~scope=ctx.fixes)
144
146
let res = rule->Rule.instantiate(insts)
147
+
let ghostSubs = Judgment.unify(Judgment.ghostJudgment, res.conclusion)
148
+
if ghostSubs->Seq.head->Option.isNone {
149
+
Some((key, res, insts))
150
+
} else {
151
+
None
152
+
}
153
+
})
154
+
->Array.forEach(((key, res, insts)) => {
145
155
let substs = Judgment.unify(res.conclusion, j, ~gen)
146
156
substs
147
157
->Seq.take(seqSizeLimit)
+6
src/SExp.res
+6
src/SExp.res
···
8
8
| Compound({subexps: array<t>})
9
9
| Var({idx: int})
10
10
| Schematic({schematic: int, allowed: array<int>})
11
+
| Ghost
11
12
type meta = string
12
13
type schematic = int
13
14
type subst = Map.t<schematic, t>
···
138
139
}
139
140
),
140
141
})
142
+
| Ghost => Ghost
141
143
}
142
144
let rec upshift = (term: t, amount: int, ~from: int=0) =>
143
145
switch term {
···
162
164
}
163
165
),
164
166
})
167
+
| Ghost => Ghost
165
168
}
166
169
let place = (x: int, ~scope: array<string>) => Schematic({
167
170
schematic: x,
···
204
207
"("
205
208
->String.concat(Array.join(subexps->Array.map(e => prettyPrint(e, ~scope)), " "))
206
209
->String.concat(")")
210
+
| Ghost => "§SExp.Ghost"
207
211
}
208
212
209
213
let prettyPrintSubst = (sub, ~scope) => Util.prettyPrintMap(sub, ~showV=t => prettyPrint(t, ~scope))
···
356
360
| Some(e) => Ok((e, cur.contents))
357
361
}
358
362
}
363
+
364
+
let ghostTerm = Ghost
+1
src/SExp.resi
+1
src/SExp.resi
+1
src/SExpView.res
+1
src/SExpView.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
27
28
}
28
29
29
30
module type JUDGMENT = {
···
54
55
) => result<(substCodom, string), string>
55
56
let prettyPrint: (t, ~scope: array<Term.meta>) => string
56
57
let prettyPrintSubstCodom: (substCodom, ~scope: array<Term.meta>) => string
58
+
let ghostJudgment: t
57
59
}
58
60
59
61
module type TERM_VIEW = {
+10
-1
src/StringTerm.res
+10
-1
src/StringTerm.res
···
7
7
| String(string)
8
8
| Var({idx: int})
9
9
| Schematic({schematic: int, allowed: array<int>})
10
+
| Ghost
10
11
type t = array<piece>
11
12
type meta = string
12
13
type schematic = int
···
91
92
| (_, _) => false
92
93
}
93
94
}
95
+
94
96
let rec oneSide = (s, t) => {
95
97
switch (s, t) {
96
98
| ([], []) => [emptySubst]
···
175
177
| None => searchSub(schematic, allowed, Eps)
176
178
| Some(p) =>
177
179
switch p {
178
-
| String(_) =>
180
+
| String(_) | Ghost =>
179
181
Array.concat(
180
182
searchSub(schematic, allowed, PieceLitSub(p)),
181
183
searchSub(schematic, allowed, Eps),
···
297
299
),
298
300
}),
299
301
]
302
+
| Ghost => [Ghost]
300
303
}
301
304
)
302
305
}
···
324
327
}
325
328
),
326
329
})
330
+
| Ghost => Ghost
327
331
}
328
332
})
329
333
···
378
382
->Array.join(" ")
379
383
`?${Int.toString(schematic)}(${allowedStr})`
380
384
}
385
+
| Ghost => "§String.Ghost"
381
386
}
382
387
})->Array.join(" ")}"`
383
388
let prettyPrintMeta = (str: string) => `${str}.`
···
504
509
| String(s) => SExp.Symbol({name: s})
505
510
| Var({idx}) => SExp.Var({idx: idx})
506
511
| Schematic({schematic, allowed}) => SExp.Schematic({schematic, allowed})
512
+
| Ghost => SExp.ghostTerm
507
513
}
508
514
switch Array.length(t) {
509
515
| 1 => convertPiece(t[0]->Option.getExn)
···
517
523
| SExp.Schematic({schematic, allowed}) => [Schematic({schematic, allowed})]
518
524
| SExp.Var({idx}) => [Var({idx: idx})]
519
525
| SExp.Compound({subexps}) => subexps->Array.flatMap(fromSExp)
526
+
| SExp.Ghost => [Ghost]
520
527
}
528
+
529
+
let ghostTerm = [Ghost]
+1
src/StringTerm.resi
+1
src/StringTerm.resi
+2
src/StringTermJudgment.res
+2
src/StringTermJudgment.res
+1
src/StringTermView.res
+1
src/StringTermView.res
+1
src/TermAsJudgment.res
+1
src/TermAsJudgment.res
+8
-7
tests/HOTermTest.res
+8
-7
tests/HOTermTest.res
···
145
145
})
146
146
147
147
zoraBlock("unify test", t => {
148
+
let testUnifyFail = Util.testUnifyFailString
148
149
t->block("symbols", t => {
149
150
let x = "x"
150
151
let y = "y"
151
152
t->testUnify(x, x)
152
-
t->Util.testUnifyFail(y, x)
153
-
t->Util.testUnifyFail(x, y)
153
+
t->testUnifyFail(y, x)
154
+
t->testUnifyFail(x, y)
154
155
})
155
156
t->block("applications", t => {
156
157
let ab = "(a b)"
157
158
let cd = "(c d)"
158
159
t->testUnify(ab, ab)
159
160
t->testUnify(cd, cd)
160
-
t->Util.testUnifyFail(ab, cd)
161
-
t->Util.testUnifyFail(cd, ab)
161
+
t->testUnifyFail(ab, cd)
162
+
t->testUnifyFail(cd, ab)
162
163
})
163
164
t->block("flex-rigid", t => {
164
165
let x = "?0"
···
278
279
let a = "(x. ?0 x)"
279
280
let b = "(x. f (?0 x))"
280
281
// ?0 occurs in the rigid term on the right → should not unify
281
-
t->Util.testUnifyFail(a, b)
282
+
t->testUnifyFail(a, b)
282
283
})
283
284
t->block("no capture", t => {
284
285
let a = "(x. ?0)"
285
286
let b = "(x. x)"
286
287
// Should fail: it cannot capture the bound variable.
287
-
t->Util.testUnifyFail(a, b)
288
+
t->testUnifyFail(a, b)
288
289
})
289
290
t->block("eta", t => {
290
291
t->testUnify(
···
340
341
let a = "(Nat (S ?6))"
341
342
let b = "(Nat (S (S \\0)))"
342
343
let c = "(Nat (S (?6 \\0)))"
343
-
t->Util.testUnifyFail(a, b)
344
+
t->testUnifyFail(a, b)
344
345
t->testUnify(c, b, ~subst=emptySubst->substAdd(6, t->Util.parse("(x. S \\0)")))
345
346
})
346
347
t->block("tests from induction examples", _t => {
+14
-8
tests/SExpTest.res
+14
-8
tests/SExpTest.res
···
50
50
let comp2 = parse("(x a y)")
51
51
let schema1 = parse("?1()")
52
52
let schemaComp = parse("(?1() a ?2())")
53
-
t->block("var eq", t => t->Util.testUnify(x, x, [Map.make()]))
54
-
t->block("var neq", t => t->Util.testUnify(x, y, []))
55
-
t->block("comp eq", t => t->Util.testUnify(comp1, comp1, [Map.make()]))
56
-
t->block("comp neq", t => t->Util.testUnify(comp1, comp2, []))
57
-
t->block("schema var", t => t->Util.testUnify(schema1, x, [Map.fromArray([(1, x)])]))
58
-
t->block("schema comp", t => t->Util.testUnify(schema1, comp2, [Map.fromArray([(1, comp2)])]))
53
+
t->block("var eq", t => t->Util.testUnify(x, x, ~expect=[Map.make()]))
54
+
t->block("var neq", t => t->Util.testUnify(x, y, ~expect=[]))
55
+
t->block("comp eq", t => t->Util.testUnify(comp1, comp1, ~expect=[Map.make()]))
56
+
t->block("comp neq", t => t->Util.testUnify(comp1, comp2, ~expect=[]))
57
+
t->block("schema var", t => t->Util.testUnify(schema1, x, ~expect=[Map.fromArray([(1, x)])]))
58
+
t->block("schema comp", t =>
59
+
t->Util.testUnify(schema1, comp2, ~expect=[Map.fromArray([(1, comp2)])])
60
+
)
59
61
t->block("comp-schema comp eq", t => {
60
-
t->Util.testUnify(schemaComp, comp2, [Map.fromArray([(1, x), (2, y)])])
62
+
t->Util.testUnify(schemaComp, comp2, ~expect=[Map.fromArray([(1, x), (2, y)])])
61
63
})
62
64
t->block("comp-schema comp neq", t => {
63
-
t->Util.testUnify(schemaComp, comp1, [])
65
+
t->Util.testUnify(schemaComp, comp1, ~expect=[])
66
+
})
67
+
t->block("ghost", t => {
68
+
t->Util.testUnifyFail(x, SExp.ghostTerm)
69
+
t->Util.testUnify(schema1, SExp.ghostTerm)
64
70
})
65
71
})
+32
-19
tests/StringTermTest.res
+32
-19
tests/StringTermTest.res
···
45
45
let b = parse(`"b"`)
46
46
let x = parse(`"?1()"`)
47
47
let y = parse(`"?2()"`)
48
+
t->block("ghost", t => {
49
+
t->Util.testUnifyFail(a, StringTerm.ghostTerm)
50
+
t->Util.testUnify(x, StringTerm.ghostTerm)
51
+
t->Util.testUnify([x, y, x]->Array.flat, StringTerm.ghostTerm)
52
+
})
48
53
t->block("schematics on at most one side", t => {
49
-
t->Util.testUnify(a, a, [Map.make()])
50
-
t->Util.testUnify(x, a, [Map.fromArray([(1, a)])])
51
-
t->Util.testUnify(a, x, [Map.fromArray([(1, a)])])
54
+
t->Util.testUnify(a, a, ~expect=[Map.make()])
55
+
t->Util.testUnify(x, a, ~expect=[Map.fromArray([(1, a)])])
56
+
t->Util.testUnify(a, x, ~expect=[Map.fromArray([(1, a)])])
52
57
53
58
let xy = parse(`"?1() ?2()"`)
54
59
let ab = parse(`"a b"`)
55
-
t->Util.testUnify(x, ab, [Map.fromArray([(1, ab)])])
60
+
t->Util.testUnify(x, ab, ~expect=[Map.fromArray([(1, ab)])])
56
61
t->Util.testUnify(
57
62
xy,
58
63
ab,
59
-
[
64
+
~expect=[
60
65
Map.fromArray([(1, []), (2, ab)]),
61
66
Map.fromArray([(1, a), (2, b)]),
62
67
Map.fromArray([(1, ab), (2, [])]),
63
68
],
64
69
)
65
70
66
-
t->Util.testUnify(parse(`"?1() b ?2()"`), ab, [Map.fromArray([(1, a), (2, [])])])
71
+
t->Util.testUnify(parse(`"?1() b ?2()"`), ab, ~expect=[Map.fromArray([(1, a), (2, [])])])
67
72
t->Util.testUnify(
68
73
parse(`"?1() ?2() b"`),
69
74
ab,
70
-
[Map.fromArray([(1, []), (2, a)]), Map.fromArray([(1, a), (2, [])])],
75
+
~expect=[Map.fromArray([(1, []), (2, a)]), Map.fromArray([(1, a), (2, [])])],
71
76
)
72
77
t->Util.testUnify(
73
78
parse(`"a ?1() ?2()"`),
74
79
ab,
75
-
[Map.fromArray([(1, []), (2, b)]), Map.fromArray([(1, b), (2, [])])],
80
+
~expect=[Map.fromArray([(1, []), (2, b)]), Map.fromArray([(1, b), (2, [])])],
76
81
)
77
82
78
83
let xax = parse(`"?1() a ?1()"`)
79
-
t->Util.testUnify(xax, parse(`"a"`), [Map.fromArray([(1, [])])])
80
-
t->Util.testUnify(xax, parse(`"a a a"`), [Map.fromArray([(1, a)])])
81
-
t->Util.testUnify(xax, parse(`"a b a a b"`), [Map.fromArray([(1, parse(`"a b"`))])])
84
+
t->Util.testUnify(xax, parse(`"a"`), ~expect=[Map.fromArray([(1, [])])])
85
+
t->Util.testUnify(xax, parse(`"a a a"`), ~expect=[Map.fromArray([(1, a)])])
86
+
t->Util.testUnify(xax, parse(`"a b a a b"`), ~expect=[Map.fromArray([(1, parse(`"a b"`))])])
82
87
})
83
88
84
89
t->block("schematics appearing at most twice", t => {
85
-
t->Util.testUnify(x, x, [Map.fromArray([(1, [])])])
86
-
t->Util.testUnify(x, y, [Map.fromArray([(1, []), (2, [])])])
90
+
t->Util.testUnify(x, x, ~expect=[Map.fromArray([(1, [])])])
91
+
t->Util.testUnify(x, y, ~expect=[Map.fromArray([(1, []), (2, [])])])
87
92
88
-
t->Util.testUnify(a, parse(`"?1() a"`), [Map.fromArray([(1, [])])])
93
+
t->Util.testUnify(a, parse(`"?1() a"`), ~expect=[Map.fromArray([(1, [])])])
89
94
t->Util.testUnify(
90
95
parse(`"?1() a"`),
91
96
parse(`"a ?1()"`),
92
-
[
97
+
~expect=[
93
98
Map.fromArray([(1, [])]),
94
99
Map.fromArray([(1, parse(`"a"`))]),
95
100
Map.fromArray([(1, parse(`"a a"`))]),
···
97
102
Map.fromArray([(1, parse(`"a a a a"`))]),
98
103
],
99
104
)
100
-
t->Util.testUnify(parse(`"a ?1()"`), parse(`"?2() b`), [Map.fromArray([(1, b), (2, a)])])
101
-
t->Util.testUnify(parse(`"a ?1() a"`), parse(`"?2() b a"`), [Map.fromArray([(1, b), (2, a)])])
105
+
t->Util.testUnify(
106
+
parse(`"a ?1()"`),
107
+
parse(`"?2() b`),
108
+
~expect=[Map.fromArray([(1, b), (2, a)])],
109
+
)
110
+
t->Util.testUnify(
111
+
parse(`"a ?1() a"`),
112
+
parse(`"?2() b a"`),
113
+
~expect=[Map.fromArray([(1, b), (2, a)])],
114
+
)
102
115
t->Util.testUnify(
103
116
parse(`"b ?1() a"`),
104
117
parse(`"?2() a ?1()"`),
105
-
[Map.fromArray([(1, a), (2, b)]), Map.fromArray([(1, []), (2, b)])],
118
+
~expect=[Map.fromArray([(1, a), (2, b)]), Map.fromArray([(1, []), (2, b)])],
106
119
)
107
120
t->Util.testUnify(
108
121
parse(`"a b ?1() c ?2()"`),
109
122
parse(`"?2() c ?1() b a"`),
110
-
[Map.fromArray([(1, a), (2, parse(`"a b a"`))])],
123
+
~expect=[Map.fromArray([(1, a), (2, parse(`"a b a"`))])],
111
124
)
112
125
})
113
126
})
+32
-18
tests/TestUtil.res
+32
-18
tests/TestUtil.res
···
98
98
ss->Array.map(t => Term.prettyPrintSubst(t, ~scope=[]))->Util.showArray
99
99
}
100
100
101
-
let testUnify = (t: Zora.t, t1: Term.t, t2: Term.t, expect: array<Term.subst>, ~msg=?) => {
102
-
let expect = Seq.fromArray(expect)
101
+
let testUnify = (
102
+
t: Zora.t,
103
+
t1: Term.t,
104
+
t2: Term.t,
105
+
~expect: option<array<Term.subst>>=?,
106
+
~msg=?,
107
+
) => {
103
108
let res = Term.unify(t1, t2)->Seq.take(10)
104
-
// Console.log(
105
-
// `t1: ${Term.prettyPrint(t1, ~scope=[])} t2:${Term.prettyPrint(t2, ~scope=[])}\nsubsts: ${res
106
-
// ->Seq.map(t => Term.prettyPrintSubst(t, ~scope=[]))
107
-
// ->Seq.join(",")}\n`,
108
-
// )
109
-
let noMatches =
110
-
expect
111
-
->Seq.filter(sub1 => Seq.find(res, sub2 => Term.substEqual(sub1, sub2))->Option.isNone)
112
-
->Seq.map(t => Term.prettyPrintSubst(t, ~scope=[]))
113
-
->Seq.toArray
114
-
let msg = msg->Option.getOr("each substitution in `expect` should have a match in solutions")
115
-
t->equal(noMatches, [], ~msg)
109
+
switch expect {
110
+
| Some(expect) => {
111
+
let expect = Seq.fromArray(expect)
112
+
let noMatches =
113
+
expect
114
+
->Seq.filter(sub1 => Seq.find(res, sub2 => Term.substEqual(sub1, sub2))->Option.isNone)
115
+
->Seq.map(t => Term.prettyPrintSubst(t, ~scope=[]))
116
+
->Seq.toArray
117
+
let msg =
118
+
msg->Option.getOr("each substitution in `expect` should have a match in solutions")
119
+
t->equal(noMatches, [], ~msg)
120
+
}
121
+
| None => {
122
+
let msg = msg->Option.getOr("expect non-nil substitution sequence")
123
+
t->ok(res->Seq.head->Option.isSome, ~msg)
124
+
}
125
+
}
116
126
}
117
127
118
-
let testUnifyFail = (t: Zora.t, at: string, bt: string, ~msg=?) => {
119
-
let gen = Term.makeGen()
120
-
let (a, _) = Term.parse(at, ~scope=[], ~gen)->Result.getExn
121
-
let (b, _) = Term.parse(bt, ~scope=[], ~gen)->Result.getExn
128
+
let testUnifyFail = (t: Zora.t, a: Term.t, b: Term.t, ~msg=?) => {
122
129
let res = Term.unify(a, b)
123
130
if res->Seq.length != 0 {
124
131
t->fail(~msg="unification succeeded: " ++ stringifyExn(a) ++ " and " ++ stringifyExn(b))
125
132
} else {
126
133
t->ok(true, ~msg=msg->Option.getOr("unification failed"))
127
134
}
135
+
}
136
+
137
+
let testUnifyFailString = (t: Zora.t, at: string, bt: string, ~msg=?) => {
138
+
let gen = Term.makeGen()
139
+
let (a, _) = Term.parse(at, ~scope=[], ~gen)->Result.getExn
140
+
let (b, _) = Term.parse(bt, ~scope=[], ~gen)->Result.getExn
141
+
testUnifyFail(t, a, b, ~msg?)
128
142
}
129
143
}