#include <stdlib.h>
#include <stdint.h>

typedef void* LPValue;
typedef uint32_t LPNat;

typedef struct LPClosure
{
	LPValue (*func)(LPValue env, LPValue arg);
	LPValue env;
} LPClosure;

static LPNat *makeNat(LPNat initVal)
{
	LPNat *n = malloc(sizeof(LPNat));
	*n = initVal;
	return n;
}

static LPValue apply(LPClosure *closure, LPValue arg)
{
	return closure->func(closure->env, arg);
}

LPNat *Succ(LPNat *k)
{
	return makeNat(*k+1);
}

LPNat *FSucc(LPNat *k)
{
	return makeNat(*k+1);
}

LPValue natElim(LPValue zero, LPClosure *succ, LPNat *n)
{
	LPValue v = zero;
	
	for (LPNat *i = makeNat(0); *i < *n; i = makeNat(*i+1))
	{
		v = apply(apply(succ, i), v);
	}
	
	return v;
}

LPValue finElim(LPClosure *zero, LPClosure *succ,
				LPNat *bound, LPNat *n)
{
	LPValue v = apply(zero, bound);
	
	for (LPNat *i = makeNat(0); *i < *n; i = makeNat(*i+1))
	{
		v = apply(apply(apply(succ, bound), i), v);
	}
	
	return v;
}

LPValue Refl(LPValue v)
{
	return v;
}

LPValue eqElim(LPValue refl, LPValue x, LPValue y, LPValue eq)
{
	return apply(refl, eq);
}

typedef struct LPVecNode
{
	LPValue data;
	struct LPVecNode *rest;
} LPVecNode, *LPVector;

LPVector Nil()
{
	return NULL;
}

LPVector Cons(LPValue val, LPVector vec)
{
	LPVecNode *node = malloc(sizeof(LPVecNode));
	
	node->data = val;
	node->rest = vec;
	return node;
}

LPVector *vecElim(LPValue nilElim, LPClosure *consElim, LPNat *n, LPVector xs)
{
	if (*n > 0)
	{
		LPNat *m = makeNat(*n-1);
		LPValue rec = vecElim(nilElim, consElim, m, xs->rest);
		return apply(apply(apply(apply(consElim, m), xs->data), xs->rest), rec);
	}
	else
	{
		return nilElim;
	}	
}