001: // This file is part of KeY - Integrated Deductive Software Design
002: // Copyright (C) 2001-2007 Universitaet Karlsruhe, Germany
003: // Universitaet Koblenz-Landau, Germany
004: // Chalmers University of Technology, Sweden
005: //
006: // The KeY system is protected by the GNU General Public License.
007: // See LICENSE.TXT for details.
008: //
009: //
010:
011: package de.uka.ilkd.key.rule;
012:
013: import de.uka.ilkd.key.logic.IteratorOfConstrainedFormula;
014: import de.uka.ilkd.key.logic.Sequent;
015: import de.uka.ilkd.key.logic.Term;
016: import de.uka.ilkd.key.logic.op.*;
017:
018: public class TacletPrefixBuilder {
019:
020: /**
021: * set of all schemavariables that are only allowed to be matched
022: * with quantifiable variables.
023: */
024: private SetOfSchemaVariable currentlyBoundVars = SetAsListOfSchemaVariable.EMPTY_SET;
025: private TacletBuilder tacletBuilder;
026:
027: protected MapFromSchemaVariableToTacletPrefix prefixMap = MapAsListFromSchemaVariableToTacletPrefix.EMPTY_MAP;
028:
029: TacletPrefixBuilder(TacletBuilder tacletBuilder) {
030: this .tacletBuilder = tacletBuilder;
031: }
032:
033: private void addVarsBoundHere(Term visited, int subTerm) {
034: ArrayOfQuantifiableVariable bdVars = visited
035: .varsBoundHere(subTerm);
036: for (int i = 0; i < bdVars.size(); i++) {
037: QuantifiableVariable boundVar = bdVars
038: .getQuantifiableVariable(i);
039: if (boundVar instanceof SchemaVariable
040: && ((SchemaVariable) boundVar).isVariableSV()) {
041: currentlyBoundVars = currentlyBoundVars
042: .add((SchemaVariable) boundVar);
043: }
044: }
045: }
046:
047: private void setPrefixOfOccurrence(SchemaVariable sv,
048: SetOfSchemaVariable relevantBoundVars) {
049: prefixMap = prefixMap.put(sv, new TacletPrefix(
050: relevantBoundVars, false));
051: }
052:
053: /**
054: * removes all variables x that are declared as x not free in sv from the
055: * currently bound vars set.
056: */
057: private SetOfSchemaVariable removeNotFreeIn(SchemaVariable sv) {
058: SetOfSchemaVariable result = currentlyBoundVars;
059: IteratorOfNotFreeIn it = tacletBuilder.varsNotFreeIn();
060: while (it.hasNext()) {
061: NotFreeIn notFreeIn = it.next();
062: if (notFreeIn.second() == sv) {
063: result = result.remove(notFreeIn.first());
064: }
065: }
066: return result;
067: }
068:
069: private void visit(Term t) {
070: if (t.op() instanceof SortedSchemaVariable
071: && !((SchemaVariable) t.op()).isVariableSV()
072: && !((SchemaVariable) t.op()).isProgramSV()
073: && !((SchemaVariable) t.op()).isSkolemTermSV()) { // see below /AR
074: SchemaVariable sv = (SchemaVariable) t.op();
075: SetOfSchemaVariable relevantBoundVars = removeNotFreeIn(sv);
076: TacletPrefix prefix = prefixMap.get(sv);
077: if (prefix == null
078: || prefix.prefix().equals(relevantBoundVars)) {
079: setPrefixOfOccurrence(sv, relevantBoundVars);
080: } else {
081: throw new InvalidPrefixException(tacletBuilder
082: .getName().toString(), sv, prefix,
083: relevantBoundVars);
084: }
085: }
086: for (int i = 0; i < t.arity(); i++) {
087: SetOfSchemaVariable oldBounds = currentlyBoundVars;
088: addVarsBoundHere(t, i);
089: visit(t.sub(i));
090: currentlyBoundVars = oldBounds;
091: }
092: }
093:
094: private void visit(Sequent s) {
095: IteratorOfConstrainedFormula it = s.iterator();
096: while (it.hasNext()) {
097: visit(it.next().formula());
098: }
099: }
100:
101: private void visit(TacletGoalTemplate templ) {
102: visit(templ.sequent());
103: if (templ instanceof RewriteTacletGoalTemplate) {
104: visit(((RewriteTacletGoalTemplate) templ).replaceWith());
105: }
106: if (templ instanceof AntecSuccTacletGoalTemplate) {
107: visit(((AntecSuccTacletGoalTemplate) templ).replaceWith());
108: }
109: }
110:
111: public void build() {
112: visit(tacletBuilder.ifSequent());
113:
114: if (tacletBuilder instanceof FindTacletBuilder) {
115: visit(((FindTacletBuilder) tacletBuilder).getFind());
116: }
117:
118: IteratorOfTacletGoalTemplate itGoalTempl = tacletBuilder
119: .goalTemplates().iterator();
120:
121: while (itGoalTempl.hasNext()) {
122: visit(itGoalTempl.next());
123: }
124:
125: itGoalTempl = tacletBuilder.goalTemplates().iterator();
126: while (itGoalTempl.hasNext()) {
127: final IteratorOfTaclet addRules = itGoalTempl.next()
128: .rules().iterator();
129: while (addRules.hasNext()) {
130: checkPrefixInAddRules(addRules.next());
131: }
132: }
133: }
134:
135: private void checkPrefixInAddRules(Taclet addRule) {
136: final MapFromSchemaVariableToTacletPrefix addRuleSV2PrefixMap = addRule
137: .prefixMap();
138: final IteratorOfEntryOfSchemaVariableAndTacletPrefix it = prefixMap
139: .entryIterator();
140: while (it.hasNext()) {
141: final EntryOfSchemaVariableAndTacletPrefix entry = it
142: .next();
143: final TacletPrefix addRulePrefix = addRuleSV2PrefixMap
144: .get(entry.key());
145:
146: if (addRulePrefix != null
147: && !addRulePrefix.prefix().equals(
148: entry.value().prefix())) {
149: throw new InvalidPrefixException(tacletBuilder
150: .getName().toString(), entry.key(), entry
151: .value(), addRulePrefix.prefix());
152: }
153: }
154:
155: // we have to descend into the addrules of the addrules
156:
157: final IteratorOfTacletGoalTemplate templateIt = addRule
158: .goalTemplates().iterator();
159: while (templateIt.hasNext()) {
160: final IteratorOfTaclet moreRules = templateIt.next()
161: .rules().iterator();
162: while (moreRules.hasNext()) {
163: checkPrefixInAddRules(moreRules.next());
164: }
165: }
166: }
167:
168: private boolean atMostOneRepl() {
169: RewriteTacletBuilder rwtacletBuilder = (RewriteTacletBuilder) tacletBuilder;
170: IteratorOfTacletGoalTemplate it = rwtacletBuilder
171: .goalTemplates().iterator();
172: int count = 0;
173: while (it.hasNext()) {
174: TacletGoalTemplate tmpl = it.next();
175: if (tmpl instanceof RewriteTacletGoalTemplate) {
176: if (((RewriteTacletGoalTemplate) tmpl).replaceWith() != null) {
177: count++;
178: }
179: }
180: if (count > 1)
181: return false;
182: }
183: return true;
184: }
185:
186: private boolean occurrsOnlyInFindOrRepl(SchemaVariable sv) {
187: RewriteTacletBuilder rwtacletBuilder = (RewriteTacletBuilder) tacletBuilder;
188: TacletSchemaVariableCollector svc = new TacletSchemaVariableCollector();
189: svc.visit(rwtacletBuilder.ifSequent());
190: IteratorOfTacletGoalTemplate it = rwtacletBuilder
191: .goalTemplates().iterator();
192: while (it.hasNext()) {
193: TacletGoalTemplate tmpl = it.next();
194: // if (tmpl instanceof RewriteTacletGoalTemplate) {
195: // RewriteTacletGoalTemplate
196: // gt=(RewriteTacletGoalTemplate)tmpl;
197: svc.visit(tmpl.sequent());
198: IteratorOfTaclet addRuleIt = tmpl.rules().iterator();
199: while (addRuleIt.hasNext()) { // addrules
200: svc.visit(addRuleIt.next(), true);
201: }
202: }
203: // }
204: return !svc.contains(sv);
205: }
206:
207: private void considerContext() {
208: if (!(tacletBuilder instanceof RewriteTacletBuilder)
209: || !atMostOneRepl()) {
210: return;
211: }
212: IteratorOfEntryOfSchemaVariableAndTacletPrefix it = prefixMap
213: .entryIterator();
214: while (it.hasNext()) {
215: EntryOfSchemaVariableAndTacletPrefix entry = it.next();
216: if (occurrsOnlyInFindOrRepl(entry.key())) {
217: prefixMap = prefixMap.put(entry.key(), entry.value()
218: .setContext(true));
219: }
220: }
221: }
222:
223: public MapFromSchemaVariableToTacletPrefix getPrefixMap() {
224: considerContext();
225: return prefixMap;
226: }
227:
228: class InvalidPrefixException extends IllegalStateException {
229: /**
230: *
231: */
232: private static final long serialVersionUID = 5855187579027274363L;
233:
234: InvalidPrefixException(String tacletName, SchemaVariable sv,
235: TacletPrefix prefix, SetOfSchemaVariable sndPrefixVar) {
236: super (
237: "Schema variable "
238: + sv
239: + "occurs at different places "
240: + "in taclet "
241: + tacletName
242: + " with different prefixes.\n"
243: + "Prefix P1:"
244: + ((prefix == null) ? SetAsListOfSchemaVariable.EMPTY_SET
245: : prefix.prefix()) + "\n"
246: + "Prefix P2:" + sndPrefixVar);
247: }
248:
249: }
250:
251: }
|