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        HasDeclarations, SharedDeclaration,
7        declarations::{IsDeclaration, SharedSymbolLike, symbols::Symbol},
8        modules::{Module, ModuleLike},
9    },
10    narrative::{SharedDocumentElement, documents::Document, elements::VariableDeclaration},
11    terms::{ComponentVar, Term, Variable},
12};
13use ftml_uris::{DocumentElementUri, IsDomainUri, IsNarrativeUri, LeafUri, ModuleUri, SymbolUri};
14use std::hint::unreachable_unchecked;
15
16pub fn get_variable(
17    backend: &AnyBackend,
18    documents: &DashSet<Document, rustc_hash::FxBuildHasher>,
19    current: &[LeafUri],
20    uri: &DocumentElementUri,
21    prepare: impl Fn(Term) -> Term,
22) -> Result<SharedDocumentElement<VariableDeclaration>, ()> {
23    fn get(
24        backend: &AnyBackend,
25        documents: &DashSet<Document, rustc_hash::FxBuildHasher>,
26        uri: &DocumentElementUri,
27    ) -> Result<SharedDocumentElement<VariableDeclaration>, ()> {
28        let doc = uri.document_uri();
29        if let Some(d) = documents.get(doc) {
30            return d.get_as(uri.name()).ok_or(());
31        }
32        let doc = backend.get_document(doc).map_err(|_| ())?;
33        documents.insert(doc.clone());
34        doc.get_as(uri.name()).ok_or(())
35    }
36
37    if current.iter().any(|u| u == uri) {
38        return Err(());
39    }
40    let d = get(backend, documents, uri)?;
41
42    if let Some(tp) = d.data.tp.get_parsed()
43        && !d.data.tp.has_checked()
44    {
45        let tp = prepare(tp.clone());
46
47        if d.data.is_seq && tp.as_sequence_type().is_none() {
48            if d.data.sequence_range.is_empty() {
49                d.data.tp.set_checked(tp.into_seq_type());
50            } else {
51                d.data
52                    .tp
53                    .set_checked(tp.into_ranged_seq_type(d.data.sequence_range.iter().cloned()));
54            }
55        } else {
56            d.data.tp.set_checked(tp);
57        }
58    }
59    if let Some(df) = d.data.df.get_parsed()
60        && !d.data.df.has_checked()
61    {
62        d.data.df.set_checked(prepare(df.clone()));
63    }
64
65    Ok(d)
66}
67
68impl<Split: SplitStrategy> Checker<Split> {
69    pub(crate) fn get_module_like(&self, uri: &ModuleUri) -> Result<ModuleLike, ()> {
70        if uri.is_top() {
71            if let Some(m) = self.modules.get(uri) {
72                return Ok(ModuleLike::Module(m.clone()));
73            }
74            let ModuleLike::Module(m) = self.backend.get_module(uri).map_err(|_| ())? else {
75                // SAFETY: uri.is_top()
76                unsafe { unreachable_unchecked() }
77            };
78            m.initialize(&mut |u| self.get_module_like(u).ok())
79                .map_err(|_| ())?;
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(inner.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    pub fn get_symbol_like(
114        &self,
115        uri: &SymbolUri,
116        prepare: impl Fn(Term) -> Term,
117    ) -> Result<SharedSymbolLike, ()> {
118        if self.current.iter().any(|u| u == uri) {
119            return Err(());
120        }
121        let uri = uri.as_simple_module();
122
123        let Some(d) = self
124            .get_module(&uri.module)
125            .map_err(|_| ())?
126            .get_symbol_like(uri.name())
127        else {
128            return Err(());
129        };
130        if let SharedSymbolLike::Symbol(d) = &d {
131            if let Some(tp) = d.data.tp.get_parsed()
132                && !d.data.tp.has_checked()
133            {
134                d.data.tp.set_checked(prepare(tp.clone()));
135            }
136            if let Some(df) = d.data.df.get_parsed()
137                && !d.data.df.has_checked()
138            {
139                d.data.df.set_checked(prepare(df.clone()));
140            }
141        }
142        Ok(d)
143    }
144
145    pub(crate) fn get_symbol(
146        &self,
147        uri: &SymbolUri,
148        prepare: impl Fn(Term) -> Term,
149    ) -> Result<SharedDeclaration<Symbol>, ()> {
150        if self.current.iter().any(|u| u == uri) {
151            return Err(());
152        }
153        let uri = uri.as_simple_module();
154        let Some(d) = self.get_module(&uri.module)?.get_as::<Symbol>(uri.name()) else {
155            return Err(());
156        };
157        if let Some(tp) = d.data.tp.get_parsed()
158            && !d.data.tp.has_checked()
159        {
160            d.data.tp.set_checked(prepare(tp.clone()));
161        }
162        if let Some(df) = d.data.df.get_parsed()
163            && !d.data.df.has_checked()
164        {
165            d.data.df.set_checked(prepare(df.clone()));
166        }
167        Ok(d)
168        //.ok_or();
169    }
170
171    pub(crate) fn get_variable(
172        &self,
173        uri: &DocumentElementUri,
174    ) -> Result<SharedDocumentElement<VariableDeclaration>, ()> {
175        get_variable(&self.backend, &self.documents, &self.current, uri, |t| {
176            self.prepare(None, t).1
177        })
178        /*
179        fn get<Split: SplitStrategy>(
180            slf: &Checker<Split>,
181            uri: &DocumentElementUri,
182        ) -> Result<SharedDocumentElement<VariableDeclaration>, ()> {
183            let doc = uri.document_uri();
184            if let Some(d) = slf.documents.get(doc) {
185                return d.get_as(uri.name()).ok_or(());
186            }
187            let doc = slf.backend.get_document(doc).map_err(|_| ())?;
188            slf.documents.insert(doc.clone());
189            doc.get_as(uri.name()).ok_or(())
190        }
191        if self.current.iter().any(|u| u == uri) {
192            return Err(());
193        }
194        let d = get(self, uri)?;
195
196        if let Some(tp) = d.data.tp.get_parsed()
197            && !d.data.tp.has_checked()
198        {
199            let (_, tp) = self.prepare(None, tp.clone());
200
201            if d.data.is_seq && tp.as_sequence_type().is_none() {
202                d.data.tp.set_checked(tp.into_seq_type());
203            } else {
204                d.data.tp.set_checked(tp);
205            }
206        }
207        if let Some(df) = d.data.df.get_parsed()
208            && !d.data.df.has_checked()
209        {
210            d.data.df.set_checked(self.prepare(None, df.clone()).1);
211        }
212
213        Ok(d)
214         */
215    }
216}
217
218impl<Split: SplitStrategy> CheckRef<'_, '_, Split> {
219    /// ### Errors
220    pub(crate) fn get_declaration<T: IsDeclaration>(
221        &self,
222        uri: &SymbolUri,
223    ) -> Result<SharedDeclaration<T>, ()> {
224        self.top
225            .get_module(&uri.module)?
226            .get_as::<T>(uri.name())
227            .ok_or(())
228    }
229
230    /// ### Errors
231    #[inline]
232    pub(crate) fn get_symbol(&self, uri: &SymbolUri) -> Result<SharedDeclaration<Symbol>, ()> {
233        self.top.get_symbol(uri, |t| self.prepare(t, None).1)
234    }
235
236    pub(crate) fn get_symbol_type(&mut self, uri: &SymbolUri) -> Option<Term> {
237        let Ok(s) = self.top.get_symbol_like(uri, |t| self.prepare(t, None).1) else {
238            self.failure(format!("Symbol not found: {uri}"));
239            return None;
240        };
241        match s {
242            SharedSymbolLike::Symbol(s) => s.data.tp.checked_or_parsed().map(|(t, _)| t),
243            SharedSymbolLike::MathStructure(_) => {
244                self.top.rules.inference().iter().find_map(|rl| {
245                    rl.as_any()
246                        .downcast_ref::<super::records::RecordUniverse>()
247                        .map(|rl| rl.0.clone())
248                })
249            }
250            _ => None,
251        }
252
253        /*
254        let Ok(s) = self.get_symbol(uri) else {
255            self.failure(format!("Symbol not found: {uri}"));
256            return None;
257        };
258        s.data.tp.checked_or_parsed().map(|(t, _)| t)
259         */
260    }
261    pub(crate) fn get_symbol_definiens(&mut self, uri: &SymbolUri) -> Option<Term> {
262        let Ok(s) = self.get_symbol(uri) else {
263            self.failure(format!("Symbol not found: {uri}"));
264            return None;
265        };
266
267        /*
268        if uri.name.as_ref() == "universal quantifier" {
269            use std::io::{Read, Write};
270            let bt = std::backtrace::Backtrace::force_capture();
271            let bts = bt.to_string();
272            if !bts.contains("simplify_implicit") {
273                println!("----------------------------------------");
274                for l in bts.split('\n').rev() {
275                    println!("{l}");
276                }
277                std::io::stdout().flush();
278                let _ = std::io::stdin().read(&mut [0]);
279            }
280        } */
281        let t = s.data.df.checked_or_parsed();
282        if t.is_none() {
283            self.comment(format!("Symbol has no definiens: {uri}"));
284        }
285        t.map(|(t, _)| t)
286    }
287
288    /// ### Errors
289    #[inline]
290    pub fn get_variable(
291        &self,
292        uri: &DocumentElementUri,
293    ) -> Result<SharedDocumentElement<VariableDeclaration>, ()> {
294        self.top.get_variable(uri)
295    }
296
297    pub(crate) fn get_var_definiens(&mut self, var: &Variable) -> Option<Term> {
298        if let Some(id) = is_solvable_var(var) {
299            return self.get_solution(id);
300        }
301        for v in self.iter_context() {
302            match (v, var) {
303                (
304                    ComponentVar {
305                        var: Variable::Name { name, .. },
306                        df,
307                        ..
308                    },
309                    Variable::Name { name: n2, .. },
310                ) if *name == *n2 => {
311                    return df.clone().map(|t| self.subst(t));
312                }
313                (
314                    ComponentVar {
315                        var: Variable::Name { name, .. },
316                        df,
317                        ..
318                    },
319                    Variable::Ref { declaration, .. },
320                ) if name.as_ref() == declaration.name().last() && df.is_some() => {
321                    return df.clone().map(|t| self.subst(t));
322                }
323                (
324                    ComponentVar {
325                        var: Variable::Ref { declaration, .. },
326                        df,
327                        ..
328                    },
329                    Variable::Name { name, .. },
330                ) if name.as_ref() == declaration.name().last() => {
331                    return if df.is_some() {
332                        df.clone().map(|t| self.subst(t))
333                    } else {
334                        self.get_variable(declaration)
335                            .ok()?
336                            .data
337                            .df
338                            .checked_or_parsed()
339                            .map(|(t, _)| t)
340                    };
341                }
342                (
343                    ComponentVar {
344                        var: Variable::Ref { declaration, .. },
345                        df,
346                        ..
347                    },
348                    Variable::Ref {
349                        declaration: d2, ..
350                    },
351                ) if *declaration == *d2 => {
352                    return if df.is_some() {
353                        df.clone().map(|t| self.subst(t))
354                    } else {
355                        self.get_variable(declaration)
356                            .ok()?
357                            .data
358                            .df
359                            .checked_or_parsed()
360                            .map(|(t, _)| t)
361                    };
362                }
363                _ => (),
364            }
365        }
366        if let Variable::Ref { declaration, .. } = var {
367            self.get_variable(declaration)
368                .ok()?
369                .data
370                .df
371                .checked_or_parsed()
372                .map(|(t, _)| t)
373        } else {
374            None
375        }
376    }
377}
ftml_solver/impls/backend.rs

ftml_solver/impls/
backend.rs
