type_operators/
lib.rs

1//! # The `type_operators` macro - a DSL for declaring type operators and type-level logic in Rust.
2//!
3//! This crate contains a macro for declaring type operators in Rust. Type operators are like functions
4//! which act at the type level. The `type_operators` macro works by translating a LISP-y DSL into a big mess of
5//! traits and impls with associated types.
6//!
7//! # The DSL
8//!
9//! Let's take a look at this fairly small example:
10//!
11//! ```rust
12//! # #[macro_use] extern crate type_operators;
13//! type_operators! {
14//!     [A, B, C, D, E]
15//!
16//!     data Nat {
17//!         P,
18//!         I(Nat = P),
19//!         O(Nat = P),
20//!     }
21//! }
22//! # fn main() {}
23//! ```
24//!
25//! There are two essential things to note in this example. The first is the "gensym list" - Rust does
26//! not currently have a way to generate unique identifiers, so we have to supply our own. It is on *you*
27//! to avoid clashes between these pseudo-gensyms and the names of the structs involved! If we put `P`, `I`, or `O`
28//! into the gensym list, things could get really bad! We'd get type errors at compile-time stemming from trait
29//! bounds, coming from the definitions of type operators later. Thankfully, the gensym list can be fairly small
30//! and usually never uses more than two or three symbols.
31//!
32//! The second thing is the `data` declaration. This declares a group of structs which fall under a marker trait.
33//! In our case, `Nat` is the marker trait generated and `P`, `I`, and `O` are the structs generated. This example
34//! shows an implementation of natural numbers (positive integers, including zero) which are represented as types.
35//! So, `P` indicates the end of a natural number - think of it as a sort of nil; we're working with a linked list
36//! here, at the type level. So, `I<P>` would represent "one plus twice `P`", which of course comes out to `1`;
37//! `O<P>` would represent "twice `P`", which of course comes out to zero. If we look at `I` and `O` as bits of a
38//! binary number, we come out with a sort of reversed binary representation where the "bit" furthest to the left
39//! is the least significant bit. As such, `O<O<I>>` represents `4`, `I<O<O<I>>>` represents `9`, and so on.
40//!
41//! When we write `I(Nat = P)`, the `= P` denotes a default. This lets us write `I`, and have it be inferred to be
42//! `I<P>`, which is probably what you mean if you just write `I` alone. `Nat` gives a trait bound. To better demonstrate,
43//! here is (roughly) what the above invocation of `type_operators` expands to:
44//!
45//! ```rust
46//! # use std::marker::PhantomData;
47//!
48//! pub trait Nat {}
49//!
50//! pub struct P;
51//! impl Nat for P {}
52//!
53//! pub struct I<A: Nat = P>(PhantomData<(A)>);
54//! impl<A: Nat> Nat for I<A> {}
55//!
56//! pub struct O<A: Nat = P>(PhantomData<(A)>);
57//! impl<A: Nat> Nat for O<A> {}
58//! # fn main() {}
59//! ```
60//!
61//! The `Undefined` value looks a little silly, but it allows for the definition of division in a way which uses
62//! type-level comparison and branching. More on that later.
63//!
64//! The above definition has a problem. We cannot *fold* our type-level representation down into a numerical representation.
65//! That makes our type-level natural numbers useless! That's why `type_operators` provides another way of defining
66//! type-level representations, the `concrete` declaration:
67//!
68//! ```rust
69//! # #[macro_use]
70//! # extern crate type_operators;
71//!
72//! type_operators! {
73//!     [A, B, C, D, E]
74//!
75//!     concrete Nat => usize {
76//!         P => 0,
77//!         I(N: Nat = P) => 1 + 2 * N,
78//!         O(N: Nat = P) => 2 * N,
79//!         Undefined => panic!("Undefined type-level arithmetic result!"),
80//!     }
81//! }
82//! # fn main() {}
83//! ```
84//!
85//! This adds an associated function to the `Nat` trait called `reify`, which allows you to turn your type-level
86//! representations into concrete values of type `usize` (in this case.) If you've ever seen primitive-recursive
87//! functions, then this should look a bit familiar to you - it's reminiscent of a recursion scheme, which is a
88//! way of recursing over a value to map it into something else. (See also "catamorphism".) It should be fairly
89//! obvious how this works, but if not, here's a breakdown:
90//!
91//! - `P` always represents zero, so we say that `P => 0`. Simple.
92//! - `I` represents double its argument plus one. If we annotate our macro's definition with a variable `N`,
93//!   then `type_operators` will automatically call `N::reify()` and substitute that value for your `N` in the
94//!   expression you give it. So, in this way, we define the reification of `I` to be one plus two times the
95//!   value that `N` reifies to.
96//! - `O` represents double its argument, so this one's straightforward - it's like `I`, but without the `1 +`.
97//!
98//! Okay. So now that we've got that under our belts, let's dive into something a bit more complex: let's define
99//! a type operator for addition.
100//!
101//! `type_operators` allows you to define recursive functions. Speaking generally, that's what you'll really need
102//! to pull this off whatever you do. (And speaking precisely, this whole approach was inspired by primitive-recursion.)
103//! So let's think about how we can add two binary numbers, starting at the least-significant bit:
104//! - Obviously, `P + P` should be `P`, since zero plus zero is zero.
105//! - What about `P + O<N>`, for any natural number `N`? Well, that should be `O<N>`. Same with `I<N>`. As a matter of
106//!   fact, now it looks pretty obvious that whenever we have `P` on one side, we should just say that whatever's on the
107//!   other side is the result.
108//! So our little table of operations now looks like:
109//! ```text
110//! [P, P] => P
111//! [P, (O N)] => (O N)
112//! [P, (I N)] => (I N)
113//! [(O N), P] => (O N)
114//! [(I N), P] => (I N)
115//! ```
116//! Now you're probably saying, "whoa! That doesn't look like Rust at all! Back up!" And that's because it *isn't.* I made
117//! a little LISP-like dialect to describe Rust types for this project because it makes things a lot easier to parse in
118//! macros; specifically, each little atomic type can be wrapped up in a pair of parentheses, while with angle brackets,
119//! Rust has to parse them as separate tokens. In this setup, `(O N)` means `O<N>`,
120//! just `P` alone means `P`, etc. etc. The notation `[X, Y] => Z` means "given inputs `X` and `Y`, produce output `Z`." So
121//! it's a sort of pattern-matching.
122//!
123//! Now let's look at the more complex cases. We need to cover all the parts where combinations of `O<N>` and `I<N>` are
124//! added together.
125//! - `O<M> + O<N>` should come out to `O<M + N>`. This is a fairly intuitive result, but we can describe it mathematically
126//!   as `2 * m + 2 * n == 2 * (m + n)`. So, it's the distributive law, and most importantly, it cuts down on the *structure*
127//!   of the arguments - we go from adding `O<M>` and `O<N>` to `M` and `N`, whatever they are, and `M` and `N` are clearly
128//!   less complex than `O<M>` and `O<N>`. If we always see that our outputs have less complexity than the inputs, then we're
129//!   that much closer to a proof that our little type operator always terminates with a result!
130//! - `I<M> + O<N>` and `O<M> + I<N>` should come out to `I<M + N>`. Again, fairly intuitive. We have `1 + 2 * m + 2 * n`,
131//!   which we can package up into `1 + 2 * (m + n)`.
132//! - `I<M> + I<N>` is the trickiest part here. We have `1 + 2 * m + 1 + 2 * m == 2 + 2 * m + 2 * n == 2 * (1 + m + n)`. We
133//!   can implement this as `I<I + M + N>`, but we can do a little bit better. More on that later, we'll head with the simpler
134//!   implementation for now.
135//!
136//! Let's add these to the table:
137//! ```text
138//! [P, P] => P
139//! [P, (O N)] => (O N)
140//! [P, (I N)] => (I N)
141//! [(O N), P] => (O N)
142//! [(I N), P] => (I N)
143//! // New:
144//! [(O M), (O N)] => (O (# M N))
145//! [(I M), (O N)] => (I (# M N))
146//! [(O M), (I N)] => (I (# M N))
147//! [(I M), (I N)] => (O (# (# I M) N))
148//! ```
149//! Here's something new: the `(# ...)` notation. This tells the macro, "hey, we wanna recurse." It's really shorthand
150//! for a slightly more complex piece of notation, but they both have one thing in common - *when type_operators processes
151//! the `(# ...)` notation, it uses it to calculate trait bounds.* This is because your type operator won't compile unless
152//! it's absolutely certain that `(# M N)` will actually have a defined result. At an even higher level, this is the reason
153//! I wish Rust had "closed type families" - if `P`, `I`, and `O` were in a closed type family `Nat`, Rust could check at compile-time
154//! and be absolutely sure that `(# M N)` existed for all `M` and `N` that are in the `Nat` family.
155//!
156//! So then. Let's load this into an invocation of `type_operators` to see how it looks like. It's pretty close to the table,
157//! but with a couple additions (I'm leaving out `Undefined` for now because it's not yet relevant):
158//!
159//! ```rust
160//! # #[macro_use] extern crate type_operators;
161//!
162//! type_operators! {
163//!     [A, B, C, D, E]
164//!
165//!     concrete Nat => usize {
166//!         P => 0,
167//!         I(N: Nat = P) => 1 + 2 * N,
168//!         O(N: Nat = P) => 2 * N,
169//!     }
170//!
171//!     (Sum) Adding(Nat, Nat): Nat {
172//!         [P, P] => P
173//!         forall (N: Nat) {
174//!             [(O N), P] => (O N)
175//!             [(I N), P] => (I N)
176//!             [P, (O N)] => (O N)
177//!             [P, (I N)] => (I N)
178//!         }
179//!         forall (N: Nat, M: Nat) {
180//!             [(O M), (O N)] => (O (# M N))
181//!             [(I M), (O N)] => (I (# M N))
182//!             [(O M), (I N)] => (I (# M N))
183//!             [(I M), (I N)] => (O (# (# M N) I))
184//!         }
185//!     }
186//! }
187//! # fn main() {}
188//! ```
189//!
190//! There are several things to note. First, the definition `(Sum) Adding(Nat, Nat): Nat`. This says,
191//! "this type operator takes two `Nat`s as input and outputs a `Nat`." Since addition is implemented
192//! as a recursive trait under the hood, this means we get a trait definition of the form:
193//!
194//! ```rust
195//! # pub trait Nat {}
196//! pub trait Adding<A: Nat>: Nat {
197//!     type Output: Nat;
198//! }
199//! ```
200//!
201//! The `(Sum)` bit declares a nice, convenient alias for us, so that instead of typing `<X as Adding<Y>>::Output`
202//! to get the sum of two numbers, we can instead type `Sum<X, Y>`. Much neater.
203//!
204//! Second, the "quantifier" sections (the parts with `forall`) avoid Rust complaining about "undeclared type variables." In any given
205//! generic `impl`, we have to worry about declaring what type variables/generic type parameters we can use in
206//! that `impl`. The `forall` bit modifies the prelude of the `impl`. For example, `forall (N: Nat)` causes all the
207//! `impl`s inside its little block to be declared as `impl<N: Nat> ...` instead of `impl ...`, so that we can use
208//! `N` as a variable inside those expressions.
209//!
210//! That just about wraps up our short introduction. To finish, here are the rest of the notations specific to our
211//! little LISP-y dialect, all of which can only be used on the right-hand side of a rule in the DSL:
212//!
213//! - `(@TypeOperator ...)` invokes another type operator (can be the original caller!) and generates the proper trait bounds.
214//! - `(% ...)` is like `(# ...)`, but does not generate any trait bounds.
215//! - `(& <type> where (<where_clause>) (<where_clause>) ...)` allows for the definition of custom `where` clauses for a given
216//!   `impl`. It can appear anywhere in the right-hand side of a rule in the DSL, but in general should probably always be
217//!   written at the top-level for consistency.
218//!
219//! In addition, it is possible to use attributes such as `#[derive(...)]` or `#[cfg(...)]` on `data` and `concrete` definitions
220//! as well as individual elements inside them. In addition, attributes can be added to the `impl`s for rules. For example:
221//!
222//! ```rust
223//! # #[macro_use] extern crate type_operators;
224//! # use std::fmt::Debug;
225//! type_operators! {
226//!     [A, B, C, D, E]
227//!
228//!     data Nat: Default + Debug where #[derive(Default, Debug)] {
229//!         P,
230//!         I(Nat = P),
231//!         O(Nat = P),
232//!         #[cfg(features = "specialization")]
233//!         Error,
234//!         #[cfg(features = "specialization")]
235//!         DEFAULT,
236//!     }
237//!
238//!     (Sum) Adding(Nat, Nat): Nat {
239//!         [P, P] => P
240//!         forall (N: Nat) {
241//!             [(O N), P] => (O N)
242//!             [(I N), P] => (I N)
243//!             [P, (O N)] => (O N)
244//!             [P, (I N)] => (I N)
245//!         }
246//!         forall (N: Nat, M: Nat) {
247//!             [(O M), (O N)] => (O (# M N))
248//!             [(I M), (O N)] => (I (# M N))
249//!             [(O M), (I N)] => (I (# M N))
250//!             [(I M), (I N)] => (O (# (# M N) I))
251//!
252//!             #[cfg(features = "specialization")] {
253//!                 {M, N} => Error
254//!             }
255//!         }
256//!     }
257//! }
258//! # fn main() {}
259//! ```
260//!
261//! Note the block `#[cfg(features = "specialization")] { ... }`. This tells `type_operators!` to add the attribute
262//! `#[cfg(features = "specialization")]` to every `impl` declared inside. It's also worth noting that adding derives
263//! to every single statement inside a `concrete` or `data` declaration can be done as shown above with a `where`
264//! clause-like structure - the reason we have to do this is because if we were allowed to define it the intuitive
265//! way, there would be no easy way to extract doc comments on the group trait (thanks to macro parsing ambiguities.)
266//!
267//! Current bugs/improvements to be made:
268//! - Bounds in type operators are currently restricted to identifiers only - they should be augmented with a LISP-like
269//!   dialect similar to the rest of the macro system.
270//!
271//! If questions are had, I may be found either at my email (which is listed on GitHub) or on the `#rust` IRC, where I go by
272//! the nick `sleffy`.
273//!
274
275
276/// The `All` trait provides a workaround to the current parsing problem of a lack of truly unbounded type operator
277/// arguments. It's implemented for all types.
278pub trait All {}
279impl<T: ?Sized> All for T {}
280
281
282/// The `type_operators` macro does a lot of different things. Specifically, there are two things
283/// it's meant to do:
284///     1. Make declaring closed type families easier. (Although they never *really* end up closed... Good enough.)
285///     2. Make declaring type operators easier. (Although there are still a lotta problems with this.)
286///
287/// By "closed type family" here, I mean a family of structs which have a marker trait indicating that they
288/// "belong" to the family. A sort of type-level enum, if you will (if only something like that could truly
289/// exist in Rust some day!) And by "type operator", I mean a sort of function which acts on types and returns
290/// a type. In the following example, the natural numbers (encoded in binary here) are our "closed type family",
291/// and addition, subtraction, multiplication, division, etc. etc. are all our type operators.
292///
293/// You should probably read the top-level documentation before you look at this more complex example.
294///
295/// ```
296/// # #[macro_use]
297/// # extern crate type_operators;
298///
299/// type_operators! {
300///     [A, B, C, D, E] // The gensym list. Be careful not to have these collide with your struct names!
301///
302///     // If I used `data` instead of concrete, no automatic `reify` function would be provided.
303///     // But since I did, we have a sort of inductive thing going on here, by which we can transform
304///     // any instance of this type into the reified version.
305///
306///     // data Nat {
307///     //     P,
308///     //     I(Nat = P),
309///     //     O(Nat = P),
310///     // }
311///
312///     concrete Nat => usize {
313///         P => 0,
314///         I(N: Nat = P) => 1 + 2 * N,
315///         O(N: Nat = P) => 2 * N,
316///         Undefined => panic!("Undefined type-level arithmetic result!"),
317///     }
318///
319///     // It's not just for natural numbers! Yes, we can do all sorts of logic here. However, in
320///     // this example, `Bool` is used later on in implementations that are hidden from you due
321///     // to their complexity.
322///     concrete Bool => bool {
323///         False => false,
324///         True => true,
325///     }
326///
327///     (Pred) Predecessor(Nat): Nat {
328///         [Undefined] => Undefined
329///         [P] => Undefined
330///         forall (N: Nat) {
331///             [(O N)] => (I (# N))
332///             [(I N)] => (O N)
333///         }
334///     }
335///
336///     (Succ) Successor(Nat): Nat {
337///         [Undefined] => Undefined
338///         [P] => I
339///         forall (N: Nat) {
340///             [(O N)] => (I N)
341///             [(I N)] => (O (# N))
342///         }
343///     }
344///
345///     (Sum) Adding(Nat, Nat): Nat {
346///         [P, P] => P
347///         forall (N: Nat) {
348///             [(O N), P] => (O N)
349///             [(I N), P] => (I N)
350///             [P, (O N)] => (O N)
351///             [P, (I N)] => (I N)
352///         }
353///         forall (N: Nat, M: Nat) {
354///             [(O M), (O N)] => (O (# M N))
355///             [(I M), (O N)] => (I (# M N))
356///             [(O M), (I N)] => (I (# M N))
357///             [(I M), (I N)] => (O (# (# M N) I))
358///         }
359///     }
360///
361///     (Difference) Subtracting(Nat, Nat): Nat {
362///         forall (N: Nat) {
363///             [N, P] => N
364///         }
365///         forall (N: Nat, M: Nat) {
366///             [(O M), (O N)] => (O (# M N))
367///             [(I M), (O N)] => (I (# M N))
368///             [(O M), (I N)] => (I (# (# M N) I))
369///             [(I M), (I N)] => (O (# M N))
370///         }
371///     }
372///
373///     (Product) Multiplying(Nat, Nat): Nat {
374///         forall (N: Nat) {
375///             [P, N] => P
376///         }
377///         forall (N: Nat, M: Nat) {
378///             [(O M), N] => (# M (O N))
379///             [(I M), N] => (@Adding N (# M (O N)))
380///         }
381///     }
382///
383///     (If) NatIf(Bool, Nat, Nat): Nat {
384///         forall (T: Nat, U: Nat) {
385///             [True, T, U] => T
386///             [False, T, U] => U
387///         }
388///     }
389///
390///     (NatIsUndef) NatIsUndefined(Nat): Bool {
391///         [Undefined] => True
392///         [P] => False
393///         forall (M: Nat) {
394///             [(O M)] => False
395///             [(I M)] => False
396///         }
397///     }
398///
399///     (NatUndef) NatUndefined(Nat, Nat): Nat {
400///         forall (M: Nat) {
401///             [Undefined, M] => Undefined
402///             [P, M] => M
403///         }
404///         forall (M: Nat, N: Nat) {
405///             [(O N), M] => M
406///             [(I N), M] => M
407///         }
408///     }
409///
410///     (TotalDifference) TotalSubtracting(Nat, Nat): Nat {
411///         [P, P] => P
412///         [Undefined, P] => Undefined
413///         forall (N: Nat) {
414///             [N, Undefined] => Undefined
415///             [P, (O N)] => (# P N)
416///             [P, (I N)] => Undefined
417///             [(O N), P] => (O N)
418///             [(I N), P] => (I N)
419///             [Undefined, (O N)] => Undefined
420///             [Undefined, (I N)] => Undefined
421///         }
422///         forall (N: Nat, M: Nat) {
423///             [(O M), (O N)] => (@NatUndefined (# M N) (O (# M N)))
424///             [(I M), (O N)] => (@NatUndefined (# M N) (I (# M N)))
425///             [(O M), (I N)] => (@NatUndefined (# (# M N) I) (I (# (# M N) I)))
426///             [(I M), (I N)] => (@NatUndefined (# M N) (O (# M N)))
427///         }
428///     }
429///
430///     (Quotient) Quotienting(Nat, Nat): Nat {
431///         forall (D: Nat) {
432///             [Undefined, D] => Undefined
433///             [P, D] => (@NatIf (@NatIsUndefined (@TotalSubtracting P D)) O (@Successor (# (@TotalSubtracting P D) D)))
434///         }
435///         forall (N: Nat, D: Nat) {
436///             [(O N), D] => (@NatIf (@NatIsUndefined (@TotalSubtracting (O N) D)) O (@Successor (# (@TotalSubtracting (O N) D) D)))
437///             [(I N), D] => (@NatIf (@NatIsUndefined (@TotalSubtracting (I N) D)) O (@Successor (# (@TotalSubtracting (I N) D) D)))
438///         }
439///     }
440///
441///     (Remainder) Remaindering(Nat, Nat): Nat {
442///         forall (D: Nat) {
443///             [Undefined, D] => Undefined
444///             [P, D] => (@NatIf (@NatIsUndefined (@TotalSubtracting P D)) P (# (@TotalSubtracting P D) D))
445///         }
446///         forall (N: Nat, D: Nat) {
447///             [(O N), D] => (@NatIf (@NatIsUndefined (@TotalSubtracting (O N) D)) (O N) (# (@TotalSubtracting (O N) D) D))
448///             [(I N), D] => (@NatIf (@NatIsUndefined (@TotalSubtracting (I N) D)) (I O) (# (@TotalSubtracting (I N) D) D))
449///         }
450///     }
451/// }
452///
453/// # fn main() {
454/// assert_eq!(<I<I> as Nat>::reify(), 3);
455/// assert_eq!(<I<O<I>> as Nat>::reify(), 5);
456/// assert_eq!(<Sum<I<O<I>>, I<I>> as Nat>::reify(), 8);
457/// assert_eq!(<Difference<I<I>, O<I>> as Nat>::reify(), 1);
458/// assert_eq!(<Difference<O<O<O<I>>>, I<I>> as Nat>::reify(), 5);
459/// assert_eq!(<Product<I<I>, I<O<I>>> as Nat>::reify(), 15);
460/// assert_eq!(<Quotient<I<I>, O<I>> as Nat>::reify(), 1);
461/// assert_eq!(<Remainder<I<O<O<I>>>, O<O<I>>> as Nat>::reify(), 1);
462/// # }
463/// ```
464#[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)*);); // Friends don't let friends derive drunk!
827    ([$($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        // It's not just for natural numbers! Yes, we can do all sorts of logic here. However, in
1019        // this example, `Bool` is used later on in implementations that are hidden from you due
1020        // to their complexity.
1021        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}