simplify pattern matching with trailing comma

Just accept any number of trailing commas.
Simplifies the matching logic quite a bit!

Author: nikomatsakis

crates/formality-core/src/judgment.rs

@@ -159,7 +159,7 @@ macro_rules! push_rules {
             };
 
             if let Some(__JudgmentStruct($($input_names),*)) = Some($input_value) {
-                $crate::push_rules!(@match inputs($($input_names)*) patterns($($patterns)*) args(@body ($judgment_name; $n; $v; $output); $($m)*));
+                $crate::push_rules!(@match inputs($($input_names)*) patterns($($patterns)*,) args(@body ($judgment_name; $n; $v; $output); $($m)*));
             }
         }
     };
@@ -198,40 +198,19 @@ macro_rules! push_rules {
         }
     };
 
-    (@match inputs($in0:ident $($inputs:tt)*) patterns($pat0:ident : $ty0:ty) args $args:tt) => {
-        {
-            if let Some($pat0) = $crate::Downcast::downcast::<$ty0>($in0) {
-                $crate::push_rules!(@match inputs($($inputs)*) patterns() args $args);
-            }
-        }
-    };
-
     (@match inputs($in0:ident $($inputs:tt)*) patterns($pat0:ident, $($pats:tt)*) args $args:tt) => {
         {
             let $pat0 = Clone::clone($in0);
             $crate::push_rules!(@match inputs($($inputs)*) patterns($($pats)*) args $args);
         }
     };
 
-    (@match inputs($in0:ident $($inputs:tt)*) patterns($pat0:ident) args $args:tt) => {
-        {
-            let $pat0 = Clone::clone($in0);
-            $crate::push_rules!(@match inputs($($inputs)*) patterns() args $args);
-        }
-    };
-
     (@match inputs($in0:ident $($inputs:tt)*) patterns($pat0:pat, $($pats:tt)*) args $args:tt) => {
         if let Some($pat0) = $crate::Downcast::downcast(&$in0) {
             $crate::push_rules!(@match inputs($($inputs)*) patterns($($pats)*) args $args);
         }
     };
 
-    (@match inputs($in0:ident $($inputs:tt)*) patterns($pat0:pat) args $args:tt) => {
-        if let Some($pat0) = $crate::Downcast::downcast(&$in0) {
-            $crate::push_rules!(@match inputs($($inputs)*) patterns() args $args);
-        }
-    };
-
     // (@match (($arg0:ident @ $pat0:pat) $($args:tt)*) ($n:literal; $v:expr; $output:ident) $($m:tt)*) => {
     //     if let Some($pat0) = $crate::cast::Downcast::downcast(&$arg0) {
     //         $crate::push_rules!(@match ($($args)*) ($n; $v; $output) $($m)*);