class Expr{
public:
	Expr typecheck(Context&);
	Expr nf(Context&);
	Expr subst(int index, Expr);
	bool depends(int index);
};

class LambdaExpr: public Expr{
public:

	Expr typecheck(Context&){
		Expr bodyType = c.withBinding(paramType, [](Context& c){
			return body.typecheck(c);
		});
		return ArrowExpr(paramType, bodyType);
	}

	Expr nf(Context& c){
		Expr paramNF = paramType.nf(c);
		return LambdaExpr(paramNF, c.withBinding(paramNF, [](Context& c){
			return body.nf(c)
		});
	}

	Expr subst(int index, Expr e){
		return LambdaExpr(paramType.subst(index, e), body.subst(index + 1, e));
	}

	bool depends(int index){
		return paramType.depends(index) || body.depends(index + 1)
	}

private:
	Expr paramType;
	Expr body;
};


class GlobalRefExpr: public Expr{
public:

	Expr typecheck(Context&){
		return decl->type;
	}

	Expr nf(Context& c){
		return decl->expr.nf(c);
	}

	Expr subst(int index, Expr e){
		return decl->expr;
	}

	bool depends(int index){
		return false;
	}

private:
	Decl* decl;
};

class TypeExpr: public Expr{
public:
	Expr typecheck(Context&){
		return TypeExpr(level + 1);
	}

	Expr nf(Context& c){
		return this;
	}

	Expr subst(int index, Expr e){
		return this;
	}

	bool depends(int index){
		return false;
	}

private:
	int level;
};


class BuiltinNat: public Expr{
public:

	Expr typecheck(Context&){
		return TypeExpr(0);
	}

	Expr nf(Context& c){
		return this;
	}

	Expr subst(int index, Expr e){
		return this;
	}

	bool depends(int index){
		return false;
	}
};

class NatValue: public Expr{
public:

	Expr typecheck(Context&){
		return BuiltinNat();
	}

	Expr nf(Context& c){
		return this;
	}

	Expr subst(int index, Expr e){
		return this;
	}

	bool depends(int index){
		return false;
	}

private:
	int val;
};