Skip to content

Commit

Permalink
Filter out properties to check only ones exported.
Browse files Browse the repository at this point in the history
  • Loading branch information
mccleeary-galois committed Mar 14, 2024
1 parent 5bbc3dc commit 6c3bcc5
Show file tree
Hide file tree
Showing 5 changed files with 33 additions and 1 deletion.
2 changes: 1 addition & 1 deletion src/Cryptol/REPL/Monad.hs
Original file line number Diff line number Diff line change
Expand Up @@ -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 ]
Expand Down
5 changes: 5 additions & 0 deletions tests/issues/issue1621/a.cry
Original file line number Diff line number Diff line change
@@ -0,0 +1,5 @@
module a where

private

property x = True
3 changes: 3 additions & 0 deletions tests/issues/issue1621/b.cry
Original file line number Diff line number Diff line change
@@ -0,0 +1,3 @@
module b where

import a
7 changes: 7 additions & 0 deletions tests/issues/issue1621/issue1621.icry
Original file line number Diff line number Diff line change
@@ -0,0 +1,7 @@
:m a
x
:m b
x
:check x
:check a::x
:check
17 changes: 17 additions & 0 deletions tests/issues/issue1621/issue1621.icry.stdout
Original file line number Diff line number Diff line change
@@ -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.

0 comments on commit 6c3bcc5

Please sign in to comment.