diff --git a/.gitlab-ci.yml b/.gitlab-ci.yml index 1740353ad9..e53ad22204 100644 --- a/.gitlab-ci.yml +++ b/.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 diff --git a/build.gradle b/build.gradle index 55d8e3def5..3f8c1cb248 100644 --- a/build.gradle +++ b/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|//)') } } diff --git a/key.ui/build.gradle b/key.ui/build.gradle index 16e4088f44..cfe16066f7 100644 --- a/key.ui/build.gradle +++ b/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) { diff --git a/keyext.isabelletranslation/build.gradle b/keyext.isabelletranslation/build.gradle new file mode 100644 index 0000000000..e5d113a3c1 --- /dev/null +++ b/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") +} diff --git a/keyext.isabelletranslation/src/main/java/org/key_project/isabelletranslation/IsabelleSettingsProvider.java b/keyext.isabelletranslation/src/main/java/org/key_project/isabelletranslation/IsabelleSettingsProvider.java new file mode 100644 index 0000000000..5fb460b186 --- /dev/null +++ b/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 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); + } +} diff --git a/keyext.isabelletranslation/src/main/java/org/key_project/isabelletranslation/IsabelleTranslationExtension.java b/keyext.isabelletranslation/src/main/java/org/key_project/isabelletranslation/IsabelleTranslationExtension.java new file mode 100644 index 0000000000..8c8593aeba --- /dev/null +++ b/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 getContextActions( + KeYMediator mediator, ContextMenuKind kind, PosInSequent pos) { + if (pos.getPosInOccurrence() != null || mediator.getSelectedGoal() == null) { + return List.of(); + } + List list = new ArrayList<>(); + list.add(new TranslationAction(MainWindow.getInstance())); + list.add(new TranslateAllAction(MainWindow.getInstance())); + return list; + } + }; + + @Override + public @NonNull List 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(); + } +} diff --git a/keyext.isabelletranslation/src/main/java/org/key_project/isabelletranslation/IsabelleTranslationSettings.java b/keyext.isabelletranslation/src/main/java/org/key_project/isabelletranslation/IsabelleTranslationSettings.java new file mode 100644 index 0000000000..21a0d47eb7 --- /dev/null +++ b/keyext.isabelletranslation/src/main/java/org/key_project/isabelletranslation/IsabelleTranslationSettings.java @@ -0,0 +1,222 @@ +/* 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.*; +import java.nio.file.Files; +import java.nio.file.Path; +import java.util.Objects; +import java.util.Properties; +import java.util.stream.Collectors; + +import de.uka.ilkd.key.settings.AbstractSettings; +import de.uka.ilkd.key.settings.Configuration; +import de.uka.ilkd.key.settings.PathConfig; + +import org.jspecify.annotations.NonNull; +import org.slf4j.Logger; +import org.slf4j.LoggerFactory; + +/** + * Settings object used for Isabelle translation. + */ +public class IsabelleTranslationSettings extends AbstractSettings { + private static final Logger LOGGER = LoggerFactory.getLogger(IsabelleTranslationSettings.class); + + /** + * the file where settings are stored + */ + protected static final File SETTINGS_FILE_NEW = + new File(PathConfig.getKeyConfigDir(), "isabelleSettings.json"); + /** + * The settings instance + */ + private static IsabelleTranslationSettings INSTANCE; + + /** + * Key to get Isabelle path in JSON + */ + protected static final String isabellePathKey = "Path"; + /** + * Key to get translation path in JSON + */ + protected static final String translationPathKey = "TranslationPath"; + /** + * Key to get timeout in JSON + */ + protected static final String timeoutKey = "Timeout"; + + /** + * The Isabelle path + */ + private Path isabellePath; + /** + * The translation path + */ + private Path translationPath; + /** + * The timeout in seconds + */ + private int timeoutSeconds; + + /** + * The default path for Isabelle + */ + private static final Path DEFAULT_ISABELLE_PATH = + Path.of(System.getProperty("user.home"), "Isabelle2024-RC1"); + /** + * The default path for translations + */ + private static final Path DEFAULT_TRANSLATION_PATH = + Path.of(PathConfig.getKeyConfigDir(), "IsabelleTranslations"); + /** + * default timeout setting + */ + private static final int DEFAULT_TIMEOUT_SECONDS = 30; + + + private static Configuration getDefaultConfig() { + Configuration config = new Configuration(); + config.set(isabellePathKey, DEFAULT_ISABELLE_PATH); + config.set(translationPathKey, DEFAULT_TRANSLATION_PATH); + config.set(timeoutKey, DEFAULT_TIMEOUT_SECONDS); + return config; + } + + private IsabelleTranslationSettings(Configuration load) { + readSettings(load); + Runtime.getRuntime().addShutdownHook(new Thread(this::save)); + } + + /** + * Returns the instance of this class + * + * @return instance of this class + */ + public static IsabelleTranslationSettings getInstance() { + if (INSTANCE == null) { + if (SETTINGS_FILE_NEW.exists()) { + try { + LOGGER.info("Load Isabelle settings at {}", SETTINGS_FILE_NEW); + return INSTANCE = + new IsabelleTranslationSettings(Configuration.load(SETTINGS_FILE_NEW)); + } catch (IOException e) { + LOGGER.error("Could not read {}, resorting to default settings", + SETTINGS_FILE_NEW, e); + return INSTANCE = new IsabelleTranslationSettings(getDefaultConfig()); + } + } + LOGGER.info("No settings present, resorting to default Isabelle settings"); + return INSTANCE = new IsabelleTranslationSettings(getDefaultConfig()); + } + return INSTANCE; + } + + protected void createSessionFiles() { + Path sessionRootPath = Path.of(translationPath + "/ROOT"); + BufferedReader sessionReader = new BufferedReader( + new InputStreamReader(Objects.requireNonNull(getClass().getResourceAsStream("ROOT")))); + String sessionRoot = + sessionReader.lines().collect(Collectors.joining(System.lineSeparator())); + + Path sessionDocumentPath = Path.of(translationPath + "/document/root.tex"); + BufferedReader sessionDocumentReader = new BufferedReader(new InputStreamReader( + Objects.requireNonNull(getClass().getResourceAsStream("root.tex")))); + String sessionDocument = + sessionDocumentReader.lines().collect(Collectors.joining(System.lineSeparator())); + + try { + Files.createDirectories(sessionDocumentPath.getParent()); + Files.write(sessionRootPath, sessionRoot.getBytes()); + Files.write(sessionDocumentPath, sessionDocument.getBytes()); + LOGGER.info("Created Isabelle session files at: {}", translationPath); + } catch (IOException e) { + LOGGER.error("Failed to create ROOT file for Isabelle Translation, because: {}", + e.toString()); + } + } + + /** + * Writes the settings to the JSON file + */ + public void save() { + LOGGER.info("Save Isabelle settings to: {}", SETTINGS_FILE_NEW.getAbsolutePath()); + try (Writer writer = new FileWriter(SETTINGS_FILE_NEW)) { + var config = new Configuration(); + writeSettings(config); + config.save(writer, "Isabelle settings"); + writer.flush(); + } catch (IOException ex) { + LOGGER.error("Failed to save Isabelle settings", ex); + } + } + + @Override + public void readSettings(Properties props) { + isabellePath = Path.of(props.getProperty(isabellePathKey)); + Path newTranslationPath = Path.of(props.getProperty(translationPathKey)); + if (newTranslationPath != translationPath) { + translationPath = newTranslationPath; + createSessionFiles(); + } + timeoutSeconds = Integer.parseInt(props.getProperty(timeoutKey, "30")); + } + + @Override + public void writeSettings(Properties props) { + props.setProperty(isabellePathKey, isabellePath.toString()); + props.setProperty(translationPathKey, translationPath.toString()); + props.setProperty(timeoutKey, String.valueOf(timeoutSeconds)); + } + + @Override + public void readSettings(@NonNull Configuration props) { + if (isabellePath == null || translationPath == null) { + isabellePath = DEFAULT_ISABELLE_PATH; + translationPath = DEFAULT_TRANSLATION_PATH; + } + isabellePath = Path.of(props.getString(isabellePathKey, isabellePath.toString())); + + Path newTranslationPath = + Path.of(props.getString(translationPathKey, translationPath.toString())); + if (newTranslationPath != translationPath) { + translationPath = newTranslationPath; + createSessionFiles(); + } + + timeoutSeconds = props.getInt(timeoutKey, 30); + } + + @Override + public void writeSettings(@NonNull Configuration props) { + props.set(isabellePathKey, isabellePath.toString()); + props.set(translationPathKey, translationPath.toString()); + props.set(timeoutKey, String.valueOf(timeoutSeconds)); + } + + /** + * @return + * The header used for translation theories. Includes the preamble and Main theory + * imports + */ + public String getHeader() { + return "theory Translation imports Main KeYTranslations.TranslationPreamble begin"; + } + + public Path getIsabellePath() { + return isabellePath; + } + + public Path getTranslationPath() { + return translationPath; + } + + public int getTimeout() { + return this.timeoutSeconds; + } + + public void setTimeout(int i) { + timeoutSeconds = i; + } +} diff --git a/keyext.isabelletranslation/src/main/java/org/key_project/isabelletranslation/automation/IsabelleLauncher.java b/keyext.isabelletranslation/src/main/java/org/key_project/isabelletranslation/automation/IsabelleLauncher.java new file mode 100644 index 0000000000..5428bf779b --- /dev/null +++ b/keyext.isabelletranslation/src/main/java/org/key_project/isabelletranslation/automation/IsabelleLauncher.java @@ -0,0 +1,227 @@ +/* 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.automation; + +import java.io.IOException; +import java.util.*; +import java.util.concurrent.*; + +import org.key_project.isabelletranslation.IsabelleTranslationSettings; +import org.key_project.isabelletranslation.gui.controller.IsabelleLauncherProgressDialogMediator; + +import org.jspecify.annotations.NonNull; +import org.slf4j.Logger; +import org.slf4j.LoggerFactory; + +/** + * This class allows for the launch of automated proof searches in Isabelle for a list of isabelle + * problems. + */ +public class IsabelleLauncher implements IsabelleSolverListener { + private static final Logger LOGGER = LoggerFactory.getLogger(IsabelleLauncher.class); + + /** + * The settings used during proof search in Isabelle. + */ + private final IsabelleTranslationSettings settings; + + /** + * The listener objects for this launcher. + * Is used to control the Isabelle dialog with {@link IsabelleLauncherProgressDialogMediator}. + */ + private final List listeners = new ArrayList<>(); + + /** + * The thread, that will be called on shutdown of KeY to ensure there are no runaway Isabelle + * instances or open ThreadPools + */ + private Thread shutdownResources; + + /** + * The ExecutorService used to call the solver instances. + */ + private ExecutorService executorService; + + /** + * The list of currently running solver instances. + */ + private final List runningSolvers = + Collections.synchronizedList(new ArrayList<>()); + + /** + * + */ + private final List finishedSolvers = + Collections.synchronizedList(new ArrayList<>()); + + /** + * The queue of solver instances that have not started yet. + */ + private final LinkedBlockingDeque solverQueue = new LinkedBlockingDeque<>(); + + + public IsabelleLauncher(@NonNull IsabelleTranslationSettings settings) { + this.settings = settings; + } + + /** + * Launches the given problems with the specified timeout using a specified number of concurrent + * Isabelle instances + * + * @param problems The problems for which proof search will be started + * @param timeoutSeconds The timeout setting to use for the Isabelle instances + * @param instanceCount The number of concurrent Isabelle instances + * @throws IOException translation files could not be written + * @throws IsabelleNotFoundException If {@link IsabelleResourceController} fails to initiate + */ + public void launch(List problems, int timeoutSeconds, + int instanceCount) throws IOException, IsabelleNotFoundException { + // Ensure the preamble theory file is present, so theory objects can be created. + // If no problems have translations, don't write anything + // All solvers should recognize this and throw an appropriate exception + List problemsWithTranslation = + problems.stream().filter(IsabelleProblem::hasTranslation).toList(); + + if (!problemsWithTranslation.isEmpty()) { + problemsWithTranslation.get(0).writeTranslationFiles(settings); + } + + + IsabelleResourceController resourceController = + new IsabelleResourceController(instanceCount, settings); + + executorService = Executors.newFixedThreadPool(instanceCount); + + shutdownResources = new Thread(() -> { + executorService.shutdown(); + resourceController.shutdownGracefully(); + finishedSolvers.clear(); + }); + Runtime.getRuntime().addShutdownHook(shutdownResources); + + for (int i = 0; i < problems.size(); i++) { + IsabelleSolver solver = new IsabelleSledgehammerSolver(problems.get(i), List.of(this), + i, resourceController, settings); + solver.setTimeout(timeoutSeconds); + + solverQueue.add(solver); + } + + notifyLauncherStarted(); + + try { + resourceController.init(); + } catch (InterruptedException e) { + stopAll(); + notifyLauncherStopped(); + return; + } + notifyPreparationFinished(); + + LOGGER.info("Setup complete, starting {} problems...", problems.size()); + + try { + executorService.invokeAll(solverQueue); + } catch (InterruptedException e) { + stopAll(); + } catch (RejectedExecutionException e) { + // Launcher has been shutdown before running instances + // Nothing to do here, intended behavior + } finally { + shutdown(); + } + + notifyLauncherStopped(); + } + + /** + * Notifies all listeners of the launcher stop. + */ + private void notifyLauncherStopped() { + listeners.forEach(listener -> listener.launcherStopped(this, finishedSolvers)); + } + + /** + * Notifies all listeners that the launcher has finished preparations. + * This usually means the Isabelle instances have been created by the + * {@link IsabelleResourceController}. + */ + private void notifyPreparationFinished() { + listeners.forEach(listener -> listener.launcherPreparationFinished(this, finishedSolvers)); + } + + /** + * Notifies all listeners that the launcher has started. + */ + private void notifyLauncherStarted() { + listeners.forEach(listener -> listener.launcherStarted(this, new ArrayList<>(solverQueue))); + } + + /** + * Starts the shutdownResources thread, if it was not started already. + * Also removes the shutdown hook. + */ + private void shutdown() { + Runtime.getRuntime().removeShutdownHook(shutdownResources); + if (shutdownResources.getState() == Thread.State.NEW) { + shutdownResources.start(); + } + } + + /** + * Adds a listener. Primarily used for {@link IsabelleLauncherProgressDialogMediator} to update + * the Isabelle dialog. + * + * @param listener The listener to be used + */ + public void addListener(IsabelleLauncherListener listener) { + listeners.add(listener); + } + + /** + * Calls the {@link #shutdown()} function. Then stops the execution of all + * {@link IsabelleSolver} instances that were not started. + * Also interrupts all running solvers. Can be used to perform a user initiated interrupt when + * using IsabelleSolver.ReasonOfInterruption.User. + */ + public void stopAll() { + shutdown(); + + executorService.shutdownNow(); + + solverQueue.forEach(IsabelleSolver::abort); + solverQueue.clear(); + + runningSolvers.forEach(IsabelleSolver::abort); + runningSolvers.clear(); + + notifyLauncherStopped(); + + finishedSolvers.clear(); + } + + @Override + public void processStarted(IsabelleSolver solver, IsabelleProblem problem) { + runningSolvers.add(solver); + if (!solverQueue.remove(solver)) { + LOGGER.error( + "Something went wrong during Isabelle instance management! Solver \"{}\" was not in queue, but started anyway.", + solver.name() + ": " + solver.getProblem().getName()); + stopAll(); + throw new RuntimeException("Something went wrong during Isabelle instance management!"); + } + } + + @Override + public void processError(IsabelleSolver solver, IsabelleProblem problem, Exception e) { + runningSolvers.remove(solver); + finishedSolvers.add(solver); + } + + @Override + public void processStopped(IsabelleSolver solver, IsabelleProblem problem) { + runningSolvers.remove(solver); + finishedSolvers.add(solver); + } +} diff --git a/keyext.isabelletranslation/src/main/java/org/key_project/isabelletranslation/automation/IsabelleLauncherListener.java b/keyext.isabelletranslation/src/main/java/org/key_project/isabelletranslation/automation/IsabelleLauncherListener.java new file mode 100644 index 0000000000..bd7438743d --- /dev/null +++ b/keyext.isabelletranslation/src/main/java/org/key_project/isabelletranslation/automation/IsabelleLauncherListener.java @@ -0,0 +1,23 @@ +/* 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.automation; + +import java.util.Collection; + +/** + * Interface for listener classes for the {@link IsabelleLauncher} + */ +public interface IsabelleLauncherListener { + /** + * Called when the launcher has stopped (both successfully and due to interruptions etc.). + * + * @param launcher The stopped launcher + * @param finishedInstances The instances which have finished processing in the launcher. + */ + void launcherStopped(IsabelleLauncher launcher, Collection finishedInstances); + + void launcherStarted(IsabelleLauncher launcher, Collection solvers); + + void launcherPreparationFinished(IsabelleLauncher launcher, Collection solvers); +} diff --git a/keyext.isabelletranslation/src/main/java/org/key_project/isabelletranslation/automation/IsabelleNotFoundException.java b/keyext.isabelletranslation/src/main/java/org/key_project/isabelletranslation/automation/IsabelleNotFoundException.java new file mode 100644 index 0000000000..45854f9c20 --- /dev/null +++ b/keyext.isabelletranslation/src/main/java/org/key_project/isabelletranslation/automation/IsabelleNotFoundException.java @@ -0,0 +1,12 @@ +/* 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.automation; + +import java.io.IOException; + +public class IsabelleNotFoundException extends IOException { + public IsabelleNotFoundException(String message) { + super(message); + } +} diff --git a/keyext.isabelletranslation/src/main/java/org/key_project/isabelletranslation/automation/IsabelleProblem.java b/keyext.isabelletranslation/src/main/java/org/key_project/isabelletranslation/automation/IsabelleProblem.java new file mode 100644 index 0000000000..9aa64ba6e4 --- /dev/null +++ b/keyext.isabelletranslation/src/main/java/org/key_project/isabelletranslation/automation/IsabelleProblem.java @@ -0,0 +1,142 @@ +/* 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.automation; + +import java.io.File; +import java.io.IOException; +import java.nio.file.Files; + +import de.uka.ilkd.key.proof.Goal; + +import org.key_project.isabelletranslation.IsabelleTranslationSettings; +import org.key_project.isabelletranslation.translation.IllegalFormulaException; + +import org.slf4j.Logger; +import org.slf4j.LoggerFactory; + +/** + * This class represents an Isabelle problem. It contains the goal corresponding to the problem, as + * well as the content of the preamble and translation theory. + * + * @author Nils Buchholz + */ +public class IsabelleProblem { + private static final Logger LOGGER = LoggerFactory.getLogger(IsabelleProblem.class); + + /** + * The goal associated with this problem + */ + private final Goal goal; + + /** + * Content of the preamble theory + */ + private final String preamble; + + /** + * Content of the translation theory + */ + private final String translation; + + /** + * Name of the problem. Contains the serialNr of the associated goal + * Used to display the goal in the rows of Isabelle dialogs + */ + private final String name; + + /** + * Exception encountered during translation + */ + private final IllegalFormulaException exception; + + /** + * Creates a new problem for the given goal. + * + * @param goal the goal associated with this problem + * @param preamble content of the preamble theory + * @param translation content of the translation theory + */ + public IsabelleProblem(Goal goal, String preamble, String translation) { + this.goal = goal; + this.preamble = preamble; + this.translation = translation; + this.name = "Goal " + goal.node().serialNr(); + this.exception = null; + } + + public IsabelleProblem(Goal goal, IllegalFormulaException exception) { + this.goal = goal; + this.preamble = null; + this.translation = null; + this.name = "Goal " + goal.node().serialNr(); + this.exception = exception; + } + + /** + * Returns goal associated with this problem. + * + * @return goal associated with this problem + */ + public Goal getGoal() { + return goal; + } + + /** + * Returns content of translation theory + * + * @return content of translation theory + */ + public String getTranslation() { + return translation; + } + + /** + * Returns content of preamble theory + * + * @return content of preamble theory + */ + public String getPreamble() { + return preamble; + } + + /** + * Returns the name of this problem + * + * @return the name of this problem + */ + public String getName() { + return name; + } + + /** + * Writes the contents of the preamble and translation theory to the files specified in the + * {@link IsabelleTranslationSettings}. + * If the files and directories are not already present, they are created. + * + * @param settings settings to be used + */ + public void writeTranslationFiles(IsabelleTranslationSettings settings) throws IOException { + File translationFile = new File(settings.getTranslationPath() + "/Translation.thy"); + File translationPreambleFile = + new File(settings.getTranslationPath() + "/TranslationPreamble.thy"); + Files.createDirectories(translationFile.toPath().getParent()); + Files.write(translationPreambleFile.toPath(), this.getPreamble().getBytes()); + Files.write(translationFile.toPath(), this.getTranslation().getBytes()); + LOGGER.info("Saved to: {} and {}", translationFile.toPath(), + translationPreambleFile.toPath()); + } + + /** + * Checks if a translation, preamble are present + * + * @return true - both translation and preamble are present, false - otherwise + */ + public boolean hasTranslation() { + return translation != null || preamble != null; + } + + public IllegalFormulaException getTranslationException() { + return exception; + } +} diff --git a/keyext.isabelletranslation/src/main/java/org/key_project/isabelletranslation/automation/IsabelleResource.java b/keyext.isabelletranslation/src/main/java/org/key_project/isabelletranslation/automation/IsabelleResource.java new file mode 100644 index 0000000000..80424e4dbc --- /dev/null +++ b/keyext.isabelletranslation/src/main/java/org/key_project/isabelletranslation/automation/IsabelleResource.java @@ -0,0 +1,48 @@ +/* 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.automation; + +import de.unruh.isabelle.control.Isabelle; +import de.unruh.isabelle.pure.Theory; + +/** + * An IsabelleResource is a bundling of an Isabelle instance and a {@link Theory} derived from that + * instance. + * It can be used to provide solvers with these values for computation. + */ +public interface IsabelleResource { + /** + * Checks if the resource has been destroyed. If this is true the resource should not be used + * anymore. + * + * @return true - resource destroyed, false otherwise + */ + boolean isDestroyed(); + + /** + * Destroys the resource. Usually by destroying the Isabelle instance. + */ + void destroy(); + + /** + * Interrupts the Isabelle instance. + */ + void interrupt(); + + /** + * Returns the instance matching the {@link Theory} returned by + * {@link IsabelleResource#theory()} + * + * @return {@link Isabelle} usable with {@link IsabelleResource#theory()} + */ + Isabelle instance(); + + /** + * Returns the {@link Theory} matching the {@link Isabelle} returned by + * {@link IsabelleResource#instance()} + * + * @return {@link Theory} usable with {@link IsabelleResource#instance()} + */ + Theory theory(); +} diff --git a/keyext.isabelletranslation/src/main/java/org/key_project/isabelletranslation/automation/IsabelleResourceController.java b/keyext.isabelletranslation/src/main/java/org/key_project/isabelletranslation/automation/IsabelleResourceController.java new file mode 100644 index 0000000000..921141f799 --- /dev/null +++ b/keyext.isabelletranslation/src/main/java/org/key_project/isabelletranslation/automation/IsabelleResourceController.java @@ -0,0 +1,307 @@ +/* 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.automation; + +import java.nio.file.Path; +import java.util.ArrayList; +import java.util.concurrent.*; + +import org.key_project.isabelletranslation.IsabelleTranslationSettings; + +import de.unruh.isabelle.control.Isabelle; +import de.unruh.isabelle.control.IsabelleMLException; +import de.unruh.isabelle.java.JIsabelle; +import de.unruh.isabelle.mlvalue.ListConverter; +import de.unruh.isabelle.mlvalue.MLFunction2; +import de.unruh.isabelle.mlvalue.MLFunction3; +import de.unruh.isabelle.mlvalue.MLValue; +import de.unruh.isabelle.pure.Implicits; +import de.unruh.isabelle.pure.Position; +import de.unruh.isabelle.pure.Theory; +import de.unruh.isabelle.pure.TheoryHeader; +import org.slf4j.Logger; +import org.slf4j.LoggerFactory; +import scala.collection.immutable.List; + +/** + * This class handles creation of Isabelle instances, as well as providing methods for their + * destruction. + * This class also acts as a semaphore for Isabelle instances. + * The Isabelle instances are bundled with a {@link Theory} into a {@link IsabelleResource} for this + * purpose. + */ +public class IsabelleResourceController { + private static final Logger LOGGER = LoggerFactory.getLogger(IsabelleResourceController.class); + /** + * The idle Isabelle instances. + */ + private final LinkedBlockingQueue idleInstances; + + /** + * The settings to be used. Needed for path to Isabelle + */ + private final IsabelleTranslationSettings settings; + + /** + * Flag to check for shutdowns. + */ + private boolean isShutdown = false; + + /** + * Queue of threads waiting for Isabelle resources. + */ + private final LinkedBlockingQueue waitingThreads; + + /** + * The number of Isabelle instances to create and store in this semaphore. + */ + private final int numberOfInstances; + + /** + * Thread pool for instance creation + */ + private final ExecutorService instanceCreatorService; + + /** + * Semaphore to ensure fairness when taking Isabelle instance. + */ + private final Semaphore takeSemaphore; + + + /** + * Creates a resource controller. Initializes the settings. + * + * @param numberOfInstances the maximum number of Isabelle instances to create at any time + * @param settings {@link IsabelleTranslationSettings} to be used + */ + public IsabelleResourceController(int numberOfInstances, IsabelleTranslationSettings settings) { + this.settings = settings; + idleInstances = new LinkedBlockingQueue<>(numberOfInstances); + waitingThreads = new LinkedBlockingQueue<>(); + this.numberOfInstances = numberOfInstances; + instanceCreatorService = Executors.newFixedThreadPool(numberOfInstances); + takeSemaphore = new Semaphore(1, true); + } + + /** + * Creates the Isabelle instances. + * + * @throws IsabelleNotFoundException If instance creation failed. + */ + public void init() throws IsabelleNotFoundException, InterruptedException { + for (int i = 0; i < numberOfInstances; i++) { + if (!isShutdown()) { + IsabelleResource newResource = createIsabelleResource(); + idleInstances.add(newResource); + } + } + } + + /** + * Tries to acquire a Isabelle instance. Fairness is ensured by a semaphore. + * + * @return an idle Isabelle resource + * @throws InterruptedException if the thread is interrupted while waiting + */ + public IsabelleResource getIsabelleResource() throws InterruptedException { + waitingThreads.add(Thread.currentThread()); + takeSemaphore.acquire(); + try { + return idleInstances.take(); + } finally { + waitingThreads.remove(Thread.currentThread()); + takeSemaphore.release(); + } + } + + /** + * Calls {@link ExecutorService#shutdownNow()} for the instance creator service thereby stopping + * instance creation. + *

+ * Interrupts all waiting threads. + *

+ * Destroys all idle instances. + */ + public void shutdownGracefully() { + isShutdown = true; + + instanceCreatorService.shutdownNow(); + + waitingThreads.forEach(Thread::interrupt); + waitingThreads.clear(); + + idleInstances.forEach(IsabelleResource::destroy); + idleInstances.clear(); + } + + /** + * Adds a resource to the queue. The resource is interrupted via + * {@link IsabelleResource#interrupt()} to ensure it is idle. + *

+ * If the controller is shutdown the resource is destroyed instead. + * + * @param resource the resource to return + */ + public void returnResource(IsabelleResource resource) { + assert resource != null; + + if (isShutdown()) { + if (!resource.isDestroyed()) { + resource.destroy(); + } + return; + } + + if (resource.isDestroyed()) { + try { + resource = createIsabelleResource(); + } catch (IsabelleNotFoundException e) { + // Should not occur. If it was possible to create instances during creation, it + // should be possible now. + shutdownGracefully(); + LOGGER.error(e.getMessage()); + } catch (InterruptedException e) { + shutdownGracefully(); + LOGGER.error(e.getMessage()); + Thread.currentThread().interrupt(); + } + } else { + resource.interrupt(); + } + idleInstances.offer(resource); + } + + /** + * Checks if the controller is shutdown. + * + * @return true - controller is shutdown, false - otherwise + */ + public boolean isShutdown() { + return isShutdown; + } + + /** + * Creates a new {@link IsabelleResource} via the thread pool used for this purpose. + * + * @return fresh IsabelleResource + * @throws IsabelleNotFoundException if instance creation failed + */ + private IsabelleResource createIsabelleResource() + throws IsabelleNotFoundException, InterruptedException { + Callable creationTask = () -> { + Isabelle isabelleInstance = startIsabelleInstance(); + Theory theory = beginTheory(isabelleInstance, settings); + return new IsabelleResourceImpl(isabelleInstance, theory); + }; + try { + return instanceCreatorService.submit(creationTask).get(); + } catch (ExecutionException e) { + LOGGER.error("Error during Isabelle setup"); + + if (e.getCause() instanceof IsabelleNotFoundException) { + throw (IsabelleNotFoundException) e.getCause(); + } + if (e.getCause() instanceof InterruptedException) { + throw (InterruptedException) e.getCause(); + } + throw new RuntimeException(e); + } catch (RejectedExecutionException e) { + throw new RuntimeException("Unreachable code during Isabelle instance creation"); + } + } + + /** + * Starts an Isabelle instance using the Isabelle installation location provided by the user in + * the settings. + * + * @return freshly started Isabelle instance + * @throws IsabelleNotFoundException if Isabelle could not be found at the location stored in + * the settings + */ + private Isabelle startIsabelleInstance() throws IsabelleNotFoundException { + ArrayList sessionRoots = new ArrayList<>(); + sessionRoots.add(settings.getTranslationPath()); + Isabelle isabelle; + try { + Isabelle.Setup setup = JIsabelle.setupSetLogic("KeYTranslations", + JIsabelle.setupSetSessionRoots(sessionRoots, + JIsabelle.setupSetWorkingDirectory(settings.getTranslationPath(), + JIsabelle.setup(settings.getIsabellePath())))); + isabelle = new Isabelle(setup); + } catch (Exception e) { + LOGGER.error("Can't find Isabelle at {}", settings.getIsabellePath()); + throw new IsabelleNotFoundException( + "Can't find Isabelle at " + settings.getIsabellePath()); + } + return isabelle; + } + + /** + * Creates a theory object for use in solvers. + *

+ * Requires the translation theories to be present. + * + * @param isabelle The Isabelle instance, which creates the theory object + * @param settings Isabelle settings, which show the location of the translation theories + * @return Theory object matching the given isabelle instance + */ + private static Theory beginTheory(Isabelle isabelle, IsabelleTranslationSettings settings) { + MLFunction3, Theory> begin_theory = + MLValue.compileFunction( + "fn (path, header, parents) => Resources.begin_theory path header parents", + isabelle, + Implicits.pathConverter(), Implicits.theoryHeaderConverter(), + new ListConverter<>(Implicits.theoryConverter()), Implicits.theoryConverter()); + MLFunction2 header_read = + MLValue.compileFunction("fn (text,pos) => Thy_Header.read pos text", isabelle, + de.unruh.isabelle.mlvalue.Implicits.stringConverter(), + Implicits.positionConverter(), Implicits.theoryHeaderConverter()); + + + TheoryHeader header = header_read + .apply(settings.getHeader(), Position.none(isabelle), isabelle, + de.unruh.isabelle.mlvalue.Implicits.stringConverter(), + Implicits.positionConverter()) + .retrieveNow(Implicits.theoryHeaderConverter(), isabelle); + Path topDir = settings.getTranslationPath(); + + + return begin_theory.apply(topDir, header, + header.imports(isabelle).map((String name) -> Theory.apply(name, isabelle)), isabelle, + Implicits.pathConverter(), Implicits.theoryHeaderConverter(), + new ListConverter<>(Implicits.theoryConverter())) + .retrieveNow(Implicits.theoryConverter(), isabelle); + } + + /** + * A record bundling a given instance to a theory. This is necessary as a theory object is only usable in conjunction with the instance used to create it. + * + * @param instance the instance + * @param theory the theory + */ + private record IsabelleResourceImpl(Isabelle instance, Theory theory) implements IsabelleResource { + + @Override + public boolean isDestroyed() { + return instance.isDestroyed(); + } + + @Override + public void destroy() { + instance.destroy(); + } + + private void interruptIntern() throws IsabelleMLException { + instance.executeMLCodeNow("error \"Interrupt\""); + } + + @Override + public void interrupt() { + try { + interruptIntern(); + } catch (IsabelleMLException e) { + // Always throws this due to the way Isabelle is interrupted. + } + } +}} diff --git a/keyext.isabelletranslation/src/main/java/org/key_project/isabelletranslation/automation/IsabelleResult.java b/keyext.isabelletranslation/src/main/java/org/key_project/isabelletranslation/automation/IsabelleResult.java new file mode 100644 index 0000000000..604071ba40 --- /dev/null +++ b/keyext.isabelletranslation/src/main/java/org/key_project/isabelletranslation/automation/IsabelleResult.java @@ -0,0 +1,205 @@ +/* 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.automation; + +import java.time.Duration; + +/** + * This class stores the result of a {@link IsabelleSolver}. + * This includes computation times and in some cases successful tactics and exceptions. + */ +public class IsabelleResult { + /** + * Returns a {@link String} description of the type of this result. + * + * @return description of the type of result this is + */ + public String getDescription() { + return this.type.getDescription(); + } + + /** + * Returns the type of result this is + * + * @return the type of result this is + */ + public Type getType() { + return this.type; + } + + /** + * Enum containing different types of Results. + */ + public enum Type { + /** + * Successful result. (Proof found) + */ + SUCCESS("Success"), + /** + * Error result. (Encountered exception) + */ + ERROR("Error"), + /** + * Timeout result. (No proof found in time) + */ + TIMEOUT("Timeout"), + /** + * Interrupt result. (Interrupt during proof search) + */ + INTERRUPTED("Interrupted"), + /** + * Unknown result. (Something went wrong, but unknown what did) + */ + UNKNOWN("Unknown"); + + Type(String description) { + this.description = description; + } + + private final String description; + + /** + * Returns a {@link String} description of the result type. + * + * @return a {@link String} description of the result type. + */ + public String getDescription() { + return description; + } + } + + /** + * The type of this result + */ + private final Type type; + + /** + * The computation time for this result. Only set for successful and timeout results. + */ + private final Duration computationTime; + + /** + * A successful tactic returned by an Isabelle automation method + */ + private final String successfulTactic; + + /** + * An exception thrown during computation by the solver + */ + private final Exception exception; + + private IsabelleResult(Type type, Duration computationTime, String successfulTactic, + Exception exception) { + this.type = type; + this.computationTime = computationTime; + this.successfulTactic = successfulTactic; + this.exception = exception; + } + + /** + * Creates a timeout result. + * + * @param computationTime the time taken for timeout to occur + * @return Isabelle result representing a timeout + */ + public static IsabelleResult getTimeoutResult(Duration computationTime) { + return new IsabelleResult(Type.TIMEOUT, computationTime, null, null); + } + + /** + * Returns an error result + * + * @param exception the exception that caused computation to fail + * @return Isabelle result representing an error + */ + public static IsabelleResult getErrorResult(Exception exception) { + return new IsabelleResult(Type.ERROR, null, null, exception); + } + + /** + * Creates a successful result + * + * @param successfulTactic the successful tactic found by a solver + * @param computationTime time taken for proof search + * @return Isabelle result representing a success + */ + public static IsabelleResult getSuccessResult(String successfulTactic, + Duration computationTime) { + return new IsabelleResult(Type.SUCCESS, computationTime, successfulTactic, null); + } + + /** + * Creates an interrupt result + * + * @return Isabelle result representing an Interrupt + */ + public static IsabelleResult getInterruptedResult() { + return new IsabelleResult(Type.INTERRUPTED, null, null, null); + } + + /** + * Creates an unknown result + * + * @return Isabelle result representing an unknown result + */ + public static IsabelleResult getUnknownResult() { + return new IsabelleResult(Type.UNKNOWN, null, null, null); + } + + + + /** + * Is this result successful? + * + * @return true - if successful, false - otherwise + */ + public boolean isSuccessful() { + return type == Type.SUCCESS; + } + + /** + * Is this an error result? + * + * @return true - if error, false - otherwise + */ + public boolean isError() { + return type == Type.ERROR; + } + + /** + * Is this a timeout result? + * + * @return true - if timeout, false - otherwise + */ + public boolean isTimeout() { + return type == Type.TIMEOUT; + } + + public Duration getComputationTime() { + return this.computationTime; + } + + /** + * Getter for exception + * + * @return exception encountered during proving || null if not error result + */ + public Exception getException() { + return this.exception; + } + + /** + * Successful proof tactic + * + * @return successful tactic || null if not successful + */ + public String getSuccessfulTactic() { + return this.successfulTactic; + } + + @Override + public String toString() { + return getDescription(); + } +} diff --git a/keyext.isabelletranslation/src/main/java/org/key_project/isabelletranslation/automation/IsabelleRuleApp.java b/keyext.isabelletranslation/src/main/java/org/key_project/isabelletranslation/automation/IsabelleRuleApp.java new file mode 100644 index 0000000000..39709ecb07 --- /dev/null +++ b/keyext.isabelletranslation/src/main/java/org/key_project/isabelletranslation/automation/IsabelleRuleApp.java @@ -0,0 +1,131 @@ +/* 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.automation; + +import java.util.ArrayList; +import java.util.List; + +import de.uka.ilkd.key.java.Services; +import de.uka.ilkd.key.logic.*; +import de.uka.ilkd.key.proof.Goal; +import de.uka.ilkd.key.rule.AbstractExternalSolverRuleApp; +import de.uka.ilkd.key.rule.RuleApp; + +import org.key_project.logic.Name; +import org.key_project.util.collection.ImmutableList; + +import org.jspecify.annotations.NonNull; + +public class IsabelleRuleApp extends AbstractExternalSolverRuleApp { + public static final IsabelleRule RULE = new IsabelleRule(); + + protected IsabelleRuleApp(IsabelleRule rule, PosInOccurrence pio, String successfulSolverName, + String successfulTactic) { + this(rule, pio, null, successfulSolverName, + "Isabelle " + successfulSolverName + ": " + successfulTactic); + } + + protected IsabelleRuleApp(IsabelleRule rule, PosInOccurrence pio, + ImmutableList ifInsts, String successfulSolverName) { + this(rule, pio, ifInsts, successfulSolverName, "Isabelle: " + successfulSolverName); + } + + private IsabelleRuleApp(IsabelleRule rule, PosInOccurrence pio, + ImmutableList ifInsts, String successfulSolverName, String title) { + super(rule, pio, ifInsts, successfulSolverName, title); + } + + @Override + public IsabelleRuleApp setTitle(String title) { + return new IsabelleRuleApp(RULE, pio, ifInsts, successfulSolverName, title); + } + + @Override + public IsabelleRuleApp replacePos(PosInOccurrence newPos) { + return new IsabelleRuleApp(RULE, newPos, successfulSolverName, title); + } + + @Override + public IsabelleRuleApp tryToInstantiate(Goal goal) { + IsabelleRuleApp app = RULE.createApp(pio, goal.proof().getServices()); + Sequent seq = goal.sequent(); + List ifInsts = new ArrayList<>(); + for (SequentFormula ante : seq.antecedent()) { + ifInsts.add(new PosInOccurrence(ante, PosInTerm.getTopLevel(), true)); + } + for (SequentFormula succ : seq.succedent()) { + ifInsts.add(new PosInOccurrence(succ, PosInTerm.getTopLevel(), false)); + } + return app.setIfInsts(ImmutableList.fromList(ifInsts)); + } + + @Override + public IsabelleRuleApp setIfInsts(ImmutableList ifInsts) { + setMutable(ifInsts); + return this; + } + + @Override + public IsabelleRule rule() { + return RULE; + } + + public static class IsabelleRule implements ExternalSolverRule { + Name name = new Name("IsabelleRule"); + + public IsabelleRuleApp createApp(String successfulSolverName, + String successfulTactic) { + return new IsabelleRuleApp(this, null, successfulSolverName, successfulTactic); + } + + @Override + public IsabelleRuleApp createApp(String successfulSolverName) { + return new IsabelleRuleApp(this, null, successfulSolverName, ""); + } + + @Override + public IsabelleRuleApp createApp(String successfulSolverName, + ImmutableList unsatCore) { + return new IsabelleRuleApp(this, null, unsatCore, successfulSolverName); + } + + @Override + public IsabelleRuleApp createApp(PosInOccurrence pos, TermServices services) { + return new IsabelleRuleApp(this, null, "", ""); + } + + /** + * Create a new goal (to be closed in {@link Goal#apply(RuleApp)} directly afterwards) + * with the same sequent as the given one. + * + * @param goal the Goal on which to apply ruleApp + * @param services the Services with the necessary information about the java programs + * @param ruleApp the rule application to be executed + * @return a list with an identical goal as the given goal + */ + @Override + @NonNull + public ImmutableList apply(Goal goal, Services services, RuleApp ruleApp) { + if (goal.proof().getInitConfig().getJustifInfo().getJustification(RULE) == null) { + goal.proof().getInitConfig().registerRule(RULE, () -> false); + } + return goal.split(1); + } + + @Override + public String toString() { + return displayName(); + } + + @Override + public String displayName() { + return "Isabelle"; + } + + @Override + public Name name() { + return name; + } + } +} diff --git a/keyext.isabelletranslation/src/main/java/org/key_project/isabelletranslation/automation/IsabelleSledgehammerSolver.java b/keyext.isabelletranslation/src/main/java/org/key_project/isabelletranslation/automation/IsabelleSledgehammerSolver.java new file mode 100644 index 0000000000..7b425a8589 --- /dev/null +++ b/keyext.isabelletranslation/src/main/java/org/key_project/isabelletranslation/automation/IsabelleSledgehammerSolver.java @@ -0,0 +1,454 @@ +/* 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.automation; + +import java.time.Instant; +import java.util.ArrayList; +import java.util.Collection; +import java.util.HashSet; +import java.util.concurrent.TimeUnit; +import java.util.concurrent.TimeoutException; + +import org.key_project.isabelletranslation.IsabelleTranslationSettings; + +import de.unruh.isabelle.control.Isabelle; +import de.unruh.isabelle.control.IsabelleMLException; +import de.unruh.isabelle.mlvalue.*; +import de.unruh.isabelle.pure.Implicits; +import de.unruh.isabelle.pure.Theory; +import de.unruh.isabelle.pure.ToplevelState; +import de.unruh.isabelle.pure.Transition; +import org.slf4j.Logger; +import org.slf4j.LoggerFactory; +import scala.Tuple2; +import scala.collection.immutable.List; +import scala.collection.mutable.Builder; +import scala.concurrent.Await; +import scala.concurrent.Future; +import scala.concurrent.duration.Duration; + +/** + * Implementation of {@link IsabelleSolver} using Sledgehammer. + */ +public class IsabelleSledgehammerSolver implements IsabelleSolver { + /** + * Needed for UI + */ + private final int solverIndex; + + /** + * The result of this solver. + */ + private IsabelleResult result; + + /** + * + */ + private IsabelleResource isabelleResource; + + /** + * The problem that is related to this solver + */ + private final IsabelleProblem problem; + + /** + * the state the solver is currently in + */ + private SolverState solverState = SolverState.Waiting; + + /** + * Stores the settings that are used for the execution. + */ + private final IsabelleTranslationSettings isabelleSettings; + + /** + * If there was an exception while executing the solver it is stored in this attribute. + */ + private Throwable exception; + + /** + * The timeout in seconds for this solver run. + */ + private int timeout; + + private Instant startTime; + + private java.time.Duration computationTime; + + private final IsabelleResourceController resourceController; + + + private static final Logger LOGGER = LoggerFactory.getLogger(IsabelleSledgehammerSolver.class); + private final Collection listeners; + private String rawOutput; + + public IsabelleSledgehammerSolver(IsabelleProblem problem, + Collection listeners, int solverIndex, + IsabelleResourceController resourceController, IsabelleTranslationSettings settings) { + this.problem = problem; + this.solverIndex = solverIndex; + this.listeners = new HashSet<>(); + this.listeners.addAll(listeners); + this.resourceController = resourceController; + this.isabelleSettings = settings; + this.timeout = isabelleSettings.getTimeout(); + } + + @Override + public int getSolverIndex() { + return solverIndex; + } + + @Override + public String name() { + return "sledgehammer"; + } + + @Override + public IsabelleProblem getProblem() { + return problem; + } + + @Override + public Throwable getException() { + return exception; + } + + @Override + public void abort() { + // If solver already completed, the interrupt should be ignored + handleInterrupt(new InterruptedException()); + } + + /** + * Returns the resource used by this solver to the controller. + */ + private void returnResource() { + if (isabelleResource == null) { + return; + } + resourceController.returnResource(isabelleResource); + isabelleResource = null; + } + + private void setSolverState(SolverState solverState) { + this.solverState = solverState; + } + + @Override + public Instant getStartTime() { + return startTime; + } + + @Override + public int getTimeout() { + return this.timeout; + } + + @Override + public void setTimeout(int timeout) { + this.timeout = timeout; + } + + @Override + public SolverState getState() { + return solverState; + } + + @Override + public String getRawSolverOutput() { + return rawOutput; + } + + @Override + public String getRawSolverInput() { + return problem.getTranslation(); + } + + @Override + public IsabelleResult getFinalResult() { + return this.result; + } + + + @Override + public IsabelleResult call() throws InterruptedException { + // Return error result, if problem does not have a translation + if (!problem.hasTranslation()) { + return handleIsabelleError(problem.getTranslationException()); + } + + // Ensure there is an active IsabelleInstance + setSolverState(SolverState.Preparing); + try { + isabelleResource = resourceController.getIsabelleResource(); + } catch (InterruptedException e) { + return handleInterrupt(e); + } + + notifyProcessStarted(); + startTime = Instant.now(); + + LOGGER.info("Parsing theory for: {}", problem.getName()); + setSolverState(SolverState.Parsing); + ToplevelState toplevel; + try { + toplevel = parseTheory(isabelleResource); + } catch (InterruptedException e) { + return handleInterrupt(e); + } catch (IsabelleMLException e) { + return handleIsabelleError(e); + } + LOGGER.info("Finished Parsing"); + + + setSolverState(SolverState.Running); + try { + if (!setFinalResult(sledgehammer(isabelleResource, toplevel))) { + return this.result; + } + } catch (TimeoutException e) { + setComputationTime(); + if (!setFinalResult(IsabelleResult.getTimeoutResult(getComputationTime()))) { + return this.result; + } + } catch (InterruptedException e) { + return handleInterrupt(e); + } catch (IsabelleMLException e) { + return handleIsabelleError(e); + } + LOGGER.info("Sledgehammer result: {}", this.result.getDescription()); + returnResource(); + setSolverState(SolverState.Stopped); + notifyProcessFinished(); + return this.result; + } + + /** + * Parse the content of a theory and return the resulting toplevelstate. + * + * @param resource Isabelle resource to use + * @return {@link ToplevelState} of the parsed theory + * @throws InterruptedException If interrupted while parsing + * @throws IsabelleMLException if parsing fails on the side of Isabelle + */ + private ToplevelState parseTheory(IsabelleResource resource) + throws InterruptedException, IsabelleMLException { + Isabelle isabelle = resource.instance(); + Theory thy0 = resource.theory(); + ToplevelState result = ToplevelState.apply(isabelle); + + if (Thread.currentThread().isInterrupted()) { + throw new InterruptedException(); + } + MLFunction2>> parse_text = + MLValue.compileFunction( + """ + fn (thy, text) => let + val transitions = Outer_Syntax.parse_text thy (K thy) Position.start text + fun addtext symbols [tr] = + [(tr, implode symbols)] + | addtext _ [] = [] + | addtext symbols (tr::nextTr::trs) = let + val (this,rest) = Library.chop (Position.distance_of (Toplevel.pos_of tr, Toplevel.pos_of nextTr) |> Option.valOf) symbols + in (tr, implode this) :: addtext rest (nextTr::trs) end + in addtext (Symbol.explode text) transitions end""", + isabelle, + Implicits.theoryConverter(), de.unruh.isabelle.mlvalue.Implicits.stringConverter(), + new ListConverter<>(new Tuple2Converter<>(Implicits.transitionConverter(), + de.unruh.isabelle.mlvalue.Implicits.stringConverter()))); + + if (Thread.currentThread().isInterrupted()) { + throw new InterruptedException(); + } + MLFunction3 command_exception = + MLValue.compileFunction("fn (int, tr, st) => Toplevel.command_exception int tr st", + isabelle, + de.unruh.isabelle.mlvalue.Implicits.booleanConverter(), + Implicits.transitionConverter(), Implicits.toplevelStateConverter(), + Implicits.toplevelStateConverter()); + + java.util.List> transitionsAndTexts = new ArrayList<>(); + List> transitionList = + parse_text.apply(thy0, getProblem().getTranslation(), isabelle, + Implicits.theoryConverter(), de.unruh.isabelle.mlvalue.Implicits.stringConverter()) + .retrieveNow( + new ListConverter<>(new Tuple2Converter<>(Implicits.transitionConverter(), + de.unruh.isabelle.mlvalue.Implicits.stringConverter())), + isabelle); + transitionList.foreach(transitionsAndTexts::add); + + for (Tuple2 transitionAndText : transitionsAndTexts) { + // println(s"""Transition: "${text.strip}"""") + if (Thread.currentThread().isInterrupted()) { + throw new InterruptedException(); + } + result = command_exception.apply(Boolean.TRUE, transitionAndText._1(), result, isabelle, + de.unruh.isabelle.mlvalue.Implicits.booleanConverter(), + Implicits.transitionConverter(), Implicits.toplevelStateConverter()) + .retrieveNow(Implicits.toplevelStateConverter(), isabelle); + } + return result; + } + + /** + * Uses sledgehammer to search for a proof + * + * @param resource the resource to use for ML requests + * @param toplevel the toplevelstate of the theory to search a proof for + * @return IsabelleResult + * + * success - proof found + * timeout - timed out during proof search + * interrupt - interrupted during proof search + * error - encountered exception during proof search + * @throws TimeoutException if proof search timed out + * @throws InterruptedException if interrupted during proof search + * @throws IsabelleMLException if Isabelle reported an error + */ + private IsabelleResult sledgehammer(IsabelleResource resource, + ToplevelState toplevel) + throws TimeoutException, InterruptedException, IsabelleMLException { + Isabelle isabelle = resource.instance(); + Theory thy0 = resource.theory(); + + String sledgehammer = thy0.importMLStructureNow("Sledgehammer", isabelle); + String Sledgehammer_Commands = thy0.importMLStructureNow("Sledgehammer_Commands", isabelle); + String Sledgehammer_Prover = thy0.importMLStructureNow("Sledgehammer_Prover", isabelle); + MLFunction4, scala.collection.immutable.List, Tuple2>>> normal_with_Sledgehammer = + MLValue.compileFunction( + """ + fn (state, thy, adds, dels) => + let + val override = {add=[],del=[],only=false}; + fun go_run (state, thy) = + let + val p_state = Toplevel.proof_of state; + val ctxt = Proof.context_of p_state; + val params =\s""" + Sledgehammer_Commands + """ + .default_params thy + [("timeout",\"""" + (double) timeout + + """ + "),("verbose","true"),("provers", "cvc4 verit z3 spass vampire zipperposition")]; + val results =\s""" + + sledgehammer + """ + .run_sledgehammer params\s""" + Sledgehammer_Prover + """ + .Normal NONE 1 override p_state; + val (result, (outcome, step)) = results; + in + (result, (""" + sledgehammer + """ + .short_string_of_sledgehammer_outcome outcome, [YXML.content_of step])) + end; + in + Timeout.apply (Time.fromSeconds\s + """ + getTimeout() + ") go_run (state, thy) end", + isabelle, Implicits.toplevelStateConverter(), Implicits.theoryConverter(), + new ListConverter<>(de.unruh.isabelle.mlvalue.Implicits.stringConverter()), + new ListConverter<>(de.unruh.isabelle.mlvalue.Implicits.stringConverter()), + (new Tuple2Converter<>(de.unruh.isabelle.mlvalue.Implicits.booleanConverter(), + new Tuple2Converter<>(de.unruh.isabelle.mlvalue.Implicits.stringConverter(), + new ListConverter<>( + de.unruh.isabelle.mlvalue.Implicits.stringConverter()))))); + + + Builder> listBuilder = scala.collection.immutable.List.newBuilder(); + scala.collection.immutable.List emptyList = listBuilder.result(); + + Future>>> resultFuture = + normal_with_Sledgehammer + .apply(toplevel, thy0, emptyList, emptyList, isabelle, + Implicits.toplevelStateConverter(), Implicits.theoryConverter(), + new ListConverter<>(de.unruh.isabelle.mlvalue.Implicits.stringConverter()), + new ListConverter<>(de.unruh.isabelle.mlvalue.Implicits.stringConverter())) + .retrieve( + new Tuple2Converter<>( + de.unruh.isabelle.mlvalue.Implicits.booleanConverter(), + new Tuple2Converter<>( + de.unruh.isabelle.mlvalue.Implicits.stringConverter(), + new ListConverter<>( + de.unruh.isabelle.mlvalue.Implicits.stringConverter()))), + isabelle); + Tuple2>> resultFutureCollect = + Await.result(resultFuture, Duration.create(getTimeout(), TimeUnit.SECONDS)); + + rawOutput = resultFutureCollect._2().toString(); + + boolean successful = (boolean) resultFutureCollect._1(); + setComputationTime(); + if (successful) { + String successfulTactic = resultFutureCollect._2()._2().head().split("Try this: ")[1]; + return IsabelleResult.getSuccessResult(successfulTactic, + getComputationTime()); + } else { + return IsabelleResult.getUnknownResult(); + } + } + + /** + * Handles an interrupt encountered during proof search + * + * @return Interrupt result + */ + private IsabelleResult handleInterrupt(InterruptedException e) { + setFinalResult(IsabelleResult.getInterruptedResult()); + returnResource(); + setComputationTime(); + Thread.currentThread().interrupt(); + setSolverState(SolverState.Stopped); + notifyProcessError(e); + return this.result; + } + + /** + * Handles an error encountered during proof search + * + * @return error result + */ + private IsabelleResult handleIsabelleError(Exception e) { + setFinalResult(IsabelleResult.getErrorResult(e)); + setComputationTime(); + this.exception = e; + returnResource(); + setSolverState(SolverState.Stopped); + notifyProcessError(e); + return this.result; + } + + @Override + public java.time.Duration getComputationTime() { + return computationTime; + } + + private void setComputationTime() { + if (getStartTime() != null) { + computationTime = java.time.Duration.between(getStartTime(), Instant.now()); + } + } + + private synchronized boolean setFinalResult(IsabelleResult result) { + if (this.result == null) { + this.result = result; + return true; + } + return false; + } + + private void notifyProcessStarted() { + for (IsabelleSolverListener listener : listeners) { + listener.processStarted(this, getProblem()); + } + } + + private void notifyProcessFinished() { + for (IsabelleSolverListener listener : listeners) { + listener.processStopped(this, getProblem()); + } + } + + private void notifyProcessError(Exception e) { + for (IsabelleSolverListener listener : listeners) { + listener.processError(this, getProblem(), e); + } + } +} diff --git a/keyext.isabelletranslation/src/main/java/org/key_project/isabelletranslation/automation/IsabelleSolver.java b/keyext.isabelletranslation/src/main/java/org/key_project/isabelletranslation/automation/IsabelleSolver.java new file mode 100644 index 0000000000..5fc97fa03e --- /dev/null +++ b/keyext.isabelletranslation/src/main/java/org/key_project/isabelletranslation/automation/IsabelleSolver.java @@ -0,0 +1,110 @@ +/* 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.automation; + +import java.time.Duration; +import java.time.Instant; +import java.util.concurrent.Callable; + +/** + * An Isabelle solver. May use different methods to arrive at the result. + * Implements callable. Thread management must be handled by callers. + */ +public interface IsabelleSolver extends Callable { + /** + * UI component index + * + * @return the index corresponding to this solver + */ + int getSolverIndex(); + + /** + * state of the solver + */ + enum SolverState { + Waiting, Preparing, Parsing, Running, Stopped + } + + /** + * Name for the solver instance + * + * @return name of the solver instance + */ + String name(); + + /** + * Getter for the problem this solver will work on + * + * @return The problem this solver will work on + */ + IsabelleProblem getProblem(); + + /** + * Returns the Exception encountered during proof search + * + * @return exception encountered during proof search, if any was encountered. + */ + Throwable getException(); + + /** + * aborts processing + */ + void abort(); + + /** + * Getter for start time of the solver + * + * @return Time solver started computing (after preparation) + */ + Instant getStartTime(); + + /** + * Getter for computation time + * + * @return computation time before solver stopped + */ + Duration getComputationTime(); + + /** + * Returns the timeout time for solver in seconds + * + * @return timeout time for solver + */ + int getTimeout(); + + /** + * Sets the timeout value for this solver (in seconds) + * + * @param timeout timeout in seconds (negative values may cause unexpected behavior) + */ + void setTimeout(int timeout); + + /** + * Getter for current solver state + * + * @return current solver state + */ + SolverState getState(); + + /** + * Raw output of solver + * + * @return raw output of solver + */ + String getRawSolverOutput(); + + /** + * Raw string of translation theory (not preamble) + * + * @return raw input of solver + */ + String getRawSolverInput(); + + /** + * The final result of solver. Recommended to be null, prior to solver completion. + * + * @return final result of solver + */ + IsabelleResult getFinalResult(); +} diff --git a/keyext.isabelletranslation/src/main/java/org/key_project/isabelletranslation/automation/IsabelleSolverListener.java b/keyext.isabelletranslation/src/main/java/org/key_project/isabelletranslation/automation/IsabelleSolverListener.java new file mode 100644 index 0000000000..e11ca49072 --- /dev/null +++ b/keyext.isabelletranslation/src/main/java/org/key_project/isabelletranslation/automation/IsabelleSolverListener.java @@ -0,0 +1,34 @@ +/* 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.automation; + +/** + * Listener for {@link IsabelleSolver}s. + */ +public interface IsabelleSolverListener { + /** + * Solver has started. Called after finishing preparations. + * + * @param solver the solver + * @param problem the problem the solver is working on + */ + void processStarted(IsabelleSolver solver, IsabelleProblem problem); + + /** + * Solver has encountered an error. + * + * @param solver the solver + * @param problem the problem the solver is working on + * @param e the exception the solver encountered + */ + void processError(IsabelleSolver solver, IsabelleProblem problem, Exception e); + + /** + * Solver has stopped as planned + * + * @param solver the solver + * @param problem the problem the solver is working on + */ + void processStopped(IsabelleSolver solver, IsabelleProblem problem); +} diff --git a/keyext.isabelletranslation/src/main/java/org/key_project/isabelletranslation/gui/InformationWindow.java b/keyext.isabelletranslation/src/main/java/org/key_project/isabelletranslation/gui/InformationWindow.java new file mode 100644 index 0000000000..0c879c18ee --- /dev/null +++ b/keyext.isabelletranslation/src/main/java/org/key_project/isabelletranslation/gui/InformationWindow.java @@ -0,0 +1,98 @@ +/* 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.gui; + +import java.awt.*; +import java.util.Collection; +import javax.swing.*; +import javax.swing.event.DocumentEvent; +import javax.swing.event.DocumentListener; +import javax.swing.text.Element; + +import de.uka.ilkd.key.gui.configuration.Config; + +import org.key_project.util.java.StringUtil; + + +/** + * The information window is used to present detailed information about the execution of a solver. + * In particular it presents information about: - the concrete translation that was passed to the + * solver - the translation of the taclets - the messages that were sent between KeY and the + * external solvers. + *

+ * Adaptation of {@link de.uka.ilkd.key.gui.smt.InformationWindow} for Isabelle solvers + */ +public class InformationWindow extends JDialog { + public record Information(String title, String content, String solver) { + } + + private JTabbedPane tabbedPane; + + public InformationWindow(Dialog parent, Collection information, + String title) { + super(parent); + this.setTitle(title); + for (Information el : information) { + getTabbedPane().addTab(el.title, newTab(el)); + } + + setSize(600, 500); + this.getContentPane().add(getTabbedPane()); + this.setModalExclusionType(ModalExclusionType.APPLICATION_EXCLUDE); + this.setDefaultCloseOperation(DISPOSE_ON_CLOSE); + this.setLocationRelativeTo(parent); + this.setVisible(true); + } + + private Component newTab(Information information) { + final JTextArea lines = new JTextArea("1"); + final JTextArea content = new JTextArea(); + content.setFont(UIManager.getFont(Config.KEY_FONT_SEQUENT_VIEW)); + lines.setBackground(Color.LIGHT_GRAY); + lines.setEditable(false); + content.setEditable(false); + + content.getDocument().addDocumentListener(new DocumentListener() { + public String getText() { + int caretPosition = content.getDocument().getLength(); + Element root = content.getDocument().getDefaultRootElement(); + StringBuilder text = new StringBuilder("1" + StringUtil.NEW_LINE); + for (int i = 2; i < root.getElementIndex(caretPosition) + 2; i++) { + text.append(i).append(StringUtil.NEW_LINE); + } + return text.toString(); + } + + @Override + public void changedUpdate(DocumentEvent de) { + lines.setText(getText()); + } + + @Override + public void insertUpdate(DocumentEvent de) { + lines.setText(getText()); + } + + @Override + public void removeUpdate(DocumentEvent de) { + lines.setText(getText()); + } + }); + content.setText(information.content); + content.setCaretPosition(0); + JScrollPane pane = new JScrollPane(); + pane.getViewport().add(content); + pane.setRowHeaderView(lines); + pane.setVerticalScrollBarPolicy(JScrollPane.VERTICAL_SCROLLBAR_ALWAYS); + return pane; + } + + + private JTabbedPane getTabbedPane() { + if (tabbedPane == null) { + tabbedPane = new JTabbedPane(); + } + return tabbedPane; + } +} diff --git a/keyext.isabelletranslation/src/main/java/org/key_project/isabelletranslation/gui/IsabelleProgressDialog.java b/keyext.isabelletranslation/src/main/java/org/key_project/isabelletranslation/gui/IsabelleProgressDialog.java new file mode 100644 index 0000000000..7a189b36d2 --- /dev/null +++ b/keyext.isabelletranslation/src/main/java/org/key_project/isabelletranslation/gui/IsabelleProgressDialog.java @@ -0,0 +1,468 @@ +/* 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.gui; + +import java.awt.*; +import javax.swing.*; +import javax.swing.event.TableModelEvent; +import javax.swing.plaf.basic.BasicProgressBarUI; +import javax.swing.table.TableCellEditor; +import javax.swing.table.TableCellRenderer; +import javax.swing.table.TableColumn; +import javax.swing.table.TableColumnModel; + +import de.uka.ilkd.key.gui.IssueDialog; +import de.uka.ilkd.key.gui.MainWindow; + +import org.key_project.isabelletranslation.gui.IsabelleProgressModel.ProcessColumn.ProcessData; +import org.key_project.util.java.SwingUtil; + +import org.slf4j.Logger; +import org.slf4j.LoggerFactory; + +/** + * Dialog showing launched Isabelle processes and results. + *

+ * Adapted version of {@link de.uka.ilkd.key.gui.smt.ProgressDialog} used for SMT. + */ +public class IsabelleProgressDialog extends JDialog { + private static final Logger LOGGER = LoggerFactory.getLogger(IsabelleProgressDialog.class); + + /** + * Contains the progress of all solvers. + */ + private final ProgressTable table; + /** + * Button to apply the results of running the Isabelle solvers. + * May close some open goals if the solvers found proofs. + */ + private JButton applyButton; + /** + * Button to stop the launched Isabelle solvers. + */ + private JButton stopButton; + /** + * Scroll pane listing the open goals and the results of running each Isabelle solver on them. + */ + private JScrollPane scrollPane; + /** + * Overall progress of the Isabelle solvers (# goals processed / total goals). + */ + private JProgressBar progressBar; + private final IsabelleProgressDialogListener listener; + + /** + * Current state of the dialog. + */ + public enum Modus { + /** + * Isabelle solvers are running and may be stopped by the user. + */ + SOLVERS_RUNNING, + /** + * Isabelle solvers are done (or terminated). Results may be applied by the user. + */ + SOLVERS_DONE + } + + /** + * Current state of the dialog. + */ + private Modus modus = Modus.SOLVERS_RUNNING; + + /** + * Listener interface to interact with this dialog. Used for functionality of stop, apply and + * discard buttons. + */ + public interface IsabelleProgressDialogListener extends ProgressTable.ProgressTableListener { + void applyButtonClicked(); + + void stopButtonClicked(); + + void discardButtonClicked(); + } + + /** + * Creates a new progress dialog. + * + * @param model progress model that is displayed in dialog + * @param listener listener to be used + * @param resolution resolution to be used for progress bars of each solver + * @param progressBarMax the total number of goals + * @param titles titles of the solver types + */ + public IsabelleProgressDialog(IsabelleProgressModel model, + IsabelleProgressDialogListener listener, + boolean counterexample, int resolution, int progressBarMax, + String... titles) { + super(MainWindow.getInstance()); + table = new ProgressTable(resolution, listener); + table.setAutoResizeMode(JTable.AUTO_RESIZE_OFF); + table.getTableHeader().setReorderingAllowed(false); + table.setModel(model, titles); + this.listener = listener; + this.setTitle("Isabelle Interface"); + + getProgressBar().setMaximum(progressBarMax); + + setDefaultCloseOperation(DISPOSE_ON_CLOSE); + setModal(true); + Container contentPane = this.getContentPane(); + contentPane.setLayout(new GridBagLayout()); + Box buttonBox = Box.createHorizontalBox(); + buttonBox.add(Box.createHorizontalGlue()); + buttonBox.add(getStopButton()); + buttonBox.add(Box.createHorizontalStrut(5)); + if (!counterexample) { + buttonBox.add(Box.createHorizontalStrut(5)); + buttonBox.add(getApplyButton()); + buttonBox.add(Box.createHorizontalStrut(5)); + } + + + GridBagConstraints constraints = new GridBagConstraints(0, 0, 1, 1, 1.0, 0.0, + GridBagConstraints.CENTER, GridBagConstraints.BOTH, new Insets(5, 5, 0, 5), 0, 0); + + contentPane.add(getProgressBar(), constraints); + constraints.gridy++; + constraints.weighty = 2.0; + contentPane.add(getScrollPane(), constraints); + constraints.gridy += 2; + constraints.weighty = 0.0; + constraints.insets.bottom = 5; + contentPane.add(buttonBox, constraints); + this.pack(); + // always set the location last, otherwise it is not centered! + setLocationRelativeTo(MainWindow.getInstance()); + } + + /** + * Updates the progress bar in the dialog. + * + * @param value the new value to set the progress bar to + */ + public void setProgress(int value) { + getProgressBar().setValue(value); + } + + /** + * Returns the progress bar or creates a new one, if not already created + * + * @return the progress bar + */ + public JProgressBar getProgressBar() { + if (progressBar == null) { + progressBar = new JProgressBar(); + } + return progressBar; + } + + /** + * Returns the apply button or creates a new one, if not already created + * + * @return the apply button + */ + private JButton getApplyButton() { + if (applyButton == null) { + applyButton = new JButton("Apply"); + applyButton.setToolTipText( + "Apply the results (i.e. close goals if the Isabelle solver was successful)"); + applyButton.setEnabled(false); + applyButton.addActionListener(e -> { + try { + listener.applyButtonClicked(); + } catch (Exception exception) { + // There may be exceptions during rule application that should not be lost. + LOGGER.error("Exception during application of Isabelle results:", exception); + IssueDialog.showExceptionDialog(this, exception); + } + }); + } + return applyButton; + } + + /** + * Returns the scroll pane or creates a new one, if not already created + * + * @return the scroll pane + */ + private JScrollPane getScrollPane() { + if (scrollPane == null) { + scrollPane = SwingUtil.createScrollPane(table); + } + return scrollPane; + } + + /** + * Returns the stop button or creates a new one, if not already created + * + * @return the stop button + */ + private JButton getStopButton() { + if (stopButton == null) { + stopButton = new JButton("Stop"); + stopButton.addActionListener(e -> { + if (modus.equals(Modus.SOLVERS_DONE)) { + listener.discardButtonClicked(); + } + if (modus.equals(Modus.SOLVERS_RUNNING)) { + listener.stopButtonClicked(); + } + }); + } + return stopButton; + } + + /** + * Switches the modus of the dialog and switches/enables the corresponding buttons. + * RUNNING -> stop button to interrupt (apply unavailable) + * DONE -> discard button to discard results (apply available) + * + * @param m new modus of dialog + */ + public void setModus(Modus m) { + modus = m; + switch (modus) { + case SOLVERS_DONE -> { + stopButton.setText("Discard"); + if (applyButton != null) { + applyButton.setEnabled(true); + } + } + case SOLVERS_RUNNING -> { + stopButton.setText("Stop"); + if (applyButton != null) { + applyButton.setEnabled(false); + } + } + } + } +} + + +/** + * The table displaying the progress of solver instances + */ +class ProgressTable extends JTable { + private static final int NUMBER_OF_VISIBLE_ROWS = 8; + + /** + * Basic listener interface for the table to enable info buttons. + * currently not working + */ + public interface ProgressTableListener { + void infoButtonClicked(int column, int row); + } + + /** + * Panel displaying the total progress of all solver instances "x/y instances completed" + */ + public static class ProgressPanel extends JPanel { + private JProgressBar progressBar; + private JButton infoButton; + + private JProgressBar getProgressBar() { + if (progressBar == null) { + progressBar = new JProgressBar(); + int height = getInfoButton().getMaximumSize().height; + progressBar.setMaximumSize(new Dimension(Integer.MAX_VALUE, height)); + progressBar.setString("Test"); + progressBar.setStringPainted(true); + progressBar.setFont(this.getFont()); + } + return progressBar; + } + + private JButton getInfoButton() { + if (infoButton == null) { + infoButton = new JButton("Info"); + infoButton.setFont(this.getFont()); + + Dimension dim = new Dimension(); + infoButton.setMargin(new Insets(0, 0, 0, 0)); + + dim.height = this.getFontMetrics(this.getFont()).getHeight() + 2; + dim.width = dim.height * 3; + + infoButton.setMinimumSize(dim); + infoButton.setPreferredSize(dim); + infoButton.setMaximumSize(dim); + } + return infoButton; + } + + ProgressPanel() { + this.setLayout(new BoxLayout(this, BoxLayout.Y_AXIS)); + this.add(Box.createVerticalStrut(2)); + Box content = Box.createHorizontalBox(); + content.add(Box.createHorizontalStrut(2)); + content.add(getProgressBar()); + content.add(Box.createHorizontalStrut(2)); + content.add(getInfoButton()); + content.add(Box.createHorizontalStrut(2)); + this.add(content); + this.add(Box.createVerticalStrut(2)); + } + + /** + * @param value the new value of the progress bar + */ + public void setValue(int value) { + getProgressBar().setValue(value); + } + + public void setText(String text) { + getProgressBar().setString(text); + getProgressBar().setStringPainted(text != null && !text.isEmpty()); + } + } + + + private final ProgressPanel progressPanelRenderer = new ProgressPanel(); + private ProgressPanel progressPanelEditor; + + + private class ProgressCellEditor extends AbstractCellEditor implements TableCellEditor { + + @Override + public Component getTableCellEditorComponent(JTable table, Object value, boolean isSelected, + int row, int column) { + currentEditorCell.x = column; + currentEditorCell.y = row; + ProcessData data = (ProcessData) value; + prepareProgressPanel(getProgressPanelEditor(), data); + return getProgressPanelEditor(); + } + + + @Override + public Object getCellEditorValue() { + return null; + } + + } + + + private void prepareProgressPanel(ProgressPanel panel, final ProcessData data) { + panel.setValue(data.getProgress()); + panel.setText(data.getText()); + panel.infoButton.setEnabled(data.isEditable()); + panel.progressBar.setBackground(data.getBackgroundColor()); + panel.progressBar.setForeground(data.getForegroundColor()); + panel.progressBar.setUI(new BasicProgressBarUI() { + + + @Override + protected Color getSelectionForeground() { + return data.getSelectedTextColor(); + } + + protected Color getSelectionBackground() { + return data.getTextColor(); + } + }); + + } + + + private final Point currentEditorCell = new Point(); + + + public ProgressTable(int resolution, ProgressTableListener listener) { + TableCellRenderer renderer = (table, value, isSelected, hasFocus, row, column) -> { + ProcessData data = (ProcessData) value; + prepareProgressPanel(progressPanelRenderer, data); + return progressPanelRenderer; + }; + this.setDefaultRenderer(IsabelleProgressModel.ProcessColumn.class, renderer); + TableCellEditor editor = new ProgressCellEditor(); + this.setDefaultEditor(IsabelleProgressModel.ProcessColumn.class, editor); + init(getProgressPanelEditor(), this.getFont(), resolution, listener); + init(progressPanelRenderer, this.getFont(), resolution, listener); + } + + private void init(ProgressPanel panel, Font font, int resolution, + final ProgressTableListener listener) { + panel.setFont(font); + panel.progressBar.setMaximum(resolution); + panel.infoButton.addActionListener( + e -> listener.infoButtonClicked(currentEditorCell.x - 1, currentEditorCell.y)); + } + + + public void setModel(IsabelleProgressModel model, String... titles) { + + assert titles.length == model.getColumnCount(); + super.setModel(model); + for (int i = 0; i < titles.length; i++) { + TableColumn col = getTableHeader().getColumnModel().getColumn(i); + + col.setHeaderValue(titles[i]); + packColumn(this, i, 5); + + } + for (int i = 0; i < model.getRowCount(); i++) { + this.setRowHeight(progressPanelRenderer.getPreferredSize().height + 5); + } + + + } + + @Override + public Dimension getPreferredScrollableViewportSize() { + Dimension dim = new Dimension(super.getPreferredScrollableViewportSize()); + + dim.height = + Math.min(NUMBER_OF_VISIBLE_ROWS * (progressPanelRenderer.getPreferredSize().height + 5), + dim.height); + return dim; + } + + public static void packColumn(JTable table, int vColIndex, int margin) { + + TableColumnModel colModel = table.getColumnModel(); + TableColumn col = colModel.getColumn(vColIndex); + int width; + + + TableCellRenderer renderer = col.getHeaderRenderer(); + if (renderer == null) { + renderer = table.getTableHeader().getDefaultRenderer(); + } + Component comp = + renderer.getTableCellRendererComponent(table, col.getHeaderValue(), false, false, 0, 0); + width = comp.getPreferredSize().width; + + + for (int r = 0; r < table.getRowCount(); r++) { + renderer = table.getCellRenderer(r, vColIndex); + comp = renderer.getTableCellRendererComponent(table, table.getValueAt(r, vColIndex), + false, false, r, vColIndex); + width = Math.max(width, comp.getPreferredSize().width); + } + + width += 10 * margin; + + col.setPreferredWidth(width); + } + + + private ProgressPanel getProgressPanelEditor() { + if (progressPanelEditor == null) { + progressPanelEditor = new ProgressPanel(); + } + return progressPanelEditor; + } + + + @Override + public void tableChanged(TableModelEvent e) { + if (e.getType() == TableModelEvent.UPDATE) { + this.repaint(); + + } + super.tableChanged(e); + } + +} diff --git a/keyext.isabelletranslation/src/main/java/org/key_project/isabelletranslation/gui/IsabelleProgressModel.java b/keyext.isabelletranslation/src/main/java/org/key_project/isabelletranslation/gui/IsabelleProgressModel.java new file mode 100644 index 0000000000..fc08390b07 --- /dev/null +++ b/keyext.isabelletranslation/src/main/java/org/key_project/isabelletranslation/gui/IsabelleProgressModel.java @@ -0,0 +1,241 @@ +/* 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.gui; + +import java.awt.Color; +import java.util.ArrayList; +import javax.swing.table.AbstractTableModel; + +/** + * Encapsulates the table of progress bars that is shown within the progress dialog: For each solver + * and each goal there is a cell. + */ +public class IsabelleProgressModel extends AbstractTableModel { + private static final long serialVersionUID = 1L; + + private interface Column { + Object getObject(int row); + + int getRowCount(); + + boolean isEditable(); + + } + + public static class TitleColumn implements Column { + private final String[] titles; + + public TitleColumn(String... titles) { + super(); + this.titles = titles; + + } + + @Override + public Object getObject(int row) { + return titles[row]; + } + + @Override + public int getRowCount() { + + return titles.length; + } + + @Override + public boolean isEditable() { + + return false; + } + + } + + public static class ProcessColumn implements Column { + + static class ProcessData { + private int progress = 0; + private String text = ""; + private boolean isEditable = false; + private Color textColor = Color.BLACK; + private Color backgroundColor = Color.WHITE; + private Color foregroundColor = Color.BLUE; + private final Color selectedTextColor = Color.WHITE; + + public int getProgress() { + return progress; + } + + public String getText() { + return text; + } + + public boolean isEditable() { + return isEditable; + } + + public Color getBackgroundColor() { + return backgroundColor; + } + + public Color getSelectedTextColor() { + return selectedTextColor; + } + + public Color getTextColor() { + return textColor; + } + + public Color getForegroundColor() { + return foregroundColor; + } + + } + + // private final Object [] processes; + public final ProcessData[] data; + private boolean isEditable = false; + + public ProcessColumn(int size) { + super(); + + this.data = new ProcessData[size]; + + for (int i = 0; i < data.length; i++) { + data[i] = new ProcessData(); + + } + + } + + @Override + public Object getObject(int row) { + + return data[row]; + } + + public void setProgress(int value, int row) { + data[row].progress = value; + } + + public void setText(String value, int row) { + data[row].text = value; + } + + @Override + public int getRowCount() { + + return data.length; + } + + public void setEditable(boolean b) { + isEditable = b; + for (ProcessData datum : data) { + datum.isEditable = b; + } + } + + @Override + public boolean isEditable() { + + return isEditable; + } + + } + + private final ArrayList columns = new ArrayList<>(); + + private int rowCount = -1; + + public IsabelleProgressModel() { + super(); + } + + public void addColumn(Column column) { + if (rowCount != -1 && rowCount != column.getRowCount()) { + throw new IllegalArgumentException("Columns must have the same number of rows."); + } + rowCount = column.getRowCount(); + columns.add(column); + } + + public void setProgress(int value, int column, int row) { + column++; + ProcessColumn col = (ProcessColumn) columns.get(column); + col.setProgress(value, row); + this.fireTableCellUpdated(row, column); + } + + public void setText(String text, int column, int row) { + column++; + ProcessColumn col = (ProcessColumn) columns.get(column); + col.setText(text, row); + this.fireTableCellUpdated(row, column); + } + + public void setTextColor(Color color, int x, int y) { + x++; + ProcessColumn col = (ProcessColumn) columns.get(x); + col.data[y].textColor = color; + + this.fireTableCellUpdated(x, y); + } + + public void setForegroundColor(Color color, int x, int y) { + x++; + ProcessColumn col = (ProcessColumn) columns.get(x); + col.data[y].foregroundColor = color; + + this.fireTableCellUpdated(x, y); + } + + public void setBackgroundColor(Color color, int x, int y) { + x++; + ProcessColumn col = (ProcessColumn) columns.get(x); + col.data[y].backgroundColor = color; + this.fireTableCellUpdated(x, y); + } + + public void setEditable(boolean b) { + for (Column column : columns) { + if (column instanceof ProcessColumn) { + ((ProcessColumn) column).setEditable(b); + } + } + } + + @Override + public int getColumnCount() { + + return columns.size(); + } + + @Override + public int getRowCount() { + + return rowCount; + } + + @Override + public boolean isCellEditable(int rowIndex, int columnIndex) { + + return columns.get(columnIndex).isEditable(); + } + + @Override + public Class getColumnClass(int columnIndex) { + return columns.get(columnIndex).getClass(); + + } + + @Override + public Object getValueAt(int row, int col) { + + return columns.get(col).getObject(row); + } + + public Column getColumn(int col) { + return columns.get(col); + } + +} diff --git a/keyext.isabelletranslation/src/main/java/org/key_project/isabelletranslation/gui/ProofApplyUserAction.java b/keyext.isabelletranslation/src/main/java/org/key_project/isabelletranslation/gui/ProofApplyUserAction.java new file mode 100644 index 0000000000..5db2e43538 --- /dev/null +++ b/keyext.isabelletranslation/src/main/java/org/key_project/isabelletranslation/gui/ProofApplyUserAction.java @@ -0,0 +1,74 @@ +/* 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.gui; + +import java.util.Collection; +import java.util.HashSet; + +import de.uka.ilkd.key.core.KeYMediator; +import de.uka.ilkd.key.gui.actions.useractions.UserAction; +import de.uka.ilkd.key.proof.Goal; +import de.uka.ilkd.key.proof.Node; +import de.uka.ilkd.key.proof.Proof; +import de.uka.ilkd.key.rule.IBuiltInRuleApp; + +import org.key_project.isabelletranslation.automation.IsabelleProblem; +import org.key_project.isabelletranslation.automation.IsabelleRuleApp; +import org.key_project.isabelletranslation.automation.IsabelleSolver; + +public class ProofApplyUserAction extends UserAction { + private final Collection solvers; + + private final Collection goalsClosed = new HashSet<>(); + + private final int numberOfGoalsClosed; + + public ProofApplyUserAction(KeYMediator mediator, Proof proof, + Collection solvers) { + super(mediator, proof); + this.solvers = solvers; + this.numberOfGoalsClosed = + (int) solvers.stream().filter(solver -> solver.getFinalResult().isSuccessful()).count(); + } + + @Override + public String name() { + return String.format("Close: %d goals by Isabelle", numberOfGoalsClosed); + } + + @Override + protected void apply() { + for (IsabelleSolver solver : solvers) { + IsabelleProblem problem = solver.getProblem(); + Goal goal = problem.getGoal(); + + if (goalsClosed.contains(goal) || !solver.getFinalResult().isSuccessful()) { + continue; + } + + goalsClosed.add(goal); + + IBuiltInRuleApp app = IsabelleRuleApp.RULE.createApp(solver.name(), + solver.getFinalResult().getSuccessfulTactic()); + app.tryToInstantiate(goal); + goal.apply(app); + } + } + + @Override + public void undo() { + for (Goal g : goalsClosed) { + Node n = g.node(); + n.setAppliedRuleApp(null); + // re-open the goal + Goal firstGoal = proof.getClosedGoal(n); + proof.reOpenGoal(firstGoal); + } + } + + @Override + public boolean canUndo() { + return goalsClosed.stream().allMatch(g -> proof.find(g.node())); + } +} diff --git a/keyext.isabelletranslation/src/main/java/org/key_project/isabelletranslation/gui/controller/IsabelleLauncherProgressDialogMediator.java b/keyext.isabelletranslation/src/main/java/org/key_project/isabelletranslation/gui/controller/IsabelleLauncherProgressDialogMediator.java new file mode 100644 index 0000000000..fc093ab3e3 --- /dev/null +++ b/keyext.isabelletranslation/src/main/java/org/key_project/isabelletranslation/gui/controller/IsabelleLauncherProgressDialogMediator.java @@ -0,0 +1,495 @@ +/* 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.gui.controller; + +import java.awt.*; +import java.text.DecimalFormat; +import java.time.Duration; +import java.time.Instant; +import java.util.*; +import java.util.Timer; +import javax.swing.*; + +import de.uka.ilkd.key.core.KeYMediator; +import de.uka.ilkd.key.gui.MainWindow; +import de.uka.ilkd.key.gui.colors.ColorSettings; +import de.uka.ilkd.key.proof.Proof; + +import org.key_project.isabelletranslation.automation.IsabelleLauncher; +import org.key_project.isabelletranslation.automation.IsabelleLauncherListener; +import org.key_project.isabelletranslation.automation.IsabelleResult; +import org.key_project.isabelletranslation.automation.IsabelleSolver; +import org.key_project.isabelletranslation.gui.InformationWindow; +import org.key_project.isabelletranslation.gui.IsabelleProgressDialog; +import org.key_project.isabelletranslation.gui.IsabelleProgressModel; +import org.key_project.isabelletranslation.gui.ProofApplyUserAction; + +/** + * Updates the {@link IsabelleProgressDialog} for a given {@link IsabelleLauncher}. + */ +public class IsabelleLauncherProgressDialogMediator implements IsabelleLauncherListener { + /** + * The format used to display the remaining time for solver instances. + */ + private static final DecimalFormat remainingTimeFormat = new DecimalFormat("#.#"); + + /** + * The Resolution used for the progress bars in the Isabelle dialog. + */ + private static final int RESOLUTION = 1000; + + /** + * The red color used to display the exception status for solvers + */ + private final static ColorSettings.ColorProperty RED = + ColorSettings.define("[isabelleDialog]red", "", new Color(180, 43, 43)); + + /** + * The green color used to display the valid status for solvers + */ + private final static ColorSettings.ColorProperty GREEN = + ColorSettings.define("[isabelleDialog]green", "", new Color(43, 180, 43)); + + /** + * Timer used to schedule periodic refreshes of the Isabelle dialog. + */ + private final Timer timer = new Timer(); + + /** + * The proof which the launcher is working on. + * Used to close solved goals. + */ + private final Proof proof; + + /** + * Indicates whether a user initiated stop has occured + */ + private boolean userStopFlag = false; + + /** + * The launcher used in conjunction with the dialog. + */ + private final IsabelleLauncher launcher; + + /** + * The number of finished instances. + */ + private int finishedCounter = 0; + + /** + * The solvers started by the launcher + */ + private Collection solvers; + + /** + * The {@link IsabelleProgressModel} associated with the launcher + */ + private IsabelleProgressModel progressModel; + + /** + * Stores which solvers have processed their problem + */ + private boolean[][] finishedSolvers; + + /** + * The dialog used + */ + private IsabelleProgressDialog progressDialog; + + @Override + public void launcherStopped(IsabelleLauncher launcher, + Collection finishedInstances) { + timer.cancel(); + + setProgressText(finishedInstances.size()); + progressModel.setEditable(true); + refreshDialog(); + progressDialog.setModus(IsabelleProgressDialog.Modus.SOLVERS_DONE); + } + + @Override + public void launcherStarted(IsabelleLauncher launcher, Collection solvers) { + prepareDialog(solvers); + + setProgressText(-1); + timer.schedule(new TimerTask() { + @Override + public void run() { + refreshDialog(); + } + }, 0, 10); + } + + @Override + public void launcherPreparationFinished(IsabelleLauncher launcher, + Collection solvers) { + setProgressText(0); + } + + /** + * The event that occurs after the stop button has been pressed in the dialog. + * Uses {@link IsabelleLauncher#stopAll()} to interrupt the + * launcher. + * Also sets the userStopFlag so solver interrupts can be allocated to the user. + */ + protected void stopEvent() { + userStopFlag = true; + launcher.stopAll(); + } + + /** + * The event that occurs after the apply button has been pressed in the dialog. + * Invokes the {@link IsabelleLauncherProgressDialogMediator#applyResults()} to close solved + * goals. + * Then disposes of the dialog. + */ + protected void applyEvent() { + applyResults(); + progressDialog.dispose(); + } + + /** + * Creates a action, which can close the solved goals. + */ + private void applyResults() { + KeYMediator mediator = MainWindow.getInstance().getMediator(); + // ensure that the goal closing does not lag the UI + mediator.stopInterface(true); + try { + new ProofApplyUserAction(mediator, proof, solvers).actionPerformed(null); + } finally { + mediator.startInterface(true); + // switch to new open goal + mediator.getSelectionModel().defaultSelection(); + } + } + + /** + * Updates the dialog for a stopped solver depending on its result. + * + * @param solver The stopped solver. + */ + private void stopped(IsabelleSolver solver) { + int x = 0; + int y = solver.getSolverIndex(); + + if (!finishedSolvers[x][y]) { + finishedCounter++; + progressDialog.setProgress(finishedCounter); + JProgressBar bar = progressDialog.getProgressBar(); + bar.setValue(finishedCounter); + setProgressText(finishedCounter); + finishedSolvers[x][y] = true; + } + + IsabelleResult result = solver.getFinalResult(); + + switch (result.getType()) { + case INTERRUPTED: + interrupted(x, y); + break; + case SUCCESS: + successfullyStopped(solver, x, y); + break; + case ERROR: + encounteredError(x, y); + break; + case TIMEOUT: + timedOut(x, y); + break; + default: + unknownStopped(x, y); + break; + } + } + + /** + * Updates the dialog for an interrupted solver. + * + * @param x The solver type index + * @param y The solver index as reported by {@link IsabelleSolver#getSolverIndex()} + */ + private void interrupted(int x, int y) { + if (userStopFlag) { + progressModel.setProgress(0, x, y); + progressModel.setText("Interrupted by user.", x, y); + } else { + throw new RuntimeException("Solver was interrupted for unknown reasons!"); + } + } + + /** + * Updates the dialog for solver that stopped successfully. + * + * @param x The solver type index + * @param y The solver index as reported by {@link IsabelleSolver#getSolverIndex()} + */ + private void successfullyStopped(IsabelleSolver solver, int x, int y) { + progressModel.setProgress(0, x, y); + progressModel.setTextColor(GREEN.get(), x, y); + + String timeInfo = solver.getComputationTime().toMillis() / 1000d + "s"; + + progressModel.setText("Valid (" + timeInfo + ")", x, y); + } + + /** + * Updates the dialog for solver that encountered an error. + * + * @param x The solver type index + * @param y The solver index as reported by {@link IsabelleSolver#getSolverIndex()} + */ + private void encounteredError(int x, int y) { + progressModel.setProgress(0, x, y); + progressModel.setTextColor(RED.get(), x, y); + progressModel.setText("Exception!", x, y); + } + + /** + * Updates the dialog for solver that timed out. + * + * @param x The solver type index + * @param y The solver index as reported by {@link IsabelleSolver#getSolverIndex()} + */ + private void timedOut(int x, int y) { + progressModel.setProgress(0, x, y); + progressModel.setText("Timeout.", x, y); + } + + /** + * Updates the dialog for solver that stopped for unknown reasons. + * + * @param x The solver type index + * @param y The solver index as reported by {@link IsabelleSolver#getSolverIndex()} + */ + private void unknownStopped(int x, int y) { + progressModel.setProgress(0, x, y); + progressModel.setTextColor(Color.BLUE, x, y); + progressModel.setText("Unknown.", x, y); + } + + /** + * Sets the progress text based on the number of solver instances that have processed their + * problem. + * A negative value may be used to indicate the Launcher is still preparing. + * + * @param value The number of solvers that have processed their problem. Negative values + * indicate the launcher is still preparing. + */ + private void setProgressText(int value) { + JProgressBar bar = progressDialog.getProgressBar(); + if (value < 0) { + bar.setString("Preparing... (this might take a few seconds)"); + bar.setStringPainted(true); + } else { + bar.setString("Processed " + value + " of " + bar.getMaximum() + " problems."); + bar.setStringPainted(true); + } + } + + /** + * The event that occurs after the discard button was pressed. + * Disposes of the dialog and does nothing else, as the button is only available once the + * launcher has stopped. + */ + protected void discardEvent() { + progressDialog.dispose(); + } + + /** + * Creates a new mediator for the given proof and launcher + * + * @param proof the given proof + * @param launcher the launcher used + */ + public IsabelleLauncherProgressDialogMediator(Proof proof, IsabelleLauncher launcher) { + this.proof = proof; + this.launcher = launcher; + } + + /** + * Prepares the dialog. Opens the dialog. + * Assigns the titles of all solver types to their columns. + * Assigns the titles of all goals to be processed by the launcher. + * + * @param solvers The solvers to be started by the launcher. + */ + private void prepareDialog(Collection solvers) { + this.solvers = solvers; + progressModel = new IsabelleProgressModel(); + + String[] captions = new String[solvers.size()]; + + int i = 0; + for (IsabelleSolver solver : solvers) { + captions[i] = solver.getProblem().getName(); + i++; + } + + progressModel.addColumn(new IsabelleProgressModel.TitleColumn(captions)); + finishedSolvers = new boolean[1][solvers.size()]; + progressModel.addColumn(new IsabelleProgressModel.ProcessColumn(solvers.size())); + + + progressDialog = new IsabelleProgressDialog(progressModel, + new IsabelleProgressDialogListenerImpl(), false, + RESOLUTION, solvers.size(), "", "Isabelle"); + + + SwingUtilities.invokeLater(() -> progressDialog.setVisible(true)); + } + + /** + * Refreshes the progress of all solvers. + */ + private void refreshDialog() { + for (IsabelleSolver solver : solvers) { + refreshProgressOfSolver(solver); + } + } + + /** + * Refreshes the progress of a given solver by calling the requisite method in this class. + * + * @param solver the given solver + */ + private void refreshProgressOfSolver(IsabelleSolver solver) { + IsabelleSolver.SolverState state = solver.getState(); + switch (state) { + case Preparing -> preparing(solver); + case Parsing -> parsing(solver); + case Running -> running(solver); + case Stopped -> stopped(solver); + case Waiting -> waiting(solver); + } + } + + /** + * Updates the dialog for a running solver. + * Updates the progress bar for this solver. + * + * @param solver the running solver + */ + private void running(IsabelleSolver solver) { + long progress = calculateProgress(solver); + progressModel.setProgress((int) progress, 0, solver.getSolverIndex()); + + float remainingTime = calculateRemainingTime(solver); + progressModel.setText(remainingTimeFormat.format(remainingTime) + " sec.", 0, + solver.getSolverIndex()); + } + + /** + * Calculates the amount of progress made as a product of the percentage of the time passed in + * comparison to the timeout duration of the solver and the RESOLUTION of the progress bar. + * + * @param solver The solver whose progress is calculated + * @return The value which reflects the progress made by the solver + */ + private long calculateProgress(IsabelleSolver solver) { + Duration maxDuration = Duration.ofSeconds(solver.getTimeout()); + Instant startTime = solver.getStartTime(); + + return (long) Math.floor(RESOLUTION + * (Duration.between(startTime, Instant.now()).toMillis() + / (double) maxDuration.toMillis())); + } + + /** + * Calculates the time remaining until the timeout of the solver. + * + * @param solver the given solver whose remaining time will be calculated + * @return The remaining time in seconds + */ + private float calculateRemainingTime(IsabelleSolver solver) { + Instant timeoutTime = solver.getStartTime().plusSeconds(solver.getTimeout()); + return Duration.between(Instant.now(), timeoutTime).toMillis() / 1000f; + } + + /** + * Updates the progress bar of a solver which is currently parsing the Isabelle theory for its + * problem. + * + * @param solver the solver whose progress bar will be updated + */ + private void parsing(IsabelleSolver solver) { + progressModel.setText("Parsing...", 0, solver.getSolverIndex()); + } + + /** + * Updates the progress bar of a solver that is waiting to be started. + * + * @param solver the solver whose progress bar will be updated + */ + private void waiting(IsabelleSolver solver) { + } + + private IsabelleSolver getSolver(int column, int row) { + // This needs to be changed, if different kinds of Isabelle solvers are supported + return solvers.stream().filter(s -> (s.getSolverIndex() == row)).findFirst().orElse(null); + } + + /** + * Updates the progress bar of a solver that is currently preparing. + * + * @param solver the solver whose progress bar will be updated + */ + private void preparing(IsabelleSolver solver) { + progressModel.setText("Preparing...", 0, solver.getSolverIndex()); + } + + /** + * Naive implementation of a dialog listener to react to button inputs by the user. + */ + private class IsabelleProgressDialogListenerImpl + implements IsabelleProgressDialog.IsabelleProgressDialogListener { + + + public IsabelleProgressDialogListenerImpl() { + super(); + } + + @Override + public void infoButtonClicked(int column, int row) { + IsabelleSolver solver = getSolver(column, row); + if (solver == null) { + throw new RuntimeException("Something went wrong in Dialog"); + } + showInformation(solver); + } + + @Override + public void stopButtonClicked() { + stopEvent(); + } + + @Override + public void applyButtonClicked() { + applyEvent(); + } + + @Override + public void discardButtonClicked() { + discardEvent(); + } + } + + private void showInformation(IsabelleSolver solver) { + Collection information = new HashSet<>(); + String informationTitle = solver.name() + ": " + solver.getProblem().getName(); + + information.add(new InformationWindow.Information("Translation theory", + solver.getRawSolverInput(), informationTitle)); + if (solver.getFinalResult().isError()) { + information.add(new InformationWindow.Information("Exception", + solver.getFinalResult().getException().getMessage(), informationTitle)); + } else { + information.add(new InformationWindow.Information("Raw Solver Output", + solver.getRawSolverOutput(), informationTitle)); + } + + new InformationWindow(progressDialog, information, + "Information for " + informationTitle); + } +} diff --git a/keyext.isabelletranslation/src/main/java/org/key_project/isabelletranslation/gui/controller/TranslateAllAction.java b/keyext.isabelletranslation/src/main/java/org/key_project/isabelletranslation/gui/controller/TranslateAllAction.java new file mode 100644 index 0000000000..45790ae1a0 --- /dev/null +++ b/keyext.isabelletranslation/src/main/java/org/key_project/isabelletranslation/gui/controller/TranslateAllAction.java @@ -0,0 +1,35 @@ +/* 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.gui.controller; + +import java.awt.event.ActionEvent; +import java.util.*; + +import de.uka.ilkd.key.core.KeYMediator; +import de.uka.ilkd.key.gui.MainWindow; +import de.uka.ilkd.key.gui.actions.MainWindowAction; + +import org.slf4j.Logger; +import org.slf4j.LoggerFactory; + +/** + * Action to translate all open goals. + */ +public class TranslateAllAction extends MainWindowAction { + private static final Logger LOGGER = LoggerFactory.getLogger(TranslateAllAction.class); + + public TranslateAllAction(MainWindow mainWindow) { + super(mainWindow); + setName("Translate all goals to Isabelle"); + } + + @Override + public void actionPerformed(ActionEvent e) { + LOGGER.info("Translating..."); + + KeYMediator mediator = getMediator(); + TranslationAction.solveGoals( + Objects.requireNonNull(mediator.getSelectedProof()).openGoals(), mediator, mainWindow); + } +} diff --git a/keyext.isabelletranslation/src/main/java/org/key_project/isabelletranslation/gui/controller/TranslationAction.java b/keyext.isabelletranslation/src/main/java/org/key_project/isabelletranslation/gui/controller/TranslationAction.java new file mode 100644 index 0000000000..20bab577f9 --- /dev/null +++ b/keyext.isabelletranslation/src/main/java/org/key_project/isabelletranslation/gui/controller/TranslationAction.java @@ -0,0 +1,81 @@ +/* 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.gui.controller; + +import java.awt.event.ActionEvent; +import java.io.IOException; +import java.util.*; +import javax.swing.*; + +import de.uka.ilkd.key.core.KeYMediator; +import de.uka.ilkd.key.gui.MainWindow; +import de.uka.ilkd.key.gui.actions.MainWindowAction; +import de.uka.ilkd.key.proof.Goal; + +import org.key_project.isabelletranslation.IsabelleTranslationSettings; +import org.key_project.isabelletranslation.automation.IsabelleLauncher; +import org.key_project.isabelletranslation.automation.IsabelleProblem; +import org.key_project.isabelletranslation.translation.IllegalFormulaException; +import org.key_project.isabelletranslation.translation.IsabelleTranslator; +import org.key_project.util.collection.ImmutableList; + +import org.slf4j.Logger; +import org.slf4j.LoggerFactory; + +/** + * Action to translate the selected goal. + */ +public class TranslationAction extends MainWindowAction { + + private static final Logger LOGGER = LoggerFactory.getLogger(TranslationAction.class); + + public TranslationAction(MainWindow mainWindow) { + super(mainWindow); + setName("Translate to Isabelle"); + } + + @Override + public void actionPerformed(ActionEvent e) { + LOGGER.info("Translating..."); + + KeYMediator mediator = getMediator(); + solveGoals(ImmutableList.of(getMediator().getSelectedGoal()), mediator, mainWindow); + } + + static void solveGoals(ImmutableList goals, KeYMediator mediator, MainWindow mainWindow) { + IsabelleTranslationSettings settings = IsabelleTranslationSettings.getInstance(); + IsabelleTranslator translator = new IsabelleTranslator(mediator.getServices()); + + List translations = new ArrayList<>(); + Map translationExceptions = new HashMap<>(); + for (Goal goal : Objects.requireNonNull(goals)) { + try { + translations.add(translator.translateProblem(goal)); + } catch (IllegalFormulaException e) { + translationExceptions.put(goal, e); + // Add problem without translation + translations.add(new IsabelleProblem(goal, translationExceptions.get(goal))); + } + } + + Thread thread = new Thread(() -> { + IsabelleLauncher launcher = new IsabelleLauncher(settings); + + IsabelleLauncherProgressDialogMediator progressDialogMediator = + new IsabelleLauncherProgressDialogMediator( + mediator.getSelectedProof(), launcher); + + launcher.addListener(progressDialogMediator); + try { + launcher.launch(translations, settings.getTimeout(), 1); + } catch (IOException e) { + // Thrown when Isabelle was not found or translation files could not be written + progressDialogMediator.discardEvent(); + JOptionPane.showMessageDialog(mainWindow, e.getMessage(), "Launch failed!", + JOptionPane.ERROR_MESSAGE); + } + }, "IsabelleLauncherThread"); + thread.start(); + } +} diff --git a/keyext.isabelletranslation/src/main/java/org/key_project/isabelletranslation/translation/BSumHandler.java b/keyext.isabelletranslation/src/main/java/org/key_project/isabelletranslation/translation/BSumHandler.java new file mode 100644 index 0000000000..1e4a4a109f --- /dev/null +++ b/keyext.isabelletranslation/src/main/java/org/key_project/isabelletranslation/translation/BSumHandler.java @@ -0,0 +1,52 @@ +/* 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.translation; + +import java.io.IOException; +import java.util.HashMap; +import java.util.Map; +import java.util.Properties; + +import de.uka.ilkd.key.java.Services; +import de.uka.ilkd.key.ldt.IntegerLDT; + +import org.key_project.logic.Term; +import org.key_project.logic.op.Operator; + +/** + * This class handles the translation of the bounded sum function. + * + * @author Nils Buchholz + */ +public class BSumHandler implements IsabelleHandler { + /** + * Map of the operators supported by this handler and their respective translation. + */ + private final Map supportedOperators = new HashMap<>(); + + @Override + public void init(IsabelleMasterHandler masterHandler, Services services, + Properties handlerSnippets, String[] handlerOptions) throws IOException { + supportedOperators.clear(); + IntegerLDT integerLDT = services.getTypeConverter().getIntegerLDT(); + + supportedOperators.put(integerLDT.getBsum(), "\\"); + } + + @Override + public boolean canHandle(Operator op) { + return supportedOperators.containsKey(op); + } + + @Override + public StringBuilder handle(IsabelleMasterHandler trans, Term term) { + StringBuilder result = + QuantifierHandler.makeBoundedVarRef(trans, term, supportedOperators.get(term.op())); + result.append("="); + result.append(trans.translate(term.sub(0))).append("..<") + .append(trans.translate(term.sub(1))).append(". "); + result.append(trans.translate(term.sub(2))).append(")"); + return result; + } +} diff --git a/keyext.isabelletranslation/src/main/java/org/key_project/isabelletranslation/translation/BooleanOpHandler.java b/keyext.isabelletranslation/src/main/java/org/key_project/isabelletranslation/translation/BooleanOpHandler.java new file mode 100644 index 0000000000..52447f2a6f --- /dev/null +++ b/keyext.isabelletranslation/src/main/java/org/key_project/isabelletranslation/translation/BooleanOpHandler.java @@ -0,0 +1,68 @@ +/* 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.translation; + +import java.util.HashMap; +import java.util.List; +import java.util.Map; +import java.util.Properties; + +import de.uka.ilkd.key.java.Services; +import de.uka.ilkd.key.ldt.BooleanLDT; +import de.uka.ilkd.key.logic.op.Equality; +import de.uka.ilkd.key.logic.op.Junctor; + +import org.key_project.logic.Term; +import org.key_project.logic.op.Operator; + +/** + * This class handles the translation of boolean operations and Boolean formulae + * + * @author Nils Buchholz + */ +public class BooleanOpHandler implements IsabelleHandler { + /** + * Map of the operators supported by this handler and their respective translation. + */ + private final Map supportedOperators = new HashMap<>(); + + + @Override + public void init(IsabelleMasterHandler masterHandler, Services services, + Properties handlerSnippets, String[] handlerOptions) { + BooleanLDT ldt = services.getTypeConverter().getBooleanLDT(); + Operator logicFalse = ldt.getFalseConst(); + supportedOperators.put(logicFalse, new StringBuilder("False")); + + Operator logicTrue = ldt.getTrueConst(); + supportedOperators.put(logicTrue, new StringBuilder("True")); + masterHandler.addPredefinedSort(ldt.targetSort(), "bool"); + supportedOperators.put(Junctor.AND, new StringBuilder("\\")); + supportedOperators.put(Junctor.OR, new StringBuilder("\\")); + supportedOperators.put(Junctor.IMP, new StringBuilder("-->")); + supportedOperators.put(Junctor.NOT, new StringBuilder("Not")); + supportedOperators.put(Junctor.FALSE, new StringBuilder("False")); + supportedOperators.put(Junctor.TRUE, new StringBuilder("True")); + supportedOperators.put(Equality.EQV, new StringBuilder("\\")); + } + + @Override + public boolean canHandle(Operator op) { + return supportedOperators.containsKey(op); + } + + @Override + public StringBuilder handle(IsabelleMasterHandler trans, Term term) { + List children = trans.translate(term.subs()); + StringBuilder result = new StringBuilder(); + Operator op = term.op(); + result.append("((").append(supportedOperators.get(op)).append(")"); + for (StringBuilder child : children) { + result.append(" ").append(child); + } + result.append(")"); + return result; + } + +} diff --git a/keyext.isabelletranslation/src/main/java/org/key_project/isabelletranslation/translation/DefinedSymbolsHandler.java b/keyext.isabelletranslation/src/main/java/org/key_project/isabelletranslation/translation/DefinedSymbolsHandler.java new file mode 100644 index 0000000000..eeadfc51d5 --- /dev/null +++ b/keyext.isabelletranslation/src/main/java/org/key_project/isabelletranslation/translation/DefinedSymbolsHandler.java @@ -0,0 +1,154 @@ +/* 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.translation; + +import java.io.IOException; +import java.util.HashMap; +import java.util.Map; +import java.util.Objects; +import java.util.Properties; + +import de.uka.ilkd.key.java.Services; +import de.uka.ilkd.key.ldt.HeapLDT; +import de.uka.ilkd.key.ldt.JavaDLTheory; +import de.uka.ilkd.key.ldt.LocSetLDT; +import de.uka.ilkd.key.ldt.SeqLDT; +import de.uka.ilkd.key.logic.Namespace; +import de.uka.ilkd.key.logic.op.JFunction; +import de.uka.ilkd.key.logic.op.SortDependingFunction; + +import org.key_project.logic.Name; +import org.key_project.logic.Term; +import org.key_project.logic.op.Function; +import org.key_project.logic.op.Operator; +import org.key_project.logic.op.SortedOperator; +import org.key_project.logic.sort.Sort; + +import org.jetbrains.annotations.NotNull; + +/** + * This class handles the translation of several functions that are already defined in the preamble. + * This prevents the functions being defined twice. + * This class also adds the necessary preamble part to the master handler, which is loaded from the + * "DefinedSymbolsHandler.preamble.xml" file. + * + * @see IsabelleMasterHandler + * + * @author Nils Buchholz + */ +public class DefinedSymbolsHandler implements IsabelleHandler { + /** + * Map of the operators supported by this handler and their respective translation. + */ + Map supportedOperators = new HashMap<>(); + + @Override + public void init(IsabelleMasterHandler masterHandler, Services services, + Properties handlerSnippets, String[] handlerOptions) throws IOException { + masterHandler.addPreamblesLocales(handlerSnippets); + masterHandler.addPredefinedSort(JavaDLTheory.ANY, "any"); + + HeapLDT heapLDT = services.getTypeConverter().getHeapLDT(); + LocSetLDT locSetLDT = services.getTypeConverter().getLocSetLDT(); + SeqLDT seqLDT = services.getTypeConverter().getSeqLDT(); + + Namespace sorts = services.getNamespaces().sorts(); + masterHandler.addPredefinedSort( + Objects.requireNonNull(sorts.lookup(new Name("java.lang.Object"))), + "java_lang_Object"); + masterHandler.addPredefinedSort(Objects.requireNonNull(sorts.lookup(new Name("Null"))), + "Null"); + masterHandler.addPredefinedSort(heapLDT.targetSort(), "Heap"); + masterHandler.addPredefinedSort(locSetLDT.targetSort(), "LocSet"); + masterHandler.addPredefinedSort(seqLDT.targetSort(), "Seq"); + + + Namespace functionNamespace = services.getNamespaces().functions(); + Map definedFunctions = getDefinedFunctions(); + + Map definedSortDependingFunctions = new HashMap<>(); + definedSortDependingFunctions.put("select", "select"); + definedSortDependingFunctions.put("cast", "cast"); + definedSortDependingFunctions.put("seqGet", "seqGet"); + + for (String name : definedFunctions.keySet()) { + Function function = functionNamespace.lookup(name); + if (function != null) + supportedOperators.put(function, definedFunctions.get(name)); + } + + for (Function function : functionNamespace.elements()) { + if (!(function instanceof SortDependingFunction)) + continue; + String funName = function.name().toString().split("::")[1]; + for (String name : definedSortDependingFunctions.keySet()) { + if (funName.equals(name)) { + supportedOperators.put(function, definedSortDependingFunctions.get(name)); + } + } + } + } + + /** + * Returns the list of predefined functions in the preamble. + * + * @return The list of predefined functions in the preamble. + */ + private static @NotNull Map getDefinedFunctions() { + Map definedFunctions = new HashMap<>(); + definedFunctions.put("null", "null"); + definedFunctions.put("length", "obj_length"); + definedFunctions.put("arr", "arr"); + definedFunctions.put("wellFormed", "wellFormed"); + definedFunctions.put("anon", "anon"); + definedFunctions.put("store", "store"); + definedFunctions.put("create", "create"); + + // Seq functions + definedFunctions.put("seqLen", "seqLen"); + definedFunctions.put("seqIndexOf", "seqIndexOf"); + definedFunctions.put("seqGetOutside", "seqGetOutside"); + definedFunctions.put("seqEmpty", "seqEmpty"); + definedFunctions.put("seqSingleton", "seqSingleton"); + definedFunctions.put("seqConcat", "seqConcat"); + definedFunctions.put("seqSub", "seqSub"); + definedFunctions.put("seqPerm", "seqPerm"); + definedFunctions.put("seqNPerm", "seqNPerm"); + definedFunctions.put("seqSwap", "seqSwap"); + definedFunctions.put("seqRemove", "seqRemove"); + definedFunctions.put("seqReverse", "seqReverse"); + + + // LocSet functions + definedFunctions.put("elementOf", "elementOf"); + definedFunctions.put("subset", "subset"); + definedFunctions.put("disjoint", "disjoint"); + definedFunctions.put("empty", "empty"); + definedFunctions.put("allLocs", "allLocs"); + definedFunctions.put("singleton", "singleton"); + definedFunctions.put("union", "union"); + definedFunctions.put("intersect", "intersect"); + definedFunctions.put("setMinus", "setMinus"); + definedFunctions.put("allFields", "allFields"); + definedFunctions.put("allObjects", "allObjects"); + definedFunctions.put("arrayRange", "arrayRange"); + return definedFunctions; + } + + @Override + public boolean canHandle(Operator op) { + return supportedOperators.containsKey(op); + } + + @Override + public StringBuilder handle(IsabelleMasterHandler trans, Term term) { + if (term.op() instanceof SortDependingFunction) { + return SortDependingFunctionHandler.getSortDependingFunctionRef(trans, term, + (SortDependingFunction) term.op(), + supportedOperators.get(term.op())); + } + return UninterpretedSymbolsHandler.getFunctionRef(trans, term, (SortedOperator) term.op(), + supportedOperators.get(term.op())); + } +} diff --git a/keyext.isabelletranslation/src/main/java/org/key_project/isabelletranslation/translation/FieldHandler.java b/keyext.isabelletranslation/src/main/java/org/key_project/isabelletranslation/translation/FieldHandler.java new file mode 100644 index 0000000000..58b8d56978 --- /dev/null +++ b/keyext.isabelletranslation/src/main/java/org/key_project/isabelletranslation/translation/FieldHandler.java @@ -0,0 +1,72 @@ +/* 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.translation; + +import java.io.IOException; +import java.util.Collection; +import java.util.HashSet; +import java.util.Objects; +import java.util.Properties; +import java.util.regex.Matcher; +import java.util.regex.Pattern; + +import de.uka.ilkd.key.java.Services; +import de.uka.ilkd.key.logic.Namespace; + +import org.key_project.logic.Name; +import org.key_project.logic.Term; +import org.key_project.logic.op.Function; +import org.key_project.logic.op.Operator; +import org.key_project.logic.sort.Sort; + +/** + * This class handles the translation of field values. + * + * @author Nils Buchholz + */ +public class FieldHandler implements IsabelleHandler { + /** + * The predefined fields. + */ + private final Collection predefinedFields = new HashSet<>(); + + /** + * The Field sort. + */ + private Sort fieldSort; + + @Override + public void init(IsabelleMasterHandler masterHandler, Services services, + Properties handlerSnippets, String[] handlerOptions) throws IOException { + fieldSort = services.getNamespaces().sorts().lookup("Field"); + predefinedFields.add("created"); + + Namespace sorts = services.getNamespaces().sorts(); + masterHandler.addPredefinedSort(Objects.requireNonNull(sorts.lookup(new Name("Field"))), + "Field"); + } + + @Override + public boolean canHandle(Operator op) { + return (op instanceof Function && ((Function) op).sort() == fieldSort && op.arity() == 0); + } + + @Override + public StringBuilder handle(IsabelleMasterHandler trans, Term term) { + if (trans.isNewSymbol(term)) { + Operator op = term.op(); + Matcher m = Pattern.compile("<(.*?)>").matcher(op.name().toString()); + String fieldName = op.name().toString().replace("::$", "_").replace(".", "_"); + if (m.find()) { + fieldName = m.group(1); + } + if (predefinedFields.contains(fieldName)) { + return new StringBuilder(fieldName); + } + trans.addSymbolAndDeclaration(term, new StringBuilder(fieldName)); + trans.addField((Function) op); + } + return trans.getKnownSymbol(term); + } +} diff --git a/keyext.isabelletranslation/src/main/java/org/key_project/isabelletranslation/translation/IllegalFormulaException.java b/keyext.isabelletranslation/src/main/java/org/key_project/isabelletranslation/translation/IllegalFormulaException.java new file mode 100644 index 0000000000..cf7a7d142e --- /dev/null +++ b/keyext.isabelletranslation/src/main/java/org/key_project/isabelletranslation/translation/IllegalFormulaException.java @@ -0,0 +1,15 @@ +/* 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.translation; + +public class IllegalFormulaException extends Exception { + /** + * + */ + private static final long serialVersionUID = 1L; + + IllegalFormulaException(String msg) { + super(msg); + } +} diff --git a/keyext.isabelletranslation/src/main/java/org/key_project/isabelletranslation/translation/InfiniteUnionHandler.java b/keyext.isabelletranslation/src/main/java/org/key_project/isabelletranslation/translation/InfiniteUnionHandler.java new file mode 100644 index 0000000000..e1826af419 --- /dev/null +++ b/keyext.isabelletranslation/src/main/java/org/key_project/isabelletranslation/translation/InfiniteUnionHandler.java @@ -0,0 +1,49 @@ +/* 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.translation; + +import java.io.IOException; +import java.util.HashMap; +import java.util.Map; +import java.util.Properties; + +import de.uka.ilkd.key.java.Services; + +import org.key_project.logic.Term; +import org.key_project.logic.op.Operator; + +/** + * This class handles the infiniteUnion function. + * + * @author Nils Buchholz + */ +public class InfiniteUnionHandler implements IsabelleHandler { + /** + * Map of the operators supported by this handler and their respective translation. + */ + private final Map supportedOperators = new HashMap<>(); + + @Override + public void init(IsabelleMasterHandler masterHandler, Services services, + Properties handlerSnippets, String[] handlerOptions) throws IOException { + supportedOperators.put(services.getTypeConverter().getLocSetLDT().getInfiniteUnion(), + "infiniteUnion"); + } + + @Override + public boolean canHandle(Operator op) { + return supportedOperators.containsKey(op); + } + + @Override + public StringBuilder handle(IsabelleMasterHandler trans, Term term) { + Operator op = term.op(); + String arg1 = "{" + + trans.translate(term.sub(0)) + "| " + LogicalVariableHandler.makeVarRef(trans, + term.boundVars().get(0).name().toString(), term.boundVars().get(0).sort()) + + ". True }"; + + return new StringBuilder("(").append(supportedOperators.get(op)).append(arg1).append(")"); + } +} diff --git a/keyext.isabelletranslation/src/main/java/org/key_project/isabelletranslation/translation/InstanceOperatorHandler.java b/keyext.isabelletranslation/src/main/java/org/key_project/isabelletranslation/translation/InstanceOperatorHandler.java new file mode 100644 index 0000000000..80c3462c61 --- /dev/null +++ b/keyext.isabelletranslation/src/main/java/org/key_project/isabelletranslation/translation/InstanceOperatorHandler.java @@ -0,0 +1,70 @@ +/* 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.translation; + +import java.io.IOException; +import java.util.HashMap; +import java.util.Map; +import java.util.Properties; + +import de.uka.ilkd.key.java.Services; +import de.uka.ilkd.key.logic.Namespace; +import de.uka.ilkd.key.logic.op.JFunction; +import de.uka.ilkd.key.logic.op.SortDependingFunction; + +import org.key_project.logic.Term; +import org.key_project.logic.op.Function; +import org.key_project.logic.op.Operator; + +/** + * This class handles translation of the instance and exactInstance function. + * + * @author Nils Buchholz + */ +public class InstanceOperatorHandler implements IsabelleHandler { + /** + * Map of the operators supported by this handler and their respective translation. + */ + private final Map supportedOperators = new HashMap<>(); + + @Override + public void init(IsabelleMasterHandler masterHandler, Services services, + Properties handlerSnippets, String[] handlerOptions) throws IOException { + Namespace functionNamespace = services.getNamespaces().functions(); + Map definedSortDependingFunctions = new HashMap<>(); + + definedSortDependingFunctions.put("instance", "instanceof"); + definedSortDependingFunctions.put("exactInstance", "exactInstance"); + + for (Function function : functionNamespace.elements()) { + if (!(function instanceof SortDependingFunction)) + continue; + String funName = function.name().toString().split("::")[1]; + for (String name : definedSortDependingFunctions.keySet()) { + if (funName.equals(name)) { + supportedOperators.put(function, definedSortDependingFunctions.get(name)); + } + } + } + } + + @Override + public boolean canHandle(Operator op) { + return supportedOperators.containsKey(op); + } + + @Override + public StringBuilder handle(IsabelleMasterHandler trans, Term term) { + SortDependingFunction op = (SortDependingFunction) term.op(); + String functionName = supportedOperators.get(op); + String dependingSortTypeName = trans.translateSortName(op.getSortDependingOn()) + "_type"; + + StringBuilder result = new StringBuilder("("); + result.append("(").append(functionName).append(") "); + result.append(trans.translate(term.sub(0))).append(" "); + result.append(dependingSortTypeName).append(")"); + + return result; + } +} diff --git a/keyext.isabelletranslation/src/main/java/org/key_project/isabelletranslation/translation/IntegerOpHandler.java b/keyext.isabelletranslation/src/main/java/org/key_project/isabelletranslation/translation/IntegerOpHandler.java new file mode 100644 index 0000000000..aedd6a01ed --- /dev/null +++ b/keyext.isabelletranslation/src/main/java/org/key_project/isabelletranslation/translation/IntegerOpHandler.java @@ -0,0 +1,79 @@ +/* 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.translation; + +import java.util.HashMap; +import java.util.List; +import java.util.Map; +import java.util.Properties; + +import de.uka.ilkd.key.java.Services; +import de.uka.ilkd.key.ldt.IntegerLDT; + +import org.key_project.logic.Term; +import org.key_project.logic.op.Operator; + +/** + * This class handles translation of the integer operators. + * + * @author Nils Buchholz + */ +public class IntegerOpHandler implements IsabelleHandler { + private final Map supportedOperators = new HashMap<>(); + + private IntegerLDT integerLDT; + + @Override + public void init(IsabelleMasterHandler masterHandler, Services services, + Properties handlerSnippets, + String[] handlerOptions) { + supportedOperators.clear(); + integerLDT = services.getTypeConverter().getIntegerLDT(); + + supportedOperators.put(integerLDT.getAdd(), "+"); + supportedOperators.put(integerLDT.getMul(), "*"); + supportedOperators.put(integerLDT.getSub(), "-"); + supportedOperators.put(integerLDT.getDiv(), "euclDiv"); + supportedOperators.put(integerLDT.getMod(), "euclMod"); + supportedOperators.put(integerLDT.getNeg(), "-"); + + supportedOperators.put(integerLDT.getJDivision(), "jDiv"); + supportedOperators.put(integerLDT.getJModulo(), "jMod"); + + supportedOperators.put(integerLDT.getLessOrEquals(), "<="); + supportedOperators.put(integerLDT.getLessThan(), "<"); + supportedOperators.put(integerLDT.getGreaterOrEquals(), ">="); + supportedOperators.put(integerLDT.getGreaterThan(), ">"); + + masterHandler.addPreamblesLocales(handlerSnippets); + masterHandler.addPredefinedSort(integerLDT.targetSort(), "int"); + } + + @Override + public boolean canHandle(Operator op) { + return supportedOperators.containsKey(op); + } + + @Override + public StringBuilder handle(IsabelleMasterHandler trans, Term term) { + List children = trans.translate(term.subs()); + Operator op = term.op(); + + // negation has a special pattern in Isabelle and thus can't be translated like the other + // functions + if (op == integerLDT.getNeg()) { + return new StringBuilder("(-").append(children.get(0)).append(")"); + } + + StringBuilder result = new StringBuilder(); + result.append("(("); + result.append(supportedOperators.get(op)); + result.append(")"); + for (StringBuilder child : children) { + result.append(" ").append(child); + } + result.append(")"); + return result; + } +} diff --git a/keyext.isabelletranslation/src/main/java/org/key_project/isabelletranslation/translation/IsabelleHandler.java b/keyext.isabelletranslation/src/main/java/org/key_project/isabelletranslation/translation/IsabelleHandler.java new file mode 100644 index 0000000000..3b5c9eaa08 --- /dev/null +++ b/keyext.isabelletranslation/src/main/java/org/key_project/isabelletranslation/translation/IsabelleHandler.java @@ -0,0 +1,102 @@ +/* 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.translation; + +import java.io.IOException; +import java.util.Properties; + +import de.uka.ilkd.key.java.Services; + +import org.key_project.logic.Term; +import org.key_project.logic.op.Operator; + +/** + * This class is a slightly adjusted version of {@link de.uka.ilkd.key.smt.newsmt2.SMTHandler}. It + * largely has the same functionality. + * + * @author Mattias Ulbrich + * @author Jonas Schiffl + * @author Nils Buchholz + */ +public interface IsabelleHandler { + + /** + * An enumeration of the possible answers of a handler to the {@link #canHandle(Term)} method. + */ + enum Capability { + /** + * This indicates that the handler cannot translate a term + */ + UNABLE, + /** + * This indicates that the handler can translate a term + */ + YES_THIS_INSTANCE, + /** + * This indicates that the handler can translate any term with the same operator + */ + YES_THIS_OPERATOR + } + + /** + * Initialise this handler. + *

+ * This method is only called once after creation and before any other method is called. + *

+ * This method may also allocate additional resources that it needs for translation. + * + * @param masterHandler the MasterHandler coordinating the other handlers (including the one at + * hand) + * @param services the non-null services object which is relevant for this handler + * @param handlerSnippets the snippets loaded for this handler, null if no snippet property file + * is available for this handler + * @param handlerOptions arbitrary options for the handler to take into account + * @throws IOException if resources cannot be read. + */ + void init(IsabelleMasterHandler masterHandler, Services services, Properties handlerSnippets, + String[] handlerOptions) throws IOException; + + /** + * Query if this handler can translate a term. + *

+ * Test if this particular term can be translated. Usually this requires checking whether the + * toplevel operator of the term is in the list of supported operators, but the handler can also + * choose to use other aspects of the term to decide. + * + * @param term a non-null term to translate + * @return {@link Capability#YES_THIS_OPERATOR} if this handler can successfully translate any + * term with the same toplevel operator, {@link Capability#YES_THIS_INSTANCE} if this + * handler can successfully translate this particular term, {@link Capability#UNABLE} if + * this handler cannot deal with the term. + */ + default Capability canHandle(Term term) { + return canHandle(term.op()) ? Capability.YES_THIS_OPERATOR : Capability.UNABLE; + } + + /** + * Query if this handler can translate an operator. + *

+ * Test if this handler can translate any term with the given argument top level operator. + * + * @param op a non-null operator to translate + * @return true if this handler can successfully translate all terms with op as toplevel + * operator + */ + boolean canHandle(Operator op); + + /** + * Translate the given term into a StringBuilder. + *

+ * This method will only be called if {@link #canHandle(Term)} returned true for the same term + * argument. + *

+ * The translation may add to the set of assumptions and declarations using corresponding calls + * to the {@link IsabelleMasterHandler} that it receives. + * + * @param trans the non-null master handler to which it belongs + * @param term the non-null term to translate + * @return a StringBuilder containing the translation + */ + StringBuilder handle(IsabelleMasterHandler trans, Term term); +} diff --git a/keyext.isabelletranslation/src/main/java/org/key_project/isabelletranslation/translation/IsabelleHandlerServices.java b/keyext.isabelletranslation/src/main/java/org/key_project/isabelletranslation/translation/IsabelleHandlerServices.java new file mode 100644 index 0000000000..1052c5f0ab --- /dev/null +++ b/keyext.isabelletranslation/src/main/java/org/key_project/isabelletranslation/translation/IsabelleHandlerServices.java @@ -0,0 +1,221 @@ +/* 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.translation; + +import java.io.BufferedReader; +import java.io.IOException; +import java.io.InputStream; +import java.io.InputStreamReader; +import java.lang.reflect.InvocationTargetException; +import java.net.URL; +import java.nio.charset.StandardCharsets; +import java.util.*; +import java.util.concurrent.ConcurrentHashMap; + +import de.uka.ilkd.key.java.Services; + +import org.jspecify.annotations.NonNull; +import org.slf4j.Logger; +import org.slf4j.LoggerFactory; + +/** + * Adapted version of the {@link de.uka.ilkd.key.smt.newsmt2.SMTHandlerServices} for the Isabelle + * translation. + *

+ * This class provides some infrastructure to the translation process. + *

+ * In particular, it collects the preamble and the snippets for the handlers such that they need not + * be read from disk multiple times. + *

+ * This class is a singleton. + * + * @author Mattias Ulbrich + * @author Alicia Appelhagen (load handlers from handler names array instead of ServiceLoader) + * @author Nils Buchholz (adaptation for Isabelle translation) + */ +public class IsabelleHandlerServices { + + private static final Logger LOGGER = LoggerFactory.getLogger(IsabelleHandlerServices.class); + + /** + * A .txt file containing a default handler list to load via + * {@link #getTemplateHandlers(String[])} if that method's parameter is an empty handlerNames + * array. + */ + private static final String DEFAULT_HANDLERS = "defaultHandlers.txt"; + + /** + * Singleton instance + */ + private static IsabelleHandlerServices theInstance; + + /** + * A map from template handler objects to their smt2 snippets. + */ + private final Map snippetMap = new ConcurrentHashMap<>(); + + /** + * lock for synchronisation + */ + private final Object handlerModificationLock = new Object(); + + /** + * Get the instance of this singleton. + * + * @return non-null instance of this class. Always the same. + */ + public static IsabelleHandlerServices getInstance() { + if (theInstance == null) { + theInstance = new IsabelleHandlerServices(); + } + return theInstance; + } + + /** + * Load the original/template IsabelleHandler instances (from the snippetMap) of all handlers + * specified as arguments. Add fresh handlers to the snippetMap and load the snippets that + * belong to these instances if that has not happened yet for any object of a given handler + * class. + *

+ * Caution: Do not call this method too often since it may add to the static map of + * instances to snippets. + *

+ * It would be a good idea to call this method (at most) once for each solver type with a custom + * array of handler names. + *

+ * An empty handlerNames list leads to the usage of the handlers defined by defaultHandlers.txt. + * + * @param handlerNames a non-null list of non-null strings with class names (s. above) + * @return a fresh collection containing only the original IsabelleHandlers from the + * snippetMap's key + * set that match the given handler names. The collection's order matches that of the + * names as well. + * @throws IOException if loading the snippet Properties for a handler class fails + */ + public Collection getTemplateHandlers(String[] handlerNames) + throws IOException { + // If handlerNames is empty, use default handlerNames list. + if (handlerNames.length == 0) { + InputStream stream = + IsabelleHandlerServices.class.getResourceAsStream(DEFAULT_HANDLERS); + assert stream != null; + BufferedReader reader = + new BufferedReader(new InputStreamReader(stream, StandardCharsets.UTF_8)); + handlerNames = reader.lines().toArray(String[]::new); + } + Collection result = new LinkedList<>(); + for (String name : handlerNames) { + try { + Class handlerClass = (Class) Class.forName(name); + if (findHandler(handlerClass, result)) { + continue; + } + synchronized (handlerModificationLock) { + /* + * Make sure that each handler is added to the template handlers (keyset of + * snippetMap) at most once and that every thread waits for the result. Also, + * every search access on smtProperties should be synchronized in order to avoid + * concurrent modification. + */ + if (!findHandler(handlerClass, result)) { + IsabelleHandler handler = handlerClass.getConstructor().newInstance(); + result.add(handler); + Properties handlerSnippets = loadSnippets(handlerClass); + if (handlerSnippets != null) { + snippetMap.put(handler, handlerSnippets); + } + } + } + } catch (ClassNotFoundException e) { + LOGGER.warn("Could not load IsabelleHandler:{}{}", System.lineSeparator(), + e.getMessage()); + } catch (NoSuchMethodException | InvocationTargetException | InstantiationException + | IllegalAccessException e) { + LOGGER.warn("Could not create IsabelleHandler:{}{}", System.lineSeparator(), + e.getMessage()); + } + } + // TODO make sure that the order of handlers in result is the same as the order + // of their names in the name array + return result; + } + + // Search for a handler of the given class in the snippetMap and if it exists, add it to + // the result collection. + private boolean findHandler(Class clazz, Collection result) { + Optional handler = + snippetMap.keySet().stream().filter(h -> h.getClass().equals(clazz)).findFirst(); + if (handler.isPresent()) { + if (!result.contains(handler.get())) { + result.add(handler.get()); + } + return true; + } + return false; + } + + /** + * Get a copy of freshly created {@link IsabelleHandler}s by cloning the reference handlers. + * They can be used to translate problems to Isabelle. + * + * @param services passed on to the handlers for initialisation + * @param handlerNames the fully classified class names of the IsabelleHandlers to be used If + * this is + * empty or null, all existing handlers will be used. + * @param handlerOptions arbitrary String options for the IsabelleHandlers + * @param mh passed on to the handlers for initialisation + * @return a freshly created list of freshly created handlers + * @throws IOException if the resources cannot be read + */ + + public List getFreshHandlers(Services services, @NonNull String[] handlerNames, + String[] handlerOptions, IsabelleMasterHandler mh) throws IOException { + + List result = new ArrayList<>(); + + // Possibly problematic: snippetMap may be modified by another thread while + // calling snippetMap.get(handler) + // -> concurrent modification? + for (IsabelleHandler handler : getTemplateHandlers(handlerNames)) { + // After getOriginalHandlers(handlerNames), snippets for all handlers are + try { + IsabelleHandler copy = handler.getClass().getConstructor().newInstance(); + /* + * Either use that synchronized block or make snippetMap a ConcurrentHashMap: + * Properties snippet; synchronized (handlerModificationLock) { // Avoid concurrent + * modification of the snippetMap while accessing it. snippet = + * snippetMap.get(handler); } + */ + copy.init(mh, services, snippetMap.get(handler), handlerOptions); + result.add(copy); + } catch (Exception e) { + throw new IOException(e); + } + } + + return result; + } + + /** + * Look up the resource for the snippets of a particular IsabelleHandler class. They must be in + * the + * same package and have the name of the class with ".preamble.xml" attached. + * + * @param aClass class reference for localisation + * @return freshly created property object, null if the resource does not exist + * @throws IOException may be thrown during reading of the resource + */ + private static Properties loadSnippets(Class aClass) throws IOException { + String resourceName = aClass.getSimpleName() + ".preamble.xml"; + URL resource = aClass.getResource(resourceName); + if (resource != null) { + Properties snippets = new Properties(); + try (InputStream is = resource.openStream()) { + snippets.loadFromXML(is); + } + return snippets; + } + return null; + } +} diff --git a/keyext.isabelletranslation/src/main/java/org/key_project/isabelletranslation/translation/IsabelleMasterHandler.java b/keyext.isabelletranslation/src/main/java/org/key_project/isabelletranslation/translation/IsabelleMasterHandler.java new file mode 100644 index 0000000000..0315d70dd3 --- /dev/null +++ b/keyext.isabelletranslation/src/main/java/org/key_project/isabelletranslation/translation/IsabelleMasterHandler.java @@ -0,0 +1,416 @@ +/* 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.translation; + +import java.io.IOException; +import java.util.*; + +import de.uka.ilkd.key.java.Services; +import de.uka.ilkd.key.ldt.JavaDLTheory; +import de.uka.ilkd.key.logic.sort.ArraySort; +import de.uka.ilkd.key.proof.Goal; + +import org.key_project.logic.Term; +import org.key_project.logic.op.Function; +import org.key_project.logic.op.Operator; +import org.key_project.logic.op.SortedOperator; +import org.key_project.logic.sort.Sort; +import org.key_project.util.collection.ImmutableArray; + +import org.jspecify.annotations.NonNull; + +/** + * This class is responsible for translating the sequent of a given goal. + * It collects all declarations and definitions which need to be added to the translation. + *

+ * The sequent is repeatedly given to the respective {@link IsabelleHandler}, which can translate + * its top most operator. + * + * @author Nils Buchholz + */ +public class IsabelleMasterHandler { + + /** + * The services object used to obtain the namespace for standard sorts in KeY + */ + private final Services services; + + /** + * The exceptions thrown by handlers during translation. + */ + private final List exceptions = new ArrayList<>(); + + /** + * The list of handlers to be used for translation. + */ + private final List handlers; + + /** + * The preambles added for each of the handlers. + * Currently only two such preambles exist, separating this preamble into multiple preambles is + * a complex undertaking due to various dependencies within it. + */ + private final List preambles = new ArrayList<>(); + + /** + * A list of the names of locales that need to be added to the translation locale. + * These can be added by the handler + */ + private final List locales = new ArrayList<>(); + + /** + * A map of operators that were not predefined and their respective translations + */ + private final Map notPredefinedFunctions = new HashMap<>(); + + /** + * A map of predefined sorts and their translations + */ + private final Map predefinedSorts = new HashMap<>(); + + /** + * A map of sorts that were not predefined and for which a definition needs to be generated in + * the translation theory and their translations. + */ + private final Map extraSorts = new HashMap<>(); + + /** + * Stores handlers who are able to handle a given operator to avoid searching through the list + * of handlers + */ + private final Map handlerMap = new IdentityHashMap<>(); + + /** + * The declarations that are added to the locale to introduce variables and functions only found + * on the sequent + */ + private final Collection variableDeclarations = new HashSet<>(); + + /** + * A collection of all fields. These require separate storage to add the lemma stating that they + * are separate values. + */ + private final Collection newFields = new HashSet<>(); + + /** + * Create a new handler with the default set of Isabelle handlers. + * + * @param services non-null services + * @param handlerNames fully qualified class names of the handlers to use. If empty, all + * available handlers are used. + * @param handlerOptions arbitrary String options for the handlers to process + * @throws IOException if the handlers cannot be loaded + */ + public IsabelleMasterHandler(Services services, String[] handlerNames, + String[] handlerOptions) throws IOException { + this.services = services; + List handlers = IsabelleHandlerServices.getInstance() + .getFreshHandlers(services, handlerNames, handlerOptions, this); + predefinedSorts.put(JavaDLTheory.ANY, new StringBuilder("any")); + predefinedSorts.put(JavaDLTheory.FORMULA, new StringBuilder("bool")); + this.handlers = handlers; + } + + /** + * Translates the given term using the handlers. + * + * @param problem the problem to be translated + * @return a string builder containing the translation of the sequent (does not contain the full + * Isabelle theory necessary for proof search. for that see + * {@link IsabelleTranslator#translateProblem(Goal)}) + */ + public StringBuilder translate(Term problem) { + try { + IsabelleHandler cached = handlerMap.get(problem.op()); + if (cached != null) { + // There is a handler that promised to handle this operator ... + return cached.handle(this, problem); + } + + for (IsabelleHandler isabelleHandler : handlers) { + IsabelleHandler.Capability response = isabelleHandler.canHandle(problem); + switch (response) { + case YES_THIS_INSTANCE -> { + // handle this but do not cache. + return isabelleHandler.handle(this, problem); + } + case YES_THIS_OPERATOR -> { + // handle it and cache it for future instances of the op. + handlerMap.put(problem.op(), isabelleHandler); + return isabelleHandler.handle(this, problem); + } + } + } + exceptions.add(new IllegalFormulaException( + "Couldn't translate: \"" + problem.op().name() + "\"")); + return handleAsUnknownValue(problem); + } catch (Exception ex) { + exceptions.add(ex); + return handleAsUnknownValue(problem); + } + } + + /** + * Translates multiple terms in the same manner as {@link IsabelleMasterHandler#translate(Term)} + * + * @param terms terms to be translated + * @return a List of StringBuilders containing translations in the same order as the given terms + */ + public List translate(ImmutableArray terms) { + List result = new LinkedList<>(); + for (Term term : terms) { + result.add(translate(term)); + } + return result; + } + + /** + * If no handler can handle a term, it is taken care of here. + * + * @param problem the problematic term + * @return a generic translation as unknown value + */ + private StringBuilder handleAsUnknownValue(Term problem) { + if (notPredefinedFunctions.containsKey(problem.op())) { + return notPredefinedFunctions.get(problem.op()); + } + StringBuilder abbr = new StringBuilder("unknown_" + problem.op().name()); + notPredefinedFunctions.put(problem.op(), abbr); + return abbr; + } + + /** + * Adds a field value to the newFields collection + * + * @param field a field value + */ + protected void addField(@NonNull Function field) { + assert (field.sort() == services.getNamespaces().sorts().lookup("Field") + && field.arity() == 0); + newFields.add(notPredefinedFunctions.get(field)); + } + + /** + * Returns the fields not predefined, but found on the sequent. + * + * @return the list of fields found during translation + */ + protected Collection getNewFields() { + return newFields; + } + + /** + * Adds the necessary line to declare the top-most operator of the given term in the translation + * locale. + * + * @param term the term whose top-most operator is supposed to be introduced + */ + private void addVariableDeclaration(@NonNull Term term) { + StringBuilder decl = new StringBuilder(); + assert notPredefinedFunctions.get(term.op()) != null; + decl.append("fixes "); + decl.append(notPredefinedFunctions.get(term.op())); + decl.append("::\""); + + if (term.op() instanceof SortedOperator) { + SortedOperator op = (SortedOperator) term.op(); + for (Sort argSort : op.argSorts()) { + if (isNewSort(argSort)) { + addGenericSort(argSort); + } + decl.append(translateSortName(argSort)).append("=>"); + } + decl.append((translateSortName(op.sort()))); + decl.append("\""); + } else { + for (Term sub : term.subs()) { + if (isNewSort(sub.sort())) { + addGenericSort(sub.sort()); + } + decl.append(translateSortName(sub.sort())).append("=>"); + } + decl.append((translateSortName(term.sort()))); + decl.append("\""); + } + variableDeclarations.add(decl.toString()); + } + + /** + * Checks whether the given top-most operator of the given term is not predefined + * Used for handlers to check if they need to add a declaration to the translation locale + * + * @param term the term whose top-most operator is + * @return true - the top-most operator is not predefined, false otherwise + */ + boolean isNewSymbol(Term term) { + return !notPredefinedFunctions.containsKey(term.op()); + } + + /** + * Checks if a given sort has not been defined already. + * + * @param s the sort to check for + * @return true - the sort was not defined yet, false otherwise + */ + boolean isNewSort(Sort s) { + return (!predefinedSorts.containsKey(s) && !extraSorts.containsKey(s)); + } + + /** + * Adds a generic sort to the translation. A generic sort in this context means a sort that is + * not part of the core vocabulary of JFOL as introduced in the KeY book. Examples include java + * class sorts + * + * @param sort the sort to be introduced + */ + void addGenericSort(@NonNull Sort sort) { + if (isNewSort(sort)) { + extraSorts.put(sort, + new StringBuilder(sort.name().toString().replace("[]", "arr").replace(".", "_"))); + if (sort instanceof ArraySort) { + addGenericSort(((ArraySort) sort).elementSort()); + } + } + } + + /** + * Adds a preamble to the translation. + * + * @param stringBuilder the preamble in form of a stringbuilder + */ + void addPreamble(StringBuilder stringBuilder) { + preambles.add(stringBuilder); + } + + /** + * Returns the list of preambles for the translation + * + * @return the list of preambles + */ + List getPreambles() { + return preambles; + } + + /** + * Returns the translation of the given sort. + * + * @param sort sort whose translation is returned + * @return String value containing the translation of the given sort + */ + String translateSortName(@NonNull Sort sort) { + if (isNewSort(sort)) { + addGenericSort(sort); + } + if (predefinedSorts.containsKey(sort)) { + return predefinedSorts.get(sort).toString(); + } + return extraSorts.get(sort).toString(); + } + + + /** + * Adds the preambles and locales associated with the handlers + * + * @param handlerSnippets the snippets object containing the preambles/locales and their + * contents + */ + void addPreamblesLocales(Properties handlerSnippets) { + for (Map.Entry entry : handlerSnippets.entrySet()) { + String key = (String) entry.getKey(); + if (key.endsWith(".preamble")) { + addPreamble(new StringBuilder((String) entry.getValue())); + } + if (key.endsWith(".locale")) { + addLocale(new StringBuilder((String) entry.getValue())); + } + } + } + + /** + * Adds a locale name to the translation. This will be included in the translation locale + * + * @param stringBuilder name of the locale + */ + void addLocale(@NonNull StringBuilder stringBuilder) { + locales.add(stringBuilder); + } + + /** + * Returns the list of locales to be added to the translation locale + * + * @return list of locales + */ + List getLocales() { + return locales; + } + + /** + * Adds a sort to the predefined sorts list. Used by handlers that include their own preamble. + * + * @param s the sort that was predefined + * @param name the name used for the sort in translation + */ + void addPredefinedSort(@NonNull Sort s, String name) { + predefinedSorts.put(s, new StringBuilder(name)); + } + + /** + * Returns the sorts that require a generated declaration in the translation theory. + * + * @return Collection of the sorts that need to be declared in theory + */ + Set getExtraSorts() { + return extraSorts.keySet(); + } + + /** + * Adds the top-most operator of the term to the map containing operators and their + * translations. + * Also adds the necessary declaration line to the list of declarations + * + * @param term the term whose top-most operator is being added + * @param s the translation of the top-most operator + */ + void addSymbolAndDeclaration(Term term, StringBuilder s) { + notPredefinedFunctions.put(term.op(), s); + addVariableDeclaration(term); + } + + /** + * Returns the translation of a symbol introduced during translation (!not predefined) + * + * @param term the term whose top-most operator will be translated + * @return translation of the top-most operator + */ + StringBuilder getKnownSymbol(Term term) { + return notPredefinedFunctions.get(term.op()); + } + + /** + * Returns the declarations that need to be added to the translation locale + * + * @return collection of the declaration lines that need to be added to the translation locale + */ + Collection getVariableDeclarations() { + return variableDeclarations; + } + + /** + * Returns the set of predefined sorts + * + * @return set of predefined sorts + */ + Set getPredefinedSorts() { + return predefinedSorts.keySet(); + } + + /** + * Returns the list of exceptions encountered during translation + * + * @return list of exceptions + */ + List getExceptions() { + return exceptions; + } +} diff --git a/keyext.isabelletranslation/src/main/java/org/key_project/isabelletranslation/translation/IsabelleTranslator.java b/keyext.isabelletranslation/src/main/java/org/key_project/isabelletranslation/translation/IsabelleTranslator.java new file mode 100644 index 0000000000..304a5adad7 --- /dev/null +++ b/keyext.isabelletranslation/src/main/java/org/key_project/isabelletranslation/translation/IsabelleTranslator.java @@ -0,0 +1,468 @@ +/* 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.translation; + +import java.io.IOException; +import java.util.*; + +import de.uka.ilkd.key.java.Services; +import de.uka.ilkd.key.ldt.JavaDLTheory; +import de.uka.ilkd.key.logic.Sequent; +import de.uka.ilkd.key.logic.SequentFormula; +import de.uka.ilkd.key.logic.Term; +import de.uka.ilkd.key.logic.sort.ArraySort; +import de.uka.ilkd.key.proof.Goal; + +import org.key_project.isabelletranslation.IsabelleTranslationSettings; +import org.key_project.isabelletranslation.automation.IsabelleProblem; +import org.key_project.logic.sort.Sort; + +/** + * Translator for Isabelle. + */ +public class IsabelleTranslator { + /** + * Line ending to use in translations + */ + private static final String LINE_ENDING = "\n"; + + /** + * Services object used to initiate handlers + */ + private final Services services; + /** + * The null sort + */ + private final Sort nullSort; + + public IsabelleTranslator(Services services) { + this.services = services; + nullSort = services.getNamespaces().sorts().lookup("Null"); + } + + /** + * Translates the given goal. + * + * @param goal goal to translate + * @return IsabelleProblem containing the translation + * @throws IllegalFormulaException if translation fails + */ + public final IsabelleProblem translateProblem(Goal goal) throws IllegalFormulaException { + Sequent sequent = goal.sequent(); + List antecedents = + sequent.antecedent().asList().stream().map(SequentFormula::formula).toList(); + List succedents = + sequent.succedent().asList().stream().map(SequentFormula::formula).toList(); + IsabelleMasterHandler masterHandler; + try { + masterHandler = new IsabelleMasterHandler(services, new String[0], new String[0]); + } catch (IOException e) { + throw new RuntimeException(e); + } + List antecedentTranslations = + antecedents.stream().map(masterHandler::translate).toList(); + List succedentTranslations = + new ArrayList<>(succedents.stream().map(masterHandler::translate).toList()); + + List exceptions = masterHandler.getExceptions(); + if (!exceptions.isEmpty()) { + StringBuilder message = new StringBuilder(); + for (Throwable t : exceptions) { + message.append(t.getMessage()).append(System.lineSeparator()); + } + throw new IllegalFormulaException(message.toString()); + } + + + // Construction of translation preamble + StringBuilder translationPreamble = new StringBuilder(); + translationPreamble.append( + "theory TranslationPreamble imports Main \"HOL-Combinatorics.List_Permutation\" begin") + .append(LINE_ENDING); + + for (StringBuilder preamble : masterHandler.getPreambles()) { + translationPreamble.append(LINE_ENDING).append(preamble).append(LINE_ENDING); + } + translationPreamble.append("end"); + + + // Construct translation theory + StringBuilder translationTheory = + new StringBuilder(IsabelleTranslationSettings.getInstance().getHeader()) + .append(LINE_ENDING); + + // Find the sorts present on sequent to add definitions for sorts not in preamble + Map> sortParentsMap = + getSortsParents(masterHandler.getExtraSorts(), masterHandler.getPredefinedSorts()); + Map sortImplemented = new HashMap<>(); + sortParentsMap.keySet().forEach((Sort sort) -> sortImplemented.put(sort, false)); + masterHandler.getPredefinedSorts().forEach((Sort sort) -> sortImplemented.put(sort, true)); + + Queue sortImplementationQueue = new LinkedList<>(sortParentsMap.keySet()); + addSortsDefinitions(translationTheory, sortImplementationQueue, sortImplemented, + sortParentsMap, masterHandler); + + + + // Construct proof locale + translationTheory.append("locale varsAndFunctions"); + List locales = masterHandler.getLocales(); + + // used for formatting + boolean locale_empty = true; + + // add any supplementary locales like integer operation locale + if (!locales.isEmpty()) { + translationTheory.append(" = "); + translationTheory.append(locales.remove(0)); + locale_empty = false; + } + for (StringBuilder locale : locales) { + translationTheory.append(" + ").append(locale); + } + + // Add declarations for variables present on sequent that are not in preamble + Collection variableDeclarations = masterHandler.getVariableDeclarations(); + if (!variableDeclarations.isEmpty() && locale_empty) { + translationTheory.append(" = "); + translationTheory.append(locales.remove(0)); + locale_empty = false; + } else if (!variableDeclarations.isEmpty()) { + translationTheory.append(" + ").append(LINE_ENDING); + } + for (String variableDecl : variableDeclarations) { + translationTheory.append(LINE_ENDING).append(variableDecl); + } + translationTheory.append(LINE_ENDING); + + // Add assumption, that all field values are distinct. This is based on the KeY book + if (!masterHandler.getNewFields().isEmpty()) { + translationTheory.append("assumes distinct_fields:"); + translationTheory.append(getDistinctFieldLemma(masterHandler.getNewFields())); + translationTheory.append(LINE_ENDING); + } + + // This did not seem helpful from my testing, would add the assumption, that all sorts are + // disjunct + // sequentTranslation.append(getDistinctExtraSortsAssumptions(masterHandler)); + + translationTheory.append("begin").append(LINE_ENDING); + + + // Add proof theorem + translationTheory.append("theorem solve: "); + for (int i = 0; i < antecedentTranslations.size(); i++) { + StringBuilder antecedentFormula = antecedentTranslations.get(i); + translationTheory.append(LINE_ENDING).append("assumes antecedent_").append(i) + .append(":\"").append(antecedentFormula).append("\""); + } + translationTheory.append(LINE_ENDING); + translationTheory.append("shows \""); + if (succedentTranslations.isEmpty()) { + translationTheory.append("False"); + } else { + translationTheory.append(succedentTranslations.get(0)); + } + for (int i = 1; i < succedentTranslations.size(); i++) { + StringBuilder succedentFormula = succedentTranslations.get(i); + translationTheory.append(LINE_ENDING).append("\\").append(succedentFormula); + } + translationTheory.append("\""); + + return new IsabelleProblem(goal, translationPreamble.toString(), + translationTheory.toString()); + } + + /** + * Creates an assumption, that all sorts are disjunct (mod null). + * + * @param masterHandler masterHandler that handled translation + * @return assumption, that sorts are disjunct + */ + private StringBuilder getDistinctExtraSortsAssumptions(IsabelleMasterHandler masterHandler) { + Set sorts = masterHandler.getExtraSorts(); + Queue sortsCheckQueue = new LinkedList<>(sorts); + StringBuilder sortsAssumptions = new StringBuilder(); + + while (!sortsCheckQueue.isEmpty()) { + Sort s = sortsCheckQueue.remove(); + if (s == JavaDLTheory.ANY || s == JavaDLTheory.FORMULA) { + continue; + } + String sType = masterHandler.translateSortName(s) + "_type"; + String sVal = "(" + masterHandler.translateSortName(s) + "\\<^sub>v\\<^sub>a\\<^sub>l::" + + masterHandler.translateSortName(s) + ")"; + for (Sort s2 : sortsCheckQueue) { + if (s2 == JavaDLTheory.ANY || s2 == JavaDLTheory.FORMULA) { + continue; + } + if (!s.extendsTrans(s2) && !s2.extendsTrans(s)) { + String s2Type = masterHandler.translateSortName(s2) + "_type"; + String s2Val = + "(" + masterHandler.translateSortName(s2) + "\\<^sub>v\\<^sub>a\\<^sub>l::" + + masterHandler.translateSortName(s2) + ")"; + if (nullSort.extendsTrans(s) && nullSort.extendsTrans(s2)) { + sortsAssumptions.append("assumes disjointModNull_") + .append(masterHandler.translateSortName(s)).append("_") + .append(masterHandler.translateSortName(s2)) + .append(":\"").append(sVal).append(" = ").append(s2Val) + .append("\\ s=null\"").append(LINE_ENDING); + } else { + // Sorts are unrelated. need to add distinctness assumption + sortsAssumptions.append("assumes \"disjointTypes ").append(sType) + .append(" ").append(s2Type).append("\"").append(LINE_ENDING); + } + } + } + } + return sortsAssumptions; + } + + /** + * Lemma to show fields are distinct + * + * @param newFields the list of translations of field variables + * @return a lemma stating the distinctness of all field variables + */ + private StringBuilder getDistinctFieldLemma(Collection newFields) { + if (newFields.isEmpty()) + return new StringBuilder(); + String commaSeparatedFields = String.join(",", newFields); + StringBuilder distinctFieldLemma = new StringBuilder(); + distinctFieldLemma.append("\"(distinct ["); + distinctFieldLemma.append(commaSeparatedFields); + distinctFieldLemma.append(", created]) \\ (({"); + distinctFieldLemma.append(commaSeparatedFields); + distinctFieldLemma.append(", created} \\ image arr (UNIV::int set)) = {})\""); + return distinctFieldLemma; + } + + /** + * Adds the definitions for the given sorts to the given translation theory. + * Works recursively using the queue of sorts to be implemented + * + * @param translationTheory {@link StringBuilder} containing the translation theory up to this + * point + * @param sortImplementationQueue queue for the implementation of sorts + * @param sortImplemented Map to check whether a sort has been implemented + * @param sortParentsMap Map, mapping a sort to the set of its parents + * @param masterHandler the masterHandler used during translation + */ + private void addSortsDefinitions(StringBuilder translationTheory, + Queue sortImplementationQueue, Map sortImplemented, + Map> sortParentsMap, IsabelleMasterHandler masterHandler) { + if (sortImplementationQueue.isEmpty()) { + return; + } + + // Ensure that a sort is not implemented before its parents + // Instead push it to the end of the queue + Sort sort = sortImplementationQueue.poll(); + for (Sort parent : sortParentsMap.get(sort)) { + if (!sortImplemented.get(parent)) { + sortImplementationQueue.add(sort); + addSortsDefinitions(translationTheory, sortImplementationQueue, sortImplemented, + sortParentsMap, masterHandler); + return; + } + } + + // Ensure an array sort is not implemented before its elementsort + if ((sort instanceof ArraySort) && !sortImplemented.get(((ArraySort) sort).elementSort())) { + sortImplementationQueue.add(sort); + addSortsDefinitions(translationTheory, sortImplementationQueue, sortImplemented, + sortParentsMap, masterHandler); + return; + } + + + // Add generated declaration + String sortName = masterHandler.translateSortName(sort); + String UNIV = sortName + "_UNIV"; + + translationTheory.append("(* generated declaration for sort: ") + .append(sort.name()).append(" *)").append(LINE_ENDING); + // Lemma showing there is at least one element in this sort + translationTheory.append("lemma ex_").append(UNIV).append(":"); + translationTheory.append(getUnivSpec(masterHandler, sortParentsMap.get(sort), "{bottom}")) + .append(LINE_ENDING); + translationTheory.append(" by simp").append(LINE_ENDING).append(LINE_ENDING); + + // Introduce the universe of this sort + translationTheory.append("consts").append(LINE_ENDING).append(UNIV).append("::\"any set\"") + .append(LINE_ENDING); + translationTheory.append(LINE_ENDING); + + // Use specification to specify the properties of the universe of this sort (subset of + // parents) + translationTheory.append("specification (").append(UNIV).append(") "); + translationTheory.append(getUnivSpec(masterHandler, sortParentsMap.get(sort), UNIV)) + .append(LINE_ENDING); + translationTheory.append(" using ex_").append(UNIV).append(" by blast") + .append(LINE_ENDING); + translationTheory.append(LINE_ENDING); + + + // Reformulate specification as lemma for easier use by Isabelle + String UNIV_spec_lemma_name = UNIV + "_specification"; + translationTheory.append("lemma ").append(UNIV_spec_lemma_name).append(":") + .append(getUnivSpec(masterHandler, sortParentsMap.get(sort), UNIV)) + .append(LINE_ENDING); + translationTheory.append(" by (metis (mono_tags, lifting) ").append(UNIV) + .append("_def someI_ex ex_").append(UNIV).append(")").append(LINE_ENDING); + translationTheory.append(LINE_ENDING); + + // Defines this sort as a new type in Isabelle based on the established universe + translationTheory.append("typedef ").append(sortName).append(" = \"").append(UNIV) + .append("\"").append(LINE_ENDING); + String repName = sortName + "2any"; + String absName = "any2" + sortName; + + // Add morphisms that map between the sort and the any sort + translationTheory.append(" morphisms ").append(repName).append(" ").append(absName) + .append(LINE_ENDING); + translationTheory.append(" using ").append(UNIV_spec_lemma_name).append(" by auto") + .append(LINE_ENDING).append(LINE_ENDING); + + // Add coercions for Isabelle to use coercive subtyping + translationTheory.append("declare [[coercion ").append(repName).append("]]") + .append(LINE_ENDING).append(LINE_ENDING); + + // Repeat properties of type for UNIV constants of Isabelle + // Improves performance and shortens proofs. Used in schema + String IsabelleTypeUniverseOfSort = "(UNIV::" + sortName + " set)"; + translationTheory.append("lemma ").append(sortName).append("_type_specification[simp]:") + .append(getUnivSpec(masterHandler, sortParentsMap.get(sort), + IsabelleTypeUniverseOfSort)) + .append(LINE_ENDING); + translationTheory.append(" using ").append(UNIV_spec_lemma_name) + .append(" using type_definition.Rep_range type_definition_").append(sortName) + .append(" by blast").append(LINE_ENDING); + translationTheory.append(LINE_ENDING).append(LINE_ENDING); + + // extra coercions for all other parent types + // may lead to extra performance if left out, because Isabelle will only need to deal with + // comparisons in any + for (Sort parentSort : sortParentsMap.get(sort)) { + if (parentSort == JavaDLTheory.ANY) { + continue; + } + String parentSortName = masterHandler.translateSortName(parentSort); + String parentSortInj = sortName + "2" + parentSortName; + translationTheory.append(LINE_ENDING).append("fun ").append(parentSortInj) + .append(" where \"").append(parentSortInj) + .append(" x = ").append("any2").append(parentSortName).append(" (") + .append(repName).append(" x)\"").append(LINE_ENDING); + translationTheory.append("declare [[coercion ").append(parentSortInj).append("]]") + .append(LINE_ENDING).append(LINE_ENDING); + } + + // Instantiation of any typeclass for this sort + // the typeclass provides polymorphisms for the cast functions + translationTheory.append("instantiation ").append(sortName).append("::any") + .append(LINE_ENDING); + translationTheory.append("begin").append(LINE_ENDING); + String to_any_fun_Name = "to_any_" + sortName; + translationTheory.append("fun ").append(to_any_fun_Name) + .append(" where \"").append(to_any_fun_Name).append(" x = ").append(repName) + .append(" x\"") + .append(LINE_ENDING); + String cast_fun_Name = "cast_" + sortName; + translationTheory.append("fun ").append(cast_fun_Name) + .append(" where \"").append(cast_fun_Name).append(" x = ").append(absName) + .append(" x\"") + .append(LINE_ENDING); + translationTheory.append("instance by standard").append(LINE_ENDING); + translationTheory.append("end").append(LINE_ENDING).append(LINE_ENDING); + + // coercion of null sort to this sort + if (nullSort.extendsTrans(sort)) { + String null_to_sort_name = "Null2" + sortName; + translationTheory.append("fun ").append(null_to_sort_name).append(" where \"") + .append(null_to_sort_name) + .append(" x = ").append(absName).append("(Null2any x)\"").append(LINE_ENDING); + translationTheory.append("declare [[coercion Null2").append(sortName).append("]]") + .append(LINE_ENDING).append(LINE_ENDING); + } + + // Instantiation of array typeclass, which provides polymorphism for element type + if (sort instanceof ArraySort) { + translationTheory.append("instantiation ").append(sortName).append("::array") + .append(LINE_ENDING); + translationTheory.append("begin").append(LINE_ENDING); + + String element_type_name = "element_type_" + sortName; + String elementSortName = + masterHandler.translateSortName(((ArraySort) sort).elementSort()); + String elementSortType = + "Abs_javaDL_type ((UNIV::" + elementSortName + " set)::any set)"; + translationTheory.append("fun ").append(element_type_name) + .append(" where \"").append(element_type_name) + .append(" (x::").append(sortName).append(")").append(" = ") + .append(elementSortType).append("\"") + .append(LINE_ENDING); + + translationTheory.append("instance by standard").append(LINE_ENDING); + translationTheory.append("end").append(LINE_ENDING).append(LINE_ENDING); + } + + // Constant representing the sort as a Abs_javaDL_type value + String typeConstName = sortName + "_type"; + translationTheory.append("definition \"").append(typeConstName) + .append(" = Abs_javaDL_type ").append(IsabelleTypeUniverseOfSort).append("\""); + + translationTheory.append(LINE_ENDING).append(LINE_ENDING); + + sortImplemented.put(sort, true); + addSortsDefinitions(translationTheory, sortImplementationQueue, sortImplemented, + sortParentsMap, masterHandler); + } + + /** + * Creates the statement about the properties of the universe of a sort. Subset of the universes + * of its parents + * + * @param masterHandler masterhandler used during translation + * @param parents parent sorts of the sort + * @param insert name of the universe constant + * @return the statement about the properties of the universe of a sort + */ + private static String getUnivSpec(IsabelleMasterHandler masterHandler, Set parents, + String insert) { + List parentSortNames = + new ArrayList<>(parents.stream().map(masterHandler::translateSortName).toList()); + StringBuilder univSpec = new StringBuilder(); + if (parentSortNames.isEmpty()) { + parentSortNames.add("any"); + } + univSpec.append("\"").append(insert).append(" \\ (UNIV::") + .append(parentSortNames.get(0)).append(" set)"); + for (int i = 1; i < parentSortNames.size(); i++) { + univSpec.append(" \\ ").append(insert).append(" \\ (UNIV::") + .append(parentSortNames.get(i)).append(" set)"); + } + univSpec.append(" \\ bottom \\ ").append(insert).append("\""); + return univSpec.toString(); + } + + private static Map> getSortsParents(Set sorts, Set outsideParents) { + // may want to avoid some of the looping over sorts by presorting? + HashMap> result = new HashMap<>(); + for (Sort sort : sorts) { + Set parents = new HashSet<>(); + for (Sort sort2 : sorts) { + if (!sort.equals(sort2) && sort.extendsTrans(sort2)) { + parents.add(sort2); + } + } + for (Sort sort2 : outsideParents) { + if (!sort.equals(sort2) && sort.extendsTrans(sort2)) { + parents.add(sort2); + } + } + result.put(sort, parents); + } + return result; + } +} diff --git a/keyext.isabelletranslation/src/main/java/org/key_project/isabelletranslation/translation/LogicalVariableHandler.java b/keyext.isabelletranslation/src/main/java/org/key_project/isabelletranslation/translation/LogicalVariableHandler.java new file mode 100644 index 0000000000..4ae94f2a30 --- /dev/null +++ b/keyext.isabelletranslation/src/main/java/org/key_project/isabelletranslation/translation/LogicalVariableHandler.java @@ -0,0 +1,56 @@ +/* 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.translation; + +import java.util.Properties; + +import de.uka.ilkd.key.java.Services; +import de.uka.ilkd.key.logic.op.LogicVariable; + +import org.key_project.logic.Term; +import org.key_project.logic.op.Operator; +import org.key_project.logic.sort.Sort; + +/** + * Handles the translation of LogicVariables. + */ +public class LogicalVariableHandler implements IsabelleHandler { + + static final String VAR_POSTFIX = UninterpretedSymbolsHandler.POSTFIX; + + @Override + public void init(IsabelleMasterHandler masterHandler, Services services, + Properties handlerSnippets, String[] handlerOptions) { + + } + + @Override + public boolean canHandle(Operator op) { + return op instanceof LogicVariable; + } + + @Override + public StringBuilder handle(IsabelleMasterHandler trans, Term term) { + Sort sort = term.sort(); + if (trans.isNewSort(sort)) { + trans.addGenericSort(sort); + } + return makeVarRef(trans, term.toString(), sort); + } + + /** + * Used to reference a given variable in the translation. + * + * @param trans The master handler used for translation + * @param name intended name of the variable + * @param sort sort of the variable + * @return reference of the given variable in the translation + */ + public static StringBuilder makeVarRef(IsabelleMasterHandler trans, String name, Sort sort) { + StringBuilder result = new StringBuilder("("); + result.append(name).append(VAR_POSTFIX).append("::").append(trans.translateSortName(sort)) + .append(")"); + return result; + } +} diff --git a/keyext.isabelletranslation/src/main/java/org/key_project/isabelletranslation/translation/NumberConstantsHandler.java b/keyext.isabelletranslation/src/main/java/org/key_project/isabelletranslation/translation/NumberConstantsHandler.java new file mode 100644 index 0000000000..846453b9af --- /dev/null +++ b/keyext.isabelletranslation/src/main/java/org/key_project/isabelletranslation/translation/NumberConstantsHandler.java @@ -0,0 +1,47 @@ +/* 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.translation; + +import java.util.Properties; + +import de.uka.ilkd.key.java.Services; +import de.uka.ilkd.key.logic.op.AbstractTermTransformer; + +import org.key_project.logic.Term; +import org.key_project.logic.op.Function; +import org.key_project.logic.op.Operator; + +/** + * This handler is responsible to render number constants Z(3(2(1(#)))) as "123". + */ +public class NumberConstantsHandler implements IsabelleHandler { + + private Function numberSymbol; + private Services services; + + @Override + public void init(IsabelleMasterHandler masterHandler, Services services, + Properties handlerSnippets, + String[] handlerOptions) { + this.services = services; + numberSymbol = services.getTypeConverter().getIntegerLDT().getNumberSymbol(); + } + + @Override + public boolean canHandle(Operator op) { + return op == numberSymbol; + } + + @Override + public StringBuilder handle(IsabelleMasterHandler trans, Term term) { + // TODO This needs an updated AbstractTermTransformer to comply with the new ncore package + // of KeY + assert (term instanceof de.uka.ilkd.key.logic.Term); + + String string = AbstractTermTransformer + .convertToDecimalString((de.uka.ilkd.key.logic.Term) term, services); + return new StringBuilder("(").append(string).append("::int)"); + } + +} diff --git a/keyext.isabelletranslation/src/main/java/org/key_project/isabelletranslation/translation/ObserverFunctionHandler.java b/keyext.isabelletranslation/src/main/java/org/key_project/isabelletranslation/translation/ObserverFunctionHandler.java new file mode 100644 index 0000000000..f9952fd1fe --- /dev/null +++ b/keyext.isabelletranslation/src/main/java/org/key_project/isabelletranslation/translation/ObserverFunctionHandler.java @@ -0,0 +1,52 @@ +/* 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.translation; + +import java.io.IOException; +import java.util.Properties; +import java.util.regex.Matcher; +import java.util.regex.Pattern; + +import de.uka.ilkd.key.java.Services; +import de.uka.ilkd.key.logic.op.ObserverFunction; + +import org.key_project.logic.Term; +import org.key_project.logic.op.Operator; +import org.key_project.logic.op.SortedOperator; + +/** + * Handles translation of Observer functions. + */ +public class ObserverFunctionHandler implements IsabelleHandler { + @Override + public void init(IsabelleMasterHandler masterHandler, Services services, + Properties handlerSnippets, String[] handlerOptions) throws IOException { + + } + + @Override + public boolean canHandle(Operator op) { + return (op instanceof ObserverFunction); + } + + @Override + public StringBuilder handle(IsabelleMasterHandler trans, Term term) { + if (trans.isNewSymbol(term)) { + Operator op = term.op(); + Matcher m = Pattern.compile("<(.*?)>").matcher(op.name().toString()); + String functionName; + if (m.find()) { + functionName = + op.name().toString().replace("<" + m.group(1) + ">", "_" + m.group(1)) + .replace("::", "_").replace("$", "").replace(".", "_"); + } else { + functionName = + op.name().toString().replace("::", "_").replace("$", "").replace(".", "_"); + } + trans.addSymbolAndDeclaration(term, new StringBuilder(functionName)); + } + return UninterpretedSymbolsHandler.getFunctionRef(trans, term, (SortedOperator) term.op(), + trans.getKnownSymbol(term).toString()); + } +} diff --git a/keyext.isabelletranslation/src/main/java/org/key_project/isabelletranslation/translation/PolymorphicHandler.java b/keyext.isabelletranslation/src/main/java/org/key_project/isabelletranslation/translation/PolymorphicHandler.java new file mode 100644 index 0000000000..d53e8c030f --- /dev/null +++ b/keyext.isabelletranslation/src/main/java/org/key_project/isabelletranslation/translation/PolymorphicHandler.java @@ -0,0 +1,55 @@ +/* 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.translation; + +import java.util.List; +import java.util.Properties; + +import de.uka.ilkd.key.java.Services; +import de.uka.ilkd.key.logic.op.Equality; +import de.uka.ilkd.key.logic.op.IfThenElse; + +import org.key_project.logic.Term; +import org.key_project.logic.op.Operator; + +/** + * This handles translation of equals and if-then-else + */ +public class PolymorphicHandler implements IsabelleHandler { + + @Override + public void init(IsabelleMasterHandler masterHandler, Services services, + Properties handlerSnippets, + String[] handlerOptions) { + } + + @Override + public boolean canHandle(Operator op) { + return op == Equality.EQUALS || op == IfThenElse.IF_THEN_ELSE; + } + + @Override + public StringBuilder handle(IsabelleMasterHandler trans, Term term) { + Operator op = term.op(); + StringBuilder result; + if (op == Equality.EQUALS) { + List children = trans.translate(term.subs()); + result = new StringBuilder("("); + result.append(children.get(0)).append("=").append(children.get(1)).append(")"); + return result; + } + + if (op == IfThenElse.IF_THEN_ELSE) { + List children = trans.translate(term.subs()); + result = new StringBuilder("(if ("); + result.append(children.get(0)).append(") then "); + result.append(children.get(1)).append(" else "); + result.append(children.get(2)).append(")"); + return result; + } + + throw new Error("unreachable"); + } + +} diff --git a/keyext.isabelletranslation/src/main/java/org/key_project/isabelletranslation/translation/QuantifierHandler.java b/keyext.isabelletranslation/src/main/java/org/key_project/isabelletranslation/translation/QuantifierHandler.java new file mode 100644 index 0000000000..0879e50177 --- /dev/null +++ b/keyext.isabelletranslation/src/main/java/org/key_project/isabelletranslation/translation/QuantifierHandler.java @@ -0,0 +1,68 @@ +/* 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.translation; + +import java.io.IOException; +import java.util.HashMap; +import java.util.Map; +import java.util.Properties; + +import de.uka.ilkd.key.java.Services; +import de.uka.ilkd.key.logic.op.Quantifier; + +import org.key_project.logic.Term; +import org.key_project.logic.op.Operator; +import org.key_project.logic.op.QuantifiableVariable; +import org.key_project.logic.sort.Sort; + +/** + * This handles translation of quantifiers. + */ +public class QuantifierHandler implements IsabelleHandler { + private final Map supportedOperators = new HashMap<>(); + + @Override + public void init(IsabelleMasterHandler masterHandler, Services services, + Properties handlerSnippets, String[] handlerOptions) throws IOException { + supportedOperators.put(Quantifier.ALL, "\\"); + supportedOperators.put(Quantifier.EX, "\\"); + } + + @Override + public boolean canHandle(Operator op) { + return supportedOperators.containsKey(op); + } + + @Override + public StringBuilder handle(IsabelleMasterHandler trans, Term term) { + StringBuilder result = makeBoundedVarRef(trans, term, supportedOperators.get(term.op())); + result.append(". ("); + result.append(trans.translate(term.sub(0))).append("))"); + return result; + } + + /** + * Makes a reference to a binding variable and the variables it binds + * + * @param trans master handler used for translation + * @param term the term in which the binding variable occurs + * @param name name of the binding variable in translation + * @return a reference to a binding variable and the variables it binds + */ + public static StringBuilder makeBoundedVarRef(IsabelleMasterHandler trans, Term term, + String name) { + StringBuilder result = new StringBuilder("("); + result.append(name); + for (QuantifiableVariable bv : term.boundVars()) { + Sort sort = bv.sort(); + result.append(" ") + .append(LogicalVariableHandler.makeVarRef(trans, bv.name().toString(), sort)); + if (trans.isNewSort(sort)) { + trans.addGenericSort(sort); + } + } + return result; + } + +} diff --git a/keyext.isabelletranslation/src/main/java/org/key_project/isabelletranslation/translation/SeqDefHandler.java b/keyext.isabelletranslation/src/main/java/org/key_project/isabelletranslation/translation/SeqDefHandler.java new file mode 100644 index 0000000000..3a7f2d2a70 --- /dev/null +++ b/keyext.isabelletranslation/src/main/java/org/key_project/isabelletranslation/translation/SeqDefHandler.java @@ -0,0 +1,46 @@ +/* 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.translation; + +import java.io.IOException; +import java.util.HashMap; +import java.util.Map; +import java.util.Properties; + +import de.uka.ilkd.key.java.Services; + +import org.key_project.logic.Term; +import org.key_project.logic.op.Operator; + +/** + * Handles translation of seqDef function. + */ +public class SeqDefHandler implements IsabelleHandler { + + private final Map supportedOperators = new HashMap<>(); + + @Override + public void init(IsabelleMasterHandler masterHandler, Services services, + Properties handlerSnippets, String[] handlerOptions) throws IOException { + supportedOperators.put(services.getTypeConverter().getSeqLDT().getSeqDef(), "SeqDef"); + } + + @Override + public boolean canHandle(Operator op) { + return supportedOperators.containsKey(op); + } + + @Override + public StringBuilder handle(IsabelleMasterHandler trans, Term term) { + StringBuilder arg1 = trans.translate(term.sub(0)); + StringBuilder arg2 = trans.translate(term.sub(1)); + String arg3 = "(\\" + + LogicalVariableHandler.makeVarRef(trans, term.boundVars().get(0).name().toString(), + term.boundVars().get(0).sort()) + + ". " + + " to_any (" + trans.translate(term.sub(2)) + "))"; + + return new StringBuilder("(seqDef ").append(arg1).append(arg2).append(arg3).append(")"); + } +} diff --git a/keyext.isabelletranslation/src/main/java/org/key_project/isabelletranslation/translation/SortDependingFunctionHandler.java b/keyext.isabelletranslation/src/main/java/org/key_project/isabelletranslation/translation/SortDependingFunctionHandler.java new file mode 100644 index 0000000000..a02f7a17d1 --- /dev/null +++ b/keyext.isabelletranslation/src/main/java/org/key_project/isabelletranslation/translation/SortDependingFunctionHandler.java @@ -0,0 +1,72 @@ +/* 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.translation; + +import java.io.IOException; +import java.util.Properties; +import java.util.stream.Collectors; + +import de.uka.ilkd.key.java.Services; +import de.uka.ilkd.key.logic.op.SortDependingFunction; + +import org.key_project.logic.Term; +import org.key_project.logic.op.Operator; +import org.key_project.logic.sort.Sort; + +/** + * Handles translation of sort depending functions + */ +public class SortDependingFunctionHandler implements IsabelleHandler { + + @Override + public void init(IsabelleMasterHandler masterHandler, Services services, + Properties handlerSnippets, String[] handlerOptions) throws IOException { + + } + + @Override + public boolean canHandle(Operator op) { + return (op instanceof SortDependingFunction); + } + + @Override + public StringBuilder handle(IsabelleMasterHandler trans, Term term) { + assert term.op() instanceof SortDependingFunction; + SortDependingFunction op = (SortDependingFunction) term.op(); + Sort dependentSort = op.getSortDependingOn(); + + if (trans.isNewSort(dependentSort)) { + trans.addGenericSort(dependentSort); + } + StringBuilder name; + if (trans.isNewSymbol(term)) { + name = LogicalVariableHandler.makeVarRef(trans, op.name().toString().split("::")[1], + dependentSort); + trans.addSymbolAndDeclaration(term, name); + } else { + name = trans.getKnownSymbol(term); + } + + return getSortDependingFunctionRef(trans, term, op, name.toString()); + } + + /** + * Creates a reference to a sort depending function + * + * @param trans master handler used for translation + * @param term term the function occurs in + * @param op the function + * @param name the name of the function in translation + * @return reference to a sort depending function for use in translation + */ + static StringBuilder getSortDependingFunctionRef(IsabelleMasterHandler trans, Term term, + SortDependingFunction op, String name) { + StringBuilder ref = new StringBuilder("(").append(name).append("::"); + String parameterTypesDecl = + op.argSorts().stream().map(trans::translateSortName).collect(Collectors.joining("=>")); + ref.append(parameterTypesDecl).append("=>").append(trans.translateSortName(op.sort())) + .append(")"); + return UninterpretedSymbolsHandler.getFunctionRef(trans, term, op, ref.toString()); + } +} diff --git a/keyext.isabelletranslation/src/main/java/org/key_project/isabelletranslation/translation/UninterpretedSymbolsHandler.java b/keyext.isabelletranslation/src/main/java/org/key_project/isabelletranslation/translation/UninterpretedSymbolsHandler.java new file mode 100644 index 0000000000..ea94539be1 --- /dev/null +++ b/keyext.isabelletranslation/src/main/java/org/key_project/isabelletranslation/translation/UninterpretedSymbolsHandler.java @@ -0,0 +1,91 @@ +/* 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.translation; + +import java.util.List; +import java.util.Properties; + +import de.uka.ilkd.key.java.Services; +import de.uka.ilkd.key.logic.op.ProgramVariable; + +import org.key_project.logic.Term; +import org.key_project.logic.op.Function; +import org.key_project.logic.op.Operator; +import org.key_project.logic.op.SortedOperator; +import org.key_project.logic.sort.Sort; + +/** + * This handler is a fallback handler that introduces a new uninterpreted function symbol with + * prefix in subscript + *

+ * According declarations are added. + */ +public class UninterpretedSymbolsHandler implements IsabelleHandler { + + public final static String POSTFIX = "\\<^sub>v\\<^sub>a\\<^sub>r"; + + @Override + public void init(IsabelleMasterHandler masterHandler, Services services, + Properties handlerSnippets, + String[] handlerOptions) { + } + + @Override + public boolean canHandle(Operator op) { + return (op instanceof Function && !bindsVars(op)) || op instanceof ProgramVariable; + } + + /* + * return true if op binds in at least one argument. + */ + private static boolean bindsVars(Operator op) { + for (int i = 0; i < op.arity(); i++) { + if (op.bindVarsAt(i)) { + return true; + } + } + return false; + } + + @Override + public StringBuilder handle(IsabelleMasterHandler trans, Term term) { + SortedOperator op = (SortedOperator) term.op(); + if (trans.isNewSymbol(term)) { + String name = op.name() + POSTFIX; + trans.addSymbolAndDeclaration(term, + new StringBuilder(name.replace("::", "_").replace(".", "_") + .replace("$", "_").replace("#", "_"))); + } + + String name = trans.getKnownSymbol(term).toString(); + return getFunctionRef(trans, term, op, name); + } + + /** + * Creates a reference to a function for use in translations. + * + * @param trans master handler used for translation + * @param term the term the function occurs in as the top operator + * @param op the function + * @param name name of the function in translations + * @return a reference to a function for use in translations. + */ + static StringBuilder getFunctionRef(IsabelleMasterHandler trans, Term term, SortedOperator op, + String name) { + List children = trans.translate(term.subs()); + StringBuilder result = new StringBuilder("("); + result.append(name); + + for (StringBuilder child : children) { + result.append(" ").append(child); + } + Sort sort = op.sort(); + if (trans.isNewSort(sort)) { + trans.addGenericSort(sort); + } + result.append(")"); + return result; + } + +} diff --git a/keyext.isabelletranslation/src/main/resources/META-INF/services/de.uka.ilkd.key.gui.extension.api.KeYGuiExtension b/keyext.isabelletranslation/src/main/resources/META-INF/services/de.uka.ilkd.key.gui.extension.api.KeYGuiExtension new file mode 100644 index 0000000000..9138565744 --- /dev/null +++ b/keyext.isabelletranslation/src/main/resources/META-INF/services/de.uka.ilkd.key.gui.extension.api.KeYGuiExtension @@ -0,0 +1 @@ +org.key_project.isabelletranslation.IsabelleTranslationExtension \ No newline at end of file diff --git a/keyext.isabelletranslation/src/main/resources/org/key_project/isabelletranslation/ROOT b/keyext.isabelletranslation/src/main/resources/org/key_project/isabelletranslation/ROOT new file mode 100644 index 0000000000..0dec1b31ef --- /dev/null +++ b/keyext.isabelletranslation/src/main/resources/org/key_project/isabelletranslation/ROOT @@ -0,0 +1,7 @@ +session KeYTranslations = HOL + + options [document=false] + sessions "HOL-Combinatorics" + theories + TranslationPreamble + document_files + "root.tex" \ No newline at end of file diff --git a/keyext.isabelletranslation/src/main/resources/org/key_project/isabelletranslation/root.tex b/keyext.isabelletranslation/src/main/resources/org/key_project/isabelletranslation/root.tex new file mode 100644 index 0000000000..aa5dbaa6a3 --- /dev/null +++ b/keyext.isabelletranslation/src/main/resources/org/key_project/isabelletranslation/root.tex @@ -0,0 +1,60 @@ +\documentclass[11pt,a4paper]{article} +\usepackage[T1]{fontenc} +\usepackage{isabelle,isabellesym} + +% further packages required for unusual symbols (see also +% isabellesym.sty), use only when needed + +%\usepackage{amssymb} + %for \, \, \, \, \, \, + %\, \, \, \, \, + %\, \, \ + +%\usepackage{eurosym} + %for \ + +%\usepackage[only,bigsqcap,bigparallel,fatsemi,interleave,sslash]{stmaryrd} + %for \, \, \, \, \ + +%\usepackage{eufrak} + %for \ ... \, \ ... \ (also included in amssymb) + +%\usepackage{textcomp} + %for \, \, \, \, \, + %\ + +% this should be the last package used +\usepackage{pdfsetup} + +% urls in roman style, theory text in math-similar italics +\urlstyle{rm} +\isabellestyle{it} + +% for uniform font size +%\renewcommand{\isastyle}{\isastyleminor} + + +\begin{document} + +\title{KeYTranslations} +\author{Nils Buchholz} +\maketitle + +\tableofcontents + +% sane default for proof documents +\parindent 0pt\parskip 0.5ex + +% generated text of all theories +\input{session} + +% optional bibliography +%\bibliographystyle{abbrv} +%\bibliography{root} + +\end{document} + +%%% Local Variables: +%%% mode: latex +%%% TeX-master: t +%%% End: \ No newline at end of file diff --git a/keyext.isabelletranslation/src/main/resources/org/key_project/isabelletranslation/translation/DefinedSymbolsHandler.preamble.xml b/keyext.isabelletranslation/src/main/resources/org/key_project/isabelletranslation/translation/DefinedSymbolsHandler.preamble.xml new file mode 100644 index 0000000000..0dd3102e77 --- /dev/null +++ b/keyext.isabelletranslation/src/main/resources/org/key_project/isabelletranslation/translation/DefinedSymbolsHandler.preamble.xml @@ -0,0 +1,379 @@ + + + + + General preamble + +declare [[coercion_enabled]] +declare [[coercion_map image]] +typedecl any + +consts + bottom::"any" + +specification (bottom) "bottom = bottom" + by simp + +lemma bottom_in_any:"bottom \<in> (UNIV::any set)" + by simp + +typedef javaDL_type = "(UNIV::any set set)" + by auto + +setup_lifting type_definition_javaDL_type +lift_definition typeof::"any\<Rightarrow>javaDL_type\<Rightarrow>bool" is Set.member. +lift_definition subtype::"javaDL_type\<Rightarrow>javaDL_type\<Rightarrow>bool" is Set.subset_eq. +lift_definition strict_subtype::"javaDL_type\<Rightarrow>javaDL_type\<Rightarrow>bool" is Set.subset. +lift_definition disjointTypes::"javaDL_type\<Rightarrow>javaDL_type\<Rightarrow>bool" is Set.disjnt. + +consts + int_UNIV::"any set" + int2any::"int\<Rightarrow>any" + any2int::"any\<Rightarrow>int" + +axiomatization where int_sub_any[simp]:"type_definition int2any any2int (int_UNIV)" +declare [[coercion int2any]] + +interpretation int:type_definition int2any any2int int_UNIV + by simp + + +definition int_type::"javaDL_type" where "int_type \<equiv> Abs_javaDL_type (UNIV::int set)" + +consts + bool_UNIV::"any set" + bool2any::"bool\<Rightarrow>any" + any2bool::"any\<Rightarrow>bool" + +axiomatization where bool_sub_any[simp]:"type_definition bool2any any2bool (bool_UNIV)" +declare [[coercion bool2any]] + +interpretation bool:type_definition bool2any any2bool bool_UNIV + by simp + + +definition bool_type::"javaDL_type" where "bool_type \<equiv> Abs_javaDL_type (UNIV::bool set)" + + + + + +consts + java_lang_Object_UNIV::"any set" + + +specification (java_lang_Object_UNIV) "java_lang_Object_UNIV \<subseteq> (UNIV::any set)" + "bottom:java_lang_Object_UNIV" + by auto + +lemma java_lang_Object_UNIV_specification:"java_lang_Object_UNIV \<subseteq> (UNIV::any set) \<and> + bottom:java_lang_Object_UNIV" + by (metis (mono_tags, lifting) java_lang_Object_UNIV_def UNIV_I subset_UNIV verit_sko_ex_indirect) + + +typedef java_lang_Object = "java_lang_Object_UNIV" + morphisms java_lang_Object2any any2java_lang_Object + using java_lang_Object_UNIV_specification by auto + +declare [[coercion java_lang_Object2any]] + +definition java_lang_Object_type::"javaDL_type" where "java_lang_Object_type \<equiv> Abs_javaDL_type (UNIV::java_lang_Object set)" + +lemma java_lang_Object_subset_any[simp]:"(UNIV::java_lang_Object set) \<subseteq> (UNIV::any set)" + by simp + +lemma bottom_in_java_lang_Object[simp] :"bottom \<in> (UNIV::java_lang_Object set)" + using java_lang_Object_UNIV_specification + using type_definition.Rep_range type_definition_java_lang_Object by blast + + +consts + Field_UNIV::"any set" + +specification (Field_UNIV) "Field_UNIV \<subseteq> (UNIV::any set)" + "Field_UNIV \<noteq> {}" + by auto + +lemma Field_UNIV_specification:"Field_UNIV \<subseteq> (UNIV::any set) \<and> + Field_UNIV \<noteq> {}" + by (metis (mono_tags, lifting) Field_UNIV_def empty_not_UNIV someI_ex top_greatest) + +typedef Field = Field_UNIV + morphisms Field2any any2Field + using Field_UNIV_specification by auto + +declare [[coercion Field2any]] + +consts + created::"Field" + fieldType::"Field\<Rightarrow>javaDL_type" + +axiomatization arr::"int\<Rightarrow>Field" where arr_inject[simp]:"(arr x = arr y) = (x = y)" + +definition Field_type::"javaDL_type" where "Field_type \<equiv> Abs_javaDL_type (UNIV::Field set)" + + +typedef LocSet = "UNIV::(java_lang_Object \<times> Field) set set" + by simp + + +setup_lifting type_definition_LocSet +lift_definition elementOf::"java_lang_Object \<Rightarrow> Field \<Rightarrow>LocSet\<Rightarrow>bool" is "\<lambda>obj f s. (obj, f) \<in> s". +lift_definition empty::"LocSet" is Set.empty. +lift_definition allLocs::"LocSet" is Set.UNIV. +lift_definition singleton::"java_lang_Object\<Rightarrow>Field\<Rightarrow>LocSet" is "\<lambda>obj f. {(obj, f)}". +lift_definition disjoint::"LocSet\<Rightarrow>LocSet\<Rightarrow>bool" is Set.disjnt. +lift_definition union::"LocSet\<Rightarrow>LocSet\<Rightarrow>LocSet" is Set.union. +lift_definition intersect::"LocSet\<Rightarrow>LocSet\<Rightarrow>LocSet" is Set.inter. +lift_definition setMinus::"LocSet\<Rightarrow>LocSet\<Rightarrow>LocSet" is minus. +lift_definition allFields::"java_lang_Object\<Rightarrow>LocSet" is "\<lambda>x. {x} \<times> (UNIV::Field set)". +lift_definition allObjects::"Field\<Rightarrow>LocSet" is "\<lambda>x. (UNIV::java_lang_Object set) \<times> {x}". +lift_definition arrayRange::"java_lang_Object\<Rightarrow>int\<Rightarrow>int\<Rightarrow>LocSet" is "\<lambda>obj x y. {obj} \<times> (image arr {x..y})". +lift_definition subset::"LocSet\<Rightarrow>LocSet\<Rightarrow>bool" is Set.subset. +lift_definition infiniteUnion::"LocSet set\<Rightarrow>LocSet" is Complete_Lattices.Union. + +consts + LocSet_Image::"any set" + LocSet2any::"LocSet\<Rightarrow>any" + any2LocSet::"any\<Rightarrow>LocSet" + +axiomatization where LocSet_sub_any:"type_definition LocSet2any any2LocSet LocSet_Image" + +declare [[coercion LocSet2any]] + +interpretation LocSet:type_definition LocSet2any any2LocSet LocSet_Image + by (rule LocSet_sub_any) + + +definition LocSet_type::"javaDL_type" where "LocSet_type \<equiv> Abs_javaDL_type (UNIV::LocSet set)" + + + +typedef Heap = "UNIV::(java_lang_Object \<Rightarrow> Field \<Rightarrow> any) set" + by simp + +declare [[coercion Rep_Heap]] + +consts + Heap_Image::"any set" + Heap2any::"Heap\<Rightarrow>any" + any2Heap::"any\<Rightarrow>Heap" + +axiomatization where Heap_sub_any:"type_definition Heap2any any2Heap Heap_Image" + +declare [[coercion Heap2any]] + +interpretation Heap:type_definition Heap2any any2Heap Heap_Image + by (rule Heap_sub_any) + + +definition Heap_type::"javaDL_type" where "Heap_type \<equiv> Abs_javaDL_type (UNIV::Heap set)" + + +class any = + fixes to_any::"'a\<Rightarrow>any" + fixes cast::"any\<Rightarrow>'a" + +instantiation any::any +begin +fun to_any_any where "to_any_any x = (id::any\<Rightarrow>any) x" +fun cast_any where "cast_any x = (id::any\<Rightarrow>any) x" +instance by standard +end + +instantiation int::any +begin +fun to_any_int where "to_any_int x = int2any x" +fun cast_int where "cast_int x = any2int x" +instance by standard +end + +instantiation bool::any +begin +fun to_any_bool where "to_any_bool x = bool2any x" +fun cast_bool where "cast_bool x = any2bool x" +instance by standard +end + +instantiation Field::any +begin +fun to_any_Field where "to_any_Field x = Field2any x" +fun cast_Field where "cast_Field x = any2Field x" +instance by standard +end + +instantiation LocSet::any +begin +fun to_any_LocSet where "to_any_LocSet x = LocSet2any x" +fun cast_LocSet where "cast_LocSet x = any2LocSet x" +instance by standard +end + +instantiation Heap::any +begin +fun to_any_Heap where "to_any_Heap x = Heap2any x" +fun cast_Heap where "cast_Heap x = any2Heap x" +instance by standard +end + +instantiation java_lang_Object::any +begin +fun cast_java_lang_Object where "cast_java_lang_Object x = any2java_lang_Object x" +fun to_any_java_lang_Object where "to_any_java_lang_Object x = java_lang_Object2any x" +instance by standard +end + +typedef (overloaded) Null = "{bottom}" + morphisms Null2any any2Null + by simp + +declare [[coercion Null2any]] + +lemma bottom_Null_set:"(UNIV::Null set) = {bottom}" + using type_definition.Rep_range type_definition_Null by blast + +lemma Null_sub_java_lang_Object_Types: "(UNIV::Null set) \<subseteq> (UNIV::java_lang_Object set)" + using bottom_Null_set bottom_in_java_lang_Object by auto + +definition "null \<equiv> any2Null bottom" + +instantiation Null::any +begin +fun to_any_Null where "to_any_Null (x::Null) = Null2any x" +fun cast_Null where "cast_Null x = any2Null x" +instance by standard +end + +abbreviation "Null2java_lang_Object\<equiv>any2java_lang_Object \<circ> Null2any" + +declare [[coercion Null2java_lang_Object]] + +fun instanceof::"any\<Rightarrow>javaDL_type\<Rightarrow>bool" + where "instanceof x type = typeof x type" + +typedef Seq = "UNIV::any list set" + by auto + +axiomatization Seq2any any2Seq Seq_UNIV + where Seq_sub_any:"type_definition (Seq2any::Seq\<Rightarrow>any) (any2Seq::any\<Rightarrow>Seq) (Seq_UNIV::any set)" + +declare [[coercion Seq2any]] + +interpretation Seq:type_definition Seq2any any2Seq Seq_UNIV + by (rule Seq_sub_any) + + +instantiation Seq::any +begin +fun to_any_Seq where "to_any_Seq (x::Seq) = Seq2any x" +fun cast_Seq where "cast_Seq (x::any) = any2Seq x" +instance by standard +end + +definition Seq_type::"javaDL_type" where "Seq_type \<equiv> Abs_javaDL_type (UNIV::Seq set)" + +consts + seqGetOutside::any + +setup_lifting type_definition_Seq +lift_definition seqLen::"Seq\<Rightarrow>int" is "int \<circ> List.length". +lift_definition seqGet::"Seq\<Rightarrow>int\<Rightarrow>'a::any" is "\<lambda>s i. (if (0::int)\<le>i\<and>i<(int (length s)) then cast (s ! (nat i)) else cast seqGetOutside)". +lift_definition seqDef::"int\<Rightarrow>int\<Rightarrow>(int\<Rightarrow>any)\<Rightarrow>Seq" is "\<lambda>le ri e. map e [le..ri - 1]". +lift_definition seqEmpty::"Seq" is "[]". +lift_definition seqSingleton::"any\<Rightarrow>Seq" is "\<lambda>x. [x]". +lift_definition seqConcat::"Seq\<Rightarrow>Seq\<Rightarrow>Seq" is List.append. +lift_definition seqReverse::"Seq\<Rightarrow>Seq" is List.rev. +lift_definition seqPerm::"Seq\<Rightarrow>Seq\<Rightarrow>bool" is List_Permutation.perm. + +fun seqNPerm::"Seq\<Rightarrow>bool" + where "seqNPerm s = seqPerm s (seqDef 0 (seqLen s - 1) (to_any))" + +fun seqSub::"Seq\<Rightarrow>int\<Rightarrow>int\<Rightarrow>Seq" where + "seqSub s i j = seqDef i j (\<lambda>x. seqGet s x)" + +primrec (nonexhaustive) listIndexOf::"'a list\<Rightarrow>'a\<Rightarrow>int" where + "listIndexOf (x#xs) a = (if (x=a) then 0 else 1+(listIndexOf xs a))" + +lift_definition seqIndexOf::"Seq\<Rightarrow>any\<Rightarrow>int" is "listIndexOf". + +fun listSwap::"'a list\<Rightarrow>int\<Rightarrow>int\<Rightarrow>'a list" + where "listSwap l i j = +(if \<not>(0\<le>i \<and> i<int (length l) \<and> 0\<le>j \<and> i<int (length l)) +then l +else list_update (list_update l (nat i) (l ! (nat j))) (nat j) (l ! (nat i)))" + +lift_definition seqSwap::"Seq\<Rightarrow>int\<Rightarrow>int\<Rightarrow>Seq" is listSwap. + +fun listRemove::"'a list\<Rightarrow>nat\<Rightarrow>'a list" + where "listRemove [] _ = []" + | "listRemove (x#xs) 0 = xs" + | "listRemove (x#xs) (Suc k) = x # (listRemove xs k)" + +lift_definition seqRemove::"Seq\<Rightarrow>int\<Rightarrow>Seq" is "\<lambda>s (i::int). (if \<not>(0\<le>i \<and> i<int (length s)) then s else listRemove s (nat i))". + + +consts + exactInstance::"any\<Rightarrow>javaDL_type\<Rightarrow>bool" + +axiomatization obj_length::"java_lang_Object\<Rightarrow>int" where length_nonneg[simp]:"obj_length obj \<ge> 0" + +fun unusedLocs where "unusedLocs (h::Heap) = Abs_LocSet {((obj::java_lang_Object), (f::Field)). (h obj created=False)\<and> obj\<noteq>null}" + +fun select::"Heap\<Rightarrow>java_lang_Object\<Rightarrow>Field\<Rightarrow>'a::any" where + "select h obj f = cast (h obj f)" + +fun anon::"Heap\<Rightarrow>LocSet\<Rightarrow>Heap\<Rightarrow>Heap" where + "anon h1 s h2 = Abs_Heap (\<lambda>(obj::java_lang_Object) (f::Field). (if elementOf obj f s \<and> f\<noteq>created \<or> elementOf obj f (unusedLocs h1) + then select h2 obj f else select h1 obj f))" + +fun store::"Heap\<Rightarrow>java_lang_Object\<Rightarrow>Field\<Rightarrow>any\<Rightarrow>Heap" where + "store h obj f x = Abs_Heap (\<lambda>(obj'::java_lang_Object) (f'::Field). (if obj'=obj \<and> f'=f \<and> f\<noteq>created then x else h obj' f'))" + +fun create::"Heap\<Rightarrow>java_lang_Object\<Rightarrow>Heap" where + "create h obj = Abs_Heap (\<lambda>(obj'::java_lang_Object) (f'::Field). (if obj'=obj \<and> f'=created \<and> obj\<noteq>null then cast True else h obj' f'))" + + +class array = any + + fixes element_type::"'a\<Rightarrow>javaDL_type" + +section \<open>wellFormed Axioms\<close> +axiomatization wellFormed::"Heap\<Rightarrow>bool" where + onlyCreatedjava_lang_ObjecteAreReferenced:"wellFormed h \<Longrightarrow> select h obj f = null \<or> + ((select h (select h obj f) created)::bool)" + and onlyCreatedjava_lang_ObjectsAreInLocSets:"wellFormed h \<and> elementOf (o2::java_lang_Object) f2 ((select + h obj f)::LocSet) \<Longrightarrow> Null2java_lang_Object null=o2 \<or> ((select h o2 + created)::bool)" + and wellFormedStorejava_lang_Object:"wellFormed h \<and> ((x::java_lang_Object)=null \<or> ((select + h x created) \<and> instanceof x (fieldType f))) \<Longrightarrow> wellFormed (store h obj f x)" + and wellFormedStoreLocSet:"wellFormed h \<and> (\<forall>ov fv. (elementOf ov fv y \<longrightarrow> ov = null \<or> select h ov created)) + \<Longrightarrow> wellFormed (store h obj f y)" + and wellFormedStorePrimitive:"(typeof x (fieldType f) \<Longrightarrow> \<not>typeof x java_lang_Object_type \<Longrightarrow> \<not>typeof x LocSet_type \<Longrightarrow> wellFormed h + \<Longrightarrow> wellFormed (store h obj f x))" + and wellFormedCreate:"wellFormed h \<Longrightarrow> wellFormed (create h obj)" + and wellFormedAnon:"wellFormed h \<and> wellFormed h2 \<Longrightarrow> wellFormed (anon h y h2)" + +axiomatization where wellFormedStoreArray:"wellFormed h \<and> ((x::java_lang_Object)=null \<or> (select h x created \<and> (typeof x (element_type obj)))) + \<Longrightarrow> wellFormed (store h (cast (to_any (obj::'a::{array, any}))) (arr idx) x)" + +lemma induct_sum_upper_limit: + fixes f::"int\<Rightarrow>int" + fixes lower::int + fixes upper::int + assumes "lower<upper" + shows "(\<Sum>(i::int) = lower..<upper. f i) = (\<Sum>(i::int) = lower..<upper - 1. f i) + f (upper - 1)" +proof - + have "{lower..<upper} = {lower..<upper-1} \<union> {upper-1..<upper}" + using assms by auto + have "{upper-1..<upper} = {upper - 1}" + by auto + then have "sum f ({lower..<upper-1} \<union> {upper-1..<upper}) = (\<Sum>(i::int) = lower..<upper-1. f i) + (\<Sum>(i::int) = upper-1..<upper. f i) - sum f ({lower..<upper-1} \<inter> {upper-1..<upper})" + by (subst sum.union_inter [symmetric]) (auto simp add: algebra_simps) + then have "sum f {lower..<upper} = (\<Sum>(i::int) = lower..<upper-1. f i) + (\<Sum>(i::int) = upper-1..<upper. f i) - sum f ({lower..<upper-1} \<inter> {upper-1..<upper})" + using \<open>{lower..<upper} = {lower..<upper-1} \<union> {upper-1..<upper}\<close> by presburger + also have "... = (\<Sum>(i::int) = lower..<upper-1. f i) + (\<Sum>(i::int) = upper-1..<upper. f i)" + by simp + finally show ?thesis + using \<open>{upper-1..<upper} = {upper - 1}\<close> by auto +qed + + diff --git a/keyext.isabelletranslation/src/main/resources/org/key_project/isabelletranslation/translation/IntegerOpHandler.preamble.xml b/keyext.isabelletranslation/src/main/resources/org/key_project/isabelletranslation/translation/IntegerOpHandler.preamble.xml new file mode 100644 index 0000000000..82b715b068 --- /dev/null +++ b/keyext.isabelletranslation/src/main/resources/org/key_project/isabelletranslation/translation/IntegerOpHandler.preamble.xml @@ -0,0 +1,246 @@ + + + + +General preamble + +locale jArithmetics = + fixes jDiv::"int\<Rightarrow>int\<Rightarrow>int" + assumes jDiv_def [simp]: "b\<noteq>0 \<Longrightarrow> jDiv a b = +(if ((a\<le>0 \<and> b<0) \<or> (a\<ge>0 \<and> b>0) \<or> (b dvd a)) then (a div b) +else ((a div b) + 1))" + +fixes euclMod::"int\<Rightarrow>int\<Rightarrow>int" +assumes eucl_Mod_def [simp]: "l\<noteq>0 \<Longrightarrow> euclMod k l = (if (k mod l < 0) then ((k mod l) + abs(l)) +else (k mod l))" +begin + +definition int_HALFRANGE::int where [simp, intro]:"int_HALFRANGE=2^31" +definition int_RANGE::int where [simp, intro]:"int_RANGE=2^32" +definition int_MIN::int where [simp, intro]:"int_MIN=-(2^31)" + +lemma jDiv_spec_requirement: + fixes a::int + fixes b::int + assumes "b\<noteq>0" + shows "abs(jDiv a b * b) \<le> abs(a) \<and> abs(a) < abs(jDiv a b * b) + abs(b)" +proof - + have "abs(jDiv a b * b) + abs(b) \<equiv> abs(jDiv a b) * abs(b) + abs(b)" + by (simp add: abs_mult) + also have "... \<equiv> (abs(jDiv a b) + 1) * abs(b)" + by algebra + finally have dist_jDiv_largest: "abs(jDiv a b * b) + abs(b) \<equiv> abs((abs(jDiv a b) + 1) * b)" + by (simp add: abs_mult) + consider (is_Div) "(a\<ge>0 \<and> b>0) \<or> (a\<le>0) \<and> (b<0) \<or> (b dvd a)" | (not_Div) "(a<0\<and>b>0 \<or> a>0\<and>b<0) \<and> \<not>(b dvd a)" using assms by linarith + then show ?thesis + proof cases + case is_Div + then have jDiv_eq_div: "jDiv a b = a div b" using assms by auto + consider (b_dvd_a) "b dvd a" | (both_pos) "(a>0 \<and> b>0)" | (both_neg) "(a<0) \<and> (b<0)" using is_Div by (metis dvd_0_right leD linorder_neqE_linordered_idom) + then show ?thesis + proof cases + case (b_dvd_a) + then have "a div b * b = a" using assms by simp + then show ?thesis by (simp add: assms jDiv_eq_div) + next + case (both_pos) + then have "abs(a div b * b) \<le> abs(a) \<equiv> a div b * b \<le> a" + by (simp add:pos_imp_zdiv_nonneg_iff) + also + have "... \<equiv> a div b * b \<le> a div b * b + a mod b" using both_pos by simp + also + have "... \<equiv> 0 \<le> a mod b" using both_pos by linarith + finally + have req:"abs(jDiv a b * b) \<le> abs(a)" + by (simp add: both_pos jDiv_eq_div) + have "a mod b < abs(b)" using both_pos by auto + then have "a < a div b * b + abs(b)" + by (metis add.commute add_less_cancel_right mod_mult_div_eq mult.commute) + then have largest:"abs(a) < abs(jDiv a b * b) + abs(b)" using both_pos by auto + then show ?thesis using req largest by blast + next + case (both_neg) + then have "abs(a div b * b) \<le> abs (a) \<equiv> -(a div b * b) \<le> -a" + by (simp add: div_int_pos_iff mult_nonneg_nonpos) + also + have "... \<equiv> a div b * b \<ge> a div b * b + a mod b" by simp + also + have "... \<equiv> 0 \<ge> a mod b" by linarith + finally + have req:"abs(jDiv a b * b) \<le> abs(a)" + by (simp add: both_neg jDiv_eq_div) + have "abs(a) < abs(jDiv a b * b) + abs(b) \<equiv> -((a div b * b) + a mod b) < abs(a div b * b) - b" using both_neg by simp + also have "... \<equiv> -((a div b * b) + a mod b) < -(a div b * b) - b" using both_neg by (simp add: div_int_pos_iff mult_nonneg_nonpos) + also have "... \<equiv> (a div b * b) + a mod b > (a div b * b) + b" by linarith + also have "... \<equiv> a mod b > b" by linarith + finally have largest:"abs(a) < abs(jDiv a b * b) + abs(b)" using both_neg neg_mod_bound by blast + then show ?thesis using req largest by blast + qed + next + case not_Div + then have jDiv_eq_divplus: "jDiv a b = (a div b) + 1" using assms by auto + then have "abs(jDiv a b * b) \<le> abs(a) \<equiv> abs(a div b * b + b) \<le> abs(a div b * b + a mod b)" + by (simp add: distrib_left mult.commute) + consider (b_neg) "b<0\<and>a>0" | (b_pos) "b>0\<and>a<0" using assms not_Div by linarith + then show ?thesis + proof cases + case (b_neg) + then have quotient_neg:"a div b < 0" + by (simp add: neg_imp_zdiv_neg_iff) + then have abs_jDiv:"abs((jDiv a b) * b) = (a div b + 1) * b" using b_neg jDiv_eq_divplus + by (simp add: mult_nonpos_nonpos) + then have "abs(jDiv a b * b) \<le> abs(a) \<equiv> (a div b + 1) * b \<le> a div b * b + a mod b" + by (simp add: abs_of_pos b_neg jDiv_eq_divplus) + also have "... \<equiv> a div b * b + b \<le> a div b * b + a mod b" + by (simp add: distrib_left mult.commute) + also have "... \<equiv> b \<le> a mod b" + by linarith + finally have requirement:"abs(jDiv a b * b) \<le> abs(a)" using b_neg neg_mod_bound order_less_imp_le + by blast + + have mod_le_zero:"a mod b < 0" using mod_eq_0_iff_dvd not_Div b_neg neg_mod_sign + by (metis linorder_not_less verit_la_disequality) + + have "abs(a) < abs(jDiv a b * b) + abs(b) \<equiv> a < ((a div b + 1) * b) + abs(b)" using jDiv_eq_divplus b_neg abs_jDiv + by simp + also have "... \<equiv> a < a div b * b + b + abs b" + by (simp add: distrib_left mult.commute) + also have "... \<equiv> a < a div b * b" using b_neg abs_of_neg + by simp + also have "... \<equiv> a div b * b + a mod b < a div b * b" using mult_div_mod_eq + by simp + also have "... \<equiv> a mod b < 0" + by linarith + finally have largest:"abs(a) < abs(jDiv a b * b) + abs(b)" using mod_le_zero + by blast + + show ?thesis using requirement largest by blast + next + case (b_pos) + then have "a div b < 0" + by (simp add: pos_imp_zdiv_neg_iff) + then have abs_jDiv:"abs((jDiv a b) * b) = -((a div b + 1) * b)" using b_pos jDiv_eq_divplus + by (simp add: mult_le_0_iff) + then have "abs(jDiv a b * b) \<le> abs(a) \<equiv> -((a div b + 1) * b) \<le> -(a div b * b + a mod b)" + by (simp add: abs_of_neg b_pos jDiv_eq_divplus) + also have "... \<equiv> (a div b + 1) * b \<ge> a div b * b + a mod b" + by simp + also have "... \<equiv> a div b * b + b \<ge> a div b * b + a mod b" + by (simp add: distrib_left mult.commute abs_of_neg b_pos jDiv_eq_divplus) + also have "... \<equiv> b \<ge> a mod b" by linarith + finally have requirement:"abs(jDiv a b * b) \<le> abs(a)" using b_pos pos_mod_bound order_less_imp_le + by blast + + have mod_greater_zero:"a mod b > 0" using mod_eq_0_iff_dvd not_Div + by (metis b_pos mod_int_pos_iff order_antisym_conv verit_comp_simplify1(3)) + + have "abs(a) < abs(jDiv a b * b) + abs(b) \<equiv> -a < -((a div b + 1) * b) + abs(b)" using jDiv_eq_divplus b_pos abs_jDiv + by simp + also have "... \<equiv> -a < -(a div b * b) - b + abs b" + by (simp add: distrib_left mult.commute) + also have "... \<equiv> a > a div b * b" using b_pos abs_of_pos + by simp + also have "... \<equiv> a div b * b + a mod b > a div b * b" using mult_div_mod_eq + by simp + also have "... \<equiv> a mod b > 0" + by linarith + finally have largest:"abs(a) < abs(jDiv a b * b) + abs(b)" + using mod_greater_zero by blast + + show ?thesis using requirement largest by blast + qed + qed +qed + +fun jMod::"int\<Rightarrow>int\<Rightarrow>int" where +"jMod a b = a - (jDiv a b)*b" + +lemma jMod_jDiv_eq: + fixes a::int + fixes b::int + assumes "b\<noteq>0" + shows "a = (jDiv a b)*b + jMod a b" + by simp + +fun moduloInt::"int\<Rightarrow>int" + where "moduloInt a = int_MIN + ((int_HALFRANGE + a) mod (int_RANGE))" + +fun jAdd::"int\<Rightarrow>int\<Rightarrow>int" + where "jAdd a b = moduloInt (a+b)" + +fun jSub:: "int\<Rightarrow>int\<Rightarrow>int" where + "jSub a b = moduloInt (a-b)" + +fun jMul:: "int\<Rightarrow>int\<Rightarrow>int" where + "jMul a b = moduloInt (a*b)" + +lemma euclMod_spec: + fixes a::int + fixes b::int + assumes "b\<noteq>0" + shows "0\<le>euclMod a b \<and> euclMod a b < abs(b)" +proof - + consider (mod_neg) "a mod b < 0" | (mod_nonneg) "a mod b\<ge>0" by linarith + then show ?thesis + proof cases + case (mod_neg) + then have "0\<le>euclMod a b \<and> euclMod a b < abs(b) \<equiv> 0\<le>a mod b + abs(b) \<and> a mod b + abs(b) < abs(b)" using assms + by auto + also have "... \<equiv> -abs(b)\<le>a mod b \<and> a mod b + abs(b) < abs(b)" + by linarith + also have "... \<equiv> abs(b) \<ge> abs(a mod b) \<and> a mod b + abs(b) < abs(b)" + using mod_neg by linarith + also have "... \<equiv> a mod b + abs(b) < abs(b)" + by (simp add: abs_mod_less assms dual_order.order_iff_strict) + finally show ?thesis + using mod_neg by auto + next + case (mod_nonneg) + then have "0\<le>euclMod a b \<and> euclMod a b < abs(b) \<equiv> 0\<le>a mod b \<and> a mod b < abs(b)" using assms + by auto + + then show ?thesis + by (metis abs_mod_less abs_of_nonneg assms mod_nonneg) + qed +qed + +fun euclDiv::"int\<Rightarrow>int\<Rightarrow>int" where +"(euclDiv k l) = (k - euclMod k l) div l" + +lemma euclMod_euclDiv_eq: + fixes a::int + fixes b::int + assumes "b\<noteq>0" + shows "a = euclDiv a b * b + euclMod a b" +proof - + consider (mod_le0) "a mod b<0" | (mod_geq0) "a mod b\<ge>0" by linarith + then show ?thesis +proof cases + case mod_le0 + then have "euclMod a b = a mod b + abs(b)" using assms + by simp + then have "euclMod a b = a - ((a div b) * b) + abs(b)" + by (metis minus_div_mult_eq_mod) + then have "(euclDiv a b) = (a div b * b) div b - (abs(b)) div b" + by simp + then have "euclDiv a b = (a div b) - sgn(b)" + by (metis div_by_0 linordered_idom_class.abs_sgn nonzero_mult_div_cancel_left nonzero_mult_div_cancel_right sgn_0) + then have "euclDiv a b * b = (a div b)*b - abs b" + by (metis linordered_idom_class.abs_sgn mult.commute right_diff_distrib') + then show ?thesis using assms + by auto +next + case mod_geq0 + then have euclMod_eq_mod:"euclMod a b = a mod b" using assms + by simp + then have "euclDiv a b = a div b" + by (simp add: minus_mod_eq_mult_div) + then show ?thesis using euclMod_eq_mod + by auto + qed +qed +end + + + jArithmetics + diff --git a/keyext.isabelletranslation/src/main/resources/org/key_project/isabelletranslation/translation/defaultHandlers.txt b/keyext.isabelletranslation/src/main/resources/org/key_project/isabelletranslation/translation/defaultHandlers.txt new file mode 100644 index 0000000000..fbe87b6245 --- /dev/null +++ b/keyext.isabelletranslation/src/main/resources/org/key_project/isabelletranslation/translation/defaultHandlers.txt @@ -0,0 +1,15 @@ +org.key_project.isabelletranslation.translation.DefinedSymbolsHandler +org.key_project.isabelletranslation.translation.InstanceOperatorHandler +org.key_project.isabelletranslation.translation.BooleanOpHandler +org.key_project.isabelletranslation.translation.PolymorphicHandler +org.key_project.isabelletranslation.translation.QuantifierHandler +org.key_project.isabelletranslation.translation.LogicalVariableHandler +org.key_project.isabelletranslation.translation.NumberConstantsHandler +org.key_project.isabelletranslation.translation.IntegerOpHandler +org.key_project.isabelletranslation.translation.InfiniteUnionHandler +org.key_project.isabelletranslation.translation.BSumHandler +org.key_project.isabelletranslation.translation.SeqDefHandler +org.key_project.isabelletranslation.translation.SortDependingFunctionHandler +org.key_project.isabelletranslation.translation.FieldHandler +org.key_project.isabelletranslation.translation.ObserverFunctionHandler +org.key_project.isabelletranslation.translation.UninterpretedSymbolsHandler \ No newline at end of file diff --git a/settings.gradle b/settings.gradle index 171f3b1d56..5a33f30e72 100644 --- a/settings.gradle +++ b/settings.gradle @@ -15,6 +15,7 @@ include 'keyext.proofmanagement' include 'keyext.exploration' include 'keyext.slicing' include 'keyext.caching' +include 'keyext.isabelletranslation' // ENABLE NULLNESS here or on the CLI // This flag is activated to enable the checker framework.