1pub trait All {}
279impl<T: ?Sized> All for T {}
280
281
282#[macro_export]
465macro_rules! type_operators {
466 ($gensym:tt $(#$docs:tt)* data $name:ident: $fbound:ident $(+ $bound:ident)* where $(#$attr:tt)+ { $($stuff:tt)* } $($rest:tt)*) => {
467 $(#$docs)*
468 pub trait $name: $fbound $(+ $bound)* {}
469
470 _tlsm_data!([$name ($fbound $(+ $bound)*) [] $($attr)*] $gensym $($stuff)*);
471 type_operators!($gensym $($rest)*);
472 };
473 ($gensym:tt $(#$docs:tt)* data $name:ident where $(#$attr:tt)+ { $($stuff:tt)* } $($rest:tt)*) => {
474 $(#$docs)*
475 pub trait $name {}
476
477 _tlsm_data!([$name () [] $($attr)*] $gensym $($stuff)*);
478 type_operators!($gensym $($rest)*);
479 };
480 ($gensym:tt $(#$docs:tt)* data $name:ident: $fbound:ident $(+ $bound:ident)* { $($stuff:tt)* } $($rest:tt)*) => {
481 $(#$docs)*
482 pub trait $name: $fbound $(+ $bound)* {}
483
484 _tlsm_data!([$name ($fbound $(+ $bound)*) []] $gensym $($stuff)*);
485 type_operators!($gensym $($rest)*);
486 };
487 ($gensym:tt $(#$docs:tt)* data $name:ident { $($stuff:tt)* } $($rest:tt)*) => {
488 $(#$docs)*
489 pub trait $name {}
490
491 _tlsm_data!([$name () []] $gensym $($stuff)*);
492 type_operators!($gensym $($rest)*);
493 };
494
495 ($gensym:tt $(#$docs:tt)* concrete $name:ident: $fbound:ident $(+ $bound:ident)* => $output:ty where $(#$attr:tt)+ { $($stuff:tt)* } $($rest:tt)*) => {
496 $(#$docs)*
497 pub trait $name: $fbound $(+ $bound)* {
498 fn reify() -> $output;
499 }
500
501 _tlsm_concrete!([$name ($fbound $(+ $bound)*) [] $($attr)*] $output; $gensym $($stuff)*);
502 type_operators!($gensym $($rest)*);
503 };
504 ($gensym:tt $(#$docs:tt)* concrete $name:ident => $output:ty where $(#$attr:tt)+ { $($stuff:tt)* } $($rest:tt)*) => {
505 $(#$docs)*
506 pub trait $name {
507 fn reify() -> $output;
508 }
509
510 _tlsm_concrete!([$name () [] $($attr)*] $output; $gensym $($stuff)*);
511 type_operators!($gensym $($rest)*);
512 };
513 ($gensym:tt $(#$docs:tt)* concrete $name:ident: $fbound:ident $(+ $bound:ident)* => $output:ty { $($stuff:tt)* } $($rest:tt)*) => {
514 $(#$docs)*
515 pub trait $name: $fbound $(+ $bound)* {
516 fn reify() -> $output;
517 }
518
519 _tlsm_concrete!([$name ($fbound $(+ $bound)*) []] $output; $gensym $($stuff)*);
520 type_operators!($gensym $($rest)*);
521 };
522 ($gensym:tt $(#$docs:tt)* concrete $name:ident => $output:ty { $($stuff:tt)* } $($rest:tt)*) => {
523 $(#$docs)*
524 pub trait $name {
525 fn reify() -> $output;
526 }
527
528 _tlsm_concrete!([$name () []] $output; $gensym $($stuff)*);
529 type_operators!($gensym $($rest)*);
530 };
531
532 ($gensym:tt $(#$docs:tt)* ($alias:ident) $machine:ident ($($kind:tt)*): $out:tt where $(#$attr:tt)* { $($states:tt)* } $($rest:tt)*) => {
533 _tlsm_machine!([$($docs)*] [$($attr)*] $alias $machine $gensym [$($kind)*] [] $out);
534 _tlsm_states!($machine [$($attr)*] $($states)*);
535
536 type_operators!($gensym $($rest)*);
537 };
538 ($gensym:tt $(#$docs:tt)* ($alias:ident) $machine:ident ($($kind:tt)*): $out:tt { $($states:tt)* } $($rest:tt)*) => {
539 _tlsm_machine!([$($docs)*] [] $alias $machine $gensym [$($kind)*] [] $out);
540 _tlsm_states!($machine [] $($states)*);
541
542 type_operators!($gensym $($rest)*);
543 };
544
545 ($gensym:tt) => {};
546}
547
548#[macro_export]
549macro_rules! _tlsm_parse_type {
550 ((@ $external:ident $arg:tt $($more:tt)+)) => {
551 <_tlsm_parse_type!($arg) as $external< $(_tlsm_parse_type!($more)),+ >>::Output
552 };
553 ((@ $external:ident $arg:tt)) => {
554 <_tlsm_parse_type!($arg) as $external>::Output
555 };
556 (($parameterized:ident $($arg:tt)*)) => {
557 $parameterized<$(_tlsm_parse_type!($arg)),*>
558 };
559 ($constant:ident) => {
560 $constant
561 };
562}
563
564#[macro_export]
565macro_rules! _tlsm_states {
566 (@bounds $attrs:tt $machine:ident $implinfo:tt [$($bounds:tt)*] [$($queue:tt)*] (& $arg:tt where $($extra:tt)*)) => {
567 _tlsm_states!(@bounds $attrs $machine $implinfo [$($bounds)* $($extra)*] [$($queue)*] $arg);
568 };
569 (@bounds $attrs:tt $machine:ident $implinfo:tt $bounds:tt [$($queue:tt)*] (% $arg:tt $($more:tt)*)) => {
570 _tlsm_states!(@bounds $attrs $machine $implinfo $bounds [$($more)* $($queue)*] $arg);
571 };
572 (@bounds $attrs:tt $machine:ident $implinfo:tt [$($bounds:tt)*] [$($queue:tt)*] (# $arg:tt $($more:tt)+)) => {
573 _tlsm_states!(@bounds $attrs $machine $implinfo
574 [$($bounds)* (_tlsm_states!(@output $machine $arg):
575 $machine< $(_tlsm_states!(@output $machine $more)),+ >)] [$($more)* $($queue)*] $arg);
576 };
577 (@bounds $attrs:tt $machine:ident $implinfo:tt [$($bounds:tt)*] [$($queue:tt)*] (@ $external:ident $arg:tt $($more:tt)+)) => {
578 _tlsm_states!(@bounds $attrs $machine $implinfo
579 [$($bounds)* (_tlsm_states!(@output $machine $arg):
580 $external< $(_tlsm_states!(@output $machine $more)),+ >)] [$($more)* $($queue)*] $arg);
581 };
582 (@bounds $attrs:tt $machine:ident $implinfo:tt [$($bounds:tt)*] [$($queue:tt)*] (# $arg:tt)) => {
583 _tlsm_states!(@bounds $attrs $machine $implinfo
584 [$($bounds)* (_tlsm_states!(@output $machine $arg): $machine)] [$($queue)*] $arg);
585 };
586 (@bounds $attrs:tt $machine:ident $implinfo:tt [$($bounds:tt)*] [$($queue:tt)*] (@ $external:ident $arg:tt)) => {
587 _tlsm_states!(@bounds $attrs $machine $implinfo
588 [$($bounds)* (_tlsm_states!(@output $machine $arg): $external)] [$($queue)*] $arg);
589 };
590 (@bounds $attrs:tt $machine:ident $implinfo:tt $bounds:tt [$($queue:tt)*] ($parameterized:ident $arg:tt $($args:tt)*)) => {
591 _tlsm_states!(@bounds $attrs $machine $implinfo $bounds [$($args)* $($queue)*] $arg);
592 };
593 (@bounds $attrs:tt $machine:ident $implinfo:tt $bounds:tt [$next:tt $($queue:tt)*] $constant:ident) => {
594 _tlsm_states!(@bounds $attrs $machine $implinfo $bounds [$($queue)*] $next);
595 };
596 (@bounds $attrs:tt $machine:ident { $($implinfo:tt)* } $bounds:tt [] $constant:ident) => {
597 _tlsm_states!(@implement $attrs $machine $bounds $($implinfo)*);
598 };
599 (@maybedefault $attrs:tt $machine:ident $quantified:tt [$($input:tt)*] => $output:tt) => {
600 _tlsm_states!(@bounds $attrs $machine { [] $quantified [$($input)*] => $output } [] [] $output);
601 };
602 (@maybedefault $attrs:tt $machine:ident $quantified:tt {$($input:tt)*} => $output:tt) => {
603 _tlsm_states!(@bounds $attrs $machine { [default] $quantified [$($input)*] => $output } [] [] $output);
604 };
605 (@dispatchgroup $attrs:tt $machine:ident $quantified:tt $($head:tt $body:tt $tail:tt)*) => {
606 $(_tlsm_states!(@dispatch $attrs $machine $quantified $head $body $tail);)*
607 };
608 (@dispatch [$($attr:meta)*] $machine:ident $quantified:tt # [$newattr:meta] { $($head:tt $body:tt $tail:tt)* }) => {
609 _tlsm_states!(@dispatchgroup [$($attr)* $newattr] $machine $quantified $($head $body $tail)*);
610 };
611 (@dispatch $attrs:tt $machine:ident ($(($lsym:ident: $lbound:tt))*) forall ($($rsym:ident: $rbound:tt),*) { $($head:tt $body:tt $tail:tt)* }) => {
612 _tlsm_states!(@dispatchgroup $attrs $machine ($(($lsym: $lbound))* $(($rsym: $rbound))*) $($head $body $tail)*);
613 };
614 (@dispatch $attrs:tt $machine:ident $quantified:tt $input:tt => $output:tt) => {
615 _tlsm_states!(@maybedefault $attrs $machine $quantified $input => $output);
616 };
617 (@implement [$($attr:meta)*] $machine:ident [$(($($constraint:tt)*))+] [$($default:tt)*] ($(($sym:ident: $bound:ident))+) [$head:tt $(, $input:tt)+] => $output:tt) => {
618 $(#[$attr])*
619 impl<$($sym: $bound),+> $machine< $(_tlsm_parse_type!($input)),+ > for _tlsm_parse_type!($head) where $($($constraint)*),+
620 {
621 $($default)* type Output = _tlsm_states!(@output $machine $output);
622 }
623 };
624 (@implement [$($attr:meta)*] $machine:ident [$(($($constraint:tt)*))+] [$($default:tt)*] ($(($sym:ident: $bound:ident))+) [$head:tt] => $output:tt) => {
625 $(#[$attr])*
626 impl<$($sym: $bound),+> $machine for _tlsm_parse_type!($head) where $($($constraint)*),+
627 {
628 $($default)* type Output = _tlsm_states!(@output $machine $output);
629 }
630 };
631 (@implement [$($attr:meta)*] $machine:ident [$(($($constraint:tt)*))+] [$($default:tt)*] () [$head:tt $(, $input:tt)+] => $output:tt) => {
632 $(#[$attr])*
633 impl $machine< $(_tlsm_parse_type!($input)),+ > for _tlsm_parse_type!($head) where $($($constraint)*),+
634 {
635 $($default)* type Output = _tlsm_states!(@output $machine $output);
636 }
637 };
638 (@implement [$($attr:meta)*] $machine:ident [$(($($constraint:tt)*))+] [$($default:tt)*] () [$head:tt] => $output:tt) => {
639 $(#[$attr])*
640 impl $machine for _tlsm_parse_type!($head) where $($($constraint)*),+
641 {
642 $($default)* type Output = _tlsm_states!(@output $machine $output);
643 }
644 };
645 (@implement [$($attr:meta)*] $machine:ident [] [$($default:tt)*] ($(($sym:ident: $bound:ident))+) [$head:tt $(, $input:tt)+] => $output:tt) => {
646 $(#[$attr])*
647 impl<$($sym: $bound),+> $machine< $(_tlsm_parse_type!($input)),+ > for _tlsm_parse_type!($head) {
648 $($default)* type Output = _tlsm_states!(@output $machine $output);
649 }
650 };
651 (@implement [$($attr:meta)*] $machine:ident [] [$($default:tt)*] ($(($sym:ident: $bound:ident))+) [$head:tt] => $output:tt) => {
652 $(#[$attr])*
653 impl<$($sym: $bound),+> $machine for _tlsm_parse_type!($head) {
654 $($default)* type Output = _tlsm_states!(@output $machine $output);
655 }
656 };
657 (@implement [$($attr:meta)*] $machine:ident [] [$($default:tt)*] () [$head:tt $(, $input:tt)+] => $output:tt) => {
658 $(#[$attr])*
659 impl $machine< $(_tlsm_parse_type!($input)),+ > for _tlsm_parse_type!($head) {
660 $($default)* type Output = _tlsm_states!(@output $machine $output);
661 }
662 };
663 (@implement [$($attr:meta)*] $machine:ident [] [$($default:tt)*] () [$head:tt] => $output:tt) => {
664 $(#[$attr])*
665 impl $machine for _tlsm_parse_type!($head) {
666 $($default)* type Output = _tlsm_states!(@output $machine $output);
667 }
668 };
669 (@output $machine:ident (& $arg:tt $($extra:tt)*)) => {
670 _tlsm_states!(@output $machine $arg)
671 };
672 (@output $machine:ident (# $arg:tt $($more:tt)+)) => {
673 <_tlsm_states!(@output $machine $arg) as $machine< $(_tlsm_states!(@output $machine $more)),+ >>::Output
674 };
675 (@output $machine:ident (# $arg:tt)) => {
676 <_tlsm_states!(@output $machine $arg) as $machine>::Output
677 };
678 (@output $machine:ident (% $arg:tt $($more:tt)+)) => {
679 <_tlsm_states!(@output $machine $arg) as $machine< $(_tlsm_states!(@output $machine $more)),+ >>::Output
680 };
681 (@output $machine:ident (% $arg:tt)) => {
682 <_tlsm_states!(@output $machine $arg) as $machine>::Output
683 };
684 (@output $machine:ident (@ $external:ident $arg:tt $($more:tt)+)) => {
685 <_tlsm_states!(@output $machine $arg) as $external< $(_tlsm_states!(@output $machine $more)),+ >>::Output
686 };
687 (@output $machine:ident (@ $external:ident $arg:tt)) => {
688 <_tlsm_states!(@output $machine $arg) as $external>::Output
689 };
690 (@output $machine:ident ($parameterized:ident $($arg:tt)+)) => {
691 $parameterized<$(_tlsm_states!(@output $machine $arg)),+>
692 };
693 (@output $machine:ident $constant:ident) => {
694 $constant
695 };
696 (@reduceattrs [$($attr:tt)*] [$($specific:tt)*] $machine:ident $head:tt $body:tt $tail:tt) => {
697 _tlsm_states!(@dispatch [$($attr)* $($specific)*] $machine () $head $body $tail);
698 };
699 ($machine:ident $attrs:tt $($(# $specific:tt)* $head:tt $body:tt $tail:tt)*) => {
700 $(_tlsm_states!(@reduceattrs $attrs [$($specific)*] $machine $head $body $tail);)*
701 };
702}
703
704#[macro_export]
705macro_rules! _tlsm_machine {
706 ([$($docs:tt)*] $attrs:tt $alias:ident $machine:ident [$gensym:ident $(, $gensyms:ident)*] [_ , $($kinds:tt)+] [$($accum:tt)*] $out:tt) => {
707 _tlsm_machine!(@cont [$($docs)*] $attrs $alias $machine [$($gensyms),*] [$($kinds)+] [$($accum)* ($gensym)] $out);
708 };
709 (@cont $docs:tt $attrs:tt $alias:ident $machine:ident [$gensym:ident $(, $gensyms:ident)*] [_ , $($kinds:tt)+] [$($accum:tt)*] $out:tt) => {
710 _tlsm_machine!(@cont $docs $attrs $alias $machine [$($gensyms),*] [$($kinds)+] [$($accum)* ($gensym)] $out);
711 };
712 ([$($docs:tt)*] $attrs:tt $alias:ident $machine:ident [$gensym:ident $(, $gensyms:ident)*] [_] [$($accum:tt)*] $out:tt) => {
713 _tlsm_machine!(@cont [$($docs)*] $attrs $alias $machine [$($gensyms),*] [] [$($accum)* ($gensym)] $out);
714 };
715 (@cont $docs:tt $attrs:tt $alias:ident $machine:ident [$gensym:ident $(, $gensyms:ident)*] [_] [$($accum:tt)*] $out:tt) => {
716 _tlsm_machine!(@cont $docs $attrs $alias $machine [$($gensyms),*] [] [$($accum)* ($gensym)] $out);
717 };
718 ([$($docs:tt)*] $attrs:tt $alias:ident $machine:ident $gensym:tt [$ksym:ident: _ , $($kinds:tt)+] [$($accum:tt)*] $out:tt) => {
719 First parameter cannot be named; use Self instead.
720 };
721 (@cont $docs:tt $attrs:tt $alias:ident $machine:ident $gensym:tt [$ksym:ident: _ , $($kinds:tt)+] [$($accum:tt)*] $out:tt) => {
722 _tlsm_machine!(@cont $docs $attrs $alias $machine $gensym [$($kinds)+] [$($accum)* ($ksym)] $out);
723 };
724 ([$($docs:tt)*] $attrs:tt $alias:ident $machine:ident $gensym:tt [$ksym:ident: _] [$($accum:tt)*] $out:tt) => {
725 First parameter cannot be named; use Self instead.
726 };
727 (@cont $docs:tt $attrs:tt $alias:ident $machine:ident $gensym:tt [$ksym:ident: _] [$($accum:tt)*] $out:tt) => {
728 _tlsm_machine!(@cont $docs $attrs $alias $machine $gensym [] [$($accum)* ($ksym)] $out);
729 };
730 ([$($docs:tt)*] $attrs:tt $alias:ident $machine:ident $gensym:tt [$ksym:ident: $kind:tt, $($kinds:tt)+] [$($accum:tt)*] $out:tt) => {
731 First parameter cannot be named; use Self instead.
732 };
733 (@cont $docs:tt $attrs:tt $alias:ident $machine:ident $gensym:tt [$ksym:ident: $kind:tt, $($kinds:tt)+] [$($accum:tt)*] $out:tt) => {
734 _tlsm_machine!(@cont $docs $attrs $alias $machine $gensym [$($kinds)+] [$($accum)* ($ksym: $kind)] $out);
735 };
736 ([$($docs:tt)*] $attrs:tt $alias:ident $machine:ident $gensym:tt [$ksym:ident: $kind:tt] [$($accum:tt)*] $out:tt) => {
737 First parameter cannot be named; use Self instead.
738 };
739 (@cont $docs:tt $attrs:tt $alias:ident $machine:ident $gensym:tt [$ksym:ident: $kind:tt] [$($accum:tt)*] $out:tt) => {
740 _tlsm_machine!(@cont $docs $attrs $alias $machine $gensym [] [$($accum)* ($ksym: $kind)] $out);
741 };
742 ([$($docs:tt)*] $attrs:tt $alias:ident $machine:ident [$gensym:ident $(, $gensyms:ident)*] [$kind:tt , $($kinds:tt)+] [$($accum:tt)*] $out:tt) => {
743 _tlsm_machine!(@cont [$($docs)*] $attrs $alias $machine [$($gensyms),*] [$($kinds)+] [$($accum)* ($gensym: $kind)] $out);
744 };
745 (@cont $docs:tt $attrs:tt $alias:ident $machine:ident [$gensym:ident $(, $gensyms:ident)*] [$kind:tt , $($kinds:tt)+] [$($accum:tt)*] $out:tt) => {
746 _tlsm_machine!(@cont $docs $attrs $alias $machine [$($gensyms),*] [$($kinds)+] [$($accum)* ($gensym: $kind)] $out);
747 };
748 ([$($docs:tt)*] $attrs:tt $alias:ident $machine:ident [$gensym:ident $(, $gensyms:ident)*] [$kind:tt] [$($accum:tt)*] $out:tt) => {
749 _tlsm_machine!(@cont [$($docs)*] $attrs $alias $machine [$($gensyms),*] [] [$($accum)* ($gensym: $kind)] $out);
750 };
751 (@cont $docs:tt $attrs:tt $alias:ident $machine:ident [$gensym:ident $(, $gensyms:ident)*] [$kind:tt] [$($accum:tt)*] $out:tt) => {
752 _tlsm_machine!(@cont $docs $attrs $alias $machine [$($gensyms),*] [] [$($accum)* ($gensym: $kind)] $out);
753 };
754 (@cont [$($docs:tt)*] [$($attr:tt)*] $alias:ident $machine:ident $gensym:tt [] [($fsym:ident $($fbound:tt)*) $(($sym:ident $($bound:tt)*))+] _) => {
755 $(#$docs)*
756 $(#$attr)*
757 pub trait $machine < $($sym $($bound)*),+ > $($fbound)* {
758 type Output;
759 }
760
761 $(#$attr)*
762 pub type $alias < $fsym $($fbound)* $(, $sym $($bound)*)+ > = <$fsym as $machine< $($sym),+ >>::Output;
763 };
764 (@cont [$($docs:tt)*] [$($attr:tt)*] $alias:ident $machine:ident $gensym:tt [] [($fsym:ident $($fbound:tt)*)] _) => {
765 $(#$docs)*
766 $(#$attr)*
767 pub trait $machine $($fbound)* {
768 type Output;
769 }
770
771 $(#$attr)*
772 pub type $alias < $fsym $($fbound)* > = <$fsym as $machine>::Output;
773 };
774 (@cont [$($docs:tt)*] [$($attr:tt)*] $alias:ident $machine:ident $gensym:tt [] [($fsym:ident $($fbound:tt)*) $(($sym:ident $($bound:tt)*))+] ($parameterized:ident $($param:tt)*)) => {
775 $(#$docs)*
776 $(#$attr)*
777 pub trait $machine < $($sym $($bound)*),+ > $($fbound)* {
778 type Output: $parameterized<$(_tlsm_parse_type!($param)),*>;
779 }
780
781 $(#$attr)*
782 pub type $alias < $fsym $($fbound)* $(, $sym $($bound)*)+ > = <$fsym as $machine< $($sym),+ >>::Output;
783 };
784 (@cont [$($docs:tt)*] [$($attr:tt)*] $alias:ident $machine:ident $gensym:tt [] [($fsym:ident $($fbound:tt)*)] ($parameterized:ident $($param:tt)*)) => {
785 $(#$docs)*
786 $(#$attr)*
787 pub trait $machine $($fbound)* {
788 type Output: $parameterized<$(_tlsm_parse_type!($param)),*>;
789 }
790
791 $(#$attr)*
792 pub type $alias < $fsym $($fbound)* > = <$fsym as $machine>::Output;
793 };
794 (@cont [$($docs:tt)*] [$($attr:tt)*] $alias:ident $machine:ident $gensym:tt [] [($fsym:ident $($fbound:tt)*) $(($sym:ident $($bound:tt)*))+] $out:ident) => {
795 $(#$docs)*
796 $(#$attr)*
797 pub trait $machine < $($sym $($bound)*),+ > $($fbound)* {
798 type Output: $out;
799 }
800
801 $(#$attr)*
802 pub type $alias < $fsym $($fbound)* $(, $sym $($bound)*)+ > = <$fsym as $machine< $($sym),+ >>::Output;
803 };
804 (@cont [$($docs:tt)*] [$($attr:tt)*] $alias:ident $machine:ident $gensym:tt [] [($fsym:ident $($fbound:tt)*)] $out:ident) => {
805 $(#$docs)*
806 $(#$attr)*
807 pub trait $machine $($fbound)* {
808 type Output: $out;
809 }
810
811 $(#$attr)*
812 pub type $alias < $fsym $($fbound)* > = <$fsym as $machine>::Output;
813 };
814}
815
816#[macro_export]
817macro_rules! _tlsm_meta_filter_struct {
818 ([$($preceding:tt)*] #[struct: $attr:meta] $($more:tt)*) => (_tlsm_meta_filter_struct!([$($preceding)* #[$attr]] $($more)*););
819 ([$($preceding:tt)*] #$attr:tt $($more:tt)*) => (_tlsm_meta_filter_struct!([$($preceding)* #$attr] $($more)*););
820 ([$($preceding:tt)*] $($decl:tt)*) => ($($preceding)* $($decl)*);
821}
822
823#[macro_export]
824macro_rules! _tlsm_meta_filter_impl {
825 ([$($preceding:tt)*] #[impl: $attr:meta] $($more:tt)*) => (_tlsm_meta_filter_impl!([$($preceding)* #[$attr]] $($more)*););
826 ($preceding:tt #[derive $traits:tt] $($more:tt)*) => (_tlsm_meta_filter_impl!($preceding $($more)*);); ([$($preceding:tt)*] #$attr:tt $($more:tt)*) => (_tlsm_meta_filter_impl!([$($preceding)* #$attr] $($more)*););
828 ([$($preceding:tt)*] $($decl:tt)*) => ($($preceding)* $($decl)*);
829}
830
831#[macro_export]
832macro_rules! _tlsm_data {
833 ($attrs:tt @parameterized $name:ident [$gensym:ident $(, $next:ident)*] [$($args:tt)*] [$($bounds:tt)*] [$($phantom:tt)*] _) => {
834 _tlsm_data!($attrs @parameterized $name [$($next),*] [$($args)* ($gensym)] [$($bounds)* ($gensym)] [$($phantom)* ($gensym)]);
835 };
836 ($attrs:tt @parameterized $name:ident [$gensym:ident $(, $next:ident)*] [$($args:tt)*] [$($bounds:tt)*] [$($phantom:tt)*] _ , $($rest:tt)*) => {
837 _tlsm_data!($attrs @parameterized $name [$($next),*] [$($args)* ($gensym)] [$($bounds)* ($gensym)] [$($phantom)* ($gensym)] $($rest)*);
838 };
839 ($attrs:tt @parameterized $name:ident [$gensym:ident $(, $next:ident)*] [$($args:tt)*] [$($bounds:tt)*] [$($phantom:tt)*] $kind:ident = $default:ty) => {
840 _tlsm_data!($attrs @parameterized $name [$($next),*] [$($args)* ($gensym: $kind = $default)] [$($bounds)* ($gensym: $kind)] [$($phantom)* ($gensym)]);
841 };
842 ($attrs:tt @parameterized $name:ident [$gensym:ident $(, $next:ident)*] [$($args:tt)*] [$($bounds:tt)*] [$($phantom:tt)*] $kind:ident = $default:ty , $($rest:tt)*) => {
843 _tlsm_data!($attrs @parameterized $name [$($next),*] [$($args)* ($gensym: $kind = $default)] [$($bounds)* ($gensym: $kind)] [$($phantom)* ($gensym)] $($rest)*);
844 };
845 ($attrs:tt @parameterized $name:ident [$gensym:ident $(, $next:ident)*] [$($args:tt)*] [$($bounds:tt)*] [$($phantom:tt)*] $kind:ident) => {
846 _tlsm_data!($attrs @parameterized $name [$($next),*] [$($args)* ($gensym: $kind)] [$($bounds)* ($gensym: $kind)] [$($phantom)* ($gensym)]);
847 };
848 ($attrs:tt @parameterized $name:ident [$gensym:ident $(, $next:ident)*] [$($args:tt)*] [$($bounds:tt)*] [$($phantom:tt)*] $kind:ident , $($rest:tt)*) => {
849 _tlsm_data!($attrs @parameterized $name [$($next),*] [$($args)* ($gensym: $kind)] [$($bounds)* ($gensym: $kind)] [$($phantom)* ($gensym)] $($rest)*);
850 };
851 ([$group:ident $derives:tt [$($specific:tt)*] $($attr:tt)*] @parameterized $name:ident $gensyms:tt [$(($asym:ident $($args:tt)*))*] [$(($bsym:ident $($bounds:tt)*))*] [$(($($phantom:tt)*))*]) => {
852 _tlsm_meta_filter_struct! { []
853 $(#$attr)*
854 $(#$specific)*
855
856 pub struct $name < $($asym $($args)*),* >($(::std::marker::PhantomData<$($phantom)*>),*);
857 }
858
859 _tlsm_meta_filter_impl! { []
860 $(#$attr)*
861 $(#$specific)*
862
863 impl< $($bsym $($bounds)*),* > $group for $name<$($($phantom)*),*> {}
864 }
865 };
866 ([$group:ident $derives:tt [$($specific:tt)*] $($attr:tt)*] $gensym:tt # $nextspecific:tt $($rest:tt)*) => {
867 _tlsm_data!([$group $derives [$($specific)* $nextspecific] $($attr)*] $gensym $($rest)*);
868 };
869 ([$group:ident () [$($specific:tt)*] $($attr:tt)*] $gensym:tt DEFAULT, $($rest:tt)*) => {
870 _tlsm_meta_filter_impl! { []
871 $(#$attr)*
872 $(#$specific)*
873
874 impl<T> $group for T {}
875 }
876
877 _tlsm_data!([$group () [] $($attr)*] $gensym $($rest)*);
878 };
879 ([$group:ident ($fbound:ident $(+ $bound:ident)*) [$($specific:tt)*] $($attr:tt)*] $gensym:tt DEFAULT, $($rest:tt)*) => {
880 _tlsm_meta_filter_impl! { []
881 $(#$attr)*
882 $(#$specific)*
883
884 impl<T> $group for T where T: $fbound $(+ $bound)* {}
885 }
886
887 _tlsm_data!([$group ($fbound $(+ $bound)*) [] $($attr)*] $gensym $($rest)*);
888 };
889 ([$group:ident $derives:tt [$($specific:tt)*] $($attr:tt)*] $gensym:tt $name:ident, $($rest:tt)*) => {
890 _tlsm_meta_filter_struct! { []
891 $(#$attr)*
892 $(#$specific)*
893
894 pub struct $name;
895 }
896
897 _tlsm_meta_filter_impl! { []
898 $(#$attr)*
899 $(#$specific)*
900
901 impl $group for $name {}
902 }
903
904 _tlsm_data!([$group $derives [] $($attr)*] $gensym $($rest)*);
905 };
906 ([$group:ident $derives:tt [$($specific:tt)*] $($attr:tt)*] $gensym:tt $name:ident($($args:tt)*), $($rest:tt)*) => {
907 _tlsm_data!([$group $derives [$($specific)*] $($attr)*] @parameterized $name $gensym [] [] [] $($args)*);
908 _tlsm_data!([$group $derives [] $($attr)*] $gensym $($rest)*);
909 };
910 ($attrs:tt $gensym:tt) => {};
911}
912
913#[macro_export]
914macro_rules! _tlsm_concrete {
915 ($attrs:tt $output:ty; @parameterized $name:ident => $value:expr; $gensym:tt [$($args:tt)*] [$($bounds:tt)*] [$($syms:ident)*] $sym:ident: $kind:ident = $default:ty) => {
916 _tlsm_concrete!($attrs $output; @parameterized $name => $value; $gensym [$($args)* ($sym: $kind = $default)] [$($bounds)* ($sym: $kind)] [$($syms)* $sym]);
917 };
918 ($attrs:tt $output:ty; @parameterized $name:ident => $value:expr; $gensym:tt [$($args:tt)*] [$($bounds:tt)*] [$($syms:ident)*] $sym:ident: $kind:ident = $default:ty , $($rest:tt)*) => {
919 _tlsm_concrete!($attrs $output; @parameterized $name => $value; $gensym [$($args)* ($sym: $kind = $default)] [$($bounds)* ($sym: $kind)] [$($syms)* $sym] $($rest)*);
920 };
921 ($attrs:tt $output:ty; @parameterized $name:ident => $value:expr; $gensym:tt [$($args:tt)*] [$($bounds:tt)*] [$($syms:ident)*] $sym:ident: $kind:ident) => {
922 _tlsm_concrete!($attrs $output; @parameterized $name => $value; $gensym [$($args)* ($sym: $kind)] [$($bounds)* ($sym: $kind)] [$($syms)* $sym]);
923 };
924 ($attrs:tt $output:ty; @parameterized $name:ident => $value:expr; $gensym:tt [$($args:tt)*] [$($bounds:tt)*] [$($syms:ident)*] $sym:ident: $kind:ident , $($rest:tt)*) => {
925 _tlsm_concrete!($attrs $output; @parameterized $name => $value; $gensym [$($args)* ($sym: $kind)] [$($bounds)* ($sym: $kind)] [$($syms)* $sym] $($rest)*);
926 };
927 ($attrs:tt $output:ty; @parameterized $name:ident => $value:expr; [$gensym:ident $(, $next:ident)*] [$($args:tt)*] [$($bounds:tt)*] $syms:tt $kind:ident = $default:ty) => {
928 _tlsm_concrete!($attrs $output; @parameterized $name => $value; [$($next),*] [$($args)* ($gensym: $kind = $default)] [$($bounds)* ($gensym: $kind)] $syms);
929 };
930 ($attrs:tt $output:ty; @parameterized $name:ident => $value:expr; [$gensym:ident $(, $next:ident)*] [$($args:tt)*] [$($bounds:tt)*] $syms:tt $kind:ident = $default:ty , $($rest:tt)*) => {
931 _tlsm_concrete!($attrs $output; @parameterized $name => $value; [$($next),*] [$($args)* ($gensym: $kind = $default)] [$($bounds)* ($gensym: $kind)] $syms $($rest)*);
932 };
933 ($attrs:tt $output:ty; @parameterized $name:ident => $value:expr; [$gensym:ident $(, $next:ident)*] [$($args:tt)*] [$($bounds:tt)*] $syms:tt $kind:ident) => {
934 _tlsm_concrete!($attrs $output; @parameterized $name => $value; [$($next),*] [$($args)* ($gensym: $kind)] [$($bounds)* ($gensym: $kind)] $syms);
935 };
936 ($attrs:tt $output:ty; @parameterized $name:ident => $value:expr; [$gensym:ident $(, $next:ident)*] [$($args:tt)*] [$($bounds:tt)*] $syms:tt $kind:ident , $($rest:tt)*) => {
937 _tlsm_concrete!($attrs $output; @parameterized $name => $value; [$($next),*] [$($args)* ($gensym: $kind)] [$($bounds)* ($gensym: $kind)] $syms $($rest)*);
938 };
939 ([$group:ident $derives:tt [$($specific:tt)*] $($attr:tt)*] $output:ty; $gensym:tt # $nextspecific:tt $($rest:tt)*) => {
940 _tlsm_concrete!([$group $derives [$($specific)* $nextspecific] $($attr)*] $output; $gensym $($rest)*);
941 };
942 ([$group:ident $derives:tt [$($specific:tt)*] $($attr:tt)*] $output:ty; @parameterized $name:ident => $value:expr; $gensyms:tt [$(($tysym:ident: $($args:tt)*))*] [$(($bsym:ident: $bound:ident))*] [$($sym:ident)*]) => {
943 _tlsm_meta_filter_struct! { []
944 $(#$attr)*
945 $(#$specific)*
946 pub struct $name < $($tysym: $($args)*),* >($(::std::marker::PhantomData<$tysym>),*);
947 }
948
949 _tlsm_meta_filter_impl! { []
950 $(#$attr)*
951 $(#$specific)*
952 impl< $($bsym: $bound),* > $group for $name<$($bsym),*> {
953 #[allow(non_snake_case)]
954 fn reify() -> $output { $(let $sym = <$sym>::reify();)* $value }
955 }
956 }
957 };
958 ([$group:ident () [$($specific:tt)*] $($attr:tt)*] $output:ty; $gensym:tt DEFAULT => $value:expr, $($rest:tt)*) => {
959 _tlsm_meta_filter_impl! { []
960 $(#$attr)*
961 $(#$specific)*
962 impl<T> $group for T {
963 default fn reify() -> $output { $value }
964 }
965 }
966
967 _tlsm_concrete!([$group () [] $($attr)*] $output; $gensym $($rest)*);
968 };
969 ([$group:ident ($fbound:ident $(+ $bound:ident)*) [$($specific:tt)*] $($attr:tt)*] $output:ty; $gensym:tt DEFAULT => $value:expr, $($rest:tt)*) => {
970 _tlsm_meta_filter_impl! { []
971 $(#$attr)*
972 $(#$specific)*
973 impl<T> $group for T where T: $fbound $(+ $bound)* {
974 default fn reify() -> $output { $value }
975 }
976 }
977
978 _tlsm_concrete!([$group ($fbound $(+ $bound)*) [] $($attr)*] $output; $gensym $($rest)*);
979 };
980 ([$group:ident $derives:tt [$($specific:tt)*] $($attr:tt)*] $output:ty; $gensym:tt $name:ident => $value:expr, $($rest:tt)*) => {
981 _tlsm_meta_filter_struct! { []
982 $(#$attr)*
983 $(#$specific)*
984 pub struct $name;
985 }
986
987 _tlsm_meta_filter_impl! { []
988 $(#$attr)*
989 $(#$specific)*
990 impl $group for $name {
991 fn reify() -> $output { $value }
992 }
993 }
994
995 _tlsm_concrete!([$group $derives [] $($attr)*] $output; $gensym $($rest)*);
996 };
997 ([$group:ident $derives:tt [$($specific:tt)*] $($attr:tt)*] $output:ty; $gensym:tt $name:ident($($args:tt)*) => $value:expr, $($rest:tt)*) => {
998 _tlsm_concrete!([$group $derives [$($specific)*] $($attr)*] $output; @parameterized $name => $value; $gensym [] [] [] $($args)*);
999 _tlsm_concrete!([$group $derives [] $($attr)*] $output; $gensym $($rest)*);
1000 };
1001 ($attrs:tt $output:ty; $gensym:tt) => {};
1002}
1003
1004
1005#[cfg(test)]
1006mod tests_1 {
1007 use super::*;
1008
1009 type_operators! {
1010 [A, B, C, D, E]
1011
1012 concrete Nat => usize {
1013 P => 0,
1014 I(N: Nat = P) => 1 + 2 * N,
1015 O(N: Nat = P) => 2 * N,
1016 Undefined => panic!("Undefined type-level arithmetic result!"),
1017 }
1018 concrete Bool => bool {
1022 False => false,
1023 True => true,
1024 }
1025 (Pred) Predecessor(Nat): Nat {
1026 [Undefined] => Undefined
1027 [P] => Undefined
1028 forall (N: Nat) {
1029 [(O N)] => (I (# N))
1030 [(I N)] => (O N)
1031 }
1032 }
1033 (Succ) Successor(Nat): Nat {
1034 [Undefined] => Undefined
1035 [P] => I
1036 forall (N: Nat) {
1037 [(O N)] => (I N)
1038 [(I N)] => (O (# N))
1039 }
1040 }
1041 (Sum) Adding(Nat, Nat): Nat {
1042 [P, P] => P
1043 forall (N: Nat) {
1044 [(O N), P] => (O N)
1045 [(I N), P] => (I N)
1046 [P, (O N)] => (O N)
1047 [P, (I N)] => (I N)
1048 }
1049 forall (N: Nat, M: Nat) {
1050 [(O M), (O N)] => (O (# M N))
1051 [(I M), (O N)] => (I (# M N))
1052 [(O M), (I N)] => (I (# M N))
1053 [(I M), (I N)] => (O (# (# M N) I))
1054 }
1055 }
1056 (Difference) Subtracting(Nat, Nat): Nat {
1057 forall (N: Nat) {
1058 [N, P] => N
1059 }
1060 forall (N: Nat, M: Nat) {
1061 [(O M), (O N)] => (O (# M N))
1062 [(I M), (O N)] => (I (# M N))
1063 [(O M), (I N)] => (I (# (# M N) I))
1064 [(I M), (I N)] => (O (# M N))
1065 }
1066 }
1067 (Product) Multiplying(Nat, Nat): Nat {
1068 forall (N: Nat) {
1069 [P, N] => P
1070 }
1071 forall (N: Nat, M: Nat) {
1072 [(O M), N] => (# M (O N))
1073 [(I M), N] => (@Adding N (# M (O N)))
1074 }
1075 }
1076 (If) NatIf(Bool, Nat, Nat): Nat {
1077 forall (T: Nat, U: Nat) {
1078 [True, T, U] => T
1079 [False, T, U] => U
1080 }
1081 }
1082 (NatIsUndef) NatIsUndefined(Nat): Bool {
1083 [Undefined] => True
1084 [P] => False
1085 forall (M: Nat) {
1086 [(O M)] => False
1087 [(I M)] => False
1088 }
1089 }
1090 (NatUndef) NatUndefined(Nat, Nat): Nat {
1091 forall (M: Nat) {
1092 [Undefined, M] => Undefined
1093 [P, M] => M
1094 }
1095 forall (M: Nat, N: Nat) {
1096 [(O N), M] => M
1097 [(I N), M] => M
1098 }
1099 }
1100 (TotalDifference) TotalSubtracting(Nat, Nat): Nat {
1101 [P, P] => P
1102 [Undefined, P] => Undefined
1103 forall (N: Nat) {
1104 [N, Undefined] => Undefined
1105 [P, (O N)] => (# P N)
1106 [P, (I N)] => Undefined
1107 [(O N), P] => (O N)
1108 [(I N), P] => (I N)
1109 [Undefined, (O N)] => Undefined
1110 [Undefined, (I N)] => Undefined
1111 }
1112 forall (N: Nat, M: Nat) {
1113 [(O M), (O N)] => (@NatUndefined (# M N) (O (# M N)))
1114 [(I M), (O N)] => (@NatUndefined (# M N) (I (# M N)))
1115 [(O M), (I N)] => (@NatUndefined (# (# M N) I) (I (# (# M N) I)))
1116 [(I M), (I N)] => (@NatUndefined (# M N) (O (# M N)))
1117 }
1118 }
1119 (Quotient) Quotienting(Nat, Nat): Nat {
1120 forall (D: Nat) {
1121 [Undefined, D] => Undefined
1122 [P, D] => (@NatIf (@NatIsUndefined (@TotalSubtracting P D)) O (@Successor (# (@TotalSubtracting P D) D)))
1123 }
1124 forall (N: Nat, D: Nat) {
1125 [(O N), D] => (@NatIf (@NatIsUndefined (@TotalSubtracting (O N) D)) O (@Successor (# (@TotalSubtracting (O N) D) D)))
1126 [(I N), D] => (@NatIf (@NatIsUndefined (@TotalSubtracting (I N) D)) O (@Successor (# (@TotalSubtracting (I N) D) D)))
1127 }
1128 }
1129 (Remainder) Remaindering(Nat, Nat): Nat {
1130 forall (D: Nat) {
1131 [Undefined, D] => Undefined
1132 [P, D] => (@NatIf (@NatIsUndefined (@TotalSubtracting P D)) P (# (@TotalSubtracting P D) D))
1133 }
1134 forall (N: Nat, D: Nat) {
1135 [(O N), D] => (@NatIf (@NatIsUndefined (@TotalSubtracting (O N) D)) (O N) (# (@TotalSubtracting (O N) D) D))
1136 [(I N), D] => (@NatIf (@NatIsUndefined (@TotalSubtracting (I N) D)) (I O) (# (@TotalSubtracting (I N) D) D))
1137 }
1138 }
1139 }
1140
1141 fn invariants() {
1142 assert_eq!(<I<I> as Nat>::reify(), 3);
1143 assert_eq!(<I<O<I>> as Nat>::reify(), 5);
1144 assert_eq!(<Sum<I<O<I>>, I<I>> as Nat>::reify(), 8);
1145 assert_eq!(<Difference<I<I>, O<I>> as Nat>::reify(), 1);
1146 assert_eq!(<Difference<O<O<O<I>>>, I<I>> as Nat>::reify(), 5);
1147 assert_eq!(<Product<I<I>, I<O<I>>> as Nat>::reify(), 15);
1148 assert_eq!(<Quotient<I<I>, O<I>> as Nat>::reify(), 1);
1149 assert_eq!(<Remainder<I<O<O<I>>>, O<O<I>>> as Nat>::reify(), 1);
1150 }
1151}
1152
1153#[cfg(test)]
1154mod tests_2 {
1155 use super::*;
1156
1157 type_operators! {
1158 [A, B, C, D, E]
1159
1160 data Nat {
1161 P,
1162 I(Nat = P),
1163 O(Nat = P),
1164 }
1165 }
1166}