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.rule;
012:
013: import de.uka.ilkd.key.logic.Constraint;
014: import de.uka.ilkd.key.logic.RenameTable;
015: import de.uka.ilkd.key.logic.op.Metavariable;
016: import de.uka.ilkd.key.logic.op.QuantifiableVariable;
017: import de.uka.ilkd.key.logic.op.SetAsListOfMetavariable;
018: import de.uka.ilkd.key.logic.op.SetOfMetavariable;
019: import de.uka.ilkd.key.rule.inst.SVInstantiations;
020:
021: /**
022: * Simple container class containing the information resulting from a
023: * Taclet.match-call
024: */
025: public class MatchConditions {
026:
027: public static final MatchConditions EMPTY_MATCHCONDITIONS = new MatchConditions(
028: SVInstantiations.EMPTY_SVINSTANTIATIONS, Constraint.BOTTOM,
029: SetAsListOfMetavariable.EMPTY_SET, RenameTable.EMPTY_TABLE);
030:
031: private SVInstantiations instantiations = SVInstantiations.EMPTY_SVINSTANTIATIONS;
032: private Constraint constraint = Constraint.BOTTOM;
033: private SetOfMetavariable newMetavariables = SetAsListOfMetavariable.EMPTY_SET;
034:
035: private RenameTable renameTable = RenameTable.EMPTY_TABLE;
036:
037: public MatchConditions(SVInstantiations p_instantiations,
038: Constraint p_constraint,
039: SetOfMetavariable p_newMetavariables,
040: RenameTable p_renameTable) {
041: instantiations = p_instantiations;
042: constraint = p_constraint;
043: newMetavariables = p_newMetavariables;
044: renameTable = p_renameTable;
045: }
046:
047: public SVInstantiations getInstantiations() {
048: return instantiations;
049: }
050:
051: public MatchConditions setInstantiations(
052: SVInstantiations p_instantiations) {
053: if (instantiations == p_instantiations)
054: return this ;
055: else
056: return new MatchConditions(p_instantiations, constraint,
057: newMetavariables, renameTable);
058: }
059:
060: public Constraint getConstraint() {
061: return constraint;
062: }
063:
064: public MatchConditions setConstraint(Constraint p_constraint) {
065: if (constraint == p_constraint)
066: return this ;
067: else
068: return new MatchConditions(instantiations, p_constraint,
069: newMetavariables, renameTable);
070: }
071:
072: public SetOfMetavariable getNewMetavariables() {
073: return newMetavariables;
074: }
075:
076: public MatchConditions setNewMetavariables(
077: SetOfMetavariable p_newMetavariables) {
078: if (newMetavariables == p_newMetavariables)
079: return this ;
080: else
081: return new MatchConditions(instantiations, constraint,
082: p_newMetavariables, renameTable);
083: }
084:
085: public MatchConditions addNewMetavariable(Metavariable p_mv) {
086: return new MatchConditions(instantiations, constraint,
087: newMetavariables.add(p_mv), renameTable);
088: }
089:
090: public MatchConditions extendRenameTable() {
091: return new MatchConditions(instantiations, constraint,
092: newMetavariables, renameTable.extend());
093: }
094:
095: public MatchConditions addRenaming(QuantifiableVariable q1,
096: QuantifiableVariable q2) {
097: return new MatchConditions(instantiations, constraint,
098: newMetavariables, renameTable.assign(q1, q2));
099: }
100:
101: public RenameTable renameTable() {
102: return renameTable;
103: }
104:
105: public MatchConditions shrinkRenameTable() {
106: return new MatchConditions(instantiations, constraint,
107: newMetavariables, renameTable.parent());
108: }
109:
110: }
|