the next generation of the in-browser educational proof assistant
1open Signatures
2open Component
3module 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 >
59 {Dict.toArray(props.content)
60 ->Array.mapWithIndex(((n, r), i) =>
61 <RuleView
62 rule={r}
63 scope={[]}
64 key={String.make(i)}
65 style={props.imports.ruleStyle->Option.getOr(Hybrid)}
66 >
67 {React.string(n)}
68 </RuleView>
69 )
70 ->React.array}
71 </div>
72 }
73}