the next generation of the in-browser educational proof assistant
Merge pull request #7 from joshcbrown/push-myvkwmvlyywr
Fix warnings
authored by
Liam O'Connor
and committed by
GitHub
f382fdd6
97edd823
+107
-95
+6
-3
src/AxiomSet.res
+6
-3
src/AxiomSet.res
···
16
16
}
17
17
18
18
let serialise = (state: state) => {
19
-
state->Dict.toArray->Array.map(((k, r)) => r->Rule.prettyPrintTopLevel(~name=k))->Array.join("\n")
19
+
state
20
+
->Dict.toArray
21
+
->Array.map(((k, r)) => r->Rule.prettyPrintTopLevel(~name=k))
22
+
->Array.join("\n")
20
23
}
21
-
let deserialise = (str: string, ~imports: Ports.t) => {
24
+
let deserialise = (str: string, ~imports as _: Ports.t) => {
22
25
let cur = ref(str)
23
26
let go = ref(true)
24
27
let results = Dict.make()
···
47
50
ret.contents->Result.map(state => (state, {Ports.facts: state, ruleStyle: None}))
48
51
}
49
52
50
-
let make = props => {
53
+
let make = props => {
51
54
<div
52
55
className={"axiom-set axiom-set-"->String.concat(
53
56
String.make(props.imports.ruleStyle->Option.getOr(Hybrid)),
+46
-42
src/Editable.res
+46
-42
src/Editable.res
···
3
3
module TextArea = (Underlying: COMPONENT) => {
4
4
module Ports = Underlying.Ports
5
5
type props = {
6
-
content: result<Underlying.state,(string, string)>,
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
-
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
-
}
10
+
type state = result<Underlying.state, (string, string)>
11
+
12
+
let serialise = state =>
13
+
switch state {
14
+
| Ok(s) => Underlying.serialise(s)
15
+
| Error((_err, str)) => str
16
+
}
16
17
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)
18
+
switch Underlying.deserialise(str, ~imports) {
19
+
| Ok((s, e)) => Ok(Ok(s), e)
20
+
| Error(e) => Ok(Error(e, str), Ports.empty)
20
21
}
21
22
}
22
23
let make = props => {
···
25
26
let onTextChange = (ev: JsxEvent.Form.t) => {
26
27
let target = JsxEvent.Form.target(ev)
27
28
let value: string = target["value"]
28
-
setText(_ => value)
29
+
setText(_ => value)
29
30
}
30
31
let done = _ => {
31
32
switch deserialise(text, ~imports=props.imports) {
32
-
| Ok((st,ex)) => {
33
-
props.onChange(st,~exports=ex)
34
-
}
35
-
| Error(e) => Console.log("Impossible happened")
33
+
| Ok((st, ex)) => props.onChange(st, ~exports=ex)
34
+
| Error(_e) => Console.log("Impossible happened")
36
35
}
37
36
setEditing(_ => false)
38
37
}
···
47
46
</div>
48
47
} else {
49
48
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=?exports)
49
+
| Ok(us) =>
50
+
<div>
51
+
<Underlying
52
+
content={us}
53
+
imports={props.imports}
54
+
/* onLoad={(~exports, ~string=?) =>
55
+
props.onLoad(~exports, ~string=string->Option.getOr(Underlying.serialise(us)))} */
56
+
onChange={(state, ~exports=?) => {
57
+
props.onChange(Ok(state), ~exports=?exports)
58
+
}}
59
+
/>
60
+
<div className="editor-controls">
61
+
<span
62
+
className="editor-button button-icon button-icon-blue typcn typcn-edit"
63
+
onClick={_ => {
64
+
setText(_ => serialise(props.content))
65
+
setEditing(_ => true)
59
66
}}
60
67
/>
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
68
</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>
69
+
</div>
70
+
| Error((err, _str)) =>
71
+
<div>
72
+
<div className="error"> {React.string(err)} </div>
73
+
<div className="editor-controls">
74
+
<span
75
+
className="editor-button button-icon button-icon-blue typcn typcn-edit"
76
+
onClick={_ => {
77
+
setText(_ => serialise(props.content))
78
+
setEditing(_ => true)
79
+
}}
80
+
/>
77
81
</div>
78
-
}
79
-
}
82
+
</div>
83
+
}
80
84
}
81
85
}
82
86
}
+5
-5
src/HOTerm.res
+5
-5
src/HOTerm.res
···
263
263
| Some(idx) => Var({idx: idx})
264
264
}
265
265
}
266
-
let idx1 = (is: array<t>, j: int): t => idx1'(is, Var({idx: j}))
266
+
let _idx1 = (is: array<t>, j: int): t => idx1'(is, Var({idx: j}))
267
267
let idx2' = (is: array<t>, j: t): result<int, int => t> => {
268
268
switch idx(is, j) {
269
269
| None => Error(_ => Unallowed)
270
270
| Some(idx) => Ok(idx)
271
271
}
272
272
}
273
-
let idx2 = (is: array<t>, j: int) => idx2'(is, Var({idx: j}))
273
+
let _idx2 = (is: array<t>, j: int) => idx2'(is, Var({idx: j}))
274
274
let rec app = (term: t, args: array<t>): t => {
275
275
if args->Array.length == 0 {
276
276
term
···
326
326
// this function is called proj in Nipkow 1993 and it is called pruning in FCU paper
327
327
let rec proj = (subst: subst, term: t, ~gen: option<gen>): subst => {
328
328
switch strip(devar(subst, term)) {
329
-
| (Lam({name, body}), args) if args->Array.length == 0 => proj(subst, body, ~gen)
330
-
| (Unallowed, args) => raise(UnifyFail("unallowed"))
329
+
| (Lam({name: _, body}), args) if args->Array.length == 0 => proj(subst, body, ~gen)
330
+
| (Unallowed, _args) => raise(UnifyFail("unallowed"))
331
331
| (Symbol(_) | Var(_), args) => Array.reduce(args, subst, (acc, a) => proj(acc, a, ~gen))
332
332
| (Schematic({schematic}), args) => {
333
333
assert(!substHas(subst, schematic))
···
462
462
| UnifyFail(_) => []
463
463
}
464
464
}
465
-
let place = (x: int, ~scope: array<string>) => Schematic({
465
+
let place = (x: int, ~scope as _: array<string>) => Schematic({
466
466
schematic: x,
467
467
})
468
468
let prettyPrintVar = (idx: int, scope: array<string>) =>
+1
src/HOTermView.res
+1
src/HOTermView.res
+10
-10
src/Method.res
+10
-10
src/Method.res
···
17
17
let keywords: array<string>
18
18
let substitute: (t<'a>, Term.subst) => t<'a>
19
19
let check: (t<'a>, Context.t, Judgment.t, ('a, Rule.t) => 'b) => result<t<'b>, string>
20
-
let apply: (Context.t, Judgment.t, Term.gen, (Rule.t => 'a)) => Dict.t<(t<'a>, Term.subst)>
20
+
let apply: (Context.t, Judgment.t, Term.gen, Rule.t => 'a) => Dict.t<(t<'a>, Term.subst)>
21
21
let map: (t<'a>, 'a => 'b) => t<'b>
22
22
let parse: (
23
23
string,
···
53
53
{
54
54
ruleName: it.ruleName,
55
55
instantiation: it.instantiation->Array.map(t => t->Term.substitute(subst)),
56
-
subgoals: it.subgoals
56
+
subgoals: it.subgoals,
57
57
}
58
58
}
59
59
exception InternalParseError(string)
···
138
138
let apply = (ctx: Context.t, j: Judgment.t, gen: Term.gen, f: Rule.t => 'a) => {
139
139
let ret = Dict.make()
140
140
ctx.facts->Dict.forEachWithKey((rule, key) => {
141
-
let insts = rule.vars
142
-
->Array.map(m => Term.place(gen->Term.fresh(~replacing=m),~scope=ctx.fixes))
141
+
let insts =
142
+
rule.vars->Array.map(m => Term.place(gen->Term.fresh(~replacing=m), ~scope=ctx.fixes))
143
143
let res = rule->Rule.instantiate(insts)
144
-
let substs = Judgment.unify(res.conclusion,j,~gen)
144
+
let substs = Judgment.unify(res.conclusion, j, ~gen)
145
145
substs->Array.forEach(subst => {
146
146
let new = {
147
147
ruleName: key,
148
148
instantiation: insts,
149
-
subgoals: res.premises->Array.map(f)
149
+
subgoals: res.premises->Array.map(f),
150
150
}
151
151
ret->Dict.set("intro " ++ key, (new, subst))
152
152
})
···
208
208
{
209
209
rule: it.rule->Rule.substitute(subst),
210
210
proof: it.proof,
211
-
show: it.show
211
+
show: it.show,
212
212
}
213
213
}
214
214
let keywords = ["have"]
···
240
240
| Error(e) => Error(e)
241
241
}
242
242
}
243
-
let apply = (ctx: Context.t, j: Judgment.t, gen: Term.gen, f: Rule.t => 'a) => {
243
+
let apply = (_ctx: Context.t, _j: Judgment.t, _gen: Term.gen, _f: Rule.t => 'a) => {
244
244
Dict.make()
245
245
}
246
246
let check = (it: t<'a>, _ctx: Context.t, j: Judgment.t, f: ('a, Rule.t) => 'b) => {
···
270
270
}
271
271
let keywords = Array.concat(Method1.keywords, Method2.keywords)
272
272
let apply = (ctx: Context.t, j: Judgment.t, gen: Term.gen, f: Rule.t => 'a) => {
273
-
let d1 = Method1.apply(ctx,j,gen,f)->Dict.mapValues(((m,s)) => (First(m),s))
274
-
let d2 = Method2.apply(ctx,j,gen,f)->Dict.mapValues(((m,s)) => (Second(m),s))
273
+
let d1 = Method1.apply(ctx, j, gen, f)->Dict.mapValues(((m, s)) => (First(m), s))
274
+
let d2 = Method2.apply(ctx, j, gen, f)->Dict.mapValues(((m, s)) => (Second(m), s))
275
275
d1->Dict.assign(d2)
276
276
}
277
277
let check = (it, ctx, j, f) =>
-1
src/MethodView.res
-1
src/MethodView.res
+27
-23
src/Proof.res
+27
-23
src/Proof.res
···
13
13
assumptions: array<string>,
14
14
method: option<Method.t<t>>,
15
15
}
16
-
16
+
17
17
type rec checked =
18
18
| Checked({
19
19
fixes: array<Term.meta>,
···
24
24
| ProofError({raw: t, rule: Rule.t, msg: string})
25
25
and checked_option_method =
26
26
| Do(Method.t<checked>)
27
-
| Goal(Term.gen => Dict.t<(Method.t<checked>,Term.subst)>)
27
+
| Goal(Term.gen => Dict.t<(Method.t<checked>, Term.subst)>)
28
28
let parseKeyword = input => {
29
29
Method.keywords
30
30
->Array.concat(["?"])
31
31
->Array.find(kw => String.trim(input)->String.startsWith(kw))
32
32
}
33
33
let rec substitute = (prf: t, subst: Term.subst) => {
34
-
fixes: prf.fixes,
35
-
assumptions: prf.assumptions,
36
-
method: prf.method->Option.map(m =>
34
+
fixes: prf.fixes,
35
+
assumptions: prf.assumptions,
36
+
method: prf.method->Option.map(m =>
37
37
m->Method.substitute(subst)->Method.map(m => m->substitute(subst))
38
-
)
38
+
),
39
39
}
40
40
let rec prettyPrint = (prf: t, ~scope, ~indentation=0) => {
41
41
let mtd = switch prf.method {
···
131
131
method: switch method {
132
132
| Do(m) => Some(m->Method.map(uncheck))
133
133
| Goal(_) => None
134
-
}
134
+
},
135
135
}
136
136
}
137
137
let rec check = (ctx: Context.t, prf: t, rule: Rule.t) => {
138
-
let ruleStr = Rule.prettyPrintInline(rule, ~scope=[])
138
+
let _ruleStr = Rule.prettyPrintInline(rule, ~scope=[])
139
139
switch enter(ctx, prf, rule) {
140
140
| Ok(ctx') =>
141
141
switch prf.method {
···
155
155
rule,
156
156
fixes: prf.fixes,
157
157
assumptions: prf.assumptions,
158
-
method: Goal(gen => {
159
-
Method.apply(ctx',rule.conclusion,gen, rl => {
160
-
check(ctx',{
161
-
fixes:rl.vars,
162
-
method: None,
163
-
assumptions:Array.fromInitializer(
164
-
~length=rl.premises->Array.length,
165
-
i => Int.toString(i)
158
+
method: Goal(
159
+
gen => {
160
+
Method.apply(ctx', rule.conclusion, gen, rl => {
161
+
check(
162
+
ctx',
163
+
{
164
+
fixes: rl.vars,
165
+
method: None,
166
+
assumptions: Array.fromInitializer(~length=rl.premises->Array.length, i =>
167
+
Int.toString(i)
168
+
),
169
+
},
170
+
rl,
166
171
)
167
-
},rl)
168
-
})
169
-
}),
172
+
})
173
+
},
174
+
),
170
175
})
171
176
}
172
177
| Error(e) => ProofError({raw: prf, rule, msg: e})
173
178
}
174
179
} // result<checked,string>
175
-
176
-
let substituteChecked = (prf: checked,ctx: Context.t, subst: Term.subst) => {
180
+
181
+
let substituteChecked = (prf: checked, ctx: Context.t, subst: Term.subst) => {
177
182
switch prf {
178
183
| Checked(prf) =>
179
-
check(ctx,Checked(prf)->uncheck->substitute(subst),prf.rule->Rule.substitute(subst))
184
+
check(ctx, Checked(prf)->uncheck->substitute(subst), prf.rule->Rule.substitute(subst))
180
185
| ProofError({raw, rule, msg}) =>
181
186
ProofError({raw: raw->substitute(subst), rule: rule->Rule.substitute(subst), msg})
182
187
}
183
-
184
188
}
185
189
}
186
190
-1
src/ProofView.res
-1
src/ProofView.res
+1
-1
src/SExp.res
+1
-1
src/SExp.res
+10
-8
src/Theorem.res
+10
-8
src/Theorem.res
···
21
21
onChange: (state, ~exports: Ports.t=?) => unit,
22
22
}
23
23
let serialise = (state: state) => {
24
-
state.rule->Rule.prettyPrintTopLevel(~name=state.name)
25
-
->String.concat(Proof.prettyPrint(state.proof,~scope=[]))
24
+
state.rule
25
+
->Rule.prettyPrintTopLevel(~name=state.name)
26
+
->String.concat(Proof.prettyPrint(state.proof, ~scope=[]))
26
27
}
27
28
let deserialise = (str: string, ~imports: Ports.t) => {
28
-
let facts = imports.facts
29
+
let _facts = imports.facts
29
30
let gen = Term.makeGen()
30
31
let cur = ref(str)
31
32
switch Rule.parseTopLevel(cur.contents, ~scope=[], ~gen) {
···
35
36
| Error(e) => Error(e)
36
37
| Ok((_, s')) if String.length(String.trim(s')) > 0 =>
37
38
Error("Trailing input: "->String.concat(s'))
38
-
| Ok((proof, _)) => {
39
-
Ok(({name, rule, proof, gen}, {Ports.facts: Dict.fromArray([(name,rule)]), ruleStyle: None}))
40
-
}
39
+
| Ok((proof, _)) => Ok((
40
+
{name, rule, proof, gen},
41
+
{Ports.facts: Dict.fromArray([(name, rule)]), ruleStyle: None},
42
+
))
41
43
}
42
44
}
43
45
}
44
46
let make = props => {
45
-
Console.log(props.imports)
47
+
Console.log(props.imports)
46
48
let ruleStyle = props.imports.ruleStyle->Option.getOr(Hybrid)
47
49
let ctx: Context.t = {fixes: [], facts: props.imports.facts}
48
50
let checked = Proof.check(ctx, props.content.proof, props.content.rule)
···
55
57
{React.string(props.content.name)}
56
58
</RuleView>
57
59
<ProofView ruleStyle={ruleStyle} scope={[]} proof=checked gen={props.content.gen} onChange=proofChanged/>
58
-
</>
60
+
</>
59
61
}
60
62
}
+1
-1
tests/HOTermTest.res
+1
-1
tests/HOTermTest.res
···
18
18
| None => t->ok(true, ~msg=msg->Option.getOr("unification succeeded"))
19
19
| Some(subst) =>
20
20
t->equal(subst->Belt.Map.Int.size, res->Belt.Map.Int.size)
21
-
subst->Belt.Map.Int.forEach((k, v) => {
21
+
subst->Belt.Map.Int.forEach((k, _v) => {
22
22
let expected = subst->Belt.Map.Int.getExn(k)
23
23
if res->Belt.Map.Int.has(k) == false {
24
24
t->fail(