package org.simantics.scl.compiler.types;

import java.io.StringReader;
import java.util.ArrayList;
import java.util.Arrays;
import java.util.Collections;
import java.util.List;

import org.simantics.scl.compiler.common.exceptions.InternalCompilerError;
import org.simantics.scl.compiler.environment.Environments;
import org.simantics.scl.compiler.errors.Locations;
import org.simantics.scl.compiler.internal.parsing.exceptions.SCLSyntaxErrorException;
import org.simantics.scl.compiler.internal.parsing.parser.SCLParserImpl;
import org.simantics.scl.compiler.internal.types.HashConsing;
import org.simantics.scl.compiler.internal.types.TypeElaborationContext;
import org.simantics.scl.compiler.internal.types.effects.EffectIdMap;
import org.simantics.scl.compiler.types.exceptions.KindUnificationException;
import org.simantics.scl.compiler.types.exceptions.MatchException;
import org.simantics.scl.compiler.types.exceptions.Problem;
import org.simantics.scl.compiler.types.exceptions.SCLTypeParseException;
import org.simantics.scl.compiler.types.exceptions.UnificationException;
import org.simantics.scl.compiler.types.kinds.Kind;
import org.simantics.scl.compiler.types.kinds.Kinds;
import org.simantics.scl.compiler.types.util.ITypeEnvironment;
import org.simantics.scl.compiler.types.util.MultiApply;
import org.simantics.scl.compiler.types.util.MultiFunction;
import org.simantics.scl.compiler.types.util.TMultiApply;
import org.simantics.scl.compiler.types.util.TypeUnparsingContext;
import org.simantics.scl.compiler.types.util.Typed;

import gnu.trove.map.hash.THashMap;
import gnu.trove.set.hash.THashSet;

/**
 * An utility class for creating and manipulating types.
 * 
 * @author Hannu Niemistö
 */
public class Types {

    private static final HashConsing<TCon> conCache = 
            new HashConsing<TCon>() {
        protected boolean equals(TCon a, TCon b) {
            return a.name.equals(b.name) && a.module.equals(b.module);
        }

        protected int hashCode(TCon obj) {
            return obj.module.hashCode()*31 + obj.name.hashCode();
        }
    };

    public static final String BUILTIN = "Builtin";

    public static final TCon BOOLEAN = con(BUILTIN, "Boolean");
    public static final TCon BYTE = con(BUILTIN, "Byte");
    public static final TCon CHARACTER = con(BUILTIN, "Character");
    public static final TCon SHORT = con(BUILTIN, "Short");
    public static final TCon INTEGER = con(BUILTIN, "Integer");
    public static final TCon LONG = con(BUILTIN, "Long");
    public static final TCon FLOAT = con(BUILTIN, "Float");
    public static final TCon DOUBLE = con(BUILTIN, "Double");

    public static final TCon STRING = con(BUILTIN, "String");
    public static final TCon ARROW = con(BUILTIN, "->");

    public static final TCon LIST = con(BUILTIN, "[]");
    public static final TCon VECTOR = con(BUILTIN, "Vector");
    public static final TCon MVECTOR = con(BUILTIN, "MVector");
    public static final TCon MAYBE = con(BUILTIN, "Maybe");
    public static final TCon ARRAY = con(BUILTIN, "Array");
    public static final TCon UNIT = con(BUILTIN, "()");
    
    public static final TCon PUNIT = con(BUILTIN, "@");
    
    public static final TCon TYPE_PROXY = con(BUILTIN, "TypeProxy");

    public static final TCon TYPEABLE = con(BUILTIN, "Typeable");
    public static final TCon SERIALIZABLE = con(BUILTIN, "Serializable");
    public static final TCon VEC_COMP = con(BUILTIN, "VecComp");
    public static final TCon CLASS = con(BUILTIN, "Class");
    public static final TCon BINDING = con(BUILTIN, "Binding");

    public static final TCon TYPE = con(BUILTIN, "Type");
    
    public static final TCon DYNAMIC = con("Prelude", "Dynamic");
    public static final TCon VARIANT = con(BUILTIN, "Variant");
    
    public static final TCon ADDITIVE = con("Prelude", "Additive");
    public static final TCon MONAD = con("Prelude", "Monad");
    public static final TCon MONAD_E = con("Prelude", "MonadE");
    public static final TCon INTEGRAL = con("Prelude", "Integral");
    public static final TCon RING = con("Prelude", "Ring");
    public static final TCon ORDERED_RING = con("Prelude", "OrderedRing");
    public static final TCon REAL = con("Prelude", "Real");
    public static final TCon SHOW = con("Prelude", "Show");
    public static final TCon ORD = con("Prelude", "Ord");
    public static final TCon IO = con("Serialization", "IO");

    public static final Type REF = con("Prelude", "Ref");
    
    public static final TCon RANDOM = Types.con("Random", "Random");
    public static final TCon READ_GRAPH = Types.con("Simantics/DB", "ReadGraph");
    public static final TCon WRITE_GRAPH = Types.con("Simantics/DB", "WriteGraph");
    public static final Type RESOURCE = Types.con("Simantics/DB", "Resource"); 
    
    public static final TUnion NO_EFFECTS = new TUnion();
    public static final TCon PROC = con(BUILTIN, "Proc");
    public static final TCon EXCEPTION = con(BUILTIN, "Exception");
    
    public static final TCon BRANCH_POINT = con(BUILTIN, "BranchPoint");
    
    public static final TCon CHRContext = con(BUILTIN, "CHRContext");

    public static final Type BOOLEAN_ARRAY = vector(BOOLEAN);
    public static final Type BYTE_ARRAY = vector(BYTE);
    public static final Type CHARACTER_ARRAY = vector(CHARACTER);
    public static final Type SHORT_ARRAY = vector(SHORT);
    public static final Type INTEGER_ARRAY = vector(INTEGER);
    public static final Type LONG_ARRAY = vector(LONG);
    public static final Type FLOAT_ARRAY = vector(FLOAT);
    public static final Type DOUBLE_ARRAY = vector(DOUBLE);

    private volatile static TCon[] tupleCache = new TCon[] {
        UNIT, null
    };

    private static final ITypeEnvironment DUMMY_TYPE_ENVIRONMENT = new ITypeEnvironment() {

        @Override
        public TCon resolve(String namespace, String name) {
            if(namespace == null)
                return con(BUILTIN, name);
            else
                return con(namespace, name);
        }

    };

    public static boolean isPrimitive(Type type) {
    	return type == BOOLEAN || type == BYTE || type == CHARACTER || type == SHORT ||
    			type == INTEGER || type == LONG || type == FLOAT || type == DOUBLE || type == STRING;
    }
    
    public static boolean isNumeric(Type type) {
    	return type == BYTE || type == SHORT || type == INTEGER || type == LONG || type == FLOAT || type == DOUBLE;
    }
        
    public static TApply apply(Type function, Type parameter) {
        return new TApply(function, parameter);
    }

    public static Type apply(Type function, Type ... parameters) {
        for(Type parameter : parameters)
            function = apply(function, parameter);
        return function;
    }
    
    /**
     * Get the concrete type pointed to by a chain of type meta-variables.
     */
    public static Type canonical(Type type) {
        if(type instanceof TMetaVar) {
            TMetaVar metaVar = (TMetaVar)type;
            type = metaVar.ref;
            if(type == null)
                return metaVar;
            else
                return metaVar.ref = canonical(type);
        }
        return type;
    }

    public static Type closure(Type type, ArrayList<TVar> vars) {
        for(int i=vars.size()-1;i>=0;--i)
            type = forAll(vars.get(i), type);
        return type;
    }

    public static Type closure(Type type, TVar[] vars) {
        for(int i=vars.length-1;i>=0;--i)
            type = forAll(vars[i], type);
        return type;
    }

    public static Type closure(Type type) {
        return closure(type, freeVars(type));
    }

    public static TCon con(String module, String name) {
        return conCache.canonical(new TCon(module, name));
    }

    public static Type[] concat(Type[] a, Type[] b) {
        if(a.length == 0)
            return b;
        if(b.length == 0)
            return a;
        Type[] result = new Type[a.length + b.length];
        for(int i=0;i<a.length;++i)
            result[i] = a[i];
        for(int i=0;i<b.length;++i)
            result[i+a.length] = b[i];
        return result;
    }

    public static TVar[] concat(TVar[] a, TVar[] b) {
        if(a.length == 0)
            return b;
        if(b.length == 0)
            return a;
        TVar[] result = new TVar[a.length + b.length];
        for(int i=0;i<a.length;++i)
            result[i] = a[i];
        for(int i=0;i<b.length;++i)
            result[i+a.length] = b[i];
        return result;
    }

    public static boolean equals(TApply a, TApply b) {
        return equals(a.parameter, b.parameter)
                && equals(a.function , b.function );
    }

    public static boolean equals(TFun a, TFun b) {
        return equals(a.domain, b.domain)
                && equals(a.effect, b.effect)
                && equals(a.range, b.range);
    }
    
    public static boolean subsumes(TFun a, TFun b) {
        return subsumes(b.domain, a.domain)
                && subsumesEffect(a.effect, b.effect)
                && subsumes(a.range, b.range);
    }

    public static boolean subsumesEffect(Type a, Type b) {
        EffectIdMap idMap = new EffectIdMap();
        ArrayList<TMetaVar> mVars = new ArrayList<TMetaVar>(0);
        int idA = idMap.toId(a, mVars);
        int idB = idMap.toId(b, mVars);
        return (idA&idB) == idA;
    }
    
    public static boolean equalsEffect(Type a, Type b) {
        EffectIdMap idMap = new EffectIdMap();
        ArrayList<TMetaVar> mVars = new ArrayList<TMetaVar>(0);
        int idA = idMap.toId(a, mVars);
        int idB = idMap.toId(b, mVars);
        return idA == idB;
    }

    public static boolean equals(TForAll a, TForAll b) {
        Kind aKind = a.var.getKind();
        if(!Kinds.equalsCanonical(aKind, b.var.getKind()))
            return false;
        TVar newVar = var(aKind);
        return equals(a.type.replace(a.var, newVar), b.type.replace(b.var, newVar));
    }

    public static boolean equals(TPred a, TPred b) {
        if(a.typeClass != b.typeClass 
                || a.parameters.length != b.parameters.length)
            return false;
        Type[] aParameters = a.parameters;
        Type[] bParameters = b.parameters;
        for(int i=0;i<aParameters.length;++i)
            if(!equals(aParameters[i], bParameters[i]))
                return false;
        return true;
    }

    public static boolean equals(TUnion a, TUnion b) {
        if(a.effects.length != b.effects.length)
            return false;
        for(int i=0;i<a.effects.length;++i)
            if(!equals(a.effects[i], b.effects[i]))
                return false;
        return true;
    }

    /**
     * Tests equality of two types. Unbound TVars
     * are equal only if they are the same variable.
     * Bound TMetaVar is equal to the type it is bound to.
     * Unbound TMetaVars are equal only if they are the same metavariable.
     * Order of predicates and forall quantifiers matters.
     */
    public static boolean equals(Type a, Type b) {
        a = canonical(a);
        b = canonical(b);
        if(a == b)
            return true;
        Class<?> ca = a.getClass();
        Class<?> cb = b.getClass();
        if(ca != cb)
            return false;
        if(ca == TApply.class) 
            return equals((TApply)a, (TApply)b);
        else if(ca == TFun.class) 
            return equals((TFun)a, (TFun)b);
        else if(ca == TForAll.class)
            return equals((TForAll)a, (TForAll)b);
        else if(ca == TPred.class) 
            return equals((TPred)a, (TPred)b);
        else if(ca == TUnion.class) 
            return equals((TUnion)a, (TUnion)b);        
        else // ca == TCon.class 
            // || (ca == TMetaVar.class && a.ref == null && b.ref == null) 
            // || ca = TVar.class 
            return false; // Equals only if a == b, that was already tested
    }
    
    public static boolean subsumes(Type a, Type b) {
        a = canonical(a);
        b = canonical(b);
        if(a == b)
            return true;
        Class<?> ca = a.getClass();
        Class<?> cb = b.getClass();
        if(ca != cb)
            return false;
        if(ca == TApply.class) 
            return equals((TApply)a, (TApply)b);
        else if(ca == TFun.class) 
            return subsumes((TFun)a, (TFun)b);
        else if(ca == TForAll.class) {
            TForAll aForAll = (TForAll)a;
            TForAll bForAll = (TForAll)b;
            TVar newVar = var(aForAll.var.getKind());
            return subsumes(aForAll.type.replace(aForAll.var, newVar),
                            bForAll.type.replace(bForAll.var, newVar));
        }
        else if(ca == TPred.class) 
            return equals((TPred)a, (TPred)b);
        else if(ca == TUnion.class) 
            return equals((TUnion)a, (TUnion)b);        
        else // ca == TCon.class 
            // || (ca == TMetaVar.class && a.ref == null && b.ref == null) 
            // || ca = TVar.class 
            return false; // Equals only if a == b, that was already tested
    }

    public static TForAll forAll(TVar parameter, Type type) {
        return new TForAll(parameter, type);
    }

    public static Type forAll(TVar[] parameters, Type type) {
        for(int i=parameters.length-1;i>=0;--i)
            type = forAll(parameters[i], type);
        return type;
    }

    public static ArrayList<TVar> freeVars(Type type) {
        ArrayList<TVar> vars = new ArrayList<TVar>(2);
        type.collectFreeVars(vars);
        return vars;
    }

    public static ArrayList<TVar> freeVars(Type[] types) {
        ArrayList<TVar> vars = new ArrayList<TVar>(2);
        for(Type type : types)
            type.collectFreeVars(vars);
        return vars;
    }

    public static TVar[] freeVarsArray(Type type) {
        ArrayList<TVar> vars = freeVars(type);        
        return vars.toArray(new TVar[vars.size()]);
    }

    public static TVar[] freeVarsArray(Type[] types) {
        ArrayList<TVar> vars = freeVars(types);        
        return vars.toArray(new TVar[vars.size()]);
    }

    public static TPred pred(TCon typeClass, Type ... parameters) {
        return new TPred(typeClass, parameters);
    }

    public static Type function(Type ... types) {
        Type result = types[types.length-1];
        for(int i=types.length-2;i>=0;--i)
            result = function(types[i], result);
        return result;
    }

    public static Type function(Type from, Type to) {
        return new TFun(from, Types.NO_EFFECTS, to);
    }

    public static Type function(Type[] from, Type to) {
        for(int i=from.length-1;i>=0;--i)
            to = function(from[i], to);
        return to;
    }

    public static TFun functionE(Type from, Type effect, Type to) {
        return new TFun(from, effect, to);
    }

    public static Type functionE(Type[] from, Type effect, Type to) {
        for(int i=from.length-1;i>=0;--i) {
            to = functionE(from[i], effect, to);
            effect = Types.NO_EFFECTS;
        }
        return to;
    }

    public static Type removeForAll(Type type, ArrayList<TVar> vars) {
        while(true) {
            if(type instanceof TForAll) {
                TForAll forAll = (TForAll)type;
                type = forAll.type;
                vars.add(forAll.var);
            }
            else if(type instanceof TMetaVar) {
                TMetaVar var = (TMetaVar)type;
                if(var.ref != null)
                    type = var.ref;
                else
                    return type;
            }
            else
                return type;
        }
    }
    
    public static Type removeForAll(Type type) {
        while(true) {
            if(type instanceof TForAll) {
                TForAll forAll = (TForAll)type;
                type = forAll.type;
            }
            else if(type instanceof TMetaVar) {
                TMetaVar var = (TMetaVar)type;
                if(var.ref != null)
                    type = var.ref;
                else
                    return type;
            }
            else
                return type;
        }
    }

    public static Type instantiate(TForAll forAll, ArrayList<TMetaVar> vars) {
        TMetaVar metaVar = metaVar(forAll.var.getKind());
        vars.add(metaVar);
        return instantiate(forAll.type.replace(forAll.var, metaVar), vars);
    }

    public static Type instantiate(Type type, ArrayList<TMetaVar> vars) {
        if(type == null)
            throw new NullPointerException();
        type = canonical(type);
        if(type instanceof TForAll)
            return instantiate((TForAll)type, vars);
        else
            return type;
    }

    public static Type list(Type parameter) {
        return apply(LIST, parameter);
    }
    
    public static Type vector(Type parameter) {
        return apply(VECTOR, parameter);
    }
    
    public static Type mvector(Type parameter) {
        return apply(MVECTOR, parameter);
    }

    public static MultiFunction matchFunction(Type type, int arity) throws MatchException {
    	if (type instanceof TForAll)
    		return matchFunction(((TForAll)type).type, arity);
    	
        type = canonical(type);
        /*while(type instanceof TForAll)
            type = canonical(((TForAll)type).type);*/
        Type[] parameterTypes = new Type[arity];
        Type effect = Types.NO_EFFECTS;
        for(int i=0;i<arity;++i) {
            if(type instanceof TFun) {
                TFun fun = (TFun)type;            
                parameterTypes[i] = fun.domain;
                type = canonical(fun.range);
                if(i == arity-1)
                    effect = fun.effect;
                else if(Types.canonical(fun.effect) != Types.NO_EFFECTS)
                    throw new MatchException();
            }
            /*else if(type instanceof TMetaVar) {
                TMetaVar metaVar = (TMetaVar)type;
                type = Types.metaVar(Kinds.STAR);
                Type template = type;
                effect = Types.metaVar(Kinds.EFFECT);
                for(int j=arity-1;j>=i;--j) {
                    Type pType = Types.metaVar(Kinds.STAR);
                    parameterTypes[j] = pType;
                    template = Types.functionE(pType, 
                            j==arity-1 ? effect : Types.NO_EFFECTS,
                                    template);
                }
                try {
                    metaVar.setRef(template);
                } catch (UnificationException e) {
                    // Should never happen
                    throw new MatchException();                    
                }
                break;
            }*/
            /*else if(type instanceof TApply) {
                TApply apply1 = (TApply)type;
                Type function1 = canonical(apply1.function);
                if(function1 instanceof TApply) {
                    TApply apply2 = (TApply)function1;
                    Type function2 = canonical(apply2.function);
                    if(function2 == ARROW) {
                        result[i] = apply2.parameter;
                        type = canonical(apply1.parameter);
                    }
                    else
                        throw new MatchException();
                }
                else
                    throw new MatchException();
            }*/
            else
                throw new MatchException();
        }
        return new MultiFunction(parameterTypes, effect, type);
    }

    public static boolean isApply(Type func, int arity, Type type) {        
        while(arity-- > 0) {
            type = canonical(type);
            if(!(type instanceof TApply))
                return false;
            type = ((TApply)type).function;
        }
        return equals(func, type);
    }

    public static Type matchApply(TCon func, Type type) throws MatchException {
        type = canonical(type);
        if(type instanceof TApply) {
            TApply apply = (TApply)type;
            Type f = canonical(apply.function);
            if(f.equals(func))
                return canonical(apply.parameter);
        }
        throw new MatchException();
    }
    
    public static MultiApply matchApply(Type type) {
        ArrayList<Type> parameters = new ArrayList<Type>();
        type = canonical(type);
        while(type instanceof TApply) {
            TApply apply = (TApply)type;
            parameters.add(Types.canonical(apply.parameter));
            type = canonical(apply.function);
        }
        Type[] parametersArray;
        if(parameters.isEmpty())
            parametersArray = Type.EMPTY_ARRAY;
        else {
            parametersArray = new Type[parameters.size()];
            for(int i=0,j=parametersArray.length-1;i<parametersArray.length;++i,--j)
                parametersArray[i] = parameters.get(j);
        }
        return new MultiApply(type, parametersArray);
    }
    
    public static Type unifyApply(TCon func, Type type) throws MatchException {
        type = canonical(type);
        if(type instanceof TApply) {
            TApply apply = (TApply)type;
            Type f = canonical(apply.function);
            if(f.equals(func))
                return canonical(apply.parameter);
            else if(f instanceof TMetaVar)
                try {
                    ((TMetaVar)f).setRef(func);
                    return canonical(apply.parameter);
                } catch (UnificationException e) {
                    throw new MatchException();
                }
        }
        else if(type instanceof TMetaVar) {
            TMetaVar parameter = Types.metaVar(Kinds.metaVar());
            try {
                ((TMetaVar) type).setRef(apply(func, parameter));
            } catch (UnificationException e) {
                throw new MatchException();
            }
            return parameter;
        }
        throw new MatchException();
    }

    public static MultiFunction matchFunction(Type type) {
        type = canonical(type);
        while(type instanceof TForAll)
            type = canonical(((TForAll)type).type);
        ArrayList<Type> parameterTypes = new ArrayList<Type>();
        Type effect = Types.NO_EFFECTS;
        while(true) {
            if(type instanceof TFun) {
                TFun fun = (TFun)type;
                parameterTypes.add(fun.domain);
                type = canonical(fun.range);
                if(canonical(fun.effect) != Types.NO_EFFECTS) {
                    effect = fun.effect;
                    break;
                }
            }            
            /*else if(type instanceof TApply) {
                TApply apply1 = (TApply)type;
                Type function1 = canonical(apply1.function);
                if(function1 instanceof TApply) {
                    TApply apply2 = (TApply)function1;
                    Type function2 = canonical(apply2.function);
                    if(function2 == ARROW) {
                        types.add(apply2.parameter);
                        type = apply1.parameter;
                    }
                    else {
                        types.add(type);
                        break;
                    }
                }
                else {
                    types.add(type);
                    break;
                }
            }*/
            else {
                break;
            }
        }
        return new MultiFunction(
                parameterTypes.toArray(new Type[parameterTypes.size()]),
                effect,
                type);
    }
    
    /**
     * This function always success, but may return a multi function
     * with arity smaller than given parameter
     */
    public static MultiFunction unifyFunction2(Type type, int arity) {
        type = canonical(type);

        Type[] parameterTypes = new Type[arity];
        Type effect = Types.NO_EFFECTS;
        int i;
        for(i=0;i<arity;++i) {
            if(type instanceof TFun) {
                TFun fun = (TFun)type;
                parameterTypes[i] = fun.getCanonicalDomain();
                type = fun.getCanonicalRange();
                effect = fun.getCanonicalEffect();
                if(effect != Types.NO_EFFECTS) {
                    ++i;
                    break;
                }
            }
            else if(type instanceof TMetaVar) {
                Type domain = metaVar(Kinds.STAR);
                parameterTypes[i] = domain;
                Type range = metaVar(Kinds.STAR);
                effect = metaVar(Kinds.EFFECT);
                try {
                    ((TMetaVar) type).setRef(functionE(domain, effect, range));
                } catch (UnificationException e) {
                    // Should never happen, if we have checked maximum arity before calling this function
                    throw new InternalCompilerError(e);
                }
                type = range;
                ++i;
                break;
            }
            else
                break;
        }
        
        if(i < arity)
            parameterTypes = Arrays.copyOf(parameterTypes, i);
        return new MultiFunction(parameterTypes, effect, type);
    }
    
    public static MultiFunction unifyFunction(Type type, int arity) throws UnificationException {
        Type[] parameterTypes = new Type[arity];
        for(int i=0;i<arity;++i)
            parameterTypes[i] = metaVar(Kinds.STAR);
        Type effect = metaVar(Kinds.EFFECT);
        Type requiredType = metaVar(Kinds.STAR);
        MultiFunction result = new MultiFunction(parameterTypes, effect, requiredType);

        for(int i=arity-1;i>=0;--i) {
            requiredType = functionE(parameterTypes[i], effect, requiredType);
            effect = Types.NO_EFFECTS;
        }
        unify(type, requiredType);
        return result;
    }

    private static Type getRangeIfFunction(Type type) {
        type = canonical(type);

        if(type instanceof TFun) {
            return ((TFun)type).range;
        }
        /*else if(type instanceof TApply) {
            TApply apply1 = (TApply)type;
            Type f = canonical(apply1.function);
            if(f instanceof TApply) {
                if( canonical(((TApply)f).function) == Types.ARROW ) {
                    return apply1.parameter;
                }
                else
                    return null;
            }
            else
                return null;
        }*/
        else
            return null;
    }

    public static int getArity(Type type) {
        int arity = 0;
        while(true) {
            type = getRangeIfFunction(type);
            if(type == null)
                break;
            ++arity;
        }
        return arity;
    }
    
    public static int getMaxArity(Type type) {
        type = Skeletons.canonicalSkeleton(type);
        int arity = 0;
        while(true) {
            if(type instanceof TFun) {
                ++arity;
                type = Skeletons.canonicalSkeleton(((TFun) type).getCanonicalRange());
            }
            else if(type instanceof TMetaVar) {
                return Integer.MAX_VALUE;
            }
            else
                break;
        }
        return arity;
    }

    public static TMetaVar metaVar(Kind kind) {
        return new TMetaVar(kind);
    }

    public static Type constrained(TPred constraint, Type type) {
        return new TFun(constraint, Types.NO_EFFECTS, type);
    }

    public static Type constrained(TPred[] constraints, Type type) {
        for(int i=constraints.length-1;i>=0;--i)
            type = constrained(constraints[i], type);
        return type;
    }

    public static TMultiApply toMultiApply(Type type) {
        ArrayList<Type> parameters = new ArrayList<Type>();
        type = canonical(type);
        while(type instanceof TApply) {
            TApply apply = (TApply)type;
            parameters.add(apply.parameter);
            type = canonical(apply.function);
        }
        Collections.reverse(parameters);
        return new TMultiApply(type, parameters);
    }

    public static Type tuple(Type ... parameters) {
        if(parameters.length == 1)
            return parameters[0];
        else
            return apply(tupleConstructor(parameters.length), parameters);
    }

    public static TCon tupleConstructor(int arity) {
        if(arity < 0 || arity == 1)
            throw new IllegalArgumentException("The arity of a tuple cannot be " + arity + ".");

        TCon[] oldTupleCache = tupleCache;
        if(oldTupleCache.length <= arity) {         
            int oldLength = oldTupleCache.length;
            int newLength = oldLength*2;
            while(newLength <= arity)
                newLength *= 2;
            TCon[] newTupleCache = Arrays.copyOf(oldTupleCache, newLength);
            for(int i=oldLength;i<newLength;++i) {
                StringBuilder b = new StringBuilder();
                b.append('(');
                for(int j=1;j<i;++j)
                    b.append(',');
                b.append(')');
                newTupleCache[i] = con(BUILTIN, b.toString());
            }
            TCon result = newTupleCache[arity];
            tupleCache = newTupleCache;
            return result;
        }
        else
            return oldTupleCache[arity];
    }

    public static void unify(TFun a, TFun b) throws UnificationException {
        unify(a.domain, b.domain);
        unify(a.effect, b.effect);
        unify(a.range, b.range);
    }

    public static void unify(TApply a, TApply b) throws UnificationException {
        unify(a.function, b.function);
        unify(a.parameter, b.parameter);
    }

    public static void unify(TForAll a, TForAll b) throws UnificationException {
        try {
            Kinds.unify(a.var.getKind(), b.var.getKind());
        } catch (KindUnificationException e) {
            throw new UnificationException(a, b);
        }
        TVar newVar = var(a.var.getKind());
        unify(a.type.replace(a.var, newVar), b.type.replace(b.var, newVar));
    }

    public static void unify(TPred a, TPred b) throws UnificationException {
        if(a.typeClass != b.typeClass
                || a.parameters.length != b.parameters.length)
            throw new UnificationException(a, b);
        for(int i=0;i<a.parameters.length;++i)
            unify(a.parameters[i], b.parameters[i]);
    }

    public static void unify(TUnion a, TUnion b) throws UnificationException {
        if(a.effects.length != b.effects.length)
            throw new UnificationException(a, b);
        for(int i=0;i<a.effects.length;++i)
            unify(a.effects[i], b.effects[i]);        
    }

    public static void unify(Type a, Type b) throws UnificationException {
        a = canonical(a);
        b = canonical(b);
        if(a == b)
            return;
        if(a instanceof TMetaVar) {
            ((TMetaVar)a).setRef(b);
            return;
        }
        if(b instanceof TMetaVar) {
            ((TMetaVar)b).setRef(a);
            return;
        }
        else
            b = canonical(b);
        Class<?> ca = a.getClass();
        Class<?> cb = b.getClass();
        if(ca != cb) {
            throw new UnificationException(a, b);
        }
        if(ca == TApply.class) 
            unify((TApply)a, (TApply)b);
        else if(ca == TFun.class) 
            unify((TFun)a, (TFun)b);
        else if(ca == TForAll.class)
            unify((TForAll)a, (TForAll)b);
        else if(ca == TPred.class) 
            unify((TPred)a, (TPred)b);
        else if(ca == TUnion.class) 
            unify((TUnion)a, (TUnion)b);
        else // ca == TCon.class || ca = TVar.class 
            throw new UnificationException(a, b);
    }

    public static TVar var(Kind kind) {
        return new TVar(kind);
    }

    public static TVar[] vars(TVar[] otherVars) {
        TVar[] vars = new TVar[otherVars.length];
        for(int i=0;i<otherVars.length;++i)
            vars[i] = var(otherVars[i].getKind());
        return vars;
    }

    public static Type instantiate(Type type, Type ... parameters) {
        for(int i=0;i<parameters.length;++i) {
            type = canonical(type);
            if(!(type instanceof TForAll))
                throw new IllegalArgumentException();
            TForAll forAll = (TForAll)type;
            type = forAll.type.replace(forAll.var, parameters[i]);
        }
        return type;
    }

    public static Type[] getTypes(Typed[] values) {
        Type[] types = new Type[values.length];
        for(int i=0;i<values.length;++i)
            types[i] = values[i].getType();
        return types;                
    }

    /**
     * Matches b to a, i.e. finds a substitution such that a[substitution] = b.
     * Unbound metavariables in b are consired as normal variables. It is assumed
     * that a does not contain metavariables and b does not contain any type variables
     * in a (no occurs checks needed).
     * @param a pattern
     * @param b instance
     * @param substitution
     * @return
     */
    public static boolean match(Type a, Type b, THashMap<TVar, Type> substitution) {
        b = canonical(b);

        Class<?> ca = a.getClass();
        if(ca == TVar.class) {
            TVar ta = (TVar)a;
            Type t = substitution.get(ta);
            if(t == null) {
                substitution.put(ta, b); // no occurs check needed
                return true;
            }
            else
                return match(t, b, substitution);                
        }        
        if(a == b)
            return true;        
        Class<?> cb = b.getClass();
        if(ca != cb || ca == TCon.class)
            return false;
        if(ca == TApply.class) 
            return match((TApply)a, (TApply)b, substitution);        
        else if(ca == TFun.class) 
            return match((TFun)a, (TFun)b, substitution);
        else if(ca == TPred.class) 
            return match((TPred)a, (TPred)b, substitution);
        else {
            throw new UnsupportedOperationException("match(" + a + ", " + b +") not supported"); // TForAll not supported
        }
    }

    public static boolean match(TApply a, TApply b, THashMap<TVar, Type> substitution) {
        return match(a.function, b.function, substitution) && match(a.parameter, b.parameter, substitution);
    }

    public static boolean match(TPred a, TPred b, THashMap<TVar, Type> substitution) {
        if(a.typeClass != b.typeClass || a.parameters.length != b.parameters.length)
            return false;
        for(int i=0;i<a.parameters.length;++i)
            if(!match(a.parameters[i], b.parameters[i], substitution))
                return false;
        return true;
    }

    public static boolean match(TFun a, TFun b, THashMap<TVar, Type> substitution) {
        return match(a.domain, b.domain, substitution) 
                && match(a.effect, b.effect, substitution)
                && match(a.range, b.range, substitution);
    }

    public static Type removePred(Type type,
            ArrayList<TPred> preds) {
        while(type instanceof TFun) {
            TFun pred = (TFun)type;
            if(!(pred.domain instanceof TPred))
                break;
            preds.add((TPred)pred.domain);
            type = canonical(pred.range);
        }
        return type;
    }

    public static <T extends Typed> Type[] getTypes(List<T> vars) {
        Type[] result = new Type[vars.size()];
        for(int i=0;i<result.length;++i)
            result[i] = vars.get(i).getType();
        return result;
    }

    public static boolean isBoxed(Type type) {
        while(true) {
            if(type instanceof TVar)
                return true;
            else if(type instanceof TApply) {
                TApply apply = (TApply)type;
                Type function = Types.canonical(apply.function);
                if(function == Types.MAYBE || function == Types.MVECTOR || function == Types.VECTOR) 
                    // FIXME Special case handled now here.
                    // The same problem is possibly with other types also!!!
                    type = apply.parameter;
                else
                    type = function;
            }
            else if(type instanceof TMetaVar) {
                type = ((TMetaVar)type).ref;
                if(type == null)
                    return true;
            }
            else if(type instanceof TForAll) {
                type = ((TForAll)type).type;
            }
            else
                return false;
        }
    }

    public static boolean isFunction(Type type) {
        type = canonical(type);
        return type instanceof TFun;
        /*if(!(type instanceof TApply))
            return false;
        type = canonical(((TApply)type).function);
        if(!(type instanceof TApply))
            return false;
        type = canonical(((TApply)type).function);
        return type == ARROW;*/
    }

    public static boolean equals(Type[] as, Type[] bs) {
        if(as.length != bs.length)
            return false;
        for(int i=0;i<as.length;++i)
            if(!equals(as[i], bs[i]))
                return false;
        return true;
    }

    public static String toString(Type[] types) {
        StringBuilder b = new StringBuilder();
        TypeUnparsingContext tuc = new TypeUnparsingContext();
        b.append('[');
        boolean first = true;
        for(Type type : types) {
            if(first)
                first = false;
            else
                b.append(", ");
            b.append(type.toString(tuc));
        }
        b.append(']');
        return b.toString();
    }

    public static TCon getConstructor(Type type) throws MatchException {
        while(true) {
            if(type instanceof TCon)
                return (TCon)type;
            else if(type instanceof TApply)
                type = ((TApply)type).function;
            else if(type instanceof TMetaVar) {
                Type ref = ((TMetaVar)type).ref;
                if(ref == null)
                    throw new MatchException();
                type = ref;
            }
            else
                throw new MatchException();
        }
    }

    public static Type[] replace(Type[] types, TVar[] from, Type[] to) {
        if(types.length == 0)
            return Type.EMPTY_ARRAY;
        Type[] result = new Type[types.length];
        for(int i=0;i<types.length;++i)
            result[i] = types[i].replace(from, to);
        return result;
    }
    
    public static TPred[] replace(TPred[] types, TVar[] from, Type[] to) {
        if(types.length == 0)
            return TPred.EMPTY_ARRAY;
        TPred[] result = new TPred[types.length];
        for(int i=0;i<types.length;++i)
            result[i] = (TPred)types[i].replace(from, to);
        return result;
    }
    
    public static <T extends Type> Type[] replace(Type[] types, THashMap<TVar, T> map) {
        if(types.length == 0)
            return Type.EMPTY_ARRAY;
        Type[] result = new Type[types.length];
        for(int i=0;i<types.length;++i)
            result[i] = types[i].replace(map);
        return result;
    }

    public static Type union(Type ... effects) {
        if(effects.length == 0)
            return NO_EFFECTS;
        else if(effects.length == 1)
            return effects[0];
        else
            return new TUnion(effects);
    }
    
    public static Type union(Type effect1, Type effect2) {
        return new TUnion(effect1, effect2);
    }
    
    public static Type union(Type effect1, Type effect2, Type effect3) {
        return new TUnion(effect1, effect2, effect3);
    }

    public static Type union(List<Type> effects) {
        if(effects.size() == 0)
            return NO_EFFECTS;
        else if(effects.size() == 1)
            return effects.get(0);
        else
            return new TUnion(effects.toArray(new Type[effects.size()]));
    }

    public static void canonize(Type[] types) {
        for(int i=0;i<types.length;++i)
            types[i] = canonical(types[i]);
    }
    
    public static Type simplifyFinalEffect(Type effect) {
        effect = canonical(effect);
        if(effect instanceof TMetaVar) {
            try {
                //((TMetaVar) effect).setRef(Types.NO_EFFECTS);
                Type t = Types.var(Kinds.EFFECT);
                ((TMetaVar) effect).setRef(t);
                return t;
            } catch (UnificationException e) {
                // Should not happen.
                throw new RuntimeException(e);
            }
        }
        if(effect instanceof TUnion) {
            TUnion union = (TUnion)effect;
            if(union.effects.length == 0)
                return Types.NO_EFFECTS;
            ArrayList<Type> effects = new ArrayList<Type>(union.effects.length);
            for(Type c : union.effects) {
                c = simplifyFinalEffect(c);
                if(c instanceof TUnion)
                    for(Type c2 : ((TUnion)c).effects)
                        effects.add(c2);
                else
                    effects.add(c);
            }
            return union(effects);
        }
        return effect;
    }
    
    public static Type simplifyType(Type effect) {
        effect = canonical(effect);
        if(effect instanceof TUnion) {
            TUnion union = (TUnion)effect;
            if(union.effects.length == 0)
                return Types.NO_EFFECTS;
            THashSet<Type> effects = new THashSet<Type>(union.effects.length);
            for(Type c : union.effects) {
                c = simplifyFinalEffect(c);
                if(c instanceof TUnion)
                    for(Type c2 : ((TUnion)c).effects)
                        effects.add(c2);
                else
                    effects.add(c);
            }
            return union(effects.toArray(new Type[effects.size()]));
        }
        return effect;
    }

    /**
     * Use {@link Environments#getType(org.simantics.scl.compiler.environment.Environment, String)} instead.
     */
    @Deprecated
    public static Type parseType(ITypeEnvironment environment, String text) throws SCLTypeParseException {
        return parseType(new TypeElaborationContext(environment), text);
    }

    /**
     * This method uses DUMMY_TYPE_ENVIRONMENT that almost does anything useful. Use
     * {@link Environments#getType(org.simantics.scl.compiler.environment.Environment, String)} instead.
     */
    @Deprecated
    public static Type parseType(String text) throws SCLTypeParseException {
        return parseType(new TypeElaborationContext(DUMMY_TYPE_ENVIRONMENT), text);
    }

    /**
     * Use {@link Environments#getType(org.simantics.scl.compiler.environment.Environment, String)} instead.
     */
    @Deprecated
    private static Type parseType(TypeElaborationContext context, String text) throws SCLTypeParseException {
        SCLParserImpl parser = new SCLParserImpl(new StringReader(text));
        try {
            org.simantics.scl.compiler.internal.parsing.types.TypeAst ast = 
                    (org.simantics.scl.compiler.internal.parsing.types.TypeAst)parser.parseType();
            return ast.toType(context);
        } catch (SCLSyntaxErrorException e) {
            throw new SCLTypeParseException(new Problem(
                    Locations.beginOf(e.location),
                    Locations.endOf(e.location),
                    e.getMessage()));
        }
    }

    public static Type instantiateAndStrip(Type type) {
        while(true) {
            if(type instanceof TForAll) {
                TForAll forAll = (TForAll)type;
                type = forAll.type.replace(forAll.var, metaVar(forAll.var.getKind()));
            }
            else if(type instanceof TFun) {
                TFun fun = (TFun)type;
                if(fun.domain instanceof TPred || fun.domain == Types.PUNIT)
                    type = fun.range;
                else
                    return type;
            }
            else if(type instanceof TMetaVar) {
                TMetaVar metaVar = (TMetaVar)type;
                if(metaVar.ref == null)
                    return type;
                else
                    type = metaVar.ref;
            }
            else
                return type;
        }
    }
    
}