//PL 2018-12-19: typeInferenceOld nach typeInference uebertragen
package de.dhbwstuttgart.core;

import de.dhbwstuttgart.bytecode.Codegen;
import de.dhbwstuttgart.bytecode.FunNGenerator;
import de.dhbwstuttgart.environment.CompilationEnvironment;
import de.dhbwstuttgart.environment.DirectoryClassLoader;
import de.dhbwstuttgart.exceptions.DebugException;
import de.dhbwstuttgart.languageServerInterface.model.LanguageServerTransferObject;
import de.dhbwstuttgart.parser.JavaTXParser;
import de.dhbwstuttgart.parser.NullToken;
import de.dhbwstuttgart.parser.scope.GenericsRegistry;
import de.dhbwstuttgart.parser.SyntaxTreeGenerator.SyntaxTreeGenerator;
import de.dhbwstuttgart.parser.antlr.Java17Parser.SourceFileContext;
import de.dhbwstuttgart.parser.scope.JavaClassName;
import de.dhbwstuttgart.parser.scope.JavaClassRegistry;
import de.dhbwstuttgart.syntaxtree.ClassOrInterface;
import de.dhbwstuttgart.syntaxtree.GenericTypeVar;
import de.dhbwstuttgart.syntaxtree.Method;
import de.dhbwstuttgart.syntaxtree.ParameterList;
import de.dhbwstuttgart.syntaxtree.SourceFile;
import de.dhbwstuttgart.syntaxtree.GenericDeclarationList;
import de.dhbwstuttgart.syntaxtree.factory.ASTFactory;
import de.dhbwstuttgart.syntaxtree.factory.UnifyTypeFactory;
import de.dhbwstuttgart.syntaxtree.type.ExtendsWildcardType;
import de.dhbwstuttgart.syntaxtree.type.GenericRefType;
import de.dhbwstuttgart.syntaxtree.type.RefType;
import de.dhbwstuttgart.syntaxtree.type.RefTypeOrTPHOrWildcardOrGeneric;
import de.dhbwstuttgart.syntaxtree.type.SuperWildcardType;
import de.dhbwstuttgart.syntaxtree.type.TypePlaceholder;
import de.dhbwstuttgart.syntaxtree.type.TypeVisitor;
import de.dhbwstuttgart.syntaxtree.visual.ASTTypePrinter;
import de.dhbwstuttgart.target.generate.ASTToTargetAST;
import de.dhbwstuttgart.target.generate.GenericsResult;
import de.dhbwstuttgart.typeinference.constraints.Constraint;
import de.dhbwstuttgart.typeinference.constraints.ConstraintSet;
import de.dhbwstuttgart.typeinference.constraints.Pair;
import de.dhbwstuttgart.typeinference.result.ResultSet;
import de.dhbwstuttgart.typeinference.typeAlgo.TYPE;
import de.dhbwstuttgart.typeinference.unify.RuleSet;
import de.dhbwstuttgart.typeinference.unify.TypeUnify;
import de.dhbwstuttgart.typeinference.unify.distributeVariance;
import de.dhbwstuttgart.typeinference.unify.interfaces.IFiniteClosure;
import de.dhbwstuttgart.typeinference.unify.model.PairOperator;
import de.dhbwstuttgart.typeinference.unify.model.PlaceholderType;
import de.dhbwstuttgart.typeinference.unify.model.UnifyPair;
import de.dhbwstuttgart.typeinference.unify.model.UnifyType;
import de.dhbwstuttgart.typeinference.unify.TypeUnifyTask;
import de.dhbwstuttgart.typeinference.unify.UnifyResultListener;
import de.dhbwstuttgart.typeinference.unify.UnifyResultListenerImpl;
import de.dhbwstuttgart.typeinference.unify.UnifyResultModel;
import de.dhbwstuttgart.typeinference.unify.UnifyTaskModel;

import java.io.*;
import java.lang.reflect.Modifier;
import java.nio.file.Path;
import java.util.*;
import java.util.Map.Entry;
import java.util.function.Function;
import java.util.stream.Collectors;

import org.apache.commons.io.output.NullOutputStream;

public class JavaTXCompiler {

	// public static JavaTXCompiler INSTANCE;
	final CompilationEnvironment environment;
	Boolean resultmodel = true;
    public final Map<File, SourceFile> sourceFiles = new HashMap<>();

    Boolean log = false; //gibt an ob ein Log-File nach System.getProperty("user.dir")+""/logFiles/"" geschrieben werden soll?
    public volatile UnifyTaskModel usedTasks = new UnifyTaskModel();
    public final DirectoryClassLoader classLoader;

	public final List<File> classPath;
	private final File outputPath;

	public final Map<String, FunNGenerator.GenericParameters> usedFunN = new HashMap<>();
	public final Set<Integer> usedFunNSuperTypes = new HashSet<>();

	public Map<String, byte[]> auxiliaries = new HashMap<>();

	public DirectoryClassLoader getClassLoader() {
		return classLoader;
	}
   
	public JavaTXCompiler(File sourceFile) throws IOException, ClassNotFoundException {
		this(Arrays.asList(sourceFile), List.of(), new File("."));
	}

	public JavaTXCompiler(File sourceFile, Boolean log) throws IOException, ClassNotFoundException {
		this(sourceFile);
		this.log = log;
	}

	public JavaTXCompiler(List<File> sourceFiles) throws IOException, ClassNotFoundException {
		this(sourceFiles, List.of(), new File("."));
	}

	public JavaTXCompiler(List<File> sources, List<File> contextPath, File outputPath) throws IOException, ClassNotFoundException {
		var path = new ArrayList<>(contextPath);
		if (contextPath.isEmpty()) {
			// When no contextPaths are given, the working directory is the sources root
			path.add(new File(System.getProperty("user.dir")));
		}
		if (outputPath != null) path.add(outputPath);
		classLoader = new DirectoryClassLoader(path, ClassLoader.getSystemClassLoader());
		environment = new CompilationEnvironment(sources, classLoader);
		classPath = path;
		this.outputPath = outputPath;

		for (File s : sources) {
			parse(s);
		}
		// INSTANCE = this;
	}

	private void addSourceFile(File file, SourceFile sf) {
		sourceFiles.put(file, sf);
	}

	public ClassOrInterface getClass(JavaClassName name) {
		if (loadedClasses.containsKey(name)) return loadedClasses.get(name).cif();
		for (var sf : sourceFiles.values()) {
			for (var clazz : sf.KlassenVektor) {
				if (clazz.getClassName().equals(name)) return clazz;
			}
		}
		try {
			var clazz = classLoader.loadClass(name.toString());
			if (clazz != null)
				return ASTFactory.createClass(clazz);
		} catch (ClassNotFoundException ignored) {}
		return null;
	}

	public ConstraintSet<Pair> getConstraints(File sourceFile) throws ClassNotFoundException, IOException {
		Set<ClassOrInterface> allClasses = new HashSet<>();// environment.getAllAvailableClasses();
		ClassOrInterface objectClass = ASTFactory.createClass(Object.class);
		var recordClass = ASTFactory.createClass(Record.class);
		allClasses.add(objectClass);
		allClasses.add(recordClass);

		var sf = sourceFiles.get(sourceFile);
		var importedClasses = new ArrayList<ClassOrInterface>();
		for (JavaClassName name : sf.getImports()) {
			importedClasses.addAll(getAvailableClasses(name));
		}
		for (Class c : CompilationEnvironment.loadDefaultPackageClasses(sf.getPkgName(), sourceFile, this)) {
			ClassOrInterface importedClass = ASTFactory.createClass(c);
			importedClasses.add(importedClass);
		}
		sf.availableClasses.addAll(importedClasses);

		SourceFile sf_new = new SourceFile(sf.getPkgName(), sf.KlassenVektor.stream().map(cl -> new ClassOrInterface(cl)).collect(Collectors.toCollection(ArrayList::new)), sf.imports);
		// sf enthaelt neues Source-File, neue Klassen-Objekte und neue
		// ArrayListen-Objekte fuer Fields, Construktoren und Methoden
		// Alle anderen Objekte werden nur kopiert.
		var isCached = false;
		for (var clazz : sf.availableClasses) {
			if (loadedClasses.containsKey(clazz.getClassName())) {
				allClasses.removeIf(cl -> cl.getClassName().equals(clazz.getClassName()));
				var cif = loadedClasses.get(clazz.getClassName()).cif();
				allClasses.add(cif);
				isCached = true;
			}
		}

		if (!isCached) {
			sf_new.KlassenVektor.forEach(cl -> addMethods(sf_new, cl, sf.availableClasses, objectClass));
			allClasses.addAll(sf_new.getClasses());
		}

		allClasses.addAll(sf.KlassenVektor);

		TYPE ty = new TYPE(sf, allClasses);
		var constraints = ty.getConstraints();
		return constraints;
	}

	void addMethods(SourceFile sf, ClassOrInterface cl, List<ClassOrInterface> importedClasses, ClassOrInterface objectClass) {
		if (!cl.areMethodsAdded()) {
			ClassOrInterface superclass = null;
			Optional<ClassOrInterface> optSuperclass = importedClasses.stream().filter(x -> x.getClassName().equals(cl.getSuperClass().getName())).findFirst();
			if (optSuperclass.isPresent()) {
				superclass = optSuperclass.get();
			} else {
				optSuperclass = sf.KlassenVektor.stream().filter(x -> x.getClassName().equals(cl.getSuperClass().getName())).findFirst();
				if (optSuperclass.isPresent()) {
					superclass = optSuperclass.get();
					addMethods(sf, superclass, importedClasses, objectClass);
				} else {
					try {
						var className = cl.getSuperClass().getName().toString();
						superclass = ASTFactory.createClass(classLoader.loadClass(className));
					} catch (ClassNotFoundException ignored) {}
					// throw new ClassNotFoundException("");
				}
			}

			Iterator<RefTypeOrTPHOrWildcardOrGeneric> paraIt = cl.getSuperClass().getParaList().iterator();
			Iterator<GenericTypeVar> tvarVarIt = superclass.getGenerics().iterator();

			HashMap<String, RefTypeOrTPHOrWildcardOrGeneric> gtvs = new HashMap<>();
			while (paraIt.hasNext()) {
				gtvs.put(tvarVarIt.next().getName(), paraIt.next());
			}

            for (Method m : superclass.getMethods()) {
                if (m.isInherited || Modifier.isStatic(m.modifier)) continue;
				// TODO: Add gtvs from method itself

                ParameterList newParaList = new ParameterList(m.getParameterList().getFormalparalist().stream().map(fp -> fp.withType(fp.getType().acceptTV(new TypeExchanger(gtvs)))).collect(Collectors.toCollection(ArrayList::new)), m.getParameterList().getOffset());
                cl.getMethods().add(new Method(m.modifier, m.name, m.getReturnType().acceptTV(new TypeExchanger(gtvs)), newParaList, m.block,
                        // new GenericDeclarationList(newGenericsList,
                        // ((GenericDeclarationList)m.getGenerics()).getOffset()),
                        (GenericDeclarationList) m.getGenerics(), m.getOffset(), true, false));
            }

		}
		cl.setMethodsAdded();
	}

	private Set<ClassOrInterface> getAvailableClasses(JavaClassName name) throws ClassNotFoundException {
		Set<ClassOrInterface> allClasses = new HashSet<>();
		var clazz = loadJavaTXClass(name);
		if (clazz == null) {
			ClassOrInterface importedClass = ASTFactory.createClass(classLoader.loadClass(name.toString()));
			allClasses.add(importedClass);
		} else {
			allClasses.add(clazz);
		}
		return allClasses;
	}

	public Set<ClassOrInterface> getAvailableClasses(SourceFile forSourceFile) throws ClassNotFoundException {
		// PL 2018-09-18: List durch Set ersetzt, damit die Klassen nur einmal
		// hinzugefuegt werden
		// List<ClassOrInterface> allClasses = new
		// ArrayList<>();//environment.getAllAvailableClasses();
		Set<ClassOrInterface> allClasses = new HashSet<>();

		for (JavaClassName name : forSourceFile.getImports()) {
			allClasses.addAll(getAvailableClasses(name));
		}
		return allClasses;
	}

	/*
	 * public List<ResultSet> typeInferenceOld() throws ClassNotFoundException { List<ClassOrInterface> allClasses = new ArrayList<>();//environment.getAllAvailableClasses(); //Alle Importierten Klassen in allen geparsten Sourcefiles kommen ins FC for(SourceFile sf : this.sourceFiles.values()) { allClasses.addAll(getAvailableClasses(sf)); allClasses.addAll(sf.getClasses()); }
	 *
	 * final ConstraintSet<Pair> cons = getConstraints();
	 *
	 * FiniteClosure finiteClosure = UnifyTypeFactory.generateFC(allClasses); System.out.println(finiteClosure); ConstraintSet<UnifyPair> unifyCons = UnifyTypeFactory.convert(cons);
	 *
	 * TypeUnify unify = new TypeUnify(); Set<Set<UnifyPair>> results = new HashSet<>(); try { File logPath = new File(System.getProperty("user.dir")+"/target/logFiles/"); logPath.mkdirs(); FileWriter logFile = new FileWriter(new File(logPath, "log")); logFile.write("FC:\\" + finiteClosure.toString()+"\n"); for(SourceFile sf : this.sourceFiles.values()) { logFile.write(ASTTypePrinter.print(sf)); } logFile.flush(); Set<List<Constraint<UnifyPair>>> cardProd = unifyCons.cartesianProduct(); for
	 * (List<Constraint<UnifyPair>> xCons : cardProd ){ Set<UnifyPair> xConsSet = new HashSet<>(); for (Constraint<UnifyPair> constraint : xCons) { xConsSet.addAll(constraint); } //.collect(Collectors.toCollection(ArrayList::new)))) System.out.println(xConsSet); Set<String> methodParaTypeVarNames = allClasses.stream().map(x -> x.getMethods().stream().map(y -> y.getParameterList().getFormalparalist() .stream().filter(z -> z.getType() instanceof TypePlaceholder) .map(z ->
	 * ((TypePlaceholder)z.getType()).getName()).collect(Collectors.toCollection( HashSet::new))) .reduce(new HashSet<String>(), (a,b) -> { a.addAll(b); return a;}, (a,b) -> { a.addAll(b); return a;} ) ) .reduce(new HashSet<String>(), (a,b) -> { a.addAll(b); return a;} );
	 *
	 * Set<String> constructorParaTypeVarNames = allClasses.stream().map(x -> x.getConstructors().stream().map(y -> y.getParameterList().getFormalparalist() .stream().filter(z -> z.getType() instanceof TypePlaceholder) .map(z -> ((TypePlaceholder)z.getType()).getName()).collect(Collectors.toCollection( HashSet::new))) .reduce(new HashSet<String>(), (a,b) -> { a.addAll(b); return a;}, (a,b) -> { a.addAll(b); return a;} ) ) .reduce(new HashSet<String>(), (a,b) -> { a.addAll(b); return a;} );
	 *
	 * Set<String> paraTypeVarNames = methodParaTypeVarNames; paraTypeVarNames.addAll(constructorParaTypeVarNames);
	 *
	 * Set<String> returnTypeVarNames = allClasses.stream().map(x -> x.getMethods().stream().filter(y -> y.getReturnType() instanceof TypePlaceholder) .map(z -> ((TypePlaceholder)z.getReturnType()).getName()).collect(Collectors. toCollection(HashSet::new))).reduce((a,b) -> { a.addAll(b); return a;} ).get();
	 *
	 * Set<String> fieldTypeVarNames = allClasses.stream().map(x -> x.getFieldDecl().stream().filter(y -> y.getReturnType() instanceof TypePlaceholder) .map(z -> ((TypePlaceholder)z.getReturnType()).getName()).collect(Collectors. toCollection(HashSet::new))).reduce((a,b) -> { a.addAll(b); return a;} ).get();
	 *
	 * returnTypeVarNames.addAll(fieldTypeVarNames);
	 *
	 * xConsSet = xConsSet.stream().map(x -> { //Hier muss ueberlegt werden, ob //1. alle Argument- und Retuntyp-Variablen in allen UnifyPairs // mit disableWildcardtable() werden. //2. alle Typvariablen mit Argument- oder Retuntyp-Variablen //in Beziehung auch auf disableWildcardtable() gesetzt werden muessen //PL 2018-04-23 if ((x.getLhsType() instanceof PlaceholderType)) { if (paraTypeVarNames.contains(x.getLhsType().getName())) { ((PlaceholderType)x.getLhsType()).setVariance((byte)1);
	 * ((PlaceholderType)x.getLhsType()).disableWildcardtable(); } if (returnTypeVarNames.contains(x.getLhsType().getName())) { ((PlaceholderType)x.getLhsType()).setVariance((byte)-1); ((PlaceholderType)x.getLhsType()).disableWildcardtable(); } } if ((x.getRhsType() instanceof PlaceholderType)) { if (paraTypeVarNames.contains(x.getRhsType().getName())) { ((PlaceholderType)x.getRhsType()).setVariance((byte)1); ((PlaceholderType)x.getRhsType()).disableWildcardtable(); } if
	 * (returnTypeVarNames.contains(x.getRhsType().getName())) { ((PlaceholderType)x.getRhsType()).setVariance((byte)-1); ((PlaceholderType)x.getRhsType()).disableWildcardtable(); } } return x;//HIER DIE JEWEILS RECHT BZW. LINKE SEITE AUF GLEICHE VARIANZ SETZEN WIE DIE JEWEILS ANDERE SEITE }).map( y -> { if ((y.getLhsType() instanceof PlaceholderType) && (y.getRhsType() instanceof PlaceholderType)) { if (((PlaceholderType)y.getLhsType()).getVariance() != 0 &&
	 * ((PlaceholderType)y.getRhsType()).getVariance() == 0) { ((PlaceholderType)y.getRhsType()).setVariance(((PlaceholderType)y.getLhsType( )).getVariance()); } if (((PlaceholderType)y.getLhsType()).getVariance() == 0 && ((PlaceholderType)y.getRhsType()).getVariance() != 0) { ((PlaceholderType)y.getLhsType()).setVariance(((PlaceholderType)y.getRhsType( )).getVariance()); } } return y; } ) .collect(Collectors.toCollection(HashSet::new)); varianceInheritance(xConsSet); Set<Set<UnifyPair>> result =
	 * unify.unifySequential(xConsSet, finiteClosure, logFile, log); //Set<Set<UnifyPair>> result = unify.unify(xConsSet, finiteClosure); System.out.println("RESULT: " + result); logFile.write("RES: " + result.toString()+"\n"); logFile.flush(); results.addAll(result); }
	 *
	 * results = results.stream().map(x -> { Optional<Set<UnifyPair>> res = new RuleSet().subst(x.stream().map(y -> { if (y.getPairOp() == PairOperator.SMALLERDOTWC) y.setPairOp(PairOperator.EQUALSDOT); return y; //alle Paare a <.? b erden durch a =. b ersetzt }).collect(Collectors.toCollection(HashSet::new))); if (res.isPresent()) {//wenn subst ein Erg liefert wurde was veraendert return new TypeUnifyTask().applyTypeUnificationRules(res.get(), finiteClosure); } else return x; //wenn nichts
	 * veraendert wurde wird x zurueckgegeben }).collect(Collectors.toCollection(HashSet::new)); System.out.println("RESULT Final: " + results); logFile.write("RES_FINAL: " + results.toString()+"\n"); logFile.flush(); logFile.write("PLACEHOLDERS: " + PlaceholderType.EXISTING_PLACEHOLDERS); logFile.flush(); } catch (IOException e) { e.printStackTrace(); } return results.stream().map((unifyPairs -> new ResultSet(UnifyTypeFactory.convert(unifyPairs,
	 * generateTPHMap(cons))))).collect(Collectors.toList()); }
	 */
	/**
	 * Vererbt alle Variancen bei Paaren (a <. theta) oder (Theta <. a) wenn a eine Variance !=0 hat auf alle Typvariablen in Theta.
	 *
	 *
	 */
	/*
	 * private void varianceInheritance(Set<UnifyPair> eq) { Set<PlaceholderType> usedTPH = new HashSet<>(); Set<PlaceholderType> phSet = eq.stream().map(x -> { Set<PlaceholderType> pair = new HashSet<>(); if (x.getLhsType() instanceof PlaceholderType) pair.add((PlaceholderType)x.getLhsType()); if (x.getRhsType() instanceof PlaceholderType) pair.add((PlaceholderType)x.getRhsType()); return pair; }).reduce(new HashSet<>(), (a,b) -> { a.addAll(b); return a;} , (c,d) -> { c.addAll(d); return c;});
	 *
	 * ArrayList<PlaceholderType> phSetVariance = new ArrayList<>(phSet); phSetVariance.removeIf(x -> (x.getVariance() == 0)); while(!phSetVariance.isEmpty()) { PlaceholderType a = phSetVariance.remove(0); usedTPH.add(a); //HashMap<PlaceholderType,Integer> ht = new HashMap<>(); //ht.put(a, a.getVariance()); Set<UnifyPair> eq1 = new HashSet<>(eq); eq1.removeIf(x -> !(x.getLhsType() instanceof PlaceholderType && ((PlaceholderType)x.getLhsType()).equals(a))); eq1.stream().forEach(x -> {
	 * x.getRhsType().accept(new distributeVariance(), a.getVariance());}); eq1 = new HashSet<>(eq); eq1.removeIf(x -> !(x.getRhsType() instanceof PlaceholderType && ((PlaceholderType)x.getRhsType()).equals(a))); eq1.stream().forEach(x -> { x.getLhsType().accept(new distributeVariance(), a.getVariance());}); phSetVariance = new ArrayList<>(phSet); phSetVariance.removeIf(x -> (x.getVariance() == 0 || usedTPH.contains(x))); } }
	 */

	public UnifyResultModel typeInferenceAsync(UnifyResultListener resultListener, Writer logFile) throws ClassNotFoundException, IOException {
		List<ClassOrInterface> allClasses = new ArrayList<>();// environment.getAllAvailableClasses();
		// Alle Importierten Klassen in allen geparsten Sourcefiles kommen ins FC
		for (Entry<File, SourceFile> source : this.sourceFiles.entrySet()) {
			SourceFile sf = source.getValue();
			allClasses.addAll(getAvailableClasses(sf));
			allClasses.addAll(sf.getClasses());
			allClasses.addAll(CompilationEnvironment.loadDefaultPackageClasses(sf.getPkgName(), source.getKey(), this).stream().map(ASTFactory::createClass).collect(Collectors.toList()));
		}

		final ConstraintSet<Pair> cons = new ConstraintSet<>();
		for (var f : this.sourceFiles.keySet()) {
			cons.addAll(getConstraints(f));
		}

		Set<Set<UnifyPair>> results = new HashSet<>();
		UnifyResultModel urm = null;
		// urm.addUnifyResultListener(resultListener);
		try {
			logFile = logFile == null ? new FileWriter(new File("log_" + sourceFiles.keySet().iterator().next().getName())) : logFile;
			IFiniteClosure finiteClosure = UnifyTypeFactory.generateFC(allClasses, logFile, getClassLoader(), this);
			System.out.println(finiteClosure);
			urm = new UnifyResultModel(cons, finiteClosure);
			urm.addUnifyResultListener(resultListener);
			ConstraintSet<UnifyPair> unifyCons = UnifyTypeFactory.convert(this, cons);

			Function<UnifyPair, UnifyPair> distributeInnerVars = x -> {
				UnifyType lhs, rhs;
				if (((lhs = x.getLhsType()) instanceof PlaceholderType) && ((rhs = x.getRhsType()) instanceof PlaceholderType) && (((PlaceholderType) lhs).isInnerType() || ((PlaceholderType) rhs).isInnerType())) {
					((PlaceholderType) lhs).setInnerType(true);
					((PlaceholderType) rhs).setInnerType(true);
				}
				return x;

			};
			logFile.write(unifyCons.toString());
			unifyCons = unifyCons.map(distributeInnerVars);
			logFile.write(unifyCons.toString());
			TypeUnify unify = new TypeUnify();
			// Set<Set<UnifyPair>> results = new HashSet<>(); Nach vorne gezogen
			logFile.write("FC:\\" + finiteClosure.toString() + "\n");
			for (SourceFile f : this.sourceFiles.values()) {
				logFile.write(ASTTypePrinter.print(f));
			}
			logFile.flush();
			Set<PlaceholderType> varianceTPHold;
			Set<PlaceholderType> varianceTPH = new HashSet<>();
			varianceTPH = varianceInheritanceConstraintSet(unifyCons);

			/*
			 * PL 2018-11-07 wird in varianceInheritanceConstraintSet erledigt do { //PL 2018-11-05 Huellenbildung Variance auf alle TPHs der Terme auf der jeweiligen //anderen Seite übertragen varianceTPHold = new HashSet<>(varianceTPH); varianceTPH = varianceInheritanceConstraintSet(unifyCons); unifyCons.map( y -> { if ((y.getLhsType() instanceof PlaceholderType) && (y.getRhsType() instanceof PlaceholderType)) { if (((PlaceholderType)y.getLhsType()).getVariance() != 0 &&
			 * ((PlaceholderType)y.getRhsType()).getVariance() == 0) { ((PlaceholderType)y.getRhsType()).setVariance(((PlaceholderType)y.getLhsType( )).getVariance()); } if (((PlaceholderType)y.getLhsType()).getVariance() == 0 && ((PlaceholderType)y.getRhsType()).getVariance() != 0) { ((PlaceholderType)y.getLhsType()).setVariance(((PlaceholderType)y.getRhsType( )).getVariance()); } } return y; } ); } while (!varianceTPHold.equals(varianceTPH));
			 */

			// Set<Set<UnifyPair>> result = unify.unifySequential(xConsSet, finiteClosure,
			// logFile, log);
			// Set<Set<UnifyPair>> result = unify.unify(xConsSet, finiteClosure);
			List<Set<Constraint<UnifyPair>>> oderConstraints = unifyCons.getOderConstraints()/*
																								 * .stream().map(x -> { Set<Set<UnifyPair>> ret = new HashSet<>(); for (Constraint<UnifyPair> y : x) { ret.add(new HashSet<>(y)); } return ret; }).collect(Collectors. toCollection(ArrayList::new))
																								 */;
			unify.unifyAsync(unifyCons.getUndConstraints(), oderConstraints, finiteClosure, logFile, log, urm, usedTasks);
		} catch (IOException e) {
			System.err.println("kein LogFile");
		}
		return urm;
	}

	public List<ResultSet> typeInference(File file) throws ClassNotFoundException, IOException {
		var sf = sourceFiles.get(file);
		Set<ClassOrInterface> allClasses = new HashSet<>();// environment.getAllAvailableClasses();
		allClasses.addAll(getAvailableClasses(sf));
		allClasses.addAll(sf.getClasses());
		var newClasses = CompilationEnvironment.loadDefaultPackageClasses(sf.getPkgName(), file, this).stream().map(ASTFactory::createClass).collect(Collectors.toSet());
		for (var clazz : newClasses) {
			// Don't load classes that get recompiled
			if (sf.getClasses().stream().anyMatch(nf -> nf.getClassName().equals(clazz.getClassName())))
				continue;
			if (allClasses.stream().noneMatch(old -> old.getClassName().equals(clazz.getClassName())))
				allClasses.add(clazz);
		}

		final ConstraintSet<Pair> cons = getConstraints(file);
		Set<Set<UnifyPair>> results = new HashSet<>();
		try {
			var logFolder = new File(System.getProperty("user.dir") + "/logFiles/");
			if (log) logFolder.mkdirs();
			Writer logFile = log ? new FileWriter(new File(logFolder, "log_" + sourceFiles.keySet().iterator().next().getName())) : new OutputStreamWriter(new NullOutputStream());
			IFiniteClosure finiteClosure = UnifyTypeFactory.generateFC(allClasses.stream().toList(), logFile, classLoader, this);
			System.out.println(finiteClosure);
			ConstraintSet<UnifyPair> unifyCons = UnifyTypeFactory.convert(this, cons);
			System.out.println("xxx1");
			Function<UnifyPair, UnifyPair> distributeInnerVars = x -> {
				UnifyType lhs, rhs;
				if (((lhs = x.getLhsType()) instanceof PlaceholderType) && ((rhs = x.getRhsType()) instanceof PlaceholderType) && (((PlaceholderType) lhs).isInnerType() || ((PlaceholderType) rhs).isInnerType())) {
					((PlaceholderType) lhs).setInnerType(true);
					((PlaceholderType) rhs).setInnerType(true);
				}
				return x;

			};

			logFile.write("Unify:" + unifyCons.toString());
			System.out.println("Unify:" + unifyCons.toString());
			unifyCons = unifyCons.map(distributeInnerVars);
			logFile.write("\nUnify_distributeInnerVars: " + unifyCons.toString());
			TypeUnify unify = new TypeUnify();
			// Set<Set<UnifyPair>> results = new HashSet<>(); Nach vorne gezogen
			logFile.write("FC:\\" + finiteClosure.toString() + "\n");
			logFile.write(ASTTypePrinter.print(sf));
			System.out.println(ASTTypePrinter.print(sf));
			logFile.flush();
			List<UnifyPair> andConstraintsSorted = unifyCons.getUndConstraints().stream()
					.sorted(Comparator.comparing(UnifyPair::getPairOp).thenComparing(UnifyPair::getLhsType, Comparator.comparing(UnifyType::getName)))
					.collect(Collectors.toList());

			System.out.println(andConstraintsSorted);

			Set<PlaceholderType> varianceTPHold;
			Set<PlaceholderType> varianceTPH = new HashSet<>();
			varianceTPH = varianceInheritanceConstraintSet(unifyCons);

			/*
			 * PL 2018-11-07 wird in varianceInheritanceConstraintSet erledigt do { //PL 2018-11-05 Huellenbildung Variance auf alle TPHs der Terme auf der jeweiligen //anderen Seite übertragen varianceTPHold = new HashSet<>(varianceTPH); varianceTPH = varianceInheritanceConstraintSet(unifyCons); unifyCons.map( y -> { if ((y.getLhsType() instanceof PlaceholderType) && (y.getRhsType() instanceof PlaceholderType)) { if (((PlaceholderType)y.getLhsType()).getVariance() != 0 &&
			 * ((PlaceholderType)y.getRhsType()).getVariance() == 0) { ((PlaceholderType)y.getRhsType()).setVariance(((PlaceholderType)y.getLhsType( )).getVariance()); } if (((PlaceholderType)y.getLhsType()).getVariance() == 0 && ((PlaceholderType)y.getRhsType()).getVariance() != 0) { ((PlaceholderType)y.getLhsType()).setVariance(((PlaceholderType)y.getRhsType( )).getVariance()); } } return y; } ); } while (!varianceTPHold.equals(varianceTPH));
			 */

			// Set<Set<UnifyPair>> result = unify.unifySequential(xConsSet, finiteClosure,
			// logFile, log);
			// Set<Set<UnifyPair>> result = unify.unify(xConsSet, finiteClosure);
			List<Set<Constraint<UnifyPair>>> oderConstraints = unifyCons.getOderConstraints()// .stream().map(x -> {
			/*
			 * Set<Set<UnifyPair>> ret = new HashSet<>(); for (Constraint<UnifyPair> y : x) { ret.add(new HashSet<>(y)); } return ret; }).collect(Collectors.toCollection(ArrayList::new))
			 */;
			if (resultmodel) {
				/* UnifyResultModel Anfang */
				UnifyResultModel urm = new UnifyResultModel(cons, finiteClosure);
				UnifyResultListenerImpl li = new UnifyResultListenerImpl();
				urm.addUnifyResultListener(li);
				unify.unifyParallel(unifyCons.getUndConstraints(), oderConstraints, finiteClosure, logFile, log, urm, usedTasks);
				//System.out.println("RESULT Final: " + li.getResults());
				var finalResults = li.getResults().stream().sorted().toList();
				int i = 0;
				System.out.println("RESULT Final: ");
				for (var result : finalResults){
					System.out.println("Result: " + i++);
					System.out.println(result.getSortedResults());
				}
				System.out.println("Constraints for Generated Generics: " + " ???");
				logFile.write("RES_FINAL: " + li.getResults().toString() + "\n");
				logFile.flush();
				return li.getResults();
			}
			/* UnifyResultModel End */
			else {
				// Set<Set<UnifyPair>> result = unify.unify(unifyCons.getUndConstraints(),
				// oderConstraints, finiteClosure, logFile, log, new UnifyResultModel(cons,
				// finiteClosure));
				Set<Set<UnifyPair>> result = unify.unifyOderConstraints(unifyCons.getUndConstraints(), oderConstraints, finiteClosure, logFile, log, new UnifyResultModel(cons, finiteClosure), usedTasks);
				System.out.println("RESULT: " + result);
				logFile.write("RES: " + result.toString() + "\n");
				logFile.flush();
				results.addAll(result);

				results = results.stream().map(x -> {
					Optional<Set<UnifyPair>> res = new RuleSet().subst(x.stream().map(y -> {
						if (y.getPairOp() == PairOperator.SMALLERDOTWC)
							y.setPairOp(PairOperator.EQUALSDOT);
						return y; // alle Paare a <.? b erden durch a =. b ersetzt
					}).collect(Collectors.toCollection(HashSet::new)));
					if (res.isPresent()) {// wenn subst ein Erg liefert wurde was veraendert
						return new TypeUnifyTask().applyTypeUnificationRules(res.get(), finiteClosure);
					} else
						return x; // wenn nichts veraendert wurde wird x zurueckgegeben
				}).collect(Collectors.toCollection(HashSet::new));
				System.out.println("RESULT Final: " + results);
				System.out.println("Constraints for Generated Generics: " + " ???");
				logFile.write("RES_FINAL: " + results.toString() + "\n");
				logFile.flush();
				logFile.write("PLACEHOLDERS: " + PlaceholderType.EXISTING_PLACEHOLDERS);
				logFile.flush();
			}
		} catch (IOException e) {
			System.err.println("kein LogFile");
		}
		return results.stream().map((unifyPairs -> new ResultSet(UnifyTypeFactory.convert(unifyPairs, Pair.generateTPHMap(cons))))).collect(Collectors.toList());
	}

	/**
	 * TEMPORARY - Only for Language Server Usage
	 */
	public LanguageServerTransferObject getResultSetAndAbstractSyntax(File file) throws IOException, ClassNotFoundException {
		var sf = sourceFiles.get(file);
		if(sf == null){
			sf = sourceFiles.values().stream().findFirst().get();
		}
		Set<ClassOrInterface> allClasses = new HashSet<>();
		allClasses.addAll(getAvailableClasses(sf));
		allClasses.addAll(sf.getClasses());
		var newClasses = CompilationEnvironment.loadDefaultPackageClasses(sf.getPkgName(), file, this).stream().map(ASTFactory::createClass).collect(Collectors.toSet());
		for (var clazz : newClasses) {
			// Don't load classes that get recompiled
			if (sf.getClasses().stream().anyMatch(nf -> nf.getClassName().equals(clazz.getClassName())))
				continue;
			if (allClasses.stream().noneMatch(old -> old.getClassName().equals(clazz.getClassName())))
				allClasses.add(clazz);
		}

		final ConstraintSet<Pair> cons = getConstraints(file);
		Set<Set<UnifyPair>> results = new HashSet<>();
		try {
			Writer logFile = new OutputStreamWriter(new NullOutputStream());
			IFiniteClosure finiteClosure = UnifyTypeFactory.generateFC(allClasses.stream().toList(), logFile, classLoader, this);
			ConstraintSet<UnifyPair> unifyCons = UnifyTypeFactory.convert(this, cons);
			Function<UnifyPair, UnifyPair> distributeInnerVars = x -> {
				UnifyType lhs, rhs;
				if (((lhs = x.getLhsType()) instanceof PlaceholderType) && ((rhs = x.getRhsType()) instanceof PlaceholderType) && (((PlaceholderType) lhs).isInnerType() || ((PlaceholderType) rhs).isInnerType())) {
					((PlaceholderType) lhs).setInnerType(true);
					((PlaceholderType) rhs).setInnerType(true);
				}
				return x;

			};


			unifyCons = unifyCons.map(distributeInnerVars);
			TypeUnify unify = new TypeUnify();
			Set<PlaceholderType> varianceTPHold;
			Set<PlaceholderType> varianceTPH = new HashSet<>();
			varianceTPH = varianceInheritanceConstraintSet(unifyCons);

			List<Set<Constraint<UnifyPair>>> oderConstraints = unifyCons.getOderConstraints();

			if (resultmodel) {
				/* UnifyResultModel Anfang */
				UnifyResultModel urm = new UnifyResultModel(cons, finiteClosure);
				UnifyResultListenerImpl li = new UnifyResultListenerImpl();
				urm.addUnifyResultListener(li);
				unify.unifyParallel(unifyCons.getUndConstraints(), oderConstraints, finiteClosure, logFile, log, urm, usedTasks);
				generateBytecode(sf, li.getResults());
				return new LanguageServerTransferObject(li.getResults(), sf, ASTTypePrinter.print(sf), generatedGenerics);
			}
			/* UnifyResultModel End */
			else {
				Set<Set<UnifyPair>> result = unify.unifyOderConstraints(unifyCons.getUndConstraints(), oderConstraints, finiteClosure, logFile, log, new UnifyResultModel(cons, finiteClosure), usedTasks);
				results.addAll(result);

				results = results.stream().map(x -> {
					Optional<Set<UnifyPair>> res = new RuleSet().subst(x.stream().map(y -> {
						if (y.getPairOp() == PairOperator.SMALLERDOTWC)
							y.setPairOp(PairOperator.EQUALSDOT);
						return y; // alle Paare a <.? b erden durch a =. b ersetzt
					}).collect(Collectors.toCollection(HashSet::new)));
					if (res.isPresent()) {// wenn subst ein Erg liefert wurde was veraendert
						return new TypeUnifyTask().applyTypeUnificationRules(res.get(), finiteClosure);
					} else
						return x; // wenn nichts veraendert wurde wird x zurueckgegeben
				}).collect(Collectors.toCollection(HashSet::new));
			}
		} catch (ClassNotFoundException e) {
		}
		generateBytecode(sf, results.stream().map((unifyPairs -> new ResultSet(UnifyTypeFactory.convert(unifyPairs, Pair.generateTPHMap(cons))))).collect(Collectors.toList()));
		return new LanguageServerTransferObject(results.stream().map((unifyPairs -> new ResultSet(UnifyTypeFactory.convert(unifyPairs, Pair.generateTPHMap(cons))))).collect(Collectors.toList()), sf, ASTTypePrinter.print(sf), generatedGenerics);
	}



	/**
	 * Vererbt alle Variancen bei Paaren (a <. theta) oder (Theta <. a) wenn a eine Variance !=0 hat auf alle Typvariablen in Theta.
	 * 
	 *
	 */
	private Set<PlaceholderType> varianceInheritanceConstraintSet(ConstraintSet<UnifyPair> cons) {
		Set<UnifyPair> eq = cons.getAll();
		Set<PlaceholderType> usedTPH = new HashSet<>();
		Set<PlaceholderType> phSet = eq.stream().map(x -> {
			Set<PlaceholderType> pair = new HashSet<>();
			if (x.getLhsType() instanceof PlaceholderType)
				pair.add((PlaceholderType) x.getLhsType());
			if (x.getRhsType() instanceof PlaceholderType)
				pair.add((PlaceholderType) x.getRhsType());
			return pair;
		}).reduce(new HashSet<>(), (a, b) -> {
			a.addAll(b);
			return a;
		}, (c, d) -> {
			c.addAll(d);
			return c;
		});

		ArrayList<PlaceholderType> phSetVariance = new ArrayList<>(phSet);
		phSetVariance.removeIf(x -> (x.getVariance() == 0));
		while (!phSetVariance.isEmpty()) {
			PlaceholderType a = phSetVariance.remove(0);
			usedTPH.add(a);
			// HashMap<PlaceholderType,Integer> ht = new HashMap<>();
			// ht.put(a, a.getVariance());
			// ConstraintSet<UnifyPair> eq1 = cons;
			// eq1.removeIf(x -> !(x.getLhsType() instanceof PlaceholderType &&
			// ((PlaceholderType)x.getLhsType()).equals(a)));
			// durch if-Abfrage im foreach geloest
			cons.forEach(x -> {
				if (x.getLhsType() instanceof PlaceholderType && ((PlaceholderType) x.getLhsType()).equals(a)) {
					x.getRhsType().accept(new distributeVariance(), a.getVariance());
				}
			});
			// ` eq1 = new HashSet<>(eq);
			// eq1.removeIf(x -> !(x.getRhsType() instanceof PlaceholderType &&
			// ((PlaceholderType)x.getRhsType()).equals(a)));
			// durch if-Abfrage im foreach geloest
			cons.forEach(x -> {
				if (x.getRhsType() instanceof PlaceholderType && ((PlaceholderType) x.getRhsType()).equals(a)) {
					x.getLhsType().accept(new distributeVariance(), a.getVariance());
				}
			});
			phSetVariance = new ArrayList<>(phSet); // macht vermutlich keinen Sinn PL 2018-10-18, doch, es koennen neue
			// TPHs mit Variancen dazugekommen sein PL 2018-11-07
			phSetVariance.removeIf(x -> (x.getVariance() == 0 || usedTPH.contains(x)));
		}
		return usedTPH;
	}

	public final JavaClassRegistry classRegistry = new JavaClassRegistry();

	public record ClassEntry(File classFile, ClassOrInterface cif) {}

	public final Map<JavaClassName, ClassEntry> loadedClasses = new HashMap<>();

	private SourceFile parse(File sourceFile) throws IOException, java.lang.ClassNotFoundException {
		if (sourceFiles.containsKey(sourceFile)) return sourceFiles.get(sourceFile);
		SourceFileContext tree = JavaTXParser.parse(sourceFile);
		environment.addClassesToRegistry(classRegistry, tree, sourceFile, this);
		SyntaxTreeGenerator generator = new SyntaxTreeGenerator(this, classRegistry, new GenericsRegistry(null), sourceFile.getName());
		var classes = new ArrayList<ClassOrInterface>();
		var sf = new SourceFile("", classes, generator.imports);
		addSourceFile(sourceFile, sf);
		generator.convert(classes, tree, environment.packageCrawler);
		sf.setPackageName(generator.pkgName);
		sf.imports.addAll(generator.imports);
		return sf;
	}

	/**
	 * When an import tries to import a JavaTX class it first looks it up in the cache and
	 * if it doesn't exist it's going to compile it and add it to the source files list
	 * @param name
	 */
	public ClassOrInterface loadJavaTXClass(JavaClassName name) {
		var file = findFileForClass(name);
		if (file != null) {
			if (loadedClasses.containsKey(name)) return loadedClasses.get(name).cif();
			try {
				var tree = JavaTXParser.parse(file);
				classRegistry.addName(name.toString(), 0); // TODO This gets overwritten later, is it bad if we don't know this right away?
				environment.addClassesToRegistry(classRegistry, tree, file, this);
				SyntaxTreeGenerator generator = new SyntaxTreeGenerator(this, classRegistry, new GenericsRegistry(null), file.getName());
				var classes = new ArrayList<ClassOrInterface>();
				var sf = new SourceFile("", classes, generator.imports);
				addSourceFile(file, sf);
				generator.convert(classes, tree, environment.packageCrawler);
				sf.setPackageName(generator.pkgName);
				var classFiles = generateBytecode(file);

				sf.setGenerated();
				writeClassFile(classFiles, outputPath != null ? outputPath : new File("."), false);
				var clazz = classLoader.loadClass(name.toString());
				var classOrInterface = ASTFactory.createClass(clazz);
				loadedClasses.put(name, new ClassEntry(new File(outputPath, clazz.getName() + ".class"), classOrInterface));
				return classOrInterface;
			} catch (Exception e) {
				throw new RuntimeException(e);
			}
		}
		return null;
	}

	public File findFileForClass(JavaClassName name) {
		var packageName = name.getPackageName();
		var className = name.getClassName().split("\\.")[0];
		for (var cp : classPath) {
			var file = new File(cp, packageName.replaceAll("\\.", "/") + "/" + className + ".jav");
			if (file.exists()) return file;
		}
		return null;
	}

	public void generateBytecode() throws ClassNotFoundException, IOException {
		for (var file : sourceFiles.keySet()) {
			var sf = sourceFiles.get(file);
			if (sf.isGenerated()) continue;
			var classes = generateBytecode(file);
			sf.setGenerated();
			writeClassFile(classes, outputPath == null ? file.getParentFile() : outputPath, outputPath == null);
		}
	}

	/**
	 * @param path - output-Directory can be null, then class file output is in the same directory as the parsed source files
	 * @return
	 */
	public Map<JavaClassName, byte[]> generateBytecode(File sourceFile) throws ClassNotFoundException, IOException {
		var sf = sourceFiles.get(sourceFile);
		if (sf.isGenerated()) return null;
		List<ResultSet> typeinferenceResult = this.typeInference(sourceFile);
		var classes = generateBytecode(sf, typeinferenceResult);
		sf.setGenerated();
		return classes;
	}

	private Map<SourceFile, List<GenericsResult>> generatedGenerics = new HashMap<>();

	public Map<SourceFile, List<GenericsResult>> getGeneratedGenerics() {
		return generatedGenerics;
	}

	/**
	 * @param outputPath          - can be null, then class file output is in the same directory as the parsed source files
	 * @param typeinferenceResult
	 * @throws IOException
	 */
	public void generateBytecode(File outputPath, List<ResultSet> typeinferenceResult) throws IOException {
		for (File f : sourceFiles.keySet()) {
			HashMap<JavaClassName, byte[]> classFiles = new HashMap<>();
			SourceFile sf = sourceFiles.get(f);
			File path = outputPath;
			if (outputPath == null) {
				path = f.getParentFile(); // Set path to path of the parsed .jav file
			}

			var generatedClasses = generateBytecode(sf, typeinferenceResult);
			writeClassFile(generatedClasses, path, outputPath == null);
		}
	}

	public synchronized Map<JavaClassName, byte[]> generateBytecode(SourceFile sf, List<ResultSet> typeInferenceResult) {
		var converter = new ASTToTargetAST(this, typeInferenceResult, sf, classLoader);
		var generatedClasses = new HashMap<JavaClassName, byte[]>();
		for (var clazz : sf.getClasses()) {
			var codegen = new Codegen(converter.convert(clazz), this, converter);
			var code = codegen.generate();
			generatedClasses.put(clazz.getClassName(), code);
		}
		generatedGenerics.put(sf, converter.javaGenerics());
		converter.generateFunNTypes();
		auxiliaries.forEach((name, source) -> {
			generatedClasses.put(new JavaClassName(name), source);
		});
		return generatedClasses;
	}

	public synchronized void writeClassFile(Map<JavaClassName, byte[]> classFiles, File path, boolean preserveHierarchy) throws IOException {
		FileOutputStream output;
		for (JavaClassName name : classFiles.keySet()) {
			byte[] bytecode = classFiles.get(name);
			System.out.println("generating " + name + ".class file ...");
			var subPath = preserveHierarchy ? path : Path.of(path.toString(), name.getPackageName().split("\\.")).toFile();
			File outputFile = new File(subPath, name.getClassName() + ".class");
			outputFile.getAbsoluteFile().getParentFile().mkdirs();
			System.out.println(outputFile);
			output = new FileOutputStream(outputFile);
			output.write(bytecode);
			output.close();
			System.out.println(name + ".class file generated");
		}
	}

	/* PL 2020-03-17 mit TypeExchanger in FCGenerator.java zusammenfuehren */
	/**
	 * Tauscht die GTVs in einem Typ gegen die entsprechenden Typen in der übergebenen Map aus.
	 */
	private static class TypeExchanger implements TypeVisitor<RefTypeOrTPHOrWildcardOrGeneric> {

		private final HashMap<String, RefTypeOrTPHOrWildcardOrGeneric> gtvs;

		TypeExchanger(HashMap<String, RefTypeOrTPHOrWildcardOrGeneric> gtvs) {
			this.gtvs = gtvs;
		}

		@Override
		public RefTypeOrTPHOrWildcardOrGeneric visit(RefType refType) {
			List<RefTypeOrTPHOrWildcardOrGeneric> params = new ArrayList<>();
			for (RefTypeOrTPHOrWildcardOrGeneric param : refType.getParaList()) {
				params.add(param.acceptTV(this));
			}
			RefTypeOrTPHOrWildcardOrGeneric ret = new RefType(refType.getName(), params, new NullToken());
			return ret;
		}

		@Override
		public RefTypeOrTPHOrWildcardOrGeneric visit(SuperWildcardType superWildcardType) {
			SuperWildcardType ret = new SuperWildcardType(superWildcardType.getInnerType().acceptTV(this), superWildcardType.getOffset());
			return ret;
		}

		@Override
		public RefTypeOrTPHOrWildcardOrGeneric visit(TypePlaceholder typePlaceholder) {
			return typePlaceholder; // TypePlaceholder der vererbert wird kann bei der Vererbung nicht instanziert
									// werden.
		}

		@Override
		public RefTypeOrTPHOrWildcardOrGeneric visit(ExtendsWildcardType extendsWildcardType) {
			ExtendsWildcardType ret = new ExtendsWildcardType(extendsWildcardType.getInnerType().acceptTV(this), extendsWildcardType.getOffset());
			return ret;
		}

		@Override
		public RefTypeOrTPHOrWildcardOrGeneric visit(GenericRefType genericRefType) {
			if (!gtvs.containsKey(genericRefType.getParsedName()))
				throw new DebugException("Dieser Fall darf nicht auftreten");
			return gtvs.get(genericRefType.getParsedName());
		}

	}

}
