Skip to content

Commit

Permalink
[ fix ] Ensure local defs with no claim are local
Browse files Browse the repository at this point in the history
  • Loading branch information
dunhamsteve committed Jul 16, 2023
1 parent 6729fa8 commit 5165c79
Show file tree
Hide file tree
Showing 8 changed files with 50 additions and 1 deletion.
1 change: 1 addition & 0 deletions src/TTImp/TTImp.idr
Original file line number Diff line number Diff line change
Expand Up @@ -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]
Expand Down
2 changes: 1 addition & 1 deletion tests/Main.idr
Original file line number Diff line number Diff line change
Expand Up @@ -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",
Expand Down
4 changes: 4 additions & 0 deletions tests/idris2/basic070/Issue2592.idr
Original file line number Diff line number Diff line change
@@ -0,0 +1,4 @@
bar = 3
where wat = 2
baz = 3
where wat = 2
6 changes: 6 additions & 0 deletions tests/idris2/basic070/Issue2593.idr
Original file line number Diff line number Diff line change
@@ -0,0 +1,6 @@
two: Nat
two = 2

bar: a -> a
bar x = x where
wat = two
9 changes: 9 additions & 0 deletions tests/idris2/basic070/Issue2782.idr
Original file line number Diff line number Diff line change
@@ -0,0 +1,9 @@
foo : Integer
foo =
let z : Int
z = 1
y = 1
in y

fee : Integer
fee = y
9 changes: 9 additions & 0 deletions tests/idris2/basic070/Issue3016.idr
Original file line number Diff line number Diff line change
@@ -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
14 changes: 14 additions & 0 deletions tests/idris2/basic070/expected
Original file line number Diff line number Diff line change
@@ -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)
6 changes: 6 additions & 0 deletions tests/idris2/basic070/run
Original file line number Diff line number Diff line change
@@ -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

0 comments on commit 5165c79

Please sign in to comment.