pde_state_machine.py 51.2 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

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

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

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

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


class CriticalSubdict():
29
    def __init__(self, subdict, output_function=print, outermost=True):
30 31 32
        """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"""
33 34
        self.subdict = subdict
        self.initial_subdict = self.subdict.copy()
35 36
        self.output_function = output_function
        self.outermost = outermost
37 38 39 40 41 42

    def __enter__(self):
        return self.subdict

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

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


class PDE_States:
68 69
    """Just a state machine using pytranisitions that walks our theory graph and creates ephemeral theories and views"""

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

74
        # callback handles
75 76
        self.poutput = output_function
        self.please_prompt = prompt_function
77
        self.display_html = display_html_function
78 79

        # Initialize a state machine
80 81
        self.states = [
            State('greeting', on_exit=['greeting_exit']),
82 83 84 85 86 87 88 89 90
            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']),
        ]
91 92 93
        self.states.reverse()
        self.machine = Machine(model=self, states=self.states, initial=self.states[-1],
                               after_state_change=after_state_change_function, queued=True)
94 95 96 97
        # 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()
98
        self.machine.add_transition(trigger='greeting_over', source='greeting', dest='dimensions')
99 100 101 102
        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')
103 104
        self.machine.add_transition(trigger='unknowns_parsed', source='unknowns', dest='parameters')
        self.machine.add_transition(trigger='parameters_parsed', source='parameters', dest='pdes')
105
        self.machine.add_transition(trigger='pdes_parsed', source='pdes', dest='bcs', before='print_empty_line')
106 107
        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')
108 109 110 111
        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 = {
112
            'greeting': self.greeting_handle_input,
113 114 115 116 117 118 119 120 121 122 123 124 125 126 127 128 129 130 131 132 133 134
            '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([
135
            ('domain', ["mInterval", "http://mathhub.info/MitM/smglom/arithmetics?RealArithmetics"]),
136
            # new: RealArithmetics
137 138 139
            ('unknowns', ["http://mathhub.info/MitM/Foundation?Strings", "ephdomain"]),
                          #"http://mathhub.info/MitM/smglom/calculus?higherderivative"]),
            ('parameters', ["http://mathhub.info/MitM/smglom/arithmetics?RealArithmetics", "ephdomain",
140
                            "http://mathhub.info/MitM/Foundation?Math"]),
141
            ('pdes', ["mDifferentialOperators"]),  # +params, unknowns,
142
            ('bcs',
143
             ["ephdomain", "mLinearity", "mDifferentialOperators",
144
              "http://mathhub.info/MitM/smglom/arithmetics?RealArithmetics"]),  # +params, unknowns, pdes, bctypes
145 146
            ('props',
             ["mLinearity",
147
              "http://mathhub.info/MitM/Foundation?Strings"]),  # +bcs, pde
148
            ('sim',
149
             ["http://mathhub.info/MitM/Foundation?Strings"]),  # +props
150 151 152 153 154 155 156 157 158 159 160 161 162 163 164 165 166 167 168 169 170 171 172 173 174 175
        ])

        # 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": {

            },
176
            "sim": {
177 178 179 180
                "type": None,
            },
        }

181 182
        self.exaout = None

183 184
        self.mmtinterface = MMTInterface()
        #with MMTInterface() as self.mmtinterface:
185
        """Variables to signal callbacks depending on yes/no prompts"""
186 187 188
        self.prompted = False
        self.if_yes = None
        self.if_no = None
189 190
        self.pass_other = False

191 192 193 194 195 196 197 198 199
    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

200 201
    def greeting_handle_input(self, userstring):
        self.greeting_over()
202

203
    def greeting_exit(self):
204 205 206 207 208 209 210 211 212 213 214 215 216 217
        # username = getpass.getuser()
        # self.poutput("Hello, " + username + "! I am TheInterview, your partial differential equations and simulations expert. "
        #              "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("")
        # self.poutput("")
        # self.poutput("")
        return
218

219 220
    ##### for state dimensions
    def dimensions_begin(self):
221
        self.print_subheading("Modeling")
222
        self.poutput("How many dimensions does your model have?")
223
        self.print_empty_line()
224
        self.poutput("I am just assuming it's 1, since that is all we can currently handle.")  # TODO
225
        self.print_empty_line()
226 227 228 229 230 231 232 233 234 235 236 237 238 239 240
        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()
241
            ExaOutput(self.testsimdata)
242 243 244 245 246 247 248 249 250 251
            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):
252
        self.poutput("What is the domain in your model?     Ω : type ❘ = [?;?], e.g. `\\\\Omega = [0.0;1.0]`")
253
        # self.poutput("By the way, you can always try and use LaTeX-type input.")
254 255 256 257
        self.simdata[self.state]["axes"] = OrderedDict()
        self.domain_mmt_preamble()

    def domain_handle_input(self, userstring):
258
        domain_name = string_handling.get_first_word(userstring)
259
        # subdict = self.simdata[self.state]
260
        with CriticalSubdict(self.simdata[self.state], self.poutput) as subdict:
261 262 263 264 265
            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!")
266
            result = self.mmtinterface.query_for(subdict["theoryname"])
267
            subdict["name"] = domain_name
268
            (fro, to) = mmtreply.getIntervalBoundaries(result, domain_name)
269
            subdict["axes"]["x"] = "[" + str(fro) + ";" + str(to) + "]"
270 271
            (subdict["from"], subdict["to"]) = (fro, to)

272
            self.poutput("we will just assume that the variable is called " + string_handling.get_first_key(subdict["axes"]) + " for now.")
273 274 275 276 277 278 279 280 281 282 283 284 285
            # 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"
        self.new_theory(self.simdata[self.state]["theoryname"])
        # (ok, root) = self.mmtinterface.query_for(self.simdata[self.state]["theoryname"])

    def domain_mmt_postamble(self):
286
        with CriticalSubdict(self.simdata[self.state], self.poutput) as subdict:
287
            subdict["boundary_name"] = subdict["name"]  # todo
288 289 290 291 292
            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"])
293
                # and a view to understand our interval as a domain -- view ephDomainAsDomain : ?GeneralDomains ⟶ ?ephDomain =
294 295 296 297 298 299 300 301 302 303 304 305 306 307 308
                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 : " +
309
                     self.simdata["domain"]["name"] + " ⟶ ??,  e.g., u : " + self.simdata["domain"]["name"] + " ⟶ ℝ ?")
310 311 312
        self.simdata["unknowns"] = OrderedDict()

    def unknowns_handle_input(self, userstring):
313
        unknown_name = string_handling.get_first_word(userstring)
314 315 316 317 318
        # replace interval with domain
        parsestring = (
            userstring.replace(self.simdata["domain"]["name"],
                               "pred myDomainPred") if not self.cheating else userstring)

319
        with CriticalSubdict(self.simdata[self.state], self.poutput) as usubdict:
320 321 322 323 324 325 326 327 328 329
            # 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)
330
            #type = self.get_inferred_type(parsestring, unknown_name) #TODO in a smarter way
331 332 333 334
            usubdict[unknown_name] = {
                "theoryname": unknown_name,
                "string": parsestring,
                "type": type,
335
                "codomain": type.replace(self.simdata["domain"]["name"] + " ⟶", "", 1).strip(),
336
            }
337
            with CriticalSubdict(self.simdata["unknowns"][unknown_name], self.poutput, False) as subdict:
338 339
                if self.mmtinterface.query_for(unknown_name + "_to_go_to_trash").hasDefinition(unknown_name):
                    raise InterviewError("Unknowns cannot be defined!")
340
                if not string_handling.type_is_function_from(subdict["type"], self.simdata["domain"]["name"]):
341 342 343 344 345 346 347 348 349 350 351
                    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)
352
                # self.please_prompt("Are these all the unknowns?", lambda: self.trigger('unknowns_parsed'), pass_other=True) #TODO
353 354 355
                self.trigger('unknowns_parsed')

    def unknowns_exit(self):
356 357 358 359 360
        # 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
361 362 363

    ##### for state parameters
    def parameters_begin(self):
364
        self.print_empty_line()
365
        self.poutput(
366 367
            "Would you like to name additional parameters like constants or functions (that are independent of your \
            unknowns)?  c : ℝ = ? or f : Ω ⟶ ℝ = ?")  # ℝ
368 369 370 371
        self.simdata["parameters"] = OrderedDict()

    def parameters_handle_input(self, userstring):
        # self.poutput ("parameterinput "+ userstring)
372
        if string_handling.means_no(userstring):
373 374 375
            self.trigger('parameters_parsed')
            return

376
        parameter_name = string_handling.get_first_word(userstring)
377 378 379
        with CriticalSubdict(self.simdata["parameters"], self.poutput) as psubdict:
            psubdict[parameter_name] = {}
            with CriticalSubdict(self.simdata["parameters"][parameter_name], self.poutput, False) as subdict:
380 381 382
                # create mmt theory
                self.new_theory(parameter_name)
                # we might need the other parameters created so far, so use them
383
                for otherparamentry in string_handling.get_recursively(self.simdata["parameters"], "theoryname"):
Theresa Pollinger's avatar
Theresa Pollinger committed
384 385
                    if otherparamentry in userstring:
                        self.include_in(parameter_name, otherparamentry)
386 387

                # sanitize userstring - check if this works for all cases
388
                parsestring = string_handling.add_ods(userstring)
389 390
                if parsestring.startswith(parameter_name + "(") or parsestring.startswith(
                        parameter_name + " ("):  # todo make smarter for more dimensions
391 392
                    parsestring = string_handling.remove_apply_brackets(parsestring)
                parsestring = string_handling.functionize(parsestring, self.simdata["domain"]["name"])
393
                # self.poutput(parsestring)
394 395 396

                # add the quantitiy role for display as MPD
                reply_pconstant = self.mmtinterface.mmt_new_decl("param", parameter_name, parsestring +
397
                                                                 string_handling.object_delimiter + " role Quantity")
398 399 400 401 402 403 404 405 406 407 408 409
                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"],
410
                                               "ptype = " + subdict["type"])
411
                self.mmtinterface.mmt_new_decl("param", subdict["viewname"],
412
                                               "param = " + parameter_name)
413
                self.poutput("Ok, " + parsestring)
414
                self.print_empty_line()
415 416
                self.please_prompt("Would you like to declare more parameters?", None,
                                   lambda: self.trigger('parameters_parsed'), True)
417 418 419 420 421

    def parameters_exit(self):
        # print(str(self.simdata["parameters"]))
        for parameter in self.simdata["parameters"]:
            self.poutput(self.simdata["parameters"][parameter]["string"])
422
        self.print_empty_line()
423 424 425 426 427 428 429 430

    ##### for state pdes
    def pdes_begin(self):
        self.poutput(
            "Let's talk about your partial differential equation(s). What do they look like? Δu = 0.0, or laplace_operator Ω ℝ u = f ?")
        self.simdata["pdes"]["pdes"] = []

    def pdes_handle_input(self, userstring):
431 432 433
        with CriticalSubdict(self.simdata["pdes"]["pdes"], self.poutput) as psubdict:
            psubdict.append({})
            with CriticalSubdict(self.simdata["pdes"]["pdes"][-1], self.poutput, False) as subdict:
434
                subdict["theoryname"] = "ephemeral_pde" + str(len(self.simdata["pdes"]["pdes"]))
435
                # create new theory including all unknowns and parameters
436
                self.new_theory(subdict["theoryname"])
437
                for unknownentry in string_handling.get_recursively(self.simdata["unknowns"], "theoryname"):
438
                    self.include_in(subdict["theoryname"], unknownentry)
439
                for paramentry in string_handling.get_recursively(self.simdata["parameters"], "theoryname"):
440
                    self.include_in(subdict["theoryname"], paramentry)
441 442 443 444 445 446 447 448 449 450

                # 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()
451
                subdict["rhsstring"] = parts[1].strip()
452
                subdict["rhsstring_expanded"] = self.try_expand(subdict["rhsstring"])  # TODO expand properly
453 454

                # to make the left-hand side a function on x, place " [ variablename : domainname ] " in front
Theresa Pollinger's avatar
Theresa Pollinger committed
455
                lambda_x = " [ x : " + self.simdata["domain"]["name"] + " ] "
456
                if "x" in parts[0]:
Theresa Pollinger's avatar
Theresa Pollinger committed
457
                    parts[0] = lambda_x + parts[0]
458
                # right-hand side: infer type, make function if not one yet
459
                if not string_handling.type_is_function_from(self.get_inferred_type(subdict["theoryname"], parts[1]),
460
                                             self.simdata["domain"]["name"]):
Theresa Pollinger's avatar
Theresa Pollinger committed
461
                    parts[1] = lambda_x + parts[1]
462 463

                # in lhs replace all unknown names used by more generic ones and add lambda clause in front
464
                for unkname in string_handling.get_recursively(self.simdata["unknowns"], "theoryname"):
465 466 467 468
                    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)
469
                for parname in string_handling.get_recursively(self.simdata["parameters"], "theoryname"):
470 471 472 473 474 475 476 477 478 479 480 481
                    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")
482
                eqtype = string_handling.get_last_type(ltype)
483 484
                rtype = self.get_inferred_type(subdict["theoryname"], "myrhs")
                self.mmtinterface.mmt_new_decl("eqtype", subdict["viewname"],
485
                                               "eqtype = " + eqtype)
486
                self.mmtinterface.mmt_new_decl("lhs", subdict["viewname"],
487
                                               "lhs = " + "mylhs")
488
                self.mmtinterface.mmt_new_decl("rhs", subdict["viewname"],
489
                                               "rhs = " + "myrhs")
490
                self.mmtinterface.mmt_new_decl("pde", subdict["viewname"],
491
                                               "pde = " + "[u](mylhs u) ≐ myrhs")
492 493 494

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

495
                for unkname in string_handling.get_recursively(self.simdata["unknowns"], "theoryname"):
496 497 498 499 500 501 502 503 504 505 506 507 508 509 510 511 512 513
                    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"])
                self.poutput("Ok, " + reply.tostring())
                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!")
514 515 516 517 518 519 520

    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. "
521 522
                     "What do they look like? u(x) = f(x) or u(" + str(self.simdata["domain"]["to"]) + ") = \\alpha ?")
        with CriticalSubdict(self.simdata["bcs"], self.poutput) as subdict:
523 524 525 526
            subdict["theoryname"] = "ephbcs"
            subdict["bcs"] = []
            self.new_theory(subdict["theoryname"])
            # apparently, need to include everything explicitly so that view works
527
            for unknownentry in string_handling.get_recursively(self.simdata["unknowns"], "theoryname"):
528
                self.include_in(subdict["theoryname"], unknownentry)
529 530 531
            # generate the concretely typted boundary conditions for each unknown
            self.add_bc_structs(subdict["theoryname"])

532
            for paramentry in string_handling.get_recursively(self.simdata["parameters"], "theoryname"):
533
                self.include_in(subdict["theoryname"], paramentry)
534
            for pdeentry in string_handling.get_recursively(self.simdata["pdes"], "theoryname"):
535 536 537 538 539
                self.include_in(subdict["theoryname"], pdeentry)
            self.new_view(subdict)
            subdict["measure_given"] = 0

    def bcs_handle_input(self, userstring):
540
        with CriticalSubdict(self.simdata["bcs"], self.poutput) as subdict:
541 542 543 544 545 546 547 548 549 550
            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()
551
            subdict["bcs"][-1]["rhsstring"] = parts[1].strip()  # TODO expand
552 553
            subdict["bcs"][-1]["rhsstring_expanded"] = self.try_expand(subdict["bcs"][-1]["rhsstring"])

554
            domain_boundary_name = self.simdata["domain"]['boundary_name']
555
            # to make a function on x, place " [ variablename : boundaryname ] " in front
556
            if "x" in parts[0]:
557
                parts[0] = " [ x : " + domain_boundary_name + " ] " + parts[0]
558
            if "x" in parts[1]:
559
                parts[1] = " [ x : " + domain_boundary_name + " ] " + parts[1]
560

561
            first_pde_theory_name = self.simdata["pdes"]['pdes'][0]['theoryname']
562
            # in lhs replace all unknown names used by more generic ones and add lambda clause in front
563
            for unkname in string_handling.get_recursively(self.simdata["unknowns"], "theoryname"):
564 565 566
                parts[0] = parts[0].replace(unkname, " any" + unkname)
                parts[0] = " [ any" + unkname + " : " + self.simdata["unknowns"][unkname]["type"] + " ] " + parts[0]

567 568
                type = self.get_inferred_type(first_pde_theory_name, parts[0])
                bc_type_struct_name = unkname + "_boundary_types"
569
                if string_handling.type_is_function_to(type, self.simdata["unknowns"][unkname]["type"]):
570
                    # right-hand side: infer type, make function if not one yet
571
                    rhstype = self.get_inferred_type(first_pde_theory_name, parts[1])
572
                    if not string_handling.type_is_function_from(rhstype, self.simdata["domain"]["name"]) \
573 574 575
                            and not string_handling.type_is_function_from(rhstype,
                                                                          self.simdata["domain"]["boundary_name"]):
                        parts[1] = " [ x : " + domain_boundary_name + " ] " + parts[1]
576 577 578 579 580 581 582 583 584 585 586 587 588 589 590
                    #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

591 592 593 594
                    subdict["bcs"][-1]["type"] = "Dirichlet",
                    subdict["bcs"][-1]["on"] = "x",
                    subdict["bcs"][-1]["measure"] = 2,
                    subdict["measure_given"] = 2
595
                elif string_handling.type_is_function_to(type, self.simdata["unknowns"][unkname]["codomain"]):
596
                    # at_x = re.split('[\(\)]', subdict["bcs"][-1]["lhsstring"])[-1] #TODO
597
                    at_x = subdict["bcs"][-1]["lhsstring"].split('(', 1)[1].split(')')[0].strip()
598
                    if at_x != self.simdata["domain"]["from"] and at_x != self.simdata["domain"]["to"]:
599 600 601
                        raise InterviewError(at_x + " is not on the boundary!")
                    if len(subdict["bcs"]) == 1:
                        self.mmtinterface.mmt_new_decl("bc1", subdict["viewname"],
602
                                                       "firstBC = solutionat " + at_x + " is " + parts[1])#TODO struct workaround
603 604
                    elif len(subdict["bcs"]) == 2:
                        self.mmtinterface.mmt_new_decl("bc2", subdict["viewname"],
605
                                                       "secondBC = solutionat " + at_x + " is " + parts[1])
606 607 608 609 610 611 612
                    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,

613
            # try:
614 615
            #    type = self.get_inferred_type(subdict["theoryname"], "[u : Ω ⟶ ℝ] u(0.0)")
            #    type = self.get_inferred_type(subdict["theoryname"], "[u : Ω ⟶ ℝ] u")
616
            # except MMTServerError as error:
617 618 619
            #    self.poutput(error.args[0])

            self.poutput("Ok ")
620
            if subdict["measure_given"] == len(self.simdata["unknowns"]) * 2:  # TODO times inferred order of PDE
621 622 623
                self.trigger('bcs_parsed')
            elif subdict["measure_given"] > len(self.simdata["unknowns"]):
                raise InterviewError("now that's too many boundary conditions. ignoring last input.")
624 625
            else:
                self.poutput("Please enter more boundary conditions")
626 627 628

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

631
    def add_bc_structs(self, bc_theory_name):
632
        for unknown in string_handling.get_recursively(self.simdata["unknowns"], "theoryname"):
633 634 635 636 637 638 639 640 641 642 643 644 645 646 647 648 649 650 651 652 653 654 655 656 657 658 659 660 661 662 663 664 665 666 667 668 669 670 671 672 673
            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
            ])
#                subdict["bctypes"] = {}
#                bctypetheoryname = unknown + "BCTypes"
#                subdict["bctypes"]["theoryname"] = bctypetheoryname
#                self.new_theory(bctypetheoryname)
#                self.include_in(bctypetheoryname, unknown)
#                self.include_in(bctypetheoryname, "mDifferentialOperators")
#                self.add_list_of_declarations(bctypetheoryname,
#                                              [
#                                                  "myDirichletBC: {where: " + self.simdata["domain"][
#                                                      "boundary_name"] + ", rhs: " +
#                                                  self.simdata["unknowns"][unknown]["codomain"] + "}(" +
#                                                  self.simdata["domain"]["name"] + " ⟶ " +
#                                                  self.simdata["unknowns"][unknown]["codomain"] + ") ⟶ prop "
#                                                                                                  " ❘ = [where, rhs][u] u where ≐ rhs ❘  # solutionat 1 is 2 ",
#                                                  "myDirichletBCfun : {rhs: " + self.simdata["domain"][
#                                                      "boundary_name"] + " ⟶ " +
#                                                  self.simdata["unknowns"][unknown]["codomain"] + " }(" +
#                                                  self.simdata["domain"]["name"] + " ⟶ " +
#                                                  self.simdata["unknowns"][unknown][
#                                                      "codomain"] + ") ⟶ prop ❘ = [rhs] [u] ∀[x:" +
#                                                  self.simdata["domain"]["boundary_name"] + " ] u x ≐ rhs x "
#                                                                                            "❘ # solutionatboundaryis 1",
#                                              ]
#                                              )
#                viewname = bctypetheoryname + "ASmBCTypes"
#                subdict["bctypes"]["viewname"] = viewname
#                self.mmtinterface.mmt_new_view(viewname, "mBCTypes", bctypetheoryname)
#                self.include_former_views(viewname)
#                self.add_list_of_declarations(viewname,
#                                              ["DirichletBC = myDirichletBC ",
#                                               # " = myDirichletBCfun"
#                                               ])
#                return bctypetheoryname  # Todo adapt for more than 1
674 675 676

    ##### for state props
    def props_begin(self):
677
        with CriticalSubdict(self.simdata["props"], self.poutput) as subdict:
678 679 680
            # TODO try to find out things about the solvability ourselves
            subdict["theoryname"] = "ephBoundaryValueProblem"
            self.new_theory(subdict["theoryname"])
681
            # apparently, need to include everything explicitly so that view works
682
            for unknownentry in string_handling.get_recursively(self.simdata["unknowns"], "theoryname"):
683
                self.include_in(subdict["theoryname"], unknownentry)
684
            for paramentry in string_handling.get_recursively(self.simdata["parameters"], "theoryname"):
685
                self.include_in(subdict["theoryname"], paramentry)
686
            for pdeentry in string_handling.get_recursively(self.simdata["pdes"], "theoryname"):
687 688 689 690 691 692 693
                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"] = []
694 695
            for pde in self.simdata["pdes"]["pdes"]:
                self.poutput("Do you know something about the operator " + pde["op"] + "? "
696 697 698 699
                                                                                       "Is it e.g. linear, or not elliptic ? ")
                subdict["ops"].append({})
                subdict["ops"][-1]["name"] = pde["op"]
                subdict["ops"][-1]["props"] = []
700 701

    def props_handle_input(self, userstring):
702
        if string_handling.means_no(userstring):
703 704 705
            self.trigger("props_parsed")
            return

706
        with CriticalSubdict(self.simdata["props"], self.poutput) as subdict:
707 708
            #            "linear": True, #or false or unknown
            #            "props": ["elliptic"]
709

710
            parsestring = userstring.replace("not", "¬")
711

712
            if "linear" in parsestring:
713
                self.add_list_of_declarations(subdict["theoryname"], [
714
                    string_handling.add_ods("user_linear : ⊦ " + parsestring + ' mylhs = sketch "user knowledge" ')
715
                ])
716
                if "¬" in parsestring:
717 718 719 720 721 722
                    subdict["ops"][-1]["linear"] = False
                else:
                    subdict["ops"][-1]["linear"] = True
                    self.add_list_of_declarations(subdict["viewname"], [
                        "isLinear = user_linear"
                    ])
723
                self.poutput("OK!")
724 725

            for property in ["elliptic"]:  # TODO more properties
726
                if property in parsestring:
727
                    self.add_list_of_declarations(subdict["theoryname"], [
728
                        string_handling.add_ods("user_" + property + " : ⊦ " + parsestring + ' mylhs = sketch "user knowledge" ')
729
                    ])
730
                    subdict["ops"][-1]["props"].append(parsestring)
731
                    if "¬" not in parsestring:
732 733 734
                        self.add_list_of_declarations(subdict["viewname"], [
                            "isElliptic = user_elliptic"
                        ])
735
                    self.poutput("OK!")
736 737 738
            self.poutput("do you know anything else?")

    def props_exit(self):
739
        # TODO totality check on the view from uniquelysolvable to ephBoundaryValueProblem
740 741 742 743
        return

    ##### for state sim
    def sim_begin(self):
744
        self.recap()
745
        self.print_subheading("Solving")
746
        self.please_prompt("Would you like to try and solve the PDE using the Finite Difference Method in ExaStencils? "
747
                           "If yes, you can provide a configuration name, or we'll just use your name.",
748
                           if_yes=self.sim_ok_fd, if_no=None, pass_other=True)
749 750

    def sim_handle_input(self, userstring):
751
        self.sim_exit(userstring)
752

753 754 755 756 757
    def sim_ok_fd(self):
        self.sim_exit()

    def sim_exit(self, problem_name=None):
        self.simdata["sim"]["type"] = "FiniteDifferences"
758
        # generate output
759
        self.exaout = ExaOutput(self.simdata, getpass.getuser(), problem_name)
760 761
        print("Generated ExaStencils input; running ExaStencils")
        # generate and run simulation
762
        runner = ExaRunner(self.exaout)
763 764 765 766 767 768 769 770
        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):

771 772
        unknowns = [*self.simdata["unknowns"]]

773 774 775
        # create a new plot with default tools, using figure
        p = figure(plot_width=1000, plot_height=400)

776 777 778
        runner = ExaRunner(self.exaout)
        data = runner.load_data(unknowns[0])  # TODO more dimensions
        source = ColumnDataSource(data=data)
779 780 781 782
        source.data = source.from_df(data)
        source.add(data.index, 'index')

        # add a circle renderer with a size, color, and alpha
783
        p.circle(x='index', y=unknowns[0], size=2, line_color="navy", fill_color="orange", fill_alpha=0.5, source=source)
784 785 786 787 788 789 790
        #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
791 792 793
        # script, div = components(p)
        # div = notebook_div(p)
        # self.Display(Javascript(script + div))  # show the results
794

795
    def generate_mpd_theories(self):
796
        with CriticalSubdict(self.simdata[self.state], self.poutput):
797 798 799 800 801 802 803 804 805 806
            # 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"
                ])

807
            # generate Laws that define the parameters, if applicable
808
            for paramentry in string_handling.get_recursively(self.simdata["parameters"], "theoryname"):
809 810 811 812 813 814
                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("=", "≐")
815
                        + string_handling.object_delimiter + " role Law"
816 817
                    ])

818
            # generate the Laws that define it, namely boundary conditions and PDEs
819 820 821 822
            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]
823
                self.mmtinterface.mmt_new_theory(mpd_theory_name)
824
                self.include_in(mpd_theory_name, pde_names[pde_number])
825

Theresa Pollinger's avatar
Theresa Pollinger committed
826
                # include all the mpd_unknowns, and parameters
827

828
                for paramentry in string_handling.get_recursively(self.simdata["parameters"], "theoryname"):
829 830
                    if paramentry in pde['string']:
                        self.include_in(mpd_theory_name, paramentry)
831

Theresa Pollinger's avatar
Theresa Pollinger committed
832 833 834 835 836 837 838
                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")
                    ])
839

840
        with CriticalSubdict(self.simdata[self.state], self.poutput):
841 842 843 844 845 846 847 848 849 850 851 852 853
            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")
854 855
                ])

856
        with CriticalSubdict(self.simdata[self.state], self.poutput):
857 858
            # make an actual model theory that includes all of the Laws declared so far,
            # which in turn include the Quantities
859
            modelname = "MPD_Model"
860
            self.mmtinterface.mmt_new_theory(modelname)
861
            for paramentry in string_handling.get_recursively(self.simdata["parameters"], "theoryname"):
862
                self.include_in(modelname, "MPD_" + paramentry)
863 864 865
            for pde_number in range(len(pde_names)):
                self.include_in(modelname, "MPD_pde" + str(pde_number))
            self.include_in(modelname, "MPD_bcs")
866 867 868

            return modelname

869
    # functions for user interaction
870 871 872 873 874
    def obvious