Compile time lambda calculator in C++

lambda_calculator.cpp

#include <type_traits>
#include <tuple>
#include <iostream>
#include <string>

namespace lambda_term {
    struct TermBase {};

    template <typename T>
    concept Term = std::is_base_of_v<TermBase, T>;

    template <unsigned X>       struct Var : TermBase {};
    template <Term T1, Term T2> struct App : TermBase {};
    template <Term T>           struct Lam : TermBase {};

}

using lambda_term::Var, lambda_term::App, lambda_term::Lam,  lambda_term::Term;

namespace lifting {

    template <int m, int k, Term T> struct lift_impl;
    template <int m, int k, Term T> using lift = typename lift_impl<m, k, T>::res;

    template <int m, int k, unsigned I> struct lift_impl<m, k, Var<I>> {
        using res = Var< I < m ? I : I + k >;
    };
    template <int m, int k, Term L, Term R> struct lift_impl<m, k, App<L, R>> {
        using liftL = lift<m, k, L>;
        using liftR = lift<m, k, R>;
        using res = App<liftL, liftR>;
    };
    template <int m, int k, Term T> struct lift_impl<m, k, Lam<T>> {
        using liftT = lift<m + 1, k, T>;
        using res = Lam<liftT>;
    };

}

namespace substitution {

    template <Term A, Term N, unsigned I> struct subst_impl;
    template <Term A, Term N, unsigned I = 0> using subst = typename subst_impl<A, N, I>::res;
    template <Term M, Term N> using beta = lifting::lift<0, -1, subst<M, lifting::lift<0, 1, N>, 0>>;

    template <Term N, unsigned I> struct subst_impl<Var<I>, N, I> {
        using res = N;
    };
    template <Term N, unsigned I, unsigned i> struct subst_impl<Var<i>, N, I> {
        using res = Var<i>;
    };
    template <Term N, Term L, Term R, unsigned I> struct subst_impl<App<L, R>, N, I> {
        using substL = subst<L, N, I>;
        using substR = subst<R, N, I>;
        using res = App<substL, substR>;
    };
    template <Term N, Term T, unsigned I> struct subst_impl<Lam<T>, N, I> {
        using substT = subst<T, lifting::lift<0, 1, N>, I + 1>;
        using res = Lam<substT>;
    };

}

namespace evaluation {

    struct NF : lambda_term::TermBase {};

    template <unsigned I>     auto constexpr one_step_impl(Var<I>);
    template <Term T>         auto constexpr one_step_impl(Lam<T>);
    template <Term M, Term N> auto constexpr one_step_impl(App<Lam<M>, N>);
    template <Term L, Term R> auto constexpr one_step_impl(App<L, R>);

    template <Term T> using one_step = decltype(one_step_impl(T{}));
    template <Term T> 
    auto constexpr eval_normal_impl() {
        using StepT = one_step<T>;
        if constexpr (std::is_same_v<NF, StepT>) {
            return T{};
        } else {
            return eval_normal_impl<StepT>();
        }
    };
    template <Term T> using eval_normal = decltype(eval_normal_impl<T>());

    template <unsigned I> auto constexpr one_step_impl(Var<I>) { 
        return NF{}; 
    };

    template <Term T> 
    auto constexpr one_step_impl(Lam<T>) { 
        using EvalT = one_step<T>;
        if constexpr (std::is_same_v<NF, EvalT>) {
            return NF{};
        } else {
            return Lam<EvalT>{};
        }
    };

    template <Term L, Term R> 
    auto constexpr one_step_impl(App<L, R>) { 
        using EvalL = one_step<L>;
        using EvalR = one_step<R>;

        if constexpr (std::is_same_v<NF, EvalL>) {
            if constexpr (std::is_same_v<NF, EvalR>) {
                return NF{};
            } else {
                return App<L, EvalR>{};
            }
        } else {
            return App<EvalL, R>{};
        }
    };

    template <Term M, Term N>
    auto constexpr one_step_impl(App<Lam<M>, N>) { 
        using EvalM = one_step<Lam<M>>;

        if constexpr (std::is_same_v<NF, EvalM>) {
            return substitution::beta<M, N>{};
        } else {
            return App<EvalM, N>{};
        }
    };

    template <Term M, Term N>
    static constexpr bool equals = std::same_as<eval_normal<M>, eval_normal<N>>;
}


using evaluation::eval_normal;
using evaluation::equals;


namespace pretty_printer {

    template <unsigned I> 
    std::string pretty_print_impl (Var<I>, char c) {
        return std::string() + char(c - I - 1);
    };

    template <Term L, Term R> 
    std::string pretty_print_impl (App<L, R>, char c) {
        return "(" + pretty_print(L{}, c) + ")(" + pretty_print_impl(R{}, c) + ")";
    };

    template <Term T> 
    std::string pretty_print_impl (Lam<T>, char c) {
        return std::string("\\") + c + " -> " + pretty_print_impl(T{}, c + 1);
    };

    template <Term T>
    std::string pretty_print = pretty_print_impl(T{}, 'a');

}

using pretty_printer::pretty_print;

namespace parser {
    template <unsigned N, const char (&STR)[N], unsigned POS, typename STACK> 
    constexpr auto parse_impl(STACK);

    template <unsigned N, const char (&STR)[N], unsigned POS, typename STACK > 
    using parse_pos = decltype(parse_impl<N, STR, POS, STACK>({}));

    template <unsigned N, const char (&STR)[N]> 
    using parse = parse_pos<N, STR, 0, int>;

    template <typename RES, unsigned POS> 
    struct parsing_result {
        using type = RES;
        static constexpr unsigned pos = POS;
    };

    template <char C, typename T> struct Cons {};

    template <unsigned I, char S, char C, typename Cs> 
    constexpr char get_stack_element_impl(Cons<C, Cs>) {
        if constexpr (C == S) {
            return I;
        } else {
            return get_stack_element_impl<I + 1, S>(Cs{});
        }
    }

    template <typename STACK, char S> 
    constexpr char get_stack_element = get_stack_element_impl<0, S>(STACK{});

    template <unsigned N, const char (&STR)[N], unsigned POS, typename STACK> 
    constexpr auto parse_var_impl(STACK) {
        return parsing_result<Var<get_stack_element<STACK, STR[POS]>>, POS + 1>{};
    }

    template <unsigned N, const char (&STR)[N], unsigned POS, typename STACK>
    using parse_var = decltype(parse_var_impl<N, STR, POS>(STACK{}));

    template <unsigned N, const char (&STR)[N], unsigned POS, typename STACK> 
    constexpr auto parse_app_impl(STACK) {
        using T1 = parse_pos<N, STR, POS + 1, STACK>;
        using T2 = parse_pos<N, STR, T1::pos + 2, STACK>;
        return parsing_result<App<typename T1::type, typename T2::type>, T2::pos + 1>{};
    }

    template <unsigned N, const char (&STR)[N], unsigned POS, typename STACK>
    using parse_app = decltype(parse_app_impl<N, STR, POS>(STACK{}));

    template <unsigned N, const char (&STR)[N], unsigned POS, typename STACK> 
    constexpr auto parse_lam_impl(STACK) {
        using Stack2 = Cons<STR[POS + 1], STACK>;
        using T = parse_pos<N, STR, POS + 4, Stack2>;
        return parsing_result<Lam<typename T::type>, T::pos>{};
    }

    template <unsigned N, const char (&STR)[N], unsigned POS, typename STACK>
    using parse_lam = decltype(parse_lam_impl<N, STR, POS>(STACK{}));

    template <unsigned N, const char (&STR)[N], unsigned POS, typename STACK> 
    constexpr auto parse_impl(STACK) {
        if constexpr (STR[POS] == '\\') {
            return parse_lam<N, STR, POS, STACK>{};
        } else if constexpr(STR[POS] == '(') {
            return parse_app<N, STR, POS, STACK>{};
        } else {
            return parse_var<N, STR, POS, STACK>{};
        }
    }
}

#define TERM(term) decltype([] {                      \
    static constexpr char str[] = #term;              \
    return parser::parse<sizeof(str), str>::type{};   \
}())



int main() {
    // Test

    using K = TERM(\\x->\\y->x); 
    using KK = TERM(\\y->\\x->\\z->x);

    using Id = TERM(\\x->(\\x->x)((\\x->x)(x)));

    static_assert(equals< App<K, K> , KK >);
    static_assert(equals< App<App<K, K>, K> , K >);
    static_assert(equals< Id, TERM(\\x->x) >);
    std::cout << pretty_print<eval_normal<KK>> << std::endl; // \a -> \b -> \c -> b

    return 0;
};

Upd: added simple compile time parser
Grammar:

  Variable = a | b | ... | z
  Term = \\Variable->Term | (Term)(Term) |  Variable 

View on godbolt.org