package de.tu_dresden.lat.forgettingBasedProofs

import de.tu_dresden.lat.forgettingBasedProofs.dataStructures.{Forgetter, Justifier}
import de.tu_dresden.lat.proofs.data.{Inference, Proof}
import de.tu_dresden.lat.proofs.interfaces.{IInference, IProof, IProofGenerator}
import org.semanticweb.owlapi.model.{OWLAxiom, OWLClass, OWLEntity, OWLOntology}
import org.semanticweb.owlapi.reasoner.OWLReasoner

import scala.collection.JavaConverters._

class CompleteForgettingBasedProofGenerator(var ontology: OWLOntology,
        forgetter: Forgetter,
        justifier: Justifier,
        skipSteps: Boolean = false) extends IProofGenerator
{

  var targetSignature: Set[OWLEntity] = _
  var targetAxiom: OWLAxiom = _
  var inferences: Set[IInference] = _

  var processedSignatures = Set[Set[OWLEntity]]()

  override def setOntology(ont: OWLOntology) = {
    ontology = ont
  }

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


  override def proveSubsumption(owlClass: OWLClass, owlClass1: OWLClass): IProof = {
    targetSignature = Set(owlClass, owlClass1)
    targetAxiom = ontology.getOWLOntologyManager.getOWLDataFactory.getOWLSubClassOfAxiom(owlClass,owlClass1)
    inferences = Set()

    justifier.justify(ontology.axioms().iterator.asScala.toSet, targetAxiom).foreach{ axiom =>
      inferences += new Inference(axiom, "asserted", List().asJava)
    }

    prove(ontology.axioms().iterator().asScala.toSet)

    new Proof(targetAxiom, inferences.toList.asJava)
  }

  override def proveEquivalence(owlClass: OWLClass, owlClass1: OWLClass): IProof = {
    targetSignature = Set(owlClass, owlClass1)
    targetAxiom = ontology.getOWLOntologyManager.getOWLDataFactory.getOWLEquivalentClassesAxiom(owlClass,owlClass1)
    inferences = Set()

    justifier.justify(ontology.axioms().iterator.asScala.toSet, targetAxiom).foreach {axiom =>
      inferences += new Inference(axiom, "asserted", List().asJava)
    }

    prove(ontology.axioms().iterator().asScala.toSet)


    new Proof(targetAxiom, inferences.toList.asJava)
  }

  def prove(axioms: Set[OWLAxiom]): Set[OWLAxiom] ={

    val just = justifier.justify(axioms, targetAxiom)

    val signature = just.flatMap(_.classesInSignature().iterator().asScala.toSet[OWLEntity])--targetSignature

    println(processedSignatures)
    println("SIGNATURE: "+signature.map(_.getIRI.getFragment))

    if(!processedSignatures.contains(signature)) {
      processedSignatures += signature

      signature.foreach { concept =>

        if(!processedSignatures.contains(signature-concept)) {
          val nextOnt = forgetter.forget(just, concept)

          val relevantAxioms = prove(nextOnt)

          relevantAxioms.foreach { axiom =>
            val premises = justifier.justify(just, axiom)
            inferences += new Inference(axiom, "forgetting", premises.toList.asJava)
          }
        }
      }
    } else
      println("SKIPPED!")
    just
  }
}
