1 | /* This file is part of the project "Hilbert II" - http://www.qedeq.org |
2 | * |
3 | * Copyright 2000-2014, Michael Meyling <mime@qedeq.org>. |
4 | * |
5 | * "Hilbert II" is free software; you can redistribute |
6 | * it and/or modify it under the terms of the GNU General Public |
7 | * License as published by the Free Software Foundation; either |
8 | * version 2 of the License, or (at your option) any later version. |
9 | * |
10 | * This program is distributed in the hope that it will be useful, |
11 | * but WITHOUT ANY WARRANTY; without even the implied warranty of |
12 | * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the |
13 | * GNU General Public License for more details. |
14 | */ |
15 | |
16 | package org.qedeq.kernel.se.dto.module; |
17 | |
18 | import org.qedeq.base.utility.EqualsUtility; |
19 | import org.qedeq.kernel.se.base.module.Axiom; |
20 | import org.qedeq.kernel.se.base.module.FormalProofList; |
21 | import org.qedeq.kernel.se.base.module.Formula; |
22 | import org.qedeq.kernel.se.base.module.FunctionDefinition; |
23 | import org.qedeq.kernel.se.base.module.InitialFunctionDefinition; |
24 | import org.qedeq.kernel.se.base.module.InitialPredicateDefinition; |
25 | import org.qedeq.kernel.se.base.module.LatexList; |
26 | import org.qedeq.kernel.se.base.module.PredicateDefinition; |
27 | import org.qedeq.kernel.se.base.module.ProofList; |
28 | import org.qedeq.kernel.se.base.module.Proposition; |
29 | import org.qedeq.kernel.se.base.module.Rule; |
30 | |
31 | |
32 | /** |
33 | * Proposition. |
34 | * |
35 | * @author Michael Meyling |
36 | */ |
37 | public class PropositionVo implements Proposition { |
38 | |
39 | /** Proposition formula. */ |
40 | private Formula formula; |
41 | |
42 | /** Further proposition description. Normally <code>null</code>. */ |
43 | private LatexList description; |
44 | |
45 | /** List of non formal proofs. */ |
46 | private ProofListVo proofList; |
47 | |
48 | /** List of formal proofs. */ |
49 | private FormalProofListVo formalProofList; |
50 | |
51 | /** |
52 | * Constructs a new proposition. |
53 | */ |
54 | public PropositionVo() { |
55 | // nothing to do |
56 | } |
57 | |
58 | public Axiom getAxiom() { |
59 | return null; |
60 | } |
61 | |
62 | public InitialPredicateDefinition getInitialPredicateDefinition() { |
63 | return null; |
64 | } |
65 | |
66 | public PredicateDefinition getPredicateDefinition() { |
67 | return null; |
68 | } |
69 | |
70 | public InitialFunctionDefinition getInitialFunctionDefinition() { |
71 | return null; |
72 | } |
73 | |
74 | public FunctionDefinition getFunctionDefinition() { |
75 | return null; |
76 | } |
77 | |
78 | public Proposition getProposition() { |
79 | return this; |
80 | } |
81 | |
82 | public Rule getRule() { |
83 | return null; |
84 | } |
85 | |
86 | /** |
87 | * Set proposition formula. |
88 | * |
89 | * @param formula Proposition formula. |
90 | */ |
91 | public final void setFormula(final FormulaVo formula) { |
92 | this.formula = formula; |
93 | } |
94 | |
95 | public final Formula getFormula() { |
96 | return formula; |
97 | } |
98 | |
99 | /** |
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 | } |