Merge pull request #344 from christopherastone/constants-with-comma

Multiple constants on a line requires commas

src/parser/parser.mly

@@ -123,7 +123,7 @@ plain_topcomp:
   | HANDLE lst=top_handler_cases END                  { TopHandle lst }
   | DO c=term                                         { TopDo c }
   | FAIL c=term                                       { TopFail c }
-  | CONSTANT xs=nonempty_list(var_name) COLON u=term  { DeclConstants (xs, u) }
+  | CONSTANT xs=separated_nonempty_list(COMMA, var_name) COLON u=term  { DeclConstants (xs, u) }
   | MLTYPE lst=mlty_defs                              { DefMLType lst }
   | MLTYPE REC lst=mlty_defs                          { DefMLTypeRec lst }
   | OPERATION op=var_name COLON opsig=op_mlsig        { DeclOperation (op, opsig) }

tests/bad-congr.m31

@@ -1,7 +1,7 @@
 
 fail congr_prod Type Type Type
 
-constant A B : Type
+constant A, B : Type
 
 fail congr_prod (assume x : A -> B in x) A (refl B)
 

tests/coerce.m31

@@ -1,4 +1,4 @@
-constant A B C : Type
+constant A, B, C : Type
 constant a : A
 constant f : A -> B
 constant g : B -> C

tests/dynamic.m31

@@ -1,6 +1,6 @@
 
 constant A : Type
-constant a b : A
+constant a, b : A
 
 dynamic x = a
 

tests/error-context-subst.m31

@@ -1,6 +1,6 @@
 (* Substitute with different values in separate subterms, then join. *)
 
-constant A B C : Type
+constant A, B, C : Type
 constant pair : A -> B -> C
 
 let T = assume T : Type in T

tests/eta-pair.m31

@@ -26,7 +26,7 @@ constant pair_eta :
 
 constant C : Type
 constant D : Type
-constant p q : prod C D
+constant p, q : prod C D
 
 
 (* Beta rules. *)

tests/everything.m31

@@ -17,9 +17,9 @@ operation nonary_op : color
 (** Declare constants *)
 (* constant `names` : `type` *)
 constant A : (* the type of types *) Type
-constant a b : A
+constant a, b : A
 (* Ocaml-style infixes are valid `name`s and `label`s *)
-constant ( + ) ( * ) ( ^ ) ( - ) ( <= ) :
+constant ( + ), ( * ), ( ^ ), ( - ), ( <= ) :
   (* non-dependent product type *) A -> A -> A
 
 (* Infixes and prefixes are printed as such. *)

tests/generic.m31

@@ -1,5 +1,5 @@
 
-constant A B : Type
+constant A, B : Type
 constant eq : A == B
 now betas = add_beta eq
 

tests/handle-pattern-default.m31

@@ -2,7 +2,7 @@
 operation O : judgement -> mlstring
 
 constant A : Type
-constant a b : A
+constant a, b : A
 
 (* when an operation doesn't match, we need to bubble it upwards, then pass the result to the continuation *)
 do 

tests/implicit.m31

@@ -1,6 +1,6 @@
 constant A : Type
 constant a : A
-constant f g h : A -> A
+constant f, g, h : A -> A
 constant g_def : g == (lambda x : A, f (f x))
 constant h_def : h == g
 

tests/infixes.m31

@@ -2,9 +2,9 @@
 (** TT infixes *)
 constant A : Type
 
-constant a b c d : A
+constant a, b, c, d : A
 
-constant ( + ) ( - ) ( ^ ) ( / ) : A -> A -> A
+constant ( + ), ( - ), ( ^ ), ( / ) : A -> A -> A
 
 let s = (-) ((+) a b) ((^) c ((^) d d))
 

tests/many-constants-declaration.m31

@@ -1,5 +1,5 @@
 (* Test whether declaration of several constants works. *)
-constant A B : Type
-constant f g : A -> Type
+constant A, B : Type
+constant f, g : A -> Type
 constant a : A
-constant x y z : f a -> Type
+constant x, y, z : f a -> Type

tests/natural.m31

@@ -1,4 +1,4 @@
-constant A B : Type
+constant A, B : Type
 constant a : A
 constant eq : A == B
 
@@ -18,4 +18,4 @@ do
     natural (f a : (a == a))
   with
   | coerce (|- _ : C a) (|- a == a) => yield (Convertible xi)
-  end
+  end

tests/unhandled-op.m31

@@ -2,7 +2,7 @@
 mltype x = x end
 
 constant A : Type
-constant a b : A
+constant a, b : A
 constant (+) : A -> A -> A
 
 operation Not_found : empty