001 /* This file is part of the project "Hilbert II" - http://www.qedeq.org
002 *
003 * Copyright 2000-2011, Michael Meyling <mime@qedeq.org>.
004 *
005 * "Hilbert II" is free software; you can redistribute
006 * it and/or modify it under the terms of the GNU General Public
007 * License as published by the Free Software Foundation; either
008 * version 2 of the License, or (at your option) any later version.
009 *
010 * This program is distributed in the hope that it will be useful,
011 * but WITHOUT ANY WARRANTY; without even the implied warranty of
012 * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
013 * GNU General Public License for more details.
014 */
015
016 package org.qedeq.kernel.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.se.dto.module.ReasonTypeVo;
022 import org.qedeq.kernel.xml.common.XmlSyntaxException;
023 import org.qedeq.kernel.xml.handler.common.AbstractSimpleHandler;
024 import org.qedeq.kernel.xml.handler.common.SimpleAttributes;
025
026
027 /**
028 * Parse author list.
029 *
030 * @author Michael Meyling
031 */
032 public class FormalProofLineListHandler extends AbstractSimpleHandler {
033
034 /** Value object with list of all module imports. */
035 private FormalProofLineListVo list;
036
037 /** Handler for proposition formula. */
038 private final FormulaHandler formulaHandler;
039
040 /** Handler for Modus Ponens usage. */
041 private final ModusPonensHandler modusPonensHandler;
042
043 /** Handler for Addition usage. */
044 private final AddHandler addHandler;
045
046 /** Handler for Rename Subject Variable usage. */
047 private final RenameHandler renameHandler;
048
049 /** Handler for Substitution Predicate Variable usage. */
050 private final SubstPredvarHandler substPredvarHandler;
051
052 /** Handler for Substitution Free Variable usage. */
053 private final SubstFreevarHandler substFreevarHandler;
054
055 /** Handler for Substitution Function Variable usage. */
056 private final SubstFuncvarHandler substFuncvarHandler;
057
058 /** Handler for Existential Generalization usage. */
059 private final ExistentialHandler existentialHandler;
060
061 /** Handler for Universal Generalization usage. */
062 private final UniversalHandler universalHandler;
063
064 /** Label for a single module. */
065 private String label;
066
067 /** Reason for proof line. */
068 private Reason reason;
069
070
071 /**
072 * Handles list of imports.
073 *
074 * @param handler Parent handler.
075 */
076 public FormalProofLineListHandler(final AbstractSimpleHandler handler) {
077 super(handler, "LINES");
078 formulaHandler = new FormulaHandler(this);
079 modusPonensHandler = new ModusPonensHandler(this);
080 addHandler = new AddHandler(this);
081 substPredvarHandler = new SubstPredvarHandler(this);
082 renameHandler = new RenameHandler(this);
083 substFreevarHandler = new SubstFreevarHandler(this);
084 substFuncvarHandler = new SubstFuncvarHandler(this);
085 existentialHandler = new ExistentialHandler(this);
086 universalHandler = new UniversalHandler(this);
087 }
088
089 public final void init() {
090 list = null;
091 reason = null;
092 label = null;
093 }
094
095 /**
096 * Get parsed result.
097 *
098 * @return Location list.
099 */
100 public final FormalProofLineListVo getFormalProofLineList() {
101 return list;
102 }
103
104 public final void startElement(final String name, final SimpleAttributes attributes)
105 throws XmlSyntaxException {
106 if (getStartTag().equals(name)) {
107 list = new FormalProofLineListVo();
108 } else if ("L".equals(name)) {
109 label = attributes.getString("label");
110 reason = null;
111 } else if (formulaHandler.getStartTag().equals(name)) {
112 changeHandler(formulaHandler, name, attributes);
113 } else if (modusPonensHandler.getStartTag().equals(name)) {
114 changeHandler(modusPonensHandler, name, attributes);
115 } else if (addHandler.getStartTag().equals(name)) {
116 changeHandler(addHandler, name, attributes);
117 } else if (substPredvarHandler.getStartTag().equals(name)) {
118 changeHandler(substPredvarHandler, name, attributes);
119 } else if (renameHandler.getStartTag().equals(name)) {
120 changeHandler(renameHandler, name, attributes);
121 } else if (substFreevarHandler.getStartTag().equals(name)) {
122 changeHandler(substFreevarHandler, name, attributes);
123 } else if (substFuncvarHandler.getStartTag().equals(name)) {
124 changeHandler(substFuncvarHandler, name, attributes);
125 } else if (existentialHandler.getStartTag().equals(name)) {
126 changeHandler(existentialHandler, name, attributes);
127 } else if (universalHandler.getStartTag().equals(name)) {
128 changeHandler(universalHandler, name, attributes);
129 } else {
130 throw XmlSyntaxException.createUnexpectedTagException(name);
131 }
132 }
133
134 public final void endElement(final String name) throws XmlSyntaxException {
135 if (getStartTag().equals(name)) {
136 // nothing to do
137 } else if (formulaHandler.getStartTag().equals(name)) {
138 // nothing to do
139 } else if ("L".equals(name)) {
140 list.add(new FormalProofLineVo(label, formulaHandler.getFormula(), new ReasonTypeVo(reason)));
141 } else if (modusPonensHandler.getStartTag().equals(name)) {
142 reason = modusPonensHandler.getModusPonensVo();
143 } else if (addHandler.getStartTag().equals(name)) {
144 reason = addHandler.getAddVo();
145 } else if (substPredvarHandler.getStartTag().equals(name)) {
146 reason = substPredvarHandler.getSubstPredVo();
147 } else if (renameHandler.getStartTag().equals(name)) {
148 reason = renameHandler.getRenameVo();
149 } else if (substFreevarHandler.getStartTag().equals(name)) {
150 reason = substFreevarHandler.getSubstFreeVo();
151 } else if (substFuncvarHandler.getStartTag().equals(name)) {
152 reason = substFuncvarHandler.getSubstFuncVo();
153 } else if (existentialHandler.getStartTag().equals(name)) {
154 reason = existentialHandler.getExistentialVo();
155 } else if (universalHandler.getStartTag().equals(name)) {
156 reason = universalHandler.getUniversalVo();
157 } else {
158 throw XmlSyntaxException.createUnexpectedTagException(name);
159 }
160 }
161 }
|