Something went wrong. Try again.
the next generation of the in-browser educational proof assistant
Something went wrong. Try again.
2.6 kB · 90 lines
at main
12345678910111213141516171819202122232425262728293031323334353637383940414243444546474849505152535455565758596061626364656667686970717273747576777879808182838485868788899091module type ATOM_VIEW = AtomDef.ATOM_VIEW
module Make = ( Atom: AtomDef.ATOM, AtomView: ATOM_VIEW with module Atom := Atom, SExp: module type of SExp.Make(Atom),): { include Signatures.TERM_VIEW with module Term := SExp} => { type props = {term: SExp.t, scope: array<string>} open Util type idx_props = {idx: int, scope: array<string>} let viewVar = (props: idx_props) => switch props.scope[props.idx] { | Some(n) if Array.indexOf(props.scope, n) == props.idx => <span className="term-metavar"> {React.string(n)} </span> | _ => <span className="term-metavar-unnamed"> {React.string("\\")} {React.int(props.idx)} </span> }
let makeMeta = (str: string) => <span className="rule-binder"> {React.string(str)} {React.string(".")} </span>
let parenthesise = f => [ <span className="symbol" key={"-1"}> {React.string("(")} </span>, ...f, <span className="symbol" key={"-2"}> {React.string(")")} </span>, ]
let intersperse = a => a->Array.flatMapWithIndex((e, i) => if i == 0 { [e] } else { [React.string(" "), e] } )
module Inner = { @react.component let rec make = (~term: SExp.t, ~scope: array<string>, ~parens: bool=true) => switch term { | Compound({subexps: bits}) => <span className="term-compound"> {bits ->Array.mapWithIndex((t, i) => <React.Fragment key={i->Int.toString}> {React.createElement(React.component(make), {term: t, scope, parens: true})} </React.Fragment> ) ->intersperse ->(a => if parens { parenthesise(a) } else { a }) ->React.array} </span> | Var({idx}) => viewVar({idx, scope}) | Atom(atom) => <span className="term-const"> <AtomView atom scope /> </span> | Schematic({schematic: s, allowed: vs}) => <span className="term-schematic"> {React.string("?")} {React.int(s)} <span className="term-schematic-telescope"> {vs ->Array.mapWithIndex((v, i) => React.createElement(React.component(viewVar), withKey({idx: v, scope}, i)) ) ->intersperse ->parenthesise ->React.array} </span> </span> } } @react.componentWithProps let make = ({term, scope}) => <Inner term scope parens=false />}