0 | module Idris.IDEMode.CaseSplit
  1 |
  2 | import Core.Env
  3 | import Core.Metadata
  4 | import Core.Value
  5 |
  6 | import Parser.Lexer.Source
  7 | import Parser.Unlit
  8 |
  9 | import TTImp.Interactive.CaseSplit
 10 | import TTImp.TTImp
 11 | import TTImp.TTImp.Functor
 12 | import TTImp.Utils
 13 |
 14 | import Idris.IDEMode.TokenLine
 15 | import Idris.REPL.Opts
 16 | import Idris.Resugar
 17 | import Idris.Syntax
 18 |
 19 | import Data.List.Views
 20 | import Libraries.Data.List.Extra
 21 | import Data.String
 22 | import Libraries.Data.String as L
 23 | import System.File
 24 | import Data.Fin
 25 |
 26 | %default covering
 27 |
 28 | ||| A series of updates is a mapping from `RawName` to `String`
 29 | ||| `RawName` is currently just an alias for `String`
 30 | ||| `String` is a rendered `List SourcePart`
 31 | Updates : Type
 32 | Updates = List (RawName, String)
 33 |
 34 | ||| Convert a RawImp update to a SourcePart one
 35 | toStrUpdate : {auto c : Ref Ctxt Defs} ->
 36 |               {auto s : Ref Syn SyntaxInfo} ->
 37 |               (Name, RawImp) -> Core Updates
 38 | toStrUpdate (UN (Basic n), term)
 39 |     = do clause <- pterm (map defaultKindedName term) -- hack
 40 |          pure [(n, show (bracket clause))]
 41 |   where
 42 |     bracket : PTerm' nm -> PTerm' nm
 43 |     bracket tm@(PRef {}) = tm
 44 |     bracket tm@(PList {}) = tm
 45 |     bracket tm@(PSnocList {}) = tm
 46 |     bracket tm@(PPair {}) = tm
 47 |     bracket tm@(PUnit {}) = tm
 48 |     bracket tm@(PComprehension {}) = tm
 49 |     bracket tm@(PPrimVal {}) = tm
 50 |     bracket tm = PBracketed emptyFC tm
 51 | toStrUpdate _ = pure [] -- can't replace non user names
 52 |
 53 | data UPD : Type where
 54 |
 55 |
 56 | ||| Returns True if the SourcePart is a `Whitespace _` and False if not. Useful
 57 | ||| for filtering or spanning a `List SourcPart`
 58 | isWhitespace : SourcePart -> Bool
 59 | isWhitespace (Whitespace _) = True
 60 | isWhitespace _              = False
 61 |
 62 | splitSpaceAndComments : List SourcePart -> (List SourcePart, List SourcePart)
 63 | splitSpaceAndComments = skipSpace Lin
 64 |   where
 65 |     skipSpace : SnocList SourcePart -> List SourcePart -> (List SourcePart, List SourcePart)
 66 |     skipComment : SnocList SourcePart -> List SourcePart -> (List SourcePart, List SourcePart)
 67 |
 68 |     skipComment left [] = (left <>> [], [])
 69 |     skipComment left (Other "-" :: RBrace :: toks) = skipSpace (left :< Other "-" :< RBrace) toks
 70 |     skipComment left (tok :: toks) = skipComment (left :< tok) toks
 71 |
 72 |     skipSpace left [] = (left <>> [], [])
 73 |     skipSpace left (LBrace :: Other "-" :: toks) = skipComment (left :< LBrace :< Other "-") toks
 74 |     skipSpace left (Whitespace ws :: toks) = skipSpace (left :< Whitespace ws) toks
 75 |     skipSpace left toks = (left <>> [], toks)
 76 |
 77 | data Wrap = Brace | Auto | Paren | Bracket
 78 |
 79 | ||| Given a list of definitions, a list of mappings from `RawName` to `String`,
 80 | ||| and a list of tokens to update, work out the updates to do, apply them, and
 81 | ||| return the result. Maintain a stack of brackets so we know if we need to insert
 82 | ||| a named application.
 83 | doUpdates : {auto s : Ref Syn SyntaxInfo} ->
 84 |             {auto u : Ref UPD (List String)} ->
 85 |             Defs -> Updates -> List Wrap -> List SourcePart ->
 86 |             Core (List SourcePart)
 87 | doUpdates defs ups stk [] = pure []   -- no more tokens to update, so we are done
 88 | -- if we have a name that acts as an as-pattern then do not update it
 89 | doUpdates defs ups stk (Name n :: AsPattern :: xs)
 90 |     = pure $ Name n :: AsPattern :: !(doUpdates defs ups stk xs)
 91 | -- if we have an `@{` that was not handled as a named pattern, it should not
 92 | -- result in named expansion (i.e. `@{n = ...}`) because that is not syntactically
 93 | -- valid. Push `Auto` to mark this case.
 94 | doUpdates defs ups stk (AsPattern :: LBrace :: xs)
 95 |     = pure $ AsPattern :: LBrace :: !(doUpdates defs ups (Auto :: stk) xs)
 96 | doUpdates defs ups stk toks@(LBrace :: Other "-" :: _) =
 97 |   let (ws, nws) = splitSpaceAndComments toks in
 98 |   pure (ws ++ !(doUpdates defs ups stk nws))
 99 | -- Handle tuples inside an implicit by pushing Paren
100 | doUpdates defs ups stk (Other "(" :: xs)  = pure (Other "(" :: !(doUpdates defs ups (Paren :: stk) xs))
101 | doUpdates defs ups stk (Other ")" :: xs)  = case stk of
102 |   (Paren :: stk) => pure (Other ")" :: !(doUpdates defs ups stk xs))
103 |   _ => pure (Other ")" :: !(doUpdates defs ups stk xs))
104 | doUpdates defs ups stk (Other "[" :: xs)  = pure (Other "[" :: !(doUpdates defs ups (Bracket :: stk) xs))
105 | doUpdates defs ups stk (Other "]" :: xs)  = case stk of
106 |   Bracket :: stk => pure (Other "]" :: !(doUpdates defs ups stk xs))
107 |   stk => pure (Other "]" :: !(doUpdates defs ups stk xs))
108 | doUpdates defs ups stk (Other "-" :: Other "-" :: xs) = pure (Other "--" :: xs)
109 | -- name after LBrace
110 | doUpdates defs ups stk (LBrace :: xs) =
111 |   let (ws, nws) = splitSpaceAndComments xs in
112 |     case nws of
113 |       Name n :: rest => case lookup n ups of
114 |         Just up => pure (LBrace :: ws ++ Name n :: Whitespace " " :: Equal :: Whitespace " " :: Other up :: !(doUpdates defs ups stk rest))
115 |         Nothing => pure (LBrace :: ws ++ !(doUpdates defs ups (Brace :: stk) nws))
116 |       _ => pure (LBrace :: ws ++ !(doUpdates defs ups (Brace :: stk) nws))
117 | -- handle commas directly inside an implicit
118 | doUpdates defs ups stk (Other "," :: xs) =
119 |       let (ws, nws) = splitSpaceAndComments xs in
120 |         case nws of
121 |           Name n :: rest => case lookup n ups of
122 |             Nothing => pure (Other "," :: ws ++ !(doUpdates defs ups stk nws))
123 |             Just up => case stk of
124 |               Brace :: _ => pure (Other "," :: ws ++ Name n :: Whitespace " " :: Equal :: Whitespace " " :: Other up :: !(doUpdates defs ups stk rest))
125 |               _ => pure (Other "," :: ws ++ Other up :: !(doUpdates defs ups stk rest))
126 |           _ => pure (Other "," :: ws ++ !(doUpdates defs ups stk nws))
127 |
128 | doUpdates defs ups stk (RBrace :: xs) = case stk of
129 |   Brace :: stk => pure (RBrace :: !(doUpdates defs ups stk xs))
130 |   Auto :: stk => pure (RBrace :: !(doUpdates defs ups stk xs))
131 |   stk => pure (RBrace :: !(doUpdates defs ups stk xs))
132 |
133 | -- if we have a name, look up if it's a name we're updating. If it isn't, keep
134 | -- the old name, otherwise update the name, i.e. replace with the new name
135 | doUpdates defs ups stk (Name n :: xs)
136 |     = case lookup n ups of
137 |            Nothing => pure (Name n :: !(doUpdates defs ups stk xs))
138 |            Just up => pure (Other up :: !(doUpdates defs ups stk xs))
139 | -- if we have a hole, get the used names, generate+register a new unique name,
140 | -- and change the hole's name to the new one
141 | doUpdates defs ups stk (HoleName n :: xs)
142 |     = do used <- get UPD
143 |          n' <- uniqueHoleName defs used n
144 |          put UPD (n' :: used)
145 |          pure $ HoleName n' :: !(doUpdates defs ups stk xs)
146 | -- if it's not a thing we update, leave it and continue working on the rest
147 | doUpdates defs ups stk (x :: xs)
148 |     = pure $ x :: !(doUpdates defs ups stk xs)
149 |
150 | -- State here is a list of new hole names we generated (so as not to reuse any).
151 | -- Update the token list with the string replacements for each match, and return
152 | -- the newly generated strings.
153 | updateAll : {auto s : Ref Syn SyntaxInfo} ->
154 |             {auto u : Ref UPD (List String)} ->
155 |             Defs -> List SourcePart -> List Updates ->
156 |             Core (List String)
157 | updateAll defs l [] = pure []
158 | updateAll defs l (rs :: rss)
159 |     = do l' <- doUpdates defs rs [] l
160 |          rss' <- updateAll defs l rss
161 |          pure (concatMap toString l' :: rss')
162 |
163 | -- Turn the replacements we got from 'getSplits' into a list of actual string
164 | -- replacements
165 | getReplaces : {auto c : Ref Ctxt Defs} ->
166 |               {auto s : Ref Syn SyntaxInfo} ->
167 |               List (Name, RawImp) -> Core Updates
168 | getReplaces updates
169 |     = do strups <- traverse toStrUpdate updates
170 |          pure (concat strups)
171 |
172 | showImpossible : {auto c : Ref Ctxt Defs} ->
173 |                  {auto s : Ref Syn SyntaxInfo} ->
174 |                  (indent : Nat) -> RawImp -> Core String
175 | showImpossible indent lhs
176 |     = do clause <- pterm (map defaultKindedName lhs) -- hack
177 |          pure (fastPack (replicate indent ' ') ++ show clause ++ " impossible")
178 |
179 | ||| What type of `case` block we're splitting:
180 | ||| - OneLine Nat
181 | |||   ```
182 | |||   f n = (case n of case_val => ?f_rhs)
183 | |||   ```
184 | |||   The `Nat` is the index of the "of" keyword
185 | ||| - HoleNameParen
186 | |||   ```
187 | |||   g n = (case n of
188 | |||               case_val => ?g_rhs)
189 | |||   ```
190 | data CaseStmtType = Oneline Nat
191 |                   | OnelineParen Nat
192 |                   | HoleNameParen
193 |
194 | ||| Inspect the token list to see if it contains an interesting `case` block for
195 | ||| splitting, and if it does, determine the type of interesting `case` block
196 | getCaseStmtType : (toks : List SourcePart) -> Maybe CaseStmtType
197 | getCaseStmtType toks
198 |   = let nws = dropComment $ filter (not . isWhitespace) toks in
199 |         -- use SnocList of nws so we can express the pattern we're looking for
200 |         -- as it would appear
201 |         case Lin <>< nws of
202 |              -- If the line ends with a right parenthesis followed by a
203 |              -- `HoleName`, we're interested in what kind of `case` block it is
204 |              start :< HoleName _ :< Other ")" =>
205 |                   -- try to find the index of a `Name "of"` in the SnocList of
206 |                   -- all tokens, including whitespace; if we don't find one, the
207 |                   -- line must be a case hole on a new line, otherwise, it must
208 |                   -- be a oneline case statement and the index let's us
209 |                   -- calculate the indentation required!
210 |                   case findIndex isNameOf (Lin <>< toks) of
211 |                        Nothing => Just HoleNameParen
212 |                        (Just skotOfIndex) =>
213 |                             -- calculate the indentation, remembering that we
214 |                             -- constructed a SnocList so the index is backwards
215 |                             let ofIndex = minus (length toks) (finToNat skotOfIndex) in
216 |                                 Just $ OnelineParen (calcIndent ofIndex toks)
217 |              -- If the line ends with a `HoleName`, check if it's a oneline `case` block
218 |              start :< HoleName _ =>
219 |                   case findIndex isNameOf (Lin <>< toks) of
220 |                        Nothing => Nothing
221 |                        (Just skotOfIndex) =>
222 |                             let ofIndex = minus (length toks) (finToNat skotOfIndex) in
223 |                                 Just $ Oneline (calcIndent ofIndex toks)
224 |              -- If it doesn't, it's not a statement we're interested in
225 |              _ => Nothing
226 |     where
227 |       dropComment : List SourcePart -> List SourcePart
228 |       dropComment [] = []
229 |       dropComment (Other "-" :: Other "-" :: xs) = []
230 |       dropComment (x :: xs) = x :: dropComment xs
231 |
232 |       isNameOf : SourcePart -> Bool
233 |       isNameOf (Name "of") = True
234 |       isNameOf _ = False
235 |
236 |       calcIndent : Nat -> List SourcePart -> Nat
237 |       calcIndent ofIndex toks
238 |         = let (preOf, _) = splitAt ofIndex toks in
239 |               foldr (\e,a => a + (length . toString) e) 0 preOf
240 |
241 |
242 | ||| Given a list of characters reprsenting an update string, drop its last
243 | ||| element.
244 | dropLast : (updChars : List Char) -> List Char
245 | dropLast updChars with (snocList updChars)
246 |   dropLast [] | Empty = []
247 |   dropLast (xs ++ [x]) | (Snoc x xs rec) = xs
248 |
249 | -- remove last paren
250 | dropLastParen : SnocList Char -> SnocList Char
251 | dropLastParen Lin = Lin
252 | dropLastParen (cs :< ')') = cs
253 | dropLastParen (cs :< c) = dropLastParen cs :< c
254 |
255 | ||| Drop the closing parenthesis and any indentation preceding it.
256 | parenTrim : String -> String
257 | parenTrim = L.rtrim . fastPack . cast . dropLastParen . cast . fastUnpack
258 |
259 | ||| Drop the number of letters equal to the indentation level to align
260 | ||| just after the `of`.
261 | onelineIndent : Nat -> String -> String
262 | onelineIndent indentation
263 |   = (indent indentation) . fastPack . (drop indentation) . fastUnpack
264 |
265 | ||| An unbracketed, oneline `case` block just needs to have the last updates
266 | ||| indented to align with the statement after the `of`.
267 | handleOneline : (indentation : Nat) -> (upds : List String) -> List String
268 | handleOneline indentation [] = []
269 | handleOneline indentation (u :: us) = u :: ((onelineIndent indentation) <$> us)
270 |
271 | ||| A bracketed, oneline `case` block needs to have the parenthesis cut off the
272 | ||| first update; all the following updates, apart from the last, need to have
273 | ||| the parenthesis cut off and be indented rather than having the line
274 | ||| repeated; the final update only needs to be indented, but must preserve the
275 | ||| parenthesis from the original line that was split.
276 | handleOnelineParen : (indentation : Nat) -> (upds : List String) -> List String
277 | handleOnelineParen indentation upds with (snocList upds)
278 |   handleOnelineParen indentation [] | Empty = []
279 |   handleOnelineParen indentation (xs ++ [x]) | (Snoc x xs rec)
280 |     = handleMiddle xs ++ [onelineIndent indentation x]
281 |   where
282 |     handleMiddle : (us : List String) -> List String
283 |     handleMiddle [] = []
284 |     handleMiddle (u :: us)
285 |       = (parenTrim $ onelineIndent indentation u) :: handleMiddle us
286 |
287 | ||| A `HoleName` folled by a parenthesis needs to have the parenthesis removed
288 | ||| from every update apart from the final one.
289 | handleHoleNameParen : (upds : List String) -> List String
290 | handleHoleNameParen upds with (snocList upds)
291 |   handleHoleNameParen [] | Empty = []
292 |   handleHoleNameParen (xs ++ [x]) | (Snoc x xs rec) = map parenTrim xs ++ [x]
293 |
294 | ||| Given a list of updates and some information as to what kind of `case` block
295 | ||| needs handling, change the updates such that the result is syntactically
296 | ||| correct Idris.
297 | handleCaseStmtType : (upds : List String) ->
298 |                      (cst : CaseStmtType) ->
299 |                      List String
300 | handleCaseStmtType [] _ = []
301 | handleCaseStmtType (u :: us) (Oneline indentation) = handleOneline indentation (u :: us)
302 | handleCaseStmtType (u :: us) (OnelineParen indentation)
303 |   = (parenTrim u) :: handleOnelineParen indentation us
304 | handleCaseStmtType upds HoleNameParen = handleHoleNameParen upds
305 |
306 | ||| Given a list of updates and a line and column, find the relevant line in
307 | ||| the source file and return the lines to replace it with.
308 | export
309 | updateCase : {auto c : Ref Ctxt Defs} ->
310 |              {auto s : Ref Syn SyntaxInfo} ->
311 |              {auto o : Ref ROpts REPLOpts} ->
312 |              List ClauseUpdate -> Int -> Int ->
313 |              Core (List String)
314 | updateCase splits line col
315 |     = do opts <- get ROpts
316 |          case mainfile opts of
317 |               Nothing => throw (InternalError "No file loaded")
318 |               Just f =>
319 |                 do Right file <- coreLift $ readFile f
320 |                        | Left err => throw (FileErr f err)
321 |                    let thisline = elemAt (lines file) (integerToNat (cast line))
322 |                    case thisline of
323 |                         Nothing => throw (InternalError "File too short!")
324 |                         Just l =>
325 |                             do let valid = mapMaybe getValid splits
326 |                                let bad = mapMaybe getBad splits
327 |                                log "interaction.casesplit" 3 $ "Valid: " ++ show valid
328 |                                log "interaction.casesplit" 3 $ "Bad: " ++ show bad
329 |                                if isNil valid
330 |                                   then do let indent = getIndent 0 $ fastUnpack l
331 |                                           traverse (showImpossible indent) bad
332 |                                   else do rs <- traverse getReplaces valid
333 |                                           let stok = tokens l
334 |                                           defs <- get Ctxt
335 |                                           u <- newRef UPD []
336 |                                           upds <- updateAll defs stok rs
337 |                                           pure $ case getCaseStmtType stok of
338 |                                                       Nothing => upds
339 |                                                       (Just cst) =>
340 |                                                           handleCaseStmtType upds cst
341 |   where
342 |     getValid : ClauseUpdate -> Maybe (List (Name, RawImp))
343 |     getValid (Valid _ ups) = Just ups
344 |     getValid _ = Nothing
345 |
346 |     getBad : ClauseUpdate -> Maybe RawImp
347 |     getBad (Impossible lhs) = Just lhs
348 |     getBad _ = Nothing
349 |
350 |     getIndent : (acc : Nat) -> List Char -> Nat
351 |     getIndent acc [] = acc
352 |     getIndent acc (' ' :: xs) = getIndent (acc + 1) xs
353 |     getIndent acc _ = acc
354 |
355 | fnName : Bool -> Name -> String
356 | fnName lhs (UN (Basic n))
357 |     = if isIdentNormal n then n
358 |       else if lhs then "(" ++ n ++ ")"
359 |       else "op"
360 | fnName lhs (NS _ n) = fnName lhs n
361 | fnName lhs (DN s _) = s
362 | fnName lhs n = nameRoot n
363 |
364 |
365 | export
366 | getClause : {auto c : Ref Ctxt Defs} ->
367 |             {auto m : Ref MD Metadata} ->
368 |             {auto o : Ref ROpts REPLOpts} ->
369 |             Int -> Name -> Core (Maybe String)
370 | getClause l n
371 |     = do defs <- get Ctxt
372 |          Just (loc, nidx, envlen, ty) <- findTyDeclAt (\p, n => onLine (l-1) p)
373 |              | Nothing => pure Nothing
374 |          n <- getFullName nidx
375 |          argns <- getEnvArgNames defs envlen !(nf defs Env.empty ty)
376 |          Just srcLine <- getSourceLine l
377 |            | Nothing => pure Nothing
378 |          let (mark, src) = isLitLine srcLine
379 |          pure (Just (indent mark loc ++ fnName True n ++ concat (map (" " ++) argns) ++
380 |                   " = ?" ++ fnName False n ++ "_rhs"))
381 |   where
382 |     indent : Maybe String -> NonEmptyFC -> String
383 |     indent (Just mark) fc
384 |         = relit (Just mark) $ pack (replicate (integerToNat (cast (max 0 (snd (startPos fc) - 1)))) ' ')
385 |     indent Nothing fc = pack (replicate (integerToNat (cast (snd (startPos fc)))) ' ')
386 |