@@ -190,12 +190,39 @@ splitOnLine l n fn = do
190190-- iputStrLn (showSep "\n" (map show tms))
191191 return tms -- "" -- not yet done...
192192
193−replaceSplits :: String -> [[(Name, PTerm)]] -> [String]
194−replaceSplits l ups = map (rep (expandBraces l)) ups
193+replaceSplits :: String -> [[(Name, PTerm)]] -> Idris [String]
194+replaceSplits l ups = updateRHSs 1 (map (rep (expandBraces l)) ups)
195195 where
196196 rep str [] = str ++ "\n"
197197 rep str ((n, tm) : ups) = rep (updatePat False (show n) (nshow False tm) str) ups
198198
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+
199226 -- TMP HACK: If there are Nats, we don't want to show as numerals since
200227 -- this isn't supported in a pattern, so special case here
201228 nshow brack (PRef _ (UN "Z")) = "Z"