flams_ontology/content/
mod.rs1use 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!()}
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 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}