the next generation of the in-browser educational proof assistant
implemented grouping by constructor/arity
+68
-3
+9
index.html
+9
index.html
···
257
257
</style>
258
258
</head>
259
259
<body>
260
+
<hol-inductive id="index.html/nat" deps="index.html/myconfig">
261
+
---- Z
262
+
(Nat 0)
263
+
264
+
n.
265
+
(Nat n)
266
+
------- S
267
+
(Nat (S n))
268
+
</hol-inductive>
260
269
<hol-comp id="index.html/baz" deps="index.html/myconfig">
261
270
x.y.
262
271
(/\ x y)
+56
-2
src/InductiveSet.res
+56
-2
src/InductiveSet.res
···
1
1
open Signatures
2
2
open Component
3
+
4
+
// InductiveSet is specific to HOTerm to allow pattern matching on term structure
3
5
module Make = (
4
-
Term: TERM,
5
-
Judgment: JUDGMENT with module Term := Term,
6
+
Term: TERM with type t = HOTerm.t,
7
+
Judgment: JUDGMENT with module Term := Term and type t = HOTerm.t,
6
8
JudgmentView: JUDGMENT_VIEW with module Term := Term and module Judgment := Judgment,
7
9
) => {
8
10
module Rule = Rule.Make(Term, Judgment)
···
15
17
onChange: (state, ~exports: Ports.t=?) => unit,
16
18
}
17
19
20
+
let isIntroduction = (rule: Rule.t): bool => {
21
+
let (head, _args) = HOTerm.strip(rule.conclusion)
22
+
23
+
switch head {
24
+
| Symbol(_) => true
25
+
| _ => false
26
+
}
27
+
}
28
+
29
+
let introRoot = (rule: Rule.t): option<(string, int)> => {
30
+
let (head, args) = HOTerm.strip(rule.conclusion)
31
+
32
+
switch head {
33
+
| Symbol({name}) => Some((name, Array.length(args)))
34
+
| _ => None
35
+
}
36
+
}
37
+
38
+
type constructorKey = (string, int)
39
+
let groupByConstructor = (rules: dict<Rule.t>): dict<array<(string, Rule.t)>> => {
40
+
// filter to only introduction rules and extract their roots
41
+
let introRules =
42
+
Dict.toArray(rules)
43
+
->Array.map(((name, rule)) => (name, rule, introRoot(rule)))
44
+
->Array.filter(((_, _, root)) => root->Option.isSome)
45
+
->Array.map(((name, rule, root)) => (name, rule, root->Option.getUnsafe))
46
+
47
+
let grouped = Dict.make()
48
+
Array.forEach(introRules, ((name, rule, (constructorName, arity))) => {
49
+
let key = constructorName ++ "§" ++ Int.toString(arity)
50
+
switch Dict.get(grouped, key) {
51
+
| None => Dict.set(grouped, key, [(name, rule)])
52
+
| Some(existing) => Dict.set(grouped, key, Array.concat(existing, [(name, rule)]))
53
+
}
54
+
})
55
+
56
+
grouped
57
+
}
58
+
18
59
let derived = (state: state): state => {
60
+
let groups = groupByConstructor(state)
61
+
62
+
Console.log("=== Inductive Set Grouping ===")
63
+
Dict.toArray(groups)->Array.forEach(((key, rules)) => {
64
+
Console.log2("Group", key)
65
+
Array.forEach(rules, ((name, rule)) => {
66
+
let root = introRoot(rule)
67
+
Console.log2(name, root)
68
+
})
69
+
})
70
+
Console.log("=== End Grouping ===")
71
+
72
+
// For now, just return empty - we'll generate induction rules here later
19
73
Dict.make()
20
74
}
21
75
let serialise = (state: state) => {
+1
src/Scratch.res
+1
src/Scratch.res
+2
-1
src/testcomponent.tsx
+2
-1
src/testcomponent.tsx
···
1
1
import * as ComponentGraph from './componentgraph'
2
-
import { AxiomS, ConfS, TheoremS } from './Scratch.mjs'
2
+
import { AxiomS, ConfS, TheoremS, InductiveS } from './Scratch.mjs'
3
3
import ReactDOM from 'react-dom/client';
4
4
import React from 'react';
5
5
···
76
76
window.localStorage.clear()
77
77
ComponentGraph.setup({
78
78
"hol-comp": HolComp(AxiomS),
79
+
"hol-inductive": HolComp(InductiveS),
79
80
"hol-config":HolComp(ConfS),
80
81
"hol-proof": HolComp(TheoremS)
81
82
});