Skip to content

P
ProofScriptParser
Commit 6bc9bfa1 authored by Alexander Weigl's avatar Alexander Weigl
Browse files
Options

try to fix deps

parent 095d41f0
Expand all Hide whitespace changes
Inline Side-by-side
Showing with 967 additions and 23897 deletions
keydeps/README
View file @ 6bc9bfa1
# Execute this in this folder.
# Set to key/key/deployment/components/
COMPONENTS=lib/components/
COMPONENTS=~/work/key/key/deployment/components/
mvn install:install-file -Dfile=$COMPONENTS/key.core.jar \
-DgroupId=key-project-psdbg \
-DartifactId=key.core \
-Dversion=2.7 \
-Dversion=2.7-SNAPSHOT \
-Dpackaging=jar \
-DlocalRepositoryPath=local-repo
......@@ -15,7 +15,7 @@ mvn install:install-file -Dfile=$COMPONENTS/key.core.jar \
mvn install:install-file -Dfile=$COMPONENTS/key.ui.jar \
-DgroupId=key-project-psdbg \
-DartifactId=key.ui \
-Dversion=2.7 \
-Dversion=2.7-SNAPSHOT \
-Dpackaging=jar \
-DlocalRepositoryPath=local-repo
......@@ -23,7 +23,7 @@ mvn install:install-file -Dfile=$COMPONENTS/key.ui.jar \
mvn install:install-file -Dfile=$COMPONENTS/key.util.jar \
-DgroupId=key-project-psdbg \
-DartifactId=key.util \
-Dversion=2.7 \
-Dversion=2.7-SNAPSHOT \
-Dpackaging=jar \
-DlocalRepositoryPath=local-repo
......@@ -31,6 +31,6 @@ mvn install:install-file -Dfile=$COMPONENTS/key.util.jar \
mvn install:install-file -Dfile=$COMPONENTS/../libs/recoderKey.jar\
-DgroupId=key-project-psdbg \
-DartifactId=recoder \
-Dversion=2.7 \
-Dversion=2.7\
-Dpackaging=jar \
-DlocalRepositoryPath=local-repo
\ No newline at end of file
-DlocalRepositoryPath=local-repo
keydeps/README.user 0 → 100644
View file @ 6bc9bfa1
# Execute this in this folder.
# Set to key/key/deployment/components/
COMPONENTS=~/work/key/key/deployment/components/
mvn install:install-file -Dfile=$COMPONENTS/key.core.jar \
-DgroupId=key-project-psdbg \
-DartifactId=key.core \
-Dversion=2.7-SNAPSHOT \
-Dpackaging=jar \
mvn install:install-file -Dfile=$COMPONENTS/key.ui.jar \
-DgroupId=key-project-psdbg \
-DartifactId=key.ui \
-Dversion=2.7-SNAPSHOT \
-Dpackaging=jar \
mvn install:install-file -Dfile=$COMPONENTS/key.util.jar \
-DgroupId=key-project-psdbg \
-DartifactId=key.util \
-Dversion=2.7-SNAPSHOT \
-Dpackaging=jar \
mvn install:install-file -Dfile=$COMPONENTS/../libs/recoderKey.jar\
-DgroupId=key-project-psdbg \
-DartifactId=recoder \
-Dversion=2.7\
-Dpackaging=jar \
keydeps/local-repo/key-project-psdbg/key.core/2.7/key.core-2.7.pom → keydeps/local-repo/key-project-psdbg/key.core/2.7-SNAPSHOT/key.core-2.7-SNAPSHOT.pom
View file @ 6bc9bfa1
......@@ -4,6 +4,6 @@
<modelVersion>4.0.0</modelVersion>
<groupId>key-project-psdbg</groupId>
<artifactId>key.core</artifactId>
<version>2.7</version>
<version>2.7-SNAPSHOT</version>
<description>POM was created from install:install-file</description>
</project>
keydeps/local-repo/key-project-psdbg/key.core/2.7-SNAPSHOT/maven-metadata-local.xml 0 → 100644
View file @ 6bc9bfa1
<?xml version="1.0" encoding="UTF-8"?>
<metadata modelVersion="1.1.0">
<groupId>key-project-psdbg</groupId>
<artifactId>key.core</artifactId>
<version>2.7-SNAPSHOT</version>
<versioning>
<snapshot>
<localCopy>true</localCopy>
</snapshot>
<lastUpdated>20170911152346</lastUpdated>
<snapshotVersions>
<snapshotVersion>
<extension>jar</extension>
<value>2.7-SNAPSHOT</value>
<updated>20170911152346</updated>
</snapshotVersion>
<snapshotVersion>
<extension>pom</extension>
<value>2.7-SNAPSHOT</value>
<updated>20170911152346</updated>
</snapshotVersion>
</snapshotVersions>
</versioning>
</metadata>
keydeps/local-repo/key-project-psdbg/key.core/maven-metadata-local.xml
View file @ 6bc9bfa1
......@@ -3,10 +3,9 @@
<groupId>key-project-psdbg</groupId>
<artifactId>key.core</artifactId>
<versioning>
<release>2.7</release>
<versions>
<version>2.7</version>
<version>2.7-SNAPSHOT</version>
</versions>
<lastUpdated>20170828163803</lastUpdated>
<lastUpdated>20170911152346</lastUpdated>
</versioning>
</metadata>
keydeps/local-repo/key-project-psdbg/key.ui/2.7/key.ui-2.7.pom → keydeps/local-repo/key-project-psdbg/key.ui/2.7-SNAPSHOT/key.ui-2.7-SNAPSHOT.pom
View file @ 6bc9bfa1
......@@ -4,6 +4,6 @@
<modelVersion>4.0.0</modelVersion>
<groupId>key-project-psdbg</groupId>
<artifactId>key.ui</artifactId>
<version>2.7</version>
<version>2.7-SNAPSHOT</version>
<description>POM was created from install:install-file</description>
</project>
keydeps/local-repo/key-project-psdbg/key.ui/2.7-SNAPSHOT/maven-metadata-local.xml 0 → 100644
View file @ 6bc9bfa1
<?xml version="1.0" encoding="UTF-8"?>
<metadata modelVersion="1.1.0">
<groupId>key-project-psdbg</groupId>
<artifactId>key.ui</artifactId>
<version>2.7-SNAPSHOT</version>
<versioning>
<snapshot>
<localCopy>true</localCopy>
</snapshot>
<lastUpdated>20170911152349</lastUpdated>
<snapshotVersions>
<snapshotVersion>
<extension>jar</extension>
<value>2.7-SNAPSHOT</value>
<updated>20170911152349</updated>
</snapshotVersion>
<snapshotVersion>
<extension>pom</extension>
<value>2.7-SNAPSHOT</value>
<updated>20170911152349</updated>
</snapshotVersion>
</snapshotVersions>
</versioning>
</metadata>
keydeps/local-repo/key-project-psdbg/key.ui/maven-metadata-local.xml
View file @ 6bc9bfa1
......@@ -3,10 +3,9 @@
<groupId>key-project-psdbg</groupId>
<artifactId>key.ui</artifactId>
<versioning>
<release>2.7</release>
<versions>
<version>2.7</version>
<version>2.7-SNAPSHOT</version>
</versions>
<lastUpdated>20170828163805</lastUpdated>
<lastUpdated>20170911152349</lastUpdated>
</versioning>
</metadata>
keydeps/local-repo/key-project-psdbg/key.util/2.7/key.util-2.7.pom → keydeps/local-repo/key-project-psdbg/key.util/2.7-SNAPSHOT/key.util-2.7-SNAPSHOT.pom
View file @ 6bc9bfa1
......@@ -4,6 +4,6 @@
<modelVersion>4.0.0</modelVersion>
<groupId>key-project-psdbg</groupId>
<artifactId>key.util</artifactId>
<version>2.7</version>
<version>2.7-SNAPSHOT</version>
<description>POM was created from install:install-file</description>
</project>
keydeps/local-repo/key-project-psdbg/key.util/2.7-SNAPSHOT/maven-metadata-local.xml 0 → 100644
View file @ 6bc9bfa1
<?xml version="1.0" encoding="UTF-8"?>
<metadata modelVersion="1.1.0">
<groupId>key-project-psdbg</groupId>
<artifactId>key.util</artifactId>
<version>2.7-SNAPSHOT</version>
<versioning>
<snapshot>
<localCopy>true</localCopy>
</snapshot>
<lastUpdated>20170911152351</lastUpdated>
<snapshotVersions>
<snapshotVersion>
<extension>jar</extension>
<value>2.7-SNAPSHOT</value>
<updated>20170911152351</updated>
</snapshotVersion>
<snapshotVersion>
<extension>pom</extension>
<value>2.7-SNAPSHOT</value>
<updated>20170911152351</updated>
</snapshotVersion>
</snapshotVersions>
</versioning>
</metadata>
keydeps/local-repo/key-project-psdbg/key.util/maven-metadata-local.xml
View file @ 6bc9bfa1
......@@ -3,10 +3,9 @@
<groupId>key-project-psdbg</groupId>
<artifactId>key.util</artifactId>
<versioning>
<release>2.7</release>
<versions>
<version>2.7</version>
<version>2.7-SNAPSHOT</version>
</versions>
<lastUpdated>20170828163808</lastUpdated>
<lastUpdated>20170911152351</lastUpdated>
</versioning>
</metadata>
keydeps/local-repo/key-project-psdbg/recoder/maven-metadata-local.xml
View file @ 6bc9bfa1
......@@ -7,6 +7,6 @@
<versions>
<version>2.7</version>
</versions>
<lastUpdated>20170828163810</lastUpdated>
<lastUpdated>20170911152354</lastUpdated>
</versioning>
</metadata>
keydeps/pom.xml
View file @ 6bc9bfa1
......@@ -18,6 +18,11 @@
<id>local-repo</id>
<name>local-repo</name>
<url>file:///${basedir}/local-repo</url>
<snapshots>
<enabled>true</enabled>
<updatePolicy>always</updatePolicy>
<checksumPolicy>ignore</checksumPolicy>
</snapshots>
</repository>
</repositories>
......@@ -25,17 +30,17 @@
<dependency>
<groupId>key-project-psdbg</groupId>
<artifactId>key.core</artifactId>
<version>2.7</version>
<version>2.7-SNAPSHOT</version>
</dependency>
<dependency>
<groupId>key-project-psdbg</groupId>
<artifactId>key.ui</artifactId>
<version>2.7</version>
<version>2.7-SNAPSHOT</version>
</dependency>
<dependency>
<groupId>key-project-psdbg</groupId>
<artifactId>key.util</artifactId>
<version>2.7</version>
<version>2.7-SNAPSHOT</version>
</dependency>
<dependency>
<groupId>org.antlr</groupId>
......@@ -59,4 +64,34 @@
</dependency>
</dependencies>
<build>
<plugins>
<plugin>
<groupId>org.codehaus.mojo</groupId>
<artifactId>exec-maven-plugin</artifactId>
<version>1.2.1</version>
<executions>
<execution>
<phase>test</phase>
<goals>
<goal>java</goal>
</goals>
</execution>
</executions>
<configuration>
<workingDirectory>${basedir}/../</workingDirectory>
<!-- <arguments>
<systemProperties>
<systemProperty>
<key>java.security.policy</key>
<value>policy</value>
</systemProperty>
</systemProperties>
</arguments>-->
<mainClass>GenDoc</mainClass>
</configuration>
</plugin>
</plugins>
</build>
</project>
keydeps/src/main/java/GenDoc.java 0 → 100644
View file @ 6bc9bfa1
import de.uka.ilkd.key.api.KeYApi;
import de.uka.ilkd.key.control.KeYEnvironment;
import de.uka.ilkd.key.macros.ProofMacro;
import de.uka.ilkd.key.macros.scripts.ProofScriptCommand;
import de.uka.ilkd.key.macros.scripts.meta.ProofScriptArgument;
import de.uka.ilkd.key.proof.io.ProblemLoaderException;
import de.uka.ilkd.key.rule.Taclet;
import org.key_project.util.collection.ImmutableList;
import java.io.File;
import java.io.FileOutputStream;
import java.io.FileWriter;
import java.io.IOException;
import java.util.*;
import java.util.stream.Collectors;
/**
* @author Alexander Weigl
* @version 1 (11.09.17)
*/
public class GenDoc {
private static File basedir = new File("..");
private static File propertiesFile = new File(basedir, "rt-key/src/main/resources/edu/kit/iti/formal/psdbg/taclets.properties.xml");
private static File dummyFile = new File(basedir, "rt-key/src/test/resources/edu/kit/iti/formal/psdbg/interpreter/contraposition/contraposition.key");
private static File websiteDoc = new File(basedir, "website/docs/");
private static List<Taclet> getTaclets() throws ProblemLoaderException {
System.out.println("Use dummy file: " + dummyFile.getAbsolutePath());
KeYEnvironment env = KeYApi.loadFromKeyFile(dummyFile).getLoadedProof().getEnv();
ImmutableList<Taclet> a = env.getInitConfig().getTaclets();
return a.stream().collect(Collectors.toList());
}
private static void writeProperties(File file, List<Taclet> taclets) {
Properties documentation = new Properties();
for (Taclet taclet : taclets) {
System.out.println((taclet.displayName()));
documentation.put(taclet.displayName(), taclet.toString());
}
// write properties file!
propertiesFile.getParentFile().mkdirs();
try (FileOutputStream stream = new FileOutputStream(file)) {
documentation.storeToXML(stream,
String.format("Generated on: %s. Use gen", new Date()),
"utf-8");
stream.close();
} catch (IOException e) {
e.printStackTrace();
}
}
private static void writeTacletDocumentation(File file, List<Taclet> taclets) {
file.getParentFile().mkdirs();
try (FileWriter stream = new FileWriter(file)) {
stream.write("# Taclets\n\n");
stream.write(String.format("Generated on: %s", new Date()) +
"\n\nCovering the *default* taclets of [KeY](http://key-project.org).");
for (Taclet t : taclets) {
stream.write("\n\n## ${t.displayName()}\n\n");
stream.write("```\n" + t.toString() + "\n```");
}
stream.close();
} catch (IOException e) {
e.printStackTrace();
}
}
private static void writeMacros(File file) {
List<ProofMacro> macros = new ArrayList<>(KeYApi.getMacroApi().getMacros());
file.getParentFile().mkdirs();
try (FileWriter stream = new FileWriter(file)) {
stream.write("# Macros\n\n" +
"Generated on: ${new Date()} by `gendoc.groovy`.\n\n"
+ "Covering the macros of [KeY](http://key-project.org).");
macros.sort(Comparator.comparing(ProofMacro::getScriptCommandName));
for (ProofMacro t : macros) {
stream.write(String.format("\n\n## %s (`%s`) \n\n",
t.getName(), t.getScriptCommandName()));
stream.write(t.getCategory() + "\n\n");
stream.write(t.getDescription() + "\n\n");
}
stream.close();
} catch (IOException e) {
e.printStackTrace();
}
}
private static String helpForCommand(ProofScriptCommand<?> c) {
StringBuilder html = new StringBuilder();
html.append("## " + c.getName());
html.append("\n> Synopsis: `" + c.getName());
for (ProofScriptArgument a : c.getArguments()) {
html.append(' ');
if (a.isFlag()) {
html.append("[").append(a.getName()).append("]");
} else {
if (!a.isRequired())
html.append("[");
if (a.getName().startsWith("#"))
html.append("<" + a.getType().getSimpleName().toUpperCase() + ">");
else
html.append(a.getName() + "=<" + a.getType().getSimpleName().toUpperCase() + ">");
if (!a.isRequired())
html.append("]");
}
}
html.append("`\n\n");
html.append(c.getDocumentation().replaceAll("\n[ \t]*", "\n"));
html.append("\n\n**Arguments:**\n");
for (ProofScriptArgument<?> a : c.getArguments()) {
html.append(
String.format("\n* `%s` : *%s* ",
a.getName(), a.getType().getSimpleName().toUpperCase()));
if (a.isRequired()) {
html.append("(*R*)");
}
html.append(a.getDocumentation());
}
return html.toString();
}
private static void writeCommand(File file) {
List<ProofScriptCommand> commands = new ArrayList<>(KeYApi.getScriptCommandApi().getScriptCommands());
file.getParentFile().mkdirs();
try (FileWriter stream = new FileWriter(file)) {
stream.write("# Commands\n\n");
stream.write("\n\nGenerated on: " + new Date() + "by `gendoc.groovy`.");
stream.write("\n\nCovering the proof script commands of [KeY](http://key-project.org).\n\n");
commands.sort(Comparator.comparing(ProofScriptCommand::getName));
for (ProofScriptCommand t : commands) {
stream.write(helpForCommand(t) + "\n\n");
}
stream.close();
} catch (IOException e) {
e.printStackTrace();
}
}
public static void main(String[] args) throws ProblemLoaderException {
List<Taclet> taclets = getTaclets();
taclets.sort(Comparator.comparing(Taclet::name));
writeProperties(propertiesFile, taclets);
writeTacletDocumentation(new File(websiteDoc, "taclets.md"), taclets);
writeMacros(new File(websiteDoc, "macros.md"));
writeCommand(new File(websiteDoc, "commands.md"));
}
}
scripts/gendoc.groovy deleted 100644 → 0
View file @ 095d41f0
import de.uka.ilkd.key.macros.scripts.meta.ProofScriptArgument
import de.uka.ilkd.key.api.KeYApi
import de.uka.ilkd.key.macros.ProofMacro
import de.uka.ilkd.key.control.KeYEnvironment
import de.uka.ilkd.key.macros.scripts.ProofScriptCommand
import de.uka.ilkd.key.rule.Taclet
import org.key_project.util.collection.ImmutableList
propertiesFile = new File("rt-key/src/main/resources/edu/kit/iti/formal/psdbg/taclets.properties.xml")
dummyFile = new File("rt-key/src/test/resources/edu/kit/iti/formal/psdbg/interpreter/contraposition/contraposition.key")
websiteDoc = new File("website/doc/")
ImmutableList<Taclet> getTaclets() {
println("Use dummy file: ${dummyFile}")
KeYEnvironment env = KeYApi.loadFromKeyFile(dummyFile).getLoadedProof().getEnv()
return env.initConfig.taclets
}
def writeProperties(File file, List<Taclet> taclets) {
documentation = new Properties()
for (Taclet taclet in taclets) {
println(taclet.displayName())
documentation.put(taclet.displayName(), taclet.toString())
}
// write properties file!
propertiesFile.getParentFile().mkdirs()
stream = new FileOutputStream(file)
documentation.storeToXML(stream,
"Generated on: ${new Date()}. Use extractDocumentation.groovy".toString(),
"utf-8")
stream.close()
}
def writeTacletDocumentation(File file, taclets) {
file.parentFile.mkdirs()
stream = new FileWriter(file)
stream.write("""
# Taclets
Generated on: ${new Date()} by `gendoc.groovy`.
Covering the *default* taclets of [KeY](http://key-project.org).""")
for (t in taclets) {
stream.write("\n\n## ${t.displayName()}\n\n")
stream.write("```\n" + t.toString() + "\n```")
}
stream.close()
}
def writeMacros(File file) {
macros = de.uka.ilkd.key.api.KeYApi.getMacroApi().getMacros()
file.parentFile.mkdirs()
stream = new FileWriter(file)
stream.write("""
# Macros
Generated on: ${new Date()} by `gendoc.groovy`.
Covering the macros of [KeY](http://key-project.org).""")
macros.sort()
for (t in macros) {
stream.write("\n\n## ${t.name} (`${t.scriptCommandName}`) \n\n")
stream.write("${t.category}\n\n")
stream.write("${t.description}\n\n")
}
stream.close()
}
def helpForCommand(ProofScriptCommand c) {
html = new StringBuilder()
html.append("""
# ${c.getName()}
> Synopsis: `c.getName())""")
for (a in c.getArguments()) {
html.append(' ')
if (a.isFlag()) {
html.append("[").append(a.getName()).append("]")
} else {
if (!a.isRequired())
html.append("[")
if (a.getName().startsWith("#"))
html.append("<${a.getType().getSimpleName().toUpperCase()}>")
else
html.append("${a.name}=<${a.getType().getSimpleName().toUpperCase()}>")
if (!a.isRequired())
html.append("]")
}
}
html.append("`\n\n")
html.append("**Arguments:**\n")
for (a in c.getArguments()) {
html.append("\n* `${a.getName()}` : *${a.getType().getSimpleName().toUpperCase()}* ")
if (a.isRequired()) {
html.append("(*R*)")
}
}
return html.toString()
}
def writeCommand(File file) {
commands = de.uka.ilkd.key.api.KeYApi.getScriptCommandApi().getScriptCommands()
file.parentFile.mkdirs()
stream = new FileWriter(file)
stream.write("""
# Commands
Generated on: ${new Date()} by `gendoc.groovy`.
Covering the macros of [KeY](http://key-project.org).""")
commands.sort()
for (t in commands) {
stream.write(helpForCommand(t) + "\n\n")
}
stream.close()
}
taclets = getTaclets().asList()
Collections.sort(taclets, new Comparator<Taclet>() {
@Override
int compare(Taclet o1, Taclet o2) {
return o1.displayName().compareTo(o2.displayName())
}
})
writeProperties(propertiesFile, taclets)
writeTacletDocumentation(new File(websiteDoc, "taclets.md"), taclets)
writeMacros(new File(websiteDoc, "macros.md"))
writeCommand(new File(websiteDoc, "commands.md"))
\ No newline at end of file
website/doc/commands.md deleted 100644 → 0
View file @ 095d41f0
# Commands
Generated on: Sat Sep 09 23:02:01 CEST 2017 by `gendoc.groovy`.
Covering the macros of [KeY](http://key-project.org).
# macro
> Synopsis: `c.getName()) <STRING>`
**Arguments:**
* `#2` : *STRING* (*R*)
# auto
> Synopsis: `c.getName()) [all=<BOOLEAN>] [steps=<INT>]`
**Arguments:**
* `all` : *BOOLEAN*
* `steps` : *INT*
# cut
> Synopsis: `c.getName()) <TERM>`
**Arguments:**
* `#2` : *TERM* (*R*)
# set
> Synopsis: `c.getName()) [oss=<BOOLEAN>]`
**Arguments:**
* `oss` : *BOOLEAN*
# select
> Synopsis: `c.getName()) formula=<TERM>`
**Arguments:**
* `formula` : *TERM* (*R*)
# schemaVar
> Synopsis: `c.getName()) <STRING> <STRING>`
**Arguments:**
* `#2` : *STRING* (*R*)
* `#3` : *STRING* (*R*)
# focus
> Synopsis: `c.getName()) <SEQUENT>`
**Arguments:**
* `#2` : *SEQUENT* (*R*)
# rule
> Synopsis: `c.getName()) <STRING> [on=<TERM>] [formula=<TERM>] [occ=<INT>]`
**Arguments:**
* `#2` : *STRING* (*R*)
* `on` : *TERM*
* `formula` : *TERM*
* `occ` : *INT*
# skip
> Synopsis: `c.getName())`
**Arguments:**
# instantiate
> Synopsis: `c.getName()) formula=<TERM> var=<STRING> occ=<INT> with=<TERM>`
**Arguments:**
* `formula` : *TERM* (*R*)
* `var` : *STRING* (*R*)
* `occ` : *INT* (*R*)