-- |
-- Module      :  Cryptol.REPL.Command
-- Copyright   :  (c) 2013-2016 Galois, Inc.
-- License     :  BSD3
-- Maintainer  :  cryptol@galois.com
-- Stability   :  provisional
-- Portability :  portable

{-# LANGUAGE BangPatterns #-}
{-# LANGUAGE BlockArguments #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE LambdaCase #-}
{-# 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 #-}
module Cryptol.REPL.Command (
    -- * Commands
    Command(..), CommandDescr(..), CommandBody(..), CommandExitCode(..)
  , parseCommand
  , runCommand
  , splitCommand
  , findCommand
  , findCommandExact
  , findNbCommand
  , commandList

  , moduleCmd, loadCmd, loadPrelude, setOptionCmd

    -- Parsing
  , interactiveConfig
  , replParseExpr

    -- Evaluation and Typechecking
  , replEvalExpr
  , replCheckExpr

    -- Check, SAT, and prove
  , TestReport(..)
  , qcExpr, qcCmd, QCMode(..)
  , satCmd
  , proveCmd
  , onlineProveSat
  , offlineProveSat

    -- Misc utilities
  , handleCtrlC
  , sanitize
  , withRWTempFile

    -- To support Notebook interface (might need to refactor)
  , replParse
  , liftModuleCmd
  , moduleCmdResult
  ) where

import Cryptol.REPL.Monad
import Cryptol.REPL.Trie
import Cryptol.REPL.Browse
import Cryptol.REPL.Help

import qualified Cryptol.ModuleSystem as M
import qualified Cryptol.ModuleSystem.Name as M
import qualified Cryptol.ModuleSystem.NamingEnv as M
import qualified Cryptol.ModuleSystem.Renamer as M
    (RenamerWarning(SymbolShadowed, PrefixAssocChanged))
import qualified Cryptol.Utils.Ident as M
import qualified Cryptol.ModuleSystem.Env as M
import Cryptol.ModuleSystem.Fingerprint(fingerprintHexString)

import           Cryptol.Backend.FloatHelpers as FP
import qualified Cryptol.Backend.Monad as E
import qualified Cryptol.Backend.SeqMap as E
import           Cryptol.Eval.Concrete( Concrete(..) )
import qualified Cryptol.Eval.Concrete as Concrete
import qualified Cryptol.Eval.Env as E
import           Cryptol.Eval.FFI
import           Cryptol.Eval.FFI.GenHeader
import qualified Cryptol.Eval.Type as E
import qualified Cryptol.Eval.Value as E
import qualified Cryptol.Eval.Reference as R
import Cryptol.Testing.Random
import qualified Cryptol.Testing.Random  as TestR
import Cryptol.Parser
    (parseExprWith,parseReplWith,ParseError(),Config(..),defaultConfig
    ,parseModName,parseHelpName)
import           Cryptol.Parser.Position (Position(..),Range(..),HasLoc(..))
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.PP (dump)
import qualified Cryptol.Utils.Benchmark as Bench
import           Cryptol.Utils.PP hiding ((</>))
import           Cryptol.Utils.Panic(panic)
import           Cryptol.Utils.RecordMap
import qualified Cryptol.Parser.AST as P
import qualified Cryptol.Transform.Specialize as S
import Cryptol.Symbolic
  ( ProverCommand(..), QueryType(..)
  , ProverStats,ProverResult(..),CounterExampleType(..)
  )
import qualified Cryptol.Symbolic.SBV as SBV
import qualified Cryptol.Symbolic.What4 as W4
import Cryptol.Version (displayVersion)

import qualified Control.Exception as X
import Control.Monad hiding (mapM, mapM)
import qualified Control.Monad.Catch as Ex
import Control.Monad.IO.Class(liftIO)
import Text.Read (readMaybe)
import Control.Applicative ((<|>))
import qualified Data.Set as Set
import Data.ByteString (ByteString)
import qualified Data.ByteString as BS
import qualified Data.ByteString.Char8 as BS8
import Data.Bits (shiftL, (.&.), (.|.))
import Data.Char (isSpace,isPunctuation,isSymbol,isAlphaNum,isAscii)
import Data.Function (on)
import Data.List (intercalate, nub, isPrefixOf)
import qualified Data.Map as Map
import Data.Maybe (fromMaybe,mapMaybe,isNothing)
import System.Environment (lookupEnv)
import System.Exit (ExitCode(ExitSuccess))
import System.Process (shell,createProcess,waitForProcess)
import qualified System.Process as Process(runCommand)
import System.FilePath((</>), (-<.>), isPathSeparator)
import System.Directory(getHomeDirectory,setCurrentDirectory,doesDirectoryExist
                       ,getTemporaryDirectory,setPermissions,removeFile
                       ,emptyPermissions,setOwnerReadable)
import System.IO
         (Handle,hFlush,stdout,openTempFile,hClose,openFile
         ,IOMode(..),hGetContents,hSeek,SeekMode(..))
import qualified System.Random.TF as TF
import qualified System.Random.TF.Instances as TFI
import Numeric (showFFloat)
import qualified Data.Text as T
import Data.IORef(newIORef,readIORef,writeIORef)

import GHC.Float (log1p, expm1)

import Prelude ()
import Prelude.Compat

import qualified Data.SBV.Internals as SBV (showTDiff)



-- Commands --------------------------------------------------------------------

-- | Commands.
data Command
  = Command (Int -> Maybe FilePath -> REPL ())         -- ^ Successfully parsed command
  | Ambiguous String [String] -- ^ Ambiguous command, list of conflicting
                              --   commands
  | Unknown String            -- ^ The unknown command

-- | Command builder.
data CommandDescr = CommandDescr
  { CommandDescr -> [String]
cNames    :: [String]
  , CommandDescr -> [String]
cArgs     :: [String]
  , CommandDescr -> CommandBody
cBody     :: CommandBody
  , CommandDescr -> String
cHelp     :: String
  , CommandDescr -> String
cLongHelp :: String
  }

instance Show CommandDescr where
  show :: CommandDescr -> String
show = [String] -> String
forall a. Show a => a -> String
show ([String] -> String)
-> (CommandDescr -> [String]) -> CommandDescr -> String
forall b c a. (b -> c) -> (a -> b) -> a -> c
. CommandDescr -> [String]
cNames

instance Eq CommandDescr where
  == :: CommandDescr -> CommandDescr -> Bool
(==) = [String] -> [String] -> Bool
forall a. Eq a => a -> a -> Bool
(==) ([String] -> [String] -> Bool)
-> (CommandDescr -> [String])
-> CommandDescr
-> CommandDescr
-> Bool
forall b c a. (b -> b -> c) -> (a -> b) -> a -> a -> c
`on` CommandDescr -> [String]
cNames

instance Ord CommandDescr where
  compare :: CommandDescr -> CommandDescr -> Ordering
compare = [String] -> [String] -> Ordering
forall a. Ord a => a -> a -> Ordering
compare ([String] -> [String] -> Ordering)
-> (CommandDescr -> [String])
-> CommandDescr
-> CommandDescr
-> Ordering
forall b c a. (b -> b -> c) -> (a -> b) -> a -> a -> c
`on` CommandDescr -> [String]
cNames

data CommandBody
  = ExprArg     (String   -> (Int,Int) -> Maybe FilePath -> REPL ())
  | FileExprArg (FilePath -> String -> (Int,Int) -> Maybe FilePath -> REPL ())
  | DeclsArg    (String   -> REPL ())
  | ExprTypeArg (String   -> REPL ())
  | ModNameArg  (String   -> REPL ())
  | FilenameArg (FilePath -> REPL ())
  | OptionArg   (String   -> REPL ())
  | ShellArg    (String   -> REPL ())
  | HelpArg     (String   -> REPL ())
  | NoArg       (REPL ())


data CommandExitCode = CommandOk
                     | CommandError -- XXX: More?


-- | REPL command parsing.
commands :: CommandMap
commands :: CommandMap
commands  = (CommandMap -> CommandDescr -> CommandMap)
-> CommandMap -> [CommandDescr] -> CommandMap
forall b a. (b -> a -> b) -> b -> [a] -> b
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl CommandMap -> CommandDescr -> CommandMap
insert CommandMap
forall a. Trie a
emptyTrie [CommandDescr]
commandList
  where
  insert :: CommandMap -> CommandDescr -> CommandMap
insert CommandMap
m CommandDescr
d = (CommandMap -> String -> CommandMap)
-> CommandMap -> [String] -> CommandMap
forall b a. (b -> a -> b) -> b -> [a] -> b
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl (CommandDescr -> CommandMap -> String -> CommandMap
forall {a}. a -> Trie a -> String -> Trie a
insertOne CommandDescr
d) CommandMap
m (CommandDescr -> [String]
cNames CommandDescr
d)
  insertOne :: a -> Trie a -> String -> Trie a
insertOne a
d Trie a
m String
name = String -> a -> Trie a -> Trie a
forall a. String -> a -> Trie a -> Trie a
insertTrie String
name a
d Trie a
m

-- | Notebook command parsing.
nbCommands :: CommandMap
nbCommands :: CommandMap
nbCommands  = (CommandMap -> CommandDescr -> CommandMap)
-> CommandMap -> [CommandDescr] -> CommandMap
forall b a. (b -> a -> b) -> b -> [a] -> b
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl CommandMap -> CommandDescr -> CommandMap
insert CommandMap
forall a. Trie a
emptyTrie [CommandDescr]
nbCommandList
  where
  insert :: CommandMap -> CommandDescr -> CommandMap
insert CommandMap
m CommandDescr
d = (CommandMap -> String -> CommandMap)
-> CommandMap -> [String] -> CommandMap
forall b a. (b -> a -> b) -> b -> [a] -> b
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl (CommandDescr -> CommandMap -> String -> CommandMap
forall {a}. a -> Trie a -> String -> Trie a
insertOne CommandDescr
d) CommandMap
m (CommandDescr -> [String]
cNames CommandDescr
d)
  insertOne :: a -> Trie a -> String -> Trie a
insertOne a
d Trie a
m String
name = String -> a -> Trie a -> Trie a
forall a. String -> a -> Trie a -> Trie a
insertTrie String
name a
d Trie a
m

-- | A subset of commands safe for Notebook execution
nbCommandList :: [CommandDescr]
nbCommandList :: [CommandDescr]
nbCommandList  =
  [ [String]
-> [String] -> CommandBody -> String -> String -> CommandDescr
CommandDescr [ String
":t", String
":type" ] [String
"EXPR"] ((String -> (Int, Int) -> Maybe String -> REPL ()) -> CommandBody
ExprArg String -> (Int, Int) -> Maybe String -> REPL ()
typeOfCmd)
    String
"Check the type of an expression."
    String
""
  , [String]
-> [String] -> CommandBody -> String -> String -> CommandDescr
CommandDescr [ String
":b", String
":browse" ] [String
"[ MODULE ]"] ((String -> REPL ()) -> CommandBody
ModNameArg String -> REPL ()
browseCmd)
    String
"Display information about loaded modules."
    ([String] -> String
unlines
       [ String
"With no arguent, :browse shows information about the names in scope."
       , String
"With an argument M, shows information about the names exported from M"
       ]
    )
  , [String]
-> [String] -> CommandBody -> String -> String -> CommandDescr
CommandDescr [ String
":version"] [] (REPL () -> CommandBody
NoArg REPL ()
versionCmd)
    String
"Display the version of this Cryptol executable"
    String
""
  , [String]
-> [String] -> CommandBody -> String -> String -> CommandDescr
CommandDescr [ String
":?", String
":help" ] [String
"[ TOPIC ]"] ((String -> REPL ()) -> CommandBody
HelpArg String -> REPL ()
helpCmd)
    String
"Display a brief description of a function, type, or command. (e.g. :help :help)"
    ([String] -> String
unlines
      [ String
"TOPIC can be any of:"
      , String
" * Specific REPL colon-commands (e.g. :help :prove)"
      , String
" * Functions (e.g. :help join)"
      , String
" * Infix operators (e.g. :help +)"
      , String
" * Type constructors (e.g. :help Z)"
      , String
" * Type constraints (e.g. :help fin)"
      , String
" * :set-able options (e.g. :help :set base)" ])
  , [String]
-> [String] -> CommandBody -> String -> String -> CommandDescr
CommandDescr [ String
":s", String
":set" ] [String
"[ OPTION [ = VALUE ] ]"] ((String -> REPL ()) -> CommandBody
OptionArg String -> REPL ()
setOptionCmd)
    String
"Set an environmental option (:set on its own displays current values)."
    String
""
  , [String]
-> [String] -> CommandBody -> String -> String -> CommandDescr
CommandDescr [ String
":check" ] [String
"[ EXPR ]"] ((String -> (Int, Int) -> Maybe String -> REPL ()) -> CommandBody
ExprArg (QCMode -> String -> (Int, Int) -> Maybe String -> REPL ()
qcCmd QCMode
QCRandom))
    String
"Use random testing to check that the argument always returns true.\n(If no argument, check all properties.)"
    String
""
  , [String]
-> [String] -> CommandBody -> String -> String -> CommandDescr
CommandDescr [ String
":exhaust" ] [String
"[ EXPR ]"] ((String -> (Int, Int) -> Maybe String -> REPL ()) -> CommandBody
ExprArg (QCMode -> String -> (Int, Int) -> Maybe String -> REPL ()
qcCmd QCMode
QCExhaust))
    String
"Use exhaustive testing to prove that the argument always returns\ntrue. (If no argument, check all properties.)"
    String
""
  , [String]
-> [String] -> CommandBody -> String -> String -> CommandDescr
CommandDescr [ String
":prove" ] [String
"[ EXPR ]"] ((String -> (Int, Int) -> Maybe String -> REPL ()) -> CommandBody
ExprArg String -> (Int, Int) -> Maybe String -> REPL ()
proveCmd)
    String
"Use an external solver to prove that the argument always returns\ntrue. (If no argument, check all properties.)"
    String
""
  , [String]
-> [String] -> CommandBody -> String -> String -> CommandDescr
CommandDescr [ String
":sat" ] [String
"[ EXPR ]"] ((String -> (Int, Int) -> Maybe String -> REPL ()) -> CommandBody
ExprArg String -> (Int, Int) -> Maybe String -> REPL ()
satCmd)
    String
"Use a solver to find a satisfying assignment for which the argument\nreturns true. (If no argument, find an assignment for all properties.)"
    String
""
  , [String]
-> [String] -> CommandBody -> String -> String -> CommandDescr
CommandDescr [ String
":safe" ] [String
"[ EXPR ]"] ((String -> (Int, Int) -> Maybe String -> REPL ()) -> CommandBody
ExprArg String -> (Int, Int) -> Maybe String -> REPL ()
safeCmd)
    String
"Use an external solver to prove that an expression is safe\n(does not encounter run-time errors) for all inputs."
    String
""
  , [String]
-> [String] -> CommandBody -> String -> String -> CommandDescr
CommandDescr [ String
":debug_specialize" ] [String
"EXPR"]((String -> (Int, Int) -> Maybe String -> REPL ()) -> CommandBody
ExprArg String -> (Int, Int) -> Maybe String -> REPL ()
specializeCmd)
    String
"Do type specialization on a closed expression."
    String
""
  , [String]
-> [String] -> CommandBody -> String -> String -> CommandDescr
CommandDescr [ String
":eval" ] [String
"EXPR"] ((String -> (Int, Int) -> Maybe String -> REPL ()) -> CommandBody
ExprArg String -> (Int, Int) -> Maybe String -> REPL ()
refEvalCmd)
    String
"Evaluate an expression with the reference evaluator."
    String
""
  , [String]
-> [String] -> CommandBody -> String -> String -> CommandDescr
CommandDescr [ String
":ast" ] [String
"EXPR"] ((String -> (Int, Int) -> Maybe String -> REPL ()) -> CommandBody
ExprArg String -> (Int, Int) -> Maybe String -> REPL ()
astOfCmd)
    String
"Print out the pre-typechecked AST of a given term."
    String
""
  , [String]
-> [String] -> CommandBody -> String -> String -> CommandDescr
CommandDescr [ String
":extract-coq" ] [] (REPL () -> CommandBody
NoArg REPL ()
allTerms)
    String
"Print out the post-typechecked AST of all currently defined terms,\nin a Coq-parseable format."
    String
""
  , [String]
-> [String] -> CommandBody -> String -> String -> CommandDescr
CommandDescr [ String
":time" ] [String
"EXPR"] ((String -> (Int, Int) -> Maybe String -> REPL ()) -> CommandBody
ExprArg String -> (Int, Int) -> Maybe String -> REPL ()
timeCmd)
    String
"Measure the time it takes to evaluate the given expression."
    ([String] -> String
unlines
      [ String
"The expression will be evaluated many times to get accurate results."
      , String
"Note that the first evaluation of a binding may take longer due to"
      , String
"  laziness, and this may affect the reported time. If this is not"
      , String
"  desired then make sure to evaluate the expression once first before"
      , String
"  running :time."
      , String
"The amount of time to spend collecting measurements can be changed"
      , String
"  with the timeMeasurementPeriod option."
      , String
"Reports the average wall clock time, CPU time, and cycles."
      , String
"  (Cycles are in unspecified units that may be CPU cycles.)"
      , String
"Binds the result to"
      , String
"  it : { avgTime : Float64"
      , String
"       , avgCpuTime : Float64"
      , String
"       , avgCycles : Integer }" ])

  , [String]
-> [String] -> CommandBody -> String -> String -> CommandDescr
CommandDescr [ String
":set-seed" ] [String
"SEED"] ((String -> REPL ()) -> CommandBody
OptionArg String -> REPL ()
seedCmd)
      String
"Seed the random number generator for operations using randomness"
      ([String] -> String
unlines
        [ String
"A seed takes the form of either a single integer or a 4-tuple"
        , String
"of unsigned 64-bit integers.  Examples of commands using randomness"
        , String
"are dumpTests and check."
        ])
  , [String]
-> [String] -> CommandBody -> String -> String -> CommandDescr
CommandDescr [ String
":new-seed"] [] (REPL () -> CommandBody
NoArg REPL ()
newSeedCmd)
      String
"Randomly generate and set a new seed for the random number generator"
      String
""
  ]

commandList :: [CommandDescr]
commandList :: [CommandDescr]
commandList  =
  [CommandDescr]
nbCommandList [CommandDescr] -> [CommandDescr] -> [CommandDescr]
forall a. [a] -> [a] -> [a]
++
  [ [String]
-> [String] -> CommandBody -> String -> String -> CommandDescr
CommandDescr [ String
":q", String
":quit" ] [] (REPL () -> CommandBody
NoArg REPL ()
quitCmd)
    String
"Exit the REPL."
    String
""
  , [String]
-> [String] -> CommandBody -> String -> String -> CommandDescr
CommandDescr [ String
":l", String
":load" ] [String
"FILE"] ((String -> REPL ()) -> CommandBody
FilenameArg String -> REPL ()
loadCmd)
    String
"Load a module by filename."
    String
""
  , [String]
-> [String] -> CommandBody -> String -> String -> CommandDescr
CommandDescr [ String
":r", String
":reload" ] [] (REPL () -> CommandBody
NoArg REPL ()
reloadCmd)
    String
"Reload the currently loaded module."
    String
""
  , [String]
-> [String] -> CommandBody -> String -> String -> CommandDescr
CommandDescr [ String
":e", String
":edit" ] [String
"[ FILE ]"] ((String -> REPL ()) -> CommandBody
FilenameArg String -> REPL ()
editCmd)
    String
"Edit FILE or the currently loaded module."
    String
""
  , [String]
-> [String] -> CommandBody -> String -> String -> CommandDescr
CommandDescr [ String
":!" ] [String
"COMMAND"] ((String -> REPL ()) -> CommandBody
ShellArg String -> REPL ()
runShellCmd)
    String
"Execute a command in the shell."
    String
""
  , [String]
-> [String] -> CommandBody -> String -> String -> CommandDescr
CommandDescr [ String
":cd" ] [String
"DIR"] ((String -> REPL ()) -> CommandBody
FilenameArg String -> REPL ()
cdCmd)
    String
"Set the current working directory."
    String
""
  , [String]
-> [String] -> CommandBody -> String -> String -> CommandDescr
CommandDescr [ String
":m", String
":module" ] [String
"[ MODULE ]"] ((String -> REPL ()) -> CommandBody
FilenameArg String -> REPL ()
moduleCmd)
    String
"Load a module by its name."
    String
""
  , [String]
-> [String] -> CommandBody -> String -> String -> CommandDescr
CommandDescr [ String
":w", String
":writeByteArray" ] [String
"FILE", String
"EXPR"] ((String -> String -> (Int, Int) -> Maybe String -> REPL ())
-> CommandBody
FileExprArg String -> String -> (Int, Int) -> Maybe String -> REPL ()
writeFileCmd)
    String
"Write data of type 'fin n => [n][8]' to a file."
    String
""
  , [String]
-> [String] -> CommandBody -> String -> String -> CommandDescr
CommandDescr [ String
":readByteArray" ] [String
"FILE"] ((String -> REPL ()) -> CommandBody
FilenameArg String -> REPL ()
readFileCmd)
    String
"Read data from a file as type 'fin n => [n][8]', binding\nthe value to variable 'it'."
    String
""
  , [String]
-> [String] -> CommandBody -> String -> String -> CommandDescr
CommandDescr [ String
":dumptests" ] [String
"FILE", String
"EXPR"] ((String -> String -> (Int, Int) -> Maybe String -> REPL ())
-> CommandBody
FileExprArg String -> String -> (Int, Int) -> Maybe String -> REPL ()
dumpTestsCmd)
    ([String] -> String
unlines [ String
"Dump a tab-separated collection of tests for the given"
             , String
"expression into a file. The first column in each line is"
             , String
"the expected output, and the remainder are the inputs. The"
             , String
"number of tests is determined by the \"tests\" option."
             ])
    String
""
  , [String]
-> [String] -> CommandBody -> String -> String -> CommandDescr
CommandDescr [ String
":generate-foreign-header" ] [String
"FILE"] ((String -> REPL ()) -> CommandBody
FilenameArg String -> REPL ()
genHeaderCmd)
    String
"Generate a C header file from foreign declarations in a Cryptol file."
    ([String] -> String
unlines
      [ String
"Converts all foreign declarations in the given Cryptol file into C"
      , String
"function declarations, and writes them to a file with the same name"
      , String
"but with a .h extension." ])


  , [String]
-> [String] -> CommandBody -> String -> String -> CommandDescr
CommandDescr [ String
":file-deps" ] [ String
"FILE" ]
    ((String -> REPL ()) -> CommandBody
FilenameArg (Bool -> String -> REPL ()
moduleInfoCmd Bool
True))
    String
"Show information about the dependencies of a file"
    String
""

  , [String]
-> [String] -> CommandBody -> String -> String -> CommandDescr
CommandDescr [ String
":module-deps" ] [ String
"MODULE" ]
    ((String -> REPL ()) -> CommandBody
ModNameArg (Bool -> String -> REPL ()
moduleInfoCmd Bool
False))
    String
"Show information about the dependencies of a module"
    String
""
  ]

genHelp :: [CommandDescr] -> [String]
genHelp :: [CommandDescr] -> [String]
genHelp [CommandDescr]
cs = (CommandDescr -> String) -> [CommandDescr] -> [String]
forall a b. (a -> b) -> [a] -> [b]
map CommandDescr -> String
cmdHelp [CommandDescr]
cs
  where
  cmdHelp :: CommandDescr -> String
cmdHelp CommandDescr
cmd  = [String] -> String
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat ([String] -> String) -> [String] -> String
forall a b. (a -> b) -> a -> b
$ [ String
"  ", CommandDescr -> String
cmdNames CommandDescr
cmd, ShowS
forall {t :: * -> *} {a}. Foldable t => t a -> String
pad (CommandDescr -> String
cmdNames CommandDescr
cmd),
                            String -> [String] -> String
forall a. [a] -> [[a]] -> [a]
intercalate (String
"\n  " String -> ShowS
forall a. [a] -> [a] -> [a]
++ [Any] -> String
forall {t :: * -> *} {a}. Foldable t => t a -> String
pad []) (String -> [String]
lines (CommandDescr -> String
cHelp CommandDescr
cmd)) ]
  cmdNames :: CommandDescr -> String
cmdNames CommandDescr
cmd = String -> [String] -> String
forall a. [a] -> [[a]] -> [a]
intercalate String
", " (CommandDescr -> [String]
cNames CommandDescr
cmd)
  padding :: Int
padding      = Int
2 Int -> Int -> Int
forall a. Num a => a -> a -> a
+ [Int] -> Int
forall a. Ord a => [a] -> a
forall (t :: * -> *) a. (Foldable t, Ord a) => t a -> a
maximum ((CommandDescr -> Int) -> [CommandDescr] -> [Int]
forall a b. (a -> b) -> [a] -> [b]
map (String -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length (String -> Int) -> (CommandDescr -> String) -> CommandDescr -> Int
forall b c a. (b -> c) -> (a -> b) -> a -> c
. CommandDescr -> String
cmdNames) [CommandDescr]
cs)
  pad :: t a -> String
pad t a
n        = Int -> Char -> String
forall a. Int -> a -> [a]
replicate (Int -> Int -> Int
forall a. Ord a => a -> a -> a
max Int
0 (Int
padding Int -> Int -> Int
forall a. Num a => a -> a -> a
- t a -> Int
forall a. t a -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length t a
n)) Char
' '


-- Command Evaluation ----------------------------------------------------------

-- | Run a command.
runCommand :: Int -> Maybe FilePath -> Command -> REPL CommandExitCode
runCommand :: Int -> Maybe String -> Command -> REPL CommandExitCode
runCommand Int
lineNum Maybe String
mbBatch Command
c = case Command
c of

  Command Int -> Maybe String -> REPL ()
cmd -> (Int -> Maybe String -> REPL ()
cmd Int
lineNum Maybe String
mbBatch REPL () -> REPL CommandExitCode -> REPL CommandExitCode
forall a b. REPL a -> REPL b -> REPL b
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> CommandExitCode -> REPL CommandExitCode
forall a. a -> REPL a
forall (m :: * -> *) a. Monad m => a -> m a
return CommandExitCode
CommandOk) REPL CommandExitCode
-> (REPLException -> REPL CommandExitCode) -> REPL CommandExitCode
forall a. REPL a -> (REPLException -> REPL a) -> REPL a
`Cryptol.REPL.Monad.catch` REPLException -> REPL CommandExitCode
forall {a}. PP a => a -> REPL CommandExitCode
handler
    where
    handler :: a -> REPL CommandExitCode
handler a
re = String -> REPL ()
rPutStrLn String
"" REPL () -> REPL () -> REPL ()
forall a b. REPL a -> REPL b -> REPL b
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> Doc -> REPL ()
forall a. Show a => a -> REPL ()
rPrint (a -> Doc
forall a. PP a => a -> Doc
pp a
re) REPL () -> REPL CommandExitCode -> REPL CommandExitCode
forall a b. REPL a -> REPL b -> REPL b
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> CommandExitCode -> REPL CommandExitCode
forall a. a -> REPL a
forall (m :: * -> *) a. Monad m => a -> m a
return CommandExitCode
CommandError

  Unknown String
cmd -> do String -> REPL ()
rPutStrLn (String
"Unknown command: " String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
cmd)
                    CommandExitCode -> REPL CommandExitCode
forall a. a -> REPL a
forall (m :: * -> *) a. Monad m => a -> m a
return CommandExitCode
CommandError

  Ambiguous String
cmd [String]
cmds -> do
    String -> REPL ()
rPutStrLn (String
cmd String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
" is ambiguous, it could mean one of:")
    String -> REPL ()
rPutStrLn (String
"\t" String -> ShowS
forall a. [a] -> [a] -> [a]
++ String -> [String] -> String
forall a. [a] -> [[a]] -> [a]
intercalate String
", " [String]
cmds)
    CommandExitCode -> REPL CommandExitCode
forall a. a -> REPL a
forall (m :: * -> *) a. Monad m => a -> m a
return CommandExitCode
CommandError


evalCmd :: String -> Int -> Maybe FilePath -> REPL ()
evalCmd :: String -> Int -> Maybe String -> REPL ()
evalCmd String
str Int
lineNum Maybe String
mbBatch = do
  ReplInput PName
ri <- String -> Int -> Maybe String -> REPL (ReplInput PName)
replParseInput String
str Int
lineNum Maybe String
mbBatch
  case ReplInput PName
ri of
    P.ExprInput Expr PName
expr -> do
      (Value
val,Type
_ty) <- Expr PName -> REPL (Value, Type)
replEvalExpr Expr PName
expr
      PPOpts
ppOpts <- REPL PPOpts
getPPValOpts
      Doc
valDoc <- Eval Doc -> REPL Doc
forall a. Eval a -> REPL a
rEvalRethrow (Concrete -> PPOpts -> Value -> SEval Concrete Doc
forall sym.
Backend sym =>
sym -> PPOpts -> GenValue sym -> SEval sym Doc
E.ppValue Concrete
Concrete PPOpts
ppOpts Value
val)

      -- This is the point where the value gets forced. We deepseq the
      -- pretty-printed representation of it, rather than the value
      -- itself, leaving it up to the pretty-printer to determine how
      -- much of the value to force
      --out <- io $ rethrowEvalError
      --          $ return $!! show $ pp $ E.WithBase ppOpts val

      String -> REPL ()
rPutStrLn (Doc -> String
forall a. Show a => a -> String
show Doc
valDoc)
    P.LetInput [Decl PName]
ds -> do
      -- explicitly make this a top-level declaration, so that it will
      -- be generalized if mono-binds is enabled
      [Decl PName] -> REPL ()
replEvalDecls [Decl PName]
ds
    ReplInput PName
P.EmptyInput ->
      -- comment or empty input does nothing
      () -> REPL ()
forall a. a -> REPL a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ()

printCounterexample :: CounterExampleType -> Doc -> [Concrete.Value] -> REPL ()
printCounterexample :: CounterExampleType -> Doc -> [Value] -> REPL ()
printCounterexample CounterExampleType
cexTy Doc
exprDoc [Value]
vs =
  do PPOpts
ppOpts <- REPL PPOpts
getPPValOpts
     -- NB: Use a precedence of 1 here, as `vs` will be pretty-printed as
     -- arguments to the function in `exprDoc`. This ensures that arguments
     -- are parenthesized as needed.
     [Doc]
docs <- (Value -> REPL Doc) -> [Value] -> REPL [Doc]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [b]
mapM (Eval Doc -> REPL Doc
forall a. Eval a -> REPL a
rEval (Eval Doc -> REPL Doc) -> (Value -> Eval Doc) -> Value -> REPL Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Concrete -> PPOpts -> Int -> Value -> SEval Concrete Doc
forall sym.
Backend sym =>
sym -> PPOpts -> Int -> GenValue sym -> SEval sym Doc
E.ppValuePrec Concrete
Concrete PPOpts
ppOpts Int
1) [Value]
vs
     let cexRes :: [Doc]
cexRes = case CounterExampleType
cexTy of
           CounterExampleType
SafetyViolation    -> [String -> Doc
text String
"~> ERROR"]
           CounterExampleType
PredicateFalsified -> [String -> Doc
text String
"= False"]
     Doc -> REPL ()
forall a. Show a => a -> REPL ()
rPrint (Doc -> REPL ()) -> Doc -> REPL ()
forall a b. (a -> b) -> a -> b
$ Int -> Doc -> Doc
nest Int
2 ([Doc] -> Doc
sep ([Doc
exprDoc] [Doc] -> [Doc] -> [Doc]
forall a. [a] -> [a] -> [a]
++ [Doc]
docs [Doc] -> [Doc] -> [Doc]
forall a. [a] -> [a] -> [a]
++ [Doc]
cexRes))

printSatisfyingModel :: Doc -> [Concrete.Value] -> REPL ()
printSatisfyingModel :: Doc -> [Value] -> REPL ()
printSatisfyingModel Doc
exprDoc [Value]
vs =
  do PPOpts
ppOpts <- REPL PPOpts
getPPValOpts
     [Doc]
docs <- (Value -> REPL Doc) -> [Value] -> REPL [Doc]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [b]
mapM (Eval Doc -> REPL Doc
forall a. Eval a -> REPL a
rEval (Eval Doc -> REPL Doc) -> (Value -> Eval Doc) -> Value -> REPL Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Concrete -> PPOpts -> Value -> SEval Concrete Doc
forall sym.
Backend sym =>
sym -> PPOpts -> GenValue sym -> SEval sym Doc
E.ppValue Concrete
Concrete PPOpts
ppOpts) [Value]
vs
     Doc -> REPL ()
forall a. Show a => a -> REPL ()
rPrint (Doc -> REPL ()) -> Doc -> REPL ()
forall a b. (a -> b) -> a -> b
$ Int -> Doc -> Doc
nest Int
2 ([Doc] -> Doc
sep ([Doc
exprDoc] [Doc] -> [Doc] -> [Doc]
forall a. [a] -> [a] -> [a]
++ [Doc]
docs [Doc] -> [Doc] -> [Doc]
forall a. [a] -> [a] -> [a]
++ [String -> Doc
text String
"= True"]))


dumpTestsCmd :: FilePath -> String -> (Int,Int) -> Maybe FilePath -> REPL ()
dumpTestsCmd :: String -> String -> (Int, Int) -> Maybe String -> REPL ()
dumpTestsCmd String
outFile String
str (Int, Int)
pos Maybe String
fnm =
  do Expr PName
expr <- String -> (Int, Int) -> Maybe String -> REPL (Expr PName)
replParseExpr String
str (Int, Int)
pos Maybe String
fnm
     (Value
val, Type
ty) <- Expr PName -> REPL (Value, Type)
replEvalExpr Expr PName
expr
     PPOpts
ppopts <- REPL PPOpts
getPPValOpts
     Int
testNum <- String -> REPL Int
forall a. IsEnvVal a => String -> REPL a
getKnownUser String
"tests" :: REPL Int
     TypeEnv
tenv <- GenEvalEnv Concrete -> TypeEnv
forall sym. GenEvalEnv sym -> TypeEnv
E.envTypes (GenEvalEnv Concrete -> TypeEnv)
-> (DynamicEnv -> GenEvalEnv Concrete) -> DynamicEnv -> TypeEnv
forall b c a. (b -> c) -> (a -> b) -> a -> c
. DynamicEnv -> GenEvalEnv Concrete
M.deEnv (DynamicEnv -> TypeEnv) -> REPL DynamicEnv -> REPL TypeEnv
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> REPL DynamicEnv
getDynEnv
     let tyv :: TValue
tyv = TypeEnv -> Type -> TValue
E.evalValType TypeEnv
tenv Type
ty
     [Integer -> TFGen -> (Eval Value, TFGen)]
gens <-
       case TValue -> Maybe [Gen TFGen Concrete]
forall g. RandomGen g => TValue -> Maybe [Gen g Concrete]
TestR.dumpableType TValue
tyv of
         Maybe [Gen TFGen Concrete]
Nothing -> REPLException -> REPL [Integer -> TFGen -> (Eval Value, TFGen)]
forall a. REPLException -> REPL a
raise (Type -> REPLException
TypeNotTestable Type
ty)
         Just [Gen TFGen Concrete]
gens -> [Integer -> TFGen -> (Eval Value, TFGen)]
-> REPL [Integer -> TFGen -> (Eval Value, TFGen)]
forall a. a -> REPL a
forall (m :: * -> *) a. Monad m => a -> m a
return [Integer -> TFGen -> (Eval Value, TFGen)]
[Gen TFGen Concrete]
gens
     [([Value], Value)]
tests <- (TFGen -> REPL ([([Value], Value)], TFGen))
-> REPL [([Value], Value)]
forall a. (TFGen -> REPL (a, TFGen)) -> REPL a
withRandomGen (\TFGen
g -> IO ([([Value], Value)], TFGen) -> REPL ([([Value], Value)], TFGen)
forall a. IO a -> REPL a
io (IO ([([Value], Value)], TFGen)
 -> REPL ([([Value], Value)], TFGen))
-> IO ([([Value], Value)], TFGen)
-> REPL ([([Value], Value)], TFGen)
forall a b. (a -> b) -> a -> b
$ TFGen
-> [Gen TFGen Concrete]
-> Value
-> Int
-> IO ([([Value], Value)], TFGen)
forall g.
RandomGen g =>
g -> [Gen g Concrete] -> Value -> Int -> IO ([([Value], Value)], g)
TestR.returnTests' TFGen
g [Integer -> TFGen -> (Eval Value, TFGen)]
[Gen TFGen Concrete]
gens Value
val Int
testNum)
     [String]
out <- [([Value], Value)]
-> (([Value], Value) -> REPL String) -> REPL [String]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
t a -> (a -> m b) -> m (t b)
forM [([Value], Value)]
tests ((([Value], Value) -> REPL String) -> REPL [String])
-> (([Value], Value) -> REPL String) -> REPL [String]
forall a b. (a -> b) -> a -> b
$
            \([Value]
args, Value
x) ->
              do [Doc]
argOut <- (Value -> REPL Doc) -> [Value] -> REPL [Doc]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [b]
mapM (Eval Doc -> REPL Doc
forall a. Eval a -> REPL a
rEval (Eval Doc -> REPL Doc) -> (Value -> Eval Doc) -> Value -> REPL Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Concrete -> PPOpts -> Value -> SEval Concrete Doc
forall sym.
Backend sym =>
sym -> PPOpts -> GenValue sym -> SEval sym Doc
E.ppValue Concrete
Concrete PPOpts
ppopts) [Value]
args
                 Doc
resOut <- Eval Doc -> REPL Doc
forall a. Eval a -> REPL a
rEval (Concrete -> PPOpts -> Value -> SEval Concrete Doc
forall sym.
Backend sym =>
sym -> PPOpts -> GenValue sym -> SEval sym Doc
E.ppValue Concrete
Concrete PPOpts
ppopts Value
x)
                 String -> REPL String
forall a. a -> REPL a
forall (m :: * -> *) a. Monad m => a -> m a
return (Doc -> String
renderOneLine Doc
resOut String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
"\t" String -> ShowS
forall a. [a] -> [a] -> [a]
++ String -> [String] -> String
forall a. [a] -> [[a]] -> [a]
intercalate String
"\t" ((Doc -> String) -> [Doc] -> [String]
forall a b. (a -> b) -> [a] -> [b]
map Doc -> String
renderOneLine [Doc]
argOut) String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
"\n")
     IO () -> REPL ()
forall a. IO a -> REPL a
io (IO () -> REPL ()) -> IO () -> REPL ()
forall a b. (a -> b) -> a -> b
$ String -> String -> IO ()
writeFile String
outFile ([String] -> String
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat [String]
out) IO () -> (SomeException -> IO ()) -> IO ()
forall e a. Exception e => IO a -> (e -> IO a) -> IO a
`X.catch` SomeException -> IO ()
handler
  where
    handler :: X.SomeException -> IO ()
    handler :: SomeException -> IO ()
handler SomeException
e = String -> IO ()
putStrLn (SomeException -> String
forall e. Exception e => e -> String
X.displayException SomeException
e)



data QCMode = QCRandom | QCExhaust deriving (QCMode -> QCMode -> Bool
(QCMode -> QCMode -> Bool)
-> (QCMode -> QCMode -> Bool) -> Eq QCMode
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: QCMode -> QCMode -> Bool
== :: QCMode -> QCMode -> Bool
$c/= :: QCMode -> QCMode -> Bool
/= :: QCMode -> QCMode -> Bool
Eq, Int -> QCMode -> ShowS
[QCMode] -> ShowS
QCMode -> String
(Int -> QCMode -> ShowS)
-> (QCMode -> String) -> ([QCMode] -> ShowS) -> Show QCMode
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> QCMode -> ShowS
showsPrec :: Int -> QCMode -> ShowS
$cshow :: QCMode -> String
show :: QCMode -> String
$cshowList :: [QCMode] -> ShowS
showList :: [QCMode] -> ShowS
Show)


-- | 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 -> String -> (Int, Int) -> Maybe String -> REPL ()
qcCmd QCMode
qcMode String
"" (Int, Int)
_pos Maybe String
_fnm =
  do ([(Name, IfaceDecl)]
xs,NameDisp
disp) <- REPL ([(Name, IfaceDecl)], NameDisp)
getPropertyNames
     let nameStr :: a -> String
nameStr a
x = Doc -> String
forall a. Show a => a -> String
show (NameDisp -> Doc -> Doc
fixNameDisp NameDisp
disp (a -> Doc
forall a. PP a => a -> Doc
pp a
x))
     if [(Name, IfaceDecl)] -> Bool
forall a. [a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [(Name, IfaceDecl)]
xs
        then String -> REPL ()
rPutStrLn String
"There are no properties in scope."
        else [(Name, IfaceDecl)] -> ((Name, IfaceDecl) -> REPL ()) -> REPL ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
t a -> (a -> m b) -> m ()
forM_ [(Name, IfaceDecl)]
xs (((Name, IfaceDecl) -> REPL ()) -> REPL ())
-> ((Name, IfaceDecl) -> REPL ()) -> REPL ()
forall a b. (a -> b) -> a -> b
$ \(Name
x,IfaceDecl
d) ->
               do let str :: String
str = Name -> String
forall {a}. PP a => a -> String
nameStr Name
x
                  String -> REPL ()
rPutStr (String -> REPL ()) -> String -> REPL ()
forall a b. (a -> b) -> a -> b
$ String
"property " String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
str String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
" "
                  let texpr :: Expr
texpr = Name -> Expr
T.EVar Name
x
                  let schema :: Schema
schema = IfaceDecl -> Schema
M.ifDeclSig IfaceDecl
d
                  NameDisp
nd <- ModContext -> NameDisp
M.mctxNameDisp (ModContext -> NameDisp) -> REPL ModContext -> REPL NameDisp
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> REPL ModContext
getFocusedEnv
                  let doc :: Doc
doc = NameDisp -> Doc -> Doc
fixNameDisp NameDisp
nd (Expr -> Doc
forall a. PP a => a -> Doc
pp Expr
texpr)
                  REPL TestReport -> REPL ()
forall (f :: * -> *) a. Functor f => f a -> f ()
void (QCMode -> Doc -> Expr -> Schema -> REPL TestReport
qcExpr QCMode
qcMode Doc
doc Expr
texpr Schema
schema)

qcCmd QCMode
qcMode String
str (Int, Int)
pos Maybe String
fnm =
  do Expr PName
expr <- String -> (Int, Int) -> Maybe String -> REPL (Expr PName)
replParseExpr String
str (Int, Int)
pos Maybe String
fnm
     (Expr Name
_,Expr
texpr,Schema
schema) <- Expr PName -> REPL (Expr Name, Expr, Schema)
replCheckExpr Expr PName
expr
     NameDisp
nd <- ModContext -> NameDisp
M.mctxNameDisp (ModContext -> NameDisp) -> REPL ModContext -> REPL NameDisp
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> REPL ModContext
getFocusedEnv
     let doc :: Doc
doc = NameDisp -> Doc -> Doc
fixNameDisp NameDisp
nd (Int -> Expr PName -> Doc
forall a. PP a => Int -> a -> Doc
ppPrec Int
3 Expr PName
expr) -- function application has precedence 3
     REPL TestReport -> REPL ()
forall (f :: * -> *) a. Functor f => f a -> f ()
void (QCMode -> Doc -> Expr -> Schema -> REPL TestReport
qcExpr QCMode
qcMode Doc
doc Expr
texpr Schema
schema)


data TestReport = TestReport
  { TestReport -> Doc
reportExpr :: Doc
  , TestReport -> TestResult
reportResult :: TestResult
  , TestReport -> Integer
reportTestsRun :: Integer
  , TestReport -> Maybe Integer
reportTestsPossible :: Maybe Integer
  }

qcExpr ::
  QCMode ->
  Doc ->
  T.Expr ->
  T.Schema ->
  REPL TestReport
qcExpr :: QCMode -> Doc -> Expr -> Schema -> REPL TestReport
qcExpr QCMode
qcMode Doc
exprDoc Expr
texpr Schema
schema =
  do (Value
val,Type
ty) <- Expr -> Schema -> REPL (Maybe (Value, Type))
replEvalCheckedExpr Expr
texpr Schema
schema REPL (Maybe (Value, Type))
-> (Maybe (Value, Type) -> REPL (Value, Type))
-> REPL (Value, Type)
forall a b. REPL a -> (a -> REPL b) -> REPL b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \Maybe (Value, Type)
mb_res -> case Maybe (Value, Type)
mb_res of
       Just (Value, Type)
res -> (Value, Type) -> REPL (Value, Type)
forall a. a -> REPL a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Value, Type)
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.
       Maybe (Value, Type)
Nothing -> REPLException -> REPL (Value, Type)
forall a. REPLException -> REPL a
raise (Schema -> REPLException
InstantiationsNotFound Schema
schema)
     Integer
testNum <- (Int -> Integer
forall a. Integral a => a -> Integer
toInteger :: Int -> Integer) (Int -> Integer) -> REPL Int -> REPL Integer
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> String -> REPL Int
forall a. IsEnvVal a => String -> REPL a
getKnownUser String
"tests"
     TypeEnv
tenv <- GenEvalEnv Concrete -> TypeEnv
forall sym. GenEvalEnv sym -> TypeEnv
E.envTypes (GenEvalEnv Concrete -> TypeEnv)
-> (DynamicEnv -> GenEvalEnv Concrete) -> DynamicEnv -> TypeEnv
forall b c a. (b -> c) -> (a -> b) -> a -> c
. DynamicEnv -> GenEvalEnv Concrete
M.deEnv (DynamicEnv -> TypeEnv) -> REPL DynamicEnv -> REPL TypeEnv
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> REPL DynamicEnv
getDynEnv
     let tyv :: TValue
tyv = TypeEnv -> Type -> TValue
E.evalValType TypeEnv
tenv Type
ty
     -- tv has already had polymorphism instantiated 
     IORef (Maybe String)
percentRef <- IO (IORef (Maybe String)) -> REPL (IORef (Maybe String))
forall a. IO a -> REPL a
io (IO (IORef (Maybe String)) -> REPL (IORef (Maybe String)))
-> IO (IORef (Maybe String)) -> REPL (IORef (Maybe String))
forall a b. (a -> b) -> a -> b
$ Maybe String -> IO (IORef (Maybe String))
forall a. a -> IO (IORef a)
newIORef Maybe String
forall a. Maybe a
Nothing
     IORef Integer
testsRef <- IO (IORef Integer) -> REPL (IORef Integer)
forall a. IO a -> REPL a
io (IO (IORef Integer) -> REPL (IORef Integer))
-> IO (IORef Integer) -> REPL (IORef Integer)
forall a b. (a -> b) -> a -> b
$ Integer -> IO (IORef Integer)
forall a. a -> IO (IORef a)
newIORef Integer
0

     case TValue
-> Maybe (Maybe Integer, [TValue], [[Value]], [Gen TFGen Concrete])
forall g.
RandomGen g =>
TValue
-> Maybe (Maybe Integer, [TValue], [[Value]], [Gen g Concrete])
testableType TValue
tyv of
       Just (Just Integer
sz,[TValue]
tys,[[Value]]
vss,[Gen TFGen Concrete]
_gens) | QCMode
qcMode QCMode -> QCMode -> Bool
forall a. Eq a => a -> a -> Bool
== QCMode
QCExhaust Bool -> Bool -> Bool
|| Integer
sz Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
<= Integer
testNum -> do
            String -> REPL ()
rPutStrLn String
"Using exhaustive testing."
            String -> REPL ()
prt String
testingMsg
            (TestResult
res,Integer
num) <-
                  REPL (TestResult, Integer)
-> (SomeException -> REPL (TestResult, Integer))
-> REPL (TestResult, Integer)
forall e a.
(HasCallStack, Exception e) =>
REPL a -> (e -> REPL a) -> REPL a
forall (m :: * -> *) e a.
(MonadCatch m, HasCallStack, Exception e) =>
m a -> (e -> m a) -> m a
Ex.catch ((Integer -> REPL ())
-> Value -> [[Value]] -> REPL (TestResult, Integer)
forall (m :: * -> *).
MonadIO m =>
(Integer -> m ()) -> Value -> [[Value]] -> m (TestResult, Integer)
exhaustiveTests (\Integer
n -> IORef (Maybe String)
-> IORef Integer -> Integer -> Integer -> REPL ()
forall {a}.
(Show a, Integral a) =>
IORef (Maybe String) -> IORef a -> a -> a -> REPL ()
ppProgress IORef (Maybe String)
percentRef IORef Integer
testsRef Integer
n Integer
sz)
                                            Value
val [[Value]]
vss)
                         (\SomeException
ex -> do String -> REPL ()
rPutStrLn String
"\nTest interrupted..."
                                    Integer
num <- IO Integer -> REPL Integer
forall a. IO a -> REPL a
io (IO Integer -> REPL Integer) -> IO Integer -> REPL Integer
forall a b. (a -> b) -> a -> b
$ IORef Integer -> IO Integer
forall a. IORef a -> IO a
readIORef IORef Integer
testsRef
                                    let report :: TestReport
report = Doc -> TestResult -> Integer -> Maybe Integer -> TestReport
TestReport Doc
exprDoc TestResult
Pass Integer
num (Integer -> Maybe Integer
forall a. a -> Maybe a
Just Integer
sz)
                                    [TValue] -> Bool -> TestReport -> REPL ()
ppReport [TValue]
tys Bool
False TestReport
report
                                    String -> REPL ()
rPutStrLn (String -> REPL ()) -> String -> REPL ()
forall a b. (a -> b) -> a -> b
$ Integer -> Integer -> String
interruptedExhaust Integer
num Integer
sz
                                    SomeException -> REPL (TestResult, Integer)
forall e a. (HasCallStack, Exception e) => e -> REPL a
forall (m :: * -> *) e a.
(MonadThrow m, HasCallStack, Exception e) =>
e -> m a
Ex.throwM (SomeException
ex :: Ex.SomeException))
            let report :: TestReport
report = Doc -> TestResult -> Integer -> Maybe Integer -> TestReport
TestReport Doc
exprDoc TestResult
res Integer
num (Integer -> Maybe Integer
forall a. a -> Maybe a
Just Integer
sz)
            REPL ()
delProgress
            REPL ()
delTesting
            [TValue] -> Bool -> TestReport -> REPL ()
ppReport [TValue]
tys Bool
True TestReport
report
            TestReport -> REPL TestReport
forall a. a -> REPL a
forall (m :: * -> *) a. Monad m => a -> m a
return TestReport
report

       Just (Maybe Integer
sz,[TValue]
tys,[[Value]]
_,[Gen TFGen Concrete]
gens) | QCMode
qcMode QCMode -> QCMode -> Bool
forall a. Eq a => a -> a -> Bool
== QCMode
QCRandom -> do
            String -> REPL ()
rPutStrLn String
"Using random testing."
            String -> REPL ()
prt String
testingMsg
            (TestResult
res,Integer
num) <-
              (TFGen -> REPL ((TestResult, Integer), TFGen))
-> REPL (TestResult, Integer)
forall a. (TFGen -> REPL (a, TFGen)) -> REPL a
withRandomGen
                ((Integer -> REPL ())
-> Integer
-> Value
-> [Gen TFGen Concrete]
-> TFGen
-> REPL ((TestResult, Integer), TFGen)
forall (m :: * -> *) g.
(MonadIO m, RandomGen g) =>
(Integer -> m ())
-> Integer
-> Value
-> [Gen g Concrete]
-> g
-> m ((TestResult, Integer), g)
randomTests' (\Integer
n -> IORef (Maybe String)
-> IORef Integer -> Integer -> Integer -> REPL ()
forall {a}.
(Show a, Integral a) =>
IORef (Maybe String) -> IORef a -> a -> a -> REPL ()
ppProgress IORef (Maybe String)
percentRef IORef Integer
testsRef Integer
n Integer
testNum)
                                      Integer
testNum Value
val [Gen TFGen Concrete]
gens)
              REPL (TestResult, Integer)
-> (SomeException -> REPL (TestResult, Integer))
-> REPL (TestResult, Integer)
forall e a.
(HasCallStack, Exception e) =>
REPL a -> (e -> REPL a) -> REPL a
forall (m :: * -> *) e a.
(MonadCatch m, HasCallStack, Exception e) =>
m a -> (e -> m a) -> m a
`Ex.catch` (\SomeException
ex -> do String -> REPL ()
rPutStrLn String
"\nTest interrupted..."
                                    Integer
num <- IO Integer -> REPL Integer
forall a. IO a -> REPL a
io (IO Integer -> REPL Integer) -> IO Integer -> REPL Integer
forall a b. (a -> b) -> a -> b
$ IORef Integer -> IO Integer
forall a. IORef a -> IO a
readIORef IORef Integer
testsRef
                                    let report :: TestReport
report = Doc -> TestResult -> Integer -> Maybe Integer -> TestReport
TestReport Doc
exprDoc TestResult
Pass Integer
num Maybe Integer
sz
                                    [TValue] -> Bool -> TestReport -> REPL ()
ppReport [TValue]
tys Bool
False TestReport
report
                                    case Maybe Integer
sz of
                                      Just Integer
n -> String -> REPL ()
rPutStrLn (String -> REPL ()) -> String -> REPL ()
forall a b. (a -> b) -> a -> b
$ Integer -> Integer -> String
coverageString Integer
num Integer
n
                                      Maybe Integer
_ -> () -> REPL ()
forall a. a -> REPL a
forall (m :: * -> *) a. Monad m => a -> m a
return ()
                                    SomeException -> REPL (TestResult, Integer)
forall e a. (HasCallStack, Exception e) => e -> REPL a
forall (m :: * -> *) e a.
(MonadThrow m, HasCallStack, Exception e) =>
e -> m a
Ex.throwM (SomeException
ex :: Ex.SomeException))
            let report :: TestReport
report = Doc -> TestResult -> Integer -> Maybe Integer -> TestReport
TestReport Doc
exprDoc TestResult
res Integer
num Maybe Integer
sz
            REPL ()
delProgress
            REPL ()
delTesting
            [TValue] -> Bool -> TestReport -> REPL ()
ppReport [TValue]
tys Bool
False TestReport
report
            case Maybe Integer
sz of
              Just Integer
n | TestResult -> Bool
isPass TestResult
res -> String -> REPL ()
rPutStrLn (String -> REPL ()) -> String -> REPL ()
forall a b. (a -> b) -> a -> b
$ Integer -> Integer -> String
coverageString Integer
testNum Integer
n
              Maybe Integer
_ -> () -> REPL ()
forall a. a -> REPL a
forall (m :: * -> *) a. Monad m => a -> m a
return ()
            TestReport -> REPL TestReport
forall a. a -> REPL a
forall (m :: * -> *) a. Monad m => a -> m a
return TestReport
report
       Maybe (Maybe Integer, [TValue], [[Value]], [Gen TFGen Concrete])
_ -> REPLException -> REPL TestReport
forall a. REPLException -> REPL a
raise (Type -> REPLException
TypeNotTestable Type
ty)

  where
  testingMsg :: String
testingMsg = String
"Testing... "

  interruptedExhaust :: Integer -> Integer -> String
interruptedExhaust Integer
testNum Integer
sz =
     let percent :: Double
percent = (Double
100.0 :: Double) Double -> Double -> Double
forall a. Num a => a -> a -> a
* (Integer -> Double
forall a. Num a => Integer -> a
fromInteger Integer
testNum) Double -> Double -> Double
forall a. Fractional a => a -> a -> a
/ Integer -> Double
forall a. Num a => Integer -> a
fromInteger Integer
sz
         showValNum :: String
showValNum
            | Integer
sz Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
> Integer
2 Integer -> Integer -> Integer
forall a b. (Num a, Integral b) => a -> b -> a
^ (Integer
20::Integer) =
              String
"2^^" String -> ShowS
forall a. [a] -> [a] -> [a]
++ Integer -> String
forall a. Show a => a -> String
show (Integer -> Integer
lg2 Integer
sz)
            | Bool
otherwise = Integer -> String
forall a. Show a => a -> String
show Integer
sz
      in String
"Test coverage: "
            String -> ShowS
forall a. [a] -> [a] -> [a]
++ Maybe Int -> Double -> ShowS
forall a. RealFloat a => Maybe Int -> a -> ShowS
showFFloat (Int -> Maybe Int
forall a. a -> Maybe a
Just Int
2) Double
percent String
"% ("
            String -> ShowS
forall a. [a] -> [a] -> [a]
++ Integer -> String
forall a. Show a => a -> String
show Integer
testNum String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
" of "
            String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
showValNum
            String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
" values)"

  coverageString :: Integer -> Integer -> String
coverageString Integer
testNum Integer
sz =
     let (Double
percent, Double
expectedUnique) = Integer -> Integer -> (Double, Double)
expectedCoverage Integer
testNum Integer
sz
         showValNum :: String
showValNum
           | Integer
sz Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
> Integer
2 Integer -> Integer -> Integer
forall a b. (Num a, Integral b) => a -> b -> a
^ (Integer
20::Integer) =
             String
"2^^" String -> ShowS
forall a. [a] -> [a] -> [a]
++ Integer -> String
forall a. Show a => a -> String
show (Integer -> Integer
lg2 Integer
sz)
           | Bool
otherwise = Integer -> String
forall a. Show a => a -> String
show Integer
sz
     in String
"Expected test coverage: "
       String -> ShowS
forall a. [a] -> [a] -> [a]
++ Maybe Int -> Double -> ShowS
forall a. RealFloat a => Maybe Int -> a -> ShowS
showFFloat (Int -> Maybe Int
forall a. a -> Maybe a
Just Int
2) Double
percent String
"% ("
       String -> ShowS
forall a. [a] -> [a] -> [a]
++ Maybe Int -> Double -> ShowS
forall a. RealFloat a => Maybe Int -> a -> ShowS
showFFloat (Int -> Maybe Int
forall a. a -> Maybe a
Just Int
0) Double
expectedUnique String
" of "
       String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
showValNum
       String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
" values)"

  totProgressWidth :: Int
totProgressWidth = Int
4    -- 100%

  lg2 :: Integer -> Integer
  lg2 :: Integer -> Integer
lg2 Integer
x | Integer
x Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
>= Integer
2Integer -> Int -> Integer
forall a b. (Num a, Integral b) => a -> b -> a
^(Int
1024::Int) = Integer
1024 Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
+ Integer -> Integer
lg2 (Integer
x Integer -> Integer -> Integer
forall a. Integral a => a -> a -> a
`div` Integer
2Integer -> Int -> Integer
forall a b. (Num a, Integral b) => a -> b -> a
^(Int
1024::Int))
        | Integer
x Integer -> Integer -> Bool
forall a. Eq a => a -> a -> Bool
== Integer
0       = Integer
0
        | Bool
otherwise    = let valNumD :: Double
valNumD = Integer -> Double
forall a. Num a => Integer -> a
fromInteger Integer
x :: Double
                         in Double -> Integer
forall b. Integral b => Double -> b
forall a b. (RealFrac a, Integral b) => a -> b
round (Double -> Integer) -> Double -> Integer
forall a b. (a -> b) -> a -> b
$ Double -> Double -> Double
forall a. Floating a => a -> a -> a
logBase Double
2 Double
valNumD :: Integer

  prt :: String -> REPL ()
prt String
msg   = String -> REPL ()
rPutStr String
msg REPL () -> REPL () -> REPL ()
forall a b. REPL a -> REPL b -> REPL b
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> IO () -> REPL ()
forall a. IO a -> REPL a
io (Handle -> IO ()
hFlush Handle
stdout)

  ppProgress :: IORef (Maybe String) -> IORef a -> a -> a -> REPL ()
ppProgress IORef (Maybe String)
percentRef IORef a
testsRef a
this a
tot =
    do IO () -> REPL ()
forall a. IO a -> REPL a
io (IO () -> REPL ()) -> IO () -> REPL ()
forall a b. (a -> b) -> a -> b
$ IORef a -> a -> IO ()
forall a. IORef a -> a -> IO ()
writeIORef IORef a
testsRef a
this
       let percent :: String
percent = a -> String
forall a. Show a => a -> String
show (a -> a -> a
forall a. Integral a => a -> a -> a
div (a
100 a -> a -> a
forall a. Num a => a -> a -> a
* a
this) a
tot) String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
"%"
           width :: Int
width   = String -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length String
percent
           pad :: String
pad     = Int -> Char -> String
forall a. Int -> a -> [a]
replicate (Int
totProgressWidth Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
width) Char
' '
       REPL () -> REPL ()
unlessBatch (REPL () -> REPL ()) -> REPL () -> REPL ()
forall a b. (a -> b) -> a -> b
$
         do Maybe String
oldPercent <- IO (Maybe String) -> REPL (Maybe String)
forall a. IO a -> REPL a
io (IO (Maybe String) -> REPL (Maybe String))
-> IO (Maybe String) -> REPL (Maybe String)
forall a b. (a -> b) -> a -> b
$ IORef (Maybe String) -> IO (Maybe String)
forall a. IORef a -> IO a
readIORef IORef (Maybe String)
percentRef
            case Maybe String
oldPercent of
              Maybe String
Nothing ->
                do IO () -> REPL ()
forall a. IO a -> REPL a
io (IO () -> REPL ()) -> IO () -> REPL ()
forall a b. (a -> b) -> a -> b
$ IORef (Maybe String) -> Maybe String -> IO ()
forall a. IORef a -> a -> IO ()
writeIORef IORef (Maybe String)
percentRef (String -> Maybe String
forall a. a -> Maybe a
Just String
percent)
                   String -> REPL ()
prt (String
pad String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
percent)
              Just String
p | String
p String -> String -> Bool
forall a. Eq a => a -> a -> Bool
/= String
percent ->
                do IO () -> REPL ()
forall a. IO a -> REPL a
io (IO () -> REPL ()) -> IO () -> REPL ()
forall a b. (a -> b) -> a -> b
$ IORef (Maybe String) -> Maybe String -> IO ()
forall a. IORef a -> a -> IO ()
writeIORef IORef (Maybe String)
percentRef (String -> Maybe String
forall a. a -> Maybe a
Just String
percent)
                   REPL ()
delProgress
                   String -> REPL ()
prt (String
pad String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
percent)
              Maybe String
_ -> () -> REPL ()
forall a. a -> REPL a
forall (m :: * -> *) a. Monad m => a -> m a
return ()

  del :: Int -> REPL ()
del Int
n       = REPL () -> REPL ()
unlessBatch
              (REPL () -> REPL ()) -> REPL () -> REPL ()
forall a b. (a -> b) -> a -> b
$ String -> REPL ()
prt (Int -> Char -> String
forall a. Int -> a -> [a]
replicate Int
n Char
'\BS' String -> ShowS
forall a. [a] -> [a] -> [a]
++ Int -> Char -> String
forall a. Int -> a -> [a]
replicate Int
n Char
' ' String -> ShowS
forall a. [a] -> [a] -> [a]
++ Int -> Char -> String
forall a. Int -> a -> [a]
replicate Int
n Char
'\BS')
  delTesting :: REPL ()
delTesting  = Int -> REPL ()
del (String -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length String
testingMsg)
  delProgress :: REPL ()
delProgress = Int -> REPL ()
del Int
totProgressWidth


ppReport :: [E.TValue] -> Bool -> TestReport -> REPL ()
ppReport :: [TValue] -> Bool -> TestReport -> REPL ()
ppReport [TValue]
_tys Bool
isExhaustive (TestReport Doc
_exprDoc TestResult
Pass Integer
testNum Maybe Integer
_testPossible) =
    do String -> REPL ()
rPutStrLn (String
"Passed " String -> ShowS
forall a. [a] -> [a] -> [a]
++ Integer -> String
forall a. Show a => a -> String
show Integer
testNum String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
" tests.")
       Bool -> REPL () -> REPL ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when Bool
isExhaustive (String -> REPL ()
rPutStrLn String
"Q.E.D.")
ppReport [TValue]
tys Bool
_ (TestReport Doc
exprDoc TestResult
failure Integer
_testNum Maybe Integer
_testPossible) =
    do [TValue] -> Doc -> TestResult -> REPL ()
ppFailure [TValue]
tys Doc
exprDoc TestResult
failure

ppFailure :: [E.TValue] -> Doc -> TestResult -> REPL ()
ppFailure :: [TValue] -> Doc -> TestResult -> REPL ()
ppFailure [TValue]
tys Doc
exprDoc TestResult
failure = do
    ~(EnvBool Bool
showEx) <- String -> REPL EnvVal
getUser String
"showExamples"

    [Value]
vs <- case TestResult
failure of
            FailFalse [Value]
vs ->
              do String -> REPL ()
rPutStrLn String
"Counterexample"
                 Bool -> REPL () -> REPL ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when Bool
showEx (CounterExampleType -> Doc -> [Value] -> REPL ()
printCounterexample CounterExampleType
PredicateFalsified Doc
exprDoc [Value]
vs)
                 [Value] -> REPL [Value]
forall a. a -> REPL a
forall (f :: * -> *) a. Applicative f => a -> f a
pure [Value]
vs
            FailError EvalErrorEx
err [Value]
vs
              | [Value] -> Bool
forall a. [a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [Value]
vs Bool -> Bool -> Bool
|| Bool -> Bool
not Bool
showEx ->
                do String -> REPL ()
rPutStrLn String
"ERROR"
                   Doc -> REPL ()
forall a. Show a => a -> REPL ()
rPrint (EvalErrorEx -> Doc
forall a. PP a => a -> Doc
pp EvalErrorEx
err)
                   [Value] -> REPL [Value]
forall a. a -> REPL a
forall (f :: * -> *) a. Applicative f => a -> f a
pure [Value]
vs
              | Bool
otherwise ->
                do String -> REPL ()
rPutStrLn String
"ERROR for the following inputs:"
                   CounterExampleType -> Doc -> [Value] -> REPL ()
printCounterexample CounterExampleType
SafetyViolation Doc
exprDoc [Value]
vs
                   Doc -> REPL ()
forall a. Show a => a -> REPL ()
rPrint (EvalErrorEx -> Doc
forall a. PP a => a -> Doc
pp EvalErrorEx
err)
                   [Value] -> REPL [Value]
forall a. a -> REPL a
forall (f :: * -> *) a. Applicative f => a -> f a
pure [Value]
vs

            TestResult
Pass -> String -> [String] -> REPL [Value]
forall a. HasCallStack => String -> [String] -> a
panic String
"Cryptol.REPL.Command" [String
"unexpected Test.Pass"]

    -- bind the 'it' variable
    case ([TValue]
tys,[Value]
vs) of
      ([TValue
t],[Value
v]) -> TValue -> Value -> REPL ()
bindItVariableVal TValue
t Value
v
      ([TValue], [Value])
_ -> let fs :: [Ident]
fs = [ String -> Ident
M.packIdent (String
"arg" String -> ShowS
forall a. [a] -> [a] -> [a]
++ Int -> String
forall a. Show a => a -> String
show (Int
i::Int)) | Int
i <- [ Int
1 .. ] ]
               t :: TValue
t = RecordMap Ident TValue -> TValue
E.TVRec ([(Ident, TValue)] -> RecordMap Ident TValue
forall a b. (Show a, Ord a) => [(a, b)] -> RecordMap a b
recordFromFields ([Ident] -> [TValue] -> [(Ident, TValue)]
forall a b. [a] -> [b] -> [(a, b)]
zip [Ident]
fs [TValue]
tys))
               v :: Value
v = RecordMap Ident (SEval Concrete Value) -> Value
forall sym.
RecordMap Ident (SEval sym (GenValue sym)) -> GenValue sym
E.VRecord ([(Ident, Eval Value)] -> RecordMap Ident (Eval Value)
forall a b. (Show a, Ord a) => [(a, b)] -> RecordMap a b
recordFromFields ([Ident] -> [Eval Value] -> [(Ident, Eval Value)]
forall a b. [a] -> [b] -> [(a, b)]
zip [Ident]
fs ((Value -> Eval Value) -> [Value] -> [Eval Value]
forall a b. (a -> b) -> [a] -> [b]
map Value -> Eval Value
forall a. a -> Eval a
forall (m :: * -> *) a. Monad m => a -> m a
return [Value]
vs)))
           in TValue -> Value -> REPL ()
bindItVariableVal TValue
t Value
v


-- | This function computes the expected coverage percentage and
-- expected number of unique test vectors when using random testing.
--
-- The expected test coverage proportion is:
--  @1 - ((n-1)/n)^k@
--
-- This formula takes into account the fact that test vectors are chosen
-- uniformly at random _with replacement_, and thus the same vectors
-- may be generated multiple times.  If the test vectors were chosen
-- randomly without replacement, the proportion would instead be @k/n@.
--
-- We compute raising to the @k@ power in the log domain to improve
-- numerical precision. The equivalant comptutation is:
--   @-expm1( k * log1p (-1/n) )@
--
-- Where @expm1(x) = exp(x) - 1@ and @log1p(x) = log(1 + x)@.
--
-- However, if @sz@ is large enough, even carefully preserving
-- precision may not be enough to get sensible results.  In such
-- situations, we expect the naive approximation @k/n@ to be very
-- close to accurate and the expected number of unique values is
-- essentially equal to the number of tests.
expectedCoverage :: Integer -> Integer -> (Double, Double)
expectedCoverage :: Integer -> Integer -> (Double, Double)
expectedCoverage Integer
testNum Integer
sz =
    -- If the Double computation has enough precision, use the
    --  "with replacement" formula.
    if Integer
testNum Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
> Integer
0 Bool -> Bool -> Bool
&& Double
proportion Double -> Double -> Bool
forall a. Ord a => a -> a -> Bool
> Double
0 then
       (Double
100.0 Double -> Double -> Double
forall a. Num a => a -> a -> a
* Double
proportion, Double
szD Double -> Double -> Double
forall a. Num a => a -> a -> a
* Double
proportion)
    else
       (Double
100.0 Double -> Double -> Double
forall a. Num a => a -> a -> a
* Double
naiveProportion, Double
numD)

  where
   szD :: Double
   szD :: Double
szD = Integer -> Double
forall a. Num a => Integer -> a
fromInteger Integer
sz

   numD :: Double
   numD :: Double
numD = Integer -> Double
forall a b. (Integral a, Num b) => a -> b
fromIntegral Integer
testNum

   naiveProportion :: Double
naiveProportion = Double
numD Double -> Double -> Double
forall a. Fractional a => a -> a -> a
/ Double
szD

   proportion :: Double
proportion = Double -> Double
forall a. Num a => a -> a
negate (Double -> Double
forall a. Floating a => a -> a
expm1 (Double
numD Double -> Double -> Double
forall a. Num a => a -> a -> a
* Double -> Double
forall a. Floating a => a -> a
log1p (Double -> Double
forall a. Num a => a -> a
negate (Double -> Double
forall a. Fractional a => a -> a
recip Double
szD))))

satCmd, proveCmd :: String -> (Int,Int) -> Maybe FilePath -> REPL ()
satCmd :: String -> (Int, Int) -> Maybe String -> REPL ()
satCmd = Bool -> String -> (Int, Int) -> Maybe String -> REPL ()
cmdProveSat Bool
True
proveCmd :: String -> (Int, Int) -> Maybe String -> REPL ()
proveCmd = Bool -> String -> (Int, Int) -> Maybe String -> REPL ()
cmdProveSat Bool
False

showProverStats :: Maybe String -> ProverStats -> REPL ()
showProverStats :: Maybe String -> ProverStats -> REPL ()
showProverStats Maybe String
mprover ProverStats
stat = String -> REPL ()
rPutStrLn String
msg
  where

  msg :: String
msg = String
"(Total Elapsed Time: " String -> ShowS
forall a. [a] -> [a] -> [a]
++ ProverStats -> String
SBV.showTDiff ProverStats
stat String -> ShowS
forall a. [a] -> [a] -> [a]
++
        String -> ShowS -> Maybe String -> String
forall b a. b -> (a -> b) -> Maybe a -> b
maybe String
"" (\String
p -> String
", using " String -> ShowS
forall a. [a] -> [a] -> [a]
++ ShowS
forall a. Show a => a -> String
show String
p) Maybe String
mprover String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
")"

rethrowErrorCall :: REPL a -> REPL a
rethrowErrorCall :: forall a. REPL a -> REPL a
rethrowErrorCall REPL a
m = (IORef RW -> IO a) -> REPL a
forall a. (IORef RW -> IO a) -> REPL a
REPL (\IORef RW
r -> REPL a -> IORef RW -> IO a
forall a. REPL a -> IORef RW -> IO a
unREPL REPL a
m IORef RW
r IO a -> [Handler a] -> IO a
forall a. IO a -> [Handler a] -> IO a
`X.catches` [Handler a]
forall {a}. [Handler a]
hs)
  where
    hs :: [Handler a]
hs =
      [ (ErrorCall -> IO a) -> Handler a
forall a e. Exception e => (e -> IO a) -> Handler a
X.Handler ((ErrorCall -> IO a) -> Handler a)
-> (ErrorCall -> IO a) -> Handler a
forall a b. (a -> b) -> a -> b
$ \ (X.ErrorCallWithLocation String
s String
_) -> REPLException -> IO a
forall e a. Exception e => e -> IO a
X.throwIO (String -> REPLException
SBVError String
s)
      , (SBVException -> IO a) -> Handler a
forall a e. Exception e => (e -> IO a) -> Handler a
X.Handler ((SBVException -> IO a) -> Handler a)
-> (SBVException -> IO a) -> Handler a
forall a b. (a -> b) -> a -> b
$ \ SBVException
e -> REPLException -> IO a
forall e a. Exception e => e -> IO a
X.throwIO (SBVException -> REPLException
SBVException SBVException
e)
      , (SBVPortfolioException -> IO a) -> Handler a
forall a e. Exception e => (e -> IO a) -> Handler a
X.Handler ((SBVPortfolioException -> IO a) -> Handler a)
-> (SBVPortfolioException -> IO a) -> Handler a
forall a b. (a -> b) -> a -> b
$ \ SBVPortfolioException
e -> REPLException -> IO a
forall e a. Exception e => e -> IO a
X.throwIO (SBVPortfolioException -> REPLException
SBVPortfolioException SBVPortfolioException
e)
      , (W4Exception -> IO a) -> Handler a
forall a e. Exception e => (e -> IO a) -> Handler a
X.Handler ((W4Exception -> IO a) -> Handler a)
-> (W4Exception -> IO a) -> Handler a
forall a b. (a -> b) -> a -> b
$ \ W4Exception
e -> REPLException -> IO a
forall e a. Exception e => e -> IO a
X.throwIO (W4Exception -> REPLException
W4Exception W4Exception
e)
      ]

-- | Attempts to prove the given term is safe for all inputs
safeCmd :: String -> (Int,Int) -> Maybe FilePath -> REPL ()
safeCmd :: String -> (Int, Int) -> Maybe String -> REPL ()
safeCmd String
str (Int, Int)
pos Maybe String
fnm = do
  String
proverName <- String -> REPL String
forall a. IsEnvVal a => String -> REPL a
getKnownUser String
"prover"
  String
fileName   <- String -> REPL String
forall a. IsEnvVal a => String -> REPL a
getKnownUser String
"smtFile"
  let mfile :: Maybe String
mfile = if String
fileName String -> String -> Bool
forall a. Eq a => a -> a -> Bool
== String
"-" then Maybe String
forall a. Maybe a
Nothing else String -> Maybe String
forall a. a -> Maybe a
Just String
fileName
  Expr PName
pexpr <- String -> (Int, Int) -> Maybe String -> REPL (Expr PName)
replParseExpr String
str (Int, Int)
pos Maybe String
fnm
  NameDisp
nd <- ModContext -> NameDisp
M.mctxNameDisp (ModContext -> NameDisp) -> REPL ModContext -> REPL NameDisp
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> REPL ModContext
getFocusedEnv
  let exprDoc :: Doc
exprDoc = NameDisp -> Doc -> Doc
fixNameDisp NameDisp
nd (Int -> Expr PName -> Doc
forall a. PP a => Int -> a -> Doc
ppPrec Int
3 Expr PName
pexpr) -- function application has precedence 3

  let rng :: Range
rng = Range -> Maybe Range -> Range
forall a. a -> Maybe a -> a
fromMaybe ((Int, Int) -> Maybe String -> Range
mkInteractiveRange (Int, Int)
pos Maybe String
fnm) (Expr PName -> Maybe Range
forall t. HasLoc t => t -> Maybe Range
getLoc Expr PName
pexpr)
  (Expr Name
_,Expr
texpr,Schema
schema) <- Expr PName -> REPL (Expr Name, Expr, Schema)
replCheckExpr Expr PName
pexpr

  if String
proverName String -> [String] -> Bool
forall a. Eq a => a -> [a] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [String
"offline",String
"sbv-offline",String
"w4-offline"] then
    String -> QueryType -> Expr -> Schema -> Maybe String -> REPL ()
offlineProveSat String
proverName QueryType
SafetyQuery Expr
texpr Schema
schema Maybe String
mfile
  else
     do (Maybe String
firstProver,ProverResult
result,ProverStats
stats) <- REPL (Maybe String, ProverResult, ProverStats)
-> REPL (Maybe String, ProverResult, ProverStats)
forall a. REPL a -> REPL a
rethrowErrorCall (String
-> QueryType
-> Expr
-> Schema
-> Maybe String
-> REPL (Maybe String, ProverResult, ProverStats)
onlineProveSat String
proverName QueryType
SafetyQuery Expr
texpr Schema
schema Maybe String
mfile)
        case ProverResult
result of
          ProverResult
EmptyResult         ->
            String -> [String] -> REPL ()
forall a. HasCallStack => String -> [String] -> a
panic String
"REPL.Command" [ String
"got EmptyResult for online prover query" ]

          ProverError String
msg -> String -> REPL ()
rPutStrLn String
msg

          ThmResult [TValue]
_ts -> String -> REPL ()
rPutStrLn String
"Safe"

          CounterExample CounterExampleType
cexType SatResult
tevs -> do
            String -> REPL ()
rPutStrLn String
"Counterexample"
            let tes :: [(TValue, Expr)]
tes = ((TValue, Expr, Value) -> (TValue, Expr))
-> SatResult -> [(TValue, Expr)]
forall a b. (a -> b) -> [a] -> [b]
map ( \(TValue
t,Expr
e,Value
_) -> (TValue
t,Expr
e)) SatResult
tevs
                vs :: [Value]
vs  = ((TValue, Expr, Value) -> Value) -> SatResult -> [Value]
forall a b. (a -> b) -> [a] -> [b]
map ( \(TValue
_,Expr
_,Value
v) -> Value
v)     SatResult
tevs

            (TValue
t,Expr
e) <- String
-> Range
-> Bool
-> Either [TValue] [(TValue, Expr)]
-> REPL (TValue, Expr)
mkSolverResult String
"counterexample" Range
rng Bool
False ([(TValue, Expr)] -> Either [TValue] [(TValue, Expr)]
forall a b. b -> Either a b
Right [(TValue, Expr)]
tes)

            ~(EnvBool Bool
yes) <- String -> REPL EnvVal
getUser String
"showExamples"
            Bool -> REPL () -> REPL ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when Bool
yes (REPL () -> REPL ()) -> REPL () -> REPL ()
forall a b. (a -> b) -> a -> b
$ CounterExampleType -> Doc -> [Value] -> REPL ()
printCounterexample CounterExampleType
cexType Doc
exprDoc [Value]
vs
            Bool -> REPL () -> REPL ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when Bool
yes (REPL () -> REPL ()) -> REPL () -> REPL ()
forall a b. (a -> b) -> a -> b
$ Expr -> Schema -> [Value] -> REPL ()
printSafetyViolation Expr
texpr Schema
schema [Value]
vs

            REPL Name -> REPL ()
forall (f :: * -> *) a. Functor f => f a -> f ()
void (REPL Name -> REPL ()) -> REPL Name -> REPL ()
forall a b. (a -> b) -> a -> b
$ TValue -> Expr -> REPL Name
bindItVariable TValue
t Expr
e

          AllSatResult [SatResult]
_ -> do
            String -> [String] -> REPL ()
forall a. HasCallStack => String -> [String] -> a
panic String
"REPL.Command" [String
"Unexpected AllSAtResult for ':safe' call"]

        Bool
seeStats <- REPL Bool
getUserShowProverStats
        Bool -> REPL () -> REPL ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when Bool
seeStats (Maybe String -> ProverStats -> REPL ()
showProverStats Maybe String
firstProver ProverStats
stats)


-- | Console-specific version of 'proveSat'. Prints output to the
-- console, and binds the @it@ variable to a record whose form depends
-- on the expression given. See ticket #66 for a discussion of this
-- design.
cmdProveSat :: Bool -> String -> (Int,Int) -> Maybe FilePath -> REPL ()
cmdProveSat :: Bool -> String -> (Int, Int) -> Maybe String -> REPL ()
cmdProveSat Bool
isSat String
"" (Int, Int)
_pos Maybe String
_fnm =
  do ([(Name, IfaceDecl)]
xs,NameDisp
disp) <- REPL ([(Name, IfaceDecl)], NameDisp)
getPropertyNames
     let nameStr :: a -> String
nameStr a
x = Doc -> String
forall a. Show a => a -> String
show (NameDisp -> Doc -> Doc
fixNameDisp NameDisp
disp (a -> Doc
forall a. PP a => a -> Doc
pp a
x))
     if [(Name, IfaceDecl)] -> Bool
forall a. [a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [(Name, IfaceDecl)]
xs
        then String -> REPL ()
rPutStrLn String
"There are no properties in scope."
        else [(Name, IfaceDecl)] -> ((Name, IfaceDecl) -> REPL ()) -> REPL ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
t a -> (a -> m b) -> m ()
forM_ [(Name, IfaceDecl)]
xs (((Name, IfaceDecl) -> REPL ()) -> REPL ())
-> ((Name, IfaceDecl) -> REPL ()) -> REPL ()
forall a b. (a -> b) -> a -> b
$ \(Name
x,IfaceDecl
d) ->
               do let str :: String
str = Name -> String
forall {a}. PP a => a -> String
nameStr Name
x
                  if Bool
isSat
                     then String -> REPL ()
rPutStr (String -> REPL ()) -> String -> REPL ()
forall a b. (a -> b) -> a -> b
$ String
":sat "   String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
str String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
"\n\t"
                     else String -> REPL ()
rPutStr (String -> REPL ()) -> String -> REPL ()
forall a b. (a -> b) -> a -> b
$ String
":prove " String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
str String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
"\n\t"
                  let texpr :: Expr
texpr = Name -> Expr
T.EVar Name
x
                  let schema :: Schema
schema = IfaceDecl -> Schema
M.ifDeclSig IfaceDecl
d
                  NameDisp
nd <- ModContext -> NameDisp
M.mctxNameDisp (ModContext -> NameDisp) -> REPL ModContext -> REPL NameDisp
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> REPL ModContext
getFocusedEnv
                  let doc :: Doc
doc = NameDisp -> Doc -> Doc
fixNameDisp NameDisp
nd (Expr -> Doc
forall a. PP a => a -> Doc
pp Expr
texpr)
                  Bool -> Range -> Doc -> Expr -> Schema -> REPL ()
proveSatExpr Bool
isSat (Name -> Range
M.nameLoc Name
x) Doc
doc Expr
texpr Schema
schema

cmdProveSat Bool
isSat String
str (Int, Int)
pos Maybe String
fnm = do
  Expr PName
pexpr <- String -> (Int, Int) -> Maybe String -> REPL (Expr PName)
replParseExpr String
str (Int, Int)
pos Maybe String
fnm
  NameDisp
nd <- ModContext -> NameDisp
M.mctxNameDisp (ModContext -> NameDisp) -> REPL ModContext -> REPL NameDisp
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> REPL ModContext
getFocusedEnv
  let doc :: Doc
doc = NameDisp -> Doc -> Doc
fixNameDisp NameDisp
nd (Int -> Expr PName -> Doc
forall a. PP a => Int -> a -> Doc
ppPrec Int
3 Expr PName
pexpr) -- function application has precedence 3
  (Expr Name
_,Expr
texpr,Schema
schema) <- Expr PName -> REPL (Expr Name, Expr, Schema)
replCheckExpr Expr PName
pexpr
  let rng :: Range
rng = Range -> Maybe Range -> Range
forall a. a -> Maybe a -> a
fromMaybe ((Int, Int) -> Maybe String -> Range
mkInteractiveRange (Int, Int)
pos Maybe String
fnm) (Expr PName -> Maybe Range
forall t. HasLoc t => t -> Maybe Range
getLoc Expr PName
pexpr)
  Bool -> Range -> Doc -> Expr -> Schema -> REPL ()
proveSatExpr Bool
isSat Range
rng Doc
doc Expr
texpr Schema
schema

proveSatExpr ::
  Bool ->
  Range ->
  Doc ->
  T.Expr ->
  T.Schema ->
  REPL ()
proveSatExpr :: Bool -> Range -> Doc -> Expr -> Schema -> REPL ()
proveSatExpr Bool
isSat Range
rng Doc
exprDoc Expr
texpr Schema
schema = do
  let cexStr :: String
cexStr | Bool
isSat = String
"satisfying assignment"
             | Bool
otherwise = String
"counterexample"
  QueryType
qtype <- if Bool
isSat then SatNum -> QueryType
SatQuery (SatNum -> QueryType) -> REPL SatNum -> REPL QueryType
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> REPL SatNum
getUserSatNum else QueryType -> REPL QueryType
forall a. a -> REPL a
forall (f :: * -> *) a. Applicative f => a -> f a
pure QueryType
ProveQuery
  String
proverName <- String -> REPL String
forall a. IsEnvVal a => String -> REPL a
getKnownUser String
"prover"
  String
fileName   <- String -> REPL String
forall a. IsEnvVal a => String -> REPL a
getKnownUser String
"smtFile"
  let mfile :: Maybe String
mfile = if String
fileName String -> String -> Bool
forall a. Eq a => a -> a -> Bool
== String
"-" then Maybe String
forall a. Maybe a
Nothing else String -> Maybe String
forall a. a -> Maybe a
Just String
fileName

  if String
proverName String -> [String] -> Bool
forall a. Eq a => a -> [a] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [String
"offline",String
"sbv-offline",String
"w4-offline"] then
     String -> QueryType -> Expr -> Schema -> Maybe String -> REPL ()
offlineProveSat String
proverName QueryType
qtype Expr
texpr Schema
schema Maybe String
mfile
  else
     do (Maybe String
firstProver,ProverResult
result,ProverStats
stats) <- REPL (Maybe String, ProverResult, ProverStats)
-> REPL (Maybe String, ProverResult, ProverStats)
forall a. REPL a -> REPL a
rethrowErrorCall (String
-> QueryType
-> Expr
-> Schema
-> Maybe String
-> REPL (Maybe String, ProverResult, ProverStats)
onlineProveSat String
proverName QueryType
qtype Expr
texpr Schema
schema Maybe String
mfile)
        case ProverResult
result of
          ProverResult
EmptyResult         ->
            String -> [String] -> REPL ()
forall a. HasCallStack => String -> [String] -> a
panic String
"REPL.Command" [ String
"got EmptyResult for online prover query" ]

          ProverError String
msg     -> String -> REPL ()
rPutStrLn String
msg

          ThmResult [TValue]
ts        -> do
            String -> REPL ()
rPutStrLn (if Bool
isSat then String
"Unsatisfiable" else String
"Q.E.D.")
            (TValue
t, Expr
e) <- String
-> Range
-> Bool
-> Either [TValue] [(TValue, Expr)]
-> REPL (TValue, Expr)
mkSolverResult String
cexStr Range
rng (Bool -> Bool
not Bool
isSat) ([TValue] -> Either [TValue] [(TValue, Expr)]
forall a b. a -> Either a b
Left [TValue]
ts)
            REPL Name -> REPL ()
forall (f :: * -> *) a. Functor f => f a -> f ()
void (REPL Name -> REPL ()) -> REPL Name -> REPL ()
forall a b. (a -> b) -> a -> b
$ TValue -> Expr -> REPL Name
bindItVariable TValue
t Expr
e

          CounterExample CounterExampleType
cexType SatResult
tevs -> do
            String -> REPL ()
rPutStrLn String
"Counterexample"
            let tes :: [(TValue, Expr)]
tes = ((TValue, Expr, Value) -> (TValue, Expr))
-> SatResult -> [(TValue, Expr)]
forall a b. (a -> b) -> [a] -> [b]
map ( \(TValue
t,Expr
e,Value
_) -> (TValue
t,Expr
e)) SatResult
tevs
                vs :: [Value]
vs  = ((TValue, Expr, Value) -> Value) -> SatResult -> [Value]
forall a b. (a -> b) -> [a] -> [b]
map ( \(TValue
_,Expr
_,Value
v) -> Value
v)     SatResult
tevs

            (TValue
t,Expr
e) <- String
-> Range
-> Bool
-> Either [TValue] [(TValue, Expr)]
-> REPL (TValue, Expr)
mkSolverResult String
cexStr Range
rng Bool
isSat ([(TValue, Expr)] -> Either [TValue] [(TValue, Expr)]
forall a b. b -> Either a b
Right [(TValue, Expr)]
tes)

            ~(EnvBool Bool
yes) <- String -> REPL EnvVal
getUser String
"showExamples"
            Bool -> REPL () -> REPL ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when Bool
yes (REPL () -> REPL ()) -> REPL () -> REPL ()
forall a b. (a -> b) -> a -> b
$ CounterExampleType -> Doc -> [Value] -> REPL ()
printCounterexample CounterExampleType
cexType Doc
exprDoc [Value]
vs

            -- if there's a safety violation, evalute the counterexample to
            -- find and print the actual concrete error
            case CounterExampleType
cexType of
              CounterExampleType
SafetyViolation -> Bool -> REPL () -> REPL ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when Bool
yes (REPL () -> REPL ()) -> REPL () -> REPL ()
forall a b. (a -> b) -> a -> b
$ Expr -> Schema -> [Value] -> REPL ()
printSafetyViolation Expr
texpr Schema
schema [Value]
vs
              CounterExampleType
_ -> () -> REPL ()
forall a. a -> REPL a
forall (m :: * -> *) a. Monad m => a -> m a
return ()

            REPL Name -> REPL ()
forall (f :: * -> *) a. Functor f => f a -> f ()
void (REPL Name -> REPL ()) -> REPL Name -> REPL ()
forall a b. (a -> b) -> a -> b
$ TValue -> Expr -> REPL Name
bindItVariable TValue
t Expr
e

          AllSatResult [SatResult]
tevss -> do
            String -> REPL ()
rPutStrLn String
"Satisfiable"
            let tess :: [[(TValue, Expr)]]
tess = (SatResult -> [(TValue, Expr)])
-> [SatResult] -> [[(TValue, Expr)]]
forall a b. (a -> b) -> [a] -> [b]
map (((TValue, Expr, Value) -> (TValue, Expr))
-> SatResult -> [(TValue, Expr)]
forall a b. (a -> b) -> [a] -> [b]
map (((TValue, Expr, Value) -> (TValue, Expr))
 -> SatResult -> [(TValue, Expr)])
-> ((TValue, Expr, Value) -> (TValue, Expr))
-> SatResult
-> [(TValue, Expr)]
forall a b. (a -> b) -> a -> b
$ \(TValue
t,Expr
e,Value
_) -> (TValue
t,Expr
e)) [SatResult]
tevss
                vss :: [[Value]]
vss  = (SatResult -> [Value]) -> [SatResult] -> [[Value]]
forall a b. (a -> b) -> [a] -> [b]
map (((TValue, Expr, Value) -> Value) -> SatResult -> [Value]
forall a b. (a -> b) -> [a] -> [b]
map (((TValue, Expr, Value) -> Value) -> SatResult -> [Value])
-> ((TValue, Expr, Value) -> Value) -> SatResult -> [Value]
forall a b. (a -> b) -> a -> b
$ \(TValue
_,Expr
_,Value
v) -> Value
v)     [SatResult]
tevss
            [(TValue, Expr)]
resultRecs <- ([(TValue, Expr)] -> REPL (TValue, Expr))
-> [[(TValue, Expr)]] -> REPL [(TValue, Expr)]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [b]
mapM (String
-> Range
-> Bool
-> Either [TValue] [(TValue, Expr)]
-> REPL (TValue, Expr)
mkSolverResult String
cexStr Range
rng Bool
isSat (Either [TValue] [(TValue, Expr)] -> REPL (TValue, Expr))
-> ([(TValue, Expr)] -> Either [TValue] [(TValue, Expr)])
-> [(TValue, Expr)]
-> REPL (TValue, Expr)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [(TValue, Expr)] -> Either [TValue] [(TValue, Expr)]
forall a b. b -> Either a b
Right) [[(TValue, Expr)]]
tess
            let collectTes :: [(a, b)] -> (a, [b])
collectTes [(a, b)]
tes = (a
t, [b]
es)
                  where
                    ([a]
ts, [b]
es) = [(a, b)] -> ([a], [b])
forall a b. [(a, b)] -> ([a], [b])
unzip [(a, b)]
tes
                    t :: a
t = case [a] -> [a]
forall a. Eq a => [a] -> [a]
nub [a]
ts of
                          [a
t'] -> a
t'
                          [a]
_ -> String -> [String] -> a
forall a. HasCallStack => String -> [String] -> a
panic String
"REPL.Command.onlineProveSat"
                                 [ String
"satisfying assignments with different types" ]
                (TValue
ty, [Expr]
exprs) =
                  case [(TValue, Expr)]
resultRecs of
                    [] -> String -> [String] -> (TValue, [Expr])
forall a. HasCallStack => String -> [String] -> a
panic String
"REPL.Command.onlineProveSat"
                            [ String
"no satisfying assignments after mkSolverResult" ]
                    [(TValue
t, Expr
e)] -> (TValue
t, [Expr
e])
                    [(TValue, Expr)]
_        -> [(TValue, Expr)] -> (TValue, [Expr])
forall {a} {b}. Eq a => [(a, b)] -> (a, [b])
collectTes [(TValue, Expr)]
resultRecs

            ~(EnvBool Bool
yes) <- String -> REPL EnvVal
getUser String
"showExamples"
            Bool -> REPL () -> REPL ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when Bool
yes (REPL () -> REPL ()) -> REPL () -> REPL ()
forall a b. (a -> b) -> a -> b
$ [[Value]] -> ([Value] -> REPL ()) -> REPL ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
t a -> (a -> m b) -> m ()
forM_ [[Value]]
vss (Doc -> [Value] -> REPL ()
printSatisfyingModel Doc
exprDoc)

            let numModels :: Int
numModels = [SatResult] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [SatResult]
tevss
            Bool -> REPL () -> REPL ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (Int
numModels Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
> Int
1) (String -> REPL ()
rPutStrLn (String
"Models found: " String -> ShowS
forall a. [a] -> [a] -> [a]
++ Int -> String
forall a. Show a => a -> String
show Int
numModels))

            case [Expr]
exprs of
              [Expr
e] -> REPL Name -> REPL ()
forall (f :: * -> *) a. Functor f => f a -> f ()
void (REPL Name -> REPL ()) -> REPL Name -> REPL ()
forall a b. (a -> b) -> a -> b
$ TValue -> Expr -> REPL Name
bindItVariable TValue
ty Expr
e
              [Expr]
_   -> TValue -> [Expr] -> REPL ()
bindItVariables TValue
ty [Expr]
exprs

        Bool
seeStats <- REPL Bool
getUserShowProverStats
        Bool -> REPL () -> REPL ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when Bool
seeStats (Maybe String -> ProverStats -> REPL ()
showProverStats Maybe String
firstProver ProverStats
stats)


printSafetyViolation :: T.Expr -> T.Schema -> [E.GenValue Concrete] -> REPL ()
printSafetyViolation :: Expr -> Schema -> [Value] -> REPL ()
printSafetyViolation Expr
texpr Schema
schema [Value]
vs =
    REPL () -> (REPLException -> REPL ()) -> REPL ()
forall a. REPL a -> (REPLException -> REPL a) -> REPL a
catch
      (do Value
fn <- Expr -> Schema -> REPL (Maybe (Value, Type))
replEvalCheckedExpr Expr
texpr Schema
schema REPL (Maybe (Value, Type))
-> (Maybe (Value, Type) -> REPL Value) -> REPL Value
forall a b. REPL a -> (a -> REPL b) -> REPL b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \Maybe (Value, Type)
mb_res -> case Maybe (Value, Type)
mb_res of 
            Just (Value
fn, Type
_) -> Value -> REPL Value
forall a. a -> REPL a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Value
fn
            Maybe (Value, Type)
Nothing -> REPLException -> REPL Value
forall a. REPLException -> REPL a
raise (Schema -> REPLException
EvalPolyError Schema
schema)
          Eval () -> REPL ()
forall a. Eval a -> REPL a
rEval (Value -> Eval ()
Value -> SEval Concrete ()
forall sym. Backend sym => GenValue sym -> SEval sym ()
E.forceValue (Value -> Eval ()) -> Eval Value -> Eval ()
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< (Value -> Value -> Eval Value) -> Value -> [Value] -> Eval Value
forall (t :: * -> *) (m :: * -> *) b a.
(Foldable t, Monad m) =>
(b -> a -> m b) -> b -> t a -> m b
foldM (\Value
f Value
v -> Concrete -> Value -> SEval Concrete Value -> SEval Concrete Value
forall sym.
Backend sym =>
sym
-> GenValue sym
-> SEval sym (GenValue sym)
-> SEval sym (GenValue sym)
E.fromVFun Concrete
Concrete Value
f (Value -> Eval Value
forall a. a -> Eval a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Value
v)) Value
fn [Value]
vs))
      (\case
          EvalError EvalErrorEx
eex -> String -> REPL ()
rPutStrLn (Doc -> String
forall a. Show a => a -> String
show (EvalErrorEx -> Doc
forall a. PP a => a -> Doc
pp EvalErrorEx
eex))
          REPLException
ex -> REPLException -> REPL ()
forall a. REPLException -> REPL a
raise REPLException
ex)

onlineProveSat ::
  String ->
  QueryType ->
  T.Expr ->
  T.Schema ->
  Maybe FilePath ->
  REPL (Maybe String,ProverResult,ProverStats)
onlineProveSat :: String
-> QueryType
-> Expr
-> Schema
-> Maybe String
-> REPL (Maybe String, ProverResult, ProverStats)
onlineProveSat String
proverName QueryType
qtype Expr
expr Schema
schema Maybe String
mfile = do
  Bool
verbose <- String -> REPL Bool
forall a. IsEnvVal a => String -> REPL a
getKnownUser String
"debug"
  Bool
modelValidate <- REPL Bool
getUserProverValidate
  Expr -> REPL ()
forall a. FreeVars a => a -> REPL ()
validEvalContext Expr
expr
  Schema -> REPL ()
forall a. FreeVars a => a -> REPL ()
validEvalContext Schema
schema
  [DeclGroup]
decls <- (DynamicEnv -> [DeclGroup]) -> REPL DynamicEnv -> REPL [DeclGroup]
forall a b. (a -> b) -> REPL a -> REPL b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap DynamicEnv -> [DeclGroup]
M.deDecls REPL DynamicEnv
getDynEnv
  IORef ProverStats
timing <- IO (IORef ProverStats) -> REPL (IORef ProverStats)
forall a. IO a -> REPL a
io (ProverStats -> IO (IORef ProverStats)
forall a. a -> IO (IORef a)
newIORef ProverStats
0)
  ~(EnvBool Bool
ignoreSafety) <- String -> REPL EnvVal
getUser String
"ignoreSafety"
  let cmd :: ProverCommand
cmd = ProverCommand {
          pcQueryType :: QueryType
pcQueryType    = QueryType
qtype
        , pcProverName :: String
pcProverName   = String
proverName
        , pcVerbose :: Bool
pcVerbose      = Bool
verbose
        , pcValidate :: Bool
pcValidate     = Bool
modelValidate
        , pcProverStats :: IORef ProverStats
pcProverStats  = IORef ProverStats
timing
        , pcExtraDecls :: [DeclGroup]
pcExtraDecls   = [DeclGroup]
decls
        , pcSmtFile :: Maybe String
pcSmtFile      = Maybe String
mfile
        , pcExpr :: Expr
pcExpr         = Expr
expr
        , pcSchema :: Schema
pcSchema       = Schema
schema
        , pcIgnoreSafety :: Bool
pcIgnoreSafety = Bool
ignoreSafety
        }
  (Maybe String
firstProver, ProverResult
res) <- REPL (Either SBVProverConfig W4ProverConfig)
getProverConfig REPL (Either SBVProverConfig W4ProverConfig)
-> (Either SBVProverConfig W4ProverConfig
    -> REPL (Maybe String, ProverResult))
-> REPL (Maybe String, ProverResult)
forall a b. REPL a -> (a -> REPL b) -> REPL b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case
       Left SBVProverConfig
sbvCfg -> ModuleCmd (Maybe String, ProverResult)
-> REPL (Maybe String, ProverResult)
forall a. ModuleCmd a -> REPL a
liftModuleCmd (ModuleCmd (Maybe String, ProverResult)
 -> REPL (Maybe String, ProverResult))
-> ModuleCmd (Maybe String, ProverResult)
-> REPL (Maybe String, ProverResult)
forall a b. (a -> b) -> a -> b
$ SBVProverConfig
-> ProverCommand -> ModuleCmd (Maybe String, ProverResult)
SBV.satProve SBVProverConfig
sbvCfg ProverCommand
cmd
       Right W4ProverConfig
w4Cfg ->
         do ~(EnvBool Bool
hashConsing) <- String -> REPL EnvVal
getUser String
"hashConsing"
            ~(EnvBool Bool
warnUninterp) <- String -> REPL EnvVal
getUser String
"warnUninterp"
            ModuleCmd (Maybe String, ProverResult)
-> REPL (Maybe String, ProverResult)
forall a. ModuleCmd a -> REPL a
liftModuleCmd (ModuleCmd (Maybe String, ProverResult)
 -> REPL (Maybe String, ProverResult))
-> ModuleCmd (Maybe String, ProverResult)
-> REPL (Maybe String, ProverResult)
forall a b. (a -> b) -> a -> b
$ W4ProverConfig
-> Bool
-> Bool
-> ProverCommand
-> ModuleCmd (Maybe String, ProverResult)
W4.satProve W4ProverConfig
w4Cfg Bool
hashConsing Bool
warnUninterp ProverCommand
cmd

  ProverStats
stas <- IO ProverStats -> REPL ProverStats
forall a. IO a -> REPL a
io (IORef ProverStats -> IO ProverStats
forall a. IORef a -> IO a
readIORef IORef ProverStats
timing)
  (Maybe String, ProverResult, ProverStats)
-> REPL (Maybe String, ProverResult, ProverStats)
forall a. a -> REPL a
forall (m :: * -> *) a. Monad m => a -> m a
return (Maybe String
firstProver,ProverResult
res,ProverStats
stas)

offlineProveSat :: String -> QueryType -> T.Expr -> T.Schema -> Maybe FilePath -> REPL ()
offlineProveSat :: String -> QueryType -> Expr -> Schema -> Maybe String -> REPL ()
offlineProveSat String
proverName QueryType
qtype Expr
expr Schema
schema Maybe String
mfile = do
  Bool
verbose <- String -> REPL Bool
forall a. IsEnvVal a => String -> REPL a
getKnownUser String
"debug"
  Bool
modelValidate <- REPL Bool
getUserProverValidate

  [DeclGroup]
decls <- (DynamicEnv -> [DeclGroup]) -> REPL DynamicEnv -> REPL [DeclGroup]
forall a b. (a -> b) -> REPL a -> REPL b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap DynamicEnv -> [DeclGroup]
M.deDecls REPL DynamicEnv
getDynEnv
  IORef ProverStats
timing <- IO (IORef ProverStats) -> REPL (IORef ProverStats)
forall a. IO a -> REPL a
io (ProverStats -> IO (IORef ProverStats)
forall a. a -> IO (IORef a)
newIORef ProverStats
0)
  ~(EnvBool Bool
ignoreSafety) <- String -> REPL EnvVal
getUser String
"ignoreSafety"
  let cmd :: ProverCommand
cmd = ProverCommand {
          pcQueryType :: QueryType
pcQueryType    = QueryType
qtype
        , pcProverName :: String
pcProverName   = String
proverName
        , pcVerbose :: Bool
pcVerbose      = Bool
verbose
        , pcValidate :: Bool
pcValidate     = Bool
modelValidate
        , pcProverStats :: IORef ProverStats
pcProverStats  = IORef ProverStats
timing
        , pcExtraDecls :: [DeclGroup]
pcExtraDecls   = [DeclGroup]
decls
        , pcSmtFile :: Maybe String
pcSmtFile      = Maybe String
mfile
        , pcExpr :: Expr
pcExpr         = Expr
expr
        , pcSchema :: Schema
pcSchema       = Schema
schema
        , pcIgnoreSafety :: Bool
pcIgnoreSafety = Bool
ignoreSafety
        }

  String -> IO ()
put <- REPL (String -> IO ())
getPutStr
  let putLn :: String -> IO ()
putLn String
x = String -> IO ()
put (String
x String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
"\n")
  let displayMsg :: IO ()
displayMsg =
        do let filename :: String
filename = String -> Maybe String -> String
forall a. a -> Maybe a -> a
fromMaybe String
"standard output" Maybe String
mfile
           let satWord :: String
satWord = case QueryType
qtype of
                           SatQuery SatNum
_  -> String
"satisfiability"
                           QueryType
ProveQuery  -> String
"validity"
                           QueryType
SafetyQuery -> String
"safety"
           String -> IO ()
putLn (String -> IO ()) -> String -> IO ()
forall a b. (a -> b) -> a -> b
$
               String
"Writing to SMT-Lib file " String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
filename String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
"..."
           String -> IO ()
putLn (String -> IO ()) -> String -> IO ()
forall a b. (a -> b) -> a -> b
$
             String
"To determine the " String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
satWord String -> ShowS
forall a. [a] -> [a] -> [a]
++
             String
" of the expression, use an external SMT solver."

  REPL (Either SBVProverConfig W4ProverConfig)
getProverConfig REPL (Either SBVProverConfig W4ProverConfig)
-> (Either SBVProverConfig W4ProverConfig -> REPL ()) -> REPL ()
forall a b. REPL a -> (a -> REPL b) -> REPL b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case
    Left SBVProverConfig
sbvCfg ->
      do Either String String
result <- ModuleCmd (Either String String) -> REPL (Either String String)
forall a. ModuleCmd a -> REPL a
liftModuleCmd (ModuleCmd (Either String String) -> REPL (Either String String))
-> ModuleCmd (Either String String) -> REPL (Either String String)
forall a b. (a -> b) -> a -> b
$ SBVProverConfig
-> ProverCommand -> ModuleCmd (Either String String)
SBV.satProveOffline SBVProverConfig
sbvCfg ProverCommand
cmd
         case Either String String
result of
           Left String
msg -> String -> REPL ()
rPutStrLn String
msg
           Right String
smtlib -> do
             IO () -> REPL ()
forall a. IO a -> REPL a
io (IO () -> REPL ()) -> IO () -> REPL ()
forall a b. (a -> b) -> a -> b
$ IO ()
displayMsg
             case Maybe String
mfile of
               Just String
path -> IO () -> REPL ()
forall a. IO a -> REPL a
io (IO () -> REPL ()) -> IO () -> REPL ()
forall a b. (a -> b) -> a -> b
$ String -> String -> IO ()
writeFile String
path String
smtlib
               Maybe String
Nothing -> String -> REPL ()
rPutStr String
smtlib

    Right W4ProverConfig
_w4Cfg ->
      do ~(EnvBool Bool
hashConsing) <- String -> REPL EnvVal
getUser String
"hashConsing"
         ~(EnvBool Bool
warnUninterp) <- String -> REPL EnvVal
getUser String
"warnUninterp"
         Maybe String
result <- ModuleCmd (Maybe String) -> REPL (Maybe String)
forall a. ModuleCmd a -> REPL a
liftModuleCmd (ModuleCmd (Maybe String) -> REPL (Maybe String))
-> ModuleCmd (Maybe String) -> REPL (Maybe String)
forall a b. (a -> b) -> a -> b
$ Bool
-> Bool
-> ProverCommand
-> ((Handle -> IO ()) -> IO ())
-> ModuleCmd (Maybe String)
W4.satProveOffline Bool
hashConsing Bool
warnUninterp ProverCommand
cmd (((Handle -> IO ()) -> IO ()) -> ModuleCmd (Maybe String))
-> ((Handle -> IO ()) -> IO ()) -> ModuleCmd (Maybe String)
forall a b. (a -> b) -> a -> b
$ \Handle -> IO ()
f ->
                     do IO ()
displayMsg
                        case Maybe String
mfile of
                          Just String
path ->
                            IO Handle -> (Handle -> IO ()) -> (Handle -> IO ()) -> IO ()
forall a b c. IO a -> (a -> IO b) -> (a -> IO c) -> IO c
X.bracket (String -> IOMode -> IO Handle
openFile String
path IOMode
WriteMode) Handle -> IO ()
hClose Handle -> IO ()
f
                          Maybe String
Nothing ->
                            String -> (Handle -> IO ()) -> IO ()
forall a. String -> (Handle -> IO a) -> IO a
withRWTempFile String
"smtOutput.tmp" ((Handle -> IO ()) -> IO ()) -> (Handle -> IO ()) -> IO ()
forall a b. (a -> b) -> a -> b
$ \Handle
h ->
                              do Handle -> IO ()
f Handle
h
                                 Handle -> SeekMode -> Integer -> IO ()
hSeek Handle
h SeekMode
AbsoluteSeek Integer
0
                                 Handle -> IO String
hGetContents Handle
h IO String -> (String -> IO ()) -> IO ()
forall a b. IO a -> (a -> IO b) -> IO b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= String -> IO ()
put

         case Maybe String
result of
           Just String
msg -> String -> REPL ()
rPutStrLn String
msg
           Maybe String
Nothing -> () -> REPL ()
forall a. a -> REPL a
forall (m :: * -> *) a. Monad m => a -> m a
return ()


rIdent :: M.Ident
rIdent :: Ident
rIdent  = String -> Ident
M.packIdent String
"result"

-- | Make a type/expression pair that is suitable for binding to @it@
-- after running @:sat@ or @:prove@
mkSolverResult ::
  String ->
  Range ->
  Bool ->
  Either [E.TValue] [(E.TValue, T.Expr)] ->
  REPL (E.TValue, T.Expr)
mkSolverResult :: String
-> Range
-> Bool
-> Either [TValue] [(TValue, Expr)]
-> REPL (TValue, Expr)
mkSolverResult String
thing Range
rng Bool
result Either [TValue] [(TValue, Expr)]
earg =
  do PrimMap
prims <- REPL PrimMap
getPrimMap
     let addError :: TValue -> (TValue, Expr)
addError TValue
t = (TValue
t, Range -> Expr -> Expr
T.ELocated Range
rng (PrimMap -> Type -> String -> Expr
T.eError PrimMap
prims (TValue -> Type
E.tValTy TValue
t) (String
"no " String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
thing String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
" available")))

         argF :: [((Ident, TValue), (Ident, Expr))]
argF = case Either [TValue] [(TValue, Expr)]
earg of
                  Left [TValue]
ts   -> [(TValue, Expr)] -> [((Ident, TValue), (Ident, Expr))]
forall {b} {b}. [(b, b)] -> [((Ident, b), (Ident, b))]
mkArgs ((TValue -> (TValue, Expr)) -> [TValue] -> [(TValue, Expr)]
forall a b. (a -> b) -> [a] -> [b]
map TValue -> (TValue, Expr)
addError [TValue]
ts)
                  Right [(TValue, Expr)]
tes -> [(TValue, Expr)] -> [((Ident, TValue), (Ident, Expr))]
forall {b} {b}. [(b, b)] -> [((Ident, b), (Ident, b))]
mkArgs [(TValue, Expr)]
tes

         eTrue :: Expr
eTrue  = PrimMap -> PrimIdent -> Expr
T.ePrim PrimMap
prims (Text -> PrimIdent
M.prelPrim Text
"True")
         eFalse :: Expr
eFalse = PrimMap -> PrimIdent -> Expr
T.ePrim PrimMap
prims (Text -> PrimIdent
M.prelPrim Text
"False")
         resultE :: Expr
resultE = if Bool
result then Expr
eTrue else Expr
eFalse

         rty :: TValue
rty = RecordMap Ident TValue -> TValue
E.TVRec ([(Ident, TValue)] -> RecordMap Ident TValue
forall a b. (Show a, Ord a) => [(a, b)] -> RecordMap a b
recordFromFields ([(Ident, TValue)] -> RecordMap Ident TValue)
-> [(Ident, TValue)] -> RecordMap Ident TValue
forall a b. (a -> b) -> a -> b
$ [(Ident
rIdent, TValue
E.TVBit)] [(Ident, TValue)] -> [(Ident, TValue)] -> [(Ident, TValue)]
forall a. [a] -> [a] -> [a]
++ (((Ident, TValue), (Ident, Expr)) -> (Ident, TValue))
-> [((Ident, TValue), (Ident, Expr))] -> [(Ident, TValue)]
forall a b. (a -> b) -> [a] -> [b]
map ((Ident, TValue), (Ident, Expr)) -> (Ident, TValue)
forall a b. (a, b) -> a
fst [((Ident, TValue), (Ident, Expr))]
argF)
         re :: Expr
re  = RecordMap Ident Expr -> Expr
T.ERec ([(Ident, Expr)] -> RecordMap Ident Expr
forall a b. (Show a, Ord a) => [(a, b)] -> RecordMap a b
recordFromFields ([(Ident, Expr)] -> RecordMap Ident Expr)
-> [(Ident, Expr)] -> RecordMap Ident Expr
forall a b. (a -> b) -> a -> b
$ [(Ident
rIdent, Expr
resultE)] [(Ident, Expr)] -> [(Ident, Expr)] -> [(Ident, Expr)]
forall a. [a] -> [a] -> [a]
++ (((Ident, TValue), (Ident, Expr)) -> (Ident, Expr))
-> [((Ident, TValue), (Ident, Expr))] -> [(Ident, Expr)]
forall a b. (a -> b) -> [a] -> [b]
map ((Ident, TValue), (Ident, Expr)) -> (Ident, Expr)
forall a b. (a, b) -> b
snd [((Ident, TValue), (Ident, Expr))]
argF)

     (TValue, Expr) -> REPL (TValue, Expr)
forall a. a -> REPL a
forall (m :: * -> *) a. Monad m => a -> m a
return (TValue
rty, Expr
re)
  where
  mkArgs :: [(b, b)] -> [((Ident, b), (Ident, b))]
mkArgs [(b, b)]
tes = (Int -> (b, b) -> ((Ident, b), (Ident, b)))
-> [Int] -> [(b, b)] -> [((Ident, b), (Ident, b))]
forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
zipWith Int -> (b, b) -> ((Ident, b), (Ident, b))
forall {p} {b} {b}.
Show p =>
p -> (b, b) -> ((Ident, b), (Ident, b))
mkArg [Int
1 :: Int ..] [(b, b)]
tes
    where
    mkArg :: p -> (b, b) -> ((Ident, b), (Ident, b))
mkArg p
n (b
t,b
e) =
      let argName :: Ident
argName = String -> Ident
M.packIdent (String
"arg" String -> ShowS
forall a. [a] -> [a] -> [a]
++ p -> String
forall a. Show a => a -> String
show p
n)
       in ((Ident
argName,b
t),(Ident
argName,b
e))

specializeCmd :: String -> (Int,Int) -> Maybe FilePath -> REPL ()
specializeCmd :: String -> (Int, Int) -> Maybe String -> REPL ()
specializeCmd String
str (Int, Int)
pos Maybe String
fnm = do
  Expr PName
parseExpr <- String -> (Int, Int) -> Maybe String -> REPL (Expr PName)
replParseExpr String
str (Int, Int)
pos Maybe String
fnm
  (Expr Name
_, Expr
expr, Schema
schema) <- Expr PName -> REPL (Expr Name, Expr, Schema)
replCheckExpr Expr PName
parseExpr
  Expr
spexpr <- Expr -> REPL Expr
replSpecExpr Expr
expr
  String -> REPL ()
rPutStrLn  String
"Expression type:"
  Doc -> REPL ()
forall a. Show a => a -> REPL ()
rPrint    (Doc -> REPL ()) -> Doc -> REPL ()
forall a b. (a -> b) -> a -> b
$ Schema -> Doc
forall a. PP a => a -> Doc
pp Schema
schema
  String -> REPL ()
rPutStrLn  String
"Original expression:"
  String -> REPL ()
rPutStrLn (String -> REPL ()) -> String -> REPL ()
forall a b. (a -> b) -> a -> b
$ Expr -> String
forall a. PP (WithNames a) => a -> String
dump Expr
expr
  String -> REPL ()
rPutStrLn  String
"Specialized expression:"
  String -> REPL ()
rPutStrLn (String -> REPL ()) -> String -> REPL ()
forall a b. (a -> b) -> a -> b
$ Expr -> String
forall a. PP (WithNames a) => a -> String
dump Expr
spexpr

refEvalCmd :: String -> (Int,Int) -> Maybe FilePath -> REPL ()
refEvalCmd :: String -> (Int, Int) -> Maybe String -> REPL ()
refEvalCmd String
str (Int, Int)
pos Maybe String
fnm = do
  Expr PName
parseExpr <- String -> (Int, Int) -> Maybe String -> REPL (Expr PName)
replParseExpr String
str (Int, Int)
pos Maybe String
fnm
  (Expr Name
_, Expr
expr, Schema
schema) <- Expr PName -> REPL (Expr Name, Expr, Schema)
replCheckExpr Expr PName
parseExpr
  Expr -> REPL ()
forall a. FreeVars a => a -> REPL ()
validEvalContext Expr
expr
  Schema -> REPL ()
forall a. FreeVars a => a -> REPL ()
validEvalContext Schema
schema
  E Value
val <- ModuleCmd (E Value) -> REPL (E Value)
forall a. ModuleCmd a -> REPL a
liftModuleCmd (IO (ModuleRes (E Value)) -> IO (ModuleRes (E Value))
forall a. IO a -> IO a
rethrowEvalError (IO (ModuleRes (E Value)) -> IO (ModuleRes (E Value)))
-> ModuleCmd (E Value) -> ModuleCmd (E Value)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Expr -> ModuleCmd (E Value)
R.evaluate Expr
expr)
  PPOpts
opts <- REPL PPOpts
getPPValOpts
  Doc -> REPL ()
forall a. Show a => a -> REPL ()
rPrint (Doc -> REPL ()) -> Doc -> REPL ()
forall a b. (a -> b) -> a -> b
$ PPOpts -> E Value -> Doc
R.ppEValue PPOpts
opts E Value
val

astOfCmd :: String -> (Int,Int) -> Maybe FilePath -> REPL ()
astOfCmd :: String -> (Int, Int) -> Maybe String -> REPL ()
astOfCmd String
str (Int, Int)
pos Maybe String
fnm = do
 Expr PName
expr <- String -> (Int, Int) -> Maybe String -> REPL (Expr PName)
replParseExpr String
str (Int, Int)
pos Maybe String
fnm
 (Expr Name
re,Expr
_,Schema
_) <- Expr PName -> REPL (Expr Name, Expr, Schema)
replCheckExpr (Expr PName -> Expr PName
forall t. NoPos t => t -> t
P.noPos Expr PName
expr)
 Expr Int -> REPL ()
forall a. Show a => a -> REPL ()
rPrint ((Name -> Int) -> Expr Name -> Expr Int
forall a b. (a -> b) -> Expr a -> Expr b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Name -> Int
M.nameUnique Expr Name
re)

allTerms :: REPL ()
allTerms :: REPL ()
allTerms = do
  ModuleEnv
me <- REPL ModuleEnv
getModuleEnv
  Doc Void -> REPL ()
forall a. Show a => a -> REPL ()
rPrint (Doc Void -> REPL ()) -> Doc Void -> REPL ()
forall a b. (a -> b) -> a -> b
$ [DeclGroup] -> Doc Void
forall t. ShowParseable t => t -> Doc Void
T.showParseable ([DeclGroup] -> Doc Void) -> [DeclGroup] -> Doc Void
forall a b. (a -> b) -> a -> b
$ (Module -> [DeclGroup]) -> [Module] -> [DeclGroup]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap Module -> [DeclGroup]
forall mname. ModuleG mname -> [DeclGroup]
T.mDecls ([Module] -> [DeclGroup]) -> [Module] -> [DeclGroup]
forall a b. (a -> b) -> a -> b
$ ModuleEnv -> [Module]
M.loadedModules ModuleEnv
me

typeOfCmd :: String -> (Int,Int) -> Maybe FilePath -> REPL ()
typeOfCmd :: String -> (Int, Int) -> Maybe String -> REPL ()
typeOfCmd String
str (Int, Int)
pos Maybe String
fnm = do

  Expr PName
expr         <- String -> (Int, Int) -> Maybe String -> REPL (Expr PName)
replParseExpr String
str (Int, Int)
pos Maybe String
fnm
  (Expr Name
_re,Expr
def,Schema
sig) <- Expr PName -> REPL (Expr Name, Expr, Schema)
replCheckExpr Expr PName
expr

  -- XXX need more warnings from the module system
  REPL () -> REPL ()
whenDebug (String -> REPL ()
rPutStrLn (Expr -> String
forall a. PP (WithNames a) => a -> String
dump Expr
def))
  NameDisp
fDisp <- ModContext -> NameDisp
M.mctxNameDisp (ModContext -> NameDisp) -> REPL ModContext -> REPL NameDisp
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> REPL ModContext
getFocusedEnv
  -- type annotation ':' has precedence 2
  Doc Void -> REPL ()
forall a. Show a => a -> REPL ()
rPrint (Doc Void -> REPL ()) -> Doc Void -> REPL ()
forall a b. (a -> b) -> a -> b
$ NameDisp -> Doc -> Doc Void
runDoc NameDisp
fDisp (Doc -> Doc Void) -> Doc -> Doc Void
forall a b. (a -> b) -> a -> b
$ Doc -> Doc
group (Doc -> Doc) -> Doc -> Doc
forall a b. (a -> b) -> a -> b
$ Doc -> Int -> Doc -> Doc
hang
    (Int -> Expr PName -> Doc
forall a. PP a => Int -> a -> Doc
ppPrec Int
2 Expr PName
expr Doc -> Doc -> Doc
<+> String -> Doc
text String
":") Int
2 (Schema -> Doc
forall a. PP a => a -> Doc
pp Schema
sig)

timeCmd :: String -> (Int, Int) -> Maybe FilePath -> REPL ()
timeCmd :: String -> (Int, Int) -> Maybe String -> REPL ()
timeCmd String
str (Int, Int)
pos Maybe String
fnm = do
  Int
period <- String -> REPL Int
forall a. IsEnvVal a => String -> REPL a
getKnownUser String
"timeMeasurementPeriod" :: REPL Int
  Bool
quiet <- String -> REPL Bool
forall a. IsEnvVal a => String -> REPL a
getKnownUser String
"timeQuiet"
  Bool -> REPL () -> REPL ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless Bool
quiet (REPL () -> REPL ()) -> REPL () -> REPL ()
forall a b. (a -> b) -> a -> b
$
    String -> REPL ()
rPutStrLn (String -> REPL ()) -> String -> REPL ()
forall a b. (a -> b) -> a -> b
$ String
"Measuring for " String -> ShowS
forall a. [a] -> [a] -> [a]
++ Int -> String
forall a. Show a => a -> String
show Int
period String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
" seconds"
  Expr PName
pExpr <- String -> (Int, Int) -> Maybe String -> REPL (Expr PName)
replParseExpr String
str (Int, Int)
pos Maybe String
fnm
  (Expr Name
_, Expr
def, Schema
sig) <- Expr PName -> REPL (Expr Name, Expr, Schema)
replCheckExpr Expr PName
pExpr
  Expr -> Schema -> REPL (Maybe ([(TParam, Type)], Expr))
replPrepareCheckedExpr Expr
def Schema
sig REPL (Maybe ([(TParam, Type)], Expr))
-> (Maybe ([(TParam, Type)], Expr) -> REPL ()) -> REPL ()
forall a b. REPL a -> (a -> REPL b) -> REPL b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case
    Maybe ([(TParam, Type)], Expr)
Nothing -> REPLException -> REPL ()
forall a. REPLException -> REPL a
raise (Schema -> REPLException
EvalPolyError Schema
sig)
    Just ([(TParam, Type)]
_, Expr
expr) -> do
      Bench.BenchmarkStats {Double
Int64
benchAvgTime :: Double
benchAvgCpuTime :: Double
benchAvgCycles :: Int64
benchAvgTime :: BenchmarkStats -> Double
benchAvgCpuTime :: BenchmarkStats -> Double
benchAvgCycles :: BenchmarkStats -> Int64
..} <- ModuleCmd BenchmarkStats -> REPL BenchmarkStats
forall a. ModuleCmd a -> REPL a
liftModuleCmd
        (IO (ModuleRes BenchmarkStats) -> IO (ModuleRes BenchmarkStats)
forall a. IO a -> IO a
rethrowEvalError (IO (ModuleRes BenchmarkStats) -> IO (ModuleRes BenchmarkStats))
-> ModuleCmd BenchmarkStats -> ModuleCmd BenchmarkStats
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Double -> Expr -> ModuleCmd BenchmarkStats
M.benchmarkExpr (Int -> Double
forall a b. (Integral a, Num b) => a -> b
fromIntegral Int
period) Expr
expr)
      Bool -> REPL () -> REPL ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless Bool
quiet (REPL () -> REPL ()) -> REPL () -> REPL ()
forall a b. (a -> b) -> a -> b
$
        String -> REPL ()
rPutStrLn (String -> REPL ()) -> String -> REPL ()
forall a b. (a -> b) -> a -> b
$ String
"Avg time: " String -> ShowS
forall a. [a] -> [a] -> [a]
++ Double -> String
Bench.secs Double
benchAvgTime
             String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
"    Avg CPU time: " String -> ShowS
forall a. [a] -> [a] -> [a]
++ Double -> String
Bench.secs Double
benchAvgCpuTime
             String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
"    Avg cycles: " String -> ShowS
forall a. [a] -> [a] -> [a]
++ Int64 -> String
forall a. Show a => a -> String
show Int64
benchAvgCycles
      let mkStatsRec :: b -> b -> b -> RecordMap a b
mkStatsRec b
time b
cpuTime b
cycles = [(a, b)] -> RecordMap a b
forall a b. (Show a, Ord a) => [(a, b)] -> RecordMap a b
recordFromFields
            [(a
"avgTime", b
time), (a
"avgCpuTime", b
cpuTime), (a
"avgCycles", b
cycles)]
          itType :: TValue
itType = RecordMap Ident TValue -> TValue
E.TVRec (RecordMap Ident TValue -> TValue)
-> RecordMap Ident TValue -> TValue
forall a b. (a -> b) -> a -> b
$ TValue -> TValue -> TValue -> RecordMap Ident TValue
forall {a} {b}.
(Show a, Ord a, IsString a) =>
b -> b -> b -> RecordMap a b
mkStatsRec TValue
E.tvFloat64 TValue
E.tvFloat64 TValue
E.TVInteger
          itVal :: Value
itVal = RecordMap Ident (SEval Concrete Value) -> Value
forall sym.
RecordMap Ident (SEval sym (GenValue sym)) -> GenValue sym
E.VRecord (RecordMap Ident (SEval Concrete Value) -> Value)
-> RecordMap Ident (SEval Concrete Value) -> Value
forall a b. (a -> b) -> a -> b
$ SEval Concrete Value
-> SEval Concrete Value
-> SEval Concrete Value
-> RecordMap Ident (SEval Concrete Value)
forall {a} {b}.
(Show a, Ord a, IsString a) =>
b -> b -> b -> RecordMap a b
mkStatsRec
            (Value -> SEval Concrete Value
forall a. a -> SEval Concrete a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Value -> SEval Concrete Value) -> Value -> SEval Concrete Value
forall a b. (a -> b) -> a -> b
$ SFloat Concrete -> Value
forall sym. SFloat sym -> GenValue sym
E.VFloat (SFloat Concrete -> Value) -> SFloat Concrete -> Value
forall a b. (a -> b) -> a -> b
$ Double -> BF
FP.floatFromDouble Double
benchAvgTime)
            (Value -> SEval Concrete Value
forall a. a -> SEval Concrete a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Value -> SEval Concrete Value) -> Value -> SEval Concrete Value
forall a b. (a -> b) -> a -> b
$ SFloat Concrete -> Value
forall sym. SFloat sym -> GenValue sym
E.VFloat (SFloat Concrete -> Value) -> SFloat Concrete -> Value
forall a b. (a -> b) -> a -> b
$ Double -> BF
FP.floatFromDouble Double
benchAvgCpuTime)
            (Value -> SEval Concrete Value
forall a. a -> SEval Concrete a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Value -> SEval Concrete Value) -> Value -> SEval Concrete Value
forall a b. (a -> b) -> a -> b
$ SInteger Concrete -> Value
forall sym. SInteger sym -> GenValue sym
E.VInteger (SInteger Concrete -> Value) -> SInteger Concrete -> Value
forall a b. (a -> b) -> a -> b
$ Int64 -> Integer
forall a. Integral a => a -> Integer
toInteger Int64
benchAvgCycles)
      TValue -> Value -> REPL ()
bindItVariableVal TValue
itType Value
itVal

readFileCmd :: FilePath -> REPL ()
readFileCmd :: String -> REPL ()
readFileCmd String
fp = do
  Maybe ByteString
bytes <- String
-> (SomeException -> REPL (Maybe ByteString))
-> REPL (Maybe ByteString)
replReadFile String
fp (\SomeException
err -> String -> REPL ()
rPutStrLn (SomeException -> String
forall a. Show a => a -> String
show SomeException
err) REPL () -> REPL (Maybe ByteString) -> REPL (Maybe ByteString)
forall a b. REPL a -> REPL b -> REPL b
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> Maybe ByteString -> REPL (Maybe ByteString)
forall a. a -> REPL a
forall (m :: * -> *) a. Monad m => a -> m a
return Maybe ByteString
forall a. Maybe a
Nothing)
  case Maybe ByteString
bytes of
    Maybe ByteString
Nothing -> () -> REPL ()
forall a. a -> REPL a
forall (m :: * -> *) a. Monad m => a -> m a
return ()
    Just ByteString
bs ->
      do PrimMap
pm <- REPL PrimMap
getPrimMap
         let val :: Integer
val = ByteString -> Integer
byteStringToInteger ByteString
bs
         let len :: Int
len = ByteString -> Int
BS.length ByteString
bs
         let split :: Expr
split = PrimMap -> PrimIdent -> Expr
T.ePrim PrimMap
pm (Text -> PrimIdent
M.prelPrim Text
"split")
         let number :: Expr
number = PrimMap -> PrimIdent -> Expr
T.ePrim PrimMap
pm (Text -> PrimIdent
M.prelPrim Text
"number")
         let f :: Expr
f = Expr -> Expr
T.EProofApp ((Expr -> Type -> Expr) -> Expr -> [Type] -> Expr
forall b a. (b -> a -> b) -> b -> [a] -> b
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl Expr -> Type -> Expr
T.ETApp Expr
split [Int -> Type
forall a. Integral a => a -> Type
T.tNum Int
len, Integer -> Type
forall a. Integral a => a -> Type
T.tNum (Integer
8::Integer), Type
T.tBit])
         let t :: Type
t = Type -> Type
T.tWord (Integer -> Type
forall a. Integral a => a -> Type
T.tNum (Int -> Integer
forall a. Integral a => a -> Integer
toInteger Int
len Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
* Integer
8))
         let x :: Expr
x = Expr -> Expr
T.EProofApp (Expr -> Type -> Expr
T.ETApp (Expr -> Type -> Expr
T.ETApp Expr
number (Integer -> Type
forall a. Integral a => a -> Type
T.tNum Integer
val)) Type
t)
         let expr :: Expr
expr = Expr -> Expr -> Expr
T.EApp Expr
f Expr
x
         REPL Name -> REPL ()
forall (f :: * -> *) a. Functor f => f a -> f ()
void (REPL Name -> REPL ()) -> REPL Name -> REPL ()
forall a b. (a -> b) -> a -> b
$ TValue -> Expr -> REPL Name
bindItVariable (Integer -> TValue -> TValue
E.TVSeq (Int -> Integer
forall a. Integral a => a -> Integer
toInteger Int
len) (Integer -> TValue -> TValue
E.TVSeq Integer
8 TValue
E.TVBit)) Expr
expr

-- | Convert a 'ByteString' (big-endian) of length @n@ to an 'Integer'
-- with @8*n@ bits. This function uses a balanced binary fold to
-- achieve /O(n log n)/ total memory allocation and run-time, in
-- contrast to the /O(n^2)/ that would be required by a naive
-- left-fold.
byteStringToInteger :: BS.ByteString -> Integer
-- byteStringToInteger = BS.foldl' (\a b -> a `shiftL` 8 .|. toInteger b) 0
byteStringToInteger :: ByteString -> Integer
byteStringToInteger ByteString
bs
  | Int
l Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
0 = Integer
0
  | Int
l Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
1 = Word8 -> Integer
forall a. Integral a => a -> Integer
toInteger (HasCallStack => ByteString -> Word8
ByteString -> Word8
BS.head ByteString
bs)
  | Bool
otherwise = Integer
x1 Integer -> Int -> Integer
forall a. Bits a => a -> Int -> a
`shiftL` (Int
l2 Int -> Int -> Int
forall a. Num a => a -> a -> a
* Int
8) Integer -> Integer -> Integer
forall a. Bits a => a -> a -> a
.|. Integer
x2
  where
    l :: Int
l = ByteString -> Int
BS.length ByteString
bs
    l1 :: Int
l1 = Int
l Int -> Int -> Int
forall a. Integral a => a -> a -> a
`div` Int
2
    l2 :: Int
l2 = Int
l Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
l1
    (ByteString
bs1, ByteString
bs2) = Int -> ByteString -> (ByteString, ByteString)
BS.splitAt Int
l1 ByteString
bs
    x1 :: Integer
x1 = ByteString -> Integer
byteStringToInteger ByteString
bs1
    x2 :: Integer
x2 = ByteString -> Integer
byteStringToInteger ByteString
bs2

writeFileCmd :: FilePath -> String -> (Int,Int) -> Maybe FilePath -> REPL ()
writeFileCmd :: String -> String -> (Int, Int) -> Maybe String -> REPL ()
writeFileCmd String
file String
str (Int, Int)
pos Maybe String
fnm = do
  Expr PName
expr         <- String -> (Int, Int) -> Maybe String -> REPL (Expr PName)
replParseExpr String
str (Int, Int)
pos Maybe String
fnm
  (Value
val,Type
ty)     <- Expr PName -> REPL (Value, Type)
replEvalExpr Expr PName
expr
  if Bool -> Bool
not (Type -> Bool
tIsByteSeq Type
ty)
   then Doc -> REPL ()
forall a. Show a => a -> REPL ()
rPrint (Doc -> REPL ()) -> Doc -> REPL ()
forall a b. (a -> b) -> a -> b
$  Doc
"Cannot write expression of types other than [n][8]."
              Doc -> Doc -> Doc
<+> Doc
"Type was: " Doc -> Doc -> Doc
<+> Type -> Doc
forall a. PP a => a -> Doc
pp Type
ty
   else String -> ByteString -> REPL ()
wf String
file (ByteString -> REPL ()) -> REPL ByteString -> REPL ()
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< Value -> REPL ByteString
serializeValue Value
val
 where
  wf :: String -> ByteString -> REPL ()
wf String
fp ByteString
bytes = String -> ByteString -> (SomeException -> REPL ()) -> REPL ()
replWriteFile String
fp ByteString
bytes (String -> REPL ()
rPutStrLn (String -> REPL ())
-> (SomeException -> String) -> SomeException -> REPL ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. SomeException -> String
forall a. Show a => a -> String
show)
  tIsByteSeq :: Type -> Bool
tIsByteSeq Type
x = Bool -> ((Type, Type) -> Bool) -> Maybe (Type, Type) -> Bool
forall b a. b -> (a -> b) -> Maybe a -> b
maybe Bool
False
                       (Type -> Bool
tIsByte (Type -> Bool) -> ((Type, Type) -> Type) -> (Type, Type) -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Type, Type) -> Type
forall a b. (a, b) -> b
snd)
                       (Type -> Maybe (Type, Type)
T.tIsSeq Type
x)
  tIsByte :: Type -> Bool
tIsByte    Type
x = Bool -> ((Type, Type) -> Bool) -> Maybe (Type, Type) -> Bool
forall b a. b -> (a -> b) -> Maybe a -> b
maybe Bool
False
                       (\(Type
n,Type
b) -> Type -> Bool
T.tIsBit Type
b Bool -> Bool -> Bool
&& Type -> Maybe Integer
T.tIsNum Type
n Maybe Integer -> Maybe Integer -> Bool
forall a. Eq a => a -> a -> Bool
== Integer -> Maybe Integer
forall a. a -> Maybe a
Just Integer
8)
                       (Type -> Maybe (Type, Type)
T.tIsSeq Type
x)
  serializeValue :: Value -> REPL ByteString
serializeValue (E.VSeq Integer
n SeqMap Concrete Value
vs) = do
    [BV]
ws <- Eval [BV] -> REPL [BV]
forall a. Eval a -> REPL a
rEval
            ((Eval Value -> Eval BV) -> [Eval Value] -> Eval [BV]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [b]
mapM (Eval Value -> (Value -> Eval BV) -> Eval BV
forall a b. Eval a -> (a -> Eval b) -> Eval b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= Concrete -> String -> Value -> SEval Concrete (SWord Concrete)
forall sym.
Backend sym =>
sym -> String -> GenValue sym -> SEval sym (SWord sym)
E.fromVWord Concrete
Concrete String
"serializeValue") ([Eval Value] -> Eval [BV]) -> [Eval Value] -> Eval [BV]
forall a b. (a -> b) -> a -> b
$ Integer -> SeqMap Concrete Value -> [SEval Concrete Value]
forall sym n a.
(Backend sym, Integral n) =>
n -> SeqMap sym a -> [SEval sym a]
E.enumerateSeqMap Integer
n SeqMap Concrete Value
vs)
    ByteString -> REPL ByteString
forall a. a -> REPL a
forall (m :: * -> *) a. Monad m => a -> m a
return (ByteString -> REPL ByteString) -> ByteString -> REPL ByteString
forall a b. (a -> b) -> a -> b
$ [Word8] -> ByteString
BS.pack ([Word8] -> ByteString) -> [Word8] -> ByteString
forall a b. (a -> b) -> a -> b
$ (BV -> Word8) -> [BV] -> [Word8]
forall a b. (a -> b) -> [a] -> [b]
map BV -> Word8
forall {b}. Num b => BV -> b
serializeByte [BV]
ws
  serializeValue Value
_             =
    String -> [String] -> REPL ByteString
forall a. HasCallStack => String -> [String] -> a
panic String
"Cryptol.REPL.Command.writeFileCmd"
      [String
"Impossible: Non-VSeq value of type [n][8]."]
  serializeByte :: BV -> b
serializeByte (Concrete.BV Integer
_ Integer
v) = Integer -> b
forall a b. (Integral a, Num b) => a -> b
fromIntegral (Integer
v Integer -> Integer -> Integer
forall a. Bits a => a -> a -> a
.&. Integer
0xFF)


rEval :: E.Eval a -> REPL a
rEval :: forall a. Eval a -> REPL a
rEval Eval a
m = IO a -> REPL a
forall a. IO a -> REPL a
io (CallStack -> Eval a -> IO a
forall a. CallStack -> Eval a -> IO a
E.runEval CallStack
forall a. Monoid a => a
mempty Eval a
m)

rEvalRethrow :: E.Eval a -> REPL a
rEvalRethrow :: forall a. Eval a -> REPL a
rEvalRethrow Eval a
m = IO a -> REPL a
forall a. IO a -> REPL a
io (IO a -> REPL a) -> IO a -> REPL a
forall a b. (a -> b) -> a -> b
$ IO a -> IO a
forall a. IO a -> IO a
rethrowEvalError (IO a -> IO a) -> IO a -> IO a
forall a b. (a -> b) -> a -> b
$ CallStack -> Eval a -> IO a
forall a. CallStack -> Eval a -> IO a
E.runEval CallStack
forall a. Monoid a => a
mempty Eval a
m

reloadCmd :: REPL ()
reloadCmd :: REPL ()
reloadCmd  = do
  Maybe LoadedModule
mb <- REPL (Maybe LoadedModule)
getLoadedMod
  case Maybe LoadedModule
mb of
    Just LoadedModule
lm  ->
      case LoadedModule -> ModulePath
lPath LoadedModule
lm of
        M.InFile String
f -> String -> REPL ()
loadCmd String
f
        ModulePath
_ -> () -> REPL ()
forall a. a -> REPL a
forall (m :: * -> *) a. Monad m => a -> m a
return ()
    Maybe LoadedModule
Nothing -> () -> REPL ()
forall a. a -> REPL a
forall (m :: * -> *) a. Monad m => a -> m a
return ()


editCmd :: String -> REPL ()
editCmd :: String -> REPL ()
editCmd String
path =
  do Maybe String
mbE <- REPL (Maybe String)
getEditPath
     Maybe LoadedModule
mbL <- REPL (Maybe LoadedModule)
getLoadedMod
     if Bool -> Bool
not (String -> Bool
forall a. [a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null String
path)
        then do Bool -> REPL () -> REPL ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (Maybe LoadedModule -> Bool
forall a. Maybe a -> Bool
isNothing Maybe LoadedModule
mbL)
                  (REPL () -> REPL ()) -> REPL () -> REPL ()
forall a b. (a -> b) -> a -> b
$ LoadedModule -> REPL ()
setLoadedMod LoadedModule { lName :: Maybe ModName
lName = Maybe ModName
forall a. Maybe a
Nothing
                                              , lPath :: ModulePath
lPath = String -> ModulePath
M.InFile String
path }
                String -> REPL ()
doEdit String
path
        else case [Maybe ModulePath] -> Maybe ModulePath
forall (t :: * -> *) (m :: * -> *) a.
(Foldable t, MonadPlus m) =>
t (m a) -> m a
msum [ String -> ModulePath
M.InFile (String -> ModulePath) -> Maybe String -> Maybe ModulePath
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Maybe String
mbE, LoadedModule -> ModulePath
lPath (LoadedModule -> ModulePath)
-> Maybe LoadedModule -> Maybe ModulePath
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Maybe LoadedModule
mbL ] of
               Maybe ModulePath
Nothing -> String -> REPL ()
rPutStrLn String
"No filed to edit."
               Just ModulePath
p  ->
                  case ModulePath
p of
                    M.InFile String
f   -> String -> REPL ()
doEdit String
f
                    M.InMem String
l ByteString
bs -> String -> ByteString -> (String -> REPL Bool) -> REPL Bool
forall a. String -> ByteString -> (String -> REPL a) -> REPL a
withROTempFile String
l ByteString
bs String -> REPL Bool
replEdit REPL Bool -> REPL () -> REPL ()
forall a b. REPL a -> REPL b -> REPL b
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> () -> REPL ()
forall a. a -> REPL a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ()
  where
  doEdit :: String -> REPL ()
doEdit String
p =
    do String -> REPL ()
setEditPath String
p
       Bool
_ <- String -> REPL Bool
replEdit String
p
       REPL ()
reloadCmd

withRWTempFile :: String -> (Handle -> IO a) -> IO a
withRWTempFile :: forall a. String -> (Handle -> IO a) -> IO a
withRWTempFile String
name Handle -> IO a
k =
  IO (String, Handle)
-> ((String, Handle) -> IO ())
-> ((String, Handle) -> IO a)
-> IO a
forall a b c. IO a -> (a -> IO b) -> (a -> IO c) -> IO c
X.bracket
    (do String
tmp <- IO String
getTemporaryDirectory
        let esc :: Char -> Char
esc Char
c = if Char -> Bool
isAscii Char
c Bool -> Bool -> Bool
&& Char -> Bool
isAlphaNum Char
c then Char
c else Char
'_'
        String -> String -> IO (String, Handle)
openTempFile String
tmp ((Char -> Char) -> ShowS
forall a b. (a -> b) -> [a] -> [b]
map Char -> Char
esc String
name))
    (\(String
nm,Handle
h) -> Handle -> IO ()
hClose Handle
h IO () -> IO () -> IO ()
forall a b. IO a -> IO b -> IO b
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> String -> IO ()
removeFile String
nm)
    (Handle -> IO a
k (Handle -> IO a)
-> ((String, Handle) -> Handle) -> (String, Handle) -> IO a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (String, Handle) -> Handle
forall a b. (a, b) -> b
snd)

withROTempFile :: String -> ByteString -> (FilePath -> REPL a) -> REPL a
withROTempFile :: forall a. String -> ByteString -> (String -> REPL a) -> REPL a
withROTempFile String
name ByteString
cnt String -> REPL a
k =
  do (String
path,Handle
h) <- REPL (String, Handle)
mkTmp
     do String -> Handle -> REPL ()
forall {m :: * -> *}. MonadIO m => String -> Handle -> m ()
mkFile String
path Handle
h
        String -> REPL a
k String
path
      REPL a -> REPL () -> REPL a
forall a b. REPL a -> REPL b -> REPL a
`finally` IO () -> REPL ()
forall a. IO a -> REPL a
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (do Handle -> IO ()
hClose Handle
h
                           String -> IO ()
removeFile String
path)
  where
  mkTmp :: REPL (String, Handle)
mkTmp =
    IO (String, Handle) -> REPL (String, Handle)
forall a. IO a -> REPL a
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (IO (String, Handle) -> REPL (String, Handle))
-> IO (String, Handle) -> REPL (String, Handle)
forall a b. (a -> b) -> a -> b
$
    do String
tmp <- IO String
getTemporaryDirectory
       let esc :: Char -> Char
esc Char
c = if Char -> Bool
isAscii Char
c Bool -> Bool -> Bool
&& Char -> Bool
isAlphaNum Char
c then Char
c else Char
'_'
       String -> String -> IO (String, Handle)
openTempFile String
tmp ((Char -> Char) -> ShowS
forall a b. (a -> b) -> [a] -> [b]
map Char -> Char
esc String
name String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
".cry")

  mkFile :: String -> Handle -> m ()
mkFile String
path Handle
h =
    IO () -> m ()
forall a. IO a -> m a
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (IO () -> m ()) -> IO () -> m ()
forall a b. (a -> b) -> a -> b
$
    do Handle -> ByteString -> IO ()
BS8.hPutStrLn Handle
h ByteString
cnt
       Handle -> IO ()
hFlush Handle
h
       String -> Permissions -> IO ()
setPermissions String
path (Bool -> Permissions -> Permissions
setOwnerReadable Bool
True Permissions
emptyPermissions)



moduleCmd :: String -> REPL ()
moduleCmd :: String -> REPL ()
moduleCmd String
modString
  | String -> Bool
forall a. [a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null String
modString = () -> REPL ()
forall a. a -> REPL a
forall (m :: * -> *) a. Monad m => a -> m a
return ()
  | Bool
otherwise      = do
    case String -> Maybe ModName
parseModName String
modString of
      Just ModName
m ->
        do ModulePath
mpath <- ModuleCmd ModulePath -> REPL ModulePath
forall a. ModuleCmd a -> REPL a
liftModuleCmd (ModName -> ModuleCmd ModulePath
M.findModule ModName
m)
           case ModulePath
mpath of
             M.InFile String
file ->
               do String -> REPL ()
setEditPath String
file
                  LoadedModule -> REPL ()
setLoadedMod LoadedModule { lName :: Maybe ModName
lName = ModName -> Maybe ModName
forall a. a -> Maybe a
Just ModName
m, lPath :: ModulePath
lPath = ModulePath
mpath }
                  ModuleCmd (ModulePath, TCTopEntity) -> REPL ()
loadHelper (String -> ModuleCmd (ModulePath, TCTopEntity)
M.loadModuleByPath String
file)
             M.InMem {} -> ModuleCmd (ModulePath, TCTopEntity) -> REPL ()
loadHelper (ModName -> ModuleCmd (ModulePath, TCTopEntity)
M.loadModuleByName ModName
m)
      Maybe ModName
Nothing -> String -> REPL ()
rPutStrLn String
"Invalid module name."

loadPrelude :: REPL ()
loadPrelude :: REPL ()
loadPrelude  = String -> REPL ()
moduleCmd (String -> REPL ()) -> String -> REPL ()
forall a b. (a -> b) -> a -> b
$ Doc -> String
forall a. Show a => a -> String
show (Doc -> String) -> Doc -> String
forall a b. (a -> b) -> a -> b
$ ModName -> Doc
forall a. PP a => a -> Doc
pp ModName
M.preludeName

loadCmd :: FilePath -> REPL ()
loadCmd :: String -> REPL ()
loadCmd String
path
  | String -> Bool
forall a. [a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null String
path = () -> REPL ()
forall a. a -> REPL a
forall (m :: * -> *) a. Monad m => a -> m a
return ()

  -- when `:load`, the edit and focused paths become the parameter
  | Bool
otherwise = do String -> REPL ()
setEditPath String
path
                   LoadedModule -> REPL ()
setLoadedMod LoadedModule { lName :: Maybe ModName
lName = Maybe ModName
forall a. Maybe a
Nothing
                                             , lPath :: ModulePath
lPath = String -> ModulePath
M.InFile String
path
                                             }
                   ModuleCmd (ModulePath, TCTopEntity) -> REPL ()
loadHelper (String -> ModuleCmd (ModulePath, TCTopEntity)
M.loadModuleByPath String
path)

loadHelper :: M.ModuleCmd (M.ModulePath,T.TCTopEntity) -> REPL ()
loadHelper :: ModuleCmd (ModulePath, TCTopEntity) -> REPL ()
loadHelper ModuleCmd (ModulePath, TCTopEntity)
how =
  do REPL ()
clearLoadedMod
     (ModulePath
path,TCTopEntity
ent) <- ModuleCmd (ModulePath, TCTopEntity)
-> REPL (ModulePath, TCTopEntity)
forall a. ModuleCmd a -> REPL a
liftModuleCmd ModuleCmd (ModulePath, TCTopEntity)
how

     REPL () -> REPL ()
whenDebug (String -> REPL ()
rPutStrLn (TCTopEntity -> String
forall a. PP (WithNames a) => a -> String
dump TCTopEntity
ent))
     LoadedModule -> REPL ()
setLoadedMod LoadedModule
        { lName :: Maybe ModName
lName = ModName -> Maybe ModName
forall a. a -> Maybe a
Just (TCTopEntity -> ModName
T.tcTopEntitytName TCTopEntity
ent)
        , lPath :: ModulePath
lPath = ModulePath
path
        }
     -- after a successful load, the current module becomes the edit target
     case ModulePath
path of
       M.InFile String
f -> String -> REPL ()
setEditPath String
f
       M.InMem {} -> REPL ()
clearEditPath
     DynamicEnv -> REPL ()
setDynEnv DynamicEnv
forall a. Monoid a => a
mempty

genHeaderCmd :: FilePath -> REPL ()
genHeaderCmd :: String -> REPL ()
genHeaderCmd String
path
  | String -> Bool
forall a. [a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null String
path = () -> REPL ()
forall a. a -> REPL a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ()
  | Bool
otherwise = do
    (ModulePath
mPath, TCTopEntity
m) <- ModuleCmd (ModulePath, TCTopEntity)
-> REPL (ModulePath, TCTopEntity)
forall a. ModuleCmd a -> REPL a
liftModuleCmd (ModuleCmd (ModulePath, TCTopEntity)
 -> REPL (ModulePath, TCTopEntity))
-> ModuleCmd (ModulePath, TCTopEntity)
-> REPL (ModulePath, TCTopEntity)
forall a b. (a -> b) -> a -> b
$ String -> ModuleCmd (ModulePath, TCTopEntity)
M.checkModuleByPath String
path
    let decls :: [(Name, FFIFunType)]
decls = case TCTopEntity
m of
                   T.TCTopModule Module
mo -> Module -> [(Name, FFIFunType)]
forall mname. ModuleG mname -> [(Name, FFIFunType)]
findForeignDecls Module
mo
                   T.TCTopSignature {} -> []
    if [(Name, FFIFunType)] -> Bool
forall a. [a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [(Name, FFIFunType)]
decls
      then String -> REPL ()
rPutStrLn (String -> REPL ()) -> String -> REPL ()
forall a b. (a -> b) -> a -> b
$ String
"No foreign declarations in " String -> ShowS
forall a. [a] -> [a] -> [a]
++ ModulePath -> String
forall {a}. PP a => a -> String
pretty ModulePath
mPath
      else do
        let header :: String
header = [(Name, FFIFunType)] -> String
generateForeignHeader [(Name, FFIFunType)]
decls
        case ModulePath
mPath of
          M.InFile String
p -> do
            let hPath :: String
hPath = String
p String -> ShowS
-<.> String
"h"
            String -> REPL ()
rPutStrLn (String -> REPL ()) -> String -> REPL ()
forall a b. (a -> b) -> a -> b
$ String
"Writing header to " String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
hPath
            String -> String -> (SomeException -> REPL ()) -> REPL ()
replWriteFileString String
hPath String
header (String -> REPL ()
rPutStrLn (String -> REPL ())
-> (SomeException -> String) -> SomeException -> REPL ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. SomeException -> String
forall a. Show a => a -> String
show)
          M.InMem String
_ ByteString
_ -> String -> REPL ()
rPutStrLn String
header

versionCmd :: REPL ()
versionCmd :: REPL ()
versionCmd = (String -> REPL ()) -> REPL ()
forall (m :: * -> *). Monad m => (String -> m ()) -> m ()
displayVersion String -> REPL ()
rPutStrLn

quitCmd :: REPL ()
quitCmd :: REPL ()
quitCmd  = REPL ()
stop

browseCmd :: String -> REPL ()
browseCmd :: String -> REPL ()
browseCmd String
input
  | String -> Bool
forall a. [a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null String
input =
    do ModContext
fe <- REPL ModContext
getFocusedEnv
       Doc Void -> REPL ()
forall a. Show a => a -> REPL ()
rPrint (BrowseHow -> ModContext -> Doc Void
browseModContext BrowseHow
BrowseInScope ModContext
fe)
  | Bool
otherwise =
    case String -> Maybe ModName
parseModName String
input of
      Maybe ModName
Nothing -> String -> REPL ()
rPutStrLn String
"Invalid module name"
      Just ModName
m ->
        do Maybe ModContext
mb <- ModName -> ModuleEnv -> Maybe ModContext
M.modContextOf ModName
m (ModuleEnv -> Maybe ModContext)
-> REPL ModuleEnv -> REPL (Maybe ModContext)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> REPL ModuleEnv
getModuleEnv
           case Maybe ModContext
mb of
             Maybe ModContext
Nothing -> String -> REPL ()
rPutStrLn (String
"Module " String -> ShowS
forall a. [a] -> [a] -> [a]
++ ShowS
forall a. Show a => a -> String
show String
input String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
" is not loaded")
             Just ModContext
fe -> Doc Void -> REPL ()
forall a. Show a => a -> REPL ()
rPrint (BrowseHow -> ModContext -> Doc Void
browseModContext BrowseHow
BrowseExported ModContext
fe)


setOptionCmd :: String -> REPL ()
setOptionCmd :: String -> REPL ()
setOptionCmd String
str
  | Just String
value <- Maybe String
mbValue = String -> String -> REPL ()
setUser String
key String
value
  | String -> Bool
forall a. [a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null String
key              = (OptionDescr -> REPL ()) -> [OptionDescr] -> REPL ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ (String -> REPL ()
describe (String -> REPL ())
-> (OptionDescr -> String) -> OptionDescr -> REPL ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. OptionDescr -> String
optName) (Trie OptionDescr -> [OptionDescr]
forall a. Trie a -> [a]
leaves Trie OptionDescr
userOptions)
  | Bool
otherwise             = String -> REPL ()
describe String
key
  where
  (String
before,String
after) = (Char -> Bool) -> String -> (String, String)
forall a. (a -> Bool) -> [a] -> ([a], [a])
break (Char -> Char -> Bool
forall a. Eq a => a -> a -> Bool
== Char
'=') String
str
  key :: String
key   = ShowS
trim String
before
  mbValue :: Maybe String
mbValue = case String
after of
              Char
_ : String
stuff -> String -> Maybe String
forall a. a -> Maybe a
Just (ShowS
trim String
stuff)
              String
_         -> Maybe String
forall a. Maybe a
Nothing

  describe :: String -> REPL ()
describe String
k = do
    Maybe EnvVal
ev <- String -> REPL (Maybe EnvVal)
tryGetUser String
k
    case Maybe EnvVal
ev of
      Just EnvVal
v  -> String -> REPL ()
rPutStrLn (String
k String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
" = " String -> ShowS
forall a. [a] -> [a] -> [a]
++ EnvVal -> String
showEnvVal EnvVal
v)
      Maybe EnvVal
Nothing -> do String -> REPL ()
rPutStrLn (String
"Unknown user option: `" String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
k String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
"`")
                    Bool -> REPL () -> REPL ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when ((Char -> Bool) -> String -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any Char -> Bool
isSpace String
k) (REPL () -> REPL ()) -> REPL () -> REPL ()
forall a b. (a -> b) -> a -> b
$ do
                      let (String
k1, String
k2) = (Char -> Bool) -> String -> (String, String)
forall a. (a -> Bool) -> [a] -> ([a], [a])
break Char -> Bool
isSpace String
k
                      String -> REPL ()
rPutStrLn (String
"Did you mean: `:set " String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
k1 String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
" =" String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
k2 String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
"`?")

showEnvVal :: EnvVal -> String
showEnvVal :: EnvVal -> String
showEnvVal EnvVal
ev =
  case EnvVal
ev of
    EnvString String
s   -> String
s
    EnvProg String
p [String]
as  -> String -> [String] -> String
forall a. [a] -> [[a]] -> [a]
intercalate String
" " (String
pString -> [String] -> [String]
forall a. a -> [a] -> [a]
:[String]
as)
    EnvNum Int
n      -> Int -> String
forall a. Show a => a -> String
show Int
n
    EnvBool Bool
True  -> String
"on"
    EnvBool Bool
False -> String
"off"

-- XXX at the moment, this can only look at declarations.
helpCmd :: String -> REPL ()
helpCmd :: String -> REPL ()
helpCmd String
cmd
  | String -> Bool
forall a. [a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null String
cmd  = (String -> REPL ()) -> [String] -> REPL ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ String -> REPL ()
rPutStrLn ([CommandDescr] -> [String]
genHelp [CommandDescr]
commandList)
  | String
cmd0 : [String]
args <- String -> [String]
words String
cmd, String
":" String -> String -> Bool
forall a. Eq a => [a] -> [a] -> Bool
`isPrefixOf` String
cmd0 =
    case String -> [CommandDescr]
findCommandExact String
cmd0 of
      []  -> REPL CommandExitCode -> REPL ()
forall (f :: * -> *) a. Functor f => f a -> f ()
void (REPL CommandExitCode -> REPL ())
-> REPL CommandExitCode -> REPL ()
forall a b. (a -> b) -> a -> b
$ Int -> Maybe String -> Command -> REPL CommandExitCode
runCommand Int
1 Maybe String
forall a. Maybe a
Nothing (String -> Command
Unknown String
cmd0)
      [CommandDescr
c] -> CommandDescr -> [String] -> REPL ()
showCmdHelp CommandDescr
c [String]
args
      [CommandDescr]
cs  -> REPL CommandExitCode -> REPL ()
forall (f :: * -> *) a. Functor f => f a -> f ()
void (REPL CommandExitCode -> REPL ())
-> REPL CommandExitCode -> REPL ()
forall a b. (a -> b) -> a -> b
$ Int -> Maybe String -> Command -> REPL CommandExitCode
runCommand Int
1 Maybe String
forall a. Maybe a
Nothing (String -> [String] -> Command
Ambiguous String
cmd0 ((CommandDescr -> [String]) -> [CommandDescr] -> [String]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap CommandDescr -> [String]
cNames [CommandDescr]
cs))
  | Bool
otherwise =
    case String -> Maybe PName
parseHelpName String
cmd of
      Just PName
qname -> PName -> REPL ()
helpForNamed PName
qname
      Maybe PName
Nothing    -> String -> REPL ()
rPutStrLn (String
"Unable to parse name: " String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
cmd)

  where
  showCmdHelp :: CommandDescr -> [String] -> REPL ()
showCmdHelp CommandDescr
c [String
arg] | String
":set" String -> [String] -> Bool
forall a. Eq a => a -> [a] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` CommandDescr -> [String]
cNames CommandDescr
c = String -> REPL ()
showOptionHelp String
arg
  showCmdHelp CommandDescr
c [String]
_args =
    do String -> REPL ()
rPutStrLn (String
"\n    " String -> ShowS
forall a. [a] -> [a] -> [a]
++ String -> [String] -> String
forall a. [a] -> [[a]] -> [a]
intercalate String
", " (CommandDescr -> [String]
cNames CommandDescr
c) String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
" " String -> ShowS
forall a. [a] -> [a] -> [a]
++ String -> [String] -> String
forall a. [a] -> [[a]] -> [a]
intercalate String
" " (CommandDescr -> [String]
cArgs CommandDescr
c))
       String -> REPL ()
rPutStrLn String
""
       String -> REPL ()
rPutStrLn (CommandDescr -> String
cHelp CommandDescr
c)
       String -> REPL ()
rPutStrLn String
""
       Bool -> REPL () -> REPL ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (Bool -> Bool
not (String -> Bool
forall a. [a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null (CommandDescr -> String
cLongHelp CommandDescr
c))) (REPL () -> REPL ()) -> REPL () -> REPL ()
forall a b. (a -> b) -> a -> b
$ do
         String -> REPL ()
rPutStrLn (CommandDescr -> String
cLongHelp CommandDescr
c)
         String -> REPL ()
rPutStrLn String
""

  showOptionHelp :: String -> REPL ()
showOptionHelp String
arg =
    case String -> Trie OptionDescr -> [OptionDescr]
forall a. String -> Trie a -> [a]
lookupTrieExact String
arg Trie OptionDescr
userOptions of
      [OptionDescr
opt] ->
        do let k :: String
k = OptionDescr -> String
optName OptionDescr
opt
           Maybe EnvVal
ev <- String -> REPL (Maybe EnvVal)
tryGetUser String
k
           String -> REPL ()
rPutStrLn (String -> REPL ()) -> String -> REPL ()
forall a b. (a -> b) -> a -> b
$ String
"\n    " String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
k String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
" = " String -> ShowS
forall a. [a] -> [a] -> [a]
++ String -> (EnvVal -> String) -> Maybe EnvVal -> String
forall b a. b -> (a -> b) -> Maybe a -> b
maybe String
"???" EnvVal -> String
showEnvVal Maybe EnvVal
ev
           String -> REPL ()
rPutStrLn String
""
           String -> REPL ()
rPutStrLn (String
"Default value: " String -> ShowS
forall a. [a] -> [a] -> [a]
++ EnvVal -> String
showEnvVal (OptionDescr -> EnvVal
optDefault OptionDescr
opt))
           String -> REPL ()
rPutStrLn String
""
           String -> REPL ()
rPutStrLn (OptionDescr -> String
optHelp OptionDescr
opt)
           String -> REPL ()
rPutStrLn String
""
      [] -> String -> REPL ()
rPutStrLn (String
"Unknown setting name `" String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
arg String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
"`")
      [OptionDescr]
_  -> String -> REPL ()
rPutStrLn (String
"Ambiguous setting name `" String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
arg String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
"`")


runShellCmd :: String -> REPL ()
runShellCmd :: String -> REPL ()
runShellCmd String
cmd
  = IO () -> REPL ()
forall a. IO a -> REPL a
io (IO () -> REPL ()) -> IO () -> REPL ()
forall a b. (a -> b) -> a -> b
$ do ProcessHandle
h <- String -> IO ProcessHandle
Process.runCommand String
cmd
            ExitCode
_ <- ProcessHandle -> IO ExitCode
waitForProcess ProcessHandle
h
            () -> IO ()
forall a. a -> IO a
forall (m :: * -> *) a. Monad m => a -> m a
return ()

cdCmd :: FilePath -> REPL ()
cdCmd :: String -> REPL ()
cdCmd String
f | String -> Bool
forall a. [a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null String
f = String -> REPL ()
rPutStrLn (String -> REPL ()) -> String -> REPL ()
forall a b. (a -> b) -> a -> b
$ String
"[error] :cd requires a path argument"
        | Bool
otherwise = do
  Bool
exists <- IO Bool -> REPL Bool
forall a. IO a -> REPL a
io (IO Bool -> REPL Bool) -> IO Bool -> REPL Bool
forall a b. (a -> b) -> a -> b
$ String -> IO Bool
doesDirectoryExist String
f
  if Bool
exists
    then IO () -> REPL ()
forall a. IO a -> REPL a
io (IO () -> REPL ()) -> IO () -> REPL ()
forall a b. (a -> b) -> a -> b
$ String -> IO ()
setCurrentDirectory String
f
    else REPLException -> REPL ()
forall a. REPLException -> REPL a
raise (REPLException -> REPL ()) -> REPLException -> REPL ()
forall a b. (a -> b) -> a -> b
$ String -> REPLException
DirectoryNotFound String
f

-- C-c Handlings ---------------------------------------------------------------

-- XXX this should probably do something a bit more specific.
handleCtrlC :: a -> REPL a
handleCtrlC :: forall a. a -> REPL a
handleCtrlC a
a = do String -> REPL ()
rPutStrLn String
"Ctrl-C"
                   REPL ()
resetTCSolver
                   a -> REPL a
forall a. a -> REPL a
forall (m :: * -> *) a. Monad m => a -> m a
return a
a

-- Utilities -------------------------------------------------------------------

-- | Lift a parsing action into the REPL monad.
replParse :: (String -> Either ParseError a) -> String -> REPL a
replParse :: forall a. (String -> Either ParseError a) -> String -> REPL a
replParse String -> Either ParseError a
parse String
str = case String -> Either ParseError a
parse String
str of
  Right a
a -> a -> REPL a
forall a. a -> REPL a
forall (m :: * -> *) a. Monad m => a -> m a
return a
a
  Left ParseError
e  -> REPLException -> REPL a
forall a. REPLException -> REPL a
raise (ParseError -> REPLException
ParseError ParseError
e)

replParseInput :: String -> Int -> Maybe FilePath -> REPL (P.ReplInput P.PName)
replParseInput :: String -> Int -> Maybe String -> REPL (ReplInput PName)
replParseInput String
str Int
lineNum Maybe String
fnm = (String -> Either ParseError (ReplInput PName))
-> String -> REPL (ReplInput PName)
forall a. (String -> Either ParseError a) -> String -> REPL a
replParse (Config -> Text -> Either ParseError (ReplInput PName)
parseReplWith Config
cfg (Text -> Either ParseError (ReplInput PName))
-> (String -> Text)
-> String
-> Either ParseError (ReplInput PName)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. String -> Text
T.pack) String
str
  where
  cfg :: Config
cfg = case Maybe String
fnm of
          Maybe String
Nothing -> Config
interactiveConfig{ cfgStart = Position lineNum 1 }
          Just String
f  -> Config
defaultConfig
                     { cfgSource = f
                     , cfgStart  = Position lineNum 1
                     }

replParseExpr :: String -> (Int,Int) -> Maybe FilePath -> REPL (P.Expr P.PName)
replParseExpr :: String -> (Int, Int) -> Maybe String -> REPL (Expr PName)
replParseExpr String
str (Int
l,Int
c) Maybe String
fnm = (String -> Either ParseError (Expr PName))
-> String -> REPL (Expr PName)
forall a. (String -> Either ParseError a) -> String -> REPL a
replParse (Config -> Text -> Either ParseError (Expr PName)
parseExprWith Config
cfg(Text -> Either ParseError (Expr PName))
-> (String -> Text) -> String -> Either ParseError (Expr PName)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. String -> Text
T.pack) String
str
  where
  cfg :: Config
cfg = case Maybe String
fnm of
          Maybe String
Nothing -> Config
interactiveConfig{ cfgStart = Position l c }
          Just String
f  -> Config
defaultConfig
                     { cfgSource = f
                     , cfgStart  = Position l c
                     }

mkInteractiveRange :: (Int,Int) -> Maybe FilePath -> Range
mkInteractiveRange :: (Int, Int) -> Maybe String -> Range
mkInteractiveRange (Int
l,Int
c) Maybe String
mb = Position -> Position -> String -> Range
Range Position
p Position
p String
src
  where
  p :: Position
p = Int -> Int -> Position
Position Int
l Int
c
  src :: String
src = case Maybe String
mb of
          Maybe String
Nothing -> String
"<interactive>"
          Just String
b  -> String
b

interactiveConfig :: Config
interactiveConfig :: Config
interactiveConfig = Config
defaultConfig { cfgSource = "<interactive>" }

getPrimMap :: REPL M.PrimMap
getPrimMap :: REPL PrimMap
getPrimMap  = ModuleCmd PrimMap -> REPL PrimMap
forall a. ModuleCmd a -> REPL a
liftModuleCmd ModuleCmd PrimMap
M.getPrimMap

liftModuleCmd :: M.ModuleCmd a -> REPL a
liftModuleCmd :: forall a. ModuleCmd a -> REPL a
liftModuleCmd ModuleCmd a
cmd =
  do IO EvalOpts
evo <- REPL (IO EvalOpts)
getEvalOptsAction
     ModuleEnv
env <- REPL ModuleEnv
getModuleEnv
     Bool
callStacks <- REPL Bool
getCallStacks
     Solver
tcSolver <- REPL Solver
getTCSolver
     let minp :: ModuleInput IO
minp =
             M.ModuleInput
                { minpCallStacks :: Bool
minpCallStacks = Bool
callStacks
                , minpEvalOpts :: IO EvalOpts
minpEvalOpts   = IO EvalOpts
evo
                , minpByteReader :: String -> IO ByteString
minpByteReader = String -> IO ByteString
BS.readFile
                , minpModuleEnv :: ModuleEnv
minpModuleEnv  = ModuleEnv
env
                , minpTCSolver :: Solver
minpTCSolver   = Solver
tcSolver
                }
     ModuleRes a -> REPL a
forall a. ModuleRes a -> REPL a
moduleCmdResult (ModuleRes a -> REPL a) -> REPL (ModuleRes a) -> REPL a
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< IO (ModuleRes a) -> REPL (ModuleRes a)
forall a. IO a -> REPL a
io (ModuleCmd a
cmd ModuleInput IO
minp)

-- TODO: add filter for my exhaustie prop guards warning here

moduleCmdResult :: M.ModuleRes a -> REPL a
moduleCmdResult :: forall a. ModuleRes a -> REPL a
moduleCmdResult (Either ModuleError (a, ModuleEnv)
res,[ModuleWarning]
ws0) = do
  Bool
warnDefaulting  <- String -> REPL Bool
forall a. IsEnvVal a => String -> REPL a
getKnownUser String
"warnDefaulting"
  Bool
warnShadowing   <- String -> REPL Bool
forall a. IsEnvVal a => String -> REPL a
getKnownUser String
"warnShadowing"
  Bool
warnPrefixAssoc <- String -> REPL Bool
forall a. IsEnvVal a => String -> REPL a
getKnownUser String
"warnPrefixAssoc"
  Bool
warnNonExhConGrds <- String -> REPL Bool
forall a. IsEnvVal a => String -> REPL a
getKnownUser String
"warnNonExhaustiveConstraintGuards"
  -- XXX: let's generalize this pattern
  let isShadowWarn :: RenamerWarning -> Bool
isShadowWarn (M.SymbolShadowed {}) = Bool
True
      isShadowWarn RenamerWarning
_                     = Bool
False

      isPrefixAssocWarn :: RenamerWarning -> Bool
isPrefixAssocWarn (M.PrefixAssocChanged {}) = Bool
True
      isPrefixAssocWarn RenamerWarning
_                         = Bool
False

      filterRenamer :: Bool
-> (RenamerWarning -> Bool) -> ModuleWarning -> Maybe ModuleWarning
filterRenamer Bool
True RenamerWarning -> Bool
_ ModuleWarning
w = ModuleWarning -> Maybe ModuleWarning
forall a. a -> Maybe a
Just ModuleWarning
w
      filterRenamer Bool
_ RenamerWarning -> Bool
check (M.RenamerWarnings [RenamerWarning]
xs) =
        case (RenamerWarning -> Bool) -> [RenamerWarning] -> [RenamerWarning]
forall a. (a -> Bool) -> [a] -> [a]
filter (Bool -> Bool
not (Bool -> Bool)
-> (RenamerWarning -> Bool) -> RenamerWarning -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. RenamerWarning -> Bool
check) [RenamerWarning]
xs of
          [] -> Maybe ModuleWarning
forall a. Maybe a
Nothing
          [RenamerWarning]
ys -> ModuleWarning -> Maybe ModuleWarning
forall a. a -> Maybe a
Just ([RenamerWarning] -> ModuleWarning
M.RenamerWarnings [RenamerWarning]
ys)
      filterRenamer Bool
_ RenamerWarning -> Bool
_ ModuleWarning
w = ModuleWarning -> Maybe ModuleWarning
forall a. a -> Maybe a
Just ModuleWarning
w

      -- ignore certain warnings during typechecking
      filterTypecheck :: M.ModuleWarning -> Maybe M.ModuleWarning
      filterTypecheck :: ModuleWarning -> Maybe ModuleWarning
filterTypecheck (M.TypeCheckWarnings NameMap
nameMap [(Range, Warning)]
xs) = 
        case ((Range, Warning) -> Bool)
-> [(Range, Warning)] -> [(Range, Warning)]
forall a. (a -> Bool) -> [a] -> [a]
filter (Warning -> Bool
allow (Warning -> Bool)
-> ((Range, Warning) -> Warning) -> (Range, Warning) -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Range, Warning) -> Warning
forall a b. (a, b) -> b
snd) [(Range, Warning)]
xs of 
          [] -> Maybe ModuleWarning
forall a. Maybe a
Nothing
          [(Range, Warning)]
ys -> ModuleWarning -> Maybe ModuleWarning
forall a. a -> Maybe a
Just (NameMap -> [(Range, Warning)] -> ModuleWarning
M.TypeCheckWarnings NameMap
nameMap [(Range, Warning)]
ys)
          where
            allow :: T.Warning -> Bool 
            allow :: Warning -> Bool
allow = \case
              T.DefaultingTo TVarInfo
_ Type
_ | Bool -> Bool
not Bool
warnDefaulting -> Bool
False
              T.NonExhaustivePropGuards Name
_ | Bool -> Bool
not Bool
warnNonExhConGrds -> Bool
False
              Warning
_ -> Bool
True
      filterTypecheck ModuleWarning
w = ModuleWarning -> Maybe ModuleWarning
forall a. a -> Maybe a
Just ModuleWarning
w

  let ws :: [ModuleWarning]
ws = (ModuleWarning -> Maybe ModuleWarning)
-> [ModuleWarning] -> [ModuleWarning]
forall a b. (a -> Maybe b) -> [a] -> [b]
mapMaybe (Bool
-> (RenamerWarning -> Bool) -> ModuleWarning -> Maybe ModuleWarning
filterRenamer Bool
warnShadowing RenamerWarning -> Bool
isShadowWarn)
         ([ModuleWarning] -> [ModuleWarning])
-> ([ModuleWarning] -> [ModuleWarning])
-> [ModuleWarning]
-> [ModuleWarning]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (ModuleWarning -> Maybe ModuleWarning)
-> [ModuleWarning] -> [ModuleWarning]
forall a b. (a -> Maybe b) -> [a] -> [b]
mapMaybe (Bool
-> (RenamerWarning -> Bool) -> ModuleWarning -> Maybe ModuleWarning
filterRenamer Bool
warnPrefixAssoc RenamerWarning -> Bool
isPrefixAssocWarn)
         ([ModuleWarning] -> [ModuleWarning])
-> ([ModuleWarning] -> [ModuleWarning])
-> [ModuleWarning]
-> [ModuleWarning]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (ModuleWarning -> Maybe ModuleWarning)
-> [ModuleWarning] -> [ModuleWarning]
forall a b. (a -> Maybe b) -> [a] -> [b]
mapMaybe ModuleWarning -> Maybe ModuleWarning
filterTypecheck
         ([ModuleWarning] -> [ModuleWarning])
-> [ModuleWarning] -> [ModuleWarning]
forall a b. (a -> b) -> a -> b
$ [ModuleWarning]
ws0
  NameDisp
names <- ModContext -> NameDisp
M.mctxNameDisp (ModContext -> NameDisp) -> REPL ModContext -> REPL NameDisp
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> REPL ModContext
getFocusedEnv
  (ModuleWarning -> REPL ()) -> [ModuleWarning] -> REPL ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ (Doc Void -> REPL ()
forall a. Show a => a -> REPL ()
rPrint (Doc Void -> REPL ())
-> (ModuleWarning -> Doc Void) -> ModuleWarning -> REPL ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. NameDisp -> Doc -> Doc Void
runDoc NameDisp
names (Doc -> Doc Void)
-> (ModuleWarning -> Doc) -> ModuleWarning -> Doc Void
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ModuleWarning -> Doc
forall a. PP a => a -> Doc
pp) [ModuleWarning]
ws
  case Either ModuleError (a, ModuleEnv)
res of
    Right (a
a,ModuleEnv
me') -> ModuleEnv -> REPL ()
setModuleEnv ModuleEnv
me' REPL () -> REPL a -> REPL a
forall a b. REPL a -> REPL b -> REPL b
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> a -> REPL a
forall a. a -> REPL a
forall (m :: * -> *) a. Monad m => a -> m a
return a
a
    Left ModuleError
err      ->
      do ModuleError
e <- case ModuleError
err of
                M.ErrorInFile (M.InFile String
file) ModuleError
e ->
                  -- on error, the file with the error becomes the edit
                  -- target.  Note, however, that the focused module is not
                  -- changed.
                  do String -> REPL ()
setEditPath String
file
                     ModuleError -> REPL ModuleError
forall a. a -> REPL a
forall (m :: * -> *) a. Monad m => a -> m a
return ModuleError
e
                ModuleError
_ -> ModuleError -> REPL ModuleError
forall a. a -> REPL a
forall (m :: * -> *) a. Monad m => a -> m a
return ModuleError
err
         REPLException -> REPL a
forall a. REPLException -> REPL a
raise (NameDisp -> ModuleError -> REPLException
ModuleSystemError NameDisp
names ModuleError
e)


replCheckExpr :: P.Expr P.PName -> REPL (P.Expr M.Name,T.Expr,T.Schema)
replCheckExpr :: Expr PName -> REPL (Expr Name, Expr, Schema)
replCheckExpr Expr PName
e = ModuleCmd (Expr Name, Expr, Schema)
-> REPL (Expr Name, Expr, Schema)
forall a. ModuleCmd a -> REPL a
liftModuleCmd (ModuleCmd (Expr Name, Expr, Schema)
 -> REPL (Expr Name, Expr, Schema))
-> ModuleCmd (Expr Name, Expr, Schema)
-> REPL (Expr Name, Expr, Schema)
forall a b. (a -> b) -> a -> b
$ Expr PName -> ModuleCmd (Expr Name, Expr, Schema)
M.checkExpr Expr PName
e

-- | Check declarations as though they were defined at the top-level.
replCheckDecls :: [P.Decl P.PName] -> REPL [T.DeclGroup]
replCheckDecls :: [Decl PName] -> REPL [DeclGroup]
replCheckDecls [Decl PName]
ds = do

  -- check the decls
  [Decl PName]
npds        <- ModuleCmd [Decl PName] -> REPL [Decl PName]
forall a. ModuleCmd a -> REPL a
liftModuleCmd ([Decl PName] -> ModuleCmd [Decl PName]
forall a. RemovePatterns a => a -> ModuleCmd a
M.noPat [Decl PName]
ds)

  let mkTop :: Decl name -> TopDecl name
mkTop Decl name
d = TopLevel (Decl name) -> TopDecl name
forall name. TopLevel (Decl name) -> TopDecl name
P.Decl P.TopLevel { tlExport :: ExportType
P.tlExport = ExportType
P.Public
                                  , tlDoc :: Maybe (Located Text)
P.tlDoc    = Maybe (Located Text)
forall a. Maybe a
Nothing
                                  , tlValue :: Decl name
P.tlValue  = Decl name
d }
  (NamingEnv
names,[DeclGroup]
ds',Map Name TySyn
tyMap) <- ModuleCmd (NamingEnv, [DeclGroup], Map Name TySyn)
-> REPL (NamingEnv, [DeclGroup], Map Name TySyn)
forall a. ModuleCmd a -> REPL a
liftModuleCmd ([TopDecl PName]
-> ModuleCmd (NamingEnv, [DeclGroup], Map Name TySyn)
M.checkDecls ((Decl PName -> TopDecl PName) -> [Decl PName] -> [TopDecl PName]
forall a b. (a -> b) -> [a] -> [b]
map Decl PName -> TopDecl PName
forall {name}. Decl name -> TopDecl name
mkTop [Decl PName]
npds))

  -- extend the naming env and type synonym maps
  DynamicEnv
denv        <- REPL DynamicEnv
getDynEnv
  DynamicEnv -> REPL ()
setDynEnv DynamicEnv
denv { M.deNames  = names `M.shadowing` M.deNames denv
                 , M.deTySyns = tyMap <> M.deTySyns denv
                 }
  [DeclGroup] -> REPL [DeclGroup]
forall a. a -> REPL a
forall (m :: * -> *) a. Monad m => a -> m a
return [DeclGroup]
ds'

replSpecExpr :: T.Expr -> REPL T.Expr
replSpecExpr :: Expr -> REPL Expr
replSpecExpr Expr
e = ModuleCmd Expr -> REPL Expr
forall a. ModuleCmd a -> REPL a
liftModuleCmd (ModuleCmd Expr -> REPL Expr) -> ModuleCmd Expr -> REPL Expr
forall a b. (a -> b) -> a -> b
$ Expr -> ModuleCmd Expr
S.specialize Expr
e

replEvalExpr :: P.Expr P.PName -> REPL (Concrete.Value, T.Type)
replEvalExpr :: Expr PName -> REPL (Value, Type)
replEvalExpr Expr PName
expr =
  do (Expr Name
_,Expr
def,Schema
sig) <- Expr PName -> REPL (Expr Name, Expr, Schema)
replCheckExpr Expr PName
expr
     Expr -> Schema -> REPL (Maybe (Value, Type))
replEvalCheckedExpr Expr
def Schema
sig REPL (Maybe (Value, Type))
-> (Maybe (Value, Type) -> REPL (Value, Type))
-> REPL (Value, Type)
forall a b. REPL a -> (a -> REPL b) -> REPL b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case
       Just (Value, Type)
res -> (Value, Type) -> REPL (Value, Type)
forall a. a -> REPL a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Value, Type)
res
       Maybe (Value, Type)
Nothing -> REPLException -> REPL (Value, Type)
forall a. REPLException -> REPL a
raise (Schema -> REPLException
EvalPolyError Schema
sig)

replEvalCheckedExpr :: T.Expr -> T.Schema -> REPL (Maybe (Concrete.Value, T.Type))
replEvalCheckedExpr :: Expr -> Schema -> REPL (Maybe (Value, Type))
replEvalCheckedExpr Expr
def Schema
sig =
  Expr -> Schema -> REPL (Maybe ([(TParam, Type)], Expr))
replPrepareCheckedExpr Expr
def Schema
sig REPL (Maybe ([(TParam, Type)], Expr))
-> (Maybe ([(TParam, Type)], Expr) -> REPL (Maybe (Value, Type)))
-> REPL (Maybe (Value, Type))
forall a b. REPL a -> (a -> REPL b) -> REPL b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>=
    (([(TParam, Type)], Expr) -> REPL (Value, Type))
-> Maybe ([(TParam, Type)], Expr) -> REPL (Maybe (Value, Type))
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> Maybe a -> f (Maybe b)
traverse \([(TParam, Type)]
tys, Expr
def1) -> do
      let su :: Subst
su = [(TParam, Type)] -> Subst
T.listParamSubst [(TParam, Type)]
tys
      let ty :: Type
ty = Subst -> Type -> Type
forall t. TVars t => Subst -> t -> t
T.apSubst Subst
su (Schema -> Type
T.sType Schema
sig)
      REPL () -> REPL ()
whenDebug (String -> REPL ()
rPutStrLn (Expr -> String
forall a. PP (WithNames a) => a -> String
dump Expr
def1))

      TypeEnv
tenv <- GenEvalEnv Concrete -> TypeEnv
forall sym. GenEvalEnv sym -> TypeEnv
E.envTypes (GenEvalEnv Concrete -> TypeEnv)
-> (DynamicEnv -> GenEvalEnv Concrete) -> DynamicEnv -> TypeEnv
forall b c a. (b -> c) -> (a -> b) -> a -> c
. DynamicEnv -> GenEvalEnv Concrete
M.deEnv (DynamicEnv -> TypeEnv) -> REPL DynamicEnv -> REPL TypeEnv
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> REPL DynamicEnv
getDynEnv
      let tyv :: TValue
tyv = TypeEnv -> Type -> TValue
E.evalValType TypeEnv
tenv Type
ty

      -- add "it" to the namespace via a new declaration
      Name
itVar <- TValue -> Expr -> REPL Name
bindItVariable TValue
tyv Expr
def1

      let itExpr :: Expr
itExpr = case Expr -> Maybe Range
forall t. HasLoc t => t -> Maybe Range
getLoc Expr
def of
                      Maybe Range
Nothing  -> Name -> Expr
T.EVar Name
itVar
                      Just Range
rng -> Range -> Expr -> Expr
T.ELocated Range
rng (Name -> Expr
T.EVar Name
itVar)

      -- evaluate the it variable
      Value
val <- ModuleCmd Value -> REPL Value
forall a. ModuleCmd a -> REPL a
liftModuleCmd (IO (ModuleRes Value) -> IO (ModuleRes Value)
forall a. IO a -> IO a
rethrowEvalError (IO (ModuleRes Value) -> IO (ModuleRes Value))
-> ModuleCmd Value -> ModuleCmd Value
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Expr -> ModuleCmd Value
M.evalExpr Expr
itExpr)
      (Value, Type) -> REPL (Value, Type)
forall a. a -> REPL a
forall (m :: * -> *) a. Monad m => a -> m a
return (Value
val,Type
ty)

-- | Check that we are in a valid evaluation context and apply defaulting.
replPrepareCheckedExpr :: T.Expr -> T.Schema ->
  REPL (Maybe ([(T.TParam, T.Type)], T.Expr))
replPrepareCheckedExpr :: Expr -> Schema -> REPL (Maybe ([(TParam, Type)], Expr))
replPrepareCheckedExpr Expr
def Schema
sig = do
  Expr -> REPL ()
forall a. FreeVars a => a -> REPL ()
validEvalContext Expr
def
  Schema -> REPL ()
forall a. FreeVars a => a -> REPL ()
validEvalContext Schema
sig

  Solver
s <- REPL Solver
getTCSolver
  Maybe ([(TParam, Type)], Expr)
mbDef <- IO (Maybe ([(TParam, Type)], Expr))
-> REPL (Maybe ([(TParam, Type)], Expr))
forall a. IO a -> REPL a
io (Solver -> Expr -> Schema -> IO (Maybe ([(TParam, Type)], Expr))
defaultReplExpr Solver
s Expr
def Schema
sig)

  case Maybe ([(TParam, Type)], Expr)
mbDef of
    Maybe ([(TParam, Type)], Expr)
Nothing -> Maybe ([(TParam, Type)], Expr)
-> REPL (Maybe ([(TParam, Type)], Expr))
forall a. a -> REPL a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Maybe ([(TParam, Type)], Expr)
forall a. Maybe a
Nothing
    Just ([(TParam, Type)]
tys, Expr
def1) -> do
      [(TParam, Type)] -> REPL ()
forall {a}. PP a => [(TParam, a)] -> REPL ()
warnDefaults [(TParam, Type)]
tys
      Maybe ([(TParam, Type)], Expr)
-> REPL (Maybe ([(TParam, Type)], Expr))
forall a. a -> REPL a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Maybe ([(TParam, Type)], Expr)
 -> REPL (Maybe ([(TParam, Type)], Expr)))
-> Maybe ([(TParam, Type)], Expr)
-> REPL (Maybe ([(TParam, Type)], Expr))
forall a b. (a -> b) -> a -> b
$ ([(TParam, Type)], Expr) -> Maybe ([(TParam, Type)], Expr)
forall a. a -> Maybe a
Just ([(TParam, Type)]
tys, Expr
def1)
  where
  warnDefaults :: [(TParam, a)] -> REPL ()
warnDefaults [(TParam, a)]
ts =
    case [(TParam, a)]
ts of
      [] -> () -> REPL ()
forall a. a -> REPL a
forall (m :: * -> *) a. Monad m => a -> m a
return ()
      [(TParam, a)]
_  -> do String -> REPL ()
rPutStrLn String
"Showing a specific instance of polymorphic result:"
               ((TParam, a) -> REPL ()) -> [(TParam, a)] -> REPL ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ (TParam, a) -> REPL ()
forall {a}. PP a => (TParam, a) -> REPL ()
warnDefault [(TParam, a)]
ts

  warnDefault :: (TParam, a) -> REPL ()
warnDefault (TParam
x,a
t) =
    Doc -> REPL ()
forall a. Show a => a -> REPL ()
rPrint (Doc
"  *" Doc -> Doc -> Doc
<+> Int -> Doc -> Doc
nest Int
2  (Doc
"Using" Doc -> Doc -> Doc
<+> Doc -> Doc
quotes (a -> Doc
forall a. PP a => a -> Doc
pp a
t) Doc -> Doc -> Doc
<+> Doc
"for" Doc -> Doc -> Doc
<+>
                                TypeSource -> Doc
forall a. PP a => a -> Doc
pp (TVarInfo -> TypeSource
T.tvarDesc (TParam -> TVarInfo
T.tpInfo TParam
x))))

itIdent :: M.Ident
itIdent :: Ident
itIdent  = String -> Ident
M.packIdent String
"it"

replWriteFile :: FilePath -> BS.ByteString -> (X.SomeException -> REPL ()) -> REPL ()
replWriteFile :: String -> ByteString -> (SomeException -> REPL ()) -> REPL ()
replWriteFile = (String -> ByteString -> IO ())
-> String -> ByteString -> (SomeException -> REPL ()) -> REPL ()
forall a.
(String -> a -> IO ())
-> String -> a -> (SomeException -> REPL ()) -> REPL ()
replWriteFileWith String -> ByteString -> IO ()
BS.writeFile

replWriteFileString :: FilePath -> String -> (X.SomeException -> REPL ()) -> REPL ()
replWriteFileString :: String -> String -> (SomeException -> REPL ()) -> REPL ()
replWriteFileString = (String -> String -> IO ())
-> String -> String -> (SomeException -> REPL ()) -> REPL ()
forall a.
(String -> a -> IO ())
-> String -> a -> (SomeException -> REPL ()) -> REPL ()
replWriteFileWith String -> String -> IO ()
writeFile

replWriteFileWith :: (FilePath -> a -> IO ()) -> FilePath -> a ->
  (X.SomeException -> REPL ()) -> REPL ()
replWriteFileWith :: forall a.
(String -> a -> IO ())
-> String -> a -> (SomeException -> REPL ()) -> REPL ()
replWriteFileWith String -> a -> IO ()
write String
fp a
contents SomeException -> REPL ()
handler =
 do Maybe SomeException
x <- IO (Maybe SomeException) -> REPL (Maybe SomeException)
forall a. IO a -> REPL a
io (IO (Maybe SomeException) -> REPL (Maybe SomeException))
-> IO (Maybe SomeException) -> REPL (Maybe SomeException)
forall a b. (a -> b) -> a -> b
$ IO (Maybe SomeException)
-> (SomeException -> IO (Maybe SomeException))
-> IO (Maybe SomeException)
forall e a. Exception e => IO a -> (e -> IO a) -> IO a
X.catch (String -> a -> IO ()
write String
fp a
contents IO () -> IO (Maybe SomeException) -> IO (Maybe SomeException)
forall a b. IO a -> IO b -> IO b
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> Maybe SomeException -> IO (Maybe SomeException)
forall a. a -> IO a
forall (m :: * -> *) a. Monad m => a -> m a
return Maybe SomeException
forall a. Maybe a
Nothing) (Maybe SomeException -> IO (Maybe SomeException)
forall a. a -> IO a
forall (m :: * -> *) a. Monad m => a -> m a
return (Maybe SomeException -> IO (Maybe SomeException))
-> (SomeException -> Maybe SomeException)
-> SomeException
-> IO (Maybe SomeException)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. SomeException -> Maybe SomeException
forall a. a -> Maybe a
Just)
    REPL ()
-> (SomeException -> REPL ()) -> Maybe SomeException -> REPL ()
forall b a. b -> (a -> b) -> Maybe a -> b
maybe (() -> REPL ()
forall a. a -> REPL a
forall (m :: * -> *) a. Monad m => a -> m a
return ()) SomeException -> REPL ()
handler Maybe SomeException
x

replReadFile :: FilePath -> (X.SomeException -> REPL (Maybe BS.ByteString)) -> REPL (Maybe BS.ByteString)
replReadFile :: String
-> (SomeException -> REPL (Maybe ByteString))
-> REPL (Maybe ByteString)
replReadFile String
fp SomeException -> REPL (Maybe ByteString)
handler =
 do Either SomeException ByteString
x <- IO (Either SomeException ByteString)
-> REPL (Either SomeException ByteString)
forall a. IO a -> REPL a
io (IO (Either SomeException ByteString)
 -> REPL (Either SomeException ByteString))
-> IO (Either SomeException ByteString)
-> REPL (Either SomeException ByteString)
forall a b. (a -> b) -> a -> b
$ IO (Either SomeException ByteString)
-> (SomeException -> IO (Either SomeException ByteString))
-> IO (Either SomeException ByteString)
forall e a. Exception e => IO a -> (e -> IO a) -> IO a
X.catch (ByteString -> Either SomeException ByteString
forall a b. b -> Either a b
Right (ByteString -> Either SomeException ByteString)
-> IO ByteString -> IO (Either SomeException ByteString)
forall a b. (a -> b) -> IO a -> IO b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
`fmap` String -> IO ByteString
BS.readFile String
fp) (\SomeException
e -> Either SomeException ByteString
-> IO (Either SomeException ByteString)
forall a. a -> IO a
forall (m :: * -> *) a. Monad m => a -> m a
return (Either SomeException ByteString
 -> IO (Either SomeException ByteString))
-> Either SomeException ByteString
-> IO (Either SomeException ByteString)
forall a b. (a -> b) -> a -> b
$ SomeException -> Either SomeException ByteString
forall a b. a -> Either a b
Left SomeException
e)
    (SomeException -> REPL (Maybe ByteString))
-> (ByteString -> REPL (Maybe ByteString))
-> Either SomeException ByteString
-> REPL (Maybe ByteString)
forall a c b. (a -> c) -> (b -> c) -> Either a b -> c
either SomeException -> REPL (Maybe ByteString)
handler (Maybe ByteString -> REPL (Maybe ByteString)
forall a. a -> REPL a
forall (m :: * -> *) a. Monad m => a -> m a
return (Maybe ByteString -> REPL (Maybe ByteString))
-> (ByteString -> Maybe ByteString)
-> ByteString
-> REPL (Maybe ByteString)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ByteString -> Maybe ByteString
forall a. a -> Maybe a
Just) Either SomeException ByteString
x

-- | Creates a fresh binding of "it" to the expression given, and adds
-- it to the current dynamic environment.  The fresh name generated
-- is returned.
bindItVariable :: E.TValue -> T.Expr -> REPL T.Name
bindItVariable :: TValue -> Expr -> REPL Name
bindItVariable TValue
ty Expr
expr = do
  Name
freshIt <- Ident -> NameSource -> REPL Name
freshName Ident
itIdent NameSource
M.UserName
  let schema :: Schema
schema = T.Forall { sVars :: [TParam]
T.sVars  = []
                        , sProps :: [Type]
T.sProps = []
                        , sType :: Type
T.sType  = TValue -> Type
E.tValTy TValue
ty
                        }
      decl :: Decl
decl = T.Decl { dName :: Name
T.dName       = Name
freshIt
                    , dSignature :: Schema
T.dSignature  = Schema
schema
                    , dDefinition :: DeclDef
T.dDefinition = Expr -> DeclDef
T.DExpr Expr
expr
                    , dPragmas :: [Pragma]
T.dPragmas    = []
                    , dInfix :: Bool
T.dInfix      = Bool
False
                    , dFixity :: Maybe Fixity
T.dFixity     = Maybe Fixity
forall a. Maybe a
Nothing
                    , dDoc :: Maybe Text
T.dDoc        = Maybe Text
forall a. Maybe a
Nothing
                    }
  ModuleCmd () -> REPL ()
forall a. ModuleCmd a -> REPL a
liftModuleCmd ([DeclGroup] -> ModuleCmd ()
M.evalDecls [Decl -> DeclGroup
T.NonRecursive Decl
decl])
  DynamicEnv
denv <- REPL DynamicEnv
getDynEnv
  let nenv' :: NamingEnv
nenv' = Namespace -> PName -> Name -> NamingEnv
M.singletonNS Namespace
M.NSValue (Ident -> PName
P.UnQual Ident
itIdent) Name
freshIt
                           NamingEnv -> NamingEnv -> NamingEnv
`M.shadowing` DynamicEnv -> NamingEnv
M.deNames DynamicEnv
denv
  DynamicEnv -> REPL ()
setDynEnv (DynamicEnv -> REPL ()) -> DynamicEnv -> REPL ()
forall a b. (a -> b) -> a -> b
$ DynamicEnv
denv { M.deNames = nenv' }
  Name -> REPL Name
forall a. a -> REPL a
forall (m :: * -> *) a. Monad m => a -> m a
return Name
freshIt


-- | Extend the dynamic environment with a fresh binding for "it",
-- as defined by the given value.  If we cannot determine the definition
-- of the value, then we don't bind `it`.
bindItVariableVal :: E.TValue -> Concrete.Value -> REPL ()
bindItVariableVal :: TValue -> Value -> REPL ()
bindItVariableVal TValue
ty Value
val =
  do PrimMap
prims   <- REPL PrimMap
getPrimMap
     Maybe Expr
mb      <- Eval (Maybe Expr) -> REPL (Maybe Expr)
forall a. Eval a -> REPL a
rEval (PrimMap -> TValue -> Value -> Eval (Maybe Expr)
Concrete.toExpr PrimMap
prims TValue
ty Value
val)
     case Maybe Expr
mb of
       Maybe Expr
Nothing   -> () -> REPL ()
forall a. a -> REPL a
forall (m :: * -> *) a. Monad m => a -> m a
return ()
       Just Expr
expr -> REPL Name -> REPL ()
forall (f :: * -> *) a. Functor f => f a -> f ()
void (REPL Name -> REPL ()) -> REPL Name -> REPL ()
forall a b. (a -> b) -> a -> b
$ TValue -> Expr -> REPL Name
bindItVariable TValue
ty Expr
expr


-- | Creates a fresh binding of "it" to a finite sequence of
-- expressions of the same type, and adds that sequence to the current
-- dynamic environment
bindItVariables :: E.TValue -> [T.Expr] -> REPL ()
bindItVariables :: TValue -> [Expr] -> REPL ()
bindItVariables TValue
ty [Expr]
exprs = REPL Name -> REPL ()
forall (f :: * -> *) a. Functor f => f a -> f ()
void (REPL Name -> REPL ()) -> REPL Name -> REPL ()
forall a b. (a -> b) -> a -> b
$ TValue -> Expr -> REPL Name
bindItVariable TValue
seqTy Expr
seqExpr
  where
    len :: Int
len = [Expr] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [Expr]
exprs
    seqTy :: TValue
seqTy = Integer -> TValue -> TValue
E.TVSeq (Int -> Integer
forall a. Integral a => a -> Integer
toInteger Int
len) TValue
ty
    seqExpr :: Expr
seqExpr = [Expr] -> Type -> Expr
T.EList [Expr]
exprs (TValue -> Type
E.tValTy TValue
ty)

replEvalDecls :: [P.Decl P.PName] -> REPL ()
replEvalDecls :: [Decl PName] -> REPL ()
replEvalDecls [Decl PName]
ds = do
  [DeclGroup]
dgs <- [Decl PName] -> REPL [DeclGroup]
replCheckDecls [Decl PName]
ds
  [DeclGroup] -> REPL ()
forall a. FreeVars a => a -> REPL ()
validEvalContext [DeclGroup]
dgs
  REPL () -> REPL ()
whenDebug ((DeclGroup -> REPL ()) -> [DeclGroup] -> REPL ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ (\DeclGroup
dg -> (String -> REPL ()
rPutStrLn (DeclGroup -> String
forall a. PP (WithNames a) => a -> String
dump DeclGroup
dg))) [DeclGroup]
dgs)
  ModuleCmd () -> REPL ()
forall a. ModuleCmd a -> REPL a
liftModuleCmd ([DeclGroup] -> ModuleCmd ()
M.evalDecls [DeclGroup]
dgs)

replEdit :: String -> REPL Bool
replEdit :: String -> REPL Bool
replEdit String
file = do
  Maybe String
mb <- IO (Maybe String) -> REPL (Maybe String)
forall a. IO a -> REPL a
io (String -> IO (Maybe String)
lookupEnv String
"EDITOR")
  let editor :: String
editor = String -> Maybe String -> String
forall a. a -> Maybe a -> a
fromMaybe String
"vim" Maybe String
mb
  IO Bool -> REPL Bool
forall a. IO a -> REPL a
io (IO Bool -> REPL Bool) -> IO Bool -> REPL Bool
forall a b. (a -> b) -> a -> b
$ do
    (Maybe Handle
_,Maybe Handle
_,Maybe Handle
_,ProcessHandle
ph) <- CreateProcess
-> IO (Maybe Handle, Maybe Handle, Maybe Handle, ProcessHandle)
createProcess (String -> CreateProcess
shell ([String] -> String
unwords [String
editor, String
file]))
    ExitCode
exit       <- ProcessHandle -> IO ExitCode
waitForProcess ProcessHandle
ph
    Bool -> IO Bool
forall a. a -> IO a
forall (m :: * -> *) a. Monad m => a -> m a
return (ExitCode
exit ExitCode -> ExitCode -> Bool
forall a. Eq a => a -> a -> Bool
== ExitCode
ExitSuccess)

type CommandMap = Trie CommandDescr

newSeedCmd :: REPL ()
newSeedCmd :: REPL ()
newSeedCmd =
  do  (Word64, Word64, Word64, Word64)
seed <- REPL (Word64, Word64, Word64, Word64)
createAndSetSeed
      String -> REPL ()
rPutStrLn String
"Seed initialized to:"
      String -> REPL ()
rPutStrLn ((Word64, Word64, Word64, Word64) -> String
forall a. Show a => a -> String
show (Word64, Word64, Word64, Word64)
seed)
  where
    createAndSetSeed :: REPL (Word64, Word64, Word64, Word64)
createAndSetSeed =
      (TFGen -> REPL ((Word64, Word64, Word64, Word64), TFGen))
-> REPL (Word64, Word64, Word64, Word64)
forall a. (TFGen -> REPL (a, TFGen)) -> REPL a
withRandomGen ((TFGen -> REPL ((Word64, Word64, Word64, Word64), TFGen))
 -> REPL (Word64, Word64, Word64, Word64))
-> (TFGen -> REPL ((Word64, Word64, Word64, Word64), TFGen))
-> REPL (Word64, Word64, Word64, Word64)
forall a b. (a -> b) -> a -> b
$ \TFGen
g0 ->
        let (Word64
s1, TFGen
g1) = TFGen -> (Word64, TFGen)
forall g. RandomGen g => g -> (Word64, g)
forall a g. (Random a, RandomGen g) => g -> (a, g)
TFI.random TFGen
g0
            (Word64
s2, TFGen
g2) = TFGen -> (Word64, TFGen)
forall g. RandomGen g => g -> (Word64, g)
forall a g. (Random a, RandomGen g) => g -> (a, g)
TFI.random TFGen
g1
            (Word64
s3, TFGen
g3) = TFGen -> (Word64, TFGen)
forall g. RandomGen g => g -> (Word64, g)
forall a g. (Random a, RandomGen g) => g -> (a, g)
TFI.random TFGen
g2
            (Word64
s4, TFGen
_)  = TFGen -> (Word64, TFGen)
forall g. RandomGen g => g -> (Word64, g)
forall a g. (Random a, RandomGen g) => g -> (a, g)
TFI.random TFGen
g3
            seed :: (Word64, Word64, Word64, Word64)
seed = (Word64
s1, Word64
s2, Word64
s3, Word64
s4)
        in  ((Word64, Word64, Word64, Word64), TFGen)
-> REPL ((Word64, Word64, Word64, Word64), TFGen)
forall a. a -> REPL a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ((Word64, Word64, Word64, Word64)
seed, (Word64, Word64, Word64, Word64) -> TFGen
TF.seedTFGen (Word64, Word64, Word64, Word64)
seed)

seedCmd :: String -> REPL ()
seedCmd :: String -> REPL ()
seedCmd String
s =
  case Maybe TFGen
mbGen of
    Maybe TFGen
Nothing -> String -> REPL ()
rPutStrLn String
"Could not parse seed argument - expecting an integer or 4-tuple of integers."
    Just TFGen
gen -> TFGen -> REPL ()
setRandomGen TFGen
gen

  where
    mbGen :: Maybe TFGen
mbGen =
          (Int -> TFGen
TF.mkTFGen (Int -> TFGen) -> Maybe Int -> Maybe TFGen
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> String -> Maybe Int
forall a. Read a => String -> Maybe a
readMaybe String
s)
      Maybe TFGen -> Maybe TFGen -> Maybe TFGen
forall a. Maybe a -> Maybe a -> Maybe a
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> ((Word64, Word64, Word64, Word64) -> TFGen
TF.seedTFGen ((Word64, Word64, Word64, Word64) -> TFGen)
-> Maybe (Word64, Word64, Word64, Word64) -> Maybe TFGen
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> String -> Maybe (Word64, Word64, Word64, Word64)
forall a. Read a => String -> Maybe a
readMaybe String
s)

-- Command Parsing -------------------------------------------------------------

-- | Strip leading space.
sanitize :: String -> String
sanitize :: ShowS
sanitize  = (Char -> Bool) -> ShowS
forall a. (a -> Bool) -> [a] -> [a]
dropWhile Char -> Bool
isSpace

-- | Strip trailing space.
sanitizeEnd :: String -> String
sanitizeEnd :: ShowS
sanitizeEnd = ShowS
forall a. [a] -> [a]
reverse ShowS -> ShowS -> ShowS
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ShowS
sanitize ShowS -> ShowS -> ShowS
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ShowS
forall a. [a] -> [a]
reverse

trim :: String -> String
trim :: ShowS
trim = ShowS
sanitizeEnd ShowS -> ShowS -> ShowS
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ShowS
sanitize

-- | Split at the first word boundary.
splitCommand :: String -> Maybe (Int,String,String)
splitCommand :: String -> Maybe (Int, String, String)
splitCommand = Int -> String -> Maybe (Int, String, String)
go Int
0
  where
   go :: Int -> String -> Maybe (Int, String, String)
go !Int
len (Char
c  : String
more)
      | Char -> Bool
isSpace Char
c = Int -> String -> Maybe (Int, String, String)
go (Int
lenInt -> Int -> Int
forall a. Num a => a -> a -> a
+Int
1) String
more

   go !Int
len (Char
':': String
more)
      | (String
as,String
bs) <- (Char -> Bool) -> String -> (String, String)
forall a. (a -> Bool) -> [a] -> ([a], [a])
span (\Char
x -> Char -> Bool
isPunctuation Char
x Bool -> Bool -> Bool
|| Char -> Bool
isSymbol Char
x) String
more
      , (String
ws,String
cs) <- (Char -> Bool) -> String -> (String, String)
forall a. (a -> Bool) -> [a] -> ([a], [a])
span Char -> Bool
isSpace String
bs
      , Bool -> Bool
not (String -> Bool
forall a. [a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null String
as) = (Int, String, String) -> Maybe (Int, String, String)
forall a. a -> Maybe a
Just (Int
lenInt -> Int -> Int
forall a. Num a => a -> a -> a
+Int
1Int -> Int -> Int
forall a. Num a => a -> a -> a
+String -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length String
asInt -> Int -> Int
forall a. Num a => a -> a -> a
+String -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length String
ws, Char
':' Char -> ShowS
forall a. a -> [a] -> [a]
: String
as, String
cs)

      | (String
as,String
bs) <- (Char -> Bool) -> String -> (String, String)
forall a. (a -> Bool) -> [a] -> ([a], [a])
break Char -> Bool
isSpace String
more
      , (String
ws,String
cs) <- (Char -> Bool) -> String -> (String, String)
forall a. (a -> Bool) -> [a] -> ([a], [a])
span Char -> Bool
isSpace String
bs
      , Bool -> Bool
not (String -> Bool
forall a. [a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null String
as) = (Int, String, String) -> Maybe (Int, String, String)
forall a. a -> Maybe a
Just (Int
lenInt -> Int -> Int
forall a. Num a => a -> a -> a
+Int
1Int -> Int -> Int
forall a. Num a => a -> a -> a
+String -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length String
asInt -> Int -> Int
forall a. Num a => a -> a -> a
+String -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length String
ws, Char
':' Char -> ShowS
forall a. a -> [a] -> [a]
: String
as, String
cs)

      | Bool
otherwise = Maybe (Int, String, String)
forall a. Maybe a
Nothing

   go !Int
len String
expr
      | String -> Bool
forall a. [a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null String
expr = Maybe (Int, String, String)
forall a. Maybe a
Nothing
      | Bool
otherwise = (Int, String, String) -> Maybe (Int, String, String)
forall a. a -> Maybe a
Just (Int
lenInt -> Int -> Int
forall a. Num a => a -> a -> a
+String -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length String
expr, String
expr, [])

-- | Uncons a list.
uncons :: [a] -> Maybe (a,[a])
uncons :: forall a. [a] -> Maybe (a, [a])
uncons [a]
as = case [a]
as of
  a
a:[a]
rest -> (a, [a]) -> Maybe (a, [a])
forall a. a -> Maybe a
Just (a
a,[a]
rest)
  [a]
_      -> Maybe (a, [a])
forall a. Maybe a
Nothing

-- | Lookup a string in the command list.
findCommand :: String -> [CommandDescr]
findCommand :: String -> [CommandDescr]
findCommand String
str = String -> CommandMap -> [CommandDescr]
forall a. String -> Trie a -> [a]
lookupTrie String
str CommandMap
commands

-- | Lookup a string in the command list, returning an exact match
-- even if it's the prefix of another command.
findCommandExact :: String -> [CommandDescr]
findCommandExact :: String -> [CommandDescr]
findCommandExact String
str = String -> CommandMap -> [CommandDescr]
forall a. String -> Trie a -> [a]
lookupTrieExact String
str CommandMap
commands

-- | Lookup a string in the notebook-safe command list.
findNbCommand :: Bool -> String -> [CommandDescr]
findNbCommand :: Bool -> String -> [CommandDescr]
findNbCommand Bool
True  String
str = String -> CommandMap -> [CommandDescr]
forall a. String -> Trie a -> [a]
lookupTrieExact String
str CommandMap
nbCommands
findNbCommand Bool
False String
str = String -> CommandMap -> [CommandDescr]
forall a. String -> Trie a -> [a]
lookupTrie      String
str CommandMap
nbCommands

-- | Parse a line as a command.
parseCommand :: (String -> [CommandDescr]) -> String -> Maybe Command
parseCommand :: (String -> [CommandDescr]) -> String -> Maybe Command
parseCommand String -> [CommandDescr]
findCmd String
line = do
  (Int
cmdLen,String
cmd,String
args) <- String -> Maybe (Int, String, String)
splitCommand String
line
  let args' :: String
args' = ShowS
sanitizeEnd String
args
  case String -> [CommandDescr]
findCmd String
cmd of
    [CommandDescr
c] -> case CommandDescr -> CommandBody
cBody CommandDescr
c of
      ExprArg     String -> (Int, Int) -> Maybe String -> REPL ()
body -> Command -> Maybe Command
forall a. a -> Maybe a
Just ((Int -> Maybe String -> REPL ()) -> Command
Command \Int
l Maybe String
fp -> (String -> (Int, Int) -> Maybe String -> REPL ()
body String
args' (Int
l,Int
cmdLenInt -> Int -> Int
forall a. Num a => a -> a -> a
+Int
1) Maybe String
fp))
      DeclsArg    String -> REPL ()
body -> Command -> Maybe Command
forall a. a -> Maybe a
Just ((Int -> Maybe String -> REPL ()) -> Command
Command \Int
_ Maybe String
_ -> (String -> REPL ()
body String
args'))
      ExprTypeArg String -> REPL ()
body -> Command -> Maybe Command
forall a. a -> Maybe a
Just ((Int -> Maybe String -> REPL ()) -> Command
Command \Int
_ Maybe String
_ -> (String -> REPL ()
body String
args'))
      ModNameArg  String -> REPL ()
body -> Command -> Maybe Command
forall a. a -> Maybe a
Just ((Int -> Maybe String -> REPL ()) -> Command
Command \Int
_ Maybe String
_ -> (String -> REPL ()
body String
args'))
      FilenameArg String -> REPL ()
body -> Command -> Maybe Command
forall a. a -> Maybe a
Just ((Int -> Maybe String -> REPL ()) -> Command
Command \Int
_ Maybe String
_ -> (String -> REPL ()
body (String -> REPL ()) -> REPL String -> REPL ()
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< String -> REPL String
expandHome String
args'))
      OptionArg   String -> REPL ()
body -> Command -> Maybe Command
forall a. a -> Maybe a
Just ((Int -> Maybe String -> REPL ()) -> Command
Command \Int
_ Maybe String
_ -> (String -> REPL ()
body String
args'))
      ShellArg    String -> REPL ()
body -> Command -> Maybe Command
forall a. a -> Maybe a
Just ((Int -> Maybe String -> REPL ()) -> Command
Command \Int
_ Maybe String
_ -> (String -> REPL ()
body String
args'))
      HelpArg     String -> REPL ()
body -> Command -> Maybe Command
forall a. a -> Maybe a
Just ((Int -> Maybe String -> REPL ()) -> Command
Command \Int
_ Maybe String
_ -> (String -> REPL ()
body String
args'))
      NoArg       REPL ()
body -> Command -> Maybe Command
forall a. a -> Maybe a
Just ((Int -> Maybe String -> REPL ()) -> Command
Command \Int
_ Maybe String
_ -> REPL ()
body)
      FileExprArg String -> String -> (Int, Int) -> Maybe String -> REPL ()
body ->
           do (Int
fpLen,String
fp,String
expr) <- String -> Maybe (Int, String, String)
extractFilePath String
args'
              Command -> Maybe Command
forall a. a -> Maybe a
Just ((Int -> Maybe String -> REPL ()) -> Command
Command \Int
l Maybe String
fp' -> do let col :: Int
col = Int
cmdLen Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
fpLen Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
1
                                         String
hm <- String -> REPL String
expandHome String
fp
                                         String -> String -> (Int, Int) -> Maybe String -> REPL ()
body String
hm String
expr (Int
l,Int
col) Maybe String
fp')
    [] -> case String -> Maybe (Char, String)
forall a. [a] -> Maybe (a, [a])
uncons String
cmd of
      Just (Char
':',String
_) -> Command -> Maybe Command
forall a. a -> Maybe a
Just (String -> Command
Unknown String
cmd)
      Just (Char, String)
_       -> Command -> Maybe Command
forall a. a -> Maybe a
Just ((Int -> Maybe String -> REPL ()) -> Command
Command (String -> Int -> Maybe String -> REPL ()
evalCmd String
line))
      Maybe (Char, String)
_            -> Maybe Command
forall a. Maybe a
Nothing

    [CommandDescr]
cs -> Command -> Maybe Command
forall a. a -> Maybe a
Just (String -> [String] -> Command
Ambiguous String
cmd ((CommandDescr -> [String]) -> [CommandDescr] -> [String]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap CommandDescr -> [String]
cNames [CommandDescr]
cs))

  where
  expandHome :: String -> REPL String
expandHome String
path =
    case String
path of
      Char
'~' : Char
c : String
more | Char -> Bool
isPathSeparator Char
c -> do String
dir <- IO String -> REPL String
forall a. IO a -> REPL a
io IO String
getHomeDirectory
                                               String -> REPL String
forall a. a -> REPL a
forall (m :: * -> *) a. Monad m => a -> m a
return (String
dir String -> ShowS
</> String
more)
      String
_ -> String -> REPL String
forall a. a -> REPL a
forall (m :: * -> *) a. Monad m => a -> m a
return String
path

  extractFilePath :: String -> Maybe (Int, String, String)
extractFilePath String
ipt =
    let quoted :: a -> [a] -> (Int, [a], [a])
quoted a
q = (\([a]
a,[a]
b) -> ([a] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [a]
a Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
2, [a]
a, Int -> [a] -> [a]
forall a. Int -> [a] -> [a]
drop Int
1 [a]
b)) (([a], [a]) -> (Int, [a], [a]))
-> ([a] -> ([a], [a])) -> [a] -> (Int, [a], [a])
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (a -> Bool) -> [a] -> ([a], [a])
forall a. (a -> Bool) -> [a] -> ([a], [a])
break (a -> a -> Bool
forall a. Eq a => a -> a -> Bool
== a
q)
    in case String
ipt of
        String
""        -> Maybe (Int, String, String)
forall a. Maybe a
Nothing
        Char
'\'':String
rest -> (Int, String, String) -> Maybe (Int, String, String)
forall a. a -> Maybe a
Just ((Int, String, String) -> Maybe (Int, String, String))
-> (Int, String, String) -> Maybe (Int, String, String)
forall a b. (a -> b) -> a -> b
$ Char -> String -> (Int, String, String)
forall {a}. Eq a => a -> [a] -> (Int, [a], [a])
quoted Char
'\'' String
rest
        Char
'"':String
rest  -> (Int, String, String) -> Maybe (Int, String, String)
forall a. a -> Maybe a
Just ((Int, String, String) -> Maybe (Int, String, String))
-> (Int, String, String) -> Maybe (Int, String, String)
forall a b. (a -> b) -> a -> b
$ Char -> String -> (Int, String, String)
forall {a}. Eq a => a -> [a] -> (Int, [a], [a])
quoted Char
'"' String
rest
        String
_         -> let (String
a,String
b) = (Char -> Bool) -> String -> (String, String)
forall a. (a -> Bool) -> [a] -> ([a], [a])
break Char -> Bool
isSpace String
ipt in
                     if String -> Bool
forall a. [a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null String
a then Maybe (Int, String, String)
forall a. Maybe a
Nothing else (Int, String, String) -> Maybe (Int, String, String)
forall a. a -> Maybe a
Just (String -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length String
a, String
a, String
b)



moduleInfoCmd :: Bool -> String -> REPL ()
moduleInfoCmd :: Bool -> String -> REPL ()
moduleInfoCmd Bool
isFile String
name
  | Bool
isFile = (ModulePath, FileInfo) -> REPL ()
showInfo ((ModulePath, FileInfo) -> REPL ())
-> REPL (ModulePath, FileInfo) -> REPL ()
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< ModuleCmd (ModulePath, FileInfo) -> REPL (ModulePath, FileInfo)
forall a. ModuleCmd a -> REPL a
liftModuleCmd (String -> ModuleCmd (ModulePath, FileInfo)
M.getFileDependencies String
name)
  | Bool
otherwise =
    case String -> Maybe ModName
parseModName String
name of
      Just ModName
m  -> (ModulePath, FileInfo) -> REPL ()
showInfo ((ModulePath, FileInfo) -> REPL ())
-> REPL (ModulePath, FileInfo) -> REPL ()
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< ModuleCmd (ModulePath, FileInfo) -> REPL (ModulePath, FileInfo)
forall a. ModuleCmd a -> REPL a
liftModuleCmd (ModName -> ModuleCmd (ModulePath, FileInfo)
M.getModuleDependencies ModName
m)
      Maybe ModName
Nothing -> String -> REPL ()
rPutStrLn String
"Invalid module name."

  where
  showInfo :: (ModulePath, FileInfo) -> REPL ()
showInfo (ModulePath
p,FileInfo
fi) =
    do String -> REPL ()
rPutStr String
"{ \"source\": "
       case ModulePath
p of
         M.InFile String
f  -> String -> REPL ()
rPutStrLn (ShowS
forall a. Show a => a -> String
show String
f)
         M.InMem String
l ByteString
_ -> String -> REPL ()
rPutStrLn (String
"{ \"internal\": " String -> ShowS
forall a. [a] -> [a] -> [a]
++ ShowS
forall a. Show a => a -> String
show String
l String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
" }")

       String -> REPL ()
rPutStrLn (String
", \"fingerprint\": \"0x" String -> ShowS
forall a. [a] -> [a] -> [a]
++
                       Fingerprint -> String
fingerprintHexString (FileInfo -> Fingerprint
M.fiFingerprint FileInfo
fi) String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
"\"")

       let depList :: (t -> String) -> String -> [t] -> REPL ()
depList t -> String
f String
x [t]
ys =
             do String -> REPL ()
rPutStr (String
", " String -> ShowS
forall a. [a] -> [a] -> [a]
++ ShowS
forall a. Show a => a -> String
show (String
x :: String) String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
":")
                case [t]
ys of
                  [] -> String -> REPL ()
rPutStrLn String
" []"
                  t
i : [t]
is ->
                    do String -> REPL ()
rPutStrLn String
""
                       String -> REPL ()
rPutStrLn (String
"     [ " String -> ShowS
forall a. [a] -> [a] -> [a]
++ t -> String
f t
i)
                       (t -> REPL ()) -> [t] -> REPL ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ (\t
j -> String -> REPL ()
rPutStrLn (String
"     , " String -> ShowS
forall a. [a] -> [a] -> [a]
++ t -> String
f t
j)) [t]
is
                       String -> REPL ()
rPutStrLn String
"     ]"

       ShowS -> String -> [String] -> REPL ()
forall {t}. (t -> String) -> String -> [t] -> REPL ()
depList ShowS
forall a. Show a => a -> String
show               String
"includes" (Set String -> [String]
forall a. Set a -> [a]
Set.toList (FileInfo -> Set String
M.fiIncludeDeps FileInfo
fi))
       (ModName -> String) -> String -> [ModName] -> REPL ()
forall {t}. (t -> String) -> String -> [t] -> REPL ()
depList (ShowS
forall a. Show a => a -> String
show ShowS -> (ModName -> String) -> ModName -> String
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Doc -> String
forall a. Show a => a -> String
show (Doc -> String) -> (ModName -> Doc) -> ModName -> String
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ModName -> Doc
forall a. PP a => a -> Doc
pp) String
"imports"  (Set ModName -> [ModName]
forall a. Set a -> [a]
Set.toList (FileInfo -> Set ModName
M.fiImportDeps  FileInfo
fi))
       ((String, Bool) -> String) -> String -> [(String, Bool)] -> REPL ()
forall {t}. (t -> String) -> String -> [t] -> REPL ()
depList (String, Bool) -> String
forall a. Show a => a -> String
show               String
"foreign"  (Map String Bool -> [(String, Bool)]
forall k a. Map k a -> [(k, a)]
Map.toList (FileInfo -> Map String Bool
M.fiForeignDeps FileInfo
fi))

       String -> REPL ()
rPutStrLn String
"}"