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::terms::{Argument, Term, termpaths::TermPath};
13use std::{fmt::Debug, ops::ControlFlow};
14
15macro_rules! rules{
16    ($($name:ident = $tp:ident $(($($e:expr),* $(,)?))? ),*$(,)?) => {
17        #[derive(Debug)]
18        pub struct RuleSet<Split: SplitStrategy> {
19            $(
20                $name:Vec<Box<dyn $tp<Split>>>
21            ),*
22        }
23
24        paste::paste!{
25            $(
26            trait [< ClonableDyn $tp>]<Split:SplitStrategy>:$tp<Split> {
27                fn [<to_dyn_ $name>](&self) -> Box<dyn $tp<Split>>;
28            }
29            impl<Split:SplitStrategy,T:$tp<Split>+Sized+Clone> [< ClonableDyn $tp>]<Split> for T {
30                fn [<to_dyn_ $name>](&self) -> Box<dyn $tp<Split>> {
31                    Box::new(self.clone()) as _
32                }
33            }
34            )*
35        }
36
37
38        impl<Split:SplitStrategy> Default for RuleSet<Split> {
39            paste::paste!{
40                fn default() -> Self {
41                    Self {
42                        $(
43                            $name: Self::[<DEFAULT_ $name:snake:upper >].iter().map(|r| r.[<to_dyn_ $name>]()).collect()
44                        ),*
45                    }
46                }
47            }
48        }
49
50        impl<Split: SplitStrategy> RuleSet<Split> {
51            paste::paste!{
52                $(
53
54                    const [<DEFAULT_ $name:snake:upper >] : &[&dyn [< ClonableDyn $tp>]<Split>] = &[
55                        $($(
56                            &$e as _
57                        ),*)?
58                    ];
59
60                    pub fn [<push_ $name>](&mut self,rule:Box<dyn $tp<Split>>) {
61                        if !self.$name.iter().any(|v| v.eq(&*rule)) {
62                            let i = self
63                                .$name
64                                .binary_search_by_key(&(-rule.priority()), |e| -e.priority())
65                                .map_or_else(|i| i, |i| i);
66                            self.$name.insert(i, rule);
67                        }
68                    }
69                    #[inline]
70                    #[must_use]
71                    pub fn $name(&self) -> &[Box<dyn $tp<Split>>] {
72                        &self.$name
73                    }
74                )*
75            }
76        }
77    }
78}
79
80rules! {
81    inference = InferenceRule(
82        sequences::SeqIndexRule,
83        sequences::SeqInferenceRule,
84        sequences::fold::FoldInferenceRule,
85        sequences::SeqConcatInferenceRule,
86        operators::numbers::NumberTypes,
87        implicits::ImplicitRule,
88        unknowns::UnknownsRule,
89        CommentRule
90    ),
91    subtyping = SubtypeRule(operators::numbers::NumberTypes,CommentRule),
92    checking = CheckingRule(operators::numbers::NumberTypes),
93    inhabitable = InhabitableRule(sequences::SeqUniverseRule,CommentRule),
94    equality = EqualityRule(
95        operators::numbers::NumberTypes,
96        CommentRule
97        //sequences::SeqTypeEqRule
98    ),
99    universe = UniverseRule(sequences::SeqUniverseRule,CommentRule),
100    preparation = PreparationRule,
101    simplification = SimplificationRule(
102        unknowns::UnknownsRule,
103        typing::InferredTypeSimplificationRule,
104        CommentRule
105    ),
106    marker = MarkerRule,
107    proof = ProofRule
108}
109
110pub trait SimplificationRule<Split: SplitStrategy>: CheckerRule {
111    fn applicable(&self, term: &Term) -> bool;
112    fn apply<'t>(
113        &self,
114        checker: CheckRef<'t, '_, Split>,
115        term: &'t Term,
116    ) -> Result<Term, Option<TermPath>>;
117}
118
119pub trait EqualityRule<Split: SplitStrategy>: CheckerRule {
120    fn applicable(&self, lhs: &Term, rhs: &Term) -> bool;
121    fn apply<'t>(
122        &self,
123        checker: CheckRef<'t, '_, Split>,
124        lhs: &'t Term,
125        rhs: &'t Term,
126    ) -> Option<bool>;
127}
128
129pub trait InferenceRule<Split: SplitStrategy>: CheckerRule {
130    fn applicable(&self, term: &Term) -> bool;
131    fn infer<'t>(&self, checker: CheckRef<'t, '_, Split>, term: &'t Term) -> Option<Term>;
132}
133
134pub trait CheckingRule<Split: SplitStrategy>: CheckerRule {
135    fn applicable(&self, checker: &CheckRef<'_, '_, Split>, term: &Term, tp: &Term) -> bool;
136    fn apply<'t>(
137        &self,
138        checker: CheckRef<'t, '_, Split>,
139        term: &'t Term,
140        tp: &'t Term,
141    ) -> Option<bool>;
142}
143
144pub trait InhabitableRule<Split: SplitStrategy>: CheckerRule {
145    fn applicable(&self, term: &Term) -> bool;
146    fn apply<'t>(&self, checker: CheckRef<'t, '_, Split>, term: &'t Term) -> Option<bool>;
147}
148
149pub trait UniverseRule<Split: SplitStrategy>: CheckerRule {
150    fn applicable(&self, term: &Term) -> bool;
151    fn apply<'t>(&self, checker: CheckRef<'t, '_, Split>, term: &'t Term) -> Option<bool>;
152}
153
154pub trait SubtypeRule<Split: SplitStrategy>: CheckerRule {
155    fn applicable(&self, checker: &CheckRef<'_, '_, Split>, sub: &Term, sup: &Term) -> bool;
156    fn apply<'t>(
157        &self,
158        checker: CheckRef<'t, '_, Split>,
159        sub: &'t Term,
160        sup: &'t Term,
161    ) -> Option<bool>;
162}
163
164pub trait PreparationRule<Split: SplitStrategy>: CheckerRule {
165    fn applicable(&self, checker: &CheckRef<'_, '_, Split>, t: &Term) -> bool;
166    fn apply(
167        &self,
168        checker: &mut CheckRef<'_, '_, Split>,
169        t: Term,
170        path: Option<(&mut smallvec::SmallVec<u8, 16>, usize)>,
171    ) -> ControlFlow<Term, Term>;
172    fn applicable_revert(&self, checker: &CheckRef<'_, '_, Split>, t: &Term) -> bool;
173    fn revert(&self, checker: &CheckRef<'_, '_, Split>, t: Term) -> ControlFlow<Term, Term>;
174}
175pub trait MarkerRule<Split: SplitStrategy>: CheckerRule {}
176
177pub trait ProofRule<Split: SplitStrategy>: CheckerRule {
178    fn applicable(&self, term: &Term) -> bool;
179    fn prove<'t>(&self, checker: CheckRef<'t, '_, Split>, goal: &'t Term) -> Option<Term>;
180}
181
182#[derive(Debug, Clone, PartialEq, Eq)]
183pub struct IsJudgmentRule(pub SymbolUri);
184impl SizedSolverRule for IsJudgmentRule {
185    fn display(&self) -> Vec<crate::trace::Displayable> {
186        ftml_solver_trace::trace!(&self.0, "is a judgment")
187    }
188}
189impl<Split: SplitStrategy> MarkerRule<Split> for IsJudgmentRule {}
190
191#[derive(Debug, Clone, PartialEq, Eq)]
192pub struct HOASRule {
193    pub lambda: SymbolUri,
194    pub pi: SymbolUri,
195    pub apply: Option<SymbolUri>,
196}
197impl SizedSolverRule for HOASRule {
198    fn display(&self) -> Vec<crate::trace::Displayable> {
199        ftml_solver_trace::trace!("HOAS using ", &self.lambda, " and ", &self.pi)
200    }
201}
202impl<Split: SplitStrategy> MarkerRule<Split> for HOASRule {}
203
204#[derive(Debug, Clone, Copy, PartialEq, Eq)]
205struct CommentRule;
206impl SizedSolverRule for CommentRule {
207    fn display(&self) -> Vec<crate::trace::Displayable> {
208        ftml_solver_trace::trace!("comment")
209    }
210    fn priority(&self) -> isize {
211        1_000_000
212    }
213}
214
215fn as_comment(term: &Term) -> Option<&Term> {
216    if let Term::Application(app) = term
217        && app.head.is(&*ftml_uris::metatheory::COMMENTED)
218        && let [Argument::Simple(r), Argument::Simple(_)] = &*app.arguments
219    {
220        Some(r)
221    } else {
222        None
223    }
224}
225
226impl<Split: SplitStrategy> SimplificationRule<Split> for CommentRule {
227    fn applicable(&self, term: &Term) -> bool {
228        as_comment(term).is_some()
229    }
230    fn apply<'t>(
231        &self,
232        _: CheckRef<'t, '_, Split>,
233        term: &'t Term,
234    ) -> Result<Term, Option<TermPath>> {
235        as_comment(term).cloned().ok_or(None)
236    }
237}
238
239impl<Split: SplitStrategy> InferenceRule<Split> for CommentRule {
240    fn applicable(&self, term: &Term) -> bool {
241        as_comment(term).is_some()
242    }
243    fn infer<'t>(&self, mut checker: CheckRef<'t, '_, Split>, term: &'t Term) -> Option<Term> {
244        as_comment(term).and_then(|t| checker.infer_type(t))
245    }
246}
247
248impl<Split: SplitStrategy> InhabitableRule<Split> for CommentRule {
249    fn applicable(&self, term: &Term) -> bool {
250        as_comment(term).is_some()
251    }
252    fn apply<'t>(&self, mut checker: CheckRef<'t, '_, Split>, term: &'t Term) -> Option<bool> {
253        as_comment(term).and_then(|t| checker.check_inhabitable(t))
254    }
255}
256
257impl<Split: SplitStrategy> UniverseRule<Split> for CommentRule {
258    fn applicable(&self, term: &Term) -> bool {
259        as_comment(term).is_some()
260    }
261    fn apply<'t>(&self, mut checker: CheckRef<'t, '_, Split>, term: &'t Term) -> Option<bool> {
262        as_comment(term).and_then(|t| checker.check_universe(t))
263    }
264}
265impl<Split: SplitStrategy> SubtypeRule<Split> for CommentRule {
266    fn applicable(&self, _: &CheckRef<'_, '_, Split>, sub: &Term, sup: &Term) -> bool {
267        as_comment(sub).is_some() || as_comment(sup).is_some()
268    }
269    fn apply<'t>(
270        &self,
271        mut checker: CheckRef<'t, '_, Split>,
272        sub: &'t Term,
273        sup: &'t Term,
274    ) -> Option<bool> {
275        // one of them is different, because .applicable()
276        let sub = as_comment(sub).unwrap_or(sub);
277        let sup = as_comment(sup).unwrap_or(sup);
278        checker.check_subtype(sub, sup)
279    }
280}
281
282impl<Split: SplitStrategy> EqualityRule<Split> for CommentRule {
283    fn applicable(&self, lhs: &Term, rhs: &Term) -> bool {
284        as_comment(lhs).is_some() || as_comment(rhs).is_some()
285    }
286    fn apply<'t>(
287        &self,
288        mut checker: CheckRef<'t, '_, Split>,
289        lhs: &'t Term,
290        rhs: &'t Term,
291    ) -> Option<bool> {
292        // one of them is different, because .applicable()
293        let lhs = as_comment(lhs).unwrap_or(lhs);
294        let rhs = as_comment(rhs).unwrap_or(rhs);
295        checker.check_subtype(lhs, rhs)
296    }
297}
ftml_solver/rules/mod.rs

ftml_solver/rules/
mod.rs
