build.rs

use std::{env, fs, path::PathBuf};

const MAX_N: usize = 8 * 1024;

fn main() {
    println!("cargo:rerun-if-changed=build.rs");

    let out_dir = PathBuf::from(env::var("OUT_DIR").expect("OUT_DIR should be set by Cargo"));

    let nats_path = out_dir.join("generated_nats.rs");
    let expr_nat_path = out_dir.join("generated_expr_nat.rs");

    fs::write(&nats_path, generate_nats()).expect("write generated_nats.rs");
    fs::write(&expr_nat_path, generate_expr_nat()).expect("write generated_expr_nat.rs");
}

fn generate_nats() -> String {
    let mut out = String::new();
    out.push_str("// @generated by build.rs\n");
    out.push_str(&format!("// Defines N0..N{} as Peano naturals.\n\n", MAX_N));

    out.push_str("pub type N0 = Z;\n");
    for i in 1..=MAX_N {
        out.push_str(&format!("pub type N{} = S<N{}>;\n", i, i - 1));
    }

    out
}
fn generate_expr_nat() -> String {
    let mut out = String::new();
    out.push_str("// @generated by build.rs\n");
    out.push_str("// Maps numeric literals to Const<N..> for expr! parsing.\n\n");

    out.push_str("#[macro_export]\nmacro_rules! expr_nat {\n");
    for i in 0..=MAX_N {
        out.push_str(&format!(
            "    ({n}) => {{ $crate::Const<$crate::N{n}> }};\n",
            n = i
        ));
    }
    out.push_str("}\n\n");

    out
}