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.module.Axiom;
020 import org.qedeq.kernel.se.base.module.Formula;
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 operator. This is a predicate constant. For example the
032 * predicate "x is a set" could be defined in MK with the formula "\exists y: x \in y".
033 *
034 * @author Michael Meyling
035 */
036 public class PredicateDefinitionVo implements PredicateDefinition {
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 /** Formula that defines the object.*/
050 private Formula formula;
051
052 /** Further proposition description. Normally <code>null</code>. */
053 private LatexList description;
054
055 /**
056 * Constructs a new definition.
057 */
058 public PredicateDefinitionVo() {
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 this;
072 }
073
074 public InitialFunctionDefinition getInitialFunctionDefinition() {
075 return null;
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 predicate name. Together with {@link #getArgumentNumber()} this
105 * identifies a predicate.
106 *
107 * @param name Predicate 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 /**
133 * Set defining formula or term that defines the object. Could be <code>null</code>.
134 *
135 * @param formulaOrTerm Formula or term that defines the new operator.
136 */
137 public final void setFormula(final FormulaVo formulaOrTerm) {
138 this.formula = formulaOrTerm;
139 }
140
141 public final Formula getFormula() {
142 return formula;
143 }
144
145 /**
146 * Set description. Only necessary if formula is not self-explanatory.
147 *
148 * @param description Description.
149 */
150 public final void setDescription(final LatexListVo description) {
151 this.description = description;
152 }
153
154 public LatexList getDescription() {
155 return description;
156 }
157
158 public boolean equals(final Object obj) {
159 if (!(obj instanceof PredicateDefinition)) {
160 return false;
161 }
162 final PredicateDefinition other = (PredicateDefinition) obj;
163 return EqualsUtility.equals(getArgumentNumber(), other.getArgumentNumber())
164 && EqualsUtility.equals(getName(), other.getName())
165 && EqualsUtility.equals(getLatexPattern(), other.getLatexPattern())
166 && EqualsUtility.equals(getFormula(), other.getFormula())
167 && EqualsUtility.equals(getDescription(), other.getDescription());
168 }
169
170 public int hashCode() {
171 return (getArgumentNumber() != null ? getArgumentNumber().hashCode() : 0)
172 ^ (getName() != null ? 1 ^ getName().hashCode() : 0)
173 ^ (getLatexPattern() != null ? 2 ^ getLatexPattern().hashCode() : 0)
174 ^ (getFormula() != null ? 4 ^ getFormula().hashCode() : 0)
175 ^ (getDescription() != null ? 5 ^ getDescription().hashCode() : 0);
176 }
177
178 public String toString() {
179 final StringBuffer buffer = new StringBuffer();
180 buffer.append("Predicate Definition arguments=" + getArgumentNumber() + "\n");
181 buffer.append("\tname=" + getName() + "\n");
182 buffer.append("\tpattern=" + getLatexPattern() + "\n");
183 buffer.append("\tformula:\n" + getFormula() + "\n");
184 buffer.append("\tdescription:\n" + getDescription() + "\n");
185 return buffer.toString();
186 }
187
188
189 }
|