ftml_solver/impls/
solving.rs

1use std::borrow::{Borrow, Cow};
2
3use ftml_ontology::terms::{
4    ApplicationTerm, Argument, BindingTerm, BoundArgument, ComponentVar, MaybeSequence, Term,
5    Variable,
6};
7use ftml_uris::Id;
8use smallvec::SmallVec;
9
10use crate::{
11    CheckRef, Checker,
12    rules::unknowns::beta_unknowns,
13    split::SplitStrategy,
14    utils::{Merge, MutableRefList},
15};
16
17const PREFIX: &str = "SOLVE!";
18
19pub trait TermExtSolvable {
20    fn is_solvable(&self) -> Option<&Id>;
21    fn has_solvable(&self) -> bool;
22    fn solvables(&self) -> SmallVec<&Variable, 2>;
23}
24
25/*
26impl TermExtSolvable for Variable {
27    fn is_solvable(&self) -> Option<&Id> {
28        let Self::Name { name, .. } = self else {
29            return None;
30        };
31        if name.as_ref().starts_with(PREFIX)
32            && name.as_ref().as_bytes()[PREFIX.len()..]
33                .iter()
34                .all(u8::is_ascii_digit)
35        {
36            Some(name)
37        } else {
38            None
39        }
40    }
41    #[inline]
42    fn has_solvable(&self) -> bool {
43        self.is_solvable().is_some()
44    }
45}
46 */
47
48pub fn is_solvable_id(name: &Id) -> bool {
49    name.as_ref().starts_with(PREFIX)
50        && name.as_ref().as_bytes()[PREFIX.len()..]
51            .iter()
52            .all(u8::is_ascii_digit)
53}
54
55pub fn is_solvable_var(var: &Variable) -> Option<&Id> {
56    let Variable::Name { name, .. } = var else {
57        return None;
58    };
59    if is_solvable_id(name) {
60        Some(name)
61    } else {
62        None
63    }
64}
65
66impl TermExtSolvable for Term {
67    fn is_solvable(&self) -> Option<&Id> {
68        if let Self::Var { variable, .. } = self {
69            is_solvable_var(variable)
70        } else if let Self::Application(app) = self
71            && let Self::Var { variable, .. } = &app.head
72        {
73            is_solvable_var(variable)
74        } else {
75            None
76        }
77    }
78    fn has_solvable(&self) -> bool {
79        self.has_free_such_that(|v| is_solvable_var(v).is_some())
80    }
81    fn solvables(&self) -> SmallVec<&Variable, 2> {
82        self.free_variables()
83            .into_iter()
84            .filter(|s| is_solvable_var(s).is_some())
85            .collect()
86    }
87}
88
89#[derive(Clone)]
90pub enum BoundedValue {
91    None,
92    Solved(Term),
93    Bounded(Option<Term>, Option<Term>),
94}
95impl std::fmt::Debug for BoundedValue {
96    fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result {
97        match self {
98            Self::None => f.write_str("(None)"),
99            Self::Solved(t) => t.debug_short().fmt(f),
100            Self::Bounded(a, b) => write!(
101                f,
102                "({:?} <= _ <= {:?})",
103                a.as_ref().map(Term::debug_short),
104                b.as_ref().map(Term::debug_short)
105            ),
106        }
107    }
108}
109
110#[derive(Clone)]
111pub struct Solvable {
112    pub(crate) name: Id,
113    solution: BoundedValue,
114    context: Vec<ComponentVar>,
115    tp: BoundedValue,
116}
117impl Solvable {
118    pub(crate) fn new(name: Id, context: impl Iterator<Item = ComponentVar>) -> Self {
119        Self {
120            name,
121            solution: BoundedValue::None,
122            tp: BoundedValue::None,
123            context: context.collect(),
124        }
125    }
126
127    pub const fn solution(&self) -> Option<&Term> {
128        if let BoundedValue::Solved(t) = &self.solution {
129            Some(t)
130        } else {
131            None
132        }
133    }
134}
135impl std::fmt::Debug for Solvable {
136    fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result {
137        struct CtxWrap<'i>(&'i [ComponentVar]);
138        impl std::fmt::Debug for CtxWrap<'_> {
139            fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result {
140                let mut first = true;
141                for ComponentVar { var, tp, df } in self.0 {
142                    if !first {
143                        f.write_str(", ")?;
144                    }
145                    first = false;
146                    var.name().fmt(f)?;
147                    if let Some(tp) = tp {
148                        write!(f, " : {:?}", tp.debug_short())?;
149                    }
150                    if let Some(df) = df {
151                        write!(f, " := {:?}", df.debug_short())?;
152                    }
153                }
154                Ok(())
155            }
156        }
157        write!(
158            f,
159            "{} := {{{:?}}} {:?} (: {:?})",
160            self.name,
161            CtxWrap(&self.context),
162            self.solution,
163            self.tp
164        )
165    }
166}
167impl PartialEq for Solvable {
168    #[inline]
169    fn eq(&self, other: &Self) -> bool {
170        self.name == other.name
171    }
172}
173impl Eq for Solvable {}
174impl Borrow<Id> for Solvable {
175    #[inline]
176    fn borrow(&self) -> &Id {
177        &self.name
178    }
179}
180impl std::hash::Hash for Solvable {
181    #[inline]
182    fn hash<H: std::hash::Hasher>(&self, state: &mut H) {
183        self.name.hash(state);
184    }
185}
186
187#[derive(Default, Debug, Clone, PartialEq, Eq)]
188pub struct Solutions(pub(crate) rustc_hash::FxHashSet<Solvable>);
189impl Merge for Solutions {
190    fn merge(&mut self, other: Self) {
191        for e in other.0 {
192            self.0.remove(&e);
193            self.0.insert(e);
194        }
195    }
196}
197impl std::hash::Hash for Solutions {
198    fn hash<H: std::hash::Hasher>(&self, state: &mut H) {
199        for s in self.0.iter() {
200            s.hash(state);
201        }
202    }
203}
204
205impl MutableRefList<'_, Solutions> {
206    #[inline]
207    fn get_solvable<'s>(&'s self, name: &Id) -> Option<&'s Solvable> {
208        fn get_i<'s>(
209            slf: &'s MutableRefList<Solutions>,
210            name: &Id,
211            first: Option<&Id>,
212        ) -> Option<&'s Solvable> {
213            let s = slf.find(|s| s.0.get(name))?;
214            if let BoundedValue::Solved(s) = &s.solution
215                && let Some(s) = s.is_solvable()
216                && first != Some(s)
217            {
218                get_i(slf, s, Some(first.unwrap_or(name)))
219            } else {
220                Some(s)
221            }
222        }
223        get_i(self, name, None)
224    }
225
226    fn set_solution(&mut self, name: Id, solution: Term) {
227        let (tp, context) = self
228            .get_solvable(&name)
229            .map_or((BoundedValue::None, Vec::new()), |e| {
230                (e.tp.clone(), e.context.clone())
231            });
232        self.0.remove(&name);
233
234        let ne = Solvable {
235            name,
236            solution: BoundedValue::Solved(solution),
237            tp,
238            context,
239        };
240        self.0.insert(ne);
241    }
242    fn set_type(&mut self, name: Id, tp: Term) {
243        let (solution, context) = self
244            .get_solvable(&name)
245            .map_or((BoundedValue::None, Vec::new()), |e| {
246                (e.solution.clone(), e.context.clone())
247            });
248        let ne = Solvable {
249            name,
250            solution,
251            tp: BoundedValue::Solved(tp),
252            context,
253        };
254
255        self.0.remove(&ne);
256        self.0.insert(ne);
257    }
258    #[must_use]
259    pub fn subst(&self, term: Term) -> Term {
260        fn subst_i(slf: &MutableRefList<Solutions>, term: Term) -> Term {
261            /*
262            beta_unknowns(
263                term.modify(|t| {
264                    if let Term::Var { variable, .. } = t
265                        && let Some(var) = is_solvable_var(variable)
266                    {
267                        self.iter().flat_map(|s| s.0.iter()).find_map(|s| {
268                            if s.name == *var
269                                && let BoundedValue::Solved(t) = &s.solution
270                            {
271                                Some(std::ops::ControlFlow::Continue(t.clone()))
272                            } else {
273                                None
274                            }
275                        })
276                    } else {
277                        None
278                    }
279                })
280                .into_owned(),
281            )
282            */
283            let freevars = term.free_variables();
284            if freevars.is_empty() {
285                drop(freevars);
286                return term;
287            }
288            let mut ret = smallvec::SmallVec::<_, 2>::new();
289            for v in slf.iter().flat_map(|m| m.0.iter()) {
290                if let BoundedValue::Solved(tm) = &v.solution
291                    && freevars.iter().any(|f| f.name() == v.name.as_ref())
292                {
293                    ret.push((v.name.to_string(), slf.subst(tm.clone()))); //get(curr.0, curr.1, tm))); //tm.clone()));
294                }
295            }
296            drop(freevars);
297
298            //term / ret.as_slice()
299            match &term / ret.as_slice() {
300                Cow::Borrowed(_) => term,
301                Cow::Owned(t) if t.has_solvable() => {
302                    tracing::trace!(
303                        "substituted {:?}\n  =>  {:?}",
304                        term.debug_short(),
305                        t.debug_short()
306                    );
307                    subst_i(slf, t)
308                }
309                Cow::Owned(t) => t,
310            }
311        }
312        beta_unknowns(subst_i(self, term))
313    }
314}
315
316impl<Split: SplitStrategy> Checker<Split> {
317    pub(crate) fn new_solvable(&self) -> Id {
318        let i = self
319            .implicits
320            .fetch_add(1, std::sync::atomic::Ordering::Relaxed);
321        // SAFETY: is a valid Id
322        unsafe { format!("{PREFIX}{i}").parse().unwrap_unchecked() }
323    }
324}
325
326fn apply_solvable(name: Id, ctx: impl ExactSizeIterator<Item = Variable>) -> Term {
327    let head: Term = Variable::Name {
328        name,
329        notated: None,
330    }
331    .into();
332    if ctx.len() == 0 {
333        head
334    } else {
335        Term::Application(ApplicationTerm::new(
336            head,
337            Box::new([Argument::Sequence(MaybeSequence::Seq(
338                ctx.map(Into::into).collect(),
339            ))]),
340            None,
341        ))
342    }
343}
344
345impl<Split: SplitStrategy> CheckRef<'_, '_, Split> {
346    #[must_use]
347    pub fn new_solvable(&mut self) -> Term {
348        let name = self.top.new_solvable();
349        self.add_solvable(name.clone());
350        apply_solvable(name, self.context.as_ref().iter().map(|cv| cv.var.clone()))
351    }
352    pub(crate) fn solve_equality(&mut self, unk: &Id, solution: &Term) -> Option<bool> {
353        self.comment(format!("solving unknown {unk}"));
354        let Some(unks) = self.get_solvable(unk) else {
355            self.failure("Unknown unknown!");
356            return Some(false);
357        };
358        let solution = self.subst(solution.clone());
359
360        if let BoundedValue::Solved(tm) = &unks.solution {
361            let tm = tm.clone();
362            let ctx = unks
363                .context
364                .iter()
365                .cloned()
366                .map(cleanup_cv)
367                .collect::<Vec<_>>();
368            self.comment("already solved");
369            let solution = if ctx.is_empty() {
370                solution
371            } else {
372                Term::Bound(BindingTerm::new(
373                    (*ftml_uris::metatheory::BIND_UNKNOWNS).clone().into(),
374                    Box::new([
375                        BoundArgument::BoundSeq(MaybeSequence::Seq(ctx.into_boxed_slice())),
376                        BoundArgument::Simple(solution),
377                    ]),
378                    None,
379                ))
380            };
381            return self.scoped(|slf| slf.check_equality(&solution, &tm));
382        }
383        self.solve(unk.clone(), solution)?;
384        Some(true)
385    }
386
387    pub(crate) fn solve_upper_bound(&mut self, unk: &Id, bound: &Term) -> Option<bool> {
388        tracing::debug!("Solving upper bound");
389        self.comment(format!("solving boundaries of unknown {unk}"));
390        let Some(unks) = self.get_solvable(unk) else {
391            self.failure("Unknown unknown!");
392            return Some(false);
393        };
394        let bound = self.subst(bound.clone());
395
396        if let BoundedValue::Solved(tm) = &unks.solution {
397            let tm = tm.clone();
398            let ctx = unks
399                .context
400                .iter()
401                .cloned()
402                .map(cleanup_cv)
403                .collect::<Vec<_>>();
404            self.comment("already solved");
405            let bound = if ctx.is_empty() {
406                bound
407            } else {
408                Term::Bound(BindingTerm::new(
409                    (*ftml_uris::metatheory::BIND_UNKNOWNS).clone().into(),
410                    Box::new([
411                        BoundArgument::BoundSeq(MaybeSequence::Seq(ctx.into_boxed_slice())),
412                        BoundArgument::Simple(bound),
413                    ]),
414                    None,
415                ))
416            };
417            return self.scoped(|slf| slf.check_subtype(&tm, &bound));
418        }
419        /*
420        if let BoundedValue::Bounded(lower, upper) = &unks.solution {
421            let lower = lower.clone();
422            let upper = upper.clone();
423            drop(unks);
424            return context.in_branch(|context| {
425                if let Some(lower) = lower {
426                    trace.comment("Checking against previous lower bound");
427                    let r = self.check_subtype(trace, context, &lower, sup);
428                    if r != Some(true) {
429                        return r;
430                    }
431                }
432                if let Some(upper) = upper {
433                    trace.comment("Checking against previous upper bound");
434                    let r = self.check_subtype(trace, context, &upper, sup);
435                    if r != Some(true) {
436                        return r;
437                    }
438                }
439            });
440        }
441
442        trace.comment(format!("Solving upper type bound of {unk}"));
443         */
444        self.solve(unk.clone(), bound)?;
445        Some(true)
446    }
447
448    pub(crate) fn solve_lower_bound(&mut self, unk: &Id, bound: &Term) -> Option<bool> {
449        tracing::debug!("Solving lower bound");
450        self.comment(format!("solving boundaries of unknown {unk}"));
451        let Some(unks) = self.get_solvable(unk) else {
452            self.failure("Unknown unknown!");
453            return Some(false);
454        };
455
456        let bound = self.subst(bound.clone());
457
458        // todo boundary checks
459        //
460        if let BoundedValue::Solved(tm) = &unks.solution {
461            let tm = tm.clone();
462            let ctx = unks
463                .context
464                .iter()
465                .cloned()
466                .map(cleanup_cv)
467                .collect::<Vec<_>>();
468            self.comment("already solved");
469            let bound = if ctx.is_empty() {
470                bound
471            } else {
472                Term::Bound(BindingTerm::new(
473                    (*ftml_uris::metatheory::BIND_UNKNOWNS).clone().into(),
474                    Box::new([
475                        BoundArgument::BoundSeq(MaybeSequence::Seq(ctx.into_boxed_slice())),
476                        BoundArgument::Simple(bound),
477                    ]),
478                    None,
479                ))
480            };
481            return self.scoped(|slf| slf.check_subtype(&bound, &tm));
482        }
483        self.solve(unk.clone(), bound)?;
484        Some(true)
485    }
486
487    #[inline]
488    pub(crate) fn merge_solutions(&mut self, solutions: Solutions) {
489        self.solutions.merge(solutions);
490    }
491    fn add_solvable(&mut self, name: Id) {
492        self.solutions.0.insert(Solvable::new(
493            name,
494            self.context.as_ref().iter().map(|v| v.clone().into_owned()),
495        ));
496    }
497
498    pub fn get_solution(&self, name: &Id) -> Option<Term> {
499        self.get_solvable(name)
500            .and_then(Solvable::solution)
501            .map(|t| self.subst(t.clone()))
502    }
503
504    fn get_solvable<'s>(&'s self, name: &Id) -> Option<&'s Solvable> {
505        self.solutions.get_solvable(name)
506        /*
507        fn get<'i>(
508            sols: &'i rustc_hash::FxHashSet<Solvable>,
509            anc: Option<Ancestor<'i>>,
510            name: &Id,
511        ) -> Option<&'i Solvable> {
512            sols.get(name)
513                .or_else(|| anc.and_then(|Ancestor { p, gp }| get(p, gp.copied(), name)))
514        }
515        fn get_solvable_i<'s, Split: SplitStrategy>(
516            slf: &'s CheckRef<Split>,
517            name: &Id,
518            first: Option<&Id>,
519        ) -> Option<&'s Solvable> {
520            let s = get(slf.solutions, slf.parent_solutions, name)?;
521            if let BoundedValue::Solved(s) = &s.solution
522                && let Some(s) = s.is_solvable()
523                && first != Some(s)
524            {
525                get_solvable_i(slf, s, Some(first.unwrap_or(name)))
526            } else {
527                Some(s)
528            }
529        }
530        get_solvable_i(self, name, None)
531         */
532    }
533
534    pub(crate) fn get_solvable_type(&mut self, name: &Id) -> Term {
535        let ctx = if let Some(s) = self.get_solvable(name) {
536            if let BoundedValue::Solved(t) = &s.tp {
537                return t.clone();
538            }
539            Some(
540                s.context
541                    .iter()
542                    .cloned()
543                    .map(cleanup_cv)
544                    .collect::<Vec<_>>(),
545            )
546        } else {
547            None
548        };
549        let ctx = ctx.unwrap_or(Vec::new());
550        let tp_name = self.top.new_solvable();
551        self.solutions
552            .0
553            .insert(Solvable::new(tp_name.clone(), ctx.iter().cloned()));
554        let tp: Term = if ctx.is_empty() {
555            tp_name.into()
556        } else {
557            let body = apply_solvable(tp_name, ctx.iter().map(|cv| cv.var.clone()));
558            Term::Bound(BindingTerm::new(
559                (*ftml_uris::metatheory::BIND_UNKNOWNS).clone().into(),
560                Box::new([
561                    BoundArgument::BoundSeq(MaybeSequence::Seq(ctx.into_boxed_slice())),
562                    BoundArgument::Simple(body),
563                ]),
564                None,
565            ))
566        };
567        self.solve_type(name.clone(), tp.clone());
568        tp
569    }
570
571    fn solve(&mut self, name: Id, solution: Term) -> Option<()> {
572        let Some((ctx, tp)) = self.get_solvable(&name).map(|s| {
573            (
574                s.context
575                    .iter()
576                    .cloned()
577                    .map(cleanup_cv)
578                    .collect::<Vec<_>>(),
579                (), /*s.tp.clone()*/
580            )
581        }) else {
582            self.failure("Unknown not found");
583            return None;
584        };
585        let solution = self.subst(solution);
586        if solution.has_free_such_that(|v| v.name() == name.as_ref()) {
587            tracing::debug!("Circular solution! {:?}", solution.debug_short());
588            self.failure(format!("Circular solution: {:?}", solution.debug_short()));
589            return None;
590        }
591        let solution = if ctx.is_empty() {
592            solution
593        } else {
594            Term::Bound(BindingTerm::new(
595                (*ftml_uris::metatheory::BIND_UNKNOWNS).clone().into(),
596                Box::new([
597                    BoundArgument::BoundSeq(MaybeSequence::Seq(ctx.into_boxed_slice())),
598                    BoundArgument::Simple(solution),
599                ]),
600                None,
601            ))
602        };
603        tracing::debug!("solving {name} as {:?}", solution.debug_short());
604        self.comment(format!("Solved {name} as {:?}", solution.debug_short()));
605        /*if let BoundedValue::Solved(tp) = tp {
606            self.comment("Checking against previous type solution");
607            self.scoped(|slf| slf.check_type(&solution, &tp))?;
608        }*/
609        self.solutions.set_solution(name, solution);
610        Some(())
611    }
612    fn solve_type(&mut self, name: Id, tp: Term) {
613        let tp = self.subst(tp);
614        self.solutions.set_type(name, tp);
615    }
616
617    pub(crate) fn subst(&self, term: Term) -> Term {
618        self.solutions.subst(term) //Self::subst_map(term, self.solutions, self.parent_solutions)
619    }
620}
621
622fn cleanup_cv(cv: ComponentVar) -> ComponentVar {
623    ComponentVar {
624        var: cv.var,
625        tp: None,
626        df: None,
627    }
628}
ftml_solver/impls/solving.rs

ftml_solver/impls/
solving.rs
