mirror of
https://github.com/ilyakooo0/Idris-dev.git
synced 2024-10-26 18:02:24 +03:00
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.
This commit is contained in:
parent
d0e06806a2
commit
64084571d3
@ -51,7 +51,6 @@ import Data.Traversable (Traversable)
|
||||
import Data.Typeable
|
||||
import GHC.Generics (Generic)
|
||||
|
||||
|
||||
data ElabWhat = ETypes | EDefns | EAll
|
||||
deriving (Show, Eq)
|
||||
|
||||
@ -2279,25 +2278,41 @@ allNamesIn tm = nub $ ni 0 [] tm
|
||||
ni 0 env (PPatvar _ n) = [n]
|
||||
ni 0 env (PApp _ f as) = ni 0 env f ++ concatMap (ni 0 env . getTm) as
|
||||
ni 0 env (PAppBind _ f as) = ni 0 env f ++ concatMap (ni 0 env . getTm) as
|
||||
ni 0 env (PWithApp _ f a) = ni 0 env f ++ ni 0 env a
|
||||
ni 0 env (PAppImpl t _) = ni 0 env t
|
||||
ni 0 env (PCase _ c os) = ni 0 env c ++ concatMap (ni 0 env . snd) os
|
||||
ni 0 env (PIfThenElse _ c t f) = ni 0 env c ++ ni 0 env t ++ ni 0 env f
|
||||
ni 0 env (PLam fc n _ ty sc) = ni 0 env ty ++ ni 0 (n:env) sc
|
||||
ni 0 env (PPi p n _ ty sc) = niTacImp 0 env p ++ ni 0 env ty ++ ni 0 (n:env) sc
|
||||
ni 0 env (PLet _ _ n _ ty val sc) = ni 0 env ty ++ ni 0 env val ++ ni 0 (n:env) sc
|
||||
ni 0 env (PHidden tm) = ni 0 env tm
|
||||
ni 0 env (PGoal _ t _ sc) = ni 0 env t ++ ni 0 env sc
|
||||
ni 0 env (PIdiom _ tm) = ni 0 env tm
|
||||
ni 0 env (PRewrite _ _ l r _) = ni 0 env l ++ ni 0 env r
|
||||
ni 0 env (PTyped l r) = ni 0 env l ++ ni 0 env r
|
||||
ni 0 env (PPair _ _ _ l r) = ni 0 env l ++ ni 0 env r
|
||||
ni 0 env (PDPair _ _ _ (PRef _ _ n) Placeholder r) = n : ni 0 env r
|
||||
ni 0 env (PDPair _ _ _ (PRef _ _ n) t r) = ni 0 env t ++ ni 0 (n:env) r
|
||||
ni 0 env (PDPair _ _ _ l t r) = ni 0 env l ++ ni 0 env t ++ ni 0 env r
|
||||
ni 0 env (PAs _ _ tm) = ni 0 env tm
|
||||
-- Just take the first, when disambiguating, since the shape will be
|
||||
-- the same and we'll get the name root
|
||||
ni 0 env (PAlternative ns (ExactlyOne _) (a : as))
|
||||
= map snd ns ++ ni 0 env a
|
||||
ni 0 env (PAlternative ns a ls) = map snd ns ++ concatMap (ni 0 env) ls
|
||||
ni 0 env (PUnifyLog tm) = ni 0 env tm
|
||||
ni 0 env (PDisamb _ tm) = ni 0 env tm
|
||||
ni 0 env (PNoImplicits tm) = ni 0 env tm
|
||||
ni 0 env (PCoerced tm) = ni 0 env tm
|
||||
ni 0 env (PRunElab _ tm _) = ni 0 env tm
|
||||
ni 0 env (PConstSugar _ tm) = ni 0 env tm
|
||||
ni 0 env tm@(PDoBlock _) = concatMap (ni 0 env) (children tm)
|
||||
ni 0 env tm@(PProof _) = concatMap (ni 0 env) (children tm)
|
||||
ni 0 env tm@(PTactics _) = concatMap (ni 0 env) (children tm)
|
||||
|
||||
ni i env (PQuasiquote tm ty) = ni (i+1) env tm ++ maybe [] (ni i env) ty
|
||||
ni i env (PUnquote tm) = ni (i - 1) env tm
|
||||
ni 0 env tm = []
|
||||
ni i env tm = concatMap (ni i env) (children tm)
|
||||
|
||||
niTacImp i env (TacImp _ _ scr _) = ni i env scr
|
||||
|
Loading…
Reference in New Issue
Block a user