Something went wrong. Try again.
the next generation of the in-browser educational proof assistant
Something went wrong. Try again.
7.0 kB · 210 lines
at main
123456789101112131415161718192021222324252627282930313233343536373839404142434445464748495051525354555657585960616263646566676869707172737475767778798081828384858687888990919293949596979899100101102103104105106107108109110111112113114115116117118119120121122123124125126127128129130131132133134135136137138139140141142143144145146147148149150151152153154155156157158159160161162163164165166167168169170171172173174175176177178179180181182183184185186187188189190191192193194195196197198199200201202203204205206207208209210211open Signaturesopen MethodView
@send external closest: ({..}, string) => Nullable.t<Dom.element> = "closest"@send external focus: {..} => unit = "focus"
module Make = ( Term: TERM, Judgment: JUDGMENT with module Term := Term, JudgmentView: JUDGMENT_VIEW with module Term := Term and module Judgment := Judgment, MethodView: METHOD_VIEW with module Term := Term and module Judgment := Judgment,) => { module Rule = Rule.Make(Term, Judgment) module ScopeView = ScopeView.Make(Term, JudgmentView.TermView) module Proof = Proof.Make(Term, Judgment, MethodView.Method) module Results = Method.MethodResults(Term) module ResultsView = { type menuState<'a> = { history: list<array<Results.t<MethodView.Method.t<Proof.checked>>>>, // Stack of previous menus current: array<Results.t<MethodView.Method.t<Proof.checked>>>, // What is currently visible } type props = { initialNodes: array<Results.t<MethodView.Method.t<Proof.checked>>>, onApply: (MethodView.Method.t<Proof.checked>, Term.subst) => unit, onBlur: ReactEvent.Focus.t => unit, } @react.componentWithProps let make = (props: props) => { let (state, setState) = React.useState(_ => { history: list{}, current: props.initialNodes, })
let goBack = _ => { setState(prev => { switch prev.history { | list{parent, ...rest} => {current: parent, history: rest} | list{} => prev // Already at the root } }) }
let drillDown = (newNodes: array<Results.t<'a>>) => { setState(prev => { history: list{prev.current, ...prev.history}, current: newNodes, }) }
<div className="drill-down-container"> {state.history != list{} ? <button tabIndex=0 onBlur={props.onBlur} onClick={goBack} className="back-button"> {React.string("← Back")} </button> : React.null}
<div className="menu-options"> {state.current ->Array.mapWithIndex((node, i) => { switch node { | Action(label, nextTree, subst) => <button tabIndex=0 onBlur={props.onBlur} key={label ++ i->Int.toString} onClick={_ => props.onApply(nextTree, subst)} > {React.string(label ++ "")} </button>
| Group(label, children) => <button tabIndex=0 onBlur={props.onBlur} key={label ++ i->Int.toString} onClick={_ => drillDown(children)} > {React.string(label ++ " →")} </button>
| Delay(label, getChildren) => <button tabIndex=0 onBlur={props.onBlur} key={label ++ i->Int.toString} onClick={_ => drillDown(getChildren())} > {React.string(label ++ " ...")} </button> } }) ->React.array} </div> </div> } }
type props = { proof: Proof.checked, scope: array<Term.meta>, ruleStyle: RuleView.style, gen: Term.gen, onChange: (Proof.checked, Term.subst) => unit, } module RuleView = RuleView.Make(Term, Judgment, JudgmentView) @react.componentWithProps let rec make = (props: props) => { let {sidebarRef} = React.useContext(SidebarContext.context) let (isFocused, setFocused) = React.useState(() => false)
let onBlur = e => { let leavingProof = ReactEvent.Focus.relatedTarget(e) ->Option.flatMap(el => el->closest(".sidebar")->Nullable.toOption) ->Option.isNone if leavingProof { setFocused(_ => false) } } switch props.proof { | Proof.Checked({fixes, assumptions, method, rule}) => { let scope = Array.concat(fixes, props.scope) <> <ScopeView scope=fixes /> <ul className="proof-assumptions"> {Belt.Array.zipBy(assumptions, rule.premises, (n, r) => { <li key={n}> <RuleView rule=r style=props.ruleStyle scope> {React.string(n)} </RuleView> </li> })->React.array} </ul> <div className="proof-show"> <JudgmentView judgment={rule.conclusion} scope /> {switch method { | Goal(options) => let portal = switch sidebarRef.current->Nullable.toOption { | None => React.null | Some(node) => let res = options(props.gen) Portal.createPortal( <> {<ResultsView initialNodes=res onBlur onApply={(opt, subst) => props.onChange( Proof.Checked({fixes, assumptions, method: Do(opt), rule}), subst, )} > </ResultsView>} </>, node, ) } <div className="proof-goal" tabIndex=0 onBlur onFocus={e => { setFocused(_ => true) ReactEvent.Focus.stopPropagation(e) }} > {if isFocused { <> <span className="button-icon button-icon-blue typcn typcn-location" /> {portal} </> } else { <span className="button-icon button-icon-blue typcn typcn-location-outline" /> }} </div> | Do(method) => React.createElement( React.component( MethodView.make(p => React.createElement( React.component(make), { proof: p["proof"], scope: p["scope"], ruleStyle: p["ruleStyle"], gen: p["gen"], onChange: p["onChange"], }, ) ), ), { method, scope, ruleStyle: props.ruleStyle, gen: props.gen, onChange: (newm, subst) => { props.onChange( Proof.Checked({fixes, assumptions, method: Do(newm), rule}), subst, ) }, }, ) }} </div> </> } | Proof.ProofError({raw: _, rule: _, msg}) => <div className="error"> {React.string(msg)} </div> } }}