the next generation of the in-browser educational proof assistant
copy AxiomSet to InductiveSet
+71
+71
src/InductiveSet.res
+71
src/InductiveSet.res
···
1
+
open Signatures
2
+
open Component
3
+
module Make = (
4
+
Term: TERM,
5
+
Judgment: JUDGMENT with module Term := Term,
6
+
JudgmentView: JUDGMENT_VIEW with module Term := Term and module Judgment := Judgment,
7
+
) => {
8
+
module Rule = Rule.Make(Term, Judgment)
9
+
module RuleView = RuleView.Make(Term, Judgment, JudgmentView)
10
+
module Ports = Ports(Term, Judgment)
11
+
type state = dict<Rule.t>
12
+
type props = {
13
+
content: state,
14
+
imports: Ports.t,
15
+
onChange: (state, ~exports: Ports.t=?) => unit,
16
+
}
17
+
18
+
let serialise = (state: state) => {
19
+
state
20
+
->Dict.toArray
21
+
->Array.map(((k, r)) => r->Rule.prettyPrintTopLevel(~name=k))
22
+
->Array.join("\n")
23
+
}
24
+
let deserialise = (str: string, ~imports as _: Ports.t) => {
25
+
let cur = ref(str)
26
+
let go = ref(true)
27
+
let results = Dict.make()
28
+
let ret = ref(Error("impossible"))
29
+
while go.contents {
30
+
switch Rule.parseTopLevel(cur.contents, ~scope=[]) {
31
+
| Ok((t, n), rest) =>
32
+
if n->String.trim == "" {
33
+
go := false
34
+
ret := Error("Rule given with no name")
35
+
} else {
36
+
Dict.set(results, n, t)
37
+
if rest->String.trim == "" {
38
+
go := false
39
+
ret := Ok(results)
40
+
} else {
41
+
cur := rest
42
+
}
43
+
}
44
+
| Error(e) => {
45
+
go := false
46
+
ret := Error(e)
47
+
}
48
+
}
49
+
}
50
+
ret.contents->Result.map(state => (state, {Ports.facts: state, ruleStyle: None}))
51
+
}
52
+
53
+
let make = props => {
54
+
<div
55
+
className={"axiom-set axiom-set-"->String.concat(
56
+
String.make(props.imports.ruleStyle->Option.getOr(Hybrid)),
57
+
)}>
58
+
{Dict.toArray(props.content)
59
+
->Array.mapWithIndex(((n, r), i) =>
60
+
<RuleView
61
+
rule={r}
62
+
scope={[]}
63
+
key={String.make(i)}
64
+
style={props.imports.ruleStyle->Option.getOr(Hybrid)}>
65
+
{React.string(n)}
66
+
</RuleView>
67
+
)
68
+
->React.array}
69
+
</div>
70
+
}
71
+
}