0001 /* This file is part of the project "Hilbert II" - http://www.qedeq.org
0002 *
0003 * Copyright 2000-2011, 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 org.qedeq.kernel.se.base.list.Atom;
0019 import org.qedeq.kernel.se.base.list.Element;
0020 import org.qedeq.kernel.se.base.list.ElementList;
0021 import org.qedeq.kernel.se.base.module.Add;
0022 import org.qedeq.kernel.se.base.module.Author;
0023 import org.qedeq.kernel.se.base.module.AuthorList;
0024 import org.qedeq.kernel.se.base.module.Axiom;
0025 import org.qedeq.kernel.se.base.module.Chapter;
0026 import org.qedeq.kernel.se.base.module.ChapterList;
0027 import org.qedeq.kernel.se.base.module.Existential;
0028 import org.qedeq.kernel.se.base.module.FormalProof;
0029 import org.qedeq.kernel.se.base.module.FormalProofLine;
0030 import org.qedeq.kernel.se.base.module.FormalProofLineList;
0031 import org.qedeq.kernel.se.base.module.FormalProofList;
0032 import org.qedeq.kernel.se.base.module.Formula;
0033 import org.qedeq.kernel.se.base.module.FunctionDefinition;
0034 import org.qedeq.kernel.se.base.module.Header;
0035 import org.qedeq.kernel.se.base.module.Import;
0036 import org.qedeq.kernel.se.base.module.ImportList;
0037 import org.qedeq.kernel.se.base.module.InitialFunctionDefinition;
0038 import org.qedeq.kernel.se.base.module.InitialPredicateDefinition;
0039 import org.qedeq.kernel.se.base.module.Latex;
0040 import org.qedeq.kernel.se.base.module.LatexList;
0041 import org.qedeq.kernel.se.base.module.LinkList;
0042 import org.qedeq.kernel.se.base.module.LiteratureItem;
0043 import org.qedeq.kernel.se.base.module.LiteratureItemList;
0044 import org.qedeq.kernel.se.base.module.Location;
0045 import org.qedeq.kernel.se.base.module.LocationList;
0046 import org.qedeq.kernel.se.base.module.ModusPonens;
0047 import org.qedeq.kernel.se.base.module.Node;
0048 import org.qedeq.kernel.se.base.module.PredicateDefinition;
0049 import org.qedeq.kernel.se.base.module.Proof;
0050 import org.qedeq.kernel.se.base.module.ProofList;
0051 import org.qedeq.kernel.se.base.module.Proposition;
0052 import org.qedeq.kernel.se.base.module.Qedeq;
0053 import org.qedeq.kernel.se.base.module.Reason;
0054 import org.qedeq.kernel.se.base.module.ReasonType;
0055 import org.qedeq.kernel.se.base.module.Rename;
0056 import org.qedeq.kernel.se.base.module.Rule;
0057 import org.qedeq.kernel.se.base.module.Section;
0058 import org.qedeq.kernel.se.base.module.SectionList;
0059 import org.qedeq.kernel.se.base.module.Specification;
0060 import org.qedeq.kernel.se.base.module.Subsection;
0061 import org.qedeq.kernel.se.base.module.SubsectionList;
0062 import org.qedeq.kernel.se.base.module.SubstFree;
0063 import org.qedeq.kernel.se.base.module.SubstFunc;
0064 import org.qedeq.kernel.se.base.module.SubstPred;
0065 import org.qedeq.kernel.se.base.module.Universal;
0066 import org.qedeq.kernel.se.base.module.UsedByList;
0067 import org.qedeq.kernel.se.common.IllegalModuleDataException;
0068 import org.qedeq.kernel.se.common.ModuleAddress;
0069 import org.qedeq.kernel.se.common.ModuleContext;
0070 import org.qedeq.kernel.se.common.ModuleDataException;
0071 import org.qedeq.kernel.se.dto.list.DefaultAtom;
0072 import org.qedeq.kernel.se.dto.list.DefaultElementList;
0073 import org.qedeq.kernel.se.dto.module.AddVo;
0074 import org.qedeq.kernel.se.dto.module.AuthorListVo;
0075 import org.qedeq.kernel.se.dto.module.AuthorVo;
0076 import org.qedeq.kernel.se.dto.module.AxiomVo;
0077 import org.qedeq.kernel.se.dto.module.ChapterListVo;
0078 import org.qedeq.kernel.se.dto.module.ChapterVo;
0079 import org.qedeq.kernel.se.dto.module.ExistentialVo;
0080 import org.qedeq.kernel.se.dto.module.FormalProofLineListVo;
0081 import org.qedeq.kernel.se.dto.module.FormalProofLineVo;
0082 import org.qedeq.kernel.se.dto.module.FormalProofListVo;
0083 import org.qedeq.kernel.se.dto.module.FormalProofVo;
0084 import org.qedeq.kernel.se.dto.module.FormulaVo;
0085 import org.qedeq.kernel.se.dto.module.FunctionDefinitionVo;
0086 import org.qedeq.kernel.se.dto.module.HeaderVo;
0087 import org.qedeq.kernel.se.dto.module.ImportListVo;
0088 import org.qedeq.kernel.se.dto.module.ImportVo;
0089 import org.qedeq.kernel.se.dto.module.InitialFunctionDefinitionVo;
0090 import org.qedeq.kernel.se.dto.module.InitialPredicateDefinitionVo;
0091 import org.qedeq.kernel.se.dto.module.LatexListVo;
0092 import org.qedeq.kernel.se.dto.module.LatexVo;
0093 import org.qedeq.kernel.se.dto.module.LinkListVo;
0094 import org.qedeq.kernel.se.dto.module.LiteratureItemListVo;
0095 import org.qedeq.kernel.se.dto.module.LiteratureItemVo;
0096 import org.qedeq.kernel.se.dto.module.LocationListVo;
0097 import org.qedeq.kernel.se.dto.module.LocationVo;
0098 import org.qedeq.kernel.se.dto.module.ModusPonensVo;
0099 import org.qedeq.kernel.se.dto.module.NodeVo;
0100 import org.qedeq.kernel.se.dto.module.PredicateDefinitionVo;
0101 import org.qedeq.kernel.se.dto.module.ProofListVo;
0102 import org.qedeq.kernel.se.dto.module.ProofVo;
0103 import org.qedeq.kernel.se.dto.module.PropositionVo;
0104 import org.qedeq.kernel.se.dto.module.QedeqVo;
0105 import org.qedeq.kernel.se.dto.module.ReasonTypeVo;
0106 import org.qedeq.kernel.se.dto.module.RenameVo;
0107 import org.qedeq.kernel.se.dto.module.RuleVo;
0108 import org.qedeq.kernel.se.dto.module.SectionListVo;
0109 import org.qedeq.kernel.se.dto.module.SectionVo;
0110 import org.qedeq.kernel.se.dto.module.SpecificationVo;
0111 import org.qedeq.kernel.se.dto.module.SubsectionListVo;
0112 import org.qedeq.kernel.se.dto.module.SubsectionVo;
0113 import org.qedeq.kernel.se.dto.module.SubstFreeVo;
0114 import org.qedeq.kernel.se.dto.module.SubstFuncVo;
0115 import org.qedeq.kernel.se.dto.module.SubstPredVo;
0116 import org.qedeq.kernel.se.dto.module.UniversalVo;
0117 import org.qedeq.kernel.se.dto.module.UsedByListVo;
0118
0119
0120 /**
0121 * FIXME 20110125 m31: why do we need this builder? To make copies. Why don't we take the original?
0122 * At least use director pattern or transfer creation methods into BOs or use visitor pattern!
0123 * We have lots of duplicate code here!
0124 * <p>
0125 * An builder for creating {@link org.qedeq.kernel.se.dto.module.QedeqVo}s. This builder takes
0126 * something that implements the QEDEQ interfaces (beginning with
0127 * (@link org.qedeq.kernel.base.module.Qedeq} and makes copies that are out of the package
0128 * <code>org.qedeq.kernel.dto.*</code>. Only elements that are not <code>null</code> are
0129 * copied.
0130
0131 * @author Michael Meyling
0132 */
0133 public class QedeqVoBuilder {
0134
0135 /** QEDEQ module input object. */
0136 private Qedeq original;
0137
0138 /** Current context during creation. */
0139 private ModuleContext currentContext;
0140
0141 /**
0142 * Constructor.
0143 *
0144 * @param address QEDEQ address.
0145 */
0146 protected QedeqVoBuilder(final ModuleAddress address) {
0147 this.currentContext = address.createModuleContext();
0148 }
0149
0150 /**
0151 * Create {@link QedeqVo} out of an {@link Qedeq} instance.
0152 * The resulting object has no references to the original {@link Qedeq} instance.
0153 * <p>
0154 * During the creation process the caller must assert that no modifications are made
0155 * to the {@link Qedeq} instance including its referenced objects.
0156 *
0157 * @param address Module address.
0158 * @param original Basic QEDEQ module object.
0159 * @return Created copy object.
0160 * @throws ModuleDataException Invalid data found.
0161 */
0162 public static QedeqVo createQedeq(final ModuleAddress address,
0163 final Qedeq original) throws ModuleDataException {
0164 final QedeqVoBuilder creator = new QedeqVoBuilder(address);
0165 QedeqVo vo = creator.create(original);
0166 return vo;
0167 }
0168
0169 /**
0170 * Create {@linkQedeqVo} out of an {@link Qedeq} instance.
0171 * During that procedure some basic checking is done. E.g. the uniqueness of entries
0172 * is tested. The resulting business object has no references to the original
0173 * {@link Qedeq} instance.
0174 *
0175 * <p>
0176 * During the creation process the caller must assert that no modifications are made
0177 * to the {@link Qedeq} instance including its referenced objects.
0178 *
0179 * @param original Basic QEDEQ module object.
0180 * @return Copied QEDEQ object.
0181 * @throws IllegalModuleDataException Basic semantic error occurred.
0182 */
0183 protected final QedeqVo create(final Qedeq original) throws IllegalModuleDataException {
0184 this.original = original;
0185 getCurrentContext().setLocationWithinModule("");
0186 QedeqVo qedeq;
0187 if (original == null) {
0188 qedeq = null;
0189 return qedeq;
0190 }
0191 qedeq = new QedeqVo();
0192 final String context = getCurrentContext().getLocationWithinModule();
0193 if (original.getHeader() != null) {
0194 getCurrentContext().setLocationWithinModule(context + "getHeader()");
0195 qedeq.setHeader(create(original.getHeader()));
0196 }
0197 if (original.getChapterList() != null) {
0198 getCurrentContext().setLocationWithinModule(context + "getChapterList()");
0199 qedeq.setChapterList(create(original.getChapterList()));
0200 }
0201 if (original.getLiteratureItemList() != null) {
0202 getCurrentContext().setLocationWithinModule(context + "getLiteratureItemList()");
0203 qedeq.setLiteratureItemList(create(original.getLiteratureItemList()));
0204 }
0205 return qedeq;
0206 }
0207
0208 /**
0209 * Create {@link HeaderVo} out of an {@link Header} instance.
0210 * During that procedure some basic checking is done. E.g. the uniqueness of entries
0211 * is tested. The resulting business object has no references to the original
0212 * {@link Header} instance.
0213 * <p>
0214 * During the creation process the caller must assert that no modifications are made
0215 * to the {@link Header} instance including its referenced objects.
0216 *
0217 * @param header Basic header object.
0218 * @return Filled header business object. Is equal to the parameter <code>header</code>.
0219 * @throws IllegalModuleDataException Basic semantic error occurred.
0220 */
0221 private final HeaderVo create(final Header header)
0222 throws IllegalModuleDataException {
0223 if (header == null) {
0224 return null;
0225 }
0226 final HeaderVo h = new HeaderVo();
0227 final String context = getCurrentContext().getLocationWithinModule();
0228 if (header.getTitle() != null) {
0229 setLocationWithinModule(context + ".getTitle()");
0230 h.setTitle(create(header.getTitle()));
0231 }
0232 if (header.getAuthorList() != null) {
0233 setLocationWithinModule(context + ".getAuthorList()");
0234 h.setAuthorList(create(header.getAuthorList()));
0235 }
0236 if (header.getSummary() != null) {
0237 setLocationWithinModule(context + ".getSummary()");
0238 h.setSummary(create(header.getSummary()));
0239 }
0240 if (header.getEmail() != null) {
0241 setLocationWithinModule(context + ".getEmail()");
0242 h.setEmail(header.getEmail());
0243 }
0244 if (header.getSpecification() != null) {
0245 setLocationWithinModule(context + ".getSpecification()");
0246 h.setSpecification(create(header.getSpecification()));
0247 }
0248 if (header.getImportList() != null) {
0249 setLocationWithinModule(context + ".getImportList()");
0250 h.setImportList(create(header.getImportList()));
0251 }
0252 if (header.getUsedByList() != null) {
0253 setLocationWithinModule(context + ".getUsedByList()");
0254 h.setUsedByList(create(header.getUsedByList()));
0255 }
0256 setLocationWithinModule(context);
0257 return h;
0258 }
0259
0260 /**
0261 * Create {@link UsedByListVo} out of an {@link UsedByList} instance.
0262 * During that procedure some basic checking is done. E.g. the uniqueness of entries
0263 * is tested. The resulting business object has no references to the original
0264 * {@link UsedByList} instance.
0265 * <p>
0266 * During the creation process the caller must assert that no modifications are made
0267 * to the {@link UsedByList} instance including its referenced objects.
0268 *
0269 * @param usedByList Basic header object.
0270 * @return Filled used by business object. Is equal to the parameter <code>usedByList</code>.
0271 */
0272 private final UsedByListVo create(final UsedByList usedByList) {
0273 if (usedByList == null) {
0274 return null;
0275 }
0276 final String context = getCurrentContext().getLocationWithinModule();
0277 final UsedByListVo list = new UsedByListVo();
0278 for (int i = 0; i < usedByList.size(); i++) {
0279 setLocationWithinModule(context + ".get(" + i + ")");
0280 list.add(create(usedByList.get(i)));
0281 }
0282 setLocationWithinModule(context);
0283 return list;
0284 }
0285
0286 private final ImportListVo create(final ImportList importList) {
0287 if (importList == null) {
0288 return null;
0289 }
0290 final String context = getCurrentContext().getLocationWithinModule();
0291 final ImportListVo list = new ImportListVo();
0292 for (int i = 0; i < importList.size(); i++) {
0293 setLocationWithinModule(context + ".get(" + i + ")");
0294 list.add(create(importList.get(i)));
0295 }
0296 setLocationWithinModule(context);
0297 return list;
0298 }
0299
0300 private final ImportVo create(final Import imp) {
0301 if (imp == null) {
0302 return null;
0303 }
0304 final ImportVo i = new ImportVo();
0305 final String context = getCurrentContext().getLocationWithinModule();
0306 if (imp.getLabel() != null) {
0307 setLocationWithinModule(context + ".getLabel()");
0308 i.setLabel(imp.getLabel());
0309 }
0310 if (imp.getSpecification() != null) {
0311 setLocationWithinModule(context + ".getSpecification()");
0312 i.setSpecification(create(imp.getSpecification()));
0313 }
0314 setLocationWithinModule(context);
0315 return i;
0316 }
0317
0318 private final SpecificationVo create(final Specification specification) {
0319 if (specification == null) {
0320 return null;
0321 }
0322 final SpecificationVo s = new SpecificationVo();
0323 final String context = getCurrentContext().getLocationWithinModule();
0324 if (specification.getName() != null) {
0325 setLocationWithinModule(context + ".getName()");
0326 s.setName(specification.getName());
0327 }
0328 if (specification.getRuleVersion() != null) {
0329 setLocationWithinModule(context + ".getRuleVersion()");
0330 s.setRuleVersion(specification.getRuleVersion());
0331 }
0332 if (specification.getLocationList() != null) {
0333 setLocationWithinModule(context + ".getLocationList()");
0334 s.setLocationList(create(specification.getLocationList()));
0335 }
0336 setLocationWithinModule(context);
0337 return s;
0338 }
0339
0340 private final LocationListVo create(final LocationList locationList) {
0341 if (locationList == null) {
0342 return null;
0343 }
0344 final LocationListVo list = new LocationListVo();
0345 final String context = getCurrentContext().getLocationWithinModule();
0346 for (int i = 0; i < locationList.size(); i++) {
0347 setLocationWithinModule(context + ".get(" + i + ")");
0348 list.add(create(locationList.get(i)));
0349 }
0350 setLocationWithinModule(context);
0351 return list;
0352 }
0353
0354 private final LocationVo create(final Location location) {
0355 if (location == null) {
0356 return null;
0357 }
0358 final LocationVo loc = new LocationVo();
0359 final String context = getCurrentContext().getLocationWithinModule();
0360 if (location.getLocation() != null) {
0361 setLocationWithinModule(context + ".getLocation()");
0362 loc.setLocation(location.getLocation());
0363 }
0364 setLocationWithinModule(context);
0365 return loc;
0366 }
0367
0368 private final AuthorListVo create(final AuthorList authorList) {
0369 if (authorList == null) {
0370 return null;
0371 }
0372 final AuthorListVo list = new AuthorListVo();
0373 final String context = getCurrentContext().getLocationWithinModule();
0374 for (int i = 0; i < authorList.size(); i++) {
0375 setLocationWithinModule(context + ".get(" + i + ")");
0376 list.add(create(authorList.get(i)));
0377 }
0378 setLocationWithinModule(context);
0379 return list;
0380 }
0381
0382 private final AuthorVo create(final Author author) {
0383 if (author == null) {
0384 return null;
0385 }
0386 final AuthorVo a = new AuthorVo();
0387 final String context = getCurrentContext().getLocationWithinModule();
0388 if (author.getName() != null) {
0389 setLocationWithinModule(context + ".getName()");
0390 a.setName(create(author.getName()));
0391 }
0392 if (author.getEmail() != null) {
0393 setLocationWithinModule(context + ".getEmail()");
0394 a.setEmail(author.getEmail());
0395 }
0396 setLocationWithinModule(context);
0397 return a;
0398 }
0399
0400 private final ChapterListVo create(final ChapterList chapterList)
0401 throws IllegalModuleDataException {
0402 if (chapterList == null) {
0403 return null;
0404 }
0405 final ChapterListVo list = new ChapterListVo();
0406 final String context = getCurrentContext().getLocationWithinModule();
0407 for (int i = 0; i < chapterList.size(); i++) {
0408 setLocationWithinModule(context + ".get(" + i + ")");
0409 list.add(create(chapterList.get(i)));
0410 }
0411 setLocationWithinModule(context);
0412 return list;
0413 }
0414
0415 private final ChapterVo create(final Chapter chapter)
0416 throws IllegalModuleDataException {
0417 if (chapter == null) {
0418 return null;
0419 }
0420 final ChapterVo c = new ChapterVo();
0421 final String context = getCurrentContext().getLocationWithinModule();
0422 if (chapter.getTitle() != null) {
0423 setLocationWithinModule(context + ".getTitle()");
0424 c.setTitle(create(chapter.getTitle()));
0425 }
0426 if (chapter.getNoNumber() != null) {
0427 setLocationWithinModule(context + ".getNoNumber()");
0428 c.setNoNumber(chapter.getNoNumber());
0429 }
0430 if (chapter.getIntroduction() != null) {
0431 setLocationWithinModule(context + ".getIntroduction()");
0432 c.setIntroduction(create(chapter.getIntroduction()));
0433 }
0434 if (chapter.getSectionList() != null) {
0435 setLocationWithinModule(context + ".getSectionList()");
0436 c.setSectionList(create(chapter.getSectionList()));
0437 }
0438 setLocationWithinModule(context);
0439 return c;
0440 }
0441
0442 private LiteratureItemListVo create(final LiteratureItemList literatureItemList)
0443 throws IllegalModuleDataException {
0444 if (literatureItemList == null) {
0445 return null;
0446 }
0447 final LiteratureItemListVo list = new LiteratureItemListVo();
0448 final String context = getCurrentContext().getLocationWithinModule();
0449 for (int i = 0; i < literatureItemList.size(); i++) {
0450 setLocationWithinModule(context + ".get(" + i + ")");
0451 list.add(create(literatureItemList.get(i)));
0452 }
0453 setLocationWithinModule(context);
0454 return list;
0455 }
0456
0457 private LiteratureItemVo create(final LiteratureItem item)
0458 throws IllegalModuleDataException {
0459 if (item == null) {
0460 return null;
0461 }
0462 final LiteratureItemVo it = new LiteratureItemVo();
0463 final String context = getCurrentContext().getLocationWithinModule();
0464 if (item.getLabel() != null) {
0465 setLocationWithinModule(context + ".getLabel()");
0466 it.setLabel(item.getLabel());
0467 }
0468 if (item.getItem() != null) {
0469 setLocationWithinModule(context + ".getItem()");
0470 it.setItem(create(item.getItem()));
0471 }
0472 setLocationWithinModule(context);
0473 return it;
0474
0475 }
0476
0477 private final SectionListVo create(final SectionList sectionList)
0478 throws IllegalModuleDataException {
0479 if (sectionList == null) {
0480 return null;
0481 }
0482 final SectionListVo list = new SectionListVo();
0483 final String context = getCurrentContext().getLocationWithinModule();
0484 for (int i = 0; i < sectionList.size(); i++) {
0485 setLocationWithinModule(context + ".get(" + i + ")");
0486 list.add(create(sectionList.get(i)));
0487 }
0488 setLocationWithinModule(context);
0489 return list;
0490 }
0491
0492 private final SectionVo create(final Section section)
0493 throws IllegalModuleDataException {
0494 if (section == null) {
0495 return null;
0496 }
0497 final SectionVo s = new SectionVo();
0498 final String context = getCurrentContext().getLocationWithinModule();
0499 if (section.getTitle() != null) {
0500 setLocationWithinModule(context + ".getTitle()");
0501 s.setTitle(create(section.getTitle()));
0502 }
0503 if (section.getNoNumber() != null) {
0504 setLocationWithinModule(context + ".getNoNumber()");
0505 s.setNoNumber(section.getNoNumber());
0506 }
0507 if (section.getIntroduction() != null) {
0508 setLocationWithinModule(context + ".getIntroduction()");
0509 s.setIntroduction(create(section.getIntroduction()));
0510 }
0511 if (section.getSubsectionList() != null) {
0512 setLocationWithinModule(context + ".getSubsectionList()");
0513 s.setSubsectionList(create(section.getSubsectionList()));
0514 }
0515 setLocationWithinModule(context);
0516 return s;
0517 }
0518
0519 private final SubsectionListVo create(final SubsectionList subsectionList)
0520 throws IllegalModuleDataException {
0521 if (subsectionList == null) {
0522 return null;
0523 }
0524 final SubsectionListVo list = new SubsectionListVo();
0525 final String context = getCurrentContext().getLocationWithinModule();
0526 for (int i = 0; i < subsectionList.size(); i++) {
0527 setLocationWithinModule(context + ".get(" + i + ")");
0528 // TODO mime 20050608: here the Subsection context is type dependently specified
0529 if (subsectionList.get(i) instanceof Subsection) {
0530 list.add(create((Subsection) subsectionList.get(i)));
0531 } else if (subsectionList.get(i) instanceof Node) {
0532 list.add(create((Node) subsectionList.get(i)));
0533 } else {
0534 throw new IllegalArgumentException("unexpected subsection type: "
0535 + subsectionList.get(i).getClass());
0536 }
0537 }
0538 setLocationWithinModule(context);
0539 return list;
0540 }
0541
0542 private final SubsectionVo create(final Subsection subsection) {
0543 if (subsection == null) {
0544 return null;
0545 }
0546 final SubsectionVo s = new SubsectionVo();
0547 final String context = getCurrentContext().getLocationWithinModule();
0548 if (subsection.getId() != null) {
0549 setLocationWithinModule(context + ".getId()");
0550 s.setId(subsection.getId());
0551 }
0552 if (subsection.getLevel() != null) {
0553 setLocationWithinModule(context + ".getLevel()");
0554 s.setLevel(subsection.getLevel());
0555 }
0556 if (subsection.getTitle() != null) {
0557 setLocationWithinModule(context + ".getTitle()");
0558 s.setTitle(create(subsection.getTitle()));
0559 }
0560 if (subsection.getLatex() != null) {
0561 setLocationWithinModule(context + ".getLatex()");
0562 s.setLatex(create(subsection.getLatex()));
0563 }
0564 setLocationWithinModule(context);
0565 return s;
0566 }
0567
0568 private final NodeVo create(final Node node)
0569 throws IllegalModuleDataException {
0570 if (node == null) {
0571 return null;
0572 }
0573 final NodeVo n = new NodeVo();
0574 final String context = getCurrentContext().getLocationWithinModule();
0575 if (node.getName() != null) {
0576 setLocationWithinModule(context + ".getName()");
0577 n.setName(create(node.getName()));
0578 }
0579 if (node.getId() != null) {
0580 setLocationWithinModule(context + ".getId()");
0581 n.setId(node.getId());
0582 }
0583 if (node.getLevel() != null) {
0584 setLocationWithinModule(context + ".getLevel()");
0585 n.setLevel(node.getLevel());
0586 }
0587 if (node.getTitle() != null) {
0588 setLocationWithinModule(context + ".getTitle()");
0589 n.setTitle(create(node.getTitle()));
0590 }
0591 if (node.getPrecedingText() != null) {
0592 setLocationWithinModule(context + ".getPrecedingText()");
0593 n.setPrecedingText(create(node.getPrecedingText()));
0594 }
0595 if (node.getNodeType() != null) {
0596 setLocationWithinModule(context + ".getNodeType()");
0597 if (node.getNodeType() instanceof Axiom) {
0598 setLocationWithinModule(context + ".getNodeType().getAxiom()");
0599 n.setNodeType(create((Axiom) node.getNodeType()));
0600 } else if (node.getNodeType() instanceof InitialPredicateDefinition) {
0601 setLocationWithinModule(context + ".getNodeType().getInitialPredicateDefinition()");
0602 n.setNodeType(create((InitialPredicateDefinition) node.getNodeType()));
0603 } else if (node.getNodeType() instanceof PredicateDefinition) {
0604 setLocationWithinModule(context + ".getNodeType().getPredicateDefinition()");
0605 n.setNodeType(create((PredicateDefinition) node.getNodeType()));
0606 } else if (node.getNodeType() instanceof InitialFunctionDefinition) {
0607 setLocationWithinModule(context + ".getNodeType().getInitialFunctionDefinition()");
0608 n.setNodeType(create((InitialFunctionDefinition) node.getNodeType()));
0609 } else if (node.getNodeType() instanceof FunctionDefinition) {
0610 setLocationWithinModule(context + ".getNodeType().getFunctionDefinition()");
0611 n.setNodeType(create((FunctionDefinition) node.getNodeType()));
0612 } else if (node.getNodeType() instanceof Proposition) {
0613 setLocationWithinModule(context + ".getNodeType().getProposition()");
0614 n.setNodeType(create((Proposition) node.getNodeType()));
0615 } else if (node.getNodeType() instanceof Rule) {
0616 setLocationWithinModule(context + ".getNodeType().getRule()");
0617 n.setNodeType(create((Rule) node.getNodeType()));
0618 } else {
0619 throw new IllegalModuleDataException(ServiceErrors.RUNTIME_ERROR_CODE,
0620 ServiceErrors.RUNTIME_ERROR_TEXT + " "
0621 + "unexpected node type: " + node.getNodeType().getClass(),
0622 getCurrentContext());
0623 }
0624 }
0625 if (node.getSucceedingText() != null) {
0626 setLocationWithinModule(context + ".getSucceedingText()");
0627 n.setSucceedingText(create(node.getSucceedingText()));
0628 }
0629 setLocationWithinModule(context);
0630 return n;
0631 }
0632
0633 private final AxiomVo create(final Axiom axiom) {
0634 if (axiom == null) {
0635 return null;
0636 }
0637 final AxiomVo a = new AxiomVo();
0638 final String context = getCurrentContext().getLocationWithinModule();
0639 if (axiom.getDefinedOperator() != null) {
0640 setLocationWithinModule(context + ".getDefinedOperator()");
0641 a.setDefinedOperator(axiom.getDefinedOperator());
0642 }
0643 if (axiom.getFormula() != null) {
0644 setLocationWithinModule(context + ".getFormula()");
0645 a.setFormula(create(axiom.getFormula()));
0646 }
0647 if (axiom.getDescription() != null) {
0648 setLocationWithinModule(context + ".getDescription()");
0649 a.setDescription(create(axiom.getDescription()));
0650 }
0651 setLocationWithinModule(context);
0652 return a;
0653 }
0654
0655 private final InitialPredicateDefinitionVo create(final InitialPredicateDefinition definition) {
0656 if (definition == null) {
0657 return null;
0658 }
0659 final InitialPredicateDefinitionVo d = new InitialPredicateDefinitionVo();
0660 final String context = getCurrentContext().getLocationWithinModule();
0661 if (definition.getLatexPattern() != null) {
0662 setLocationWithinModule(context + ".getLatexPattern()");
0663 d.setLatexPattern(definition.getLatexPattern());
0664 }
0665 if (definition.getName() != null) {
0666 setLocationWithinModule(context + ".getName()");
0667 d.setName(definition.getName());
0668 }
0669 if (definition.getArgumentNumber() != null) {
0670 setLocationWithinModule(context + ".getArgumentNumber()");
0671 d.setArgumentNumber(definition.getArgumentNumber());
0672 }
0673 if (definition.getPredCon() != null) {
0674 setLocationWithinModule(context + ".getPredCon()");
0675 d.setPredCon(create(definition.getPredCon()));
0676 }
0677 if (definition.getDescription() != null) {
0678 setLocationWithinModule(context + ".getDescription()");
0679 d.setDescription(create(definition.getDescription()));
0680 }
0681 setLocationWithinModule(context);
0682 return d;
0683 }
0684
0685 private final PredicateDefinitionVo create(final PredicateDefinition definition) {
0686 if (definition == null) {
0687 return null;
0688 }
0689 final PredicateDefinitionVo d = new PredicateDefinitionVo();
0690 final String context = getCurrentContext().getLocationWithinModule();
0691 if (definition.getLatexPattern() != null) {
0692 setLocationWithinModule(context + ".getLatexPattern()");
0693 d.setLatexPattern(definition.getLatexPattern());
0694 }
0695 if (definition.getName() != null) {
0696 setLocationWithinModule(context + ".getName()");
0697 d.setName(definition.getName());
0698 }
0699 if (definition.getArgumentNumber() != null) {
0700 setLocationWithinModule(context + ".getArgumentNumber()");
0701 d.setArgumentNumber(definition.getArgumentNumber());
0702 }
0703 if (definition.getFormula() != null) {
0704 setLocationWithinModule(context + ".getFormula()");
0705 d.setFormula(create(definition.getFormula()));
0706 }
0707 if (definition.getDescription() != null) {
0708 setLocationWithinModule(context + ".getDescription()");
0709 d.setDescription(create(definition.getDescription()));
0710 }
0711 setLocationWithinModule(context);
0712 return d;
0713 }
0714
0715 private final InitialFunctionDefinitionVo create(final InitialFunctionDefinition definition) {
0716 if (definition == null) {
0717 return null;
0718 }
0719 final InitialFunctionDefinitionVo d = new InitialFunctionDefinitionVo();
0720 final String context = getCurrentContext().getLocationWithinModule();
0721 if (definition.getLatexPattern() != null) {
0722 setLocationWithinModule(context + ".getLatexPattern()");
0723 d.setLatexPattern(definition.getLatexPattern());
0724 }
0725 if (definition.getArgumentNumber() != null) {
0726 setLocationWithinModule(context + ".getArgumentNumber()");
0727 d.setArgumentNumber(definition.getArgumentNumber());
0728 }
0729 if (definition.getName() != null) {
0730 setLocationWithinModule(context + ".getName()");
0731 d.setName(definition.getName());
0732 }
0733 if (definition.getFunCon() != null) {
0734 setLocationWithinModule(context + ".getFunCon()");
0735 d.setFunCon(create(definition.getFunCon()));
0736 }
0737 if (definition.getDescription() != null) {
0738 setLocationWithinModule(context + ".getDescription()");
0739 d.setDescription(create(definition.getDescription()));
0740 }
0741 setLocationWithinModule(context);
0742 return d;
0743 }
0744
0745 private final FunctionDefinitionVo create(final FunctionDefinition definition) {
0746 if (definition == null) {
0747 return null;
0748 }
0749 final FunctionDefinitionVo d = new FunctionDefinitionVo();
0750 final String context = getCurrentContext().getLocationWithinModule();
0751 if (definition.getLatexPattern() != null) {
0752 setLocationWithinModule(context + ".getLatexPattern()");
0753 d.setLatexPattern(definition.getLatexPattern());
0754 }
0755 if (definition.getArgumentNumber() != null) {
0756 setLocationWithinModule(context + ".getArgumentNumber()");
0757 d.setArgumentNumber(definition.getArgumentNumber());
0758 }
0759 if (definition.getName() != null) {
0760 setLocationWithinModule(context + ".getName()");
0761 d.setName(definition.getName());
0762 }
0763 if (definition.getFormula() != null) {
0764 setLocationWithinModule(context + ".getFormula()");
0765 d.setFormula(create(definition.getFormula()));
0766 }
0767 if (definition.getDescription() != null) {
0768 setLocationWithinModule(context + ".getDescription()");
0769 d.setDescription(create(definition.getDescription()));
0770 }
0771 setLocationWithinModule(context);
0772 return d;
0773 }
0774
0775 private final PropositionVo create(final Proposition proposition) {
0776 if (proposition == null) {
0777 return null;
0778 }
0779 final PropositionVo p = new PropositionVo();
0780 final String context = getCurrentContext().getLocationWithinModule();
0781 if (proposition.getFormula() != null) {
0782 setLocationWithinModule(context + ".getFormula()");
0783 p.setFormula(create(proposition.getFormula()));
0784 }
0785 if (proposition.getDescription() != null) {
0786 setLocationWithinModule(context + ".getDescription()");
0787 p.setDescription(create(proposition.getDescription()));
0788 }
0789 if (proposition.getProofList() != null) {
0790 setLocationWithinModule(context + ".getProofList()");
0791 p.setProofList(create(proposition.getProofList()));
0792 }
0793 if (proposition.getFormalProofList() != null) {
0794 setLocationWithinModule(context + ".getFormalProofList()");
0795 p.setFormalProofList(create(proposition.getFormalProofList()));
0796 }
0797 setLocationWithinModule(context);
0798 return p;
0799 }
0800
0801 private final RuleVo create(final Rule rule) {
0802 if (rule == null) {
0803 return null;
0804 }
0805 final RuleVo r = new RuleVo();
0806 final String context = getCurrentContext().getLocationWithinModule();
0807 if (rule.getName() != null) {
0808 setLocationWithinModule(context + ".getName()");
0809 r.setName(rule.getName());
0810 }
0811 if (rule.getLinkList() != null) {
0812 setLocationWithinModule(context + ".getLinkList()");
0813 r.setLinkList(create(rule.getLinkList()));
0814 }
0815 if (rule.getDescription() != null) {
0816 setLocationWithinModule(context + ".getDescription()");
0817 r.setDescription(create(rule.getDescription()));
0818 }
0819 if (rule.getProofList() != null) {
0820 setLocationWithinModule(context + ".getProofList()");
0821 r.setProofList(create(rule.getProofList()));
0822 }
0823 setLocationWithinModule(context);
0824 return r;
0825 }
0826
0827 private final LinkListVo create(final LinkList linkList) {
0828 if (linkList == null) {
0829 return null;
0830 }
0831 final LinkListVo list = new LinkListVo();
0832 final String context = getCurrentContext().getLocationWithinModule();
0833 for (int i = 0; i < linkList.size(); i++) {
0834 setLocationWithinModule(context + ".get(" + i + ")");
0835 list.add(linkList.get(i));
0836 }
0837 setLocationWithinModule(context);
0838 return list;
0839 }
0840
0841 private final ProofListVo create(final ProofList proofList) {
0842 if (proofList == null) {
0843 return null;
0844 }
0845 final ProofListVo list = new ProofListVo();
0846 final String context = getCurrentContext().getLocationWithinModule();
0847 for (int i = 0; i < proofList.size(); i++) {
0848 setLocationWithinModule(context + ".get(" + i + ")");
0849 list.add(create(proofList.get(i)));
0850 }
0851 setLocationWithinModule(context);
0852 return list;
0853 }
0854
0855 private final ProofVo create(final Proof proof) {
0856 if (proof == null) {
0857 return null;
0858 }
0859 final ProofVo p = new ProofVo();
0860 final String context = getCurrentContext().getLocationWithinModule();
0861 setLocationWithinModule(context + ".getKind()");
0862 p.setKind(proof.getKind());
0863 setLocationWithinModule(context + ".getLevel()");
0864 p.setLevel(proof.getLevel());
0865 setLocationWithinModule(context);
0866 if (proof.getNonFormalProof() != null) {
0867 setLocationWithinModule(context + ".getNonFormalProof()");
0868 p.setNonFormalProof(create(proof.getNonFormalProof()));
0869 }
0870 setLocationWithinModule(context);
0871 return p;
0872 }
0873
0874 private final FormalProofListVo create(final FormalProofList proofList) {
0875 if (proofList == null) {
0876 return null;
0877 }
0878 final FormalProofListVo list = new FormalProofListVo();
0879 final String context = getCurrentContext().getLocationWithinModule();
0880 for (int i = 0; i < proofList.size(); i++) {
0881 setLocationWithinModule(context + ".get(" + i + ")");
0882 list.add(create(proofList.get(i)));
0883 }
0884 setLocationWithinModule(context);
0885 return list;
0886 }
0887
0888 private final FormalProofVo create(final FormalProof proof) {
0889 if (proof == null) {
0890 return null;
0891 }
0892 final FormalProofVo p = new FormalProofVo();
0893 final String context = getCurrentContext().getLocationWithinModule();
0894 setLocationWithinModule(context);
0895 if (proof.getPrecedingText() != null) {
0896 setLocationWithinModule(context + ".getPrecedingText()");
0897 p.setPrecedingText(create(proof.getPrecedingText()));
0898 }
0899 if (proof.getFormalProofLineList() != null) {
0900 setLocationWithinModule(context + ".getFormalProofLineList()");
0901 p.setFormalProofLineList(create(proof.getFormalProofLineList()));
0902 }
0903 if (proof.getSucceedingText() != null) {
0904 setLocationWithinModule(context + ".getSucceedingText()");
0905 p.setSucceedingText(create(proof.getSucceedingText()));
0906 }
0907 setLocationWithinModule(context);
0908 return p;
0909 }
0910
0911 private final FormalProofLineListVo create(final FormalProofLineList proofList) {
0912 if (proofList == null) {
0913 return null;
0914 }
0915 final FormalProofLineListVo list = new FormalProofLineListVo();
0916 final String context = getCurrentContext().getLocationWithinModule();
0917 for (int i = 0; i < proofList.size(); i++) {
0918 setLocationWithinModule(context + ".get(" + i + ")");
0919 list.add(create(proofList.get(i)));
0920 }
0921 setLocationWithinModule(context);
0922 return list;
0923 }
0924
0925 private final FormalProofLineVo create(final FormalProofLine proofLine) {
0926 if (proofLine == null) {
0927 return null;
0928 }
0929 final FormalProofLineVo line = new FormalProofLineVo();
0930 final String context = getCurrentContext().getLocationWithinModule();
0931 if (proofLine.getLabel() != null) {
0932 setLocationWithinModule(context + ".getLabel()");
0933 line.setLabel(proofLine.getLabel());
0934 }
0935 if (proofLine.getFormula() != null) {
0936 setLocationWithinModule(context + ".getFormula()");
0937 line.setFormula(create(proofLine.getFormula()));
0938 }
0939 if (proofLine.getReasonType() != null) {
0940 setLocationWithinModule(context + ".getReasonType()");
0941 line.setReasonType(create(proofLine.getReasonType()));
0942 }
0943 setLocationWithinModule(context);
0944 return line;
0945 }
0946
0947 private final ReasonTypeVo create(final ReasonType reasonType) {
0948 if (reasonType == null) {
0949 return null;
0950 }
0951 final String context = getCurrentContext().getLocationWithinModule();
0952 final ReasonTypeVo result = new ReasonTypeVo();
0953 if (reasonType.getReason() != null) {
0954 final Reason reason = reasonType.getReason();
0955 Reason res = null;
0956 if (reason instanceof ModusPonens) {
0957 setLocationWithinModule(context + ".getModusPonens()");
0958 final ModusPonens r = (ModusPonens) reason;
0959 res = new ModusPonensVo(r.getReference1(), r.getReference2());
0960 } else if (reason instanceof Add) {
0961 setLocationWithinModule(context + ".getAdd()");
0962 final Add r = (Add) reason;
0963 res = new AddVo(r.getReference());
0964 } else if (reason instanceof Rename) {
0965 setLocationWithinModule(context + ".getRename()");
0966 final Rename r = (Rename) reason;
0967 res = new RenameVo(r.getReference(), r.getOriginalSubjectVariable(),
0968 r.getReplacementSubjectVariable(), r.getOccurrence());
0969 } else if (reason instanceof SubstFree) {
0970 setLocationWithinModule(context + ".getSubstFree()");
0971 final SubstFree r = (SubstFree) reason;
0972 res = new SubstFreeVo(r.getReference(), r.getSubjectVariable(),
0973 r.getSubstituteTerm());
0974 } else if (reason instanceof SubstFunc) {
0975 setLocationWithinModule(context + ".getSubstFunc()");
0976 final SubstFunc r = (SubstFunc) reason;
0977 res = new SubstFuncVo(r.getReference(), r.getFunctionVariable(),
0978 r.getSubstituteTerm());
0979 } else if (reason instanceof SubstPred) {
0980 setLocationWithinModule(context + ".getSubstPred()");
0981 final SubstPred r = (SubstPred) reason;
0982 res = new SubstPredVo(r.getReference(), r.getPredicateVariable(),
0983 r.getSubstituteFormula());
0984 } else if (reason instanceof Existential) {
0985 setLocationWithinModule(context + ".getExistential()");
0986 final Existential r = (Existential) reason;
0987 res = new ExistentialVo(r.getReference(), r.getSubjectVariable());
0988 } else if (reason instanceof Universal) {
0989 setLocationWithinModule(context + ".getUniversal()");
0990 final Universal r = (Universal) reason;
0991 res = new UniversalVo(r.getReference(), r.getSubjectVariable());
0992 } else {
0993 throw new RuntimeException("unknown reason class: " + reason.getClass());
0994 }
0995 result.setReason(res);
0996 }
0997 setLocationWithinModule(context);
0998 return result;
0999 }
1000
1001 private final FormulaVo create(final Formula formula) {
1002 if (formula == null) {
1003 return null;
1004 }
1005 final FormulaVo f = new FormulaVo();
1006 final String context = getCurrentContext().getLocationWithinModule();
1007 if (formula.getElement() != null) {
1008 setLocationWithinModule(context + ".getElement()");
1009 f.setElement(create(formula.getElement()));
1010 }
1011 setLocationWithinModule(context);
1012 return f;
1013 }
1014
1015 private final Element create(final Element element) {
1016 if (element == null) {
1017 return null;
1018 }
1019 final Element e;
1020 final String context = getCurrentContext().getLocationWithinModule();
1021 if (element.isList()) {
1022 setLocationWithinModule(context + ".getList()");
1023 e = create(element.getList());
1024 } else if (element.isAtom()) {
1025 // setLocationWithinModule(context + ".getAtom()");
1026 return create(element.getAtom());
1027 } else {
1028 throw new RuntimeException("unknown element type: " + element);
1029 }
1030 setLocationWithinModule(context);
1031 return e;
1032 }
1033
1034
1035 private final DefaultElementList create(final ElementList list) {
1036 if (list == null) {
1037 return null;
1038 }
1039 final DefaultElementList n = new DefaultElementList(list.getOperator(), new Element[] {});
1040 final String context = getCurrentContext().getLocationWithinModule();
1041 for (int i = 0; i < list.size(); i++) {
1042 if (list.getElement(i).isList()) {
1043 setLocationWithinModule(context + ".getElement(" + i + ")");
1044 }
1045 n.add(create(list.getElement(i)));
1046 }
1047 setLocationWithinModule(context);
1048 return n;
1049 }
1050
1051 private final DefaultAtom create(final Atom atom) {
1052 if (atom == null) {
1053 return null;
1054 }
1055 return new DefaultAtom(atom.getString());
1056 }
1057
1058 private final LatexListVo create(final LatexList latexList) {
1059 if (latexList == null) {
1060 return null;
1061 }
1062 final LatexListVo list = new LatexListVo();
1063 final String context = getCurrentContext().getLocationWithinModule();
1064 for (int i = 0; i < latexList.size(); i++) {
1065 setLocationWithinModule(context + ".get(" + i + ")");
1066 list.add(create(latexList.get(i)));
1067 }
1068 setLocationWithinModule(context);
1069 return list;
1070 }
1071
1072 /**
1073 * Creates LaTeX business object.
1074 *
1075 * @param latex LaTeX object.
1076 * @return LaTeX business object.
1077 */
1078 private final LatexVo create(final Latex latex) {
1079 if (latex == null) {
1080 return null;
1081 }
1082 final LatexVo lat = new LatexVo();
1083 lat.setLanguage(latex.getLanguage());
1084 lat.setLatex(latex.getLatex());
1085 return lat;
1086 }
1087
1088 /**
1089 * Set location information where are we within the original module.
1090 *
1091 * @param locationWithinModule Location within module.
1092 */
1093 protected void setLocationWithinModule(final String locationWithinModule) {
1094 getCurrentContext().setLocationWithinModule(locationWithinModule);
1095 }
1096
1097 /**
1098 * Get current context within original.
1099 *
1100 * @return Current context.
1101 */
1102 protected final ModuleContext getCurrentContext() {
1103 return currentContext;
1104 }
1105
1106 /**
1107 * Get original QEDEQ module.
1108 *
1109 * @return Original QEDEQ module.
1110 */
1111 protected final Qedeq getQedeqOriginal() {
1112 return original;
1113 }
1114
1115 }
|