ftml_solver/
facts.rs

1use std::borrow::Cow;
2
3use ftml_ontology::{
4    domain::declarations::symbols::Symbol,
5    narrative::{SharedDocumentElement, elements::VariableDeclaration},
6    terms::{Argument, ComponentVar, Term, Variable, helpers::Bound, patterns::Pattern},
7};
8use ftml_uris::{DocumentElementUri, Id, SymbolUri};
9use smallvec::SmallVec;
10
11use crate::{
12    CheckRef, Checker, hoas::HOASSymbols, impls::solving::TermExtSolvable,
13    rules::implicits::ImplicitExtBound, split::SplitStrategy,
14};
15
16impl<Split: SplitStrategy> Checker<Split> {
17    pub(crate) fn add_fact(&mut self, s: &Symbol) {
18        // SAFETY: valid ID
19        static NOAUTO: std::sync::LazyLock<Id> =
20            std::sync::LazyLock::new(|| unsafe { "noauto".parse().unwrap_unchecked() });
21        if !s.data.role.contains(&*NOAUTO)
22            && let Some(hoas) = self.hoas()
23            && let Some(fact) = Fact::from_symbol(hoas, s, self, |uri| {
24                crate::impls::backend::get_variable(
25                    &self.backend,
26                    &self.documents,
27                    &self.current,
28                    uri,
29                    |t| self.prepare(None, t).1,
30                )
31            })
32        {
33            self.facts.facts.push((s.uri.clone(), fact));
34            /*self.facts.add(hoas, s, );*/
35        }
36    }
37}
38
39impl<Split: SplitStrategy> CheckRef<'_, '_, Split> {
40    pub fn facts_for(
41        &self,
42        goal: &Term,
43    ) -> impl Iterator<Item = (GlobalOrLocal, Vec<GoalPremise>)> {
44        self.context
45            .facts()
46            .find_applicable(self.context.goal_counter(), goal)
47            .chain(self.top.facts.find_applicable(
48                goal,
49                self.context.goal_counter(),
50                self.context.blocked(),
51            ))
52    }
53}
54#[derive(Clone)]
55pub enum GlobalOrLocal {
56    Global(SymbolUri),
57    Local(usize),
58}
59impl GlobalOrLocal {
60    pub(crate) fn into_term(self, ctx: &[Cow<'_, ComponentVar>]) -> Term {
61        match self {
62            Self::Global(s) => s.into(),
63            Self::Local(i) => ctx[i].var.clone().into(),
64        }
65    }
66}
67impl std::fmt::Display for GlobalOrLocal {
68    fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result {
69        match self {
70            Self::Global(uri) => uri.name().fmt(f),
71            Self::Local(i) => i.fmt(f),
72        }
73    }
74}
75
76#[derive(Clone, Default)]
77pub(crate) struct GlobalFacts {
78    facts: Vec<(SymbolUri, Fact)>,
79}
80impl GlobalFacts {
81    pub fn find_applicable(
82        &self,
83        goal: &Term,
84        counter: &std::sync::atomic::AtomicUsize,
85        blocked: &[GlobalOrLocal],
86    ) -> impl Iterator<Item = (GlobalOrLocal, Vec<GoalPremise>)> {
87        self.facts.iter().filter_map(|(uri, fact)| {
88            if blocked.iter().any(|b| {
89                if let GlobalOrLocal::Global(b) = b {
90                    b == uri
91                } else {
92                    false
93                }
94            }) {
95                return None;
96            }
97            fact.applies(goal, counter)
98                .map(|r| (GlobalOrLocal::Global(uri.clone()), r))
99        })
100    }
101}
102
103#[derive(Default, Clone)]
104pub(crate) struct LocalFacts {
105    pub(crate) facts: Vec<(usize, Fact)>,
106}
107impl LocalFacts {
108    pub fn find_applicable(
109        &self,
110        counter: &std::sync::atomic::AtomicUsize,
111        goal: &Term,
112    ) -> impl Iterator<Item = (GlobalOrLocal, Vec<GoalPremise>)> {
113        self.facts.iter().filter_map(|(idx, fact)| {
114            fact.applies(goal, counter)
115                .map(|r| (GlobalOrLocal::Local(*idx), r))
116        })
117    }
118}
119
120impl std::fmt::Debug for LocalFacts {
121    #[inline]
122    fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result {
123        let mut ls = f.debug_list();
124        for f in &self.facts {
125            ls.entry(f);
126        }
127        ls.finish()
128    }
129}
130
131impl std::fmt::Debug for GlobalFacts {
132    #[inline]
133    fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result {
134        let mut ls = f.debug_list();
135        for f in &self.facts {
136            ls.entry(&(f.0.name(), &f.1));
137        }
138        ls.finish()
139    }
140}
141
142#[derive(Clone)]
143pub(crate) struct TypeGuard {
144    pub name: Id,
145    pub tp: Term,
146    pub is_sequence: bool,
147    pub is_premise: bool,
148}
149impl std::fmt::Debug for TypeGuard {
150    fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result {
151        if self.is_premise {
152            write!(
153                f,
154                "Premise({}: ({:?}){})",
155                self.name,
156                self.tp.debug_short(),
157                if self.is_sequence { "*" } else { "" }
158            )
159        } else {
160            write!(
161                f,
162                "{}: ({:?}){}",
163                self.name,
164                self.tp.debug_short(),
165                if self.is_sequence { "*" } else { "" }
166            )
167        }
168    }
169}
170
171#[derive(Clone)]
172pub(crate) struct Fact {
173    pub type_guards: Box<[TypeGuard]>,
174    //pub judgment: SymbolUri,
175    pub pattern: Pattern,
176}
177#[allow(clippy::missing_fields_in_debug)]
178impl std::fmt::Debug for Fact {
179    fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result {
180        f.debug_struct("Fact")
181            .field("guards", &self.type_guards)
182            .field("pattern", &self.pattern)
183            .finish()
184    }
185}
186impl Fact {
187    pub fn applies(
188        &self,
189        goal: &Term,
190        counter: &std::sync::atomic::AtomicUsize,
191    ) -> Option<Vec<GoalPremise>> {
192        fn get_name(counter: &std::sync::atomic::AtomicUsize) -> Id {
193            let i = counter.fetch_add(1, std::sync::atomic::Ordering::AcqRel);
194            // SAFETY: valid ID
195            unsafe { format!("SGL_{i}").parse().unwrap_unchecked() }
196        }
197        fn do_tg<'s>(
198            slf: &'s Fact,
199            mut tgs: impl Iterator<Item = &'s TypeGuard>,
200            ret: &mut Vec<GoalPremise>,
201            subst: &mut Vec<(&'s str, Cow<'s, Term>)>,
202            ass: &'s [Cow<'s, Term>],
203            counter: &std::sync::atomic::AtomicUsize,
204        ) {
205            while let Some(tg) = tgs.next() {
206                if let Some(idx) = slf.pattern.vars.iter().position(|v| *v == tg.name) {
207                    let p = &*ass[idx];
208                    ret.push(GoalPremise::Typing {
209                        elem: p.clone(),
210                        tp: tg.tp.clone() / &**subst,
211                        is_sequence: tg.is_sequence,
212                    });
213                    subst.push((tg.name.as_ref(), Cow::Borrowed(p)));
214                } else if tg.is_premise {
215                    ret.push(GoalPremise::Proof(tg.tp.clone() / &**subst));
216                } else {
217                    let name = get_name(counter);
218                    let tp = tg.tp.clone() / &**subst;
219                    let is_sequence = tg.is_sequence;
220                    let mut premises = Vec::new();
221                    let idx = ret.len();
222                    subst.push((tg.name.as_ref(), Cow::Owned(name.clone().into())));
223                    do_tg(slf, tgs, ret, subst, ass, counter);
224                    let mut curr = idx;
225                    while let Some(e) = ret.get(curr) {
226                        if e.uses(&name) {
227                            let e = ret.remove(curr);
228                            premises.push(e)
229                        } else {
230                            curr += 1;
231                        }
232                    }
233                    ret.insert(
234                        idx,
235                        GoalPremise::NeedSuchThat {
236                            name,
237                            tp,
238                            is_sequence,
239                            premises,
240                        },
241                    );
242                    return;
243                }
244            }
245        }
246        let ass = self.pattern.matches(goal)?;
247        let mut ret = Vec::new();
248        let mut subst = Vec::new();
249        do_tg(
250            self,
251            self.type_guards.iter(),
252            &mut ret,
253            &mut subst,
254            &ass,
255            counter,
256        );
257        Some(ret)
258    }
259
260    pub fn from_tp<Split: SplitStrategy>(
261        hoas: &HOASSymbols,
262        tp: &Term,
263        checker: &Checker<Split>,
264    ) -> Option<Self> {
265        return None;
266        if tp.has_solvable() {
267            return None;
268        }
269        tracing::trace!("Fact?");
270        let Some(judg) = hoas.judgment.as_ref() else {
271            //tracing::warn!("No judgment");
272            return None;
273        };
274        let mut type_guards = Vec::new();
275        let stp = checker
276            .wrap_none(None, |mut slf| {
277                slf.simplify_full(crate::impls::simplify::Expansion::Full, tp)
278            })
279            .1;
280        let mut curr = stp.as_ref().unwrap_or(tp);
281        loop {
282            if let Some([Argument::Simple(prop)]) = curr.unapply(judg) {
283                let pat = Pattern::from(prop.clone(), true);
284                return Some(Self {
285                    type_guards: type_guards.into_boxed_slice(),
286                    //judgment: judg,
287                    pattern: pat,
288                });
289            }
290            if let Some(Bound {
291                var,
292                tp,
293                body,
294                is_sequence,
295            }) = curr.unbind(&hoas.pi)
296            {
297                let name = var.name_id().into_owned();
298                let tg = if !body.has_free_such_that(|v| v.name() == name.as_ref())
299                    && let Some([Argument::Simple(premise)]) = tp.unapply(judg)
300                {
301                    TypeGuard {
302                        name,
303                        tp: premise.clone(),
304                        is_sequence,
305                        is_premise: true,
306                    }
307                } else {
308                    TypeGuard {
309                        name,
310                        tp: tp.clone(),
311                        is_sequence,
312                        is_premise: false,
313                    }
314                };
315                type_guards.push(tg);
316                curr = body;
317            } else {
318                //tracing::warn!("Type does not match: {:?} ({:?})", curr.debug_short(), curr);
319                return None;
320            }
321        }
322    }
323
324    pub fn from_symbol<Split: SplitStrategy>(
325        hoas: &HOASSymbols,
326        s: &Symbol,
327        checker: &Checker<Split>,
328        get: impl Fn(&DocumentElementUri) -> Result<SharedDocumentElement<VariableDeclaration>, ()>,
329    ) -> Option<Self> {
330        let Some(judg) = hoas.judgment.as_ref() else {
331            //tracing::warn!("No judgment");
332            return None;
333        };
334        let Some(tp) = s.data.tp.checked_or_parsed() else {
335            //tracing::warn!("No type");
336            return None;
337        };
338        if !tp.1 {
339            return None;
340        }
341        let tp =
342            tp.0.get_bound_implicits()
343                .map(|(t, _)| t.clone())
344                .unwrap_or(tp.0);
345        /*let tp = checker
346        .wrap_none(None, |mut slf| slf.simplify_full(true, &tp))
347        .1
348        .unwrap_or(tp);*/
349        let allvars = tp.free_variables();
350        let mut type_guards = Vec::new();
351        let mut curr = &tp;
352        loop {
353            if let Some([Argument::Simple(prop)]) = curr.unapply(judg) {
354                let pat = Pattern::from(prop.clone(), true);
355
356                let mut allvars = allvars.into_iter().cloned().collect::<SmallVec<_, 4>>();
357                let mut curr_idx = 0;
358                let mut added_since = 0;
359                let mut insert_idx = 0;
360                while curr_idx < allvars.len() {
361                    if let Variable::Ref { declaration, .. } = &allvars[curr_idx]
362                        && let Ok(v) = get(declaration)
363                        && let Some((tp, _)) = v.data.tp.checked_or_parsed()
364                    {
365                        let vars = tp.free_variables();
366                        let mut changed = false;
367                        for v in vars {
368                            if matches!(v, Variable::Ref { .. }) && !allvars[..curr_idx].contains(v)
369                            {
370                                allvars.insert(curr_idx, v.clone());
371                                changed = true;
372                            }
373                        }
374                        if !type_guards
375                            .iter()
376                            .any(|tg: &TypeGuard| tg.name.as_ref() == v.uri.name().last())
377                        {
378                            let name = allvars[curr_idx].name_id().into_owned();
379                            let is_sequence = v.data.is_seq;
380                            let tg = if !pat.vars.contains(&name)
381                                && let Some([Argument::Simple(premise)]) = tp.unapply(judg)
382                            {
383                                TypeGuard {
384                                    name,
385                                    tp: premise.clone(),
386                                    is_sequence,
387                                    is_premise: true,
388                                }
389                            } else {
390                                TypeGuard {
391                                    name,
392                                    tp,
393                                    is_sequence,
394                                    is_premise: false,
395                                }
396                            };
397                            type_guards.insert(insert_idx, tg);
398                            added_since += 1;
399                        }
400                        if changed {
401                            continue;
402                        }
403                    }
404                    insert_idx += added_since;
405                    added_since = 0;
406                    curr_idx += 1;
407                }
408
409                let ret = Self {
410                    type_guards: type_guards.into_boxed_slice(),
411                    //judgment: judg,
412                    pattern: pat,
413                };
414
415                if ret.pattern.body.has_solvable()
416                    || ret.type_guards.iter().any(|g| g.tp.has_solvable())
417                {
418                    return None;
419                }
420
421                return Some(ret);
422            }
423            if let Some(Bound {
424                var,
425                tp,
426                body,
427                is_sequence,
428            }) = curr.unbind(&hoas.pi)
429            {
430                let name = var.name_id().into_owned();
431                let tg = if !body.has_free_such_that(|v| v.name() == name.as_ref())
432                    && let Some([Argument::Simple(premise)]) = tp.unapply(judg)
433                {
434                    TypeGuard {
435                        name,
436                        tp: premise.clone(),
437                        is_sequence,
438                        is_premise: true,
439                    }
440                } else {
441                    TypeGuard {
442                        name,
443                        tp: tp.clone(),
444                        is_sequence,
445                        is_premise: false,
446                    }
447                };
448                type_guards.push(tg);
449                curr = body;
450            } else {
451                //tracing::warn!("Type does not match: {:?} ({:?})", curr.debug_short(), curr);
452                return None;
453            }
454        }
455    }
456}
457
458pub enum GoalPremise {
459    Typing {
460        elem: Term,
461        tp: Term,
462        is_sequence: bool,
463    },
464    Proof(Term),
465    NeedSuchThat {
466        name: Id,
467        tp: Term,
468        is_sequence: bool,
469        premises: Vec<Self>,
470    },
471}
472impl GoalPremise {
473    fn uses(&self, name: &Id) -> bool {
474        match self {
475            Self::Typing { elem, tp, .. } => {
476                elem.has_free_such_that(|v| v.name() == name.as_ref())
477                    || tp.has_free_such_that(|v| v.name() == name.as_ref())
478            }
479            Self::Proof(t) => t.has_free_such_that(|v| v.name() == name.as_ref()),
480            Self::NeedSuchThat { tp, premises, .. } => {
481                tp.has_free_such_that(|v| v.name() == name.as_ref())
482                    || premises.iter().any(|p| p.uses(name))
483            }
484        }
485    }
486}
487impl std::fmt::Debug for GoalPremise {
488    fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result {
489        match self {
490            Self::Typing {
491                elem,
492                tp,
493                is_sequence,
494            } => write!(
495                f,
496                "{:?}  :  {:?}{}",
497                elem.debug_short(),
498                tp.debug_short(),
499                if *is_sequence { "*" } else { "" }
500            ),
501            Self::Proof(tm) => write!(f, "⊢ {:?}", tm.debug_short()),
502            Self::NeedSuchThat {
503                name,
504                tp,
505                is_sequence,
506                premises,
507            } => {
508                write!(
509                    f,
510                    "SOME {name} : {:?}{}",
511                    tp.debug_short(),
512                    if *is_sequence { "*" } else { "" }
513                )?;
514                if !premises.is_empty() {
515                    f.write_str(" such that [")?;
516                    for p in premises {
517                        p.fmt(f)?;
518                    }
519                    f.write_str("]")?;
520                }
521                Ok(())
522            }
523        }
524    }
525}
ftml_solver/facts.rs

ftml_solver/
facts.rs
