diff --git a/key.core/src/main/java/de/uka/ilkd/key/control/KeYEnvironment.java b/key.core/src/main/java/de/uka/ilkd/key/control/KeYEnvironment.java index 4835d68e9d8..01f3aa1e095 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/control/KeYEnvironment.java +++ b/key.core/src/main/java/de/uka/ilkd/key/control/KeYEnvironment.java @@ -11,6 +11,7 @@ import de.uka.ilkd.key.java.JavaInfo; import de.uka.ilkd.key.java.Services; import de.uka.ilkd.key.nparser.KeyAst; +import de.uka.ilkd.key.nparser.KeyAst.ProofScript; import de.uka.ilkd.key.proof.Proof; import de.uka.ilkd.key.proof.init.InitConfig; import de.uka.ilkd.key.proof.init.Profile; @@ -48,7 +49,7 @@ public class KeYEnvironment { /** * An optional field denoting a script contained in the proof file. */ - private final KeyAst.@Nullable ProofScript proofScript; + private final @Nullable ProofScript proofScript; /** * Indicates that this {@link KeYEnvironment} is disposed. @@ -78,7 +79,7 @@ public KeYEnvironment(U ui, InitConfig initConfig) { * @param proofScript add an optional proof script */ public KeYEnvironment(U ui, InitConfig initConfig, Proof loadedProof, - KeyAst.@Nullable ProofScript proofScript, ReplayResult replayResult) { + @Nullable ProofScript proofScript, ReplayResult replayResult) { this.ui = ui; this.initConfig = initConfig; this.loadedProof = loadedProof; @@ -322,7 +323,7 @@ public boolean isDisposed() { return disposed; } - public KeyAst.@Nullable ProofScript getProofScript() { + public @Nullable ProofScript getProofScript() { return proofScript; } } diff --git a/key.core/src/main/java/de/uka/ilkd/key/macros/scripts/AbstractCommand.java b/key.core/src/main/java/de/uka/ilkd/key/macros/scripts/AbstractCommand.java index 7eea7692550..b056819bb9b 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/macros/scripts/AbstractCommand.java +++ b/key.core/src/main/java/de/uka/ilkd/key/macros/scripts/AbstractCommand.java @@ -10,7 +10,6 @@ import de.uka.ilkd.key.control.AbstractUserInterfaceControl; import de.uka.ilkd.key.java.Services; import de.uka.ilkd.key.macros.scripts.meta.ArgumentsLifter; -import de.uka.ilkd.key.macros.scripts.meta.DescriptionFacade; import de.uka.ilkd.key.macros.scripts.meta.ProofScriptArgument; import de.uka.ilkd.key.proof.Proof; @@ -82,18 +81,10 @@ public void execute(AbstractUserInterfaceControl uiControl, T args, EngineState * @throws ScriptException * @throws InterruptedException */ - protected void execute(T args) throws ScriptException, InterruptedException { + protected void execute(T args) throws ScriptException, InterruptedException {} - } - - /** - * {@inheritDoc} - */ @Override public String getDocumentation() { - if (documentation == null) { - documentation = DescriptionFacade.getDocumentation(this); - } - return documentation; + return ""; } } diff --git a/key.core/src/main/java/de/uka/ilkd/key/macros/scripts/ActivateCommand.java b/key.core/src/main/java/de/uka/ilkd/key/macros/scripts/ActivateCommand.java index d8df0e3d1d2..480feb82a09 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/macros/scripts/ActivateCommand.java +++ b/key.core/src/main/java/de/uka/ilkd/key/macros/scripts/ActivateCommand.java @@ -19,6 +19,11 @@ public String getName() { return "activate"; } + @Override + public String getDocumentation() { + return ""; + } + @Override public void execute(AbstractUserInterfaceControl uiControl, Void args, EngineState state) throws ScriptException, InterruptedException { diff --git a/key.core/src/main/java/de/uka/ilkd/key/macros/scripts/AllCommand.java b/key.core/src/main/java/de/uka/ilkd/key/macros/scripts/AllCommand.java index e90f0c24f5d..f452d9c290e 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/macros/scripts/AllCommand.java +++ b/key.core/src/main/java/de/uka/ilkd/key/macros/scripts/AllCommand.java @@ -7,7 +7,6 @@ import java.util.Map; import de.uka.ilkd.key.control.AbstractUserInterfaceControl; -import de.uka.ilkd.key.macros.scripts.meta.DescriptionFacade; import de.uka.ilkd.key.macros.scripts.meta.ProofScriptArgument; import de.uka.ilkd.key.nparser.KeYParser; import de.uka.ilkd.key.proof.Goal; @@ -56,9 +55,7 @@ public String getName() { */ @Override public String getDocumentation() { - if (documentation == null) { - documentation = DescriptionFacade.getDocumentation(this); - } - return documentation; + return """ + Applies the given command to all the open goals."""; } } diff --git a/key.core/src/main/java/de/uka/ilkd/key/macros/scripts/AssumeCommand.java b/key.core/src/main/java/de/uka/ilkd/key/macros/scripts/AssumeCommand.java index 4f27f1137d4..5a1a0f962b2 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/macros/scripts/AssumeCommand.java +++ b/key.core/src/main/java/de/uka/ilkd/key/macros/scripts/AssumeCommand.java @@ -3,17 +3,16 @@ * SPDX-License-Identifier: GPL-2.0-only */ package de.uka.ilkd.key.macros.scripts; -import java.util.Map; - import de.uka.ilkd.key.logic.Term; import de.uka.ilkd.key.logic.op.SchemaVariable; import de.uka.ilkd.key.macros.scripts.meta.Option; import de.uka.ilkd.key.rule.NoPosTacletApp; import de.uka.ilkd.key.rule.Taclet; import de.uka.ilkd.key.rule.TacletApp; - import org.key_project.logic.Name; +import java.util.Map; + /** * The assume command takes one argument: * a formula to which the command is applied */ @@ -26,7 +25,7 @@ public AssumeCommand() { @Override public FormulaParameter evaluateArguments(EngineState state, - Map arguments) + Map arguments) throws Exception { return state.getValueInjector().inject(this, new FormulaParameter(), arguments); } @@ -36,15 +35,24 @@ public String getName() { return "assume"; } + @Override + public String getDocumentation() { + return """ + The assume command is an unsound taclet rule and takes one argument: + + The command adds the formula passed as argument to the antecedent + a formula #2 to which the command is applied"""; + } + @Override public void execute(FormulaParameter parameter) throws ScriptException, InterruptedException { Taclet cut = - state.getProof().getEnv().getInitConfigForEnvironment().lookupActiveTaclet(TACLET_NAME); + state.getProof().getEnv().getInitConfigForEnvironment().lookupActiveTaclet(TACLET_NAME); TacletApp app = NoPosTacletApp.createNoPosTacletApp(cut); SchemaVariable sv = app.uninstantiatedVars().iterator().next(); app = app.addCheckedInstantiation(sv, parameter.formula, state.getProof().getServices(), - true); + true); state.getFirstOpenAutomaticGoal().apply(app); } diff --git a/key.core/src/main/java/de/uka/ilkd/key/macros/scripts/AutoCommand.java b/key.core/src/main/java/de/uka/ilkd/key/macros/scripts/AutoCommand.java index d52aa0102d4..653d014a7f3 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/macros/scripts/AutoCommand.java +++ b/key.core/src/main/java/de/uka/ilkd/key/macros/scripts/AutoCommand.java @@ -38,6 +38,11 @@ public String getName() { return "auto"; } + @Override + public String getDocumentation() { + return "The AutoCommand invokes the automatic strategy \"Auto\""; + } + @Override public Parameters evaluateArguments(EngineState state, Map arguments) throws ConversionException, ArgumentRequiredException, InjectionReflectionException, diff --git a/key.core/src/main/java/de/uka/ilkd/key/macros/scripts/CutCommand.java b/key.core/src/main/java/de/uka/ilkd/key/macros/scripts/CutCommand.java index e9f0c717cf2..975fa8e290a 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/macros/scripts/CutCommand.java +++ b/key.core/src/main/java/de/uka/ilkd/key/macros/scripts/CutCommand.java @@ -3,8 +3,6 @@ * SPDX-License-Identifier: GPL-2.0-only */ package de.uka.ilkd.key.macros.scripts; -import java.util.Map; - import de.uka.ilkd.key.control.AbstractUserInterfaceControl; import de.uka.ilkd.key.logic.Term; import de.uka.ilkd.key.logic.op.SchemaVariable; @@ -12,9 +10,10 @@ import de.uka.ilkd.key.rule.NoPosTacletApp; import de.uka.ilkd.key.rule.Taclet; import de.uka.ilkd.key.rule.TacletApp; - import org.key_project.logic.Name; +import java.util.Map; + /** * The command object CutCommand has as scriptcommand name "cut" As parameters: a formula with the * id "#2" @@ -31,15 +30,23 @@ public String getName() { return "cut"; } + @Override + public String getDocumentation() { + return """ + CutCommand has as script command name "cut" + + As parameters: + * a formula with the id "#2"""; + } + @Override public Parameters evaluateArguments(EngineState state, - Map arguments) + Map arguments) throws Exception { return state.getValueInjector().inject(this, new Parameters(), arguments); } /** - * * @param uiControl * @param args * @param state diff --git a/key.core/src/main/java/de/uka/ilkd/key/macros/scripts/ExitCommand.java b/key.core/src/main/java/de/uka/ilkd/key/macros/scripts/ExitCommand.java index 071cb6dbb30..aa57c484075 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/macros/scripts/ExitCommand.java +++ b/key.core/src/main/java/de/uka/ilkd/key/macros/scripts/ExitCommand.java @@ -18,4 +18,9 @@ public void execute(AbstractUserInterfaceControl uiControl, Void args, EngineSta public String getName() { return "exit"; } + + @Override + public String getDocumentation() { + return "Kills the script execution."; + } } diff --git a/key.core/src/main/java/de/uka/ilkd/key/macros/scripts/InstantiateCommand.java b/key.core/src/main/java/de/uka/ilkd/key/macros/scripts/InstantiateCommand.java index f94b7f187ea..c685cf965ea 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/macros/scripts/InstantiateCommand.java +++ b/key.core/src/main/java/de/uka/ilkd/key/macros/scripts/InstantiateCommand.java @@ -3,8 +3,6 @@ * SPDX-License-Identifier: GPL-2.0-only */ package de.uka.ilkd.key.macros.scripts; -import java.util.Map; - import de.uka.ilkd.key.control.AbstractUserInterfaceControl; import de.uka.ilkd.key.java.Services; import de.uka.ilkd.key.logic.*; @@ -20,11 +18,12 @@ import de.uka.ilkd.key.rule.PosTacletApp; import de.uka.ilkd.key.rule.Taclet; import de.uka.ilkd.key.rule.TacletApp; - import org.key_project.logic.Name; import org.key_project.util.collection.ImmutableList; import org.key_project.util.collection.ImmutableSLList; +import java.util.Map; + import static de.uka.ilkd.key.logic.equality.RenamingTermProperty.RENAMING_TERM_PROPERTY; /** @@ -42,14 +41,14 @@ public InstantiateCommand() { @Override public Parameters evaluateArguments(EngineState state, - Map arguments) + Map arguments) throws Exception { return state.getValueInjector().inject(this, new Parameters(), arguments); } @Override public void execute(AbstractUserInterfaceControl uiControl, Parameters params, - EngineState state) throws ScriptException, InterruptedException { + EngineState state) throws ScriptException, InterruptedException { Goal goal = state.getFirstOpenAutomaticGoal(); @@ -71,7 +70,7 @@ public void execute(AbstractUserInterfaceControl uiControl, Parameters params, SchemaVariable sv = theApp.uninstantiatedVars().iterator().next(); theApp = theApp.addInstantiation(sv, params.with, true /* ??? */, - state.getProof().getServices()); + state.getProof().getServices()); theApp = theApp.tryToInstantiate(state.getProof().getServices()); @@ -116,7 +115,7 @@ private ImmutableList findAllTacletApps(Parameters p, EngineState sta continue; } allApps = allApps.append(index.getTacletAppAtAndBelow(filter, - new PosInOccurrence(sf, PosInTerm.getTopLevel(), true), services)); + new PosInOccurrence(sf, PosInTerm.getTopLevel(), true), services)); } for (SequentFormula sf : g.node().sequent().succedent()) { @@ -125,7 +124,7 @@ private ImmutableList findAllTacletApps(Parameters p, EngineState sta continue; } allApps = allApps.append(index.getTacletAppAtAndBelow(filter, - new PosInOccurrence(sf, PosInTerm.getTopLevel(), false), services)); + new PosInOccurrence(sf, PosInTerm.getTopLevel(), false), services)); } return allApps; @@ -138,7 +137,7 @@ private TacletApp filterList(Parameters p, ImmutableList list) { for (TacletApp tacletApp : list) { if (tacletApp instanceof PosTacletApp pta) { if (pta.posInOccurrence().subTerm().equalsModProperty(p.formula, - RENAMING_TERM_PROPERTY)) { + RENAMING_TERM_PROPERTY)) { return pta; } } @@ -181,7 +180,7 @@ private void computeFormula(Parameters params, Goal goal) throws ScriptException } throw new ScriptException( - "Variable '" + params.var + "' has no occurrence no. '" + params.occ + "'."); + "Variable '" + params.var + "' has no occurrence no. '" + params.occ + "'."); } private Term stripUpdates(Term term) { @@ -219,6 +218,15 @@ public String getName() { return "instantiate"; } + @Override + public String getDocumentation() { + return """ + instantiate var=a occ=2 with="a_8" hide +

+ instantiate formula="\\forall int a; phi(a)" with="a_8\" + """; + } + /** * */ diff --git a/key.core/src/main/java/de/uka/ilkd/key/macros/scripts/LeaveCommand.java b/key.core/src/main/java/de/uka/ilkd/key/macros/scripts/LeaveCommand.java index 5815bf6533f..45166cbe52a 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/macros/scripts/LeaveCommand.java +++ b/key.core/src/main/java/de/uka/ilkd/key/macros/scripts/LeaveCommand.java @@ -17,6 +17,11 @@ public String getName() { return "leave"; } + @Override + public String getDocumentation() { + return "Marks the current goal to be ignored by the macros."; + } + @Override public void execute(AbstractUserInterfaceControl uiControl, Void args, EngineState state) throws ScriptException, InterruptedException { diff --git a/key.core/src/main/java/de/uka/ilkd/key/macros/scripts/LetCommand.java b/key.core/src/main/java/de/uka/ilkd/key/macros/scripts/LetCommand.java index b53a402846c..e69852908f8 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/macros/scripts/LetCommand.java +++ b/key.core/src/main/java/de/uka/ilkd/key/macros/scripts/LetCommand.java @@ -38,7 +38,7 @@ public void execute(AbstractUserInterfaceControl uiControl, Map for (Map.Entry entry : args.entrySet()) { String key = entry.getKey(); - if (key.startsWith("#") && key.equals("force")) { + if (key.startsWith("#") || key.equals("force")) { continue; } diff --git a/key.core/src/main/java/de/uka/ilkd/key/macros/scripts/NoArgumentCommand.java b/key.core/src/main/java/de/uka/ilkd/key/macros/scripts/NoArgumentCommand.java index 45827ebace6..18ceacd1c1d 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/macros/scripts/NoArgumentCommand.java +++ b/key.core/src/main/java/de/uka/ilkd/key/macros/scripts/NoArgumentCommand.java @@ -7,7 +7,6 @@ import java.util.List; import java.util.Map; -import de.uka.ilkd.key.macros.scripts.meta.DescriptionFacade; import de.uka.ilkd.key.macros.scripts.meta.ProofScriptArgument; /** @@ -25,9 +24,4 @@ public Void evaluateArguments(EngineState state, Map arguments) { return null; } - - @Override - public String getDocumentation() { - return DescriptionFacade.getDocumentation(this); - } } diff --git a/key.core/src/main/java/de/uka/ilkd/key/macros/scripts/RuleCommand.java b/key.core/src/main/java/de/uka/ilkd/key/macros/scripts/RuleCommand.java index dbca1f2d780..a528233673f 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/macros/scripts/RuleCommand.java +++ b/key.core/src/main/java/de/uka/ilkd/key/macros/scripts/RuleCommand.java @@ -3,11 +3,12 @@ * SPDX-License-Identifier: GPL-2.0-only */ package de.uka.ilkd.key.macros.scripts; -import java.util.*; - import de.uka.ilkd.key.control.AbstractUserInterfaceControl; import de.uka.ilkd.key.java.Services; -import de.uka.ilkd.key.logic.*; +import de.uka.ilkd.key.logic.PosInOccurrence; +import de.uka.ilkd.key.logic.PosInTerm; +import de.uka.ilkd.key.logic.SequentFormula; +import de.uka.ilkd.key.logic.Term; import de.uka.ilkd.key.logic.op.SchemaVariable; import de.uka.ilkd.key.macros.scripts.meta.Option; import de.uka.ilkd.key.macros.scripts.meta.Varargs; @@ -18,11 +19,12 @@ import de.uka.ilkd.key.proof.RuleAppIndex; import de.uka.ilkd.key.proof.rulefilter.TacletFilter; import de.uka.ilkd.key.rule.*; - import org.key_project.logic.Name; import org.key_project.util.collection.ImmutableList; import org.key_project.util.collection.ImmutableSLList; +import java.util.*; + import static de.uka.ilkd.key.logic.equality.IrrelevantTermLabelsProperty.IRRELEVANT_TERM_LABELS_PROPERTY; import static de.uka.ilkd.key.logic.equality.RenamingTermProperty.RENAMING_TERM_PROPERTY; @@ -49,9 +51,26 @@ public String getName() { return "rule"; } + @Override + public String getDocumentation() { + return """ + Command that applies a calculus rule. + All parameters are passed as strings and converted by the command. + + The parameters are: +

    +
  1. #2 = rule name
    2. +
  2. on= key.core.logic.Term on which the rule should be applied to as String (find part of the rule)
    3. +
  3. formula= toplevel formula in which term appears in
    4. +
  4. occ = occurrence number
    5. +
  5. inst_= instantiation
    6. +
+ """; + } + @Override public Parameters evaluateArguments(EngineState state, - Map arguments) throws Exception { + Map arguments) throws Exception { return state.getValueInjector().inject(this, new Parameters(), arguments); } @@ -65,7 +84,7 @@ public void execute(AbstractUserInterfaceControl uiControl, Parameters args, Eng if (!tacletApp.ifInstsComplete()) { ImmutableList ifSeqCandidates = - tacletApp.findIfFormulaInstantiations(g.sequent(), g.proof().getServices()); + tacletApp.findIfFormulaInstantiations(g.sequent(), g.proof().getServices()); if (ifSeqCandidates.size() == 1) { theApp = ifSeqCandidates.head(); @@ -86,21 +105,21 @@ private RuleApp makeRuleApp(Parameters p, EngineState state) throws ScriptExcept final Proof proof = state.getProof(); final Optional maybeBuiltInRule = - proof.getInitConfig().getProfile().getStandardRules().standardBuiltInRules().stream() - .filter(r -> r.name().toString().equals(p.rulename)).findAny(); + proof.getInitConfig().getProfile().getStandardRules().standardBuiltInRules().stream() + .filter(r -> r.name().toString().equals(p.rulename)).findAny(); final Optional maybeTaclet = Optional.ofNullable( - proof.getEnv().getInitConfigForEnvironment().lookupActiveTaclet(new Name(p.rulename))); + proof.getEnv().getInitConfigForEnvironment().lookupActiveTaclet(new Name(p.rulename))); if (!maybeBuiltInRule.isPresent() && !maybeTaclet.isPresent()) { /* * (DS, 2019-01-31): Might be a locally introduced taclet, e.g., by hide_left etc. */ final Optional maybeApp = Optional.ofNullable( - state.getFirstOpenAutomaticGoal().indexOfTaclets().lookup(p.rulename)); + state.getFirstOpenAutomaticGoal().indexOfTaclets().lookup(p.rulename)); TacletApp app = maybeApp.orElseThrow( - () -> new ScriptException("Taclet '" + p.rulename + "' not known.")); + () -> new ScriptException("Taclet '" + p.rulename + "' not known.")); if (app.taclet() instanceof FindTaclet) { app = findTacletApp(p, state); @@ -120,7 +139,7 @@ private RuleApp makeRuleApp(Parameters p, EngineState state) throws ScriptExcept return instantiateTacletApp(p, state, proof, theApp); } else { IBuiltInRuleApp builtInRuleApp = // - builtInRuleApp(p, state, maybeBuiltInRule.get()); + builtInRuleApp(p, state, maybeBuiltInRule.get()); if (builtInRuleApp.isSufficientlyComplete()) { builtInRuleApp = builtInRuleApp.forceInstantiate(state.getFirstOpenAutomaticGoal()); } @@ -129,7 +148,7 @@ private RuleApp makeRuleApp(Parameters p, EngineState state) throws ScriptExcept } private TacletApp instantiateTacletApp(final Parameters p, final EngineState state, - final Proof proof, final TacletApp theApp) throws ScriptException { + final Proof proof, final TacletApp theApp) throws ScriptException { TacletApp result = theApp; Services services = proof.getServices(); @@ -159,7 +178,7 @@ private TacletApp instantiateTacletApp(final Parameters p, final EngineState sta * "\newPV", Skolem terms etc. */ final TacletApp maybeInstApp = result.tryToInstantiateAsMuchAsPossible( - services.getOverlay(state.getFirstOpenAutomaticGoal().getLocalNamespaces())); + services.getOverlay(state.getFirstOpenAutomaticGoal().getLocalNamespaces())); if (maybeInstApp != null) { result = maybeInstApp; @@ -184,7 +203,7 @@ private TacletApp instantiateTacletApp(final Parameters p, final EngineState sta // try to instantiate remaining symbols result = result.tryToInstantiate( - services.getOverlay(state.getFirstOpenAutomaticGoal().getLocalNamespaces())); + services.getOverlay(state.getFirstOpenAutomaticGoal().getLocalNamespaces())); if (result == null) { throw new ScriptException("Cannot instantiate this rule"); @@ -192,7 +211,7 @@ private TacletApp instantiateTacletApp(final Parameters p, final EngineState sta if (recheckMatchConditions) { final MatchConditions appMC = - result.taclet().getMatcher().checkConditions(result.matchConditions(), services); + result.taclet().getMatcher().checkConditions(result.matchConditions(), services); if (appMC == null) { return null; } else { @@ -211,8 +230,8 @@ private TacletApp makeNoFindTacletApp(Taclet taclet) { private IBuiltInRuleApp builtInRuleApp(Parameters p, EngineState state, BuiltInRule rule) throws ScriptException { final List matchingApps = // - findBuiltInRuleApps(p, state).stream().filter(r -> r.rule().name().equals(rule.name())) - .toList(); + findBuiltInRuleApps(p, state).stream().filter(r -> r.rule().name().equals(rule.name())) + .toList(); if (matchingApps.isEmpty()) { throw new ScriptException("No matching applications."); @@ -227,7 +246,7 @@ private IBuiltInRuleApp builtInRuleApp(Parameters p, EngineState state, BuiltInR } else { if (p.occ >= matchingApps.size()) { throw new ScriptException("Occurence " + p.occ - + " has been specified, but there are only " + matchingApps.size() + " hits."); + + " has been specified, but there are only " + matchingApps.size() + " hits."); } return matchingApps.get(p.occ); @@ -251,7 +270,7 @@ private TacletApp findTacletApp(Parameters p, EngineState state) throws ScriptEx } else { if (p.occ >= matchingApps.size()) { throw new ScriptException("Occurence " + p.occ - + " has been specified, but there are only " + matchingApps.size() + " hits."); + + " has been specified, but there are only " + matchingApps.size() + " hits."); } return matchingApps.get(p.occ); } @@ -272,7 +291,7 @@ private ImmutableList findBuiltInRuleApps(Parameters p, EngineS } allApps = allApps.append( - index.getBuiltInRule(g, new PosInOccurrence(sf, PosInTerm.getTopLevel(), true))); + index.getBuiltInRule(g, new PosInOccurrence(sf, PosInTerm.getTopLevel(), true))); } for (SequentFormula sf : g.node().sequent().succedent()) { @@ -281,7 +300,7 @@ private ImmutableList findBuiltInRuleApps(Parameters p, EngineS } allApps = allApps.append( - index.getBuiltInRule(g, new PosInOccurrence(sf, PosInTerm.getTopLevel(), false))); + index.getBuiltInRule(g, new PosInOccurrence(sf, PosInTerm.getTopLevel(), false))); } return allApps; @@ -303,7 +322,7 @@ private ImmutableList findAllTacletApps(Parameters p, EngineState sta } allApps = allApps.append(index.getTacletAppAtAndBelow(filter, - new PosInOccurrence(sf, PosInTerm.getTopLevel(), true), services)); + new PosInOccurrence(sf, PosInTerm.getTopLevel(), true), services)); } for (SequentFormula sf : g.node().sequent().succedent()) { @@ -312,7 +331,7 @@ private ImmutableList findAllTacletApps(Parameters p, EngineState sta } allApps = allApps.append(index.getTacletAppAtAndBelow(filter, - new PosInOccurrence(sf, PosInTerm.getTopLevel(), false), services)); + new PosInOccurrence(sf, PosInTerm.getTopLevel(), false), services)); } return allApps; @@ -323,18 +342,18 @@ private ImmutableList findAllTacletApps(Parameters p, EngineState sta * {@link Parameters#formula} parameter or its String representation matches the * {@link Parameters#matches} regex. If both parameters are not supplied, always returns true. * - * @param p The {@link Parameters} object. + * @param p The {@link Parameters} object. * @param sf The {@link SequentFormula} to check. * @return true if sf matches. */ private boolean isFormulaSearchedFor(Parameters p, SequentFormula sf, Services services) throws ScriptException { final boolean satisfiesFormulaParameter = - p.formula != null && sf.formula().equalsModProperty(p.formula, RENAMING_TERM_PROPERTY); + p.formula != null && sf.formula().equalsModProperty(p.formula, RENAMING_TERM_PROPERTY); final boolean satisfiesMatchesParameter = p.matches != null && formatTermString(LogicPrinter.quickPrintTerm(sf.formula(), services)) - .matches(".*" + p.matches + ".*"); + .matches(".*" + p.matches + ".*"); return (p.formula == null && p.matches == null) || satisfiesFormulaParameter || satisfiesMatchesParameter; @@ -360,15 +379,15 @@ private List filterList(Parameters p, ImmutableList list) for (TacletApp tacletApp : list) { if (tacletApp instanceof PosTacletApp pta) { boolean add = - p.on == null || pta.posInOccurrence().subTerm() - .equalsModProperty(p.on, RENAMING_TERM_PROPERTY); + p.on == null || pta.posInOccurrence().subTerm() + .equalsModProperty(p.on, RENAMING_TERM_PROPERTY); Iterator it = pta.instantiations().svIterator(); while (it.hasNext()) { SchemaVariable sv = it.next(); Term userInst = p.instantiations.get(sv.name().toString()); Object ptaInst = - pta.instantiations().getInstantiationEntry(sv).getInstantiation(); + pta.instantiations().getInstantiationEntry(sv).getInstantiation(); add &= userInst == null || userInst.equalsModProperty(ptaInst, IRRELEVANT_TERM_LABELS_PROPERTY); diff --git a/key.core/src/main/java/de/uka/ilkd/key/macros/scripts/SkipCommand.java b/key.core/src/main/java/de/uka/ilkd/key/macros/scripts/SkipCommand.java index 94ae7521398..a00f4b55182 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/macros/scripts/SkipCommand.java +++ b/key.core/src/main/java/de/uka/ilkd/key/macros/scripts/SkipCommand.java @@ -17,4 +17,8 @@ public String getName() { return "skip"; } + @Override + public String getDocumentation() { + return "Does exactly nothing. Really nothing."; + } } diff --git a/key.core/src/main/java/de/uka/ilkd/key/macros/scripts/meta/ArgumentsLifter.java b/key.core/src/main/java/de/uka/ilkd/key/macros/scripts/meta/ArgumentsLifter.java index 958a61dc8dc..23be89b33a6 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/macros/scripts/meta/ArgumentsLifter.java +++ b/key.core/src/main/java/de/uka/ilkd/key/macros/scripts/meta/ArgumentsLifter.java @@ -64,7 +64,6 @@ private static ProofScriptArgument lift(Option option, Field field) { arg.setRequired(option.required()); arg.setField(field); arg.setType(field.getType()); - arg.setDocumentation(DescriptionFacade.getDocumentation(arg)); return arg; } diff --git a/key.core/src/main/java/de/uka/ilkd/key/macros/scripts/meta/DescriptionFacade.java b/key.core/src/main/java/de/uka/ilkd/key/macros/scripts/meta/DescriptionFacade.java deleted file mode 100644 index c1f6c7fda90..00000000000 --- a/key.core/src/main/java/de/uka/ilkd/key/macros/scripts/meta/DescriptionFacade.java +++ /dev/null @@ -1,100 +0,0 @@ -/* This file is part of KeY - https://key-project.org - * KeY is licensed under the GNU General Public License Version 2 - * SPDX-License-Identifier: GPL-2.0-only */ -package de.uka.ilkd.key.macros.scripts.meta; - -import java.io.IOException; -import java.util.Properties; - -import de.uka.ilkd.key.macros.scripts.ProofScriptCommand; - -import org.slf4j.Logger; -import org.slf4j.LoggerFactory; - -/** - * This facade is used to load documentation for {@link ProofScriptCommand} and - * {@link ProofScriptArgument}. - *

- * It uses a {@code COMMANDS_DESCRIPTION} property file. - * - * @author Alexander Weigl - * @version 1 (18.08.17) - */ -public final class DescriptionFacade { - /** - * The filename of the XML properties containing the documentation of proof script commands. - */ - private static final String COMMANDS_DESCRIPTION = "commands_description.xml"; - private static final Logger LOGGER = LoggerFactory.getLogger(DescriptionFacade.class); - - /** - * Lazy-loaded properties - * - * @see #getProperties - */ - private static Properties properties = null; - - private DescriptionFacade() { - } - - /** - * Lazy loading of the properties. - * - * @return a properties - */ - public static Properties getProperties() { - try { - if (properties == null) { - properties = new Properties(); - properties.loadFromXML( - DescriptionFacade.class.getResourceAsStream(COMMANDS_DESCRIPTION)); - } - } catch (IOException e) { - LOGGER.warn("Failed to load properties", e); - } - return properties; - } - - /** - * Looks up the documentation for the given command in the properties file. If no documentation - * is available an empty string is returned. - * - * @param cmd non-null proof script command - * @return a non-null string - * @see ProofScriptCommand#getDocumentation() - */ - public static String getDocumentation(ProofScriptCommand cmd) { - return getString(cmd.getName()); - } - - /** - * Looks up the documentation for the given proof script argument. If no documentation is - * available an empty string is returned. - * - * @param arg non-null proof script argument - * @return a string or null, if {@code arg} is null or {@code arg.getCommand} returns null - * @see ProofScriptArgument#getDocumentation() - */ - public static String getDocumentation(ProofScriptArgument arg) { - if (arg == null || arg.getCommand() == null) { - return null; - } - String key = arg.getCommand().getName() + "." + arg.getName(); - return getString(key); - } - - /** - * Helper function for look-ups in the property file. - * - * @param key look up key - * @return a non-null string - */ - private static String getString(String key) { - String property = getProperties().getProperty(key); - if (null == property) { - LOGGER.warn("No documentation entry found for {} in {}", key, COMMANDS_DESCRIPTION); - return ""; - } - return property; - } -} diff --git a/key.core/src/main/resources/de/uka/ilkd/key/macros/scripts/meta/commands_description.xml b/key.core/src/main/resources/de/uka/ilkd/key/macros/scripts/meta/commands_description.xml deleted file mode 100644 index 5f40816623b..00000000000 --- a/key.core/src/main/resources/de/uka/ilkd/key/macros/scripts/meta/commands_description.xml +++ /dev/null @@ -1,59 +0,0 @@ - - - This is a comment - - - - - - The assume command is an unsound taclet rule and takes one argument: - - The command adds the formula passed as argument to the antecedent - a formula #2 to which the command is applied - - - The AutoCommand invokes the automatic strategy "Auto" - - - * The command object CutCommand has as scriptcommand name "cut" - * As parameters: - * a formula with the id "#2" - - - - - - - - - - - - - - - - *

  • #2 = rule name
    • - *
  • on= key.core.logic.Term on which the rule should be applied to as String (find part of the rule)
    • - *
  • formula= toplevel formula in which term appears in
    • - *
  • occ = occurrence number
    • - *
  • inst_= instantiation
    • - * - ]]> - - - - - - - - instantiate formula="\forall int a; phi(a)" with="a_8" - ]]> - - \ No newline at end of file