import java.io.File

import de.tu_dresden.lat.forgettingBasedProofs.{FameBasedProofGenerator, ForgettingBasedProofGenerator, LetheBasedALCHProofGenerator, LetheBasedALCHProofGeneratorSkippingSteps}
import de.tu_dresden.lat.forgettingBasedProofs.adaptors.{LetheBasedForgetter, OWLApiBasedJustifier}
import de.tu_dresden.lat.proofs.interfaces.IProofGenerator
import de.tu_dresden.lat.proofs.json.JsonProofParser
import org.eclipse.rdf4j.model.vocabulary.OWL
import org.semanticweb.HermiT.ReasonerFactory
import org.semanticweb.owlapi.apibinding.OWLManager
import org.semanticweb.owlapi.model.{OWLClass, OWLEquivalentClassesAxiom, OWLSubClassOfAxiom}

import scala.collection.JavaConverters._

object ExampleFileTest {
  def main(args: Array[String]) = {
    val dir = new File(
      getClass()
        .getClassLoader()
        .getResource("justificationProofs")
        .getFile()
    )

    val justifier =
      OWLApiBasedJustifier.UsingHermiT(OWLManager.createOWLOntologyManager())

    List(
     // new FameBasedProofGenerator(),
      new LetheBasedALCHProofGenerator(),
      new LetheBasedALCHProofGeneratorSkippingSteps(),
      new ForgettingBasedProofGenerator(
        LetheBasedForgetter.ALC_ABox, justifier, skipSteps = false),
      new ForgettingBasedProofGenerator(
        LetheBasedForgetter.ALC_ABox, justifier, skipSteps = true),
    ).foreach{ proofGenerator =>

      val tester = new ExampleFileTest(proofGenerator)

      tester.testDir(dir)
    }

  }
}

class ExampleFileTest(proofGenerator: IProofGenerator) {

  val parser = new JsonProofParser()

  val manager = OWLManager.createOWLOntologyManager()

  def testDir(dir: File) = {
    dir.listFiles().foreach(testFile)
  }

  def testFile(file: File) = {

    val justificationProof = parser.fromFile(file)

    val ontology = manager.createOntology()

    manager.addAxioms(ontology, justificationProof.getInferences().get(0).getPremises)

    proofGenerator.setOntology(ontology)

    val proof = justificationProof.getFinalConclusion match {
      case eq: OWLEquivalentClassesAxiom =>
        val classes = eq.getClassExpressionsAsList
        assert(classes.size()==2)
        proofGenerator.proveEquivalence(
          classes.get(0).asInstanceOf[OWLClass],
          classes.get(1).asInstanceOf[OWLClass])
      case subs: OWLSubClassOfAxiom =>
        proofGenerator.proveSubsumption(
          subs.getSubClass.asInstanceOf[OWLClass],
          subs.getSuperClass.asInstanceOf[OWLClass])
    }

    println(proof)
  }
}
