ftml_solver/rules/
extractors.rs

1use super::operators::*;
2use crate::{
3    rules::{RuleSet, SimplificationRule},
4    split::SplitStrategy,
5};
6use ftml_ontology::{
7    domain::declarations::symbols::{AssocType, Symbol},
8    terms::{
9        ApplicationTerm, Argument, BindingTerm, BoundArgument, ComponentVar, Term,
10        patterns::Pattern,
11    },
12};
13use ftml_solver_trace::SizedSolverRule;
14use ftml_uris::{Id, SymbolUri};
15
16pub type SymbolRuleExtractor<Split> = fn(&Symbol, &mut RuleSet<Split>);
17pub type RuleExtractor<Split> = (&'static str, fn(&[Term], &mut RuleSet<Split>));
18
19#[must_use]
20pub const fn all_symbol_extractors<Split: SplitStrategy>() -> &'static [SymbolRuleExtractor<Split>]
21{
22    &[
23        prenex,
24        binl,
25        binr,
26        conj,
27        pwconj,
28        reorder,
29        of_type,
30        apply,
31        lambda,
32        pi,
33        prop,
34        judgment,
35        universe,
36        inhabitable,
37        any,
38        implicit,
39        conjunction,
40        map,
41        letrule,
42        numnat,
43        numposnat,
44        numint,
45        numnegint,
46        numnonzeroint,
47        numrat,
48        numposrat,
49        numnegrat,
50        numnonzerorat,
51        numreal,
52        numposreal,
53        numnegreal,
54        numnonzeroreal,
55        numcomplex,
56        addition,
57        multiplication,
58        exponentiation,
59        division,
60        subtraction,
61        logarithm,
62        leq,
63        max,
64    ]
65}
66#[must_use]
67pub const fn all_rule_extractors<Split: SplitStrategy>() -> &'static [RuleExtractor<Split>] {
68    &[
69        ("hoas-lambda-pi-apply", hoas_lpa),
70        ("arrow-for-pi", arrow_for),
71        ("hoas-bindin", bind_in),
72        ("intersection-type", intersection),
73        ("inhabitable", inhab),
74        ("universe", univ),
75        ("subtype", subtp),
76        ("record-universe", record_universe),
77        ("forallEI", forall_ei),
78        ("complex", super::symbols::parse),
79    ]
80}
81
82macro_rules! rules {
83    (
84        $(
85            $v:vis $name:ident $( ($id:expr) )? = ($symbol:ident,$rules:ident) => $b:block
86        )*
87    ) => {
88        $( rules!(@I $v $name $(($id))? = ($symbol,$rules) => $b ); )*
89    };
90    (@I $v:vis $name:ident($id:expr) = ($symbol:ident,$rules:ident) => $b:block) => {
91        #[allow(unused_variables)]
92        $v fn $name<Split: SplitStrategy>($symbol:&Symbol,$rules:&mut RuleSet<Split>) {
93            static ID: std::sync::LazyLock<Id> =
94                std::sync::LazyLock::new(|| unsafe { $id.parse().unwrap_unchecked() });
95            if $symbol.data.role.contains(&ID) $b
96        }
97    };
98    (@I $v:vis $name:ident = ($symbol:ident,$rules:ident) => $b:block) => {
99        rules!(@I $v $name(stringify!($name)) = ($symbol,$rules) => $b);
100    }
101}
102
103pub fn subtp<Split: SplitStrategy>(params: &[Term], rules: &mut RuleSet<Split>) {
104    let [sub, sup] = params else { return };
105    rules.push_subtyping(Box::new(typing::Subtyping {
106        sub: Pattern::from(sub.clone(), false),
107        sup: Pattern::from(sup.clone(), false),
108    }));
109}
110
111pub fn forall_ei<Split: SplitStrategy>(params: &[Term], rules: &mut RuleSet<Split>) {
112    let [
113        Term::Symbol { uri: foral, .. },
114        Term::Symbol { uri: proof, .. },
115        Term::Symbol { uri: pi, .. },
116    ] = params
117    else {
118        return;
119    };
120    rules.push_simplification(Box::new(ForallSimp {
121        foral: foral.clone(),
122        proof: proof.clone(),
123        pi: pi.clone(),
124    }));
125}
126
127pub fn inhab<Split: SplitStrategy>(params: &[Term], rules: &mut RuleSet<Split>) {
128    let [term] = params else { return };
129    rules.push_inhabitable(Box::new(universe::ComplexInhabitableRule(Pattern::from(
130        term.clone(),
131        false,
132    ))));
133}
134
135pub fn record_universe<Split: SplitStrategy>(params: &[Term], rules: &mut RuleSet<Split>) {
136    let [term] = params else { return };
137    rules.push_inference(Box::new(crate::impls::records::RecordUniverse(
138        term.clone(),
139    )));
140}
141
142pub fn univ<Split: SplitStrategy>(params: &[Term], rules: &mut RuleSet<Split>) {
143    let [term] = params else {
144        //tracing::error!("Parameters don't match: {params:?}");
145        return;
146    };
147    let rl = universe::ComplexUniverseRule(Pattern::from(term.clone(), false));
148    //tracing::warn!("New universe rule: {rl:?}");
149    rules.push_inhabitable(Box::new(rl.clone()));
150    rules.push_universe(Box::new(rl));
151}
152
153pub fn intersection<Split: SplitStrategy>(params: &[Term], rules: &mut RuleSet<Split>) {
154    let [
155        Term::Symbol { uri: intersect, .. },
156        Term::Symbol { uri: lambda, .. },
157        Term::Symbol { uri: pi, .. },
158    ] = params
159    else {
160        return;
161    };
162    rules.push_inhabitable(Box::new(intersection::IntersectionTypeInhabitable(
163        intersect.clone(),
164    )));
165    rules.push_universe(Box::new(intersection::IntersectionTypeInhabitable(
166        intersect.clone(),
167    )));
168    rules.push_marker(Box::new(intersection::intersect_pi_extension(
169        intersect.clone(),
170        pi.clone(),
171    )));
172}
173
174pub fn bind_in<Split: SplitStrategy>(params: &[Term], rules: &mut RuleSet<Split>) {
175    let [
176        Term::Symbol { uri: bindin, .. },
177        Term::Symbol { uri: bind, .. },
178    ] = params
179    else {
180        return;
181    };
182    rules.push_inhabitable(Box::new(bindin::BindInInhabitableRule {
183        bindin: bindin.clone(),
184        bind: bind.clone(),
185    }));
186    rules.push_preparation(Box::new(pi::NeedsTypeRule(bindin.clone())));
187    rules.push_inference(Box::new(bindin::BindInInferenceRule {
188        bindin: bindin.clone(),
189        bind: bind.clone(),
190    }));
191    rules.push_inference(Box::new(bindin::BindInApplyRule {
192        bindin: bindin.clone(),
193        bind: bind.clone(),
194    }));
195    rules.push_simplification(Box::new(bindin::BindInComputationRule {
196        bindin: bindin.clone(),
197        bind: bind.clone(),
198    }));
199}
200
201pub fn arrow_for<Split: SplitStrategy>(params: &[Term], rules: &mut RuleSet<Split>) {
202    if let [Term::Symbol { uri: head, .. }, Term::Symbol { uri: pi, .. }] = params {
203        let rule = Box::new(pi::ArrowRule {
204            arrow: head.clone(),
205            pi: pi.clone(),
206        });
207        rules.push_preparation(rule.clone());
208        rules.push_simplification(rule);
209    }
210}
211
212pub fn hoas_lpa<Split: SplitStrategy>(params: &[Term], rules: &mut RuleSet<Split>) {
213    let (lambda, pi, apply) = if let [
214        Term::Symbol { uri: lambda, .. },
215        Term::Symbol { uri: pi, .. },
216        Term::Symbol { uri: apply, .. },
217    ] = params
218    {
219        (lambda, pi, Some(apply))
220    } else if let [
221        Term::Symbol { uri: lambda, .. },
222        Term::Symbol { uri: pi, .. },
223    ] = params
224    {
225        (lambda, pi, None)
226    } else {
227        return;
228    };
229    rules.push_inhabitable(Box::new(pi::PiInhabitableRule(pi.clone())));
230    rules.push_universe(Box::new(pi::PiUniverseRule(pi.clone())));
231    rules.push_inference(Box::new(pi::PiInferenceRule(pi.clone())));
232    rules.push_subtyping(Box::new(pi::PiVarianceRule(pi.clone())));
233    rules.push_inference(Box::new(pi::LambdaPiInferenceRule {
234        lambda: lambda.clone(),
235        pi: pi.clone(),
236    }));
237    rules.push_checking(Box::new(pi::LambdaPiCheckingRule {
238        lambda: lambda.clone(),
239        pi: pi.clone(),
240    }));
241    rules.push_simplification(Box::new(pi::BetaRule(lambda.clone())));
242    rules.push_simplification(Box::new(pi::EtaRule(lambda.clone())));
243    rules.push_preparation(Box::new(pi::NeedsTypeRule(lambda.clone())));
244    if lambda != pi {
245        rules.push_preparation(Box::new(pi::NeedsTypeRule(pi.clone())));
246    }
247    rules.push_marker(Box::new(super::HOASRule {
248        lambda: lambda.clone(),
249        pi: pi.clone(),
250        apply: apply.cloned(),
251    }));
252}
253
254pub fn reorder<Split: SplitStrategy>(sym: &Symbol, rules: &mut RuleSet<Split>) {
255    if let Some(perm) = &sym.data.reordering {
256        rules.push_preparation(Box::new(super::fixity::ReorderRule {
257            symbol: sym.uri.clone(),
258            reorder: perm.clone(),
259        }));
260    }
261}
262
263pub fn prenex<Split: SplitStrategy>(sym: &Symbol, rules: &mut RuleSet<Split>) {
264    if sym.data.assoctype.is_some_and(|at| at == AssocType::Prenex) {
265        rules.push_preparation(Box::new(super::fixity::PrenexRule(sym.uri.clone())));
266    }
267}
268
269pub fn conj<Split: SplitStrategy>(sym: &Symbol, rules: &mut RuleSet<Split>) {
270    if sym
271        .data
272        .assoctype
273        .is_some_and(|at| at == AssocType::Conjunctive)
274    {
275        rules.push_preparation(Box::new(super::fixity::ConjunctiveRule(sym.uri.clone())));
276    }
277}
278
279pub fn pwconj<Split: SplitStrategy>(sym: &Symbol, rules: &mut RuleSet<Split>) {
280    if sym
281        .data
282        .assoctype
283        .is_some_and(|at| at == AssocType::PairwiseConjunctive)
284    {
285        rules.push_preparation(Box::new(super::fixity::PairwiseConjunctiveRule(
286            sym.uri.clone(),
287        )));
288    }
289}
290
291pub fn binl<Split: SplitStrategy>(sym: &Symbol, rules: &mut RuleSet<Split>) {
292    if sym
293        .data
294        .assoctype
295        .is_some_and(|at| at == AssocType::LeftAssociativeBinary)
296    {
297        rules.push_preparation(Box::new(super::fixity::BinLRule(sym.uri.clone())));
298    }
299}
300
301pub fn binr<Split: SplitStrategy>(sym: &Symbol, rules: &mut RuleSet<Split>) {
302    if sym
303        .data
304        .assoctype
305        .is_some_and(|at| at == AssocType::RightAssociativeBinary)
306    {
307        rules.push_preparation(Box::new(super::fixity::BinRRule(sym.uri.clone())));
308    }
309}
310
311rules! {
312    pub conjunction = (sym,rules) => {
313        rules.push_marker(Box::new(super::fixity::IsConjunctionRule(sym.uri.clone())));
314    }
315    pub universe = (sym,rules) => {
316        rules.push_inhabitable(Box::new(universe::SimpleUniverseRule(sym.uri.clone())));
317        rules.push_universe(Box::new(universe::SimpleUniverseRule(sym.uri.clone())));
318    }
319    pub of_type("oftype") = (sym,rules) => {
320        rules.push_preparation(Box::new(typing::SimpleTypeOperatorRule(sym.uri.clone())));
321        rules.push_inference(Box::new(typing::SimpleTypeOperatorRule(sym.uri.clone())));
322        rules.push_simplification(Box::new(typing::SimpleTypeOperatorRule(sym.uri.clone())));
323    }
324    pub apply = (sym,rules) => {
325        rules.push_preparation(Box::new(pi::ApplyRule(sym.uri.clone())));
326    }
327    pub lambda = (sym,rules) => {
328
329    }
330    pub pi = (sym,rules) => {
331        rules.push_inhabitable(Box::new(pi::PiInhabitableRule(sym.uri.clone())));
332        rules.push_inference(Box::new(pi::PiInferenceRule(sym.uri.clone())));
333    }
334    pub prop = (sym,rules) => {
335
336    }
337    pub judgment = (sym,rules) => {
338        rules.push_marker(Box::new(super::IsJudgmentRule(sym.uri.clone())));
339    }
340    pub inhabitable = (sym,rules) => {
341        rules.push_inhabitable(Box::new(universe::SimpleInhabitableRule(sym.uri.clone(),sym.data.arity.num())));
342    }
343    pub any = (sym,rules) => {
344        rules.push_inhabitable(Box::new(universe::SimpleInhabitableRule(sym.uri.clone(),0)));
345        rules.push_subtyping(Box::new(universe::AnyRule(sym.uri.clone())));
346        rules.push_checking(Box::new(universe::AnyRule(sym.uri.clone())));
347        rules.push_marker(Box::new(universe::AnyRule(sym.uri.clone())));
348    }
349    pub implicit = (sym,rules) => {
350
351    }
352    pub map = (sym,rules) => {
353        rules.push_inhabitable(Box::new(super::sequences::map::MapInhabitableRule(sym.uri.clone())));
354        rules.push_simplification(Box::new(super::sequences::map::MapSimplificationRule(sym.uri.clone())));
355        rules.push_simplification(Box::new(super::sequences::map::MapArgumentSimplificationRule(sym.uri.clone())));
356        rules.push_simplification(Box::new(super::sequences::map::MapIndexSimplificationRule(sym.uri.clone())));
357        rules.push_inference(Box::new(super::sequences::map::MapInferenceRule(sym.uri.clone())));
358    }
359    pub letrule("let") = (sym,rules) => {
360        rules.push_simplification(Box::new(letin::LetinComputation(sym.uri.clone())));
361    }
362
363    pub numnat = (sym,rules) => {
364        rules.push_marker(Box::new(numbers::NumberRule{
365            typ:numbers::NumberType::Naturals,
366            sym:sym.uri.clone()
367        }));
368    }
369    pub numposnat = (sym,rules) => {
370        rules.push_marker(Box::new(numbers::NumberRule{
371            typ: numbers::NumberType::PositiveNaturals,
372            sym:sym.uri.clone()
373        }));
374    }
375    pub numint = (sym,rules) => {
376        rules.push_marker(Box::new(numbers::NumberRule{
377            typ:numbers::NumberType::Integers,
378            sym:sym.uri.clone()
379        }));
380    }
381    pub numnegint = (sym,rules) => {
382        rules.push_marker(Box::new(numbers::NumberRule{
383            typ:numbers::NumberType::NegativeIntegers,
384            sym:sym.uri.clone()
385        }));
386    }
387    pub numnonzeroint = (sym,rules) => {
388        rules.push_marker(Box::new(numbers::NumberRule{
389            typ:numbers::NumberType::NonZeroIntegers,
390            sym:sym.uri.clone()
391        }));
392    }
393    pub numrat = (sym,rules) => {
394        rules.push_marker(Box::new(numbers::NumberRule{
395            typ:numbers::NumberType::Rationals,
396            sym:sym.uri.clone()
397        }));
398    }
399    pub numposrat = (sym,rules) => {
400        rules.push_marker(Box::new(numbers::NumberRule{
401            typ:numbers::NumberType::PositiveRationals,
402            sym:sym.uri.clone()
403        }));
404    }
405    pub numnegrat = (sym,rules) => {
406        rules.push_marker(Box::new(numbers::NumberRule{
407            typ:numbers::NumberType::NegativeRationals,
408            sym:sym.uri.clone()
409        }));
410    }
411    pub numnonzerorat = (sym,rules) => {
412        rules.push_marker(Box::new(numbers::NumberRule{
413            typ:numbers::NumberType::NonZeroRationals,
414            sym:sym.uri.clone()
415        }));
416    }
417    pub numreal = (sym,rules) => {
418        rules.push_marker(Box::new(numbers::NumberRule{
419            typ:numbers::NumberType::Reals,
420            sym:sym.uri.clone()
421        }));
422    }
423    pub numposreal = (sym,rules) => {
424        rules.push_marker(Box::new(numbers::NumberRule{
425            typ:numbers::NumberType::PositiveReals,
426            sym:sym.uri.clone()
427        }));
428    }
429    pub numnegreal = (sym,rules) => {
430        rules.push_marker(Box::new(numbers::NumberRule{
431            typ:numbers::NumberType::NegativeReals,
432            sym:sym.uri.clone()
433        }));
434    }
435    pub numnonzeroreal = (sym,rules) => {
436        rules.push_marker(Box::new(numbers::NumberRule{
437            typ:numbers::NumberType::NonZeroReals,
438            sym:sym.uri.clone()
439        }));
440    }
441    pub numcomplex = (sym,rules) => {
442        rules.push_marker(Box::new(numbers::NumberRule{
443            typ:numbers::NumberType::Complex,
444            sym:sym.uri.clone()
445        }));
446    }
447    pub addition = (sym,rules) => {
448        rules.push_simplification(Box::new(numbers::AdditionRule(sym.uri.clone())));
449    }
450    pub multiplication = (sym,rules) => {
451        rules.push_simplification(Box::new(numbers::MultiplicationRule(sym.uri.clone())));
452    }
453    pub division = (sym,rules) => {
454        rules.push_simplification(Box::new(numbers::DivisionRule(sym.uri.clone())));
455    }
456    pub exponentiation = (sym,rules) => {
457        rules.push_simplification(Box::new(numbers::ExponentiationRule(sym.uri.clone())));
458    }
459    pub subtraction = (sym,rules) => {
460        rules.push_simplification(Box::new(numbers::SubtractionRule(sym.uri.clone())));
461    }
462    pub logarithm = (sym,rules) => {
463        rules.push_simplification(Box::new(numbers::Logarithm(sym.uri.clone())));
464    }
465    pub leq = (sym,rules) => {
466        rules.push_proof(Box::new(numbers::LessThan(sym.uri.clone())));
467    }
468    pub max = (sym,rules) => {
469        rules.push_simplification(Box::new(numbers::Max(sym.uri.clone())));
470    }
471}
472
473#[derive(Debug, Clone, PartialEq, Eq)]
474struct ForallSimp {
475    foral: SymbolUri,
476    proof: SymbolUri,
477    pi: SymbolUri,
478}
479impl SizedSolverRule for ForallSimp {
480    fn display(&self) -> Vec<crate::trace::Displayable> {
481        ftml_solver_trace::trace!(
482            &self.proof,
483            "(",
484            &self.foral,
485            " x:T. P)  ==>  ",
486            &self.pi,
487            " x:T. ",
488            &self.proof,
489            " P"
490        )
491    }
492}
493impl<Split: SplitStrategy> SimplificationRule<Split> for ForallSimp {
494    fn applicable(&self, term: &Term) -> bool {
495        if let Term::Application(app) = term
496            && let Term::Symbol { uri, .. } = &app.head
497            && *uri == self.proof
498            && let [Argument::Simple(Term::Bound(forall))] = &*app.arguments
499            && let Term::Symbol { uri, .. } = &forall.head
500            && *uri == self.foral
501            && let [
502                BoundArgument::Simple(_), // tp
503                BoundArgument::Bound(_),
504                BoundArgument::Simple(_),
505            ] = &*forall.arguments
506        {
507            true
508        } else {
509            false
510        }
511    }
512    fn apply<'t>(
513        &self,
514        mut checker: crate::CheckRef<'t, '_, Split>,
515        term: &'t Term,
516    ) -> Result<Term, Option<ftml_ontology::terms::termpaths::TermPath>> {
517        if let Term::Application(app) = term
518            && let Term::Symbol { uri, .. } = &app.head
519            && *uri == self.proof
520            && let [Argument::Simple(Term::Bound(forall))] = &*app.arguments
521            && let Term::Symbol { uri, .. } = &forall.head
522            && *uri == self.foral
523            && let [
524                BoundArgument::Simple(tp),
525                BoundArgument::Bound(v),
526                BoundArgument::Simple(bd),
527            ] = &*forall.arguments
528        {
529            if let Some(otp) = &v.tp
530                && checker.check_equality(tp, otp) != Some(true)
531            {
532                return Err(None);
533            }
534
535            Ok(Term::Bound(BindingTerm::new(
536                self.pi.clone().into(),
537                Box::new([
538                    BoundArgument::Bound(ComponentVar {
539                        var: v.var.clone(),
540                        tp: Some(tp.clone()),
541                        df: None,
542                    }),
543                    BoundArgument::Simple(Term::Application(ApplicationTerm::new(
544                        self.proof.clone().into(),
545                        Box::new([Argument::Simple(bd.clone())]),
546                        None,
547                    ))),
548                ]),
549                None,
550            )))
551        } else {
552            Err(None)
553        }
554    }
555}
ftml_solver/rules/extractors.rs

ftml_solver/rules/
extractors.rs
