diff --git a/grammar.js b/grammar.js index 00fc15d..0abba60 100644 --- a/grammar.js +++ b/grammar.js @@ -21,32 +21,26 @@ module.exports = grammar({ comment : $ => token(seq('--', /.*/)), - param : $ => $.identifier, - param_block : $ => seq( '(', - repeat($.param), + field('param', repeat($.identifier)), ':', - $.type, + field('type', $.expr), ')' ), - type : $ => $.expr, - star : $ => "*", square : $ => choice('□', '[]'), - lambda : $ => choice('λ', 'fun'), - pi : $ => choice('∏', 'forall'), labs : $ => seq( - $.lambda, + choice('λ', 'fun'), repeat1($.param_block), choice('=>', '⇒'), $.expr, ), pabs : $ => seq( - $.pi, + choice('∏', 'forall'), repeat1($.param_block), ',', $.expr, @@ -82,11 +76,11 @@ module.exports = grammar({ ascription : $ => seq( ':', - $.type, + field('type', $.expr), ), definition : $ => seq( - $.identifier, + field('name', $.identifier), repeat($.param_block), optional($.ascription), ':=', diff --git a/src/grammar.json b/src/grammar.json index 1eef610..4a66ad5 100644 --- a/src/grammar.json +++ b/src/grammar.json @@ -1,5 +1,4 @@ { - "$schema": "https://tree-sitter.github.io/tree-sitter/assets/schemas/grammar.schema.json", "name": "perga", "rules": { "program": { @@ -46,10 +45,14 @@ "value": "(" }, { - "type": "REPEAT", + "type": "FIELD", + "name": "param", "content": { - "type": "SYMBOL", - "name": "identifier" + "type": "REPEAT", + "content": { + "type": "SYMBOL", + "name": "identifier" + } } }, { @@ -57,8 +60,12 @@ "value": ":" }, { - "type": "SYMBOL", - "name": "expr" + "type": "FIELD", + "name": "type", + "content": { + "type": "SYMBOL", + "name": "expr" + } }, { "type": "STRING", @@ -83,38 +90,21 @@ } ] }, - "lambda": { - "type": "CHOICE", - "members": [ - { - "type": "STRING", - "value": "λ" - }, - { - "type": "STRING", - "value": "fun" - } - ] - }, - "pi": { - "type": "CHOICE", - "members": [ - { - "type": "STRING", - "value": "∏" - }, - { - "type": "STRING", - "value": "forall" - } - ] - }, "labs": { "type": "SEQ", "members": [ { - "type": "SYMBOL", - "name": "lambda" + "type": "CHOICE", + "members": [ + { + "type": "STRING", + "value": "λ" + }, + { + "type": "STRING", + "value": "fun" + } + ] }, { "type": "REPEAT1", @@ -146,8 +136,17 @@ "type": "SEQ", "members": [ { - "type": "SYMBOL", - "name": "pi" + "type": "CHOICE", + "members": [ + { + "type": "STRING", + "value": "∏" + }, + { + "type": "STRING", + "value": "forall" + } + ] }, { "type": "REPEAT1", @@ -279,8 +278,12 @@ "value": ":" }, { - "type": "SYMBOL", - "name": "expr" + "type": "FIELD", + "name": "type", + "content": { + "type": "SYMBOL", + "name": "expr" + } } ] }, @@ -288,8 +291,12 @@ "type": "SEQ", "members": [ { - "type": "SYMBOL", - "name": "identifier" + "type": "FIELD", + "name": "name", + "content": { + "type": "SYMBOL", + "name": "identifier" + } }, { "type": "REPEAT", diff --git a/src/node-types.json b/src/node-types.json index 2fd46e0..72a3bf1 100644 --- a/src/node-types.json +++ b/src/node-types.json @@ -59,22 +59,34 @@ { "type": "ascription", "named": true, - "fields": {}, - "children": { - "multiple": false, - "required": true, - "types": [ - { - "type": "expr", - "named": true - } - ] + "fields": { + "type": { + "multiple": false, + "required": true, + "types": [ + { + "type": "expr", + "named": true + } + ] + } } }, { "type": "definition", "named": true, - "fields": {}, + "fields": { + "name": { + "multiple": false, + "required": true, + "types": [ + { + "type": "identifier", + "named": true + } + ] + } + }, "children": { "multiple": true, "required": true, @@ -91,10 +103,6 @@ "type": "expr", "named": true }, - { - "type": "identifier", - "named": true - }, { "type": "param_block", "named": true @@ -133,10 +141,6 @@ "type": "expr", "named": true }, - { - "type": "lambda", - "named": true - }, { "type": "param_block", "named": true @@ -144,11 +148,6 @@ ] } }, - { - "type": "lambda", - "named": true, - "fields": {} - }, { "type": "pabs", "named": true, @@ -164,10 +163,6 @@ { "type": "param_block", "named": true - }, - { - "type": "pi", - "named": true } ] } @@ -175,31 +170,32 @@ { "type": "param_block", "named": true, - "fields": {}, - "children": { - "multiple": true, - "required": true, - "types": [ - { - "type": "expr", - "named": true - }, - { - "type": "identifier", - "named": true - } - ] + "fields": { + "param": { + "multiple": true, + "required": false, + "types": [ + { + "type": "identifier", + "named": true + } + ] + }, + "type": { + "multiple": false, + "required": true, + "types": [ + { + "type": "expr", + "named": true + } + ] + } } }, - { - "type": "pi", - "named": true, - "fields": {} - }, { "type": "program", "named": true, - "root": true, "fields": {}, "children": { "multiple": true, diff --git a/src/parser.c b/src/parser.c index 6cbff8a..aacf927 100644 --- a/src/parser.c +++ b/src/parser.c @@ -5,15 +5,15 @@ #endif #define LANGUAGE_VERSION 14 -#define STATE_COUNT 52 -#define LARGE_STATE_COUNT 12 -#define SYMBOL_COUNT 39 +#define STATE_COUNT 50 +#define LARGE_STATE_COUNT 5 +#define SYMBOL_COUNT 37 #define ALIAS_COUNT 0 #define TOKEN_COUNT 21 #define EXTERNAL_TOKEN_COUNT 0 -#define FIELD_COUNT 0 +#define FIELD_COUNT 3 #define MAX_ALIAS_SEQUENCE_LENGTH 6 -#define PRODUCTION_ID_COUNT 1 +#define PRODUCTION_ID_COUNT 5 enum ts_symbol_identifiers { sym_identifier = 1, @@ -26,10 +26,10 @@ enum ts_symbol_identifiers { anon_sym_LBRACK_RBRACK = 8, anon_sym_u03bb = 9, anon_sym_fun = 10, - anon_sym_u220f = 11, - anon_sym_forall = 12, - anon_sym_EQ_GT = 13, - anon_sym_u21d2 = 14, + 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, @@ -39,21 +39,19 @@ enum ts_symbol_identifiers { sym_program = 21, sym_param_block = 22, sym_square = 23, - sym_lambda = 24, - sym_pi = 25, - sym_labs = 26, - sym_pabs = 27, - sym_term = 28, - sym_app = 29, - sym_arrow = 30, - sym_app_term = 31, - sym_expr = 32, - sym_ascription = 33, - sym_definition = 34, - aux_sym_program_repeat1 = 35, - aux_sym_param_block_repeat1 = 36, - aux_sym_labs_repeat1 = 37, - aux_sym_app_repeat1 = 38, + 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, }; static const char * const ts_symbol_names[] = { @@ -68,10 +66,10 @@ static const char * const ts_symbol_names[] = { [anon_sym_LBRACK_RBRACK] = "[]", [anon_sym_u03bb] = "\u03bb", [anon_sym_fun] = "fun", - [anon_sym_u220f] = "\u220f", - [anon_sym_forall] = "forall", [anon_sym_EQ_GT] = "=>", [anon_sym_u21d2] = "\u21d2", + [anon_sym_u220f] = "\u220f", + [anon_sym_forall] = "forall", [anon_sym_COMMA] = ",", [sym_axiom] = "axiom", [anon_sym_DASH_GT] = "->", @@ -81,8 +79,6 @@ static const char * const ts_symbol_names[] = { [sym_program] = "program", [sym_param_block] = "param_block", [sym_square] = "square", - [sym_lambda] = "lambda", - [sym_pi] = "pi", [sym_labs] = "labs", [sym_pabs] = "pabs", [sym_term] = "term", @@ -110,10 +106,10 @@ static const TSSymbol ts_symbol_map[] = { [anon_sym_LBRACK_RBRACK] = anon_sym_LBRACK_RBRACK, [anon_sym_u03bb] = anon_sym_u03bb, [anon_sym_fun] = anon_sym_fun, - [anon_sym_u220f] = anon_sym_u220f, - [anon_sym_forall] = anon_sym_forall, [anon_sym_EQ_GT] = anon_sym_EQ_GT, [anon_sym_u21d2] = anon_sym_u21d2, + [anon_sym_u220f] = anon_sym_u220f, + [anon_sym_forall] = anon_sym_forall, [anon_sym_COMMA] = anon_sym_COMMA, [sym_axiom] = sym_axiom, [anon_sym_DASH_GT] = anon_sym_DASH_GT, @@ -123,8 +119,6 @@ static const TSSymbol ts_symbol_map[] = { [sym_program] = sym_program, [sym_param_block] = sym_param_block, [sym_square] = sym_square, - [sym_lambda] = sym_lambda, - [sym_pi] = sym_pi, [sym_labs] = sym_labs, [sym_pabs] = sym_pabs, [sym_term] = sym_term, @@ -185,14 +179,6 @@ static const TSSymbolMetadata ts_symbol_metadata[] = { .visible = true, .named = false, }, - [anon_sym_u220f] = { - .visible = true, - .named = false, - }, - [anon_sym_forall] = { - .visible = true, - .named = false, - }, [anon_sym_EQ_GT] = { .visible = true, .named = false, @@ -201,6 +187,14 @@ static const TSSymbolMetadata ts_symbol_metadata[] = { .visible = true, .named = false, }, + [anon_sym_u220f] = { + .visible = true, + .named = false, + }, + [anon_sym_forall] = { + .visible = true, + .named = false, + }, [anon_sym_COMMA] = { .visible = true, .named = false, @@ -237,14 +231,6 @@ static const TSSymbolMetadata ts_symbol_metadata[] = { .visible = true, .named = true, }, - [sym_lambda] = { - .visible = true, - .named = true, - }, - [sym_pi] = { - .visible = true, - .named = true, - }, [sym_labs] = { .visible = true, .named = true, @@ -299,6 +285,38 @@ static const TSSymbolMetadata ts_symbol_metadata[] = { }, }; +enum ts_field_identifiers { + field_name = 1, + field_param = 2, + field_type = 3, +}; + +static const char * const ts_field_names[] = { + [0] = NULL, + [field_name] = "name", + [field_param] = "param", + [field_type] = "type", +}; + +static const TSFieldMapSlice ts_field_map_slices[PRODUCTION_ID_COUNT] = { + [1] = {.index = 0, .length = 1}, + [2] = {.index = 1, .length = 1}, + [3] = {.index = 2, .length = 1}, + [4] = {.index = 3, .length = 2}, +}; + +static const TSFieldMapEntry ts_field_map_entries[] = { + [0] = + {field_type, 1}, + [1] = + {field_name, 0}, + [2] = + {field_type, 2}, + [3] = + {field_param, 1}, + {field_type, 3}, +}; + static const TSSymbol ts_alias_sequences[PRODUCTION_ID_COUNT][MAX_ALIAS_SEQUENCE_LENGTH] = { [0] = {0}, }; @@ -358,8 +376,6 @@ static const TSStateId ts_primary_state_ids[STATE_COUNT] = { [47] = 47, [48] = 48, [49] = 49, - [50] = 50, - [51] = 51, }; static bool ts_lex(TSLexer *lexer, TSStateId state) { @@ -382,8 +398,8 @@ static bool ts_lex(TSLexer *lexer, TSStateId state) { 'f', 13, 0x3bb, 25, 0x2192, 34, - 0x21d2, 30, - 0x220f, 27, + 0x21d2, 28, + 0x220f, 29, 0x25a1, 23, ); if (('\t' <= lookahead && lookahead <= '\r') || @@ -398,7 +414,7 @@ static bool ts_lex(TSLexer *lexer, TSStateId state) { if (lookahead == '[') ADVANCE(4); if (lookahead == 'f') ADVANCE(13); if (lookahead == 0x3bb) ADVANCE(25); - if (lookahead == 0x220f) ADVANCE(27); + if (lookahead == 0x220f) ADVANCE(29); if (lookahead == 0x25a1) ADVANCE(23); if (('\t' <= lookahead && lookahead <= '\r') || lookahead == ' ') SKIP(1); @@ -411,7 +427,7 @@ static bool ts_lex(TSLexer *lexer, TSStateId state) { if (lookahead == '>') ADVANCE(33); END_STATE(); case 3: - if (lookahead == '>') ADVANCE(29); + if (lookahead == '>') ADVANCE(27); END_STATE(); case 4: if (lookahead == ']') ADVANCE(24); @@ -456,7 +472,7 @@ static bool ts_lex(TSLexer *lexer, TSStateId state) { END_STATE(); case 9: ACCEPT_TOKEN(sym_identifier); - if (lookahead == 'l') ADVANCE(28); + if (lookahead == 'l') ADVANCE(30); if (('0' <= lookahead && lookahead <= '9') || ('A' <= lookahead && lookahead <= 'Z') || lookahead == '_' || @@ -561,21 +577,21 @@ static bool ts_lex(TSLexer *lexer, TSStateId state) { ('a' <= lookahead && lookahead <= 'z')) ADVANCE(17); END_STATE(); case 27: - ACCEPT_TOKEN(anon_sym_u220f); + ACCEPT_TOKEN(anon_sym_EQ_GT); END_STATE(); case 28: + ACCEPT_TOKEN(anon_sym_u21d2); + END_STATE(); + case 29: + ACCEPT_TOKEN(anon_sym_u220f); + END_STATE(); + case 30: ACCEPT_TOKEN(anon_sym_forall); if (('0' <= lookahead && lookahead <= '9') || ('A' <= lookahead && lookahead <= 'Z') || lookahead == '_' || ('a' <= lookahead && lookahead <= 'z')) ADVANCE(17); END_STATE(); - case 29: - ACCEPT_TOKEN(anon_sym_EQ_GT); - END_STATE(); - case 30: - ACCEPT_TOKEN(anon_sym_u21d2); - END_STATE(); case 31: ACCEPT_TOKEN(anon_sym_COMMA); END_STATE(); @@ -631,18 +647,18 @@ static const TSLexMode ts_lex_modes[STATE_COUNT] = { [24] = {.lex_state = 0}, [25] = {.lex_state = 0}, [26] = {.lex_state = 5}, - [27] = {.lex_state = 5}, + [27] = {.lex_state = 0}, [28] = {.lex_state = 0}, [29] = {.lex_state = 0}, - [30] = {.lex_state = 0}, + [30] = {.lex_state = 5}, [31] = {.lex_state = 0}, - [32] = {.lex_state = 0}, + [32] = {.lex_state = 5}, [33] = {.lex_state = 5}, - [34] = {.lex_state = 0}, + [34] = {.lex_state = 5}, [35] = {.lex_state = 5}, - [36] = {.lex_state = 5}, + [36] = {.lex_state = 0}, [37] = {.lex_state = 5}, - [38] = {.lex_state = 5}, + [38] = {.lex_state = 0}, [39] = {.lex_state = 5}, [40] = {.lex_state = 0}, [41] = {.lex_state = 0}, @@ -654,8 +670,6 @@ static const TSLexMode ts_lex_modes[STATE_COUNT] = { [47] = {.lex_state = 0}, [48] = {.lex_state = 0}, [49] = {.lex_state = 0}, - [50] = {.lex_state = 0}, - [51] = {.lex_state = 0}, }; static const uint16_t ts_parse_table[LARGE_STATE_COUNT][SYMBOL_COUNT] = { @@ -671,10 +685,10 @@ static const uint16_t ts_parse_table[LARGE_STATE_COUNT][SYMBOL_COUNT] = { [anon_sym_LBRACK_RBRACK] = ACTIONS(1), [anon_sym_u03bb] = ACTIONS(1), [anon_sym_fun] = ACTIONS(1), - [anon_sym_u220f] = ACTIONS(1), - [anon_sym_forall] = ACTIONS(1), [anon_sym_EQ_GT] = ACTIONS(1), [anon_sym_u21d2] = ACTIONS(1), + [anon_sym_u220f] = ACTIONS(1), + [anon_sym_forall] = ACTIONS(1), [anon_sym_COMMA] = ACTIONS(1), [sym_axiom] = ACTIONS(1), [anon_sym_DASH_GT] = ACTIONS(1), @@ -683,23 +697,21 @@ static const uint16_t ts_parse_table[LARGE_STATE_COUNT][SYMBOL_COUNT] = { [anon_sym_SEMI] = ACTIONS(1), }, [1] = { - [sym_program] = STATE(45), - [sym_definition] = STATE(27), - [aux_sym_program_repeat1] = STATE(27), + [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), }, [2] = { - [sym_square] = STATE(16), - [sym_lambda] = STATE(32), - [sym_pi] = STATE(34), - [sym_labs] = STATE(22), - [sym_pabs] = STATE(22), + [sym_square] = STATE(15), + [sym_labs] = STATE(23), + [sym_pabs] = STATE(23), [sym_term] = STATE(12), - [sym_app] = STATE(22), - [sym_arrow] = STATE(23), - [sym_app_term] = STATE(25), + [sym_app] = STATE(23), + [sym_arrow] = STATE(24), + [sym_app_term] = STATE(22), [sym_expr] = STATE(44), [aux_sym_app_repeat1] = STATE(12), [sym_identifier] = ACTIONS(9), @@ -714,16 +726,14 @@ static const uint16_t ts_parse_table[LARGE_STATE_COUNT][SYMBOL_COUNT] = { [sym_axiom] = ACTIONS(25), }, [3] = { - [sym_square] = STATE(16), - [sym_lambda] = STATE(32), - [sym_pi] = STATE(34), - [sym_labs] = STATE(22), - [sym_pabs] = STATE(22), + [sym_square] = STATE(15), + [sym_labs] = STATE(23), + [sym_pabs] = STATE(23), [sym_term] = STATE(12), - [sym_app] = STATE(22), - [sym_arrow] = STATE(23), - [sym_app_term] = STATE(25), - [sym_expr] = STATE(49), + [sym_app] = STATE(23), + [sym_arrow] = STATE(24), + [sym_app_term] = STATE(22), + [sym_expr] = STATE(40), [aux_sym_app_repeat1] = STATE(12), [sym_identifier] = ACTIONS(9), [anon_sym_LPAREN] = ACTIONS(11), @@ -737,16 +747,14 @@ static const uint16_t ts_parse_table[LARGE_STATE_COUNT][SYMBOL_COUNT] = { [sym_axiom] = ACTIONS(27), }, [4] = { - [sym_square] = STATE(16), - [sym_lambda] = STATE(32), - [sym_pi] = STATE(34), - [sym_labs] = STATE(22), - [sym_pabs] = STATE(22), + [sym_square] = STATE(15), + [sym_labs] = STATE(23), + [sym_pabs] = STATE(23), [sym_term] = STATE(12), - [sym_app] = STATE(22), - [sym_arrow] = STATE(23), - [sym_app_term] = STATE(25), - [sym_expr] = STATE(47), + [sym_app] = STATE(23), + [sym_arrow] = STATE(24), + [sym_app_term] = STATE(22), + [sym_expr] = STATE(45), [aux_sym_app_repeat1] = STATE(12), [sym_identifier] = ACTIONS(9), [anon_sym_LPAREN] = ACTIONS(11), @@ -759,167 +767,244 @@ 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(16), - [sym_lambda] = STATE(32), - [sym_pi] = STATE(34), - [sym_labs] = STATE(22), - [sym_pabs] = STATE(22), - [sym_term] = STATE(12), - [sym_app] = STATE(22), - [sym_arrow] = STATE(23), - [sym_app_term] = STATE(25), - [sym_expr] = STATE(41), - [aux_sym_app_repeat1] = STATE(12), - [sym_identifier] = ACTIONS(9), - [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(16), - [sym_lambda] = STATE(32), - [sym_pi] = STATE(34), - [sym_labs] = STATE(22), - [sym_pabs] = STATE(22), - [sym_term] = STATE(12), - [sym_app] = STATE(22), - [sym_arrow] = STATE(23), - [sym_app_term] = STATE(25), - [sym_expr] = STATE(42), - [aux_sym_app_repeat1] = STATE(12), - [sym_identifier] = ACTIONS(9), - [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(16), - [sym_lambda] = STATE(32), - [sym_pi] = STATE(34), - [sym_labs] = STATE(22), - [sym_pabs] = STATE(22), - [sym_term] = STATE(12), - [sym_app] = STATE(22), - [sym_arrow] = STATE(23), - [sym_app_term] = STATE(25), - [sym_expr] = STATE(50), - [aux_sym_app_repeat1] = STATE(12), - [sym_identifier] = ACTIONS(9), - [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(16), - [sym_lambda] = STATE(32), - [sym_pi] = STATE(34), - [sym_labs] = STATE(22), - [sym_pabs] = STATE(22), - [sym_term] = STATE(12), - [sym_app] = STATE(22), - [sym_arrow] = STATE(23), - [sym_app_term] = STATE(25), - [sym_expr] = STATE(40), - [aux_sym_app_repeat1] = STATE(12), - [sym_identifier] = ACTIONS(9), - [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(16), - [sym_lambda] = STATE(32), - [sym_pi] = STATE(34), - [sym_labs] = STATE(22), - [sym_pabs] = STATE(22), - [sym_term] = STATE(12), - [sym_app] = STATE(22), - [sym_arrow] = STATE(23), - [sym_app_term] = STATE(25), - [sym_expr] = STATE(28), - [aux_sym_app_repeat1] = STATE(12), - [sym_identifier] = ACTIONS(9), - [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(16), - [sym_lambda] = STATE(32), - [sym_pi] = STATE(34), - [sym_labs] = STATE(22), - [sym_pabs] = STATE(22), - [sym_term] = STATE(12), - [sym_app] = STATE(22), - [sym_arrow] = STATE(23), - [sym_app_term] = STATE(25), - [sym_expr] = STATE(29), - [aux_sym_app_repeat1] = STATE(12), - [sym_identifier] = ACTIONS(9), - [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(16), - [sym_lambda] = STATE(32), - [sym_pi] = STATE(34), - [sym_labs] = STATE(22), - [sym_pabs] = STATE(22), - [sym_term] = STATE(12), - [sym_app] = STATE(22), - [sym_arrow] = STATE(23), - [sym_app_term] = STATE(25), - [sym_expr] = STATE(30), - [aux_sym_app_repeat1] = STATE(12), - [sym_identifier] = ACTIONS(9), - [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] = 6, + [0] = 14, + ACTIONS(9), 1, + sym_identifier, ACTIONS(11), 1, anon_sym_LPAREN, - STATE(16), 1, + 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, + ACTIONS(11), 1, + anon_sym_LPAREN, + STATE(15), 1, sym_square, ACTIONS(13), 2, sym_identifier, @@ -936,10 +1021,10 @@ static const uint16_t ts_small_parse_table[] = { anon_sym_u2192, anon_sym_COLON_EQ, anon_sym_SEMI, - [26] = 6, + [355] = 6, ACTIONS(36), 1, anon_sym_LPAREN, - STATE(16), 1, + STATE(15), 1, sym_square, ACTIONS(33), 2, sym_identifier, @@ -956,7 +1041,7 @@ static const uint16_t ts_small_parse_table[] = { anon_sym_u2192, anon_sym_COLON_EQ, anon_sym_SEMI, - [52] = 1, + [381] = 1, ACTIONS(44), 10, sym_identifier, anon_sym_LPAREN, @@ -968,7 +1053,7 @@ static const uint16_t ts_small_parse_table[] = { anon_sym_u2192, anon_sym_COLON_EQ, anon_sym_SEMI, - [65] = 1, + [394] = 1, ACTIONS(46), 10, sym_identifier, anon_sym_LPAREN, @@ -980,7 +1065,7 @@ static const uint16_t ts_small_parse_table[] = { anon_sym_u2192, anon_sym_COLON_EQ, anon_sym_SEMI, - [78] = 1, + [407] = 1, ACTIONS(48), 10, sym_identifier, anon_sym_LPAREN, @@ -992,7 +1077,7 @@ static const uint16_t ts_small_parse_table[] = { anon_sym_u2192, anon_sym_COLON_EQ, anon_sym_SEMI, - [91] = 4, + [420] = 4, ACTIONS(50), 1, anon_sym_LPAREN, ACTIONS(53), 1, @@ -1005,31 +1090,31 @@ static const uint16_t ts_small_parse_table[] = { anon_sym_u21d2, anon_sym_COMMA, anon_sym_COLON_EQ, - [108] = 5, + [437] = 5, ACTIONS(57), 1, anon_sym_LPAREN, ACTIONS(59), 1, anon_sym_COLON, ACTIONS(61), 1, anon_sym_COLON_EQ, - STATE(51), 1, + STATE(49), 1, sym_ascription, STATE(19), 2, sym_param_block, aux_sym_labs_repeat1, - [125] = 5, + [454] = 5, ACTIONS(57), 1, anon_sym_LPAREN, ACTIONS(59), 1, anon_sym_COLON, ACTIONS(63), 1, anon_sym_COLON_EQ, - STATE(46), 1, + STATE(47), 1, sym_ascription, STATE(17), 2, sym_param_block, aux_sym_labs_repeat1, - [142] = 2, + [471] = 2, ACTIONS(67), 1, anon_sym_COLON, ACTIONS(65), 5, @@ -1038,7 +1123,7 @@ static const uint16_t ts_small_parse_table[] = { anon_sym_u21d2, anon_sym_COMMA, anon_sym_COLON_EQ, - [153] = 2, + [482] = 2, ACTIONS(71), 1, anon_sym_COLON, ACTIONS(69), 5, @@ -1047,38 +1132,38 @@ static const uint16_t ts_small_parse_table[] = { anon_sym_u21d2, anon_sym_COMMA, anon_sym_COLON_EQ, - [164] = 1, + [493] = 2, + ACTIONS(75), 2, + anon_sym_DASH_GT, + anon_sym_u2192, + ACTIONS(73), 3, + anon_sym_RPAREN, + anon_sym_COLON_EQ, + anon_sym_SEMI, + [503] = 1, + ACTIONS(77), 5, + anon_sym_RPAREN, + anon_sym_DASH_GT, + anon_sym_u2192, + anon_sym_COLON_EQ, + anon_sym_SEMI, + [511] = 1, ACTIONS(73), 5, anon_sym_RPAREN, anon_sym_DASH_GT, anon_sym_u2192, anon_sym_COLON_EQ, anon_sym_SEMI, - [172] = 1, - ACTIONS(75), 5, - anon_sym_RPAREN, - anon_sym_DASH_GT, - anon_sym_u2192, - anon_sym_COLON_EQ, - anon_sym_SEMI, - [180] = 3, + [519] = 3, ACTIONS(57), 1, anon_sym_LPAREN, - ACTIONS(77), 2, + ACTIONS(79), 2, anon_sym_EQ_GT, anon_sym_u21d2, STATE(17), 2, sym_param_block, aux_sym_labs_repeat1, - [192] = 2, - ACTIONS(79), 2, - anon_sym_DASH_GT, - anon_sym_u2192, - ACTIONS(75), 3, - anon_sym_RPAREN, - anon_sym_COLON_EQ, - anon_sym_SEMI, - [202] = 4, + [531] = 4, ACTIONS(81), 1, ts_builtin_sym_end, ACTIONS(83), 1, @@ -1088,38 +1173,38 @@ static const uint16_t ts_small_parse_table[] = { STATE(26), 2, sym_definition, aux_sym_program_repeat1, - [216] = 4, - ACTIONS(5), 1, - sym_identifier, - ACTIONS(89), 1, - ts_builtin_sym_end, - ACTIONS(91), 1, - sym_comment, - STATE(26), 2, - sym_definition, - aux_sym_program_repeat1, - [230] = 1, + [545] = 1, + ACTIONS(89), 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, - [238] = 1, - ACTIONS(95), 5, - anon_sym_RPAREN, - anon_sym_DASH_GT, - anon_sym_u2192, - anon_sym_COLON_EQ, - anon_sym_SEMI, - [246] = 1, - ACTIONS(97), 5, - anon_sym_RPAREN, - anon_sym_DASH_GT, - anon_sym_u2192, - anon_sym_COLON_EQ, - anon_sym_SEMI, - [254] = 3, + [569] = 4, + ACTIONS(5), 1, + sym_identifier, + ACTIONS(95), 1, + ts_builtin_sym_end, + ACTIONS(97), 1, + sym_comment, + STATE(26), 2, + sym_definition, + aux_sym_program_repeat1, + [583] = 3, ACTIONS(57), 1, anon_sym_LPAREN, ACTIONS(99), 1, @@ -1127,133 +1212,132 @@ static const uint16_t ts_small_parse_table[] = { STATE(17), 2, sym_param_block, aux_sym_labs_repeat1, - [265] = 2, - ACTIONS(57), 1, - anon_sym_LPAREN, - STATE(24), 2, - sym_param_block, - aux_sym_labs_repeat1, - [273] = 3, + [594] = 3, ACTIONS(101), 1, sym_identifier, - ACTIONS(104), 1, + ACTIONS(103), 1, anon_sym_COLON, STATE(33), 1, aux_sym_param_block_repeat1, - [283] = 2, + [604] = 3, + ACTIONS(105), 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, + sym_comment, + [630] = 2, ACTIONS(57), 1, anon_sym_LPAREN, STATE(31), 2, sym_param_block, aux_sym_labs_repeat1, - [291] = 3, - ACTIONS(106), 1, - sym_identifier, - ACTIONS(108), 1, - anon_sym_COLON, - STATE(37), 1, - aux_sym_param_block_repeat1, - [301] = 1, - ACTIONS(110), 3, - ts_builtin_sym_end, - sym_identifier, - sym_comment, - [307] = 3, - ACTIONS(112), 1, - sym_identifier, - ACTIONS(114), 1, - anon_sym_COLON, - STATE(33), 1, - aux_sym_param_block_repeat1, - [317] = 1, + [638] = 1, ACTIONS(116), 3, ts_builtin_sym_end, sym_identifier, sym_comment, - [323] = 1, + [644] = 2, + ACTIONS(57), 1, + anon_sym_LPAREN, + STATE(25), 2, + sym_param_block, + aux_sym_labs_repeat1, + [652] = 1, ACTIONS(118), 3, ts_builtin_sym_end, sym_identifier, sym_comment, - [329] = 1, + [658] = 1, ACTIONS(120), 1, - anon_sym_RPAREN, - [333] = 1, + anon_sym_SEMI, + [662] = 1, ACTIONS(122), 1, - anon_sym_COLON_EQ, - [337] = 1, - ACTIONS(124), 1, anon_sym_RPAREN, - [341] = 1, + [666] = 1, + ACTIONS(124), 1, + ts_builtin_sym_end, + [670] = 1, ACTIONS(126), 1, - anon_sym_LPAREN, - [345] = 1, + anon_sym_COLON_EQ, + [674] = 1, ACTIONS(128), 1, anon_sym_SEMI, - [349] = 1, + [678] = 1, ACTIONS(130), 1, - ts_builtin_sym_end, - [353] = 1, + anon_sym_SEMI, + [682] = 1, ACTIONS(132), 1, - anon_sym_COLON_EQ, - [357] = 1, - ACTIONS(134), 1, - anon_sym_SEMI, - [361] = 1, - ACTIONS(136), 1, - anon_sym_LPAREN, - [365] = 1, - ACTIONS(138), 1, - anon_sym_SEMI, - [369] = 1, - ACTIONS(140), 1, anon_sym_RPAREN, - [373] = 1, + [686] = 1, + ACTIONS(134), 1, + anon_sym_COLON_EQ, + [690] = 1, + ACTIONS(136), 1, + anon_sym_RPAREN, + [694] = 1, ACTIONS(63), 1, anon_sym_COLON_EQ, }; static const uint32_t ts_small_parse_table_map[] = { - [SMALL_STATE(12)] = 0, - [SMALL_STATE(13)] = 26, - [SMALL_STATE(14)] = 52, - [SMALL_STATE(15)] = 65, - [SMALL_STATE(16)] = 78, - [SMALL_STATE(17)] = 91, - [SMALL_STATE(18)] = 108, - [SMALL_STATE(19)] = 125, - [SMALL_STATE(20)] = 142, - [SMALL_STATE(21)] = 153, - [SMALL_STATE(22)] = 164, - [SMALL_STATE(23)] = 172, - [SMALL_STATE(24)] = 180, - [SMALL_STATE(25)] = 192, - [SMALL_STATE(26)] = 202, - [SMALL_STATE(27)] = 216, - [SMALL_STATE(28)] = 230, - [SMALL_STATE(29)] = 238, - [SMALL_STATE(30)] = 246, - [SMALL_STATE(31)] = 254, - [SMALL_STATE(32)] = 265, - [SMALL_STATE(33)] = 273, - [SMALL_STATE(34)] = 283, - [SMALL_STATE(35)] = 291, - [SMALL_STATE(36)] = 301, - [SMALL_STATE(37)] = 307, - [SMALL_STATE(38)] = 317, - [SMALL_STATE(39)] = 323, - [SMALL_STATE(40)] = 329, - [SMALL_STATE(41)] = 333, - [SMALL_STATE(42)] = 337, - [SMALL_STATE(43)] = 341, - [SMALL_STATE(44)] = 345, - [SMALL_STATE(45)] = 349, - [SMALL_STATE(46)] = 353, - [SMALL_STATE(47)] = 357, - [SMALL_STATE(48)] = 361, - [SMALL_STATE(49)] = 365, - [SMALL_STATE(50)] = 369, - [SMALL_STATE(51)] = 373, + [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, }; static const TSParseActionEntry ts_parse_actions[] = { @@ -1261,70 +1345,68 @@ static const TSParseActionEntry ts_parse_actions[] = { [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(27), - [9] = {.entry = {.count = 1, .reusable = false}}, SHIFT(16), - [11] = {.entry = {.count = 1, .reusable = true}}, SHIFT(6), - [13] = {.entry = {.count = 1, .reusable = true}}, SHIFT(16), - [15] = {.entry = {.count = 1, .reusable = true}}, SHIFT(14), - [17] = {.entry = {.count = 1, .reusable = true}}, SHIFT(48), - [19] = {.entry = {.count = 1, .reusable = false}}, SHIFT(48), - [21] = {.entry = {.count = 1, .reusable = true}}, SHIFT(43), - [23] = {.entry = {.count = 1, .reusable = false}}, SHIFT(43), + [7] = {.entry = {.count = 1, .reusable = true}}, SHIFT(30), + [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), + [21] = {.entry = {.count = 1, .reusable = true}}, SHIFT(36), + [23] = {.entry = {.count = 1, .reusable = false}}, SHIFT(36), [25] = {.entry = {.count = 1, .reusable = false}}, SHIFT(44), - [27] = {.entry = {.count = 1, .reusable = false}}, SHIFT(49), - [29] = {.entry = {.count = 1, .reusable = false}}, SHIFT(47), + [27] = {.entry = {.count = 1, .reusable = false}}, SHIFT(40), + [29] = {.entry = {.count = 1, .reusable = false}}, SHIFT(45), [31] = {.entry = {.count = 1, .reusable = true}}, REDUCE(sym_app, 1, 0, 0), - [33] = {.entry = {.count = 2, .reusable = true}}, REDUCE(aux_sym_app_repeat1, 2, 0, 0), SHIFT_REPEAT(16), - [36] = {.entry = {.count = 2, .reusable = true}}, REDUCE(aux_sym_app_repeat1, 2, 0, 0), SHIFT_REPEAT(6), + [33] = {.entry = {.count = 2, .reusable = true}}, REDUCE(aux_sym_app_repeat1, 2, 0, 0), SHIFT_REPEAT(15), + [36] = {.entry = {.count = 2, .reusable = true}}, REDUCE(aux_sym_app_repeat1, 2, 0, 0), SHIFT_REPEAT(8), [39] = {.entry = {.count = 1, .reusable = true}}, REDUCE(aux_sym_app_repeat1, 2, 0, 0), - [41] = {.entry = {.count = 2, .reusable = true}}, REDUCE(aux_sym_app_repeat1, 2, 0, 0), SHIFT_REPEAT(14), - [44] = {.entry = {.count = 1, .reusable = true}}, REDUCE(sym_square, 1, 0, 0), - [46] = {.entry = {.count = 1, .reusable = true}}, REDUCE(sym_term, 3, 0, 0), - [48] = {.entry = {.count = 1, .reusable = true}}, REDUCE(sym_term, 1, 0, 0), - [50] = {.entry = {.count = 2, .reusable = true}}, REDUCE(aux_sym_labs_repeat1, 2, 0, 0), SHIFT_REPEAT(35), + [41] = {.entry = {.count = 2, .reusable = true}}, REDUCE(aux_sym_app_repeat1, 2, 0, 0), SHIFT_REPEAT(16), + [44] = {.entry = {.count = 1, .reusable = true}}, REDUCE(sym_term, 3, 0, 0), + [46] = {.entry = {.count = 1, .reusable = true}}, REDUCE(sym_term, 1, 0, 0), + [48] = {.entry = {.count = 1, .reusable = true}}, REDUCE(sym_square, 1, 0, 0), + [50] = {.entry = {.count = 2, .reusable = true}}, REDUCE(aux_sym_labs_repeat1, 2, 0, 0), SHIFT_REPEAT(32), [53] = {.entry = {.count = 1, .reusable = false}}, REDUCE(aux_sym_labs_repeat1, 2, 0, 0), [55] = {.entry = {.count = 1, .reusable = true}}, REDUCE(aux_sym_labs_repeat1, 2, 0, 0), - [57] = {.entry = {.count = 1, .reusable = true}}, SHIFT(35), + [57] = {.entry = {.count = 1, .reusable = true}}, SHIFT(32), [59] = {.entry = {.count = 1, .reusable = false}}, SHIFT(5), - [61] = {.entry = {.count = 1, .reusable = true}}, SHIFT(2), - [63] = {.entry = {.count = 1, .reusable = true}}, SHIFT(3), - [65] = {.entry = {.count = 1, .reusable = true}}, REDUCE(sym_param_block, 5, 0, 0), - [67] = {.entry = {.count = 1, .reusable = false}}, REDUCE(sym_param_block, 5, 0, 0), - [69] = {.entry = {.count = 1, .reusable = true}}, REDUCE(sym_param_block, 4, 0, 0), - [71] = {.entry = {.count = 1, .reusable = false}}, REDUCE(sym_param_block, 4, 0, 0), - [73] = {.entry = {.count = 1, .reusable = true}}, REDUCE(sym_app_term, 1, 0, 0), - [75] = {.entry = {.count = 1, .reusable = true}}, REDUCE(sym_expr, 1, 0, 0), - [77] = {.entry = {.count = 1, .reusable = true}}, SHIFT(10), - [79] = {.entry = {.count = 1, .reusable = true}}, SHIFT(9), + [61] = {.entry = {.count = 1, .reusable = true}}, SHIFT(3), + [63] = {.entry = {.count = 1, .reusable = true}}, SHIFT(2), + [65] = {.entry = {.count = 1, .reusable = true}}, REDUCE(sym_param_block, 4, 0, 3), + [67] = {.entry = {.count = 1, .reusable = false}}, REDUCE(sym_param_block, 4, 0, 3), + [69] = {.entry = {.count = 1, .reusable = true}}, REDUCE(sym_param_block, 5, 0, 4), + [71] = {.entry = {.count = 1, .reusable = false}}, REDUCE(sym_param_block, 5, 0, 4), + [73] = {.entry = {.count = 1, .reusable = true}}, REDUCE(sym_expr, 1, 0, 0), + [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_program, 1, 0, 0), - [91] = {.entry = {.count = 1, .reusable = true}}, SHIFT(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_labs, 4, 0, 0), - [97] = {.entry = {.count = 1, .reusable = true}}, REDUCE(sym_pabs, 4, 0, 0), - [99] = {.entry = {.count = 1, .reusable = true}}, SHIFT(11), - [101] = {.entry = {.count = 2, .reusable = true}}, REDUCE(aux_sym_param_block_repeat1, 2, 0, 0), SHIFT_REPEAT(33), - [104] = {.entry = {.count = 1, .reusable = true}}, REDUCE(aux_sym_param_block_repeat1, 2, 0, 0), - [106] = {.entry = {.count = 1, .reusable = true}}, SHIFT(37), - [108] = {.entry = {.count = 1, .reusable = true}}, SHIFT(7), - [110] = {.entry = {.count = 1, .reusable = true}}, REDUCE(sym_definition, 5, 0, 0), - [112] = {.entry = {.count = 1, .reusable = true}}, SHIFT(33), - [114] = {.entry = {.count = 1, .reusable = true}}, SHIFT(8), - [116] = {.entry = {.count = 1, .reusable = true}}, REDUCE(sym_definition, 4, 0, 0), - [118] = {.entry = {.count = 1, .reusable = true}}, REDUCE(sym_definition, 6, 0, 0), - [120] = {.entry = {.count = 1, .reusable = true}}, SHIFT(20), - [122] = {.entry = {.count = 1, .reusable = true}}, REDUCE(sym_ascription, 2, 0, 0), - [124] = {.entry = {.count = 1, .reusable = true}}, SHIFT(15), - [126] = {.entry = {.count = 1, .reusable = true}}, REDUCE(sym_pi, 1, 0, 0), - [128] = {.entry = {.count = 1, .reusable = true}}, SHIFT(38), - [130] = {.entry = {.count = 1, .reusable = true}}, ACCEPT_INPUT(), - [132] = {.entry = {.count = 1, .reusable = true}}, SHIFT(4), - [134] = {.entry = {.count = 1, .reusable = true}}, SHIFT(39), - [136] = {.entry = {.count = 1, .reusable = true}}, REDUCE(sym_lambda, 1, 0, 0), - [138] = {.entry = {.count = 1, .reusable = true}}, SHIFT(36), - [140] = {.entry = {.count = 1, .reusable = true}}, SHIFT(21), + [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), }; #ifdef __cplusplus @@ -1355,6 +1437,9 @@ TS_PUBLIC const TSLanguage *tree_sitter_perga(void) { .small_parse_table_map = ts_small_parse_table_map, .parse_actions = ts_parse_actions, .symbol_names = ts_symbol_names, + .field_names = ts_field_names, + .field_map_slices = ts_field_map_slices, + .field_map_entries = ts_field_map_entries, .symbol_metadata = ts_symbol_metadata, .public_symbol_map = ts_symbol_map, .alias_map = ts_non_terminal_alias_map, diff --git a/src/tree_sitter/alloc.h b/src/tree_sitter/alloc.h index 1abdd12..1f4466d 100644 --- a/src/tree_sitter/alloc.h +++ b/src/tree_sitter/alloc.h @@ -12,10 +12,10 @@ extern "C" { // Allow clients to override allocation functions #ifdef TREE_SITTER_REUSE_ALLOCATOR -extern void *(*ts_current_malloc)(size_t size); -extern void *(*ts_current_calloc)(size_t count, size_t size); -extern void *(*ts_current_realloc)(void *ptr, size_t size); -extern void (*ts_current_free)(void *ptr); +extern void *(*ts_current_malloc)(size_t); +extern void *(*ts_current_calloc)(size_t, size_t); +extern void *(*ts_current_realloc)(void *, size_t); +extern void (*ts_current_free)(void *); #ifndef ts_malloc #define ts_malloc ts_current_malloc diff --git a/test/corpus/arrows.txt b/test/corpus/arrows.txt index cea8495..a478818 100644 --- a/test/corpus/arrows.txt +++ b/test/corpus/arrows.txt @@ -7,48 +7,55 @@ foo (A B : *) (f : A -> A -> B) (x : A) := f x 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 - (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 - (identifier)) - (term - (identifier)) - (term - (identifier))))))) + (definition + (identifier) + (param_block + (param + (identifier)) + (param + (identifier)) + (type + (expr + (app_term + (app + (term + (star))))))) + (param_block + (param + (identifier)) + (type + (expr + (arrow + (app_term + (app + (term + (identifier)))) + (expr + (arrow + (app_term + (app + (term + (identifier)))) + (expr + (app_term + (app + (term + (identifier))))))))))) + (param_block + (param + (identifier)) + (type + (expr + (app_term + (app + (term + (identifier))))))) + (expr + (app_term + (app + (term + (identifier)) + (term + (identifier)) + (term + (identifier))))))) diff --git a/test/corpus/axioms.txt b/test/corpus/axioms.txt index 1cdbf91..5221067 100644 --- a/test/corpus/axioms.txt +++ b/test/corpus/axioms.txt @@ -10,9 +10,10 @@ nat : * := axiom; (definition (identifier) (ascription - (expr - (app_term - (app - (term - (star)))))) + (type + (expr + (app_term + (app + (term + (star))))))) (axiom))) diff --git a/test/corpus/labs.txt b/test/corpus/labs.txt index b8a55c0..edca5ff 100644 --- a/test/corpus/labs.txt +++ b/test/corpus/labs.txt @@ -14,19 +14,23 @@ foo := fun (A : *) (x : A) => x; (labs (lambda) (param_block - (identifier) - (expr - (app_term - (app - (term - (star)))))) + (param + (identifier)) + (type + (expr + (app_term + (app + (term + (star))))))) (param_block - (identifier) - (expr - (app_term - (app - (term - (identifier)))))) + (param + (identifier)) + (type + (expr + (app_term + (app + (term + (identifier))))))) (expr (app_term (app diff --git a/test/corpus/pabs.txt b/test/corpus/pabs.txt index 44bb39e..b592538 100644 --- a/test/corpus/pabs.txt +++ b/test/corpus/pabs.txt @@ -14,19 +14,23 @@ rel := forall (A : *) (x : A), *; (pabs (pi) (param_block - (identifier) - (expr - (app_term - (app - (term - (star)))))) + (param + (identifier)) + (type + (expr + (app_term + (app + (term + (star))))))) (param_block - (identifier) - (expr - (app_term - (app - (term - (identifier)))))) + (param + (identifier)) + (type + (expr + (app_term + (app + (term + (identifier))))))) (expr (app_term (app diff --git a/test/corpus/params.txt b/test/corpus/params.txt index 927a406..91a5d9b 100644 --- a/test/corpus/params.txt +++ b/test/corpus/params.txt @@ -10,21 +10,27 @@ foo (A : *) (x y z : A) := x; (definition (identifier) (param_block - (identifier) - (expr - (app_term - (app - (term - (star)))))) + (param + (identifier)) + (type + (expr + (app_term + (app + (term + (star))))))) (param_block - (identifier) - (identifier) - (identifier) - (expr - (app_term - (app - (term - (identifier)))))) + (param + (identifier)) + (param + (identifier)) + (param + (identifier)) + (type + (expr + (app_term + (app + (term + (identifier))))))) (expr (app_term (app