the next generation of the in-browser educational proof assistant
add command res:format and format
+1057
-859
+2
-1
package.json
+2
-1
package.json
+57
-42
src/AxiomSet.res
+57
-42
src/AxiomSet.res
···
1
1
open Signatures
2
2
open Component
3
3
module Make = (
4
-
Term : TERM,
5
-
Judgment : JUDGMENT with module Term := Term,
6
-
JudgmentView : JUDGMENT_VIEW with module Term := Term and module Judgment := Judgment) => {
7
-
module Rule = Rule.Make(Term,Judgment)
8
-
module RuleView = RuleView.Make(Term,Judgment,JudgmentView)
9
-
module Ports = Ports(Term,Judgment)
10
-
type props = { content: string, imports: Ports.t, onLoad: (~exports:Ports.t,~string:string=?) => (), onChange: (string,~exports:Ports.t) => () }
11
-
4
+
Term: TERM,
5
+
Judgment: JUDGMENT with module Term := Term,
6
+
JudgmentView: JUDGMENT_VIEW with module Term := Term and module Judgment := Judgment,
7
+
) => {
8
+
module Rule = Rule.Make(Term, Judgment)
9
+
module RuleView = RuleView.Make(Term, Judgment, JudgmentView)
10
+
module Ports = Ports(Term, Judgment)
11
+
type props = {
12
+
content: string,
13
+
imports: Ports.t,
14
+
onLoad: (~exports: Ports.t, ~string: string=?) => unit,
15
+
onChange: (string, ~exports: Ports.t) => unit,
16
+
}
17
+
12
18
let deserialise = (str: string) => {
13
19
let cur = ref(str)
14
20
let go = ref(true)
15
-
let results = Dict.make()
21
+
let results = Dict.make()
16
22
let ret = ref(Error("impossible"))
17
23
while go.contents {
18
-
switch Rule.parseTopLevel(cur.contents,~scope=[]) {
19
-
| Ok((t,n),rest) => {
20
-
if n->String.trim == "" {
24
+
switch Rule.parseTopLevel(cur.contents, ~scope=[]) {
25
+
| Ok((t, n), rest) => if n->String.trim == "" {
26
+
go := false
27
+
ret := Error("Rule given with no name")
28
+
} else {
29
+
Dict.set(results, n, t)
30
+
if rest->String.trim == "" {
21
31
go := false
22
-
ret := Error("Rule given with no name")
23
-
} else {
24
-
Dict.set(results,n,t)
25
-
if rest->String.trim == "" {
26
-
go := false
27
-
ret := Ok(results)
28
-
} else {
29
-
cur := rest
30
-
}
32
+
ret := Ok(results)
33
+
} else {
34
+
cur := rest
31
35
}
32
36
}
33
-
| Error(e) => { go := false; ret := Error(e) }
37
+
| Error(e) => {
38
+
go := false
39
+
ret := Error(e)
40
+
}
34
41
}
35
42
}
36
43
ret.contents
37
44
}
38
-
39
-
let make = (props ) => {
45
+
46
+
let make = props => {
40
47
switch deserialise(props.content) {
41
48
| Ok(s) => {
42
49
React.useEffect(() => {
43
-
// Run effects
44
-
props.onLoad(~exports= {Ports.facts: s, ruleStyle: None});
50
+
// Run effects
51
+
props.onLoad(~exports={Ports.facts: s, ruleStyle: None})
45
52
None // or Some(() => {})
46
53
}, [])
47
-
48
-
<div className={"axiom-set axiom-set-"->String.concat(String.make(props.imports.ruleStyle->Option.getOr(Hybrid)))}>
49
-
{ Dict.toArray(s)->Array.mapWithIndex(((n,r), i) =>
50
-
<RuleView rule={r} scope={[]} key={String.make(i)} style={props.imports.ruleStyle->Option.getOr(Hybrid)}>
51
-
{React.string(n)}
52
-
//<Name content={n} onChange={(_) => Error("BLAH!")} />
53
-
</RuleView>)
54
-
->React.array
55
-
}
54
+
55
+
<div
56
+
className={"axiom-set axiom-set-"->String.concat(
57
+
String.make(props.imports.ruleStyle->Option.getOr(Hybrid)),
58
+
)}>
59
+
{Dict.toArray(s)
60
+
->Array.mapWithIndex(((n, r), i) =>
61
+
<RuleView
62
+
rule={r}
63
+
scope={[]}
64
+
key={String.make(i)}
65
+
style={props.imports.ruleStyle->Option.getOr(Hybrid)}>
66
+
{React.string(n)}
67
+
//<Name content={n} onChange={(_) => Error("BLAH!")} />
68
+
</RuleView>
69
+
)
70
+
->React.array}
56
71
</div>
57
72
}
58
73
| Error(e) => {
59
-
React.useEffect(() => {
60
-
// Run effects
61
-
props.onLoad(~exports= {Ports.facts: Dict.make(), ruleStyle: None});
62
-
None // or Some(() => {})
63
-
}, [])
64
-
<div className="error"> {React.string(e)} </div>
74
+
React.useEffect(() => {
75
+
// Run effects
76
+
props.onLoad(~exports={Ports.facts: Dict.make(), ruleStyle: None})
77
+
None // or Some(() => {})
78
+
}, [])
79
+
<div className="error"> {React.string(e)} </div>
65
80
}
66
81
}
67
82
}
68
-
}
83
+
}
+16
-11
src/Component.res
+16
-11
src/Component.res
···
1
1
open Signatures
2
2
module type PORTS = {
3
3
type t
4
-
let combine : (t,t) => t
4
+
let combine: (t, t) => t
5
5
let empty: t
6
6
}
7
-
module Ports = (Term : TERM, Judgment : JUDGMENT with module Term := Term) => {
7
+
module Ports = (Term: TERM, Judgment: JUDGMENT with module Term := Term) => {
8
8
module Rule = Rule.Make(Term, Judgment)
9
-
type t = { facts: Dict.t<Rule.t>, ruleStyle: option<RuleView.style> }
10
-
let empty = { facts: Dict.make(), ruleStyle: None }
11
-
let combine = (p1,p2) => {
12
-
let facts = Dict.copy(p1.facts)->Dict.assign(p2.facts);
13
-
let ruleStyle = p2.ruleStyle->Option.mapOr(p1.ruleStyle, x => Some(x));
14
-
{ facts, ruleStyle }
9
+
type t = {facts: Dict.t<Rule.t>, ruleStyle: option<RuleView.style>}
10
+
let empty = {facts: Dict.make(), ruleStyle: None}
11
+
let combine = (p1, p2) => {
12
+
let facts = Dict.copy(p1.facts)->Dict.assign(p2.facts)
13
+
let ruleStyle = p2.ruleStyle->Option.mapOr(p1.ruleStyle, x => Some(x))
14
+
{facts, ruleStyle}
15
15
}
16
16
}
17
17
module type COMPONENT = {
18
-
module Ports : PORTS
19
-
type props = { content: string, imports: Ports.t, onLoad: (~exports:Ports.t, ~string:string=?) => (),onChange: (string,~exports:Ports.t) => () }
20
-
let make : props => React.element
18
+
module Ports: PORTS
19
+
type props = {
20
+
content: string,
21
+
imports: Ports.t,
22
+
onLoad: (~exports: Ports.t, ~string: string=?) => unit,
23
+
onChange: (string, ~exports: Ports.t) => unit,
24
+
}
25
+
let make: props => React.element
21
26
}
+34
-23
src/ConfigBlock.res
+34
-23
src/ConfigBlock.res
···
1
1
open Signatures
2
2
open Component
3
3
4
-
module Make = (
5
-
Term : TERM,
6
-
Judgment : JUDGMENT with module Term := Term
7
-
) => {
8
-
module Ports = Ports(Term,Judgment)
4
+
module Make = (Term: TERM, Judgment: JUDGMENT with module Term := Term) => {
5
+
module Ports = Ports(Term, Judgment)
9
6
open RuleView
10
-
type props = { content: string, imports: Ports.t, onLoad: (~exports:Ports.t) => (), onChange: (string,~exports:Ports.t) => () }
11
-
let deserialise = (str) => switch str {
12
-
| "Gentzen" => Gentzen
13
-
| "Linear" => Linear
14
-
| "Hybrid" => Hybrid
15
-
| _ => Hybrid
7
+
type props = {
8
+
content: string,
9
+
imports: Ports.t,
10
+
onLoad: (~exports: Ports.t) => unit,
11
+
onChange: (string, ~exports: Ports.t) => unit,
16
12
}
17
-
let make = (props) => {
18
-
let (style,setStyle) = React.useState (_=>deserialise(props.content))
13
+
let deserialise = str =>
14
+
switch str {
15
+
| "Gentzen" => Gentzen
16
+
| "Linear" => Linear
17
+
| "Hybrid" => Hybrid
18
+
| _ => Hybrid
19
+
}
20
+
let make = props => {
21
+
let (style, setStyle) = React.useState(_ => deserialise(props.content))
19
22
React.useEffect(() => {
20
-
props.onLoad(~exports={Ports.facts: Dict.make(), ruleStyle:Some(style)})
23
+
props.onLoad(~exports={Ports.facts: Dict.make(), ruleStyle: Some(style)})
21
24
None
22
-
},[])
23
-
let onChange= (e) => {
25
+
}, [])
26
+
let onChange = e => {
24
27
let target = JsxEvent.Form.target(e)
25
28
let value: string = target["value"]
26
29
let sty = deserialise(value)
27
30
setStyle(_ => sty)
28
-
29
-
props.onChange(value,~exports={Ports.facts: Dict.make(), ruleStyle:Some(sty)})
31
+
32
+
props.onChange(value, ~exports={Ports.facts: Dict.make(), ruleStyle: Some(sty)})
30
33
}
31
-
[Gentzen,Linear,Hybrid]->Array.map(n =>
32
-
<input type_="radio" id={"style_"->String.concat(String.make(n))} key={String.make(n)} name="style" onChange value={String.make(n)} checked={style==n}/>
33
-
)->React.array
34
-
34
+
[Gentzen, Linear, Hybrid]
35
+
->Array.map(n =>
36
+
<input
37
+
type_="radio"
38
+
id={"style_"->String.concat(String.make(n))}
39
+
key={String.make(n)}
40
+
name="style"
41
+
onChange
42
+
value={String.make(n)}
43
+
checked={style == n}
44
+
/>
45
+
)
46
+
->React.array
35
47
}
36
48
}
37
-
+34
-25
src/Editable.res
+34
-25
src/Editable.res
···
1
1
open Component
2
2
3
-
module TextArea = (Underlying : COMPONENT) => {
3
+
module TextArea = (Underlying: COMPONENT) => {
4
4
module Ports = Underlying.Ports
5
-
type props = { content: string, imports: Ports.t, onLoad: (~exports:Ports.t, ~string:string=?) => (), onChange: (string,~exports:Ports.t) => () }
6
-
let make = (props) => {
7
-
let (editing,setEditing) = React.useState (_ => false)
8
-
let (text,setText) = React.useState (_ => props.content)
9
-
let onTextChange= (ev: JsxEvent.Form.t) => {
5
+
type props = {
6
+
content: string,
7
+
imports: Ports.t,
8
+
onLoad: (~exports: Ports.t, ~string: string=?) => unit,
9
+
onChange: (string, ~exports: Ports.t) => unit,
10
+
}
11
+
let make = props => {
12
+
let (editing, setEditing) = React.useState(_ => false)
13
+
let (text, setText) = React.useState(_ => props.content)
14
+
let onTextChange = (ev: JsxEvent.Form.t) => {
10
15
let target = JsxEvent.Form.target(ev)
11
16
let value: string = target["value"]
12
17
setText(_ => value)
13
18
}
14
-
let done = (_) => {
15
-
setEditing(_=>false)
19
+
let done = _ => {
20
+
setEditing(_ => false)
16
21
}
17
22
if editing {
18
23
<div>
19
24
<textarea className="editor-textArea" value={text} onChange={onTextChange} />
20
25
<div className="editor-controls">
21
-
<span className="editor-button button-icon button-icon-blue typcn typcn-tick" onClick={done}>
22
-
</span>
26
+
<span
27
+
className="editor-button button-icon button-icon-blue typcn typcn-tick" onClick={done}
28
+
/>
23
29
</div>
24
30
</div>
25
31
} else {
26
32
<div>
27
-
<Underlying
28
-
content={text}
29
-
imports={props.imports}
30
-
onLoad={(~exports,~string=?) => {
31
-
props.onLoad(~exports,~string=string->Option.getOr(text))
32
-
}}
33
-
onChange={(string, ~exports) => {
34
-
setText(_=>string)
35
-
props.onChange(string,~exports)
36
-
}} />
37
-
<div className="editor-controls">
38
-
<span className="editor-button button-icon button-icon-blue typcn typcn-edit" onClick={_ => setEditing(_ => true)}>
39
-
</span>
40
-
</div>
33
+
<Underlying
34
+
content={text}
35
+
imports={props.imports}
36
+
onLoad={(~exports, ~string=?) => {
37
+
props.onLoad(~exports, ~string=string->Option.getOr(text))
38
+
}}
39
+
onChange={(string, ~exports) => {
40
+
setText(_ => string)
41
+
props.onChange(string, ~exports)
42
+
}}
43
+
/>
44
+
<div className="editor-controls">
45
+
<span
46
+
className="editor-button button-icon button-icon-blue typcn typcn-edit"
47
+
onClick={_ => setEditing(_ => true)}
48
+
/>
49
+
</div>
41
50
</div>
42
51
}
43
52
}
44
-
}
53
+
}
+144
-115
src/Method.res
+144
-115
src/Method.res
···
1
1
open Signatures
2
2
open Util
3
-
module Context = (Term : TERM, Judgment : JUDGMENT with module Term := Term) => {
4
-
module Rule = Rule.Make(Term,Judgment)
3
+
module Context = (Term: TERM, Judgment: JUDGMENT with module Term := Term) => {
4
+
module Rule = Rule.Make(Term, Judgment)
5
5
type rec t = {
6
-
fixes: array<Term.meta>,
6
+
fixes: array<Term.meta>,
7
7
facts: Dict.t<Rule.t>,
8
8
}
9
9
}
10
10
11
11
module type PROOF_METHOD = {
12
-
module Term : TERM
13
-
module Judgment : JUDGMENT with module Term := Term
14
-
module Rule : module type of Rule.Make(Term,Judgment)
15
-
module Context : module type of Context(Term,Judgment)
12
+
module Term: TERM
13
+
module Judgment: JUDGMENT with module Term := Term
14
+
module Rule: module type of Rule.Make(Term, Judgment)
15
+
module Context: module type of Context(Term, Judgment)
16
16
type t<'a>
17
-
let keywords : array<string>
18
-
let check : (t<'a>, Context.t, Judgment.t,
19
-
('a, Rule.t) => 'b) => result<t<'b>,string>
20
-
let uncheck : (t<'a>, 'a => 'b) => t<'b>
21
-
let parse : (string, ~keyword: string, ~scope: array<Term.meta>,~gen: Term.gen,
22
-
~subparser: (string, ~scope: array<Term.meta>, ~gen: Term.gen)
23
-
=> result<('a,string),string> )
24
-
=> result<(t<'a>,string),string>
25
-
let prettyPrint : (t<'a>,~scope: array<Term.meta>,~indentation:int=?,
26
-
~subprinter: ('a,~scope:array<Term.meta>,~indentation:int=?)
27
-
=>string)
28
-
=> string
17
+
let keywords: array<string>
18
+
let check: (t<'a>, Context.t, Judgment.t, ('a, Rule.t) => 'b) => result<t<'b>, string>
19
+
let uncheck: (t<'a>, 'a => 'b) => t<'b>
20
+
let parse: (
21
+
string,
22
+
~keyword: string,
23
+
~scope: array<Term.meta>,
24
+
~gen: Term.gen,
25
+
~subparser: (string, ~scope: array<Term.meta>, ~gen: Term.gen) => result<('a, string), string>,
26
+
) => result<(t<'a>, string), string>
27
+
let prettyPrint: (
28
+
t<'a>,
29
+
~scope: array<Term.meta>,
30
+
~indentation: int=?,
31
+
~subprinter: ('a, ~scope: array<Term.meta>, ~indentation: int=?) => string,
32
+
) => string
29
33
}
30
34
31
-
32
-
module Derivation = (
33
-
Term : TERM, Judgment : JUDGMENT with module Term := Term
34
-
) => {
35
-
module Rule = Rule.Make(Term,Judgment)
36
-
module Context = Context(Term,Judgment)
35
+
module Derivation = (Term: TERM, Judgment: JUDGMENT with module Term := Term) => {
36
+
module Rule = Rule.Make(Term, Judgment)
37
+
module Context = Context(Term, Judgment)
37
38
type t<'a> = {
38
39
ruleName: string,
39
40
instantiation: array<Term.t>,
40
-
subgoals: array<'a>
41
+
subgoals: array<'a>,
41
42
}
42
-
let uncheck = (it : t<'a>, f) => {
43
-
{ ruleName: it.ruleName,
44
-
instantiation: it.instantiation,
45
-
subgoals: it.subgoals->Array.map(f)
43
+
let uncheck = (it: t<'a>, f) => {
44
+
{
45
+
ruleName: it.ruleName,
46
+
instantiation: it.instantiation,
47
+
subgoals: it.subgoals->Array.map(f),
46
48
}
47
49
}
48
50
exception InternalParseError(string)
49
51
let keywords = ["by"]
50
-
let prettyPrint = (it : t<'a>, ~scope,~indentation=0,
51
-
~subprinter: ('a,~scope:array<Term.meta>, ~indentation:int=?)=>string) => {
52
-
let args = it.instantiation->Array.map(t => Term.prettyPrint(t,~scope));
52
+
let prettyPrint = (
53
+
it: t<'a>,
54
+
~scope,
55
+
~indentation=0,
56
+
~subprinter: ('a, ~scope: array<Term.meta>, ~indentation: int=?) => string,
57
+
) => {
58
+
let args = it.instantiation->Array.map(t => Term.prettyPrint(t, ~scope))
53
59
"by ("
54
-
->String.concat(Array.join([it.ruleName,...args]," "))
55
-
->String.concat(") {")
56
-
->String.concat(if Array.length(it.subgoals) > 0 { newline } else { "" })
57
-
->String.concat(it.subgoals
58
-
->Array.map(s => subprinter(s, ~scope,~indentation=indentation+2))
59
-
->Array.join(newline))
60
-
->String.concat("}")
60
+
->String.concat(Array.join([it.ruleName, ...args], " "))
61
+
->String.concat(") {")
62
+
->String.concat(
63
+
if Array.length(it.subgoals) > 0 {
64
+
newline
65
+
} else {
66
+
""
67
+
},
68
+
)
69
+
->String.concat(
70
+
it.subgoals
71
+
->Array.map(s => subprinter(s, ~scope, ~indentation=indentation + 2))
72
+
->Array.join(newline),
73
+
)
74
+
->String.concat("}")
61
75
}
62
76
let parse = (input, ~keyword as _, ~scope, ~gen, ~subparser) => {
63
77
let cur = ref(String.trim(input))
64
-
if (cur.contents->String.get(0) == Some("(")) {
65
-
switch Rule.parseRuleName(cur.contents->String.sliceToEnd(~start=1)) {
66
-
| Ok((ruleName,rest)) => {
78
+
if cur.contents->String.get(0) == Some("(") {
79
+
switch Rule.parseRuleName(cur.contents->String.sliceToEnd(~start=1)) {
80
+
| Ok((ruleName, rest)) => {
67
81
cur := rest
68
-
let instantiation = [];
82
+
let instantiation = []
69
83
let it = ref(Error(""))
70
-
while {it := Term.parse(cur.contents,~scope,~gen);
71
-
it.contents->Result.isOk} {
72
-
let (val, rest) = it.contents->Result.getExn
84
+
while {
85
+
it := Term.parse(cur.contents, ~scope, ~gen)
86
+
it.contents->Result.isOk
87
+
} {
88
+
let (val, rest) = it.contents->Result.getExn
73
89
Array.push(instantiation, val)
74
90
cur := String.trim(rest)
75
91
}
76
-
if (cur.contents->String.get(0) == Some(")")) {
92
+
if cur.contents->String.get(0) == Some(")") {
77
93
cur := String.trim(cur.contents->String.sliceToEnd(~start=1))
78
94
let subgoals = []
79
-
if (cur.contents->String.get(0) == Some("{")) {
95
+
if cur.contents->String.get(0) == Some("{") {
80
96
cur := String.trim(cur.contents->String.sliceToEnd(~start=1))
81
97
try {
82
-
while (cur.contents->String.get(0) != Some("}")) {
83
-
switch subparser(cur.contents,~scope,~gen) {
98
+
while cur.contents->String.get(0) != Some("}") {
99
+
switch subparser(cur.contents, ~scope, ~gen) {
84
100
| Ok((sg, rest)) => {
85
-
Array.push(subgoals,sg)
101
+
Array.push(subgoals, sg)
86
102
cur := String.trim(rest)
87
103
}
88
104
| Error(e) => raise(InternalParseError(e))
89
105
}
90
-
}
91
-
if (cur.contents->String.get(0) == Some("}")) {
106
+
}
107
+
if cur.contents->String.get(0) == Some("}") {
92
108
cur := String.trim(cur.contents->String.sliceToEnd(~start=1))
93
-
Ok(({ruleName,instantiation,subgoals},cur.contents))
109
+
Ok(({ruleName, instantiation, subgoals}, cur.contents))
94
110
} else {
95
111
Error("} or subgoal proof expected")
96
112
}
···
98
114
| InternalParseError(e) => Error(e)
99
115
}
100
116
} else {
101
-
Error("{ expected")
117
+
Error("{ expected")
102
118
}
103
119
} else {
104
120
Error(") or term expected")
···
110
126
Error("Expected (")
111
127
}
112
128
}
113
-
let check = (it: t<'a>, ctx : Context.t, j: Judgment.t, f : ('a, Rule.t) => 'b) => {
129
+
let check = (it: t<'a>, ctx: Context.t, j: Judgment.t, f: ('a, Rule.t) => 'b) => {
114
130
switch ctx.facts->Dict.get(it.ruleName) {
115
-
| None =>
116
-
Error("Cannot find rule '"->String.concat(it.ruleName)->String.concat("'") )
131
+
| None => Error("Cannot find rule '"->String.concat(it.ruleName)->String.concat("'"))
117
132
| Some(rule) if Array.length(rule.vars) == Array.length(it.instantiation) => {
118
-
let {premises,conclusion} = Rule.instantiate(rule,it.instantiation)
119
-
if Judgment.equivalent(conclusion,j) {
133
+
let {premises, conclusion} = Rule.instantiate(rule, it.instantiation)
134
+
if Judgment.equivalent(conclusion, j) {
120
135
if Array.length(it.subgoals) == Array.length(premises) {
121
136
Ok({
122
137
ruleName: it.ruleName,
123
138
instantiation: it.instantiation,
124
-
subgoals: Belt.Array.zipBy(it.subgoals,premises,f)
139
+
subgoals: Belt.Array.zipBy(it.subgoals, premises, f),
125
140
})
126
141
} else {
127
142
Error("Incorrect number of subgoals")
128
143
}
129
144
} else {
130
-
let concString = Judgment.prettyPrint(conclusion,~scope=ctx.fixes)
131
-
let goalString = Judgment.prettyPrint(j,~scope=ctx.fixes)
132
-
Error("Conclusion of rule '"
145
+
let concString = Judgment.prettyPrint(conclusion, ~scope=ctx.fixes)
146
+
let goalString = Judgment.prettyPrint(j, ~scope=ctx.fixes)
147
+
Error(
148
+
"Conclusion of rule '"
133
149
->String.concat(concString)
134
150
->String.concat("' doesn't match goal '")
135
151
->String.concat(goalString)
136
-
->String.concat("'"))
152
+
->String.concat("'"),
153
+
)
137
154
}
138
-
}
155
+
}
139
156
| _ => Error("Incorrect number of binders")
140
157
}
141
158
}
142
159
}
143
-
module Lemma = (
144
-
Term : TERM, Judgment : JUDGMENT with module Term := Term
145
-
) => {
146
-
module Rule = Rule.Make(Term,Judgment)
147
-
module Context = Context(Term,Judgment)
160
+
module Lemma = (Term: TERM, Judgment: JUDGMENT with module Term := Term) => {
161
+
module Rule = Rule.Make(Term, Judgment)
162
+
module Context = Context(Term, Judgment)
148
163
type t<'a> = {
149
164
rule: Rule.t,
150
165
proof: 'a,
151
-
show: 'a
166
+
show: 'a,
152
167
}
153
168
let uncheck = (it: t<'a>, f) => {
154
-
{ rule: it.rule,
169
+
{
170
+
rule: it.rule,
155
171
proof: f(it.proof),
156
-
show: f(it.show)
172
+
show: f(it.show),
157
173
}
158
174
}
159
175
let keywords = ["have"]
160
-
let prettyPrint = (it : t<'a>, ~scope,~indentation=0,
161
-
~subprinter: ('a,~scope:array<Term.meta>, ~indentation:int=?)=>string) => {
162
-
"have "->String.concat(Rule.prettyPrintInline(it.rule,~scope))
163
-
->String.concat(newline)
164
-
->String.concat(subprinter(it.proof,~scope,~indentation))
165
-
->String.concat(newline)
166
-
->String.concat(subprinter(it.show,~scope,~indentation))
176
+
let prettyPrint = (
177
+
it: t<'a>,
178
+
~scope,
179
+
~indentation=0,
180
+
~subprinter: ('a, ~scope: array<Term.meta>, ~indentation: int=?) => string,
181
+
) => {
182
+
"have "
183
+
->String.concat(Rule.prettyPrintInline(it.rule, ~scope))
184
+
->String.concat(newline)
185
+
->String.concat(subprinter(it.proof, ~scope, ~indentation))
186
+
->String.concat(newline)
187
+
->String.concat(subprinter(it.show, ~scope, ~indentation))
167
188
}
168
189
let parse = (input, ~keyword as _, ~scope, ~gen, ~subparser) => {
169
190
//todo add toplevel
170
191
switch Rule.parseInner(input, ~scope, ~gen) {
171
-
| Ok((rule,rest)) => {
172
-
switch (subparser(rest,~scope,~gen)) {
173
-
| Ok((proof,rest')) =>
174
-
switch String.trim(rest')->subparser(~scope,~gen) {
175
-
| Ok((show,rest'')) => Ok({rule,proof,show}, rest'')
176
-
| Error(e) => Error(e)
177
-
}
192
+
| Ok((rule, rest)) => switch subparser(rest, ~scope, ~gen) {
193
+
| Ok((proof, rest')) =>
194
+
switch String.trim(rest')->subparser(~scope, ~gen) {
195
+
| Ok((show, rest'')) => Ok({rule, proof, show}, rest'')
178
196
| Error(e) => Error(e)
179
197
}
198
+
| Error(e) => Error(e)
180
199
}
181
200
| Error(e) => Error(e)
182
201
}
183
202
}
184
-
let check = (it: t<'a>, _ctx : Context.t, j: Judgment.t, f : ('a, Rule.t) => 'b) => {
185
-
let first = f(it.proof,it.rule)
186
-
let second = f(it.show,{vars:[],premises:[it.rule],conclusion:j})
187
-
Ok({rule:it.rule, proof:first, show:second})
203
+
let check = (it: t<'a>, _ctx: Context.t, j: Judgment.t, f: ('a, Rule.t) => 'b) => {
204
+
let first = f(it.proof, it.rule)
205
+
let second = f(it.show, {vars: [], premises: [it.rule], conclusion: j})
206
+
Ok({rule: it.rule, proof: first, show: second})
188
207
}
189
208
}
190
209
module Combine = (
191
-
Term : TERM, Judgment : JUDGMENT with module Term := Term,
192
-
Method1 : PROOF_METHOD with module Term := Term and module Judgment := Judgment,
193
-
Method2 : PROOF_METHOD with module Term := Term and module Judgment := Judgment
210
+
Term: TERM,
211
+
Judgment: JUDGMENT with module Term := Term,
212
+
Method1: PROOF_METHOD with module Term := Term and module Judgment := Judgment,
213
+
Method2: PROOF_METHOD with module Term := Term and module Judgment := Judgment,
194
214
) => {
195
-
module Rule = Rule.Make(Term,Judgment)
196
-
module Context = Context(Term,Judgment)
215
+
module Rule = Rule.Make(Term, Judgment)
216
+
module Context = Context(Term, Judgment)
197
217
type t<'a> = First(Method1.t<'a>) | Second(Method2.t<'a>)
198
-
let uncheck = (it, f) => switch it {
199
-
| First(m) => First(Method1.uncheck(m,f))
200
-
| Second(m) => Second(Method2.uncheck(m,f))
201
-
}
202
-
let keywords = Array.concat(Method1.keywords,Method2.keywords)
203
-
204
-
let check = (it,ctx, j, f) => switch it {
205
-
| First(m) => m->Method1.check(ctx,j,f)->Result.map(x => First(x))
206
-
| Second(m) => m->Method2.check(ctx,j,f)->Result.map(x => Second(x))
207
-
}
208
-
let prettyPrint = (it : t<'a>, ~scope, ~indentation=0,~subprinter) => switch it {
209
-
| First(m) => m->Method1.prettyPrint(~scope,~indentation,~subprinter)
210
-
| Second(m) => m->Method2.prettyPrint(~scope,~indentation,~subprinter)
211
-
}
218
+
let uncheck = (it, f) =>
219
+
switch it {
220
+
| First(m) => First(Method1.uncheck(m, f))
221
+
| Second(m) => Second(Method2.uncheck(m, f))
222
+
}
223
+
let keywords = Array.concat(Method1.keywords, Method2.keywords)
224
+
225
+
let check = (it, ctx, j, f) =>
226
+
switch it {
227
+
| First(m) => m->Method1.check(ctx, j, f)->Result.map(x => First(x))
228
+
| Second(m) => m->Method2.check(ctx, j, f)->Result.map(x => Second(x))
229
+
}
230
+
let prettyPrint = (it: t<'a>, ~scope, ~indentation=0, ~subprinter) =>
231
+
switch it {
232
+
| First(m) => m->Method1.prettyPrint(~scope, ~indentation, ~subprinter)
233
+
| Second(m) => m->Method2.prettyPrint(~scope, ~indentation, ~subprinter)
234
+
}
212
235
let parse = (input, ~keyword, ~scope, ~gen, ~subparser) => {
213
236
if Method1.keywords->Array.indexOf(keyword) > -1 {
214
-
Method1.parse(input,~keyword,~scope,~gen,~subparser)->Result.map(((x,r)) => (First(x),r))
237
+
Method1.parse(input, ~keyword, ~scope, ~gen, ~subparser)->Result.map(((x, r)) => (
238
+
First(x),
239
+
r,
240
+
))
215
241
} else {
216
-
Method2.parse(input,~keyword,~scope,~gen,~subparser)->Result.map(((x,r)) => (Second(x),r))
242
+
Method2.parse(input, ~keyword, ~scope, ~gen, ~subparser)->Result.map(((x, r)) => (
243
+
Second(x),
244
+
r,
245
+
))
217
246
}
218
247
}
219
-
}
248
+
}
+53
-42
src/MethodView.res
+53
-42
src/MethodView.res
···
2
2
open Signatures
3
3
open Method
4
4
module type METHOD_VIEW = {
5
-
module Term : TERM
6
-
module Judgment : JUDGMENT with module Term := Term
7
-
module Method : PROOF_METHOD with
8
-
module Term := Term and
9
-
module Judgment := Judgment
10
-
type props<'a> = {method: Method.t<'a>, scope: array<Term.meta>, ruleStyle: RuleView.style}
5
+
module Term: TERM
6
+
module Judgment: JUDGMENT with module Term := Term
7
+
module Method: PROOF_METHOD with module Term := Term and module Judgment := Judgment
8
+
type props<'a> = {method: Method.t<'a>, scope: array<Term.meta>, ruleStyle: RuleView.style}
11
9
type srProps<'a> = {"proof": 'a, "scope": array<Term.meta>, "ruleStyle": RuleView.style}
12
-
let make : (srProps<'a> => React.element) => props<'a> => React.element
10
+
let make: (srProps<'a> => React.element) => props<'a> => React.element
13
11
}
14
12
15
-
module DerivationView = (
16
-
Term : TERM, Judgment : JUDGMENT with module Term := Term
17
-
) => {
13
+
module DerivationView = (Term: TERM, Judgment: JUDGMENT with module Term := Term) => {
18
14
module Method = Derivation(Term, Judgment)
19
-
type props<'a> = {method: Method.t<'a>, scope: array<Term.meta>, ruleStyle: RuleView.style}
15
+
type props<'a> = {method: Method.t<'a>, scope: array<Term.meta>, ruleStyle: RuleView.style}
20
16
type srProps<'a> = {"proof": 'a, "scope": array<Term.meta>, "ruleStyle": RuleView.style}
21
-
let make = (subRender : srProps<'a> => React.element) => (props) => {
22
-
<div>
23
-
<b>{React.string("by ")}</b>
17
+
let make = (subRender: srProps<'a> => React.element) => props => {
18
+
<div>
19
+
<b> {React.string("by ")} </b>
24
20
{React.string(props.method.ruleName)}
25
21
<ul>
26
-
{ props.method.subgoals->Array.mapWithIndex((sg,i) => {
22
+
{props.method.subgoals
23
+
->Array.mapWithIndex((sg, i) => {
27
24
<li key={String.make(i)}>
28
-
{React.createElement(subRender, {"proof":sg, "scope": props.scope, "ruleStyle": props.ruleStyle})}
25
+
{React.createElement(
26
+
subRender,
27
+
{"proof": sg, "scope": props.scope, "ruleStyle": props.ruleStyle},
28
+
)}
29
29
</li>
30
-
})->React.array
31
-
}
30
+
})
31
+
->React.array}
32
32
</ul>
33
-
</div>
33
+
</div>
34
34
}
35
35
}
36
36
37
37
module LemmaView = (
38
-
Term : TERM, Judgment : JUDGMENT with module Term := Term,
39
-
JudgmentView : JUDGMENT_VIEW with module Term := Term and module Judgment := Judgment
38
+
Term: TERM,
39
+
Judgment: JUDGMENT with module Term := Term,
40
+
JudgmentView: JUDGMENT_VIEW with module Term := Term and module Judgment := Judgment,
40
41
) => {
41
42
module Method = Lemma(Term, Judgment)
42
-
type props<'a> = {method: Method.t<'a>, scope: array<Term.meta>, ruleStyle: RuleView.style}
43
+
type props<'a> = {method: Method.t<'a>, scope: array<Term.meta>, ruleStyle: RuleView.style}
43
44
type srProps<'a> = {"proof": 'a, "scope": array<Term.meta>, "ruleStyle": RuleView.style}
44
-
module RuleView = RuleView.Make(Term,Judgment, JudgmentView)
45
-
let make = (subRender : srProps<'a> => React.element) => (props) => {
46
-
<div>
47
-
<b>{React.string("have ")}</b>
48
-
<RuleView
49
-
rule={props.method.rule}
50
-
scope={props.scope}
51
-
style={props.ruleStyle}> {React.null}
45
+
module RuleView = RuleView.Make(Term, Judgment, JudgmentView)
46
+
let make = (subRender: srProps<'a> => React.element) => props => {
47
+
<div>
48
+
<b> {React.string("have ")} </b>
49
+
<RuleView rule={props.method.rule} scope={props.scope} style={props.ruleStyle}>
50
+
{React.null}
52
51
</RuleView>
53
-
{React.createElement(subRender,{"proof":props.method.proof, "scope": props.scope, "ruleStyle": props.ruleStyle})}
54
-
{React.createElement(subRender,{"proof":props.method.show, "scope": props.scope, "ruleStyle": props.ruleStyle})}
55
-
</div>
52
+
{React.createElement(
53
+
subRender,
54
+
{"proof": props.method.proof, "scope": props.scope, "ruleStyle": props.ruleStyle},
55
+
)}
56
+
{React.createElement(
57
+
subRender,
58
+
{"proof": props.method.show, "scope": props.scope, "ruleStyle": props.ruleStyle},
59
+
)}
60
+
</div>
56
61
}
57
62
}
58
63
module CombineMethodView = (
59
-
Term : TERM, Judgment : JUDGMENT with module Term := Term,
60
-
Method1View : METHOD_VIEW with module Term := Term and module Judgment := Judgment,
61
-
Method2View : METHOD_VIEW with module Term := Term and module Judgment := Judgment and type srProps<'a> = Method1View.srProps<'a>
64
+
Term: TERM,
65
+
Judgment: JUDGMENT with module Term := Term,
66
+
Method1View: METHOD_VIEW with module Term := Term and module Judgment := Judgment,
67
+
Method2View: METHOD_VIEW
68
+
with module Term := Term
69
+
and module Judgment := Judgment
70
+
and type srProps<'a> = Method1View.srProps<'a>,
62
71
) => {
63
-
module Method = Combine(Term,Judgment,Method1View.Method, Method2View.Method)
64
-
type props<'a> = {method: Method.t<'a>, scope: array<Term.meta>, ruleStyle: RuleView.style}
72
+
module Method = Combine(Term, Judgment, Method1View.Method, Method2View.Method)
73
+
type props<'a> = {method: Method.t<'a>, scope: array<Term.meta>, ruleStyle: RuleView.style}
65
74
type srProps<'a> = Method1View.srProps<'a>
66
-
let make = (subrender : srProps<'a> => React.element) => (props) => {
75
+
let make = (subrender: srProps<'a> => React.element) => props => {
67
76
switch props.method {
68
-
| First(m) => Method1View.make(subrender)({method:m, scope:props.scope, ruleStyle: props.ruleStyle})
69
-
| Second(m) => Method2View.make(subrender)({method:m, scope:props.scope, ruleStyle: props.ruleStyle})
77
+
| First(m) =>
78
+
Method1View.make(subrender)({method: m, scope: props.scope, ruleStyle: props.ruleStyle})
79
+
| Second(m) =>
80
+
Method2View.make(subrender)({method: m, scope: props.scope, ruleStyle: props.ruleStyle})
70
81
}
71
82
}
72
-
}
83
+
}
+95
-75
src/Proof.res
+95
-75
src/Proof.res
···
2
2
open Signatures
3
3
4
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)
5
+
Term: TERM,
6
+
Judgment: JUDGMENT with module Term := Term,
7
+
Method: PROOF_METHOD with module Term := Term and module Judgment := Judgment,
8
+
) => {
9
+
module Rule = Rule.Make(Term, Judgment)
10
+
module Context = Context(Term, Judgment)
10
11
type rec t = {
11
-
fixes: array<Term.meta>,
12
+
fixes: array<Term.meta>,
12
13
assumptions: array<string>,
13
-
method: option<Method.t<t>>
14
-
}
15
-
type rec checked
16
-
= Checked({
17
-
fixes: array<Term.meta>,
14
+
method: option<Method.t<t>>,
15
+
}
16
+
type rec checked =
17
+
| Checked({
18
+
fixes: array<Term.meta>,
18
19
assumptions: array<string>,
19
20
method: option<Method.t<checked>>,
20
-
rule: Rule.t
21
+
rule: Rule.t,
21
22
})
22
-
| ProofError({ raw: t, rule: Rule.t, msg: string})
23
-
let parseKeyword = (input) => {
23
+
| ProofError({raw: t, rule: Rule.t, msg: string})
24
+
let parseKeyword = input => {
24
25
Method.keywords
25
-
->Array.concat(["?"])
26
-
->Array.find(kw => String.trim(input)->String.startsWith(kw))
26
+
->Array.concat(["?"])
27
+
->Array.find(kw => String.trim(input)->String.startsWith(kw))
27
28
}
28
-
let rec prettyPrint = (prf : t, ~scope, ~indentation=0) => {
29
+
let rec prettyPrint = (prf: t, ~scope, ~indentation=0) => {
29
30
let mtd = switch prf.method {
30
31
| None => "?"
31
-
| Some(m) => Method.prettyPrint(m,
32
+
| Some(m) =>
33
+
Method.prettyPrint(
34
+
m,
32
35
~scope=prf.fixes->Array.concat(scope),
33
-
~indentation=indentation+2,
34
-
~subprinter=prettyPrint)
36
+
~indentation=indentation + 2,
37
+
~subprinter=prettyPrint,
38
+
)
35
39
}
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)
40
+
String.padStart("", indentation, " ")
41
+
->String.concat(prf.fixes->Array.map(Term.prettyPrintMeta)->Array.join(""))
42
+
->String.concat(
43
+
prf.assumptions
44
+
->Array.map(s => String.concat(" ", s))
45
+
->Array.join(""),
46
+
)
47
+
->String.concat(
48
+
if Array.length(prf.assumptions) == 0 {
49
+
"|- "
50
+
} else {
51
+
" |- "
52
+
},
53
+
)
54
+
->String.concat(mtd)
47
55
}
48
-
let rec parse = (input, ~scope,~gen) => {
56
+
let rec parse = (input, ~scope, ~gen) => {
49
57
let it = ref(Error(""))
50
58
let cur = ref(String.trim(input))
51
59
let fixes = []
52
-
while {it := Term.parseMeta(cur.contents); it.contents->Result.isOk} {
53
-
let (n,r) = Result.getExn(it.contents)
60
+
while {
61
+
it := Term.parseMeta(cur.contents)
62
+
it.contents->Result.isOk
63
+
} {
64
+
let (n, r) = Result.getExn(it.contents)
54
65
cur := String.trim(r)
55
66
fixes->Array.unshift(n)
56
67
}
57
68
let it = ref(Error(""))
58
69
let assumptions = []
59
-
while {it := Rule.parseRuleName(cur.contents); it.contents->Result.isOk} {
60
-
let (a,r) = Result.getExn(it.contents)
70
+
while {
71
+
it := Rule.parseRuleName(cur.contents)
72
+
it.contents->Result.isOk
73
+
} {
74
+
let (a, r) = Result.getExn(it.contents)
61
75
cur := String.trim(r)
62
76
assumptions->Array.push(a)
63
77
}
64
-
if cur.contents->String.slice(~start=0,~end=2) != "|-" {
65
-
Console.log((fixes,assumptions))
78
+
if cur.contents->String.slice(~start=0, ~end=2) != "|-" {
79
+
Console.log((fixes, assumptions))
66
80
Error("expected turnstile or rule name"->String.concat(cur.contents))
67
81
} else {
68
82
cur := cur.contents->String.trim->String.sliceToEnd(~start=2)->String.trim
69
83
let scope' = Array.concat(fixes, scope)
70
84
switch parseKeyword(cur.contents) {
71
-
| Some("?") => {
72
-
Ok(({fixes,assumptions,method:None},
73
-
cur.contents->String.sliceToEnd(~start=1)))
74
-
}
85
+
| Some("?") => Ok((
86
+
{fixes, assumptions, method: None},
87
+
cur.contents->String.sliceToEnd(~start=1),
88
+
))
75
89
| Some(keyword) => {
76
90
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))
91
+
switch Method.parse(cur.contents, ~keyword, ~scope=scope', ~gen, ~subparser=parse) {
92
+
| Ok((method, r)) => Ok(({fixes, assumptions, method: Some(method)}, r))
80
93
| Error(e) => Error(e)
81
94
}
82
95
}
···
84
97
}
85
98
}
86
99
}
87
-
let enter = (ctx : Context.t, prf: t, rule: Rule.t) => {
100
+
let enter = (ctx: Context.t, prf: t, rule: Rule.t) => {
88
101
if Array.length(prf.fixes) == Array.length(rule.vars) {
89
102
if Array.length(prf.assumptions) == Array.length(rule.premises) {
90
-
let newFacts = Dict.fromArray(Belt.Array.zip(prf.assumptions,rule.premises))
91
-
Ok({
103
+
let newFacts = Dict.fromArray(Belt.Array.zip(prf.assumptions, rule.premises))
104
+
Ok({
92
105
Context.fixes: rule.vars->Array.concat(ctx.fixes),
93
-
facts: Dict.copy(ctx.facts)->Dict.assign(newFacts)
106
+
facts: Dict.copy(ctx.facts)->Dict.assign(newFacts),
94
107
})
95
108
} else {
96
109
Error("Proof introduces a different number of assumptions than the rule")
···
98
111
} else {
99
112
Error("Proof introduces a different number of variables than the rule")
100
113
}
101
-
102
114
} //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))
115
+
116
+
let rec uncheck = (prf: checked) =>
117
+
switch prf {
118
+
| ProofError({raw, rule: _, msg: _}) => raw
119
+
| Checked({fixes, assumptions, method, rule: _}) => {
120
+
fixes,
121
+
assumptions,
122
+
method: method->Option.map(xs => xs->Method.uncheck(uncheck)),
123
+
}
109
124
}
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 {
125
+
let rec check = (ctx: Context.t, prf: t, rule: Rule.t) => {
126
+
let ruleStr = Rule.prettyPrintInline(rule, ~scope=[])
127
+
Console.log(("CHECK", ctx, prf, ruleStr))
128
+
switch enter(ctx, prf, rule) {
129
+
| Ok(ctx') =>
130
+
switch prf.method {
116
131
| 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')
132
+
switch m->Method.check(ctx', rule.conclusion, (s, r) => check(ctx', s, r)) {
133
+
| Ok(m') =>
134
+
Checked({
135
+
rule,
136
+
fixes: prf.fixes,
137
+
assumptions: prf.assumptions,
138
+
method: Some(m'),
122
139
})
123
-
| Error(e) => ProofError({raw:prf, rule, msg:e})
140
+
| Error(e) => ProofError({raw: prf, rule, msg: e})
124
141
}
125
-
| None => Checked({
126
-
rule, fixes: prf.fixes, assumptions: prf.assumptions, method: None
142
+
| None =>
143
+
Checked({
144
+
rule,
145
+
fixes: prf.fixes,
146
+
assumptions: prf.assumptions,
147
+
method: None,
127
148
})
128
149
}
129
-
| Error(e) => ProofError({raw:prf, rule, msg: e})
150
+
| Error(e) => ProofError({raw: prf, rule, msg: e})
130
151
}
131
-
}// result<checked,string>
132
-
152
+
} // result<checked,string>
133
153
}
134
154
135
-
/*
155
+
/*
136
156
137
157
138
158
139
-
*/
159
+
*/
+32
-36
src/ProofView.res
+32
-36
src/ProofView.res
···
3
3
open MethodView
4
4
5
5
module Make = (
6
-
Term : TERM, Judgment : JUDGMENT with module Term := Term,
7
-
JudgmentView : JUDGMENT_VIEW with module Term := Term and module Judgment := Judgment,
8
-
MethodView : METHOD_VIEW with module Term := Term and module Judgment := Judgment
9
-
) => {
10
-
module Rule = Rule.Make(Term, Judgment)
6
+
Term: TERM,
7
+
Judgment: JUDGMENT with module Term := Term,
8
+
JudgmentView: JUDGMENT_VIEW with module Term := Term and module Judgment := Judgment,
9
+
MethodView: METHOD_VIEW with module Term := Term and module Judgment := Judgment,
10
+
) => {
11
+
module Rule = Rule.Make(Term, Judgment)
11
12
module ScopeView = ScopeView.Make(Term, JudgmentView.TermView)
12
13
module Proof = Proof.Make(Term, Judgment, MethodView.Method)
13
-
14
+
14
15
type props = {
15
-
proof: Proof.checked,
16
-
scope: array<Term.meta>,
17
-
ruleStyle: RuleView.style
16
+
proof: Proof.checked,
17
+
scope: array<Term.meta>,
18
+
ruleStyle: RuleView.style,
18
19
}
19
20
module RuleView = RuleView.Make(Term, Judgment, JudgmentView)
20
21
@react.componentWithProps
21
-
let rec make = (props : props) => {
22
+
let rec make = (props: props) => {
22
23
switch props.proof {
23
24
| Proof.Checked({fixes, assumptions, method, rule}) => {
24
-
let scope = Array.concat(fixes,props.scope)
25
+
let scope = Array.concat(fixes, props.scope)
25
26
<>
26
-
<ScopeView scope=fixes />
27
-
<ul className="proof-assumptions">
28
-
{ Belt.Array.zipBy(assumptions,rule.premises, (n,r) => {
27
+
<ScopeView scope=fixes />
28
+
<ul className="proof-assumptions">
29
+
{Belt.Array.zipBy(assumptions, rule.premises, (n, r) => {
29
30
<li key={n}>
30
-
<RuleView rule=r style=props.ruleStyle scope>
31
-
{React.string(n)}
32
-
</RuleView>
31
+
<RuleView rule=r style=props.ruleStyle scope> {React.string(n)} </RuleView>
33
32
</li>
34
-
})->React.array
35
-
}
36
-
</ul>
37
-
<div className="proof-show">
38
-
<JudgmentView judgment={rule.conclusion} scope />
39
-
{
40
-
switch method {
33
+
})->React.array}
34
+
</ul>
35
+
<div className="proof-show">
36
+
<JudgmentView judgment={rule.conclusion} scope />
37
+
{switch method {
41
38
| None => React.null
42
-
| Some(method) => React.createElement(
43
-
MethodView.make(p => make({proof: p["proof"], scope: p["scope"], ruleStyle:p["ruleStyle"] })),
44
-
{method, scope, ruleStyle: props.ruleStyle})
45
-
}
46
-
}
47
-
</div>
39
+
| Some(method) =>
40
+
React.createElement(
41
+
MethodView.make(p =>
42
+
make({proof: p["proof"], scope: p["scope"], ruleStyle: p["ruleStyle"]})
43
+
),
44
+
{method, scope, ruleStyle: props.ruleStyle},
45
+
)
46
+
}}
47
+
</div>
48
48
</>
49
49
}
50
-
| Proof.ProofError({raw:_, rule:_, msg}) => {
51
-
<div className="error">{React.string(msg)}</div>
52
-
}
53
-
50
+
| Proof.ProofError({raw: _, rule: _, msg}) => <div className="error"> {React.string(msg)} </div>
54
51
}
55
52
}
56
-
57
-
}
53
+
}
+108
-88
src/Rule.res
+108
-88
src/Rule.res
···
3
3
// level..
4
4
let ruleNamePattern = "^[^|()\\s\\-—][^()\\s]*"
5
5
let vinculumRES = "^\s*\\n\\s*[-—][-—][\\-—]+[ \t]*([^()|\\s\\-—][^()\\s]*)?"
6
-
module Make = (Term : TERM, Judgment : JUDGMENT with module Term := Term) => {
6
+
module Make = (Term: TERM, Judgment: JUDGMENT with module Term := Term) => {
7
7
type rec t = {vars: array<Term.meta>, premises: array<t>, conclusion: Judgment.t}
8
8
let rec substitute = (rule: t, subst: Term.subst) => {
9
-
let subst' = subst->Util.mapMapValues(v => v->Term.upshift(Array.length(rule.vars)));
10
-
{
11
-
vars: rule.vars,
9
+
let subst' = subst->Util.mapMapValues(v => v->Term.upshift(Array.length(rule.vars)))
10
+
{
11
+
vars: rule.vars,
12
12
premises: rule.premises->Array.map(premise => premise->substitute(subst')),
13
-
conclusion: rule.conclusion->Judgment.substitute(subst')
13
+
conclusion: rule.conclusion->Judgment.substitute(subst'),
14
14
}
15
15
}
16
-
let rec substDeBruijn = (rule: t, substs: array<Term.t>, ~from:int=0) => {
16
+
let rec substDeBruijn = (rule: t, substs: array<Term.t>, ~from: int=0) => {
17
17
let len = Array.length(rule.vars)
18
-
let substs' = substs->Array.map(v => v->Term.upshift(len,~from=from))
18
+
let substs' = substs->Array.map(v => v->Term.upshift(len, ~from))
19
19
{
20
20
vars: rule.vars,
21
-
premises: rule.premises
22
-
->Array.map(premise => premise->substDeBruijn(substs', ~from=from+len)),
23
-
conclusion: rule.conclusion
24
-
->Judgment.substDeBruijn(substs',~from=from+len),
21
+
premises: rule.premises->Array.map(premise =>
22
+
premise->substDeBruijn(substs', ~from=from + len)
23
+
),
24
+
conclusion: rule.conclusion->Judgment.substDeBruijn(substs', ~from=from + len),
25
25
}
26
26
}
27
-
let rec upshift = (rule: t, amount: int, ~from:int=0) => {
27
+
let rec upshift = (rule: t, amount: int, ~from: int=0) => {
28
28
let len = Array.length(rule.vars)
29
29
{
30
30
vars: rule.vars,
31
-
premises: rule.premises->Array.map(r => r->upshift(amount, ~from = from + len)),
32
-
conclusion: rule.conclusion->Judgment.upshift(amount, ~from = from + len)
31
+
premises: rule.premises->Array.map(r => r->upshift(amount, ~from=from + len)),
32
+
conclusion: rule.conclusion->Judgment.upshift(amount, ~from=from + len),
33
33
}
34
34
}
35
-
type bare = { premises: array<t>, conclusion: Judgment.t }
35
+
type bare = {premises: array<t>, conclusion: Judgment.t}
36
36
let instantiate = (rule: t, terms: array<Term.t>) => {
37
37
assert(Array.length(terms) == Array.length(rule.vars))
38
38
let terms' = [...terms]
39
39
Array.reverse(terms')
40
40
{
41
-
premises: rule.premises->Array.map(r => r-> substDeBruijn(terms')),
42
-
conclusion: rule.conclusion->Judgment.substDeBruijn(terms')
41
+
premises: rule.premises->Array.map(r => r->substDeBruijn(terms')),
42
+
conclusion: rule.conclusion->Judgment.substDeBruijn(terms'),
43
43
}
44
44
}
45
-
let parseRuleName = (str) => {
46
-
let re = RegExp.fromStringWithFlags(ruleNamePattern,~flags="y")
45
+
let parseRuleName = str => {
46
+
let re = RegExp.fromStringWithFlags(ruleNamePattern, ~flags="y")
47
47
switch re->RegExp.exec(String.trim(str)) {
48
48
| None => Error("expected rule name")
49
-
| Some(res) => { switch res[0] {
50
-
| Some(Some(n)) if String.trim(n) != ""
51
-
=> Ok(n,String.sliceToEnd(String.trim(str),~start=RegExp.lastIndex(re)))
49
+
| Some(res) => switch res[0] {
50
+
| Some(Some(n)) if String.trim(n) != "" =>
51
+
Ok(n, String.sliceToEnd(String.trim(str), ~start=RegExp.lastIndex(re)))
52
52
| _ => Error("expected rule name")
53
-
}}
53
+
}
54
54
}
55
55
}
56
-
let parseVinculum = (str) => {
57
-
let re = RegExp.fromStringWithFlags(vinculumRES,~flags="y")
56
+
let parseVinculum = str => {
57
+
let re = RegExp.fromStringWithFlags(vinculumRES, ~flags="y")
58
58
switch re->RegExp.exec(str) {
59
59
| None => Error("expected vinculum")
60
-
| Some(res) => { switch res[1] {
61
-
| Some(Some(n)) if String.trim(n) != ""
62
-
=> Ok(n,String.sliceToEnd(str,~start=RegExp.lastIndex(re)))
63
-
| _ => Ok("", String.sliceToEnd(str,~start=RegExp.lastIndex(re)))
64
-
}}
60
+
| Some(res) => switch res[1] {
61
+
| Some(Some(n)) if String.trim(n) != "" =>
62
+
Ok(n, String.sliceToEnd(str, ~start=RegExp.lastIndex(re)))
63
+
| _ => Ok("", String.sliceToEnd(str, ~start=RegExp.lastIndex(re)))
64
+
}
65
65
}
66
66
}
67
67
exception InternalParseError(string)
68
68
let rec parseInner = (string, ~scope=[]: array<Term.meta>, ~gen=?) => {
69
-
if (string->String.trim->String.get(0) == Some("[")) {
70
-
let cur = ref(String.make(string->String.trim->String.sliceToEnd(~start=1)));
69
+
if string->String.trim->String.get(0) == Some("[") {
70
+
let cur = ref(String.make(string->String.trim->String.sliceToEnd(~start=1)))
71
71
let it = ref(Error(""))
72
72
let vars = []
73
-
while {it := Term.parseMeta(cur.contents); it.contents->Result.isOk} {
74
-
let (str,rest) = Result.getExn(it.contents)
75
-
Array.unshift(vars,str)
73
+
while {
74
+
it := Term.parseMeta(cur.contents)
75
+
it.contents->Result.isOk
76
+
} {
77
+
let (str, rest) = Result.getExn(it.contents)
78
+
Array.unshift(vars, str)
76
79
cur := rest
77
80
}
78
81
let premises = []
79
-
switch {
80
-
while (cur.contents->String.trim->String.slice(~start=0,~end=2) != "|-"
81
-
&& cur.contents->String.trim->String.get(0) != Some("]")) {
82
-
switch parseInner(cur.contents,~scope=vars->Array.concat(scope), ~gen=?gen) {
83
-
| Ok(p,rest) => {
82
+
switch {
83
+
while (
84
+
cur.contents->String.trim->String.slice(~start=0, ~end=2) != "|-" &&
85
+
cur.contents->String.trim->String.get(0) != Some("]")
86
+
) {
87
+
switch parseInner(cur.contents, ~scope=vars->Array.concat(scope), ~gen?) {
88
+
| Ok(p, rest) => {
84
89
cur := rest
85
90
premises->Array.push(p)
86
91
}
87
92
| Error(_) => raise(InternalParseError("expected turnstile or premise"))
88
93
}
89
94
}
90
-
if (cur.contents->String.trim->String.get(0) == Some("]")) {
95
+
if cur.contents->String.trim->String.get(0) == Some("]") {
91
96
let rest = cur.contents->String.trim->String.sliceToEnd(~start=1)
92
97
cur := rest
93
98
switch premises {
94
-
| [{vars:[],premises:[],conclusion:e}] => Ok(({vars,premises:[],conclusion:e}, rest))
99
+
| [{vars: [], premises: [], conclusion: e}] =>
100
+
Ok(({vars, premises: [], conclusion: e}, rest))
95
101
| _ => Error("Conclusion appears to be multiple terms")
96
102
}
97
103
} else {
98
104
cur := cur.contents->String.trim->String.sliceToEnd(~start=2)
99
-
switch Judgment.parse(cur.contents,~scope=vars->Array.concat(scope),~gen=?gen) {
105
+
switch Judgment.parse(cur.contents, ~scope=vars->Array.concat(scope), ~gen?) {
100
106
| Ok(conclusion, rest) =>
101
-
if (rest->String.trim->String.get(0) == Some("]")) {
102
-
cur := rest->String.trim->String.sliceToEnd(~start=1);
107
+
if rest->String.trim->String.get(0) == Some("]") {
108
+
cur := rest->String.trim->String.sliceToEnd(~start=1)
103
109
Ok(({vars, premises, conclusion}, cur.contents))
104
110
} else {
105
111
Error("Expected closing bracket")
···
111
117
| exception InternalParseError(e) => Error(e)
112
118
| v => v
113
119
}
114
-
} else {
115
-
switch Judgment.parse(string,~scope,~gen=?gen) {
116
-
| Ok(conclusion, rest) => Ok(({vars:[], premises:[], conclusion}, rest))
120
+
} else {
121
+
switch Judgment.parse(string, ~scope, ~gen?) {
122
+
| Ok(conclusion, rest) => Ok(({vars: [], premises: [], conclusion}, rest))
117
123
| Error(e) => Error(e)
118
124
}
119
125
}
120
126
}
121
127
let parseTopLevel = (string, ~gen=?, ~scope=[]) => {
122
-
let cur = ref(String.make(string));
128
+
let cur = ref(String.make(string))
123
129
let it = ref(Error(""))
124
130
let vars = []
125
131
switch {
126
-
while {it := Term.parseMeta(cur.contents); it.contents->Result.isOk} {
127
-
let (str,rest) = Result.getExn(it.contents)
128
-
Array.unshift(vars,str)
132
+
while {
133
+
it := Term.parseMeta(cur.contents)
134
+
it.contents->Result.isOk
135
+
} {
136
+
let (str, rest) = Result.getExn(it.contents)
137
+
Array.unshift(vars, str)
129
138
cur := rest
130
139
}
131
140
let it = ref(Error(""))
132
141
let premises = []
133
-
while {it := parseVinculum(cur.contents); it.contents->Result.isError} {
134
-
switch parseInner(cur.contents,~scope=vars->Array.concat(scope), ~gen=?gen) {
135
-
| Ok(p,rest) => {
142
+
while {
143
+
it := parseVinculum(cur.contents)
144
+
it.contents->Result.isError
145
+
} {
146
+
switch parseInner(cur.contents, ~scope=vars->Array.concat(scope), ~gen?) {
147
+
| Ok(p, rest) => {
136
148
cur := rest
137
149
premises->Array.push(p)
138
150
}
139
151
| Error(e) => raise(InternalParseError(e))
140
152
}
141
153
}
142
-
let (ruleName,rest) = it.contents->Result.getExn
154
+
let (ruleName, rest) = it.contents->Result.getExn
143
155
cur := rest
144
-
switch Judgment.parse(cur.contents,~scope=vars->Array.concat(scope),~gen=?gen) {
156
+
switch Judgment.parse(cur.contents, ~scope=vars->Array.concat(scope), ~gen?) {
145
157
| Ok(conclusion, rest) => Ok((({vars, premises, conclusion}, ruleName), rest))
146
158
| Error(e) => Error(e)
147
159
}
···
150
162
| v => v
151
163
}
152
164
}
153
-
154
-
let rec prettyPrintInline = (rule: t,~scope=[]:array<Term.meta>) => {
165
+
166
+
let rec prettyPrintInline = (rule: t, ~scope=[]: array<Term.meta>) => {
155
167
switch rule {
156
-
| {vars: [], premises: [], conclusion: c} => Judgment.prettyPrint(c,~scope)
168
+
| {vars: [], premises: [], conclusion: c} => Judgment.prettyPrint(c, ~scope)
157
169
| _ => {
158
-
let vars' = Array.copy(rule.vars)
159
-
Array.reverse(vars')
160
-
"["->String.concat(vars'
161
-
->Array.map(Term.prettyPrintMeta)
162
-
->Array.join("")
163
-
->String.concat(" ")
164
-
->String.concat(if Array.length(rule.premises) == 0 {
165
-
Judgment.prettyPrint(rule.conclusion,~scope=[...rule.vars,...scope])
166
-
} else {
167
-
rule.premises
168
-
->Array.map(r => prettyPrintInline(r,~scope=[...rule.vars,...scope]))->Array.join(" ")
170
+
let vars' = Array.copy(rule.vars)
171
+
Array.reverse(vars')
172
+
"["
173
+
->String.concat(
174
+
vars'
175
+
->Array.map(Term.prettyPrintMeta)
176
+
->Array.join("")
177
+
->String.concat(" ")
178
+
->String.concat(
179
+
if Array.length(rule.premises) == 0 {
180
+
Judgment.prettyPrint(rule.conclusion, ~scope=[...rule.vars, ...scope])
181
+
} else {
182
+
rule.premises
183
+
->Array.map(r => prettyPrintInline(r, ~scope=[...rule.vars, ...scope]))
184
+
->Array.join(" ")
169
185
->String.concat(" |- ")
170
-
->String.concat(Judgment.prettyPrint(rule.conclusion,~scope=[...rule.vars,...scope]))
171
-
}
172
-
))->String.concat("]")
186
+
->String.concat(
187
+
Judgment.prettyPrint(rule.conclusion, ~scope=[...rule.vars, ...scope]),
188
+
)
189
+
},
190
+
),
191
+
)
192
+
->String.concat("]")
173
193
}
174
194
}
175
195
}
176
-
let prettyPrintTopLevel = (rule: t,~name="",~scope=[]:array<Term.meta>) => {
196
+
let prettyPrintTopLevel = (rule: t, ~name="", ~scope=[]: array<Term.meta>) => {
177
197
let vinculise = (strs: array<string>) => {
178
198
let l = strs->Array.map(String.length)->Array.concat([4])->Math.Int.maxMany
179
199
strs->Array.concat(["-"->String.repeat(l)->String.concat(" ")->String.concat(name)])
180
200
}
181
-
let myReverse = (arr) => {
201
+
let myReverse = arr => {
182
202
Array.reverse(arr)
183
203
arr
184
204
}
185
205
rule.vars
186
-
->Array.map(Term.prettyPrintMeta)
187
-
->myReverse
188
-
->Array.join("")
189
-
->String.concat(Util.newline)
190
-
->String.concat(
191
-
rule.premises
192
-
->Array.map(r => prettyPrintInline(r,~scope=[...rule.vars,...scope]))
193
-
->vinculise
194
-
->Array.concat([Judgment.prettyPrint(rule.conclusion,
195
-
~scope=[...rule.vars,...scope])])
196
-
->Array.map(s => String.concat(" ",s))
197
-
->Array.join(Util.newline))
206
+
->Array.map(Term.prettyPrintMeta)
207
+
->myReverse
208
+
->Array.join("")
209
+
->String.concat(Util.newline)
210
+
->String.concat(
211
+
rule.premises
212
+
->Array.map(r => prettyPrintInline(r, ~scope=[...rule.vars, ...scope]))
213
+
->vinculise
214
+
->Array.concat([Judgment.prettyPrint(rule.conclusion, ~scope=[...rule.vars, ...scope])])
215
+
->Array.map(s => String.concat(" ", s))
216
+
->Array.join(Util.newline),
217
+
)
198
218
}
199
219
}
+118
-88
src/RuleView.res
+118
-88
src/RuleView.res
···
2
2
open Util
3
3
type style = Gentzen | Linear | Hybrid
4
4
module Make = (
5
-
Term : TERM,
6
-
Judgment : JUDGMENT with module Term := Term,
7
-
JudgmentView : JUDGMENT_VIEW with module Term := Term and module Judgment := Judgment
5
+
Term: TERM,
6
+
Judgment: JUDGMENT with module Term := Term,
7
+
JudgmentView: JUDGMENT_VIEW with module Term := Term and module Judgment := Judgment,
8
8
) => {
9
-
module Rule = Rule.Make(Term, Judgment)
9
+
module Rule = Rule.Make(Term, Judgment)
10
10
module ScopeView = ScopeView.Make(Term, JudgmentView.TermView)
11
11
type props = {
12
-
rule:Rule.t,
13
-
style: style,
14
-
scope?: array<Term.meta>,
15
-
children: React.element
12
+
rule: Rule.t,
13
+
style: style,
14
+
scope?: array<Term.meta>,
15
+
children: React.element,
16
16
}
17
17
module type RULE_COMPONENT = {
18
-
let make : props => React.element
18
+
let make: props => React.element
19
19
}
20
-
module Inline : RULE_COMPONENT = {
21
-
let rec make = (props : props) => {
22
-
let {vars, premises,conclusion} = props.rule
20
+
module Inline: RULE_COMPONENT = {
21
+
let rec make = (props: props) => {
22
+
let {vars, premises, conclusion} = props.rule
23
23
let scope = vars->Array.concat(props.scope->Option.getOr([]))
24
24
<span className="inline-rule">
25
-
<span className="rule-rulename-defined">
26
-
{props.children}
27
-
</span>
25
+
<span className="rule-rulename-defined"> {props.children} </span>
28
26
<ScopeView scope=vars />
29
-
{React.array(premises
30
-
->Array.mapWithIndex((p,i)=><span key={String.make(i)} className="rule-context">
31
-
{React.createElement(make,withKey({rule:p, scope,children:React.string(""),style:props.style}, i))}</span>)
32
-
->Array.flatMapWithIndex( (e, i) =>
33
-
if i == 0 {
34
-
[e]
35
-
} else {
36
-
[<span key={String.make(-i)} className="symbol symbol-bold symbol-comma">{React.string(",")}</span>,e]
37
-
}))}
38
-
{if premises->Array.length > 0 {
39
-
<span className="symbol symbol-turnstile symbol-bold">
40
-
{React.string("⊢")}
41
-
</span>
42
-
} else {
27
+
{React.array(
28
+
premises
29
+
->Array.mapWithIndex((p, i) =>
30
+
<span key={String.make(i)} className="rule-context">
31
+
{React.createElement(
32
+
make,
33
+
withKey({rule: p, scope, children: React.string(""), style: props.style}, i),
34
+
)}
35
+
</span>
36
+
)
37
+
->Array.flatMapWithIndex((e, i) =>
38
+
if i == 0 {
39
+
[e]
40
+
} else {
41
+
[
42
+
<span key={String.make(-i)} className="symbol symbol-bold symbol-comma">
43
+
{React.string(",")}
44
+
</span>,
45
+
e,
46
+
]
47
+
}
48
+
),
49
+
)}
50
+
{if premises->Array.length > 0 {
51
+
<span className="symbol symbol-turnstile symbol-bold"> {React.string("⊢")} </span>
52
+
} else {
43
53
React.string("")
44
54
}}
45
-
<JudgmentView judgment={conclusion}
46
-
scope={scope} />
55
+
<JudgmentView judgment={conclusion} scope={scope} />
47
56
</span>
48
57
}
49
58
}
50
-
module Hypothetical = (Premise : RULE_COMPONENT) => {
51
-
let make = (props : props) => if Array.length(props.rule.premises) == 0 { Inline.make(props) } else {
52
-
let {vars, premises,conclusion} = props.rule
53
-
let scope = vars->Array.concat(props.scope->Option.getOr([]))
54
-
<table className="inference"><tbody>
55
-
<tr><td className="rule-cell rule-binderbox" rowSpan=3>
56
-
<ScopeView scope=vars/></td>
57
-
{React.array(premises->Array.mapWithIndex((p,i)=>
58
-
<td className="rule-cell rule-premise" key={String.make(i)}>
59
-
<Premise rule={p} scope={scope} key={String.make(i)} style={props.style}>
60
-
{React.string("")}
61
-
</Premise>
62
-
</td>))}
63
-
<td className="rule-cell rule-spacer"></td>
64
-
<td rowSpan=3 className="rule-cell rule-rulebox">
65
-
<span className="rule-rulename-defined">
66
-
{props.children}
67
-
</span>
68
-
</td>
69
-
</tr>
70
-
<tr> <td colSpan={premises->Array.length + 1} className="rule-cell">
71
-
{React.string("⋮")}
72
-
</td></tr>
73
-
<tr>
74
-
<td colSpan={premises->Array.length + 1} className="rule-cell rule-hypothetical-conclusion">
75
-
<JudgmentView judgment={conclusion} scope={scope} />
76
-
</td>
77
-
</tr></tbody></table>
78
-
}
59
+
module Hypothetical = (Premise: RULE_COMPONENT) => {
60
+
let make = (props: props) =>
61
+
if Array.length(props.rule.premises) == 0 {
62
+
Inline.make(props)
63
+
} else {
64
+
let {vars, premises, conclusion} = props.rule
65
+
let scope = vars->Array.concat(props.scope->Option.getOr([]))
66
+
<table className="inference">
67
+
<tbody>
68
+
<tr>
69
+
<td className="rule-cell rule-binderbox" rowSpan=3>
70
+
<ScopeView scope=vars />
71
+
</td>
72
+
{React.array(
73
+
premises->Array.mapWithIndex((p, i) =>
74
+
<td className="rule-cell rule-premise" key={String.make(i)}>
75
+
<Premise rule={p} scope={scope} key={String.make(i)} style={props.style}>
76
+
{React.string("")}
77
+
</Premise>
78
+
</td>
79
+
),
80
+
)}
81
+
<td className="rule-cell rule-spacer" />
82
+
<td rowSpan=3 className="rule-cell rule-rulebox">
83
+
<span className="rule-rulename-defined"> {props.children} </span>
84
+
</td>
85
+
</tr>
86
+
<tr>
87
+
<td colSpan={premises->Array.length + 1} className="rule-cell">
88
+
{React.string("⋮")}
89
+
</td>
90
+
</tr>
91
+
<tr>
92
+
<td
93
+
colSpan={premises->Array.length + 1}
94
+
className="rule-cell rule-hypothetical-conclusion">
95
+
<JudgmentView judgment={conclusion} scope={scope} />
96
+
</td>
97
+
</tr>
98
+
</tbody>
99
+
</table>
100
+
}
79
101
}
80
-
module TopLevel = (Premise : RULE_COMPONENT) => {
81
-
let make = (props : props) => {
82
-
let {vars, premises,conclusion} = props.rule
102
+
module TopLevel = (Premise: RULE_COMPONENT) => {
103
+
let make = (props: props) => {
104
+
let {vars, premises, conclusion} = props.rule
83
105
let scope = vars->Array.concat(props.scope->Option.getOr([]))
84
-
<div className="axiom"><table className="inference"><tbody>
85
-
<tr><td className="rule-cell rule-binderbox" rowSpan=2>
86
-
<ScopeView scope=vars/></td>
87
-
{React.array(premises->Array.mapWithIndex((p,i)=>
88
-
<td className="rule-cell rule-premise" key={String.make(i)}>
89
-
<Premise rule={p} scope={scope} key={String.make(i)} style={props.style}>
90
-
{React.string("")}
91
-
</Premise>
92
-
</td>))}
93
-
<td className="rule-cell rule-spacer"></td>
94
-
<td rowSpan=2 className="rule-cell rule-rulebox">
95
-
<span className="rule-rulename-defined">
96
-
{props.children}
97
-
</span>
98
-
</td>
99
-
</tr>
100
-
<tr>
101
-
<td colSpan={premises->Array.length + 1} className="rule-cell rule-conclusion">
102
-
<JudgmentView judgment={conclusion} scope={scope} />
103
-
</td>
104
-
</tr></tbody></table></div>
106
+
<div className="axiom">
107
+
<table className="inference">
108
+
<tbody>
109
+
<tr>
110
+
<td className="rule-cell rule-binderbox" rowSpan=2>
111
+
<ScopeView scope=vars />
112
+
</td>
113
+
{React.array(
114
+
premises->Array.mapWithIndex((p, i) =>
115
+
<td className="rule-cell rule-premise" key={String.make(i)}>
116
+
<Premise rule={p} scope={scope} key={String.make(i)} style={props.style}>
117
+
{React.string("")}
118
+
</Premise>
119
+
</td>
120
+
),
121
+
)}
122
+
<td className="rule-cell rule-spacer" />
123
+
<td rowSpan=2 className="rule-cell rule-rulebox">
124
+
<span className="rule-rulename-defined"> {props.children} </span>
125
+
</td>
126
+
</tr>
127
+
<tr>
128
+
<td colSpan={premises->Array.length + 1} className="rule-cell rule-conclusion">
129
+
<JudgmentView judgment={conclusion} scope={scope} />
130
+
</td>
131
+
</tr>
132
+
</tbody>
133
+
</table>
134
+
</div>
105
135
}
106
136
}
107
137
module Gentzen = TopLevel(Hypothetical(Inline))
108
138
module Hybrid = TopLevel(Inline)
109
-
139
+
110
140
@react.componentWithProps
111
-
let make = (props) => {
112
-
switch (props.style) {
141
+
let make = props => {
142
+
switch props.style {
113
143
| Hybrid => Hybrid.make(props)
114
144
| Gentzen => Gentzen.make(props)
115
145
| Linear => Inline.make(props)
116
146
}
117
147
}
118
-
}
148
+
}
+212
-166
src/SExp.res
+212
-166
src/SExp.res
···
1
-
module IntCmp = Belt.Id.MakeComparable({type t = int;let cmp = Pervasives.compare })
1
+
module IntCmp = Belt.Id.MakeComparable({
2
+
type t = int
3
+
let cmp = Pervasives.compare
4
+
})
2
5
3
6
type rec t =
4
-
Symbol({name: string })
5
-
| Compound({subexps: array<t>})
6
-
| Var({idx:int})
7
-
| Schematic({schematic:int, allowed: array<int>})
7
+
| Symbol({name: string})
8
+
| Compound({subexps: array<t>})
9
+
| Var({idx: int})
10
+
| Schematic({schematic: int, allowed: array<int>})
8
11
type meta = string
9
12
type schematic = int
10
-
type subst = Map.t<schematic,t>
11
-
let equivalent = (a : t, b: t) => {
13
+
type subst = Map.t<schematic, t>
14
+
let equivalent = (a: t, b: t) => {
12
15
a == b
13
16
}
14
-
let rec schematicsIn : (t) => Belt.Set.t<int, IntCmp.identity> = (it : t) => switch it {
15
-
| Schematic({schematic,_}) => Belt.Set.make(~id=module(IntCmp))->Belt.Set.add(schematic)
16
-
| Compound({subexps}) => subexps->Array.reduce(
17
-
Belt.Set.make(~id=module(IntCmp)),
18
-
(s, x) => Belt.Set.union(s, schematicsIn(x))
17
+
let rec schematicsIn: t => Belt.Set.t<int, IntCmp.identity> = (it: t) =>
18
+
switch it {
19
+
| Schematic({schematic, _}) => Belt.Set.make(~id=module(IntCmp))->Belt.Set.add(schematic)
20
+
| Compound({subexps}) =>
21
+
subexps->Array.reduce(Belt.Set.make(~id=module(IntCmp)), (s, x) =>
22
+
Belt.Set.union(s, schematicsIn(x))
23
+
)
24
+
| _ => Belt.Set.make(~id=module(IntCmp))
25
+
}
26
+
let rec freeVarsIn: t => Belt.Set.t<int, IntCmp.identity> = (it: t) =>
27
+
switch it {
28
+
| Var({idx}) => Belt.Set.make(~id=module(IntCmp))->Belt.Set.add(idx)
29
+
| Compound({subexps}) =>
30
+
subexps->Array.reduce(Belt.Set.make(~id=module(IntCmp)), (s, x) =>
31
+
Belt.Set.union(s, freeVarsIn(x))
32
+
)
33
+
| _ => Belt.Set.make(~id=module(IntCmp))
34
+
}
35
+
let rec substitute = (term: t, subst: subst) =>
36
+
switch term {
37
+
| Compound({subexps}) => Compound({subexps: Array.map(subexps, x => substitute(x, subst))})
38
+
| Schematic({schematic, _}) =>
39
+
switch Map.get(subst, schematic) {
40
+
| None => term
41
+
| Some(found) => found
42
+
}
43
+
| _ => term
44
+
}
45
+
46
+
let combineSubst = (s: subst, t: subst) => {
47
+
let nu = Map.make()
48
+
Map.entries(s)->Iterator.forEach(opt =>
49
+
switch opt {
50
+
| None => ()
51
+
| Some((key, term)) => nu->Map.set(key, term->substitute(t))
52
+
}
19
53
)
20
-
| _ => Belt.Set.make(~id=module(IntCmp))
21
-
}
22
-
let rec freeVarsIn : (t) => Belt.Set.t<int, IntCmp.identity> = (it : t) => switch it {
23
-
| Var({idx}) => Belt.Set.make(~id=module(IntCmp))->Belt.Set.add(idx)
24
-
| Compound({subexps}) => subexps->Array.reduce(
25
-
Belt.Set.make(~id=module(IntCmp)),
26
-
(s, x) => Belt.Set.union(s, freeVarsIn(x))
54
+
Map.entries(t)->Iterator.forEach(opt =>
55
+
switch opt {
56
+
| None => ()
57
+
| Some((key, term)) => nu->Map.set(key, term->substitute(s))
58
+
}
27
59
)
28
-
| _ => Belt.Set.make(~id=module(IntCmp))
29
-
}
30
-
let rec substitute = (term: t, subst: subst) => switch term {
31
-
| Compound({subexps}) =>
32
-
Compound({subexps: Array.map(subexps, x => substitute(x,subst))})
33
-
| Schematic({schematic, _}) => switch Map.get(subst,schematic) {
34
-
| None => term
35
-
| Some(found) => found
36
-
}
37
-
| _ => term
38
-
}
39
-
40
-
let combineSubst = (s : subst, t: subst) => {
41
-
let nu = Map.make();
42
-
Map.entries(s)->Iterator.forEach(opt => switch opt {
43
-
| None => ()
44
-
| Some((key,term)) => nu->Map.set(key, term->substitute(t))
45
-
})
46
-
Map.entries(t)->Iterator.forEach(opt => switch opt {
47
-
| None => ()
48
-
| Some((key,term)) => nu->Map.set(key, term->substitute(s))
49
-
})
50
60
nu
51
61
}
52
-
let emptySubst : subst = Map.make()
53
-
let singletonSubst : (int, t) => subst = (schematic,term) => {
62
+
let emptySubst: subst = Map.make()
63
+
let singletonSubst: (int, t) => subst = (schematic, term) => {
54
64
let s = Map.make()
55
-
s->Map.set(schematic,term)
65
+
s->Map.set(schematic, term)
56
66
s
57
67
}
58
-
let rec unifyTerm = (a: t, b: t) => switch (a,b) {
59
-
| (Symbol({name:na}), Symbol({name:nb})) if na == nb => Some(emptySubst)
60
-
| (Var({idx:ia}), Var({idx:ib})) if ia == ib => Some(emptySubst)
61
-
| (Schematic({schematic:sa,_}), Schematic({schematic:sb,_})) if sa == sb => Some(emptySubst)
62
-
| (Compound({subexps:xa}), Compound({subexps:xb})) if Array.length(xa) == Array.length(xb) =>
63
-
unifyArray(Belt.Array.zip(xa,xb))
64
-
| (Schematic({schematic,allowed}), t)
65
-
if !Belt.Set.has(schematicsIn(t), schematic)
66
-
&& Belt.Set.subset(freeVarsIn(t), Belt.Set.fromArray(allowed,~id=module(IntCmp)))
67
-
=> Some(singletonSubst(schematic,t))
68
-
| (t, Schematic({schematic,allowed}))
69
-
if !Belt.Set.has(schematicsIn(t), schematic)
70
-
&& Belt.Set.subset(freeVarsIn(t), Belt.Set.fromArray(allowed,~id=module(IntCmp)))
71
-
=> Some(singletonSubst(schematic,t))
72
-
| (_,_) => None
73
-
}
74
-
and unifyArray = (a: array<(t,t)>) => {
75
-
if (Array.length(a) == 0) {
68
+
let rec unifyTerm = (a: t, b: t) =>
69
+
switch (a, b) {
70
+
| (Symbol({name: na}), Symbol({name: nb})) if na == nb => Some(emptySubst)
71
+
| (Var({idx: ia}), Var({idx: ib})) if ia == ib => Some(emptySubst)
72
+
| (Schematic({schematic: sa, _}), Schematic({schematic: sb, _})) if sa == sb => Some(emptySubst)
73
+
| (Compound({subexps: xa}), Compound({subexps: xb})) if Array.length(xa) == Array.length(xb) =>
74
+
unifyArray(Belt.Array.zip(xa, xb))
75
+
| (Schematic({schematic, allowed}), t)
76
+
if !Belt.Set.has(schematicsIn(t), schematic) &&
77
+
Belt.Set.subset(freeVarsIn(t), Belt.Set.fromArray(allowed, ~id=module(IntCmp))) =>
78
+
Some(singletonSubst(schematic, t))
79
+
| (t, Schematic({schematic, allowed}))
80
+
if !Belt.Set.has(schematicsIn(t), schematic) &&
81
+
Belt.Set.subset(freeVarsIn(t), Belt.Set.fromArray(allowed, ~id=module(IntCmp))) =>
82
+
Some(singletonSubst(schematic, t))
83
+
| (_, _) => None
84
+
}
85
+
and unifyArray = (a: array<(t, t)>) => {
86
+
if Array.length(a) == 0 {
76
87
Some(emptySubst)
77
88
} else {
78
-
let (x,y) = a[0]->Option.getUnsafe
79
-
switch unifyTerm(x,y) {
80
-
| None => None
81
-
| Some(s1) => {
82
-
switch a
83
-
->Array.sliceToEnd(~start=1)
84
-
->Array.map(((t1,t2)) => (substitute(t1,s1),substitute(t2,s1)))
85
-
->unifyArray {
86
-
| None => None
87
-
| Some(s2) => Some(combineSubst(s1,s2))
88
-
}
89
+
let (x, y) = a[0]->Option.getUnsafe
90
+
switch unifyTerm(x, y) {
91
+
| None => None
92
+
| Some(s1) => switch a
93
+
->Array.sliceToEnd(~start=1)
94
+
->Array.map(((t1, t2)) => (substitute(t1, s1), substitute(t2, s1)))
95
+
->unifyArray {
96
+
| None => None
97
+
| Some(s2) => Some(combineSubst(s1, s2))
89
98
}
90
99
}
91
100
}
92
101
}
93
102
let unify = (a: t, b: t) => {
94
-
switch unifyTerm(a,b) {
103
+
switch unifyTerm(a, b) {
95
104
| None => []
96
105
| Some(s) => [s]
97
106
}
98
107
}
99
-
let rec substDeBruijn = (term: t, substs: array<t>, ~from:int=0) => switch term {
100
-
| Symbol(_) => term
101
-
| Compound({subexps}) =>
102
-
Compound({subexps: Array.map(subexps, x => substDeBruijn(x,substs,~from=from))})
103
-
| Var({idx:var}) => if (var < from) {
104
-
term
105
-
} else if (var - from < Array.length(substs) && var - from >= 0) {
106
-
Option.getUnsafe(substs[var - from])
107
-
} else {
108
-
Var({idx: var - Array.length(substs) })
109
-
}
110
-
| Schematic({schematic,allowed}) =>
111
-
Schematic({schematic, allowed:
112
-
Array.filterMap(allowed, i =>
113
-
if (i < from + Array.length(substs)) {
114
-
None
115
-
} else {
108
+
let rec substDeBruijn = (term: t, substs: array<t>, ~from: int=0) =>
109
+
switch term {
110
+
| Symbol(_) => term
111
+
| Compound({subexps}) =>
112
+
Compound({subexps: Array.map(subexps, x => substDeBruijn(x, substs, ~from))})
113
+
| Var({idx: var}) =>
114
+
if var < from {
115
+
term
116
+
} else if var - from < Array.length(substs) && var - from >= 0 {
117
+
Option.getUnsafe(substs[var - from])
118
+
} else {
119
+
Var({idx: var - Array.length(substs)})
120
+
}
121
+
| Schematic({schematic, allowed}) =>
122
+
Schematic({
123
+
schematic,
124
+
allowed: Array.filterMap(allowed, i =>
125
+
if i < from + Array.length(substs) {
126
+
None
127
+
} else {
116
128
Some(i - (from + Array.length(substs)))
117
129
}
118
-
)
130
+
),
119
131
})
120
-
}
121
-
let rec upshift = (term: t, amount: int, ~from:int=0) => switch term {
122
-
| Symbol(_) => term
123
-
| Compound({subexps}) =>
124
-
Compound({subexps: Array.map(subexps, x => upshift(x,amount,~from=from))})
125
-
| Var({idx}) => Var({idx: if (idx >= from) { idx + amount } else { idx }})
126
-
| Schematic({schematic,allowed}) =>
127
-
Schematic({schematic, allowed:
128
-
Array.map(allowed, i => if (i >= from) { i + amount } else { i })
132
+
}
133
+
let rec upshift = (term: t, amount: int, ~from: int=0) =>
134
+
switch term {
135
+
| Symbol(_) => term
136
+
| Compound({subexps}) => Compound({subexps: Array.map(subexps, x => upshift(x, amount, ~from))})
137
+
| Var({idx}) =>
138
+
Var({
139
+
idx: if idx >= from {
140
+
idx + amount
141
+
} else {
142
+
idx
143
+
},
129
144
})
130
-
}
131
-
let place = (x : int,~scope: array<string>)
132
-
=> Schematic({schematic:x,allowed: Array.fromInitializer(~length=Array.length(scope), i=>i)})
145
+
| Schematic({schematic, allowed}) =>
146
+
Schematic({
147
+
schematic,
148
+
allowed: Array.map(allowed, i =>
149
+
if i >= from {
150
+
i + amount
151
+
} else {
152
+
i
153
+
}
154
+
),
155
+
})
156
+
}
157
+
let place = (x: int, ~scope: array<string>) => Schematic({
158
+
schematic: x,
159
+
allowed: Array.fromInitializer(~length=Array.length(scope), i => i),
160
+
})
133
161
type gen = ref<int>
134
-
let seen = (g : gen, s : int) => {
135
-
if (s >= g.contents) {
162
+
let seen = (g: gen, s: int) => {
163
+
if s >= g.contents {
136
164
g := s + 1
137
165
}
138
166
}
139
-
let fresh = (g : gen, ~replacing as _ =?) => {
167
+
let fresh = (g: gen, ~replacing as _=?) => {
140
168
let v = g.contents
141
169
g := g.contents + 1
142
170
v
143
171
}
144
-
let prettyPrintVar = (idx: int, scope: array<string>) => switch scope[idx] {
145
-
| Some(n) if Array.indexOf(scope,n) == idx && false => n
146
-
| _ => "\\"->String.concat(String.make(idx))
147
-
}
172
+
let prettyPrintVar = (idx: int, scope: array<string>) =>
173
+
switch scope[idx] {
174
+
| Some(n) if Array.indexOf(scope, n) == idx && false => n
175
+
| _ => "\\"->String.concat(String.make(idx))
176
+
}
148
177
let makeGen = () => {
149
178
ref(0)
150
179
}
151
-
let rec prettyPrint = (it: t, ~scope: array<string>) => switch it{
152
-
| Symbol({name}) => name
153
-
| Var({idx}) => prettyPrintVar(idx,scope)
154
-
| Schematic({schematic,allowed}) =>
155
-
"?"->String.concat(String.make(schematic))
180
+
let rec prettyPrint = (it: t, ~scope: array<string>) =>
181
+
switch it {
182
+
| Symbol({name}) => name
183
+
| Var({idx}) => prettyPrintVar(idx, scope)
184
+
| Schematic({schematic, allowed}) =>
185
+
"?"
186
+
->String.concat(String.make(schematic))
156
187
->String.concat("(")
157
-
->String.concat(Array.join(allowed->Array.map(idx =>prettyPrintVar(idx,scope))," "))
188
+
->String.concat(Array.join(allowed->Array.map(idx => prettyPrintVar(idx, scope)), " "))
158
189
->String.concat(")")
159
-
| Compound({subexps}) =>
160
-
"("->String.concat(Array.join(subexps->Array.map(e => prettyPrint(e,~scope=scope)), " "))
190
+
| Compound({subexps}) =>
191
+
"("
192
+
->String.concat(Array.join(subexps->Array.map(e => prettyPrint(e, ~scope)), " "))
161
193
->String.concat(")")
162
-
}
163
-
let symbolRegexpString = "^([^\\s()]+)";
164
-
let varRegexpString = "^\\\\([0-9]+)$";
165
-
let schematicRegexpString = "^\\?([0-9]+)$";
194
+
}
195
+
let symbolRegexpString = "^([^\\s()]+)"
196
+
let varRegexpString = "^\\\\([0-9]+)$"
197
+
let schematicRegexpString = "^\\?([0-9]+)$"
166
198
type lexeme = LParen | RParen | VarT(int) | SymbolT(string) | SchematicT(int)
167
199
let nameRES = "^([^\\s.\\[\\]()]+)\\."
168
200
let prettyPrintMeta = (str: string) => {
169
-
String.concat(str,".")
201
+
String.concat(str, ".")
170
202
}
171
203
let parseMeta = (str: string) => {
172
-
let re = RegExp.fromStringWithFlags(nameRES,~flags="y")
204
+
let re = RegExp.fromStringWithFlags(nameRES, ~flags="y")
173
205
switch re->RegExp.exec(str->String.trim) {
174
206
| None => Error("not a meta name")
175
-
| Some(res) => switch RegExp.Result.matches(res) {
176
-
| [n] => Ok(n,String.sliceToEnd(str->String.trim,~start=RegExp.lastIndex(re)))
207
+
| Some(res) =>
208
+
switch RegExp.Result.matches(res) {
209
+
| [n] => Ok(n, String.sliceToEnd(str->String.trim, ~start=RegExp.lastIndex(re)))
177
210
| _ => Error("impossible happened")
178
211
}
179
212
}
180
213
}
181
214
let parse = (str: string, ~scope: array<string>, ~gen=?) => {
182
-
let cur = ref(String.make(str));
183
-
let lex : () => option<lexeme> = () => {
184
-
let str = String.trim(cur.contents);
215
+
let cur = ref(String.make(str))
216
+
let lex: unit => option<lexeme> = () => {
217
+
let str = String.trim(cur.contents)
185
218
cur := str
186
219
let checkVariable = (candidate: string) => {
187
220
let varRegexp = RegExp.fromString(varRegexpString)
188
-
switch (Array.indexOf(scope,candidate)) {
189
-
| -1 => switch varRegexp->RegExp.exec(candidate) {
190
-
| Some(res') => switch RegExp.Result.matches(res') {
221
+
switch Array.indexOf(scope, candidate) {
222
+
| -1 =>
223
+
switch varRegexp->RegExp.exec(candidate) {
224
+
| Some(res') =>
225
+
switch RegExp.Result.matches(res') {
191
226
| [idx] => Some(idx->Int.fromString->Option.getUnsafe)
192
227
| _ => None
193
228
}
···
196
231
| idx => Some(idx)
197
232
}
198
233
}
199
-
if (String.get(str,0) == Some("(")) {
200
-
cur := String.sliceToEnd(str,~start=1)
234
+
if String.get(str, 0) == Some("(") {
235
+
cur := String.sliceToEnd(str, ~start=1)
201
236
Some(LParen)
202
-
} else if (String.get(str,0) == Some(")")) {
203
-
cur := String.sliceToEnd(str,~start=1)
237
+
} else if String.get(str, 0) == Some(")") {
238
+
cur := String.sliceToEnd(str, ~start=1)
204
239
Some(RParen)
205
240
} else {
206
-
let symbolRegexp = RegExp.fromStringWithFlags(symbolRegexpString,~flags="y")
241
+
let symbolRegexp = RegExp.fromStringWithFlags(symbolRegexpString, ~flags="y")
207
242
switch symbolRegexp->RegExp.exec(str) {
208
243
| None => None
209
-
| Some(res) => switch RegExp.Result.matches(res) {
244
+
| Some(res) =>
245
+
switch RegExp.Result.matches(res) {
210
246
| [symb] => {
211
-
cur := String.sliceToEnd(str,~start=RegExp.lastIndex(symbolRegexp))
247
+
cur := String.sliceToEnd(str, ~start=RegExp.lastIndex(symbolRegexp))
212
248
switch checkVariable(symb) {
213
249
| Some(idx) => Some(VarT(idx))
214
250
| None => {
215
251
let schematicRegexp = RegExp.fromString(schematicRegexpString)
216
252
switch schematicRegexp->RegExp.exec(symb) {
217
253
| None => Some(SymbolT(symb))
218
-
| Some(res') => switch RegExp.Result.matches(res') {
254
+
| Some(res') =>
255
+
switch RegExp.Result.matches(res') {
219
256
| [s] => Some(SchematicT(s->Int.fromString->Option.getUnsafe))
220
257
| _ => Some(SymbolT(symb))
221
258
}
···
228
265
}
229
266
}
230
267
}
231
-
268
+
232
269
let peek = () => {
233
270
// a bit slow, better would be to keep a backlog of lexed tokens..
234
271
let str = String.make(cur.contents)
235
272
let tok = lex()
236
273
cur := str
237
-
tok
274
+
tok
238
275
}
239
276
exception ParseError(string)
240
277
let rec parseExp = () => {
241
278
let tok = peek()
242
279
switch tok {
243
-
| Some(SymbolT(s)) => { let _ = lex(); Some(Symbol({name: s})) }
244
-
| Some(VarT(idx)) => { let _ = lex(); Some(Var({idx: idx})) }
280
+
| Some(SymbolT(s)) => {
281
+
let _ = lex()
282
+
Some(Symbol({name: s}))
283
+
}
284
+
| Some(VarT(idx)) => {
285
+
let _ = lex()
286
+
Some(Var({idx: idx}))
287
+
}
245
288
| Some(SchematicT(num)) => {
246
-
let _ = lex();
289
+
let _ = lex()
247
290
switch lex() {
248
291
| Some(LParen) => {
249
292
let it = ref(None)
250
-
let bits = [];
251
-
let getVar = (t : option<lexeme>) => switch t {
252
-
| Some(VarT(idx)) => Some(idx)
253
-
| _ => None
254
-
}
255
-
while {it := lex(); it.contents->getVar->Option.isSome} {
293
+
let bits = []
294
+
let getVar = (t: option<lexeme>) =>
295
+
switch t {
296
+
| Some(VarT(idx)) => Some(idx)
297
+
| _ => None
298
+
}
299
+
while {
300
+
it := lex()
301
+
it.contents->getVar->Option.isSome
302
+
} {
256
303
Array.push(bits, it.contents->getVar->Option.getUnsafe)
257
304
}
258
305
switch it.contents {
259
-
| Some(RParen) => {
260
-
switch gen {
261
-
| Some(g) => {
262
-
seen(g,num);
263
-
Some(Schematic({schematic: num, allowed: bits }))
264
-
}
265
-
| None => raise(ParseError("Schematics not allowed here"))
306
+
| Some(RParen) => switch gen {
307
+
| Some(g) => {
308
+
seen(g, num)
309
+
Some(Schematic({schematic: num, allowed: bits}))
266
310
}
267
-
311
+
| None => raise(ParseError("Schematics not allowed here"))
268
312
}
269
313
| _ => raise(ParseError("Expected closing parenthesis"))
270
314
}
···
273
317
}
274
318
}
275
319
| Some(LParen) => {
276
-
let _ = lex();
277
-
let bits = [];
320
+
let _ = lex()
321
+
let bits = []
278
322
let it = ref(None)
279
-
while {it := parseExp(); it.contents->Option.isSome} {
323
+
while {
324
+
it := parseExp()
325
+
it.contents->Option.isSome
326
+
} {
280
327
Array.push(bits, it.contents->Option.getUnsafe)
281
328
}
282
329
switch lex() {
283
-
| Some(RParen) => Some(Compound({subexps:bits}))
330
+
| Some(RParen) => Some(Compound({subexps: bits}))
284
331
| _ => raise(ParseError("Expected closing parenthesis"))
285
332
}
286
333
}
···
290
337
switch parseExp() {
291
338
| exception ParseError(s) => Error(s)
292
339
| None => Error("No expression to parse")
293
-
| Some(e) => Ok((e,cur.contents))
340
+
| Some(e) => Ok((e, cur.contents))
294
341
}
295
342
}
296
-
+9
-10
src/SExp.resi
+9
-10
src/SExp.resi
···
1
-
2
1
type rec t =
3
-
Symbol({name: string })
4
-
| Compound({subexps: array<t>})
5
-
| Var({idx:int})
6
-
| Schematic({schematic:int, allowed: array<int>})
2
+
| Symbol({name: string})
3
+
| Compound({subexps: array<t>})
4
+
| Var({idx: int})
5
+
| Schematic({schematic: int, allowed: array<int>})
7
6
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>
7
+
include Signatures.TERM
8
+
with type t := t
9
+
and type meta = string
10
+
and type schematic = int
11
+
and type subst = Map.t<int, t>
+4
-4
src/SExpJView.res
+4
-4
src/SExpJView.res
···
1
1
module TermView = SExpView
2
-
type props = {
3
-
judgment: SExp.t,
4
-
scope: array<string>
2
+
type props = {
3
+
judgment: SExp.t,
4
+
scope: array<string>,
5
5
}
6
-
let make = ({judgment,scope}) => SExpView.make({term: judgment,scope})
6
+
let make = ({judgment, scope}) => SExpView.make({term: judgment, scope})
+1
-1
src/SExpJView.resi
+1
-1
src/SExpJView.resi
+47
-41
src/SExpView.res
+47
-41
src/SExpView.res
···
1
1
type props = {term: SExp.t, scope: array<string>}
2
2
open Util
3
-
type idx_props = {idx:int, scope:array<string>}
4
-
let viewVar = (props : idx_props) => switch props.scope[props.idx] {
5
-
| Some(n) if Array.indexOf(props.scope,n) == props.idx =>
6
-
<span className="term-metavar">
7
-
{ React.string(n)}
8
-
</span>
9
-
| _ =>
10
-
<span className="term-metavar-unnamed">
11
-
{React.string("\\")} { React.int(props.idx) }
12
-
</span>
13
-
}
3
+
type idx_props = {idx: int, scope: array<string>}
4
+
let viewVar = (props: idx_props) =>
5
+
switch props.scope[props.idx] {
6
+
| Some(n) if Array.indexOf(props.scope, n) == props.idx =>
7
+
<span className="term-metavar"> {React.string(n)} </span>
8
+
| _ =>
9
+
<span className="term-metavar-unnamed">
10
+
{React.string("\\")}
11
+
{React.int(props.idx)}
12
+
</span>
13
+
}
14
14
15
-
let makeMeta = (str : string) =>
15
+
let makeMeta = (str: string) =>
16
16
<span className="rule-binder">
17
-
{React.string(str)}{React.string(".")}
17
+
{React.string(str)}
18
+
{React.string(".")}
18
19
</span>
19
20
20
-
let parenthesise = (f) => [
21
-
<span className="symbol" key={"-1"}>
22
-
{React.string("(")}
23
-
</span>,
24
-
...f,
25
-
<span className="symbol" key={"-2"}>
26
-
{React.string(")")}
27
-
</span>
28
-
]
29
-
30
-
let intersperse = (a) =>
31
-
a->Array.flatMapWithIndex((e, i) => if i == 0 { [e] } else { [React.string(" "),e] })
32
-
21
+
let parenthesise = f =>
22
+
[
23
+
<span className="symbol" key={"-1"}> {React.string("(")} </span>,
24
+
...f,
25
+
<span className="symbol" key={"-2"}> {React.string(")")} </span>,
26
+
]
27
+
28
+
let intersperse = a =>
29
+
a->Array.flatMapWithIndex((e, i) =>
30
+
if i == 0 {
31
+
[e]
32
+
} else {
33
+
[React.string(" "), e]
34
+
}
35
+
)
33
36
34
37
@react.componentWithProps
35
-
let rec make = ({term, scope}) => switch term {
36
-
| Compound({subexps:bits}) => {
37
-
<span className="term-compound">
38
-
{bits
39
-
->Array.mapWithIndex( (t, i) =>
40
-
React.createElement(make,withKey({term:t,scope },i)))
41
-
->intersperse->parenthesise->React.array}
38
+
let rec make = ({term, scope}) =>
39
+
switch term {
40
+
| Compound({subexps: bits}) => <span className="term-compound">
41
+
{bits
42
+
->Array.mapWithIndex((t, i) => React.createElement(make, withKey({term: t, scope}, i)))
43
+
->intersperse
44
+
->parenthesise
45
+
->React.array}
42
46
</span>
43
-
}
44
-
| Var({idx:idx}) => viewVar({idx,scope})
45
-
| Symbol({name:s}) => <span className="term-const"> { React.string(s) } </span>
46
-
| Schematic({schematic:s, allowed:vs}) =>
47
+
| Var({idx}) => viewVar({idx, scope})
48
+
| Symbol({name: s}) => <span className="term-const"> {React.string(s)} </span>
49
+
| Schematic({schematic: s, allowed: vs}) =>
47
50
<span className="term-schematic">
48
-
{React.string("?")} {React.int(s)}
51
+
{React.string("?")}
52
+
{React.int(s)}
49
53
<span className="term-schematic-telescope">
50
54
{vs
51
-
->Array.mapWithIndex( (v,i) => React.createElement(viewVar, withKey({idx:v,scope},i)))
52
-
->intersperse->parenthesise->React.array}
55
+
->Array.mapWithIndex((v, i) => React.createElement(viewVar, withKey({idx: v, scope}, i)))
56
+
->intersperse
57
+
->parenthesise
58
+
->React.array}
53
59
</span>
54
60
</span>
55
-
}
61
+
}
+1
-1
src/SExpView.resi
+1
-1
src/SExpView.resi
+10
-15
src/ScopeView.res
+10
-15
src/ScopeView.res
···
1
1
open Signatures
2
2
3
-
module Make = (
4
-
Term : TERM,
5
-
TermView : TERM_VIEW with module Term := Term
6
-
) => {
7
-
type props = { scope: array<Term.meta> }
3
+
module Make = (Term: TERM, TermView: TERM_VIEW with module Term := Term) => {
4
+
type props = {scope: array<Term.meta>}
8
5
@react.componentWithProps
9
-
let make = (props) => {
10
-
let arr = props.scope->Array.mapWithIndex((m,i) =>
11
-
<React.Fragment key={String.make(i)}>
12
-
{TermView.makeMeta(m)}
13
-
</React.Fragment>)
6
+
let make = props => {
7
+
let arr =
8
+
props.scope->Array.mapWithIndex((m, i) =>
9
+
<React.Fragment key={String.make(i)}> {TermView.makeMeta(m)} </React.Fragment>
10
+
)
14
11
Array.reverse(arr)
15
-
if Array.length(arr) > 0 {
16
-
<span className="rule-binders">
17
-
{React.array(arr)}
18
-
</span>
12
+
if Array.length(arr) > 0 {
13
+
<span className="rule-binders"> {React.array(arr)} </span>
19
14
} else {
20
15
React.null
21
16
}
22
17
}
23
-
}
18
+
}
+9
-5
src/Scratch.res
+9
-5
src/Scratch.res
···
1
-
module AxiomS = Editable.TextArea(AxiomSet.Make(SExp,SExp,SExpJView))
2
-
module DerivationsOrLemmasView = MethodView.CombineMethodView(SExp,SExp,MethodView.DerivationView(SExp,SExp),MethodView.LemmaView(SExp,SExp,SExpJView))
3
-
module TheoremS = Editable.TextArea(Theorem.Make(SExp,SExp,SExpJView,DerivationsOrLemmasView))
4
-
module ConfS = ConfigBlock.Make(SExp,SExp)
5
-
1
+
module AxiomS = Editable.TextArea(AxiomSet.Make(SExp, SExp, SExpJView))
2
+
module DerivationsOrLemmasView = MethodView.CombineMethodView(
3
+
SExp,
4
+
SExp,
5
+
MethodView.DerivationView(SExp, SExp),
6
+
MethodView.LemmaView(SExp, SExp, SExpJView),
7
+
)
8
+
module TheoremS = Editable.TextArea(Theorem.Make(SExp, SExp, SExpJView, DerivationsOrLemmasView))
9
+
module ConfS = ConfigBlock.Make(SExp, SExp)
+30
-34
src/Signatures.res
+30
-34
src/Signatures.res
···
1
-
2
1
module type TERM = {
3
2
type t
4
3
type schematic
5
4
type meta
6
-
type subst = Map.t<schematic,t>
7
-
let substitute : (t, subst) => t
8
-
let unify : (t, t) => array<subst>
5
+
type subst = Map.t<schematic, t>
6
+
let substitute: (t, subst) => t
7
+
let unify: (t, t) => array<subst>
9
8
// law: unify(a,b) == [{}] iff equivalent(a,b)
10
-
let equivalent : (t, t) => bool
11
-
let substDeBruijn : (t, array<t>, ~from:int=?) => t
12
-
let upshift : (t, int, ~from:int=?) => t
9
+
let equivalent: (t, t) => bool
10
+
let substDeBruijn: (t, array<t>, ~from: int=?) => t
11
+
let upshift: (t, int, ~from: int=?) => t
13
12
type gen
14
-
let fresh : (gen, ~replacing:meta=?) => schematic
15
-
let seen : (gen, schematic) => ()
16
-
let place : (schematic, ~scope: array<meta>) => t
17
-
let makeGen : () => gen
18
-
let parse : (string, ~scope: array<meta>, ~gen: gen=?) => result<(t,string),string>
19
-
let parseMeta : (string) => result<(meta,string),string>
20
-
let prettyPrint : (t, ~scope: array<meta>) => string
21
-
let prettyPrintMeta : (meta) => string
13
+
let fresh: (gen, ~replacing: meta=?) => schematic
14
+
let seen: (gen, schematic) => unit
15
+
let place: (schematic, ~scope: array<meta>) => t
16
+
let makeGen: unit => gen
17
+
let parse: (string, ~scope: array<meta>, ~gen: gen=?) => result<(t, string), string>
18
+
let parseMeta: string => result<(meta, string), string>
19
+
let prettyPrint: (t, ~scope: array<meta>) => string
20
+
let prettyPrintMeta: meta => string
22
21
}
23
22
24
23
module type JUDGMENT = {
25
-
module Term : TERM
24
+
module Term: TERM
26
25
type t
27
-
let substitute : (t, Term.subst) => t
28
-
let equivalent : (t,t) => bool
29
-
let unify : (t, t) => array<Term.subst>
30
-
let substDeBruijn : (t, array<Term.t>, ~from:int=?) => t
31
-
let upshift : (t, int, ~from:int=?) => t
32
-
let parse : (string, ~scope: array<Term.meta>, ~gen: Term.gen=?) => result<(t,string),string>
33
-
let prettyPrint : (t, ~scope: array<Term.meta>) => string
26
+
let substitute: (t, Term.subst) => t
27
+
let equivalent: (t, t) => bool
28
+
let unify: (t, t) => array<Term.subst>
29
+
let substDeBruijn: (t, array<Term.t>, ~from: int=?) => t
30
+
let upshift: (t, int, ~from: int=?) => t
31
+
let parse: (string, ~scope: array<Term.meta>, ~gen: Term.gen=?) => result<(t, string), string>
32
+
let prettyPrint: (t, ~scope: array<Term.meta>) => string
34
33
}
35
-
36
34
37
35
module type TERM_VIEW = {
38
-
module Term : TERM
36
+
module Term: TERM
39
37
type props = {term: Term.t, scope: array<Term.meta>}
40
-
let make : props => React.element
41
-
let makeMeta : Term.meta => React.element
38
+
let make: props => React.element
39
+
let makeMeta: Term.meta => React.element
42
40
}
43
41
44
42
module type JUDGMENT_VIEW = {
45
-
module Term : TERM
46
-
module Judgment : JUDGMENT with module Term := Term;
47
-
module TermView : TERM_VIEW with module Term := Term;
43
+
module Term: TERM
44
+
module Judgment: JUDGMENT with module Term := Term
45
+
module TermView: TERM_VIEW with module Term := Term
48
46
type props = {judgment: Judgment.t, scope: array<Term.meta>}
49
-
let make : props => React.element
50
-
}
51
-
52
-
47
+
let make: props => React.element
48
+
}
+34
-29
src/Theorem.res
+34
-29
src/Theorem.res
···
2
2
open Component
3
3
open MethodView
4
4
module Make = (
5
-
Term : TERM,
6
-
Judgment : JUDGMENT with module Term := Term,
7
-
JudgmentView : JUDGMENT_VIEW with module Term := Term and module Judgment := Judgment,
8
-
MethodView : METHOD_VIEW with module Term := Term and module Judgment := Judgment
5
+
Term: TERM,
6
+
Judgment: JUDGMENT with module Term := Term,
7
+
JudgmentView: JUDGMENT_VIEW with module Term := Term and module Judgment := Judgment,
8
+
MethodView: METHOD_VIEW with module Term := Term and module Judgment := Judgment,
9
9
) => {
10
-
module Rule = Rule.Make(Term,Judgment)
11
-
module Proof = Proof.Make(Term,Judgment,MethodView.Method)
12
-
module Context = Method.Context(Term,Judgment)
13
-
module ProofView = ProofView.Make(Term,Judgment,JudgmentView,MethodView)
10
+
module Rule = Rule.Make(Term, Judgment)
11
+
module Proof = Proof.Make(Term, Judgment, MethodView.Method)
12
+
module Context = Method.Context(Term, Judgment)
13
+
module ProofView = ProofView.Make(Term, Judgment, JudgmentView, MethodView)
14
14
open RuleView
15
-
module RuleView = RuleView.Make(Term,Judgment,JudgmentView)
16
-
module Ports = Ports(Term,Judgment)
17
-
type props = { content: string, imports: Ports.t, onLoad: (~exports:Ports.t,~string:string=?) => (), onChange: (string,~exports:Ports.t) => () }
15
+
module RuleView = RuleView.Make(Term, Judgment, JudgmentView)
16
+
module Ports = Ports(Term, Judgment)
17
+
type props = {
18
+
content: string,
19
+
imports: Ports.t,
20
+
onLoad: (~exports: Ports.t, ~string: string=?) => unit,
21
+
onChange: (string, ~exports: Ports.t) => unit,
22
+
}
18
23
type state = {name: string, rule: Rule.t, proof: Proof.checked}
19
-
let deserialise = (facts : Dict.t<Rule.t>, gen : Term.gen, str : string) : result<state,string> => {
24
+
let deserialise = (facts: Dict.t<Rule.t>, gen: Term.gen, str: string): result<state, string> => {
20
25
let cur = ref(str)
21
-
switch Rule.parseTopLevel(cur.contents,~scope=[],~gen=gen) {
26
+
switch Rule.parseTopLevel(cur.contents, ~scope=[], ~gen) {
22
27
| Error(e) => Error(e)
23
-
| Ok(((r,n),s)) => switch Proof.parse(s,~scope=[],~gen=gen) {
28
+
| Ok(((r, n), s)) =>
29
+
switch Proof.parse(s, ~scope=[], ~gen) {
24
30
| Error(e) => Error(e)
25
-
| Ok((_,s')) if String.length(String.trim(s')) > 0 =>
26
-
Error("Trailing input: "->String.concat(s'))
27
-
| Ok((prf,_)) => {
28
-
let ctx : Context.t = {fixes:[],facts}
29
-
Ok({name:n,rule:r,proof:Proof.check(ctx,prf,r)})
31
+
| Ok((_, s')) if String.length(String.trim(s')) > 0 =>
32
+
Error("Trailing input: "->String.concat(s'))
33
+
| Ok((prf, _)) => {
34
+
let ctx: Context.t = {fixes: [], facts}
35
+
Ok({name: n, rule: r, proof: Proof.check(ctx, prf, r)})
30
36
}
31
37
}
32
38
}
33
39
}
34
-
let make = (props) => {
35
-
40
+
let make = props => {
36
41
let gen = Term.makeGen()
37
42
switch deserialise(props.imports.facts, gen, props.content) {
38
43
| Ok(state) => {
39
44
React.useEffect(() => {
40
-
let export = Dict.fromArray([(state.name,state.rule)])
41
-
props.onLoad(~exports= {Ports.facts: export, ruleStyle: None});
45
+
let export = Dict.fromArray([(state.name, state.rule)])
46
+
props.onLoad(~exports={Ports.facts: export, ruleStyle: None})
42
47
None
43
48
}, [])
44
49
let ruleStyle = props.imports.ruleStyle->Option.getOr(Hybrid)
45
50
<>
46
-
<RuleView rule={state.rule} scope={[]} style={ruleStyle}>
47
-
{React.string(state.name)}
48
-
</RuleView>
49
-
<ProofView ruleStyle={ruleStyle} scope={[]} proof=state.proof />
51
+
<RuleView rule={state.rule} scope={[]} style={ruleStyle}>
52
+
{React.string(state.name)}
53
+
</RuleView>
54
+
<ProofView ruleStyle={ruleStyle} scope={[]} proof=state.proof />
50
55
</>
51
56
}
52
57
| Error(err) => {
53
58
React.useEffect(() => {
54
-
props.onLoad(~exports={Ports.facts: Dict.make(), ruleStyle: None});
59
+
props.onLoad(~exports={Ports.facts: Dict.make(), ruleStyle: None})
55
60
None
56
61
}, [])
57
62
<div className="error"> {React.string(err)} </div>
58
-
}
63
+
}
59
64
}
60
65
}
61
66
}
+7
-7
src/Util.res
+7
-7
src/Util.res
···
1
1
let newline = "\n"
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))
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
6
})
7
7
nu
8
8
}
9
-
let withKey: ('props, int) => 'props = %raw(`(props, key) => ({...props, key})`)
9
+
let withKey: ('props, int) => 'props = %raw(`(props, key) => ({...props, key})`)
10
10
11
-
let arrayWithIndex = (arr : array<React.element>) => {
12
-
React.array(arr->Array.mapWithIndex((m,i) => <span key={String.make(i)}>m</span>))
11
+
let arrayWithIndex = (arr: array<React.element>) => {
12
+
React.array(arr->Array.mapWithIndex((m, i) => <span key={String.make(i)}> m </span>))
13
13
}