codekingpro/portable-devtools

1"""2    pygments.lexers.tnt3    ~~~~~~~~~~~~~~~~~~~4 5    Lexer for Typographic Number Theory.6 7    :copyright: Copyright 2006-2024 by the Pygments team, see AUTHORS.8    :license: BSD, see LICENSE for details.9"""10 11import re12 13from pygments.lexer import Lexer14from pygments.token import Text, Comment, Operator, Keyword, Name, Number, \15    Punctuation, Error16 17__all__ = ['TNTLexer']18 19 20class TNTLexer(Lexer):21    """22    Lexer for Typographic Number Theory, as described in the book23    Gödel, Escher, Bach, by Douglas R. Hofstadter24    """25 26    name = 'Typographic Number Theory'27    url = 'https://github.com/Kenny2github/language-tnt'28    aliases = ['tnt']29    filenames = ['*.tnt']30    version_added = '2.7'31 32    cur = []33 34    LOGIC = set('⊃→]&∧^|∨Vv')35    OPERATORS = set('+.⋅*')36    VARIABLES = set('abcde')37    PRIMES = set("'′")38    NEGATORS = set('~!')39    QUANTIFIERS = set('AE∀∃')40    NUMBERS = set('0123456789')41    WHITESPACE = set('\t \v\n')42 43    RULES = re.compile('''(?xi)44        joining | separation | double-tilde | fantasy\\ rule45        | carry[- ]over(?:\\ of)?(?:\\ line)?\\ ([0-9]+) | detachment46        | contrapositive | De\\ Morgan | switcheroo47        | specification | generalization | interchange48        | existence | symmetry | transitivity49        | add\\ S | drop\\ S | induction50        | axiom\\ ([1-5]) | premise | push | pop51    ''')52    LINENOS = re.compile(r'(?:[0-9]+)(?:(?:, ?|,? and )(?:[0-9]+))*')53    COMMENT = re.compile(r'\[[^\n\]]+\]')54 55    def __init__(self, *args, **kwargs):56        Lexer.__init__(self, *args, **kwargs)57        self.cur = []58 59    def whitespace(self, start, text, required=False):60        """Tokenize whitespace."""61        end = start62        try:63            while text[end] in self.WHITESPACE:64                end += 165        except IndexError:66            end = len(text)67        if required and end == start:68            raise AssertionError69        if end != start:70            self.cur.append((start, Text, text[start:end]))71        return end72 73    def variable(self, start, text):74        """Tokenize a variable."""75        if text[start] not in self.VARIABLES:76            raise AssertionError77        end = start+178        while text[end] in self.PRIMES:79            end += 180        self.cur.append((start, Name.Variable, text[start:end]))81        return end82 83    def term(self, start, text):84        """Tokenize a term."""85        if text[start] == 'S':  # S...S(...) or S...086            end = start+187            while text[end] == 'S':88                end += 189            self.cur.append((start, Number.Integer, text[start:end]))90            return self.term(end, text)91        if text[start] == '0':  # the singleton 092            self.cur.append((start, Number.Integer, text[start]))93            return start+194        if text[start] in self.VARIABLES:  # a''...95            return self.variable(start, text)96        if text[start] == '(':  # (...+...)97            self.cur.append((start, Punctuation, text[start]))98            start = self.term(start+1, text)99            if text[start] not in self.OPERATORS:100                raise AssertionError101            self.cur.append((start, Operator, text[start]))102            start = self.term(start+1, text)103            if text[start] != ')':104                raise AssertionError105            self.cur.append((start, Punctuation, text[start]))106            return start+1107        raise AssertionError  # no matches108 109    def formula(self, start, text):110        """Tokenize a formula."""111        if text[start] in self.NEGATORS:  # ~<...>112            end = start+1113            while text[end] in self.NEGATORS:114                end += 1115            self.cur.append((start, Operator, text[start:end]))116            return self.formula(end, text)117        if text[start] in self.QUANTIFIERS:  # Aa:<...>118            self.cur.append((start, Keyword.Declaration, text[start]))119            start = self.variable(start+1, text)120            if text[start] != ':':121                raise AssertionError122            self.cur.append((start, Punctuation, text[start]))123            return self.formula(start+1, text)124        if text[start] == '<':  # <...&...>125            self.cur.append((start, Punctuation, text[start]))126            start = self.formula(start+1, text)127            if text[start] not in self.LOGIC:128                raise AssertionError129            self.cur.append((start, Operator, text[start]))130            start = self.formula(start+1, text)131            if text[start] != '>':132                raise AssertionError133            self.cur.append((start, Punctuation, text[start]))134            return start+1135        # ...=...136        start = self.term(start, text)137        if text[start] != '=':138            raise AssertionError139        self.cur.append((start, Operator, text[start]))140        start = self.term(start+1, text)141        return start142 143    def rule(self, start, text):144        """Tokenize a rule."""145        match = self.RULES.match(text, start)146        if match is None:147            raise AssertionError148        groups = sorted(match.regs[1:])  # exclude whole match149        for group in groups:150            if group[0] >= 0:  # this group matched151                self.cur.append((start, Keyword, text[start:group[0]]))152                self.cur.append((group[0], Number.Integer,153                                 text[group[0]:group[1]]))154                if group[1] != match.end():155                    self.cur.append((group[1], Keyword,156                                     text[group[1]:match.end()]))157                break158        else:159            self.cur.append((start, Keyword, text[start:match.end()]))160        return match.end()161 162    def lineno(self, start, text):163        """Tokenize a line referral."""164        end = start165        while text[end] not in self.NUMBERS:166            end += 1167        self.cur.append((start, Punctuation, text[start]))168        self.cur.append((start+1, Text, text[start+1:end]))169        start = end170        match = self.LINENOS.match(text, start)171        if match is None:172            raise AssertionError173        if text[match.end()] != ')':174            raise AssertionError175        self.cur.append((match.start(), Number.Integer, match.group(0)))176        self.cur.append((match.end(), Punctuation, text[match.end()]))177        return match.end() + 1178 179    def error_till_line_end(self, start, text):180        """Mark everything from ``start`` to the end of the line as Error."""181        end = start182        try:183            while text[end] != '\n':  # there's whitespace in rules184                end += 1185        except IndexError:186            end = len(text)187        if end != start:188            self.cur.append((start, Error, text[start:end]))189        end = self.whitespace(end, text)190        return end191 192    def get_tokens_unprocessed(self, text):193        """Returns a list of TNT tokens."""194        self.cur = []195        start = end = self.whitespace(0, text)196        while start <= end < len(text):197            try:198                # try line number199                while text[end] in self.NUMBERS:200                    end += 1201                if end != start:  # actual number present202                    self.cur.append((start, Number.Integer, text[start:end]))203                    # whitespace is required after a line number204                    orig = len(self.cur)205                    try:206                        start = end = self.whitespace(end, text, True)207                    except AssertionError:208                        del self.cur[orig:]209                        start = end = self.error_till_line_end(end, text)210                        continue211                # at this point it could be a comment212                match = self.COMMENT.match(text, start)213                if match is not None:214                    self.cur.append((start, Comment, text[start:match.end()]))215                    start = end = match.end()216                    # anything after the closing bracket is invalid217                    start = end = self.error_till_line_end(start, text)218                    # do not attempt to process the rest219                    continue220                del match221                if text[start] in '[]':  # fantasy push or pop222                    self.cur.append((start, Keyword, text[start]))223                    start += 1224                    end += 1225                else:226                    # one formula, possibly containing subformulae227                    orig = len(self.cur)228                    try:229                        start = end = self.formula(start, text)230                    except (AssertionError, RecursionError):  # not well-formed231                        del self.cur[orig:]232                        while text[end] not in self.WHITESPACE:233                            end += 1234                        self.cur.append((start, Error, text[start:end]))235                        start = end236                # skip whitespace after formula237                orig = len(self.cur)238                try:239                    start = end = self.whitespace(end, text, True)240                except AssertionError:241                    del self.cur[orig:]242                    start = end = self.error_till_line_end(start, text)243                    continue244                # rule proving this formula a theorem245                orig = len(self.cur)246                try:247                    start = end = self.rule(start, text)248                except AssertionError:249                    del self.cur[orig:]250                    start = end = self.error_till_line_end(start, text)251                    continue252                # skip whitespace after rule253                start = end = self.whitespace(end, text)254                # line marker255                if text[start] == '(':256                    orig = len(self.cur)257                    try:258                        start = end = self.lineno(start, text)259                    except AssertionError:260                        del self.cur[orig:]261                        start = end = self.error_till_line_end(start, text)262                        continue263                    start = end = self.whitespace(start, text)264            except IndexError:265                try:266                    del self.cur[orig:]267                except NameError:268                    pass  # if orig was never defined, fine269                self.error_till_line_end(start, text)270        return self.cur271