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"