rem/enriching-properties

src/Cryptol/Parser.y

@@ -29,6 +29,7 @@ import           Control.Applicative as A
 import           Data.Maybe(fromMaybe)
 import           Data.List.NonEmpty ( NonEmpty(..), cons )
 import           Data.Text(Text)
+import qualified Data.Map as M
 import qualified Data.Text as T
 import           Control.Monad(liftM2,msum)
 
@@ -279,14 +280,34 @@ vtop_decls                 :: { [TopDecl PName]  }
   | vtop_decls 'v;' vtop_decl { $3 ++ $1 }
   | vtop_decls ';'  vtop_decl { $3 ++ $1 }
 
+property_option :: { (Text, Located Literal) }
+  : ':' ident ident '=' property_value {% (mkPropertyOption $2 $3 $5)}
+
+property_value :: { Located Literal } 
+  : aexpr {% mkOptionValue $1 }
+
+
+property_type :: { PropertyType }
+  : ident {% (mkPropertyType $1)}
+
+property_configuration :: { M.Map Text (Located Literal) }
+  : {- empty -} {mempty}
+  | property_configuration property_option {% addPropertyOption $2 $1 }
+
+property_pragma   :: { PropertyPragma }
+  : 'property' { DefaultPropertyPragma }
+  | 'property' ':' property_type property_configuration { ConfigurableProperty $3 $4}
+
+
 vtop_decl               :: { [TopDecl PName] }
   : decl                   { [exportDecl Nothing   Public $1]                 }
   | doc decl               { [exportDecl (Just $1) Public $2]                 }
+  -- TODO % means that the production of value could fail
   | mbDoc 'include' STRLIT {% (return . Include) `fmap` fromStrLit $3         }
-  | mbDoc 'property' name iapats '=' expr
-                           { [exportDecl $1 Public (mkProperty $3 $4 $6)]     }
-  | mbDoc 'property' name       '=' expr
-                           { [exportDecl $1 Public (mkProperty $3 [] $5)]     }
+  | mbDoc property_pragma name iapats '=' expr
+                           { [exportDecl $1 Public (mkProperty $3 $4 $6 $2)]     }
+  | mbDoc property_pragma name       '=' expr
+                           { [exportDecl $1 Public (mkProperty $3 [] $5 $2)]     }
   | mbDoc newtype          { [exportNewtype Public $1 $2]                     }
   | mbDoc enum             { [exportEnum Public $1 $2]                        }
   | prim_bind              { $1                                               }

src/Cryptol/Parser/AST.hs

@@ -66,6 +66,9 @@
   , BindDef(..), LBindDef
   , BindImpl(..), bindImpl, exprDef
   , Pragma(..)
+  , PropertyPragma(..)
+  , PropertyType(..)
+  , PropertyOptions
   , ExportType(..)
   , TopLevel(..)
   , Import, ImportG(..), ImportSpec(..), ImpName(..), impNameModPath
@@ -516,8 +519,19 @@
   }
   deriving (Eq,Generic,NFData,Functor,Show)
 
+data PropertyType = TestType
+                  | ProveType
+                  | SatType
+  deriving (Eq, Show, Generic, NFData)
+
+type PropertyOptions = Map Text (Located Literal)
+data PropertyPragma = DefaultPropertyPragma
+                    | ConfigurableProperty PropertyType PropertyOptions
+                    deriving (Eq, Show, Generic, NFData)
+
 data Pragma   = PragmaNote String
-              | PragmaProperty
+              | Property PropertyPragma
+
                 deriving (Eq, Show, Generic, NFData)
 
 data Newtype name = Newtype
@@ -1099,8 +1113,8 @@
 
 
 instance PP Pragma where
   ppPrec _ (PragmaNote x) = text x
-  ppPrec _ PragmaProperty = text "property"
+  ppPrec _ (Property DefaultPropertyPragma) = text "property"
 
 ppPragma :: PPName name => [Located name] -> Pragma -> Doc
 ppPragma xs p =
@@ -1567,8 +1581,8 @@
                  }
 
 instance NoPos Pragma where
   noPos p@(PragmaNote {})   = p
-  noPos p@(PragmaProperty)  = p
+  noPos p@(Property DefaultPropertyPragma)  = p
 
 
 

src/Cryptol/Parser/ParserUtils.hs

@@ -270,6 +270,11 @@
     _ -> panic "[Parser] fracLit" [ "Invalid fraction", show tok ]
 
 
+strVal :: Located Token -> ParseM String
+strVal l = case thing l of
+             Token (StrLit x) _ -> return x
+             _         -> errorMessage (srcRange l) ["Expected a String"]
+
 intVal :: Located Token -> ParseM Integer
 intVal tok =
   case tokenType (thing tok) of
@@ -753,15 +758,51 @@
                        ["Polynomial contains multiple terms with exponent " ++ show n]
     | otherwise     = mk (setBit res n) ns
 
+mkPropertyType :: LIdent -> ParseM PropertyType
+mkPropertyType propIdent =
+  case identText (thing propIdent) of
+     "test" -> pure TestType
+     "prove" -> pure ProveType
+     "sat" -> pure SatType
+     _ -> errorMessage (srcRange propIdent) ["Invalid property type.", "Valid options are `test`, `prove`, or `sat`."]
+
+mkOptionValue :: Expr PName -> ParseM (Located Literal)
+mkOptionValue = checkLoc Nothing
+   where 
+     checkLoc :: Maybe Range -> Expr PName -> ParseM (Located Literal)
+     checkLoc mbLoc expr = 
+      case expr of
+        ELocated e r -> checkLoc (Just r) e
+        ELit lit -> case mbLoc of 
+                      Just loc -> pure Located{srcRange = loc, thing = lit}
+                      Nothing -> expected "Literal"
+        _ -> 
+          case mbLoc of 
+            Just loc -> errorMessage loc ["Invalid property option." , "Expected a literal"]
+            Nothing -> expected "Literal"
+
+
+mkPropertyOption :: Located Ident -> Located Ident -> Located Literal -> ParseM (Text, Located Literal)
+mkPropertyOption setIdent settingIdent v = 
+   case identText (thing setIdent) of
+    "set" -> pure (identText (thing settingIdent), v)
+    _ -> errorMessage (srcRange setIdent) ["Invalid property option." , "To set a property option use `:set name = value`"]
+
+addPropertyOption :: (Text, Located Literal) -> Map.Map Text (Located Literal)  -> ParseM (Map.Map Text (Located Literal))
+addPropertyOption (t,ll) m = 
+  let (mbV, nMap) = Map.insertLookupWithKey (\ _ _ v -> v) t ll m in
+    case mbV of
+      Nothing -> pure nMap
+      Just _ -> errorMessage (srcRange ll) ["Invalid property option." , "This property option has already been set."]
 
 -- NOTE: The list of patterns is reversed!
-mkProperty :: LPName -> [Pattern PName] -> Expr PName -> Decl PName
-mkProperty f ps e = at (f,e) $
+mkProperty :: LPName -> [Pattern PName] -> Expr PName -> PropertyPragma -> Decl PName
+mkProperty f ps e pp = at (f,e) $
                     DBind Bind { bName       = f
                                , bParams     = reverse ps
                                , bDef        = at e (Located emptyRange (exprDef e))
                                , bSignature  = Nothing
-                               , bPragmas    = [PragmaProperty]
+                               , bPragmas    = [Property pp]
                                , bMono       = False
                                , bInfix      = False
                                , bFixity     = Nothing

src/Cryptol/REPL/Browse.hs

@@ -9,7 +9,7 @@ import Data.List(sortBy)
 import Data.Void (Void)
 import qualified Prettyprinter as PP
 
-import Cryptol.Parser.AST(Pragma(..))
+import Cryptol.Parser.AST(Pragma(..), PropertyPragma (..))
 import qualified Cryptol.TypeCheck.Type as T
 
 import Cryptol.Utils.PP
@@ -125,7 +125,7 @@ browseVars disp decls =
      ppSection disp "Properties" ppVar props
   ++ ppSection disp "Symbols"    ppVar syms
   where
-  isProp p     = PragmaProperty `elem` ifDeclPragmas p
+  isProp p     = (Property DefaultPropertyPragma) `elem` ifDeclPragmas p
   (props,syms) = Map.partition isProp (ifDecls decls)
 
   ppVar d      = nest 2 (sep [pp (ifDeclName d) <+> ":", pp (ifDeclSig d)])

src/Cryptol/REPL/Command.hs

@@ -146,6 +146,7 @@
 import Prelude.Compat
 
 import qualified Data.SBV.Internals as SBV (showTDiff)
+import Cryptol.Parser.AST (PropertyPragma(..))
 
 
 
@@ -236,6 +237,9 @@
   , CommandDescr [ ":s", ":set" ] ["[ OPTION [ = VALUE ] ]"] (OptionArg setOptionCmd)
     "Set an environmental option (:set on its own displays current values)."
     ""
+  , CommandDescr [ ":prop" ] ["[ EXPR ]"] (ExprArg propCmd)
+    "Use testing described by properties to check that property (default equivalent :check). \n(If no argument, check all properties.)"
+    ""
   , CommandDescr [ ":check" ] ["[ EXPR ]"] (ExprArg (qcCmd QCRandom))
     "Use random testing to check that the argument always returns true.\n(If no argument, check all properties.)"
     ""
@@ -475,6 +479,47 @@
      void (qcExpr qcMode doc texpr schema)
 
 
+--TODO Remove components that are not REPL specific from here.
+-- TODO We probably want a factor out the results of these into a data structure.
+propCmd :: String -> (Int,Int) -> Maybe FilePath -> REPL ()
+propCmd _ _pos _fnm = 
+  do 
+    (checks, dispCheck) <- getPropertiesOfType P.TestType
+    (proves, dispProv) <- getPropertiesOfType P.ProveType
+    (sats, dispSats) <- getPropertiesOfType P.SatType
+    let nameStrChecks x = show (fixNameDisp dispCheck (pp x))
+    if null checks
+        then rPutStrLn "There are no properties in scope."
+        else forM_ checks $ \(x,d,ops) ->
+               do let str = nameStrChecks x
+                  rPutStr $ "property " ++ str ++ " options " ++ propOptsShow ops ++ " "
+                  let texpr = T.EVar x
+                  let schema = M.ifDeclSig d
+                  nd <- M.mctxNameDisp <$> getFocusedEnv
+                  let doc = fixNameDisp nd (pp texpr)
+                  void (qcExpr QCRandom doc texpr schema)
+
+    let nameStrProves x = show (fixNameDisp dispProv (pp x))
+    if null proves
+        then rPutStrLn "There are no properties in scope."
+        else forM_ proves $ \(x,_,ops) ->
+               do let str = nameStrProves x
+                  rPutStr $ "property " ++ str ++ " options " ++ propOptsShow ops ++ " "
+                  proveCmd str _pos _fnm
+    let nameStrSats x = show (fixNameDisp dispSats (pp x))
+    if null sats
+        then rPutStrLn "There are no properties in scope."
+        else forM_ sats $ \(x,_,ops) ->
+               do let str = nameStrSats x
+                  rPutStr $ "property " ++ str ++ " options " ++ propOptsShow ops ++ " "
+                  satCmd str _pos _fnm
+  where
+    propOptsShow :: P.PropertyOptions -> String
+    propOptsShow opts = show [(optionName, P.thing ov) |(optionName, ov) <- Map.toList opts]
+
+
+
+
 data TestReport = TestReport
   { reportExpr :: Doc
   , reportResult :: TestResult
@@ -904,6 +949,7 @@
   (firstProver, res) <- getProverConfig >>= \case
        Left sbvCfg -> liftModuleCmd $ SBV.satProve sbvCfg cmd
        Right w4Cfg ->
+        -- TODO Look into factoring out all of these getUser out of REPL monad
          do ~(EnvBool hashConsing) <- getUser "hashConsing"
             ~(EnvBool warnUninterp) <- getUser "warnUninterp"
             liftModuleCmd $ W4.satProve w4Cfg hashConsing warnUninterp cmd

src/Cryptol/REPL/Help.hs

@@ -337,7 +337,7 @@ showValHelp ctxparams env nameEnv qname name =
          do rPutStrLn ""
 
             let property 
-                  | P.PragmaProperty `elem` ifDeclPragmas = [text "property"]
+                  | (P.Property P.DefaultPropertyPragma) `elem` ifDeclPragmas = [text "property"]
                   | otherwise                             = []
             rPrint $ runDoc nameEnv
                    $ indent 4

src/Cryptol/REPL/Monad.hs

@@ -47,6 +47,7 @@
   , getExprNames
   , getTypeNames
   , getPropertyNames
+  , getPropertiesOfType
   , getModNames
   , LoadedModule(..), getLoadedMod, setLoadedMod, clearLoadedMod
   , setEditPath, getEditPath, clearEditPath
@@ -123,7 +124,7 @@
 import Data.Char (isSpace, toLower)
 import Data.IORef
     (IORef,newIORef,readIORef,atomicModifyIORef)
-import Data.List (intercalate, isPrefixOf, unfoldr, sortBy)
+import Data.List (intercalate, isPrefixOf, unfoldr, sortBy, mapAccumL, find)
 import Data.Maybe (catMaybes)
 import Data.Ord (comparing)
 import Data.Tuple (swap)
@@ -140,6 +141,10 @@
 
 import Prelude ()
 import Prelude.Compat
+import Cryptol.Parser.AST (PropertyPragma(ConfigurableProperty))
+import qualified Cryptol.Parser.AST as P
+--import qualified Cryptol.Validation.Monad as V
+import qualified Data.Text as Text
 
 -- REPL Environment ------------------------------------------------------------
 
@@ -357,11 +362,11 @@
     ParseError e         -> ppError e
     FileNotFound path    -> sep [ text "File"
                                 , text ("`" ++ path ++ "'")
-                                , text"not found"
+                                , text "not found"
                                 ]
     DirectoryNotFound path -> sep [ text "Directory"
                                   , text ("`" ++ path ++ "'")
-                                  , text"not found or not a directory"
+                                  , text "not found or not a directory"
                                   ]
     NoPatError es        -> vcat (map pp es)
     NoIncludeError es    -> vcat (map ppIncludeError es)
@@ -645,10 +650,33 @@
      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 ]
-
+                    T.Property P.DefaultPropertyPragma `elem` M.ifDeclPragmas d ]
      return (ps, M.mctxNameDisp fe)
 
+-- | Return a list of property check names of type, sorted by position in the file.
+
+--TODO Refactor
+getPropertiesOfType :: P.PropertyType ->  REPL ([(M.Name,M.IfaceDecl, P.PropertyOptions)],NameDisp)
+getPropertiesOfType propType =
+  do fe <- getFocusedEnv
+     let xs = M.ifDecls (M.mctxDecls fe)
+         zipped =  [(x,d, getOptions l) 
+                      | ((x,d),l) <- zip (Map.toList xs) (getListOfOptions xs),
+                       any fst l
+                   ]
+
+     return (zipped, M.mctxNameDisp fe)
+  where getOptions xs = case find fst xs of
+                          Just (_,ops) -> ops
+                          Nothing -> mempty
+        getListOfOptions xs = (map (map (isOfType propType)) (map M.ifDeclPragmas (Map.elems xs)))
+
+isOfType :: P.PropertyType -> P.Pragma -> (Bool, Map.Map Text.Text (P.Located P.Literal))
+isOfType P.SatType (T.Property (P.ConfigurableProperty P.SatType options)) = (True, options)
+isOfType P.TestType (T.Property (P.ConfigurableProperty P.TestType options)) = (True, options)
+isOfType P.ProveType (T.Property (P.ConfigurableProperty P.ProveType options)) = (True, options)
+isOfType _ _ = (False, mempty)
+
 getModNames :: REPL [I.ModName]
 getModNames =
   do me <- getModuleEnv
@@ -717,21 +745,21 @@
 
 parseSearchPath :: String -> [String]
 parseSearchPath path = path'
-#if defined(mingw32_HOST_OS) || defined(__MINGW32__)
-      -- Windows paths search from end to beginning
-      where path' = reverse (splitSearchPath path)
-#else
+
+
+
+
       where path' = splitSearchPath path
-#endif
+
 
 renderSearchPath :: [String] -> String
 renderSearchPath pathSegs = path
-#if defined(mingw32_HOST_OS) || defined(__MINGW32__)
-      -- Windows paths search from end to beginning
-      where path = intercalate [searchPathSeparator] (reverse pathSegs)
-#else
+
+
+
+
       where path = intercalate [searchPathSeparator] pathSegs
-#endif
+
 
 -- User Environment Interaction ------------------------------------------------
 
@@ -1203,3 +1231,6 @@
   case mPath of
     Nothing -> return (Just Z3NotFound)
     Just _  -> return Nothing
+
+
+