From 6de6e3d801a513fc4b06180d80897e3f95bd57d5 Mon Sep 17 00:00:00 2001 From: William Ball Date: Sun, 1 Dec 2024 20:53:58 -0800 Subject: [PATCH] new syntax, also block comments are totally broken --- grammar.js | 27 +- src/grammar.json | 104 +- src/node-types.json | 52 +- src/parser.c | 3305 ++++++++++++++++++----------------- test/corpus/application.txt | 3 +- test/corpus/arrows.txt | 2 +- test/corpus/axioms.txt | 7 +- test/corpus/comments.txt | 20 +- test/corpus/include.txt | 2 +- test/corpus/labs.txt | 2 +- test/corpus/let.txt | 19 +- test/corpus/pabs.txt | 2 +- test/corpus/params.txt | 2 +- 13 files changed, 1786 insertions(+), 1761 deletions(-) diff --git a/grammar.js b/grammar.js index 00b9826..846e049 100644 --- a/grammar.js +++ b/grammar.js @@ -12,30 +12,17 @@ module.exports = grammar({ extras: $ => [ $.comment, - $.block_comment, /\s/, ], rules: { - program : $ => repeat(choice($.definition, $.preprocess)), + program : $ => repeat(choice($.definition, $.preprocess, $.axiom)), identifier : $ => /[a-zA-Z_]\w*/, comment : $ => token(seq('--', /.*/)), - block_comment: $ => token(seq( - '[*', - repeat(choice( - /[^\[\]*]/, - /\[[^*]/, - /\*[^\]]/, - /\[\*/, - /\*\]/, - )), - '*]' - )), - param_block : $ => seq( '(', field('param', repeat1($.identifier)), @@ -72,6 +59,7 @@ module.exports = grammar({ '(', $.identifier, repeat($.param_block), + optional($.ascription), ':=', $.expr, ')', @@ -112,12 +100,21 @@ module.exports = grammar({ field('type', $.expr), ), + axiom : $ => seq( + 'axiom', + field('name', $.identifier), + repeat($.param_block), + $.ascription, + ';' + ), + definition : $ => seq( + 'def', field('name', $.identifier), repeat($.param_block), optional($.ascription), ':=', - choice($.expr, $.axiom), + choice($.expr), ';', ), diff --git a/src/grammar.json b/src/grammar.json index f318b76..7e82397 100644 --- a/src/grammar.json +++ b/src/grammar.json @@ -13,6 +13,10 @@ { "type": "SYMBOL", "name": "preprocess" + }, + { + "type": "SYMBOL", + "name": "axiom" } ] } @@ -37,50 +41,6 @@ ] } }, - "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": [ @@ -261,6 +221,18 @@ "name": "param_block" } }, + { + "type": "CHOICE", + "members": [ + { + "type": "SYMBOL", + "name": "ascription" + }, + { + "type": "BLANK" + } + ] + }, { "type": "STRING", "value": ":=" @@ -311,8 +283,36 @@ } }, "axiom": { - "type": "STRING", - "value": "axiom" + "type": "SEQ", + "members": [ + { + "type": "STRING", + "value": "axiom" + }, + { + "type": "FIELD", + "name": "name", + "content": { + "type": "SYMBOL", + "name": "identifier" + } + }, + { + "type": "REPEAT", + "content": { + "type": "SYMBOL", + "name": "param_block" + } + }, + { + "type": "SYMBOL", + "name": "ascription" + }, + { + "type": "STRING", + "value": ";" + } + ] }, "arrow": { "type": "PREC_LEFT", @@ -398,6 +398,10 @@ "definition": { "type": "SEQ", "members": [ + { + "type": "STRING", + "value": "def" + }, { "type": "FIELD", "name": "name", @@ -435,10 +439,6 @@ { "type": "SYMBOL", "name": "expr" - }, - { - "type": "SYMBOL", - "name": "axiom" } ] }, @@ -475,10 +475,6 @@ "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 8ca0e6c..5f001a2 100644 --- a/src/node-types.json +++ b/src/node-types.json @@ -76,6 +76,36 @@ } } }, + { + "type": "axiom", + "named": true, + "fields": { + "name": { + "multiple": false, + "required": true, + "types": [ + { + "type": "identifier", + "named": true + } + ] + } + }, + "children": { + "multiple": true, + "required": true, + "types": [ + { + "type": "ascription", + "named": true + }, + { + "type": "param_block", + "named": true + } + ] + } + }, { "type": "binding", "named": true, @@ -84,6 +114,10 @@ "multiple": true, "required": true, "types": [ + { + "type": "ascription", + "named": true + }, { "type": "expr", "named": true @@ -122,10 +156,6 @@ "type": "ascription", "named": true }, - { - "type": "axiom", - "named": true - }, { "type": "expr", "named": true @@ -266,6 +296,10 @@ "multiple": true, "required": false, "types": [ + { + "type": "axiom", + "named": true + }, { "type": "definition", "named": true @@ -347,11 +381,7 @@ }, { "type": "axiom", - "named": true - }, - { - "type": "block_comment", - "named": true + "named": false }, { "type": "command", @@ -361,6 +391,10 @@ "type": "comment", "named": true }, + { + "type": "def", + "named": false + }, { "type": "end", "named": false diff --git a/src/parser.c b/src/parser.c index 3920c52..5074d2d 100644 --- a/src/parser.c +++ b/src/parser.c @@ -5,41 +5,41 @@ #endif #define LANGUAGE_VERSION 14 -#define STATE_COUNT 79 +#define STATE_COUNT 92 #define LARGE_STATE_COUNT 2 -#define SYMBOL_COUNT 47 +#define SYMBOL_COUNT 48 #define ALIAS_COUNT 0 #define TOKEN_COUNT 27 #define EXTERNAL_TOKEN_COUNT 0 #define FIELD_COUNT 3 -#define MAX_ALIAS_SEQUENCE_LENGTH 6 +#define MAX_ALIAS_SEQUENCE_LENGTH 7 #define PRODUCTION_ID_COUNT 4 enum ts_symbol_identifiers { sym_identifier = 1, sym_comment = 2, - 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, - anon_sym_COLON_EQ = 17, - anon_sym_let = 18, - anon_sym_in = 19, - anon_sym_end = 20, - sym_axiom = 21, + 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, + anon_sym_COLON_EQ = 16, + anon_sym_let = 17, + anon_sym_in = 18, + anon_sym_end = 19, + anon_sym_axiom = 20, + anon_sym_SEMI = 21, anon_sym_DASH_GT = 22, anon_sym_u2192 = 23, - anon_sym_SEMI = 24, + anon_sym_def = 24, sym_post_command = 25, sym_command = 26, sym_program = 27, @@ -51,24 +51,24 @@ enum ts_symbol_identifiers { sym_binding = 33, sym_let = 34, sym_app = 35, - sym_arrow = 36, - sym_app_term = 37, - sym_expr = 38, - sym_ascription = 39, - sym_definition = 40, - sym_preprocess = 41, - aux_sym_program_repeat1 = 42, - aux_sym_param_block_repeat1 = 43, - aux_sym_labs_repeat1 = 44, - aux_sym_let_repeat1 = 45, - aux_sym_app_repeat1 = 46, + sym_axiom = 36, + sym_arrow = 37, + sym_app_term = 38, + sym_expr = 39, + sym_ascription = 40, + sym_definition = 41, + sym_preprocess = 42, + aux_sym_program_repeat1 = 43, + aux_sym_param_block_repeat1 = 44, + aux_sym_labs_repeat1 = 45, + aux_sym_let_repeat1 = 46, + aux_sym_app_repeat1 = 47, }; 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] = ")", @@ -86,10 +86,11 @@ static const char * const ts_symbol_names[] = { [anon_sym_let] = "let", [anon_sym_in] = "in", [anon_sym_end] = "end", - [sym_axiom] = "axiom", + [anon_sym_axiom] = "axiom", + [anon_sym_SEMI] = ";", [anon_sym_DASH_GT] = "->", [anon_sym_u2192] = "\u2192", - [anon_sym_SEMI] = ";", + [anon_sym_def] = "def", [sym_post_command] = "post_command", [sym_command] = "command", [sym_program] = "program", @@ -101,6 +102,7 @@ static const char * const ts_symbol_names[] = { [sym_binding] = "binding", [sym_let] = "let", [sym_app] = "app", + [sym_axiom] = "axiom", [sym_arrow] = "arrow", [sym_app_term] = "app_term", [sym_expr] = "expr", @@ -118,7 +120,6 @@ 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, @@ -136,10 +137,11 @@ static const TSSymbol ts_symbol_map[] = { [anon_sym_let] = anon_sym_let, [anon_sym_in] = anon_sym_in, [anon_sym_end] = anon_sym_end, - [sym_axiom] = sym_axiom, + [anon_sym_axiom] = anon_sym_axiom, + [anon_sym_SEMI] = anon_sym_SEMI, [anon_sym_DASH_GT] = anon_sym_DASH_GT, [anon_sym_u2192] = anon_sym_u2192, - [anon_sym_SEMI] = anon_sym_SEMI, + [anon_sym_def] = anon_sym_def, [sym_post_command] = sym_post_command, [sym_command] = sym_command, [sym_program] = sym_program, @@ -151,6 +153,7 @@ static const TSSymbol ts_symbol_map[] = { [sym_binding] = sym_binding, [sym_let] = sym_let, [sym_app] = sym_app, + [sym_axiom] = sym_axiom, [sym_arrow] = sym_arrow, [sym_app_term] = sym_app_term, [sym_expr] = sym_expr, @@ -177,10 +180,6 @@ static const TSSymbolMetadata ts_symbol_metadata[] = { .visible = true, .named = true, }, - [sym_block_comment] = { - .visible = true, - .named = true, - }, [anon_sym_LPAREN] = { .visible = true, .named = false, @@ -249,9 +248,13 @@ static const TSSymbolMetadata ts_symbol_metadata[] = { .visible = true, .named = false, }, - [sym_axiom] = { + [anon_sym_axiom] = { .visible = true, - .named = true, + .named = false, + }, + [anon_sym_SEMI] = { + .visible = true, + .named = false, }, [anon_sym_DASH_GT] = { .visible = true, @@ -261,7 +264,7 @@ static const TSSymbolMetadata ts_symbol_metadata[] = { .visible = true, .named = false, }, - [anon_sym_SEMI] = { + [anon_sym_def] = { .visible = true, .named = false, }, @@ -309,6 +312,10 @@ static const TSSymbolMetadata ts_symbol_metadata[] = { .visible = true, .named = true, }, + [sym_axiom] = { + .visible = true, + .named = true, + }, [sym_arrow] = { .visible = true, .named = true, @@ -378,7 +385,7 @@ static const TSFieldMapEntry ts_field_map_entries[] = { [0] = {field_type, 1}, [1] = - {field_name, 0}, + {field_name, 1}, [2] = {field_param, 1}, {field_type, 3}, @@ -407,24 +414,24 @@ static const TSStateId ts_primary_state_ids[STATE_COUNT] = { [11] = 11, [12] = 12, [13] = 13, - [14] = 10, - [15] = 9, - [16] = 5, - [17] = 8, - [18] = 18, + [14] = 6, + [15] = 15, + [16] = 9, + [17] = 15, + [18] = 4, [19] = 19, - [20] = 18, - [21] = 19, - [22] = 22, + [20] = 20, + [21] = 20, + [22] = 19, [23] = 23, [24] = 24, - [25] = 24, + [25] = 25, [26] = 26, - [27] = 23, - [28] = 22, - [29] = 29, - [30] = 30, - [31] = 31, + [27] = 27, + [28] = 28, + [29] = 24, + [30] = 23, + [31] = 25, [32] = 32, [33] = 33, [34] = 34, @@ -435,30 +442,30 @@ static const TSStateId ts_primary_state_ids[STATE_COUNT] = { [39] = 39, [40] = 40, [41] = 41, - [42] = 40, + [42] = 42, [43] = 43, [44] = 44, [45] = 45, [46] = 46, - [47] = 47, - [48] = 43, + [47] = 45, + [48] = 48, [49] = 49, [50] = 50, - [51] = 41, + [51] = 51, [52] = 52, [53] = 53, [54] = 54, [55] = 55, - [56] = 50, - [57] = 57, + [56] = 56, + [57] = 55, [58] = 58, [59] = 59, - [60] = 54, - [61] = 61, + [60] = 60, + [61] = 43, [62] = 62, [63] = 63, - [64] = 64, - [65] = 65, + [64] = 58, + [65] = 63, [66] = 66, [67] = 67, [68] = 68, @@ -466,12 +473,25 @@ static const TSStateId ts_primary_state_ids[STATE_COUNT] = { [70] = 70, [71] = 71, [72] = 72, - [73] = 67, + [73] = 73, [74] = 74, [75] = 75, [76] = 76, [77] = 77, [78] = 78, + [79] = 79, + [80] = 80, + [81] = 81, + [82] = 82, + [83] = 83, + [84] = 84, + [85] = 85, + [86] = 76, + [87] = 87, + [88] = 88, + [89] = 89, + [90] = 90, + [91] = 91, }; static bool ts_lex(TSLexer *lexer, TSStateId state) { @@ -479,132 +499,126 @@ static bool ts_lex(TSLexer *lexer, TSStateId state) { eof = lexer->eof(lexer); switch (state) { case 0: - if (eof) ADVANCE(35); + if (eof) ADVANCE(33); ADVANCE_MAP( - '(', 54, - ')', 56, - '*', 57, - ',', 68, - '-', 8, - ':', 55, - ';', 79, - '=', 9, + '(', 46, + ')', 48, + '*', 49, + ',', 60, + '-', 6, + ':', 47, + ';', 68, + '=', 7, '@', 18, - '[', 5, + '[', 8, 'a', 32, + 'd', 13, 'e', 23, 'f', 27, 'i', 24, - 'l', 15, - 0x3bb, 60, - 0x2192, 78, - 0x21d2, 64, - 0x220f, 65, - 0x25a1, 58, + 'l', 14, + 0x3bb, 52, + 0x2192, 70, + 0x21d2, 56, + 0x220f, 57, + 0x25a1, 50, ); if (('\t' <= lookahead && lookahead <= '\r') || lookahead == ' ') SKIP(0); END_STATE(); case 1: if (lookahead == '\n') SKIP(1); - if (lookahead == '-') ADVANCE(84); - if (lookahead == '[') ADVANCE(83); + if (lookahead == '-') ADVANCE(72); if (('\t' <= lookahead && lookahead <= '\r') || - lookahead == ' ') ADVANCE(85); - if (lookahead != 0) ADVANCE(86); + lookahead == ' ') ADVANCE(73); + if (lookahead != 0) ADVANCE(74); END_STATE(); case 2: - if (lookahead == '(') ADVANCE(54); - if (lookahead == '*') ADVANCE(57); - if (lookahead == '-') ADVANCE(8); - if (lookahead == '[') ADVANCE(5); - if (lookahead == 'e') ADVANCE(44); - if (lookahead == 0x2192) ADVANCE(78); - if (lookahead == 0x25a1) ADVANCE(58); + ADVANCE_MAP( + '(', 46, + ')', 48, + '*', 49, + '-', 6, + ':', 47, + ';', 68, + '[', 8, + 0x2192, 70, + 0x25a1, 50, + ); if (('\t' <= lookahead && lookahead <= '\r') || lookahead == ' ') SKIP(2); if (('A' <= lookahead && lookahead <= 'Z') || lookahead == '_' || - ('a' <= lookahead && lookahead <= 'z')) ADVANCE(50); + ('a' <= lookahead && lookahead <= 'z')) ADVANCE(44); END_STATE(); case 3: - ADVANCE_MAP( - '(', 54, - '*', 57, - '-', 7, - '[', 5, - 'a', 49, - 'f', 45, - 'l', 38, - 0x3bb, 60, - 0x220f, 65, - 0x25a1, 58, - ); + if (lookahead == '(') ADVANCE(46); + if (lookahead == '*') ADVANCE(49); + if (lookahead == '-') ADVANCE(6); + if (lookahead == '[') ADVANCE(8); + if (lookahead == 'e') ADVANCE(40); + if (lookahead == 0x2192) ADVANCE(70); + if (lookahead == 0x25a1) ADVANCE(50); if (('\t' <= lookahead && lookahead <= '\r') || lookahead == ' ') SKIP(3); if (('A' <= lookahead && lookahead <= 'Z') || lookahead == '_' || - ('b' <= lookahead && lookahead <= 'z')) ADVANCE(50); + ('a' <= lookahead && lookahead <= 'z')) ADVANCE(44); END_STATE(); case 4: ADVANCE_MAP( - '(', 54, - '*', 57, - '-', 7, - '[', 5, - 'f', 45, - 'l', 38, - 0x3bb, 60, - 0x220f, 65, - 0x25a1, 58, + '(', 46, + '*', 49, + '-', 5, + '[', 8, + 'f', 41, + 'l', 36, + 0x3bb, 52, + 0x220f, 57, + 0x25a1, 50, ); if (('\t' <= lookahead && lookahead <= '\r') || lookahead == ' ') SKIP(4); if (('A' <= lookahead && lookahead <= 'Z') || lookahead == '_' || - ('a' <= lookahead && lookahead <= 'z')) ADVANCE(50); + ('a' <= lookahead && lookahead <= 'z')) ADVANCE(44); END_STATE(); case 5: - if (lookahead == '*') ADVANCE(6); - if (lookahead == ']') ADVANCE(59); + if (lookahead == '-') ADVANCE(45); END_STATE(); case 6: - if (lookahead == '*') ADVANCE(10); - if (lookahead == '[') ADVANCE(33); - if (lookahead != 0 && - lookahead != ']') ADVANCE(6); + if (lookahead == '-') ADVANCE(45); + if (lookahead == '>') ADVANCE(69); END_STATE(); case 7: - if (lookahead == '-') ADVANCE(51); + if (lookahead == '>') ADVANCE(55); END_STATE(); case 8: - if (lookahead == '-') ADVANCE(51); - if (lookahead == '>') ADVANCE(77); + if (lookahead == ']') ADVANCE(51); END_STATE(); case 9: - if (lookahead == '>') ADVANCE(63); - END_STATE(); - case 10: - if (lookahead == ']') ADVANCE(53); - if (lookahead != 0) ADVANCE(6); - END_STATE(); - case 11: if (lookahead == 'a') ADVANCE(21); END_STATE(); - case 12: + case 10: if (lookahead == 'c') ADVANCE(19); END_STATE(); + case 11: + if (lookahead == 'd') ADVANCE(65); + END_STATE(); + case 12: + if (lookahead == 'd') ADVANCE(15); + END_STATE(); case 13: - if (lookahead == 'd') ADVANCE(73); + if (lookahead == 'e') ADVANCE(16); END_STATE(); case 14: - if (lookahead == 'd') ADVANCE(16); - END_STATE(); - case 15: if (lookahead == 'e') ADVANCE(30); END_STATE(); + case 15: + if (lookahead == 'e') ADVANCE(75); + END_STATE(); case 16: - if (lookahead == 'e') ADVANCE(87); + if (lookahead == 'f') ADVANCE(71); END_STATE(); case 17: if (lookahead == 'i') ADVANCE(28); @@ -616,25 +630,25 @@ static bool ts_lex(TSLexer *lexer, TSStateId state) { if (lookahead == 'l') ADVANCE(31); END_STATE(); case 20: - if (lookahead == 'l') ADVANCE(66); + if (lookahead == 'l') ADVANCE(58); END_STATE(); case 21: if (lookahead == 'l') ADVANCE(20); END_STATE(); case 22: - if (lookahead == 'm') ADVANCE(75); + if (lookahead == 'm') ADVANCE(67); END_STATE(); case 23: - if (lookahead == 'n') ADVANCE(13); + if (lookahead == 'n') ADVANCE(11); END_STATE(); case 24: - if (lookahead == 'n') ADVANCE(72); + if (lookahead == 'n') ADVANCE(64); END_STATE(); case 25: - if (lookahead == 'n') ADVANCE(12); + if (lookahead == 'n') ADVANCE(10); END_STATE(); case 26: - if (lookahead == 'n') ADVANCE(61); + if (lookahead == 'n') ADVANCE(53); END_STATE(); case 27: if (lookahead == 'o') ADVANCE(29); @@ -644,329 +658,229 @@ static bool ts_lex(TSLexer *lexer, TSStateId state) { if (lookahead == 'o') ADVANCE(22); END_STATE(); case 29: - if (lookahead == 'r') ADVANCE(11); + if (lookahead == 'r') ADVANCE(9); END_STATE(); case 30: - if (lookahead == 't') ADVANCE(70); + if (lookahead == 't') ADVANCE(62); END_STATE(); case 31: - if (lookahead == 'u') ADVANCE(14); + if (lookahead == 'u') ADVANCE(12); END_STATE(); case 32: if (lookahead == 'x') ADVANCE(17); END_STATE(); case 33: - if (lookahead != 0) ADVANCE(6); + ACCEPT_TOKEN(ts_builtin_sym_end); END_STATE(); case 34: - if (eof) ADVANCE(35); - ADVANCE_MAP( - '(', 54, - ')', 56, - '*', 57, - '-', 8, - ':', 55, - ';', 79, - '@', 18, - '[', 5, - 0x2192, 78, - 0x25a1, 58, - ); - if (('\t' <= lookahead && lookahead <= '\r') || - lookahead == ' ') SKIP(34); - if (('A' <= lookahead && lookahead <= 'Z') || + ACCEPT_TOKEN(sym_identifier); + if (lookahead == 'a') ADVANCE(38); + if (('0' <= lookahead && lookahead <= '9') || + ('A' <= lookahead && lookahead <= 'Z') || lookahead == '_' || - ('a' <= lookahead && lookahead <= 'z')) ADVANCE(50); + ('b' <= lookahead && lookahead <= 'z')) ADVANCE(44); END_STATE(); case 35: - ACCEPT_TOKEN(ts_builtin_sym_end); + ACCEPT_TOKEN(sym_identifier); + if (lookahead == 'd') ADVANCE(66); + if (('0' <= lookahead && lookahead <= '9') || + ('A' <= lookahead && lookahead <= 'Z') || + lookahead == '_' || + ('a' <= lookahead && lookahead <= 'z')) ADVANCE(44); END_STATE(); case 36: ACCEPT_TOKEN(sym_identifier); - if (lookahead == 'a') ADVANCE(41); + if (lookahead == 'e') ADVANCE(43); if (('0' <= lookahead && lookahead <= '9') || ('A' <= lookahead && lookahead <= 'Z') || lookahead == '_' || - ('b' <= lookahead && lookahead <= 'z')) ADVANCE(50); + ('a' <= lookahead && lookahead <= 'z')) ADVANCE(44); END_STATE(); case 37: ACCEPT_TOKEN(sym_identifier); - if (lookahead == 'd') ADVANCE(74); + if (lookahead == 'l') ADVANCE(59); if (('0' <= lookahead && lookahead <= '9') || ('A' <= lookahead && lookahead <= 'Z') || lookahead == '_' || - ('a' <= lookahead && lookahead <= 'z')) ADVANCE(50); + ('a' <= lookahead && lookahead <= 'z')) ADVANCE(44); END_STATE(); case 38: ACCEPT_TOKEN(sym_identifier); - if (lookahead == 'e') ADVANCE(48); + if (lookahead == 'l') ADVANCE(37); if (('0' <= lookahead && lookahead <= '9') || ('A' <= lookahead && lookahead <= 'Z') || lookahead == '_' || - ('a' <= lookahead && lookahead <= 'z')) ADVANCE(50); + ('a' <= lookahead && lookahead <= 'z')) ADVANCE(44); END_STATE(); case 39: ACCEPT_TOKEN(sym_identifier); - if (lookahead == 'i') ADVANCE(46); + if (lookahead == 'n') ADVANCE(54); if (('0' <= lookahead && lookahead <= '9') || ('A' <= lookahead && lookahead <= 'Z') || lookahead == '_' || - ('a' <= lookahead && lookahead <= 'z')) ADVANCE(50); + ('a' <= lookahead && lookahead <= 'z')) ADVANCE(44); END_STATE(); case 40: ACCEPT_TOKEN(sym_identifier); - if (lookahead == 'l') ADVANCE(67); + if (lookahead == 'n') ADVANCE(35); if (('0' <= lookahead && lookahead <= '9') || ('A' <= lookahead && lookahead <= 'Z') || lookahead == '_' || - ('a' <= lookahead && lookahead <= 'z')) ADVANCE(50); + ('a' <= lookahead && lookahead <= 'z')) ADVANCE(44); END_STATE(); case 41: ACCEPT_TOKEN(sym_identifier); - if (lookahead == 'l') ADVANCE(40); + if (lookahead == 'o') ADVANCE(42); + if (lookahead == 'u') ADVANCE(39); if (('0' <= lookahead && lookahead <= '9') || ('A' <= lookahead && lookahead <= 'Z') || lookahead == '_' || - ('a' <= lookahead && lookahead <= 'z')) ADVANCE(50); + ('a' <= lookahead && lookahead <= 'z')) ADVANCE(44); END_STATE(); case 42: ACCEPT_TOKEN(sym_identifier); - if (lookahead == 'm') ADVANCE(76); + if (lookahead == 'r') ADVANCE(34); if (('0' <= lookahead && lookahead <= '9') || ('A' <= lookahead && lookahead <= 'Z') || lookahead == '_' || - ('a' <= lookahead && lookahead <= 'z')) ADVANCE(50); + ('a' <= lookahead && lookahead <= 'z')) ADVANCE(44); END_STATE(); case 43: ACCEPT_TOKEN(sym_identifier); - if (lookahead == 'n') ADVANCE(62); + if (lookahead == 't') ADVANCE(63); if (('0' <= lookahead && lookahead <= '9') || ('A' <= lookahead && lookahead <= 'Z') || lookahead == '_' || - ('a' <= lookahead && lookahead <= 'z')) ADVANCE(50); + ('a' <= lookahead && lookahead <= 'z')) ADVANCE(44); END_STATE(); case 44: ACCEPT_TOKEN(sym_identifier); - if (lookahead == 'n') ADVANCE(37); if (('0' <= lookahead && lookahead <= '9') || ('A' <= lookahead && lookahead <= 'Z') || lookahead == '_' || - ('a' <= lookahead && lookahead <= 'z')) ADVANCE(50); + ('a' <= lookahead && lookahead <= 'z')) ADVANCE(44); END_STATE(); case 45: - ACCEPT_TOKEN(sym_identifier); - if (lookahead == 'o') ADVANCE(47); - if (lookahead == 'u') ADVANCE(43); - if (('0' <= lookahead && lookahead <= '9') || - ('A' <= lookahead && lookahead <= 'Z') || - lookahead == '_' || - ('a' <= lookahead && lookahead <= 'z')) ADVANCE(50); - END_STATE(); - case 46: - ACCEPT_TOKEN(sym_identifier); - if (lookahead == 'o') ADVANCE(42); - if (('0' <= lookahead && lookahead <= '9') || - ('A' <= lookahead && lookahead <= 'Z') || - lookahead == '_' || - ('a' <= lookahead && lookahead <= 'z')) ADVANCE(50); - END_STATE(); - case 47: - ACCEPT_TOKEN(sym_identifier); - if (lookahead == 'r') ADVANCE(36); - if (('0' <= lookahead && lookahead <= '9') || - ('A' <= lookahead && lookahead <= 'Z') || - lookahead == '_' || - ('a' <= lookahead && lookahead <= 'z')) ADVANCE(50); - END_STATE(); - case 48: - ACCEPT_TOKEN(sym_identifier); - if (lookahead == 't') ADVANCE(71); - if (('0' <= lookahead && lookahead <= '9') || - ('A' <= lookahead && lookahead <= 'Z') || - lookahead == '_' || - ('a' <= lookahead && lookahead <= 'z')) ADVANCE(50); - END_STATE(); - case 49: - ACCEPT_TOKEN(sym_identifier); - if (lookahead == 'x') ADVANCE(39); - if (('0' <= lookahead && lookahead <= '9') || - ('A' <= lookahead && lookahead <= 'Z') || - lookahead == '_' || - ('a' <= lookahead && lookahead <= 'z')) ADVANCE(50); - END_STATE(); - case 50: - ACCEPT_TOKEN(sym_identifier); - if (('0' <= lookahead && lookahead <= '9') || - ('A' <= lookahead && lookahead <= 'Z') || - lookahead == '_' || - ('a' <= lookahead && lookahead <= 'z')) ADVANCE(50); - END_STATE(); - case 51: ACCEPT_TOKEN(sym_comment); if (lookahead != 0 && - lookahead != '\n') ADVANCE(51); + lookahead != '\n') ADVANCE(45); END_STATE(); - case 52: - ACCEPT_TOKEN(sym_block_comment); - if (lookahead == '\n') ADVANCE(6); - if (lookahead == '*') ADVANCE(81); - if (lookahead == '[') ADVANCE(82); - if (lookahead == ']') ADVANCE(86); - if (lookahead != 0) ADVANCE(80); - END_STATE(); - case 53: - ACCEPT_TOKEN(sym_block_comment); - if (lookahead == '*') ADVANCE(10); - if (lookahead == '[') ADVANCE(33); - if (lookahead != 0 && - lookahead != ']') ADVANCE(6); - END_STATE(); - case 54: + case 46: ACCEPT_TOKEN(anon_sym_LPAREN); END_STATE(); - case 55: + case 47: ACCEPT_TOKEN(anon_sym_COLON); - if (lookahead == '=') ADVANCE(69); + if (lookahead == '=') ADVANCE(61); END_STATE(); - case 56: + case 48: ACCEPT_TOKEN(anon_sym_RPAREN); END_STATE(); - case 57: + case 49: ACCEPT_TOKEN(sym_star); END_STATE(); - case 58: + case 50: ACCEPT_TOKEN(anon_sym_u25a1); END_STATE(); - case 59: + case 51: ACCEPT_TOKEN(anon_sym_LBRACK_RBRACK); END_STATE(); - case 60: + case 52: ACCEPT_TOKEN(anon_sym_u03bb); END_STATE(); - case 61: + case 53: ACCEPT_TOKEN(anon_sym_fun); END_STATE(); - case 62: + case 54: ACCEPT_TOKEN(anon_sym_fun); if (('0' <= lookahead && lookahead <= '9') || ('A' <= lookahead && lookahead <= 'Z') || lookahead == '_' || - ('a' <= lookahead && lookahead <= 'z')) ADVANCE(50); + ('a' <= lookahead && lookahead <= 'z')) ADVANCE(44); END_STATE(); - case 63: + case 55: ACCEPT_TOKEN(anon_sym_EQ_GT); END_STATE(); - case 64: + case 56: ACCEPT_TOKEN(anon_sym_u21d2); END_STATE(); - case 65: + case 57: ACCEPT_TOKEN(anon_sym_u220f); END_STATE(); - case 66: + case 58: ACCEPT_TOKEN(anon_sym_forall); END_STATE(); - case 67: + case 59: ACCEPT_TOKEN(anon_sym_forall); if (('0' <= lookahead && lookahead <= '9') || ('A' <= lookahead && lookahead <= 'Z') || lookahead == '_' || - ('a' <= lookahead && lookahead <= 'z')) ADVANCE(50); + ('a' <= lookahead && lookahead <= 'z')) ADVANCE(44); END_STATE(); - case 68: + case 60: ACCEPT_TOKEN(anon_sym_COMMA); END_STATE(); - case 69: + case 61: ACCEPT_TOKEN(anon_sym_COLON_EQ); END_STATE(); - case 70: + case 62: ACCEPT_TOKEN(anon_sym_let); END_STATE(); - case 71: + case 63: ACCEPT_TOKEN(anon_sym_let); if (('0' <= lookahead && lookahead <= '9') || ('A' <= lookahead && lookahead <= 'Z') || lookahead == '_' || - ('a' <= lookahead && lookahead <= 'z')) ADVANCE(50); + ('a' <= lookahead && lookahead <= 'z')) ADVANCE(44); END_STATE(); - case 72: + case 64: ACCEPT_TOKEN(anon_sym_in); END_STATE(); - case 73: + case 65: ACCEPT_TOKEN(anon_sym_end); END_STATE(); - case 74: + case 66: ACCEPT_TOKEN(anon_sym_end); if (('0' <= lookahead && lookahead <= '9') || ('A' <= lookahead && lookahead <= 'Z') || lookahead == '_' || - ('a' <= lookahead && lookahead <= 'z')) ADVANCE(50); + ('a' <= lookahead && lookahead <= 'z')) ADVANCE(44); END_STATE(); - case 75: - ACCEPT_TOKEN(sym_axiom); + case 67: + ACCEPT_TOKEN(anon_sym_axiom); END_STATE(); - case 76: - ACCEPT_TOKEN(sym_axiom); - if (('0' <= lookahead && lookahead <= '9') || - ('A' <= lookahead && lookahead <= 'Z') || - lookahead == '_' || - ('a' <= lookahead && lookahead <= 'z')) ADVANCE(50); - END_STATE(); - case 77: - ACCEPT_TOKEN(anon_sym_DASH_GT); - END_STATE(); - case 78: - ACCEPT_TOKEN(anon_sym_u2192); - END_STATE(); - case 79: + case 68: ACCEPT_TOKEN(anon_sym_SEMI); END_STATE(); - case 80: - ACCEPT_TOKEN(sym_post_command); - if (lookahead == '\n') ADVANCE(6); - if (lookahead == '*') ADVANCE(81); - if (lookahead == '[') ADVANCE(82); - if (lookahead == ']') ADVANCE(86); - if (lookahead != 0) ADVANCE(80); + case 69: + ACCEPT_TOKEN(anon_sym_DASH_GT); END_STATE(); - case 81: - ACCEPT_TOKEN(sym_post_command); - if (lookahead == '\n') ADVANCE(6); - if (lookahead == ']') ADVANCE(52); - if (lookahead != 0) ADVANCE(80); + case 70: + ACCEPT_TOKEN(anon_sym_u2192); END_STATE(); - case 82: - ACCEPT_TOKEN(sym_post_command); - if (lookahead == '\n') ADVANCE(6); - if (lookahead != 0) ADVANCE(80); + case 71: + ACCEPT_TOKEN(anon_sym_def); END_STATE(); - case 83: + case 72: ACCEPT_TOKEN(sym_post_command); - if (lookahead == '*') ADVANCE(80); + if (lookahead == '-') ADVANCE(45); if (lookahead != 0 && - lookahead != '\n') ADVANCE(86); + lookahead != '\n') ADVANCE(74); END_STATE(); - case 84: + case 73: ACCEPT_TOKEN(sym_post_command); - if (lookahead == '-') ADVANCE(51); - if (lookahead != 0 && - lookahead != '\n') ADVANCE(86); - END_STATE(); - case 85: - ACCEPT_TOKEN(sym_post_command); - if (lookahead == '-') ADVANCE(84); - if (lookahead == '[') ADVANCE(83); + if (lookahead == '-') ADVANCE(72); if (lookahead == '\t' || (0x0b <= lookahead && lookahead <= '\r') || - lookahead == ' ') ADVANCE(85); + lookahead == ' ') ADVANCE(73); if (lookahead != 0 && - (lookahead < '\t' || '\r' < lookahead)) ADVANCE(86); + (lookahead < '\t' || '\r' < lookahead)) ADVANCE(74); END_STATE(); - case 86: + case 74: ACCEPT_TOKEN(sym_post_command); if (lookahead != 0 && - lookahead != '\n') ADVANCE(86); + lookahead != '\n') ADVANCE(74); END_STATE(); - case 87: + case 75: ACCEPT_TOKEN(sym_command); END_STATE(); default: @@ -976,10 +890,10 @@ static bool ts_lex(TSLexer *lexer, TSStateId state) { static const TSLexMode ts_lex_modes[STATE_COUNT] = { [0] = {.lex_state = 0}, - [1] = {.lex_state = 34}, - [2] = {.lex_state = 3}, - [3] = {.lex_state = 3}, - [4] = {.lex_state = 3}, + [1] = {.lex_state = 0}, + [2] = {.lex_state = 4}, + [3] = {.lex_state = 4}, + [4] = {.lex_state = 4}, [5] = {.lex_state = 4}, [6] = {.lex_state = 4}, [7] = {.lex_state = 4}, @@ -993,21 +907,21 @@ static const TSLexMode ts_lex_modes[STATE_COUNT] = { [15] = {.lex_state = 4}, [16] = {.lex_state = 4}, [17] = {.lex_state = 4}, - [18] = {.lex_state = 34}, - [19] = {.lex_state = 34}, + [18] = {.lex_state = 4}, + [19] = {.lex_state = 2}, [20] = {.lex_state = 2}, - [21] = {.lex_state = 2}, - [22] = {.lex_state = 34}, - [23] = {.lex_state = 34}, - [24] = {.lex_state = 34}, + [21] = {.lex_state = 3}, + [22] = {.lex_state = 3}, + [23] = {.lex_state = 2}, + [24] = {.lex_state = 2}, [25] = {.lex_state = 2}, [26] = {.lex_state = 0}, - [27] = {.lex_state = 2}, - [28] = {.lex_state = 2}, - [29] = {.lex_state = 34}, - [30] = {.lex_state = 0}, - [31] = {.lex_state = 0}, - [32] = {.lex_state = 34}, + [27] = {.lex_state = 0}, + [28] = {.lex_state = 0}, + [29] = {.lex_state = 3}, + [30] = {.lex_state = 3}, + [31] = {.lex_state = 3}, + [32] = {.lex_state = 0}, [33] = {.lex_state = 0}, [34] = {.lex_state = 0}, [35] = {.lex_state = 0}, @@ -1024,43 +938,55 @@ static const TSLexMode ts_lex_modes[STATE_COUNT] = { [46] = {.lex_state = 0}, [47] = {.lex_state = 0}, [48] = {.lex_state = 0}, - [49] = {.lex_state = 34}, + [49] = {.lex_state = 0}, [50] = {.lex_state = 0}, [51] = {.lex_state = 0}, - [52] = {.lex_state = 34}, - [53] = {.lex_state = 34}, + [52] = {.lex_state = 0}, + [53] = {.lex_state = 0}, [54] = {.lex_state = 0}, - [55] = {.lex_state = 34}, + [55] = {.lex_state = 0}, [56] = {.lex_state = 0}, - [57] = {.lex_state = 34}, - [58] = {.lex_state = 34}, + [57] = {.lex_state = 0}, + [58] = {.lex_state = 0}, [59] = {.lex_state = 0}, - [60] = {.lex_state = 0}, + [60] = {.lex_state = 2}, [61] = {.lex_state = 0}, - [62] = {.lex_state = 34}, + [62] = {.lex_state = 2}, [63] = {.lex_state = 0}, [64] = {.lex_state = 0}, [65] = {.lex_state = 0}, [66] = {.lex_state = 0}, [67] = {.lex_state = 0}, [68] = {.lex_state = 0}, - [69] = {.lex_state = 1}, + [69] = {.lex_state = 2}, [70] = {.lex_state = 0}, - [71] = {.lex_state = 34}, + [71] = {.lex_state = 0}, [72] = {.lex_state = 0}, [73] = {.lex_state = 0}, [74] = {.lex_state = 0}, [75] = {.lex_state = 0}, [76] = {.lex_state = 0}, [77] = {.lex_state = 0}, - [78] = {.lex_state = 0}, + [78] = {.lex_state = 2}, + [79] = {.lex_state = 0}, + [80] = {.lex_state = 0}, + [81] = {.lex_state = 0}, + [82] = {.lex_state = 2}, + [83] = {.lex_state = 0}, + [84] = {.lex_state = 1}, + [85] = {.lex_state = 2}, + [86] = {.lex_state = 0}, + [87] = {.lex_state = 0}, + [88] = {.lex_state = 0}, + [89] = {.lex_state = 0}, + [90] = {.lex_state = 0}, + [91] = {.lex_state = 0}, }; static const uint16_t ts_parse_table[LARGE_STATE_COUNT][SYMBOL_COUNT] = { [0] = { [ts_builtin_sym_end] = 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), @@ -1078,752 +1004,793 @@ static const uint16_t ts_parse_table[LARGE_STATE_COUNT][SYMBOL_COUNT] = { [anon_sym_let] = ACTIONS(1), [anon_sym_in] = ACTIONS(1), [anon_sym_end] = ACTIONS(1), - [sym_axiom] = ACTIONS(1), + [anon_sym_axiom] = ACTIONS(1), + [anon_sym_SEMI] = ACTIONS(1), [anon_sym_DASH_GT] = ACTIONS(1), [anon_sym_u2192] = ACTIONS(1), - [anon_sym_SEMI] = ACTIONS(1), + [anon_sym_def] = ACTIONS(1), [sym_command] = ACTIONS(1), }, [1] = { - [sym_program] = STATE(75), - [sym_definition] = STATE(32), - [sym_preprocess] = STATE(32), - [aux_sym_program_repeat1] = STATE(32), + [sym_program] = STATE(71), + [sym_axiom] = STATE(27), + [sym_definition] = STATE(27), + [sym_preprocess] = STATE(27), + [aux_sym_program_repeat1] = STATE(27), [ts_builtin_sym_end] = ACTIONS(5), - [sym_identifier] = ACTIONS(7), [sym_comment] = ACTIONS(3), - [sym_block_comment] = ACTIONS(3), - [sym_command] = ACTIONS(9), + [anon_sym_axiom] = ACTIONS(7), + [anon_sym_def] = ACTIONS(9), + [sym_command] = ACTIONS(11), }, }; static const uint16_t ts_small_parse_table[] = { - [0] = 17, - ACTIONS(11), 1, - sym_identifier, + [0] = 16, + ACTIONS(3), 1, + sym_comment, ACTIONS(13), 1, - anon_sym_LPAREN, + sym_identifier, ACTIONS(15), 1, + anon_sym_LPAREN, + ACTIONS(17), 1, sym_star, - ACTIONS(19), 1, - anon_sym_u03bb, ACTIONS(21), 1, - anon_sym_fun, + anon_sym_u03bb, ACTIONS(23), 1, - anon_sym_u220f, + anon_sym_fun, ACTIONS(25), 1, - anon_sym_forall, + anon_sym_u220f, ACTIONS(27), 1, - anon_sym_let, + anon_sym_forall, ACTIONS(29), 1, - sym_axiom, - STATE(23), 1, - sym_square, - STATE(35), 1, - sym_arrow, - STATE(41), 1, - sym_app_term, - STATE(76), 1, - sym_expr, - ACTIONS(3), 2, - sym_comment, - sym_block_comment, - ACTIONS(17), 2, - anon_sym_u25a1, - anon_sym_LBRACK_RBRACK, - STATE(19), 2, - sym_term, - aux_sym_app_repeat1, - STATE(39), 4, - sym_labs, - sym_pabs, - sym_let, - sym_app, - [58] = 17, - ACTIONS(11), 1, - sym_identifier, - ACTIONS(13), 1, - anon_sym_LPAREN, - ACTIONS(15), 1, - sym_star, - ACTIONS(19), 1, - anon_sym_u03bb, - ACTIONS(21), 1, - anon_sym_fun, - ACTIONS(23), 1, - anon_sym_u220f, - ACTIONS(25), 1, - anon_sym_forall, - ACTIONS(27), 1, anon_sym_let, - ACTIONS(31), 1, - sym_axiom, - STATE(23), 1, + STATE(24), 1, sym_square, - STATE(35), 1, + STATE(40), 1, sym_arrow, - STATE(41), 1, - sym_app_term, - STATE(72), 1, - sym_expr, - ACTIONS(3), 2, - sym_comment, - sym_block_comment, - ACTIONS(17), 2, - anon_sym_u25a1, - anon_sym_LBRACK_RBRACK, - STATE(19), 2, - sym_term, - aux_sym_app_repeat1, - STATE(39), 4, - sym_labs, - sym_pabs, - sym_let, - sym_app, - [116] = 17, - ACTIONS(11), 1, - sym_identifier, - ACTIONS(13), 1, - anon_sym_LPAREN, - ACTIONS(15), 1, - sym_star, - ACTIONS(19), 1, - anon_sym_u03bb, - ACTIONS(21), 1, - anon_sym_fun, - ACTIONS(23), 1, - anon_sym_u220f, - ACTIONS(25), 1, - anon_sym_forall, - ACTIONS(27), 1, - anon_sym_let, - ACTIONS(33), 1, - sym_axiom, - STATE(23), 1, - sym_square, - STATE(35), 1, - sym_arrow, - STATE(41), 1, - sym_app_term, - STATE(64), 1, - sym_expr, - ACTIONS(3), 2, - sym_comment, - sym_block_comment, - ACTIONS(17), 2, - anon_sym_u25a1, - anon_sym_LBRACK_RBRACK, - STATE(19), 2, - sym_term, - aux_sym_app_repeat1, - STATE(39), 4, - sym_labs, - sym_pabs, - sym_let, - sym_app, - [174] = 16, - ACTIONS(11), 1, - sym_identifier, - ACTIONS(13), 1, - anon_sym_LPAREN, - ACTIONS(15), 1, - sym_star, - ACTIONS(19), 1, - anon_sym_u03bb, - ACTIONS(21), 1, - anon_sym_fun, - ACTIONS(23), 1, - anon_sym_u220f, - ACTIONS(25), 1, - anon_sym_forall, - ACTIONS(27), 1, - anon_sym_let, - STATE(23), 1, - sym_square, - STATE(35), 1, - sym_arrow, - STATE(36), 1, - sym_expr, - STATE(41), 1, - sym_app_term, - ACTIONS(3), 2, - sym_comment, - sym_block_comment, - ACTIONS(17), 2, - anon_sym_u25a1, - anon_sym_LBRACK_RBRACK, - STATE(19), 2, - sym_term, - aux_sym_app_repeat1, - STATE(39), 4, - sym_labs, - sym_pabs, - sym_let, - sym_app, - [229] = 16, - ACTIONS(11), 1, - sym_identifier, - ACTIONS(13), 1, - anon_sym_LPAREN, - ACTIONS(15), 1, - sym_star, - ACTIONS(19), 1, - anon_sym_u03bb, - ACTIONS(21), 1, - anon_sym_fun, - ACTIONS(23), 1, - anon_sym_u220f, - ACTIONS(25), 1, - anon_sym_forall, - ACTIONS(27), 1, - anon_sym_let, - STATE(23), 1, - sym_square, - STATE(35), 1, - sym_arrow, - STATE(41), 1, - sym_app_term, - STATE(70), 1, - sym_expr, - ACTIONS(3), 2, - sym_comment, - sym_block_comment, - ACTIONS(17), 2, - anon_sym_u25a1, - anon_sym_LBRACK_RBRACK, - STATE(19), 2, - sym_term, - aux_sym_app_repeat1, - STATE(39), 4, - sym_labs, - sym_pabs, - sym_let, - sym_app, - [284] = 16, - ACTIONS(11), 1, - sym_identifier, - ACTIONS(13), 1, - anon_sym_LPAREN, - ACTIONS(15), 1, - sym_star, - ACTIONS(19), 1, - anon_sym_u03bb, - ACTIONS(21), 1, - anon_sym_fun, - ACTIONS(23), 1, - anon_sym_u220f, - ACTIONS(25), 1, - anon_sym_forall, - ACTIONS(27), 1, - anon_sym_let, - STATE(23), 1, - sym_square, - STATE(35), 1, - sym_arrow, - STATE(41), 1, - sym_app_term, - STATE(77), 1, - sym_expr, - ACTIONS(3), 2, - sym_comment, - sym_block_comment, - ACTIONS(17), 2, - anon_sym_u25a1, - anon_sym_LBRACK_RBRACK, - STATE(19), 2, - sym_term, - aux_sym_app_repeat1, - STATE(39), 4, - sym_labs, - sym_pabs, - sym_let, - sym_app, - [339] = 16, - ACTIONS(11), 1, - sym_identifier, - ACTIONS(13), 1, - anon_sym_LPAREN, - ACTIONS(15), 1, - sym_star, - ACTIONS(19), 1, - anon_sym_u03bb, - ACTIONS(21), 1, - anon_sym_fun, - ACTIONS(23), 1, - anon_sym_u220f, - ACTIONS(25), 1, - anon_sym_forall, - ACTIONS(27), 1, - anon_sym_let, - STATE(23), 1, - sym_square, - STATE(35), 1, - sym_arrow, - STATE(41), 1, - sym_app_term, - STATE(67), 1, - sym_expr, - ACTIONS(3), 2, - sym_comment, - sym_block_comment, - ACTIONS(17), 2, - anon_sym_u25a1, - anon_sym_LBRACK_RBRACK, - STATE(19), 2, - sym_term, - aux_sym_app_repeat1, - STATE(39), 4, - sym_labs, - sym_pabs, - sym_let, - sym_app, - [394] = 16, - ACTIONS(11), 1, - sym_identifier, - ACTIONS(13), 1, - anon_sym_LPAREN, - ACTIONS(15), 1, - sym_star, - ACTIONS(19), 1, - anon_sym_u03bb, - ACTIONS(21), 1, - anon_sym_fun, - ACTIONS(23), 1, - anon_sym_u220f, - ACTIONS(25), 1, - anon_sym_forall, - ACTIONS(27), 1, - anon_sym_let, - STATE(23), 1, - sym_square, - STATE(33), 1, - sym_expr, - STATE(35), 1, - sym_arrow, - STATE(41), 1, - sym_app_term, - ACTIONS(3), 2, - sym_comment, - sym_block_comment, - ACTIONS(17), 2, - anon_sym_u25a1, - anon_sym_LBRACK_RBRACK, - STATE(19), 2, - sym_term, - aux_sym_app_repeat1, - STATE(39), 4, - sym_labs, - sym_pabs, - sym_let, - sym_app, - [449] = 16, - ACTIONS(11), 1, - sym_identifier, - ACTIONS(13), 1, - anon_sym_LPAREN, - ACTIONS(15), 1, - sym_star, - ACTIONS(19), 1, - anon_sym_u03bb, - ACTIONS(21), 1, - anon_sym_fun, - ACTIONS(23), 1, - anon_sym_u220f, - ACTIONS(25), 1, - anon_sym_forall, - ACTIONS(27), 1, - anon_sym_let, - STATE(23), 1, - sym_square, - STATE(35), 1, - sym_arrow, - STATE(38), 1, - sym_expr, - STATE(41), 1, - sym_app_term, - ACTIONS(3), 2, - sym_comment, - sym_block_comment, - ACTIONS(17), 2, - anon_sym_u25a1, - anon_sym_LBRACK_RBRACK, - STATE(19), 2, - sym_term, - aux_sym_app_repeat1, - STATE(39), 4, - sym_labs, - sym_pabs, - sym_let, - sym_app, - [504] = 16, - ACTIONS(27), 1, - anon_sym_let, - ACTIONS(35), 1, - sym_identifier, - ACTIONS(37), 1, - anon_sym_LPAREN, - ACTIONS(39), 1, - sym_star, - ACTIONS(43), 1, - anon_sym_u03bb, - ACTIONS(45), 1, - anon_sym_fun, - ACTIONS(47), 1, - anon_sym_u220f, - ACTIONS(49), 1, - anon_sym_forall, - STATE(27), 1, - sym_square, - STATE(35), 1, - sym_arrow, - STATE(51), 1, - sym_app_term, - STATE(66), 1, - sym_expr, - ACTIONS(3), 2, - sym_comment, - sym_block_comment, - ACTIONS(41), 2, - anon_sym_u25a1, - anon_sym_LBRACK_RBRACK, - STATE(21), 2, - sym_term, - aux_sym_app_repeat1, - STATE(39), 4, - sym_labs, - sym_pabs, - sym_let, - sym_app, - [559] = 16, - ACTIONS(11), 1, - sym_identifier, - ACTIONS(13), 1, - anon_sym_LPAREN, - ACTIONS(15), 1, - sym_star, - ACTIONS(19), 1, - anon_sym_u03bb, - ACTIONS(21), 1, - anon_sym_fun, - ACTIONS(23), 1, - anon_sym_u220f, - ACTIONS(25), 1, - anon_sym_forall, - ACTIONS(27), 1, - anon_sym_let, - STATE(23), 1, - sym_square, - STATE(35), 1, - sym_arrow, - STATE(41), 1, + STATE(43), 1, sym_app_term, STATE(68), 1, sym_expr, - ACTIONS(3), 2, - sym_comment, - sym_block_comment, - ACTIONS(17), 2, + ACTIONS(19), 2, anon_sym_u25a1, anon_sym_LBRACK_RBRACK, STATE(19), 2, sym_term, aux_sym_app_repeat1, - STATE(39), 4, + STATE(32), 4, sym_labs, sym_pabs, sym_let, sym_app, - [614] = 16, - ACTIONS(11), 1, - sym_identifier, + [54] = 16, + ACTIONS(3), 1, + sym_comment, ACTIONS(13), 1, - anon_sym_LPAREN, + sym_identifier, ACTIONS(15), 1, + anon_sym_LPAREN, + ACTIONS(17), 1, sym_star, - ACTIONS(19), 1, - anon_sym_u03bb, ACTIONS(21), 1, - anon_sym_fun, + anon_sym_u03bb, ACTIONS(23), 1, - anon_sym_u220f, + anon_sym_fun, ACTIONS(25), 1, - anon_sym_forall, + anon_sym_u220f, ACTIONS(27), 1, + anon_sym_forall, + ACTIONS(29), 1, anon_sym_let, - STATE(23), 1, + STATE(24), 1, sym_square, - STATE(35), 1, + STATE(40), 1, sym_arrow, - STATE(41), 1, + STATE(43), 1, sym_app_term, - STATE(74), 1, + STATE(83), 1, sym_expr, - ACTIONS(3), 2, - sym_comment, - sym_block_comment, - ACTIONS(17), 2, + ACTIONS(19), 2, anon_sym_u25a1, anon_sym_LBRACK_RBRACK, STATE(19), 2, sym_term, aux_sym_app_repeat1, - STATE(39), 4, + STATE(32), 4, sym_labs, sym_pabs, sym_let, sym_app, - [669] = 16, - ACTIONS(27), 1, - anon_sym_let, - ACTIONS(35), 1, - sym_identifier, - ACTIONS(37), 1, - anon_sym_LPAREN, - ACTIONS(39), 1, - sym_star, - ACTIONS(43), 1, - anon_sym_u03bb, - ACTIONS(45), 1, - anon_sym_fun, - ACTIONS(47), 1, - anon_sym_u220f, - ACTIONS(49), 1, - anon_sym_forall, - STATE(27), 1, - sym_square, - STATE(35), 1, - sym_arrow, - STATE(38), 1, - sym_expr, - STATE(51), 1, - sym_app_term, - ACTIONS(3), 2, + [108] = 16, + ACTIONS(3), 1, sym_comment, - sym_block_comment, - ACTIONS(41), 2, + ACTIONS(13), 1, + sym_identifier, + ACTIONS(15), 1, + anon_sym_LPAREN, + ACTIONS(17), 1, + sym_star, + ACTIONS(21), 1, + anon_sym_u03bb, + ACTIONS(23), 1, + anon_sym_fun, + ACTIONS(25), 1, + anon_sym_u220f, + ACTIONS(27), 1, + anon_sym_forall, + ACTIONS(29), 1, + anon_sym_let, + STATE(24), 1, + sym_square, + STATE(40), 1, + sym_arrow, + STATE(43), 1, + sym_app_term, + STATE(76), 1, + sym_expr, + ACTIONS(19), 2, anon_sym_u25a1, anon_sym_LBRACK_RBRACK, - STATE(21), 2, + STATE(19), 2, sym_term, aux_sym_app_repeat1, - STATE(39), 4, + STATE(32), 4, sym_labs, sym_pabs, sym_let, sym_app, - [724] = 16, - ACTIONS(27), 1, - anon_sym_let, - ACTIONS(35), 1, + [162] = 16, + ACTIONS(3), 1, + sym_comment, + ACTIONS(13), 1, sym_identifier, - ACTIONS(37), 1, + ACTIONS(15), 1, anon_sym_LPAREN, - ACTIONS(39), 1, + ACTIONS(17), 1, sym_star, - ACTIONS(43), 1, + ACTIONS(21), 1, anon_sym_u03bb, - ACTIONS(45), 1, + ACTIONS(23), 1, anon_sym_fun, - ACTIONS(47), 1, + ACTIONS(25), 1, anon_sym_u220f, - ACTIONS(49), 1, + ACTIONS(27), 1, anon_sym_forall, - STATE(27), 1, + ACTIONS(29), 1, + anon_sym_let, + STATE(24), 1, + sym_square, + STATE(40), 1, + sym_arrow, + STATE(43), 1, + sym_app_term, + STATE(91), 1, + sym_expr, + ACTIONS(19), 2, + anon_sym_u25a1, + anon_sym_LBRACK_RBRACK, + STATE(19), 2, + sym_term, + aux_sym_app_repeat1, + STATE(32), 4, + sym_labs, + sym_pabs, + sym_let, + sym_app, + [216] = 16, + ACTIONS(3), 1, + sym_comment, + ACTIONS(13), 1, + sym_identifier, + ACTIONS(15), 1, + anon_sym_LPAREN, + ACTIONS(17), 1, + sym_star, + ACTIONS(21), 1, + anon_sym_u03bb, + ACTIONS(23), 1, + anon_sym_fun, + ACTIONS(25), 1, + anon_sym_u220f, + ACTIONS(27), 1, + anon_sym_forall, + ACTIONS(29), 1, + anon_sym_let, + STATE(24), 1, sym_square, STATE(33), 1, sym_expr, - STATE(35), 1, + STATE(40), 1, sym_arrow, - STATE(51), 1, + STATE(43), 1, sym_app_term, - ACTIONS(3), 2, - sym_comment, - sym_block_comment, - ACTIONS(41), 2, - anon_sym_u25a1, - anon_sym_LBRACK_RBRACK, - STATE(21), 2, - sym_term, - aux_sym_app_repeat1, - STATE(39), 4, - sym_labs, - sym_pabs, - sym_let, - sym_app, - [779] = 16, - ACTIONS(27), 1, - anon_sym_let, - ACTIONS(35), 1, - sym_identifier, - ACTIONS(37), 1, - anon_sym_LPAREN, - ACTIONS(39), 1, - sym_star, - ACTIONS(43), 1, - anon_sym_u03bb, - ACTIONS(45), 1, - anon_sym_fun, - ACTIONS(47), 1, - anon_sym_u220f, - ACTIONS(49), 1, - anon_sym_forall, - STATE(27), 1, - sym_square, - STATE(35), 1, - sym_arrow, - STATE(36), 1, - sym_expr, - STATE(51), 1, - sym_app_term, - ACTIONS(3), 2, - sym_comment, - sym_block_comment, - ACTIONS(41), 2, - anon_sym_u25a1, - anon_sym_LBRACK_RBRACK, - STATE(21), 2, - sym_term, - aux_sym_app_repeat1, - STATE(39), 4, - sym_labs, - sym_pabs, - sym_let, - sym_app, - [834] = 16, - ACTIONS(11), 1, - sym_identifier, - ACTIONS(13), 1, - anon_sym_LPAREN, - ACTIONS(15), 1, - sym_star, - ACTIONS(19), 1, - anon_sym_u03bb, - ACTIONS(21), 1, - anon_sym_fun, - ACTIONS(23), 1, - anon_sym_u220f, - ACTIONS(25), 1, - anon_sym_forall, - ACTIONS(27), 1, - anon_sym_let, - STATE(23), 1, - sym_square, - STATE(35), 1, - sym_arrow, - STATE(41), 1, - sym_app_term, - STATE(73), 1, - sym_expr, - ACTIONS(3), 2, - sym_comment, - sym_block_comment, - ACTIONS(17), 2, + ACTIONS(19), 2, anon_sym_u25a1, anon_sym_LBRACK_RBRACK, STATE(19), 2, sym_term, aux_sym_app_repeat1, - STATE(39), 4, + STATE(32), 4, sym_labs, sym_pabs, sym_let, sym_app, - [889] = 7, - ACTIONS(54), 1, - anon_sym_LPAREN, - STATE(23), 1, - sym_square, - ACTIONS(3), 2, + [270] = 16, + ACTIONS(3), 1, sym_comment, - sym_block_comment, - ACTIONS(51), 2, - sym_identifier, - sym_star, - ACTIONS(59), 2, - anon_sym_u25a1, - anon_sym_LBRACK_RBRACK, - STATE(18), 2, - sym_term, - aux_sym_app_repeat1, - ACTIONS(57), 5, - anon_sym_RPAREN, - anon_sym_COLON_EQ, - anon_sym_DASH_GT, - anon_sym_u2192, - anon_sym_SEMI, - [919] = 7, ACTIONS(13), 1, - anon_sym_LPAREN, - STATE(23), 1, - sym_square, - ACTIONS(3), 2, - sym_comment, - sym_block_comment, - ACTIONS(15), 2, sym_identifier, + ACTIONS(15), 1, + anon_sym_LPAREN, + ACTIONS(17), 1, sym_star, - ACTIONS(17), 2, + ACTIONS(21), 1, + anon_sym_u03bb, + ACTIONS(23), 1, + anon_sym_fun, + ACTIONS(25), 1, + anon_sym_u220f, + ACTIONS(27), 1, + anon_sym_forall, + ACTIONS(29), 1, + anon_sym_let, + STATE(24), 1, + sym_square, + STATE(40), 1, + sym_arrow, + STATE(43), 1, + sym_app_term, + STATE(79), 1, + sym_expr, + ACTIONS(19), 2, anon_sym_u25a1, anon_sym_LBRACK_RBRACK, - STATE(18), 2, + STATE(19), 2, sym_term, aux_sym_app_repeat1, - ACTIONS(62), 5, + STATE(32), 4, + sym_labs, + sym_pabs, + sym_let, + sym_app, + [324] = 16, + ACTIONS(3), 1, + sym_comment, + ACTIONS(13), 1, + sym_identifier, + ACTIONS(15), 1, + anon_sym_LPAREN, + ACTIONS(17), 1, + sym_star, + ACTIONS(21), 1, + anon_sym_u03bb, + ACTIONS(23), 1, + anon_sym_fun, + ACTIONS(25), 1, + anon_sym_u220f, + ACTIONS(27), 1, + anon_sym_forall, + ACTIONS(29), 1, + anon_sym_let, + STATE(24), 1, + sym_square, + STATE(40), 1, + sym_arrow, + STATE(43), 1, + sym_app_term, + STATE(88), 1, + sym_expr, + ACTIONS(19), 2, + anon_sym_u25a1, + anon_sym_LBRACK_RBRACK, + STATE(19), 2, + sym_term, + aux_sym_app_repeat1, + STATE(32), 4, + sym_labs, + sym_pabs, + sym_let, + sym_app, + [378] = 16, + ACTIONS(3), 1, + sym_comment, + ACTIONS(13), 1, + sym_identifier, + ACTIONS(15), 1, + anon_sym_LPAREN, + ACTIONS(17), 1, + sym_star, + ACTIONS(21), 1, + anon_sym_u03bb, + ACTIONS(23), 1, + anon_sym_fun, + ACTIONS(25), 1, + anon_sym_u220f, + ACTIONS(27), 1, + anon_sym_forall, + ACTIONS(29), 1, + anon_sym_let, + STATE(24), 1, + sym_square, + STATE(36), 1, + sym_expr, + STATE(40), 1, + sym_arrow, + STATE(43), 1, + sym_app_term, + ACTIONS(19), 2, + anon_sym_u25a1, + anon_sym_LBRACK_RBRACK, + STATE(19), 2, + sym_term, + aux_sym_app_repeat1, + STATE(32), 4, + sym_labs, + sym_pabs, + sym_let, + sym_app, + [432] = 16, + ACTIONS(3), 1, + sym_comment, + ACTIONS(29), 1, + anon_sym_let, + ACTIONS(31), 1, + sym_identifier, + ACTIONS(33), 1, + anon_sym_LPAREN, + ACTIONS(35), 1, + sym_star, + ACTIONS(39), 1, + anon_sym_u03bb, + ACTIONS(41), 1, + anon_sym_fun, + ACTIONS(43), 1, + anon_sym_u220f, + ACTIONS(45), 1, + anon_sym_forall, + STATE(29), 1, + sym_square, + STATE(40), 1, + sym_arrow, + STATE(61), 1, + sym_app_term, + STATE(77), 1, + sym_expr, + ACTIONS(37), 2, + anon_sym_u25a1, + anon_sym_LBRACK_RBRACK, + STATE(22), 2, + sym_term, + aux_sym_app_repeat1, + STATE(32), 4, + sym_labs, + sym_pabs, + sym_let, + sym_app, + [486] = 16, + ACTIONS(3), 1, + sym_comment, + ACTIONS(13), 1, + sym_identifier, + ACTIONS(15), 1, + anon_sym_LPAREN, + ACTIONS(17), 1, + sym_star, + ACTIONS(21), 1, + anon_sym_u03bb, + ACTIONS(23), 1, + anon_sym_fun, + ACTIONS(25), 1, + anon_sym_u220f, + ACTIONS(27), 1, + anon_sym_forall, + ACTIONS(29), 1, + anon_sym_let, + STATE(24), 1, + sym_square, + STATE(40), 1, + sym_arrow, + STATE(43), 1, + sym_app_term, + STATE(81), 1, + sym_expr, + ACTIONS(19), 2, + anon_sym_u25a1, + anon_sym_LBRACK_RBRACK, + STATE(19), 2, + sym_term, + aux_sym_app_repeat1, + STATE(32), 4, + sym_labs, + sym_pabs, + sym_let, + sym_app, + [540] = 16, + ACTIONS(3), 1, + sym_comment, + ACTIONS(13), 1, + sym_identifier, + ACTIONS(15), 1, + anon_sym_LPAREN, + ACTIONS(17), 1, + sym_star, + ACTIONS(21), 1, + anon_sym_u03bb, + ACTIONS(23), 1, + anon_sym_fun, + ACTIONS(25), 1, + anon_sym_u220f, + ACTIONS(27), 1, + anon_sym_forall, + ACTIONS(29), 1, + anon_sym_let, + STATE(24), 1, + sym_square, + STATE(40), 1, + sym_arrow, + STATE(43), 1, + sym_app_term, + STATE(72), 1, + sym_expr, + ACTIONS(19), 2, + anon_sym_u25a1, + anon_sym_LBRACK_RBRACK, + STATE(19), 2, + sym_term, + aux_sym_app_repeat1, + STATE(32), 4, + sym_labs, + sym_pabs, + sym_let, + sym_app, + [594] = 16, + ACTIONS(3), 1, + sym_comment, + ACTIONS(13), 1, + sym_identifier, + ACTIONS(15), 1, + anon_sym_LPAREN, + ACTIONS(17), 1, + sym_star, + ACTIONS(21), 1, + anon_sym_u03bb, + ACTIONS(23), 1, + anon_sym_fun, + ACTIONS(25), 1, + anon_sym_u220f, + ACTIONS(27), 1, + anon_sym_forall, + ACTIONS(29), 1, + anon_sym_let, + STATE(24), 1, + sym_square, + STATE(40), 1, + sym_arrow, + STATE(43), 1, + sym_app_term, + STATE(75), 1, + sym_expr, + ACTIONS(19), 2, + anon_sym_u25a1, + anon_sym_LBRACK_RBRACK, + STATE(19), 2, + sym_term, + aux_sym_app_repeat1, + STATE(32), 4, + sym_labs, + sym_pabs, + sym_let, + sym_app, + [648] = 16, + ACTIONS(3), 1, + sym_comment, + ACTIONS(29), 1, + anon_sym_let, + ACTIONS(31), 1, + sym_identifier, + ACTIONS(33), 1, + anon_sym_LPAREN, + ACTIONS(35), 1, + sym_star, + ACTIONS(39), 1, + anon_sym_u03bb, + ACTIONS(41), 1, + anon_sym_fun, + ACTIONS(43), 1, + anon_sym_u220f, + ACTIONS(45), 1, + anon_sym_forall, + STATE(29), 1, + sym_square, + STATE(33), 1, + sym_expr, + STATE(40), 1, + sym_arrow, + STATE(61), 1, + sym_app_term, + ACTIONS(37), 2, + anon_sym_u25a1, + anon_sym_LBRACK_RBRACK, + STATE(22), 2, + sym_term, + aux_sym_app_repeat1, + STATE(32), 4, + sym_labs, + sym_pabs, + sym_let, + sym_app, + [702] = 16, + ACTIONS(3), 1, + sym_comment, + ACTIONS(13), 1, + sym_identifier, + ACTIONS(15), 1, + anon_sym_LPAREN, + ACTIONS(17), 1, + sym_star, + ACTIONS(21), 1, + anon_sym_u03bb, + ACTIONS(23), 1, + anon_sym_fun, + ACTIONS(25), 1, + anon_sym_u220f, + ACTIONS(27), 1, + anon_sym_forall, + ACTIONS(29), 1, + anon_sym_let, + STATE(24), 1, + sym_square, + STATE(37), 1, + sym_expr, + STATE(40), 1, + sym_arrow, + STATE(43), 1, + sym_app_term, + ACTIONS(19), 2, + anon_sym_u25a1, + anon_sym_LBRACK_RBRACK, + STATE(19), 2, + sym_term, + aux_sym_app_repeat1, + STATE(32), 4, + sym_labs, + sym_pabs, + sym_let, + sym_app, + [756] = 16, + ACTIONS(3), 1, + sym_comment, + ACTIONS(29), 1, + anon_sym_let, + ACTIONS(31), 1, + sym_identifier, + ACTIONS(33), 1, + anon_sym_LPAREN, + ACTIONS(35), 1, + sym_star, + ACTIONS(39), 1, + anon_sym_u03bb, + ACTIONS(41), 1, + anon_sym_fun, + ACTIONS(43), 1, + anon_sym_u220f, + ACTIONS(45), 1, + anon_sym_forall, + STATE(29), 1, + sym_square, + STATE(36), 1, + sym_expr, + STATE(40), 1, + sym_arrow, + STATE(61), 1, + sym_app_term, + ACTIONS(37), 2, + anon_sym_u25a1, + anon_sym_LBRACK_RBRACK, + STATE(22), 2, + sym_term, + aux_sym_app_repeat1, + STATE(32), 4, + sym_labs, + sym_pabs, + sym_let, + sym_app, + [810] = 16, + ACTIONS(3), 1, + sym_comment, + ACTIONS(29), 1, + anon_sym_let, + ACTIONS(31), 1, + sym_identifier, + ACTIONS(33), 1, + anon_sym_LPAREN, + ACTIONS(35), 1, + sym_star, + ACTIONS(39), 1, + anon_sym_u03bb, + ACTIONS(41), 1, + anon_sym_fun, + ACTIONS(43), 1, + anon_sym_u220f, + ACTIONS(45), 1, + anon_sym_forall, + STATE(29), 1, + sym_square, + STATE(37), 1, + sym_expr, + STATE(40), 1, + sym_arrow, + STATE(61), 1, + sym_app_term, + ACTIONS(37), 2, + anon_sym_u25a1, + anon_sym_LBRACK_RBRACK, + STATE(22), 2, + sym_term, + aux_sym_app_repeat1, + STATE(32), 4, + sym_labs, + sym_pabs, + sym_let, + sym_app, + [864] = 16, + ACTIONS(3), 1, + sym_comment, + ACTIONS(13), 1, + sym_identifier, + ACTIONS(15), 1, + anon_sym_LPAREN, + ACTIONS(17), 1, + sym_star, + ACTIONS(21), 1, + anon_sym_u03bb, + ACTIONS(23), 1, + anon_sym_fun, + ACTIONS(25), 1, + anon_sym_u220f, + ACTIONS(27), 1, + anon_sym_forall, + ACTIONS(29), 1, + anon_sym_let, + STATE(24), 1, + sym_square, + STATE(40), 1, + sym_arrow, + STATE(43), 1, + sym_app_term, + STATE(86), 1, + sym_expr, + ACTIONS(19), 2, + anon_sym_u25a1, + anon_sym_LBRACK_RBRACK, + STATE(19), 2, + sym_term, + aux_sym_app_repeat1, + STATE(32), 4, + sym_labs, + sym_pabs, + sym_let, + sym_app, + [918] = 7, + ACTIONS(3), 1, + sym_comment, + ACTIONS(15), 1, + anon_sym_LPAREN, + STATE(24), 1, + sym_square, + ACTIONS(17), 2, + sym_identifier, + sym_star, + ACTIONS(19), 2, + anon_sym_u25a1, + anon_sym_LBRACK_RBRACK, + STATE(20), 2, + sym_term, + aux_sym_app_repeat1, + ACTIONS(47), 5, anon_sym_RPAREN, anon_sym_COLON_EQ, - anon_sym_DASH_GT, - anon_sym_u2192, anon_sym_SEMI, - [949] = 9, - ACTIONS(64), 1, - sym_identifier, - ACTIONS(67), 1, - anon_sym_LPAREN, - ACTIONS(70), 1, - sym_star, - ACTIONS(76), 1, - anon_sym_end, - STATE(27), 1, - sym_square, - ACTIONS(3), 2, + anon_sym_DASH_GT, + anon_sym_u2192, + [947] = 7, + ACTIONS(3), 1, sym_comment, - sym_block_comment, + ACTIONS(52), 1, + anon_sym_LPAREN, + STATE(24), 1, + sym_square, + ACTIONS(49), 2, + sym_identifier, + sym_star, ACTIONS(57), 2, - anon_sym_DASH_GT, - anon_sym_u2192, - ACTIONS(73), 2, anon_sym_u25a1, anon_sym_LBRACK_RBRACK, STATE(20), 2, sym_term, aux_sym_app_repeat1, - [981] = 9, - ACTIONS(35), 1, + ACTIONS(55), 5, + anon_sym_RPAREN, + anon_sym_COLON_EQ, + anon_sym_SEMI, + anon_sym_DASH_GT, + anon_sym_u2192, + [976] = 9, + ACTIONS(3), 1, + sym_comment, + ACTIONS(60), 1, sym_identifier, - ACTIONS(37), 1, + ACTIONS(63), 1, anon_sym_LPAREN, - ACTIONS(39), 1, + ACTIONS(66), 1, sym_star, - ACTIONS(78), 1, + ACTIONS(72), 1, anon_sym_end, - STATE(27), 1, + STATE(29), 1, sym_square, - ACTIONS(3), 2, - sym_comment, - sym_block_comment, - ACTIONS(41), 2, - anon_sym_u25a1, - anon_sym_LBRACK_RBRACK, - ACTIONS(62), 2, + ACTIONS(55), 2, anon_sym_DASH_GT, anon_sym_u2192, - STATE(20), 2, + ACTIONS(69), 2, + anon_sym_u25a1, + anon_sym_LBRACK_RBRACK, + STATE(21), 2, sym_term, aux_sym_app_repeat1, - [1013] = 2, - ACTIONS(3), 2, + [1007] = 9, + ACTIONS(3), 1, + sym_comment, + ACTIONS(31), 1, + sym_identifier, + ACTIONS(33), 1, + anon_sym_LPAREN, + ACTIONS(35), 1, + sym_star, + ACTIONS(74), 1, + anon_sym_end, + STATE(29), 1, + sym_square, + ACTIONS(37), 2, + anon_sym_u25a1, + anon_sym_LBRACK_RBRACK, + ACTIONS(47), 2, + anon_sym_DASH_GT, + anon_sym_u2192, + STATE(21), 2, + sym_term, + aux_sym_app_repeat1, + [1038] = 2, + ACTIONS(3), 1, + sym_comment, + ACTIONS(76), 10, + sym_identifier, + anon_sym_LPAREN, + anon_sym_RPAREN, + sym_star, + anon_sym_u25a1, + anon_sym_LBRACK_RBRACK, + anon_sym_COLON_EQ, + anon_sym_SEMI, + anon_sym_DASH_GT, + anon_sym_u2192, + [1054] = 2, + ACTIONS(3), 1, + sym_comment, + ACTIONS(78), 10, + sym_identifier, + anon_sym_LPAREN, + anon_sym_RPAREN, + sym_star, + anon_sym_u25a1, + anon_sym_LBRACK_RBRACK, + anon_sym_COLON_EQ, + anon_sym_SEMI, + anon_sym_DASH_GT, + anon_sym_u2192, + [1070] = 2, + ACTIONS(3), 1, sym_comment, - sym_block_comment, ACTIONS(80), 10, sym_identifier, anon_sym_LPAREN, @@ -1832,88 +1799,86 @@ static const uint16_t ts_small_parse_table[] = { anon_sym_u25a1, anon_sym_LBRACK_RBRACK, anon_sym_COLON_EQ, - anon_sym_DASH_GT, - anon_sym_u2192, anon_sym_SEMI, - [1030] = 2, - ACTIONS(3), 2, - sym_comment, - sym_block_comment, - ACTIONS(82), 10, - sym_identifier, - anon_sym_LPAREN, - anon_sym_RPAREN, - sym_star, - anon_sym_u25a1, - anon_sym_LBRACK_RBRACK, - anon_sym_COLON_EQ, anon_sym_DASH_GT, anon_sym_u2192, - anon_sym_SEMI, - [1047] = 2, - ACTIONS(3), 2, + [1086] = 5, + ACTIONS(3), 1, sym_comment, - sym_block_comment, - ACTIONS(84), 10, - sym_identifier, + ACTIONS(82), 1, anon_sym_LPAREN, - anon_sym_RPAREN, - sym_star, - anon_sym_u25a1, - anon_sym_LBRACK_RBRACK, - anon_sym_COLON_EQ, - anon_sym_DASH_GT, - anon_sym_u2192, - anon_sym_SEMI, - [1064] = 3, - ACTIONS(3), 2, - sym_comment, - sym_block_comment, - ACTIONS(86), 2, - sym_identifier, - anon_sym_end, - ACTIONS(84), 6, - anon_sym_LPAREN, - sym_star, - anon_sym_u25a1, - anon_sym_LBRACK_RBRACK, - anon_sym_DASH_GT, - anon_sym_u2192, - [1081] = 5, - ACTIONS(88), 1, - anon_sym_LPAREN, - ACTIONS(91), 1, + ACTIONS(85), 1, anon_sym_COLON, - ACTIONS(3), 2, - sym_comment, - sym_block_comment, STATE(26), 2, sym_param_block, aux_sym_labs_repeat1, - ACTIONS(93), 4, + ACTIONS(87), 4, anon_sym_EQ_GT, anon_sym_u21d2, anon_sym_COMMA, anon_sym_COLON_EQ, - [1102] = 3, - ACTIONS(3), 2, + [1106] = 6, + ACTIONS(3), 1, sym_comment, - sym_block_comment, - ACTIONS(95), 2, + ACTIONS(7), 1, + anon_sym_axiom, + ACTIONS(9), 1, + anon_sym_def, + ACTIONS(11), 1, + sym_command, + ACTIONS(89), 1, + ts_builtin_sym_end, + STATE(28), 4, + sym_axiom, + sym_definition, + sym_preprocess, + aux_sym_program_repeat1, + [1128] = 6, + ACTIONS(3), 1, + sym_comment, + ACTIONS(91), 1, + ts_builtin_sym_end, + ACTIONS(93), 1, + anon_sym_axiom, + ACTIONS(96), 1, + anon_sym_def, + ACTIONS(99), 1, + sym_command, + STATE(28), 4, + sym_axiom, + sym_definition, + sym_preprocess, + aux_sym_program_repeat1, + [1150] = 3, + ACTIONS(3), 1, + sym_comment, + ACTIONS(102), 2, sym_identifier, anon_sym_end, - ACTIONS(82), 6, + ACTIONS(78), 6, anon_sym_LPAREN, sym_star, anon_sym_u25a1, anon_sym_LBRACK_RBRACK, anon_sym_DASH_GT, anon_sym_u2192, - [1119] = 3, - ACTIONS(3), 2, + [1166] = 3, + ACTIONS(3), 1, sym_comment, - sym_block_comment, - ACTIONS(97), 2, + ACTIONS(104), 2, + sym_identifier, + anon_sym_end, + ACTIONS(76), 6, + anon_sym_LPAREN, + sym_star, + anon_sym_u25a1, + anon_sym_LBRACK_RBRACK, + anon_sym_DASH_GT, + anon_sym_u2192, + [1182] = 3, + ACTIONS(3), 1, + sym_comment, + ACTIONS(106), 2, sym_identifier, anon_sym_end, ACTIONS(80), 6, @@ -1923,541 +1888,572 @@ static const uint16_t ts_small_parse_table[] = { anon_sym_LBRACK_RBRACK, anon_sym_DASH_GT, anon_sym_u2192, - [1136] = 5, - ACTIONS(99), 1, - ts_builtin_sym_end, - ACTIONS(101), 1, - sym_identifier, - ACTIONS(104), 1, - sym_command, - ACTIONS(3), 2, + [1198] = 2, + ACTIONS(3), 1, sym_comment, - sym_block_comment, - STATE(29), 3, - sym_definition, - sym_preprocess, - aux_sym_program_repeat1, - [1155] = 6, - ACTIONS(107), 1, - anon_sym_LPAREN, - ACTIONS(109), 1, - anon_sym_COLON, - ACTIONS(111), 1, + ACTIONS(108), 6, + anon_sym_RPAREN, anon_sym_COLON_EQ, - STATE(78), 1, + anon_sym_end, + anon_sym_SEMI, + anon_sym_DASH_GT, + anon_sym_u2192, + [1210] = 2, + ACTIONS(3), 1, + sym_comment, + ACTIONS(110), 6, + anon_sym_RPAREN, + anon_sym_COLON_EQ, + anon_sym_end, + anon_sym_SEMI, + anon_sym_DASH_GT, + anon_sym_u2192, + [1222] = 6, + ACTIONS(3), 1, + sym_comment, + ACTIONS(112), 1, + anon_sym_LPAREN, + ACTIONS(114), 1, + anon_sym_COLON, + ACTIONS(116), 1, + anon_sym_COLON_EQ, + STATE(74), 1, sym_ascription, - ACTIONS(3), 2, - sym_comment, - sym_block_comment, - STATE(31), 2, + STATE(39), 2, sym_param_block, aux_sym_labs_repeat1, - [1176] = 6, - ACTIONS(107), 1, - anon_sym_LPAREN, - ACTIONS(109), 1, + [1242] = 3, + ACTIONS(3), 1, + sym_comment, + ACTIONS(120), 1, anon_sym_COLON, - ACTIONS(113), 1, + ACTIONS(118), 5, + anon_sym_LPAREN, + anon_sym_EQ_GT, + anon_sym_u21d2, + anon_sym_COMMA, anon_sym_COLON_EQ, - STATE(65), 1, + [1256] = 2, + ACTIONS(3), 1, + sym_comment, + ACTIONS(122), 6, + anon_sym_RPAREN, + anon_sym_COLON_EQ, + anon_sym_end, + anon_sym_SEMI, + anon_sym_DASH_GT, + anon_sym_u2192, + [1268] = 2, + ACTIONS(3), 1, + sym_comment, + ACTIONS(124), 6, + anon_sym_RPAREN, + anon_sym_COLON_EQ, + anon_sym_end, + anon_sym_SEMI, + anon_sym_DASH_GT, + anon_sym_u2192, + [1280] = 6, + ACTIONS(3), 1, + sym_comment, + ACTIONS(112), 1, + anon_sym_LPAREN, + ACTIONS(114), 1, + anon_sym_COLON, + ACTIONS(126), 1, + anon_sym_COLON_EQ, + STATE(73), 1, sym_ascription, - ACTIONS(3), 2, - sym_comment, - sym_block_comment, - STATE(26), 2, - sym_param_block, - aux_sym_labs_repeat1, - [1197] = 5, - ACTIONS(7), 1, - sym_identifier, - ACTIONS(9), 1, - sym_command, - ACTIONS(115), 1, - ts_builtin_sym_end, - ACTIONS(3), 2, - sym_comment, - sym_block_comment, - STATE(29), 3, - sym_definition, - sym_preprocess, - aux_sym_program_repeat1, - [1216] = 2, - ACTIONS(3), 2, - sym_comment, - sym_block_comment, - ACTIONS(117), 6, - anon_sym_RPAREN, - anon_sym_COLON_EQ, - anon_sym_end, - anon_sym_DASH_GT, - anon_sym_u2192, - anon_sym_SEMI, - [1229] = 3, - ACTIONS(121), 1, - anon_sym_COLON, - ACTIONS(3), 2, - sym_comment, - sym_block_comment, - ACTIONS(119), 5, - anon_sym_LPAREN, - anon_sym_EQ_GT, - anon_sym_u21d2, - anon_sym_COMMA, - anon_sym_COLON_EQ, - [1244] = 2, - ACTIONS(3), 2, - sym_comment, - sym_block_comment, - ACTIONS(123), 6, - anon_sym_RPAREN, - anon_sym_COLON_EQ, - anon_sym_end, - anon_sym_DASH_GT, - anon_sym_u2192, - anon_sym_SEMI, - [1257] = 2, - ACTIONS(3), 2, - sym_comment, - sym_block_comment, - ACTIONS(125), 6, - anon_sym_RPAREN, - anon_sym_COLON_EQ, - anon_sym_end, - anon_sym_DASH_GT, - anon_sym_u2192, - anon_sym_SEMI, - [1270] = 2, - ACTIONS(3), 2, - sym_comment, - sym_block_comment, - ACTIONS(127), 6, - anon_sym_RPAREN, - anon_sym_COLON_EQ, - anon_sym_end, - anon_sym_DASH_GT, - anon_sym_u2192, - anon_sym_SEMI, - [1283] = 2, - ACTIONS(3), 2, - sym_comment, - sym_block_comment, - ACTIONS(129), 6, - anon_sym_RPAREN, - anon_sym_COLON_EQ, - anon_sym_end, - anon_sym_DASH_GT, - anon_sym_u2192, - anon_sym_SEMI, - [1296] = 2, - ACTIONS(3), 2, - sym_comment, - sym_block_comment, - ACTIONS(131), 6, - anon_sym_RPAREN, - anon_sym_COLON_EQ, - anon_sym_end, - anon_sym_DASH_GT, - anon_sym_u2192, - anon_sym_SEMI, - [1309] = 4, - ACTIONS(107), 1, - anon_sym_LPAREN, - ACTIONS(3), 2, - sym_comment, - sym_block_comment, - ACTIONS(133), 2, - anon_sym_EQ_GT, - anon_sym_u21d2, - STATE(26), 2, - sym_param_block, - aux_sym_labs_repeat1, - [1325] = 3, - ACTIONS(3), 2, - sym_comment, - sym_block_comment, - ACTIONS(135), 2, - anon_sym_DASH_GT, - anon_sym_u2192, - ACTIONS(123), 3, - anon_sym_RPAREN, - anon_sym_COLON_EQ, - anon_sym_SEMI, - [1339] = 4, - ACTIONS(107), 1, - anon_sym_LPAREN, - ACTIONS(3), 2, - sym_comment, - sym_block_comment, - ACTIONS(137), 2, - anon_sym_EQ_GT, - anon_sym_u21d2, - STATE(26), 2, - sym_param_block, - aux_sym_labs_repeat1, - [1355] = 4, - ACTIONS(107), 1, - anon_sym_LPAREN, - ACTIONS(139), 1, - anon_sym_COMMA, - ACTIONS(3), 2, - sym_comment, - sym_block_comment, - STATE(26), 2, - sym_param_block, - aux_sym_labs_repeat1, - [1370] = 4, - ACTIONS(141), 1, - anon_sym_LPAREN, - ACTIONS(143), 1, - anon_sym_in, - ACTIONS(3), 2, - sym_comment, - sym_block_comment, - STATE(46), 2, - sym_binding, - aux_sym_let_repeat1, - [1385] = 4, - ACTIONS(107), 1, - anon_sym_LPAREN, - ACTIONS(145), 1, - anon_sym_COLON_EQ, - ACTIONS(3), 2, - sym_comment, - sym_block_comment, - STATE(47), 2, - sym_param_block, - aux_sym_labs_repeat1, - [1400] = 4, - ACTIONS(147), 1, - anon_sym_LPAREN, - ACTIONS(150), 1, - anon_sym_in, - ACTIONS(3), 2, - sym_comment, - sym_block_comment, - STATE(46), 2, - sym_binding, - aux_sym_let_repeat1, - [1415] = 4, - ACTIONS(107), 1, - anon_sym_LPAREN, - ACTIONS(152), 1, - anon_sym_COLON_EQ, - ACTIONS(3), 2, - sym_comment, - sym_block_comment, - STATE(26), 2, - sym_param_block, - aux_sym_labs_repeat1, - [1430] = 4, - ACTIONS(107), 1, - anon_sym_LPAREN, - ACTIONS(154), 1, - anon_sym_COMMA, - ACTIONS(3), 2, - sym_comment, - sym_block_comment, - STATE(26), 2, - sym_param_block, - aux_sym_labs_repeat1, - [1445] = 2, - ACTIONS(3), 2, - sym_comment, - sym_block_comment, - ACTIONS(156), 3, - ts_builtin_sym_end, - sym_identifier, - sym_command, - [1455] = 3, - ACTIONS(107), 1, - anon_sym_LPAREN, - ACTIONS(3), 2, - sym_comment, - sym_block_comment, - STATE(48), 2, - sym_param_block, - aux_sym_labs_repeat1, - [1467] = 3, - ACTIONS(123), 1, - anon_sym_end, - ACTIONS(3), 2, - sym_comment, - sym_block_comment, - ACTIONS(158), 2, - anon_sym_DASH_GT, - anon_sym_u2192, - [1479] = 2, - ACTIONS(3), 2, - sym_comment, - sym_block_comment, - ACTIONS(160), 3, - ts_builtin_sym_end, - sym_identifier, - sym_command, - [1489] = 2, - ACTIONS(3), 2, - sym_comment, - sym_block_comment, - ACTIONS(162), 3, - ts_builtin_sym_end, - sym_identifier, - sym_command, - [1499] = 3, - ACTIONS(107), 1, - anon_sym_LPAREN, - ACTIONS(3), 2, - sym_comment, - sym_block_comment, - STATE(40), 2, - sym_param_block, - aux_sym_labs_repeat1, - [1511] = 4, - ACTIONS(164), 1, - sym_identifier, - ACTIONS(166), 1, - anon_sym_COLON, - STATE(57), 1, - aux_sym_param_block_repeat1, - ACTIONS(3), 2, - sym_comment, - sym_block_comment, - [1525] = 3, - ACTIONS(107), 1, - anon_sym_LPAREN, - ACTIONS(3), 2, - sym_comment, - sym_block_comment, - STATE(43), 2, - sym_param_block, - aux_sym_labs_repeat1, - [1537] = 4, - ACTIONS(168), 1, - sym_identifier, - ACTIONS(171), 1, - anon_sym_COLON, - STATE(57), 1, - aux_sym_param_block_repeat1, - ACTIONS(3), 2, - sym_comment, - sym_block_comment, - [1551] = 2, - ACTIONS(3), 2, - sym_comment, - sym_block_comment, - ACTIONS(173), 3, - ts_builtin_sym_end, - sym_identifier, - sym_command, - [1561] = 3, - ACTIONS(141), 1, - anon_sym_LPAREN, - ACTIONS(3), 2, - sym_comment, - sym_block_comment, - STATE(44), 2, - sym_binding, - aux_sym_let_repeat1, - [1573] = 3, - ACTIONS(107), 1, - anon_sym_LPAREN, - ACTIONS(3), 2, - sym_comment, - sym_block_comment, STATE(42), 2, sym_param_block, aux_sym_labs_repeat1, - [1585] = 2, - ACTIONS(3), 2, + [1300] = 6, + ACTIONS(3), 1, sym_comment, - sym_block_comment, - ACTIONS(175), 2, + ACTIONS(112), 1, anon_sym_LPAREN, - anon_sym_in, - [1594] = 3, - ACTIONS(177), 1, - sym_identifier, - STATE(55), 1, - aux_sym_param_block_repeat1, - ACTIONS(3), 2, - sym_comment, - sym_block_comment, - [1605] = 2, - ACTIONS(3), 2, - sym_comment, - sym_block_comment, - ACTIONS(179), 2, - anon_sym_LPAREN, - anon_sym_in, - [1614] = 2, - ACTIONS(181), 1, - anon_sym_SEMI, - ACTIONS(3), 2, - sym_comment, - sym_block_comment, - [1622] = 2, - ACTIONS(183), 1, + ACTIONS(114), 1, + anon_sym_COLON, + ACTIONS(128), 1, anon_sym_COLON_EQ, - ACTIONS(3), 2, + STATE(87), 1, + sym_ascription, + STATE(26), 2, + sym_param_block, + aux_sym_labs_repeat1, + [1320] = 2, + ACTIONS(3), 1, sym_comment, - sym_block_comment, - [1630] = 2, - ACTIONS(185), 1, + ACTIONS(130), 6, + anon_sym_RPAREN, + anon_sym_COLON_EQ, anon_sym_end, - ACTIONS(3), 2, - sym_comment, - sym_block_comment, - [1638] = 2, - ACTIONS(187), 1, - anon_sym_RPAREN, - ACTIONS(3), 2, - sym_comment, - sym_block_comment, - [1646] = 2, - ACTIONS(189), 1, - anon_sym_RPAREN, - ACTIONS(3), 2, - sym_comment, - sym_block_comment, - [1654] = 2, - ACTIONS(193), 1, - sym_post_command, - ACTIONS(191), 2, - sym_comment, - sym_block_comment, - [1662] = 2, - ACTIONS(195), 1, - anon_sym_COLON_EQ, - ACTIONS(3), 2, - sym_comment, - sym_block_comment, - [1670] = 2, - ACTIONS(197), 1, - sym_identifier, - ACTIONS(3), 2, - sym_comment, - sym_block_comment, - [1678] = 2, - ACTIONS(199), 1, anon_sym_SEMI, - ACTIONS(3), 2, + anon_sym_DASH_GT, + anon_sym_u2192, + [1332] = 2, + ACTIONS(3), 1, sym_comment, - sym_block_comment, - [1686] = 2, - ACTIONS(201), 1, + ACTIONS(132), 6, anon_sym_RPAREN, - ACTIONS(3), 2, + anon_sym_COLON_EQ, + anon_sym_end, + anon_sym_SEMI, + anon_sym_DASH_GT, + anon_sym_u2192, + [1344] = 6, + ACTIONS(3), 1, sym_comment, - sym_block_comment, - [1694] = 2, - ACTIONS(203), 1, + ACTIONS(112), 1, + anon_sym_LPAREN, + ACTIONS(114), 1, + anon_sym_COLON, + ACTIONS(134), 1, + anon_sym_COLON_EQ, + STATE(89), 1, + sym_ascription, + STATE(26), 2, + sym_param_block, + aux_sym_labs_repeat1, + [1364] = 3, + ACTIONS(3), 1, + sym_comment, + ACTIONS(136), 2, + anon_sym_DASH_GT, + anon_sym_u2192, + ACTIONS(130), 3, anon_sym_RPAREN, - ACTIONS(3), 2, + anon_sym_COLON_EQ, + anon_sym_SEMI, + [1377] = 5, + ACTIONS(3), 1, sym_comment, - sym_block_comment, - [1702] = 2, - ACTIONS(205), 1, + ACTIONS(112), 1, + anon_sym_LPAREN, + ACTIONS(138), 1, + anon_sym_COLON, + STATE(80), 1, + sym_ascription, + STATE(46), 2, + sym_param_block, + aux_sym_labs_repeat1, + [1394] = 4, + ACTIONS(3), 1, + sym_comment, + ACTIONS(112), 1, + anon_sym_LPAREN, + ACTIONS(140), 2, + anon_sym_EQ_GT, + anon_sym_u21d2, + STATE(26), 2, + sym_param_block, + aux_sym_labs_repeat1, + [1409] = 5, + ACTIONS(3), 1, + sym_comment, + ACTIONS(112), 1, + anon_sym_LPAREN, + ACTIONS(138), 1, + anon_sym_COLON, + STATE(90), 1, + sym_ascription, + STATE(26), 2, + sym_param_block, + aux_sym_labs_repeat1, + [1426] = 4, + ACTIONS(3), 1, + sym_comment, + ACTIONS(112), 1, + anon_sym_LPAREN, + ACTIONS(142), 2, + anon_sym_EQ_GT, + anon_sym_u21d2, + STATE(26), 2, + sym_param_block, + aux_sym_labs_repeat1, + [1441] = 2, + ACTIONS(3), 1, + sym_comment, + ACTIONS(144), 4, ts_builtin_sym_end, - ACTIONS(3), 2, + anon_sym_axiom, + anon_sym_def, + sym_command, + [1451] = 2, + ACTIONS(3), 1, sym_comment, - sym_block_comment, - [1710] = 2, - ACTIONS(207), 1, - anon_sym_SEMI, - ACTIONS(3), 2, + ACTIONS(146), 4, + ts_builtin_sym_end, + anon_sym_axiom, + anon_sym_def, + sym_command, + [1461] = 2, + ACTIONS(3), 1, sym_comment, - sym_block_comment, - [1718] = 2, - ACTIONS(209), 1, - anon_sym_RPAREN, - ACTIONS(3), 2, + ACTIONS(148), 4, + ts_builtin_sym_end, + anon_sym_axiom, + anon_sym_def, + sym_command, + [1471] = 4, + ACTIONS(3), 1, sym_comment, - sym_block_comment, - [1726] = 2, - ACTIONS(113), 1, + ACTIONS(150), 1, + anon_sym_LPAREN, + ACTIONS(153), 1, + anon_sym_in, + STATE(51), 2, + sym_binding, + aux_sym_let_repeat1, + [1485] = 2, + ACTIONS(3), 1, + sym_comment, + ACTIONS(155), 4, + ts_builtin_sym_end, + anon_sym_axiom, + anon_sym_def, + sym_command, + [1495] = 2, + ACTIONS(3), 1, + sym_comment, + ACTIONS(157), 4, + ts_builtin_sym_end, + anon_sym_axiom, + anon_sym_def, + sym_command, + [1505] = 4, + ACTIONS(3), 1, + sym_comment, + ACTIONS(159), 1, + anon_sym_LPAREN, + ACTIONS(161), 1, + anon_sym_in, + STATE(51), 2, + sym_binding, + aux_sym_let_repeat1, + [1519] = 4, + ACTIONS(3), 1, + sym_comment, + ACTIONS(112), 1, + anon_sym_LPAREN, + ACTIONS(163), 1, + anon_sym_COMMA, + STATE(26), 2, + sym_param_block, + aux_sym_labs_repeat1, + [1533] = 2, + ACTIONS(3), 1, + sym_comment, + ACTIONS(165), 4, + ts_builtin_sym_end, + anon_sym_axiom, + anon_sym_def, + sym_command, + [1543] = 4, + ACTIONS(3), 1, + sym_comment, + ACTIONS(112), 1, + anon_sym_LPAREN, + ACTIONS(167), 1, + anon_sym_COMMA, + STATE(26), 2, + sym_param_block, + aux_sym_labs_repeat1, + [1557] = 3, + ACTIONS(3), 1, + sym_comment, + ACTIONS(112), 1, + anon_sym_LPAREN, + STATE(45), 2, + sym_param_block, + aux_sym_labs_repeat1, + [1568] = 3, + ACTIONS(3), 1, + sym_comment, + ACTIONS(159), 1, + anon_sym_LPAREN, + STATE(54), 2, + sym_binding, + aux_sym_let_repeat1, + [1579] = 4, + ACTIONS(3), 1, + sym_comment, + ACTIONS(169), 1, + sym_identifier, + ACTIONS(172), 1, + anon_sym_COLON, + STATE(60), 1, + aux_sym_param_block_repeat1, + [1592] = 3, + ACTIONS(3), 1, + sym_comment, + ACTIONS(130), 1, + anon_sym_end, + ACTIONS(174), 2, + anon_sym_DASH_GT, + anon_sym_u2192, + [1603] = 4, + ACTIONS(3), 1, + sym_comment, + ACTIONS(176), 1, + sym_identifier, + ACTIONS(178), 1, + anon_sym_COLON, + STATE(60), 1, + aux_sym_param_block_repeat1, + [1616] = 3, + ACTIONS(3), 1, + sym_comment, + ACTIONS(112), 1, + anon_sym_LPAREN, + STATE(55), 2, + sym_param_block, + aux_sym_labs_repeat1, + [1627] = 3, + ACTIONS(3), 1, + sym_comment, + ACTIONS(112), 1, + anon_sym_LPAREN, + STATE(47), 2, + sym_param_block, + aux_sym_labs_repeat1, + [1638] = 3, + ACTIONS(3), 1, + sym_comment, + ACTIONS(112), 1, + anon_sym_LPAREN, + STATE(57), 2, + sym_param_block, + aux_sym_labs_repeat1, + [1649] = 2, + ACTIONS(3), 1, + sym_comment, + ACTIONS(180), 2, + anon_sym_LPAREN, + anon_sym_in, + [1657] = 2, + ACTIONS(3), 1, + sym_comment, + ACTIONS(182), 2, + anon_sym_LPAREN, + anon_sym_in, + [1665] = 2, + ACTIONS(3), 1, + sym_comment, + ACTIONS(184), 2, anon_sym_COLON_EQ, - ACTIONS(3), 2, + anon_sym_SEMI, + [1673] = 3, + ACTIONS(3), 1, sym_comment, - sym_block_comment, + ACTIONS(186), 1, + sym_identifier, + STATE(62), 1, + aux_sym_param_block_repeat1, + [1683] = 2, + ACTIONS(3), 1, + sym_comment, + ACTIONS(188), 2, + anon_sym_LPAREN, + anon_sym_in, + [1691] = 2, + ACTIONS(3), 1, + sym_comment, + ACTIONS(190), 1, + ts_builtin_sym_end, + [1698] = 2, + ACTIONS(3), 1, + sym_comment, + ACTIONS(192), 1, + anon_sym_RPAREN, + [1705] = 2, + ACTIONS(3), 1, + sym_comment, + ACTIONS(134), 1, + anon_sym_COLON_EQ, + [1712] = 2, + ACTIONS(3), 1, + sym_comment, + ACTIONS(128), 1, + anon_sym_COLON_EQ, + [1719] = 2, + ACTIONS(3), 1, + sym_comment, + ACTIONS(194), 1, + anon_sym_RPAREN, + [1726] = 2, + ACTIONS(3), 1, + sym_comment, + ACTIONS(196), 1, + anon_sym_RPAREN, + [1733] = 2, + ACTIONS(3), 1, + sym_comment, + ACTIONS(198), 1, + anon_sym_end, + [1740] = 2, + ACTIONS(3), 1, + sym_comment, + ACTIONS(200), 1, + sym_identifier, + [1747] = 2, + ACTIONS(3), 1, + sym_comment, + ACTIONS(202), 1, + anon_sym_RPAREN, + [1754] = 2, + ACTIONS(3), 1, + sym_comment, + ACTIONS(204), 1, + anon_sym_SEMI, + [1761] = 2, + ACTIONS(3), 1, + sym_comment, + ACTIONS(206), 1, + anon_sym_RPAREN, + [1768] = 2, + ACTIONS(3), 1, + sym_comment, + ACTIONS(208), 1, + sym_identifier, + [1775] = 2, + ACTIONS(3), 1, + sym_comment, + ACTIONS(210), 1, + anon_sym_SEMI, + [1782] = 2, + ACTIONS(212), 1, + sym_comment, + ACTIONS(214), 1, + sym_post_command, + [1789] = 2, + ACTIONS(3), 1, + sym_comment, + ACTIONS(216), 1, + sym_identifier, + [1796] = 2, + ACTIONS(3), 1, + sym_comment, + ACTIONS(218), 1, + anon_sym_RPAREN, + [1803] = 2, + ACTIONS(3), 1, + sym_comment, + ACTIONS(220), 1, + anon_sym_COLON_EQ, + [1810] = 2, + ACTIONS(3), 1, + sym_comment, + ACTIONS(222), 1, + anon_sym_SEMI, + [1817] = 2, + ACTIONS(3), 1, + sym_comment, + ACTIONS(224), 1, + anon_sym_COLON_EQ, + [1824] = 2, + ACTIONS(3), 1, + sym_comment, + ACTIONS(226), 1, + anon_sym_SEMI, + [1831] = 2, + ACTIONS(3), 1, + sym_comment, + ACTIONS(228), 1, + anon_sym_SEMI, }; static const uint32_t ts_small_parse_table_map[] = { [SMALL_STATE(2)] = 0, - [SMALL_STATE(3)] = 58, - [SMALL_STATE(4)] = 116, - [SMALL_STATE(5)] = 174, - [SMALL_STATE(6)] = 229, - [SMALL_STATE(7)] = 284, - [SMALL_STATE(8)] = 339, - [SMALL_STATE(9)] = 394, - [SMALL_STATE(10)] = 449, - [SMALL_STATE(11)] = 504, - [SMALL_STATE(12)] = 559, - [SMALL_STATE(13)] = 614, - [SMALL_STATE(14)] = 669, - [SMALL_STATE(15)] = 724, - [SMALL_STATE(16)] = 779, - [SMALL_STATE(17)] = 834, - [SMALL_STATE(18)] = 889, - [SMALL_STATE(19)] = 919, - [SMALL_STATE(20)] = 949, - [SMALL_STATE(21)] = 981, - [SMALL_STATE(22)] = 1013, - [SMALL_STATE(23)] = 1030, - [SMALL_STATE(24)] = 1047, - [SMALL_STATE(25)] = 1064, - [SMALL_STATE(26)] = 1081, - [SMALL_STATE(27)] = 1102, - [SMALL_STATE(28)] = 1119, - [SMALL_STATE(29)] = 1136, - [SMALL_STATE(30)] = 1155, - [SMALL_STATE(31)] = 1176, - [SMALL_STATE(32)] = 1197, - [SMALL_STATE(33)] = 1216, - [SMALL_STATE(34)] = 1229, - [SMALL_STATE(35)] = 1244, - [SMALL_STATE(36)] = 1257, - [SMALL_STATE(37)] = 1270, - [SMALL_STATE(38)] = 1283, - [SMALL_STATE(39)] = 1296, - [SMALL_STATE(40)] = 1309, - [SMALL_STATE(41)] = 1325, - [SMALL_STATE(42)] = 1339, - [SMALL_STATE(43)] = 1355, - [SMALL_STATE(44)] = 1370, - [SMALL_STATE(45)] = 1385, - [SMALL_STATE(46)] = 1400, - [SMALL_STATE(47)] = 1415, - [SMALL_STATE(48)] = 1430, - [SMALL_STATE(49)] = 1445, - [SMALL_STATE(50)] = 1455, - [SMALL_STATE(51)] = 1467, - [SMALL_STATE(52)] = 1479, - [SMALL_STATE(53)] = 1489, - [SMALL_STATE(54)] = 1499, - [SMALL_STATE(55)] = 1511, - [SMALL_STATE(56)] = 1525, - [SMALL_STATE(57)] = 1537, - [SMALL_STATE(58)] = 1551, - [SMALL_STATE(59)] = 1561, - [SMALL_STATE(60)] = 1573, - [SMALL_STATE(61)] = 1585, - [SMALL_STATE(62)] = 1594, - [SMALL_STATE(63)] = 1605, - [SMALL_STATE(64)] = 1614, - [SMALL_STATE(65)] = 1622, - [SMALL_STATE(66)] = 1630, - [SMALL_STATE(67)] = 1638, - [SMALL_STATE(68)] = 1646, - [SMALL_STATE(69)] = 1654, - [SMALL_STATE(70)] = 1662, - [SMALL_STATE(71)] = 1670, - [SMALL_STATE(72)] = 1678, - [SMALL_STATE(73)] = 1686, - [SMALL_STATE(74)] = 1694, - [SMALL_STATE(75)] = 1702, - [SMALL_STATE(76)] = 1710, - [SMALL_STATE(77)] = 1718, - [SMALL_STATE(78)] = 1726, + [SMALL_STATE(3)] = 54, + [SMALL_STATE(4)] = 108, + [SMALL_STATE(5)] = 162, + [SMALL_STATE(6)] = 216, + [SMALL_STATE(7)] = 270, + [SMALL_STATE(8)] = 324, + [SMALL_STATE(9)] = 378, + [SMALL_STATE(10)] = 432, + [SMALL_STATE(11)] = 486, + [SMALL_STATE(12)] = 540, + [SMALL_STATE(13)] = 594, + [SMALL_STATE(14)] = 648, + [SMALL_STATE(15)] = 702, + [SMALL_STATE(16)] = 756, + [SMALL_STATE(17)] = 810, + [SMALL_STATE(18)] = 864, + [SMALL_STATE(19)] = 918, + [SMALL_STATE(20)] = 947, + [SMALL_STATE(21)] = 976, + [SMALL_STATE(22)] = 1007, + [SMALL_STATE(23)] = 1038, + [SMALL_STATE(24)] = 1054, + [SMALL_STATE(25)] = 1070, + [SMALL_STATE(26)] = 1086, + [SMALL_STATE(27)] = 1106, + [SMALL_STATE(28)] = 1128, + [SMALL_STATE(29)] = 1150, + [SMALL_STATE(30)] = 1166, + [SMALL_STATE(31)] = 1182, + [SMALL_STATE(32)] = 1198, + [SMALL_STATE(33)] = 1210, + [SMALL_STATE(34)] = 1222, + [SMALL_STATE(35)] = 1242, + [SMALL_STATE(36)] = 1256, + [SMALL_STATE(37)] = 1268, + [SMALL_STATE(38)] = 1280, + [SMALL_STATE(39)] = 1300, + [SMALL_STATE(40)] = 1320, + [SMALL_STATE(41)] = 1332, + [SMALL_STATE(42)] = 1344, + [SMALL_STATE(43)] = 1364, + [SMALL_STATE(44)] = 1377, + [SMALL_STATE(45)] = 1394, + [SMALL_STATE(46)] = 1409, + [SMALL_STATE(47)] = 1426, + [SMALL_STATE(48)] = 1441, + [SMALL_STATE(49)] = 1451, + [SMALL_STATE(50)] = 1461, + [SMALL_STATE(51)] = 1471, + [SMALL_STATE(52)] = 1485, + [SMALL_STATE(53)] = 1495, + [SMALL_STATE(54)] = 1505, + [SMALL_STATE(55)] = 1519, + [SMALL_STATE(56)] = 1533, + [SMALL_STATE(57)] = 1543, + [SMALL_STATE(58)] = 1557, + [SMALL_STATE(59)] = 1568, + [SMALL_STATE(60)] = 1579, + [SMALL_STATE(61)] = 1592, + [SMALL_STATE(62)] = 1603, + [SMALL_STATE(63)] = 1616, + [SMALL_STATE(64)] = 1627, + [SMALL_STATE(65)] = 1638, + [SMALL_STATE(66)] = 1649, + [SMALL_STATE(67)] = 1657, + [SMALL_STATE(68)] = 1665, + [SMALL_STATE(69)] = 1673, + [SMALL_STATE(70)] = 1683, + [SMALL_STATE(71)] = 1691, + [SMALL_STATE(72)] = 1698, + [SMALL_STATE(73)] = 1705, + [SMALL_STATE(74)] = 1712, + [SMALL_STATE(75)] = 1719, + [SMALL_STATE(76)] = 1726, + [SMALL_STATE(77)] = 1733, + [SMALL_STATE(78)] = 1740, + [SMALL_STATE(79)] = 1747, + [SMALL_STATE(80)] = 1754, + [SMALL_STATE(81)] = 1761, + [SMALL_STATE(82)] = 1768, + [SMALL_STATE(83)] = 1775, + [SMALL_STATE(84)] = 1782, + [SMALL_STATE(85)] = 1789, + [SMALL_STATE(86)] = 1796, + [SMALL_STATE(87)] = 1803, + [SMALL_STATE(88)] = 1810, + [SMALL_STATE(89)] = 1817, + [SMALL_STATE(90)] = 1824, + [SMALL_STATE(91)] = 1831, }; static const TSParseActionEntry ts_parse_actions[] = { @@ -2465,102 +2461,111 @@ static const TSParseActionEntry ts_parse_actions[] = { [1] = {.entry = {.count = 1, .reusable = false}}, RECOVER(), [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(30), - [9] = {.entry = {.count = 1, .reusable = true}}, SHIFT(69), - [11] = {.entry = {.count = 1, .reusable = false}}, SHIFT(23), - [13] = {.entry = {.count = 1, .reusable = true}}, SHIFT(8), - [15] = {.entry = {.count = 1, .reusable = true}}, SHIFT(23), - [17] = {.entry = {.count = 1, .reusable = true}}, SHIFT(22), - [19] = {.entry = {.count = 1, .reusable = true}}, SHIFT(54), - [21] = {.entry = {.count = 1, .reusable = false}}, SHIFT(54), - [23] = {.entry = {.count = 1, .reusable = true}}, SHIFT(56), - [25] = {.entry = {.count = 1, .reusable = false}}, SHIFT(56), - [27] = {.entry = {.count = 1, .reusable = false}}, SHIFT(59), - [29] = {.entry = {.count = 1, .reusable = false}}, SHIFT(76), - [31] = {.entry = {.count = 1, .reusable = false}}, SHIFT(72), - [33] = {.entry = {.count = 1, .reusable = false}}, SHIFT(64), - [35] = {.entry = {.count = 1, .reusable = false}}, SHIFT(27), - [37] = {.entry = {.count = 1, .reusable = true}}, SHIFT(17), - [39] = {.entry = {.count = 1, .reusable = true}}, SHIFT(27), - [41] = {.entry = {.count = 1, .reusable = true}}, SHIFT(28), - [43] = {.entry = {.count = 1, .reusable = true}}, SHIFT(60), - [45] = {.entry = {.count = 1, .reusable = false}}, SHIFT(60), - [47] = {.entry = {.count = 1, .reusable = true}}, SHIFT(50), - [49] = {.entry = {.count = 1, .reusable = false}}, SHIFT(50), - [51] = {.entry = {.count = 2, .reusable = true}}, REDUCE(aux_sym_app_repeat1, 2, 0, 0), SHIFT_REPEAT(23), - [54] = {.entry = {.count = 2, .reusable = true}}, REDUCE(aux_sym_app_repeat1, 2, 0, 0), SHIFT_REPEAT(8), - [57] = {.entry = {.count = 1, .reusable = true}}, REDUCE(aux_sym_app_repeat1, 2, 0, 0), - [59] = {.entry = {.count = 2, .reusable = true}}, REDUCE(aux_sym_app_repeat1, 2, 0, 0), SHIFT_REPEAT(22), - [62] = {.entry = {.count = 1, .reusable = true}}, REDUCE(sym_app, 1, 0, 0), - [64] = {.entry = {.count = 2, .reusable = false}}, REDUCE(aux_sym_app_repeat1, 2, 0, 0), SHIFT_REPEAT(27), - [67] = {.entry = {.count = 2, .reusable = true}}, REDUCE(aux_sym_app_repeat1, 2, 0, 0), SHIFT_REPEAT(17), - [70] = {.entry = {.count = 2, .reusable = true}}, REDUCE(aux_sym_app_repeat1, 2, 0, 0), SHIFT_REPEAT(27), - [73] = {.entry = {.count = 2, .reusable = true}}, REDUCE(aux_sym_app_repeat1, 2, 0, 0), SHIFT_REPEAT(28), - [76] = {.entry = {.count = 1, .reusable = false}}, REDUCE(aux_sym_app_repeat1, 2, 0, 0), - [78] = {.entry = {.count = 1, .reusable = false}}, REDUCE(sym_app, 1, 0, 0), - [80] = {.entry = {.count = 1, .reusable = true}}, REDUCE(sym_square, 1, 0, 0), - [82] = {.entry = {.count = 1, .reusable = true}}, REDUCE(sym_term, 1, 0, 0), - [84] = {.entry = {.count = 1, .reusable = true}}, REDUCE(sym_term, 3, 0, 0), - [86] = {.entry = {.count = 1, .reusable = false}}, REDUCE(sym_term, 3, 0, 0), - [88] = {.entry = {.count = 2, .reusable = true}}, REDUCE(aux_sym_labs_repeat1, 2, 0, 0), SHIFT_REPEAT(62), - [91] = {.entry = {.count = 1, .reusable = false}}, REDUCE(aux_sym_labs_repeat1, 2, 0, 0), - [93] = {.entry = {.count = 1, .reusable = true}}, REDUCE(aux_sym_labs_repeat1, 2, 0, 0), - [95] = {.entry = {.count = 1, .reusable = false}}, REDUCE(sym_term, 1, 0, 0), - [97] = {.entry = {.count = 1, .reusable = false}}, REDUCE(sym_square, 1, 0, 0), - [99] = {.entry = {.count = 1, .reusable = true}}, REDUCE(aux_sym_program_repeat1, 2, 0, 0), - [101] = {.entry = {.count = 2, .reusable = true}}, REDUCE(aux_sym_program_repeat1, 2, 0, 0), SHIFT_REPEAT(30), - [104] = {.entry = {.count = 2, .reusable = true}}, REDUCE(aux_sym_program_repeat1, 2, 0, 0), SHIFT_REPEAT(69), - [107] = {.entry = {.count = 1, .reusable = true}}, SHIFT(62), - [109] = {.entry = {.count = 1, .reusable = false}}, SHIFT(6), - [111] = {.entry = {.count = 1, .reusable = true}}, SHIFT(2), - [113] = {.entry = {.count = 1, .reusable = true}}, SHIFT(3), - [115] = {.entry = {.count = 1, .reusable = true}}, REDUCE(sym_program, 1, 0, 0), - [117] = {.entry = {.count = 1, .reusable = true}}, REDUCE(sym_arrow, 3, 0, 0), - [119] = {.entry = {.count = 1, .reusable = true}}, REDUCE(sym_param_block, 5, 0, 3), - [121] = {.entry = {.count = 1, .reusable = false}}, REDUCE(sym_param_block, 5, 0, 3), - [123] = {.entry = {.count = 1, .reusable = true}}, REDUCE(sym_expr, 1, 0, 0), - [125] = {.entry = {.count = 1, .reusable = true}}, REDUCE(sym_labs, 4, 0, 0), - [127] = {.entry = {.count = 1, .reusable = true}}, REDUCE(sym_let, 5, 0, 0), - [129] = {.entry = {.count = 1, .reusable = true}}, REDUCE(sym_pabs, 4, 0, 0), - [131] = {.entry = {.count = 1, .reusable = true}}, REDUCE(sym_app_term, 1, 0, 0), - [133] = {.entry = {.count = 1, .reusable = true}}, SHIFT(5), - [135] = {.entry = {.count = 1, .reusable = true}}, SHIFT(9), - [137] = {.entry = {.count = 1, .reusable = true}}, SHIFT(16), - [139] = {.entry = {.count = 1, .reusable = true}}, SHIFT(10), - [141] = {.entry = {.count = 1, .reusable = true}}, SHIFT(71), - [143] = {.entry = {.count = 1, .reusable = true}}, SHIFT(11), - [145] = {.entry = {.count = 1, .reusable = true}}, SHIFT(12), - [147] = {.entry = {.count = 2, .reusable = true}}, REDUCE(aux_sym_let_repeat1, 2, 0, 0), SHIFT_REPEAT(71), - [150] = {.entry = {.count = 1, .reusable = true}}, REDUCE(aux_sym_let_repeat1, 2, 0, 0), - [152] = {.entry = {.count = 1, .reusable = true}}, SHIFT(13), - [154] = {.entry = {.count = 1, .reusable = true}}, SHIFT(14), - [156] = {.entry = {.count = 1, .reusable = true}}, REDUCE(sym_definition, 5, 0, 2), - [158] = {.entry = {.count = 1, .reusable = true}}, SHIFT(15), - [160] = {.entry = {.count = 1, .reusable = true}}, REDUCE(sym_preprocess, 2, 0, 0), - [162] = {.entry = {.count = 1, .reusable = true}}, REDUCE(sym_definition, 4, 0, 2), - [164] = {.entry = {.count = 1, .reusable = true}}, SHIFT(57), - [166] = {.entry = {.count = 1, .reusable = true}}, SHIFT(7), - [168] = {.entry = {.count = 2, .reusable = true}}, REDUCE(aux_sym_param_block_repeat1, 2, 0, 0), SHIFT_REPEAT(57), - [171] = {.entry = {.count = 1, .reusable = true}}, REDUCE(aux_sym_param_block_repeat1, 2, 0, 0), - [173] = {.entry = {.count = 1, .reusable = true}}, REDUCE(sym_definition, 6, 0, 2), - [175] = {.entry = {.count = 1, .reusable = true}}, REDUCE(sym_binding, 6, 0, 0), - [177] = {.entry = {.count = 1, .reusable = true}}, SHIFT(55), - [179] = {.entry = {.count = 1, .reusable = true}}, REDUCE(sym_binding, 5, 0, 0), - [181] = {.entry = {.count = 1, .reusable = true}}, SHIFT(58), - [183] = {.entry = {.count = 1, .reusable = true}}, SHIFT(4), - [185] = {.entry = {.count = 1, .reusable = true}}, SHIFT(37), - [187] = {.entry = {.count = 1, .reusable = true}}, SHIFT(24), - [189] = {.entry = {.count = 1, .reusable = true}}, SHIFT(63), - [191] = {.entry = {.count = 1, .reusable = false}}, SHIFT_EXTRA(), - [193] = {.entry = {.count = 1, .reusable = false}}, SHIFT(52), - [195] = {.entry = {.count = 1, .reusable = true}}, REDUCE(sym_ascription, 2, 0, 1), - [197] = {.entry = {.count = 1, .reusable = true}}, SHIFT(45), - [199] = {.entry = {.count = 1, .reusable = true}}, SHIFT(49), - [201] = {.entry = {.count = 1, .reusable = true}}, SHIFT(25), - [203] = {.entry = {.count = 1, .reusable = true}}, SHIFT(61), - [205] = {.entry = {.count = 1, .reusable = true}}, ACCEPT_INPUT(), - [207] = {.entry = {.count = 1, .reusable = true}}, SHIFT(53), - [209] = {.entry = {.count = 1, .reusable = true}}, SHIFT(34), + [7] = {.entry = {.count = 1, .reusable = true}}, SHIFT(78), + [9] = {.entry = {.count = 1, .reusable = true}}, SHIFT(85), + [11] = {.entry = {.count = 1, .reusable = true}}, SHIFT(84), + [13] = {.entry = {.count = 1, .reusable = false}}, SHIFT(24), + [15] = {.entry = {.count = 1, .reusable = true}}, SHIFT(4), + [17] = {.entry = {.count = 1, .reusable = true}}, SHIFT(24), + [19] = {.entry = {.count = 1, .reusable = true}}, SHIFT(23), + [21] = {.entry = {.count = 1, .reusable = true}}, SHIFT(58), + [23] = {.entry = {.count = 1, .reusable = false}}, SHIFT(58), + [25] = {.entry = {.count = 1, .reusable = true}}, SHIFT(63), + [27] = {.entry = {.count = 1, .reusable = false}}, SHIFT(63), + [29] = {.entry = {.count = 1, .reusable = false}}, SHIFT(59), + [31] = {.entry = {.count = 1, .reusable = false}}, SHIFT(29), + [33] = {.entry = {.count = 1, .reusable = true}}, SHIFT(18), + [35] = {.entry = {.count = 1, .reusable = true}}, SHIFT(29), + [37] = {.entry = {.count = 1, .reusable = true}}, SHIFT(30), + [39] = {.entry = {.count = 1, .reusable = true}}, SHIFT(64), + [41] = {.entry = {.count = 1, .reusable = false}}, SHIFT(64), + [43] = {.entry = {.count = 1, .reusable = true}}, SHIFT(65), + [45] = {.entry = {.count = 1, .reusable = false}}, SHIFT(65), + [47] = {.entry = {.count = 1, .reusable = true}}, REDUCE(sym_app, 1, 0, 0), + [49] = {.entry = {.count = 2, .reusable = true}}, REDUCE(aux_sym_app_repeat1, 2, 0, 0), SHIFT_REPEAT(24), + [52] = {.entry = {.count = 2, .reusable = true}}, REDUCE(aux_sym_app_repeat1, 2, 0, 0), SHIFT_REPEAT(4), + [55] = {.entry = {.count = 1, .reusable = true}}, REDUCE(aux_sym_app_repeat1, 2, 0, 0), + [57] = {.entry = {.count = 2, .reusable = true}}, REDUCE(aux_sym_app_repeat1, 2, 0, 0), SHIFT_REPEAT(23), + [60] = {.entry = {.count = 2, .reusable = false}}, REDUCE(aux_sym_app_repeat1, 2, 0, 0), SHIFT_REPEAT(29), + [63] = {.entry = {.count = 2, .reusable = true}}, REDUCE(aux_sym_app_repeat1, 2, 0, 0), SHIFT_REPEAT(18), + [66] = {.entry = {.count = 2, .reusable = true}}, REDUCE(aux_sym_app_repeat1, 2, 0, 0), SHIFT_REPEAT(29), + [69] = {.entry = {.count = 2, .reusable = true}}, REDUCE(aux_sym_app_repeat1, 2, 0, 0), SHIFT_REPEAT(30), + [72] = {.entry = {.count = 1, .reusable = false}}, REDUCE(aux_sym_app_repeat1, 2, 0, 0), + [74] = {.entry = {.count = 1, .reusable = false}}, REDUCE(sym_app, 1, 0, 0), + [76] = {.entry = {.count = 1, .reusable = true}}, REDUCE(sym_square, 1, 0, 0), + [78] = {.entry = {.count = 1, .reusable = true}}, REDUCE(sym_term, 1, 0, 0), + [80] = {.entry = {.count = 1, .reusable = true}}, REDUCE(sym_term, 3, 0, 0), + [82] = {.entry = {.count = 2, .reusable = true}}, REDUCE(aux_sym_labs_repeat1, 2, 0, 0), SHIFT_REPEAT(69), + [85] = {.entry = {.count = 1, .reusable = false}}, REDUCE(aux_sym_labs_repeat1, 2, 0, 0), + [87] = {.entry = {.count = 1, .reusable = true}}, REDUCE(aux_sym_labs_repeat1, 2, 0, 0), + [89] = {.entry = {.count = 1, .reusable = true}}, REDUCE(sym_program, 1, 0, 0), + [91] = {.entry = {.count = 1, .reusable = true}}, REDUCE(aux_sym_program_repeat1, 2, 0, 0), + [93] = {.entry = {.count = 2, .reusable = true}}, REDUCE(aux_sym_program_repeat1, 2, 0, 0), SHIFT_REPEAT(78), + [96] = {.entry = {.count = 2, .reusable = true}}, REDUCE(aux_sym_program_repeat1, 2, 0, 0), SHIFT_REPEAT(85), + [99] = {.entry = {.count = 2, .reusable = true}}, REDUCE(aux_sym_program_repeat1, 2, 0, 0), SHIFT_REPEAT(84), + [102] = {.entry = {.count = 1, .reusable = false}}, REDUCE(sym_term, 1, 0, 0), + [104] = {.entry = {.count = 1, .reusable = false}}, REDUCE(sym_square, 1, 0, 0), + [106] = {.entry = {.count = 1, .reusable = false}}, REDUCE(sym_term, 3, 0, 0), + [108] = {.entry = {.count = 1, .reusable = true}}, REDUCE(sym_app_term, 1, 0, 0), + [110] = {.entry = {.count = 1, .reusable = true}}, REDUCE(sym_arrow, 3, 0, 0), + [112] = {.entry = {.count = 1, .reusable = true}}, SHIFT(69), + [114] = {.entry = {.count = 1, .reusable = false}}, SHIFT(2), + [116] = {.entry = {.count = 1, .reusable = true}}, SHIFT(11), + [118] = {.entry = {.count = 1, .reusable = true}}, REDUCE(sym_param_block, 5, 0, 3), + [120] = {.entry = {.count = 1, .reusable = false}}, REDUCE(sym_param_block, 5, 0, 3), + [122] = {.entry = {.count = 1, .reusable = true}}, REDUCE(sym_labs, 4, 0, 0), + [124] = {.entry = {.count = 1, .reusable = true}}, REDUCE(sym_pabs, 4, 0, 0), + [126] = {.entry = {.count = 1, .reusable = true}}, SHIFT(3), + [128] = {.entry = {.count = 1, .reusable = true}}, SHIFT(12), + [130] = {.entry = {.count = 1, .reusable = true}}, REDUCE(sym_expr, 1, 0, 0), + [132] = {.entry = {.count = 1, .reusable = true}}, REDUCE(sym_let, 5, 0, 0), + [134] = {.entry = {.count = 1, .reusable = true}}, SHIFT(5), + [136] = {.entry = {.count = 1, .reusable = true}}, SHIFT(6), + [138] = {.entry = {.count = 1, .reusable = true}}, SHIFT(2), + [140] = {.entry = {.count = 1, .reusable = true}}, SHIFT(9), + [142] = {.entry = {.count = 1, .reusable = true}}, SHIFT(16), + [144] = {.entry = {.count = 1, .reusable = true}}, REDUCE(sym_preprocess, 2, 0, 0), + [146] = {.entry = {.count = 1, .reusable = true}}, REDUCE(sym_definition, 5, 0, 2), + [148] = {.entry = {.count = 1, .reusable = true}}, REDUCE(sym_axiom, 5, 0, 2), + [150] = {.entry = {.count = 2, .reusable = true}}, REDUCE(aux_sym_let_repeat1, 2, 0, 0), SHIFT_REPEAT(82), + [153] = {.entry = {.count = 1, .reusable = true}}, REDUCE(aux_sym_let_repeat1, 2, 0, 0), + [155] = {.entry = {.count = 1, .reusable = true}}, REDUCE(sym_axiom, 4, 0, 2), + [157] = {.entry = {.count = 1, .reusable = true}}, REDUCE(sym_definition, 6, 0, 2), + [159] = {.entry = {.count = 1, .reusable = true}}, SHIFT(82), + [161] = {.entry = {.count = 1, .reusable = true}}, SHIFT(10), + [163] = {.entry = {.count = 1, .reusable = true}}, SHIFT(15), + [165] = {.entry = {.count = 1, .reusable = true}}, REDUCE(sym_definition, 7, 0, 2), + [167] = {.entry = {.count = 1, .reusable = true}}, SHIFT(17), + [169] = {.entry = {.count = 2, .reusable = true}}, REDUCE(aux_sym_param_block_repeat1, 2, 0, 0), SHIFT_REPEAT(60), + [172] = {.entry = {.count = 1, .reusable = true}}, REDUCE(aux_sym_param_block_repeat1, 2, 0, 0), + [174] = {.entry = {.count = 1, .reusable = true}}, SHIFT(14), + [176] = {.entry = {.count = 1, .reusable = true}}, SHIFT(60), + [178] = {.entry = {.count = 1, .reusable = true}}, SHIFT(7), + [180] = {.entry = {.count = 1, .reusable = true}}, REDUCE(sym_binding, 5, 0, 0), + [182] = {.entry = {.count = 1, .reusable = true}}, REDUCE(sym_binding, 6, 0, 0), + [184] = {.entry = {.count = 1, .reusable = true}}, REDUCE(sym_ascription, 2, 0, 1), + [186] = {.entry = {.count = 1, .reusable = true}}, SHIFT(62), + [188] = {.entry = {.count = 1, .reusable = true}}, REDUCE(sym_binding, 7, 0, 0), + [190] = {.entry = {.count = 1, .reusable = true}}, ACCEPT_INPUT(), + [192] = {.entry = {.count = 1, .reusable = true}}, SHIFT(67), + [194] = {.entry = {.count = 1, .reusable = true}}, SHIFT(70), + [196] = {.entry = {.count = 1, .reusable = true}}, SHIFT(25), + [198] = {.entry = {.count = 1, .reusable = true}}, SHIFT(41), + [200] = {.entry = {.count = 1, .reusable = true}}, SHIFT(44), + [202] = {.entry = {.count = 1, .reusable = true}}, SHIFT(35), + [204] = {.entry = {.count = 1, .reusable = true}}, SHIFT(52), + [206] = {.entry = {.count = 1, .reusable = true}}, SHIFT(66), + [208] = {.entry = {.count = 1, .reusable = true}}, SHIFT(34), + [210] = {.entry = {.count = 1, .reusable = true}}, SHIFT(49), + [212] = {.entry = {.count = 1, .reusable = false}}, SHIFT_EXTRA(), + [214] = {.entry = {.count = 1, .reusable = false}}, SHIFT(48), + [216] = {.entry = {.count = 1, .reusable = true}}, SHIFT(38), + [218] = {.entry = {.count = 1, .reusable = true}}, SHIFT(31), + [220] = {.entry = {.count = 1, .reusable = true}}, SHIFT(13), + [222] = {.entry = {.count = 1, .reusable = true}}, SHIFT(56), + [224] = {.entry = {.count = 1, .reusable = true}}, SHIFT(8), + [226] = {.entry = {.count = 1, .reusable = true}}, SHIFT(50), + [228] = {.entry = {.count = 1, .reusable = true}}, SHIFT(53), }; #ifdef __cplusplus diff --git a/test/corpus/application.txt b/test/corpus/application.txt index 5511fa6..58f1a58 100644 --- a/test/corpus/application.txt +++ b/test/corpus/application.txt @@ -2,10 +2,11 @@ Application =========== -foo (A B : *) (f : A -> B) (x : A) := +def foo (A B : *) (f : A -> B) (x : A) := (fun (x : B) => x) (f x); --- + (program (definition (identifier) diff --git a/test/corpus/arrows.txt b/test/corpus/arrows.txt index 23539fa..88675c2 100644 --- a/test/corpus/arrows.txt +++ b/test/corpus/arrows.txt @@ -2,7 +2,7 @@ Arrows ====== -foo (A B : *) (f : A -> A -> B) (x : A) := f x x; +def foo (A B : *) (f : A -> A -> B) (x : A) := f x x; --- diff --git a/test/corpus/axioms.txt b/test/corpus/axioms.txt index 1cdbf91..1b52a05 100644 --- a/test/corpus/axioms.txt +++ b/test/corpus/axioms.txt @@ -2,17 +2,16 @@ Axioms ====== -nat : * := axiom; +axiom nat : *; ----- (program - (definition + (axiom (identifier) (ascription (expr (app_term (app (term - (star)))))) - (axiom))) + (star)))))))) diff --git a/test/corpus/comments.txt b/test/corpus/comments.txt index d8709fe..2c6184d 100644 --- a/test/corpus/comments.txt +++ b/test/corpus/comments.txt @@ -2,23 +2,9 @@ Comments ======== --- here's a comment - -foo := - -- and a comment in the middle - [* and a [* nested *] block comment *] - *; +[* foo [* nested *] *] +axiom nat : *; +[* bar *] --- -(program - (comment) - (definition - (identifier) - (comment) - (block_comment) - (expr - (app_term - (app - (term - (star))))))) diff --git a/test/corpus/include.txt b/test/corpus/include.txt index ec2b3c9..4863ee1 100644 --- a/test/corpus/include.txt +++ b/test/corpus/include.txt @@ -4,7 +4,7 @@ Include @include foo.pg -baz : * := A; +def baz : * := A; @include bar.pg diff --git a/test/corpus/labs.txt b/test/corpus/labs.txt index 65d23fc..17a56f0 100644 --- a/test/corpus/labs.txt +++ b/test/corpus/labs.txt @@ -2,7 +2,7 @@ Lambda Abstraction ================== -foo := fun (A : *) (x : A) => x; +def foo := fun (A : *) (x : A) => x; ---------- diff --git a/test/corpus/let.txt b/test/corpus/let.txt index acfe6f1..a5a11da 100644 --- a/test/corpus/let.txt +++ b/test/corpus/let.txt @@ -2,12 +2,13 @@ Let === -foo := let (x := a) - (y := x) - (f (x : A) := x) - in - x - end; +def foo := + let (x : bar := a) + (y := x) + (f (x : A) := x) + in + x + end; --- @@ -19,6 +20,12 @@ foo := let (x := a) (let (binding (identifier) + (ascription + (expr + (app_term + (app + (term + (identifier)))))) (expr (app_term (app diff --git a/test/corpus/pabs.txt b/test/corpus/pabs.txt index 7101edf..7d2f45c 100644 --- a/test/corpus/pabs.txt +++ b/test/corpus/pabs.txt @@ -2,7 +2,7 @@ Pi Abstraction ============== -rel := forall (A : *) (x : A), *; +def rel := forall (A : *) (x : A), *; ---------- diff --git a/test/corpus/params.txt b/test/corpus/params.txt index 927a406..73b871c 100644 --- a/test/corpus/params.txt +++ b/test/corpus/params.txt @@ -2,7 +2,7 @@ Definition ========== -foo (A : *) (x y z : A) := x; +def foo (A : *) (x y z : A) := x; ---