Small tweaks to proof script engine

key.core/src/main/java/de/uka/ilkd/key/macros/scripts/EngineState.java

@@ -22,6 +22,8 @@
 import de.uka.ilkd.key.proof.Proof;
 import de.uka.ilkd.key.settings.ProofSettings;
 
+import javax.annotation.Nonnull;
+
 /**
  * @author Alexander Weigl
  * @version 1 (28.03.17)
@@ -87,7 +89,7 @@ public Proof getProof() {
      * @throws ScriptException If there is no such {@link Goal}, or something else goes wrong.
      */
     @SuppressWarnings("unused")
-    public Goal getFirstOpenGoal(boolean checkAutomatic) throws ScriptException {
+    public @Nonnull Goal getFirstOpenGoal(boolean checkAutomatic) throws ScriptException {
         if (proof.closed()) {
             throw new ProofAlreadyClosedException("The proof is closed already");
         }

key.core/src/main/java/de/uka/ilkd/key/macros/scripts/FocusCommand.java

@@ -0,0 +1,126 @@
+package de.uka.ilkd.key.macros.scripts;
+
+import de.uka.ilkd.key.logic.*;
+import de.uka.ilkd.key.logic.op.SchemaVariable;
+import de.uka.ilkd.key.macros.scripts.meta.Option;
+import de.uka.ilkd.key.proof.Goal;
+import de.uka.ilkd.key.rule.FindTaclet;
+import de.uka.ilkd.key.rule.PosTacletApp;
+import de.uka.ilkd.key.rule.Taclet;
+import de.uka.ilkd.key.rule.TacletApp;
+import de.uka.ilkd.key.rule.inst.SVInstantiations;
+import org.key_project.util.collection.ImmutableList;
+
+import java.util.Iterator;
+import java.util.Set;
+
+/**
+ * Hide all formulas that are not selected Parameter: * The sequent with those formulas that should
+ * not be hidden Created by sarah on 1/12/17.
+ */
+public class FocusCommand extends AbstractCommand<FocusCommand.Parameters> {
+
+    public FocusCommand() {
+        super(Parameters.class);
+    }
+
+    static class Parameters {
+        @Option("#2")
+        public Sequent toKeep;
+    }
+
+    @Override
+    public void execute(Parameters s) throws ScriptException, InterruptedException {
+        if (s == null) {
+            throw new ScriptException("Missing 'sequent' argument for focus");
+        }
+
+        Sequent toKeep = s.toKeep;
+
+        // toKeep = parseSequent(sequentString, getGoalFromCurrentState());
+        hideAll(toKeep);
+
+    }
+
+    @Override
+    public String getName() {
+        return "focus";
+    }
+
+    /*
+     * private Goal getGoalFromCurrentState() { Object fixedGoal = stateMap.get(GOAL_KEY); if
+     * (fixedGoal instanceof Node) { Node fixed = (Node) fixedGoal; //case node is already modified
+     * by focus, the child has to be returned if (!fixed.leaf()) { assert fixed.childrenCount() ==
+     * 1; fixed = fixed.child(0); } Goal g = state.getGoal(proof.openGoals(), fixed); return g; }
+     * return null; }
+     */
+
+    /**
+     * Hide all formulas of the sequent that are not on focus sequent
+     *
+     * @param toKeep sequent containing formulas to keep
+     * @throws ScriptException if no goal is currently open
+     */
+    private void hideAll(Sequent toKeep) throws ScriptException {
+        Goal goal = state.getFirstOpenAutomaticGoal();
+        assert goal != null : "not null by contract of the method";
+
+        // The formulas to keep in the antecedent
+        ImmutableList<Term> keepAnte = toKeep.antecedent().asList().map(SequentFormula::formula);
+        ImmutableList<SequentFormula> ante = goal.sequent().antecedent().asList();
+
+        for (SequentFormula seqFormula : ante) {
+            // This means "!keepAnte.contains(seqFormula.formula)" but with equality mod renaming!
+            if (!keepAnte.exists(it -> it.equalsModRenaming(seqFormula.formula()))) {
+                Taclet tac = getHideTaclet("left");
+                makeTacletApp(goal, seqFormula, tac, true);
+            }
+        }
+
+        ImmutableList<Term> keepSucc = toKeep.succedent().asList().map(SequentFormula::formula);
+        ImmutableList<SequentFormula> succ = goal.sequent().succedent().asList();
+        for (SequentFormula seqFormula : succ) {
+            if (!keepSucc.exists(it -> it.equalsModRenaming(seqFormula.formula()))) {
+                Taclet tac = getHideTaclet("right");
+                makeTacletApp(goal, seqFormula, tac, false);
+            }
+        }
+    }
+
+    // determine where formula in sequent and apply either hide_left or hide_right
+    private Taclet getHideTaclet(String pos) {
+        String ruleName = "hide_" + pos;
+        return proof.getEnv().getInitConfigForEnvironment().lookupActiveTaclet(new Name(ruleName));
+    }
+
+    /**
+     * Make tacletApp for one sequent formula to hide on the sequent
+     *
+     * @param g the goal on which this hide rule should be applied to
+     * @param toHide the sequent formula to hide
+     * @param tac the taclet top apply (either hide_left or hide_right)
+     * @param antec whether the formula is in the antecedent
+     */
+    private void makeTacletApp(Goal g, SequentFormula toHide, Taclet tac, boolean antec) {
+
+        // hide rules only applicable to top-level terms/sequent formulas
+        PosInTerm pit = PosInTerm.getTopLevel();
+
+        PosInOccurrence pio = new PosInOccurrence(toHide, pit, antec);
+
+        Set<SchemaVariable> svs = tac.collectSchemaVars();
+        assert svs.size() == 1;
+        Iterator<SchemaVariable> iter = svs.iterator();
+        SchemaVariable sv = (SchemaVariable) iter.next();
+
+        SVInstantiations inst = SVInstantiations.EMPTY_SVINSTANTIATIONS;
+
+        TacletApp app =
+            PosTacletApp.createPosTacletApp((FindTaclet) tac, inst, pio, proof.getServices());
+        app = app.addCheckedInstantiation(sv, toHide.formula(), proof.getServices(), true);
+        g.apply(app);
+
+    }
+
+}
+

key.core/src/main/java/de/uka/ilkd/key/macros/scripts/meta/ValueInjector.java

@@ -191,7 +191,7 @@ private Object convert(ProofScriptArgument<?> meta, String val)
             return converter.convert(val);
         } catch (Exception e) {
             throw new ConversionException(String.format("Could not convert value %s to type %s",
-                val, meta.getField().getType()), e, meta);
+                val, meta.getField().getType().getName()), e, meta);
         }
     }
 

key.core/src/main/java/de/uka/ilkd/key/nparser/KeyIO.java

@@ -104,9 +104,10 @@ public KeyIO() {
      * @return a valid sequent
      * @throws BuildingException if an unrecoverable error during construction or parsing happened
      */
-    public @Nonnull Sequent parseSequence(@Nonnull CharStream stream) {
+    public @Nonnull Sequent parseSequent(@Nonnull CharStream stream) {
         KeyAst.Seq ctx = ParsingFacade.parseSequent(stream);
         ExpressionBuilder visitor = new ExpressionBuilder(services, nss);
+        visitor.setAbbrevMap(abbrevMap);
         if (schemaNamespace != null)
             visitor.setSchemaVariables(schemaNamespace);
         Sequent seq = (Sequent) ctx.accept(visitor);