Implement new parameters syntax

Previously, parameter block reused the same syntax as in Idris1:

```
parameters (v1 : t1, … , vn : tn)
```

Unfortunately this syntax presents some issues:
 - It does not allow to declare implicit parameters
 - It does not allow to specify which multiplicity to use
 - It is inconsistent with the syntax used for named arguments elsewhere
   in the language.

This change fixes those three problems by borrowing the syntax for
declaring type parameters in records:

```
parameters (v1 : t2) (v2 : t2) … (vn : tn)
```

It also enables other features like multiple declarations of arguments
with the same type:

```
parameters (v1, v2 : Type)
```

CHANGELOG.md

@@ -13,6 +13,13 @@ REPL/IDE mode changes:
 * Added `:search` command, which searches for functions by type
 * `:load`/`:l` and `:cd` commands now only accept paths surrounded by double quotes
 
+Syntax changes:
+
+* The syntax for parameter blocks has been updated. It now allows to declare
+  implicit parameters and give multiplicities for parameters. The old syntax
+  is still available for compatibility purposes but will be removed in the
+  future.
+
 Compiler changes:
 
 * Racket codegen now always uses `blodwen-sleep` instead of `idris2_sleep` in
@@ -29,18 +36,6 @@ Library changes:
 
 Other changes:
 
-* The `version` field in `.ipkg` files is now used. Packages are installed into
-  a directory which includes its version number, and dependencies can have
-  version number ranges using `<=`, `<`, `>=`, `>`, `==` to express version
-  constraints. Version numbers must be in the form of integers, separated by
-  dots (e.g. `1.0`, `0.3.0`, `3.1.4.1.5` etc)
-* Idris now looks in the current working directory, under a subdirectory
-  `depends` for local installations of packages before looking globally.
-* Added an environment variable `IDRIS2_PACKAGE_PATH` for extending where to
-  look for packages.
-
-Other changes:
-
 * The `version` field in `.ipkg` files is now used. Packages are installed into
   a directory which includes its version number, and dependencies can have
   version number ranges using `<=`, `<`, `>=`, `>`, `==` to express version

src/Core/TT.idr

@@ -388,6 +388,20 @@ Functor PiInfo where
   map func AutoImplicit = AutoImplicit
   map func (DefImplicit t) = (DefImplicit (func t))
 
+export
+Foldable PiInfo where
+  foldr f acc Implicit = acc
+  foldr f acc Explicit = acc
+  foldr f acc AutoImplicit = acc
+  foldr f acc (DefImplicit x) = f x acc
+
+export
+Traversable PiInfo where
+  traverse f Implicit = pure Implicit
+  traverse f Explicit = pure Explicit
+  traverse f AutoImplicit = pure AutoImplicit
+  traverse f (DefImplicit x) = map DefImplicit (f x)
+
 export
 Functor Binder where
   map func (Lam fc c x ty) = Lam fc c (map func x) (func ty)

src/Idris/Desugar.idr

@@ -783,16 +783,17 @@ mutual
       = pure [IData fc vis !(desugarData ps doc ddecl)]
   desugarDecl ps (PParameters fc params pds)
       = do pds' <- traverse (desugarDecl (ps ++ map fst params)) pds
-           params' <- traverse (\ ntm => do tm' <- desugar AnyExpr ps (snd ntm)
-                                            pure (fst ntm, tm')) params
+           params' <- traverse (\(n, rig, i, ntm) => do tm' <- desugar AnyExpr ps ntm
+                                                        i' <- traverse (desugar AnyExpr ps) i
+                                                        pure (n, rig, i', tm')) params
            -- Look for implicitly bindable names in the parameters
            let pnames = ifThenElse !isUnboundImplicits
                           (concatMap (findBindableNames True
                                          (ps ++ map Builtin.fst params) [])
-                                       (map Builtin.snd params'))
+                                       (map (Builtin.snd . Builtin.snd . Builtin.snd) params'))
                           []
-           let paramsb = map (\ ntm => (Builtin.fst ntm,
-                                        doBind pnames (Builtin.snd ntm))) params'
+           let paramsb = map (\(n, rig, info, tm) =>
+                                 (n, rig, info, doBind pnames tm)) params'
            pure [IParameters fc paramsb (concat pds')]
   desugarDecl ps (PUsing fc uimpls uds)
       = do syn <- get Syn
@@ -935,12 +936,7 @@ mutual
       mkConName n = DN (show n) (MN ("__mk" ++ show n) 0)
 
       mapDesugarPiInfo : List Name -> PiInfo PTerm -> Core (PiInfo RawImp)
-      mapDesugarPiInfo ps Implicit         = pure   Implicit
-      mapDesugarPiInfo ps Explicit         = pure   Explicit
-      mapDesugarPiInfo ps AutoImplicit     = pure   AutoImplicit
-      mapDesugarPiInfo ps (DefImplicit tm) = pure $ DefImplicit
-                                                  !(desugar AnyExpr ps tm)
-
+      mapDesugarPiInfo ps = traverse (desugar AnyExpr ps)
 
   desugarDecl ps (PFixity fc Prefix prec (UN n))
       = do syn <- get Syn

src/Idris/Parser.idr

@@ -1129,22 +1129,6 @@ mutualDecls fname indents
     = do ds <- bounds (keyword "mutual" *> commit *> assert_total (nonEmptyBlock (topDecl fname)))
          pure (PMutual (boundToFC fname ds) (concat ds.val))
 
-paramDecls : FileName -> IndentInfo -> Rule PDecl
-paramDecls fname indents
-    = do b <- bounds (do keyword "parameters"
-                         commit
-                         symbol "("
-                         ps <- sepBy (symbol ",")
-                                     (do x <- unqualifiedName
-                                         symbol ":"
-                                         ty <- typeExpr pdef fname indents
-                                         pure (UN x, ty))
-                         symbol ")"
-                         ds <- assert_total (nonEmptyBlock (topDecl fname))
-                         pure (ps, ds))
-         (ps, ds) <- pure b.val
-         pure (PParameters (boundToFC fname b) ps (collectDefs (concat ds)))
-
 usingDecls : FileName -> IndentInfo -> Rule PDecl
 usingDecls fname indents
     = do b <- bounds (do keyword "using"
@@ -1335,8 +1319,8 @@ fieldDecl fname indents
                              pure (\fc : FC => map (\n => MkField fc doc rig p n ty) (forget ns)))
              pure (b.val (boundToFC fname b))
 
-recordParam : FileName -> IndentInfo -> Rule (List (Name, RigCount, PiInfo PTerm,  PTerm))
-recordParam fname indents
+typedArg : FileName -> IndentInfo -> Rule (List (Name, RigCount, PiInfo PTerm, PTerm))
+typedArg fname indents
     = do symbol "("
          params <- pibindListName fname indents
          symbol ")"
@@ -1350,6 +1334,10 @@ recordParam fname indents
          params <- pibindListName fname indents
          symbol "}"
          pure $ map (\(c, n, tm) => (n.val, c, info, tm)) params
+
+recordParam : FileName -> IndentInfo -> Rule (List (Name, RigCount, PiInfo PTerm,  PTerm))
+recordParam fname indents
+    = typedArg fname indents
   <|> do n <- bounds name
          pure [(n.val, top, Explicit, PInfer (boundToFC fname n))]
 
@@ -1369,6 +1357,33 @@ recordDecl fname indents
                          pure (\fc : FC => PRecord fc doc vis n params (fst dcflds) (concat (snd dcflds))))
          pure (b.val (boundToFC fname b))
 
+paramDecls : FileName -> IndentInfo -> Rule PDecl
+paramDecls fname indents
+    = do b1 <- bounds (keyword "parameters")
+         commit
+         args <- bounds (newParamDecls fname indents <|> oldParamDecls fname indents)
+         commit
+         declarations <- the (Rule (WithBounds (List1 (List PDecl)))) (assert_total (Core.bounds $ nonEmptyBlock (topDecl fname)))
+         mergedBounds <- pure $  b1 `mergeBounds` (args `mergeBounds` declarations)
+         pure (PParameters (boundToFC fname mergedBounds) args.val (collectDefs (concat declarations.val)))
+
+  where
+    oldParamDecls : FileName -> IndentInfo -> Rule (List (Name, RigCount, PiInfo PTerm, PTerm))
+    oldParamDecls fname indents
+        = do symbol "("
+             ps <- sepBy (symbol ",")
+                         (do x <- unqualifiedName
+                             symbol ":"
+                             ty <- typeExpr pdef fname indents
+                             pure (UN x, top, Explicit, ty))
+             symbol ")"
+             pure ps
+
+    newParamDecls : FileName -> IndentInfo -> Rule (List (Name, RigCount, PiInfo PTerm, PTerm))
+    newParamDecls fname indents
+        = map concat (some $ typedArg fname indents)
+
+
 claims : FileName -> IndentInfo -> Rule (List1 PDecl)
 claims fname indents
     = do bs <- bounds (do

src/Idris/Resugar.idr

@@ -423,8 +423,10 @@ mutual
   toPDecl (IParameters fc ps ds)
       = do ds' <- traverse toPDecl ds
            pure (Just (PParameters fc
-                !(traverse (\ntm => do tm' <- toPTerm startPrec (snd ntm)
-                                       pure (fst ntm, tm')) ps)
+                        !(traverse (\(n, rig, info, tpe) =>
+                            do info' <- traverse (toPTerm startPrec) info
+                               tpe' <- toPTerm startPrec tpe
+                               pure (n, rig, info', tpe')) ps)
                 (mapMaybe id ds')))
   toPDecl (IRecord fc _ vis r)
       = do (n, ps, con, fs) <- toPRecord r

src/Idris/Syntax.idr

@@ -297,7 +297,7 @@ mutual
        PClaim : FC -> RigCount -> Visibility -> List PFnOpt -> PTypeDecl -> PDecl
        PDef : FC -> List PClause -> PDecl
        PData : FC -> (doc : String) -> Visibility -> PDataDecl -> PDecl
-       PParameters : FC -> List (Name, PTerm) -> List PDecl -> PDecl
+       PParameters : FC -> List (Name, RigCount, PiInfo PTerm, PTerm) -> List PDecl -> PDecl
        PUsing : FC -> List (Maybe Name, PTerm) -> List PDecl -> PDecl
        PReflect : FC -> PTerm -> PDecl
        PInterface : FC ->
@@ -1057,7 +1057,7 @@ mapPTermM f = goPTerm where
     goPDecl (PDef fc cls) = PDef fc <$> goPClauses cls
     goPDecl (PData fc doc v d) = PData fc doc v <$> goPDataDecl d
     goPDecl (PParameters fc nts ps) =
-      PParameters fc <$> goPairedPTerms nts
+      PParameters fc <$> go4TupledPTerms nts
                      <*> goPDecls ps
     goPDecl (PUsing fc mnts ps) =
       PUsing fc <$> goPairedPTerms mnts

src/TTImp/Elab/Quote.idr

@@ -152,11 +152,12 @@ mutual
   getUnquoteDecl (IDef fc v d)
       = pure $ IDef fc v !(traverse getUnquoteClause d)
   getUnquoteDecl (IParameters fc ps ds)
-      = pure $ IParameters fc !(traverse unqPair ps)
+      = pure $ IParameters fc
+                           !(traverse unqTuple ps)
                            !(traverse getUnquoteDecl ds)
     where
-      unqPair : (Name, RawImp) -> Core (Name, RawImp)
-      unqPair (n, t) = pure (n, !(getUnquote t))
+      unqTuple : (Name, RigCount, PiInfo RawImp, RawImp) -> Core (Name, RigCount, PiInfo RawImp, RawImp)
+      unqTuple (n, rig, i, t) = pure (n, rig, i, !(getUnquote t))
   getUnquoteDecl (IRecord fc ns v d)
       = pure $ IRecord fc ns v !(getUnquoteRecord d)
   getUnquoteDecl (INamespace fc ns ds)

src/TTImp/ProcessParams.idr

@@ -33,7 +33,7 @@ processParams : {vars : _} ->
                 {auto u : Ref UST UState} ->
                 NestedNames vars ->
                 Env Term vars ->
-                FC -> List (Name, RawImp) -> List ImpDecl ->
+                FC -> List (Name, RigCount, PiInfo RawImp, RawImp) -> List ImpDecl ->
                 Core ()
 processParams {vars} {c} {m} {u} nest env fc ps ds
     = do -- Turn the parameters into a function type, (x : ps) -> Type,
@@ -55,10 +55,10 @@ processParams {vars} {c} {m} {u} nest env fc ps ds
          let nestBlock = record { names $= (names' ++) } nest'
          traverse_ (processDecl [] nestBlock env') ds
   where
-    mkParamTy : List (Name, RawImp) -> RawImp
+    mkParamTy : List (Name, RigCount, PiInfo RawImp, RawImp) -> RawImp
     mkParamTy [] = IType fc
-    mkParamTy ((n, ty) :: ps)
-       = IPi fc top Explicit (Just n) ty (mkParamTy ps)
+    mkParamTy ((n, rig, info, ty) :: ps)
+       = IPi fc rig info (Just n) ty (mkParamTy ps)
 
     applyEnv : {vs : _} ->
                Env Term vs -> Name ->

src/TTImp/TTImp.idr

@@ -341,7 +341,7 @@ mutual
                 ImpTy -> ImpDecl
        IData : FC -> Visibility -> ImpData -> ImpDecl
        IDef : FC -> Name -> List ImpClause -> ImpDecl
-       IParameters : FC -> List (Name, RawImp) ->
+       IParameters : FC -> List (Name, RigCount, PiInfo RawImp, RawImp) ->
                      List ImpDecl -> ImpDecl
        IRecord : FC ->
                  Maybe String -> -- nested namespace

tests/Main.idr

@@ -163,7 +163,7 @@ idrisTests = MkTestPool []
        -- Namespace blocks
        "namespace001",
        -- Parameters blocks
-       "params001",
+       "params001","params002",
        -- Packages and ipkg files
        "pkg001", "pkg002", "pkg003", "pkg004", "pkg005", "pkg006", "pkg007",
        "pkg008", "pkg009",

tests/idris2/basic029/Params.idr

@@ -1,3 +1,3 @@
-parameters (x : Nat, y : Nat)
+parameters (x : Nat) (y : Nat)
   add : Nat
   add = x + y

tests/idris2/params002/ParamsPrint.idr

@@ -0,0 +1,13 @@
+parameters {n : Nat}
+           (a : Int)
+  0 func : Bool -> Type
+  func True = List Bool
+  func False = List Nat
+
+  getType : (b : Bool) -> func b
+  getType False = [0,1,2]
+  getType True = [True, True, True]
+
+  prf : (b : Bool) -> Int -> func b
+  prf b i = let i1 = getType b in ?whut
+

tests/idris2/params002/expected

@@ -0,0 +1,9 @@
+1/1: Building ParamsPrint (ParamsPrint.idr)
+Main>    {n : Nat}
+   a : Int
+   i : Int
+   b : Bool
+   i1 : func a b
+------------------------------
+whut : func a b
+Main> Bye for now!

tests/idris2/params002/input

@@ -0,0 +1,2 @@
+:t whut
+:q

tests/idris2/params002/run

@@ -0,0 +1,3 @@
+$1 --no-color --console-width 0 --no-banner ParamsPrint.idr < input
+
+rm -rf build