ftml_solver/rules/
implicits.rs

1use std::borrow::Cow;
2
3use ftml_ontology::terms::{
4    ApplicationTerm, Argument, BindingTerm, BoundArgument, ComponentVar, MaybeSequence, Term,
5    Variable,
6};
7use ftml_solver_trace::SizedSolverRule;
8use ftml_uris::{Id, SymbolUri};
9use smallvec::SmallVec;
10
11use crate::{
12    Checker,
13    rules::{EqualityRule, InferenceRule, SimplificationRule},
14    split::SplitStrategy,
15};
16
17pub trait ImplicitExtBound {
18    fn get_bound_implicits(&self) -> Option<(&Term, &[ComponentVar])>;
19}
20pub trait ImplicitExtApp: Sized {
21    fn unapply_implicits(&self, in_prepare_revert: bool) -> Option<(&Term, &[Term])>;
22}
23pub trait ImplicitExtTerm: ImplicitExtBound + ImplicitExtApp {
24    fn apply_implicits(self, num: usize, new: impl FnMut(usize) -> Term) -> Self;
25}
26impl ImplicitExtApp for ApplicationTerm {
27    // invariant: return.0 matches Term::Symbol {..} or Term::Field(_)
28    fn unapply_implicits(&self, in_prepare_revert: bool) -> Option<(&Term, &[Term])> {
29        if !self.head.is(&*ftml_uris::metatheory::APPLY_IMPLICIT) {
30            return None;
31        }
32        if let [
33            Argument::Simple(t @ (Term::Symbol { .. } | Term::Field(_))),
34            Argument::Sequence(MaybeSequence::Seq(bound)),
35        ] = &*self.arguments
36        {
37            Some((t, bound))
38        } else if in_prepare_revert {
39            None
40        } else {
41            //panic!("WWWWEEEEIIIIRRRD: {:#?}", self.arguments);
42            None
43        }
44    }
45}
46impl ImplicitExtBound for BindingTerm {
47    fn get_bound_implicits(&self) -> Option<(&Term, &[ComponentVar])> {
48        if !self.head.is(&*ftml_uris::metatheory::IMPLICIT_BIND) {
49            return None;
50        }
51        if let [
52            BoundArgument::BoundSeq(MaybeSequence::Seq(impls)),
53            BoundArgument::Simple(body),
54        ] = &*self.arguments
55        {
56            Some((body, impls))
57        } else {
58            None
59        }
60    }
61}
62impl ImplicitExtBound for Term {
63    fn get_bound_implicits(&self) -> Option<(&Term, &[ComponentVar])> {
64        if let Self::Bound(b) = self {
65            b.get_bound_implicits()
66        } else {
67            None
68        }
69    }
70}
71impl ImplicitExtApp for Term {
72    fn unapply_implicits(&self, in_prepare_revert: bool) -> Option<(&Term, &[Term])> {
73        if let Self::Application(app) = self {
74            app.unapply_implicits(in_prepare_revert)
75        } else {
76            None
77        }
78    }
79}
80impl ImplicitExtTerm for Term {
81    fn apply_implicits(self, num: usize, mut new: impl FnMut(usize) -> Self) -> Self {
82        if num == 0 {
83            return self;
84        }
85        let mut index = 0;
86        Self::Application(ApplicationTerm::new(
87            (*ftml_uris::metatheory::APPLY_IMPLICIT).clone().into(),
88            Box::new([
89                Argument::Simple(self),
90                Argument::Sequence(MaybeSequence::Seq(
91                    (0..num)
92                        .map(|_| {
93                            let r = new(index);
94                            index += 1;
95                            r
96                        })
97                        .collect(),
98                )),
99            ]),
100            None,
101        ))
102    }
103}
104
105#[derive(Debug, Copy, Clone, PartialEq, Eq)]
106pub struct ImplicitRule;
107impl SizedSolverRule for ImplicitRule {
108    fn display(&self) -> Vec<crate::trace::Displayable> {
109        ftml_solver_trace::trace!("implicit arguments")
110    }
111    fn priority(&self) -> isize {
112        100_000
113    }
114}
115/*
116impl<Split: SplitStrategy> SimplificationRule<Split> for ImplicitRule {
117    fn applicable(&self, term: &Term) -> bool {
118        if let Term::Application(app) = term
119            && let Some((bd, vars)) = app.head.get_bound_implicits()
120        {
121            app.arguments.len() == vars.len()
122        } else {
123            false
124        }
125    }
126}
127 */
128impl<Split: SplitStrategy> InferenceRule<Split> for ImplicitRule {
129    fn applicable(&self, term: &Term) -> bool {
130        term.unapply_implicits(false).is_some()
131    }
132    fn infer<'t>(
133        &self,
134        mut checker: crate::CheckRef<'t, '_, Split>,
135        term: &'t Term,
136    ) -> Option<Term> {
137        let (body, args) = term.unapply_implicits(false)?;
138        let btp = checker.infer_type(body)?;
139        let (tpbody, bounds) = btp.get_bound_implicits()?;
140        if bounds.len() != args.len() {
141            return None;
142        }
143        let mut substs = Vec::new();
144        for (ComponentVar { var, tp, .. }, arg) in bounds.iter().zip(args) {
145            if let Some(tp) = tp {
146                let tp: Cow<Term> = tp / &*substs;
147                if checker.scoped(|checker| checker.check_type(arg, &tp)) != Some(true) {
148                    return None;
149                }
150                substs.push((var.name(), arg));
151            }
152        }
153        Some((tpbody / &*substs).into_owned())
154    }
155}
156
157impl<Split: SplitStrategy> Checker<Split> {
158    pub(crate) fn bind_implicits(&self, nt: &Term) -> Option<Term> {
159        self.collect_implicits(nt).map(|(cvs, t)| {
160            if cvs.is_empty() {
161                t
162            } else {
163                Term::Bound(BindingTerm::new(
164                    ftml_uris::metatheory::IMPLICIT_BIND.clone().into(),
165                    Box::new([
166                        BoundArgument::BoundSeq(MaybeSequence::Seq(cvs.into_boxed_slice())),
167                        BoundArgument::Simple(t),
168                    ]),
169                    None,
170                ))
171            }
172        })
173    }
174    fn collect_implicits(&self, nt: &Term) -> Option<(Vec<ComponentVar>, Term)> {
175        fn new_name(i: usize) -> Id {
176            // SAFETY: valid ID
177            unsafe { format!("IMPL_{i}").parse().unwrap_unchecked() }
178        }
179        tracing::trace!("Collecting implicits for {:?}", nt.debug_short());
180        let mut allvars = nt
181            .free_variables()
182            .into_iter()
183            .cloned()
184            .collect::<SmallVec<_, 4>>();
185        if allvars.is_empty() {
186            return None;
187        }
188
189        let mut curr_idx = 0;
190        while curr_idx < allvars.len() {
191            if let Variable::Ref { declaration, .. } = &allvars[curr_idx]
192                && let Ok(v) = self.get_variable(declaration)
193                && let Some((tp, _)) = v.data.tp.checked_or_parsed()
194            {
195                let vars = tp.free_variables();
196                let mut changed = false;
197                for v in vars {
198                    if !allvars[..curr_idx].contains(v) {
199                        allvars.insert(curr_idx, v.clone());
200                        changed = true;
201                    }
202                }
203                if changed {
204                    continue;
205                }
206            }
207            curr_idx += 1;
208        }
209        tracing::trace!("All variables: {allvars:?}");
210
211        //let mut counter = 1;
212
213        let mut subst = smallvec::SmallVec::<(&str, Term), 4>::new();
214        let mut dones = smallvec::SmallVec::<&str, 4>::new();
215        let mut ret = Vec::new();
216        for v in &allvars {
217            if !dones.iter().any(|var| *var == v.name()) {
218                //let name = new_name(counter);
219                //counter += 1;
220
221                let tp = if let Variable::Ref { declaration, .. } = v {
222                    let var = self.get_variable(declaration).ok();
223                    if let Some(df) = var
224                        .as_ref()
225                        .and_then(|v| v.data.df.checked_or_parsed().map(|t| t.0 / &*subst))
226                    {
227                        subst.push((v.name(), df));
228                        continue;
229                    }
230                    var.and_then(|v| v.data.tp.checked_or_parsed().map(|t| t.0 / &*subst))
231                } else {
232                    None
233                };
234
235                dones.push(v.name());
236                //subst.push((v.name(), name.clone().into()));
237                ret.push(ComponentVar {
238                    var: v.name_id().into_owned().into(), //name.into(),
239                    df: None,
240                    tp,
241                });
242            }
243        }
244        let n = nt / &*subst;
245        tracing::trace!("Implicitified: {:?}", n.debug_short());
246        Some((ret, n.into_owned()))
247    }
248}
ftml_solver/rules/implicits.rs

ftml_solver/rules/
implicits.rs
