the next generation of the in-browser educational proof assistant
add HOTermView
+62
+6
src/HOTermJView.res
+6
src/HOTermJView.res
+1
src/HOTermJView.resi
+1
src/HOTermJView.resi
···
1
+
include Signatures.JUDGMENT_VIEW with module Term := HOTerm and module Judgment := HOTerm
+54
src/HOTermView.res
+54
src/HOTermView.res
···
1
+
type props = {term: HOTerm.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
+
}
14
+
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
+
| Var({idx}) => viewVar({idx, scope})
41
+
| Symbol({name: s}) => <span className="term-const"> {React.string(s)} </span>
42
+
| Schematic({schematic: s, allowed: vs}) =>
43
+
<span className="term-schematic">
44
+
{React.string("?")}
45
+
{React.int(s)}
46
+
<span className="term-schematic-telescope">
47
+
{vs
48
+
->Array.mapWithIndex((v, i) => React.createElement(viewVar, withKey({idx: v, scope}, i)))
49
+
->intersperse
50
+
->parenthesise
51
+
->React.array}
52
+
</span>
53
+
</span>
54
+
}
+1
src/HOTermView.resi
+1
src/HOTermView.resi
···
1
+
include Signatures.TERM_VIEW with module Term := HOTerm