Numeric literals sampling

.gitignore

@@ -10,6 +10,7 @@ dist-newstyle
 .ghc.environment.*
 cabal.project.freeze
 cabal.project.local*
+.vscode
 
 # don't check in generated documentation
 #docs/CryptolPrims.pdf

LiteralSampling.md

@@ -0,0 +1,10 @@
+# Literal Sampling
+
+
+
+## TODO
+
+- [x] remove use of vector-sized and related dependencies -- its not worth it now that I have a good idea of what I'm doing
+  - this will require explicit nVars included in some places probably
+- [x] make sure to use the `SamplingM` monad basically everywhere -- so that you can reasonably throw errors without causing a crash
+- [ ] where to call `sample` from, so I know what type exactly it should have?

cryptol.cabal

@@ -78,7 +78,9 @@ library
                        mtl               >= 2.2.1,
                        time              >= 1.6.0.1,
                        panic             >= 0.3,
-                       what4             >= 1.3 && < 1.4
+                       what4             >= 1.3 && < 1.4,
+                       constraints,
+                       vector
 
   if impl(ghc >= 9.0)
     build-depends:     ghc-bignum        >= 1.0 && < 1.3
@@ -176,6 +178,16 @@ library
                        Cryptol.Transform.Specialize,
                        Cryptol.Transform.AddModParams,
 
+                       Cryptol.TypeCheck.Solver.Numeric.Sampling
+                       Cryptol.TypeCheck.Solver.Numeric.Sampling.Base,
+                       Cryptol.TypeCheck.Solver.Numeric.Sampling.Constraints,
+                       Cryptol.TypeCheck.Solver.Numeric.Sampling.Exp,
+                       Cryptol.TypeCheck.Solver.Numeric.Sampling.Preconstraints,
+                       Cryptol.TypeCheck.Solver.Numeric.Sampling.Q,
+                       Cryptol.TypeCheck.Solver.Numeric.Sampling.Sampling,
+                       Cryptol.TypeCheck.Solver.Numeric.Sampling.SolvedConstraints,
+                       Cryptol.TypeCheck.Solver.Numeric.Sampling.System,
+
                        Cryptol.IR.FreeVars,
 
                        Cryptol.Backend,

src/Cryptol/Eval/Concrete.hs

@@ -520,3 +520,9 @@ updateBack_word (Nat n) _eltTy bs (Left idx) val = do
 updateBack_word (Nat n) _eltTy bs (Right w) val = do
   idx <- bvVal <$> asWordVal Concrete w
   updateWordValue Concrete bs (n - idx - 1) (fromVBit <$> val)
+
+-- FIX: remove this
+-- applySampleToValue :: Sample -> Value -> Value
+-- applySampleToValue sample = \case
+--   VNumPoly cs f -> _
+--   val -> val

src/Cryptol/ModuleSystem/Exports.hs

@@ -1,4 +1,5 @@
 {-# LANGUAGE DeriveGeneric #-}
+{-# LANGUAGE Safe #-}
 module Cryptol.ModuleSystem.Exports where
 
 import Data.Set(Set)

src/Cryptol/ModuleSystem/Interface.hs

@@ -11,6 +11,7 @@
 {-# LANGUAGE DeriveGeneric #-}
 {-# LANGUAGE PatternGuards #-}
 {-# LANGUAGE RecordWildCards #-}
+{-# LANGUAGE Safe #-}
 module Cryptol.ModuleSystem.Interface (
     Iface
   , IfaceG(..)

src/Cryptol/Parser/AST.hs

@@ -7,7 +7,6 @@
 -- Portability :  portable
 
 {-# LANGUAGE Safe #-}
-
 {-# LANGUAGE DeriveAnyClass #-}
 {-# LANGUAGE DeriveFoldable #-}
 {-# LANGUAGE DeriveTraversable #-}

src/Cryptol/Parser/Name.hs

@@ -7,6 +7,7 @@
 -- Portability :  portable
 
 {-# LANGUAGE DeriveGeneric #-}
+{-# LANGUAGE Safe #-}
 
 module Cryptol.Parser.Name where
 

src/Cryptol/Parser/Names.hs

@@ -9,6 +9,8 @@
 -- This module defines the scoping rules for value- and type-level
 -- names in Cryptol.
 
+{-# LANGUAGE Safe #-}
+
 module Cryptol.Parser.Names
   ( tnamesNT
   , tnamesT

src/Cryptol/Parser/ParserUtils.hs

@@ -7,7 +7,6 @@
 -- Portability :  portable
 
 {-# LANGUAGE Safe #-}
-
 {-# LANGUAGE CPP #-}
 {-# LANGUAGE DeriveAnyClass #-}
 {-# LANGUAGE DeriveGeneric #-}

src/Cryptol/Parser/Position.hs

@@ -7,7 +7,6 @@
 -- Portability :  portable
 
 {-# LANGUAGE Safe #-}
-
 {-# LANGUAGE DeriveAnyClass #-}
 {-# LANGUAGE DeriveGeneric #-}
 {-# LANGUAGE DeriveFunctor #-}

src/Cryptol/Parser/Selector.hs

@@ -6,7 +6,7 @@
 -- Stability   :  provisional
 -- Portability :  portable
 
-{-# LANGUAGE Safe #-}
+{-# LANGUAGE Trustworthy #-}
 
 {-# LANGUAGE DeriveAnyClass #-}
 {-# LANGUAGE DeriveGeneric #-}

src/Cryptol/Parser/Token.hs

@@ -1,5 +1,6 @@
 {-# LANGUAGE DeriveAnyClass #-}
 {-# LANGUAGE DeriveGeneric #-}
+{-# LANGUAGE Safe #-}
 module Cryptol.Parser.Token where
 
 import Data.Text(Text)

src/Cryptol/Parser/Utils.hs

@@ -10,6 +10,7 @@
 -- from previous Cryptol versions.
 
 {-# LANGUAGE OverloadedStrings #-}
+{-# LANGUAGE Safe #-}
 
 module Cryptol.Parser.Utils
   ( translateExprToNumT

src/Cryptol/REPL/Command.hs

@@ -10,12 +10,17 @@
 {-# LANGUAGE BlockArguments #-}
 {-# LANGUAGE FlexibleContexts #-}
 {-# LANGUAGE LambdaCase #-}
+{-# LANGUAGE ViewPatterns #-}
 {-# LANGUAGE MultiWayIf #-}
 {-# LANGUAGE OverloadedStrings #-}
 {-# LANGUAGE PatternGuards #-}
 {-# LANGUAGE RecordWildCards #-}
 -- See Note [-Wincomplete-uni-patterns and irrefutable patterns] in Cryptol.TypeCheck.TypePat
 {-# OPTIONS_GHC -Wno-incomplete-uni-patterns #-}
+{-# OPTIONS_GHC -Wno-unrecognised-pragmas #-}
+{-# HLINT ignore "Use camelCase" #-}
+{-# LANGUAGE NamedFieldPuns #-}
+{-# OPTIONS_GHC -Wno-name-shadowing #-}
 module Cryptol.REPL.Command (
     -- * Commands
     Command(..), CommandDescr(..), CommandBody(..), CommandExitCode(..)
@@ -86,7 +91,7 @@ import qualified Cryptol.TypeCheck.AST as T
 import qualified Cryptol.TypeCheck.Error as T
 import qualified Cryptol.TypeCheck.Parseable as T
 import qualified Cryptol.TypeCheck.Subst as T
-import           Cryptol.TypeCheck.Solve(defaultReplExpr)
+import           Cryptol.TypeCheck.Solve(defaultReplExpr,sampleLiterals)
 import           Cryptol.TypeCheck.PP (dump,ppWithNames,emptyNameMap)
 import           Cryptol.Utils.PP hiding ((</>))
 import           Cryptol.Utils.Panic(panic)
@@ -112,7 +117,7 @@ import Data.Bits (shiftL, (.&.), (.|.))
 import Data.Char (isSpace,isPunctuation,isSymbol,isAlphaNum,isAscii)
 import Data.Function (on)
 import Data.List (intercalate, nub, isPrefixOf,intersperse)
-import Data.Maybe (fromMaybe,mapMaybe,isNothing)
+import Data.Maybe (fromMaybe,mapMaybe,isNothing, isJust, fromJust)
 import System.Environment (lookupEnv)
 import System.Exit (ExitCode(ExitSuccess))
 import System.Process (shell,createProcess,waitForProcess)
@@ -137,6 +142,9 @@ import Prelude ()
 import Prelude.Compat
 
 import qualified Data.SBV.Internals as SBV (showTDiff)
+import Cryptol.TypeCheck.Solver.Numeric.Sampling (Sample)
+import qualified Data.List as List
+import Cryptol.TypeCheck.Solver.InfNat (Nat' (..))
 
 -- Commands --------------------------------------------------------------------
 
@@ -391,32 +399,107 @@ dumpTestsCmd outFile str pos fnm =
 
 data QCMode = QCRandom | QCExhaust deriving (Eq, Show)
 
+data SampleBinInfo = SampleBinInfo
+  { sample :: Sample -- the sample used for this bin
+  , binIndex :: Integer -- the index of this bin among all bins
+  , bins :: Integer -- the number of total bins
+  , binSize :: Integer -- the number of tests for this bin
+  }
+
 
 -- | Randomly test a property, or exhaustively check it if the number
 -- of values in the type under test is smaller than the @tests@
 -- environment variable, or we specify exhaustive testing.
 qcCmd :: QCMode -> String -> (Int,Int) -> Maybe FilePath -> REPL ()
-qcCmd qcMode "" _pos _fnm =
-  do (xs,disp) <- getPropertyNames
-     let nameStr x = show (fixNameDisp disp (pp x))
-     if null xs
-        then rPutStrLn "There are no properties in scope."
-        else forM_ xs $ \(x,d) ->
-               do let str = nameStr x
-                  rPutStr $ "property " ++ str ++ " "
-                  let texpr = T.EVar x
-                  let schema = M.ifDeclSig d
-                  nd <- M.mctxNameDisp <$> getFocusedEnv
-                  let doc = fixNameDisp nd (pp texpr)
-                  void (qcExpr qcMode doc texpr schema)
-
-qcCmd qcMode str pos fnm =
-  do expr <- replParseExpr str pos fnm
-     (_,texpr,schema) <- replCheckExpr expr
-     nd <- M.mctxNameDisp <$> getFocusedEnv
-     let doc = fixNameDisp nd (ppPrec 3 expr) -- function application has precedence 3
-     void (qcExpr qcMode doc texpr schema)
-
+qcCmd qcMode str pos fnm = do
+  -- (qcMde, doc, texpr, schema) <- case str of 
+  case str of
+    "" -> do
+      (xs,disp) <- getPropertyNames
+      let nameStr x = show (fixNameDisp disp (pp x))
+      if null xs
+      then do
+        rPutStrLn "There are no properties in scope."
+      else
+        forM_ xs $ \(x,d) -> do
+          let str = nameStr x
+          rPutStr $ "property " ++ str ++ " "
+          let texpr = T.EVar x
+          let schema = M.ifDeclSig d
+          nd <- M.mctxNameDisp <$> getFocusedEnv
+          let doc = fixNameDisp nd (pp texpr)
+          go doc Nothing texpr schema
+    _ -> do
+      expr <- replParseExpr str pos fnm
+      (_,texpr,schema) <- replCheckExpr expr
+      nd <- M.mctxNameDisp <$> getFocusedEnv
+      let doc = fixNameDisp nd (ppPrec 3 expr) -- function application has precedence 3
+      go doc (Just expr) texpr schema
+  where
+    go :: Doc -> Maybe (P.Expr P.PName) -> T.Expr -> T.Schema -> REPL ()
+    go doc mb_expr texpr schema = case qcMode of
+      QCExhaust -> do
+        testNum <- (toInteger :: Int -> Integer) <$> getKnownUser "tests"
+        (val, ty) <- replEvalCheckedExpr' texpr schema
+        void (qcExpr qcMode doc texpr schema testNum val ty Nothing)
+      QCRandom -> do
+        testNum <- (toInteger :: Int -> Integer) <$> getKnownUser "tests"
+        useLitSampling <- getKnownUser "literalSampling" :: REPL Bool
+        if  useLitSampling &&
+            not (null (T.sVars schema)) &&
+            all ((T.KNum ==) . T.tpKind) (T.sVars schema)
+          then do
+          case mb_expr of
+            Nothing -> do
+              (val, ty) <- replEvalCheckedExpr' texpr schema
+              void (qcExpr qcMode doc texpr schema testNum val ty Nothing)
+            Just expr -> do
+              -- do this many tests per sample, until out of tests
+              binSize <- (toInteger :: Int -> Integer) <$> getKnownUser "literalSamplingBinSize"
+              let bins = testNum `div` binSize
+              io (sampleLiterals schema (fromInteger bins)) >>= \case
+                Right samples_schemas -> do
+                  rPutStrLn "Using literal sampling."
+                  let -- this generates a new expression that has the appropriate
+                      -- type arguments given to it according to the sampling,
+                      -- which is then typechecked and evaluated again
+                      applySampleToTExpr :: Sample -> P.Expr P.PName -> P.Expr P.PName
+                      applySampleToTExpr sample e = P.EAppT e $ f <$> sample
+                        where
+                          f :: (T.TParam, Nat') -> P.TypeInst P.PName
+                          f (tparam, v) = P.NamedInst $ P.Named
+                            { name = fromTParamToNamedIdent tparam
+                            -- , value = P.TNum v }
+                            , value = case v of
+                                Nat n -> P.TNum n
+                                Inf -> P.TUser (P.UnQual (M.mkIdent (T.pack "inf"))) []}
+
+                          fromTParamToNamedIdent :: T.TParam -> P.Located P.Ident
+                          fromTParamToNamedIdent tparam = case T.tvarDesc . T.tpInfo $ tparam of
+                            T.TVFromSignature name -> P.Located {
+                              thing = M.nameIdent name,
+                              srcRange = M.nameLoc name
+                            }
+                            varDesc -> panic "qcCmd" ["cannot substitute type var with TypeSource: " ++ show varDesc]
+
+                      qcSampleSchema ((sample, _schema), binIndex) = do
+                        expr <- pure $ applySampleToTExpr sample expr
+                        (_, texpr, schema') <- replCheckExpr expr
+                        (val, ty) <- replEvalCheckedExpr' texpr schema'
+                        qcExpr qcMode doc texpr schema' binSize val ty
+                          (Just SampleBinInfo
+                            { sample, bins, binIndex, binSize })
+
+                  qcSampleSchema `mapM_` (take (fromInteger $ testNum `div` binSize) samples_schemas `zip` [0..])
+
+                Left err -> do
+                  rPutStrLn $ "Failed to use liteal sampling: " ++ err
+                  rPutStrLn "Using default literal solution instead."
+                  (val, ty) <- replEvalCheckedExpr' texpr schema
+                  void (qcExpr qcMode doc texpr schema testNum val ty Nothing)
+        else do
+          (val, ty) <- replEvalCheckedExpr' texpr schema
+          void (qcExpr qcMode doc texpr schema testNum val ty Nothing)
 
 data TestReport = TestReport
   { reportExpr :: Doc
@@ -425,27 +508,50 @@ data TestReport = TestReport
   , reportTestsPossible :: Maybe Integer
   }
 
+replEvalCheckedExpr' :: T.Expr -> T.Schema -> REPL (Concrete.Value, T.Type)
+replEvalCheckedExpr' texpr schema =
+  replEvalCheckedExpr texpr schema >>= \case
+    Just res -> pure res
+    -- If instance is not found, doesn't necessarily mean that there is no
+    -- instance. And due to nondeterminism in result from the solver (for
+    -- finding solution to numeric type constraints), `:check` can get to
+    -- this exception sometimes, but successfully find an instance and test
+    -- with it other times.
+    Nothing -> raise (InstantiationsNotFound schema)
+
 qcExpr ::
   QCMode ->
   Doc ->
   T.Expr ->
   T.Schema ->
+  Integer ->
+  Concrete.Value ->
+  T.Type ->
+  Maybe SampleBinInfo -> -- if using literal sampling
   REPL TestReport
-qcExpr qcMode exprDoc texpr schema =
-  do (val,ty) <- replEvalCheckedExpr texpr schema >>= \mb_res -> case mb_res of
-       Just res -> pure res
-       -- If instance is not found, doesn't necessarily mean that there is no instance.
-       -- And due to nondeterminism in result from the solver (for finding solution to 
-       -- numeric type constraints), `:check` can get to this exception sometimes, but
-       -- successfully find an instance and test with it other times.
-       Nothing -> raise (InstantiationsNotFound schema)
-     testNum <- (toInteger :: Int -> Integer) <$> getKnownUser "tests"
-     tenv <- E.envTypes . M.deEnv <$> getDynEnv
+qcExpr qcMode exprDoc _texpr _schema testNum val ty mb_sampleInfo =
+  do tenv <- E.envTypes . M.deEnv <$> getDynEnv
      let tyv = E.evalValType tenv ty
+
+     case mb_sampleInfo of
+      Just SampleBinInfo{..} -> do
+        rPutStrLn ""
+        rPutStrLn $ unwords
+          [ "Bin:", show (binIndex + 1), "/", show bins ]
+        rPutStrLn . unwords $
+          [ "Sample:"
+          , List.intercalate ", "
+              [ pretty (fromJust $ T.tpName tp) ++ " = " ++ show i
+              | (tp, i) <- sample
+              , isJust (T.tpName tp) ] ]
+
+      Nothing -> pure ()
+
      -- tv has already had polymorphism instantiated 
      percentRef <- io $ newIORef Nothing
      testsRef <- io $ newIORef 0
 
+
      case testableType tyv of
        Just (Just sz,tys,vss,_gens) | qcMode == QCExhaust || sz <= testNum -> do
             rPutStrLn "Using exhaustive testing."
@@ -494,7 +600,7 @@ qcExpr qcMode exprDoc texpr schema =
   testingMsg = "Testing... "
 
   interruptedExhaust testNum sz =
-     let percent = (100.0 :: Double) * (fromInteger testNum) / fromInteger sz
+     let percent = (100.0 :: Double) * fromInteger testNum / fromInteger sz
          showValNum
             | sz > 2 ^ (20::Integer) =
               "2^^" ++ show (lg2 sz)
@@ -809,7 +915,7 @@ proveSatExpr isSat rng exprDoc texpr schema = do
 printSafetyViolation :: T.Expr -> T.Schema -> [E.GenValue Concrete] -> REPL ()
 printSafetyViolation texpr schema vs =
     catch
-      (do fn <- replEvalCheckedExpr texpr schema >>= \mb_res -> case mb_res of 
+      (do fn <- replEvalCheckedExpr texpr schema >>= \mb_res -> case mb_res of
             Just (fn, _) -> pure fn
             Nothing -> raise (EvalPolyError schema)
           rEval (E.forceValue =<< foldM (\f v -> E.fromVFun Concrete f (pure v)) fn vs))
@@ -1791,3 +1897,4 @@ parseCommand findCmd line = do
         '"':rest  -> Just $ quoted '"' rest
         _         -> let (a,b) = break isSpace ipt in
                      if null a then Nothing else Just (length a, a, b)
+