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)]
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}
197
198impl MutableRefList<'_, Solutions> {
199    #[inline]
200    fn get_solvable<'s>(&'s self, name: &Id) -> Option<&'s Solvable> {
201        fn get_i<'s>(
202            slf: &'s MutableRefList<Solutions>,
203            name: &Id,
204            first: Option<&Id>,
205        ) -> Option<&'s Solvable> {
206            let s = slf.find(|s| s.0.get(name))?;
207            if let BoundedValue::Solved(s) = &s.solution
208                && let Some(s) = s.is_solvable()
209                && first != Some(s)
210            {
211                get_i(slf, s, Some(first.unwrap_or(name)))
212            } else {
213                Some(s)
214            }
215        }
216        get_i(self, name, None)
217    }
218
219    fn set_solution(&mut self, name: Id, solution: Term) {
220        let (tp, context) = self
221            .get_solvable(&name)
222            .map_or((BoundedValue::None, Vec::new()), |e| {
223                (e.tp.clone(), e.context.clone())
224            });
225        self.0.remove(&name);
226
227        let ne = Solvable {
228            name,
229            solution: BoundedValue::Solved(solution),
230            tp,
231            context,
232        };
233        self.0.insert(ne);
234    }
235    fn set_type(&mut self, name: Id, tp: Term) {
236        let (solution, context) = self
237            .get_solvable(&name)
238            .map_or((BoundedValue::None, Vec::new()), |e| {
239                (e.solution.clone(), e.context.clone())
240            });
241        let ne = Solvable {
242            name,
243            solution,
244            tp: BoundedValue::Solved(tp),
245            context,
246        };
247
248        self.0.remove(&ne);
249        self.0.insert(ne);
250    }
251    #[must_use]
252    pub fn subst(&self, term: Term) -> Term {
253        fn subst_i(slf: &MutableRefList<Solutions>, term: Term) -> Term {
254            let freevars = term.free_variables();
255            if freevars.is_empty() {
256                drop(freevars);
257                return term;
258            }
259            let mut ret = smallvec::SmallVec::<_, 2>::new();
260            for v in slf.iter().flat_map(|m| m.0.iter()) {
261                if let BoundedValue::Solved(tm) = &v.solution
262                    && freevars.iter().any(|f| f.name() == v.name.as_ref())
263                {
264                    ret.push((v.name.to_string(), slf.subst(tm.clone()))); //get(curr.0, curr.1, tm))); //tm.clone()));
265                }
266            }
267            drop(freevars);
268
269            //term / ret.as_slice()
270            match &term / ret.as_slice() {
271                Cow::Borrowed(_) => term,
272                Cow::Owned(t) if t.has_solvable() => {
273                    tracing::trace!(
274                        "substituted {:?}\n  =>  {:?}",
275                        term.debug_short(),
276                        t.debug_short()
277                    );
278                    subst_i(slf, t)
279                }
280                Cow::Owned(t) => t,
281            }
282        }
283        beta_unknowns(subst_i(self, term))
284    }
285}
286
287impl<Split: SplitStrategy> Checker<Split> {
288    pub(crate) fn new_solvable(&self) -> Id {
289        let i = self
290            .implicits
291            .fetch_add(1, std::sync::atomic::Ordering::Relaxed);
292        // SAFETY: is a valid Id
293        unsafe { format!("{PREFIX}{i}").parse().unwrap_unchecked() }
294    }
295}
296
297fn apply_solvable(name: Id, ctx: impl ExactSizeIterator<Item = Variable>) -> Term {
298    let head: Term = Variable::Name {
299        name,
300        notated: None,
301    }
302    .into();
303    if ctx.len() == 0 {
304        head
305    } else {
306        Term::Application(ApplicationTerm::new(
307            head,
308            Box::new([Argument::Sequence(MaybeSequence::Seq(
309                ctx.map(Into::into).collect(),
310            ))]),
311            None,
312        ))
313    }
314}
315
316impl<Split: SplitStrategy> CheckRef<'_, '_, Split> {
317    #[must_use]
318    pub fn new_solvable(&mut self) -> Term {
319        let name = self.top.new_solvable();
320        self.add_solvable(name.clone());
321        apply_solvable(name, self.context.as_ref().iter().map(|cv| cv.var.clone()))
322    }
323    pub(crate) fn solve_equality(&mut self, unk: &Id, solution: &Term) -> Option<bool> {
324        self.comment(format!("solving unknown {unk}"));
325        let Some(unks) = self.get_solvable(unk) else {
326            self.failure("Unknown unknown!");
327            return Some(false);
328        };
329        let solution = self.subst(solution.clone());
330
331        if let BoundedValue::Solved(tm) = &unks.solution {
332            let tm = tm.clone();
333            let ctx = unks
334                .context
335                .iter()
336                .cloned()
337                .map(cleanup_cv)
338                .collect::<Vec<_>>();
339            self.comment("already solved");
340            let solution = if ctx.is_empty() {
341                solution
342            } else {
343                Term::Bound(BindingTerm::new(
344                    (*ftml_uris::metatheory::BIND_UNKNOWNS).clone().into(),
345                    Box::new([
346                        BoundArgument::BoundSeq(MaybeSequence::Seq(ctx.into_boxed_slice())),
347                        BoundArgument::Simple(solution),
348                    ]),
349                    None,
350                ))
351            };
352            return self.scoped(|slf| slf.check_equality(&solution, &tm));
353        }
354        self.solve(unk.clone(), solution)?;
355        Some(true)
356    }
357
358    pub(crate) fn solve_upper_bound(&mut self, unk: &Id, bound: &Term) -> Option<bool> {
359        tracing::debug!("Solving upper bound");
360        self.comment(format!("solving boundaries of unknown {unk}"));
361        let Some(unks) = self.get_solvable(unk) else {
362            self.failure("Unknown unknown!");
363            return Some(false);
364        };
365        let bound = self.subst(bound.clone());
366
367        if let BoundedValue::Solved(tm) = &unks.solution {
368            let tm = tm.clone();
369            let ctx = unks
370                .context
371                .iter()
372                .cloned()
373                .map(cleanup_cv)
374                .collect::<Vec<_>>();
375            self.comment("already solved");
376            let bound = if ctx.is_empty() {
377                bound
378            } else {
379                Term::Bound(BindingTerm::new(
380                    (*ftml_uris::metatheory::BIND_UNKNOWNS).clone().into(),
381                    Box::new([
382                        BoundArgument::BoundSeq(MaybeSequence::Seq(ctx.into_boxed_slice())),
383                        BoundArgument::Simple(bound),
384                    ]),
385                    None,
386                ))
387            };
388            return self.scoped(|slf| slf.check_subtype(&tm, &bound));
389        }
390        /*
391        if let BoundedValue::Bounded(lower, upper) = &unks.solution {
392            let lower = lower.clone();
393            let upper = upper.clone();
394            drop(unks);
395            return context.in_branch(|context| {
396                if let Some(lower) = lower {
397                    trace.comment("Checking against previous lower bound");
398                    let r = self.check_subtype(trace, context, &lower, sup);
399                    if r != Some(true) {
400                        return r;
401                    }
402                }
403                if let Some(upper) = upper {
404                    trace.comment("Checking against previous upper bound");
405                    let r = self.check_subtype(trace, context, &upper, sup);
406                    if r != Some(true) {
407                        return r;
408                    }
409                }
410            });
411        }
412
413        trace.comment(format!("Solving upper type bound of {unk}"));
414         */
415        self.solve(unk.clone(), bound)?;
416        Some(true)
417    }
418
419    pub(crate) fn solve_lower_bound(&mut self, unk: &Id, bound: &Term) -> Option<bool> {
420        tracing::debug!("Solving lower bound");
421        self.comment(format!("solving boundaries of unknown {unk}"));
422        let Some(unks) = self.get_solvable(unk) else {
423            self.failure("Unknown unknown!");
424            return Some(false);
425        };
426
427        let bound = self.subst(bound.clone());
428
429        // todo boundary checks
430        //
431        if let BoundedValue::Solved(tm) = &unks.solution {
432            let tm = tm.clone();
433            let ctx = unks
434                .context
435                .iter()
436                .cloned()
437                .map(cleanup_cv)
438                .collect::<Vec<_>>();
439            self.comment("already solved");
440            let bound = if ctx.is_empty() {
441                bound
442            } else {
443                Term::Bound(BindingTerm::new(
444                    (*ftml_uris::metatheory::BIND_UNKNOWNS).clone().into(),
445                    Box::new([
446                        BoundArgument::BoundSeq(MaybeSequence::Seq(ctx.into_boxed_slice())),
447                        BoundArgument::Simple(bound),
448                    ]),
449                    None,
450                ))
451            };
452            return self.scoped(|slf| slf.check_subtype(&bound, &tm));
453        }
454        self.solve(unk.clone(), bound)?;
455        Some(true)
456    }
457
458    #[inline]
459    pub(crate) fn merge_solutions(&mut self, solutions: Solutions) {
460        self.solutions.merge(solutions);
461    }
462    fn add_solvable(&mut self, name: Id) {
463        self.solutions.0.insert(Solvable::new(
464            name,
465            self.context.as_ref().iter().map(|v| v.clone().into_owned()),
466        ));
467    }
468
469    pub fn get_solution(&self, name: &Id) -> Option<Term> {
470        self.get_solvable(name)
471            .and_then(Solvable::solution)
472            .map(|t| self.subst(t.clone()))
473    }
474
475    fn get_solvable<'s>(&'s self, name: &Id) -> Option<&'s Solvable> {
476        self.solutions.get_solvable(name)
477        /*
478        fn get<'i>(
479            sols: &'i rustc_hash::FxHashSet<Solvable>,
480            anc: Option<Ancestor<'i>>,
481            name: &Id,
482        ) -> Option<&'i Solvable> {
483            sols.get(name)
484                .or_else(|| anc.and_then(|Ancestor { p, gp }| get(p, gp.copied(), name)))
485        }
486        fn get_solvable_i<'s, Split: SplitStrategy>(
487            slf: &'s CheckRef<Split>,
488            name: &Id,
489            first: Option<&Id>,
490        ) -> Option<&'s Solvable> {
491            let s = get(slf.solutions, slf.parent_solutions, name)?;
492            if let BoundedValue::Solved(s) = &s.solution
493                && let Some(s) = s.is_solvable()
494                && first != Some(s)
495            {
496                get_solvable_i(slf, s, Some(first.unwrap_or(name)))
497            } else {
498                Some(s)
499            }
500        }
501        get_solvable_i(self, name, None)
502         */
503    }
504
505    pub(crate) fn get_solvable_type(&mut self, name: &Id) -> Term {
506        let ctx = if let Some(s) = self.get_solvable(name) {
507            if let BoundedValue::Solved(t) = &s.tp {
508                return t.clone();
509            }
510            Some(
511                s.context
512                    .iter()
513                    .cloned()
514                    .map(cleanup_cv)
515                    .collect::<Vec<_>>(),
516            )
517        } else {
518            None
519        };
520        let ctx = ctx.unwrap_or(Vec::new());
521        let tp_name = self.top.new_solvable();
522        self.solutions
523            .0
524            .insert(Solvable::new(tp_name.clone(), ctx.iter().cloned()));
525        let tp: Term = if ctx.is_empty() {
526            tp_name.into()
527        } else {
528            let body = apply_solvable(tp_name, ctx.iter().map(|cv| cv.var.clone()));
529            Term::Bound(BindingTerm::new(
530                (*ftml_uris::metatheory::BIND_UNKNOWNS).clone().into(),
531                Box::new([
532                    BoundArgument::BoundSeq(MaybeSequence::Seq(ctx.into_boxed_slice())),
533                    BoundArgument::Simple(body),
534                ]),
535                None,
536            ))
537        };
538        self.solve_type(name.clone(), tp.clone());
539        tp
540    }
541
542    fn solve(&mut self, name: Id, solution: Term) -> Option<()> {
543        let Some((ctx, tp)) = self.get_solvable(&name).map(|s| {
544            (
545                s.context
546                    .iter()
547                    .cloned()
548                    .map(cleanup_cv)
549                    .collect::<Vec<_>>(),
550                (), /*s.tp.clone()*/
551            )
552        }) else {
553            self.failure("Unknown not found");
554            return None;
555        };
556        let solution = self.subst(solution);
557        if solution.has_free_such_that(|v| v.name() == name.as_ref()) {
558            tracing::debug!("Circular solution! {:?}", solution.debug_short());
559            self.failure(format!("Circular solution: {:?}", solution.debug_short()));
560            return None;
561        }
562        let solution = if ctx.is_empty() {
563            solution
564        } else {
565            Term::Bound(BindingTerm::new(
566                (*ftml_uris::metatheory::BIND_UNKNOWNS).clone().into(),
567                Box::new([
568                    BoundArgument::BoundSeq(MaybeSequence::Seq(ctx.into_boxed_slice())),
569                    BoundArgument::Simple(solution),
570                ]),
571                None,
572            ))
573        };
574        tracing::debug!("solving {name} as {:?}", solution.debug_short());
575        self.comment(format!("Solved {name} as {:?}", solution.debug_short()));
576        /*if let BoundedValue::Solved(tp) = tp {
577            self.comment("Checking against previous type solution");
578            self.scoped(|slf| slf.check_type(&solution, &tp))?;
579        }*/
580        self.solutions.set_solution(name, solution);
581        Some(())
582    }
583    fn solve_type(&mut self, name: Id, tp: Term) {
584        let tp = self.subst(tp);
585        self.solutions.set_type(name, tp);
586    }
587
588    pub(crate) fn subst(&self, term: Term) -> Term {
589        self.solutions.subst(term) //Self::subst_map(term, self.solutions, self.parent_solutions)
590    }
591}
592
593fn cleanup_cv(cv: ComponentVar) -> ComponentVar {
594    ComponentVar {
595        var: cv.var,
596        tp: None,
597        df: None,
598    }
599}
ftml_solver/impls/solving.rs

ftml_solver/impls/
solving.rs
