the next generation of the in-browser educational proof assistant
1open Util
2type idx_props = {idx: int, scope: array<string>}
3let viewVar = (props: idx_props) =>
4 switch props.scope[props.idx] {
5 | Some(n) if Array.indexOf(props.scope, n) == props.idx =>
6 <span className="term-metavar"> {React.string(n)} </span>
7 | _ =>
8 <span className="term-metavar-unnamed">
9 {React.string("\\")}
10 {React.int(props.idx)}
11 </span>
12 }
13
14let makeMeta = (str: string) =>
15 <span className="rule-binder">
16 {React.string(str)}
17 {React.string(".")}
18 </span>
19
20let parenthesise = f =>
21 [
22 <span className="symbol" key={"-1"}> {React.string("(")} </span>,
23 ...f,
24 <span className="symbol" key={"-2"}> {React.string(")")} </span>,
25 ]
26
27let intersperse = a =>
28 a->Array.flatMapWithIndex((e, i) =>
29 if i == 0 {
30 [e]
31 } else {
32 [React.string(" "), e]
33 }
34 )
35type props1 = {term: HOTerm.t, scope: array<string>, brackets: bool}
36@react.componentWithProps
37let rec make1 = ({term, scope, brackets}) =>
38 switch term {
39 | Var({idx}) => viewVar({idx, scope})
40 | Symbol({name: s}) => <span className="term-const"> {React.string(s)} </span>
41 | Schematic({schematic: s}) =>
42 <span className="term-schematic">
43 {React.string("?")}
44 {React.int(s)}
45 </span>
46 | App(_) =>
47 switch HOTerm.strip(term) {
48 | (Symbol({name: "="}), args) if Array.length(args) == 2 =>
49 <span className="term-equality">
50 {React.createElement(make1, {term: args->Array.getUnsafe(0), scope, brackets: true})}
51 {React.string("=")}
52 {React.createElement(make1, {term: args->Array.getUnsafe(1), scope, brackets: true})}
53 </span>
54 | (func, args) =>
55 let xs = Array.concat([func], args)
56 let a =
57 <span className="term-app">
58 {xs
59 ->Array.mapWithIndex((t, i) =>
60 React.createElement(make1, withKey({term: t, scope, brackets: true}, i))
61 )
62 ->intersperse
63 ->React.array}
64 </span>
65 if brackets {
66 [a]->parenthesise->React.array
67 } else {
68 a
69 }
70 }
71 | Lam({name, body}) => {
72 let newScope = Array.concat([name], scope)
73 <span className="term-lambda">
74 {React.string(name)}
75 {React.createElement(make1, {term: body, scope: newScope, brackets: false})}
76 </span>
77 }
78 | Unallowed => <p> {React.string("Internal error: unallowed")} </p>
79 }
80type props = {term: HOTerm.t, scope: array<string>}
81@react.componentWithProps
82let make = ({term, scope}) => make1({term, scope, brackets: false})