1use crate::{
2 components::{IntoLOs, LOs},
3 FTMLString, FTMLStringMath,
4};
5use flams_ontology::{
6 content::{declarations::symbols::ArgSpec, terms::Term},
7 languages::Language,
8 uris::{ContentURITrait, ModuleURI, Name, SymbolURI, URIOrRefTrait, URIRefTrait, URI},
9};
10use flams_utils::vecmap::VecSet;
11
12use super::{narration::OMDocDocumentElement, OMDoc, OMDocDecl};
13use flams_web_utils::{
14 components::{Block, Header, HeaderLeft, HeaderRight, LazyCollapsible},
15 inject_css,
16};
17use leptos::{
18 context::Provider,
19 either::{Either, EitherOf5},
20 prelude::*,
21};
22use thaw::{Text, TextTag};
23
24#[derive(Copy, Clone)]
25struct InStruct;
26
27#[derive(Clone, Debug, serde::Serialize, serde::Deserialize)]
28#[cfg_attr(feature = "ts", derive(tsify_next::Tsify))]
29pub struct OMDocModule<E: OMDocDecl> {
30 pub uri: ModuleURI,
31 #[cfg_attr(feature = "ts", tsify(type = "ModuleURI[]"))]
32 pub imports: VecSet<ModuleURI>,
33 #[cfg_attr(feature = "ts", tsify(type = "ModuleURI[]"))]
34 pub uses: VecSet<ModuleURI>,
35 pub metatheory: Option<ModuleURI>,
36 pub signature: Option<Language>,
37 pub children: Vec<E>,
38}
39impl<E: OMDocDecl> super::OMDocT for OMDocModule<E> {
40 fn into_view(self) -> impl IntoView {
41 view! {
42 <Block>
43 <Header slot><b>"Module "
44 {super::module_name(&self.uri)}
45 {self.metatheory.map(|m|
46 view!(" (Metatheory "{super::module_name(&m)}")")
47 )}
48 </b></Header>
49 <HeaderLeft slot>{super::uses("Imports",self.imports.0)}</HeaderLeft>
50 <HeaderRight slot>{super::uses("Uses",self.uses.0)}</HeaderRight>
51 {self.children.into_iter().map(super::OMDocT::into_view).collect_view()}
52 </Block>
53 }
54 }
55}
56impl From<OMDocModule<OMDocDeclaration>> for OMDoc {
57 #[inline]
58 fn from(value: OMDocModule<OMDocDeclaration>) -> Self {
59 Self::Module(value)
60 }
61}
62impl From<OMDocModule<OMDocDocumentElement>> for OMDoc {
63 #[inline]
64 fn from(value: OMDocModule<OMDocDocumentElement>) -> Self {
65 Self::DocModule(value)
66 }
67}
68impl From<OMDocModule<OMDocDeclaration>> for OMDocDeclaration {
69 #[inline]
70 fn from(value: OMDocModule<OMDocDeclaration>) -> Self {
71 Self::NestedModule(value)
72 }
73}
74
75#[derive(Clone, Debug, serde::Serialize, serde::Deserialize)]
76#[cfg_attr(feature = "ts", derive(tsify_next::Tsify))]
77pub struct OMDocMorphism<E: OMDocDecl> {
78 pub uri: SymbolURI,
79 pub total: bool,
80 pub target: Option<ModuleURI>,
81 #[cfg_attr(feature = "ts", tsify(type = "ModuleURI[]"))]
82 pub uses: VecSet<ModuleURI>,
83 pub children: Vec<E>,
84}
85impl<E: OMDocDecl> super::OMDocT for OMDocMorphism<E> {
86 fn into_view(self) -> impl IntoView {
87 view!(<div>"TODO: Morphism"</div>)
88 }
89}
90impl From<OMDocMorphism<OMDocDeclaration>> for OMDoc {
91 #[inline]
92 fn from(value: OMDocMorphism<OMDocDeclaration>) -> Self {
93 Self::Morphism(value)
94 }
95}
96impl From<OMDocMorphism<OMDocDocumentElement>> for OMDoc {
97 #[inline]
98 fn from(value: OMDocMorphism<OMDocDocumentElement>) -> Self {
99 Self::DocMorphism(value)
100 }
101}
102impl From<OMDocMorphism<OMDocDeclaration>> for OMDocDeclaration {
103 #[inline]
104 fn from(value: OMDocMorphism<OMDocDeclaration>) -> Self {
105 Self::Morphism(value)
106 }
107}
108
109#[derive(Clone, Debug, serde::Serialize, serde::Deserialize)]
110#[cfg_attr(feature = "ts", derive(tsify_next::Tsify))]
111pub struct OMDocStructure<E: OMDocDecl> {
112 pub uri: SymbolURI,
113 pub macro_name: Option<String>,
114 #[cfg_attr(feature = "ts", tsify(type = "ModuleURI[]"))]
115 pub uses: VecSet<ModuleURI>,
116 #[cfg_attr(feature = "ts", tsify(type = "ModuleURI[]"))]
117 pub extends: VecSet<ModuleURI>,
118 pub children: Vec<E>,
119 pub extensions: Vec<(SymbolURI, Vec<OMDocSymbol>)>,
120}
121impl<E: OMDocDecl> super::OMDocT for OMDocStructure<E> {
122 fn into_view(self) -> impl IntoView {
123 let OMDocStructure {
124 uri,
125 macro_name,
126 extends,
127 extensions,
128 uses,
129 children,
130 } = self;
131 let uriclone = uri.clone();
132 view! {
133 <Provider value=InStruct>
134 <Block>
135 <Header slot><span>
136 <b>"Structure "{super::symbol_name(&uri, uri.name().last_name().as_ref())}</b>
137 {macro_name.map(|name| view!(<span>" ("<Text tag=TextTag::Code>"\\"{name}</Text>")"</span>))}
138 </span></Header>
139 <HeaderLeft slot>{super::uses("Extends",extends.0)}</HeaderLeft>
140 <HeaderRight slot>{super::uses("Uses",uses.0)}</HeaderRight>
141 {children.into_iter().map(super::OMDocT::into_view).collect_view()}
142 {if !extensions.is_empty() {Some(view!{
143 <b>"Conservative Extensions:"</b>
144 {extensions.into_iter().map(|(uri,s)| view!{
145 <Block show_separator=false>
146 <Header slot>{super::module_name(uri.module())}</Header>
147 {s.into_iter().map(super::OMDocT::into_view).collect_view()}
148 </Block>
149 }).collect_view()}
150 })} else {None}}
151 {do_los(uriclone)}
152 </Block>
153 </Provider>
154 }
155 }
156}
157impl From<OMDocStructure<OMDocDeclaration>> for OMDoc {
158 #[inline]
159 fn from(value: OMDocStructure<OMDocDeclaration>) -> Self {
160 Self::Structure(value)
161 }
162}
163impl From<OMDocStructure<OMDocDocumentElement>> for OMDoc {
164 #[inline]
165 fn from(value: OMDocStructure<OMDocDocumentElement>) -> Self {
166 Self::DocStructure(value)
167 }
168}
169impl From<OMDocStructure<OMDocDeclaration>> for OMDocDeclaration {
170 #[inline]
171 fn from(value: OMDocStructure<OMDocDeclaration>) -> Self {
172 Self::Structure(value)
173 }
174}
175
176#[derive(Clone, Debug, serde::Serialize, serde::Deserialize)]
177#[cfg_attr(feature = "ts", derive(tsify_next::Tsify))]
178pub struct OMDocExtension<E: OMDocDecl> {
179 pub uri: SymbolURI,
180 pub target: SymbolURI,
181 #[cfg_attr(feature = "ts", tsify(type = "ModuleURI[]"))]
182 pub uses: VecSet<ModuleURI>,
183 pub children: Vec<E>,
184}
185impl<E: OMDocDecl> super::OMDocT for OMDocExtension<E> {
186 fn into_view(self) -> impl IntoView {
187 let OMDocExtension {
188 uri,
189 target,
190 uses,
191 children,
192 } = self;
193 view! {
194 <Provider value=InStruct>
195 <Block>
196 <Header slot><span>
197 <b>"Conservative Extension for "{super::symbol_name(&target, target.name().last_name().as_ref())}</b>
198 </span></Header>
199 <HeaderRight slot>{super::uses("Uses",uses.0)}</HeaderRight>
200 {children.into_iter().map(super::OMDocT::into_view).collect_view()}
201 </Block>
202 </Provider>
203 }
204 }
205}
206impl From<OMDocExtension<OMDocDeclaration>> for OMDoc {
207 #[inline]
208 fn from(value: OMDocExtension<OMDocDeclaration>) -> Self {
209 Self::Extension(value)
210 }
211}
212impl From<OMDocExtension<OMDocDocumentElement>> for OMDoc {
213 #[inline]
214 fn from(value: OMDocExtension<OMDocDocumentElement>) -> Self {
215 Self::DocExtension(value)
216 }
217}
218impl From<OMDocExtension<OMDocDeclaration>> for OMDocDeclaration {
219 #[inline]
220 fn from(value: OMDocExtension<OMDocDeclaration>) -> Self {
221 Self::Extension(value)
222 }
223}
224
225#[derive(Clone, Debug, serde::Serialize, serde::Deserialize)]
226#[cfg_attr(feature = "ts", derive(tsify_next::Tsify))]
227#[cfg_attr(feature = "ts", tsify(into_wasm_abi, from_wasm_abi))]
228#[serde(tag = "type")]
229pub enum OMDocDeclaration {
230 Symbol(OMDocSymbol),
231 NestedModule(OMDocModule<OMDocDeclaration>),
232 Structure(OMDocStructure<OMDocDeclaration>),
233 Morphism(OMDocMorphism<OMDocDeclaration>),
234 Extension(OMDocExtension<OMDocDeclaration>),
235}
236
237impl super::sealed::Sealed for OMDocDeclaration {}
238impl super::OMDocDecl for OMDocDeclaration {}
239impl super::OMDocT for OMDocDeclaration {
240 #[inline]
241 fn into_view(self) -> impl IntoView {
242 match self {
243 Self::Symbol(e) => EitherOf5::A(e.into_view()),
244 Self::NestedModule(e) => EitherOf5::B(e.into_view()),
245 Self::Structure(e) => EitherOf5::C(e.into_view()),
246 Self::Morphism(e) => EitherOf5::D(e.into_view()),
247 Self::Extension(e) => EitherOf5::E(e.into_view()),
248 }
249 }
250}
251impl From<OMDocDeclaration> for OMDoc {
252 #[inline]
253 fn from(value: OMDocDeclaration) -> Self {
254 match value {
255 OMDocDeclaration::Symbol(s) => Self::SymbolDeclaration(s),
256 OMDocDeclaration::NestedModule(s) => Self::Module(s),
257 OMDocDeclaration::Structure(s) => Self::Structure(s),
258 OMDocDeclaration::Morphism(s) => Self::Morphism(s),
259 OMDocDeclaration::Extension(s) => Self::Extension(s),
260 }
261 }
262}
263
264pub(super) fn do_notations(uri: URI, arity: ArgSpec) -> impl IntoView {
265 use flams_web_utils::components::{Popover, PopoverTrigger};
266 use thaw::{Table, TableCell, TableHeader, TableHeaderCell, TableRow};
267 let functional = arity.num() > 0;
268 let as_variable = match &uri {
269 URI::Content(_) => false,
270 URI::Narrative(_) => true,
271 _ => unreachable!(),
272 };
273 let uriclone = uri.clone();
274 inject_css("flams-notation-table", include_str!("notations.css"));
275 crate::remote::get!(notations(uri.clone()) = v => {
276 let uri = uriclone.clone();
277 if v.is_empty() {None} else {
278 Some(view!{
279 <div>
280 <Table class="flams-notation-table"><TableRow>
281 <TableCell class="flams-notation-header"><span>"Notations: "</span></TableCell>
282 {let uri = uri;v.into_iter().map(move |(u,n)| {
283 let html = n.display_ftml(false,as_variable,&uri).to_string();
284 let htmlclone = html.clone();
285 let uri = uri.clone();
286 view!{
287 <TableCell class="flams-notation-cell">
288 <Popover>
289 <PopoverTrigger slot><span>
290 <Provider value=crate::components::terms::DisablePopover>
291 <FTMLStringMath html/>
292 </Provider>
293 </span></PopoverTrigger>
294 {
295 let html = htmlclone;
296 let op = if functional {
297 n.op.as_ref().map(|op| op.display_ftml(as_variable,&uri).to_string())
298 } else {None};
299 view!{<Table class="flams-notation-table">
300 <TableHeader>
301 <TableRow>
302 <TableHeaderCell class="flams-notation-header">"source document"</TableHeaderCell>
303 {if functional {Some(view!{<TableHeaderCell class="flams-notation-header">"operation"</TableHeaderCell>})} else {None}}
304 <TableHeaderCell class="flams-notation-header">"notation"</TableHeaderCell>
305 </TableRow>
306 </TableHeader>
307 <TableRow>
308 <TableCell class="flams-notation-cell">{
309 super::doc_name(u.document(), u.document().name().last_name().to_string())
310 }</TableCell>
311 {if functional {Some(view!{<TableCell class="flams-notation-cell">{
312 op.map_or_else(
313 || Either::Left("(No op)"),
314 |html| Either::Right(view!{
315 <Provider value=crate::components::terms::DisablePopover>
316 <FTMLStringMath html/>
317 </Provider>
318 })
319 )
320 }</TableCell>})} else {None}}
321 <TableCell class="flams-notation-cell">
322 <Provider value=crate::components::terms::DisablePopover>
323 <FTMLStringMath html/>
324 </Provider>
325 </TableCell>
326 </TableRow>
327 </Table>}
328 }
329 </Popover>
330 </TableCell>
331 }
332 }).collect_view()}
333 </TableRow></Table>
334 </div>
335 })
336 }
337 })
338}
339
340fn do_los(uri: SymbolURI) -> impl IntoView {
341 use flams_ontology::narration::LOKind;
342 view! {
343 <LazyCollapsible>
344 <Header slot><span>"Learning Objects"</span></Header>
345 <div style="padding-left:15px">{
346 let uri = uri.clone();
347 crate::remote::get!(get_los(uri.clone(),true) = v => {
348 let LOs {definitions,examples,problems} = v.lo_sort();
349 view!{
350 <div>{if definitions.is_empty() { None } else {Some(
351 super::comma_sep("Definitions", definitions.into_iter().map(|uri| {
352 let title = uri.name().last_name().to_string();
353 super::doc_elem_name(uri,None,title)
354 }))
355 )}}</div>
356 <div>{if examples.is_empty() { None } else {Some(
357 super::comma_sep("Examples", examples.into_iter().map(|uri| {
358 let title = uri.name().last_name().to_string();
359 super::doc_elem_name(uri,None,title)
360 }))
361 )}}</div>
362 <div>{if problems.is_empty() { None } else {Some(
363 super::comma_sep("Problems", problems.into_iter().map(|(_,uri,cd)| {
364 let title = uri.name().last_name().to_string();
365 view!{
366 {super::doc_elem_name(uri,None,title)}
367 " ("{cd.to_string()}")"
368 }
369 }))
370 )}}</div>
371 }
372 })
373 }</div>
374 </LazyCollapsible>
375 }
376}
377
378#[derive(Clone, Debug, serde::Serialize, serde::Deserialize)]
379#[cfg_attr(feature = "ts", derive(tsify_next::Tsify))]
380#[cfg_attr(feature = "ts", tsify(into_wasm_abi, from_wasm_abi))]
381pub struct OMDocSymbol {
382 pub uri: SymbolURI,
383 pub df: Option<Term>,
384 pub tp: Option<Term>,
385 pub arity: ArgSpec,
386 pub roles: Vec<String>,
387 pub macro_name: Option<String>,
388 }
390impl super::OMDocT for OMDocSymbol {
391 fn into_view(self) -> impl IntoView {
392 let OMDocSymbol {
393 uri,
394 df,
395 tp,
396 arity,
397 roles,
398 macro_name,
399 } = self;
400 let show_separator = true; let symbol_str = if use_context::<InStruct>().is_some() {
402 "Field "
403 } else if roles.iter().any(|s| s == "textsymdecl") {
404 "Text Symbol "
405 } else {
406 "Symbol "
407 };
408 let uriclone = uri.clone();
409 let uriclone_b = uri.clone();
410 view! {
411 <Block show_separator>
412 <Header slot><span>
413 <b>{symbol_str}{super::symbol_name(&uri, uri.name().last_name().as_ref())}</b>
414 {macro_name.map(|name| view!(<span>" ("<Text tag=TextTag::Code>"\\"{name}</Text>")"</span>))}
415 {tp.map(|t| view! {
416 " of type "{
417 crate::remote::get!(present(t.clone()) = html => {
418 view!(<FTMLStringMath html/>)
419 })
420 }
421 })}
422 </span></Header>
423 <HeaderLeft slot>{do_notations(URI::Content(uriclone_b.into()),arity)}</HeaderLeft>
424 <HeaderRight slot><span style="white-space:nowrap;">{df.map(|t| view! {
425 "Definiens: "{
426 crate::remote::get!(present(t.clone()) = html => {
427 view!(<FTMLStringMath html/>)
428 })
429 }
430 })}</span></HeaderRight>
431 {do_los(uriclone)}
432 </Block>
433 }
434 }
435}
436impl From<OMDocSymbol> for OMDoc {
437 #[inline]
438 fn from(value: OMDocSymbol) -> Self {
439 Self::SymbolDeclaration(value)
440 }
441}
442impl From<OMDocSymbol> for OMDocDeclaration {
443 #[inline]
444 fn from(value: OMDocSymbol) -> Self {
445 Self::Symbol(value)
446 }
447}
448
449#[cfg(feature = "ssr")]
450mod froms {
451 use super::{
452 super::OMDoc, OMDocDeclaration, OMDocExtension, OMDocModule, OMDocMorphism, OMDocStructure,
453 OMDocSymbol,
454 };
455 use flams_ontology::{
456 content::{
457 declarations::{
458 morphisms::Morphism,
459 structures::{Extension, MathStructure},
460 symbols::Symbol,
461 Declaration, OpenDeclaration,
462 },
463 modules::{Module, NestedModule},
464 ModuleLike, ModuleTrait,
465 },
466 uris::ModuleURI,
467 Checked, Resolvable,
468 };
469 use flams_system::backend::{Backend, StringPresenter};
470 use flams_utils::vecmap::VecSet;
471
472 impl OMDoc {
473 pub fn from_module_like<B: Backend>(
474 m: &ModuleLike,
475 backend: &B, ) -> Self {
477 match m {
478 ModuleLike::Module(m) => OMDocModule::from_module(m, backend).into(),
479 ModuleLike::NestedModule(m) => {
480 let mut imports = VecSet::new();
481 let children =
482 OMDocDeclaration::do_children(backend, &m.as_ref().elements, &mut imports);
483 OMDocModule {
484 uri: m.as_ref().uri.clone().into_module(),
485 children,
486 imports,
487 uses: VecSet::new(),
488 metatheory: None,
489 signature: None,
490 }
491 .into()
492 }
493 ModuleLike::Structure(s) => {
494 OMDocStructure::from_structure(s.as_ref(), backend).into()
495 }
496 ModuleLike::Extension(e) => {
497 OMDocExtension::from_extension(e.as_ref(), backend).into()
498 }
499 ModuleLike::Morphism(m) => OMDocMorphism::from_morphism(m.as_ref(), backend).into(),
500 }
501 }
502 }
503
504 impl OMDocSymbol {
505 pub fn from_symbol<B: Backend>(
506 Symbol {
507 uri,
508 arity,
509 df,
510 tp,
511 macroname,
512 role,
513 ..
514 }: &Symbol,
515 backend: &B, ) -> Self {
517 Self {
518 uri: uri.clone(),
519 arity: arity.clone(),
520 roles: role.iter().map(|s| s.to_string()).collect(),
521 df: df.clone(), tp: tp.clone(), macro_name: macroname.as_ref().map(ToString::to_string),
524 }
526 }
527 }
528
529 impl OMDocModule<OMDocDeclaration> {
530 pub fn from_module<B: Backend>(
531 module: &Module,
532 backend: &B, ) -> Self {
534 let uri = module.id().into_owned();
535 let metatheory = module.meta().map(|c| c.id().into_owned());
536 let signature = module.signature().map(|c| c.id().into_owned());
537 let mut imports = VecSet::new();
538 let children =
539 OMDocDeclaration::do_children(backend, module.declarations(), &mut imports);
540 Self {
541 uri,
542 metatheory,
543 signature,
544 children,
545 uses: VecSet::default(),
546 imports,
547 }
548 }
549 }
550
551 impl OMDocStructure<OMDocDeclaration> {
552 pub fn from_structure<B: Backend>(
553 s: &MathStructure<Checked>,
554 backend: &B, ) -> Self {
556 let uri = s.uri.clone();
557 let macro_name = s.macroname.as_ref().map(ToString::to_string);
558 let extensions = super::super::froms::get_extensions(backend, &uri)
559 .map(|e| {
560 (
561 e.as_ref().uri.clone(),
562 e.as_ref()
563 .elements
564 .iter()
565 .filter_map(|e| {
566 if let OpenDeclaration::Symbol(s) = e {
567 Some(OMDocSymbol::from_symbol(s, backend))
568 } else {
569 None
570 }
571 })
572 .collect(),
573 )
574 })
575 .collect();
576 let mut imports = VecSet::new();
577 let children = OMDocDeclaration::do_children(backend, s.declarations(), &mut imports);
578 Self {
579 uri,
580 macro_name,
581 extends: imports,
582 uses: VecSet::new(),
583 children,
584 extensions,
585 }
586 }
587 }
588
589 impl OMDocExtension<OMDocDeclaration> {
590 pub fn from_extension<B: Backend>(
591 e: &Extension<Checked>,
592 backend: &B, ) -> Self {
594 let target = e.target.id().into_owned();
595 let uri = e.uri.clone();
596 let mut imports = VecSet::new();
597 let children = OMDocDeclaration::do_children(backend, &e.elements, &mut imports);
598 OMDocExtension {
599 uri,
600 target,
601 uses: VecSet::new(),
602 children,
603 }
604 }
605 }
606
607 impl OMDocMorphism<OMDocDeclaration> {
608 pub fn from_morphism<B: Backend>(
609 m: &Morphism<Checked>,
610 backend: &B, ) -> Self {
612 let uri = m.uri.clone();
613 let total = m.total;
614 let target = Some(m.domain.id().into_owned());
615 let mut imports = VecSet::new();
616 let children = OMDocDeclaration::do_children(backend, &m.elements, &mut imports);
617 OMDocMorphism {
618 uri,
619 total,
620 target,
621 uses: VecSet::new(),
622 children,
623 }
624 }
625 }
626
627 impl OMDocDeclaration {
628 pub fn do_children<B: Backend>(
629 backend: &B, children: &[Declaration],
631 imports: &mut VecSet<ModuleURI>,
632 ) -> Vec<Self> {
633 let mut ret = Vec::new();
634 for c in children {
635 match c {
636 OpenDeclaration::Symbol(s) => {
637 ret.push(OMDocSymbol::from_symbol(s, backend).into())
638 }
639 OpenDeclaration::Import(m) => imports.insert(m.id().into_owned()),
640 OpenDeclaration::MathStructure(s) => {
641 ret.push(OMDocStructure::from_structure(s, backend).into())
642 }
643 OpenDeclaration::NestedModule(m) => {
644 let mut imports = VecSet::new();
645 let children = Self::do_children(backend, &m.elements, &mut imports);
646 ret.push(
647 OMDocModule {
648 uri: m.uri.clone().into_module(),
649 children,
650 imports,
651 uses: VecSet::new(),
652 metatheory: None,
653 signature: None,
654 }
655 .into(),
656 )
657 }
658 OpenDeclaration::Extension(e) => {
659 ret.push(OMDocExtension::from_extension(e, backend).into())
660 }
661 OpenDeclaration::Morphism(m) => {
662 ret.push(OMDocMorphism::from_morphism(m, backend).into())
663 }
664 }
665 }
666 ret
667 }
668 }
669}