pde_state_machine.py 49 KB
Newer Older
1
2
3
4
5
#!/usr/bin/env python3

# https://github.com/pytransitions/transitions
from transitions import Machine, State
from collections import OrderedDict
6
7

import getpass
8
import re
9
from html import escape
10

11
12
13
from . import string_handling
from .exaoutput import ExaOutput, ExaRunner
from .mmtinterface import *
14

15
16
17
18
19
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
20
21

class InterviewError(Exception):
22
    """Errors that occur during the course of the interview and are not due to mmt server errors"""
23

24
25
26
27
28
29
    def __init__(self, err):
        self.error = err
        super(InterviewError, self).__init__("Interview error: " + str(self.error))


class CriticalSubdict():
30
    def __init__(self, subdict, output_function=print, outermost=True):
31
32
33
        """The sub-part of a dictionary that needs to be restored if something goes wrong -
        To be used in with-statements.
        Catches errors only if it is the outermost one"""
34
35
        self.subdict = subdict
        self.initial_subdict = self.subdict.copy()
36
37
        self.output_function = output_function
        self.outermost = outermost
38
39
40
41
42
43

    def __enter__(self):
        return self.subdict

    def __exit__(self, type, value, traceback):
        if type is not None:
44
            # restore the initial state
45
46
47
            self.subdict.clear()
            for key in self.initial_subdict:
                self.subdict[key] = self.initial_subdict[key]
48
            # handling: give feedback, only if our own error, and the outermost subdict
49
50
51
52
            if isinstance(value, MMTServerError) and self.outermost:
                self.please_repeat(value.args[0], value.longerr)
                return True
            elif isinstance(value, InterviewError) and self.outermost:
53
54
55
56
57
58
                self.please_repeat(value.args[0])
                return True
            else:
                return False
        return True

59
    def please_repeat(self, moreinfo=None, evenmoreinfo=None):
60
61
62
        append = ""
        if moreinfo:
            append = "\nDetails: " + moreinfo
63
64
        if evenmoreinfo:
            append += ". " + evenmoreinfo
65
        self.output_function("I did not catch that. Could you please rephrase?" + append, 'stderr')
66
67
68


class PDE_States:
69
    """A state machine using pytranisitions that walks our theory graph and creates ephemeral theories and views"""
70

71
    def __init__(self, output_function, after_state_change_function, prompt_function, display_html_function=None,
72
                 install_run=False, toggle_show_button=None):
73
74
75
        # just act like we were getting the right replies from MMT
        self.cheating = True

76
        # callback handles
77
78
        self.poutput = output_function
        self.please_prompt = prompt_function
79
        self.display_html = display_html_function
80
        self.toggle_show_button = toggle_show_button
81
82

        # Initialize a state machine
83
84
        self.states = [
            State('greeting', on_exit=['greeting_exit']),
85
86
87
88
89
90
91
92
93
            State('dimensions', on_enter=['dimensions_begin']),
            State('domain', on_enter=['domain_begin'], on_exit=['domain_exit']),
            State('unknowns', on_enter=['unknowns_begin'], on_exit=['unknowns_exit']),
            State('parameters', on_enter=['parameters_begin'], on_exit=['parameters_exit']),
            State('pdes', on_enter=['pdes_begin'], on_exit=['pdes_exit']),
            State('bcs', on_enter=['bcs_begin'], on_exit=['bcs_exit']),
            State('props', on_enter=['props_begin'], on_exit=['props_exit']),
            State('sim', on_enter=['sim_begin'], on_exit=['sim_exit']),
        ]
94
95
96
        self.states.reverse()
        self.machine = Machine(model=self, states=self.states, initial=self.states[-1],
                               after_state_change=after_state_change_function, queued=True)
97
98
99
100
        # this is why we were reverting the states => can always go back
        self.machine.add_ordered_transitions(
            trigger='last_state')  # TODO do something to avoid going back from the first state
        # self.to_dimensions()
101
        self.machine.add_transition(trigger='greeting_over', source='greeting', dest='dimensions')
102
103
104
105
        self.machine.add_transition(trigger='dimensions_parsed', source='dimensions', dest='domain',
                                    before='print_empty_line')
        self.machine.add_transition(trigger='domain_parsed', source='domain', dest='unknowns',
                                    before='print_empty_line')
106
107
        self.machine.add_transition(trigger='unknowns_parsed', source='unknowns', dest='parameters')
        self.machine.add_transition(trigger='parameters_parsed', source='parameters', dest='pdes')
108
        self.machine.add_transition(trigger='pdes_parsed', source='pdes', dest='bcs', before='print_empty_line')
109
110
        self.machine.add_transition(trigger='bcs_parsed', source='bcs', dest='props', before='print_empty_line')
        self.machine.add_transition(trigger='props_parsed', source='props', dest='sim', before='print_empty_line')
111
112
113
114
        self.machine.add_transition(trigger='sim_finished', source='sim', dest='sim', before='print_empty_line')

        # define what happens when input is received in a certain state
        self.stateDependentInputHandling = {
115
            'greeting': self.greeting_handle_input,
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
            'dimensions': self.dimensions_handle_input,
            'domain': self.domain_handle_input,
            'unknowns': self.unknowns_handle_input,
            'parameters': self.parameters_handle_input,
            'pdes': self.pdes_handle_input,
            'bcs': self.bcs_handle_input,
            'props': self.props_handle_input,
            'sim': self.sim_handle_input,
        }

        # for ladder-like views
        self.viewfrom = OrderedDict([
            ('domain', "mDomain"),
            ('unknowns', "mUnknown"),
            ('parameters', "mParameter"),
            ('pdes', "mPDE"),
            ('bcs', "mBCsRequired"),
            ('props', "mEllipticLinearDirichletBoundaryValueProblem"),
            ('sim', "mSolvability"),
        ])
        # to include all the necessary theories every time
        self.bgthys = OrderedDict([
138
            ('domain', ["mInterval", "http://mathhub.info/MitM/smglom/arithmetics?RealArithmetics"]),
139
            # new: RealArithmetics
140
141
142
            ('unknowns', ["http://mathhub.info/MitM/Foundation?Strings", "ephdomain"]),
                          #"http://mathhub.info/MitM/smglom/calculus?higherderivative"]),
            ('parameters', ["http://mathhub.info/MitM/smglom/arithmetics?RealArithmetics", "ephdomain",
143
                            "http://mathhub.info/MitM/Foundation?Math"]),
144
            ('pdes', ["mDifferentialOperators", "mFunctionArithmetics"]),  # +params, unknowns,
145
            ('bcs',
146
             ["ephdomain", "mLinearity", "mDifferentialOperators",
147
              "http://mathhub.info/MitM/smglom/arithmetics?RealArithmetics"]),  # +params, unknowns, pdes, bctypes
148
149
            ('props',
             ["mLinearity",
150
              "http://mathhub.info/MitM/Foundation?Strings"]),  # +bcs, pde
151
            ('sim',
152
             ["http://mathhub.info/MitM/Foundation?Strings"]),  # +props
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
        ])

        # the things we'd like to find out
        self.simdata = {
            "num_dimensions": None,
            "domain": {
                "name": None,
                "theoryname": None,
                # "viewname" : None,
                "axes": OrderedDict(),
                "from": None,
                "to": None,
            },
            "unknowns": OrderedDict(),
            "parameters": OrderedDict(),
            "pdes": {
                #               "theoryname": None,
                "pdes": [],
            },
            "bcs": {
                "theoryname": None,
                "bcs": None,
            },
            "props": {

            },
179
            "sim": {
180
181
182
183
                "type": None,
            },
        }

184
185
        self.exaout = None

186
187
188
189
190
191
192
        self.install_run = install_run

        if self.install_run:
            self.mmtinterface = None
        else:
            self.mmtinterface = MMTInterface()

193
        #with MMTInterface() as self.mmtinterface:
194
        """Variables to signal callbacks depending on yes/no prompts"""
195
196
197
        self.prompted = False
        self.if_yes = None
        self.if_no = None
198
199
        self.pass_other = False

200
201
202
203
204
205
206
207
208
    def handle_state_dependent_input(self, userstring):
        """The standard input handling, depending on which state we are in"""
        # pythonic switch-case, cf. https://bytebaker.com/2008/11/03/switch-case-statement-in-python/
        try:
            self.stateDependentInputHandling[self.state](userstring)
        except Exception as error:
            #self.exaout.create_output(self.simdata)
            raise

209
210
    def greeting_handle_input(self, userstring):
        self.greeting_over()
211

212
    def greeting_exit(self):
213
        # username = getpass.getuser()
Theresa Pollinger's avatar
mosis    
Theresa Pollinger committed
214
        # self.poutput("Hello, " + username + "! I am MoSIS, your partial differential equations and simulations expert. "
215
216
217
218
219
220
221
222
223
224
        #              "Let's set up a simulation together.")
        # self.poutput("")
        # self.poutput("To get explanations, enter \"explain <optional keyword>\". ")
        # self.poutput("To see a recap of what we know so far, enter \"recap <optional keyword>\". ")
        # self.poutput("To interactively visualize ther current theory graph, enter \"tgwiev <optional theory name>\". ")
        # self.poutput("Otherwise, you can always try and use LaTeX-type input.")
        # self.poutput("")
        # self.poutput("You can inspect the currently loaded MMT theories under " + self.mmtinterface.serverInstance)
        # self.poutput("")
        return
225

226
227
    ##### for state dimensions
    def dimensions_begin(self):
228
        self.print_subheading("Modeling")
229
        self.poutput("How many dimensions does your model have?")
230
        self.print_empty_line()
231
        self.poutput("I am just assuming it's 1, since that is all we can currently handle.")  # TODO
232
        self.print_empty_line()
233
234
235
236
237
238
239
240
241
242
243
244
245
246
247
        self.simdata["num_dimensions"] = 1
        self.dimensions_parsed()

    def dimensions_handle_input(self, userstring):
        # reply_diffops = self.mmtinterface.query_for("mDifferentialOperators")
        # self.poutput(reply_diffops.tostring())
        # self.poutput(element_to_string(reply_diffops.getConstant("derivative")))
        # self.poutput(element_to_string(reply_diffops.getConstant("laplace_operator")))
        try:
            numdim = int(userstring)
        except ValueError:
            self.poutput("Please enter a number.")
            return
        if numdim < 1:
            self.obviously_stupid_input()
248
            ExaOutput(self.testsimdata)
249
250
251
252
253
254
255
256
257
258
            self.dimensions_begin()
        elif numdim == 1:  # or self.numdim == 2:
            self.simdata["num_dimensions"] = numdim
            self.dimensions_parsed()
        else:
            self.poutput(
                "Sorry, cannot handle " + str(numdim) + " dimensions as of now. Please try less than that.")

    ##### for state domain
    def domain_begin(self):
259
        self.poutput("What is the domain in your model?     Ω : type ❘ = [?;?], e.g. `\\\\Omega = [0.0;1.0]`")
260
        # self.poutput("By the way, you can always try and use LaTeX-type input.")
261
262
263
264
        self.simdata[self.state]["axes"] = OrderedDict()
        self.domain_mmt_preamble()

    def domain_handle_input(self, userstring):
265
        domain_name = string_handling.get_first_word(userstring)
266
        # subdict = self.simdata[self.state]
267
        with CriticalSubdict(self.simdata[self.state], self.poutput) as subdict:
268
269
270
271
272
            parsestring = userstring
            mmtreply = self.mmtinterface.mmt_new_decl(domain_name, subdict["theoryname"], parsestring)
            mmttype = self.mmtinterface.mmt_infer_type(subdict["theoryname"], domain_name)
            if mmttype.inferred_type_to_string() != "type":
                raise InterviewError("This seems to not be a type. It should be!")
273
            result = self.mmtinterface.query_for(subdict["theoryname"])
274
            subdict["name"] = domain_name
275
            (fro, to) = mmtreply.getIntervalBoundaries(result, domain_name)
276
            subdict["axes"]["x"] = "[" + str(fro) + ";" + str(to) + "]"
277
278
            (subdict["from"], subdict["to"]) = (fro, to)

279
            self.poutput("we will just assume that the variable is called " + string_handling.get_first_key(subdict["axes"]) + " for now.")
280
281
282
283
284
285
286
287
288
            # mmtreply = self.mmtinterface.mmt_new_decl(domain_name, subdict["theoryname"], "x : " + domain_name)
            self.trigger('domain_parsed')

    def domain_exit(self):
        self.domain_mmt_postamble()

    def domain_mmt_preamble(self):
        # set the current MMT theoryname for parsing the input TODO use right dimension
        self.simdata[self.state]["theoryname"] = "ephdomain"
289
290
291

        if not self.install_run:
            self.new_theory(self.simdata[self.state]["theoryname"])
292
293
294
        # (ok, root) = self.mmtinterface.query_for(self.simdata[self.state]["theoryname"])

    def domain_mmt_postamble(self):
295
        with CriticalSubdict(self.simdata[self.state], self.poutput) as subdict:
296
            subdict["boundary_name"] = subdict["name"]  # todo
297
298
299
300
301
            if not self.cheating:
                self.mmtinterface.mmt_new_decl('mydomainpred', subdict["theoryname"],
                                               "myDomainPred = " + subdict["name"] + ".interval_pred")
                self.mmtinterface.mmt_new_decl('mydomain', subdict["theoryname"],
                                               "myDomain = intervalType " + subdict["name"])
302
                # and a view to understand our interval as a domain -- view ephDomainAsDomain : ?GeneralDomains ⟶ ?ephDomain =
303
304
305
306
307
308
309
310
311
312
313
314
315
316
317
                self.new_view(subdict)
                self.mmtinterface.mmt_new_decl('Vecspace', subdict["viewname"],
                                               "Vecspace = real_lit")  # TODO adjust for higher dimensions
                self.mmtinterface.mmt_new_decl('DomainPred', subdict["viewname"], "DomainPred = " + subdict[
                    "name"] + ".interval_pred")  # the . is unbound, apparently...
            else:
                self.new_view(subdict)
                self.mmtinterface.mmt_new_decl('dom', subdict["viewname"],
                                               "domain = " + subdict["name"])
                self.mmtinterface.mmt_new_decl('boun', subdict["viewname"],
                                               "boundary = " + subdict["boundary_name"])

    ##### for state unknowns
    def unknowns_begin(self):
        self.poutput("Which variable(s) are you looking for? / What are the unknowns in your model?  u : " +
318
                     self.simdata["domain"]["name"] + " ⟶ ??,  e.g., u : " + self.simdata["domain"]["name"] + " ⟶ ℝ ?")
319
320
321
        self.simdata["unknowns"] = OrderedDict()

    def unknowns_handle_input(self, userstring):
322
        unknown_name = string_handling.get_first_word(userstring)
323
324
325
326
327
        # replace interval with domain
        parsestring = (
            userstring.replace(self.simdata["domain"]["name"],
                               "pred myDomainPred") if not self.cheating else userstring)

328
        with CriticalSubdict(self.simdata[self.state], self.poutput) as usubdict:
329
330
331
332
333
334
335
336
337
338
            # create mmt theory with includes
            once = self.new_theory(unknown_name)
            # self.include_in(unknown_name, self.simdata["domain"]["theoryname"])

            # and one to "throw away" to infer the type
            self.new_theory(unknown_name + "_to_go_to_trash")
            test = self.mmtinterface.mmt_new_decl(unknown_name, unknown_name + "_to_go_to_trash",
                                                  parsestring)

            type = self.get_inferred_type(unknown_name + "_to_go_to_trash", unknown_name)
339
            #type = self.get_inferred_type(parsestring, unknown_name) #TODO in a smarter way
340
341
342
343
            usubdict[unknown_name] = {
                "theoryname": unknown_name,
                "string": parsestring,
                "type": type,
344
                "codomain": type.replace(self.simdata["domain"]["name"] + " ⟶", "", 1).strip(),
345
            }
346
            with CriticalSubdict(self.simdata["unknowns"][unknown_name], self.poutput, False) as subdict:
347
348
                if self.mmtinterface.query_for(unknown_name + "_to_go_to_trash").hasDefinition(unknown_name):
                    raise InterviewError("Unknowns cannot be defined!")
349
                if not string_handling.type_is_function_from(subdict["type"], self.simdata["domain"]["name"]):
350
351
352
353
354
355
356
357
358
359
360
                    raise InterviewError("Unknown should be a function on " + self.simdata["domain"]["name"] + "!")

                # add unknown's type as constant
                twice = self.mmtinterface.mmt_new_decl(unknown_name, subdict["theoryname"],
                                                       "myUnkType = " + subdict["type"])
                twice = (self.mmtinterface.mmt_new_decl('diffable', subdict["theoryname"],
                                                        "anyuwillbediffable : {u : myUnkType} ⊦ twodiff u ") if not self.cheating else twice)
                self.new_view(subdict)
                self.mmtinterface.mmt_new_decl("codomain", subdict["viewname"], "ucodomain = " + subdict["codomain"])
                self.mmtinterface.mmt_new_decl("unktype", subdict["viewname"], "unknowntype = myUnkType")
                self.poutput("Ok, " + userstring)
361
                # self.please_prompt("Are these all the unknowns?", lambda: self.trigger('unknowns_parsed'), pass_other=True) #TODO
362
363
364
                self.trigger('unknowns_parsed')

    def unknowns_exit(self):
365
366
367
368
369
        # TODO do this once we can do more than one
        # for unknown in self.simdata["unknowns"]:
        #    self.poutput(self.simdata["unknowns"][unknown]["string"])
        # self.print_empty_line()
        return
370
371
372

    ##### for state parameters
    def parameters_begin(self):
373
        self.print_empty_line()
374
        self.poutput(
375
            "Would you like to name additional parameters like constants or functions (that are independent of your \
376
            unknowns)?  c : ℝ = ? or f : Ω ⟶ ℝ = ?, e.g. `k = x \\cdot x`")  # ℝ
377
378
379
380
        self.simdata["parameters"] = OrderedDict()

    def parameters_handle_input(self, userstring):
        # self.poutput ("parameterinput "+ userstring)
381
        if string_handling.means_no(userstring):
382
383
384
            self.trigger('parameters_parsed')
            return

385
        parameter_name = string_handling.get_first_word(userstring)
386
387
388
        with CriticalSubdict(self.simdata["parameters"], self.poutput) as psubdict:
            psubdict[parameter_name] = {}
            with CriticalSubdict(self.simdata["parameters"][parameter_name], self.poutput, False) as subdict:
389
390
391
                # create mmt theory
                self.new_theory(parameter_name)
                # we might need the other parameters created so far, so use them
392
                for otherparamentry in string_handling.get_recursively(self.simdata["parameters"], "theoryname"):
Theresa Pollinger's avatar
Theresa Pollinger committed
393
394
                    if otherparamentry in userstring:
                        self.include_in(parameter_name, otherparamentry)
395
396

                # sanitize userstring - check if this works for all cases
397
                parsestring = string_handling.add_ods(userstring)
398
399
                if parsestring.startswith(parameter_name + "(") or parsestring.startswith(
                        parameter_name + " ("):  # todo make smarter for more dimensions
400
401
                    parsestring = string_handling.remove_apply_brackets(parsestring)
                parsestring = string_handling.functionize(parsestring, self.simdata["domain"]["name"])
402
                # self.poutput(parsestring)
403
404
405

                # add the quantitiy role for display as MPD
                reply_pconstant = self.mmtinterface.mmt_new_decl("param", parameter_name, parsestring +
406
                                                                 string_handling.object_delimiter + " role Quantity")
407
408
409
410
411
412
413
414
415
416
417
418
                reply_pconstant = self.mmtinterface.query_for(parameter_name)
                subdict["theoryname"] = parameter_name
                subdict["string"] = userstring
                subdict["parsestring"] = parsestring
                subdict["type"] = self.get_inferred_type(parameter_name, parameter_name)

                # if not reply_pconstant.hasDefinition(parameter_name) and not self.cheating:
                #    InterviewError("Please define this parameter.")

                # create view
                self.new_view(subdict)
                self.mmtinterface.mmt_new_decl("ptype", subdict["viewname"],
419
                                               "ptype = " + subdict["type"])
420
                self.mmtinterface.mmt_new_decl("param", subdict["viewname"],
421
                                               "param = " + parameter_name)
422
                self.poutput("Ok, " + parsestring)
423
                self.print_empty_line()
424
425
                self.please_prompt("Would you like to declare more parameters?", None,
                                   lambda: self.trigger('parameters_parsed'), True)
426
427
428
429
430

    def parameters_exit(self):
        # print(str(self.simdata["parameters"]))
        for parameter in self.simdata["parameters"]:
            self.poutput(self.simdata["parameters"][parameter]["string"])
431
        self.print_empty_line()
432
433
434
435

    ##### for state pdes
    def pdes_begin(self):
        self.poutput(
436
            "Let's talk about your partial differential equation(s). What do they look like? e.g. `Δu = 0.0` ?")
437
438
439
        self.simdata["pdes"]["pdes"] = []

    def pdes_handle_input(self, userstring):
440
441
442
        with CriticalSubdict(self.simdata["pdes"]["pdes"], self.poutput) as psubdict:
            psubdict.append({})
            with CriticalSubdict(self.simdata["pdes"]["pdes"][-1], self.poutput, False) as subdict:
443
                subdict["theoryname"] = "ephemeral_pde" + str(len(self.simdata["pdes"]["pdes"]))
444
                # create new theory including all unknowns and parameters
445
                self.new_theory(subdict["theoryname"])
446
                for unknownentry in string_handling.get_recursively(self.simdata["unknowns"], "theoryname"):
447
                    self.include_in(subdict["theoryname"], unknownentry)
448
                for paramentry in string_handling.get_recursively(self.simdata["parameters"], "theoryname"):
449
                    self.include_in(subdict["theoryname"], paramentry)
450
451
452
453
454
455
456
457
458
459

                # TODO use symbolic computation to order into LHS and RHS
                parts = re.split("=", userstring)

                if len(parts) is not 2:
                    raise InterviewError("This does not look like an equation.")

                # store the info
                subdict["string"] = userstring
                subdict["lhsstring"] = parts[0].strip()
460
                subdict["rhsstring"] = parts[1].strip()
461
                subdict["rhsstring_expanded"] = self.try_expand(subdict["rhsstring"])  # TODO expand properly
462
463

                # to make the left-hand side a function on x, place " [ variablename : domainname ] " in front
Theresa Pollinger's avatar
Theresa Pollinger committed
464
                lambda_x = " [ x : " + self.simdata["domain"]["name"] + " ] "
465
                if "x" in parts[0]:
Theresa Pollinger's avatar
Theresa Pollinger committed
466
                    parts[0] = lambda_x + parts[0]
467
                # right-hand side: infer type, make function if not one yet
468
                if not string_handling.type_is_function_from(self.get_inferred_type(subdict["theoryname"], parts[1]),
469
                                             self.simdata["domain"]["name"]):
Theresa Pollinger's avatar
Theresa Pollinger committed
470
                    parts[1] = lambda_x + parts[1]
471
472

                # in lhs replace all unknown names used by more generic ones and add lambda clause in front
473
                for unkname in string_handling.get_recursively(self.simdata["unknowns"], "theoryname"):
474
475
476
477
                    parts[0] = parts[0].replace(unkname, " any" + unkname)
                    parts[0] = " [ any" + unkname + " : " + self.simdata["unknowns"][unkname]["type"] + " ] " + parts[0]
                    # and include the original ones as theory
                    inc = self.include_in(subdict["theoryname"], unkname)
478
                for parname in string_handling.get_recursively(self.simdata["parameters"], "theoryname"):
479
480
481
482
483
484
485
486
487
488
489
490
                    inc = self.include_in(subdict["theoryname"], parname)

                # send declarations to mmt
                self.mmtinterface.mmt_new_decl("lhs", subdict["theoryname"], " mylhs = " + parts[0])
                reply_lhsconstant = self.mmtinterface.query_for(subdict["theoryname"])

                self.mmtinterface.mmt_new_decl("rhs", subdict["theoryname"], " myrhs = " + parts[1])
                reply_rhsconstant = self.mmtinterface.query_for(subdict["theoryname"])

                # create view
                self.new_view(subdict)
                ltype = self.get_inferred_type(subdict["theoryname"], "mylhs")
491
                eqtype = string_handling.get_last_type(ltype)
492
493
                rtype = self.get_inferred_type(subdict["theoryname"], "myrhs")
                self.mmtinterface.mmt_new_decl("eqtype", subdict["viewname"],
494
                                               "eqtype = " + eqtype)
495
                self.mmtinterface.mmt_new_decl("lhs", subdict["viewname"],
496
                                               "lhs = " + "mylhs")
497
                self.mmtinterface.mmt_new_decl("rhs", subdict["viewname"],
498
                                               "rhs = " + "myrhs")
499
                self.mmtinterface.mmt_new_decl("pde", subdict["viewname"],
500
                                               "pde = " + "[u](mylhs u) ≐ myrhs")
501
502
503

                reply = self.mmtinterface.query_for(subdict["theoryname"])

504
                for unkname in string_handling.get_recursively(self.simdata["unknowns"], "theoryname"):
505
506
507
508
509
510
511
512
513
514
515
                    op = subdict["lhsstring"].replace(unkname, "")
                    op = op.strip()

                # store the info
                subdict["op"] = op
                subdict["lhsparsestring"] = parts[0]
                subdict["rhsparsestring"] = parts[1]

                # TODO query number of effective pdes and unknowns from mmt for higher dimensional PDEs
                # => can assume each to be ==1 for now
                numpdesgiven = len(self.simdata["pdes"]["pdes"])
516
517
                # self.poutput("Ok, this is what this looks like in omdoc: " + reply.tostring())
                self.toggle_show_button("Show PDE as omdoc", escape(reply.tostring())) #TODO
518
519
520
521
522
523
                if numpdesgiven == len(self.simdata["unknowns"]):
                    self.trigger('pdes_parsed')
                elif numpdesgiven > len(self.simdata["unknowns"]):
                    self.poutput("now that's too many PDEs. Please go back and add more unknowns.")
                else:
                    self.poutput("More PDEs, please!")
524
525
526
527
528
529
530

    def pdes_exit(self):
        self.poutput("These are all the PDEs needed.")

    ##### for state bcs
    def bcs_begin(self):
        self.poutput("Let's discuss your boundary conditions. "
531
                     "What do they look like? u = f or u(" + str(self.simdata["domain"]["to"]) + ") = \\alpha ?")
532
        with CriticalSubdict(self.simdata["bcs"], self.poutput) as subdict:
533
534
535
536
            subdict["theoryname"] = "ephbcs"
            subdict["bcs"] = []
            self.new_theory(subdict["theoryname"])
            # apparently, need to include everything explicitly so that view works
537
            for unknownentry in string_handling.get_recursively(self.simdata["unknowns"], "theoryname"):
538
                self.include_in(subdict["theoryname"], unknownentry)
539
540
541
            # generate the concretely typted boundary conditions for each unknown
            self.add_bc_structs(subdict["theoryname"])

542
            for paramentry in string_handling.get_recursively(self.simdata["parameters"], "theoryname"):
543
                self.include_in(subdict["theoryname"], paramentry)
544
            for pdeentry in string_handling.get_recursively(self.simdata["pdes"], "theoryname"):
545
546
547
548
549
                self.include_in(subdict["theoryname"], pdeentry)
            self.new_view(subdict)
            subdict["measure_given"] = 0

    def bcs_handle_input(self, userstring):
550
        with CriticalSubdict(self.simdata["bcs"], self.poutput) as subdict:
551
552
553
554
555
556
557
558
559
560
            currentname = "bc" + str(len(subdict["bcs"]))
            subdict["bcs"].append({"name": currentname})
            # TODO use symbolic computation to order into LHS and RHS
            parts = re.split("=", userstring)

            if len(parts) is not 2:
                raise InterviewError("This does not look like a boundary condition.")
            # store the info
            subdict["bcs"][-1]["string"] = userstring
            subdict["bcs"][-1]["lhsstring"] = parts[0].strip()
561
            subdict["bcs"][-1]["rhsstring"] = parts[1].strip()  # TODO expand
562
563
            subdict["bcs"][-1]["rhsstring_expanded"] = self.try_expand(subdict["bcs"][-1]["rhsstring"])

564
            domain_boundary_name = self.simdata["domain"]['boundary_name']
565
            # to make a function on x, place " [ variablename : boundaryname ] " in front
566
            if "x" in parts[0]:
567
                parts[0] = " [ x : " + domain_boundary_name + " ] " + parts[0]
568
            if "x" in parts[1]:
569
                parts[1] = " [ x : " + domain_boundary_name + " ] " + parts[1]
570

571
            first_pde_theory_name = self.simdata["pdes"]['pdes'][0]['theoryname']
572
            # in lhs replace all unknown names used by more generic ones and add lambda clause in front
573
            for unkname in string_handling.get_recursively(self.simdata["unknowns"], "theoryname"):
574
575
576
                parts[0] = parts[0].replace(unkname, " any" + unkname)
                parts[0] = " [ any" + unkname + " : " + self.simdata["unknowns"][unkname]["type"] + " ] " + parts[0]

577
578
                type = self.get_inferred_type(first_pde_theory_name, parts[0])
                bc_type_struct_name = unkname + "_boundary_types"
579
                if string_handling.type_is_function_to(type, self.simdata["unknowns"][unkname]["type"]):
580
                    # right-hand side: infer type, make function if not one yet
581
                    rhstype = self.get_inferred_type(first_pde_theory_name, parts[1])
582
                    if not string_handling.type_is_function_from(rhstype, self.simdata["domain"]["name"]) \
583
584
585
                            and not string_handling.type_is_function_from(rhstype,
                                                                          self.simdata["domain"]["boundary_name"]):
                        parts[1] = " [ x : " + domain_boundary_name + " ] " + parts[1]
586
587
588
589
590
591
592
593
594
595
596
597
598
599
600
                    #self.add_list_of_declarations(subdict["viewname"], [
                    #    "firstBC = " + bc_type_struct_name + "/DirichletBCfun " + parts[1], #TODO
                    #    "secondBC = " + bc_type_struct_name + "/DirichletBCfun " + parts[1],
                    #])
                    try:
                        self.mmtinterface.mmt_new_decl("first", subdict["viewname"], "firstBC = " + bc_type_struct_name +
                                                                        "/DirichletBCfun " + parts[1])
                    except MMTServerError as error:#TODO!!
                        pass
                    try:
                        self.mmtinterface.mmt_new_decl("second", subdict["viewname"], "secondBC = " + bc_type_struct_name +
                                                                        "/DirichletBCfun " + parts[1])
                    except MMTServerError as error:#TODO!!
                        pass

601
602
603
604
                    subdict["bcs"][-1]["type"] = "Dirichlet",
                    subdict["bcs"][-1]["on"] = "x",
                    subdict["bcs"][-1]["measure"] = 2,
                    subdict["measure_given"] = 2
605
                elif string_handling.type_is_function_to(type, self.simdata["unknowns"][unkname]["codomain"]):
606
                    # at_x = re.split('[\(\)]', subdict["bcs"][-1]["lhsstring"])[-1] #TODO
607
                    at_x = subdict["bcs"][-1]["lhsstring"].split('(', 1)[1].split(')')[0].strip()
608
                    if at_x != self.simdata["domain"]["from"] and at_x != self.simdata["domain"]["to"]:
609
610
611
                        raise InterviewError(at_x + " is not on the boundary!")
                    if len(subdict["bcs"]) == 1:
                        self.mmtinterface.mmt_new_decl("bc1", subdict["viewname"],
612
                                                       "firstBC = solutionat " + at_x + " is " + parts[1])#TODO struct workaround
613
614
                    elif len(subdict["bcs"]) == 2:
                        self.mmtinterface.mmt_new_decl("bc2", subdict["viewname"],
615
                                                       "secondBC = solutionat " + at_x + " is " + parts[1])
616
617
618
619
620
621
622
                    else:
                        raise InterviewError("too many boundary conditions saved")
                    subdict["measure_given"] += 1
                    subdict["bcs"][-1]["type"] = "Dirichlet",
                    subdict["bcs"][-1]["on"] = at_x,
                    subdict["bcs"][-1]["measure"] = 1,

623
            # try:
624
625
            #    type = self.get_inferred_type(subdict["theoryname"], "[u : Ω ⟶ ℝ] u(0.0)")
            #    type = self.get_inferred_type(subdict["theoryname"], "[u : Ω ⟶ ℝ] u")
626
            # except MMTServerError as error:
627
628
629
            #    self.poutput(error.args[0])

            self.poutput("Ok ")
630
            if subdict["measure_given"] == len(self.simdata["unknowns"]) * 2:  # TODO times inferred order of PDE
631
632
633
                self.trigger('bcs_parsed')
            elif subdict["measure_given"] > len(self.simdata["unknowns"]):
                raise InterviewError("now that's too many boundary conditions. ignoring last input.")
634
635
            else:
                self.poutput("Please enter more boundary conditions")
636
637
638

    def bcs_exit(self):
        self.poutput("These are all the boundary conditions needed.")
639
        self.print_empty_line()
640

641
    def add_bc_structs(self, bc_theory_name):
642
        for unknown in string_handling.get_recursively(self.simdata["unknowns"], "theoryname"):
643
644
645
646
647
648
649
650
            self.add_list_of_declarations(bc_theory_name, [
                "structure " + unknown + "_boundary_types : ?mBCTypes =" +
                    "include " + string_handling.assert_question_mark("mUnknown") + " = " +
                        string_handling.assert_question_mark(self.simdata['unknowns'][unknown]['viewname']) +
                        string_handling.declaration_delimiter +
                    "include ?mDifferentialOperators = ?mDifferentialOperators" + string_handling.declaration_delimiter +
                string_handling.module_delimiter
            ])
651
652
653

    ##### for state props
    def props_begin(self):
654
        with CriticalSubdict(self.simdata["props"], self.poutput) as subdict:
655
656
657
            # TODO try to find out things about the solvability ourselves
            subdict["theoryname"] = "ephBoundaryValueProblem"
            self.new_theory(subdict["theoryname"])
658
            # apparently, need to include everything explicitly so that view works
659
            for unknownentry in string_handling.get_recursively(self.simdata["unknowns"], "theoryname"):
660
                self.include_in(subdict["theoryname"], unknownentry)
661
            for paramentry in string_handling.get_recursively(self.simdata["parameters"], "theoryname"):
662
                self.include_in(subdict["theoryname"], paramentry)
663
            for pdeentry in string_handling.get_recursively(self.simdata["pdes"], "theoryname"):
664
665
666
667
668
669
670
                self.include_in(subdict["theoryname"], pdeentry)
            self.include_in(subdict["theoryname"], self.simdata["bcs"]["theoryname"])
            self.new_view(subdict)
            self.include_trivial_assignment(subdict["viewname"], "mDifferentialOperators")
            self.include_trivial_assignment(subdict["viewname"], "mLinearity")

            subdict["ops"] = []
671
672
            for pde in self.simdata["pdes"]["pdes"]:
                self.poutput("Do you know something about the operator " + pde["op"] + "? "
673
674
675
676
                                                                                       "Is it e.g. linear, or not elliptic ? ")
                subdict["ops"].append({})
                subdict["ops"][-1]["name"] = pde["op"]
                subdict["ops"][-1]["props"] = []
677
678

    def props_handle_input(self, userstring):
679
        if string_handling.means_no(userstring):
680
681
682
            self.trigger("props_parsed")
            return

683
        with CriticalSubdict(self.simdata["props"], self.poutput) as subdict:
684
685
            #            "linear": True, #or false or unknown
            #            "props": ["elliptic"]
686

687
            parsestring = userstring.replace("not", "¬")
688

689
            if "linear" in parsestring:
690
                self.add_list_of_declarations(subdict["theoryname"], [
691
                    string_handling.add_ods("user_linear : ⊦ " + parsestring + ' mylhs = sketch "user knowledge" ')
692
                ])
693
                if "¬" in parsestring:
694
695
696
697
698
699
                    subdict["ops"][-1]["linear"] = False
                else:
                    subdict["ops"][-1]["linear"] = True
                    self.add_list_of_declarations(subdict["viewname"], [
                        "isLinear = user_linear"
                    ])
700
                self.poutput("OK!")
701
702

            for property in ["elliptic"]:  # TODO more properties
703
                if property in parsestring:
704
                    self.add_list_of_declarations(subdict["theoryname"], [
705
                        string_handling.add_ods("user_" + property + " : ⊦ " + parsestring + ' mylhs = sketch "user knowledge" ')
706
                    ])
707
                    subdict["ops"][-1]["props"].append(parsestring)
708
                    if "¬" not in parsestring:
709
710
711
                        self.add_list_of_declarations(subdict["viewname"], [
                            "isElliptic = user_elliptic"
                        ])
712
                    self.poutput("OK!")
713
714
715
            self.poutput("do you know anything else?")

    def props_exit(self):
716
        # TODO totality check on the view from uniquelysolvable to ephBoundaryValueProblem
717
718
719
720
        return

    ##### for state sim
    def sim_begin(self):
721
        self.recap()
722
        self.print_subheading("Solving")
723
        self.please_prompt("Would you like to try and solve the PDE using the Finite Difference Method in ExaStencils? "
724
                           "If yes, you can provide a configuration name, or we'll just use your name.",
725
                           if_yes=self.sim_ok_fd, if_no=None, pass_other=True)
726
727

    def sim_handle_input(self, userstring):
728
        self.sim_exit(userstring)
729

730
731
732
733
734
    def sim_ok_fd(self):
        self.sim_exit()

    def sim_exit(self, problem_name=None):
        self.simdata["sim"]["type"] = "FiniteDifferences"
735
        # generate output
736
        self.exaout = ExaOutput(self.simdata, getpass.getuser(), problem_name)
737
        print("Generated ExaStencils input; running ExaStencils")
738
        self.toggle_show_button("Show .exa1 code", self.exaout.l1_string)
739
        # generate and run simulation
740
        runner = ExaRunner(self.exaout)
741
742
743
744
745
746
747
748
        runner.run_exastencils()
        print("Ran ExaStencils; preparing visualization")
        # output
        self.display_result_as_bokeh()

    # cf. nbviewer.jupyter.org/github/bokeh/bokeh-notebooks/blob/master/tutorial/01 - Basic Plotting.ipynb
    def display_result_as_bokeh(self):

749
750
        unknowns = [*self.simdata["unknowns"]]

751
752
753
        # create a new plot with default tools, using figure
        p = figure(plot_width=1000, plot_height=400)

754
755
756
        runner = ExaRunner(self.exaout)
        data = runner.load_data(unknowns[0])  # TODO more dimensions
        source = ColumnDataSource(data=data)
757
758
759
760
        source.data = source.from_df(data)
        source.add(data.index, 'index')

        # add a circle renderer with a size, color, and alpha
761
        p.circle(x='index', y=unknowns[0], size=2, line_color="navy", fill_color="orange", fill_alpha=0.5, source=source)
762
763
764
765
766
767
768
        #show(p)

        output_notebook()
        # cf. http://bokeh.pydata.org/en/0.10.0/docs/user_guide/embed.html
        self.display_html(file_html(p, CDN, "my plot"))  # show the results

        # using JS requires jupyter widgets extension
769
770
771
        # script, div = components(p)
        # div = notebook_div(p)
        # self.Display(Javascript(script + div))  # show the results
772

773
    def generate_mpd_theories(self):
774
        with CriticalSubdict(self.simdata[self.state], self.poutput):
775
776
777
778
779
780
781
782
783
784
            # generate the Quantity of a hypothetical solution to an unknown
            for unknownentry in string_handling.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"]
                    + string_handling.object_delimiter + " role Quantity"
                ])

785
            # generate Laws that define the parameters, if applicable
786
            for paramentry in string_handling.get_recursively(self.simdata["parameters"], "theoryname"):
787
788
789
790
791
792
                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("=", "≐")
793
                        + string_handling.object_delimiter + " role Law"
794
795
                    ])

796
            # generate the Laws that define it, namely boundary conditions and PDEs
797
798
799
800
            pde_names = string_handling.get_recursively(self.simdata["pdes"], "theoryname")
            for pde_number in range(len(pde_names)):
                mpd_theory_name = "MPD_pde" + str(pde_number)
                pde = self.simdata["pdes"]["pdes"][pde_number]
801
                self.mmtinterface.mmt_new_theory(mpd_theory_name)
802
                self.include_in(mpd_theory_name, pde_names[pde_number])
803

Theresa Pollinger's avatar
Theresa Pollinger committed
804
                # include all the mpd_unknowns, and parameters
805

806
                for paramentry in string_handling.get_recursively(self.simdata["parameters"], "theoryname"):
807
808
                    if paramentry in pde['string']:
                        self.include_in(mpd_theory_name, paramentry)
809

Theresa Pollinger's avatar
Theresa Pollinger committed
810
811
812
813
814
815
816
                for unknownentry in string_handling.get_recursively(self.simdata["unknowns"], "theoryname"):
                    # TODO make more robust + rework for more unknowns
                    self.include_in(mpd_theory_name, "MPD_" + unknownentry)
                    self.add_list_of_declarations(mpd_theory_name, [
                        str("proof_" + str(pde_number) + " : ⊦ " + pde["lhsstring"].replace(unknownentry, " " + unknownentry)
                            + " ≐ " + pde["rhsparsestring"] + string_handling.object_delimiter + " role Law")
                    ])
817

818
        with CriticalSubdict(self.simdata[self.state], self.poutput):
819
820
821
822
823
824
825
826
827
828
829
830
831
            mpd_theory_name = "MPD_bcs"
            self.mmtinterface.mmt_new_theory(mpd_theory_name)
            for unknownentry in string_handling.get_recursively(self.simdata["unknowns"], "theoryname"):
                self.include_in(mpd_theory_name, "MPD_" + unknownentry)
            self.include_in(mpd_theory_name, self.simdata["bcs"]["theoryname"])

            for bc in self.simdata["bcs"]["bcs"]:
                for paramentry in string_handling.get_recursively(self.simdata["parameters"], "theoryname"):
                    if paramentry in bc['string']:
                        self.include_in(mpd_theory_name, paramentry)
                self.add_list_of_declarations(mpd_theory_name, [
                    str("proof_" + bc['name'] + " : ⊦ " + bc['lhsstring'] + " ≐ " + bc["rhsstring"] +
                        string_handling.object_delimiter + " role BoundaryCondition")
832
833
                ])

834
        with CriticalSubdict(self.simdata[self.state], self.poutput):
835
836
            # make an actual model theory that includes all of the Laws declared so far,
            # which in turn include the Quantities
837
            modelname = "MPD_Model"
838
            self.mmtinterface.mmt_new_theory(modelname)
839
            for paramentry in string_handling.get_recursively(self.simdata["parameters"], "theoryname"):
840
                self.include_in(modelname, "MPD_" + paramentry)
841
842
843
            for pde_number in range(len(pde_names)):
                self.include_in(modelname, "MPD_pde" + str(pde_number))
            self.include_in(modelname, "MPD_bcs")
844
845
846

            return modelname

847
    # functions for user interaction
848
849
850
851
852
    def obviously_stupid_input(self):
        self.poutput("Trying to be funny, huh?")

    # mmt input helper functions
    def include_in(self, in_which_theory, what):
853
854
        return self.mmtinterface.mmt_new_decl("inc", in_which_theory,
                                              "include " + string_handling.assert_question_mark(what))
855
856
857
858
859
860

    def add_list_of_declarations(self, in_which_theory, declaration_list):
        for declaration in declaration_list:
            self.mmtinterface.mmt_new_decl("inc", in_which_theory, declaration)

    def include_bgthys(self, in_which_theory):
861
        """Includes all the background theories specified in self.bgthys for the current state"""
862
863
864
865
866
867
        ok = True
        for bgthy in self.bgthys[self.state]:
            ok = ok and self.include_in(in_which_theory, bgthy)
        return ok

    def new_theory(self, thyname):
868
869
        self.mmtinterface.mmt_new_theory(thyname)
        return self.include_bgthys(thyname)
870
871

    def new_view(self, dictentry):
872
873
        """Constructs a new entry 'viewname' into the given dictionary and creates the view,
        including all applicable former views"""
874
875
        dictentry["viewname"] = self.construct_current_view_name(dictentry)
        # self.poutput("new view: "+dictentry["viewname"])
876
877
878
879
880
        self.mmtinterface.mmt_new_view(dictentry["viewname"], self.viewfrom[self.state], dictentry["theoryname"])
        return self.include_former_views(dictentry["viewname"])

    def include_former_views(self, current_view_name):
        """recursively look for all views already done and try to include them into the current view."""
881
        for viewstring in string_handling.get_recursively(self.simdata, "viewname"):
882
            if (current_view_name != viewstring):
883
                try:
884
                    self.include_in(current_view_name,
885
                                    "?" + string_handling.split_string_at_AS(viewstring)[-1] + " = " + "?" + viewstring)
886
887
888
                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
889
                    expected_str = "no backend available that is applicable to " + self.mmtinterface.namespace
Theresa Pollinger's avatar
Theresa Pollinger committed
890
                    if expected_str not in error.args[0]:
891
892
893
894
895
896
897
898
                        raise

    def construct_current_view_name(self, dictentry):
        return self.construct_view_name(dictentry, self.state)

    def construct_view_name(self, dictentry, state):
        return dictentry["theoryname"] + "AS" + (self.viewfrom[state])

899
    def include_trivial_assignment(self, in_view, theoryname):
900
        self.include_in(in_view, string_handling.assert_question_mark(theoryname) + " = " + string_handling.assert_question_mark(theoryname))
901

902
903
904
    def get_inferred_type(self, in_theory, term):
        return self.mmtinterface.mmt_infer_type(in_theory, term).inferred_type_to_string()

905
906
    def try_expand(self, term,
                   in_theory=None):  # TODO do using mmt definition expansion, issue UniFormal/MMT/issues/295
907
        for param in reversed(self.simdata["parameters"]):
908
            if param in term:
909
910
911
912
913
914
915
916
                parts = self.simdata["parameters"][param]["string"].split("=")
                if (len(parts) != 2):
                    raise InterviewError("no definition for " + param + " given")
                paramdef = parts[-1]
                term = term.replace(param, paramdef.strip())
        return term

    def print_empty_line(self):
917
        self.poutput("\n\n")  # double to actually make it a Markdown newline
918

919
920
921
922
    def print_subheading(self, heading):
        self.poutput("## " + heading)
        self.print_empty_line()

923
    def explain(self, userstring=None):  # TODO
924
925
926
927
        with CriticalSubdict({}, self.poutput):
            reply = self.mmtinterface.query_for(
                "http://mathhub.info/smglom/calculus/nderivative.omdoc?nderivative?nderivative")
            self.poutput(reply.tostring())
928

929
    def recap(self, userstring=None):  # TODO
930
        self.print_simdata()
931
        self.print_empty_line()
932
        # self.poutput("You can inspect the persistently loaded MMT theories under " + self.mmtinterface.mmt_frontend_base_url)
Theresa Pollinger's avatar
Theresa Pollinger committed
933
        #TODO
934
935

    def print_simdata(self):
936
        self.poutput("These are the things we know so far about your problem:")
937
938
939
        for s in reversed(self.states):
            state_name = s.name
            if state_name in self.simdata:
940
941
                self.print_empty_line()
                self.print_empty_line()
942
943
                self.poutput(state_name + ": " + str(self.simdata[state_name]))
            if state_name == self.state:
944
                self.print_empty_line()
945
946
                return

947