From a23f9fc63e5d01274a9d43e3f4e0a2d39a320571 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Andreas=20Sch=C3=A4rtl?= <andreas@schaertl.me>
Date: Fri, 2 Oct 2020 13:33:43 +0200
Subject: [PATCH] app: infer isabelle afp url from ulo:sourceref
---
src/ulo-storage-applications/pom.xml | 8 ++
.../java/info/mathhub/uloapi/html/AFP.java | 131 ++++++++++++++++++
.../java/info/mathhub/uloapi/html/Routes.java | 2 +
.../template/freemarker/explore_node.flt | 5 +
4 files changed, 146 insertions(+)
create mode 100644 src/ulo-storage-applications/src/main/java/info/mathhub/uloapi/html/AFP.java
diff --git a/src/ulo-storage-applications/pom.xml b/src/ulo-storage-applications/pom.xml
index e7cb484..489b550 100644
--- a/src/ulo-storage-applications/pom.xml
+++ b/src/ulo-storage-applications/pom.xml
@@ -44,6 +44,14 @@
<mainClass>info.mathhub.uloapi.html.Main</mainClass>
</configuration>
</plugin>
+ <plugin>
+ <groupId>org.apache.maven.plugins</groupId>
+ <artifactId>maven-compiler-plugin</artifactId>
+ <configuration>
+ <source>11</source>
+ <target>11</target>
+ </configuration>
+ </plugin>
</plugins>
</build>
diff --git a/src/ulo-storage-applications/src/main/java/info/mathhub/uloapi/html/AFP.java b/src/ulo-storage-applications/src/main/java/info/mathhub/uloapi/html/AFP.java
new file mode 100644
index 0000000..09e20ee
--- /dev/null
+++ b/src/ulo-storage-applications/src/main/java/info/mathhub/uloapi/html/AFP.java
@@ -0,0 +1,131 @@
+package info.mathhub.uloapi.html;
+
+import org.slf4j.Logger;
+import org.slf4j.LoggerFactory;
+
+import java.net.URI;
+import java.net.URISyntaxException;
+import java.util.Arrays;
+import java.util.List;
+import java.util.regex.Pattern;
+import java.util.stream.Collectors;
+
+/**
+ * Provide functionality for dealing with URI to the Isabelle AFP
+ * export.
+ */
+public class AFP {
+ private static final Logger log = LoggerFactory.getLogger(AFP.class);
+
+ private AFP() {}
+
+ /**
+ * Given an sourceref address from the Isabelle AFP export, try to return an URL to the original
+ * source document.
+ *
+ * This implementation is very specific, it will only work for the specific AFP export were
+ * are dealing with. As of writing this, it is reachable at http://gl.mathhub.info/Isabelle/AFP,
+ * for our experiments we used commit 346f2887.
+ *
+ * @return The URL to the original document, viewable in a web browser. Returns {@code null} if
+ * no URL could be inferred.
+ */
+ public static String sourceUrlFor(String exportIri) {
+ // parse IRI as URI so we can look at the different parts
+
+ URI uri;
+
+ try {
+ uri = new URI(exportIri);
+ } catch (URISyntaxException e) {
+ log.warn("got bad IRI={} error=malformed exception={}", exportIri, e);
+ return null;
+ }
+
+ // we only support this particular host
+
+ if (!uri.getHost().equals("isabelle.in.tum.de")) {
+ log.warn("got bad IRI={} error=bad host", exportIri);
+ return null;
+ }
+
+ // get the path from the full URI
+
+ final String path = uri.getPath();
+
+ if (path == null) {
+ log.warn("got bad IRI={} error=no path", exportIri);
+ return null;
+ }
+
+ log.info("working w/ path={}", path);
+
+ // split into components; we expect there to be at least four
+
+ final List<String> components = splitPath(path, '/');
+ log.info("working w/ components={}", components);
+
+ if (components.size() < 4) {
+ log.warn("got bad IRI={} error=too few components expected=4+ got={}", exportIri, components.size());
+ return null;
+ }
+
+ // evaluate the first two components, which should be fixed
+
+ if (!components.get(0).equals("source")) {
+ log.warn("got bad IRI={} error=bad first component expected=source got={}", exportIri, components.get(0));
+ return null;
+ }
+
+ if (!components.get(1).equals("HOL")) {
+ log.warn("got bad IRI={} error=bad second component expected=HOL got={}", exportIri, components.get(1));
+ return null;
+ }
+
+ // the third component is the library, that is the collection the target
+ // file is in
+
+ final String library = components.get(2);
+
+ // the fourth component is the target package with a lot of cruft
+
+ final String end = ".theory";
+ final String packageWithCruft = components.get(3);
+ final int endIdx = packageWithCruft.indexOf(end);
+
+ if (endIdx == -1) {
+ log.warn("got bad IRI={} error=missing .theory extension", exportIri);
+ return null;
+ }
+
+ final String packageName = packageWithCruft.substring(0, endIdx + end.length());
+
+ // from the package we need to infer the filename
+
+ final List<String> packageComponents = splitPath(packageName, '.');
+
+ log.info("working w/ package={} components={}", packageName, packageComponents);
+
+ if (packageComponents.size() < 2) {
+ throw new IllegalStateException("too few components in IRI=" + exportIri);
+ }
+
+ if (!packageComponents.get(packageComponents.size() - 1).equals("theory")) {
+ throw new IllegalStateException("last component should be .theory, IRI=" + exportIri);
+ }
+
+ final String file = packageComponents.get(packageComponents.size() - 2);
+
+ // finally we can generate the URL
+
+ return String.format(
+ "https://isabelle.in.tum.de/dist/library/HOL/%s/%s.html",
+ library, file
+ );
+ }
+
+ private static List<String> splitPath(String path, char sep) {
+ final String[] components = path.split(Pattern.quote(String.valueOf(sep)));
+ return Arrays.stream(components).map(String::trim).filter(s -> !s.isEmpty()).collect(Collectors.toList());
+ }
+}
diff --git a/src/ulo-storage-applications/src/main/java/info/mathhub/uloapi/html/Routes.java b/src/ulo-storage-applications/src/main/java/info/mathhub/uloapi/html/Routes.java
index 4e6b100..c0c282f 100644
--- a/src/ulo-storage-applications/src/main/java/info/mathhub/uloapi/html/Routes.java
+++ b/src/ulo-storage-applications/src/main/java/info/mathhub/uloapi/html/Routes.java
@@ -83,11 +83,13 @@ public class Routes {
final String uri = Base64.decode(base64uri);
final Meta meta = query.getMeta(uri);
+ final String afpUrl = AFP.sourceUrlFor(meta.sourceref);
final List<PrintableIRI> uses = PrintableIRI.convert(query.getUses(uri));
final Map<String, Object> model = new HashMap<>();
model.put("uri", uri);
model.put("meta", meta);
+ model.put("afp_url", afpUrl);
model.put("uses", uses);
return new ModelAndView(withGlobals(model), "explore_node.flt");
diff --git a/src/ulo-storage-applications/src/main/resources/spark/template/freemarker/explore_node.flt b/src/ulo-storage-applications/src/main/resources/spark/template/freemarker/explore_node.flt
index 2cf4638..d47e28e 100644
--- a/src/ulo-storage-applications/src/main/resources/spark/template/freemarker/explore_node.flt
+++ b/src/ulo-storage-applications/src/main/resources/spark/template/freemarker/explore_node.flt
@@ -41,6 +41,11 @@
<li>
<code>${meta.sourceref}</code>
</li>
+ <#if afp_url??>
+ <li>
+ <a href="${afp_url}">Original Isabelle Source</a> (Experimental. Link might lead to the void.)
+ </li>
+ </#if>
</ul>
<h3>Node uses...</h3>
--
GitLab