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