app: infer isabelle afp url from ulo:sourceref

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>
 

src/ulo-storage-applications/src/main/java/info/mathhub/uloapi/html/AFP.java

+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());
+    }
+}

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");

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>