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: package de.uka.ilkd.key.rule.metaconstruct;
09:
10: import java.util.*;
11:
12: import de.uka.ilkd.key.java.Services;
13: import de.uka.ilkd.key.logic.*;
14: import de.uka.ilkd.key.logic.op.*;
15: import de.uka.ilkd.key.logic.sort.Sort;
16: import de.uka.ilkd.key.proof.init.AbstractPO;
17: import de.uka.ilkd.key.rule.MatchConditions;
18: import de.uka.ilkd.key.rule.inst.SVInstantiations;
19:
20: public class AtPreEquations extends AbstractMetaOperator {
21:
22: private static Term updateFormula = null;
23: private static HashMap atPreMapping = null;
24:
25: public static Map getAtPreFunctions(Term t) {
26: if (t == updateFormula) {
27: // atPre Functions were already calculated for updateFormula
28: return atPreMapping;
29: }
30: updateFormula = t;
31: atPreMapping = new HashMap();
32: AbstractPO.createAtPreFunctionsForTerm(t, atPreMapping);
33: return atPreMapping;
34: }
35:
36: public AtPreEquations() {
37: super (new Name("#atPreEqs"), 1);
38: }
39:
40: /* (non-Javadoc)
41: * @see de.uka.ilkd.key.logic.op.MetaOperator#calculate(de.uka.ilkd.key.logic.Term, de.uka.ilkd.key.rule.inst.SVInstantiations, de.uka.ilkd.key.java.Services)
42: */
43: public Term calculate(Term term, SVInstantiations svInst,
44: Services services) {
45: Map atPreFunctions = getAtPreFunctions(term.sub(0));
46: final Iterator it = atPreFunctions.values().iterator();
47: while (it.hasNext()) {
48: services.getNamespaces().functions().add(
49: (Function) it.next());
50: }
51: return AbstractPO.buildAtPreDefinitions(atPreFunctions);
52: }
53:
54: /* (non-Javadoc)
55: * @see de.uka.ilkd.key.logic.op.Operator#validTopLevel(de.uka.ilkd.key.logic.Term)
56: */
57: public boolean validTopLevel(Term term) {
58: return term.arity() == 1 && term.sub(0).sort() == Sort.FORMULA;
59: }
60:
61: /* (non-Javadoc)
62: * @see de.uka.ilkd.key.logic.op.Operator#sort(de.uka.ilkd.key.logic.Term[])
63: */
64: public Sort sort(Term[] term) {
65: return Sort.FORMULA;
66: }
67:
68: /* (non-Javadoc)
69: * @see de.uka.ilkd.key.logic.op.Operator#isRigid(de.uka.ilkd.key.logic.Term)
70: */
71: public boolean isRigid(Term term) {
72: return false;
73: }
74:
75: /** (non-Javadoc)
76: * by default meta operators do not match anything
77: * @see de.uka.ilkd.key.logic.op.Operator#match(SVSubstitute, de.uka.ilkd.key.rule.MatchConditions, de.uka.ilkd.key.java.Services)
78: */
79: public MatchConditions match(SVSubstitute subst,
80: MatchConditions mc, Services services) {
81: return null;
82: }
83:
84: }
|