{-# LANGUAGE BangPatterns #-}
{-# LANGUAGE BlockArguments #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE LambdaCase #-}
{-# LANGUAGE MultiWayIf #-}
{-# LANGUAGE OverloadedStrings #-}
{-# LANGUAGE PatternGuards #-}
{-# LANGUAGE RecordWildCards #-}
{-# OPTIONS_GHC -Wno-incomplete-uni-patterns #-}
module Cryptol.REPL.Command (
Command(..), CommandDescr(..), CommandBody(..), CommandExitCode(..)
, parseCommand
, runCommand
, splitCommand
, findCommand
, findCommandExact
, findNbCommand
, commandList
, moduleCmd, loadCmd, loadPrelude, setOptionCmd
, interactiveConfig
, replParseExpr
, replEvalExpr
, replCheckExpr
, TestReport(..)
, qcExpr, qcCmd, QCMode(..)
, satCmd
, proveCmd
, onlineProveSat
, offlineProveSat
, handleCtrlC
, sanitize
, withRWTempFile
, 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)
data Command
= Command (Int -> Maybe FilePath -> REPL ())
| Ambiguous String [String]
| Unknown String
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
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
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
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
' '
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)
String -> REPL ()
rPutStrLn (Doc -> String
forall a. Show a => a -> String
show Doc
valDoc)
P.LetInput [Decl PName]
ds -> do
[Decl PName] -> REPL ()
replEvalDecls [Decl PName]
ds
ReplInput PName
P.EmptyInput ->
() -> 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
[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)
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)
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
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
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
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"]
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
expectedCoverage :: Integer -> Integer -> (Double, Double)
expectedCoverage :: Integer -> Integer -> (Double, Double)
expectedCoverage Integer
testNum Integer
sz =
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)
]
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)
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)
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)
(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
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"
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
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
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
byteStringToInteger :: BS.ByteString -> Integer
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 ()
| 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
}
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 ()
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"
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
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
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)
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"
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
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 ->
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
replCheckDecls :: [P.Decl P.PName] -> REPL [T.DeclGroup]
replCheckDecls :: [Decl PName] -> REPL [DeclGroup]
replCheckDecls [Decl PName]
ds = do
[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))
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
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)
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)
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
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
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
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)
sanitize :: String -> String
sanitize :: ShowS
sanitize = (Char -> Bool) -> ShowS
forall a. (a -> Bool) -> [a] -> [a]
dropWhile Char -> Bool
isSpace
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
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] -> 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
findCommand :: String -> [CommandDescr]
findCommand :: String -> [CommandDescr]
findCommand String
str = String -> CommandMap -> [CommandDescr]
forall a. String -> Trie a -> [a]
lookupTrie String
str CommandMap
commands
findCommandExact :: String -> [CommandDescr]
findCommandExact :: String -> [CommandDescr]
findCommandExact String
str = String -> CommandMap -> [CommandDescr]
forall a. String -> Trie a -> [a]
lookupTrieExact String
str CommandMap
commands
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
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
"}"