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.io.StringReader;
014:
015: import javax.swing.DefaultComboBoxModel;
016:
017: import de.uka.ilkd.key.java.Recoder2KeY;
018: import de.uka.ilkd.key.java.Services;
019: import de.uka.ilkd.key.logic.*;
020: import de.uka.ilkd.key.parser.KeYLexer;
021: import de.uka.ilkd.key.parser.KeYParser;
022: import de.uka.ilkd.key.parser.ParserMode;
023: import de.uka.ilkd.key.pp.AbbrevMap;
024: import de.uka.ilkd.key.rule.IfFormulaInstDirect;
025: import de.uka.ilkd.key.rule.IfFormulaInstantiation;
026: import de.uka.ilkd.key.rule.IteratorOfIfFormulaInstantiation;
027: import de.uka.ilkd.key.rule.ListOfIfFormulaInstantiation;
028:
029: public class IfChoiceModel extends DefaultComboBoxModel {
030:
031: private static final String manualText = "Manual Input";
032: private String manualInput;
033: // private RuleApp app;
034: private Term ifFma;
035:
036: /** namespaces (variables, functions, sorts, etc.) */
037: private NamespaceSet nss;
038: private AbbrevMap scm;
039: private Services services;
040:
041: public IfChoiceModel(Term p_ifFma,
042: ListOfIfFormulaInstantiation p_candidates,
043: Services p_services, NamespaceSet nss, AbbrevMap scm) {
044: super (createIfInsts(p_candidates));
045:
046: ifFma = p_ifFma;
047: services = p_services;
048: this .nss = nss;
049: this .scm = scm;
050:
051: addElement(manualText);
052: manualInput = "";
053: }
054:
055: public String manualText() {
056: return manualText;
057: }
058:
059: public void setInput(String s) {
060: manualInput = s;
061: }
062:
063: public Term ifFma() {
064: return ifFma;
065: }
066:
067: public static Object[] createIfInsts(
068: ListOfIfFormulaInstantiation p_candidates) {
069: Object[] res = new Object[p_candidates.size()];
070: IteratorOfIfFormulaInstantiation it = p_candidates.iterator();
071: int i = 0;
072:
073: while (it.hasNext())
074: res[i++] = it.next();
075:
076: return res;
077: }
078:
079: /** creates a new Termparser that parses the given string
080: * @param s the String to parse
081: */
082: private KeYParser stringParser(String s) {
083: return new KeYParser(ParserMode.TERM, new KeYLexer(
084: new StringReader(s), services.getExceptionHandler()),
085: "", TermFactory.DEFAULT,
086: new Recoder2KeY(services, nss), services, nss, scm);
087: }
088:
089: /**
090: * parses and returns the term encoded as string 's'
091: * @param s the String to parse
092: * @return the term encoded in 's'
093: */
094: public Term parseFormula(String s) throws antlr.ANTLRException {
095: KeYParser p = stringParser(s);
096: return p.formula();
097: }
098:
099: /**
100: * @param pos int describes position of the if-sequent
101: * (only required for error message)
102: * @return the selected instantiation of the if sequent
103: */
104: public IfFormulaInstantiation getSelection(int pos)
105: throws SVInstantiationParserException,
106: MissingInstantiationException {
107: Object o = getSelectedItem();
108: if (o != manualText) {
109: return (IfFormulaInstantiation) o;
110: }
111: try {
112: if (manualInput == null || "".equals(manualInput)) {
113: throw new MissingInstantiationException(
114: "'\\assumes'-formula: "
115: + ProofSaver.printAnything(ifFma,
116: services), pos + 1, -1, true);
117: }
118:
119: return new IfFormulaInstDirect(new ConstrainedFormula(
120: parseFormula(manualInput), Constraint.BOTTOM));
121: } catch (antlr.RecognitionException are) {
122: throw new SVInstantiationParserException(manualInput, pos
123: + are.getLine(), are.getColumn(),
124: "Problem occured parsing a manual input"
125: + " of an '\\assumes'-sequent.\n"
126: + are.getMessage(), true);
127: } catch (antlr.ANTLRException e) {
128: throw new SVInstantiationParserException(manualInput, pos,
129: -1, "Problem occured parsing a manual input"
130: + " of an '\\assumes'-sequent.\n"
131: + e.getMessage(), true);
132: }
133: }
134:
135: }
|