/*-
 * #%L
 * ELK Reasoner Protege Plug-in
 * $Id:$
 * $HeadURL:$
 * %%
 * Copyright (C) 2011 - 2017 Department of Computer Science, University of Oxford
 * %%
 * Licensed under the Apache License, Version 2.0 (the "License");
 * you may not use this file except in compliance with the License.
 * You may obtain a copy of the License at
 * 
 *      http://www.apache.org/licenses/LICENSE-2.0
 * 
 * Unless required by applicable law or agreed to in writing, software
 * distributed under the License is distributed on an "AS IS" BASIS,
 * WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
 * See the License for the specific language governing permissions and
 * limitations under the License.
 * #L%
 */
package org.semanticweb.elk.protege.proof;

import java.util.Collection;
import java.util.Collections;
import java.util.Set;

import org.liveontologies.protege.justification.proof.service.JustificationCompleteProof;
import org.liveontologies.puli.Inference;
import org.liveontologies.puli.InferenceJustifier;
import org.liveontologies.puli.InferenceJustifiers;
import org.liveontologies.puli.Proof;
import org.liveontologies.puli.Proofs;
import org.semanticweb.elk.owlapi.ElkProver;
import org.semanticweb.elk.owlapi.ElkReasoner;
import org.semanticweb.owlapi.model.OWLAxiom;

import com.google.common.base.Function;

public class ElkOwlJustificationProofService
		extends ElkJustificationProofService {

	@Override
	public JustificationCompleteProof computeProof(OWLAxiom entailment) {
		ElkReasoner elkReasoner = getCurrentElkReasoner();
		if (elkReasoner == null) {
			return null;
		}
		// else
		ElkProver elkProver = new ElkProver(elkReasoner);
		final Proof<OWLAxiom> OwlProof = Proofs.addAssertedInferences(
				elkProver.getProof(entailment), getEditorKit()
						.getOWLModelManager().getActiveOntology().getAxioms());
		final Proof<Object> proof = Proofs.transform(OwlProof,
				new Function<OWLAxiom, Object>() {
					@Override
					public Object apply(final OWLAxiom input) {
						return input;
					}
				}, new Function<Object, OWLAxiom>() {
					@Override
					public OWLAxiom apply(final Object input) {
						// This is safe, because only OWLAxioms will be queried.
						return (OWLAxiom) input;
					}
				});
		InferenceJustifier<Object, ? extends Set<? extends OWLAxiom>> justifier = InferenceJustifiers
				.transform(InferenceJustifiers.justifyAssertedInferences(),
						new Function<Object, OWLAxiom>() {
							@Override
							public OWLAxiom apply(Object input) {
								/*
								 * This is safe, because the inferences are
								 * justified only by OWLAxioms.
								 */
								return (OWLAxiom) input;
							}
						});
		return new JustificationCompleteProof() {

			@Override
			public Collection<? extends Inference<Object>> getInferences(
					Object conclusion) {
				if (!(conclusion instanceof OWLAxiom)) {
					return Collections.emptyList();
				}
				// else
				return proof.getInferences((OWLAxiom) conclusion);
			}

			@Override
			public Set<? extends OWLAxiom> getJustification(
					Inference<Object> inference) {
				return justifier.getJustification(inference);
			}

			@Override
			public OWLAxiom getGoal() {
				return entailment;
			}
		};
	}

	@Override
	public String getName() {
		return "ELK OWL Proof";
	}

}

@@ -1692,21 +1692,16 @@
 of%3CO
-WLAxiom%3E OwlP
+bject%3E p
 roof
@@ -1737,16 +1737,33 @@
 es(%0A%09%09%09%09
+Proofs.transform(
 elkProve
@@ -1789,143 +1789,11 @@
 nt),
- getEditorKit()%0A%09%09%09%09%09%09.getOWLModelManager().getActiveOntology().getAxioms());%0A%09%09final Proof%3CObject%3E proof = Proofs.transform(OwlProof,%0A
+%0A%09%09
 %09%09%09%09
@@ -1824,32 +1824,34 @@
 bject%3E() %7B%0A%09%09%09%09%09
+%09
+%09
 @Override%0A%09%09%09%09%09p
@@ -1836,32 +1836,34 @@
 %09%09%09%09%09%09@Override%0A
+%09%09
 %09%09%09%09%09public Obje
@@ -1897,24 +1897,26 @@
 ut) %7B%0A%09%09%09%09%09%09
+%09%09
 return input
@@ -1922,22 +1922,26 @@
 t;%0A%09%09%09%09%09
+%09%09
 %7D%0A%09%09%09%09
+%09
+%09
 %7D, new F
@@ -1971,24 +1971,26 @@
 m%3E() %7B%0A%09%09%09%09%09
+%09%09
 @Override%0A%09%09
@@ -1983,24 +1983,26 @@
 %09%09@Override%0A
+%09%09
 %09%09%09%09%09public 
@@ -2044,16 +2044,18 @@
 %7B%0A%09%09%09%09%09%09
+%09%09
 // This 
@@ -2093,16 +2093,27 @@
  will be
+%0A%09%09%09%09%09%09%09%09//
  queried
@@ -2116,24 +2116,26 @@
 ried.%0A%09%09%09%09%09%09
+%09%09
 return (OWLA
@@ -2156,15 +2156,100 @@
 %09%09%09%09
-%7D%0A%09%09%09%09%7D
+%09%09%7D%0A%09%09%09%09%09%09%7D),%0A%09%09%09%09getEditorKit().getOWLModelManager().getActiveOntology()%0A%09%09%09%09%09%09.getAxioms()
 );%0A%09

Fix OWL Proof justification computation