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 java.util.Arrays;
0014: import java.util.HashSet;
0015:
0016: import de.uka.ilkd.key.collection.ListOfString;
0017: import de.uka.ilkd.key.collection.SLListOfString;
0018: import de.uka.ilkd.key.java.ProgramElement;
0019: import de.uka.ilkd.key.java.Services;
0020: import de.uka.ilkd.key.logic.*;
0021: import de.uka.ilkd.key.logic.op.*;
0022: import de.uka.ilkd.key.logic.sort.ProgramSVSort;
0023: import de.uka.ilkd.key.logic.sort.Sort;
0024: import de.uka.ilkd.key.proof.*;
0025: import de.uka.ilkd.key.rule.conditions.NewDepOnAnonUpdates;
0026: import de.uka.ilkd.key.rule.inst.*;
0027: import de.uka.ilkd.key.util.Debug;
0028:
0029: /**
0030: * A TacletApp object contains information required for a concrete application.
0031: * These information may consist of
0032: * <ul>
0033: * <li> instantiations of the schemavariables </li>
0034: * <li> position of the find term </li>
0035: * </ul>
0036: * Its methods <code>complete</code> or <code>sufficientlyComplete</code> are
0037: * used to determine if the information is complete or at least sufficient
0038: * (can be completed using meta variables) complete, so that is can be
0039: * applied.
0040: */
0041: public abstract class TacletApp implements RuleApp {
0042:
0043: /** the taclet for which the application information is collected */
0044: private Taclet taclet;
0045:
0046: /**
0047: * contains the instantiations of the schemavarioables of the
0048: * Taclet
0049: */
0050: protected SVInstantiations instantiations;
0051:
0052: /**
0053: * constraint under which the taclet application can be performed
0054: */
0055: protected Constraint matchConstraint;
0056:
0057: /**
0058: * metavariables that have been created during the matching
0059: */
0060: protected SetOfMetavariable matchNewMetavariables;
0061:
0062: /**
0063: * choosen instantiations for the if sequent formulas
0064: */
0065: ListOfIfFormulaInstantiation ifInstantiations = null;
0066:
0067: /** set of schemavariables that appear in the Taclet and need to be
0068: * instantiated but are not instantiated yet. This means
0069: * SchemaVariables in addrule-sections have to be ignored
0070: */
0071: private SetOfSchemaVariable missingVars = null;
0072:
0073: /** subset of missingVars that cannot be instantiated using
0074: * metavariables
0075: */
0076: private SetOfSchemaVariable neededMissingVars = null;
0077:
0078: /**
0079: * the instantiations of the following SVs must not be changed;
0080: * they must not be instantiated with metavariables either
0081: */
0082: protected SetOfSchemaVariable fixedVars = SetAsListOfSchemaVariable.EMPTY_SET;
0083: /**
0084: * the update context given by the current instantiations must not
0085: * be changed
0086: */
0087: protected boolean updateContextFixed = false;
0088:
0089: /** constructs a TacletApp for the given taclet, with an empty instantiation
0090: * map
0091: */
0092: TacletApp(Taclet taclet) {
0093: this (taclet, SVInstantiations.EMPTY_SVINSTANTIATIONS,
0094: Constraint.BOTTOM, SetAsListOfMetavariable.EMPTY_SET,
0095: null);
0096: }
0097:
0098: TacletApp(Taclet taclet, SVInstantiations instantiations,
0099: Constraint matchConstraint,
0100: SetOfMetavariable matchNewMetavariables,
0101: ListOfIfFormulaInstantiation ifInstantiations) {
0102: this .taclet = taclet;
0103: this .instantiations = instantiations;
0104: this .matchConstraint = matchConstraint;
0105: this .matchNewMetavariables = matchNewMetavariables;
0106: this .ifInstantiations = ifInstantiations;
0107: }
0108:
0109: /** constructs a TacletApp for the given taclet. With some information about
0110: * required instantiations.
0111: */
0112: TacletApp(Taclet taclet, SVInstantiations instantiations) {
0113: this (taclet, instantiations, Constraint.BOTTOM,
0114: SetAsListOfMetavariable.EMPTY_SET, null);
0115: }
0116:
0117: /** collects all bound variables above the occurrence of the schemavariable
0118: * whose prefix is given
0119: * @param prefix the TacletPrefix of the schemavariable
0120: * @param instantiations the SVInstantiations so that the
0121: * find(if)-expression matches
0122: * @return set of the bound variables
0123: */
0124: protected static SetOfQuantifiableVariable boundAtOccurrenceSet(
0125: TacletPrefix prefix, SVInstantiations instantiations) {
0126: return collectPrefixInstantiations(prefix, instantiations);
0127: }
0128:
0129: /** collects all bound variables above the occurrence of the schemavariable
0130: * whose prefix is given
0131: * @param prefix the TacletPrefix of the schemavariable
0132: * @param instantiations the SVInstantiations so that the
0133: * find(if)-expression matches
0134: * @param pos the posInOccurrence describing the position of the
0135: * schemavariable
0136: * @return set of the bound variables
0137: */
0138: protected static SetOfQuantifiableVariable boundAtOccurrenceSet(
0139: TacletPrefix prefix, SVInstantiations instantiations,
0140: PosInOccurrence pos) {
0141:
0142: SetOfQuantifiableVariable result = boundAtOccurrenceSet(prefix,
0143: instantiations);
0144:
0145: if (prefix.context())
0146: result = result.union(collectBoundVarsAbove(pos));
0147:
0148: return result;
0149: }
0150:
0151: /** collects all those logic variable that are instances of the variableSV
0152: * of the given prefix
0153: * @param pre the TacletPrefix of a SchemaVariable that is bound
0154: * @param instantiations the SVInstantiations to look at
0155: * @return the set of the logic variables whose elements are the
0156: * instantiations of a bound SchemaVariable appearing in the TacletPrefix
0157: */
0158: private static SetOfQuantifiableVariable collectPrefixInstantiations(
0159: TacletPrefix pre, SVInstantiations instantiations) {
0160:
0161: SetOfQuantifiableVariable instanceSet = SetAsListOfQuantifiableVariable.EMPTY_SET;
0162: IteratorOfSchemaVariable it = pre.prefix().iterator();
0163: while (it.hasNext()) {
0164: SchemaVariable var = it.next();
0165: instanceSet = instanceSet
0166: .add((LogicVariable) ((Term) instantiations
0167: .getInstantiation(var)).op());
0168: }
0169: return instanceSet;
0170: }
0171:
0172: /** returns the taclet the application information is collected for
0173: * @return the Taclet the application information is collected for
0174: */
0175: public Taclet taclet() {
0176: return taclet;
0177: }
0178:
0179: /** returns the rule the application information is collected for
0180: * @return the Rule the application information is collected for
0181: */
0182: public Rule rule() {
0183: return taclet;
0184: }
0185:
0186: /**
0187: * returns the instantiations for the application of the Taclet at the
0188: * specified position.
0189: * @return the SVInstantiations needed to instantiate the Taclet
0190: */
0191: public SVInstantiations instantiations() {
0192: return instantiations;
0193: }
0194:
0195: public Constraint constraint() {
0196: return matchConstraint;
0197: }
0198:
0199: public SetOfMetavariable newMetavariables() {
0200: return matchNewMetavariables;
0201: }
0202:
0203: public MatchConditions matchConditions() {
0204: return new MatchConditions(instantiations(), constraint(),
0205: newMetavariables(), RenameTable.EMPTY_TABLE);
0206: }
0207:
0208: public ListOfIfFormulaInstantiation ifFormulaInstantiations() {
0209: return ifInstantiations;
0210: }
0211:
0212: /**
0213: * resolves collisions between bound SchemaVariables in an SVInstantiation
0214: *
0215: * @param insts the original SVInstantiations
0216: * @return the resolved SVInstantiations
0217: */
0218: protected static SVInstantiations resolveCollisionVarSV(
0219: Taclet taclet, SVInstantiations insts) {
0220:
0221: HashMapFromLogicVariableToSchemaVariable collMap = new HashMapFromLogicVariableToSchemaVariable();
0222: IteratorOfEntryOfSchemaVariableAndInstantiationEntry it = insts
0223: .pairIterator();
0224: while (it.hasNext()) {
0225: EntryOfSchemaVariableAndInstantiationEntry pair = it.next();
0226: if (pair.key().isVariableSV()) {
0227: SchemaVariable varSV = pair.key();
0228: Term value = ((TermInstantiation) pair.value())
0229: .getTerm();
0230: if (!collMap.containsKey((LogicVariable) value.op())) {
0231: collMap.put((LogicVariable) value.op(), varSV);
0232: } else {
0233: insts = replaceInstantiation(taclet, insts, varSV);
0234: }
0235: }
0236: }
0237: return insts;
0238: }
0239:
0240: /**
0241: * delivers the term below the (unique) quantifier of a bound
0242: * SchemaVariable in the given term.
0243: *
0244: * @param varSV the searched Bound Schemavariable
0245: * @param term the term to be searched in
0246: * @return the term below the given quantifier in the given term
0247: */
0248: private static Term getTermBelowQuantifier(SchemaVariable varSV,
0249: Term term) {
0250: for (int i = 0; i < term.arity(); i++) {
0251: for (int j = 0; j < term.varsBoundHere(i).size(); j++) {
0252: if (term.varsBoundHere(i).getQuantifiableVariable(j) == varSV) {
0253: return term.sub(i);
0254: }
0255: }
0256: Term rec = getTermBelowQuantifier(varSV, term.sub(i));
0257: if (rec != null) {
0258: return rec;
0259: }
0260: }
0261: return null;
0262: }
0263:
0264: /**
0265: * delivers the term below the (unique) quantifier of
0266: * a bound SchemaVariable varSV in the find and if-parts of the Taclet
0267: *
0268: * @param varSV the searched bound SchemaVariable
0269: * @return the term below the given quantifier in the find and if-parts of
0270: * the Taclet
0271: */
0272: private static Term getTermBelowQuantifier(Taclet taclet,
0273: SchemaVariable varSV) {
0274: IteratorOfConstrainedFormula it = taclet.ifSequent().iterator();
0275: while (it.hasNext()) {
0276: Term result = getTermBelowQuantifier(varSV, it.next()
0277: .formula());
0278: if (result != null) {
0279: return result;
0280: }
0281: }
0282:
0283: if (taclet instanceof FindTaclet) {
0284: return getTermBelowQuantifier(varSV, ((FindTaclet) taclet)
0285: .find());
0286: } else
0287: return null;
0288: }
0289:
0290: /** returns true iff the instantiation of a bound SchemaVariable contains the given
0291: * Logicvariable
0292: * @param boundVars ArrayOfQuantifiableVariable with the
0293: * bound SchemaVariables
0294: * @param x the LogicVariable that is looked for
0295: * @param insts the SVInstantiations where to get the necessary
0296: * instantiations of the bound SchemaVariables
0297: * @return true iff the instantiation of a Bound Schemavariable contains the given
0298: * Logicvariable
0299: */
0300: private static boolean contains(
0301: ArrayOfQuantifiableVariable boundVars, LogicVariable x,
0302: SVInstantiations insts) {
0303: for (int i = 0; i < boundVars.size(); i++) {
0304: Term instance = (Term) insts
0305: .getInstantiation((SchemaVariable) boundVars
0306: .getQuantifiableVariable(i));
0307: if (instance.op() == x) {
0308: return true;
0309: }
0310: }
0311:
0312: return false;
0313: }
0314:
0315: /**
0316: * returns a new SVInstantiations that modifies the given
0317: * SVInstantiations insts at the bound SchemaVariable varSV to a new LogicVariable.
0318: */
0319: protected static SVInstantiations replaceInstantiation(
0320: Taclet taclet, SVInstantiations insts, SchemaVariable varSV) {
0321: Term term = getTermBelowQuantifier(taclet, varSV);
0322: LogicVariable newVariable = new LogicVariable(new Name(
0323: ((Term) insts.getInstantiation(varSV)).op().name()
0324: .toString()
0325: + "0"), ((Term) insts.getInstantiation(varSV))
0326: .sort());
0327: // __CHANGE__ How to name the new variable? TODO
0328: Term newVariableTerm = TermFactory.DEFAULT
0329: .createVariableTerm(newVariable);
0330: return replaceInstantiation(insts, term, varSV, newVariableTerm);
0331: }
0332:
0333: /**
0334: * returns a new SVInstantiations that modifies the given
0335: * SVInstantiations insts at the bound SchemaVariable u to the Term (that is
0336: * a LogicVariable) y.
0337: */
0338: private static SVInstantiations replaceInstantiation(
0339: SVInstantiations insts, Term t, SchemaVariable u, Term y) {
0340:
0341: SVInstantiations result = insts;
0342: LogicVariable x = (LogicVariable) ((Term) insts
0343: .getInstantiation(u)).op();
0344: if (t.op() instanceof SchemaVariable) {
0345: if (!((SchemaVariable) t.op()).isVariableSV()) {
0346: SchemaVariable sv = (SchemaVariable) t.op();
0347: ClashFreeSubst cfSubst = new ClashFreeSubst(x, y);
0348: result = result.replace(sv, cfSubst.apply((Term) insts
0349: .getInstantiation(sv)));
0350: }
0351: } else {
0352: for (int i = 0; i < t.arity(); i++) {
0353: if (!contains(t.varsBoundHere(i), x, insts)) {
0354: result = replaceInstantiation(result, t.sub(i), u,
0355: y);
0356: }
0357: }
0358:
0359: }
0360:
0361: result = result.replace(u, y);
0362: return result;
0363: }
0364:
0365: /** applies the specified rule at the specified position
0366: * if all schema variables have been instantiated
0367: * @param goal the Goal at which the Taclet is applied
0368: * @param services the Services encapsulating all java information
0369: * @return list of new created goals
0370: */
0371: public ListOfGoal execute(Goal goal, Services services) {
0372:
0373: if (!complete()) {
0374: throw new IllegalStateException("Tried to apply rule \n"
0375: + taclet + "\nthat is not complete.");
0376: }
0377: goal.addAppliedRuleApp(this );
0378: return taclet().apply(goal, services, this );
0379: }
0380:
0381: /** applies the specified rule at the specified position
0382: * if all schema variables have been instantiated
0383: * and creates a new goal if the if-sequent does not match.
0384: * The new goal proves that the if sequent can be derived.
0385: * @param goal the Goal where to apply the rule
0386: * @param services the Services encapsulating all java information
0387: * @return list of new created goals
0388: */
0389: /*
0390: public ListOfGoal executeForceIf(Goal goal, Services services) {
0391: if (!complete()) {
0392: throw new IllegalStateException("Applied rule not complete.");
0393: }
0394: goal.addAppliedRuleApp(this);
0395: return taclet().apply(goal, services, this, true);
0396: }
0397: */
0398:
0399: /** calculate needed SchemaVariables that have not been
0400: * instantiated yet. This means to ignore SchemaVariables that
0401: * appear only in addrule-sections of Taclets
0402: * @return SetOfSchemaVariable that need to be instantiated but
0403: * are not
0404: */
0405: protected SetOfSchemaVariable calculateNonInstantiatedSV() {
0406: if (missingVars == null) {
0407: missingVars = SetAsListOfSchemaVariable.EMPTY_SET;
0408: TacletSchemaVariableCollector coll = new TacletSchemaVariableCollector(
0409: instantiations());
0410: coll.visitWithoutAddrule(taclet());
0411: IteratorOfSchemaVariable it = coll.varIterator();
0412: while (it.hasNext()) {
0413: SchemaVariable var = it.next();
0414: if (!instantiations().isInstantiated(var)
0415: && !isDependingOnModifiesSV(var)) {
0416: missingVars = missingVars.add(var);
0417: }
0418: }
0419: }
0420: return missingVars;
0421: }
0422:
0423: private NewDepOnAnonUpdates getDependingOnModifies(
0424: SchemaVariable var) {
0425: if (!var.isFormulaSV())
0426: return null;
0427:
0428: NewDepOnAnonUpdates result = null;
0429: final IteratorOfVariableCondition it = taclet
0430: .getVariableConditions();
0431: while (it.hasNext()) {
0432: final VariableCondition vc = it.next();
0433: if (vc instanceof NewDepOnAnonUpdates
0434: && ((NewDepOnAnonUpdates) vc).getUpdateSV() == var) {
0435: assert result == null : "" + vc
0436: + "is a duplicate dependency condition for "
0437: + "schema variable " + var;
0438: result = (NewDepOnAnonUpdates) vc;
0439: }
0440: }
0441:
0442: return result;
0443: }
0444:
0445: /**
0446: * @param sv a schema variable
0447: * @return true iff sv there is a variable condition of the form
0448: * \newDepOnMod(modifies,sv)
0449: */
0450: public boolean isDependingOnModifiesSV(SchemaVariable sv) {
0451: return getDependingOnModifies(sv) != null;
0452: }
0453:
0454: /** Calculate needed SchemaVariables that have not been
0455: * instantiated yet and cannot be instantiated using
0456: * metavariables. This is a subset of
0457: * calculateNonInstantiatedSV();
0458: * @return SetOfSchemaVariable that need to be instantiated but
0459: * are not
0460: */
0461: protected SetOfSchemaVariable calculateNeededNonInstantiatedSV() {
0462: if (neededMissingVars == null) {
0463: IteratorOfSchemaVariable it = calculateNonInstantiatedSV()
0464: .iterator();
0465: SchemaVariable var;
0466: SVInstantiations svi = instantiations();
0467:
0468: neededMissingVars = SetAsListOfSchemaVariable.EMPTY_SET;
0469:
0470: while (it.hasNext()) {
0471: var = it.next();
0472: if (isDependingOnModifiesSV(var))
0473: continue;
0474: if (canUseMVAPriori(var)) {
0475: GenericSortCondition c = GenericSortCondition
0476: .forceInstantiation(
0477: ((SortedSchemaVariable) var).sort(),
0478: true);
0479: if (c == null)
0480: continue; // then the sort is not generic
0481: else {
0482: try {
0483: svi = svi.add(c);
0484: continue; // then the sort can be guessed
0485: } catch (GenericSortException e) {
0486: Debug
0487: .out("Exception thrown by class TacletApp "
0488: + "at svi.add()");
0489: }
0490: }
0491: }
0492:
0493: neededMissingVars = neededMissingVars.add(var);
0494: }
0495: }
0496: return neededMissingVars;
0497: }
0498:
0499: /** creates a new Tacletapp where the SchemaVariable sv is
0500: * instantiated with the the given Term term. Sort equality is
0501: * checked. If the check fails an IllegalArgumentException is
0502: * thrown
0503: * @param sv the SchemaVariable to be instantiated
0504: * @param term the Term the SchemaVariable is instantiated with
0505: * @return the new TacletApp
0506: */
0507: public TacletApp addCheckedInstantiation(SchemaVariable sv,
0508: Term term, Services services, boolean interesting) {
0509:
0510: if (sv.isVariableSV() && !(term.op() instanceof LogicVariable)) {
0511: throw new IllegalInstantiationException("Could not add "
0512: + "the instantiation of " + sv + " because " + term
0513: + " is no variable.");
0514: }
0515:
0516: MatchConditions cond = matchConditions();
0517:
0518: if (sv instanceof SortedSchemaVariable) {
0519: cond = ((SortedSchemaVariable) sv).match(term, cond,
0520: services);
0521: } else {
0522: cond = sv.match(term.op(), cond, services);
0523: }
0524:
0525: if (cond == null) {
0526: throw new IllegalInstantiationException("Instantiation "
0527: + term + " is not matched by " + sv);
0528: }
0529:
0530: cond = taclet().checkVariableConditions(sv, term, cond,
0531: services);
0532:
0533: if (cond == null) {
0534: throw new IllegalInstantiationException("Instantiation "
0535: + term + " of " + sv
0536: + "does not satisfy the variable conditions");
0537: }
0538:
0539: if (interesting) {
0540: cond = cond.setInstantiations(cond.getInstantiations()
0541: .makeInteresting(sv));
0542: }
0543:
0544: return addInstantiation(cond.getInstantiations());
0545:
0546: }
0547:
0548: /**
0549: * returns the variables that have not yet been instantiated and
0550: * need to be instantiated to apply the Taclet. (These are not all
0551: * SchemaVariables like the one that appear only in the addrule
0552: * sections)
0553: * @return SetOfSchemaVariable with SchemaVariables that have not
0554: * been instantiated yet
0555: */
0556: public SetOfSchemaVariable uninstantiatedVars() {
0557: return calculateNonInstantiatedSV();
0558: }
0559:
0560: /**
0561: * returns the variables that are currently uninstantiated and
0562: * cannot be instantiated automatically using metavariables
0563: * @return SetOfSchemaVariable with SchemaVariables that have not
0564: * been instantiated yet
0565: */
0566: public SetOfSchemaVariable neededUninstantiatedVars() {
0567: return calculateNeededNonInstantiatedSV();
0568: }
0569:
0570: /**
0571: * @return A TacletApp with this.sufficientlyComplete() or null
0572: */
0573: public TacletApp tryToInstantiate(Goal goal, Services services) {
0574: final VariableNamer varNamer = services.getVariableNamer();
0575: final TermBuilder tb = TermBuilder.DF;
0576:
0577: TacletApp app = this ;
0578: ListOfString proposals = SLListOfString.EMPTY_LIST;
0579:
0580: final IteratorOfSchemaVariable it = uninstantiatedVars()
0581: .iterator();
0582: while (it.hasNext()) {
0583: SchemaVariable var = it.next();
0584:
0585: if (LoopInvariantProposer.inLoopInvariantRuleSet(taclet()
0586: .ruleSets())) {
0587: Object inv = LoopInvariantProposer.DEFAULT
0588: .tryToInstantiate(this , var, services);
0589: if (inv instanceof Term) {
0590: app = app.addCheckedInstantiation(var, (Term) inv,
0591: services, true);
0592: } else if (inv instanceof ListOfTerm) {
0593: app = app.addInstantiation(var, ((ListOfTerm) inv)
0594: .toArray(), true);
0595: } else if (inv instanceof SetOfLocationDescriptor) {
0596: app = app.addInstantiation(var,
0597: ((SetOfLocationDescriptor) inv).toArray(),
0598: true);
0599: }
0600: if (inv != null)
0601: continue;
0602: }
0603: if (var instanceof SortedSchemaVariable) {
0604: SortedSchemaVariable sv = (SortedSchemaVariable) var;
0605: if (sv.sort() == ProgramSVSort.VARIABLE) {
0606: String proposal = varNamer
0607: .getSuggestiveNameProposalForProgramVariable(
0608: sv, this , goal, services, proposals);
0609: ProgramElement pe = TacletInstantiationsTableModel
0610: .getProgramElement(app, proposal, sv,
0611: services);
0612: app = app.addCheckedInstantiation(sv, pe, services,
0613: true);
0614: proposals = proposals.append(proposal);
0615: } else if (sv.sort() == ProgramSVSort.LABEL) {
0616: boolean nameclash;
0617: do {
0618: String proposal = VariableNameProposer.DEFAULT
0619: .getProposal(this , sv, services, goal
0620: .node(), proposals);
0621: ProgramElement pe = TacletInstantiationsTableModel
0622: .getProgramElement(app, proposal, sv,
0623: services);
0624: proposals = proposals.prepend(proposal);
0625: try {
0626: app = app.addCheckedInstantiation(sv, pe,
0627: services, true);
0628: } catch (IllegalInstantiationException iie) {
0629: // name clash
0630: nameclash = true;
0631: }
0632: nameclash = false;
0633: } while (nameclash);
0634: } else if (sv.isSkolemTermSV()) {
0635: // if the sort of the schema variable is generic,
0636: // ensure that it is instantiated
0637: app = forceGenericSortInstantiation(app, sv);
0638: if (app == null)
0639: return null;
0640:
0641: String proposal = VariableNameProposer.DEFAULT
0642: .getProposal(app, sv, services,
0643: goal.node(), proposals);
0644:
0645: proposals = proposals.append(proposal);
0646:
0647: app = app.createSkolemConstant(proposal, sv, true,
0648: services);
0649:
0650: } else if (sv.isVariableSV()) {
0651: // if the sort of the schema variable is generic,
0652: // ensure that it is instantiated
0653: app = forceGenericSortInstantiation(app, sv);
0654: if (app == null)
0655: return null;
0656:
0657: String proposal = VariableNameProposer.DEFAULT
0658: .getProposal(this , sv, services, goal
0659: .node(), null);
0660: final LogicVariable v = new LogicVariable(new Name(
0661: proposal), getRealSort(sv, services));
0662: app = app.addCheckedInstantiation(sv, tb.var(v),
0663: services, true);
0664: } else if (!(sv.isTermSV() && canUseMVAPriori(sv))) {
0665: return null;
0666: }
0667: }
0668: }
0669:
0670: if (app != this ) {
0671: final MatchConditions appMC = app.taclet().checkConditions(
0672: app.matchConditions(), services);
0673: if (appMC == null) {
0674: return null;
0675: } else {
0676: app = app.setMatchConditions(appMC);
0677: }
0678: }
0679:
0680: if (!app.sufficientlyComplete()) {
0681: return null;
0682: }
0683: return app;
0684: }
0685:
0686: /**
0687: * If the sort of the given schema variable is generic, add a
0688: * condition to the instantiations of the given taclet app that
0689: * requires the sort to be instantiated
0690: * @return the new taclet app, or <code>null</code> if the sort of
0691: * <code>sv</code> is generic and cannot be instantiated (at least
0692: * at the time)
0693: */
0694: private static TacletApp forceGenericSortInstantiation(
0695: TacletApp app, SortedSchemaVariable sv) {
0696: final GenericSortCondition c = GenericSortCondition
0697: .forceInstantiation(sv.sort(), false);
0698: if (c != null) {
0699: try {
0700: app = app.setInstantiation(app.instantiations().add(c));
0701: } catch (GenericSortException e) {
0702: return null;
0703: }
0704: }
0705: return app;
0706: }
0707:
0708: /**
0709: * Examine all schema variables of the taclet that are currently
0710: * not instantiated, and for each one whose sort is generic add a
0711: * condition to the instantiations object <code>insts</code> that
0712: * requires this sort to be instantiated
0713: * @return the instantiations object after adding all the
0714: * conditions, or <code>null</code> if any of the generic sorts
0715: * found cannot be instantiated (at least at the time)
0716: */
0717: private SVInstantiations forceGenericSortInstantiations(
0718: SVInstantiations insts) {
0719: final IteratorOfSchemaVariable it = uninstantiatedVars()
0720: .iterator();
0721:
0722: // force all generic sorts to be instantiated
0723: try {
0724: while (it.hasNext()) {
0725: final SchemaVariable sv = it.next();
0726: final GenericSortCondition c = GenericSortCondition
0727: .forceInstantiation(((SortedSchemaVariable) sv)
0728: .sort(), true);
0729: if (c != null)
0730: insts = insts.add(c);
0731: }
0732: } catch (GenericSortException e) {
0733: Debug.fail("TacletApp cannot be made complete");
0734: }
0735: return insts;
0736: }
0737:
0738: /**
0739: * Make the instantiation complete using metavariables and convert plain
0740: * instantiations to metavariables and user constraint entries if possible.
0741: * Pre-condition: this.sufficientlyComplete()
0742: */
0743: public TacletApp instantiateWithMV(Goal p_goal) {
0744:
0745: Debug.assertTrue(this .sufficientlyComplete(),
0746: "TacletApp cannot be made complete");
0747:
0748: final Proof proof = p_goal.proof();
0749:
0750: Services services = proof.getServices();
0751:
0752: SVInstantiations insts = instantiations();
0753: SetOfMetavariable newVars = newMetavariables();
0754: Constraint constr = constraint();
0755:
0756: if (newVars != SetAsListOfMetavariable.EMPTY_SET) {
0757: // Replace temporary metavariables that were introduced
0758: // when matching the taclet with real MVs
0759: final IteratorOfMetavariable mvIt = newVars.iterator();
0760: newVars = SetAsListOfMetavariable.EMPTY_SET;
0761: SetOfMetavariable removeVars = SetAsListOfMetavariable.EMPTY_SET;
0762: Constraint replaceC = Constraint.BOTTOM;
0763: while (mvIt.hasNext()) {
0764: final Metavariable mv = mvIt.next();
0765: if (mv.isTemporaryVariable()) {
0766: String s = "" + mv.name();
0767: s += "_"
0768: + MetavariableDeliverer.mv_Counter(s,
0769: p_goal);
0770: final Metavariable newMV = proof
0771: .getMetavariableDeliverer()
0772: .createNewVariable(s, mv.sort());
0773: newVars = newVars.add(newMV);
0774: removeVars = removeVars.add(mv);
0775: final Term newT = TermFactory.DEFAULT
0776: .createFunctionTerm(newMV);
0777: final Term t = TermFactory.DEFAULT
0778: .createFunctionTerm(mv);
0779: replaceC = replaceC.unify(t, newT, services);
0780: } else
0781: newVars = newVars.add(mv);
0782: }
0783:
0784: if (!replaceC.isBottom()) {
0785: constr = removeTemporaryMVsFromConstraint(constr,
0786: removeVars, replaceC, services);
0787: insts = removeTemporaryMVsFromInstantiations(insts,
0788: replaceC);
0789: }
0790: }
0791:
0792: // Replace plain instantiations of termSV
0793:
0794: final IteratorOfEntryOfSchemaVariableAndInstantiationEntry it = insts
0795: .pairIterator();
0796:
0797: while (it.hasNext()) {
0798: final EntryOfSchemaVariableAndInstantiationEntry entry = it
0799: .next();
0800: final SchemaVariable sv = entry.key();
0801:
0802: if (introduceMVFor(entry, sv)) {
0803: final Metavariable mv = getMVFor(sv, proof, p_goal,
0804: insts);
0805: newVars = newVars.add(mv);
0806: final Term t = TermFactory.DEFAULT
0807: .createFunctionTerm(mv);
0808: proof.getUserConstraint().addEquality(t,
0809: ((TermInstantiation) entry.value()).getTerm());
0810: insts = insts.replace(sv, t);
0811: }
0812: }
0813:
0814: return handleUninstantiatedSVs(proof, p_goal, insts, constr,
0815: newVars);
0816: }
0817:
0818: /**
0819: * Replace temporary metavariables (that were introduced when
0820: * matching the taclet parts) within <code>insts</code> with
0821: * definite metavariables
0822: * @param replaceC a constraint that unifies each temporary
0823: * metavariable with the corresponding definite metavariable
0824: */
0825: private static SVInstantiations removeTemporaryMVsFromInstantiations(
0826: SVInstantiations insts, Constraint replaceC) {
0827: final IteratorOfEntryOfSchemaVariableAndInstantiationEntry it = insts
0828: .pairIterator();
0829:
0830: while (it.hasNext()) {
0831: final EntryOfSchemaVariableAndInstantiationEntry entry = it
0832: .next();
0833: final SchemaVariable sv = entry.key();
0834:
0835: if (sv.isFormulaSV() || sv.isTermSV()) {
0836: final Object inst = entry.value().getInstantiation();
0837: // NB: this only works because of the implementation of
0838: // <code>Metavariable.compareTo</code>, in which temporary MVs
0839: // are regarded as greater than normal MVs
0840: final SyntacticalReplaceVisitor srVisitor = new SyntacticalReplaceVisitor(
0841: replaceC);
0842: ((Term) inst).execPostOrder(srVisitor);
0843: insts = insts.replace(sv, srVisitor.getTerm());
0844: }
0845: }
0846: return insts;
0847: }
0848:
0849: /**
0850: * Replace temporary metavariables (that were introduced when
0851: * matching the taclet parts) within <code>constr</code> with
0852: * definite metavariables
0853: * @param removeVars the set of temporary metavariables to be
0854: * removed
0855: * @param replaceC a constraint that unifies each temporary
0856: * metavariable with the corresponding definite metavariable
0857: * @param services the Services
0858: */
0859: private static Constraint removeTemporaryMVsFromConstraint(
0860: Constraint constr, SetOfMetavariable removeVars,
0861: Constraint replaceC, Services services) {
0862: // that's tricky ...
0863: constr = constr.join(replaceC, services);
0864: return constr.removeVariables(removeVars);
0865: }
0866:
0867: /**
0868: * @return true iff it is possible to use a metavariable to make
0869: * the given instantiation indirect, i.e. to instantiate the
0870: * schema variable with a metavariable instead of a term, and to
0871: * add the real instantiation to the user constraint
0872: */
0873: private boolean introduceMVFor(
0874: EntryOfSchemaVariableAndInstantiationEntry entry,
0875: SchemaVariable sv) {
0876: return sv.isTermSV()
0877: && !sv.isListSV()
0878: && !taclet().getIfFindVariables().contains(sv)
0879: && canUseMVAPosteriori(sv, ((TermInstantiation) entry
0880: .value()).getTerm());
0881: }
0882:
0883: /**
0884: * Instantiate all uninstantiated schema variables with
0885: * metavariables; it is assumed that this is possible (currently
0886: * checked using an assertion)
0887: * @return a new taclet app in which all schema variables are
0888: * instantiated
0889: */
0890: private TacletApp handleUninstantiatedSVs(Proof proof, Goal goal,
0891: SVInstantiations insts, Constraint constr,
0892: SetOfMetavariable newVars) {
0893: insts = forceGenericSortInstantiations(insts);
0894:
0895: final IteratorOfSchemaVariable it = uninstantiatedVars()
0896: .iterator();
0897: while (it.hasNext()) {
0898: final SchemaVariable sv = it.next();
0899: if (isDependingOnModifiesSV(sv))
0900: continue;
0901: Debug.assertTrue(canUseMVAPriori(sv),
0902: "Should be able to instantiate " + sv
0903: + " using metavariables, but am not");
0904:
0905: final Metavariable mv = getMVFor(sv, proof, goal, insts);
0906: newVars = newVars.add(mv);
0907: final Term t = TermFactory.DEFAULT.createFunctionTerm(mv);
0908: insts = insts.add(sv, t);
0909: NameSV nameSV = new NameSV(new Name(NameSV.MV_NAME_PREFIX
0910: + sv.name()));
0911: insts = insts.addInteresting(nameSV, mv.name());
0912: }
0913:
0914: return setMatchConditions(new MatchConditions(insts, constr,
0915: newVars, RenameTable.EMPTY_TABLE));
0916: }
0917:
0918: /**
0919: * Create a Metavariable the given SchemaVariable can be
0920: * instantiated with
0921: * @return an appropriate mv, or null if for some reason the
0922: * creation failed
0923: */
0924: private Metavariable getMVFor(SchemaVariable sv, Proof proof,
0925: Goal goal, SVInstantiations insts) {
0926: final Sort realSort = insts.getGenericSortInstantiations()
0927: .getRealSort(sv, proof.getServices());
0928: SchemaVariable nameSV = insts.lookupVar(new Name(
0929: NameSV.MV_NAME_PREFIX + sv.name()));
0930: Name proposal = (Name) insts.getInstantiation(nameSV);
0931: String s = (proposal == null) ? "" : proposal.toString();
0932: return getMVFor(sv, realSort, proof, goal, s);
0933: }
0934:
0935: /**
0936: * Create a Metavariable the given SchemaVariable can be
0937: * instantiated with
0938: * @return an appropriate mv, or null if for some reason the
0939: * creation failed
0940: */
0941: private Metavariable getMVFor(SchemaVariable p_sv, Sort p_sort,
0942: Proof p_proof, Goal goal, String nameProposal) {
0943: if ("".equals(nameProposal)) {
0944: nameProposal = TacletInstantiationsTableModel
0945: .getNameProposalForMetavariable(goal, this , p_sv);
0946: }
0947: return p_proof.getMetavariableDeliverer().createNewVariable(
0948: nameProposal, p_sort);
0949: }
0950:
0951: /**
0952: * @param services the Services class allowing access to the type model
0953: * @return p_s iff p_s is not a generic sort, the concrete sort
0954: * p_s is instantiated with currently otherwise
0955: * @throws GenericSortException iff p_s is a generic sort which is
0956: * not yet instantiated
0957: */
0958: public Sort getRealSort(SchemaVariable p_sv, Services services) {
0959: return instantiations().getGenericSortInstantiations()
0960: .getRealSort(p_sv, services);
0961: }
0962:
0963: /**
0964: * Create a new constant named "instantiation" and instantiate
0965: * "sv" with. This constant will later (by
0966: * "createSkolemFunctions") be replaced by a function having
0967: * the occurring metavariables as arguments
0968: * @param services the Services class allowing access to the type model
0969: */
0970: public TacletApp createSkolemConstant(String instantiation,
0971: SchemaVariable sv, boolean interesting, Services services) {
0972: return createSkolemConstant(instantiation, sv, getRealSort(sv,
0973: services), interesting);
0974: }
0975:
0976: public TacletApp createSkolemConstant(String instantiation,
0977: SchemaVariable sv, Sort sort, boolean interesting) {
0978: Function c = new RigidFunction(new Name(instantiation), sort,
0979: new Sort[0]);
0980: return addInstantiation(sv, TermFactory.DEFAULT
0981: .createFunctionTerm(c), interesting);
0982: }
0983:
0984: /**
0985: * Create skolem functions (for variables declared via "\\new(c,
0986: * \\dependingOn(phi))" or via "\\new(upd, \\dependingOnMod(#modifiers))")
0987: * to replace previously created constants with
0988: */
0989: public TacletApp createSkolemFunctions(Namespace p_func_ns,
0990: Services services) {
0991: SVInstantiations insts = instantiations();
0992:
0993: final IteratorOfSchemaVariable svIt = insts.svIterator();
0994: while (svIt.hasNext())
0995: insts = createTermSkolemFunctions(svIt.next(), insts,
0996: p_func_ns);
0997:
0998: final IteratorOfVariableCondition vcIt = taclet
0999: .getVariableConditions();
1000: while (vcIt.hasNext()) {
1001: final VariableCondition vc = vcIt.next();
1002: if (vc instanceof NewDepOnAnonUpdates)
1003: insts = createModifiesSkolemFunctions(
1004: (NewDepOnAnonUpdates) vc, insts, services);
1005: }
1006:
1007: if (insts == instantiations())
1008: return this ;
1009: return setInstantiation(insts);
1010: }
1011:
1012: /**
1013: * Instantiate a SkolemTermSV
1014: */
1015: private SVInstantiations createTermSkolemFunctions(
1016: SchemaVariable depSV, SVInstantiations insts,
1017: Namespace p_func_ns) {
1018: if (!depSV.isSkolemTermSV())
1019: return insts;
1020:
1021: final Term tempDepVar = (Term) insts.getInstantiation(depSV);
1022:
1023: Debug.assertTrue(tempDepVar != null,
1024: "Name for skolemterm variable missing");
1025:
1026: return createSkolemFunction(insts, p_func_ns, depSV,
1027: tempDepVar, determineArgMVs(insts, depSV));
1028: }
1029:
1030: /**
1031: * Instantiate a schemavariable for an anonymous update (FormulaSV)
1032: */
1033: private SVInstantiations createModifiesSkolemFunctions(
1034: NewDepOnAnonUpdates cond, SVInstantiations insts,
1035: Services services) {
1036: final SchemaVariable modifies = cond.getModifiesSV();
1037: final SchemaVariable updateSV = cond.getUpdateSV();
1038:
1039: if (insts.isInstantiated(updateSV)) {
1040: System.err
1041: .println("Modifies skolem functions already created - ignoring.");
1042: return insts;
1043: }
1044:
1045: final ListOfObject locationList = (ListOfObject) insts
1046: .getInstantiation(modifies);
1047: final AnonymisingUpdateFactory auf = new AnonymisingUpdateFactory(
1048: new UpdateFactory(services, new UpdateSimplifier()));
1049: final Term[] mvArgs = toTermArray(determineArgMVs(insts,
1050: updateSV));
1051: return insts.add(updateSV, auf.createAnonymisingUpdateAsFor(
1052: toLocationDescriptorArray(locationList), mvArgs,
1053: services));
1054: }
1055:
1056: private static LocationDescriptor[] toLocationDescriptorArray(
1057: ListOfObject locationList) {
1058: final LocationDescriptor[] locations = new LocationDescriptor[locationList
1059: .size()];
1060:
1061: for (int i = 0; i < locations.length; i++) {
1062: locations[i] = (LocationDescriptor) locationList.head();
1063: locationList = locationList.tail();
1064: }
1065: return locations;
1066: }
1067:
1068: /**
1069: * Determine the metavariables that have to be added as arguments to newly
1070: * created skolem symbols (as basis of the occurs check)
1071: */
1072: private SetOfMetavariable determineArgMVs(SVInstantiations insts,
1073: SchemaVariable depSV) {
1074: return determineExplicitArgMVs(insts, depSV).union(
1075: determineArgMVsFromUpdate(insts));
1076: }
1077:
1078: private SetOfMetavariable determineExplicitArgMVs(
1079: SVInstantiations insts, SchemaVariable depSV) {
1080: final IteratorOfNewDependingOn it = taclet()
1081: .varsNewDependingOn();
1082: SetOfMetavariable mvs = SetAsListOfMetavariable.EMPTY_SET;
1083: while (it.hasNext()) {
1084: final NewDependingOn newDepOn = it.next();
1085: if (depSV != newDepOn.first())
1086: continue;
1087:
1088: final Term dominantTerm = (Term) insts
1089: .getInstantiation(newDepOn.second());
1090:
1091: assert dominantTerm != null : "Variable depends on uninstantiated variable";
1092: mvs = mvs.union(dominantTerm.metaVars());
1093: }
1094: return mvs;
1095: }
1096:
1097: private SetOfMetavariable determineArgMVsFromUpdate(
1098: SVInstantiations insts) {
1099: final IteratorOfUpdatePair it = insts.getUpdateContext()
1100: .iterator();
1101: SetOfMetavariable mvs = SetAsListOfMetavariable.EMPTY_SET;
1102: while (it.hasNext()) {
1103: final UpdatePair pair = it.next();
1104: final IUpdateOperator upOp = pair.updateOperator();
1105: for (int i = 0; i != upOp.arity(); ++i) {
1106: if (i == upOp.targetPos())
1107: continue;
1108: mvs = mvs.union(pair.sub(i).metaVars());
1109: }
1110: }
1111: return mvs;
1112: }
1113:
1114: private SVInstantiations createSkolemFunction(
1115: SVInstantiations insts, Namespace p_func_ns,
1116: SchemaVariable depSV, Term tempDepVar, SetOfMetavariable mvs) {
1117: if (mvs == SetAsListOfMetavariable.EMPTY_SET) {
1118: // if the term contains no metavariables, we just use the
1119: // (nullary) constant <code>tempDepVar</code> as skolem symbol
1120: p_func_ns.add(tempDepVar.op());
1121: return insts;
1122: }
1123:
1124: final Term[] argTerms = toTermArray(mvs);
1125: final Function skolemFunc = new RigidFunction(tempDepVar.op()
1126: .name(), tempDepVar.sort(), extractSorts(argTerms));
1127: final Term skolemTerm = TermFactory.DEFAULT.createFunctionTerm(
1128: skolemFunc, argTerms);
1129:
1130: p_func_ns.add(skolemFunc);
1131: return insts.replace(depSV, skolemTerm);
1132: }
1133:
1134: private Term[] toTermArray(SetOfMetavariable mvs) {
1135: final Metavariable[] mvArray = mvs.toArray();
1136: Arrays.sort(mvArray);
1137:
1138: // Create function with correct arguments
1139: final Term[] argTerms = new Term[mvArray.length];
1140:
1141: for (int i = 0; i != mvArray.length; ++i)
1142: argTerms[i] = TermFactory.DEFAULT
1143: .createFunctionTerm(mvArray[i]);
1144:
1145: return argTerms;
1146: }
1147:
1148: private Sort[] extractSorts(Term[] argTerms) {
1149: final Sort[] argSorts = new Sort[argTerms.length];
1150: for (int i = 0; i != argTerms.length; ++i)
1151: argSorts[i] = argTerms[i].sort();
1152: return argSorts;
1153: }
1154:
1155: /** adds a new instantiation to this TacletApp
1156: * @param sv the SchemaVariable to be instantiated
1157: * @param term the Term the SchemaVariable is instantiated with
1158: * @return the new TacletApp
1159: */
1160: public abstract TacletApp addInstantiation(SchemaVariable sv,
1161: Term term, boolean interesting);
1162:
1163: public abstract TacletApp addInstantiation(SchemaVariable sv,
1164: Object[] list, boolean interesting);
1165:
1166: /**
1167: * adds a new instantiation to this TacletApp. This method does not
1168: * check (beside some very rudimentary tests) if the instantiation is possible.
1169: * If you cannot guarantee that adding the entry <code>(sv, pe)</code> will
1170: * result in a valid taclet instantiation, you have to use
1171: * {@link #addCheckedInstantiation(SchemaVariable, ProgramElement, Services, boolean)}
1172: * instead
1173: * @param sv the SchemaVariable to be instantiated
1174: * @param pe the ProgramElement the SV is instantiated with
1175: * @param interesting a boolean marking if the instantiation of this
1176: * sv needs to be saved for later proof loading (<code>interesting==true</code>)
1177: * or if it can be derived deterministically (e.g. by matching)
1178: * (<code>interesting==false</code>)
1179: * @return a new taclet application equal to this one but including the
1180: * newly added instantiation entry <code>(sv, pe)</code>
1181: */
1182: public abstract TacletApp addInstantiation(SchemaVariable sv,
1183: ProgramElement pe, boolean interesting);
1184:
1185: /**
1186: * checks if the instantiation of <code>sv</code> with <code>pe</code>
1187: * is possible. If the resulting instantiation is valid a new taclet application
1188: * with an extended instantiation mapping is created and returned. Otherwise an
1189: * exception is thrown.
1190: * @param sv the SchemaVariable to be instantiated
1191: * @param pe the ProgramElement the SV is instantiated with
1192: * @param services the Services
1193: * @param interesting a boolean marking if the instantiation of this
1194: * sv needs to be saved for later proof loading (<code>interesting==true</code>)
1195: * or if it can be derived deterministically (e.g. by matching)
1196: * (<code>interesting==false</code>)
1197: * @return a new taclet application equal to this one but including the
1198: * newly added instantiation entry <code>(sv, pe)</code>, if the
1199: * instantiation results in a valid taclet application otherwise an exception is thrown
1200: * @throws IllegalInstantiationException exception thrown if
1201: * <code>sv</code> cannot be instantiated with <code>pe</code> no matter if in general
1202: * or due to side conditions posed by this particular application
1203: *
1204: */
1205: public TacletApp addCheckedInstantiation(SchemaVariable sv,
1206: ProgramElement pe, Services services, boolean interesting) {
1207:
1208: MatchConditions cond = matchConditions();
1209:
1210: if (sv instanceof ProgramSV) {
1211: cond = ((ProgramSV) sv).match(pe, cond, services);
1212: } else {
1213: throw new IllegalInstantiationException(
1214: "Cannot match program element '"
1215: + pe
1216: + "'("
1217: + (pe == null ? null : pe.getClass()
1218: .getName())
1219: + ") to non program sv " + sv);
1220: }
1221:
1222: if (cond == null) {
1223: throw new IllegalInstantiationException("Instantiation "
1224: + pe + "("
1225: + (pe == null ? null : pe.getClass().getName())
1226: + ") is not matched by " + sv);
1227: }
1228:
1229: cond = taclet().checkConditions(cond, services);
1230:
1231: if (cond == null) {
1232: throw new IllegalInstantiationException("Instantiation "
1233: + pe + " of " + sv
1234: + "does not satisfy variable conditions");
1235: }
1236:
1237: if (interesting) {
1238: cond = cond.setInstantiations(cond.getInstantiations()
1239: .makeInteresting(sv));
1240: }
1241:
1242: return addInstantiation(cond.getInstantiations());
1243:
1244: }
1245:
1246: public TacletApp addInstantiation(SchemaVariable sv, Name name) {
1247: return addInstantiation(SVInstantiations.EMPTY_SVINSTANTIATIONS
1248: .addInteresting(sv, name));
1249: }
1250:
1251: /**
1252: * creates a new Taclet application containing all the
1253: * instantiations given
1254: * by the SVInstantiations
1255: * @param svi the SVInstantiations whose entries are the needed
1256: * instantiations
1257: * @return the new Taclet application
1258: */
1259: public abstract TacletApp addInstantiation(SVInstantiations svi);
1260:
1261: /**
1262: * creates a new Taclet application containing all the
1263: * instantiations given
1264: * by the SVInstantiations and forget the old ones
1265: * @param svi the SVInstantiations whose entries are the needed
1266: * instantiations
1267: * @return the new Taclet application
1268: */
1269: protected abstract TacletApp setInstantiation(SVInstantiations svi);
1270:
1271: /**
1272: * creates a new Taclet application containing all the
1273: * instantiations, constraints and new metavariables given
1274: * by the mc object and forget the old ones
1275: */
1276: protected abstract TacletApp setMatchConditions(MatchConditions mc);
1277:
1278: /**
1279: * creates a new Taclet application containing all the
1280: * instantiations, constraints, new metavariables and if formula
1281: * instantiations given and forget the old ones
1282: */
1283: protected abstract TacletApp setAllInstantiations(
1284: MatchConditions mc,
1285: ListOfIfFormulaInstantiation ifInstantiations);
1286:
1287: /**
1288: * Creates a new Taclet application by matching the given formulas
1289: * against the formulas of the if sequent, adding SV
1290: * instantiations, constraints and metavariables as needed. This
1291: * will fail if the if formulas have already been instantiated.
1292: */
1293: public TacletApp setIfFormulaInstantiations(
1294: ListOfIfFormulaInstantiation p_list, Services p_services,
1295: Constraint p_userConstraint) {
1296: assert p_list != null && ifInstsCorrectSize(taclet, p_list)
1297: && ifInstantiations == null : "If instantiations list has wrong size or is null "
1298: + "or the if formulas have already been instantiated";
1299:
1300: MatchConditions mc = taclet().matchIf(p_list.iterator(),
1301: matchConditions(), p_services, p_userConstraint);
1302:
1303: return mc == null ? null : setAllInstantiations(mc, p_list);
1304: }
1305:
1306: /**
1307: * Find all possible instantiations of the if sequent formulas
1308: * within the sequent "p_seq".
1309: * @return a list of tacletapps with the found if formula
1310: * instantiations
1311: */
1312: public ListOfTacletApp findIfFormulaInstantiations(Sequent p_seq,
1313: Services p_services, Constraint p_userConstraint) {
1314:
1315: Debug.assertTrue(ifInstantiations == null,
1316: "The if formulas have already been instantiated");
1317:
1318: if (taclet().ifSequent() == Sequent.EMPTY_SEQUENT)
1319: return SLListOfTacletApp.EMPTY_LIST.prepend(this );
1320:
1321: return findIfFormulaInstantiationsHelp(
1322: createSemisequentList(taclet().ifSequent() // Matching starting
1323: .succedent()), // with the last formula
1324: createSemisequentList(taclet().ifSequent().antecedent()),
1325: IfFormulaInstSeq.createList(p_seq, false),
1326: IfFormulaInstSeq.createList(p_seq, true),
1327: SLListOfIfFormulaInstantiation.EMPTY_LIST,
1328: matchConditions(), p_services, p_userConstraint);
1329:
1330: }
1331:
1332: /**
1333: * Recursive function for matching the remaining tail of an if sequent
1334: * @param p_ifSeqTail tail of the current semisequent as list
1335: * @param p_ifSeqTail2nd the following semisequent
1336: * (i.e. antecedent) or null
1337: * @param p_toMatch list of the formulas to match the current if
1338: * semisequent formulas with
1339: * @param p_toMatch2nd list of the formulas of the antecedent
1340: * @param p_matchCond match conditions until now, i.e. after
1341: * matching the first formulas of the if sequent
1342: */
1343: private ListOfTacletApp findIfFormulaInstantiationsHelp(
1344: ListOfConstrainedFormula p_ifSeqTail,
1345: ListOfConstrainedFormula p_ifSeqTail2nd,
1346: ListOfIfFormulaInstantiation p_toMatch,
1347: ListOfIfFormulaInstantiation p_toMatch2nd,
1348: ListOfIfFormulaInstantiation p_alreadyMatched,
1349: MatchConditions p_matchCond, Services p_services,
1350: Constraint p_userConstraint) {
1351:
1352: while (p_ifSeqTail == SLListOfConstrainedFormula.EMPTY_LIST) {
1353: if (p_ifSeqTail2nd == null) {
1354: // All formulas have been matched, collect the results
1355: TacletApp res = setAllInstantiations(p_matchCond,
1356: p_alreadyMatched);
1357: if (res != null)
1358: return SLListOfTacletApp.EMPTY_LIST.prepend(res);
1359: return SLListOfTacletApp.EMPTY_LIST;
1360: } else {
1361: // Change from succedent to antecedent
1362: p_ifSeqTail = p_ifSeqTail2nd;
1363: p_ifSeqTail2nd = null;
1364: p_toMatch = p_toMatch2nd;
1365: }
1366: }
1367:
1368: // Match the current formula
1369: IfMatchResult mr = taclet().matchIf(p_toMatch.iterator(),
1370: p_ifSeqTail.head().formula(), p_matchCond, p_services,
1371: p_userConstraint);
1372:
1373: // For each matching formula call the method again to match
1374: // the remaining terms
1375: ListOfTacletApp res = SLListOfTacletApp.EMPTY_LIST;
1376: IteratorOfIfFormulaInstantiation itCand = mr.getFormulas()
1377: .iterator();
1378: IteratorOfMatchConditions itMC = mr.getMatchConditions()
1379: .iterator();
1380: p_ifSeqTail = p_ifSeqTail.tail();
1381: while (itCand.hasNext()) {
1382: res = res.prepend(findIfFormulaInstantiationsHelp(
1383: p_ifSeqTail, p_ifSeqTail2nd, p_toMatch,
1384: p_toMatch2nd, p_alreadyMatched.prepend(itCand
1385: .next()), itMC.next(), p_services,
1386: p_userConstraint));
1387: }
1388:
1389: return res;
1390: }
1391:
1392: private ListOfConstrainedFormula createSemisequentList(
1393: Semisequent p_ss) {
1394: ListOfConstrainedFormula res = SLListOfConstrainedFormula.EMPTY_LIST;
1395:
1396: IteratorOfConstrainedFormula it = p_ss.iterator();
1397: while (it.hasNext())
1398: res = res.prepend(it.next());
1399:
1400: return res;
1401: }
1402:
1403: /**
1404: * returns a new PosTacletApp that is equal to this TacletApp except
1405: * that the position is set to the given PosInOccurrence
1406: * @param pos the PosInOccurrence of the newl created PosTacletApp
1407: * @return the new TacletApp
1408: */
1409: public PosTacletApp setPosInOccurrence(PosInOccurrence pos) {
1410: if (taclet() instanceof NoFindTaclet) {
1411: throw new IllegalStateException(
1412: "Cannot add position to an taclet"
1413: + " without find");
1414: }
1415: return PosTacletApp.createPosTacletApp((FindTaclet) taclet(),
1416: instantiations(), constraint(), newMetavariables(),
1417: ifFormulaInstantiations(), pos);
1418: }
1419:
1420: /** returns true iff all necessary informations are collected, so
1421: * that the Taclet can be applied.
1422: * @return true iff all necessary informations are collected, so
1423: * that the Taclet can be applied.
1424: */
1425: public abstract boolean complete();
1426:
1427: /**
1428: * @return true iff the taclet instantiation can be made complete
1429: * using metavariables
1430: */
1431: public abstract boolean sufficientlyComplete();
1432:
1433: /**
1434: * @return true iff the SV instantiations can be made complete
1435: * using metavariables
1436: */
1437: public boolean instsSufficientlyComplete() {
1438: return neededUninstantiatedVars() == SetAsListOfSchemaVariable.EMPTY_SET;
1439: }
1440:
1441: /**
1442: * @return true iff the if instantiation list is not null or no if
1443: * sequent is needed
1444: */
1445: public boolean ifInstsComplete() {
1446: return ifInstantiations != null
1447: || (taclet().ifSequent() == Sequent.EMPTY_SEQUENT);
1448: }
1449:
1450: /**
1451: * returns the PositionInOccurrence (representing a ConstrainedFormula and
1452: * a position in the corresponding formula)
1453: * @return the PosInOccurrence
1454: */
1455: public abstract PosInOccurrence posInOccurrence();
1456:
1457: /** compares the given Object with this one and returns true iff both are
1458: * from type TacletApp with equal taclets, instantiations and positions.
1459: */
1460: public boolean equals(Object o) {
1461: if (o == this )
1462: return true;
1463: if (!(o instanceof TacletApp))
1464: return false;
1465: TacletApp s = (TacletApp) o;
1466: return (s.taclet().equals(taclet()) && s.instantiations()
1467: .equals(instantiations()));
1468: }
1469:
1470: public int hashCode() {
1471: int result = 17;
1472: result = 37 * result + taclet.hashCode();
1473: result = 37 * result + instantiations.hashCode();
1474: return result;
1475: }
1476:
1477: public String toString() {
1478: return "Application of Taclet " + taclet() + " with "
1479: + instantiations() + " and "
1480: + ifFormulaInstantiations();
1481: }
1482:
1483: /**
1484: * checks if there are name conflicts (i.e. there are
1485: * two matched bound SchemaVariable that are matched to variables with an
1486: * equal name); if yes a new TacletApp is returned that equals this
1487: * TacletApp except that the name conflict is resolved by replacing the
1488: * instantiation of one of the conflict-causing SchemaVariables by a
1489: * bound SchemaVariable with a new name;
1490: * if the check is negative, the same TacletApp is returned.
1491: *
1492: * @return a conflict resolved TacletApp, remainder equal to this TacletApp
1493: */
1494: public TacletApp prepareUserInstantiation() {
1495: TacletApp result = this ;
1496: SchemaVariable varSV = varSVNameConflict();
1497: while (varSV != null) {
1498: result = setInstantiation(replaceInstantiation(taclet,
1499: result.instantiations(), varSV));
1500: varSV = result.varSVNameConflict();
1501: }
1502: return result;
1503: }
1504:
1505: protected abstract SetOfQuantifiableVariable contextVars(
1506: SchemaVariable sv);
1507:
1508: /**
1509: * creates a new variable namespace by adding names of the instantiations
1510: * of the schema variables in the context of the given schema
1511: * variable and (if the TacletApp's prefix has the context flag set)
1512: * by adding names of the logic variables of the context.
1513: *
1514: * @param sv the schema variable to be considered
1515: * @param var_ns the old variable namespace
1516: * @return the new created variable namespace
1517: */
1518: public Namespace extendVarNamespaceForSV(Namespace var_ns,
1519: SchemaVariable sv) {
1520: Namespace ns = new Namespace(var_ns);
1521: IteratorOfSchemaVariable it = taclet().getPrefix(sv).prefix()
1522: .iterator();
1523: while (it.hasNext()) {
1524: LogicVariable var = (LogicVariable) ((Term) instantiations()
1525: .getInstantiation(it.next())).op();
1526: ns.add(var);
1527: }
1528: if (taclet().getPrefix(sv).context()) {
1529: IteratorOfQuantifiableVariable lit = contextVars(sv)
1530: .iterator();
1531: while (lit.hasNext()) {
1532: ns.add(lit.next());
1533: }
1534: }
1535: return ns;
1536: }
1537:
1538: /**
1539: * returns the bound SchemaVariable that causes a name conflict (i.e. there are
1540: * two matched bound SchemaVariables that are matched to variables with an
1541: * equal name, the returned SchemaVariable is (an arbitrary) one of these
1542: * SchemaVariables) or null if there is no such conflict
1543: *
1544: * @return null iff there is no conflict and one of the
1545: * conflict-causing bound SchemaVariables
1546: */
1547: public SchemaVariable varSVNameConflict() {
1548: IteratorOfSchemaVariable svIt = uninstantiatedVars().iterator();
1549: while (svIt.hasNext()) {
1550: SchemaVariable sv = svIt.next();
1551: if (sv.isTermSV() || sv.isFormulaSV()) {
1552: TacletPrefix prefix = taclet().getPrefix(sv);
1553: HashSet names = new HashSet();
1554: if (prefix.context()) {
1555: IteratorOfQuantifiableVariable contextIt = contextVars(
1556: sv).iterator();
1557: while (contextIt.hasNext()) {
1558: names.add(contextIt.next().name());
1559: }
1560: }
1561: IteratorOfSchemaVariable varSVIt = prefix.iterator();
1562: while (varSVIt.hasNext()) {
1563: SchemaVariable varSV = varSVIt.next();
1564: Term inst = (Term) instantiations()
1565: .getInstantiation(varSV);
1566: if (inst != null) {
1567: Name name = inst.op().name();
1568: if (!names.contains(name)) {
1569: names.add(name);
1570: } else {
1571: return varSV;
1572: }
1573: }
1574: }
1575: }
1576: }
1577: return null;
1578: }
1579:
1580: /**
1581: * For a given SV of the taclet decide a priori whether an
1582: * instantiation via metavariable is possible
1583: * @return true iff p_var is a termSV with empty prefix
1584: */
1585: public boolean canUseMVAPriori(SchemaVariable p_var) {
1586: if (!p_var.isTermSV() || fixedVars.contains(p_var))
1587: return false;
1588: else {
1589: TacletPrefix prefix = taclet().getPrefix(p_var);
1590: return (prefix.prefix().size() == 0 && !prefix.context());
1591: }
1592: }
1593:
1594: /**
1595: * For a given SV of the taclet decide a posteriori whether an
1596: * instantiation via metavariable is possible
1597: * @param p_term Term to instantiate the schemavariable with
1598: */
1599: protected boolean canUseMVAPosteriori(SchemaVariable p_var,
1600: Term p_term) {
1601: // disabled
1602: return false;
1603: // return canUseMVAPriori ( p_var ) && p_term.isRigid ();
1604: }
1605:
1606: /**
1607: * @return true iff the list of if instantiations has the correct
1608: * size or is null
1609: */
1610: protected static boolean ifInstsCorrectSize(Taclet p_taclet,
1611: ListOfIfFormulaInstantiation p_list) {
1612: return p_list == null
1613: || p_list.size() == (p_taclet.ifSequent().antecedent()
1614: .size() + p_taclet.ifSequent().succedent()
1615: .size());
1616: }
1617:
1618: /**
1619: * @return true iff the Taclet may be applied for the
1620: * given mode (interactive/non-interactive, activated rule sets)
1621: */
1622: public boolean admissible(boolean interactive,
1623: ListOfRuleSet ruleSets) {
1624: return taclet().admissible(interactive, ruleSets);
1625: }
1626:
1627: /** checks if the variable conditions of type 'x not free in y' are
1628: * hold by the found instantiations. The variable conditions is used
1629: * implicit in the prefix. (Used to calculate the prefix)
1630: * @param taclet the Taclet that is tried to be instantiated. A match for the
1631: * find (or/and if) has been found.
1632: * @param instantiations the SVInstantiations so that the find(if)
1633: * expression matches
1634: * @param pos the PosInOccurrence where the Taclet is applied
1635: * @return true iff all variable conditions x not free in y are hold
1636: */
1637: public static boolean checkVarCondNotFreeIn(Taclet taclet,
1638: SVInstantiations instantiations, PosInOccurrence pos) {
1639:
1640: IteratorOfSchemaVariable it = instantiations.svIterator();
1641: while (it.hasNext()) {
1642: SchemaVariable sv = it.next();
1643: if (sv.isTermSV() || sv.isFormulaSV()) {
1644: if (!((Term) instantiations.getInstantiation(sv))
1645: .freeVars().subset(
1646: boundAtOccurrenceSet(taclet
1647: .getPrefix(sv), instantiations,
1648: pos))) {
1649:
1650: return false;
1651: }
1652: }
1653: }
1654: return true;
1655: }
1656:
1657: /** collects all bound vars that are bound above the subterm described by
1658: * the given term position information
1659: * @param pos the PosInOccurrence describing a subterm in Term
1660: * @return a set of logic variables that are bound above the specified
1661: * subterm
1662: */
1663: protected static SetOfQuantifiableVariable collectBoundVarsAbove(
1664: PosInOccurrence pos) {
1665: SetOfQuantifiableVariable result = SetAsListOfQuantifiableVariable.EMPTY_SET;
1666:
1667: PIOPathIterator it = pos.iterator();
1668: int i;
1669: ArrayOfQuantifiableVariable vars;
1670:
1671: while ((i = it.next()) != -1) {
1672: vars = it.getSubTerm().varsBoundHere(i);
1673: for (i = 0; i < vars.size(); i++)
1674: result = result.add(vars.getQuantifiableVariable(i));
1675: }
1676:
1677: return result;
1678: }
1679: }
|