package de.tu_dresden.lat.proofs;

import static org.junit.Assert.assertEquals;

import java.io.IOException;
import java.util.Arrays;
import java.util.LinkedList;

import org.junit.Test;
import org.semanticweb.owlapi.apibinding.OWLManager;
import org.semanticweb.owlapi.model.IRI;
import org.semanticweb.owlapi.model.OWLAxiom;
import org.semanticweb.owlapi.model.OWLClass;
import org.semanticweb.owlapi.model.OWLDataFactory;
import org.semanticweb.owlapi.model.OWLObjectProperty;
import org.semanticweb.owlapi.model.OWLObjectSomeValuesFrom;
import org.semanticweb.owlapi.model.OWLOntologyManager;
import org.semanticweb.owlapi.model.OWLSubClassOfAxiom;

import com.fasterxml.jackson.core.JsonGenerationException;
import com.fasterxml.jackson.databind.JsonMappingException;

import de.tu_dresden.lat.proofs.data.FormattingException;
import de.tu_dresden.lat.proofs.data.Inference;
import de.tu_dresden.lat.proofs.data.ParsingException;
import de.tu_dresden.lat.proofs.data.Proof;
import de.tu_dresden.lat.proofs.interfaces.IProof;
import de.tu_dresden.lat.proofs.json.JsonProofParser;
import de.tu_dresden.lat.proofs.json.JsonProofWriter;

/**
 * @author Christian Alrabbaa
 *
 */
public class JsonProofReadingAndWritingTest {

	private static final OWLOntologyManager manager = OWLManager.createOWLOntologyManager();
	private static final OWLDataFactory factory = manager.getOWLDataFactory();

	@Test

	public void JSonProofWriterTest1()
			throws JsonGenerationException, JsonMappingException, IOException, FormattingException, ParsingException {

		OWLClass a = factory.getOWLClass(IRI.create("A"));
		OWLClass b = factory.getOWLClass(IRI.create("B"));
		OWLClass c = factory.getOWLClass(IRI.create("C"));
		OWLClass d = factory.getOWLClass(IRI.create("D"));

		OWLObjectProperty r = factory.getOWLObjectProperty(IRI.create("r"));

		OWLObjectSomeValuesFrom existsRB = factory.getOWLObjectSomeValuesFrom(r, b);
		OWLObjectSomeValuesFrom existsRC = factory.getOWLObjectSomeValuesFrom(r, c);

		OWLSubClassOfAxiom aInExistsrB = factory.getOWLSubClassOfAxiom(a, existsRB);
		OWLSubClassOfAxiom bInC = factory.getOWLSubClassOfAxiom(b, c);
		OWLSubClassOfAxiom dInA = factory.getOWLSubClassOfAxiom(d, a);

		Inference prem1 = new Inference(aInExistsrB, "Asserted", new LinkedList<>());
		Inference prem2 = new Inference(bInC, "Asserted", new LinkedList<>());
		Inference prem3 = new Inference(dInA, "Asserted", new LinkedList<>());

		OWLAxiom con1 = factory.getOWLSubClassOfAxiom(a, existsRC);
		OWLAxiom con2 = factory.getOWLSubClassOfAxiom(d, existsRC);

		Inference inner = new Inference(con1, "rule 1", Arrays.asList(aInExistsrB, bInC));
		Inference outer = new Inference(con2, "rule 2", Arrays.asList(dInA, con1));

		IProof proof = new Proof(con2);
		proof.addInference(outer);
		proof.addInference(prem3);
		proof.addInference(inner);
		proof.addInference(prem1);
		proof.addInference(prem2);

		JsonProofWriter writer = JsonProofWriter.getInstance();

		String formatted = writer.toString(proof);

		System.out.println(formatted);

		JsonProofParser parser = new JsonProofParser();

		IProof parsed = parser.parseProof(formatted);

		assertEquals(proof, parsed);
	}

}
