001: // This file is part of KeY - Integrated Deductive Software Design
002: // Copyright (C) 2001-2007 Universitaet Karlsruhe, Germany
003: // Universitaet Koblenz-Landau, Germany
004: // Chalmers University of Technology, Sweden
005: //
006: // The KeY system is protected by the GNU General Public License.
007: // See LICENSE.TXT for details.
008: //
009: //
010:
011: package de.uka.ilkd.key.logic.op;
012:
013: import de.uka.ilkd.key.logic.Name;
014: import de.uka.ilkd.key.logic.Term;
015: import de.uka.ilkd.key.logic.sort.ArrayOfSort;
016: import de.uka.ilkd.key.logic.sort.ProgramSVSort;
017: import de.uka.ilkd.key.logic.sort.Sort;
018:
019: public abstract class Function extends TermSymbol {
020:
021: /**
022: * sorts of arguments
023: */
024: private ArrayOfSort argSorts;
025:
026: /** creates a Function
027: * @param name String with name of the function
028: * @param sort the Sort of the function (result type)
029: * @param argSorts an array of Sort with the sorts of
030: * the function's arguments
031: */
032: public Function(Name name, Sort sort, Sort[] argSorts) {
033: this (name, sort, new ArrayOfSort(argSorts));
034: }
035:
036: /** creates a Function
037: * @param name String with name of the function
038: * @param sort the Sort of the function (result type)
039: * @param argSorts ArrayOfSort of the function's arguments
040: */
041: public Function(Name name, Sort sort, ArrayOfSort argSorts) {
042: super (name, sort);
043: this .argSorts = argSorts;
044: }
045:
046: /** @return array of allowed sorts of the function arguments */
047: public ArrayOfSort argSort() {
048: return argSorts;
049: }
050:
051: /** @return Sort of the n-th argument */
052: public Sort argSort(int n) {
053: return argSorts.getSort(n);
054: }
055:
056: /** @return arity of the Function as int */
057: public int arity() {
058: return argSorts.size();
059: }
060:
061: /**
062: * checks if a given Term could be subterm (at the atth subterm
063: * position) of a term with this function at its top level. The
064: * validity of the given subterm is NOT checked.
065: * @param at theposition of the term where this method should check
066: * the validity.
067: * @param possibleSub the subterm to be ckecked.
068: * @return true iff the given term can be subterm at the indicated
069: * position
070: */
071: public boolean possibleSub(int at, Term possibleSub) {
072: if (possibleSub.op() instanceof SchemaVariable
073: || possibleSub.sort() instanceof ProgramSVSort
074: || possibleSub.op() instanceof MetaOperator) {
075: return true;
076: }
077: return possibleSub.sort().extendsTrans(argSort(at));
078: }
079:
080: /**
081: * checks if given Terms could be subterms of a term with this
082: * function at its top level. The check includes the comparison of
083: * the required number of subterms and the number of given
084: * terms. The validity of the given subterms is NOT checked.
085: * @param possibleSubs the subterms to be ckecked.
086: * @return true iff the given terms can be subterms and the number of given
087: * terms and the required number of subterms are equal.
088: */
089: public boolean possibleSubs(Term[] possibleSubs) {
090: if (possibleSubs.length != arity())
091: return false;
092: for (int i = 0; i < arity(); i++) {
093: if (!possibleSub(i, possibleSubs[i])) {
094: return false;
095: }
096: }
097: return true;
098: }
099:
100: /**
101: * checks if the given term is syntactically valid at its top
102: * level assumed the top level operator were this, i.e. if the
103: * direct subterms can be subterms of a term with this top level
104: * operator, the method returns true. Furthermore, it is checked
105: * that no variables are bound for none of the subterms.
106: * @param term the Term to be checked.
107: * @return true iff the given term has subterms that are suitable
108: * for this function.
109: */
110: public boolean validTopLevel(Term term) {
111: if (term.arity() != arity()) {
112: return false;
113: }
114: for (int i = 0; i < arity(); i++) {
115: if (!possibleSub(i, term.sub(i))) {
116: return false;
117: }
118: //Need to comment this away because of OCL simplification
119: //BinaryBindingTerm & TernaryBindingTerm have
120: //"Function" as operator and have bound vars
121: //if (term.varsBoundHere(i).size()!=0) {
122: // return false;
123: //}
124: }
125: return true;
126: }
127:
128: public String toString() {
129: return (name() + ((sort() == Sort.FORMULA) ? "" : ":" + sort()));
130: }
131:
132: public String proofToString() {
133: String s = null;
134: if (sort() != null) {
135: s = sort().toString() + " " + name();
136: } else {
137: s = "NO_SORT" + " " + name();
138: }
139: if (arity() > 0) {
140: int i = 0;
141: s += "(";
142: while (i < arity()) {
143: if (i > 0)
144: s += ",";
145: s += argSort(i);
146: i++;
147: }
148: s += ")";
149: }
150: s += ";\n";
151: return s;
152: }
153:
154: }
|