the next generation of the in-browser educational proof assistant
Merge pull request #20 from mio-19/mio
support more than one parameter predicate; add a simple 2 ary test case
authored by
Liam O'Connor
and committed by
GitHub
f00a5280
b31f978c
+32
-23
+9
index.html
+9
index.html
···
284
284
---- Pair
285
285
(Data (A a b))
286
286
</hol-inductive>
287
+
<hol-inductive id="index.html/natt" deps="index.html/myconfig">
288
+
x.
289
+
-------- Znatt
290
+
(natt x 0)
291
+
n.x.
292
+
(natt x n)
293
+
-------- sucnatt
294
+
(natt x (S n))
295
+
</hol-inductive>
287
296
<hol-comp id="index.html/baz" deps="index.html/myconfig">
288
297
x.y.
289
298
(/\ x y)
+23
-23
src/InductiveSet.res
+23
-23
src/InductiveSet.res
···
25
25
}
26
26
27
27
let makeKey = (name, arity) => name ++ "§" ++ Int.toString(arity)
28
+
let makeVarNames = (arity: int) =>
29
+
Array.fromInitializer(~length=arity, i => "§" ++ Int.toString(i))
30
+
let makeVarArgs = (arity: int) => Array.fromInitializer(~length=arity, i => HOTerm.Var({idx: i}))
28
31
29
32
let extractPredicateSignature = (rule: Rule.t): option<(string, int)> => {
30
33
let (head, args) = HOTerm.strip(rule.conclusion)
···
40
43
->Array.filterMap(((name, rule)) =>
41
44
extractPredicateSignature(rule)->Option.map(sig => (name, rule, sig))
42
45
)
43
-
// Only allow predicates with arity 1
44
-
->Array.filter(((_, _, (_cname, arity))) => arity == 1)
45
46
->Array.reduce(Dict.make(), (acc, (name, rule, (cname, arity))) => {
46
47
let key = makeKey(cname, arity)
47
48
Dict.set(acc, key, [(name, rule), ...Dict.get(acc, key)->Option.getOr([])])
···
103
104
104
105
{
105
106
Rule.vars: Array.concat(
106
-
Array.fromInitializer(~length=i, i => "§" ++ Int.toString(i)),
107
+
makeVarNames(i),
107
108
Array.fromInitializer(~length=numFormers, i => "§P" ++ Int.toString(i)),
108
109
),
109
110
premises: [
110
111
{
111
112
Rule.vars: [],
112
113
premises: [],
113
-
conclusion: HOTerm.app(HOTerm.Symbol({name: str, constructor: false}), HOTerm.mkvars(i)),
114
+
conclusion: HOTerm.app(HOTerm.Symbol({name: str, constructor: false}), makeVarArgs(i)),
114
115
},
115
116
...subgoals,
116
117
],
117
-
conclusion: HOTerm.app(HOTerm.Var({idx: i + groupIndex}), HOTerm.mkvars(i)),
118
+
conclusion: HOTerm.app(HOTerm.Var({idx: i + groupIndex}), makeVarArgs(i)),
118
119
}
119
120
}
120
121
···
177
178
}
178
179
179
180
let generateCasesRule = (group: predicateGroup): Rule.t => {
180
-
let {name: str, arity: _i} = group
181
+
let {name: str, arity} = group
181
182
182
183
let caseSubgoal = ((_constructorName: string, predicateRule: Rule.t)): Rule.t => {
183
184
let offset = Array.length(predicateRule.vars)
···
185
186
// Extract the argument from the predicate conclusion
186
187
// e.g., from (Nat 0) extract 0, from (Nat (S n)) extract (S n)
187
188
let (_head, args) = HOTerm.strip(predicateRule.conclusion)
188
-
let predicateArg = switch args[0] {
189
-
| Some(arg) => arg
190
-
| None => throw(Unreachable("Predicate conclusion must have one argument"))
191
-
}
189
+
assert(Array.length(args) == arity)
192
190
193
-
let equalityPremise = {
194
-
Rule.vars: [],
195
-
premises: [],
196
-
conclusion: HOTerm.app(
197
-
HOTerm.Symbol({name: "=", constructor: false}),
198
-
[HOTerm.Var({idx: offset}), predicateArg],
199
-
),
200
-
}
191
+
let equalityPremises = args->Array.mapWithIndex((arg, idx) => {
192
+
{
193
+
Rule.vars: [],
194
+
premises: [],
195
+
conclusion: HOTerm.app(
196
+
HOTerm.Symbol({name: "=", constructor: false}),
197
+
[HOTerm.Var({idx: offset + idx}), arg],
198
+
),
199
+
}
200
+
})
201
201
202
202
{
203
203
Rule.vars: predicateRule.vars,
204
-
premises: Array.concat([equalityPremise], predicateRule.premises),
205
-
conclusion: HOTerm.Var({idx: offset + 1}),
204
+
premises: Array.concat(equalityPremises, predicateRule.premises),
205
+
conclusion: HOTerm.Var({idx: offset + arity}),
206
206
}
207
207
}
208
208
209
209
let subgoals = Array.map(group.rules, ((name, rule)) => caseSubgoal((name, rule)))
210
210
211
211
{
212
-
Rule.vars: Array.concat(["§0"], ["§P"]),
212
+
Rule.vars: Array.concat(makeVarNames(arity), ["§P"]),
213
213
premises: [
214
214
{
215
215
Rule.vars: [],
216
216
premises: [],
217
217
conclusion: HOTerm.app(
218
218
HOTerm.Symbol({name: str, constructor: false}),
219
-
[HOTerm.Var({idx: 0})],
219
+
makeVarArgs(arity),
220
220
),
221
221
},
222
222
...subgoals,
223
223
],
224
-
conclusion: HOTerm.Var({idx: 1}),
224
+
conclusion: HOTerm.Var({idx: arity}),
225
225
}
226
226
}
227
227