diff --git a/src/TTImp/Elab/Local.idr b/src/TTImp/Elab/Local.idr index d4c7b81e44..6107e8d1eb 100644 --- a/src/TTImp/Elab/Local.idr +++ b/src/TTImp/Elab/Local.idr @@ -54,9 +54,7 @@ localHelper {vars} nest env nestdecls_in func else nestdeclsVis let defNames = definedInBlock emptyNS nestdeclsMult - names' <- traverse (applyEnv f) - (nub defNames) -- binding names must be unique - -- fixes bug #115 + names' <- traverse (applyEnv f) defNames let nest' = { names $= (names' ++) } nest let env' = dropLinear env -- We don't want to keep rechecking delayed elaborators in the diff --git a/src/TTImp/TTImp.idr b/src/TTImp/TTImp.idr index bd57502729..0c1bd6e125 100644 --- a/src/TTImp/TTImp.idr +++ b/src/TTImp/TTImp.idr @@ -13,6 +13,8 @@ import Data.List import Data.List1 import Data.Maybe +import Libraries.Data.SortedSet + %default covering -- Information about names in nested blocks @@ -772,7 +774,7 @@ export definedInBlock : Namespace -> -- namespace to resolve names List ImpDecl -> List Name definedInBlock ns decls = - concatMap (defName ns) decls + SortedSet.toList $ foldl (defName ns) empty decls where getName : ImpTy -> Name getName (MkImpTy _ _ n _) = n @@ -788,17 +790,17 @@ definedInBlock ns decls = DN _ _ => NS ns n _ => n - defName : Namespace -> ImpDecl -> List Name - defName ns (IClaim _ _ _ _ ty) = [expandNS ns (getName ty)] - defName ns (IDef _ nm _) = [expandNS ns nm] - defName ns (IData _ _ _ (MkImpData _ n _ _ cons)) - = expandNS ns n :: map (expandNS ns) (map getName cons) - defName ns (IData _ _ _ (MkImpLater _ n _)) = [expandNS ns n] - defName ns (IParameters _ _ pds) = concatMap (defName ns) pds - defName ns (IFail _ _ nds) = concatMap (defName ns) nds - defName ns (INamespace _ n nds) = concatMap (defName (ns <.> n)) nds - defName ns (IRecord _ fldns _ _ (MkImpRecord _ n _ opts con flds)) - = expandNS ns con :: all + defName : Namespace -> SortedSet Name -> ImpDecl -> SortedSet Name + defName ns acc (IClaim _ _ _ _ ty) = insert (expandNS ns (getName ty)) acc + defName ns acc (IDef _ nm _) = insert (expandNS ns nm) acc + defName ns acc (IData _ _ _ (MkImpData _ n _ _ cons)) + = foldl (flip insert) acc $ expandNS ns n :: map (expandNS ns . getName) cons + defName ns acc (IData _ _ _ (MkImpLater _ n _)) = insert (expandNS ns n) acc + defName ns acc (IParameters _ _ pds) = foldl (defName ns) acc pds + defName ns acc (IFail _ _ nds) = foldl (defName ns) acc nds + defName ns acc (INamespace _ n nds) = foldl (defName (ns <.> n)) acc nds + defName ns acc (IRecord _ fldns _ _ (MkImpRecord _ n _ opts con flds)) + = foldl (flip insert) acc $ expandNS ns con :: all where fldns' : Namespace fldns' = maybe ns (\ f => ns <.> mkNamespace f) fldns @@ -823,8 +825,8 @@ definedInBlock ns decls = all : List Name all = expandNS ns n :: map (expandNS fldns') (fnsRF ++ fnsUN) - defName ns (IPragma _ pns _) = map (expandNS ns) pns - defName _ _ = [] + defName ns acc (IPragma _ pns _) = foldl (flip insert) acc $ map (expandNS ns) pns + defName _ acc _ = acc export isIVar : RawImp' nm -> Maybe (FC, nm)