the next generation of the in-browser educational proof assistant
1open Signatures
2open Method
3open HOTermMethod
4module type METHOD_VIEW = {
5 module Term: TERM
6 module Judgment: JUDGMENT with module Term := Term
7 module Method: PROOF_METHOD with module Term := Term and module Judgment := Judgment
8 type props<'a> = {
9 method: Method.t<'a>,
10 scope: array<Term.meta>,
11 ruleStyle: RuleView.style,
12 gen: Term.gen,
13 onChange: (Method.t<'a>, Term.subst) => unit,
14 }
15 type srProps<'a> = {
16 "proof": 'a,
17 "scope": array<Term.meta>,
18 "ruleStyle": RuleView.style,
19 "gen": Term.gen,
20 "onChange": ('a, Term.subst) => unit,
21 }
22 let make: (srProps<'a> => React.element) => props<'a> => React.element
23}
24
25module DerivationView = (Term: TERM, Judgment: JUDGMENT with module Term := Term) => {
26 module Method = Derivation(Term, Judgment)
27 type props<'a> = {
28 method: Method.t<'a>,
29 scope: array<Term.meta>,
30 ruleStyle: RuleView.style,
31 gen: Term.gen,
32 onChange: (Method.t<'a>, Term.subst) => unit,
33 }
34 type srProps<'a> = {
35 "proof": 'a,
36 "scope": array<Term.meta>,
37 "ruleStyle": RuleView.style,
38 "gen": Term.gen,
39 "onChange": ('a, Term.subst) => unit,
40 }
41 let make = (subRender: srProps<'a> => React.element) =>
42 props => {
43 <div>
44 <b> {React.string("by ")} </b>
45 {React.string(props.method.ruleName)}
46 <ul>
47 {props.method.subgoals
48 ->Array.mapWithIndex((sg, i) => {
49 <li key={String.make(i)}>
50 {React.createElement(
51 subRender,
52 {
53 "proof": sg,
54 "scope": props.scope,
55 "ruleStyle": props.ruleStyle,
56 "gen": props.gen,
57 "onChange": (newa, subst: Term.subst) =>
58 props.onChange(props.method->Method.updateAtKey(i, _ => newa), subst),
59 },
60 )}
61 </li>
62 })
63 ->React.array}
64 </ul>
65 </div>
66 }
67}
68
69module EliminationView = (Term: TERM, Judgment: JUDGMENT with module Term := Term) => {
70 module Method = Elimination(Term, Judgment)
71 type props<'a> = {
72 method: Method.t<'a>,
73 scope: array<Term.meta>,
74 ruleStyle: RuleView.style,
75 gen: Term.gen,
76 onChange: (Method.t<'a>, Term.subst) => unit,
77 }
78 type srProps<'a> = {
79 "proof": 'a,
80 "scope": array<Term.meta>,
81 "ruleStyle": RuleView.style,
82 "gen": Term.gen,
83 "onChange": ('a, Term.subst) => unit,
84 }
85 let make = (subRender: srProps<'a> => React.element) =>
86 props => {
87 <div>
88 <b> {React.string("elim ")} </b>
89 {React.string(`${props.method.ruleName} ${props.method.elimName}`)}
90 <ul>
91 {props.method.subgoals
92 ->Array.mapWithIndex((sg, i) => {
93 <li key={String.make(i)}>
94 {React.createElement(
95 subRender,
96 {
97 "proof": sg,
98 "scope": props.scope,
99 "ruleStyle": props.ruleStyle,
100 "gen": props.gen,
101 "onChange": (newa, subst: Term.subst) =>
102 props.onChange(props.method->Method.updateAtKey(i, _ => newa), subst),
103 },
104 )}
105 </li>
106 })
107 ->React.array}
108 </ul>
109 </div>
110 }
111}
112
113module LemmaView = (
114 Term: TERM,
115 Judgment: JUDGMENT with module Term := Term,
116 JudgmentView: JUDGMENT_VIEW with module Term := Term and module Judgment := Judgment,
117) => {
118 module Method = Lemma(Term, Judgment)
119 type props<'a> = {
120 method: Method.t<'a>,
121 scope: array<Term.meta>,
122 ruleStyle: RuleView.style,
123 gen: Term.gen,
124 onChange: (Method.t<'a>, Term.subst) => unit,
125 }
126 type srProps<'a> = {
127 "proof": 'a,
128 "scope": array<Term.meta>,
129 "ruleStyle": RuleView.style,
130 "gen": Term.gen,
131 "onChange": ('a, Term.subst) => unit,
132 }
133 module RuleView = RuleView.Make(Term, Judgment, JudgmentView)
134 let make = (subRender: srProps<'a> => React.element) =>
135 props => {
136 <div>
137 <b> {React.string("have ")} </b>
138 <RuleView rule={props.method.rule} scope={props.scope} style={props.ruleStyle}>
139 {React.null}
140 </RuleView>
141 {React.createElement(
142 subRender,
143 {
144 "proof": props.method.proof,
145 "scope": props.scope,
146 "ruleStyle": props.ruleStyle,
147 "gen": props.gen,
148 "onChange": (proof, subst) => {props.onChange({...props.method, proof}, subst)},
149 },
150 )}
151 {React.createElement(
152 subRender,
153 {
154 "proof": props.method.show,
155 "scope": props.scope,
156 "ruleStyle": props.ruleStyle,
157 "gen": props.gen,
158 "onChange": (show, subst) => {props.onChange({...props.method, show}, subst)},
159 },
160 )}
161 </div>
162 }
163}
164
165module RewriteView = (Judgment: JUDGMENT with module Term := HOTerm and type t = HOTerm.t) => {
166 module Method = Rewrite(Judgment)
167 type props<'a> = {
168 method: Method.t<'a>,
169 scope: array<HOTerm.meta>,
170 ruleStyle: RuleView.style,
171 gen: HOTerm.gen,
172 onChange: (Method.t<'a>, HOTerm.subst) => unit,
173 }
174 type srProps<'a> = {
175 "proof": 'a,
176 "scope": array<HOTerm.meta>,
177 "ruleStyle": RuleView.style,
178 "gen": HOTerm.gen,
179 "onChange": ('a, HOTerm.subst) => unit,
180 }
181 let make = (subRender: srProps<'a> => React.element) =>
182 props => {
183 <div>
184 <b> {React.string("rewrite ")} </b>
185 {React.string(props.method.equalityName)}
186 <ul>
187 <li>
188 {React.createElement(
189 subRender,
190 {
191 "proof": props.method.subgoal,
192 "scope": props.scope,
193 "ruleStyle": props.ruleStyle,
194 "gen": props.gen,
195 "onChange": (subgoal, subst: HOTerm.subst) =>
196 props.onChange({...props.method, subgoal}, subst),
197 },
198 )}
199 </li>
200 </ul>
201 </div>
202 }
203}
204
205module RewriteReverseView = (
206 Judgment: JUDGMENT with module Term := HOTerm and type t = HOTerm.t,
207) => {
208 module Method = RewriteReverse(Judgment)
209 type props<'a> = {
210 method: Method.t<'a>,
211 scope: array<HOTerm.meta>,
212 ruleStyle: RuleView.style,
213 gen: HOTerm.gen,
214 onChange: (Method.t<'a>, HOTerm.subst) => unit,
215 }
216 type srProps<'a> = {
217 "proof": 'a,
218 "scope": array<HOTerm.meta>,
219 "ruleStyle": RuleView.style,
220 "gen": HOTerm.gen,
221 "onChange": ('a, HOTerm.subst) => unit,
222 }
223 let make = (subRender: srProps<'a> => React.element) =>
224 props => {
225 <div>
226 <b> {React.string("rewrite_reverse ")} </b>
227 {React.string(props.method.equalityName)}
228 <ul>
229 <li>
230 {React.createElement(
231 subRender,
232 {
233 "proof": props.method.subgoal,
234 "scope": props.scope,
235 "ruleStyle": props.ruleStyle,
236 "gen": props.gen,
237 "onChange": (subgoal, subst: HOTerm.subst) =>
238 props.onChange({...props.method, subgoal}, subst),
239 },
240 )}
241 </li>
242 </ul>
243 </div>
244 }
245}
246
247module ConstructorNeqView = (
248 Judgment: JUDGMENT with module Term := HOTerm and type t = HOTerm.t,
249) => {
250 module Method = ConstructorNeq(Judgment)
251 type props<'a> = {
252 method: Method.t<'a>,
253 scope: array<HOTerm.meta>,
254 ruleStyle: RuleView.style,
255 gen: HOTerm.gen,
256 onChange: (Method.t<'a>, HOTerm.subst) => unit,
257 }
258 type srProps<'a> = {
259 "proof": 'a,
260 "scope": array<HOTerm.meta>,
261 "ruleStyle": RuleView.style,
262 "gen": HOTerm.gen,
263 "onChange": ('a, HOTerm.subst) => unit,
264 }
265 let make = (_subRender: srProps<'a> => React.element) =>
266 _props => {
267 <div>
268 <b> {React.string("constructor_neq")} </b>
269 </div>
270 }
271}
272
273module ConstructorInjView = (
274 Judgment: JUDGMENT with module Term := HOTerm and type t = HOTerm.t,
275) => {
276 module Method = ConstructorInj(Judgment)
277 type props<'a> = {
278 method: Method.t<'a>,
279 scope: array<HOTerm.meta>,
280 ruleStyle: RuleView.style,
281 gen: HOTerm.gen,
282 onChange: (Method.t<'a>, HOTerm.subst) => unit,
283 }
284 type srProps<'a> = {
285 "proof": 'a,
286 "scope": array<HOTerm.meta>,
287 "ruleStyle": RuleView.style,
288 "gen": HOTerm.gen,
289 "onChange": ('a, HOTerm.subst) => unit,
290 }
291 let make = (_subRender: srProps<'a> => React.element) =>
292 props => {
293 <div>
294 <b>
295 {React.string(
296 `constructor_inj ${props.method.source} ${Int.toString(props.method.argIndex)}`,
297 )}
298 </b>
299 </div>
300 }
301}
302
303module CombineMethodView = (
304 Term: TERM,
305 Judgment: JUDGMENT with module Term := Term,
306 Method1View: METHOD_VIEW with module Term := Term and module Judgment := Judgment,
307 Method2View: METHOD_VIEW
308 with module Term := Term
309 and module Judgment := Judgment
310 and type srProps<'a> = Method1View.srProps<'a>,
311) => {
312 module Method = Combine(Term, Judgment, Method1View.Method, Method2View.Method)
313 type props<'a> = {
314 method: Method.t<'a>,
315 scope: array<Term.meta>,
316 ruleStyle: RuleView.style,
317 gen: Term.gen,
318 onChange: (Method.t<'a>, Term.subst) => unit,
319 }
320 type srProps<'a> = Method1View.srProps<'a>
321 let make = (subrender: srProps<'a> => React.element) =>
322 props => {
323 switch props.method {
324 | First(m) =>
325 Method1View.make(subrender)({
326 method: m,
327 scope: props.scope,
328 ruleStyle: props.ruleStyle,
329 gen: props.gen,
330 onChange: (n, s) => props.onChange(First(n), s),
331 })
332 | Second(m) =>
333 Method2View.make(subrender)({
334 method: m,
335 scope: props.scope,
336 ruleStyle: props.ruleStyle,
337 gen: props.gen,
338 onChange: (n, s) => props.onChange(Second(n), s),
339 })
340 }
341 }
342}