0001: // This file is part of KeY - Integrated Deductive Software Design
0002: // Copyright (C) 2001-2007 Universitaet Karlsruhe, Germany
0003: // Universitaet Koblenz-Landau, Germany
0004: // Chalmers University of Technology, Sweden
0005: //
0006: // The KeY system is protected by the GNU General Public License.
0007: // See LICENSE.TXT for details.
0008: //
0009: //
0010:
0011: package de.uka.ilkd.key.rule;
0012:
0013: import de.uka.ilkd.key.java.ContextStatementBlock;
0014: import de.uka.ilkd.key.java.Services;
0015: import de.uka.ilkd.key.java.SourceData;
0016: import de.uka.ilkd.key.logic.*;
0017: import de.uka.ilkd.key.logic.op.*;
0018: import de.uka.ilkd.key.proof.Goal;
0019: import de.uka.ilkd.key.proof.IteratorOfGoal;
0020: import de.uka.ilkd.key.proof.ListOfGoal;
0021: import de.uka.ilkd.key.rule.inst.IllegalInstantiationException;
0022: import de.uka.ilkd.key.rule.inst.IteratorOfGenericSortCondition;
0023: import de.uka.ilkd.key.rule.inst.ListOfGenericSortCondition;
0024: import de.uka.ilkd.key.rule.inst.SVInstantiations;
0025: import de.uka.ilkd.key.util.Debug;
0026:
0027: /**
0028: * Taclets are the DL-extension of schematic theory specific rules. They are
0029: * used to describe rules of a logic (sequent) calculus. A typical taclet
0030: * definition looks similar to <br></br>
0031: * <code>
0032: * taclet_name { if ( ... ) find ( ... ) goal_descriptions }
0033: * </code> <br></br>
0034: * where the if-part must and the find-part can contain a sequent arrow, that
0035: * indicates, if a term has to occur at the top level and if so, on which side of
0036: * the sequent. The goal descriptions consists of lists of add and replacewith
0037: * constructs. They describe, how to construct a new goal out of the old one by
0038: * adding or replacing parts of the sequent. Each of these lists describe a new
0039: * goal, whereas if no such list exists, means that the goal is closed. <p>
0040: * The find part of a taclet is used to attached the rule to a term in the
0041: * sequent of the current goal. Therefore the term of the sequent has to match
0042: * the schema as found in the taclet's find part. The taclet is then attached to
0043: * this term, more precise not the taclet itself, but an application object of
0044: * this taclet (see {@link de.uka.ilkd.key.rule.TacletApp TacletApp}. When
0045: * this attached taclet application object is applied, the new goals are
0046: * constructed as described by the goal descriptions. For example <br></br>
0047: * <code>
0048: * find (A | B ==>) replacewith ( A ==> ); replacewith(B ==>)
0049: * </code> <br></br>creates
0050: * two new goals, where the first has been built by replacing <code> A | B </code>
0051: * with <code>A</code> and the second one by replacing <code>A | B</code> with
0052: * <code>B</code>. For a complete description of the syntax and semantics of
0053: * taclets consult the KeY-Manual. The objects of this class serve different
0054: * purposes: First they represent the syntactical structure of a taclet, but
0055: * they also include the taclet interpreter isself. The taclet interpreter
0056: * knows two modes: the match and the execution mode. The match mode tries to
0057: * find a a mapping from schemavariables to a given term or formula. In the
0058: * execution mode, a given goal is manipulated in the manner as described by the
0059: * goal descriptions. </p>
0060: * <p>
0061: * But an object of this class neither copies or split the goal, nor it
0062: * iterates through a sequent looking where it can be applied, these tasks have
0063: * to be done in advance. For example by one of the following classes
0064: * {@link de.uka.ilkd.key.proof.RuleAppIndex RuleAppIndex} or
0065: * {@link de.uka.ilkd.key.proof.TacletAppIndex TacletAppIndex} or
0066: * {@link de.uka.ilkd.key.rule.TacletApp TacletApp} </p>
0067: */
0068: public abstract class Taclet implements Rule, Named {
0069:
0070: private static final String AUTONAME = "_taclet";
0071:
0072: /** name of the taclet */
0073: private final Name name;
0074: /** name displayed by the pretty printer */
0075: private final String displayName;
0076: /** list of old names for downward compatibility */
0077: private final ListOfName oldNames;
0078: /** contains useful text explaining the taclet */
0079: private final String helpText = null;
0080: /** the set of taclet options for this taclet */
0081: protected final SetOfChoice choices;
0082:
0083: /**
0084: * the <tt>if</tt> sequent of the taclet
0085: */
0086: private final Sequent ifSequent;
0087: /**
0088: * Variables that have to be created each time the taclet is applied.
0089: * Those variables occur in the varcond part of a taclet description.
0090: */
0091: private final ListOfNewVarcond varsNew;
0092: /**
0093: * variables with a "x not free in y" variable condition. This means the
0094: * instantiation of VariableSV x must not occur free in the instantiation of
0095: * TermSV y.
0096: */
0097: private final ListOfNotFreeIn varsNotFreeIn;
0098: /**
0099: * variable conditions used to express that a termsv depends on the free
0100: * variables of a given formula(SV)
0101: * Used by skolemization rules.
0102: */
0103: private final ListOfNewDependingOn varsNewDependingOn;
0104:
0105: /** Additional generic conditions for schema variable instantiations. */
0106: private final ListOfVariableCondition variableConditions;
0107:
0108: /**
0109: * the list of taclet goal descriptions
0110: */
0111: private final ListOfTacletGoalTemplate goalTemplates;
0112:
0113: /**
0114: * list of rulesets (formerly known as heuristica) the taclet belongs to
0115: */
0116: protected final ListOfRuleSet ruleSets;
0117:
0118: /**
0119: * should taclet be applied by strategies only
0120: */
0121: private final boolean noninteractive;
0122: /**
0123: * constraint under which the Taclet is valid
0124: */
0125: private final Constraint constraint;
0126:
0127: /**
0128: * map from a schemavariable to its prefix. The prefix is used to test
0129: * correct instantiations of the schemavariables by resolving/avoiding
0130: * collisions. Mainly the prefix consists of a list of all variables that
0131: * may appear free in the instantiation of the schemavariable (a bit more
0132: * complicated for rewrite taclets, see paper of M:Giese)
0133: */
0134: protected final MapFromSchemaVariableToTacletPrefix prefixMap;
0135:
0136: /** cache */
0137: protected SetOfSchemaVariable addedRuleNameVars = null;
0138:
0139: /** cache; contains set of all bound variables */
0140: private SetOfQuantifiableVariable boundVariables = null;
0141:
0142: /** tracks state of pre-computation */
0143: private boolean contextInfoComputed = false;
0144: private boolean contextIsInPrefix = false;
0145: /** true if one of the goal descriptions is a replacewith */
0146: private boolean hasReplaceWith = false;
0147:
0148: protected String tacletAsString;
0149:
0150: /** Set of schemavariables of the if part */
0151: private SetOfSchemaVariable ifVariables = null;
0152:
0153: /** This map contains (a, b) if there is a substitution {b a}
0154: * somewhere in this taclet */
0155: private MapFromSchemaVariableToSchemaVariable svNameCorrespondences = null;
0156:
0157: /** Integer to cache the hashcode */
0158: private int hashcode = 0;
0159:
0160: /**
0161: * creates an empty Taclet
0162: */
0163: private Taclet() {
0164: name = new Name("");
0165: ifSequent = Sequent.EMPTY_SEQUENT;
0166: varsNew = SLListOfNewVarcond.EMPTY_LIST;
0167: varsNotFreeIn = SLListOfNotFreeIn.EMPTY_LIST;
0168: varsNewDependingOn = SLListOfNewDependingOn.EMPTY_LIST;
0169: variableConditions = SLListOfVariableCondition.EMPTY_LIST;
0170: goalTemplates = SLListOfTacletGoalTemplate.EMPTY_LIST;
0171: ruleSets = SLListOfRuleSet.EMPTY_LIST;
0172: noninteractive = false;
0173: constraint = Constraint.BOTTOM;
0174: choices = SetAsListOfChoice.EMPTY_SET;
0175: prefixMap = MapAsListFromSchemaVariableToTacletPrefix.EMPTY_MAP;
0176: this .displayName = "";
0177: this .oldNames = SLListOfName.EMPTY_LIST;
0178: }
0179:
0180: /**
0181: * creates a Schematic Theory Specific Rule (Taclet) with the given
0182: * parameters.
0183: * @param name the name of the Taclet
0184: * @param applPart contains the application part of an Taclet that is
0185: * the if-sequence, the variable conditions
0186: * @param goalTemplates a list of goal descriptions.
0187: * @param ruleSets a list of rule sets for the Taclet
0188: * @param constraint the Constraint under which the Taclet is valid
0189: * @param attrs attributes for the Taclet; these are boolean values
0190: * indicating a noninteractive or recursive use of the Taclet.
0191: */
0192: Taclet(Name name, TacletApplPart applPart,
0193: ListOfTacletGoalTemplate goalTemplates,
0194: ListOfRuleSet ruleSets, Constraint constraint,
0195: TacletAttributes attrs,
0196: MapFromSchemaVariableToTacletPrefix prefixMap,
0197: SetOfChoice choices) {
0198:
0199: this .name = name;
0200: ifSequent = applPart.ifSequent();
0201: varsNew = applPart.varsNew();
0202: varsNotFreeIn = applPart.varsNotFreeIn();
0203: varsNewDependingOn = applPart.varsNewDependingOn();
0204: variableConditions = applPart.getVariableConditions();
0205: this .goalTemplates = goalTemplates;
0206: this .ruleSets = ruleSets;
0207: noninteractive = attrs.noninteractive();
0208: this .constraint = constraint;
0209: this .choices = choices;
0210: this .prefixMap = prefixMap;
0211: this .displayName = attrs.displayName() == null ? name
0212: .toString() : attrs.displayName();
0213: this .oldNames = attrs.oldNames();
0214:
0215: }
0216:
0217: protected void cacheMatchInfo() {
0218: boundVariables = getBoundVariables();
0219:
0220: final IteratorOfTacletGoalTemplate goalDescriptions = goalTemplates
0221: .iterator();
0222:
0223: while (!hasReplaceWith && goalDescriptions.hasNext()) {
0224: if (goalDescriptions.next().replaceWithExpressionAsObject() != null) {
0225: hasReplaceWith = true;
0226: }
0227: }
0228: }
0229:
0230: /**
0231: * computes and returns all variables that occur bound in the taclet
0232: * including the taclets defined in <tt>addrules</tt> sections. The result
0233: * is cached and therefore only computed once.
0234: * @return all variables occuring bound in the taclet
0235: */
0236: public SetOfQuantifiableVariable getBoundVariables() {
0237: if (boundVariables == null) {
0238: SetOfQuantifiableVariable result = SetAsListOfQuantifiableVariable.EMPTY_SET;
0239: final IteratorOfTacletGoalTemplate it = goalTemplates()
0240: .iterator();
0241:
0242: while (it.hasNext()) {
0243: result = result.union(it.next().getBoundVariables());
0244: }
0245:
0246: final BoundVarsVisitor bvv = new BoundVarsVisitor();
0247: bvv.visit(ifSequent());
0248: result = result.union(bvv.getBoundVariables());
0249:
0250: result = result.union(getBoundVariablesHelper());
0251:
0252: boundVariables = result;
0253: }
0254:
0255: return boundVariables;
0256: }
0257:
0258: /**
0259: * collects bound variables in taclet entities others than goal templates
0260: * @return set of variables that occur bound in taclet entities others
0261: * than goal templates
0262: */
0263: protected abstract SetOfQuantifiableVariable getBoundVariablesHelper();
0264:
0265: /**
0266: * looks if a variable is declared as not free in
0267: * @param var the SchemaVariable to look for
0268: * @return true iff declared not free
0269: */
0270: private boolean varDeclaredNotFree(SchemaVariable var) {
0271: final IteratorOfNotFreeIn it = varsNotFreeIn();
0272: while (it.hasNext()) {
0273: if (it.next().first() == var) {
0274: return true;
0275: }
0276: }
0277: return false;
0278: }
0279:
0280: /**
0281: * returns true iff the taclet contains a "close goal"-statement
0282: * @return true iff the taclet contains a "close goal"-statement
0283: */
0284: public boolean closeGoal() {
0285: return goalTemplates.isEmpty();
0286: }
0287:
0288: /**
0289: * looks if a variable is declared as new and returns its sort to match
0290: * with or the schema variable it shares the match-sort with. Returns
0291: * null if the SV is not declared to as new.
0292: * @param var the SchemaVariable to look for
0293: * @return the sort of the SV to match or the SV it shares the same
0294: * match-sort with
0295: */
0296: public NewVarcond varDeclaredNew(SchemaVariable var) {
0297: final IteratorOfNewVarcond it = varsNew.iterator();
0298: while (it.hasNext()) {
0299: final NewVarcond nv = it.next();
0300: if (nv.getSchemaVariable() == var) {
0301: return nv;
0302: }
0303: }
0304: return null;
0305: }
0306:
0307: /**
0308: * @return the generic variable conditions of this taclet
0309: */
0310: public IteratorOfVariableCondition getVariableConditions() {
0311: return variableConditions.iterator();
0312: }
0313:
0314: /**
0315: * returns true iff the given variable is bound either in the
0316: * ifSequent or in
0317: * any part of the TacletGoalTemplates
0318: * @param v the bound variable to be searched
0319: */
0320: protected boolean varIsBound(SchemaVariable v) {
0321: return (v instanceof QuantifiableVariable) ? getBoundVariables()
0322: .contains((QuantifiableVariable) v)
0323: : false;
0324: }
0325:
0326: /**
0327: * returns a SVInstantiations object iff the given Term
0328: * template can be instantiated to
0329: * match the given Term term using the known instantiations stored in
0330: * svInst. If a
0331: * matching cannot be found null is returned.
0332: * The not free in condition is checked in TacletApp. Collisions are
0333: * resolved there as well, if necessary.
0334: * @param term the Term that has to be matched
0335: * @param template the Term that is checked if it can match term
0336: * @param ignoreUpdates a boolean if set to true updates will be ignored as
0337: * e.g. wanted if an if-sequent is matched
0338: * @param matchCond the SVInstantiations/Constraint that are
0339: * required because of formerly matchings
0340: * @param services the Services object encapsulating information
0341: * about the java datastructures like (static)types etc.
0342: * @param userConstraint current user constraint (which is in some
0343: * situations used to find instantiations)
0344: * @return the new MatchConditions needed to match template with
0345: * term , if possible, null otherwise
0346: */
0347: protected MatchConditions match(Term term, Term template,
0348: boolean ignoreUpdates, MatchConditions matchCond,
0349: Services services, Constraint userConstraint) {
0350: Debug.out("taclet: Start Matching rule: ", name);
0351: matchCond = matchHelp(term, template, ignoreUpdates, matchCond,
0352: services, userConstraint);
0353: return matchCond == null ? null : checkConditions(matchCond,
0354: services);
0355: }
0356:
0357: /**
0358: * same as the method above but with ignoreUpdates always false
0359: * @param term the Term that has to be matched
0360: * @param template the Term that is checked if it can match term
0361: * @param matchCond the SVInstantiations/Constraint that are
0362: * required because of formerly matchings
0363: * @param services the Services object encapsulating information
0364: * about the java datastructures like (static)types etc.
0365: * @param userConstraint current user constraint (which is in some
0366: * situations used to find instantiations)
0367: * @return the new MatchConditions needed to match template with
0368: * term , if possible, null otherwise
0369: */
0370: protected MatchConditions match(Term term, Term template,
0371: MatchConditions matchCond, Services services,
0372: Constraint userConstraint) {
0373: return match(term, template, false, matchCond, services,
0374: userConstraint);
0375: }
0376:
0377: /**
0378: * checks if the conditions for a correct instantiation are satisfied
0379: * @param var the SchemaVariable to be instantiated
0380: * @param instantiationCandidate the SVSubstitute, which is a
0381: * candidate for a possible instantiation of var
0382: * @param matchCond the MatchConditions which have to be respected
0383: * for the new match
0384: * @param services the Services object encapsulating information
0385: * about the Java type model
0386: * @return the match conditions resulting from matching
0387: * <code>var</code> with <code>instantiationCandidate</code> or
0388: * <code>null</code> if a match was not possible
0389: */
0390: public MatchConditions checkVariableConditions(SchemaVariable var,
0391: SVSubstitute instantiationCandidate,
0392: MatchConditions matchCond, Services services) {
0393:
0394: if (instantiationCandidate instanceof Term) {
0395: Term term = (Term) instantiationCandidate;
0396: if (!(term.op() instanceof QuantifiableVariable)) {
0397: if (varIsBound(var) || varDeclaredNotFree(var)) {
0398: // match(x) is not a variable, but the
0399: // corresponding template variable is bound
0400: // or declared non free (so it has to be
0401: // matched to a variable)
0402: return null; // FAILED
0403: }
0404: }
0405: }
0406:
0407: // check generic conditions
0408: for (final IteratorOfVariableCondition it = variableConditions
0409: .iterator(); it.hasNext();) {
0410: final VariableCondition vc = it.next();
0411: matchCond = vc.check(var, instantiationCandidate,
0412: matchCond, services);
0413: if (matchCond == null) {
0414: return null; // FAILED
0415: }
0416: }
0417:
0418: return matchCond;
0419: }
0420:
0421: public MatchConditions checkConditions(MatchConditions cond,
0422: Services services) {
0423: if (cond == null) {
0424: return null;
0425: }
0426: MatchConditions result = cond;
0427: final IteratorOfSchemaVariable svIterator = cond
0428: .getInstantiations().svIterator();
0429: while (svIterator.hasNext()) {
0430: final SchemaVariable sv = svIterator.next();
0431: final Object o = result.getInstantiations()
0432: .getInstantiation(sv);
0433: if (o instanceof SVSubstitute) {
0434: result = checkVariableConditions(sv, (SVSubstitute) o,
0435: result, services);
0436: }
0437: if (result == null) {
0438: Debug
0439: .out(
0440: "FAILED. InstantiationEntry failed condition for ",
0441: sv, o);
0442: return null;
0443: }
0444: }
0445: return result;
0446: }
0447:
0448: private MatchConditions addInstantiation(Term term,
0449: SchemaVariable sv, MatchConditions matchCond,
0450: Services services) {
0451: MatchConditions result = matchCond;
0452: Term t = null;
0453: try {
0454: t = result.getInstantiations()
0455: .getTermInstantiation(
0456: sv,
0457: matchCond.getInstantiations()
0458: .getExecutionContext(), services);
0459: } catch (IllegalInstantiationException e) {
0460: return null;
0461: }
0462: if (t != null) {
0463: Constraint c = result.getConstraint().unify(t, term,
0464: services);
0465: if (!c.isSatisfiable()) {
0466: Debug
0467: .out("FAILED. 13: addInstantiation not satisfiable");
0468: return null; //FAILED;
0469: } else {
0470: return result.setConstraint(c);
0471: }
0472: }
0473:
0474: // no former matching found
0475: result = checkVariableConditions(sv, term, result, services);
0476:
0477: if (result == null) {
0478: Debug.out("FAILED. 13: Var Conds not met");
0479: return null; //FAILED;
0480: }
0481:
0482: try {
0483: return result.setInstantiations(result.getInstantiations()
0484: .add(sv, term));
0485: } catch (IllegalInstantiationException e) {
0486: Debug
0487: .out("Exception thrown by class Taclet at setInstantiations");
0488: }
0489: Debug.out("FAILED. 14: Illegal Instantiation");
0490: return null;
0491: }
0492:
0493: /**
0494: * Add a set of schema variable instantiations to the given match
0495: * conditions object
0496: * @param newInst the instantiations to be added; if the operator
0497: * of any of the instantiations is a metavariable, this variable
0498: * is also added to the set of new metavariable held by
0499: * <code>matchCond</code>
0500: * @return the match conditions after adding the new
0501: * instantiations, or <code>null</code> if any of the new
0502: * instantiations collide with older ones
0503: */
0504: private MatchConditions addNewInstantiations(
0505: MapFromSchemaVariableToTerm newInst,
0506: MatchConditions matchCond, Services services) {
0507: final IteratorOfEntryOfSchemaVariableAndTerm it = newInst
0508: .entryIterator();
0509: while (it.hasNext()) {
0510: final EntryOfSchemaVariableAndTerm entry = it.next();
0511: matchCond = addInstantiation(entry.value(), entry.key(),
0512: matchCond, services);
0513: if (matchCond == null)
0514: return null;
0515: final Operator op = entry.value().op();
0516: if (op instanceof Metavariable) {
0517: final SetOfMetavariable newMVs = matchCond
0518: .getNewMetavariables().add((Metavariable) op);
0519: matchCond = matchCond.setNewMetavariables(newMVs);
0520: }
0521: }
0522: return matchCond;
0523: }
0524:
0525: /**
0526: * tries to match the bound variables of the given term against the one
0527: * described by the template
0528: * @param term the Term whose bound variables are matched against the
0529: * JavaBlock of the template
0530: * (marked as final to help the compiler inlining methods)
0531: * @param template the Term whose bound variables are the template that have
0532: * to be matched
0533: * @param matchCond the MatchConditions that has to be paid respect when
0534: * trying to match
0535: * @return the new matchconditions if a match is possible, otherwise null
0536: */
0537: private final MatchConditions matchBoundVariables(Term term,
0538: Term template, MatchConditions matchCond, Services services) {
0539:
0540: matchCond = matchCond.extendRenameTable();
0541:
0542: for (int j = 0, arity = term.arity(); j < arity; j++) {
0543:
0544: ArrayOfQuantifiableVariable bound = term.varsBoundHere(j);
0545: ArrayOfQuantifiableVariable tplBound = template
0546: .varsBoundHere(j);
0547:
0548: if (bound.size() != tplBound.size()) {
0549: return null; //FAILED
0550: }
0551:
0552: for (int i = 0, boundSize = bound.size(); i < boundSize; i++) {
0553: final QuantifiableVariable templateQVar = tplBound
0554: .getQuantifiableVariable(i);
0555: final QuantifiableVariable qVar = bound
0556: .getQuantifiableVariable(i);
0557: if (templateQVar instanceof LogicVariable) {
0558: final RenameTable rt = matchCond.renameTable();
0559: if (!rt.containsLocally(templateQVar)
0560: && !rt.containsLocally(qVar)) {
0561: matchCond = matchCond.addRenaming(templateQVar,
0562: qVar);
0563: }
0564: }
0565: matchCond = templateQVar.match(qVar, matchCond,
0566: services);
0567:
0568: if (matchCond == null) {
0569: return null;
0570: }
0571: }
0572: }
0573: return matchCond;
0574: }
0575:
0576: /**
0577: * returns the matchconditions that are required if the java block of the
0578: * given term matches the schema given by the template term or null if no
0579: * match is possible
0580: * (marked as final to help the compiler inlining methods)
0581: * @param term the Term whose JavaBlock is matched against the JavaBlock of
0582: * the template
0583: * @param template the Term whose JavaBlock is the template that has to
0584: * be matched
0585: * @param matchCond the MatchConditions that has to be paid respect when
0586: * trying to match the JavaBlocks
0587: * @param services the Services object encapsulating information about the
0588: * program context
0589: * @return the new matchconditions if a match is possible, otherwise null
0590: */
0591: protected final MatchConditions matchJavaBlock(Term term,
0592: Term template, MatchConditions matchCond, Services services) {
0593:
0594: if (term.javaBlock().isEmpty()) {
0595: if (!template.javaBlock().isEmpty()) {
0596: Debug.out("Match Failes. No program to match.");
0597: return null; //FAILED
0598: }
0599: if (template.javaBlock().program() instanceof ContextStatementBlock) {
0600: // we must match empty context blocks too
0601: matchCond = template.javaBlock().program().match(
0602: new SourceData(term.javaBlock().program(), -1,
0603: services), matchCond);
0604: }
0605: } else { //both javablocks != null
0606: matchCond = template.javaBlock().program().match(
0607: new SourceData(term.javaBlock().program(), -1,
0608: services), matchCond);
0609: }
0610: return matchCond;
0611: }
0612:
0613: /** returns a SVInstantiations object with the needed SchemaVariable to Term
0614: * mappings to match the given Term template to the Term term or
0615: * null if no matching is possible.
0616: * (marked as final to help the compiler inlining methods)
0617: * @param term the Term the Template should match
0618: * @param template the Term tried to be instantiated so that it matches term
0619: * @param ignoreUpdates a boolean if set to true updates will be ignored as
0620: * e.g. wanted if an if-sequent is matched
0621: * @param matchCond the MatchConditions to be obeyed by a
0622: * successfull match
0623: * @param userConstraint current user constraint (which is in some
0624: * situations used to find instantiations)
0625: * @return the new MatchConditions needed to match template with
0626: * term, if possible, null otherwise
0627: *
0628: * PRECONDITION: matchCond.getConstraint ().isSatisfiable ()
0629: */
0630:
0631: private MatchConditions matchHelp(final Term term,
0632: final Term template, final boolean ignoreUpdates,
0633: MatchConditions matchCond, final Services services,
0634: final Constraint userConstraint) {
0635: Debug.out("Match: ", template);
0636: Debug.out("With: ", term);
0637:
0638: final Operator sourceOp = term.op();
0639: final Operator templateOp = template.op();
0640:
0641: if (ignoreUpdates
0642: && sourceOp instanceof IUpdateOperator
0643: && (!(templateOp instanceof SchemaVariable) || (templateOp instanceof ModalOperatorSV))
0644: && !(templateOp instanceof IUpdateOperator)) {
0645: // updates can be ignored
0646: matchCond = matchCond.setInstantiations(matchCond
0647: .getInstantiations().addUpdate(term));
0648: return matchHelp(((IUpdateOperator) sourceOp).target(term),
0649: template, true, matchCond, services, userConstraint);
0650: }
0651:
0652: if (templateOp instanceof Metavariable) {
0653: Constraint c = matchCond.getConstraint().unify(term,
0654: template, services);
0655:
0656: if (c.isSatisfiable()) {
0657: return matchCond.setConstraint(c);
0658: }
0659:
0660: Debug.out("FAILED. 3a: constraint unsatisfiable");
0661: return null;
0662: }
0663:
0664: if (!(templateOp instanceof SchemaVariable)
0665: && sourceOp instanceof Metavariable) {
0666: // "term" is a metavariable, "template" neither a
0667: // schemavariable nor a metavariable
0668: return matchMVTerm(term, template, ignoreUpdates,
0669: matchCond, services, userConstraint);
0670: }
0671:
0672: if (templateOp instanceof SortedSchemaVariable) {
0673: return ((SortedSchemaVariable) templateOp).match(term,
0674: matchCond, services);
0675: }
0676:
0677: matchCond = templateOp.match(sourceOp, matchCond, services);
0678:
0679: if (matchCond == null) {
0680: Debug.out("FAILED 3x.");
0681: return null; ///FAILED
0682: }
0683:
0684: //match java blocks:
0685: matchCond = matchJavaBlock(term, template, matchCond, services);
0686: if (matchCond == null) {
0687: Debug.out("FAILED. 9: Java Blocks not matching");
0688: return null; //FAILED
0689: }
0690:
0691: //match bound variables:
0692: matchCond = matchBoundVariables(term, template, matchCond,
0693: services);
0694: if (matchCond == null) {
0695: Debug.out("FAILED. 10: Bound Vars");
0696: return null; //FAILED
0697: }
0698:
0699: for (int i = 0, arity = term.arity(); i < arity; i++) {
0700: matchCond = matchHelp(term.sub(i), template.sub(i), false,
0701: matchCond, services, userConstraint);
0702: if (matchCond == null) {
0703: return null; //FAILED
0704: }
0705: }
0706:
0707: return matchCond.shrinkRenameTable();
0708: }
0709:
0710: /**
0711: * Match a template which is neither a metavariable nor a schema
0712: * variable against a term that is a metavariable
0713: * @param term term whose operator is a metavariable
0714: * @param template template whose operator is neither a
0715: * metavariable nor a schema variable
0716: */
0717: private MatchConditions matchMVTerm(Term term, Term template,
0718: boolean ignoreUpdates, MatchConditions matchCond,
0719: Services services, Constraint userConstraint) {
0720:
0721: // try to instantiate "term" according to the current constraint
0722: final Term t = getInstantiationFor((Metavariable) term.op(),
0723: matchCond.getConstraint());
0724: if (t != null)
0725: return matchHelp(t, template, ignoreUpdates, matchCond,
0726: services, userConstraint);
0727:
0728: return matchMVTermHelp(term, template, ignoreUpdates,
0729: matchCond, services, userConstraint);
0730: }
0731:
0732: /**
0733: * Match a template which is neither a metavariable nor a schema
0734: * variable against a term that is a metavariable; try to use an
0735: * instantiation of the metavariable given by the user constraint
0736: * @param term term whose operator is a metavariable
0737: * @param template template whose operator is neither a
0738: * metavariable nor a schema variable
0739: */
0740: private MatchConditions matchMVTermHelp(Term term, Term template,
0741: boolean ignoreUpdates, MatchConditions matchCond,
0742: Services services, Constraint userConstraint) {
0743: // try to instantiate "term" according to the current user constraint
0744: final Term t = getInstantiationFor((Metavariable) term.op(),
0745: userConstraint);
0746:
0747: if (t == null)
0748: return matchMVTermWithMatchVariables(term, template,
0749: matchCond, services);
0750:
0751: final Constraint c = matchCond.getConstraint().unify(term, t,
0752: services);
0753: if (c.isSatisfiable()) {
0754: MatchConditions mc = matchHelp(t, template, ignoreUpdates,
0755: matchCond.setConstraint(c), services,
0756: userConstraint);
0757: if (mc != null)
0758: return mc;
0759: }
0760:
0761: return matchMVTermWithMatchVariables(term, template, matchCond,
0762: services);
0763: }
0764:
0765: private Term getInstantiationFor(Metavariable p_mv,
0766: Constraint p_constraint) {
0767: if (!(p_constraint instanceof EqualityConstraint))
0768: return null;
0769:
0770: final EqualityConstraint ec = (EqualityConstraint) p_constraint;
0771: return ec.getDirectInstantiation(p_mv);
0772: }
0773:
0774: /**
0775: * Match a template which is neither a metavariable nor a schema
0776: * variable against a term that is a metavariable; try to replace
0777: * schema variables that occur in the template with new metavariables
0778: * @param term term whose operator is a metavariable
0779: * @param template template whose operator is neither a
0780: * metavariable nor a schema variable
0781: */
0782: private MatchConditions matchMVTermWithMatchVariables(Term term,
0783: Term template, MatchConditions matchCond, Services services) {
0784: // try to instantiate uninstantiated SVs by
0785: // creating new metavariables or bound
0786: // logicvariables
0787: SyntacticalReplaceVisitor srVisitor;
0788: try {
0789: srVisitor = new SyntacticalReplaceVisitor(services,
0790: matchCond.getInstantiations(), matchCond
0791: .getConstraint(), true, term.op().name());
0792: template.execPostOrder(srVisitor);
0793: } catch (IllegalInstantiationException e) {
0794: return null; //FAILED;
0795: }
0796:
0797: final MapFromSchemaVariableToTerm newInst = srVisitor
0798: .getNewInstantiations();
0799: if (newInst == null)
0800: return null; //FAILED;
0801:
0802: final MatchConditions mc = addNewInstantiations(newInst,
0803: matchCond, services);
0804:
0805: if (mc == null)
0806: return null; //FAILED;
0807:
0808: return addConstraint(term, srVisitor.getTerm(), mc, services);
0809: }
0810:
0811: /**
0812: * Unify the given terms and add the result to the constraint held
0813: * by <code>matchCond</code>
0814: * @return the new match conditions, or <code>null</code> if the
0815: * terms are not unifiable given the constraint already present
0816: */
0817: private MatchConditions addConstraint(Term term,
0818: Term instantiatedTerm, MatchConditions matchCond,
0819: Services services) {
0820: final Constraint c = matchCond.getConstraint().unify(term,
0821: instantiatedTerm, services);
0822:
0823: return c.isSatisfiable() ? matchCond.setConstraint(c) : null;
0824: }
0825:
0826: /**
0827: * Match the given template (which is probably a formula of the if
0828: * sequence) against a list of constraint formulas (probably the
0829: * formulas of the antecedent or the succedent), starting with the
0830: * given instantiations and constraint p_matchCond.
0831: * @param p_toMatch list of constraint formulas to match p_template to
0832: * @param p_template template formula as in "match"
0833: * @param p_matchCond already performed instantiations
0834: * @param p_services the Services object encapsulating information
0835: * about the java datastructures like (static)types etc.
0836: * @return Two lists (in an IfMatchResult object), containing the
0837: * the elements of p_toMatch that could successfully be matched
0838: * against p_template, and the corresponding MatchConditions.
0839: */
0840: public IfMatchResult matchIf(
0841: IteratorOfIfFormulaInstantiation p_toMatch,
0842: Term p_template, MatchConditions p_matchCond,
0843: Services p_services, Constraint p_userConstraint) {
0844: ListOfIfFormulaInstantiation resFormulas = SLListOfIfFormulaInstantiation.EMPTY_LIST;
0845: ListOfMatchConditions resMC = SLListOfMatchConditions.EMPTY_LIST;
0846:
0847: Term updateFormula;
0848: if (p_matchCond.getInstantiations().getUpdateContext() == SLListOfUpdatePair.EMPTY_LIST)
0849: updateFormula = p_template;
0850: else
0851: updateFormula = TermFactory.DEFAULT.createUpdateTerm(
0852: p_matchCond.getInstantiations().getUpdateContext(),
0853: p_template);
0854:
0855: IfFormulaInstantiation cf;
0856: Constraint newConstraint;
0857: MatchConditions newMC;
0858:
0859: while (p_toMatch.hasNext()) {
0860: cf = p_toMatch.next();
0861:
0862: newConstraint = p_matchCond.getConstraint()
0863: .join(cf.getConstrainedFormula().constraint(),
0864: p_services);
0865:
0866: if (newConstraint.isSatisfiable()) {
0867: newMC = match(cf.getConstrainedFormula().formula(),
0868: updateFormula, false, p_matchCond
0869: .setConstraint(newConstraint),
0870: p_services, p_userConstraint);
0871: if (newMC != null) {
0872: resFormulas = resFormulas.prepend(cf);
0873: resMC = resMC.prepend(newMC);
0874: }
0875: }
0876: }
0877:
0878: return new IfMatchResult(resFormulas, resMC);
0879: }
0880:
0881: /**
0882: * Match the whole if sequent using the given list of
0883: * instantiations of all if sequent formulas, starting with the
0884: * instantiations given by p_matchCond.
0885: * PRECONDITION: p_toMatch.size () == ifSequent ().size ()
0886: * @return resulting MatchConditions or null if the given list
0887: * p_toMatch does not match
0888: */
0889: public MatchConditions matchIf(
0890: IteratorOfIfFormulaInstantiation p_toMatch,
0891: MatchConditions p_matchCond, Services p_services,
0892: Constraint p_userConstraint) {
0893:
0894: IteratorOfConstrainedFormula itIfSequent = ifSequent()
0895: .iterator();
0896:
0897: ListOfMatchConditions newMC;
0898:
0899: while (itIfSequent.hasNext()) {
0900: newMC = matchIf(
0901: (SLListOfIfFormulaInstantiation.EMPTY_LIST
0902: .prepend(p_toMatch.next()).iterator()),
0903: itIfSequent.next().formula(), p_matchCond,
0904: p_services, p_userConstraint).getMatchConditions();
0905:
0906: if (newMC == SLListOfMatchConditions.EMPTY_LIST)
0907: return null;
0908:
0909: p_matchCond = newMC.head();
0910: }
0911:
0912: return p_matchCond;
0913:
0914: }
0915:
0916: /** returns the name of the Taclet
0917: */
0918: public Name name() {
0919: return name;
0920: }
0921:
0922: /** returns the display name of the taclet, or, if not specified --
0923: * the canonical name
0924: */
0925: public String displayName() {
0926: return displayName;
0927: }
0928:
0929: /** returns the list of old names of the taclet
0930: */
0931: public ListOfName oldNames() {
0932: return oldNames;
0933: }
0934:
0935: public String helpText() {
0936: return helpText;
0937: }
0938:
0939: /**
0940: * returns the if-sequence of the application part of the Taclet.
0941: */
0942: public Sequent ifSequent() {
0943: return ifSequent;
0944: }
0945:
0946: /** returns an iterator over the variables that are new in the Taclet.
0947: */
0948: public ListOfNewVarcond varsNew() {
0949: return varsNew;
0950: }
0951:
0952: /** returns an iterator over the variable pairs that indicate that are
0953: * new in the Taclet.
0954: */
0955: public IteratorOfNotFreeIn varsNotFreeIn() {
0956: return varsNotFreeIn.iterator();
0957: }
0958:
0959: public IteratorOfNewDependingOn varsNewDependingOn() {
0960: return varsNewDependingOn.iterator();
0961: }
0962:
0963: /** returns the Constraint under which the Taclet is
0964: * valid */
0965: public Constraint constraint() {
0966: return constraint;
0967: }
0968:
0969: /** returns an iterator over the goal descriptions.
0970: */
0971: public ListOfTacletGoalTemplate goalTemplates() {
0972: return goalTemplates;
0973: }
0974:
0975: public SetOfChoice getChoices() {
0976: return choices;
0977: }
0978:
0979: /** returns an iterator over the rule sets. */
0980: public IteratorOfRuleSet ruleSets() {
0981: return ruleSets.iterator();
0982: }
0983:
0984: public ListOfRuleSet getRuleSets() {
0985: return ruleSets;
0986: }
0987:
0988: /**
0989: * returns true iff the Taclet is to be applied only noninteractive
0990: */
0991: public boolean noninteractive() {
0992: return noninteractive;
0993: }
0994:
0995: public MapFromSchemaVariableToTacletPrefix prefixMap() {
0996: return prefixMap;
0997: }
0998:
0999: /**
1000: * returns true if one of the goal templates is a replacewith. Already
1001: * computed and cached by method cacheMatchInfo
1002: */
1003: public boolean hasReplaceWith() {
1004: return hasReplaceWith;
1005: }
1006:
1007: public SetOfSchemaVariable addedRuleNameVars() {
1008: if (addedRuleNameVars == null) {
1009: int i = 0;
1010: addedRuleNameVars = SetAsListOfSchemaVariable.EMPTY_SET;
1011: IteratorOfTacletGoalTemplate itgt = goalTemplates()
1012: .iterator();
1013: while (itgt.hasNext()) {
1014: TacletGoalTemplate tgt = itgt.next();
1015: IteratorOfTaclet itt = tgt.rules().iterator();
1016: while (itt.hasNext()) {
1017: addedRuleNameVars = addedRuleNameVars
1018: .add(SchemaVariableFactory
1019: .createNameSV(new Name("T" + i++)));
1020: itt.next();
1021: }
1022: }
1023: }
1024: return addedRuleNameVars;
1025: }
1026:
1027: /**
1028: * returns the computed prefix for the given schemavariable. The
1029: * prefix of a schemavariable is used to determine if an
1030: * instantiation is correct, in more detail: it mainly contains all
1031: * variables that can appear free in an instantiation of the
1032: * schemvariable sv (rewrite taclets have some special handling, see
1033: * paper of M. Giese and comment of method isContextInPrefix).
1034: * @param sv the Schemavariable
1035: * @return prefix of schema variable sv
1036: */
1037: public TacletPrefix getPrefix(SchemaVariable sv) {
1038: return prefixMap.get(sv);
1039: }
1040:
1041: /**
1042: * returns true iff a context flag is set in one of the entries in
1043: * the prefix map. Is cached after having been called
1044: * once. __OPTIMIZE__ is caching really necessary here?
1045: *
1046: * @return true iff a context flag is set in one of the entries in
1047: * the prefix map.
1048: */
1049: public boolean isContextInPrefix() {
1050: if (contextInfoComputed) {
1051: return contextIsInPrefix;
1052: }
1053: contextInfoComputed = true;
1054: IteratorOfTacletPrefix it = prefixMap().valueIterator();
1055: while (it.hasNext()) {
1056: if (it.next().context()) {
1057: contextIsInPrefix = true;
1058: return true;
1059: }
1060: }
1061: contextIsInPrefix = false;
1062: return false;
1063: }
1064:
1065: /**
1066: * return true if <code>o</code> is a taclet of the same name and
1067: * <code>o</code> and <code>this</code> contain no mutually exclusive
1068: * taclet options.
1069: */
1070: public boolean equals(Object o) {
1071: if (o == this )
1072: return true;
1073:
1074: if (!(o instanceof Taclet)) {
1075: return false;
1076: }
1077:
1078: final Taclet t2 = (Taclet) o;
1079:
1080: if (!name.equals(t2.name))
1081: return false;
1082:
1083: final IteratorOfChoice it1 = choices.iterator();
1084:
1085: while (it1.hasNext()) {
1086: final Choice c1 = it1.next();
1087: final IteratorOfChoice it2 = t2.getChoices().iterator();
1088: while (it2.hasNext()) {
1089: final Choice c2 = it2.next();
1090: if (c1 != c2 && c1.category().equals(c2.category())) {
1091: return false;
1092: }
1093: }
1094: }
1095:
1096: return true;
1097: }
1098:
1099: public int hashCode() {
1100: if (hashcode == 0) {
1101: hashcode = 37 * name.hashCode() + 17;
1102: if (hashcode == 0) {
1103: hashcode = -1;
1104: }
1105: }
1106: return hashcode;
1107: }
1108:
1109: /**
1110: * a new term is created by replacing variables of term whose replacement is
1111: * found in the given SVInstantiations
1112: * @param term the Term the syntactical replacement is performed on
1113: * @param services the Services
1114: * @param mc the {@link MatchConditions} with all instantiations and
1115: * the constraint
1116: * @return the (partially) instantiated term
1117: */
1118: protected Term syntacticalReplace(Term term, Services services,
1119: MatchConditions mc) {
1120: final SyntacticalReplaceVisitor srVisitor = new SyntacticalReplaceVisitor(
1121: services, mc.getInstantiations(), mc.getConstraint());
1122: term.execPostOrder(srVisitor);
1123:
1124: return srVisitor.getTerm();
1125: }
1126:
1127: /**
1128: * adds ConstrainedFormula to antecedent or succedent depending on
1129: * position information or the boolean antec
1130: * contrary to "addToPos" frm will not be modified
1131: * @param frm the formula that should be added
1132: * @param goal the Goal that knows the node the formulae have to be added
1133: * @param pos the PosInOccurrence describing the place in the sequent
1134: * @param antec boolean true(false) if elements have to be added to the
1135: * antecedent(succedent) (only looked at if pos == null)
1136: */
1137: private void addToPosWithoutInst(ConstrainedFormula frm, Goal goal,
1138: PosInOccurrence pos, boolean antec) {
1139: if (pos != null) {
1140: goal.addFormula(frm, pos);
1141: } else {
1142: // cf : formula to be added , 1. true/false: antec/succ,
1143: // 2. true: at head
1144: goal.addFormula(frm, antec, true);
1145: }
1146: }
1147:
1148: /**
1149: * the given constrained formula is instantiated and then
1150: * the result (usually a complete instantiated formula) is returned.
1151: * @param schemaFormula the ConstrainedFormula to be instantiated
1152: * @param services the Services object carrying ja related information
1153: * @param matchCond the MatchConditions object with the instantiations of
1154: * the schemavariables, constraints etc.
1155: * @return the as far as possible instantiated ConstrainedFormula
1156: */
1157: private ConstrainedFormula instantiateReplacement(
1158: ConstrainedFormula schemaFormula, Services services,
1159: MatchConditions matchCond) {
1160:
1161: final SVInstantiations svInst = matchCond.getInstantiations();
1162:
1163: Term instantiatedFormula = syntacticalReplace(schemaFormula
1164: .formula(), services, matchCond);
1165:
1166: if (!svInst.getUpdateContext().isEmpty()) {
1167: instantiatedFormula = TermFactory.DEFAULT.createUpdateTerm(
1168: svInst.getUpdateContext(), instantiatedFormula);
1169: }
1170:
1171: return new ConstrainedFormula(instantiatedFormula, matchCond
1172: .getConstraint());
1173: }
1174:
1175: /**
1176: * instantiates the given semisequent with the instantiations found in
1177: * Matchconditions
1178: * @param semi the Semisequent to be instantiated
1179: * @param services the Services
1180: * @param matchCond the MatchConditions including the mapping
1181: * Schemavariables to concrete logic elements
1182: * @return the instanted formulas of the semisquent as list
1183: */
1184: private ListOfConstrainedFormula instantiateSemisequent(
1185: Semisequent semi, Services services,
1186: MatchConditions matchCond) {
1187:
1188: ListOfConstrainedFormula replacements = SLListOfConstrainedFormula.EMPTY_LIST;
1189: final IteratorOfConstrainedFormula it = semi.iterator();
1190:
1191: while (it.hasNext()) {
1192: replacements = replacements.append(instantiateReplacement(
1193: it.next(), services, matchCond));
1194: }
1195: return replacements;
1196: }
1197:
1198: /**
1199: * replaces the constrained formula at the given position with the first
1200: * formula in the given semisequent and adds possible other formulas of the
1201: * semisequent starting at the position
1202: * @param semi the Semisequent with the the ConstrainedFormulae to be added
1203: * @param goal the Goal that knows the node the formulae have to be added
1204: * @param pos the PosInOccurrence describing the place in the sequent
1205: * @param antec boolean true(false) if elements have to be added to the
1206: * antecedent(succedent) (only looked at if pos == null)
1207: * @param services the Services encapsulating all java information
1208: * @param matchCond the MatchConditions containing in particular
1209: * the instantiations of the schemavariables
1210: */
1211: protected void replaceAtPos(Semisequent semi, Goal goal,
1212: PosInOccurrence pos, Services services,
1213: MatchConditions matchCond) {
1214: goal.changeFormula(instantiateSemisequent(semi, services,
1215: matchCond), pos);
1216: }
1217:
1218: /**
1219: * instantiates the constrained formulas of semisequent
1220: * <code>semi</code> and adds the instantiatied formulas at the specified
1221: * position to <code>goal</code>
1222: * @param semi the Semisequent with the the ConstrainedFormulae to be added
1223: * @param goal the Goal that knows the node the formulae have to be added
1224: * @param pos the PosInOccurrence describing the place in the sequent
1225: * @param antec boolean true(false) if elements have to be added to the
1226: * antecedent(succedent) (only looked at if pos == null)
1227: * @param services the Services encapsulating all java information
1228: * @param matchCond the MatchConditions containing in particular
1229: * the instantiations of the schemavariables
1230: */
1231: private void addToPos(Semisequent semi, Goal goal,
1232: PosInOccurrence pos, boolean antec, Services services,
1233: MatchConditions matchCond) {
1234: final ListOfConstrainedFormula replacements = instantiateSemisequent(
1235: semi, services, matchCond);
1236:
1237: if (pos != null) {
1238: goal.addFormula(replacements, pos);
1239: } else {
1240: goal.addFormula(replacements, antec, true);
1241: }
1242: }
1243:
1244: /**
1245: * adds ConstrainedFormula to antecedent depending on
1246: * position information (if none is handed over it is added at the
1247: * head of the antecedent). Of course it has to be ensured that
1248: * the position information describes one occurrence in the
1249: * antecedent of the sequent.
1250: * @param semi the Semisequent with the the ConstrainedFormulae to be added
1251: * @param goal the Goal that knows the node the formulae have to be added
1252: * @param pos the PosInOccurrence describing the place in the
1253: * sequent or null for head of antecedent
1254: * @param services the Services encapsulating all java information
1255: * @param matchCond the MatchConditions containing in particular
1256: * the instantiations of the schemavariables
1257: */
1258: protected void addToAntec(Semisequent semi, Goal goal,
1259: PosInOccurrence pos, Services services,
1260: MatchConditions matchCond) {
1261: addToPos(semi, goal, pos, true, services, matchCond);
1262: }
1263:
1264: /**
1265: * adds ConstrainedFormula to succedent depending on
1266: * position information (if none is handed over it is added at the
1267: * head of the succedent). Of course it has to be ensured that
1268: * the position information describes one occurrence in the
1269: * succedent of the sequent.
1270: * @param semi the Semisequent with the the ConstrainedFormulae to be added
1271: * @param goal the Goal that knows the node the formulae have to be added
1272: * @param pos the PosInOccurrence describing the place in the
1273: * sequent or null for head of antecedent
1274: * @param services the Services encapsulating all java information
1275: * @param matchCond the MatchConditions containing in particular
1276: * the instantiations of the schemavariables
1277: */
1278: protected void addToSucc(Semisequent semi, Goal goal,
1279: PosInOccurrence pos, Services services,
1280: MatchConditions matchCond) {
1281: addToPos(semi, goal, pos, false, services, matchCond);
1282: }
1283:
1284: protected abstract Taclet setName(String s);
1285:
1286: protected Taclet setName(String s, TacletBuilder b) {
1287: b.setTacletGoalTemplates(goalTemplates());
1288: b.setRuleSets(getRuleSets());
1289: b.setName(new Name(s));
1290: b.setDisplayName(displayName());
1291: b.setIfSequent(ifSequent());
1292: b.setConstraint(constraint());
1293: b.addVarsNew(varsNew());
1294: b.addVarsNotFreeIn(varsNotFreeIn);
1295: return b.getTaclet();
1296: }
1297:
1298: /**
1299: * adds the given rules (i.e. the rules to add according to the Taclet goal
1300: * template to the node of the given goal
1301: * @param rules the rules to be added
1302: * @param goal the goal describing the node where the rules should be added
1303: * @param services the Services encapsulating all java information
1304: * @param matchCond the MatchConditions containing in particular
1305: * the instantiations of the schemavariables
1306: */
1307: protected void applyAddrule(ListOfTaclet rules, Goal goal,
1308: Services services, MatchConditions matchCond) {
1309:
1310: final IteratorOfTaclet it = rules.iterator();
1311: while (it.hasNext()) {
1312: Taclet tacletToAdd = it.next();
1313: String uniqueTail = ""; // we need to name the new taclet uniquely
1314: /*
1315: TacletGoalTemplate replacewithCandidate = null;
1316: IteratorOfTacletGoalTemplate actions =
1317: tacletToAdd.goalTemplates().iterator();
1318: while (actions.hasNext()) {
1319: replacewithCandidate = actions.next();
1320: if (replacewithCandidate instanceof RewriteTacletGoalTemplate)
1321: break;
1322: }
1323: if ((replacewithCandidate instanceof RewriteTacletGoalTemplate) &&
1324: (tacletToAdd instanceof FindTaclet)) {
1325: // we have _both_ FIND and REPLACEWITH
1326: Term find = ((FindTaclet)tacletToAdd).find();
1327: Term replwith =
1328: ((RewriteTacletGoalTemplate)
1329: replacewithCandidate).replaceWith();
1330:
1331: SyntacticalReplaceVisitor visitor = // now instantiate them!
1332: new SyntacticalReplaceVisitor(services, matchCond.getInstantiations ());
1333: visitor.visit(find);
1334: uniqueTail = "_" + visitor.getTerm();
1335: visitor = new SyntacticalReplaceVisitor(services, matchCond.getInstantiations ());
1336: visitor.visit(replwith);
1337: uniqueTail += "_" + visitor.getTerm();
1338: }
1339: */
1340:
1341: if ("".equals(uniqueTail)) { // otherwise just number it
1342: de.uka.ilkd.key.proof.Node n = goal.node();
1343: uniqueTail = AUTONAME + n.getUniqueTacletNr() + "_"
1344: + n.siblingNr();
1345: }
1346:
1347: tacletToAdd = tacletToAdd.setName(tacletToAdd.name()
1348: + uniqueTail);
1349:
1350: // the new Taclet may contain variables with a known
1351: // instantiation. These must be used by the new Taclet and all
1352: // further rules it contains in the addrules-sections. Therefore all
1353: // appearing (including the addrules) SchemaVariables have to be
1354: // collected, then it is looked if an instantiation is known and if
1355: // positive the instantiation is memorized. At last the Taclet with
1356: // its required instantiations is handed over to the goal, where a
1357: // new TacletApp should be built including the necessary instantiation
1358: // information
1359:
1360: SVInstantiations neededInstances = SVInstantiations.EMPTY_SVINSTANTIATIONS
1361: .addUpdateList(matchCond.getInstantiations()
1362: .getUpdateContext());
1363: final TacletSchemaVariableCollector collector = new TacletSchemaVariableCollector();
1364: collector.visit(tacletToAdd, true);// true, because
1365: // descend into
1366: // addrules
1367: final IteratorOfSchemaVariable svIt = collector
1368: .varIterator();
1369: while (svIt.hasNext()) {
1370: SchemaVariable sv = svIt.next();
1371: if (matchCond.getInstantiations().isInstantiated(sv)) {
1372: neededInstances = neededInstances.add(sv, matchCond
1373: .getInstantiations().getInstantiationEntry(
1374: sv));
1375: }
1376: }
1377:
1378: {
1379: final ListOfGenericSortCondition cs = matchCond
1380: .getInstantiations()
1381: .getGenericSortInstantiations().toConditions();
1382: final IteratorOfGenericSortCondition cit = cs
1383: .iterator();
1384:
1385: while (cit.hasNext())
1386: neededInstances = neededInstances.add(cit.next());
1387: }
1388:
1389: goal.addTaclet(tacletToAdd, neededInstances, matchCond
1390: .getConstraint());
1391: }
1392: }
1393:
1394: protected void applyAddProgVars(SetOfSchemaVariable pvs, Goal goal,
1395: PosInOccurrence posOfFind, Services services,
1396: MatchConditions matchCond) {
1397: final IteratorOfSchemaVariable it = pvs.iterator();
1398: ListOfRenamingTable renamings = SLListOfRenamingTable.EMPTY_LIST;
1399: while (it.hasNext()) {
1400: ProgramVariable inst = (ProgramVariable) matchCond
1401: .getInstantiations().getInstantiation(it.next());
1402: final VariableNamer vn = services.getVariableNamer();
1403: inst = vn.rename(inst, goal, posOfFind);
1404: final RenamingTable rt = RenamingTable.getRenamingTable(vn
1405: .getRenamingMap());
1406: if (rt != null) {
1407: renamings = renamings.append(rt);
1408: }
1409: goal.addProgramVariable(inst);
1410: }
1411: goal.node().setRenamings(renamings);
1412: }
1413:
1414: /** the rule is applied to the given goal using the
1415: * information of rule application.
1416: * @param goal the goal that the rule application should refer to.
1417: * @param services the Services encapsulating all java information
1418: * @param tacletApp the rule application that is executed.
1419: * @return List of the goals created by the rule which have to be
1420: * proved. If this is a close-goal-taclet ( this.closeGoal () ),
1421: * the first goal of the return list is the goal that should be
1422: * closed (with the constraint this taclet is applied under).
1423: */
1424: public abstract ListOfGoal apply(Goal goal, Services services,
1425: RuleApp tacletApp);
1426:
1427: /**
1428: * Search for formulas within p_list that have to be proved by an
1429: * explicit if goal, i.e. elements of type IfFormulaInstDirect.
1430: * @return an array with two goals if such formulas exist (the
1431: * second goal is the if goal), otherwise an array consisting of
1432: * the single element p_goal
1433: */
1434: protected ListOfGoal checkIfGoals(Goal p_goal,
1435: ListOfIfFormulaInstantiation p_list,
1436: MatchConditions p_matchCond, int p_numberOfNewGoals) {
1437: ListOfGoal res = null;
1438: IteratorOfGoal itGoal;
1439:
1440: // proof obligation for the if formulas
1441: Term ifObl = null;
1442:
1443: // always create at least one new goal
1444: if (p_numberOfNewGoals == 0)
1445: p_numberOfNewGoals = 1;
1446:
1447: if (p_list != null) {
1448: IteratorOfIfFormulaInstantiation it = p_list.iterator();
1449: IfFormulaInstantiation inst;
1450: int i = ifSequent().antecedent().size();
1451: Term ifPart;
1452:
1453: while (it.hasNext()) {
1454: inst = it.next();
1455: if (!(inst instanceof IfFormulaInstSeq)) {
1456: // build the if obligation formula
1457: ifPart = inst.getConstrainedFormula().formula();
1458:
1459: // negate formulas of the if succedent
1460: if (i <= 0)
1461: ifPart = TermFactory.DEFAULT.createJunctorTerm(
1462: Op.NOT, ifPart);
1463:
1464: if (res == null) {
1465: res = p_goal.split(p_numberOfNewGoals + 1);
1466: ifObl = ifPart;
1467: } else
1468: ifObl = TermFactory.DEFAULT.createJunctorTerm(
1469: Op.AND, ifObl, ifPart);
1470:
1471: // UGLY: We create a flat structure of the new
1472: // goals, thus the if formulas have to be added to
1473: // every new goal
1474: itGoal = res.iterator();
1475: p_goal = itGoal.next();
1476: while (itGoal.hasNext()) {
1477: addToPosWithoutInst(inst
1478: .getConstrainedFormula(), p_goal, null,
1479: (i > 0)); // ( i > 0 ) iff inst is formula
1480: // of the antecedent
1481: p_goal = itGoal.next();
1482: }
1483: }
1484:
1485: --i;
1486: }
1487: }
1488:
1489: if (res == null)
1490: res = p_goal.split(p_numberOfNewGoals);
1491: else {
1492: // find the sequent the if obligation has to be added to
1493: itGoal = res.iterator();
1494: p_goal = itGoal.next();
1495: while (itGoal.hasNext())
1496: p_goal = itGoal.next();
1497:
1498: addToPosWithoutInst(new ConstrainedFormula(ifObl,
1499: Constraint.BOTTOM), p_goal, null, false);
1500: }
1501:
1502: return res;
1503: }
1504:
1505: /**
1506: * Restrict introduced metavariables to the subtree
1507: */
1508: protected void setRestrictedMetavariables(Goal p_goal,
1509: MatchConditions p_matchCond) {
1510: IteratorOfMetavariable it = p_matchCond.getNewMetavariables()
1511: .iterator();
1512: while (it.hasNext())
1513: p_goal.addRestrictedMetavariable(it.next());
1514: }
1515:
1516: /**
1517: * returns the set of schemavariables of the taclet's if-part
1518: * @return Set of schemavariables of the if part
1519: */
1520: protected SetOfSchemaVariable getIfVariables() {
1521: // should be synchronized
1522: if (ifVariables == null) {
1523: TacletSchemaVariableCollector svc = new TacletSchemaVariableCollector();
1524: svc.visit(ifSequent());
1525:
1526: ifVariables = SetAsListOfSchemaVariable.EMPTY_SET;
1527: IteratorOfSchemaVariable it = svc.varIterator();
1528: while (it.hasNext())
1529: ifVariables = ifVariables.add(it.next());
1530: }
1531:
1532: return ifVariables;
1533: }
1534:
1535: /**
1536: * @return set of schemavariables of the if and the (optional)
1537: * find part
1538: */
1539: public abstract SetOfSchemaVariable getIfFindVariables();
1540:
1541: /**
1542: * Find a schema variable that could be used to choose a name for
1543: * an instantiation (a new variable or constant) of "p"
1544: * @return a schema variable that is substituted by "p" somewhere
1545: * in this taclet (that is, these schema variables occur as
1546: * arguments of a substitution operator)
1547: */
1548: public SchemaVariable getNameCorrespondent(SchemaVariable p) {
1549: // should be synchronized
1550: if (svNameCorrespondences == null) {
1551: final SVNameCorrespondenceCollector c = new SVNameCorrespondenceCollector();
1552: c.visit(this , true);
1553: svNameCorrespondences = c.getCorrespondences();
1554: }
1555:
1556: return svNameCorrespondences.get(p);
1557: }
1558:
1559: StringBuffer toStringIf(StringBuffer sb) {
1560: if (!ifSequent.isEmpty()) {
1561: sb = sb.append("\\assumes (").append(ifSequent)
1562: .append(") ");
1563: sb = sb.append("\n");
1564: }
1565: return sb;
1566: }
1567:
1568: StringBuffer toStringVarCond(StringBuffer sb) {
1569: IteratorOfNewVarcond itVarsNew = varsNew().iterator();
1570: IteratorOfNotFreeIn itVarsNotFreeIn = varsNotFreeIn();
1571: IteratorOfVariableCondition itVC = getVariableConditions();
1572: if (itVarsNew.hasNext() || itVarsNotFreeIn.hasNext()
1573: || itVC.hasNext()) {
1574: sb = sb.append("\\varcond(");
1575: while (itVarsNew.hasNext()) {
1576: sb = sb.append(itVarsNew.next());
1577: if (itVarsNew.hasNext() || itVarsNotFreeIn.hasNext())
1578: sb = sb.append(", ");
1579: }
1580: while (itVarsNotFreeIn.hasNext()) {
1581: NotFreeIn pair = itVarsNotFreeIn.next();
1582: sb = sb.append("\\notFreeIn(").append(pair.first())
1583: .append(", ").append(pair.second()).append(")");
1584: if (itVarsNotFreeIn.hasNext())
1585: sb = sb.append(", ");
1586: }
1587: while (itVC.hasNext()) {
1588: sb.append("" + itVC.next());
1589: if (itVC.hasNext())
1590: sb.append(", ");
1591: }
1592: sb = sb.append(")\n");
1593: }
1594: return sb;
1595: }
1596:
1597: StringBuffer toStringGoalTemplates(StringBuffer sb) {
1598: if (goalTemplates.isEmpty()) {
1599: sb.append("\\closegoal");
1600: } else {
1601: IteratorOfTacletGoalTemplate it = goalTemplates()
1602: .iterator();
1603: while (it.hasNext()) {
1604: sb = sb.append(it.next());
1605: if (it.hasNext())
1606: sb = sb.append(";");
1607: sb = sb.append("\n");
1608: }
1609: }
1610: return sb;
1611: }
1612:
1613: StringBuffer toStringRuleSets(StringBuffer sb) {
1614: IteratorOfRuleSet itRS = ruleSets();
1615: if (itRS.hasNext()) {
1616: sb = sb.append("\\heuristics(");
1617: while (itRS.hasNext()) {
1618: sb = sb.append(itRS.next());
1619: if (itRS.hasNext())
1620: sb = sb.append(", ");
1621: }
1622: sb = sb.append(")");
1623: }
1624: return sb;
1625: }
1626:
1627: StringBuffer toStringAttribs(StringBuffer sb) {
1628: if (noninteractive())
1629: sb = sb.append(" \\noninteractive");
1630: return sb;
1631: }
1632:
1633: /**
1634: * returns a representation of the Taclet as String
1635: * @return string representation
1636: */
1637: public String toString() {
1638: if (tacletAsString == null) {
1639: StringBuffer sb = new StringBuffer();
1640: sb = sb.append(name()).append(" {\n");
1641: sb = toStringIf(sb);
1642: sb = toStringVarCond(sb);
1643: sb = toStringGoalTemplates(sb);
1644: sb = toStringRuleSets(sb);
1645: sb = toStringAttribs(sb);
1646: tacletAsString = sb.append("}").toString();
1647: }
1648: return tacletAsString;
1649: }
1650:
1651: /**
1652: * @return true iff <code>this</code> taclet may be applied for the
1653: * given mode (interactive/non-interactive, activated rule sets)
1654: */
1655: public boolean admissible(boolean interactive,
1656: ListOfRuleSet ruleSets) {
1657: if (interactive)
1658: return admissibleInteractive(ruleSets);
1659: else
1660: return admissibleAutomatic(ruleSets);
1661: }
1662:
1663: protected boolean admissibleInteractive(ListOfRuleSet ruleSets) {
1664: if (noninteractive()) {
1665: final IteratorOfRuleSet tacletRSIt = ruleSets();
1666:
1667: while (tacletRSIt.hasNext()) {
1668: if (ruleSets.contains(tacletRSIt.next()))
1669: return false;
1670: }
1671: }
1672:
1673: return true;
1674: }
1675:
1676: protected boolean admissibleAutomatic(ListOfRuleSet ruleSets) {
1677: final IteratorOfRuleSet tacletRSIt = ruleSets();
1678:
1679: while (tacletRSIt.hasNext()) {
1680: if (ruleSets.contains(tacletRSIt.next()))
1681: return true;
1682: }
1683:
1684: return false;
1685: }
1686:
1687: /** returns the variables in a Taclet with a read access
1688: */
1689: public ListOfSchemaVariable readSet() {
1690: return SLListOfSchemaVariable.EMPTY_LIST;
1691: }
1692:
1693: /** returns the variable in a Taclet to which is written to
1694: */
1695: public ListOfSchemaVariable writeSet() {
1696: return SLListOfSchemaVariable.EMPTY_LIST;
1697: }
1698: }
|