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.Add;
020 import org.qedeq.kernel.se.base.module.Existential;
021 import org.qedeq.kernel.se.base.module.ModusPonens;
022 import org.qedeq.kernel.se.base.module.Reason;
023 import org.qedeq.kernel.se.base.module.ReasonType;
024 import org.qedeq.kernel.se.base.module.Rename;
025 import org.qedeq.kernel.se.base.module.SubstFree;
026 import org.qedeq.kernel.se.base.module.SubstFunc;
027 import org.qedeq.kernel.se.base.module.SubstPred;
028 import org.qedeq.kernel.se.base.module.Universal;
029
030
031 /**
032 * Contains a formal proof for a proposition.
033 *
034 * @author Michael Meyling
035 */
036 public class ReasonTypeVo implements ReasonType {
037
038 /** Rule that is used for deriving. */
039 private Reason reason;
040
041 /**
042 * Constructs an proof line.
043 *
044 * @param reason Rule that was used to derive the formula.
045 */
046 public ReasonTypeVo(final Reason reason) {
047 this.reason = reason;
048 }
049
050 /**
051 * Default constructor.
052 */
053 public ReasonTypeVo() {
054 // nothing to do
055 }
056
057 public Reason getReason() {
058 return reason;
059 }
060
061 /**
062 * Set used rule for proof line.
063 *
064 * @param reason This rule was used.
065 */
066 public void setReason(final Reason reason) {
067 this.reason = reason;
068 }
069
070 public Add getAdd() {
071 if (reason instanceof Add) {
072 return (Add) reason;
073 }
074 return null;
075 }
076
077 public Existential getExistential() {
078 if (reason instanceof Existential) {
079 return (Existential) reason;
080 }
081 return null;
082 }
083
084 public ModusPonens getModusPonens() {
085 if (reason instanceof ModusPonens) {
086 return (ModusPonens) reason;
087 }
088 return null;
089 }
090
091 public Rename getRename() {
092 if (reason instanceof Rename) {
093 return (Rename) reason;
094 }
095 return null;
096 }
097
098 public SubstFree getSubstFree() {
099 if (reason instanceof SubstFree) {
100 return (SubstFree) reason;
101 }
102 return null;
103 }
104
105 public SubstFunc getSubstFunc() {
106 if (reason instanceof SubstFunc) {
107 return (SubstFunc) reason;
108 }
109 return null;
110 }
111
112 public SubstPred getSubstPred() {
113 if (reason instanceof SubstPred) {
114 return (SubstPred) reason;
115 }
116 return null;
117 }
118
119 public Universal getUniversal() {
120 if (reason instanceof Universal) {
121 return (Universal) reason;
122 }
123 return null;
124 }
125
126 public boolean equals(final Object obj) {
127 if (!(obj instanceof ReasonTypeVo)) {
128 return false;
129 }
130 final ReasonTypeVo other = (ReasonTypeVo) obj;
131 return EqualsUtility.equals(reason, other.reason);
132 }
133
134 public int hashCode() {
135 return (reason != null ? reason.hashCode() : 0);
136 }
137
138 public String toString() {
139 return (reason != null ? reason.toString() : "");
140 }
141
142 }
|