e1dc450 · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

on master help sign in

Pick unique names for rhs when case splitting

e1dc450Edwin Brady13 years ago

src/Idris/CaseSplit.hs+29−2

compare with master

unifiedsplit

@@ -190,12 +190,39 @@ splitOnLine l n fn = do

190-- iputStrLn (showSep "\n" (map show tms))

191 return tms -- "" -- not yet done...

192

193−replaceSplits :: String -> [[(Name, PTerm)]] -> [String]

193+replaceSplits :: String -> [[(Name, PTerm)]] -> Idris [String]

194−replaceSplits l ups = map (rep (expandBraces l)) ups

194+replaceSplits l ups = updateRHSs 1 (map (rep (expandBraces l)) ups)

195 where

196 rep str [] = str ++ "\n"

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

198

199+ updateRHSs i [] = return []

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

201+ xs' <- updateRHSs i' xs

202+ return (x' : xs')

203+

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

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

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

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

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

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

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

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

212+

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+

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

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

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

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

201 nshow brack (PRef _ (UN "Z")) = "Z"

228 nshow brack (PRef _ (UN "Z")) = "Z"

src/Idris/ElabTerm.hs−1

@@ -530,7 +530,6 @@ elab ist info pattern tcgen fn tm

530 = let args' = map (shadowed (allNamesIn l)) args

531 lhs = PApp (getFC fc l) (PRef (getFC fc l) n)

532 (map pexp args' ++ [pexp l]) in

533−-- trace (show (getFC fc l, getFC fc r)) $

534 PClause (getFC fc l) n lhs [] r []

533 PClause (getFC fc l) n lhs [] r []

535

534

536 shadowed new (PRef _ n) | n `elem` new = Placeholder

535 shadowed new (PRef _ n) | n `elem` new = Placeholder

src/Idris/REPL.hs+2−1

@@ -506,7 +506,8 @@ process h fn (CaseSplitAt updatefile l n)

506 res <- splitOnLine l n fn

507 iLOG (showSep "\n" (map show res))

508 let (before, (ap : later)) = splitAt (l-1) (lines src)

509+ res' <- replaceSplits ap res

509− let new = concat (replaceSplits ap res)

510+ let new = concat res'

510 if updatefile then

511 if updatefile then

511 do let fb = fn ++ "~" -- make a backup!

512 do let fb = fn ++ "~" -- make a backup!

512 runIO $ writeFile fb (unlines before ++ new ++ unlines later)

513 runIO $ writeFile fb (unlines before ++ new ++ unlines later)