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.qedeq.base.utility.EqualsUtility;
019 import org.qedeq.kernel.se.base.list.Element;
020 import org.qedeq.kernel.se.base.module.Axiom;
021 import org.qedeq.kernel.se.base.module.FunctionDefinition;
022 import org.qedeq.kernel.se.base.module.InitialFunctionDefinition;
023 import org.qedeq.kernel.se.base.module.InitialPredicateDefinition;
024 import org.qedeq.kernel.se.base.module.LatexList;
025 import org.qedeq.kernel.se.base.module.PredicateDefinition;
026 import org.qedeq.kernel.se.base.module.Proposition;
027 import org.qedeq.kernel.se.base.module.Rule;
028
029
030 /**
031 * Definition of function operator. This is a function constant. For example the function
032 * "x union y" or constants like the empty set.
033 *
034 * @author Michael Meyling
035 */
036 public class InitialFunctionDefinitionVo implements InitialFunctionDefinition {
037
038 /** Carries information about the argument number the defined object needs. */
039 private String argumentNumber;
040
041 /** This name together with argumentNumber identifies a function. */
042 private String name;
043
044 /** LaTeX pattern for definition visualisation. The replaceable arguments must are
045 * marked as <code>#1</code>, <code>#2</code> and so on. For example
046 * <code>\mathfrak{M}(#1)</code> */
047 private String latexPattern;
048
049 /** Defined function constant with free subject variables as arguments. */
050 private Element funCon;
051
052 /** Further proposition description. Normally <code>null</code>. */
053 private LatexList description;
054
055 /**
056 * Constructs a new definition.
057 */
058 public InitialFunctionDefinitionVo() {
059 // nothing to do
060 }
061
062 public Axiom getAxiom() {
063 return null;
064 }
065
066 public InitialPredicateDefinition getInitialPredicateDefinition() {
067 return null;
068 }
069
070 public PredicateDefinition getPredicateDefinition() {
071 return null;
072 }
073
074 public InitialFunctionDefinition getInitialFunctionDefinition() {
075 return this;
076 }
077
078 public FunctionDefinition getFunctionDefinition() {
079 return null;
080 }
081
082 public Proposition getProposition() {
083 return null;
084 }
085
086 public Rule getRule() {
087 return null;
088 }
089
090 /**
091 * Set information about the argument number the defined object needs.
092 *
093 * @param argumentNumber Argument number information.
094 */
095 public final void setArgumentNumber(final String argumentNumber) {
096 this.argumentNumber = argumentNumber;
097 }
098
099 public final String getArgumentNumber() {
100 return argumentNumber;
101 }
102
103 /**
104 * Set function name. Together with {@link #getArgumentNumber()} this
105 * identifies a function.
106 *
107 * @param name Function name.
108 */
109 public void setName(final String name) {
110 this.name = name;
111 }
112
113 public String getName() {
114 return name;
115 }
116
117 /**
118 * Set LaTeX pattern for definition visualisation. The replaceable arguments are
119 * marked as <code>#1</code>, <code>#2</code> and so on. For example
120 * <code>\mathfrak{M}(#1)</code>.
121 *
122 * @param latexPattern LaTeX pattern for definition visualisation.
123 */
124 public final void setLatexPattern(final String latexPattern) {
125 this.latexPattern = latexPattern;
126 }
127
128 public final String getLatexPattern() {
129 return latexPattern;
130 }
131
132 public Element getFunCon() {
133 return funCon;
134 }
135
136 /**
137 * Set function constant that we define. The function constant must
138 * match {@link #getName()} and {@link #getArgumentNumber()}.
139 *
140 * @param funCon Function constant with free subject variables as arguments.
141 */
142 public void setFunCon(final Element funCon) {
143 this.funCon = funCon;
144 }
145
146 /**
147 * Set description. Only necessary if formula is not self-explanatory.
148 *
149 * @param description Description.
150 */
151 public final void setDescription(final LatexListVo description) {
152 this.description = description;
153 }
154
155 public LatexList getDescription() {
156 return description;
157 }
158
159 public boolean equals(final Object obj) {
160 if (!(obj instanceof InitialFunctionDefinition)) {
161 return false;
162 }
163 final InitialFunctionDefinition other = (InitialFunctionDefinition) obj;
164 return EqualsUtility.equals(getArgumentNumber(), other.getArgumentNumber())
165 && EqualsUtility.equals(getName(), other.getName())
166 && EqualsUtility.equals(getLatexPattern(), other.getLatexPattern())
167 && EqualsUtility.equals(getFunCon(), other.getFunCon())
168 && EqualsUtility.equals(getDescription(), other.getDescription());
169 }
170
171 public int hashCode() {
172 return (getArgumentNumber() != null ? getArgumentNumber().hashCode() : 0)
173 ^ (getName() != null ? 1 ^ getName().hashCode() : 0)
174 ^ (getLatexPattern() != null ? 2 ^ getLatexPattern().hashCode() : 0)
175 ^ (getFunCon() != null ? 3 ^ getFunCon().hashCode() : 0)
176 ^ (getDescription() != null ? 5 ^ getDescription().hashCode() : 0);
177 }
178
179 public String toString() {
180 final StringBuffer buffer = new StringBuffer();
181 buffer.append("Initial Function Definition arguments=" + getArgumentNumber() + "\n");
182 buffer.append("\tname=" + getName() + "\n");
183 buffer.append("\tpattern=" + getLatexPattern() + "\n");
184 buffer.append("\tfuncon=" + getFunCon() + "\n");
185 buffer.append("\tdescription:\n" + getDescription() + "\n");
186 return buffer.toString();
187 }
188
189 }
|