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| slf.simplify_full(true, tp))
277            .1;
278        let mut curr = stp.as_ref().unwrap_or(tp);
279        loop {
280            if let Some([Argument::Simple(prop)]) = curr.unapply(judg) {
281                let pat = Pattern::from(prop.clone(), true);
282                return Some(Self {
283                    type_guards: type_guards.into_boxed_slice(),
284                    //judgment: judg,
285                    pattern: pat,
286                });
287            }
288            if let Some(Bound {
289                var,
290                tp,
291                body,
292                is_sequence,
293            }) = curr.unbind(&hoas.pi)
294            {
295                let name = var.name_id().into_owned();
296                let tg = if !body.has_free_such_that(|v| v.name() == name.as_ref())
297                    && let Some([Argument::Simple(premise)]) = tp.unapply(judg)
298                {
299                    TypeGuard {
300                        name,
301                        tp: premise.clone(),
302                        is_sequence,
303                        is_premise: true,
304                    }
305                } else {
306                    TypeGuard {
307                        name,
308                        tp: tp.clone(),
309                        is_sequence,
310                        is_premise: false,
311                    }
312                };
313                type_guards.push(tg);
314                curr = body;
315            } else {
316                //tracing::warn!("Type does not match: {:?} ({:?})", curr.debug_short(), curr);
317                return None;
318            }
319        }
320    }
321
322    pub fn from_symbol<Split: SplitStrategy>(
323        hoas: &HOASSymbols,
324        s: &Symbol,
325        checker: &Checker<Split>,
326        get: impl Fn(&DocumentElementUri) -> Result<SharedDocumentElement<VariableDeclaration>, ()>,
327    ) -> Option<Self> {
328        let Some(judg) = hoas.judgment.as_ref() else {
329            //tracing::warn!("No judgment");
330            return None;
331        };
332        let Some(tp) = s.data.tp.checked_or_parsed() else {
333            //tracing::warn!("No type");
334            return None;
335        };
336        if !tp.1 {
337            return None;
338        }
339        let tp =
340            tp.0.get_bound_implicits()
341                .map(|(t, _)| t.clone())
342                .unwrap_or(tp.0);
343        /*let tp = checker
344        .wrap_none(None, |mut slf| slf.simplify_full(true, &tp))
345        .1
346        .unwrap_or(tp);*/
347        let allvars = tp.free_variables();
348        let mut type_guards = Vec::new();
349        let mut curr = &tp;
350        loop {
351            if let Some([Argument::Simple(prop)]) = curr.unapply(judg) {
352                let pat = Pattern::from(prop.clone(), true);
353
354                let mut allvars = allvars.into_iter().cloned().collect::<SmallVec<_, 4>>();
355                let mut curr_idx = 0;
356                let mut added_since = 0;
357                let mut insert_idx = 0;
358                while curr_idx < allvars.len() {
359                    if let Variable::Ref { declaration, .. } = &allvars[curr_idx]
360                        && let Ok(v) = get(declaration)
361                        && let Some((tp, _)) = v.data.tp.checked_or_parsed()
362                    {
363                        let vars = tp.free_variables();
364                        let mut changed = false;
365                        for v in vars {
366                            if matches!(v, Variable::Ref { .. }) && !allvars[..curr_idx].contains(v)
367                            {
368                                allvars.insert(curr_idx, v.clone());
369                                changed = true;
370                            }
371                        }
372                        if !type_guards
373                            .iter()
374                            .any(|tg: &TypeGuard| tg.name.as_ref() == v.uri.name().last())
375                        {
376                            let name = allvars[curr_idx].name_id().into_owned();
377                            let is_sequence = v.data.is_seq;
378                            let tg = if !pat.vars.contains(&name)
379                                && let Some([Argument::Simple(premise)]) = tp.unapply(judg)
380                            {
381                                TypeGuard {
382                                    name,
383                                    tp: premise.clone(),
384                                    is_sequence,
385                                    is_premise: true,
386                                }
387                            } else {
388                                TypeGuard {
389                                    name,
390                                    tp,
391                                    is_sequence,
392                                    is_premise: false,
393                                }
394                            };
395                            type_guards.insert(insert_idx, tg);
396                            added_since += 1;
397                        }
398                        if changed {
399                            continue;
400                        }
401                    }
402                    insert_idx += added_since;
403                    added_since = 0;
404                    curr_idx += 1;
405                }
406
407                let ret = Self {
408                    type_guards: type_guards.into_boxed_slice(),
409                    //judgment: judg,
410                    pattern: pat,
411                };
412
413                if ret.pattern.body.has_solvable()
414                    || ret.type_guards.iter().any(|g| g.tp.has_solvable())
415                {
416                    return None;
417                }
418
419                return Some(ret);
420            }
421            if let Some(Bound {
422                var,
423                tp,
424                body,
425                is_sequence,
426            }) = curr.unbind(&hoas.pi)
427            {
428                let name = var.name_id().into_owned();
429                let tg = if !body.has_free_such_that(|v| v.name() == name.as_ref())
430                    && let Some([Argument::Simple(premise)]) = tp.unapply(judg)
431                {
432                    TypeGuard {
433                        name,
434                        tp: premise.clone(),
435                        is_sequence,
436                        is_premise: true,
437                    }
438                } else {
439                    TypeGuard {
440                        name,
441                        tp: tp.clone(),
442                        is_sequence,
443                        is_premise: false,
444                    }
445                };
446                type_guards.push(tg);
447                curr = body;
448            } else {
449                //tracing::warn!("Type does not match: {:?} ({:?})", curr.debug_short(), curr);
450                return None;
451            }
452        }
453    }
454}
455
456pub enum GoalPremise {
457    Typing {
458        elem: Term,
459        tp: Term,
460        is_sequence: bool,
461    },
462    Proof(Term),
463    NeedSuchThat {
464        name: Id,
465        tp: Term,
466        is_sequence: bool,
467        premises: Vec<Self>,
468    },
469}
470impl GoalPremise {
471    fn uses(&self, name: &Id) -> bool {
472        match self {
473            Self::Typing { elem, tp, .. } => {
474                elem.has_free_such_that(|v| v.name() == name.as_ref())
475                    || tp.has_free_such_that(|v| v.name() == name.as_ref())
476            }
477            Self::Proof(t) => t.has_free_such_that(|v| v.name() == name.as_ref()),
478            Self::NeedSuchThat { tp, premises, .. } => {
479                tp.has_free_such_that(|v| v.name() == name.as_ref())
480                    || premises.iter().any(|p| p.uses(name))
481            }
482        }
483    }
484}
485impl std::fmt::Debug for GoalPremise {
486    fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result {
487        match self {
488            Self::Typing {
489                elem,
490                tp,
491                is_sequence,
492            } => write!(
493                f,
494                "{:?}  :  {:?}{}",
495                elem.debug_short(),
496                tp.debug_short(),
497                if *is_sequence { "*" } else { "" }
498            ),
499            Self::Proof(tm) => write!(f, "⊢ {:?}", tm.debug_short()),
500            Self::NeedSuchThat {
501                name,
502                tp,
503                is_sequence,
504                premises,
505            } => {
506                write!(
507                    f,
508                    "SOME {name} : {:?}{}",
509                    tp.debug_short(),
510                    if *is_sequence { "*" } else { "" }
511                )?;
512                if !premises.is_empty() {
513                    f.write_str(" such that [")?;
514                    for p in premises {
515                        p.fmt(f)?;
516                    }
517                    f.write_str("]")?;
518                }
519                Ok(())
520            }
521        }
522    }
523}
ftml_solver/facts.rs

ftml_solver/
facts.rs
