public class CheckType {

        /**
         *  Check that the type of an expression is a type and that the 
         *  expression has that type.
         *  @param m The expression to typecheck
         *  @param a The type of the expression
         */
        public boolean typecheck(Context c, Exp m, Exp a) {
                return checkTypeType(c, a) && checkExpType(c, m, eval(c.rho, a));
        }

        /**
         *  Check that the type of an expression is Type.
         */
        public boolean checkTypeType(Context c, Exp e) {
                return checkType(new TCContext(c), e);
        }

        /**
         *  Check that the type of an expression is the given type
         *  @param e The expression to typecheck
         *  @param v The type of the expression
         */
        public boolean checkExpType(Context c, Exp e, Val v) {
                return checkExp(new TCContext(c), e, v);
        }


        private boolean checkType(TCContext c, Exp e) {
                return checkExp(c, e, new VType());
        }

        private boolean checkExp(TCContext c, Exp e, final Val v) {
                return new ExpVisitor<Boolean,TCContext>() {
                        public Boolean visit(Abs e, TCContext c) { 
                                if (v instanceof VPi) {
                                        VPi p = (VPi)v;
                                        Val vk = new VGen(c.k);
                                        TCContext c_ = new TCContext(c.k+1,
                                                                     c.rho.update(e.id, vk),
                                                                     c.gamma.update(e.id, p.t));
                                        return checkExp(c_, e.e, fapp(p.f, vk));
                                }
                                throw new TypeException("Expected Pi");
                        }
                        public Boolean visit(Pi e, TCContext c) { 
                                if (v instanceof VType) {
                                        TCContext c_ = new TCContext(c.k+1,
                                                                     c.rho.update(e.id, new VGen(c.k)),
                                                                     c.gamma.update(e.id, eval(c.rho, e.t)));
                                        return checkType(c, e.t) && checkType(c_, e.e);
                                }
                                throw new TypeException("Expected Type");
                        }
                        public Boolean visit(Let e, TCContext c) { 
                                TCContext c_ = new TCContext(c.k, 
                                                             c.rho.update(e.id, eval(c.rho, e.e1)),
                                                             c.gamma.update(e.id, eval(c.rho, e.t)));
                                return checkType(c, e.t) && checkExp(c_, e.e2, v);
                        }
                        public Boolean baseVisit(Exp e, TCContext c) {
                                return eqVal(c.k, inferExp(c, e), v);
                        }
                }.visit(e, c);
        }

        private Val inferExp(TCContext c, Exp e) {
                return inferVisitor.visit(e, c);
        }

        private ExpVisitor<Val,TCContext> inferVisitor = new ExpVisitor<Val,TCContext>() {
                public Val visit(Var e, TCContext c) { 
                        return c.gamma.lookup(e.id);
                }
                public Val visit(App e, TCContext c) {
                        Val v = inferExp(c, e.e1);
                        if (v instanceof VPi) {
                                VPi p = (VPi)v;
                                if (checkExp(c, e.e2, p.t))
                                        return fapp(p.f, eval(c.rho, e.e2));
                                throw new TypeException("In application " + e + ": Argument " + e.e2 
                                                        + " does not have type " + p.t);
                        }
                        throw new TypeException("Applied term should be Pi, got " + v);
                }
                public Val visit(Type e, TCContext c) {
                        return new VType();
                }

                public Val baseVisit(Exp e, TCContext c) {
                        throw new TypeException("Cannot infer type of " + e);
                }
        };

        private static class TCContext extends Context {
                public final int k;

                public TCContext(Context c) {
                        super(c);
                        this.k = 0;
                }

                public TCContext(int k, Env rho, Env gamma) {
                        super(rho, gamma);
                        this.k = k;
                }
        }

        public Val fapp(FVal f, Val v) {
                return eval(f.env.update(f.id, v), f.e);
        }

        // conversion algorithm


        public boolean eqVal(Val v1, Val v2) {
                return eqVal(0, v1, v2);
        }

        private boolean eqVal(int k, Val v1, Val v2) {
                if (v1 instanceof VType && v2 instanceof VType) {
                        return true;
                } else if (v1 instanceof VApp && v2 instanceof VApp) {
                        VApp a1 = (VApp)v1, a2 = (VApp)v2;
                        return eqVal(k, a1.v1, a2.v1) && eqVal(k, a1.v2, a2.v2);
                } else if (v1 instanceof VGen && v2 instanceof VGen) {
                        return ((VGen)v1).k == ((VGen)v2).k;
                } else if (v1 instanceof VAbs && v2 instanceof VAbs) {
                        VAbs va1 = (VAbs)v1, va2 = (VAbs)v2;
                        Val vk = new VGen(k);
                        return eqVal(k+1, fapp(va1.f, vk), fapp(va2.f, vk));
                } else if (v1 instanceof VPi && v2 instanceof VPi) {
                        VPi vp1 = (VPi)v1, vp2 = (VPi)v2;
                        Val vk = new VGen(k);
                        return eqVal(k, vp1.t, vp2.t) 
                                && eqVal(k+1, fapp(vp1.f, vk), fapp(vp2.f, vk));
                } else if (v1 instanceof VConst && v2 instanceof VConst) {
                        VConst vc1 = (VConst)v1, vc2 = (VConst)v2;
                        return vc1.name.equals(vc2.name);
                } 
                return false;
        }

        // Weak head normal form stuff

        private Val app(Val v1, Val v2) {
                return appVisitor.visit(v1, v2);
        }

        private ValVisitor<Val,Val> appVisitor = new ValVisitor<Val,Val>() {
                public Val visit(VAbs a, Val v) {
                        return fapp(a.f, v);
                }
                public Val baseVisit(Val u, Val v) {
                        return new VApp(u, v);
                }
        };

        public Val eval(Env env, Exp e) {
                return evalVisitor.visit(e, env);
        }

        private ExpVisitor<Val,Env> evalVisitor = new ExpVisitor<Val,Env>() {
                public Val visit(Var e, Env env) { 
                        return env.lookup(e.id);
                }
                public Val visit(App e, Env env) {
                        return app(eval(env, e.e1), eval(env, e.e2));
                }
                public Val visit(Let e, Env env) {
                        return eval(env.update(e.id, eval(env, e.e1)), e.e2);
                }
                public Val visit(Type e, Env env) {
                        return new VType();
                }
                public Val visit(Abs e, Env env) {
                        return new VAbs(new FVal(e.id, e.e, env));
                }
                public Val visit(Pi e, Env env) {
                        return new VPi(eval(env,e.t), new FVal(e.id, e.e, env));
                }
        };

}