package de.tu_dresden.lat.forgettingBasedProofs.dataStructures


import org.semanticweb.owlapi.model.{OWLAxiom, OWLClass, OWLEntity, OWLOntology}
import uk.ac.man.cs.lethe.internal.tools.formatting.SimpleOWLFormatter

import scala.collection.mutable



/**
 * Abstraction for proof generator:
 */
trait ProofGenerator {

  def proveSubsumption(lhs: OWLClass, rhs: OWLClass): Proof

  def proveUnsatisfiability(concept: OWLClass): Proof

  def proveEquivalence(lhs: OWLClass, rhs: OWLClass): Proof
}

/**
 * Internal structure of proofs used.
 *
 * @param finalConclusion what is proven by the proof.
 */
class Proof(val finalConclusion: OWLAxiom) {

  private val leafs = new mutable.HashSet[OWLAxiom]()

  private val premiseMap = new mutable.HashMap[OWLAxiom, Iterable[OWLAxiom]]()

  def premisses(axiom: OWLAxiom): Iterable[OWLAxiom] =
    premiseMap(axiom)

  def hasNode(axiom: OWLAxiom) =
    premiseMap.contains(axiom)

  def setPremisses(axiom: OWLAxiom, premisses: Iterable[OWLAxiom]) = {

    println("premises for "+SimpleOWLFormatter.format(axiom))
    println("  are "+premisses.map(SimpleOWLFormatter.format))

    premiseMap.put(axiom, premisses)
  }

  def setLeaf(axiom: OWLAxiom)  ={
    leafs.add(axiom)
  }

  def isLeaf(axiom: OWLAxiom) =
    leafs.contains(axiom)
}

/**
 * Abstraction for forgetting component (only single names, from sets of axioms)
 */
trait Forgetter {

  def forget(axioms: Iterable[OWLAxiom], name: OWLEntity): Set[OWLAxiom]
}

/**
 * Abstraction for justification.
 */
trait Justifier {

  def justify(axioms: Iterable[OWLAxiom], axiom: OWLAxiom): Set[OWLAxiom]
}