Skip to content

add: optional-fn-return-type #406

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Open
xonx4l wants to merge 2 commits into
base: main
Choose a base branch
from
Open

add: optional-fn-return-type #406

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
2 commits
Select commit Hold shift + click to select a range
dcde538
optional-fn-return-type
xonx4l Jun 25, 2026
cb28bf5
OutputTy newtype instead of Default for Ty
xonx4l Aug 24, 2026
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
7 changes: 6 additions & 1 deletion crates/formality-macros/src/debug.rs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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() =>
Expand Down
209 changes: 60 additions & 149 deletions crates/formality-macros/src/parse.rs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -520,149 +520,68 @@ 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");
(
quote!(__p.expect_char(#first).is_ok()),
quote!(#(__p.expect_char(#chars)?;)*),
)
}
};

// 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 {
Expand All @@ -673,40 +592,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
}
)
}
}
}
Expand Down
55 changes: 46 additions & 9 deletions crates/formality-macros/src/spec.rs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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<FieldMode> },
/// $: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<FieldMode> },

/// $<x> -- `x` is a `Vec<E>`, parse `<E0,...,En>`
/// $[x] -- `x` is a `Vec<E>`, parse `[E0,...,En]`
Expand Down Expand Up @@ -229,12 +241,37 @@ fn parse_variable_binding(
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 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
Expand Down Expand Up @@ -262,7 +299,7 @@ fn parse_variable_binding(
};

let guard_mode = FieldMode::Guarded {
guard: guard_ident,
guard,
mode: Arc::new(mode),
};

Expand Down
6 changes: 3 additions & 3 deletions crates/formality-rust/src/grammar/fns.rs
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -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;

Expand All @@ -10,10 +10,10 @@ pub struct Fn {
pub binder: Binder<FnBoundData>,
}

#[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<InputArg>,
pub output_ty: Ty,
pub output_ty: OutputTy,
pub where_clauses: Vec<WhereClause>,
pub body: MaybeFnBody,
}
Expand Down
Loading
Loading