package de.tu_dresden.lat.forgettingBasedProofs.adaptors

import java.util.Collections

import forgetting.Fame
import org.semanticweb.HermiT
import com.clarkparsia.owlapi.explanation.DefaultExplanationGenerator
import com.clarkparsia.owlapi.explanation.util.{ExplanationProgressMonitor, SilentExplanationProgressMonitor}
import de.tu_dresden.lat.forgettingBasedProofs.dataStructures.{Forgetter, Justifier}
import org.semanticweb.owlapi.apibinding.OWLManager
import org.semanticweb.owlapi.model.{IRI, OWLAxiom, OWLClass, OWLEntity, OWLObjectProperty, OWLOntology, OWLOntologyManager, OWLSubObjectPropertyOfAxiom}
import org.semanticweb.owlapi.reasoner.OWLReasonerFactory
import uk.ac.man.cs.lethe.forgetting.{AlcOntologyForgetter, AlchTBoxForgetter, IOWLForgetter, ShqTBoxForgetter}

import scala.collection.JavaConverters._

object LetheBasedForgetter {

  def ALCH = new LetheBasedForgetter(new AlchTBoxForgetter())
  def ALC_ABox = new LetheBasedForgetter(new AlcOntologyForgetter())
  def SHQ = new LetheBasedForgetter(new ShqTBoxForgetter())
}

class LetheBasedForgetter(internalForgetter: IOWLForgetter) extends Forgetter {

  val ontologyManager = OWLManager.createOWLOntologyManager

  override def forget(axioms: Iterable[OWLAxiom], name: OWLEntity): Set[OWLAxiom] = {

    val axiomSet = axioms.toSet

    val ontology = ontologyManager.createOntology(axiomSet.asJava)

    internalForgetter.forget(ontology, Collections.singleton(name)).getAxioms().asScala.toSet
  }
}

class FameBasedForgetter extends Forgetter {
  val forgetter = new Fame()

  val ontologyManager = OWLManager.createOWLOntologyManager

  override def forget(axioms: Iterable[OWLAxiom], name: OWLEntity): Set[OWLAxiom] = {

    val ontology = ontologyManager.createOntology(axioms.toSet.asJava)

    val resultOnt: OWLOntology = name match {
      case cl: OWLClass =>
        forgetter.forget_alcoi(Set().asJava, Set(cl).asJava, ontology)
      case prp: OWLObjectProperty =>
        forgetter.forget_alcoi(Set(prp).asJava, Set().asJava, ontology)
      case _ => throw new UnsupportedOperationException()
    }

    resultOnt.getAxioms().asScala.toSet
  }
}

object OWLApiBasedJustifier {

  def UsingHermiT( manager: OWLOntologyManager)  =
    new OWLApiBasedJustifier(new HermiT.Reasoner.ReasonerFactory, manager)

}

/**
 * Extend the DefaultExplanationGenerator to also support role inclusions.
 */
class ExtendedDefaultExplanationGenerator(ontologyManager: OWLOntologyManager,
                                          reasonerFactory: OWLReasonerFactory,
                                          ontology: OWLOntology,
                                          progressMonitor: ExplanationProgressMonitor)
extends DefaultExplanationGenerator(ontologyManager, reasonerFactory, ontology, progressMonitor){

  val factory = ontologyManager.getOWLDataFactory

  val nominal = factory.getOWLNamedIndividual(IRI.create("ANYTHING"))

  // need to add an axiom to match signature with fresh individual name
  val addedAxiom = factory.getOWLClassAssertionAxiom(factory.getOWLThing, nominal)
  ontology.addAxiom(addedAxiom)

  override def getExplanation(axiom: OWLAxiom) = axiom match {
    case ri: OWLSubObjectPropertyOfAxiom => {
      val concept = factory.getOWLObjectIntersectionOf(
        factory.getOWLObjectHasValue(ri.getSubProperty, nominal),
        factory.getOWLObjectComplementOf(
          factory.getOWLObjectHasValue(ri.getSuperProperty, nominal)
        )
      )
      var result = getExplanation(concept)
      result.remove(addedAxiom)
      result
    }
    case _ => super.getExplanation(axiom)
  }
}

class OWLApiBasedJustifier(reasonerFactory: OWLReasonerFactory,
                           ontologyManager: OWLOntologyManager) extends Justifier {

  override def justify(axioms: Iterable[OWLAxiom], axiom: OWLAxiom): Set[OWLAxiom] = {

    val explanationGenerator =
      new ExtendedDefaultExplanationGenerator(
        ontologyManager,
        reasonerFactory,
        ontologyManager.createOntology(axioms.toSet.asJava),
        new SilentExplanationProgressMonitor()
      )

    explanationGenerator.getExplanation(axiom).asScala.toSet
  }

  override def toString() = {
    "OWLApiBasedJustifier("+reasonerFactory+")"
  }
}