ftml_solver/impls/
preparation.rs

1use crate::{
2    CheckRef,
3    impls::{records::Record, solving::Solutions},
4    rules::implicits::{ImplicitExtApp, ImplicitExtBound, ImplicitExtTerm},
5    split::SplitStrategy,
6};
7use either::Either;
8use ftml_ontology::{
9    domain::{
10        SharedDeclaration,
11        declarations::{morphisms::Morphism, symbols::Symbol},
12    },
13    narrative::{SharedDocumentElement, elements::VariableDeclaration},
14    terms::{
15        ApplicationTerm, Argument, BindingTerm, BoundArgument, ComponentVar, IsTerm, MaybeSequence,
16        OpaqueTerm, Term, Variable, helpers::IntoTerm, sequences::Sequence, termpaths::TermPath,
17    },
18};
19
20impl<Split: SplitStrategy> CheckRef<'_, '_, Split> {
21    #[inline]
22    #[must_use]
23    pub const fn rules(&self) -> &crate::rules::RuleSet<Split> {
24        &self.top.rules
25    }
26
27    pub(crate) fn prepare(&self, t: Term, path: Option<&mut TermPath>) -> (Solutions, Term) {
28        let mut cp = self.copied();
29        let mut ncp = cp.get_ref();
30        let old = ncp.context.take();
31        let r = ncp.prepare_i(t, path.map(|p| (p.inner_mut(), 0)));
32        ncp.context.set(old);
33        drop(ncp);
34        let sols = std::mem::take(&mut cp.solutions);
35        (sols, r)
36    }
37
38    pub(crate) fn revert_prepare(&self, t: Term) -> Term {
39        tracing::trace!("reverting preparation {:?}", t.debug_short());
40        let mut cp = self.copied();
41        let mut ncp = cp.get_ref();
42        let old = ncp.context.take();
43        let r = ncp.revert_i(t);
44        ncp.context.set(old);
45        r
46    }
47
48    /*
49    pub(crate) fn bind_implicits(&mut self, nt: Term) -> Term {
50        tracing::trace!("Binding implicits for {:?}", nt.debug_short());
51        let mut allvars = nt
52            .free_variables()
53            .into_iter()
54            .cloned()
55            .collect::<SmallVec<_, 4>>();
56        let mut curr_idx = 0;
57        if allvars.is_empty() {
58            return nt;
59        }
60        while curr_idx < allvars.len() {
61            if let Variable::Ref { declaration, .. } = &allvars[curr_idx]
62                && let Ok(v) = self.get_variable(declaration)
63                && let Some((tp, _)) = v.data.tp.checked_or_parsed()
64            {
65                let vars = tp.free_variables();
66                let mut changed = false;
67                for v in vars {
68                    if !allvars[..curr_idx].contains(v) {
69                        allvars.insert(curr_idx, v.clone());
70                        changed = true;
71                    }
72                }
73                if changed {
74                    continue;
75                }
76            }
77            curr_idx += 1;
78        }
79        tracing::trace!("All variables: {allvars:?}");
80
81        let mut ctx = smallvec::SmallVec::<_, 4>::new();
82        for v in allvars {
83            if !ctx.iter().any(|(var, _)| *var == v) {
84                let name = self.new_solvable();
85                let Variable::Name { name: id, .. } = &name else {
86                    // SAFETY: new_solvable always returns Variable::Name
87                    unsafe { unreachable_unchecked() }
88                };
89                let tp = self.infer_var_type_i(&v);
90                if let Some(tp) = tp {
91                    self.comment(format!("Solving type of {id}"));
92                    self.solve_type(id.clone(), tp / ctx.as_slice());
93                }
94
95                ctx.push((
96                    v,
97                    Term::Var {
98                        variable: name,
99                        presentation: None,
100                    },
101                ));
102            }
103        }
104        if ctx.is_empty() {
105            return nt;
106        }
107        tracing::trace!("New context: {ctx:?}");
108        let n = nt / ctx.as_slice();
109        tracing::trace!("Implicitified: {:?}", n.debug_short());
110        n
111    }
112     */
113
114    pub fn get_head(
115        &self,
116        t: &Term,
117    ) -> Option<Either<SharedDeclaration<Symbol>, SharedDocumentElement<VariableDeclaration>>> {
118        let head = t.head()?;
119        Some(match head {
120            Either::Left(uri) => Either::Left(self.get_symbol(uri).ok()?),
121            Either::Right(Variable::Ref { declaration, .. }) => {
122                Either::Right(self.get_variable(declaration).ok()?)
123            }
124            either::Right(Variable::Name { .. }) => return None,
125        })
126    }
127
128    /*
129    fn push_down_implicits(term: Term) -> Term {
130        if let Term::Application(ref app) = term
131            && app.head.is(&*ftml_uris::metatheory::APPLY_IMPLICIT)
132            && let [
133                Argument::Simple(f @ (Term::Application(_) | Term::Bound(_))),
134                Argument::Sequence(MaybeSequence::Seq(args)),
135            ] = &*app.arguments
136        {
137            let mut iter = args.iter();
138            let next = if let Term::Application(fapp) = f {
139                let napp = fapp
140                    .head
141                    .clone()
142                    .apply_implicits(args.len(), |_| iter.next().expect("bug").clone());
143                Term::Application(ApplicationTerm::new(
144                    napp,
145                    fapp.arguments.clone(),
146                    fapp.presentation.clone(),
147                ))
148            } else if let Term::Bound(fapp) = f {
149                let napp = fapp
150                    .head
151                    .clone()
152                    .apply_implicits(args.len(), |_| iter.next().expect("bug").clone());
153                Term::Bound(BindingTerm::new(
154                    napp,
155                    fapp.arguments.clone(),
156                    fapp.presentation.clone(),
157                ))
158            } else {
159                unreachable!("bug");
160            };
161            Self::push_down_implicits(next)
162        } else {
163            term
164        }
165    }
166     */
167
168    fn prepare_i(
169        &mut self,
170        mut t: Term,
171        mut path: Option<(&mut smallvec::SmallVec<u8, 16>, usize)>,
172    ) -> Term {
173        tracing::trace!("preparing {:?}", t.debug_short());
174        //let mut t = Self::prepare_seqs(t);
175        //let mut t = Self::push_down_implicits(t);
176        if t.unapply_implicits(false).is_some() {
177            return t;
178        }
179        match &t {
180            Term::Field(f) => {
181                if let Some(r) = self.scoped(|slf| {
182                    if let Ok(r) = Record::from_term(&f.record, f.record_type.as_ref(), slf)
183                    && let Some(sym) = r.get_type().get_symbol(&f.key)
184                    //&& sym.data.tp.has_checked()
185                    && let Some(Some(vars)) = sym
186                        .data
187                        .tp
188                        .with_checked(|t| Some(t.get_bound_implicits()?.1.len()))
189                    {
190                        Some(t.clone().apply_implicits(vars, |_| slf.new_solvable()))
191                    } else {
192                        None
193                    }
194                }) {
195                    return r;
196                }
197            }
198            Term::Symbol { uri, presentation } => {
199                return if let Ok(sym) = self.get_symbol(uri)
200                    && sym.data.tp.has_checked()
201                {
202                    sym.data
203                        .tp
204                        .with_checked(|t| {
205                            let (_, vars) = t.get_bound_implicits()?;
206                            Some(
207                                Term::Symbol {
208                                    uri: uri.clone(),
209                                    presentation: presentation.clone(),
210                                }
211                                .apply_implicits(vars.len(), |_| self.new_solvable()),
212                            )
213                        })
214                        .flatten()
215                        .unwrap_or(t)
216                } else {
217                    t
218                };
219            }
220            Term::Var { .. } => return t,
221            _ => (),
222        }
223
224        for rl in self.top.rules.preparation() {
225            if !rl.applicable(self, &t) {
226                continue;
227            }
228            let path = match &mut path {
229                Some((p, t)) => Some((&mut **p, *t)),
230                _ => None,
231            };
232            match rl.apply(self, t, path) {
233                std::ops::ControlFlow::Break(t) => return t,
234                std::ops::ControlFlow::Continue(tm) => {
235                    t = tm;
236                }
237            }
238            tracing::trace!("Rule {rl:?} applied; result: {:?}", t.debug_short());
239        }
240        self.prepare_recurse(t, |s, t, p| s.prepare_i(t, p), path)
241    }
242
243    fn revert_i(&mut self, t: Term) -> Term {
244        match &t {
245            Term::Application(b) if b.head.unapply_implicits(true).is_some() => {
246                // SAFETY: pattern match
247                let (t, args) = unsafe { b.head.unapply_implicits(true).unwrap_unchecked() };
248                {
249                    return self.revert_i(
250                        Term::Application(ApplicationTerm::new(
251                            t.clone(),
252                            b.arguments.clone(),
253                            b.presentation.clone(),
254                        ))
255                        .apply_implicits(args.len(), |i| args[i].clone()),
256                    );
257                }
258            }
259            Term::Bound(b) if b.head.unapply_implicits(true).is_some() => {
260                // SAFETY: pattern match
261                let (t, args) = unsafe { b.head.unapply_implicits(true).unwrap_unchecked() };
262                {
263                    return self.revert_i(
264                        Term::Bound(BindingTerm::new(
265                            t.clone(),
266                            b.arguments.clone(),
267                            b.presentation.clone(),
268                        ))
269                        .apply_implicits(args.len(), |i| args[i].clone()),
270                    );
271                }
272            }
273
274            Term::Application(a) if a.unapply_implicits(true).is_some() => {
275                // SAFETY: pattern match
276                let (t, _) = unsafe { a.unapply_implicits(true).unwrap_unchecked() };
277                return t.clone();
278            }
279            Term::Symbol { .. } | Term::Var { .. } => return t,
280            _ => (),
281        }
282
283        let mut tm = t;
284
285        for rl in self.top.rules.preparation().iter().rev() {
286            // SAFETY: not yet replaced
287            if !rl.applicable_revert(self, &tm) {
288                continue;
289            }
290            tm = match rl.revert(self, tm) {
291                std::ops::ControlFlow::Break(t) => return t,
292                std::ops::ControlFlow::Continue(t) => t,
293            };
294            tracing::trace!("Rule {rl:?} applied; result: {:?}", tm.debug_short());
295        }
296        self.prepare_recurse(tm, |s, t, _| s.revert_i(t), None)
297    }
298
299    fn prepare_recurse(
300        &mut self,
301        term: Term,
302        then: fn(
303            &mut CheckRef<'_, '_, Split>,
304            Term,
305            Option<(&mut smallvec::SmallVec<u8, 16>, usize)>,
306        ) -> Term,
307        mut path: Option<(&mut smallvec::SmallVec<u8, 16>, usize)>,
308    ) -> Term {
309        tracing::trace!("Recursing {:?}", term.debug_short());
310        match term {
311            Term::Opaque(ot) => Term::Opaque(OpaqueTerm::new(
312                ot.node.clone(),
313                ot.terms
314                    .iter()
315                    .enumerate()
316                    .map(|(i, t)| then(self, t.clone(), get_path(&mut path, i)))
317                    .collect(),
318            )),
319            Term::Application(a) => Term::Application(ApplicationTerm::new(
320                then(self, a.head.clone(), get_path(&mut path, 0)),
321                {
322                    let mut idx = 0;
323                    a.arguments
324                        .iter()
325                        .map(|arg| match arg {
326                            Argument::Simple(t) => Argument::Simple(then(
327                                self,
328                                t.clone(),
329                                get_path(&mut path, {
330                                    idx += 1;
331                                    idx
332                                }),
333                            )),
334                            Argument::Sequence(MaybeSequence::One(t)) => {
335                                Argument::Sequence(MaybeSequence::One(then(
336                                    self,
337                                    t.clone(),
338                                    get_path(&mut path, {
339                                        idx += 1;
340                                        idx
341                                    }),
342                                )))
343                            }
344                            Argument::Sequence(MaybeSequence::Seq(ts)) => {
345                                idx += 1;
346                                let mut npath = get_path(&mut path, idx);
347                                Argument::Sequence(MaybeSequence::Seq(
348                                    ts.iter()
349                                        .cloned()
350                                        .enumerate()
351                                        .map(|(i, t)| then(self, t, get_path(&mut npath, i)))
352                                        .collect(),
353                                ))
354                            }
355                        })
356                        .collect()
357                },
358                a.presentation.clone(),
359            )),
360            Term::Bound(b) => Term::Bound(BindingTerm::new(
361                then(self, b.head.clone(), get_path(&mut path, 0)),
362                self.scoped(|slf| {
363                    let mut idx = 0;
364                    b.arguments
365                        .iter()
366                        .map(|arg| match arg {
367                            BoundArgument::Simple(t) => BoundArgument::Simple(then(
368                                slf,
369                                t.clone(),
370                                get_path(&mut path, {
371                                    idx += 1;
372                                    idx
373                                }),
374                            )),
375                            BoundArgument::Sequence(MaybeSequence::One(t)) => {
376                                BoundArgument::Sequence(MaybeSequence::One(then(
377                                    slf,
378                                    t.clone(),
379                                    get_path(&mut path, {
380                                        idx += 1;
381                                        idx
382                                    }),
383                                )))
384                            }
385                            BoundArgument::Sequence(MaybeSequence::Seq(ts)) => {
386                                idx += 1;
387                                let mut npath = get_path(&mut path, idx);
388                                BoundArgument::Sequence(MaybeSequence::Seq(
389                                    ts.iter()
390                                        .cloned()
391                                        .enumerate()
392                                        .map(|(i, t)| then(slf, t, get_path(&mut npath, i)))
393                                        .collect(),
394                                ))
395                            }
396                            BoundArgument::Bound(cv) => BoundArgument::Bound(slf.prepare_cv(
397                                cv,
398                                then,
399                                get_path(&mut path, {
400                                    idx += 1;
401                                    idx
402                                }),
403                            )),
404                            BoundArgument::BoundSeq(MaybeSequence::One(cv)) => {
405                                BoundArgument::BoundSeq(MaybeSequence::One(slf.prepare_cv(
406                                    cv,
407                                    then,
408                                    get_path(&mut path, {
409                                        idx += 1;
410                                        idx
411                                    }),
412                                )))
413                            }
414                            BoundArgument::BoundSeq(MaybeSequence::Seq(vars)) => {
415                                idx += 1;
416                                let mut npath = get_path(&mut path, idx);
417                                BoundArgument::BoundSeq(MaybeSequence::Seq(
418                                    vars.iter()
419                                        .enumerate()
420                                        .map(|(i, cv)| {
421                                            slf.prepare_cv(cv, then, get_path(&mut npath, i))
422                                        })
423                                        .collect(),
424                                ))
425                            }
426                        })
427                        .collect()
428                }),
429                b.presentation.clone(),
430            )),
431            t => t,
432        }
433    }
434
435    #[allow(clippy::single_match_else)]
436    fn prepare_cv(
437        &mut self,
438        cv: &ComponentVar,
439        then: fn(&mut Self, Term, Option<(&mut smallvec::SmallVec<u8, 16>, usize)>) -> Term,
440        mut path: Option<(&mut smallvec::SmallVec<u8, 16>, usize)>,
441    ) -> ComponentVar {
442        tracing::trace!("preparing bound variable {}", cv.var.name());
443        let mut next = 0;
444        let tp = match &cv.tp {
445            Some(t) => {
446                next += 1;
447                Some(then(self, t.clone(), get_path(&mut path, 0)))
448            }
449            None => {
450                let r = self.infer_var_type_i(&cv.var);
451                if r.is_some()
452                    && let Some((p, i)) = &mut path
453                    && let Some(i) = p.get_mut(*i)
454                {
455                    *i += 1;
456                    next += 1;
457                }
458                r
459            }
460        };
461        let df = match &cv.df {
462            Some(t) => Some(then(self, t.clone(), get_path(&mut path, next))),
463            None => {
464                let r = self.get_var_definiens(&cv.var);
465                if r.is_some()
466                    && let Some((p, i)) = &mut path
467                    && let Some(i) = p.get_mut(*i)
468                {
469                    *i += 1;
470                    next += 1;
471                }
472                r
473            }
474        };
475        let cv = ComponentVar {
476            var: cv.var.clone(),
477            tp,
478            df,
479        };
480        tracing::trace!("Extending context");
481        self.extend_context(cv.clone());
482        tracing::trace!("Done");
483        cv
484    }
485}
486
487fn get_path<'a, 'b>(
488    op: &'a mut Option<(&'b mut smallvec::SmallVec<u8, 16>, usize)>,
489    idx: usize,
490) -> Option<(&'a mut smallvec::SmallVec<u8, 16>, usize)> {
491    op.as_mut().and_then(|(s, i)| {
492        if s.get(*i).copied() == Some(idx as u8) {
493            Some((&mut **s, *i + 1))
494        } else {
495            None
496        }
497    })
498}
ftml_solver/impls/preparation.rs

ftml_solver/impls/
preparation.rs
