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