the next generation of the in-browser educational proof assistant
symbol view logic
+39
-94
+1
-1
index.html
+1
-1
index.html
+6
-63
src/SExpView.res
+6
-63
src/SExpView.res
···
1
-
type props = {term: SExp.t, scope: array<string>}
2
-
open Util
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
-
}
1
+
module ConstSymbol = SExp.ConstSymbol
2
+
module ConstSymbolView: SExpViewFunc.SYMBOL_VIEW with module Symbol := SExp.ConstSymbol = {
3
+
type props = {name: ConstSymbol.t, scope: array<string>}
4
+
let make = (props: props) => React.string(props.name)
5
+
}
14
6
15
-
let makeMeta = (str: string) =>
16
-
<span className="rule-binder">
17
-
{React.string(str)}
18
-
{React.string(".")}
19
-
</span>
20
-
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
-
)
36
-
37
-
@react.componentWithProps
38
-
let rec make = ({term, scope}) =>
39
-
switch term {
40
-
| Compound({subexps: bits}) =>
41
-
<span className="term-compound">
42
-
{bits
43
-
->Array.mapWithIndex((t, i) => React.createElement(make, withKey({term: t, scope}, i)))
44
-
->intersperse
45
-
->parenthesise
46
-
->React.array}
47
-
</span>
48
-
| Var({idx}) => viewVar({idx, scope})
49
-
| Symbol(name) =>
50
-
<span className="term-const"> {React.string(name->SExp.Symbol.prettyPrint(~scope))} </span>
51
-
| Schematic({schematic: s, allowed: vs}) =>
52
-
<span className="term-schematic">
53
-
{React.string("?")}
54
-
{React.int(s)}
55
-
<span className="term-schematic-telescope">
56
-
{vs
57
-
->Array.mapWithIndex((v, i) => React.createElement(viewVar, withKey({idx: v, scope}, i)))
58
-
->intersperse
59
-
->parenthesise
60
-
->React.array}
61
-
</span>
62
-
</span>
63
-
| Ghost => React.null
64
-
}
7
+
include SExpViewFunc.Make(ConstSymbol, ConstSymbolView, SExp)
+2
src/SExpView.resi
+2
src/SExpView.resi
+14
-2
src/SExpViewFunc.res
+14
-2
src/SExpViewFunc.res
···
1
-
module Make = (Symbol: SExpFunc.SYMBOL, SExp: module type of SExpFunc.Make(Symbol)): {
1
+
module type SYMBOL_VIEW = {
2
+
module Symbol: SExpFunc.SYMBOL
3
+
type props = {name: Symbol.t, scope: array<string>}
4
+
let make: props => React.element
5
+
}
6
+
7
+
module Make = (
8
+
Symbol: SExpFunc.SYMBOL,
9
+
SymbolView: SYMBOL_VIEW with module Symbol := Symbol,
10
+
SExp: module type of SExpFunc.Make(Symbol),
11
+
): {
2
12
include Signatures.TERM_VIEW with module Term := SExp
3
13
} => {
4
14
type props = {term: SExp.t, scope: array<string>}
···
50
60
</span>
51
61
| Var({idx}) => viewVar({idx, scope})
52
62
| Symbol(name) =>
53
-
<span className="term-const"> {React.string(name->SExp.Symbol.prettyPrint(~scope))} </span>
63
+
<span className="term-const">
64
+
<SymbolView name scope />
65
+
</span>
54
66
| Schematic({schematic: s, allowed: vs}) =>
55
67
<span className="term-schematic">
56
68
{React.string("?")}
-27
src/StringTerm.res
-27
src/StringTerm.res
···
503
503
acc.contents->Result.map(r => (r, str->String.sliceToEnd(~start=pos.contents)))
504
504
}
505
505
506
-
let toSExp = t => {
507
-
let convertPiece = p =>
508
-
switch p {
509
-
| String(s) => {
510
-
// FIX: dirty as fuck
511
-
let (s, _) = SExp.Symbol.parse(s, ~scope=[])->Result.getExn
512
-
SExp.Symbol(s)
513
-
}
514
-
| Var({idx}) => SExp.Var({idx: idx})
515
-
| Schematic({schematic, allowed}) => SExp.Schematic({schematic, allowed})
516
-
| Ghost => SExp.ghostTerm
517
-
}
518
-
switch Array.length(t) {
519
-
| 1 => convertPiece(t[0]->Option.getExn)
520
-
| _ => SExp.Compound({subexps: Array.map(t, convertPiece)})
521
-
}
522
-
}
523
-
524
-
let rec fromSExp = (t: SExp.t) =>
525
-
switch t {
526
-
| SExp.Symbol(name) => [String(SExp.Symbol.prettyPrint(name, ~scope=[]))]
527
-
| SExp.Schematic({schematic, allowed}) => [Schematic({schematic, allowed})]
528
-
| SExp.Var({idx}) => [Var({idx: idx})]
529
-
| SExp.Compound({subexps}) => subexps->Array.flatMap(fromSExp)
530
-
| SExp.Ghost => [Ghost]
531
-
}
532
-
533
506
let ghostTerm = [Ghost]
+16
-1
src/StringTermJView.res
+16
-1
src/StringTermJView.res
···
1
+
open StringTermJudgment
2
+
3
+
module StringSymbolView: SExpViewFunc.SYMBOL_VIEW with module Symbol := StringSymbol = {
4
+
type props = {name: StringSymbol.t, scope: array<string>}
5
+
let make = ({name, scope}: props) =>
6
+
switch name {
7
+
| StringS(term) => <StringTermView term scope />
8
+
| ConstS(name) => <SExpView.ConstSymbolView name scope />
9
+
}
10
+
}
11
+
1
12
module TermView = StringTermView
2
13
type props = {
3
14
judgment: StringTermJudgment.t,
4
15
scope: array<string>,
5
16
}
6
-
module SExpView = SExpViewFunc.Make(StringTermJudgment.StringSymbol, StringTermJudgment.StringSExp)
17
+
module SExpView = SExpViewFunc.Make(
18
+
StringTermJudgment.StringSymbol,
19
+
StringSymbolView,
20
+
StringTermJudgment.StringSExp,
21
+
)
7
22
let make = ({judgment: (term, j), scope}) => {
8
23
<span className="term-compound">
9
24
<StringTermView term scope />