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.proof;
012:
013: import java.util.Vector;
014:
015: import de.uka.ilkd.key.java.Services;
016: import de.uka.ilkd.key.logic.*;
017: import de.uka.ilkd.key.pp.AbbrevMap;
018: import de.uka.ilkd.key.rule.*;
019: import de.uka.ilkd.key.rule.inst.IllegalInstantiationException;
020: import de.uka.ilkd.key.rule.inst.SortException;
021:
022: public class ApplyTacletDialogModel {
023:
024: /** the model used for the instantiation of the if-sequent */
025: private IfChoiceModel[] ifChoiceModel;
026: private static final IfChoiceModel[] EMPTY_IF_CHOICES = new IfChoiceModel[0];
027: /** the model used for the instantiation of the schemavariables */
028: private TacletInstantiationsTableModel tableModel;
029:
030: /**
031: * the application of the Taclet of which this model is used to
032: * complete the instantiations of the schemavariables and/or
033: * if-sequent
034: */
035: private TacletApp app;
036:
037: /** the sequent the application above is applied */
038: private Sequent seq;
039:
040: /** listeners of this model */
041: private Vector listeners = new Vector();
042: /** the change event that is sent */
043: private final ModelEvent changeEvent = new ModelEvent(this );
044:
045: /** namespace of variables */
046: private NamespaceSet nss;
047: private Services services;
048: private Constraint userConstraint;
049: private AbbrevMap scm;
050: private Proof proof;
051:
052: /**
053: * create new data model for the apply Taclet dialog wrapping a combo box
054: * model and a table model
055: */
056: public ApplyTacletDialogModel(TacletApp app, Sequent seq,
057: Services services, Constraint userConstraint,
058: NamespaceSet nss, AbbrevMap scm, Goal goal) {
059: this .app = app;
060: this .seq = seq;
061: this .services = services;
062: this .userConstraint = userConstraint;
063: this .nss = nss;
064: this .scm = scm;
065: this .proof = goal.proof();
066: initIfChoiceModels();
067:
068: tableModel = new TacletInstantiationsTableModel(app, services,
069: nss, scm, goal);
070: }
071:
072: public void addModelChangeListener(ModelChangeListener l) {
073: listeners.add(l);
074: }
075:
076: public void removeModelChangeListener(ModelChangeListener l) {
077: listeners.remove(l);
078: }
079:
080: public IfChoiceModel ifChoiceModel(int i) {
081: return ifChoiceModel[i];
082: }
083:
084: public int ifChoiceModelCount() {
085: return ifChoiceModel.length;
086: }
087:
088: public TacletInstantiationsTableModel tableModel() {
089: return tableModel;
090: }
091:
092: public TacletApp application() {
093: return app;
094: }
095:
096: public Taclet taclet() {
097: return app.taclet();
098: }
099:
100: public TacletApp tacletApp() {
101: return app;
102: }
103:
104: public Proof proof() {
105: return proof;
106: }
107:
108: public Term ifFma(int i) {
109: return ifChoiceModel(i).ifFma();
110: }
111:
112: private void initIfChoiceModels() {
113: Sequent ifseq = taclet().ifSequent();
114: int asize = ifseq.antecedent().size();
115: int size = asize + ifseq.succedent().size();
116:
117: if (size > 0) {
118: ListOfIfFormulaInstantiation antecCand = IfFormulaInstSeq
119: .createList(seq, true);
120: ListOfIfFormulaInstantiation succCand = IfFormulaInstSeq
121: .createList(seq, false);
122:
123: IteratorOfConstrainedFormula it = ifseq.iterator();
124: Term ifFma;
125: MatchConditions matchCond = app.matchConditions();
126:
127: ifChoiceModel = new IfChoiceModel[size];
128:
129: for (int i = 0; i < size; i++) {
130: ifFma = it.next().formula();
131: ifChoiceModel[i] = new IfChoiceModel(ifFma, taclet()
132: .matchIf(
133: (i < asize ? antecCand.iterator()
134: : succCand.iterator()), ifFma,
135: matchCond, services, userConstraint)
136: .getFormulas(), services, nss, scm);
137: }
138: } else
139: ifChoiceModel = EMPTY_IF_CHOICES;
140: }
141:
142: private TacletApp createTacletAppFromIfs(TacletApp tacletApp)
143: throws IfMismatchException, SVInstantiationParserException,
144: MissingInstantiationException, SortMismatchException {
145:
146: ListOfIfFormulaInstantiation instList = SLListOfIfFormulaInstantiation.EMPTY_LIST;
147:
148: int i = ifChoiceModel.length;
149: while (i-- != 0) {
150: instList = instList.prepend(ifChoiceModel[i]
151: .getSelection(i));
152: }
153:
154: try {
155: tacletApp = tacletApp.setIfFormulaInstantiations(instList,
156: services, userConstraint);
157: } catch (SortException e) {
158: throw new SortMismatchException("'\\assumes'-sequent",
159: null, 0, 0);
160: }
161:
162: if (tacletApp == null) {
163: throw new IfMismatchException(
164: "Mismatch of '\\assumes'-formulas.\n"
165: + "Reasons may be: ambigous instantiation "
166: + "of schemavariables or unsatisfiable constraints.");
167: }
168:
169: return tacletApp;
170: }
171:
172: public String getStatusString() {
173: TacletApp rapp = app;
174:
175: if (rapp == null) {
176: return "Rule is not applicable.";
177: }
178:
179: try {
180: rapp = createTacletApp();
181: } catch (SVInstantiationException ime) {
182: return "Rule is not applicable.\n Detail:"
183: + ime.getMessage();
184: } catch (IllegalInstantiationException iie) {
185: return "Rule is not applicable.\n Detail:"
186: + iie.getMessage();
187: } catch (de.uka.ilkd.key.util.ExceptionHandlerException e) {
188: services.getExceptionHandler().clear();
189: return "Rule is not applicable.\n Detail:"
190: + e.getCause().getMessage();
191: }
192:
193: if (rapp.sufficientlyComplete())
194: return "Instantiation is OK.";
195: else
196: return "Instantiations are incomplete.";
197:
198: }
199:
200: public TacletApp createTacletApp() throws SVInstantiationException {
201: return createTacletAppFromIfs(tableModel
202: .createTacletAppFromVarInsts());
203: }
204:
205: private void informListenerAboutModelChange() {
206: for (int i = 0; i < listeners.size(); i++) {
207: if (listeners.get(i) != null) {
208: ((ModelChangeListener) listeners.get(i))
209: .modelChanged(changeEvent);
210: }
211: }
212: }
213:
214: /** sets the manual if-input */
215: public void setManualInput(int i, String s) {
216: ifChoiceModel(i).setInput(s);
217: informListenerAboutModelChange();
218: }
219:
220: /**
221: * replaces the TacletApp of this ApplyTacletDialogModel by an TacletApp
222: * where all name conflicts are resolved and thus the parser is enabled
223: * to accept variables from the context or the prefix of the Taclet.
224: *
225: */
226: public void prepareUnmatchedInstantiation() {
227: app = app.prepareUserInstantiation();
228: }
229:
230: public Namespace programVariables() {
231: return nss.programVariables();
232: }
233:
234: }
|