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