mod inject;
mod validate;
use proc_macro::TokenStream;
use quote::quote;
use syn::parse::{Parse, ParseStream};
use syn::{Expr, LitStr, Token};
#[derive(Default)]
pub(crate) struct IntentArgs {
pub(crate) text: Option<LitStr>,
pub(crate) verify: Option<Expr>,
#[allow(dead_code)] pub(crate) parent: Option<Expr>,
pub(crate) id: Option<LitStr>,
}
impl Parse for IntentArgs {
fn parse(input: ParseStream) -> syn::Result<Self> {
let mut args = IntentArgs::default();
if input.is_empty() {
return Ok(args);
}
args.text = Some(input.parse::<LitStr>()?);
while input.peek(Token![,]) {
input.parse::<Token![,]>()?;
if input.is_empty() {
break; }
let key: syn::Ident = input.parse()?;
input.parse::<Token![=]>()?;
match key.to_string().as_str() {
"verify" => args.verify = Some(input.parse()?),
"parent" => args.parent = Some(input.parse()?),
"id" => args.id = Some(input.parse()?),
other => {
return Err(syn::Error::new(
key.span(),
format!(
"unknown `intent` argument `{other}`; expected one of: verify, parent, id"
),
));
}
}
}
Ok(args)
}
}
#[proc_macro_attribute]
pub fn intent(attr: TokenStream, item: TokenStream) -> TokenStream {
let args = match syn::parse::<IntentArgs>(attr) {
Ok(a) => a,
Err(err) => return err.to_compile_error().into(),
};
if let Err(err) = validate::validate_intent(&args) {
return err.to_compile_error().into();
}
match inject::doc_attribute_or_error(args.id.as_ref()) {
Ok(prefix) => {
let item_ts = proc_macro2::TokenStream::from(item);
quote!(#prefix #item_ts).into()
}
Err(err) => err.to_compile_error().into(),
}
}
#[proc_macro]
pub fn intent_stmt(input: TokenStream) -> TokenStream {
match syn::parse::<IntentArgs>(input).and_then(|args| validate::validate_intent(&args)) {
Ok(()) => TokenStream::new(),
Err(err) => err.to_compile_error().into(),
}
}
#[derive(Default)]
pub(crate) struct AssumeArgs {
pub(crate) text: Option<LitStr>,
#[allow(dead_code)] pub(crate) parent: Option<Expr>,
pub(crate) id: Option<LitStr>,
}
impl Parse for AssumeArgs {
fn parse(input: ParseStream) -> syn::Result<Self> {
let mut args = AssumeArgs::default();
if input.is_empty() {
return Ok(args);
}
args.text = Some(input.parse::<LitStr>()?);
while input.peek(Token![,]) {
input.parse::<Token![,]>()?;
if input.is_empty() {
break;
}
let key: syn::Ident = input.parse()?;
input.parse::<Token![=]>()?;
match key.to_string().as_str() {
"parent" => args.parent = Some(input.parse()?),
"id" => args.id = Some(input.parse()?),
"verify" => {
return Err(syn::Error::new(
key.span(),
"`verify` is not allowed on `assume` (A5): assumptions describe \
invariants you rely on, not properties to be verified. \
Use `intent` if you meant a verifiable claim.",
));
}
other => {
return Err(syn::Error::new(
key.span(),
format!("unknown `assume` argument `{other}`; expected one of: parent, id"),
));
}
}
}
Ok(args)
}
}
#[proc_macro_attribute]
pub fn assume(attr: TokenStream, item: TokenStream) -> TokenStream {
let args = match syn::parse::<AssumeArgs>(attr) {
Ok(a) => a,
Err(err) => return err.to_compile_error().into(),
};
if let Err(err) = validate::validate_assume(&args) {
return err.to_compile_error().into();
}
match inject::doc_attribute_or_error(args.id.as_ref()) {
Ok(prefix) => {
let item_ts = proc_macro2::TokenStream::from(item);
quote!(#prefix #item_ts).into()
}
Err(err) => err.to_compile_error().into(),
}
}
#[proc_macro]
pub fn assume_stmt(input: TokenStream) -> TokenStream {
match syn::parse::<AssumeArgs>(input).and_then(|args| validate::validate_assume(&args)) {
Ok(()) => TokenStream::new(),
Err(err) => err.to_compile_error().into(),
}
}