ftml_solver/rules/
extractors.rs

1use super::operators::*;
2use crate::{rules::RuleSet, split::SplitStrategy};
3use ftml_ontology::{
4    domain::declarations::symbols::{AssocType, Symbol},
5    terms::{Term, patterns::Pattern},
6};
7use ftml_uris::Id;
8
9pub type SymbolRuleExtractor<Split> = fn(&Symbol, &mut RuleSet<Split>);
10pub type RuleExtractor<Split> = (&'static str, fn(&[Term], &mut RuleSet<Split>));
11
12#[must_use]
13pub const fn all_symbol_extractors<Split: SplitStrategy>() -> &'static [SymbolRuleExtractor<Split>]
14{
15    &[
16        prenex,
17        binl,
18        binr,
19        conj,
20        pwconj,
21        reorder,
22        of_type,
23        apply,
24        lambda,
25        pi,
26        prop,
27        judgment,
28        universe,
29        inhabitable,
30        any,
31        implicit,
32        conjunction,
33        map,
34        letrule,
35        numnat,
36        numposnat,
37        numint,
38        numnegint,
39        numnonzeroint,
40        numrat,
41        numposrat,
42        numnegrat,
43        numnonzerorat,
44        numreal,
45        numposreal,
46        numnegreal,
47        numnonzeroreal,
48        numcomplex,
49        addition,
50        multiplication,
51        exponentiation,
52        division,
53        subtraction,
54        logarithm,
55        leq,
56        max,
57    ]
58}
59#[must_use]
60pub const fn all_rule_extractors<Split: SplitStrategy>() -> &'static [RuleExtractor<Split>] {
61    &[
62        ("hoas-lambda-pi-apply", hoas_lpa),
63        ("arrow-for-pi", arrow_for),
64        ("hoas-bindin", bind_in),
65        ("intersection-type", intersection),
66        ("inhabitable", inhab),
67        ("universe", univ),
68        ("subtype", subtp),
69        ("complex", super::symbols::parse),
70    ]
71}
72
73macro_rules! rules {
74    (
75        $(
76            $v:vis $name:ident $( ($id:expr) )? = ($symbol:ident,$rules:ident) => $b:block
77        )*
78    ) => {
79        $( rules!(@I $v $name $(($id))? = ($symbol,$rules) => $b ); )*
80    };
81    (@I $v:vis $name:ident($id:expr) = ($symbol:ident,$rules:ident) => $b:block) => {
82        #[allow(unused_variables)]
83        $v fn $name<Split: SplitStrategy>($symbol:&Symbol,$rules:&mut RuleSet<Split>) {
84            static ID: std::sync::LazyLock<Id> =
85                std::sync::LazyLock::new(|| unsafe { $id.parse().unwrap_unchecked() });
86            if $symbol.data.role.contains(&ID) $b
87        }
88    };
89    (@I $v:vis $name:ident = ($symbol:ident,$rules:ident) => $b:block) => {
90        rules!(@I $v $name(stringify!($name)) = ($symbol,$rules) => $b);
91    }
92}
93
94pub fn subtp<Split: SplitStrategy>(params: &[Term], rules: &mut RuleSet<Split>) {
95    let [sub, sup] = params else { return };
96    rules.push_subtyping(Box::new(typing::Subtyping {
97        sub: Pattern::from(sub.clone(), false),
98        sup: Pattern::from(sup.clone(), false),
99    }));
100}
101
102pub fn inhab<Split: SplitStrategy>(params: &[Term], rules: &mut RuleSet<Split>) {
103    let [term] = params else { return };
104    rules.push_inhabitable(Box::new(universe::ComplexInhabitableRule(Pattern::from(
105        term.clone(),
106        false,
107    ))));
108}
109
110pub fn univ<Split: SplitStrategy>(params: &[Term], rules: &mut RuleSet<Split>) {
111    let [term] = params else {
112        //tracing::error!("Parameters don't match: {params:?}");
113        return;
114    };
115    let rl = universe::ComplexUniverseRule(Pattern::from(term.clone(), false));
116    //tracing::warn!("New universe rule: {rl:?}");
117    rules.push_inhabitable(Box::new(rl.clone()));
118    rules.push_universe(Box::new(rl));
119}
120
121pub fn intersection<Split: SplitStrategy>(params: &[Term], rules: &mut RuleSet<Split>) {
122    let [
123        Term::Symbol { uri: intersect, .. },
124        Term::Symbol { uri: lambda, .. },
125        Term::Symbol { uri: pi, .. },
126    ] = params
127    else {
128        return;
129    };
130    rules.push_inhabitable(Box::new(intersection::IntersectionTypeInhabitable(
131        intersect.clone(),
132    )));
133    rules.push_universe(Box::new(intersection::IntersectionTypeInhabitable(
134        intersect.clone(),
135    )));
136    rules.push_marker(Box::new(intersection::intersect_pi_extension(
137        intersect.clone(),
138        pi.clone(),
139    )));
140}
141
142pub fn bind_in<Split: SplitStrategy>(params: &[Term], rules: &mut RuleSet<Split>) {
143    let [
144        Term::Symbol { uri: bindin, .. },
145        Term::Symbol { uri: bind, .. },
146    ] = params
147    else {
148        return;
149    };
150    rules.push_inhabitable(Box::new(bindin::BindInInhabitableRule {
151        bindin: bindin.clone(),
152        bind: bind.clone(),
153    }));
154    rules.push_preparation(Box::new(pi::NeedsTypeRule(bindin.clone())));
155    rules.push_inference(Box::new(bindin::BindInInferenceRule {
156        bindin: bindin.clone(),
157        bind: bind.clone(),
158    }));
159    rules.push_inference(Box::new(bindin::BindInApplyRule {
160        bindin: bindin.clone(),
161        bind: bind.clone(),
162    }));
163    rules.push_simplification(Box::new(bindin::BindInComputationRule {
164        bindin: bindin.clone(),
165        bind: bind.clone(),
166    }));
167}
168
169pub fn arrow_for<Split: SplitStrategy>(params: &[Term], rules: &mut RuleSet<Split>) {
170    if let [Term::Symbol { uri: head, .. }, Term::Symbol { uri: pi, .. }] = params {
171        let rule = Box::new(pi::ArrowRule {
172            arrow: head.clone(),
173            pi: pi.clone(),
174        });
175        rules.push_preparation(rule.clone());
176        rules.push_simplification(rule);
177    }
178}
179
180pub fn hoas_lpa<Split: SplitStrategy>(params: &[Term], rules: &mut RuleSet<Split>) {
181    let (lambda, pi, apply) = if let [
182        Term::Symbol { uri: lambda, .. },
183        Term::Symbol { uri: pi, .. },
184        Term::Symbol { uri: apply, .. },
185    ] = params
186    {
187        (lambda, pi, Some(apply))
188    } else if let [
189        Term::Symbol { uri: lambda, .. },
190        Term::Symbol { uri: pi, .. },
191    ] = params
192    {
193        (lambda, pi, None)
194    } else {
195        return;
196    };
197    rules.push_inhabitable(Box::new(pi::PiInhabitableRule(pi.clone())));
198    rules.push_universe(Box::new(pi::PiUniverseRule(pi.clone())));
199    rules.push_inference(Box::new(pi::PiInferenceRule(pi.clone())));
200    rules.push_subtyping(Box::new(pi::PiVarianceRule(pi.clone())));
201    rules.push_inference(Box::new(pi::LambdaPiInferenceRule {
202        lambda: lambda.clone(),
203        pi: pi.clone(),
204    }));
205    rules.push_checking(Box::new(pi::LambdaPiCheckingRule {
206        lambda: lambda.clone(),
207        pi: pi.clone(),
208    }));
209    rules.push_simplification(Box::new(pi::BetaRule(lambda.clone())));
210    rules.push_preparation(Box::new(pi::NeedsTypeRule(lambda.clone())));
211    if lambda != pi {
212        rules.push_preparation(Box::new(pi::NeedsTypeRule(pi.clone())));
213    }
214    rules.push_marker(Box::new(super::HOASRule {
215        lambda: lambda.clone(),
216        pi: pi.clone(),
217        apply: apply.cloned(),
218    }));
219}
220
221pub fn reorder<Split: SplitStrategy>(sym: &Symbol, rules: &mut RuleSet<Split>) {
222    if let Some(perm) = &sym.data.reordering {
223        rules.push_preparation(Box::new(super::fixity::ReorderRule {
224            symbol: sym.uri.clone(),
225            reorder: perm.clone(),
226        }));
227    }
228}
229
230pub fn prenex<Split: SplitStrategy>(sym: &Symbol, rules: &mut RuleSet<Split>) {
231    if sym.data.assoctype.is_some_and(|at| at == AssocType::Prenex) {
232        rules.push_preparation(Box::new(super::fixity::PrenexRule(sym.uri.clone())));
233    }
234}
235
236pub fn conj<Split: SplitStrategy>(sym: &Symbol, rules: &mut RuleSet<Split>) {
237    if sym
238        .data
239        .assoctype
240        .is_some_and(|at| at == AssocType::Conjunctive)
241    {
242        rules.push_preparation(Box::new(super::fixity::ConjunctiveRule(sym.uri.clone())));
243    }
244}
245
246pub fn pwconj<Split: SplitStrategy>(sym: &Symbol, rules: &mut RuleSet<Split>) {
247    if sym
248        .data
249        .assoctype
250        .is_some_and(|at| at == AssocType::PairwiseConjunctive)
251    {
252        rules.push_preparation(Box::new(super::fixity::PairwiseConjunctiveRule(
253            sym.uri.clone(),
254        )));
255    }
256}
257
258pub fn binl<Split: SplitStrategy>(sym: &Symbol, rules: &mut RuleSet<Split>) {
259    if sym
260        .data
261        .assoctype
262        .is_some_and(|at| at == AssocType::LeftAssociativeBinary)
263    {
264        rules.push_preparation(Box::new(super::fixity::BinLRule(sym.uri.clone())));
265    }
266}
267
268pub fn binr<Split: SplitStrategy>(sym: &Symbol, rules: &mut RuleSet<Split>) {
269    if sym
270        .data
271        .assoctype
272        .is_some_and(|at| at == AssocType::RightAssociativeBinary)
273    {
274        rules.push_preparation(Box::new(super::fixity::BinRRule(sym.uri.clone())));
275    }
276}
277
278rules! {
279    pub conjunction = (sym,rules) => {
280        rules.push_marker(Box::new(super::fixity::IsConjunctionRule(sym.uri.clone())));
281    }
282    pub universe = (sym,rules) => {
283        rules.push_inhabitable(Box::new(universe::SimpleUniverseRule(sym.uri.clone())));
284        rules.push_universe(Box::new(universe::SimpleUniverseRule(sym.uri.clone())));
285    }
286    pub of_type("oftype") = (sym,rules) => {
287        rules.push_preparation(Box::new(typing::SimpleTypeOperatorRule(sym.uri.clone())));
288    }
289    pub apply = (sym,rules) => {
290        rules.push_preparation(Box::new(pi::ApplyRule(sym.uri.clone())));
291    }
292    pub lambda = (sym,rules) => {
293
294    }
295    pub pi = (sym,rules) => {
296        rules.push_inhabitable(Box::new(pi::PiInhabitableRule(sym.uri.clone())));
297        rules.push_inference(Box::new(pi::PiInferenceRule(sym.uri.clone())));
298    }
299    pub prop = (sym,rules) => {
300
301    }
302    pub judgment = (sym,rules) => {
303        rules.push_marker(Box::new(super::IsJudgmentRule(sym.uri.clone())));
304    }
305    pub inhabitable = (sym,rules) => {
306        rules.push_inhabitable(Box::new(universe::SimpleInhabitableRule(sym.uri.clone(),sym.data.arity.num())));
307    }
308    pub any = (sym,rules) => {
309        rules.push_inhabitable(Box::new(universe::SimpleInhabitableRule(sym.uri.clone(),0)));
310        rules.push_subtyping(Box::new(universe::AnyRule(sym.uri.clone())));
311        rules.push_checking(Box::new(universe::AnyRule(sym.uri.clone())));
312        rules.push_marker(Box::new(universe::AnyRule(sym.uri.clone())));
313    }
314    pub implicit = (sym,rules) => {
315
316    }
317    pub map = (sym,rules) => {
318        rules.push_inhabitable(Box::new(super::sequences::map::MapInhabitableRule(sym.uri.clone())));
319        rules.push_simplification(Box::new(super::sequences::map::MapSimplificationRule(sym.uri.clone())));
320        rules.push_simplification(Box::new(super::sequences::map::MapArgumentSimplificationRule(sym.uri.clone())));
321        rules.push_simplification(Box::new(super::sequences::map::MapIndexSimplificationRule(sym.uri.clone())));
322        rules.push_inference(Box::new(super::sequences::map::MapInferenceRule(sym.uri.clone())));
323    }
324    pub letrule("let") = (sym,rules) => {
325        rules.push_simplification(Box::new(letin::LetinComputation(sym.uri.clone())));
326    }
327
328    pub numnat = (sym,rules) => {
329        rules.push_marker(Box::new(numbers::NumberRule{
330            typ:numbers::NumberType::Naturals,
331            sym:sym.uri.clone()
332        }));
333    }
334    pub numposnat = (sym,rules) => {
335        rules.push_marker(Box::new(numbers::NumberRule{
336            typ: numbers::NumberType::PositiveNaturals,
337            sym:sym.uri.clone()
338        }));
339    }
340    pub numint = (sym,rules) => {
341        rules.push_marker(Box::new(numbers::NumberRule{
342            typ:numbers::NumberType::Integers,
343            sym:sym.uri.clone()
344        }));
345    }
346    pub numnegint = (sym,rules) => {
347        rules.push_marker(Box::new(numbers::NumberRule{
348            typ:numbers::NumberType::NegativeIntegers,
349            sym:sym.uri.clone()
350        }));
351    }
352    pub numnonzeroint = (sym,rules) => {
353        rules.push_marker(Box::new(numbers::NumberRule{
354            typ:numbers::NumberType::NonZeroIntegers,
355            sym:sym.uri.clone()
356        }));
357    }
358    pub numrat = (sym,rules) => {
359        rules.push_marker(Box::new(numbers::NumberRule{
360            typ:numbers::NumberType::Rationals,
361            sym:sym.uri.clone()
362        }));
363    }
364    pub numposrat = (sym,rules) => {
365        rules.push_marker(Box::new(numbers::NumberRule{
366            typ:numbers::NumberType::PositiveRationals,
367            sym:sym.uri.clone()
368        }));
369    }
370    pub numnegrat = (sym,rules) => {
371        rules.push_marker(Box::new(numbers::NumberRule{
372            typ:numbers::NumberType::NegativeRationals,
373            sym:sym.uri.clone()
374        }));
375    }
376    pub numnonzerorat = (sym,rules) => {
377        rules.push_marker(Box::new(numbers::NumberRule{
378            typ:numbers::NumberType::NonZeroRationals,
379            sym:sym.uri.clone()
380        }));
381    }
382    pub numreal = (sym,rules) => {
383        rules.push_marker(Box::new(numbers::NumberRule{
384            typ:numbers::NumberType::Reals,
385            sym:sym.uri.clone()
386        }));
387    }
388    pub numposreal = (sym,rules) => {
389        rules.push_marker(Box::new(numbers::NumberRule{
390            typ:numbers::NumberType::PositiveReals,
391            sym:sym.uri.clone()
392        }));
393    }
394    pub numnegreal = (sym,rules) => {
395        rules.push_marker(Box::new(numbers::NumberRule{
396            typ:numbers::NumberType::NegativeReals,
397            sym:sym.uri.clone()
398        }));
399    }
400    pub numnonzeroreal = (sym,rules) => {
401        rules.push_marker(Box::new(numbers::NumberRule{
402            typ:numbers::NumberType::NonZeroReals,
403            sym:sym.uri.clone()
404        }));
405    }
406    pub numcomplex = (sym,rules) => {
407        rules.push_marker(Box::new(numbers::NumberRule{
408            typ:numbers::NumberType::Complex,
409            sym:sym.uri.clone()
410        }));
411    }
412    pub addition = (sym,rules) => {
413        rules.push_simplification(Box::new(numbers::AdditionRule(sym.uri.clone())));
414    }
415    pub multiplication = (sym,rules) => {
416        rules.push_simplification(Box::new(numbers::MultiplicationRule(sym.uri.clone())));
417    }
418    pub division = (sym,rules) => {
419        rules.push_simplification(Box::new(numbers::DivisionRule(sym.uri.clone())));
420    }
421    pub exponentiation = (sym,rules) => {
422        rules.push_simplification(Box::new(numbers::ExponentiationRule(sym.uri.clone())));
423    }
424    pub subtraction = (sym,rules) => {
425        rules.push_simplification(Box::new(numbers::SubtractionRule(sym.uri.clone())));
426    }
427    pub logarithm = (sym,rules) => {
428        rules.push_simplification(Box::new(numbers::Logarithm(sym.uri.clone())));
429    }
430    pub leq = (sym,rules) => {
431        rules.push_proof(Box::new(numbers::LessThan(sym.uri.clone())));
432    }
433    pub max = (sym,rules) => {
434        rules.push_simplification(Box::new(numbers::Max(sym.uri.clone())));
435    }
436}
ftml_solver/rules/extractors.rs

ftml_solver/rules/
extractors.rs
