error message improvement

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):

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))

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 = '_'

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
+}

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
+

test/should-error/function_not_union.pf

@@ -0,0 +1,4 @@
+function f(bool) -> bool {
+  f(true) = false
+  f(false) = true
+}

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