From 1599f4e1fdc3c55d11d74d604e0ed24268a12aab Mon Sep 17 00:00:00 2001 From: Calvin Josenhans Date: Fri, 24 Jan 2025 10:00:20 -0500 Subject: [PATCH 1/6] add new keywords to parser list --- rec_desc_parser.py | 8 ++++---- 1 file changed, 4 insertions(+), 4 deletions(-) diff --git a/rec_desc_parser.py b/rec_desc_parser.py index 375abb7..76a3712 100644 --- a/rec_desc_parser.py +++ b/rec_desc_parser.py @@ -591,12 +591,12 @@ def parse_assumption(): else: return label,None -proof_keywords = {'apply', 'arbitrary', +proof_keywords = {'apply', 'arbitrary', 'assume', 'cases', 'choose', 'conclude', 'conjunct', 'definition', - 'enable', 'equations', 'extensionality', - 'have', 'induction', 'obtain', - 'reflexive', 'rewrite', + 'enable', 'equations', 'evaluate', 'extensionality', + 'have', 'help', 'induction', 'injective', 'obtain', + 'recall', 'reflexive', 'rewrite', 'suffices', 'suppose', 'switch', 'symmetric', 'transitive'} From a74282dc237703d9c3adcbaf3614e68368268bfb Mon Sep 17 00:00:00 2001 From: Calvin Josenhans Date: Fri, 24 Jan 2025 10:13:58 -0500 Subject: [PATCH 2/6] change != to /= (matching lark parser --- rec_desc_parser.py | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/rec_desc_parser.py b/rec_desc_parser.py index 76a3712..66c17cb 100644 --- a/rec_desc_parser.py +++ b/rec_desc_parser.py @@ -499,7 +499,7 @@ def parse_term_equal(): if opr == '=': term = Call(meta_from_tokens(token, previous_token()), None, eq, [term,right]) - elif opr == '≠' or opr == '!=': + elif opr == '≠' or opr == '/=': term = IfThen(meta, None, Call(meta, None, eq, [term,right]), Bool(meta, None, False)) From 152e974a3a65ea241cd5e3870e138b6f17901ad8 Mon Sep 17 00:00:00 2001 From: Calvin Josenhans Date: Fri, 24 Jan 2025 10:14:39 -0500 Subject: [PATCH 3/6] Fixing != to /= --- rec_desc_parser.py | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/rec_desc_parser.py b/rec_desc_parser.py index 66c17cb..7e4aa2a 100644 --- a/rec_desc_parser.py +++ b/rec_desc_parser.py @@ -29,8 +29,8 @@ def get_deduce_directory(): mult_operators = {'*', '/', '%', '∘', '.o.'} add_operators = {'+', '-', '∪', '|', '∩', '&', '⨄', '.+.', '++' } -compare_operators = {'<', '>', '≤', '<=', '>', '≥', '>=', '⊆', '(=', '∈', 'in'} -equal_operators = {'=', '≠', '!='} +compare_operators = {'<', '>', '≤', '<=', '≥', '>=', '⊆', '(=', '∈', 'in'} +equal_operators = {'=', '≠', '/='} iff_operators = {'iff', "<=>", "⇔"} to_unicode = {'.o.': '∘', '|': '∪', '&': '∩', '.+.': '⨄', '<=': '≤', '>=': '≥', From af8408b225ce0eac2029db41bc477ce117e0c9ac Mon Sep 17 00:00:00 2001 From: Calvin Josenhans Date: Fri, 24 Jan 2025 10:20:07 -0500 Subject: [PATCH 4/6] help is too close to els --- rec_desc_parser.py | 36 +++++++++++++++++++++++++++++------- 1 file changed, 29 insertions(+), 7 deletions(-) diff --git a/rec_desc_parser.py b/rec_desc_parser.py index 7e4aa2a..2455d12 100644 --- a/rec_desc_parser.py +++ b/rec_desc_parser.py @@ -53,10 +53,16 @@ def init_parser(): token_list = [] def current_token(): - return token_list[current_position] + if end_of_file(): + error(meta_from_tokens(token_list[-1], token_list[-1]), + 'Expected a token, got end of file') + return token_list[current_position] def next_token(): - return token_list[current_position + 1] + if current_position + 1 >= len(token_list): + error(meta_from_tokens(token_list[-1], token_list[-1]), + 'Expected a token, got end of file') + return token_list[current_position + 1] def previous_token(): return token_list[current_position - 1] @@ -595,7 +601,7 @@ def parse_assumption(): 'cases', 'choose', 'conclude', 'conjunct', 'definition', 'enable', 'equations', 'evaluate', 'extensionality', - 'have', 'help', 'induction', 'injective', 'obtain', + 'have', 'induction', 'injective', 'obtain', 'recall', 'reflexive', 'rewrite', 'suffices', 'suppose', 'switch', 'symmetric', 'transitive'} @@ -1085,6 +1091,11 @@ def parse_have(): start_token = current_token() token = start_token advance() + + if end_of_file(): + error(meta_from_tokens(start_token, start_token), + 'expected an identifier or colon after "have", not end of file') + if current_token().type != 'COLON': try: label = parse_identifier() @@ -1094,13 +1105,20 @@ def parse_have(): + current_token().value) else: label = '_' - if current_token().type != 'COLON': + + if end_of_file(): + error(meta_from_tokens(start_token, start_token), + 'expected a colon after label of "have", not end of file') + elif current_token().type != 'COLON': error(meta_from_tokens(current_token(), current_token()), 'expected a colon after label of "have", not\n\t' \ + current_token().value) advance() proved = parse_term() - if current_token().type == 'BY': + if end_of_file(): + error(meta_from_tokens(start_token, start_token), + 'expected the keyword "by" after formula of "have", not end of file') + elif current_token().type == 'BY': advance() because = parse_proof() else: @@ -1246,8 +1264,12 @@ def parse_theorem(): try: name = parse_identifier() except Exception as e: - error(meta_from_tokens(current_token(), current_token()), - 'expected name of theorem, not:\n\t' + current_token().value) + if end_of_file(): + error(meta_from_tokens(start_token, start_token), + 'expected name of theorem, not end of file') + else: + error(meta_from_tokens(current_token(), current_token()), + 'expected name of theorem, not:\n\t' + current_token().value) if current_token().type != 'COLON': error(meta_from_tokens(current_token(), current_token()), From 5a1069c1a94d2ce756fd1ebf59ade66c0e367d28 Mon Sep 17 00:00:00 2001 From: Calvin Josenhans Date: Fri, 24 Jan 2025 11:04:06 -0500 Subject: [PATCH 5/6] Synchronize lalr and rec_desc parsers --- Deduce.lark | 26 +++++++++++-------- abstract_syntax.py | 2 +- rec_desc_parser.py | 51 ++++++++++++++++++++++--------------- test/should-pass/bicond3.pf | 9 +++++++ test/should-pass/bicond4.pf | 27 ++++++++++++++++++++ 5 files changed, 83 insertions(+), 32 deletions(-) create mode 100644 test/should-pass/bicond3.pf create mode 100644 test/should-pass/bicond4.pf diff --git a/Deduce.lark b/Deduce.lark index 77786f9..80131d0 100644 --- a/Deduce.lark +++ b/Deduce.lark @@ -9,22 +9,24 @@ WS: /[ \t\f\r\n]/+ LINECOMMENT: "//" /[^\n]*/ COMMENT: /\/\*([^\*]|\*+[^\/])*\*+\// -?term: term "iff" term_log -> iff_formula - | term "<=>" term_log -> iff_formula - | term "⇔" term_log -> iff_formula +?term: term_iff + +?term_iff: term_iff "iff" term_log -> iff_formula + | term_iff "<=>" term_log -> iff_formula + | term_iff "⇔" term_log -> iff_formula | term_log -?term_log: term_log "and" term_compare -> and_formula - | term_log "or" term_compare -> or_formula +?term_log: term_log "and" term_equal -> and_formula + | term_log "or" term_equal -> or_formula | term_log ":" type -> annote_type - | "if" term_log "then" term_log "else" term_log -> conditional - | "if" term_log "then" term_log -> if_then_formula + | term_equal + +?term_equal: term_equal "=" term_compare -> equal + | term_equal "≠" term_compare -> not_equal + | term_equal "/=" term_compare -> not_equal | term_compare -?term_compare: term_compare "=" term_add -> equal - | term_compare "≠" term_add -> not_equal - | term_compare "/=" term_add -> not_equal - | term_compare "<" term_add -> less +?term_compare: term_compare "<" term_add -> less | term_compare ">" term_add -> greater | term_compare "≤" term_add -> less_equal | term_compare "<=" term_add -> less_equal @@ -99,6 +101,8 @@ ident: IDENT -> ident | "(" term ")" -> paren | "[" term_list "]" -> list_literal | "#" term "#" -> mark + | "if" term "then" term "else" term -> conditional + | "if" term "then" term -> if_then_formula | "%" type ?term_list: -> empty diff --git a/abstract_syntax.py b/abstract_syntax.py index f99cd3c..bd7998e 100644 --- a/abstract_syntax.py +++ b/abstract_syntax.py @@ -1553,7 +1553,7 @@ class All(Formula): def copy(self): x, t = self.var - return All(self.location, (x, t.copy()), self.pos, self.body.copy()) + return All(self.location, self.typeof, (x, t.copy()), self.pos, self.body.copy()) def __str__(self): v, t = self.var diff --git a/rec_desc_parser.py b/rec_desc_parser.py index 2455d12..fb71bbf 100644 --- a/rec_desc_parser.py +++ b/rec_desc_parser.py @@ -369,7 +369,10 @@ def parse_term_hi(): 'expected closing bracket \']\', not\n\t' + current_token().value) advance() return listToNodeList(meta_from_tokens(token,token), lst_terms) - + + elif token.type == 'DEFINE': + return parse_define_term() + else: try: name = parse_identifier() @@ -534,32 +537,40 @@ def parse_term_logic(): return term +def parse_term_iff(): + token = current_token() + term = parse_term_logic() + while (not end_of_file()) and (current_token().value in iff_operators): + opr = current_token().type + advance() + right = parse_term_logic() + loc = meta_from_tokens(token, previous_token()) + left_right = IfThen(loc, None, term.copy(), right.copy()) + right_left = IfThen(loc, None, right.copy(), term.copy()) + term = And(loc, None, [left_right, right_left]) + + if (not end_of_file()) and current_token().type == 'COLON': + advance() + typ = parse_type() + term = TAnnote(meta_from_tokens(token, previous_token()), None, + term, typ) + + return term + def parse_term(): if end_of_file(): error(meta_from_tokens(previous_token(),previous_token()), 'expected a term, not end of file') token = current_token() + term = parse_term_iff() - if token.type == 'DEFINE': - return parse_define_term() - else: - term = parse_term_logic() - if (not end_of_file()) and (current_token().value in iff_operators): - advance() - right = parse_term_logic() - loc = meta_from_tokens(token, previous_token()) - left_right = IfThen(loc, None, term.copy(), right.copy()) - right_left = IfThen(loc, None, right.copy(), term.copy()) - term = And(loc, None, [left_right, right_left]) - - if (not end_of_file()) and current_token().type == 'COLON': - advance() - typ = parse_type() - term = TAnnote(meta_from_tokens(token, previous_token()), None, - term, typ) - - return term + if not end_of_file() and current_token().type == 'COLON': + advance() + typ = parse_type() + term = TAnnote(meta_from_tokens(token, previous_token()), None, + term, typ) + return term def parse_define_term(): while_parsing = 'while parsing\n' \ diff --git a/test/should-pass/bicond3.pf b/test/should-pass/bicond3.pf new file mode 100644 index 0000000..4856bfd --- /dev/null +++ b/test/should-pass/bicond3.pf @@ -0,0 +1,9 @@ +theorem bicond_commute : all P : bool, Q : bool. + if P <=> Q then Q <=> P +proof + arbitrary P : bool, Q : bool + switch P { + case true assume prop_t { . } + case false assume prop_f { . } + } +end \ No newline at end of file diff --git a/test/should-pass/bicond4.pf b/test/should-pass/bicond4.pf new file mode 100644 index 0000000..515b791 --- /dev/null +++ b/test/should-pass/bicond4.pf @@ -0,0 +1,27 @@ +theorem bicond_trans : all P : bool, Q : bool, R : bool. + if (P <=> Q) and (Q <=> R) then P <=> R +proof + arbitrary P : bool, Q : bool, R : bool + switch P { + case true assume prop_t { + switch Q { + case true assume prop_t { + . + } + case false assume prop_f { + . + } + } + } + case false assume prop_f { + switch Q { + case true assume prop_t { + . + } + case false assume prop_f { + . + } + } + } + } +end \ No newline at end of file From ea211d6503e0e4318968cb2d92b608d13a1d6ac7 Mon Sep 17 00:00:00 2001 From: Calvin Josenhans Date: Fri, 24 Jan 2025 15:58:48 -0500 Subject: [PATCH 6/6] updating the comma error --- rec_desc_parser.py | 8 ++++---- test/should-error/deep_error.pf.err | 1 + 2 files changed, 5 insertions(+), 4 deletions(-) diff --git a/rec_desc_parser.py b/rec_desc_parser.py index fb71bbf..bde5234 100644 --- a/rec_desc_parser.py +++ b/rec_desc_parser.py @@ -366,7 +366,7 @@ def parse_term_hi(): token = current_token() if token.type != 'RSQB': error(meta_from_tokens(current_token(),current_token()), - 'expected closing bracket \']\', not\n\t' + current_token().value) + 'expected closing bracket "]" at end of list literal, not\n\t' + current_token().value) advance() return listToNodeList(meta_from_tokens(token,token), lst_terms) @@ -416,9 +416,9 @@ def parse_call(): advance() args = parse_term_list() if current_token().type != 'RPAR': - msg = f'expected closing parenthesis ")", not\n\t{current_token().value}' - if current_token().type == 'IDENT': - msg += '\nPerhaps you forgot a comma?' + msg = 'expected closing parenthesis ")", not\n\t' \ + + current_token().value \ + + '\nPerhaps you forgot a comma?' error(meta_from_tokens(start_token, previous_token()), msg) term = Call(meta_from_tokens(start_token, current_token()), None, term, args) diff --git a/test/should-error/deep_error.pf.err b/test/should-error/deep_error.pf.err index a87bbec..4da97fc 100644 --- a/test/should-error/deep_error.pf.err +++ b/test/should-error/deep_error.pf.err @@ -1,5 +1,6 @@ ./test/should-error/deep_error.pf:1.28-1.34: expected closing parenthesis ")", not 2 +Perhaps you forgot a comma? ./test/should-error/deep_error.pf:1.28-1.34: while parsing function call term ::= term "(" term_list ")"