deprecate old parameter-block syntax (#3464)

CHANGELOG_NEXT.md

@@ -78,6 +78,13 @@ This CHANGELOG describes the merged but unreleased changes. Please see [CHANGELO
 
 * Added syntax to specifying quantity for proof in with-clause.
 
+* Old-style parameter block syntax is deprecated in favor of the new one.
+  In Idris1 you could write `parameters (a : t1, b : t2)` but this did not
+  allow for implicits arguments or quantities, this is deprecated. Use the
+  new Idris2 syntax instead where you can write
+  `parameters {0 t : Type} (v : t)` to indicate if arguments are implicit or
+  erased.
+
 ### Compiler changes
 
 * The compiler now differentiates between "package search path" and "package

docs/source/tutorial/modules.rst

@@ -301,15 +301,15 @@ Look at the following example.
     useNSFromOutside' : String
     useNSFromOutside' = Y.g "x" -- value is "xa"
 
-Parameterised blocks
-====================
+Parameterised blocks - `parameters`-blocks
+==========================================
 
 Groups of functions can be parameterised over a number of arguments
 using a ``parameters`` declaration, for example:
 
 .. code-block:: idris
 
-    parameters (x : Nat, y : Nat)
+    parameters (x : Nat) (y : Nat)
       addAll : Nat -> Nat
       addAll z = x + y + z
 
@@ -338,7 +338,7 @@ constructors. They may also be dependent types with implicit arguments:
 
 .. code-block:: idris
 
-    parameters (y : Nat, xs : Vect x a)
+    parameters (y : Nat) (xs : Vect x a)
       data Vects : Type -> Type where
         MkVects : Vect y a -> Vects a
 
@@ -353,3 +353,11 @@ which can be inferred by the type checker:
 
     Main> show (append _ _ (MkVects _ [1,2,3] [4,5,6]))
     "[1, 2, 3, 4, 5, 6]"
+
+You can specify what quantity and if the parameters are implicits using
+the same syntax as record parameters.
+
+.. code-block:: idris
+
+    parameters {0 m : Type -> Type} {auto mon : Monad m}
+

src/Compiler/Scheme/Common.idr

@@ -335,10 +335,10 @@ weakMemoLaziness = MkLazyExprProc
   (\expr => "(blodwen-delay-lazy (lambda () " ++ expr ++ "))")
   (\expr => "(blodwen-force-lazy " ++ expr ++ ")")
 
-parameters (constants : SortedSet Name,
-            schExtPrim : Nat -> ExtPrim -> List NamedCExp -> Core Builder,
-            schString : String -> Builder,
-            schLazy : LazyExprProc)
+parameters (constants : SortedSet Name)
+           (schExtPrim : Nat -> ExtPrim -> List NamedCExp -> Core Builder)
+           (schString : String -> Builder)
+           (schLazy : LazyExprProc)
   showTag : Name -> Maybe Int -> Builder
   showTag n (Just i) = showB i
   showTag n Nothing = schString (show n)

src/Core/Normalise/Eval.idr

@@ -91,7 +91,7 @@ record TermWithEnv (free : List Name) where
     locEnv : LocalEnv free varsEnv
     term : Term $ varsEnv ++ free
 
-parameters (defs : Defs, topopts : EvalOpts)
+parameters (defs : Defs) (topopts : EvalOpts)
   mutual
     eval : {auto c : Ref Ctxt Defs} ->
            {free, vars : _} ->

src/Idris/Parser.idr

@@ -1850,7 +1850,7 @@ paramDecls fname indents = do
          _ <- decoratedKeyword fname "parameters"
          _ <- commit
          params <- Right <$> newParamDecls fname indents
-               <|> Left <$> oldParamDecls fname indents
+               <|> Left <$> withWarning "DEPRECATED: old parameter syntax https://github.com/idris-lang/Idris2/issues/3447" (oldParamDecls fname indents)
          commit
          declarations <- bounds $ nonEmptyBlockAfter startCol (topDecl fname)
          pure (PParameters params