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.module.Axiom;
020 import org.qedeq.kernel.se.base.module.FunctionDefinition;
021 import org.qedeq.kernel.se.base.module.InitialFunctionDefinition;
022 import org.qedeq.kernel.se.base.module.InitialPredicateDefinition;
023 import org.qedeq.kernel.se.base.module.LatexList;
024 import org.qedeq.kernel.se.base.module.LinkList;
025 import org.qedeq.kernel.se.base.module.PredicateDefinition;
026 import org.qedeq.kernel.se.base.module.ProofList;
027 import org.qedeq.kernel.se.base.module.Proposition;
028 import org.qedeq.kernel.se.base.module.Rule;
029
030
031 /**
032 * Rule declaration.
033 *
034 * @author Michael Meyling
035 */
036 public class RuleVo implements Rule {
037
038 /** List of necessary ids. */
039 private LinkListVo linkList;
040
041 /** Further proposition description. Normally <code>null</code>. */
042 private LatexList description;
043
044 /** Rule name. */
045 private String name;
046
047 /** Proofs for this rule. */
048 private ProofListVo proofList;
049
050 /**
051 * Constructs a new rule declaration.
052 */
053 public RuleVo() {
054 // nothing to do
055 }
056
057 public Axiom getAxiom() {
058 return null;
059 }
060
061 public InitialPredicateDefinition getInitialPredicateDefinition() {
062 return null;
063 }
064
065 public PredicateDefinition getPredicateDefinition() {
066 return null;
067 }
068
069 public InitialFunctionDefinition getInitialFunctionDefinition() {
070 return null;
071 }
072
073 public FunctionDefinition getFunctionDefinition() {
074 return null;
075 }
076
077 public Proposition getProposition() {
078 return null;
079 }
080
081 public Rule getRule() {
082 return this;
083 }
084
085 /**
086 * Set rule name.
087 *
088 * @param name Rule name.
089 */
090 public final void setName(final String name) {
091 this.name = name;
092 }
093
094 public final String getName() {
095 return name;
096 }
097
098 /**
099 * Set list of necessary ids.
100 *
101 * @param linkList List.
102 */
103 public final void setLinkList(final LinkListVo linkList) {
104 this.linkList = linkList;
105 }
106
107 public final LinkList getLinkList() {
108 return linkList;
109 }
110
111 /**
112 * Add link for this rule.
113 *
114 * @param id Id to add.
115 */
116 public final void addLink(final String id) {
117 if (linkList == null) {
118 linkList = new LinkListVo();
119 }
120 linkList.add(id);
121 }
122
123 /**
124 * Set description. Only necessary if formula is not self-explanatory.
125 *
126 * @param description Description.
127 */
128 public final void setDescription(final LatexListVo description) {
129 this.description = description;
130 }
131
132 public LatexList getDescription() {
133 return description;
134 }
135
136 /**
137 * Set rule proof list.
138 *
139 * @param proofList Proof list.
140 */
141 public final void setProofList(final ProofListVo proofList) {
142 this.proofList = proofList;
143 }
144
145 public final ProofList getProofList() {
146 return proofList;
147 }
148
149 /**
150 * Add proof to this list.
151 *
152 * @param proof Proof to add.
153 */
154 public final void addProof(final ProofVo proof) {
155 if (proofList == null) {
156 proofList = new ProofListVo();
157 }
158 proofList.add(proof);
159 }
160
161 public boolean equals(final Object obj) {
162 if (!(obj instanceof RuleVo)) {
163 return false;
164 }
165 final RuleVo other = (RuleVo) obj;
166 return EqualsUtility.equals(getName(), other.getName())
167 && EqualsUtility.equals(getLinkList(), other.getLinkList())
168 && EqualsUtility.equals(getDescription(), other.getDescription())
169 && EqualsUtility.equals(getProofList(), other.getProofList());
170 }
171
172 public int hashCode() {
173 return (getName() != null ? 1 ^ getName().hashCode() : 0)
174 ^ (getLinkList() != null ? 1 ^ getLinkList().hashCode() : 0)
175 ^ (getDescription() != null ? 2 ^ getDescription().hashCode() : 0)
176 ^ (getProofList() != null ? 2 ^ getProofList().hashCode() : 0);
177 }
178
179 public String toString() {
180 final StringBuffer buffer = new StringBuffer();
181 buffer.append("Rule: " + getName() + "\n");
182 buffer.append(getLinkList());
183 buffer.append("\nDescription:\n");
184 buffer.append(getDescription());
185 buffer.append("\nProof:\n");
186 buffer.append(getProofList());
187 return buffer.toString();
188 }
189 }
|