script for documentation generation

scripts/gendoc.groovy

+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

+
+# 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*)
+* `with` :  *TERM* (*R*)
+
+
+# script
+
+> Synopsis: `c.getName()) <STRING>`
+
+**Arguments:**
+
+* `#2` :  *STRING* (*R*)
+
+
+# javascript
+
+> Synopsis: `c.getName()) <STRING>`
+
+**Arguments:**
+
+* `#2` :  *STRING* (*R*)
+
+
+# exit
+
+> Synopsis: `c.getName())`
+
+**Arguments:**
+
+
+
+# tryclose
+
+> Synopsis: `c.getName()) steps=<INTEGER> <STRING>`
+
+**Arguments:**
+
+* `steps` :  *INTEGER* (*R*)
+* `#2` :  *STRING* (*R*)
+
+
+# leave
+
+> Synopsis: `c.getName())`
+
+**Arguments:**
+
+
+
+# let
+
+> Synopsis: `c.getName())`
+
+**Arguments:**
+
+
+
+# smt
+
+> Synopsis: `c.getName()) solver=<STRING>`
+
+**Arguments:**
+
+* `solver` :  *STRING* (*R*)
+
+
+# assume
+
+> Synopsis: `c.getName()) <TERM>`
+
+**Arguments:**
+
+* `#2` :  *TERM* (*R*)
+

website/doc/macros.md

+
+# Macros
+    
+Generated on: Sat Sep 09 23:02:00 CEST 2017 by `gendoc.groovy`. 
+
+Covering the macros of [KeY](http://key-project.org).
+
+## Full Information Flow Auto Pilot (`infflow-autopilot`) 
+
+Information Flow
+
+<html><ol><li>Search exhaustively for applicable position, then<li>Start auxiliary computation<li>Finish symbolic execution<li>Try to close as many goals as possible<li>Apply macro recursively<li>Finish auxiliary computation<li>Use information flow contracts<li>Try to close as many goals as possible</ol>
+
+
+
+## Close provable goals below (`tryclose`) 
+
+null
+
+Closes closable goals, leave rest untouched (see settings AutoPrune). Applies only to goals beneath the selected node.
+
+
+
+## Update Simplification Only (`simp-upd`) 
+
+Simplification
+
+Applies only update simplification rules
+
+
+
+## Full Auto Pilot (`autopilot`) 
+
+Auto Pilot
+
+<html><ol><li>Finish symbolic execution<li>Separate proof obligations<li>Expand invariant definitions<li>Try to close all proof obligations</ol>
+
+
+
+## Finish symbolic execution (`symbex`) 
+
+Auto Pilot
+
+Continue automatic strategy application until no more modality is on the sequent.
+
+
+
+## Propositional expansion (w/ splits) (`split-prop`) 
+
+Propositional
+
+Apply rules to decompose propositional toplevel formulas; splits the goal if necessary
+
+
+
+## Heap Simplification (`simp-heap`) 
+
+Simplification
+
+This macro performs simplification of Heap and LocSet terms.
+It applies simplification rules (including the "unoptimized" select rules), One Step Simplification, alpha, and delta rules.
+
+
+
+## Auto pilot (preparation only) (`autopilot-prep`) 
+
+Auto Pilot
+
+<html><ol><li>Finish symbolic execution<li>Separate proof obligations<li>Expand invariant definitions</ol>
+
+
+
+## Propositional expansion (w/o splits) (`nosplit-prop`) 
+
+Propositional
+
+Apply rules to decompose propositional toplevel formulas; does not split the goal.
+
+
+
+## One Single Proof Step (`onestep`) 
+
+Simplification
+
+One single proof step is applied
+