the next generation of the in-browser educational proof assistant
fix bug with component loading updates, basic proof view
+198
-35
+2
-2
src/AxiomSet.res
+2
-2
src/AxiomSet.res
···
7
7
module Rule = Rule.Make(Term,Judgment)
8
8
module RuleView = RuleView.Make(Term,Judgment,JudgmentView)
9
9
module Ports = Ports(Term,Judgment)
10
-
type props = { content: string, imports: Ports.t, onLoad: (~exports:Ports.t) => (), onChange: (string,~exports:Ports.t) => () }
10
+
type props = { content: string, imports: Ports.t, onLoad: (~exports:Ports.t,~string:string=?) => (), onChange: (string,~exports:Ports.t) => () }
11
11
12
12
let deserialise = (str: string) => {
13
13
let cur = ref(str)
···
40
40
switch deserialise(props.content) {
41
41
| Ok(s) => {
42
42
React.useEffect(() => {
43
-
// Run effects
43
+
// Run effects
44
44
props.onLoad(~exports= {Ports.facts: s, ruleStyle: None});
45
45
None // or Some(() => {})
46
46
}, [])
+1
-1
src/Component.res
+1
-1
src/Component.res
···
16
16
}
17
17
module type COMPONENT = {
18
18
module Ports : PORTS
19
-
type props = { content: string, imports: Ports.t, onLoad: (~exports:Ports.t) => (),onChange: (string,~exports:Ports.t) => () }
19
+
type props = { content: string, imports: Ports.t, onLoad: (~exports:Ports.t, ~string:string=?) => (),onChange: (string,~exports:Ports.t) => () }
20
20
let make : props => React.element
21
21
}
+4
-2
src/Editable.res
+4
-2
src/Editable.res
···
2
2
3
3
module TextArea = (Underlying : COMPONENT) => {
4
4
module Ports = Underlying.Ports
5
-
type props = { content: string, imports: Ports.t, onLoad: (~exports:Ports.t) => (), onChange: (string,~exports:Ports.t) => () }
5
+
type props = { content: string, imports: Ports.t, onLoad: (~exports:Ports.t, ~string:string=?) => (), onChange: (string,~exports:Ports.t) => () }
6
6
let make = (props) => {
7
7
let (editing,setEditing) = React.useState (_ => false)
8
8
let (text,setText) = React.useState (_ => props.content)
···
27
27
<Underlying
28
28
content={text}
29
29
imports={props.imports}
30
-
onLoad={props.onLoad}
30
+
onLoad={(~exports,~string=?) => {
31
+
props.onLoad(~exports,~string=string->Option.getOr(text))
32
+
}}
31
33
onChange={(string, ~exports) => {
32
34
setText(_=>string)
33
35
props.onChange(string,~exports)
+72
src/MethodView.res
+72
src/MethodView.res
···
1
+
open Util
2
+
open Signatures
3
+
open Method
4
+
module type METHOD_VIEW = {
5
+
module Term : TERM
6
+
module Judgment : JUDGMENT with module Term := Term
7
+
module Method : PROOF_METHOD with
8
+
module Term := Term and
9
+
module Judgment := Judgment
10
+
type props<'a> = {method: Method.t<'a>, scope: array<Term.meta>, ruleStyle: RuleView.style}
11
+
type srProps<'a> = {"proof": 'a, "scope": array<Term.meta>, "ruleStyle": RuleView.style}
12
+
let make : (srProps<'a> => React.element) => props<'a> => React.element
13
+
}
14
+
15
+
module DerivationView = (
16
+
Term : TERM, Judgment : JUDGMENT with module Term := Term
17
+
) => {
18
+
module Method = Derivation(Term, Judgment)
19
+
type props<'a> = {method: Method.t<'a>, scope: array<Term.meta>, ruleStyle: RuleView.style}
20
+
type srProps<'a> = {"proof": 'a, "scope": array<Term.meta>, "ruleStyle": RuleView.style}
21
+
let make = (subRender : srProps<'a> => React.element) => (props) => {
22
+
<div>
23
+
<b>{React.string("by ")}</b>
24
+
{React.string(props.method.ruleName)}
25
+
<ul>
26
+
{ props.method.subgoals->Array.mapWithIndex((sg,i) => {
27
+
<li key={String.make(i)}>
28
+
{React.createElement(subRender, {"proof":sg, "scope": props.scope, "ruleStyle": props.ruleStyle})}
29
+
</li>
30
+
})->React.array
31
+
}
32
+
</ul>
33
+
</div>
34
+
}
35
+
}
36
+
37
+
module LemmaView = (
38
+
Term : TERM, Judgment : JUDGMENT with module Term := Term,
39
+
JudgmentView : JUDGMENT_VIEW with module Term := Term and module Judgment := Judgment
40
+
) => {
41
+
module Method = Lemma(Term, Judgment)
42
+
type props<'a> = {method: Method.t<'a>, scope: array<Term.meta>, ruleStyle: RuleView.style}
43
+
type srProps<'a> = {"proof": 'a, "scope": array<Term.meta>, "ruleStyle": RuleView.style}
44
+
module RuleView = RuleView.Make(Term,Judgment, JudgmentView)
45
+
let make = (subRender : srProps<'a> => React.element) => (props) => {
46
+
<div>
47
+
<b>{React.string("have ")}</b>
48
+
<RuleView
49
+
rule={props.method.rule}
50
+
scope={props.scope}
51
+
style={props.ruleStyle}> {React.null}
52
+
</RuleView>
53
+
{React.createElement(subRender,{"proof":props.method.proof, "scope": props.scope, "ruleStyle": props.ruleStyle})}
54
+
{React.createElement(subRender,{"proof":props.method.show, "scope": props.scope, "ruleStyle": props.ruleStyle})}
55
+
</div>
56
+
}
57
+
}
58
+
module CombineMethodView = (
59
+
Term : TERM, Judgment : JUDGMENT with module Term := Term,
60
+
Method1View : METHOD_VIEW with module Term := Term and module Judgment := Judgment,
61
+
Method2View : METHOD_VIEW with module Term := Term and module Judgment := Judgment and type srProps<'a> = Method1View.srProps<'a>
62
+
) => {
63
+
module Method = Combine(Term,Judgment,Method1View.Method, Method2View.Method)
64
+
type props<'a> = {method: Method.t<'a>, scope: array<Term.meta>, ruleStyle: RuleView.style}
65
+
type srProps<'a> = Method1View.srProps<'a>
66
+
let make = (subrender : srProps<'a> => React.element) => (props) => {
67
+
switch props.method {
68
+
| First(m) => Method1View.make(subrender)({method:m, scope:props.scope, ruleStyle: props.ruleStyle})
69
+
| Second(m) => Method2View.make(subrender)({method:m, scope:props.scope, ruleStyle: props.ruleStyle})
70
+
}
71
+
}
72
+
}
+57
src/ProofView.res
+57
src/ProofView.res
···
1
+
open Signatures
2
+
open Method
3
+
open MethodView
4
+
5
+
module Make = (
6
+
Term : TERM, Judgment : JUDGMENT with module Term := Term,
7
+
JudgmentView : JUDGMENT_VIEW with module Term := Term and module Judgment := Judgment,
8
+
MethodView : METHOD_VIEW with module Term := Term and module Judgment := Judgment
9
+
) => {
10
+
module Rule = Rule.Make(Term, Judgment)
11
+
module ScopeView = ScopeView.Make(Term, JudgmentView.TermView)
12
+
module Proof = Proof.Make(Term, Judgment, MethodView.Method)
13
+
14
+
type props = {
15
+
proof: Proof.checked,
16
+
scope: array<Term.meta>,
17
+
ruleStyle: RuleView.style
18
+
}
19
+
module RuleView = RuleView.Make(Term, Judgment, JudgmentView)
20
+
@react.componentWithProps
21
+
let rec make = (props : props) => {
22
+
switch props.proof {
23
+
| Proof.Checked({fixes, assumptions, method, rule}) => {
24
+
let scope = Array.concat(fixes,props.scope)
25
+
<>
26
+
<ScopeView scope=fixes />
27
+
<ul className="proof-assumptions">
28
+
{ Belt.Array.zipBy(assumptions,rule.premises, (n,r) => {
29
+
<li key={n}>
30
+
<RuleView rule=r style=props.ruleStyle scope>
31
+
{React.string(n)}
32
+
</RuleView>
33
+
</li>
34
+
})->React.array
35
+
}
36
+
</ul>
37
+
<div className="proof-show">
38
+
<JudgmentView judgment={rule.conclusion} scope />
39
+
{
40
+
switch method {
41
+
| None => React.null
42
+
| Some(method) => React.createElement(
43
+
MethodView.make(p => make({proof: p["proof"], scope: p["scope"], ruleStyle:p["ruleStyle"] })),
44
+
{method, scope, ruleStyle: props.ruleStyle})
45
+
}
46
+
}
47
+
</div>
48
+
</>
49
+
}
50
+
| Proof.ProofError({raw:_, rule:_, msg}) => {
51
+
<div className="error">{React.string(msg)}</div>
52
+
}
53
+
54
+
}
55
+
}
56
+
57
+
}
+6
-17
src/RuleView.res
+6
-17
src/RuleView.res
···
7
7
JudgmentView : JUDGMENT_VIEW with module Term := Term and module Judgment := Judgment
8
8
) => {
9
9
module Rule = Rule.Make(Term, Judgment)
10
-
10
+
module ScopeView = ScopeView.Make(Term, JudgmentView.TermView)
11
11
type props = {
12
12
rule:Rule.t,
13
13
style: style,
···
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.mapWithIndex((m,i) =>
25
-
<React.Fragment key={String.make(i)}>{JudgmentView.TermView.makeMeta(m)}</React.Fragment>
26
-
)
27
-
Array.reverse(arr)
28
24
<span className="inline-rule">
29
25
<span className="rule-rulename-defined">
30
26
{props.children}
31
27
</span>
32
-
{if Array.length(arr) > 0 { <span className="rule-binders">{React.array(arr)}</span> }
33
-
else { React.string("") }}
28
+
<ScopeView scope=vars />
34
29
{React.array(premises
35
30
->Array.mapWithIndex((p,i)=><span key={String.make(i)} className="rule-context">
36
31
{React.createElement(make,withKey({rule:p, scope,children:React.string(""),style:props.style}, i))}</span>)
···
55
50
module Hypothetical = (Premise : RULE_COMPONENT) => {
56
51
let make = (props : props) => if Array.length(props.rule.premises) == 0 { Inline.make(props) } else {
57
52
let {vars, premises,conclusion} = props.rule
58
-
let arr = vars->Array.mapWithIndex((m,i) =>
59
-
<React.Fragment key={String.make(i)}>{JudgmentView.TermView.makeMeta(m)}</React.Fragment>
60
-
)
61
-
Array.reverse(arr)
62
53
let scope = vars->Array.concat(props.scope->Option.getOr([]))
63
54
<table className="inference"><tbody>
64
-
<tr><td className="rule-cell rule-binderbox" rowSpan=3>{React.array(arr)}</td>
55
+
<tr><td className="rule-cell rule-binderbox" rowSpan=3>
56
+
<ScopeView scope=vars/></td>
65
57
{React.array(premises->Array.mapWithIndex((p,i)=>
66
58
<td className="rule-cell rule-premise" key={String.make(i)}>
67
59
<Premise rule={p} scope={scope} key={String.make(i)} style={props.style}>
···
88
80
module TopLevel = (Premise : RULE_COMPONENT) => {
89
81
let make = (props : props) => {
90
82
let {vars, premises,conclusion} = props.rule
91
-
let arr = vars->Array.mapWithIndex((m,i) =>
92
-
<React.Fragment key={String.make(i)}>{JudgmentView.TermView.makeMeta(m)}</React.Fragment>
93
-
)
94
-
Array.reverse(arr)
95
83
let scope = vars->Array.concat(props.scope->Option.getOr([]))
96
84
<div className="axiom"><table className="inference"><tbody>
97
-
<tr><td className="rule-cell rule-binderbox" rowSpan=2>{React.array(arr)}</td>
85
+
<tr><td className="rule-cell rule-binderbox" rowSpan=2>
86
+
<ScopeView scope=vars/></td>
98
87
{React.array(premises->Array.mapWithIndex((p,i)=>
99
88
<td className="rule-cell rule-premise" key={String.make(i)}>
100
89
<Premise rule={p} scope={scope} key={String.make(i)} style={props.style}>
+23
src/ScopeView.res
+23
src/ScopeView.res
···
1
+
open Signatures
2
+
3
+
module Make = (
4
+
Term : TERM,
5
+
TermView : TERM_VIEW with module Term := Term
6
+
) => {
7
+
type props = { scope: array<Term.meta> }
8
+
@react.componentWithProps
9
+
let make = (props) => {
10
+
let arr = props.scope->Array.mapWithIndex((m,i) =>
11
+
<React.Fragment key={String.make(i)}>
12
+
{TermView.makeMeta(m)}
13
+
</React.Fragment>)
14
+
Array.reverse(arr)
15
+
if Array.length(arr) > 0 {
16
+
<span className="rule-binders">
17
+
{React.array(arr)}
18
+
</span>
19
+
} else {
20
+
React.null
21
+
}
22
+
}
23
+
}
+2
-2
src/Scratch.res
+2
-2
src/Scratch.res
···
1
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))
2
+
module DerivationsOrLemmasView = MethodView.CombineMethodView(SExp,SExp,MethodView.DerivationView(SExp,SExp),MethodView.LemmaView(SExp,SExp,SExpJView))
3
+
module TheoremS = Editable.TextArea(Theorem.Make(SExp,SExp,SExpJView,DerivationsOrLemmasView))
4
4
module ConfS = ConfigBlock.Make(SExp,SExp)
5
5
+23
-10
src/Theorem.res
+23
-10
src/Theorem.res
···
1
1
open Signatures
2
2
open Component
3
-
open Method
3
+
open MethodView
4
4
module Make = (
5
5
Term : TERM,
6
6
Judgment : JUDGMENT with module Term := Term,
7
7
JudgmentView : JUDGMENT_VIEW with module Term := Term and module Judgment := Judgment,
8
-
Method : PROOF_METHOD with module Term := Term and module Judgment := Judgment
8
+
MethodView : METHOD_VIEW with module Term := Term and module Judgment := Judgment
9
9
) => {
10
10
module Rule = Rule.Make(Term,Judgment)
11
-
module Proof = Proof.Make(Term,Judgment,Method)
12
-
module Context = Context(Term,Judgment)
13
-
11
+
module Proof = Proof.Make(Term,Judgment,MethodView.Method)
12
+
module Context = Method.Context(Term,Judgment)
13
+
module ProofView = ProofView.Make(Term,Judgment,JudgmentView,MethodView)
14
14
open RuleView
15
15
module RuleView = RuleView.Make(Term,Judgment,JudgmentView)
16
16
module Ports = Ports(Term,Judgment)
17
-
type props = { content: string, imports: Ports.t, onLoad: (~exports:Ports.t) => (), onChange: (string,~exports:Ports.t) => () }
17
+
type props = { content: string, imports: Ports.t, onLoad: (~exports:Ports.t,~string:string=?) => (), onChange: (string,~exports:Ports.t) => () }
18
18
type state = {name: string, rule: Rule.t, proof: Proof.checked}
19
19
let deserialise = (facts : Dict.t<Rule.t>, gen : Term.gen, str : string) : result<state,string> => {
20
20
let cur = ref(str)
···
36
36
let gen = Term.makeGen()
37
37
switch deserialise(props.imports.facts, gen, props.content) {
38
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)}>
39
+
React.useEffect(() => {
40
+
let export = Dict.fromArray([(state.name,state.rule)])
41
+
props.onLoad(~exports= {Ports.facts: export, ruleStyle: None});
42
+
None
43
+
}, [])
44
+
let ruleStyle = props.imports.ruleStyle->Option.getOr(Hybrid)
45
+
<>
46
+
<RuleView rule={state.rule} scope={[]} style={ruleStyle}>
42
47
{React.string(state.name)}
43
48
</RuleView>
49
+
<ProofView ruleStyle={ruleStyle} scope={[]} proof=state.proof />
50
+
</>
44
51
}
45
-
| Error(err) => <div className="error"> {React.string(err)} </div>
52
+
| Error(err) => {
53
+
React.useEffect(() => {
54
+
props.onLoad(~exports={Ports.facts: Dict.make(), ruleStyle: None});
55
+
None
56
+
}, [])
57
+
<div className="error"> {React.string(err)} </div>
58
+
}
46
59
}
47
60
}
48
61
}
+1
src/componentgraph.ts
+1
src/componentgraph.ts
+7
-1
src/testcomponent.tsx
+7
-1
src/testcomponent.tsx
···
28
28
ret = RComp.Ports.combine(ret,this.deps[x]["exports"])
29
29
}
30
30
}
31
+
console.log("EXPORTS",ret)
31
32
return ret
32
33
}
33
34
render(signal : (msg: any) => void,loaded : (msg: any) => void) {
···
40
41
signal(null)
41
42
this.render(signal, loaded)
42
43
}}
43
-
onLoad={ (exports) => {
44
+
onLoad={ (exports,str) => {
44
45
this.exports = exports
46
+
if (str) {
47
+
this.stringRep = str;
48
+
}
45
49
if (!this.loaded) {
46
50
this.loaded = true;
47
51
loaded(null)
52
+
} else {
53
+
signal(null)
48
54
}
49
55
}}
50
56
/>