[ fix #1175 ] case-splitting for inline case blocks (#2010)

src/Idris/IDEMode/CaseSplit.idr

@@ -22,10 +22,13 @@ import Idris.Syntax
 
 import Data.List
 import Data.List1
+import Data.List.Views
+import Data.SnocList
 import Libraries.Data.List.Extra
 import Libraries.Data.String.Extra
 import Data.String
 import System.File
+import Data.Fin
 
 %hide Data.String.lines
 %hide Data.String.lines'
@@ -61,6 +64,13 @@ toStrUpdate _ = pure [] -- can't replace non user names
 
 data UPD : Type where
 
+
+||| Returns True if the SourcePart is a `Whitespace _` and False if not. Useful
+||| for filtering or spanning a `List SourcPart`
+isWhitespace : SourcePart -> Bool
+isWhitespace (Whitespace _) = True
+isWhitespace _              = False
+
 ||| Given a list of definitions, a list of mappings from `RawName` to `String`,
 ||| and a list of tokens to update, work out the updates to do, apply them, and
 ||| return the result.
@@ -99,10 +109,6 @@ doUpdates defs ups (LBrace :: xs)
                              )
           -- not a special case: proceed as normal
           _ => pure (LBrace :: [] ++ !(doUpdates defs ups xs))
-  where
-    isWhitespace : SourcePart -> Bool
-    isWhitespace (Whitespace _) = True
-    isWhitespace _              = False
 -- if we have a name, look up if it's a name we're updating. If it isn't, keep
 -- the old name, otherwise update the name, i.e. replace with the new name
 doUpdates defs ups (Name n :: xs)
@@ -150,8 +156,128 @@ showImpossible indent lhs
     = do clause <- pterm (map defaultKindedName lhs) -- hack
          pure (fastPack (replicate indent ' ') ++ show clause ++ " impossible")
 
--- Given a list of updates and a line and column, find the relevant line in
--- the source file and return the lines to replace it with
+||| What type of `case` block we're splitting:
+||| - OneLine Nat
+|||   ```
+|||   f n = (case n of case_val => ?f_rhs)
+|||   ```
+|||   The `Nat` is the index of the "of" keyword
+||| - HoleNameParen
+|||   ```
+|||   g n = (case n of
+|||               case_val => ?g_rhs)
+|||   ```
+data CaseStmtType = Oneline Nat
+                  | OnelineParen Nat
+                  | HoleNameParen
+
+||| Inspect the token list to see if it contains an interesting `case` block for
+||| splitting, and if it does, determine the type of interesting `case` block
+getCaseStmtType : (toks : List SourcePart) -> Maybe CaseStmtType
+getCaseStmtType toks
+  = let nws = filter (not . isWhitespace) toks in
+        -- use SnocList of nws so we can express the pattern we're looking for
+        -- as it would appear
+        case Lin <>< nws of
+             -- If the line ends with a right parenthesis followed by a
+             -- `HoleName`, we're interested in what kind of `case` block it is
+             start :< HoleName _ :< Other ")" =>
+                  -- try to find the index of a `Name "of"` in the SnocList of
+                  -- all tokens, including whitespace; if we don't find one, the
+                  -- line must be a case hole on a new line, otherwise, it must
+                  -- be a oneline case statement and the index let's us
+                  -- calculate the indentation required!
+                  case findIndex isNameOf (Lin <>< toks) of
+                       Nothing => Just HoleNameParen
+                       (Just skotOfIndex) =>
+                            -- calculate the indentation, remembering that we
+                            -- constructed a SnocList so the index is backwards
+                            let ofIndex = minus (length toks) (finToNat skotOfIndex) in
+                                Just $ OnelineParen (calcIndent ofIndex toks)
+             -- If the line ends with a `HoleName`, check if its a oneline `case` block
+             start :< HoleName _ =>
+                  case findIndex isNameOf (Lin <>< toks) of
+                       Nothing => Nothing
+                       (Just skotOfIndex) =>
+                            let ofIndex = minus (length toks) (finToNat skotOfIndex) in
+                                Just $ Oneline (calcIndent ofIndex toks)
+             -- If it doesn't, it's not a statement we're interested in
+             _ => Nothing
+    where
+      isNameOf : SourcePart -> Bool
+      isNameOf (Name "of") = True
+      isNameOf _ = False
+
+      calcIndent : Nat -> List SourcePart -> Nat
+      calcIndent ofIndex toks
+        = let (preOf, _) = splitAt ofIndex toks in
+              foldr (\e,a => a + (length . toString) e) 0 preOf
+
+
+||| Given a list of characters reprsenting an update string, drop its last
+||| element.
+dropLast : (updChars : List Char) -> List Char
+dropLast updChars with (snocList updChars)
+  dropLast [] | Empty = []
+  dropLast (xs ++ [x]) | (Snoc x xs rec) = xs
+
+||| Trim whitespace to the right of the string
+rtrim : String -> String
+rtrim = reverse . ltrim . reverse
+
+||| Drop the closing parenthesis and any indentation preceding it.
+parenTrim : String -> String
+parenTrim = Idris.IDEMode.CaseSplit.rtrim . fastPack . dropLast . fastUnpack
+
+||| Drop the number of letters equal to the indentation level to align
+||| just after the `of`.
+onelineIndent : Nat -> String -> String
+onelineIndent indentation
+  = (Data.String.indent indentation) . fastPack . (drop indentation) . fastUnpack
+
+||| An unbracketed, oneline `case` block just needs to have the last updates
+||| indented to lign up with the statement after the `of`.
+handleOneline : (indentation : Nat) -> (upds : List String) -> List String
+handleOneline indentation [] = []
+handleOneline indentation (u :: us) = u :: ((onelineIndent indentation) <$> us)
+
+||| A bracketed, oneline `case` block needs to have the parenthesis cut off the
+||| first update; all the following updates, apart from the last, need to have
+||| the parenthesis cut off and be indented rather than having the line
+||| repeated; the final update only needs to be indented, but must preserve the
+||| parenthesis from the original line that was split.
+handleOnelineParen : (indentation : Nat) -> (upds : List String) -> List String
+handleOnelineParen indentation upds with (snocList upds)
+  handleOnelineParen indentation [] | Empty = []
+  handleOnelineParen indentation (xs ++ [x]) | (Snoc x xs rec)
+    = handleMiddle xs ++ [onelineIndent indentation x]
+  where
+    handleMiddle : (us : List String) -> List String
+    handleMiddle [] = []
+    handleMiddle (u :: us)
+      = (parenTrim $ onelineIndent indentation u) :: handleMiddle us
+
+||| A `HoleName` folled by a parenthesis needs to have the parenthesis removed
+||| from every update apart from the final one.
+handleHoleNameParen : (upds : List String) -> List String
+handleHoleNameParen upds with (snocList upds)
+  handleHoleNameParen [] | Empty = []
+  handleHoleNameParen (xs ++ [x]) | (Snoc x xs rec) = map parenTrim xs ++ [x]
+
+||| Given a list of updates and some information as to what kind of `case` block
+||| needs handling, change the updates such that the result is syntactically
+||| correct Idris.
+handleCaseStmtType : (upds : List String) ->
+                     (cst : CaseStmtType) ->
+                     List String
+handleCaseStmtType [] _ = []
+handleCaseStmtType (u :: us) (Oneline indentation) = handleOneline indentation (u :: us)
+handleCaseStmtType (u :: us) (OnelineParen indentation)
+  = (parenTrim u) :: handleOnelineParen indentation us
+handleCaseStmtType upds HoleNameParen = handleHoleNameParen upds
+
+||| Given a list of updates and a line and column, find the relevant line in
+||| the source file and return the lines to replace it with.
 export
 updateCase : {auto c : Ref Ctxt Defs} ->
              {auto s : Ref Syn SyntaxInfo} ->
@@ -180,7 +306,11 @@ updateCase splits line col
                                           let stok = tokens l
                                           defs <- get Ctxt
                                           u <- newRef UPD []
-                                          updateAll defs stok rs
+                                          upds <- updateAll defs stok rs
+                                          pure $ case getCaseStmtType stok of
+                                                      Nothing => upds
+                                                      (Just cst) =>
+                                                          handleCaseStmtType upds cst
   where
     getValid : ClauseUpdate -> Maybe (List (Name, RawImp))
     getValid (Valid _ ups) = Just ups

tests/Main.idr

@@ -88,7 +88,7 @@ idrisTestsInteractive = MkTestPool "Interactive editing" [] Nothing
        "interactive025", "interactive026", "interactive027", "interactive028",
        "interactive029", "interactive030", "interactive031", "interactive032",
        "interactive033", "interactive034", "interactive035", "interactive036",
-       "interactive037", "interactive038"]
+       "interactive037", "interactive038", "interactive039"]
 
 idrisTestsInterface : TestPool
 idrisTestsInterface = MkTestPool "Interface" [] Nothing

tests/idris2/interactive039/CS_Syntax.idr

@@ -0,0 +1,43 @@
+f : Nat -> Nat
+f n = case n of case_val => ?f_rhs
+
+g : Nat -> Nat
+g n = (case n of case_val => ?g_rhs)
+
+h : Nat -> Nat
+h n = (case n of
+            case_val => ?h_rhs     )
+
+data Test = One
+          | Two Nat
+          | Three String Nat
+          | Four
+
+toTest : Nat -> Test
+
+i : Nat -> Nat
+i n = case toTest n of case_val => ?i_rhs
+
+j : Nat -> Nat
+j n = j_Where n where
+  j_Where : Nat -> Nat
+  j_Where k = (case toTest k of case_val => ?j_Where_rhs    )
+
+k : Nat -> Nat
+k n = (case toTest n of
+            case_val => ?k_rhs)
+
+l : Nat -> Nat -> Unit
+l n m = case n of foo => case toTest m of case_val => ?l_rhs
+
+m : Nat -> Nat -> Unit
+m n k = (case n of foo => case toTest k of case_val => ?m_rhs  )
+
+n : Nat -> Nat -> Unit
+n k m = case k of foo => case toTest m of
+                              case_val => ?n_rhs
+
+o : Nat -> Nat -> Unit
+o n m = (case n of foo => case toTest m of
+                               case_val => ?o_rhs   )
+

tests/idris2/interactive039/expected

@@ -0,0 +1,34 @@
+1/1: Building CS_Syntax (CS_Syntax.idr)
+Main> f n = case n of 0 => ?f_rhs_1
+                (S k) => ?f_rhs_2
+Main> g n = (case n of 0 => ?g_rhs_1
+                 (S k) => ?g_rhs_2)
+Main>             0 => ?h_rhs_1
+            (S k) => ?h_rhs_2     )
+Main>             0 => ?h_rhs_1
+            (S k) => ?h_rhs_2     )
+Main>   j_Where k = (case toTest k of One => ?j_Where_rhs_1
+                                (Two j) => ?j_Where_rhs_2
+                                (Three x j) => ?j_Where_rhs_3
+                                Four => ?j_Where_rhs_4    )
+Main>             One => ?k_rhs_1
+            (Two k) => ?k_rhs_2
+            (Three x k) => ?k_rhs_3
+            Four => ?k_rhs_4)
+Main> l n m = case n of foo => case toTest m of One => ?l_rhs_1
+                                          (Two k) => ?l_rhs_2
+                                          (Three x k) => ?l_rhs_3
+                                          Four => ?l_rhs_4
+Main> m n k = (case n of foo => case toTest k of One => ?m_rhs_1
+                                           (Two j) => ?m_rhs_2
+                                           (Three x j) => ?m_rhs_3
+                                           Four => ?m_rhs_4  )
+Main>                               One => ?n_rhs_1
+                              (Two j) => ?n_rhs_2
+                              (Three x j) => ?n_rhs_3
+                              Four => ?n_rhs_4
+Main>                                One => ?o_rhs_1
+                               (Two k) => ?o_rhs_2
+                               (Three x k) => ?o_rhs_3
+                               Four => ?o_rhs_4   )
+Main> Bye for now!

tests/idris2/interactive039/input

@@ -0,0 +1,11 @@
+:cs 2 17 case_val
+:cs 5 18 case_val
+:cs 9 13 case_val
+:cs 9 24 case_val
+:cs 24 33 case_val
+:cs 28 13 case_val
+:cs 31 43 case_val
+:cs 34 44 case_val
+:cs 38 31 case_val
+:cs 42 32 case_val
+:q

tests/idris2/interactive039/run

@@ -0,0 +1,3 @@
+rm -rf build
+
+$1 --no-color --console-width 0 --no-banner CS_Syntax.idr < input