// StaticTypeCheck.java

import java.util.*;

// Static type checking for Jay is defined by the functions 
// V and the auxiliary functions typing and typeOf.  These
// functions use the classes in the Abstract Syntax of Jay.

class TypeMap extends Hashtable { 

// TypeMap is implemented as a Java Hashtable.  
// It has a 'display' method added to facilitate experimentation.

  public void display () {
    System.out.print("{ ");
    for (Enumeration e = this.keys(); e.hasMoreElements(); ) {
        Variable key = (Variable)e.nextElement();
        Type t = (Type)this.get(key);
        System.out.print("<" + key.id + ", " + t.id + ">");
        if (e.hasMoreElements())
           System.out.print(", ");
    }
    System.out.println(" }");
  }
}

class StaticTypeCheck {

public TypeMap typing (Declarations d) {
  // put the variables and their types into a new 
  // Dictionary (symbol table) and return it.

  TypeMap map = new TypeMap();
  for (int i=0; i<d.size(); i++) {
       map.put (((Declaration)(d.elementAt(i))).v,
                ((Declaration)(d.elementAt(i))).t);
  }
  return map;
} 

public boolean V (Declarations d) {
   for (int i=0; i<d.size() - 1; i++)
     for (int j=i+1; j<d.size(); j++)
       if ((((Declaration)(d.elementAt(i))).v).equals
           (((Declaration)(d.elementAt(j))).v)) 
       return false;
   return true;
} 

public boolean V (Program p) {
  return V (p.decpart) && V (p.body, typing (p.decpart));
} 

public Type typeOf (Expression e, TypeMap tm) {
  if (e instanceof Value) return ((Value)e).type;
  if (e instanceof Variable) {
     Variable v = (Variable)e;
     if (!tm.containsKey(v)) 
       return new Type(Type.UNDEFINED);
     else return (Type) tm.get(v);
  }
  if (e instanceof Binary) {
     Binary b = (Binary)e;
     if (b.op.ArithmeticOp( )) 
       return new Type(Type.INTEGER);
     if (b.op.RelationalOp( ) ||
         b.op.BooleanOp( )) 
       return new Type(Type.BOOLEAN);
  }
  if (e instanceof Unary) {
     Unary u = (Unary)e;
     if (u.op.UnaryOp( )) 
       return new Type(Type.BOOLEAN);
  }
  return null;
} 

public boolean V (Expression e, TypeMap tm) {
  if (e instanceof Value) {
    return true;
  }
  if (e instanceof Variable) {
    return tm.containsKey((Variable)e);
  }
  if (e instanceof Binary) {
     Type typ1 = typeOf(((Binary)e).term1, tm);
     Type typ2 = typeOf(((Binary)e).term2, tm);
     if (! V (((Binary)e).term1, tm)) return false;
     if (! V (((Binary)e).term2, tm)) return false;
     if (((Binary)e).op.ArithmeticOp( ) ||
       ((Binary)e).op.RelationalOp( ))
       return typ1.isInteger() && typ2.isInteger();
     if (((Binary)e).op.BooleanOp( ))
       return typ1.isBoolean() && typ2.isBoolean();
  }
  if (e instanceof Unary) {
     Type typ1 = typeOf(((Unary)e).term, tm);
     return typ1.isBoolean() && V(((Unary)e).term, tm) &&
       (((Unary)e).op.val).equals("!") ;    
  }
  return false;
}

public boolean V (Statement s, TypeMap tm) {
  if (s instanceof Skip || s==null) return true;
  if (s instanceof Assignment) {
     boolean b1 = tm.containsKey(((Assignment)s).target);
     boolean b2 = V(((Assignment)s).source, tm);
     if (b1 && b2) 
       return ((Type)tm.get(((Assignment)s).target)).id.equals 
               (typeOf(((Assignment)s).source, tm).id);
     else return false;
  } 
  if (s instanceof Conditional)
     return V (((Conditional)s).test, tm) &&
        typeOf(((Conditional)s).test, tm).isBoolean() &&
        V (((Conditional)s).thenbranch, tm) &&
        V (((Conditional)s).elsebranch, tm);
  if (s instanceof Loop)
     return V (((Loop)s).test, tm) &&
        typeOf(((Loop)s).test, tm).isBoolean() &&
        V (((Loop)s).body, tm);
  if (s instanceof Block) {
     for (int j=0; j < ((Block)s).members.size(); j++)
       if (! V((Statement)(((Block)s).members.elementAt(j)), tm))
         return false; 
     return true;
  }
  return false;
}

} // class StaticTypeCheck