From 5165c79b671f0ae5cd300993561b66425d9abbb7 Mon Sep 17 00:00:00 2001 From: Steve Dunham Date: Sat, 15 Jul 2023 17:05:05 -0700 Subject: [PATCH 1/2] [ fix ] Ensure local defs with no claim are local --- src/TTImp/TTImp.idr | 1 + tests/Main.idr | 2 +- tests/idris2/basic070/Issue2592.idr | 4 ++++ tests/idris2/basic070/Issue2593.idr | 6 ++++++ tests/idris2/basic070/Issue2782.idr | 9 +++++++++ tests/idris2/basic070/Issue3016.idr | 9 +++++++++ tests/idris2/basic070/expected | 14 ++++++++++++++ tests/idris2/basic070/run | 6 ++++++ 8 files changed, 50 insertions(+), 1 deletion(-) create mode 100644 tests/idris2/basic070/Issue2592.idr create mode 100644 tests/idris2/basic070/Issue2593.idr create mode 100644 tests/idris2/basic070/Issue2782.idr create mode 100644 tests/idris2/basic070/Issue3016.idr create mode 100644 tests/idris2/basic070/expected create mode 100755 tests/idris2/basic070/run diff --git a/src/TTImp/TTImp.idr b/src/TTImp/TTImp.idr index 6e50dab44..bd5750272 100644 --- a/src/TTImp/TTImp.idr +++ b/src/TTImp/TTImp.idr @@ -790,6 +790,7 @@ definedInBlock ns decls = 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] diff --git a/tests/Main.idr b/tests/Main.idr index 9888cafcc..ae109ea3c 100644 --- a/tests/Main.idr +++ b/tests/Main.idr @@ -42,7 +42,7 @@ idrisTestsBasic = MkTestPool "Fundamental language features" [] Nothing "basic051", "basic052", "basic053", "basic054", "basic055", "basic056", "basic057", "basic058", "basic059", "basic060", "basic061", "basic062", "basic063", "basic064", "basic065", - "basic066", "basic067", "basic068", "basic069", + "basic066", "basic067", "basic068", "basic069", "basic070", "idiom001", "dotted001", "rewrite001", diff --git a/tests/idris2/basic070/Issue2592.idr b/tests/idris2/basic070/Issue2592.idr new file mode 100644 index 000000000..2e07c2b91 --- /dev/null +++ b/tests/idris2/basic070/Issue2592.idr @@ -0,0 +1,4 @@ +bar = 3 + where wat = 2 +baz = 3 + where wat = 2 diff --git a/tests/idris2/basic070/Issue2593.idr b/tests/idris2/basic070/Issue2593.idr new file mode 100644 index 000000000..93d3a14de --- /dev/null +++ b/tests/idris2/basic070/Issue2593.idr @@ -0,0 +1,6 @@ +two: Nat +two = 2 + +bar: a -> a +bar x = x where + wat = two diff --git a/tests/idris2/basic070/Issue2782.idr b/tests/idris2/basic070/Issue2782.idr new file mode 100644 index 000000000..9271e7201 --- /dev/null +++ b/tests/idris2/basic070/Issue2782.idr @@ -0,0 +1,9 @@ +foo : Integer +foo = + let z : Int + z = 1 + y = 1 + in y + +fee : Integer +fee = y diff --git a/tests/idris2/basic070/Issue3016.idr b/tests/idris2/basic070/Issue3016.idr new file mode 100644 index 000000000..1907ba378 --- /dev/null +++ b/tests/idris2/basic070/Issue3016.idr @@ -0,0 +1,9 @@ +import Data.String + +test str = len + where + xs = words str + len = length xs + +parameters (n : Nat) (strs : List String) + len = List.length strs diff --git a/tests/idris2/basic070/expected b/tests/idris2/basic070/expected new file mode 100644 index 000000000..90af640b7 --- /dev/null +++ b/tests/idris2/basic070/expected @@ -0,0 +1,14 @@ +1/1: Building Issue3016 (Issue3016.idr) +1/1: Building Issue2782 (Issue2782.idr) +Error: While processing right hand side of fee. Undefined name y. + +Issue2782:9:7--9:8 + 5 | y = 1 + 6 | in y + 7 | + 8 | fee : Integer + 9 | fee = y + ^ + +1/1: Building Issue2592 (Issue2592.idr) +1/1: Building Issue2593 (Issue2593.idr) diff --git a/tests/idris2/basic070/run b/tests/idris2/basic070/run new file mode 100755 index 000000000..59c5abe15 --- /dev/null +++ b/tests/idris2/basic070/run @@ -0,0 +1,6 @@ +rm -rf build + +$1 --no-color --console-width 0 --no-banner --check Issue3016.idr +$1 --no-color --console-width 0 --no-banner --check Issue2782.idr +$1 --no-color --console-width 0 --no-banner --check Issue2592.idr +$1 --no-color --console-width 0 --no-banner --check Issue2593.idr From 113c3930f353e81068acde0b34ec28628ae0bcc2 Mon Sep 17 00:00:00 2001 From: Steve Dunham Date: Sun, 16 Jul 2023 09:01:13 -0700 Subject: [PATCH 2/2] [ fix ] deduplicate definedInBlock results --- src/TTImp/Elab/Local.idr | 4 +--- src/TTImp/TTImp.idr | 30 ++++++++++++++++-------------- 2 files changed, 17 insertions(+), 17 deletions(-) diff --git a/src/TTImp/Elab/Local.idr b/src/TTImp/Elab/Local.idr index d4c7b81e4..6107e8d1e 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 bd5750272..0c1bd6e12 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)