started on neat mpd visualization. need more things: have ephemeral theories...

started on neat mpd visualization. need more things: have ephemeral theories appear in tgview, have mmt use the mpd role BoundaryCondition, have mpds only display nodes of type Quantity, Law or BoundaryCondition

interview_kernel/interview_kernel.py

@@ -5,27 +5,20 @@ from os.path import join
 from metakernel import MetaKernel
 from IPython.display import HTML, Javascript
 from metakernel import IPythonKernel
+import ipywidgets as widgets
 
 # http://mattoc.com/python-yes-no-prompt-cli.html
 # https://github.com/phfaist/pylatexenc for directly converting Latex commands to unicode
 from pylatexenc.latex2text import LatexNodes2Text
 import getpass
-import matplotlib
-matplotlib.use('nbagg')
-import matplotlib.pyplot as plt
-from bokeh.io import output_notebook, show, export_svgs
-from bokeh.plotting import figure
-from bokeh.resources import CDN
-from bokeh.embed import file_html, components#, notebook_div
-from bokeh.models import ColumnDataSource
-#from tempfile import NamedTemporaryFile
+from bokeh.io import output_notebook
 
 from pde_state_machine import *
 from string_handling import build_url, get_recursively
 
 
-# This "main class" is two things: a REPL loop, by subclassing the cmd2 Cmd class
-# and a state machine as given by the pytransitions package
+"""This is a Jupyter kernel derived from MetaKernel. To use it, install it with the install.py script and run 
+"jupyter notebook --debug --NotebookApp.token='' " from terminal. """
 class Interview(MetaKernel):
     implementation = 'Interview'
     implementation_version = '1.0'
@@ -107,11 +100,12 @@ class Interview(MetaKernel):
         return  # stream_content['text']
 
     def please_prompt(self, query, if_yes, if_no=None, pass_other=False):
-        self.poutput(str(query) + " [y/n]? ")
+        self.poutput(str(query)) # + " [y/n]? ")
         self.state_machine.prompted = True
         self.state_machine.if_yes = if_yes
         self.state_machine.if_no = if_no
         self.state_machine.pass_other = pass_other
+        self.display_widget()
 
     def prompt_input_handling(self, arg):
         """ If we asked for a yes-no answer, execute what was specified in please_prompt.
@@ -152,6 +146,9 @@ class Interview(MetaKernel):
         if arg.startswith("undo"):
             self.do_undo(arg)
             return True
+        if arg.startswith("widget"):
+            self.display_widget()
+            return True
         return False
 
     # called when user types 'explain [expression]'
@@ -235,27 +232,33 @@ class Interview(MetaKernel):
     def display_tgview(self, args=''):
         """displays the theory graph viewer as html, cf. https://github.com/UniFormal/TGView/wiki/"""
 
-        args = args.replace("tgview ", '', 1).strip()
+        args = args.replace("tgview", '', 1).strip()
 
         server_url = str(self.state_machine.mmtinterface.serverInstance)
 
         url_args_dict = {
-            "type": "thgraph",
+            "type": "pgraph",
         }
 
         if args == '':
-            url_args_dict["graphdata"] = self.state_machine.mmtinterface.URIprefix + \
-                                     self.state_machine.mmtinterface.namespace
+            url_args_dict = dict(type="pgraph",
+                                 graphdata=self.state_machine.mmtinterface.namespace)
         else:
-            url_args_dict["graphdata"] = self.state_machine.mmtinterface.URIprefix + \
-                                     self.state_machine.mmtinterface.namespace + "?" + args
+            model_name = self.state_machine.generate_mpd_theories()
+            if model_name is None:  # Fallback for now, because ephemeral theories are not yet accessible to tgview
+                model_name = "Model"
+            url_args_dict = dict(type="mpd",
+                                 graphdata=self.state_machine.mmtinterface.namespace + "?" + model_name)
+
+        url_args_dict["viewOnlyMode"] = "true"
 
         # if applicable, highlight the ephemeral parts https://github.com/UniFormal/TGView/issues/25
         thynames = get_recursively(self.state_machine.simdata, "theoryname")
-        if thynames:
-            url_args_dict["highlight"] = ",".join(thynames)
+        #if thynames:
+        #    url_args_dict["highlight"] = ",".join(thynames)
 
         tgview_url = build_url(server_url, "graphs/tgview.html", args_dict=url_args_dict)
+        print(tgview_url)
 
         code = """
             <iframe 
@@ -267,6 +270,33 @@ class Interview(MetaKernel):
 
         self.display_html(code)
 
+    def display_widget(self):
+        # needs jupyter nbextension enable --py widgetsnbextension
+        from IPython.display import display
+        from IPython.core.formatters import IPythonDisplayFormatter
+        w = widgets.ToggleButton(
+            value=False,
+            description='Click me',
+            disabled=False,
+            button_style='', # 'success', 'info', 'warning', 'danger' or ''
+            tooltip='Description',
+            icon='check'
+        )
+        f = IPythonDisplayFormatter()
+        # these should all do it, but all return the same string
+        #f(w) # = "ToggleButton(value=False, description='Click me', icon='check', tooltip='Description')"
+        #self._ipy_formatter(w)  # = "
+        #display(w) # = "
+        # self.Display(w)  # = "
+        widgets.ToggleButton(
+            value=False,
+            description='Click me',
+            disabled=False,
+            button_style='',  # 'success', 'info', 'warning', 'danger' or ''
+            tooltip='Description',
+            icon='check'
+        )
+
 
 if __name__ == '__main__':
     # from ipykernel.kernelapp import IPKernelApp

interview_kernel/mmtinterface.py

@@ -22,6 +22,7 @@ from lxml import etree
 
 
 def start_mmt_server(port_number, mmtjar):
+    """starts the mmt server as a separate subprocess"""
     p = subprocess.run(["/usr/bin/java", "-jar", mmtjar, # "--file=server-interview.msl",
                           "server", "on", str(port_number), "--keepalive"],
                           stdin=subprocess.PIPE, stdout=subprocess.PIPE, stderr=subprocess.STDOUT)
@@ -31,17 +32,17 @@ def start_mmt_server(port_number, mmtjar):
 
 
 def exit_mmt_server(port_number, mmtjar, timeout=3.0):
+    """tries to shutdown the mmt server process"""
     completed = subprocess.run(["/usr/bin/java", "-jar", mmtjar, ":send", str(port_number),
                                 "exit"],
                                stdin=subprocess.PIPE, stdout=subprocess.PIPE, stderr=subprocess.STDOUT)
     if completed.stdout != None and "(Connection refused)" in str(completed.stdout):
         if timeout > 0.0:
             exit_mmt_server(port_number, mmtjar, timeout - 0.1)
-        # else:
-          #  raise MMTServerError("unable to exit mmt server")
 
 
 def start_mmt_extension(port_number, mmtjar, timeout=3.0):
+    """starts the interview extension for mmt"""
     time.sleep(0.1)  # hope for server to have started communication already
     completed = subprocess.run(["/usr/bin/java", "-jar", mmtjar, ":send", str(port_number),
                   "extension", "info.kwarc.mmt.interviews.InterviewServer"],
@@ -53,6 +54,19 @@ def start_mmt_extension(port_number, mmtjar, timeout=3.0):
             raise MMTServerError("unable to start interview extension")
 
 
+def start_mmt_relational_reader(port_number, mmtjar, timeout=3.0):
+    """starts the relational reader mmt server extension, which is required for some tgview graph types
+            attention: this loads everything in the local mathhub folder, can take some time depending on your files"""
+    completed = subprocess.run(["/usr/bin/java", "-jar", mmtjar, ":send", str(port_number),
+                  "extension", "info.kwarc.mmt.api.ontology.RelationalReader"],
+                               stdin=subprocess.PIPE, stdout=subprocess.PIPE, stderr=subprocess.STDOUT)
+    if completed.stdout != None and "(Connection refused)" in str(completed.stdout):
+        if timeout > 0.0:
+            start_mmt_extension(port_number, mmtjar, timeout-0.1)
+        else:
+            raise MMTServerError("unable to start interview extension")
+
+
 def find_free_port():
     import socket
     port_number = 0
@@ -69,9 +83,12 @@ def run_mmt(mmtjar, port_number=None):
 
     t1 = threading.Thread(target=start_mmt_server, args=(port_number, mmtjar), daemon=True)
     t1.start()
+
+    start_mmt_extension(port_number, mmtjar)
+    start_mmt_relational_reader(port_number, mmtjar)
+
     #t2 = threading.Thread(target=start_mmt_extension, args=[port_number], daemon=True)
     #t2.start()
-    start_mmt_extension(port_number, mmtjar)
     return port_number
 
 
@@ -184,7 +201,7 @@ class MMTInterface:
         self.serverInstance = 'http://localhost:'+str(self.port_number)
         self.extension = ':interview'
         self.URIprefix = 'http://mathhub.info/'
-        self.namespace = 'MitM/smglom/calculus'  # TODO
+        self.namespace = self.URIprefix + 'MitM/smglom/calculus/differentialequations'  # TODO
         self.debugprint = False
 
     def __enter__(self):
@@ -259,7 +276,7 @@ class MMTInterface:
     def get_mpath(self, thyname):
         mpath = thyname
         if not (mpath.startswith("http://") or mpath.startswith("https://")):
-            mpath = self.URIprefix + self.namespace + "?" + thyname  # TODO
+            mpath = self.namespace + "?" + thyname  # TODO
         return mpath
 
     def query_for(self, thingname):

interview_kernel/pde_state_machine.py

@@ -480,7 +480,10 @@ class PDE_States:
                     parsestring = remove_apply_brackets(parsestring)
                 parsestring = functionize(parsestring, self.simdata["domain"]["name"])
                 # self.poutput(parsestring)
-                reply_pconstant = self.mmtinterface.mmt_new_decl("param", parameter_name, parsestring)
+
+                # add the quantitiy role for display as MPD
+                reply_pconstant = self.mmtinterface.mmt_new_decl("param", parameter_name, parsestring +
+                                                                 object_delimiter + " role Quantity")
                 reply_pconstant = self.mmtinterface.query_for(parameter_name)
                 subdict["theoryname"] = parameter_name
                 subdict["string"] = userstring
@@ -572,7 +575,7 @@ class PDE_States:
                 self.mmtinterface.mmt_new_decl("rhs", subdict["viewname"],
                                                "rhs = " + "myrhs")
                 self.mmtinterface.mmt_new_decl("pde", subdict["viewname"],
-                                               "pde = " + "[u](mylhs u) funcEq myrhs")
+                                               "pde = " + "[u](mylhs u) ≐ myrhs")
 
                 reply = self.mmtinterface.query_for(subdict["theoryname"])
 
@@ -852,6 +855,60 @@ class PDE_States:
         # div = notebook_div(p)
         # self.Display(Javascript(script + div))  # show the results
 
+    def generate_mpd_theories(self):
+        with CriticalSubdict({}, self.poutput):
+            # generate Laws that define the parameters, if applicable
+            for paramentry in get_recursively(self.simdata["parameters"], "theoryname"):
+                mpd_theory_name = "MPD_" + paramentry
+                self.mmtinterface.mmt_new_theory(mpd_theory_name)
+                self.include_in(mpd_theory_name, paramentry)
+                if self.mmtinterface.query_for(paramentry).hasDefinition(paramentry):
+                    self.add_list_of_declarations(mpd_theory_name, [
+                        "proof_" + paramentry + " : ⊦ " + self.simdata["parameters"][paramentry]["parsestring"].replace("=", "≐")
+                        + object_delimiter + " role Law"
+                    ])
+
+            # generate the Quantity of a hypothetical solution to an unknown
+            for unknownentry in get_recursively(self.simdata["unknowns"], "theoryname"):
+                mpd_theory_name = "MPD_" + unknownentry
+                self.mmtinterface.mmt_new_theory(mpd_theory_name)
+                self.include_in(mpd_theory_name, unknownentry)
+                self.add_list_of_declarations(mpd_theory_name, [
+                    unknownentry + " : " + self.simdata["unknowns"][unknownentry]["type"]
+                    + object_delimiter + " role Quantity"
+                ])
+
+            # generate the Laws that define it, namely boundary conditions and PDEs #TODO BCs
+            for pdeentry in get_recursively(self.simdata["pdes"], "theoryname"):
+                mpd_theory_name = "MPD_" + pdeentry
+                self.mmtinterface.mmt_new_theory(mpd_theory_name)
+                self.include_in(mpd_theory_name, pdeentry)
+
+                #include all the mpd_unknowns, parameters and bcs #TODO
+                for unknownentry in get_recursively(self.simdata["unknowns"], "theoryname"):
+                    self.include_in(mpd_theory_name, "MPD_" + unknownentry)
+
+                for paramentry in get_recursively(self.simdata["parameters"], "theoryname"):
+                    self.include_in(mpd_theory_name, paramentry)
+
+                self.add_list_of_declarations(mpd_theory_name, [
+                    "proof_" + pdeentry + " : ⊦ " + self.simdata["pdes"]["pdes"][pdeentry]["lhsstring"] +
+                    " ≐ " + self.simdata["pdes"]["pdes"][pdeentry]["rhsstring"]
+                    + object_delimiter + " role Law"
+                ])
+
+            # make an actual model theory that includes all of the Laws declared so far,
+            # which in turn include the Quantities
+            modelname = "Model"
+            self.mmtinterface.mmt_new_theory(modelname)
+            # include all the mpd_parameters, mpd_pdes and mpd_bcs #TODO
+            for paramentry in get_recursively(self.simdata["parameters"], "theoryname"):
+                self.include_in(modelname, "MPD_" + paramentry)
+            for pdeentry in get_recursively(self.simdata["pdes"], "theoryname"):
+                self.include_in(modelname, "MPD_" + pdeentry)
+
+            return modelname
+
     # functions for user interaction
     def obviously_stupid_input(self):
         self.poutput("Trying to be funny, huh?")
@@ -872,14 +929,8 @@ class PDE_States:
         return ok
 
     def new_theory(self, thyname):
-        try:
-            self.mmtinterface.mmt_new_theory(thyname)
-            return self.include_bgthys(thyname)
-        except MMTServerError as error:
-            self.poutput(error.args[0])
-            # self.poutput(error.with_traceback())
-            raise
-        # (ok, root) = self.mmtinterface.query_for(self.simdata[self.state]["theoryname"])
+        self.mmtinterface.mmt_new_theory(thyname)
+        return self.include_bgthys(thyname)
 
     def new_view(self, dictentry):
         """Constructs a new entry 'viewname' into the given dictionary and creates the view,
@@ -899,7 +950,7 @@ class PDE_States:
                 except MMTServerError as error:
                     # self.poutput("no backend available that is applicable to " + "http://mathhub.info/MitM/smglom/calculus" + "?" + re.split('AS', dictentry["viewname"])[-1] + "?")
                     # we are expecting errors if we try to include something that is not referenced in the source theory, so ignore them
-                    expected_str = "no backend available that is applicable to " + "http://mathhub.info/MitM/smglom/calculus" + "?" + re.split('AS', current_view_name)[-1] + "?"
+                    expected_str = "no backend available that is applicable to " + self.mmtinterface.namespace + "?" + re.split('AS', current_view_name)[-1] + "?"
                     if expected_str not in error.args[0]:
                         raise
 
@@ -929,13 +980,13 @@ class PDE_States:
     def print_empty_line(self):
         self.poutput("\n")
 
-    def explain(self, userstring=None):
+    def explain(self, userstring=None):  # TODO
         with CriticalSubdict({}, self.poutput):
             reply = self.mmtinterface.query_for(
                 "http://mathhub.info/smglom/calculus/nderivative.omdoc?nderivative?nderivative")
             self.poutput(reply.tostring())
 
-    def recap(self, userstring=None):
+    def recap(self, userstring=None):  # TODO
         self.print_simdata()
 
     def print_simdata(self):

interview_kernel/string_handling.py

@@ -4,6 +4,8 @@ from distutils.util import strtobool
 import re
 from urllib.parse import urlparse, urlencode, ParseResult
 
+object_delimiter = "❘"
+
 def means_no(answer):
     try:
         ret = strtobool(answer)
@@ -17,8 +19,9 @@ def build_url(baseurl, path, args_dict={}, query_dict={}):
     # Returns a list in the structure of urlparse.ParseResult
     url = urlparse(baseurl)
     # construct new parseresult
-    new_url = ParseResult(url.scheme, url.netloc, path, urlencode(args_dict),
-                          urlencode(query_dict, doseq=True), url.fragment)
+    new_url = ParseResult(url.scheme, url.netloc, path, "", urlencode(args_dict),  # todo urlencode
+                          # urlencode(query_dict, doseq=True),
+                           url.fragment)
     return new_url.geturl()
 
 # cf. https://stackoverflow.com/questions/14962485/finding-a-key-recursively-in-a-dictionary
@@ -51,8 +54,8 @@ def insert_type(string, whichtype):
         raise Exception
     if not self.has_colon(string):
         # print('has no colon ' + equidx)
-        return string[:eqidx] + " : " + whichtype + " ❘ " + string[eqidx:]
-    return string[:eqidx] + " ❘ " + string[eqidx:]
+        return string[:eqidx] + " : " + whichtype + " " + object_delimiter + " " + string[eqidx:]
+    return string[:eqidx] + " " + object_delimiter + " " + string[eqidx:]
 
 
 def type_is_function_from(type_string, from_string):
@@ -171,7 +174,7 @@ def add_ods(string):
     for i in range(2, len(objects)):
         if bool(re.match('[:=]', objects[i], re.I)):  # if it starts with : or =
             if onedel:
-                objects[i] = "❘" + objects[i]
+                objects[i] = object_delimiter + objects[i]
                 return ''.join(objects)
             onedel = True  # start only at second : or =
     return ''.join(objects)