Macro push_rules

macro_rules! push_rules {
    ($judgment_name:ident, $input_value:expr, $output:expr, $input_names:tt => $output_ty:ty, $($rule:tt)*) => { ... };
    (@rule ($judgment_name:ident, $input_value:expr, $output:expr, $input_names:tt => $output_ty:ty) ($($m:tt)*)) => { ... };
    (@accum
        args($judgment_name:ident, $input_value:expr, $output:expr, ($($input_names:ident),*) => $output_ty:ty)
        accum($($m:tt)*)
        ---$(-)* ($n:literal)
        ($conclusion_name:ident($($patterns:tt)*) => $v:expr)
    ) => { ... };
    (@accum args $args:tt accum($($m:tt)*) ($($n:tt)*) $($o:tt)*) => { ... };
    (@match inputs() patterns() args($judgment_name:ident; $n:literal; $v:expr; $output:expr; $($m:tt)*)) => { ... };
    (@match inputs() patterns(,) args $args:tt) => { ... };
    (@match inputs($in0:ident $($inputs:tt)*) patterns($pat0:ident, $($pats:tt)*) args $args:tt) => { ... };
    (@match inputs($in0:ident) patterns($pat0:ident) args $args:tt) => { ... };
    (@match inputs($in0:ident $($inputs:tt)*) patterns($pat0:ident : $ty0:ty, $($pats:tt)*) args $args:tt) => { ... };
    (@match inputs($in0:ident) patterns($pat0:ident : $ty0:ty) args $args:tt) => { ... };
    (@match inputs($in0:ident $($inputs:tt)*) patterns($pat0:pat, $($pats:tt)*) args $args:tt) => { ... };
    (@match inputs($in0:ident) patterns($pat0:pat) args $args:tt) => { ... };
    (@body $args:tt (if $c:expr) $($m:tt)*) => { ... };
    (@body $args:tt (assert $c:expr) $($m:tt)*) => { ... };
    (@body $args:tt (if let $p:pat = $e:expr) $($m:tt)*) => { ... };
    (@body $args:tt ($i:expr => $p:pat) $($m:tt)*) => { ... };
    (@body $args:tt (let $p:pat = $i:expr) $($m:tt)*) => { ... };
    (@body ($judgment_name:ident, $rule_name:literal, $v:expr, $output:expr)) => { ... };
}

push_rules! allows construction of inference rules using a more logic-like notation.

The macro input looks like: push_rules!(builder, (...) (...) (...)) where each parenthesized group (...) is an inference rule. Inference rules are written like so:

(
    ( /* condition 1 */) // each condition is a parenthesized group
    ( /* condition 2 */)
    -------------------- // 3 or more `-` separate the condition from the conclusion
    ( /* conclusion */)  // as is the conclusion
)

The conditions can be the following

• (<expr> => <binding>) – used to apply judgments, but really <expr> can be anything with an into_iter method.
• (if <expr>)
• (if let <pat> = <expr>)
• (let <binding> = <expr>)

The conclusions can be the following

• `( => )