ftml_solver/rules/operators/
typing.rs

1use crate::{
2    CheckRef,
3    rules::{PreparationRule, SimplificationRule, SizedSolverRule, SubtypeRule},
4    split::SplitStrategy,
5};
6use ftml_ontology::terms::{
7    Argument, ArgumentMode, BindingTerm, BoundArgument, ComponentVar, IsTerm, MaybeSequence, Term,
8    Variable, patterns::Pattern,
9};
10use ftml_uris::SymbolUri;
11use std::{hint::unreachable_unchecked, ops::ControlFlow};
12
13#[derive(Debug, Clone, PartialEq, Eq)]
14pub struct SimpleTypeOperatorRule(pub SymbolUri);
15
16impl SizedSolverRule for SimpleTypeOperatorRule {
17    fn priority(&self) -> isize {
18        100_000
19    }
20    fn display(&self) -> Vec<crate::trace::Displayable> {
21        ftml_solver_trace::trace!(&self.0, " is a typing operator")
22    }
23}
24
25impl SimpleTypeOperatorRule {
26    fn is_app(&self, t: &Term) -> bool {
27        //ftml_ontology::matchtm!(app({sym(=self.0)},[]) = t);
28        matches!(
29            t,
30            Term::Application(app)
31            if matches!(
32                &app.head,
33                Term::Symbol{uri,..} if *uri == self.0
34            ) && (matches!(
35                app.arguments.first(),
36                Some(Argument::Simple(Term::Var{..}))
37            ) || matches!(
38                app.arguments.first(),
39                Some(Argument::Sequence(MaybeSequence::Seq(s)))
40                if s.iter().all(|t| matches!(t,Term::Var{..}))
41            )) && matches!(app.arguments.get(1),Some(Argument::Simple(_)))
42        )
43    }
44    /// Only safe to call iff `self.is_app(&t)`
45    unsafe fn get_var(t: &Term) -> (Vec<Variable>, Term) {
46        let Term::Application(a) = t else {
47            unsafe { unreachable_unchecked() }
48        };
49        let Argument::Simple(tp) = a.arguments[1].clone() else {
50            unsafe { unreachable_unchecked() }
51        };
52        (
53            match a.arguments[0].clone() {
54                Argument::Simple(Term::Var { variable, .. }) => vec![variable],
55                Argument::Sequence(MaybeSequence::Seq(vars)) => vars
56                    .into_iter()
57                    .map(|v| {
58                        let Term::Var { variable, .. } = v else {
59                            unsafe { unreachable_unchecked() }
60                        };
61                        variable
62                    })
63                    .collect(),
64                _ => unsafe { unreachable_unchecked() },
65            },
66            tp,
67        )
68    }
69}
70impl<Split: SplitStrategy> PreparationRule<Split> for SimpleTypeOperatorRule {
71    fn applicable(&self, checker: &crate::CheckRef<'_, '_, Split>, t: &Term) -> bool {
72        let Term::Bound(b) = t else {
73            //tracing::trace!("Not bound");
74            return false;
75        };
76        let Some(head) = checker.get_head(t) else {
77            return false;
78        };
79        let spec = head.as_ref().either(|s| &s.data.arity, |v| &v.data.arity);
80        if spec.num() as usize != b.arguments.len() {
81            //tracing::trace!("Arguments don't match: {spec:?} != {:?}", b.arguments);
82            return false;
83        }
84        spec.iter()
85            .zip(b.arguments.iter())
86            .any(|(a, b)| match (a, b) {
87                (ArgumentMode::BoundVariable, BoundArgument::Simple(t)) => t
88                    .head()
89                    .is_some_and(|v| matches!(v,either::Left(uri) if *uri == self.0)),
90                (
91                    ArgumentMode::BoundVariableSequence,
92                    BoundArgument::Sequence(MaybeSequence::One(t)),
93                ) => t
94                    .head()
95                    .is_some_and(|v| matches!(v,either::Left(uri) if *uri == self.0)),
96                (
97                    ArgumentMode::BoundVariableSequence,
98                    BoundArgument::Sequence(MaybeSequence::Seq(ts)),
99                ) => ts.iter().any(|t| {
100                    t.head()
101                        .is_some_and(|v| matches!(v,either::Left(uri) if *uri == self.0))
102                }),
103                _ => false,
104            })
105    }
106    fn apply(
107        &self,
108        checker: &mut CheckRef<'_, '_, Split>,
109        t: Term,
110        _: Option<(&mut smallvec::SmallVec<u8, 16>, usize)>,
111    ) -> ControlFlow<Term, Term> {
112        let Some(head) = checker.get_head(&t) else {
113            return ControlFlow::Continue(t);
114        };
115        let Term::Bound(b) = t else {
116            unreachable!("wut");
117        };
118        let spec = head.as_ref().either(|s| &s.data.arity, |v| &v.data.arity);
119
120        let nargs = spec
121            .iter()
122            .zip(b.arguments.clone())
123            .map(|(m, a)| match (m, a) {
124                (ArgumentMode::BoundVariable, BoundArgument::Simple(t)) => {
125                    if self.is_app(&t) {
126                        // SAFETY: is_app
127                        let (mut v, tp) = unsafe { Self::get_var(&t) };
128                        if v.len() == 1 {
129                            // SAFETY: len==1
130                            let var = unsafe { v.pop().unwrap_unchecked() };
131                            BoundArgument::Bound(ComponentVar {
132                                var,
133                                tp: Some(tp),
134                                df: None,
135                            })
136                        } else {
137                            BoundArgument::Simple(t)
138                        }
139                    } else {
140                        BoundArgument::Simple(t)
141                    }
142                }
143                (
144                    ArgumentMode::BoundVariableSequence,
145                    BoundArgument::Sequence(MaybeSequence::Seq(s)),
146                ) => {
147                    let mut works = true;
148                    let mut types = Vec::new();
149                    let ns = s
150                        .into_iter()
151                        .flat_map(|t| {
152                            if self.is_app(&t) {
153                                // SAFETY: is_app
154                                let (v, tp) = unsafe { Self::get_var(&t) };
155                                for _ in &v {
156                                    types.push(tp.clone());
157                                }
158                                v.into_iter()
159                                    .map(|v| Term::Var {
160                                        variable: v,
161                                        presentation: None,
162                                    })
163                                    .collect::<Vec<_>>()
164                            } else {
165                                works = false;
166                                vec![t]
167                            }
168                        })
169                        .collect::<Vec<_>>();
170                    if works {
171                        BoundArgument::BoundSeq(MaybeSequence::Seq(
172                            ns.into_iter()
173                                .zip(types)
174                                .map(|(t, tp)| {
175                                    let Term::Var { variable, .. } = t else {
176                                        // SAFETY: works == true
177                                        unsafe { unreachable_unchecked() }
178                                    };
179                                    ComponentVar {
180                                        var: variable,
181                                        tp: Some(tp),
182                                        df: None,
183                                    }
184                                })
185                                .collect(),
186                        ))
187                    } else {
188                        BoundArgument::Sequence(MaybeSequence::Seq(ns.into_boxed_slice()))
189                    }
190                }
191                (m, a) => {
192                    //tracing::trace!("Other: {m:?} = {a:?}");
193                    a
194                }
195            })
196            .collect::<Vec<_>>()
197            .into_boxed_slice();
198        ControlFlow::Continue(Term::Bound(BindingTerm::new(
199            b.head.clone(),
200            nargs,
201            b.presentation.clone(),
202        )))
203    }
204    fn applicable_revert(&self, _: &CheckRef<'_, '_, Split>, _: &Term) -> bool {
205        false
206    }
207    fn revert(&self, _: &CheckRef<'_, '_, Split>, t: Term) -> ControlFlow<Term, Term> {
208        ControlFlow::Continue(t)
209    }
210}
211
212#[derive(Debug, Clone, PartialEq, Eq)]
213pub struct Subtyping {
214    pub sub: Pattern,
215    pub sup: Pattern,
216}
217impl SizedSolverRule for Subtyping {
218    fn display(&self) -> Vec<crate::trace::Displayable> {
219        ftml_solver_trace::trace!(
220            self.sub.body.clone(),
221            "is a subtype of",
222            self.sup.body.clone()
223        )
224    }
225}
226impl<Split: SplitStrategy> SubtypeRule<Split> for Subtyping {
227    fn applicable(&self, checker: &CheckRef<'_, '_, Split>, sub: &Term, sup: &Term) -> bool {
228        /*println!(
229            "Applicable? ({:?}   <:   {:?})\n {:?}   <:   {:?}",
230            self.sub.body.debug_short(),
231            self.sup.body.debug_short(),
232            sub.debug_short(),
233            sup.debug_short()
234        );*/
235        let Some(sub) = self.sub.matches(sub) else {
236            return false;
237        };
238        let Some(sup) = self.sup.matches(sup) else {
239            return false;
240        };
241        for (i, j) in self
242            .sub
243            .vars
244            .iter()
245            .enumerate()
246            .filter_map(|(i, v)| Some((i, self.sup.vars.iter().position(|v2| v2 == v)?)))
247        {
248            let Some(sub) = sub.get(i) else { return false };
249            let Some(sup) = sup.get(j) else { return false };
250            if !sub.alpha_equal(sup) {
251                return false;
252            }
253        }
254        //println!("Applicable!");
255        true
256    }
257    fn apply<'t>(
258        &self,
259        mut checker: CheckRef<'t, '_, Split>,
260        sub: &'t Term,
261        sup: &'t Term,
262    ) -> Option<bool> {
263        // sanity check
264        checker.check_inhabitable(sub)?;
265        checker.check_inhabitable(sup)?;
266        Some(true)
267    }
268}
269
270#[derive(Debug, Clone, Copy, PartialEq, Eq)]
271pub struct InferredTypeSimplificationRule;
272
273impl SizedSolverRule for InferredTypeSimplificationRule {
274    fn display(&self) -> Vec<crate::trace::Displayable> {
275        ftml_solver_trace::trace!(&*ftml_uris::metatheory::TYPE_OF, " infers type")
276    }
277}
278impl<Split: SplitStrategy> SimplificationRule<Split> for InferredTypeSimplificationRule {
279    fn applicable(&self, term: &Term) -> bool {
280        if let Term::Application(app) = term
281            && app.head.is(&*ftml_uris::metatheory::TYPE_OF)
282            && let [Argument::Simple(_)] = &*app.arguments
283        {
284            true
285        } else {
286            false
287        }
288    }
289    fn apply<'t>(
290        &self,
291        mut checker: CheckRef<'t, '_, Split>,
292        term: &'t Term,
293    ) -> Result<Term, Option<ftml_ontology::terms::termpaths::TermPath>> {
294        let Term::Application(app) = term else {
295            return Err(None);
296        };
297        let [Argument::Simple(t)] = &*app.arguments else {
298            return Err(None);
299        };
300        checker.infer_type(t).ok_or(None)
301    }
302}
ftml_solver/rules/operators/typing.rs

ftml_solver/rules/operators/
typing.rs
