Merge pull request #119 from idris-lang/idemode

[ refactor ] Idris.IDEMode.CaseSplit

idris2.ipkg

@@ -52,6 +52,7 @@ modules =
     Data.Bool.Extra,
     Data.IntMap,
     Data.LengthMatch,
+    Data.List.Extra,
     Data.NameMap,
     Data.StringMap,
     Data.These,

src/Data/List/Extra.idr

@@ -0,0 +1,11 @@
+module Data.List.Extra
+
+%default covering
+
+||| Fetches the element at a given position.
+||| Returns `Nothing` if the position beyond the list's end.
+public export
+elemAt : List a -> Nat -> Maybe a
+elemAt []        _     = Nothing
+elemAt (l :: _)  Z     = Just l
+elemAt (_ :: ls) (S n) = elemAt ls n

src/Idris/IDEMode/CaseSplit.idr

@@ -19,19 +19,22 @@ import Idris.Resugar
 import Idris.Syntax
 
 import Data.List
+import Data.List.Extra
 import Data.Strings
 import System.File
 
 %default covering
 
-getLine : Nat -> List String -> Maybe String
-getLine Z (l :: ls) = Just l
-getLine (S k) (l :: ls) = getLine k ls
-getLine _ [] = Nothing
+||| A series of updates is a mapping from `RawName` to `String`
+||| `RawName` is currently just an alias for `String`
+||| `String` is a rendered `List SourcePart`
+Updates : Type
+Updates = List (RawName, String)
 
+||| Convert a RawImp update to a SourcePart one
 toStrUpdate : {auto c : Ref Ctxt Defs} ->
               {auto s : Ref Syn SyntaxInfo} ->
-              (Name, RawImp) -> Core (List (String, String))
+              (Name, RawImp) -> Core Updates
 toStrUpdate (UN n, term)
     = do clause <- pterm term
          pure [(n, show (bracket clause))]
@@ -46,38 +49,30 @@ toStrUpdate (UN n, term)
     bracket tm = PBracketed emptyFC tm
 toStrUpdate _ = pure [] -- can't replace non user names
 
-dump : SourcePart -> String
-dump (Whitespace str) = str
-dump (Name n) = n
-dump (HoleName n) = "?" ++ n
-dump LBrace = "{"
-dump RBrace = "}"
-dump Equal = "="
-dump (Other str) = str
-
 data UPD : Type where
 
 doUpdates : {auto u : Ref UPD (List String)} ->
-            Defs -> List (String, String) -> List SourcePart ->
+            Defs -> Updates -> List SourcePart ->
             Core (List SourcePart)
 doUpdates defs ups [] = pure []
 doUpdates defs ups (LBrace :: xs)
-    = case dropSpace xs of
+    = let (ws, nws) = spanSpace xs in map (LBrace :: ws ++) $
+         case nws of
            Name n :: RBrace :: rest =>
-                pure (LBrace :: Name n ::
+                pure (Name n ::
                       Whitespace " " :: Equal :: Whitespace " " ::
                       !(doUpdates defs ups (Name n :: RBrace :: rest)))
            Name n :: Equal :: rest =>
-                pure (LBrace :: Name n ::
+                pure (Name n ::
                       Whitespace " " :: Equal :: Whitespace " " ::
                       !(doUpdates defs ups rest))
-           _ => pure (LBrace :: !(doUpdates defs ups xs))
+           _ => doUpdates defs ups xs
   where
-    dropSpace : List SourcePart -> List SourcePart
-    dropSpace [] = []
-    dropSpace (RBrace :: xs) = RBrace :: xs
-    dropSpace (Whitespace _ :: xs) = dropSpace xs
-    dropSpace (x :: xs) = x :: dropSpace xs
+    spanSpace : List SourcePart -> (List SourcePart, List SourcePart)
+    spanSpace []                   = ([], [])
+    spanSpace (RBrace           :: xs) = ([], RBrace :: xs)
+    spanSpace (w@(Whitespace _) :: xs) = mapFst (w ::) (spanSpace xs)
+    spanSpace (x                :: xs) = map    (x ::) (spanSpace xs)
 doUpdates defs ups (Name n :: xs)
     = case lookup n ups of
            Nothing => pure (Name n :: !(doUpdates defs ups xs))
@@ -94,20 +89,20 @@ doUpdates defs ups (x :: xs)
 -- Update the token list with the string replacements for each match, and return
 -- the newly generated strings.
 updateAll : {auto u : Ref UPD (List String)} ->
-            Defs -> List SourcePart -> List (List (String, String)) ->
+            Defs -> List SourcePart -> List Updates ->
             Core (List String)
 updateAll defs l [] = pure []
 updateAll defs l (rs :: rss)
     = do l' <- doUpdates defs rs l
          rss' <- updateAll defs l rss
-         pure (concat (map dump l') :: rss')
+         pure (concatMap toString l' :: rss')
 
 -- Turn the replacements we got from 'getSplits' into a list of actual string
 -- replacements
 getReplaces : {auto c : Ref Ctxt Defs} ->
               {auto s : Ref Syn SyntaxInfo} ->
               {auto o : Ref ROpts REPLOpts} ->
-              List (Name, RawImp) -> Core (List (String, String))
+              List (Name, RawImp) -> Core Updates
 getReplaces updates
     = do strups <- traverse toStrUpdate updates
          pure (concat strups)
@@ -135,7 +130,7 @@ updateCase splits line col
               Just f =>
                 do Right file <- coreLift $ readFile f
                        | Left err => throw (FileErr f err)
-                   let thisline = getLine (integerToNat (cast line)) (lines file)
+                   let thisline = elemAt (lines file) (integerToNat (cast line))
                    case thisline of
                         Nothing => throw (InternalError "File too short!")
                         Just l =>

src/Idris/IDEMode/TokenLine.idr

@@ -4,16 +4,38 @@ module Idris.IDEMode.TokenLine
 import Parser.Lexer.Source
 import Text.Lexer
 
+public export
+RawName : Type
+RawName = String
+
 public export
 data SourcePart
   = Whitespace String
-  | Name String
+  | Name RawName
   | HoleName String
   | LBrace
   | RBrace
   | Equal
   | Other String
 
+------------------------------------------------------------------------
+-- Printer
+------------------------------------------------------------------------
+
+export
+toString : SourcePart -> String
+toString (Whitespace str) = str
+toString (Name n) = n
+toString (HoleName n) = "?" ++ n
+toString LBrace = "{"
+toString RBrace = "}"
+toString Equal = "="
+toString (Other str) = str
+
+------------------------------------------------------------------------
+-- Parser
+------------------------------------------------------------------------
+
 holeIdent : Lexer
 holeIdent = is '?' <+> identNormal
 

tests/Main.idr

@@ -53,6 +53,7 @@ idrisTests
        "interactive001", "interactive002", "interactive003", "interactive004",
        "interactive005", "interactive006", "interactive007", "interactive008",
        "interactive009", "interactive010", "interactive011", "interactive012",
+       "interactive013",
        -- Literate
        "literate001", "literate002", "literate003", "literate004",
        "literate005", "literate006", "literate007", "literate008",

tests/idris2/interactive013/Spacing.idr

@@ -0,0 +1,4 @@
+module Spacing
+
+id : {n : Nat} -> Nat
+id {  n} = ?a

tests/idris2/interactive013/expected

@@ -0,0 +1,5 @@
+1/1: Building Spacing (Spacing.idr)
+Spacing> id {  n = 0} = ?a_1
+id {  n = (S k)} = ?a_2
+Spacing> 
+Bye for now!

tests/idris2/interactive013/input

@@ -0,0 +1,2 @@
+:cs 4 6 n
+:q

tests/idris2/interactive013/run

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