|
##########################################################################
## # The Coq Proof Assistant / The Coq Development Team ##
## v # INRIA, CNRS and contributors - Copyright 1999-2018 ##
## <O___,, # (see CREDITS file for the list of authors) ##
## \VV/ ###############################################################
## // # This file is distributed under the terms of the ##
## # GNU Lesser General Public License Version 2.1 ##
## # (see LICENSE file for the text of the license) ##
##########################################################################
from .TacticNotationsLexer import TacticNotationsLexer
from .TacticNotationsParser import TacticNotationsParser
from antlr4 import CommonTokenStream, InputStream
from antlr4.error.ErrorListener import ErrorListener
SUBSTITUTIONS = [#("@bindings_list", "{+ (@id := @val) }"),
("@qualid_or_string", "@id|@string")]
class ParseError(Exception):
def __init__(self, msg):
super().__init__()
self.msg = msg
class ExceptionRaisingErrorListener(ErrorListener):
def syntaxError(self, recognizer, offendingSymbol, line, column, msg, e):
raise ParseError("{}:{}: {}".format(line, column, msg))
ERROR_LISTENER = ExceptionRaisingErrorListener()
def substitute(notation):
"""Perform common substitutions in the notation string.
Nested notations quickly became unwieldy in the original ‘…’-based format,
so they were avoided and replaced by pointers to grammar rules. With the
new format, it's usually nicer to remove the indirection.
"""
for (src, dst) in SUBSTITUTIONS:
notation = notation.replace(src, dst)
return notation
def parse(notation):
"""Parse a notation string, optionally reporting errors to `error_listener`.
:return: An ANTLR AST. Use one of the supplied visitors (or write your own)
to turn it into useful output.
"""
substituted = substitute(notation)
lexer = TacticNotationsLexer(InputStream(substituted))
parser = TacticNotationsParser(CommonTokenStream(lexer))
parser.addErrorListener(ERROR_LISTENER)
return parser.top()
¤ Dauer der Verarbeitung: 0.15 Sekunden
(vorverarbeitet)
¤
|
Haftungshinweis
Die Informationen auf dieser Webseite wurden
nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit,
noch Qualität der bereit gestellten Informationen zugesichert.
Bemerkung:
Die farbliche Syntaxdarstellung ist noch experimentell.
|
