6408457 · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

Reduce work allNamesIn has to do

This is a major performance hit when functions get big (especially in do blocks) and a lot of the work it's doing is not actually necessary since the primary goal is to find shadowed names. So, only search alternatives if they are genuine alternatives rather than there for name disambiguation. Also reduce the reliance on uniplate a little bit, since this causes some (smaller) performance problems too.

commit64084571d368269c0bd565e99d1ecb2fad4ff1fc authorEdwin Brady <ecb10@st-andrews.ac.uk> dateThu 19 Apr 2018, 12:36 (8 years ago) parentd0e0680

1 file changed+16−1

compare with master

unifiedsplit

src/Idris/AbsSyntaxTree.hs+16−1

src/Idris/AbsSyntaxTree.hs+16−1

@@ -51,7 +51,6 @@ import Data.Traversable (Traversable)

5151import Data.Typeable

5252import GHC.Generics (Generic)

5353

54−

5554data ElabWhat = ETypes | EDefns | EAll

5655 deriving (Show, Eq)

5756

@@ -2279,25 +2278,41 @@ allNamesIn tm = nub $ ni 0 [] tm

22792278 ni 0 env (PPatvar _ n) = [n]

22802279 ni 0 env (PApp _ f as) = ni 0 env f ++ concatMap (ni 0 env . getTm) as

22812280 ni 0 env (PAppBind _ f as) = ni 0 env f ++ concatMap (ni 0 env . getTm) as

2281+ ni 0 env (PWithApp _ f a) = ni 0 env f ++ ni 0 env a

2282+ ni 0 env (PAppImpl t _) = ni 0 env t

22822283 ni 0 env (PCase _ c os) = ni 0 env c ++ concatMap (ni 0 env . snd) os

22832284 ni 0 env (PIfThenElse _ c t f) = ni 0 env c ++ ni 0 env t ++ ni 0 env f

22842285 ni 0 env (PLam fc n _ ty sc) = ni 0 env ty ++ ni 0 (n:env) sc

22852286 ni 0 env (PPi p n _ ty sc) = niTacImp 0 env p ++ ni 0 env ty ++ ni 0 (n:env) sc

22862287 ni 0 env (PLet _ _ n _ ty val sc) = ni 0 env ty ++ ni 0 env val ++ ni 0 (n:env) sc

22872288 ni 0 env (PHidden tm) = ni 0 env tm

2289+ ni 0 env (PGoal _ t _ sc) = ni 0 env t ++ ni 0 env sc

2290+ ni 0 env (PIdiom _ tm) = ni 0 env tm

22882291 ni 0 env (PRewrite _ _ l r _) = ni 0 env l ++ ni 0 env r

22892292 ni 0 env (PTyped l r) = ni 0 env l ++ ni 0 env r

22902293 ni 0 env (PPair _ _ _ l r) = ni 0 env l ++ ni 0 env r

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

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

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

2297+ ni 0 env (PAs _ _ tm) = ni 0 env tm

2298+ -- Just take the first, when disambiguating, since the shape will be

2299+ -- the same and we'll get the name root

2300+ ni 0 env (PAlternative ns (ExactlyOne _) (a : as))

2301+ = map snd ns ++ ni 0 env a

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

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

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

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

2306+ ni 0 env (PCoerced tm) = ni 0 env tm

2307+ ni 0 env (PRunElab _ tm _) = ni 0 env tm

2308+ ni 0 env (PConstSugar _ tm) = ni 0 env tm

2309+ ni 0 env tm@(PDoBlock _) = concatMap (ni 0 env) (children tm)

2310+ ni 0 env tm@(PProof _) = concatMap (ni 0 env) (children tm)

2311+ ni 0 env tm@(PTactics _) = concatMap (ni 0 env) (children tm)

22982312

22992313 ni i env (PQuasiquote tm ty) = ni (i+1) env tm ++ maybe [] (ni i env) ty

23002314 ni i env (PUnquote tm) = ni (i - 1) env tm

2315+ ni 0 env tm = []

23012316 ni i env tm = concatMap (ni i env) (children tm)

23022317

23032318 niTacImp i env (TacImp _ _ scr _) = ni i env scr