/*

 * Copyright (c) 1999, 2014, 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.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.JCDiagnostic.DiagnosticPosition;

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

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

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

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

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

import com.sun.tools.javac.comp.DeferredAttr.AttrMode;

import com.sun.tools.javac.comp.Infer.GraphSolver.InferenceGraph;

import com.sun.tools.javac.comp.Infer.GraphSolver.InferenceGraph.Node;

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

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

import com.sun.tools.javac.util.GraphUtils.TarjanNode;

import java.util.ArrayList;

import java.util.Collections;

import java.util.EnumMap;

import java.util.EnumSet;

import java.util.HashMap;

import java.util.HashSet;

import java.util.LinkedHashSet;

import java.util.Map;

import java.util.Set;

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

/** 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<>();

    Resolve rs;

    Check chk;

    Symtab syms;

    Types types;

    JCDiagnostic.Factory diags;

    Log log;

    /** should the graph solver be used? */

    boolean allowGraphInference;

    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);

        rs = Resolve.instance(context);

        chk = Check.instance(context);

        syms = Symtab.instance(context);

        types = Types.instance(context);

        diags = JCDiagnostic.Factory.instance(context);

        log = Log.instance(context);

        inferenceException = new InferenceException(diags);

        Options options = Options.instance(context);

        allowGraphInference = Source.instance(context).allowGraphInference()

                && options.isUnset("useLegacyInference");

    }

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

    public static final Type anyPoly = new JCNoType();

   /**

    * 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() {

            //no message to set

            return this;

        }

        @Override

        InapplicableMethodException setMessage(JCDiagnostic diag) {

            messages = messages.append(diag);

            return this;

        }

        @Override

        public JCDiagnostic getDiagnostic() {

            return messages.head;

        }

        void clear() {

            messages = List.nil();

        }

    }

    protected final InferenceException inferenceException;

    // <editor-fold defaultstate="collapsed" desc="Inference routines">

    /**

     * Main inference entry point - instantiate a generic method type

     * using given argument types and (possibly) an expected target-type.

     */

    Type instantiateMethod( Env<AttrContext> env,

                            List<Type> tvars,

                            MethodType mt,

                            Attr.ResultInfo resultInfo,

                            MethodSymbol msym,

                            List<Type> argtypes,

                            boolean allowBoxing,

                            boolean useVarargs,

                            Resolve.MethodResolutionContext resolveContext,

                            Warner warn) throws InferenceException {

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

        final InferenceContext inferenceContext = new InferenceContext(tvars);  //B0

        inferenceException.clear();

        try {

            DeferredAttr.DeferredAttrContext deferredAttrContext =

                        resolveContext.deferredAttrContext(msym, inferenceContext, resultInfo, warn);

            resolveContext.methodCheck.argumentsAcceptable(env, deferredAttrContext,   //B2

                    argtypes, mt.getParameterTypes(), warn);

            if (allowGraphInference &&

                    resultInfo != null &&

                    !warn.hasNonSilentLint(Lint.LintCategory.UNCHECKED)) {

                //inject return constraints earlier

                checkWithinBounds(inferenceContext, warn); //propagation

                Type newRestype = generateReturnConstraints(env.tree, resultInfo,  //B3

                        mt, inferenceContext);

                mt = (MethodType)types.createMethodTypeWithReturn(mt, newRestype);

                //propagate outwards if needed

                if (resultInfo.checkContext.inferenceContext().free(resultInfo.pt)) {

                    //propagate inference context outwards and exit

                    inferenceContext.dupTo(resultInfo.checkContext.inferenceContext());

                    deferredAttrContext.complete();

                    return mt;

                }

            }

            deferredAttrContext.complete();

            // minimize as yet undetermined type variables

            if (allowGraphInference) {

                inferenceContext.solve(warn);

            } else {

                inferenceContext.solveLegacy(true, warn, LegacyInferenceSteps.EQ_LOWER.steps); //minimizeInst

            }

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

            if (!allowGraphInference &&

                    inferenceContext.restvars().nonEmpty() &&

                    resultInfo != null &&

                    !warn.hasNonSilentLint(Lint.LintCategory.UNCHECKED)) {

                generateReturnConstraints(env.tree, resultInfo, mt, inferenceContext);

                inferenceContext.solveLegacy(false, warn, LegacyInferenceSteps.EQ_UPPER.steps); //maximizeInst

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

            }

            if (resultInfo != null && 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 {

            if (resultInfo != null || !allowGraphInference) {

                inferenceContext.notifyChange();

            } else {

                inferenceContext.notifyChange(inferenceContext.boundedVars());

            }

            if (resultInfo == null) {

                /* if the is no result info then we can clear the capture types

                 * cache without affecting any result info check

                 */

                inferenceContext.captureTypeCache.clear();

            }

        }

    }

    /**

     * Generate constraints from the generic method's return type. If the method

     * call occurs in a context where a type T is expected, use the expected

     * type to derive more constraints on the generic method inference variables.

     */

    Type generateReturnConstraints(JCTree tree, Attr.ResultInfo resultInfo,

            MethodType mt, InferenceContext inferenceContext) {

        InferenceContext rsInfoInfContext = resultInfo.checkContext.inferenceContext();

        Type from = mt.getReturnType();

        if (mt.getReturnType().containsAny(inferenceContext.inferencevars) &&

                rsInfoInfContext != emptyContext) {

            from = types.capture(from);

            //add synthetic captured ivars

            for (Type t : from.getTypeArguments()) {

                if (t.hasTag(TYPEVAR) && ((TypeVar)t).isCaptured()) {

                    inferenceContext.addVar((TypeVar)t);

                }

            }

        }

        Type qtype = inferenceContext.asUndetVar(from);

        Type to = resultInfo.pt;

        if (qtype.hasTag(VOID)) {

            to = syms.voidType;

        } else if (to.hasTag(NONE)) {

            to = from.isPrimitive() ? from : syms.objectType;

        } else if (qtype.hasTag(UNDETVAR)) {

            if (resultInfo.pt.isReference()) {

                to = generateReturnConstraintsUndetVarToReference(

                        tree, (UndetVar)qtype, to, resultInfo, inferenceContext);

            } else {

                if (to.isPrimitive()) {

                    to = generateReturnConstraintsPrimitive(tree, (UndetVar)qtype, to,

                        resultInfo, inferenceContext);

                }

            }

        }

        Assert.check(allowGraphInference || !rsInfoInfContext.free(to),

                "legacy inference engine cannot handle constraints on both sides of a subtyping assertion");

        //we need to skip capture?

        Warner retWarn = new Warner();

        if (!resultInfo.checkContext.compatible(qtype, rsInfoInfContext.asUndetVar(to), retWarn) ||

                //unchecked conversion is not allowed in source 7 mode

                (!allowGraphInference && retWarn.hasLint(Lint.LintCategory.UNCHECKED))) {

            throw inferenceException

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

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

        }

        return from;

    }

    private Type generateReturnConstraintsPrimitive(JCTree tree, UndetVar from,

            Type to, Attr.ResultInfo resultInfo, InferenceContext inferenceContext) {

        if (!allowGraphInference) {

            //if legacy, just return boxed type

            return types.boxedClass(to).type;

        }

        //if graph inference we need to skip conflicting boxed bounds...

        for (Type t : from.getBounds(InferenceBound.EQ, InferenceBound.UPPER,

                InferenceBound.LOWER)) {

            Type boundAsPrimitive = types.unboxedType(t);

            if (boundAsPrimitive == null || boundAsPrimitive.hasTag(NONE)) {

                continue;

            }

            return generateReferenceToTargetConstraint(tree, from, to,

                    resultInfo, inferenceContext);

        }

        return types.boxedClass(to).type;

    }

    private Type generateReturnConstraintsUndetVarToReference(JCTree tree,

            UndetVar from, Type to, Attr.ResultInfo resultInfo,

            InferenceContext inferenceContext) {

        Type captureOfTo = types.capture(to);

        /* T is a reference type, but is not a wildcard-parameterized type, and either

         */

        if (captureOfTo == to) { //not a wildcard parameterized type

            /* i) B2 contains a bound of one of the forms alpha = S or S <: alpha,

             *      where S is a wildcard-parameterized type, or

             */

            for (Type t : from.getBounds(InferenceBound.EQ, InferenceBound.LOWER)) {

                Type captureOfBound = types.capture(t);

                if (captureOfBound != t) {

                    return generateReferenceToTargetConstraint(tree, from, to,

                            resultInfo, inferenceContext);

                }

            }

            /* ii) B2 contains two bounds of the forms S1 <: alpha and S2 <: alpha,

             * where S1 and S2 have supertypes that are two different

             * parameterizations of the same generic class or interface.

             */

            for (Type aLowerBound : from.getBounds(InferenceBound.LOWER)) {

                for (Type anotherLowerBound : from.getBounds(InferenceBound.LOWER)) {

                    if (aLowerBound != anotherLowerBound &&

                        commonSuperWithDiffParameterization(aLowerBound, anotherLowerBound)) {

                        /* self comment check if any lower bound may be and undetVar,

                         * in that case the result of this call may be a false positive.

                         * Should this be restricted to non free types?

                         */

                        return generateReferenceToTargetConstraint(tree, from, to,

                            resultInfo, inferenceContext);

                    }

                }

            }

        }

        /* T is a parameterization of a generic class or interface, G,

         * and B2 contains a bound of one of the forms alpha = S or S <: alpha,

         * where there exists no type of the form G<...> that is a

         * supertype of S, but the raw type G is a supertype of S

         */

        if (to.isParameterized()) {

            for (Type t : from.getBounds(InferenceBound.EQ, InferenceBound.LOWER)) {

                Type sup = types.asSuper(t, to.tsym);

                if (sup != null && sup.isRaw()) {

                    return generateReferenceToTargetConstraint(tree, from, to,

                            resultInfo, inferenceContext);

                }

            }

        }

        return to;

    }

    private boolean commonSuperWithDiffParameterization(Type t, Type s) {

    }

    private Type generateReferenceToTargetConstraint(JCTree tree, UndetVar from,

            Type to, Attr.ResultInfo resultInfo,

            InferenceContext inferenceContext) {

        inferenceContext.solve(List.of(from.qtype), new Warner());

        Type capturedType = resultInfo.checkContext.inferenceContext()

                .cachedCapture(tree, from.inst, false);

        if (types.isConvertible(capturedType,

                resultInfo.checkContext.inferenceContext().asUndetVar(to))) {

            //effectively skip additional return-type constraint generation (compatibility)

            return syms.objectType;

        }

        return to;

    }

    /**

      * Infer cyclic inference variables as described in 15.12.2.8.

      */

    private void instantiateAsUninferredVars(List<Type> vars, InferenceContext inferenceContext) {

        ListBuffer<Type> todo = new ListBuffer<>();

        //step 1 - create fresh tvars

        for (Type t : vars) {

            UndetVar uv = (UndetVar)inferenceContext.asUndetVar(t);

            List<Type> upperBounds = uv.getBounds(InferenceBound.UPPER);

            if (Type.containsAny(upperBounds, vars)) {

                TypeSymbol fresh_tvar = new TypeVariableSymbol(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, Type.noAnnotations);

                todo.append(uv);

                uv.inst = fresh_tvar.type;

            } else if (upperBounds.nonEmpty()) {

                uv.inst = types.glb(upperBounds);

            } else {

                uv.inst = syms.objectType;

            }

        }

        //step 2 - replace fresh tvars in their bounds

        List<Type> formals = vars;

        for (Type t : todo) {

            UndetVar uv = (UndetVar)t;

            TypeVar ct = (TypeVar)uv.inst;

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

            if (ct.bound.isErroneous()) {

                //report inference error if glb fails

                reportBoundError(uv, BoundErrorKind.BAD_UPPER);

            }

            formals = formals.tail;

        }

    }

    /**

     * 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

                                            Resolve.MethodResolutionContext resolveContext,

                                            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.

        switch (env.next.tree.getTag()) {

            case TYPECAST:

                JCTypeCast castTree = (JCTypeCast)env.next.tree;

                restype = (TreeInfo.skipParens(castTree.expr) == env.tree) ?

                    castTree.clazz.type :

                    syms.objectType;

                break;

            case EXEC:

                JCTree.JCExpressionStatement execTree =

                        (JCTree.JCExpressionStatement)env.next.tree;

                restype = (TreeInfo.skipParens(execTree.expr) == env.tree) ?

                    syms.voidType :

                    syms.objectType;

                break;

            default:

                restype = syms.objectType;

        }

        List<Type> paramtypes = Type.map(argtypes, new ImplicitArgType(spMethod, resolveContext.step));

        List<Type> exType = spMethod != null ?

            spMethod.getThrownTypes() :

            List.of(syms.throwableType); // make it throw all exceptions

        MethodType mtype = new MethodType(paramtypes,

                                          restype,

                                          exType,

                                          syms.methodClass);

        return mtype;

    }

    //where

        class ImplicitArgType extends DeferredAttr.DeferredTypeMap {

            public ImplicitArgType(Symbol msym, Resolve.MethodResolutionPhase phase) {

                rs.deferredAttr.super(AttrMode.SPECULATIVE, msym, phase);

            }

            public Type apply(Type t) {

                t = types.erasure(super.apply(t));

                if (t.hasTag(BOT))

                    // nulls type as the marker type Null (which has no instances)

                    // infer as java.lang.Void for now

                    t = types.boxedClass(syms.voidType).type;

                return t;

            }

        }

    /**

      * This method is used to infer a suitable target SAM in case the original

      * SAM type contains one or more wildcards. An inference process is applied

      * so that wildcard bounds, as well as explicit lambda/method ref parameters

      * (where applicable) are used to constraint the solution.

      */

    public Type instantiateFunctionalInterface(DiagnosticPosition pos, Type funcInterface,

            List<Type> paramTypes, Check.CheckContext checkContext) {

        if (types.capture(funcInterface) == funcInterface) {

            //if capture doesn't change the type then return the target unchanged

            //(this means the target contains no wildcards!)

            return funcInterface;

        } else {

            Type formalInterface = funcInterface.tsym.type;

            InferenceContext funcInterfaceContext =

                    new InferenceContext(funcInterface.tsym.type.getTypeArguments());

            Assert.check(paramTypes != null);

            //get constraints from explicit params (this is done by

            //checking that explicit param types are equal to the ones

            //in the functional interface descriptors)

            List<Type> descParameterTypes = types.findDescriptorType(formalInterface).getParameterTypes();

            if (descParameterTypes.size() != paramTypes.size()) {

                checkContext.report(pos, diags.fragment("incompatible.arg.types.in.lambda"));