f869396 · Idris-dev · git.iko.soy

idris.cabal+4

compare with master

unifiedsplit

@@ -271,6 +271,10 @@ Extra-source-files:

271 test/test031/run

272 test/test031/*.idr

273 test/test031/expected

274+ test/test032/run

275+ test/test032/*.idr

276+ test/test032/input

277+ test/test032/expected

274

278

275source-repository head

279source-repository head

276 type: git

280 type: git

src/Idris/AbsSyntaxTree.hs+1

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

242 | CaseSplit Name PTerm

243 | CaseSplitAt Bool Int Name

244 | AddClauseFrom Bool Int Name

245+ | AddMissing Bool Int Name

245 | MakeWith Bool Int Name

246 | MakeWith Bool Int Name

246 | DoProofSearch Bool Int Name

247 | DoProofSearch Bool Int Name

247 | SetOpt Opt

248 | SetOpt Opt

src/Idris/CaseSplit.hs+14−13

@@ -2,7 +2,8 @@

2

3module Idris.CaseSplit(split, splitOnLine, replaceSplits,

4 getClause,

5− mkWith) where

5+ mkWith,

6+ getUniq, nameRoot) where

6

7

7-- splitting a variable in a pattern clause

8-- splitting a variable in a pattern clause

8

9

@@ -210,18 +211,6 @@ replaceSplits l ups = updateRHSs 1 (map (rep (expandBraces l)) ups)

210 return (x : xs', i')

211 return (x : xs', i')

211 updateRHS i [] = return ("", i)

212 updateRHS i [] = return ("", i)

212

213

213− getUniq nm i

214− = do ist <- getIState

215− let n = nameRoot [] nm ++ "_" ++ show i

216− case lookupTy (UN n) (tt_ctxt ist) of

217− [] -> return (n, i+1)

218− _ -> getUniq nm (i+1)

219−

220− nameRoot acc nm | all isDigit nm = showSep "_" acc

221− nameRoot acc nm =

222− case span (/='_') nm of

223− (before, ('_' : after)) -> nameRoot (acc ++ [before]) after

224− _ -> showSep "_" (acc ++ [nm])

225

214

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

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

227 -- this isn't supported in a pattern, so special case here

216 -- this isn't supported in a pattern, so special case here

@@ -255,6 +244,18 @@ replaceSplits l ups = updateRHSs 1 (map (rep (expandBraces l)) ups)

255 addBrackets tm | ' ' `elem` tm = "(" ++ tm ++ ")"

244 addBrackets tm | ' ' `elem` tm = "(" ++ tm ++ ")"

256 | otherwise = tm

245 | otherwise = tm

257

246

247+getUniq nm i

248+ = do ist <- getIState

249+ let n = nameRoot [] nm ++ "_" ++ show i

250+ case lookupTy (UN n) (tt_ctxt ist) of

251+ [] -> return (n, i+1)

252+ _ -> getUniq nm (i+1)

253+

254+nameRoot acc nm | all isDigit nm = showSep "_" acc

255+nameRoot acc nm =

256+ case span (/='_') nm of

257+ (before, ('_' : after)) -> nameRoot (acc ++ [before]) after

258+ _ -> showSep "_" (acc ++ [nm])

258getClause :: Int -> -- ^ Line type is declared on

259getClause :: Int -> -- ^ Line type is declared on

259 Name -> -- ^ Function name

260 Name -> -- ^ Function name

260 FilePath -> -- ^ Source file name

261 FilePath -> -- ^ Source file name

src/Idris/REPL.hs+32

@@ -567,6 +567,38 @@ process h fn (AddClauseFrom updatefile l n)

567 getIndent i n [] = 0

568 getIndent i n xs | take (length n) xs == n = i

569 getIndent i n (x : xs) = getIndent (i + 1) n xs

570+process h fn (AddMissing updatefile l n)

571+ = do src <- runIO $ readFile fn

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

573+ i <- getIState

574+ cl <- getInternalApp fn l

575+ let n' = getAppName cl

576+ extras <- case lookupCtxt n' (idris_patdefs i) of

577+ [] -> return ""

578+ [(_, tms)] -> showNew (show n ++ "_rhs") 1 tms

579+ let (nonblank, rest) = span (not . all isSpace) (tyline:later)

580+ if updatefile then

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

582+ runIO $ writeFile fb (unlines (before ++ nonblank) ++

583+ extras ++ unlines rest)

584+ runIO $ copyFile fb fn

585+ else ihputStrLn h extras

586+ where showPat = show . stripNS

587+ stripNS tm = mapPT dens tm where

588+ dens (PRef fc n) = PRef fc (nsroot n)

589+ dens t = t

590+

591+ getAppName (PApp _ r _) = getAppName r

592+ getAppName (PRef _ r) = r

593+ getAppName _ = n

594+

595+ showNew nm i (tm : tms)

596+ = do (nm', i') <- getUniq nm i

597+ rest <- showNew nm i' tms

598+ return (showPat tm ++ " = ?" ++ nm' ++

599+ "\n" ++ rest)

600+ showNew nm i [] = return ""

601+

570process h fn (MakeWith updatefile l n)

602process h fn (MakeWith updatefile l n)

571 = do src <- runIO $ readFile fn

603 = do src <- runIO $ readFile fn

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

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

src/Idris/REPLParser.hs+4

@@ -73,6 +73,10 @@ pCmd = do P.whiteSpace; try (do cmd ["q", "quit"]; eof; return Quit)

73 upd <- option False (do P.lchar '!'; return True)

74 l <- P.natural; n <- P.name;

75 return (AddClauseFrom upd (fromInteger l) n))

76+ <|> try (do cmd ["am", "addmissing"]; P.whiteSpace;

77+ upd <- option False (do P.lchar '!'; return True)

78+ l <- P.natural; n <- P.name;

79+ return (AddMissing upd (fromInteger l) n))

76 <|> try (do cmd ["mw", "makewith"]; P.whiteSpace;

80 <|> try (do cmd ["mw", "makewith"]; P.whiteSpace;

77 upd <- option False (do P.lchar '!'; return True)

81 upd <- option False (do P.lchar '!'; return True)

78 l <- P.natural; n <- P.name;

82 l <- P.natural; n <- P.name;