forked from
liamoc.net/holbert-ng
the next generation of the in-browser educational proof assistant
refactoring, no more react errors
+205
-265
+68
src/AxiomSet.res
+68
src/AxiomSet.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
+
module Rule = Rule.Make(Term,Judgment)
8
+
module RuleView = RuleView.Make(Term,Judgment,JudgmentView)
9
+
module Ports = Ports(Term,Judgment)
10
+
type props = { content: string, imports: Ports.t, onLoad: (~exports:Ports.t) => (), onChange: (string,~exports:Ports.t) => () }
11
+
12
+
let deserialise = (str: string) => {
13
+
let cur = ref(str)
14
+
let go = ref(true)
15
+
let results = Dict.make()
16
+
let ret = ref(Error("impossible"))
17
+
while go.contents {
18
+
switch Rule.parseTopLevel(cur.contents,~scope=[]) {
19
+
| Ok((t,n),rest) => {
20
+
if n->String.trim == "" {
21
+
go := false
22
+
ret := Error("Rule given with no name")
23
+
} else {
24
+
Dict.set(results,n,t)
25
+
if rest->String.trim == "" {
26
+
go := false
27
+
ret := Ok(results)
28
+
} else {
29
+
cur := rest
30
+
}
31
+
}
32
+
}
33
+
| Error(e) => { go := false; ret := Error(e) }
34
+
}
35
+
}
36
+
ret.contents
37
+
}
38
+
39
+
let make = (props ) => {
40
+
switch deserialise(props.content) {
41
+
| Ok(s) => {
42
+
React.useEffect(() => {
43
+
// Run effects
44
+
props.onLoad(~exports= {Ports.facts: s, ruleStyle: None});
45
+
None // or Some(() => {})
46
+
}, [])
47
+
48
+
<div className={"axiom-set axiom-set-"->String.concat(String.make(props.imports.ruleStyle->Option.getOr(Hybrid)))}>
49
+
{ Dict.toArray(s)->Array.mapWithIndex(((n,r), i) =>
50
+
<RuleView rule={r} scope={[]} key={String.make(i)} style={props.imports.ruleStyle->Option.getOr(Hybrid)}>
51
+
{React.string(n)}
52
+
//<Name content={n} onChange={(_) => Error("BLAH!")} />
53
+
</RuleView>)
54
+
->React.array
55
+
}
56
+
</div>
57
+
}
58
+
| Error(e) => {
59
+
React.useEffect(() => {
60
+
// Run effects
61
+
props.onLoad(~exports= {Ports.facts: Dict.make(), ruleStyle: None});
62
+
None // or Some(() => {})
63
+
}, [])
64
+
<div className="error"> {React.string(e)} </div>
65
+
}
66
+
}
67
+
}
68
+
}
+21
src/Component.res
+21
src/Component.res
···
1
+
open Signatures
2
+
module type PORTS = {
3
+
type t
4
+
let combine : (t,t) => t
5
+
let empty: t
6
+
}
7
+
module Ports = (Term : TERM, Judgment : JUDGMENT with module Term := Term) => {
8
+
module Rule = Rule.Make(Term, Judgment)
9
+
type t = { facts: Dict.t<Rule.t>, ruleStyle: option<RuleView.style> }
10
+
let empty = { facts: Dict.make(), ruleStyle: None }
11
+
let combine = (p1,p2) => {
12
+
let facts = Dict.copy(p1.facts)->Dict.assign(p2.facts);
13
+
let ruleStyle = p2.ruleStyle->Option.mapOr(p1.ruleStyle, x => Some(x));
14
+
{ facts, ruleStyle }
15
+
}
16
+
}
17
+
module type COMPONENT = {
18
+
module Ports : PORTS
19
+
type props = { content: string, imports: Ports.t, onLoad: (~exports:Ports.t) => (),onChange: (string,~exports:Ports.t) => () }
20
+
let make : props => React.element
21
+
}
+37
src/ConfigBlock.res
+37
src/ConfigBlock.res
···
1
+
open Signatures
2
+
open Component
3
+
4
+
module Make = (
5
+
Term : TERM,
6
+
Judgment : JUDGMENT with module Term := Term
7
+
) => {
8
+
module Ports = Ports(Term,Judgment)
9
+
open RuleView
10
+
type props = { content: string, imports: Ports.t, onLoad: (~exports:Ports.t) => (), onChange: (string,~exports:Ports.t) => () }
11
+
let deserialise = (str) => switch str {
12
+
| "Gentzen" => Gentzen
13
+
| "Linear" => Linear
14
+
| "Hybrid" => Hybrid
15
+
| _ => Hybrid
16
+
}
17
+
let make = (props) => {
18
+
let (style,setStyle) = React.useState (_=>deserialise(props.content))
19
+
React.useEffect(() => {
20
+
props.onLoad(~exports={Ports.facts: Dict.make(), ruleStyle:Some(style)})
21
+
None
22
+
},[])
23
+
let onChange= (e) => {
24
+
let target = JsxEvent.Form.target(e)
25
+
let value: string = target["value"]
26
+
let sty = deserialise(value)
27
+
setStyle(_ => sty)
28
+
29
+
props.onChange(value,~exports={Ports.facts: Dict.make(), ruleStyle:Some(sty)})
30
+
}
31
+
[Gentzen,Linear,Hybrid]->Array.map(n =>
32
+
<input type_="radio" id={"style_"->String.concat(String.make(n))} key={String.make(n)} name="style" onChange value={String.make(n)} checked={style==n}/>
33
+
)->React.array
34
+
35
+
}
36
+
}
37
+
+2
-213
src/Editable.res
+2
-213
src/Editable.res
···
1
-
open Method
2
-
open Signatures
3
-
4
-
module type PORTS = {
5
-
type t
6
-
let combine : (t,t) => t
7
-
let empty: t
8
-
}
9
-
module Ports = (Term : TERM, Judgment : JUDGMENT with module Term := Term) => {
10
-
module Rule = Rule.Make(Term, Judgment)
11
-
type t = { facts: Dict.t<Rule.t>, ruleStyle: option<RuleView.style> }
12
-
let empty = { facts: Dict.make(), ruleStyle: None }
13
-
let combine = (p1,p2) => {
14
-
let facts = Dict.copy(p1.facts)->Dict.assign(p2.facts);
15
-
let ruleStyle = p2.ruleStyle->Option.mapOr(p1.ruleStyle, x => Some(x));
16
-
{ facts, ruleStyle }
17
-
}
18
-
}
19
-
20
-
21
-
module type COMPONENT = {
22
-
module Ports : PORTS
23
-
type props = { content: string, imports: Ports.t, onLoad: (~exports:Ports.t) => (),onChange: (string,~exports:Ports.t) => () }
24
-
let make : props => React.element
25
-
}
26
-
27
-
module Config = (
28
-
Term : TERM,
29
-
Judgment : JUDGMENT with module Term := Term
30
-
) => {
31
-
module Ports = Ports(Term,Judgment)
32
-
open RuleView
33
-
type props = { content: string, imports: Ports.t, onLoad: (~exports:Ports.t) => (), onChange: (string,~exports:Ports.t) => () }
34
-
let deserialise = (str) => switch str {
35
-
| "Gentzen" => Gentzen
36
-
| "Linear" => Linear
37
-
| "Hybrid" => Hybrid
38
-
| _ => Hybrid
39
-
}
40
-
let make = (props) => {
41
-
let (style,setStyle) = React.useState (_=>deserialise(props.content))
42
-
React.useEffect(() => {
43
-
props.onLoad(~exports={Ports.facts: Dict.make(), ruleStyle:Some(style)})
44
-
None
45
-
},[])
46
-
let onChange= (e) => {
47
-
let target = JsxEvent.Form.target(e)
48
-
let value: string = target["value"]
49
-
let sty = deserialise(value)
50
-
setStyle(_ => sty)
51
-
52
-
props.onChange(value,~exports={Ports.facts: Dict.make(), ruleStyle:Some(sty)})
53
-
}
54
-
[Gentzen,Linear,Hybrid]->Array.map(n =>
55
-
<input type_="radio" id={"style_"->String.concat(String.make(n))} name="style" onChange value={String.make(n)} checked={style==n}/>
56
-
)->React.array
57
-
58
-
}
59
-
}
60
-
1
+
open Component
61
2
62
-
module TextAreaEditor = (Underlying : COMPONENT) => {
3
+
module TextArea = (Underlying : COMPONENT) => {
63
4
module Ports = Underlying.Ports
64
5
type props = { content: string, imports: Ports.t, onLoad: (~exports:Ports.t) => (), onChange: (string,~exports:Ports.t) => () }
65
6
let make = (props) => {
···
98
39
</div>
99
40
}
100
41
}
101
-
}
102
-
103
-
module AxiomSet = (
104
-
Term : TERM,
105
-
Judgment : JUDGMENT with module Term := Term,
106
-
JudgmentView : JUDGMENT_VIEW with module Term := Term and module Judgment := Judgment) => {
107
-
module Rule = Rule.Make(Term,Judgment)
108
-
module RuleView = RuleView.Make(Term,Judgment,JudgmentView)
109
-
module Ports = Ports(Term,Judgment)
110
-
type props = { content: string, imports: Ports.t, onLoad: (~exports:Ports.t) => (), onChange: (string,~exports:Ports.t) => () }
111
-
112
-
let deserialise = (str: string) => {
113
-
let cur = ref(str)
114
-
let go = ref(true)
115
-
let results = Dict.make()
116
-
let ret = ref(Error("impossible"))
117
-
while go.contents {
118
-
switch Rule.parseTopLevel(cur.contents,~scope=[]) {
119
-
| Ok((t,n),rest) => {
120
-
if n->String.trim == "" {
121
-
go := false
122
-
ret := Error("Rule given with no name")
123
-
} else {
124
-
Dict.set(results,n,t)
125
-
if rest->String.trim == "" {
126
-
go := false
127
-
ret := Ok(results)
128
-
} else {
129
-
cur := rest
130
-
}
131
-
}
132
-
}
133
-
| Error(e) => { go := false; ret := Error(e) }
134
-
}
135
-
}
136
-
ret.contents
137
-
}
138
-
139
-
let make = (props ) => {
140
-
switch deserialise(props.content) {
141
-
| Ok(s) => {
142
-
React.useEffect(() => {
143
-
// Run effects
144
-
props.onLoad(~exports= {Ports.facts: s, ruleStyle: None});
145
-
None // or Some(() => {})
146
-
}, [])
147
-
148
-
<div className={"axiom-set axiom-set-"->String.concat(String.make(props.imports.ruleStyle->Option.getOr(Hybrid)))}>
149
-
{ Dict.toArray(s)->Array.mapWithIndex(((n,r), i) =>
150
-
<RuleView rule={r} scope={[]} key={String.make(i)} style={props.imports.ruleStyle->Option.getOr(Hybrid)}>
151
-
{React.string(n)}
152
-
//<Name content={n} onChange={(_) => Error("BLAH!")} />
153
-
</RuleView>)
154
-
->React.array
155
-
}
156
-
</div>
157
-
}
158
-
| Error(e) => {
159
-
React.useEffect(() => {
160
-
// Run effects
161
-
props.onLoad(~exports= {Ports.facts: Dict.make(), ruleStyle: None});
162
-
None // or Some(() => {})
163
-
}, [])
164
-
<div className="error"> {React.string(e)} </div>
165
-
}
166
-
}
167
-
}
168
-
}
169
-
module Theorem = (
170
-
Term : TERM,
171
-
Judgment : JUDGMENT with module Term := Term,
172
-
JudgmentView : JUDGMENT_VIEW with module Term := Term and module Judgment := Judgment,
173
-
Method : PROOF_METHOD with module Term := Term and module Judgment := Judgment
174
-
) => {
175
-
module Rule = Rule.Make(Term,Judgment)
176
-
module Proof = Proof.Make(Term,Judgment,Method)
177
-
module Context = Context(Term,Judgment)
178
-
179
-
open RuleView
180
-
module RuleView = RuleView.Make(Term,Judgment,JudgmentView)
181
-
module Ports = Ports(Term,Judgment)
182
-
type props = { content: string, imports: Ports.t, onLoad: (~exports:Ports.t) => (), onChange: (string,~exports:Ports.t) => () }
183
-
type state = {name: string, rule: Rule.t, proof: Proof.checked}
184
-
let deserialise = (facts : Dict.t<Rule.t>, gen : Term.gen, str : string) : result<state,string> => {
185
-
let cur = ref(str)
186
-
switch Rule.parseTopLevel(cur.contents,~scope=[],~gen=gen) {
187
-
| Error(e) => Error(e)
188
-
| Ok(((r,n),s)) => switch Proof.parse(s,~scope=[],~gen=gen) {
189
-
| Error(e) => Error(e)
190
-
| Ok((_,s')) if String.length(String.trim(s')) > 0 =>
191
-
Error("Trailing input: "->String.concat(s'))
192
-
| Ok((prf,_)) => {
193
-
let ctx : Context.t = {fixes:[],facts}
194
-
Ok({name:n,rule:r,proof:Proof.check(ctx,prf,r)})
195
-
}
196
-
}
197
-
}
198
-
}
199
-
let make = (props) => {
200
-
201
-
let gen = Term.makeGen()
202
-
switch deserialise(props.imports.facts, gen, props.content) {
203
-
| Ok(state) => {
204
-
props.onLoad(~exports={facts: Dict.fromArray([(state.name,state.rule)]), ruleStyle: None})
205
-
<RuleView rule={state.rule} scope={[]}
206
-
style={props.imports.ruleStyle->Option.getOr(Hybrid)}>
207
-
{React.string(state.name)}
208
-
</RuleView>
209
-
}
210
-
| Error(err) => <div className="error"> {React.string(err)} </div>
211
-
}
212
-
213
-
}
214
-
215
-
216
-
}
217
-
218
-
module TheoremSB = (
219
-
Term : TERM,
220
-
Judgment : JUDGMENT with module Term := Term,
221
-
JudgmentView : JUDGMENT_VIEW with module Term := Term and module Judgment := Judgment,
222
-
Method : PROOF_METHOD with module Term := Term and module Judgment := Judgment
223
-
) => {
224
-
module Rule = Rule.Make(Term, Judgment)
225
-
226
-
module Proof = Proof.Make(Term,Judgment,Method)
227
-
module Context = Context(Term,Judgment)
228
-
type state = { name : string, rule: Rule.t, proof: Proof.checked }
229
-
type rec props = {
230
-
name: string,
231
-
rule: Rule.t,
232
-
proof: Proof.checked,
233
-
facts: Dict.t<Rule.t>,
234
-
gen : Term.gen,
235
-
style : RuleView.style,
236
-
onChange: props => result<(),string>
237
-
}
238
-
module RuleView = RuleView.Make(Term,Judgment,JudgmentView)
239
-
let getState : props => state
240
-
= ({name,rule,proof,gen:_,onChange:_,style:_,facts:_})
241
-
=> {name,rule,proof}
242
-
let setState : (props,state) => props = (props,{name,rule,proof})
243
-
=> {name,rule,proof, style:props.style,
244
-
onChange:props.onChange,gen: props.gen,facts: props.facts}
245
-
let onChange = (props) => props.onChange(props)
246
-
let serialise = (props : props, state : state) => {
247
-
state.rule
248
-
->Rule.prettyPrintTopLevel(~scope=[],~name=state.name)
249
-
->String.concat(newline)
250
-
->String.concat(Proof.prettyPrint(Proof.uncheck(state.proof), ~scope=[]))
251
-
}
252
-
253
42
}
+2
-2
src/Method.res
+2
-2
src/Method.res
···
7
7
facts: Dict.t<Rule.t>,
8
8
}
9
9
}
10
-
let newline = "\n"
10
+
11
11
module type PROOF_METHOD = {
12
12
module Term : TERM
13
13
module Judgment : JUDGMENT with module Term := Term
···
181
181
| Error(e) => Error(e)
182
182
}
183
183
}
184
-
let check = (it: t<'a>, ctx : Context.t, j: Judgment.t, f : ('a, Rule.t) => 'b) => {
184
+
let check = (it: t<'a>, _ctx : Context.t, j: Judgment.t, f : ('a, Rule.t) => 'b) => {
185
185
let first = f(it.proof,it.rule)
186
186
let second = f(it.show,{vars:[],premises:[it.rule],conclusion:j})
187
187
Ok({rule:it.rule, proof:first, show:second})
+1
-2
src/Rule.res
+1
-2
src/Rule.res
···
75
75
Array.unshift(vars,str)
76
76
cur := rest
77
77
}
78
-
let it = ref(Error(""))
79
78
let premises = []
80
79
switch {
81
80
while (cur.contents->String.trim->String.slice(~start=0,~end=2) != "|-"
···
174
173
}
175
174
}
176
175
}
177
-
let rec prettyPrintTopLevel = (rule: t,~name="",~scope=[]:array<Term.meta>) => {
176
+
let prettyPrintTopLevel = (rule: t,~name="",~scope=[]:array<Term.meta>) => {
178
177
let vinculise = (strs: array<string>) => {
179
178
let l = strs->Array.map(String.length)->Array.concat([4])->Math.Int.maxMany
180
179
strs->Array.concat(["-"->String.repeat(l)->String.concat(" ")->String.concat(name)])
+17
-11
src/RuleView.res
+17
-11
src/RuleView.res
···
21
21
let rec make = (props : props) => {
22
22
let {vars, premises,conclusion} = props.rule
23
23
let scope = vars->Array.concat(props.scope->Option.getOr([]))
24
-
let arr = vars->Array.map(JudgmentView.TermView.makeMeta)
24
+
let arr = vars->Array.mapWithIndex((m,i) =>
25
+
<React.Fragment key={String.make(i)}>{JudgmentView.TermView.makeMeta(m)}</React.Fragment>
26
+
)
25
27
Array.reverse(arr)
26
28
<span className="inline-rule">
27
29
<span className="rule-rulename-defined">
···
30
32
{if Array.length(arr) > 0 { <span className="rule-binders">{React.array(arr)}</span> }
31
33
else { React.string("") }}
32
34
{React.array(premises
33
-
->Array.mapWithIndex((p,i)=><span className="rule-context">
35
+
->Array.mapWithIndex((p,i)=><span key={String.make(i)} className="rule-context">
34
36
{React.createElement(make,withKey({rule:p, scope,children:React.string(""),style:props.style}, i))}</span>)
35
37
->Array.flatMapWithIndex( (e, i) =>
36
38
if i == 0 {
37
39
[e]
38
40
} else {
39
-
[<span className="symbol symbol-bold symbol-comma">{React.string(",")}</span>,e]
41
+
[<span key={String.make(-i)} className="symbol symbol-bold symbol-comma">{React.string(",")}</span>,e]
40
42
}))}
41
43
{if premises->Array.length > 0 {
42
44
<span className="symbol symbol-turnstile symbol-bold">
···
53
55
module Hypothetical = (Premise : RULE_COMPONENT) => {
54
56
let make = (props : props) => if Array.length(props.rule.premises) == 0 { Inline.make(props) } else {
55
57
let {vars, premises,conclusion} = props.rule
56
-
let arr = vars->Array.map(JudgmentView.TermView.makeMeta)
58
+
let arr = vars->Array.mapWithIndex((m,i) =>
59
+
<React.Fragment key={String.make(i)}>{JudgmentView.TermView.makeMeta(m)}</React.Fragment>
60
+
)
57
61
Array.reverse(arr)
58
62
let scope = vars->Array.concat(props.scope->Option.getOr([]))
59
63
<table className="inference"><tbody>
60
64
<tr><td className="rule-cell rule-binderbox" rowSpan=3>{React.array(arr)}</td>
61
-
{React.array(premises->Array.map(p=>
62
-
<td className="rule-cell rule-premise">
63
-
<Premise rule={p} scope={scope} style={props.style}>
65
+
{React.array(premises->Array.mapWithIndex((p,i)=>
66
+
<td className="rule-cell rule-premise" key={String.make(i)}>
67
+
<Premise rule={p} scope={scope} key={String.make(i)} style={props.style}>
64
68
{React.string("")}
65
69
</Premise>
66
70
</td>))}
···
84
88
module TopLevel = (Premise : RULE_COMPONENT) => {
85
89
let make = (props : props) => {
86
90
let {vars, premises,conclusion} = props.rule
87
-
let arr = vars->Array.map(JudgmentView.TermView.makeMeta)
91
+
let arr = vars->Array.mapWithIndex((m,i) =>
92
+
<React.Fragment key={String.make(i)}>{JudgmentView.TermView.makeMeta(m)}</React.Fragment>
93
+
)
88
94
Array.reverse(arr)
89
95
let scope = vars->Array.concat(props.scope->Option.getOr([]))
90
96
<div className="axiom"><table className="inference"><tbody>
91
97
<tr><td className="rule-cell rule-binderbox" rowSpan=2>{React.array(arr)}</td>
92
-
{React.array(premises->Array.map(p=>
93
-
<td className="rule-cell rule-premise">
94
-
<Premise rule={p} scope={scope} style={props.style}>
98
+
{React.array(premises->Array.mapWithIndex((p,i)=>
99
+
<td className="rule-cell rule-premise" key={String.make(i)}>
100
+
<Premise rule={p} scope={scope} key={String.make(i)} style={props.style}>
95
101
{React.string("")}
96
102
</Premise>
97
103
</td>))}
+1
-7
src/SExp.res
+1
-7
src/SExp.res
···
293
293
| Some(e) => Ok((e,cur.contents))
294
294
}
295
295
}
296
-
let testParse = (str : string, scope: array<string>) => {
297
-
let gen = ref(0)
298
-
switch parse(str,~scope=scope,~gen=gen) {
299
-
| Ok(t,_) => {Console.log(t); Some(t)}
300
-
| Error(e) => {Console.log(e); None}
301
-
}
302
-
}
296
+
+2
-2
src/SExpView.res
+2
-2
src/SExpView.res
···
18
18
</span>
19
19
20
20
let parenthesise = (f) => [
21
-
<span className="symbol">
21
+
<span className="symbol" key={"-1"}>
22
22
{React.string("(")}
23
23
</span>,
24
24
...f,
25
-
<span className="symbol">
25
+
<span className="symbol" key={"-2"}>
26
26
{React.string(")")}
27
27
</span>
28
28
]
+4
-18
src/Scratch.res
+4
-18
src/Scratch.res
···
1
-
open Editable
2
-
open Method
3
-
open Util
4
-
module AxiomS = TextAreaEditor(AxiomSet(SExp,SExp,SExpJView))
5
-
module DerivationsOrLemmas = Combine(SExp,SExp,Derivation(SExp,SExp),Lemma(SExp,SExp))
6
-
module TheoremS = TextAreaEditor(Theorem(SExp,SExp,SExpJView,DerivationsOrLemmas))
7
-
module Conf = Config(SExp,SExp)
8
-
//module RuleSExpTE = RuleSetSB(SExp,SExp,SExpJView)
9
-
//module RuleSExpView = WithTextArea(RuleSExpTE)
10
-
//include RuleSExpView//(RuleSExpView.Hypothetical(RuleSExpView.Inline))
11
-
//
12
-
//module PM = Proof.Make(SExp,SExp,DerivationsOrLemmas)
13
-
14
-
//module TheoremView = WithTextArea(TheoremTE)
15
-
16
-
let \"AxiomSet" = AxiomS.make
17
-
18
-
//include SExpBaseView
1
+
module AxiomS = Editable.TextArea(AxiomSet.Make(SExp,SExp,SExpJView))
2
+
module DerivationsOrLemmas = Method.Combine(SExp,SExp,Method.Derivation(SExp,SExp),Method.Lemma(SExp,SExp))
3
+
module TheoremS = Editable.TextArea(Theorem.Make(SExp,SExp,SExpJView,DerivationsOrLemmas))
4
+
module ConfS = ConfigBlock.Make(SExp,SExp)
19
5
+48
src/Theorem.res
+48
src/Theorem.res
···
1
+
open Signatures
2
+
open Component
3
+
open Method
4
+
module Make = (
5
+
Term : TERM,
6
+
Judgment : JUDGMENT with module Term := Term,
7
+
JudgmentView : JUDGMENT_VIEW with module Term := Term and module Judgment := Judgment,
8
+
Method : PROOF_METHOD with module Term := Term and module Judgment := Judgment
9
+
) => {
10
+
module Rule = Rule.Make(Term,Judgment)
11
+
module Proof = Proof.Make(Term,Judgment,Method)
12
+
module Context = Context(Term,Judgment)
13
+
14
+
open RuleView
15
+
module RuleView = RuleView.Make(Term,Judgment,JudgmentView)
16
+
module Ports = Ports(Term,Judgment)
17
+
type props = { content: string, imports: Ports.t, onLoad: (~exports:Ports.t) => (), onChange: (string,~exports:Ports.t) => () }
18
+
type state = {name: string, rule: Rule.t, proof: Proof.checked}
19
+
let deserialise = (facts : Dict.t<Rule.t>, gen : Term.gen, str : string) : result<state,string> => {
20
+
let cur = ref(str)
21
+
switch Rule.parseTopLevel(cur.contents,~scope=[],~gen=gen) {
22
+
| Error(e) => Error(e)
23
+
| Ok(((r,n),s)) => switch Proof.parse(s,~scope=[],~gen=gen) {
24
+
| Error(e) => Error(e)
25
+
| Ok((_,s')) if String.length(String.trim(s')) > 0 =>
26
+
Error("Trailing input: "->String.concat(s'))
27
+
| Ok((prf,_)) => {
28
+
let ctx : Context.t = {fixes:[],facts}
29
+
Ok({name:n,rule:r,proof:Proof.check(ctx,prf,r)})
30
+
}
31
+
}
32
+
}
33
+
}
34
+
let make = (props) => {
35
+
36
+
let gen = Term.makeGen()
37
+
switch deserialise(props.imports.facts, gen, props.content) {
38
+
| Ok(state) => {
39
+
props.onLoad(~exports={facts: Dict.fromArray([(state.name,state.rule)]), ruleStyle: None})
40
+
<RuleView rule={state.rule} scope={[]}
41
+
style={props.imports.ruleStyle->Option.getOr(Hybrid)}>
42
+
{React.string(state.name)}
43
+
</RuleView>
44
+
}
45
+
| Error(err) => <div className="error"> {React.string(err)} </div>
46
+
}
47
+
}
48
+
}
-7
src/componentgraph.ts
-7
src/componentgraph.ts
···
97
97
})
98
98
}
99
99
if (awaiting.length == 0) {
100
-
console.trace();
101
-
console.log("MAKING", this.url)
102
100
this.component = new maker(textual, {},
103
101
(msg) => { this.notifySubscribers(msg) }, (msg) => {
104
-
console.log("LOADED", this.url)
105
102
this.status = "ready";
106
103
for (let sub of this.subscribers) {
107
104
sub.dependencyReady(this.url);
···
110
107
}
111
108
}
112
109
this.dependencyReady = function(url) {
113
-
console.log("READY",this.url,url)
114
110
let index = awaiting.indexOf(url);
115
111
if (index > -1) {
116
112
awaiting.splice(index, 1);
···
124
120
deps2[dep] = v;
125
121
}
126
122
}
127
-
console.trace();
128
-
console.log("MAKING", this.url)
129
123
this.component = new maker(textual, deps2,
130
124
(msg) => { this.notifySubscribers(msg) }, (msg) => {
131
-
console.log("LOADED", this.url)
132
125
this.status = "ready";
133
126
for (let sub of this.subscribers) {
134
127
sub.dependencyReady(this.url);
+2
-3
src/testcomponent.tsx
+2
-3
src/testcomponent.tsx
···
1
1
import * as ComponentGraph from './componentgraph'
2
-
import { AxiomS, Conf, TheoremS } from './Scratch.mjs'
2
+
import { AxiomS, ConfS, TheoremS } from './Scratch.mjs'
3
3
import ReactDOM from 'react-dom/client';
4
4
import React from 'react';
5
5
···
25
25
let ret = RComp.Ports.empty
26
26
for (const x in this.deps) {
27
27
if ("exports" in this.deps[x]) {
28
-
console.log(x,this.deps[x])
29
28
ret = RComp.Ports.combine(ret,this.deps[x]["exports"])
30
29
}
31
30
}
···
73
72
window.localStorage.clear()
74
73
ComponentGraph.setup({
75
74
"hol-comp": HolComp(AxiomS),
76
-
"hol-config":HolComp(Conf),
75
+
"hol-config":HolComp(ConfS),
77
76
"hol-proof": HolComp(TheoremS)
78
77
});//"hol-config": ConfigComponent, "hol-proof":ProofComponent});