Isabelle Translation

.gitlab-ci.yml

@@ -26,10 +26,10 @@ before_script:
   - export SONAR_SCANNER_OPTS="-Xmx8G"
 
 stages:
-    - primary
-    - secondary
-    - ternary
-    - deploy
+  - primary
+  - secondary
+  - ternary
+  - deploy
 
 compile:classes:
   stage: primary

build.gradle

@@ -368,9 +368,9 @@ subprojects {
             // specific delimiter: normally just 'package', but spotless crashes for files in default package
             // (see https://github.com/diffplug/spotless/issues/30), therefore 'import' is needed. '//' is for files
             // with completely commented out code (which would probably better just be removed in future).
-            if(project.name == 'recoder') {
+            if (project.name == 'recoder') {
                 licenseHeaderFile("$rootDir/gradle/header-recoder", '(package|import|//)')
-            }else {
+            } else {
                 licenseHeaderFile("$rootDir/gradle/header", '(package|import|//)')
             }
         }

key.ui/build.gradle

@@ -33,6 +33,7 @@ dependencies {
     runtimeOnly project(":keyext.exploration")
     runtimeOnly project(":keyext.slicing")
     runtimeOnly project(":keyext.proofmanagement")
+    runtimeOnly project(":keyext.isabelletranslation")
 }
 
 task createExamplesZip(type: Zip) {

keyext.isabelletranslation/build.gradle

@@ -0,0 +1,7 @@
+description "Translation of Sequents to Isabelle"
+
+dependencies {
+    implementation project(':key.core')
+    implementation project(':key.ui')
+    implementation("de.unruh:scala-isabelle_2.13:0.4.3-RC1")
+}

keyext.isabelletranslation/src/main/java/org/key_project/isabelletranslation/IsabelleSettingsProvider.java

@@ -0,0 +1,171 @@
+/* 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 org.key_project.isabelletranslation;
+
+import java.io.IOException;
+import java.math.RoundingMode;
+import java.nio.file.Files;
+import java.nio.file.Path;
+import java.nio.file.Paths;
+import java.util.Collection;
+import java.util.List;
+import javax.swing.*;
+
+import de.uka.ilkd.key.gui.MainWindow;
+import de.uka.ilkd.key.gui.settings.InvalidSettingsInputException;
+import de.uka.ilkd.key.gui.settings.SettingsPanel;
+import de.uka.ilkd.key.gui.settings.SettingsProvider;
+import de.uka.ilkd.key.settings.Configuration;
+
+/**
+ * {@link SettingsProvider} for Isabelle translation extension
+ */
+public class IsabelleSettingsProvider extends SettingsPanel implements SettingsProvider {
+    private static final String INFO_TIMEOUT_FIELD =
+        """
+                Timeout for the external solvers in seconds.
+                """;
+    private static final String infoTranslationPathPanel =
+        """
+                Choose where the isabelle translation files are stored.
+                """;
+    private static final String infoIsabellePathPanel =
+        """
+                Specify the absolute path of the Isabelle folder.
+                Currently supports Isabelle2024-RC1.
+                """;
+
+    private static final Collection<String> SUPPORTED_VERSIONS_TEXT = List.of("Isabelle2024-RC1");
+
+    /**
+     * Panel for inputting the path to where translations are stored
+     */
+    private final JTextField translationPathPanel;
+
+    /**
+     * Panel for inputting the path to Isabelle installation
+     */
+    private final JTextField isabellePathPanel;
+
+    /**
+     * Input field for timeout in seconds
+     */
+    private final JSpinner timeoutField;
+
+    /**
+     * Supported version info for user
+     */
+    private final JTextField versionSupported;
+
+    /**
+     * The current settings object
+     */
+    private final IsabelleTranslationSettings settings;
+
+    public IsabelleSettingsProvider() {
+        super();
+        setHeaderText(getDescription());
+        setSubHeaderText(
+            "Isabelle settings are stored in: "
+                + IsabelleTranslationSettings.SETTINGS_FILE_NEW.getAbsolutePath());
+        translationPathPanel = createTranslationPathPanel();
+        isabellePathPanel = createIsabellePathPanel();
+        timeoutField = createTimeoutField();
+
+        createCheckSupportButton();
+        this.versionSupported = createSolverSupported();
+        this.settings = IsabelleTranslationSettings.getInstance();
+    }
+
+    @Override
+    public String getDescription() {
+        return "Isabelle Translation";
+    }
+
+    @Override
+    public JPanel getPanel(MainWindow window) {
+        isabellePathPanel
+                .setText(settings.getIsabellePath().toString());
+        translationPathPanel
+                .setText(settings.getTranslationPath().toString());
+        timeoutField.setValue(settings.getTimeout());
+        return this;
+    }
+
+    private JTextField createTranslationPathPanel() {
+        return addFileChooserPanel("Location for translation files:", "", infoTranslationPathPanel,
+            true, e -> {
+            });
+    }
+
+    private JTextField createIsabellePathPanel() {
+        return addFileChooserPanel("Isabelle installation folder:", "", infoIsabellePathPanel,
+            true, e -> {
+            });
+    }
+
+    private JSpinner createTimeoutField() {
+        // Use doubles so that the formatter doesn't make every entered String into integers.
+        // [see NumberFormatter#stringToValue()].
+        JSpinner timeoutSpinner = addNumberField("Timeout:", 1, Integer.MAX_VALUE, 1,
+            INFO_TIMEOUT_FIELD,
+            e -> settings.setTimeout(e.intValue()));
+        // Set the editor so that entered Strings only have three decimal places.
+        JSpinner.NumberEditor editor = new JSpinner.NumberEditor(timeoutSpinner, "#");
+        // Use floor rounding to be consistent with the value that will be set for the timeout.
+        editor.getFormat().setRoundingMode(RoundingMode.FLOOR);
+        timeoutSpinner.setEditor(editor);
+        return timeoutSpinner;
+    }
+
+    protected JButton createCheckSupportButton() {
+        JButton checkForSupportButton = new JButton("Check for support");
+        checkForSupportButton.setEnabled(true);
+        checkForSupportButton
+                .addActionListener(arg0 -> versionSupported.setText(getSolverSupportText()));
+        addRowWithHelp(null, new JLabel(), checkForSupportButton);
+        return checkForSupportButton;
+    }
+
+    private boolean checkForSupport() {
+        String isabelleVersion;
+        Path isabelleIdentifierPath =
+            Paths.get(isabellePathPanel.getText(), "/etc/ISABELLE_IDENTIFIER");
+        try {
+            isabelleVersion = Files.readAllLines(isabelleIdentifierPath).getFirst();
+        } catch (IOException e) {
+            return false;
+        }
+        return SUPPORTED_VERSIONS_TEXT.contains(isabelleVersion);
+    }
+
+    protected JTextField createSolverSupported() {
+        JTextField txt = addTextField("Support", getSolverSupportText(),
+            createSupportedVersionText(),
+            emptyValidator());
+        txt.setEditable(false);
+        return txt;
+    }
+
+    private String createSupportedVersionText() {
+        String supportText = "Supports these Isabelle versions: ";
+        supportText = supportText + String.join(", ", SUPPORTED_VERSIONS_TEXT);
+        return supportText;
+    }
+
+    private String getSolverSupportText() {
+        return checkForSupport() ? "Version of Isabelle is supported."
+                : "Version of Isabelle may not be supported.";
+    }
+
+
+    @Override
+    public void applySettings(MainWindow window) throws InvalidSettingsInputException {
+        Configuration newConfig = new Configuration();
+        newConfig.set(IsabelleTranslationSettings.translationPathKey,
+            translationPathPanel.getText());
+        newConfig.set(IsabelleTranslationSettings.isabellePathKey, isabellePathPanel.getText());
+        settings.readSettings(newConfig);
+    }
+}

keyext.isabelletranslation/src/main/java/org/key_project/isabelletranslation/IsabelleTranslationExtension.java

@@ -0,0 +1,63 @@
+/* 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 org.key_project.isabelletranslation;
+
+import java.util.ArrayList;
+import java.util.List;
+import javax.swing.*;
+
+import de.uka.ilkd.key.core.KeYMediator;
+import de.uka.ilkd.key.gui.MainWindow;
+import de.uka.ilkd.key.gui.extension.api.ContextMenuAdapter;
+import de.uka.ilkd.key.gui.extension.api.ContextMenuKind;
+import de.uka.ilkd.key.gui.extension.api.KeYGuiExtension;
+import de.uka.ilkd.key.gui.settings.SettingsProvider;
+import de.uka.ilkd.key.pp.PosInSequent;
+
+import org.key_project.isabelletranslation.gui.controller.TranslateAllAction;
+import org.key_project.isabelletranslation.gui.controller.TranslationAction;
+
+import org.jspecify.annotations.NonNull;
+
+/**
+ * Extension class for Isabelle translation
+ */
+@KeYGuiExtension.Info(name = "Isabelle Translation", optional = true,
+    experimental = false)
+public class IsabelleTranslationExtension implements KeYGuiExtension, KeYGuiExtension.Settings,
+        KeYGuiExtension.ContextMenu, KeYGuiExtension.Startup {
+    @Override
+    public SettingsProvider getSettings() {
+        return new IsabelleSettingsProvider();
+    }
+
+
+    /**
+     * The context menu adapter used by the extension.
+     */
+    private final ContextMenuAdapter adapter = new ContextMenuAdapter() {
+        @Override
+        public List<Action> getContextActions(
+                KeYMediator mediator, ContextMenuKind kind, PosInSequent pos) {
+            if (pos.getPosInOccurrence() != null || mediator.getSelectedGoal() == null) {
+                return List.of();
+            }
+            List<Action> list = new ArrayList<>();
+            list.add(new TranslationAction(MainWindow.getInstance()));
+            list.add(new TranslateAllAction(MainWindow.getInstance()));
+            return list;
+        }
+    };
+
+    @Override
+    public @NonNull List<Action> getContextActions(@NonNull KeYMediator mediator,
+            @NonNull ContextMenuKind kind, @NonNull Object underlyingObject) {
+        return adapter.getContextActions(mediator, kind, underlyingObject);
+    }
+
+    @Override
+    public void init(MainWindow window, KeYMediator mediator) {
+        IsabelleTranslationSettings.getInstance();
+    }
+}