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.bo.module;
017
018 import org.qedeq.kernel.bo.common.NodeBo;
019 import org.qedeq.kernel.bo.common.QedeqBo;
020 import org.qedeq.kernel.se.base.list.Element;
021 import org.qedeq.kernel.se.base.module.ConditionalProof;
022 import org.qedeq.kernel.se.base.module.FormalProofLineList;
023 import org.qedeq.kernel.se.base.module.FormalProofList;
024 import org.qedeq.kernel.se.base.module.NodeType;
025 import org.qedeq.kernel.se.base.module.Proposition;
026 import org.qedeq.kernel.se.base.module.Reason;
027 import org.qedeq.kernel.se.common.CheckLevel;
028 import org.qedeq.kernel.se.common.ModuleContext;
029 import org.qedeq.kernel.se.dto.module.NodeVo;
030 import org.qedeq.kernel.se.visitor.QedeqNumbers;
031
032 /**
033 * Business object for node access.
034 *
035 * @author Michael Meyling
036 */
037 public class KernelNodeBo implements NodeBo, CheckLevel {
038
039 /** The plain node data. */
040 private final NodeVo node;
041
042 /** The module context the node is within. */
043 private final ModuleContext context;
044
045 /** Parent module the node is within. */
046 private final KernelQedeqBo qedeq;
047
048 /** Herein are the results of various counters for the node. */
049 private final QedeqNumbers data;
050
051 /** Are all formal formulas of this node well formed.
052 * See {@link CheckLevel} for value format. */
053 private int wellFormedCheck;
054
055 /** Is this node been successfully formally proved at least once.
056 * See {@link CheckLevel} for value format. */
057 private int provedCheck;
058
059
060 /**
061 * Constructor.
062 *
063 * @param node The plain node data.
064 * @param context The module context the node is within.
065 * @param qedeq Parent module the node is within.
066 * @param data Herein are the results of various counters for the node.
067 */
068 public KernelNodeBo(final NodeVo node, final ModuleContext context, final KernelQedeqBo qedeq,
069 final QedeqNumbers data) {
070 this.node = node;
071 this.context = new ModuleContext(context);
072 this.qedeq = qedeq;
073 this.data = new QedeqNumbers(data);
074 }
075
076 /**
077 * Get plain node data.
078 *
079 * @return The plain node data.
080 */
081 public NodeVo getNodeVo() {
082 return node;
083 }
084
085 /**
086 * Get module context the node is within.
087 *
088 * @return The module context the node is within.
089 */
090 public ModuleContext getModuleContext() {
091 return context;
092 }
093
094 /**
095 * Get parent module the node is within.
096 *
097 * @return Parent module the node is within.
098 */
099 public QedeqBo getParentQedeqBo() {
100 return qedeq;
101 }
102
103 /**
104 * Get parent module the node is within.
105 *
106 * @return Parent module the node is within.
107 */
108 public KernelQedeqBo getQedeqBo() {
109 return qedeq;
110 }
111
112 /**
113 * Get the results of various counters for the node.
114 *
115 * @return Herein are the results of various counters for the node.
116 */
117 public QedeqNumbers getNumbers() {
118 return data;
119 }
120
121 /**
122 * // FIXME 20110316 m31: we have to solve the uniqueness problem if we have several formal proofs
123 * Is the given name a proof line label within this node?
124 *
125 * @param label Look if this node is a proposition that contains this label name.
126 * @return Answer.
127 */
128 public boolean isProofLineLabel(final String label) {
129 if (label == null || label.length() == 0) {
130 return false;
131 }
132 final Proposition theorem = getNodeVo().getNodeType().getProposition();
133 if (theorem == null) {
134 return false;
135 }
136 final FormalProofList proofs = theorem.getFormalProofList();
137 if (proofs == null) {
138 return false;
139 }
140 // iterate through all formal proofs
141 for (int i = 0; i < proofs.size(); i++) {
142 final FormalProofLineList list = proofs.get(i).getFormalProofLineList();
143 if (hasProofLineLabel(label, list)) {
144 return true;
145 }
146 }
147 // nowhere found:
148 return false;
149 }
150
151 private boolean hasProofLineLabel(final String label, final FormalProofLineList list) {
152 if (list == null) {
153 return false;
154 }
155 for (int j = 0; j < list.size(); j++) {
156 if (label.equals(list.get(j).getLabel())) {
157 return true;
158 }
159 final Reason reason = list.get(j).getReason();
160 if (reason instanceof ConditionalProof) {
161 final ConditionalProof conditionalProof = (ConditionalProof) reason;
162 if (conditionalProof.getHypothesis() != null) {
163 if (label.equals(conditionalProof.getHypothesis().getLabel())) {
164 return true;
165 }
166 }
167 final FormalProofLineList list2 = conditionalProof.getFormalProofLineList();
168 if (hasProofLineLabel(label, list2)) {
169 return true;
170 }
171 }
172 }
173 return false;
174 }
175
176 /**
177 * Set proved parameter. See {@link #isWellFormed()}.
178 *
179 * @param wellFormedCheck Node well formed state.
180 * See {@link CheckLevel} for parameter format.
181 */
182 public void setWellFormed(final int wellFormedCheck) {
183 this.wellFormedCheck = wellFormedCheck;
184 }
185
186 public boolean isWellFormed() {
187 return wellFormedCheck >= SUCCESS;
188 }
189
190 public boolean isNotWellFormed() {
191 return wellFormedCheck < SUCCESS && wellFormedCheck > UNCHECKED;
192 }
193
194 /**
195 * Set proved parameter. See {@link #isProved()}.
196 *
197 * @param provedCheck Node proved state.
198 * See {@link CheckLevel} for parameter format.
199 */
200 public void setProved(final int provedCheck) {
201 this.provedCheck = provedCheck;
202 }
203
204 public boolean isProved() {
205 return provedCheck >= SUCCESS;
206 }
207
208 public boolean isNotProved() {
209 return provedCheck < SUCCESS && provedCheck > UNCHECKED;
210 }
211
212 public boolean hasFormula() {
213 return null != getFormula();
214 }
215
216 public Element getFormula() {
217 if (getNodeVo() == null || getNodeVo().getNodeType() == null) {
218 return null;
219 }
220 final NodeType nodeType = getNodeVo().getNodeType();
221 if (nodeType.getProposition() != null) {
222 if (nodeType.getProposition().getFormula() != null) {
223 return nodeType.getProposition().getFormula().getElement();
224 } else {
225 return null;
226 }
227 } else if (nodeType.getPredicateDefinition() != null) {
228 if (nodeType.getPredicateDefinition().getFormula() != null) {
229 return nodeType.getPredicateDefinition().getFormula().getElement();
230 } else {
231 return null;
232 }
233 } else if (nodeType.getFunctionDefinition() != null) {
234 if (nodeType.getFunctionDefinition().getFormula() != null) {
235 return nodeType.getFunctionDefinition().getFormula().getElement();
236 } else {
237 return null;
238 }
239 } else if (nodeType.getAxiom() != null) {
240 if (nodeType.getAxiom().getFormula() != null) {
241 return nodeType.getAxiom().getFormula().getElement();
242 } else {
243 return null;
244 }
245 }
246 return null;
247 }
248 }
|