From 851606e0dd034c79d0f026c658aaab21bfbd2ded Mon Sep 17 00:00:00 2001 From: Mattias Ulbrich Date: Sun, 5 Feb 2023 12:58:08 +0100 Subject: [PATCH 1/4] adding features to immutable lists --- .../util/collection/ImmutableList.java | 92 +++++++++++++++++++ .../util/collection/Immutables.java | 56 +++++++++++ .../util/collection/TestImmutables.java | 55 +++++++++++ 3 files changed, 203 insertions(+) diff --git a/key.util/src/main/java/org/key_project/util/collection/ImmutableList.java b/key.util/src/main/java/org/key_project/util/collection/ImmutableList.java index 5417d7f2662..abf764c46e1 100644 --- a/key.util/src/main/java/org/key_project/util/collection/ImmutableList.java +++ b/key.util/src/main/java/org/key_project/util/collection/ImmutableList.java @@ -1,6 +1,8 @@ package org.key_project.util.collection; +import javax.annotation.Nonnull; import java.util.*; +import java.util.function.Function; import java.util.function.Predicate; import java.util.stream.Collector; import java.util.stream.Stream; @@ -39,6 +41,70 @@ public static ImmutableList fromList(Collection list) { return result; } + /** + * Return an empty immutable list. + * + * @return empty immutable list. + * @param the entry type of the list. + */ + public static ImmutableList of() { + return ImmutableSLList.nil(); + } + + /** + * Return a singleton immutable list. + * + * @param e1 the element to put into the list + * @return singleton immutable list. + * @param the entry type of the list. + */ + public static ImmutableList of(T e1) { + return ImmutableSLList.singleton(e1); + } + + /** + * Return an immutable list with two elements. + * The iteration order is: e1 then e2 + * + * @param e1 the element to put into the list + * @param e2 the element to put into the list + * @return (e1, e2) as immutable list + * @param the entry type of the list. + */ + public static ImmutableList of(T e1, T e2) { + return ImmutableSLList.singleton(e2).prepend(e1); + } + + /** + * Return an immutable list with three elements. + * The iteration order is: e1 then e2 then e3 + * + * @param e1 the element to put into the list + * @param e2 the element to put into the list + * @param e3 the element to put into the list + * @return (e1, e2, e3) as immutable list + * @param the entry type of the list. + */ + public static ImmutableList of(T e1, T e2, T e3) { + return ImmutableSLList.singleton(e3).prepend(e2).prepend(e1); + } + + /** + * Return an immutable list with the iterated elements. + * The iteration order is the order of the arguments + * + * @param es the elements to put into the list + * @return (e1, e2, e3, ...) as immutable list + * @param the entry type of the list. + */ + public static ImmutableList of(T... es) { + ImmutableList result = ImmutableSLList.nil(); + for (int i = es.length-1; i >= 0; i--) { + result = result.prepend(es[i]); + } + return result; + } + /** * prepends element to the list (non-destructive) * @@ -207,4 +273,30 @@ default List toList() { } return result; } + + /* + * Returns an immutable list consisting of the elements of this list that match + * the given predicate. + * + * @param predicate a non-interfering, stateless + * predicate to apply to each element to determine if it + * should be included + * @returns the filtered list + */ + default @Nonnull ImmutableList filter(@Nonnull Predicate predicate) { + return Immutables.filter(this, predicate); + } + + /** + * Returns an immutable list consisting of the results of applying the given + * function to the elements of this list. + * + * @param The element type of the result list + * @param function a non-interfering, stateless function to apply to each element + * @return the mapped list of the same length as this + */ + default ImmutableList map(Function function) { + return Immutables.map(this, function); + } + } diff --git a/key.util/src/main/java/org/key_project/util/collection/Immutables.java b/key.util/src/main/java/org/key_project/util/collection/Immutables.java index 269f8918852..f853c08b4b0 100644 --- a/key.util/src/main/java/org/key_project/util/collection/Immutables.java +++ b/key.util/src/main/java/org/key_project/util/collection/Immutables.java @@ -2,6 +2,8 @@ import java.util.HashSet; import java.util.Set; +import java.util.function.Function; +import java.util.function.Predicate; /** * This class is a collection of methods that operate on immutable collections, in particular @@ -131,6 +133,16 @@ public static ImmutableSet createSetFrom(Iterable iterable) { return DefaultImmutableSet.fromImmutableList(createListFrom(iterable)); } + /* + * Returns an immutable list consisting of the elements of the + * given iterable collection. + * + * The iteration order of the result is identical to that of the argument. + * + * @param iterable the collection to iterate through to obtain the elements + * for the resulting list + * @returns the view onto the iterable as an immutable list + */ public static ImmutableList createListFrom(Iterable iterable) { ImmutableList result = ImmutableSLList.nil(); for (T t : iterable) { @@ -139,4 +151,48 @@ public static ImmutableList createListFrom(Iterable iterable) { return result.reverse(); } + /* + * Returns an immutable list consisting of the elements of the list that match + * the given predicate. + * + * @param ts non-null immutable list. + * @param predicate a non-interfering, stateless + * predicate to apply to each element to determine if it + * should be included + * @returns the filtered list + */ + public static ImmutableList filter(ImmutableList ts, Predicate predicate) { + // This must be a loop. A tail recursive implementation is not optimised + // by the compiler and quickly leads to a stack overlow. + ImmutableList acc = ImmutableSLList.nil(); + while(ts.size() > 0) { + T hd = ts.head(); + if (predicate.test(hd)) { + acc = acc.prepend(hd); + } + ts = ts.tail(); + } + return acc.reverse(); + } + + /** + * Returns an immutable list consisting of the results of applying the given + * function to the elements of the list. + * + * @param The element type of the result list + * @param ts ts non-null immutable list. + * @param function a non-interfering, stateless function to apply to each element + * @return the mapped list of the same length as this + */ + public static ImmutableList map(ImmutableList ts, Function function) { + // This must be a loop. A tail recursive implementation is not optimised + // by the compiler and quickly leads to a stack overlow. + ImmutableList acc = ImmutableSLList.nil(); + while(ts.size() > 0) { + T hd = ts.head(); + acc = acc.prepend(function.apply(hd)); + ts = ts.tail(); + } + return acc.reverse(); + } } diff --git a/key.util/src/test/java/org/key_project/util/collection/TestImmutables.java b/key.util/src/test/java/org/key_project/util/collection/TestImmutables.java index cf52f5d14ce..bcfa6b8aff3 100644 --- a/key.util/src/test/java/org/key_project/util/collection/TestImmutables.java +++ b/key.util/src/test/java/org/key_project/util/collection/TestImmutables.java @@ -155,4 +155,59 @@ public void testHashCodes() { assertEquals(hash1, hash2); } + @Test + public void testFilter() { + ImmutableList l = ImmutableList.of(1,2,3,4,5,6,7,8,9); + ImmutableList filtered = Immutables.filter(l, n -> n % 2 == 0); + assertEquals(ImmutableList.of(2,4,6,8), filtered); + } + + @Test + public void testFilterStackoverflow() { + // With the original tail recursive implementation, this would give + // an overflow --> made it a loop. + ImmutableList l = ImmutableSLList.nil(); + for (int i = 0; i < 1_000_000; i++) { + l = l.prepend(i); + } + + ImmutableList filtered = Immutables.filter(l, n -> n % 2 == 0); + assertEquals(500_000, filtered.size()); + } + + @Test + public void testMap() { + ImmutableList l = ImmutableList.of(1,2,3,4); + ImmutableList mapped = Immutables.map(l, n -> n % 2 == 0); + assertEquals(ImmutableList.of(false, true, false, true), mapped); + } + + @Test + public void testMapStackoverflow() { + // With the original tail recursive implementation, this would give + // an overflow --> made it a loop. + ImmutableList l = ImmutableSLList.nil(); + for (int i = 0; i < 1_000_000; i++) { + l = l.prepend(i); + } + + ImmutableList mapped = Immutables.map(l, n -> n % 2 == 0); + assertEquals(1_000_000, mapped.size()); + } + + @Test + public void testExistsStackoverflow() { + // With a tail recursive implementation, this would give + // an overflow --> it is a loop. + ImmutableList l = ImmutableSLList.nil(); + for (int i = 0; i < 1_000_000; i++) { + l = l.prepend(i); + } + + boolean result = l.exists(x -> x == 999_998); + assertTrue(result); + result = l.exists(x -> x == 1_999_998); + assertFalse(result); + } + } From c040d95a5f74647441ddda4a09bcd65611510b34 Mon Sep 17 00:00:00 2001 From: Mattias Ulbrich Date: Sun, 5 Feb 2023 13:04:28 +0100 Subject: [PATCH 2/4] small fixes and improvements to proof scripts --- .../ilkd/key/macros/scripts/EngineState.java | 4 +- .../ilkd/key/macros/scripts/FocusCommand.java | 126 ++++++++++ .../FocusOnSelectionAndHideCommand.java | 229 ------------------ .../macros/scripts/meta/ValueInjector.java | 2 +- .../java/de/uka/ilkd/key/nparser/KeyIO.java | 3 +- .../ilkd/key/parser/DefaultTermParser.java | 3 +- .../key/proof/io/OutputStreamProofSaver.java | 6 +- ...ilkd.key.macros.scripts.ProofScriptCommand | 2 +- .../key/macros/scripts/FocusCommandTest.java | 59 +++++ 9 files changed, 199 insertions(+), 235 deletions(-) create mode 100644 key.core/src/main/java/de/uka/ilkd/key/macros/scripts/FocusCommand.java delete mode 100644 key.core/src/main/java/de/uka/ilkd/key/macros/scripts/FocusOnSelectionAndHideCommand.java create mode 100644 key.core/src/test/java/de/uka/ilkd/key/macros/scripts/FocusCommandTest.java diff --git a/key.core/src/main/java/de/uka/ilkd/key/macros/scripts/EngineState.java b/key.core/src/main/java/de/uka/ilkd/key/macros/scripts/EngineState.java index f1e8411b5a1..835c51790f2 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/macros/scripts/EngineState.java +++ b/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"); } diff --git a/key.core/src/main/java/de/uka/ilkd/key/macros/scripts/FocusCommand.java b/key.core/src/main/java/de/uka/ilkd/key/macros/scripts/FocusCommand.java new file mode 100644 index 00000000000..3986b84b495 --- /dev/null +++ b/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 { + + 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 keepAnte = toKeep.antecedent().asList().map(SequentFormula::formula); + ImmutableList 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 keepSucc = toKeep.succedent().asList().map(SequentFormula::formula); + ImmutableList 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 svs = tac.collectSchemaVars(); + assert svs.size() == 1; + Iterator 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); + + } + +} + diff --git a/key.core/src/main/java/de/uka/ilkd/key/macros/scripts/FocusOnSelectionAndHideCommand.java b/key.core/src/main/java/de/uka/ilkd/key/macros/scripts/FocusOnSelectionAndHideCommand.java deleted file mode 100644 index 9a04eb43ae2..00000000000 --- a/key.core/src/main/java/de/uka/ilkd/key/macros/scripts/FocusOnSelectionAndHideCommand.java +++ /dev/null @@ -1,229 +0,0 @@ -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.parser.ParserException; -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 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 FocusOnSelectionAndHideCommand - extends AbstractCommand { - - public FocusOnSelectionAndHideCommand() { - 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()); - try { - hideAll(toKeep); - } catch (ParserException e) { - e.printStackTrace(); - } - - } - - @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 focus sequent - * - * @param toKeep - * @throws ParserException - * @throws ScriptException - */ - private void hideAll(Sequent toKeep) throws ParserException, ScriptException { - while (true) { - // get current goal - Goal g = state.getFirstOpenAutomaticGoal(); - // find formulas that should be hidden in sequent of current goal - - // hide - - if (g != null) { - - SequentFormula toHide = iterateThroughSequentAndFindNonMatch(g, toKeep); - // as long as there is a match - if (toHide != null) { - boolean antec = false; - - Taclet tac; - if (g.sequent().antecedent().contains(toHide)) { - tac = getTaclet(toHide.formula(), "left"); - antec = true; - - } else { - tac = getTaclet(toHide.formula(), "right"); - - } - makeTacletApp(g, toHide, tac, antec); - - } else { - // no formulas to hide any more on sequent - break; - } - - } else { - // goal is null - break; - } - } - - } - - // determine where formula in sequent and apply either hide_left or hide_right - private Taclet getTaclet(Term t, String pos) throws ScriptException { - String ruleName; - Taclet tac; - switch (pos) { - case "left": - ruleName = "hide_left"; - break; - case "right": - ruleName = "hide_right"; - break; - default: - ruleName = ""; - throw new ScriptException("Position of term " + t.toString() + "unknown"); - } - - tac = proof.getEnv().getInitConfigForEnvironment().lookupActiveTaclet(new Name(ruleName)); - - return tac; - - } - - /** - * Iterate through sequent and find first formula that is not in the list of formulas to keep - * and return this formula - * - * @param g - * @param toKeep - * @return formula to hide, if all formulas in the sequent should be kept, returns null - * @throws ScriptException - * @throws ParserException - */ - - private SequentFormula iterateThroughSequentAndFindNonMatch(Goal g, Sequent toKeep) - throws ScriptException, ParserException { - Semisequent focusedAntec = toKeep.antecedent(); - Semisequent focusedSucc = toKeep.succedent(); - - Sequent currentGoalSeq = g.sequent(); - Semisequent currentAntec = currentGoalSeq.antecedent(); - Semisequent currentSucc = currentGoalSeq.succedent(); - - // first iterate through antecedent - Iterator iterator = currentAntec.iterator(); - while (iterator.hasNext()) { - SequentFormula form = iterator.next(); - Iterator focusAntecIter = focusedAntec.iterator(); - - Boolean isIn = false; - while (focusAntecIter.hasNext()) { - SequentFormula toKeepForm = focusAntecIter.next(); - if (toKeepForm.equals(form)) { - isIn = true; - break; - } - } - - /* - * if(form.formula().equalsModRenaming(t) ){ isIn = true; } - */ - - if (!isIn) { - return form; - } - } - // if in antecedent no formula to hide iterate through succedent - Iterator iteratorSucc = currentSucc.iterator(); - - while (iteratorSucc.hasNext()) { - Boolean isIn = false; - SequentFormula form = iteratorSucc.next(); - Iterator focusSuccIter = focusedSucc.iterator(); - - while (focusSuccIter.hasNext()) { - SequentFormula toKeepForm = focusSuccIter.next(); - if (toKeepForm.equals(form)) { - isIn = true; - break; - } - } - if (!isIn) { - return form; - } - } - // if no formulas to hide, return null - return null; - } - - /** - * 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 - * @throws ScriptException - */ - private void makeTacletApp(Goal g, SequentFormula toHide, Taclet tac, boolean antec) - throws ScriptException { - - // hide rules only applicable to top-level terms/sequent formulas - PosInTerm pit = PosInTerm.getTopLevel(); - - PosInOccurrence pio = new PosInOccurrence(toHide, pit, antec); - - Set svs = tac.collectSchemaVars(); - assert svs.size() == 1; - Iterator 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); - - } - -} - diff --git a/key.core/src/main/java/de/uka/ilkd/key/macros/scripts/meta/ValueInjector.java b/key.core/src/main/java/de/uka/ilkd/key/macros/scripts/meta/ValueInjector.java index c0cc1df3b2c..73fa0685794 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/macros/scripts/meta/ValueInjector.java +++ b/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); } } diff --git a/key.core/src/main/java/de/uka/ilkd/key/nparser/KeyIO.java b/key.core/src/main/java/de/uka/ilkd/key/nparser/KeyIO.java index 6127e0493de..6319ba60d60 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/nparser/KeyIO.java +++ b/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); diff --git a/key.core/src/main/java/de/uka/ilkd/key/parser/DefaultTermParser.java b/key.core/src/main/java/de/uka/ilkd/key/parser/DefaultTermParser.java index 21a70c2736c..45c0d448d57 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/parser/DefaultTermParser.java +++ b/key.core/src/main/java/de/uka/ilkd/key/parser/DefaultTermParser.java @@ -85,8 +85,9 @@ public Term parse(Reader in, Sort sort, Services services, NamespaceSet nss, Abb public Sequent parseSeq(Reader in, Services services, NamespaceSet nss, AbbrevMap scm) throws ParserException { KeyIO keyIO = new KeyIO(services, nss); + keyIO.setAbbrevMap(scm); try { - final Sequent seq = keyIO.parseSequence(CharStreams.fromReader(in)); + final Sequent seq = keyIO.parseSequent(CharStreams.fromReader(in)); // p = new KeYParserF(ParserMode.TERM, new KeYLexerF(in, ""), new Recoder2KeY(services, // nss), services, nss, scm); return seq; diff --git a/key.core/src/main/java/de/uka/ilkd/key/proof/io/OutputStreamProofSaver.java b/key.core/src/main/java/de/uka/ilkd/key/proof/io/OutputStreamProofSaver.java index 74bf38421d0..e3c9b563f15 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/proof/io/OutputStreamProofSaver.java +++ b/key.core/src/main/java/de/uka/ilkd/key/proof/io/OutputStreamProofSaver.java @@ -798,7 +798,11 @@ public static StringBuffer printAnything(Object val, Services services, private static StringBuffer printSequent(Sequent val, Services services) { final LogicPrinter printer = createLogicPrinter(services, services == null); printer.printSequent(val); - return printer.result(); + StringBuffer result = printer.result(); + if (result.charAt(result.length() - 1) == '\n') { + result.deleteCharAt(result.length() - 1); + } + return result; } private static LogicPrinter createLogicPrinter(Services serv, boolean shortAttrNotation) { diff --git a/key.core/src/main/resources/META-INF/services/de.uka.ilkd.key.macros.scripts.ProofScriptCommand b/key.core/src/main/resources/META-INF/services/de.uka.ilkd.key.macros.scripts.ProofScriptCommand index f244214c860..3cac23e7e25 100644 --- a/key.core/src/main/resources/META-INF/services/de.uka.ilkd.key.macros.scripts.ProofScriptCommand +++ b/key.core/src/main/resources/META-INF/services/de.uka.ilkd.key.macros.scripts.ProofScriptCommand @@ -4,7 +4,7 @@ de.uka.ilkd.key.macros.scripts.EchoCommand de.uka.ilkd.key.macros.scripts.MacroCommand -de.uka.ilkd.key.macros.scripts.FocusOnSelectionAndHideCommand +de.uka.ilkd.key.macros.scripts.FocusCommand de.uka.ilkd.key.macros.scripts.AutoCommand de.uka.ilkd.key.macros.scripts.CutCommand de.uka.ilkd.key.macros.scripts.SetCommand diff --git a/key.core/src/test/java/de/uka/ilkd/key/macros/scripts/FocusCommandTest.java b/key.core/src/test/java/de/uka/ilkd/key/macros/scripts/FocusCommandTest.java new file mode 100644 index 00000000000..d0a15e80694 --- /dev/null +++ b/key.core/src/test/java/de/uka/ilkd/key/macros/scripts/FocusCommandTest.java @@ -0,0 +1,59 @@ +package de.uka.ilkd.key.macros.scripts; + +import de.uka.ilkd.key.control.DefaultUserInterfaceControl; +import de.uka.ilkd.key.control.KeYEnvironment; +import de.uka.ilkd.key.parser.Location; +import de.uka.ilkd.key.proof.Goal; +import de.uka.ilkd.key.proof.Proof; +import de.uka.ilkd.key.proof.io.ProofSaver; +import org.junit.jupiter.api.Test; + +import java.net.URL; +import java.nio.file.Files; +import java.nio.file.Path; + +import static org.junit.jupiter.api.Assertions.assertEquals; + +/** + * @author Alexander Weigl + * @version 1 (17.10.19) + */ +public class FocusCommandTest { + @Test + public void testSimpleSelection() throws Exception { + Path temp = Files.createTempFile("key-focus-command", ".key"); + Files.writeString(temp, "\\functions { int i; } \\problem { i=1&i=2 -> i=3|i=4 }" + + "\\proofScript \"prop-simp; \""); + KeYEnvironment env = KeYEnvironment.load(temp.toFile()); + Proof p = env.getLoadedProof(); + ProofScriptEngine pse = new ProofScriptEngine( + "macro 'nosplit-prop'; focus 'i=1 ==> i = 4';", new Location((URL) null, 0, 0)); + pse.execute(env.getUi(), p); + + assertEquals(1, p.openGoals().size()); + Goal g = p.openGoals().head(); + assertEquals("i = Z(1(#)) ==> i = Z(4(#))", + ProofSaver.printAnything(g.sequent(), env.getServices())); + } + + @Test + public void testSelectionWithLabels() throws Exception { + Path temp = Files.createTempFile("key-focus-command", ".key"); + Files.writeString(temp, + "\\functions { int i; } \\problem { i=1<> -> i=(3< (implicit)\", \"[]\")>>) }" + + + "\\proofScript \"prop-simp; \""); + + KeYEnvironment env = KeYEnvironment.load(temp.toFile()); + Proof p = env.getLoadedProof(); + ProofScriptEngine pse = new ProofScriptEngine( + "macro 'nosplit-prop'; focus 'i=1 ==> i = 3';", new Location((URL) null, 0, 0)); + pse.execute(env.getUi(), p); + + assertEquals(1, p.openGoals().size()); + Goal g = p.openGoals().head(); + assertEquals("i = Z(1(#))<> ==> i = Z(3(#))", + ProofSaver.printAnything(g.sequent(), env.getServices())); + } + +} From 560d4e1882a997736bed35f4e0e0fba77b7134f0 Mon Sep 17 00:00:00 2001 From: Mattias Ulbrich Date: Sun, 5 Feb 2023 13:16:11 +0100 Subject: [PATCH 3/4] applying spotless --- .../key_project/util/collection/ImmutableList.java | 7 ++++--- .../org/key_project/util/collection/Immutables.java | 11 +++++++---- .../key_project/util/collection/TestImmutables.java | 6 +++--- 3 files changed, 14 insertions(+), 10 deletions(-) diff --git a/key.util/src/main/java/org/key_project/util/collection/ImmutableList.java b/key.util/src/main/java/org/key_project/util/collection/ImmutableList.java index abf764c46e1..59f5a43da0b 100644 --- a/key.util/src/main/java/org/key_project/util/collection/ImmutableList.java +++ b/key.util/src/main/java/org/key_project/util/collection/ImmutableList.java @@ -99,7 +99,7 @@ public static ImmutableList of(T e1, T e2, T e3) { */ public static ImmutableList of(T... es) { ImmutableList result = ImmutableSLList.nil(); - for (int i = es.length-1; i >= 0; i--) { + for (int i = es.length - 1; i >= 0; i--) { result = result.prepend(es[i]); } return result; @@ -279,8 +279,9 @@ default List toList() { * the given predicate. * * @param predicate a non-interfering, stateless - * predicate to apply to each element to determine if it - * should be included + * predicate to apply to each element to determine if it + * should be included + * * @returns the filtered list */ default @Nonnull ImmutableList filter(@Nonnull Predicate predicate) { diff --git a/key.util/src/main/java/org/key_project/util/collection/Immutables.java b/key.util/src/main/java/org/key_project/util/collection/Immutables.java index f853c08b4b0..440fc8d0f2c 100644 --- a/key.util/src/main/java/org/key_project/util/collection/Immutables.java +++ b/key.util/src/main/java/org/key_project/util/collection/Immutables.java @@ -141,6 +141,7 @@ public static ImmutableSet createSetFrom(Iterable iterable) { * * @param iterable the collection to iterate through to obtain the elements * for the resulting list + * * @returns the view onto the iterable as an immutable list */ public static ImmutableList createListFrom(Iterable iterable) { @@ -156,16 +157,18 @@ public static ImmutableList createListFrom(Iterable iterable) { * the given predicate. * * @param ts non-null immutable list. + * * @param predicate a non-interfering, stateless - * predicate to apply to each element to determine if it - * should be included + * predicate to apply to each element to determine if it + * should be included + * * @returns the filtered list */ public static ImmutableList filter(ImmutableList ts, Predicate predicate) { // This must be a loop. A tail recursive implementation is not optimised // by the compiler and quickly leads to a stack overlow. ImmutableList acc = ImmutableSLList.nil(); - while(ts.size() > 0) { + while (ts.size() > 0) { T hd = ts.head(); if (predicate.test(hd)) { acc = acc.prepend(hd); @@ -188,7 +191,7 @@ public static ImmutableList map(ImmutableList ts, Function fu // This must be a loop. A tail recursive implementation is not optimised // by the compiler and quickly leads to a stack overlow. ImmutableList acc = ImmutableSLList.nil(); - while(ts.size() > 0) { + while (ts.size() > 0) { T hd = ts.head(); acc = acc.prepend(function.apply(hd)); ts = ts.tail(); diff --git a/key.util/src/test/java/org/key_project/util/collection/TestImmutables.java b/key.util/src/test/java/org/key_project/util/collection/TestImmutables.java index bcfa6b8aff3..79862758b42 100644 --- a/key.util/src/test/java/org/key_project/util/collection/TestImmutables.java +++ b/key.util/src/test/java/org/key_project/util/collection/TestImmutables.java @@ -157,9 +157,9 @@ public void testHashCodes() { @Test public void testFilter() { - ImmutableList l = ImmutableList.of(1,2,3,4,5,6,7,8,9); + ImmutableList l = ImmutableList.of(1, 2, 3, 4, 5, 6, 7, 8, 9); ImmutableList filtered = Immutables.filter(l, n -> n % 2 == 0); - assertEquals(ImmutableList.of(2,4,6,8), filtered); + assertEquals(ImmutableList.of(2, 4, 6, 8), filtered); } @Test @@ -177,7 +177,7 @@ public void testFilterStackoverflow() { @Test public void testMap() { - ImmutableList l = ImmutableList.of(1,2,3,4); + ImmutableList l = ImmutableList.of(1, 2, 3, 4); ImmutableList mapped = Immutables.map(l, n -> n % 2 == 0); assertEquals(ImmutableList.of(false, true, false, true), mapped); } From e50e9f0e906a7b4e35fbcaa786511173579b7644 Mon Sep 17 00:00:00 2001 From: Mattias Ulbrich Date: Tue, 7 Feb 2023 09:58:31 +0100 Subject: [PATCH 4/4] improving javadoc, removing old code. --- .../ilkd/key/macros/scripts/FocusCommand.java | 24 +++++++++---------- 1 file changed, 12 insertions(+), 12 deletions(-) diff --git a/key.core/src/main/java/de/uka/ilkd/key/macros/scripts/FocusCommand.java b/key.core/src/main/java/de/uka/ilkd/key/macros/scripts/FocusCommand.java index 3986b84b495..19673020e42 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/macros/scripts/FocusCommand.java +++ b/key.core/src/main/java/de/uka/ilkd/key/macros/scripts/FocusCommand.java @@ -15,8 +15,18 @@ 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. + * The command "focus" allows you to select formulas from the current sequent + * to focus verification on. This means that all other formulas are discarded + * (i.e. hidden using hide_right, hide_left). + * + * Benefits are: The automation is guided into focussing on a relevant set of + * formulas. + * + * The selected set of sequent formulas can be regarded as an equivalent to an + * unsat core. + * + * @author Created by sarah on 1/12/17. + * @author Mattias Ulbrich, 2023 */ public class FocusCommand extends AbstractCommand { @@ -37,9 +47,7 @@ public void execute(Parameters s) throws ScriptException, InterruptedException { Sequent toKeep = s.toKeep; - // toKeep = parseSequent(sequentString, getGoalFromCurrentState()); hideAll(toKeep); - } @Override @@ -47,14 +55,6 @@ 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 *