ftml_solver/rules/operators/
numbers.rs

1use ftml_ontology::terms::{Argument, Numeric, Term, helpers::IntoTerm};
2use ftml_solver_trace::SizedSolverRule;
3use ftml_uris::{Id, SymbolUri};
4
5use crate::{
6    CheckRef,
7    rules::{
8        CheckingRule, EqualityRule, InferenceRule, MarkerRule, ProofRule, SimplificationRule,
9        SubtypeRule,
10    },
11    split::SplitStrategy,
12};
13
14#[derive(Debug, Clone, Copy, PartialEq, Eq, Hash)]
15pub enum NumberType {
16    PositiveNaturals,
17    Naturals,
18    NegativeIntegers,
19    Integers, // PositiveIntegers = Naturals
20    NonZeroIntegers,
21    Rationals,
22    PositiveRationals,
23    NegativeRationals,
24    NonZeroRationals,
25    Reals,
26    PositiveReals,
27    NegativeReals,
28    NonZeroReals,
29    Complex,
30}
31impl NumberType {
32    pub const fn as_str(self) -> &'static str {
33        match self {
34            Self::PositiveNaturals => "natural numbers (excluding zero)",
35            Self::Naturals => "natural numbers (including 0)",
36            Self::NegativeIntegers => "negative integers",
37            Self::Integers => "integers",
38            Self::NonZeroIntegers => "non-zero integers",
39            Self::Rationals => "rational numbers",
40            Self::PositiveRationals => "positive rational numbers (including 0)",
41            Self::NegativeRationals => "negative rational numbers",
42            Self::NonZeroRationals => "non-zero rational numbers",
43            Self::Reals => "real numbers",
44            Self::PositiveReals => "positive real numbers (including zero)",
45            Self::NegativeReals => "negative real numbers",
46            Self::NonZeroReals => "non-zero real numbers",
47            Self::Complex => "complex numbers",
48        }
49    }
50    pub fn contains(self, num: &Numeric) -> bool {
51        match self {
52            Self::Complex => true,
53            Self::Reals => true,
54            Self::NonZeroReals => match num {
55                Numeric::Int(i) => *i != 0,
56                Numeric::Float(i) => **i != 0.0,
57            },
58            Self::PositiveReals => match num {
59                Numeric::Int(i) => *i >= 0,
60                Numeric::Float(i) => **i >= 0.0,
61            },
62            Self::NegativeReals => match num {
63                Numeric::Int(i) => *i < 0,
64                Numeric::Float(i) => **i < 0.0,
65            },
66            Self::Integers => num.as_int().is_some(),
67            Self::NegativeIntegers => num.as_int().is_some_and(|i| i < 0),
68            Self::NonZeroIntegers => num.as_int().is_some_and(|i| i != 0),
69            Self::Naturals => num.as_int().is_some_and(|i| i >= 0),
70            Self::PositiveNaturals => num.as_int().is_some_and(|i| i > 0),
71            _ => false,
72        }
73    }
74    pub fn get<'c, Split: SplitStrategy>(
75        self,
76        checker: &'c CheckRef<'_, '_, Split>,
77    ) -> Option<&'c SymbolUri> {
78        checker.rules().marker().iter().rev().find_map(|rl| {
79            rl.as_any()
80                .downcast_ref::<NumberRule>()
81                .and_then(|rl| if rl.typ == self { Some(&rl.sym) } else { None })
82        })
83    }
84}
85impl PartialOrd for NumberType {
86    #[allow(clippy::match_same_arms)]
87    fn partial_cmp(&self, other: &Self) -> Option<std::cmp::Ordering> {
88        use std::cmp::Ordering::{Greater, Less};
89        if *self == *other {
90            return Some(std::cmp::Ordering::Equal);
91        }
92        match (*self, *other) {
93            (_, Self::Complex) => Some(Less),
94            (Self::Complex, _) => Some(Greater),
95            //(_, Self::Reals) => Some(Less),
96            //(Self::Reals, _) => Some(Greater),
97            (
98                Self::PositiveNaturals,
99                Self::NegativeIntegers | Self::NegativeRationals | Self::NegativeReals,
100            ) => None,
101            (Self::PositiveNaturals, _) => Some(Less),
102            (Self::Naturals, Self::PositiveNaturals) => Some(Greater),
103            (
104                Self::Naturals,
105                Self::Integers
106                | Self::Rationals
107                | Self::PositiveRationals
108                | Self::PositiveReals
109                | Self::Reals,
110            ) => Some(Less),
111            (
112                Self::NegativeIntegers,
113                Self::Integers
114                | Self::NonZeroIntegers
115                | Self::Rationals
116                | Self::NegativeRationals
117                | Self::NonZeroRationals
118                | Self::NegativeReals
119                | Self::NonZeroReals
120                | Self::Reals,
121            ) => Some(Less),
122            (Self::Integers, Self::PositiveNaturals | Self::Naturals) => Some(Greater),
123            (Self::Integers, Self::Rationals | Self::PositiveReals | Self::Reals) => Some(Less),
124            (Self::NonZeroIntegers, Self::PositiveNaturals | Self::NegativeIntegers) => {
125                Some(Greater)
126            }
127            (
128                Self::Rationals,
129                Self::PositiveNaturals
130                | Self::Naturals
131                | Self::NegativeIntegers
132                | Self::Integers
133                | Self::NonZeroIntegers,
134            ) => Some(Greater),
135            (Self::PositiveRationals, Self::PositiveNaturals | Self::Naturals) => Some(Greater),
136            (Self::PositiveRationals, Self::PositiveReals | Self::Reals) => Some(Less),
137            (Self::NegativeRationals, Self::NegativeIntegers | Self::NonZeroIntegers) => {
138                Some(Greater)
139            }
140            (
141                Self::NegativeRationals,
142                Self::NonZeroRationals | Self::NegativeReals | Self::NonZeroReals | Self::Reals,
143            ) => Some(Less),
144            (
145                Self::NonZeroRationals,
146                Self::PositiveNaturals | Self::NegativeIntegers | Self::NonZeroIntegers,
147            ) => Some(Greater),
148            (Self::NonZeroRationals, Self::Rationals | Self::NonZeroReals | Self::Reals) => {
149                Some(Less)
150            }
151            (
152                Self::PositiveReals,
153                Self::PositiveNaturals | Self::Naturals | Self::PositiveRationals,
154            ) => Some(Greater),
155            (Self::PositiveReals, Self::NonZeroReals | Self::Reals) => Some(Less),
156            (Self::NegativeReals, Self::NegativeIntegers | Self::NegativeRationals) => {
157                Some(Greater)
158            }
159            (Self::NegativeReals, Self::NonZeroReals | Self::Reals) => Some(Less),
160            (Self::NonZeroReals, Self::Reals) => Some(Less),
161            (Self::Reals, o) if o != Self::Complex => Some(Greater),
162            _ => None,
163        }
164    }
165}
166
167#[derive(Debug, Clone, PartialEq, Eq)]
168pub struct NumberRule {
169    pub typ: NumberType,
170    pub sym: SymbolUri,
171}
172impl SizedSolverRule for NumberRule {
173    fn display(&self) -> Vec<ftml_solver_trace::Displayable> {
174        ftml_solver_trace::trace!(&self.sym, "is type of", self.typ.as_str())
175    }
176}
177impl<Split: SplitStrategy> MarkerRule<Split> for NumberRule {}
178impl NumberRule {
179    pub fn is_number_term<Split: SplitStrategy>(
180        term: &Term,
181        checker: &CheckRef<'_, '_, Split>,
182    ) -> Option<NumberType> {
183        if let Term::Symbol { uri, .. } = term {
184            Self::is_number_sym(uri, checker)
185        } else {
186            None
187        }
188    }
189    pub fn is_number_sym<Split: SplitStrategy>(
190        uri: &SymbolUri,
191        checker: &CheckRef<'_, '_, Split>,
192    ) -> Option<NumberType> {
193        checker.rules().marker().iter().rev().find_map(|rl| {
194            rl.as_any()
195                .downcast_ref::<Self>()
196                .and_then(|rl| if rl.sym == *uri { Some(rl.typ) } else { None })
197        })
198    }
199}
200
201#[derive(Debug, Clone, Copy, PartialEq, Eq)]
202pub struct NumberTypes;
203impl SizedSolverRule for NumberTypes {
204    fn display(&self) -> Vec<ftml_solver_trace::Displayable> {
205        ftml_solver_trace::trace!("number type")
206    }
207}
208impl<Split: SplitStrategy> SubtypeRule<Split> for NumberTypes {
209    fn applicable(&self, checker: &CheckRef<'_, '_, Split>, sub: &Term, sup: &Term) -> bool {
210        if let Term::Symbol { uri: n1, .. } = sub
211            && let Term::Symbol { uri: n2, .. } = sup
212            && let Some(type1) = NumberRule::is_number_sym(n1, checker)
213            && let Some(type2) = NumberRule::is_number_sym(n2, checker)
214        {
215            type1 <= type2
216        } else {
217            false
218        }
219    }
220    fn apply<'t>(
221        &self,
222        mut checker: CheckRef<'t, '_, Split>,
223        sub: &'t Term,
224        sup: &'t Term,
225    ) -> Option<bool> {
226        let Term::Symbol { uri: n1, .. } = sub else {
227            return None;
228        };
229        let Term::Symbol { uri: n2, .. } = sup else {
230            return None;
231        };
232        let type1 = NumberRule::is_number_sym(n1, &checker)?;
233        let type2 = NumberRule::is_number_sym(n2, &checker)?;
234        checker.comment(format!("{} <= {}", type1.as_str(), type2.as_str()));
235        // by applicability
236        Some(true)
237    }
238}
239impl<Split: SplitStrategy> CheckingRule<Split> for NumberTypes {
240    fn applicable(&self, checker: &CheckRef<'_, '_, Split>, term: &Term, tp: &Term) -> bool {
241        if let Term::Number(n) = term
242            && let Term::Symbol { uri, .. } = tp
243            && let Some(typ) = NumberRule::is_number_sym(uri, checker)
244        {
245            typ.contains(n)
246        } else {
247            false
248        }
249    }
250    fn apply<'t>(&self, _: CheckRef<'t, '_, Split>, _: &'t Term, _: &'t Term) -> Option<bool> {
251        // by applicability
252        Some(true)
253    }
254}
255impl<Split: SplitStrategy> InferenceRule<Split> for NumberTypes {
256    fn applicable(&self, term: &Term) -> bool {
257        matches!(term, Term::Number(_))
258    }
259    fn infer<'t>(&self, checker: CheckRef<'t, '_, Split>, term: &'t Term) -> Option<Term> {
260        macro_rules! get {
261            ($typ:ident,$cond:expr) => {
262                if $cond && let Some(uri) = NumberType::$typ.get(&checker) {
263                    return Some(Term::Symbol {
264                        uri: uri.clone(),
265                        presentation: None,
266                    });
267                }
268            };
269        }
270        let Term::Number(num) = term else {
271            return None;
272        };
273        if let Some(n) = num.as_int() {
274            get!(PositiveNaturals, n > 0);
275            get!(Naturals, n >= 0);
276            get!(NegativeIntegers, n < 0);
277        }
278        let f = num.as_float();
279        get!(PositiveReals, f >= 0.0);
280        get!(NegativeReals, f < 0.0);
281        None
282    }
283}
284
285impl<Split: SplitStrategy> EqualityRule<Split> for NumberTypes {
286    fn applicable(&self, lhs: &Term, rhs: &Term) -> bool {
287        matches!(lhs, Term::Number(_)) && matches!(rhs, Term::Number(_))
288    }
289    fn apply<'t>(&self, _: CheckRef<'t, '_, Split>, lhs: &'t Term, rhs: &'t Term) -> Option<bool> {
290        let (Term::Number(lhs), Term::Number(rhs)) = (lhs, rhs) else {
291            return None;
292        };
293        Some(lhs == rhs)
294    }
295}
296
297// -------------------------------------------------------------------------------------------
298
299#[derive(Debug, Clone, PartialEq, Eq)]
300pub struct Max(pub SymbolUri);
301impl SizedSolverRule for Max {
302    fn display(&self) -> Vec<ftml_solver_trace::Displayable> {
303        ftml_solver_trace::trace!(&self.0, " is maximum")
304    }
305}
306impl<Split: SplitStrategy> SimplificationRule<Split> for Max {
307    fn applicable(&self, term: &Term) -> bool {
308        let Term::Application(app) = term else {
309            return false;
310        };
311        if app.head.is(&self.0)
312            && let [
313                Argument::Simple(Term::Number(_)),
314                Argument::Simple(Term::Number(_)),
315            ] = &*app.arguments
316        {
317            true
318        } else {
319            false
320        }
321    }
322    fn apply<'t>(
323        &self,
324        _: CheckRef<'t, '_, Split>,
325        term: &'t Term,
326    ) -> Result<Term, Option<ftml_ontology::terms::termpaths::TermPath>> {
327        let Term::Application(app) = term else {
328            return Err(None);
329        };
330        if let [
331            Argument::Simple(Term::Number(a)),
332            Argument::Simple(Term::Number(b)),
333        ] = &*app.arguments
334        {
335            let a = a.as_float();
336            let b = b.as_float();
337            Ok(Term::Number(Numeric::Float(a.max(b).into())))
338        } else {
339            Err(None)
340        }
341    }
342}
343
344#[derive(Debug, Clone, PartialEq, Eq)]
345pub struct LessThan(pub SymbolUri);
346impl SizedSolverRule for LessThan {
347    fn display(&self) -> Vec<ftml_solver_trace::Displayable> {
348        ftml_solver_trace::trace!(&self.0, " is <=")
349    }
350}
351impl<Split: SplitStrategy> ProofRule<Split> for LessThan {
352    fn applicable(&self, term: &Term) -> bool {
353        let Term::Application(app) = term else {
354            return false;
355        };
356        if app.head.is(&self.0)
357            && let [
358                Argument::Simple(Term::Number(a)),
359                Argument::Simple(Term::Number(b)),
360            ] = &*app.arguments
361        {
362            true
363        } else {
364            false
365        }
366    }
367    fn prove<'t>(&self, _: CheckRef<'t, '_, Split>, goal: &'t Term) -> Option<Term> {
368        let Term::Application(app) = goal else {
369            return None;
370        };
371        let [
372            Argument::Simple(Term::Number(a)),
373            Argument::Simple(Term::Number(b)),
374        ] = &*app.arguments
375        else {
376            return None;
377        };
378
379        if a.as_float() <= b.as_float() {
380            Some(ftml_uris::metatheory::AUTO_PROVE.clone().into())
381        } else {
382            None
383        }
384    }
385}
386
387#[derive(Debug, Clone, PartialEq, Eq)]
388pub struct Logarithm(pub SymbolUri);
389impl SizedSolverRule for Logarithm {
390    fn display(&self) -> Vec<ftml_solver_trace::Displayable> {
391        ftml_solver_trace::trace!(&self.0, " is logarithm")
392    }
393}
394impl<Split: SplitStrategy> SimplificationRule<Split> for Logarithm {
395    fn applicable(&self, term: &Term) -> bool {
396        let Term::Application(app) = term else {
397            return false;
398        };
399        if app.head.is(&self.0)
400            && let [
401                Argument::Simple(Term::Number(b)),
402                Argument::Simple(Term::Number(x)),
403            ] = &*app.arguments
404        {
405            let b = b.as_float();
406            let x = x.as_float();
407            b > 0.0 && x > 0.0 && b != 1.0
408        } else {
409            false
410        }
411    }
412    fn apply<'t>(
413        &self,
414        _: CheckRef<'t, '_, Split>,
415        term: &'t Term,
416    ) -> Result<Term, Option<ftml_ontology::terms::termpaths::TermPath>> {
417        let Term::Application(app) = term else {
418            return Err(None);
419        };
420        if let [
421            Argument::Simple(Term::Number(b)),
422            Argument::Simple(Term::Number(x)),
423        ] = &*app.arguments
424        {
425            let b = b.as_float();
426            let x = x.as_float();
427            let r = if b == 2.0 {
428                x.log2()
429            } else if b == 10.0 {
430                x.log10()
431            } else if b == std::f64::consts::E {
432                x.ln()
433            } else {
434                x.log(b)
435            };
436            Ok(Term::Number(Numeric::Float(r.into())))
437        } else {
438            Err(None)
439        }
440    }
441}
442
443fn applicable(uri: &SymbolUri, term: &Term, unit: f64) -> bool {
444    let Term::Application(app) = term else {
445        return false;
446    };
447    app.head.is(uri)
448        && (matches!(
449            &*app.arguments,
450            [
451                Argument::Simple(Term::Number(_)),
452                Argument::Simple(Term::Number(_))
453            ] | [Argument::Sequence(_)]
454        ) || matches!(
455        &*app.arguments,
456        [
457            Argument::Simple(Term::Number(n)),
458            Argument::Simple(_)
459        ]
460        if n.as_float() == unit
461        ) || matches!(
462        &*app.arguments,
463        [
464            Argument::Simple(_),
465            Argument::Simple(Term::Number(n)),
466        ]
467        if n.as_float() == unit
468        ))
469}
470
471macro_rules! arith {
472    ($($name:ident $trace:literal $unit:literal = ($a:ident,$b:ident => $op:expr))*) => {
473        $(
474            #[derive(Debug, Clone, PartialEq, Eq)]
475            pub struct $name(pub SymbolUri);
476            impl SizedSolverRule for $name {
477                fn display(&self) -> Vec<ftml_solver_trace::Displayable> {
478                    ftml_solver_trace::trace!(&self.0, $trace)
479                }
480            }
481            impl<Split: SplitStrategy> SimplificationRule<Split> for $name {
482                fn applicable(&self, term: &Term) -> bool {
483                    applicable(&self.0,term,$unit)
484                }
485                fn apply<'t>(
486                    &self,
487                    _: CheckRef<'t, '_, Split>,
488                    term: &'t Term,
489                ) -> Result<Term, Option<ftml_ontology::terms::termpaths::TermPath>> {
490                    let Term::Application(app) = term else {
491                        return Err(None);
492                    };
493                    match &*app.arguments {
494                        [Argument::Simple(Term::Number(z)), Argument::Simple(o)] if z.as_float() == $unit => {
495                            Ok(o.clone())
496                        }
497                        [Argument::Simple(o), Argument::Simple(Term::Number(z))] if z.as_float() == $unit => {
498                            Ok(o.clone())
499                        }
500                        [
501                            Argument::Simple(Term::Number($a)),
502                            Argument::Simple(Term::Number($b)),
503                        ] => ($op).map_or(Err(None), |r| Ok(Term::Number(r))),
504                        [Argument::Sequence(seq)] => Ok(super::super::sequences::fold::Fold::apply_init(
505                            seq.clone(),
506                            Term::Number(Numeric::Int(0)),
507                            |x, y| self.0.clone().apply_tms([y.into(), x.into()]),
508                        )),
509                        _ => Err(None),
510                    }
511                }
512            }
513        )*
514    };
515}
516arith! {
517    AdditionRule " is addition" 0.0 = (a,b => *a + *b)
518    SubtractionRule " is subtraction" 0.0 = (a,b => *a - *b)
519    MultiplicationRule " is multiplication" 1.0 = (a,b => *a * *b)
520    DivisionRule " is division" 1.0 = (a,b => *a / *b)
521    ExponentiationRule " is exponentiation" 1.0 = (a,b => *a ^ *b)
522}
523
524/*
525#[derive(Debug, Clone, PartialEq, Eq)]
526pub struct AdditionRule(pub SymbolUri);
527impl SizedSolverRule for AdditionRule {
528    fn display(&self) -> Vec<ftml_solver_trace::Displayable> {
529        ftml_solver_trace::trace!(&self.0, " is addition")
530    }
531}
532impl<Split: SplitStrategy> SimplificationRule<Split> for AdditionRule {
533    fn applicable(&self, term: &Term) -> bool {
534        let Term::Application(app) = term else {
535            return false;
536        };
537        app.head.is(&self.0)
538            && (matches!(
539                &*app.arguments,
540                [
541                    Argument::Simple(Term::Number(_)),
542                    Argument::Simple(Term::Number(_))
543                ] | [Argument::Sequence(_)]
544            ) || matches!(
545            &*app.arguments,
546            [
547                Argument::Simple(Term::Number(n)),
548                Argument::Simple(_)
549            ]
550            if n.as_float() == 0.0
551            ) || matches!(
552            &*app.arguments,
553            [
554                Argument::Simple(_),
555                Argument::Simple(Term::Number(n)),
556            ]
557            if n.as_float() == 0.0
558            ))
559    }
560    fn apply<'t>(
561        &self,
562        _: CheckRef<'t, '_, Split>,
563        term: &'t Term,
564    ) -> Result<Term, Option<ftml_ontology::terms::termpaths::TermPath>> {
565        let Term::Application(app) = term else {
566            return Err(None);
567        };
568        match &*app.arguments {
569            [Argument::Simple(Term::Number(z)), Argument::Simple(o)] if z.as_float() == 0.0 => {
570                Ok(o.clone())
571            }
572            [Argument::Simple(o), Argument::Simple(Term::Number(z))] if z.as_float() == 0.0 => {
573                Ok(o.clone())
574            }
575            [
576                Argument::Simple(Term::Number(a)),
577                Argument::Simple(Term::Number(b)),
578            ] => (*a + *b).map_or(Err(None), |r| Ok(Term::Number(r))),
579            [Argument::Sequence(seq)] => Ok(super::super::sequences::fold::Fold::apply_init(
580                seq.clone(),
581                Term::Number(Numeric::Int(0)),
582                |x, y| self.0.clone().apply_tms([y.into(), x.into()]),
583            )),
584            _ => Err(None),
585        }
586    }
587}
588 */
ftml_solver/rules/operators/numbers.rs

ftml_solver/rules/operators/
numbers.rs
