From 54d60a76f3cff47a576b9de38b9f5dc678e920cc Mon Sep 17 00:00:00 2001 From: "Jeremy G. Siek" Date: Fri, 6 Dec 2024 16:14:32 -0500 Subject: [PATCH] error message improvement --- abstract_syntax.py | 14 ++-- proof_checker.py | 12 ++-- rec_desc_parser.py | 71 ++++++++++++-------- test/should-error/define_missing_semi.pf | 10 +++ test/should-error/define_missing_semi.pf.err | 5 ++ test/should-error/function_not_union.pf | 4 ++ test/should-error/function_not_union.pf.err | 1 + 7 files changed, 79 insertions(+), 38 deletions(-) create mode 100644 test/should-error/define_missing_semi.pf create mode 100644 test/should-error/define_missing_semi.pf.err create mode 100644 test/should-error/function_not_union.pf create mode 100644 test/should-error/function_not_union.pf.err diff --git a/abstract_syntax.py b/abstract_syntax.py index 0563a55..ffbd972 100644 --- a/abstract_syntax.py +++ b/abstract_syntax.py @@ -2217,11 +2217,15 @@ def __str__(self): def uniquify(self, env): self.pattern.uniquify(env) body_env = copy_dict(env) - - new_pat_params = [generate_name(x) for x in self.pattern.parameters] - for (old,new) in zip(self.pattern.parameters, new_pat_params): - body_env[old] = [new] - self.pattern.parameters = new_pat_params + + match self.pattern: + case PatternCons(loc, cons, parameters): + new_pat_params = [generate_name(x) for x in parameters] + for (old,new) in zip(parameters, new_pat_params): + body_env[old] = [new] + self.pattern.parameters = new_pat_params + case PatternBool(loc, b): + pass new_params = [generate_name(x) for x in self.parameters] for (old,new) in zip(self.parameters, new_params): diff --git a/proof_checker.py b/proof_checker.py index 2ebe0ea..3d81b96 100644 --- a/proof_checker.py +++ b/proof_checker.py @@ -2150,7 +2150,7 @@ def lookup_union(loc, typ, env): case TypeInst(loc2, inst_typ, tyargs): tyname = inst_typ case _: - error(loc, str(typ) + ' is not a union type') + error(loc, 'expected a union type but instead got ' + str(typ)) return env.get_def_of_type_var(tyname) def check_constructor_pattern(loc, pat_constr, params, typ, env, cases_present): @@ -2322,8 +2322,12 @@ def type_check_fun_case(fun_case, name, params, returns, body_env, cases_present + 'expected ' + str(len(params))) body_env = body_env.declare_term_vars(fun_case.location, zip(fun_case.parameters, params[1:])) - new_body = type_check_term(fun_case.body, returns, body_env, - name, fun_case.pattern.parameters) + match fun_case.pattern: + case PatternCons(loc, cons, parameters): + pat_params = parameters + case PatternBool(loc, val): + pat_params = [] + new_body = type_check_term(fun_case.body, returns, body_env, name, pat_params) return FunCase(fun_case.location, fun_case.pattern, fun_case.parameters, new_body) def type_check_stmt(stmt, env): @@ -2360,7 +2364,7 @@ def type_check_stmt(stmt, env): for c in cases] # check for completeness of cases - uniondef = lookup_union(loc, params[0], env) + uniondef = lookup_union(params[0].location, params[0], env) for c in uniondef.alternatives: if not c.name in cases_present.keys(): error(loc, 'missing function case for ' + base_name(c.name)) diff --git a/rec_desc_parser.py b/rec_desc_parser.py index 1ca7c2f..6ecd57f 100644 --- a/rec_desc_parser.py +++ b/rec_desc_parser.py @@ -353,18 +353,25 @@ def parse_term_hi(): 'expected a term, not\n\t' + quote(current_token().value)) def parse_call(): + while_parsing = 'while parsing function call\n' \ + + '\tterm ::= term "(" term_list ")"\n' term = parse_term_hi() while (not end_of_file()) and current_token().type == 'LPAR': - start_token = current_token() - advance() - args = parse_term_list() - if current_token().type != 'RPAR': - error(meta_from_tokens(start_token, previous_token()), - 'expected closing parenthesis `)`') - advance() - term = Call(meta_from_tokens(start_token, previous_token()), None, - term, args, False) + try: + start_token = current_token() + advance() + args = parse_term_list() + if current_token().type != 'RPAR': + error(meta_from_tokens(start_token, current_token()), + 'expected closing parenthesis ")", not\n\t' \ + + current_token().value) + term = Call(meta_from_tokens(start_token, current_token()), None, + term, args, False) + advance() + except Exception as e: + meta = meta_from_tokens(start_token, previous_token()) + raise Exception(str(e) + '\n' + error_header(meta) + while_parsing) return term @@ -459,27 +466,8 @@ def parse_term(): token = current_token() if token.type == 'DEFINE': - advance() - name = parse_identifier() - if current_token().type != 'EQUAL': - error(meta_from_tokens(current_token(),current_token()), - 'expected `=` after name in `define`, not\n\t' \ - + current_token().value) - advance() - rhs = parse_term_logic() - if current_token().type != 'SEMICOLON': - error(meta_from_tokens(current_token(),current_token()), - 'expected `;` after term of `define`, not\n\t' \ - + current_token().value \ - + '\nwhile parsing\n' \ - + '\tterm ::= "define" IDENT "=" term ";" term') - advance() - meta = meta_from_tokens(token, previous_token()) - body = parse_term() - return TLet(meta, None, name, rhs, body) - + return parse_define_term() else: - term = parse_term_logic() if (not end_of_file()) and (current_token().value in iff_operators): advance() @@ -497,6 +485,31 @@ def parse_term(): return term +def parse_define_term(): + while_parsing = 'while parsing\n' \ + + '\tterm ::= "define" identifier "=" term ";" term\n' + try: + start_token = current_token() + advance() + name = parse_identifier() + if current_token().type != 'EQUAL': + error(meta_from_tokens(current_token(),current_token()), + 'expected "=" after name in "define", not\n\t' \ + + quote(current_token().value)) + advance() + rhs = parse_term_logic() + if current_token().type != 'SEMICOLON': + error(meta_from_tokens(current_token(),current_token()), + 'expected ";" after right-hand side of "define", not\n\t' \ + + quote(current_token().value)) + advance() + meta = meta_from_tokens(start_token, previous_token()) + body = parse_term() + return TLet(meta, None, name, rhs, body) + except Exception as e: + meta = meta_from_tokens(start_token, previous_token()) + raise Exception(str(e) + '\n' + error_header(meta) + while_parsing) + def parse_assumption(): if current_token().type == 'COLON': label = '_' diff --git a/test/should-error/define_missing_semi.pf b/test/should-error/define_missing_semi.pf new file mode 100644 index 0000000..e62d60a --- /dev/null +++ b/test/should-error/define_missing_semi.pf @@ -0,0 +1,10 @@ +union Bit { + zero + one +} + +function f(Bit) -> Bit { + f(zero) = one + f(one) = define z = zero + z +} diff --git a/test/should-error/define_missing_semi.pf.err b/test/should-error/define_missing_semi.pf.err new file mode 100644 index 0000000..c3ffac9 --- /dev/null +++ b/test/should-error/define_missing_semi.pf.err @@ -0,0 +1,5 @@ +./test/should-error/define_missing_semi.pf:9.12-9.13: expected ";" after right-hand side of "define", not + "z" +./test/should-error/define_missing_semi.pf:8.12-8.27: while parsing + term ::= "define" identifier "=" term ";" term + diff --git a/test/should-error/function_not_union.pf b/test/should-error/function_not_union.pf new file mode 100644 index 0000000..13d8136 --- /dev/null +++ b/test/should-error/function_not_union.pf @@ -0,0 +1,4 @@ +function f(bool) -> bool { + f(true) = false + f(false) = true +} diff --git a/test/should-error/function_not_union.pf.err b/test/should-error/function_not_union.pf.err new file mode 100644 index 0000000..b91df91 --- /dev/null +++ b/test/should-error/function_not_union.pf.err @@ -0,0 +1 @@ +./test/should-error/function_not_union.pf:1.12-1.16: expected a union type but instead got bool