the next generation of the in-browser educational proof assistant
extremely barebones proof construction UI
+73
-33
+1
-1
src/AxiomSet.res
+1
-1
src/AxiomSet.res
+1
-1
src/Component.res
+1
-1
src/Component.res
···
22
22
content: state,
23
23
imports: Ports.t,
24
24
/* onLoad: (~exports: Ports.t, ~string: string=?) => unit, */
25
-
onChange: (state, ~exports: Ports.t) => unit,
25
+
onChange: (state, ~exports: Ports.t=?) => unit,
26
26
}
27
27
let serialise: state => string
28
28
let deserialise: (string, ~imports: Ports.t) => result<(state,Ports.t),string>
+1
-1
src/ConfigBlock.res
+1
-1
src/ConfigBlock.res
+3
-3
src/Editable.res
+3
-3
src/Editable.res
···
5
5
type props = {
6
6
content: result<Underlying.state,(string, string)>,
7
7
imports: Ports.t,
8
-
onChange: (result<Underlying.state, (string,string)>, ~exports: Ports.t) => unit,
8
+
onChange: (result<Underlying.state, (string,string)>, ~exports: Ports.t=?) => unit,
9
9
}
10
10
type state = result<Underlying.state,(string,string)>
11
11
···
54
54
imports={props.imports}
55
55
/* onLoad={(~exports, ~string=?) =>
56
56
props.onLoad(~exports, ~string=string->Option.getOr(Underlying.serialise(us)))} */
57
-
onChange={(state, ~exports) => {
58
-
props.onChange(Ok(state), ~exports)
57
+
onChange={(state, ~exports=?) => {
58
+
props.onChange(Ok(state), ~exports=?exports)
59
59
}}
60
60
/>
61
61
<div className="editor-controls">
+5
src/Method.res
+5
src/Method.res
···
183
183
| _ => Error("Incorrect number of binders")
184
184
}
185
185
}
186
+
let updateAtKey = (it: t<'a>, key: int, f: 'a => 'a) => {
187
+
let newsgs = [...it.subgoals]
188
+
newsgs->Array.set(key,f(newsgs[key]->Option.getExn))
189
+
{...it, subgoals: newsgs}
190
+
}
186
191
}
187
192
module Lemma = (Term: TERM, Judgment: JUDGMENT with module Term := Term) => {
188
193
module Rule = Rule.Make(Term, Judgment)
+38
-18
src/MethodView.res
+38
-18
src/MethodView.res
···
5
5
module Term: TERM
6
6
module Judgment: JUDGMENT with module Term := Term
7
7
module Method: PROOF_METHOD with module Term := Term and module Judgment := Judgment
8
-
type props<'a> = {method: Method.t<'a>, scope: array<Term.meta>, ruleStyle: RuleView.style}
9
-
type srProps<'a> = {"proof": 'a, "scope": array<Term.meta>, "ruleStyle": RuleView.style}
8
+
type props<'a> = {method: Method.t<'a>, scope: array<Term.meta>, ruleStyle: RuleView.style, gen: Term.gen, onChange: (Method.t<'a>, Term.subst) => ()}
9
+
type srProps<'a> = {"proof": 'a, "scope": array<Term.meta>, "ruleStyle": RuleView.style, "gen": Term.gen, "onChange": ('a, Term.subst) => ()}
10
10
let make: (srProps<'a> => React.element) => props<'a> => React.element
11
11
}
12
12
13
13
module DerivationView = (Term: TERM, Judgment: JUDGMENT with module Term := Term) => {
14
14
module Method = Derivation(Term, Judgment)
15
-
type props<'a> = {method: Method.t<'a>, scope: array<Term.meta>, ruleStyle: RuleView.style}
16
-
type srProps<'a> = {"proof": 'a, "scope": array<Term.meta>, "ruleStyle": RuleView.style}
15
+
type props<'a> = {method: Method.t<'a>, scope: array<Term.meta>, ruleStyle: RuleView.style, gen: Term.gen, onChange: (Method.t<'a>, Term.subst) => ()}
16
+
type srProps<'a> = {"proof": 'a, "scope": array<Term.meta>, "ruleStyle": RuleView.style, "gen": Term.gen, "onChange": ('a, Term.subst) => ()}
17
17
let make = (subRender: srProps<'a> => React.element) => props => {
18
18
<div>
19
19
<b> {React.string("by ")} </b>
···
24
24
<li key={String.make(i)}>
25
25
{React.createElement(
26
26
subRender,
27
-
{"proof": sg, "scope": props.scope, "ruleStyle": props.ruleStyle},
27
+
{"proof": sg, "scope": props.scope, "ruleStyle": props.ruleStyle, "gen": props.gen, "onChange": (newa, subst) =>
28
+
props.onChange(props.method->Method.updateAtKey(i, _ => newa), subst)
29
+
},
28
30
)}
29
31
</li>
30
32
})
···
40
42
JudgmentView: JUDGMENT_VIEW with module Term := Term and module Judgment := Judgment,
41
43
) => {
42
44
module Method = Lemma(Term, Judgment)
43
-
type props<'a> = {method: Method.t<'a>, scope: array<Term.meta>, ruleStyle: RuleView.style}
44
-
type srProps<'a> = {"proof": 'a, "scope": array<Term.meta>, "ruleStyle": RuleView.style}
45
+
type props<'a> = {
46
+
method: Method.t<'a>,
47
+
scope: array<Term.meta>,
48
+
ruleStyle: RuleView.style,
49
+
gen: Term.gen,
50
+
onChange: (Method.t<'a>, Term.subst) => ()
51
+
}
52
+
type srProps<'a> = {
53
+
"proof": 'a,
54
+
"scope": array<Term.meta>,
55
+
"ruleStyle": RuleView.style,
56
+
"gen":Term.gen,
57
+
"onChange": ('a, Term.subst) => ()
58
+
}
45
59
module RuleView = RuleView.Make(Term, Judgment, JudgmentView)
46
60
let make = (subRender: srProps<'a> => React.element) => props => {
47
61
<div>
···
49
63
<RuleView rule={props.method.rule} scope={props.scope} style={props.ruleStyle}>
50
64
{React.null}
51
65
</RuleView>
52
-
{React.createElement(
53
-
subRender,
54
-
{"proof": props.method.proof, "scope": props.scope, "ruleStyle": props.ruleStyle},
55
-
)}
56
-
{React.createElement(
57
-
subRender,
58
-
{"proof": props.method.show, "scope": props.scope, "ruleStyle": props.ruleStyle},
59
-
)}
66
+
{React.createElement(subRender, {
67
+
"proof": props.method.proof,
68
+
"scope": props.scope,
69
+
"ruleStyle": props.ruleStyle,
70
+
"gen": props.gen,
71
+
"onChange": (proof, subst) => { props.onChange({...props.method, proof}, subst) }
72
+
})}
73
+
{React.createElement(subRender, {
74
+
"proof": props.method.show,
75
+
"scope": props.scope,
76
+
"ruleStyle": props.ruleStyle,
77
+
"gen": props.gen,
78
+
"onChange": (show, subst) => { props.onChange({...props.method, show}, subst) }
79
+
})}
60
80
</div>
61
81
}
62
82
}
···
70
90
and type srProps<'a> = Method1View.srProps<'a>,
71
91
) => {
72
92
module Method = Combine(Term, Judgment, Method1View.Method, Method2View.Method)
73
-
type props<'a> = {method: Method.t<'a>, scope: array<Term.meta>, ruleStyle: RuleView.style}
93
+
type props<'a> = {method: Method.t<'a>, scope: array<Term.meta>, ruleStyle: RuleView.style, gen: Term.gen, onChange: (Method.t<'a>, Term.subst) => ()}
74
94
type srProps<'a> = Method1View.srProps<'a>
75
95
let make = (subrender: srProps<'a> => React.element) => props => {
76
96
switch props.method {
77
97
| First(m) =>
78
-
Method1View.make(subrender)({method: m, scope: props.scope, ruleStyle: props.ruleStyle})
98
+
Method1View.make(subrender)({method: m, scope: props.scope, ruleStyle: props.ruleStyle, gen: props.gen, onChange: (n,s) => props.onChange(First(n), s)})
79
99
| Second(m) =>
80
-
Method2View.make(subrender)({method: m, scope: props.scope, ruleStyle: props.ruleStyle})
100
+
Method2View.make(subrender)({method: m, scope: props.scope, ruleStyle: props.ruleStyle, gen: props.gen, onChange: (n,s) => props.onChange(Second(n), s)})
81
101
}
82
102
}
83
103
}
+12
-3
src/ProofView.res
+12
-3
src/ProofView.res
···
16
16
proof: Proof.checked,
17
17
scope: array<Term.meta>,
18
18
ruleStyle: RuleView.style,
19
+
gen: Term.gen,
20
+
onChange: (Proof.checked, Term.subst) => ()
19
21
}
20
22
module RuleView = RuleView.Make(Term, Judgment, JudgmentView)
21
23
@react.componentWithProps
···
35
37
<div className="proof-show">
36
38
<JudgmentView judgment={rule.conclusion} scope />
37
39
{switch method {
38
-
| Goal(options) => <button onClick={_ => Console.log(options(Term.makeGen()))}> {React.string("Test")} </button>
40
+
| Goal(options) =>
41
+
options(props.gen)->Dict.toArray->Array.map( ((str, (opt,subst))) => {
42
+
<button key=str onClick={_ => props.onChange(Proof.Checked({fixes, assumptions, method: Do(opt), rule}), subst)}> {React.string(str)} </button>
43
+
})->React.array
39
44
| Do(method) =>
40
45
React.createElement(
41
46
MethodView.make(p =>
42
-
make({proof: p["proof"], scope: p["scope"], ruleStyle: p["ruleStyle"]})
47
+
make({proof: p["proof"], scope: p["scope"], ruleStyle: p["ruleStyle"], gen: p["gen"], onChange: p["onChange"]})
43
48
),
44
-
{method, scope, ruleStyle: props.ruleStyle},
49
+
{method, scope, ruleStyle: props.ruleStyle, gen: props.gen, onChange:
50
+
(newm, subst) => {
51
+
props.onChange(Proof.Checked({fixes, assumptions, method: Do(newm), rule}), subst)
52
+
}
53
+
},
45
54
)
46
55
}}
47
56
</div>
+8
-4
src/Theorem.res
+8
-4
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
+
type state = {name: string, rule: Rule.t, proof: Proof.t, gen: Term.gen}
18
18
type props = {
19
19
content: state,
20
20
imports: Ports.t,
21
-
onChange: (state, ~exports: Ports.t) => unit,
21
+
onChange: (state, ~exports: Ports.t=?) => unit,
22
22
}
23
23
let serialise = (state: state) => {
24
24
state.rule->Rule.prettyPrintTopLevel(~name=state.name)
···
36
36
| Ok((_, s')) if String.length(String.trim(s')) > 0 =>
37
37
Error("Trailing input: "->String.concat(s'))
38
38
| Ok((proof, _)) => {
39
-
Ok(({name, rule, proof}, {Ports.facts: Dict.fromArray([(name,rule)]), ruleStyle: None}))
39
+
Ok(({name, rule, proof, gen}, {Ports.facts: Dict.fromArray([(name,rule)]), ruleStyle: None}))
40
40
}
41
41
}
42
42
}
···
46
46
let ruleStyle = props.imports.ruleStyle->Option.getOr(Hybrid)
47
47
let ctx: Context.t = {fixes: [], facts: props.imports.facts}
48
48
let checked = Proof.check(ctx, props.content.proof, props.content.rule)
49
+
let proofChanged = (proof, subst) => {
50
+
props.onChange({...props.content,proof:Proof.uncheck(proof)->Proof.substitute(subst)},
51
+
~exports={Ports.facts: Dict.fromArray([(props.content.name,props.content.rule)]), ruleStyle: None})
52
+
}
49
53
<>
50
54
<RuleView rule={props.content.rule} scope={[]} style={ruleStyle}>
51
55
{React.string(props.content.name)}
52
56
</RuleView>
53
-
<ProofView ruleStyle={ruleStyle} scope={[]} proof=checked />
57
+
<ProofView ruleStyle={ruleStyle} scope={[]} proof=checked gen={props.content.gen} onChange=proofChanged/>
54
58
</>
55
59
}
56
60
}
+4
-2
src/testcomponent.tsx
+4
-2
src/testcomponent.tsx
···
35
35
this.root.render(
36
36
<Tag content={this.state} imports={this.gatherImports()}
37
37
onChange={ (state, exports) => {
38
-
this.exports = exports
38
+
if (exports) {
39
+
this.exports = exports
40
+
signal(null)
41
+
}
39
42
this.state = state;
40
-
signal(null)
41
43
this.render(signal)
42
44
}}
43
45
/>