001 /* This file is part of the project "Hilbert II" - http://www.qedeq.org
002 *
003 * Copyright 2000-2013, 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.module;
017
018 import java.io.File;
019 import java.io.IOException;
020
021 import org.qedeq.kernel.bo.common.KernelProperties;
022 import org.qedeq.kernel.se.base.module.Specification;
023 import org.qedeq.kernel.se.common.ModuleAddress;
024 import org.qedeq.kernel.se.common.SourceFileExceptionList;
025 import org.qedeq.kernel.se.config.QedeqConfig;
026 import org.qedeq.kernel.se.visitor.ContextChecker;
027
028 /**
029 * The kernel internal service methods are assembled here. Needed by the kernel and its helpers.
030 *
031 * @author Michael Meyling
032 */
033 public interface InternalKernelServices extends KernelProperties {
034
035 /**
036 * Get access to configuration parameters.
037 *
038 * @return Configuration access.
039 */
040 public QedeqConfig getConfig();
041
042 /**
043 * Get buffer directory for QEDEQ module files.
044 *
045 * @return buffer directory.
046 */
047 public File getBufferDirectory();
048
049 /**
050 * Get directory for generated files.
051 *
052 * @return Generation directory.
053 */
054 public File getGenerationDirectory();
055
056 /**
057 * Get {@link KernelQedeqBo} for an address.
058 *
059 * @param address Look for this address.
060 * @return Existing or new {@link KernelQedeqBo}, if address is malformed
061 * <code>null</code> is returned.
062 */
063 public KernelQedeqBo getKernelQedeqBo(ModuleAddress address);
064
065 /**
066 * Transform an URL address into a local file path where the QEDEQ module is buffered.
067 * If the QEDEQ module is a local file the path to that file is given.
068 *
069 * @param address Get local address for this QEDEQ module address.
070 * @return Local file path for that <code>address</code>.
071 */
072 public File getLocalFilePath(ModuleAddress address);
073
074 /**
075 * Load specified QEDEQ module from QEDEQ parent module.
076 *
077 * @param parent Parent module address.
078 * @param spec Specification for another QEDEQ module.
079 * @return Loaded module.
080 * @throws SourceFileExceptionList Loading failed.
081 */
082 public KernelQedeqBo loadModule(ModuleAddress parent, Specification spec)
083 throws SourceFileExceptionList;
084
085 /**
086 * Get required modules of given module. You can check the status to know if the loading was
087 * successful.
088 *
089 * @param qedeq Module to check.
090 * @param process Working process.
091 * @return Successful loading.
092 */
093 public boolean loadRequiredModules(KernelQedeqBo qedeq, InternalServiceProcess process);
094
095 /**
096 * Check if all formulas of a QEDEQ module and its required modules are well formed.
097 *
098 * @param qedeq Module to check.
099 * @param process Working process.
100 * @return Was check successful?
101 */
102 public boolean checkWellFormedness(KernelQedeqBo qedeq, InternalServiceProcess process);
103
104 /**
105 * Check if all propositions of this and all required modules have correct formal proofs.
106 *
107 * @param qedeq Module to check.
108 * @param process Working process.
109 * @return Was check successful?
110 */
111 public boolean checkFormallyProved(KernelQedeqBo qedeq, InternalServiceProcess process);
112
113 /**
114 * Execute plugin on given QEDEQ module.
115 *
116 * @param id Plugin id.
117 * @param qedeq QEDEQ module.
118 * @param data Process data. Additional data beside module.
119 * @param parent Parent service process. Might be <code>null</code>
120 * @return Plugin specific resulting object. Might be <code>null</code>.
121 */
122 public Object executePlugin(final String id, final KernelQedeqBo qedeq, final Object data,
123 final InternalServiceProcess parent);
124
125 /**
126 * Get DAO for reading and writing QEDEQ modules from or to a file.
127 *
128 * @return DAO.
129 */
130 public QedeqFileDao getQedeqFileDao();
131
132 /**
133 * Creates a list with a {@link org.qedeq.kernel.se.common.SourceFileException} with dummy
134 * position.
135 *
136 * @param address This source had a problem.
137 * @param code Failure code.
138 * @param message Textual description of failure.
139 * @param e Wrapped exception.
140 * @return Created list.
141 */
142 public SourceFileExceptionList createSourceFileExceptionList(int code, String message,
143 String address, IOException e);
144
145 /**
146 * Creates a list with a {@link org.qedeq.kernel.se.common.SourceFileException} with dummy
147 * position.
148 *
149 * @param address This source had a problem.
150 * @param code Failure code.
151 * @param message Textual description of failure.
152 * @param e Wrapped exception.
153 * @return Created list.
154 */
155 public SourceFileExceptionList createSourceFileExceptionList(int code, String message,
156 String address, RuntimeException e);
157
158 /**
159 * Creates a list with a {@link org.qedeq.kernel.se.common.SourceFileException} with dummy
160 * position.
161 *
162 * @param address This source had a problem.
163 * @param code Failure code.
164 * @param message Textual description of failure.
165 * @param e Wrapped exception.
166 * @return Created list.
167 */
168 public SourceFileExceptionList createSourceFileExceptionList(int code, String message,
169 String address, Exception e);
170
171 /**
172 * Get context checker.
173 *
174 * @return Checker for testing if context is valid.
175 */
176 public ContextChecker getContextChecker();
177
178 }
|