diff --git a/CHANGELOG_NEXT.md b/CHANGELOG_NEXT.md index 7952b2244e..3ebc62d6d7 100644 --- a/CHANGELOG_NEXT.md +++ b/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 diff --git a/docs/source/tutorial/modules.rst b/docs/source/tutorial/modules.rst index c5744120f0..4fc26aa057 100644 --- a/docs/source/tutorial/modules.rst +++ b/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} + diff --git a/src/Compiler/Scheme/Common.idr b/src/Compiler/Scheme/Common.idr index b872f0e9ca..16f4a7602f 100644 --- a/src/Compiler/Scheme/Common.idr +++ b/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) diff --git a/src/Core/Normalise/Eval.idr b/src/Core/Normalise/Eval.idr index d141c0ff7a..60ee283859 100644 --- a/src/Core/Normalise/Eval.idr +++ b/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 : _} -> diff --git a/src/Idris/Parser.idr b/src/Idris/Parser.idr index 1d7db8830a..fcd008a257 100644 --- a/src/Idris/Parser.idr +++ b/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