package de.dhbwstuttgart.syntaxtree.factory;

import java.io.FileWriter;
import java.io.Writer;
import java.util.*;
import java.util.regex.Matcher;
import java.util.regex.Pattern;
import java.util.stream.Collectors;

import de.dhbwstuttgart.exceptions.DebugException;
import de.dhbwstuttgart.exceptions.NotImplementedException;
import de.dhbwstuttgart.parser.NullToken;
import de.dhbwstuttgart.parser.SyntaxTreeGenerator.FCGenerator;
import de.dhbwstuttgart.parser.scope.JavaClassName;
import de.dhbwstuttgart.sat.asp.model.ASPRule;
import de.dhbwstuttgart.sat.asp.parser.ASPParser;
import de.dhbwstuttgart.syntaxtree.ClassOrInterface;
import de.dhbwstuttgart.syntaxtree.type.*;
import de.dhbwstuttgart.syntaxtree.type.Void;
import de.dhbwstuttgart.syntaxtree.type.WildcardType;
import de.dhbwstuttgart.typeinference.constraints.Constraint;
import de.dhbwstuttgart.typeinference.constraints.ConstraintSet;
import de.dhbwstuttgart.typeinference.constraints.Pair;
import de.dhbwstuttgart.typeinference.result.PairTPHEqualTPH;
import de.dhbwstuttgart.typeinference.result.PairTPHequalRefTypeOrWildcardType;
import de.dhbwstuttgart.typeinference.result.PairTPHsmallerTPH;
import de.dhbwstuttgart.typeinference.result.ResultPair;
import de.dhbwstuttgart.typeinference.unify.model.*;

public class UnifyTypeFactory {
	
	private static ArrayList<PlaceholderType> PLACEHOLDERS = new ArrayList<>(); 

    public static FiniteClosure generateFC(List<ClassOrInterface> fromClasses, Writer logFile) throws ClassNotFoundException {
        /*
        Die transitive Hülle muss funktionieren.
        Man darf schreiben List<A> extends AL<A>
        und Vector<B> extends List<B>
        hier muss dann aber dennoch die Vererbung V < L < AL
        hergestellt werden.
        In einem solchen Vererbungsbaum dürfen die TPH auch die gleichen Namen haben.
        Generell dürfen sie immer die gleichen Namen haben.
        TODO: die transitive Hülle bilden
         */
        return new FiniteClosure(FCGenerator.toUnifyFC(fromClasses), logFile);
    }

    public static UnifyPair generateSmallerPair(UnifyType tl, UnifyType tr){
        return new UnifyPair(tl, tr, PairOperator.SMALLER);
    }

    public static UnifyPair generateSmallerDotPair(UnifyType tl, UnifyType tr){
        return new UnifyPair(tl, tr, PairOperator.SMALLERDOT);
    }

    public static UnifyPair generateSmallNotEqualDotPair(UnifyType tl, UnifyType tr){
        return new UnifyPair(tl, tr, PairOperator.SMALLERNEQDOT);
    }
    
    public static UnifyPair generateEqualDotPair(UnifyType tl, UnifyType tr){
        return new UnifyPair(tl, tr, PairOperator.EQUALSDOT);
    }

    /**
     * Convert from
     * ASTType -> UnifyType
     */
    public static UnifyType convert(RefTypeOrTPHOrWildcardOrGeneric t, Boolean innerType){
        if(t instanceof GenericRefType){
            return UnifyTypeFactory.convert((GenericRefType)t, innerType);
        }else if(t instanceof TypePlaceholder){
            return UnifyTypeFactory.convert((TypePlaceholder)t, innerType);
        }else if(t instanceof ExtendsWildcardType){
            return UnifyTypeFactory.convert((ExtendsWildcardType)t, innerType);
        }else if(t instanceof SuperWildcardType){
            return UnifyTypeFactory.convert((SuperWildcardType)t, innerType);
        }else if(t instanceof RefType){
            return UnifyTypeFactory.convert((RefType)t, innerType);
        }
        //Es wurde versucht ein Typ umzuwandeln, welcher noch nicht von der Factory abgedeckt ist
        throw new NotImplementedException("Der Typ "+t+" kann nicht umgewandelt werden");
    }

    public static UnifyType convert(RefType t, Boolean innerType){
        //Check if it is a FunN Type:
        Pattern p = Pattern.compile("Fun(\\d+)[$][$]");
        Matcher m = p.matcher(t.getName().toString());
        boolean b = m.matches();
        if(b){
            Integer N = Integer.valueOf(m.group(1));
            if((N + 1) == t.getParaList().size()){
                return convertFunN(t.getParaList(), false);
            }
        }
        UnifyType ret;
        if(t.getParaList() != null && t.getParaList().size() > 0){
            List<UnifyType> params = new ArrayList<>();
            for(RefTypeOrTPHOrWildcardOrGeneric pT : t.getParaList()){
                params.add(UnifyTypeFactory.convert(pT, true));
            }
            ret = new ReferenceType(t.getName().toString(),new TypeParams(params));
        }else{
            ret = new ReferenceType(t.getName().toString(), false);
        }
        return ret;
    }

    public static UnifyType convertFunN(List<RefTypeOrTPHOrWildcardOrGeneric> paraList, Boolean innerType){
        UnifyType ret;
        List<UnifyType> params = new ArrayList<>();
        if(paraList != null && paraList.size() > 0){
            for(RefTypeOrTPHOrWildcardOrGeneric pT : paraList){
                params.add(UnifyTypeFactory.convert(pT, false));
            }
        }
        ret = FunNType.getFunNType(new TypeParams(params));
        return ret;
    }

    public static UnifyType convert(TypePlaceholder tph, Boolean innerType){
    	if (tph.getName().equals("AFR")) {
    		System.out.println("XXX"+innerType);
    	}
    	PlaceholderType ntph = new PlaceholderType(tph.getName());
    	int in = PLACEHOLDERS.indexOf(ntph);
		if (in == -1) {
			PLACEHOLDERS.add(ntph);
			ntph.setInnerType(innerType);
			return ntph;
		}
		else {
			 PlaceholderType oldpht = PLACEHOLDERS.get(in);
			 oldpht.setInnerType(oldpht.isInnerType() || innerType);
			 return oldpht;
		}
    }

    public static UnifyType convert(GenericRefType t, Boolean innerType){
        return new ReferenceType(t.getParsedName(), true);
    }

    public static UnifyType convert(WildcardType t, Boolean innerType){
        if(t.isExtends())
            return new ExtendsType(UnifyTypeFactory.convert(t.getInnerType(), false));
        else if(t.isSuper())
            return new SuperType(UnifyTypeFactory.convert(t.getInnerType(), false));
        else throw new NotImplementedException();
    }


    public static ConstraintSet<UnifyPair> convert(ConstraintSet<Pair> constraints) {
        return constraints.map(UnifyTypeFactory::convert);
    }

    public static Constraint<UnifyPair> convert(Constraint<Pair> constraint){
        return constraint.stream().map(UnifyTypeFactory::convert).collect(Collectors.toCollection(Constraint::new));
    }

    public static UnifyPair convert(Pair p) {
    	UnifyPair ret = null;
        if(p.GetOperator().equals(PairOperator.SMALLERDOT)) {
             ret = generateSmallerDotPair(UnifyTypeFactory.convert(p.TA1, false)
                    , UnifyTypeFactory.convert(p.TA2, false));
            //return ret;
        }else if(p.GetOperator().equals(PairOperator.SMALLERNEQDOT)) {
             ret = generateSmallNotEqualDotPair(UnifyTypeFactory.convert(p.TA1, false)
                    , UnifyTypeFactory.convert(p.TA2, false));
            //return ret;
        }else if(p.GetOperator().equals(PairOperator.EQUALSDOT)) {
             ret = generateEqualDotPair(UnifyTypeFactory.convert(p.TA1, false)
                    , UnifyTypeFactory.convert(p.TA2, false));
            //return ret;
        }else if(p.GetOperator().equals(PairOperator.SMALLER)){
            ret =  generateSmallerPair(UnifyTypeFactory.convert(p.TA1, false),
                    UnifyTypeFactory.convert(p.TA2, false));
        }else            throw new NotImplementedException();
        UnifyType lhs, rhs;
        if (((lhs = ret.getLhsType()) instanceof PlaceholderType) 
        		&& ((PlaceholderType)lhs).isWildcardable() 
        		&&	(rhs = ret.getLhsType()) instanceof PlaceholderType) {
        	if (lhs.getName().equals("AQ")) {
        		System.out.println("");
        	}
        	((PlaceholderType)rhs).enableWildcardtable();
        }
        
        if (((rhs = ret.getLhsType()) instanceof PlaceholderType) 
        		&& ((PlaceholderType)rhs).isWildcardable()
        		&&	(lhs = ret.getLhsType()) instanceof PlaceholderType) {
        	if (rhs.getName().equals("AQ")) {
        		System.out.println("");
        	}
        	((PlaceholderType)lhs).enableWildcardtable();
        }
        return ret;
    }

    /**
     * Convert from
     * UnifyType -> ASTType
     */
    public static Set<ResultPair> convert(Set<UnifyPair> unifyPairSet, Map<String,TypePlaceholder> tphs) {
        return unifyPairSet.stream().map(
                unifyPair -> convert(unifyPair, tphs))
                        .collect(Collectors.toSet());
    }

    public static ResultPair convert(UnifyPair mp, Map<String,TypePlaceholder> tphs) {
        RefTypeOrTPHOrWildcardOrGeneric tl = UnifyTypeFactory.convert(mp.getLhsType(), tphs);
        RefTypeOrTPHOrWildcardOrGeneric tr = UnifyTypeFactory.convert(mp.getRhsType(), tphs);
        if(tl instanceof TypePlaceholder){
            if(tr instanceof TypePlaceholder) {

                if(mp.getPairOp().equals(PairOperator.EQUALSDOT)) {
                    return new PairTPHEqualTPH((TypePlaceholder)tl, (TypePlaceholder)tr);
                    //Einfach ignorieren TODO: Das hier muss ausgebessert werden:
                    //return new PairTPHequalRefTypeOrWildcardType((TypePlaceholder)tl, ASTFactory.createObjectType());
                }else{
                    return new PairTPHsmallerTPH((TypePlaceholder)tl, (TypePlaceholder)tr);
                }
            }else if(tr instanceof RefType){
                return new PairTPHequalRefTypeOrWildcardType((TypePlaceholder)tl, (RefType) tr);
            }else if(tr instanceof WildcardType){
                return new PairTPHequalRefTypeOrWildcardType((TypePlaceholder)tl, (WildcardType) tr);
            }else if(tr instanceof GenericRefType){
                return new PairTPHequalRefTypeOrWildcardType((TypePlaceholder)tl, (GenericRefType) tr);
            }else throw new NotImplementedException();
        }else throw new NotImplementedException();
    }

    public static RefTypeOrTPHOrWildcardOrGeneric convert(ReferenceType t, Map<String,TypePlaceholder> tphs) {
        if(JavaClassName.Void.equals(t.getName()))return new Void(new NullToken());
        if (t.isGenTypeVar()) return new GenericRefType(t.getName(),new NullToken());
        RefType ret = new RefType(new JavaClassName(t.getName()),convert(t.getTypeParams(), tphs),new NullToken());
        return ret;
    }

    public static RefTypeOrTPHOrWildcardOrGeneric convert(FunNType t, Map<String,TypePlaceholder> tphs) {
        RefType ret = new RefType(new JavaClassName(t.getName()), convert(t.getTypeParams(), tphs), new NullToken());
        return ret;
    }

    public static RefTypeOrTPHOrWildcardOrGeneric convert(SuperType t, Map<String,TypePlaceholder> tphs) {
        RefTypeOrTPHOrWildcardOrGeneric innerType = convert(t.getSuperedType(), tphs);
        return new SuperWildcardType(innerType, new NullToken());
    }

    public static RefTypeOrTPHOrWildcardOrGeneric convert(ExtendsType t, Map<String,TypePlaceholder> tphs) {
        RefTypeOrTPHOrWildcardOrGeneric innerType = convert(t.getExtendedType(), tphs);
        return new ExtendsWildcardType(innerType, new NullToken());
    }

    public static RefTypeOrTPHOrWildcardOrGeneric convert(PlaceholderType t, Map<String,TypePlaceholder> tphs) {
        TypePlaceholder ret = tphs.get(t.getName());
        if(ret == null){ //Dieser TPH wurde vom Unifikationsalgorithmus erstellt
            ret = TypePlaceholder.fresh(new NullToken());
            tphs.put(t.getName(), ret);
        }
        return ret;
    }

    public static RefTypeOrTPHOrWildcardOrGeneric convert(UnifyType t, Map<String,TypePlaceholder> tphs) {
        if(t instanceof FunNType)return convert((FunNType) t, tphs);
        if(t instanceof ReferenceType)return convert((ReferenceType) t, tphs);
        if(t instanceof SuperType)return convert((SuperType) t, tphs);
        if(t instanceof ExtendsType)return convert((ExtendsType) t, tphs);
        if(t instanceof PlaceholderType)return convert((PlaceholderType) t, tphs);
        throw new NotImplementedException("Der Typ "+t+" kann nicht umgewandelt werden");
    }

    private static List<RefTypeOrTPHOrWildcardOrGeneric> convert(TypeParams typeParams, Map<String,TypePlaceholder> tphs) {
        List<RefTypeOrTPHOrWildcardOrGeneric> ret = new ArrayList<>();
        for(UnifyType uT : typeParams){
            RefTypeOrTPHOrWildcardOrGeneric toAdd = convert(uT, tphs);
            ret.add(toAdd);
        }
        return ret;
    }

}
