use guarded bindings for optional where-clauses

Woohoo!

Author: nikomatsakis

crates/formality-core/src/lib.rs

@@ -32,6 +32,7 @@ pub mod language;
 pub mod parse;
 pub mod substitution;
 pub mod term;
+pub mod util;
 pub mod variable;
 pub mod visit;
 

crates/formality-core/src/util.rs

@@ -0,0 +1,9 @@
+/// Returns true if `t` is the default value for `t`.
+/// Used by the "derive" code for `Debug`.
+pub fn is_default<T>(t: &T) -> bool
+where
+    T: Default + Eq,
+{
+    let default_value: T = Default::default();
+    default_value == *t
+}

crates/formality-macros/src/debug.rs

@@ -256,6 +256,19 @@ fn debug_field_with_mode(name: &Ident, mode: &FieldMode) -> TokenStream {
                 }
             }
         }
+
+        FieldMode::Guarded { guard, mode } => {
+            let guard = as_literal(guard);
+            let base = debug_field_with_mode(name, mode);
+
+            quote_spanned! { name.span() =>
+                if !::formality_core::util::is_default(#name) {
+                    write!(fmt, "{}{}", sep, #guard)?;
+                    sep = " ";
+                    #base
+                }
+            }
+        }
     }
 }
 

crates/formality-macros/src/parse.rs

@@ -230,6 +230,18 @@ fn parse_field_mode(span: Span, mode: &FieldMode) -> TokenStream {
                 __p.comma_nonterminal()?
             }
         }
+
+        FieldMode::Guarded { guard, mode } => {
+            let guard_keyword = as_literal(guard);
+            let initializer = parse_field_mode(span, mode);
+            quote_spanned! {
+                span =>
+                match __p.expect_keyword(#guard_keyword) {
+                    Ok(()) => #initializer,
+                    Err(_) => Default::default(),
+                }
+            }
+        }
     }
 }
 

crates/formality-macros/src/spec.rs

@@ -1,4 +1,4 @@
-use std::iter::Peekable;
+use std::{iter::Peekable, sync::Arc};
 
 use proc_macro2::{Group, Ident, Punct, TokenStream, TokenTree};
 use syn::spanned::Spanned;
@@ -36,6 +36,11 @@ pub enum FieldMode {
     /// $x -- just parse `x`
     Single,
 
+    Guarded {
+        guard: Ident,
+        mode: Arc<FieldMode>,
+    },
+
     /// $<x> -- `x` is a `Vec<E>`, parse `<E0,...,En>`
     /// $[x] -- `x` is a `Vec<E>`, parse `[E0,...,En]`
     /// $(x) -- `x` is a `Vec<E>`, parse `(E0,...,En)`
@@ -100,7 +105,7 @@ fn token_stream_to_symbols(
             }
             proc_macro2::TokenTree::Ident(ident) => symbols.push(Keyword { ident }),
             proc_macro2::TokenTree::Punct(punct) => match punct.as_char() {
-                '$' => symbols.push(parse_variable_binding(punct, &mut tokens)?),
+                '$' => symbols.push(parse_variable_binding(&punct, &mut tokens)?),
                 _ => symbols.push(Char { punct }),
             },
             proc_macro2::TokenTree::Literal(_) => {
@@ -120,14 +125,16 @@ fn token_stream_to_symbols(
 /// or we could also see a `$`, in which case user wrote `$$`, and we treat that as a single
 /// `$` sign.
 fn parse_variable_binding(
-    dollar_token: Punct,
-    tokens: &mut impl Iterator<Item = TokenTree>,
+    dollar_token: &Punct,
+    tokens: &mut dyn Iterator<Item = TokenTree>,
 ) -> syn::Result<FormalitySpecSymbol> {
-    let dollar_token = &dollar_token;
     let mut tokens = tokens.peekable();
 
     let Some(token) = tokens.peek() else {
-        return error(dollar_token);
+        return error(
+            dollar_token,
+            "incomplete field reference; use `$$` if you just want a dollar sign",
+        );
     };
 
     return match token {
@@ -162,6 +169,12 @@ fn parse_variable_binding(
             parse_variable_binding_name(dollar_token, FieldMode::Optional, &mut tokens)
         }
 
+        // $:guard $x
+        TokenTree::Punct(punct) if punct.as_char() == ':' => {
+            let guard_token = tokens.next().unwrap();
+            parse_guarded_variable_binding(dollar_token, guard_token, &mut tokens)
+        }
+
         // $<x> or $<?x>
         TokenTree::Punct(punct) if punct.as_char() == '<' => {
             tokens.next();
@@ -172,7 +185,7 @@ fn parse_variable_binding(
             // we should see a `>` next
             match tokens.next() {
                 Some(TokenTree::Punct(punct)) if punct.as_char() == '>' => Ok(result),
-                _ => error(dollar_token),
+                _ => error(dollar_token, "expected a `>` to end this field reference"),
             }
         }
 
@@ -184,7 +197,7 @@ fn parse_variable_binding(
                 unreachable!()
             };
             let Some((open, close)) = open_close(&group) else {
-                return error(&group);
+                return error(&group, "did not expect a spliced macro_rules group here");
             };
 
             // consume `x` or `?x`
@@ -193,14 +206,65 @@ fn parse_variable_binding(
 
             // there shouldn't be anything else in the token tree
             if let Some(t) = group_tokens.next() {
-                return error(&t);
+                return error(
+                    &t,
+                    "extra characters in delimited field reference after field name",
+                );
             }
             Ok(result)
         }
 
-        _ => error(dollar_token),
+        _ => error(dollar_token, "invalid field reference"),
     };
 
+    fn parse_guarded_variable_binding(
+        dollar_token: &Punct,
+        guard_token: TokenTree,
+        tokens: &mut Peekable<impl Iterator<Item = TokenTree>>,
+    ) -> syn::Result<FormalitySpecSymbol> {
+        // The next token should be an identifier
+        let Some(TokenTree::Ident(guard_ident)) = tokens.next() else {
+            return error(
+                &guard_token,
+                "expected an identifier after a `:` in a field reference",
+            );
+        };
+
+        // The next token should be a `$`, beginning another variable binding
+        let next_dollar_token = match tokens.next() {
+            Some(TokenTree::Punct(next_dollar_token)) if next_dollar_token.as_char() == '$' => {
+                next_dollar_token
+            }
+
+            _ => {
+                return error(
+                    &dollar_token,
+                    "expected another `$` field reference to follow the `:` guard",
+                );
+            }
+        };
+
+        // Then should come another field reference.
+        let FormalitySpecSymbol::Field { name, mode } =
+            parse_variable_binding(&next_dollar_token, tokens)?
+        else {
+            return error(
+                &next_dollar_token,
+                "`$:` must be followed by another field reference, not a `$$` literal",
+            );
+        };
+
+        let guard_mode = FieldMode::Guarded {
+            guard: guard_ident,
+            mode: Arc::new(mode),
+        };
+
+        Ok(FormalitySpecSymbol::Field {
+            name: name,
+            mode: guard_mode,
+        })
+    }
+
     fn parse_delimited(
         dollar_token: &Punct,
         open: char,
@@ -236,14 +300,17 @@ fn parse_variable_binding(
         // Extract the name of the field.
         let name = match tokens.next() {
             Some(TokenTree::Ident(name)) => name,
-            _ => return error(dollar_token),
+            _ => return error(dollar_token, "expected field name"),
         };
 
         Ok(FormalitySpecSymbol::Field { name, mode })
     }
 
-    fn error(at_token: &impl Spanned) -> syn::Result<FormalitySpecSymbol> {
-        let message = "invalid field reference in grammar";
+    fn error(at_token: &impl Spanned, message: impl ToString) -> syn::Result<FormalitySpecSymbol> {
+        let mut message = message.to_string();
+        if message.is_empty() {
+            message = "invalid field reference in grammar".into();
+        }
         Err(syn::Error::new(at_token.span(), message))
     }
 }

crates/formality-prove/src/decls.rs

@@ -111,7 +111,7 @@ pub struct ImplDecl {
 }
 
 /// Data bound under the generics from [`ImplDecl`][]
-#[term($trait_ref where $where_clause)]
+#[term($trait_ref $:where $where_clause)]
 pub struct ImplDeclBoundData {
     /// The trait ref that is implemented
     pub trait_ref: TraitRef,
@@ -129,7 +129,7 @@ pub struct NegImplDecl {
 }
 
 /// Data bound under the impl generics for a negative impl
-#[term(!$trait_ref where $where_clause)]
+#[term(!$trait_ref $:where $where_clause)]
 pub struct NegImplDeclBoundData {
     pub trait_ref: TraitRef,
     pub where_clause: Wcs,
@@ -209,7 +209,7 @@ pub struct TraitInvariantBoundData {
 }
 
 /// The "bound data" for a [`TraitDecl`][] -- i.e., what is covered by the forall.
-#[term(where $where_clause)]
+#[term($:where $where_clause)]
 pub struct TraitDeclBoundData {
     /// The where-clauses declared on the trait
     pub where_clause: Wcs,
@@ -231,7 +231,7 @@ impl AliasEqDecl {
 }
 
 /// Data bound under the impl generics for a [`AliasEqDecl`][]
-#[term($alias = $ty where $where_clause)]
+#[term($alias = $ty $:where $where_clause)]
 pub struct AliasEqDeclBoundData {
     /// The alias that is equal
     pub alias: AliasTy,
@@ -258,7 +258,7 @@ impl AliasBoundDecl {
     }
 }
 
-#[term($alias : $ensures where $where_clause)]
+#[term($alias : $ensures $:where $where_clause)]
 pub struct AliasBoundDeclBoundData {
     pub alias: AliasTy,
     // FIXME: this is currently encoded as something like `<T> [T: Foo]` where
@@ -281,7 +281,7 @@ pub struct AdtDecl {
 }
 
 /// The "bound data" for a [`AdtDecl`][].
-#[term(where $where_clause)]
+#[term($:where $where_clause)]
 pub struct AdtDeclBoundData {
     /// The where-clauses declared on the ADT,
     pub where_clause: Wcs,

crates/formality-rust/src/grammar.rs

@@ -96,7 +96,7 @@ impl Struct {
     }
 }
 
-#[term(where $where_clauses { $,fields })]
+#[term($:where $,where_clauses { $,fields })]
 pub struct StructBoundData {
     pub where_clauses: Vec<WhereClause>,
     pub fields: Vec<Field>,
@@ -148,7 +148,7 @@ pub struct Adt {
     pub binder: Binder<AdtBoundData>,
 }
 
-#[term(where $where_clauses { $,variants })]
+#[term($:where $,where_clauses { $,variants })]
 pub struct AdtBoundData {
     pub where_clauses: Vec<WhereClause>,
     pub variants: Vec<Variant>,
@@ -179,7 +179,7 @@ impl<T: Term> TraitBinder<T> {
     }
 }
 
-#[term(where $where_clauses { $*trait_items })]
+#[term($:where $,where_clauses { $*trait_items })]
 pub struct TraitBoundData {
     pub where_clauses: Vec<WhereClause>,
     pub trait_items: Vec<TraitItem>,
@@ -199,7 +199,7 @@ pub struct Fn {
     pub binder: Binder<FnBoundData>,
 }
 
-#[term($(input_tys) -> $output_ty where $where_clauses $body)]
+#[term($(input_tys) -> $output_ty $:where $,where_clauses $body)]
 pub struct FnBoundData {
     pub input_tys: Vec<Ty>,
     pub output_ty: Ty,
@@ -232,7 +232,7 @@ pub struct AssociatedTy {
     pub binder: Binder<AssociatedTyBoundData>,
 }
 
-#[term(: $ensures where $where_clauses)]
+#[term(: $ensures $:where $,where_clauses)]
 pub struct AssociatedTyBoundData {
     /// So e.g. `type Item : [Sized]` would be encoded as `<type I> (I: Sized)`.
     pub ensures: Vec<WhereBound>,
@@ -252,7 +252,7 @@ impl TraitImpl {
     }
 }
 
-#[term($trait_id $<?trait_parameters> for $self_ty where $where_clauses { $*impl_items })]
+#[term($trait_id $<?trait_parameters> for $self_ty $:where $,where_clauses { $*impl_items })]
 pub struct TraitImplBoundData {
     pub trait_id: TraitId,
     pub self_ty: Ty,
@@ -272,7 +272,7 @@ pub struct NegTraitImpl {
     pub binder: Binder<NegTraitImplBoundData>,
 }
 
-#[term(!$trait_id $<?trait_parameters> for $self_ty where $where_clauses { })]
+#[term(!$trait_id $<?trait_parameters> for $self_ty $:where $,where_clauses { })]
 pub struct NegTraitImplBoundData {
     pub trait_id: TraitId,
     pub self_ty: Ty,
@@ -300,7 +300,7 @@ pub struct AssociatedTyValue {
     pub binder: Binder<AssociatedTyValueBoundData>,
 }
 
-#[term(= $ty where $where_clauses)]
+#[term(= $ty $:where $,where_clauses)]
 pub struct AssociatedTyValueBoundData {
     pub where_clauses: Vec<WhereClause>,
     pub ty: Ty,