From 6c3bcc5bec6e449bdd295256f2f46801f464a909 Mon Sep 17 00:00:00 2001
From: Ryan <mccleeary@galois.com>
Date: Thu, 14 Mar 2024 10:38:18 -0600
Subject: [PATCH] Filter out properties to check only ones exported.

---
 src/Cryptol/REPL/Monad.hs                    |  2 +-
 tests/issues/issue1621/a.cry                 |  5 +++++
 tests/issues/issue1621/b.cry                 |  3 +++
 tests/issues/issue1621/issue1621.icry        |  7 +++++++
 tests/issues/issue1621/issue1621.icry.stdout | 17 +++++++++++++++++
 5 files changed, 33 insertions(+), 1 deletion(-)
 create mode 100644 tests/issues/issue1621/a.cry
 create mode 100644 tests/issues/issue1621/b.cry
 create mode 100644 tests/issues/issue1621/issue1621.icry
 create mode 100644 tests/issues/issue1621/issue1621.icry.stdout

diff --git a/src/Cryptol/REPL/Monad.hs b/src/Cryptol/REPL/Monad.hs
index 1627dc810..bb5bb5757 100644
--- a/src/Cryptol/REPL/Monad.hs
+++ b/src/Cryptol/REPL/Monad.hs
@@ -642,7 +642,7 @@ getTypeNames  =
 getPropertyNames :: REPL ([(M.Name,M.IfaceDecl)],NameDisp)
 getPropertyNames =
   do fe <- getFocusedEnv
-     let xs = M.ifDecls (M.mctxDecls fe)
+     let xs = Map.filterWithKey (\n _ -> Set.member n (M.mctxExported fe)) (M.ifDecls (M.mctxDecls fe))
          ps = sortBy (comparing (from . M.nameLoc . fst))
               [ (x,d) | (x,d) <- Map.toList xs,
                     T.PragmaProperty `elem` M.ifDeclPragmas d ]
diff --git a/tests/issues/issue1621/a.cry b/tests/issues/issue1621/a.cry
new file mode 100644
index 000000000..91fc5cac1
--- /dev/null
+++ b/tests/issues/issue1621/a.cry
@@ -0,0 +1,5 @@
+module a where
+
+private
+
+property x = True
\ No newline at end of file
diff --git a/tests/issues/issue1621/b.cry b/tests/issues/issue1621/b.cry
new file mode 100644
index 000000000..b456bfb54
--- /dev/null
+++ b/tests/issues/issue1621/b.cry
@@ -0,0 +1,3 @@
+module b where
+
+import a
\ No newline at end of file
diff --git a/tests/issues/issue1621/issue1621.icry b/tests/issues/issue1621/issue1621.icry
new file mode 100644
index 000000000..83b805e3a
--- /dev/null
+++ b/tests/issues/issue1621/issue1621.icry
@@ -0,0 +1,7 @@
+:m a
+x
+:m b
+x
+:check x
+:check a::x
+:check
diff --git a/tests/issues/issue1621/issue1621.icry.stdout b/tests/issues/issue1621/issue1621.icry.stdout
new file mode 100644
index 000000000..0ccdab591
--- /dev/null
+++ b/tests/issues/issue1621/issue1621.icry.stdout
@@ -0,0 +1,17 @@
+Loading module Cryptol
+Loading module Cryptol
+Loading module a
+True
+Loading module Cryptol
+Loading module a
+Loading module b
+
+[error] at issue1621.icry:4:1--4:2
+    Value not in scope: x
+
+[error] at issue1621.icry:5:8--5:9
+    Value not in scope: x
+
+[error] at issue1621.icry:6:8--6:12
+    Value not in scope: a::x
+There are no properties in scope.