ftml_solver/impls/
preparation.rs

1use crate::{
2    CheckRef,
3    impls::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        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    fn push_down_implicits(term: Term) -> Term {
129        if let Term::Application(ref app) = term
130            && app.head.is(&*ftml_uris::metatheory::APPLY_IMPLICIT)
131            && let [
132                Argument::Simple(f @ (Term::Application(_) | Term::Bound(_))),
133                Argument::Sequence(MaybeSequence::Seq(args)),
134            ] = &*app.arguments
135        {
136            let mut iter = args.iter();
137            let next = if let Term::Application(fapp) = f {
138                let napp = fapp
139                    .head
140                    .clone()
141                    .apply_implicits(args.len(), |_| iter.next().expect("bug").clone());
142                Term::Application(ApplicationTerm::new(
143                    napp,
144                    fapp.arguments.clone(),
145                    fapp.presentation.clone(),
146                ))
147            } else if let Term::Bound(fapp) = f {
148                let napp = fapp
149                    .head
150                    .clone()
151                    .apply_implicits(args.len(), |_| iter.next().expect("bug").clone());
152                Term::Bound(BindingTerm::new(
153                    napp,
154                    fapp.arguments.clone(),
155                    fapp.presentation.clone(),
156                ))
157            } else {
158                unreachable!("bug");
159            };
160            Self::push_down_implicits(next)
161        } else {
162            term
163        }
164    }
165
166    fn prepare_i(
167        &mut self,
168        mut t: Term,
169        mut path: Option<(&mut smallvec::SmallVec<u8, 16>, usize)>,
170    ) -> Term {
171        tracing::trace!("preparing {:?}", t.debug_short());
172        //let mut t = Self::prepare_seqs(t);
173        //let mut t = Self::push_down_implicits(t);
174        if t.unapply_implicits().is_some() {
175            return t;
176        }
177        match &t {
178            Term::Symbol { uri, presentation } => {
179                return if let Ok(sym) = self.get_symbol(uri)
180                    && sym.data.tp.has_checked()
181                {
182                    sym.data
183                        .tp
184                        .with_checked(|t| {
185                            let (_, vars) = t.get_bound_implicits()?;
186                            Some(
187                                Term::Symbol {
188                                    uri: uri.clone(),
189                                    presentation: presentation.clone(),
190                                }
191                                .apply_implicits(vars.len(), |_| self.new_solvable()),
192                            )
193                        })
194                        .flatten()
195                        .unwrap_or(t)
196                } else {
197                    t
198                };
199            }
200            Term::Var { .. } => return t,
201            _ => (),
202        }
203
204        for rl in self.top.rules.preparation() {
205            if !rl.applicable(self, &t) {
206                continue;
207            }
208            let path = match &mut path {
209                Some((p, t)) => Some((&mut **p, *t)),
210                _ => None,
211            };
212            match rl.apply(self, t, path) {
213                std::ops::ControlFlow::Break(t) => return t,
214                std::ops::ControlFlow::Continue(tm) => {
215                    t = tm;
216                }
217            }
218            tracing::trace!("Rule {rl:?} applied; result: {:?}", t.debug_short());
219        }
220        self.prepare_recurse(t, |s, t, p| s.prepare_i(t, p), path)
221    }
222
223    fn revert_i(&mut self, t: Term) -> Term {
224        match &t {
225            Term::Application(b) if b.head.unapply_implicits().is_some() => {
226                // SAFETY: pattern match
227                let (t, args) = unsafe { b.head.unapply_implicits().unwrap_unchecked() };
228                {
229                    return self.revert_i(
230                        Term::Application(ApplicationTerm::new(
231                            t.clone(),
232                            b.arguments.clone(),
233                            b.presentation.clone(),
234                        ))
235                        .apply_implicits(args.len(), |i| args[i].clone()),
236                    );
237                }
238            }
239            Term::Bound(b) if b.head.unapply_implicits().is_some() => {
240                // SAFETY: pattern match
241                let (t, args) = unsafe { b.head.unapply_implicits().unwrap_unchecked() };
242                {
243                    return self.revert_i(
244                        Term::Bound(BindingTerm::new(
245                            t.clone(),
246                            b.arguments.clone(),
247                            b.presentation.clone(),
248                        ))
249                        .apply_implicits(args.len(), |i| args[i].clone()),
250                    );
251                }
252            }
253
254            Term::Application(a) if a.unapply_implicits().is_some() => {
255                // SAFETY: pattern match
256                let (t, _) = unsafe { a.unapply_implicits().unwrap_unchecked() };
257                return t.clone();
258            }
259            Term::Symbol { .. } | Term::Var { .. } => return t,
260            _ => (),
261        }
262
263        let mut tm = t;
264
265        for rl in self.top.rules.preparation().iter().rev() {
266            // SAFETY: not yet replaced
267            if !rl.applicable_revert(self, &tm) {
268                continue;
269            }
270            tm = match rl.revert(self, tm) {
271                std::ops::ControlFlow::Break(t) => return t,
272                std::ops::ControlFlow::Continue(t) => t,
273            };
274            tracing::trace!("Rule {rl:?} applied; result: {:?}", tm.debug_short());
275        }
276        self.prepare_recurse(tm, |s, t, _| s.revert_i(t), None)
277    }
278
279    fn prepare_recurse(
280        &mut self,
281        term: Term,
282        then: fn(
283            &mut CheckRef<'_, '_, Split>,
284            Term,
285            Option<(&mut smallvec::SmallVec<u8, 16>, usize)>,
286        ) -> Term,
287        mut path: Option<(&mut smallvec::SmallVec<u8, 16>, usize)>,
288    ) -> Term {
289        tracing::trace!("Recursing {:?}", term.debug_short());
290        match term {
291            Term::Application(a) => {
292                if let Term::Symbol { uri, .. } = &a.head
293                    && let Ok(m) = self.get_declaration::<Morphism>(uri)
294                {
295                    // TODO @Marcel
296                }
297                Term::Application(ApplicationTerm::new(
298                    then(self, a.head.clone(), get_path(&mut path, 0)),
299                    {
300                        let mut idx = 0;
301                        a.arguments
302                            .iter()
303                            .map(|arg| match arg {
304                                Argument::Simple(t) => Argument::Simple(then(
305                                    self,
306                                    t.clone(),
307                                    get_path(&mut path, {
308                                        idx += 1;
309                                        idx
310                                    }),
311                                )),
312                                Argument::Sequence(MaybeSequence::One(t)) => {
313                                    Argument::Sequence(MaybeSequence::One(then(
314                                        self,
315                                        t.clone(),
316                                        get_path(&mut path, {
317                                            idx += 1;
318                                            idx
319                                        }),
320                                    )))
321                                }
322                                Argument::Sequence(MaybeSequence::Seq(ts)) => {
323                                    idx += 1;
324                                    let mut npath = get_path(&mut path, idx);
325                                    Argument::Sequence(MaybeSequence::Seq(
326                                        ts.iter()
327                                            .cloned()
328                                            .enumerate()
329                                            .map(|(i, t)| then(self, t, get_path(&mut npath, i)))
330                                            .collect(),
331                                    ))
332                                }
333                            })
334                            .collect()
335                    },
336                    a.presentation.clone(),
337                ))
338            }
339            Term::Bound(b) => Term::Bound(BindingTerm::new(
340                then(self, b.head.clone(), get_path(&mut path, 0)),
341                self.scoped(|slf| {
342                    let mut idx = 0;
343                    b.arguments
344                        .iter()
345                        .map(|arg| match arg {
346                            BoundArgument::Simple(t) => BoundArgument::Simple(then(
347                                slf,
348                                t.clone(),
349                                get_path(&mut path, {
350                                    idx += 1;
351                                    idx
352                                }),
353                            )),
354                            BoundArgument::Sequence(MaybeSequence::One(t)) => {
355                                BoundArgument::Sequence(MaybeSequence::One(then(
356                                    slf,
357                                    t.clone(),
358                                    get_path(&mut path, {
359                                        idx += 1;
360                                        idx
361                                    }),
362                                )))
363                            }
364                            BoundArgument::Sequence(MaybeSequence::Seq(ts)) => {
365                                idx += 1;
366                                let mut npath = get_path(&mut path, idx);
367                                BoundArgument::Sequence(MaybeSequence::Seq(
368                                    ts.iter()
369                                        .cloned()
370                                        .enumerate()
371                                        .map(|(i, t)| then(slf, t, get_path(&mut npath, i)))
372                                        .collect(),
373                                ))
374                            }
375                            BoundArgument::Bound(cv) => BoundArgument::Bound(slf.prepare_cv(
376                                cv,
377                                then,
378                                get_path(&mut path, {
379                                    idx += 1;
380                                    idx
381                                }),
382                            )),
383                            BoundArgument::BoundSeq(MaybeSequence::One(cv)) => {
384                                BoundArgument::BoundSeq(MaybeSequence::One(slf.prepare_cv(
385                                    cv,
386                                    then,
387                                    get_path(&mut path, {
388                                        idx += 1;
389                                        idx
390                                    }),
391                                )))
392                            }
393                            BoundArgument::BoundSeq(MaybeSequence::Seq(vars)) => {
394                                idx += 1;
395                                let mut npath = get_path(&mut path, idx);
396                                BoundArgument::BoundSeq(MaybeSequence::Seq(
397                                    vars.iter()
398                                        .enumerate()
399                                        .map(|(i, cv)| {
400                                            slf.prepare_cv(cv, then, get_path(&mut npath, i))
401                                        })
402                                        .collect(),
403                                ))
404                            }
405                        })
406                        .collect()
407                }),
408                b.presentation.clone(),
409            )),
410            t => t,
411        }
412    }
413
414    #[allow(clippy::single_match_else)]
415    fn prepare_cv(
416        &mut self,
417        cv: &ComponentVar,
418        then: fn(&mut Self, Term, Option<(&mut smallvec::SmallVec<u8, 16>, usize)>) -> Term,
419        mut path: Option<(&mut smallvec::SmallVec<u8, 16>, usize)>,
420    ) -> ComponentVar {
421        tracing::trace!("preparing bound variable {}", cv.var.name());
422        let mut next = 0;
423        let tp = match &cv.tp {
424            Some(t) => {
425                next += 1;
426                Some(then(self, t.clone(), get_path(&mut path, 0)))
427            }
428            None => {
429                let r = self.infer_var_type_i(&cv.var);
430                if r.is_some()
431                    && let Some((p, i)) = &mut path
432                    && let Some(i) = p.get_mut(*i)
433                {
434                    *i += 1;
435                    next += 1;
436                }
437                r
438            }
439        };
440        let df = match &cv.df {
441            Some(t) => Some(then(self, t.clone(), get_path(&mut path, next))),
442            None => {
443                let r = self.get_var_definiens(&cv.var);
444                if r.is_some()
445                    && let Some((p, i)) = &mut path
446                    && let Some(i) = p.get_mut(*i)
447                {
448                    *i += 1;
449                    next += 1;
450                }
451                r
452            }
453        };
454        let cv = ComponentVar {
455            var: cv.var.clone(),
456            tp,
457            df,
458        };
459        tracing::trace!("Extending context");
460        self.extend_context(cv.clone());
461        tracing::trace!("Done");
462        cv
463    }
464}
465
466fn get_path<'a, 'b>(
467    op: &'a mut Option<(&'b mut smallvec::SmallVec<u8, 16>, usize)>,
468    idx: usize,
469) -> Option<(&'a mut smallvec::SmallVec<u8, 16>, usize)> {
470    op.as_mut().and_then(|(s, i)| {
471        if s.get(*i).copied() == Some(idx as u8) {
472            Some((&mut **s, *i + 1))
473        } else {
474            None
475        }
476    })
477}
ftml_solver/impls/preparation.rs

ftml_solver/impls/
preparation.rs
