mmtinterface.py 12.8 KB
Newer Older
Theresa Pollinger's avatar
Theresa Pollinger committed
1 2
# to run mmt server : cf. https://docs.python.org/3/library/subprocess.html
import subprocess
3
import time
4
import threading
5
import os
6
# TODO ask dennis on whether and how to delete modules
Theresa Pollinger's avatar
Theresa Pollinger committed
7 8

# to do http requests
9
# http://docs.python-requests.org/en/master/user/quickstart/
Theresa Pollinger's avatar
Theresa Pollinger committed
10 11
import requests
from requests.utils import quote
12
from contextlib import closing
Theresa Pollinger's avatar
Theresa Pollinger committed
13
#from urllib.parse import urlencode # is what we actually want to use
Theresa Pollinger's avatar
Theresa Pollinger committed
14
from lxml import etree
Theresa Pollinger's avatar
Theresa Pollinger committed
15
#from openmath import openmath
Theresa Pollinger's avatar
Theresa Pollinger committed
16

17

18 19 20 21 22 23 24 25 26 27 28 29 30 31 32 33 34 35 36 37 38 39 40 41 42 43 44 45 46 47 48 49 50 51 52 53 54 55 56 57 58 59 60 61 62 63 64 65 66 67 68 69 70 71 72 73 74 75 76 77 78 79 80 81 82 83 84 85 86 87
#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)
#    out = p.stdout
#    if p.returncode != 0 and p.returncode != 130:  # if not closed gracefully or through ctrl-c
#        raise MMTServerError("Server aborted, return code " + str(p.returncode) + ", " + str(out))
#
#
#def exit_mmt_server(port_number, mmtjar, timeout=3.0):
#    """tries to shut down 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)
#
#
#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"],
#                               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 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
#    while (port_number < 1024) or (8888 < port_number < 10000):
#        with closing(socket.socket(socket.AF_INET, socket.SOCK_STREAM)) as s1:
#            s1.bind(('localhost', 0))            # Bind to a free port provided by the host.
#            port_number = s1.getsockname()[1]
#    return port_number  # Return the port number assigned.
#
#
#def run_mmt(mmtjar, port_number=None):
#    if port_number is None:
#        port_number = find_free_port()
#
#    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()
#    return port_number
#
88

Theresa Pollinger's avatar
Theresa Pollinger committed
89
class MMTServerError(Exception):
90
    def __init__(self, err, longerr=None):
Theresa Pollinger's avatar
Theresa Pollinger committed
91
        self.error = err
92 93
        self.longerr = longerr
        super(MMTServerError, self).__init__("MMT server error: " + str(self.error), longerr)
Theresa Pollinger's avatar
Theresa Pollinger committed
94 95 96


class MMTReply:
97 98 99
    """An object that holds
        ok : whether the request was successful and
        root: the returned answer, usually an etree holding the xml reply"""
100

101 102 103
    def __init__(self, ok, root=None):
        self.ok = ok
        self.root = root
104 105
        #        print("creating reply")
        #        print(root)
106 107
        if isinstance(root, etree._Element):
            for element in root.iter():
108 109
                # for element in root.iter("div"): # why not entering this loop?
                # print("for element " + elementToString(element))
110 111 112 113
                if (element.get('class')) == 'error':
                    self.ok = False
                    for child in element:
                        if (child.get('class')) == 'message':
114
                            raise MMTServerError(child.text, element_to_string(self.root))
Theresa Pollinger's avatar
Theresa Pollinger committed
115
        if not self.ok:
116
            raise MMTServerError(element_to_string(self.root))
Theresa Pollinger's avatar
Theresa Pollinger committed
117 118 119

    def getConstant(self, constantname):
        elements = self.getConstants()
120
        # print ("elements: " + str(elements))
Theresa Pollinger's avatar
Theresa Pollinger committed
121 122 123 124 125 126 127
        for element in elements:
            if element.get('name') == constantname:
                return element

    def getConstants(self):
        elements = []
        for element in self.root.iter("constant"):
128
            # print("Constant: %s - %s - %s" % (element, element.text, element.keys()))
Theresa Pollinger's avatar
Theresa Pollinger committed
129 130 131
            elements.append(element)
        return elements

132 133
    def hasDefinition(self, constantname):
        if self.getDefinition(constantname) is not None:
134 135
            return True

Theresa Pollinger's avatar
Theresa Pollinger committed
136 137 138 139 140
    def getDefinition(self, constantname):
        element = self.getConstant(constantname)
        if element is not None:
            for child in element:
                if (child.tag) == 'definition':
141
                    # print(elementToString(child))
Theresa Pollinger's avatar
Theresa Pollinger committed
142 143 144 145 146 147 148
                    return child

    def getType(self, constantname):
        element = self.getConstant(constantname)
        if element is not None:
            for child in element:
                if (child.tag) == 'type':
149 150 151 152 153 154 155 156 157 158 159 160
                    print(element_to_string(child))
                    #return child
                    for oms in child.iter("{*}OMS"):
                        return self.get_name_or_expand_if_arrow(oms)

    def get_name_or_expand_if_arrow(self, oms):
        name = oms.get('name')
        if name == 'arrow':
            next = oms.getnext()
            name = next.get('name')
            while next.getnext() is not None:
                next = next.getnext()
161
                name = name + " ⟶ " + next.get('name')
162
        return name
Theresa Pollinger's avatar
Theresa Pollinger committed
163

164 165
    # (probably very volatile) accesses to concrete data structures
    def getIntervalBoundaries(self, mmtreply, intervalname):
Theresa Pollinger's avatar
Theresa Pollinger committed
166 167
        child = mmtreply.getDefinition(intervalname)
        for oms in child.iter("{*}OMS"):
Theresa Pollinger's avatar
Theresa Pollinger committed
168 169
            #print("OMS: %s - %s - %s" % (oms, oms.text, oms.keys()))
            if (oms.get('name') == 'interval'):
Theresa Pollinger's avatar
Theresa Pollinger committed
170 171
                a = oms.getnext()
                b = a.getnext()
Theresa Pollinger's avatar
Theresa Pollinger committed
172 173
                #print("a: %s - %s - %s" % (a, a.text, a.get('value')))
                #print("b: %s - %s - %s" % (b, b.text, b.get('value')))
Theresa Pollinger's avatar
Theresa Pollinger committed
174 175
                return (a.get('value'), b.get('value'))

176 177
    def tostring(self):
        return element_to_string(self.root)
Theresa Pollinger's avatar
Theresa Pollinger committed
178

179 180 181 182
    def inferred_type_to_string(self):
        type_string = ""
        for mo in self.root.iter("{*}mo"):
            type_string = type_string + " " + mo.text
183
        return type_string.strip()
184

185 186 187

def element_to_string(element):
    return etree.tostring(element, pretty_print=True).decode('utf8')
Theresa Pollinger's avatar
Theresa Pollinger committed
188

189

Theresa Pollinger's avatar
Theresa Pollinger committed
190
class MMTInterface:
191 192 193 194 195 196 197 198 199 200
    def __init__(self):
        # get current mmt url
        self.mmt_base_url = os.environ.setdefault('MMT_BASE_URL', 'http://localhost:9000')

        # set up session
        self.session = requests.Session()
        self.adapter = requests.adapters.HTTPAdapter()
        self.session.mount('https://', self.adapter)
        self.session.mount('http://', self.adapter)

Theresa Pollinger's avatar
Theresa Pollinger committed
201
        # set parameters for communication with mmt server
202
        self.mmt_extension = ':interview'
Theresa Pollinger's avatar
Theresa Pollinger committed
203
        self.URIprefix = 'http://mathhub.info/'
204
        self.namespace = self.URIprefix + 'MitM/smglom/calculus/differentialequations'  # TODO
205

206
        self.debugprint = False
Theresa Pollinger's avatar
Theresa Pollinger committed
207 208

    def mmt_new_theory(self, thyname):
209 210 211
        # So, ich hab mal was zu MMT/devel gepusht. Es gibt jetzt eine Extension namens InterviewServer. Starten tut man die mit "extension info.kwarc.mmt.interviews.InterviewServer"
        # Wenn du dann in MMT den Server (sagen wir auf Port 8080) startest, kannst du folgende HTTP-Requests ausführen:
        # "http://localhost:8080/:interview/new?theory="<MMT URI>"" fügt eine neue theorie mit der uri <MMT URI> hinzu
212
        req = '/' + self.mmt_extension + '/new?theory=' + quote(self.get_mpath(
213
            thyname)) + '&meta=' + quote('http://mathhub.info/MitM/Foundation?Logic')
Theresa Pollinger's avatar
Theresa Pollinger committed
214 215 216 217
        return self.http_request(req)

    def mmt_new_view(self, viewname, fromtheory, totheory):
        # analog für ?view="<MMT URI>".
218
        req = '/' + self.mmt_extension + '/new?view=' + quote(self.get_mpath(viewname)) + '&from=' + quote(self.get_mpath(
219
            fromtheory)) + '&to=' + quote(self.get_mpath(totheory))
Theresa Pollinger's avatar
Theresa Pollinger committed
220 221 222
        return self.http_request(req)

    def mmt_new_decl(self, declname, thyname, declcontent):
223
        # ".../:interview/new?decl="<irgendwas>"&cont="<MMT URI>" ist der query-path um der theorie <MMT URI> eine neue declaration hinzuzufügen (includes, konstanten...). Die Declaration sollte dabei in MMT-syntax als text im Body des HTTP-requests stehen.
224
        post = '/' + self.mmt_extension + '/new?decl=d&cont=' + quote(self.get_mpath(thyname))
Theresa Pollinger's avatar
Theresa Pollinger committed
225 226 227
        return self.http_request(post, add_dd(declcontent))

    def mmt_new_term(self, termname, thyname, termcontent):
228
        # analog für ".../:interview/new?term="<irgendwas>"&cont="<MMT URI>" für terme - nachdem da nicht klar ist was der server damit tun sollte gibt er den geparsten term als omdoc-xml zurück (wenn alles funktioniert)
229
        post = '/' + self.mmt_extension + '/new?term=' + quote(termname) + '&cont=' + quote(self.get_mpath(thyname))
230 231 232
        return self.http_request(post, termcontent)

    def mmt_infer_type(self, thyname, termcontent):
233
        post = '/' + self.mmt_extension + '/infer?cont=' + quote(self.get_mpath(thyname))
Theresa Pollinger's avatar
Theresa Pollinger committed
234 235 236
        return self.http_request(post, termcontent)

    def http_request(self, message, data=None):
237
        url = self.mmt_base_url + message
Theresa Pollinger's avatar
Theresa Pollinger committed
238 239 240 241 242 243
        print(url) if self.debugprint else 0
        try:
            if data:
                binary_data = data.encode('UTF-8')
                print('\n' + str(data)) if self.debugprint else 0
                headers = {'content-type': 'application/json',
244
                           'content-encoding': 'UTF-8'}
245
                req = self.session.post(url, data=binary_data, headers=headers, stream=True)
Theresa Pollinger's avatar
Theresa Pollinger committed
246 247
            else:
                req = requests.get(url)
248
        except ConnectionError as error:  # this seems to never be called
Theresa Pollinger's avatar
Theresa Pollinger committed
249 250
            print(error)
            print("Are you sure the mmt server is running?")
251
            raise
252
        # print(req.text) if self.debugprint else 0
Theresa Pollinger's avatar
Theresa Pollinger committed
253 254
        if req.text.startswith('<'):
            root = etree.fromstring(req.text)
255 256
        else:
            root = None
Theresa Pollinger's avatar
Theresa Pollinger committed
257
        if req.status_code == 200:
258 259
            return MMTReply(True, root)
        return MMTReply(False, root)
Theresa Pollinger's avatar
Theresa Pollinger committed
260 261

    def get_mpath(self, thyname):
262 263
        mpath = thyname
        if not (mpath.startswith("http://") or mpath.startswith("https://")):
264
            mpath = self.namespace + "?" + thyname  # TODO
Theresa Pollinger's avatar
Theresa Pollinger committed
265 266 267
        return mpath

    def query_for(self, thingname):
268 269
        # this here just stolen from what MMTPy does
        # querycontent = b'<function name="presentDecl" param="xml"><literal><uri path="http://mathhub.info/MitM/smglom/algebra?magma"/></literal></function>'
Theresa Pollinger's avatar
Theresa Pollinger committed
270
        querycontent = '<function name="presentDecl" param="xml"><literal><uri path="' + (self.get_mpath(thingname)) + '"/></literal></function>'
271

Theresa Pollinger's avatar
Theresa Pollinger committed
272 273 274
        return self.http_qrequest(querycontent)

    def http_qrequest(self, data, message='/:query'):
275
        url = self.mmt_base_url + message
276
        print(url) if self.debugprint else 0
277 278
        self.session.mount('https://', self.adapter)
        self.session.mount('http://', self.adapter)
279
        print('\n' + str(data)) if self.debugprint else 0
Theresa Pollinger's avatar
Theresa Pollinger committed
280 281
        binary_data = data.encode('UTF-8')
        headers = {'content-type': 'application/xml'}
282
        req = self.session.post(url, data=binary_data, headers=headers, stream=True)
Theresa Pollinger's avatar
Theresa Pollinger committed
283 284
        root = etree.fromstring(req.text)
        if req.status_code == 200:
285 286
            return MMTReply(True, root)
        return MMTReply(False, root)
Theresa Pollinger's avatar
Theresa Pollinger committed
287

288

Theresa Pollinger's avatar
Theresa Pollinger committed
289
def add_dd(string):
290 291
    if string.endswith("❙") or string.endswith("❚"):
        return string
Theresa Pollinger's avatar
Theresa Pollinger committed
292
    return string + "❙"