flams_ontology/content/
mod.rs

1use std::{borrow::Cow, fmt::Debug};
2
3use declarations::{
4    morphisms::Morphism,
5    structures::{Extension, MathStructure},
6    Declaration, DeclarationTrait,
7};
8use flams_utils::prelude::InnerArc;
9use modules::{Module, NestedModule};
10
11use crate::{uris::{ContentURIRef, ModuleURI, Name, NameStep, SymbolURI}, Checked, Resolvable};
12
13pub mod checking;
14pub mod declarations;
15mod macros;
16pub mod modules;
17pub mod terms;
18
19pub struct ContentReference<T: DeclarationTrait>(InnerArc<Module, T>);
20impl<T:DeclarationTrait+Resolvable<From=SymbolURI>> Resolvable for ContentReference<T> {
21    type From = SymbolURI;
22    fn id(&self) -> Cow<'_,Self::From> {
23        self.0.as_ref().id()
24    }
25}
26
27impl<T: DeclarationTrait> ContentReference<T> {
28    #[must_use]
29    pub fn new(m: &ModuleLike, name: &Name) -> Option<Self> {
30        macro_rules! get {
31            () => {
32                |m| {
33                    if let Some(d) = m.find(name.steps()) {
34                        Ok(d)
35                    } else {
36                        Err(())
37                    }
38                }
39            };
40        }
41        let r = unsafe {
42            match m {
43                ModuleLike::Module(m) => InnerArc::new(m, |m| &m.0, get!()).ok()?,
44                ModuleLike::NestedModule(m) => m.0.inherit(get!()).ok()?,
45                ModuleLike::Structure(s) => s.0.inherit(get!()).ok()?,
46                ModuleLike::Extension(e) => e.0.inherit(get!()).ok()?,
47                ModuleLike::Morphism(m) => m.0.inherit(get!()).ok()?,
48            }
49        };
50        Some(Self(r))
51    }
52}
53
54impl<T: DeclarationTrait> AsRef<T> for ContentReference<T> {
55    #[inline]
56    fn as_ref(&self) -> &T {
57        self.0.as_ref()
58    }
59}
60
61impl<T: DeclarationTrait + Debug> Debug for ContentReference<T> {
62    #[inline]
63    fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result {
64        Debug::fmt(self.as_ref(), f)
65    }
66}
67
68#[derive(Debug)]
69pub enum ModuleLike {
70    Module(Module),
71    NestedModule(ContentReference<NestedModule<Checked>>),
72    Structure(ContentReference<MathStructure<Checked>>),
73    Extension(ContentReference<Extension<Checked>>),
74    Morphism(ContentReference<Morphism<Checked>>),
75}
76impl Resolvable for ModuleLike {
77    type From = ModuleURI;
78    fn id(&self) -> Cow<'_,Self::From> {
79        match self {
80            Self::Module(m) => Cow::Borrowed(m.uri()),
81            Self::NestedModule(m) => Cow::Owned(m.as_ref().uri.clone().into_module()),
82            Self::Structure(s) => Cow::Owned(s.as_ref().uri.clone().into_module()),
83            Self::Extension(e) => Cow::Owned(e.as_ref().uri.clone().into_module()),
84            Self::Morphism(_) => todo!()//Cow::Owned(m.0.as_ref().uri.into_module()),
85        }
86    }
87}
88
89impl ModuleLike {
90    #[must_use]
91    pub fn in_module(m: &Module, name: &Name) -> Option<Self> {
92        let steps = name.steps();
93        if steps.is_empty() || &steps[0] != m.uri().name().last_name() {
94            return None;
95        }
96        let steps = &steps[1..];
97        if steps.is_empty() {
98            return Some(Self::Module(m.clone()));
99        }
100        let d: &Declaration = m.find(steps)?;
101        match d {
102            Declaration::NestedModule(nm) => Some(Self::NestedModule(ContentReference(unsafe {
103                InnerArc::new_owned_infallible(m.clone(), |m| &m.0, |_| nm)
104            }))),
105            Declaration::MathStructure(s) => Some(Self::Structure(ContentReference(unsafe {
106                InnerArc::new_owned_infallible(m.clone(), |m| &m.0, |_| s)
107            }))),
108            Declaration::Extension(s) => Some(Self::Extension(ContentReference(unsafe {
109                InnerArc::new_owned_infallible(m.clone(), |m| &m.0, |_| s)
110            }))),
111            Declaration::Morphism(s) => Some(Self::Morphism(ContentReference(unsafe {
112                InnerArc::new_owned_infallible(m.clone(), |m| &m.0, |_| s)
113            }))),
114            _ => None,
115        }
116    }
117}
118
119pub trait ModuleTrait {
120    fn declarations(&self) -> &[Declaration];
121    fn content_uri(&self) -> ContentURIRef;
122    fn find<T: DeclarationTrait>(&self, steps: &[NameStep]) -> Option<&T> {
123        //println!("Trying to find {steps:?} in {}",self.content_uri());
124        let mut steps = steps;
125        let mut curr = self.declarations().iter();
126        while !steps.is_empty() {
127            let step = &steps[0];
128            steps = &steps[1..];
129            while let Some(c) = curr.next() {
130                match c {
131                    Declaration::NestedModule(m) if m.uri.name().last_name() == step => {
132                        if steps.is_empty() {
133                            return T::from_declaration(c);
134                        }
135                        curr = m.declarations().iter();
136                    }
137                    Declaration::MathStructure(m) if m.uri.name().last_name() == step => {
138                        if steps.is_empty() {
139                            return T::from_declaration(c);
140                        }
141                        curr = m.declarations().iter();
142                    }
143                    Declaration::Morphism(m)
144                        if m.uri.name().last_name() == step =>
145                    {
146                        if steps.is_empty() {
147                            return T::from_declaration(c);
148                        }
149                        curr = m.declarations().iter();
150                    }
151                    Declaration::Extension(m) if m.uri.name().last_name() == step => {
152                        if steps.is_empty() {
153                            return T::from_declaration(c);
154                        }
155                        curr = m.declarations().iter();
156                    }
157                    Declaration::Symbol(s) if s.uri.name().last_name() == step => {
158                        return if steps.is_empty() {
159                            T::from_declaration(c)
160                        } else {
161                            None
162                        }
163                    }
164                    _ => (),
165                }
166            }
167        }
168        None
169    }
170}
171
172impl ModuleTrait for ModuleLike {
173    #[inline]
174    fn declarations(&self) -> &[Declaration] {
175        match self {
176            Self::Module(m) => m.declarations(),
177            Self::NestedModule(m) => m.as_ref().declarations(),
178            Self::Structure(s) => s.as_ref().declarations(),
179            Self::Extension(s) => s.as_ref().declarations(),
180            Self::Morphism(s) => s.as_ref().declarations(),
181        }
182    }
183    #[inline]
184    fn content_uri(&self) -> ContentURIRef {
185        match self {
186            Self::Module(m) => m.content_uri(),
187            Self::NestedModule(m) => m.as_ref().content_uri(),
188            Self::Structure(s) => s.as_ref().content_uri(),
189            Self::Extension(s) => s.as_ref().content_uri(),
190            Self::Morphism(s) => s.as_ref().content_uri(),
191        }
192    }
193}