Add a 'reject' count to :gd

This gives the number of implementations to reject before accepting one.
It's intended as a reasonably cheap way of giving multiple results from
interactive editing (e.g. the vim mode, which goes via the REPL and
--client rather than the IDE mode)

src/Idris/IDEMode/REPL.idr

@@ -172,7 +172,7 @@ process (ExprSearch l n hs all)
 process ExprSearchNext
     = replWrap $ Idris.REPL.process (Editing ExprSearchNext)
 process (GenerateDef l n)
-    = replWrap $ Idris.REPL.process (Editing (GenerateDef False (fromInteger l) (UN n)))
+    = replWrap $ Idris.REPL.process (Editing (GenerateDef False (fromInteger l) (UN n) 0))
 process GenerateDefNext
     = replWrap $ Idris.REPL.process (Editing GenerateDefNext)
 process (MakeLemma l n)

src/Idris/Parser.idr

@@ -1717,7 +1717,8 @@ editCmd
          upd <- option False (do symbol "!"; pure True)
          line <- intLit
          n <- name
-         pure (GenerateDef upd (fromInteger line) n)
+         nreject <- option 0 intLit
+         pure (GenerateDef upd (fromInteger line) n (fromInteger nreject))
   <|> do replCmd ["gdnext"]
          pure GenerateDefNext
   <|> do replCmd ["ml", "makelemma"]

src/Idris/REPL.idr

@@ -311,8 +311,9 @@ nextProofSearch
 nextGenDef : {auto c : Ref Ctxt Defs} ->
              {auto u : Ref UST UState} ->
              {auto o : Ref ROpts REPLOpts} ->
+             (reject : Nat) ->
              Core (Maybe (Int, (FC, List ImpClause)))
-nextGenDef
+nextGenDef reject
     = do opts <- get ROpts
          let Just (line, res) = gdResult opts
               | Nothing => pure Nothing
@@ -321,7 +322,9 @@ nextGenDef
                     do put ROpts (record { gdResult = Nothing } opts)
                        pure Nothing
          put ROpts (record { gdResult = Just (line, next) } opts)
-         pure (Just (line, res))
+         case reject of
+              Z => pure (Just (line, res))
+              S k => nextGenDef k
 
 dropLams : {vars : _} ->
            Nat -> Env Term vars -> Term vars ->
@@ -418,7 +421,7 @@ processEdit ExprSearchNext
                                        else itm))
          pure $ DisplayEdit [res]
 
-processEdit (GenerateDef upd line name)
+processEdit (GenerateDef upd line name rej)
     = do defs <- get Ctxt
          Just (_, n', _, _) <- findTyDeclAt (\p, n => onLine (line - 1) p)
              | Nothing => pure (EditError ("Can't find declaration for " ++ show name ++ " on line " ++ show line))
@@ -427,7 +430,7 @@ processEdit (GenerateDef upd line name)
                  do let searchdef = makeDef (\p, n => onLine (line - 1) p) n'
                     ropts <- get ROpts
                     put ROpts (record { gdResult = Just (line, searchdef) } ropts)
-                    Just (_, (fc, cs)) <- nextGenDef
+                    Just (_, (fc, cs)) <- nextGenDef rej
                          | Nothing => pure (EditError "No search results")
                     let l : Nat =  integerToNat (cast (snd (startPos fc)))
                     Just srcLine <- getSourceLine line
@@ -440,7 +443,7 @@ processEdit (GenerateDef upd line name)
               Just _ => pure $ EditError "Already defined"
               Nothing => pure $ EditError $ "Can't find declaration for " ++ show name
 processEdit GenerateDefNext
-    = do Just (line, (fc, cs)) <- nextGenDef
+    = do Just (line, (fc, cs)) <- nextGenDef 0
               | Nothing => pure (EditError "No more results")
          let l : Nat =  integerToNat (cast (snd (startPos fc)))
          Just srcLine <- getSourceLine line

src/Idris/Syntax.idr

@@ -386,7 +386,7 @@ data EditCmd : Type where
      AddClause : Bool -> Int -> Name -> EditCmd
      ExprSearch : Bool -> Int -> Name -> List Name -> EditCmd
      ExprSearchNext : EditCmd
-     GenerateDef : Bool -> Int -> Name -> EditCmd
+     GenerateDef : Bool -> Int -> Name -> Nat -> EditCmd
      GenerateDefNext : EditCmd
      MakeLemma : Bool -> Int -> Name -> EditCmd
      MakeCase : Bool -> Int -> Name -> EditCmd

tests/idris2/interactive015/expected

@@ -25,6 +25,8 @@ Main> lappend1 [] ys = ys
 lappend1 (x :: xs) ys = x :: lappend1 xs xs
 Main> lappend1 [] ys = ys
 lappend1 (x :: xs) ys = x :: lappend1 xs ys
+Main> lappend1 [] ys = ys
+lappend1 (x :: xs) ys = x :: lappend1 xs ys
 Main> ys
 Main> []
 Main> lappend2 ys ys

tests/idris2/interactive015/input

@@ -13,6 +13,7 @@
 :gdnext
 :gdnext
 :gdnext
+:gd 13 lappend1 7
 :ps 16 lappend2_rhs_1
 :psnext
 :psnext