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| matches!(t, Term::Bound(_)))? {
922                Cow::Borrowed(_) => Some(None),
923                Cow::Owned(tp) => Some(Some(tp)),
924            }
925        }) else {
926            checker.add_msg(traceref!(FAIL "type is not a binder: ",tp.clone()).into());
927            return Err(tp);
928        };
929        let Term::Bound(b) = nret.unwrap_or(tp) else {
930            // SAFETY: simplify_until above would have returned None otherwise
931            unsafe { unreachable_unchecked() }
932        };
933        if !matches!(&b.head,Term::Symbol { uri, .. } if *uri == *bind_uri)
934            || b.arguments.len() != 2
935            || !matches!(b.arguments.get(1), Some(BoundArgument::Simple(_)))
936        {
937            checker.failure("Type is not a Π anymore");
938            return Err(Term::Bound(b));
939        }
940        Ok(b)
941    }
942
943    // INVARIANT: tp.is_concrete_sequence()
944    pub(super) fn flatten_sequence<Split: SplitStrategy>(
945        checker: &mut CheckRef<'_, '_, Split>,
946        tp: &Term,
947        b: &BindingTerm,
948        body: Term,
949    ) -> Term {
950        let Some(new_args) = tp.as_sequence().and_then(|s| s.to_concrete()) else {
951            // SAFETY: tp.is_concrete_sequence()
952            unsafe { unreachable_unchecked() }
953        };
954        checker.comment("Flattening concrete sequence argument");
955        new_args.into_iter().rfold(body.clone(), |body, arg| {
956            Term::Bound(BindingTerm::new(
957                b.head.clone(),
958                Box::new([
959                    BoundArgument::Bound(ComponentVar {
960                        var: Variable::Name {
961                            name: crate::DUMMY.clone(),
962                            notated: None,
963                        },
964                        tp: Some(arg),
965                        df: None,
966                    }),
967                    BoundArgument::Simple(body),
968                ]),
969                b.presentation.clone(),
970            ))
971        })
972    }
973
974    // INVARIANT: !seq.is_empty()
975    pub(super) fn recurse_seq_args<'t, Split: SplitStrategy>(
976        uri: &SymbolUri,
977        checker: &mut CheckRef<'t, '_, Split>,
978        b: &BindingTerm,
979        seq: &'t [Term],
980        body: &Term,
981    ) -> Option<Term> {
982        // SAFETY: !seq.is_empty()
983        let first = unsafe { seq.first().unwrap_unchecked() };
984        let rest = &seq[1..];
985        let mut ret = Self::simple_apply(checker, b, first, body)?;
986        for arg in rest {
987            let b = Self::deconstruct_tp(uri, checker, ret).ok()?;
988            let [_, BoundArgument::Simple(body)] = &*b.arguments else {
989                // SAFETY: invariant of deconstruct_tp
990                unsafe { unreachable_unchecked() }
991            };
992            ret = Self::simple_apply(checker, &b, arg, body)?;
993        }
994        Some(ret)
995    }
996
997    fn try_extension<'t, Split: SplitStrategy>(
998        &self,
999        checker: &mut CheckRef<'t, '_, Split>,
1000        tp: &'t Term,
1001        args: &'t [Argument],
1002        index: &mut usize,
1003    ) -> Option<Term> {
1004        let exts = checker
1005            .rules()
1006            .marker()
1007            .iter()
1008            .rev()
1009            .filter_map(|rl| rl.as_any().downcast_ref::<PiExtensionRule<Split>>())
1010            .cloned()
1011            .collect::<SmallVec<_, 1>>();
1012        let arg = &args[*index];
1013        let Some(ntp) =
1014            checker.simplify_until(tp, |_, t| exts.iter().any(|rl| (rl.applicable)(rl, t, arg)))
1015        else {
1016            checker.failure("type is not a pi");
1017            return None;
1018        };
1019        for rl in exts {
1020            if (rl.applicable)(&rl, &ntp, arg)
1021                && let Some(t) = (rl.infer)(&rl, self, checker, &ntp, args, index)
1022            {
1023                return Some(t);
1024            }
1025        }
1026        None
1027    }
1028
1029    pub fn type_apply<'t, Split: SplitStrategy>(
1030        &self,
1031        checker: &mut CheckRef<'t, '_, Split>,
1032        tp: Term,
1033        args: &'t [Argument],
1034    ) -> Option<Term> {
1035        let mut ret = tp;
1036        let mut i = 0;
1037        loop {
1038            let Some(arg) = args.get(i) else {
1039                return Some(ret);
1040            };
1041            let dec = Self::deconstruct_tp(&self.0, checker, ret);
1042            let b = match dec {
1043                Ok(b) => b,
1044                Err(t) => {
1045                    ret =
1046                        checker.scoped(|checker| self.try_extension(checker, &t, args, &mut i))?;
1047                    continue;
1048                }
1049            };
1050            let [first, BoundArgument::Simple(body)] = &*b.arguments else {
1051                // SAFETY: invariant of deconstruct_tp
1052                unsafe { unreachable_unchecked() }
1053            };
1054            match (first, arg) {
1055                (
1056                    BoundArgument::Bound(ComponentVar {
1057                        var,
1058                        tp: Some(tp),
1059                        df: None,
1060                    }),
1061                    Argument::Sequence(seq),
1062                ) if !body.has_free_such_that(|v| v.name() == var.name())
1063                    && tp.as_sequence().is_some_and(|s| s.is_concrete()) =>
1064                {
1065                    ret = Self::flatten_sequence(checker, tp, &b, body.clone());
1066                }
1067                (
1068                    BoundArgument::Bound(ComponentVar {
1069                        var,
1070                        tp: Some(tp),
1071                        df: None,
1072                    }),
1073                    Argument::Sequence(MaybeSequence::Seq(seq)),
1074                ) if !seq.is_empty() => {
1075                    i += 1;
1076                    checker.counter("(a) Checking Argument ", i);
1077                    ret = Self::recurse_seq_args(&self.0, checker, &b, seq, body)?;
1078                }
1079                (_, Argument::Simple(arg)) => {
1080                    i += 1;
1081                    checker.counter("(b) Checking Argument ", i);
1082                    ret = Self::simple_apply(checker, &b, arg, body)?;
1083                }
1084                (_, Argument::Sequence(arg)) => {
1085                    i += 1;
1086                    checker.counter("(c) Checking Argument ", i);
1087                    ret = checker.scoped(|checker| Self::seq_apply(checker, &b, arg, body))?;
1088                }
1089            }
1090        }
1091    }
1092
1093    pub(super) fn simple_apply<'t, Split: SplitStrategy>(
1094        checker: &mut CheckRef<'t, '_, Split>,
1095        b: &BindingTerm,
1096        arg: &'t Term,
1097        body: &Term,
1098    ) -> Option<Term> {
1099        let headvar = match b.arguments.first() {
1100            Some(BoundArgument::Bound(headvar)) => headvar,
1101            Some(BoundArgument::BoundSeq(MaybeSequence::Seq(vs))) => {
1102                if let [headvar] = &**vs {
1103                    headvar
1104                } else {
1105                    checker.failure("First argument is not a bound variable");
1106                    return None;
1107                }
1108            }
1109            Some(BoundArgument::BoundSeq(MaybeSequence::One(v))) if arg.is_sequence() => v,
1110            Some(BoundArgument::BoundSeq(MaybeSequence::One(_))) => {
1111                let seq = Term::into_seq(std::iter::once(arg.clone()));
1112                return checker.scoped(|slf| Self::simple_apply(slf, b, &seq, body));
1113            }
1114            _ => {
1115                checker.failure("First argument is not a bound variable");
1116                /*checker.comment(format!(
1117                    "Here: {:?}{:?}  <-- {:?}",
1118                    b.head.debug_short(),
1119                    b.arguments,
1120                    arg.debug_short()
1121                ));*/
1122                return None;
1123            }
1124        };
1125
1126        let (varname, vartp) = match headvar {
1127            ComponentVar {
1128                var, tp: Some(tp), ..
1129            } => (var.name(), tp.clone()),
1130            ComponentVar { var, .. } => (
1131                var.name(),
1132                checker.scoped(|checker| {
1133                    checker
1134                        .infer_var_type(var)
1135                        .unwrap_or_else(|| checker.new_solvable())
1136                }),
1137            ),
1138        };
1139
1140        if checker
1141            .scoped(|checker| checker.check_type(arg, &vartp))
1142            .is_none_or(|b| !b)
1143        {
1144            return None;
1145        }
1146        Some((body / (varname, arg)).into_owned())
1147    }
1148
1149    pub(super) fn seq_apply<'t, Split: SplitStrategy>(
1150        checker: &mut CheckRef<'t, '_, Split>,
1151        b: &'t BindingTerm,
1152        arg: &'t MaybeSequence<Term>,
1153        body: &Term,
1154    ) -> Option<Term> {
1155        if let Some(BoundArgument::Bound(ComponentVar {
1156            var,
1157            tp: Some(tp),
1158            df: None,
1159        })) = b.arguments.first()
1160            && let Some(tpargs) = tp.as_sequence().and_then(|s| s.to_concrete())
1161            && !body
1162                .free_variables()
1163                .into_iter()
1164                .any(|v| v.name() == var.name())
1165            && let MaybeSequence::Seq(args) = arg
1166            && args.len() == tpargs.len()
1167        {
1168            for (a, t) in args.iter().zip(tpargs.iter()) {
1169                if !checker.scoped(|checker| checker.check_type(a, t))? {
1170                    return None;
1171                }
1172            }
1173            return Some(body.clone());
1174        }
1175
1176        let Some(BoundArgument::BoundSeq(MaybeSequence::One(headvar))) = b.arguments.first() else {
1177            checker.failure("First argument is not a bound variable sequence");
1178            /*checker.comment(format!(
1179                "Here: {:?}{:?}  <-- {arg:?}",
1180                b.head.debug_short(),
1181                b.arguments
1182            ));*/
1183            return None;
1184        };
1185
1186        let (varname, vartp) = match headvar {
1187            ComponentVar {
1188                var, tp: Some(tp), ..
1189            } => (var.name(), tp.clone()),
1190            ComponentVar { var, .. } => (
1191                var.name(),
1192                checker.scoped(|checker| {
1193                    checker
1194                        .infer_var_type(var)
1195                        .unwrap_or_else(|| checker.new_solvable())
1196                }),
1197            ),
1198        };
1199
1200        match arg {
1201            MaybeSequence::One(arg) => {
1202                if checker
1203                    .scoped(|checker| checker.check_type(arg, &vartp))
1204                    .is_none_or(|b| !b)
1205                {
1206                    return None;
1207                }
1208                Some((body / (varname, arg)).into_owned())
1209            }
1210            MaybeSequence::Seq(arg) => {
1211                let narg = Term::into_seq(arg.iter().cloned());
1212                if let Some(SequenceType::SeqType(vartp, _)) = vartp.as_sequence_type() {
1213                    if !checker.scoped(|checker| {
1214                        for a in arg {
1215                            if !checker.check_type(a, vartp)? {
1216                                return None;
1217                            }
1218                        }
1219                        Some(true)
1220                    })? {
1221                        return None;
1222                    }
1223                } else if checker
1224                    .scoped(|checker| checker.check_type(&narg, &vartp))
1225                    .is_none_or(|b| !b)
1226                {
1227                    return None;
1228                }
1229
1230                Some((body / (varname, &narg)).into_owned())
1231            }
1232        }
1233    }
1234}
1235
1236#[derive(Debug, Clone, PartialEq, Eq)]
1237pub struct BetaRule(pub SymbolUri);
1238impl SizedSolverRule for BetaRule {
1239    fn display(&self) -> Vec<crate::trace::Displayable> {
1240        ftml_solver_trace::trace!("{ a:A } (", &self.0, " x:A. t)(a) ==> t[x/a]")
1241    }
1242}
1243impl<Split: SplitStrategy> SimplificationRule<Split> for BetaRule {
1244    fn applicable(&self, term: &Term) -> bool {
1245        if let Term::Application(app) = term
1246            && let Term::Bound(op) = &app.head
1247            && let Term::Symbol { uri, .. } = &op.head
1248        {
1249            *uri == self.0 && app.arguments.len() >= op.arguments.len() - 1
1250        } else {
1251            false
1252        }
1253    }
1254    fn apply<'t>(
1255        &self,
1256        mut checker: CheckRef<'t, '_, Split>,
1257        term: &'t Term,
1258    ) -> Result<Term, Option<ftml_ontology::terms::termpaths::TermPath>> {
1259        let Term::Application(app) = term else {
1260            return Err(None);
1261        };
1262        let Term::Bound(fun) = &app.head else {
1263            return Err(None);
1264        };
1265        let Some(BoundArgument::Simple(ret)) = fun.arguments.last() else {
1266            return Err(None);
1267        };
1268        let funargs = &fun.arguments[..fun.arguments.len() - 1];
1269        let actual_args = &app.arguments[..funargs.len()];
1270        let rest_args = &app.arguments[funargs.len()..];
1271        let mut ret = Cow::Borrowed(ret);
1272        for (i, (v, a)) in funargs.iter().zip(actual_args).enumerate() {
1273            checker.counter("Checking argument ", i + 1);
1274            match (v, a) {
1275                (
1276                    BoundArgument::Bound(ComponentVar {
1277                        var,
1278                        tp: Some(tp),
1279                        df: None,
1280                    }),
1281                    Argument::Simple(a),
1282                ) => {
1283                    if !checker.check_type(a, tp).ok_or(None)? {
1284                        return Err(None);
1285                    }
1286                    if let Cow::Owned(nr) = &*ret / (var.name(), a) {
1287                        ret = Cow::Owned(nr);
1288                    }
1289                }
1290                (
1291                    BoundArgument::Bound(ComponentVar {
1292                        var,
1293                        tp: None,
1294                        df: None,
1295                    }),
1296                    Argument::Simple(a),
1297                ) => {
1298                    let Some(tp) = checker.infer_var_type(var) else {
1299                        checker.add_msg(traceref!(FAIL "untyped variable ",var).into());
1300                        return Err(None);
1301                    };
1302                    if checker.scoped(|checker| checker.check_type(a, &tp)) != Some(true) {
1303                        return Err(None);
1304                    }
1305                    if let Cow::Owned(nr) = &*ret / (var.name(), a) {
1306                        ret = Cow::Owned(nr);
1307                    }
1308                }
1309                (
1310                    BoundArgument::BoundSeq(MaybeSequence::One(ComponentVar {
1311                        var,
1312                        tp: Some(tp),
1313                        df: None,
1314                    })),
1315                    Argument::Sequence(MaybeSequence::Seq(ts)),
1316                ) => {
1317                    let Some(SequenceType::SeqType(tp, _)) = tp.as_sequence_type() else {
1318                        checker.failure("Type of sequence variable is not a sequence type");
1319                        //checker.comment(format!("Here: {:?} <-> {ts:?}", tp.debug_short()));
1320                        return Err(None);
1321                    };
1322                    for t in ts {
1323                        if !checker.check_type(t, tp).ok_or(None)? {
1324                            return Err(None);
1325                        }
1326                    }
1327                    if let Cow::Owned(nr) =
1328                        &*ret / (var.name(), &Term::into_seq(ts.iter().cloned()))
1329                    {
1330                        ret = Cow::Owned(nr);
1331                    }
1332                }
1333                (
1334                    BoundArgument::BoundSeq(MaybeSequence::One(ComponentVar {
1335                        var,
1336                        tp: Some(tp),
1337                        df: None,
1338                    })),
1339                    Argument::Simple(t),
1340                ) => {
1341                    if tp.as_sequence_type().is_none() {
1342                        checker.failure("Type of sequence variable is not a sequence type");
1343                        //checker.comment(format!("Here: {:?} <-> {ts:?}", tp.debug_short()));
1344                        return Err(None);
1345                    }
1346                    if !checker.check_type(t, tp).ok_or(None)? {
1347                        return Err(None);
1348                    }
1349                    if let Cow::Owned(nr) = &*ret / (var.name(), t) {
1350                        ret = Cow::Owned(nr);
1351                    }
1352                }
1353
1354                (
1355                    BoundArgument::Bound(ComponentVar {
1356                        var,
1357                        tp: None,
1358                        df: None,
1359                    }),
1360                    Argument::Sequence(MaybeSequence::Seq(args)),
1361                ) => {
1362                    let Some(tp) = checker.infer_var_type(var) else {
1363                        checker.add_msg(traceref!(FAIL "untyped variable ",var).into());
1364                        return Err(None);
1365                    };
1366                    let Some(tp) = checker.scoped(|checker| {
1367                        checker
1368                            .simplify_until(&tp, |_, t| {
1369                                t.as_sequence().is_some_and(|s| s.is_concrete())
1370                            })
1371                            .map(Cow::into_owned)
1372                    }) else {
1373                        checker.failure("Not a concrete sequence");
1374                        return Err(None);
1375                    };
1376                    let vartps = tp.as_sequence().and_then(|s| s.to_concrete()).ok_or(None)?;
1377                    if vartps.len() != args.len() {
1378                        checker.failure("sequence lengths don't match");
1379                        return Err(None);
1380                    }
1381                    for (a, tp) in args.iter().zip(vartps) {
1382                        if !checker
1383                            .scoped(|checker| checker.check_type(a, &tp))
1384                            .ok_or(None)?
1385                        {
1386                            return Err(None);
1387                        }
1388                    }
1389                }
1390                (
1391                    BoundArgument::Bound(ComponentVar {
1392                        var,
1393                        tp: Some(tp),
1394                        df: None,
1395                    }),
1396                    Argument::Sequence(MaybeSequence::Seq(args)),
1397                ) => {
1398                    let ntp = checker
1399                        .scoped(|checker| {
1400                            checker
1401                                .simplify_until(tp, |_, t| {
1402                                    t.as_sequence().is_some_and(|s| s.is_concrete())
1403                                })
1404                                .map(Cow::into_owned)
1405                        })
1406                        .ok_or(None)?;
1407                    let Some(vartps) = ntp.as_sequence().and_then(|s| s.to_concrete()) else {
1408                        checker.failure("type of bound variable not a concrete sequence");
1409                        return Err(None);
1410                    };
1411                    if vartps.len() != args.len() {
1412                        checker.failure("sequence lengths don't match");
1413                        return Err(None);
1414                    }
1415                    for (a, tp) in args.iter().zip(vartps) {
1416                        if !checker
1417                            .scoped(|checker| checker.check_type(a, &tp))
1418                            .ok_or(None)?
1419                        {
1420                            return Err(None);
1421                        }
1422                    }
1423                }
1424
1425                (a, b) => {
1426                    checker.failure(format!("TODO: {a:?} <-> {b:?}"));
1427                    return Err(None);
1428                }
1429            }
1430        }
1431        if rest_args.is_empty() {
1432            Ok(ret.into_owned())
1433        } else {
1434            Ok(Term::Application(ApplicationTerm::new(
1435                ret.into_owned(),
1436                rest_args.iter().cloned().collect(),
1437                None,
1438            )))
1439        }
1440    }
1441}
1442
1443#[derive(Debug, Clone, PartialEq, Eq)]
1444pub struct ApplyRule(pub SymbolUri);
1445impl SizedSolverRule for ApplyRule {
1446    fn display(&self) -> Vec<crate::trace::Displayable> {
1447        ftml_solver_trace::trace!("{ a:A } ", &self.0, "(f,a*) ==> f(a*)")
1448    }
1449    fn priority(&self) -> isize {
1450        isize::MAX
1451    }
1452}
1453impl<Split: SplitStrategy> PreparationRule<Split> for ApplyRule {
1454    fn applicable(&self, _: &CheckRef<'_, '_, Split>, t: &Term) -> bool {
1455        if let Term::Application(app) = t
1456            && let [Argument::Simple(_), Argument::Sequence(_)] = &*app.arguments
1457            && let Term::Symbol { uri, .. } = &app.head
1458        {
1459            *uri == self.0
1460        } else {
1461            false
1462        }
1463    }
1464    fn apply(
1465        &self,
1466        _: &mut CheckRef<'_, '_, Split>,
1467        t: Term,
1468        path: Option<(&mut smallvec::SmallVec<u8, 16>, usize)>,
1469    ) -> std::ops::ControlFlow<Term, Term> {
1470        let Term::Application(app) = t else {
1471            return std::ops::ControlFlow::Continue(t);
1472        };
1473        let [Argument::Simple(f), Argument::Sequence(a)] = &*app.arguments else {
1474            return std::ops::ControlFlow::Continue(Term::Application(app));
1475        };
1476        let ret = Term::Application(ApplicationTerm::new(
1477            f.clone(),
1478            match a {
1479                MaybeSequence::One(o) => {
1480                    Box::new([Argument::Sequence(MaybeSequence::One(o.clone()))])
1481                }
1482                MaybeSequence::Seq(ts) => ts.iter().map(|t| Argument::Simple(t.clone())).collect(),
1483            },
1484            /*Box::new([Argument::Sequence(match a {
1485                MaybeSequence::One(o) => MaybeSequence::One(o.clone()),
1486                MaybeSequence::Seq(ts) => MaybeSequence::Seq(ts.clone()),
1487            })]),*/
1488            app.presentation.clone(),
1489        ));
1490        if let Some((p, i)) = path
1491            && let Some(j) = p.get_mut(i)
1492        {
1493            *j = j.saturating_sub(1);
1494        }
1495        std::ops::ControlFlow::Continue(ret)
1496    }
1497    fn applicable_revert(&self, _: &CheckRef<'_, '_, Split>, _: &Term) -> bool {
1498        false
1499    }
1500    fn revert(&self, _: &CheckRef<'_, '_, Split>, t: Term) -> std::ops::ControlFlow<Term, Term> {
1501        std::ops::ControlFlow::Continue(t)
1502    }
1503}
ftml_solver/rules/operators/pi.rs

ftml_solver/rules/operators/
pi.rs
