Macro type_operators::type_operators

macro_rules! type_operators {
    ($gensym:tt $(#$docs:tt)* data $name:ident: $fbound:ident $(+ $bound:ident)* where $(#$attr:tt)+ { $($stuff:tt)* } $($rest:tt)*) => { ... };
    ($gensym:tt $(#$docs:tt)* data $name:ident where $(#$attr:tt)+ { $($stuff:tt)* } $($rest:tt)*) => { ... };
    ($gensym:tt $(#$docs:tt)* data $name:ident: $fbound:ident $(+ $bound:ident)* { $($stuff:tt)* } $($rest:tt)*) => { ... };
    ($gensym:tt $(#$docs:tt)* data $name:ident { $($stuff:tt)* } $($rest:tt)*) => { ... };
    ($gensym:tt $(#$docs:tt)* concrete $name:ident: $fbound:ident $(+ $bound:ident)* => $output:ty where $(#$attr:tt)+ { $($stuff:tt)* } $($rest:tt)*) => { ... };
    ($gensym:tt $(#$docs:tt)* concrete $name:ident => $output:ty where $(#$attr:tt)+ { $($stuff:tt)* } $($rest:tt)*) => { ... };
    ($gensym:tt $(#$docs:tt)* concrete $name:ident: $fbound:ident $(+ $bound:ident)* => $output:ty { $($stuff:tt)* } $($rest:tt)*) => { ... };
    ($gensym:tt $(#$docs:tt)* concrete $name:ident => $output:ty { $($stuff:tt)* } $($rest:tt)*) => { ... };
    ($gensym:tt $(#$docs:tt)* ($alias:ident) $machine:ident ($($kind:tt)*): $out:tt where $(#$attr:tt)* { $($states:tt)* } $($rest:tt)*) => { ... };
    ($gensym:tt $(#$docs:tt)* ($alias:ident) $machine:ident ($($kind:tt)*): $out:tt { $($states:tt)* } $($rest:tt)*) => { ... };
    ($gensym:tt) => { ... };
}

The type_operators macro does a lot of different things. Specifically, there are two things it's meant to do: 1. Make declaring closed type families easier. (Although they never really end up closed... Good enough.) 2. Make declaring type operators easier. (Although there are still a lotta problems with this.)

By "closed type family" here, I mean a family of structs which have a marker trait indicating that they "belong" to the family. A sort of type-level enum, if you will (if only something like that could truly exist in Rust some day!) And by "type operator", I mean a sort of function which acts on types and returns a type. In the following example, the natural numbers (encoded in binary here) are our "closed type family", and addition, subtraction, multiplication, division, etc. etc. are all our type operators.

You should probably read the top-level documentation before you look at this more complex example.

type_operators! {
    [A, B, C, D, E] // The gensym list. Be careful not to have these collide with your struct names!

    // If I used `data` instead of concrete, no automatic `reify` function would be provided.
    // But since I did, we have a sort of inductive thing going on here, by which we can transform
    // any instance of this type into the reified version.

    // data Nat {
    //     P,
    //     I(Nat = P),
    //     O(Nat = P),
    // }

    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!"),
    }

    // It's not just for natural numbers! Yes, we can do all sorts of logic here. However, in
    // this example, `Bool` is used later on in implementations that are hidden from you due
    // to their complexity.
    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))
        }
    }
}

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);