#!/usr/bin/env python3 # http://cmd2.readthedocs.io import cmd2 as cmd # https://github.com/pytransitions/transitions from transitions import Machine, State from collections import OrderedDict # strings: # http://mattoc.com/python-yes-no-prompt-cli.html from distutils.util import strtobool from pathlib import Path # https://github.com/phfaist/pylatexenc for directly converting Latex commands to unicode from pylatexenc.latex2text import LatexNodes2Text import pyparsing as pp import re from string_handling import * from exaoutput import ExaOutput from mmtinterface import * class InterviewError(Exception): def __init__(self, err): self.error = err super(InterviewError, self).__init__("Interview error: " + str(self.error)) ###For the part of the simdata whose contents will be cleaned up if there was an error ###to be used in with statements class CriticalSubdict(): def __init__(self, subdict): self.subdict = subdict self.initial_subdict = self.subdict.copy() def __enter__(self): return self.subdict def __exit__(self, type, value, traceback): if type is not None: #restore the initial state self.subdict.clear() for key in self.initial_subdict: self.subdict[key] = self.initial_subdict[key] print(value) if isinstance(value, MMTServerError) or isinstance(value, InterviewError): self.please_repeat(value.args[0]) return True else: return False return True def please_repeat(self, moreinfo=None): append = "" if moreinfo: append = "\nDetails: " + moreinfo print("I did not catch that. Could you please rephrase?" + append) # This "main class" is two things: a REPL loop, by subclassing the cmd2 Cmd class # and a state machine as given by the pytransitions package class Interview(cmd.Cmd): def __init__(self, *args, **kwargs): # just act like we were getting the right replies from MMT self.cheating = True # initialize legal characters for cmd self.legalChars = u'!#$%.:;?@_-<>' + pp.printables + pp.alphas8bit + pp.punc8bit # TODO why does "<" not show? # allow all useful unicode characters to be used, and some more for i in range(0x20, 0x2E7F): self.legalChars += chr(i) # call cmd constructor super(Interview, self).__init__(*args, **kwargs) # Initialize a state machine states = [ # State('greeting'), 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']), ] states.reverse() self.machine = Machine(model=self, states=states, initial=states[-1], after_state_change='update_prompt') # 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() # self.machine.add_transition(trigger='greeting_over', source='greeting', dest='dimensions') 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') self.machine.add_transition(trigger='unknowns_parsed', source='unknowns', dest='parameters', after='print_empty_line') self.machine.add_transition(trigger='parameters_parsed', source='parameters', dest='pdes', after='print_empty_line') self.machine.add_transition(trigger='pdes_parsed', source='pdes', dest='bcs', before='print_empty_line') self.machine.add_transition(trigger='bcs_parsed', source='bcs', dest='sim', before='print_empty_line') #self.machine.add_transition(trigger='props_parsed', source='props', dest='sim', before='print_empty_line')#TODO props self.machine.add_transition(trigger='sim_finished', source='sim', dest='sim', before='print_empty_line') # Initialize cmd member variables self.myname = 'TheInterview' self.username = 'user' self.intro = "Hello, " + self.username + "! I am " + self.myname + ", your partial differential equations and simulations expert. " \ "Let's set up a simulation together.\n" \ "How many dimensions does your model have?" # define what happens when input is received in a certain state self.stateDependentInputHandling = { '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, } self.mmtinterface = MMTInterface() # 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([ ('domain', ["mInterval", "http://mathhub.info/MitM/smglom/arithmetics?realarith"]), # new: RealArithmetics ('unknowns', ["http://mathhub.info/MitM/Foundation?Strings", "ephdomain", "http://mathhub.info/MitM/smglom/calculus?higherderivative"]), ('parameters', ["http://mathhub.info/MitM/smglom/arithmetics?realarith", "ephdomain", "http://mathhub.info/MitM/Foundation?Math"]), ('pdes', ["mDifferentialOperators"]),#+params, unknowns, ('bcs', ["ephdomain", "mLinearity", "http://mathhub.info/MitM/smglom/arithmetics?realarith"]),#+params, unknowns, pdes, bctypes ('props', ["mLinearity", "http://mathhub.info/MitM/Foundation?Strings"]), #+bcs, pde ('sim', ["http://mathhub.info/MitM/Foundation?Strings"]), #+props ]) # 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": { }, "sim" : { "type": None, }, } axes = OrderedDict([ ("x_1", "[0;1]"), ]) self.examplesimdata = { "num_dimensions": 1, "domain": { "name": "Ω", "theoryname": "Omega", "axes": axes, # names and intervals "from": 0.0, "to": 1.0, }, "unknowns": { # names and theorynames #TODO OrderedDict "u": { "theoryname": "u", "string": "u : Ω → ℝ", }, }, "parameters": { # names and theorynames "μ": { "theoryname": "mu", "string": "μ : ℝ = 1", }, "f": { "theoryname": "f", "string": "f : Ω → ℝ = [x] x ⋅ x", }, }, "pdes": { "pdes": [ { "theoryname": "pde1", "string": "μ ∆u = f(x)", # TODO use function arithmetic 'lhsstring': 'μ Δu ', 'rhsstring': 'f(x)', 'op': 'Δ', 'lhsparsestring': ' [ anyu : Ω → ℝ ] Δ anyu ', 'rhsparsestring': ' [ x : Ω ] f(x)', # this is more of a wish list... cf https://github.com/UniFormal/MMT/issues/295 "expanded": "μ d²/dx_1² u = f(x_1)", "order_in_unknown": { "u": 2, }, }, ], }, "bcs": { "theoryname": "ephbcs", "bcs": [ { "name": "bc1", "type": "Dirichlet", "string": "u (0) = x_1**2", "on": "0", }, { "name": "bc2", "type": "Dirichlet", "string": "u (1) = x_1**2", "on": "1", }, ], }, "props": { "theoryname": "ephboundaryvalueproblem", "ops": [ { "name": "op1", "linear": True, #or false or unknown "props": ["elliptic"] } ] }, "sim":{ "type": "FD", }, } self.testsimdata = { 'num_dimensions': 1, 'domain': {'name': 'Ω', 'theoryname': 'ephdomain', 'axes': OrderedDict([('x_1', '[0.0;1.0]')]), 'from': 0.0, 'to': 1.0, 'boundary_name': 'Ω', 'viewname': 'ephdomainASmDomain'}, 'unknowns': OrderedDict([('u', {'theoryname': 'u', 'string': 'u : Ω → ℝ', 'type': 'Ω → ℝ', 'codomain': 'ℝ', 'viewname': 'uASmUnknown'})]), 'parameters': { 'f': {'theoryname': 'f', 'string': 'f = x', 'parsestring': 'f = [ x : Ω] x', 'type': '{ : Ω } Ω', 'viewname': 'fASmParameter'}}, 'pdes': {'pdes': [ {'theoryname': 'ephpde1', 'string': 'Δu = 0.0', 'lhsstring': 'Δu', 'rhsstring': '0.0', 'viewname': 'ephpde1ASmPDE', 'op': 'Δ', 'lhsparsestring': ' [ anyu : Ω → ℝ ] Δ anyu ', 'rhsparsestring': ' [ x : Ω ] 0.0'}]}, 'bcs': {'theoryname': 'ephbcs', 'bcs': [ {'name': 'bc0', 'string': 'u = f', 'lhsstring': 'u ', 'rhsstring': ' f', 'type': ('Dirichlet',), 'on': ('x',), 'measure': (2,)}], 'bctypes': {'theoryname': 'uBCTypes'}, 'viewname': 'ephbcsASmBCsRequired', 'measure_given': 2}, 'props': {}, 'sim': {}, } self.exaout = ExaOutput() # self.greeting() self.update_prompt() self.prompted = False self.if_yes = None self.if_no = None ##### for state dimensions def dimensions_begin(self): self.poutput("How many dimensions does your model have?") self.poutput("I am just assuming it's 1, since that is all we can currently handle.") # TODO 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() self.exaout.create_output(self.testsimdata) 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): self.poutput("What is the domain you would like to simulate for? Ω : type ❘ = [?;?], e.g. Ω = [0.0;1.0]") self.poutput("By the way, you can always try and use LaTeX-type input.") self.simdata[self.state]["axes"] = OrderedDict() self.domain_mmt_preamble() def domain_handle_input(self, userstring): domain_name = get_first_word(userstring) # subdict = self.simdata[self.state] with CriticalSubdict(self.simdata[self.state]) as subdict: 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!") result = self.mmtinterface.query_for(subdict["theoryname"]) # if not self.cheating else #print(result.tostring()) subdict["name"] = domain_name (fro, to) = mmtreply.getIntervalBoundaries(result, domain_name) #if not self.cheating else (0.0, 1.0) # todo make work again subdict["axes"]["x_1"] = "[" + str(fro) + ";" + str(to) + "]" (subdict["from"], subdict["to"]) = (fro, to) self.poutput("we will just assume that the variable is called x for now.") # 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): with CriticalSubdict(self.simdata[self.state]) as subdict: subdict["boundary_name"] = subdict["name"] #todo 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"]) # and a view to understand our interval as a domain -- view ephDomainAsDomain : ?GeneralDomains → ?ephDomain = 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 : " + self.simdata["domain"]["name"] + " → ??, e.g., u : " + self.simdata["domain"]["name"] + " → ℝ ?") self.simdata["unknowns"] = OrderedDict() def unknowns_handle_input(self, userstring): unknown_name = get_first_word(userstring) # replace interval with domain parsestring = ( userstring.replace(self.simdata["domain"]["name"], "pred myDomainPred") if not self.cheating else userstring) with CriticalSubdict(self.simdata[self.state]) as usubdict: # 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) usubdict[unknown_name] = { "theoryname": unknown_name, "string": parsestring, "type": type, "codomain": type.replace(self.simdata["domain"]["name"] + " →", "", 1).strip(), } with CriticalSubdict(self.simdata["unknowns"][unknown_name]) as subdict: if self.mmtinterface.query_for(unknown_name + "_to_go_to_trash").hasDefinition(unknown_name): raise InterviewError("Unknowns cannot be defined!") if not type_is_function_from(subdict["type"], self.simdata["domain"]["name"]): 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) #if self.please_prompt("Are these all the unknowns?"): #TODO self.trigger('unknowns_parsed') def unknowns_exit(self): for unknown in self.simdata["unknowns"]: self.poutput(self.simdata["unknowns"][unknown]["string"]) ##### for state parameters def parameters_begin(self): self.poutput( "Would you like to name additional parameters like constants or functions (that are independent of your unknowns)? c : ℝ = ? or f : Ω → ℝ = ?") # ℝ self.simdata["parameters"] = OrderedDict() def parameters_handle_input(self, userstring): # self.poutput ("parameterinput "+ userstring) if means_no(userstring): self.trigger('parameters_parsed') return parameter_name = get_first_word(userstring) self.simdata["parameters"][parameter_name] = {} with CriticalSubdict(self.simdata["parameters"][parameter_name]) as subdict: # create mmt theory self.new_theory(parameter_name) # we might need the other parameters created so far, so use them for otherparamentry in get_recursively(self.simdata["parameters"], "theoryname"): self.include_in(parameter_name, otherparamentry) # sanitize userstring - check if this works for all cases parsestring = add_ods(userstring) if parsestring.startswith(parameter_name + "(") or parsestring.startswith(parameter_name + " ("):#todo make smarter for more dimensions parsestring = remove_apply_brackets(parsestring) parsestring = functionize(parsestring, self.simdata["domain"]["name"]) # self.poutput(parsestring) reply_pconstant = self.mmtinterface.mmt_new_decl("param", parameter_name, parsestring) 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"], "ptype = " + subdict["type"]) self.mmtinterface.mmt_new_decl("param", subdict["viewname"], "param = " + parameter_name) self.poutput("Ok, " + parsestring) self.please_prompt("Are these all the parameters?", lambda: self.trigger('parameters_parsed')) def parameters_exit(self): # print(str(self.simdata["parameters"])) for parameter in self.simdata["parameters"]: self.poutput(self.simdata["parameters"][parameter]["string"]) ##### 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): self.simdata["pdes"]["pdes"].append({}) with CriticalSubdict(self.simdata["pdes"]["pdes"][-1]) as subdict: subdict["theoryname"] = "ephpde" + str(len(self.simdata["pdes"]["pdes"])) self.new_theory(subdict["theoryname"]) # 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() subdict["rhsstring"] = parts[1].strip()#TODO expand subdict["rhsstring_expanded"] = self.try_expand(subdict["rhsstring"]) # to make the left-hand side a function on x, place " [ variablename : domainname ] " in front if parts[0].find("x") > -1: parts[0] = " [ x : " + self.simdata["domain"]["name"] + " ] " + parts[0] # right-hand side: infer type, make function if not one yet if not type_is_function_from(self.get_inferred_type(subdict["theoryname"], parts[1]), self.simdata["domain"]["name"]): parts[1] = " [ x : " + self.simdata["domain"]["name"] + " ] " + parts[1] # in lhs replace all unknown names used by more generic ones and add lambda clause in front for unkname in get_recursively(self.simdata["unknowns"], "theoryname"): 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) for parname in get_recursively(self.simdata["parameters"], "theoryname"): 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") eqtype = get_last_type(ltype) rtype = self.get_inferred_type(subdict["theoryname"], "myrhs") self.mmtinterface.mmt_new_decl("eqtype", subdict["viewname"], "eqtype = " + eqtype) self.mmtinterface.mmt_new_decl("lhs", subdict["viewname"], "lhs = " + "mylhs") self.mmtinterface.mmt_new_decl("rhs", subdict["viewname"], "rhs = " + "myrhs") self.mmtinterface.mmt_new_decl("pde", subdict["viewname"], "pde = " + "[u](mylhs u) funcEq myrhs") reply = self.mmtinterface.query_for(subdict["theoryname"]) for unkname in get_recursively(self.simdata["unknowns"], "theoryname"): 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!") 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. " "What do they look like? u(x) = f(x) or u(" + str(self.simdata["domain"]["to"]) + ") = \\alpha ?") #TODO remove square brakcets bctypetheoryname = self.redefine_bcs() with CriticalSubdict(self.simdata["bcs"]) as subdict: subdict["theoryname"] = "ephbcs" subdict["bcs"] = [] self.new_theory(subdict["theoryname"]) # apparently, need to include everything explicitly so that view works for unknownentry in get_recursively(self.simdata["unknowns"], "theoryname"): self.include_in(subdict["theoryname"], unknownentry) for paramentry in get_recursively(self.simdata["parameters"], "theoryname"): self.include_in(subdict["theoryname"], paramentry) for pdeentry in get_recursively(self.simdata["pdes"], "theoryname"): self.include_in(subdict["theoryname"], pdeentry) self.include_in(subdict["theoryname"], bctypetheoryname) self.new_view(subdict) subdict["measure_given"] = 0 def bcs_handle_input(self, userstring): with CriticalSubdict(self.simdata["bcs"]) as subdict: 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() subdict["bcs"][-1]["rhsstring"] = parts[1].strip()#TODO expand subdict["bcs"][-1]["rhsstring_expanded"] = self.try_expand(subdict["bcs"][-1]["rhsstring"]) # to make a function on x, place " [ variablename : boundaryname ] " in front if parts[0].find("x") > -1: parts[0] = " [ x : " + self.simdata["domain"]['boundary_name'] + " ] " + parts[0] if parts[1].find("x") > -1: parts[1] = " [ x : " + self.simdata["domain"]['boundary_name'] + " ] " + parts[1] # in lhs replace all unknown names used by more generic ones and add lambda clause in front for unkname in get_recursively(self.simdata["unknowns"], "theoryname"): parts[0] = parts[0].replace(unkname, " any" + unkname) parts[0] = " [ any" + unkname + " : " + self.simdata["unknowns"][unkname]["type"] + " ] " + parts[0] type = self.get_inferred_type(subdict["theoryname"], parts[0]) if type_is_function_to(type, self.simdata["unknowns"][unkname]["type"]): # right-hand side: infer type, make function if not one yet rhstype = self.get_inferred_type(subdict["theoryname"], parts[1]) if not type_is_function_from(rhstype, self.simdata["domain"]["name"])\ and not type_is_function_from(rhstype, self.simdata["domain"]["boundary_name"]): parts[1] = " [ x : " + self.simdata["domain"]["boundary_name"] + " ] " + parts[1] self.add_list_of_declarations(subdict["viewname"], [ "firstBC = myDirichletBCfun " + parts[1], "secondBC = myDirichletBCfun " + parts[1], ]) subdict["bcs"][-1]["type"] = "Dirichlet", subdict["bcs"][-1]["on"] = "x", subdict["bcs"][-1]["measure"] = 2, subdict["measure_given"] = 2 elif type_is_function_to(type, self.simdata["unknowns"][unkname]["codomain"]): #at_x = re.split('[\(\)]', subdict["bcs"][-1]["lhsstring"])[-1] #TODO at_x = subdict["bcs"][-1]["lhsstring"].split('(', 1)[1].split(')')[0].strip() if not at_x is self.simdata["domain"]["from"] or at_x is self.simdata["domain"]["to"]: raise InterviewError(at_x + " is not on the boundary!") if len(subdict["bcs"]) == 1: self.mmtinterface.mmt_new_decl("bc1", subdict["viewname"], "firstBC = solutionat " + at_x + " is " + parts[1]) elif len(subdict["bcs"]) == 2: self.mmtinterface.mmt_new_decl("bc2", subdict["viewname"], "secondBC = solutionat " + at_x + " is " + parts[1]) #TODO store at and type 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, #try: # type = self.get_inferred_type(subdict["theoryname"], "[u : Ω → ℝ] u(0.0)") # type = self.get_inferred_type(subdict["theoryname"], "[u : Ω → ℝ] u") #except MMTServerError as error: # self.poutput(error.args[0]) self.poutput("Ok ") if subdict["measure_given"] == len(self.simdata["unknowns"])*2: #TODO times order self.trigger('bcs_parsed') elif subdict["measure_given"] > len(self.simdata["unknowns"]): raise InterviewError("now that's too many boundary conditions. ignoring last input.") def bcs_exit(self): self.poutput("These are all the boundary conditions needed.") def redefine_bcs(self): for unknown in get_recursively(self.simdata["unknowns"], "theoryname"): with CriticalSubdict(self.simdata["bcs"]) as subdict: 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", ] ) err = """when trying to include include ?mDomain = ?ephdomainASmDomain and all others in view info.kwarc.mmt.api.InvalidObject of level 2 invalid object (ill-formed morphism: expected http://mathhub.info/MitM/smglom/calculus?mDomain -> (http://cds.omdoc.org/urtheories?ModExp?complextheory [] ), found http://mathhub.info/MitM/smglom/calculus?mDomain -> http://mathhub.info/MitM/smglom/calculus?ephdomain): http://mathhub.info/MitM/smglom/calculus?ephdomainASmDomain info.kwarc.mmt.api.checking.MMTStructureChecker.checkMorphism(MMTStructureChecker.scala:535) info.kwarc.mmt.api.checking.MMTStructureChecker.checkRealization(MMTStructureChecker.scala:545) info.kwarc.mmt.api.checking.MMTStructureChecker.check(MMTStructureChecker.scala:187) info.kwarc.mmt.api.checking.MMTStructureChecker.applyElementBegin(MMTStructureChecker.scala:57) info.kwarc.mmt.interviews.InterviewServer$$anon$1.onElement(InterviewServer.scala:94) info.kwarc.mmt.api.parser.KeywordBasedParser.seCont(StructureParser.scala:96) info.kwarc.mmt.api.parser.KeywordBasedParser.addDeclaration$1(StructureParser.scala:481) info.kwarc.mmt.api.parser.KeywordBasedParser.readInModuleAux(StructureParser.scala:525) info.kwarc.mmt.api.parser.KeywordBasedParser.readInModule(StructureParser.scala:461) info.kwarc.mmt.interviews.InterviewServer.parseDecl(InterviewServer.scala:102) info.kwarc.mmt.interviews.InterviewServer.apply(InterviewServer.scala:50) info.kwarc.mmt.api.web.Server.resolveExtension(Server.scala:95) info.kwarc.mmt.api.web.Server.resolve(Server.scala:76) info.kwarc.mmt.api.web.Server.handleRequest(Server.scala:53) info.kwarc.mmt.api.web.TiscafServerImplementation$RequestHandler$$anon$1.act(TiscafServerImplementation.scala:49) tiscaf.HSimpleLet.aact(HLet.scala:166) tiscaf.HSimpleLet.aact$(HLet.scala:165) info.kwarc.mmt.api.web.TiscafServerImplementation$RequestHandler$$anon$1.aact(TiscafServerImplementation.scala:47) tiscaf.HAcceptor.talk(HAcceptor.scala:246) tiscaf.HSimplePeer.doTalkItself$1(HPeer.scala:101) tiscaf.HSimplePeer.$anonfun$readChannel$1(HPeer.scala:114) scala.runtime.java8.JFunction0$mcV$sp.apply(JFunction0$mcV$sp.java:12) scala.concurrent.Future$.$anonfun$apply$1(Future.scala:653) scala.util.Success.$anonfun$map$1(Try.scala:251) scala.util.Success.map(Try.scala:209) scala.concurrent.Future.$anonfun$map$1(Future.scala:287) scala.concurrent.impl.Promise.liftedTree1$1(Promise.scala:29) scala.concurrent.impl.Promise.$anonfun$transform$1(Promise.scala:29) scala.concurrent.impl.CallbackRunnable.run(Promise.scala:60) tiscaf.sync.SyncQuExecutionContext$$anon$1.run(SyncQuExecutionContext.scala:69) """#TODO #viewname = bctypetheoryname + "ASmBCTypes" #subdict["bctypes"]["viewname"] = viewname #self.mmtinterface.mmt_new_view(viewname, bctypetheoryname, "mBCTypes") #self.add_list_of_declarations(viewname, # ["DirichletBC = myDirichletBC ", # #" = myDirichletBCfun" # ]) return bctypetheoryname # Todo adapt for more than 1 ##### for state props def props_begin(self): with CriticalSubdict(self.simdata["props"]) as subdict: # TODO try to find out things about the solvability ourselves subdict["theoryname"] = "ephBoundaryValueProblem" self.new_theory(subdict["theoryname"]) #self.new_view(subdict) for pde in self.simdata["pdes"]["pdes"]: self.poutput("Do you know something about the operator " + pde["op"] + "? " "Is it e.g. linear, or not elliptic ? ") def props_handle_input(self, userstring): if means_no(userstring): self.trigger("props_parsed") return with CriticalSubdict(self.simdata["props"]) as subdict: # "props": { # "theoryname": "ephboundaryvalueproblem", # "ops": [ # { # "name": "op1", # "linear": True, #or false or unknown # "props": ["elliptic"] # } # ] #}, #parts = re.split(" ", userstring) #TODO can add arbitrary proofs of undefined terms?? parsestring = userstring.replace("not", "¬") for property in ["linear", "elliptic"]: if parsestring.find(property) > -1: self.add_list_of_declarations(subdict["theoryname"], [ "user_" + property + " : ⊦ " + parsestring + " mylhs" ]) self.poutput("OK!") self.poutput("do you know anything else?") def props_exit(self): return ##### for state sim def sim_begin(self): self.please_prompt("Would you like to try and solve the PDE using the Finite Difference Method in ExaStencils?", self.sim_ok_fd) def sim_handle_input(self, userstring): self.please_prompt("Would you like to try and solve the PDE using the Finite Difference Method in ExaStencils?", self.sim_ok_fd) def sim_exit(self): # generate output self.exaout.create_output(self.simdata) self.poutput("Generated ExaStencils input.") #TODO generate and run simulation def sim_ok_fd(self): self.simdata["sim"]["type"] = "FiniteDifferences" self.sim_exit() #### functions for user interaction def please_prompt(self, query): self.poutput(query + " [y/n]? ") val = input() if val == "": return True try: ret = strtobool(val) except ValueError: # or use as input to callback an input processing fcn..? self.poutput("Please answer with Y/n") return self.please_prompt(query) return ret def obviously_stupid_input(self): self.poutput("Trying to be funny, huh?") # mmt input helper functions def include_in(self, in_which_theory, what): return self.mmtinterface.mmt_new_decl("inc", in_which_theory, "include " + assert_question_mark(what)) def add_list_of_declarations(self, in_which_theory, declaration_list): for declaration in declaration_list: self.mmtinterface.mmt_new_decl("inc", in_which_theory, declaration) def include_bgthys(self, in_which_theory): ok = True for bgthy in self.bgthys[self.state]: ok = ok and self.include_in(in_which_theory, bgthy) return ok def new_theory(self, thyname): try: self.mmtinterface.mmt_new_theory(thyname) return self.include_bgthys(thyname) except MMTServerError as error: self.poutput(error.args[0]) # self.poutput(error.with_traceback()) raise # (ok, root) = self.mmtinterface.query_for(self.simdata[self.state]["theoryname"]) def new_view(self, dictentry): dictentry["viewname"] = self.construct_current_view_name(dictentry) # self.poutput("new view: "+dictentry["viewname"]) ok = self.mmtinterface.mmt_new_view(dictentry["viewname"], self.viewfrom[self.state], dictentry["theoryname"]) # recursively look for all views already done and try to include them for viewstring in get_recursively(self.simdata, "viewname"): if (dictentry["viewname"] != viewstring) and ok: try: ok = self.include_in(dictentry["viewname"], "?" + re.split('AS', viewstring)[-1] + " = " + "?" + viewstring) except MMTServerError as error: # self.poutput("no backend available that is applicable to " + "http://mathhub.info/MitM/smglom/calculus" + "?" + re.split('AS', dictentry["viewname"])[-1] + "?") # we are expecting errors if we try to include something that is not referenced in the source theory, so ignore them if error.args[0].find( "no backend available that is applicable to " + "http://mathhub.info/MitM/smglom/calculus" + "?" + re.split('AS', dictentry["viewname"])[-1] + "?") < 1: raise return ok def construct_current_view_name(self, dictentry): return self.construct_view_name(dictentry, self.state) def construct_view_name(self, dictentry, state): return dictentry["theoryname"] + "AS" + (self.viewfrom[state]) def get_inferred_type(self, in_theory, term): return self.mmtinterface.mmt_infer_type(in_theory, term).inferred_type_to_string() def try_expand(self, term, in_theory=None): #TODO do using mmt definition expansion for param in reversed(self.simdata["parameters"]): if term.find(param) > -1: parts = self.simdata["parameters"][param]["string"].split("=") if (len(parts) != 2): raise InterviewError("no definition for " + param + " given") paramdef = parts[-1] term = term.replace(param, paramdef.strip()) return term def print_empty_line(self): self.poutput("\n") ############# input processing if not explain or undo def default(self, line): raw = line.parsed['raw'] arg = LatexNodes2Text().latex_to_text(raw) # pythonic switch-case, cf. https://bytebaker.com/2008/11/03/switch-case-statement-in-python/ if not self.prompt_input_handling(arg): self.state_input_handling(arg) def state_input_handling(self, arg): """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](arg) except Exception as error: #self.exaout.create_output(self.simdata) raise def please_prompt(self, query, if_yes, if_no=None): self.poutput(str(query) + " [y/n]? ") self.prompted = True self.if_yes = if_yes self.if_no = if_no def prompt_input_handling(self, arg): """ If we asked for a yes-no answer, execute what was specified in please_prompt. return true if the input was handled here, and false if not.""" if self.prompted: if arg == "": self.poutput("Yes") ret = True else: try: ret = strtobool(str(arg).strip().lower()) except ValueError: # or use as input to callback an input processing fcn..? self.poutput("Please answer with Y/n") return True self.prompted = False if ret: self.if_yes() elif self.if_no is not None: self.if_no() else: return False return True return False # called when user types 'explain [expression]' def do_explain(self, expression): "Explain an expression or the theoretical background to what we are currently looking for" if expression: explanation = "hello, " + expression # TODO query flexiformal content through mmt else: explanation = 'hello' self.poutput(explanation) def help_explain(self): self.poutput('\n'.join(['explain [expression]', 'explain the expression given or the theory currently used', ])) # called when user types 'undo' def do_undo(self, expression): "Go back to the last question" self.trigger('last_state') def help_undo(self): self.poutput('\n'.join(['undo', 'Go back to the last question', ])) def update_prompt(self): self.prompt = "(" + self.state + ")" # tab completion for empty lines def completenames(self, text, line, begidx, endidx): """Override of cmd2 method which completes command names both for command completion and help.""" command = text if self.case_insensitive: command = text.lower() if not command: # define the "default" input for the different states we can be in self.stateDependentDefaultInput = { 'dimensions': '1', 'domain': ['Ω = [ 0 ; 1 ]'], 'unknowns': ['u : Ω → ℝ'], 'parameters': ['f : ℝ → ℝ = [x: ℝ] x '], # ['f : Ω → ℝ = [x:Ω] x ⋅ x'], 'pdes': ['∆u = f(x_1)'], 'bcs': ['u (0) = 0'], # ,'u (1) = x_1**2'], 'sim': ['FD'], } return self.stateDependentDefaultInput[self.state] else: # Call super class method. Need to do it this way for Python 2 and 3 compatibility cmd_completion = cmd.Cmd.completenames(self, command) # If we are completing the initial command name and get exactly 1 result and are at end of line, add a space if begidx == 0 and len(cmd_completion) == 1 and endidx == len(line): cmd_completion[0] += ' ' return cmd_completion def greeting(self): # TODO make work in proper order self.poutput( "Hello, " + self.username + "! I am " + self.myname + ", your partial differential equations and simulations expert. " \ "Let's set up a simulation together.\n") self.trigger("greeting_over") if __name__ == '__main__': Interview().cmdloop()