f869396 · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

Add :addmissing REPL command

:am [line] [name] gives the missing clauses for the [name] defined on line [line]. Correspondingly, :am! updates the source file.

commitf8693964f30af86d5e54644ad499c5aea40ecc4b authorEdwin Brady <ecb10@st-andrews.ac.uk> dateWed 30 Oct 2013, 11:02 (13 years ago) parent3dfae18

5 files changed+55−13

compare with master

unifiedsplit

idris.cabal+4 src/Idris/AbsSyntaxTree.hs+1 src/Idris/CaseSplit.hs+14−13 src/Idris/REPL.hs+32 src/Idris/REPLParser.hs+4

idris.cabal+4

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

271271 test/test031/run

272272 test/test031/*.idr

273273 test/test031/expected

274+ test/test032/run

275+ test/test032/*.idr

276+ test/test032/input

277+ test/test032/expected

274278

275279source-repository head

276280 type: git

src/Idris/AbsSyntaxTree.hs+1

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

242242 | CaseSplit Name PTerm

243243 | CaseSplitAt Bool Int Name

244244 | AddClauseFrom Bool Int Name

245+ | AddMissing Bool Int Name

245246 | MakeWith Bool Int Name

246247 | DoProofSearch Bool Int Name

247248 | SetOpt Opt

src/Idris/CaseSplit.hs+14−13

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

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

44 getClause,

5− mkWith) where

5+ mkWith,

6+ getUniq, nameRoot) where

78-- splitting a variable in a pattern clause

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

210211 return (x : xs', i')

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

212213

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

225214

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

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

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

256245 | otherwise = tm

257246

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

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

259260 Name -> -- ^ Function name

260261 FilePath -> -- ^ Source file name

src/Idris/REPL.hs+32

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

567567 getIndent i n [] = 0

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

569569 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+

570602process h fn (MakeWith updatefile l n)

571603 = do src <- runIO $ readFile fn

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

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

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

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

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

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

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