01: // This file is part of KeY - Integrated Deductive Software Design
02: // Copyright (C) 2001-2007 Universitaet Karlsruhe, Germany
03: // Universitaet Koblenz-Landau, Germany
04: // Chalmers University of Technology, Sweden
05: //
06: // The KeY system is protected by the GNU General Public License.
07: // See LICENSE.TXT for details.
08: //
09: //
10:
11: /* Generated by Together */
12:
13: package de.uka.ilkd.key.logic.op;
14:
15: import de.uka.ilkd.key.logic.ClashFreeSubst;
16: import de.uka.ilkd.key.logic.Name;
17: import de.uka.ilkd.key.logic.Term;
18: import de.uka.ilkd.key.logic.sort.Sort;
19:
20: /**
21: * Standard first-order substitution operator, resolving clashes but not
22: * preventing (usually unsound) substitution of non-rigid terms across modal
23: * operators. Currently, only the subclass <code>WarySubstOp</code> is used
24: * and accessible through the key parser.
25: */
26: public class SubstOp extends Op {
27:
28: SubstOp(Name name) {
29: super (name);
30: }
31:
32: /**
33: * @return true iff the sort of the subterm 0 of the given term
34: * has the same sort as or a subsort of the variable to be substituted
35: * and the
36: * term's arity is 2 and the numer of variables bound there is 0
37: * for the 0th subterm and 1 for the 1st subterm.
38: */
39: public boolean validTopLevel(Term term) {
40: if (term.arity() != 2)
41: return false;
42: if (term.varsBoundHere(1).size() != 1)
43: return false;
44: if (term.varsBoundHere(0).size() != 0)
45: return false;
46: Sort substSort = term.sub(0).sort();
47: Sort varSort = term.varsBoundHere(1).getQuantifiableVariable(0)
48: .sort();
49: return substSort.extendsTrans(varSort);
50: }
51:
52: /**
53: * @return sort of the second subterm or throws an
54: * IllegalArgumentException if the given term has no correct (2=) arity
55: */
56: public Sort sort(Term[] term) {
57: if (term.length == 2)
58: return term[1].sort();
59: else
60: throw new IllegalArgumentException(
61: "Cannot determine sort of "
62: + "invalid term (Wrong arity).");
63: }
64:
65: /** @return arity of the Substitution operator as int */
66: public int arity() {
67: return 2;
68: }
69:
70: /**
71: * Apply this substitution operator to <code>term</code>, which
72: * has this operator as top-level operator
73: */
74: public Term apply(Term term) {
75: QuantifiableVariable v = term.varsBoundHere(1)
76: .getQuantifiableVariable(0);
77: ClashFreeSubst cfSubst = new ClashFreeSubst(v, term.sub(0));
78: Term res = cfSubst.apply(term.sub(1));
79: return res;
80: }
81: }
|