the next generation of the in-browser educational proof assistant
1module type ATOM_VIEW = AtomDef.ATOM_VIEW
2
3module Make = (
4 Atom: AtomDef.ATOM,
5 AtomView: ATOM_VIEW with module Atom := Atom,
6 SExp: module type of SExp.Make(Atom),
7): {
8 include Signatures.TERM_VIEW with module Term := SExp
9} => {
10 type props = {term: SExp.t, scope: array<string>}
11 open Util
12 type idx_props = {idx: int, scope: array<string>}
13 let viewVar = (props: idx_props) =>
14 switch props.scope[props.idx] {
15 | Some(n) if Array.indexOf(props.scope, n) == props.idx =>
16 <span className="term-metavar"> {React.string(n)} </span>
17 | _ =>
18 <span className="term-metavar-unnamed">
19 {React.string("\\")}
20 {React.int(props.idx)}
21 </span>
22 }
23
24 let makeMeta = (str: string) =>
25 <span className="rule-binder">
26 {React.string(str)}
27 {React.string(".")}
28 </span>
29
30 let parenthesise = f =>
31 [
32 <span className="symbol" key={"-1"}> {React.string("(")} </span>,
33 ...f,
34 <span className="symbol" key={"-2"}> {React.string(")")} </span>,
35 ]
36
37 let intersperse = a =>
38 a->Array.flatMapWithIndex((e, i) =>
39 if i == 0 {
40 [e]
41 } else {
42 [React.string(" "), e]
43 }
44 )
45
46 @react.componentWithProps
47 let rec make = ({term, scope}) =>
48 switch term {
49 | Compound({subexps: bits}) =>
50 <span className="term-compound">
51 {bits
52 ->Array.mapWithIndex((t, i) => React.createElement(make, withKey({term: t, scope}, i)))
53 ->intersperse
54 ->parenthesise
55 ->React.array}
56 </span>
57 | Var({idx}) => viewVar({idx, scope})
58 | Atom(name) =>
59 <span className="term-const">
60 <AtomView name scope />
61 </span>
62 | Schematic({schematic: s, allowed: vs}) =>
63 <span className="term-schematic">
64 {React.string("?")}
65 {React.int(s)}
66 <span className="term-schematic-telescope">
67 {vs
68 ->Array.mapWithIndex((v, i) => React.createElement(viewVar, withKey({idx: v, scope}, i)))
69 ->intersperse
70 ->parenthesise
71 ->React.array}
72 </span>
73 </span>
74 }
75}