View Javadoc

1   /* This file is part of the project "Hilbert II" - http://www.qedeq.org" target="alexandria_uri">http://www.qedeq.org
2    *
3    * Copyright 2000-2014,  Michael Meyling <mime@qedeq.org>.
4    *
5    * "Hilbert II" is free software; you can redistribute
6    * it and/or modify it under the terms of the GNU General Public
7    * License as published by the Free Software Foundation; either
8    * version 2 of the License, or (at your option) any later version.
9    *
10   * This program is distributed in the hope that it will be useful,
11   * but WITHOUT ANY WARRANTY; without even the implied warranty of
12   * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
13   * GNU General Public License for more details.
14   */
15  
16  package org.qedeq.kernel.se.dto.module;
17  
18  import org.apache.commons.lang.ArrayUtils;
19  import org.qedeq.base.utility.EqualsUtility;
20  import org.qedeq.kernel.se.base.list.Element;
21  import org.qedeq.kernel.se.base.module.SubstFunc;
22  
23  
24  /**
25   * Usage of rule for substitute function variable.
26   *
27   * @author  Michael Meyling
28   */
29  public class SubstFuncVo implements SubstFunc {
30  
31      /** Reference to previously proven formula. */
32      private String reference;
33  
34      /** Function variable that will be substituted. */
35      private Element functionVariable;
36  
37      /** Replacement term. */
38      private Element substituteTerm;
39  
40      /**
41       * Constructs an reason.
42       *
43       * @param   reference                   Reference to a valid formula.
44       * @param   functionVariable            Function variable that will be substituted.
45       * @param   substituteFormula           Replacement term.
46       */
47  
48      public SubstFuncVo(final String reference, final Element functionVariable,
49              final Element substituteFormula) {
50          this.reference = reference;
51          this.functionVariable = functionVariable;
52          this.substituteTerm = substituteFormula;
53      }
54  
55      /**
56       * Default constructor.
57       */
58      public SubstFuncVo() {
59          // nothing to do
60      }
61  
62      public SubstFunc getSubstFunc() {
63          return this;
64      }
65  
66      public String getReference() {
67          return reference;
68      }
69  
70      /**
71       * Set formula reference.
72       *
73       * @param   reference   Reference to formula.
74       */
75      public void setReference(final String reference) {
76          this.reference = reference;
77      }
78  
79      public String[] getReferences() {
80          if (reference == null) {
81              return ArrayUtils.EMPTY_STRING_ARRAY;
82          }
83          return new String[] {reference };
84      }
85  
86      public Element getFunctionVariable() {
87          return functionVariable;
88      }
89  
90      /**
91       * Set function variable that will be substituted.
92       *
93       * @param   functionVariable  Function variable that will be replaced.
94       */
95      public void setFunctionVariable(final Element functionVariable) {
96          this.functionVariable = functionVariable;
97      }
98  
99      public Element getSubstituteTerm() {
100         return substituteTerm;
101     }
102 
103     /**
104      * Set substitution term.
105      *
106      * @param   substituteTerm  New term.
107      */
108     public void setSubstituteTerm(final Element substituteTerm) {
109         this.substituteTerm = substituteTerm;
110     }
111 
112     public String getName() {
113         return "SubstFun";
114     }
115 
116     public boolean equals(final Object obj) {
117         if (!(obj instanceof SubstFuncVo)) {
118             return false;
119         }
120         final SubstFuncVo other = (SubstFuncVo) obj;
121         return EqualsUtility.equals(reference, other.reference)
122             && EqualsUtility.equals(functionVariable, other.functionVariable)
123             && EqualsUtility.equals(substituteTerm, other.substituteTerm);
124     }
125 
126     public int hashCode() {
127         return (reference != null ? reference.hashCode() : 0)
128             ^ (functionVariable != null ? 2 ^ functionVariable.hashCode() : 0)
129             ^ (substituteTerm != null ? 3 ^ substituteTerm.hashCode() : 0);
130     }
131 
132     public String toString() {
133         StringBuffer result = new StringBuffer();
134         result.append(getName());
135         if (reference != null || functionVariable != null
136                 || substituteTerm != null) {
137             result.append(" (");
138             boolean w = false;
139             if (reference != null) {
140                 result.append(reference);
141                 w = true;
142             }
143             if (functionVariable != null) {
144                 if (w) {
145                     result.append(", ");
146                 }
147                 result.append(functionVariable);
148                 w = true;
149             }
150             if (substituteTerm != null) {
151                 if (w) {
152                     result.append(", ");
153                 }
154                 result.append("by ");
155                 result.append(substituteTerm);
156                 w = true;
157             }
158             result.append(")");
159         }
160         return result.toString();
161     }
162 
163 }