type_proof_macros/
lib.rs

1#![deny(
2    rustdoc::broken_intra_doc_links,
3    rustdoc::private_intra_doc_links,
4    rustdoc::missing_crate_level_docs,
5    rustdoc::invalid_codeblock_attributes,
6    rustdoc::invalid_html_tags,
7    rustdoc::invalid_rust_codeblocks,
8    rustdoc::bare_urls,
9    rustdoc::unescaped_backticks,
10    missing_docs
11)]
12
13//! Macros for the `type-proof` crate.
14//!
15//! The macros are re-exported in `type-proof`, so it's recommended to just use them through that.
16
17use proc_macro::TokenStream;
18use quote::quote;
19use syn::{LitInt, parse_macro_input};
20
21/// Creates a typed version of the given natural number.
22///
23/// Useful for creating natural numbers beyond the hard-coded type aliases.
24///
25/// # Example
26///
27/// ```
28/// use type_proof::{
29///     peano::{N, N3},
30///     type_utils::assert_type_eq,
31/// };
32///
33/// assert_type_eq::<N!(3), N3>();
34/// ```
35#[proc_macro]
36#[allow(non_snake_case)]
37pub fn N(input: TokenStream) -> TokenStream {
38    let input = parse_macro_input!(input as LitInt);
39    let value = input
40        .base10_parse::<usize>()
41        .expect("natural numbers are non-negative");
42
43    let mut output = quote! { ::type_proof::peano::N0 };
44    for _ in 0..value {
45        output = quote! { ::type_proof::peano::Succ<#output> };
46    }
47
48    TokenStream::from(output)
49}
50
51/// Creates a typed propositional variable with the given natural number as the index.
52///
53/// Useful for creating propositional variables with indices beyond the hard-coded type aliases.
54///
55/// # Example
56///
57/// ```
58/// use type_proof::{
59///     formula::{P, P3},
60///     type_utils::assert_type_eq,
61/// };
62///
63/// assert_type_eq::<P!(3), P3>();
64/// ```
65#[proc_macro]
66#[allow(non_snake_case)]
67pub fn P(input: TokenStream) -> TokenStream {
68    let input = parse_macro_input!(input as LitInt);
69
70    let nat = quote! { ::type_proof_macros::N!(#input) };
71    let output = quote! { ::type_proof::formula::Var<#nat> };
72
73    TokenStream::from(output)
74}
type_proof_macros/lib.rs

type_proof_macros/
lib.rs
