the next generation of the in-browser educational proof assistant
working proof checking?
+190
-48
+7
-12
index.html
+7
-12
index.html
···
182
182
}
183
183
.rule-rulename-defined {
184
184
font-family: "Neo Euler Medium";
185
-
font-weight: bold;
186
185
font-size: small;
187
186
}
188
187
.rule-rulename-cases {
189
188
font-family: "Neo Euler Medium";
190
-
font-weight: bold;
191
189
font-size: small;
192
190
}
193
191
194
192
.rule-rulename-cases-keyword {
195
193
font-family: "Computer Modern Sans";
196
-
font-weight: bold;
197
194
font-size: small;
198
195
}
199
196
.rule-rulename-local {
···
209
206
/* TERMS */
210
207
.term-metavar {
211
208
color: var(--metavar-col);
212
-
font-weight: bold;
213
209
}
214
210
.term-metavar-unnamed {
215
211
color: var(--metavar-unnamed-col);
216
-
font-weight: bold;
217
212
}
218
213
.term-schematic {
219
214
color: var(--schematic-col);
···
229
224
}
230
225
.term-constructor {
231
226
font-family: "Computer Modern Sans";
232
-
font-weight: bold;
233
227
color: var(--constructor-col);
234
228
}
235
229
.placeholder {
···
238
232
/* SYMBOLS */
239
233
.symbol {
240
234
color: var(--symbol-col);
241
-
}
242
-
.symbol-bold {
243
-
font-weight: bold;
244
235
}
245
236
.symbol-turnstile {
246
237
padding-left: 6px;
···
279
270
(/\ x y)
280
271
</hol-comp>
281
272
<hol-config id="test.html/myconfig">Gentzen</hol-config>
282
-
<hol-proof id="test.html/prooftest" deps="test.html/baz">
273
+
<hol-proof id="test.html/prooftest" deps="test.html/myconfig test.html/baz">
274
+
a.b.
275
+
(/\ b a)
276
+
-------- theorem
277
+
(/\ a b)
283
278
x.y. ayx |- have x
284
-
|- by (AE2 x y) {
279
+
|- by (AE2 y x) {
285
280
|- by (ayx) {} }
286
281
asm |- by (AI x y) {
287
282
|- by (asm) {}
288
-
|- by (AE1 x y) {
283
+
|- by (AE1 y x) {
289
284
|- by (ayx) {} }
290
285
}
291
286
</hol-proof>
+68
-12
src/Editable.res
+68
-12
src/Editable.res
···
22
22
type props = Underlying.props
23
23
@react.componentWithProps
24
24
let make = props => {
25
-
Console.log(("MK",props))
26
25
let (editing,setEditing) = React.useState (_ => "off")
27
26
let (tree,setTree) = React.useState (_=>Underlying.getState(props))
28
27
let (text,setText) =
···
30
29
let done = _ => {
31
30
switch Underlying.deserialise(props,text) {
32
31
| Ok(t) => {
33
-
switch Underlying.onChange(Underlying.setState(props,t)) {
32
+
let foo = Underlying.onChange(Underlying.setState(props,t))
33
+
Console.log(foo)
34
+
switch foo {
34
35
| Ok(()) => {
35
36
setTree(_ => t)
36
37
setText(_=> Underlying.serialise(props,t))
···
219
220
JudgmentView : JUDGMENT_VIEW with module Term := Term and module Judgment := Judgment
220
221
) => {
221
222
module Rule = Rule.Make(Term,Judgment)
222
-
module TheRuleView = RuleView.Make(Term,Judgment,JudgmentView)
223
+
module RuleView = RuleView.Make(Term,Judgment,JudgmentView)
223
224
224
225
type rec props = {
225
226
rule: Rule.t,
226
227
scope: array<Term.meta>,
227
228
name?: string,
228
229
gen?: Term.gen,
229
-
style: TheRuleView.style,
230
+
style: RuleView.style,
230
231
onChange: props => ()
231
232
}
232
233
type state = (Rule.t, string)
···
244
245
}
245
246
}
246
247
let make = (props) => {
247
-
<TheRuleView rule={props.rule} scope={props.scope}
248
+
<RuleView rule={props.rule} scope={props.scope}
248
249
style={props.style}>
249
250
{React.string(props.name->Option.getOr(""))}
250
-
</TheRuleView>
251
+
</RuleView>
252
+
}
253
+
}
254
+
module TheoremSB = (
255
+
Term : TERM,
256
+
Judgment : JUDGMENT with module Term := Term,
257
+
JudgmentView : JUDGMENT_VIEW with module Term := Term and module Judgment := Judgment,
258
+
Method : PROOF_METHOD with module Term := Term and module Judgment := Judgment
259
+
) => {
260
+
module Rule = Rule.Make(Term, Judgment)
261
+
module RuleView = RuleView.Make(Term,Judgment,JudgmentView)
262
+
module Proof = Proof(Term,Judgment,Method)
263
+
module Context = Context(Term,Judgment)
264
+
type state = { name : string, rule: Rule.t, proof: Proof.checked }
265
+
type rec props = {
266
+
name: string,
267
+
rule: Rule.t,
268
+
proof: Proof.checked,
269
+
facts: Dict.t<Rule.t>,
270
+
gen : Term.gen,
271
+
style : RuleView.style,
272
+
onChange: props => result<(),string>
273
+
}
274
+
let getState : props => state
275
+
= ({name,rule,proof,gen:_,onChange:_,style:_,facts:_})
276
+
=> {name,rule,proof}
277
+
let setState : (props,state) => props = (props,{name,rule,proof})
278
+
=> {name,rule,proof, style:props.style,
279
+
onChange:props.onChange,gen: props.gen,facts: props.facts}
280
+
let onChange = (props) => props.onChange(props)
281
+
let serialise = (props : props, state : state) => {
282
+
state.rule
283
+
->Rule.prettyPrintTopLevel(~scope=[],~name=state.name)
284
+
->String.concat(newline)
285
+
->String.concat(Proof.prettyPrint(Proof.uncheck(state.proof), ~scope=[]))
286
+
}
287
+
let deserialise = (props : props, str : string) => {
288
+
let cur = ref(str)
289
+
Console.log("P1")
290
+
switch Rule.parseTopLevel(cur.contents,~scope=[],~gen=props.gen) {
291
+
| Error(e) => {Console.log("P2"); Error(e)}
292
+
| Ok(((r,n),s)) => switch Proof.parse(s,~scope=[],~gen=props.gen) {
293
+
| Error(e) => Error(e)
294
+
| Ok((_,s')) if String.length(String.trim(s')) > 0 =>
295
+
Error("Trailing input")
296
+
| Ok((prf,_)) => {
297
+
let ctx : Context.t = {fixes:[],facts:props.facts}
298
+
Ok({name:n,rule:r,proof:Proof.check(ctx,prf,r)})
299
+
}
300
+
}
301
+
}
302
+
}
303
+
let make = (props) => {
304
+
<RuleView rule={props.rule} scope={[]}
305
+
style={props.style}>
306
+
{React.string(props.name)}
307
+
</RuleView>
251
308
}
252
309
}
253
-
254
310
module RuleSetSB = (
255
311
Term : TERM,
256
312
Judgment : JUDGMENT with module Term := Term,
257
313
JudgmentView : JUDGMENT_VIEW with module Term := Term and module Judgment := Judgment
258
314
) => {
259
315
module Rule = Rule.Make(Term, Judgment)
260
-
module TheRuleView = RuleView.Make(Term,Judgment,JudgmentView)
316
+
module RuleView = RuleView.Make(Term,Judgment,JudgmentView)
261
317
module Name = WithTextBox(StringSB)
262
318
type state = Dict.t<Rule.t>
263
319
type rec props = {
264
320
rules: Dict.t<Rule.t>,
265
-
style: TheRuleView.style,
321
+
style: RuleView.style,
266
322
onChange: props => result<(),string>
267
323
}
268
324
let getState = (props) => props.rules
···
278
334
let deserialise = (props : props, str : string) => {
279
335
let cur = ref(str)
280
336
let go = ref(true)
281
-
let results = Dict.make()
337
+
let results = Dict.make()
282
338
let ret = ref(Error("impossible"))
283
339
while go.contents {
284
340
switch Rule.parseTopLevel(cur.contents,~scope=[]) {
···
304
360
let make = (props) => {
305
361
<div className={"axiom-set axiom-set-"->String.concat(String.make(props.style))}>
306
362
{ Dict.toArray(props.rules)->Array.map(((n,r)) =>
307
-
<TheRuleView rule={r} scope={[]} style={props.style}>
363
+
<RuleView rule={r} scope={[]} style={props.style}>
308
364
<Name content={n} onChange={(_) => Error("BLAH!")} />
309
-
</TheRuleView>)
365
+
</RuleView>)
310
366
->React.array
311
367
}
312
368
</div>
+58
-2
src/ProofEngine.res
+58
-2
src/ProofEngine.res
···
8
8
facts: Dict.t<Rule.t>,
9
9
}
10
10
}
11
-
11
+
let newline = "\n"
12
12
module type PROOF_METHOD = {
13
13
module Term : TERM
14
14
module Judgment : JUDGMENT with module Term := Term
···
23
23
~subparser: (string, ~scope: array<Term.meta>, ~gen: Term.gen)
24
24
=> result<('a,string),string> )
25
25
=> result<(t<'a>,string),string>
26
+
let prettyPrint : (t<'a>,~scope: array<Term.meta>,~indentation:int=?,
27
+
~subprinter: ('a,~scope:array<Term.meta>,~indentation:int=?)
28
+
=>string)
29
+
=> string
26
30
}
27
31
28
32
···
44
48
}
45
49
exception InternalParseError(string)
46
50
let keywords = ["by"]
51
+
let prettyPrint = (it : t<'a>, ~scope,~indentation=0,
52
+
~subprinter: ('a,~scope:array<Term.meta>, ~indentation:int=?)=>string) => {
53
+
let args = it.instantiation->Array.map(t => Term.prettyPrint(t,~scope));
54
+
"by ("
55
+
->String.concat(Array.join([it.ruleName,...args]," "))
56
+
->String.concat(") {")
57
+
->String.concat(if Array.length(it.subgoals) > 0 { newline } else { "" })
58
+
->String.concat(it.subgoals
59
+
->Array.map(s => subprinter(s, ~scope,~indentation=indentation+2))
60
+
->Array.join(newline))
61
+
->String.concat("}")
62
+
}
47
63
let parse = (input, ~keyword as _, ~scope, ~gen, ~subparser) => {
48
64
let cur = ref(String.trim(input))
49
65
if (cur.contents->String.get(0) == Some("(")) {
···
112
128
Error("Incorrect number of subgoals")
113
129
}
114
130
} else {
115
-
Error("Conclusion of rule doesn't match goal")
131
+
let concString = Judgment.prettyPrint(conclusion,~scope=ctx.fixes)
132
+
let goalString = Judgment.prettyPrint(j,~scope=ctx.fixes)
133
+
Error("Conclusion of rule '"
134
+
->String.concat(concString)
135
+
->String.concat("' doesn't match goal '")
136
+
->String.concat(goalString)
137
+
->String.concat("'"))
116
138
}
117
139
}
118
140
| _ => Error("Incorrect number of binders")
···
136
158
}
137
159
}
138
160
let keywords = ["have"]
161
+
let prettyPrint = (it : t<'a>, ~scope,~indentation=0,
162
+
~subprinter: ('a,~scope:array<Term.meta>, ~indentation:int=?)=>string) => {
163
+
"have "->String.concat(Rule.prettyPrintInline(it.rule,~scope))
164
+
->String.concat(newline)
165
+
->String.concat(subprinter(it.proof,~scope,~indentation))
166
+
->String.concat(newline)
167
+
->String.concat(subprinter(it.show,~scope,~indentation))
168
+
}
139
169
let parse = (input, ~keyword as _, ~scope, ~gen, ~subparser) => {
140
170
//todo add toplevel
141
171
switch Rule.parseInner(input, ~scope, ~gen) {
···
175
205
let check = (it,ctx, j, f) => switch it {
176
206
| First(m) => m->Method1.check(ctx,j,f)->Result.map(x => First(x))
177
207
| Second(m) => m->Method2.check(ctx,j,f)->Result.map(x => Second(x))
208
+
}
209
+
let prettyPrint = (it : t<'a>, ~scope, ~indentation=0,~subprinter) => switch it {
210
+
| First(m) => m->Method1.prettyPrint(~scope,~indentation,~subprinter)
211
+
| Second(m) => m->Method2.prettyPrint(~scope,~indentation,~subprinter)
178
212
}
179
213
let parse = (input, ~keyword, ~scope, ~gen, ~subparser) => {
180
214
if Method1.keywords->Array.indexOf(keyword) > -1 {
···
208
242
->Array.concat(["?"])
209
243
->Array.find(kw => String.trim(input)->String.startsWith(kw))
210
244
}
245
+
let rec prettyPrint = (prf : t, ~scope, ~indentation=0) => {
246
+
let mtd = switch prf.method {
247
+
| None => "?"
248
+
| Some(m) => Method.prettyPrint(m,
249
+
~scope=prf.fixes->Array.concat(scope),
250
+
~indentation=indentation+2,
251
+
~subprinter=prettyPrint)
252
+
}
253
+
String.padStart("",indentation," ")
254
+
->String.concat(prf.fixes->Array.map(Term.prettyPrintMeta)->Array.join(""))
255
+
->String.concat(prf.assumptions
256
+
->Array.map(s => String.concat(" ", s))
257
+
->Array.join(""))
258
+
->String.concat(if Array.length(prf.assumptions) == 0 {
259
+
"|- "
260
+
} else {
261
+
" |- "
262
+
})
263
+
->String.concat(mtd)
264
+
}
211
265
let rec parse = (input, ~scope,~gen) => {
212
266
let it = ref(Error(""))
213
267
let cur = ref(String.trim(input))
···
272
326
}
273
327
}
274
328
let rec check = (ctx : Context.t, prf: t, rule: Rule.t) => {
329
+
let ruleStr = Rule.prettyPrintInline(rule,~scope=[])
330
+
Console.log(("CHECK",ctx,prf,ruleStr))
275
331
switch enter(ctx,prf,rule) {
276
332
| Ok(ctx') => switch prf.method {
277
333
| Some(m) =>
+3
-2
src/Rule.res
+3
-2
src/Rule.res
···
156
156
switch rule {
157
157
| {vars: [], premises: [], conclusion: c} => Judgment.prettyPrint(c,~scope)
158
158
| _ => {
159
-
"["->String.concat(
160
-
rule.vars
159
+
let vars' = Array.copy(rule.vars)
160
+
Array.reverse(vars')
161
+
"["->String.concat(vars'
161
162
->Array.map(Term.prettyPrintMeta)
162
163
->Array.join("")
163
164
->String.concat(" ")
+1
-1
src/SExp.res
+1
-1
src/SExp.res
···
142
142
v
143
143
}
144
144
let prettyPrintVar = (idx: int, scope: array<string>) => switch scope[idx] {
145
-
| Some(n) if Array.indexOf(scope,n) == idx => n
145
+
| Some(n) if Array.indexOf(scope,n) == idx && false => n
146
146
| _ => "\\"->String.concat(String.make(idx))
147
147
}
148
148
let makeGen = () => {
+5
-1
src/Scratch.res
+5
-1
src/Scratch.res
···
3
3
module RuleSExpTE = RuleSetSB(SExp,SExp,SExpJView)
4
4
module RuleSExpView = WithTextArea(RuleSExpTE)
5
5
include RuleSExpView//(RuleSExpView.Hypothetical(RuleSExpView.Inline))
6
-
module PM = Proof(SExp,SExp,Combine(SExp,SExp,Derivation(SExp,SExp),Lemma(SExp,SExp)))
6
+
module Method = Combine(SExp,SExp,Derivation(SExp,SExp),Lemma(SExp,SExp))
7
+
module PM = Proof(SExp,SExp,Method)
8
+
module TheoremTE = TheoremSB(SExp,SExp,SExpJView, Method)
9
+
module TheoremView = WithTextArea(TheoremTE)
7
10
11
+
let \"Theorem" = TheoremView.make
8
12
9
13
//include SExpBaseView
10
14
+48
-18
src/testcomponent.tsx
+48
-18
src/testcomponent.tsx
···
1
1
import * as ComponentGraph2 from './componentgraph'
2
-
import { make as SExpBaseView, RuleSExpTE, PM } from './Scratch.mjs'
2
+
import { make as SExpBaseView, Theorem,TheoremTE, RuleSExpTE } from './Scratch.mjs'
3
3
import ReactDOM from 'react-dom/client';
4
4
import React from 'react';
5
5
···
44
44
if (view != null) {
45
45
this.root = ReactDOM.createRoot(view);
46
46
this.root.render(<SExpBaseView rules={this.data} style={this.config}
47
-
onChange={ e => { this.data = e.rules; signal("changed") }} />)
47
+
onChange={ e => { this.data = e.rules;
48
+
signal("changed");
49
+
return {"TAG":"Ok","_0":{}} }} />)
48
50
}
49
51
this.dependencyChanged = (_depName, comp) => {
50
52
if (comp instanceof ConfigComponent) {
51
53
this.config = comp.data
52
-
console.log(this.config)
53
54
this.root.render(<SExpBaseView rules={this.data} style={this.config}
54
-
onChange={ e => { this.data = e.rules; signal("changed") }} />)
55
+
onChange={ e => {
56
+
this.data = e.rules;
57
+
signal("changed");
58
+
return {"TAG":"Ok","_0":{}} }} />)
55
59
}
56
60
};
57
61
}
···
60
64
61
65
export class ProofComponent implements Component {
62
66
data : any;
63
-
dependencies : Record<string,any>;
67
+
deps : Record<string,Component>;
64
68
dependencyChanged : (id: string, comp: Component) => void;
65
69
root : ReactDOM.Root;
70
+
gen : {contents: number}
71
+
config : string;
66
72
toString() {
67
-
return ""
73
+
return TheoremTE.serialise({name:this.data.name,rule:this.data.rule,proof:this.data.proof},{name:this.data.name,rule:this.data.rule,proof:this.data.proof})
68
74
}
69
-
constructor(str : string, deps : Record<string,Component>, signal : (msg: any) => void, view? : HTMLElement) {
70
-
console.log("FOO")
71
-
for (const x in deps) {
72
-
if (deps[x] instanceof TestComponent) {
73
-
this.dependencies = deps[x].data
75
+
refreshData(str) {
76
+
let dependencies = {}
77
+
for (const x in this.deps) {
78
+
if (this.deps[x] instanceof TestComponent) {
79
+
for (let k in this.deps[x].data) {
80
+
dependencies[k] = this.deps[x].data[k]
81
+
}
82
+
}
83
+
if (this.deps[x] instanceof ConfigComponent) {
84
+
this.config = this.deps[x].data
74
85
}
75
86
}
76
-
var gen = {contents:0};
77
-
this.data = PM.parse(str, [], gen);
78
-
console.log(this.data)
79
-
if (view != null) {
80
-
//this.root = ReactDOM.createRoot(view);
81
-
//this.root.render(<SExpBaseView rules={this.data} style={this.config}
82
-
// onChange={ e => { this.data = e.rules; signal("changed") }} />)
87
+
this.data = {rule:undefined, name: "", proof:undefined}
88
+
this.gen = {contents:0};
89
+
this.data = (TheoremTE.deserialise({gen:this.gen,facts:dependencies},str))["_0"]
90
+
if (this.root) {
91
+
this.root.render(
92
+
<Theorem
93
+
rule={this.data.rule}
94
+
proof={this.data.proof}
95
+
name={this.data.name}
96
+
style={this.config}
97
+
onChange={(e) => {
98
+
this.data.rule = e.rule;
99
+
this.data.proof = e.proof;
100
+
this.data.name = e.name;
101
+
return {"TAG":"Ok","_0":{}} }}
102
+
gen={this.gen}
103
+
facts={dependencies} />);
83
104
}
105
+
106
+
}
107
+
constructor(str : string, deps : Record<string,Component>, signal : (msg: any) => void, view? : HTMLElement) {
108
+
this.deps = deps;
109
+
if (view != null) { this.root = ReactDOM.createRoot(view); }
110
+
this.refreshData(str)
84
111
this.dependencyChanged = (_depName, comp) => {
112
+
this.refreshData(this.toString()); signal("changed");
113
+
console.log(this.data)
85
114
};
115
+
86
116
}
87
117
}
88
118