Add :psnext and :gdnext at the REPL

These continue the search from :ps and :gd next respectively, giving the
next search result until there are no more results.
Correspondingly, added ':proof-search-next' and ':generate-def-next' in
IDE mode, which continue the search from the previous ':proof-search'
and ':generate-def' respectively.

CHANGELOG.md

@@ -63,6 +63,14 @@ REPL changes:
 * Implemented `:module` command, to load a module during a REPL session.
 * Implemented `:doc`, which displays documentation for a name.
 * Implemented `:browse`, which lists the names exported by a namespace.
+* Added `:psnext`, which continues the previous proof search, looking for the
+  next type correct expression
+  + Correspondingly, added the IDE mode command `proof-search-next` (which takes
+    no arguments)
+* Added `:gdnext`, which continues the previous program search, looking for the
+  next type correct implementation
+  + Correspondingly, added the IDE mode command `generate-def-next` (which takes
+    no arguments)
 
 Changes since Idris 2 v0.1.0
 ----------------------------

src/Idris/IDEMode/Commands.idr

@@ -29,7 +29,9 @@ data IDECommand
      -- deprecated: | AddProofClause
      | AddMissing Integer String
      | ExprSearch Integer String (List String) Bool
+     | ExprSearchNext
      | GenerateDef Integer String
+     | GenerateDefNext
      | MakeLemma Integer String
      | MakeCase Integer String
      | MakeWith Integer String
@@ -150,7 +152,9 @@ putIDECommand (ExprSearch line n exprs mode)  = (SExpList [SymbolAtom "proof-sea
   getMode : Bool -> SExp
   getMode True  = SymbolAtom "all"
   getMode False = SymbolAtom "other"
+putIDECommand ExprSearchNext                  = SymbolAtom "proof-search--next"
 putIDECommand (GenerateDef line n)            = (SExpList [SymbolAtom "generate-def", IntegerAtom line, StringAtom n])
+putIDECommand GenerateDefNext                 = SymbolAtom "generate-def-next"
 putIDECommand (MakeLemma line n)              = (SExpList [SymbolAtom "make-lemma", IntegerAtom line, StringAtom n])
 putIDECommand (MakeCase line n)               = (SExpList [SymbolAtom "make-case", IntegerAtom line, StringAtom n])
 putIDECommand (MakeWith line n)               = (SExpList [SymbolAtom "make-with", IntegerAtom line, StringAtom n])

src/Idris/IDEMode/REPL.idr

@@ -168,9 +168,13 @@ process (AddMissing l n)
          pure $ REPL $ Edited $ DisplayEdit []
 process (ExprSearch l n hs all)
     = replWrap $ Idris.REPL.process (Editing (ExprSearch False (fromInteger l) (UN n)
-                                                 (map UN hs) all))
+                                                 (map UN hs)))
+process ExprSearchNext
+    = replWrap $ Idris.REPL.process (Editing ExprSearchNext)
 process (GenerateDef l n)
-    = replWrap $ Idris.REPL.process (Editing (GenerateDef False (fromInteger l) (UN n) False))
+    = replWrap $ Idris.REPL.process (Editing (GenerateDef False (fromInteger l) (UN n)))
+process GenerateDefNext
+    = replWrap $ Idris.REPL.process (Editing GenerateDefNext)
 process (MakeLemma l n)
     = replWrap $ Idris.REPL.process (Editing (MakeLemma False (fromInteger l) (UN n)))
 process (MakeCase l n)

src/Idris/Parser.idr

@@ -1710,22 +1710,16 @@ editCmd
          upd <- option False (do symbol "!"; pure True)
          line <- intLit
          n <- name
-         pure (ExprSearch upd (fromInteger line) n [] False)
-  <|> do replCmd ["psall"]
-         upd <- option False (do symbol "!"; pure True)
-         line <- intLit
-         n <- name
-         pure (ExprSearch upd (fromInteger line) n [] True)
+         pure (ExprSearch upd (fromInteger line) n [])
+  <|> do replCmd ["psnext"]
+         pure ExprSearchNext
   <|> do replCmd ["gd"]
          upd <- option False (do symbol "!"; pure True)
          line <- intLit
          n <- name
-         pure (GenerateDef upd (fromInteger line) n False)
-  <|> do replCmd ["gdall"]
-         upd <- option False (do symbol "!"; pure True)
-         line <- intLit
-         n <- name
-         pure (GenerateDef upd (fromInteger line) n True)
+         pure (GenerateDef upd (fromInteger line) n)
+  <|> do replCmd ["gdnext"]
+         pure GenerateDefNext
   <|> do replCmd ["ml", "makelemma"]
          upd <- option False (do symbol "!"; pure True)
          line <- intLit

src/Idris/REPL.idr

@@ -293,6 +293,43 @@ addMadeCase lit wapp line content
     addW (S k) acc (x :: xs) = addW k (x :: acc) xs
     addW (S k) acc [] = reverse acc
 
+nextProofSearch : {auto c : Ref Ctxt Defs} ->
+                  {auto u : Ref UST UState} ->
+                  {auto o : Ref ROpts REPLOpts} ->
+                  Core (Maybe (Name, ClosedTerm))
+nextProofSearch
+    = do opts <- get ROpts
+         let Just (n, res) = psResult opts
+              | Nothing => pure Nothing
+         Just (res, next) <- nextResult res
+              | Nothing =>
+                    do put ROpts (record { psResult = Nothing } opts)
+                       pure Nothing
+         put ROpts (record { psResult = Just (n, next) } opts)
+         pure (Just (n, res))
+
+nextGenDef : {auto c : Ref Ctxt Defs} ->
+             {auto u : Ref UST UState} ->
+             {auto o : Ref ROpts REPLOpts} ->
+             Core (Maybe (Int, (FC, List ImpClause)))
+nextGenDef
+    = do opts <- get ROpts
+         let Just (line, res) = gdResult opts
+              | Nothing => pure Nothing
+         Just (res, next) <- nextResult res
+              | Nothing =>
+                    do put ROpts (record { gdResult = Nothing } opts)
+                       pure Nothing
+         put ROpts (record { gdResult = Just (line, next) } opts)
+         pure (Just (line, res))
+
+dropLams : {vars : _} ->
+           Nat -> Env Term vars -> Term vars ->
+           (vars' ** (Env Term vars', Term vars'))
+dropLams Z env tm = (_ ** (env, tm))
+dropLams (S k) env (Bind _ _ b sc) = dropLams k (b :: env) sc
+dropLams _ env tm = (_ ** (env, tm))
+
 processEdit : {auto c : Ref Ctxt Defs} ->
               {auto u : Ref UST UState} ->
               {auto s : Ref Syn SyntaxInfo} ->
@@ -330,30 +367,27 @@ processEdit (AddClause upd line name)
          if upd
             then updateFile (addClause c (integerToNat (cast line)))
             else pure $ DisplayEdit [c]
-processEdit (ExprSearch upd line name hints all)
+processEdit (ExprSearch upd line name hints)
     = do defs <- get Ctxt
          syn <- get Syn
          let brack = elemBy (\x, y => dropNS x == dropNS y) name (bracketholes syn)
          case !(lookupDefName name (gamma defs)) of
               [(n, nidx, Hole locs _)] =>
-                  do tms <- exprSearchN replFC (if all then 20 else 1) name []
+                  do let searchtm = exprSearch replFC name []
+                     ropts <- get ROpts
+                     put ROpts (record { psResult = Just (name, searchtm) } ropts)
                      defs <- get Ctxt
-                     restms <- traverse (normaliseHoles defs []) tms
-                     itms <- the (Core (List PTerm))
-                               (traverse (\tm =>
-                                           do let (_ ** (env, tm')) = dropLams locs [] tm
-                                              resugar env tm') restms)
-                     if all
-                        then pure $ DisplayEdit (map show itms)
-                        else case itms of
-                                  [] => pure $ EditError "No search results"
-                                  (x :: xs) =>
-                                     let res = show (the PTerm (if brack
-                                                        then addBracket replFC x
-                                                        else x)) in
-                                       if upd
-                                          then updateFile (proofSearch name res (integerToNat (cast (line - 1))))
-                                          else pure $ DisplayEdit [res]
+                     Just (_, tm) <- nextProofSearch
+                          | Nothing => pure $ EditError "No search results"
+                     restm <- normaliseHoles defs [] tm
+                     let (_ ** (env, tm')) = dropLams locs [] restm
+                     itm <- resugar env tm'
+                     let res = show (the PTerm (if brack
+                                                   then addBracket replFC itm
+                                                   else itm))
+                     if upd
+                        then updateFile (proofSearch name res (integerToNat (cast (line - 1))))
+                        else pure $ DisplayEdit [res]
               [(n, nidx, PMDef pi [] (STerm _ tm) _ _)] =>
                   case holeInfo pi of
                        NotHole => pure $ EditError "Not a searchable hole"
@@ -368,43 +402,52 @@ processEdit (ExprSearch upd line name hints all)
                                 else pure $ DisplayEdit [res]
               [] => pure $ EditError $ "Unknown name " ++ show name
               _ => pure $ EditError "Not a searchable hole"
-  where
-    dropLams : {vars : _} ->
-               Nat -> Env Term vars -> Term vars ->
-               (vars' ** (Env Term vars', Term vars'))
-    dropLams Z env tm = (_ ** (env, tm))
-    dropLams (S k) env (Bind _ _ b sc) = dropLams k (b :: env) sc
-    dropLams _ env tm = (_ ** (env, tm))
-processEdit (GenerateDef upd line name all)
+processEdit ExprSearchNext
+    = do defs <- get Ctxt
+         syn <- get Syn
+         Just (name, tm) <- nextProofSearch
+              | Nothing => pure $ EditError "No more results"
+         [(n, nidx, Hole locs _)] <- lookupDefName name (gamma defs)
+              | _ => pure $ EditError "Not a searchable hole"
+         let brack = elemBy (\x, y => dropNS x == dropNS y) name (bracketholes syn)
+         restm <- normaliseHoles defs [] tm
+         let (_ ** (env, tm')) = dropLams locs [] restm
+         itm <- resugar env tm'
+         let res = show (the PTerm (if brack
+                                       then addBracket replFC itm
+                                       else itm))
+         pure $ DisplayEdit [res]
+
+processEdit (GenerateDef upd line name)
     = 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))
          case !(lookupDefExact n' (gamma defs)) of
               Just None =>
-                  handleUnify
-                    (do progs <- makeDefN (\p, n => onLine (line - 1) p)
-                                          (if all then 20 else 1)
-                                          n'
-                        Just srcLine <- getSourceLine line
-                           | Nothing => pure (EditError "Source line not found")
-                        let (markM, srcLineUnlit) = isLitLine srcLine
-                        if all
-                           then do ls <- traverse (\ (fc, cs) =>
-                                              do let l : Nat =  integerToNat (cast (snd (startPos fc)))
-                                                 res <- traverse (printClause markM l) cs
-                                                 pure (res ++ ["----"])) progs
-                                   pure $ DisplayEdit (concat ls)
-                           else case progs of
-                                     [] => pure (EditError "No search results")
-                                     ((fc, cs) :: _) =>
-                                        do let l : Nat =  integerToNat (cast (snd (startPos fc)))
-                                           ls <- traverse (printClause markM l) cs
-                                           if upd
-                                              then updateFile (addClause (unlines ls) (integerToNat (cast line)))
-                                              else pure $ DisplayEdit ls)
-                    (\err => pure $ EditError $ "Can't find a definition for " ++ show n' ++ ": " ++ show err)
+                 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
+                         | Nothing => pure (EditError "No search results")
+                    let l : Nat =  integerToNat (cast (snd (startPos fc)))
+                    Just srcLine <- getSourceLine line
+                       | Nothing => pure (EditError "Source line not found")
+                    let (markM, srcLineUnlit) = isLitLine srcLine
+                    ls <- traverse (printClause markM l) cs
+                    if upd
+                       then updateFile (addClause (unlines ls) (integerToNat (cast line)))
+                       else pure $ DisplayEdit ls
               Just _ => pure $ EditError "Already defined"
               Nothing => pure $ EditError $ "Can't find declaration for " ++ show name
+processEdit GenerateDefNext
+    = do Just (line, (fc, cs)) <- nextGenDef
+              | Nothing => pure (EditError "No more results")
+         let l : Nat =  integerToNat (cast (snd (startPos fc)))
+         Just srcLine <- getSourceLine line
+            | Nothing => pure (EditError "Source line not found")
+         let (markM, srcLineUnlit) = isLitLine srcLine
+         ls <- traverse (printClause markM l) cs
+         pure $ DisplayEdit ls
 processEdit (MakeLemma upd line name)
     = do defs <- get Ctxt
          syn <- get Syn
@@ -550,6 +593,7 @@ loadMainFile f
          errs <- logTime "Build deps" $ buildDeps f
          updateErrorLine errs
          setSource res
+         resetProofState
          case errs of
            [] => pure (FileLoaded f)
            _ => pure (ErrorsBuildingFile f errs)

src/Idris/REPLOpts.idr

@@ -3,6 +3,8 @@ module Idris.REPLOpts
 import Compiler.Common
 import Idris.Syntax
 import Parser.Unlit
+import TTImp.Interactive.ExprSearch
+import TTImp.TTImp
 
 import Data.List
 import Data.Strings
@@ -27,15 +29,17 @@ record REPLOpts where
   errorLine : Maybe Int
   idemode : OutputMode
   currentElabSource : String
+  psResult : Maybe (Name, Core (Search ClosedTerm)) -- last proof search continuation (and name)
+  gdResult : Maybe (Int, Core (Search (FC, List ImpClause))) -- last generate def continuation (and line number)
   -- TODO: Move extraCodegens from here, it doesn't belong, but there's nowhere
   -- better to stick it now.
   extraCodegens : List (String, Codegen)
 
-
 export
 defaultOpts : Maybe String -> OutputMode -> List (String, Codegen) -> REPLOpts
 defaultOpts fname outmode cgs
-    = MkREPLOpts False NormaliseAll fname (litStyle fname) "" "vim" Nothing outmode "" cgs
+    = MkREPLOpts False NormaliseAll fname (litStyle fname) "" "vim"
+                 Nothing outmode "" Nothing Nothing cgs
   where
     litStyle : Maybe String -> Maybe LiterateStyle
     litStyle Nothing = Nothing
@@ -72,6 +76,14 @@ setMainFile src
     litStyle Nothing = Nothing
     litStyle (Just fn) = isLitFile fn
 
+export
+resetProofState : {auto o : Ref ROpts REPLOpts} ->
+                  Core ()
+resetProofState
+    = do opts <- get ROpts
+         put ROpts (record { psResult = Nothing,
+                             gdResult = Nothing } opts)
+
 export
 setSource : {auto o : Ref ROpts REPLOpts} ->
             String -> Core ()

src/Idris/Syntax.idr

@@ -384,8 +384,10 @@ data EditCmd : Type where
      TypeAt : Int -> Int -> Name -> EditCmd
      CaseSplit : Bool -> Int -> Int -> Name -> EditCmd
      AddClause : Bool -> Int -> Name -> EditCmd
-     ExprSearch : Bool -> Int -> Name -> List Name -> Bool -> EditCmd
-     GenerateDef : Bool -> Int -> Name -> Bool -> EditCmd
+     ExprSearch : Bool -> Int -> Name -> List Name -> EditCmd
+     ExprSearchNext : EditCmd
+     GenerateDef : Bool -> Int -> Name -> EditCmd
+     GenerateDefNext : EditCmd
      MakeLemma : Bool -> Int -> Name -> EditCmd
      MakeCase : Bool -> Int -> Name -> EditCmd
      MakeWith : Bool -> Int -> Name -> EditCmd

src/TTImp/Interactive/ExprSearch.idr

@@ -87,13 +87,11 @@ filterS p (Result r next)
 
 export
 searchN : {auto c : Ref Ctxt Defs} ->
-          {auto m : Ref MD Metadata} ->
           {auto u : Ref UST UState} ->
           Nat -> Core (Search a) -> Core (List a)
 searchN max s
     = tryUnify
-         (do foo <- getNextEntry
-             res <- s
+         (do res <- s
              xs <- count max res
              pure xs)
          (pure [])
@@ -104,6 +102,17 @@ searchN max s
     count (S Z) (Result a next) = pure [a]
     count (S k) (Result a next) = pure $ a :: !(count k !next)
 
+export
+nextResult : {auto c : Ref Ctxt Defs} ->
+             {auto u : Ref UST UState} ->
+             Core (Search a) -> Core (Maybe (a, Core (Search a)))
+nextResult s
+    = tryUnify
+         (do res <- s
+             case res of
+                  NoMore => pure Nothing
+                  Result r next => pure (Just (r, next)))
+         (pure Nothing)
 
 search : {auto c : Ref Ctxt Defs} ->
          {auto m : Ref MD Metadata} ->

tests/Main.idr

@@ -57,7 +57,7 @@ idrisTests
        "interactive001", "interactive002", "interactive003", "interactive004",
        "interactive005", "interactive006", "interactive007", "interactive008",
        "interactive009", "interactive010", "interactive011", "interactive012",
-       "interactive013", "interactive014",
+       "interactive013", "interactive014", "interactive015",
        -- Interfaces
        "interface001", "interface002", "interface003", "interface004",
        "interface005", "interface006", "interface007", "interface008",

tests/idris2/interactive015/IEdit.idr

@@ -0,0 +1,17 @@
+data Vect : Nat -> Type -> Type where
+     Nil : Vect Z a
+     (::) : a -> Vect k a -> Vect (S k) a
+
+%name Vect xs, ys, zs
+
+my_cong : forall f . (x : a) -> (y : a) -> x = y -> f x = f y
+
+append : Vect n a -> Vect m a -> Vect (n + m) a
+
+lappend : (1 _ : List a) -> (1 _ : List a) -> List a
+
+lappend1 : List a -> List a -> List a
+
+lappend2 : List a -> List a -> List a
+lappend2 [] ys = ?lappend2_rhs_1
+lappend2 (x :: xs) ys = ?lappend2_rhs_2

tests/idris2/interactive015/expected

@@ -0,0 +1,33 @@
+1/1: Building IEdit (IEdit.idr)
+Main> my_cong x x Refl = Refl
+Main> No more results
+Main> append [] ys = ys
+append (x :: xs) ys = x :: append xs ys
+Main> append [] ys = ys
+append (x :: xs) [] = x :: append xs []
+append (x :: xs) (y :: ys) = x :: append xs (x :: ys)
+Main> lappend [] ys = ys
+lappend (x :: xs) ys = x :: lappend xs ys
+Main> lappend [] ys = ys
+lappend (x :: xs) ys = x :: lappend ys xs
+Main> lappend [] ys = ys
+lappend (x :: xs) ys = lappend xs (x :: ys)
+Main> lappend1 xs ys = ys
+Main> lappend1 xs ys = xs
+Main> lappend1 xs ys = []
+Main> lappend1 [] ys = ys
+lappend1 (x :: xs) ys = xs
+Main> lappend1 [] ys = ys
+lappend1 (x :: xs) ys = ys
+Main> lappend1 [] ys = ys
+lappend1 (x :: xs) ys = []
+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> ys
+Main> []
+Main> lappend2 ys ys
+Main> lappend2 ys []
+Main> lappend2 [] ys
+Main> Bye for now!

tests/idris2/interactive015/input

@@ -0,0 +1,21 @@
+:gd 7 my_cong
+:gdnext
+:gd 9 append
+:gdnext
+:gd 11 lappend
+:gdnext
+:gdnext
+:gd 13 lappend1
+:gdnext
+:gdnext
+:gdnext
+:gdnext
+:gdnext
+:gdnext
+:gdnext
+:ps 16 lappend2_rhs_1
+:psnext
+:psnext
+:psnext
+:psnext
+:q

tests/idris2/interactive015/run

@@ -0,0 +1,3 @@
+$1 --no-banner IEdit.idr < input
+
+rm -rf build