/*

 * Copyright (c) 1999, 2012, Oracle and/or its affiliates. All rights reserved.

 * DO NOT ALTER OR REMOVE COPYRIGHT NOTICES OR THIS FILE HEADER.

 *

 * This code is free software; you can redistribute it and/or modify it

 * under the terms of the GNU General Public License version 2 only, as

 * published by the Free Software Foundation.  Oracle designates this

 * particular file as subject to the "Classpath" exception as provided

 * by Oracle in the LICENSE file that accompanied this code.

 *

 * This code is distributed in the hope that it will be useful, but WITHOUT

 * ANY WARRANTY; without even the implied warranty of MERCHANTABILITY or

 * FITNESS FOR A PARTICULAR PURPOSE.  See the GNU General Public License

 * version 2 for more details (a copy is included in the LICENSE file that

 * accompanied this code).

 *

 * You should have received a copy of the GNU General Public License version

 * 2 along with this work; if not, write to the Free Software Foundation,

 * Inc., 51 Franklin St, Fifth Floor, Boston, MA 02110-1301 USA.

 *

 * Please contact Oracle, 500 Oracle Parkway, Redwood Shores, CA 94065 USA

 * or visit www.oracle.com if you need additional information or have any

 * questions.

 */

package com.sun.tools.javac.comp;

import com.sun.tools.javac.code.*;

import com.sun.tools.javac.code.Symbol.*;

import com.sun.tools.javac.code.Type.*;

import com.sun.tools.javac.code.Type.UndetVar.InferenceBound;

import com.sun.tools.javac.comp.Resolve.InapplicableMethodException;

import com.sun.tools.javac.comp.Resolve.VerboseResolutionMode;

import com.sun.tools.javac.tree.JCTree;

import com.sun.tools.javac.tree.JCTree.JCTypeCast;

import com.sun.tools.javac.tree.TreeInfo;

import com.sun.tools.javac.util.*;

import com.sun.tools.javac.util.List;

import com.sun.tools.javac.util.JCDiagnostic.DiagnosticPosition;

import java.util.HashMap;

import java.util.Map;

import java.util.Set;

import static com.sun.tools.javac.code.TypeTags.*;

/** Helper class for type parameter inference, used by the attribution phase.

 *

 *  <p><b>This is NOT part of any supported API.

 *  If you write code that depends on this, you do so at your own risk.

 *  This code and its internal interfaces are subject to change or

 *  deletion without notice.</b>

 */

public class Infer {

    protected static final Context.Key<Infer> inferKey =

        new Context.Key<Infer>();

    /** A value for prototypes that admit any type, including polymorphic ones. */

    public static final Type anyPoly = new Type(NONE, null);

    Symtab syms;

    Types types;

    Check chk;

    Resolve rs;

    Log log;

    JCDiagnostic.Factory diags;

    public static Infer instance(Context context) {

        Infer instance = context.get(inferKey);

        if (instance == null)

            instance = new Infer(context);

        return instance;

    }

    protected Infer(Context context) {

        context.put(inferKey, this);

        syms = Symtab.instance(context);

        types = Types.instance(context);

        rs = Resolve.instance(context);

        log = Log.instance(context);

        chk = Check.instance(context);

        diags = JCDiagnostic.Factory.instance(context);

        inferenceException = new InferenceException(diags);

    }

   /**

    * This exception class is design to store a list of diagnostics corresponding

    * to inference errors that can arise during a method applicability check.

    */

    public static class InferenceException extends InapplicableMethodException {

        private static final long serialVersionUID = 0;

        List<JCDiagnostic> messages = List.nil();

        InferenceException(JCDiagnostic.Factory diags) {

            super(diags);

        }

        @Override

        InapplicableMethodException setMessage(JCDiagnostic diag) {

            messages = messages.append(diag);

            return this;

        }

        @Override

        public JCDiagnostic getDiagnostic() {

            return messages.head;

        }

        void clear() {

            messages = List.nil();

        }

    }

    private final InferenceException inferenceException;

/***************************************************************************

 * Mini/Maximization of UndetVars

 ***************************************************************************/

    /** Instantiate undetermined type variable to its minimal upper bound.

     *  Throw a NoInstanceException if this not possible.

     */

   void maximizeInst(UndetVar that, Warner warn) throws InferenceException {

        List<Type> hibounds = Type.filter(that.getBounds(InferenceBound.UPPER), boundFilter);

        if (that.getBounds(InferenceBound.EQ).isEmpty()) {

            if (hibounds.isEmpty())

                that.inst = syms.objectType;

            else if (hibounds.tail.isEmpty())

                that.inst = hibounds.head;

            else

                that.inst = types.glb(hibounds);

        } else {

            that.inst = that.getBounds(InferenceBound.EQ).head;

        }

        if (that.inst == null ||

            that.inst.isErroneous())

            throw inferenceException

                .setMessage("no.unique.maximal.instance.exists",

                            that.qtype, hibounds);

    }

    private Filter<Type> boundFilter = new Filter<Type>() {

        @Override

        public boolean accepts(Type t) {

            return !t.isErroneous() && t.tag != BOT;

        }

    };

    /** Instantiate undetermined type variable to the lub of all its lower bounds.

     *  Throw a NoInstanceException if this not possible.

     */

    void minimizeInst(UndetVar that, Warner warn) throws InferenceException {

        List<Type> lobounds = Type.filter(that.getBounds(InferenceBound.LOWER), boundFilter);

        if (that.getBounds(InferenceBound.EQ).isEmpty()) {

            if (lobounds.isEmpty()) {

                //do nothing - the inference variable is under-constrained

                return;

            } else if (lobounds.tail.isEmpty())

                that.inst = lobounds.head.isPrimitive() ? syms.errType : lobounds.head;

            else {

                that.inst = types.lub(lobounds);

            }

            if (that.inst == null || that.inst.tag == ERROR)

                    throw inferenceException

                        .setMessage("no.unique.minimal.instance.exists",

                                    that.qtype, lobounds);

        } else {

            that.inst = that.getBounds(InferenceBound.EQ).head;

        }

    }

/***************************************************************************

 * Exported Methods

 ***************************************************************************/

    /**

     * Instantiate uninferred inference variables (JLS 15.12.2.8). First

     * if the method return type is non-void, we derive constraints from the

     * expected type - then we use declared bound well-formedness to derive additional

     * constraints. If no instantiation exists, or if several incomparable

     * best instantiations exist throw a NoInstanceException.

     */

    public void instantiateUninferred(DiagnosticPosition pos,

            InferenceContext inferenceContext,

            MethodType mtype,

            Attr.ResultInfo resultInfo,

            Warner warn) throws InferenceException {

        Type to = resultInfo.pt;

            to = mtype.getReturnType().tag <= VOID ?

                    mtype.getReturnType() : syms.objectType;

        }

        Type qtype1 = inferenceContext.asFree(mtype.getReturnType(), types);

        if (!types.isSubtype(qtype1,

                qtype1.tag == UNDETVAR ? types.boxedTypeOrType(to) : to)) {

            throw inferenceException

                    .setMessage("infer.no.conforming.instance.exists",

                    inferenceContext.restvars(), mtype.getReturnType(), to);

        }

        while (true) {

            boolean stuck = true;

            for (Type t : inferenceContext.undetvars) {

                UndetVar uv = (UndetVar)t;

                if (uv.inst == null && (uv.getBounds(InferenceBound.EQ).nonEmpty() ||

                        !inferenceContext.free(uv.getBounds(InferenceBound.UPPER)))) {

                    maximizeInst((UndetVar)t, warn);

                    stuck = false;

                }

            }

            if (inferenceContext.restvars().isEmpty()) {

                //all variables have been instantiated - exit

                break;

            } else if (stuck) {

                //some variables could not be instantiated because of cycles in

                //upper bounds - provide a (possibly recursive) default instantiation

                instantiateAsUninferredVars(inferenceContext);

                break;

            } else {

                //some variables have been instantiated - replace newly instantiated

                //variables in remaining upper bounds and continue

                for (Type t : inferenceContext.undetvars) {

                    UndetVar uv = (UndetVar)t;

                    uv.substBounds(inferenceContext.inferenceVars(), inferenceContext.instTypes(), types);

                }

            }

        }

    }

    /**

     * Infer cyclic inference variables as described in 15.12.2.8.

     */

    private void instantiateAsUninferredVars(InferenceContext inferenceContext) {

        ListBuffer<Type> todo = ListBuffer.lb();

        //step 1 - create fresh tvars

        for (Type t : inferenceContext.undetvars) {

            UndetVar uv = (UndetVar)t;

            if (uv.inst == null) {

                TypeSymbol fresh_tvar = new TypeSymbol(Flags.SYNTHETIC, uv.qtype.tsym.name, null, uv.qtype.tsym.owner);

                fresh_tvar.type = new TypeVar(fresh_tvar, types.makeCompoundType(uv.getBounds(InferenceBound.UPPER)), null);

                todo.append(uv);

                uv.inst = fresh_tvar.type;

            }

        }

        //step 2 - replace fresh tvars in their bounds

        List<Type> formals = inferenceContext.inferenceVars();

        for (Type t : todo) {

            UndetVar uv = (UndetVar)t;

            TypeVar ct = (TypeVar)uv.inst;

            ct.bound = types.glb(inferenceContext.asInstTypes(types.getBounds(ct), types));

            if (ct.bound.isErroneous()) {

                //report inference error if glb fails

                reportBoundError(uv, BoundErrorKind.BAD_UPPER);

            }

            formals = formals.tail;

        }

    }

    /** Instantiate a generic method type by finding instantiations for all its

     * inference variables so that it can be applied to a given argument type list.

     */

    public Type instantiateMethod(Env<AttrContext> env,

                                  List<Type> tvars,

                                  MethodType mt,

                                  Attr.ResultInfo resultInfo,

                                  Symbol msym,

                                  List<Type> argtypes,

                                  boolean allowBoxing,

                                  boolean useVarargs,

                                  Warner warn) throws InferenceException {

        //-System.err.println("instantiateMethod(" + tvars + ", " + mt + ", " + argtypes + ")"); //DEBUG

        final InferenceContext inferenceContext = new InferenceContext(tvars, this);

        inferenceException.clear();

        try {

            // minimize as yet undetermined type variables

            for (Type t : inferenceContext.undetvars) {

                minimizeInst((UndetVar)t, warn);

            }

            checkWithinBounds(inferenceContext, warn);

            mt = (MethodType)inferenceContext.asInstType(mt, types);

            List<Type> restvars = inferenceContext.restvars();

            if (!restvars.isEmpty()) {

                if (resultInfo != null && !warn.hasNonSilentLint(Lint.LintCategory.UNCHECKED)) {

                    instantiateUninferred(env.tree.pos(), inferenceContext, mt, resultInfo, warn);

                    checkWithinBounds(inferenceContext, warn);

                    mt = (MethodType)inferenceContext.asInstType(mt, types);

                    if (rs.verboseResolutionMode.contains(VerboseResolutionMode.DEFERRED_INST)) {

                        log.note(env.tree.pos, "deferred.method.inst", msym, mt, resultInfo.pt);

                    }

                }

            }

            // return instantiated version of method type

            return mt;

        } finally {

            inferenceContext.notifyChange(types);

        }

    }

    //where

        /** inference check handler **/

        class InferenceCheckHandler implements Resolve.MethodCheckHandler {

            InferenceContext inferenceContext;

            public InferenceCheckHandler(InferenceContext inferenceContext) {

                this.inferenceContext = inferenceContext;

            }

            public InapplicableMethodException arityMismatch() {

                return inferenceException.setMessage("infer.arg.length.mismatch", inferenceContext.inferenceVars());

            }

            public InapplicableMethodException argumentMismatch(boolean varargs, JCDiagnostic details) {

                String key = varargs ?

                        "infer.varargs.argument.mismatch" :

                        "infer.no.conforming.assignment.exists";

                return inferenceException.setMessage(key,

                        inferenceContext.inferenceVars(), details);

            }

            public InapplicableMethodException inaccessibleVarargs(Symbol location, Type expected) {

                return inferenceException.setMessage("inaccessible.varargs.type",

                        expected, Kinds.kindName(location), location);

            }

        }

    /** check that type parameters are within their bounds.

     */

    void checkWithinBounds(InferenceContext inferenceContext,

                           Warner warn) throws InferenceException {

        //step 1 - check compatibility of instantiated type w.r.t. initial bounds

        for (Type t : inferenceContext.undetvars) {

            UndetVar uv = (UndetVar)t;

            uv.substBounds(inferenceContext.inferenceVars(), inferenceContext.instTypes(), types);

            checkCompatibleUpperBounds(uv, inferenceContext.inferenceVars());

            if (!inferenceContext.restvars().contains(uv.qtype)) {

                Type inst = inferenceContext.asInstType(t, types);

                for (Type u : uv.getBounds(InferenceBound.UPPER)) {

                    if (!types.isSubtypeUnchecked(inst, inferenceContext.asFree(u, types), warn)) {

                        reportBoundError(uv, BoundErrorKind.UPPER);

                    }

                }

                for (Type l : uv.getBounds(InferenceBound.LOWER)) {

                    Assert.check(!inferenceContext.free(l));

                    if (!types.isSubtypeUnchecked(l, inst, warn)) {

                        reportBoundError(uv, BoundErrorKind.LOWER);

                    }

                }

                for (Type e : uv.getBounds(InferenceBound.EQ)) {

                    Assert.check(!inferenceContext.free(e));

                    if (!types.isSameType(inst, e)) {

                        reportBoundError(uv, BoundErrorKind.EQ);

                    }

                }

            }

        }

        //step 2 - check that eq bounds are consistent w.r.t. eq/lower bounds

        for (Type t : inferenceContext.undetvars) {

            UndetVar uv = (UndetVar)t;

            //check eq bounds consistency

            Type eq = null;

            for (Type e : uv.getBounds(InferenceBound.EQ)) {

                Assert.check(!inferenceContext.free(e));

                if (eq != null && !types.isSameType(e, eq)) {

                    reportBoundError(uv, BoundErrorKind.EQ);

                }

                eq = e;

                for (Type l : uv.getBounds(InferenceBound.LOWER)) {

                    Assert.check(!inferenceContext.free(l));

                    if (!types.isSubtypeUnchecked(l, e, warn)) {

                        reportBoundError(uv, BoundErrorKind.BAD_EQ_LOWER);

                    }

                }

                for (Type u : uv.getBounds(InferenceBound.UPPER)) {

                    if (inferenceContext.free(u)) continue;

                    if (!types.isSubtypeUnchecked(e, u, warn)) {

                        reportBoundError(uv, BoundErrorKind.BAD_EQ_UPPER);

                    }

                }

            }

        }

    }

    void checkCompatibleUpperBounds(UndetVar uv, List<Type> tvars) {

        // VGJ: sort of inlined maximizeInst() below.  Adding

        // bounds can cause lobounds that are above hibounds.

        ListBuffer<Type> hiboundsNoVars = ListBuffer.lb();

        for (Type t : Type.filter(uv.getBounds(InferenceBound.UPPER), boundFilter)) {

            if (!t.containsAny(tvars)) {

                hiboundsNoVars.append(t);

            }

        }

        List<Type> hibounds = hiboundsNoVars.toList();

        Type hb = null;

        if (hibounds.isEmpty())

            hb = syms.objectType;

        else if (hibounds.tail.isEmpty())

            hb = hibounds.head;

        else

            hb = types.glb(hibounds);

        if (hb == null || hb.isErroneous())

            reportBoundError(uv, BoundErrorKind.BAD_UPPER);

    }

    enum BoundErrorKind {

        BAD_UPPER() {

            @Override

            InapplicableMethodException setMessage(InferenceException ex, UndetVar uv) {

                return ex.setMessage("incompatible.upper.bounds", uv.qtype,

                        uv.getBounds(InferenceBound.UPPER));

            }

        },

        BAD_EQ_UPPER() {

            @Override

            InapplicableMethodException setMessage(InferenceException ex, UndetVar uv) {

                return ex.setMessage("incompatible.eq.upper.bounds", uv.qtype,

                        uv.getBounds(InferenceBound.EQ), uv.getBounds(InferenceBound.UPPER));

            }

        },

        BAD_EQ_LOWER() {

            @Override

            InapplicableMethodException setMessage(InferenceException ex, UndetVar uv) {

                return ex.setMessage("incompatible.eq.lower.bounds", uv.qtype,

                        uv.getBounds(InferenceBound.EQ), uv.getBounds(InferenceBound.LOWER));

            }

        },

        UPPER() {

            @Override

            InapplicableMethodException setMessage(InferenceException ex, UndetVar uv) {

                return ex.setMessage("inferred.do.not.conform.to.upper.bounds", uv.inst,

                        uv.getBounds(InferenceBound.UPPER));

            }

        },

        LOWER() {

            @Override

            InapplicableMethodException setMessage(InferenceException ex, UndetVar uv) {

                return ex.setMessage("inferred.do.not.conform.to.lower.bounds", uv.inst,

                        uv.getBounds(InferenceBound.LOWER));

            }

        },

        EQ() {

            @Override

            InapplicableMethodException setMessage(InferenceException ex, UndetVar uv) {

                return ex.setMessage("inferred.do.not.conform.to.eq.bounds", uv.inst,

                        uv.getBounds(InferenceBound.EQ));

            }

        };

        abstract InapplicableMethodException setMessage(InferenceException ex, UndetVar uv);

    }

    //where

    void reportBoundError(UndetVar uv, BoundErrorKind bk) {

        throw bk.setMessage(inferenceException, uv);

    }

    /**

     * Compute a synthetic method type corresponding to the requested polymorphic

     * method signature. The target return type is computed from the immediately

     * enclosing scope surrounding the polymorphic-signature call.

     */

    Type instantiatePolymorphicSignatureInstance(Env<AttrContext> env,

                                            MethodSymbol spMethod,  // sig. poly. method or null if none

                                            List<Type> argtypes) {

        final Type restype;

        //The return type for a polymorphic signature call is computed from

        //the enclosing tree E, as follows: if E is a cast, then use the

        //target type of the cast expression as a return type; if E is an

        //expression statement, the return type is 'void' - otherwise the

        //return type is simply 'Object'. A correctness check ensures that

        //env.next refers to the lexically enclosing environment in which

        //the polymorphic signature call environment is nested.