// StaticTypeCheck.java
//
// This file is from Tucker and Noonan's web site (Appendix B and Chapter 3),
// except that the following changes have been made:
//  (1) Modifications to take advantage of the use of Java Generics in the
//      AbstractSyntax.java file from the previous lab.
//  (2) Modification of TypeMap to also use Java Generics.
//  (3) Addition of a main method to run the type checker.

import java.util.*;
import java.io.IOException;

// 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<Variable,Type> { 

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

  public void display () {
    System.out.print("{ ");
    for (Enumeration<Variable> e = this.keys(); e.hasMoreElements(); ) {
        Variable key = e.nextElement();
        Type t = 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 (d.elementAt(i).v,
                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 (d.elementAt(i).v.equals
           (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 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 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(((Block)s).members.elementAt(j), tm))
         return false; 
     return true;
  }
  return false;
}

    public static void main(String[] args){
        if(args.length != 1){
            System.err.println("Usage: java StaticTypeCheck inputfile");
            System.exit(1);
        }
        try {
            ConcreteSyntax cs = new ConcreteSyntax(new TokenStream(args[0]));
            Program p = cs.program();
            StaticTypeCheck checker = new StaticTypeCheck();
            if(checker.V(p)){
                System.out.println("The program is valid.");
            } else {
                System.out.println("The type checker found one or more errors.");
            }
        } catch (IOException e){
            e.printStackTrace();
            System.exit(1);
        }
    }


} // class StaticTypeCheck