Commit 6273e7d4 authored by Sarah Grebing's avatar Sarah Grebing
Browse files

Resolved mergeconlcit

parents 1ee32d19 b247aa36
......@@ -4,8 +4,8 @@ import com.google.common.collect.Sets;
import de.uka.ilkd.key.java.Services;
import de.uka.ilkd.key.logic.*;
import de.uka.ilkd.key.logic.op.QuantifiableVariable;
import edu.kit.formal.psdb.termmatcher.MatchPatternLexer;
import edu.kit.formal.psdb.termmatcher.MatchPatternParser;
import edu.kit.iti.formal.psdbg.termmatcher.MatchPatternLexer;
import edu.kit.iti.formal.psdbg.termmatcher.MatchPatternParser;
import edu.kit.iti.formal.psdbg.termmatcher.mp.MatchPath;
import lombok.Getter;
import lombok.RequiredArgsConstructor;
......
package edu.kit.iti.formal.psdbg.termmatcher;
import edu.kit.formal.psdb.termmatcher.MatchPatternParser;
import edu.kit.iti.formal.psdbg.termmatcher.MatchPatternParser;
import org.antlr.v4.runtime.Token;
import org.antlr.v4.runtime.tree.TerminalNode;
......
<?xml version="1.0" encoding="UTF-8"?>
<project xmlns="http://maven.apache.org/POM/4.0.0" xmlns:xsi="http://www.w3.org/2001/XMLSchema-instance"
xsi:schemaLocation="http://maven.apache.org/POM/4.0.0 http://maven.apache.org/xsd/maven-4.0.0.xsd">
<modelVersion>4.0.0</modelVersion>
<groupId>edu.kit.iti.formal.psdbg</groupId>
<artifactId>psdbg</artifactId>
<version>1.0-FM</version>
<packaging>pom</packaging>
<name>ProofScriptParser</name>
<description>
A parser and AST for the proof script language.
</description>
<url>https://git.scc.kit.edu/sarah.grebing/ProofScriptParser</url>
<developers>
<developer>
<name>Sarah Grebing</name>
<email>sarah.grebing@kit.edu</email>
<organization>Karlsruhe Institute of Technology</organization>
</developer>
<developer>
<name>Alexander Weigl</name>
<email>weigl@kit.edu</email>
<organization>Karlsruhe Institute of Technology</organization>
</developer>
</developers>
<scm>
</scm>
<organization>
<name>Application-oriented Formal Verification</name>
<url>https://formal.iti.kit.edu</url>
</organization>
<inceptionYear>2017</inceptionYear>
<licenses>
<license>
<name>gpl_v3</name>
</license>
</licenses>
<properties>
<project.build.sourceEncoding>UTF-8</project.build.sourceEncoding>
<maven.compiler.target>1.8</maven.compiler.target>
<maven.compiler.source>1.8</maven.compiler.source>
<skipTests>true</skipTests>
</properties>
<modules>
<module>lang</module>
<module>rt</module>
<module>rt-key</module>
<module>ui</module>
<module>DockFX</module>
<module>lint</module>
<module>keydeps</module>
<module>matcher</module>
</modules>
<distributionManagement>
<repository>
<id>bwcloud-ssh</id>
<url>scp://141.52.38.245:/var/www/html/psdbg/</url>
</repository>
<snapshotRepository>
<id>bwcloud-ssh</id>
<url>scp://141.52.38.245:/var/www/html/psdbg-devel/</url>
</snapshotRepository>
</distributionManagement>
<build>
<extensions>
<extension>
<groupId>org.apache.maven.wagon</groupId>
<artifactId>wagon-ssh</artifactId>
<version>2.12</version>
</extension>
</extensions>
<pluginManagement>
<plugins>
<plugin>
<groupId>org.apache.maven.plugins</groupId>
<artifactId>maven-checkstyle-plugin</artifactId>
<version>2.17</version>
<dependencies>
<dependency>
<groupId>com.puppycrawl.tools</groupId>
<artifactId>checkstyle</artifactId>
<version>7.6.1</version>
</dependency>
</dependencies>
<configuration>
<configLocation>.checkstyle_rules.xml</configLocation>
</configuration>
</plugin>
</plugins>
</pluginManagement>
<plugins>
<!--
<plugin>
<groupId>org.codehaus.mojo</groupId>
<artifactId>build-helper-maven-plugin</artifactId>
<version>1.7</version>
<executions>
<execution>
<id>released-version</id>
<goals>
<goal>released-version</goal>
</goals>
</execution>
<execution>
<id>add-source</id>
<phase>generate-sources</phase>
<goals>
<goal>add-source</goal>
</goals>
<configuration>
<sources>
<source>lib/DockFX/src/main/java</source>
</sources>
</configuration>
</execution>
<execution>
<id>add-resource</id>
<phase>generate-resources</phase>
<goals>
<goal>add-resource</goal>
</goals>
<configuration>
<resources>
<resource>
<directory>lib/DockFX/src/main/resources</directory>
</resource>
</resources>
</configuration>
</execution>
</executions>
</plugin>
-->
<plugin>
<groupId>org.codehaus.mojo</groupId>
<artifactId>license-maven-plugin</artifactId>
<version>1.12</version>
<configuration>
<licenseName>gpl_v3</licenseName>
<copyrightOwners>
Sarah Grebing, Alexander Weigl
</copyrightOwners>
</configuration>
</plugin>
<plugin>
<artifactId>maven-compiler-plugin</artifactId>
<version>3.6.2</version>
<configuration>
<source>1.8</source>
<target>1.8</target>
<fork>true</fork>
<showWarnings>true</showWarnings>
<useIncrementalCompilation>false</useIncrementalCompilation>
</configuration>
</plugin>
<!--
<plugin>
<artifactId>maven-assembly-plugin</artifactId>
<executions>
<execution>
<id>make-assembly</id>
<phase>package</phase>
<goals>
<goal>single</goal>
</goals>
</execution>
</executions>
<configuration>
<archive>
<manifest>
<mainClass>edu.kit.iti.formal.psdbg.gui.ProofScriptDebugger</mainClass>
</manifest>
</archive>
<descriptorRefs>
<descriptorRef>exe</descriptorRef>
</descriptorRefs>
</configuration>
</plugin>
-->
<plugin>
<groupId>org.apache.maven.plugins</groupId>
<artifactId>maven-javadoc-plugin</artifactId>
<version>2.9</version>
<executions>
<execution>
<id>attach-javadocs</id>
<goals>
<goal>jar</goal>
</goals>
<configuration>
<additionalparam>-Xdoclint:none</additionalparam>
</configuration>
</execution>
</executions>
</plugin>
<plugin>
<groupId>org.apache.maven.plugins</groupId>
<artifactId>maven-site-plugin</artifactId>
<version>3.3</version>
<configuration>
<reportPlugins>
<plugin>
<groupId>org.apache.maven.plugins</groupId>
<artifactId>maven-javadoc-plugin</artifactId>
<configuration>
<additionalparam>-Xdoclint:none</additionalparam>
</configuration>
</plugin>
</reportPlugins>
</configuration>
</plugin>
</plugins>
</build>
<dependencies>
<dependency>
<groupId>junit</groupId>
<artifactId>junit</artifactId>
<version>4.12</version>
<scope>test</scope>
</dependency>
<dependency>
<groupId>org.projectlombok</groupId>
<artifactId>lombok</artifactId>
<version>1.16.16</version>
<scope>provided</scope>
</dependency>
<!-- https://mvnrepository.com/artifact/commons-cli/commons-cli -->
<dependency>
<groupId>commons-cli</groupId>
<artifactId>commons-cli</artifactId>
<version>1.4</version>
</dependency>
<dependency>
<groupId>com.google.guava</groupId>
<artifactId>guava</artifactId>
<version>22.0</version>
</dependency>
<dependency>
<groupId>commons-io</groupId>
<artifactId>commons-io</artifactId>
<version>2.5</version>
</dependency>
<dependency>
<groupId>commons-lang</groupId>
<artifactId>commons-lang</artifactId>
<version>2.6</version>
</dependency>
<dependency>
<groupId>org.apache.logging.log4j</groupId>
<artifactId>log4j-api</artifactId>
<version>2.6</version>
</dependency>
<dependency>
<groupId>org.apache.logging.log4j</groupId>
<artifactId>log4j-core</artifactId>
<version>2.6</version>
</dependency>
</dependencies>
<reporting>
<plugins>
<plugin>
<groupId>org.apache.maven.plugins</groupId>
<artifactId>maven-jxr-plugin</artifactId>
<version>2.5</version>
</plugin>
<plugin>
<groupId>org.apache.maven.plugins</groupId>
<artifactId>maven-checkstyle-plugin</artifactId>
<version>2.17</version>
<reportSets>
<reportSet>
<reports>
<report>checkstyle</report>
</reports>
</reportSet>
</reportSets>
</plugin>
<plugin>
<groupId>org.codehaus.mojo</groupId>
<artifactId>findbugs-maven-plugin</artifactId>
<version>3.0.4</version>
</plugin>
<plugin>
<groupId>org.codehaus.mojo</groupId>
<artifactId>jdepend-maven-plugin</artifactId>
<version>2.0</version>
</plugin>
</plugins>
</reporting>
</project>
\ No newline at end of file
description = ''
dependencies {
compile project(':rt')
compile project(':keydeps')
compile project(':matcher')
}
<?xml version="1.0" encoding="UTF-8"?>
<project xmlns="http://maven.apache.org/POM/4.0.0" xmlns:xsi="http://www.w3.org/2001/XMLSchema-instance" xsi:schemaLocation="http://maven.apache.org/POM/4.0.0 http://maven.apache.org/xsd/maven-4.0.0.xsd">
<modelVersion>4.0.0</modelVersion>
<parent>
<groupId>edu.kit.iti.formal.psdbg</groupId>
<artifactId>psdbg</artifactId>
<version>1.0-FM</version>
<relativePath>..</relativePath>
</parent>
<artifactId>rt-key</artifactId>
<packaging>jar</packaging>
<dependencies>
<dependency>
<groupId>edu.kit.iti.formal.psdbg</groupId>
<artifactId>rt</artifactId>
<version>1.0-FM</version>
</dependency>
<dependency>
<groupId>edu.kit.iti.formal.psdbg</groupId>
<artifactId>keydeps</artifactId>
<version>1.0</version>
</dependency>
<dependency>
<groupId>edu.kit.iti.formal.psdbg</groupId>
<artifactId>matcher</artifactId>
<version>1.0-FM</version>
</dependency>
</dependencies>
</project>
......@@ -56,9 +56,7 @@ public class Execute {
//pa.getProof().getProofIndependentSettings().getGeneralSettings().setOneStepSimplification(false);
Interpreter<KeyData> inter = interpreterBuilder.build();
KeyData keyData = new KeyData(root.getProofNode(), pa.getEnv(), pa.getProof());
inter.newState(new GoalNode<>(null, keyData, keyData.isClosedNode()));
Interpreter<KeyData> inter = interpreterBuilder.startState().build();
inter.interpret(ast.get(0));
return inter;
} catch (ProblemLoaderException | IOException e) {
......
......@@ -111,14 +111,11 @@ public class KeYMatcher implements MatcherApi<KeyData> {
List<VariableAssignment> assignments = new ArrayList<>();
resultsFromLabelMatch = new ArrayList<>();
//compile pattern
String cleanLabel = label.replaceAll(" ", "");
String cleanLabel2 = cleanLabel.replaceAll("\\(", "\\\\(");
cleanLabel = cleanLabel2.replaceAll("\\)", "\\\\)");
String cleanLabel = cleanLabel(label);
String branchLabel = currentState.getData().getBranchingLabel();
String cleanBranchLabel = branchLabel.replaceAll(" ", "");
String cleanBranchLabel = branchLabel.replaceAll(" ", "");
Pattern regexpForLabel = Pattern.compile(cleanLabel);
Matcher branchLabelMatcher = regexpForLabel.matcher(cleanBranchLabel);
......@@ -216,6 +213,16 @@ public class KeYMatcher implements MatcherApi<KeyData> {
);
}
private String cleanLabel(String label) {
String cleaned = label.replaceAll(" ", "");
cleaned = cleaned.replaceAll("\\(", "\\\\(");
cleaned = cleaned.replaceAll("\\)", "\\\\)");
cleaned = cleaned.replaceAll("\\[", "\\\\[");
cleaned = cleaned.replaceAll("\\]", "\\\\]");
return cleaned;
}
//private TermLiteral from(SequentFormula sf) {
// return new TermLiteral(sf.toString());
......
......@@ -89,4 +89,13 @@ public class ExecuteTest {
}
@Test
public void testInstantiate() throws IOException, ParseException, ParserException {
Execute exec = create("/home/sarah/Documents/KIT_Mitarbeiter/ProofScriptingLanguage/bigIntProof/compareMagnitude_openCases.key.proof",
"-s", "/home/sarah/Documents/KIT_Mitarbeiter/ProofScriptingLanguage/bigIntProof/instAll.kps");
Interpreter<KeyData> i = exec.run();
State<KeyData> currentState = i.getCurrentState();
System.out.println(currentState);
}
}
\ No newline at end of file
description = ''
dependencies {
compile project(':lang')
}
<?xml version="1.0" encoding="UTF-8"?>
<project xmlns="http://maven.apache.org/POM/4.0.0" xmlns:xsi="http://www.w3.org/2001/XMLSchema-instance" xsi:schemaLocation="http://maven.apache.org/POM/4.0.0 http://maven.apache.org/xsd/maven-4.0.0.xsd">
<modelVersion>4.0.0</modelVersion>
<parent>
<groupId>edu.kit.iti.formal.psdbg</groupId>
<artifactId>psdbg</artifactId>
<version>1.0-FM</version>
<relativePath>..</relativePath>
</parent>
<artifactId>rt</artifactId>
<packaging>jar</packaging>
<dependencies>
<dependency>
<groupId>edu.kit.iti.formal.psdbg</groupId>
<artifactId>lang</artifactId>
<version>1.0-FM</version>
</dependency>
</dependencies>
</project>
rootProject.name = 'psdbg'
include ':lang'
include ':rt'
include ':rt-key'
include ':ui'
include ':DockFX'
include ':lint'
include ':keydeps'
include ':matcher'
project(':lang').projectDir = "$rootDir/lang" as File
project(':rt').projectDir = "$rootDir/rt" as File
project(':rt-key').projectDir = "$rootDir/rt-key" as File
project(':ui').projectDir = "$rootDir/ui" as File
project(':DockFX').projectDir = "$rootDir/DockFX" as File
project(':lint').projectDir = "$rootDir/lint" as File
project(':keydeps').projectDir = "$rootDir/keydeps" as File
project(':matcher').projectDir = "$rootDir/matcher" as File
\ No newline at end of file
plugins {
id "com.github.voplex95.lesscompiler" version "1.0.3"
}
apply plugin: 'antlr'
description = 'ui'
generateGrammarSource {
arguments += ["-long-messages", "-package","antlrgrammars"]
}
lessCompile {
source = file('src/main/resources/edu/kit/iti/formal/psdbg/gui/debugger-ui.less')
target = file('build/resources/main/edu/kit/iti/formal/psdbg/gui/')
//compress = true
}
processResources.dependsOn lessCompile
dependencies {
compile group: 'de.jensd', name: 'fontawesomefx-materialdesignfont', version: '1.7.22-4'
compile group: 'de.jensd', name: 'fontawesomefx-commons', version: '8.15'
compile group: 'org.fxmisc.richtext', name: 'richtextfx', version: '1.0.0-SNAPSHOT'
compile group: 'org.controlsfx', name: 'controlsfx', version: '8.40.12'
compile group: 'org.antlr', name: 'antlr4', version: '4.7'
antlr group: 'org.antlr', name: 'antlr4', version: '4.7'
compile project(':rt-key')
compile project(':matcher')
compile project(':DockFX')
compile project(':lint')
}
def mainClassName = 'edu.kit.iti.formal.psdbg.gui.ProofScriptDebugger'
task runApp(type: JavaExec) {
classpath = sourceSets.main.runtimeClasspath
main = mainClassName
}
task distJar(type: Jar) {
manifest {
attributes 'Main-Class': mainClassName
}
classifier="exe"
from { configurations.compile.collect { it.isDirectory() ? it : zipTree(it) } }
with jar
}
distJar.dependsOn jar
\ No newline at end of file
......@@ -53,6 +53,17 @@ public class Events {
private final Goal currentGoal;
}
@Data
@RequiredArgsConstructor
public static class CommandApplicationEvent {
private final String commandName;
private final PosInOccurrence pio;
private final Goal currentGoal;
}
@Data
......
......@@ -161,8 +161,8 @@ public class InteractiveModeController {
SequentFormula seqForm = tap.getPio().sequentFormula();
//transform term to parsable string representation
Sequent seq = g.sequent();
String sfTerm = LogicPrinter.quickPrintTerm(seqForm.formula(), keYServices, false, false);
String onTerm = LogicPrinter.quickPrintTerm(tap.getPio().subTerm(), keYServices, false, false);
String sfTerm = Utils.printParsableTerm(seqForm.formula(), keYServices);
String onTerm = Utils.printParsableTerm(tap.getPio().subTerm(), keYServices);
RuleCommand.Parameters params = new RuleCommand.Parameters();
......
......@@ -2,12 +2,11 @@ package edu.kit.iti.formal.psdbg.gui.controls;
import de.uka.ilkd.key.control.ProofControl;
import de.uka.ilkd.key.gui.nodeviews.TacletMenu.TacletAppComparator;
import de.uka.ilkd.key.java.Services;
import de.uka.ilkd.key.logic.Name;
import de.uka.ilkd.key.logic.PosInOccurrence;
import de.uka.ilkd.key.logic.Term;
import de.uka.ilkd.key.pp.AbbrevMap;
import de.uka.ilkd.key.pp.NotationInfo;
import de.uka.ilkd.key.pp.PosInSequent;
import de.uka.ilkd.key.pp.*;
import de.uka.ilkd.key.proof.Goal;
import de.uka.ilkd.key.rule.*;
import edu.kit.iti.formal.psdbg.gui.controller.DebuggerMain;
......@@ -26,6 +25,7 @@ import javafx.scene.text.Text;
import org.key_project.util.collection.ImmutableList;
import org.key_project.util.collection.ImmutableSLList;
import java.io.IOException;
import java.util.*;
import java.util.stream.Collectors;
......@@ -127,6 +127,11 @@ public class TacletContextMenu extends ContextMenu {
createDummyMenuItem();
}
// copyToClipboard = new MenuItem("Copy To Clipboad");
// copyToClipboard.setOnAction(event -> handleCopyToClipboard(goal, pos, event));
// rootMenu.getItems().add(copyToClipboard);
//proofMacroMenuController.initViewController(getMainApp(), getContext());
//proofMacroMenuController.init(occ);
}
......@@ -194,17 +199,20 @@ public class TacletContextMenu extends ContextMenu {
//compare by name
Comparator.comparing(o -> o.taclet().name())