From dcde5386702d0d71b0e7d26fd032ede9abc73f36 Mon Sep 17 00:00:00 2001 From: xonx <119700621+xonx4l@users.noreply.github.com> Date: Thu, 25 Jun 2026 11:37:04 +0000 Subject: [PATCH 1/2] optional-fn-return-type --- crates/formality-macros/src/debug.rs | 7 +- crates/formality-macros/src/parse.rs | 208 +++++++---------------- crates/formality-macros/src/spec.rs | 55 +++++- crates/formality-rust/src/grammar/fns.rs | 2 +- crates/formality-rust/src/grammar/ty.rs | 7 + crates/formality-rust/src/test.rs | 46 +++++ tests/functions.rs | 16 ++ 7 files changed, 181 insertions(+), 160 deletions(-) diff --git a/crates/formality-macros/src/debug.rs b/crates/formality-macros/src/debug.rs index e816ef00e..515dfd860 100644 --- a/crates/formality-macros/src/debug.rs +++ b/crates/formality-macros/src/debug.rs @@ -325,7 +325,12 @@ fn debug_field_with_mode(name: &Ident, mode: &FieldMode) -> TokenStream { } FieldMode::Guarded { guard, mode } => { - let guard = as_literal(guard); + // The guard can be a keyword (`where`) or an operator (`->`) print + // its text either way. + let guard = match guard { + spec::Guard::Keyword(ident) => Literal::string(&ident.to_string()), + spec::Guard::Operator(operator) => Literal::string(operator), + }; let base = debug_field_with_mode(name, mode); quote_spanned! { name.span() => diff --git a/crates/formality-macros/src/parse.rs b/crates/formality-macros/src/parse.rs index 58a4cd09b..c5764dde7 100644 --- a/crates/formality-macros/src/parse.rs +++ b/crates/formality-macros/src/parse.rs @@ -520,149 +520,67 @@ fn wrap_field_mode( } FieldMode::Guarded { guard, mode } => { - let guard_keyword = as_literal(guard); - match mode.as_ref() { + // A guard is present when its leading token matches. `cond` is a + // `bool` expression that consumes the leading token on success (and + // nothing on failure) `after` consumes any remaining guard tokens + // once we have committed to the guard. + let (cond, after) = match guard { + spec::Guard::Keyword(ident) => { + let keyword = as_literal(ident); + (quote!(__p.expect_keyword(#keyword).is_ok()), quote!()) + } + spec::Guard::Operator(operator) => { + let mut chars = operator.chars(); + let first = chars + .next() + .expect("operator guard must have at least one character"); + let rest: Vec = + chars.map(|c| quote!(__p.expect_char(#c)?;)).collect(); + (quote!(__p.expect_char(#first).is_ok()), quote!(#(#rest)*)) + } + }; + + // How to parse the field once the guard has matched. + let parse_present = match mode.as_ref() { FieldMode::Single => { if let Some(ty) = field_ty { if let Some(inner_ty) = option_inner_type(ty) { - quote_spanned!(name.span() => - match __p.expect_keyword(#guard_keyword) { - Ok(()) => { - __p.each_nonterminal(|#name: #inner_ty, __p| { - let #name: #ty = Some(#name); - #inner - }) - } - Err(_) => { - let #name: #ty = None; - #inner - } - } - ) + quote!(__p.each_nonterminal(|#name: #inner_ty, __p| { + let #name: #ty = Some(#name); + #inner + })) } else { - quote_spanned!(name.span() => - match __p.expect_keyword(#guard_keyword) { - Ok(()) => { - __p.each_nonterminal(|#name: #ty, __p| { - #inner - }) - } - Err(_) => { - let #name: #ty = Default::default(); - #inner - } - } - ) + quote!(__p.each_nonterminal(|#name: #ty, __p| { #inner })) } } else { - quote_spanned!(name.span() => - match __p.expect_keyword(#guard_keyword) { - Ok(()) => { - __p.each_nonterminal(|#name, __p| { - #inner - }) - } - Err(_) => { - let #name = Default::default(); - #inner - } - } - ) + quote!(__p.each_nonterminal(|#name, __p| { #inner })) } } FieldMode::Optional => { if let Some(ty) = field_ty { - quote_spanned!(name.span() => - match __p.expect_keyword(#guard_keyword) { - Ok(()) => { - __p.each_opt_nonterminal(|#name: Option<#ty>, __p| { - let #name: #ty = #name.unwrap_or_default(); - #inner - }) - } - Err(_) => { - let #name: #ty = Default::default(); - #inner - } - } - ) + quote!(__p.each_opt_nonterminal(|#name: Option<#ty>, __p| { + let #name: #ty = #name.unwrap_or_default(); + #inner + })) } else { - quote_spanned!(name.span() => - match __p.expect_keyword(#guard_keyword) { - Ok(()) => { - __p.each_opt_nonterminal(|#name, __p| { - let #name = #name.unwrap_or_default(); - #inner - }) - } - Err(_) => { - let #name = Default::default(); - #inner - } - } - ) + quote!(__p.each_opt_nonterminal(|#name, __p| { + let #name = #name.unwrap_or_default(); + #inner + })) } } FieldMode::Many => { if let Some(ty) = field_ty { - quote_spanned!(name.span() => - match __p.expect_keyword(#guard_keyword) { - Ok(()) => { - __p.each_many_nonterminal(|#name: #ty, __p| { - #inner - }) - } - Err(_) => { - let #name: #ty = Default::default(); - #inner - } - } - ) + quote!(__p.each_many_nonterminal(|#name: #ty, __p| { #inner })) } else { - quote_spanned!(name.span() => - match __p.expect_keyword(#guard_keyword) { - Ok(()) => { - __p.each_many_nonterminal(|#name, __p| { - #inner - }) - } - Err(_) => { - let #name = Default::default(); - #inner - } - } - ) + quote!(__p.each_many_nonterminal(|#name, __p| { #inner })) } } FieldMode::Comma => { if let Some(ty) = field_ty { - quote_spanned!(name.span() => - match __p.expect_keyword(#guard_keyword) { - Ok(()) => { - __p.each_comma_nonterminal(|#name: #ty, __p| { - #inner - }) - } - Err(_) => { - let #name: #ty = Default::default(); - #inner - } - } - ) + quote!(__p.each_comma_nonterminal(|#name: #ty, __p| { #inner })) } else { - quote_spanned!(name.span() => - match __p.expect_keyword(#guard_keyword) { - Ok(()) => { - __p.each_comma_nonterminal(|#name, __p| { - #inner - }) - } - Err(_) => { - let #name = Default::default(); - #inner - } - } - ) + quote!(__p.each_comma_nonterminal(|#name, __p| { #inner })) } } FieldMode::DelimitedVec { @@ -673,40 +591,32 @@ fn wrap_field_mode( let open = Literal::character(*open); let close = Literal::character(*close); if let Some(ty) = field_ty { - quote_spanned!(name.span() => - match __p.expect_keyword(#guard_keyword) { - Ok(()) => { - __p.each_delimited_nonterminal(#open, #optional, #close, |#name: #ty, __p| { - #inner - }) - } - Err(_) => { - let #name: #ty = Default::default(); - #inner - } - } - ) + quote!(__p.each_delimited_nonterminal(#open, #optional, #close, |#name: #ty, __p| { #inner })) } else { - quote_spanned!(name.span() => - match __p.expect_keyword(#guard_keyword) { - Ok(()) => { - __p.each_delimited_nonterminal(#open, #optional, #close, |#name, __p| { - #inner - }) - } - Err(_) => { - let #name = Default::default(); - #inner - } - } - ) + quote!(__p.each_delimited_nonterminal(#open, #optional, #close, |#name, __p| { #inner })) } } FieldMode::Guarded { .. } => { // Nested guarded — unlikely but handle by falling back panic!("nested Guarded modes are not supported"); } - } + }; + + // How to fill the field in when the guard is absent. + let parse_absent = if let Some(ty) = field_ty { + quote!(let #name: #ty = Default::default(); #inner) + } else { + quote!(let #name = Default::default(); #inner) + }; + + quote_spanned!(name.span() => + if #cond { + #after + #parse_present + } else { + #parse_absent + } + ) } } } diff --git a/crates/formality-macros/src/spec.rs b/crates/formality-macros/src/spec.rs index 794a49885..635794c64 100644 --- a/crates/formality-macros/src/spec.rs +++ b/crates/formality-macros/src/spec.rs @@ -34,13 +34,25 @@ pub enum FormalitySpecSymbol { Delimeter { text: char }, } +/// The token that gates a [`FieldMode::Guarded`] field. It is parsed only if +/// the guard is present in the input. +#[derive(Debug)] +pub enum Guard { + /// A keyword guard, e.g. the `where` in `$:where $,where_clauses`. + Keyword(Ident), + + /// A run of punctuation, e.g. the `->` in `$:-> $output_ty`. + Operator(String), +} + #[derive(Debug)] pub enum FieldMode { /// $x -- just parse `x` Single, - /// $:ident $nt -- try to parse `ident` and, if present, parse `$nt` - Guarded { guard: Ident, mode: Arc }, + /// $:ident $nt -- try to parse the guard (a keyword like `where` or an + /// operator like `->`) and, if present, parse `$nt`; otherwise use `Default`. + Guarded { guard: Guard, mode: Arc }, /// $ -- `x` is a `Vec`, parse `` /// $[x] -- `x` is a `Vec`, parse `[E0,...,En]` @@ -229,12 +241,37 @@ fn parse_variable_binding( guard_token: TokenTree, tokens: &mut Peekable>, ) -> syn::Result { - // 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 guard is either a single keyword identifier (e.g. `where`) or a + // run of punctuation (e.g. `->`). It is terminated by the `$` that + // begins the guarded field reference. + let guard = match tokens.peek() { + Some(TokenTree::Ident(_)) => { + let Some(TokenTree::Ident(guard_ident)) = tokens.next() else { + unreachable!() + }; + Guard::Keyword(guard_ident) + } + + Some(TokenTree::Punct(punct)) if punct.as_char() != '$' => { + let mut operator = String::new(); + while let Some(TokenTree::Punct(punct)) = tokens.peek() { + let ch = punct.as_char(); + // The `$` that introduces the guarded field ends the guard. + if ch == '$' { + break; + } + operator.push(ch); + tokens.next(); + } + Guard::Operator(operator) + } + + _ => { + return error( + &guard_token, + "expected an identifier or operator after a `:` in a field reference", + ); + } }; // The next token should be a `$`, beginning another variable binding @@ -262,7 +299,7 @@ fn parse_variable_binding( }; let guard_mode = FieldMode::Guarded { - guard: guard_ident, + guard, mode: Arc::new(mode), }; diff --git a/crates/formality-rust/src/grammar/fns.rs b/crates/formality-rust/src/grammar/fns.rs index 8d59f2f6c..9e5e5e419 100644 --- a/crates/formality-rust/src/grammar/fns.rs +++ b/crates/formality-rust/src/grammar/fns.rs @@ -10,7 +10,7 @@ pub struct Fn { pub binder: Binder, } -#[term($(input_args) -> $output_ty $:where $,where_clauses $body)] +#[term($(input_args) $:-> $output_ty $:where $,where_clauses $body)] pub struct FnBoundData { pub input_args: Vec, pub output_ty: Ty, diff --git a/crates/formality-rust/src/grammar/ty.rs b/crates/formality-rust/src/grammar/ty.rs index 65be3c01d..ab9821057 100644 --- a/crates/formality-rust/src/grammar/ty.rs +++ b/crates/formality-rust/src/grammar/ty.rs @@ -91,6 +91,13 @@ impl Ty { } } +/// The default type is the unit type `()`. +impl Default for Ty { + fn default() -> Self { + Ty::unit() + } +} + // ANCHOR: RigidTy_decl #[term((rigid $name $*parameters))] #[customize(parse, debug)] diff --git a/crates/formality-rust/src/test.rs b/crates/formality-rust/src/test.rs index 89306b957..b7c41adf8 100644 --- a/crates/formality-rust/src/test.rs +++ b/crates/formality-rust/src/test.rs @@ -187,6 +187,52 @@ fn test_parse_trusted_fn() { .assert_debug_eq(&r); } +#[test] +fn test_parse_fn_without_return_type() { + // Same as `test_parse_trusted_fn`, but the return type is omitted. The + // parsed structure is identical `output_ty` defaults to the unit type + // `()`, exactly as if `-> ()` had been written. + let r: Crates = term( + "[ + crate core { + fn run() {trusted} + } + ]", + ); + + expect_test::expect![[r#" + Crates { + crates: [ + Crate { + id: core, + items: [ + Fn( + Fn { + id: run, + safety: Safe, + binder: Binder { + kinds: [], + term: FnBoundData { + input_args: [], + output_ty: RigidTy( + (), + ), + where_clauses: [], + body: FnBody( + TrustedFnBody, + ), + }, + }, + }, + ), + ], + }, + ], + } + "#]] + .assert_debug_eq(&r); +} + #[test] fn test_place_expr_ambiguity_deref_vs_field() { let p: PlaceExpr = term("*p.f"); diff --git a/tests/functions.rs b/tests/functions.rs index a5db9d753..0c760d148 100644 --- a/tests/functions.rs +++ b/tests/functions.rs @@ -38,3 +38,19 @@ fn lifetime() { .rustc_ok() .ok() } + +#[test] +fn omitted_return_type() { + FormalityTest::new(crates![ + crate Foo { + fn simple_fn() { trusted } + fn one_arg(v0: T) { trusted } + fn with_where<'a, T>(v0: &'a T) + where + T: 'a, + { trusted } + } + ]) + .skip_execute() + .ok() +} From cb28bf51d1f5833deeb28fd35e022c8b7e3e4edd Mon Sep 17 00:00:00 2001 From: xonx <119700621+xonx4l@users.noreply.github.com> Date: Mon, 24 Aug 2026 17:54:10 +0000 Subject: [PATCH 2/2] OutputTy newtype instead of Default for Ty --- crates/formality-macros/src/parse.rs | 7 ++-- crates/formality-rust/src/grammar/fns.rs | 4 +-- crates/formality-rust/src/grammar/ty.rs | 33 +++++++++++++++++-- .../src/grammar/ty/debug_impls.rs | 11 ++++++- 4 files changed, 46 insertions(+), 9 deletions(-) diff --git a/crates/formality-macros/src/parse.rs b/crates/formality-macros/src/parse.rs index c5764dde7..e51333d18 100644 --- a/crates/formality-macros/src/parse.rs +++ b/crates/formality-macros/src/parse.rs @@ -534,9 +534,10 @@ fn wrap_field_mode( let first = chars .next() .expect("operator guard must have at least one character"); - let rest: Vec = - chars.map(|c| quote!(__p.expect_char(#c)?;)).collect(); - (quote!(__p.expect_char(#first).is_ok()), quote!(#(#rest)*)) + ( + quote!(__p.expect_char(#first).is_ok()), + quote!(#(__p.expect_char(#chars)?;)*), + ) } }; diff --git a/crates/formality-rust/src/grammar/fns.rs b/crates/formality-rust/src/grammar/fns.rs index 9e5e5e419..b294da4eb 100644 --- a/crates/formality-rust/src/grammar/fns.rs +++ b/crates/formality-rust/src/grammar/fns.rs @@ -1,5 +1,5 @@ use crate::grammar::expr::Block; -use crate::grammar::{Binder, Ty, ValueId, WhereClause}; +use crate::grammar::{Binder, OutputTy, Ty, ValueId, WhereClause}; use crate::prove::Safety; use formality_core::term; @@ -13,7 +13,7 @@ pub struct Fn { #[term($(input_args) $:-> $output_ty $:where $,where_clauses $body)] pub struct FnBoundData { pub input_args: Vec, - pub output_ty: Ty, + pub output_ty: OutputTy, pub where_clauses: Vec, pub body: MaybeFnBody, } diff --git a/crates/formality-rust/src/grammar/ty.rs b/crates/formality-rust/src/grammar/ty.rs index ab9821057..8e98dbac0 100644 --- a/crates/formality-rust/src/grammar/ty.rs +++ b/crates/formality-rust/src/grammar/ty.rs @@ -91,10 +91,37 @@ impl Ty { } } -/// The default type is the unit type `()`. -impl Default for Ty { +/// The return type of a function: a [`Ty`] that defaults to `()`, which +/// is what lets `-> $output_ty` be omitted. +#[term($ty)] +#[customize(debug)] +pub struct OutputTy { + pub ty: Ty, +} + +impl Default for OutputTy { fn default() -> Self { - Ty::unit() + OutputTy { ty: Ty::unit() } + } +} + +impl std::ops::Deref for OutputTy { + type Target = Ty; + + fn deref(&self) -> &Ty { + &self.ty + } +} + +impl UpcastFrom for Ty { + fn upcast_from(output_ty: OutputTy) -> Self { + output_ty.ty + } +} + +impl UpcastFrom for Parameter { + fn upcast_from(output_ty: OutputTy) -> Self { + output_ty.ty.upcast() } } diff --git a/crates/formality-rust/src/grammar/ty/debug_impls.rs b/crates/formality-rust/src/grammar/ty/debug_impls.rs index c3217baae..9ac94b117 100644 --- a/crates/formality-rust/src/grammar/ty/debug_impls.rs +++ b/crates/formality-rust/src/grammar/ty/debug_impls.rs @@ -1,8 +1,17 @@ use crate::grammar::PtrKind; -use super::{AliasName, AliasTy, AssociatedTyName, Parameter, RefKind, RigidName, RigidTy}; +use super::{ + AliasName, AliasTy, AssociatedTyName, OutputTy, Parameter, RefKind, RigidName, RigidTy, +}; use std::fmt::Debug; +/// `OutputTy` is a transparent wrapper around `Ty`, so print it as the type it wraps. +impl Debug for OutputTy { + fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result { + Debug::fmt(&self.ty, f) + } +} + // ANCHOR: RigidTy_impl impl Debug for RigidTy { fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result {