f866fec · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

on master help sign in

Use Set for unique name checking for efficiency

f866fecEdwin Brady12 years ago

src/Idris/AbsSyntax.hs+25−24

compare with master

unifiedsplit

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

21import Control.Monad.State

22import Control.Monad.Error(throwError)

24−import Data.List

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

25import Data.Char

26import qualified Data.Text as T

27import Data.Either

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

498

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

500addDeferred' 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

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

503 i <- getIState

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

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

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

508 -- needed in tactic scripts

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

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

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

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

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

512 tidyNames used (Bind n b sc)

513− = let n' = uniqueName n used in

513+ = let n' = uniqueNameSet n used in

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

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

515 tidyNames used b = b

516

517solveDeferred :: Name -> Idris ()

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

1909-- about with shadowing anywhere else).

1910

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

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

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

1913+ inScope :: S.Set Name

1913− inScope = boundNamesIn tm

1914+ inScope = S.fromList $ boundNamesIn tm

1914

1915

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

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

1916 return (arg { getTm = t' })

1917 return (arg { getTm = t' })

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

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

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

1926 mkUniqT tac = return tac

1927 mkUniqT tac = return tac

1927

1928

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

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

1929 mkUniq (PLam n ty sc)

1930 mkUniq (PLam n ty sc)

1930 = do env <- get

1931 = do env <- get

1931 (n', sc') <-

1932 (n', sc') <-

1932− if n `elem` env

1933+ if n `S.member` env

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

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

1934− (env ++ inScope)

1935+ (S.union env inScope)

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

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

1936 else return (n, sc)

1937 else return (n, sc)

1937− put (n' : env)

1938+ put (S.insert n' env)

1938 ty' <- mkUniq ty

1939 ty' <- mkUniq ty

1939 sc'' <- mkUniq sc'

1940 sc'' <- mkUniq sc'

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

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

1941 mkUniq (PPi p n ty sc)

1942 mkUniq (PPi p n ty sc)

1942 = do env <- get

1943 = do env <- get

1943 (n', sc') <-

1944 (n', sc') <-

1944− if n `elem` env

1945+ if n `S.member` env

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

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

1946− (env ++ inScope)

1947+ (S.union env inScope)

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

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

1948 else return (n, sc)

1949 else return (n, sc)

1949− put (n' : env)

1950+ put (S.insert n' env)

1950 ty' <- mkUniq ty

1951 ty' <- mkUniq ty

1951 sc'' <- mkUniq sc'

1952 sc'' <- mkUniq sc'

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

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

1953 mkUniq (PLet n ty val sc)

1954 mkUniq (PLet n ty val sc)

1954 = do env <- get

1955 = do env <- get

1955 (n', sc') <-

1956 (n', sc') <-

1956− if n `elem` env

1957+ if n `S.member` env

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

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

1958− (env ++ inScope)

1959+ (S.union env inScope)

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

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

1960 else return (n, sc)

1961 else return (n, sc)

1961− put (n' : env)

1962+ put (S.insert n' env)

1962 ty' <- mkUniq ty; val' <- mkUniq val

1963 ty' <- mkUniq ty; val' <- mkUniq val

1963 sc'' <- mkUniq sc'

1964 sc'' <- mkUniq sc'

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

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

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

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

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

1982 | t /= Placeholder

1983 | t /= Placeholder

1983 = do env <- get

1984 = do env <- get

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

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

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

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

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

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

1987 else return (n, sc)

1988 else return (n, sc)

1988− put (n' : env)

1989+ put (S.insert n' env)

1989 t' <- mkUniq t

1990 t' <- mkUniq t

1990 sc'' <- mkUniq sc'

1991 sc'' <- mkUniq sc'

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

1992 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

29import Data.Char

30import Numeric (showIntAtBase)

31import qualified Data.Text as T

32−import Data.List

32+import Data.List hiding (insert)

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

33import Data.Maybe (listToMaybe)

34import Data.Maybe (listToMaybe)

34import Data.Foldable (Foldable)

35import Data.Foldable (Foldable)

35import Data.Traversable (Traversable)

36import Data.Traversable (Traversable)

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

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

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

1137 | otherwise = n

1138 | otherwise = n

1138

1139

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

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

1142+ | otherwise = n

1143+

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

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

1140−uniqueBinders ns (Bind n b sc)

1145+uniqueBinders ns = ubSet (fromList ns) where

1141− = let n' = uniqueName n ns

1146+ ubSet ns (Bind n b sc)

1147+ = let n' = uniqueNameSet n ns

1142− ns' = n' : ns in

1148+ ns' = insert n' ns in

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

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

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

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

1145−uniqueBinders ns t = t

1151+ ubSet ns t = t

1146

1152

1147

1153

1148nextName (NS x s) = NS (nextName x) s

1154nextName (NS x s) = NS (nextName x) s

src/Idris/ElabTerm.hs+17−11

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

319 let (tc, _) = unApply ty

320 env <- get_env

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

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

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

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

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

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

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

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

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

325 showHd (PRef _ n) = n

327 showHd (PRef _ n) = n

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

1034

1036

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

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

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

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

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

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

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

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

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

1039pruneByType env t c as

1042pruneByType env t c as

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

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

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

1048 getName (PApp _ f _) = getName f

1051 getName (PApp _ f _) = getName f

1049 getName _ = Nothing

1052 getName _ = Nothing

1050

1053

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

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

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

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

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

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

1054 | otherwise

1057 | otherwise

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

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

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

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

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

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

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

1067

1070

1068 typeHead var f f'

1071 typeHead var f f'

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

1069− = case lookupTy f' c of

1073+ case lookupTy f' ctxt of

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

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

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

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

1071− case unApply (getRetTy ty') of

1077+ case unApply (getRetTy ty') of

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

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

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

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

1074− _ -> False

1080+ _ -> False

1075− _ -> False

1081+ _ -> False

1076

1082

1077pruneByType _ t _ as = as

1083pruneByType _ t _ as = as

1078

1084