Add LaTeX support in Jupyter, improve HTML

Example.ipynb

@@ -29,7 +29,7 @@
    "source": [
     "## Creating OpenMath and LC objects\n",
     "\n",
-    "The usual `OM.simple()` factory function builds OpenMath objects, which have been taught to represent themselves using OpenMath XML."
+    "The usual `OM.simple()` factory function builds OpenMath objects, which have been taught to represent themselves using a simple encoding."
    ]
   },
   {
@@ -40,11 +40,10 @@
     {
      "data": {
       "text/html": [
-       "<pre>&lt;OMA&gt;\n",
-       "  &lt;OMV name=&quot;f&quot;/&gt;\n",
-       "  &lt;OMV name=&quot;x&quot;/&gt;\n",
-       "  &lt;OMV name=&quot;y&quot;/&gt;\n",
-       "&lt;/OMA&gt;</pre>"
+       "$f(x,y)$"
+      ],
+      "text/latex": [
+       "$f(x,y)$"
       ],
       "text/plain": [
        "OMNode {\n",
@@ -78,6 +77,9 @@
       "text/html": [
        "<pre>{ f(x) { :A B } }</pre>"
       ],
+      "text/latex": [
+       "$\\{~f(x)~\\{~{:}A~B~\\}~\\}$"
+      ],
       "text/plain": [
        "<ref *1> Environment {\n",
        "  attributes: { declaration: 'none', formula: false },\n",
@@ -135,6 +137,12 @@
       "text/html": [
        "<table style=\"border: 1px solid black;\"><tr><td>Pattern</td><td>Expression</td></tr><tr><td style=\"text-align: left;\">f(A,B)</td><td style=\"text-align: left;\">f(one,two)</td></tr></table>"
       ],
+      "text/latex": [
+       "\\begin{tabular}{ll}\n",
+       "Pattern & Expression \\\\\\hline\n",
+       "$f(A,B)$ & $f(one,two)$\n",
+       "\\end{tabular}"
+      ],
       "text/plain": [
        "MatchingProblem {\n",
        "  _MC: MatchingChallenge {\n",
@@ -214,6 +222,13 @@
       "text/html": [
        "<table style=\"border: 1px solid black;\"><tr><td>Metavariable</td><td>Instantiation</td></tr><tr><td>A</td><td style=\"text-align: left;\">one</td></tr><tr><td>B</td><td style=\"text-align: left;\">two</td></tr></table>"
       ],
+      "text/latex": [
+       "\\begin{tabular}{rl}\n",
+       "Metavariable & Instantiation \\\\\\hline\n",
+       "A & $one$\\\\\n",
+       "B & $two$\n",
+       "\\end{tabular}"
+      ],
       "text/plain": [
        "MatchingSolution {\n",
        "  _mapping: {\n",
@@ -267,6 +282,9 @@
       "text/html": [
        "<pre>{ :X :Y and(X,Y) }</pre>"
       ],
+      "text/latex": [
+       "$\\{~{:}X~{:}Y~and(X,Y)~\\}$"
+      ],
       "text/plain": [
        "<ref *1> Environment {\n",
        "  attributes: { declaration: 'none', formula: false },\n",
@@ -334,6 +352,9 @@
       "text/html": [
        "<tt>a, b, { :X :Y and(X,Y) }</tt> $~\\vdash~$ <tt>and(b,a)</tt>"
       ],
+      "text/latex": [
+       "$a, b, \\{~{:}X~{:}Y~and(X,Y)~\\} \\vdash and(b,a)$"
+      ],
       "text/plain": [
        "Turnstile {\n",
        "  premises: [\n",
@@ -429,6 +450,13 @@
       "text/html": [
        "<table style=\"border: 1px solid black;\"><tr><td>Metavariable</td><td>Instantiation</td></tr><tr><td>X</td><td style=\"text-align: left;\">b</td></tr><tr><td>Y</td><td style=\"text-align: left;\">a</td></tr></table>"
       ],
+      "text/latex": [
+       "\\begin{tabular}{rl}\n",
+       "Metavariable & Instantiation \\\\\\hline\n",
+       "X & $b$\\\\\n",
+       "Y & $a$\n",
+       "\\end{tabular}"
+      ],
       "text/plain": [
        "MatchingSolution {\n",
        "  _mapping: {\n",
@@ -483,6 +511,16 @@
       "text/html": [
        "<table style=\"border: 1px solid black;\"><tr><td style=\"text-align: left;\"><tt>a, b, { :b :a and(b,a) }</tt> $~\\vdash~$ <tt>and(b,a)</tt></td><td style=\"text-align: left;\">GL</td></tr><tr><td style=\"text-align: left;\">&nbsp; &nbsp; &nbsp; &nbsp; &nbsp; &nbsp; <tt>a, b, and(b,a)</tt> $~\\vdash~$ <tt>and(b,a)</tt></td><td style=\"text-align: left;\">S</td></tr><tr><td style=\"text-align: left;\">&nbsp; &nbsp; &nbsp; &nbsp; &nbsp; &nbsp; <tt>a, b</tt> $~\\vdash~$ <tt>{ b a }</tt></td><td style=\"text-align: left;\">CR</td></tr><tr><td style=\"text-align: left;\">&nbsp; &nbsp; &nbsp; &nbsp; &nbsp; &nbsp; &nbsp; &nbsp; &nbsp; &nbsp; &nbsp; &nbsp; <tt>a, b</tt> $~\\vdash~$ <tt>b</tt></td><td style=\"text-align: left;\">S</td></tr><tr><td style=\"text-align: left;\">&nbsp; &nbsp; &nbsp; &nbsp; &nbsp; &nbsp; &nbsp; &nbsp; &nbsp; &nbsp; &nbsp; &nbsp; <tt>a, b</tt> $~\\vdash~$ <tt>{ a }</tt></td><td style=\"text-align: left;\">CR</td></tr><tr><td style=\"text-align: left;\">&nbsp; &nbsp; &nbsp; &nbsp; &nbsp; &nbsp; &nbsp; &nbsp; &nbsp; &nbsp; &nbsp; &nbsp; &nbsp; &nbsp; &nbsp; &nbsp; &nbsp; &nbsp; <tt>a, b</tt> $~\\vdash~$ <tt>a</tt></td><td style=\"text-align: left;\">S</td></tr><tr><td style=\"text-align: left;\">&nbsp; &nbsp; &nbsp; &nbsp; &nbsp; &nbsp; &nbsp; &nbsp; &nbsp; &nbsp; &nbsp; &nbsp; &nbsp; &nbsp; &nbsp; &nbsp; &nbsp; &nbsp; <tt>a, b</tt> $~\\vdash~$ <tt>{  }</tt></td><td style=\"text-align: left;\">T</td></tr><tr><td style=\"text-align: left;\"><tt></tt></td><td style=\"text-align: left;\"></td></tr></table>"
       ],
+      "text/latex": [
+       "$\\begin{array}{ll}a,~b,~\\{~{:}b~{:}a~and(b,a)~\\}~\\vdash~and(b,a) & \\text{GL}\\\\\n",
+       "\\hspace{1cm}a,~b,~and(b,a)~\\vdash~and(b,a) & \\text{S}\\\\\n",
+       "\\hspace{1cm}a,~b~\\vdash~\\{~b~a~\\} & \\text{CR}\\\\\n",
+       "\\hspace{1cm}\\hspace{1cm}a,~b~\\vdash~b & \\text{S}\\\\\n",
+       "\\hspace{1cm}\\hspace{1cm}a,~b~\\vdash~\\{~a~\\} & \\text{CR}\\\\\n",
+       "\\hspace{1cm}\\hspace{1cm}\\hspace{1cm}a,~b~\\vdash~a & \\text{S}\\\\\n",
+       "\\hspace{1cm}\\hspace{1cm}\\hspace{1cm}a,~b~\\vdash~\\{~~\\} & \\text{T}\\\\\n",
+       " & \\text{}\\end{array}$"
+      ],
       "text/plain": [
        "Proof {\n",
        "  turnstile: Turnstile {\n",

classes/deduction.js

@@ -52,6 +52,14 @@ class Turnstile {
     const concl = withoutPreTags( this.conclusion._toHtml() )
     return `<tt>${prems}</tt> $~\\vdash~$ <tt>${concl}</tt>`
   }
+  // for converting Jupyter notebooks to LaTeX/PDF
+  _toMime () {
+    const removeMathMode = ( text ) => text.substring( 1, text.length - 1 )
+    const prems = this.premises.map( p =>
+      removeMathMode( p._toMime()["text/latex"] ) ).join( ', ' )
+    const concl = removeMathMode( this.conclusion._toMime()["text/latex"] )
+    return { "text/latex": `$${prems} \\vdash ${concl}$` }
+  }
   // Compare two LCs in a way that is useful for the derivation checker, defined
   // later in this class.
   // Specifically, it returns an object with the following attributes:
@@ -633,6 +641,27 @@ class Proof {
     } )
     return `<table style="border: 1px solid black;">${lines.join( '' )}</table>`
   }
+  // for converting Jupyter notebooks to LaTeX/PDF
+  _toMime () {
+    const prepareMath = ( text ) =>
+      text.replace( / /g, '~' ).replace( /{/g, '\\{' ).replace( /}/g, '\\}' )
+          .replace( /[:]/g, '{:}' ).replace( /[|]-/g, '\\vdash' )
+    const lines = this.toString().split( '\n' ).map( line => {
+      if ( line.substring( line.length - 25 ) == ' using these subproof(s):' )
+        line = line.substring( 0, line.length - 25 )
+      const rule = line.split( ' ' ).pop()
+      line = line.substring( 0, line.length - rule.length - 4 )
+      let indent = ''
+      while ( line.substring( 0, 2 ) == '. ' ) {
+        line = line.substring( 2 )
+        indent += '\\hspace{1cm}'
+      }
+      return `${indent}${prepareMath( line )} & \\text{${rule}}`
+    } )
+    return {
+      "text/latex": `$\\begin{array}{ll}${lines.join('\\\\\n')}\\end{array}$`
+    }
+  }
 }
 
 

classes/lc.js

@@ -166,6 +166,13 @@ class LC extends Structure {
           .replace( /'/g, "'" )
     return `<pre>${escapeXML(this.toString())}</pre>`
   }
+  // for converting Jupyter notebooks to LaTeX/PDF
+  _toMime () {
+    const escapeMath = ( text ) =>
+      text.replace( / /g, '~' ).replace( /{/g, '\\{' ).replace( /}/g, '\\}' )
+          .replace( /[:]/g, '{:}' )
+    return { "text/latex": `$${escapeMath( this.toString() )}$` }
+  }
 
   // Abstract-like method that subclasses will fix:
   toOM () {

classes/matching.js

@@ -35,9 +35,9 @@ const escapeXML = ( text ) => text.replace( /&/g, "&" )
                                   .replace( />/g, ">" )
                                   .replace( /"/g, """ )
                                   .replace( /'/g, "'" )
-OM.prototype._toHtml = function () {
-  return `<pre>${escapeXML(this.toXML())}</pre>`
-}
+OM.prototype._toHtml = function () { return `$${this.simpleEncode()}$` }
+// And support converting Jupyter notebooks to LaTeX/PDF
+OM.prototype._toMime = function () { return { "text/latex": this._toHtml() } }
 
 // A MatchingSolution is a mapping from metavariables to expressions,
 // representing the solution to a MatchingProblem (which is defined below).
@@ -145,6 +145,27 @@ class MatchingSolution {
          + `<tr><td>Metavariable</td><td>Instantiation</td></tr>`
          + `${result}</table>`
   }
+  // for converting Jupyter notebooks to LaTeX/PDF
+  _toMime () {
+    let result = this.keys().map( metavariableName => {
+      const instantiation = this.lookup( metavariableName )
+      let rhs
+      if ( instantiation.isAQuantifier && instantiation.identifier == 'gEF' ) {
+        const vars = instantiation.allButLast.map( v => `${v}` )
+        rhs = instantiation.last._toMime()["text/latex"]
+        rhs = rhs.substring( 1, rhs.length - 1 )
+        rhs = `\\lambda ${vars.join( ',' )}.${rhs}`
+      } else {
+        rhs = instantiation._toMime()["text/latex"]
+      }
+      return `${metavariableName} & ${rhs}`
+    } ).join( '\\\\\n' )
+    if ( result == '' )
+      result = '(empty & function)\\\\'
+    return { "text/latex": `\\begin{tabular}{rl}\n`
+         + `Metavariable & Instantiation \\\\\\hline\n`
+         + `${result}\n\\end{tabular}` }
+  }
 }
 
 // A matching problem is an object that a client constructs to pose a matching
@@ -259,6 +280,18 @@ class MatchingProblem {
          + `<tr><td>Pattern</td><td>Expression</td></tr>`
          + `${result}</table>`
   }
+  // for converting Jupyter notebooks to LaTeX/PDF
+  _toMime () {
+    let result = this._MC.challengeList.contents.map( pair => {
+      return `${pair.pattern._toMime()["text/latex"]} & `
+           + `${pair.expression._toMime()["text/latex"]}`
+    } ).join( '\\\\\n' )
+    if ( result == '' )
+      result = '(empty & function)\\\\'
+    return { "text/latex": `\\begin{tabular}{ll}\n`
+         + `Pattern & Expression \\\\\\hline\n`
+         + `${result}\n\\end{tabular}` }
+  }
 }
 
 module.exports.MatchingSolution = MatchingSolution