5bd5777 · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

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.

commit5bd5777fb7b96e4b4068ca09ac6278e3438b20d0 authorEdwin Brady <ecb10@st-andrews.ac.uk> dateThu 30 Jul 2015, 16:30 (11 years ago) parent798958d

6 files changed+66−10

compare with master

unifiedsplit

src/Idris/AbsSyntaxTree.hs+1 src/Idris/CaseSplit.hs+14−9 src/Idris/IdeMode.hs+2 src/Idris/Interactive.hs+42−1 src/Idris/REPL.hs+5 src/Idris/REPLParser.hs+2

src/Idris/AbsSyntaxTree.hs+1

@@ -402,6 +402,7 @@ data Command = Quit

402402 | AddProofClauseFrom Bool Int Name

403403 | AddMissing Bool Int Name

404404 | MakeWith Bool Int Name

405+ | MakeCase Bool Int Name

405406 | MakeLemma Bool Int Name

406407 | DoProofSearch Bool Bool Int Name [Name]

407408 -- ^ the first bool is whether to update,

src/Idris/CaseSplit.hs+14−9

@@ -265,18 +265,23 @@ replaceSplits l ups = updateRHSs 1 (map (rep (expandBraces l)) ups)

265265 rep str ((n, tm) : ups) = rep (updatePat False (show n) (nshow tm) str) ups

266266

267267 updateRHSs i [] = return []

268− updateRHSs i (x : xs) = do (x', i') <- updateRHS i x

268+ updateRHSs i (x : xs) = do (x', i') <- updateRHS (null xs) i x

269269 xs' <- updateRHSs i' xs

270270 return (x' : xs')

271271

272− updateRHS i ('?':'=':xs) = do (xs', i') <- updateRHS i xs

273− return ("?=" ++ xs', i')

274− updateRHS i ('?':xs) = do let (nm, rest) = span (not . isSpace) xs

275− (nm', i') <- getUniq nm i

276− return ('?':nm' ++ rest, i')

277− updateRHS i (x : xs) = do (xs', i') <- updateRHS i xs

278− return (x : xs', i')

279− updateRHS i [] = return ("", i)

272+ updateRHS last i ('?':'=':xs) = do (xs', i') <- updateRHS last i xs

273+ return ("?=" ++ xs', i')

274+ updateRHS last i ('?':xs)

275+ = do let (nm, rest_in) = span (not . (\x -> isSpace x || x == ')'

276+ || x == '(')) xs

277+ let rest = if last then rest_in else

278+ case span (not . (=='\n')) rest_in of

279+ (_, restnl) -> restnl

280+ (nm', i') <- getUniq nm i

281+ return ('?':nm' ++ rest, i')

282+ updateRHS last i (x : xs) = do (xs', i') <- updateRHS last i xs

283+ return (x : xs', i')

284+ updateRHS last i [] = return ("", i)

280285

281286

282287 -- TMP HACK: If there are Nats, we don't want to show as numerals since

src/Idris/IdeMode.hs+2

@@ -229,6 +229,7 @@ data IdeModeCommand = REPLCompletions String

229229 | AddProofClause Int String

230230 | AddMissing Int String

231231 | MakeWithBlock Int String

232+ | MakeCaseBlock Int String

232233 | ProofSearch Bool Int String [String] (Maybe Int) -- ^^ Recursive?, line, name, hints, depth

233234 | MakeLemma Int String

234235 | LoadFile String (Maybe Int)

@@ -261,6 +262,7 @@ sexpToCommand (SexpList [SymbolAtom "add-clause", IntegerAtom line, StringAtom n

261262sexpToCommand (SexpList [SymbolAtom "add-proof-clause", IntegerAtom line, StringAtom name]) = Just (AddProofClause (fromInteger line) name)

262263sexpToCommand (SexpList [SymbolAtom "add-missing", IntegerAtom line, StringAtom name]) = Just (AddMissing (fromInteger line) name)

263264sexpToCommand (SexpList [SymbolAtom "make-with", IntegerAtom line, StringAtom name]) = Just (MakeWithBlock (fromInteger line) name)

265+sexpToCommand (SexpList [SymbolAtom "make-case", IntegerAtom line, StringAtom name]) = Just (MakeCaseBlock (fromInteger line) name)

264266-- The Boolean in ProofSearch means "search recursively"

265267-- If it's False, that means "refine", i.e. apply the name and fill in any

266268-- arguments which can be done by unification.

src/Idris/Interactive.hs+42−1

@@ -1,7 +1,7 @@

11{-# LANGUAGE PatternGuards #-}

33module Idris.Interactive(caseSplitAt, addClauseFrom, addProofClauseFrom,

4− addMissing, makeWith, doProofSearch,

4+ addMissing, makeWith, makeCase, doProofSearch,

55 makeLemma) where

77{- Bits and pieces for editing source files interactively, called from

@@ -158,6 +158,47 @@ makeWith fn updatefile l n

158158 else iPrintResult with

159159 where getIndent s = length (takeWhile isSpace s)

160160

161+-- Replace the given metavariable on the given line with a 'case'

162+-- block, using a _ for the scrutinee

163+makeCase :: FilePath -> Bool -> Int -> Name -> Idris ()

164+makeCase fn updatefile l n

165+ = do src <- runIO $ readSource fn

166+ let (before, tyline : later) = splitAt (l-1) (lines src)

167+ let newcase = addCaseSkel (show n) tyline

168+

169+ if updatefile then

170+ do let fb = fn ++ "~"

171+ runIO $ writeSource fb (unlines (before ++ newcase ++ later))

172+ runIO $ copyFile fb fn

173+ else iPrintResult (unlines newcase)

174+ where addCaseSkel n line =

175+ let b = brackets False line in

176+ case findSubstr ('?':n) line of

177+ Just (before, pos, after) ->

178+ [before ++ (if b then "(" else "") ++ "case _ of",

179+ take (pos + (if b then 6 else 5)) (repeat ' ') ++

180+ "case_val => ?" ++ n ++ if b then ")" else "",

181+ after]

182+ Nothing -> fail "No such metavariable"

183+

184+ -- Assume case needs to be bracketed unless the metavariable is

185+ -- on its own after an =

186+ brackets eq line | line == '?' : show n = not eq

187+ brackets eq ('=':ls) = brackets True ls

188+ brackets eq (' ':ls) = brackets eq ls

189+ brackets eq (l : ls) = brackets False ls

190+ brackets eq [] = True

191+

192+ findSubstr n xs = findSubstr' [] 0 n xs

193+

194+ findSubstr' acc i n xs | take (length n) xs == n

195+ = Just (reverse acc, i, drop (length n) xs)

196+ findSubstr' acc i n [] = Nothing

197+ findSubstr' acc i n (x : xs) = findSubstr' (x : acc) (i + 1) n xs

198+

199+

200+

201+

161202

162203doProofSearch :: FilePath -> Bool -> Bool ->

163204 Int -> Name -> [Name] -> Maybe Int -> Idris ()

src/Idris/REPL.hs+5

@@ -366,6 +366,8 @@ runIdeModeCommand h id orig fn mods (IdeMode.AddMissing line name) =

366366 process fn (AddMissing False line (sUN name))

367367runIdeModeCommand h id orig fn mods (IdeMode.MakeWithBlock line name) =

368368 process fn (MakeWith False line (sUN name))

369+runIdeModeCommand h id orig fn mods (IdeMode.MakeCaseBlock line name) =

370+ process fn (MakeCase False line (sUN name))

369371runIdeModeCommand h id orig fn mods (IdeMode.ProofSearch r line name hints depth) =

370372 doProofSearch fn False r line (sUN name) (map sUN hints) depth

371373runIdeModeCommand h id orig fn mods (IdeMode.MakeLemma line name) =

@@ -632,6 +634,7 @@ idemodeProcess fn (AddProofClauseFrom False pos str) = process fn (AddProofClaus

632634idemodeProcess fn (AddClauseFrom False pos str) = process fn (AddClauseFrom False pos str)

633635idemodeProcess fn (AddMissing False pos str) = process fn (AddMissing False pos str)

634636idemodeProcess fn (MakeWith False pos str) = process fn (MakeWith False pos str)

637+idemodeProcess fn (MakeCase False pos str) = process fn (MakeCase False pos str)

635638idemodeProcess fn (DoProofSearch False r pos str xs) = process fn (DoProofSearch False r pos str xs)

636639idemodeProcess fn (SetConsoleWidth w) = do process fn (SetConsoleWidth w)

637640 iPrintResult ""

@@ -1049,6 +1052,8 @@ process fn (AddMissing updatefile l n)

10491052 = addMissing fn updatefile l n

10501053process fn (MakeWith updatefile l n)

10511054 = makeWith fn updatefile l n

1055+process fn (MakeCase updatefile l n)

1056+ = makeCase fn updatefile l n

10521057process fn (MakeLemma updatefile l n)

10531058 = makeLemma fn updatefile l n

10541059process fn (DoProofSearch updatefile rec l n hints)

src/Idris/REPLParser.hs+2

@@ -123,6 +123,8 @@ parserCommands =

123123 ":am <line> <name> adds all missing pattern matches for the name on the line"

124124 , proofArgCmd ["mw", "makewith"] MakeWith

125125 ":mw <line> <name> adds a with clause for the definition of the name on the line"

126+ , proofArgCmd ["mc", "makecase"] MakeCase

127+ ":mc <line> <name> adds a case block for the definition of the metavariable on the line"

126128 , proofArgCmd ["ml", "makelemma"] MakeLemma "?"

127129 , (["log"], NumberArg, "Set logging verbosity level", cmd_log)

128130 , (["lto", "loadto"], SeqArgs NumberArg FileArg