Limit :check to return only locally defined properties (#1731)

src/Cryptol/REPL/Command.hs

@@ -505,7 +505,7 @@ qcCmd qcMode "" _pos _fnm =
                do let str = nameStr x
                   rPutStr $ "property " ++ str ++ " "
                   let texpr = T.EVar x
-                  let schema = M.ifDeclSig d
+                  let schema = T.dSignature d
                   nd <- M.mctxNameDisp <$> getFocusedEnv
                   let doc = fixNameDisp nd (pp texpr)
                   testReport <- qcExpr qcMode doc texpr schema
@@ -827,7 +827,7 @@ cmdProveSat isSat "" _pos _fnm =
                   then rPutStr $ ":sat "   ++ str ++ "\n\t"
                   else rPutStr $ ":prove " ++ str ++ "\n\t"
                 let texpr = T.EVar x
-                let schema = M.ifDeclSig d
+                let schema = T.dSignature d
                 nd <- M.mctxNameDisp <$> getFocusedEnv
                 let doc = fixNameDisp nd (pp texpr)
                 success <- proveSatExpr isSat (M.nameLoc x) doc texpr schema

src/Cryptol/REPL/Monad.hs

@@ -248,7 +248,7 @@ mkPrompt rw
         | M.isLoadedParamMod m loaded -> modName ++ "(parameterized)"
         | M.isLoadedInterface m loaded -> modName ++ "(interface)"
         | otherwise -> modName
-        where 
+        where
           modName = pretty m
           loaded = M.meLoadedModules (eModuleEnv rw)
 
@@ -646,15 +646,29 @@ getTypeNames  =
      return (map (show . pp) (Map.keys (M.namespaceMap M.NSType fNames)))
 
 -- | Return a list of property names, sorted by position in the file.
-getPropertyNames :: REPL ([(M.Name,M.IfaceDecl)],NameDisp)
+-- Only properties defined in the current module are returned, including
+-- private properties in the current module. Imported properties are not
+-- returned.
+getPropertyNames :: REPL ([(M.Name, T.Decl)], NameDisp)
 getPropertyNames =
-  do fe <- getFocusedEnv
-     let xs = 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 ]
+ do fe <- getFocusedEnv
+    let nd = M.mctxNameDisp fe
+    mblm <- fmap (lName =<<) getLoadedMod
+    case mblm of
+      Nothing -> pure ([], nd)
+      Just mn ->
+       do mb <- M.lookupModule mn <$> getModuleEnv
+          case mb of
+            Nothing -> pure ([], nd)
+            Just lm -> pure (ps, nd)
+              where
+                ps =
+                  sortBy (comparing (from . M.nameLoc . fst))
+                    [ (T.dName d,d)
+                    | d <- T.groupDecls =<< T.mDecls (M.lmdModule (M.lmData lm))
+                    , T.PragmaProperty `elem` T.dPragmas d
+                    ]
 
-     return (ps, M.mctxNameDisp fe)
 
 getModNames :: REPL [I.ModName]
 getModNames =

tests/docstrings/T10.cry

@@ -0,0 +1,30 @@
+/**
+```
+:check
+```
+*/
+module T10 where
+
+p : Bit
+property p = True
+
+submodule M where
+  q : Bit
+  property q = True
+
+  private
+    r : Bit
+    property r = True
+
+submodule F where
+  parameter
+    type N : #
+
+  s : Bit
+  property s = True
+
+  private
+    t : Bit
+    property t = True
+
+submodule F1 = submodule F where type N = 1

tests/docstrings/T10.icry

@@ -0,0 +1,2 @@
+:m T10
+:check-docstrings

tests/docstrings/T10.icry.stdout

@@ -0,0 +1,25 @@
+Loading module Cryptol
+Loading module Cryptol
+Loading module T10
+
+
+Checking T10
+
+:check
+property p Using exhaustive testing.
+Testing... Passed 1 tests.
+Q.E.D.
+property M::q Using exhaustive testing.
+Testing... Passed 1 tests.
+Q.E.D.
+property T10::M::r Using exhaustive testing.
+Testing... Passed 1 tests.
+Q.E.D.
+property F1::s Using exhaustive testing.
+Testing... Passed 1 tests.
+Q.E.D.
+property T10::F1::t Using exhaustive testing.
+Testing... Passed 1 tests.
+Q.E.D.
+
+Successes: 1, No fences: 11, Failures: 0

tests/issues/issue639.icry

@@ -2,3 +2,7 @@
 :check
 :prove
 :sat
+:m Issue639_M
+:check
+:prove
+:sat

tests/issues/issue639.icry.stdout

@@ -2,12 +2,17 @@ Loading module Cryptol
 Loading module Cryptol
 Loading module Issue639_M
 Loading module Issue639_C
-property Issue639_M::p Using exhaustive testing.
+There are no properties in scope.
+There are no properties in scope.
+There are no properties in scope.
+Loading module Cryptol
+Loading module Issue639_M
+property p Using exhaustive testing.
 Testing... Counterexample
-Issue639_M::p False = False
-:prove Issue639_M::p
+p False = False
+:prove p
 	Counterexample
-Issue639_M::p False = False
-:sat Issue639_M::p
+p False = False
+:sat p
 	Satisfiable
-Issue639_M::p True = True
+p True = True

tests/suiteb/ECDSAKeyPair.icry

@@ -1,2 +1,4 @@
+:m NISTCurves
+:check
 :l ECDSAKeyPair.cry
 :check

tests/suiteb/ECDSAKeyPair.icry.stdout

@@ -2,10 +2,6 @@ Loading module Cryptol
 Loading module Cryptol
 Loading module PrimeEC
 Loading module NISTCurves
-Loading module Main
-property p192_keypair_test Using exhaustive testing.
-Testing... Passed 1 tests.
-Q.E.D.
 property p192_valid_curve Using exhaustive testing.
 Testing... Passed 1 tests.
 Q.E.D.
@@ -15,15 +11,22 @@ Q.E.D.
 property p256_valid_curve Using exhaustive testing.
 Testing... Passed 1 tests.
 Q.E.D.
-property p224_keypair_test Using exhaustive testing.
-Testing... Passed 1 tests.
-Q.E.D.
 property p384_valid_curve Using exhaustive testing.
 Testing... Passed 1 tests.
 Q.E.D.
 property p521_valid_curve Using exhaustive testing.
 Testing... Passed 1 tests.
 Q.E.D.
+Loading module Cryptol
+Loading module PrimeEC
+Loading module NISTCurves
+Loading module Main
+property p192_keypair_test Using exhaustive testing.
+Testing... Passed 1 tests.
+Q.E.D.
+property p224_keypair_test Using exhaustive testing.
+Testing... Passed 1 tests.
+Q.E.D.
 property p256_keypair_test Using exhaustive testing.
 Testing... Passed 1 tests.
 Q.E.D.

tests/suiteb/ECDSASigGen.icry

@@ -1,2 +1,4 @@
+:m NISTCurves
+:check
 :l ECDSASigGen.cry
 :check

tests/suiteb/ECDSASigGen.icry.stdout

@@ -2,14 +2,9 @@ Loading module Cryptol
 Loading module Cryptol
 Loading module PrimeEC
 Loading module NISTCurves
-Loading module SuiteB
-Loading module Main
 property p192_valid_curve Using exhaustive testing.
 Testing... Passed 1 tests.
 Q.E.D.
-property p224_sha224_siggen Using exhaustive testing.
-Testing... Passed 1 tests.
-Q.E.D.
 property p224_valid_curve Using exhaustive testing.
 Testing... Passed 1 tests.
 Q.E.D.
@@ -22,6 +17,14 @@ Q.E.D.
 property p521_valid_curve Using exhaustive testing.
 Testing... Passed 1 tests.
 Q.E.D.
+Loading module Cryptol
+Loading module PrimeEC
+Loading module NISTCurves
+Loading module SuiteB
+Loading module Main
+property p224_sha224_siggen Using exhaustive testing.
+Testing... Passed 1 tests.
+Q.E.D.
 property p224_sha256_siggen Using exhaustive testing.
 Testing... Passed 1 tests.
 Q.E.D.

tests/suiteb/ECDSASigVerify.icry

@@ -1,2 +1,4 @@
+:m NISTCurves
+:check
 :l ECDSASigVerify.cry
 :check

tests/suiteb/ECDSASigVerify.icry.stdout

@@ -2,14 +2,9 @@ Loading module Cryptol
 Loading module Cryptol
 Loading module PrimeEC
 Loading module NISTCurves
-Loading module SuiteB
-Loading module Main
 property p192_valid_curve Using exhaustive testing.
 Testing... Passed 1 tests.
 Q.E.D.
-property p192_sha224_sigverify Using exhaustive testing.
-Testing... Passed 1 tests.
-Q.E.D.
 property p224_valid_curve Using exhaustive testing.
 Testing... Passed 1 tests.
 Q.E.D.
@@ -22,6 +17,14 @@ Q.E.D.
 property p521_valid_curve Using exhaustive testing.
 Testing... Passed 1 tests.
 Q.E.D.
+Loading module Cryptol
+Loading module PrimeEC
+Loading module NISTCurves
+Loading module SuiteB
+Loading module Main
+property p192_sha224_sigverify Using exhaustive testing.
+Testing... Passed 1 tests.
+Q.E.D.
 property p192_sha256_sigverify Using exhaustive testing.
 Testing... Passed 1 tests.
 Q.E.D.