ftml_solver/rules/operators/
pi.rs

1use crate::{
2    CheckRef,
3    impls::solving::TermExtSolvable,
4    rules::{
5        CheckingRule, InferenceRule, InhabitableRule, MarkerRule, PreparationRule,
6        SimplificationRule, SizedSolverRule, SubtypeRule, UniverseRule,
7        operators::numbers::{NumberRule, NumberType},
8    },
9    split::SplitStrategy,
10};
11use ftml_ontology::terms::{
12    ApplicationTerm, Argument, BindingTerm, BoundArgument, ComponentVar, MaybeSequence, Term,
13    Variable, sequences::SequenceType,
14};
15use ftml_solver_trace::traceref;
16use ftml_uris::SymbolUri;
17use smallvec::SmallVec;
18use std::{borrow::Cow, hint::unreachable_unchecked};
19
20#[allow(unpredictable_function_pointer_comparisons)]
21#[derive(Debug, Clone, PartialEq, Eq)]
22pub struct PiExtensionRule<Split: SplitStrategy> {
23    pub extension: SymbolUri,
24    pub pi: SymbolUri,
25    pub applicable: fn(&Self, &Term, &Argument) -> bool,
26    pub infer: for<'t> fn(
27        &Self,
28        &super::pi::PiInferenceRule,
29        &mut CheckRef<'t, '_, Split>,
30        &Term,
31        &'t [Argument],
32        &mut usize,
33    ) -> Option<Term>,
34}
35impl<Split: SplitStrategy> SizedSolverRule for PiExtensionRule<Split> {
36    fn display(&self) -> Vec<crate::trace::Displayable> {
37        ftml_solver_trace::trace!(&self.extension, "is extension of", &self.pi)
38    }
39}
40impl<Split: SplitStrategy> MarkerRule<Split> for PiExtensionRule<Split> {}
41
42macro_rules! ret_i {
43    ($(;)?) => {};
44    (& $e:expr; $($tk:tt)*) => {
45        if !$e {
46            return None;
47        }
48        ret_i!($($tk)*)
49    };
50    ($p:pat = $e:expr; $($tk:tt)*) => {
51        let $p = $e else {
52            return None;
53        };
54        ret_i!($($tk)*)
55    };
56
57}
58macro_rules! ret {
59    ( $($tk:tt)* ) => {
60        ret_i!($($tk)*;)
61    };
62}
63
64pub(crate) fn destruct_binder<'t>(
65    t: &'t Term,
66    head: &SymbolUri,
67) -> Option<(either::Either<&'t ComponentVar, &'t ComponentVar>, &'t Term)> {
68    ret!(
69        Term::Bound(b) = t;
70        & b.arguments.len() == 2;
71        & matches!(&b.head,Term::Symbol { uri, .. } if *uri == *head);
72        //Some(BoundArgument::Bound(v)) = b.arguments.first();
73        Some(BoundArgument::Simple(body)) = b.arguments.get(1);
74    );
75    let v = if let Some(BoundArgument::Bound(v)) = b.arguments.first() {
76        either::Left(v)
77    } else if let Some(BoundArgument::BoundSeq(MaybeSequence::One(s))) = b.arguments.first() {
78        either::Right(s)
79    } else {
80        return None;
81    };
82    Some((v, body))
83}
84fn construct_binder(var: ComponentVar, body: Term, head: &SymbolUri) -> Term {
85    Term::Bound(BindingTerm::new(
86        Term::Symbol {
87            uri: head.clone(),
88            presentation: None,
89        },
90        Box::new([BoundArgument::Bound(var), BoundArgument::Simple(body)]),
91        None,
92    ))
93}
94
95#[derive(Debug, Clone, PartialEq, Eq)]
96pub struct ArrowRule {
97    pub arrow: SymbolUri,
98    pub pi: SymbolUri,
99}
100impl SizedSolverRule for ArrowRule {
101    fn display(&self) -> Vec<crate::trace::Displayable> {
102        ftml_solver_trace::trace!(&self.arrow, " is simple version of ", &self.pi)
103    }
104    fn priority(&self) -> isize {
105        100_000_000 // SimpleTypeOperatorRule::priority() * 100
106    }
107}
108impl ArrowRule {
109    fn go<Split: SplitStrategy>(
110        &self,
111        t: &Term,
112        mut path: Option<(&mut smallvec::SmallVec<u8, 16>, usize)>,
113    ) -> Option<Term> {
114        let Term::Application(app) = t else {
115            return None;
116        };
117        let Some(Argument::Simple(ret)) = app.arguments.last() else {
118            return None;
119        };
120        let args = &app.arguments[..app.arguments.len() - 1];
121        if args.is_empty() {
122            return Some(ret.clone());
123        }
124        let mut count = 0u16;
125        let args = args.iter().map(|a| match a {
126            Argument::Simple(t) => {
127                if let Some((v, i)) = path.as_mut()
128                    && v.get(*i).copied() == Some(count as u8)
129                {
130                    v.insert(*i + 1, 0);
131                }
132                let (v, idx) = ret.fresh_variable(&crate::DUMMY, Some(count));
133                if let Some(idx) = idx {
134                    count = idx + 1;
135                } else {
136                    count += 1;
137                }
138                BoundArgument::Bound(ComponentVar {
139                    var: v,
140                    tp: Some(t.clone()),
141                    df: None,
142                })
143            }
144            Argument::Sequence(MaybeSequence::One(t)) => {
145                if let Some((v, i)) = path.as_mut()
146                    && v.get(*i).copied() == Some(count as u8)
147                {
148                    v.insert(*i + 1, 0);
149                }
150                let (v, idx) = ret.fresh_variable(&crate::DUMMY, Some(count));
151                if let Some(idx) = idx {
152                    count = idx + 1;
153                } else {
154                    count += 1;
155                }
156                BoundArgument::BoundSeq(MaybeSequence::One(ComponentVar {
157                    var: v,
158                    tp: Some(t.clone()),
159                    df: None,
160                }))
161            }
162            Argument::Sequence(MaybeSequence::Seq(ts)) => {
163                if let Some((v, i)) = path.as_mut()
164                    && v.get(*i).copied() == Some(count as u8)
165                {
166                    v.insert(*i + 2, 0);
167                }
168                BoundArgument::BoundSeq(MaybeSequence::Seq(
169                    ts.iter()
170                        .map(|t| {
171                            let (v, idx) = ret.fresh_variable(&crate::DUMMY, Some(count));
172                            if let Some(idx) = idx {
173                                count = idx + 1;
174                            } else {
175                                count += 1;
176                            }
177                            ComponentVar {
178                                var: v,
179                                tp: Some(t.clone()),
180                                df: None,
181                            }
182                        })
183                        .collect(),
184                ))
185            }
186        });
187        let ret = Term::Bound(BindingTerm::new(
188            Term::Symbol {
189                uri: self.pi.clone(),
190                presentation: None,
191            },
192            args.chain([BoundArgument::Simple(ret.clone())]).collect(),
193            None,
194        ));
195        Some(ret)
196    }
197}
198impl<Split: SplitStrategy> SimplificationRule<Split> for ArrowRule {
199    fn applicable(&self, term: &Term) -> bool {
200        if let Term::Application(app) = term {
201            matches!(&app.head,Term::Symbol{uri,..} if *uri == self.arrow)
202        } else {
203            false
204        }
205    }
206    fn apply<'t>(
207        &self,
208        _: CheckRef<'t, '_, Split>,
209        t: &'t Term,
210    ) -> Result<Term, Option<ftml_ontology::terms::termpaths::TermPath>> {
211        self.go::<Split>(t, None).ok_or(None)
212    }
213}
214impl<Split: SplitStrategy> PreparationRule<Split> for ArrowRule {
215    fn applicable(&self, _: &CheckRef<'_, '_, Split>, t: &Term) -> bool {
216        <Self as SimplificationRule<Split>>::applicable(self, t)
217    }
218    fn applicable_revert(&self, _: &CheckRef<'_, '_, Split>, t: &Term) -> bool {
219        if let Term::Bound(bind) = t {
220            matches!(&bind.head,Term::Symbol { uri, .. } if *uri == self.pi)
221        } else {
222            false
223        }
224    }
225
226    #[allow(clippy::cast_possible_truncation)]
227    fn apply(
228        &self,
229        _: &mut CheckRef<'_, '_, Split>,
230        t: Term,
231        path: Option<(&mut smallvec::SmallVec<u8, 16>, usize)>,
232    ) -> std::ops::ControlFlow<Term, Term> {
233        std::ops::ControlFlow::Continue(self.go::<Split>(&t, path).unwrap_or(t))
234    }
235
236    fn revert(&self, _: &CheckRef<'_, '_, Split>, t: Term) -> std::ops::ControlFlow<Term, Term> {
237        let Term::Bound(app) = t else {
238            return std::ops::ControlFlow::Continue(t);
239        };
240        let Some(BoundArgument::Simple(ret)) = app.arguments.last() else {
241            return std::ops::ControlFlow::Continue(Term::Bound(app));
242        };
243        let args = &app.arguments[..app.arguments.len() - 1];
244        let mut free_vars = args.iter().map(|a| a.free_variables()).collect::<Vec<_>>();
245        free_vars.push(ret.free_variables());
246
247        let args: Result<Vec<Argument>, ()> = args
248            .iter()
249            .enumerate()
250            .map(|(i, a)| match a {
251                BoundArgument::Bound(ComponentVar {
252                    var,
253                    tp: Some(tp),
254                    df: None,
255                }) if !free_vars[i + 1..]
256                    .iter()
257                    .flatten()
258                    .any(|v| v.name() == var.name()) =>
259                {
260                    Ok(Argument::Simple(tp.clone()))
261                }
262                BoundArgument::BoundSeq(MaybeSequence::One(ComponentVar {
263                    var,
264                    tp: Some(tp),
265                    df: None,
266                })) if !free_vars[i + 1..]
267                    .iter()
268                    .flatten()
269                    .any(|v| v.name() == var.name()) =>
270                {
271                    Ok(Argument::Sequence(MaybeSequence::One(tp.clone())))
272                }
273                BoundArgument::BoundSeq(MaybeSequence::Seq(vs)) => {
274                    let seq: Result<Box<[Term]>, ()> = vs
275                        .iter()
276                        .map(|v| {
277                            if let ComponentVar {
278                                var,
279                                tp: Some(tp),
280                                df: None,
281                            } = v
282                                && !free_vars[i + 1..]
283                                    .iter()
284                                    .flatten()
285                                    .any(|v| v.name() == var.name())
286                            {
287                                Ok(tp.clone())
288                            } else {
289                                Err(())
290                            }
291                        })
292                        .collect();
293                    Ok(Argument::Sequence(MaybeSequence::Seq(seq?)))
294                }
295                _ => Err(()),
296            })
297            .collect();
298        drop(free_vars);
299        std::ops::ControlFlow::Continue(match args {
300            Err(()) => Term::Bound(app),
301            Ok(mut args) => {
302                args.push(Argument::Simple(ret.clone()));
303                Term::Application(ApplicationTerm::new(
304                    Term::Symbol {
305                        uri: self.arrow.clone(),
306                        presentation: None,
307                    },
308                    args.into_boxed_slice(),
309                    None,
310                ))
311            }
312        })
313    }
314}
315
316#[derive(Debug, Clone, PartialEq, Eq)]
317pub struct NeedsTypeRule(pub SymbolUri);
318impl SizedSolverRule for NeedsTypeRule {
319    fn display(&self) -> Vec<ftml_solver_trace::Displayable> {
320        ftml_solver_trace::trace!(&self.0, "needs typed variables")
321    }
322}
323impl<Split: SplitStrategy> PreparationRule<Split> for NeedsTypeRule {
324    fn applicable(&self, _: &CheckRef<'_, '_, Split>, t: &Term) -> bool {
325        if let Term::Bound(b) = t
326            && let Term::Symbol { uri, .. } = &b.head
327            && *uri == self.0
328        {
329            b.arguments.iter().any(|a| matches!(a,BoundArgument::Bound(ComponentVar { tp:None, .. })|BoundArgument::BoundSeq(MaybeSequence::One(ComponentVar { tp:None, .. })))
330                || matches!(a,BoundArgument::BoundSeq(MaybeSequence::Seq(seq)) if seq.iter().any(|a| matches!(a,ComponentVar { tp:None, .. }))))
331        } else {
332            false
333        }
334    }
335    fn applicable_revert(&self, _: &CheckRef<'_, '_, Split>, _: &Term) -> bool {
336        false
337    }
338    fn apply(
339        &self,
340        checker: &mut CheckRef<'_, '_, Split>,
341        t: Term,
342        path: Option<(&mut smallvec::SmallVec<u8, 16>, usize)>,
343    ) -> std::ops::ControlFlow<Term, Term> {
344        let Term::Bound(b) = t else {
345            return std::ops::ControlFlow::Continue(t);
346        };
347        let arguments = &b.arguments;
348        let ret = checker.scoped(|checker| {
349            let mut changed = false;
350            let nargs = arguments
351                .iter()
352                .map(|a| match a {
353                    BoundArgument::Bound(ComponentVar { var, tp: None, df }) => {
354                        if checker.infer_var_type(var).is_none() {
355                            changed = true;
356                            let v = checker.new_solvable();
357                            Cow::Owned(BoundArgument::Bound(ComponentVar {
358                                var: var.clone(),
359                                tp: Some(v),
360                                df: df.clone(),
361                            }))
362                        } else {
363                            Cow::Borrowed(a)
364                        }
365                    }
366                    BoundArgument::BoundSeq(MaybeSequence::One(ComponentVar {
367                        var,
368                        tp: None,
369                        df,
370                    })) => {
371                        if checker.infer_var_type(var).is_none() {
372                            changed = true;
373                            let v = checker.new_solvable();
374                            Cow::Owned(BoundArgument::BoundSeq(MaybeSequence::One(ComponentVar {
375                                var: var.clone(),
376                                tp: Some(v),
377                                df: df.clone(),
378                            })))
379                        } else {
380                            Cow::Borrowed(a)
381                        }
382                    }
383                    BoundArgument::BoundSeq(MaybeSequence::Seq(vs)) => {
384                        let nvs = vs
385                            .iter()
386                            .map(|cv @ ComponentVar { var, tp, df }| {
387                                if tp.is_none() && checker.infer_var_type(var).is_none() {
388                                    changed = true;
389                                    let v = checker.new_solvable();
390                                    Cow::Owned(ComponentVar {
391                                        var: var.clone(),
392                                        tp: Some(v),
393                                        df: df.clone(),
394                                    })
395                                } else {
396                                    Cow::Borrowed(cv)
397                                }
398                            })
399                            .collect::<Vec<_>>();
400                        if changed {
401                            Cow::Owned(BoundArgument::BoundSeq(MaybeSequence::Seq(
402                                nvs.into_iter().map(Cow::into_owned).collect(),
403                            )))
404                        } else {
405                            Cow::Borrowed(a)
406                        }
407                    }
408                    _ => Cow::Borrowed(a),
409                })
410                .collect::<Vec<_>>();
411            if changed {
412                Some(Term::Bound(BindingTerm::new(
413                    b.head.clone(),
414                    nargs.into_iter().map(Cow::into_owned).collect(),
415                    b.presentation.clone(),
416                )))
417            } else {
418                None
419            }
420        });
421        std::ops::ControlFlow::Continue(ret.unwrap_or(Term::Bound(b)))
422    }
423
424    fn revert(&self, _: &CheckRef<'_, '_, Split>, t: Term) -> std::ops::ControlFlow<Term, Term> {
425        std::ops::ControlFlow::Continue(t)
426    }
427}
428
429#[derive(Debug, Clone, PartialEq, Eq)]
430pub struct PiVarianceRule(pub SymbolUri);
431
432impl SizedSolverRule for PiVarianceRule {
433    fn display(&self) -> Vec<crate::trace::Displayable> {
434        ftml_solver_trace::trace!(
435            &self.0,
436            " is contravariant in arguments and covariant in its return type"
437        )
438    }
439}
440impl<Split: SplitStrategy> SubtypeRule<Split> for PiVarianceRule {
441    fn applicable(&self, _: &CheckRef<'_, '_, Split>, sub: &Term, sup: &Term) -> bool {
442        if let Term::Bound(b) = sub
443            && let Term::Bound(b2) = sup
444            && let Term::Symbol { uri, .. } = &b.head
445            && let Term::Symbol { uri: uri2, .. } = &b2.head
446        {
447            *uri == self.0 && *uri2 == self.0 && b.arguments.len() == b2.arguments.len()
448        } else {
449            false
450        }
451    }
452    fn apply<'t>(
453        &self,
454        mut checker: CheckRef<'t, '_, Split>,
455        sub: &'t Term,
456        sup: &'t Term,
457    ) -> Option<bool> {
458        let Term::Bound(sub) = sub else { return None };
459        let Term::Bound(sup) = sup else { return None };
460        let Some(BoundArgument::Simple(subret)) = sub.arguments.last() else {
461            return None;
462        };
463        let Some(BoundArgument::Simple(supret)) = sup.arguments.last() else {
464            return None;
465        };
466        let mut currsub = Vec::<(&str, Term)>::new();
467        for (sub, sup) in sub.arguments[..sub.arguments.len() - 1]
468            .iter()
469            .zip(sup.arguments[..sup.arguments.len() - 1].iter())
470        {
471            match (sub, sup) {
472                (
473                    BoundArgument::Bound(ComponentVar {
474                        var: varsub,
475                        tp: Some(sub),
476                        ..
477                    }),
478                    BoundArgument::Bound(ComponentVar {
479                        var: varsup,
480                        tp: Some(sup),
481                        ..
482                    }),
483                ) => {
484                    let sup = sup / &*currsub;
485                    if !checker.scoped(|checker| checker.check_subtype(&sup, sub))? {
486                        return None;
487                    }
488                    currsub.push((varsup.name(), varsub.clone().into()));
489                    checker.extend_context(ComponentVar {
490                        var: varsub.clone(),
491                        tp: Some(sub.clone()),
492                        df: None,
493                    });
494                }
495                (
496                    BoundArgument::BoundSeq(MaybeSequence::One(ComponentVar {
497                        var: varsub,
498                        tp: Some(sub),
499                        ..
500                    })),
501                    BoundArgument::BoundSeq(MaybeSequence::One(ComponentVar {
502                        var: varsup,
503                        tp: Some(sup),
504                        ..
505                    }))
506                    | BoundArgument::Bound(ComponentVar {
507                        var: varsup,
508                        tp: Some(sup),
509                        ..
510                    }),
511                ) => {
512                    let sup = sup / &*currsub;
513                    if !checker.scoped(|checker| checker.check_subtype(&sup, sub))? {
514                        return None;
515                    }
516                    currsub.push((varsup.name(), varsub.clone().into()));
517                    checker.extend_context(ComponentVar {
518                        var: varsub.clone(),
519                        tp: Some(sub.clone()),
520                        df: None,
521                    });
522                }
523                _ => {
524                    checker.failure("argument not bound single variable or variable sequence");
525                    //checker.failure(format!("{sub:?}  vs  {sup:?}"));
526                    return None;
527                }
528            }
529        }
530        let supret = supret / &*currsub;
531        checker.scoped(|checker| checker.check_subtype(subret, &supret))
532    }
533}
534
535#[derive(Debug, Clone, PartialEq, Eq)]
536pub struct LambdaPiInferenceRule {
537    pub lambda: SymbolUri,
538    pub pi: SymbolUri,
539}
540impl SizedSolverRule for LambdaPiInferenceRule {
541    fn display(&self) -> Vec<crate::trace::Displayable> {
542        ftml_solver_trace::trace!(
543            "{ x:A, B(x):T } ⊢ (",
544            &self.lambda,
545            " x:A. B) :=> ",
546            &self.pi,
547            " x:A. T"
548        )
549    }
550}
551impl LambdaPiInferenceRule {
552    fn infer_simple<'t, Split: SplitStrategy>(
553        &self,
554        mut checker: CheckRef<'t, '_, Split>,
555        var: &'t ComponentVar,
556        body: &'t Term,
557    ) -> Option<Term> {
558        let btp = match &var.tp {
559            None => {
560                if checker.infer_var_type(&var.var).is_some() {
561                    checker.scoped(|checker| {
562                        checker.extend_context(var);
563                        checker.infer_type(body)
564                    })?
565                } else {
566                    let nvar = ComponentVar {
567                        var: var.var.clone(),
568                        tp: Some(checker.new_solvable()),
569                        df: var.df.clone(),
570                    };
571                    checker.scoped(|checker| {
572                        checker.extend_context(nvar);
573                        checker.infer_type(body)
574                    })?
575                }
576            }
577            Some(tp) if tp.is_solvable().is_some() => {
578                let inf = checker.scoped(|checker| {
579                    checker.extend_context(var);
580                    checker.infer_type(body)
581                })?;
582                ret!(&checker.check_inhabitable(tp) == Some(true));
583                inf
584            }
585            Some(tp) => {
586                ret!(&checker.check_inhabitable(tp) == Some(true));
587                checker.scoped(|checker| {
588                    checker.extend_context(var);
589                    checker.infer_type(body)
590                })?
591            }
592        };
593        Some(construct_binder(var.clone(), btp, &self.pi))
594    }
595
596    fn infer_sequence<'t, Split: SplitStrategy>(
597        &self,
598        mut checker: CheckRef<'t, '_, Split>,
599        var: &'t ComponentVar,
600        body: &'t Term,
601    ) -> Option<Term> {
602        let btp = match &var.tp {
603            None => {
604                if let Some(tp) = checker.infer_var_type(&var.var) {
605                    checker.scoped(|checker| {
606                        checker.extend_context(var);
607                        checker.infer_type(body)
608                    })?
609                } else {
610                    let nvar = ComponentVar {
611                        var: var.var.clone(),
612                        tp: Some(checker.new_solvable()),
613                        df: var.df.clone(),
614                    };
615                    checker.scoped(|checker| {
616                        checker.extend_context(nvar);
617                        checker.infer_type(body)
618                    })?
619                }
620            }
621            Some(tp) if tp.is_solvable().is_some() => {
622                let inf = checker.scoped(|checker| {
623                    checker.extend_context(var);
624                    checker.infer_type(body)
625                })?;
626                ret!(&checker.check_inhabitable(tp) == Some(true));
627                inf
628            }
629            Some(tp) => {
630                ret!(&checker.check_inhabitable(tp) == Some(true));
631                checker.scoped(|checker| {
632                    checker.extend_context(var);
633                    checker.infer_type(body)
634                })?
635            }
636        };
637        let r = Term::Bound(BindingTerm::new(
638            Term::Symbol {
639                uri: self.pi.clone(),
640                presentation: None,
641            },
642            Box::new([
643                BoundArgument::BoundSeq(MaybeSequence::One(var.clone())),
644                BoundArgument::Simple(btp),
645            ]),
646            None,
647        ));
648        Some(r)
649    }
650}
651impl<Split: SplitStrategy> InferenceRule<Split> for LambdaPiInferenceRule {
652    fn applicable(&self, term: &Term) -> bool {
653        destruct_binder(term, &self.lambda).is_some()
654    }
655    fn infer<'t>(&self, checker: CheckRef<'t, '_, Split>, term: &'t Term) -> Option<Term> {
656        let (var, body) = destruct_binder(term, &self.lambda)?;
657        match var {
658            either::Left(var) => self.infer_simple(checker, var, body),
659            either::Right(var) => self.infer_sequence(checker, var, body),
660        }
661    }
662}
663
664#[derive(Debug, Clone, PartialEq, Eq)]
665pub struct LambdaPiCheckingRule {
666    pub lambda: SymbolUri,
667    pub pi: SymbolUri,
668}
669impl SizedSolverRule for LambdaPiCheckingRule {
670    fn display(&self) -> Vec<crate::trace::Displayable> {
671        ftml_solver_trace::trace!(
672            "{ x:A, B(x):T } ⊢ (",
673            &self.lambda,
674            " x:A. B) : ",
675            &self.pi,
676            " y:A. T"
677        )
678    }
679}
680impl<Split: SplitStrategy> CheckingRule<Split> for LambdaPiCheckingRule {
681    fn applicable(&self, _: &CheckRef<'_, '_, Split>, term: &Term, tp: &Term) -> bool {
682        destruct_binder(term, &self.lambda).is_some_and(|(v, _)| v.is_left())
683            && destruct_binder(tp, &self.pi).is_some_and(|(v, _)| v.is_left())
684    }
685    fn apply<'t>(
686        &self,
687        mut checker: CheckRef<'t, '_, Split>,
688        term: &'t Term,
689        tp: &'t Term,
690    ) -> Option<bool> {
691        let (var, lambda_body) = destruct_binder(term, &self.lambda)?;
692        let var = var.expect_left("applicable");
693        let (pivar, pi_body) = destruct_binder(tp, &self.pi)?;
694        let pivar = pivar.expect_left("applicable");
695        let pi_tp = match &pivar.tp {
696            None => Cow::Owned(checker.infer_var_type(&var.var)?),
697            Some(tp) => {
698                //ret!(&checker.check_inhabitable(trace, context.branch(), tp) == Some(true));
699                Cow::Borrowed(tp)
700            }
701        };
702        let lam_tp = match &var.tp {
703            None => Cow::Owned(checker.infer_var_type(&var.var)?),
704            Some(tp) => {
705                //ret!(&checker.check_inhabitable(trace, context.branch(), tp) == Some(true));
706                Cow::Borrowed(tp)
707            }
708        };
709        ret!(&checker.scoped(|checker| { checker.check_subtype(&pi_tp, &lam_tp) }) == Some(true));
710        let ntp = pi_body
711            / (
712                pivar.var.name(),
713                &Term::Var {
714                    variable: var.var.clone(),
715                    presentation: None,
716                },
717            );
718        checker.scoped(|checker| {
719            checker.extend_context(var);
720            checker.check_type(lambda_body, &ntp)
721        })
722    }
723}
724
725#[derive(Debug, Clone, PartialEq, Eq)]
726pub struct PiInhabitableRule(pub SymbolUri);
727impl SizedSolverRule for PiInhabitableRule {
728    fn display(&self) -> Vec<crate::trace::Displayable> {
729        ftml_solver_trace::trace!("{ INH A, x:A, INH B(x) } ⊢ INH ", &self.0, " x:A. B")
730    }
731}
732
733impl<Split: SplitStrategy> InhabitableRule<Split> for PiInhabitableRule {
734    fn applicable(&self, term: &Term) -> bool {
735        matches!(term,Term::Bound(b) if matches!(&b.head,Term::Symbol { uri, .. } if *uri == self.0))
736    }
737    fn apply<'t>(&self, mut checker: CheckRef<'t, '_, Split>, term: &'t Term) -> Option<bool> {
738        let Term::Bound(b) = term else { return None };
739        let Some(BoundArgument::Simple(body)) = b.arguments.last() else {
740            return None;
741        };
742        let previous = &b.arguments[..&b.arguments.len() - 1];
743        let mut deferred = Vec::new();
744        //checker.add_msg(traceref!("Here:", body.clone()).into());
745        for arg in previous {
746            match arg {
747                BoundArgument::Simple(t) | BoundArgument::Sequence(MaybeSequence::One(t)) => {
748                    let _ = checker.infer_type(t)?;
749                }
750                BoundArgument::Sequence(MaybeSequence::Seq(ts)) => {
751                    for t in ts {
752                        let _ = checker.infer_type(t)?;
753                    }
754                }
755                BoundArgument::Bound(cv @ ComponentVar { var, tp, .. })
756                | BoundArgument::BoundSeq(MaybeSequence::One(cv @ ComponentVar { var, tp, .. })) => {
757                    if let Some(tp) = tp {
758                        if tp.has_solvable() {
759                            deferred.push(tp);
760                        } else if !checker.check_inhabitable(tp)? {
761                            return Some(false);
762                        }
763                    } else {
764                        let _ = checker.infer_var_type(var)?;
765                    }
766                    checker.extend_context(cv);
767                }
768                BoundArgument::BoundSeq(MaybeSequence::Seq(vars)) => {
769                    for cv @ ComponentVar { var, tp, .. } in vars {
770                        if let Some(tp) = tp {
771                            if tp.has_solvable() {
772                                deferred.push(tp);
773                            } else if !checker.check_inhabitable(tp)? {
774                                return Some(false);
775                            }
776                        } else {
777                            let _ = checker.infer_var_type(var)?;
778                        }
779                        checker.extend_context(cv);
780                    }
781                }
782            }
783        }
784        if !checker.check_inhabitable(body)? {
785            return None;
786        }
787        for d in deferred {
788            if !checker.check_inhabitable(d)? {
789                return None;
790            }
791        }
792        Some(true)
793    }
794}
795
796#[derive(Debug, Clone, PartialEq, Eq)]
797pub struct PiUniverseRule(pub SymbolUri);
798impl SizedSolverRule for PiUniverseRule {
799    fn display(&self) -> Vec<crate::trace::Displayable> {
800        ftml_solver_trace::trace!("{ INH A, x:A, UNIV B(x) } ⊢ UNIV ", &self.0, " x:A. B")
801    }
802}
803
804impl<Split: SplitStrategy> UniverseRule<Split> for PiUniverseRule {
805    fn applicable(&self, term: &Term) -> bool {
806        matches!(term,Term::Bound(b) if matches!(&b.head,Term::Symbol { uri, .. } if *uri == self.0))
807    }
808    fn apply<'t>(&self, mut checker: CheckRef<'t, '_, Split>, term: &'t Term) -> Option<bool> {
809        let Term::Bound(b) = term else { return None };
810        let Some(BoundArgument::Simple(body)) = b.arguments.last() else {
811            return None;
812        };
813        let previous = &b.arguments[..&b.arguments.len() - 1];
814        let mut deferred = Vec::new();
815        //checker.add_msg(traceref!("Here:", body.clone()).into());
816        for arg in previous {
817            match arg {
818                BoundArgument::Simple(t) | BoundArgument::Sequence(MaybeSequence::One(t)) => {
819                    let _ = checker.infer_type(t)?;
820                }
821                BoundArgument::Sequence(MaybeSequence::Seq(ts)) => {
822                    for t in ts {
823                        let _ = checker.infer_type(t)?;
824                    }
825                }
826                BoundArgument::Bound(cv @ ComponentVar { var, tp, .. })
827                | BoundArgument::BoundSeq(MaybeSequence::One(cv @ ComponentVar { var, tp, .. })) => {
828                    if let Some(tp) = tp {
829                        if tp.has_solvable() {
830                            deferred.push(tp);
831                        } else if !checker.check_inhabitable(tp)? {
832                            return Some(false);
833                        }
834                    } else {
835                        let _ = checker.infer_var_type(var)?;
836                    }
837                    checker.extend_context(cv);
838                }
839                BoundArgument::BoundSeq(MaybeSequence::Seq(vars)) => {
840                    for cv @ ComponentVar { var, tp, .. } in vars {
841                        if let Some(tp) = tp {
842                            if tp.has_solvable() {
843                                deferred.push(tp);
844                            } else if !checker.check_inhabitable(tp)? {
845                                return Some(false);
846                            }
847                        } else {
848                            let _ = checker.infer_var_type(var)?;
849                        }
850                        checker.extend_context(cv);
851                    }
852                }
853            }
854        }
855        if !checker.check_universe(body)? {
856            return None;
857        }
858        for d in deferred {
859            if !checker.check_inhabitable(d)? {
860                return None;
861            }
862        }
863        Some(true)
864    }
865}
866
867#[derive(Debug, Clone, PartialEq, Eq)]
868pub struct PiInferenceRule(pub SymbolUri);
869impl SizedSolverRule for PiInferenceRule {
870    fn display(&self) -> Vec<crate::trace::Displayable> {
871        ftml_solver_trace::trace!("{ f: ", &self.0, " x:A.B(x), t:A } ⊢ f(t) :=> B(t)")
872    }
873}
874
875impl<Split: SplitStrategy> InferenceRule<Split> for PiInferenceRule {
876    fn applicable(&self, term: &Term) -> bool {
877        matches!(term, Term::Application(_)) // | Term::Bound(_))
878    }
879    fn infer<'t>(&self, mut checker: CheckRef<'t, '_, Split>, term: &'t Term) -> Option<Term> {
880        if let Term::Application(app) = term {
881            if app.arguments.is_empty() {
882                return None;
883            }
884            let tp = checker.infer_type(&app.head)?;
885            if let Some(SequenceType::SeqType(tp, _)) = tp.as_sequence_type()
886                && let [Argument::Simple(idx)] = &*app.arguments
887            {
888                checker.comment("is sequence type");
889                let nat = checker.rules().marker().iter().rev().find_map(|rl| {
890                    rl.as_any().downcast_ref::<NumberRule>().and_then(|rl| {
891                        if rl.typ == NumberType::Naturals {
892                            Some(rl.sym.clone())
893                        } else {
894                            None
895                        }
896                    })
897                })?;
898                let ntp: Term = nat.into();
899                if checker.scoped(|checker| checker.check_type(idx, &ntp)) != Some(true) {
900                    return None;
901                }
902                Some(tp.clone())
903            } else {
904                self.type_apply(&mut checker, tp, &app.arguments)
905            }
906        } else {
907            checker.failure("Not an application");
908            None
909        }
910    }
911}
912
913impl PiInferenceRule {
914    // INVARIANT: return has 2 arguments, the second one being simple
915    pub fn deconstruct_tp<Split: SplitStrategy>(
916        bind_uri: &SymbolUri,
917        checker: &mut CheckRef<'_, '_, Split>,
918        tp: Term,
919    ) -> Result<BindingTerm, Term> {
920        let Some(nret) = checker.scoped(|checker| {
921            match checker.simplify_until(&tp, |_, t| {
922                if let Term::Bound(b) = t
923                    && let Term::Symbol { uri, .. } = &b.head
924                {
925                    *uri == *bind_uri
926                        && b.arguments.len() == 2
927                        && matches!(b.arguments.get(1), Some(BoundArgument::Simple(_)))
928                } else {
929                    false
930                }
931            })? {
932                Cow::Borrowed(_) => Some(None),
933                Cow::Owned(tp) => Some(Some(tp)),
934            }
935        }) else {
936            checker.add_msg(traceref!(FAIL "type is not a binder: ",tp.clone()).into());
937            return Err(tp);
938        };
939        let Term::Bound(b) = nret.unwrap_or(tp) else {
940            // SAFETY: simplify_until above would have returned None otherwise
941            unsafe { unreachable_unchecked() }
942        };
943        if !matches!(&b.head,Term::Symbol { uri, .. } if *uri == *bind_uri)
944            || b.arguments.len() != 2
945            || !matches!(b.arguments.get(1), Some(BoundArgument::Simple(_)))
946        {
947            checker.failure("Type is not a Π anymore");
948            return Err(Term::Bound(b));
949        }
950        Ok(b)
951    }
952
953    // INVARIANT: tp.is_concrete_sequence()
954    pub(super) fn flatten_sequence<Split: SplitStrategy>(
955        checker: &mut CheckRef<'_, '_, Split>,
956        tp: &Term,
957        b: &BindingTerm,
958        body: Term,
959    ) -> Term {
960        let Some(new_args) = tp.as_sequence().and_then(|s| s.to_concrete()) else {
961            // SAFETY: tp.is_concrete_sequence()
962            unsafe { unreachable_unchecked() }
963        };
964        checker.comment("Flattening concrete sequence argument");
965        new_args.into_iter().rfold(body.clone(), |body, arg| {
966            Term::Bound(BindingTerm::new(
967                b.head.clone(),
968                Box::new([
969                    BoundArgument::Bound(ComponentVar {
970                        var: Variable::Name {
971                            name: crate::DUMMY.clone(),
972                            notated: None,
973                        },
974                        tp: Some(arg),
975                        df: None,
976                    }),
977                    BoundArgument::Simple(body),
978                ]),
979                b.presentation.clone(),
980            ))
981        })
982    }
983
984    // INVARIANT: !seq.is_empty()
985    pub(super) fn recurse_seq_args<'t, Split: SplitStrategy>(
986        uri: &SymbolUri,
987        checker: &mut CheckRef<'t, '_, Split>,
988        b: &BindingTerm,
989        seq: &'t [Term],
990        body: &Term,
991    ) -> Option<Term> {
992        // SAFETY: !seq.is_empty()
993        let first = unsafe { seq.first().unwrap_unchecked() };
994        let rest = &seq[1..];
995        let mut ret = Self::simple_apply(checker, b, first, body)?;
996        for arg in rest {
997            let b = Self::deconstruct_tp(uri, checker, ret).ok()?;
998            let [_, BoundArgument::Simple(body)] = &*b.arguments else {
999                // SAFETY: invariant of deconstruct_tp
1000                unsafe { unreachable_unchecked() }
1001            };
1002            ret = Self::simple_apply(checker, &b, arg, body)?;
1003        }
1004        Some(ret)
1005    }
1006
1007    fn try_extension<'t, Split: SplitStrategy>(
1008        &self,
1009        checker: &mut CheckRef<'t, '_, Split>,
1010        tp: &'t Term,
1011        args: &'t [Argument],
1012        index: &mut usize,
1013    ) -> Option<Term> {
1014        let exts = checker
1015            .rules()
1016            .marker()
1017            .iter()
1018            .rev()
1019            .filter_map(|rl| rl.as_any().downcast_ref::<PiExtensionRule<Split>>())
1020            .cloned()
1021            .collect::<SmallVec<_, 1>>();
1022        let arg = &args[*index];
1023        let Some(ntp) =
1024            checker.simplify_until(tp, |_, t| exts.iter().any(|rl| (rl.applicable)(rl, t, arg)))
1025        else {
1026            checker.failure("type is not a pi");
1027            return None;
1028        };
1029        for rl in exts {
1030            if (rl.applicable)(&rl, &ntp, arg)
1031                && let Some(t) = (rl.infer)(&rl, self, checker, &ntp, args, index)
1032            {
1033                return Some(t);
1034            }
1035        }
1036        None
1037    }
1038
1039    pub fn type_apply<'t, Split: SplitStrategy>(
1040        &self,
1041        checker: &mut CheckRef<'t, '_, Split>,
1042        tp: Term,
1043        args: &'t [Argument],
1044    ) -> Option<Term> {
1045        let mut ret = tp;
1046        let mut i = 0;
1047        loop {
1048            let Some(arg) = args.get(i) else {
1049                return Some(ret);
1050            };
1051            let dec = Self::deconstruct_tp(&self.0, checker, ret);
1052            let b = match dec {
1053                Ok(b) => b,
1054                Err(t) => {
1055                    ret =
1056                        checker.scoped(|checker| self.try_extension(checker, &t, args, &mut i))?;
1057                    continue;
1058                }
1059            };
1060            let [first, BoundArgument::Simple(body)] = &*b.arguments else {
1061                // SAFETY: invariant of deconstruct_tp
1062                unsafe { unreachable_unchecked() }
1063            };
1064            match (first, arg) {
1065                (
1066                    BoundArgument::Bound(ComponentVar {
1067                        var,
1068                        tp: Some(tp),
1069                        df: None,
1070                    }),
1071                    Argument::Sequence(seq),
1072                ) if !body.has_free_such_that(|v| v.name() == var.name())
1073                    && tp.as_sequence().is_some_and(|s| s.is_concrete()) =>
1074                {
1075                    ret = Self::flatten_sequence(checker, tp, &b, body.clone());
1076                }
1077                (
1078                    BoundArgument::Bound(ComponentVar {
1079                        var,
1080                        tp: Some(tp),
1081                        df: None,
1082                    }),
1083                    Argument::Sequence(MaybeSequence::Seq(seq)),
1084                ) if !seq.is_empty() => {
1085                    i += 1;
1086                    checker.counter("(a) Checking Argument ", i);
1087                    ret = Self::recurse_seq_args(&self.0, checker, &b, seq, body)?;
1088                }
1089                (_, Argument::Simple(arg)) => {
1090                    i += 1;
1091                    checker.counter("(b) Checking Argument ", i);
1092                    ret = Self::simple_apply(checker, &b, arg, body)?;
1093                }
1094                (_, Argument::Sequence(arg)) => {
1095                    i += 1;
1096                    checker.counter("(c) Checking Argument ", i);
1097                    ret = checker.scoped(|checker| Self::seq_apply(checker, &b, arg, body))?;
1098                }
1099            }
1100        }
1101    }
1102
1103    pub(super) fn simple_apply<'t, Split: SplitStrategy>(
1104        checker: &mut CheckRef<'t, '_, Split>,
1105        b: &BindingTerm,
1106        arg: &'t Term,
1107        body: &Term,
1108    ) -> Option<Term> {
1109        let headvar = match b.arguments.first() {
1110            Some(BoundArgument::Bound(headvar)) => headvar,
1111            Some(BoundArgument::BoundSeq(MaybeSequence::Seq(vs))) => {
1112                if let [headvar] = &**vs {
1113                    headvar
1114                } else {
1115                    checker.failure("First argument is not a bound variable");
1116                    return None;
1117                }
1118            }
1119            Some(BoundArgument::BoundSeq(MaybeSequence::One(v))) if arg.is_sequence() => v,
1120            Some(BoundArgument::BoundSeq(MaybeSequence::One(_))) => {
1121                let seq = Term::into_seq(std::iter::once(arg.clone()));
1122                return checker.scoped(|slf| Self::simple_apply(slf, b, &seq, body));
1123            }
1124            _ => {
1125                checker.failure("First argument is not a bound variable");
1126                /*checker.comment(format!(
1127                    "Here: {:?}{:?}  <-- {:?}",
1128                    b.head.debug_short(),
1129                    b.arguments,
1130                    arg.debug_short()
1131                ));*/
1132                return None;
1133            }
1134        };
1135
1136        let (varname, vartp) = match headvar {
1137            ComponentVar {
1138                var, tp: Some(tp), ..
1139            } => (var.name(), tp.clone()),
1140            ComponentVar { var, .. } => (
1141                var.name(),
1142                checker.scoped(|checker| {
1143                    checker
1144                        .infer_var_type(var)
1145                        .unwrap_or_else(|| checker.new_solvable())
1146                }),
1147            ),
1148        };
1149
1150        if checker
1151            .scoped(|checker| checker.check_type(arg, &vartp))
1152            .is_none_or(|b| !b)
1153        {
1154            return None;
1155        }
1156        Some((body / (varname, arg)).into_owned())
1157    }
1158
1159    pub(super) fn seq_apply<'t, Split: SplitStrategy>(
1160        checker: &mut CheckRef<'t, '_, Split>,
1161        b: &'t BindingTerm,
1162        arg: &'t MaybeSequence<Term>,
1163        body: &Term,
1164    ) -> Option<Term> {
1165        if let Some(BoundArgument::Bound(ComponentVar {
1166            var,
1167            tp: Some(tp),
1168            df: None,
1169        })) = b.arguments.first()
1170            && let Some(tpargs) = tp.as_sequence().and_then(|s| s.to_concrete())
1171            && !body
1172                .free_variables()
1173                .into_iter()
1174                .any(|v| v.name() == var.name())
1175            && let MaybeSequence::Seq(args) = arg
1176            && args.len() == tpargs.len()
1177        {
1178            for (a, t) in args.iter().zip(tpargs.iter()) {
1179                if !checker.scoped(|checker| checker.check_type(a, t))? {
1180                    return None;
1181                }
1182            }
1183            return Some(body.clone());
1184        }
1185
1186        let Some(BoundArgument::BoundSeq(MaybeSequence::One(headvar))) = b.arguments.first() else {
1187            checker.failure("First argument is not a bound variable sequence");
1188            /*checker.comment(format!(
1189                "Here: {:?}{:?}  <-- {arg:?}",
1190                b.head.debug_short(),
1191                b.arguments
1192            ));*/
1193            return None;
1194        };
1195
1196        let (varname, vartp) = match headvar {
1197            ComponentVar {
1198                var, tp: Some(tp), ..
1199            } => (var.name(), tp.clone()),
1200            ComponentVar { var, .. } => (
1201                var.name(),
1202                checker.scoped(|checker| {
1203                    checker
1204                        .infer_var_type(var)
1205                        .unwrap_or_else(|| checker.new_solvable())
1206                }),
1207            ),
1208        };
1209
1210        match arg {
1211            MaybeSequence::One(arg) => {
1212                if checker
1213                    .scoped(|checker| checker.check_type(arg, &vartp))
1214                    .is_none_or(|b| !b)
1215                {
1216                    return None;
1217                }
1218                Some((body / (varname, arg)).into_owned())
1219            }
1220            MaybeSequence::Seq(arg) => {
1221                let narg = Term::into_seq(arg.iter().cloned());
1222                if let Some(SequenceType::SeqType(vartp, _)) = vartp.as_sequence_type() {
1223                    if !checker.scoped(|checker| {
1224                        for a in arg {
1225                            if !checker.check_type(a, vartp)? {
1226                                return None;
1227                            }
1228                        }
1229                        Some(true)
1230                    })? {
1231                        return None;
1232                    }
1233                } else if checker
1234                    .scoped(|checker| checker.check_type(&narg, &vartp))
1235                    .is_none_or(|b| !b)
1236                {
1237                    return None;
1238                }
1239
1240                Some((body / (varname, &narg)).into_owned())
1241            }
1242        }
1243    }
1244}
1245
1246#[derive(Debug, Clone, PartialEq, Eq)]
1247pub struct EtaRule(pub SymbolUri);
1248impl SizedSolverRule for EtaRule {
1249    fn display(&self) -> Vec<crate::trace::Displayable> {
1250        ftml_solver_trace::trace!(&self.0, " x1:A1,...,xn:An. s(x1,...,xn) ==> s")
1251    }
1252}
1253impl<Split: SplitStrategy> SimplificationRule<Split> for EtaRule {
1254    fn applicable(&self, term: &Term) -> bool {
1255        fn applicable_inner(idx: usize, term: &Term, slf: &SymbolUri) -> bool {
1256            if let Term::Bound(op) = &term
1257                && let Term::Symbol { uri, .. } = &op.head
1258                && *uri == *slf
1259                && op.arguments.len() == 2
1260                && let Some(BoundArgument::Bound(v)) = op.arguments.first()
1261                && let Some(BoundArgument::Simple(a)) = op.arguments.get(1)
1262            {
1263                matches!(a,Term::Application(app) if matches!(app.arguments.get(idx),Some(Argument::Simple(Term::Var { variable, .. })) if variable.name() == v.var.name()))
1264                    || applicable_inner(idx + 1, a, slf)
1265            } else {
1266                false
1267            }
1268        }
1269        applicable_inner(0, term, &self.0)
1270    }
1271    fn apply<'t>(
1272        &self,
1273        checker: CheckRef<'t, '_, Split>,
1274        mut term: &'t Term,
1275    ) -> Result<Term, Option<ftml_ontology::terms::termpaths::TermPath>> {
1276        let mut vars = Vec::new();
1277        loop {
1278            let Term::Bound(op) = term else {
1279                return Err(None);
1280            };
1281            let Term::Symbol { uri, .. } = &op.head else {
1282                return Err(None);
1283            };
1284            if *uri != self.0 {
1285                return Err(None);
1286            };
1287            let [BoundArgument::Bound(v), BoundArgument::Simple(body)] = &*op.arguments else {
1288                return Err(None);
1289            };
1290            vars.push(&v.var);
1291            match body {
1292                Term::Application(app) if app.arguments.len() >= vars.len() => {
1293                    let idx = app.arguments.len() - vars.len();
1294                    let margs = &app.arguments[idx..];
1295                    for (a, v) in margs.iter().zip(vars.iter()) {
1296                        if let Argument::Simple(Term::Var { variable, .. }) = a
1297                            && variable.name() == v.name()
1298                        {
1299                            // all good
1300                        } else {
1301                            return Err(None);
1302                        }
1303                    }
1304                    if idx == 0 {
1305                        return Ok(app.head.clone());
1306                    }
1307                    return Ok(Term::Application(ApplicationTerm::new(
1308                        app.head.clone(),
1309                        app.arguments.iter().take(idx).cloned().collect(),
1310                        None,
1311                    )));
1312                }
1313                _ => term = body,
1314            }
1315        }
1316    }
1317}
1318
1319#[derive(Debug, Clone, PartialEq, Eq)]
1320pub struct BetaRule(pub SymbolUri);
1321impl SizedSolverRule for BetaRule {
1322    fn priority(&self) -> isize {
1323        100_000_000
1324    }
1325    fn display(&self) -> Vec<crate::trace::Displayable> {
1326        ftml_solver_trace::trace!("{ a:A } (", &self.0, " x:A. t)(a) ==> t[x/a]")
1327    }
1328}
1329impl<Split: SplitStrategy> SimplificationRule<Split> for BetaRule {
1330    fn applicable(&self, term: &Term) -> bool {
1331        if let Term::Application(app) = term
1332            && let Term::Bound(op) = &app.head
1333            && let Term::Symbol { uri, .. } = &op.head
1334        {
1335            *uri == self.0 && app.arguments.len() >= op.arguments.len() - 1
1336        } else {
1337            false
1338        }
1339    }
1340    fn apply<'t>(
1341        &self,
1342        mut checker: CheckRef<'t, '_, Split>,
1343        term: &'t Term,
1344    ) -> Result<Term, Option<ftml_ontology::terms::termpaths::TermPath>> {
1345        let Term::Application(app) = term else {
1346            return Err(None);
1347        };
1348        let Term::Bound(fun) = &app.head else {
1349            return Err(None);
1350        };
1351        let Some(BoundArgument::Simple(ret)) = fun.arguments.last() else {
1352            return Err(None);
1353        };
1354        let funargs = &fun.arguments[..fun.arguments.len() - 1];
1355        let actual_args = &app.arguments[..funargs.len()];
1356        let rest_args = &app.arguments[funargs.len()..];
1357        let mut ret = Cow::Borrowed(ret);
1358        for (i, (v, a)) in funargs.iter().zip(actual_args).enumerate() {
1359            checker.counter("Checking argument ", i + 1);
1360            match (v, a) {
1361                (
1362                    BoundArgument::Bound(ComponentVar {
1363                        var,
1364                        tp: Some(tp),
1365                        df: None,
1366                    }),
1367                    Argument::Simple(a),
1368                ) => {
1369                    if !checker.check_type(a, tp).ok_or(None)? {
1370                        return Err(None);
1371                    }
1372                    if let Cow::Owned(nr) = &*ret / (var.name(), a) {
1373                        ret = Cow::Owned(nr);
1374                    }
1375                }
1376                (
1377                    BoundArgument::Bound(ComponentVar {
1378                        var,
1379                        tp: None,
1380                        df: None,
1381                    }),
1382                    Argument::Simple(a),
1383                ) => {
1384                    let Some(tp) = checker.infer_var_type(var) else {
1385                        checker.add_msg(traceref!(FAIL "untyped variable ",var).into());
1386                        return Err(None);
1387                    };
1388                    if checker.scoped(|checker| checker.check_type(a, &tp)) != Some(true) {
1389                        return Err(None);
1390                    }
1391                    if let Cow::Owned(nr) = &*ret / (var.name(), a) {
1392                        ret = Cow::Owned(nr);
1393                    }
1394                }
1395                (
1396                    BoundArgument::BoundSeq(MaybeSequence::One(ComponentVar {
1397                        var,
1398                        tp: Some(tp),
1399                        df: None,
1400                    })),
1401                    Argument::Sequence(MaybeSequence::Seq(ts)),
1402                ) => {
1403                    let Some(SequenceType::SeqType(tp, _)) = tp.as_sequence_type() else {
1404                        checker.failure("Type of sequence variable is not a sequence type");
1405                        //checker.comment(format!("Here: {:?} <-> {ts:?}", tp.debug_short()));
1406                        return Err(None);
1407                    };
1408                    for t in ts {
1409                        if !checker.check_type(t, tp).ok_or(None)? {
1410                            return Err(None);
1411                        }
1412                    }
1413                    if let Cow::Owned(nr) =
1414                        &*ret / (var.name(), &Term::into_seq(ts.iter().cloned()))
1415                    {
1416                        ret = Cow::Owned(nr);
1417                    }
1418                }
1419                (
1420                    BoundArgument::BoundSeq(MaybeSequence::One(ComponentVar {
1421                        var,
1422                        tp: Some(tp),
1423                        df: None,
1424                    })),
1425                    Argument::Simple(t),
1426                ) => {
1427                    if tp.as_sequence_type().is_none() {
1428                        checker.failure("Type of sequence variable is not a sequence type");
1429                        //checker.comment(format!("Here: {:?} <-> {ts:?}", tp.debug_short()));
1430                        return Err(None);
1431                    }
1432                    if !checker.check_type(t, tp).ok_or(None)? {
1433                        return Err(None);
1434                    }
1435                    if let Cow::Owned(nr) = &*ret / (var.name(), t) {
1436                        ret = Cow::Owned(nr);
1437                    }
1438                }
1439
1440                (
1441                    BoundArgument::Bound(ComponentVar {
1442                        var,
1443                        tp: None,
1444                        df: None,
1445                    }),
1446                    Argument::Sequence(MaybeSequence::Seq(args)),
1447                ) => {
1448                    let Some(tp) = checker.infer_var_type(var) else {
1449                        checker.add_msg(traceref!(FAIL "untyped variable ",var).into());
1450                        return Err(None);
1451                    };
1452                    let Some(tp) = checker.scoped(|checker| {
1453                        checker
1454                            .simplify_until(&tp, |_, t| {
1455                                t.as_sequence().is_some_and(|s| s.is_concrete())
1456                            })
1457                            .map(Cow::into_owned)
1458                    }) else {
1459                        checker.failure("Not a concrete sequence");
1460                        return Err(None);
1461                    };
1462                    let vartps = tp.as_sequence().and_then(|s| s.to_concrete()).ok_or(None)?;
1463                    if vartps.len() != args.len() {
1464                        checker.failure("sequence lengths don't match");
1465                        return Err(None);
1466                    }
1467                    for (a, tp) in args.iter().zip(vartps) {
1468                        if !checker
1469                            .scoped(|checker| checker.check_type(a, &tp))
1470                            .ok_or(None)?
1471                        {
1472                            return Err(None);
1473                        }
1474                    }
1475                }
1476                (
1477                    BoundArgument::Bound(ComponentVar {
1478                        var,
1479                        tp: Some(tp),
1480                        df: None,
1481                    }),
1482                    Argument::Sequence(MaybeSequence::Seq(args)),
1483                ) => {
1484                    let ntp = checker
1485                        .scoped(|checker| {
1486                            checker
1487                                .simplify_until(tp, |_, t| {
1488                                    t.as_sequence().is_some_and(|s| s.is_concrete())
1489                                })
1490                                .map(Cow::into_owned)
1491                        })
1492                        .ok_or(None)?;
1493                    let Some(vartps) = ntp.as_sequence().and_then(|s| s.to_concrete()) else {
1494                        checker.failure("type of bound variable not a concrete sequence");
1495                        return Err(None);
1496                    };
1497                    if vartps.len() != args.len() {
1498                        checker.failure("sequence lengths don't match");
1499                        return Err(None);
1500                    }
1501                    for (a, tp) in args.iter().zip(vartps) {
1502                        if !checker
1503                            .scoped(|checker| checker.check_type(a, &tp))
1504                            .ok_or(None)?
1505                        {
1506                            return Err(None);
1507                        }
1508                    }
1509                }
1510
1511                (a, b) => {
1512                    checker.failure(format!("TODO: {a:?} <-> {b:?}"));
1513                    return Err(None);
1514                }
1515            }
1516        }
1517        if rest_args.is_empty() {
1518            Ok(ret.into_owned())
1519        } else {
1520            Ok(Term::Application(ApplicationTerm::new(
1521                ret.into_owned(),
1522                rest_args.iter().cloned().collect(),
1523                None,
1524            )))
1525        }
1526    }
1527}
1528
1529#[derive(Debug, Clone, PartialEq, Eq)]
1530pub struct ApplyRule(pub SymbolUri);
1531impl SizedSolverRule for ApplyRule {
1532    fn display(&self) -> Vec<crate::trace::Displayable> {
1533        ftml_solver_trace::trace!("{ a:A } ", &self.0, "(f,a*) ==> f(a*)")
1534    }
1535    fn priority(&self) -> isize {
1536        isize::MAX
1537    }
1538}
1539impl<Split: SplitStrategy> PreparationRule<Split> for ApplyRule {
1540    fn applicable(&self, _: &CheckRef<'_, '_, Split>, t: &Term) -> bool {
1541        if let Term::Application(app) = t
1542            && let [Argument::Simple(_), Argument::Sequence(_)] = &*app.arguments
1543            && let Term::Symbol { uri, .. } = &app.head
1544        {
1545            *uri == self.0
1546        } else {
1547            false
1548        }
1549    }
1550    fn apply(
1551        &self,
1552        _: &mut CheckRef<'_, '_, Split>,
1553        t: Term,
1554        path: Option<(&mut smallvec::SmallVec<u8, 16>, usize)>,
1555    ) -> std::ops::ControlFlow<Term, Term> {
1556        let Term::Application(app) = t else {
1557            return std::ops::ControlFlow::Continue(t);
1558        };
1559        let [Argument::Simple(f), Argument::Sequence(a)] = &*app.arguments else {
1560            return std::ops::ControlFlow::Continue(Term::Application(app));
1561        };
1562        let ret = Term::Application(ApplicationTerm::new(
1563            f.clone(),
1564            match a {
1565                MaybeSequence::One(o) => {
1566                    Box::new([Argument::Sequence(MaybeSequence::One(o.clone()))])
1567                }
1568                MaybeSequence::Seq(ts) => ts.iter().map(|t| Argument::Simple(t.clone())).collect(),
1569            },
1570            /*Box::new([Argument::Sequence(match a {
1571                MaybeSequence::One(o) => MaybeSequence::One(o.clone()),
1572                MaybeSequence::Seq(ts) => MaybeSequence::Seq(ts.clone()),
1573            })]),*/
1574            app.presentation.clone(),
1575        ));
1576        if let Some((p, i)) = path
1577            && let Some(j) = p.get_mut(i)
1578        {
1579            *j = j.saturating_sub(1);
1580        }
1581        std::ops::ControlFlow::Continue(ret)
1582    }
1583    fn applicable_revert(&self, _: &CheckRef<'_, '_, Split>, _: &Term) -> bool {
1584        false
1585    }
1586    fn revert(&self, _: &CheckRef<'_, '_, Split>, t: Term) -> std::ops::ControlFlow<Term, Term> {
1587        std::ops::ControlFlow::Continue(t)
1588    }
1589}
ftml_solver/rules/operators/pi.rs

ftml_solver/rules/operators/
pi.rs
