git.iko.soy/Idris-dev
on master help sign in
Merge pull request #1844 from david-christiansen/issue/1843

Default case for name generation + proper name supply for identity type

commite41c0f92787e7e09675a242bb794f871afcc090c authorDavid Christiansen <david@davidchristiansen.dk> dateMon 12 Jan 2015, 00:01 (12 years ago) parent35e604acd30b8e
2 files changed+2−1
compare with master
unifiedsplit
src/Idris/CaseSplit.hs+1−1 src/Idris/Core/TT.hs+1
src/Idris/CaseSplit.hs+1−1
@@ -361,7 +361,7 @@ getClause l fn fp
361361 getNameFrom i used (PPi _ _ _ _)
362362 = uniqueNameFrom (mkSupply [sUN "f", sUN "g"]) used
363363 getNameFrom i used (PApp fc f as) = getNameFrom i used f
364− getNameFrom i used (PEq _ _ _ _ _) = uniqueNameFrom [sUN "prf"] used
364+ getNameFrom i used (PEq _ _ _ _ _) = uniqueNameFrom (mkSupply [sUN "prf"]) used
365365 getNameFrom i used (PRef fc f)
366366 = case getNameHints i f of
367367 [] -> uniqueName (sUN "x") used
src/Idris/Core/TT.hs+1
@@ -1181,6 +1181,7 @@ getRetTy (Bind n (Pi _ _ _) sc) = getRetTy sc
11811181getRetTy sc = sc
11821182
11831183uniqueNameFrom :: [Name] -> [Name] -> Name
1184+uniqueNameFrom [] hs = uniqueName (nextName (sUN "x")) hs
11841185uniqueNameFrom (s : supply) hs
11851186 | s `elem` hs = uniqueNameFrom supply hs
11861187 | otherwise = s