the next generation of the in-browser educational proof assistant
refactor component interface
+154
-145
+25
-41
src/AxiomSet.res
+25
-41
src/AxiomSet.res
···
8
8
module Rule = Rule.Make(Term, Judgment)
9
9
module RuleView = RuleView.Make(Term, Judgment, JudgmentView)
10
10
module Ports = Ports(Term, Judgment)
11
+
type state = dict<Rule.t>
11
12
type props = {
12
-
content: string,
13
+
content: state,
13
14
imports: Ports.t,
14
-
onLoad: (~exports: Ports.t, ~string: string=?) => unit,
15
-
onChange: (string, ~exports: Ports.t) => unit,
15
+
onChange: (state, ~exports: Ports.t) => unit,
16
16
}
17
17
18
-
let deserialise = (str: string) => {
18
+
let serialise = (state: state) => {
19
+
state->Dict.toArray->Array.map(((k, r)) => r->Rule.prettyPrintTopLevel(~name=k))->Array.join("\n")
20
+
}
21
+
let deserialise = (str: string, ~imports: Ports.t) => {
19
22
let cur = ref(str)
20
23
let go = ref(true)
21
24
let results = Dict.make()
···
41
44
}
42
45
}
43
46
}
44
-
ret.contents
47
+
ret.contents->Result.map(state => (state, {Ports.facts: state, ruleStyle: None}))
45
48
}
46
49
47
-
let make = props => {
48
-
switch deserialise(props.content) {
49
-
| Ok(s) => {
50
-
React.useEffect(() => {
51
-
// Run effects
52
-
props.onLoad(~exports={Ports.facts: s, ruleStyle: None})
53
-
None // or Some(() => {})
54
-
}, [])
55
-
56
-
<div
57
-
className={"axiom-set axiom-set-"->String.concat(
58
-
String.make(props.imports.ruleStyle->Option.getOr(Hybrid)),
59
-
)}>
60
-
{Dict.toArray(s)
61
-
->Array.mapWithIndex(((n, r), i) =>
62
-
<RuleView
63
-
rule={r}
64
-
scope={[]}
65
-
key={String.make(i)}
66
-
style={props.imports.ruleStyle->Option.getOr(Hybrid)}>
67
-
{React.string(n)}
68
-
//<Name content={n} onChange={(_) => Error("BLAH!")} />
69
-
</RuleView>
70
-
)
71
-
->React.array}
72
-
</div>
73
-
}
74
-
| Error(e) => {
75
-
React.useEffect(() => {
76
-
// Run effects
77
-
props.onLoad(~exports={Ports.facts: Dict.make(), ruleStyle: None})
78
-
None // or Some(() => {})
79
-
}, [])
80
-
<div className="error"> {React.string(e)} </div>
81
-
}
82
-
}
50
+
let make = props => {
51
+
<div
52
+
className={"axiom-set axiom-set-"->String.concat(
53
+
String.make(props.imports.ruleStyle->Option.getOr(Hybrid)),
54
+
)}>
55
+
{Dict.toArray(props.content)
56
+
->Array.mapWithIndex(((n, r), i) =>
57
+
<RuleView
58
+
rule={r}
59
+
scope={[]}
60
+
key={String.make(i)}
61
+
style={props.imports.ruleStyle->Option.getOr(Hybrid)}>
62
+
{React.string(n)}
63
+
</RuleView>
64
+
)
65
+
->React.array}
66
+
</div>
83
67
}
84
68
}
+7
-3
src/Component.res
+7
-3
src/Component.res
···
14
14
{facts, ruleStyle}
15
15
}
16
16
}
17
+
17
18
module type COMPONENT = {
18
19
module Ports: PORTS
20
+
type state
19
21
type props = {
20
-
content: string,
22
+
content: state,
21
23
imports: Ports.t,
22
-
onLoad: (~exports: Ports.t, ~string: string=?) => unit,
23
-
onChange: (string, ~exports: Ports.t) => unit,
24
+
/* onLoad: (~exports: Ports.t, ~string: string=?) => unit, */
25
+
onChange: (state, ~exports: Ports.t) => unit,
24
26
}
27
+
let serialise: state => string
28
+
let deserialise: (string, ~imports: Ports.t) => result<(state,Ports.t),string>
25
29
let make: props => React.element
26
30
}
+22
-16
src/ConfigBlock.res
+22
-16
src/ConfigBlock.res
···
5
5
module Ports = Ports(Term, Judgment)
6
6
open RuleView
7
7
type props = {
8
-
content: string,
8
+
content: style,
9
9
imports: Ports.t,
10
-
onLoad: (~exports: Ports.t) => unit,
11
-
onChange: (string, ~exports: Ports.t) => unit,
10
+
onChange: (style, ~exports: Ports.t) => unit,
12
11
}
13
12
let deserialise = str =>
14
13
switch str {
15
-
| "Gentzen" => Gentzen
16
-
| "Linear" => Linear
17
-
| "Hybrid" => Hybrid
18
-
| _ => Hybrid
14
+
| "Gentzen" => Ok((Gentzen, Ports.empty))
15
+
| "Linear" => Ok((Linear, Ports.empty))
16
+
| "Hybrid" => Ok((Hybrid, Ports.empty))
17
+
| _ => Error("unknown rule style")
19
18
}
19
+
let serialise = style => switch style {
20
+
| Gentzen => "Gentzen"
21
+
| Linear => "Linear"
22
+
| Hybrid => "Hybrid"
23
+
}
24
+
25
+
20
26
let make = props => {
21
-
let (style, setStyle) = React.useState(_ => deserialise(props.content))
22
-
React.useEffect(() => {
23
-
props.onLoad(~exports={Ports.facts: Dict.make(), ruleStyle: Some(style)})
24
-
None
25
-
}, [])
27
+
let (style, setStyle) = React.useState(_ => props.content)
26
28
let onChange = e => {
27
29
let target = JsxEvent.Form.target(e)
28
30
let value: string = target["value"]
29
-
let sty = deserialise(value)
30
-
setStyle(_ => sty)
31
-
32
-
props.onChange(value, ~exports={Ports.facts: Dict.make(), ruleStyle: Some(sty)})
31
+
switch deserialise(value) {
32
+
| Ok((sty,_)) => {
33
+
setStyle(_ => sty)
34
+
props.onChange(sty, ~exports={Ports.facts: Dict.make(), ruleStyle: Some(sty)})
35
+
}
36
+
| Error(_) => ()
37
+
}
38
+
33
39
}
34
40
[Gentzen, Linear, Hybrid]
35
41
->Array.map(n =>
+53
-24
src/Editable.res
+53
-24
src/Editable.res
···
3
3
module TextArea = (Underlying: COMPONENT) => {
4
4
module Ports = Underlying.Ports
5
5
type props = {
6
-
content: string,
6
+
content: result<Underlying.state,(string, string)>,
7
7
imports: Ports.t,
8
-
onLoad: (~exports: Ports.t, ~string: string=?) => unit,
9
-
onChange: (string, ~exports: Ports.t) => unit,
8
+
onChange: (result<Underlying.state, (string,string)>, ~exports: Ports.t) => unit,
9
+
}
10
+
type state = result<Underlying.state,(string,string)>
11
+
12
+
let serialise = state => switch state {
13
+
| Ok(s) => Underlying.serialise(s)
14
+
| Error((err,str)) => str
15
+
}
16
+
let deserialise = (str: string, ~imports: Ports.t) => {
17
+
switch Underlying.deserialise(str,~imports) {
18
+
| Ok((s,e)) => Ok(Ok(s),e)
19
+
| Error(e) => Ok(Error(e,str),Ports.empty)
20
+
}
10
21
}
11
22
let make = props => {
12
23
let (editing, setEditing) = React.useState(_ => false)
13
-
let (text, setText) = React.useState(_ => props.content)
24
+
let (text, setText) = React.useState(_ => serialise(props.content))
14
25
let onTextChange = (ev: JsxEvent.Form.t) => {
15
26
let target = JsxEvent.Form.target(ev)
16
27
let value: string = target["value"]
17
-
setText(_ => value)
28
+
setText(_ => value)
18
29
}
19
30
let done = _ => {
31
+
switch deserialise(text, ~imports=props.imports) {
32
+
| Ok((st,ex)) => {
33
+
props.onChange(st,~exports=ex)
34
+
}
35
+
| Error(e) => Console.log("Impossible happened")
36
+
}
20
37
setEditing(_ => false)
21
38
}
22
39
if editing {
···
29
46
</div>
30
47
</div>
31
48
} else {
32
-
<div>
33
-
<Underlying
34
-
content={text}
35
-
imports={props.imports}
36
-
onLoad={(~exports, ~string=?) => {
37
-
props.onLoad(~exports, ~string=string->Option.getOr(text))
38
-
}}
39
-
onChange={(string, ~exports) => {
40
-
setText(_ => string)
41
-
props.onChange(string, ~exports)
42
-
}}
43
-
/>
44
-
<div className="editor-controls">
45
-
<span
46
-
className="editor-button button-icon button-icon-blue typcn typcn-edit"
47
-
onClick={_ => setEditing(_ => true)}
48
-
/>
49
-
</div>
50
-
</div>
49
+
switch props.content {
50
+
|Ok(us) =>
51
+
<div>
52
+
<Underlying
53
+
content={us}
54
+
imports={props.imports}
55
+
/* onLoad={(~exports, ~string=?) =>
56
+
props.onLoad(~exports, ~string=string->Option.getOr(Underlying.serialise(us)))} */
57
+
onChange={(state, ~exports) => {
58
+
props.onChange(Ok(state), ~exports)
59
+
}}
60
+
/>
61
+
<div className="editor-controls">
62
+
<span
63
+
className="editor-button button-icon button-icon-blue typcn typcn-edit"
64
+
onClick={_ => { setText(_ => serialise(props.content)); setEditing(_ => true)}}
65
+
/>
66
+
</div>
67
+
</div>
68
+
| Error((err, str)) => {
69
+
<div>
70
+
<div className="error"> {React.string(err)} </div>
71
+
<div className="editor-controls">
72
+
<span
73
+
className="editor-button button-icon button-icon-blue typcn typcn-edit"
74
+
onClick={_ => { setText(_ => serialise(props.content)); setEditing(_ => true)}}
75
+
/>
76
+
</div>
77
+
</div>
78
+
}
79
+
}
51
80
}
52
81
}
53
82
}
+1
-1
src/Method.res
+1
-1
src/Method.res
···
261
261
let substitute = (it, subst) =>
262
262
switch it {
263
263
| First(m) => First(Method1.substitute(m, subst))
264
-
| Second(m) => Second(Method2.substitute(m, subst))
264
+
| Second(m) => Second(Method2.substitute(m, f))
265
265
}
266
266
let keywords = Array.concat(Method1.keywords, Method2.keywords)
267
267
let apply = (ctx: Context.t, j: Judgment.t, gen: Term.gen, f: Rule.t => 'a) => {
+23
-33
src/Theorem.res
+23
-33
src/Theorem.res
···
14
14
open RuleView
15
15
module RuleView = RuleView.Make(Term, Judgment, JudgmentView)
16
16
module Ports = Ports(Term, Judgment)
17
+
type state = {name: string, rule: Rule.t, proof: Proof.t}
17
18
type props = {
18
-
content: string,
19
+
content: state,
19
20
imports: Ports.t,
20
-
onLoad: (~exports: Ports.t, ~string: string=?) => unit,
21
-
onChange: (string, ~exports: Ports.t) => unit,
21
+
onChange: (state, ~exports: Ports.t) => unit,
22
22
}
23
-
type state = {name: string, rule: Rule.t, proof: Proof.checked}
24
-
let deserialise = (facts: Dict.t<Rule.t>, gen: Term.gen, str: string): result<state, string> => {
23
+
let serialise = (state: state) => {
24
+
state.rule->Rule.prettyPrintTopLevel(~name=state.name)
25
+
->String.concat(Proof.prettyPrint(state.proof,~scope=[]))
26
+
}
27
+
let deserialise = (str: string, ~imports: Ports.t) => {
28
+
let facts = imports.facts
29
+
let gen = Term.makeGen()
25
30
let cur = ref(str)
26
31
switch Rule.parseTopLevel(cur.contents, ~scope=[], ~gen) {
27
32
| Error(e) => Error(e)
28
-
| Ok(((r, n), s)) =>
33
+
| Ok(((rule, name), s)) =>
29
34
switch Proof.parse(s, ~scope=[], ~gen) {
30
35
| Error(e) => Error(e)
31
36
| Ok((_, s')) if String.length(String.trim(s')) > 0 =>
32
37
Error("Trailing input: "->String.concat(s'))
33
-
| Ok((prf, _)) => {
34
-
let ctx: Context.t = {fixes: [], facts}
35
-
Ok({name: n, rule: r, proof: Proof.check(ctx, prf, r)})
38
+
| Ok((proof, _)) => {
39
+
Ok(({name, rule, proof}, {Ports.facts: Dict.fromArray([(name,rule)]), ruleStyle: None}))
36
40
}
37
41
}
38
42
}
39
43
}
40
44
let make = props => {
41
-
let gen = Term.makeGen()
42
-
switch deserialise(props.imports.facts, gen, props.content) {
43
-
| Ok(state) => {
44
-
React.useEffect(() => {
45
-
let export = Dict.fromArray([(state.name, state.rule)])
46
-
props.onLoad(~exports={Ports.facts: export, ruleStyle: None})
47
-
None
48
-
}, [])
49
-
let ruleStyle = props.imports.ruleStyle->Option.getOr(Hybrid)
50
-
<>
51
-
<RuleView rule={state.rule} scope={[]} style={ruleStyle}>
52
-
{React.string(state.name)}
53
-
</RuleView>
54
-
<ProofView ruleStyle={ruleStyle} scope={[]} proof=state.proof />
55
-
</>
56
-
}
57
-
| Error(err) => {
58
-
React.useEffect(() => {
59
-
props.onLoad(~exports={Ports.facts: Dict.make(), ruleStyle: None})
60
-
None
61
-
}, [])
62
-
<div className="error"> {React.string(err)} </div>
63
-
}
64
-
}
45
+
Console.log(props.imports)
46
+
let ruleStyle = props.imports.ruleStyle->Option.getOr(Hybrid)
47
+
let ctx: Context.t = {fixes: [], facts: props.imports.facts}
48
+
let checked = Proof.check(ctx, props.content.proof, props.content.rule)
49
+
<>
50
+
<RuleView rule={props.content.rule} scope={[]} style={ruleStyle}>
51
+
{React.string(props.content.name)}
52
+
</RuleView>
53
+
<ProofView ruleStyle={ruleStyle} scope={[]} proof=checked />
54
+
</>
65
55
}
66
56
}
+23
-27
src/testcomponent.tsx
+23
-27
src/testcomponent.tsx
···
17
17
exports : Record<string,any>;
18
18
loaded: boolean;
19
19
root : ReactDOM.Root;
20
-
stringRep:string;
20
+
state: any;
21
21
toString() {
22
-
return this.stringRep
22
+
return RComp.serialise(this.state)
23
23
}
24
24
gatherImports() {
25
25
let ret = RComp.Ports.empty
···
28
28
ret = RComp.Ports.combine(ret,this.deps[x]["exports"])
29
29
}
30
30
}
31
-
console.log("EXPORTS",ret)
32
31
return ret
33
32
}
34
-
render(signal : (msg: any) => void,loaded : (msg: any) => void) {
33
+
render(signal : (msg: any) => void) {
35
34
let Tag = RComp.make
36
35
this.root.render(
37
-
<Tag content={this.stringRep} imports={this.gatherImports()}
38
-
onChange={ (str, exports) => {
36
+
<Tag content={this.state} imports={this.gatherImports()}
37
+
onChange={ (state, exports) => {
39
38
this.exports = exports
40
-
this.stringRep = str;
39
+
this.state = state;
41
40
signal(null)
42
-
this.render(signal, loaded)
43
-
}}
44
-
onLoad={ (exports,str) => {
45
-
this.exports = exports
46
-
if (str) {
47
-
this.stringRep = str;
48
-
}
49
-
if (!this.loaded) {
50
-
this.loaded = true;
51
-
loaded(null)
52
-
} else {
53
-
signal(null)
54
-
}
55
-
}}
41
+
this.render(signal)
42
+
}}
56
43
/>
57
44
)
58
45
}
59
46
constructor(str: string,deps : Record<string,Component>, signal : (msg: any) => void, loaded : (msg: any) => void, view? : HTMLElement) {
60
47
this.deps = deps
61
-
this.stringRep = str
62
48
this.loaded = false
63
49
if (view != null) {
64
50
const newDiv = document.createElement("div");
···
66
52
view.appendChild(newDiv);
67
53
this.root = ReactDOM.createRoot(newDiv);
68
54
}
69
-
this.render(signal,loaded)
70
-
this.dependencyChanged = (_depName, _comp) => {
71
-
this.render(signal, loaded)
72
-
};
55
+
const imports = this.gatherImports();
56
+
var foo = RComp.deserialise(str,imports)
57
+
if (foo.TAG == "Ok") {
58
+
this.exports = foo._0[1]
59
+
this.state = foo._0[0]
60
+
this.dependencyChanged = (_depName, _comp) => {
61
+
this.render(signal)
62
+
};
63
+
loaded(null)
64
+
this.loaded = true;
65
+
this.render(signal)
66
+
} else {
67
+
view.innerHTML = foo._0
68
+
}
73
69
}
74
70
}
75
71
···
80
76
"hol-comp": HolComp(AxiomS),
81
77
"hol-config":HolComp(ConfS),
82
78
"hol-proof": HolComp(TheoremS)
83
-
});//"hol-config": ConfigComponent, "hol-proof":ProofComponent});
79
+
});