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

src/Idris/AbsSyntaxTree.hs+1

compare with master

unifiedsplit

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

402 | AddProofClauseFrom Bool Int Name

403 | AddMissing Bool Int Name

404 | MakeWith Bool Int Name

405+ | MakeCase Bool Int Name

405 | MakeLemma Bool Int Name

406 | MakeLemma Bool Int Name

406 | DoProofSearch Bool Bool Int Name [Name]

407 | DoProofSearch Bool Bool Int Name [Name]

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

408 -- ^ 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)

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

266

267 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

269 xs' <- updateRHSs i' xs

270 return (x' : xs')

271

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

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

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

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

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

274− updateRHS i ('?':xs) = do let (nm, rest) = span (not . isSpace) 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

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

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

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

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

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

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

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

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

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

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

280

285

281

286

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

287 -- 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

229 | AddProofClause Int String

230 | AddMissing Int String

231 | MakeWithBlock Int String

232+ | MakeCaseBlock Int String

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

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

233 | MakeLemma Int String

234 | MakeLemma Int String

234 | LoadFile String (Maybe Int)

235 | LoadFile String (Maybe Int)

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

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

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

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

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

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

264sexpToCommand (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)

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

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

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

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

266-- arguments which can be done by unification.

268-- arguments which can be done by unification.

src/Idris/Interactive.hs+42−1

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

1{-# LANGUAGE PatternGuards #-}

2

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

4− addMissing, makeWith, doProofSearch,

4+ addMissing, makeWith, makeCase, doProofSearch,

5 makeLemma) where

6

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

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

158 else iPrintResult with

159 where getIndent s = length (takeWhile isSpace s)

160

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+

161

202

162doProofSearch :: FilePath -> Bool -> Bool ->

203doProofSearch :: FilePath -> Bool -> Bool ->

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

204 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) =

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

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

368 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))

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

637 iPrintResult ""

640 iPrintResult ""

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

1049 = addMissing fn updatefile l n

1052 = addMissing fn updatefile l n

1050process fn (MakeWith updatefile l n)

1053process fn (MakeWith updatefile l n)

1051 = makeWith fn updatefile l n

1054 = makeWith fn updatefile l n

1055+process fn (MakeCase updatefile l n)

1056+ = makeCase fn updatefile l n

1052process fn (MakeLemma updatefile l n)

1057process fn (MakeLemma updatefile l n)

1053 = makeLemma fn updatefile l n

1058 = makeLemma fn updatefile l n

1054process fn (DoProofSearch updatefile rec l n hints)

1059process fn (DoProofSearch updatefile rec l n hints)

src/Idris/REPLParser.hs+2

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

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

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

125 ":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"

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

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

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

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

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

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