假设我有一个任意的Coq术语(使用s-expressions / sexp的AST格式),例如:
n = n + n
我想自动将其转换为:
= n + n n
通过遍历AST树(由于sexp,它是列表的嵌套列表)。 Python中是否有可以执行此操作的标准库?
现在,如果我要写下要执行的算法/伪代码(假设我可以将sexp转换为某些实际的树对象):
def ToPolish():
'''
"postfix" tree traversal
'''
text = ''
for node in root.children:
if node is atoms:
text := text + node.text
else:
text := text + ToPolish(node,text)
return text
我认为这很接近,但我认为某处存在一个小错误...
AST示例:
(ObjList
((CoqGoal
((fg_goals
(((name 4)
(ty
(App
(Ind
(((Mutind (MPfile (DirPath ((Id Logic) (Id Init) (Id Coq))))
(DirPath ()) (Id eq))
0)
(Instance ())))
((Ind
(((Mutind (MPfile (DirPath ((Id Datatypes) (Id Init) (Id Coq))))
(DirPath ()) (Id nat))
0)
(Instance ())))
(App
(Const
((Constant (MPfile (DirPath ((Id Nat) (Id Init) (Id Coq))))
(DirPath ()) (Id add))
(Instance ())))
((Construct
((((Mutind
(MPfile (DirPath ((Id Datatypes) (Id Init) (Id Coq))))
(DirPath ()) (Id nat))
0)
1)
(Instance ())))
(Var (Id n))))
(Var (Id n)))))
(hyp
((((Id n)) ()
(Ind
(((Mutind (MPfile (DirPath ((Id Datatypes) (Id Init) (Id Coq))))
(DirPath ()) (Id nat))
0)
(Instance ())))))))))
(bg_goals ()) (shelved_goals ()) (given_up_goals ())))))
以上就是:
(ObjList
((CoqString "\
\n n : nat\
\n============================\
\n0 + n = n"))))
要么
= n + n n
使用sexp解析器:
[Symbol('Answer'), 2, [Symbol('ObjList'), [[Symbol('CoqGoal'), [[Symbol('fg_goals'), [[[Symbol('name'), 4], [Symbol('ty'), [Symbol('App'), [Symbol('Ind'), [[[Symbol('Mutind'), [Symbol('MPfile'), [Symbol('DirPath'), [[Symbol('Id'), Symbol('Logic')], [Symbol('Id'), Symbol('Init')], [Symbol('Id'), Symbol('Coq')]]]], [Symbol('DirPath'), []], [Symbol('Id'), Symbol('eq')]], 0], [Symbol('Instance'), []]]], [[Symbol('Ind'), [[[Symbol('Mutind'), [Symbol('MPfile'), [Symbol('DirPath'), [[Symbol('Id'), Symbol('Datatypes')], [Symbol('Id'), Symbol('Init')], [Symbol('Id'), Symbol('Coq')]]]], [Symbol('DirPath'), []], [Symbol('Id'), Symbol('nat')]], 0], [Symbol('Instance'), []]]], [Symbol('App'), [Symbol('Const'), [[Symbol('Constant'), [Symbol('MPfile'), [Symbol('DirPath'), [[Symbol('Id'), Symbol('Nat')], [Symbol('Id'), Symbol('Init')], [Symbol('Id'), Symbol('Coq')]]]], [Symbol('DirPath'), []], [Symbol('Id'), Symbol('add')]], [Symbol('Instance'), []]]], [[Symbol('Construct'), [[[[Symbol('Mutind'), [Symbol('MPfile'), [Symbol('DirPath'), [[Symbol('Id'), Symbol('Datatypes')], [Symbol('Id'), Symbol('Init')], [Symbol('Id'), Symbol('Coq')]]]], [Symbol('DirPath'), []], [Symbol('Id'), Symbol('nat')]], 0], 1], [Symbol('Instance'), []]]], [Symbol('Var'), [Symbol('Id'), Symbol('n')]]]], [Symbol('Var'), [Symbol('Id'), Symbol('n')]]]]], [Symbol('hyp'), [[[[Symbol('Id'), Symbol('n')]], [], [Symbol('Ind'), [[[Symbol('Mutind'), [Symbol('MPfile'), [Symbol('DirPath'), [[Symbol('Id'), Symbol('Datatypes')], [Symbol('Id'), Symbol('Init')], [Symbol('Id'), Symbol('Coq')]]]], [Symbol('DirPath'), []], [Symbol('Id'), Symbol('nat')]], 0], [Symbol('Instance'), []]]]]]]]]], [Symbol('bg_goals'), []], [Symbol('shelved_goals'), []], [Symbol('given_up_goals'), []]]]]]]
参考方案
我看了看你的庞大清单。
在顶层/根目录中,我们有:
`['Answer', 2, nested_list]`
好的,看起来'Answer'
是运算符。 'Answer'
有两个参数,2
和nested_list
因此,用英语说“ answer
到nested_list
是2
”
如果我们更深入怎么办?
['Answer', 2, ['ObjList', 'nested_list']]
好吧,现在我们有:
Answer(2, ObjList(nested_list))
更深层次的,我们看到...
['Answer',
2,
['ObjList',
[
['CoqGoal',
['list', 'list', 'list', 'list']
]
]
]
]
在我看来,您的清单清单已经按照前置顺序排列。如果没有,请确保给我一些评论。也许剩下的就是将其转换为字符串了?同样,我不确定您想要什么。
在后缀符号中,运算符(+
,*
等)也是定界符。
但是,在前缀表示法(又称“波兰语表示法”)中,更需要定界符。
输出= n + n n
非常不明确。与此相比,=(n, +(n,n))
非常清楚。
我编写了一个使用定界符(
,)
和,
的程序。但是,您可以通过设置以下内容来摆脱它们:
open_delim = ""
close_delim = ""
comma_delim = ""
在一个小的试运行中,我们有:
TEST_DATA1 = ["+", 2, ["+", 1, 1, 1] ]
# you can put **ALL** of the inputs to update_args
# inside of the constructor call. However, it is
# then very difficult to read.
loligag = Lol2Str(open_delim="(", close_delim=")")
loligag.update_args(comma_delim =",")
loligag.update_args(is_operaND= lambda x: isinstance(x, int))
loligag.update_args(is_operaTOR = lambda x: x == "+")
loligag(TEST_DATA1, file = sys.stdout)
输出为:
+(2+(1,1,1))
您可以将定界符设置为空格字符。那更像是您最初的= n + n n
示例而不是=(n, +(n, n))
loligag = Lol2Str(open_delim=" ", close_delim=" ")
loligag.update_args(comma_delim=" ")
loligag.update_args(is_operaND=lambda x: isinstance(x, int))
loligag.update_args(is_operaTOR=lambda x: x == "+")
loligag(TEST_DATA1, file=sys.stdout)
输出:
+ 2+ 1 1 1
您所有的列表元素都是符号,例如Symbol('ty')
或整数,例如4
。如果我要完全回答您的问题,那么我需要知道Symbol('ty')
之类的哪些是运算符,哪些是操作数。
如果我对您的数据运行代码...
loligag = Lol2Str(open_delim="(", close_delim=")")
loligag.update_args(comma_delim =",")
loligag.update_args(is_operaND= lambda x: isinstance(x, type(99)))
loligag.update_args(is_operaTOR = lambda x: isinstance(x, Symbol))
r = loligag(L, file = sys.stdout)
print("\nreturned: ", r)
输出是...
Answer(2ObjList((CoqGoal(fg_goals(name(4)ty(App(Ind((Mutind(MPfile(DirPath((IdLogicId(Init)Id(Coq))))DirPath([])Id(eq)),0Instance([])))(Ind(Mutind(MPfile(DirPath((IdDatatypesId(Init)Id(Coq))))DirPath([])Id(nat)),0Instance([]))App(Const((ConstantMPfile(DirPath((IdNatId(Init)Id(Coq))))DirPath([])Id(add)Instance([])))(Construct((MutindMPfile(DirPath((IdDatatypesId(Init)Id(Coq))))DirPath([])Id(nat),0),1Instance([]))Var(Id(n))))Var(Id(n)))))hyp(((Idn)[]Ind((Mutind(MPfile(DirPath((IdDatatypesId(Init)Id(Coq))))DirPath([])Id(nat)),0Instance([]))))))bg_goals([])shelved_goals([])given_up_goals([])))))
...这显然是错误的。
您有很多空列表。显然,[Symbol("+"), 1, 2, 3]
是有意义的。 [Symbol("+"), 1, [Symbol("+"), 1, 1], 3]
也是如此。但是,[Symbol("+"), 1, [], 3]
应该是什么意思?是[]
应该是操作数?
代码如下。随便玩吧。您可以忽略FileDescriptor
类。相反,我鼓励您对edit>find
__call___
attempt_write_operaTOR
write_operaNDs
class Symbol:
def __init__(i, x):
if isinstance(x, type(i)):
raise NotImplementedError()
elif isinstance(x, str):
i._stryng = x.strip()
else:
raise NotImplementedError()
def __str__(i):
return i._stryng
def __repr__(i):
return repr(i._stryng)
import io
import itertools
import sys
import random
import string
import inspect
class FileDescriptor:
"""
There is one descriptor instance
for the one Lol2Str class.
However, there are many instances
of the Lol2Str class.
when a new `Lol2Str` comes into existence
i._master_table[id(instance)] is created
Lol2Str has a custom `__del__` method
this deletes id(instance) from the master
table.
`i._master_table[id(instance)]`
is `True` if the Lol2Str instance
owns the file and is responsible
for closing it. The value is `False`
if something else closes the file.
"""
def __init__(i):
i._master_table = dict()
@classmethod
def xkey2ikey(i, xkey):
ikey = xkey
if not isinstance(xkey, type(id(i))):
ikey = id(xkey)
return ikey
def close(i, xkey):
# master_table(True, file)
# ...... there is a file, we close it.
#
# master_table(False, file)
# ..... there is a file, we do **NOT** close it
#
# master_table(False, None)
# ..... there is no file
#
# master_table(True, None)
# ...... error. we close non-existant file.
ikey = type(i).xkey2ikey(xkey)
file = i._master_table[ikey][1]
we_own = i._master_table[ikey][1]
if we_own:
file.close()
i._master_table[ikey][0] = False
i._master_table[ikey][1] = None
else:
msg = ""
raise i.FileDescriptorException(msg)
def _update_dead_kin(i, xkey):
ikey = i.xkey2ikey(xkey)
we_own_file = i._master_table[ikey][0]
if we_own_file:
file = i._master_table[ikey][0][1]
file.close()
del i._master_table[ikey]
return
@classmethod
def verify_filestream(i, new_file):
if not (hasattr(new_file, "write")):
with io.StringIO() as string_stream:
print(
object.__repr__(new_file)
,
"has no `write` method"
,
file=string_stream
)
msg = string_stream.getvalue()
raise type(i).Lol2StrException(msg)
if not callable(new_file.write):
with io.StringIO() as string_stream:
print(
object.__repr__(new_file)
,
"has no `write` method"
,
file=string_stream
)
msg = string_stream.getvalue()
raise type(i).Lol2StrException(msg)
def __get__(i, xkey, xkey_klass):
if xkey:
ikey = i.xkey2ikey(xkey)
file_is_present = i._master_table[ikey][1]
if not file_is_present:
i.set_file_to_new_string_stream(ikey)
return i.Shell(i, ikey)
else:
# called as class method instead of
# as instance method
return i
class Shell:
def __init__(i, descriptor, ikey):
i._descriptor = descriptor
i._ikey = ikey
def write(i, material):
return i._descriptor.write(i._ikey, material)
def close(i):
return i._descriptor.close(i._ikey)
def getvalue(i):
return i._descriptor.getvalue(i._ikey)
def getvalue(i, xkey):
ikey = i.xkey2ikey(xkey)
file_is_str_stream = i._master_table[ikey][0]
if file_is_str_stream:
file = i._master_table[ikey][1]
r = file.getvalue()
else:
with io.StringIO() as string_stream:
print(
"`getvalue` is only allowed if",
"user did not input their own file",
file=string_stream
)
msg = string_stream.getvalue()
raise i.FileDescriptorException(msg)
return r
def write(i, xkey, material):
ikey = i.xkey2ikey(xkey)
file = i._master_table[ikey][1]
file.write(material)
def set_file_to_new_string_stream(i, ikey):
ikey = i.xkey2ikey(loligag)
file = i._master_table[ikey][1]
# if there is a file
if file:
msg = ''.join((
"\n\nCannot create string stream when target file",
" is already present.",
"\nTarget file already set to be: ",
object.__repr__(file)
))
raise i.FileDescriptorException(msg)
# end if
file = io.StringIO()
i._master_table[ikey][0] = True
i._master_table[ikey][1] = file
return
def __set__(i, xkey, new_file):
"""
`new_file = None` is allowed
That means a different function
was called with default arguments.
The default argument for file is `None`
We cannot simply set file to a new string
stream as a default argument...
func(lol, file=io.StringIO())
... then we don't know if owner of the
file stream is the caller or callee.
"""
ikey = i.xkey2ikey(xkey)
if new_file:
# new_file is not `None`
type(i).verify_filestream(new_file)
we_own_file = i._master_table[ikey][0]
if we_own_file:
old_file = i._master_table[ikey][1]
stryng = old_file.getvalue()
new_file.write(stryng)
old_file.close()
# end-if
i._master_table[ikey][1] = new_file
i._master_table[ikey][0] = False
else:
# `new file` is `None` or `False` or `0`
# or some other such non-sense
i.set_file_to_new_string_stream(xkey)
return
class FileDescriptorException(Exception):
pass
def register(i, xkey):
ikey = i.xkey2ikey(xkey)
i._master_table[ikey] = [False, None]
return
# END FileDescriptorClass
class Lol2Str:
"""
`lol`..............`list of lists`
See doc string for `__call__` method
"""
ALLOWED_ARGS = frozenset((
"open_delim",
"close_delim",
"comma_delim",
"is_operaND",
"is_operaTOR",
"file"
))
file = FileDescriptor()
def __init__(i, **kwargs):
"""
"""
type(i).file.register(i)
i.update_args(**kwargs)
# looks weird without a return statement,
# but __init__ not allowed to return
# END OF __init__
class Lol2StrException(Exception):
pass
def update_args(i, **kwargs):
for kw in kwargs.keys():
if kw in type(i).ALLOWED_ARGS:
kwarg = kwargs[kw]
if not isinstance(kwarg, type(None)):
# if not default argument:
setattr(i, kw, kwargs[kw])
# else:
# leave arg as it's previous value
else:
with io.StringIO() as ss:
print(
kw, "is not an allowed argument.",
file=ss
)
msg = ss.getvalue()
raise type(i).Lol2StrException(msg)
def verify_ready_all(i):
one_name = "something more"
try:
for one_name in type(i).ALLOWED_ARGS:
i.verify_ready_one(one_name)
finally:
pass
return
def verify_ready_one(i, one_name):
try:
one = getattr(i, one_name)
except AttributeError:
with io.StringIO() as ss:
print(
"You must set", repr(one_name), "before executing",
file=ss
)
msg = ss.getvalue()
raise type(i).Lol2StrException(msg)
except RecursionError:
msg = "Infinite loop on " + one_name
raise RecursionError(msg)
if isinstance(one, type(None)):
with io.StringIO() as string_stream:
print(
object.__repr__(new_file), "is",
"is missing input argument", one_name,
file=string_stream
)
msg = string_stream.getvalue()
raise type(i).Lol2StrException(msg)
return
def send_out(i, *args, sep=" ", end=""):
return print(*args, end=end,file= i.file)
def attempt_write_operaTOR(i, lol):
try:
elem = next(lol)
elem_status = (
True if i.is_operaTOR(elem) else False,
True if i.is_operaND(elem) else False
)
if elem_status == (True, True):
with io.StringIO() as ss:
print(
"A parsed item was determined to be both",
"an operAND and an operATOR. That is not allowed.",
file=ss
)
s = ss.getvalue()
raise type(i).Lol2StrException(s)
elif elem_status == (True, False):
# Inside of this if-statement
# `elem` is an operator, such as the plus sign in `2 + 3`
i.send_out(elem, end="")
elif elem_status == (False, True):
# `elem` is an argument/operand
# such as the `2` in `2 + 3`
lol = itertools.chain((elem,), lol)
else:
# (operATOR, operAND) = (False, False)
# Not operator and not operand either.
if hasattr(elem, "__iter__"):
###################################################
# Strings are a problem in python
# iter('a') == iter(iter(iter(iter(iter('a')))))
# 'a'[0][0][0][0][0][0] = 'a'[0]
##################################################
#
# redundantly nested args, such as `1 + (((2 + 3)))`
lol = itertools.chain(elem, lol)
else:
# Not operator and not operand either.
# Not redundantly nested args
with io.StringIO() as ss:
print(
type(i).__name__,
"found something which is not an operator, operand,",
"or anything else it knows how to handle.",
"\nThe object was ", object.__repr__(elem),
file=ss
)
s = ss.getvalue()
raise type(i).Lol2StrException(s)
# end if-else block
# end if-else block
finally:
pass
return lol
def write_operaNDs(i, lol):
try:
comma_state = False
i.send_out(i.open_delim)
for elem in lol:
if i.is_operaND(elem):
pass # You're golden. move on to the next step
else:
# element contains nested elements
try:
x = i(elem)
if isinstance(x, type(None)):
elem = ""
comma_state = False
else:
elem = x
except StopIteration:
# element was an EMPTY LIST!!
# WHY AN EMPTY LIST?!? Who only knows...
elem = ""
comma_state = False
# end if-else
if comma_state:
i.send_out(i.comma_delim)
i.send_out(elem)
if not comma_state:
comma_state = True
# end for-loop
i.send_out(i.close_delim)
finally:
pass
return lol
def __call__(i, lol, **kwargs):
"""
NOTES ON NOMENCLATURE:
`delim` ..........`delimiter`
`lol`.............`list of lists`
INPUT ARGUMENTS:
`file` ............ `file` has some sort of `write` method
Any outside file is NOT closed for you.
You must close it youri.
loligag = Lol2Str()
with open(p , mode = "w") as outf:
loligag(lol, file = outf)
loligag(lol, file = outf)
loligag(lol, file = outf)
# `with` statement closes the file for you
Example1: # send output to the console
import sys
loligag(lol, file=sys.stdout)
Example 2: # also send output to the console
file = type("_", tuple(), {"write": lambda i, x: print(x)})()
loligag(lol, file=sys.stdout)
Example 3:
with open("myfile.dat"), mode="w") as outf:
lol_to_prefix_str(lol, file=outf)
If `file = None` then `instance.__call__`
returns a string
`is_operaTOR`... the plus sign in `2 + 3` is an example of an operator
`is_operaTOR` is a callable receiving one argument.
`is_operaTOR(x)` is to return True if and only if `x`
is an operator. `is_operaTOR(x)` is to return False otherwise.
###################################################
# Strings are a problem in python
# iter('a') == iter(iter(iter(iter(iter('a')))))
# 'a'[0][0][0][0][0][0] = 'a'[0]
#
# do **NOT** set is_operaTOR = lambda x: hasattr(x, "__iter__")
####################################################
`lol` ............. list of lists
`open_delim` ...... opening delimeter, such as left parenthesis "("
TODO: documentation for
close_delim
comma_delim
is_operaND
"""
return_val = None
try:
i.update_args(**kwargs)
############################################
i.verify_ready_all() #
############################################
# `open_delim` is not `None`
# `is_operaTOR` is not `None`
# `close_delim` is not `None`
# `comma_delim` is not `None`
# `is_operaND` is not `None`
# `file` is not `None`
############################################
if hasattr(lol, "__iter__"):
try:
lol = type(i).sanitize_lol(lol)
done = False
except type(i).EmptyLol as exc:
# `lol` is empty
# assume empty list, empty tuple
# empty whatever it is, is an operand
i.send_out(lol)
done = True
if not done:
# At this point, lol contains more than one item
lol = i.attempt_write_operaTOR(lol)
lol = i.write_operaNDs(lol)
else:
# ONLY ONE ITEM
# must be an operand?
i.send_out(lol)
# if user originally failed to input a file:
# get string from string stream `i.file`
# close the string stream.
# return the string
we_own_the_file = type(i).file._master_table[id(i)][0]
if we_own_the_file:
return_val = i.file.getvalue()
i.file.close()
finally:
pass
return return_val
@classmethod
def sanitize_lol(cls, lol):
try:
lol = iter(lol)
try:
elem = next(lol)
lol = itertools.chain([elem], lol)
except StopIteration:
with io.StringIO() as err_stream:
print(
"Unable to convert empty container",
"into prefix notation",
file=err_stream
)
msg = err_stream.getvalue()
raise cls.EmptyLol(msg)
finally:
pass
finally:
pass
return lol
class EmptyLol(Exception):
pass
def __del__(i, *args, **kwargs):
type(i).file._update_dead_kin(i)
super_class = inspect.getmro(type(i))[1]
if super_class != object:
super_class.__del__(i, *args, **kwargs)
您如何在列表内部调用一个字符串位置? - python我一直在做迷宫游戏。我首先决定制作一个迷你教程。游戏开发才刚刚开始,现在我正在尝试使其向上发展。我正在尝试更改PlayerAre变量,但是它不起作用。我试过放在列表内和列表外。maze = ["o","*","*","*","*","*",…
用大写字母拆分字符串,但忽略AAA Python Regex - python我的正则表达式:vendor = "MyNameIsJoe. I'mWorkerInAAAinc." ven = re.split(r'(?<=[a-z])[A-Z]|[A-Z](?=[a-z])', vendor) 以大写字母分割字符串,例如:'我的名字是乔。 I'mWorkerInAAAinc”变成…
字符串文字中的正斜杠表现异常 - python为什么S1和S2在撇号位置方面表现不同?S1="1/282/03/10" S2="4/107/03/10" R1="".join({"N\'" ,S1,"\'" }) R2="".join({"N\'…
python-标签不在[index]中 - python我使用for循环创建了一个函数,该函数通过查看每一行的方向值来根据条件返回方向。我将整个数据集一分为二。我在用:def dir_func(df): for i in df.index: if df.loc[i,'dir_1'] == ['E' or 'NE' or 'SE']: …
查找字符串中的行数 - python我正在创建一个python电影播放器/制作器,我想在多行字符串中找到行数。我想知道是否有任何内置函数或可以编写代码的函数来做到这一点:x = """ line1 line2 """ getLines(x) python大神给出的解决方案 如果换行符是'\n',则nlines …