package org.simantics.scl.compiler.compilation;

import static org.simantics.scl.compiler.elaboration.expressions.Expressions.apply;
import static org.simantics.scl.compiler.elaboration.expressions.Expressions.applyTypes;
import static org.simantics.scl.compiler.elaboration.expressions.Expressions.lambda;
import static org.simantics.scl.compiler.elaboration.expressions.Expressions.loc;
import static org.simantics.scl.compiler.elaboration.expressions.Expressions.vars;
import gnu.trove.map.hash.THashMap;
import gnu.trove.map.hash.TObjectIntHashMap;
import gnu.trove.set.hash.THashSet;
import gnu.trove.set.hash.TIntHashSet;

import java.util.ArrayList;

import org.simantics.scl.compiler.elaboration.contexts.TypingContext;
import org.simantics.scl.compiler.elaboration.expressions.EPlaceholder;
import org.simantics.scl.compiler.elaboration.expressions.EVariable;
import org.simantics.scl.compiler.elaboration.expressions.Expression;
import org.simantics.scl.compiler.elaboration.expressions.Variable;
import org.simantics.scl.compiler.elaboration.modules.SCLValue;
import org.simantics.scl.compiler.elaboration.rules.MappingRelation;
import org.simantics.scl.compiler.elaboration.rules.TransformationRule;
import org.simantics.scl.compiler.environment.Environment;
import org.simantics.scl.compiler.errors.ErrorLog;
import org.simantics.scl.compiler.errors.Locations;
import org.simantics.scl.compiler.internal.elaboration.constraints.Constraint;
import org.simantics.scl.compiler.internal.elaboration.constraints.ConstraintEnvironment;
import org.simantics.scl.compiler.internal.elaboration.constraints.ConstraintSolver;
import org.simantics.scl.compiler.internal.elaboration.constraints.ExpressionAugmentation;
import org.simantics.scl.compiler.internal.elaboration.constraints.ReducedConstraints;
import org.simantics.scl.compiler.internal.elaboration.utils.StronglyConnectedComponents;
import org.simantics.scl.compiler.module.ConcreteModule;
import org.simantics.scl.compiler.types.TPred;
import org.simantics.scl.compiler.types.TVar;
import org.simantics.scl.compiler.types.Type;
import org.simantics.scl.compiler.types.Types;
import org.simantics.scl.compiler.types.kinds.Kinds;
import org.simantics.scl.compiler.types.util.Polarity;

public class TypeCheckingOld {
    public static final boolean PRINT_VALUES = false;
    
    ErrorLog errorLog;
    Environment environment;
    ConcreteModule module;
    
    ConstraintEnvironment ce;
    ArrayList<SCLValue[]> valuesWithoutTypeAnnotation = new ArrayList<SCLValue[]>(); 
    ArrayList<SCLValue> valuesWithTypeAnnotation = new ArrayList<SCLValue>();
    
    public TypeCheckingOld(ErrorLog errorLog, Environment environment,
            ConcreteModule module) {
        this.errorLog = errorLog;
        this.environment = environment;
        this.module = module;
    }
    
    public void typeCheck() {
        ce = new ConstraintEnvironment(environment);
        groupValueDefinitionsByDependency();
        typeCheckValuesWithoutTypeAnnotations();
        typeCheckValuesWithTypeAnnotations();
        typeCheckRules();
    }

    private void groupValueDefinitionsByDependency() {
        // Collect all untyped names
        final ArrayList<SCLValue> values = new ArrayList<SCLValue>();
        for(SCLValue value : module.getValues()) {
            if(value.getExpression() != null) {
                if(value.getType() == null)
                    values.add(value);
                else
                    valuesWithTypeAnnotation.add(value);   
            }            
        }
        
        // Create inverse
        final TObjectIntHashMap<Object> allRefs = 
                new TObjectIntHashMap<Object>(values.size()*2, 0.5f, -1);
        for(int i=0;i<values.size();++i)
            allRefs.put(values.get(i), i);
        
        // Create groups       
        new StronglyConnectedComponents(values.size()) {
            
            TIntHashSet set = new TIntHashSet();
            
            @Override
            protected void reportComponent(int[] component) {
                SCLValue[] valueComponent = new SCLValue[component.length];
                for(int i=0;i<component.length;++i)
                    valueComponent[i] = values.get(component[i]);
                valuesWithoutTypeAnnotation.add(valueComponent);
            }
            
            @Override
            protected int[] findDependencies(int u) {
                Expression expression = values.get(u).getExpression();
                expression.collectRefs(allRefs, set);
                
                int[] result = set.toArray();
                set.clear();
                
                return result;
            }
            
        }.findComponents();
    }
    
    private void typeCheckValuesWithoutTypeAnnotations() {
        for(SCLValue[] group : valuesWithoutTypeAnnotation) {
            if(PRINT_VALUES) {
                System.out.println("---------------------------------------------");
                System.out.print("---");
                for(SCLValue value : group)
                    System.out.print(" " + value.getName());
                System.out.println();
            }
            
            for(int i=0;i<group.length;++i)
                group[i].setType(Types.metaVar(Kinds.STAR));
            
            TypingContext context = new TypingContext(errorLog, environment);
            context.recursiveValues = new THashSet<SCLValue>();
            for(SCLValue value : group)
                context.recursiveValues.add(value);
                    
            @SuppressWarnings("unchecked")
            ArrayList<EVariable>[] constraintDemands = new ArrayList[group.length];
            
            @SuppressWarnings("unchecked")
            ArrayList<EPlaceholder>[] recursiveReferences = new ArrayList[group.length];
            for(int i=0;i<group.length;++i) {
                context.recursiveReferences = new ArrayList<EPlaceholder>();
                
                SCLValue value = group[i];
                Expression expression = value.getExpression();
                expression = expression.checkType(context, value.getType());
                value.setExpression(expression);
                
                ArrayList<EVariable> constraintDemand = context.getConstraintDemand();
                if(!constraintDemand.isEmpty()) {
                    constraintDemands[i] = constraintDemand;
                    context.resetConstraintDemand();
                }
                
                recursiveReferences[i] = context.recursiveReferences;
            }

            for(Type type : Types.getTypes(group))
                type.addPolarity(Polarity.POSITIVE);
            context.solveSubsumptions(group[0].getExpression().getLocation());
            ArrayList<Constraint> allUnsolvedConstraints = new ArrayList<Constraint>(); 
            
            @SuppressWarnings("unchecked")
            ArrayList<Variable>[] freeEvidence = new ArrayList[group.length];  
            for(int i=0;i<group.length;++i) {
                if(constraintDemands[i] != null) {
                    SCLValue value = group[i];
                    Expression expression = value.getExpression();
                    
                    ReducedConstraints red = ConstraintSolver.solve(
                            ce, new ArrayList<TPred>(0), constraintDemands[i],
                            true /*!Types.isFunction(expression.getType())*/);                                        
                    
                    expression = ExpressionAugmentation.augmentSolved(
                            red.solvedConstraints, 
                            expression);
                    value.setExpression(expression);
                    value.setType(expression.getType());
                    
                    for(Constraint c : red.unsolvedConstraints)
                        if(c.constraint.isGround()) {
                            errorLog.log(c.getDemandLocation(), "There is no instance for <"+c.constraint+">.");
                        }          
                    
                    ArrayList<Variable> fe = new ArrayList<Variable>(red.unsolvedConstraints.size());
                    for(Constraint c : red.unsolvedConstraints) {
                        allUnsolvedConstraints.add(c);
                        fe.add(c.evidence);
                    }
                    freeEvidence[i] = fe;
                }
                else {
                    group[i].setExpression(group[i].getExpression().decomposeMatching());
                    freeEvidence[i] = new ArrayList<Variable>(0);
                }
            }

            THashSet<TVar> varSet = new THashSet<TVar>(); 
            for(int i=0;i<group.length;++i) {
                SCLValue value = group[i];
                Type type = value.getType();
                type = type.convertMetaVarsToVars();
                value.setType(type);
                varSet.addAll(Types.freeVars(type));
            }
            
            TVar[] vars = varSet.toArray(new TVar[varSet.size()]);
            
            // Collect all constraints needed in the group
            THashSet<TPred> constraintSet = new THashSet<TPred>();
            for(int i=0;i<group.length;++i) {
                for(Variable evidence : freeEvidence[i]) {
                    constraintSet.add((TPred)evidence.getType());
                }
            }
            TPred[] constraints = constraintSet.toArray(new TPred[constraintSet.size()]);
            for(TPred constraint : constraints)
                if(constraint.containsMetaVars()) {
                    for(Constraint c : allUnsolvedConstraints) {
                        if(Types.equals(c.constraint, constraint)) {
                            errorLog.log(c.getDemandLocation(), 
                                    "Constrain " + constraint + 
                                    " contains free variables not mentioned in the type of the value.");
                            break;
                        }
                    }
                }


            // TODO copy to TypeChecking2 from this onwards
            for(int i=0;i<group.length;++i) {                
                // Create evidence array of every value in the group that has the variables
                // in the same array as in the shared array
                ArrayList<Variable> fe = freeEvidence[i];
                THashMap<TPred, Variable> indexedEvidence = new THashMap<TPred, Variable>(fe.size());
                for(Variable v : fe)
                    indexedEvidence.put((TPred)v.getType(), v);
                fe.clear();
                for(TPred c : constraints) {
                    Variable var = indexedEvidence.get(c);
                    if(var == null) {
                        // These are variables that are not directly needed in 
                        // this definition but in the definitions that are
                        // recursively called
                        var = new Variable("evX");
                        var.setType(c);
                        fe.add(var);
                    }
                    fe.add(var);
                }
                
                // Add evidence parameters to the functions
                SCLValue value = group[i];
                value.setExpression(lambda(Types.NO_EFFECTS, fe, value.getExpression())
                        .closure(vars));
                value.setType(Types.forAll(vars, 
                        Types.constrained(constraints, value.getType())));
                
                // Add evidence parameters to recursive calls
                for(EPlaceholder ref : recursiveReferences[i]) {
                    ref.expression = loc(ref.expression.location, apply(
                            Types.NO_EFFECTS,
                            applyTypes(ref.expression, vars),
                            vars(fe)));
                }
            }
        }
    }
    
    private void typeCheckValuesWithTypeAnnotations() {
        ArrayList<TPred> givenConstraints = new ArrayList<TPred>();
        for(SCLValue value : valuesWithTypeAnnotation) {            
            Type type = value.getType();
            if(type != null) {
                if(PRINT_VALUES) {
                    System.out.println("---------------------------------------------");
                    System.out.println("--- " + value.getName() + " :: " + type);
                }
                Expression expression = value.getExpression();
                ArrayList<TVar> vars = new ArrayList<TVar>();
                type = Types.removeForAll(type, vars);                
                type = Types.removePred(type, givenConstraints);
                
                /*System.out.println("---------------------------------------------");
                TypeUnparsingContext tuc = new TypeUnparsingContext();
                System.out.println("--- " + value.getName() + " :: " + type.toString(tuc));
                for(TPred t : givenConstraints)
                    System.out.println(">>> " + t.toString(tuc));
                */
                TypingContext context = new TypingContext(errorLog, environment);
                //System.out.println(expression);
                expression = expression.checkType(context, type);
                //System.out.println(expression);
                expression.getType().addPolarity(Polarity.POSITIVE);
                context.solveSubsumptions(expression.getLocation());
                ArrayList<EVariable> demands = context.getConstraintDemand();
                if(!demands.isEmpty() || !givenConstraints.isEmpty()) {
                    ReducedConstraints red = 
                            ConstraintSolver.solve(ce, givenConstraints, demands, true);    
                    givenConstraints.clear();
                    for(Constraint c :  red.unsolvedConstraints) {
                        errorLog.log(c.getDemandLocation(), 
                                "Constraint <"+c.constraint+"> is not given and cannot be derived.");
                    }
                    if(errorLog.isEmpty()) { // To prevent exceptions
                        expression = ExpressionAugmentation.augmentSolved(
                                red.solvedConstraints,
                                expression);
                        expression = ExpressionAugmentation.augmentUnsolved(
                                red.givenConstraints, 
                                expression); 
                    }
                }
                else {
                    if(errorLog.isEmpty()) // To prevent exceptions
                        expression = expression.decomposeMatching();
                }
                expression = expression.closure(vars.toArray(new TVar[vars.size()]));
                value.setExpression(expression);
            }
        }
    }

    public void typeCheckRules() {
        TypingContext context = new TypingContext(errorLog, environment);
        for(TransformationRule rule : module.getRules()) {
            context.pushEffectUpperBound(rule.location, Types.metaVar(Kinds.EFFECT));
            rule.checkType(context);
            rule.setEffect(Types.canonical(context.popEffectUpperBound()));
        }
        context.solveSubsumptions(Locations.NO_LOCATION);
        
        ArrayList<EVariable> demands = context.getConstraintDemand();
        if(!demands.isEmpty()) {
            ReducedConstraints red = 
                    ConstraintSolver.solve(ce, new ArrayList<TPred>(), demands, true);
            for(Constraint c :  red.unsolvedConstraints) {
                errorLog.log(c.getDemandLocation(), 
                        "Constraint <"+c.constraint+"> is not given and cannot be derived.");
            }
        }
        
        for(MappingRelation mappingRelation : module.getMappingRelations())
            for(Type parameterType : mappingRelation.parameterTypes)
                if(!parameterType.isGround()) {
                    errorLog.log(mappingRelation.location, "Parameter types of the mapping relation are not completely determined.");
                    break;
                }
        
        /*for(Rule rule : module.getRules()) {
            System.out.println(rule.name);
            for(Variable variable : rule.variables)
                System.out.println("    " + variable.getName() + " :: " + variable.getType());
        }*/
    }
}