import edu.neu.ccs.demeterf.ID;
import edu.neu.ccs.demeterf.Traversal;
import edu.neu.ccs.demeterf.control.EdgeControl;
import edu.neu.ccs.demeterf.control.Edge;
import edu.neu.ccs.demeter.Ident;

class VarT{
    String name;
    Type type; /*[*/
    VarT(String n, Type t){ name = n; type = t; }
    VarT(Ident id){ this(""+id,null); }
    public boolean equals(Object o){
        return ((o instanceof VarT) && 
                ((VarT)o).name.equals(name));
    }
    public String toString(){
        return name+(type==null?"":":"+type);
    }/*]*/
    /* ... */
}

public class TypeCheck extends ID{
    ClassList classes;
    ClassMethList mthds;
    ConDescList constr;
    
    TypeCheck(ClassList c){ 
        classes = c;
        mthds = Methods.methEnv(c); 
        constr = Methods.conEnv(c);
    }

    static Type doCheck(Exp e, ClassList c){
        return new Traversal(new ConstrCheck(c),
                             EdgeControl.builtIns(Ident.class))
            .traverse(e, Env.empty());
    }
    static void methods(ClassList cl){
        ConstrCheck check = new ConstrCheck(cl);
        Traversal t = new Traversal(check,
                                    EdgeControl.builtIns(Ident.class,
                                                         ValueList.class));
        Env<VarT> tenv = Env.empty();
        t.<Boolean>traverse(check.mthds, tenv);
        t.<Boolean>traverse(check.constr, tenv);
    }
}

class ExpCheck extends ID{
    static Type intt = new IntT();
    static Type boolt = new BoolT();

    Type combine(IntLit il){ return intt; }
    Type combine(BoolLit il){ return boolt; }
    Type combine(AddExp e,  IntT l, IntT r){ return intt; }
    Type combine(MultExp e, IntT l, IntT r){ return intt; }
    Type combine(LessExp e, IntT l, IntT r){ return boolt; }
    Type combine(NegExp e,  IntT l){ return intt; }
    Type combine(AndExp e,  BoolT l, BoolT r){ return boolt; }
    Type combine(OpExp e){ throw new TypeErr("Type Error"); }
    Type combine(IfExp e, BoolT c, Type thn, Type els){
        if(thn.equals(els))return thn;
        throw new TypeErr("Bad IfEx: Then & Else Mismatch");
    }
    Type combine(IfExp e, Type c)
      { throw new TypeErr("Bad IfEx: Non-boolean Condition"); }
}

class ConstrCheck extends MethodCheck{
    ConDescList constr;
    
    ConstrCheck(ClassList c){ super(c); constr = Methods.conEnv(c); }

    Type combine(UserT h){ return h; }
    Type combine(NewExp h, UserT t, TypeList args, Env<VarT> env){
        ConDesc c = constr.find(t);
        if(!args.applicable(c.type.args))
            throw new TypeErr("Constr: Bad Arguments");
        return t;
    }

    String combine(SymMethExp h, Ident n){ return ""+n; }
    Type combine(CallExp h, UserT ths, String n, TypeList args){
        ClassMeth cls = mthds.find(ths.name);
        MethDesc meth = cls.mthds.find(n);
        if(!args.applicable(meth.type.args))
            throw new TypeErr("CallExp: Bad Arguments");
        return meth.type.ret;
    }
    Type combine(CallExp h, Type ths, String n){
        throw new TypeErr("CallExp: Bad Target ["+ths+"]");
    }
    Type combine(Assign a, Type ee, Type er){
        if(ee.equals(er))return ee;
        throw new TypeErr("Assign: Type Mismatch");
    }
    TypeList combine(EmptyList e){ return new TypeEmpty(); }
    TypeList combine(ConsList c, Type f, TypeList r){ return r.push(f); }
}

class MethodCheck extends ExpCheck{
    ClassList classes;
    ClassMethList mthds;
    MethodCheck(ClassList c){  classes = c; mthds = Methods.methEnv(c); }
    
    Env<VarT> update(ClassMeth c, Env<VarT> env){
        return env.push(classes.find(c.name).flds.env())
                  .push(new VarT("this", new UserT(c.name)));
    }
    Env<VarT> update(MethDesc m, Env<VarT> env){
        return env.push(m.args.env());
    }
    Env<VarT> update(ConDesc c, Env<VarT> env){
        Env<VarT> e1 = env.push(classes.find(c.name).flds.env());
        return e1.push(c.args.env());
    }
    Env<VarT> update(RevDefRest d, Env<VarT> env){ return push(env, ""+d.id,d.type); }
    
    Type combine(Return r, Type t){ return t; }
    Type combine(SymExp s, Ident id, Env<VarT> env){ return env.find(new VarT(id)).type; }
    Type combine(RevDef h, Type exp, TypePair def){
        if(exp.equals(def.bind))return def.rest;
        throw new TypeErr("Def: Type Mismatch");
    }
    TypePair combine(RevDefRest h, Type b, Ident n, Type r){ return new TypePair(b,r); }

    Type combine(MethDesc h, String n, MethType mt, TypeList arg, Type body){
        if(!mt.ret.equals(body))
            throw new TypeErr("Method: Return Type Mismatch");
        return body;
    }    
    Type combine(Formal f, Type t){ return t; }

    boolean combine(ClassMeth r, String n, TypeList tl){ return true; }
    boolean combine(ConsList r, boolean n){ return true; }
    boolean combine(ConDesc c, String n, MethType t, ValueList def,
                    TypeList args, TypeList res){
        return true;
    }
    Type combine(Type t){ return t; }
    TypeList combine(EmptyList e){ return new TypeEmpty(); }
    TypeList combine(ConsList c, Type f, TypeList r){ return r.push(f); }

    static Env<VarT> push(Env<VarT> e, String n, Type t)
    { return e.push(new VarT(n,t)); }
}