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.se.dto.module;
017
018 import org.apache.commons.lang.ArrayUtils;
019 import org.qedeq.base.utility.EqualsUtility;
020 import org.qedeq.kernel.se.base.list.Element;
021 import org.qedeq.kernel.se.base.module.Rename;
022
023
024 /**
025 * Usage of rule for rename bound subject variable.
026 *
027 * @author Michael Meyling
028 */
029 public class RenameVo implements Rename {
030
031 /** Reference to previously proven formula. */
032 private String reference;
033
034 /** Bound subject variable that will be replaced. */
035 private Element originalSubjectVariable;
036
037 /** Replacement subject variable. */
038 private Element replacementSubjectVariable;
039
040 /** This bound occurrence should be replaced. If this value is 0, the replacement position
041 * is not specified. */
042 private int occurrence;
043
044 /**
045 * Constructs an addition argument.
046 *
047 * @param reference Reference to a valid formula.
048 * @param originalSubjectVariable Bound subject variable that will be replaced.
049 * @param replacementSubjectVariable Replacement subject variable.
050 * @param occurrence This bound occurrence should be replaced. If this
051 * value is 0, the replacement position
052 * is not specified. */
053
054 public RenameVo(final String reference, final Element originalSubjectVariable,
055 final Element replacementSubjectVariable, final int occurrence) {
056 this.reference = reference;
057 this.originalSubjectVariable = originalSubjectVariable;
058 this.replacementSubjectVariable = replacementSubjectVariable;
059 this.occurrence = occurrence;
060 }
061
062 /**
063 * Default constructor.
064 */
065 public RenameVo() {
066 // nothing to do
067 }
068
069 public Rename getRename() {
070 return this;
071 }
072
073 public String getReference() {
074 return reference;
075 }
076
077 /**
078 * Set formula reference.
079 *
080 * @param reference Reference to formula.
081 */
082 public void setReference(final String reference) {
083 this.reference = reference;
084 }
085
086 public String[] getReferences() {
087 if (reference == null) {
088 return ArrayUtils.EMPTY_STRING_ARRAY;
089 } else {
090 return new String[] {reference };
091 }
092 }
093
094 public int getOccurrence() {
095 return occurrence;
096 }
097
098 /**
099 * Set occurrence of bound subject variable that should be renamed.
100 *
101 * @param occurrence This occurrence should be renamed.
102 */
103 public void setOccurrence(final int occurrence) {
104 this.occurrence = occurrence;
105 }
106
107 public Element getOriginalSubjectVariable() {
108 return originalSubjectVariable;
109 }
110
111 /**
112 * Set original subject variable, which will be replaced.
113 *
114 * @param originalSubjectVariable Subject variable.
115 */
116 public void setOriginalSubjectVariable(final Element originalSubjectVariable) {
117 this.originalSubjectVariable = originalSubjectVariable;
118 }
119
120 public Element getReplacementSubjectVariable() {
121 return replacementSubjectVariable;
122 }
123
124 /**
125 * Set new subject variable subject variable.
126 *
127 * @param replacementSubjectVariable New subject variable.
128 */
129 public void setReplacementSubjectVariable(final Element replacementSubjectVariable) {
130 this.replacementSubjectVariable = replacementSubjectVariable;
131 }
132
133 public String getName() {
134 return "Rename";
135 }
136
137 public boolean equals(final Object obj) {
138 if (!(obj instanceof RenameVo)) {
139 return false;
140 }
141 final RenameVo other = (RenameVo) obj;
142 return EqualsUtility.equals(reference, other.reference)
143 && EqualsUtility.equals(originalSubjectVariable, other.originalSubjectVariable)
144 && EqualsUtility.equals(replacementSubjectVariable, other.replacementSubjectVariable)
145 && (occurrence == other.occurrence);
146 }
147
148 public int hashCode() {
149 return (reference != null ? reference.hashCode() : 0)
150 ^ (originalSubjectVariable != null ? 2 ^ originalSubjectVariable.hashCode() : 0)
151 ^ (replacementSubjectVariable != null ? 3 ^ replacementSubjectVariable.hashCode() : 0)
152 ^ (4 ^ occurrence);
153 }
154
155 public String toString() {
156 StringBuffer result = new StringBuffer();
157 result.append(getName());
158 if (reference != null || originalSubjectVariable != null
159 || replacementSubjectVariable != null
160 || occurrence != 0) {
161 result.append(" (");
162 boolean w = false;
163 if (reference != null) {
164 result.append(reference);
165 w = true;
166 }
167 if (originalSubjectVariable != null) {
168 if (w) {
169 result.append(", ");
170 }
171 result.append(originalSubjectVariable);
172 w = true;
173 }
174 if (replacementSubjectVariable != null) {
175 if (w) {
176 result.append(", ");
177 }
178 result.append("by ");
179 result.append(replacementSubjectVariable);
180 w = true;
181 }
182 if (occurrence != 0) {
183 if (w) {
184 result.append(", ");
185 }
186 result.append("occurrence: ");
187 result.append(occurrence);
188 w = true;
189 }
190 result.append(")");
191 }
192 return result.toString();
193 }
194
195 }
|