package org.simantics.scl.compiler.internal.elaboration.subsumption;

import java.util.ArrayList;

import org.simantics.scl.compiler.common.exceptions.InternalCompilerError;
import org.simantics.scl.compiler.internal.types.effects.EffectIdMap;
import org.simantics.scl.compiler.top.SCLCompilerConfiguration;
import org.simantics.scl.compiler.types.TMetaVar;
import org.simantics.scl.compiler.types.Type;
import org.simantics.scl.compiler.types.exceptions.UnificationException;

public class Var {
    String name;
    
    int constLowerBound = EffectIdMap.MIN;
    int constUpperBound = EffectIdMap.MAX;
    int upperApprox = EffectIdMap.MAX;
    TMetaVar original;
    
    ArrayList<Var> simpleLowerBounds = new ArrayList<Var>();
    ArrayList<Var> simpleUpperBounds = new ArrayList<Var>();
    ArrayList<VUnion> complexLowerBounds = new ArrayList<VUnion>();
    ArrayList<VUnion> complexUpperBounds = new ArrayList<VUnion>();
    
    SubSolver solver;
    boolean dirty;
    
    public Var(TMetaVar original, String name, SubSolver solver) {
        this.original = original;
        this.name = name;
        this.solver = solver;        
        markDirty();
    }

    void markDirty() {
        if(!dirty) {
            dirty = true;
            solver.dirtyQueue.add(this);
        }
    }
    
    /**
     * Adds a constant constraint
     */
    public void addUpperBound(int c) {
        c &= constUpperBound;
        if(c != constUpperBound) {
            if((c & constLowerBound) != constLowerBound) {
                solver.errorLog.log(solver.globalLoc, "Subsumption failed: " + 
                        solver.effectIds.toType(constLowerBound) + " is not a subtype of " +
                        solver.effectIds.toType(c)
                        );
                return;
            }
            constUpperBound = c;
            for(int i=0;i<complexUpperBounds.size();++i) {
                VUnion u = complexUpperBounds.get(i); 
                u.con &= c;
                if(u.con == 0 && u.vars.size() == 1) {
                    removeComplexUpperBound(i);               
                    --i;
                    addUpperBound(u.vars.get(0));
                }
            }
            markDirty();
        }
    }
    
    public void addLowerBound(int c) {
        if((c | constUpperBound) != constUpperBound) {
            solver.errorLog.log(solver.globalLoc, "Subsumption failed: " + 
                    solver.effectIds.toType(c) + " is not a subtype of " +
                    solver.effectIds.toType(constUpperBound)
                    );
            return;
        }
        constLowerBound |= c;
        markDirty();
    }
    
    private void removeComplexUpperBound(int i) {
        VUnion u = complexUpperBounds.get(i);
        int lastId = complexUpperBounds.size()-1;        
        VUnion last = complexUpperBounds.remove(lastId);
        if(i < lastId)
            complexUpperBounds.set(i, last);
        for(Var v : u.vars) {
            v.complexLowerBounds.remove(u);
            v.markDirty();
        }
    }
    
    /**
     * Adds a simple variable constraint
     */
    public void addUpperBound(Var var) {
        if(var == this)
            return;
        if(simpleUpperBounds.size() < var.simpleLowerBounds.size()) {
            if(simpleUpperBounds.contains(var))
                return;
        }
        else {
            if(var.simpleLowerBounds.contains(this))
                return;
        }
        
        for(int i=0;i<complexUpperBounds.size();++i)
            if(complexUpperBounds.get(i).vars.contains(var)) {
                removeComplexUpperBound(i);               
                --i;
            }
        
        simpleUpperBounds.add(var);
        var.simpleLowerBounds.add(this);
        
        markDirty();
        var.markDirty();
    }
    
    /**
     * Adds a complex constraint
     */
    public void addUpperBound(VUnion u) {
        if(u.vars.isEmpty()) {
            addUpperBound(u.con);
            return;
        }        
        if(u.vars.contains(this))
            return;        
        for(Var v : u.vars)
            if(simpleUpperBounds.contains(v))
                return;
        u.con &= constUpperBound;
        if(u.con == constUpperBound)
            return;
        if(u.con == 0 && u.vars.size() == 1)
            addUpperBound(u.vars.get(0));
        else {
            u.low = this;
            complexUpperBounds.add(u);
            markDirty();
            for(Var v : u.vars)
                v.complexLowerBounds.add(u);
        }
        // TODO compare complex upper bounds together
    }
    
    public void replaceWith(int con) {
        // Check that replacement is sound
        if(SCLCompilerConfiguration.DEBUG) {
            if((con&constLowerBound) != constLowerBound)
                throw new InternalCompilerError();
            if((con|constUpperBound) != constUpperBound)
                throw new InternalCompilerError();
        }
        
        // Remove the variable and unify original TMetaVar
        solver.vars.remove(original);
        try {
            Type type = solver.effectIds.toType(con);
            if(SubSolver.DEBUG)
                System.out.println(original.toString(solver.tuc) + " := " + type.toString(solver.tuc));
            original.setRef(type);
        } catch (UnificationException e) {
            throw new InternalCompilerError();
        }
        
        // Propagate change to lower and upper bounds
        for(Var v : simpleUpperBounds) {
            v.simpleLowerBounds.remove(this);
            v.addLowerBound(con);
            v.markDirty();
        }
        for(Var v : simpleLowerBounds) {
            v.simpleUpperBounds.remove(this);
            v.addUpperBound(con);
            v.markDirty();
        }
        for(VUnion u : complexUpperBounds) {
            u.low = null;
            u.con |= ~con;
            if(u.vars.size() == 1) {
                Var uv = u.vars.get(0);
                uv.constLowerBound |= ~u.con;
                uv.complexLowerBounds.remove(u);
                uv.markDirty();
            }
            else {
                for(Var uv : u.vars)
                    uv.markDirty();
            }
        }
        for(VUnion u : complexLowerBounds) {
            u.low.markDirty();
            u.vars.remove(this);
            u.con |= con;
            u.con &= u.low.constUpperBound;
            if(u.vars.isEmpty()) {
                u.low.complexUpperBounds.remove(u);
                u.low.addUpperBound(u.con);
            }
            else if(u.vars.size() == 1 && u.con == 0) {
                u.low.complexUpperBounds.remove(u);
                u.low.addUpperBound(u.vars.get(0));
            }
        }
    }
    
    public void replaceDownwards(Var var) {
        // Remove the variable and unify original TMetaVar
        solver.vars.remove(original);
        try {
            if(SubSolver.DEBUG)
                System.out.println(original.toString(solver.tuc) + " := " + var.original.toString(solver.tuc));
            original.setRef(var.original);
        } catch (UnificationException e) {
            throw new InternalCompilerError();
        }
        
        // Remove downwards dependencies
        if(constLowerBound != 0)
            throw new InternalCompilerError();
        for(Var v : simpleLowerBounds)
            v.simpleUpperBounds.remove(this);
        if(!complexLowerBounds.isEmpty())
            throw new InternalCompilerError();
        var.markDirty();
        
        // Propagate change to upper bounds
        var.addUpperBound(constUpperBound);
        for(Var v : simpleUpperBounds) {
            v.simpleLowerBounds.remove(this);
            var.addUpperBound(v);
        }
        for(VUnion u : complexUpperBounds) {
            var.addUpperBound(u);
        }
    }
    
    public void replaceUpwards(Var var) {
        // Remove the variable and unify original TMetaVar
        solver.vars.remove(original);
        try {
            if(SubSolver.DEBUG)
                System.out.println(original.toString(solver.tuc) + " := " + var.original.toString(solver.tuc));
            original.setRef(var.original);
        } catch (UnificationException e) {
            throw new InternalCompilerError();
        }
        
        // Remove upwards dependencies
        if(constUpperBound != EffectIdMap.MAX)
            throw new InternalCompilerError();
        for(Var v : simpleUpperBounds)
            v.simpleLowerBounds.remove(this);
        if(!complexUpperBounds.isEmpty())
            throw new InternalCompilerError();
        var.markDirty();
        
        // Propagate change to lower bounds
        var.addLowerBound(constLowerBound);
        for(Var v : simpleLowerBounds) {
            v.simpleUpperBounds.remove(this);
            v.markDirty();
            v.addUpperBound(var);
        }
        for(VUnion u : complexLowerBounds) {
            u.vars.remove(this);
            if(u.low != null) {
                u.low.markDirty();            
                if(u.vars.isEmpty() && u.con == 0) {
                    u.low.complexUpperBounds.remove(u);
                    u.low.addUpperBound(var);
                    continue;
                }
            }
            u.addVar(var);
        }
    }

    public boolean isFree() {
        return constLowerBound == EffectIdMap.MIN && 
                constUpperBound == EffectIdMap.MAX &&
                simpleLowerBounds.isEmpty() &&
                simpleUpperBounds.isEmpty() &&
                complexLowerBounds.isEmpty() &&
                complexUpperBounds.isEmpty();
    }
}