c2b01cc · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

mkUniqueName fix

Make user's names unique earlier (to save difficulty in alternative resolution, which is postponed). Also need to ensure names get added to the map in the right order for when resolving ambiguous names in alternatives. Fixes #3116

commitc2b01ccf5d8e4070000fe665200e7b7d902970a4 authorEdwin Brady <ecb10@st-andrews.ac.uk> dateFri 15 Apr 2016, 12:23 (11 years ago) parent6cbfdd3

2 files changed+9−4

compare with master

unifiedsplit

src/Idris/AbsSyntax.hs+8−3 src/Idris/AbsSyntaxTree.hs+1−1

src/Idris/AbsSyntax.hs+8−3

@@ -1691,7 +1691,7 @@ addImpl = addImpl' False [] []

16911691

16921692addImpl' :: Bool -> [Name] -> [Name] -> [Name] -> IState -> PTerm -> PTerm

16931693addImpl' inpat env infns imp_meths ist ptm

1694− = mkUniqueNames env [] (ai inpat False (zip env (repeat Nothing)) [] ptm)

1694+ = ai inpat False (zip env (repeat Nothing)) [] (mkUniqueNames env [] ptm)

16951695 where

16961696 topname = case ptm of

16971697 PRef _ _ n -> n

@@ -2272,7 +2272,8 @@ shadow n n' t = sm 0 t where

22722272 sm 0 (PTyped x y) = PTyped (sm 0 x) (sm 0 y)

22732273 sm 0 (PPair f hls p x y) = PPair f hls p (sm 0 x) (sm 0 y)

22742274 sm 0 (PDPair f hls p x t y) = PDPair f hls p (sm 0 x) (sm 0 t) (sm 0 y)

2275− sm 0 (PAlternative ms a as) = PAlternative ms a (map (sm 0) as)

2275+ sm 0 (PAlternative ms a as)

2276+ = PAlternative (map shadowAlt ms) a (map (sm 0) as)

22762277 sm 0 (PTactics ts) = PTactics (map (fmap (sm 0)) ts)

22772278 sm 0 (PProof ts) = PProof (map (fmap (sm 0)) ts)

22782279 sm 0 (PHidden x) = PHidden (sm 0 x)

@@ -2283,6 +2284,10 @@ shadow n n' t = sm 0 t where

22832284 sm ql (PUnquote tm) = PUnquote (sm (ql - 1) tm)

22842285 sm ql x = descend (sm ql) x

22852286

2287+ shadowAlt p@(x, oldn) = (update x, update oldn)

2288+ update oldn | n == oldn = n'

2289+ | otherwise = oldn

2290+

22862291-- | Rename any binders which are repeated (so that we don't have to mess

22872292-- about with shadowing anywhere else).

22882293mkUniqueNames :: [Name] -> [(Name, Name)] -> PTerm -> PTerm

@@ -2384,7 +2389,7 @@ mkUniqueNames env shadows tm

23842389 mkUniq 0 nmap (PAlternative ns b as)

23852390 -- store the nmap and defer the rest until we've pruned the set

23862391 -- during elaboration

2387− = return $ PAlternative (M.toList nmap ++ ns) b as

2392+ = return $ PAlternative (ns ++ M.toList nmap) b as

23882393 mkUniq 0 nmap (PHidden t) = liftM PHidden (mkUniq 0 nmap t)

23892394 mkUniq 0 nmap (PUnifyLog t) = liftM PUnifyLog (mkUniq 0 nmap t)

23902395 mkUniq 0 nmap (PDisamb n t) = liftM (PDisamb n) (mkUniq 0 nmap t)

src/Idris/AbsSyntaxTree.hs+1−1

@@ -2301,7 +2301,7 @@ allNamesIn tm = nub $ ni 0 [] tm

23012301 ni 0 env (PDPair _ _ _ (PRef _ _ n) Placeholder r) = n : ni 0 env r

23022302 ni 0 env (PDPair _ _ _ (PRef _ _ n) t r) = ni 0 env t ++ ni 0 (n:env) r

23032303 ni 0 env (PDPair _ _ _ l t r) = ni 0 env l ++ ni 0 env t ++ ni 0 env r

2304− ni 0 env (PAlternative ns a ls) = concatMap (ni 0 env) ls

2304+ ni 0 env (PAlternative ns a ls) = map snd ns ++ concatMap (ni 0 env) ls

23052305 ni 0 env (PUnifyLog tm) = ni 0 env tm

23062306 ni 0 env (PDisamb _ tm) = ni 0 env tm

23072307 ni 0 env (PNoImplicits tm) = ni 0 env tm