Интерпретатор бестипового лямбда-исчисления на шаблонах С++
//////////////////////////////////////////////////////////////////////////////// | |
/// Kernel definitions | |
template <char Var> struct Ref; | |
template <char Var, class Exp> struct Lam; | |
template <class Fun, class Arg> struct App; | |
struct NullEnv; | |
template <char Var, class Env> struct Lookup; | |
template <char Var, class Val, class Env> struct Bind; | |
template <char Var> | |
struct Lookup<Var, NullEnv>; | |
template <char Var, class Val, class Env> | |
struct Lookup<Var, Bind<Var, Val, Env>> | |
{ | |
typedef Val result; | |
}; | |
template <char Var, char OtherVar, class Val, class Env> | |
struct Lookup<Var, Bind<OtherVar, Val, Env>> | |
{ | |
typedef typename Lookup<Var, Env>::result result; | |
}; | |
template <class Abs, class Env> struct Closure; | |
template <class Exp, class Env> struct Eval; | |
template <class Fun, class Arg> struct Apply; | |
template <char Var, class Env> | |
struct Eval<Ref<Var>, Env> | |
{ | |
typedef typename Lookup<Var, Env>::result value; | |
}; | |
template <char Var, class Exp, class Env> | |
struct Eval<Lam<Var, Exp>, Env> | |
{ | |
typedef Closure<Lam<Var, Exp>, Env> value; | |
}; | |
template <class Fun, class Arg, class Env> | |
struct Eval<App<Fun, Arg>, Env> | |
{ | |
typedef typename Apply<typename Eval<Fun, Env>::value, | |
typename Eval<Arg, Env>::value>::result value; | |
}; | |
template <char Var, class Exp, class Env, class Arg> | |
struct Apply<Closure<Lam<Var, Exp>, Env>, Arg> | |
{ | |
typedef typename Eval<Exp, Bind<Var, Arg, Env>>::value result; | |
}; | |
//////////////////////////////////////////////////////////////////////////////// | |
/// Foreign term injection | |
template <class T> struct Inj; | |
template <class T, class Env> | |
struct Eval<Inj<T>, Env> | |
{ | |
typedef T value; | |
}; | |
//////////////////////////////////////////////////////////////////////////////// | |
/// Unchurchifier | |
struct Zero | |
{ | |
static const unsigned int interpretation = 0; | |
}; | |
struct Succ; | |
template <class N> | |
struct Apply<Succ, N> | |
{ | |
typedef struct _ { | |
static const unsigned int interpretation = N::interpretation + 1; | |
} result; | |
}; | |
/// /// | |
//////////////////////////////////////////////////////////////////////////////// | |
#include <iostream> | |
int main() | |
{ | |
// 1 = λfx.f x | |
typedef Lam<'f', Lam<'x', App<Ref<'f'>, Ref<'x'>>>> One; | |
// 2 = λfx.f (f x) | |
typedef Lam<'f', Lam<'x', App<Ref<'f'>, App<Ref<'f'>, Ref<'x'>>>>> Two; | |
// + = λab.λfx.a f (b f x) | |
typedef Lam<'a', Lam<'b', Lam<'f', Lam<'x', | |
App<App<Ref<'a'>, Ref<'f'>>, | |
App<App<Ref<'b'>, Ref<'f'>>, Ref<'x'>>> | |
>>>> Plus; | |
// Sum = (+ 1 2) | |
typedef App<App<Plus, One>, Two> Sum; | |
// Result := (Sum +1 =0) | |
typedef App<App<Sum, Inj<Succ>>, Inj<Zero>> Output; | |
typedef Eval<Output, NullEnv>::value Result; | |
std::cout << Result::interpretation; | |
} |
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment