From 5bd5777fb7b96e4b4068ca09ac6278e3438b20d0 Mon Sep 17 00:00:00 2001 From: Edwin Brady Date: Thu, 30 Jul 2015 16:30:47 +0100 Subject: [PATCH] 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 | 1 + src/Idris/CaseSplit.hs | 23 ++++++++++++-------- src/Idris/IdeMode.hs | 2 ++ src/Idris/Interactive.hs | 43 +++++++++++++++++++++++++++++++++++++- src/Idris/REPL.hs | 5 +++++ src/Idris/REPLParser.hs | 2 ++ 6 files changed, 66 insertions(+), 10 deletions(-) diff --git a/src/Idris/AbsSyntaxTree.hs b/src/Idris/AbsSyntaxTree.hs index 044f5472e..317aa9b6d 100644 --- a/src/Idris/AbsSyntaxTree.hs +++ b/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, diff --git a/src/Idris/CaseSplit.hs b/src/Idris/CaseSplit.hs index 3a2db0e13..950b8c363 100644 --- a/src/Idris/CaseSplit.hs +++ b/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 diff --git a/src/Idris/IdeMode.hs b/src/Idris/IdeMode.hs index 8a1c88497..f4eaf2822 100644 --- a/src/Idris/IdeMode.hs +++ b/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. diff --git a/src/Idris/Interactive.hs b/src/Idris/Interactive.hs index df1d2b92f..668806416 100644 --- a/src/Idris/Interactive.hs +++ b/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 () diff --git a/src/Idris/REPL.hs b/src/Idris/REPL.hs index 2c1a374ed..60cdc3291 100644 --- a/src/Idris/REPL.hs +++ b/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) diff --git a/src/Idris/REPLParser.hs b/src/Idris/REPLParser.hs index ae453034f..3bc386531 100644 --- a/src/Idris/REPLParser.hs +++ b/src/Idris/REPLParser.hs @@ -123,6 +123,8 @@ parserCommands = ":am adds all missing pattern matches for the name on the line" , proofArgCmd ["mw", "makewith"] MakeWith ":mw adds a with clause for the definition of the name on the line" + , proofArgCmd ["mc", "makecase"] MakeCase + ":mc 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