Skip to content
GitLab
Menu
Projects
Groups
Snippets
Help
Help
Support
Community forum
Keyboard shortcuts
?
Submit feedback
Contribute to GitLab
Sign in
Toggle navigation
Menu
Open sidebar
Theresa Pollinger
MoSIS
Commits
9124f181
Commit
9124f181
authored
Jan 16, 2018
by
Theresa Pollinger
Browse files
cheating my way through in need of better formalizations
parent
6152d5ef
Changes
2
Hide whitespace changes
Inline
Side-by-side
interview.py
View file @
9124f181
...
...
@@ -226,12 +226,11 @@ class Interview(cmd.Cmd):
mmtreply
=
self
.
mmtinterface
.
query_for
(
self
.
simdata
[
self
.
state
][
"theoryname"
])
except
MMTServerError
as
error
:
print
(
error
.
args
)
mmtparsed
=
(
mmtreply
.
ok
if
not
self
.
cheating
else
True
)
print
(
"mmtparset "
+
mmtparsed
)
mmtparsed
=
(
mmtreply
.
ok
)
# if not self.cheating else True)
if
mmtparsed
:
#(ok, root) = self.mmtinterface.query_for(self.simdata[self.state]["theoryname"])
self
.
simdata
[
self
.
state
][
"name"
]
=
domain_name
(
fro
,
to
)
=
mmtreply
.
getIntervalBoundaries
(
mmtreply
,
domain_name
)
if
not
self
.
cheating
else
(
0.
,
1.
)
(
fro
,
to
)
=
mmtreply
.
getIntervalBoundaries
(
mmtreply
,
domain_name
)
if
not
self
.
cheating
else
(
"
0.
"
,
"
1.
"
)
self
.
simdata
[
self
.
state
][
"axes"
][
"x_1"
]
=
"["
+
fro
+
";"
+
to
+
"]"
#self.poutput(self.simdata[self.state]["axes"]["x_1"])
(
self
.
simdata
[
self
.
state
][
"from"
],
self
.
simdata
[
self
.
state
][
"to"
])
=
(
"[ "
+
fro
+
" ]"
,
"[ "
+
to
+
" ]"
)
...
...
@@ -251,12 +250,13 @@ class Interview(cmd.Cmd):
def
domain_mmt_postamble
(
self
):
subdict
=
self
.
simdata
[
self
.
state
]
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...
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...
##### for state unknowns
def
unknowns_begin
(
self
):
...
...
@@ -266,7 +266,7 @@ class Interview(cmd.Cmd):
def
unknowns_handle_input
(
self
,
userstring
):
unknown_name
=
re
.
split
(
'\W+'
,
userstring
,
1
)[
0
]
# replace interval with domain
parsestring
=
userstring
.
replace
(
self
.
simdata
[
"domain"
][
"name"
],
"pred myDomainPred"
)
parsestring
=
(
userstring
.
replace
(
self
.
simdata
[
"domain"
][
"name"
],
"pred myDomainPred"
)
if
not
self
.
cheating
else
userstring
)
#print(parsestring)
#print('type: ' + str(self.get_last_type(self.get_type(parsestring))))
self
.
simdata
[
"unknowns"
][
unknown_name
]
=
{
...
...
@@ -282,12 +282,12 @@ class Interview(cmd.Cmd):
self
.
include_in
(
subdict
[
"theoryname"
],
self
.
simdata
[
"domain"
][
"theoryname"
])
#add unknown's type as constant
twice
=
self
.
mmtinterface
.
mmt_new_decl
(
unknown_name
,
subdict
[
"theoryname"
],
"myUnkType = "
+
self
.
simdata
[
"unknowns"
][
unknown_name
][
"type"
]
)
#hacky!
twice
=
self
.
mmtinterface
.
mmt_new_decl
(
'diffable'
,
subdict
[
"theoryname"
],
"anyuwillbediffable : {u : myUnkType} ⊦ twodiff u "
)
#hacky!
mmtparsed
=
twice
twice
=
(
self
.
mmtinterface
.
mmt_new_decl
(
'diffable'
,
subdict
[
"theoryname"
],
"anyuwillbediffable : {u : myUnkType} ⊦ twodiff u "
)
if
not
self
.
cheating
else
twice
)
mmtparsed
=
twice
.
ok
#add view
if
mmtparsed
:
mmtparsed
=
self
.
new_view
(
subdict
)
mmtparsed
=
mmtparsed
and
self
.
mmtinterface
.
mmt_new_decl
(
"codomain"
,
subdict
[
"viewname"
],
"ucodomain = ℝ"
)
mmtparsed
=
mmtparsed
and
self
.
mmtinterface
.
mmt_new_decl
(
"codomain"
,
subdict
[
"viewname"
],
"ucodomain = ℝ"
)
#TODO
mmtparsed
=
mmtparsed
and
self
.
mmtinterface
.
mmt_new_decl
(
"unktype"
,
subdict
[
"viewname"
],
"unknowntype = myUnkType"
)
if
mmtparsed
:
...
...
@@ -405,7 +405,7 @@ class Interview(cmd.Cmd):
def
obviously_stupid_input
(
self
):
self
.
poutput
(
"Trying to be funny, huh?"
)
#
# string processing
# string processing
def
has_equals
(
self
,
string
):
if
string
.
find
(
"="
)
>
-
1
:
return
True
...
...
mmtinterface.py
View file @
9124f181
...
...
@@ -15,9 +15,11 @@ from requests.utils import quote
from
lxml
import
etree
from
openmath
import
openmath
def
run_mmt_server
():
subprocess
.
run
([
"/home/freifrau/Desktop/masterarbeit/mmt/deploy/mmt.jar"
,
"file"
,
"server-interview.msl"
])
# TODO keep alive
# TODO keep alive - or wait for jupyter kernel
class
MMTServerError
(
Exception
):
def
__init__
(
self
,
err
):
...
...
@@ -26,9 +28,14 @@ class MMTServerError(Exception):
class
MMTReply
:
"""An object that holds
ok : whether the request was successful and
root: the returned answer, usually an etree holding the xml reply"""
def
__init__
(
self
,
ok
,
root
=
None
):
self
.
ok
=
ok
self
.
root
=
root
# print("creating reply")
# print(root)
if
isinstance
(
root
,
etree
.
_Element
):
for
element
in
root
.
iter
():
#for element in root.iter("div"): # why not entering this loop?
...
...
@@ -46,7 +53,6 @@ class MMTReply:
elements
=
self
.
getConstants
()
#print ("elements: " + str(elements))
for
element
in
elements
:
#print(element.get('name'))
if
element
.
get
(
'name'
)
==
constantname
:
return
element
...
...
Write
Preview
Markdown
is supported
0%
Try again
or
attach a new file
.
Attach a file
Cancel
You are about to add
0
people
to the discussion. Proceed with caution.
Finish editing this message first!
Cancel
Please
register
or
sign in
to comment