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.bo.logic.common;
17
18 import java.util.ArrayList;
19 import java.util.List;
20
21 import org.qedeq.base.utility.EqualsUtility;
22 import org.qedeq.kernel.se.base.list.Element;
23 import org.qedeq.kernel.se.base.list.ElementList;
24 import org.qedeq.kernel.se.common.ModuleContext;
25
26 /**
27 * Function constant.
28 *
29 * @author Michael Meyling
30 */
31 public final class FunctionConstant {
32
33 /** Predicate key. */
34 private final FunctionKey key;
35
36 /** Complete formula. */
37 private final ElementList completeFormula;
38
39 /** In this context the function was defined. */
40 private final ModuleContext context;
41
42 /** Function with subject variables. */
43 private final ElementList function;
44
45 /** Defining term. */
46 private final ElementList definingTerm;
47
48 /** Parameter subject variables. */
49 private final List subjectVariables;
50
51 /**
52 * Constructor.
53 *
54 * @param key Function name.
55 * @param completeFormula Complete formula defining function. Includes function.
56 * Must be like: f(x, y) = {z | z \in x & z \in y}
57 * @param context Module context we are in.
58 */
59 public FunctionConstant(final FunctionKey key, final ElementList completeFormula,
60 final ModuleContext context) {
61 this.key = key;
62 this.completeFormula = completeFormula;
63 this.context = new ModuleContext(context); // using copy constructor to fix context
64 final ElementList list = completeFormula.getList();
65 function = list.getElement(1).getList();
66 definingTerm = list.getElement(2).getList();
67 subjectVariables = new ArrayList(function.size() - 1);
68 for (int i = 0; i < function.size() - 1; i++) {
69 subjectVariables.add(new SubjectVariable(
70 function.getElement(i + 1).getList().getElement(0).getAtom().getString()));
71 }
72 }
73
74 /**
75 * Get function key.
76 *
77 * @return Function key.
78 */
79 public FunctionKey getKey() {
80 return key;
81 }
82
83 /**
84 * Get function name.
85 *
86 * @return Function name.
87 */
88 public String getName() {
89 return key.getName();
90 }
91
92 /**
93 * Get function argument number.
94 *
95 * @return Number of arguments.
96 */
97 public String getArguments() {
98 return key.getArguments();
99 }
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 }