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.list.Element;
019 import org.qedeq.kernel.se.base.module.Formula;
020 import org.qedeq.kernel.se.dto.module.SubstPredVo;
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 import org.qedeq.kernel.xml.handler.list.ElementHandler;
025
026
027 /**
028 * Parse a Substitute Predicate Variable Rule usage.
029 *
030 * @author Michael Meyling
031 */
032 public class SubstPredvarHandler extends AbstractSimpleHandler {
033
034 /** Rule value object. */
035 private SubstPredVo substPredvar;
036
037 /** Reference to previously proved formula. */
038 private String ref;
039
040 /** Predicate variable that will be substituted. */
041 private Element predicateVariable;
042
043 /** Replacement formula. */
044 private Formula substituteFormula;
045
046 /** Handle formal proofs. */
047 private final FormulaHandler formulaHandler;
048
049 /** Handle elements. */
050 private final ElementHandler elementHandler;
051
052 /**
053 * Deals with definitions.
054 *
055 * @param handler Parent handler.
056 */
057 public SubstPredvarHandler(final AbstractSimpleHandler handler) {
058 super(handler, "SUBST_PREDVAR");
059 formulaHandler = new FormulaHandler(this);
060 elementHandler = new ElementHandler(this);
061 }
062
063 public final void init() {
064 substPredvar = null;
065 predicateVariable = null;
066 substituteFormula = null;
067 ref = null;
068 }
069
070 /**
071 * Get Substitute Predicate Variable Rule usage.
072 *
073 * @return Substitute Predicate Variable usage.
074 */
075 public final SubstPredVo getSubstPredVo() {
076 return substPredvar;
077 }
078
079 public final void startElement(final String name, final SimpleAttributes attributes)
080 throws XmlSyntaxException {
081 if (getStartTag().equals(name)) {
082 ref = attributes.getString("ref");
083 } else if ("PREDVAR".equals(name)) {
084 changeHandler(elementHandler, name, attributes);
085 } else if (formulaHandler.getStartTag().equals(name)) {
086 changeHandler(formulaHandler, name, attributes);
087 } else {
088 throw XmlSyntaxException.createUnexpectedTagException(name);
089 }
090 }
091
092 public final void endElement(final String name) throws XmlSyntaxException {
093 if (getStartTag().equals(name)) {
094 substPredvar = new SubstPredVo(ref, predicateVariable,
095 (substituteFormula != null ? substituteFormula.getElement() : null));
096 } else if ("PREDVAR".equals(name)) {
097 predicateVariable = elementHandler.getElement();
098 } else if (formulaHandler.getStartTag().equals(name)) {
099 substituteFormula = formulaHandler.getFormula();
100 } else {
101 throw XmlSyntaxException.createUnexpectedTagException(name);
102 }
103 }
104
105 }
|