the next generation of the in-browser educational proof assistant
refactoring
+851
-784
-322
src/Demo.res
-322
src/Demo.res
···
1
-
2
-
let mapMapValues = (m: Map.t<'a,'b>, f: 'b => 'c) => {
3
-
let nu = Map.make();
4
-
m->Map.forEachWithKey((v,k) => {
5
-
nu->Map.set(k,f(v))
6
-
})
7
-
nu
8
-
}
9
-
10
-
11
-
module type TERM = {
12
-
type t
13
-
type schematic
14
-
type meta
15
-
type subst = Map.t<schematic,t>
16
-
let substitute : (t, subst) => t
17
-
let unify : (t, t) => array<subst>
18
-
let substDeBruijn : (t, array<t>, ~from:int=?) => t
19
-
let upshift : (t, int, ~from:int=?) => t
20
-
type gen
21
-
let fresh : (gen, ~replacing:meta=?) => schematic
22
-
let seen : (gen, schematic) => ()
23
-
let place : (schematic, ~scope: array<meta>) => t
24
-
let makeGen : () => gen
25
-
let parse : (string, ~scope: array<meta>, ~gen: gen=?) => result<(t,string),string>
26
-
let parseMeta : (string) => result<(meta,string),string>
27
-
let prettyPrint : (t, ~scope: array<meta>) => string
28
-
let prettyPrintMeta : (meta) => string
29
-
}
30
-
31
-
module type BASE = {
32
-
module Term : TERM
33
-
module Judgment : {
34
-
type t
35
-
let substitute : (t, Term.subst) => t
36
-
let unify : (t, t) => array<Term.subst>
37
-
let substDeBruijn : (t, array<Term.t>, ~from:int=?) => t
38
-
let upshift : (t, int, ~from:int=?) => t
39
-
let parse : (string, ~scope: array<Term.meta>, ~gen: Term.gen=?) => result<(t,string),string>
40
-
let prettyPrint : (t, ~scope: array<Term.meta>) => string
41
-
}
42
-
}
43
-
let newline = "\n"
44
-
let vinculumRES = "^\s*\\n\\s*[-—][-—][\\-—]+([^\\n\\-—][^\\n]*)?"
45
-
module ProofEngine = (Base : BASE) => {
46
-
open Base
47
-
module Rule = {
48
-
type rec t = {vars: array<Term.meta>, premises: array<t>, conclusion: Judgment.t}
49
-
let rec substitute = (rule: t, subst: Term.subst) => {
50
-
let subst' = subst->mapMapValues(v => v->Term.upshift(Array.length(rule.vars)));
51
-
{
52
-
vars: rule.vars,
53
-
premises: rule.premises->Array.map(premise => premise->substitute(subst')),
54
-
conclusion: rule.conclusion->Judgment.substitute(subst')
55
-
}
56
-
}
57
-
let rec substDeBruijn = (rule: t, substs: array<Term.t>, ~from:int=0) => {
58
-
let len = Array.length(rule.vars)
59
-
let substs' = substs->Array.map(v => v->Term.upshift(len,~from=from))
60
-
{
61
-
vars: rule.vars,
62
-
premises: rule.premises
63
-
->Array.map(premise => premise->substDeBruijn(substs', ~from=from+len)),
64
-
conclusion: rule.conclusion
65
-
->Judgment.substDeBruijn(substs',~from=from+len),
66
-
}
67
-
}
68
-
let rec upshift = (rule: t, amount: int, ~from:int=0) => {
69
-
let len = Array.length(rule.vars)
70
-
{
71
-
vars: rule.vars,
72
-
premises: rule.premises->Array.map(r => r->upshift(amount, ~from = from + len)),
73
-
conclusion: rule.conclusion->Judgment.upshift(amount, ~from = from + len)
74
-
}
75
-
}
76
-
type bare = { premises: array<t>, conclusion: Judgment.t }
77
-
let instantiate = (rule: t, terms: array<Term.t>) => {
78
-
assert(Array.length(terms) == Array.length(rule.vars))
79
-
let terms' = [...terms]
80
-
Array.reverse(terms')
81
-
{
82
-
premises: rule.premises->Array.map(r => r-> substDeBruijn(terms')),
83
-
conclusion: rule.conclusion->Judgment.substDeBruijn(terms')
84
-
}
85
-
}
86
-
87
-
let parseVinculum = (str) => {
88
-
let re = RegExp.fromStringWithFlags(vinculumRES,~flags="y")
89
-
switch re->RegExp.exec(str) {
90
-
| None => Error("expected vinculum")
91
-
| Some(res) => { switch res[1] {
92
-
| Some(Some(n)) if String.trim(n) != ""
93
-
=> Ok(n,String.sliceToEnd(str,~start=RegExp.lastIndex(re)))
94
-
| _ => Ok("", String.sliceToEnd(str,~start=RegExp.lastIndex(re)))
95
-
}}
96
-
}
97
-
}
98
-
99
-
exception InternalParseError(string)
100
-
let rec parseInner = (string, ~scope=[]: array<Term.meta>, ~gen=?) => {
101
-
if (string->String.trim->String.get(0) == Some("[")) {
102
-
let cur = ref(String.make(string->String.trim->String.sliceToEnd(~start=1)));
103
-
let it = ref(Error(""))
104
-
let vars = []
105
-
while {it := Term.parseMeta(cur.contents); it.contents->Result.isOk} {
106
-
let (str,rest) = Result.getExn(it.contents)
107
-
Array.unshift(vars,str)
108
-
cur := rest
109
-
}
110
-
let it = ref(Error(""))
111
-
let premises = []
112
-
switch {
113
-
while (cur.contents->String.trim->String.slice(~start=0,~end=2) != "|-"
114
-
&& cur.contents->String.trim->String.get(0) != Some("]")) {
115
-
switch parseInner(cur.contents,~scope=vars->Array.concat(scope), ~gen=?gen) {
116
-
| Ok(p,rest) => {
117
-
cur := rest
118
-
premises->Array.push(p)
119
-
}
120
-
| Error(_) => raise(InternalParseError("expected turnstile or premise"))
121
-
}
122
-
}
123
-
if (cur.contents->String.trim->String.get(0) == Some("]")) {
124
-
let rest = cur.contents->String.trim->String.sliceToEnd(~start=1)
125
-
cur := rest
126
-
switch premises {
127
-
| [{vars:[],premises:[],conclusion:e}] => Ok(({vars,premises:[],conclusion:e}, rest))
128
-
| _ => Error("Conclusion appears to be multiple terms")
129
-
}
130
-
} else {
131
-
cur := cur.contents->String.trim->String.sliceToEnd(~start=2)
132
-
switch Judgment.parse(cur.contents,~scope=vars->Array.concat(scope),~gen=?gen) {
133
-
| Ok(conclusion, rest) =>
134
-
if (rest->String.trim->String.get(0) == Some("]")) {
135
-
cur := rest->String.trim->String.sliceToEnd(~start=1);
136
-
Ok(({vars, premises, conclusion}, cur.contents))
137
-
} else {
138
-
Error("Expected closing bracket")
139
-
}
140
-
| Error(e) => Error(e)
141
-
}
142
-
}
143
-
} {
144
-
| exception InternalParseError(e) => Error(e)
145
-
| v => v
146
-
}
147
-
} else {
148
-
switch Judgment.parse(string,~scope,~gen=?gen) {
149
-
| Ok(conclusion, rest) => Ok(({vars:[], premises:[], conclusion}, rest))
150
-
| Error(e) => Error(e)
151
-
}
152
-
}
153
-
}
154
-
let parseTopLevel = (string, ~gen=?, ~scope=[]) => {
155
-
let cur = ref(String.make(string));
156
-
let it = ref(Error(""))
157
-
let vars = []
158
-
switch {
159
-
while {it := Term.parseMeta(cur.contents); it.contents->Result.isOk} {
160
-
let (str,rest) = Result.getExn(it.contents)
161
-
Array.unshift(vars,str)
162
-
cur := rest
163
-
}
164
-
let it = ref(Error(""))
165
-
let premises = []
166
-
while {it := parseVinculum(cur.contents); it.contents->Result.isError} {
167
-
switch parseInner(cur.contents,~scope=vars->Array.concat(scope), ~gen=?gen) {
168
-
| Ok(p,rest) => {
169
-
cur := rest
170
-
premises->Array.push(p)
171
-
}
172
-
| Error(e) => raise(InternalParseError(e))
173
-
}
174
-
}
175
-
let (ruleName,rest) = it.contents->Result.getExn
176
-
cur := rest
177
-
switch Judgment.parse(cur.contents,~scope=vars->Array.concat(scope),~gen=?gen) {
178
-
| Ok(conclusion, rest) => Ok((({vars, premises, conclusion}, ruleName), rest))
179
-
| Error(e) => Error(e)
180
-
}
181
-
} {
182
-
| exception InternalParseError(e) => Error(e)
183
-
| v => v
184
-
}
185
-
}
186
-
187
-
let rec prettyPrintInline = (rule: t,~scope=[]:array<Term.meta>) => {
188
-
switch rule {
189
-
| {vars: [], premises: [], conclusion: c} => Judgment.prettyPrint(c,~scope)
190
-
| _ => {
191
-
"["->String.concat(
192
-
rule.vars
193
-
->Array.map(Term.prettyPrintMeta)
194
-
->Array.join("")
195
-
->String.concat(" ")
196
-
->String.concat(if Array.length(rule.premises) == 0 {
197
-
Judgment.prettyPrint(rule.conclusion,~scope=[...rule.vars,...scope])
198
-
} else {
199
-
rule.premises
200
-
->Array.map(r => prettyPrintInline(r,~scope=[...rule.vars,...scope]))->Array.join(" ")
201
-
->String.concat(" |- ")
202
-
->String.concat(Judgment.prettyPrint(rule.conclusion,~scope=[...rule.vars,...scope]))
203
-
}
204
-
))->String.concat("]")
205
-
}
206
-
}
207
-
}
208
-
let rec prettyPrintTopLevel = (rule: t,~name="",~scope=[]:array<Term.meta>) => {
209
-
let vinculise = (strs: array<string>) => {
210
-
let l = strs->Array.map(String.length)->Array.concat([4])->Math.Int.maxMany
211
-
strs->Array.concat(["-"->String.repeat(l)->String.concat(" ")->String.concat(name)])
212
-
}
213
-
let myReverse = (arr) => {
214
-
Array.reverse(arr)
215
-
arr
216
-
}
217
-
rule.vars
218
-
->Array.map(Term.prettyPrintMeta)
219
-
->myReverse
220
-
->Array.join("")
221
-
->String.concat(newline)
222
-
->String.concat(
223
-
rule.premises
224
-
->Array.map(r => prettyPrintInline(r,~scope=[...rule.vars,...scope]))
225
-
->vinculise
226
-
->Array.concat([Judgment.prettyPrint(rule.conclusion,~scope=[...rule.vars,...scope])])
227
-
->Array.map(s => String.concat(" ",s))
228
-
->Array.join(newline))
229
-
}
230
-
}
231
-
module Step = {
232
-
type t<'a> = {
233
-
fixes: array<Term.meta>,
234
-
facts: Dict.t<Rule.t>,
235
-
proof: 'a
236
-
}
237
-
let bind : (t<'a>, 'a => t<'b>) => t<'b> = (s, f) => {
238
-
let t = f(s.proof);
239
-
{
240
-
fixes: t.fixes->Array.concat(s.fixes),
241
-
facts: Dict.copy(s.facts)->Dict.assign(t.facts),
242
-
proof: t.proof
243
-
}
244
-
}
245
-
}
246
-
module Goal = {
247
-
type t = {
248
-
fix: array<Term.meta>,
249
-
assume: array<Rule.t>,
250
-
assumeNames: array<string>,
251
-
show: Judgment.t
252
-
}
253
-
let toRule : t => Rule.t = (goal : t) => {
254
-
vars: goal.fix,
255
-
premises: goal.assume,
256
-
conclusion: goal.show
257
-
}
258
-
}
259
-
module type PROOFT = {
260
-
type t<'a>
261
-
let subproofs : (Goal.t,t<'a>, 'a=>Goal.t) => Dict.t<Step.t<'a>>
262
-
}
263
-
module Either = (A : PROOFT, B : PROOFT) => {
264
-
type t<'a> = L(A.t<'a>) | R(B.t<'a>)
265
-
let subproofs = (goal:Goal.t,it : t<'a>, f : 'a => Goal.t) => switch it {
266
-
| L(x) => A.subproofs(goal,x,f)
267
-
| R(x) => B.subproofs(goal,x,f)
268
-
}
269
-
}
270
-
271
-
module Deduction : PROOFT = {
272
-
type t<'a> = {
273
-
from: array<'a>,
274
-
ruleName: string,
275
-
instantiation: array<Term.t>
276
-
}
277
-
let subproofs = (goal : Goal.t,it : t<'a>, _ : 'a => Goal.t) => {
278
-
let toStep : 'a => Step.t<'a> = (a) => {
279
-
fixes: goal.fix,
280
-
facts: Belt.Array.zip(goal.assumeNames,goal.assume)->Dict.fromArray,
281
-
proof: a
282
-
};
283
-
Belt.Array.range(0,Array.length(it.from))
284
-
->Array.map(x =>Belt.Int.toString(x))
285
-
->Belt.Array.zip(it.from->Array.map(toStep))
286
-
->Dict.fromArray
287
-
}
288
-
}
289
-
module Lemma : PROOFT = {
290
-
type t<'a> = {
291
-
name: string,
292
-
have: 'a,
293
-
show: 'a
294
-
}
295
-
let subproofs = (goal: Goal.t,it : t<'a>, f : 'a => Goal.t) => {
296
-
let haveGoal : Step.t<'a> = {
297
-
fixes: goal.fix,
298
-
facts: Belt.Array.zip(goal.assumeNames,goal.assume)->Dict.fromArray,
299
-
proof: it.have
300
-
};
301
-
let showGoal : Step.t<'a> = {
302
-
fixes: goal.fix,
303
-
facts: Belt.Array.zip(goal.assumeNames,goal.assume)
304
-
->Array.concat([(it.name,f(it.have)->Goal.toRule)])
305
-
->Dict.fromArray,
306
-
proof: it.show
307
-
};
308
-
Dict.fromArray([(it.name,haveGoal), ("@show",showGoal)])
309
-
}
310
-
}
311
-
module Proof = (A : PROOFT) => {
312
-
type rec t = {goal:Goal.t, step?: A.t<t> }
313
-
}
314
-
}
315
-
316
-
module FirstOrder = ProofEngine({
317
-
module Term = SExp
318
-
module Judgment = SExp
319
-
})
320
-
open FirstOrder
321
-
322
-
module TestProofs = Proof(Either(Deduction,Lemma))
+314
src/Editable.res
+314
src/Editable.res
···
1
+
open ProofEngine
2
+
open Signatures
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
19
+
}
20
+
21
+
module WithTextArea = (Underlying : STRING_BASED) => {
22
+
type props = Underlying.props
23
+
@react.componentWithProps
24
+
let make = props => {
25
+
Console.log(("MK",props))
26
+
let (editing,setEditing) = React.useState (_ => "off")
27
+
let (tree,setTree) = React.useState (_=>Underlying.getState(props))
28
+
let (text,setText) =
29
+
React.useState (_=> Underlying.serialise(props,tree))
30
+
let done = _ => {
31
+
switch Underlying.deserialise(props,text) {
32
+
| Ok(t) => {
33
+
switch Underlying.onChange(Underlying.setState(props,t)) {
34
+
| Ok(()) => {
35
+
setTree(_ => t)
36
+
setText(_=> Underlying.serialise(props,t))
37
+
setEditing(_=>"off")
38
+
}
39
+
| Error(e) => {
40
+
setEditing(_ => e)
41
+
}
42
+
}
43
+
}
44
+
| Error(e) => {
45
+
setEditing(_ => e)
46
+
}
47
+
}
48
+
}
49
+
let onChange= (ev: JsxEvent.Form.t) => {
50
+
let target = JsxEvent.Form.target(ev)
51
+
let value: string = target["value"]
52
+
setText(_ => value)
53
+
}
54
+
if editing == "on" {
55
+
<div>
56
+
<textarea className="editor-textArea" onChange={onChange}>
57
+
{React.string(text)}
58
+
</textarea>
59
+
<div className="editor-controls">
60
+
<span className="editor-button button-icon button-icon-blue typcn typcn-tick" onClick={done}>
61
+
</span>
62
+
<span className="editor-button button-icon button-icon-grey typcn typcn-times" onClick={_ => {
63
+
setEditing(_ => "off")
64
+
setText(_=> Underlying.serialise(props,tree))
65
+
}}>
66
+
</span>
67
+
</div>
68
+
</div>
69
+
} else if editing == "off" {
70
+
<div>{Underlying.make(Underlying.setState(props,tree))}
71
+
<div className="editor-controls">
72
+
<span className="editor-button button-icon button-icon-blue typcn typcn-edit" onClick={_ => setEditing(_ => "on")}>
73
+
</span>
74
+
</div>
75
+
</div>
76
+
} else {
77
+
<div className="editor-error">{React.string(editing)}
78
+
<div className="editor-controls">
79
+
<span className="editor-button button-icon button-icon-blue typcn typcn-edit"
80
+
onClick={_ => setEditing(_ => "on")}>
81
+
</span>
82
+
<span className="editor-button button-icon button-icon-grey typcn typcn-times" onClick={_ => {
83
+
setText(_=> Underlying.serialise(props,tree))
84
+
setEditing(_ => "off")
85
+
}}>
86
+
</span>
87
+
</div>
88
+
</div>
89
+
}
90
+
}
91
+
}
92
+
93
+
module WithTextBox = (Underlying : STRING_BASED) => {
94
+
type props = Underlying.props
95
+
@react.componentWithProps
96
+
let make = props => {
97
+
98
+
let (editing,setEditing) = React.useState (_ => "off")
99
+
let (tree,setTree) = React.useState (_=>Underlying.getState(props))
100
+
let (text,setText) =
101
+
React.useState (_=> Underlying.serialise(props,tree))
102
+
let done = _ => {
103
+
switch Underlying.deserialise(props,text) {
104
+
| Ok(t) => {
105
+
setTree(_ => t)
106
+
switch Underlying.onChange(Underlying.setState(props,t)) {
107
+
| Ok(()) => {
108
+
setTree(_ => t)
109
+
setText(_=> Underlying.serialise(props,t))
110
+
setEditing(_=>"off")
111
+
}
112
+
| Error(e) => {
113
+
setEditing(_ => e)
114
+
}
115
+
}
116
+
}
117
+
| Error(e) => {
118
+
setEditing(_=>e)
119
+
}
120
+
}
121
+
}
122
+
let onChange= (ev: JsxEvent.Form.t) => {
123
+
let target = JsxEvent.Form.target(ev)
124
+
let value: string = target["value"]
125
+
setText(_ => value)
126
+
}
127
+
if editing == "on" {
128
+
<div>
129
+
<input value={text} onChange={onChange}/>
130
+
<div onClick={done}>{React.string("DONE")}</div>
131
+
</div>
132
+
} else if editing == "off" {
133
+
<div onClick={_ => setEditing(_ => "on")}>
134
+
{Underlying.make(Underlying.setState(props,tree))}
135
+
</div>
136
+
} else {
137
+
<div onClick={_ => setEditing(_ => "on")}>{React.string(editing)}</div>
138
+
}
139
+
}
140
+
}
141
+
142
+
143
+
module StringSB = {
144
+
type state = string
145
+
type rec props = {
146
+
content: string,
147
+
onChange: props => result<(),string>
148
+
}
149
+
150
+
let getState = (props) => props.content
151
+
let setState = (props,state) => {...props,content:state}
152
+
let serialise = (props : props,state) => state
153
+
let deserialise = (props,string) => Ok(string)
154
+
let onChange = (props) => props.onChange(props)
155
+
let make = (props) => React.string(props.content)
156
+
}
157
+
158
+
module TermSB =
159
+
(Term : TERM, TermView : TERM_VIEW with module Term := Term ) => {
160
+
type state = Term.t
161
+
type rec props = {
162
+
term: Term.t,
163
+
scope: array<Term.meta>,
164
+
gen?: Term.gen,
165
+
onChange: props => result<(),string>
166
+
}
167
+
let getState = (props) => props.term
168
+
let setState = (props,state) => {...props,term:state}
169
+
170
+
let serialise = (props : props,state) => {
171
+
state->Term.prettyPrint(~scope=props.scope)
172
+
}
173
+
let onChange = (props) => props.onChange(props)
174
+
let deserialise = (props : props, str : string) => {
175
+
switch Term.parse(str,~scope=props.scope,~gen=?props.gen) {
176
+
| Ok(t,"") => { Ok(t) }
177
+
| Ok(_,_) => Error("additional input beyond expression")
178
+
| Error(e) => Error(e)
179
+
}
180
+
}
181
+
let make = ({term,scope}) => {
182
+
<TermView term=term scope=scope/>
183
+
}
184
+
}
185
+
module JudgmentSB = (
186
+
Term : TERM,
187
+
Judgment : JUDGMENT with module Term := Term,
188
+
JudgmentView : JUDGMENT_VIEW with module Term := Term and module Judgment := Judgment
189
+
) => {
190
+
191
+
type rec props = {
192
+
judgment: Judgment.t,
193
+
scope: array<Term.meta>,
194
+
gen?: Term.gen,
195
+
onChange: props => result<(),string>
196
+
}
197
+
type state = Judgment.t
198
+
let getState = (props) => props.judgment
199
+
let setState = (props,judgment) => {...props,judgment}
200
+
let onChange = (props) => props.onChange(props)
201
+
let serialise = (props : props, state:state) => {
202
+
state->Judgment.prettyPrint(~scope=props.scope)
203
+
}
204
+
let deserialise = (props : props, str : string) => {
205
+
switch Judgment.parse(str,~scope=props.scope,~gen=?props.gen) {
206
+
| Ok(t,"") => Ok(t)
207
+
| Ok(_,_) => Error("additional input beyond expression")
208
+
| Error(e) => Error(e)
209
+
}
210
+
}
211
+
let make = ({judgment,scope}) => {
212
+
<JudgmentView judgment=judgment scope=scope/>
213
+
}
214
+
}
215
+
216
+
module RuleSB = (
217
+
Term : TERM,
218
+
Judgment : JUDGMENT with module Term := Term,
219
+
JudgmentView : JUDGMENT_VIEW with module Term := Term and module Judgment := Judgment
220
+
) => {
221
+
module Rule = Rule.Make(Term,Judgment)
222
+
module TheRuleView = RuleView.Make(Term,Judgment,JudgmentView)
223
+
224
+
type rec props = {
225
+
rule: Rule.t,
226
+
scope: array<Term.meta>,
227
+
name?: string,
228
+
gen?: Term.gen,
229
+
style: TheRuleView.style,
230
+
onChange: props => ()
231
+
}
232
+
type state = (Rule.t, string)
233
+
let getState = (props) => (props.rule,props.name->Option.getOr(""))
234
+
let setState = (props,(rule,name)) => {...props,rule,name}
235
+
let onChange = (props) => props.onChange(props)
236
+
let serialise = (props : props, state) => {
237
+
state->Rule.prettyPrintTopLevel(~scope=props.scope,~name=?props.name)
238
+
}
239
+
let deserialise = (props : props, str : string) => {
240
+
switch Rule.parseTopLevel(str,~scope=props.scope,~gen=?props.gen) {
241
+
| Ok(r,"") => Ok(r)
242
+
| Ok(_,_) => Error("additional input beyond expression")
243
+
| Error(e) => Error(e)
244
+
}
245
+
}
246
+
let make = (props) => {
247
+
<TheRuleView rule={props.rule} scope={props.scope}
248
+
style={props.style}>
249
+
{React.string(props.name->Option.getOr(""))}
250
+
</TheRuleView>
251
+
}
252
+
}
253
+
254
+
module RuleSetSB = (
255
+
Term : TERM,
256
+
Judgment : JUDGMENT with module Term := Term,
257
+
JudgmentView : JUDGMENT_VIEW with module Term := Term and module Judgment := Judgment
258
+
) => {
259
+
module Rule = Rule.Make(Term, Judgment)
260
+
module TheRuleView = RuleView.Make(Term,Judgment,JudgmentView)
261
+
module Name = WithTextBox(StringSB)
262
+
type state = Dict.t<Rule.t>
263
+
type rec props = {
264
+
rules: Dict.t<Rule.t>,
265
+
style: TheRuleView.style,
266
+
onChange: props => result<(),string>
267
+
}
268
+
let getState = (props) => props.rules
269
+
let setState = (props,state) => {...props,rules:state}
270
+
let onChange = (props) => props.onChange(props)
271
+
let serialise = (props : props, state) => {
272
+
let results = [];
273
+
state->Dict.forEachWithKey((value, key) => {
274
+
results->Array.push(value->Rule.prettyPrintTopLevel(~scope=[],~name=key))
275
+
})
276
+
results->Array.join(Util.newline)
277
+
}
278
+
let deserialise = (props : props, str : string) => {
279
+
let cur = ref(str)
280
+
let go = ref(true)
281
+
let results = Dict.make()
282
+
let ret = ref(Error("impossible"))
283
+
while go.contents {
284
+
switch Rule.parseTopLevel(cur.contents,~scope=[]) {
285
+
| Ok((t,n),rest) => {
286
+
if n->String.trim == "" {
287
+
go := false
288
+
ret := Error("Rule given with no name")
289
+
} else {
290
+
Dict.set(results,n,t)
291
+
if rest->String.trim == "" {
292
+
go := false
293
+
ret := Ok(results)
294
+
} else {
295
+
cur := rest
296
+
}
297
+
}
298
+
}
299
+
| Error(e) => { go := false; ret := Error(e) }
300
+
}
301
+
}
302
+
ret.contents
303
+
}
304
+
let make = (props) => {
305
+
<div className={"axiom-set axiom-set-"->String.concat(String.make(props.style))}>
306
+
{ Dict.toArray(props.rules)->Array.map(((n,r)) =>
307
+
<TheRuleView rule={r} scope={[]} style={props.style}>
308
+
<Name content={n} onChange={(_) => Error("BLAH!")} />
309
+
</TheRuleView>)
310
+
->React.array
311
+
}
312
+
</div>
313
+
}
314
+
}
+90
src/ProofEngine.res
+90
src/ProofEngine.res
···
1
+
2
+
open Signatures
3
+
4
+
module Make = (Term : TERM, Judgment : JUDGMENT with module Term := Term) => {
5
+
module Rule = Rule.Make(Term,Judgment)
6
+
module Step = {
7
+
type t<'a> = {
8
+
fixes: array<Term.meta>,
9
+
facts: Dict.t<Rule.t>,
10
+
proof: 'a
11
+
}
12
+
let bind : (t<'a>, 'a => t<'b>) => t<'b> = (s, f) => {
13
+
let t = f(s.proof);
14
+
{
15
+
fixes: t.fixes->Array.concat(s.fixes),
16
+
facts: Dict.copy(s.facts)->Dict.assign(t.facts),
17
+
proof: t.proof
18
+
}
19
+
}
20
+
}
21
+
module Goal = {
22
+
type t = {
23
+
fix: array<Term.meta>,
24
+
assume: array<Rule.t>,
25
+
assumeNames: array<string>,
26
+
show: Judgment.t
27
+
}
28
+
let toRule : t => Rule.t = (goal : t) => {
29
+
vars: goal.fix,
30
+
premises: goal.assume,
31
+
conclusion: goal.show
32
+
}
33
+
}
34
+
module type PROOFT = {
35
+
type t<'a>
36
+
let subproofs : (Goal.t,t<'a>, 'a=>Goal.t) => Dict.t<Step.t<'a>>
37
+
}
38
+
module Either = (A : PROOFT, B : PROOFT) => {
39
+
type t<'a> = L(A.t<'a>) | R(B.t<'a>)
40
+
let subproofs = (goal:Goal.t,it : t<'a>, f : 'a => Goal.t) => switch it {
41
+
| L(x) => A.subproofs(goal,x,f)
42
+
| R(x) => B.subproofs(goal,x,f)
43
+
}
44
+
}
45
+
46
+
module Deduction : PROOFT = {
47
+
type t<'a> = {
48
+
from: array<'a>,
49
+
ruleName: string,
50
+
instantiation: array<Term.t>
51
+
}
52
+
let subproofs = (goal : Goal.t,it : t<'a>, _ : 'a => Goal.t) => {
53
+
let toStep : 'a => Step.t<'a> = (a) => {
54
+
fixes: goal.fix,
55
+
facts: Belt.Array.zip(goal.assumeNames,goal.assume)->Dict.fromArray,
56
+
proof: a
57
+
};
58
+
Belt.Array.range(0,Array.length(it.from))
59
+
->Array.map(x =>Belt.Int.toString(x))
60
+
->Belt.Array.zip(it.from->Array.map(toStep))
61
+
->Dict.fromArray
62
+
}
63
+
}
64
+
module Lemma : PROOFT = {
65
+
type t<'a> = {
66
+
name: string,
67
+
have: 'a,
68
+
show: 'a
69
+
}
70
+
let subproofs = (goal: Goal.t,it : t<'a>, f : 'a => Goal.t) => {
71
+
let haveGoal : Step.t<'a> = {
72
+
fixes: goal.fix,
73
+
facts: Belt.Array.zip(goal.assumeNames,goal.assume)->Dict.fromArray,
74
+
proof: it.have
75
+
};
76
+
let showGoal : Step.t<'a> = {
77
+
fixes: goal.fix,
78
+
facts: Belt.Array.zip(goal.assumeNames,goal.assume)
79
+
->Array.concat([(it.name,f(it.have)->Goal.toRule)])
80
+
->Dict.fromArray,
81
+
proof: it.show
82
+
};
83
+
Dict.fromArray([(it.name,haveGoal), ("@show",showGoal)])
84
+
}
85
+
}
86
+
module Proof = (A : PROOFT) => {
87
+
type rec t = {goal:Goal.t, step?: A.t<t> }
88
+
}
89
+
}
90
+
//module TestProofs = Proof(Either(Deduction,Lemma))
+188
src/Rule.res
+188
src/Rule.res
···
1
+
open Signatures
2
+
// the tree sitter plugin hates backslashes in string literals unless they're on the top
3
+
// level..
4
+
let vinculumRES = "^\s*\\n\\s*[-—][-—][\\-—]+([^\\n\\-—][^\\n]*)?"
5
+
module Make = (Term : TERM, Judgment : JUDGMENT with module Term := Term) => {
6
+
type rec t = {vars: array<Term.meta>, premises: array<t>, conclusion: Judgment.t}
7
+
let rec substitute = (rule: t, subst: Term.subst) => {
8
+
let subst' = subst->Util.mapMapValues(v => v->Term.upshift(Array.length(rule.vars)));
9
+
{
10
+
vars: rule.vars,
11
+
premises: rule.premises->Array.map(premise => premise->substitute(subst')),
12
+
conclusion: rule.conclusion->Judgment.substitute(subst')
13
+
}
14
+
}
15
+
let rec substDeBruijn = (rule: t, substs: array<Term.t>, ~from:int=0) => {
16
+
let len = Array.length(rule.vars)
17
+
let substs' = substs->Array.map(v => v->Term.upshift(len,~from=from))
18
+
{
19
+
vars: rule.vars,
20
+
premises: rule.premises
21
+
->Array.map(premise => premise->substDeBruijn(substs', ~from=from+len)),
22
+
conclusion: rule.conclusion
23
+
->Judgment.substDeBruijn(substs',~from=from+len),
24
+
}
25
+
}
26
+
let rec upshift = (rule: t, amount: int, ~from:int=0) => {
27
+
let len = Array.length(rule.vars)
28
+
{
29
+
vars: rule.vars,
30
+
premises: rule.premises->Array.map(r => r->upshift(amount, ~from = from + len)),
31
+
conclusion: rule.conclusion->Judgment.upshift(amount, ~from = from + len)
32
+
}
33
+
}
34
+
type bare = { premises: array<t>, conclusion: Judgment.t }
35
+
let instantiate = (rule: t, terms: array<Term.t>) => {
36
+
assert(Array.length(terms) == Array.length(rule.vars))
37
+
let terms' = [...terms]
38
+
Array.reverse(terms')
39
+
{
40
+
premises: rule.premises->Array.map(r => r-> substDeBruijn(terms')),
41
+
conclusion: rule.conclusion->Judgment.substDeBruijn(terms')
42
+
}
43
+
}
44
+
45
+
let parseVinculum = (str) => {
46
+
let re = RegExp.fromStringWithFlags(vinculumRES,~flags="y")
47
+
switch re->RegExp.exec(str) {
48
+
| None => Error("expected vinculum")
49
+
| Some(res) => { switch res[1] {
50
+
| Some(Some(n)) if String.trim(n) != ""
51
+
=> Ok(n,String.sliceToEnd(str,~start=RegExp.lastIndex(re)))
52
+
| _ => Ok("", String.sliceToEnd(str,~start=RegExp.lastIndex(re)))
53
+
}}
54
+
}
55
+
}
56
+
exception InternalParseError(string)
57
+
let rec parseInner = (string, ~scope=[]: array<Term.meta>, ~gen=?) => {
58
+
if (string->String.trim->String.get(0) == Some("[")) {
59
+
let cur = ref(String.make(string->String.trim->String.sliceToEnd(~start=1)));
60
+
let it = ref(Error(""))
61
+
let vars = []
62
+
while {it := Term.parseMeta(cur.contents); it.contents->Result.isOk} {
63
+
let (str,rest) = Result.getExn(it.contents)
64
+
Array.unshift(vars,str)
65
+
cur := rest
66
+
}
67
+
let it = ref(Error(""))
68
+
let premises = []
69
+
switch {
70
+
while (cur.contents->String.trim->String.slice(~start=0,~end=2) != "|-"
71
+
&& cur.contents->String.trim->String.get(0) != Some("]")) {
72
+
switch parseInner(cur.contents,~scope=vars->Array.concat(scope), ~gen=?gen) {
73
+
| Ok(p,rest) => {
74
+
cur := rest
75
+
premises->Array.push(p)
76
+
}
77
+
| Error(_) => raise(InternalParseError("expected turnstile or premise"))
78
+
}
79
+
}
80
+
if (cur.contents->String.trim->String.get(0) == Some("]")) {
81
+
let rest = cur.contents->String.trim->String.sliceToEnd(~start=1)
82
+
cur := rest
83
+
switch premises {
84
+
| [{vars:[],premises:[],conclusion:e}] => Ok(({vars,premises:[],conclusion:e}, rest))
85
+
| _ => Error("Conclusion appears to be multiple terms")
86
+
}
87
+
} else {
88
+
cur := cur.contents->String.trim->String.sliceToEnd(~start=2)
89
+
switch Judgment.parse(cur.contents,~scope=vars->Array.concat(scope),~gen=?gen) {
90
+
| Ok(conclusion, rest) =>
91
+
if (rest->String.trim->String.get(0) == Some("]")) {
92
+
cur := rest->String.trim->String.sliceToEnd(~start=1);
93
+
Ok(({vars, premises, conclusion}, cur.contents))
94
+
} else {
95
+
Error("Expected closing bracket")
96
+
}
97
+
| Error(e) => Error(e)
98
+
}
99
+
}
100
+
} {
101
+
| exception InternalParseError(e) => Error(e)
102
+
| v => v
103
+
}
104
+
} else {
105
+
switch Judgment.parse(string,~scope,~gen=?gen) {
106
+
| Ok(conclusion, rest) => Ok(({vars:[], premises:[], conclusion}, rest))
107
+
| Error(e) => Error(e)
108
+
}
109
+
}
110
+
}
111
+
let parseTopLevel = (string, ~gen=?, ~scope=[]) => {
112
+
let cur = ref(String.make(string));
113
+
let it = ref(Error(""))
114
+
let vars = []
115
+
switch {
116
+
while {it := Term.parseMeta(cur.contents); it.contents->Result.isOk} {
117
+
let (str,rest) = Result.getExn(it.contents)
118
+
Array.unshift(vars,str)
119
+
cur := rest
120
+
}
121
+
let it = ref(Error(""))
122
+
let premises = []
123
+
while {it := parseVinculum(cur.contents); it.contents->Result.isError} {
124
+
switch parseInner(cur.contents,~scope=vars->Array.concat(scope), ~gen=?gen) {
125
+
| Ok(p,rest) => {
126
+
cur := rest
127
+
premises->Array.push(p)
128
+
}
129
+
| Error(e) => raise(InternalParseError(e))
130
+
}
131
+
}
132
+
let (ruleName,rest) = it.contents->Result.getExn
133
+
cur := rest
134
+
switch Judgment.parse(cur.contents,~scope=vars->Array.concat(scope),~gen=?gen) {
135
+
| Ok(conclusion, rest) => Ok((({vars, premises, conclusion}, ruleName), rest))
136
+
| Error(e) => Error(e)
137
+
}
138
+
} {
139
+
| exception InternalParseError(e) => Error(e)
140
+
| v => v
141
+
}
142
+
}
143
+
144
+
let rec prettyPrintInline = (rule: t,~scope=[]:array<Term.meta>) => {
145
+
switch rule {
146
+
| {vars: [], premises: [], conclusion: c} => Judgment.prettyPrint(c,~scope)
147
+
| _ => {
148
+
"["->String.concat(
149
+
rule.vars
150
+
->Array.map(Term.prettyPrintMeta)
151
+
->Array.join("")
152
+
->String.concat(" ")
153
+
->String.concat(if Array.length(rule.premises) == 0 {
154
+
Judgment.prettyPrint(rule.conclusion,~scope=[...rule.vars,...scope])
155
+
} else {
156
+
rule.premises
157
+
->Array.map(r => prettyPrintInline(r,~scope=[...rule.vars,...scope]))->Array.join(" ")
158
+
->String.concat(" |- ")
159
+
->String.concat(Judgment.prettyPrint(rule.conclusion,~scope=[...rule.vars,...scope]))
160
+
}
161
+
))->String.concat("]")
162
+
}
163
+
}
164
+
}
165
+
let rec prettyPrintTopLevel = (rule: t,~name="",~scope=[]:array<Term.meta>) => {
166
+
let vinculise = (strs: array<string>) => {
167
+
let l = strs->Array.map(String.length)->Array.concat([4])->Math.Int.maxMany
168
+
strs->Array.concat(["-"->String.repeat(l)->String.concat(" ")->String.concat(name)])
169
+
}
170
+
let myReverse = (arr) => {
171
+
Array.reverse(arr)
172
+
arr
173
+
}
174
+
rule.vars
175
+
->Array.map(Term.prettyPrintMeta)
176
+
->myReverse
177
+
->Array.join("")
178
+
->String.concat(Util.newline)
179
+
->String.concat(
180
+
rule.premises
181
+
->Array.map(r => prettyPrintInline(r,~scope=[...rule.vars,...scope]))
182
+
->vinculise
183
+
->Array.concat([Judgment.prettyPrint(rule.conclusion,
184
+
~scope=[...rule.vars,...scope])])
185
+
->Array.map(s => String.concat(" ",s))
186
+
->Array.join(Util.newline))
187
+
}
188
+
}
+123
src/RuleView.res
+123
src/RuleView.res
···
1
+
open Signatures
2
+
module Make = (
3
+
Term : TERM,
4
+
Judgment : JUDGMENT with module Term := Term,
5
+
JudgmentView : JUDGMENT_VIEW with module Term := Term and module Judgment := Judgment
6
+
) => {
7
+
module Rule = Rule.Make(Term, Judgment)
8
+
9
+
type style = Gentzen | Linear | Hybrid
10
+
11
+
type props = {
12
+
rule:Rule.t,
13
+
style: style,
14
+
scope?: array<Term.meta>,
15
+
children: React.element
16
+
}
17
+
module type RULE_COMPONENT = {
18
+
let make : props => React.element
19
+
}
20
+
module Inline : RULE_COMPONENT = {
21
+
let rec make = (props : props) => {
22
+
let {vars, premises,conclusion} = props.rule
23
+
let scope = vars->Array.concat(props.scope->Option.getOr([]))
24
+
let arr = vars->Array.map(JudgmentView.TermView.makeMeta)
25
+
Array.reverse(arr)
26
+
<span className="inline-rule">
27
+
<span className="rule-rulename-defined">
28
+
{props.children}
29
+
</span>
30
+
{if Array.length(arr) > 0 { <span className="rule-binders">{React.array(arr)}</span> }
31
+
else { React.string("") }}
32
+
{React.array(premises
33
+
->Array.map(p=><span className="rule-context">
34
+
{make({rule:p, scope,children:React.string(""),style:props.style})}</span>)
35
+
->Array.flatMapWithIndex( (e, i) =>
36
+
if i == 0 {
37
+
[e]
38
+
} else {
39
+
[<span className="symbol symbol-bold symbol-comma">{React.string(",")}</span>,e]
40
+
}))}
41
+
{if premises->Array.length > 0 {
42
+
<span className="symbol symbol-turnstile symbol-bold">
43
+
{React.string("⊢")}
44
+
</span>
45
+
} else {
46
+
React.string("")
47
+
}}
48
+
<JudgmentView judgment={conclusion}
49
+
scope={scope} />
50
+
</span>
51
+
}
52
+
}
53
+
module Hypothetical = (Premise : RULE_COMPONENT) => {
54
+
let make = (props : props) => if Array.length(props.rule.premises) == 0 { Inline.make(props) } else {
55
+
let {vars, premises,conclusion} = props.rule
56
+
let arr = vars->Array.map(JudgmentView.TermView.makeMeta)
57
+
Array.reverse(arr)
58
+
let scope = vars->Array.concat(props.scope->Option.getOr([]))
59
+
<table className="inference">
60
+
<tr><td className="rule-cell rule-binderbox" rowSpan=3>{React.array(arr)}</td>
61
+
{React.array(premises->Array.map(p=>
62
+
<td className="rule-cell rule-premise">
63
+
<Premise rule={p} scope={scope} style={props.style}>
64
+
{React.string("")}
65
+
</Premise>
66
+
</td>))}
67
+
<td className="rule-cell rule-spacer"></td>
68
+
<td rowSpan=3 className="rule-cell rule-rulebox">
69
+
<span className="rule-rulename-defined">
70
+
{props.children}
71
+
</span>
72
+
</td>
73
+
</tr>
74
+
<tr> <td colSpan={premises->Array.length + 1} className="rule-cell">
75
+
{React.string("⋮")}
76
+
</td></tr>
77
+
<tr>
78
+
<td colSpan={premises->Array.length + 1} className="rule-cell rule-hypothetical-conclusion">
79
+
<JudgmentView judgment={conclusion} scope={scope} />
80
+
</td>
81
+
</tr></table>
82
+
}
83
+
}
84
+
module TopLevel = (Premise : RULE_COMPONENT) => {
85
+
let make = (props : props) => {
86
+
let {vars, premises,conclusion} = props.rule
87
+
let arr = vars->Array.map(JudgmentView.TermView.makeMeta)
88
+
Array.reverse(arr)
89
+
let scope = vars->Array.concat(props.scope->Option.getOr([]))
90
+
<div className="axiom"><table className="inference">
91
+
<tr><td className="rule-cell rule-binderbox" rowSpan=2>{React.array(arr)}</td>
92
+
{React.array(premises->Array.map(p=>
93
+
<td className="rule-cell rule-premise">
94
+
<Premise rule={p} scope={scope} style={props.style}>
95
+
{React.string("")}
96
+
</Premise>
97
+
</td>))}
98
+
<td className="rule-cell rule-spacer"></td>
99
+
<td rowSpan=2 className="rule-cell rule-rulebox">
100
+
<span className="rule-rulename-defined">
101
+
{props.children}
102
+
</span>
103
+
</td>
104
+
</tr>
105
+
<tr>
106
+
<td colSpan={premises->Array.length + 1} className="rule-cell rule-conclusion">
107
+
<JudgmentView judgment={conclusion} scope={scope} />
108
+
</td>
109
+
</tr></table></div>
110
+
}
111
+
}
112
+
module Gentzen = TopLevel(Hypothetical(Inline))
113
+
module Hybrid = TopLevel(Inline)
114
+
115
+
@react.componentWithProps
116
+
let make = (props) => {
117
+
switch (props.style) {
118
+
| Hybrid => Hybrid.make(props)
119
+
| Gentzen => Gentzen.make(props)
120
+
| Linear => Inline.make(props)
121
+
}
122
+
}
123
+
}
-1
src/SExp.res
-1
src/SExp.res
+12
src/SExp.resi
+12
src/SExp.resi
···
1
+
2
+
type rec t =
3
+
Symbol({name: string })
4
+
| Compound({subexps: array<t>})
5
+
| Var({idx:int})
6
+
| Schematic({schematic:int, allowed: array<int>})
7
+
8
+
include Signatures.TERM with
9
+
type t := t and
10
+
type meta = string and
11
+
type schematic = int and
12
+
type subst = Map.t<int,t>
+6
src/SExpJView.res
+6
src/SExpJView.res
+1
src/SExpJView.resi
+1
src/SExpJView.resi
···
1
+
include Signatures.JUDGMENT_VIEW with module Term := SExp and module Judgment := SExp
+52
src/SExpView.res
+52
src/SExpView.res
···
1
+
type props = {term: SExp.t, scope: array<string>}
2
+
3
+
let viewVar = (idx, scope:array<string>) => switch scope[idx] {
4
+
| Some(n) if Array.indexOf(scope,n) == idx =>
5
+
<span className="term-metavar">
6
+
{ React.string(n)}
7
+
</span>
8
+
| _ =>
9
+
<span className="term-metavar-unnamed">
10
+
{React.string("\\")} { React.int(idx) }
11
+
</span>
12
+
}
13
+
14
+
let makeMeta = (str : string) =>
15
+
<span className="rule-binder">
16
+
{React.string(str)}{React.string(".")}
17
+
</span>
18
+
19
+
let parenthesise = (f) => [
20
+
<span className="symbol">
21
+
{React.string("(")}
22
+
</span>,
23
+
...f,
24
+
<span className="symbol">
25
+
{React.string(")")}
26
+
</span>
27
+
]
28
+
29
+
let intersperse = (a) =>
30
+
a->Array.flatMapWithIndex((e, i) => if i == 0 { [e] } else { [React.string(" "),e] })
31
+
32
+
@react.componentWithProps
33
+
let rec make = ({term, scope}) => switch term {
34
+
| Compound({subexps:bits}) => {
35
+
<span className="term-compound">
36
+
{bits
37
+
->Array.map(t => make({term:t,scope}))
38
+
->intersperse->parenthesise->React.array}
39
+
</span>
40
+
}
41
+
| Var({idx:idx}) => viewVar(idx,scope)
42
+
| Symbol({name:s}) => <span className="term-const"> { React.string(s) } </span>
43
+
| Schematic({schematic:s, allowed:vs}) =>
44
+
<span className="term-schematic">
45
+
{React.string("?")} {React.int(s)}
46
+
<span className="term-schematic-telescope">
47
+
{vs
48
+
->Array.map(v => viewVar(v,scope))
49
+
->intersperse->parenthesise->React.array}
50
+
</span>
51
+
</span>
52
+
}
+1
src/SExpView.resi
+1
src/SExpView.resi
···
1
+
include Signatures.TERM_VIEW with module Term := SExp
+6
src/Scratch.res
+6
src/Scratch.res
+49
src/Signatures.res
+49
src/Signatures.res
···
1
+
2
+
module type TERM = {
3
+
type t
4
+
type schematic
5
+
type meta
6
+
type subst = Map.t<schematic,t>
7
+
let substitute : (t, subst) => t
8
+
let unify : (t, t) => array<subst>
9
+
let substDeBruijn : (t, array<t>, ~from:int=?) => t
10
+
let upshift : (t, int, ~from:int=?) => t
11
+
type gen
12
+
let fresh : (gen, ~replacing:meta=?) => schematic
13
+
let seen : (gen, schematic) => ()
14
+
let place : (schematic, ~scope: array<meta>) => t
15
+
let makeGen : () => gen
16
+
let parse : (string, ~scope: array<meta>, ~gen: gen=?) => result<(t,string),string>
17
+
let parseMeta : (string) => result<(meta,string),string>
18
+
let prettyPrint : (t, ~scope: array<meta>) => string
19
+
let prettyPrintMeta : (meta) => string
20
+
}
21
+
22
+
module type JUDGMENT = {
23
+
module Term : TERM
24
+
type t
25
+
let substitute : (t, Term.subst) => t
26
+
let unify : (t, t) => array<Term.subst>
27
+
let substDeBruijn : (t, array<Term.t>, ~from:int=?) => t
28
+
let upshift : (t, int, ~from:int=?) => t
29
+
let parse : (string, ~scope: array<Term.meta>, ~gen: Term.gen=?) => result<(t,string),string>
30
+
let prettyPrint : (t, ~scope: array<Term.meta>) => string
31
+
}
32
+
33
+
34
+
module type TERM_VIEW = {
35
+
module Term : TERM
36
+
type props = {term: Term.t, scope: array<Term.meta>}
37
+
let make : props => React.element
38
+
let makeMeta : Term.meta => React.element
39
+
}
40
+
41
+
module type JUDGMENT_VIEW = {
42
+
module Term : TERM
43
+
module Judgment : JUDGMENT with module Term := Term;
44
+
module TermView : TERM_VIEW with module Term := Term;
45
+
type props = {judgment: Judgment.t, scope: array<Term.meta>}
46
+
let make : props => React.element
47
+
}
48
+
49
+
-459
src/Test.res
-459
src/Test.res
···
1
-
open Demo
2
-
module type TERM_VIEW = {
3
-
module Term : TERM
4
-
type props = {term: Term.t, scope: array<Term.meta>}
5
-
let make : props => React.element
6
-
let makeMeta : Term.meta => React.element
7
-
}
8
-
9
-
module type JUDGMENT_VIEW = {
10
-
module Base : BASE
11
-
open Base
12
-
module TermView : TERM_VIEW with module Term := Term;
13
-
type props = {judgment: Judgment.t, scope: array<Term.meta>}
14
-
let make : props => React.element
15
-
}
16
-
17
-
module SExpView : TERM_VIEW with module Term := SExp = {
18
-
19
-
type props = {term: SExp.t, scope: array<string>}
20
-
let viewVar = (idx, scope:array<string>) => {
21
-
switch scope[idx] {
22
-
| Some(n) if Array.indexOf(scope,n) == idx => <span className="term-metavar"> { React.string(n) } </span>
23
-
| _ => <span className="term-metavar-unnamed"> {React.string("\\")} { React.int(idx) } </span>
24
-
}
25
-
}
26
-
let makeMeta = (str : string) => {
27
-
<span className="rule-binder">{React.string(str)}{React.string(".")}</span>
28
-
}
29
-
let parenthesise = (f) =>
30
-
[<span className="symbol">{React.string("(")}</span>,...f,<span className="symbol">{React.string(")")}</span>]
31
-
let intersperse = (a) => a->Array.flatMapWithIndex((e, i) =>
32
-
if i == 0 { [e] } else { [React.string(" "),e] })
33
-
@react.componentWithProps
34
-
let rec make = ({term, scope}) => switch term {
35
-
| Compound({subexps:bits}) => {
36
-
<span className="term-compound">
37
-
{bits
38
-
->Array.map(t => make({term:t,scope}))
39
-
->intersperse->parenthesise->React.array}
40
-
</span>
41
-
}
42
-
| Var({idx:idx}) => viewVar(idx,scope)
43
-
| Symbol({name:s}) => <span className="term-const"> { React.string(s) } </span>
44
-
| Schematic({schematic:s, allowed:vs}) =>
45
-
<span className="term-schematic">
46
-
{React.string("?")} {React.int(s)}
47
-
<span className="term-schematic-telescope">
48
-
{vs
49
-
->Array.map(v => viewVar(v,scope))
50
-
->intersperse->parenthesise->React.array}
51
-
</span>
52
-
</span>
53
-
}
54
-
}
55
-
module SExpBase = {module Term = SExp; module Judgment = SExp}
56
-
module SExpJView : JUDGMENT_VIEW with module Base := SExpBase = {
57
-
module TermView = SExpView
58
-
type props = {judgment: SExp.t, scope: array<string>}
59
-
let make = (props : props) => SExpView.make({term: props.judgment,scope:props.scope})
60
-
}
61
-
62
-
module RuleView = (Base : BASE,
63
-
TermView : TERM_VIEW with module Term := Base.Term,
64
-
JudgmentView : JUDGMENT_VIEW with module Base := Base) => {
65
-
module PE = ProofEngine(Base)
66
-
open PE
67
-
type style = Gentzen | Linear | Hybrid
68
-
69
-
type props = {rule:Rule.t, style: style, scope?: array<Base.Term.meta>, children: React.element}
70
-
module type RULE_COMPONENT = {
71
-
let make : props => React.element
72
-
}
73
-
module Inline : RULE_COMPONENT = {
74
-
let rec make = (props : props) => {
75
-
let {vars, premises,conclusion} = props.rule
76
-
let scope = vars->Array.concat(props.scope->Option.getOr([]))
77
-
let arr = vars->Array.map(TermView.makeMeta)
78
-
Array.reverse(arr)
79
-
<span className="inline-rule">
80
-
<span className="rule-rulename-defined">
81
-
{props.children}
82
-
</span>
83
-
{if Array.length(arr) > 0 { <span className="rule-binders">{React.array(arr)}</span> }
84
-
else { React.string("") }}
85
-
{React.array(premises
86
-
->Array.map(p=><span className="rule-context">
87
-
{make({rule:p, scope,children:React.string(""),style:props.style})}</span>)
88
-
->Array.flatMapWithIndex( (e, i) =>
89
-
if i == 0 {
90
-
[e]
91
-
} else {
92
-
[<span className="symbol symbol-bold symbol-comma">{React.string(",")}</span>,e]
93
-
}))}
94
-
{if premises->Array.length > 0 {
95
-
<span className="symbol symbol-turnstile symbol-bold">
96
-
{React.string("⊢")}
97
-
</span>
98
-
} else {
99
-
React.string("")
100
-
}}
101
-
<JudgmentView judgment={conclusion}
102
-
scope={scope} />
103
-
</span>
104
-
}
105
-
}
106
-
module Hypothetical = (Premise : RULE_COMPONENT) => {
107
-
let make = (props : props) => if Array.length(props.rule.premises) == 0 { Inline.make(props) } else {
108
-
let {vars, premises,conclusion} = props.rule
109
-
let arr = vars->Array.map(TermView.makeMeta)
110
-
Array.reverse(arr)
111
-
let scope = vars->Array.concat(props.scope->Option.getOr([]))
112
-
<table className="inference">
113
-
<tr><td className="rule-cell rule-binderbox" rowSpan=3>{React.array(arr)}</td>
114
-
{React.array(premises->Array.map(p=>
115
-
<td className="rule-cell rule-premise">
116
-
<Premise rule={p} scope={scope} style={props.style}>
117
-
{React.string("")}
118
-
</Premise>
119
-
</td>))}
120
-
<td className="rule-cell rule-spacer"></td>
121
-
<td rowSpan=3 className="rule-cell rule-rulebox">
122
-
<span className="rule-rulename-defined">
123
-
{props.children}
124
-
</span>
125
-
</td>
126
-
</tr>
127
-
<tr> <td colSpan={premises->Array.length + 1} className="rule-cell">
128
-
{React.string("⋮")}
129
-
</td></tr>
130
-
<tr>
131
-
<td colSpan={premises->Array.length + 1} className="rule-cell rule-hypothetical-conclusion">
132
-
<JudgmentView judgment={conclusion} scope={scope} />
133
-
</td>
134
-
</tr></table>
135
-
}
136
-
}
137
-
module TopLevel = (Premise : RULE_COMPONENT) => {
138
-
let make = (props : props) => {
139
-
let {vars, premises,conclusion} = props.rule
140
-
let arr = vars->Array.map(TermView.makeMeta)
141
-
Array.reverse(arr)
142
-
let scope = vars->Array.concat(props.scope->Option.getOr([]))
143
-
<div className="axiom"><table className="inference">
144
-
<tr><td className="rule-cell rule-binderbox" rowSpan=2>{React.array(arr)}</td>
145
-
{React.array(premises->Array.map(p=>
146
-
<td className="rule-cell rule-premise">
147
-
<Premise rule={p} scope={scope} style={props.style}>
148
-
{React.string("")}
149
-
</Premise>
150
-
</td>))}
151
-
<td className="rule-cell rule-spacer"></td>
152
-
<td rowSpan=2 className="rule-cell rule-rulebox">
153
-
<span className="rule-rulename-defined">
154
-
{props.children}
155
-
</span>
156
-
</td>
157
-
</tr>
158
-
<tr>
159
-
<td colSpan={premises->Array.length + 1} className="rule-cell rule-conclusion">
160
-
<JudgmentView judgment={conclusion} scope={scope} />
161
-
</td>
162
-
</tr></table></div>
163
-
}
164
-
}
165
-
module Gentzen = TopLevel(Hypothetical(Inline))
166
-
module Hybrid = TopLevel(Inline)
167
-
168
-
@react.componentWithProps
169
-
let make = (props) => {
170
-
switch (props.style) {
171
-
| Hybrid => Hybrid.make(props)
172
-
| Gentzen => Gentzen.make(props)
173
-
| Linear => Inline.make(props)
174
-
}
175
-
}
176
-
}
177
-
178
-
179
-
180
-
module type TEXTUAL_COMPONENT = {
181
-
type props
182
-
type state
183
-
let getState : props => state
184
-
let setState : (props,state) => props
185
-
let serialise : (props, state) => string
186
-
let deserialise : (props, string) => result<state,string>
187
-
let onChange : props => ()
188
-
let make : props => React.element
189
-
}
190
-
191
-
module TermTextualComponent =
192
-
(Term : TERM, TermView : TERM_VIEW with module Term := Term ) => {
193
-
type state = Term.t
194
-
type rec props = {
195
-
term: Term.t,
196
-
scope: array<Term.meta>,
197
-
gen?: Term.gen,
198
-
onChange: props => ()
199
-
}
200
-
let getState = (props) => props.term
201
-
let setState = (props,state) => {...props,term:state}
202
-
203
-
let serialise = (props : props,state) => {
204
-
state->Term.prettyPrint(~scope=props.scope)
205
-
}
206
-
let onChange = (props) => props.onChange(props)
207
-
let deserialise = (props : props, str : string) => {
208
-
switch Term.parse(str,~scope=props.scope,~gen=?props.gen) {
209
-
| Ok(t,"") => { Ok(t) }
210
-
| Ok(_,_) => Error("additional input beyond expression")
211
-
| Error(e) => Error(e)
212
-
}
213
-
}
214
-
let make = ({term,scope}) => {
215
-
<TermView term=term scope=scope/>
216
-
}
217
-
}
218
-
module JudgmentTextualComponent =
219
-
(Base : BASE, JudgmentView : JUDGMENT_VIEW with module Base := Base ) => {
220
-
open Base
221
-
type rec props = {
222
-
judgment: Judgment.t,
223
-
scope: array<Term.meta>,
224
-
gen?: Term.gen,
225
-
onChange: props => ()
226
-
}
227
-
type state = Judgment.t
228
-
let getState = (props) => props.judgment
229
-
let setState = (props,judgment) => {...props,judgment}
230
-
let onChange = (props) => props.onChange(props)
231
-
let serialise = (props : props, state:state) => {
232
-
state->Judgment.prettyPrint(~scope=props.scope)
233
-
}
234
-
let deserialise = (props : props, str : string) => {
235
-
switch Judgment.parse(str,~scope=props.scope,~gen=?props.gen) {
236
-
| Ok(t,"") => Ok(t)
237
-
| Ok(_,_) => Error("additional input beyond expression")
238
-
| Error(e) => Error(e)
239
-
}
240
-
}
241
-
let make = ({judgment,scope}) => {
242
-
<JudgmentView judgment=judgment scope=scope/>
243
-
}
244
-
}
245
-
module RuleTextualComponent = (
246
-
Base : BASE,
247
-
TermView : TERM_VIEW with module Term := Base.Term,
248
-
JudgmentView : JUDGMENT_VIEW with module Base := Base
249
-
) => {
250
-
module PE = ProofEngine(Base)
251
-
open PE
252
-
open Base
253
-
module TheRuleView = RuleView(Base,TermView,JudgmentView)
254
-
type rec props = {
255
-
rule: Rule.t,
256
-
scope: array<Term.meta>,
257
-
name?: string,
258
-
gen?: Term.gen,
259
-
style: TheRuleView.style,
260
-
onChange: props => ()
261
-
}
262
-
type state = (Rule.t, string)
263
-
let getState = (props) => (props.rule,props.name->Option.getOr(""))
264
-
let setState = (props,(rule,name)) => {...props,rule,name}
265
-
let onChange = (props) => props.onChange(props)
266
-
let serialise = (props : props, state) => {
267
-
state->Rule.prettyPrintTopLevel(~scope=props.scope,~name=?props.name)
268
-
}
269
-
let deserialise = (props : props, str : string) => {
270
-
switch Rule.parseTopLevel(str,~scope=props.scope,~gen=?props.gen) {
271
-
| Ok(r,"") => Ok(r)
272
-
| Ok(_,_) => Error("additional input beyond expression")
273
-
| Error(e) => Error(e)
274
-
}
275
-
}
276
-
let make = (props) => {
277
-
<TheRuleView rule={props.rule} scope={props.scope}
278
-
style={props.style}>
279
-
{React.string(props.name->Option.getOr(""))}
280
-
</TheRuleView>
281
-
}
282
-
}
283
-
284
-
module RuleSetTextualComponent = (
285
-
Base : BASE,
286
-
TermView : TERM_VIEW with module Term := Base.Term,
287
-
JudgmentView : JUDGMENT_VIEW with module Base := Base
288
-
) => {
289
-
module PE = ProofEngine(Base)
290
-
open PE
291
-
open Base
292
-
module TheRuleView = RuleView(Base,TermView,JudgmentView)
293
-
type state = Dict.t<Rule.t>
294
-
type rec props = {
295
-
rules: Dict.t<Rule.t>,
296
-
style: TheRuleView.style,
297
-
onChange: props => ()
298
-
}
299
-
let getState = (props) => props.rules
300
-
let setState = (props,state) => {...props,rules:state}
301
-
let onChange = (props) => props.onChange(props)
302
-
let serialise = (props : props, state) => {
303
-
let results = [];
304
-
state->Dict.forEachWithKey((value, key) => {
305
-
results->Array.push(value->Rule.prettyPrintTopLevel(~scope=[],~name=key))
306
-
})
307
-
results->Array.join(Demo.newline)
308
-
}
309
-
let deserialise = (props : props, str : string) => {
310
-
let cur = ref(str)
311
-
let go = ref(true)
312
-
let results = Dict.make()
313
-
let ret = ref(Error("impossible"))
314
-
while go.contents {
315
-
switch Rule.parseTopLevel(cur.contents,~scope=[]) {
316
-
| Ok((t,n),rest) => {
317
-
if n->String.trim == "" {
318
-
go := false
319
-
ret := Error("Rule given with no name")
320
-
} else {
321
-
Dict.set(results,n,t)
322
-
if rest->String.trim == "" {
323
-
go := false
324
-
ret := Ok(results)
325
-
} else {
326
-
cur := rest
327
-
}
328
-
}
329
-
}
330
-
| Error(e) => { go := false; ret := Error(e) }
331
-
}
332
-
}
333
-
ret.contents
334
-
}
335
-
let make = (props) => {
336
-
<div className={"axiom-set axiom-set-"->String.concat(String.make(props.style))}>
337
-
{ Dict.toArray(props.rules)->Array.map(((n,r)) =>
338
-
<TheRuleView rule={r} scope={[]} style={props.style}>
339
-
{React.string(n)}
340
-
</TheRuleView>)
341
-
->React.array
342
-
}
343
-
</div>
344
-
}
345
-
}
346
-
347
-
module Editable = (Underlying : TEXTUAL_COMPONENT) => {
348
-
type props = Underlying.props
349
-
@react.componentWithProps
350
-
let make = props => {
351
-
352
-
let (editing,setEditing) = React.useState (_ => "off")
353
-
let (tree,setTree) = React.useState (_=>Underlying.getState(props))
354
-
let (text,setText) =
355
-
React.useState (_=> Underlying.serialise(props,tree))
356
-
let done = _ => {
357
-
switch Underlying.deserialise(props,text) {
358
-
| Ok(t) => {
359
-
setTree(_ => t)
360
-
Underlying.onChange(Underlying.setState(props,t))
361
-
setText(_=> Underlying.serialise(props,t))
362
-
setEditing(_=>"off")
363
-
}
364
-
| Error(e) => {
365
-
setEditing(_=>e)
366
-
}
367
-
}
368
-
}
369
-
let onChange= (ev: JsxEvent.Form.t) => {
370
-
let target = JsxEvent.Form.target(ev)
371
-
let value: string = target["value"]
372
-
setText(_ => value)
373
-
}
374
-
if editing == "on" {
375
-
<div><input value={text} onChange={onChange}/><div onClick={done}>{React.string("DONE")}</div></div>
376
-
} else if editing == "off" {
377
-
<div onClick={_ => setEditing(_ => "on")}>
378
-
{Underlying.make(Underlying.setState(props,tree))}
379
-
</div>
380
-
} else {
381
-
<div onClick={_ => setEditing(_ => "on")}>{React.string(editing)}</div>
382
-
}
383
-
}
384
-
}
385
-
386
-
module EditableTextArea = (Underlying : TEXTUAL_COMPONENT) => {
387
-
type props = Underlying.props
388
-
@react.componentWithProps
389
-
let make = props => {
390
-
Console.log(("MK",props))
391
-
let (editing,setEditing) = React.useState (_ => "off")
392
-
let (tree,setTree) = React.useState (_=>Underlying.getState(props))
393
-
let (text,setText) =
394
-
React.useState (_=> Underlying.serialise(props,tree))
395
-
let done = _ => {
396
-
switch Underlying.deserialise(props,text) {
397
-
| Ok(t) => {
398
-
setTree(_ => t)
399
-
Underlying.onChange(Underlying.setState(props,t))
400
-
setText(_=> Underlying.serialise(props,t))
401
-
setEditing(_=>"off")
402
-
}
403
-
| Error(e) => {
404
-
setEditing(_ => e)
405
-
}
406
-
}
407
-
}
408
-
let onChange= (ev: JsxEvent.Form.t) => {
409
-
let target = JsxEvent.Form.target(ev)
410
-
let value: string = target["value"]
411
-
setText(_ => value)
412
-
}
413
-
if editing == "on" {
414
-
<div>
415
-
<textarea className="editor-textArea" onChange={onChange}>
416
-
{React.string(text)}
417
-
</textarea>
418
-
<div className="editor-controls">
419
-
<span className="editor-button button-icon button-icon-blue typcn typcn-tick" onClick={done}>
420
-
</span>
421
-
<span className="editor-button button-icon button-icon-grey typcn typcn-times" onClick={_ => {
422
-
setEditing(_ => "off")
423
-
setText(_=> Underlying.serialise(props,tree))
424
-
}}>
425
-
</span>
426
-
</div>
427
-
</div>
428
-
} else if editing == "off" {
429
-
<div>{Underlying.make(Underlying.setState(props,tree))}
430
-
<div className="editor-controls">
431
-
<span className="editor-button button-icon button-icon-blue typcn typcn-edit" onClick={_ => setEditing(_ => "on")}>
432
-
</span>
433
-
</div>
434
-
</div>
435
-
} else {
436
-
<div className="editor-error">{React.string(editing)}
437
-
<div className="editor-controls">
438
-
<span className="editor-button button-icon button-icon-blue typcn typcn-edit"
439
-
onClick={_ => setEditing(_ => "on")}>
440
-
</span>
441
-
<span className="editor-button button-icon button-icon-grey typcn typcn-times" onClick={_ => {
442
-
setText(_=> Underlying.serialise(props,tree))
443
-
setEditing(_ => "off")
444
-
}}>
445
-
</span>
446
-
</div>
447
-
</div>
448
-
449
-
}
450
-
}
451
-
}
452
-
453
-
module PE2 = ProofEngine(SExpBase)
454
-
module RuleSExpTE = RuleSetTextualComponent(SExpBase,SExpView,SExpJView)
455
-
module RuleSExpView = EditableTextArea(RuleSExpTE)
456
-
include PE2.Rule
457
-
include RuleSExpView//(RuleSExpView.Hypothetical(RuleSExpView.Inline))
458
-
//include SExpBaseView
459
-
+8
src/Util.res
+8
src/Util.res
+1
-2
src/testcomponent.tsx
+1
-2
src/testcomponent.tsx
···
1
1
import * as ComponentGraph2 from './componentgraph'
2
-
import { make as SExpBaseView, RuleSExpTE } from './Test.mjs'
3
-
import { parseTopLevel, prettyPrintTopLevel } from './Test.mjs'
2
+
import { make as SExpBaseView, RuleSExpTE } from './Scratch.mjs'
4
3
import ReactDOM from 'react-dom/client';
5
4
import React from 'react';
6
5