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

import org.simantics.scl.compiler.common.exceptions.InternalCompilerError;
import org.simantics.scl.compiler.internal.types.effects.EffectIdMap;
import org.simantics.scl.compiler.types.TMetaVar;
import org.simantics.scl.compiler.types.exceptions.UnificationException;
import org.simantics.scl.compiler.types.util.Polarity;

public class SubsumptionGraph {
    public static final int REMOVED = Integer.MAX_VALUE-1;
    
    public static class LowerBoundSource {
        public final long location;
        public final int lower;
        public final LowerBoundSource next;
        public LowerBoundSource(long location, int lower, LowerBoundSource next) {
            this.location = location;
            this.lower = lower;
            this.next = next;
        }
    }
    
    public static abstract class Node {
        int lowerBound = EffectIdMap.MIN;
        int upperBound = EffectIdMap.MAX;
        Sub lower;
        LowerBoundSource lowerBoundSource;
        
        public void addLowerBoundSource(long location, int lower) {
            lowerBoundSource = new LowerBoundSource(location, lower, lowerBoundSource);
        }
    }
    
    public static class VarNode extends Node {
        TMetaVar origin;
        Sub upper;
        PartOfUnion partOf;
        int index;
        
        public VarNode(TMetaVar origin) {
            this.origin = origin;
        }
        
        public Polarity getPolarity() {
            return origin.getPolarity();
        }

        public void replaceBy(VarNode replacement) {
            try {
                origin.setRef(replacement.origin);
            } catch(UnificationException e) {
                throw new InternalCompilerError(e);
            }
            {
                Sub last = null;
                for(Sub cur=upper;cur!=null;cur=cur.aNext) {
                    cur.a = replacement;
                    last = cur;
                }
                if(last != null) {
                    last.aNext = replacement.upper;
                    if(last.aNext != null)
                        last.aNext.aPrev = last;
                    replacement.upper = upper;
                }

                last = null;
                for(Sub cur=lower;cur!=null;cur=cur.bNext) {
                    cur.b = replacement;
                    last = cur;
                }
                if(last != null) {
                    last.bNext = replacement.lower;
                    if(last.bNext != null)
                        last.bNext.bPrev = last;
                    replacement.lower = lower;
                }
            }
            {
                PartOfUnion last = null;
                for(PartOfUnion cur=partOf;cur!=null;cur=cur.bNext) {
                    cur.a = replacement;
                    last = cur;
                }
                if(last != null) {
                    last.aNext = replacement.partOf;
                    if(last.aNext != null)
                        last.aNext.bPrev = last;
                    replacement.partOf = partOf;
                }
            }
            index = REMOVED;
        }

        public void removeConstantNode(EffectIdMap effectIds, int constValue) {
            try {
                origin.setRef(effectIds.toType(constValue));
            } catch (UnificationException e) {
                throw new InternalCompilerError(e);
            }
            for(Sub cur=lower;cur!=null;cur=cur.bNext)
                cur.detachA();
            for(Sub cur=upper;cur!=null;cur=cur.aNext)
                cur.detachB();
            for(PartOfUnion cur=partOf;cur!=null;cur=cur.aNext) {
                cur.detachB();
                cur.b.constPart |= constValue;
            }
            index = REMOVED;
        }
    }
    
    public static class UnionNode extends Node {
        long location;
        PartOfUnion parts;
        int constPart;
        
        public UnionNode(long location, int constPart) {
            this.location = location;
            this.constPart = constPart;
            this.lowerBound = constPart;
        }

        public void remove() {
            for(Sub cur=lower;cur!=null;cur=cur.bNext)
                cur.detachA();
            for(PartOfUnion cur=parts;cur!=null;cur=cur.bNext)
                cur.detachA();
            constPart = REMOVED;
        }
    }
    
    public static class Sub {
        VarNode a;
        Node b;
        Sub aNext;
        Sub aPrev;
        Sub bNext;
        Sub bPrev;
        
        public Sub(VarNode a, Node b) {
            this.a = a;
            this.b = b;
            
            aNext = a.upper;
            if(aNext != null)
                aNext.aPrev = this;
            a.upper = this;
        
            bNext = b.lower;
            if(bNext != null)
                bNext.bPrev = this;
            b.lower = this;
        }
        
        public void detachA() {
            if(aNext != null)
                aNext.aPrev = aPrev;
            if(aPrev != null)
                aPrev.aNext = aNext;
            else
                a.upper = aNext;
        }

        public void detachB() {
            if(bNext != null)
                bNext.bPrev = bPrev;
            if(bPrev != null)
                bPrev.bNext = bNext;
            else
                b.lower = bNext;
        }
        
        public void remove() {
            detachA();
            detachB();
        }
    }
    
    public static class PartOfUnion {
        VarNode a;
        UnionNode b;
        PartOfUnion aNext;
        PartOfUnion aPrev;
        PartOfUnion bNext;
        PartOfUnion bPrev;
        
        public PartOfUnion(VarNode a, UnionNode b) {
            this.a = a;
            this.b = b;
            
            aNext = a.partOf;
            if(aNext != null)
                aNext.aPrev = this;
            a.partOf = this;
        
            bNext = b.parts;
            if(bNext != null)
                bNext.bPrev = this;
            b.parts = this;
        }
        
        public void detachA() {
            if(aNext != null)
                aNext.aPrev = aPrev;
            if(aPrev != null)
                aPrev.aNext = aNext;
            else
                a.partOf = aNext;
        }
        
        public void detachB() {
            if(bNext != null)
                bNext.bPrev = bPrev;
            if(bPrev != null)
                bPrev.bNext = bNext;
            else
                b.parts = bNext;
        }
        
        public void remove() {
            detachA();
            detachB();
        }

    }
}