RuleCommand can now deal with rules that have schema variables for lo…

…gical variables (#3482)
KeYProject · Jun 19, 2024 · c8b5d84 · c8b5d84
2 parents 19f83d3 + 1b48b9e
commit c8b5d84
Showing 1 changed file with 14 additions and 2 deletions.
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
@@ -61,8 +61,20 @@ public void execute(AbstractUserInterfaceControl uiControl, Parameters args, Eng
         RuleApp theApp = makeRuleApp(args, state);
         Goal g = state.getFirstOpenAutomaticGoal();
 
-        if (theApp instanceof TacletApp) {
-            RuleApp completeApp = ((TacletApp) theApp).tryToInstantiate(g.proof().getServices());
+        if (theApp instanceof TacletApp tacletApp) {
+
+            if (!tacletApp.ifInstsComplete()) {
+                ImmutableList<TacletApp> ifSeqCandidates =
+                    tacletApp.findIfFormulaInstantiations(g.sequent(), g.proof().getServices());
+
+                if (ifSeqCandidates.size() == 1) {
+                    theApp = ifSeqCandidates.head();
+                    assert theApp != null;
+                    tacletApp = (TacletApp) theApp;
+                }
+            }
+
+            RuleApp completeApp = tacletApp.tryToInstantiate(g.proof().getServices());
             theApp = completeApp == null ? theApp : completeApp;
         }
         assert theApp != null;