ftml_solver/rules/
mod.rs

1pub mod extractors;
2pub mod fixity;
3pub mod implicits;
4pub mod operators;
5pub mod sequences;
6pub mod symbols;
7pub mod unknowns;
8pub use ftml_solver_trace::{CheckerRule, SizedSolverRule};
9use ftml_uris::SymbolUri;
10
11use crate::{CheckRef, rules::operators::typing, split::SplitStrategy};
12use ftml_ontology::{
13    domain::{
14        SharedDeclaration,
15        declarations::{SharedSymbolLike, morphisms::Morphism},
16    },
17    terms::{Argument, Term, helpers::IntoTerm, termpaths::TermPath},
18};
19use std::{fmt::Debug, ops::ControlFlow};
20
21macro_rules! rules{
22    ($($name:ident = $tp:ident $(($($e:expr),* $(,)?))? ),*$(,)?) => {
23        #[derive(Debug)]
24        pub struct RuleSet<Split: SplitStrategy> {
25            $(
26                $name:Vec<Box<dyn $tp<Split>>>
27            ),*
28        }
29
30        paste::paste!{
31            $(
32            trait [< ClonableDyn $tp>]<Split:SplitStrategy>:$tp<Split> {
33                fn [<to_dyn_ $name>](&self) -> Box<dyn $tp<Split>>;
34            }
35            impl<Split:SplitStrategy,T:$tp<Split>+Sized+Clone> [< ClonableDyn $tp>]<Split> for T {
36                fn [<to_dyn_ $name>](&self) -> Box<dyn $tp<Split>> {
37                    Box::new(self.clone()) as _
38                }
39            }
40            )*
41        }
42
43
44        impl<Split:SplitStrategy> Default for RuleSet<Split> {
45            paste::paste!{
46                fn default() -> Self {
47                    Self {
48                        $(
49                            $name: Self::[<DEFAULT_ $name:snake:upper >].iter().map(|r| r.[<to_dyn_ $name>]()).collect()
50                        ),*
51                    }
52                }
53            }
54        }
55
56        impl<Split: SplitStrategy> RuleSet<Split> {
57            paste::paste!{
58                $(
59
60                    const [<DEFAULT_ $name:snake:upper >] : &[&dyn [< ClonableDyn $tp>]<Split>] = &[
61                        $($(
62                            &$e as _
63                        ),*)?
64                    ];
65
66                    pub fn [<push_ $name>](&mut self,rule:Box<dyn $tp<Split>>) {
67                        if !self.$name.iter().any(|v| v.eq(&*rule)) {
68                            let i = self
69                                .$name
70                                .binary_search_by_key(&(-rule.priority()), |e| -e.priority())
71                                .map_or_else(|i| i, |i| i);
72                            self.$name.insert(i, rule);
73                        }
74                    }
75                    #[inline]
76                    #[must_use]
77                    pub fn $name(&self) -> &[Box<dyn $tp<Split>>] {
78                        &self.$name
79                    }
80                )*
81            }
82        }
83    }
84}
85
86rules! {
87    inference = InferenceRule(
88        sequences::SeqIndexRule,
89        sequences::SeqInferenceRule,
90        sequences::fold::FoldInferenceRule,
91        sequences::SeqConcatInferenceRule,
92        operators::numbers::NumberTypes,
93        implicits::ImplicitRule,
94        unknowns::UnknownsRule,
95        CommentRule,
96        MorphismRule,
97        super::impls::records::FieldRule,
98        ProofBarrier
99    ),
100    subtyping = SubtypeRule(
101        operators::numbers::NumberTypes,
102        super::impls::records::RecordRule,
103        CommentRule
104    ),
105    checking = CheckingRule(operators::numbers::NumberTypes),
106    inhabitable = InhabitableRule(
107        sequences::SeqUniverseRule,
108        super::impls::records::RecordRule,
109        CommentRule,
110    ),
111    equality = EqualityRule(
112        operators::numbers::NumberTypes,
113        CommentRule,
114        ProofBarrier
115        //sequences::SeqTypeEqRule
116    ),
117    universe = UniverseRule(sequences::SeqUniverseRule,CommentRule),
118    preparation = PreparationRule,
119    simplification = SimplificationRule(
120        unknowns::UnknownsRule,
121        typing::InferredTypeSimplificationRule,
122        CommentRule,
123        MorphismRule,
124        super::impls::records::FieldRule
125    ),
126    marker = MarkerRule,
127    proof = ProofRule
128}
129
130pub trait SimplificationRule<Split: SplitStrategy>: CheckerRule {
131    fn applicable(&self, term: &Term) -> bool;
132    fn apply<'t>(
133        &self,
134        checker: CheckRef<'t, '_, Split>,
135        term: &'t Term,
136    ) -> Result<Term, Option<TermPath>>;
137}
138
139pub trait EqualityRule<Split: SplitStrategy>: CheckerRule {
140    fn applicable(&self, lhs: &Term, rhs: &Term) -> bool;
141    fn apply<'t>(
142        &self,
143        checker: CheckRef<'t, '_, Split>,
144        lhs: &'t Term,
145        rhs: &'t Term,
146    ) -> Option<bool>;
147}
148
149pub trait InferenceRule<Split: SplitStrategy>: CheckerRule {
150    fn applicable(&self, term: &Term) -> bool;
151    fn infer<'t>(&self, checker: CheckRef<'t, '_, Split>, term: &'t Term) -> Option<Term>;
152}
153
154pub trait CheckingRule<Split: SplitStrategy>: CheckerRule {
155    fn applicable(&self, checker: &CheckRef<'_, '_, Split>, term: &Term, tp: &Term) -> bool;
156    fn apply<'t>(
157        &self,
158        checker: CheckRef<'t, '_, Split>,
159        term: &'t Term,
160        tp: &'t Term,
161    ) -> Option<bool>;
162}
163
164pub trait InhabitableRule<Split: SplitStrategy>: CheckerRule {
165    fn applicable(&self, term: &Term) -> bool;
166    fn apply<'t>(&self, checker: CheckRef<'t, '_, Split>, term: &'t Term) -> Option<bool>;
167}
168
169pub trait UniverseRule<Split: SplitStrategy>: CheckerRule {
170    fn applicable(&self, term: &Term) -> bool;
171    fn apply<'t>(&self, checker: CheckRef<'t, '_, Split>, term: &'t Term) -> Option<bool>;
172}
173
174pub trait SubtypeRule<Split: SplitStrategy>: CheckerRule {
175    fn applicable(&self, checker: &CheckRef<'_, '_, Split>, sub: &Term, sup: &Term) -> bool;
176    fn apply<'t>(
177        &self,
178        checker: CheckRef<'t, '_, Split>,
179        sub: &'t Term,
180        sup: &'t Term,
181    ) -> Option<bool>;
182}
183
184pub trait PreparationRule<Split: SplitStrategy>: CheckerRule {
185    fn applicable(&self, checker: &CheckRef<'_, '_, Split>, t: &Term) -> bool;
186    fn apply(
187        &self,
188        checker: &mut CheckRef<'_, '_, Split>,
189        t: Term,
190        path: Option<(&mut smallvec::SmallVec<u8, 16>, usize)>,
191    ) -> ControlFlow<Term, Term>;
192    fn applicable_revert(&self, checker: &CheckRef<'_, '_, Split>, t: &Term) -> bool;
193    fn revert(&self, checker: &CheckRef<'_, '_, Split>, t: Term) -> ControlFlow<Term, Term>;
194}
195pub trait MarkerRule<Split: SplitStrategy>: CheckerRule {}
196
197pub trait ProofRule<Split: SplitStrategy>: CheckerRule {
198    fn applicable(&self, term: &Term) -> bool;
199    fn prove<'t>(&self, checker: CheckRef<'t, '_, Split>, goal: &'t Term) -> Option<Term>;
200}
201
202#[derive(Debug, Clone, PartialEq, Eq)]
203pub struct IsJudgmentRule(pub SymbolUri);
204impl SizedSolverRule for IsJudgmentRule {
205    fn display(&self) -> Vec<crate::trace::Displayable> {
206        ftml_solver_trace::trace!(&self.0, "is a judgment")
207    }
208}
209impl<Split: SplitStrategy> MarkerRule<Split> for IsJudgmentRule {}
210
211#[derive(Debug, Clone, PartialEq, Eq)]
212pub struct HOASRule {
213    pub lambda: SymbolUri,
214    pub pi: SymbolUri,
215    pub apply: Option<SymbolUri>,
216}
217impl SizedSolverRule for HOASRule {
218    fn display(&self) -> Vec<crate::trace::Displayable> {
219        ftml_solver_trace::trace!("HOAS using ", &self.lambda, " and ", &self.pi)
220    }
221}
222impl<Split: SplitStrategy> MarkerRule<Split> for HOASRule {}
223
224#[derive(Debug, Clone, Copy, PartialEq, Eq)]
225struct CommentRule;
226impl SizedSolverRule for CommentRule {
227    fn display(&self) -> Vec<crate::trace::Displayable> {
228        ftml_solver_trace::trace!("comment")
229    }
230    fn priority(&self) -> isize {
231        1_000_000
232    }
233}
234
235fn as_comment(term: &Term) -> Option<&Term> {
236    if let Term::Application(app) = term
237        && app.head.is(&*ftml_uris::metatheory::COMMENTED)
238        && let [Argument::Simple(r), Argument::Simple(_)] = &*app.arguments
239    {
240        Some(r)
241    } else {
242        None
243    }
244}
245
246impl<Split: SplitStrategy> SimplificationRule<Split> for CommentRule {
247    fn applicable(&self, term: &Term) -> bool {
248        as_comment(term).is_some()
249    }
250    fn apply<'t>(
251        &self,
252        _: CheckRef<'t, '_, Split>,
253        term: &'t Term,
254    ) -> Result<Term, Option<TermPath>> {
255        as_comment(term).cloned().ok_or(None)
256    }
257}
258
259impl<Split: SplitStrategy> InferenceRule<Split> for CommentRule {
260    fn applicable(&self, term: &Term) -> bool {
261        as_comment(term).is_some()
262    }
263    fn infer<'t>(&self, mut checker: CheckRef<'t, '_, Split>, term: &'t Term) -> Option<Term> {
264        as_comment(term).and_then(|t| checker.infer_type(t))
265    }
266}
267
268impl<Split: SplitStrategy> InhabitableRule<Split> for CommentRule {
269    fn applicable(&self, term: &Term) -> bool {
270        as_comment(term).is_some()
271    }
272    fn apply<'t>(&self, mut checker: CheckRef<'t, '_, Split>, term: &'t Term) -> Option<bool> {
273        as_comment(term).and_then(|t| checker.check_inhabitable(t))
274    }
275}
276
277impl<Split: SplitStrategy> UniverseRule<Split> for CommentRule {
278    fn applicable(&self, term: &Term) -> bool {
279        as_comment(term).is_some()
280    }
281    fn apply<'t>(&self, mut checker: CheckRef<'t, '_, Split>, term: &'t Term) -> Option<bool> {
282        as_comment(term).and_then(|t| checker.check_universe(t))
283    }
284}
285impl<Split: SplitStrategy> SubtypeRule<Split> for CommentRule {
286    fn applicable(&self, _: &CheckRef<'_, '_, Split>, sub: &Term, sup: &Term) -> bool {
287        as_comment(sub).is_some() || as_comment(sup).is_some()
288    }
289    fn apply<'t>(
290        &self,
291        mut checker: CheckRef<'t, '_, Split>,
292        sub: &'t Term,
293        sup: &'t Term,
294    ) -> Option<bool> {
295        // one of them is different, because .applicable()
296        let sub = as_comment(sub).unwrap_or(sub);
297        let sup = as_comment(sup).unwrap_or(sup);
298        checker.check_subtype(sub, sup)
299    }
300}
301
302impl<Split: SplitStrategy> EqualityRule<Split> for CommentRule {
303    fn applicable(&self, lhs: &Term, rhs: &Term) -> bool {
304        as_comment(lhs).is_some() || as_comment(rhs).is_some()
305    }
306    fn apply<'t>(
307        &self,
308        mut checker: CheckRef<'t, '_, Split>,
309        lhs: &'t Term,
310        rhs: &'t Term,
311    ) -> Option<bool> {
312        // one of them is different, because .applicable()
313        let lhs = as_comment(lhs).unwrap_or(lhs);
314        let rhs = as_comment(rhs).unwrap_or(rhs);
315        checker.check_subtype(lhs, rhs)
316    }
317}
318
319#[derive(Debug, Clone, Copy, PartialEq, Eq)]
320pub struct MorphismRule;
321impl SizedSolverRule for MorphismRule {
322    fn priority(&self) -> isize {
323        100_000
324    }
325    fn display(&self) -> Vec<crate::trace::Displayable> {
326        ftml_solver_trace::trace!("morphism rule")
327    }
328}
329impl MorphismRule {
330    pub fn is_morphism_appl<'t, Split: SplitStrategy>(
331        t: &'t Term,
332        checker: &mut CheckRef<'_, '_, Split>,
333    ) -> Option<(SharedDeclaration<Morphism>, &'t Term)> {
334        Morphism::unapply(t, &mut |head| {
335            checker
336                .top
337                .get_symbol_like(head, |t| checker.prepare(t, None).1)
338                .ok()
339        })
340    }
341}
342impl<Split: SplitStrategy> InferenceRule<Split> for MorphismRule {
343    fn applicable(&self, term: &Term) -> bool {
344        match term {
345            Term::Application(app) if app.arguments.len() == 1 => {
346                matches!(&app.head, Term::Symbol { .. })
347                    && matches!(app.arguments.first(), Some(Argument::Simple(_)))
348            }
349            _ => false,
350        }
351    }
352    fn infer<'t>(&self, mut checker: CheckRef<'t, '_, Split>, term: &'t Term) -> Option<Term> {
353        let (m, arg) = Self::is_morphism_appl(term, &mut checker)?;
354        let arg_tp = checker.infer_type(arg)?;
355        m.apply(&arg_tp, &mut |s| {
356            checker
357                .top
358                .get_symbol_like(s, |t| checker.prepare(t, None).1)
359                .ok()
360        })
361        .ok()
362        .map(std::borrow::Cow::into_owned)
363    }
364}
365impl<Split: SplitStrategy> SimplificationRule<Split> for MorphismRule {
366    fn applicable(&self, t: &Term) -> bool {
367        match t {
368            Term::Application(app) if app.arguments.len() == 1 => {
369                matches!(&app.head, Term::Symbol { .. })
370                    && matches!(app.arguments.first(), Some(Argument::Simple(_)))
371            }
372            _ => false,
373        }
374    }
375    fn apply(
376        &self,
377        mut checker: CheckRef<'_, '_, Split>,
378        t: &Term,
379    ) -> Result<Term, Option<TermPath>> {
380        tracing::debug!("Morphism? {:?}", t.debug_short());
381        let (m, arg) = Self::is_morphism_appl(t, &mut checker).ok_or(None)?;
382        tracing::debug!("Applying morphism to {:?}", arg.debug_short());
383        m.apply(arg, &mut |s| {
384            checker
385                .top
386                .get_symbol_like(s, |t| checker.prepare(t, None).1)
387                .ok()
388        })
389        .map_or(Err(None), |a| {
390            if *a == *t {
391                //println!("Not applicable: {} to {:?}", m.uri, arg.debug_short());
392                Err(None)
393            } else {
394                tracing::debug!("Result: {:?}", a.debug_short());
395                Ok(a.into_owned())
396            }
397        })
398    }
399}
400
401#[derive(Debug, Clone, Copy, PartialEq, Eq)]
402pub(crate) struct ProofBarrier;
403impl SizedSolverRule for ProofBarrier {
404    fn priority(&self) -> isize {
405        100_000
406    }
407    fn display(&self) -> Vec<crate::trace::Displayable> {
408        ftml_solver_trace::trace!("proof barrier")
409    }
410}
411impl ProofBarrier {
412    pub fn proof_for(t: &Term) -> Option<&Term> {
413        if let Term::Application(t) = t
414            && let Term::Symbol { uri, .. } = &t.head
415            && *uri == *symbols::PROOF_BARRIER
416            && let [Argument::Simple(_), Argument::Simple(prop)] = &*t.arguments
417        {
418            return Some(prop);
419        }
420        None
421    }
422    pub fn apply(df: Term, tp: Term) -> Term {
423        symbols::PROOF_BARRIER.clone().apply_tms([df, tp])
424    }
425}
426impl<Split: SplitStrategy> InferenceRule<Split> for ProofBarrier {
427    fn applicable(&self, term: &Term) -> bool {
428        Self::proof_for(term).is_some()
429    }
430    fn infer<'t>(&self, _: CheckRef<'t, '_, Split>, term: &'t Term) -> Option<Term> {
431        Self::proof_for(term).cloned()
432    }
433}
434impl<Split: SplitStrategy> EqualityRule<Split> for ProofBarrier {
435    // Proof Irrelevance
436    fn applicable(&self, lhs: &Term, rhs: &Term) -> bool {
437        Self::proof_for(lhs).is_some() && Self::proof_for(rhs).is_some()
438    }
439    fn apply<'t>(
440        &self,
441        mut checker: CheckRef<'t, '_, Split>,
442        lhs: &'t Term,
443        rhs: &'t Term,
444    ) -> Option<bool> {
445        let lhs = Self::proof_for(lhs)?;
446        let rhs = Self::proof_for(rhs)?;
447        Some(checker.check_equality(lhs, rhs) == Some(true))
448    }
449}
ftml_solver/rules/mod.rs

ftml_solver/rules/
mod.rs
