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.xml.handler.module;
017
018 import org.qedeq.kernel.se.base.module.Reason;
019 import org.qedeq.kernel.se.dto.module.FormalProofLineListVo;
020 import org.qedeq.kernel.se.dto.module.FormalProofLineVo;
021 import org.qedeq.kernel.xml.common.XmlSyntaxException;
022 import org.qedeq.kernel.xml.handler.common.AbstractSimpleHandler;
023 import org.qedeq.kernel.xml.handler.common.SimpleAttributes;
024
025
026 /**
027 * Parse formal proof lines.
028 *
029 * @author Michael Meyling
030 */
031 public class FormalProofLineListHandler extends AbstractSimpleHandler {
032
033 /** Value object with list of all module imports. */
034 private FormalProofLineListVo list;
035
036 /** Handler for proposition formula. */
037 private final FormulaHandler formulaHandler;
038
039 /** Handler for Modus Ponens usage. */
040 private final ModusPonensHandler modusPonensHandler;
041
042 /** Handler for Addition usage. */
043 private final AddHandler addHandler;
044
045 /** Handler for Rename Subject Variable usage. */
046 private final RenameHandler renameHandler;
047
048 /** Handler for Substitution Predicate Variable usage. */
049 private final SubstPredvarHandler substPredvarHandler;
050
051 /** Handler for Substitution Free Variable usage. */
052 private final SubstFreevarHandler substFreevarHandler;
053
054 /** Handler for Substitution Function Variable usage. */
055 private final SubstFuncvarHandler substFuncvarHandler;
056
057 /** Handler for Existential Generalization usage. */
058 private final ExistentialHandler existentialHandler;
059
060 /** Handler for Universal Generalization usage. */
061 private final UniversalHandler universalHandler;
062
063 /** Handler for Universal Generalization usage. */
064 private final ConditionalProofHandler conditionalProofHandler;
065
066 /** Label for a single module. */
067 private String label;
068
069 /** Reason for proof line. */
070 private Reason reason;
071
072
073 /**
074 * Handles list of imports.
075 *
076 * @param handler Parent handler.
077 */
078 public FormalProofLineListHandler(final AbstractSimpleHandler handler) {
079 super(handler, "LINES");
080 formulaHandler = new FormulaHandler(this);
081 modusPonensHandler = new ModusPonensHandler(this);
082 addHandler = new AddHandler(this);
083 substPredvarHandler = new SubstPredvarHandler(this);
084 renameHandler = new RenameHandler(this);
085 substFreevarHandler = new SubstFreevarHandler(this);
086 substFuncvarHandler = new SubstFuncvarHandler(this);
087 existentialHandler = new ExistentialHandler(this);
088 universalHandler = new UniversalHandler(this);
089 conditionalProofHandler = new ConditionalProofHandler(this);
090 }
091
092 public final void init() {
093 list = null;
094 reason = null;
095 label = null;
096 }
097
098 /**
099 * Get parsed result.
100 *
101 * @return Location list.
102 */
103 public final FormalProofLineListVo getFormalProofLineList() {
104 return list;
105 }
106
107 public final void startElement(final String name, final SimpleAttributes attributes)
108 throws XmlSyntaxException {
109 if (getStartTag().equals(name)) {
110 list = new FormalProofLineListVo();
111 } else if ("L".equals(name)) {
112 label = attributes.getString("label");
113 reason = null;
114 } else if (formulaHandler.getStartTag().equals(name)) {
115 changeHandler(formulaHandler, name, attributes);
116 } else if (modusPonensHandler.getStartTag().equals(name)) {
117 changeHandler(modusPonensHandler, name, attributes);
118 } else if (addHandler.getStartTag().equals(name)) {
119 changeHandler(addHandler, name, attributes);
120 } else if (substPredvarHandler.getStartTag().equals(name)) {
121 changeHandler(substPredvarHandler, name, attributes);
122 } else if (renameHandler.getStartTag().equals(name)) {
123 changeHandler(renameHandler, name, attributes);
124 } else if (substFreevarHandler.getStartTag().equals(name)) {
125 changeHandler(substFreevarHandler, name, attributes);
126 } else if (substFuncvarHandler.getStartTag().equals(name)) {
127 changeHandler(substFuncvarHandler, name, attributes);
128 } else if (existentialHandler.getStartTag().equals(name)) {
129 changeHandler(existentialHandler, name, attributes);
130 } else if (universalHandler.getStartTag().equals(name)) {
131 changeHandler(universalHandler, name, attributes);
132 } else if (conditionalProofHandler.getStartTag().equals(name)) {
133 changeHandler(conditionalProofHandler, name, attributes);
134 } else {
135 throw XmlSyntaxException.createUnexpectedTagException(name);
136 }
137 }
138
139 public final void endElement(final String name) throws XmlSyntaxException {
140 if (getStartTag().equals(name)) {
141 // nothing to do
142 } else if (formulaHandler.getStartTag().equals(name)) {
143 // nothing to do
144 } else if ("L".equals(name)) {
145 list.add(new FormalProofLineVo(label, formulaHandler.getFormula(), reason));
146 } else if (modusPonensHandler.getStartTag().equals(name)) {
147 reason = modusPonensHandler.getModusPonensVo();
148 } else if (addHandler.getStartTag().equals(name)) {
149 reason = addHandler.getAddVo();
150 } else if (substPredvarHandler.getStartTag().equals(name)) {
151 reason = substPredvarHandler.getSubstPredVo();
152 } else if (renameHandler.getStartTag().equals(name)) {
153 reason = renameHandler.getRenameVo();
154 } else if (substFreevarHandler.getStartTag().equals(name)) {
155 reason = substFreevarHandler.getSubstFreeVo();
156 } else if (substFuncvarHandler.getStartTag().equals(name)) {
157 reason = substFuncvarHandler.getSubstFuncVo();
158 } else if (existentialHandler.getStartTag().equals(name)) {
159 reason = existentialHandler.getExistentialVo();
160 } else if (universalHandler.getStartTag().equals(name)) {
161 reason = universalHandler.getUniversalVo();
162 } else if (conditionalProofHandler.getStartTag().equals(name)) {
163 list.add(conditionalProofHandler.getConditionalProofVo());
164 } else {
165 throw XmlSyntaxException.createUnexpectedTagException(name);
166 }
167 }
168 }
|