f866fec · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

Use Set for unique name checking for efficiency

A list is fine in most cases, but we were getting some pathologically bad cases especially where there were lots of ambiguous names in large functions.

commitf866feca9f08976b591fd2cc346bc81cc9ff259c authorEdwin Brady <ecb10@st-andrews.ac.uk> dateSat 25 Oct 2014, 18:57 (12 years ago) parent7a1b64d

3 files changed+55−42

compare with master

unifiedsplit

src/Idris/AbsSyntax.hs+25−24 src/Idris/Core/TT.hs+13−7 src/Idris/ElabTerm.hs+17−11

src/Idris/AbsSyntax.hs+25−24

@@ -21,7 +21,7 @@ import Control.Applicative

2121import Control.Monad.State

2222import Control.Monad.Error(throwError)

2323

24−import Data.List

24+import Data.List hiding (insert,union)

2525import Data.Char

2626import qualified Data.Text as T

2727import Data.Either

@@ -498,7 +498,7 @@ addDeferredTyCon = addDeferred' (TCon 0 0)

498498

499499addDeferred' :: NameType -> [(Name, (Int, Maybe Name, Type, Bool))] -> Idris ()

500500addDeferred' nt ns

501− = do mapM_ (\(n, (i, _, t, _)) -> updateContext (addTyDecl n nt (tidyNames [] t))) ns

501+ = do mapM_ (\(n, (i, _, t, _)) -> updateContext (addTyDecl n nt (tidyNames S.empty t))) ns

502502 mapM_ (\(n, _) -> when (not (n `elem` primDefs)) $ addIBC (IBCMetavar n)) ns

503503 i <- getIState

504504 putIState $ i { idris_metavars = map (\(n, (i, top, _, isTopLevel)) -> (n, (top, i, isTopLevel))) ns ++

@@ -507,11 +507,11 @@ addDeferred' nt ns

507507 -- 'tidyNames' is to generate user accessible names in case they are

508508 -- needed in tactic scripts

509509 tidyNames used (Bind (MN i x) b sc)

510− = let n' = uniqueName (UN x) used in

511− Bind n' b $ tidyNames (n':used) sc

510+ = let n' = uniqueNameSet (UN x) used in

511+ Bind n' b $ tidyNames (S.insert n' used) sc

512512 tidyNames used (Bind n b sc)

513− = let n' = uniqueName n used in

514− Bind n' b $ tidyNames (n':used) sc

513+ = let n' = uniqueNameSet n used in

514+ Bind n' b $ tidyNames (S.insert n' used) sc

515515 tidyNames used b = b

516516

517517solveDeferred :: Name -> Idris ()

@@ -1909,8 +1909,9 @@ shadow n n' t = sm t where

19091909-- about with shadowing anywhere else).

19101910

19111911mkUniqueNames :: [Name] -> PTerm -> PTerm

1912−mkUniqueNames env tm = evalState (mkUniq tm) env where

1913− inScope = boundNamesIn tm

1912+mkUniqueNames env tm = evalState (mkUniq tm) (S.fromList env) where

1913+ inScope :: S.Set Name

1914+ inScope = S.fromList $ boundNamesIn tm

19141915

19151916 mkUniqA arg = do t' <- mkUniq (getTm arg)

19161917 return (arg { getTm = t' })

@@ -1925,40 +1926,40 @@ mkUniqueNames env tm = evalState (mkUniq tm) env where

19251926 -- long as there are no bindings inside tactics though.

19261927 mkUniqT tac = return tac

19271928

1928− mkUniq :: PTerm -> State [Name] PTerm

1929+ mkUniq :: PTerm -> State (S.Set Name) PTerm

19291930 mkUniq (PLam n ty sc)

19301931 = do env <- get

19311932 (n', sc') <-

1932− if n `elem` env

1933− then do let n' = uniqueName (initN n (length env))

1934− (env ++ inScope)

1933+ if n `S.member` env

1934+ then do let n' = uniqueNameSet (initN n (S.size env))

1935+ (S.union env inScope)

19351936 return (n', shadow n n' sc)

19361937 else return (n, sc)

1937− put (n' : env)

1938+ put (S.insert n' env)

19381939 ty' <- mkUniq ty

19391940 sc'' <- mkUniq sc'

19401941 return $! PLam n' ty' sc''

19411942 mkUniq (PPi p n ty sc)

19421943 = do env <- get

19431944 (n', sc') <-

1944− if n `elem` env

1945− then do let n' = uniqueName (initN n (length env))

1946− (env ++ inScope)

1945+ if n `S.member` env

1946+ then do let n' = uniqueNameSet (initN n (S.size env))

1947+ (S.union env inScope)

19471948 return (n', shadow n n' sc)

19481949 else return (n, sc)

1949− put (n' : env)

1950+ put (S.insert n' env)

19501951 ty' <- mkUniq ty

19511952 sc'' <- mkUniq sc'

19521953 return $! PPi p n' ty' sc''

19531954 mkUniq (PLet n ty val sc)

19541955 = do env <- get

19551956 (n', sc') <-

1956− if n `elem` env

1957− then do let n' = uniqueName (initN n (length env))

1958− (env ++ inScope)

1957+ if n `S.member` env

1958+ then do let n' = uniqueNameSet (initN n (S.size env))

1959+ (S.union env inScope)

19591960 return (n', shadow n n' sc)

19601961 else return (n, sc)

1961− put (n' : env)

1962+ put (S.insert n' env)

19621963 ty' <- mkUniq ty; val' <- mkUniq val

19631964 sc'' <- mkUniq sc'

19641965 return $! PLet n' ty' val' sc''

@@ -1981,11 +1982,11 @@ mkUniqueNames env tm = evalState (mkUniq tm) env where

19811982 mkUniq (PDPair fc p (PRef fc' n) t sc)

19821983 | t /= Placeholder

19831984 = do env <- get

1984− (n', sc') <- if n `elem` env

1985− then do let n' = uniqueName n (env ++ inScope)

1985+ (n', sc') <- if n `S.member` env

1986+ then do let n' = uniqueNameSet n (S.union env inScope)

19861987 return (n', shadow n n' sc)

19871988 else return (n, sc)

1988− put (n' : env)

1989+ put (S.insert n' env)

19891990 t' <- mkUniq t

19901991 sc'' <- mkUniq sc'

19911992 return $! PDPair fc p (PRef fc' n') t' sc''

src/Idris/Core/TT.hs+13−7

@@ -29,7 +29,8 @@ import qualified Data.Map.Strict as Map

2929import Data.Char

3030import Numeric (showIntAtBase)

3131import qualified Data.Text as T

32−import Data.List

32+import Data.List hiding (insert)

33+import Data.Set(Set, member, fromList, insert)

3334import Data.Maybe (listToMaybe)

3435import Data.Foldable (Foldable)

3536import Data.Traversable (Traversable)

@@ -1136,13 +1137,18 @@ uniqueName :: Name -> [Name] -> Name

11361137uniqueName n hs | n `elem` hs = uniqueName (nextName n) hs

11371138 | otherwise = n

11381139

1140+uniqueNameSet :: Name -> Set Name -> Name

1141+uniqueNameSet n hs | n `member` hs = uniqueNameSet (nextName n) hs

1142+ | otherwise = n

1143+

11391144uniqueBinders :: [Name] -> TT Name -> TT Name

1140−uniqueBinders ns (Bind n b sc)

1141− = let n' = uniqueName n ns

1142− ns' = n' : ns in

1143− Bind n' (fmap (uniqueBinders ns') b) (uniqueBinders ns' sc)

1144−uniqueBinders ns (App f a) = App (uniqueBinders ns f) (uniqueBinders ns a)

1145−uniqueBinders ns t = t

1145+uniqueBinders ns = ubSet (fromList ns) where

1146+ ubSet ns (Bind n b sc)

1147+ = let n' = uniqueNameSet n ns

1148+ ns' = insert n' ns in

1149+ Bind n' (fmap (ubSet ns') b) (ubSet ns' sc)

1150+ ubSet ns (App f a) = App (ubSet ns f) (ubSet ns a)

1151+ ubSet ns t = t

11461152

11471153

11481154nextName (NS x s) = NS (nextName x) s

src/Idris/ElabTerm.hs+17−11

@@ -319,7 +319,9 @@ elab ist info emode opts fn tm

319319 let (tc, _) = unApply ty

320320 env <- get_env

321321 let as' = pruneByType (map fst env) tc ctxt as

322−-- trace (show as ++ "\n ==> " ++ showSep ", " (map showTmImpls as')) $

322+-- trace (-- show tc ++ " " ++ show as ++ "\n ==> " ++

323+-- show (length as') ++ "\n" ++

324+-- showSep ", " (map showTmImpls as') ++ "\nEND") $

323325 tryAll (zip (map (elab' ina) as') (map showHd as'))

324326 where showHd (PApp _ (PRef _ n) _) = n

325327 showHd (PRef _ n) = n

@@ -1034,7 +1036,8 @@ pruneAlt xs = map prune xs

10341036

10351037-- Rule out alternatives that don't return the same type as the head of the goal

10361038-- (If there are none left as a result, do nothing)

1037−pruneByType :: [Name] -> Term -> Context -> [PTerm] -> [PTerm]

1039+pruneByType :: [Name] -> Term -> -- head of the goal

1040+ Context -> [PTerm] -> [PTerm]

10381041-- if an alternative has a locally bound name at the head, take it

10391042pruneByType env t c as

10401043 | Just a <- locallyBound as = [a]

@@ -1048,9 +1051,9 @@ pruneByType env t c as

10481051 getName (PApp _ f _) = getName f

10491052 getName _ = Nothing

10501053

1051−pruneByType env (P _ n _) c as

1054+pruneByType env (P _ n _) ctxt as

10521055-- if the goal type is polymorphic, keep e

1053− | [] <- lookupTy n c = as

1056+ | [] <- lookupTy n ctxt = as

10541057 | otherwise

10551058 = let asV = filter (headIs True n) as

10561059 as' = filter (headIs False n) as in

@@ -1066,13 +1069,16 @@ pruneByType env (P _ n _) c as

10661069 headIs _ _ _ = True -- keep if it's not an application

10671070

10681071 typeHead var f f'

1069− = case lookupTy f' c of

1070− [ty] -> let ty' = normalise c [] ty in

1071− case unApply (getRetTy ty') of

1072− (P _ ftyn _, _) -> ftyn == f

1073− (V _, _) -> var -- keep, variable

1074− _ -> False

1075− _ -> False

1072+ = -- trace ("Trying " ++ show f' ++ " for " ++ show n) $

1073+ case lookupTy f' ctxt of

1074+ [ty] -> case unApply (getRetTy ty) of

1075+ (P _ ctyn _, _) | isConName ctyn ctxt -> ctyn == f

1076+ _ -> let ty' = normalise ctxt [] ty in

1077+ case unApply (getRetTy ty') of

1078+ (P _ ftyn _, _) -> ftyn == f

1079+ (V _, _) -> var -- keep, variable

1080+ _ -> False

1081+ _ -> False

10761082

10771083pruneByType _ t _ as = as

10781084