c2b01cc · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

on master help sign in

mkUniqueName fix

c2b01ccEdwin Brady11 years ago

src/Idris/AbsSyntax.hs+8−3

compare with master

unifiedsplit

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

1691

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

1693addImpl' 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)

1695 where

1696 topname = case ptm of

1697 PRef _ _ n -> n

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

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

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

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

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

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

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

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

2278 sm 0 (PHidden x) = PHidden (sm 0 x)

2279 sm 0 (PHidden x) = PHidden (sm 0 x)

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

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

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

2284 sm ql x = descend (sm ql) x

2285 sm ql x = descend (sm ql) x

2285

2286

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

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

2289+ | otherwise = oldn

2290+

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

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

2287-- about with shadowing anywhere else).

2292-- about with shadowing anywhere else).

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

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

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

2384 mkUniq 0 nmap (PAlternative ns b as)

2389 mkUniq 0 nmap (PAlternative ns b as)

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

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

2386 -- during elaboration

2391 -- during elaboration

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

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

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

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

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

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

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

2395 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

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

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

2303 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

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

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

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