the next generation of the in-browser educational proof assistant
apply rescript format
+154
-67
+1
-1
src/Component.res
+1
-1
src/Component.res
···
25
25
onChange: (state, ~exports: Ports.t=?) => unit,
26
26
}
27
27
let serialise: state => string
28
-
let deserialise: (string, ~imports: Ports.t) => result<(state,Ports.t),string>
28
+
let deserialise: (string, ~imports: Ports.t) => result<(state, Ports.t), string>
29
29
let make: props => React.element
30
30
}
+11
-12
src/ConfigBlock.res
+11
-12
src/ConfigBlock.res
···
16
16
| "Hybrid" => Ok((Hybrid, Ports.empty))
17
17
| _ => Error("unknown rule style")
18
18
}
19
-
let serialise = style => switch style {
20
-
| Gentzen => "Gentzen"
21
-
| Linear => "Linear"
22
-
| Hybrid => "Hybrid"
23
-
}
24
-
25
-
19
+
let serialise = style =>
20
+
switch style {
21
+
| Gentzen => "Gentzen"
22
+
| Linear => "Linear"
23
+
| Hybrid => "Hybrid"
24
+
}
25
+
26
26
let make = props => {
27
27
let (style, setStyle) = React.useState(_ => props.content)
28
28
let onChange = e => {
29
29
let target = JsxEvent.Form.target(e)
30
30
let value: string = target["value"]
31
31
switch deserialise(value) {
32
-
| Ok((sty,_)) => {
33
-
setStyle(_ => sty)
34
-
props.onChange(sty, ~exports={Ports.facts: Dict.make(), ruleStyle: Some(sty)})
35
-
}
32
+
| Ok((sty, _)) => {
33
+
setStyle(_ => sty)
34
+
props.onChange(sty, ~exports={Ports.facts: Dict.make(), ruleStyle: Some(sty)})
35
+
}
36
36
| Error(_) => ()
37
37
}
38
-
39
38
}
40
39
[Gentzen, Linear, Hybrid]
41
40
->Array.map(n =>
+1
-1
src/Editable.res
+1
-1
src/Editable.res
···
54
54
/* onLoad={(~exports, ~string=?) =>
55
55
props.onLoad(~exports, ~string=string->Option.getOr(Underlying.serialise(us)))} */
56
56
onChange={(state, ~exports=?) => {
57
-
props.onChange(Ok(state), ~exports=?exports)
57
+
props.onChange(Ok(state), ~exports?)
58
58
}}
59
59
/>
60
60
<div className="editor-controls">
+1
-1
src/Method.res
+1
-1
src/Method.res
+86
-33
src/MethodView.res
+86
-33
src/MethodView.res
···
4
4
module Term: TERM
5
5
module Judgment: JUDGMENT with module Term := Term
6
6
module Method: PROOF_METHOD with module Term := Term and module Judgment := Judgment
7
-
type props<'a> = {method: Method.t<'a>, scope: array<Term.meta>, ruleStyle: RuleView.style, gen: Term.gen, onChange: (Method.t<'a>, Term.subst) => ()}
8
-
type srProps<'a> = {"proof": 'a, "scope": array<Term.meta>, "ruleStyle": RuleView.style, "gen": Term.gen, "onChange": ('a, Term.subst) => ()}
7
+
type props<'a> = {
8
+
method: Method.t<'a>,
9
+
scope: array<Term.meta>,
10
+
ruleStyle: RuleView.style,
11
+
gen: Term.gen,
12
+
onChange: (Method.t<'a>, Term.subst) => unit,
13
+
}
14
+
type srProps<'a> = {
15
+
"proof": 'a,
16
+
"scope": array<Term.meta>,
17
+
"ruleStyle": RuleView.style,
18
+
"gen": Term.gen,
19
+
"onChange": ('a, Term.subst) => unit,
20
+
}
9
21
let make: (srProps<'a> => React.element) => props<'a> => React.element
10
22
}
11
23
12
24
module DerivationView = (Term: TERM, Judgment: JUDGMENT with module Term := Term) => {
13
25
module Method = Derivation(Term, Judgment)
14
-
type props<'a> = {method: Method.t<'a>, scope: array<Term.meta>, ruleStyle: RuleView.style, gen: Term.gen, onChange: (Method.t<'a>, Term.subst) => ()}
15
-
type srProps<'a> = {"proof": 'a, "scope": array<Term.meta>, "ruleStyle": RuleView.style, "gen": Term.gen, "onChange": ('a, Term.subst) => ()}
26
+
type props<'a> = {
27
+
method: Method.t<'a>,
28
+
scope: array<Term.meta>,
29
+
ruleStyle: RuleView.style,
30
+
gen: Term.gen,
31
+
onChange: (Method.t<'a>, Term.subst) => unit,
32
+
}
33
+
type srProps<'a> = {
34
+
"proof": 'a,
35
+
"scope": array<Term.meta>,
36
+
"ruleStyle": RuleView.style,
37
+
"gen": Term.gen,
38
+
"onChange": ('a, Term.subst) => unit,
39
+
}
16
40
let make = (subRender: srProps<'a> => React.element) => props => {
17
41
<div>
18
42
<b> {React.string("by ")} </b>
···
23
47
<li key={String.make(i)}>
24
48
{React.createElement(
25
49
subRender,
26
-
{"proof": sg, "scope": props.scope, "ruleStyle": props.ruleStyle, "gen": props.gen, "onChange": (newa, subst) =>
27
-
props.onChange(props.method->Method.updateAtKey(i, _ => newa), subst)
50
+
{
51
+
"proof": sg,
52
+
"scope": props.scope,
53
+
"ruleStyle": props.ruleStyle,
54
+
"gen": props.gen,
55
+
"onChange": (newa, subst) =>
56
+
props.onChange(props.method->Method.updateAtKey(i, _ => newa), subst),
28
57
},
29
58
)}
30
59
</li>
···
42
71
) => {
43
72
module Method = Lemma(Term, Judgment)
44
73
type props<'a> = {
45
-
method: Method.t<'a>,
46
-
scope: array<Term.meta>,
47
-
ruleStyle: RuleView.style,
48
-
gen: Term.gen,
49
-
onChange: (Method.t<'a>, Term.subst) => ()
74
+
method: Method.t<'a>,
75
+
scope: array<Term.meta>,
76
+
ruleStyle: RuleView.style,
77
+
gen: Term.gen,
78
+
onChange: (Method.t<'a>, Term.subst) => unit,
50
79
}
51
80
type srProps<'a> = {
52
-
"proof": 'a,
53
-
"scope": array<Term.meta>,
54
-
"ruleStyle": RuleView.style,
55
-
"gen":Term.gen,
56
-
"onChange": ('a, Term.subst) => ()
81
+
"proof": 'a,
82
+
"scope": array<Term.meta>,
83
+
"ruleStyle": RuleView.style,
84
+
"gen": Term.gen,
85
+
"onChange": ('a, Term.subst) => unit,
57
86
}
58
87
module RuleView = RuleView.Make(Term, Judgment, JudgmentView)
59
88
let make = (subRender: srProps<'a> => React.element) => props => {
···
62
91
<RuleView rule={props.method.rule} scope={props.scope} style={props.ruleStyle}>
63
92
{React.null}
64
93
</RuleView>
65
-
{React.createElement(subRender, {
66
-
"proof": props.method.proof,
67
-
"scope": props.scope,
68
-
"ruleStyle": props.ruleStyle,
69
-
"gen": props.gen,
70
-
"onChange": (proof, subst) => { props.onChange({...props.method, proof}, subst) }
71
-
})}
72
-
{React.createElement(subRender, {
73
-
"proof": props.method.show,
74
-
"scope": props.scope,
75
-
"ruleStyle": props.ruleStyle,
76
-
"gen": props.gen,
77
-
"onChange": (show, subst) => { props.onChange({...props.method, show}, subst) }
78
-
})}
94
+
{React.createElement(
95
+
subRender,
96
+
{
97
+
"proof": props.method.proof,
98
+
"scope": props.scope,
99
+
"ruleStyle": props.ruleStyle,
100
+
"gen": props.gen,
101
+
"onChange": (proof, subst) => {props.onChange({...props.method, proof}, subst)},
102
+
},
103
+
)}
104
+
{React.createElement(
105
+
subRender,
106
+
{
107
+
"proof": props.method.show,
108
+
"scope": props.scope,
109
+
"ruleStyle": props.ruleStyle,
110
+
"gen": props.gen,
111
+
"onChange": (show, subst) => {props.onChange({...props.method, show}, subst)},
112
+
},
113
+
)}
79
114
</div>
80
115
}
81
116
}
···
89
124
and type srProps<'a> = Method1View.srProps<'a>,
90
125
) => {
91
126
module Method = Combine(Term, Judgment, Method1View.Method, Method2View.Method)
92
-
type props<'a> = {method: Method.t<'a>, scope: array<Term.meta>, ruleStyle: RuleView.style, gen: Term.gen, onChange: (Method.t<'a>, Term.subst) => ()}
127
+
type props<'a> = {
128
+
method: Method.t<'a>,
129
+
scope: array<Term.meta>,
130
+
ruleStyle: RuleView.style,
131
+
gen: Term.gen,
132
+
onChange: (Method.t<'a>, Term.subst) => unit,
133
+
}
93
134
type srProps<'a> = Method1View.srProps<'a>
94
135
let make = (subrender: srProps<'a> => React.element) => props => {
95
136
switch props.method {
96
137
| First(m) =>
97
-
Method1View.make(subrender)({method: m, scope: props.scope, ruleStyle: props.ruleStyle, gen: props.gen, onChange: (n,s) => props.onChange(First(n), s)})
138
+
Method1View.make(subrender)({
139
+
method: m,
140
+
scope: props.scope,
141
+
ruleStyle: props.ruleStyle,
142
+
gen: props.gen,
143
+
onChange: (n, s) => props.onChange(First(n), s),
144
+
})
98
145
| Second(m) =>
99
-
Method2View.make(subrender)({method: m, scope: props.scope, ruleStyle: props.ruleStyle, gen: props.gen, onChange: (n,s) => props.onChange(Second(n), s)})
146
+
Method2View.make(subrender)({
147
+
method: m,
148
+
scope: props.scope,
149
+
ruleStyle: props.ruleStyle,
150
+
gen: props.gen,
151
+
onChange: (n, s) => props.onChange(Second(n), s),
152
+
})
100
153
}
101
154
}
102
155
}
+34
-10
src/ProofView.res
+34
-10
src/ProofView.res
···
16
16
scope: array<Term.meta>,
17
17
ruleStyle: RuleView.style,
18
18
gen: Term.gen,
19
-
onChange: (Proof.checked, Term.subst) => ()
19
+
onChange: (Proof.checked, Term.subst) => unit,
20
20
}
21
21
module RuleView = RuleView.Make(Term, Judgment, JudgmentView)
22
22
@react.componentWithProps
···
36
36
<div className="proof-show">
37
37
<JudgmentView judgment={rule.conclusion} scope />
38
38
{switch method {
39
-
| Goal(options) =>
40
-
options(props.gen)->Dict.toArray->Array.map( ((str, (opt,subst))) => {
41
-
<button key=str onClick={_ => props.onChange(Proof.Checked({fixes, assumptions, method: Do(opt), rule}), subst)}> {React.string(str)} </button>
42
-
})->React.array
39
+
| Goal(options) =>
40
+
options(props.gen)
41
+
->Dict.toArray
42
+
->Array.map(((str, (opt, subst))) => {
43
+
<button
44
+
key=str
45
+
onClick={_ =>
46
+
props.onChange(
47
+
Proof.Checked({fixes, assumptions, method: Do(opt), rule}),
48
+
subst,
49
+
)}>
50
+
{React.string(str)}
51
+
</button>
52
+
})
53
+
->React.array
43
54
| Do(method) =>
44
55
React.createElement(
45
56
MethodView.make(p =>
46
-
make({proof: p["proof"], scope: p["scope"], ruleStyle: p["ruleStyle"], gen: p["gen"], onChange: p["onChange"]})
57
+
make({
58
+
proof: p["proof"],
59
+
scope: p["scope"],
60
+
ruleStyle: p["ruleStyle"],
61
+
gen: p["gen"],
62
+
onChange: p["onChange"],
63
+
})
47
64
),
48
-
{method, scope, ruleStyle: props.ruleStyle, gen: props.gen, onChange:
49
-
(newm, subst) => {
50
-
props.onChange(Proof.Checked({fixes, assumptions, method: Do(newm), rule}), subst)
51
-
}
65
+
{
66
+
method,
67
+
scope,
68
+
ruleStyle: props.ruleStyle,
69
+
gen: props.gen,
70
+
onChange: (newm, subst) => {
71
+
props.onChange(
72
+
Proof.Checked({fixes, assumptions, method: Do(newm), rule}),
73
+
subst,
74
+
)
75
+
},
52
76
},
53
77
)
54
78
}}
+3
-1
src/Scratch.res
+3
-1
src/Scratch.res
···
5
5
MethodView.DerivationView(HOTerm, HOTerm),
6
6
MethodView.LemmaView(HOTerm, HOTerm, HOTermJView),
7
7
)
8
-
module TheoremS = Editable.TextArea(Theorem.Make(HOTerm, HOTerm, HOTermJView, DerivationsOrLemmasView))
8
+
module TheoremS = Editable.TextArea(
9
+
Theorem.Make(HOTerm, HOTerm, HOTermJView, DerivationsOrLemmasView),
10
+
)
9
11
module ConfS = ConfigBlock.Make(HOTerm, HOTerm)
+1
-1
src/Signatures.res
+1
-1
src/Signatures.res
···
6
6
let mapSubst: (subst, t => t) => subst
7
7
type gen
8
8
let substitute: (t, subst) => t
9
-
let makeSubst: () => subst
9
+
let makeSubst: unit => subst
10
10
let unify: (t, t, ~gen: gen=?) => array<subst>
11
11
// law: unify(a,b) == [{}] iff equivalent(a,b)
12
12
let equivalent: (t, t) => bool
+16
-7
src/Theorem.res
+16
-7
src/Theorem.res
···
22
22
}
23
23
let serialise = (state: state) => {
24
24
state.rule
25
-
->Rule.prettyPrintTopLevel(~name=state.name)->String.concat("\n\n")
25
+
->Rule.prettyPrintTopLevel(~name=state.name)
26
+
->String.concat("\n\n")
26
27
->String.concat(Proof.prettyPrint(state.proof, ~scope=[]))
27
28
}
28
29
let deserialise = (str: string, ~imports: Ports.t) => {
···
36
37
| Error(e) => Error(e)
37
38
| Ok((_, s')) if String.length(String.trim(s')) > 0 =>
38
39
Error("Trailing input: "->String.concat(s'))
39
-
| Ok((proof, _)) => Ok((
40
+
| Ok((proof, _)) =>
41
+
Ok((
40
42
{name, rule, proof, gen},
41
43
{Ports.facts: Dict.fromArray([(name, rule)]), ruleStyle: None},
42
44
))
···
49
51
let ctx: Context.t = {fixes: [], facts: props.imports.facts}
50
52
let checked = Proof.check(ctx, props.content.proof, props.content.rule)
51
53
let proofChanged = (proof, subst) => {
52
-
props.onChange({...props.content,proof:Proof.uncheck(proof)->Proof.substitute(subst)},
53
-
~exports={Ports.facts: Dict.fromArray([(props.content.name,props.content.rule)]), ruleStyle: None})
54
+
props.onChange(
55
+
{...props.content, proof: Proof.uncheck(proof)->Proof.substitute(subst)},
56
+
~exports={
57
+
Ports.facts: Dict.fromArray([(props.content.name, props.content.rule)]),
58
+
ruleStyle: None,
59
+
},
60
+
)
54
61
}
55
62
<>
56
-
<h3>{React.string("Theorem")}</h3>
63
+
<h3> {React.string("Theorem")} </h3>
57
64
<RuleView rule={props.content.rule} scope={[]} style={ruleStyle}>
58
65
{React.string(props.content.name)}
59
66
</RuleView>
60
-
<h4>{React.string("Proof")}</h4>
61
-
<ProofView ruleStyle={ruleStyle} scope={[]} proof=checked gen={props.content.gen} onChange=proofChanged/>
67
+
<h4> {React.string("Proof")} </h4>
68
+
<ProofView
69
+
ruleStyle={ruleStyle} scope={[]} proof=checked gen={props.content.gen} onChange=proofChanged
70
+
/>
62
71
</>
63
72
}
64
73
}