Skip to content

Commit 4ec24c8

Browse files
mattpolzinmattpolzin
authored
[ new ] Add a GenerateDefNext code action (idris-community#226)
1 parent 81e70d4 commit 4ec24c8

File tree

7 files changed

+216
-47
lines changed

7 files changed

+216
-47
lines changed

‎Idris2‎

Submodule Idris2 updated 107 files

‎src/Language/LSP/CodeAction.idr‎

Lines changed: 21 additions & 18 deletions
Original file line numberDiff line numberDiff line change
@@ -5,6 +5,7 @@ data IdrisAction
55
= CaseSplit
66
| ExprSearch
77
| GenerateDef
8+
| GenerateDefNext
89
| MakeCase
910
| MakeClause
1011
| MakeLemma
@@ -14,25 +15,27 @@ data IdrisAction
1415

1516
export
1617
Eq IdrisAction where
17-
CaseSplit == CaseSplit = True
18-
ExprSearch == ExprSearch = True
19-
GenerateDef == GenerateDef = True
20-
MakeCase == MakeCase = True
21-
MakeClause == MakeClause = True
22-
MakeLemma == MakeLemma = True
23-
MakeWith == MakeWith = True
24-
RefineHole == RefineHole = True
25-
Intro == Intro = True
18+
CaseSplit == CaseSplit = True
19+
ExprSearch == ExprSearch = True
20+
GenerateDef == GenerateDef = True
21+
GenerateDefNext == GenerateDefNext = True
22+
MakeCase == MakeCase = True
23+
MakeClause == MakeClause = True
24+
MakeLemma == MakeLemma = True
25+
MakeWith == MakeWith = True
26+
RefineHole == RefineHole = True
27+
Intro == Intro = True
2628
_ == _ = False
2729

2830
export
2931
Show IdrisAction where
30-
show CaseSplit = "CaseSplit"
31-
show ExprSearch = "ExprSearch"
32-
show GenerateDef = "GenerateDef"
33-
show MakeCase = "MakeCase"
34-
show MakeClause = "MakeClause"
35-
show MakeLemma = "MakeLemma"
36-
show MakeWith = "MakeWith"
37-
show RefineHole = "RefineHole"
38-
show Intro = "Intro"
32+
show CaseSplit = "CaseSplit"
33+
show ExprSearch = "ExprSearch"
34+
show GenerateDef = "GenerateDef"
35+
show GenerateDefNext = "GenerateDefNext"
36+
show MakeCase = "MakeCase"
37+
show MakeClause = "MakeClause"
38+
show MakeLemma = "MakeLemma"
39+
show MakeWith = "MakeWith"
40+
show RefineHole = "RefineHole"
41+
show Intro = "Intro"

‎src/Language/LSP/CodeAction/GenerateDef.idr‎

Lines changed: 0 additions & 25 deletions
Original file line numberDiff line numberDiff line change
@@ -22,31 +22,6 @@ import TTImp.Interactive.GenerateDef
2222
import TTImp.TTImp
2323
import TTImp.TTImp.Functor
2424

25-
printClause : Ref Ctxt Defs
26-
=> Ref Syn SyntaxInfo
27-
=> Maybe String -> Nat -> ImpClause -> Core String
28-
printClause l i (PatClause _ lhsraw rhsraw) = do
29-
lhs <- pterm $ map defaultKindedName lhsraw
30-
rhs <- pterm $ map defaultKindedName rhsraw
31-
pure $ relit l "\{pack (replicate i ' ')}\{show lhs} = \{show rhs}"
32-
printClause l i (WithClause _ lhsraw rig wvraw prf flags csraw) = do
33-
lhs <- pterm $ map defaultKindedName lhsraw
34-
wval <- pterm $ map defaultKindedName wvraw
35-
cs <- traverse (printClause l (i + 2)) csraw
36-
pure (relit l ((pack (replicate i ' ')
37-
++ show lhs
38-
++ " with \{showCount rig}(" ++ show wval ++ ")"
39-
++ maybe "" (\ nm => " proof " ++ show nm) prf
40-
++ "\n"))
41-
++ showSep "\n" cs)
42-
printClause l i (ImpossibleClause _ lhsraw) = do
43-
do lhs <- pterm $ map defaultKindedName lhsraw
44-
pure $ relit l "\{pack (replicate i ' ')}\{show lhs} impossible"
45-
46-
number : Nat -> List a -> List (Nat, a)
47-
number n [] = []
48-
number n (x :: xs) = (n, x) :: number (S n) xs
49-
5025
generateDefKind : CodeActionKind
5126
generateDefKind = Other "refactor.rewrite.GenerateDef"
5227

‎src/Language/LSP/CodeAction/GenerateDefNext.idr‎

Lines changed: 152 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,152 @@
1+
module Language.LSP.CodeAction.GenerateDefNext
2+
3+
import Core.Context
4+
import Core.Core
5+
import Core.Env
6+
import Core.Metadata
7+
import Core.UnifyState
8+
import Data.String
9+
import Idris.REPL.Opts
10+
import Idris.Resugar
11+
import Idris.Syntax
12+
import Language.JSON
13+
import Language.LSP.CodeAction
14+
import Language.LSP.CodeAction.Utils
15+
import Language.LSP.Message
16+
import Language.LSP.Utils
17+
import Parser.Unlit
18+
import Server.Configuration
19+
import Server.Log
20+
import Server.Utils
21+
import Libraries.Data.Tap
22+
import TTImp.Interactive.GenerateDef
23+
import TTImp.Interactive.ExprSearch
24+
import TTImp.TTImp
25+
import TTImp.TTImp.Functor
26+
27+
generateDefNextKind : CodeActionKind
28+
generateDefNextKind = Other "refactor.rewrite.GenerateDefNext"
29+
30+
isAllowed : CodeActionParams -> Bool
31+
isAllowed params =
32+
maybe True (\filter => (generateDefNextKind `elem` filter) || (RefactorRewrite `elem` filter)) params.context.only
33+
34+
buildCodeAction : URI -> TextEdit -> CodeAction
35+
buildCodeAction uri edit =
36+
MkCodeAction
37+
{ title = "Generate next definition"
38+
, kind = Just RefactorRewrite
39+
, diagnostics = Nothing
40+
, isPreferred = Nothing
41+
, disabled = Nothing
42+
, edit = Just $ MkWorkspaceEdit
43+
{ changes = Just (singleton uri [edit])
44+
, documentChanges = Nothing
45+
, changeAnnotations = Nothing
46+
}
47+
, command = Nothing
48+
, data_ = Nothing
49+
}
50+
51+
-- first blank line going forward (in contrast to reversed implementation found in
52+
-- some other code actions.
53+
findBlankLine : List String -> Int -> Int
54+
findBlankLine [] acc = acc
55+
findBlankLine (x :: xs) acc = if trim x == "" then acc else findBlankLine xs (acc + 1)
56+
57+
-- reproduced from compiler repo because it is not exported there (as of now)
58+
nextGenDef : {auto c : Ref Ctxt Defs} ->
59+
{auto u : Ref UST UState} ->
60+
{auto o : Ref ROpts REPLOpts} ->
61+
(reject : Nat) ->
62+
Core (Maybe (Int, (FC, List ImpClause)))
63+
nextGenDef reject
64+
= do opts <- get ROpts
65+
let Just (line, res) = gdResult opts
66+
| Nothing => pure Nothing
67+
Just (res, next) <- nextResult res
68+
| Nothing =>
69+
do put ROpts ({ gdResult := Nothing } opts)
70+
pure Nothing
71+
put ROpts ({ gdResult := Just (line, next) } opts)
72+
case reject of
73+
Z => pure (Just (line, res))
74+
S k => nextGenDef k
75+
76+
export
77+
generateDefNext : Ref LSPConf LSPConfiguration
78+
=> Ref MD Metadata
79+
=> Ref Ctxt Defs
80+
=> Ref UST UState
81+
=> Ref Syn SyntaxInfo
82+
=> Ref ROpts REPLOpts
83+
=> CodeActionParams -> Core (List CodeAction)
84+
generateDefNext params = do
85+
let True = isAllowed params
86+
| False => logI GenerateDefNext "Skipped" >> pure []
87+
logI GenerateDefNext "Checking for \{show params.textDocument.uri} at \{show params.range}"
88+
89+
withSingleLine GenerateDefNext params (pure []) $ \line => do
90+
withMultipleCache GenerateDefNext params GenerateDefNext $ do
91+
defs <- branch
92+
Just (loc, n, _, _) <- findTyDeclAt (\p, n => onLine line p)
93+
| Nothing => logD GenerateDef "No name found at line \{show line}" >> pure []
94+
logD CaseSplit "Found type declaration \{show n}"
95+
96+
previousResults <- gdResult <$> get ROpts
97+
let staleDefs = case previousResults of
98+
Nothing => True
99+
Just (l, _) => l /= line
100+
when staleDefs $ do
101+
fuel <- gets LSPConf searchLimit
102+
existingDef <- lookupDefExact n defs.gamma
103+
case existingDef of
104+
Just None => do
105+
catch (do searchdefs <- makeDefSort (\p, n => onLine line p) fuel mostUsed n
106+
update ROpts { gdResult := Just (line, pure searchdefs) }
107+
pure ())
108+
(\case Timeout _ => logI GenerateDefNext "Timed out" >> pure ()
109+
err => logC GenerateDefNext "Unexpected error while searching" >> throw err)
110+
Just _ => logD GenerateDefNext "There is already a definition for \{show n}" >> pure ()
111+
Nothing => logD GenerateDefNext "Couldn't find type declaration at line \{show line}" >> pure ()
112+
113+
Just (line', (fc, cs)) <- nextGenDef 0
114+
| Nothing => logD GenerateDefNext "No more results" >> pure []
115+
let l : Nat = integerToNat $ cast $ startCol (toNonEmptyFC fc)
116+
Just srcLine <- getSourceLine line'
117+
| Nothing => logE GenerateDefNext "Source line \{show line} not found" >> pure []
118+
let (markM, srcLineUnlit) = isLitLine srcLine
119+
lines <- traverse (printClause markM l) cs
120+
121+
put Ctxt defs
122+
123+
let newLine = endLine loc + 1
124+
125+
-- Not having an easy time figuring out how to determine how many
126+
-- following lines should be replaced if there's a definition there
127+
-- already (cycling defs and not on first one). probably just use
128+
-- whitespace.
129+
defToOverride <- lookupDefExact n defs.gamma
130+
rng <- case defToOverride of
131+
Nothing => do
132+
logD GenerateDefNext "No def to override, inserting new def"
133+
pure $ MkRange (MkPosition newLine 0) (MkPosition newLine 0) -- insert
134+
(Just None) => do
135+
logD GenerateDefNext "No def to override, inserting new def"
136+
pure $ MkRange (MkPosition newLine 0) (MkPosition newLine 0) -- insert
137+
(Just (PMDef pminfo args treeCT treeRT pats)) => do
138+
src <- String.lines <$> getSource
139+
let srcFromDef = drop (integerToNat (cast line)) src
140+
let blank = findBlankLine srcFromDef line
141+
pure $ MkRange (MkPosition newLine 0) (MkPosition blank 0) -- replace
142+
(Just _) => do
143+
logE GenerateDefNext "UNEXPECTED"
144+
pure $ MkRange (MkPosition newLine 0) (MkPosition newLine 0) -- insert
145+
146+
let docURI = params.textDocument.uri
147+
148+
action <- do
149+
let edit = MkTextEdit rng (String.unlines lines)
150+
pure $ buildCodeAction docURI edit
151+
-- TODO: retrieve the line length efficiently
152+
pure [(MkRange (MkPosition line 0) (MkPosition line 1000), [action])]

‎src/Language/LSP/CodeAction/Utils.idr‎

Lines changed: 37 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1,13 +1,19 @@
11
module Language.LSP.CodeAction.Utils
22

3-
import Core.Core
3+
import Core.Context
44
import Core.Context.Context
5+
import Core.Core
6+
import Idris.Resugar
7+
import Idris.Syntax
58
import Language.LSP.CodeAction
69
import Language.LSP.Message.CodeAction
710
import Language.LSP.Message.Location
11+
import Parser.Unlit
812
import Server.Configuration
913
import Server.Log
1014
import Server.Utils
15+
import TTImp.TTImp
16+
import TTImp.TTImp.Functor
1117

1218
||| Check for code actions that require the request to be on a single line.
1319
||| @topic Logging topic of the code action
@@ -70,3 +76,33 @@ withMultipleCache topic params action new =
7076
pure $ concat $ snd <$> locs
7177
acts => do logD topic "Found cached action"
7278
pure acts
79+
80+
||| Pretty print a clause as source-code to be sent to the editor.
81+
||| Reproduced from compiler repo where this function is not exported.
82+
export
83+
printClause : Ref Ctxt Defs
84+
=> Ref Syn SyntaxInfo
85+
=> Maybe String -> Nat -> ImpClause -> Core String
86+
printClause l i (PatClause _ lhsraw rhsraw) = do
87+
lhs <- pterm $ map defaultKindedName lhsraw
88+
rhs <- pterm $ map defaultKindedName rhsraw
89+
pure $ relit l "\{pack (replicate i ' ')}\{show lhs} = \{show rhs}"
90+
printClause l i (WithClause _ lhsraw rig wvraw prf flags csraw) = do
91+
lhs <- pterm $ map defaultKindedName lhsraw
92+
wval <- pterm $ map defaultKindedName wvraw
93+
cs <- traverse (printClause l (i + 2)) csraw
94+
pure (relit l ((pack (replicate i ' ')
95+
++ show lhs
96+
++ " with \{showCount rig}(" ++ show wval ++ ")"
97+
++ maybe "" (\ nm => " proof " ++ show nm) prf
98+
++ "\n"))
99+
++ showSep "\n" cs)
100+
printClause l i (ImpossibleClause _ lhsraw) = do
101+
do lhs <- pterm $ map defaultKindedName lhsraw
102+
pure $ relit l "\{pack (replicate i ' ')}\{show lhs} impossible"
103+
104+
||| Zip some lines up with their indices starting at the given number.
105+
export
106+
number : Nat -> List a -> List (Nat, a)
107+
number n [] = []
108+
number n (x :: xs) = (n, x) :: number (S n) xs

‎src/Server/Log.idr‎

Lines changed: 2 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -29,6 +29,7 @@ data Topic
2929
| DocumentSymbol
3030
| ExprSearch
3131
| GenerateDef
32+
| GenerateDefNext
3233
| GotoDefinition
3334
| Hover
3435
| Intro
@@ -56,6 +57,7 @@ Show Topic where
5657
show DocumentSymbol = "Request.DocumentSymbol"
5758
show ExprSearch = "Request.CodeAction.ExprSearch"
5859
show GenerateDef = "Request.CodeAction.GenerateDef"
60+
show GenerateDefNext = "Request.CodeAction.GenerateDefNext"
5961
show GotoDefinition = "Request.GotoDefinition"
6062
show Hover = "Request.Hover"
6163
show Intro = "Request.CodeAction.Intro"

‎src/Server/ProcessMessage.idr‎

Lines changed: 3 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -35,6 +35,7 @@ import Language.LSP.CodeAction.AddClause
3535
import Language.LSP.CodeAction.CaseSplit
3636
import Language.LSP.CodeAction.ExprSearch
3737
import Language.LSP.CodeAction.GenerateDef
38+
import Language.LSP.CodeAction.GenerateDefNext
3839
import Language.LSP.CodeAction.Intro
3940
import Language.LSP.CodeAction.MakeCase
4041
import Language.LSP.CodeAction.MakeLemma
@@ -249,7 +250,6 @@ loadURI conf uri version = do
249250
put MD (initMetadata (PhysicalIdrSrc modIdent))
250251
ignore $ ProcessIdr.process msgPrefix buildMsg fname modIdent
251252

252-
resetProofState
253253
let caps = (publishDiagnostics <=< textDocument) . capabilities $ conf
254254
update LSPConf ({ quickfixes := [], cachedActions := empty, cachedHovers := empty })
255255
traverse_ (findQuickfix caps uri) errs
@@ -440,9 +440,10 @@ handleRequest TextDocumentCodeAction params = whenActiveRequest $ \conf => do
440440
makeCaseAction <- makeCase params
441441
introActions <- map Just <$> intro params
442442
generateDefActions <- map Just <$> generateDef params
443+
generateDefNextActions <- map Just <$> generateDefNext params
443444
let resp = flatten $ quickfixActions
444445
++ [splitAction, lemmaAction, withAction, clauseAction, makeCaseAction]
445-
++ introActions ++ generateDefActions ++ exprSearchActions
446+
++ introActions ++ generateDefActions ++ generateDefNextActions ++ exprSearchActions
446447
pure $ pure $ make resp)
447448
where
448449
flatten : List (Maybe CodeAction) -> List (OneOf [Command, CodeAction])

0 commit comments

Comments
 (0)