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.common;
017
018 import org.qedeq.kernel.se.base.list.Element;
019 import org.qedeq.kernel.se.common.ModuleContext;
020 import org.qedeq.kernel.se.dto.module.NodeVo;
021 import org.qedeq.kernel.se.visitor.QedeqNumbers;
022
023 /**
024 * Represents a node and its properties.
025 *
026 * @author Michael Meyling
027 */
028 public interface NodeBo {
029
030 /**
031 * Get parent the node is in.
032 *
033 * @return Parent module for this node.
034 */
035 public QedeqBo getParentQedeqBo();
036
037 /**
038 * Get numbers of node.
039 *
040 * @return Node numbers.
041 */
042 public QedeqNumbers getNumbers();
043
044 /**
045 * Get module context the node is within.
046 *
047 * @return The module context the node is within.
048 */
049 public ModuleContext getModuleContext();
050
051 /**
052 * Was this node checked successfully for formal correctness? This means checking the formal
053 * syntax of the node formulas. This includes all formulas. LaTeX correctness doesn't play any
054 * role. Nodes without formal formulas return always <code>true</code>.
055 *
056 * @return <code>true</code> if the check was successful.
057 */
058 public boolean isWellFormed();
059
060 /**
061 * Was this node checked unsuccessfully for formal correctness? This means checking the formal
062 * syntax of the node formulas. This includes all formulas. LaTeX correctness doesn't play any
063 * role. Nodes without formal formulas return always <code>false</code>.
064 *
065 * @return <code>true</code> if the check was not successful.
066 */
067 public boolean isNotWellFormed();
068
069 /**
070 * This means that at least one formal proof was successfully checked for correctness and a
071 * rule declaration was possible.
072 * If we have no proposition and no rule we always get <code>true</code>.
073 *
074 * @return <code>true</code> if the check was successful.
075 */
076 public boolean isProved();
077
078 /**
079 * This means for propositions that at least not even one formal proof could be successfully
080 * checked for correctness. For rules we get the question answered if a declaration is ok.
081 * If we have no proposition and no rule we always get <code>false</code>.
082 *
083 * @return <code>true</code> if the check was not successful.
084 */
085 public boolean isNotProved();
086
087 /**
088 * Has this node a formula?
089 *
090 * @return Formula.
091 */
092 public boolean hasFormula();
093
094 /**
095 * Get formula of node. Can only be not <code>null</code> if this node is an Axiom,
096 * PredicateDefinition, FunctionDefinition or Proposition.
097 *
098 * @return Node formula.
099 */
100 public Element getFormula();
101
102 /**
103 * Get node.
104 *
105 * @return Node.
106 */
107 public NodeVo getNodeVo();
108
109 }
|