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.logic.common;
017
018 import java.util.ArrayList;
019 import java.util.List;
020
021 import org.qedeq.base.utility.EqualsUtility;
022 import org.qedeq.kernel.se.base.list.Element;
023 import org.qedeq.kernel.se.base.list.ElementList;
024 import org.qedeq.kernel.se.common.ModuleContext;
025
026 /**
027 * Function constant.
028 *
029 * @author Michael Meyling
030 */
031 public final class FunctionConstant {
032
033 /** Predicate key. */
034 private final FunctionKey key;
035
036 /** Complete formula. */
037 private final ElementList completeFormula;
038
039 /** In this context the function was defined. */
040 private final ModuleContext context;
041
042 /** Function with subject variables. */
043 private final ElementList function;
044
045 /** Defining term. */
046 private final ElementList definingTerm;
047
048 /** Parameter subject variables. */
049 private final List subjectVariables;
050
051 /**
052 * Constructor.
053 *
054 * @param key Function name.
055 * @param completeFormula Complete formula defining function. Includes function.
056 * Must be like: f(x, y) = {z | z \in x & z \in y}
057 * @param context Module context we are in.
058 */
059 public FunctionConstant(final FunctionKey key, final ElementList completeFormula,
060 final ModuleContext context) {
061 this.key = key;
062 this.completeFormula = completeFormula;
063 this.context = new ModuleContext(context); // using copy constructor to fix context
064 final ElementList list = completeFormula.getList();
065 function = list.getElement(1).getList();
066 definingTerm = list.getElement(2).getList();
067 subjectVariables = new ArrayList(function.size() - 1);
068 for (int i = 0; i < function.size() - 1; i++) {
069 subjectVariables.add(new SubjectVariable(
070 function.getElement(i + 1).getList().getElement(0).getAtom().getString()));
071 }
072 }
073
074 /**
075 * Get function key.
076 *
077 * @return Function key.
078 */
079 public FunctionKey getKey() {
080 return key;
081 }
082
083 /**
084 * Get function name.
085 *
086 * @return Function name.
087 */
088 public String getName() {
089 return key.getName();
090 }
091
092 /**
093 * Get function argument number.
094 *
095 * @return Number of arguments.
096 */
097 public String getArguments() {
098 return key.getArguments();
099 }
100
101 /**
102 * Get complete defining formula. Includes function itself.
103 *
104 * @return Complete defining formula.
105 */
106 public Element getCompleteFormula() {
107 return completeFormula;
108 }
109
110 /**
111 * Get context where the complete formula is.
112 *
113 * @return Module context for complete formula.
114 */
115 public ModuleContext getContext() {
116 return context;
117 }
118 /**
119 * Get function with parameters.
120 *
121 * @return Function term with subject variables.
122 */
123 public ElementList getFunction() {
124 return function;
125 }
126
127 /**
128 * Get list of parameter subject variables.
129 *
130 * @return Parameter subject variables as a list.
131 */
132 public List getSubjectVariables() {
133 return subjectVariables;
134 }
135
136 /**
137 * Get defining term. Function itself is not included.
138 *
139 * @return Defining term only.
140 */
141 public Element getDefiningTerm() {
142 return definingTerm;
143 }
144
145 public int hashCode() {
146 return (getKey() != null ? getKey().hashCode() : 0)
147 ^ (getCompleteFormula() != null ? getCompleteFormula().hashCode() : 0);
148 }
149
150 public boolean equals(final Object obj) {
151 if (!(obj instanceof FunctionConstant)) {
152 return false;
153 }
154 final FunctionConstant other = (FunctionConstant) obj;
155 return EqualsUtility.equals(getKey(), other.getKey())
156 && EqualsUtility.equals(getCompleteFormula(), other.getCompleteFormula());
157 }
158
159 public String toString() {
160 return getName() + "[" + getArguments() + "]";
161 }
162
163
164 }
|