Skip to content

Commit

Permalink
Allow multi-token relations in calc
Browse files Browse the repository at this point in the history
  • Loading branch information
@jaybosamiya
jaybosamiya committed Jul 25, 2023
1 parent a2e9259 commit c6930c8
Showing 1 changed file with 29 additions and 23 deletions.
52 changes: 29 additions & 23 deletions source/pervasive/calc_macro.rs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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);* ;); }
);
}};

Expand Down Expand Up @@ -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
Expand All @@ -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.
Expand Down Expand Up @@ -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);* ;
)
)
};
Expand Down

0 comments on commit c6930c8

Please sign in to comment.