Skip to content

Instantly share code, notes, and snippets.

@SimonHauguel

SimonHauguel/lc.cpp

Created July 31, 2022 18:02
Show Gist options
  • Save SimonHauguel/5c4c0db871a208d289f3506b657be0e0 to your computer and use it in GitHub Desktop.
Save SimonHauguel/5c4c0db871a208d289f3506b657be0e0 to your computer and use it in GitHub Desktop.
Download ZIP
Lambda Calcul Type Level C++
Raw
lc.cpp
struct O {};
template <class T> struct S;
struct TTrue {};
struct TFalse {};
using _0 = O;
using _1 = S<_0>;
using _2 = S<_1>;
using _3 = S<_2>;
using _4 = S<_3>;
using _5 = S<_4>;
using _6 = S<_5>;
using _7 = S<_6>;
using _8 = S<_7>;
using _9 = S<_8>;
template<class n, class m> struct Eq;
template<> struct Eq<_0, _0> { using res = TTrue; };
template<class m> struct Eq<_0, S<m>> { using res = TFalse; };
template<class n> struct Eq<S<n>, _0> { using res = TFalse; };
template<class n, class m> struct Eq<S<n>, S<m>> { using res = Eq<n, m>::res; };
template<class c, class t, class e> struct IfThenElse;
template<class t, class _> struct IfThenElse<TTrue, t, _> { using res = t; };
template<class _, class e> struct IfThenElse<TFalse, _, e> { using res = e; };
template<int> struct FromInt;
template<> struct FromInt<0> { using unwrap = O; };
template<int n> struct FromInt { using unwrap = S<typename FromInt<n - 1>::unwrap>; };
/*
type LambdaTerm = Var Int | Abs LambdaTerm | App LambdaTerm LambdaTerm
*/
template<class n> struct Var { using rank = n; };
template<class n> struct Abs { using unwrap = n; };
template<class f, class s> struct App { using getFirst = f; using getSecond = s; };
template<class f, class s, class _f = _0, class _s = _0> struct AlphaEquiv;
template<class n, class m> struct AlphaEquiv<Var<n>, Var<m>> { using res = Eq<n, m>::res; };
template<class n, class m> struct AlphaEquiv<Abs<n>, Abs<m>> { using res = AlphaEquiv<n, m>::res; };
template<class f1, class s1, class f2, class s2> struct AlphaEquiv<App<f1, s1>, App<f2, s2>> {
using res = IfThenElse<
typename AlphaEquiv<f1, f2>::res,
typename AlphaEquiv<s1, s2>::res,
TFalse
>::res;
};
template<class w, class t, class n, class _u = _0> struct Substitute;
template<class w, class t, class n> struct Substitute<Var<w>, t, n> {
using res = IfThenElse<typename Eq<w, n>::res, t, Var<w>>::res;
};
template<class w, class t, class n> struct Substitute<Abs<w>, t, n> {
using res = Abs<typename Substitute<w, t, S<n>>::res>;
};
template<class w1, class t, class n, class w2> struct Substitute<App<w1, w2>, t, n> {
using res = App<
typename Substitute<w1, t, n>::res,
typename Substitute<w2, t, n>::res
>;
};
template<class n, class _n = _0> struct BetaRed {};
template<class n> struct BetaRed<Var<n>> { using res = Var<n>; };
template<class l> struct BetaRed<Abs<l>> { using res = Abs<typename BetaRed<l>::res>; };
template<class f, class s> struct BetaRed<App<Abs<f>, s>> { using res = typename BetaRed<typename Substitute<f, s, _1>::res>::res; };
template<class f, class s> struct BetaRed<App<f, s>> { using res = App<typename BetaRed<f>::res, typename BetaRed<s>::res>; };
#define α₌ AlphaEquiv
#define λ Abs
#define β˃ BetaRed
int main() {
BetaRed<
App<Abs<Var<_1>>, Var<_3>>
>::res foo;
}
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment