ftml_solver/rules/
symbols.rs

1use std::{borrow::Cow, hint::unreachable_unchecked, sync::LazyLock};
2
3use ftml_ontology::terms::{
4    ApplicationTerm, Argument, ArgumentMode, BindingTerm, BoundArgument, ComponentVar,
5    MaybeSequence, Term, Variable, eq::Alpha, patterns::Pattern,
6};
7use ftml_solver_trace::SizedSolverRule;
8use ftml_uris::{DocumentUri, Id, ModuleUri, SymbolUri};
9
10use crate::{
11    CheckRef,
12    impls::solving::{is_solvable_id, is_solvable_var},
13    rules::{RuleSet, implicits::ImplicitExtApp},
14    split::SplitStrategy,
15};
16
17macro_rules! uri {
18    ($(  $name:ident  $(  : $t:ty := $l:literal)?   $( = $lb:literal )?  ),* $(,)?) => {
19        $(
20            uri!{@go
21                $name $( : $t := $l )? $( = $lb )?
22            }
23        )*
24    };
25    (@go $name:ident = $l:literal) => {
26            pub static $name: LazyLock<SymbolUri> = LazyLock::new(||
27                URI.clone() | $l.parse::<ftml_uris::UriName>().expect("Is a valid URI")
28            );
29    };
30    (@go $name:ident : $t:ty := $l:literal) => {
31            pub static $name: LazyLock<$t> = LazyLock::new(||
32                $l.parse().expect("Is a valid URI")
33            );
34    }
35}
36
37pub static NAMESPACE: &str = "http://mathhub.info?a=FTML/meta";
38uri! {
39    DOC_URI:DocumentUri := "http://mathhub.info?a=FTML/meta&d=Judgments&l=en",
40    URI:ModuleUri := "http://mathhub.info?a=FTML/meta&m=Judgments",
41
42    INH = "inhabitable",
43    UNIV = "universe",
44    HAS_PROOF = "has proof",
45    HAS_TYPE = "has type",
46    SUBTYPE = "subtype of",
47    SIMPLIFY = "simplifies to",
48    EQUAL = "equal",
49    BINDS = "binds"
50}
51
52pub trait GenericJudgment: SizedSolverRule {
53    fn parse<Split: SplitStrategy>(params: &[Term], rules: &mut RuleSet<Split>) {
54        parse(params, rules);
55    }
56    fn vars(&self) -> &[Id];
57    fn premises(&self) -> &[Premise];
58}
59pub fn parse<Split: SplitStrategy>(params: &[Term], rules: &mut RuleSet<Split>) {
60    /*
61    println!("Here!");
62    for p in params {
63        println!(" - {:?}",p.debug_short());
64    }
65     */
66
67    let Some(Term::Application(concl)) = params.last() else {
68        return;
69    };
70    let mut vars = Vec::new();
71    let mut premises = Vec::with_capacity(params.len() - 1);
72    for p in &params[..params.len() - 1] {
73        if let Some(p) = Premise::parse(p, &mut vars) {
74            premises.push(p);
75        } else {
76            return;
77        }
78    }
79
80    if let [Argument::Simple(t)] = &*concl.arguments {
81        if concl.head.is(&*INH) {
82            Pattern::from_with_vars(t, true, &mut vars);
83            rules.push_inhabitable(Box::new(GenericInhabitable {
84                vars: vars.into_boxed_slice(),
85                premises: premises.into_boxed_slice(),
86                concl: t.clone(),
87            }));
88        } else if concl.head.is(&*UNIV) {
89            Pattern::from_with_vars(t, true, &mut vars);
90            rules.push_universe(Box::new(GenericUniverse {
91                vars: vars.into_boxed_slice(),
92                premises: premises.into_boxed_slice(),
93                concl: t.clone(),
94            }));
95        } else if concl.head.is(&*HAS_PROOF) {
96            Pattern::from_with_vars(t, true, &mut vars);
97            rules.push_proof(Box::new(GenericProof {
98                vars: vars.into_boxed_slice(),
99                premises: premises.into_boxed_slice(),
100                concl: t.clone(),
101            }));
102        }
103    } else if let [Argument::Simple(a), Argument::Simple(b)] = &*concl.arguments {
104        if concl.head.is(&*HAS_TYPE) {
105            Pattern::from_with_vars(a, true, &mut vars);
106            Pattern::from_with_vars(b, true, &mut vars);
107            rules.push_checking(Box::new(GenericTyping {
108                vars: vars.into_boxed_slice(),
109                premises: premises.into_boxed_slice(),
110                concl: (a.clone(), b.clone()),
111            }));
112        } else if concl.head.is(&*SUBTYPE) {
113            Pattern::from_with_vars(a, true, &mut vars);
114            Pattern::from_with_vars(b, true, &mut vars);
115            rules.push_subtyping(Box::new(GenericSubtyping {
116                vars: vars.into_boxed_slice(),
117                premises: premises.into_boxed_slice(),
118                concl: (a.clone(), b.clone()),
119            }));
120        } else if concl.head.is(&*SIMPLIFY) {
121            Pattern::from_with_vars(a, true, &mut vars);
122            Pattern::from_with_vars(b, true, &mut vars);
123            rules.push_simplification(Box::new(GenericSimplification {
124                vars: vars.into_boxed_slice(),
125                premises: premises.into_boxed_slice(),
126                concl: (a.clone(), b.clone()),
127            }));
128        } else if concl.head.is(&*EQUAL) {
129            Pattern::from_with_vars(a, true, &mut vars);
130            Pattern::from_with_vars(b, true, &mut vars);
131            rules.push_equality(Box::new(GenericEquality {
132                vars: vars.into_boxed_slice(),
133                premises: premises.into_boxed_slice(),
134                concl: (a.clone(), b.clone()),
135            }));
136        } else if concl.head.is(&*BINDS)
137            && let Term::Var { variable, .. } = a
138        {
139            let b = undo_implicits(b).unwrap_or_else(|| b.clone());
140            Pattern::from_with_vars(&b, true, &mut vars);
141            rules.push_preparation(Box::new(GenericBindPrep {
142                vars: vars.into_boxed_slice(),
143                premises: premises.into_boxed_slice(),
144                concl: (variable.clone(), b),
145            }));
146        }
147    }
148}
149
150fn undo_implicits(term: &Term) -> Option<Term> {
151    if let Some((head, _)) = term.unapply_implicits() {
152        Some(head.clone())
153    } else if let Term::Application(app) = term
154        && let Some((head, _)) = app.head.unapply_implicits()
155    {
156        Some(Term::Application(ApplicationTerm::new(
157            head.clone(),
158            app.arguments.clone(),
159            app.presentation.clone(),
160        )))
161    } else if let Term::Bound(app) = term
162        && let Some((head, _)) = app.head.unapply_implicits()
163    {
164        Some(Term::Bound(BindingTerm::new(
165            head.clone(),
166            app.arguments.clone(),
167            app.presentation.clone(),
168        )))
169    } else {
170        None
171    }
172}
173
174macro_rules! judg {
175    ($($name:ident($concl:ty $(>$prec:literal)?):$rl:ident { $($impl:tt)* }),*$(,)?) => {
176        $(
177            #[derive(Clone,Debug,PartialEq,Eq)]
178            struct $name {
179                vars: Box<[Id]>,
180                premises: Box<[Premise]>,
181                concl: $concl,
182            }
183            impl SizedSolverRule for $name {
184                fn display(&self) -> Vec<ftml_solver_trace::Displayable> {
185                    ftml_solver_trace::trace!("Dynamic Rule")
186                }
187                $(
188                    fn priority(&self) -> isize {
189                        $prec
190                    }
191                )?
192            }
193            impl GenericJudgment for $name {
194                fn vars(&self) -> &[Id] { &self.vars}
195                fn premises(&self) -> &[Premise] {&self.premises}
196            }
197            impl<Split:SplitStrategy> crate::rules::$rl<Split> for $name {
198                $($impl)*
199            }
200        )*
201    };
202}
203judg! {
204    GenericInhabitable(Term): InhabitableRule {
205        fn applicable(&self, term: &Term) -> bool {
206            Pattern::r#match(term, &self.concl, &self.vars, true).is_some()
207        }
208        fn apply<'t>(&self, mut checker: CheckRef<'t, '_, Split>, term: &'t Term) -> Option<bool> {
209            let conc = Pattern::r#match(term,&self.concl,&self.vars,true)?;
210            let mut conc = self.vars.iter().cloned().zip(conc.into_iter().map(|o| o.map(Cow::into_owned))).collect::<Vec<_>>();
211            for p in &self.premises {
212                if p.check(&mut conc, &mut checker) != Some(true) { return None;}
213            }
214            if conc.iter().any(|(_,o)| o.is_none()) {None} else {
215                Some(true)
216            }
217        }
218    },
219
220    GenericUniverse(Term): UniverseRule {
221        fn applicable(&self, term: &Term) -> bool {
222            Pattern::r#match(term, &self.concl, &self.vars, true).is_some()
223        }
224        fn apply<'t>(&self, mut checker: CheckRef<'t, '_, Split>, term: &'t Term) -> Option<bool> {
225            let conc = Pattern::r#match(term,&self.concl,&self.vars,true)?;
226            let mut conc = self.vars.iter().cloned().zip(conc.into_iter().map(|o| o.map(Cow::into_owned))).collect::<Vec<_>>();
227            for p in &self.premises {
228                if p.check(&mut conc, &mut checker) != Some(true) { return None;}
229            }
230            if conc.iter().any(|(_,o)| o.is_none()) {None} else {
231                Some(true)
232            }
233        }
234    },
235
236    GenericProof(Term): ProofRule {
237        fn applicable(&self, term: &Term) -> bool {
238            Pattern::r#match(term, &self.concl, &self.vars, true).is_some()
239        }
240        fn prove<'t>(&self, mut checker: CheckRef<'t, '_, Split>, goal: &'t Term) -> Option<Term> {
241            let conc = Pattern::r#match(goal,&self.concl,&self.vars,true)?;
242            let mut conc = self.vars.iter().cloned().zip(conc.into_iter().map(|o| o.map(Cow::into_owned))).collect::<Vec<_>>();
243            for p in &self.premises {
244                if p.check(&mut conc, &mut checker) != Some(true) { return None;}
245            }
246            if conc.iter().any(|(_,o)| o.is_none()) {None} else {
247                Some(ftml_uris::metatheory::AUTO_PROVE.clone().into())
248            }
249        }
250    },
251
252    GenericBindPrep((Variable,Term) > 100_000): PreparationRule {
253        fn applicable(&self, checker: &CheckRef<'_, '_, Split>, t: &Term) -> bool {
254            let Term::Bound(b) = t else {
255                //tracing::trace!("Not bound");
256                return false;
257            };
258            let Some(head) = checker.get_head(t) else {
259                return false;
260            };
261            let spec = head.as_ref().either(|s| &s.data.arity, |v| &v.data.arity);
262            if spec.num() as usize != b.arguments.len() {
263                //tracing::trace!("Arguments don't match: {spec:?} != {:?}", b.arguments);
264                return false;
265            }
266            spec.iter()
267                .zip(b.arguments.iter())
268                .any(|(a, b)| match (a, b) {
269                    (ArgumentMode::BoundVariable, BoundArgument::Simple(t)) | (
270                        ArgumentMode::BoundVariableSequence,
271                        BoundArgument::Sequence(MaybeSequence::One(t)),
272                    ) => {
273                        Pattern::r#match(t, &self.concl.1, &self.vars, true).is_some()
274                    },
275                    (
276                        ArgumentMode::BoundVariableSequence,
277                        BoundArgument::Sequence(MaybeSequence::Seq(ts)),
278                    ) => ts.iter().any(|t| {
279                        Pattern::r#match(t, &self.concl.1, &self.vars, true).is_some()
280                    }),
281                    _ => false,
282                })
283
284        }
285        fn apply(
286            &self,
287            checker: &mut CheckRef<'_, '_, Split>,
288            t: Term,
289            path: Option<(&mut smallvec::SmallVec<u8, 16>, usize)>,
290        ) -> std::ops::ControlFlow<Term, Term> {
291            let Some(head) = checker.get_head(&t) else {
292                return std::ops::ControlFlow::Continue(t);
293            };
294            let Term::Bound(b) = t else {
295                unreachable!("wut");
296            };
297            let spec = head.as_ref().either(|s| &s.data.arity, |v| &v.data.arity);
298
299            let nargs = spec
300                .iter()
301                .zip(b.arguments.clone())
302                .map(|(m, a)| match (m, a) {
303                    (ArgumentMode::BoundVariable, BoundArgument::Simple(t)) => {
304                        if Pattern::r#match(&t, &self.concl.1, &self.vars, true).is_some() {
305                            // SAFETY: is_app
306                            let var/*(mut v, tp)*/ = unsafe { self.get_var(&t) };
307                            BoundArgument::Bound(ComponentVar {
308                                var,
309                                tp: None,//Some(tp),
310                                df: None,
311                            })
312                            /*if v.len() == 1 {
313                                // SAFETY: len==1
314                                let var = unsafe { v.pop().unwrap_unchecked() };
315                                BoundArgument::Bound(ComponentVar {
316                                    var,
317                                    tp: Some(tp),
318                                    df: None,
319                                })
320                            } else {
321                                BoundArgument::Simple(t)
322                            }*/
323                        } else {
324                            BoundArgument::Simple(t)
325                        }
326                    }
327                    (
328                        ArgumentMode::BoundVariableSequence,
329                        BoundArgument::Sequence(MaybeSequence::Seq(s)),
330                    ) => {
331                        let mut works = true;
332                        //let mut types = Vec::new();
333                        let mut ns = s
334                            .into_iter()
335                            .flat_map(|t| {
336                                if Pattern::r#match(&t, &self.concl.1, &self.vars, true).is_some() {
337                                    // SAFETY: is_app
338                                    let v = unsafe { self.get_var(&t) };
339                                    /*for _ in &v {
340                                        types.push(tp.clone());
341                                    }*/
342                                    vec![v.into()]
343                                    /*v.into_iter()
344                                        .map(|v| Term::Var {
345                                            variable: v,
346                                            presentation: None,
347                                        })
348                                        .collect::<Vec<_>>()*/
349                                } else {
350                                    works = false;
351                                    vec![t]
352                                }
353                            })
354                            .collect::<Vec<_>>();
355                        if works {
356                            BoundArgument::BoundSeq(if ns.len() == 1 && ns[0].is_sequence() {
357                                let Some(Term::Var { variable, .. }) = ns.pop() else {
358                                    // SAFETY: works == true
359                                    unsafe { unreachable_unchecked() }
360                                };
361                                MaybeSequence::One(ComponentVar {
362                                    var: variable,
363                                    tp: None,//Some(tp),
364                                    df: None,
365                                })
366                            }else {
367                            MaybeSequence::Seq(
368                                ns.into_iter()
369                                    //.zip(types)
370                                    .map(|t|{//(t, tp)| {
371                                        let Term::Var { variable, .. } = t else {
372                                            // SAFETY: works == true
373                                            unsafe { unreachable_unchecked() }
374                                        };
375                                        ComponentVar {
376                                            var: variable,
377                                            tp: None,//Some(tp),
378                                            df: None,
379                                        }
380                                    })
381                                    .collect(),
382                            )
383                            })
384                        } else {
385                            BoundArgument::Sequence(MaybeSequence::Seq(ns.into_boxed_slice()))
386                        }
387                    }
388                    (m, a) => {
389                        //tracing::trace!("Other: {m:?} = {a:?}");
390                        a
391                    }
392                })
393                .collect::<Vec<_>>()
394                .into_boxed_slice();
395            std::ops::ControlFlow::Continue(Term::Bound(BindingTerm::new(
396                b.head.clone(),
397                nargs,
398                b.presentation.clone(),
399            )))
400        }
401        fn applicable_revert(&self, _: &CheckRef<'_, '_, Split>, _: &Term) -> bool {
402            false
403        }
404        fn revert(&self, _: &CheckRef<'_, '_, Split>, t: Term) -> std::ops::ControlFlow<Term, Term> {
405            std::ops::ControlFlow::Continue(t)
406        }
407
408    },
409
410    GenericTyping((Term,Term)): CheckingRule {
411        fn applicable(&self, _: &CheckRef<'_, '_, Split>, term: &Term, tp: &Term) -> bool {
412            let (a,b) = &self.concl;
413            Pattern::r#match(term, a, &self.vars, true).is_some() &&
414            Pattern::r#match(tp, b, &self.vars, true).is_some()
415        }
416        fn apply<'t>(
417                &self,
418                mut checker: CheckRef<'t, '_, Split>,
419                term: &'t Term,
420                tp: &'t Term,
421        ) -> Option<bool> {
422            let (a,b) = &self.concl;
423            let mut vars: Vec<Option<Cow<'t, _>>> = vec![None; self.vars.len()];
424            Pattern::match_i(term,a,&self.vars,true,&mut vars,&mut Alpha::new())?;
425            Pattern::match_i(tp,b,&self.vars,true,&mut vars,&mut Alpha::new())?;
426            let mut conc = self.vars.iter().cloned().zip(vars.into_iter().map(|o| o.map(Cow::into_owned))).collect::<Vec<_>>();
427            for p in &self.premises {
428                if p.check(&mut conc, &mut checker) != Some(true) { return None;}
429            }
430            if conc.iter().any(|(_,o)| o.is_none()) {None} else {
431                Some(true)
432            }
433        }
434    },
435    GenericSubtyping((Term,Term)): SubtypeRule {
436        fn applicable(&self, _: &CheckRef<'_, '_, Split>, sub: &Term, sup: &Term) -> bool {
437            let (a,b) = &self.concl;
438            Pattern::r#match(sub, a, &self.vars, true).is_some() &&
439            Pattern::r#match(sup, b, &self.vars, true).is_some()
440        }
441        fn apply<'t>(
442            &self,
443            mut checker: CheckRef<'t, '_, Split>,
444            sub: &'t Term,
445            sup: &'t Term,
446        ) -> Option<bool> {
447            let (a,b) = &self.concl;
448            let mut vars: Vec<Option<Cow<'t, _>>> = vec![None; self.vars.len()];
449            Pattern::match_i(sub,a,&self.vars,true,&mut vars,&mut Alpha::new())?;
450            Pattern::match_i(sup,b,&self.vars,true,&mut vars,&mut Alpha::new())?;
451            let mut conc = self.vars.iter().cloned().zip(vars.into_iter().map(|o| o.map(Cow::into_owned))).collect::<Vec<_>>();
452            for p in &self.premises {
453                if p.check(&mut conc, &mut checker) != Some(true) { return None;}
454            }
455            if conc.iter().any(|(_,o)| o.is_none()) {None} else {
456                Some(true)
457            }
458        }
459    },
460
461    GenericEquality((Term,Term)): EqualityRule {
462        fn applicable(&self, lhs: &Term, rhs: &Term) -> bool {
463            let (a,b) = &self.concl;
464            Pattern::r#match(lhs, a, &self.vars, true).is_some() &&
465            Pattern::r#match(rhs, b, &self.vars, true).is_some()
466        }
467        fn apply<'t>(
468            &self,
469            mut checker: CheckRef<'t, '_, Split>,
470            lhs: &'t Term,
471            rhs: &'t Term,
472        ) -> Option<bool> {
473            let (a,b) = &self.concl;
474            let mut vars: Vec<Option<Cow<'t, _>>> = vec![None; self.vars.len()];
475            Pattern::match_i(lhs,a,&self.vars,true,&mut vars,&mut Alpha::new())?;
476            Pattern::match_i(rhs,b,&self.vars,true,&mut vars,&mut Alpha::new())?;
477            let mut conc = self.vars.iter().cloned().zip(vars.into_iter().map(|o| o.map(Cow::into_owned))).collect::<Vec<_>>();
478            for p in &self.premises {
479                if p.check(&mut conc, &mut checker) != Some(true) { return None;}
480            }
481            if conc.iter().any(|(_,o)| o.is_none()) {None} else {
482                Some(true)
483            }
484        }
485    },
486
487    GenericSimplification((Term,Term)): SimplificationRule {
488        fn applicable(&self, term: &Term) -> bool {
489            Pattern::r#match(term, &self.concl.0, &self.vars, true).is_some()
490        }
491        fn apply<'t>(
492            &self,
493            mut checker: CheckRef<'t, '_, Split>,
494            term: &'t Term,
495        ) -> Result<Term, Option<ftml_ontology::terms::termpaths::TermPath>> {
496            let (a,b) = &self.concl;
497            let mut vars: Vec<Option<Cow<'t, _>>> = vec![None; self.vars.len()];
498            Pattern::match_i(term,a,&self.vars,true,&mut vars,&mut Alpha::new()).ok_or(None)?;
499            //Pattern::match_i(rhs,b,&self.vars,true,&mut vars,&mut Alpha::new()).ok_or(None)?;
500            let mut conc = self.vars.iter().cloned().zip(vars.into_iter().map(|o| o.map(Cow::into_owned))).collect::<Vec<_>>();
501            for p in &self.premises {
502                if p.check(&mut conc, &mut checker) != Some(true) { return Err(None);}
503            }
504            if conc.iter().any(|(v,o)| !is_solvable_id(v) && o.is_none()) {return Err(None)}
505            let subst = conc.iter().filter_map(|(v,o)| if is_solvable_id(v) && o.is_none() {
506                Some((v.as_ref(),Cow::Owned(checker.new_solvable())))
507            } else {o.as_ref().map(|t| (v.as_ref(),Cow::Borrowed(t)))}).collect::<Vec<_>>();
508            Ok(b.clone() / subst.as_slice())
509        }
510    },
511}
512
513impl GenericBindPrep {
514    /// Only safe to call iff `self.is_app(&t)`
515    unsafe fn get_var(&self, t: &Term) -> Variable {
516        let Some(mut matches) = Pattern::r#match(t, &self.concl.1, &self.vars, true) else {
517            unreachable!("bug!");
518        };
519        self.vars
520            .iter()
521            .position(|v| v.as_ref() == self.concl.0.name())
522            .map_or_else(
523                || self.concl.0.clone(),
524                |i| {
525                    if let Some(Term::Var { variable, .. }) = matches.remove(i).map(Cow::into_owned)
526                    {
527                        variable
528                    } else {
529                        self.concl.0.clone()
530                    }
531                },
532            )
533    }
534}
535
536#[derive(Clone, Debug, PartialEq, Eq)]
537pub enum Premise {
538    Inhabitable(Term),
539    Universe(Term),
540    HasProof(Term),
541    HasType(Term, Term),
542    Subtype(Term, Term),
543    Equal(Term, Term),
544}
545impl Premise {
546    fn parse(t: &Term, vars: &mut Vec<Id>) -> Option<Self> {
547        let Term::Application(p) = t else { return None };
548        if let [Argument::Simple(t)] = &*p.arguments {
549            if p.head.is(&*INH) {
550                Pattern::from_with_vars(t, true, vars);
551                Some(Self::Inhabitable(t.clone()))
552            } else if p.head.is(&*UNIV) {
553                Pattern::from_with_vars(t, true, vars);
554                Some(Self::Universe(t.clone()))
555            } else if p.head.is(&*HAS_PROOF) {
556                Pattern::from_with_vars(t, true, vars);
557                Some(Self::HasProof(t.clone()))
558            } else {
559                None
560            }
561        } else if let [Argument::Simple(a), Argument::Simple(b)] = &*p.arguments {
562            if p.head.is(&*HAS_TYPE) {
563                Pattern::from_with_vars(a, true, vars);
564                Pattern::from_with_vars(b, true, vars);
565                Some(Self::HasType(a.clone(), b.clone()))
566            } else if p.head.is(&*SUBTYPE) {
567                Pattern::from_with_vars(a, true, vars);
568                Pattern::from_with_vars(b, true, vars);
569                Some(Self::Subtype(a.clone(), b.clone()))
570            } else if p.head.is(&*EQUAL) {
571                Pattern::from_with_vars(a, true, vars);
572                Pattern::from_with_vars(b, true, vars);
573                Some(Self::Equal(a.clone(), b.clone()))
574            } else {
575                None
576            }
577        } else {
578            None
579        }
580    }
581    pub fn check<Split: SplitStrategy>(
582        &self,
583        context: &mut [(Id, Option<Term>)],
584        checker: &mut CheckRef<'_, '_, Split>,
585    ) -> Option<bool> {
586        macro_rules! check {
587            ($c:ident.$f:ident($($t:ident),+) ) => {{
588                let subst = context.iter().filter_map(|(id,o)| o.as_ref().map(|t| (id.as_ref(),t))).collect::<Vec<_>>();
589                $(
590                    let $t = $t / subst.as_slice();
591                )*
592                checker.scoped(|$c| $c.$f($(&$t),*))
593            }}
594        }
595        match self {
596            Self::Inhabitable(t) => check!(c.check_inhabitable(t)),
597            Self::Universe(t) => check!(c.check_universe(t)),
598            Self::HasProof(t) => check!(c.prove(t)).map(|_| true),
599            Self::Subtype(a, b) => check!(c.check_subtype(a, b)),
600            Self::Equal(a, b) => check!(c.check_equality(a, b)),
601            Self::HasType(a, b) => {
602                if let Term::Var {
603                    variable: Variable::Name { name, .. },
604                    ..
605                } = b
606                    && context.iter().any(|(p, o)| p == name && o.is_none())
607                {
608                    let nt = check!(c.infer_type(a))?;
609                    context.iter_mut().find(|(a, _)| *a == *name)?.1 = Some(nt);
610                    Some(true)
611                } else {
612                    check!(c.check_type(a, b))
613                }
614            }
615        }
616    }
617}
ftml_solver/rules/symbols.rs

ftml_solver/rules/
symbols.rs
