Add :makecase (:mc) to REPL and ide-mode

Replaces a metavariable with a case block, with an _ for the scrutinee
(much like :makewith)

I just got bored of typing these :). There is a corresponding update to
idris-vim.

src/Idris/AbsSyntaxTree.hs

@@ -402,6 +402,7 @@ data Command = Quit
              | AddProofClauseFrom Bool Int Name
              | AddMissing Bool Int Name
              | MakeWith Bool Int Name
+             | MakeCase Bool Int Name
              | MakeLemma Bool Int Name
              | DoProofSearch Bool Bool Int Name [Name]
                -- ^ the first bool is whether to update,

src/Idris/CaseSplit.hs

@@ -265,18 +265,23 @@ replaceSplits l ups = updateRHSs 1 (map (rep (expandBraces l)) ups)
     rep str ((n, tm) : ups) = rep (updatePat False (show n) (nshow tm) str) ups
 
     updateRHSs i [] = return []
-    updateRHSs i (x : xs) = do (x', i') <- updateRHS i x
+    updateRHSs i (x : xs) = do (x', i') <- updateRHS (null xs) i x
                                xs' <- updateRHSs i' xs
                                return (x' : xs')
 
-    updateRHS i ('?':'=':xs) = do (xs', i') <- updateRHS i xs
-                                  return ("?=" ++ xs', i')
-    updateRHS i ('?':xs) = do let (nm, rest) = span (not . isSpace) xs
-                              (nm', i') <- getUniq nm i
-                              return ('?':nm' ++ rest, i')
-    updateRHS i (x : xs) = do (xs', i') <- updateRHS i xs
-                              return (x : xs', i')
-    updateRHS i [] = return ("", i)
+    updateRHS last i ('?':'=':xs) = do (xs', i') <- updateRHS last i xs
+                                       return ("?=" ++ xs', i')
+    updateRHS last i ('?':xs) 
+        = do let (nm, rest_in) = span (not . (\x -> isSpace x || x == ')'
+                                                              || x == '(')) xs
+             let rest = if last then rest_in else
+                           case span (not . (=='\n')) rest_in of
+                                (_, restnl) -> restnl
+             (nm', i') <- getUniq nm i
+             return ('?':nm' ++ rest, i')
+    updateRHS last i (x : xs) = do (xs', i') <- updateRHS last i xs
+                                   return (x : xs', i')
+    updateRHS last i [] = return ("", i)
 
 
     -- TMP HACK: If there are Nats, we don't want to show as numerals since

src/Idris/IdeMode.hs

@@ -229,6 +229,7 @@ data IdeModeCommand = REPLCompletions String
                     | AddProofClause Int String
                     | AddMissing Int String
                     | MakeWithBlock Int String
+                    | MakeCaseBlock Int String
                     | ProofSearch Bool Int String [String] (Maybe Int) -- ^^ Recursive?, line, name, hints, depth
                     | MakeLemma Int String
                     | LoadFile String (Maybe Int)
@@ -261,6 +262,7 @@ sexpToCommand (SexpList [SymbolAtom "add-clause", IntegerAtom line, StringAtom n
 sexpToCommand (SexpList [SymbolAtom "add-proof-clause", IntegerAtom line, StringAtom name])   = Just (AddProofClause (fromInteger line) name)
 sexpToCommand (SexpList [SymbolAtom "add-missing", IntegerAtom line, StringAtom name])  = Just (AddMissing (fromInteger line) name)
 sexpToCommand (SexpList [SymbolAtom "make-with", IntegerAtom line, StringAtom name])    = Just (MakeWithBlock (fromInteger line) name)
+sexpToCommand (SexpList [SymbolAtom "make-case", IntegerAtom line, StringAtom name])    = Just (MakeCaseBlock (fromInteger line) name)
 -- The Boolean in ProofSearch means "search recursively"
 -- If it's False, that means "refine", i.e. apply the name and fill in any
 -- arguments which can be done by unification.

src/Idris/Interactive.hs

@@ -1,7 +1,7 @@
 {-# LANGUAGE PatternGuards #-}
 
 module Idris.Interactive(caseSplitAt, addClauseFrom, addProofClauseFrom,
-                         addMissing, makeWith, doProofSearch,
+                         addMissing, makeWith, makeCase, doProofSearch,
                          makeLemma) where
 
 {- Bits and pieces for editing source files interactively, called from
@@ -158,6 +158,47 @@ makeWith fn updatefile l n
            else iPrintResult with
   where getIndent s = length (takeWhile isSpace s)
 
+-- Replace the given metavariable on the given line with a 'case'
+-- block, using a _ for the scrutinee
+makeCase :: FilePath -> Bool -> Int -> Name -> Idris ()
+makeCase fn updatefile l n
+   = do src <- runIO $ readSource fn
+        let (before, tyline : later) = splitAt (l-1) (lines src)
+        let newcase = addCaseSkel (show n) tyline
+
+        if updatefile then
+           do let fb = fn ++ "~"
+              runIO $ writeSource fb (unlines (before ++ newcase ++ later))
+              runIO $ copyFile fb fn
+           else iPrintResult (unlines newcase)
+  where addCaseSkel n line =
+            let b = brackets False line in
+            case findSubstr ('?':n) line of
+                 Just (before, pos, after) ->
+                      [before ++ (if b then "(" else "") ++ "case _ of",
+                       take (pos + (if b then 6 else 5)) (repeat ' ') ++ 
+                             "case_val => ?" ++ n ++ if b then ")" else "",
+                       after]
+                 Nothing -> fail "No such metavariable"
+
+        -- Assume case needs to be bracketed unless the metavariable is
+        -- on its own after an =
+        brackets eq line | line == '?' : show n = not eq
+        brackets eq ('=':ls) = brackets True ls
+        brackets eq (' ':ls) = brackets eq ls
+        brackets eq (l : ls) = brackets False ls
+        brackets eq [] = True
+
+        findSubstr n xs = findSubstr' [] 0 n xs
+
+        findSubstr' acc i n xs | take (length n) xs == n 
+                = Just (reverse acc, i, drop (length n) xs)
+        findSubstr' acc i n [] = Nothing
+        findSubstr' acc i n (x : xs) = findSubstr' (x : acc) (i + 1) n xs
+
+
+
+
 
 doProofSearch :: FilePath -> Bool -> Bool -> 
                  Int -> Name -> [Name] -> Maybe Int -> Idris ()

src/Idris/REPL.hs

@@ -366,6 +366,8 @@ runIdeModeCommand h id orig fn mods (IdeMode.AddMissing line name) =
   process fn (AddMissing False line (sUN name))
 runIdeModeCommand h id orig fn mods (IdeMode.MakeWithBlock line name) =
   process fn (MakeWith False line (sUN name))
+runIdeModeCommand h id orig fn mods (IdeMode.MakeCaseBlock line name) =
+  process fn (MakeCase False line (sUN name))
 runIdeModeCommand h id orig fn mods (IdeMode.ProofSearch r line name hints depth) =
   doProofSearch fn False r line (sUN name) (map sUN hints) depth
 runIdeModeCommand h id orig fn mods (IdeMode.MakeLemma line name) =
@@ -632,6 +634,7 @@ idemodeProcess fn (AddProofClauseFrom False pos str) = process fn (AddProofClaus
 idemodeProcess fn (AddClauseFrom False pos str) = process fn (AddClauseFrom False pos str)
 idemodeProcess fn (AddMissing False pos str) = process fn (AddMissing False pos str)
 idemodeProcess fn (MakeWith False pos str) = process fn (MakeWith False pos str)
+idemodeProcess fn (MakeCase False pos str) = process fn (MakeCase False pos str)
 idemodeProcess fn (DoProofSearch False r pos str xs) = process fn (DoProofSearch False r pos str xs)
 idemodeProcess fn (SetConsoleWidth w) = do process fn (SetConsoleWidth w)
                                            iPrintResult ""
@@ -1049,6 +1052,8 @@ process fn (AddMissing updatefile l n)
     = addMissing fn updatefile l n
 process fn (MakeWith updatefile l n)
     = makeWith fn updatefile l n
+process fn (MakeCase updatefile l n)
+    = makeCase fn updatefile l n
 process fn (MakeLemma updatefile l n)
     = makeLemma fn updatefile l n
 process fn (DoProofSearch updatefile rec l n hints)

src/Idris/REPLParser.hs

@@ -123,6 +123,8 @@ parserCommands =
       ":am <line> <name> adds all missing pattern matches for the name on the line"
   , proofArgCmd ["mw", "makewith"] MakeWith
       ":mw <line> <name> adds a with clause for the definition of the name on the line"
+  , proofArgCmd ["mc", "makecase"] MakeCase
+      ":mc <line> <name> adds a case block for the definition of the metavariable on the line"
   , proofArgCmd ["ml", "makelemma"] MakeLemma "?"
   , (["log"], NumberArg, "Set logging verbosity level", cmd_log)
   , (["lto", "loadto"], SeqArgs NumberArg FileArg