the next generation of the in-browser educational proof assistant
more refactoring, react is weird
+411
-564
+4
-4
index.html
+4
-4
index.html
···
8
8
font-weight: normal;
9
9
src: local('Neo Euler Medium'), url('euler.woff') format('woff');
10
10
}
11
-
hol-comp {
11
+
.inline-rule {
12
12
font-family:'Neo Euler Medium';
13
13
}
14
14
:root {
···
253
253
</style>
254
254
</head>
255
255
<body>
256
-
<hol-comp id="test.html/baz" deps="test.html/myconfig">
256
+
<hol-comp id="index.html/baz" deps="index.html/myconfig">
257
257
x.y.
258
258
(/\ x y)
259
259
---- AE1
···
269
269
---- AI
270
270
(/\ x y)
271
271
</hol-comp>
272
-
<hol-config id="test.html/myconfig">Gentzen</hol-config>
273
-
<hol-proof id="test.html/prooftest" deps="test.html/myconfig test.html/baz">
272
+
<hol-config id="index.html/myconfig">Gentzen</hol-config>
273
+
<hol-proof id="index.html/prooftest" deps="index.html/myconfig index.html/baz">
274
274
a.b.
275
275
(/\ b a)
276
276
-------- theorem
+167
-294
src/Editable.res
+167
-294
src/Editable.res
···
1
-
open ProofEngine
1
+
open Method
2
2
open Signatures
3
3
4
-
// Describes a React component that is backed by state that has a string
5
-
// representation.
6
-
// Such components can be passed to WithTextArea or WithTextBox to get a
7
-
// component with the same props, but which now can be edited by the user.
8
-
module type STRING_BASED = {
9
-
type props
10
-
type state
11
-
let getState : props => state
12
-
let setState : (props,state) => props
13
-
let serialise : (props, state) => string
14
-
let deserialise : (props, string) => result<state,string>
15
-
// this is only required here to "get" the change handler from props.
16
-
// In reality, the onChange function should be given as part of props.
17
-
let onChange : props => result<(),string>
18
-
let make : props => React.element
4
+
module type PORTS = {
5
+
type t
6
+
let combine : (t,t) => t
7
+
let empty: t
8
+
}
9
+
module Ports = (Term : TERM, Judgment : JUDGMENT with module Term := Term) => {
10
+
module Rule = Rule.Make(Term, Judgment)
11
+
type t = { facts: Dict.t<Rule.t>, ruleStyle: option<RuleView.style> }
12
+
let empty = { facts: Dict.make(), ruleStyle: None }
13
+
let combine = (p1,p2) => {
14
+
let facts = Dict.copy(p1.facts)->Dict.assign(p2.facts);
15
+
let ruleStyle = p2.ruleStyle->Option.mapOr(p1.ruleStyle, x => Some(x));
16
+
{ facts, ruleStyle }
17
+
}
19
18
}
20
19
21
-
module WithTextArea = (Underlying : STRING_BASED) => {
22
-
type props = Underlying.props
23
-
@react.componentWithProps
24
-
let make = props => {
25
-
let (editing,setEditing) = React.useState (_ => "off")
26
-
let (tree,setTree) = React.useState (_=>Underlying.getState(props))
27
-
let (text,setText) =
28
-
React.useState (_=> Underlying.serialise(props,tree))
29
-
let done = _ => {
30
-
switch Underlying.deserialise(props,text) {
31
-
| Ok(t) => {
32
-
let foo = Underlying.onChange(Underlying.setState(props,t))
33
-
Console.log(foo)
34
-
switch foo {
35
-
| Ok(()) => {
36
-
setTree(_ => t)
37
-
setText(_=> Underlying.serialise(props,t))
38
-
setEditing(_=>"off")
39
-
}
40
-
| Error(e) => {
41
-
setEditing(_ => e)
42
-
}
43
-
}
44
-
}
45
-
| Error(e) => {
46
-
setEditing(_ => e)
47
-
}
48
-
}
20
+
21
+
module type COMPONENT = {
22
+
module Ports : PORTS
23
+
type props = { content: string, imports: Ports.t, onChange: (string,~exports:Ports.t) => () }
24
+
let make : props => React.element
25
+
let
26
+
}
27
+
28
+
module Config = (
29
+
Term : TERM,
30
+
Judgment : JUDGMENT with module Term := Term
31
+
) => {
32
+
module Ports = Ports(Term,Judgment)
33
+
open RuleView
34
+
type props = { content: string, imports: Ports.t, onLoad: (~exports:Ports.t) => (), onChange: (string,~exports:Ports.t) => () }
35
+
let deserialise = (str) => switch str {
36
+
| "Gentzen" => Gentzen
37
+
| "Linear" => Linear
38
+
| "Hybrid" => Hybrid
39
+
| _ => Hybrid
40
+
}
41
+
let make = (props) => {
42
+
let (style,setStyle) = React.useState (_=>deserialise(props.content))
43
+
React.useEffect(() => {
44
+
props.onLoad(~exports={Ports.facts: Dict.make(), ruleStyle:Some(style)})
45
+
None
46
+
},[])
47
+
let onChange= (e) => {
48
+
let target = JsxEvent.Form.target(e)
49
+
let value: string = target["value"]
50
+
setStyle(_ => deserialise(value))
51
+
props.onChange(value,~exports={Ports.facts: Dict.make(), ruleStyle:Some(style)})
49
52
}
50
-
let onChange= (ev: JsxEvent.Form.t) => {
53
+
[Gentzen,Linear,Hybrid]->Array.map(n =>
54
+
<input type_="radio" id={"style_"->String.concat(String.make(n))} name="style" onChange value={String.make(n)} checked={style==n}/>
55
+
)->React.array
56
+
57
+
}
58
+
}
59
+
60
+
61
+
module TextAreaEditor = (Underlying : COMPONENT) => {
62
+
module Ports = Underlying.Ports
63
+
type props = { content: string, imports: Ports.t, onLoad: (~exports:Ports.t) => (), onChange: (string,~exports:Ports.t) => () }
64
+
let make = (props) => {
65
+
let (editing,setEditing) = React.useState (_ => false)
66
+
let (text,setText) = React.useState (_ => props.content)
67
+
let onTextChange= (ev: JsxEvent.Form.t) => {
51
68
let target = JsxEvent.Form.target(ev)
52
69
let value: string = target["value"]
53
70
setText(_ => value)
54
71
}
55
-
if editing == "on" {
72
+
let done = (_) => {
73
+
setEditing(_=>false)
74
+
}
75
+
if editing {
56
76
<div>
57
-
<textarea className="editor-textArea" onChange={onChange}>
77
+
<textarea className="editor-textArea" onChange={onTextChange}>
58
78
{React.string(text)}
59
79
</textarea>
60
80
<div className="editor-controls">
61
81
<span className="editor-button button-icon button-icon-blue typcn typcn-tick" onClick={done}>
62
82
</span>
63
-
<span className="editor-button button-icon button-icon-grey typcn typcn-times" onClick={_ => {
64
-
setEditing(_ => "off")
65
-
setText(_=> Underlying.serialise(props,tree))
66
-
}}>
67
-
</span>
68
83
</div>
69
84
</div>
70
-
} else if editing == "off" {
71
-
<div>{Underlying.make(Underlying.setState(props,tree))}
85
+
} else {
86
+
<div>
87
+
{Underlying.make({
88
+
content:text,
89
+
imports: props.imports,
90
+
onLoad: props.onLoad,
91
+
onChange: (string, ~exports) => {
92
+
setText(_=>string)
93
+
props.onChange(string,~exports)
94
+
}
95
+
})}
72
96
<div className="editor-controls">
73
-
<span className="editor-button button-icon button-icon-blue typcn typcn-edit" onClick={_ => setEditing(_ => "on")}>
74
-
</span>
75
-
</div>
97
+
<span className="editor-button button-icon button-icon-blue typcn typcn-edit" onClick={_ => setEditing(_ => true)}>
98
+
</span>
76
99
</div>
77
-
} else {
78
-
<div className="editor-error">{React.string(editing)}
79
-
<div className="editor-controls">
80
-
<span className="editor-button button-icon button-icon-blue typcn typcn-edit"
81
-
onClick={_ => setEditing(_ => "on")}>
82
-
</span>
83
-
<span className="editor-button button-icon button-icon-grey typcn typcn-times" onClick={_ => {
84
-
setText(_=> Underlying.serialise(props,tree))
85
-
setEditing(_ => "off")
86
-
}}>
87
-
</span>
88
-
</div>
89
100
</div>
90
101
}
91
102
}
92
103
}
93
104
94
-
module WithTextBox = (Underlying : STRING_BASED) => {
95
-
type props = Underlying.props
96
-
@react.componentWithProps
97
-
let make = props => {
98
-
99
-
let (editing,setEditing) = React.useState (_ => "off")
100
-
let (tree,setTree) = React.useState (_=>Underlying.getState(props))
101
-
let (text,setText) =
102
-
React.useState (_=> Underlying.serialise(props,tree))
103
-
let done = _ => {
104
-
switch Underlying.deserialise(props,text) {
105
-
| Ok(t) => {
106
-
setTree(_ => t)
107
-
switch Underlying.onChange(Underlying.setState(props,t)) {
108
-
| Ok(()) => {
109
-
setTree(_ => t)
110
-
setText(_=> Underlying.serialise(props,t))
111
-
setEditing(_=>"off")
112
-
}
113
-
| Error(e) => {
114
-
setEditing(_ => e)
105
+
module AxiomSet = (
106
+
Term : TERM,
107
+
Judgment : JUDGMENT with module Term := Term,
108
+
JudgmentView : JUDGMENT_VIEW with module Term := Term and module Judgment := Judgment) => {
109
+
module Rule = Rule.Make(Term,Judgment)
110
+
module RuleView = RuleView.Make(Term,Judgment,JudgmentView)
111
+
module Ports = Ports(Term,Judgment)
112
+
type props = { content: string, imports: Ports.t, onLoad: (~exports:Ports.t) => (), onChange: (string,~exports:Ports.t) => () }
113
+
114
+
let deserialise = (str: string) => {
115
+
let cur = ref(str)
116
+
let go = ref(true)
117
+
let results = Dict.make()
118
+
let ret = ref(Error("impossible"))
119
+
while go.contents {
120
+
switch Rule.parseTopLevel(cur.contents,~scope=[]) {
121
+
| Ok((t,n),rest) => {
122
+
if n->String.trim == "" {
123
+
go := false
124
+
ret := Error("Rule given with no name")
125
+
} else {
126
+
Dict.set(results,n,t)
127
+
if rest->String.trim == "" {
128
+
go := false
129
+
ret := Ok(results)
130
+
} else {
131
+
cur := rest
115
132
}
116
133
}
117
134
}
118
-
| Error(e) => {
119
-
setEditing(_=>e)
120
-
}
135
+
| Error(e) => { go := false; ret := Error(e) }
121
136
}
122
137
}
123
-
let onChange= (ev: JsxEvent.Form.t) => {
124
-
let target = JsxEvent.Form.target(ev)
125
-
let value: string = target["value"]
126
-
setText(_ => value)
127
-
}
128
-
if editing == "on" {
129
-
<div>
130
-
<input value={text} onChange={onChange}/>
131
-
<div onClick={done}>{React.string("DONE")}</div>
132
-
</div>
133
-
} else if editing == "off" {
134
-
<div onClick={_ => setEditing(_ => "on")}>
135
-
{Underlying.make(Underlying.setState(props,tree))}
136
-
</div>
137
-
} else {
138
-
<div onClick={_ => setEditing(_ => "on")}>{React.string(editing)}</div>
139
-
}
140
-
}
141
-
}
142
-
143
-
144
-
module StringSB = {
145
-
type state = string
146
-
type rec props = {
147
-
content: string,
148
-
onChange: props => result<(),string>
138
+
ret.contents
149
139
}
150
140
151
-
let getState = (props) => props.content
152
-
let setState = (props,state) => {...props,content:state}
153
-
let serialise = (props : props,state) => state
154
-
let deserialise = (props,string) => Ok(string)
155
-
let onChange = (props) => props.onChange(props)
156
-
let make = (props) => React.string(props.content)
157
-
}
158
-
159
-
module TermSB =
160
-
(Term : TERM, TermView : TERM_VIEW with module Term := Term ) => {
161
-
type state = Term.t
162
-
type rec props = {
163
-
term: Term.t,
164
-
scope: array<Term.meta>,
165
-
gen?: Term.gen,
166
-
onChange: props => result<(),string>
167
-
}
168
-
let getState = (props) => props.term
169
-
let setState = (props,state) => {...props,term:state}
170
-
171
-
let serialise = (props : props,state) => {
172
-
state->Term.prettyPrint(~scope=props.scope)
173
-
}
174
-
let onChange = (props) => props.onChange(props)
175
-
let deserialise = (props : props, str : string) => {
176
-
switch Term.parse(str,~scope=props.scope,~gen=?props.gen) {
177
-
| Ok(t,"") => { Ok(t) }
178
-
| Ok(_,_) => Error("additional input beyond expression")
179
-
| Error(e) => Error(e)
141
+
let make = (props ) => {
142
+
switch deserialise(props.content) {
143
+
| Ok(s) => {
144
+
props.onLoad(~exports= {Ports.facts: s, ruleStyle: None});
145
+
<div className={"axiom-set axiom-set-"->String.concat(String.make(props.imports.ruleStyle->Option.getOr(Hybrid)))}>
146
+
{ Dict.toArray(s)->Array.map(((n,r)) =>
147
+
<RuleView rule={r} scope={[]} style={props.imports.ruleStyle->Option.getOr(Hybrid)}>
148
+
{React.string(n)}
149
+
//<Name content={n} onChange={(_) => Error("BLAH!")} />
150
+
</RuleView>)
151
+
->React.array
152
+
}
153
+
</div>
154
+
}
155
+
| Error(e) => <div className="error"> {React.string(e)} </div>
180
156
}
181
-
}
182
-
let make = ({term,scope}) => {
183
-
<TermView term=term scope=scope/>
184
157
}
185
158
}
186
-
module JudgmentSB = (
159
+
module Theorem = (
187
160
Term : TERM,
188
-
Judgment : JUDGMENT with module Term := Term,
189
-
JudgmentView : JUDGMENT_VIEW with module Term := Term and module Judgment := Judgment
190
-
) => {
191
-
192
-
type rec props = {
193
-
judgment: Judgment.t,
194
-
scope: array<Term.meta>,
195
-
gen?: Term.gen,
196
-
onChange: props => result<(),string>
197
-
}
198
-
type state = Judgment.t
199
-
let getState = (props) => props.judgment
200
-
let setState = (props,judgment) => {...props,judgment}
201
-
let onChange = (props) => props.onChange(props)
202
-
let serialise = (props : props, state:state) => {
203
-
state->Judgment.prettyPrint(~scope=props.scope)
204
-
}
205
-
let deserialise = (props : props, str : string) => {
206
-
switch Judgment.parse(str,~scope=props.scope,~gen=?props.gen) {
207
-
| Ok(t,"") => Ok(t)
208
-
| Ok(_,_) => Error("additional input beyond expression")
209
-
| Error(e) => Error(e)
210
-
}
211
-
}
212
-
let make = ({judgment,scope}) => {
213
-
<JudgmentView judgment=judgment scope=scope/>
214
-
}
215
-
}
216
-
217
-
module RuleSB = (
218
-
Term : TERM,
219
161
Judgment : JUDGMENT with module Term := Term,
220
-
JudgmentView : JUDGMENT_VIEW with module Term := Term and module Judgment := Judgment
162
+
JudgmentView : JUDGMENT_VIEW with module Term := Term and module Judgment := Judgment,
163
+
Method : PROOF_METHOD with module Term := Term and module Judgment := Judgment
221
164
) => {
222
165
module Rule = Rule.Make(Term,Judgment)
166
+
module Proof = Proof.Make(Term,Judgment,Method)
167
+
module Context = Context(Term,Judgment)
168
+
169
+
open RuleView
223
170
module RuleView = RuleView.Make(Term,Judgment,JudgmentView)
224
-
225
-
type rec props = {
226
-
rule: Rule.t,
227
-
scope: array<Term.meta>,
228
-
name?: string,
229
-
gen?: Term.gen,
230
-
style: RuleView.style,
231
-
onChange: props => ()
232
-
}
233
-
type state = (Rule.t, string)
234
-
let getState = (props) => (props.rule,props.name->Option.getOr(""))
235
-
let setState = (props,(rule,name)) => {...props,rule,name}
236
-
let onChange = (props) => props.onChange(props)
237
-
let serialise = (props : props, state) => {
238
-
state->Rule.prettyPrintTopLevel(~scope=props.scope,~name=?props.name)
239
-
}
240
-
let deserialise = (props : props, str : string) => {
241
-
switch Rule.parseTopLevel(str,~scope=props.scope,~gen=?props.gen) {
242
-
| Ok(r,"") => Ok(r)
243
-
| Ok(_,_) => Error("additional input beyond expression")
171
+
module Ports = Ports(Term,Judgment)
172
+
type props = { content: string, imports: Ports.t, onLoad: (~exports:Ports.t) => (), onChange: (string,~exports:Ports.t) => () }
173
+
type state = {name: string, rule: Rule.t, proof: Proof.checked}
174
+
let deserialise = (facts : Dict.t<Rule.t>, gen : Term.gen, str : string) : result<state,string> => {
175
+
let cur = ref(str)
176
+
switch Rule.parseTopLevel(cur.contents,~scope=[],~gen=gen) {
244
177
| Error(e) => Error(e)
178
+
| Ok(((r,n),s)) => switch Proof.parse(s,~scope=[],~gen=gen) {
179
+
| Error(e) => Error(e)
180
+
| Ok((_,s')) if String.length(String.trim(s')) > 0 =>
181
+
Error("Trailing input: "->String.concat(s'))
182
+
| Ok((prf,_)) => {
183
+
let ctx : Context.t = {fixes:[],facts}
184
+
Ok({name:n,rule:r,proof:Proof.check(ctx,prf,r)})
185
+
}
186
+
}
245
187
}
246
188
}
247
189
let make = (props) => {
248
-
<RuleView rule={props.rule} scope={props.scope}
249
-
style={props.style}>
250
-
{React.string(props.name->Option.getOr(""))}
251
-
</RuleView>
190
+
191
+
let gen = Term.makeGen()
192
+
switch deserialise(props.imports.facts, gen, props.content) {
193
+
| Ok(state) => {
194
+
props.onLoad(~exports={facts: Dict.fromArray([(state.name,state.rule)]), ruleStyle: None})
195
+
<RuleView rule={state.rule} scope={[]}
196
+
style={props.imports.ruleStyle->Option.getOr(Hybrid)}>
197
+
{React.string(state.name)}
198
+
</RuleView>
199
+
}
200
+
| Error(err) => <div className="error"> {React.string(err)} </div>
201
+
}
202
+
252
203
}
204
+
205
+
253
206
}
207
+
254
208
module TheoremSB = (
255
209
Term : TERM,
256
210
Judgment : JUDGMENT with module Term := Term,
···
258
212
Method : PROOF_METHOD with module Term := Term and module Judgment := Judgment
259
213
) => {
260
214
module Rule = Rule.Make(Term, Judgment)
261
-
module RuleView = RuleView.Make(Term,Judgment,JudgmentView)
262
-
module Proof = Proof(Term,Judgment,Method)
215
+
216
+
module Proof = Proof.Make(Term,Judgment,Method)
263
217
module Context = Context(Term,Judgment)
264
218
type state = { name : string, rule: Rule.t, proof: Proof.checked }
265
219
type rec props = {
···
271
225
style : RuleView.style,
272
226
onChange: props => result<(),string>
273
227
}
228
+
module RuleView = RuleView.Make(Term,Judgment,JudgmentView)
274
229
let getState : props => state
275
230
= ({name,rule,proof,gen:_,onChange:_,style:_,facts:_})
276
231
=> {name,rule,proof}
···
284
239
->String.concat(newline)
285
240
->String.concat(Proof.prettyPrint(Proof.uncheck(state.proof), ~scope=[]))
286
241
}
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>
308
-
}
309
-
}
310
-
module RuleSetSB = (
311
-
Term : TERM,
312
-
Judgment : JUDGMENT with module Term := Term,
313
-
JudgmentView : JUDGMENT_VIEW with module Term := Term and module Judgment := Judgment
314
-
) => {
315
-
module Rule = Rule.Make(Term, Judgment)
316
-
module RuleView = RuleView.Make(Term,Judgment,JudgmentView)
317
-
module Name = WithTextBox(StringSB)
318
-
type state = Dict.t<Rule.t>
319
-
type rec props = {
320
-
rules: Dict.t<Rule.t>,
321
-
style: RuleView.style,
322
-
onChange: props => result<(),string>
323
-
}
324
-
let getState = (props) => props.rules
325
-
let setState = (props,state) => {...props,rules:state}
326
-
let onChange = (props) => props.onChange(props)
327
-
let serialise = (props : props, state) => {
328
-
let results = [];
329
-
state->Dict.forEachWithKey((value, key) => {
330
-
results->Array.push(value->Rule.prettyPrintTopLevel(~scope=[],~name=key))
331
-
})
332
-
results->Array.join(Util.newline)
333
-
}
334
-
let deserialise = (props : props, str : string) => {
335
-
let cur = ref(str)
336
-
let go = ref(true)
337
-
let results = Dict.make()
338
-
let ret = ref(Error("impossible"))
339
-
while go.contents {
340
-
switch Rule.parseTopLevel(cur.contents,~scope=[]) {
341
-
| Ok((t,n),rest) => {
342
-
if n->String.trim == "" {
343
-
go := false
344
-
ret := Error("Rule given with no name")
345
-
} else {
346
-
Dict.set(results,n,t)
347
-
if rest->String.trim == "" {
348
-
go := false
349
-
ret := Ok(results)
350
-
} else {
351
-
cur := rest
352
-
}
353
-
}
354
-
}
355
-
| Error(e) => { go := false; ret := Error(e) }
356
-
}
357
-
}
358
-
ret.contents
359
-
}
360
-
let make = (props) => {
361
-
<div className={"axiom-set axiom-set-"->String.concat(String.make(props.style))}>
362
-
{ Dict.toArray(props.rules)->Array.map(((n,r)) =>
363
-
<RuleView rule={r} scope={[]} style={props.style}>
364
-
<Name content={n} onChange={(_) => Error("BLAH!")} />
365
-
</RuleView>)
366
-
->React.array
367
-
}
368
-
</div>
369
-
}
370
-
}
242
+
243
+
}
+139
src/Proof.res
+139
src/Proof.res
···
1
+
open Method
2
+
open Signatures
3
+
4
+
module Make = (
5
+
Term : TERM, Judgment : JUDGMENT with module Term := Term,
6
+
Method : PROOF_METHOD with module Term := Term and module Judgment := Judgment
7
+
) => {
8
+
module Rule = Rule.Make(Term,Judgment)
9
+
module Context = Context(Term,Judgment)
10
+
type rec t = {
11
+
fixes: array<Term.meta>,
12
+
assumptions: array<string>,
13
+
method: option<Method.t<t>>
14
+
}
15
+
type rec checked
16
+
= Checked({
17
+
fixes: array<Term.meta>,
18
+
assumptions: array<string>,
19
+
method: option<Method.t<checked>>,
20
+
rule: Rule.t
21
+
})
22
+
| ProofError({ raw: t, rule: Rule.t, msg: string})
23
+
let parseKeyword = (input) => {
24
+
Method.keywords
25
+
->Array.concat(["?"])
26
+
->Array.find(kw => String.trim(input)->String.startsWith(kw))
27
+
}
28
+
let rec prettyPrint = (prf : t, ~scope, ~indentation=0) => {
29
+
let mtd = switch prf.method {
30
+
| None => "?"
31
+
| Some(m) => Method.prettyPrint(m,
32
+
~scope=prf.fixes->Array.concat(scope),
33
+
~indentation=indentation+2,
34
+
~subprinter=prettyPrint)
35
+
}
36
+
String.padStart("",indentation," ")
37
+
->String.concat(prf.fixes->Array.map(Term.prettyPrintMeta)->Array.join(""))
38
+
->String.concat(prf.assumptions
39
+
->Array.map(s => String.concat(" ", s))
40
+
->Array.join(""))
41
+
->String.concat(if Array.length(prf.assumptions) == 0 {
42
+
"|- "
43
+
} else {
44
+
" |- "
45
+
})
46
+
->String.concat(mtd)
47
+
}
48
+
let rec parse = (input, ~scope,~gen) => {
49
+
let it = ref(Error(""))
50
+
let cur = ref(String.trim(input))
51
+
let fixes = []
52
+
while {it := Term.parseMeta(cur.contents); it.contents->Result.isOk} {
53
+
let (n,r) = Result.getExn(it.contents)
54
+
cur := String.trim(r)
55
+
fixes->Array.unshift(n)
56
+
}
57
+
let it = ref(Error(""))
58
+
let assumptions = []
59
+
while {it := Rule.parseRuleName(cur.contents); it.contents->Result.isOk} {
60
+
let (a,r) = Result.getExn(it.contents)
61
+
cur := String.trim(r)
62
+
assumptions->Array.push(a)
63
+
}
64
+
if cur.contents->String.slice(~start=0,~end=2) != "|-" {
65
+
Console.log((fixes,assumptions))
66
+
Error("expected turnstile or rule name"->String.concat(cur.contents))
67
+
} else {
68
+
cur := cur.contents->String.trim->String.sliceToEnd(~start=2)->String.trim
69
+
let scope' = Array.concat(fixes, scope)
70
+
switch parseKeyword(cur.contents) {
71
+
| Some("?") => {
72
+
Ok(({fixes,assumptions,method:None},
73
+
cur.contents->String.sliceToEnd(~start=1)))
74
+
}
75
+
| Some(keyword) => {
76
+
cur := cur.contents->String.sliceToEnd(~start=String.length(keyword))
77
+
switch Method.parse(
78
+
cur.contents, ~keyword,~scope=scope',~gen,~subparser=parse) {
79
+
| Ok((method,r)) => Ok(({fixes,assumptions,method:Some(method)},r))
80
+
| Error(e) => Error(e)
81
+
}
82
+
}
83
+
| None => Error("Expected keyword")
84
+
}
85
+
}
86
+
}
87
+
let enter = (ctx : Context.t, prf: t, rule: Rule.t) => {
88
+
if Array.length(prf.fixes) == Array.length(rule.vars) {
89
+
if Array.length(prf.assumptions) == Array.length(rule.premises) {
90
+
let newFacts = Dict.fromArray(Belt.Array.zip(prf.assumptions,rule.premises))
91
+
Ok({
92
+
Context.fixes: rule.vars->Array.concat(ctx.fixes),
93
+
facts: Dict.copy(ctx.facts)->Dict.assign(newFacts)
94
+
})
95
+
} else {
96
+
Error("Proof introduces a different number of assumptions than the rule")
97
+
}
98
+
} else {
99
+
Error("Proof introduces a different number of variables than the rule")
100
+
}
101
+
102
+
} //result<Context, string>
103
+
104
+
let rec uncheck = (prf : checked) => switch prf {
105
+
| ProofError({ raw, rule:_, msg:_ }) => raw
106
+
| Checked({fixes,assumptions,method,rule:_}) => {
107
+
fixes, assumptions,
108
+
method: method->Option.map(xs => xs->Method.uncheck(uncheck))
109
+
}
110
+
}
111
+
let rec check = (ctx : Context.t, prf: t, rule: Rule.t) => {
112
+
let ruleStr = Rule.prettyPrintInline(rule,~scope=[])
113
+
Console.log(("CHECK",ctx,prf,ruleStr))
114
+
switch enter(ctx,prf,rule) {
115
+
| Ok(ctx') => switch prf.method {
116
+
| Some(m) =>
117
+
switch m->Method.check(ctx', rule.conclusion, (s, r) => check(ctx',s,r)) {
118
+
| Ok(m') => Checked({
119
+
rule, fixes: prf.fixes,
120
+
assumptions: prf.assumptions,
121
+
method:Some(m')
122
+
})
123
+
| Error(e) => ProofError({raw:prf, rule, msg:e})
124
+
}
125
+
| None => Checked({
126
+
rule, fixes: prf.fixes, assumptions: prf.assumptions, method: None
127
+
})
128
+
}
129
+
| Error(e) => ProofError({raw:prf, rule, msg: e})
130
+
}
131
+
}// result<checked,string>
132
+
133
+
}
134
+
135
+
/*
136
+
137
+
138
+
139
+
*/
+1
-138
src/ProofEngine.res
src/Method.res
+1
-138
src/ProofEngine.res
src/Method.res
···
1
-
2
1
open Signatures
3
2
4
3
module Context = (Term : TERM, Judgment : JUDGMENT with module Term := Term) => {
···
217
216
Method2.parse(input,~keyword,~scope,~gen,~subparser)->Result.map(((x,r)) => (Second(x),r))
218
217
}
219
218
}
220
-
}
221
-
module Proof = (
222
-
Term : TERM, Judgment : JUDGMENT with module Term := Term,
223
-
Method : PROOF_METHOD with module Term := Term and module Judgment := Judgment
224
-
) => {
225
-
module Rule = Rule.Make(Term,Judgment)
226
-
module Context = Context(Term,Judgment)
227
-
type rec t = {
228
-
fixes: array<Term.meta>,
229
-
assumptions: array<string>,
230
-
method: option<Method.t<t>>
231
-
}
232
-
type rec checked
233
-
= Checked({
234
-
fixes: array<Term.meta>,
235
-
assumptions: array<string>,
236
-
method: option<Method.t<checked>>,
237
-
rule: Rule.t
238
-
})
239
-
| ProofError({ raw: t, rule: Rule.t, msg: string})
240
-
let parseKeyword = (input) => {
241
-
Method.keywords
242
-
->Array.concat(["?"])
243
-
->Array.find(kw => String.trim(input)->String.startsWith(kw))
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
-
}
265
-
let rec parse = (input, ~scope,~gen) => {
266
-
let it = ref(Error(""))
267
-
let cur = ref(String.trim(input))
268
-
let fixes = []
269
-
while {it := Term.parseMeta(cur.contents); it.contents->Result.isOk} {
270
-
let (n,r) = Result.getExn(it.contents)
271
-
cur := String.trim(r)
272
-
fixes->Array.unshift(n)
273
-
}
274
-
let it = ref(Error(""))
275
-
let assumptions = []
276
-
while {it := Rule.parseRuleName(cur.contents); it.contents->Result.isOk} {
277
-
let (a,r) = Result.getExn(it.contents)
278
-
cur := String.trim(r)
279
-
assumptions->Array.push(a)
280
-
}
281
-
if cur.contents->String.slice(~start=0,~end=2) != "|-" {
282
-
Console.log((fixes,assumptions))
283
-
Error("expected turnstile or rule name"->String.concat(cur.contents))
284
-
} else {
285
-
cur := cur.contents->String.trim->String.sliceToEnd(~start=2)->String.trim
286
-
let scope' = Array.concat(fixes, scope)
287
-
switch parseKeyword(cur.contents) {
288
-
| Some("?") => {
289
-
Ok(({fixes,assumptions,method:None},
290
-
cur.contents->String.sliceToEnd(~start=1)))
291
-
}
292
-
| Some(keyword) => {
293
-
cur := cur.contents->String.sliceToEnd(~start=String.length(keyword))
294
-
switch Method.parse(
295
-
cur.contents, ~keyword,~scope=scope',~gen,~subparser=parse) {
296
-
| Ok((method,r)) => Ok(({fixes,assumptions,method:Some(method)},r))
297
-
| Error(e) => Error(e)
298
-
}
299
-
}
300
-
| None => Error("Expected keyword")
301
-
}
302
-
}
303
-
}
304
-
let enter = (ctx : Context.t, prf: t, rule: Rule.t) => {
305
-
if Array.length(prf.fixes) == Array.length(rule.vars) {
306
-
if Array.length(prf.assumptions) == Array.length(rule.premises) {
307
-
let newFacts = Dict.fromArray(Belt.Array.zip(prf.assumptions,rule.premises))
308
-
Ok({
309
-
Context.fixes: rule.vars->Array.concat(ctx.fixes),
310
-
facts: Dict.copy(ctx.facts)->Dict.assign(newFacts)
311
-
})
312
-
} else {
313
-
Error("Proof introduces a different number of assumptions than the rule")
314
-
}
315
-
} else {
316
-
Error("Proof introduces a different number of variables than the rule")
317
-
}
318
-
319
-
} //result<Context, string>
320
-
321
-
let rec uncheck = (prf : checked) => switch prf {
322
-
| ProofError({ raw, rule:_, msg:_ }) => raw
323
-
| Checked({fixes,assumptions,method,rule:_}) => {
324
-
fixes, assumptions,
325
-
method: method->Option.map(xs => xs->Method.uncheck(uncheck))
326
-
}
327
-
}
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))
331
-
switch enter(ctx,prf,rule) {
332
-
| Ok(ctx') => switch prf.method {
333
-
| Some(m) =>
334
-
switch m->Method.check(ctx', rule.conclusion, (s, r) => check(ctx',s,r)) {
335
-
| Ok(m') => Checked({
336
-
rule, fixes: prf.fixes,
337
-
assumptions: prf.assumptions,
338
-
method:Some(m')
339
-
})
340
-
| Error(e) => ProofError({raw:prf, rule, msg:e})
341
-
}
342
-
| None => Checked({
343
-
rule, fixes: prf.fixes, assumptions: prf.assumptions, method: None
344
-
})
345
-
}
346
-
| Error(e) => ProofError({raw:prf, rule, msg: e})
347
-
}
348
-
}// result<checked,string>
349
-
350
-
}
351
-
352
-
/*
353
-
354
-
355
-
356
-
*/
219
+
}
+2
-3
src/RuleView.res
+2
-3
src/RuleView.res
···
1
1
open Signatures
2
+
type style = Gentzen | Linear | Hybrid
2
3
module Make = (
3
4
Term : TERM,
4
5
Judgment : JUDGMENT with module Term := Term,
5
6
JudgmentView : JUDGMENT_VIEW with module Term := Term and module Judgment := Judgment
6
7
) => {
7
-
module Rule = Rule.Make(Term, Judgment)
8
-
9
-
type style = Gentzen | Linear | Hybrid
8
+
module Rule = Rule.Make(Term, Judgment)
10
9
11
10
type props = {
12
11
rule:Rule.t,
+14
-9
src/Scratch.res
+14
-9
src/Scratch.res
···
1
1
open Editable
2
-
open ProofEngine
3
-
module RuleSExpTE = RuleSetSB(SExp,SExp,SExpJView)
4
-
module RuleSExpView = WithTextArea(RuleSExpTE)
5
-
include RuleSExpView//(RuleSExpView.Hypothetical(RuleSExpView.Inline))
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)
2
+
open Method
3
+
4
+
module AxiomS = TextAreaEditor(AxiomSet(SExp,SExp,SExpJView))
5
+
module DerivationsOrLemmas = Combine(SExp,SExp,Derivation(SExp,SExp),Lemma(SExp,SExp))
6
+
module TheoremS = TextAreaEditor(Theorem(SExp,SExp,SExpJView,DerivationsOrLemmas))
7
+
module Conf = Config(SExp,SExp)
8
+
//module RuleSExpTE = RuleSetSB(SExp,SExp,SExpJView)
9
+
//module RuleSExpView = WithTextArea(RuleSExpTE)
10
+
//include RuleSExpView//(RuleSExpView.Hypothetical(RuleSExpView.Inline))
11
+
//
12
+
//module PM = Proof.Make(SExp,SExp,DerivationsOrLemmas)
13
+
14
+
//module TheoremView = WithTextArea(TheoremTE)
10
15
11
-
let \"Theorem" = TheoremView.make
16
+
let \"AxiomSet" = AxiomS.make
12
17
13
18
//include SExpBaseView
14
19
+21
-10
src/componentgraph.ts
+21
-10
src/componentgraph.ts
···
64
64
data: string,
65
65
deps: Record<string, Component>,
66
66
signal: (msg: any) => void,
67
+
initialised: (msg: any) => void,
67
68
view?: HTMLElement) => Component,
68
69
view?: HTMLElement) {
69
70
this.url = url;
···
96
97
})
97
98
}
98
99
if (awaiting.length == 0) {
100
+
console.trace();
101
+
console.log("MAKING", this.url)
99
102
this.component = new maker(textual, {},
100
-
(msg) => { this.notifySubscribers(msg) }, view);
101
-
this.status = "ready";
102
-
for (let sub of this.subscribers) {
103
-
sub.dependencyReady(this.url);
104
-
}
103
+
(msg) => { this.notifySubscribers(msg) }, (msg) => {
104
+
console.log("LOADED", this.url)
105
+
this.status = "ready";
106
+
for (let sub of this.subscribers) {
107
+
sub.dependencyReady(this.url);
108
+
}
109
+
}, view);
105
110
}
106
111
}
107
112
this.dependencyReady = function(url) {
113
+
console.log("READY",this.url,url)
108
114
let index = awaiting.indexOf(url);
109
115
if (index > -1) {
110
116
awaiting.splice(index, 1);
···
118
124
deps2[dep] = v;
119
125
}
120
126
}
127
+
console.trace();
128
+
console.log("MAKING", this.url)
121
129
this.component = new maker(textual, deps2,
122
-
(msg) => { this.notifySubscribers(msg) }, view);
123
-
this.status = "ready";
124
-
for (let sub of this.subscribers) {
125
-
sub.dependencyReady(this.url);
126
-
}
130
+
(msg) => { this.notifySubscribers(msg) }, (msg) => {
131
+
console.log("LOADED", this.url)
132
+
this.status = "ready";
133
+
for (let sub of this.subscribers) {
134
+
sub.dependencyReady(this.url);
135
+
}
136
+
}, view);
127
137
}
128
138
}
129
139
}
···
137
147
new (data: string,
138
148
deps: Record<string, Component>,
139
149
signal: (msg: any) => void,
150
+
initialised: (msg: any) => void,
140
151
view?: HTMLElement) => Component>) {
141
152
let promises = [];
142
153
for (const name in spec) {
+63
-106
src/testcomponent.tsx
+63
-106
src/testcomponent.tsx
···
1
-
import * as ComponentGraph2 from './componentgraph'
2
-
import { make as SExpBaseView, Theorem,TheoremTE, RuleSExpTE } from './Scratch.mjs'
1
+
import * as ComponentGraph from './componentgraph'
2
+
import { AxiomS, Conf, TheoremS } from './Scratch.mjs'
3
3
import ReactDOM from 'react-dom/client';
4
4
import React from 'react';
5
5
6
-
export let ComponentGraph = ComponentGraph2
7
-
type Component = ComponentGraph2.Component
8
-
export class ConfigComponent implements Component {
9
-
data : string;
10
-
dependencyChanged : (id: string, comp: Component) => void;
11
-
toString() {
12
-
return this.data //prettyPrint(this.data,["a","b","c"])
13
-
}
14
-
constructor(str: string,_deps : Record<string,Component>, signal : (msg: any) => void, view? : HTMLElement) {
15
-
view.innerHTML='<input type="radio" id="style_Gentzen" name="style" value="Gentzen">';
16
-
view.innerHTML+='<input type="radio" id="style_Linear" name="style" value="Linear">';
17
-
view.innerHTML+='<input type="radio" id="style_Hybrid" name="style" value="Hybrid">';
18
-
(document.getElementById("style_" + str) as HTMLInputElement).checked = true;
19
-
for (const i of ["Gentzen","Linear","Hybrid"]) {
20
-
(document.getElementById("style_" + i) as HTMLInputElement).addEventListener("change",(e) =>{ this.data = (e.target as any).value; signal("changed")})
21
-
}
22
-
this.data = str;
23
-
this.dependencyChanged = (_depName, _comp) => { };
24
-
}
25
-
26
-
}
6
+
27
7
28
-
export class TestComponent implements Component {
29
-
data : any;
30
-
config : string;
31
-
dependencyChanged : (id: string, comp: Component) => void;
32
-
root : ReactDOM.Root;
33
-
toString() {
34
-
return (RuleSExpTE.serialise({rules:this.data, style:this.config},this.data))
35
-
}
36
-
constructor(str : string, deps : Record<string,Component>, signal : (msg: any) => void, view? : HTMLElement) {
37
-
for (const x in deps) {
38
-
if (deps[x] instanceof ConfigComponent) {
39
-
this.config = deps[x].data
40
-
}
41
-
}
42
-
this.data = (RuleSExpTE.deserialise({rules:this.data, style:this.config},str))["_0"]
43
-
console.log(this.config)
44
-
if (view != null) {
45
-
this.root = ReactDOM.createRoot(view);
46
-
this.root.render(<SExpBaseView rules={this.data} style={this.config}
47
-
onChange={ e => { this.data = e.rules;
48
-
signal("changed");
49
-
return {"TAG":"Ok","_0":{}} }} />)
50
-
}
51
-
this.dependencyChanged = (_depName, comp) => {
52
-
if (comp instanceof ConfigComponent) {
53
-
this.config = comp.data
54
-
this.root.render(<SExpBaseView rules={this.data} style={this.config}
55
-
onChange={ e => {
56
-
this.data = e.rules;
57
-
signal("changed");
58
-
return {"TAG":"Ok","_0":{}} }} />)
59
-
}
60
-
};
61
-
}
62
-
}
63
8
9
+
type Component = ComponentGraph.Component
64
10
65
-
export class ProofComponent implements Component {
66
-
data : any;
67
-
deps : Record<string,Component>;
68
-
dependencyChanged : (id: string, comp: Component) => void;
69
-
root : ReactDOM.Root;
70
-
gen : {contents: number}
71
-
config : string;
72
-
toString() {
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})
74
-
}
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]
11
+
//A bridge between any module that implements the COMPONENT signature from ReScript-land
12
+
//and a ComponentGraph component.
13
+
function HolComp(RComp : any) {
14
+
return class implements Component {
15
+
dependencyChanged : (id: string, comp: Component) => void;
16
+
deps : Record<string,Component>;
17
+
exports : Record<string,any>;
18
+
loaded: boolean;
19
+
root : ReactDOM.Root;
20
+
stringRep:string;
21
+
toString() {
22
+
return this.stringRep
23
+
}
24
+
gatherImports() {
25
+
let ret = RComp.Ports.empty
26
+
for (const x in this.deps) {
27
+
if ("exports" in this.deps[x]) {
28
+
console.log(x,this.deps[x])
29
+
ret = RComp.Ports.combine(ret,this.deps[x]["exports"])
81
30
}
82
31
}
83
-
if (this.deps[x] instanceof ConfigComponent) {
84
-
this.config = this.deps[x].data
85
-
}
32
+
return ret
86
33
}
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) {
34
+
render(signal : (msg: any) => void,loaded : (msg: any) => void) {
35
+
let Tag = RComp.make
91
36
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} />);
37
+
<Tag content={this.stringRep} imports={this.gatherImports()}
38
+
onChange={ (str, exports) => {
39
+
this.exports = exports
40
+
this.stringRep = str;
41
+
signal(null)
42
+
this.render(signal, loaded)
43
+
}}
44
+
onLoad={ (exports) => {
45
+
this.exports = exports
46
+
if (!this.loaded) {
47
+
this.loaded = true;
48
+
loaded(null)
49
+
}
50
+
}}
51
+
/>
52
+
)
104
53
}
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)
111
-
this.dependencyChanged = (_depName, comp) => {
112
-
this.refreshData(this.toString()); signal("changed");
113
-
console.log(this.data)
114
-
};
115
-
54
+
constructor(str: string,deps : Record<string,Component>, signal : (msg: any) => void, loaded : (msg: any) => void, view? : HTMLElement) {
55
+
this.deps = deps
56
+
this.stringRep = str
57
+
this.loaded = false
58
+
if (view != null) {
59
+
const newDiv = document.createElement("div");
60
+
view.innerHTML = "";
61
+
view.appendChild(newDiv);
62
+
this.root = ReactDOM.createRoot(newDiv);
63
+
}
64
+
this.render(signal,loaded)
65
+
this.dependencyChanged = (_depName, _comp) => {
66
+
this.render(signal, loaded)
67
+
};
68
+
}
116
69
}
70
+
117
71
}
118
72
119
-
120
73
window.localStorage.clear()
121
-
ComponentGraph.setup({"hol-comp": TestComponent,"hol-config": ConfigComponent, "hol-proof":ProofComponent});
74
+
ComponentGraph.setup({
75
+
"hol-comp": HolComp(AxiomS),
76
+
"hol-config":HolComp(Conf),
77
+
"hol-proof": HolComp(TheoremS)
78
+
});//"hol-config": ConfigComponent, "hol-proof":ProofComponent});