ftml_solver/impls/
simplify.rs

1use std::borrow::Cow;
2
3use ftml_ontology::terms::{
4    ApplicationTerm, Argument, BindingTerm, BoundArgument, ComponentVar, MaybeSequence, Term,
5};
6use ftml_solver_trace::{CheckerRule, CheckingTask, traceref};
7
8use crate::{
9    CheckRef,
10    impls::solving::{TermExtSolvable, is_solvable_var},
11    rules::{
12        implicits::{ImplicitExtApp, ImplicitExtBound},
13        unknowns::beta_unknowns_cow,
14    },
15    split::SplitStrategy,
16};
17
18const LOOP_LIMIT: usize = 64;
19const RECURSION_LIMIT: usize = 64;
20const TOTAL_LIMIT: usize = 2048;
21
22impl<'t, Split: SplitStrategy> CheckRef<'t, '_, Split> {
23    pub fn simplify_full(&mut self, expand: bool, term: &'t Term) -> Option<Term> {
24        if matches!(term, Term::Symbol { .. } | Term::Number(_)) {
25            return None;
26        }
27        self./*wrap_check*/untraced(CheckingTask::Simplify(term), |slf| {
28            slf.simplify_full_i(expand, term,&mut 0,&mut 0)
29        }).inspect(|t| {
30            self.add_msg(traceref!("Simplified: ",t.clone()).into());
31        })
32    }
33    fn simplify_full_first(
34        &mut self,
35        expand: bool,
36        term: &'t Term,
37        recursion_limit: &mut usize,
38        total_limit: &mut usize,
39    ) -> Option<Cow<'t, Term>> {
40        match term {
41            Term::Symbol { uri, .. } if expand => self.get_symbol_definiens(uri).map(|t| {
42                self.comment("expanded definition");
43                Some(Cow::Owned(t))
44            })?,
45            Term::Var { variable, .. } => {
46                if let Some(name) = is_solvable_var(variable)
47                    && let Some(t) = self.get_solution(name)
48                {
49                    Some(Cow::Owned(t))
50                } else if expand && let Some(df) = self.get_var_definiens(variable) {
51                    Some(Cow::Owned(df))
52                } else {
53                    //println!("  : None");
54                    None
55                }
56            }
57            Term::Number(_) => {
58                //println!("  : None");
59                None
60            }
61            Term::Application(app) => {
62                let mut changed = false;
63                let nhead = self
64                    .simplify_full_i(true, &app.head, recursion_limit, total_limit)
65                    .map_or(Cow::Borrowed(&app.head), |t| {
66                        changed = true;
67                        Cow::Owned(t)
68                    });
69                let args = app
70                    .arguments
71                    .iter()
72                    .map(|a| {
73                        self.arg_full(expand, a, recursion_limit, total_limit)
74                            .map_or(Cow::Borrowed(a), |a| {
75                                changed = true;
76                                Cow::Owned(a)
77                            })
78                    })
79                    .collect::<Vec<_>>();
80                Some(if changed {
81                    Cow::Owned(Term::Application(ApplicationTerm::new(
82                        nhead.into_owned(),
83                        args.into_iter().map(Cow::into_owned).collect(),
84                        app.presentation.clone(),
85                    )))
86                } else {
87                    Cow::Borrowed(term)
88                })
89            }
90            Term::Bound(app) => {
91                let mut changed = false;
92                let nhead = self
93                    .simplify_full_i(true, &app.head, recursion_limit, total_limit)
94                    .map_or(Cow::Borrowed(&app.head), |t| {
95                        changed = true;
96                        Cow::Owned(t)
97                    });
98                let args = app
99                    .arguments
100                    .iter()
101                    .map(|a| {
102                        self.bound_arg_full(expand, a, recursion_limit, total_limit)
103                            .map_or(Cow::Borrowed(a), |a| {
104                                changed = true;
105                                Cow::Owned(a)
106                            })
107                    })
108                    .collect::<Vec<_>>();
109                Some(if changed {
110                    Cow::Owned(Term::Bound(BindingTerm::new(
111                        nhead.into_owned(),
112                        args.into_iter().map(Cow::into_owned).collect(),
113                        app.presentation.clone(),
114                    )))
115                } else {
116                    Cow::Borrowed(term)
117                })
118            }
119            _ => Some(Cow::Borrowed(term)),
120        }
121    }
122    fn simplify_full_i(
123        &mut self,
124        expand: bool,
125        term: &'t Term,
126        recursion_limit: &mut usize,
127        total_limit: &mut usize,
128    ) -> Option<Term> {
129        tracing::debug!(
130            "Fully Simplifying {:?} (expand:{expand})",
131            term.debug_short()
132        );
133        if expand && let Some(t) = self.simplify_implicit(term) {
134            //println!("  - implicits: {:?}", t.debug_short());
135            return Some(
136                self.scoped(|slf| slf.simplify_full_i(expand, &t, recursion_limit, total_limit))
137                    .unwrap_or(t),
138            );
139        }
140        /*if term.unapply_implicits().is_some() {
141            return None;
142        } else*/
143        //self.scoped(|slf| {
144        *recursion_limit += 1;
145        let Some(mut current) =
146            self.simplify_full_first(expand, term, recursion_limit, total_limit)
147        else {
148            *recursion_limit -= 1;
149            return None;
150        };
151        let mut loop_limit = 0;
152        loop {
153            loop_limit += 1;
154            *total_limit += 1;
155            if loop_limit >= LOOP_LIMIT
156                || *recursion_limit >= RECURSION_LIMIT
157                || *total_limit >= TOTAL_LIMIT
158            {
159                *recursion_limit -= 1;
160                return match current {
161                    Cow::Borrowed(_) => {
162                        //println!("  : None");
163                        None
164                    }
165                    Cow::Owned(t) => {
166                        //println!("  : {:?}", t.debug_short());
167                        Some(t)
168                    }
169                };
170            }
171            if let Some(next) = self.scoped(|slf| slf.simplify_one(expand, &current)) {
172                current = Cow::Owned(next);
173            } else {
174                return match current {
175                    Cow::Borrowed(_) => {
176                        //println!("  : None");
177                        *recursion_limit -= 1;
178                        None
179                    }
180                    Cow::Owned(t) => {
181                        //println!("  : {:?}", t.debug_short());
182                        let r = Some(
183                            self.scoped(|slf| {
184                                slf.simplify_full_i(expand, &t, recursion_limit, total_limit)
185                            })
186                            .unwrap_or(t),
187                        );
188                        *recursion_limit -= 1;
189                        r
190                    }
191                };
192            }
193        }
194        //})
195    }
196
197    pub fn simplify_until(
198        &mut self,
199        term: &'t Term,
200        mut until: impl FnMut(&Self, &Term) -> bool,
201    ) -> Option<Cow<'t, Term>> {
202        if until(self, term) {
203            return Some(Cow::Borrowed(term));
204        }
205        self.wrap_check(CheckingTask::Simplify(term), |slf| {
206            slf.simplify_until_i(term, until, &mut 0, &mut 0)
207        })
208    }
209    fn simplify_until_i(
210        &mut self,
211        term: &'t Term,
212        mut until: impl FnMut(&Self, &Term) -> bool,
213        recursion_limit: &mut usize,
214        total_limit: &mut usize,
215    ) -> Option<Cow<'t, Term>> {
216        if until(self, term) {
217            return Some(Cow::Borrowed(term));
218        }
219        let mut current = Cow::<'t, _>::Borrowed(term);
220        *recursion_limit += 1;
221        let mut loop_limit = 0;
222        loop {
223            loop_limit += 1;
224            *total_limit += 1;
225            if *recursion_limit >= RECURSION_LIMIT
226                || loop_limit >= LOOP_LIMIT
227                || *total_limit >= TOTAL_LIMIT
228            {
229                *recursion_limit -= 1;
230                return None;
231            }
232            let Some(next) = self.scoped(|slf| slf.simplify_one(true, &current)) else {
233                *recursion_limit -= 1;
234                //self.comment(format!("Final simplification: {:?}", current.debug_short()));
235                return None;
236            };
237            if until(self, &next) {
238                *recursion_limit -= 1;
239                return Some(Cow::Owned(next));
240            }
241            current = Cow::Owned(next);
242        }
243    }
244
245    pub(crate) fn simplify_rules<Rl: CheckerRule + ?Sized, R>(
246        &mut self,
247        rules: &'t [Box<Rl>],
248        term: &'t Term,
249        applicable: impl Fn(&Rl, &Term) -> bool,
250        apply: impl for<'s> Fn(CheckRef<'s, '_, Split>, &Rl, &'s Term) -> Option<R> + Send + Sync,
251    ) -> Option<R>
252    where
253        R: Send + Sync + std::fmt::Debug + Clone + 'static,
254    {
255        let mut applicables = smallvec::SmallVec::<_, 2>::default();
256        match self.simplify_until(term, |_, t| {
257            applicables = rules
258                .iter()
259                .filter_map(|rl| {
260                    if applicable(&**rl, t) {
261                        Some(&**rl)
262                    } else {
263                        None
264                    }
265                })
266                .collect();
267            !applicables.is_empty()
268        }) {
269            Some(Cow::Borrowed(term)) => {
270                if let Some(r) =
271                    Split::split(self, true, applicables, |slf, rl| apply(slf, rl, term))
272                {
273                    return Some(r);
274                }
275                self.simplify_one(true, term).and_then(|term| {
276                    self.scoped(|slf| slf.simplify_rules(rules, &term, applicable, apply))
277                })
278            }
279            Some(Cow::Owned(term)) => self.scoped(|slf| {
280                if let Some(r) =
281                    Split::split(slf, true, applicables, |slf, rl| apply(slf, rl, &term))
282                {
283                    return Some(r);
284                }
285                slf.simplify_one(true, &term).and_then(|term| {
286                    slf.scoped(|slf| slf.simplify_rules(rules, &term, applicable, apply))
287                })
288            }),
289            None => {
290                self.failure("No rule applicable");
291                None
292            }
293        }
294    }
295
296    pub(crate) fn simplify_until_two(
297        &mut self,
298        term1: &'t Term,
299        term2: &'t Term,
300        mut until: impl FnMut(&Self, &Term, &Term) -> bool,
301    ) -> Option<(Cow<'t, Term>, Cow<'t, Term>)> {
302        let mut left = true;
303        let mut right = true;
304        let mut next_left = true;
305        let mut t1 = Cow::Borrowed(term1);
306        let mut t2 = Cow::Borrowed(term2);
307        loop {
308            if next_left && left {
309                if until(self, &t1, &t2) {
310                    return Some((t1, t2));
311                }
312                next_left = false;
313                if let Some(next) = self.scoped(|slf| slf.simplify_one(true, &t1)) {
314                    t1 = Cow::Owned(next);
315                    continue;
316                }
317                left = false;
318            }
319            if right {
320                if until(self, &t1, &t2) {
321                    return Some((t1, t2));
322                }
323                next_left = true;
324                if let Some(next) = self.scoped(|slf| slf.simplify_one(true, &t2)) {
325                    t2 = Cow::Owned(next);
326                    continue;
327                }
328                right = false;
329                continue;
330            }
331            break;
332        }
333        self.add_msg(
334            traceref!(FAIL
335                "Final simplifications: ",
336                t1.into_owned(),
337                " and ",
338                t2.into_owned()
339            )
340            .into(),
341        );
342        None
343    }
344
345    pub(crate) fn simplify_rules_two<Rl: CheckerRule + ?Sized + 'static, R>(
346        &mut self,
347        rules: &'t [Box<Rl>],
348        term1: &'t Term,
349        term2: &'t Term,
350        applicable: impl Fn(&CheckRef<'_, '_, Split>, &Rl, &Term, &Term) -> bool,
351        apply: impl for<'s> Fn(CheckRef<'s, '_, Split>, &Rl, &'s Term, &'s Term) -> Option<R> + Sync,
352        abort: impl Fn(&Term, &Term) -> bool + Send + Sync,
353    ) -> either::Either<Option<R>, (Term, Term)>
354    where
355        R: Send + Sync + std::fmt::Debug + Clone + 'static,
356    {
357        //println!("Simplify rules two {{");
358        let mut applicables = smallvec::SmallVec::<_, 2>::default();
359        let mut left = true;
360        let mut right = true;
361        let mut next_left = true;
362        let mut t1 = Cow::Borrowed(term1);
363        let mut t2 = Cow::Borrowed(term2);
364        loop {
365            macro_rules! set {
366                () => {
367                    set!(NOBREAK);
368                    if !applicables.is_empty() {
369                        break;
370                    }
371                };
372                (NOBREAK) => {
373                    if abort(&*t1, &*t2) {
374                        //println!("}}");
375                        return either::Right((t1.into_owned(), t2.into_owned()));
376                    }
377                    applicables = rules
378                        .iter()
379                        .filter_map(|rl| {
380                            if applicable(self, &**rl, &*t1, &*t2) {
381                                Some(&**rl)
382                            } else {
383                                None
384                            }
385                        })
386                        .collect();
387                };
388            }
389            loop {
390                if next_left && left {
391                    set!();
392                    if right {
393                        next_left = false;
394                    }
395                    if let Some(next) = self.scoped(|slf| slf.simplify_one(true, &t1)) {
396                        t1 = Cow::Owned(next);
397                        continue;
398                    }
399                    left = false;
400                }
401                if right {
402                    set!();
403                    if left {
404                        next_left = true;
405                    }
406                    if let Some(next) = self.scoped(|slf| slf.simplify_one(true, &t2)) {
407                        t2 = Cow::Owned(next);
408                        continue;
409                    }
410                    right = false;
411                    if left {
412                        continue;
413                    }
414                }
415                break;
416            }
417
418            if applicables.is_empty() {
419                self.failure("No rule applicable");
420                self.add_msg(
421                    traceref!(FAIL
422                        "Final simplifications: ",
423                        t1.into_owned(),
424                        " and ",
425                        t2.into_owned()
426                    )
427                    .into(),
428                );
429                //println!("}}");
430                return either::Left(None);
431            }
432            if let Some(r) = self.scoped(|slf| {
433                Split::split(slf, true, std::mem::take(&mut applicables), |slf, rl| {
434                    apply(slf, rl, &t1, &t2)
435                })
436            }) {
437                //println!("}}");
438                return either::Left(Some(r));
439            }
440            if next_left && left {
441                if right {
442                    next_left = false;
443                }
444                if let Some(next) = self.scoped(|slf| slf.simplify_one(true, &t1)) {
445                    t1 = Cow::Owned(next);
446                    //set!(NOBREAK);
447                    continue;
448                }
449                left = false;
450            }
451            if right {
452                if left {
453                    next_left = true;
454                }
455                if let Some(next) = self.scoped(|slf| slf.simplify_one(true, &t2)) {
456                    t2 = Cow::Owned(next);
457                    //set!(NOBREAK);
458                    continue;
459                }
460                right = false;
461                if left {
462                    continue;
463                }
464            }
465            break;
466        }
467        self.failure("No rule applicable");
468        //println!("}}");
469        either::Left(None)
470    }
471
472    fn simplify_one(&mut self, expand: bool, term: &'t Term) -> Option<Term> {
473        if term.has_solvable() {
474            let nterm = self.subst(term.clone());
475            if *term != nterm {
476                return Some(nterm); //self.scoped(|slf| slf.simplify_one_i(expand, &nterm));
477            }
478        }
479        if let Cow::Owned(nterm) = beta_unknowns_cow(term)
480            && *term != nterm
481        {
482            return Some(nterm); //self.scoped(|slf| slf.simplify_one_i(expand, &nterm));
483        }
484        self.simplify_one_i(expand, term)
485    }
486    fn simplify_one_i(&mut self, expand: bool, term: &'t Term) -> Option<Term> {
487        /**/
488        let applicables = self
489            .top
490            .rules
491            .simplification()
492            .iter()
493            .filter_map(|rl| {
494                if rl.applicable(term) {
495                    Some(&**rl)
496                } else {
497                    None
498                }
499            })
500            .collect::<smallvec::SmallVec<_, 2>>();
501        match Split::split(self, false, applicables, |slf, rl| {
502            match rl.apply(slf, term) {
503                Ok(t) => Some(either::Left(t)),
504                Err(Some(v)) => Some(either::Right(v)),
505                _ => None,
506            }
507        }) {
508            Some(either::Left(t)) => return Some(t),
509            Some(_) => {
510                // TODO
511            }
512            None => (),
513        }
514
515        self.simplify_one_default(expand, term)
516    }
517
518    pub(crate) fn simplify_implicit(&mut self, term: &'t Term) -> Option<Term> {
519        if let Some((Term::Symbol { uri, .. }, args)) = term.unapply_implicits()
520            && let Some(def) = self.get_symbol_definiens(uri)
521            && let Some((def, vars)) = def.get_bound_implicits()
522            && args.len() == vars.len()
523        {
524            let mut substs = Vec::new();
525            for (ComponentVar { var, tp, .. }, arg) in vars.iter().zip(args) {
526                if let Some(tp) = tp {
527                    let tp: Cow<Term> = tp / &*substs;
528                    if self.scoped(|checker| checker.check_type(arg, &tp)) != Some(true) {
529                        return None;
530                    }
531                    substs.push((var.name(), arg));
532                }
533            }
534            let r = def / &*substs;
535            tracing::debug!("Unapplied implicits: {:?}", r.debug_short());
536            Some(r.into_owned())
537        } else {
538            None
539        }
540    }
541
542    fn simplify_one_default(&mut self, expand: bool, term: &'t Term) -> Option<Term> {
543        if expand && let Some(t) = self.simplify_implicit(term) {
544            return Some(t);
545        }
546        match term {
547            // Definition Expansion
548            Term::Symbol { uri, .. } if expand => self.get_symbol_definiens(uri).inspect(|_| {
549                self.comment("expanded definition");
550            }),
551            Term::Var { variable, .. } if expand || is_solvable_var(variable).is_some() => {
552                self.get_var_definiens(variable).inspect(|_| {
553                    self.comment("expanded definition");
554                })
555            }
556            Term::Application(app) => self.simplify_one(expand, &app.head).map(|nh| {
557                Term::Application(ApplicationTerm::new(
558                    nh,
559                    app.arguments.clone(),
560                    app.presentation.clone(),
561                ))
562            }),
563            Term::Bound(app) => self.simplify_one(true, &app.head).map(|nh| {
564                Term::Bound(BindingTerm::new(
565                    nh,
566                    app.arguments.clone(),
567                    app.presentation.clone(),
568                ))
569            }),
570            _ => None,
571        }
572    }
573
574    fn arg_full(
575        &mut self,
576        expand: bool,
577        arg: &'t Argument,
578        recursion_limit: &mut usize,
579        total_limit: &mut usize,
580    ) -> Option<Argument> {
581        match arg {
582            Argument::Simple(t) => self
583                .simplify_full_i(expand, t, recursion_limit, total_limit)
584                .map(Argument::Simple),
585            Argument::Sequence(MaybeSequence::One(t)) => self
586                .simplify_full_i(expand, t, recursion_limit, total_limit)
587                .map(|t| Argument::Sequence(MaybeSequence::One(t))),
588            Argument::Sequence(MaybeSequence::Seq(ts)) => {
589                let mut changed = false;
590                let nts = ts
591                    .iter()
592                    .map(|t| {
593                        self.simplify_full_i(expand, t, recursion_limit, total_limit)
594                            .map_or(Cow::Borrowed(t), |a| {
595                                changed = true;
596                                Cow::Owned(a)
597                            })
598                    })
599                    .collect::<Vec<_>>();
600                if changed {
601                    Some(Argument::Sequence(MaybeSequence::Seq(
602                        nts.into_iter().map(Cow::into_owned).collect(),
603                    )))
604                } else {
605                    None
606                }
607            }
608        }
609    }
610    fn bound_arg_full(
611        &mut self,
612        expand: bool,
613        arg: &'t BoundArgument,
614        recusion_limit: &mut usize,
615        total_limit: &mut usize,
616    ) -> Option<BoundArgument> {
617        match arg {
618            BoundArgument::Simple(t) => self
619                .simplify_full_i(expand, t, recusion_limit, total_limit)
620                .map(BoundArgument::Simple),
621            BoundArgument::Bound(cv) => self
622                .cv_full(expand, cv, recusion_limit, total_limit)
623                .map(BoundArgument::Bound),
624            BoundArgument::Sequence(MaybeSequence::One(t)) => self
625                .simplify_full_i(expand, t, recusion_limit, total_limit)
626                .map(|t| BoundArgument::Sequence(MaybeSequence::One(t))),
627            BoundArgument::BoundSeq(MaybeSequence::One(cv)) => self
628                .cv_full(expand, cv, recusion_limit, total_limit)
629                .map(|t| BoundArgument::BoundSeq(MaybeSequence::One(t))),
630            BoundArgument::Sequence(MaybeSequence::Seq(ts)) => {
631                let mut changed = false;
632                let nts = ts
633                    .iter()
634                    .map(|t| {
635                        self.simplify_full_i(expand, t, recusion_limit, total_limit)
636                            .map_or(Cow::Borrowed(t), |a| {
637                                changed = true;
638                                Cow::Owned(a)
639                            })
640                    })
641                    .collect::<Vec<_>>();
642                if changed {
643                    Some(BoundArgument::Sequence(MaybeSequence::Seq(
644                        nts.into_iter().map(Cow::into_owned).collect(),
645                    )))
646                } else {
647                    None
648                }
649            }
650            BoundArgument::BoundSeq(MaybeSequence::Seq(cvs)) => {
651                let mut changed = false;
652                let ncvs = cvs
653                    .iter()
654                    .map(|t| {
655                        self.cv_full(expand, t, recusion_limit, total_limit).map_or(
656                            Cow::Borrowed(t),
657                            |a| {
658                                changed = true;
659                                Cow::Owned(a)
660                            },
661                        )
662                    })
663                    .collect::<Vec<_>>();
664                if changed {
665                    Some(BoundArgument::BoundSeq(MaybeSequence::Seq(
666                        ncvs.into_iter().map(Cow::into_owned).collect(),
667                    )))
668                } else {
669                    None
670                }
671            }
672        }
673    }
674
675    fn cv_full(
676        &mut self,
677        expand: bool,
678        arg: &'t ComponentVar,
679        recursion_limit: &mut usize,
680        total_limit: &mut usize,
681    ) -> Option<ComponentVar> {
682        match (arg.tp.as_ref(), arg.df.as_ref()) {
683            (None, None) => None,
684            (Some(tp), None) => self
685                .simplify_full_i(expand, tp, recursion_limit, total_limit)
686                .map(|tp| ComponentVar {
687                    var: arg.var.clone(),
688                    tp: Some(tp),
689                    df: None,
690                }),
691            (None, Some(df)) => self
692                .simplify_full_i(expand, df, recursion_limit, total_limit)
693                .map(|df| ComponentVar {
694                    var: arg.var.clone(),
695                    tp: None,
696                    df: Some(df),
697                }),
698            (Some(tp), Some(df)) => {
699                let ntp = self.simplify_full_i(expand, tp, recursion_limit, total_limit);
700                let ndf = self.simplify_full_i(expand, df, recursion_limit, total_limit);
701                if ntp.is_none() && ndf.is_none() {
702                    return None;
703                }
704                Some(ComponentVar {
705                    var: arg.var.clone(),
706                    tp: Some(ntp.unwrap_or_else(|| tp.clone())),
707                    df: Some(ndf.unwrap_or_else(|| df.clone())),
708                })
709            }
710        }
711    }
712}
ftml_solver/impls/simplify.rs

ftml_solver/impls/
simplify.rs
