#include "tree_sitter/parser.h" #include "tree_sitter/alloc.h" #include "tree_sitter/array.h" #include "assert.h" #include "limits.h" #include "string.h" #include "wctype.h" /** * Macro; goes to the lexer state without consuming any codepoints. * * @param state_value The new lexer state. */ #define GO_TO_STATE(state_value) \ { \ state = state_value; \ goto start; \ } /** * Macro; marks the given lexeme as accepted. * * @param lexeme The lexeme to mark as accepted. */ #define ACCEPT_LEXEME(lexeme) \ { \ (void)result; \ result_lexeme = lexeme; \ } /** * Macro; marks the given token as accepted without also marking the * current position as its end. * * @param token The token to mark as accepted. */ #define ACCEPT_LOOKAHEAD_TOKEN(token) \ { \ result = true; \ lexer->result_symbol = token; \ } /** * Macro; ends a lexer state by returning any accepted lexeme. */ #define END_LEX_STATE() \ { \ return result_lexeme; \ } // Tokens emitted by this external scanner. enum TokenType { LEADING_EXTRAMODULAR_TEXT, // Freeform text at the start of the file. TRAILING_EXTRAMODULAR_TEXT, // Freeform text between or after modules. INDENT, // Marks beginning of junction list. BULLET, // New item of a junction list. DEDENT, // Marks end of junction list. BEGIN_PROOF, // Marks the beginning of an entire proof. BEGIN_PROOF_STEP, // Marks the beginning of a proof step. PROOF_KEYWORD, // The PROOF keyword. BY_KEYWORD, // The BY keyword. OBVIOUS_KEYWORD, // The OBVIOUS keyword. OMITTED_KEYWORD, // The OMITTED keyword. QED_KEYWORD, // The QED keyword. WEAK_FAIRNESS, // The WF_ keyword. STRONG_FAIRNESS, // The SF_ keyword. PCAL_START, // Notifies scanner of start of PlusCal block. PCAL_END, // Notifies scanner of end of PlusCal block. DOUBLE_EXCL, // The !! infix op; lexical conflict with subexpr! ERROR_SENTINEL // Only valid if in error recovery mode. }; // Datatype used to record length of nested proofs & jlists. typedef int16_t nest_address; // Datatype used to record column index of jlists. typedef int16_t column_index; // Datatype used to record proof levels. typedef int32_t proof_level; // A dynamic array of chars. typedef Array(char) CharArray; /** * Advances the scanner while marking the codepoint as non-whitespace. * * @param lexer The tree-sitter lexing control structure. */ static void advance(TSLexer* const lexer) { lexer->advance(lexer, false); } /** * Checks whether the next codepoint is the one given. * * @param lexer The tree-sitter lexing control structure. * @param codepoint The codepoint to check. * @return Whether the next codepoint is the one given. */ static bool is_next_codepoint( const TSLexer* const lexer, int32_t const codepoint ) { return codepoint == lexer->lookahead; } /** * Checks whether there are any codepoints left in the string. * * @param lexer The tree-sitter lexing control structure. * @return Whether there are any codepoints left in the string. */ static bool has_next(const TSLexer* const lexer) { return !lexer->eof(lexer); } /** * Checks whether the given codepoint could be used in an identifier, * which consist of capital ASCII letters, lowercase ASCII letters, * and underscores. * * @param codepoint The codepoint to check. * @return Whether the given codepoint could be used in an identifier. */ static bool is_identifier_char(int32_t const codepoint) { return iswalnum(codepoint) || ('_' == codepoint); } /** * Consumes codepoints as long as they are the one given. * * @param lexer The tree-sitter lexing control structure. * @param codepoint The codepoint to consume. * @return The number of codepoints consumed. */ static void consume_codepoint(TSLexer* const lexer, const int32_t codepoint) { while (has_next(lexer) && is_next_codepoint(lexer, codepoint)) { advance(lexer); } } /** * Checks whether the next codepoint sequence is the one given. * This function can change the state of the lexer. * * @param lexer The tree-sitter lexing control structure. * @param token The codepoint sequence to check for. * @return Whether the next codepoint sequence is the one given. */ static bool is_next_codepoint_sequence( TSLexer* const lexer, const char codepoint_sequence[] ) { size_t sequence_length = strlen(codepoint_sequence); for (size_t i = 0; i < sequence_length; i++) { int32_t codepoint = codepoint_sequence[i]; if (!is_next_codepoint(lexer, codepoint)) { return false; } else if (i + 1 < sequence_length) { advance(lexer); } } return true; } // Possible states for the extramodular text lexer to enter. enum EMTLexState { EMTLexState_CONSUME, EMTLexState_DASH, EMTLexState_SINGLE_LINE, EMTLexState_MODULE, EMTLexState_BLANK_BEFORE_MODULE, EMTLexState_END_OF_FILE, EMTLexState_BLANK_BEFORE_END_OF_FILE }; /** * Scans for extramodular text, the freeform text that can be present * outside of TLA⁺ modules. This function skips any leading whitespace * to avoid extraneous extramodular text tokens given newlines at the * beginning or end of the file. It will consume any text up to the * point it performs lookahead that captures the following regex: * /----[-]*[ ]*MODULE/ * or EOF, which marks the end of the extramodular text. It is important * that the extramodular text does not itself include the captured module * start sequence, which is why this is in an external scanner rather * than a regex in the grammar itself. * * @param lexer The tree-sitter lexing control structure * @param valid_symbols Tokens possibly expected in this spot. * @return Whether any extramodular text was detected. */ static bool scan_extramodular_text(TSLexer* const lexer, const bool* const valid_symbols) { bool has_consumed_any = false; enum EMTLexState state = EMTLexState_CONSUME; START_LEXER(); eof = !has_next(lexer); switch (state) { case EMTLexState_CONSUME: if (eof) ADVANCE(EMTLexState_END_OF_FILE); if (iswspace(lookahead) && !has_consumed_any) SKIP(EMTLexState_CONSUME); if (iswspace(lookahead) && has_consumed_any) ADVANCE(EMTLexState_CONSUME); lexer->mark_end(lexer); if ('-' == lookahead) ADVANCE(EMTLexState_DASH); has_consumed_any = true; ADVANCE(EMTLexState_CONSUME); END_STATE(); case EMTLexState_DASH: if (is_next_codepoint_sequence(lexer, "---")) ADVANCE(EMTLexState_SINGLE_LINE); has_consumed_any = true; GO_TO_STATE(EMTLexState_CONSUME); END_STATE(); case EMTLexState_SINGLE_LINE: consume_codepoint(lexer, '-'); consume_codepoint(lexer, ' '); if (is_next_codepoint_sequence(lexer, "MODULE")) { ADVANCE(EMTLexState_MODULE); } has_consumed_any = true; GO_TO_STATE(EMTLexState_CONSUME); END_STATE(); case EMTLexState_MODULE: if (!has_consumed_any) GO_TO_STATE(EMTLexState_BLANK_BEFORE_MODULE); ACCEPT_LOOKAHEAD_TOKEN(valid_symbols[LEADING_EXTRAMODULAR_TEXT] ? LEADING_EXTRAMODULAR_TEXT : TRAILING_EXTRAMODULAR_TEXT); END_STATE(); case EMTLexState_BLANK_BEFORE_MODULE: END_STATE(); case EMTLexState_END_OF_FILE: if (!has_consumed_any) GO_TO_STATE(EMTLexState_BLANK_BEFORE_END_OF_FILE); if (valid_symbols[TRAILING_EXTRAMODULAR_TEXT]) { ACCEPT_TOKEN(TRAILING_EXTRAMODULAR_TEXT); } END_STATE(); case EMTLexState_BLANK_BEFORE_END_OF_FILE: END_STATE(); default: END_STATE(); } } // Types of proof step IDs. enum ProofStepIdType { ProofStepIdType_STAR, // <*> ProofStepIdType_PLUS, // <+> ProofStepIdType_NUMBERED, // <1234> ProofStepIdType_NONE // Invalid or nonexistent }; // Data about a proof step ID. struct ProofStepId { // The proof step ID type. enum ProofStepIdType type; // The proof step ID level (-1 if not NUMBERED). proof_level level; }; /** * Initializes a new instance of the ProofStepId class. * * @param raw_level The unparsed contents of the <...> lexeme. */ static struct ProofStepId parse_proof_step_id(const CharArray* raw_level) { struct ProofStepId id; id.level = -1; if (0 == raw_level->size) { id.type = ProofStepIdType_NONE; } else if ('*' == *array_get(raw_level, 0)) { id.type = ProofStepIdType_STAR; } else if ('+' == *array_get(raw_level, 0)) { id.type = ProofStepIdType_PLUS; } else { id.type = ProofStepIdType_NUMBERED; id.level = 0; int32_t multiplier = 1; for (size_t i = 0; i < raw_level->size; i++) { const size_t index = raw_level->size - i - 1; const int8_t digit_value = *array_get(raw_level, index) - 48; if (0 <= digit_value && digit_value <= 9) { id.level += digit_value * multiplier; multiplier *= 10; } else { id.type = ProofStepIdType_NONE; id.level = -1; break; } } } array_delete(raw_level); return id; } // Lexemes recognized by this lexer. enum Lexeme { Lexeme_FORWARD_SLASH, Lexeme_BACKWARD_SLASH, Lexeme_GT, Lexeme_EQ, Lexeme_DASH, Lexeme_COMMA, Lexeme_COLON, Lexeme_SEMICOLON, Lexeme_LAND, Lexeme_LOR, Lexeme_DOUBLE_EXCL, Lexeme_L_PAREN, Lexeme_R_PAREN, Lexeme_R_SQUARE_BRACKET, Lexeme_R_CURLY_BRACE, Lexeme_R_ANGLE_BRACKET, Lexeme_RIGHT_ARROW, Lexeme_RIGHT_MAP_ARROW, Lexeme_COMMENT_START, Lexeme_BLOCK_COMMENT_START, Lexeme_SINGLE_LINE, Lexeme_DOUBLE_LINE, Lexeme_ASSUME_KEYWORD, Lexeme_ASSUMPTION_KEYWORD, Lexeme_AXIOM_KEYWORD, Lexeme_BY_KEYWORD, Lexeme_CONSTANT_KEYWORD, Lexeme_CONSTANTS_KEYWORD, Lexeme_COROLLARY_KEYWORD, Lexeme_ELSE_KEYWORD, Lexeme_IN_KEYWORD, Lexeme_LEMMA_KEYWORD, Lexeme_LOCAL_KEYWORD, Lexeme_OBVIOUS_KEYWORD, Lexeme_OMITTED_KEYWORD, Lexeme_PROOF_KEYWORD, Lexeme_PROPOSITION_KEYWORD, Lexeme_QED_KEYWORD, Lexeme_THEN_KEYWORD, Lexeme_THEOREM_KEYWORD, Lexeme_VARIABLE_KEYWORD, Lexeme_VARIABLES_KEYWORD, Lexeme_PROOF_STEP_ID, Lexeme_IDENTIFIER, Lexeme_WEAK_FAIRNESS, Lexeme_STRONG_FAIRNESS, Lexeme_OTHER, Lexeme_END_OF_FILE }; // Possible states for the lexer to enter. enum LexState { LexState_CONSUME_LEADING_SPACE, LexState_FORWARD_SLASH, LexState_BACKWARD_SLASH, LexState_LT, LexState_GT, LexState_EQ, LexState_DASH, LexState_COMMA, LexState_COLON, LexState_EXCL, LexState_DOUBLE_EXCL, LexState_SEMICOLON, LexState_LAND, LexState_LOR, LexState_L_PAREN, LexState_R_PAREN, LexState_R_SQUARE_BRACKET, LexState_R_CURLY_BRACE, LexState_R_ANGLE_BRACKET, LexState_S, LexState_SF_, LexState_RIGHT_ARROW, LexState_RIGHT_MAP_ARROW, LexState_COMMENT_START, LexState_BLOCK_COMMENT_START, LexState_SINGLE_LINE, LexState_DOUBLE_LINE, LexState_PIPE, LexState_RIGHT_TURNSTILE, LexState_A, LexState_ASSUM, LexState_ASSUME, LexState_ASSUMPTION, LexState_AX, LexState_AXIOM, LexState_B, LexState_BY, LexState_C, LexState_CO, LexState_CON, LexState_COR, LexState_CONSTANT, LexState_CONSTANTS, LexState_COROLLARY, LexState_E, LexState_ELSE, LexState_I, LexState_IN, LexState_L, LexState_LE, LexState_LEMMA, LexState_LO, LexState_LOCAL, LexState_O, LexState_OB, LexState_OBVIOUS, LexState_OM, LexState_OMITTED, LexState_P, LexState_PRO, LexState_PROO, LexState_PROOF, LexState_PROP, LexState_PROPOSITION, LexState_Q, LexState_QED, LexState_T, LexState_THE, LexState_THEN, LexState_THEOREM, LexState_V, LexState_VARIABLE, LexState_VARIABLES, LexState_W, LexState_WF_, LexState_IDENTIFIER, LexState_PROOF_LEVEL_NUMBER, LexState_PROOF_LEVEL_STAR, LexState_PROOF_LEVEL_PLUS, LexState_PROOF_NAME, LexState_PROOF_ID, LexState_OTHER, LexState_END_OF_FILE }; /** * Looks ahead to identify the next lexeme. Consumes all leading * whitespace. Out parameters include column of first non-whitespace * codepoint and the level of the proof step ID lexeme if encountered. * * @param lexer The tree-sitter lexing control structure. * @param lexeme_start_col The starting column of the first lexeme. * @param proof_step_id_level The level of the proof step ID. * @return The lexeme encountered. */ static enum Lexeme lex_lookahead( TSLexer* const lexer, column_index* lexeme_start_col, CharArray* proof_step_id_level ) { enum LexState state = LexState_CONSUME_LEADING_SPACE; enum Lexeme result_lexeme = Lexeme_OTHER; START_LEXER(); eof = !has_next(lexer); switch (state) { case LexState_CONSUME_LEADING_SPACE: if (iswspace(lookahead)) SKIP(LexState_CONSUME_LEADING_SPACE); *lexeme_start_col = lexer->get_column(lexer); lexer->mark_end(lexer); if (eof) ADVANCE(LexState_END_OF_FILE); if ('/' == lookahead) ADVANCE(LexState_FORWARD_SLASH); if ('\\' == lookahead) ADVANCE(LexState_BACKWARD_SLASH); if ('<' == lookahead) ADVANCE(LexState_LT); if ('>' == lookahead) ADVANCE(LexState_GT); if ('=' == lookahead) ADVANCE(LexState_EQ); if ('-' == lookahead) ADVANCE(LexState_DASH); if (',' == lookahead) ADVANCE(LexState_COMMA); if (':' == lookahead) ADVANCE(LexState_COLON); if (';' == lookahead) ADVANCE(LexState_SEMICOLON); if ('(' == lookahead) ADVANCE(LexState_L_PAREN); if (')' == lookahead) ADVANCE(LexState_R_PAREN); if (']' == lookahead) ADVANCE(LexState_R_SQUARE_BRACKET); if ('}' == lookahead) ADVANCE(LexState_R_CURLY_BRACE); if ('|' == lookahead) ADVANCE(LexState_PIPE); if ('!' == lookahead) ADVANCE(LexState_EXCL); if ('A' == lookahead) ADVANCE(LexState_A); if ('B' == lookahead) ADVANCE(LexState_B); if ('C' == lookahead) ADVANCE(LexState_C); if ('E' == lookahead) ADVANCE(LexState_E); if ('I' == lookahead) ADVANCE(LexState_I); if ('L' == lookahead) ADVANCE(LexState_L); if ('O' == lookahead) ADVANCE(LexState_O); if ('P' == lookahead) ADVANCE(LexState_P); if ('Q' == lookahead) ADVANCE(LexState_Q); if ('S' == lookahead) ADVANCE(LexState_S); if ('T' == lookahead) ADVANCE(LexState_T); if ('V' == lookahead) ADVANCE(LexState_V); if ('W' == lookahead) ADVANCE(LexState_W); if (L'\u2227' == lookahead) ADVANCE(LexState_LAND); // '∧' if (L'\u2228' == lookahead) ADVANCE(LexState_LOR); // '∨' if (L'\u3009' == lookahead) ADVANCE(LexState_R_ANGLE_BRACKET); // '〉' if (L'\u27E9' == lookahead) ADVANCE(LexState_R_ANGLE_BRACKET); // '⟩' if (L'\u27F6' == lookahead) ADVANCE(LexState_RIGHT_ARROW); // '⟶' if (L'\u2192' == lookahead) ADVANCE(LexState_RIGHT_ARROW); // '→' if (L'\u27FC' == lookahead) ADVANCE(LexState_RIGHT_MAP_ARROW); // '⟼' if (L'\u21A6' == lookahead) ADVANCE(LexState_RIGHT_MAP_ARROW); // '↦' ADVANCE(LexState_OTHER); END_LEX_STATE(); case LexState_FORWARD_SLASH: ACCEPT_LEXEME(Lexeme_FORWARD_SLASH); if ('\\' == lookahead) ADVANCE(LexState_LAND); END_LEX_STATE(); case LexState_BACKWARD_SLASH: ACCEPT_LEXEME(Lexeme_BACKWARD_SLASH); if ('/' == lookahead) ADVANCE(LexState_LOR); if ('*' == lookahead) ADVANCE(LexState_COMMENT_START); END_LEX_STATE(); case LexState_LT: array_push(proof_step_id_level, (char)(lookahead & CHAR_MAX)); if (iswdigit(lookahead)) ADVANCE(LexState_PROOF_LEVEL_NUMBER); if ('*' == lookahead) ADVANCE(LexState_PROOF_LEVEL_STAR); if ('+' == lookahead) ADVANCE(LexState_PROOF_LEVEL_PLUS); ADVANCE(LexState_OTHER); END_LEX_STATE(); case LexState_GT: ACCEPT_LEXEME(Lexeme_GT); if ('>' == lookahead) ADVANCE(LexState_R_ANGLE_BRACKET); END_LEX_STATE(); case LexState_EQ: ACCEPT_LEXEME(Lexeme_EQ); if (is_next_codepoint_sequence(lexer, "===")) ADVANCE(LexState_DOUBLE_LINE); END_LEX_STATE(); case LexState_DASH: ACCEPT_LEXEME(Lexeme_DASH); if ('>' == lookahead) ADVANCE(LexState_RIGHT_ARROW); if (is_next_codepoint_sequence(lexer, "---")) ADVANCE(LexState_SINGLE_LINE); END_LEX_STATE(); case LexState_COMMA: ACCEPT_LEXEME(Lexeme_COMMA); END_LEX_STATE(); case LexState_COLON: ACCEPT_LEXEME(Lexeme_COLON); if (':' == lookahead) ADVANCE(LexState_OTHER); if ('=' == lookahead) ADVANCE(LexState_OTHER); if ('>' == lookahead) ADVANCE(LexState_OTHER); END_LEX_STATE(); case LexState_SEMICOLON: ACCEPT_LEXEME(Lexeme_SEMICOLON); END_LEX_STATE(); case LexState_LAND: ACCEPT_LEXEME(Lexeme_LAND); END_LEX_STATE(); case LexState_LOR: ACCEPT_LEXEME(Lexeme_LOR); END_LEX_STATE(); case LexState_L_PAREN: ACCEPT_LEXEME(Lexeme_L_PAREN); if ('*' == lookahead) ADVANCE(LexState_BLOCK_COMMENT_START); END_LEX_STATE(); case LexState_R_PAREN: ACCEPT_LEXEME(Lexeme_R_PAREN); END_LEX_STATE(); case LexState_R_SQUARE_BRACKET: ACCEPT_LEXEME(Lexeme_R_SQUARE_BRACKET); END_LEX_STATE(); case LexState_R_CURLY_BRACE: ACCEPT_LEXEME(Lexeme_R_CURLY_BRACE); END_LEX_STATE(); case LexState_R_ANGLE_BRACKET: ACCEPT_LEXEME(Lexeme_R_ANGLE_BRACKET); END_LEX_STATE(); case LexState_RIGHT_ARROW: ACCEPT_LEXEME(Lexeme_RIGHT_ARROW); END_LEX_STATE(); case LexState_RIGHT_MAP_ARROW: ACCEPT_LEXEME(Lexeme_RIGHT_MAP_ARROW); END_LEX_STATE(); case LexState_COMMENT_START: ACCEPT_LEXEME(Lexeme_COMMENT_START); END_LEX_STATE(); case LexState_BLOCK_COMMENT_START: ACCEPT_LEXEME(Lexeme_BLOCK_COMMENT_START); END_LEX_STATE(); case LexState_SINGLE_LINE: ACCEPT_LEXEME(Lexeme_SINGLE_LINE); END_LEX_STATE(); case LexState_DOUBLE_LINE: ACCEPT_LEXEME(Lexeme_DOUBLE_LINE); END_LEX_STATE(); case LexState_PIPE: if ('-' == lookahead) ADVANCE(LexState_RIGHT_TURNSTILE); END_LEX_STATE(); case LexState_EXCL: if ('!' == lookahead) ADVANCE(LexState_DOUBLE_EXCL); END_LEX_STATE(); case LexState_DOUBLE_EXCL: ACCEPT_LEXEME(Lexeme_DOUBLE_EXCL); END_LEX_STATE(); case LexState_RIGHT_TURNSTILE: if ('>' == lookahead) ADVANCE(LexState_RIGHT_MAP_ARROW); END_LEX_STATE(); case LexState_A: ACCEPT_LEXEME(Lexeme_IDENTIFIER); if ('X' == lookahead) ADVANCE(LexState_AX); if (is_next_codepoint_sequence(lexer, "SSUM")) ADVANCE(LexState_ASSUM); END_LEX_STATE(); case LexState_ASSUM: ACCEPT_LEXEME(Lexeme_IDENTIFIER); if ('E' == lookahead) ADVANCE(LexState_ASSUME); if (is_next_codepoint_sequence(lexer, "PTION")) ADVANCE(LexState_ASSUMPTION); END_LEX_STATE(); case LexState_ASSUME: ACCEPT_LEXEME(Lexeme_ASSUME_KEYWORD); if (is_identifier_char(lookahead)) ADVANCE(LexState_IDENTIFIER); END_LEX_STATE(); case LexState_ASSUMPTION: ACCEPT_LEXEME(Lexeme_ASSUMPTION_KEYWORD); if (is_identifier_char(lookahead)) ADVANCE(LexState_IDENTIFIER); END_LEX_STATE(); case LexState_AX: ACCEPT_LEXEME(Lexeme_IDENTIFIER); if (is_next_codepoint_sequence(lexer, "IOM")) ADVANCE(LexState_AXIOM); END_LEX_STATE(); case LexState_AXIOM: ACCEPT_LEXEME(Lexeme_AXIOM_KEYWORD); if (is_identifier_char(lookahead)) ADVANCE(LexState_IDENTIFIER); END_LEX_STATE(); case LexState_B: ACCEPT_LEXEME(Lexeme_IDENTIFIER); if ('Y' == lookahead) ADVANCE(LexState_BY); END_LEX_STATE(); case LexState_BY: ACCEPT_LEXEME(Lexeme_BY_KEYWORD); if (is_identifier_char(lookahead)) ADVANCE(LexState_IDENTIFIER); END_LEX_STATE(); case LexState_C: ACCEPT_LEXEME(Lexeme_IDENTIFIER); if ('O' == lookahead) ADVANCE(LexState_CO); END_LEX_STATE(); case LexState_CO: ACCEPT_LEXEME(Lexeme_IDENTIFIER); if ('N' == lookahead) ADVANCE(LexState_CON); if ('R' == lookahead) ADVANCE(LexState_COR); END_LEX_STATE(); case LexState_CON: ACCEPT_LEXEME(Lexeme_IDENTIFIER); if (is_next_codepoint_sequence(lexer, "STANT")) ADVANCE(LexState_CONSTANT); END_LEX_STATE(); case LexState_CONSTANT: ACCEPT_LEXEME(Lexeme_CONSTANT_KEYWORD); if ('S' == lookahead) ADVANCE(LexState_CONSTANTS); if (is_identifier_char(lookahead)) ADVANCE(LexState_IDENTIFIER); END_LEX_STATE(); case LexState_CONSTANTS: ACCEPT_LEXEME(Lexeme_CONSTANTS_KEYWORD); if (is_identifier_char(lookahead)) ADVANCE(LexState_IDENTIFIER); END_LEX_STATE(); case LexState_COR: ACCEPT_LEXEME(Lexeme_IDENTIFIER); if (is_next_codepoint_sequence(lexer, "OLLARY")) ADVANCE(LexState_COROLLARY); END_LEX_STATE(); case LexState_COROLLARY: ACCEPT_LEXEME(Lexeme_COROLLARY_KEYWORD); if (is_identifier_char(lookahead)) ADVANCE(LexState_IDENTIFIER); END_LEX_STATE(); case LexState_E: ACCEPT_LEXEME(Lexeme_IDENTIFIER); if (is_next_codepoint_sequence(lexer, "LSE")) ADVANCE(LexState_ELSE); END_LEX_STATE(); case LexState_ELSE: ACCEPT_LEXEME(Lexeme_ELSE_KEYWORD); if (is_identifier_char(lookahead)) ADVANCE(LexState_IDENTIFIER); END_LEX_STATE(); case LexState_I: ACCEPT_LEXEME(Lexeme_IDENTIFIER); if ('N' == lookahead) ADVANCE(LexState_IN); END_LEX_STATE(); case LexState_IN: ACCEPT_LEXEME(Lexeme_IN_KEYWORD); if (is_identifier_char(lookahead)) ADVANCE(LexState_IDENTIFIER); END_LEX_STATE(); case LexState_L: ACCEPT_LEXEME(Lexeme_IDENTIFIER); if ('E' == lookahead) ADVANCE(LexState_LE); if ('O' == lookahead) ADVANCE(LexState_LO); END_LEX_STATE(); case LexState_LE: ACCEPT_LEXEME(Lexeme_IDENTIFIER); if (is_next_codepoint_sequence(lexer, "MMA")) ADVANCE(LexState_LEMMA); END_LEX_STATE(); case LexState_LEMMA: ACCEPT_LEXEME(Lexeme_LEMMA_KEYWORD); if (is_identifier_char(lookahead)) ADVANCE(LexState_IDENTIFIER); END_LEX_STATE(); case LexState_LO: ACCEPT_LEXEME(Lexeme_IDENTIFIER); if (is_next_codepoint_sequence(lexer, "CAL")) ADVANCE(LexState_LOCAL); END_LEX_STATE(); case LexState_LOCAL: ACCEPT_LEXEME(Lexeme_LOCAL_KEYWORD); if (is_identifier_char(lookahead)) ADVANCE(LexState_IDENTIFIER); END_LEX_STATE(); case LexState_O: ACCEPT_LEXEME(Lexeme_IDENTIFIER); if ('B' == lookahead) ADVANCE(LexState_OB); if ('M' == lookahead) ADVANCE(LexState_OM); END_LEX_STATE(); case LexState_OB: ACCEPT_LEXEME(Lexeme_IDENTIFIER); if (is_next_codepoint_sequence(lexer, "VIOUS")) ADVANCE(LexState_OBVIOUS); END_LEX_STATE(); case LexState_OBVIOUS: ACCEPT_LEXEME(Lexeme_OBVIOUS_KEYWORD); if (is_identifier_char(lookahead)) ADVANCE(LexState_IDENTIFIER); END_LEX_STATE(); case LexState_OM: ACCEPT_LEXEME(Lexeme_IDENTIFIER); if (is_next_codepoint_sequence(lexer, "ITTED")) ADVANCE(LexState_OMITTED); END_LEX_STATE(); case LexState_OMITTED: ACCEPT_LEXEME(Lexeme_OMITTED_KEYWORD); if (is_identifier_char(lookahead)) ADVANCE(LexState_IDENTIFIER); END_LEX_STATE(); case LexState_P: ACCEPT_LEXEME(Lexeme_IDENTIFIER); if (is_next_codepoint_sequence(lexer, "RO")) ADVANCE(LexState_PRO); END_LEX_STATE(); case LexState_PRO: ACCEPT_LEXEME(Lexeme_IDENTIFIER); if ('O' == lookahead) ADVANCE(LexState_PROO); if ('P' == lookahead) ADVANCE(LexState_PROP); END_LEX_STATE(); case LexState_PROO: ACCEPT_LEXEME(Lexeme_IDENTIFIER); if ('F' == lookahead) ADVANCE(LexState_PROOF); END_LEX_STATE(); case LexState_PROOF: ACCEPT_LEXEME(Lexeme_PROOF_KEYWORD); if (is_identifier_char(lookahead)) ADVANCE(LexState_IDENTIFIER); END_LEX_STATE(); case LexState_PROP: ACCEPT_LEXEME(Lexeme_IDENTIFIER); if (is_next_codepoint_sequence(lexer, "OSITION")) ADVANCE(LexState_PROPOSITION); END_LEX_STATE(); case LexState_PROPOSITION: ACCEPT_LEXEME(Lexeme_PROPOSITION_KEYWORD); if (is_identifier_char(lookahead)) ADVANCE(LexState_IDENTIFIER); END_LEX_STATE(); case LexState_Q: ACCEPT_LEXEME(Lexeme_IDENTIFIER); if (is_next_codepoint_sequence(lexer, "ED")) ADVANCE(LexState_QED); END_LEX_STATE(); case LexState_QED: ACCEPT_LEXEME(Lexeme_QED_KEYWORD); if (is_identifier_char(lookahead)) ADVANCE(LexState_IDENTIFIER); END_LEX_STATE(); case LexState_S: ACCEPT_LEXEME(Lexeme_IDENTIFIER); if (is_next_codepoint_sequence(lexer, "F_")) ADVANCE(LexState_SF_); END_LEX_STATE(); case LexState_SF_: ACCEPT_LEXEME(Lexeme_STRONG_FAIRNESS); END_LEX_STATE(); case LexState_T: ACCEPT_LEXEME(Lexeme_IDENTIFIER); if (is_next_codepoint_sequence(lexer, "HE")) ADVANCE(LexState_THE); END_LEX_STATE(); case LexState_THE: ACCEPT_LEXEME(Lexeme_IDENTIFIER); if ('N' == lookahead) ADVANCE(LexState_THEN); if (is_next_codepoint_sequence(lexer, "OREM")) ADVANCE(LexState_THEOREM); END_LEX_STATE(); case LexState_THEN: ACCEPT_LEXEME(Lexeme_THEN_KEYWORD); if (is_identifier_char(lookahead)) ADVANCE(LexState_IDENTIFIER); END_LEX_STATE(); case LexState_THEOREM: ACCEPT_LEXEME(Lexeme_THEOREM_KEYWORD); if (is_identifier_char(lookahead)) ADVANCE(LexState_IDENTIFIER); END_LEX_STATE(); case LexState_V: ACCEPT_LEXEME(Lexeme_IDENTIFIER); if (is_next_codepoint_sequence(lexer, "ARIABLE")) ADVANCE(LexState_VARIABLE); END_LEX_STATE(); case LexState_VARIABLE: ACCEPT_LEXEME(Lexeme_VARIABLE_KEYWORD); if ('S' == lookahead) ADVANCE(LexState_VARIABLES); if (is_identifier_char(lookahead)) ADVANCE(LexState_IDENTIFIER); END_LEX_STATE(); case LexState_VARIABLES: ACCEPT_LEXEME(Lexeme_VARIABLES_KEYWORD); if (is_identifier_char(lookahead)) ADVANCE(LexState_IDENTIFIER); END_LEX_STATE(); case LexState_W: ACCEPT_LEXEME(Lexeme_IDENTIFIER); if (is_next_codepoint_sequence(lexer, "F_")) ADVANCE(LexState_WF_); END_LEX_STATE(); case LexState_WF_: ACCEPT_LEXEME(Lexeme_WEAK_FAIRNESS); END_LEX_STATE(); case LexState_PROOF_LEVEL_NUMBER: if (iswdigit(lookahead)) { array_push(proof_step_id_level, (char)(lookahead & CHAR_MAX)); ADVANCE(LexState_PROOF_LEVEL_NUMBER); } if ('>' == lookahead) ADVANCE(LexState_PROOF_NAME); ADVANCE(LexState_OTHER); END_LEX_STATE(); case LexState_PROOF_LEVEL_STAR: if ('>' == lookahead) ADVANCE(LexState_PROOF_NAME); ADVANCE(LexState_OTHER); END_LEX_STATE(); case LexState_PROOF_LEVEL_PLUS: if ('>' == lookahead) ADVANCE(LexState_PROOF_NAME); ADVANCE(LexState_OTHER); END_LEX_STATE(); case LexState_PROOF_NAME: ACCEPT_LEXEME(Lexeme_PROOF_STEP_ID); if (iswalnum(lookahead)) ADVANCE(LexState_PROOF_NAME); if ('.' == lookahead) ADVANCE(LexState_PROOF_ID); END_LEX_STATE(); case LexState_PROOF_ID: ACCEPT_LEXEME(Lexeme_PROOF_STEP_ID); if ('.' == lookahead) ADVANCE(LexState_PROOF_ID); END_LEX_STATE(); case LexState_IDENTIFIER: ACCEPT_LEXEME(Lexeme_IDENTIFIER); END_LEX_STATE(); case LexState_OTHER: ACCEPT_LEXEME(Lexeme_OTHER); END_LEX_STATE(); case LexState_END_OF_FILE: ACCEPT_LEXEME(Lexeme_END_OF_FILE); END_LEX_STATE(); default: ACCEPT_LEXEME(Lexeme_OTHER); END_LEX_STATE(); } } // Tokens recognized by this scanner. enum Token { Token_LAND, Token_LOR, Token_DOUBLE_EXCL, Token_RIGHT_DELIMITER, Token_COMMENT_START, Token_TERMINATOR, Token_PROOF_STEP_ID, Token_PROOF_KEYWORD, Token_BY_KEYWORD, Token_OBVIOUS_KEYWORD, Token_OMITTED_KEYWORD, Token_QED_KEYWORD, Token_WEAK_FAIRNESS, Token_STRONG_FAIRNESS, Token_OTHER }; /** * Maps the given lexeme to a token. * * @param lexeme The lexeme to map to a token. * @return The token corresponding to the given lexeme. */ static enum Token tokenize_lexeme(enum Lexeme lexeme) { switch (lexeme) { case Lexeme_FORWARD_SLASH: return Token_OTHER; case Lexeme_BACKWARD_SLASH: return Token_OTHER; case Lexeme_GT: return Token_OTHER; case Lexeme_EQ: return Token_OTHER; case Lexeme_DASH: return Token_OTHER; case Lexeme_COMMA: return Token_RIGHT_DELIMITER; case Lexeme_COLON: return Token_RIGHT_DELIMITER; case Lexeme_SEMICOLON: return Token_TERMINATOR; case Lexeme_LAND: return Token_LAND; case Lexeme_LOR: return Token_LOR; case Lexeme_DOUBLE_EXCL: return Token_DOUBLE_EXCL; case Lexeme_L_PAREN: return Token_OTHER; case Lexeme_R_PAREN: return Token_RIGHT_DELIMITER; case Lexeme_R_SQUARE_BRACKET: return Token_RIGHT_DELIMITER; case Lexeme_R_CURLY_BRACE: return Token_RIGHT_DELIMITER; case Lexeme_R_ANGLE_BRACKET: return Token_RIGHT_DELIMITER; case Lexeme_RIGHT_ARROW: return Token_RIGHT_DELIMITER; case Lexeme_RIGHT_MAP_ARROW: return Token_RIGHT_DELIMITER; case Lexeme_COMMENT_START: return Token_COMMENT_START; case Lexeme_BLOCK_COMMENT_START: return Token_COMMENT_START; case Lexeme_SINGLE_LINE: return Token_TERMINATOR; case Lexeme_DOUBLE_LINE: return Token_TERMINATOR; case Lexeme_ASSUME_KEYWORD: return Token_TERMINATOR; case Lexeme_ASSUMPTION_KEYWORD: return Token_TERMINATOR; case Lexeme_AXIOM_KEYWORD: return Token_TERMINATOR; case Lexeme_BY_KEYWORD: return Token_BY_KEYWORD; case Lexeme_CONSTANT_KEYWORD: return Token_TERMINATOR; case Lexeme_CONSTANTS_KEYWORD: return Token_TERMINATOR; case Lexeme_COROLLARY_KEYWORD: return Token_TERMINATOR; case Lexeme_ELSE_KEYWORD: return Token_RIGHT_DELIMITER; case Lexeme_IN_KEYWORD: return Token_RIGHT_DELIMITER; case Lexeme_LEMMA_KEYWORD: return Token_TERMINATOR; case Lexeme_LOCAL_KEYWORD: return Token_TERMINATOR; case Lexeme_OBVIOUS_KEYWORD: return Token_OBVIOUS_KEYWORD; case Lexeme_OMITTED_KEYWORD: return Token_OMITTED_KEYWORD; case Lexeme_PROOF_KEYWORD: return Token_PROOF_KEYWORD; case Lexeme_PROPOSITION_KEYWORD: return Token_TERMINATOR; case Lexeme_THEN_KEYWORD: return Token_RIGHT_DELIMITER; case Lexeme_THEOREM_KEYWORD: return Token_TERMINATOR; case Lexeme_VARIABLE_KEYWORD: return Token_TERMINATOR; case Lexeme_VARIABLES_KEYWORD: return Token_TERMINATOR; case Lexeme_PROOF_STEP_ID: return Token_PROOF_STEP_ID; case Lexeme_QED_KEYWORD: return Token_QED_KEYWORD; case Lexeme_STRONG_FAIRNESS: return Token_STRONG_FAIRNESS; case Lexeme_WEAK_FAIRNESS: return Token_WEAK_FAIRNESS; case Lexeme_IDENTIFIER: return Token_OTHER; case Lexeme_OTHER: return Token_OTHER; case Lexeme_END_OF_FILE: return Token_TERMINATOR; default: return Token_OTHER; } } // Possible types of junction list. enum JunctType { JunctType_CONJUNCTION, JunctType_DISJUNCTION }; // Data about a jlist. struct JunctList { // The type of jlist. enum JunctType type; // The starting alignment columnt of the jlist. column_index alignment_column; }; static struct JunctList create_junctlist(enum JunctType const type, column_index const alignment_column) { struct JunctList jlist; jlist.type = type; jlist.alignment_column = alignment_column; return jlist; } static unsigned jlist_serialize(struct JunctList* this, char* const buffer, bool const is_dry_run) { unsigned offset = 0; unsigned copied = 0; // Serialize junction type copied = sizeof(uint8_t); if (!is_dry_run) { buffer[offset] = (uint8_t)(this->type); } offset += copied; // Serialize alignment column copied = sizeof(column_index); if (!is_dry_run) { memcpy(&buffer[offset], &this->alignment_column, copied); } offset += copied; return offset; } static unsigned jlist_deserialize(struct JunctList* this, const char* const buffer) { unsigned offset = 0; unsigned copied = 0; // Deserialize junction type copied = sizeof(uint8_t); this->type = (enum JunctType)buffer[offset]; offset += copied; // Deserialize alignment column copied = sizeof(column_index); memcpy(&this->alignment_column, &buffer[offset], copied); offset += copied; return offset; } /** * A stateful scanner used to parse junction lists and proofs. */ struct Scanner { // The nested junction lists at the current lexer position. Array(struct JunctList) jlists; // The nested proofs at the current lexer position. Array(proof_level) proofs; // The level of the last proof. proof_level last_proof_level; // Whether we have seen a PROOF token. bool have_seen_proof_keyword; }; /** * Serializes the Scanner state into the given buffer. * * @param this The Scanner state to serialize. * @param buffer The buffer into which to serialize the scanner state. * @param is_dry_run Whether to actually copy the bytes to the buffer. * @return Number of bytes written into the buffer. */ static unsigned scanner_try_serialize( const struct Scanner* const this, char* const buffer, const bool is_dry_run ) { unsigned offset = 0; unsigned copied = 0; const nest_address jlist_depth = (nest_address)(this->jlists.size); copied = sizeof(nest_address); if (!is_dry_run) { memcpy(&buffer[offset], &jlist_depth, copied); } offset += copied; for (nest_address i = 0; i < jlist_depth; i++) { char* const buffer_addr = is_dry_run ? NULL : &buffer[offset]; copied = jlist_serialize(array_get(&this->jlists, i), buffer_addr, is_dry_run); offset += copied; } const nest_address proof_depth = (nest_address)(this->proofs.size); copied = sizeof(nest_address); if (!is_dry_run) { memcpy(&buffer[offset], &proof_depth, copied); } offset += copied; copied = proof_depth * sizeof(proof_level); if (!is_dry_run && copied > 0) { memcpy(&buffer[offset], this->proofs.contents, copied); } offset += copied; copied = sizeof(proof_level); if (!is_dry_run) { memcpy(&buffer[offset], &this->last_proof_level, copied); } offset += copied; copied = sizeof(uint8_t); if (!is_dry_run) { buffer[offset] = (uint8_t)(this->have_seen_proof_keyword); } offset += copied; return offset; } /** * Serializes the Scanner state into the given buffer. * * @param this The Scanner state to serialize. * @param buffer The buffer into which to serialize the scanner state. * @return Number of bytes written into the buffer. */ static unsigned scanner_serialize(const struct Scanner* this, char* buffer) { return scanner_try_serialize(this, buffer, false); } /** * Calculates the serialized size of the scanner. * * @param this The Scanner state to find the deserialized size of. * @return The size of the Scanner when serialized. */ static unsigned scanner_serialized_size(const struct Scanner* const this) { return scanner_try_serialize(this, NULL, true); } /** * Deserializes the Scanner state from the given buffer. * * @param this The Scanner state to deserialize. * @param buffer The buffer from which to deserialize the state. * @param length The bytes available to read from the buffer. */ static void scanner_deserialize(struct Scanner* const this, const char* const buffer, unsigned const length) { // Very important to clear values of all fields here! // Scanner object is reused; if a variable isn't cleared, it can // lead to extremely strange & impossible-to-debug behavior. array_delete(&this->jlists); array_delete(&this->proofs); this->last_proof_level = -1; this->have_seen_proof_keyword = false; if (length > 0) { unsigned offset = 0; unsigned copied = 0; nest_address jlist_depth = 0; copied = sizeof(nest_address); memcpy(&jlist_depth, &buffer[offset], copied); array_grow_by(&(this->jlists), jlist_depth); offset += copied; for (nest_address i = 0; i < jlist_depth; i++) { assert(offset < length); copied = jlist_deserialize(array_get(&(this->jlists), i), &buffer[offset]); offset += copied; } nest_address proof_depth = 0; copied = sizeof(nest_address); memcpy(&proof_depth, &buffer[offset], copied); array_grow_by(&(this->proofs), proof_depth); offset += copied; copied = proof_depth * sizeof(proof_level); if (copied > 0) { memcpy(this->proofs.contents, &buffer[offset], copied); } offset += copied; copied = sizeof(proof_level); memcpy(&(this->last_proof_level), &buffer[offset], copied); offset += copied; copied = sizeof(uint8_t); this->have_seen_proof_keyword = (bool)(buffer[offset] & 1); offset += copied; assert(offset == length); } } /** * Initializes a new instance of the Scanner object. * * @return A newly-created Scanner. */ static struct Scanner scanner_create() { struct Scanner s; array_init(&s.jlists); array_init(&s.proofs); s.last_proof_level = -1; s.have_seen_proof_keyword = false; return s; } /** * Frees all memory associated with this Scanner. * * @param this The Scanner to free. */ static void scanner_free(struct Scanner* const this) { array_delete(&this->jlists); array_delete(&this->proofs); } /** * Whether the Scanner state indicates we are currently in a jlist. * * @param this The Scanner state. * @return Whether we are in a jlist. */ static bool is_in_jlist(const struct Scanner* const this) { return this->jlists.size > 0; } /** * The column index of the current jlist. Returns negative number if * we are not currently in a jlist. * * @param this The Scanner state. * @return The column index of the current jlist. */ static column_index get_current_jlist_column_index(const struct Scanner* const this) { return is_in_jlist(this) ? array_back(&this->jlists)->alignment_column : -1; } /** * Whether the given jlist type matches the current jlist. * * @param this The Scanner state. * @param type The jlist type to check. * @return Whether the given jlist type matches the current jlist. */ static bool current_jlist_type_is( struct Scanner* const this, enum JunctType const type ) { return is_in_jlist(this) && type == array_back(&this->jlists)->type; } /** * Assuming the lexer is situated directly after a junct token, read * to the next non-whitespace char to check whether it is a , or ) token. * If so, this is not the start of a new jlist; instead, it is a higher- * level parameter to an operator, like op(x, /\) or op(\/, x). * * @param lexer The tree-sitter lexing control structure. */ static bool is_junct_token_higher_level_op_parameter(TSLexer* const lexer) { while (iswspace(lexer->lookahead) && has_next(lexer)) { lexer->advance(lexer, true); } return ',' == lexer->lookahead || ')' == lexer->lookahead; } /** * Emits an INDENT token, recording the new jlist in the Scanner state. * * @param this The Scanner state. * @param lexer The tree-sitter lexing control structure. * @param type The type of the new jlist. * @param col The column position of the new jlist. * @return Whether an INDENT token was emitted. */ static bool emit_indent( struct Scanner* const this, TSLexer* const lexer, enum JunctType const type, column_index const col ) { lexer->result_symbol = INDENT; struct JunctList new_list = create_junctlist(type, col); array_push(&this->jlists, new_list); return true; } /** * Emits a BULLET token, marking the start of a new item in the current * jlist. * * @param lexer The tree-sitter lexing control structure. * @return Whether a BULLET token was emitted. */ static bool emit_bullet(TSLexer* const lexer) { lexer->result_symbol = BULLET; return true; } /** * Emits a DEDENT token, removing a jlist from the Scanner state. * * @param this The Scanner state. * @param lexer The tree-sitter lexing control structure. * @return Whether a DEDENT token was emitted. */ static bool emit_dedent(struct Scanner* const this, TSLexer* const lexer) { if (is_in_jlist(this)) { lexer->result_symbol = DEDENT; (void)array_pop(&this->jlists); return true; } else { return false; } } /** * Jlists are identified with the column position (cpos) of the first * junct token in the list, and the junction type. For a given junct * token there are five possible interpretations: * 1. The junct is after the cpos of the current jlist, and an * INDENT token is expected * -> this is a new nested jlist, emit INDENT token * 2. The junct is after the cpos of the current jlist, and an * INDENT token is *not* expected * -> this is an infix junct operator; emit nothing * 3. The junct is equal to the cpos of the current jlist, and is * the same junct type (conjunction or disjunction) * -> this is an item of the current jlist; emit BULLET token * 4. The junct is equal to the cpos of the current jlist, and is * a DIFFERENT junct type (conjunction vs. disjunction) * -> this is an infix operator that also ends the current list * 5. The junct is prior to the cpos of the current jlist * -> this ends the current jlist, emit DEDENT token * * @param this The Scanner state. * @param lexer The tree-sitter lexing control structure. * @param valid_symbols Tokens possibly expected in this spot. * @param type The type of junction encountered. * @param next The column position of the junct token encountered. * @return Whether a jlist-relevant token should be emitted. */ static bool handle_junct_token( struct Scanner* const this, TSLexer* const lexer, const bool* const valid_symbols, enum JunctType const next_type, column_index const next_col ) { const column_index current_col = get_current_jlist_column_index(this); if (current_col < next_col) { if (valid_symbols[INDENT]) { if (is_junct_token_higher_level_op_parameter(lexer)) { /** * Handle case op(x, /\) or op(\/, x) - junct token is the first * token of a new expression and thus could be a new jlist, but * actually is a higher-level operator parameter. */ return false; } else { /** * The start of a new junction list! */ return emit_indent(this, lexer, next_type, next_col); } } else { /** * This is an infix junction symbol. Tree-sitter will only look for * a new jlist at the start of an expression rule; infix operators * occur when joining two expression rules together, so tree-sitter * is only looking for either BULLET or DEDENT rules. Examples: * * /\ a /\ b * ^ tree-sitter will NEVER look for an INDENT here * * /\ a * /\ b * ^ tree-sitter WILL look for a BULLET here * * /\ /\ a * ^ tree-sitter WILL look for an INDENT here */ return false; } } else if (current_col == next_col) { if (current_jlist_type_is(this, next_type)) { /** * This is another entry in the jlist. */ return emit_bullet(lexer); } else { /** * Disjunct in alignment with conjunct list or vice-versa; treat * this as an infix operator by terminating the current list. */ return emit_dedent(this, lexer); } } else { /** * Junct found prior to the alignment column of the current jlist. * This marks the end of the jlist. */ return emit_dedent(this, lexer); } } /** * If a given right delimiter matches some left delimiter that occurred * *before* the beginning of the current jlist, then that ends the * current jlist. The concept of a delimiter is not limited (hah) to * (), [], <<>>, and {}; it also includes IF/THEN, THEN/ELSE, CASE/->, * and basically every other language construct where an expression is * squeezed between a known start & end token. * * Previously I implemented complicated logic using a stack to keep * track of all the delimiters that have been seen (and their * pairs) but found that tree-sitter would never trigger the * external scanner before encountering a right delimiter matching * a left delimiter that started within the scope of a jlist. Thus * we can assume that when we *do* see a right delimiter, it * matches a left delimiter that occurred prior to the start of the * jlist, so we can emit a DEDENT token to end the jlist. Example: * * /\ ( a + b ) * ^ tree-sitter will never look for an INDENT, * BULLET, or DEDENT token here; it is only * looking for another infix operator or the * right-delimiter. * * ( /\ a + b ) * ^ tree-sitter WILL look for an INDENT, BULLET, or * DEDENT token here in addition to looking for an * infix operator; it also wants to see a DEDENT * token before seeing the right delimiter, although * error recovery is simple enough that it would * barely notice its absence. * * There are a few notable exceptions to this rule; for example, the * empty set or empty sequence: * * /\ { } * ^ * /\ << >> * ^ there is the option for an expression here, so tree-sitter * looks for INDENT tokens and we will see a right delimiter * in this external scanner. * * Another example when the code is in a non-parseable state which we * nonetheless wish to handle gracefully: * * /\ [x \in S |-> ] * ^ user is about to write an expression here, but * there is a time when the code is non-parseable; * tree-sitter will again look for an INDENT token * and we will see a right delimiter in this * external scanner. * * The easy solution to these cases is to simply check whether * tree-sitter is looking for a DEDENT token. If so, emit one; if not, * emit nothing. Tree-sitter will not look for a DEDENT token inside * enclosing delimiters within the scope of a jlist. * * One side-effect of all this is that tree-sitter parses certain * arrangements of jlists and delimiters that are actually illegal * according to TLA⁺ syntax rules; that is okay since tree-sitter's * use case of error-tolerant editor tooling ensures its design * errs on the side of being overly-permissive. For a concrete * example here, tree-sitter will parse this illegal expression * without complaint: * * /\ A * /\ (B + C * ) * /\ D * * This should simply be detected as an error at the semantic level. * * @param this The Scanner state. * @param lexer The tree-sitter lexing control structure. * @param valid_symbols Tokens possibly expected in this spot. * @return Whether a jlist-relevant token should be emitted. */ static bool handle_right_delimiter_token( struct Scanner* const this, TSLexer* const lexer, const bool* const valid_symbols ) { return is_in_jlist(this) && valid_symbols[DEDENT] && emit_dedent(this, lexer); } /** * Emits a dedent token if are in jlist and have encountered a token that * unconditionally ends a jlist regardless of column position; these * include: * 1. New unit definition (op == expr, etc.) * 2. End-of-module token (====) * 3. End-of-file (this shouldn't happen but we will end the jlist to * improve error reporting since the end-of-module token is missing) * * @param this The Scanner state. * @param lexer The tree-sitter lexing control structure. * @return Whether a jlist-relevant token should be emitted. */ static bool handle_terminator_token( struct Scanner* const this, TSLexer* const lexer ) { return is_in_jlist(this) && emit_dedent(this, lexer); } /** * Non-junct tokens could possibly indicate the end of a jlist. Rules: * - If the token cpos is leq to the current jlist cpos, the jlist * has ended; emit a DEDENT token (possibly multiple); example: * IF /\ P * /\ Q * THEN R * ELSE S * - Otherwise the token is treated as part of the expression in that * junct; for example: * /\ IF e THEN P * ELSE Q * /\ R * so emit no token. * * @param this The Scanner state. * @param lexer The tree-sitter lexing control structure. * @param next The column position of the encountered token. * @return Whether a jlist-relevant token should be emitted. */ static bool handle_other_token( struct Scanner* const this, TSLexer* const lexer, column_index const next ) { return is_in_jlist(this) && next <= get_current_jlist_column_index(this) && emit_dedent(this, lexer); } /** * Handles the infix !! operator. This has a lexical conflict with the * subexpression separator !, so an expression like A!!!B will be parsed * incorrectly as A !! (!B) instead of (A!) !! B. Ideally tree-sitter * would add negative-lookahead in regexes so this wouldn't have to be * corrected in the external scanner, but it is what it is. * * This function first checks whether the !! token is interfering with an * existing jlist. If not, it checks the next character to see whether it * is !. If so, this function emits false - no !! token found - under the * assumption that this is a A!!!B scenario so this string should be * split into (!)(!!) instead of (!!)(!). * * Note there is a case A!!!!B which should be grouped as (A!) (!!) (!B) * but will not be according to these rules. The workaround for this case * (as with several other lexing ambiguities in this language) is to * insert a space for disambiguation, like A!!! !B. Humorously, this does * mean that !!!!!!!!!!!!!!!!!!!!!! (ad infinitum) is valid TLA+ syntax. * * @param this The Scanner state. * @param lexer The tree-sitter lexing control structure. * @param next The column position of the encountered token. */ static bool handle_double_excl_token( struct Scanner* const this, TSLexer* const lexer, column_index const next ) { if (handle_other_token(this, lexer, next)) { // This token is affecting a jlist, emit dedent return true; } else { if ('!' == lexer->lookahead) { return false; } else { lexer->mark_end(lexer); lexer->result_symbol = DOUBLE_EXCL; return true; } } } /** * Gets whether we are currently in a proof. * * @param this The Scanner state. * @return Whether we are currently in a proof. */ static bool is_in_proof(const struct Scanner* const this) { return this->proofs.size > 0; } /** * Gets the current proof level; -1 if none. * * @param this The Scanner state. * @return The current proof level. */ static proof_level get_current_proof_level(const struct Scanner* const this) { return is_in_proof(this) ? *array_back(&this->proofs) : -1; } /** * Emits a token indicating the start of a new proof. * * @param this The Scanner state. * @param lexer The tree-sitter lexing control structure. * @param level The level of the new proof. * @return Whether a token should be emitted. */ static bool emit_begin_proof( struct Scanner* const this, TSLexer* const lexer, proof_level level ) { lexer->result_symbol = BEGIN_PROOF; array_push(&this->proofs, level); this->last_proof_level = level; this->have_seen_proof_keyword = false; return true; } /** * Emits a token indicating the start of a new proof step. * * @param this The Scanner state. * @param lexer The tree-sitter lexing control structure. * @param level The level of the new proof step. * @return Whether a token should be emitted. */ static bool emit_begin_proof_step( struct Scanner* const this, TSLexer* const lexer, proof_level level ) { this->last_proof_level = level; lexer->result_symbol = BEGIN_PROOF_STEP; return true; } /** * Handle encountering a new proof step ID. This probably marks the * beginning of a new proof step, but could also be a reference to a * prior proof step as part of an expression. There are also various * interactions between the proof step ID and jlists. Cases: * 1. A proof step token is expected * -> This is a new proof step; see proof step logic below * 2. A proof step token is *not* expected, and a DEDENT token *is* * -> This is the beginning of a proof step but there is an open * jlist which must first be closed; emit a DEDENT token. * 3. A proof step token is not expected, and neither is a DEDENT * -> This is a proof step reference, so treat as other token. * P => <1>b * ^ tree-sitter will only look for INDENT here * * For handling proof steps alone, there are the following cases: * 1. The new proof token level is greater than the current level * -> This is the start of a new proof; emit BEGIN_PROOF token * and push level to proof stack. Set last_proof_level to * the new proof level. * 2. The new proof token level is equal to the current level * -> This is another proof step; emit BEGIN_PROOF_STEP token. * 3. The new proof token level is less than the current level * -> This is an error, which we will try to recover from. * * There are also rules to handle proof step IDs where the level is * inferred, like <+> and <*>. They are as follows: * 1. The proof step ID is <+> * -> This is the start of a new proof; its level is one higher * than last_proof_level. * 2. The proof step ID is <*> and we are not inside a proof * -> This is the start of the very first proof; its level is one * higher than last_proof_level, which should be -1; thus the * proof level should be 0. * 3. The proof step ID is <*> and it directly follows a PROOF keyword * -> This is the start of a new proof; its level is one higher * than last_proof_level. * 4. The proof step ID is <*> and it *does not* follow a PROOF keyword * -> This is another step in the same proof; its level is the * same as last_proof_level. * * Proofs are ended upon encountering a QED step, which is handled * elsewhere. * * @param this The Scanner state. * @param lexer The tree-sitter lexing control structure. * @param valid_symbols Tokens possibly expected in this spot. * @param next The column position of the encountered token. * @return Whether a token should be emitted. */ static bool handle_proof_step_id_token( struct Scanner* const this, TSLexer* const lexer, const bool* const valid_symbols, column_index const next, struct ProofStepId proof_step_id_token ) { assert(ProofStepIdType_NONE != proof_step_id_token.type); if (valid_symbols[BEGIN_PROOF] || valid_symbols[BEGIN_PROOF_STEP]) { proof_level next_proof_level = -1; const proof_level current_proof_level = get_current_proof_level(this); switch (proof_step_id_token.type) { case ProofStepIdType_STAR: /** * <*> can start a new proof only at the very first level, * or directly following a PROOF keyword. */ next_proof_level = !is_in_proof(this) || this->have_seen_proof_keyword ? this->last_proof_level + 1 : current_proof_level; break; case ProofStepIdType_PLUS: /** * This keeps us from entering an infinite loop when we see * a <+> proof step ID; the first time we encounter the <+>, * we will increase the level and emit a BEGIN_PROOF token. * The second time, we mark it as the same level and emit a * BEGIN_PROOF_STEP token. */ next_proof_level = valid_symbols[BEGIN_PROOF] ? this->last_proof_level + 1 : current_proof_level; break; case ProofStepIdType_NUMBERED: next_proof_level = proof_step_id_token.level; break; default: return false; } if (next_proof_level > current_proof_level) { return emit_begin_proof(this, lexer, next_proof_level); } else if (next_proof_level == current_proof_level) { if (this->have_seen_proof_keyword) { // This has been declared a new proof using the PROOF keyword // but does not have a level greater than the old; thus we've // detected a syntax error. // TODO: handle this. return false; } else { return emit_begin_proof_step(this, lexer, next_proof_level); } } else { // The next proof level is lower than the current. This is // invalid syntax. // TODO: handle this. return false; } } else { if (valid_symbols[DEDENT]) { // End all jlists before start of proof. return handle_terminator_token(this, lexer); } else { // This is a reference to a proof step in an expression. return handle_other_token(this, lexer, next); } } } /** * Handles the PROOF keyword token. We record that we've seen the * PROOF keyword, which modifies the interpretation of the subsequent * proof step ID. The PROOF token also terminates any current jlist. * * @param this The Scanner state. * @param lexer The tree-sitter lexing control structure. * @param valid_symbols Tokens possibly expected in this spot. * @return Whether a token should be emitted. */ static bool handle_proof_keyword_token( struct Scanner* const this, TSLexer* const lexer, const bool* const valid_symbols ) { if (valid_symbols[PROOF_KEYWORD]) { this->have_seen_proof_keyword = true; lexer->result_symbol = PROOF_KEYWORD; lexer->mark_end(lexer); return true; } else { return handle_terminator_token(this, lexer); } } /** * Handles the BY, OBVIOUS, and OMITTED keyword tokens. We record * that we've seen the keyword, which negates any PROOF keyword * previously encountered. These tokens also terminate any current * jlist. * * @param this The Scanner state. * @param lexer The tree-sitter lexing control structure. * @param valid_symbols Tokens possibly expected in this spot. * @param keyword_type The specific keyword being handled. * @return Whether a token should be emitted. */ static bool handle_terminal_proof_keyword_token( struct Scanner* const this, TSLexer* const lexer, const bool* const valid_symbols, enum TokenType keyword_type ) { if (valid_symbols[keyword_type]) { this->have_seen_proof_keyword = false; lexer->result_symbol = keyword_type; lexer->mark_end(lexer); return true; } else { return handle_terminator_token(this, lexer); } } /** * Handles the QED keyword token. The QED token indicates this is the * final step of a proof, so we modify the state accordingly. First * we record the current proof level in case there is a child proof * of this step that uses <+> or PROOF <*> for its first step. Then * we pop the top proof level off the stack. * * It's possible to encounter a QED keyword while not inside of a proof * as part of an earlier syntax error, and proof step IDs being treated * as sequences of < and > operators. In this case the current proof * state should not be modified, but a QED keyword token is still * returned to help the error recovery process. Not performing this * check previously led to a segfault; see: * https://github.com/tlaplus-community/tree-sitter-tlaplus/issues/60 * * @param this The Scanner state. * @param lexer The tree-sitter lexing control structure. * @return Whether a token should be emitted. */ static bool handle_qed_keyword_token( struct Scanner* const this, TSLexer* const lexer ) { if (is_in_proof(this)) { this->last_proof_level = get_current_proof_level(this); (void)array_pop(&this->proofs); } lexer->result_symbol = QED_KEYWORD; lexer->mark_end(lexer); return true; } /** * Handles the fairness tokens WF_ and SF_. * Need to handle this in an external scanner due to: * https://github.com/tree-sitter/tree-sitter/issues/1615 * * @param this The Scanner state. * @param lexer The tree-sitter lexing control structure. * @param next The column position of the encountered token. * @param keyword_type The specific keyword being handled. * @return Whether a token should be emitted. */ static bool handle_fairness_keyword_token( struct Scanner* const this, TSLexer* const lexer, column_index const next, enum TokenType keyword_type ) { if (handle_other_token(this, lexer, next)) { return true; } else { lexer->result_symbol = keyword_type; lexer->mark_end(lexer); return true; } } /** * Scans for various possible external tokens. * * @param this The Scanner state. * @param lexer The tree-sitter lexing control structure. * @param valid_symbols Tokens possibly expected in this spot. * @return Whether a token was encountered. */ static bool scan( struct Scanner* const this, TSLexer* const lexer, const bool* const valid_symbols ) { // All symbols are marked as valid during error recovery. // We can check for this by looking at the validity of the final // (unused) external symbol, ERROR_SENTINEL. const bool is_error_recovery = valid_symbols[ERROR_SENTINEL]; // TODO: actually function during error recovery // https://github.com/tlaplus-community/tree-sitter-tlaplus/issues/19 if (is_error_recovery) { return false; } if(valid_symbols[LEADING_EXTRAMODULAR_TEXT] || valid_symbols[TRAILING_EXTRAMODULAR_TEXT]) { return scan_extramodular_text(lexer, valid_symbols); } else { column_index col = -1; CharArray proof_step_id_level = array_new(); enum Token token = tokenize_lexeme(lex_lookahead(lexer, &col, &proof_step_id_level)); struct ProofStepId proof_step_id_token = parse_proof_step_id(&proof_step_id_level); array_delete(&proof_step_id_level); switch (token) { case Token_LAND: return handle_junct_token(this, lexer, valid_symbols, JunctType_CONJUNCTION, col); case Token_LOR: return handle_junct_token(this, lexer, valid_symbols, JunctType_DISJUNCTION, col); case Token_RIGHT_DELIMITER: return handle_right_delimiter_token(this, lexer, valid_symbols); case Token_COMMENT_START: return false; case Token_TERMINATOR: return handle_terminator_token(this, lexer); case Token_PROOF_STEP_ID: return handle_proof_step_id_token(this, lexer, valid_symbols, col, proof_step_id_token); case Token_PROOF_KEYWORD: return handle_proof_keyword_token(this, lexer, valid_symbols); case Token_BY_KEYWORD: return handle_terminal_proof_keyword_token(this, lexer, valid_symbols, BY_KEYWORD); case Token_OBVIOUS_KEYWORD: return handle_terminal_proof_keyword_token(this, lexer, valid_symbols, OBVIOUS_KEYWORD); case Token_OMITTED_KEYWORD: return handle_terminal_proof_keyword_token(this, lexer, valid_symbols, OMITTED_KEYWORD); case Token_QED_KEYWORD: return handle_qed_keyword_token(this, lexer); case Token_WEAK_FAIRNESS: return handle_fairness_keyword_token(this, lexer, col, WEAK_FAIRNESS); case Token_STRONG_FAIRNESS: return handle_fairness_keyword_token(this, lexer, col, STRONG_FAIRNESS); case Token_DOUBLE_EXCL: return handle_double_excl_token(this, lexer, col); case Token_OTHER: return handle_other_token(this, lexer, col); default: return false; } } } /** * A hierarchy of nested stateful scanners. * Each time a PlusCal block is entered, a nested context is created. * Exiting the PlusCal block exits the context. * Multiply-nested PlusCal blocks are supported. */ struct NestedScanner { // The enclosing context(s) of the PlusCal block. Array(CharArray) enclosing_contexts; // The currently-active context. struct Scanner current_context; }; /** * Serialize the nested scanner into a buffer. * * @param this The NestedScanner state. * @param buffer The buffer to serialize the state into. * @return The number of bytes written into the buffer. */ static unsigned nested_scanner_serialize( const struct NestedScanner* const this, char* const buffer ) { unsigned offset = 0; unsigned copied = 0; // First write number of enclosing contexts (guaranteed to be >= 1) nest_address const context_depth = this->enclosing_contexts.size + 1; copied = sizeof(nest_address); if (copied > 0) memcpy(&buffer[offset], &context_depth, copied); offset += copied; // Then write size of N-1 enclosing contexts for (int i = 0; i < context_depth - 1; i++) { unsigned const context_size = array_get(&this->enclosing_contexts, i)->size; copied = sizeof(unsigned); if (copied > 0) memcpy(&buffer[offset], &context_size, copied); offset += copied; } // Reserve space for current context size unsigned const current_context_size_offset = offset; copied = sizeof(unsigned); offset += copied; // Serialize N-1 enclosing contexts for (unsigned i = 0; i < this->enclosing_contexts.size; i++) { CharArray* context = array_get(&this->enclosing_contexts, i); copied = context->size; if (copied > 0) memcpy(&buffer[offset], context->contents, copied); offset += copied; } // Serialize current context copied = scanner_serialize(&this->current_context, &buffer[offset]); offset += copied; // Write current context size to reserved position memcpy(&buffer[current_context_size_offset], &copied, sizeof(unsigned)); return offset; } /** * Deserialize a nested scanner. * * @param this The nested scanner instance to deserialize into. * @param buffer The buffer to deserialize from. * @param length The number of bytes in the buffer. */ static void nested_scanner_deserialize( struct NestedScanner* const this, const char* const buffer, unsigned const length ) { for (unsigned i = 0; i < this->enclosing_contexts.size; i++) { array_delete(array_get(&this->enclosing_contexts, i)); } array_delete(&this->enclosing_contexts); scanner_deserialize(&this->current_context, NULL, 0); if (length > 0) { unsigned offset = 0; unsigned copied = 0; // First item: total number of contexts (guaranteed to be >= 1) nest_address context_depth = 0; copied = sizeof(nest_address); memcpy(&context_depth, &buffer[offset], copied); assert(1 <= context_depth); array_grow_by(&this->enclosing_contexts, context_depth - 1); offset += copied; // Next N items: size of all contexts Array(unsigned) context_sizes = array_new(); array_grow_by(&context_sizes, context_depth); copied = context_depth * sizeof(unsigned); if (copied > 0 && context_sizes.contents != NULL) memcpy(context_sizes.contents, &buffer[offset], copied); offset += copied; // Deserialize N-1 contexts as enclosing contexts for (int i = 0; i < context_depth - 1; i++) { copied = *array_get(&context_sizes, i); array_grow_by(array_get(&this->enclosing_contexts, i), copied); if (copied > 0) memcpy(array_get(&this->enclosing_contexts, i)->contents, &buffer[offset], copied); offset += copied; } // Final context is deserialized as current context copied = *array_back(&context_sizes); scanner_deserialize(&this->current_context, &buffer[offset], copied); offset += copied; array_delete(&context_sizes); assert(offset == length); } } /** * Initializes a new instance of the NestedScanner object. * * @param this The NestedScanner to initialize. */ static void nested_scanner_init(struct NestedScanner* const this) { array_init(&this->enclosing_contexts); this->current_context = scanner_create(); } /** * Frees all memory allocated by the nested scanner. * * @param this The NestedScanner to free. */ static void nested_scanner_free(struct NestedScanner* const this) { for (unsigned i = 0; i < this->enclosing_contexts.size; i++) { array_delete(array_get(&this->enclosing_contexts, i)); } array_delete(&this->enclosing_contexts); scanner_free(&this->current_context); } static bool nested_scan( struct NestedScanner* const this, TSLexer* const lexer, const bool* const valid_symbols) { // All symbols are marked as valid during error recovery. // We can check for this by looking at the validity of the final // (unused) external symbol, ERROR_SENTINEL. if (valid_symbols[ERROR_SENTINEL]) { return false; } else if (valid_symbols[PCAL_START]) { // Entering PlusCal block; push current context then clear unsigned const expected_size = scanner_serialized_size(&this->current_context); CharArray serialized_current_context = array_new(); array_grow_by(&serialized_current_context, expected_size); unsigned const actual_size = scanner_serialize(&this->current_context, serialized_current_context.contents); assert(expected_size == actual_size); array_push(&this->enclosing_contexts, serialized_current_context); scanner_free(&this->current_context); this->current_context = scanner_create(); lexer->result_symbol = PCAL_START; return true; } else if (valid_symbols[PCAL_END] && this->enclosing_contexts.size > 0) { // Exiting PlusCal block; rehydrate context then pop CharArray* next = array_back(&this->enclosing_contexts); scanner_deserialize(&this->current_context, next->contents, next->size); array_delete(&array_pop(&this->enclosing_contexts)); lexer->result_symbol = PCAL_END; return true; } else { return scan(&this->current_context, lexer, valid_symbols); } } // Called once when language is set on a parser. // Allocates memory for storing scanner state. void* tree_sitter_tlaplus_external_scanner_create() { struct NestedScanner* scanner = ts_malloc(sizeof(struct NestedScanner)); nested_scanner_init(scanner); return scanner; } // Called once parser is deleted or different language set. // Frees memory storing scanner state. void tree_sitter_tlaplus_external_scanner_destroy(void* const payload) { struct NestedScanner* const scanner = (struct NestedScanner*)(payload); nested_scanner_free(scanner); ts_free(scanner); } // Called whenever this scanner recognizes a token. // Serializes scanner state into buffer. unsigned tree_sitter_tlaplus_external_scanner_serialize( void* const payload, char* const buffer ) { const struct NestedScanner* const scanner = (struct NestedScanner*)(payload); return nested_scanner_serialize(scanner, buffer); } // Called when handling edits and ambiguities. // Deserializes scanner state from buffer. void tree_sitter_tlaplus_external_scanner_deserialize( void* const payload, const char* const buffer, unsigned const length ) { struct NestedScanner* const scanner = (struct NestedScanner*)(payload); nested_scanner_deserialize(scanner, buffer, length); } // Scans for tokens. bool tree_sitter_tlaplus_external_scanner_scan( void* const payload, TSLexer* const lexer, const bool* const valid_symbols ) { struct NestedScanner* const scanner = (struct NestedScanner*)(payload); return nested_scan(scanner, lexer, valid_symbols); }