[ new ] Add a GenerateDefNext code action

src/Language/LSP/CodeAction.idr

@@ -5,6 +5,7 @@ data IdrisAction
   = CaseSplit
   | ExprSearch
   | GenerateDef
+  | GenerateDefNext
   | MakeCase
   | MakeClause
   | MakeLemma
@@ -14,25 +15,27 @@ data IdrisAction
 
 export
 Eq IdrisAction where
-  CaseSplit   == CaseSplit   = True
-  ExprSearch  == ExprSearch  = True
-  GenerateDef == GenerateDef = True
-  MakeCase    == MakeCase    = True
-  MakeClause  == MakeClause  = True
-  MakeLemma   == MakeLemma   = True
-  MakeWith    == MakeWith    = True
-  RefineHole  == RefineHole  = True
-  Intro       == Intro       = True
+  CaseSplit       == CaseSplit   = True
+  ExprSearch      == ExprSearch  = True
+  GenerateDef     == GenerateDef = True
+  GenerateDefNext == GenerateDefNext = True
+  MakeCase        == MakeCase    = True
+  MakeClause      == MakeClause  = True
+  MakeLemma       == MakeLemma   = True
+  MakeWith        == MakeWith    = True
+  RefineHole      == RefineHole  = True
+  Intro           == Intro       = True
   _ == _ = False
 
 export
 Show IdrisAction where
-  show CaseSplit   = "CaseSplit"
-  show ExprSearch  = "ExprSearch"
-  show GenerateDef = "GenerateDef"
-  show MakeCase    = "MakeCase"
-  show MakeClause  = "MakeClause"
-  show MakeLemma   = "MakeLemma"
-  show MakeWith    = "MakeWith"
-  show RefineHole  = "RefineHole"
-  show Intro       = "Intro"
+  show CaseSplit       = "CaseSplit"
+  show ExprSearch      = "ExprSearch"
+  show GenerateDef     = "GenerateDef"
+  show GenerateDefNext = "GenerateDefNext"
+  show MakeCase        = "MakeCase"
+  show MakeClause      = "MakeClause"
+  show MakeLemma       = "MakeLemma"
+  show MakeWith        = "MakeWith"
+  show RefineHole      = "RefineHole"
+  show Intro           = "Intro"

src/Language/LSP/CodeAction/GenerateDef.idr

@@ -22,31 +22,6 @@ import TTImp.Interactive.GenerateDef
 import TTImp.TTImp
 import TTImp.TTImp.Functor
 
-printClause : Ref Ctxt Defs
-           => Ref Syn SyntaxInfo
-           => Maybe String -> Nat -> ImpClause -> Core String
-printClause l i (PatClause _ lhsraw rhsraw) = do
-  lhs <- pterm $ map defaultKindedName lhsraw
-  rhs <- pterm $ map defaultKindedName rhsraw
-  pure $ relit l "\{pack (replicate i ' ')}\{show lhs} = \{show rhs}"
-printClause l i (WithClause _ lhsraw rig wvraw prf flags csraw) = do
-  lhs <- pterm $ map defaultKindedName lhsraw
-  wval <- pterm $ map defaultKindedName wvraw
-  cs <- traverse (printClause l (i + 2)) csraw
-  pure (relit l ((pack (replicate i ' ')
-         ++ show lhs
-         ++ " with \{showCount rig}(" ++ show wval ++ ")"
-         ++ maybe "" (\ nm => " proof " ++ show nm) prf
-         ++ "\n"))
-         ++ showSep "\n" cs)
-printClause l i (ImpossibleClause _ lhsraw) = do
-  do lhs <- pterm $ map defaultKindedName lhsraw
-     pure $ relit l "\{pack (replicate i ' ')}\{show lhs} impossible"
-
-number : Nat -> List a -> List (Nat, a)
-number n [] = []
-number n (x :: xs) = (n, x) :: number (S n) xs
-
 generateDefKind : CodeActionKind
 generateDefKind = Other "refactor.rewrite.GenerateDef"
 

src/Language/LSP/CodeAction/GenerateDefNext.idr

@@ -0,0 +1,152 @@
+module Language.LSP.CodeAction.GenerateDefNext
+
+import Core.Context
+import Core.Core
+import Core.Env
+import Core.Metadata
+import Core.UnifyState
+import Data.String
+import Idris.REPL.Opts
+import Idris.Resugar
+import Idris.Syntax
+import Language.JSON
+import Language.LSP.CodeAction
+import Language.LSP.CodeAction.Utils
+import Language.LSP.Message
+import Language.LSP.Utils
+import Parser.Unlit
+import Server.Configuration
+import Server.Log
+import Server.Utils
+import Libraries.Data.Tap
+import TTImp.Interactive.GenerateDef
+import TTImp.Interactive.ExprSearch
+import TTImp.TTImp
+import TTImp.TTImp.Functor
+
+generateDefNextKind : CodeActionKind
+generateDefNextKind = Other "refactor.rewrite.GenerateDefNext"
+
+isAllowed : CodeActionParams -> Bool
+isAllowed params =
+  maybe True (\filter => (generateDefNextKind `elem` filter) || (RefactorRewrite `elem` filter)) params.context.only
+
+buildCodeAction : URI -> TextEdit -> CodeAction
+buildCodeAction uri edit =
+  MkCodeAction
+    { title       = "Generate next definition"
+    , kind        = Just RefactorRewrite
+    , diagnostics = Nothing
+    , isPreferred = Nothing
+    , disabled    = Nothing
+    , edit        = Just $ MkWorkspaceEdit
+        { changes           = Just (singleton uri [edit])
+        , documentChanges   = Nothing
+        , changeAnnotations = Nothing
+        }
+    , command     = Nothing
+    , data_       = Nothing
+    }
+
+-- first blank line going forward (in contrast to reversed implementation found in
+-- some other code actions.
+findBlankLine : List String -> Int -> Int
+findBlankLine [] acc = acc
+findBlankLine (x :: xs) acc = if trim x == "" then acc else findBlankLine xs (acc + 1)
+
+-- reproduced from compiler repo because it is not exported there (as of now)
+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 reject
+    = do opts <- get ROpts
+         let Just (line, res) = gdResult opts
+              | Nothing => pure Nothing
+         Just (res, next) <- nextResult res
+              | Nothing =>
+                    do put ROpts ({ gdResult := Nothing } opts)
+                       pure Nothing
+         put ROpts ({ gdResult := Just (line, next) } opts)
+         case reject of
+              Z => pure (Just (line, res))
+              S k => nextGenDef k
+
+export
+generateDefNext : Ref LSPConf LSPConfiguration
+               => Ref MD Metadata
+               => Ref Ctxt Defs
+               => Ref UST UState
+               => Ref Syn SyntaxInfo
+               => Ref ROpts REPLOpts
+               => CodeActionParams -> Core (List CodeAction)
+generateDefNext params = do
+  let True = isAllowed params
+    | False => logI GenerateDefNext "Skipped" >> pure []
+  logI GenerateDefNext "Checking for \{show params.textDocument.uri} at \{show params.range}"
+
+  withSingleLine GenerateDefNext params (pure []) $ \line => do
+    withMultipleCache GenerateDefNext params GenerateDefNext $ do
+      defs <- branch
+      Just (loc, n, _, _) <- findTyDeclAt (\p, n => onLine line p)
+        | Nothing => logD GenerateDef "No name found at line \{show line}" >> pure []
+      logD CaseSplit "Found type declaration \{show n}"
+
+      previousResults <- gdResult <$> get ROpts
+      let staleDefs = case previousResults of
+                           Nothing => True
+                           Just (l, _) => l /= line
+      when staleDefs $ do
+        fuel <- gets LSPConf searchLimit
+        existingDef <- lookupDefExact n defs.gamma
+        case existingDef of
+          Just None => do
+             catch (do searchdefs <- makeDefSort (\p, n => onLine line p) fuel mostUsed n
+                       update ROpts { gdResult := Just (line, pure searchdefs) }
+                       pure ())
+                   (\case Timeout _ => logI GenerateDefNext "Timed out" >> pure ()
+                          err => logC GenerateDefNext "Unexpected error while searching" >> throw err)
+          Just _ => logD GenerateDefNext "There is already a definition for \{show n}" >> pure ()
+          Nothing => logD GenerateDefNext "Couldn't find type declaration at line \{show line}" >> pure ()
+
+      Just (line', (fc, cs)) <- nextGenDef 0
+        | Nothing => logD GenerateDefNext "No more results" >> pure []
+      let l : Nat = integerToNat $ cast $ startCol (toNonEmptyFC fc)
+      Just srcLine <- getSourceLine line'
+        | Nothing => logE GenerateDefNext "Source line \{show line} not found" >> pure []
+      let (markM, srcLineUnlit) = isLitLine srcLine
+      lines <- traverse (printClause markM l) cs
+
+      put Ctxt defs
+
+      let newLine = endLine loc + 1
+
+      -- Not having an easy time figuring out how to determine how many
+      -- following lines should be replaced if there's a definition there
+      -- already (cycling defs and not on first one). probably just use
+      -- whitespace.
+      defToOverride <- lookupDefExact n defs.gamma
+      rng <- case defToOverride of
+           Nothing => do
+             logD GenerateDefNext "No def to override, inserting new def" 
+             pure $ MkRange (MkPosition newLine 0) (MkPosition newLine 0) -- insert
+           (Just None) => do
+             logD GenerateDefNext "No def to override, inserting new def" 
+             pure $ MkRange (MkPosition newLine 0) (MkPosition newLine 0) -- insert
+           (Just (PMDef pminfo args treeCT treeRT pats)) => do
+             src <- String.lines <$> getSource
+             let srcFromDef = drop (integerToNat (cast line)) src
+             let blank = findBlankLine srcFromDef line
+             pure $ MkRange (MkPosition newLine 0) (MkPosition blank 0) -- replace
+           (Just _) => do
+             logE GenerateDefNext "UNEXPECTED"
+             pure $ MkRange (MkPosition newLine 0) (MkPosition newLine 0) -- insert
+
+      let docURI = params.textDocument.uri
+
+      action <- do
+        let edit = MkTextEdit rng (String.unlines lines)
+        pure $ buildCodeAction docURI edit
+      -- TODO: retrieve the line length efficiently
+      pure [(MkRange (MkPosition line 0) (MkPosition line 1000), [action])]

src/Language/LSP/CodeAction/Utils.idr

@@ -1,13 +1,19 @@
 module Language.LSP.CodeAction.Utils
 
-import Core.Core
+import Core.Context
 import Core.Context.Context
+import Core.Core
+import Idris.Resugar
+import Idris.Syntax
 import Language.LSP.CodeAction
 import Language.LSP.Message.CodeAction
 import Language.LSP.Message.Location
+import Parser.Unlit
 import Server.Configuration
 import Server.Log
 import Server.Utils
+import TTImp.TTImp
+import TTImp.TTImp.Functor
 
 ||| Check for code actions that require the request to be on a single line.
 ||| @topic Logging topic of the code action
@@ -70,3 +76,33 @@ withMultipleCache topic params action new =
                 pure $ concat $ snd <$> locs
        acts => do logD topic "Found cached action"
                   pure acts
+
+||| Pretty print a clause as source-code to be sent to the editor.
+||| Reproduced from compiler repo where this function is not exported.
+export
+printClause : Ref Ctxt Defs
+           => Ref Syn SyntaxInfo
+           => Maybe String -> Nat -> ImpClause -> Core String
+printClause l i (PatClause _ lhsraw rhsraw) = do
+  lhs <- pterm $ map defaultKindedName lhsraw
+  rhs <- pterm $ map defaultKindedName rhsraw
+  pure $ relit l "\{pack (replicate i ' ')}\{show lhs} = \{show rhs}"
+printClause l i (WithClause _ lhsraw rig wvraw prf flags csraw) = do
+  lhs <- pterm $ map defaultKindedName lhsraw
+  wval <- pterm $ map defaultKindedName wvraw
+  cs <- traverse (printClause l (i + 2)) csraw
+  pure (relit l ((pack (replicate i ' ')
+         ++ show lhs
+         ++ " with \{showCount rig}(" ++ show wval ++ ")"
+         ++ maybe "" (\ nm => " proof " ++ show nm) prf
+         ++ "\n"))
+         ++ showSep "\n" cs)
+printClause l i (ImpossibleClause _ lhsraw) = do
+  do lhs <- pterm $ map defaultKindedName lhsraw
+     pure $ relit l "\{pack (replicate i ' ')}\{show lhs} impossible"
+
+||| Zip some lines up with their indices starting at the given number.
+export
+number : Nat -> List a -> List (Nat, a)
+number n [] = []
+number n (x :: xs) = (n, x) :: number (S n) xs

src/Server/Log.idr

@@ -29,6 +29,7 @@ data Topic
   | DocumentSymbol
   | ExprSearch
   | GenerateDef
+  | GenerateDefNext
   | GotoDefinition
   | Hover
   | Intro
@@ -56,6 +57,7 @@ Show Topic where
   show DocumentSymbol = "Request.DocumentSymbol"
   show ExprSearch = "Request.CodeAction.ExprSearch"
   show GenerateDef = "Request.CodeAction.GenerateDef"
+  show GenerateDefNext = "Request.CodeAction.GenerateDefNext"
   show GotoDefinition = "Request.GotoDefinition"
   show Hover = "Request.Hover"
   show Intro = "Request.CodeAction.Intro"

src/Server/ProcessMessage.idr

@@ -35,6 +35,7 @@ import Language.LSP.CodeAction.AddClause
 import Language.LSP.CodeAction.CaseSplit
 import Language.LSP.CodeAction.ExprSearch
 import Language.LSP.CodeAction.GenerateDef
+import Language.LSP.CodeAction.GenerateDefNext
 import Language.LSP.CodeAction.Intro
 import Language.LSP.CodeAction.MakeCase
 import Language.LSP.CodeAction.MakeLemma
@@ -249,7 +250,6 @@ loadURI conf uri version = do
     put MD (initMetadata (PhysicalIdrSrc modIdent))
     ignore $ ProcessIdr.process msgPrefix buildMsg fname modIdent
 
-  resetProofState
   let caps = (publishDiagnostics <=< textDocument) . capabilities $ conf
   update LSPConf ({ quickfixes := [], cachedActions := empty, cachedHovers := empty })
   traverse_ (findQuickfix caps uri) errs
@@ -440,9 +440,10 @@ handleRequest TextDocumentCodeAction params = whenActiveRequest $ \conf => do
         makeCaseAction <- makeCase params
         introActions <- map Just <$> intro params
         generateDefActions <- map Just <$> generateDef params
+        generateDefNextActions <- map Just <$> generateDefNext params
         let resp = flatten $ quickfixActions
                                ++ [splitAction, lemmaAction, withAction, clauseAction, makeCaseAction]
-                               ++ introActions ++ generateDefActions ++ exprSearchActions
+                               ++ introActions ++ generateDefActions ++ generateDefNextActions ++ exprSearchActions
         pure $ pure $ make resp)
     where
       flatten : List (Maybe CodeAction) -> List (OneOf [Command, CodeAction])