pub trait All {}
impl<T: ?Sized> All for T {}
#[macro_export]
macro_rules! type_operators {
($gensym:tt $(#$docs:tt)* data $name:ident: $fbound:ident $(+ $bound:ident)* where $(#$attr:tt)+ { $($stuff:tt)* } $($rest:tt)*) => {
$(#$docs)*
pub trait $name: $fbound $(+ $bound)* {}
_tlsm_data!([$name ($fbound $(+ $bound)*) [] $($attr)*] $gensym $($stuff)*);
type_operators!($gensym $($rest)*);
};
($gensym:tt $(#$docs:tt)* data $name:ident where $(#$attr:tt)+ { $($stuff:tt)* } $($rest:tt)*) => {
$(#$docs)*
pub trait $name {}
_tlsm_data!([$name () [] $($attr)*] $gensym $($stuff)*);
type_operators!($gensym $($rest)*);
};
($gensym:tt $(#$docs:tt)* data $name:ident: $fbound:ident $(+ $bound:ident)* { $($stuff:tt)* } $($rest:tt)*) => {
$(#$docs)*
pub trait $name: $fbound $(+ $bound)* {}
_tlsm_data!([$name ($fbound $(+ $bound)*) []] $gensym $($stuff)*);
type_operators!($gensym $($rest)*);
};
($gensym:tt $(#$docs:tt)* data $name:ident { $($stuff:tt)* } $($rest:tt)*) => {
$(#$docs)*
pub trait $name {}
_tlsm_data!([$name () []] $gensym $($stuff)*);
type_operators!($gensym $($rest)*);
};
($gensym:tt $(#$docs:tt)* concrete $name:ident: $fbound:ident $(+ $bound:ident)* => $output:ty where $(#$attr:tt)+ { $($stuff:tt)* } $($rest:tt)*) => {
$(#$docs)*
pub trait $name: $fbound $(+ $bound)* {
fn reify() -> $output;
}
_tlsm_concrete!([$name ($fbound $(+ $bound)*) [] $($attr)*] $output; $gensym $($stuff)*);
type_operators!($gensym $($rest)*);
};
($gensym:tt $(#$docs:tt)* concrete $name:ident => $output:ty where $(#$attr:tt)+ { $($stuff:tt)* } $($rest:tt)*) => {
$(#$docs)*
pub trait $name {
fn reify() -> $output;
}
_tlsm_concrete!([$name () [] $($attr)*] $output; $gensym $($stuff)*);
type_operators!($gensym $($rest)*);
};
($gensym:tt $(#$docs:tt)* concrete $name:ident: $fbound:ident $(+ $bound:ident)* => $output:ty { $($stuff:tt)* } $($rest:tt)*) => {
$(#$docs)*
pub trait $name: $fbound $(+ $bound)* {
fn reify() -> $output;
}
_tlsm_concrete!([$name ($fbound $(+ $bound)*) []] $output; $gensym $($stuff)*);
type_operators!($gensym $($rest)*);
};
($gensym:tt $(#$docs:tt)* concrete $name:ident => $output:ty { $($stuff:tt)* } $($rest:tt)*) => {
$(#$docs)*
pub trait $name {
fn reify() -> $output;
}
_tlsm_concrete!([$name () []] $output; $gensym $($stuff)*);
type_operators!($gensym $($rest)*);
};
($gensym:tt $(#$docs:tt)* ($alias:ident) $machine:ident ($($kind:tt)*): $out:tt where $(#$attr:tt)* { $($states:tt)* } $($rest:tt)*) => {
_tlsm_machine!([$($docs)*] [$($attr)*] $alias $machine $gensym [$($kind)*] [] $out);
_tlsm_states!($machine [$($attr)*] $($states)*);
type_operators!($gensym $($rest)*);
};
($gensym:tt $(#$docs:tt)* ($alias:ident) $machine:ident ($($kind:tt)*): $out:tt { $($states:tt)* } $($rest:tt)*) => {
_tlsm_machine!([$($docs)*] [] $alias $machine $gensym [$($kind)*] [] $out);
_tlsm_states!($machine [] $($states)*);
type_operators!($gensym $($rest)*);
};
($gensym:tt) => {};
}
#[macro_export]
macro_rules! _tlsm_parse_type {
((@ $external:ident $arg:tt $($more:tt)+)) => {
<_tlsm_parse_type!($arg) as $external< $(_tlsm_parse_type!($more)),+ >>::Output
};
((@ $external:ident $arg:tt)) => {
<_tlsm_parse_type!($arg) as $external>::Output
};
(($parameterized:ident $($arg:tt)*)) => {
$parameterized<$(_tlsm_parse_type!($arg)),*>
};
($constant:ident) => {
$constant
};
}
#[macro_export]
macro_rules! _tlsm_states {
(@bounds $attrs:tt $machine:ident $implinfo:tt [$($bounds:tt)*] [$($queue:tt)*] (& $arg:tt where $($extra:tt)*)) => {
_tlsm_states!(@bounds $attrs $machine $implinfo [$($bounds)* $($extra)*] [$($queue)*] $arg);
};
(@bounds $attrs:tt $machine:ident $implinfo:tt $bounds:tt [$($queue:tt)*] (% $arg:tt $($more:tt)*)) => {
_tlsm_states!(@bounds $attrs $machine $implinfo $bounds [$($more)* $($queue)*] $arg);
};
(@bounds $attrs:tt $machine:ident $implinfo:tt [$($bounds:tt)*] [$($queue:tt)*] (# $arg:tt $($more:tt)+)) => {
_tlsm_states!(@bounds $attrs $machine $implinfo
[$($bounds)* (_tlsm_states!(@output $machine $arg):
$machine< $(_tlsm_states!(@output $machine $more)),+ >)] [$($more)* $($queue)*] $arg);
};
(@bounds $attrs:tt $machine:ident $implinfo:tt [$($bounds:tt)*] [$($queue:tt)*] (@ $external:ident $arg:tt $($more:tt)+)) => {
_tlsm_states!(@bounds $attrs $machine $implinfo
[$($bounds)* (_tlsm_states!(@output $machine $arg):
$external< $(_tlsm_states!(@output $machine $more)),+ >)] [$($more)* $($queue)*] $arg);
};
(@bounds $attrs:tt $machine:ident $implinfo:tt [$($bounds:tt)*] [$($queue:tt)*] (# $arg:tt)) => {
_tlsm_states!(@bounds $attrs $machine $implinfo
[$($bounds)* (_tlsm_states!(@output $machine $arg): $machine)] [$($queue)*] $arg);
};
(@bounds $attrs:tt $machine:ident $implinfo:tt [$($bounds:tt)*] [$($queue:tt)*] (@ $external:ident $arg:tt)) => {
_tlsm_states!(@bounds $attrs $machine $implinfo
[$($bounds)* (_tlsm_states!(@output $machine $arg): $external)] [$($queue)*] $arg);
};
(@bounds $attrs:tt $machine:ident $implinfo:tt $bounds:tt [$($queue:tt)*] ($parameterized:ident $arg:tt $($args:tt)*)) => {
_tlsm_states!(@bounds $attrs $machine $implinfo $bounds [$($args)* $($queue)*] $arg);
};
(@bounds $attrs:tt $machine:ident $implinfo:tt $bounds:tt [$next:tt $($queue:tt)*] $constant:ident) => {
_tlsm_states!(@bounds $attrs $machine $implinfo $bounds [$($queue)*] $next);
};
(@bounds $attrs:tt $machine:ident { $($implinfo:tt)* } $bounds:tt [] $constant:ident) => {
_tlsm_states!(@implement $attrs $machine $bounds $($implinfo)*);
};
(@maybedefault $attrs:tt $machine:ident $quantified:tt [$($input:tt)*] => $output:tt) => {
_tlsm_states!(@bounds $attrs $machine { [] $quantified [$($input)*] => $output } [] [] $output);
};
(@maybedefault $attrs:tt $machine:ident $quantified:tt {$($input:tt)*} => $output:tt) => {
_tlsm_states!(@bounds $attrs $machine { [default] $quantified [$($input)*] => $output } [] [] $output);
};
(@dispatchgroup $attrs:tt $machine:ident $quantified:tt $($head:tt $body:tt $tail:tt)*) => {
$(_tlsm_states!(@dispatch $attrs $machine $quantified $head $body $tail);)*
};
(@dispatch [$($attr:meta)*] $machine:ident $quantified:tt # [$newattr:meta] { $($head:tt $body:tt $tail:tt)* }) => {
_tlsm_states!(@dispatchgroup [$($attr)* $newattr] $machine $quantified $($head $body $tail)*);
};
(@dispatch $attrs:tt $machine:ident ($(($lsym:ident: $lbound:tt))*) forall ($($rsym:ident: $rbound:tt),*) { $($head:tt $body:tt $tail:tt)* }) => {
_tlsm_states!(@dispatchgroup $attrs $machine ($(($lsym: $lbound))* $(($rsym: $rbound))*) $($head $body $tail)*);
};
(@dispatch $attrs:tt $machine:ident $quantified:tt $input:tt => $output:tt) => {
_tlsm_states!(@maybedefault $attrs $machine $quantified $input => $output);
};
(@implement [$($attr:meta)*] $machine:ident [$(($($constraint:tt)*))+] [$($default:tt)*] ($(($sym:ident: $bound:ident))+) [$head:tt $(, $input:tt)+] => $output:tt) => {
$(#[$attr])*
impl<$($sym: $bound),+> $machine< $(_tlsm_parse_type!($input)),+ > for _tlsm_parse_type!($head) where $($($constraint)*),+
{
$($default)* type Output = _tlsm_states!(@output $machine $output);
}
};
(@implement [$($attr:meta)*] $machine:ident [$(($($constraint:tt)*))+] [$($default:tt)*] ($(($sym:ident: $bound:ident))+) [$head:tt] => $output:tt) => {
$(#[$attr])*
impl<$($sym: $bound),+> $machine for _tlsm_parse_type!($head) where $($($constraint)*),+
{
$($default)* type Output = _tlsm_states!(@output $machine $output);
}
};
(@implement [$($attr:meta)*] $machine:ident [$(($($constraint:tt)*))+] [$($default:tt)*] () [$head:tt $(, $input:tt)+] => $output:tt) => {
$(#[$attr])*
impl $machine< $(_tlsm_parse_type!($input)),+ > for _tlsm_parse_type!($head) where $($($constraint)*),+
{
$($default)* type Output = _tlsm_states!(@output $machine $output);
}
};
(@implement [$($attr:meta)*] $machine:ident [$(($($constraint:tt)*))+] [$($default:tt)*] () [$head:tt] => $output:tt) => {
$(#[$attr])*
impl $machine for _tlsm_parse_type!($head) where $($($constraint)*),+
{
$($default)* type Output = _tlsm_states!(@output $machine $output);
}
};
(@implement [$($attr:meta)*] $machine:ident [] [$($default:tt)*] ($(($sym:ident: $bound:ident))+) [$head:tt $(, $input:tt)+] => $output:tt) => {
$(#[$attr])*
impl<$($sym: $bound),+> $machine< $(_tlsm_parse_type!($input)),+ > for _tlsm_parse_type!($head) {
$($default)* type Output = _tlsm_states!(@output $machine $output);
}
};
(@implement [$($attr:meta)*] $machine:ident [] [$($default:tt)*] ($(($sym:ident: $bound:ident))+) [$head:tt] => $output:tt) => {
$(#[$attr])*
impl<$($sym: $bound),+> $machine for _tlsm_parse_type!($head) {
$($default)* type Output = _tlsm_states!(@output $machine $output);
}
};
(@implement [$($attr:meta)*] $machine:ident [] [$($default:tt)*] () [$head:tt $(, $input:tt)+] => $output:tt) => {
$(#[$attr])*
impl $machine< $(_tlsm_parse_type!($input)),+ > for _tlsm_parse_type!($head) {
$($default)* type Output = _tlsm_states!(@output $machine $output);
}
};
(@implement [$($attr:meta)*] $machine:ident [] [$($default:tt)*] () [$head:tt] => $output:tt) => {
$(#[$attr])*
impl $machine for _tlsm_parse_type!($head) {
$($default)* type Output = _tlsm_states!(@output $machine $output);
}
};
(@output $machine:ident (& $arg:tt $($extra:tt)*)) => {
_tlsm_states!(@output $machine $arg)
};
(@output $machine:ident (# $arg:tt $($more:tt)+)) => {
<_tlsm_states!(@output $machine $arg) as $machine< $(_tlsm_states!(@output $machine $more)),+ >>::Output
};
(@output $machine:ident (# $arg:tt)) => {
<_tlsm_states!(@output $machine $arg) as $machine>::Output
};
(@output $machine:ident (% $arg:tt $($more:tt)+)) => {
<_tlsm_states!(@output $machine $arg) as $machine< $(_tlsm_states!(@output $machine $more)),+ >>::Output
};
(@output $machine:ident (% $arg:tt)) => {
<_tlsm_states!(@output $machine $arg) as $machine>::Output
};
(@output $machine:ident (@ $external:ident $arg:tt $($more:tt)+)) => {
<_tlsm_states!(@output $machine $arg) as $external< $(_tlsm_states!(@output $machine $more)),+ >>::Output
};
(@output $machine:ident (@ $external:ident $arg:tt)) => {
<_tlsm_states!(@output $machine $arg) as $external>::Output
};
(@output $machine:ident ($parameterized:ident $($arg:tt)+)) => {
$parameterized<$(_tlsm_states!(@output $machine $arg)),+>
};
(@output $machine:ident $constant:ident) => {
$constant
};
(@reduceattrs [$($attr:tt)*] [$($specific:tt)*] $machine:ident $head:tt $body:tt $tail:tt) => {
_tlsm_states!(@dispatch [$($attr)* $($specific)*] $machine () $head $body $tail);
};
($machine:ident $attrs:tt $($(# $specific:tt)* $head:tt $body:tt $tail:tt)*) => {
$(_tlsm_states!(@reduceattrs $attrs [$($specific)*] $machine $head $body $tail);)*
};
}
#[macro_export]
macro_rules! _tlsm_machine {
([$($docs:tt)*] $attrs:tt $alias:ident $machine:ident [$gensym:ident $(, $gensyms:ident)*] [_ , $($kinds:tt)+] [$($accum:tt)*] $out:tt) => {
_tlsm_machine!(@cont [$($docs)*] $attrs $alias $machine [$($gensyms),*] [$($kinds)+] [$($accum)* ($gensym)] $out);
};
(@cont $docs:tt $attrs:tt $alias:ident $machine:ident [$gensym:ident $(, $gensyms:ident)*] [_ , $($kinds:tt)+] [$($accum:tt)*] $out:tt) => {
_tlsm_machine!(@cont $docs $attrs $alias $machine [$($gensyms),*] [$($kinds)+] [$($accum)* ($gensym)] $out);
};
([$($docs:tt)*] $attrs:tt $alias:ident $machine:ident [$gensym:ident $(, $gensyms:ident)*] [_] [$($accum:tt)*] $out:tt) => {
_tlsm_machine!(@cont [$($docs)*] $attrs $alias $machine [$($gensyms),*] [] [$($accum)* ($gensym)] $out);
};
(@cont $docs:tt $attrs:tt $alias:ident $machine:ident [$gensym:ident $(, $gensyms:ident)*] [_] [$($accum:tt)*] $out:tt) => {
_tlsm_machine!(@cont $docs $attrs $alias $machine [$($gensyms),*] [] [$($accum)* ($gensym)] $out);
};
([$($docs:tt)*] $attrs:tt $alias:ident $machine:ident $gensym:tt [$ksym:ident: _ , $($kinds:tt)+] [$($accum:tt)*] $out:tt) => {
First parameter cannot be named; use Self instead.
};
(@cont $docs:tt $attrs:tt $alias:ident $machine:ident $gensym:tt [$ksym:ident: _ , $($kinds:tt)+] [$($accum:tt)*] $out:tt) => {
_tlsm_machine!(@cont $docs $attrs $alias $machine $gensym [$($kinds)+] [$($accum)* ($ksym)] $out);
};
([$($docs:tt)*] $attrs:tt $alias:ident $machine:ident $gensym:tt [$ksym:ident: _] [$($accum:tt)*] $out:tt) => {
First parameter cannot be named; use Self instead.
};
(@cont $docs:tt $attrs:tt $alias:ident $machine:ident $gensym:tt [$ksym:ident: _] [$($accum:tt)*] $out:tt) => {
_tlsm_machine!(@cont $docs $attrs $alias $machine $gensym [] [$($accum)* ($ksym)] $out);
};
([$($docs:tt)*] $attrs:tt $alias:ident $machine:ident $gensym:tt [$ksym:ident: $kind:tt, $($kinds:tt)+] [$($accum:tt)*] $out:tt) => {
First parameter cannot be named; use Self instead.
};
(@cont $docs:tt $attrs:tt $alias:ident $machine:ident $gensym:tt [$ksym:ident: $kind:tt, $($kinds:tt)+] [$($accum:tt)*] $out:tt) => {
_tlsm_machine!(@cont $docs $attrs $alias $machine $gensym [$($kinds)+] [$($accum)* ($ksym: $kind)] $out);
};
([$($docs:tt)*] $attrs:tt $alias:ident $machine:ident $gensym:tt [$ksym:ident: $kind:tt] [$($accum:tt)*] $out:tt) => {
First parameter cannot be named; use Self instead.
};
(@cont $docs:tt $attrs:tt $alias:ident $machine:ident $gensym:tt [$ksym:ident: $kind:tt] [$($accum:tt)*] $out:tt) => {
_tlsm_machine!(@cont $docs $attrs $alias $machine $gensym [] [$($accum)* ($ksym: $kind)] $out);
};
([$($docs:tt)*] $attrs:tt $alias:ident $machine:ident [$gensym:ident $(, $gensyms:ident)*] [$kind:tt , $($kinds:tt)+] [$($accum:tt)*] $out:tt) => {
_tlsm_machine!(@cont [$($docs)*] $attrs $alias $machine [$($gensyms),*] [$($kinds)+] [$($accum)* ($gensym: $kind)] $out);
};
(@cont $docs:tt $attrs:tt $alias:ident $machine:ident [$gensym:ident $(, $gensyms:ident)*] [$kind:tt , $($kinds:tt)+] [$($accum:tt)*] $out:tt) => {
_tlsm_machine!(@cont $docs $attrs $alias $machine [$($gensyms),*] [$($kinds)+] [$($accum)* ($gensym: $kind)] $out);
};
([$($docs:tt)*] $attrs:tt $alias:ident $machine:ident [$gensym:ident $(, $gensyms:ident)*] [$kind:tt] [$($accum:tt)*] $out:tt) => {
_tlsm_machine!(@cont [$($docs)*] $attrs $alias $machine [$($gensyms),*] [] [$($accum)* ($gensym: $kind)] $out);
};
(@cont $docs:tt $attrs:tt $alias:ident $machine:ident [$gensym:ident $(, $gensyms:ident)*] [$kind:tt] [$($accum:tt)*] $out:tt) => {
_tlsm_machine!(@cont $docs $attrs $alias $machine [$($gensyms),*] [] [$($accum)* ($gensym: $kind)] $out);
};
(@cont [$($docs:tt)*] [$($attr:tt)*] $alias:ident $machine:ident $gensym:tt [] [($fsym:ident $($fbound:tt)*) $(($sym:ident $($bound:tt)*))+] _) => {
$(#$docs)*
$(#$attr)*
pub trait $machine < $($sym $($bound)*),+ > $($fbound)* {
type Output;
}
$(#$attr)*
pub type $alias < $fsym $($fbound)* $(, $sym $($bound)*)+ > = <$fsym as $machine< $($sym),+ >>::Output;
};
(@cont [$($docs:tt)*] [$($attr:tt)*] $alias:ident $machine:ident $gensym:tt [] [($fsym:ident $($fbound:tt)*)] _) => {
$(#$docs)*
$(#$attr)*
pub trait $machine $($fbound)* {
type Output;
}
$(#$attr)*
pub type $alias < $fsym $($fbound)* > = <$fsym as $machine>::Output;
};
(@cont [$($docs:tt)*] [$($attr:tt)*] $alias:ident $machine:ident $gensym:tt [] [($fsym:ident $($fbound:tt)*) $(($sym:ident $($bound:tt)*))+] ($parameterized:ident $($param:tt)*)) => {
$(#$docs)*
$(#$attr)*
pub trait $machine < $($sym $($bound)*),+ > $($fbound)* {
type Output: $parameterized<$(_tlsm_parse_type!($param)),*>;
}
$(#$attr)*
pub type $alias < $fsym $($fbound)* $(, $sym $($bound)*)+ > = <$fsym as $machine< $($sym),+ >>::Output;
};
(@cont [$($docs:tt)*] [$($attr:tt)*] $alias:ident $machine:ident $gensym:tt [] [($fsym:ident $($fbound:tt)*)] ($parameterized:ident $($param:tt)*)) => {
$(#$docs)*
$(#$attr)*
pub trait $machine $($fbound)* {
type Output: $parameterized<$(_tlsm_parse_type!($param)),*>;
}
$(#$attr)*
pub type $alias < $fsym $($fbound)* > = <$fsym as $machine>::Output;
};
(@cont [$($docs:tt)*] [$($attr:tt)*] $alias:ident $machine:ident $gensym:tt [] [($fsym:ident $($fbound:tt)*) $(($sym:ident $($bound:tt)*))+] $out:ident) => {
$(#$docs)*
$(#$attr)*
pub trait $machine < $($sym $($bound)*),+ > $($fbound)* {
type Output: $out;
}
$(#$attr)*
pub type $alias < $fsym $($fbound)* $(, $sym $($bound)*)+ > = <$fsym as $machine< $($sym),+ >>::Output;
};
(@cont [$($docs:tt)*] [$($attr:tt)*] $alias:ident $machine:ident $gensym:tt [] [($fsym:ident $($fbound:tt)*)] $out:ident) => {
$(#$docs)*
$(#$attr)*
pub trait $machine $($fbound)* {
type Output: $out;
}
$(#$attr)*
pub type $alias < $fsym $($fbound)* > = <$fsym as $machine>::Output;
};
}
#[macro_export]
macro_rules! _tlsm_meta_filter_struct {
([$($preceding:tt)*] #[struct: $attr:meta] $($more:tt)*) => (_tlsm_meta_filter_struct!([$($preceding)* #[$attr]] $($more)*););
([$($preceding:tt)*] #$attr:tt $($more:tt)*) => (_tlsm_meta_filter_struct!([$($preceding)* #$attr] $($more)*););
([$($preceding:tt)*] $($decl:tt)*) => ($($preceding)* $($decl)*);
}
#[macro_export]
macro_rules! _tlsm_meta_filter_impl {
([$($preceding:tt)*] #[impl: $attr:meta] $($more:tt)*) => (_tlsm_meta_filter_impl!([$($preceding)* #[$attr]] $($more)*););
($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)*););
([$($preceding:tt)*] $($decl:tt)*) => ($($preceding)* $($decl)*);
}
#[macro_export]
macro_rules! _tlsm_data {
($attrs:tt @parameterized $name:ident [$gensym:ident $(, $next:ident)*] [$($args:tt)*] [$($bounds:tt)*] [$($phantom:tt)*] _) => {
_tlsm_data!($attrs @parameterized $name [$($next),*] [$($args)* ($gensym)] [$($bounds)* ($gensym)] [$($phantom)* ($gensym)]);
};
($attrs:tt @parameterized $name:ident [$gensym:ident $(, $next:ident)*] [$($args:tt)*] [$($bounds:tt)*] [$($phantom:tt)*] _ , $($rest:tt)*) => {
_tlsm_data!($attrs @parameterized $name [$($next),*] [$($args)* ($gensym)] [$($bounds)* ($gensym)] [$($phantom)* ($gensym)] $($rest)*);
};
($attrs:tt @parameterized $name:ident [$gensym:ident $(, $next:ident)*] [$($args:tt)*] [$($bounds:tt)*] [$($phantom:tt)*] $kind:ident = $default:ty) => {
_tlsm_data!($attrs @parameterized $name [$($next),*] [$($args)* ($gensym: $kind = $default)] [$($bounds)* ($gensym: $kind)] [$($phantom)* ($gensym)]);
};
($attrs:tt @parameterized $name:ident [$gensym:ident $(, $next:ident)*] [$($args:tt)*] [$($bounds:tt)*] [$($phantom:tt)*] $kind:ident = $default:ty , $($rest:tt)*) => {
_tlsm_data!($attrs @parameterized $name [$($next),*] [$($args)* ($gensym: $kind = $default)] [$($bounds)* ($gensym: $kind)] [$($phantom)* ($gensym)] $($rest)*);
};
($attrs:tt @parameterized $name:ident [$gensym:ident $(, $next:ident)*] [$($args:tt)*] [$($bounds:tt)*] [$($phantom:tt)*] $kind:ident) => {
_tlsm_data!($attrs @parameterized $name [$($next),*] [$($args)* ($gensym: $kind)] [$($bounds)* ($gensym: $kind)] [$($phantom)* ($gensym)]);
};
($attrs:tt @parameterized $name:ident [$gensym:ident $(, $next:ident)*] [$($args:tt)*] [$($bounds:tt)*] [$($phantom:tt)*] $kind:ident , $($rest:tt)*) => {
_tlsm_data!($attrs @parameterized $name [$($next),*] [$($args)* ($gensym: $kind)] [$($bounds)* ($gensym: $kind)] [$($phantom)* ($gensym)] $($rest)*);
};
([$group:ident $derives:tt [$($specific:tt)*] $($attr:tt)*] @parameterized $name:ident $gensyms:tt [$(($asym:ident $($args:tt)*))*] [$(($bsym:ident $($bounds:tt)*))*] [$(($($phantom:tt)*))*]) => {
_tlsm_meta_filter_struct! { []
$(#$attr)*
$(#$specific)*
pub struct $name < $($asym $($args)*),* >($(::std::marker::PhantomData<$($phantom)*>),*);
}
_tlsm_meta_filter_impl! { []
$(#$attr)*
$(#$specific)*
impl< $($bsym $($bounds)*),* > $group for $name<$($($phantom)*),*> {}
}
};
([$group:ident $derives:tt [$($specific:tt)*] $($attr:tt)*] $gensym:tt # $nextspecific:tt $($rest:tt)*) => {
_tlsm_data!([$group $derives [$($specific)* $nextspecific] $($attr)*] $gensym $($rest)*);
};
([$group:ident () [$($specific:tt)*] $($attr:tt)*] $gensym:tt DEFAULT, $($rest:tt)*) => {
_tlsm_meta_filter_impl! { []
$(#$attr)*
$(#$specific)*
impl<T> $group for T {}
}
_tlsm_data!([$group () [] $($attr)*] $gensym $($rest)*);
};
([$group:ident ($fbound:ident $(+ $bound:ident)*) [$($specific:tt)*] $($attr:tt)*] $gensym:tt DEFAULT, $($rest:tt)*) => {
_tlsm_meta_filter_impl! { []
$(#$attr)*
$(#$specific)*
impl<T> $group for T where T: $fbound $(+ $bound)* {}
}
_tlsm_data!([$group ($fbound $(+ $bound)*) [] $($attr)*] $gensym $($rest)*);
};
([$group:ident $derives:tt [$($specific:tt)*] $($attr:tt)*] $gensym:tt $name:ident, $($rest:tt)*) => {
_tlsm_meta_filter_struct! { []
$(#$attr)*
$(#$specific)*
pub struct $name;
}
_tlsm_meta_filter_impl! { []
$(#$attr)*
$(#$specific)*
impl $group for $name {}
}
_tlsm_data!([$group $derives [] $($attr)*] $gensym $($rest)*);
};
([$group:ident $derives:tt [$($specific:tt)*] $($attr:tt)*] $gensym:tt $name:ident($($args:tt)*), $($rest:tt)*) => {
_tlsm_data!([$group $derives [$($specific)*] $($attr)*] @parameterized $name $gensym [] [] [] $($args)*);
_tlsm_data!([$group $derives [] $($attr)*] $gensym $($rest)*);
};
($attrs:tt $gensym:tt) => {};
}
#[macro_export]
macro_rules! _tlsm_concrete {
($attrs:tt $output:ty; @parameterized $name:ident => $value:expr; $gensym:tt [$($args:tt)*] [$($bounds:tt)*] [$($syms:ident)*] $sym:ident: $kind:ident = $default:ty) => {
_tlsm_concrete!($attrs $output; @parameterized $name => $value; $gensym [$($args)* ($sym: $kind = $default)] [$($bounds)* ($sym: $kind)] [$($syms)* $sym]);
};
($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)*) => {
_tlsm_concrete!($attrs $output; @parameterized $name => $value; $gensym [$($args)* ($sym: $kind = $default)] [$($bounds)* ($sym: $kind)] [$($syms)* $sym] $($rest)*);
};
($attrs:tt $output:ty; @parameterized $name:ident => $value:expr; $gensym:tt [$($args:tt)*] [$($bounds:tt)*] [$($syms:ident)*] $sym:ident: $kind:ident) => {
_tlsm_concrete!($attrs $output; @parameterized $name => $value; $gensym [$($args)* ($sym: $kind)] [$($bounds)* ($sym: $kind)] [$($syms)* $sym]);
};
($attrs:tt $output:ty; @parameterized $name:ident => $value:expr; $gensym:tt [$($args:tt)*] [$($bounds:tt)*] [$($syms:ident)*] $sym:ident: $kind:ident , $($rest:tt)*) => {
_tlsm_concrete!($attrs $output; @parameterized $name => $value; $gensym [$($args)* ($sym: $kind)] [$($bounds)* ($sym: $kind)] [$($syms)* $sym] $($rest)*);
};
($attrs:tt $output:ty; @parameterized $name:ident => $value:expr; [$gensym:ident $(, $next:ident)*] [$($args:tt)*] [$($bounds:tt)*] $syms:tt $kind:ident = $default:ty) => {
_tlsm_concrete!($attrs $output; @parameterized $name => $value; [$($next),*] [$($args)* ($gensym: $kind = $default)] [$($bounds)* ($gensym: $kind)] $syms);
};
($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)*) => {
_tlsm_concrete!($attrs $output; @parameterized $name => $value; [$($next),*] [$($args)* ($gensym: $kind = $default)] [$($bounds)* ($gensym: $kind)] $syms $($rest)*);
};
($attrs:tt $output:ty; @parameterized $name:ident => $value:expr; [$gensym:ident $(, $next:ident)*] [$($args:tt)*] [$($bounds:tt)*] $syms:tt $kind:ident) => {
_tlsm_concrete!($attrs $output; @parameterized $name => $value; [$($next),*] [$($args)* ($gensym: $kind)] [$($bounds)* ($gensym: $kind)] $syms);
};
($attrs:tt $output:ty; @parameterized $name:ident => $value:expr; [$gensym:ident $(, $next:ident)*] [$($args:tt)*] [$($bounds:tt)*] $syms:tt $kind:ident , $($rest:tt)*) => {
_tlsm_concrete!($attrs $output; @parameterized $name => $value; [$($next),*] [$($args)* ($gensym: $kind)] [$($bounds)* ($gensym: $kind)] $syms $($rest)*);
};
([$group:ident $derives:tt [$($specific:tt)*] $($attr:tt)*] $output:ty; $gensym:tt # $nextspecific:tt $($rest:tt)*) => {
_tlsm_concrete!([$group $derives [$($specific)* $nextspecific] $($attr)*] $output; $gensym $($rest)*);
};
([$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)*]) => {
_tlsm_meta_filter_struct! { []
$(#$attr)*
$(#$specific)*
pub struct $name < $($tysym: $($args)*),* >($(::std::marker::PhantomData<$tysym>),*);
}
_tlsm_meta_filter_impl! { []
$(#$attr)*
$(#$specific)*
impl< $($bsym: $bound),* > $group for $name<$($bsym),*> {
#[allow(non_snake_case)]
fn reify() -> $output { $(let $sym = <$sym>::reify();)* $value }
}
}
};
([$group:ident () [$($specific:tt)*] $($attr:tt)*] $output:ty; $gensym:tt DEFAULT => $value:expr, $($rest:tt)*) => {
_tlsm_meta_filter_impl! { []
$(#$attr)*
$(#$specific)*
impl<T> $group for T {
default fn reify() -> $output { $value }
}
}
_tlsm_concrete!([$group () [] $($attr)*] $output; $gensym $($rest)*);
};
([$group:ident ($fbound:ident $(+ $bound:ident)*) [$($specific:tt)*] $($attr:tt)*] $output:ty; $gensym:tt DEFAULT => $value:expr, $($rest:tt)*) => {
_tlsm_meta_filter_impl! { []
$(#$attr)*
$(#$specific)*
impl<T> $group for T where T: $fbound $(+ $bound)* {
default fn reify() -> $output { $value }
}
}
_tlsm_concrete!([$group ($fbound $(+ $bound)*) [] $($attr)*] $output; $gensym $($rest)*);
};
([$group:ident $derives:tt [$($specific:tt)*] $($attr:tt)*] $output:ty; $gensym:tt $name:ident => $value:expr, $($rest:tt)*) => {
_tlsm_meta_filter_struct! { []
$(#$attr)*
$(#$specific)*
pub struct $name;
}
_tlsm_meta_filter_impl! { []
$(#$attr)*
$(#$specific)*
impl $group for $name {
fn reify() -> $output { $value }
}
}
_tlsm_concrete!([$group $derives [] $($attr)*] $output; $gensym $($rest)*);
};
([$group:ident $derives:tt [$($specific:tt)*] $($attr:tt)*] $output:ty; $gensym:tt $name:ident($($args:tt)*) => $value:expr, $($rest:tt)*) => {
_tlsm_concrete!([$group $derives [$($specific)*] $($attr)*] $output; @parameterized $name => $value; $gensym [] [] [] $($args)*);
_tlsm_concrete!([$group $derives [] $($attr)*] $output; $gensym $($rest)*);
};
($attrs:tt $output:ty; $gensym:tt) => {};
}
#[cfg(test)]
mod tests_1 {
use super::*;
type_operators! {
[A, B, C, D, E]
concrete Nat => usize {
P => 0,
I(N: Nat = P) => 1 + 2 * N,
O(N: Nat = P) => 2 * N,
Undefined => panic!("Undefined type-level arithmetic result!"),
}
concrete Bool => bool {
False => false,
True => true,
}
(Pred) Predecessor(Nat): Nat {
[Undefined] => Undefined
[P] => Undefined
forall (N: Nat) {
[(O N)] => (I (# N))
[(I N)] => (O N)
}
}
(Succ) Successor(Nat): Nat {
[Undefined] => Undefined
[P] => I
forall (N: Nat) {
[(O N)] => (I N)
[(I N)] => (O (# N))
}
}
(Sum) Adding(Nat, Nat): Nat {
[P, P] => P
forall (N: Nat) {
[(O N), P] => (O N)
[(I N), P] => (I N)
[P, (O N)] => (O N)
[P, (I N)] => (I N)
}
forall (N: Nat, M: Nat) {
[(O M), (O N)] => (O (# M N))
[(I M), (O N)] => (I (# M N))
[(O M), (I N)] => (I (# M N))
[(I M), (I N)] => (O (# (# M N) I))
}
}
(Difference) Subtracting(Nat, Nat): Nat {
forall (N: Nat) {
[N, P] => N
}
forall (N: Nat, M: Nat) {
[(O M), (O N)] => (O (# M N))
[(I M), (O N)] => (I (# M N))
[(O M), (I N)] => (I (# (# M N) I))
[(I M), (I N)] => (O (# M N))
}
}
(Product) Multiplying(Nat, Nat): Nat {
forall (N: Nat) {
[P, N] => P
}
forall (N: Nat, M: Nat) {
[(O M), N] => (# M (O N))
[(I M), N] => (@Adding N (# M (O N)))
}
}
(If) NatIf(Bool, Nat, Nat): Nat {
forall (T: Nat, U: Nat) {
[True, T, U] => T
[False, T, U] => U
}
}
(NatIsUndef) NatIsUndefined(Nat): Bool {
[Undefined] => True
[P] => False
forall (M: Nat) {
[(O M)] => False
[(I M)] => False
}
}
(NatUndef) NatUndefined(Nat, Nat): Nat {
forall (M: Nat) {
[Undefined, M] => Undefined
[P, M] => M
}
forall (M: Nat, N: Nat) {
[(O N), M] => M
[(I N), M] => M
}
}
(TotalDifference) TotalSubtracting(Nat, Nat): Nat {
[P, P] => P
[Undefined, P] => Undefined
forall (N: Nat) {
[N, Undefined] => Undefined
[P, (O N)] => (# P N)
[P, (I N)] => Undefined
[(O N), P] => (O N)
[(I N), P] => (I N)
[Undefined, (O N)] => Undefined
[Undefined, (I N)] => Undefined
}
forall (N: Nat, M: Nat) {
[(O M), (O N)] => (@NatUndefined (# M N) (O (# M N)))
[(I M), (O N)] => (@NatUndefined (# M N) (I (# M N)))
[(O M), (I N)] => (@NatUndefined (# (# M N) I) (I (# (# M N) I)))
[(I M), (I N)] => (@NatUndefined (# M N) (O (# M N)))
}
}
(Quotient) Quotienting(Nat, Nat): Nat {
forall (D: Nat) {
[Undefined, D] => Undefined
[P, D] => (@NatIf (@NatIsUndefined (@TotalSubtracting P D)) O (@Successor (# (@TotalSubtracting P D) D)))
}
forall (N: Nat, D: Nat) {
[(O N), D] => (@NatIf (@NatIsUndefined (@TotalSubtracting (O N) D)) O (@Successor (# (@TotalSubtracting (O N) D) D)))
[(I N), D] => (@NatIf (@NatIsUndefined (@TotalSubtracting (I N) D)) O (@Successor (# (@TotalSubtracting (I N) D) D)))
}
}
(Remainder) Remaindering(Nat, Nat): Nat {
forall (D: Nat) {
[Undefined, D] => Undefined
[P, D] => (@NatIf (@NatIsUndefined (@TotalSubtracting P D)) P (# (@TotalSubtracting P D) D))
}
forall (N: Nat, D: Nat) {
[(O N), D] => (@NatIf (@NatIsUndefined (@TotalSubtracting (O N) D)) (O N) (# (@TotalSubtracting (O N) D) D))
[(I N), D] => (@NatIf (@NatIsUndefined (@TotalSubtracting (I N) D)) (I O) (# (@TotalSubtracting (I N) D) D))
}
}
}
fn invariants() {
assert_eq!(<I<I> as Nat>::reify(), 3);
assert_eq!(<I<O<I>> as Nat>::reify(), 5);
assert_eq!(<Sum<I<O<I>>, I<I>> as Nat>::reify(), 8);
assert_eq!(<Difference<I<I>, O<I>> as Nat>::reify(), 1);
assert_eq!(<Difference<O<O<O<I>>>, I<I>> as Nat>::reify(), 5);
assert_eq!(<Product<I<I>, I<O<I>>> as Nat>::reify(), 15);
assert_eq!(<Quotient<I<I>, O<I>> as Nat>::reify(), 1);
assert_eq!(<Remainder<I<O<O<I>>>, O<O<I>>> as Nat>::reify(), 1);
}
}
#[cfg(test)]
mod tests_2 {
use super::*;
type_operators! {
[A, B, C, D, E]
data Nat {
P,
I(Nat = P),
O(Nat = P),
}
}
}