the next generation of the in-browser educational proof assistant
refactor: it is called predicate
+28
-31
+28
-31
src/InductiveSet.res
+28
-31
src/InductiveSet.res
···
18
18
onChange: (state, ~exports: Ports.t=?) => unit,
19
19
}
20
20
21
-
type constructorGroup = {
21
+
type predicateGroup = {
22
22
name: string,
23
23
arity: int,
24
24
rules: array<(string, Rule.t)>,
···
26
26
27
27
let makeKey = (name, arity) => name ++ "§" ++ Int.toString(arity)
28
28
29
-
let extractConstructorSignature = (rule: Rule.t): option<(string, int)> => {
29
+
let extractPredicateSignature = (rule: Rule.t): option<(string, int)> => {
30
30
let (head, args) = HOTerm.strip(rule.conclusion)
31
31
switch head {
32
32
| Symbol({name}) => Some((name, Array.length(args)))
···
34
34
}
35
35
}
36
36
37
-
let groupByConstructor = (rules: dict<Rule.t>): array<constructorGroup> =>
37
+
let groupByPredicate = (rules: dict<Rule.t>): array<predicateGroup> =>
38
38
rules
39
39
->Dict.toArray
40
40
->Array.filterMap(((name, rule)) =>
41
-
extractConstructorSignature(rule)->Option.map(sig => (name, rule, sig))
41
+
extractPredicateSignature(rule)->Option.map(sig => (name, rule, sig))
42
42
)
43
-
// Only allow type constructors with arity 1
43
+
// Only allow predicates with arity 1
44
44
->Array.filter(((_, _, (_cname, arity))) => arity == 1)
45
45
->Array.reduce(Dict.make(), (acc, (name, rule, (cname, arity))) => {
46
46
let key = makeKey(cname, arity)
···
48
48
acc
49
49
})
50
50
->Dict.valuesToArray
51
-
->Array.map(constructors => {
52
-
let (_, firstRule) = constructors[0]->Option.getExn
53
-
let (name, arity) = extractConstructorSignature(firstRule)->Option.getExn
54
-
{name, arity, rules: constructors}
51
+
->Array.map(predicates => {
52
+
let (_, firstRule) = predicates[0]->Option.getExn
53
+
let (name, arity) = extractPredicateSignature(firstRule)->Option.getExn
54
+
{name, arity, rules: predicates}
55
55
})
56
-
let generateInductionRule = (
57
-
group: constructorGroup,
58
-
allGroups: array<constructorGroup>,
59
-
): Rule.t => {
56
+
let generateInductionRule = (group: predicateGroup, allGroups: array<predicateGroup>): Rule.t => {
60
57
let {name: str, arity: i} = group
61
58
let numFormers = Array.length(allGroups)
62
59
let groupIndex = mustFindIndex(allGroups, g => g.name == str && g.arity == i)
···
134
131
}
135
132
}
136
133
137
-
let isSelfReference = (group: constructorGroup, (name, arity)): bool =>
134
+
let isSelfReference = (group: predicateGroup, (name, arity)): bool =>
138
135
name == group.name && arity == group.arity
139
136
140
-
let findDependencies = (group: constructorGroup): array<(string, int)> =>
137
+
let findDependencies = (group: predicateGroup): array<(string, int)> =>
141
138
group.rules
142
139
->Array.flatMap(((_name, rule)) => rule.premises->Array.filterMap(extractInductiveType))
143
140
->Array.filter(dep => !isSelfReference(group, dep))
···
145
142
let rec collectReachable = (
146
143
toVisit: array<(string, int)>,
147
144
visited: Belt.Set.t<string, StringCmp.identity>,
148
-
allGroups: array<constructorGroup>,
145
+
allGroups: array<predicateGroup>,
149
146
): Belt.Set.t<string, StringCmp.identity> =>
150
147
switch toVisit {
151
148
| [] => visited
···
168
165
}
169
166
170
167
let findMutuallyInductiveComponent = (
171
-
targetGroup: constructorGroup,
172
-
allGroups: array<constructorGroup>,
173
-
): array<constructorGroup> => {
168
+
targetGroup: predicateGroup,
169
+
allGroups: array<predicateGroup>,
170
+
): array<predicateGroup> => {
174
171
let reachableKeys = collectReachable(
175
172
[(targetGroup.name, targetGroup.arity)],
176
173
Belt.Set.make(~id=module(StringCmp)),
···
179
176
allGroups->Array.filter(g => Belt.Set.has(reachableKeys, makeKey(g.name, g.arity)))
180
177
}
181
178
182
-
let generateCasesRule = (group: constructorGroup): Rule.t => {
179
+
let generateCasesRule = (group: predicateGroup): Rule.t => {
183
180
let {name: str, arity: _i} = group
184
181
185
-
let caseSubgoal = ((_constructorName: string, constructorRule: Rule.t)): Rule.t => {
186
-
let offset = Array.length(constructorRule.vars)
182
+
let caseSubgoal = ((_constructorName: string, predicateRule: Rule.t)): Rule.t => {
183
+
let offset = Array.length(predicateRule.vars)
187
184
188
-
// Extract the argument from the constructor conclusion
185
+
// Extract the argument from the predicate conclusion
189
186
// 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] {
187
+
let (_head, args) = HOTerm.strip(predicateRule.conclusion)
188
+
let predicateArg = switch args[0] {
192
189
| Some(arg) => arg
193
-
| None => raise(Unreachable("Constructor conclusion must have one argument"))
190
+
| None => raise(Unreachable("Predicate conclusion must have one argument"))
194
191
}
195
192
196
193
let equalityPremise = {
···
198
195
premises: [],
199
196
conclusion: HOTerm.app(
200
197
HOTerm.Symbol({name: "=", constructor: false}),
201
-
[HOTerm.Var({idx: offset}), constructorArg],
198
+
[HOTerm.Var({idx: offset}), predicateArg],
202
199
),
203
200
}
204
201
205
202
{
206
-
Rule.vars: constructorRule.vars,
207
-
premises: Array.concat([equalityPremise], constructorRule.premises),
203
+
Rule.vars: predicateRule.vars,
204
+
premises: Array.concat([equalityPremise], predicateRule.premises),
208
205
conclusion: HOTerm.Var({idx: offset + 1}),
209
206
}
210
207
}
···
230
227
231
228
let derived = (state: state): state =>
232
229
state
233
-
->groupByConstructor
230
+
->groupByPredicate
234
231
->Array.flatMap(group => {
235
-
let mutualComponent = findMutuallyInductiveComponent(group, groupByConstructor(state))
232
+
let mutualComponent = findMutuallyInductiveComponent(group, groupByPredicate(state))
236
233
let inductionRule = generateInductionRule(group, mutualComponent)
237
234
let casesRule = generateCasesRule(group)
238
235
[("§induction-" ++ group.name, inductionRule), ("§cases-" ++ group.name, casesRule)]