/**
 * 
 */
package de.tu_dresden.lat.proofs.data;

import java.io.File;
import java.io.IOException;
import java.lang.reflect.Constructor;
import java.nio.file.Files;
import java.nio.file.Path;
import java.nio.file.Paths;
import java.util.List;
import java.util.stream.Collectors;

import org.semanticweb.owlapi.apibinding.OWLManager;
import org.semanticweb.owlapi.model.AsOWLClass;
import org.semanticweb.owlapi.model.OWLAxiomVisitorEx;
import org.semanticweb.owlapi.model.OWLClass;
import org.semanticweb.owlapi.model.OWLEquivalentClassesAxiom;
import org.semanticweb.owlapi.model.OWLOntology;
import org.semanticweb.owlapi.model.OWLOntologyCreationException;
import org.semanticweb.owlapi.model.OWLOntologyManager;
import org.semanticweb.owlapi.model.OWLSubClassOfAxiom;

import de.tu_dresden.lat.proofs.interfaces.IInference;
import de.tu_dresden.lat.proofs.interfaces.IProof;
import de.tu_dresden.lat.proofs.interfaces.IProofGenerator;
import de.tu_dresden.lat.proofs.json.JsonProofParser;
import de.tu_dresden.lat.proofs.json.JsonProofWriter;

/**
 * @author stefborg
 *
 */
public class ProofGeneratorMain {

	public static void main(String[] args) throws Exception {

		if (args.length != 3) {
			System.err.println("3 arguments expected: class name, input file prefix, output file prefix");
			return;
		}
		String className = args[0];
		String inputFilePrefix = args[1];
		String outputFilePrefix = args[2];

		IProofGenerator generator = getGenerator(className);

		IInference task = loadTask(inputFilePrefix);
		try {
			long start = System.nanoTime();
			IProof proof = generateProof(generator, task);
			long end = System.nanoTime();
			double seconds = ((double) (end - start)) / 1e9;
			System.out.println(String.format("%.1f seconds", seconds));
			writeProof(proof, outputFilePrefix);
		} catch (RuntimeException | AssertionError e) {
			e.printStackTrace();
			Path p = Paths.get(outputFilePrefix + JsonProofWriter.FILE_ENDING);
			Files.deleteIfExists(p);
			Files.createFile(p);
		}
	}

	private static IProofGenerator getGenerator(String className) throws Exception {
		Class<?> generatorClass = Class.forName(className);
		if (!IProofGenerator.class.isAssignableFrom(generatorClass)) {
			throw new IllegalStateException("The specified class does not implement the IProofGenerator interface!");
		}
		Constructor<?> constructor = generatorClass.getConstructor();
		return (IProofGenerator) constructor.newInstance();
	}

	private static IInference loadTask(String filePrefix) throws IOException {
		return JsonProofParser.getInstance().fromFile(new File(filePrefix + JsonProofWriter.FILE_ENDING))
				.getInferences().get(0);
	}

	private static IProof generateProof(IProofGenerator generator, IInference task)
			throws OWLOntologyCreationException {
		OWLOntologyManager manager = OWLManager.createOWLOntologyManager();
		OWLOntology ontology = manager.createOntology();
		manager.addAxioms(ontology, task.getPremises().stream());
		generator.setOntology(ontology);

		return task.getConclusion().accept(new OWLAxiomVisitorEx<IProof>() {
			@Override
			public IProof visit(OWLSubClassOfAxiom axiom) {
				if (!axiom.getSubClass().isOWLClass() || !axiom.getSuperClass().isOWLClass()) {
					throw new IllegalArgumentException("Subsumptions should be between two concept names.\n" + axiom);
				}
				return generator.proveSubsumption(axiom.getSubClass().asOWLClass(), axiom.getSuperClass().asOWLClass());
			}

			@Override
			public IProof visit(OWLEquivalentClassesAxiom axiom) {
				List<OWLClass> list = axiom.classExpressions().filter(AsOWLClass::isOWLClass)
						.map(AsOWLClass::asOWLClass).collect(Collectors.toList());
				if (list.size() != 2) {
					throw new IllegalArgumentException("Equivalences should be between two concept names.\n" + axiom);
				}
				return generator.proveEquivalence(list.get(0), list.get(1));
			}

			@Override
			public <T> IProof doDefault(T object) {
				throw new IllegalArgumentException(
						"Can only prove subsumptions and equivalences between concept names.");
			}
		});
	}

	private static void writeProof(IProof proof, String filePrefix) throws IOException {
		JsonProofWriter.getInstance().writeToFile(proof, filePrefix);
	}

}
