001 /* This file is part of the project "Hilbert II" - http://www.qedeq.org
002 *
003 * Copyright 2000-2011, Michael Meyling <mime@qedeq.org>.
004 *
005 * "Hilbert II" is free software; you can redistribute
006 * it and/or modify it under the terms of the GNU General Public
007 * License as published by the Free Software Foundation; either
008 * version 2 of the License, or (at your option) any later version.
009 *
010 * This program is distributed in the hope that it will be useful,
011 * but WITHOUT ANY WARRANTY; without even the implied warranty of
012 * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
013 * GNU General Public License for more details.
014 */
015
016 package org.qedeq.kernel.bo.service.logic;
017
018 import java.io.File;
019 import java.util.Map;
020
021 import org.qedeq.base.io.IoUtility;
022 import org.qedeq.base.trace.Trace;
023 import org.qedeq.base.utility.YodaUtility;
024 import org.qedeq.kernel.bo.common.PluginExecutor;
025 import org.qedeq.kernel.bo.log.QedeqLog;
026 import org.qedeq.kernel.bo.logic.ProofFinderFactoryImpl;
027 import org.qedeq.kernel.bo.logic.common.ProofFinder;
028 import org.qedeq.kernel.bo.logic.common.ProofFinderFactory;
029 import org.qedeq.kernel.bo.module.ControlVisitor;
030 import org.qedeq.kernel.bo.module.KernelQedeqBo;
031 import org.qedeq.kernel.bo.module.QedeqFileDao;
032 import org.qedeq.kernel.se.base.module.Axiom;
033 import org.qedeq.kernel.se.base.module.FormalProofLineList;
034 import org.qedeq.kernel.se.base.module.FunctionDefinition;
035 import org.qedeq.kernel.se.base.module.InitialFunctionDefinition;
036 import org.qedeq.kernel.se.base.module.InitialPredicateDefinition;
037 import org.qedeq.kernel.se.base.module.PredicateDefinition;
038 import org.qedeq.kernel.se.base.module.Proposition;
039 import org.qedeq.kernel.se.base.module.Rule;
040 import org.qedeq.kernel.se.common.LogicalModuleState;
041 import org.qedeq.kernel.se.common.ModuleDataException;
042 import org.qedeq.kernel.se.common.Plugin;
043 import org.qedeq.kernel.se.common.SourceFileExceptionList;
044 import org.qedeq.kernel.se.dto.module.AddVo;
045 import org.qedeq.kernel.se.dto.module.FormalProofLineListVo;
046 import org.qedeq.kernel.se.dto.module.FormalProofLineVo;
047 import org.qedeq.kernel.se.dto.module.FormalProofVo;
048 import org.qedeq.kernel.se.dto.module.FormulaVo;
049 import org.qedeq.kernel.se.dto.module.PropositionVo;
050 import org.qedeq.kernel.se.dto.module.ReasonTypeVo;
051
052
053 /**
054 * Finds simple formal proofs.
055 *
056 * @author Michael Meyling
057 */
058 public final class SimpleProofFinderExecutor extends ControlVisitor implements PluginExecutor {
059
060 /** This class. */
061 private static final Class CLASS = SimpleProofFinderExecutor.class;
062
063 /** Factory for generating new checkers. */
064 private ProofFinderFactory finderFactory = null;
065
066 /** List of axioms, definitions and propositions. */
067 private FormalProofLineListVo validFormulas;
068
069 /** Save changed modules directly? */
070 private boolean noSave;
071
072 /** Currently running proof finder. */
073 private ProofFinder finder;
074
075 /**
076 * Constructor.
077 *
078 * @param plugin This plugin we work for.
079 * @param qedeq QEDEQ BO object.
080 * @param parameters Parameters.
081 */
082 SimpleProofFinderExecutor(final Plugin plugin, final KernelQedeqBo qedeq,
083 final Map parameters) {
084 super(plugin, qedeq);
085 final String method = "SimpleProofFinderExecutor(Plugin, KernelQedeqBo, Map)";
086 final String finderFactoryClass
087 = (parameters != null ? (String) parameters.get("checkerFactory") : null);
088 if (finderFactoryClass != null && finderFactoryClass.length() > 0) {
089 try {
090 Class cl = Class.forName(finderFactoryClass);
091 finderFactory = (ProofFinderFactory) cl.newInstance();
092 } catch (ClassNotFoundException e) {
093 Trace.fatal(CLASS, this, method, "ProofFinderFactory class not in class path: "
094 + finderFactoryClass, e);
095 } catch (InstantiationException e) {
096 Trace.fatal(CLASS, this, method, "ProofFinderFactory class could not be instanciated: "
097 + finderFactoryClass, e);
098 } catch (IllegalAccessException e) {
099 Trace.fatal(CLASS, this, method,
100 "Programming error, access for instantiation failed for model: "
101 + finderFactoryClass, e);
102 } catch (RuntimeException e) {
103 Trace.fatal(CLASS, this, method,
104 "Programming error, instantiation failed for model: " + finderFactoryClass, e);
105 }
106 }
107 // fallback is the default finder factory
108 if (finderFactory == null) {
109 finderFactory = new ProofFinderFactoryImpl();
110 }
111 String noSaveString = null;
112 if (parameters != null) {
113 noSaveString = (String) parameters.get("noSave");
114 }
115 noSave = "true".equalsIgnoreCase(noSaveString);
116 }
117
118 public Object executePlugin() {
119 getServices().checkModule(getQedeqBo().getModuleAddress());
120 QedeqLog.getInstance().logRequest(
121 "Trying to create formal proofs for \""
122 + IoUtility.easyUrl(getQedeqBo().getUrl()) + "\"");
123 try {
124 validFormulas = new FormalProofLineListVo();
125 traverse();
126 QedeqLog.getInstance().logSuccessfulReply(
127 "Proof creation finished for \"" + IoUtility.easyUrl(getQedeqBo().getUrl()) + "\"");
128 } catch (SourceFileExceptionList e) {
129 final String msg = "Proof creation not (fully?) successful for \""
130 + IoUtility.easyUrl(getQedeqBo().getUrl()) + "\"";
131 QedeqLog.getInstance().logFailureReply(msg, e.getMessage());
132 return Boolean.FALSE;
133 } finally {
134 getQedeqBo().addPluginErrorsAndWarnings(getPlugin(), getErrorList(), getWarningList());
135 }
136 return Boolean.TRUE;
137 }
138
139 public void visitEnter(final Axiom axiom) throws ModuleDataException {
140 if (axiom == null) {
141 return;
142 }
143 validFormulas.add(new FormalProofLineVo(new FormulaVo(getNodeBo().getFormula()),
144 new ReasonTypeVo(new AddVo(getNodeBo().getNodeVo().getId()))));
145 setBlocked(true);
146 }
147
148 public void visitLeave(final Axiom axiom) {
149 setBlocked(false);
150 }
151
152 public void visitEnter(final PredicateDefinition definition)
153 throws ModuleDataException {
154 if (definition == null) {
155 return;
156 }
157 validFormulas.add(new FormalProofLineVo(new FormulaVo(getNodeBo().getFormula()),
158 new ReasonTypeVo(new AddVo(getNodeBo().getNodeVo().getId()))));
159 setBlocked(true);
160 }
161
162 public void visitLeave(final PredicateDefinition definition) {
163 setBlocked(false);
164 }
165
166 public void visitEnter(final InitialPredicateDefinition definition)
167 throws ModuleDataException {
168 setBlocked(true);
169 }
170
171 public void visitLeave(final InitialPredicateDefinition definition) {
172 setBlocked(false);
173 }
174
175 public void visitEnter(final InitialFunctionDefinition definition)
176 throws ModuleDataException {
177 setBlocked(true);
178 }
179
180 public void visitLeave(final InitialFunctionDefinition definition) {
181 setBlocked(false);
182 }
183
184 public void visitEnter(final FunctionDefinition definition)
185 throws ModuleDataException {
186 if (definition == null) {
187 return;
188 }
189 validFormulas.add(new FormalProofLineVo(new FormulaVo(getNodeBo().getFormula()),
190 new ReasonTypeVo(new AddVo(getNodeBo().getNodeVo().getId()))));
191 setBlocked(true);
192 }
193
194 public void visitLeave(final FunctionDefinition definition) {
195 setBlocked(false);
196 }
197
198 public void visitEnter(final Proposition proposition)
199 throws ModuleDataException {
200 if (proposition == null) {
201 return;
202 }
203 final String context = getCurrentContext().getLocationWithinModule();
204 if (proposition.getFormalProofList() == null) {
205 final FormalProofLineList proof;
206 // we try finding a proof
207 try {
208 finder = finderFactory.createProofFinder();
209 proof = finder.findProof(proposition.getFormula().getElement(), validFormulas,
210 getCurrentContext());
211 } finally {
212 finder = null; // so we always new if we are currently searching
213 }
214 // TODO 20110323 m31: we do a dirty cast to modify the current module
215 Object state;
216 try {
217 state = YodaUtility.getFieldValue(getQedeqBo(), "stateManager");
218 YodaUtility.executeMethod(state, "setLogicalState", new Class[] {
219 LogicalModuleState.class},
220 new Object[] {LogicalModuleState.STATE_UNCHECKED});
221 ((PropositionVo) proposition).addFormalProof(new FormalProofVo(proof));
222 YodaUtility.executeMethod(state, "setErrors", new Class[] {
223 SourceFileExceptionList.class},
224 new Object[] {null});
225 ((PropositionVo) proposition).addFormalProof(new FormalProofVo(proof));
226 } catch (Exception e) {
227 final String msg = "changing properties failed";
228 Trace.fatal(CLASS, "visitEnter(Proposition)", msg, e);
229 QedeqLog.getInstance().logMessage(msg + " " + e.toString());
230 }
231 if (proof != null && !noSave) {
232 final File file = getServices().getLocalFilePath(
233 getQedeqBo().getModuleAddress());
234 try {
235 QedeqLog.getInstance().logMessage(
236 "Saving file \"" + file + "\"");
237 QedeqFileDao dao = getServices().getQedeqFileDao();
238 dao.saveQedeq(getQedeqBo(), file);
239 if (!getQedeqBo().getModuleAddress().isFileAddress()) {
240 QedeqLog.getInstance().logMessage("Only the the buffered file changed!");
241 }
242 } catch (Exception e) {
243 final String msg = "Saving file \"" + file + "\" failed";
244 Trace.fatal(CLASS, "visitEnter(Proposition)", msg, e);
245 QedeqLog.getInstance().logMessage(msg + " " + e.toString());
246 }
247 }
248 } else {
249 validFormulas.add(new FormalProofLineVo(new FormulaVo(getNodeBo().getFormula()),
250 new ReasonTypeVo(new AddVo(getNodeBo().getNodeVo().getId()))));
251 }
252 setBlocked(true);
253 }
254
255 public void visitLeave(final Proposition definition) {
256 setBlocked(false);
257 }
258
259 public void visitEnter(final Rule rule) throws ModuleDataException {
260 if (rule == null) {
261 return;
262 }
263 setBlocked(true);
264 }
265
266 public void visitLeave(final Rule rule) {
267 setBlocked(false);
268 }
269
270 /**
271 * Set location information where are we within the original module.
272 *
273 * @param locationWithinModule Location within module.
274 */
275 public void setLocationWithinModule(final String locationWithinModule) {
276 getCurrentContext().setLocationWithinModule(locationWithinModule);
277 }
278
279 public String getExecutionActionDescription() {
280 final String s = super.getExecutionActionDescription();
281 if (finder == null) {
282 return s;
283 }
284 return s + " " + finder.getExecutionActionDescription();
285 }
286
287 }
|