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.se.dto.module;
017
018 import org.qedeq.base.utility.EqualsUtility;
019 import org.qedeq.kernel.se.base.module.FormalProofLine;
020 import org.qedeq.kernel.se.base.module.Formula;
021 import org.qedeq.kernel.se.base.module.ReasonType;
022
023
024 /**
025 * Contains a formal proof for a proposition.
026 *
027 * @author Michael Meyling
028 */
029 public class FormalProofLineVo implements FormalProofLine {
030
031 /** Label for back references. Might be <code>null</code>. */
032 private String label;
033
034 /** Rule that is used for deriving. */
035 private ReasonType reasonType;
036
037 /** Derived formula. */
038 private Formula formula;
039
040 /**
041 * Constructs an proof line.
042 *
043 * @param formula New derived formula.
044 * @param reasonType Rule that was used to derive the formula.
045 */
046 public FormalProofLineVo(final Formula formula, final ReasonType reasonType) {
047 this.label = null;
048 this.reasonType = reasonType;
049 this.formula = formula;
050 }
051
052 /**
053 * Constructs an proof line.
054 *
055 * @param label Label for back references. Might be <code>null</code>.
056 * @param formula New derived formula.
057 * @param reasonType Rule that was used to derive the formula.
058 */
059 public FormalProofLineVo(final String label, final Formula formula, final ReasonType reasonType) {
060 this.label = label;
061 this.reasonType = reasonType;
062 this.formula = formula;
063 }
064
065 /**
066 * Default constructor.
067 */
068 public FormalProofLineVo() {
069 // nothing to do
070 }
071
072 public Formula getFormula() {
073 return formula;
074 }
075
076 /**
077 * Set proof line formula.
078 *
079 * @param formula Set formula.
080 */
081 public void setFormula(final Formula formula) {
082 this.formula = formula;
083 }
084
085 public String getLabel() {
086 return label;
087 }
088
089 /**
090 * Set label for proof line.
091 *
092 * @param label Set this label.
093 */
094 public void setLabel(final String label) {
095 this.label = label;
096 }
097
098 public ReasonType getReasonType() {
099 return reasonType;
100 }
101
102 /**
103 * Set reason type for proof line.
104 *
105 * @param reasonType Set this reason type.
106 */
107 public void setReasonType(final ReasonType reasonType) {
108 this.reasonType = reasonType;
109 }
110
111 public boolean equals(final Object obj) {
112 if (!(obj instanceof FormalProofLineVo)) {
113 return false;
114 }
115 final FormalProofLineVo other = (FormalProofLineVo) obj;
116 return EqualsUtility.equals(label, other.label)
117 && EqualsUtility.equals(formula, other.formula)
118 && EqualsUtility.equals(reasonType, other.reasonType);
119 }
120
121 public int hashCode() {
122 return (label != null ? label.hashCode() : 0)
123 ^ (formula != null ? 1 ^ formula.hashCode() : 0)
124 ^ (reasonType != null ? 2 ^ reasonType.hashCode() : 0);
125 }
126
127 public String toString() {
128 return (label != null ? "[" + label + "] " : " ") + getFormula() + " "
129 + getReasonType();
130 }
131
132 }
|