flams_router_content/checks.rs
1use flams_web_utils::components::{Header, LazySubtree, Leaf, Subtree, Tree};
2use ftml_component_utils::Text;
3use ftml_components::components::content::FtmlViewable;
4use ftml_dom::notations::TermExt;
5use ftml_ontology::terms::{ComponentVar, Term, Variable};
6pub use ftml_solver_trace::results::DocumentCheckResult;
7use ftml_solver_trace::results::{
8 CheckResult, ContentCheckResult, ProofStepCheckResult, ProofStepResult, SymbolCheckResult,
9};
10use ftml_solver_trace::{CheckLog, Displayable};
11use ftml_uris::{DocumentElementUri, DocumentUri, Uri};
12use leptos::math::mrow;
13use leptos::prelude::*;
14
15pub trait ResultExt {
16 fn render(self) -> AnyView;
17}
18impl ResultExt for DocumentCheckResult {
19 fn render(self) -> AnyView {
20 crate::Views::setup_document(
21 DocumentUri::no_doc().clone(),
22 ftml_components::SidebarPosition::None,
23 false,
24 ftml_dom::toc::TocSource::None,
25 move || {
26 let inner = self
27 .checks
28 .into_iter()
29 .map(CheckResult::render)
30 .collect_view();
31 view! {<Tree>{inner}</Tree>}.into_any()
32 },
33 )
34 }
35}
36
37impl ResultExt for CheckResult {
38 fn render(self) -> AnyView {
39 match self {
40 Self::Missing(e) => view! {
41 <Leaf><Text style="color:red;">
42 {do_success(false)}"Module not found: "
43 {e.as_view()}
44 </Text></Leaf>
45 }
46 .into_any(),
47 Self::Variable(v, r) => {
48 let success = do_success(r.success());
49 view! {
50 <Subtree expanded=!r.success()>
51 <Header slot>
52 <b>{success}"Variable "{ftml_dom::utils::math(move || do_variable_uri(v))}</b>
53 </Header>
54 {
55 symbol_result(r)
56 }
57 </Subtree>
58 }
59 .into_any()
60 }
61 Self::Content(c) => match c {
62 ContentCheckResult::Symbol(u, s) => {
63 let success = s.success();
64 let succ = do_success(success);
65 view! {
66 <Subtree expanded=!success>
67 <Header slot>
68 <b>{succ}"Symbol "{u.as_view()}</b>
69 </Header>
70 {
71 symbol_result(s)
72 }
73 </Subtree>
74 }
75 .into_any()
76 }
77 },
78 Self::Proof(uri, checks) => {
79 let success = checks.iter().all(ProofStepResult::success);
80 let succ = do_success(success);
81 view! {
82 <Subtree expanded=!success>
83 <Header slot>
84 <b>{succ}"Proof "{uri.as_view()}</b>
85 </Header>
86 {
87 checks.into_iter().map(proof).collect_view()
88 }
89 </Subtree>
90 }
91 .into_any()
92 }
93 Self::Module { uri, checks } => {
94 let success = checks.iter().all(ContentCheckResult::success);
95 let succ = do_success(success);
96 view! {
97 <Subtree expanded=!success>
98 <Header slot>
99 <b>{succ}"Module "{uri.as_view()}</b>
100 </Header>
101 {
102 checks.into_iter().map(|c| match c {
103 ContentCheckResult::Symbol(u, s) => {
104 let success = s.success();
105 let succ = do_success(success);
106 view! {
107 <Subtree expanded=!success>
108 <Header slot>
109 <b>{succ}"Symbol "{u.as_view()}</b>
110 </Header>
111 {
112 symbol_result(s)
113 }
114 </Subtree>
115 }
116 }
117 }).collect_view()
118 }
119 </Subtree>
120 }
121 .into_any()
122 }
123 Self::Term { uri, inferred, log } => {
124 let success = do_success(inferred.is_some());
125 view! {
126 <Subtree expanded=inferred.is_none()>
127 <Header slot>
128 <b>{success}"Document term "{uri.name().to_string()}</b>
129 </Header>
130 {
131 do_log(log, &mut Vec::new())
132 }
133 </Subtree>
134 }
135 .into_any()
136 }
137 }
138 }
139}
140
141fn proof(r: ProofStepResult) -> impl IntoView {
142 use leptos::either::Either::{Left, Right};
143 let (prefix, var, result) = match r {
144 ProofStepResult::Assumption { var, result } => ("Assumption ", var, result),
145 ProofStepResult::Step { var, result } => ("Step ", var, result),
146 ProofStepResult::Conclusion { var, result } => ("Conclusion ", var, result),
147 ProofStepResult::Subproof { uri, var, results } => {
148 return Right({
149 let success = results.iter().all(ProofStepResult::success);
150 let succ = do_success(success);
151 view! {
152 <Subtree expanded=!success>
153 <Header slot>
154 <b>
155 {succ}
156 {"Subproof "}
157 {var.map(|v| ftml_dom::utils::math(move || do_variable_uri(v)))}
158 </b>
159 </Header>
160 {results.into_iter().map(proof).collect_view()}
161 </Subtree>
162 }
163 });
164 }
165 };
166 let success = result.success();
167 let succ = do_success(success);
168 Left(view! {
169 <Subtree expanded=!success>
170 <Header slot>
171 <b>
172 {succ}
173 {prefix}
174 {var.map(|v| ftml_dom::utils::math(move || do_variable_uri(v)))}
175 </b>
176 </Header>
177 {proofstep_result(result)}
178 </Subtree>
179 })
180}
181
182fn proofstep_result(r: ProofStepCheckResult) -> impl IntoView {
183 use leptos::either::Either::{Left, Right};
184 match r {
185 ProofStepCheckResult::GoalOnly { result }
186 | ProofStepCheckResult::Both {
187 inhabitable: result,
188 matches: None,
189 } => Left(do_log(result.log, &mut Vec::new())),
190 ProofStepCheckResult::ProofOnly { log, .. } => Left(do_log(log, &mut Vec::new())),
191 ProofStepCheckResult::Both {
192 inhabitable,
193 matches: Some(r),
194 } => Right(view! {
195 <Subtree expanded=!inhabitable.success>
196 <Header slot><Text bold=true>"Proof goal"</Text></Header>
197 {do_log(inhabitable.log, &mut Vec::new())}
198 </Subtree>
199 <Subtree expanded=!r.success>
200 <Header slot><Text bold=true>"Proof"</Text></Header>
201 {do_log(r.log, &mut Vec::new())}
202 </Subtree>
203 }),
204 }
205}
206
207fn symbol_result(r: SymbolCheckResult) -> impl IntoView {
208 use leptos::either::Either::{Left, Right};
209 match r {
210 SymbolCheckResult::TypeOnly { result }
211 | SymbolCheckResult::Both {
212 inhabitable: result,
213 matches: None,
214 } => Left(do_log(result.log, &mut Vec::new())),
215 SymbolCheckResult::DefiniensOnly { log, .. } => Left(do_log(log, &mut Vec::new())),
216 SymbolCheckResult::Both {
217 inhabitable,
218 matches: Some(r),
219 } => Right(view! {
220 <Subtree expanded=!inhabitable.success>
221 <Header slot><Text bold=true>"Type"</Text></Header>
222 {do_log(inhabitable.log, &mut Vec::new())}
223 </Subtree>
224 <Subtree expanded=!r.success>
225 <Header slot><Text bold=true>"Definiens"</Text></Header>
226 {do_log(r.log, &mut Vec::new())}
227 </Subtree>
228 }),
229 }
230}
231
232#[allow(clippy::too_many_lines)]
233fn do_log(log: CheckLog, ctx: &mut Vec<ComponentVar>) -> AnyView {
234 match log {
235 CheckLog::Comment(s) => {
236 view! {<Leaf><Text style="color:cadetblue" italic=true>{s.into_iter().map(do_displayable).collect_view()}</Text></Leaf>}.into_any()
237 }
238 CheckLog::Emph(s) => view! {<Leaf><Text bold=true>{s.into_iter().map(do_displayable).collect_view()}</Text></Leaf>}.into_any(),
239 CheckLog::Header(s) => view! {<Leaf><Text bold=true>{s.into_iter().map(do_displayable).collect_view()}</Text></Leaf>}.into_any(),
240 CheckLog::Fail(s) => view! {<Leaf><Text style="color:red">{s.into_iter().map(do_displayable).collect_view()}</Text></Leaf>}.into_any(),
241 CheckLog::Rule { header, steps } => {
242 let header = view! {
243 <Text style="color:blueviolet;" italic=true>
244 "Trying rule: "
245 {header.into_iter().map(do_displayable).collect_view()}
246 </Text>
247 };
248 let steps = steps.into_iter().map(|l| do_log(l, ctx)).collect_view();
249 view! {<Subtree expanded=true>
250 <Header slot>{header}</Header>
251 {steps}
252 </Subtree>}
253 .into_any()
254 }
255 CheckLog::Strategy {
256 name,
257 steps,
258 success,
259 } => {
260 let header = view! {
261 <Text>
262 {do_success(success)}
263 <i>"Strategy: "<span style="color:darkgoldenrod;">{name}</span></i>
264 </Text>
265 };
266
267 let mut ctx = ctx.clone();
268 tree(success, header, move || {
269 steps
270 .iter()
271 .map(|l| do_log(l.clone(), &mut ctx))
272 .collect_view()
273 })
274 .into_any()
275 /*
276 let steps = steps.into_iter().map(|l| do_log(l, ctx)).collect_view();
277 view! {<Subtree expanded=!success>
278 <Header slot>{header}</Header>
279 {steps}
280 </Subtree>}
281 .into_any()
282 */
283 }
284 CheckLog::Simplify {
285 term,
286 steps,
287 context,
288 result,
289 } => in_context(ctx, context, move |context, ctx| {
290 let success = result.is_some();
291 let suffix = result.map(|result| {
292 view! {
293 <mo>":"</mo>
294 {do_term(result)}
295 }
296 });
297 let header = view! {
298 <Text>
299 //{do_success(success)}
300 "Simplifying "
301 {ftml_dom::utils::math(move || mrow().child(view!{
302 {context}
303 <mo style="font-weight:bold">"⊢"</mo>
304 {do_term(term)}
305 {suffix}
306 }))}
307 </Text>
308 };
309
310 let mut ctx = ctx.clone();
311 tree(success, header, move || {
312 steps
313 .iter()
314 .map(|l| do_log(l.clone(), &mut ctx))
315 .collect_view()
316 })
317 .into_any()
318 /*
319 let steps = steps.into_iter().map(|l| do_log(l, ctx)).collect_view();
320 view! {<Subtree expanded=!success>
321 <Header slot>{header}</Header>
322 {steps}
323 </Subtree>}
324 .into_any()
325 */
326 }),
327 CheckLog::Proving {
328 term,
329 steps,
330 context,
331 result,
332 } => in_context(ctx, context, move |context, ctx| {
333 let success = result.is_some();
334 let suffix = result.map(|result| {
335 view! {
336 <mo>":"</mo>
337 {do_term(result)}
338 }
339 });
340 let header = view! {
341 <Text>
342 //{do_success(success)}
343 "Proving "
344 {ftml_dom::utils::math(move || mrow().child(view!{
345 {context}
346 <mo style="font-weight:bold">"⊢"</mo>
347 {do_term(term)}
348 {suffix}
349 }))}
350 </Text>
351 };
352
353 let mut ctx = ctx.clone();
354 tree(success, header, move || {
355 steps
356 .iter()
357 .map(|l| do_log(l.clone(), &mut ctx))
358 .collect_view()
359 })
360 .into_any()
361 /*
362 let steps = steps.into_iter().map(|l| do_log(l, ctx)).collect_view();
363 view! {<Subtree expanded=!success>
364 <Header slot>{header}</Header>
365 {steps}
366 </Subtree>}
367 .into_any()
368 */
369 }),
370 CheckLog::Inference {
371 term,
372 steps,
373 context,
374 result,
375 } => in_context(ctx, context, move |context, ctx| {
376 let success = result.is_some();
377 let suffix = result.map(|result| {
378 view! {
379 <mo>":"</mo>
380 {do_term(result)}
381 }
382 });
383 let header = view! {
384 <Text>
385 //{do_success(success)}
386 "Inferring type of "
387 {ftml_dom::utils::math(move || mrow().child(view!{
388 {context}
389 <mo style="font-weight:bold">"⊢"</mo>
390 {do_term(term)}
391 {suffix}
392 }))}
393 </Text>
394 };
395
396 let mut ctx = ctx.clone();
397 tree(success, header, move || {
398 steps
399 .iter()
400 .map(|l| do_log(l.clone(), &mut ctx))
401 .collect_view()
402 })
403 .into_any()
404 /*
405 let steps = steps.into_iter().map(|l| do_log(l, ctx)).collect_view();
406 view! {<Subtree expanded=!success>
407 <Header slot>{header}</Header>
408 {steps}
409 </Subtree>}
410 .into_any()
411 */
412 }),
413 CheckLog::VariableInference {
414 var,
415 steps,
416 context,
417 result,
418 } => in_context(ctx, context, move |context, ctx| {
419 let success = result.is_some();
420 let suffix = result.map(|result| {
421 view! {
422 <mo>":"</mo>
423 {do_term(result)}
424 }
425 });
426 let header = view! {
427 <Text>
428 //{do_success(success)}
429 "Inferring type of "
430 {ftml_dom::utils::math(move || mrow().child(view!{
431 {context}
432 <mo style="font-weight:bold">"⊢"</mo>
433 <mtext style="color:gray">{var.into_string()}</mtext>
434 {suffix}
435 }))}
436 </Text>
437 };
438
439 let mut ctx = ctx.clone();
440 tree(success, header, move || {
441 steps
442 .iter()
443 .map(|l| do_log(l.clone(), &mut ctx))
444 .collect_view()
445 })
446 .into_any()
447 /*
448 let steps = steps.into_iter().map(|l| do_log(l, ctx)).collect_view();
449 view! {<Subtree expanded=!success>
450 <Header slot>{header}</Header>
451 {steps}
452 </Subtree>}
453 .into_any()
454 */
455 }),
456 CheckLog::Inhabitable {
457 term,
458 steps,
459 context,
460 result,
461 } => in_context(ctx, context, move |context, ctx| {
462 let header = view! {
463 <Text>
464 //{do_success(result.unwrap_or(false))}
465 "Checking Inhabitability "
466 {ftml_dom::utils::math(move || mrow().child(view!{
467 {context}
468 <mo style="font-weight:bold">"⊢"</mo>
469 <mtext style="font-weight:bold">"INH"</mtext>
470 <mspace width="5px"/>
471 {do_term(term)}
472 }))}
473 </Text>
474 };
475
476 let mut ctx = ctx.clone();
477 tree(result.unwrap_or(false), header, move || {
478 steps
479 .iter()
480 .map(|l| do_log(l.clone(), &mut ctx))
481 .collect_view()
482 })
483 .into_any()
484 /*
485 let steps = steps.into_iter().map(|l| do_log(l, ctx)).collect_view();
486 view! {<Subtree expanded=result.is_none_or(|b| !b)>
487 <Header slot>{header}</Header>
488 {steps}
489 </Subtree>}
490 .into_any()
491 */
492 }),
493 CheckLog::Universe {
494 term,
495 steps,
496 context,
497 result,
498 } => in_context(ctx, context, move |context, ctx| {
499 let header = view! {
500 <Text>
501 //{do_success(result.unwrap_or(false))}
502 "Checking Universe "
503 {ftml_dom::utils::math(move || mrow().child(view!{
504 {context}
505 <mo style="font-weight:bold">"⊢"</mo>
506 <mtext style="font-weight:bold">"UNIV"</mtext>
507 <mspace width="5px"/>
508 {do_term(term)}
509 }))}
510 </Text>
511 };
512
513 let mut ctx = ctx.clone();
514 tree(result.unwrap_or(false), header, move || {
515 steps
516 .iter()
517 .map(|l| do_log(l.clone(), &mut ctx))
518 .collect_view()
519 })
520 .into_any()
521 /*
522 let steps = steps.into_iter().map(|l| do_log(l, ctx)).collect_view();
523 view! {<Subtree expanded=result.is_none_or(|b| !b)>
524 <Header slot>{header}</Header>
525 {steps}
526 </Subtree>}
527 .into_any()
528 */
529 }),
530 CheckLog::Equality {
531 lhs,
532 rhs,
533 steps,
534 context,
535 result,
536 } => in_context(ctx, context, move |context, ctx| {
537 let header = view! {
538 <Text>
539 //{do_success(result.unwrap_or(false))}
540 "Checking Equality "
541 {ftml_dom::utils::math(move || mrow().child(view!{
542 {context}
543 <mo style="font-weight:bold">"⊢"</mo>
544 {do_term(lhs)}
545 <mo style="font-weight:bold">"=="</mo>
546 {do_term(rhs)}
547 }))}
548 </Text>
549 };
550
551 let mut ctx = ctx.clone();
552 tree(result.unwrap_or(false), header, move || {
553 steps
554 .iter()
555 .map(|l| do_log(l.clone(), &mut ctx))
556 .collect_view()
557 })
558 .into_any()
559 /*
560 let steps = steps.into_iter().map(|l| do_log(l, ctx)).collect_view();
561 view! {<Subtree expanded=result.is_none_or(|b| !b)>
562 <Header slot>{header}</Header>
563 {steps}
564 </Subtree>}
565 .into_any()
566 */
567 }),
568 CheckLog::HasType {
569 tm,
570 tp,
571 steps,
572 context,
573 result,
574 } => in_context(ctx, context, move |context, ctx| {
575 let header = view! {
576 <Text>
577 //{do_success(result.unwrap_or(false))}
578 "Checking Typing "
579 {ftml_dom::utils::math(move || mrow().child(view!{
580 {context}
581 <mo style="font-weight:bold">"⊢"</mo>
582 {do_term(tm)}
583 <mo style="font-weight:bold">":"</mo>
584 {do_term(tp)}
585 }))}
586 </Text>
587 };
588
589 let mut ctx = ctx.clone();
590 tree(result.unwrap_or(false), header, move || {
591 steps
592 .iter()
593 .map(|l| do_log(l.clone(), &mut ctx))
594 .collect_view()
595 })
596 .into_any()
597 /*
598 let steps = steps.into_iter().map(|l| do_log(l, ctx)).collect_view();
599 view! {<Subtree expanded=result.is_none_or(|b| !b)>
600 <Header slot>{header}</Header>
601 {steps}
602 </Subtree>}
603 .into_any()
604 */
605 }),
606 CheckLog::Subtype {
607 sub,
608 sup,
609 steps,
610 context,
611 result,
612 } => in_context(ctx, context, move |context, ctx| {
613 let header = view! {
614 <Text>
615 //{do_success(result.unwrap_or(false))}
616 "Checking Subtyping "
617 {ftml_dom::utils::math(move || mrow().child(view!{
618 {context}
619 <mo style="font-weight:bold">"⊢"</mo>
620 {do_term(sub)}
621 <mo style="font-weight:bold">"<:"</mo>
622 {do_term(sup)}
623 }))}
624 </Text>
625 };
626
627 let mut ctx = ctx.clone();
628 tree(result.unwrap_or(false), header, move || {
629 steps
630 .iter()
631 .map(|l| do_log(l.clone(), &mut ctx))
632 .collect_view()
633 })
634 .into_any()
635 /*
636 let steps = steps.into_iter().map(|l| do_log(l, ctx)).collect_view();
637 view! {<Subtree expanded=true>
638 <Header slot>{header}</Header>
639 {steps}
640 </Subtree>}
641 .into_any()
642 */
643 }),
644 }
645}
646
647/*
648#[allow(clippy::too_many_lines)]
649fn do_log2(log: CheckLog, ctx: &mut Vec<ComponentVar>) -> impl IntoView + use<> + 'static {
650 fn do_log_i(
651 log: CheckLog,
652 ctx: &mut Vec<ComponentVar>,
653 ) -> (impl IntoView + use<> + 'static, bool, Vec<CheckLog>, usize) {
654 use leptos::either::EitherOf13::{A, B, C, D, E, F, G, H, I, J, K, L, M};
655 match log {
656 CheckLog::Comment(s) => (
657 A(view! {<Leaf><Text style="color:cadetblue"><i>{s}</i></Text></Leaf>}),
658 true,
659 Vec::new(),
660 0,
661 ),
662 CheckLog::Emph(s) => (
663 B(view! {<Leaf><Text><b>{s}</b></Text></Leaf>}),
664 true,
665 Vec::new(),
666 0,
667 ),
668 CheckLog::Header(s) => (
669 B(view! {<Leaf><Text><b>{s}</b></Text></Leaf>}),
670 true,
671 Vec::new(),
672 0,
673 ),
674 CheckLog::Fail(s) => (
675 C(view! {<Leaf><Text style="color:red">{s}</Text></Leaf>}),
676 true,
677 Vec::new(),
678 0,
679 ),
680 CheckLog::Rule { header, steps } => (
681 D(view! {
682 <Text><i style="color:blueviolet;">
683 "Trying rule: "
684 {header.into_iter().map(do_displayable).collect_view()}
685 </i></Text>
686 }),
687 true,
688 steps,
689 0,
690 ),
691 CheckLog::Strategy {
692 name,
693 steps,
694 success,
695 } => (
696 E(view! {
697 <Text>
698 {do_success(success)}
699 <i>"Strategy: "<span style="color:darkgoldenrod;">{name}</span></i>
700 </Text>
701 }),
702 !success,
703 steps,
704 0,
705 ),
706 CheckLog::Simplify {
707 term,
708 steps,
709 context,
710 result,
711 } => {
712 let clen = ctx.len();
713 ctx.extend(context);
714 let context = do_context(ctx);
715 let success = result.is_some();
716 let suffix = result.map(|result| {
717 view! {
718 <mo>":"</mo>
719 {do_term(result)}
720 }
721 });
722 (
723 F(view! {
724 <Text>
725 {do_success(success)}
726 "Simplifying "
727 {ftml_dom::utils::math(move || mrow().child(view!{
728 {context}
729 <mo style="font-weight:bold">"⊢"</mo>
730 {do_term(term)}
731 {suffix}
732 }))}
733 </Text>
734 }),
735 !success,
736 steps,
737 clen,
738 )
739 }
740 CheckLog::Proving {
741 term,
742 steps,
743 context,
744 result,
745 } => {
746 let clen = ctx.len();
747 ctx.extend(context);
748 let context = do_context(ctx);
749 let success = result.is_some();
750 let suffix = result.map(|result| {
751 view! {
752 <mo>":"</mo>
753 {do_term(result)}
754 }
755 });
756 (
757 F(view! {
758 <Text>
759 {do_success(success)}
760 "Proving "
761 {ftml_dom::utils::math(move || mrow().child(view!{
762 {context}
763 <mo style="font-weight:bold">"⊢"</mo>
764 {do_term(term)}
765 {suffix}
766 }))}
767 </Text>
768 }),
769 !success,
770 steps,
771 clen,
772 )
773 }
774 CheckLog::Inference {
775 term,
776 steps,
777 context,
778 result,
779 } => {
780 let clen = ctx.len();
781 ctx.extend(context);
782 let context = do_context(ctx);
783 let success = result.is_some();
784 let suffix = result.map(|result| {
785 view! {
786 <mo>":"</mo>
787 {do_term(result)}
788 }
789 });
790 (
791 G(view! {
792 <Text>
793 {do_success(success)}
794 "Inferring type of "
795 {ftml_dom::utils::math(move || mrow().child(view!{
796 {context}
797 <mo style="font-weight:bold">"⊢"</mo>
798 {do_term(term)}
799 {suffix}
800 }))}
801 </Text>
802 }),
803 !success,
804 steps,
805 clen,
806 )
807 }
808 CheckLog::VariableInference {
809 var,
810 steps,
811 context,
812 result,
813 } => {
814 let clen = ctx.len();
815 ctx.extend(context);
816 let context = do_context(ctx);
817 let success = result.is_some();
818 let suffix = result.map(|result| {
819 view! {
820 <mo>":"</mo>
821 {do_term(result)}
822 }
823 });
824 (
825 H(view! {
826 <Text>
827 {do_success(success)}
828 "Inferring type of "
829 {ftml_dom::utils::math(move || mrow().child(view!{
830 {context}
831 <mo style="font-weight:bold">"⊢"</mo>
832 <mtext style="color:gray">{var.into_string()}</mtext>
833 {suffix}
834 }))}
835 </Text>
836 }),
837 !success,
838 steps,
839 clen,
840 )
841 }
842 CheckLog::Inhabitable {
843 term,
844 steps,
845 context,
846 result,
847 } => {
848 let clen = ctx.len();
849 ctx.extend(context);
850 let context = do_context(ctx);
851 let success = result.unwrap_or(false);
852 (
853 I(view! {
854 <Text>
855 {do_success(success)}
856 "Checking Inhabitability "
857 {ftml_dom::utils::math(move || mrow().child(view!{
858 {context}
859 <mo style="font-weight:bold">"⊢"</mo>
860 <mtext style="font-weight:bold">"INH"</mtext>
861 <mspace width="5px"/>
862 {do_term(term)}
863 }))}
864 </Text>
865 }),
866 !success,
867 steps,
868 clen,
869 )
870 }
871 CheckLog::Universe {
872 term,
873 steps,
874 context,
875 result,
876 } => {
877 let clen = ctx.len();
878 ctx.extend(context);
879 let context = do_context(ctx);
880 let success = result.unwrap_or(false);
881 (
882 J(view! {
883 <Text>
884 {do_success(success)}
885 "Checking Universe "
886 {ftml_dom::utils::math(move || mrow().child(view!{
887 {context}
888 <mo style="font-weight:bold">"⊢"</mo>
889 <mtext style="font-weight:bold">"UNIV"</mtext>
890 <mspace width="5px"/>
891 {do_term(term)}
892 }))}
893 </Text>
894 }),
895 !success,
896 steps,
897 clen,
898 )
899 }
900 CheckLog::Equality {
901 lhs,
902 rhs,
903 steps,
904 context,
905 result,
906 } => {
907 let clen = ctx.len();
908 ctx.extend(context);
909 let context = do_context(ctx);
910 let success = result.unwrap_or(false);
911 (
912 K(view! {
913 <Text>
914 {do_success(success)}
915 "Checking Equality "
916 {ftml_dom::utils::math(move || mrow().child(view!{
917 {context}
918 <mo style="font-weight:bold">"⊢"</mo>
919 {do_term(lhs)}
920 <mo style="font-weight:bold">"=="</mo>
921 {do_term(rhs)}
922 }))}
923 </Text>
924 }),
925 !success,
926 steps,
927 clen,
928 )
929 }
930 CheckLog::HasType {
931 tm,
932 tp,
933 steps,
934 context,
935 result,
936 } => {
937 let clen = ctx.len();
938 ctx.extend(context);
939 let context = do_context(ctx);
940 let success = result.unwrap_or(false);
941 (
942 L(view! {
943 <Text>
944 {do_success(success)}
945 "Checking Typing "
946 {ftml_dom::utils::math(move || mrow().child(view!{
947 {context}
948 <mo style="font-weight:bold">"⊢"</mo>
949 {do_term(tm)}
950 <mo style="font-weight:bold">":"</mo>
951 {do_term(tp)}
952 }))}
953 </Text>
954 }),
955 !success,
956 steps,
957 clen,
958 )
959 }
960 CheckLog::Subtype {
961 sub,
962 sup,
963 steps,
964 context,
965 result,
966 } => {
967 let clen = ctx.len();
968 ctx.extend(context);
969 let context = do_context(ctx);
970 let success = result.unwrap_or(false);
971 (
972 M(view! {
973 <Text>
974 {do_success(result.unwrap_or(false))}
975 "Checking Subtyping "
976 {ftml_dom::utils::math(move || mrow().child(view!{
977 {context}
978 <mo style="font-weight:bold">"⊢"</mo>
979 {do_term(sub)}
980 <mo style="font-weight:bold">"<:"</mo>
981 {do_term(sup)}
982 }))}
983 </Text>
984 }),
985 !success,
986 steps,
987 clen,
988 )
989 }
990 }
991 }
992 let mut stack: Vec<(
993 _,
994 _,
995 _,
996 Vec<leptos::either::Either<_, AnyView>>,
997 std::vec::IntoIter<CheckLog>,
998 )> = Vec::new();
999 let mut current = log;
1000 let mut ret = Vec::new();
1001 'outer: loop {
1002 let (v, expanded, steps, vars) = do_log_i(current, ctx);
1003 if steps.is_empty() {
1004 ctx.truncate(vars);
1005 if let Some(mut s) = stack.last_mut() {
1006 let mut v = leptos::either::Either::Left(v);
1007 loop {
1008 s.3.push(v);
1009 if let Some(next) = s.4.next() {
1010 current = next;
1011 break;
1012 }
1013 // SAFETY: we just had Some(last_mut())
1014 let (nv, nexp, nvars, nret, _) = unsafe { stack.pop().unwrap_unchecked() };
1015 ctx.truncate(nvars);
1016 v = leptos::either::Either::Right(
1017 view! {<Subtree expanded=nexp>
1018 <Header slot>{nv}</Header>
1019 {nret}
1020 </Subtree>}
1021 .into_any(),
1022 );
1023 if let Some(ns) = stack.last_mut() {
1024 s = ns;
1025 } else {
1026 ret.push(v);
1027 break 'outer;
1028 }
1029 }
1030 } else {
1031 ret.push(leptos::either::Either::Left(v));
1032 break;
1033 }
1034 } else {
1035 let mut steps = steps.into_iter();
1036 // SAFETY: !steps.is_empty()
1037 current = unsafe { steps.next().unwrap_unchecked() };
1038 stack.push((v, expanded, vars, Vec::new(), steps));
1039 }
1040 }
1041 ret
1042}
1043
1044fn do_context(ctx: &[ComponentVar]) -> impl IntoView + use<> + 'static {
1045 fn component_var(c: &ComponentVar) -> impl IntoView + use<> + 'static {
1046 let head = do_term(Term::Var {
1047 variable: c.var.clone(),
1048 presentation: None,
1049 });
1050 if c.tp.is_none() && c.df.is_none() {
1051 return leptos::either::Either::Left(head);
1052 }
1053 let tp = c.tp.clone().map(|t| view! {<mo>":"</mo>{do_term(t)}});
1054 let df = c.df.clone().map(|t| view! {<mo>":="</mo>{do_term(t)}});
1055 leptos::either::Either::Right(view! {<mrow>{head}{tp}{df}</mrow>})
1056 }
1057 if ctx.is_empty() {
1058 return None;
1059 }
1060 Some({
1061 let mut iter = ctx.iter();
1062 let first = unsafe { iter.next().unwrap_unchecked() };
1063 view! {
1064 <mo style="font-weight:bold">"{"</mo>
1065 {component_var(first)}
1066 {iter.map(|v| view!{<mo>","</mo>{component_var(v)}}).collect_view()}
1067 <mo style="font-weight:bold">"}"</mo>
1068 }
1069 })
1070}
1071 */
1072
1073fn in_context(
1074 current: &mut Vec<ComponentVar>,
1075 new: Box<[ComponentVar]>,
1076 then: impl FnOnce(Option<AnyView>, &mut Vec<ComponentVar>) -> AnyView,
1077) -> AnyView {
1078 fn component_var(c: ComponentVar) -> impl IntoView {
1079 let head = do_term(Term::Var {
1080 variable: c.var,
1081 presentation: None,
1082 });
1083 if c.tp.is_none() && c.df.is_none() {
1084 return leptos::either::Either::Left(head);
1085 }
1086 let tp = c.tp.map(|t| view! {<mo>":"</mo>{do_term(t)}});
1087 let df = c.df.map(|t| view! {<mo>":="</mo>{do_term(t)}});
1088 leptos::either::Either::Right(view! {<mrow>{head}{tp}{df}</mrow>})
1089 }
1090 let news = new.len();
1091 for n in new {
1092 current.push(n);
1093 }
1094 let ctx = if current.is_empty() {
1095 None
1096 } else {
1097 let mut iter = current.iter().cloned();
1098 // SAFETY: !current.is_empty()
1099 let first = unsafe { iter.next().unwrap_unchecked() };
1100 Some(
1101 view! {
1102 <mo style="font-weight:bold">"{"</mo>
1103 {component_var(first)}
1104 {iter.map(|v| view!{<mo>","</mo>{component_var(v)}}).collect_view()}
1105 <mo style="font-weight:bold">"}"</mo>
1106 }
1107 .into_any(),
1108 )
1109 };
1110 let r = then(ctx, current);
1111 for _ in 0..news {
1112 current.pop();
1113 }
1114 r
1115}
1116
1117fn do_displayable(d: Displayable) -> impl IntoView {
1118 use leptos::either::EitherOf5::{A, B, C, D, E};
1119 match d {
1120 Displayable::String(s) => A(s),
1121 Displayable::Num(i) => B(i),
1122 //Displayable::Space => C(" "),
1123 Displayable::Term(t) => C(ftml_dom::utils::math(move || do_term(t))),
1124 Displayable::Var(v) => D(ftml_dom::utils::math(move || {
1125 do_term(Term::Var {
1126 variable: v,
1127 presentation: None,
1128 })
1129 })),
1130 Displayable::Uri(Uri::Symbol(s)) => E(s.as_view()),
1131 Displayable::Uri(Uri::Module(m)) => E(m.as_view()),
1132 Displayable::Uri(Uri::DocumentElement(e)) => E(e.as_view()),
1133 Displayable::Uri(u) => A(u.to_string()),
1134 }
1135}
1136
1137fn do_success(s: bool) -> impl IntoView {
1138 if s {
1139 leptos::either::Either::Left(view! {<span style="color:green">"✔ "</span>})
1140 } else {
1141 leptos::either::Either::Right(view! {<span style="color:red">"✗ "</span>})
1142 }
1143}
1144
1145const ADD_INFO: bool = true;
1146
1147fn do_term(t: Term) -> impl IntoView {
1148 if ADD_INFO {
1149 use ftml_component_utils::{Popover, PopoverSize, PopoverTrigger};
1150 let s = format!("{:#?}", t.debug_short());
1151 leptos::either::Either::Left(view! {<msup>
1152 {t.into_view::<crate::Views>(ftml_components::backend(),false)}
1153 <Popover size=PopoverSize::Small>
1154 <PopoverTrigger slot><mi>"🛈"</mi></PopoverTrigger>
1155 <pre>{s}</pre>
1156 </Popover>
1157 </msup>})
1158 } else {
1159 leptos::either::Either::Right(
1160 t.into_view::<crate::Views>(ftml_components::backend(), false),
1161 )
1162 }
1163}
1164
1165fn do_variable_uri(v: DocumentElementUri) -> impl IntoView {
1166 let t = Term::Var {
1167 variable: Variable::Ref {
1168 declaration: v,
1169 is_sequence: None,
1170 },
1171 presentation: None,
1172 };
1173 t.into_view::<crate::Views>(ftml_components::backend(), false)
1174}
1175
1176fn tree<V: IntoView + 'static>(
1177 success: bool,
1178 head: impl IntoView + 'static,
1179 mut children: impl FnMut() -> V + Send + 'static,
1180) -> impl IntoView {
1181 use leptos::either::Either::{Left, Right};
1182 if success {
1183 Left(LazySubtree(flams_web_utils::components::LazySubtreeProps {
1184 header: flams_web_utils::components::Header {
1185 children: Box::new(move || view! {{do_success(true)}{head}}.into_any()),
1186 },
1187 children: Box::new(move || children().into_any()),
1188 }))
1189 /*Left(view! {
1190 <LazySubtree>
1191 <Header slot>{do_success(true)}{head}</Header>
1192 {children()}
1193 </LazySubtree>
1194 })*/
1195 } else {
1196 Right(view! {
1197 <Subtree expanded=true>
1198 <Header slot>{do_success(false)}{head}</Header>
1199 {children()}
1200 </Subtree>
1201 })
1202 }
1203}