the next generation of the in-browser educational proof assistant
Merge pull request #18 from mio-19/main
bug fixes and constructors
authored by
Liam O'Connor
and committed by
GitHub
ddf8c3e9
b378e1fc
+111
-34
+10
index.html
+10
index.html
···
365
365
366
366
</hol-proof>
367
367
368
+
<hol-proof id="index.html/prooftest-elim-bug" deps="index.html/myconfig index.html/baz index.html/nat">
369
+
a.
370
+
(Even a)
371
+
-------
372
+
(Nat a)
373
+
374
+
a. asm |- ?
375
+
376
+
</hol-proof>
377
+
368
378
<hol-proof id="index.html/prooftest" deps="index.html/myconfig index.html/baz index.html/nat">
369
379
a.
370
380
(Nat a)
+37
-11
src/HOTerm.res
+37
-11
src/HOTerm.res
···
5
5
})
6
6
7
7
type rec t =
8
-
| Symbol({name: string})
8
+
| Symbol({name: string, constructor: bool})
9
9
| Var({idx: int})
10
10
| Schematic({schematic: int})
11
11
| Lam({name: string, body: t})
···
369
369
subst: subst,
370
370
~gen: option<gen>,
371
371
): subst => {
372
+
if gen->Option.isNone {
373
+
raise(UnifyFail("no gen provided"))
374
+
}
372
375
if sa == sb {
373
376
if xs->Array.length != ys->Array.length {
374
377
raise(UnifyFail("flexible schematics have different number of arguments"))
375
-
}
376
-
if gen->Option.isNone {
377
-
raise(UnifyFail("no gen provided"))
378
378
}
379
379
let len = xs->Array.length
380
380
let h = Schematic({schematic: fresh(Option.getExn(gen))})
···
516
516
}
517
517
let rec prettyPrint = (it: t, ~scope: array<string>) =>
518
518
switch it {
519
-
| Symbol({name}) => name
519
+
| Symbol({name, constructor}) =>
520
+
if constructor {
521
+
String.concat("@", name)
522
+
} else {
523
+
name
524
+
}
520
525
| Var({idx}) => prettyPrintVar(idx, scope)
521
526
| Schematic({schematic}) => "?"->String.concat(String.make(schematic))
522
527
| Lam(_) =>
···
543
548
let symbolRegexpString = "^([^\\s()]+)"
544
549
let nameRES = "^([^\\s.\\[\\]()]+)\\."
545
550
exception ParseError(string)
546
-
type token = LParen | RParen | VarT(int) | SchematicT(int) | AtomT(string) | NameT(string) | EOF
551
+
type token =
552
+
| LParen
553
+
| RParen
554
+
| VarT(int)
555
+
| SchematicT(int)
556
+
| AtomT(string)
557
+
| ConsT(string)
558
+
| NameT(string)
559
+
| EOF
547
560
let varRegexpString = "^\\\\([0-9]+)"
548
561
let schematicRegexpString = "^\\?([0-9]+)"
549
562
let tokenize = (str0: string): (token, string) => {
···
583
596
}
584
597
}
585
598
}
599
+
| "@" =>
600
+
let re = RegExp.fromStringWithFlags(symbolRegexpString, ~flags="y")
601
+
switch re->RegExp.exec(rest()) {
602
+
| None => raise(ParseError("invalid symbol"))
603
+
| Some(res) =>
604
+
switch RegExp.Result.matches(res) {
605
+
| [n] => (ConsT(n), String.sliceToEnd(rest(), ~start=RegExp.lastIndex(re)))
606
+
| _ => raise(ParseError("invalid symbol"))
607
+
}
608
+
}
586
609
| _ => {
587
610
let reName = RegExp.fromStringWithFlags(nameRES, ~flags="y")
588
611
switch reName->RegExp.exec(str) {
···
608
631
}
609
632
type rec simple =
610
633
| ListS({xs: array<simple>})
611
-
| AtomS({name: string})
634
+
| AtomS({name: string, constructor: bool})
612
635
| VarS({idx: int})
613
636
| SchematicS({schematic: int})
614
637
| LambdaS({name: string, body: simple})
···
636
659
| RParen => raise(ParseError("unexpected right parenthesis"))
637
660
| VarT(idx) => (VarS({idx: idx}), rest)
638
661
| SchematicT(schematic) => (SchematicS({schematic: schematic}), rest)
639
-
| AtomT(name) => (AtomS({name: name}), rest)
662
+
| AtomT(name) => (AtomS({name, constructor: false}), rest)
663
+
| ConsT(name) => (AtomS({name, constructor: true}), rest)
640
664
| NameT(name) => {
641
665
let (result, rest1) = parseSimple(rest)
642
666
(LambdaS({name, body: result}), rest1)
···
679
703
->Array.reduce(ts[0]->Option.getExn, (acc, x) => App({func: acc, arg: x}))
680
704
}
681
705
}
682
-
| AtomS({name}) =>
683
-
if env->Map.has(name) {
706
+
| AtomS({name, constructor}) =>
707
+
if constructor {
708
+
Symbol({name, constructor: true})
709
+
} else if env->Map.has(name) {
684
710
let idx = env->Map.get(name)->Option.getExn
685
711
Var({idx: idx})
686
712
} else {
687
-
Symbol({name: name})
713
+
Symbol({name, constructor: false})
688
714
}
689
715
| VarS({idx}) => Var({idx: idx})
690
716
| SchematicS({schematic}) =>
+1
-1
src/HOTerm.resi
+1
-1
src/HOTerm.resi
+18
-8
src/InductiveSet.res
+18
-8
src/InductiveSet.res
···
40
40
->Array.filterMap(((name, rule)) =>
41
41
extractConstructorSignature(rule)->Option.map(sig => (name, rule, sig))
42
42
)
43
+
// Only allow type constructors with arity 1
44
+
->Array.filter(((_, _, (_cname, arity))) => arity == 1)
43
45
->Array.reduce(Dict.make(), (acc, (name, rule, (cname, arity))) => {
44
46
let key = makeKey(cname, arity)
45
47
Dict.set(acc, key, [(name, rule), ...Dict.get(acc, key)->Option.getOr([])])
···
111
113
{
112
114
Rule.vars: [],
113
115
premises: [],
114
-
conclusion: HOTerm.app(HOTerm.Symbol({name: str}), HOTerm.mkvars(i)),
116
+
conclusion: HOTerm.app(HOTerm.Symbol({name: str, constructor: false}), HOTerm.mkvars(i)),
115
117
},
116
118
...subgoals,
117
119
],
···
183
185
let caseSubgoal = ((_constructorName: string, constructorRule: Rule.t)): Rule.t => {
184
186
let offset = Array.length(constructorRule.vars)
185
187
188
+
// Extract the argument from the constructor conclusion
189
+
// e.g., from (Nat 0) extract 0, from (Nat (S n)) extract (S n)
190
+
let (_head, args) = HOTerm.strip(constructorRule.conclusion)
191
+
let constructorArg = switch args[0] {
192
+
| Some(arg) => arg
193
+
| None => raise(Unreachable("Constructor conclusion must have one argument"))
194
+
}
195
+
186
196
let equalityPremise = {
187
197
Rule.vars: [],
188
198
premises: [],
189
199
conclusion: HOTerm.app(
190
-
HOTerm.Symbol({name: "="}),
191
-
[HOTerm.Var({idx: offset}), constructorRule.conclusion],
200
+
HOTerm.Symbol({name: "=", constructor: false}),
201
+
[HOTerm.Var({idx: offset}), constructorArg],
192
202
),
193
203
}
194
204
···
207
217
{
208
218
Rule.vars: [],
209
219
premises: [],
210
-
conclusion: HOTerm.app(HOTerm.Symbol({name: str}), [HOTerm.Var({idx: 0})]),
220
+
conclusion: HOTerm.app(
221
+
HOTerm.Symbol({name: str, constructor: false}),
222
+
[HOTerm.Var({idx: 0})],
223
+
),
211
224
},
212
225
...subgoals,
213
226
],
···
222
235
let mutualComponent = findMutuallyInductiveComponent(group, groupByConstructor(state))
223
236
let inductionRule = generateInductionRule(group, mutualComponent)
224
237
let casesRule = generateCasesRule(group)
225
-
[
226
-
("§induction-" ++ makeKey(group.name, group.arity), inductionRule),
227
-
("§cases-" ++ makeKey(group.name, group.arity), casesRule),
228
-
]
238
+
[("§induction-" ++ group.name, inductionRule), ("§cases-" ++ group.name, casesRule)]
229
239
})
230
240
->Dict.fromArray
231
241
let serialise = (state: state) =>
+1
-1
src/Method.res
+1
-1
src/Method.res
···
365
365
possibleElims->Array.forEach(((elimName, elim)) => {
366
366
let ruleInsts = rule->Rule.genSchemaInsts(gen, ~scope=ctx.fixes)
367
367
let rule' = rule->Rule.instantiate(ruleInsts)
368
-
Judgment.unify((rule'.premises[0]->Option.getExn).conclusion, elim.conclusion)
368
+
Judgment.unify((rule'.premises[0]->Option.getExn).conclusion, elim.conclusion, ~gen)
369
369
->Seq.take(seqSizeLimit)
370
370
->Seq.forEach(
371
371
elimSub => {
+44
-13
tests/HOTermTest.res
+44
-13
tests/HOTermTest.res
···
51
51
testUnify0(t, bt, at, ~subst?, ~msg?, ~reduce)
52
52
}
53
53
zoraBlock("parse symbol", t => {
54
-
t->block("single char", t => t->Util.testParse("x", Symbol({name: "x"})))
55
-
t->block("multi char", t => t->Util.testParse("xyz", Symbol({name: "xyz"})))
54
+
t->block("single char", t => t->Util.testParse("x", Symbol({name: "x", constructor: false})))
55
+
t->block("multi char", t => t->Util.testParse("xyz", Symbol({name: "xyz", constructor: false})))
56
56
})
57
57
58
58
zoraBlock("parse var", t => {
···
66
66
67
67
zoraBlock("parse application", t => {
68
68
t->block("multiple", t => {
69
-
t->Util.testParse("(a b)", App({func: Symbol({name: "a"}), arg: Symbol({name: "b"})}))
69
+
t->Util.testParse(
70
+
"(a b)",
71
+
App({
72
+
func: Symbol({name: "a", constructor: false}),
73
+
arg: Symbol({name: "b", constructor: false}),
74
+
}),
75
+
)
70
76
})
71
77
t->block("multiple more", t => {
72
78
t->Util.testParse(
73
79
"(a b c)",
74
80
App({
75
-
func: App({func: Symbol({name: "a"}), arg: Symbol({name: "b"})}),
76
-
arg: Symbol({name: "c"}),
81
+
func: App({
82
+
func: Symbol({name: "a", constructor: false}),
83
+
arg: Symbol({name: "b", constructor: false}),
84
+
}),
85
+
arg: Symbol({name: "c", constructor: false}),
77
86
}),
78
87
)
79
88
})
···
81
90
t->Util.testParse(
82
91
"(a \\1 ?1)",
83
92
App({
84
-
func: App({func: Symbol({name: "a"}), arg: Var({idx: 1})}),
93
+
func: App({func: Symbol({name: "a", constructor: false}), arg: Var({idx: 1})}),
85
94
arg: Schematic({schematic: 1}),
86
95
}),
87
96
)
···
114
123
Lam({name: "x", body: App({func: Var({idx: 0}), arg: Var({idx: 0})})}),
115
124
)
116
125
})
126
+
t->block("constructor", t => {
127
+
t->Util.testParse("@cons", Symbol({name: "cons", constructor: true}))
128
+
})
117
129
// TODO: test if remaining strings are returned correctly
118
130
})
119
131
···
121
133
t->block("examples", t => {
122
134
t->Util.testParsePrettyPrint("\\1", "\\1")
123
135
t->Util.testParsePrettyPrint("?1", "?1")
136
+
t->Util.testParsePrettyPrint("@cons", "@cons")
124
137
t->Util.testParsePrettyPrint("(x. x)", "(x. x)")
125
138
t->Util.testParsePrettyPrint("(x. x. \\0)", "(x. x. x)")
126
139
t->Util.testParsePrettyPrint("(x. x. \\1)", "(x. x. \\1)")
···
150
163
t->block("flex-rigid", t => {
151
164
let x = "?0"
152
165
let y = "y"
153
-
t->testUnify(x, y, ~subst=emptySubst->substAdd(0, Symbol({name: "y"})))
166
+
t->testUnify(x, y, ~subst=emptySubst->substAdd(0, Symbol({name: "y", constructor: false})))
154
167
})
155
168
t->block("flex-rigid2", t => {
156
169
let x = "(x. ?0 x)"
···
162
175
~reduce=false,
163
176
~subst=emptySubst->substAdd(
164
177
0,
165
-
Lam({name: "x", body: App({func: Symbol({name: "y"}), arg: Var({idx: 0})})}),
178
+
Lam({
179
+
name: "x",
180
+
body: App({func: Symbol({name: "y", constructor: false}), arg: Var({idx: 0})}),
181
+
}),
166
182
),
167
183
)
168
-
t->testUnify(x, y, ~reduce=true, ~subst=emptySubst->substAdd(0, Symbol({name: "y"})))
184
+
t->testUnify(
185
+
x,
186
+
y,
187
+
~reduce=true,
188
+
~subst=emptySubst->substAdd(0, Symbol({name: "y", constructor: false})),
189
+
)
169
190
})
170
191
t->block("flex-rigid3", t => {
171
192
let x = "(?0 \\10)"
172
193
let y = "(fst \\10)"
173
-
t->testUnify(x, y, ~reduce=true, ~subst=emptySubst->substAdd(0, Symbol({name: "fst"})))
194
+
t->testUnify(
195
+
x,
196
+
y,
197
+
~reduce=true,
198
+
~subst=emptySubst->substAdd(0, Symbol({name: "fst", constructor: false})),
199
+
)
174
200
})
175
201
t->block("flex-rigid", t => {
176
202
let x = "(?0 \\10)"
···
183
209
Lam({
184
210
name: "x",
185
211
body: App({
186
-
func: Symbol({name: "r"}),
187
-
arg: App({func: Symbol({name: "fst"}), arg: Var({idx: 0})}),
212
+
func: Symbol({name: "r", constructor: false}),
213
+
arg: App({func: Symbol({name: "fst", constructor: false}), arg: Var({idx: 0})}),
188
214
}),
189
215
}),
190
216
),
···
265
291
"(x. ?0 x)",
266
292
"a",
267
293
~reduce=true,
268
-
~subst=emptySubst->substAdd(0, Symbol({name: "a"})),
294
+
~subst=emptySubst->substAdd(0, Symbol({name: "a", constructor: false})),
269
295
)
270
296
})
271
297
t->block("divergent", t => {
···
278
304
let a = "(?0 \\0 \\0)"
279
305
let b = "\\0"
280
306
t->testUnify(a, b, ~subst=emptySubst->substAdd(0, t->Util.parse("(x. x. \\0)")))
307
+
})
308
+
t->block("dup var 2", t => {
309
+
let a = "(k. ?0 k k)"
310
+
let b = "(k. G k)"
311
+
t->testUnify(a, b, ~subst=emptySubst->substAdd(0, t->Util.parse("(x. x. G x)")))
281
312
})
282
313
// Yokoyama et al.'s example in A Functional Implementation of Function-as-Constructor Higher-Order Unification Makoto Hamana1
283
314
t->block("break global resctriction", t => {