From e24b667c1e0bfe410a766e9468f1a712347004e1 Mon Sep 17 00:00:00 2001
From: "E. Prebet" <enguerrand.prebet@kit.edu>
Date: Tue, 2 Jul 2024 16:13:57 +0200
Subject: [PATCH] Add panel selection for dRL tactics

---
 .../js/controllers/provingawesome.js          |   3 +
 .../resources/templates/menu/refinement.html  | 229 ++++++++++++++++++
 .../resources/templates/menu/tactics.html     |   3 +-
 3 files changed, 234 insertions(+), 1 deletion(-)
 create mode 100644 keymaerax-webui/src/main/resources/templates/menu/refinement.html

diff --git a/keymaerax-webui/src/main/resources/js/controllers/provingawesome.js b/keymaerax-webui/src/main/resources/js/controllers/provingawesome.js
index 7b670e16de..1ade3e3517 100644
--- a/keymaerax-webui/src/main/resources/js/controllers/provingawesome.js
+++ b/keymaerax-webui/src/main/resources/js/controllers/provingawesome.js
@@ -600,6 +600,9 @@ angular.module('keymaerax.controllers').controller('TaskCtrl',
       },
       odemenu: {
         kind: 'box'
+      },
+      refmenu: {
+        kind: 'base'
       }
     }
 
diff --git a/keymaerax-webui/src/main/resources/templates/menu/refinement.html b/keymaerax-webui/src/main/resources/templates/menu/refinement.html
new file mode 100644
index 0000000000..63511e0373
--- /dev/null
+++ b/keymaerax-webui/src/main/resources/templates/menu/refinement.html
@@ -0,0 +1,229 @@
+<a class="dropdown-toggle" ng-class="{'disabled': agenda.items().length <= 0 }" data-toggle="dropdown" role="button"
+   aria-haspopup="true" aria-expanded="false">Refinement <span class="caret"></span></a>
+<ul class="dropdown-menu">
+    <k4-tactic-menu-entry
+            disabled="agenda.items().length <= 0"
+            proof-id="{{proofId}}" user-id="{{userId}}"
+            name="[<=]" code-name="refBox"
+            exec="openTacticPosInputDialog(codeName, 'R')" option-exec="doSearch(codeName, 'R')"></k4-tactic-menu-entry>
+    <k4-tactic-menu-entry
+            disabled="agenda.items().length <= 0"
+            proof-id="{{proofId}}" user-id="{{userId}}"
+            name="Transitivity" code-name="refTrans"
+            exec="openTacticPosInputDialog(codeName, 'R')" option-exec="doSearch(codeName, 'R')"></k4-tactic-menu-entry>
+    <li>
+        <nav class="nav nav-pills nav-fill">
+            <a class="button nav-item nav-link" ng-class="{active: menu.refmenu.kind=='base'}"
+               ng-click="menu.refmenu.kind='base';$event.stopPropagation();">Base</a>
+            <a class="button nav-item nav-link" ng-class="{active: menu.refmenu.kind=='kat'}"
+               ng-click="menu.refmenu.kind='kat';$event.stopPropagation();">KAT</a>
+            <a class="button nav-item nav-link" ng-class="{active: menu.refmenu.kind=='ode'}"
+               ng-click="menu.refmenu.kind='ode';$event.stopPropagation();">ODE</a>
+        </nav>
+    </li>
+    <li role="separator" class="divider"></li>
+    <k4-tactic-menu-entry
+            ng-if="menu.refmenu.kind=='base'" disabled="agenda.items().length <= 0"
+            proof-id="{{proofId}}" user-id="{{userId}}"
+            name="Antisymmetry" code-name="refAntiSym"
+            exec="openTacticPosInputDialog(codeName, 'R')" option-exec="doSearch(codeName, 'R')"></k4-tactic-menu-entry>
+    <k4-tactic-menu-entry
+            ng-if="menu.refmenu.kind=='base'" disabled="agenda.items().length <= 0"
+            proof-id="{{proofId}}" user-id="{{userId}}"
+            name="Test" code-name="refTest"
+            exec="openTacticPosInputDialog(codeName, 'R')" option-exec="doSearch(codeName, 'R')"></k4-tactic-menu-entry>
+    <k4-tactic-menu-entry
+            ng-if="menu.refmenu.kind=='base'" disabled="agenda.items().length <= 0"
+            proof-id="{{proofId}}" user-id="{{userId}}"
+            name="Assignment" code-name="refAssign"
+            exec="openTacticPosInputDialog(codeName, 'R')" option-exec="doSearch(codeName, 'R')"></k4-tactic-menu-entry>
+    <k4-tactic-menu-entry
+            ng-if="menu.refmenu.kind=='base'" disabled="agenda.items().length <= 0"
+            proof-id="{{proofId}}" user-id="{{userId}}"
+            name="Stutter" code-name="refStutter"
+            exec="openTacticPosInputDialog(codeName, 'R')" option-exec="doSearch(codeName, 'R')"></k4-tactic-menu-entry>
+    <k4-tactic-menu-entry
+            ng-if="menu.refmenu.kind=='base'" disabled="agenda.items().length <= 0"
+            proof-id="{{proofId}}" user-id="{{userId}}"
+            name="Choice Left" code-name="refChoiceL"
+            exec="openTacticPosInputDialog(codeName, 'R')" option-exec="doSearch(codeName, 'R')"></k4-tactic-menu-entry>
+    <k4-tactic-menu-entry
+            ng-if="menu.refmenu.kind=='base'" disabled="agenda.items().length <= 0"
+            proof-id="{{proofId}}" user-id="{{userId}}"
+            name="Choice Right" code-name="refChoiceR"
+            exec="openTacticPosInputDialog(codeName, 'R')" option-exec="doSearch(codeName, 'R')"></k4-tactic-menu-entry>
+    <k4-tactic-menu-entry
+            ng-if="menu.refmenu.kind=='base'" disabled="agenda.items().length <= 0"
+            proof-id="{{proofId}}" user-id="{{userId}}"
+            name="Sequence" code-name="refSeq"
+            exec="openTacticPosInputDialog(codeName, 'R')" option-exec="doSearch(codeName, 'R')"></k4-tactic-menu-entry>
+    <k4-tactic-menu-entry
+            ng-if="menu.refmenu.kind=='base'" disabled="agenda.items().length <= 0"
+            proof-id="{{proofId}}" user-id="{{userId}}"
+            name="Loop Left" code-name="refLoopL"
+            exec="openTacticPosInputDialog(codeName, 'R')" option-exec="doSearch(codeName, 'R')"></k4-tactic-menu-entry>
+    <k4-tactic-menu-entry
+            ng-if="menu.refmenu.kind=='base'" disabled="agenda.items().length <= 0"
+            proof-id="{{proofId}}" user-id="{{userId}}"
+            name="Loop Right" code-name="refLoopR"
+            exec="openTacticPosInputDialog(codeName, 'R')" option-exec="doSearch(codeName, 'R')"></k4-tactic-menu-entry>
+    <k4-tactic-menu-entry
+            ng-if="menu.refmenu.kind=='base'" disabled="agenda.items().length <= 0"
+            proof-id="{{proofId}}" user-id="{{userId}}"
+            name="Deterministic Test" code-name="refTestDet"
+            exec="openTacticPosInputDialog(codeName, 'R')" option-exec="doSearch(codeName, 'R')"></k4-tactic-menu-entry>
+    <k4-tactic-menu-entry
+            ng-if="menu.refmenu.kind=='base'" disabled="agenda.items().length <= 0"
+            proof-id="{{proofId}}" user-id="{{userId}}"
+            name="Deterministic Assignment" code-name="refAssignDet"
+            exec="openTacticPosInputDialog(codeName, 'R')" option-exec="doSearch(codeName, 'R')"></k4-tactic-menu-entry>
+    <k4-tactic-menu-entry
+            ng-if="menu.refmenu.kind=='base'" disabled="agenda.items().length <= 0"
+            proof-id="{{proofId}}" user-id="{{userId}}"
+            name="Merge :*" code-name="refAnyMerge"
+            exec="openTacticPosInputDialog(codeName, 'R')" option-exec="doSearch(codeName, 'R')"></k4-tactic-menu-entry>
+    <k4-tactic-menu-entry
+            ng-if="menu.refmenu.kind=='base'" disabled="agenda.items().length <= 0"
+            proof-id="{{proofId}}" user-id="{{userId}}"
+            name="Merge :=*" code-name="refAssignAnyMerge"
+            exec="openTacticPosInputDialog(codeName, 'R')" option-exec="doSearch(codeName, 'R')"></k4-tactic-menu-entry>
+    <k4-tactic-menu-entry
+            ng-if="menu.refmenu.kind=='base'" disabled="agenda.items().length <= 0"
+            proof-id="{{proofId}}" user-id="{{userId}}"
+            name="Unloop" code-name="refUnloop"
+            exec="openTacticPosInputDialog(codeName, 'R')" option-exec="doSearch(codeName, 'R')"></k4-tactic-menu-entry>
+
+    <k4-tactic-menu-entry
+            ng-if="menu.refmenu.kind=='ode'" disabled="agenda.items().length <= 0"
+            proof-id="{{proofId}}" user-id="{{userId}}"
+            name="ODE" code-name="refOde"
+            exec="openTacticPosInputDialog(codeName, 'R')" option-exec="doSearch(codeName, 'R')"></k4-tactic-menu-entry>
+    <k4-tactic-menu-entry
+            ng-if="menu.refmenu.kind=='ode'" disabled="agenda.items().length <= 0"
+            proof-id="{{proofId}}" user-id="{{userId}}"
+            name="ODE idempotency" code-name="refOdeIdemp"
+            exec="openTacticPosInputDialog(codeName, 'R')" option-exec="doSearch(codeName, 'R')"></k4-tactic-menu-entry>
+    <k4-tactic-menu-entry
+            ng-if="menu.refmenu.kind=='ode'" disabled="agenda.items().length <= 0"
+            proof-id="{{proofId}}" user-id="{{userId}}"
+            name="DE" code-name="refDE"
+            exec="openTacticPosInputDialog(codeName, 'R')" option-exec="doSearch(codeName, 'R')"></k4-tactic-menu-entry>
+    <k4-tactic-menu-entry
+            ng-if="menu.refmenu.kind=='ode'" disabled="agenda.items().length <= 0"
+            proof-id="{{proofId}}" user-id="{{userId}}"
+            name="DW" code-name="refDW"
+            exec="openTacticPosInputDialog(codeName, 'R')" option-exec="doSearch(codeName, 'R')"></k4-tactic-menu-entry>
+    <k4-tactic-menu-entry
+            ng-if="menu.refmenu.kind=='ode'" disabled="agenda.items().length <= 0"
+            proof-id="{{proofId}}" user-id="{{userId}}"
+            name="DX" code-name="refDX"
+            exec="openTacticPosInputDialog(codeName, 'R')" option-exec="doSearch(codeName, 'R')"></k4-tactic-menu-entry>
+
+    <k4-tactic-menu-entry
+            ng-if="menu.refmenu.kind=='kat'" disabled="agenda.items().length <= 0"
+            proof-id="{{proofId}}" user-id="{{userId}}"
+            name="Reflexivity" code-name="refRefl"
+            exec="openTacticPosInputDialog(codeName, 'R')" option-exec="doSearch(codeName, 'R')"></k4-tactic-menu-entry>
+    <k4-tactic-menu-entry
+            ng-if="menu.refmenu.kind=='kat'" disabled="agenda.items().length <= 0"
+            proof-id="{{proofId}}" user-id="{{userId}}"
+            name="Choice Identity" code-name="refChoiceId"
+            exec="openTacticPosInputDialog(codeName, 'R')" option-exec="doSearch(codeName, 'R')"></k4-tactic-menu-entry>
+    <k4-tactic-menu-entry
+            ng-if="menu.refmenu.kind=='kat'" disabled="agenda.items().length <= 0"
+            proof-id="{{proofId}}" user-id="{{userId}}"
+            name="Choice Idempotency" code-name="refChoiceIdemp"
+            exec="openTacticPosInputDialog(codeName, 'R')" option-exec="doSearch(codeName, 'R')"></k4-tactic-menu-entry>
+    <k4-tactic-menu-entry
+            ng-if="menu.refmenu.kind=='kat'" disabled="agenda.items().length <= 0"
+            proof-id="{{proofId}}" user-id="{{userId}}"
+            name="Choice Commutativity" code-name="refChoiceComm"
+            exec="openTacticPosInputDialog(codeName, 'R')" option-exec="doSearch(codeName, 'R')"></k4-tactic-menu-entry>
+    <k4-tactic-menu-entry
+            ng-if="menu.refmenu.kind=='kat'" disabled="agenda.items().length <= 0"
+            proof-id="{{proofId}}" user-id="{{userId}}"
+            name="Choice Associativity" code-name="refChoiceAssoc"
+            exec="openTacticPosInputDialog(codeName, 'R')" option-exec="doSearch(codeName, 'R')"></k4-tactic-menu-entry>
+    <k4-tactic-menu-entry
+            ng-if="menu.refmenu.kind=='kat'" disabled="agenda.items().length <= 0"
+            proof-id="{{proofId}}" user-id="{{userId}}"
+            name="Sequence Identity Left" code-name="refSeqIdL"
+            exec="openTacticPosInputDialog(codeName, 'R')" option-exec="doSearch(codeName, 'R')"></k4-tactic-menu-entry>
+    <k4-tactic-menu-entry
+            ng-if="menu.refmenu.kind=='kat'" disabled="agenda.items().length <= 0"
+            proof-id="{{proofId}}" user-id="{{userId}}"
+            name="Sequence Identity Right" code-name="refSeqIdR"
+            exec="openTacticPosInputDialog(codeName, 'R')" option-exec="doSearch(codeName, 'R')"></k4-tactic-menu-entry>
+    <k4-tactic-menu-entry
+            ng-if="menu.refmenu.kind=='kat'" disabled="agenda.items().length <= 0"
+            proof-id="{{proofId}}" user-id="{{userId}}"
+            name="Sequence Associativity" code-name="refSeqAssoc"
+            exec="openTacticPosInputDialog(codeName, 'R')" option-exec="doSearch(codeName, 'R')"></k4-tactic-menu-entry>
+    <k4-tactic-menu-entry
+            ng-if="menu.refmenu.kind=='kat'" disabled="agenda.items().length <= 0"
+            proof-id="{{proofId}}" user-id="{{userId}}"
+            name="Distributivity Left" code-name="refDistrL"
+            exec="openTacticPosInputDialog(codeName, 'R')" option-exec="doSearch(codeName, 'R')"></k4-tactic-menu-entry>
+    <k4-tactic-menu-entry
+            ng-if="menu.refmenu.kind=='kat'" disabled="agenda.items().length <= 0"
+            proof-id="{{proofId}}" user-id="{{userId}}"
+            name="Distributivity Right" code-name="refDistrR"
+            exec="openTacticPosInputDialog(codeName, 'R')" option-exec="doSearch(codeName, 'R')"></k4-tactic-menu-entry>
+    <k4-tactic-menu-entry
+            ng-if="menu.refmenu.kind=='kat'" disabled="agenda.items().length <= 0"
+            proof-id="{{proofId}}" user-id="{{userId}}"
+            name="Annihilation Left" code-name="refAnnihL"
+            exec="openTacticPosInputDialog(codeName, 'R')" option-exec="doSearch(codeName, 'R')"></k4-tactic-menu-entry>
+    <k4-tactic-menu-entry
+            ng-if="menu.refmenu.kind=='kat'" disabled="agenda.items().length <= 0"
+            proof-id="{{proofId}}" user-id="{{userId}}"
+            name="Annihilation Right" code-name="refAnnihR"
+            exec="openTacticPosInputDialog(codeName, 'R')" option-exec="doSearch(codeName, 'R')"></k4-tactic-menu-entry>
+    <k4-tactic-menu-entry
+            ng-if="menu.refmenu.kind=='kat'" disabled="agenda.items().length <= 0"
+            proof-id="{{proofId}}" user-id="{{userId}}"
+            name="Unfold Left" code-name="refUnfoldL"
+            exec="openTacticPosInputDialog(codeName, 'R')" option-exec="doSearch(codeName, 'R')"></k4-tactic-menu-entry>
+    <k4-tactic-menu-entry
+            ng-if="menu.refmenu.kind=='kat'" disabled="agenda.items().length <= 0"
+            proof-id="{{proofId}}" user-id="{{userId}}"
+            name="Unfold Right" code-name="refUnfoldR"
+            exec="openTacticPosInputDialog(codeName, 'R')" option-exec="doSearch(codeName, 'R')"></k4-tactic-menu-entry>
+
+    <k4-tactic-menu-entry
+            ng-if="menu.refmenu.kind=='base'" disabled="agenda.items().length <= 0"
+            proof-id="{{proofId}}" user-id="{{userId}}"
+            name="Assignment Commutativity" code-name="refAssignComm"
+            exec="openTacticPosInputDialog(codeName, 'R')" option-exec="doSearch(codeName, 'R')"></k4-tactic-menu-entry>
+    <k4-tactic-menu-entry
+            ng-if="menu.refmenu.kind=='base'" disabled="agenda.items().length <= 0"
+            proof-id="{{proofId}}" user-id="{{userId}}"
+            name="Assignment Substitution" code-name="refAssignSubst"
+            exec="openTacticPosInputDialog(codeName, 'R')" option-exec="doSearch(codeName, 'R')"></k4-tactic-menu-entry>
+    <k4-tactic-menu-entry
+            ng-if="menu.refmenu.kind=='base'" disabled="agenda.items().length <= 0"
+            proof-id="{{proofId}}" user-id="{{userId}}"
+            name="Assignment/Test Commutativity" code-name="refAssignTest"
+            exec="openTacticPosInputDialog(codeName, 'R')" option-exec="doSearch(codeName, 'R')"></k4-tactic-menu-entry>
+    <k4-tactic-menu-entry
+            ng-if="menu.refmenu.kind=='base'" disabled="agenda.items().length <= 0"
+            proof-id="{{proofId}}" user-id="{{userId}}"
+            name="Assignment Merge" code-name="refAssignMerge"
+            exec="openTacticPosInputDialog(codeName, 'R')" option-exec="doSearch(codeName, 'R')"></k4-tactic-menu-entry>
+    <k4-tactic-menu-entry
+            ng-if="menu.refmenu.kind=='base'" disabled="agenda.items().length <= 0"
+            proof-id="{{proofId}}" user-id="{{userId}}"
+            name=":=* Commutativity" code-name="refAnyComm"
+            exec="openTacticPosInputDialog(codeName, 'R')" option-exec="doSearch(codeName, 'R')"></k4-tactic-menu-entry>
+    <k4-tactic-menu-entry
+            ng-if="menu.refmenu.kind=='base'" disabled="agenda.items().length <= 0"
+            proof-id="{{proofId}}" user-id="{{userId}}"
+            name="Assignment/:=* Commutativity" code-name="refAssignAnyComm"
+            exec="openTacticPosInputDialog(codeName, 'R')" option-exec="doSearch(codeName, 'R')"></k4-tactic-menu-entry>
+    <k4-tactic-menu-entry
+            ng-if="menu.refmenu.kind=='base'" disabled="agenda.items().length <= 0"
+            proof-id="{{proofId}}" user-id="{{userId}}"
+            name="Test/:=* Commutativity" code-name="refAnyTest"
+            exec="openTacticPosInputDialog(codeName, 'R')" option-exec="doSearch(codeName, 'R')"></k4-tactic-menu-entry>
+
+</ul>
diff --git a/keymaerax-webui/src/main/resources/templates/menu/tactics.html b/keymaerax-webui/src/main/resources/templates/menu/tactics.html
index 63acdbedd1..bc27c03afa 100644
--- a/keymaerax-webui/src/main/resources/templates/menu/tactics.html
+++ b/keymaerax-webui/src/main/resources/templates/menu/tactics.html
@@ -3,4 +3,5 @@
 <li class="nav-item dropdown" ng-class="{'disabled': agenda.items().length <= 0 }" ng-include="'templates/menu/quantifier.html'"></li>
 <li class="nav-item dropdown" ng-class="{'disabled': agenda.items().length <= 0 }" ng-include="'templates/menu/hybridprograms.html'"></li>
 <li class="nav-item dropdown" ng-class="{'disabled': agenda.items().length <= 0 }" ng-include="'templates/menu/differentialequation.html'"></li>
-<li class="nav-item dropdown" ng-class="{'disabled': agenda.items().length <= 0 }" ng-include="'templates/menu/tools.html'"></li>
\ No newline at end of file
+<li class="nav-item dropdown" ng-class="{'disabled': agenda.items().length <= 0 }" ng-include="'templates/menu/tools.html'"></li>
+<li class="nav-item dropdown" ng-class="{'disabled': agenda.items().length <= 0 }" ng-include="'templates/menu/refinement.html'"></li>
\ No newline at end of file