mmtinterface.py 12.5 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 psutil
4
import time
5
# for now, running
6
7
# java -jar /home/freifrau/Desktop/masterarbeit/mmt/deploy/mmt.jar --file=server-interview.msl --keepalive
# or
Theresa Pollinger's avatar
Theresa Pollinger committed
8
9
10
# mmt
# extension info.kwarc.mmt.interviews.InterviewServer
# server on 8080
11
import threading
12
# TODO ask dennis on whether and how to delete modules
Theresa Pollinger's avatar
Theresa Pollinger committed
13
14

# to do http requests
15
# http://docs.python-requests.org/en/master/user/quickstart/
Theresa Pollinger's avatar
Theresa Pollinger committed
16
17
import requests
from requests.utils import quote
18
from contextlib import closing
Theresa Pollinger's avatar
Theresa Pollinger committed
19
#from urllib.parse import urlencode # is what we actually want to use
Theresa Pollinger's avatar
Theresa Pollinger committed
20
from lxml import etree
Theresa Pollinger's avatar
Theresa Pollinger committed
21
#from openmath import openmath
Theresa Pollinger's avatar
Theresa Pollinger committed
22

23

24
def start_mmt_server(port_number, mmtjar):
Theresa Pollinger's avatar
Theresa Pollinger committed
25
26
    p = subprocess.run(["/usr/bin/java", "-jar", mmtjar, # "--file=server-interview.msl",
                          "server", "on", str(port_number),
27
28
29
                          "--keepalive"],
                          stdin=subprocess.PIPE, stdout=subprocess.PIPE, stderr=subprocess.STDOUT)
    out = p.stdout
Theresa Pollinger's avatar
Theresa Pollinger committed
30
31
    if p.returncode != 0 and p.returncode != 130:
        raise MMTServerError("Could not start the MMT server, return code " + str(p.returncode) + ", " + str(out))
32
33
34
35
36
    #outs, errs = p.communicate()
    #if outs is not None:
        #print("MMT server terminated before rest of program, ")  # this just wont stay alive!!!
        #p.terminate()
        #raise MMTServerError("MMT server terminated before rest of program, ")  # + p.stdout)
37

38
39
40
41
42
43
44
45
46
def exit_mmt_server(port_number, mmtjar, timeout=3.0):
    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:
            start_mmt_extension(port_number, mmtjar, timeout - 0.1)
        else:
            raise MMTServerError("unable to start interview extension")
47

48
49
def start_mmt_extension(port_number, mmtjar, timeout=3.0):
    time.sleep(0.1)  # hope for server to have started communication already
50
51
    completed = subprocess.run(["/usr/bin/java", "-jar", mmtjar, ":send", str(port_number),
                  "extension", "info.kwarc.mmt.interviews.InterviewServer"],
52
53
                               stdin=subprocess.PIPE, stdout=subprocess.PIPE, stderr=subprocess.STDOUT)
    if completed.stdout != None and "(Connection refused)" in str(completed.stdout):
54
55
56
57
58
59
60
61
        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
62
63
64
65
66
67
    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.
68
69


70
71
72
def run_mmt(mmtjar, port_number=None):
    if port_number is None:
        port_number = find_free_port()
73

74
75
76
77
78
    t1 = threading.Thread(target=start_mmt_server, args=(port_number, mmtjar), daemon=True)
    t1.start()
    #t2 = threading.Thread(target=start_mmt_extension, args=[port_number], daemon=True)
    #t2.start()
    start_mmt_extension(port_number, mmtjar)
79
    return port_number
80

81

Theresa Pollinger's avatar
Theresa Pollinger committed
82
class MMTServerError(Exception):
83
    def __init__(self, err, longerr=None):
Theresa Pollinger's avatar
Theresa Pollinger committed
84
        self.error = err
85
86
        self.longerr = longerr
        super(MMTServerError, self).__init__("MMT server error: " + str(self.error), longerr)
Theresa Pollinger's avatar
Theresa Pollinger committed
87
88
89


class MMTReply:
90
91
92
    """An object that holds
        ok : whether the request was successful and
        root: the returned answer, usually an etree holding the xml reply"""
93

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

    def getConstant(self, constantname):
        elements = self.getConstants()
113
        # print ("elements: " + str(elements))
Theresa Pollinger's avatar
Theresa Pollinger committed
114
115
116
117
118
119
120
        for element in elements:
            if element.get('name') == constantname:
                return element

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

125
126
    def hasDefinition(self, constantname):
        if self.getDefinition(constantname) is not None:
127
128
            return True

Theresa Pollinger's avatar
Theresa Pollinger committed
129
130
131
132
133
    def getDefinition(self, constantname):
        element = self.getConstant(constantname)
        if element is not None:
            for child in element:
                if (child.tag) == 'definition':
134
                    # print(elementToString(child))
Theresa Pollinger's avatar
Theresa Pollinger committed
135
136
137
138
139
140
141
                    return child

    def getType(self, constantname):
        element = self.getConstant(constantname)
        if element is not None:
            for child in element:
                if (child.tag) == 'type':
142
143
144
145
146
147
148
149
150
151
152
153
154
155
                    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()
                name = name + " → " + next.get('name')
        return name
Theresa Pollinger's avatar
Theresa Pollinger committed
156

157
158
    # (probably very volatile) accesses to concrete data structures
    def getIntervalBoundaries(self, mmtreply, intervalname):
Theresa Pollinger's avatar
Theresa Pollinger committed
159
160
        child = mmtreply.getDefinition(intervalname)
        for oms in child.iter("{*}OMS"):
Theresa Pollinger's avatar
Theresa Pollinger committed
161
162
            #print("OMS: %s - %s - %s" % (oms, oms.text, oms.keys()))
            if (oms.get('name') == 'interval'):
Theresa Pollinger's avatar
Theresa Pollinger committed
163
164
                a = oms.getnext()
                b = a.getnext()
Theresa Pollinger's avatar
Theresa Pollinger committed
165
166
                #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
167
168
                return (a.get('value'), b.get('value'))

169
170
    def tostring(self):
        return element_to_string(self.root)
Theresa Pollinger's avatar
Theresa Pollinger committed
171

172
173
174
175
    def inferred_type_to_string(self):
        type_string = ""
        for mo in self.root.iter("{*}mo"):
            type_string = type_string + " " + mo.text
176
        return type_string.strip()
177

178
179
180

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

182

Theresa Pollinger's avatar
Theresa Pollinger committed
183
class MMTInterface:
184
    def __init__(self, mmt_jar="/home/freifrau/Desktop/masterarbeit/mmt/deploy/mmt.jar"):
185
186
        self.mmt_jar = mmt_jar
        self.port_number = run_mmt(self.mmt_jar)  # , port_number)
Theresa Pollinger's avatar
Theresa Pollinger committed
187
        # set parameters for communication with mmt server
188
        self.serverInstance = 'http://localhost:'+str(self.port_number)
Theresa Pollinger's avatar
Theresa Pollinger committed
189
190
        self.extension = ':interview'
        self.URIprefix = 'http://mathhub.info/'
191
        self.namespace = 'MitM/smglom/calculus'  # TODO
Theresa Pollinger's avatar
Theresa Pollinger committed
192
        self.debugprint = False
193

194
195
196
197
198
199
    def __enter__(self):
        return self

    def __exit__(self, exc_type, exc_val, exc_tb):
        self.exit_mmt()

200
201
    def exit_mmt(self):
        exit_mmt_server(self.port_number, self.mmt_jar)
Theresa Pollinger's avatar
Theresa Pollinger committed
202
203

    def mmt_new_theory(self, thyname):
204
205
206
        # 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
207
208
        req = '/' + self.extension + '/new?theory=' + quote(self.get_mpath(
            thyname)) + '&meta=' + quote('http://mathhub.info/MitM/Foundation?Logic')
Theresa Pollinger's avatar
Theresa Pollinger committed
209
210
211
212
        return self.http_request(req)

    def mmt_new_view(self, viewname, fromtheory, totheory):
        # analog für ?view="<MMT URI>".
213
214
        req = '/' + self.extension + '/new?view=' + quote(self.get_mpath(viewname)) + '&from=' + quote(self.get_mpath(
            fromtheory)) + '&to=' + quote(self.get_mpath(totheory))
Theresa Pollinger's avatar
Theresa Pollinger committed
215
216
217
        return self.http_request(req)

    def mmt_new_decl(self, declname, thyname, declcontent):
218
        # ".../: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.
219
        post = '/' + self.extension + '/new?decl=d&cont=' + quote(self.get_mpath(thyname))
Theresa Pollinger's avatar
Theresa Pollinger committed
220
221
222
        return self.http_request(post, add_dd(declcontent))

    def mmt_new_term(self, termname, thyname, termcontent):
223
        # 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)
224
225
226
227
228
        post = '/' + self.extension + '/new?term=' + quote(termname) + '&cont=' + quote(self.get_mpath(thyname))
        return self.http_request(post, termcontent)

    def mmt_infer_type(self, thyname, termcontent):
        post = '/' + self.extension + '/infer?cont=' + quote(self.get_mpath(thyname))
Theresa Pollinger's avatar
Theresa Pollinger committed
229
230
231
        return self.http_request(post, termcontent)

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

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

    def query_for(self, thingname):
267
268
        # 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
269
        querycontent = '<function name="presentDecl" param="xml"><literal><uri path="' + (self.get_mpath(thingname)) + '"/></literal></function>'
270

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

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

289

Theresa Pollinger's avatar
Theresa Pollinger committed
290
291
def add_dd(string):
    return string + "❙"