additions to the Reference, improved parsing for unions

doc/Reference.md

@@ -722,15 +722,18 @@ end
 conclusion ::= "evaluate"
 ```
 
-UNDER CONSTRUCTION
+The `evaluate` proof method simplies the goal formula by applying all
+definitions. It succeeds if the formula is simplified to `true`.
 
 ## Evaluate-In (Proof)
 
 ```
 conclusion ::= "evaluate" "in" proof
 ```
 
-UNDER CONSTRUCTION
+The `evaluate`-`in` proof method simplies the formula of the given
+proof by applying all definitions, producing a proof of the simplified
+formula.
 
 ## Extensionality
 
@@ -1462,11 +1465,7 @@ A term, formula, or a proof may be surrounded in parentheses.
 ## Pattern
 
 ```
-pattern ::= identifier
-pattern ::= "0"
-pattern ::= "true"
-pattern ::= "false"
-pattern ::= identifier "(" identifier_list ")"
+pattern ::= identifier | "0" | "true" | "false" | identifier "(" identifier_list ")"
 ```
 
 This syntax is used in [Switch (Term)](#switch-term), [Switch (Proof)](#switch-proof),
@@ -1476,9 +1475,7 @@ and [Function (Statement)](#function-statement) via [Pattern List](#pattern-list
 ## Pattern List
 
 ```
-pattern_list ::=
-pattern_list ::= pattern
-pattern_list ::= pattern "," ident_list
+pattern_list ::= ε | pattern | pattern "," ident_list
 ```
 
 A pattern list is a comma-separated sequence of zero or more patterns.
@@ -1914,11 +1911,39 @@ proof
 end
 ```
 
+## Type
+
+```
+type ::= "bool"                                        // type of a Boolean
+       | identifier                                    // type of a union
+       | identifier "<" type_list ">"                  // type of a generic union
+       | "fn" type_params_opt type_list "->" type      // type of a function 
+       | "(" type ")"
+```
+
+## Type List
+
+```
+type_list ::= ε | type | type "," type_list
+```
+
+A type list is a comma-separated list of zero or more types.
+
+
+## Type Parameters
+
+```
+type_params_opt ::= ε | "<" identifier_list ">"
+```
+
+Specifies the type parameters of a generic union or generic function.
+
 
 ## Union (Statement)
 
 ```
-statement ::= "union" identifier type_params_opt "{" constructor_list "}"
+statement ::= "union" identifier type_params_opt "{" constructor* "}"
+constructor ::= identifier | identifier "(" type_list ")"
 ```
 
 The `union` statement defines a new type whose values are created by

rec_desc_parser.py

@@ -1176,24 +1176,29 @@ def parse_theorem():
 
 
 def parse_union():
-  start_token = current_token()
-  advance()
-  name = parse_identifier()
-  type_params = parse_type_parameters()
-
-  if current_token().type != 'LBRACE':
-    error(meta_from_tokens(current_token(), current_token()),
-          'expected `{` after name of union, not\n\t' \
-          + current_token().value)
-  advance()
-  constr_list = []
-  while current_token().type != 'RBRACE':
-    constr = parse_constructor()
-    constr_list.append(constr)
-  advance()
+  while_parsing = 'while parsing\n' \
+      + '\tstatement ::= "union" identifier type_params_opt "{" constructor* "}"\n'
+  try:
+    start_token = current_token()
+    advance()
+    name = parse_identifier()
+    type_params = parse_type_parameters()
 
-  meta = meta_from_tokens(start_token, previous_token())
-  return Union(meta, name, type_params, constr_list)
+    if current_token().type != 'LBRACE':
+      error(meta_from_tokens(current_token(), current_token()),
+            'expected `{` after name of union, not\n\t' \
+            + current_token().value)
+    advance()
+    constr_list = []
+    while current_token().type != 'RBRACE':
+      constr = parse_constructor()
+      constr_list.append(constr)
+    meta = meta_from_tokens(start_token, current_token())
+    advance()
+    return Union(meta, name, type_params, constr_list)
+  except Exception as e:
+    meta = meta_from_tokens(start_token, current_token())
+    raise Exception(str(e) + '\n' + error_header(meta) + while_parsing)
 
 def parse_function():
   start_token = current_token()
@@ -1383,20 +1388,27 @@ def parse_term_list():
   return trm_list
 
 def parse_constructor():
-  token = current_token()
-  name = parse_identifier()
+  while_parsing = 'while parsing\n' \
+      + '\tconstructor ::= identifier | identifier "(" type_list ")"'
+  try:  
+    start_token = current_token()
+    name = parse_identifier()
 
-  if current_token().type == 'LPAR':
-    advance()
-    param_types = parse_type_list()
-    if current_token().type != 'RPAR':
-      error(meta_from_tokens(token, previous_token()),
-            'missing closing parenthesis')
-    advance()
-  else:
-    param_types = []
-  meta = meta_from_tokens(token, previous_token())
-  return Constructor(meta, name, param_types)
+    if current_token().type == 'LPAR':
+      advance()
+      param_types = parse_type_list()
+      if current_token().type != 'RPAR':
+        error(meta_from_tokens(start_token, previous_token()),
+              'missing closing parenthesis')
+      advance()
+    else:
+      param_types = []
+    meta = meta_from_tokens(start_token, previous_token())
+    return Constructor(meta, name, param_types)
+  except Exception as e:
+    meta = meta_from_tokens(start_token, current_token())
+    raise Exception(str(e) + '\n' + error_header(meta) + while_parsing)
+
 
 def parse_constructor_pattern():
   start_token = current_token()

test/should-error/union_bad_constructor.pf

@@ -0,0 +1,4 @@
+union Tree {
+  empty(bool)
+  node(Tree Tree)
+}

test/should-error/union_bad_constructor.pf.err

@@ -0,0 +1,6 @@
+./test/should-error/union_bad_constructor.pf:3.3-3.12: missing closing parenthesis
+./test/should-error/union_bad_constructor.pf:3.3-3.17: while parsing
+	constructor ::= identifier | identifier "(" type_list ")"
+./test/should-error/union_bad_constructor.pf:1.1-3.17: while parsing
+	statement ::= "union" identifier type_params_opt "{" constructor* "}"
+

test/should-error/union_missing_name.pf

@@ -0,0 +1,4 @@
+union {
+  empty(bool)
+  node(Tree, Nat,Tree)
+}

test/should-error/union_missing_name.pf.err

@@ -0,0 +1,5 @@
+./test/should-error/union_missing_name.pf:1.7-1.8: expected an identifier, not
+	"{"
+./test/should-error/union_missing_name.pf:1.1-1.8: while parsing
+	statement ::= "union" identifier type_params_opt "{" constructor* "}"
+