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 + "❙"