ftml_solver/rules/operators/
typing.rs

1use crate::{
2    CheckRef,
3    rules::{InferenceRule, 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
212impl<Split: SplitStrategy> SimplificationRule<Split> for SimpleTypeOperatorRule {
213    fn applicable(&self, term: &Term) -> bool {
214        <Self as InferenceRule<Split>>::applicable(&self, term)
215    }
216    fn apply<'t>(
217        &self,
218        mut checker: CheckRef<'t, '_, Split>,
219        term: &'t Term,
220    ) -> Result<Term, Option<ftml_ontology::terms::termpaths::TermPath>> {
221        let Term::Application(app) = term else {
222            return Err(None);
223        };
224        let Term::Symbol { uri, .. } = &app.head else {
225            return Err(None);
226        };
227        if *uri != self.0 {
228            return Err(None);
229        }
230        let (tm, tp) = match &*app.arguments {
231            [Argument::Simple(tm), Argument::Simple(tp)] => (tm, tp),
232            [
233                Argument::Sequence(MaybeSequence::Seq(tms)),
234                Argument::Simple(tp),
235            ] => match &**tms {
236                [tm] => (tm, tp),
237                _ => return Err(None),
238            },
239            _ => return Err(None),
240        };
241        if checker.check_type(tm, tp) != Some(true) {
242            return Err(None);
243        }
244        Ok(tm.clone())
245    }
246}
247
248impl<Split: SplitStrategy> InferenceRule<Split> for SimpleTypeOperatorRule {
249    fn applicable(&self, term: &Term) -> bool {
250        if let Term::Application(app) = term
251            && let Term::Symbol { uri, .. } = &app.head
252            && *uri == self.0
253        {
254            matches!(&*app.arguments, [Argument::Simple(_), Argument::Simple(_)])
255                || matches!(&*app.arguments,[Argument::Sequence(MaybeSequence::Seq(v)),Argument::Simple(_)] if v.len() == 1)
256        } else {
257            false
258        }
259    }
260    fn infer<'t>(&self, mut checker: CheckRef<'t, '_, Split>, term: &'t Term) -> Option<Term> {
261        let Term::Application(app) = term else {
262            return None;
263        };
264        let Term::Symbol { uri, .. } = &app.head else {
265            return None;
266        };
267        if *uri != self.0 {
268            return None;
269        }
270        let (tm, tp) = match &*app.arguments {
271            [Argument::Simple(tm), Argument::Simple(tp)] => (tm, tp),
272            [
273                Argument::Sequence(MaybeSequence::Seq(tms)),
274                Argument::Simple(tp),
275            ] => match &**tms {
276                [tm] => (tm, tp),
277                _ => return None,
278            },
279            _ => return None,
280        };
281        if checker.check_type(tm, tp) != Some(true) {
282            return None;
283        }
284        Some(tp.clone())
285    }
286}
287
288#[derive(Debug, Clone, PartialEq, Eq)]
289pub struct Subtyping {
290    pub sub: Pattern,
291    pub sup: Pattern,
292}
293impl SizedSolverRule for Subtyping {
294    fn display(&self) -> Vec<crate::trace::Displayable> {
295        ftml_solver_trace::trace!(
296            self.sub.body.clone(),
297            "is a subtype of",
298            self.sup.body.clone()
299        )
300    }
301}
302impl<Split: SplitStrategy> SubtypeRule<Split> for Subtyping {
303    fn applicable(&self, checker: &CheckRef<'_, '_, Split>, sub: &Term, sup: &Term) -> bool {
304        /*println!(
305            "Applicable? ({:?}   <:   {:?})\n {:?}   <:   {:?}",
306            self.sub.body.debug_short(),
307            self.sup.body.debug_short(),
308            sub.debug_short(),
309            sup.debug_short()
310        );*/
311        let Some(sub) = self.sub.matches(sub) else {
312            return false;
313        };
314        let Some(sup) = self.sup.matches(sup) else {
315            return false;
316        };
317        for (i, j) in self
318            .sub
319            .vars
320            .iter()
321            .enumerate()
322            .filter_map(|(i, v)| Some((i, self.sup.vars.iter().position(|v2| v2 == v)?)))
323        {
324            let Some(sub) = sub.get(i) else { return false };
325            let Some(sup) = sup.get(j) else { return false };
326            if !sub.alpha_equal(sup) {
327                return false;
328            }
329        }
330        //println!("Applicable!");
331        true
332    }
333    fn apply<'t>(
334        &self,
335        mut checker: CheckRef<'t, '_, Split>,
336        sub: &'t Term,
337        sup: &'t Term,
338    ) -> Option<bool> {
339        // sanity check
340        checker.check_inhabitable(sub)?;
341        checker.check_inhabitable(sup)?;
342        Some(true)
343    }
344}
345
346#[derive(Debug, Clone, Copy, PartialEq, Eq)]
347pub struct InferredTypeSimplificationRule;
348
349impl SizedSolverRule for InferredTypeSimplificationRule {
350    fn display(&self) -> Vec<crate::trace::Displayable> {
351        ftml_solver_trace::trace!(&*ftml_uris::metatheory::TYPE_OF, " infers type")
352    }
353}
354impl<Split: SplitStrategy> SimplificationRule<Split> for InferredTypeSimplificationRule {
355    fn applicable(&self, term: &Term) -> bool {
356        if let Term::Application(app) = term
357            && app.head.is(&*ftml_uris::metatheory::TYPE_OF)
358            && let [Argument::Simple(_)] = &*app.arguments
359        {
360            true
361        } else {
362            false
363        }
364    }
365    fn apply<'t>(
366        &self,
367        mut checker: CheckRef<'t, '_, Split>,
368        term: &'t Term,
369    ) -> Result<Term, Option<ftml_ontology::terms::termpaths::TermPath>> {
370        let Term::Application(app) = term else {
371            return Err(None);
372        };
373        let [Argument::Simple(t)] = &*app.arguments else {
374            return Err(None);
375        };
376        checker.infer_type(t).ok_or(None)
377    }
378}
ftml_solver/rules/operators/typing.rs

ftml_solver/rules/operators/
typing.rs
