From c6930c8f7ea74b1a66af557e15ab3657a129a165 Mon Sep 17 00:00:00 2001 From: Jay Bosamiya Date: Tue, 25 Jul 2023 17:46:53 -0400 Subject: [PATCH] Allow multi-token relations in `calc` --- source/pervasive/calc_macro.rs | 52 +++++++++++++++++++--------------- 1 file changed, 29 insertions(+), 23 deletions(-) diff --git a/source/pervasive/calc_macro.rs b/source/pervasive/calc_macro.rs index bbe21fd13b..37b0d1cf6f 100644 --- a/source/pervasive/calc_macro.rs +++ b/source/pervasive/calc_macro.rs @@ -27,31 +27,31 @@ macro_rules! calc_internal { (__internal expr (<=) ($a:expr) ($b:expr)) => { ($a <= $b) }; (__internal expr (>) ($a:expr) ($b:expr)) => { ($a > $b) }; (__internal expr (>=) ($a:expr) ($b:expr)) => { ($a >= $b) }; - (__internal expr ($reln:tt) ($a:expr) ($b:expr)) => { - compile_error!(concat!("INTERNAL ERROR\nUnexpected ", stringify!(($reln, $a, $b)))); }; // Fallthrough + (__internal expr ($($reln:tt)+) ($a:expr) ($b:expr)) => { + compile_error!(concat!("INTERNAL ERROR\nUnexpected ", stringify!(($($reln)+, $a, $b)))); }; // Fallthrough // Any of the relation steps occuring in the middle of the chain - (__internal mid [$topreln:tt] $start:expr ; () $b:block $end:expr ; ) => {{ - ::builtin::assert_by($crate::calc_macro::calc_internal!(__internal expr ($topreln) ($start) ($end)), { $b }); + (__internal mid [$($topreln:tt)+] $start:expr ; () $b:block $end:expr ; ) => {{ + ::builtin::assert_by($crate::calc_macro::calc_internal!(__internal expr ($($topreln)+) ($start) ($end)), { $b }); }}; - (__internal mid [$topreln:tt] $start:expr ; ($reln:tt) $b:block $end:expr ; ) => {{ - ::builtin::assert_by($crate::calc_macro::calc_internal!(__internal expr ($reln) ($start) ($end)), { $b }); + (__internal mid [$($topreln:tt)+] $start:expr ; ($($reln:tt)+) $b:block $end:expr ; ) => {{ + ::builtin::assert_by($crate::calc_macro::calc_internal!(__internal expr ($($reln)+) ($start) ($end)), { $b }); }}; - (__internal mid [$topreln:tt] $start:expr ; () $b:block $mid:expr ; $(($($tailreln:tt)?) $tailb:block $taile:expr);* ;) => {{ - ::builtin::assert_by($crate::calc_macro::calc_internal!(__internal expr ($topreln) ($start) ($mid)), { $b }); - $crate::calc_macro::calc_internal!(__internal mid [$topreln] $mid ; $(($($tailreln)?) $tailb $taile);* ;); + (__internal mid [$($topreln:tt)+] $start:expr ; () $b:block $mid:expr ; $(($($tailreln:tt)*) $tailb:block $taile:expr);* ;) => {{ + ::builtin::assert_by($crate::calc_macro::calc_internal!(__internal expr ($($topreln)+) ($start) ($mid)), { $b }); + $crate::calc_macro::calc_internal!(__internal mid [$($topreln)+] $mid ; $(($($tailreln)*) $tailb $taile);* ;); }}; - (__internal mid [$topreln:tt] $start:expr ; ($reln:tt) $b:block $mid:expr ; $(($($tailreln:tt)?) $tailb:block $taile:expr);* ;) => {{ - ::builtin::assert_by($crate::calc_macro::calc_internal!(__internal expr ($reln) ($start) ($mid)), { $b }); - $crate::calc_macro::calc_internal!(__internal mid [$topreln] $mid ; $(($($tailreln)?) $tailb $taile);* ;); + (__internal mid [$($topreln:tt)+] $start:expr ; ($($reln:tt)+) $b:block $mid:expr ; $(($($tailreln:tt)*) $tailb:block $taile:expr);* ;) => {{ + ::builtin::assert_by($crate::calc_macro::calc_internal!(__internal expr ($($reln)+) ($start) ($mid)), { $b }); + $crate::calc_macro::calc_internal!(__internal mid [$($topreln)+] $mid ; $(($($tailreln)*) $tailb $taile);* ;); }}; // Main entry point to this macro; this is still an internal macro, but this is where the main // `calc!` macro will invoke this. - (($reln:tt) $start:expr ; $(($($midreln:tt)?) $b:block ; $mid:expr);* $(;)?) => {{ + (($($reln:tt)+) $start:expr ; $(($($($midreln:tt)+)?) $b:block ; $mid:expr);* $(;)?) => {{ ::builtin::assert_by( - calc_internal!(__internal expr ($reln) ($start) ($crate::calc_macro::calc_internal!(__internal get_last $($mid ;)*))), - { $crate::calc_macro::calc_internal!(__internal mid [$reln] $start ; $(($($midreln)?) $b $mid);* ;); } + calc_internal!(__internal expr ($($reln)+) ($start) ($crate::calc_macro::calc_internal!(__internal get_last $($mid ;)*))), + { $crate::calc_macro::calc_internal!(__internal mid [$($reln)+] $start ; $(($($($midreln)+)?) $b $mid);* ;); } ); }}; @@ -81,7 +81,7 @@ macro_rules! calc_aux { (confirm_allowed_relation (<=)) => { }; // Allowed (confirm_allowed_relation (>)) => { }; // Allowed (confirm_allowed_relation (>=)) => { }; // Allowed - (confirm_allowed_relation ($t:tt)) => { compile_error!(concat!("Currently unsupported relation `", stringify!($t), "` in calc")); }; // Fallthrough + (confirm_allowed_relation ($($t:tt)+)) => { compile_error!(concat!("Currently unsupported relation `", stringify!($($t)*), "` in calc")); }; // Fallthrough // Confirm that an middle relation is consistent with the main relation (confirm_middle_relation (==) (==)) => { }; // Equality is only consistent with itself @@ -97,8 +97,14 @@ macro_rules! calc_aux { (confirm_middle_relation (>) (>)) => { }; // Strictly-greater-than, similar to less-than-or-equal (confirm_middle_relation (>) (>=)) => { }; // (confirm_middle_relation (>) (==)) => { }; // - (confirm_middle_relation ($main:tt) ($middle:tt)) => { - compile_error!(concat!("Potentially inconsistent relation `", stringify!($middle), "` with `", stringify!($main), "`")); }; // Fallthrough + (confirm_middle_relation ($($main:tt)+) ($($middle:tt)+)) => { + compile_error!(concat!("Potentially inconsistent relation `", stringify!($($middle)*), "` with `", stringify!($($main)*), "`")); }; // Fallthrough + + (confirm_middle_relations ($($main:tt)+)) => { }; + (confirm_middle_relations ($($main:tt)+) ($($middle:tt)+) $($rest:tt)* ) => { + $crate::calc_macro::calc_aux!(confirm_middle_relation ($($main)+) ($($middle)+)); + $crate::calc_macro::calc_aux!(confirm_middle_relations ($($main)+) $($rest)*); + }; } /// The `calc!` macro supports structured proofs through calculations. @@ -146,15 +152,15 @@ macro_rules! calc_aux { #[macro_export] macro_rules! calc { // The main entry point to this macro. - (($reln:tt) $start:expr ; $($(($middlereln:tt))? $b:block $mid:expr);* $(;)?) => { - $crate::calc_macro::calc_aux!(confirm_allowed_relation ($reln)); + (($($reln:tt)+) $start:expr ; $($(($($middlereln:tt)+))? $b:block $mid:expr);* $(;)?) => { + $crate::calc_macro::calc_aux!(confirm_allowed_relation ($($reln)+)); $($( - $crate::calc_macro::calc_aux!(confirm_allowed_relation ($middlereln)); - $crate::calc_macro::calc_aux!(confirm_middle_relation ($reln) ($middlereln)); + $crate::calc_macro::calc_aux!(confirm_allowed_relation ($($middlereln)+)); )?)* + $crate::calc_macro::calc_aux!(confirm_middle_relations ($($reln)+) $($(($($middlereln)+))?)*); ::builtin_macros::verus_proof_macro_explicit_exprs!( $crate::calc_macro::calc_internal!( - ($reln) @@$start ; $(($($middlereln)?) @@$b ; @@$mid);* ; + ($($reln)+) @@$start ; $(($($($middlereln)+)?) @@$b ; @@$mid);* ; ) ) };