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

ftml_solver/rules/
implicits.rs
