package code.type.typechecker;

import code.symbols.DataSymbol;
import code.table.MapTable;
import code.term.*;
import code.term.visitor.TermVisitor;
import code.term.visitor.ToStringTermVisitor;
import code.type.*;
import code.type.visitor.PrintAsTxtLoadable;
import code.type.visitor.NormalizeType;
import static code.type.PredefinedTypes.*;
import static code.type.TypeFactory.*;

/**
 * A TermVisitor that gets the type of the Term (arg 1)
 * in the Environment(provided at construction time)
 *
 * @author Pravin Damle
 * @since 12/01/04
 */
public class TermGetTypeVisitor implements TermVisitor<TypeExpression,Object> {

    public static boolean debug_typechecking = false;

    private final Environment env;

    public TermGetTypeVisitor(Environment env) {
        this.env = env;
    }

    public TypeExpression visit(TermImplChar t, Object ignore) {
        return charType;
    }

    public TypeExpression visit(TermImplFloat t, Object ignore) {
        return floatType;
    }

    public TypeExpression visit(TermImplInt t, Object ignore) {
        return intType;
    }

    public TypeExpression visit(TermImplString t, Object ignore) {
        return stringType;
    }

    public TypeExpression visit(TermImplOpaque t, Object ignore) {
	return opaqueType;
    }

    public TypeExpression visit(Variable v, Object ignore) {
        return makeTypeVariable(v.getName());
    }

    public TypeExpression visit(TermImplUser t, Object ignore) {
        // get the data dymbol associsted with this user defined term
        DataSymbol datasym = MapTable.getSymbol(t.getRoot());

        String termStr = null;
        if (debug_typechecking) {
            termStr = t.accept(ToStringTermVisitor.singleton, null) + " Symbol:: " + datasym.moduleName + "." + datasym.symbolName + "  " + PrintAsTxtLoadable.getString(datasym.typeExp);
            System.err.println("Begin TypeChecking the term " + termStr);
        }

        // get the Actual arguments of the term
        Term actual[] = t.getArgument();

        // find the types of the arguments
        TypeExpression actualType[] = new TypeExpression[actual.length];
        for (int i = 0; i < actual.length; i++) {
            actualType[i] = actual[i].getRepresentation().accept(this, env);

            if (debug_typechecking) System.err.println("Data Type for arg " + i + " " + PrintAsTxtLoadable.getString(actualType[i]));
        }

        // Build the type of the term as a recursive function type using the types of its arguments.
        TypeVariable computedResultType = (TypeVariable) (makeTypeVariable("X")).accept
                (new RenameTypeVarVisitor(env), null);

        TypeExpression computedTermType = computedResultType;
        for (int i = actualType.length - 1; i >= 0; i--) {
            computedTermType = makeFunctionType(actualType[i], computedTermType);
        }

        if (debug_typechecking) System.err.println("ComputedType of Term" + PrintAsTxtLoadable.getString(computedResultType));

        // get the symbol's type expression
        TypeExpression datatype = datasym.typeExp;
        // this type expression may contain type variables.
        // ensure that they do not conflict with any type variables that we have identified so far.
        datatype = datatype.accept(new RenameTypeVarVisitor(env), null);

        if (debug_typechecking) System.err.println(" Data Symbol Type " + PrintAsTxtLoadable.getString(datatype));

        try {
            // unify actual type of the term with its expected type.
            unify(datatype, computedTermType);
        } catch (TypeError te) {
            throw new TypeError("In Term " + t.accept(ToStringTermVisitor.singleton, null) +
                    "\nExpected Type is " + PrintAsTxtLoadable.getString(datatype.accept(new RenameTypeVisitor(), null)) +
                    "\nInstead of the Actual Type " + PrintAsTxtLoadable.getString(computedTermType.accept(new RenameTypeVisitor(), null)) +
                    "\n" + te.getMessage());
        }

        TypeExpression newrettype = computedResultType;
        newrettype = newrettype.accept(new ApplySubstTypeVisitor(env), null);

        if (debug_typechecking)
            System.err.println("End   TypeChecking the term " + termStr +
                    " ActualRetType " + PrintAsTxtLoadable.getString(computedResultType) +
                    " ActualWithSubstRetType " + PrintAsTxtLoadable.getString(newrettype));
        return newrettype;
    }

    void unify(TypeExpression x, TypeExpression y) {
        if (debug_typechecking) System.err.println("Begin Unifying [" + PrintAsTxtLoadable.getString(x) + "][" + PrintAsTxtLoadable.getString(y) + "]");

        if (x instanceof TypeVariable) {
            TypeVariable newx = (TypeVariable) x;

            TypeExpression tmp = env.getSubst(newx.name);
            if (tmp != null) {
                unify(tmp, y);
                return;
            }

            if (y instanceof TypeVariable) {
                TypeVariable newy = (TypeVariable) y;
                tmp = env.getSubst(newy.name);
                if (tmp != null) {
                    unify(x, tmp);
                    return;
                }
            }
            // at this point no more substitution can be applied for x and y.

            // check if x occurs in y
            boolean occurs = ((Boolean) y.accept(new OccursCheckTypeVarVisitor(newx), null)).booleanValue();
            if (occurs) {
                if (y instanceof TypeVariable) {
                    // then obviously they share the same name.
                    // So do nothing. Since the type variable obviously unifies with itself.
                } else
                    throw new TypeError(TypeError.errVariableRecursion, x, y);
            } else
                env.setSubst(newx, y);
        } else if (y instanceof TypeVariable) {
            unify(y, x);
        } else if (x instanceof TypeConstructor) {
            if (!(y instanceof TypeConstructor)) throw new TypeError(TypeError.errTypeMismatch, x, y);
            String namex = ((TypeConstructor) x).name;
            String namey = ((TypeConstructor) y).name;
            if (!namex.equals(namey)) {
                throw new TypeError(TypeError.errTypeMismatch, x, y);
            }
        } else if (x instanceof TypeConstructorApplication) {
            if (!(y instanceof TypeConstructorApplication)) throw new TypeError(TypeError.errTypeMismatch, x, y);
            TypeConstructorApplication newx = (TypeConstructorApplication) x;
            TypeConstructorApplication newy = (TypeConstructorApplication) y;

            // was unify(newx.typeConstructor, newy.typeConstructor);
            if (!newx.typeConstructor.equals(newy.typeConstructor)) {
                throw new TypeError(TypeError.errTypeMismatch, x, y);
            }
            if (newx.arguments.length != newy.arguments.length)
                throw new TypeError(TypeError.errArityMismatch, x, y);
            for (int i = 0; i < newx.arguments.length; i++)
                unify(newx.arguments[i], newy.arguments[i]);
        } else if (x instanceof FunctionType) {
            if (!(y instanceof FunctionType)) throw new TypeError(TypeError.errTypeMismatch, x, y);
            FunctionType newx = (FunctionType) x;
            FunctionType newy = (FunctionType) y;
            unify(newx.domain, newy.domain);
            unify(newx.range, newy.range);
        } else {
            throw new TypeError(TypeError.errTypeMismatch, x, y);
        }
        if (debug_typechecking) System.err.println("End   Unifying [" + PrintAsTxtLoadable.getString(x) + "][" + PrintAsTxtLoadable.getString(y) + "]");
    }

    public static TypeExpression getType(Term t) {
        Environment env = new Environment();
        // get return type
        TypeExpression rettype = t.getRepresentation().accept(new TermGetTypeVisitor(env), null);
        // apply Type Variable substitutions
        TypeExpression newrettype = rettype.accept(new ApplySubstTypeVisitor(env), null);
        // Rename any remaining type variables.
        //newrettype = newrettype.accept(new RenameTypeVisitor(), null);
        newrettype = NormalizeType.doit(newrettype) ; // to do or not to do that is the question.
        // return the type.
        return newrettype;
    }
}