ftml_solver/impls/
backend.rs

1use crate::{CheckRef, Checker, impls::solving::is_solvable_var, split::SplitStrategy};
2use dashmap::DashSet;
3use flams_math_archives::backend::{AnyBackend, LocalBackend};
4use ftml_ontology::{
5    domain::{
6        SharedDeclaration,
7        declarations::{IsDeclaration, symbols::Symbol},
8        modules::{Module, ModuleLike},
9    },
10    narrative::{SharedDocumentElement, documents::Document, elements::VariableDeclaration},
11    terms::{ComponentVar, Term, Variable},
12};
13use ftml_uris::{
14    DocumentElementUri, IsDomainUri, IsNarrativeUri, LeafUri, ModuleUri, NamedUri, SymbolUri,
15};
16use std::hint::unreachable_unchecked;
17
18pub fn get_variable(
19    backend: &AnyBackend,
20    documents: &DashSet<Document, rustc_hash::FxBuildHasher>,
21    current: &[LeafUri],
22    uri: &DocumentElementUri,
23    prepare: impl Fn(Term) -> Term,
24) -> Result<SharedDocumentElement<VariableDeclaration>, ()> {
25    fn get(
26        backend: &AnyBackend,
27        documents: &DashSet<Document, rustc_hash::FxBuildHasher>,
28        uri: &DocumentElementUri,
29    ) -> Result<SharedDocumentElement<VariableDeclaration>, ()> {
30        let doc = uri.document_uri();
31        if let Some(d) = documents.get(doc) {
32            return d.get_as(uri.name()).ok_or(());
33        }
34        let doc = backend.get_document(doc).map_err(|_| ())?;
35        documents.insert(doc.clone());
36        doc.get_as(uri.name()).ok_or(())
37    }
38
39    if current.iter().any(|u| u == uri) {
40        return Err(());
41    }
42    let d = get(backend, documents, uri)?;
43
44    if let Some(tp) = d.data.tp.get_parsed()
45        && !d.data.tp.has_checked()
46    {
47        let tp = prepare(tp.clone());
48
49        if d.data.is_seq && tp.as_sequence_type().is_none() {
50            if d.data.sequence_range.is_empty() {
51                d.data.tp.set_checked(tp.into_seq_type());
52            } else {
53                d.data
54                    .tp
55                    .set_checked(tp.into_ranged_seq_type(d.data.sequence_range.iter().cloned()));
56            }
57        } else {
58            d.data.tp.set_checked(tp);
59        }
60    }
61    if let Some(df) = d.data.df.get_parsed()
62        && !d.data.df.has_checked()
63    {
64        d.data.df.set_checked(prepare(df.clone()));
65    }
66
67    Ok(d)
68}
69
70impl<Split: SplitStrategy> Checker<Split> {
71    pub(crate) fn get_module_like(&self, uri: &ModuleUri) -> Result<ModuleLike, ()> {
72        if uri.is_top() {
73            if let Some(m) = self.modules.get(uri) {
74                return Ok(ModuleLike::Module(m.clone()));
75            }
76            let ModuleLike::Module(m) = self.backend.get_module(uri).map_err(|_| ())? else {
77                // SAFETY: uri.is_top()
78                unsafe { unreachable_unchecked() }
79            };
80            self.modules.insert(m.clone());
81            Ok(ModuleLike::Module(m))
82        } else {
83            // SAFETY: !uri.is_top()
84            let inner = unsafe { uri.clone().into_top_symbol().unwrap_unchecked() };
85            let m = self.get_module(inner.module_uri())?;
86            m.as_module_like(uri.name()).ok_or(())
87        }
88    }
89    pub(crate) fn get_module(&self, uri: &ModuleUri) -> Result<Module, ()> {
90        if uri.is_top() {
91            if let Some(m) = self.modules.get(uri) {
92                return Ok(m.clone());
93            }
94            let ModuleLike::Module(m) = self.backend.get_module(uri).map_err(|_| ())? else {
95                // SAFETY: uri.is_top()
96                unsafe { unreachable_unchecked() }
97            };
98            self.modules.insert(m.clone());
99            Ok(m)
100        } else {
101            let uri = !uri.clone();
102            if let Some(m) = self.modules.get(&uri) {
103                return Ok(m.clone());
104            }
105            let ModuleLike::Module(m) = self.backend.get_module(&uri).map_err(|_| ())? else {
106                // SAFETY: uri = !uri enforces top-level
107                unsafe { unreachable_unchecked() }
108            };
109            self.modules.insert(m.clone());
110            Ok(m)
111        }
112    }
113
114    pub(crate) fn get_symbol(
115        &self,
116        uri: &SymbolUri,
117        prepare: impl Fn(Term) -> Term,
118    ) -> Result<SharedDeclaration<Symbol>, ()> {
119        if self.current.iter().any(|u| u == uri) {
120            return Err(());
121        }
122        let uri = uri.as_simple_module();
123        let Some(d) = self
124            .get_module(&uri.module)
125            .map_err(|_| ())?
126            .get_as::<Symbol>(uri.name())
127        else {
128            return Err(());
129        };
130        if let Some(tp) = d.data.tp.get_parsed()
131            && !d.data.tp.has_checked()
132        {
133            d.data.tp.set_checked(prepare(tp.clone()));
134        }
135        if let Some(df) = d.data.df.get_parsed()
136            && !d.data.df.has_checked()
137        {
138            d.data.df.set_checked(prepare(df.clone()));
139        }
140        Ok(d)
141        //.ok_or();
142    }
143
144    pub(crate) fn get_variable(
145        &self,
146        uri: &DocumentElementUri,
147    ) -> Result<SharedDocumentElement<VariableDeclaration>, ()> {
148        get_variable(&self.backend, &self.documents, &self.current, uri, |t| {
149            self.prepare(None, t).1
150        })
151        /*
152        fn get<Split: SplitStrategy>(
153            slf: &Checker<Split>,
154            uri: &DocumentElementUri,
155        ) -> Result<SharedDocumentElement<VariableDeclaration>, ()> {
156            let doc = uri.document_uri();
157            if let Some(d) = slf.documents.get(doc) {
158                return d.get_as(uri.name()).ok_or(());
159            }
160            let doc = slf.backend.get_document(doc).map_err(|_| ())?;
161            slf.documents.insert(doc.clone());
162            doc.get_as(uri.name()).ok_or(())
163        }
164        if self.current.iter().any(|u| u == uri) {
165            return Err(());
166        }
167        let d = get(self, uri)?;
168
169        if let Some(tp) = d.data.tp.get_parsed()
170            && !d.data.tp.has_checked()
171        {
172            let (_, tp) = self.prepare(None, tp.clone());
173
174            if d.data.is_seq && tp.as_sequence_type().is_none() {
175                d.data.tp.set_checked(tp.into_seq_type());
176            } else {
177                d.data.tp.set_checked(tp);
178            }
179        }
180        if let Some(df) = d.data.df.get_parsed()
181            && !d.data.df.has_checked()
182        {
183            d.data.df.set_checked(self.prepare(None, df.clone()).1);
184        }
185
186        Ok(d)
187         */
188    }
189}
190
191impl<Split: SplitStrategy> CheckRef<'_, '_, Split> {
192    /// ### Errors
193    pub(crate) fn get_declaration<T: IsDeclaration>(
194        &self,
195        uri: &SymbolUri,
196    ) -> Result<SharedDeclaration<T>, ()> {
197        self.top
198            .get_module(&uri.module)?
199            .get_as::<T>(uri.name())
200            .ok_or(())
201    }
202
203    /// ### Errors
204    #[inline]
205    pub(crate) fn get_symbol(&self, uri: &SymbolUri) -> Result<SharedDeclaration<Symbol>, ()> {
206        self.top.get_symbol(uri, |t| self.prepare(t, None).1)
207    }
208
209    pub(crate) fn get_symbol_type(&mut self, uri: &SymbolUri) -> Option<Term> {
210        let Ok(s) = self.get_symbol(uri) else {
211            self.failure("Symbol not found");
212            return None;
213        };
214        s.data.tp.checked_or_parsed().map(|(t, _)| t)
215    }
216    pub(crate) fn get_symbol_definiens(&mut self, uri: &SymbolUri) -> Option<Term> {
217        let Ok(s) = self.get_symbol(uri) else {
218            self.failure("Symbol not found");
219            return None;
220        };
221        s.data.df.checked_or_parsed().map(|(t, _)| t)
222    }
223
224    /// ### Errors
225    #[inline]
226    pub fn get_variable(
227        &self,
228        uri: &DocumentElementUri,
229    ) -> Result<SharedDocumentElement<VariableDeclaration>, ()> {
230        self.top.get_variable(uri)
231    }
232
233    pub(crate) fn get_var_definiens(&mut self, var: &Variable) -> Option<Term> {
234        if let Some(id) = is_solvable_var(var) {
235            return self.get_solution(id);
236        }
237        for v in self.iter_context() {
238            match (v, var) {
239                (
240                    ComponentVar {
241                        var: Variable::Name { name, .. },
242                        df,
243                        ..
244                    },
245                    Variable::Name { name: n2, .. },
246                ) if *name == *n2 => {
247                    return df.clone().map(|t| self.subst(t));
248                }
249                (
250                    ComponentVar {
251                        var: Variable::Name { name, .. },
252                        df,
253                        ..
254                    },
255                    Variable::Ref { declaration, .. },
256                ) if name.as_ref() == declaration.name().last() && df.is_some() => {
257                    return df.clone().map(|t| self.subst(t));
258                }
259                (
260                    ComponentVar {
261                        var: Variable::Ref { declaration, .. },
262                        df,
263                        ..
264                    },
265                    Variable::Name { name, .. },
266                ) if name.as_ref() == declaration.name().last() => {
267                    return if df.is_some() {
268                        df.clone().map(|t| self.subst(t))
269                    } else {
270                        self.get_variable(declaration)
271                            .ok()?
272                            .data
273                            .df
274                            .checked_or_parsed()
275                            .map(|(t, _)| t)
276                    };
277                }
278                (
279                    ComponentVar {
280                        var: Variable::Ref { declaration, .. },
281                        df,
282                        ..
283                    },
284                    Variable::Ref {
285                        declaration: d2, ..
286                    },
287                ) if *declaration == *d2 => {
288                    return if df.is_some() {
289                        df.clone().map(|t| self.subst(t))
290                    } else {
291                        self.get_variable(declaration)
292                            .ok()?
293                            .data
294                            .df
295                            .checked_or_parsed()
296                            .map(|(t, _)| t)
297                    };
298                }
299                _ => (),
300            }
301        }
302        if let Variable::Ref { declaration, .. } = var {
303            self.get_variable(declaration)
304                .ok()?
305                .data
306                .df
307                .checked_or_parsed()
308                .map(|(t, _)| t)
309        } else {
310            None
311        }
312    }
313}
ftml_solver/impls/backend.rs

ftml_solver/impls/
backend.rs
