peano_axioms/
lib.rs

1//! Type-level numbers based on an extension of the Peano axioms.
2
3#![no_std]
4#![recursion_limit = "256"]
5#![cfg_attr(test, allow(unused_parens))]
6
7mod div;
8pub use div::Quotient;
9pub use div::Remainder;
10
11mod fraction;
12pub use fraction::Fraction;
13pub use fraction::Inverse;
14pub use fraction::Reciprocal;
15pub use fraction::ToInt;
16
17mod gcd;
18pub use gcd::Gcd;
19pub use gcd::GreatestCommonDivisor;
20
21use core::fmt;
22use core::hash;
23use core::marker::PhantomData;
24use core::ops::Add;
25use core::ops::Div;
26use core::ops::Mul;
27use core::ops::Neg;
28use core::ops::Sub;
29
30/// Types which can be converted to a runtime value.
31pub trait Reify<T> {
32    /// The runtime representation of this type.
33    const REIFIED: T;
34
35    /// A convience method for getting the runtime representation of this type.
36    ///
37    /// The default implementation should always be sufficient.
38    #[inline(always)]
39    fn reify(&self) -> T {
40        Self::REIFIED
41    }
42}
43
44/// Types which are part of a sequence.
45pub trait Sequence {
46    /// The next type in the sequence.
47    type Next;
48
49    /// The previous type in the sequence.
50    type Prev;
51}
52
53/// The number zero.
54#[derive(Debug, Clone, Copy, PartialEq, Eq, Default)]
55pub struct Zero;
56
57impl Zero {
58    /// The value associated with this type, i.e. 0.
59    pub const VALUE: Zero = Zero;
60}
61
62impl Sequence for Zero {
63    type Next = Next<Zero>;
64
65    type Prev = Prev<Zero>;
66}
67
68impl fmt::Display for Zero {
69    #[inline]
70    fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
71        f.write_str("0")
72    }
73}
74
75macro_rules! reify_zero {
76    ($($ty:ty),* $(,)?) => {
77        $(
78            impl Reify<$ty> for Zero {
79                const REIFIED: $ty = 0;
80            }
81
82            impl From<Zero> for $ty {
83                #[inline(always)]
84                fn from(_: Zero) -> Self {
85                    0
86                }
87            }
88        )*
89    };
90}
91
92reify_zero![u8, u16, u32, u64, u128, usize, i8, i16, i32, i64, i128, isize];
93
94impl hash::Hash for Zero {
95    #[inline]
96    fn hash<H: hash::Hasher>(&self, state: &mut H) {
97        state.write_i128(0);
98    }
99}
100
101/// The successor to some number.
102///
103/// Some of the traits in this crate require that `Next<T>` is positive. If this
104/// causes errors, the [`Simplify`] trait can be used to remove redundancies.
105#[derive(Debug, Clone, Copy, PartialEq, Eq, Default)]
106pub struct Next<T>(PhantomData<T>);
107
108impl<T> Next<T> {
109    /// The value associated with this type.
110    pub const VALUE: Next<T> = Next(PhantomData);
111}
112
113impl<T> Sequence for Next<T> {
114    type Next = Next<Next<T>>;
115
116    type Prev = T;
117}
118
119impl<T> fmt::Display for Next<T>
120where
121    Self: Reify<u128>,
122{
123    #[inline]
124    fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
125        write!(f, "{}", Self::REIFIED)
126    }
127}
128
129impl<T> hash::Hash for Next<T>
130where
131    Self: Reify<i128>,
132{
133    #[inline]
134    fn hash<H: hash::Hasher>(&self, state: &mut H) {
135        state.write_i128(Self::REIFIED);
136    }
137}
138
139/// The predecessor to some number.
140///
141/// Some of the traits in this crate require that `Prev<T>` is negative. If this
142/// causes errors, the [`Simplify`] trait can be used to remove redundancies.
143#[derive(Debug, Clone, Copy, PartialEq, Eq, Default)]
144pub struct Prev<T>(PhantomData<T>);
145
146impl<T> Prev<T> {
147    /// The value associated with this type.
148    pub const VALUE: Prev<T> = Prev(PhantomData);
149}
150
151impl<T> Sequence for Prev<T> {
152    type Next = T;
153
154    type Prev = Prev<Prev<T>>;
155}
156
157impl<T> fmt::Display for Prev<T>
158where
159    Self: Reify<i128>,
160{
161    #[inline]
162    fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
163        write!(f, "{}", Self::REIFIED)
164    }
165}
166
167impl<T> hash::Hash for Prev<T>
168where
169    Self: Reify<i128>,
170{
171    #[inline]
172    fn hash<H: hash::Hasher>(&self, state: &mut H) {
173        state.write_i128(Self::REIFIED);
174    }
175}
176
177macro_rules! reify_generic {
178    ($name:ident, $op:tt, $($ty:ty),* $(,)?) => {
179        $(
180            impl<T> Reify<$ty> for $name<T>
181            where
182                T: Reify<$ty>
183            {
184                const REIFIED: $ty = T::REIFIED $op 1;
185            }
186
187            impl<T> From<$name<T>> for $ty
188            where
189                T: Reify<$ty>
190            {
191                #[inline(always)]
192                fn from(_: $name<T>) -> $ty {
193                    <$name<T> as Reify<$ty>>::REIFIED
194                }
195            }
196        )*
197    };
198}
199
200reify_generic![Next, +, u8, u16, u32, u64, u128, usize, i8, i16, i32, i64, i128, isize];
201
202reify_generic![Prev, -, i8, i16, i32, i64, i128, isize];
203
204trait IsNotNext {}
205
206impl IsNotNext for Zero {}
207
208impl<T> IsNotNext for Prev<T> {}
209
210trait IsNotPrev {}
211
212impl IsNotPrev for Zero {}
213
214impl<T> IsNotPrev for Next<T> {}
215
216trait IsNotZero {}
217
218impl<T> IsNotZero for Next<T> {}
219
220impl<T> IsNotZero for Prev<T> {}
221
222/// The number 1.
223pub type One = Next<Zero>;
224
225/// The number 2.
226pub type Two = Next<One>;
227
228/// The number 3.
229pub type Three = Next<Two>;
230
231/// The number 4.
232pub type Four = Next<Three>;
233
234/// The number 5.
235pub type Five = Next<Four>;
236
237/// The number 6.
238pub type Six = Next<Five>;
239
240/// The number 7.
241pub type Seven = Next<Six>;
242
243/// The number 8.
244pub type Eight = Next<Seven>;
245
246/// The number 9.
247pub type Nine = Next<Eight>;
248
249/// The number 10.
250pub type Ten = Next<Nine>;
251
252impl Add<Zero> for Zero {
253    type Output = Zero;
254
255    #[inline(always)]
256    fn add(self, _: Zero) -> Self::Output {
257        Zero
258    }
259}
260
261impl<T> Add<Zero> for Next<T> {
262    type Output = Self;
263
264    #[inline(always)]
265    fn add(self, _: Zero) -> Self::Output {
266        Self::VALUE
267    }
268}
269
270impl<T> Add<Zero> for Prev<T> {
271    type Output = Self;
272
273    #[inline(always)]
274    fn add(self, _: Zero) -> Self::Output {
275        Self::VALUE
276    }
277}
278
279impl<T> Add<Next<T>> for Zero {
280    type Output = Next<T>;
281
282    #[inline(always)]
283    fn add(self, _: Next<T>) -> Self::Output {
284        Self::Output::VALUE
285    }
286}
287
288impl<T> Add<Prev<T>> for Zero {
289    type Output = Prev<T>;
290
291    #[inline(always)]
292    fn add(self, _: Prev<T>) -> Self::Output {
293        Self::Output::VALUE
294    }
295}
296
297impl<T, U> Add<Next<U>> for Next<T>
298where
299    T: Add<U>,
300{
301    type Output = Next<Next<Sum<T, U>>>;
302
303    #[inline(always)]
304    fn add(self, _: Next<U>) -> Self::Output {
305        Self::Output::VALUE
306    }
307}
308
309impl<T, U> Add<Prev<U>> for Next<T>
310where
311    T: Add<U>,
312    Sum<T, U>: Default,
313{
314    type Output = Sum<T, U>;
315
316    #[inline(always)]
317    fn add(self, _: Prev<U>) -> Self::Output {
318        Self::Output::default()
319    }
320}
321
322impl<T, U> Add<Next<U>> for Prev<T>
323where
324    T: Add<U>,
325    Sum<T, U>: Default,
326{
327    type Output = Sum<T, U>;
328
329    #[inline(always)]
330    fn add(self, _: Next<U>) -> Self::Output {
331        Self::Output::default()
332    }
333}
334
335impl<T, U> Add<Prev<U>> for Prev<T>
336where
337    T: Add<U>,
338    Sum<T, U>: Sub<Two>,
339    Difference<Sum<T, U>, Two>: Default,
340{
341    type Output = Difference<Sum<T, U>, Two>;
342
343    #[inline(always)]
344    fn add(self, _: Prev<U>) -> Self::Output {
345        Self::Output::default()
346    }
347}
348
349/// The sum of `T` and `U`.
350pub type Sum<T, U> = <T as Add<U>>::Output;
351
352impl Mul<Zero> for Zero {
353    type Output = Zero;
354
355    #[inline(always)]
356    fn mul(self, _: Zero) -> Self::Output {
357        Zero
358    }
359}
360
361impl<T> Mul<Zero> for Next<T> {
362    type Output = Zero;
363
364    #[inline(always)]
365    fn mul(self, _: Zero) -> Self::Output {
366        Zero
367    }
368}
369
370impl<T> Mul<Zero> for Prev<T> {
371    type Output = Zero;
372
373    #[inline(always)]
374    fn mul(self, _: Zero) -> Self::Output {
375        Zero
376    }
377}
378
379impl<T> Mul<Next<T>> for Zero {
380    type Output = Zero;
381
382    #[inline(always)]
383    fn mul(self, _: Next<T>) -> Self::Output {
384        Zero
385    }
386}
387
388impl<T> Mul<Prev<T>> for Zero {
389    type Output = Zero;
390
391    #[inline(always)]
392    fn mul(self, _: Prev<T>) -> Self::Output {
393        Zero
394    }
395}
396
397impl<T, U> Mul<Next<U>> for Next<T>
398where
399    Next<T>: Mul<U> + Add<Product<Next<T>, U>>,
400    Sum<Next<T>, Product<Next<T>, U>>: Default,
401{
402    type Output = Sum<Next<T>, Product<Next<T>, U>>;
403
404    #[inline(always)]
405    fn mul(self, _: Next<U>) -> Self::Output {
406        Self::Output::default()
407    }
408}
409
410impl<T, U> Mul<Prev<U>> for Next<T>
411where
412    T: Mul<U>,
413    Product<T, U>: Sub<T>,
414    Difference<Product<T, U>, T>: Add<U>,
415    Sum<Difference<Product<T, U>, T>, U>: Sub<One>,
416    Difference<Sum<Difference<Product<T, U>, T>, U>, One>: Default,
417{
418    type Output = Difference<Sum<Difference<Product<T, U>, T>, U>, One>;
419
420    #[inline(always)]
421    fn mul(self, _: Prev<U>) -> Self::Output {
422        Self::Output::default()
423    }
424}
425
426impl<T, U> Mul<Next<U>> for Prev<T>
427where
428    Next<U>: Mul<Prev<T>>,
429    Product<Next<U>, Prev<T>>: Default,
430{
431    type Output = Product<Next<U>, Prev<T>>;
432
433    #[inline(always)]
434    fn mul(self, _: Next<U>) -> Self::Output {
435        Self::Output::default()
436    }
437}
438
439impl<T, U> Mul<Prev<U>> for Prev<T>
440where
441    T: Mul<U>,
442    Product<T, U>: Sub<T>,
443    Difference<Product<T, U>, T>: Sub<U>,
444    Difference<Difference<Product<T, U>, T>, U>: Add<One>,
445    Sum<Difference<Difference<Product<T, U>, T>, U>, One>: Default,
446{
447    type Output = Sum<Difference<Difference<Product<T, U>, T>, U>, One>;
448
449    #[inline(always)]
450    fn mul(self, _: Prev<U>) -> Self::Output {
451        Self::Output::default()
452    }
453}
454
455/// The product of `T` and `U`.
456pub type Product<T, U> = <T as Mul<U>>::Output;
457
458impl Sub<Zero> for Zero {
459    type Output = Zero;
460
461    #[inline(always)]
462    fn sub(self, _: Zero) -> Self::Output {
463        Zero
464    }
465}
466
467impl<T: Neg> Sub<Next<T>> for Zero {
468    type Output = Prev<Negation<T>>;
469
470    #[inline(always)]
471    fn sub(self, _: Next<T>) -> Self::Output {
472        Self::Output::VALUE
473    }
474}
475
476impl<T: Neg> Sub<Prev<T>> for Zero {
477    type Output = Next<Negation<T>>;
478
479    #[inline(always)]
480    fn sub(self, _: Prev<T>) -> Self::Output {
481        Self::Output::VALUE
482    }
483}
484
485impl<T> Sub<Zero> for Next<T> {
486    type Output = Self;
487
488    #[inline(always)]
489    fn sub(self, _: Zero) -> Self::Output {
490        Self::Output::VALUE
491    }
492}
493
494impl<T> Sub<Zero> for Prev<T> {
495    type Output = Self;
496
497    #[inline(always)]
498    fn sub(self, _: Zero) -> Self::Output {
499        Self::Output::VALUE
500    }
501}
502
503impl<T, U> Sub<Next<U>> for Next<T>
504where
505    T: Sub<U>,
506    Difference<T, U>: Default,
507{
508    type Output = Difference<T, U>;
509
510    #[inline(always)]
511    fn sub(self, _: Next<U>) -> Self::Output {
512        Self::Output::default()
513    }
514}
515
516impl<T, U> Sub<Prev<U>> for Next<T>
517where
518    Prev<U>: Neg,
519    Next<T>: Add<Negation<Prev<U>>>,
520    Sum<Next<T>, Negation<Prev<U>>>: Default,
521{
522    type Output = Sum<Next<T>, Negation<Prev<U>>>;
523
524    #[inline(always)]
525    fn sub(self, _: Prev<U>) -> Self::Output {
526        Self::Output::default()
527    }
528}
529
530impl<T, U> Sub<Next<U>> for Prev<T>
531where
532    Prev<Prev<T>>: Sub<U>,
533    Difference<Prev<Prev<T>>, U>: Default,
534{
535    type Output = Difference<Prev<Prev<T>>, U>;
536
537    #[inline(always)]
538    fn sub(self, _: Next<U>) -> Self::Output {
539        Self::Output::default()
540    }
541}
542
543impl<T, U> Sub<Prev<U>> for Prev<T>
544where
545    T: Sub<U>,
546    Difference<T, U>: Default,
547{
548    type Output = Difference<T, U>;
549
550    #[inline(always)]
551    fn sub(self, _: Prev<U>) -> Self::Output {
552        Self::Output::default()
553    }
554}
555
556/// The difference between `T` and `U`.
557///
558/// Note that this is not absolute difference. For the absolute difference
559/// between `T` and `U`, use [`Absolute<Difference<T, U>>`][Absolute].
560pub type Difference<T, U> = <T as Sub<U>>::Output;
561
562/// Type-level exponentiation.
563pub trait Exp<T> {
564    /// `Self` raised to the power of `T`.
565    type Result;
566}
567
568impl Exp<Zero> for Zero {
569    type Result = One;
570}
571
572impl<T> Exp<Zero> for Next<T> {
573    type Result = One;
574}
575
576impl<T> Exp<Next<T>> for Zero {
577    type Result = Zero;
578}
579
580impl<T> Exp<Zero> for Prev<T> {
581    type Result = One;
582}
583
584impl<T> Exp<Prev<T>> for Zero {
585    type Result = Zero;
586}
587
588impl<T, U> Exp<Next<U>> for Next<T>
589where
590    Next<U>: Positive,
591    Next<T>: Exp<U>,
592    Exponent<Next<T>, U>: Mul<Next<T>>,
593{
594    type Result = Product<Exponent<Next<T>, U>, Next<T>>;
595}
596
597impl<T, U> Exp<Prev<U>> for Next<T>
598where
599    Prev<U>: Negative + Abs,
600    Next<T>: Exp<Absolute<Prev<U>>>,
601    Exponent<Next<T>, Absolute<Prev<U>>>: Inverse,
602{
603    type Result = Reciprocal<Exponent<Next<T>, Absolute<Prev<U>>>>;
604}
605
606impl<T, U> Exp<Next<U>> for Prev<T>
607where
608    Next<U>: Positive,
609    Prev<T>: Exp<U>,
610    Exponent<Prev<T>, U>: Mul<Prev<T>>,
611{
612    type Result = Product<Exponent<Prev<T>, U>, Prev<T>>;
613}
614
615impl<T, U> Exp<Prev<U>> for Prev<T>
616where
617    Prev<U>: Negative + Abs,
618    Prev<T>: Exp<Absolute<Prev<U>>>,
619    Exponent<Prev<T>, Absolute<Prev<U>>>: Inverse,
620{
621    type Result = Reciprocal<Exponent<Prev<T>, Absolute<Prev<U>>>>;
622}
623
624/// `T` raised to the power of `U`.
625pub type Exponent<T, U> = <T as Exp<U>>::Result;
626
627impl Neg for Zero {
628    type Output = Zero;
629
630    #[inline(always)]
631    fn neg(self) -> Self::Output {
632        Zero
633    }
634}
635
636impl<T: Neg> Neg for Next<T> {
637    type Output = Prev<Negation<T>>;
638
639    #[inline(always)]
640    fn neg(self) -> Self::Output {
641        Self::Output::VALUE
642    }
643}
644
645impl<T: Neg> Neg for Prev<T> {
646    type Output = Next<Negation<T>>;
647
648    #[inline(always)]
649    fn neg(self) -> Self::Output {
650        Self::Output::VALUE
651    }
652}
653
654/// The negation of `Self`.
655pub type Negation<T> = <T as Neg>::Output;
656
657/// Type-level least common multiple.
658pub trait Lcm<T> {
659    /// The least common multiple of `Self` and `T`.
660    type Result;
661}
662
663impl Lcm<Zero> for Zero {
664    type Result = Zero;
665}
666
667impl<T> Lcm<Next<T>> for Zero {
668    type Result = Zero;
669}
670
671impl<T> Lcm<Zero> for Next<T> {
672    type Result = Zero;
673}
674
675impl<T> Lcm<Prev<T>> for Zero {
676    type Result = Zero;
677}
678
679impl<T> Lcm<Zero> for Prev<T> {
680    type Result = Zero;
681}
682
683macro_rules! impl_lcm {
684    ($(($name1:ident, $name2:ident)),* $(,)?) => {
685        $(
686            #[allow(unused_parens)]
687            impl<T, U> Lcm<$name2<U>> for $name1<T>
688            where
689                $name1<T>: Abs,
690                $name2<U>: Abs,
691                Absolute<$name1<T>>: Mul<Absolute<$name2<U>>>,
692                Absolute<$name1<T>>: Gcd<Absolute<$name2<U>>>,
693                Product<Absolute<$name1<T>>, Absolute<$name2<U>>>:
694                    Div<GreatestCommonDivisor<Absolute<$name1<T>>, Absolute<$name2<U>>>>,
695            {
696                type Result = rpn!(
697                    ($name1<T>) abs ($name2<U>) abs * ($name1<T>) abs ($name2<U>) abs gcd /
698                );
699            }
700        )*
701    };
702}
703
704impl_lcm![(Next, Next), (Next, Prev), (Prev, Next), (Prev, Prev)];
705
706/// The least common multiple of `T` and `U`.
707pub type LeastCommonMultiple<T, U> = <T as Lcm<U>>::Result;
708
709/// Type-level absolute value.
710pub trait Abs {
711    /// The absolute value of `Self`.
712    type Result: NonNegative;
713}
714
715impl Abs for Zero {
716    type Result = Zero;
717}
718
719impl<T> Abs for Next<T>
720where
721    Self: Simplify,
722    Simplified<Self>: Positive,
723{
724    type Result = Simplified<Self>;
725}
726
727impl<T> Abs for Prev<T>
728where
729    Self: Simplify,
730    Simplified<Self>: Neg,
731    Negation<Simplified<Self>>: Positive,
732{
733    type Result = Negation<Simplified<Self>>;
734}
735
736/// The absolute value of `T`.
737pub type Absolute<T> = <T as Abs>::Result;
738
739/// Simplification of redundancies in type-level numbers.
740pub trait Simplify {
741    /// The simplification of `Self`.
742    type Result;
743}
744
745impl Simplify for Zero {
746    type Result = Zero;
747}
748
749impl Simplify for Next<Zero> {
750    type Result = Self;
751}
752
753impl Simplify for Prev<Zero> {
754    type Result = Self;
755}
756
757impl<T> Simplify for Next<Next<T>>
758where
759    Next<T>: Simplify,
760    Simplified<Next<T>>: Add<One>,
761{
762    type Result = Sum<Simplified<Next<T>>, One>;
763}
764
765impl<T> Simplify for Prev<Prev<T>>
766where
767    Prev<T>: Simplify,
768    Simplified<Prev<T>>: Sub<One>,
769{
770    type Result = Difference<Simplified<Prev<T>>, One>;
771}
772
773impl<T> Simplify for Next<Prev<T>>
774where
775    T: Simplify,
776{
777    type Result = Simplified<T>;
778}
779
780impl<T> Simplify for Prev<Next<T>>
781where
782    T: Simplify,
783{
784    type Result = Simplified<T>;
785}
786
787/// The simplification of `T`.
788pub type Simplified<T> = <T as Simplify>::Result;
789
790/// Positive type-level numbers.
791pub trait Positive: NonNegative + NonZero {}
792
793impl<T> Positive for T where T: NonNegative + NonZero {}
794
795/// Negative type-level numbers.
796pub trait Negative: NonPositive + NonZero {}
797
798impl<T> Negative for T where T: NonPositive + NonZero {}
799
800/// Non-negative type-level numbers.
801pub trait NonNegative {}
802
803impl NonNegative for Zero {}
804
805impl<T> NonNegative for Next<T>
806where
807    Self: Simplify,
808    Simplified<Self>: IsNotPrev,
809{
810}
811
812impl<T> NonNegative for Prev<T>
813where
814    Self: Simplify,
815    Simplified<Self>: IsNotPrev,
816{
817}
818
819/// Non-positive type-level numbers.
820pub trait NonPositive {}
821
822impl NonPositive for Zero {}
823
824impl<T> NonPositive for Next<T>
825where
826    Self: Simplify,
827    Simplified<Self>: IsNotNext,
828{
829}
830
831impl<T> NonPositive for Prev<T>
832where
833    Self: Simplify,
834    Simplified<Self>: IsNotNext,
835{
836}
837
838/// Non-zero type-level numbers.
839pub trait NonZero {}
840
841impl<T> NonZero for Next<T>
842where
843    Self: Simplify,
844    Simplified<Self>: IsNotZero,
845{
846}
847
848impl<T> NonZero for Prev<T>
849where
850    Self: Simplify,
851    Simplified<Self>: IsNotZero,
852{
853}
854
855#[doc(hidden)]
856#[macro_export]
857macro_rules! rpn_impl {
858   // Numerals
859   (((0            ) $($rest:tt)*) (            $($stack:tt)*)) => { $crate::rpn_impl!(($($rest)*) (($crate::Zero                         ) $($stack)*)) };
860   (((1            ) $($rest:tt)*) (            $($stack:tt)*)) => { $crate::rpn_impl!(($($rest)*) (($crate::One                          ) $($stack)*)) };
861   (((2            ) $($rest:tt)*) (            $($stack:tt)*)) => { $crate::rpn_impl!(($($rest)*) (($crate::Two                          ) $($stack)*)) };
862   (((3            ) $($rest:tt)*) (            $($stack:tt)*)) => { $crate::rpn_impl!(($($rest)*) (($crate::Three                        ) $($stack)*)) };
863   (((4            ) $($rest:tt)*) (            $($stack:tt)*)) => { $crate::rpn_impl!(($($rest)*) (($crate::Four                         ) $($stack)*)) };
864   (((5            ) $($rest:tt)*) (            $($stack:tt)*)) => { $crate::rpn_impl!(($($rest)*) (($crate::Five                         ) $($stack)*)) };
865   (((6            ) $($rest:tt)*) (            $($stack:tt)*)) => { $crate::rpn_impl!(($($rest)*) (($crate::Six                          ) $($stack)*)) };
866   (((7            ) $($rest:tt)*) (            $($stack:tt)*)) => { $crate::rpn_impl!(($($rest)*) (($crate::Seven                        ) $($stack)*)) };
867   (((8            ) $($rest:tt)*) (            $($stack:tt)*)) => { $crate::rpn_impl!(($($rest)*) (($crate::Eight                        ) $($stack)*)) };
868   (((9            ) $($rest:tt)*) (            $($stack:tt)*)) => { $crate::rpn_impl!(($($rest)*) (($crate::Nine                         ) $($stack)*)) };
869   (((10           ) $($rest:tt)*) (            $($stack:tt)*)) => { $crate::rpn_impl!(($($rest)*) (($crate::Ten                          ) $($stack)*)) };
870
871   // Standard operators
872   (((+            ) $($rest:tt)*) ($a:tt $b:tt $($stack:tt)*)) => { $crate::rpn_impl!(($($rest)*) (($crate::Sum<$b, $a>                  ) $($stack)*)) };
873   (((-            ) $($rest:tt)*) ($a:tt $b:tt $($stack:tt)*)) => { $crate::rpn_impl!(($($rest)*) (($crate::Difference<$b, $a>           ) $($stack)*)) };
874   (((*            ) $($rest:tt)*) ($a:tt $b:tt $($stack:tt)*)) => { $crate::rpn_impl!(($($rest)*) (($crate::Product<$b, $a>              ) $($stack)*)) };
875   (((/            ) $($rest:tt)*) ($a:tt $b:tt $($stack:tt)*)) => { $crate::rpn_impl!(($($rest)*) (($crate::Quotient<$b, $a>             ) $($stack)*)) };
876   (((%            ) $($rest:tt)*) ($a:tt $b:tt $($stack:tt)*)) => { $crate::rpn_impl!(($($rest)*) (($crate::Remainder<$b, $a>            ) $($stack)*)) };
877   (((~            ) $($rest:tt)*) ($a:tt       $($stack:tt)*)) => { $crate::rpn_impl!(($($rest)*) (($crate::Negation<$a>                 ) $($stack)*)) };
878   (((^            ) $($rest:tt)*) ($a:tt $b:tt $($stack:tt)*)) => { $crate::rpn_impl!(($($rest)*) (($crate::Exponent<$b, $a>             ) $($stack)*)) };
879
880   (((abs          ) $($rest:tt)*) ($a:tt       $($stack:tt)*)) => { $crate::rpn_impl!(($($rest)*) (($crate::Absolute<$a>                 ) $($stack)*)) };
881   (((gcd          ) $($rest:tt)*) ($a:tt $b:tt $($stack:tt)*)) => { $crate::rpn_impl!(($($rest)*) (($crate::GreatestCommonDivisor<$b, $a>) $($stack)*)) };
882   (((lcm          ) $($rest:tt)*) ($a:tt $b:tt $($stack:tt)*)) => { $crate::rpn_impl!(($($rest)*) (($crate::LeastCommonMultiple<$b, $a>  ) $($stack)*)) };
883   (((simplify     ) $($rest:tt)*) ($a:tt       $($stack:tt)*)) => { $crate::rpn_impl!(($($rest)*) (($crate::Simplified<$a>               ) $($stack)*)) };
884   (((fract        ) $($rest:tt)*) ($a:tt $b:tt $($stack:tt)*)) => { $crate::rpn_impl!(($($rest)*) (($crate::Fraction<$b, $a>             ) $($stack)*)) };
885   (((inv          ) $($rest:tt)*) ($a:tt       $($stack:tt)*)) => { $crate::rpn_impl!(($($rest)*) (($crate::Reciprocal<$a>               ) $($stack)*)) };
886   (((int          ) $($rest:tt)*) ($a:tt       $($stack:tt)*)) => { $crate::rpn_impl!(($($rest)*) (($crate::ToInt<$a>                    ) $($stack)*)) };
887   (((dup          ) $($rest:tt)*) ($a:tt       $($stack:tt)*)) => { $crate::rpn_impl!(($($rest)*) (($a               ) ($a               ) $($stack)*)) };
888
889   // Custom operators
890   ((([1 $op:ident]) $($rest:tt)*) ($a:tt       $($stack:tt)*)) => { $crate::rpn_impl!(($($rest)*) (($op<$a>                              ) $($stack)*)) };
891   ((([2 $op:ident]) $($rest:tt)*) ($a:tt $b:tt $($stack:tt)*)) => { $crate::rpn_impl!(($($rest)*) (($op<$b, $a>                          ) $($stack)*)) };
892
893   // Operands
894   ((($val:ty      ) $($rest:tt)*) (            $($stack:tt)*)) => { $crate::rpn_impl!(($($rest)*) ($val                                    $($stack)*)) };
895
896   // Done
897   ((                             ) ($val:tt                 )) => { $val };
898}
899
900/// Reverse polish notation representation for type-level numerical expressions.
901///
902/// Numbers from 0-10 inclusive can be represented with numerals, but others
903/// must be represented with parenthesised types (e.g. `(Next<Next<Ten>>)`).
904#[macro_export]
905macro_rules! rpn {
906    // Entry point
907    ($($t:tt)+) => { $crate::rpn_impl!(($(($t))+) ()) };
908}
909
910#[cfg(test)]
911mod test;
peano_axioms/lib.rs

peano_axioms/
lib.rs
