package de.tu_dresden.lat.forgettingBasedProofs


import de.tu_dresden.lat.forgettingBasedProofs.dataStructures.{Forgetter, Justifier}
import de.tu_dresden.lat.forgettingBasedProofs.tools.Counter
import de.tu_dresden.lat.proofs.data.{Inference, Proof}
import de.tu_dresden.lat.proofs.interfaces.{IProof, IProofGenerator}
import org.semanticweb.owlapi.apibinding.OWLManager
import org.semanticweb.owlapi.model._
import org.semanticweb.owlapi.reasoner.OWLReasoner
import de.tu_dresden.lat.prettyPrinting.formatting.ParsableOWLFormatter

import scala.collection.JavaConverters._

/**
 *
 * @param forgetter
 * @param justifier
 * @param skipSteps when constructing the proof from the sequence of ontologies, allow to skip ontologies in the
 *                    sequence if this leads to proof steps of similar or smaller size
 */
class ForgettingBasedProofGenerator(forgetter: Forgetter,
                                    justifier: Justifier,
                                    skipSteps: Boolean = false) extends IProofGenerator {

  private var ontology: OWLOntology = _

  private var owlDataFactory: OWLDataFactory = _

  override def toString() = {
    "ForgettingBasedProofGenerator("+forgetter+", "+justifier+", skipSteps="+skipSteps+")"
  }

  override def setOntology(ont: OWLOntology) = {
    ontology = ont
    owlDataFactory = ontology.getOWLOntologyManager.getOWLDataFactory
  }

  override def setReasoner(reasoner: OWLReasoner) = {
    // does nothing
  }

  override def proveSubsumption(lhs: OWLClass, rhs: OWLClass) = {

    println("gonna prove that "+lhs+" is subsumed by "+rhs)

    targetSignature = List(lhs,rhs)
    toProve = subClassOf(lhs,rhs)
    prove()
  }

  def proveEquivalence(lhs: OWLClass, rhs: OWLClass) = {
    println("gonna prove that "+lhs+" is equivalent to "+rhs)

    targetSignature = List(lhs,rhs)
    toProve = equivalence(lhs, rhs)
    prove()
  }

  def proveUnsatisfiability(concept: OWLClass) = {

    println("gonna prove that "+concept+" is unsatisfiable")

    toProve = unsatisfiable(concept)
    targetSignature = Some(concept)
    prove()
  }

  var toProve: OWLAxiom = _
  var targetSignature: Iterable[OWLClass] = _
  var ontologySteps: List[Set[OWLAxiom]] = _
  var signatureSteps: List[OWLEntity] = _
  var doneForgettingAndJustifying: Boolean = _
  var proof: IProof = _

  var originalSignature: Set[OWLEntity] = _

  private def prove() = {

    ontologySteps = List(unifySignature(ontology.getLogicalAxioms().iterator.asScala.toSet,Set(toProve)))
    signatureSteps = List(null) 

    doneForgettingAndJustifying = false

    originalSignature = ontology
      .getLogicalAxioms()
      .iterator()
      .asScala
      .toSet[OWLAxiom].flatMap(_.getSignature.asScala)

    originalSignature ++= toProve.getSignature.asScala
    originalSignature ++= Set(owlDataFactory.getOWLThing,
      owlDataFactory.getOWLNothing,
      owlDataFactory.getOWLTopObjectProperty,
      owlDataFactory.getOWLBottomObjectProperty)


    while(!doneForgettingAndJustifying)
      forgetAndJustify()

    println("done with forgetting and justifying")

    proof = new Proof(toProve)
    for (ont <- ontologySteps)
      println(ont.map(new ParsableOWLFormatter().format))
    println(signatureSteps)
    //assert(ontologySteps.size==signatureSteps.size+1)
    reconstructProofFor(toProve, ontologySteps, signatureSteps, List(signatureSteps.head))
    proof
  }

  private def reconstructProofFor(axiom: OWLAxiom,
                                  prefix: Seq[Set[OWLAxiom]],
                                  prefixSig: Seq[OWLEntity],
                                  forgotSoFar: List[OWLEntity]): Unit = {
    println("prefix: "+prefixSig)
    println("forgotSoFar: "+forgotSoFar)
    if(!proof.hasInferenceFor(axiom)) prefix match {
      case Nil =>
        println("nothing left to prove for "+axiom)
        val inference = new Inference(axiom, "asserted", List().asJava)
        proof.addInference(inference)
        // proof.setLeaf(axiom)
        // proof.setPremisses(axiom, Set())

      case prevOnt::rest if prevOnt.contains(axiom) ||
        justifier.justify(prevOnt, axiom) // make sure we don't justify with definers!
          .exists(_.getSignature
            .asScala
            .exists(!originalSignature(_))) =>
        println(new ParsableOWLFormatter().format(axiom)+" occurs in "+prevOnt.map(new ParsableOWLFormatter().format))
        println(" or contains a definer: "+justifier.justify(prevOnt,axiom).filter(_.getSignature.asScala.exists(!originalSignature(_))))
        println("need to go one ontology further back")
        reconstructProofFor(axiom, rest, prefixSig.tail, List(prefixSig.head))

      case prevOnt::rest =>
        println("justifying "+new ParsableOWLFormatter().format(axiom)+" in "+prevOnt.map(new ParsableOWLFormatter().format))
        var premises = justifier.justify(prevOnt, axiom).filter(notAddedTautology)

        if (skipSteps) {
          // check whether we should skip
          rest match {
            case Nil => ;
            case prevPrevOnt::rest2 =>
              val premises2 = justifier.justify(prevPrevOnt, axiom).filter(notAddedTautology)
              if (premises2.size <= premises.size) {
                println("premise set\n"+premises2.map(new ParsableOWLFormatter().format)+"\nis smaller than\n"+premises.map(new ParsableOWLFormatter().format))
                reconstructProofFor(axiom, rest, prefixSig.tail, prefixSig.head::forgotSoFar)
                return
              }
          }
        }

        // no (more) skipping
        val ruleName =
          forgotSoFar match {
            case List(null) => "direct"
            case other => "forgetting "+forgotSoFar.map(_.getIRI.getFragment).mkString(", ")
          }


        proof.addInference(new Inference(
          axiom,
          ruleName,
          premises.toList.asJava))

        // proof.setPremisses(axiom, premises)
        premises.foreach(reconstructProofFor(_,rest, prefixSig.tail, List(prefixSig.head)))
    }
  }

  private def notAddedTautology(axiom: OWLAxiom) = {
    axiom match {
      case sa: OWLSubClassOfAxiom =>
        !(sa.getSubClass().isInstanceOf[OWLClass] && sa.getSuperClass().isTopEntity)
      case _ => true
    }
  }

  private def forgetAndJustify(): Unit ={
    var nextOntology::_ = ontologySteps

    println("current ontology: \n"+nextOntology.map(new ParsableOWLFormatter().format).mkString("\n")+"\n")
    
    val just = justifier.justify(nextOntology,toProve)

    assert(just.size>0, "something got lost while forgetting")

    println("Justification: \n"+just.map(new ParsableOWLFormatter().format).mkString("\n")+"\n")

    selectNextSymbol(just) match {
      case Some(nextSymbol) => {

        println("next symbol is " + nextSymbol)
        println("forgetting ..")
        var forgettingResult = forgetter.forget(just, nextSymbol)

        var tryNext = nextSymbol
        var triedSymbols = Set[OWLEntity](tryNext)
        var allFailed = false

        while(forgettingResult.exists(_.containsEntityInSignature(tryNext)) && !allFailed ) {
          println("Failed forgetting "+tryNext)
          selectNextSymbol(just, ignore = triedSymbols) match {
            case Some(next) =>
              tryNext = next
              triedSymbols += next
              println("next symbol is " + tryNext)
              println("forgetting ..")
              forgettingResult = forgetter.forget(just, tryNext)
            case None =>
              allFailed = true
          }
        }

        if(!allFailed) {
          // the following is needed to make sure justifications work even if outside
          // signature
          forgettingResult = unifySignature(forgettingResult, nextOntology)

          println("done")
          ontologySteps = forgettingResult :: ontologySteps
          signatureSteps = tryNext :: signatureSteps
        }
        else
          doneForgettingAndJustifying = true
      }
      case None => doneForgettingAndJustifying = true
    }
  }

  private def unifySignature(axioms: Set[OWLAxiom], other: Set[OWLAxiom]) = {
    var result = axioms
    val sig = axioms.flatMap(_.getSignature().iterator.asScala)
    result ++= other.flatMap(_.getSignature().iterator.asScala)
      .filterNot(sig)
      .map{ _ match {
        case cl: OWLClass => owlDataFactory.getOWLSubClassOfAxiom(cl, owlDataFactory.getOWLThing)
        case pr: OWLObjectProperty => owlDataFactory.getOWLSubClassOfAxiom(owlDataFactory.getOWLThing,
          owlDataFactory.getOWLObjectAllValuesFrom(pr, owlDataFactory.getOWLThing))
        case in: OWLNamedIndividual => owlDataFactory.getOWLClassAssertionAxiom(owlDataFactory.getOWLThing, in)
      }}


    result
  }

  def selectNextSymbol(axiomSet: Set[OWLAxiom], ignore: Set[OWLEntity] = Set()): Option[OWLEntity] = {
    val conceptNames = new Counter[OWLEntity]()
    val roleNames = new Counter[OWLEntity]()

    val nestedConceptNames = new Counter[OWLEntity]()
    val nestedRoleNames = new Counter[OWLObjectProperty]()
    var rolesWithFillers = Set[OWLObjectProperty]()

    axiomSet.foreach(_.getNestedClassExpressions().forEach{
      classExp =>

        classExp.getClassesInSignature().forEach(x =>
          if(originalSignature(x)) // we only select names in the original signature - other names would be introduced definers
                                   // and forgetting those would lead to an infinite loop
            conceptNames.add(x))

        classExp.getObjectPropertiesInSignature().forEach(x =>
          if(originalSignature(x))
            roleNames.add(x))

        classExp match {
          case e: OWLQuantifiedObjectRestriction =>
            if(!(e.getFiller.isOWLThing || e.getFiller.isOWLNothing))
              rolesWithFillers += e.getProperty().getObjectPropertiesInSignature().iterator().next()
            e.getFiller.getClassesInSignature().forEach(nestedConceptNames.add(_))
            e.getFiller.getObjectPropertiesInSignature().forEach(nestedRoleNames.add(_))
          case other => ; // do nothing
        }

    })

    conceptNames.removeKeys(targetSignature)
    conceptNames.removeKey(owlDataFactory.getOWLThing)
    conceptNames.removeKey(owlDataFactory.getOWLNothing)

    conceptNames.removeKeys(ignore)
    roleNames.removeKeys(ignore)

    nestedConceptNames.removeKey(owlDataFactory.getOWLThing)
    nestedConceptNames.removeKey(owlDataFactory.getOWLNothing)
    nestedConceptNames.removeKeys(targetSignature)
    nestedConceptNames.removeKeys(ignore)

    //if((conceptNames.keys.size+roleNames.keys.size) <= targetSignature.size+1)
    //  None
    //else

    val rolesWithoutFillers = roleNames.filter(r => !rolesWithFillers(r.asInstanceOf[OWLObjectProperty]))

    val unnestedConcepts = conceptNames.filter(!nestedConceptNames.keys.toSet(_))
    val unnestedRoles = roleNames.filter(!nestedRoleNames.keys.toSet(_))

    if(!rolesWithoutFillers.empty)
      Some(rolesWithoutFillers.max)
    else if(!unnestedConcepts.empty)
      Some(unnestedConcepts.max)
    else if(!conceptNames.empty)
      Some(conceptNames.max)
 //     else if (!unnestedRoles.empty)
 //     Some(unnestedRoles.max)
    else if(!roleNames.empty)
      Some(roleNames.max)
    else
      None
  }

  private def equivalence(lhs: OWLClass, rhs: OWLClass): OWLAxiom = {
    owlDataFactory.getOWLEquivalentClassesAxiom(lhs,rhs)
  }

  private def subClassOf(lhs: OWLClass, rhs: OWLClass): OWLAxiom = {
    owlDataFactory.getOWLSubClassOfAxiom(lhs,rhs)
  }

  private def unsatisfiable(concept: OWLClass): OWLAxiom =
    owlDataFactory.getOWLSubClassOfAxiom(concept, owlDataFactory.getOWLNothing)
}
