package org.simantics.scl.compiler.types.kinds;

import org.simantics.scl.compiler.common.exceptions.InternalCompilerError;
import org.simantics.scl.compiler.types.exceptions.KindUnificationException;

public class Kinds {
    public static final KCon STAR = new KCon("*");
    public static final KCon EFFECT = new KCon("E");
    public static final Kind STAR_TO_STAR = new KArrow(STAR, STAR);
    public static final Kind STAR_TO_STAR_TO_STAR = new KArrow(STAR, STAR_TO_STAR);
    
    public static KArrow arrow(Kind domain, Kind range) {
        return new KArrow(domain, range);
    }
    
    public static KMetaVar metaVar() {
        return new KMetaVar();
    }
    
    public static Kind canonical(Kind a) {
        while(a instanceof KMetaVar) {
            KMetaVar mv = (KMetaVar)a;
            if(mv.ref == null)
                return a;
            a = mv.ref;
        }
        return a;
    }
    
    public static void unifyWithStar(Kind a) throws KindUnificationException {
        a = canonical(a);
        if(a == STAR)
            return;
        if(a instanceof KMetaVar)
            ((KMetaVar)a).ref = STAR;
        throw new KindUnificationException();
    }
    
    /**
     * Tries to unify two kinds by linking matching meta-variables.
     * @throws KindUnificationException  if unification fails
     */
    public static void unify(Kind a, Kind b) throws KindUnificationException {
        a = canonical(a);
        b = canonical(b);
        if(a == b)
            return;
        if(a instanceof KMetaVar) {
            ((KMetaVar)a).setRef(b);
            return;
        }
        if(b instanceof KMetaVar) {
            ((KMetaVar)b).setRef(a);
            return;
        }
        if(a instanceof KArrow && b instanceof KArrow) {
            KArrow arrowA = (KArrow)a;
            KArrow arrowB = (KArrow)b;
            unify(arrowA.domain, arrowB.domain);
            unify(arrowA.range, arrowB.range);
            return;
        }
        throw new KindUnificationException();
    }

    public static boolean equalsCanonical(Kind a, Kind b) {
        if(a == b)
            return true;
        if(!(a instanceof KArrow))
            return false;
        if(!(b instanceof KArrow))
            return false;
        KArrow arrowA = (KArrow)a;
        KArrow arrowB = (KArrow)b;
        return equals(arrowA.domain, arrowB.domain) && 
                equals(arrowA.range, arrowB.range);
    }

    public static boolean equals(Kind a, Kind b) {
        return equalsCanonical(canonical(a), canonical(b));
    }

    public static Kind rangeOfArrow(Kind kind) {
        kind = canonical(kind);
        if(kind instanceof KArrow)
            return ((KArrow)kind).range;
        else if(kind instanceof KMetaVar) {
            Kind domain = Kinds.metaVar();
            Kind range = Kinds.metaVar();
            try {
                ((KMetaVar)kind).setRef(arrow(domain, range));
            } catch (KindUnificationException e) {
                // Should not fail because kind is canonical
                e.printStackTrace();
            }
            return range;
        }
        else
            throw new InternalCompilerError("Assumed arrow kind but encountered " + kind + ".");
    }    
}