From ece43957c97d7208a381dbd3475edddc98149452 Mon Sep 17 00:00:00 2001 From: William Ball Date: Thu, 21 Nov 2024 13:14:46 -0800 Subject: [PATCH] added block comments --- grammar.js | 23 +- src/grammar.json | 65 +- src/node-types.json | 8 +- src/parser.c | 1235 ++++++++++++++++++----------------- test/corpus/application.txt | 66 ++ test/corpus/arrows.txt | 59 +- test/corpus/axioms.txt | 11 +- test/corpus/comments.txt | 7 +- test/corpus/labs.txt | 29 +- test/corpus/pabs.txt | 29 +- 10 files changed, 853 insertions(+), 679 deletions(-) create mode 100644 test/corpus/application.txt diff --git a/grammar.js b/grammar.js index 0abba60..07be47c 100644 --- a/grammar.js +++ b/grammar.js @@ -10,17 +10,32 @@ module.exports = grammar({ name: "perga", + extras: $ => [ + $.comment, + $.block_comment, + /\s/, + ], + rules: { - program : $ => repeat(choice( - $.definition, - $.comment, - )), + program : $ => repeat($.definition), identifier : $ => /[a-zA-Z_]\w*/, comment : $ => token(seq('--', /.*/)), + block_comment: $ => token(seq( + '[*', + repeat(choice( + /[^\[\]*]/, + /\[[^*]/, + /\*[^\]]/, + /\[\*/, + /\*\]/, + )), + '*]' + )), + param_block : $ => seq( '(', field('param', repeat($.identifier)), diff --git a/src/grammar.json b/src/grammar.json index 4a66ad5..9c8c4ca 100644 --- a/src/grammar.json +++ b/src/grammar.json @@ -4,17 +4,8 @@ "program": { "type": "REPEAT", "content": { - "type": "CHOICE", - "members": [ - { - "type": "SYMBOL", - "name": "definition" - }, - { - "type": "SYMBOL", - "name": "comment" - } - ] + "type": "SYMBOL", + "name": "definition" } }, "identifier": { @@ -37,6 +28,50 @@ ] } }, + "block_comment": { + "type": "TOKEN", + "content": { + "type": "SEQ", + "members": [ + { + "type": "STRING", + "value": "[*" + }, + { + "type": "REPEAT", + "content": { + "type": "CHOICE", + "members": [ + { + "type": "PATTERN", + "value": "[^\\[\\]*]" + }, + { + "type": "PATTERN", + "value": "\\[[^*]" + }, + { + "type": "PATTERN", + "value": "\\*[^\\]]" + }, + { + "type": "PATTERN", + "value": "\\[\\*" + }, + { + "type": "PATTERN", + "value": "\\*\\]" + } + ] + } + }, + { + "type": "STRING", + "value": "*]" + } + ] + } + }, "param_block": { "type": "SEQ", "members": [ @@ -342,6 +377,14 @@ } }, "extras": [ + { + "type": "SYMBOL", + "name": "comment" + }, + { + "type": "SYMBOL", + "name": "block_comment" + }, { "type": "PATTERN", "value": "\\s" diff --git a/src/node-types.json b/src/node-types.json index 72a3bf1..ff15e43 100644 --- a/src/node-types.json +++ b/src/node-types.json @@ -201,10 +201,6 @@ "multiple": true, "required": false, "types": [ - { - "type": "comment", - "named": true - }, { "type": "definition", "named": true @@ -284,6 +280,10 @@ "type": "axiom", "named": true }, + { + "type": "block_comment", + "named": true + }, { "type": "comment", "named": true diff --git a/src/parser.c b/src/parser.c index aacf927..48535cd 100644 --- a/src/parser.c +++ b/src/parser.c @@ -6,10 +6,10 @@ #define LANGUAGE_VERSION 14 #define STATE_COUNT 50 -#define LARGE_STATE_COUNT 5 -#define SYMBOL_COUNT 37 +#define LARGE_STATE_COUNT 12 +#define SYMBOL_COUNT 38 #define ALIAS_COUNT 0 -#define TOKEN_COUNT 21 +#define TOKEN_COUNT 22 #define EXTERNAL_TOKEN_COUNT 0 #define FIELD_COUNT 3 #define MAX_ALIAS_SEQUENCE_LENGTH 6 @@ -18,46 +18,48 @@ enum ts_symbol_identifiers { sym_identifier = 1, sym_comment = 2, - anon_sym_LPAREN = 3, - anon_sym_COLON = 4, - anon_sym_RPAREN = 5, - sym_star = 6, - anon_sym_u25a1 = 7, - anon_sym_LBRACK_RBRACK = 8, - anon_sym_u03bb = 9, - anon_sym_fun = 10, - anon_sym_EQ_GT = 11, - anon_sym_u21d2 = 12, - anon_sym_u220f = 13, - anon_sym_forall = 14, - anon_sym_COMMA = 15, - sym_axiom = 16, - anon_sym_DASH_GT = 17, - anon_sym_u2192 = 18, - anon_sym_COLON_EQ = 19, - anon_sym_SEMI = 20, - sym_program = 21, - sym_param_block = 22, - sym_square = 23, - sym_labs = 24, - sym_pabs = 25, - sym_term = 26, - sym_app = 27, - sym_arrow = 28, - sym_app_term = 29, - sym_expr = 30, - sym_ascription = 31, - sym_definition = 32, - aux_sym_program_repeat1 = 33, - aux_sym_param_block_repeat1 = 34, - aux_sym_labs_repeat1 = 35, - aux_sym_app_repeat1 = 36, + sym_block_comment = 3, + anon_sym_LPAREN = 4, + anon_sym_COLON = 5, + anon_sym_RPAREN = 6, + sym_star = 7, + anon_sym_u25a1 = 8, + anon_sym_LBRACK_RBRACK = 9, + anon_sym_u03bb = 10, + anon_sym_fun = 11, + anon_sym_EQ_GT = 12, + anon_sym_u21d2 = 13, + anon_sym_u220f = 14, + anon_sym_forall = 15, + anon_sym_COMMA = 16, + sym_axiom = 17, + anon_sym_DASH_GT = 18, + anon_sym_u2192 = 19, + anon_sym_COLON_EQ = 20, + anon_sym_SEMI = 21, + sym_program = 22, + sym_param_block = 23, + sym_square = 24, + sym_labs = 25, + sym_pabs = 26, + sym_term = 27, + sym_app = 28, + sym_arrow = 29, + sym_app_term = 30, + sym_expr = 31, + sym_ascription = 32, + sym_definition = 33, + aux_sym_program_repeat1 = 34, + aux_sym_param_block_repeat1 = 35, + aux_sym_labs_repeat1 = 36, + aux_sym_app_repeat1 = 37, }; static const char * const ts_symbol_names[] = { [ts_builtin_sym_end] = "end", [sym_identifier] = "identifier", [sym_comment] = "comment", + [sym_block_comment] = "block_comment", [anon_sym_LPAREN] = "(", [anon_sym_COLON] = ":", [anon_sym_RPAREN] = ")", @@ -98,6 +100,7 @@ static const TSSymbol ts_symbol_map[] = { [ts_builtin_sym_end] = ts_builtin_sym_end, [sym_identifier] = sym_identifier, [sym_comment] = sym_comment, + [sym_block_comment] = sym_block_comment, [anon_sym_LPAREN] = anon_sym_LPAREN, [anon_sym_COLON] = anon_sym_COLON, [anon_sym_RPAREN] = anon_sym_RPAREN, @@ -147,6 +150,10 @@ static const TSSymbolMetadata ts_symbol_metadata[] = { .visible = true, .named = true, }, + [sym_block_comment] = { + .visible = true, + .named = true, + }, [anon_sym_LPAREN] = { .visible = true, .named = false, @@ -383,235 +390,262 @@ static bool ts_lex(TSLexer *lexer, TSStateId state) { eof = lexer->eof(lexer); switch (state) { case 0: - if (eof) ADVANCE(6); + if (eof) ADVANCE(10); ADVANCE_MAP( - '(', 19, - ')', 21, - '*', 22, - ',', 31, - '-', 2, - ':', 20, - ';', 36, - '=', 3, - '[', 4, - 'a', 16, - 'f', 13, - 0x3bb, 25, - 0x2192, 34, - 0x21d2, 28, - 0x220f, 29, - 0x25a1, 23, + '(', 24, + ')', 26, + '*', 27, + ',', 36, + '-', 5, + ':', 25, + ';', 41, + '=', 6, + '[', 2, + 'a', 20, + 'f', 17, + 0x3bb, 30, + 0x2192, 39, + 0x21d2, 33, + 0x220f, 34, + 0x25a1, 28, ); if (('\t' <= lookahead && lookahead <= '\r') || lookahead == ' ') SKIP(0); if (('A' <= lookahead && lookahead <= 'Z') || lookahead == '_' || - ('b' <= lookahead && lookahead <= 'z')) ADVANCE(17); + ('b' <= lookahead && lookahead <= 'z')) ADVANCE(21); END_STATE(); case 1: - if (lookahead == '(') ADVANCE(19); - if (lookahead == '*') ADVANCE(22); - if (lookahead == '[') ADVANCE(4); - if (lookahead == 'f') ADVANCE(13); - if (lookahead == 0x3bb) ADVANCE(25); - if (lookahead == 0x220f) ADVANCE(29); - if (lookahead == 0x25a1) ADVANCE(23); + ADVANCE_MAP( + '(', 24, + '*', 27, + '-', 4, + '[', 2, + 'f', 17, + 0x3bb, 30, + 0x220f, 34, + 0x25a1, 28, + ); if (('\t' <= lookahead && lookahead <= '\r') || lookahead == ' ') SKIP(1); if (('A' <= lookahead && lookahead <= 'Z') || lookahead == '_' || - ('a' <= lookahead && lookahead <= 'z')) ADVANCE(17); + ('a' <= lookahead && lookahead <= 'z')) ADVANCE(21); END_STATE(); case 2: - if (lookahead == '-') ADVANCE(18); - if (lookahead == '>') ADVANCE(33); + if (lookahead == '*') ADVANCE(3); + if (lookahead == ']') ADVANCE(29); END_STATE(); case 3: - if (lookahead == '>') ADVANCE(27); + if (lookahead == '*') ADVANCE(7); + if (lookahead == '[') ADVANCE(8); + if (lookahead != 0 && + lookahead != ']') ADVANCE(3); END_STATE(); case 4: - if (lookahead == ']') ADVANCE(24); + if (lookahead == '-') ADVANCE(22); END_STATE(); case 5: - if (eof) ADVANCE(6); - ADVANCE_MAP( - '(', 19, - ')', 21, - '*', 22, - '-', 2, - ':', 20, - ';', 36, - '[', 4, - 0x2192, 34, - 0x25a1, 23, - ); - if (('\t' <= lookahead && lookahead <= '\r') || - lookahead == ' ') SKIP(5); - if (('A' <= lookahead && lookahead <= 'Z') || - lookahead == '_' || - ('a' <= lookahead && lookahead <= 'z')) ADVANCE(17); + if (lookahead == '-') ADVANCE(22); + if (lookahead == '>') ADVANCE(38); END_STATE(); case 6: - ACCEPT_TOKEN(ts_builtin_sym_end); + if (lookahead == '>') ADVANCE(32); END_STATE(); case 7: - ACCEPT_TOKEN(sym_identifier); - if (lookahead == 'a') ADVANCE(10); - if (('0' <= lookahead && lookahead <= '9') || - ('A' <= lookahead && lookahead <= 'Z') || - lookahead == '_' || - ('b' <= lookahead && lookahead <= 'z')) ADVANCE(17); + if (lookahead == ']') ADVANCE(23); + if (lookahead != 0) ADVANCE(3); END_STATE(); case 8: - ACCEPT_TOKEN(sym_identifier); - if (lookahead == 'i') ADVANCE(14); - if (('0' <= lookahead && lookahead <= '9') || - ('A' <= lookahead && lookahead <= 'Z') || - lookahead == '_' || - ('a' <= lookahead && lookahead <= 'z')) ADVANCE(17); + if (lookahead != 0) ADVANCE(3); END_STATE(); case 9: - ACCEPT_TOKEN(sym_identifier); - if (lookahead == 'l') ADVANCE(30); - if (('0' <= lookahead && lookahead <= '9') || - ('A' <= lookahead && lookahead <= 'Z') || + if (eof) ADVANCE(10); + ADVANCE_MAP( + '(', 24, + ')', 26, + '*', 27, + '-', 5, + ':', 25, + ';', 41, + '[', 2, + 0x2192, 39, + 0x25a1, 28, + ); + if (('\t' <= lookahead && lookahead <= '\r') || + lookahead == ' ') SKIP(9); + if (('A' <= lookahead && lookahead <= 'Z') || lookahead == '_' || - ('a' <= lookahead && lookahead <= 'z')) ADVANCE(17); + ('a' <= lookahead && lookahead <= 'z')) ADVANCE(21); END_STATE(); case 10: - ACCEPT_TOKEN(sym_identifier); - if (lookahead == 'l') ADVANCE(9); - if (('0' <= lookahead && lookahead <= '9') || - ('A' <= lookahead && lookahead <= 'Z') || - lookahead == '_' || - ('a' <= lookahead && lookahead <= 'z')) ADVANCE(17); + ACCEPT_TOKEN(ts_builtin_sym_end); END_STATE(); case 11: ACCEPT_TOKEN(sym_identifier); - if (lookahead == 'm') ADVANCE(32); + if (lookahead == 'a') ADVANCE(14); if (('0' <= lookahead && lookahead <= '9') || ('A' <= lookahead && lookahead <= 'Z') || lookahead == '_' || - ('a' <= lookahead && lookahead <= 'z')) ADVANCE(17); + ('b' <= lookahead && lookahead <= 'z')) ADVANCE(21); END_STATE(); case 12: ACCEPT_TOKEN(sym_identifier); - if (lookahead == 'n') ADVANCE(26); + if (lookahead == 'i') ADVANCE(18); if (('0' <= lookahead && lookahead <= '9') || ('A' <= lookahead && lookahead <= 'Z') || lookahead == '_' || - ('a' <= lookahead && lookahead <= 'z')) ADVANCE(17); + ('a' <= lookahead && lookahead <= 'z')) ADVANCE(21); END_STATE(); case 13: ACCEPT_TOKEN(sym_identifier); - if (lookahead == 'o') ADVANCE(15); - if (lookahead == 'u') ADVANCE(12); + if (lookahead == 'l') ADVANCE(35); if (('0' <= lookahead && lookahead <= '9') || ('A' <= lookahead && lookahead <= 'Z') || lookahead == '_' || - ('a' <= lookahead && lookahead <= 'z')) ADVANCE(17); + ('a' <= lookahead && lookahead <= 'z')) ADVANCE(21); END_STATE(); case 14: ACCEPT_TOKEN(sym_identifier); - if (lookahead == 'o') ADVANCE(11); + if (lookahead == 'l') ADVANCE(13); if (('0' <= lookahead && lookahead <= '9') || ('A' <= lookahead && lookahead <= 'Z') || lookahead == '_' || - ('a' <= lookahead && lookahead <= 'z')) ADVANCE(17); + ('a' <= lookahead && lookahead <= 'z')) ADVANCE(21); END_STATE(); case 15: ACCEPT_TOKEN(sym_identifier); - if (lookahead == 'r') ADVANCE(7); + if (lookahead == 'm') ADVANCE(37); if (('0' <= lookahead && lookahead <= '9') || ('A' <= lookahead && lookahead <= 'Z') || lookahead == '_' || - ('a' <= lookahead && lookahead <= 'z')) ADVANCE(17); + ('a' <= lookahead && lookahead <= 'z')) ADVANCE(21); END_STATE(); case 16: ACCEPT_TOKEN(sym_identifier); - if (lookahead == 'x') ADVANCE(8); + if (lookahead == 'n') ADVANCE(31); if (('0' <= lookahead && lookahead <= '9') || ('A' <= lookahead && lookahead <= 'Z') || lookahead == '_' || - ('a' <= lookahead && lookahead <= 'z')) ADVANCE(17); + ('a' <= lookahead && lookahead <= 'z')) ADVANCE(21); END_STATE(); case 17: + ACCEPT_TOKEN(sym_identifier); + if (lookahead == 'o') ADVANCE(19); + if (lookahead == 'u') ADVANCE(16); + if (('0' <= lookahead && lookahead <= '9') || + ('A' <= lookahead && lookahead <= 'Z') || + lookahead == '_' || + ('a' <= lookahead && lookahead <= 'z')) ADVANCE(21); + END_STATE(); + case 18: + ACCEPT_TOKEN(sym_identifier); + if (lookahead == 'o') ADVANCE(15); + if (('0' <= lookahead && lookahead <= '9') || + ('A' <= lookahead && lookahead <= 'Z') || + lookahead == '_' || + ('a' <= lookahead && lookahead <= 'z')) ADVANCE(21); + END_STATE(); + case 19: + ACCEPT_TOKEN(sym_identifier); + if (lookahead == 'r') ADVANCE(11); + if (('0' <= lookahead && lookahead <= '9') || + ('A' <= lookahead && lookahead <= 'Z') || + lookahead == '_' || + ('a' <= lookahead && lookahead <= 'z')) ADVANCE(21); + END_STATE(); + case 20: + ACCEPT_TOKEN(sym_identifier); + if (lookahead == 'x') ADVANCE(12); + if (('0' <= lookahead && lookahead <= '9') || + ('A' <= lookahead && lookahead <= 'Z') || + lookahead == '_' || + ('a' <= lookahead && lookahead <= 'z')) ADVANCE(21); + END_STATE(); + case 21: ACCEPT_TOKEN(sym_identifier); if (('0' <= lookahead && lookahead <= '9') || ('A' <= lookahead && lookahead <= 'Z') || lookahead == '_' || - ('a' <= lookahead && lookahead <= 'z')) ADVANCE(17); - END_STATE(); - case 18: - ACCEPT_TOKEN(sym_comment); - if (lookahead != 0 && - lookahead != '\n') ADVANCE(18); - END_STATE(); - case 19: - ACCEPT_TOKEN(anon_sym_LPAREN); - END_STATE(); - case 20: - ACCEPT_TOKEN(anon_sym_COLON); - if (lookahead == '=') ADVANCE(35); - END_STATE(); - case 21: - ACCEPT_TOKEN(anon_sym_RPAREN); + ('a' <= lookahead && lookahead <= 'z')) ADVANCE(21); END_STATE(); case 22: - ACCEPT_TOKEN(sym_star); + ACCEPT_TOKEN(sym_comment); + if (lookahead != 0 && + lookahead != '\n') ADVANCE(22); END_STATE(); case 23: - ACCEPT_TOKEN(anon_sym_u25a1); + ACCEPT_TOKEN(sym_block_comment); + if (lookahead == '*') ADVANCE(7); + if (lookahead == '[') ADVANCE(8); + if (lookahead != 0 && + lookahead != ']') ADVANCE(3); END_STATE(); case 24: - ACCEPT_TOKEN(anon_sym_LBRACK_RBRACK); + ACCEPT_TOKEN(anon_sym_LPAREN); END_STATE(); case 25: - ACCEPT_TOKEN(anon_sym_u03bb); + ACCEPT_TOKEN(anon_sym_COLON); + if (lookahead == '=') ADVANCE(40); END_STATE(); case 26: + ACCEPT_TOKEN(anon_sym_RPAREN); + END_STATE(); + case 27: + ACCEPT_TOKEN(sym_star); + END_STATE(); + case 28: + ACCEPT_TOKEN(anon_sym_u25a1); + END_STATE(); + case 29: + ACCEPT_TOKEN(anon_sym_LBRACK_RBRACK); + END_STATE(); + case 30: + ACCEPT_TOKEN(anon_sym_u03bb); + END_STATE(); + case 31: ACCEPT_TOKEN(anon_sym_fun); if (('0' <= lookahead && lookahead <= '9') || ('A' <= lookahead && lookahead <= 'Z') || lookahead == '_' || - ('a' <= lookahead && lookahead <= 'z')) ADVANCE(17); + ('a' <= lookahead && lookahead <= 'z')) ADVANCE(21); END_STATE(); - case 27: + case 32: ACCEPT_TOKEN(anon_sym_EQ_GT); END_STATE(); - case 28: + case 33: ACCEPT_TOKEN(anon_sym_u21d2); END_STATE(); - case 29: + case 34: ACCEPT_TOKEN(anon_sym_u220f); END_STATE(); - case 30: + case 35: ACCEPT_TOKEN(anon_sym_forall); if (('0' <= lookahead && lookahead <= '9') || ('A' <= lookahead && lookahead <= 'Z') || lookahead == '_' || - ('a' <= lookahead && lookahead <= 'z')) ADVANCE(17); + ('a' <= lookahead && lookahead <= 'z')) ADVANCE(21); END_STATE(); - case 31: + case 36: ACCEPT_TOKEN(anon_sym_COMMA); END_STATE(); - case 32: + case 37: ACCEPT_TOKEN(sym_axiom); if (('0' <= lookahead && lookahead <= '9') || ('A' <= lookahead && lookahead <= 'Z') || lookahead == '_' || - ('a' <= lookahead && lookahead <= 'z')) ADVANCE(17); + ('a' <= lookahead && lookahead <= 'z')) ADVANCE(21); END_STATE(); - case 33: + case 38: ACCEPT_TOKEN(anon_sym_DASH_GT); END_STATE(); - case 34: + case 39: ACCEPT_TOKEN(anon_sym_u2192); END_STATE(); - case 35: + case 40: ACCEPT_TOKEN(anon_sym_COLON_EQ); END_STATE(); - case 36: + case 41: ACCEPT_TOKEN(anon_sym_SEMI); END_STATE(); default: @@ -621,7 +655,7 @@ static bool ts_lex(TSLexer *lexer, TSStateId state) { static const TSLexMode ts_lex_modes[STATE_COUNT] = { [0] = {.lex_state = 0}, - [1] = {.lex_state = 5}, + [1] = {.lex_state = 9}, [2] = {.lex_state = 0}, [3] = {.lex_state = 0}, [4] = {.lex_state = 0}, @@ -632,11 +666,11 @@ static const TSLexMode ts_lex_modes[STATE_COUNT] = { [9] = {.lex_state = 1}, [10] = {.lex_state = 1}, [11] = {.lex_state = 1}, - [12] = {.lex_state = 5}, - [13] = {.lex_state = 5}, - [14] = {.lex_state = 5}, - [15] = {.lex_state = 5}, - [16] = {.lex_state = 5}, + [12] = {.lex_state = 9}, + [13] = {.lex_state = 9}, + [14] = {.lex_state = 9}, + [15] = {.lex_state = 9}, + [16] = {.lex_state = 9}, [17] = {.lex_state = 0}, [18] = {.lex_state = 0}, [19] = {.lex_state = 0}, @@ -646,20 +680,20 @@ static const TSLexMode ts_lex_modes[STATE_COUNT] = { [23] = {.lex_state = 0}, [24] = {.lex_state = 0}, [25] = {.lex_state = 0}, - [26] = {.lex_state = 5}, + [26] = {.lex_state = 0}, [27] = {.lex_state = 0}, [28] = {.lex_state = 0}, [29] = {.lex_state = 0}, - [30] = {.lex_state = 5}, - [31] = {.lex_state = 0}, - [32] = {.lex_state = 5}, - [33] = {.lex_state = 5}, - [34] = {.lex_state = 5}, - [35] = {.lex_state = 5}, + [30] = {.lex_state = 9}, + [31] = {.lex_state = 9}, + [32] = {.lex_state = 9}, + [33] = {.lex_state = 9}, + [34] = {.lex_state = 9}, + [35] = {.lex_state = 0}, [36] = {.lex_state = 0}, - [37] = {.lex_state = 5}, - [38] = {.lex_state = 0}, - [39] = {.lex_state = 5}, + [37] = {.lex_state = 9}, + [38] = {.lex_state = 9}, + [39] = {.lex_state = 9}, [40] = {.lex_state = 0}, [41] = {.lex_state = 0}, [42] = {.lex_state = 0}, @@ -676,7 +710,8 @@ static const uint16_t ts_parse_table[LARGE_STATE_COUNT][SYMBOL_COUNT] = { [0] = { [ts_builtin_sym_end] = ACTIONS(1), [sym_identifier] = ACTIONS(1), - [sym_comment] = ACTIONS(1), + [sym_comment] = ACTIONS(3), + [sym_block_comment] = ACTIONS(3), [anon_sym_LPAREN] = ACTIONS(1), [anon_sym_COLON] = ACTIONS(1), [anon_sym_RPAREN] = ACTIONS(1), @@ -698,11 +733,12 @@ static const uint16_t ts_parse_table[LARGE_STATE_COUNT][SYMBOL_COUNT] = { }, [1] = { [sym_program] = STATE(42), - [sym_definition] = STATE(30), - [aux_sym_program_repeat1] = STATE(30), - [ts_builtin_sym_end] = ACTIONS(3), - [sym_identifier] = ACTIONS(5), - [sym_comment] = ACTIONS(7), + [sym_definition] = STATE(31), + [aux_sym_program_repeat1] = STATE(31), + [ts_builtin_sym_end] = ACTIONS(5), + [sym_identifier] = ACTIONS(7), + [sym_comment] = ACTIONS(3), + [sym_block_comment] = ACTIONS(3), }, [2] = { [sym_square] = STATE(15), @@ -715,6 +751,8 @@ static const uint16_t ts_parse_table[LARGE_STATE_COUNT][SYMBOL_COUNT] = { [sym_expr] = STATE(44), [aux_sym_app_repeat1] = STATE(12), [sym_identifier] = ACTIONS(9), + [sym_comment] = ACTIONS(3), + [sym_block_comment] = ACTIONS(3), [anon_sym_LPAREN] = ACTIONS(11), [sym_star] = ACTIONS(13), [anon_sym_u25a1] = ACTIONS(15), @@ -736,6 +774,8 @@ static const uint16_t ts_parse_table[LARGE_STATE_COUNT][SYMBOL_COUNT] = { [sym_expr] = STATE(40), [aux_sym_app_repeat1] = STATE(12), [sym_identifier] = ACTIONS(9), + [sym_comment] = ACTIONS(3), + [sym_block_comment] = ACTIONS(3), [anon_sym_LPAREN] = ACTIONS(11), [sym_star] = ACTIONS(13), [anon_sym_u25a1] = ACTIONS(15), @@ -757,6 +797,8 @@ static const uint16_t ts_parse_table[LARGE_STATE_COUNT][SYMBOL_COUNT] = { [sym_expr] = STATE(45), [aux_sym_app_repeat1] = STATE(12), [sym_identifier] = ACTIONS(9), + [sym_comment] = ACTIONS(3), + [sym_block_comment] = ACTIONS(3), [anon_sym_LPAREN] = ACTIONS(11), [sym_star] = ACTIONS(13), [anon_sym_u25a1] = ACTIONS(15), @@ -767,245 +809,171 @@ static const uint16_t ts_parse_table[LARGE_STATE_COUNT][SYMBOL_COUNT] = { [anon_sym_forall] = ACTIONS(23), [sym_axiom] = ACTIONS(29), }, + [5] = { + [sym_square] = STATE(15), + [sym_labs] = STATE(23), + [sym_pabs] = STATE(23), + [sym_term] = STATE(12), + [sym_app] = STATE(23), + [sym_arrow] = STATE(24), + [sym_app_term] = STATE(22), + [sym_expr] = STATE(43), + [aux_sym_app_repeat1] = STATE(12), + [sym_identifier] = ACTIONS(9), + [sym_comment] = ACTIONS(3), + [sym_block_comment] = ACTIONS(3), + [anon_sym_LPAREN] = ACTIONS(11), + [sym_star] = ACTIONS(13), + [anon_sym_u25a1] = ACTIONS(15), + [anon_sym_LBRACK_RBRACK] = ACTIONS(15), + [anon_sym_u03bb] = ACTIONS(17), + [anon_sym_fun] = ACTIONS(19), + [anon_sym_u220f] = ACTIONS(21), + [anon_sym_forall] = ACTIONS(23), + }, + [6] = { + [sym_square] = STATE(15), + [sym_labs] = STATE(23), + [sym_pabs] = STATE(23), + [sym_term] = STATE(12), + [sym_app] = STATE(23), + [sym_arrow] = STATE(24), + [sym_app_term] = STATE(22), + [sym_expr] = STATE(26), + [aux_sym_app_repeat1] = STATE(12), + [sym_identifier] = ACTIONS(9), + [sym_comment] = ACTIONS(3), + [sym_block_comment] = ACTIONS(3), + [anon_sym_LPAREN] = ACTIONS(11), + [sym_star] = ACTIONS(13), + [anon_sym_u25a1] = ACTIONS(15), + [anon_sym_LBRACK_RBRACK] = ACTIONS(15), + [anon_sym_u03bb] = ACTIONS(17), + [anon_sym_fun] = ACTIONS(19), + [anon_sym_u220f] = ACTIONS(21), + [anon_sym_forall] = ACTIONS(23), + }, + [7] = { + [sym_square] = STATE(15), + [sym_labs] = STATE(23), + [sym_pabs] = STATE(23), + [sym_term] = STATE(12), + [sym_app] = STATE(23), + [sym_arrow] = STATE(24), + [sym_app_term] = STATE(22), + [sym_expr] = STATE(41), + [aux_sym_app_repeat1] = STATE(12), + [sym_identifier] = ACTIONS(9), + [sym_comment] = ACTIONS(3), + [sym_block_comment] = ACTIONS(3), + [anon_sym_LPAREN] = ACTIONS(11), + [sym_star] = ACTIONS(13), + [anon_sym_u25a1] = ACTIONS(15), + [anon_sym_LBRACK_RBRACK] = ACTIONS(15), + [anon_sym_u03bb] = ACTIONS(17), + [anon_sym_fun] = ACTIONS(19), + [anon_sym_u220f] = ACTIONS(21), + [anon_sym_forall] = ACTIONS(23), + }, + [8] = { + [sym_square] = STATE(15), + [sym_labs] = STATE(23), + [sym_pabs] = STATE(23), + [sym_term] = STATE(12), + [sym_app] = STATE(23), + [sym_arrow] = STATE(24), + [sym_app_term] = STATE(22), + [sym_expr] = STATE(46), + [aux_sym_app_repeat1] = STATE(12), + [sym_identifier] = ACTIONS(9), + [sym_comment] = ACTIONS(3), + [sym_block_comment] = ACTIONS(3), + [anon_sym_LPAREN] = ACTIONS(11), + [sym_star] = ACTIONS(13), + [anon_sym_u25a1] = ACTIONS(15), + [anon_sym_LBRACK_RBRACK] = ACTIONS(15), + [anon_sym_u03bb] = ACTIONS(17), + [anon_sym_fun] = ACTIONS(19), + [anon_sym_u220f] = ACTIONS(21), + [anon_sym_forall] = ACTIONS(23), + }, + [9] = { + [sym_square] = STATE(15), + [sym_labs] = STATE(23), + [sym_pabs] = STATE(23), + [sym_term] = STATE(12), + [sym_app] = STATE(23), + [sym_arrow] = STATE(24), + [sym_app_term] = STATE(22), + [sym_expr] = STATE(48), + [aux_sym_app_repeat1] = STATE(12), + [sym_identifier] = ACTIONS(9), + [sym_comment] = ACTIONS(3), + [sym_block_comment] = ACTIONS(3), + [anon_sym_LPAREN] = ACTIONS(11), + [sym_star] = ACTIONS(13), + [anon_sym_u25a1] = ACTIONS(15), + [anon_sym_LBRACK_RBRACK] = ACTIONS(15), + [anon_sym_u03bb] = ACTIONS(17), + [anon_sym_fun] = ACTIONS(19), + [anon_sym_u220f] = ACTIONS(21), + [anon_sym_forall] = ACTIONS(23), + }, + [10] = { + [sym_square] = STATE(15), + [sym_labs] = STATE(23), + [sym_pabs] = STATE(23), + [sym_term] = STATE(12), + [sym_app] = STATE(23), + [sym_arrow] = STATE(24), + [sym_app_term] = STATE(22), + [sym_expr] = STATE(28), + [aux_sym_app_repeat1] = STATE(12), + [sym_identifier] = ACTIONS(9), + [sym_comment] = ACTIONS(3), + [sym_block_comment] = ACTIONS(3), + [anon_sym_LPAREN] = ACTIONS(11), + [sym_star] = ACTIONS(13), + [anon_sym_u25a1] = ACTIONS(15), + [anon_sym_LBRACK_RBRACK] = ACTIONS(15), + [anon_sym_u03bb] = ACTIONS(17), + [anon_sym_fun] = ACTIONS(19), + [anon_sym_u220f] = ACTIONS(21), + [anon_sym_forall] = ACTIONS(23), + }, + [11] = { + [sym_square] = STATE(15), + [sym_labs] = STATE(23), + [sym_pabs] = STATE(23), + [sym_term] = STATE(12), + [sym_app] = STATE(23), + [sym_arrow] = STATE(24), + [sym_app_term] = STATE(22), + [sym_expr] = STATE(27), + [aux_sym_app_repeat1] = STATE(12), + [sym_identifier] = ACTIONS(9), + [sym_comment] = ACTIONS(3), + [sym_block_comment] = ACTIONS(3), + [anon_sym_LPAREN] = ACTIONS(11), + [sym_star] = ACTIONS(13), + [anon_sym_u25a1] = ACTIONS(15), + [anon_sym_LBRACK_RBRACK] = ACTIONS(15), + [anon_sym_u03bb] = ACTIONS(17), + [anon_sym_fun] = ACTIONS(19), + [anon_sym_u220f] = ACTIONS(21), + [anon_sym_forall] = ACTIONS(23), + }, }; static const uint16_t ts_small_parse_table[] = { - [0] = 14, - ACTIONS(9), 1, - sym_identifier, - ACTIONS(11), 1, - anon_sym_LPAREN, - ACTIONS(13), 1, - sym_star, - ACTIONS(17), 1, - anon_sym_u03bb, - ACTIONS(19), 1, - anon_sym_fun, - ACTIONS(21), 1, - anon_sym_u220f, - ACTIONS(23), 1, - anon_sym_forall, - STATE(15), 1, - sym_square, - STATE(22), 1, - sym_app_term, - STATE(24), 1, - sym_arrow, - STATE(43), 1, - sym_expr, - ACTIONS(15), 2, - anon_sym_u25a1, - anon_sym_LBRACK_RBRACK, - STATE(12), 2, - sym_term, - aux_sym_app_repeat1, - STATE(23), 3, - sym_labs, - sym_pabs, - sym_app, - [47] = 14, - ACTIONS(9), 1, - sym_identifier, - ACTIONS(11), 1, - anon_sym_LPAREN, - ACTIONS(13), 1, - sym_star, - ACTIONS(17), 1, - anon_sym_u03bb, - ACTIONS(19), 1, - anon_sym_fun, - ACTIONS(21), 1, - anon_sym_u220f, - ACTIONS(23), 1, - anon_sym_forall, - STATE(15), 1, - sym_square, - STATE(22), 1, - sym_app_term, - STATE(24), 1, - sym_arrow, - STATE(28), 1, - sym_expr, - ACTIONS(15), 2, - anon_sym_u25a1, - anon_sym_LBRACK_RBRACK, - STATE(12), 2, - sym_term, - aux_sym_app_repeat1, - STATE(23), 3, - sym_labs, - sym_pabs, - sym_app, - [94] = 14, - ACTIONS(9), 1, - sym_identifier, - ACTIONS(11), 1, - anon_sym_LPAREN, - ACTIONS(13), 1, - sym_star, - ACTIONS(17), 1, - anon_sym_u03bb, - ACTIONS(19), 1, - anon_sym_fun, - ACTIONS(21), 1, - anon_sym_u220f, - ACTIONS(23), 1, - anon_sym_forall, - STATE(15), 1, - sym_square, - STATE(22), 1, - sym_app_term, - STATE(24), 1, - sym_arrow, - STATE(41), 1, - sym_expr, - ACTIONS(15), 2, - anon_sym_u25a1, - anon_sym_LBRACK_RBRACK, - STATE(12), 2, - sym_term, - aux_sym_app_repeat1, - STATE(23), 3, - sym_labs, - sym_pabs, - sym_app, - [141] = 14, - ACTIONS(9), 1, - sym_identifier, - ACTIONS(11), 1, - anon_sym_LPAREN, - ACTIONS(13), 1, - sym_star, - ACTIONS(17), 1, - anon_sym_u03bb, - ACTIONS(19), 1, - anon_sym_fun, - ACTIONS(21), 1, - anon_sym_u220f, - ACTIONS(23), 1, - anon_sym_forall, - STATE(15), 1, - sym_square, - STATE(22), 1, - sym_app_term, - STATE(24), 1, - sym_arrow, - STATE(46), 1, - sym_expr, - ACTIONS(15), 2, - anon_sym_u25a1, - anon_sym_LBRACK_RBRACK, - STATE(12), 2, - sym_term, - aux_sym_app_repeat1, - STATE(23), 3, - sym_labs, - sym_pabs, - sym_app, - [188] = 14, - ACTIONS(9), 1, - sym_identifier, - ACTIONS(11), 1, - anon_sym_LPAREN, - ACTIONS(13), 1, - sym_star, - ACTIONS(17), 1, - anon_sym_u03bb, - ACTIONS(19), 1, - anon_sym_fun, - ACTIONS(21), 1, - anon_sym_u220f, - ACTIONS(23), 1, - anon_sym_forall, - STATE(15), 1, - sym_square, - STATE(22), 1, - sym_app_term, - STATE(24), 1, - sym_arrow, - STATE(48), 1, - sym_expr, - ACTIONS(15), 2, - anon_sym_u25a1, - anon_sym_LBRACK_RBRACK, - STATE(12), 2, - sym_term, - aux_sym_app_repeat1, - STATE(23), 3, - sym_labs, - sym_pabs, - sym_app, - [235] = 14, - ACTIONS(9), 1, - sym_identifier, - ACTIONS(11), 1, - anon_sym_LPAREN, - ACTIONS(13), 1, - sym_star, - ACTIONS(17), 1, - anon_sym_u03bb, - ACTIONS(19), 1, - anon_sym_fun, - ACTIONS(21), 1, - anon_sym_u220f, - ACTIONS(23), 1, - anon_sym_forall, - STATE(15), 1, - sym_square, - STATE(22), 1, - sym_app_term, - STATE(24), 1, - sym_arrow, - STATE(29), 1, - sym_expr, - ACTIONS(15), 2, - anon_sym_u25a1, - anon_sym_LBRACK_RBRACK, - STATE(12), 2, - sym_term, - aux_sym_app_repeat1, - STATE(23), 3, - sym_labs, - sym_pabs, - sym_app, - [282] = 14, - ACTIONS(9), 1, - sym_identifier, - ACTIONS(11), 1, - anon_sym_LPAREN, - ACTIONS(13), 1, - sym_star, - ACTIONS(17), 1, - anon_sym_u03bb, - ACTIONS(19), 1, - anon_sym_fun, - ACTIONS(21), 1, - anon_sym_u220f, - ACTIONS(23), 1, - anon_sym_forall, - STATE(15), 1, - sym_square, - STATE(22), 1, - sym_app_term, - STATE(24), 1, - sym_arrow, - STATE(27), 1, - sym_expr, - ACTIONS(15), 2, - anon_sym_u25a1, - anon_sym_LBRACK_RBRACK, - STATE(12), 2, - sym_term, - aux_sym_app_repeat1, - STATE(23), 3, - sym_labs, - sym_pabs, - sym_app, - [329] = 6, + [0] = 7, ACTIONS(11), 1, anon_sym_LPAREN, STATE(15), 1, sym_square, + ACTIONS(3), 2, + sym_comment, + sym_block_comment, ACTIONS(13), 2, sym_identifier, sym_star, @@ -1021,11 +989,14 @@ static const uint16_t ts_small_parse_table[] = { anon_sym_u2192, anon_sym_COLON_EQ, anon_sym_SEMI, - [355] = 6, + [30] = 7, ACTIONS(36), 1, anon_sym_LPAREN, STATE(15), 1, sym_square, + ACTIONS(3), 2, + sym_comment, + sym_block_comment, ACTIONS(33), 2, sym_identifier, sym_star, @@ -1041,7 +1012,10 @@ static const uint16_t ts_small_parse_table[] = { anon_sym_u2192, anon_sym_COLON_EQ, anon_sym_SEMI, - [381] = 1, + [60] = 2, + ACTIONS(3), 2, + sym_comment, + sym_block_comment, ACTIONS(44), 10, sym_identifier, anon_sym_LPAREN, @@ -1053,7 +1027,10 @@ static const uint16_t ts_small_parse_table[] = { anon_sym_u2192, anon_sym_COLON_EQ, anon_sym_SEMI, - [394] = 1, + [77] = 2, + ACTIONS(3), 2, + sym_comment, + sym_block_comment, ACTIONS(46), 10, sym_identifier, anon_sym_LPAREN, @@ -1065,7 +1042,10 @@ static const uint16_t ts_small_parse_table[] = { anon_sym_u2192, anon_sym_COLON_EQ, anon_sym_SEMI, - [407] = 1, + [94] = 2, + ACTIONS(3), 2, + sym_comment, + sym_block_comment, ACTIONS(48), 10, sym_identifier, anon_sym_LPAREN, @@ -1077,11 +1057,14 @@ static const uint16_t ts_small_parse_table[] = { anon_sym_u2192, anon_sym_COLON_EQ, anon_sym_SEMI, - [420] = 4, + [111] = 5, ACTIONS(50), 1, anon_sym_LPAREN, ACTIONS(53), 1, anon_sym_COLON, + ACTIONS(3), 2, + sym_comment, + sym_block_comment, STATE(17), 2, sym_param_block, aux_sym_labs_repeat1, @@ -1090,7 +1073,7 @@ static const uint16_t ts_small_parse_table[] = { anon_sym_u21d2, anon_sym_COMMA, anon_sym_COLON_EQ, - [437] = 5, + [132] = 6, ACTIONS(57), 1, anon_sym_LPAREN, ACTIONS(59), 1, @@ -1099,10 +1082,13 @@ static const uint16_t ts_small_parse_table[] = { anon_sym_COLON_EQ, STATE(49), 1, sym_ascription, + ACTIONS(3), 2, + sym_comment, + sym_block_comment, STATE(19), 2, sym_param_block, aux_sym_labs_repeat1, - [454] = 5, + [153] = 6, ACTIONS(57), 1, anon_sym_LPAREN, ACTIONS(59), 1, @@ -1111,28 +1097,40 @@ static const uint16_t ts_small_parse_table[] = { anon_sym_COLON_EQ, STATE(47), 1, sym_ascription, + ACTIONS(3), 2, + sym_comment, + sym_block_comment, STATE(17), 2, sym_param_block, aux_sym_labs_repeat1, - [471] = 2, + [174] = 3, ACTIONS(67), 1, anon_sym_COLON, + ACTIONS(3), 2, + sym_comment, + sym_block_comment, ACTIONS(65), 5, anon_sym_LPAREN, anon_sym_EQ_GT, anon_sym_u21d2, anon_sym_COMMA, anon_sym_COLON_EQ, - [482] = 2, + [189] = 3, ACTIONS(71), 1, anon_sym_COLON, + ACTIONS(3), 2, + sym_comment, + sym_block_comment, ACTIONS(69), 5, anon_sym_LPAREN, anon_sym_EQ_GT, anon_sym_u21d2, anon_sym_COMMA, anon_sym_COLON_EQ, - [493] = 2, + [204] = 3, + ACTIONS(3), 2, + sym_comment, + sym_block_comment, ACTIONS(75), 2, anon_sym_DASH_GT, anon_sym_u2192, @@ -1140,218 +1138,285 @@ static const uint16_t ts_small_parse_table[] = { anon_sym_RPAREN, anon_sym_COLON_EQ, anon_sym_SEMI, - [503] = 1, + [218] = 2, + ACTIONS(3), 2, + sym_comment, + sym_block_comment, ACTIONS(77), 5, anon_sym_RPAREN, anon_sym_DASH_GT, anon_sym_u2192, anon_sym_COLON_EQ, anon_sym_SEMI, - [511] = 1, + [230] = 2, + ACTIONS(3), 2, + sym_comment, + sym_block_comment, ACTIONS(73), 5, anon_sym_RPAREN, anon_sym_DASH_GT, anon_sym_u2192, anon_sym_COLON_EQ, anon_sym_SEMI, - [519] = 3, + [242] = 4, ACTIONS(57), 1, anon_sym_LPAREN, + ACTIONS(3), 2, + sym_comment, + sym_block_comment, ACTIONS(79), 2, anon_sym_EQ_GT, anon_sym_u21d2, STATE(17), 2, sym_param_block, aux_sym_labs_repeat1, - [531] = 4, - ACTIONS(81), 1, - ts_builtin_sym_end, - ACTIONS(83), 1, - sym_identifier, - ACTIONS(86), 1, + [258] = 2, + ACTIONS(3), 2, sym_comment, - STATE(26), 2, - sym_definition, - aux_sym_program_repeat1, - [545] = 1, - ACTIONS(89), 5, + sym_block_comment, + ACTIONS(81), 5, anon_sym_RPAREN, anon_sym_DASH_GT, anon_sym_u2192, anon_sym_COLON_EQ, anon_sym_SEMI, - [553] = 1, - ACTIONS(91), 5, - anon_sym_RPAREN, - anon_sym_DASH_GT, - anon_sym_u2192, - anon_sym_COLON_EQ, - anon_sym_SEMI, - [561] = 1, - ACTIONS(93), 5, - anon_sym_RPAREN, - anon_sym_DASH_GT, - anon_sym_u2192, - anon_sym_COLON_EQ, - anon_sym_SEMI, - [569] = 4, - ACTIONS(5), 1, - sym_identifier, - ACTIONS(95), 1, - ts_builtin_sym_end, - ACTIONS(97), 1, + [270] = 2, + ACTIONS(3), 2, sym_comment, - STATE(26), 2, - sym_definition, - aux_sym_program_repeat1, - [583] = 3, + sym_block_comment, + ACTIONS(83), 5, + anon_sym_RPAREN, + anon_sym_DASH_GT, + anon_sym_u2192, + anon_sym_COLON_EQ, + anon_sym_SEMI, + [282] = 2, + ACTIONS(3), 2, + sym_comment, + sym_block_comment, + ACTIONS(85), 5, + anon_sym_RPAREN, + anon_sym_DASH_GT, + anon_sym_u2192, + anon_sym_COLON_EQ, + anon_sym_SEMI, + [294] = 4, ACTIONS(57), 1, anon_sym_LPAREN, - ACTIONS(99), 1, + ACTIONS(87), 1, anon_sym_COMMA, + ACTIONS(3), 2, + sym_comment, + sym_block_comment, STATE(17), 2, sym_param_block, aux_sym_labs_repeat1, - [594] = 3, - ACTIONS(101), 1, + [309] = 4, + ACTIONS(89), 1, + ts_builtin_sym_end, + ACTIONS(91), 1, sym_identifier, - ACTIONS(103), 1, + ACTIONS(3), 2, + sym_comment, + sym_block_comment, + STATE(30), 2, + sym_definition, + aux_sym_program_repeat1, + [324] = 4, + ACTIONS(7), 1, + sym_identifier, + ACTIONS(94), 1, + ts_builtin_sym_end, + ACTIONS(3), 2, + sym_comment, + sym_block_comment, + STATE(30), 2, + sym_definition, + aux_sym_program_repeat1, + [339] = 4, + ACTIONS(96), 1, + sym_identifier, + ACTIONS(98), 1, anon_sym_COLON, STATE(33), 1, aux_sym_param_block_repeat1, - [604] = 3, - ACTIONS(105), 1, + ACTIONS(3), 2, + sym_comment, + sym_block_comment, + [353] = 4, + ACTIONS(100), 1, + sym_identifier, + ACTIONS(102), 1, + anon_sym_COLON, + STATE(34), 1, + aux_sym_param_block_repeat1, + ACTIONS(3), 2, + sym_comment, + sym_block_comment, + [367] = 4, + ACTIONS(104), 1, sym_identifier, ACTIONS(107), 1, anon_sym_COLON, STATE(34), 1, aux_sym_param_block_repeat1, - [614] = 3, - ACTIONS(109), 1, - sym_identifier, - ACTIONS(112), 1, - anon_sym_COLON, - STATE(34), 1, - aux_sym_param_block_repeat1, - [624] = 1, - ACTIONS(114), 3, - ts_builtin_sym_end, - sym_identifier, + ACTIONS(3), 2, sym_comment, - [630] = 2, + sym_block_comment, + [381] = 3, ACTIONS(57), 1, anon_sym_LPAREN, - STATE(31), 2, - sym_param_block, - aux_sym_labs_repeat1, - [638] = 1, - ACTIONS(116), 3, - ts_builtin_sym_end, - sym_identifier, + ACTIONS(3), 2, sym_comment, - [644] = 2, - ACTIONS(57), 1, - anon_sym_LPAREN, + sym_block_comment, STATE(25), 2, sym_param_block, aux_sym_labs_repeat1, - [652] = 1, - ACTIONS(118), 3, + [393] = 3, + ACTIONS(57), 1, + anon_sym_LPAREN, + ACTIONS(3), 2, + sym_comment, + sym_block_comment, + STATE(29), 2, + sym_param_block, + aux_sym_labs_repeat1, + [405] = 2, + ACTIONS(3), 2, + sym_comment, + sym_block_comment, + ACTIONS(109), 2, ts_builtin_sym_end, sym_identifier, + [414] = 2, + ACTIONS(3), 2, sym_comment, - [658] = 1, - ACTIONS(120), 1, - anon_sym_SEMI, - [662] = 1, - ACTIONS(122), 1, - anon_sym_RPAREN, - [666] = 1, - ACTIONS(124), 1, + sym_block_comment, + ACTIONS(111), 2, ts_builtin_sym_end, - [670] = 1, - ACTIONS(126), 1, - anon_sym_COLON_EQ, - [674] = 1, - ACTIONS(128), 1, + sym_identifier, + [423] = 2, + ACTIONS(3), 2, + sym_comment, + sym_block_comment, + ACTIONS(113), 2, + ts_builtin_sym_end, + sym_identifier, + [432] = 2, + ACTIONS(115), 1, anon_sym_SEMI, - [678] = 1, - ACTIONS(130), 1, - anon_sym_SEMI, - [682] = 1, - ACTIONS(132), 1, + ACTIONS(3), 2, + sym_comment, + sym_block_comment, + [440] = 2, + ACTIONS(117), 1, anon_sym_RPAREN, - [686] = 1, - ACTIONS(134), 1, + ACTIONS(3), 2, + sym_comment, + sym_block_comment, + [448] = 2, + ACTIONS(119), 1, + ts_builtin_sym_end, + ACTIONS(3), 2, + sym_comment, + sym_block_comment, + [456] = 2, + ACTIONS(121), 1, anon_sym_COLON_EQ, - [690] = 1, - ACTIONS(136), 1, + ACTIONS(3), 2, + sym_comment, + sym_block_comment, + [464] = 2, + ACTIONS(123), 1, + anon_sym_SEMI, + ACTIONS(3), 2, + sym_comment, + sym_block_comment, + [472] = 2, + ACTIONS(125), 1, + anon_sym_SEMI, + ACTIONS(3), 2, + sym_comment, + sym_block_comment, + [480] = 2, + ACTIONS(127), 1, anon_sym_RPAREN, - [694] = 1, + ACTIONS(3), 2, + sym_comment, + sym_block_comment, + [488] = 2, + ACTIONS(129), 1, + anon_sym_COLON_EQ, + ACTIONS(3), 2, + sym_comment, + sym_block_comment, + [496] = 2, + ACTIONS(131), 1, + anon_sym_RPAREN, + ACTIONS(3), 2, + sym_comment, + sym_block_comment, + [504] = 2, ACTIONS(63), 1, anon_sym_COLON_EQ, + ACTIONS(3), 2, + sym_comment, + sym_block_comment, }; static const uint32_t ts_small_parse_table_map[] = { - [SMALL_STATE(5)] = 0, - [SMALL_STATE(6)] = 47, - [SMALL_STATE(7)] = 94, - [SMALL_STATE(8)] = 141, - [SMALL_STATE(9)] = 188, - [SMALL_STATE(10)] = 235, - [SMALL_STATE(11)] = 282, - [SMALL_STATE(12)] = 329, - [SMALL_STATE(13)] = 355, - [SMALL_STATE(14)] = 381, - [SMALL_STATE(15)] = 394, - [SMALL_STATE(16)] = 407, - [SMALL_STATE(17)] = 420, - [SMALL_STATE(18)] = 437, - [SMALL_STATE(19)] = 454, - [SMALL_STATE(20)] = 471, - [SMALL_STATE(21)] = 482, - [SMALL_STATE(22)] = 493, - [SMALL_STATE(23)] = 503, - [SMALL_STATE(24)] = 511, - [SMALL_STATE(25)] = 519, - [SMALL_STATE(26)] = 531, - [SMALL_STATE(27)] = 545, - [SMALL_STATE(28)] = 553, - [SMALL_STATE(29)] = 561, - [SMALL_STATE(30)] = 569, - [SMALL_STATE(31)] = 583, - [SMALL_STATE(32)] = 594, - [SMALL_STATE(33)] = 604, - [SMALL_STATE(34)] = 614, - [SMALL_STATE(35)] = 624, - [SMALL_STATE(36)] = 630, - [SMALL_STATE(37)] = 638, - [SMALL_STATE(38)] = 644, - [SMALL_STATE(39)] = 652, - [SMALL_STATE(40)] = 658, - [SMALL_STATE(41)] = 662, - [SMALL_STATE(42)] = 666, - [SMALL_STATE(43)] = 670, - [SMALL_STATE(44)] = 674, - [SMALL_STATE(45)] = 678, - [SMALL_STATE(46)] = 682, - [SMALL_STATE(47)] = 686, - [SMALL_STATE(48)] = 690, - [SMALL_STATE(49)] = 694, + [SMALL_STATE(12)] = 0, + [SMALL_STATE(13)] = 30, + [SMALL_STATE(14)] = 60, + [SMALL_STATE(15)] = 77, + [SMALL_STATE(16)] = 94, + [SMALL_STATE(17)] = 111, + [SMALL_STATE(18)] = 132, + [SMALL_STATE(19)] = 153, + [SMALL_STATE(20)] = 174, + [SMALL_STATE(21)] = 189, + [SMALL_STATE(22)] = 204, + [SMALL_STATE(23)] = 218, + [SMALL_STATE(24)] = 230, + [SMALL_STATE(25)] = 242, + [SMALL_STATE(26)] = 258, + [SMALL_STATE(27)] = 270, + [SMALL_STATE(28)] = 282, + [SMALL_STATE(29)] = 294, + [SMALL_STATE(30)] = 309, + [SMALL_STATE(31)] = 324, + [SMALL_STATE(32)] = 339, + [SMALL_STATE(33)] = 353, + [SMALL_STATE(34)] = 367, + [SMALL_STATE(35)] = 381, + [SMALL_STATE(36)] = 393, + [SMALL_STATE(37)] = 405, + [SMALL_STATE(38)] = 414, + [SMALL_STATE(39)] = 423, + [SMALL_STATE(40)] = 432, + [SMALL_STATE(41)] = 440, + [SMALL_STATE(42)] = 448, + [SMALL_STATE(43)] = 456, + [SMALL_STATE(44)] = 464, + [SMALL_STATE(45)] = 472, + [SMALL_STATE(46)] = 480, + [SMALL_STATE(47)] = 488, + [SMALL_STATE(48)] = 496, + [SMALL_STATE(49)] = 504, }; static const TSParseActionEntry ts_parse_actions[] = { [0] = {.entry = {.count = 0, .reusable = false}}, [1] = {.entry = {.count = 1, .reusable = false}}, RECOVER(), - [3] = {.entry = {.count = 1, .reusable = true}}, REDUCE(sym_program, 0, 0, 0), - [5] = {.entry = {.count = 1, .reusable = true}}, SHIFT(18), - [7] = {.entry = {.count = 1, .reusable = true}}, SHIFT(30), + [3] = {.entry = {.count = 1, .reusable = true}}, SHIFT_EXTRA(), + [5] = {.entry = {.count = 1, .reusable = true}}, REDUCE(sym_program, 0, 0, 0), + [7] = {.entry = {.count = 1, .reusable = true}}, SHIFT(18), [9] = {.entry = {.count = 1, .reusable = false}}, SHIFT(15), [11] = {.entry = {.count = 1, .reusable = true}}, SHIFT(8), [13] = {.entry = {.count = 1, .reusable = true}}, SHIFT(15), [15] = {.entry = {.count = 1, .reusable = true}}, SHIFT(16), - [17] = {.entry = {.count = 1, .reusable = true}}, SHIFT(38), - [19] = {.entry = {.count = 1, .reusable = false}}, SHIFT(38), + [17] = {.entry = {.count = 1, .reusable = true}}, SHIFT(35), + [19] = {.entry = {.count = 1, .reusable = false}}, SHIFT(35), [21] = {.entry = {.count = 1, .reusable = true}}, SHIFT(36), [23] = {.entry = {.count = 1, .reusable = false}}, SHIFT(36), [25] = {.entry = {.count = 1, .reusable = false}}, SHIFT(44), @@ -1380,33 +1445,31 @@ static const TSParseActionEntry ts_parse_actions[] = { [75] = {.entry = {.count = 1, .reusable = true}}, SHIFT(10), [77] = {.entry = {.count = 1, .reusable = true}}, REDUCE(sym_app_term, 1, 0, 0), [79] = {.entry = {.count = 1, .reusable = true}}, SHIFT(11), - [81] = {.entry = {.count = 1, .reusable = true}}, REDUCE(aux_sym_program_repeat1, 2, 0, 0), - [83] = {.entry = {.count = 2, .reusable = true}}, REDUCE(aux_sym_program_repeat1, 2, 0, 0), SHIFT_REPEAT(18), - [86] = {.entry = {.count = 2, .reusable = true}}, REDUCE(aux_sym_program_repeat1, 2, 0, 0), SHIFT_REPEAT(26), - [89] = {.entry = {.count = 1, .reusable = true}}, REDUCE(sym_labs, 4, 0, 0), - [91] = {.entry = {.count = 1, .reusable = true}}, REDUCE(sym_pabs, 4, 0, 0), - [93] = {.entry = {.count = 1, .reusable = true}}, REDUCE(sym_arrow, 3, 0, 0), - [95] = {.entry = {.count = 1, .reusable = true}}, REDUCE(sym_program, 1, 0, 0), - [97] = {.entry = {.count = 1, .reusable = true}}, SHIFT(26), - [99] = {.entry = {.count = 1, .reusable = true}}, SHIFT(6), - [101] = {.entry = {.count = 1, .reusable = true}}, SHIFT(33), - [103] = {.entry = {.count = 1, .reusable = true}}, SHIFT(7), - [105] = {.entry = {.count = 1, .reusable = true}}, SHIFT(34), - [107] = {.entry = {.count = 1, .reusable = true}}, SHIFT(9), - [109] = {.entry = {.count = 2, .reusable = true}}, REDUCE(aux_sym_param_block_repeat1, 2, 0, 0), SHIFT_REPEAT(34), - [112] = {.entry = {.count = 1, .reusable = true}}, REDUCE(aux_sym_param_block_repeat1, 2, 0, 0), - [114] = {.entry = {.count = 1, .reusable = true}}, REDUCE(sym_definition, 5, 0, 2), - [116] = {.entry = {.count = 1, .reusable = true}}, REDUCE(sym_definition, 4, 0, 2), - [118] = {.entry = {.count = 1, .reusable = true}}, REDUCE(sym_definition, 6, 0, 2), - [120] = {.entry = {.count = 1, .reusable = true}}, SHIFT(37), - [122] = {.entry = {.count = 1, .reusable = true}}, SHIFT(20), - [124] = {.entry = {.count = 1, .reusable = true}}, ACCEPT_INPUT(), - [126] = {.entry = {.count = 1, .reusable = true}}, REDUCE(sym_ascription, 2, 0, 1), - [128] = {.entry = {.count = 1, .reusable = true}}, SHIFT(35), - [130] = {.entry = {.count = 1, .reusable = true}}, SHIFT(39), - [132] = {.entry = {.count = 1, .reusable = true}}, SHIFT(14), - [134] = {.entry = {.count = 1, .reusable = true}}, SHIFT(4), - [136] = {.entry = {.count = 1, .reusable = true}}, SHIFT(21), + [81] = {.entry = {.count = 1, .reusable = true}}, REDUCE(sym_pabs, 4, 0, 0), + [83] = {.entry = {.count = 1, .reusable = true}}, REDUCE(sym_labs, 4, 0, 0), + [85] = {.entry = {.count = 1, .reusable = true}}, REDUCE(sym_arrow, 3, 0, 0), + [87] = {.entry = {.count = 1, .reusable = true}}, SHIFT(6), + [89] = {.entry = {.count = 1, .reusable = true}}, REDUCE(aux_sym_program_repeat1, 2, 0, 0), + [91] = {.entry = {.count = 2, .reusable = true}}, REDUCE(aux_sym_program_repeat1, 2, 0, 0), SHIFT_REPEAT(18), + [94] = {.entry = {.count = 1, .reusable = true}}, REDUCE(sym_program, 1, 0, 0), + [96] = {.entry = {.count = 1, .reusable = true}}, SHIFT(33), + [98] = {.entry = {.count = 1, .reusable = true}}, SHIFT(7), + [100] = {.entry = {.count = 1, .reusable = true}}, SHIFT(34), + [102] = {.entry = {.count = 1, .reusable = true}}, SHIFT(9), + [104] = {.entry = {.count = 2, .reusable = true}}, REDUCE(aux_sym_param_block_repeat1, 2, 0, 0), SHIFT_REPEAT(34), + [107] = {.entry = {.count = 1, .reusable = true}}, REDUCE(aux_sym_param_block_repeat1, 2, 0, 0), + [109] = {.entry = {.count = 1, .reusable = true}}, REDUCE(sym_definition, 4, 0, 2), + [111] = {.entry = {.count = 1, .reusable = true}}, REDUCE(sym_definition, 5, 0, 2), + [113] = {.entry = {.count = 1, .reusable = true}}, REDUCE(sym_definition, 6, 0, 2), + [115] = {.entry = {.count = 1, .reusable = true}}, SHIFT(37), + [117] = {.entry = {.count = 1, .reusable = true}}, SHIFT(20), + [119] = {.entry = {.count = 1, .reusable = true}}, ACCEPT_INPUT(), + [121] = {.entry = {.count = 1, .reusable = true}}, REDUCE(sym_ascription, 2, 0, 1), + [123] = {.entry = {.count = 1, .reusable = true}}, SHIFT(38), + [125] = {.entry = {.count = 1, .reusable = true}}, SHIFT(39), + [127] = {.entry = {.count = 1, .reusable = true}}, SHIFT(14), + [129] = {.entry = {.count = 1, .reusable = true}}, SHIFT(4), + [131] = {.entry = {.count = 1, .reusable = true}}, SHIFT(21), }; #ifdef __cplusplus diff --git a/test/corpus/application.txt b/test/corpus/application.txt new file mode 100644 index 0000000..5511fa6 --- /dev/null +++ b/test/corpus/application.txt @@ -0,0 +1,66 @@ +=========== +Application +=========== + +foo (A B : *) (f : A -> B) (x : A) := + (fun (x : B) => x) (f x); + +--- +(program + (definition + (identifier) + (param_block + (identifier) + (identifier) + (expr + (app_term + (app + (term + (star)))))) + (param_block + (identifier) + (expr + (arrow + (app_term + (app + (term + (identifier)))) + (expr + (app_term + (app + (term + (identifier)))))))) + (param_block + (identifier) + (expr + (app_term + (app + (term + (identifier)))))) + (expr + (app_term + (app + (term + (expr + (app_term + (labs + (param_block + (identifier) + (expr + (app_term + (app + (term + (identifier)))))) + (expr + (app_term + (app + (term + (identifier))))))))) + (term + (expr + (app_term + (app + (term + (identifier)) + (term + (identifier))))))))))) diff --git a/test/corpus/arrows.txt b/test/corpus/arrows.txt index a478818..23539fa 100644 --- a/test/corpus/arrows.txt +++ b/test/corpus/arrows.txt @@ -10,46 +10,39 @@ foo (A B : *) (f : A -> A -> B) (x : A) := f x x; (definition (identifier) (param_block - (param - (identifier)) - (param - (identifier)) - (type - (expr + (identifier) + (identifier) + (expr + (app_term + (app + (term + (star)))))) + (param_block + (identifier) + (expr + (arrow (app_term (app (term - (star))))))) - (param_block - (param - (identifier)) - (type - (expr - (arrow - (app_term - (app - (term - (identifier)))) - (expr - (arrow + (identifier)))) + (expr + (arrow + (app_term + (app + (term + (identifier)))) + (expr (app_term (app (term - (identifier)))) - (expr - (app_term - (app - (term - (identifier))))))))))) + (identifier)))))))))) (param_block - (param - (identifier)) - (type - (expr - (app_term - (app - (term - (identifier))))))) + (identifier) + (expr + (app_term + (app + (term + (identifier)))))) (expr (app_term (app diff --git a/test/corpus/axioms.txt b/test/corpus/axioms.txt index 5221067..1cdbf91 100644 --- a/test/corpus/axioms.txt +++ b/test/corpus/axioms.txt @@ -10,10 +10,9 @@ nat : * := axiom; (definition (identifier) (ascription - (type - (expr - (app_term - (app - (term - (star))))))) + (expr + (app_term + (app + (term + (star)))))) (axiom))) diff --git a/test/corpus/comments.txt b/test/corpus/comments.txt index 6079025..d8709fe 100644 --- a/test/corpus/comments.txt +++ b/test/corpus/comments.txt @@ -4,7 +4,10 @@ Comments -- here's a comment -foo := *; +foo := + -- and a comment in the middle + [* and a [* nested *] block comment *] + *; --- @@ -12,6 +15,8 @@ foo := *; (comment) (definition (identifier) + (comment) + (block_comment) (expr (app_term (app diff --git a/test/corpus/labs.txt b/test/corpus/labs.txt index edca5ff..65d23fc 100644 --- a/test/corpus/labs.txt +++ b/test/corpus/labs.txt @@ -12,25 +12,20 @@ foo := fun (A : *) (x : A) => x; (expr (app_term (labs - (lambda) (param_block - (param - (identifier)) - (type - (expr - (app_term - (app - (term - (star))))))) + (identifier) + (expr + (app_term + (app + (term + (star)))))) (param_block - (param - (identifier)) - (type - (expr - (app_term - (app - (term - (identifier))))))) + (identifier) + (expr + (app_term + (app + (term + (identifier)))))) (expr (app_term (app diff --git a/test/corpus/pabs.txt b/test/corpus/pabs.txt index b592538..7101edf 100644 --- a/test/corpus/pabs.txt +++ b/test/corpus/pabs.txt @@ -12,25 +12,20 @@ rel := forall (A : *) (x : A), *; (expr (app_term (pabs - (pi) (param_block - (param - (identifier)) - (type - (expr - (app_term - (app - (term - (star))))))) + (identifier) + (expr + (app_term + (app + (term + (star)))))) (param_block - (param - (identifier)) - (type - (expr - (app_term - (app - (term - (identifier))))))) + (identifier) + (expr + (app_term + (app + (term + (identifier)))))) (expr (app_term (app