the next generation of the in-browser educational proof assistant
1open Signatures
2open MethodView
3
4@send external closest: ({..}, string) => Nullable.t<Dom.element> = "closest"
5@send external focus: {..} => unit = "focus"
6
7module Make = (
8 Term: TERM,
9 Judgment: JUDGMENT with module Term := Term,
10 JudgmentView: JUDGMENT_VIEW with module Term := Term and module Judgment := Judgment,
11 MethodView: METHOD_VIEW with module Term := Term and module Judgment := Judgment,
12) => {
13 module Rule = Rule.Make(Term, Judgment)
14 module ScopeView = ScopeView.Make(Term, JudgmentView.TermView)
15 module Proof = Proof.Make(Term, Judgment, MethodView.Method)
16 module Results = Method.MethodResults(Term)
17 module ResultsView = {
18 type menuState<'a> = {
19 history: list<array<Results.t<MethodView.Method.t<Proof.checked>>>>, // Stack of previous menus
20 current: array<Results.t<MethodView.Method.t<Proof.checked>>>, // What is currently visible
21 }
22 type props = {
23 initialNodes: array<Results.t<MethodView.Method.t<Proof.checked>>>,
24 onApply: (MethodView.Method.t<Proof.checked>, Term.subst) => (),
25 onBlur: (ReactEvent.Focus.t) => ()
26 }
27 @react.componentWithProps
28 let make = (props: props) => {
29 let (state, setState) = React.useState(_ => {
30 history: list{},
31 current: props.initialNodes,
32 })
33
34 let goBack = _ => {
35 setState(prev => {
36 switch prev.history {
37 | list{parent, ...rest} => {current: parent, history: rest}
38 | list{} => prev // Already at the root
39 }
40 })
41 }
42
43 let drillDown = (newNodes: array<Results.t<'a>>) => {
44 setState(prev => {
45 history: list{prev.current, ...prev.history},
46 current: newNodes,
47 })
48 }
49
50 <div className="drill-down-container">
51 {state.history != list{}
52 ? <button tabIndex=0 onBlur={props.onBlur} onClick={goBack} className="back-button"> {React.string("← Back")} </button>
53 : React.null}
54
55 <div className="menu-options">
56 {state.current->Array.mapWithIndex((node, i) => {
57 switch node {
58 | Action(label, nextTree, subst) =>
59 <button tabIndex=0 onBlur={props.onBlur} key={label ++ i->Int.toString} onClick={_ => props.onApply(nextTree, subst)}>
60 {React.string(label ++ "")}
61 </button>
62
63 | Group(label, children) =>
64 <button tabIndex=0 onBlur={props.onBlur} key={label ++ i->Int.toString} onClick={_ => drillDown(children)}>
65 {React.string(label ++ " →")}
66 </button>
67
68 | Delay(label, getChildren) =>
69 <button tabIndex=0 onBlur={props.onBlur} key={label ++ i->Int.toString} onClick={_ => drillDown(getChildren())}>
70 {React.string(label ++ " ...")}
71 </button>
72 }
73 })->React.array}
74 </div>
75 </div>
76 }
77 }
78
79
80 type props = {
81 proof: Proof.checked,
82 scope: array<Term.meta>,
83 ruleStyle: RuleView.style,
84 gen: Term.gen,
85 onChange: (Proof.checked, Term.subst) => unit,
86 }
87 module RuleView = RuleView.Make(Term, Judgment, JudgmentView)
88 @react.componentWithProps
89 let rec make = (props: props) => {
90 let {sidebarRef} = React.useContext(SidebarContext.context)
91 let (isFocused, setFocused) = React.useState(() => false)
92
93 let onBlur = e => {
94 let leavingProof =
95 ReactEvent.Focus.relatedTarget(e)
96 ->Option.flatMap(el => el->closest(".sidebar")->Nullable.toOption)
97 ->Option.isNone
98 if leavingProof {
99 setFocused(_ => false)
100 }
101 }
102 switch props.proof {
103 | Proof.Checked({fixes, assumptions, method, rule}) => {
104 let scope = Array.concat(fixes, props.scope)
105 <>
106 <ScopeView scope=fixes />
107 <ul className="proof-assumptions">
108 {Belt.Array.zipBy(assumptions, rule.premises, (n, r) => {
109 <li key={n}>
110 <RuleView rule=r style=props.ruleStyle scope> {React.string(n)} </RuleView>
111 </li>
112 })->React.array}
113 </ul>
114 <div className="proof-show">
115 <JudgmentView judgment={rule.conclusion} scope />
116 {switch method {
117 | Goal(options) =>
118 let portal = switch sidebarRef.current->Nullable.toOption {
119 | None => React.null
120 | Some(node) =>
121 let res = options(props.gen);
122 Portal.createPortal(
123 <>
124 {
125 <ResultsView initialNodes=res
126 onBlur
127 onApply={(opt,subst)=>
128 props.onChange(
129 Proof.Checked({fixes, assumptions, method: Do(opt), rule}),
130 subst,
131 )}
132 ></ResultsView>
133 }
134 </>,
135 node,
136 )
137 }
138 <div
139 className="proof-goal"
140 tabIndex=0
141 onBlur
142 onFocus={e => {
143 setFocused(_ => true)
144 ReactEvent.Focus.stopPropagation(e)
145 }}
146 >
147 {if isFocused {
148 <>
149 <span className="button-icon button-icon-blue typcn typcn-location" />
150 {portal}
151 </>
152 } else {
153 <span className="button-icon button-icon-blue typcn typcn-location-outline" />
154 }}
155 </div>
156 | Do(method) =>
157 React.createElement(
158 MethodView.make(p =>
159 make({
160 proof: p["proof"],
161 scope: p["scope"],
162 ruleStyle: p["ruleStyle"],
163 gen: p["gen"],
164 onChange: p["onChange"],
165 })
166 ),
167 {
168 method,
169 scope,
170 ruleStyle: props.ruleStyle,
171 gen: props.gen,
172 onChange: (newm, subst) => {
173 props.onChange(
174 Proof.Checked({fixes, assumptions, method: Do(newm), rule}),
175 subst,
176 )
177 },
178 },
179 )
180 }}
181 </div>
182 </>
183 }
184 | Proof.ProofError({raw: _, rule: _, msg}) => <div className="error"> {React.string(msg)} </div>
185 }
186 }
187}