使用Python将Coq术语在AST形式下转换为波兰式表示法

26

假设我有一个任意的 Coq 术语(使用 s-表达式/sexp 格式的 AST):

n = n + n

我想通过遍历 AST 树(由于 sexp,它只是一个嵌套列表的列表)来自动将其转换为:

= n + n n

在 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
使用S表达式解析器:
[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'), []]]]]]]

2
你特别想使用Python有什么原因吗?我问这个问题是因为在OCaml中做这件事情会更容易,因为你可以访问Coq源代码中的AST操作函数。 - Arthur Azevedo De Amorim
2
@ArthurAzevedoDeAmorim 我可以轻松地从SerAPI(https://github.com/ejgallego/coq-serapi)获取s表达式,并将它们作为列表的列表。我不懂OCaml,但我懂Python。 - Charlie Parker
1
如果你对使用Lisp语法的Python感兴趣,那么你应该看看[Hy][http://docs.hylang.org/en/stable/index.html]。他们已经修改了Python AST模块,为Python创建了一种新的Lisp语法,这可能会引导你朝着正确的方向前进。 - VoNWooDSoN
你的伪代码几乎看起来像Python,但是在Python中赋值运算符用 = 表示,而不是 := - Samuel Muldoon
在您的伪代码中,您写了“后缀树遍历”。然而,波兰式表示法是前缀表示法。波兰式和逆波兰式不同。您想要哪个?参考前缀表示法为+(n,n),中缀表示法为(n + n),后缀表示法为(n,n)+。前缀表示法是波兰式表示法。后缀表示法是逆波兰式表示法。 - Samuel Muldoon
我已经查看了sexp解析器返回的列表和原始树。我无法确定哪些项目是运算符,哪些是操作数。显然,对于+(n, m)+是运算符,nm是操作数。该列表只是一堆Symbol类的实例。似乎操作数和运算符都变成了符号。哪些符号是运算符(函数),哪些符号是操作数(参数)? - Samuel Muldoon
2个回答

1
我已经查看了您的庞大列表。
在顶部/根目录下,我们有:
`['Answer', 2, nested_list]`

好的,看起来'Answer'是运算符。'Answer'有两个参数,2nested_list

因此,用英语表达就是说:“nested_listanswer2
如果我们深入一些呢?

['Answer', 2, ['ObjList', 'nested_list']]

Well, now we have:

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 类。相反,我鼓励您在进行编辑时查找:

  • __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)

0

很抱歉,我不知道有哪些模块可以满足你的需求。但是,如果我正确理解了你想要做的事情,并且正如你所指出的,你只需要遍历这棵树。你的递归实现只是稍微有点问题。你觉得这个怎么样?

class Node:
  def __init__(self, text, children=None):
    self.text = text
    self.children = children or []

  def is_atomic(self):
    return not self.children

def to_polish(root):
    ''' postfix tree traversal '''
    return root.text + ' ' + ''.join(to_polish(n) for n in root.children)

print(to_polish(
  Node('=', [
    Node('a', [
      Node('+', [
        Node('b'),
        Node('c')
      ])
    ])
  ])
))

网页内容由stack overflow 提供, 点击上面的
可以查看英文原文,
原文链接