0001 /* This file is part of the project "Hilbert II" - http://www.qedeq.org
0002 *
0003 * Copyright 2000-2013, Michael Meyling <mime@qedeq.org>.
0004 *
0005 * "Hilbert II" is free software; you can redistribute
0006 * it and/or modify it under the terms of the GNU General Public
0007 * License as published by the Free Software Foundation; either
0008 * version 2 of the License, or (at your option) any later version.
0009 *
0010 * This program is distributed in the hope that it will be useful,
0011 * but WITHOUT ANY WARRANTY; without even the implied warranty of
0012 * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
0013 * GNU General Public License for more details.
0014 */
0015
0016 package org.qedeq.kernel.bo.service;
0017
0018 import java.io.File;
0019 import java.io.FileFilter;
0020 import java.io.IOException;
0021 import java.io.Reader;
0022 import java.io.UnsupportedEncodingException;
0023 import java.net.MalformedURLException;
0024 import java.net.URL;
0025 import java.net.URLEncoder;
0026 import java.util.ArrayList;
0027 import java.util.List;
0028
0029 import org.qedeq.base.io.IoUtility;
0030 import org.qedeq.base.io.LoadingListener;
0031 import org.qedeq.base.io.SourceArea;
0032 import org.qedeq.base.io.TextInput;
0033 import org.qedeq.base.io.UrlUtility;
0034 import org.qedeq.base.trace.Trace;
0035 import org.qedeq.base.utility.StringUtility;
0036 import org.qedeq.kernel.bo.common.KernelProperties;
0037 import org.qedeq.kernel.bo.common.QedeqBo;
0038 import org.qedeq.kernel.bo.common.ServiceModule;
0039 import org.qedeq.kernel.bo.common.ServiceProcess;
0040 import org.qedeq.kernel.bo.log.QedeqLog;
0041 import org.qedeq.kernel.bo.module.InternalKernelServices;
0042 import org.qedeq.kernel.bo.module.InternalServiceProcess;
0043 import org.qedeq.kernel.bo.module.KernelQedeqBo;
0044 import org.qedeq.kernel.bo.module.QedeqFileDao;
0045 import org.qedeq.kernel.bo.service.dependency.LoadAllRequiredModulesPlugin;
0046 import org.qedeq.kernel.bo.service.dependency.LoadDirectlyRequiredModulesPlugin;
0047 import org.qedeq.kernel.bo.service.dependency.LoadRequiredModulesPlugin;
0048 import org.qedeq.kernel.bo.service.logic.FormalProofCheckerPlugin;
0049 import org.qedeq.kernel.bo.service.logic.SimpleProofFinderPlugin;
0050 import org.qedeq.kernel.bo.service.logic.WellFormedCheckerPlugin;
0051 import org.qedeq.kernel.se.base.module.Qedeq;
0052 import org.qedeq.kernel.se.base.module.Specification;
0053 import org.qedeq.kernel.se.common.DefaultModuleAddress;
0054 import org.qedeq.kernel.se.common.ModuleAddress;
0055 import org.qedeq.kernel.se.common.ModuleDataException;
0056 import org.qedeq.kernel.se.common.Plugin;
0057 import org.qedeq.kernel.se.common.SourceFileException;
0058 import org.qedeq.kernel.se.common.SourceFileExceptionList;
0059 import org.qedeq.kernel.se.config.QedeqConfig;
0060 import org.qedeq.kernel.se.dto.module.QedeqVo;
0061 import org.qedeq.kernel.se.state.LoadingState;
0062 import org.qedeq.kernel.se.visitor.ContextChecker;
0063 import org.qedeq.kernel.se.visitor.DefaultContextChecker;
0064
0065
0066 /**
0067 * This class provides a default implementation for the QEDEQ module services.
0068 *
0069 * @author Michael Meyling
0070 */
0071 public class DefaultInternalKernelServices implements ServiceModule, InternalKernelServices,
0072 Plugin {
0073
0074 /** This class. */
0075 private static final Class CLASS = DefaultInternalKernelServices.class;
0076
0077 /** For synchronized waiting. */
0078 private static final Object MONITOR = new Object();
0079
0080 /** Number of method calls. */
0081 private final String processCounterSync = CLASS.toString();
0082
0083 /** Number of method calls. */
0084 private volatile int processCounter = 0;
0085
0086 /** Collection of already known QEDEQ modules. */
0087 private KernelQedeqBoStorage modules;
0088
0089 /** Config access. */
0090 private final QedeqConfig config;
0091
0092 /** Basic kernel properties. */
0093 private final KernelProperties kernel;
0094
0095 /** This instance nows how to load a module from the file system. */
0096 private final QedeqFileDao qedeqFileDao;
0097
0098 /** Synchronize module access. */
0099 private final ModuleArbiter arbiter;
0100
0101 /** This instance manages plugins. */
0102 private final PluginManager pluginManager;
0103
0104 /** This instance manages service processes. */
0105 private final ServiceProcessManager processManager;
0106
0107 /** Validate module dependencies and status. */
0108 private boolean validate = true;
0109
0110 /** We check the context with this checker. */
0111 private ContextChecker contextChecker;
0112
0113 /**
0114 * Constructor.
0115 *
0116 * @param config For config access.
0117 * @param kernel For kernel properties.
0118 * @param loader For loading QEDEQ modules.
0119 */
0120 public DefaultInternalKernelServices(final QedeqConfig config, final KernelProperties kernel,
0121 final QedeqFileDao loader) {
0122 this.config = config;
0123 this.kernel = kernel;
0124 this.qedeqFileDao = loader;
0125 arbiter = new ModuleArbiter();
0126 pluginManager = new PluginManager(this);
0127 processManager = new ServiceProcessManager(pluginManager, arbiter);
0128 contextChecker = new DefaultContextChecker();
0129 loader.setServices(this);
0130
0131 //// pluginManager.addPlugin(MultiProofFinderPlugin.class.getName());
0132 pluginManager.addPlugin("org.qedeq.kernel.bo.service.unicode.Qedeq2UnicodeTextPlugin");
0133 pluginManager.addPlugin("org.qedeq.kernel.bo.service.latex.Qedeq2LatexPlugin");
0134 pluginManager.addPlugin("org.qedeq.kernel.bo.service.unicode.Qedeq2Utf8Plugin");
0135 //// pluginManager.addPlugin("org.qedeq.kernel.bo.service.heuristic.HeuristicCheckerPlugin");
0136 pluginManager.addPlugin("org.qedeq.kernel.bo.service.heuristic.DynamicHeuristicCheckerPlugin");
0137 pluginManager.addPlugin(SimpleProofFinderPlugin.class.getName());
0138
0139 // add internal plugins
0140 pluginManager.addPlugin(LoadDirectlyRequiredModulesPlugin.class.getName());
0141 pluginManager.addPlugin(LoadAllRequiredModulesPlugin.class.getName());
0142 pluginManager.addPlugin(LoadRequiredModulesPlugin.class.getName());
0143 pluginManager.addPlugin(WellFormedCheckerPlugin.class.getName());
0144 pluginManager.addPlugin(FormalProofCheckerPlugin.class.getName());
0145 }
0146
0147 public void startupServices() {
0148 modules = new KernelQedeqBoStorage();
0149 if (config.isAutoReloadLastSessionChecked()) {
0150 autoReloadLastSessionChecked();
0151 }
0152 }
0153
0154 public void shutdownServices() {
0155 processManager.terminateAndRemoveAllServiceProcesses();
0156 modules.removeAllModules();
0157 modules = null;
0158 // clear thread interrupt flag because we might have interrupted ourself
0159 Thread.interrupted();
0160 }
0161
0162 /**
0163 * If configured load all QEDEQ modules that where successfully loaded the last time.
0164 */
0165 public void autoReloadLastSessionChecked() {
0166 if (config.isAutoReloadLastSessionChecked()) {
0167 final Thread thread = new Thread() {
0168 public void run() {
0169 final String method = "autoReloadLastSessionChecked.thread.run()";
0170 try {
0171 Trace.begin(CLASS, this, method);
0172 QedeqLog.getInstance().logMessage(
0173 "Trying to load previously successfully loaded modules.");
0174 final int number = config.getPreviouslyLoadedModules().length;
0175 if (loadPreviouslySuccessfullyLoadedModules()) {
0176 QedeqLog.getInstance().logMessage(
0177 "Loading of " + number + " previously successfully loaded module"
0178 + (number != 1 ? "s" : "") + " successfully done.");
0179 } else {
0180 QedeqLog.getInstance().logMessage(
0181 "Loading of all previously successfully checked modules failed. "
0182 + number + " module" + (number != 1 ? "s" : "")
0183 + " were tried.");
0184 }
0185 } catch (Exception e) {
0186 Trace.trace(CLASS, this, method, e);
0187 } finally {
0188 Trace.end(CLASS, this, method);
0189 }
0190 }
0191 };
0192 thread.setDaemon(true);
0193 thread.start();
0194 }
0195 }
0196
0197 public void removeAllModules() {
0198 do {
0199 synchronized (this) {
0200 if (processCounter == 0) {
0201 getModules().removeAllModules();
0202 return;
0203 }
0204 }
0205 // we must wait for the other processes to stop (so that processCounter == 0)
0206 synchronized (MONITOR) {
0207 try {
0208 MONITOR.wait(10000);
0209 } catch (InterruptedException e) {
0210 }
0211 }
0212 } while (true);
0213
0214 }
0215
0216 /**
0217 * Remove a QEDEQ module from memory.
0218 *
0219 * @param address Remove module identified by this address.
0220 */
0221 public void removeModule(final ModuleAddress address) {
0222 final QedeqBo prop = getQedeqBo(address);
0223 if (prop != null) {
0224 QedeqLog.getInstance().logRequest("Removing module", address.getUrl());
0225 try {
0226 removeModule(getModules().getKernelQedeqBo(this, address));
0227 } catch (final RuntimeException e) {
0228 QedeqLog.getInstance().logFailureReply(
0229 "Remove failed", address.getUrl(), e.getMessage());
0230 }
0231
0232 if (validate) {
0233 modules.validateDependencies();
0234 }
0235 }
0236 }
0237
0238 /**
0239 * Remove a QEDEQ module from memory. This method must block all other methods and if this
0240 * method runs no other is allowed to run
0241 *
0242 * @param prop Remove module identified by this property.
0243 */
0244 private void removeModule(final DefaultKernelQedeqBo prop) {
0245 do {
0246 synchronized (this) {
0247 if (processCounter == 0) { // no other method is allowed to run
0248 // FIXME mime 20080319: one could call prop.setLoadingProgressState(
0249 // LoadingState.STATE_DELETED) alone but that would
0250 // miss to inform the KernelQedeqBoPool. How do we inform the pool?
0251 // must the StateManager have a reference to it?
0252 prop.delete();
0253 getModules().removeModule(prop);
0254 return;
0255 }
0256 }
0257 // we must wait for the other processes to stop (so that processCounter == 0)
0258 synchronized (MONITOR) {
0259 try {
0260 MONITOR.wait(10000);
0261 } catch (InterruptedException e) {
0262 }
0263 }
0264 } while (true);
0265
0266 }
0267
0268 /**
0269 * Clear local file buffer and all loaded QEDEQ modules.
0270 *
0271 * @return Successful?
0272 */
0273 public boolean clearLocalBuffer() {
0274 final String method = "clearLocalBuffer";
0275 try {
0276 QedeqLog.getInstance().logMessage(
0277 "Clear local buffer from all QEDEQ files.");
0278 removeAllModules();
0279 final File bufferDir = getBufferDirectory().getCanonicalFile();
0280 if (bufferDir.exists() && !IoUtility.deleteDir(bufferDir, new FileFilter() {
0281 public boolean accept(final File pathname) {
0282 return pathname.getName().endsWith(".xml");
0283 }
0284 })) {
0285 throw new IOException("buffer could not be deleted: " + bufferDir);
0286 }
0287 QedeqLog.getInstance().logMessage("Local buffer was cleared.");
0288 return true;
0289 } catch (IOException e) {
0290 Trace.fatal(CLASS, this, method, "IO access problem", e);
0291 QedeqLog.getInstance().logMessage(
0292 "Local buffer not cleared. IO access problem. " + e.getMessage());
0293 return false;
0294 } catch (final RuntimeException e) {
0295 Trace.fatal(CLASS, this, method, "unexpected problem", e);
0296 QedeqLog.getInstance().logMessage(
0297 "Local buffer not cleared. " + e.getMessage());
0298 return false;
0299 }
0300 }
0301
0302 public QedeqBo loadModule(final ModuleAddress address) {
0303 final String method = "loadModule(ModuleAddress)";
0304 processInc();
0305 final DefaultKernelQedeqBo prop = getModules().getKernelQedeqBo(this, address);
0306 try {
0307 synchronized (prop) {
0308 if (prop.isLoaded()) {
0309 return prop;
0310 }
0311 QedeqLog.getInstance().logRequest("Load module", address.getUrl());
0312 if (prop.getModuleAddress().isFileAddress()) {
0313 loadLocalModule(prop);
0314 } else {
0315 // search in local file buffer
0316 try {
0317 getCanonicalReadableFile(prop);
0318 } catch (ModuleFileNotFoundException e) { // file not found
0319 // we will continue by creating a local copy
0320 saveQedeqFromWebToBuffer(prop);
0321 }
0322 loadBufferedModule(prop);
0323 }
0324 QedeqLog.getInstance().logSuccessfulReply(
0325 "Successfully loaded", address.getUrl());
0326 }
0327 } catch (SourceFileExceptionList e) {
0328 Trace.trace(CLASS, this, method, e);
0329 QedeqLog.getInstance().logFailureState("Loading of module failed!", address.getUrl(),
0330 e.toString());
0331 } catch (final RuntimeException e) {
0332 Trace.fatal(CLASS, this, method, "unexpected problem", e);
0333 QedeqLog.getInstance().logFailureReply("Loading failed", address.getUrl(), e.getMessage());
0334 } finally {
0335 processDec();
0336 }
0337 return prop;
0338 }
0339
0340 /**
0341 * Load buffered QEDEQ module file.
0342 *
0343 * @param prop Load this.
0344 * @throws SourceFileExceptionList Loading or QEDEQ module failed.
0345 */
0346 private void loadBufferedModule(final DefaultKernelQedeqBo prop)
0347 throws SourceFileExceptionList {
0348 prop.setLoadingProgressState(this, LoadingState.STATE_LOADING_FROM_BUFFER);
0349 final File localFile;
0350 try {
0351 localFile = getCanonicalReadableFile(prop);
0352 } catch (ModuleFileNotFoundException e) {
0353 final SourceFileExceptionList sfl = createSourceFileExceptionList(
0354 ServiceErrors.LOADING_FROM_FILE_BUFFER_FAILED_CODE,
0355 ServiceErrors.LOADING_FROM_FILE_BUFFER_FAILED_TEXT,
0356 prop.getUrl(), e);
0357 prop.setLoadingFailureState(LoadingState.STATE_LOADING_FROM_BUFFER_FAILED, sfl);
0358 throw sfl;
0359 }
0360
0361 prop.setQedeqFileDao(getQedeqFileDao()); // remember loader for this module
0362 final Qedeq qedeq;
0363 try {
0364 // FIXME 20130321 m31: use another service process and don't create a new one here!
0365 qedeq = getQedeqFileDao().loadQedeq(new ServiceProcessImpl("loadBufferedModule"),
0366 prop, localFile);
0367 } catch (SourceFileExceptionList sfl) {
0368 prop.setLoadingFailureState(LoadingState.STATE_LOADING_FROM_BUFFER_FAILED, sfl);
0369 throw sfl;
0370 }
0371 setCopiedQedeq(prop, qedeq);
0372 }
0373
0374 /**
0375 * Load QEDEQ module file with file loader.
0376 *
0377 * @param prop Load this.
0378 * @throws SourceFileExceptionList Loading or copying QEDEQ module failed.
0379 */
0380 private void loadLocalModule(final DefaultKernelQedeqBo prop) throws SourceFileExceptionList {
0381 prop.setLoadingProgressState(this, LoadingState.STATE_LOADING_FROM_LOCAL_FILE);
0382 final File localFile;
0383 try {
0384 localFile = getCanonicalReadableFile(prop);
0385 } catch (ModuleFileNotFoundException e) {
0386 final SourceFileExceptionList sfl = createSourceFileExceptionList(
0387 ServiceErrors.LOADING_FROM_LOCAL_FILE_FAILED_CODE,
0388 ServiceErrors.LOADING_FROM_LOCAL_FILE_FAILED_TEXT,
0389 prop.getUrl(), e);
0390 prop.setLoadingFailureState(LoadingState.STATE_LOADING_FROM_LOCAL_FILE_FAILED, sfl);
0391 throw sfl;
0392 }
0393 prop.setQedeqFileDao(getQedeqFileDao()); // remember loader for this module
0394
0395 final Qedeq qedeq;
0396 try {
0397 // FIXME 20130321 m31: use another service process and don't create a new one here!
0398 qedeq = getQedeqFileDao().loadQedeq(new ServiceProcessImpl("loadLocalModule"), prop,
0399 localFile);
0400 } catch (SourceFileExceptionList sfl) {
0401 prop.setLoadingFailureState(LoadingState.STATE_LOADING_FROM_LOCAL_FILE_FAILED, sfl);
0402 throw sfl;
0403 }
0404 setCopiedQedeq(prop, qedeq);
0405 }
0406
0407 private void setCopiedQedeq(final DefaultKernelQedeqBo prop, final Qedeq qedeq)
0408 throws SourceFileExceptionList {
0409 final String method = "setCopiedQedeq(DefaultKernelQedeqBo, Qedeq)";
0410 prop.setLoadingProgressState(this, LoadingState.STATE_LOADING_INTO_MEMORY);
0411 QedeqVo vo = null;
0412 try {
0413 vo = QedeqVoBuilder.createQedeq(prop.getModuleAddress(), qedeq);
0414 } catch (RuntimeException e) {
0415 Trace.fatal(CLASS, this, method, "looks like a programming error", e);
0416 final SourceFileExceptionList xl = createSourceFileExceptionList(
0417 ServiceErrors.RUNTIME_ERROR_CODE,
0418 ServiceErrors.RUNTIME_ERROR_TEXT,
0419 prop.getModuleAddress().getUrl(), e);
0420 prop.setLoadingFailureState(LoadingState.STATE_LOADING_INTO_MEMORY_FAILED, xl);
0421 throw xl;
0422 } catch (ModuleDataException e) {
0423 if (e.getCause() != null) {
0424 Trace.fatal(CLASS, this, method, "looks like a programming error", e.getCause());
0425 } else {
0426 Trace.fatal(CLASS, this, method, "looks like a programming error", e);
0427 }
0428 final SourceFileExceptionList xl = prop.createSourceFileExceptionList(this, e, qedeq);
0429 prop.setLoadingFailureState(LoadingState.STATE_LOADING_INTO_MEMORY_FAILED, xl);
0430 throw xl;
0431 }
0432 prop.setQedeqVo(vo);
0433 // TODO 20110213 m31: perhaps we need a new state, pre loaded? So when we put more
0434 // label testing into the moduleLabelCreator, we still can launch some plugins
0435 // On the other side: Label checking is only possible, if all referenced modules can
0436 // be loaded.
0437 //
0438 // Correct labels are necessary for many plugins (e.g. LaTeX and UTF-8 generation).
0439 // So a label checker must be run before that.
0440 // It might be a good idea to put it into the formal logic checker.
0441 // We could make a FormalChecker plugin. This starts loading required modules, checks
0442 // the labels and checks if the formulas are correctly written.
0443 // So we get some sub status (for every check) and an overall status (all checks
0444 // green). Later on the formal proof checker can be integrated too.
0445 // This should be the extended load status.
0446 final ModuleLabelsCreator moduleNodesCreator = new ModuleLabelsCreator(this, prop);
0447 try {
0448 // FIXME 20130321 m31: use another service process and don't create a new one here!
0449 moduleNodesCreator.createLabels(new ServiceProcessImpl("copyQedeq"));
0450 prop.setLoaded(vo, moduleNodesCreator.getLabels(), moduleNodesCreator.getConverter(),
0451 moduleNodesCreator.getTextConverter());
0452 } catch (SourceFileExceptionList sfl) {
0453 prop.setLoadingFailureState(LoadingState.STATE_LOADING_INTO_MEMORY_FAILED, sfl);
0454 throw sfl;
0455 }
0456 }
0457
0458 /**
0459 * Check if file exists and is readable. Checks the local buffer file for a buffered module or
0460 * the module file address directly. Returns canonical file path.
0461 *
0462 * @param prop Check for this file.
0463 * @return Canonical file path.
0464 * @throws ModuleFileNotFoundException File doesn't exist or is not readable.
0465 */
0466 private File getCanonicalReadableFile(final QedeqBo prop) throws ModuleFileNotFoundException {
0467 final String method = "getCanonicalReadableFile(File)";
0468 final File localFile = getLocalFilePath(prop.getModuleAddress());
0469 final File file;
0470 try {
0471 file = localFile.getCanonicalFile();
0472 } catch (IOException e) {
0473 Trace.trace(CLASS, this, method, e);
0474 throw new ModuleFileNotFoundException("file path not correct: " + localFile);
0475 }
0476 if (!file.canRead()) {
0477 Trace.trace(CLASS, this, method, "file not readable=" + file);
0478 throw new ModuleFileNotFoundException("file not readable: " + file);
0479 }
0480 return file;
0481 }
0482
0483 /**
0484 * Load specified QEDEQ module from QEDEQ parent module.
0485 *
0486 * @param parent Parent module address.
0487 * @param spec Specification for another QEDEQ module.
0488 * @return Loaded module.
0489 * @throws SourceFileExceptionList Loading failed.
0490 */
0491 public KernelQedeqBo loadModule(final ModuleAddress parent, final Specification spec)
0492 throws SourceFileExceptionList {
0493
0494 final String method = "loadModule(Module, Specification)";
0495 Trace.begin(CLASS, this, method);
0496 Trace.trace(CLASS, this, method, spec);
0497 processInc();
0498 DefaultKernelQedeqBo prop = null; // currently tried module
0499 try {
0500 final ModuleAddress[] modulePaths;
0501 try {
0502 modulePaths = parent.getModulePaths(spec);
0503 } catch (IOException e) {
0504 Trace.fatal(CLASS, this, method, "getting module path failed", e); // TODO 20110308 m31: make constant
0505 throw createSourceFileExceptionList(
0506 ServiceErrors.LOADING_FROM_FILE_BUFFER_FAILED_CODE,
0507 ServiceErrors.LOADING_FROM_FILE_BUFFER_FAILED_TEXT,
0508 parent.getUrl(), e);
0509 }
0510
0511 // now we iterate over the possible module addresses
0512 for (int i = 0; i < modulePaths.length; i++) {
0513 prop = getModules().getKernelQedeqBo(this, modulePaths[i]);
0514 Trace.trace(CLASS, this, method, "synchronizing at prop=" + prop);
0515 if (prop.isLoaded()) {
0516 return (prop);
0517 }
0518 synchronized (prop) {
0519 if (prop.isLoaded()) {
0520 return (prop);
0521 }
0522 try {
0523 if (prop.getModuleAddress().isFileAddress()) {
0524 loadLocalModule(prop);
0525 } else {
0526 // search in local file buffer
0527 try {
0528 getCanonicalReadableFile(prop);
0529 } catch (ModuleFileNotFoundException e) { // file not found
0530 // we will continue by creating a local copy
0531 saveQedeqFromWebToBuffer(prop);
0532 }
0533 loadBufferedModule(prop);
0534 }
0535 // success!
0536 return prop;
0537 } catch (SourceFileExceptionList e) {
0538 Trace.trace(CLASS, this, method, e);
0539 if (i + 1 < modulePaths.length) {
0540 QedeqLog.getInstance().logMessage("trying alternate path");
0541 // we continue with the next path
0542 } else {
0543 // we surrender
0544 throw e;
0545 }
0546 }
0547 }
0548 }
0549 return prop; // never called, only here to soothe the compiler
0550 } catch (final RuntimeException e) {
0551 Trace.fatal(CLASS, this, method, "unexpected problem", e);
0552 QedeqLog.getInstance().logFailureReply("Loading failed",
0553 (prop != null ? prop.getUrl() : "unknownURL"), e.getMessage());
0554 throw e;
0555 } finally {
0556 processDec();
0557 Trace.end(CLASS, this, method);
0558 }
0559 }
0560
0561 public ModuleAddress[] getAllLoadedModules() {
0562 return getModules().getAllLoadedModules();
0563 }
0564
0565 /**
0566 * Load all previously checked QEDEQ modules.
0567 *
0568 * @return Successfully reloaded all modules.
0569 */
0570 public boolean loadPreviouslySuccessfullyLoadedModules() {
0571 processInc();
0572 try {
0573 final String[] list = config.getPreviouslyLoadedModules();
0574 boolean errors = false;
0575 for (int i = 0; i < list.length; i++) {
0576 try {
0577 final ModuleAddress address = getModuleAddress(list[i]);
0578 final QedeqBo prop = loadModule(address);
0579 if (prop.hasErrors()) {
0580 errors = true;
0581 }
0582 } catch (IOException e) {
0583 Trace.fatal(CLASS, this, "loadPreviouslySuccessfullyLoadedModules",
0584 "internal error: " + "saved URLs are malformed", e);
0585 errors = true;
0586 }
0587 }
0588 return !errors;
0589 } finally {
0590 processDec();
0591 }
0592 }
0593
0594 // LATER mime 20070326: dynamic loading from web page directory
0595 public boolean loadAllModulesFromQedeq() {
0596 processInc();
0597 try {
0598 final String prefix = "http://www.qedeq.org/" + kernel.getKernelVersionDirectory() + "/";
0599 final String[] list = new String[] {
0600 prefix + "doc/math/qedeq_logic_v1.xml",
0601 prefix + "doc/math/qedeq_formal_logic_v1.xml",
0602 prefix + "doc/math/qedeq_set_theory_v1.xml",
0603 prefix + "doc/project/qedeq_basic_concept.xml",
0604 prefix + "doc/project/qedeq_logic_language.xml",
0605 prefix + "sample/qedeq_sample1.xml",
0606 prefix + "sample/qedeq_sample2.xml",
0607 prefix + "sample/qedeq_sample3.xml",
0608 prefix + "sample/qedeq_sample4.xml",
0609 prefix + "sample/qedeq_error_sample_00.xml",
0610 prefix + "sample/qedeq_error_sample_01.xml",
0611 prefix + "sample/qedeq_error_sample_02.xml",
0612 prefix + "sample/qedeq_error_sample_03.xml",
0613 prefix + "sample/qedeq_error_sample_04.xml",
0614 prefix + "sample/qedeq_error_sample_05.xml",
0615 prefix + "sample/qedeq_error_sample_12.xml",
0616 prefix + "sample/qedeq_error_sample_13.xml",
0617 prefix + "sample/qedeq_error_sample_14.xml",
0618 prefix + "sample/qedeq_error_sample_15.xml",
0619 prefix + "sample/qedeq_error_sample_16.xml",
0620 prefix + "sample/qedeq_error_sample_17.xml",
0621 prefix + "sample/qedeq_error_sample_18.xml"};
0622 boolean errors = false;
0623 for (int i = 0; i < list.length; i++) {
0624 try {
0625 final ModuleAddress address = getModuleAddress(list[i]);
0626 final QedeqBo prop = loadModule(address);
0627 if (prop.hasErrors()) {
0628 errors = true;
0629 }
0630 } catch (IOException e) {
0631 Trace.fatal(CLASS, this, "loadPreviouslySuccessfullyLoadedModules",
0632 "internal error: " + "saved URLs are malformed", e);
0633 errors = true;
0634 }
0635 }
0636 return !errors;
0637 } finally {
0638 processDec();
0639 }
0640 }
0641
0642 /**
0643 * Make local copy of a module if it is no file address.
0644 *
0645 * @param prop Module properties.
0646 * @throws SourceFileExceptionList Address was malformed or the file can not be found.
0647 */
0648 private void saveQedeqFromWebToBuffer(final DefaultKernelQedeqBo prop)
0649 throws SourceFileExceptionList {
0650 final String method = "saveQedeqFromWebToBuffer(DefaultKernelQedeqBo)";
0651 Trace.begin(CLASS, this, method);
0652
0653 if (prop.getModuleAddress().isFileAddress()) { // this is already a local file
0654 Trace.fatal(CLASS, this, method, "tried to make a local copy for a local module", null);
0655 Trace.end(CLASS, this, method);
0656 return;
0657 }
0658 prop.setLoadingProgressState(this, LoadingState.STATE_LOADING_FROM_WEB);
0659
0660 final File f = getLocalFilePath(prop.getModuleAddress());
0661 try {
0662 UrlUtility.saveUrlToFile(prop.getUrl(), f,
0663 config.getHttpProxyHost(), config.getHttpProxyPort(), config.getHttpNonProxyHosts(),
0664 config.getConnectionTimeout(), config.getReadTimeout(), new LoadingListener() {
0665 public void loadingCompletenessChanged(final double completeness) {
0666 prop.setLoadingCompleteness((int) completeness * 100);
0667 }
0668 });
0669 } catch (IOException e) {
0670 Trace.trace(CLASS, this, method, e);
0671 try {
0672 f.delete();
0673 } catch (Exception ex) {
0674 Trace.trace(CLASS, this, method, ex);
0675 }
0676 final SourceFileExceptionList sfl = createSourceFileExceptionList(
0677 ServiceErrors.LOADING_FROM_WEB_FAILED_CODE,
0678 ServiceErrors.LOADING_FROM_WEB_FAILED_TEXT,
0679 prop.getUrl(), e);
0680 prop.setLoadingFailureState(LoadingState.STATE_LOADING_FROM_WEB_FAILED, sfl);
0681 Trace.trace(CLASS, this, method, "Couldn't access " + prop.getUrl());
0682 throw sfl;
0683 } finally {
0684 Trace.end(CLASS, this, method);
0685 }
0686 }
0687
0688 public final File getLocalFilePath(final ModuleAddress address) {
0689 final String method = "getLocalFilePath(ModuleAddress)";
0690 URL url;
0691 try {
0692 url = new URL(address.getUrl());
0693 } catch (MalformedURLException e) {
0694 Trace.fatal(CLASS, this, method, "Could not get local file path.", e);
0695 return null;
0696 }
0697 Trace.param(CLASS, this, method, "protocol", url.getProtocol());
0698 Trace.param(CLASS, this, method, "host", url.getHost());
0699 Trace.param(CLASS, this, method, "port", url.getPort());
0700 Trace.param(CLASS, this, method, "path", url.getPath());
0701 Trace.param(CLASS, this, method, "file", url.getFile());
0702 if (address.isFileAddress()) {
0703 try {
0704 return UrlUtility.transformURLPathToFilePath(url);
0705 } catch (IllegalArgumentException e) {
0706 // should not occur because check for validy must be done in constructor of address
0707 Trace.fatal(CLASS, this, method, "Loading failed of local file with URL=" + url, e);
0708 throw new RuntimeException(e);
0709 }
0710 }
0711 StringBuffer file = new StringBuffer(url.getFile());
0712 StringUtility.replace(file, "_", "_1"); // remember all '_'
0713 StringUtility.replace(file, "/", "_2"); // preserve all '/'
0714 String encoded = file.toString(); // fallback file name
0715 try {
0716 encoded = URLEncoder.encode(file.toString(), "UTF-8");
0717 } catch (UnsupportedEncodingException e) {
0718 // should not occur
0719 Trace.trace(CLASS, method, e);
0720 }
0721 file.setLength(0);
0722 file.append(encoded);
0723 StringUtility.replace(file, "#", "##"); // escape all '#'
0724 StringUtility.replace(file, "_2", "#"); // from '/' into '#'
0725 StringUtility.replace(file, "_1", "_"); // from '_' into '_'
0726 // mime 2010-06-25: use if we throw no RuntimException
0727 // StringBuffer adr = new StringBuffer(url.toExternalForm());
0728 final StringBuffer adr;
0729 try {
0730 adr = new StringBuffer(new URL(url.getProtocol(), url.getHost(), url.getPort(), file
0731 .toString()).toExternalForm());
0732 } catch (MalformedURLException e) {
0733 Trace.fatal(CLASS, this, method, "unexpected", e);
0734 throw new RuntimeException(e);
0735 }
0736 // escape characters:
0737 StringUtility.replace(adr, "://", "_"); // before host
0738 StringUtility.replace(adr, ":", "_"); // before protocol
0739 return new File(getBufferDirectory(), adr.toString());
0740 }
0741
0742 /**
0743 * Increment intern process counter.
0744 */
0745 private void processInc() {
0746 synchronized (processCounterSync) {
0747 this.processCounter++;
0748 }
0749 }
0750
0751 /**
0752 * Decrement intern process counter.
0753 */
0754 private void processDec() {
0755 synchronized (processCounterSync) {
0756 this.processCounter--;
0757 }
0758 }
0759
0760 public File getBufferDirectory() {
0761 return config.getBufferDirectory();
0762 }
0763
0764 public File getGenerationDirectory() {
0765 return config.getGenerationDirectory();
0766 }
0767
0768 public KernelQedeqBo getKernelQedeqBo(final ModuleAddress address) {
0769 return getModules().getKernelQedeqBo(this, address);
0770 }
0771
0772 public QedeqBo getQedeqBo(final ModuleAddress address) {
0773 return getKernelQedeqBo(address);
0774 }
0775
0776 public ModuleAddress getModuleAddress(final URL url) throws IOException {
0777 return new DefaultModuleAddress(url);
0778 }
0779
0780 public ModuleAddress getModuleAddress(final String url) throws IOException {
0781 return new DefaultModuleAddress(url);
0782 }
0783
0784 public ModuleAddress getModuleAddress(final File file) throws IOException {
0785 return new DefaultModuleAddress(file);
0786 }
0787
0788 public String getSource(final ModuleAddress address) throws IOException {
0789 final KernelQedeqBo bo = getKernelQedeqBo(address);
0790 if (bo.getLoadingState().equals(LoadingState.STATE_UNDEFINED)
0791 || bo.getLoadingState().equals(LoadingState.STATE_LOADING_FROM_WEB)
0792 || bo.getLoadingState().equals(LoadingState.STATE_LOADING_FROM_WEB_FAILED)) {
0793 return null;
0794 }
0795 final StringBuffer buffer = new StringBuffer();
0796 final Reader reader = getQedeqFileDao().getModuleReader(bo);
0797 try {
0798 IoUtility.loadReader(reader, buffer);
0799 } finally {
0800 IoUtility.close(reader);
0801 }
0802 return buffer.toString();
0803 }
0804
0805 public boolean loadRequiredModules(final ModuleAddress address) {
0806 final KernelQedeqBo prop = (KernelQedeqBo) loadModule(address);
0807 // did we check this already?
0808 if (prop.hasLoadedRequiredModules()) {
0809 return true; // everything is OK
0810 }
0811 loadModule(address);
0812 executePlugin(LoadRequiredModulesPlugin.class.getName(), prop, null, null);
0813 return prop.hasLoadedRequiredModules();
0814 }
0815
0816 public boolean loadRequiredModules(final KernelQedeqBo qedeq, final InternalServiceProcess process) {
0817 // did we check this already?
0818 if (qedeq.hasLoadedRequiredModules()) {
0819 return true; // everything is OK
0820 }
0821 executePlugin(LoadRequiredModulesPlugin.class.getName(), qedeq, null, process);
0822 return qedeq.hasLoadedRequiredModules();
0823 }
0824
0825 public boolean checkWellFormedness(final ModuleAddress address) {
0826 final DefaultKernelQedeqBo prop = modules.getKernelQedeqBo(this, address);
0827 // did we check this already?
0828 if (prop.isWellFormed()) {
0829 return true; // everything is OK
0830 }
0831 loadModule(address);
0832 executePlugin(WellFormedCheckerPlugin.class.getName(), prop, null, null);
0833 return prop.isWellFormed();
0834 }
0835
0836 public boolean checkWellFormedness(final KernelQedeqBo qedeq, final InternalServiceProcess process) {
0837 // did we check this already?
0838 if (qedeq.isWellFormed()) {
0839 return true; // everything is OK
0840 }
0841 executePlugin(WellFormedCheckerPlugin.class.getName(), qedeq, null,
0842 process);
0843 return qedeq.isWellFormed();
0844 }
0845
0846 public boolean checkFormallyProved(final ModuleAddress address) {
0847 final DefaultKernelQedeqBo prop = modules.getKernelQedeqBo(this, address);
0848 // did we check this already?
0849 if (prop.isFullyFormallyProved()) {
0850 return true; // everything is OK
0851 }
0852 loadModule(address);
0853 executePlugin(FormalProofCheckerPlugin.class.getName(), prop, null, null);
0854 return prop.isFullyFormallyProved();
0855 }
0856
0857 public boolean checkFormallyProved(final KernelQedeqBo qedeq, final InternalServiceProcess process) {
0858 // did we check this already?
0859 if (qedeq.isFullyFormallyProved()) {
0860 return true; // everything is OK
0861 }
0862 executePlugin(FormalProofCheckerPlugin.class.getName(), qedeq, null, process);
0863 return qedeq.isFullyFormallyProved();
0864 }
0865
0866 /**
0867 * Add plugin to services.
0868 *
0869 * @param pluginClass Plugin class to instantiate.
0870 * @throws RuntimeException Addition failed.
0871 */
0872 public void addPlugin(final String pluginClass) {
0873 pluginManager.addPlugin(pluginClass);
0874 }
0875
0876 public Plugin[] getPlugins() {
0877 return pluginManager.getNonInternalPlugins();
0878 }
0879
0880 public Object executePlugin(final String id, final ModuleAddress address, final Object data) {
0881 loadModule(address);
0882 return processManager.executePlugin(id, getKernelQedeqBo(address), data, null);
0883 }
0884
0885 public Object executePlugin(final String id, final KernelQedeqBo qedeq, final Object data,
0886 final InternalServiceProcess process) {
0887 return processManager.executePlugin(id, qedeq, data, process);
0888 }
0889
0890 public void clearAllPluginResults(final ModuleAddress address) {
0891 pluginManager.clearAllPluginResults(getKernelQedeqBo(address));
0892 }
0893
0894 public ServiceProcess[] getServiceProcesses() {
0895 return processManager.getServiceProcesses();
0896 }
0897
0898 public ServiceProcess[] getRunningServiceProcesses() {
0899 return processManager.getRunningServiceProcesses();
0900 }
0901
0902 public void stopAllPluginExecutions() {
0903 processManager.terminateAllServiceProcesses();
0904 }
0905
0906
0907 /**
0908 * Get all loaded QEDEQ modules.
0909 *
0910 * @return All QEDEQ modules.
0911 */
0912 private KernelQedeqBoStorage getModules() {
0913 return modules;
0914 }
0915
0916 public SourceFileExceptionList createSourceFileExceptionList(final int code,
0917 final String message, final String address, final IOException e) {
0918 return new SourceFileExceptionList(new SourceFileException(this,
0919 code, message, e, new SourceArea(address), null));
0920 }
0921
0922 public SourceFileExceptionList createSourceFileExceptionList(final int code,
0923 final String message, final String address, final RuntimeException e) {
0924 return new SourceFileExceptionList(new SourceFileException(this,
0925 code, message, e, new SourceArea(address), null));
0926 }
0927
0928 public SourceFileExceptionList createSourceFileExceptionList(final int code,
0929 final String message, final String address, final Exception e) {
0930 return new SourceFileExceptionList(new SourceFileException(this,
0931 code, message, e, new SourceArea(address), null));
0932 }
0933
0934 /**
0935 * Get description of source file exception list.
0936 *
0937 * @param address Get description for this module exceptions.
0938 * @return Error description and location.
0939 */
0940 public String[] getSourceFileExceptionList(final ModuleAddress address) {
0941 final List list = new ArrayList();
0942 final KernelQedeqBo bo = getKernelQedeqBo(address);
0943 final SourceFileExceptionList sfl = bo.getErrors();
0944 if (sfl.size() > 0) {
0945 final StringBuffer buffer = new StringBuffer();
0946 do {
0947 Reader reader = null;
0948 try {
0949 reader = getQedeqFileDao().getModuleReader(bo);
0950 IoUtility.loadReader(reader, buffer);
0951 } catch (IOException e) {
0952 IoUtility.close(reader);
0953 for (int i = 0; i < sfl.size(); i++) {
0954 list.add(sfl.get(i).getDescription());
0955 }
0956 break; // out of do while
0957 }
0958 final TextInput input = new TextInput(buffer);
0959 try {
0960 input.setPosition(0);
0961 final StringBuffer buf = new StringBuffer();
0962 for (int i = 0; i < sfl.size(); i++) {
0963 buf.setLength(0);
0964 final SourceFileException sf = sfl.get(i);
0965 buf.append(sf.getDescription());
0966 try {
0967 if (sf.getSourceArea() != null
0968 && sf.getSourceArea().getStartPosition() != null) {
0969 buf.append("\n");
0970 input.setRow(sf.getSourceArea().getStartPosition().getRow());
0971 buf.append(StringUtility.replace(input.getLine(), "\t", " "));
0972 buf.append("\n");
0973 final StringBuffer whitespace = StringUtility.getSpaces(sf
0974 .getSourceArea().getStartPosition().getColumn() - 1);
0975 buffer.append(whitespace);
0976 buffer.append("^");
0977 }
0978 } catch (Exception e) {
0979 Trace.trace(CLASS, this, "getSourceFileExceptionList(ModuleAddress)", e);
0980 }
0981 list.add(buf.toString());
0982 }
0983 } finally {
0984 IoUtility.close(input);
0985 }
0986 break; // out of do while
0987 } while (true);
0988 }
0989 return (String[]) list.toArray(new String[list.size()]);
0990 }
0991
0992 public String getPluginId() {
0993 return CLASS.getName();
0994 }
0995
0996 public String getPluginActionName() {
0997 return "Basis";
0998 }
0999 public QedeqFileDao getQedeqFileDao() {
1000 return qedeqFileDao;
1001 }
1002
1003 public String getPluginDescription() {
1004 return "provides basic services for loading QEDEQ modules";
1005 }
1006
1007 public QedeqConfig getConfig() {
1008 return config;
1009 }
1010
1011 public String getKernelVersionDirectory() {
1012 return kernel.getKernelVersionDirectory();
1013 }
1014
1015 public String getBuildId() {
1016 return kernel.getBuildId();
1017 }
1018
1019 public String getDedication() {
1020 return kernel.getDedication();
1021 }
1022
1023 public String getDescriptiveKernelVersion() {
1024 return kernel.getDescriptiveKernelVersion();
1025 }
1026
1027 public String getKernelCodeName() {
1028 return kernel.getKernelCodeName();
1029 }
1030
1031 public String getKernelVersion() {
1032 return kernel.getKernelVersion();
1033 }
1034
1035 public String getMaximalRuleVersion() {
1036 return kernel.getMaximalRuleVersion();
1037 }
1038
1039 public boolean isRuleVersionSupported(final String ruleVersion) {
1040 return kernel.isRuleVersionSupported(ruleVersion);
1041 }
1042
1043 public boolean isSetConnectionTimeOutSupported() {
1044 return kernel.isSetConnectionTimeOutSupported();
1045 }
1046
1047 public boolean isSetReadTimeoutSupported() {
1048 return kernel.isSetReadTimeoutSupported();
1049 }
1050
1051 public ContextChecker getContextChecker() {
1052 return contextChecker;
1053 }
1054
1055 /**
1056 * Set the context checker. This is useful especially for test classes.
1057 *
1058 * @param contextChecker We check the context with this checker now.
1059 */
1060 public void setContextChecker(final ContextChecker contextChecker) {
1061 this.contextChecker = contextChecker;
1062 }
1063
1064 }
|