{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE OverloadedStrings #-}
{-# LANGUAGE PatternGuards #-}
{-# LANGUAGE RecordWildCards #-}
module Cryptol.REPL.Command (
Command(..), CommandDescr(..), CommandBody(..), CommandExitCode(..)
, parseCommand
, runCommand
, splitCommand
, findCommand
, findCommandExact
, findNbCommand
, commandList
, moduleCmd, loadCmd, loadPrelude, setOptionCmd
, interactiveConfig
, replParseExpr
, replEvalExpr
, replCheckExpr
, qcCmd, QCMode(..)
, satCmd
, proveCmd
, onlineProveSat
, offlineProveSat
, handleCtrlC
, sanitize
, replParse
, liftModuleCmd
, moduleCmdResult
) where
import Cryptol.REPL.Monad
import Cryptol.REPL.Trie
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))
import qualified Cryptol.Utils.Ident as M
import qualified Cryptol.ModuleSystem.Env as M
import qualified Cryptol.Eval.Monad as E
import qualified Cryptol.Eval.Value as E
import qualified Cryptol.Eval.Reference as R
import Cryptol.Testing.Concrete
import qualified Cryptol.Testing.Random as TestR
import Cryptol.Parser
(parseExprWith,parseReplWith,ParseError(),Config(..),defaultConfig
,parseModName,parseHelpName)
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 qualified Cryptol.TypeCheck.Solver.SMT as SMT
import Cryptol.TypeCheck.PP (dump,ppWithNames,emptyNameMap,backticks)
import Cryptol.Utils.PP
import Cryptol.Utils.Panic(panic)
import qualified Cryptol.Parser.AST as P
import qualified Cryptol.Transform.Specialize as S
import Cryptol.Symbolic (ProverCommand(..), QueryType(..), SatNum(..),ProverStats)
import qualified Cryptol.Symbolic as Symbolic
import qualified Control.Exception as X
import Control.Monad hiding (mapM, mapM)
import Control.Monad.IO.Class(liftIO)
import Data.ByteString (ByteString)
import qualified Data.ByteString as BS
import qualified Data.ByteString.Char8 as BS8
import Data.Bits ((.&.))
import Data.Char (isSpace,isPunctuation,isSymbol,isAlphaNum,isAscii)
import Data.Function (on)
import Data.List (intercalate, nub, sortBy, partition, isPrefixOf,intersperse)
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 qualified Data.Map as Map
import qualified Data.Set as Set
import System.IO(hFlush,stdout,openTempFile,hClose)
import System.Random.TF(newTFGen)
import Numeric (showFFloat)
import qualified Data.Text as T
import Data.IORef(newIORef,readIORef)
import GHC.Float (log1p, expm1)
import Prelude ()
import Prelude.Compat
import qualified Data.SBV as SBV (Solver)
import qualified Data.SBV.Internals as SBV (showTDiff)
data Command
= Command (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
}
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 -> REPL ())
| FileExprArg (FilePath -> String -> 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 (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 m :: CommandMap
m d :: CommandDescr
d = (CommandMap -> String -> CommandMap)
-> CommandMap -> [String] -> CommandMap
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 d :: a
d m :: Trie a
m name :: 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 (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 m :: CommandMap
m d :: CommandDescr
d = (CommandMap -> String -> CommandMap)
-> CommandMap -> [String] -> CommandMap
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 d :: a
d m :: Trie a
m name :: 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 -> CommandDescr
CommandDescr [ ":t", ":type" ] ["EXPR"] ((String -> REPL ()) -> CommandBody
ExprArg String -> REPL ()
typeOfCmd)
"Check the type of an expression."
, [String] -> [String] -> CommandBody -> String -> CommandDescr
CommandDescr [ ":b", ":browse" ] ["[ MODULE ]"] ((String -> REPL ()) -> CommandBody
ModNameArg String -> REPL ()
browseCmd)
"Display environment for all loaded modules, or for a specific module."
, [String] -> [String] -> CommandBody -> String -> CommandDescr
CommandDescr [ ":?", ":help" ] ["[ TOPIC ]"] ((String -> REPL ()) -> CommandBody
HelpArg String -> REPL ()
helpCmd)
"Display a brief description of a function, type, or command."
, [String] -> [String] -> CommandBody -> String -> CommandDescr
CommandDescr [ ":s", ":set" ] ["[ OPTION [ = VALUE ] ]"] ((String -> REPL ()) -> CommandBody
OptionArg String -> REPL ()
setOptionCmd)
"Set an environmental option (:set on its own displays current values)."
, [String] -> [String] -> CommandBody -> String -> CommandDescr
CommandDescr [ ":check" ] ["[ EXPR ]"] ((String -> REPL ()) -> CommandBody
ExprArg (REPL [TestReport] -> REPL ()
forall (f :: * -> *) a. Functor f => f a -> f ()
void (REPL [TestReport] -> REPL ())
-> (String -> REPL [TestReport]) -> String -> REPL ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. QCMode -> String -> REPL [TestReport]
qcCmd QCMode
QCRandom))
"Use random testing to check that the argument always returns true.\n(If no argument, check all properties.)"
, [String] -> [String] -> CommandBody -> String -> CommandDescr
CommandDescr [ ":exhaust" ] ["[ EXPR ]"] ((String -> REPL ()) -> CommandBody
ExprArg (REPL [TestReport] -> REPL ()
forall (f :: * -> *) a. Functor f => f a -> f ()
void (REPL [TestReport] -> REPL ())
-> (String -> REPL [TestReport]) -> String -> REPL ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. QCMode -> String -> REPL [TestReport]
qcCmd QCMode
QCExhaust))
"Use exhaustive testing to prove that the argument always returns\ntrue. (If no argument, check all properties.)"
, [String] -> [String] -> CommandBody -> String -> CommandDescr
CommandDescr [ ":prove" ] ["[ EXPR ]"] ((String -> REPL ()) -> CommandBody
ExprArg String -> REPL ()
proveCmd)
"Use an external solver to prove that the argument always returns\ntrue. (If no argument, check all properties.)"
, [String] -> [String] -> CommandBody -> String -> CommandDescr
CommandDescr [ ":sat" ] ["[ EXPR ]"] ((String -> REPL ()) -> CommandBody
ExprArg String -> REPL ()
satCmd)
"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] -> CommandBody -> String -> CommandDescr
CommandDescr [ ":debug_specialize" ] ["EXPR"]((String -> REPL ()) -> CommandBody
ExprArg String -> REPL ()
specializeCmd)
"Do type specialization on a closed expression."
, [String] -> [String] -> CommandBody -> String -> CommandDescr
CommandDescr [ ":eval" ] ["EXPR"] ((String -> REPL ()) -> CommandBody
ExprArg String -> REPL ()
refEvalCmd)
"Evaluate an expression with the reference evaluator."
, [String] -> [String] -> CommandBody -> String -> CommandDescr
CommandDescr [ ":ast" ] ["EXPR"] ((String -> REPL ()) -> CommandBody
ExprArg String -> REPL ()
astOfCmd)
"Print out the pre-typechecked AST of a given term."
, [String] -> [String] -> CommandBody -> String -> CommandDescr
CommandDescr [ ":extract-coq" ] [] (REPL () -> CommandBody
NoArg REPL ()
allTerms)
"Print out the post-typechecked AST of all currently defined terms,\nin a Coq-parseable format."
]
commandList :: [CommandDescr]
commandList :: [CommandDescr]
commandList =
[CommandDescr]
nbCommandList [CommandDescr] -> [CommandDescr] -> [CommandDescr]
forall a. [a] -> [a] -> [a]
++
[ [String] -> [String] -> CommandBody -> String -> CommandDescr
CommandDescr [ ":q", ":quit" ] [] (REPL () -> CommandBody
NoArg REPL ()
quitCmd)
"Exit the REPL."
, [String] -> [String] -> CommandBody -> String -> CommandDescr
CommandDescr [ ":l", ":load" ] ["FILE"] ((String -> REPL ()) -> CommandBody
FilenameArg String -> REPL ()
loadCmd)
"Load a module by filename."
, [String] -> [String] -> CommandBody -> String -> CommandDescr
CommandDescr [ ":r", ":reload" ] [] (REPL () -> CommandBody
NoArg REPL ()
reloadCmd)
"Reload the currently loaded module."
, [String] -> [String] -> CommandBody -> String -> CommandDescr
CommandDescr [ ":e", ":edit" ] ["[ FILE ]"] ((String -> REPL ()) -> CommandBody
FilenameArg String -> REPL ()
editCmd)
"Edit FILE or the currently loaded module."
, [String] -> [String] -> CommandBody -> String -> CommandDescr
CommandDescr [ ":!" ] ["COMMAND"] ((String -> REPL ()) -> CommandBody
ShellArg String -> REPL ()
runShellCmd)
"Execute a command in the shell."
, [String] -> [String] -> CommandBody -> String -> CommandDescr
CommandDescr [ ":cd" ] ["DIR"] ((String -> REPL ()) -> CommandBody
FilenameArg String -> REPL ()
cdCmd)
"Set the current working directory."
, [String] -> [String] -> CommandBody -> String -> CommandDescr
CommandDescr [ ":m", ":module" ] ["[ MODULE ]"] ((String -> REPL ()) -> CommandBody
FilenameArg String -> REPL ()
moduleCmd)
"Load a module by its name."
, [String] -> [String] -> CommandBody -> String -> CommandDescr
CommandDescr [ ":w", ":writeByteArray" ] ["FILE", "EXPR"] ((String -> String -> REPL ()) -> CommandBody
FileExprArg String -> String -> REPL ()
writeFileCmd)
"Write data of type 'fin n => [n][8]' to a file."
, [String] -> [String] -> CommandBody -> String -> CommandDescr
CommandDescr [ ":readByteArray" ] ["FILE"] ((String -> REPL ()) -> CommandBody
FilenameArg String -> REPL ()
readFileCmd)
"Read data from a file as type 'fin n => [n][8]', binding\nthe value to variable 'it'."
, [String] -> [String] -> CommandBody -> String -> CommandDescr
CommandDescr [ ":dumptests" ] ["FILE", "EXPR"] ((String -> String -> REPL ()) -> CommandBody
FileExprArg String -> String -> REPL ()
dumpTestsCmd)
([String] -> String
unlines [ "Dump a tab-separated collection of tests for the given"
, "expression into a file. The first column in each line is"
, "the expected output, and the remainder are the inputs. The"
, "number of tests is determined by the \"tests\" option."
])
]
genHelp :: [CommandDescr] -> [String]
genHelp :: [CommandDescr] -> [String]
genHelp cs :: [CommandDescr]
cs = (CommandDescr -> String) -> [CommandDescr] -> [String]
forall a b. (a -> b) -> [a] -> [b]
map CommandDescr -> String
cmdHelp [CommandDescr]
cs
where
cmdHelp :: CommandDescr -> String
cmdHelp cmd :: CommandDescr
cmd = [String] -> String
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat ([String] -> String) -> [String] -> String
forall a b. (a -> b) -> a -> b
$ [ " ", 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 ("\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 cmd :: CommandDescr
cmd = String -> [String] -> String
forall a. [a] -> [[a]] -> [a]
intercalate ", " (CommandDescr -> [String]
cNames CommandDescr
cmd)
padding :: Int
padding = 2 Int -> Int -> Int
forall a. Num a => a -> a -> a
+ [Int] -> Int
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 (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 n :: t a
n = Int -> Char -> String
forall a. Int -> a -> [a]
replicate (Int -> Int -> Int
forall a. Ord a => a -> a -> a
max 0 (Int
padding Int -> Int -> Int
forall a. Num a => a -> a -> a
- t a -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length t a
n)) ' '
runCommand :: Command -> REPL CommandExitCode
runCommand :: Command -> REPL CommandExitCode
runCommand c :: Command
c = case Command
c of
Command cmd :: REPL ()
cmd -> (REPL ()
cmd REPL () -> REPL CommandExitCode -> REPL CommandExitCode
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> CommandExitCode -> REPL CommandExitCode
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 re :: a
re = String -> REPL ()
rPutStrLn "" REPL () -> REPL () -> REPL ()
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 (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> CommandExitCode -> REPL CommandExitCode
forall (m :: * -> *) a. Monad m => a -> m a
return CommandExitCode
CommandError
Unknown cmd :: String
cmd -> do String -> REPL ()
rPutStrLn ("Unknown command: " String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
cmd)
CommandExitCode -> REPL CommandExitCode
forall (m :: * -> *) a. Monad m => a -> m a
return CommandExitCode
CommandError
Ambiguous cmd :: String
cmd cmds :: [String]
cmds -> do
String -> REPL ()
rPutStrLn (String
cmd String -> ShowS
forall a. [a] -> [a] -> [a]
++ " is ambiguous, it could mean one of:")
String -> REPL ()
rPutStrLn ("\t" String -> ShowS
forall a. [a] -> [a] -> [a]
++ String -> [String] -> String
forall a. [a] -> [[a]] -> [a]
intercalate ", " [String]
cmds)
CommandExitCode -> REPL CommandExitCode
forall (m :: * -> *) a. Monad m => a -> m a
return CommandExitCode
CommandError
getPPValOpts :: REPL E.PPOpts
getPPValOpts :: REPL PPOpts
getPPValOpts =
do Int
base <- String -> REPL Int
forall a. IsEnvVal a => String -> REPL a
getKnownUser "base"
Bool
ascii <- String -> REPL Bool
forall a. IsEnvVal a => String -> REPL a
getKnownUser "ascii"
Int
infLength <- String -> REPL Int
forall a. IsEnvVal a => String -> REPL a
getKnownUser "infLength"
PPOpts -> REPL PPOpts
forall (m :: * -> *) a. Monad m => a -> m a
return PPOpts :: Bool -> Int -> Int -> PPOpts
E.PPOpts { useBase :: Int
E.useBase = Int
base
, useAscii :: Bool
E.useAscii = Bool
ascii
, useInfLength :: Int
E.useInfLength = Int
infLength
}
getEvalOpts :: REPL E.EvalOpts
getEvalOpts :: REPL EvalOpts
getEvalOpts =
do PPOpts
ppOpts <- REPL PPOpts
getPPValOpts
Logger
l <- REPL Logger
getLogger
EvalOpts -> REPL EvalOpts
forall (m :: * -> *) a. Monad m => a -> m a
return EvalOpts :: Logger -> PPOpts -> EvalOpts
E.EvalOpts { evalPPOpts :: PPOpts
E.evalPPOpts = PPOpts
ppOpts, evalLogger :: Logger
E.evalLogger = Logger
l }
evalCmd :: String -> REPL ()
evalCmd :: String -> REPL ()
evalCmd str :: String
str = do
Bool
letEnabled <- REPL Bool
getLetEnabled
ReplInput PName
ri <- if Bool
letEnabled
then String -> REPL (ReplInput PName)
replParseInput String
str
else Expr PName -> ReplInput PName
forall name. Expr name -> ReplInput name
P.ExprInput (Expr PName -> ReplInput PName)
-> REPL (Expr PName) -> REPL (ReplInput PName)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> String -> REPL (Expr PName)
replParseExpr String
str
case ReplInput PName
ri of
P.ExprInput expr :: Expr PName
expr -> do
(val :: Value
val,_ty :: 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 (PPOpts -> Value -> Eval Doc
forall b w i. BitWord b w i => PPOpts -> GenValue b w i -> Eval Doc
E.ppValue PPOpts
ppOpts Value
val)
String -> REPL ()
rPutStrLn (Doc -> String
forall a. Show a => a -> String
show Doc
valDoc)
P.LetInput decl :: Decl PName
decl -> do
Decl PName -> REPL ()
replEvalDecl Decl PName
decl
printCounterexample :: Bool -> P.Expr P.PName -> [E.Value] -> REPL ()
printCounterexample :: Bool -> Expr PName -> [Value] -> REPL ()
printCounterexample isSat :: Bool
isSat pexpr :: Expr PName
pexpr vs :: [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)
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
. PPOpts -> Value -> Eval Doc
forall b w i. BitWord b w i => PPOpts -> GenValue b w i -> Eval Doc
E.ppValue PPOpts
ppOpts) [Value]
vs
let doc :: Doc
doc = Int -> Expr PName -> Doc
forall a. PP a => Int -> a -> Doc
ppPrec 3 Expr PName
pexpr
Doc -> REPL ()
forall a. Show a => a -> REPL ()
rPrint (Doc -> REPL ()) -> Doc -> REPL ()
forall a b. (a -> b) -> a -> b
$ Doc -> Int -> Doc -> Doc
hang Doc
doc 2 ([Doc] -> Doc
sep [Doc]
docs) Doc -> Doc -> Doc
<+>
String -> Doc
text (if Bool
isSat then "= True" else "= False")
dumpTestsCmd :: FilePath -> String -> REPL ()
dumpTestsCmd :: String -> String -> REPL ()
dumpTestsCmd outFile :: String
outFile str :: String
str =
do Expr PName
expr <- String -> REPL (Expr PName)
replParseExpr String
str
(val :: Value
val, ty :: Type
ty) <- Expr PName -> REPL (Value, Type)
replEvalExpr Expr PName
expr
EvalOpts
evo <- REPL EvalOpts
getEvalOpts
PPOpts
ppopts <- REPL PPOpts
getPPValOpts
Int
testNum <- String -> REPL Int
forall a. IsEnvVal a => String -> REPL a
getKnownUser "tests" :: REPL Int
TFGen
g <- IO TFGen -> REPL TFGen
forall a. IO a -> REPL a
io IO TFGen
newTFGen
[Gen TFGen Bool BV Integer]
gens <-
case Type -> Maybe [Gen TFGen Bool BV Integer]
forall g. RandomGen g => Type -> Maybe [Gen g Bool BV Integer]
TestR.dumpableType Type
ty of
Nothing -> REPLException -> REPL [Gen TFGen Bool BV Integer]
forall a. REPLException -> REPL a
raise (Type -> REPLException
TypeNotTestable Type
ty)
Just gens :: [Gen TFGen Bool BV Integer]
gens -> [Gen TFGen Bool BV Integer] -> REPL [Gen TFGen Bool BV Integer]
forall (m :: * -> *) a. Monad m => a -> m a
return [Gen TFGen Bool BV Integer]
gens
[([Value], Value)]
tests <- IO [([Value], Value)] -> REPL [([Value], Value)]
forall a. IO a -> REPL a
io (IO [([Value], Value)] -> REPL [([Value], Value)])
-> IO [([Value], Value)] -> REPL [([Value], Value)]
forall a b. (a -> b) -> a -> b
$ TFGen
-> EvalOpts
-> [Gen TFGen Bool BV Integer]
-> Value
-> Int
-> IO [([Value], Value)]
forall g.
RandomGen g =>
g
-> EvalOpts
-> [Gen g Bool BV Integer]
-> Value
-> Int
-> IO [([Value], Value)]
TestR.returnTests TFGen
g EvalOpts
evo [Gen TFGen Bool BV Integer]
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
$
\(args :: [Value]
args, x :: 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)
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
. PPOpts -> Value -> Eval Doc
forall b w i. BitWord b w i => PPOpts -> GenValue b w i -> Eval Doc
E.ppValue PPOpts
ppopts) [Value]
args
Doc
resOut <- Eval Doc -> REPL Doc
forall a. Eval a -> REPL a
rEval (PPOpts -> Value -> Eval Doc
forall b w i. BitWord b w i => PPOpts -> GenValue b w i -> Eval Doc
E.ppValue PPOpts
ppopts Value
x)
String -> REPL String
forall (m :: * -> *) a. Monad m => a -> m a
return (Doc -> String
renderOneLine Doc
resOut String -> ShowS
forall a. [a] -> [a] -> [a]
++ "\t" String -> ShowS
forall a. [a] -> [a] -> [a]
++ String -> [String] -> String
forall a. [a] -> [[a]] -> [a]
intercalate "\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]
++ "\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 e :: 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
/= :: QCMode -> QCMode -> Bool
$c/= :: QCMode -> QCMode -> Bool
== :: QCMode -> QCMode -> Bool
$c== :: 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
showList :: [QCMode] -> ShowS
$cshowList :: [QCMode] -> ShowS
show :: QCMode -> String
$cshow :: QCMode -> String
showsPrec :: Int -> QCMode -> ShowS
$cshowsPrec :: Int -> QCMode -> ShowS
Show)
qcCmd :: QCMode -> String -> REPL [TestReport]
qcCmd :: QCMode -> String -> REPL [TestReport]
qcCmd qcMode :: QCMode
qcMode "" =
do (xs :: [Name]
xs,disp :: NameDisp
disp) <- REPL ([Name], NameDisp)
getPropertyNames
let nameStr :: a -> String
nameStr x :: 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] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [Name]
xs
then String -> REPL ()
rPutStrLn "There are no properties in scope." REPL () -> REPL [TestReport] -> REPL [TestReport]
forall (f :: * -> *) a b. Applicative f => f a -> f b -> f b
*> [TestReport] -> REPL [TestReport]
forall (m :: * -> *) a. Monad m => a -> m a
return []
else [[TestReport]] -> [TestReport]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat ([[TestReport]] -> [TestReport])
-> REPL [[TestReport]] -> REPL [TestReport]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ([Name] -> (Name -> REPL [TestReport]) -> REPL [[TestReport]]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
t a -> (a -> m b) -> m (t b)
forM [Name]
xs ((Name -> REPL [TestReport]) -> REPL [[TestReport]])
-> (Name -> REPL [TestReport]) -> REPL [[TestReport]]
forall a b. (a -> b) -> a -> b
$ \x :: Name
x ->
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
$ "property " String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
str String -> ShowS
forall a. [a] -> [a] -> [a]
++ " "
QCMode -> String -> REPL [TestReport]
qcCmd QCMode
qcMode String
str)
qcCmd qcMode :: QCMode
qcMode str :: String
str =
do Expr PName
expr <- String -> REPL (Expr PName)
replParseExpr String
str
(val :: Value
val,ty :: Type
ty) <- Expr PName -> REPL (Value, Type)
replEvalExpr Expr PName
expr
Int
testNum <- String -> REPL Int
forall a. IsEnvVal a => String -> REPL a
getKnownUser "tests"
case Type -> Maybe (Maybe Integer, [Type], [[Value]])
testableType Type
ty of
Just (Just sz :: Integer
sz,tys :: [Type]
tys,vss :: [[Value]]
vss) | 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
<= Int -> Integer
forall a. Integral a => a -> Integer
toInteger Int
testNum -> do
String -> REPL ()
rPutStrLn "Using exhaustive testing."
let f :: p -> [[Value]] -> REPL (TestResult, [[Value]])
f _ [] = String -> [String] -> REPL (TestResult, [[Value]])
forall a. HasCallStack => String -> [String] -> a
panic "Cryptol.REPL.Command"
["Exhaustive testing ran out of test cases"]
f _ (vs :: [Value]
vs : vss1 :: [[Value]]
vss1) = do
EvalOpts
evo <- REPL EvalOpts
getEvalOpts
TestResult
result <- IO TestResult -> REPL TestResult
forall a. IO a -> REPL a
io (IO TestResult -> REPL TestResult)
-> IO TestResult -> REPL TestResult
forall a b. (a -> b) -> a -> b
$ EvalOpts -> Value -> [Value] -> IO TestResult
runOneTest EvalOpts
evo Value
val [Value]
vs
(TestResult, [[Value]]) -> REPL (TestResult, [[Value]])
forall (m :: * -> *) a. Monad m => a -> m a
return (TestResult
result, [[Value]]
vss1)
testSpec :: TestSpec REPL [[Value]]
testSpec = TestSpec :: forall (m :: * -> *) s.
(Integer -> s -> m (TestResult, s))
-> String
-> Integer
-> Maybe Integer
-> (Integer -> Integer -> m ())
-> m ()
-> (TestResult -> m ())
-> m ()
-> TestSpec m s
TestSpec {
testFn :: Integer -> [[Value]] -> REPL (TestResult, [[Value]])
testFn = Integer -> [[Value]] -> REPL (TestResult, [[Value]])
forall p. p -> [[Value]] -> REPL (TestResult, [[Value]])
f
, testProp :: String
testProp = String
str
, testTotal :: Integer
testTotal = Integer
sz
, testPossible :: Maybe Integer
testPossible = Integer -> Maybe Integer
forall a. a -> Maybe a
Just Integer
sz
, testRptProgress :: Integer -> Integer -> REPL ()
testRptProgress = Integer -> Integer -> REPL ()
forall a. (Show a, Integral a) => a -> a -> REPL ()
ppProgress
, testClrProgress :: REPL ()
testClrProgress = REPL ()
delProgress
, testRptFailure :: TestResult -> REPL ()
testRptFailure = [Type] -> Expr PName -> TestResult -> REPL ()
ppFailure [Type]
tys Expr PName
expr
, testRptSuccess :: REPL ()
testRptSuccess = do
REPL ()
delTesting
String -> REPL ()
prtLn (String -> REPL ()) -> String -> REPL ()
forall a b. (a -> b) -> a -> b
$ "Passed " String -> ShowS
forall a. [a] -> [a] -> [a]
++ Integer -> String
forall a. Show a => a -> String
show Integer
sz String -> ShowS
forall a. [a] -> [a] -> [a]
++ " tests."
String -> REPL ()
rPutStrLn "Q.E.D."
}
String -> REPL ()
prt String
testingMsg
TestReport
report <- TestSpec REPL [[Value]] -> [[Value]] -> REPL TestReport
forall (m :: * -> *) s.
Monad m =>
TestSpec m s -> s -> m TestReport
runTests TestSpec REPL [[Value]]
testSpec [[Value]]
vss
[TestReport] -> REPL [TestReport]
forall (m :: * -> *) a. Monad m => a -> m a
return [TestReport
report]
Just (sz :: Maybe Integer
sz,tys :: [Type]
tys,_) | QCMode
qcMode QCMode -> QCMode -> Bool
forall a. Eq a => a -> a -> Bool
== QCMode
QCRandom ->
case Type -> Maybe [Gen TFGen Bool BV Integer]
forall g. RandomGen g => Type -> Maybe [Gen g Bool BV Integer]
TestR.testableType Type
ty of
Nothing -> REPLException -> REPL [TestReport]
forall a. REPLException -> REPL a
raise (Type -> REPLException
TypeNotTestable Type
ty)
Just gens :: [Gen TFGen Bool BV Integer]
gens -> do
String -> REPL ()
rPutStrLn "Using random testing."
EvalOpts
evo <- REPL EvalOpts
getEvalOpts
let testSpec :: TestSpec REPL TFGen
testSpec = TestSpec :: forall (m :: * -> *) s.
(Integer -> s -> m (TestResult, s))
-> String
-> Integer
-> Maybe Integer
-> (Integer -> Integer -> m ())
-> m ()
-> (TestResult -> m ())
-> m ()
-> TestSpec m s
TestSpec {
testFn :: Integer -> TFGen -> REPL (TestResult, TFGen)
testFn = \sz' :: Integer
sz' g :: TFGen
g ->
IO (TestResult, TFGen) -> REPL (TestResult, TFGen)
forall a. IO a -> REPL a
io (IO (TestResult, TFGen) -> REPL (TestResult, TFGen))
-> IO (TestResult, TFGen) -> REPL (TestResult, TFGen)
forall a b. (a -> b) -> a -> b
$ EvalOpts
-> Value
-> [Gen TFGen Bool BV Integer]
-> Integer
-> TFGen
-> IO (TestResult, TFGen)
forall g.
RandomGen g =>
EvalOpts
-> Value
-> [Gen g Bool BV Integer]
-> Integer
-> g
-> IO (TestResult, g)
TestR.runOneTest EvalOpts
evo Value
val [Gen TFGen Bool BV Integer]
gens Integer
sz' TFGen
g
, testProp :: String
testProp = String
str
, testTotal :: Integer
testTotal = Int -> Integer
forall a. Integral a => a -> Integer
toInteger Int
testNum
, testPossible :: Maybe Integer
testPossible = Maybe Integer
sz
, testRptProgress :: Integer -> Integer -> REPL ()
testRptProgress = Integer -> Integer -> REPL ()
forall a. (Show a, Integral a) => a -> a -> REPL ()
ppProgress
, testClrProgress :: REPL ()
testClrProgress = REPL ()
delProgress
, testRptFailure :: TestResult -> REPL ()
testRptFailure = [Type] -> Expr PName -> TestResult -> REPL ()
ppFailure [Type]
tys Expr PName
expr
, testRptSuccess :: REPL ()
testRptSuccess = do
REPL ()
delTesting
String -> REPL ()
prtLn (String -> REPL ()) -> String -> REPL ()
forall a b. (a -> b) -> a -> b
$ "Passed " String -> ShowS
forall a. [a] -> [a] -> [a]
++ Int -> String
forall a. Show a => a -> String
show Int
testNum String -> ShowS
forall a. [a] -> [a] -> [a]
++ " tests."
}
String -> REPL ()
prt String
testingMsg
TFGen
g <- IO TFGen -> REPL TFGen
forall a. IO a -> REPL a
io IO TFGen
newTFGen
TestReport
report <- TestSpec REPL TFGen -> TFGen -> REPL TestReport
forall (m :: * -> *) s.
Monad m =>
TestSpec m s -> s -> m TestReport
runTests TestSpec REPL TFGen
testSpec TFGen
g
Bool -> REPL () -> REPL ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (TestResult -> Bool
isPass (TestReport -> TestResult
reportResult TestReport
report)) (REPL () -> REPL ()) -> REPL () -> REPL ()
forall a b. (a -> b) -> a -> b
$
case Maybe Integer
sz of
Nothing -> () -> REPL ()
forall (m :: * -> *) a. Monad m => a -> m a
return ()
Just n :: Integer
n -> String -> REPL ()
rPutStrLn (String -> REPL ()) -> String -> REPL ()
forall a b. (a -> b) -> a -> b
$ Int -> Integer -> String
coverageString Int
testNum Integer
n
[TestReport] -> REPL [TestReport]
forall (m :: * -> *) a. Monad m => a -> m a
return [TestReport
report]
_ -> REPLException -> REPL [TestReport]
forall a. REPLException -> REPL a
raise (Type -> REPLException
TypeNotTestable Type
ty)
where
testingMsg :: String
testingMsg = "Testing... "
coverageString :: Int -> Integer -> String
coverageString testNum :: Int
testNum sz :: Integer
sz =
let (percent :: Double
percent, expectedUnique :: Double
expectedUnique) = Int -> Integer -> (Double, Double)
expectedCoverage Int
testNum Integer
sz
showValNum :: String
showValNum
| Integer
sz Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
> 2 Integer -> Integer -> Integer
forall a b. (Num a, Integral b) => a -> b -> a
^ (20::Integer) =
"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 "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 2) Double
percent "% ("
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 0) Double
expectedUnique " of "
String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
showValNum
String -> ShowS
forall a. [a] -> [a] -> [a]
++ " values)"
totProgressWidth :: Int
totProgressWidth = 4
lg2 :: Integer -> Integer
lg2 :: Integer -> Integer
lg2 x :: Integer
x | Integer
x Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
>= 2Integer -> Int -> Integer
forall a b. (Num a, Integral b) => a -> b -> a
^(1024::Int) = 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` 2Integer -> Int -> Integer
forall a b. (Num a, Integral b) => a -> b -> a
^(1024::Int))
| Integer
x Integer -> Integer -> Bool
forall a. Eq a => a -> a -> Bool
== 0 = 0
| Bool
otherwise = let valNumD :: Double
valNumD = Integer -> Double
forall a. Num a => Integer -> a
fromInteger Integer
x :: Double
in Double -> Integer
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 2 Double
valNumD :: Integer
prt :: String -> REPL ()
prt msg :: String
msg = String -> REPL ()
rPutStr String
msg REPL () -> REPL () -> REPL ()
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)
prtLn :: String -> REPL ()
prtLn msg :: String
msg = String -> REPL ()
rPutStrLn String
msg REPL () -> REPL () -> REPL ()
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 :: a -> a -> REPL ()
ppProgress this :: a
this tot :: a
tot = REPL () -> REPL ()
unlessBatch (REPL () -> REPL ()) -> REPL () -> REPL ()
forall a b. (a -> b) -> a -> b
$
let percent :: String
percent = a -> String
forall a. Show a => a -> String
show (a -> a -> a
forall a. Integral a => a -> a -> a
div (100 a -> a -> a
forall a. Num a => a -> a -> a
* a
this) a
tot) String -> ShowS
forall a. [a] -> [a] -> [a]
++ "%"
width :: Int
width = String -> 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) ' '
in String -> REPL ()
prt (String
pad String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
percent)
del :: Int -> REPL ()
del n :: 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 '\BS' String -> ShowS
forall a. [a] -> [a] -> [a]
++ Int -> Char -> String
forall a. Int -> a -> [a]
replicate Int
n ' ' String -> ShowS
forall a. [a] -> [a] -> [a]
++ Int -> Char -> String
forall a. Int -> a -> [a]
replicate Int
n '\BS')
delTesting :: REPL ()
delTesting = Int -> REPL ()
del (String -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length String
testingMsg)
delProgress :: REPL ()
delProgress = Int -> REPL ()
del Int
totProgressWidth
ppFailure :: [Type] -> Expr PName -> TestResult -> REPL ()
ppFailure tys :: [Type]
tys pexpr :: Expr PName
pexpr failure :: TestResult
failure = do
REPL ()
delTesting
PPOpts
opts <- REPL PPOpts
getPPValOpts
case TestResult
failure of
FailFalse vs :: [Value]
vs -> do
let isSat :: Bool
isSat = Bool
False
Bool -> Expr PName -> [Value] -> REPL ()
printCounterexample Bool
isSat Expr PName
pexpr [Value]
vs
case ([Type]
tys,[Value]
vs) of
([t :: Type
t],[v :: Value
v]) -> Type -> Value -> REPL ()
bindItVariableVal Type
t Value
v
_ -> let fs :: [Ident]
fs = [ String -> Ident
M.packIdent ("arg" String -> ShowS
forall a. [a] -> [a] -> [a]
++ Int -> String
forall a. Show a => a -> String
show (Int
i::Int)) | Int
i <- [ 1 .. ] ]
t :: Type
t = [(Ident, Type)] -> Type
T.TRec ([Ident] -> [Type] -> [(Ident, Type)]
forall a b. [a] -> [b] -> [(a, b)]
zip [Ident]
fs [Type]
tys)
v :: Value
v = [(Ident, Eval Value)] -> Value
forall b w i. [(Ident, Eval (GenValue b w i))] -> GenValue b w i
E.VRecord ([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 (m :: * -> *) a. Monad m => a -> m a
return [Value]
vs))
in Type -> Value -> REPL ()
bindItVariableVal Type
t Value
v
FailError err :: EvalError
err [] -> do
String -> REPL ()
prtLn "ERROR"
Doc -> REPL ()
forall a. Show a => a -> REPL ()
rPrint (EvalError -> Doc
forall a. PP a => a -> Doc
pp EvalError
err)
FailError err :: EvalError
err vs :: [Value]
vs -> do
String -> REPL ()
prtLn "ERROR for the following inputs:"
(Value -> REPL ()) -> [Value] -> REPL ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ (\v :: Value
v -> Doc -> REPL ()
forall a. Show a => a -> REPL ()
rPrint (Doc -> REPL ()) -> REPL Doc -> REPL ()
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< (Eval Doc -> REPL Doc
forall a. Eval a -> REPL a
rEval (Eval Doc -> REPL Doc) -> Eval Doc -> REPL Doc
forall a b. (a -> b) -> a -> b
$ PPOpts -> Value -> Eval Doc
forall b w i. BitWord b w i => PPOpts -> GenValue b w i -> Eval Doc
E.ppValue PPOpts
opts Value
v)) [Value]
vs
Doc -> REPL ()
forall a. Show a => a -> REPL ()
rPrint (EvalError -> Doc
forall a. PP a => a -> Doc
pp EvalError
err)
Pass -> String -> [String] -> REPL ()
forall a. HasCallStack => String -> [String] -> a
panic "Cryptol.REPL.Command" ["unexpected Test.Pass"]
expectedCoverage :: Int -> Integer -> (Double, Double)
expectedCoverage :: Int -> Integer -> (Double, Double)
expectedCoverage testNum :: Int
testNum sz :: Integer
sz =
if Int
testNum Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
> 0 Bool -> Bool -> Bool
&& Double
proportion Double -> Double -> Bool
forall a. Ord a => a -> a -> Bool
> 0 then
(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
(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 = Int -> Double
forall a b. (Integral a, Num b) => a -> b
fromIntegral Int
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 -> REPL ()
satCmd :: String -> REPL ()
satCmd = Bool -> String -> REPL ()
cmdProveSat Bool
True
proveCmd :: String -> REPL ()
proveCmd = Bool -> String -> REPL ()
cmdProveSat Bool
False
showProverStats :: Maybe SBV.Solver -> ProverStats -> REPL ()
showProverStats :: Maybe Solver -> ProverStats -> REPL ()
showProverStats mprover :: Maybe Solver
mprover stat :: ProverStats
stat = String -> REPL ()
rPutStrLn String
msg
where
msg :: String
msg = "(Total Elapsed Time: " String -> ShowS
forall a. [a] -> [a] -> [a]
++ ProverStats -> String
SBV.showTDiff ProverStats
stat String -> ShowS
forall a. [a] -> [a] -> [a]
++
String -> (Solver -> String) -> Maybe Solver -> String
forall b a. b -> (a -> b) -> Maybe a -> b
maybe "" (\p :: Solver
p -> ", using " String -> ShowS
forall a. [a] -> [a] -> [a]
++ Solver -> String
forall a. Show a => a -> String
show Solver
p) Maybe Solver
mprover String -> ShowS
forall a. [a] -> [a] -> [a]
++ ")"
rethrowErrorCall :: REPL a -> REPL a
rethrowErrorCall :: REPL a -> REPL a
rethrowErrorCall m :: REPL a
m = (IORef RW -> IO a) -> REPL a
forall a. (IORef RW -> IO a) -> REPL a
REPL (\r :: 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 -> (ErrorCall -> IO a) -> IO a
forall e a. Exception e => IO a -> (e -> IO a) -> IO a
`X.catch` ErrorCall -> IO a
forall a. ErrorCall -> IO a
handler)
where
handler :: ErrorCall -> IO a
handler (X.ErrorCallWithLocation s :: String
s _) = REPLException -> IO a
forall e a. Exception e => e -> IO a
X.throwIO (String -> REPLException
SBVError String
s)
cmdProveSat :: Bool -> String -> REPL ()
cmdProveSat :: Bool -> String -> REPL ()
cmdProveSat isSat :: Bool
isSat "" =
do (xs :: [Name]
xs,disp :: NameDisp
disp) <- REPL ([Name], NameDisp)
getPropertyNames
let nameStr :: a -> String
nameStr x :: 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] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [Name]
xs
then String -> REPL ()
rPutStrLn "There are no properties in scope."
else [Name] -> (Name -> REPL ()) -> REPL ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
t a -> (a -> m b) -> m ()
forM_ [Name]
xs ((Name -> REPL ()) -> REPL ()) -> (Name -> REPL ()) -> REPL ()
forall a b. (a -> b) -> a -> b
$ \x :: Name
x ->
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
$ ":sat " String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
str String -> ShowS
forall a. [a] -> [a] -> [a]
++ "\n\t"
else String -> REPL ()
rPutStr (String -> REPL ()) -> String -> REPL ()
forall a b. (a -> b) -> a -> b
$ ":prove " String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
str String -> ShowS
forall a. [a] -> [a] -> [a]
++ "\n\t"
Bool -> String -> REPL ()
cmdProveSat Bool
isSat String
str
cmdProveSat isSat :: Bool
isSat str :: String
str = do
let cexStr :: String
cexStr | Bool
isSat = "satisfying assignment"
| Bool
otherwise = "counterexample"
String
proverName <- String -> REPL String
forall a. IsEnvVal a => String -> REPL a
getKnownUser "prover"
String
fileName <- String -> REPL String
forall a. IsEnvVal a => String -> REPL a
getKnownUser "smtfile"
let mfile :: Maybe String
mfile = if String
fileName String -> String -> Bool
forall a. Eq a => a -> a -> Bool
== "-" then Maybe String
forall a. Maybe a
Nothing else String -> Maybe String
forall a. a -> Maybe a
Just String
fileName
case String
proverName :: String of
"offline" -> do
Either String String
result <- Bool -> String -> Maybe String -> REPL (Either String String)
offlineProveSat Bool
isSat String
str Maybe String
mfile
case Either String String
result of
Left msg :: String
msg -> String -> REPL ()
rPutStrLn String
msg
Right smtlib :: String
smtlib -> do
let filename :: String
filename = String -> Maybe String -> String
forall a. a -> Maybe a -> a
fromMaybe "standard output" Maybe String
mfile
let satWord :: String
satWord | Bool
isSat = "satisfiability"
| Bool
otherwise = "validity"
String -> REPL ()
rPutStrLn (String -> REPL ()) -> String -> REPL ()
forall a b. (a -> b) -> a -> b
$
"Writing to SMT-Lib file " String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
filename String -> ShowS
forall a. [a] -> [a] -> [a]
++ "..."
String -> REPL ()
rPutStrLn (String -> REPL ()) -> String -> REPL ()
forall a b. (a -> b) -> a -> b
$
"To determine the " String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
satWord String -> ShowS
forall a. [a] -> [a] -> [a]
++
" of the expression, use an external SMT solver."
case Maybe String
mfile of
Just path :: 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
Nothing -> String -> REPL ()
rPutStr String
smtlib
_ -> do
(firstProver :: Maybe Solver
firstProver,result :: ProverResult
result,stats :: ProverStats
stats) <- REPL (Maybe Solver, ProverResult, ProverStats)
-> REPL (Maybe Solver, ProverResult, ProverStats)
forall a. REPL a -> REPL a
rethrowErrorCall (Bool
-> String
-> Maybe String
-> REPL (Maybe Solver, ProverResult, ProverStats)
onlineProveSat Bool
isSat String
str Maybe String
mfile)
case ProverResult
result of
Symbolic.EmptyResult ->
String -> [String] -> REPL ()
forall a. HasCallStack => String -> [String] -> a
panic "REPL.Command" [ "got EmptyResult for online prover query" ]
Symbolic.ProverError msg :: String
msg -> String -> REPL ()
rPutStrLn String
msg
Symbolic.ThmResult ts :: [Type]
ts -> do
String -> REPL ()
rPutStrLn (if Bool
isSat then "Unsatisfiable" else "Q.E.D.")
(t :: Type
t, e :: Expr
e) <- String -> Bool -> Either [Type] [(Type, Expr)] -> REPL (Type, Expr)
mkSolverResult String
cexStr (Bool -> Bool
not Bool
isSat) ([Type] -> Either [Type] [(Type, Expr)]
forall a b. a -> Either a b
Left [Type]
ts)
Type -> Expr -> REPL ()
bindItVariable Type
t Expr
e
Symbolic.AllSatResult tevss :: [SatResult]
tevss -> do
let tess :: [[(Type, Expr)]]
tess = (SatResult -> [(Type, Expr)]) -> [SatResult] -> [[(Type, Expr)]]
forall a b. (a -> b) -> [a] -> [b]
map (((Type, Expr, Value) -> (Type, Expr))
-> SatResult -> [(Type, Expr)]
forall a b. (a -> b) -> [a] -> [b]
map (((Type, Expr, Value) -> (Type, Expr))
-> SatResult -> [(Type, Expr)])
-> ((Type, Expr, Value) -> (Type, Expr))
-> SatResult
-> [(Type, Expr)]
forall a b. (a -> b) -> a -> b
$ \(t :: Type
t,e :: Expr
e,_) -> (Type
t,Expr
e)) [SatResult]
tevss
vss :: [[Value]]
vss = (SatResult -> [Value]) -> [SatResult] -> [[Value]]
forall a b. (a -> b) -> [a] -> [b]
map (((Type, Expr, Value) -> Value) -> SatResult -> [Value]
forall a b. (a -> b) -> [a] -> [b]
map (((Type, Expr, Value) -> Value) -> SatResult -> [Value])
-> ((Type, Expr, Value) -> Value) -> SatResult -> [Value]
forall a b. (a -> b) -> a -> b
$ \(_,_,v :: Value
v) -> Value
v) [SatResult]
tevss
[(Type, Expr)]
resultRecs <- ([(Type, Expr)] -> REPL (Type, Expr))
-> [[(Type, Expr)]] -> REPL [(Type, Expr)]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM (String -> Bool -> Either [Type] [(Type, Expr)] -> REPL (Type, Expr)
mkSolverResult String
cexStr Bool
isSat (Either [Type] [(Type, Expr)] -> REPL (Type, Expr))
-> ([(Type, Expr)] -> Either [Type] [(Type, Expr)])
-> [(Type, Expr)]
-> REPL (Type, Expr)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [(Type, Expr)] -> Either [Type] [(Type, Expr)]
forall a b. b -> Either a b
Right) [[(Type, Expr)]]
tess
let collectTes :: [(a, b)] -> (a, [b])
collectTes tes :: [(a, b)]
tes = (a
t, [b]
es)
where
(ts :: [a]
ts, es :: [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
[t' :: a
t'] -> a
t'
_ -> String -> [String] -> a
forall a. HasCallStack => String -> [String] -> a
panic "REPL.Command.onlineProveSat"
[ "satisfying assignments with different types" ]
(ty :: Type
ty, exprs :: [Expr]
exprs) =
case [(Type, Expr)]
resultRecs of
[] -> String -> [String] -> (Type, [Expr])
forall a. HasCallStack => String -> [String] -> a
panic "REPL.Command.onlineProveSat"
[ "no satisfying assignments after mkSolverResult" ]
[(t :: Type
t, e :: Expr
e)] -> (Type
t, [Expr
e])
_ -> [(Type, Expr)] -> (Type, [Expr])
forall a b. Eq a => [(a, b)] -> (a, [b])
collectTes [(Type, Expr)]
resultRecs
Expr PName
pexpr <- String -> REPL (Expr PName)
replParseExpr String
str
~(EnvBool yes :: Bool
yes) <- String -> REPL EnvVal
getUser "show-examples"
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 (Bool -> Expr PName -> [Value] -> REPL ()
printCounterexample Bool
isSat Expr PName
pexpr)
case (Type
ty, [Expr]
exprs) of
(t :: Type
t, [e :: Expr
e]) -> Type -> Expr -> REPL ()
bindItVariable Type
t Expr
e
(t :: Type
t, es :: [Expr]
es ) -> Type -> [Expr] -> REPL ()
bindItVariables Type
t [Expr]
es
Bool
seeStats <- REPL Bool
getUserShowProverStats
Bool -> REPL () -> REPL ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when Bool
seeStats (Maybe Solver -> ProverStats -> REPL ()
showProverStats Maybe Solver
firstProver ProverStats
stats)
onlineProveSat :: Bool
-> String -> Maybe FilePath
-> REPL (Maybe SBV.Solver,Symbolic.ProverResult,ProverStats)
onlineProveSat :: Bool
-> String
-> Maybe String
-> REPL (Maybe Solver, ProverResult, ProverStats)
onlineProveSat isSat :: Bool
isSat str :: String
str mfile :: Maybe String
mfile = do
String
proverName <- String -> REPL String
forall a. IsEnvVal a => String -> REPL a
getKnownUser "prover"
Bool
verbose <- String -> REPL Bool
forall a. IsEnvVal a => String -> REPL a
getKnownUser "debug"
SatNum
satNum <- REPL SatNum
getUserSatNum
Bool
modelValidate <- REPL Bool
getUserProverValidate
Expr PName
parseExpr <- String -> REPL (Expr PName)
replParseExpr String
str
(_, expr :: Expr
expr, schema :: 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
[DeclGroup]
decls <- (DynamicEnv -> [DeclGroup]) -> REPL DynamicEnv -> REPL [DeclGroup]
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 0)
let cmd :: ProverCommand
cmd = $WProverCommand :: QueryType
-> String
-> Bool
-> Bool
-> IORef ProverStats
-> [DeclGroup]
-> Maybe String
-> Expr
-> Schema
-> ProverCommand
Symbolic.ProverCommand {
pcQueryType :: QueryType
pcQueryType = if Bool
isSat then SatNum -> QueryType
SatQuery SatNum
satNum else QueryType
ProveQuery
, 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
}
(firstProver :: Maybe Solver
firstProver, res :: ProverResult
res) <- ModuleCmd (Maybe Solver, ProverResult)
-> REPL (Maybe Solver, ProverResult)
forall a. ModuleCmd a -> REPL a
liftModuleCmd (ModuleCmd (Maybe Solver, ProverResult)
-> REPL (Maybe Solver, ProverResult))
-> ModuleCmd (Maybe Solver, ProverResult)
-> REPL (Maybe Solver, ProverResult)
forall a b. (a -> b) -> a -> b
$ ProverCommand -> ModuleCmd (Maybe Solver, ProverResult)
Symbolic.satProve 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 Solver, ProverResult, ProverStats)
-> REPL (Maybe Solver, ProverResult, ProverStats)
forall (m :: * -> *) a. Monad m => a -> m a
return (Maybe Solver
firstProver,ProverResult
res,ProverStats
stas)
offlineProveSat :: Bool -> String -> Maybe FilePath -> REPL (Either String String)
offlineProveSat :: Bool -> String -> Maybe String -> REPL (Either String String)
offlineProveSat isSat :: Bool
isSat str :: String
str mfile :: Maybe String
mfile = do
Bool
verbose <- String -> REPL Bool
forall a. IsEnvVal a => String -> REPL a
getKnownUser "debug"
Bool
modelValidate <- REPL Bool
getUserProverValidate
Expr PName
parseExpr <- String -> REPL (Expr PName)
replParseExpr String
str
(_, expr :: Expr
expr, schema :: Schema
schema) <- Expr PName -> REPL (Expr Name, Expr, Schema)
replCheckExpr Expr PName
parseExpr
[DeclGroup]
decls <- (DynamicEnv -> [DeclGroup]) -> REPL DynamicEnv -> REPL [DeclGroup]
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 0)
let cmd :: ProverCommand
cmd = $WProverCommand :: QueryType
-> String
-> Bool
-> Bool
-> IORef ProverStats
-> [DeclGroup]
-> Maybe String
-> Expr
-> Schema
-> ProverCommand
Symbolic.ProverCommand {
pcQueryType :: QueryType
pcQueryType = if Bool
isSat then SatNum -> QueryType
SatQuery (Int -> SatNum
SomeSat 0) else QueryType
ProveQuery
, pcProverName :: String
pcProverName = "offline"
, 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
}
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
$ ProverCommand -> ModuleCmd (Either String String)
Symbolic.satProveOffline ProverCommand
cmd
rIdent :: M.Ident
rIdent :: Ident
rIdent = String -> Ident
M.packIdent "result"
mkSolverResult :: String
-> Bool
-> Either [T.Type] [(T.Type, T.Expr)]
-> REPL (T.Type, T.Expr)
mkSolverResult :: String -> Bool -> Either [Type] [(Type, Expr)] -> REPL (Type, Expr)
mkSolverResult thing :: String
thing result :: Bool
result earg :: Either [Type] [(Type, Expr)]
earg =
do PrimMap
prims <- REPL PrimMap
getPrimMap
let addError :: Type -> (Type, Expr)
addError t :: Type
t = (Type
t, PrimMap -> Type -> String -> Expr
T.eError PrimMap
prims Type
t ("no " String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
thing String -> ShowS
forall a. [a] -> [a] -> [a]
++ " available"))
argF :: [((Ident, Type), (Ident, Expr))]
argF = case Either [Type] [(Type, Expr)]
earg of
Left ts :: [Type]
ts -> [(Type, Expr)] -> [((Ident, Type), (Ident, Expr))]
forall b b. [(b, b)] -> [((Ident, b), (Ident, b))]
mkArgs ((Type -> (Type, Expr)) -> [Type] -> [(Type, Expr)]
forall a b. (a -> b) -> [a] -> [b]
map Type -> (Type, Expr)
addError [Type]
ts)
Right tes :: [(Type, Expr)]
tes -> [(Type, Expr)] -> [((Ident, Type), (Ident, Expr))]
forall b b. [(b, b)] -> [((Ident, b), (Ident, b))]
mkArgs [(Type, Expr)]
tes
eTrue :: Expr
eTrue = PrimMap -> Ident -> Expr
T.ePrim PrimMap
prims (String -> Ident
M.packIdent "True")
eFalse :: Expr
eFalse = PrimMap -> Ident -> Expr
T.ePrim PrimMap
prims (String -> Ident
M.packIdent "False")
resultE :: Expr
resultE = if Bool
result then Expr
eTrue else Expr
eFalse
rty :: Type
rty = [(Ident, Type)] -> Type
T.TRec ([(Ident, Type)] -> Type) -> [(Ident, Type)] -> Type
forall a b. (a -> b) -> a -> b
$ [(Ident
rIdent, Type
T.tBit )] [(Ident, Type)] -> [(Ident, Type)] -> [(Ident, Type)]
forall a. [a] -> [a] -> [a]
++ (((Ident, Type), (Ident, Expr)) -> (Ident, Type))
-> [((Ident, Type), (Ident, Expr))] -> [(Ident, Type)]
forall a b. (a -> b) -> [a] -> [b]
map ((Ident, Type), (Ident, Expr)) -> (Ident, Type)
forall a b. (a, b) -> a
fst [((Ident, Type), (Ident, Expr))]
argF
re :: Expr
re = [(Ident, Expr)] -> Expr
T.ERec ([(Ident, Expr)] -> Expr) -> [(Ident, Expr)] -> Expr
forall a b. (a -> b) -> a -> b
$ [(Ident
rIdent, Expr
resultE)] [(Ident, Expr)] -> [(Ident, Expr)] -> [(Ident, Expr)]
forall a. [a] -> [a] -> [a]
++ (((Ident, Type), (Ident, Expr)) -> (Ident, Expr))
-> [((Ident, Type), (Ident, Expr))] -> [(Ident, Expr)]
forall a b. (a -> b) -> [a] -> [b]
map ((Ident, Type), (Ident, Expr)) -> (Ident, Expr)
forall a b. (a, b) -> b
snd [((Ident, Type), (Ident, Expr))]
argF
(Type, Expr) -> REPL (Type, Expr)
forall (m :: * -> *) a. Monad m => a -> m a
return (Type
rty, Expr
re)
where
mkArgs :: [(b, b)] -> [((Ident, b), (Ident, b))]
mkArgs tes :: [(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 a b b. Show a => a -> (b, b) -> ((Ident, b), (Ident, b))
mkArg [1 :: Int ..] [(b, b)]
tes
where
mkArg :: a -> (b, b) -> ((Ident, b), (Ident, b))
mkArg n :: a
n (t :: b
t,e :: b
e) =
let argName :: Ident
argName = String -> Ident
M.packIdent ("arg" String -> ShowS
forall a. [a] -> [a] -> [a]
++ a -> String
forall a. Show a => a -> String
show a
n)
in ((Ident
argName,b
t),(Ident
argName,b
e))
specializeCmd :: String -> REPL ()
specializeCmd :: String -> REPL ()
specializeCmd str :: String
str = do
Expr PName
parseExpr <- String -> REPL (Expr PName)
replParseExpr String
str
(_, expr :: Expr
expr, schema :: Schema
schema) <- Expr PName -> REPL (Expr Name, Expr, Schema)
replCheckExpr Expr PName
parseExpr
Expr
spexpr <- Expr -> REPL Expr
replSpecExpr Expr
expr
String -> REPL ()
rPutStrLn "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 "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 "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 -> REPL ()
refEvalCmd :: String -> REPL ()
refEvalCmd str :: String
str = do
Expr PName
parseExpr <- String -> REPL (Expr PName)
replParseExpr String
str
(_, expr :: Expr
expr, schema :: 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
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
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 -> Value -> Doc
R.ppValue PPOpts
opts Value
val
astOfCmd :: String -> REPL ()
astOfCmd :: String -> REPL ()
astOfCmd str :: String
str = do
Expr PName
expr <- String -> REPL (Expr PName)
replParseExpr String
str
(re :: Expr Name
re,_,_) <- 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 (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 -> REPL ()
forall a. Show a => a -> REPL ()
rPrint (Doc -> REPL ()) -> Doc -> REPL ()
forall a b. (a -> b) -> a -> b
$ [DeclGroup] -> Doc
forall t. ShowParseable t => t -> Doc
T.showParseable ([DeclGroup] -> Doc) -> [DeclGroup] -> Doc
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]
T.mDecls ([Module] -> [DeclGroup]) -> [Module] -> [DeclGroup]
forall a b. (a -> b) -> a -> b
$ ModuleEnv -> [Module]
M.loadedModules ModuleEnv
me
typeOfCmd :: String -> REPL ()
typeOfCmd :: String -> REPL ()
typeOfCmd str :: String
str = do
Expr PName
expr <- String -> REPL (Expr PName)
replParseExpr String
str
(_re :: Expr Name
_re,def :: Expr
def,sig :: 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))
(_,_,_,names :: NameDisp
names) <- REPL (IfaceParams, IfaceDecls, NamingEnv, NameDisp)
getFocusedEnv
Doc -> REPL ()
forall a. Show a => a -> REPL ()
rPrint (Doc -> REPL ()) -> Doc -> REPL ()
forall a b. (a -> b) -> a -> b
$ NameDisp -> Doc -> Doc
runDoc NameDisp
names (Doc -> Doc) -> Doc -> Doc
forall a b. (a -> b) -> a -> b
$ Int -> Expr PName -> Doc
forall a. PP a => Int -> a -> Doc
ppPrec 2 Expr PName
expr Doc -> Doc -> Doc
<+> String -> Doc
text ":" Doc -> Doc -> Doc
<+> Schema -> Doc
forall a. PP a => a -> Doc
pp Schema
sig
readFileCmd :: FilePath -> REPL ()
readFileCmd :: String -> REPL ()
readFileCmd fp :: String
fp = do
Maybe ByteString
bytes <- String
-> (SomeException -> REPL (Maybe ByteString))
-> REPL (Maybe ByteString)
replReadFile String
fp (\err :: SomeException
err -> String -> REPL ()
rPutStrLn (SomeException -> String
forall a. Show a => a -> String
show SomeException
err) REPL () -> REPL (Maybe ByteString) -> REPL (Maybe ByteString)
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> Maybe ByteString -> REPL (Maybe ByteString)
forall (m :: * -> *) a. Monad m => a -> m a
return Maybe ByteString
forall a. Maybe a
Nothing)
case Maybe ByteString
bytes of
Nothing -> () -> REPL ()
forall (m :: * -> *) a. Monad m => a -> m a
return ()
Just bs :: ByteString
bs ->
do PrimMap
pm <- REPL PrimMap
getPrimMap
let expr :: Expr
expr = PrimMap -> String -> Expr
T.eString PrimMap
pm ((Word8 -> Char) -> [Word8] -> String
forall a b. (a -> b) -> [a] -> [b]
map (Int -> Char
forall a. Enum a => Int -> a
toEnum (Int -> Char) -> (Word8 -> Int) -> Word8 -> Char
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Word8 -> Int
forall a b. (Integral a, Num b) => a -> b
fromIntegral) (ByteString -> [Word8]
BS.unpack ByteString
bs))
ty :: Type
ty = Int -> Type
T.tString (ByteString -> Int
BS.length ByteString
bs)
Type -> Expr -> REPL ()
bindItVariable Type
ty Expr
expr
writeFileCmd :: FilePath -> String -> REPL ()
writeFileCmd :: String -> String -> REPL ()
writeFileCmd file :: String
file str :: String
str = do
Expr PName
expr <- String -> REPL (Expr PName)
replParseExpr String
str
(val :: Value
val,ty :: 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
$ "Cannot write expression of types other than [n][8]."
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 fp :: String
fp bytes :: 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 x :: 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 x :: Type
x = Bool -> ((Type, Type) -> Bool) -> Maybe (Type, Type) -> Bool
forall b a. b -> (a -> b) -> Maybe a -> b
maybe Bool
False
(\(n :: Type
n,b :: 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 8)
(Type -> Maybe (Type, Type)
T.tIsSeq Type
x)
serializeValue :: Value -> REPL ByteString
serializeValue (E.VSeq n :: Integer
n vs :: SeqMap Bool BV Integer
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)
mapM (Eval Value -> (Value -> Eval BV) -> Eval BV
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>=String -> Value -> Eval BV
forall b w i. BitWord b w i => String -> GenValue b w i -> Eval w
E.fromVWord "serializeValue") ([Eval Value] -> Eval [BV]) -> [Eval Value] -> Eval [BV]
forall a b. (a -> b) -> a -> b
$ Integer -> SeqMap Bool BV Integer -> [Eval Value]
forall n b w i.
Integral n =>
n -> SeqMap b w i -> [Eval (GenValue b w i)]
E.enumerateSeqMap Integer
n SeqMap Bool BV Integer
vs)
ByteString -> REPL ByteString
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 _ =
String -> [String] -> REPL ByteString
forall a. HasCallStack => String -> [String] -> a
panic "Cryptol.REPL.Command.writeFileCmd"
["Impossible: Non-VSeq value of type [n][8]."]
serializeByte :: BV -> b
serializeByte (E.BV _ v :: 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
.&. 0xFF)
rEval :: E.Eval a -> REPL a
rEval :: Eval a -> REPL a
rEval m :: Eval a
m = do EvalOpts
ev <- REPL EvalOpts
getEvalOpts
IO a -> REPL a
forall a. IO a -> REPL a
io (EvalOpts -> Eval a -> IO a
forall a. EvalOpts -> Eval a -> IO a
E.runEval EvalOpts
ev Eval a
m)
rEvalRethrow :: E.Eval a -> REPL a
rEvalRethrow :: Eval a -> REPL a
rEvalRethrow m :: Eval a
m = do EvalOpts
ev <- REPL EvalOpts
getEvalOpts
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
$ EvalOpts -> Eval a -> IO a
forall a. EvalOpts -> Eval a -> IO a
E.runEval EvalOpts
ev Eval a
m
reloadCmd :: REPL ()
reloadCmd :: REPL ()
reloadCmd = do
Maybe LoadedModule
mb <- REPL (Maybe LoadedModule)
getLoadedMod
case Maybe LoadedModule
mb of
Just lm :: LoadedModule
lm ->
case LoadedModule -> Maybe ModName
lName LoadedModule
lm of
Just m :: ModName
m | ModName -> Bool
M.isParamInstModName ModName
m -> ModuleCmd (ModulePath, Module) -> REPL ()
loadHelper (ModName -> ModuleCmd (ModulePath, Module)
M.loadModuleByName ModName
m)
_ -> case LoadedModule -> ModulePath
lPath LoadedModule
lm of
M.InFile f :: String
f -> String -> REPL ()
loadCmd String
f
_ -> () -> REPL ()
forall (m :: * -> *) a. Monad m => a -> m a
return ()
Nothing -> () -> REPL ()
forall (m :: * -> *) a. Monad m => a -> m a
return ()
editCmd :: String -> REPL ()
editCmd :: String -> REPL ()
editCmd path :: String
path =
do Maybe String
mbE <- REPL (Maybe String)
getEditPath
Maybe LoadedModule
mbL <- REPL (Maybe LoadedModule)
getLoadedMod
if Bool -> Bool
not (String -> 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 :: Maybe ModName -> ModulePath -> LoadedModule
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
Nothing -> String -> REPL ()
rPutStrLn "No filed to edit."
Just p :: ModulePath
p ->
case ModulePath
p of
M.InFile f :: String
f -> String -> REPL ()
doEdit String
f
M.InMem l :: String
l bs :: 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 (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> () -> REPL ()
forall (f :: * -> *) a. Applicative f => a -> f a
pure ()
where
doEdit :: String -> REPL ()
doEdit p :: String
p =
do String -> REPL ()
setEditPath String
p
Bool
_ <- String -> REPL Bool
replEdit String
p
REPL ()
reloadCmd
withROTempFile :: String -> ByteString -> (FilePath -> REPL a) -> REPL a
withROTempFile :: String -> ByteString -> (String -> REPL a) -> REPL a
withROTempFile name :: String
name cnt :: ByteString
cnt k :: String -> REPL a
k =
do (path :: String
path,h :: 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 (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 (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 c :: Char
c = if Char -> Bool
isAscii Char
c Bool -> Bool -> Bool
&& Char -> Bool
isAlphaNum Char
c then Char
c else '_'
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]
++ ".cry")
mkFile :: String -> Handle -> m ()
mkFile path :: String
path h :: Handle
h =
IO () -> m ()
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 modString :: String
modString
| String -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null String
modString = () -> REPL ()
forall (m :: * -> *) a. Monad m => a -> m a
return ()
| Bool
otherwise = do
case String -> Maybe ModName
parseModName String
modString of
Just m :: ModName
m -> ModuleCmd (ModulePath, Module) -> REPL ()
loadHelper (ModName -> ModuleCmd (ModulePath, Module)
M.loadModuleByName ModName
m)
Nothing -> String -> REPL ()
rPutStrLn "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 path :: String
path
| String -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null String
path = () -> REPL ()
forall (m :: * -> *) a. Monad m => a -> m a
return ()
| Bool
otherwise = do String -> REPL ()
setEditPath String
path
LoadedModule -> REPL ()
setLoadedMod LoadedModule :: Maybe ModName -> ModulePath -> LoadedModule
LoadedModule { lName :: Maybe ModName
lName = Maybe ModName
forall a. Maybe a
Nothing
, lPath :: ModulePath
lPath = String -> ModulePath
M.InFile String
path
}
ModuleCmd (ModulePath, Module) -> REPL ()
loadHelper (String -> ModuleCmd (ModulePath, Module)
M.loadModuleByPath String
path)
loadHelper :: M.ModuleCmd (M.ModulePath,T.Module) -> REPL ()
loadHelper :: ModuleCmd (ModulePath, Module) -> REPL ()
loadHelper how :: ModuleCmd (ModulePath, Module)
how =
do REPL ()
clearLoadedMod
(path :: ModulePath
path,m :: Module
m) <- ModuleCmd (ModulePath, Module) -> REPL (ModulePath, Module)
forall a. ModuleCmd a -> REPL a
liftModuleCmd ModuleCmd (ModulePath, Module)
how
REPL () -> REPL ()
whenDebug (String -> REPL ()
rPutStrLn (Module -> String
forall a. PP (WithNames a) => a -> String
dump Module
m))
LoadedModule -> REPL ()
setLoadedMod LoadedModule :: Maybe ModName -> ModulePath -> LoadedModule
LoadedModule
{ lName :: Maybe ModName
lName = ModName -> Maybe ModName
forall a. a -> Maybe a
Just (Module -> ModName
T.mName Module
m)
, lPath :: ModulePath
lPath = ModulePath
path
}
case ModulePath
path of
M.InFile f :: String
f -> String -> REPL ()
setEditPath String
f
M.InMem {} -> REPL ()
clearEditPath
DynamicEnv -> REPL ()
setDynEnv DynamicEnv
forall a. Monoid a => a
mempty
quitCmd :: REPL ()
quitCmd :: REPL ()
quitCmd = REPL ()
stop
browseCmd :: String -> REPL ()
browseCmd :: String -> REPL ()
browseCmd input :: String
input = do
(params :: IfaceParams
params, iface :: IfaceDecls
iface, fNames :: NamingEnv
fNames, disp :: NameDisp
disp) <- REPL (IfaceParams, IfaceDecls, NamingEnv, NameDisp)
getFocusedEnv
DynamicEnv
denv <- REPL DynamicEnv
getDynEnv
let names :: NamingEnv
names = DynamicEnv -> NamingEnv
M.deNames DynamicEnv
denv NamingEnv -> NamingEnv -> NamingEnv
`M.shadowing` NamingEnv
fNames
let mnames :: [ModName]
mnames = (String -> ModName) -> [String] -> [ModName]
forall a b. (a -> b) -> [a] -> [b]
map (Text -> ModName
M.textToModName (Text -> ModName) -> (String -> Text) -> String -> ModName
forall b c a. (b -> c) -> (a -> b) -> a -> c
. String -> Text
T.pack) (String -> [String]
words String
input)
[ModName]
validModNames <- (:) ModName
M.interactiveName ([ModName] -> [ModName]) -> REPL [ModName] -> REPL [ModName]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> REPL [ModName]
getModNames
let checkModName :: ModName -> REPL ()
checkModName m :: ModName
m =
Bool -> REPL () -> REPL ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless (ModName
m ModName -> [ModName] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [ModName]
validModNames) (REPL () -> REPL ()) -> REPL () -> REPL ()
forall a b. (a -> b) -> a -> b
$
String -> REPL ()
rPutStrLn ("error: " String -> ShowS
forall a. [a] -> [a] -> [a]
++ ModName -> String
forall a. Show a => a -> String
show ModName
m String -> ShowS
forall a. [a] -> [a] -> [a]
++ " is not a loaded module.")
(ModName -> REPL ()) -> [ModName] -> REPL ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ ModName -> REPL ()
checkModName [ModName]
mnames
let f :: t -> Bool
f &&& :: (t -> Bool) -> (t -> Bool) -> t -> Bool
&&& g :: t -> Bool
g = \x :: t
x -> t -> Bool
f t
x Bool -> Bool -> Bool
&& t -> Bool
g t
x
isUser :: Name -> Bool
isUser x :: Name
x = case Name -> NameInfo
M.nameInfo Name
x of
M.Declared _ M.SystemName -> Bool
False
_ -> Bool
True
inSet :: Set a -> a -> Bool
inSet s :: Set a
s x :: a
x = a
x a -> Set a -> Bool
forall a. Ord a => a -> Set a -> Bool
`Set.member` Set a
s
let (visibleTypes :: Set Name
visibleTypes,visibleDecls :: Set Name
visibleDecls) = NamingEnv -> (Set Name, Set Name)
M.visibleNames NamingEnv
names
restricted :: Name -> Bool
restricted = if [ModName] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [ModName]
mnames then Bool -> Name -> Bool
forall a b. a -> b -> a
const Bool
True else [ModName] -> Name -> Bool
hasAnyModName [ModName]
mnames
visibleType :: Name -> Bool
visibleType = Name -> Bool
isUser (Name -> Bool) -> (Name -> Bool) -> Name -> Bool
forall t. (t -> Bool) -> (t -> Bool) -> t -> Bool
&&& Name -> Bool
restricted (Name -> Bool) -> (Name -> Bool) -> Name -> Bool
forall t. (t -> Bool) -> (t -> Bool) -> t -> Bool
&&& Set Name -> Name -> Bool
forall a. Ord a => Set a -> a -> Bool
inSet Set Name
visibleTypes
visibleDecl :: Name -> Bool
visibleDecl = Name -> Bool
isUser (Name -> Bool) -> (Name -> Bool) -> Name -> Bool
forall t. (t -> Bool) -> (t -> Bool) -> t -> Bool
&&& Name -> Bool
restricted (Name -> Bool) -> (Name -> Bool) -> Name -> Bool
forall t. (t -> Bool) -> (t -> Bool) -> t -> Bool
&&& Set Name -> Name -> Bool
forall a. Ord a => Set a -> a -> Bool
inSet Set Name
visibleDecls
(Name -> Bool)
-> (Name -> Bool) -> IfaceParams -> NameDisp -> REPL ()
browseMParams Name -> Bool
visibleType Name -> Bool
visibleDecl IfaceParams
params NameDisp
disp
(Name -> Bool) -> IfaceDecls -> NameDisp -> REPL ()
browseTSyns Name -> Bool
visibleType IfaceDecls
iface NameDisp
disp
(Name -> Bool) -> IfaceDecls -> NameDisp -> REPL ()
browsePrimTys Name -> Bool
visibleType IfaceDecls
iface NameDisp
disp
(Name -> Bool) -> IfaceDecls -> NameDisp -> REPL ()
browseNewtypes Name -> Bool
visibleType IfaceDecls
iface NameDisp
disp
(Name -> Bool) -> IfaceDecls -> NameDisp -> REPL ()
browseVars Name -> Bool
visibleDecl IfaceDecls
iface NameDisp
disp
browseMParams :: (M.Name -> Bool) -> (M.Name -> Bool) ->
M.IfaceParams-> NameDisp -> REPL ()
browseMParams :: (Name -> Bool)
-> (Name -> Bool) -> IfaceParams -> NameDisp -> REPL ()
browseMParams visT :: Name -> Bool
visT visD :: Name -> Bool
visD M.IfaceParams { .. } names :: NameDisp
names =
do NameDisp -> (ModTParam -> Doc) -> String -> [ModTParam] -> REPL ()
forall a. NameDisp -> (a -> Doc) -> String -> [a] -> REPL ()
ppBlock NameDisp
names ModTParam -> Doc
ppParamTy "Type Parameters"
((Name -> Bool)
-> (ModTParam -> Name) -> Map Name ModTParam -> [ModTParam]
forall a k. (Name -> Bool) -> (a -> Name) -> Map k a -> [a]
sorted Name -> Bool
visT ModTParam -> Name
T.mtpName Map Name ModTParam
ifParamTypes)
NameDisp -> (ModVParam -> Doc) -> String -> [ModVParam] -> REPL ()
forall a. NameDisp -> (a -> Doc) -> String -> [a] -> REPL ()
ppBlock NameDisp
names ModVParam -> Doc
ppParamFu "Value Parameters"
((Name -> Bool)
-> (ModVParam -> Name) -> Map Name ModVParam -> [ModVParam]
forall a k. (Name -> Bool) -> (a -> Name) -> Map k a -> [a]
sorted Name -> Bool
visD ModVParam -> Name
T.mvpName Map Name ModVParam
ifParamFuns)
where
ppParamTy :: ModTParam -> Doc
ppParamTy T.ModTParam { .. } = Doc -> Int -> Doc -> Doc
hang ("type" Doc -> Doc -> Doc
<+> Name -> Doc
forall a. PP a => a -> Doc
pp Name
mtpName Doc -> Doc -> Doc
<+> ":")
2 (Kind -> Doc
forall a. PP a => a -> Doc
pp Kind
mtpKind)
ppParamFu :: ModVParam -> Doc
ppParamFu T.ModVParam { .. } = Doc -> Int -> Doc -> Doc
hang (Name -> Doc
forall a. PP a => a -> Doc
pp Name
mvpName Doc -> Doc -> Doc
<+> ":") 2 (Schema -> Doc
forall a. PP a => a -> Doc
pp Schema
mvpType)
sorted :: (Name -> Bool) -> (a -> Name) -> Map k a -> [a]
sorted vis :: Name -> Bool
vis nm :: a -> Name
nm mp :: Map k a
mp = (a -> a -> Ordering) -> [a] -> [a]
forall a. (a -> a -> Ordering) -> [a] -> [a]
sortBy (NameDisp -> Name -> Name -> Ordering
M.cmpNameDisplay NameDisp
names (Name -> Name -> Ordering) -> (a -> Name) -> a -> a -> Ordering
forall b c a. (b -> b -> c) -> (a -> b) -> a -> a -> c
`on` a -> Name
nm)
([a] -> [a]) -> [a] -> [a]
forall a b. (a -> b) -> a -> b
$ (a -> Bool) -> [a] -> [a]
forall a. (a -> Bool) -> [a] -> [a]
filter (Name -> Bool
vis (Name -> Bool) -> (a -> Name) -> a -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. a -> Name
nm) ([a] -> [a]) -> [a] -> [a]
forall a b. (a -> b) -> a -> b
$ Map k a -> [a]
forall k a. Map k a -> [a]
Map.elems Map k a
mp
browsePrimTys :: (M.Name -> Bool) -> M.IfaceDecls -> NameDisp -> REPL ()
browsePrimTys :: (Name -> Bool) -> IfaceDecls -> NameDisp -> REPL ()
browsePrimTys isVisible :: Name -> Bool
isVisible M.IfaceDecls { .. } names :: NameDisp
names =
do let pts :: [IfaceAbstractType]
pts = (IfaceAbstractType -> IfaceAbstractType -> Ordering)
-> [IfaceAbstractType] -> [IfaceAbstractType]
forall a. (a -> a -> Ordering) -> [a] -> [a]
sortBy (NameDisp -> Name -> Name -> Ordering
M.cmpNameDisplay NameDisp
names (Name -> Name -> Ordering)
-> (IfaceAbstractType -> Name)
-> IfaceAbstractType
-> IfaceAbstractType
-> Ordering
forall b c a. (b -> b -> c) -> (a -> b) -> a -> a -> c
`on` IfaceAbstractType -> Name
T.atName)
[ IfaceAbstractType
ts | IfaceAbstractType
ts <- Map Name IfaceAbstractType -> [IfaceAbstractType]
forall k a. Map k a -> [a]
Map.elems Map Name IfaceAbstractType
ifAbstractTypes, Name -> Bool
isVisible (IfaceAbstractType -> Name
T.atName IfaceAbstractType
ts) ]
NameDisp
-> (IfaceAbstractType -> Doc)
-> String
-> [IfaceAbstractType]
-> REPL ()
forall a. NameDisp -> (a -> Doc) -> String -> [a] -> REPL ()
ppBlock NameDisp
names IfaceAbstractType -> Doc
ppA "Primitive Types" [IfaceAbstractType]
pts
where
ppA :: IfaceAbstractType -> Doc
ppA a :: IfaceAbstractType
a = Name -> Doc
forall a. PP a => a -> Doc
pp (IfaceAbstractType -> Name
T.atName IfaceAbstractType
a) Doc -> Doc -> Doc
<+> ":" Doc -> Doc -> Doc
<+> Kind -> Doc
forall a. PP a => a -> Doc
pp (IfaceAbstractType -> Kind
T.atKind IfaceAbstractType
a)
browseTSyns :: (M.Name -> Bool) -> M.IfaceDecls -> NameDisp -> REPL ()
browseTSyns :: (Name -> Bool) -> IfaceDecls -> NameDisp -> REPL ()
browseTSyns isVisible :: Name -> Bool
isVisible M.IfaceDecls { .. } names :: NameDisp
names = do
let tsyns :: [IfaceTySyn]
tsyns = (IfaceTySyn -> IfaceTySyn -> Ordering)
-> [IfaceTySyn] -> [IfaceTySyn]
forall a. (a -> a -> Ordering) -> [a] -> [a]
sortBy (NameDisp -> Name -> Name -> Ordering
M.cmpNameDisplay NameDisp
names (Name -> Name -> Ordering)
-> (IfaceTySyn -> Name) -> IfaceTySyn -> IfaceTySyn -> Ordering
forall b c a. (b -> b -> c) -> (a -> b) -> a -> a -> c
`on` IfaceTySyn -> Name
T.tsName)
[ IfaceTySyn
ts | IfaceTySyn
ts <- Map Name IfaceTySyn -> [IfaceTySyn]
forall k a. Map k a -> [a]
Map.elems Map Name IfaceTySyn
ifTySyns, Name -> Bool
isVisible (IfaceTySyn -> Name
T.tsName IfaceTySyn
ts) ]
(cts :: [IfaceTySyn]
cts,tss :: [IfaceTySyn]
tss) = (IfaceTySyn -> Bool)
-> [IfaceTySyn] -> ([IfaceTySyn], [IfaceTySyn])
forall a. (a -> Bool) -> [a] -> ([a], [a])
partition IfaceTySyn -> Bool
isCtrait [IfaceTySyn]
tsyns
NameDisp
-> (IfaceTySyn -> Doc) -> String -> [IfaceTySyn] -> REPL ()
forall a. NameDisp -> (a -> Doc) -> String -> [a] -> REPL ()
ppBlock NameDisp
names IfaceTySyn -> Doc
forall a. PP a => a -> Doc
pp "Type Synonyms" [IfaceTySyn]
tss
NameDisp
-> (IfaceTySyn -> Doc) -> String -> [IfaceTySyn] -> REPL ()
forall a. NameDisp -> (a -> Doc) -> String -> [a] -> REPL ()
ppBlock NameDisp
names IfaceTySyn -> Doc
forall a. PP a => a -> Doc
pp "Constraint Synonyms" [IfaceTySyn]
cts
where
isCtrait :: IfaceTySyn -> Bool
isCtrait t :: IfaceTySyn
t = Kind -> Kind
T.kindResult (Type -> Kind
forall t. HasKind t => t -> Kind
T.kindOf (IfaceTySyn -> Type
T.tsDef IfaceTySyn
t)) Kind -> Kind -> Bool
forall a. Eq a => a -> a -> Bool
== Kind
T.KProp
browseNewtypes :: (M.Name -> Bool) -> M.IfaceDecls -> NameDisp -> REPL ()
browseNewtypes :: (Name -> Bool) -> IfaceDecls -> NameDisp -> REPL ()
browseNewtypes isVisible :: Name -> Bool
isVisible M.IfaceDecls { .. } names :: NameDisp
names = do
let nts :: [IfaceNewtype]
nts = (IfaceNewtype -> IfaceNewtype -> Ordering)
-> [IfaceNewtype] -> [IfaceNewtype]
forall a. (a -> a -> Ordering) -> [a] -> [a]
sortBy (NameDisp -> Name -> Name -> Ordering
M.cmpNameDisplay NameDisp
names (Name -> Name -> Ordering)
-> (IfaceNewtype -> Name)
-> IfaceNewtype
-> IfaceNewtype
-> Ordering
forall b c a. (b -> b -> c) -> (a -> b) -> a -> a -> c
`on` IfaceNewtype -> Name
T.ntName)
[ IfaceNewtype
nt | IfaceNewtype
nt <- Map Name IfaceNewtype -> [IfaceNewtype]
forall k a. Map k a -> [a]
Map.elems Map Name IfaceNewtype
ifNewtypes, Name -> Bool
isVisible (IfaceNewtype -> Name
T.ntName IfaceNewtype
nt) ]
Bool -> REPL () -> REPL ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless ([IfaceNewtype] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [IfaceNewtype]
nts) (REPL () -> REPL ()) -> REPL () -> REPL ()
forall a b. (a -> b) -> a -> b
$ do
String -> REPL ()
rPutStrLn "Newtypes"
String -> REPL ()
rPutStrLn "========"
Doc -> REPL ()
forall a. Show a => a -> REPL ()
rPrint (NameDisp -> Doc -> Doc
runDoc NameDisp
names (Int -> Doc -> Doc
nest 4 ([Doc] -> Doc
vcat ((IfaceNewtype -> Doc) -> [IfaceNewtype] -> [Doc]
forall a b. (a -> b) -> [a] -> [b]
map IfaceNewtype -> Doc
T.ppNewtypeShort [IfaceNewtype]
nts))))
String -> REPL ()
rPutStrLn ""
browseVars :: (M.Name -> Bool) -> M.IfaceDecls -> NameDisp -> REPL ()
browseVars :: (Name -> Bool) -> IfaceDecls -> NameDisp -> REPL ()
browseVars isVisible :: Name -> Bool
isVisible M.IfaceDecls { .. } names :: NameDisp
names = do
let vars :: [IfaceDecl]
vars = (IfaceDecl -> IfaceDecl -> Ordering) -> [IfaceDecl] -> [IfaceDecl]
forall a. (a -> a -> Ordering) -> [a] -> [a]
sortBy (NameDisp -> Name -> Name -> Ordering
M.cmpNameDisplay NameDisp
names (Name -> Name -> Ordering)
-> (IfaceDecl -> Name) -> IfaceDecl -> IfaceDecl -> Ordering
forall b c a. (b -> b -> c) -> (a -> b) -> a -> a -> c
`on` IfaceDecl -> Name
M.ifDeclName)
[ IfaceDecl
d | IfaceDecl
d <- Map Name IfaceDecl -> [IfaceDecl]
forall k a. Map k a -> [a]
Map.elems Map Name IfaceDecl
ifDecls, Name -> Bool
isVisible (IfaceDecl -> Name
M.ifDeclName IfaceDecl
d) ]
let isProp :: IfaceDecl -> Bool
isProp p :: IfaceDecl
p = Pragma
T.PragmaProperty Pragma -> [Pragma] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` (IfaceDecl -> [Pragma]
M.ifDeclPragmas IfaceDecl
p)
(props :: [IfaceDecl]
props,syms :: [IfaceDecl]
syms) = (IfaceDecl -> Bool) -> [IfaceDecl] -> ([IfaceDecl], [IfaceDecl])
forall a. (a -> Bool) -> [a] -> ([a], [a])
partition IfaceDecl -> Bool
isProp [IfaceDecl]
vars
let ppVar :: IfaceDecl -> Doc
ppVar M.IfaceDecl { .. } = Doc -> Int -> Doc -> Doc
hang (Name -> Doc
forall a. PP a => a -> Doc
pp Name
ifDeclName Doc -> Doc -> Doc
<+> Char -> Doc
char ':')
2 (Schema -> Doc
forall a. PP a => a -> Doc
pp Schema
ifDeclSig)
NameDisp -> (IfaceDecl -> Doc) -> String -> [IfaceDecl] -> REPL ()
forall a. NameDisp -> (a -> Doc) -> String -> [a] -> REPL ()
ppBlock NameDisp
names IfaceDecl -> Doc
ppVar "Properties" [IfaceDecl]
props
NameDisp -> (IfaceDecl -> Doc) -> String -> [IfaceDecl] -> REPL ()
forall a. NameDisp -> (a -> Doc) -> String -> [a] -> REPL ()
ppBlock NameDisp
names IfaceDecl -> Doc
ppVar "Symbols" [IfaceDecl]
syms
ppBlock :: NameDisp -> (a -> Doc) -> String -> [a] -> REPL ()
ppBlock :: NameDisp -> (a -> Doc) -> String -> [a] -> REPL ()
ppBlock names :: NameDisp
names ppFun :: a -> Doc
ppFun name :: String
name xs :: [a]
xs = Bool -> REPL () -> REPL ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless ([a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [a]
xs) (REPL () -> REPL ()) -> REPL () -> REPL ()
forall a b. (a -> b) -> a -> b
$
do String -> REPL ()
rPutStrLn String
name
String -> REPL ()
rPutStrLn (Int -> Char -> String
forall a. Int -> a -> [a]
replicate (String -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length String
name) '=')
Doc -> REPL ()
forall a. Show a => a -> REPL ()
rPrint (NameDisp -> Doc -> Doc
runDoc NameDisp
names (Int -> Doc -> Doc
nest 4 ([Doc] -> Doc
vcat ((a -> Doc) -> [a] -> [Doc]
forall a b. (a -> b) -> [a] -> [b]
map a -> Doc
ppFun [a]
xs))))
String -> REPL ()
rPutStrLn ""
setOptionCmd :: String -> REPL ()
setOptionCmd :: String -> REPL ()
setOptionCmd str :: String
str
| Just value :: String
value <- Maybe String
mbValue = String -> String -> REPL ()
setUser String
key String
value
| String -> 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
(before :: String
before,after :: 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
== '=') String
str
key :: String
key = ShowS
trim String
before
mbValue :: Maybe String
mbValue = case String
after of
_ : stuff :: String
stuff -> String -> Maybe String
forall a. a -> Maybe a
Just (ShowS
trim String
stuff)
_ -> Maybe String
forall a. Maybe a
Nothing
describe :: String -> REPL ()
describe k :: String
k = do
Maybe EnvVal
ev <- String -> REPL (Maybe EnvVal)
tryGetUser String
k
case Maybe EnvVal
ev of
Just v :: EnvVal
v -> String -> REPL ()
rPutStrLn (String
k String -> ShowS
forall a. [a] -> [a] -> [a]
++ " = " String -> ShowS
forall a. [a] -> [a] -> [a]
++ EnvVal -> String
showEnvVal EnvVal
v)
Nothing -> do String -> REPL ()
rPutStrLn ("Unknown user option: `" String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
k String -> ShowS
forall a. [a] -> [a] -> [a]
++ "`")
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 (k1 :: String
k1, k2 :: String
k2) = (Char -> Bool) -> String -> (String, String)
forall a. (a -> Bool) -> [a] -> ([a], [a])
break Char -> Bool
isSpace String
k
String -> REPL ()
rPutStrLn ("Did you mean: `:set " String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
k1 String -> ShowS
forall a. [a] -> [a] -> [a]
++ " =" String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
k2 String -> ShowS
forall a. [a] -> [a] -> [a]
++ "`?")
showEnvVal :: EnvVal -> String
showEnvVal :: EnvVal -> String
showEnvVal ev :: EnvVal
ev =
case EnvVal
ev of
EnvString s :: String
s -> String
s
EnvProg p :: String
p as :: [String]
as -> String -> [String] -> String
forall a. [a] -> [[a]] -> [a]
intercalate " " (String
pString -> [String] -> [String]
forall a. a -> [a] -> [a]
:[String]
as)
EnvNum n :: Int
n -> Int -> String
forall a. Show a => a -> String
show Int
n
EnvBool True -> "on"
EnvBool False -> "off"
helpCmd :: String -> REPL ()
helpCmd :: String -> REPL ()
helpCmd cmd :: String
cmd
| String -> 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)
| cmd0 :: String
cmd0 : args :: [String]
args <- String -> [String]
words String
cmd, ":" 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
$ Command -> REPL CommandExitCode
runCommand (String -> Command
Unknown String
cmd0)
[c :: CommandDescr
c] -> CommandDescr -> [String] -> REPL ()
showCmdHelp CommandDescr
c [String]
args
cs :: [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
$ Command -> REPL CommandExitCode
runCommand (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 qname :: PName
qname ->
do (params :: IfaceParams
params,env :: IfaceDecls
env,rnEnv :: NamingEnv
rnEnv,nameEnv :: NameDisp
nameEnv) <- REPL (IfaceParams, IfaceDecls, NamingEnv, NameDisp)
getFocusedEnv
let vNames :: [Name]
vNames = PName -> NamingEnv -> [Name]
M.lookupValNames PName
qname NamingEnv
rnEnv
tNames :: [Name]
tNames = PName -> NamingEnv -> [Name]
M.lookupTypeNames PName
qname NamingEnv
rnEnv
let helps :: [REPL ()]
helps = (Name -> REPL ()) -> [Name] -> [REPL ()]
forall a b. (a -> b) -> [a] -> [b]
map (IfaceParams -> IfaceDecls -> NameDisp -> Name -> REPL ()
showTypeHelp IfaceParams
params IfaceDecls
env NameDisp
nameEnv) [Name]
tNames [REPL ()] -> [REPL ()] -> [REPL ()]
forall a. [a] -> [a] -> [a]
++
(Name -> REPL ()) -> [Name] -> [REPL ()]
forall a b. (a -> b) -> [a] -> [b]
map (IfaceParams -> IfaceDecls -> NameDisp -> PName -> Name -> REPL ()
forall a.
PP a =>
IfaceParams -> IfaceDecls -> NameDisp -> a -> Name -> REPL ()
showValHelp IfaceParams
params IfaceDecls
env NameDisp
nameEnv PName
qname) [Name]
vNames
separ :: REPL ()
separ = String -> REPL ()
rPutStrLn " ~~~ * ~~~"
[REPL ()] -> REPL ()
forall (t :: * -> *) (m :: * -> *) a.
(Foldable t, Monad m) =>
t (m a) -> m ()
sequence_ (REPL () -> [REPL ()] -> [REPL ()]
forall a. a -> [a] -> [a]
intersperse REPL ()
separ [REPL ()]
helps)
Bool -> REPL () -> REPL ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when ([Name] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null ([Name]
vNames [Name] -> [Name] -> [Name]
forall a. [a] -> [a] -> [a]
++ [Name]
tNames)) (REPL () -> REPL ()) -> REPL () -> REPL ()
forall a b. (a -> b) -> a -> b
$
Doc -> REPL ()
forall a. Show a => a -> REPL ()
rPrint (Doc -> REPL ()) -> Doc -> REPL ()
forall a b. (a -> b) -> a -> b
$ "Undefined name:" Doc -> Doc -> Doc
<+> PName -> Doc
forall a. PP a => a -> Doc
pp PName
qname
Nothing ->
String -> REPL ()
rPutStrLn ("Unable to parse name: " String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
cmd)
where
noInfo :: NameDisp -> Name -> REPL ()
noInfo nameEnv :: NameDisp
nameEnv name :: Name
name =
case Name -> NameInfo
M.nameInfo Name
name of
M.Declared m :: ModName
m _ ->
Doc -> REPL ()
forall a. Show a => a -> REPL ()
rPrint (Doc -> REPL ()) -> Doc -> REPL ()
forall a b. (a -> b) -> a -> b
$NameDisp -> Doc -> Doc
runDoc NameDisp
nameEnv ("Name defined in module" Doc -> Doc -> Doc
<+> ModName -> Doc
forall a. PP a => a -> Doc
pp ModName
m)
M.Parameter -> String -> REPL ()
rPutStrLn "// No documentation is available."
showTypeHelp :: IfaceParams -> IfaceDecls -> NameDisp -> Name -> REPL ()
showTypeHelp params :: IfaceParams
params env :: IfaceDecls
env nameEnv :: NameDisp
nameEnv name :: Name
name =
REPL () -> Maybe (REPL ()) -> REPL ()
forall a. a -> Maybe a -> a
fromMaybe (NameDisp -> Name -> REPL ()
noInfo NameDisp
nameEnv Name
name) (Maybe (REPL ()) -> REPL ()) -> Maybe (REPL ()) -> REPL ()
forall a b. (a -> b) -> a -> b
$
[Maybe (REPL ())] -> Maybe (REPL ())
forall (t :: * -> *) (m :: * -> *) a.
(Foldable t, MonadPlus m) =>
t (m a) -> m a
msum [ Maybe (REPL ())
fromTySyn, Maybe (REPL ())
fromPrimType, Maybe (REPL ())
fromNewtype, Maybe (REPL ())
fromTyParam ]
where
fromTySyn :: Maybe (REPL ())
fromTySyn =
do IfaceTySyn
ts <- Name -> Map Name IfaceTySyn -> Maybe IfaceTySyn
forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup Name
name (IfaceDecls -> Map Name IfaceTySyn
M.ifTySyns IfaceDecls
env)
REPL () -> Maybe (REPL ())
forall (m :: * -> *) a. Monad m => a -> m a
return (NameDisp -> Doc -> Maybe String -> REPL ()
doShowTyHelp NameDisp
nameEnv (IfaceTySyn -> Doc
forall a. PP a => a -> Doc
pp IfaceTySyn
ts) (IfaceTySyn -> Maybe String
T.tsDoc IfaceTySyn
ts))
fromNewtype :: Maybe (REPL ())
fromNewtype =
do IfaceNewtype
nt <- Name -> Map Name IfaceNewtype -> Maybe IfaceNewtype
forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup Name
name (IfaceDecls -> Map Name IfaceNewtype
M.ifNewtypes IfaceDecls
env)
let decl :: Doc
decl = IfaceNewtype -> Doc
forall a. PP a => a -> Doc
pp IfaceNewtype
nt Doc -> Doc -> Doc
$$ (Name -> Doc
forall a. PP a => a -> Doc
pp Name
name Doc -> Doc -> Doc
<+> String -> Doc
text ":" Doc -> Doc -> Doc
<+> Schema -> Doc
forall a. PP a => a -> Doc
pp (IfaceNewtype -> Schema
T.newtypeConType IfaceNewtype
nt))
REPL () -> Maybe (REPL ())
forall (m :: * -> *) a. Monad m => a -> m a
return (REPL () -> Maybe (REPL ())) -> REPL () -> Maybe (REPL ())
forall a b. (a -> b) -> a -> b
$ NameDisp -> Doc -> Maybe String -> REPL ()
doShowTyHelp NameDisp
nameEnv Doc
decl (IfaceNewtype -> Maybe String
T.ntDoc IfaceNewtype
nt)
fromPrimType :: Maybe (REPL ())
fromPrimType =
do IfaceAbstractType
a <- Name -> Map Name IfaceAbstractType -> Maybe IfaceAbstractType
forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup Name
name (IfaceDecls -> Map Name IfaceAbstractType
M.ifAbstractTypes IfaceDecls
env)
REPL () -> Maybe (REPL ())
forall (f :: * -> *) a. Applicative f => a -> f a
pure (REPL () -> Maybe (REPL ())) -> REPL () -> Maybe (REPL ())
forall a b. (a -> b) -> a -> b
$ do String -> REPL ()
rPutStrLn ""
Doc -> REPL ()
forall a. Show a => a -> REPL ()
rPrint (Doc -> REPL ()) -> Doc -> REPL ()
forall a b. (a -> b) -> a -> b
$ NameDisp -> Doc -> Doc
runDoc NameDisp
nameEnv (Doc -> Doc) -> Doc -> Doc
forall a b. (a -> b) -> a -> b
$ Int -> Doc -> Doc
nest 4
(Doc -> Doc) -> Doc -> Doc
forall a b. (a -> b) -> a -> b
$ "primitive type" Doc -> Doc -> Doc
<+> Name -> Doc
forall a. PP a => a -> Doc
pp (IfaceAbstractType -> Name
T.atName IfaceAbstractType
a)
Doc -> Doc -> Doc
<+> ":" Doc -> Doc -> Doc
<+> Kind -> Doc
forall a. PP a => a -> Doc
pp (IfaceAbstractType -> Kind
T.atKind IfaceAbstractType
a)
let (vs :: [TParam]
vs,cs :: [Type]
cs) = IfaceAbstractType -> ([TParam], [Type])
T.atCtrs IfaceAbstractType
a
Bool -> REPL () -> REPL ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless ([Type] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [Type]
cs) (REPL () -> REPL ()) -> REPL () -> REPL ()
forall a b. (a -> b) -> a -> b
$
do let example :: Type
example = TCon -> [Type] -> Type
T.TCon (IfaceAbstractType -> TCon
T.abstractTypeTC IfaceAbstractType
a)
((TParam -> Type) -> [TParam] -> [Type]
forall a b. (a -> b) -> [a] -> [b]
map (TVar -> Type
T.TVar (TVar -> Type) -> (TParam -> TVar) -> TParam -> Type
forall b c a. (b -> c) -> (a -> b) -> a -> c
. TParam -> TVar
T.tpVar) [TParam]
vs)
ns :: NameMap
ns = [TParam] -> NameMap -> NameMap
T.addTNames [TParam]
vs NameMap
emptyNameMap
rs :: [Doc]
rs = [ "•" Doc -> Doc -> Doc
<+> NameMap -> Type -> Doc
forall a. PP (WithNames a) => NameMap -> a -> Doc
ppWithNames NameMap
ns Type
c | Type
c <- [Type]
cs ]
String -> REPL ()
rPutStrLn ""
Doc -> REPL ()
forall a. Show a => a -> REPL ()
rPrint (Doc -> REPL ()) -> Doc -> REPL ()
forall a b. (a -> b) -> a -> b
$ NameDisp -> Doc -> Doc
runDoc NameDisp
nameEnv (Doc -> Doc) -> Doc -> Doc
forall a b. (a -> b) -> a -> b
$ Int -> Doc -> Doc
nest 4 (Doc -> Doc) -> Doc -> Doc
forall a b. (a -> b) -> a -> b
$
Doc -> Doc
backticks (NameMap -> Type -> Doc
forall a. PP (WithNames a) => NameMap -> a -> Doc
ppWithNames NameMap
ns Type
example) Doc -> Doc -> Doc
<+>
"requires:" Doc -> Doc -> Doc
$$ Int -> Doc -> Doc
nest 2 ([Doc] -> Doc
vcat [Doc]
rs)
Maybe Fixity -> REPL ()
doShowFix (IfaceAbstractType -> Maybe Fixity
T.atFixitiy IfaceAbstractType
a)
case IfaceAbstractType -> Maybe String
T.atDoc IfaceAbstractType
a of
Nothing -> () -> REPL ()
forall (f :: * -> *) a. Applicative f => a -> f a
pure ()
Just d :: String
d -> do String -> REPL ()
rPutStrLn ""
String -> REPL ()
rPutStrLn String
d
fromTyParam :: Maybe (REPL ())
fromTyParam =
do ModTParam
p <- Name -> Map Name ModTParam -> Maybe ModTParam
forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup Name
name (IfaceParams -> Map Name ModTParam
M.ifParamTypes IfaceParams
params)
let uses :: t -> Bool
uses c :: t
c = TParam -> TVar
T.TVBound (ModTParam -> TParam
T.mtpParam ModTParam
p) TVar -> Set TVar -> Bool
forall a. Ord a => a -> Set a -> Bool
`Set.member` t -> Set TVar
forall t. FVS t => t -> Set TVar
T.fvs t
c
ctrs :: [Type]
ctrs = (Type -> Bool) -> [Type] -> [Type]
forall a. (a -> Bool) -> [a] -> [a]
filter Type -> Bool
forall t. FVS t => t -> Bool
uses ((Located Type -> Type) -> [Located Type] -> [Type]
forall a b. (a -> b) -> [a] -> [b]
map Located Type -> Type
forall a. Located a -> a
P.thing (IfaceParams -> [Located Type]
M.ifParamConstraints IfaceParams
params))
ctrDoc :: Doc
ctrDoc = case [Type]
ctrs of
[] -> Doc
empty
[x :: Type
x] -> Type -> Doc
forall a. PP a => a -> Doc
pp Type
x
xs :: [Type]
xs -> Doc -> Doc
parens (Doc -> Doc) -> Doc -> Doc
forall a b. (a -> b) -> a -> b
$ [Doc] -> Doc
hsep ([Doc] -> Doc) -> [Doc] -> Doc
forall a b. (a -> b) -> a -> b
$ Doc -> [Doc] -> [Doc]
punctuate Doc
comma ([Doc] -> [Doc]) -> [Doc] -> [Doc]
forall a b. (a -> b) -> a -> b
$ (Type -> Doc) -> [Type] -> [Doc]
forall a b. (a -> b) -> [a] -> [b]
map Type -> Doc
forall a. PP a => a -> Doc
pp [Type]
xs
decl :: Doc
decl = String -> Doc
text "parameter" Doc -> Doc -> Doc
<+> Name -> Doc
forall a. PP a => a -> Doc
pp Name
name Doc -> Doc -> Doc
<+> String -> Doc
text ":"
Doc -> Doc -> Doc
<+> Kind -> Doc
forall a. PP a => a -> Doc
pp (ModTParam -> Kind
T.mtpKind ModTParam
p)
Doc -> Doc -> Doc
$$ Doc
ctrDoc
REPL () -> Maybe (REPL ())
forall (m :: * -> *) a. Monad m => a -> m a
return (REPL () -> Maybe (REPL ())) -> REPL () -> Maybe (REPL ())
forall a b. (a -> b) -> a -> b
$ NameDisp -> Doc -> Maybe String -> REPL ()
doShowTyHelp NameDisp
nameEnv Doc
decl (ModTParam -> Maybe String
T.mtpDoc ModTParam
p)
doShowTyHelp :: NameDisp -> Doc -> Maybe String -> REPL ()
doShowTyHelp nameEnv :: NameDisp
nameEnv decl :: Doc
decl doc :: Maybe String
doc =
do String -> REPL ()
rPutStrLn ""
Doc -> REPL ()
forall a. Show a => a -> REPL ()
rPrint (NameDisp -> Doc -> Doc
runDoc NameDisp
nameEnv (Int -> Doc -> Doc
nest 4 Doc
decl))
case Maybe String
doc of
Nothing -> () -> REPL ()
forall (m :: * -> *) a. Monad m => a -> m a
return ()
Just d :: String
d -> String -> REPL ()
rPutStrLn "" REPL () -> REPL () -> REPL ()
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> String -> REPL ()
rPutStrLn String
d
doShowFix :: Maybe Fixity -> REPL ()
doShowFix fx :: Maybe Fixity
fx =
case Maybe Fixity
fx of
Just f :: Fixity
f ->
let msg :: String
msg = "Precedence " String -> ShowS
forall a. [a] -> [a] -> [a]
++ Int -> String
forall a. Show a => a -> String
show (Fixity -> Int
P.fLevel Fixity
f) String -> ShowS
forall a. [a] -> [a] -> [a]
++ ", " String -> ShowS
forall a. [a] -> [a] -> [a]
++
(case Fixity -> Assoc
P.fAssoc Fixity
f of
P.LeftAssoc -> "associates to the left."
P.RightAssoc -> "associates to the right."
P.NonAssoc -> "does not associate.")
in String -> REPL ()
rPutStrLn ('\n' Char -> ShowS
forall a. a -> [a] -> [a]
: String
msg)
Nothing -> () -> REPL ()
forall (m :: * -> *) a. Monad m => a -> m a
return ()
showValHelp :: IfaceParams -> IfaceDecls -> NameDisp -> a -> Name -> REPL ()
showValHelp params :: IfaceParams
params env :: IfaceDecls
env nameEnv :: NameDisp
nameEnv qname :: a
qname name :: Name
name =
REPL () -> Maybe (REPL ()) -> REPL ()
forall a. a -> Maybe a -> a
fromMaybe (NameDisp -> Name -> REPL ()
noInfo NameDisp
nameEnv Name
name)
([Maybe (REPL ())] -> Maybe (REPL ())
forall (t :: * -> *) (m :: * -> *) a.
(Foldable t, MonadPlus m) =>
t (m a) -> m a
msum [ Maybe (REPL ())
fromDecl, Maybe (REPL ())
fromNewtype, Maybe (REPL ())
fromParameter ])
where
fromDecl :: Maybe (REPL ())
fromDecl =
do M.IfaceDecl { .. } <- Name -> Map Name IfaceDecl -> Maybe IfaceDecl
forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup Name
name (IfaceDecls -> Map Name IfaceDecl
M.ifDecls IfaceDecls
env)
REPL () -> Maybe (REPL ())
forall (m :: * -> *) a. Monad m => a -> m a
return (REPL () -> Maybe (REPL ())) -> REPL () -> Maybe (REPL ())
forall a b. (a -> b) -> a -> b
$
do String -> REPL ()
rPutStrLn ""
let property :: Doc
property
| Pragma
P.PragmaProperty Pragma -> [Pragma] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [Pragma]
ifDeclPragmas = String -> Doc
text "property"
| Bool
otherwise = Doc
empty
Doc -> REPL ()
forall a. Show a => a -> REPL ()
rPrint (Doc -> REPL ()) -> Doc -> REPL ()
forall a b. (a -> b) -> a -> b
$ NameDisp -> Doc -> Doc
runDoc NameDisp
nameEnv
(Doc -> Doc) -> Doc -> Doc
forall a b. (a -> b) -> a -> b
$ Int -> Doc -> Doc
nest 4
(Doc -> Doc) -> Doc -> Doc
forall a b. (a -> b) -> a -> b
$ Doc
property
Doc -> Doc -> Doc
<+> a -> Doc
forall a. PP a => a -> Doc
pp a
qname
Doc -> Doc -> Doc
<+> Doc
colon
Doc -> Doc -> Doc
<+> Schema -> Doc
forall a. PP a => a -> Doc
pp (Schema
ifDeclSig)
Maybe Fixity -> REPL ()
doShowFix (Maybe Fixity -> REPL ()) -> Maybe Fixity -> REPL ()
forall a b. (a -> b) -> a -> b
$ Maybe Fixity
ifDeclFixity Maybe Fixity -> Maybe Fixity -> Maybe Fixity
forall (m :: * -> *) a. MonadPlus m => m a -> m a -> m a
`mplus`
(Bool -> Maybe ()
forall (f :: * -> *). Alternative f => Bool -> f ()
guard Bool
ifDeclInfix Maybe () -> Maybe Fixity -> Maybe Fixity
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> Fixity -> Maybe Fixity
forall (m :: * -> *) a. Monad m => a -> m a
return Fixity
P.defaultFixity)
case Maybe String
ifDeclDoc of
Just str :: String
str -> String -> REPL ()
rPutStrLn ('\n' Char -> ShowS
forall a. a -> [a] -> [a]
: String
str)
Nothing -> () -> REPL ()
forall (m :: * -> *) a. Monad m => a -> m a
return ()
fromNewtype :: Maybe (REPL ())
fromNewtype =
do IfaceNewtype
_ <- Name -> Map Name IfaceNewtype -> Maybe IfaceNewtype
forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup Name
name (IfaceDecls -> Map Name IfaceNewtype
M.ifNewtypes IfaceDecls
env)
REPL () -> Maybe (REPL ())
forall (m :: * -> *) a. Monad m => a -> m a
return (REPL () -> Maybe (REPL ())) -> REPL () -> Maybe (REPL ())
forall a b. (a -> b) -> a -> b
$ () -> REPL ()
forall (m :: * -> *) a. Monad m => a -> m a
return ()
fromParameter :: Maybe (REPL ())
fromParameter =
do ModVParam
p <- Name -> Map Name ModVParam -> Maybe ModVParam
forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup Name
name (IfaceParams -> Map Name ModVParam
M.ifParamFuns IfaceParams
params)
REPL () -> Maybe (REPL ())
forall (m :: * -> *) a. Monad m => a -> m a
return (REPL () -> Maybe (REPL ())) -> REPL () -> Maybe (REPL ())
forall a b. (a -> b) -> a -> b
$
do String -> REPL ()
rPutStrLn ""
Doc -> REPL ()
forall a. Show a => a -> REPL ()
rPrint (Doc -> REPL ()) -> Doc -> REPL ()
forall a b. (a -> b) -> a -> b
$ NameDisp -> Doc -> Doc
runDoc NameDisp
nameEnv
(Doc -> Doc) -> Doc -> Doc
forall a b. (a -> b) -> a -> b
$ Int -> Doc -> Doc
nest 4
(Doc -> Doc) -> Doc -> Doc
forall a b. (a -> b) -> a -> b
$ String -> Doc
text "parameter" Doc -> Doc -> Doc
<+> a -> Doc
forall a. PP a => a -> Doc
pp a
qname
Doc -> Doc -> Doc
<+> Doc
colon
Doc -> Doc -> Doc
<+> Schema -> Doc
forall a. PP a => a -> Doc
pp (ModVParam -> Schema
T.mvpType ModVParam
p)
Maybe Fixity -> REPL ()
doShowFix (ModVParam -> Maybe Fixity
T.mvpFixity ModVParam
p)
case ModVParam -> Maybe String
T.mvpDoc ModVParam
p of
Just str :: String
str -> String -> REPL ()
rPutStrLn ('\n' Char -> ShowS
forall a. a -> [a] -> [a]
: String
str)
Nothing -> () -> REPL ()
forall (m :: * -> *) a. Monad m => a -> m a
return ()
showCmdHelp :: CommandDescr -> [String] -> REPL ()
showCmdHelp c :: CommandDescr
c [arg :: String
arg] | ":set" String -> [String] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` CommandDescr -> [String]
cNames CommandDescr
c = String -> REPL ()
showOptionHelp String
arg
showCmdHelp c :: CommandDescr
c _args :: [String]
_args =
do String -> REPL ()
rPutStrLn ("\n " String -> ShowS
forall a. [a] -> [a] -> [a]
++ String -> [String] -> String
forall a. [a] -> [[a]] -> [a]
intercalate ", " (CommandDescr -> [String]
cNames CommandDescr
c) String -> ShowS
forall a. [a] -> [a] -> [a]
++ " " String -> ShowS
forall a. [a] -> [a] -> [a]
++ String -> [String] -> String
forall a. [a] -> [[a]] -> [a]
intercalate " " (CommandDescr -> [String]
cArgs CommandDescr
c))
String -> REPL ()
rPutStrLn ""
String -> REPL ()
rPutStrLn (CommandDescr -> String
cHelp CommandDescr
c)
String -> REPL ()
rPutStrLn ""
showOptionHelp :: String -> REPL ()
showOptionHelp arg :: String
arg =
case String -> Trie OptionDescr -> [OptionDescr]
forall a. String -> Trie a -> [a]
lookupTrieExact String
arg Trie OptionDescr
userOptions of
[opt :: 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
$ "\n " String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
k String -> ShowS
forall a. [a] -> [a] -> [a]
++ " = " String -> ShowS
forall a. [a] -> [a] -> [a]
++ String -> (EnvVal -> String) -> Maybe EnvVal -> String
forall b a. b -> (a -> b) -> Maybe a -> b
maybe "???" EnvVal -> String
showEnvVal Maybe EnvVal
ev
String -> REPL ()
rPutStrLn ""
String -> REPL ()
rPutStrLn ("Default value: " String -> ShowS
forall a. [a] -> [a] -> [a]
++ EnvVal -> String
showEnvVal (OptionDescr -> EnvVal
optDefault OptionDescr
opt))
String -> REPL ()
rPutStrLn ""
String -> REPL ()
rPutStrLn (OptionDescr -> String
optHelp OptionDescr
opt)
String -> REPL ()
rPutStrLn ""
[] -> String -> REPL ()
rPutStrLn ("Unknown setting name `" String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
arg String -> ShowS
forall a. [a] -> [a] -> [a]
++ "`")
_ -> String -> REPL ()
rPutStrLn ("Ambiguous setting name `" String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
arg String -> ShowS
forall a. [a] -> [a] -> [a]
++ "`")
runShellCmd :: String -> REPL ()
runShellCmd :: String -> REPL ()
runShellCmd cmd :: 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 (m :: * -> *) a. Monad m => a -> m a
return ()
cdCmd :: FilePath -> REPL ()
cdCmd :: String -> REPL ()
cdCmd f :: String
f | String -> 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
$ "[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 :: a -> REPL a
handleCtrlC a :: a
a = do String -> REPL ()
rPutStrLn "Ctrl-C"
a -> REPL a
forall (m :: * -> *) a. Monad m => a -> m a
return a
a
hasAnyModName :: [M.ModName] -> M.Name -> Bool
hasAnyModName :: [ModName] -> Name -> Bool
hasAnyModName mnames :: [ModName]
mnames n :: Name
n =
case Name -> NameInfo
M.nameInfo Name
n of
M.Declared m :: ModName
m _ -> ModName
m ModName -> [ModName] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [ModName]
mnames
M.Parameter -> Bool
False
replParse :: (String -> Either ParseError a) -> String -> REPL a
replParse :: (String -> Either ParseError a) -> String -> REPL a
replParse parse :: String -> Either ParseError a
parse str :: String
str = case String -> Either ParseError a
parse String
str of
Right a :: a
a -> a -> REPL a
forall (m :: * -> *) a. Monad m => a -> m a
return a
a
Left e :: ParseError
e -> REPLException -> REPL a
forall a. REPLException -> REPL a
raise (ParseError -> REPLException
ParseError ParseError
e)
replParseInput :: String -> REPL (P.ReplInput P.PName)
replParseInput :: String -> REPL (ReplInput PName)
replParseInput = (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
interactiveConfig (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)
replParseExpr :: String -> REPL (P.Expr P.PName)
replParseExpr :: String -> REPL (Expr PName)
replParseExpr = (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
interactiveConfig (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)
interactiveConfig :: Config
interactiveConfig :: Config
interactiveConfig = Config
defaultConfig { cfgSource :: String
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 :: ModuleCmd a -> REPL a
liftModuleCmd cmd :: ModuleCmd a
cmd =
do EvalOpts
evo <- REPL EvalOpts
getEvalOpts
ModuleEnv
env <- REPL ModuleEnv
getModuleEnv
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 (EvalOpts
evo,ModuleEnv
env))
moduleCmdResult :: M.ModuleRes a -> REPL a
moduleCmdResult :: ModuleRes a -> REPL a
moduleCmdResult (res :: Either ModuleError (a, ModuleEnv)
res,ws0 :: [ModuleWarning]
ws0) = do
Bool
warnDefaulting <- String -> REPL Bool
forall a. IsEnvVal a => String -> REPL a
getKnownUser "warnDefaulting"
Bool
warnShadowing <- String -> REPL Bool
forall a. IsEnvVal a => String -> REPL a
getKnownUser "warnShadowing"
let isDefaultWarn :: Warning -> Bool
isDefaultWarn (T.DefaultingTo _ _) = Bool
True
isDefaultWarn _ = Bool
False
filterDefaults :: ModuleWarning -> Maybe ModuleWarning
filterDefaults w :: ModuleWarning
w | Bool
warnDefaulting = ModuleWarning -> Maybe ModuleWarning
forall a. a -> Maybe a
Just ModuleWarning
w
filterDefaults (M.TypeCheckWarnings xs :: [(Range, Warning)]
xs) =
case ((Range, Warning) -> Bool)
-> [(Range, Warning)] -> [(Range, Warning)]
forall a. (a -> Bool) -> [a] -> [a]
filter (Bool -> Bool
not (Bool -> Bool)
-> ((Range, Warning) -> Bool) -> (Range, Warning) -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Warning -> Bool
isDefaultWarn (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
ys :: [(Range, Warning)]
ys -> ModuleWarning -> Maybe ModuleWarning
forall a. a -> Maybe a
Just ([(Range, Warning)] -> ModuleWarning
M.TypeCheckWarnings [(Range, Warning)]
ys)
filterDefaults w :: ModuleWarning
w = ModuleWarning -> Maybe ModuleWarning
forall a. a -> Maybe a
Just ModuleWarning
w
isShadowWarn :: RenamerWarning -> Bool
isShadowWarn (M.SymbolShadowed {}) = Bool
True
isShadowWarn _ = Bool
False
filterShadowing :: ModuleWarning -> Maybe ModuleWarning
filterShadowing w :: ModuleWarning
w | Bool
warnShadowing = ModuleWarning -> Maybe ModuleWarning
forall a. a -> Maybe a
Just ModuleWarning
w
filterShadowing (M.RenamerWarnings xs :: [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
isShadowWarn) [RenamerWarning]
xs of
[] -> Maybe ModuleWarning
forall a. Maybe a
Nothing
ys :: [RenamerWarning]
ys -> ModuleWarning -> Maybe ModuleWarning
forall a. a -> Maybe a
Just ([RenamerWarning] -> ModuleWarning
M.RenamerWarnings [RenamerWarning]
ys)
filterShadowing w :: 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 ModuleWarning -> Maybe ModuleWarning
filterDefaults ([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
filterShadowing ([ModuleWarning] -> [ModuleWarning])
-> [ModuleWarning] -> [ModuleWarning]
forall a b. (a -> b) -> a -> b
$ [ModuleWarning]
ws0
(_,_,_,names :: NameDisp
names) <- REPL (IfaceParams, IfaceDecls, NamingEnv, NameDisp)
getFocusedEnv
(ModuleWarning -> REPL ()) -> [ModuleWarning] -> REPL ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ (Doc -> REPL ()
forall a. Show a => a -> REPL ()
rPrint (Doc -> REPL ())
-> (ModuleWarning -> Doc) -> ModuleWarning -> REPL ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. NameDisp -> Doc -> Doc
runDoc NameDisp
names (Doc -> Doc) -> (ModuleWarning -> Doc) -> ModuleWarning -> Doc
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
a,me' :: ModuleEnv
me') -> ModuleEnv -> REPL ()
setModuleEnv ModuleEnv
me' REPL () -> REPL a -> REPL a
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> a -> REPL a
forall (m :: * -> *) a. Monad m => a -> m a
return a
a
Left err :: ModuleError
err ->
do ModuleError
e <- case ModuleError
err of
M.ErrorInFile (M.InFile file :: String
file) e :: ModuleError
e ->
do String -> REPL ()
setEditPath String
file
ModuleError -> REPL ModuleError
forall (m :: * -> *) a. Monad m => a -> m a
return ModuleError
e
_ -> ModuleError -> REPL ModuleError
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 e :: 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 ds :: [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 d :: Decl name
d = TopLevel (Decl name) -> TopDecl name
forall name. TopLevel (Decl name) -> TopDecl name
P.Decl TopLevel :: forall a. ExportType -> Maybe (Located String) -> a -> TopLevel a
P.TopLevel { tlExport :: ExportType
P.tlExport = ExportType
P.Public
, tlDoc :: Maybe (Located String)
P.tlDoc = Maybe (Located String)
forall a. Maybe a
Nothing
, tlValue :: Decl name
P.tlValue = Decl name
d }
(names :: NamingEnv
names,ds' :: [DeclGroup]
ds') <- ModuleCmd (NamingEnv, [DeclGroup]) -> REPL (NamingEnv, [DeclGroup])
forall a. ModuleCmd a -> REPL a
liftModuleCmd ([TopDecl PName] -> ModuleCmd (NamingEnv, [DeclGroup])
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 { deNames :: NamingEnv
M.deNames = NamingEnv
names NamingEnv -> NamingEnv -> NamingEnv
`M.shadowing` DynamicEnv -> NamingEnv
M.deNames DynamicEnv
denv }
[DeclGroup] -> REPL [DeclGroup]
forall (m :: * -> *) a. Monad m => a -> m a
return [DeclGroup]
ds'
replSpecExpr :: T.Expr -> REPL T.Expr
replSpecExpr :: Expr -> REPL Expr
replSpecExpr e :: 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 (E.Value, T.Type)
replEvalExpr :: Expr PName -> REPL (Value, Type)
replEvalExpr expr :: Expr PName
expr =
do (_,def :: Expr
def,sig :: Schema
sig) <- Expr PName -> REPL (Expr Name, Expr, Schema)
replCheckExpr Expr PName
expr
Expr -> REPL ()
forall a. FreeVars a => a -> REPL ()
validEvalContext Expr
def
Schema -> REPL ()
forall a. FreeVars a => a -> REPL ()
validEvalContext Schema
sig
ModuleEnv
me <- REPL ModuleEnv
getModuleEnv
let cfg :: SolverConfig
cfg = ModuleEnv -> SolverConfig
M.meSolverConfig ModuleEnv
me
Maybe ([(TParam, Type)], Expr)
mbDef <- IO (Maybe ([(TParam, Type)], Expr))
-> REPL (Maybe ([(TParam, Type)], Expr))
forall a. IO a -> REPL a
io (IO (Maybe ([(TParam, Type)], Expr))
-> REPL (Maybe ([(TParam, Type)], Expr)))
-> IO (Maybe ([(TParam, Type)], Expr))
-> REPL (Maybe ([(TParam, Type)], Expr))
forall a b. (a -> b) -> a -> b
$ SolverConfig
-> (Solver -> IO (Maybe ([(TParam, Type)], Expr)))
-> IO (Maybe ([(TParam, Type)], Expr))
forall a. SolverConfig -> (Solver -> IO a) -> IO a
SMT.withSolver SolverConfig
cfg (\s :: Solver
s -> Solver -> Expr -> Schema -> IO (Maybe ([(TParam, Type)], Expr))
defaultReplExpr Solver
s Expr
def Schema
sig)
(def1 :: Expr
def1,ty :: Type
ty) <-
case Maybe ([(TParam, Type)], Expr)
mbDef of
Nothing -> REPLException -> REPL (Expr, Type)
forall a. REPLException -> REPL a
raise (Schema -> REPLException
EvalPolyError Schema
sig)
Just (tys :: [(TParam, Type)]
tys,def1 :: Expr
def1) ->
do [(TParam, Type)] -> REPL ()
forall a. PP a => [(TParam, a)] -> REPL ()
warnDefaults [(TParam, Type)]
tys
let su :: Subst
su = [(TParam, Type)] -> Subst
T.listParamSubst [(TParam, Type)]
tys
(Expr, Type) -> REPL (Expr, Type)
forall (m :: * -> *) a. Monad m => a -> m a
return (Expr
def1, Subst -> Type -> Type
forall t. TVars t => Subst -> t -> t
T.apSubst Subst
su (Schema -> Type
T.sType Schema
sig))
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
def1)
REPL () -> REPL ()
whenDebug (String -> REPL ()
rPutStrLn (Expr -> String
forall a. PP (WithNames a) => a -> String
dump Expr
def1))
Type -> Expr -> REPL ()
bindItVariable Type
ty Expr
def1
(Value, Type) -> REPL (Value, Type)
forall (m :: * -> *) a. Monad m => a -> m a
return (Value
val,Type
ty)
where
warnDefaults :: [(TParam, a)] -> REPL ()
warnDefaults ts :: [(TParam, a)]
ts =
case [(TParam, a)]
ts of
[] -> () -> REPL ()
forall (m :: * -> *) a. Monad m => a -> m a
return ()
_ ->
do Bool
warnDefaulting <- String -> REPL Bool
forall a. IsEnvVal a => String -> REPL a
getKnownUser "warnDefaulting"
Bool -> REPL () -> REPL ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when Bool
warnDefaulting (REPL () -> REPL ()) -> REPL () -> REPL ()
forall a b. (a -> b) -> a -> b
$
do String -> REPL ()
rPutStrLn "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 (x :: TParam
x,t :: a
t) =
Doc -> REPL ()
forall a. Show a => a -> REPL ()
rPrint (" *" Doc -> Doc -> Doc
<+> Int -> Doc -> Doc
nest 2 ("Using" Doc -> Doc -> Doc
<+> Doc -> Doc
quotes (a -> Doc
forall a. PP a => a -> Doc
pp a
t) Doc -> Doc -> Doc
<+> "for" Doc -> Doc -> Doc
<+>
TVarSource -> Doc
forall a. PP a => a -> Doc
pp (TVarInfo -> TVarSource
T.tvarDesc (TParam -> TVarInfo
T.tpInfo TParam
x))))
itIdent :: M.Ident
itIdent :: Ident
itIdent = String -> Ident
M.packIdent "it"
replWriteFile :: FilePath -> BS.ByteString -> (X.SomeException -> REPL ()) -> REPL ()
replWriteFile :: String -> ByteString -> (SomeException -> REPL ()) -> REPL ()
replWriteFile fp :: String
fp bytes :: ByteString
bytes handler :: 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 -> ByteString -> IO ()
BS.writeFile String
fp ByteString
bytes IO () -> IO (Maybe SomeException) -> IO (Maybe SomeException)
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> Maybe SomeException -> IO (Maybe SomeException)
forall (m :: * -> *) a. Monad m => a -> m a
return Maybe SomeException
forall a. Maybe a
Nothing) (Maybe SomeException -> IO (Maybe SomeException)
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 (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 fp :: String
fp handler :: 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 (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
`fmap` String -> IO ByteString
BS.readFile String
fp) (\e :: SomeException
e -> Either SomeException ByteString
-> IO (Either SomeException ByteString)
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 (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 :: T.Type -> T.Expr -> REPL ()
bindItVariable :: Type -> Expr -> REPL ()
bindItVariable ty :: Type
ty expr :: Expr
expr = do
Name
freshIt <- Ident -> NameSource -> REPL Name
freshName Ident
itIdent NameSource
M.UserName
let schema :: Schema
schema = Forall :: [TParam] -> [Type] -> Type -> Schema
T.Forall { sVars :: [TParam]
T.sVars = []
, sProps :: [Type]
T.sProps = []
, sType :: Type
T.sType = Type
ty
}
decl :: Decl
decl = $WDecl :: Name
-> Schema
-> DeclDef
-> [Pragma]
-> Bool
-> Maybe Fixity
-> Maybe String
-> 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 String
T.dDoc = Maybe String
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' = PName -> Name -> NamingEnv
M.singletonE (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 { deNames :: NamingEnv
M.deNames = NamingEnv
nenv' }
bindItVariableVal :: T.Type -> E.Value -> REPL ()
bindItVariableVal :: Type -> Value -> REPL ()
bindItVariableVal ty :: Type
ty val :: 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 -> Type -> Value -> Eval (Maybe Expr)
E.toExpr PrimMap
prims Type
ty Value
val)
case Maybe Expr
mb of
Nothing -> () -> REPL ()
forall (m :: * -> *) a. Monad m => a -> m a
return ()
Just expr :: Expr
expr -> Type -> Expr -> REPL ()
bindItVariable Type
ty Expr
expr
bindItVariables :: T.Type -> [T.Expr] -> REPL ()
bindItVariables :: Type -> [Expr] -> REPL ()
bindItVariables ty :: Type
ty exprs :: [Expr]
exprs = Type -> Expr -> REPL ()
bindItVariable Type
seqTy Expr
seqExpr
where
len :: Int
len = [Expr] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [Expr]
exprs
seqTy :: Type
seqTy = Type -> Type -> Type
T.tSeq (Int -> Type
forall a. Integral a => a -> Type
T.tNum Int
len) Type
ty
seqExpr :: Expr
seqExpr = [Expr] -> Type -> Expr
T.EList [Expr]
exprs Type
ty
replEvalDecl :: P.Decl P.PName -> REPL ()
replEvalDecl :: Decl PName -> REPL ()
replEvalDecl decl :: Decl PName
decl = do
[DeclGroup]
dgs <- [Decl PName] -> REPL [DeclGroup]
replCheckDecls [Decl PName
decl]
[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_ (\dg :: 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 file :: String
file = do
Maybe String
mb <- IO (Maybe String) -> REPL (Maybe String)
forall a. IO a -> REPL a
io (String -> IO (Maybe String)
lookupEnv "EDITOR")
let editor :: String
editor = String -> Maybe String -> String
forall a. a -> Maybe a -> a
fromMaybe "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
(_,_,_,ph :: 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 (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
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 (String,String)
splitCommand :: String -> Maybe (String, String)
splitCommand txt :: String
txt =
case ShowS
sanitize String
txt of
':' : more :: String
more
| (as :: String
as,bs :: String
bs) <- (Char -> Bool) -> String -> (String, String)
forall a. (a -> Bool) -> [a] -> ([a], [a])
span (\x :: Char
x -> Char -> Bool
isPunctuation Char
x Bool -> Bool -> Bool
|| Char -> Bool
isSymbol Char
x) String
more
, Bool -> Bool
not (String -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null String
as) -> (String, String) -> Maybe (String, String)
forall a. a -> Maybe a
Just (':' Char -> ShowS
forall a. a -> [a] -> [a]
: String
as, ShowS
sanitize String
bs)
| (as :: String
as,bs :: String
bs) <- (Char -> Bool) -> String -> (String, String)
forall a. (a -> Bool) -> [a] -> ([a], [a])
break Char -> Bool
isSpace String
more
, Bool -> Bool
not (String -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null String
as) -> (String, String) -> Maybe (String, String)
forall a. a -> Maybe a
Just (':' Char -> ShowS
forall a. a -> [a] -> [a]
: String
as, ShowS
sanitize String
bs)
| Bool
otherwise -> Maybe (String, String)
forall a. Maybe a
Nothing
expr :: String
expr -> Bool -> Maybe ()
forall (f :: * -> *). Alternative f => Bool -> f ()
guard (Bool -> Bool
not (String -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null String
expr)) Maybe () -> Maybe (String, String) -> Maybe (String, String)
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> (String, String) -> Maybe (String, String)
forall (m :: * -> *) a. Monad m => a -> m a
return (String
expr,[])
uncons :: [a] -> Maybe (a,[a])
uncons :: [a] -> Maybe (a, [a])
uncons as :: [a]
as = case [a]
as of
a :: a
a:rest :: [a]
rest -> (a, [a]) -> Maybe (a, [a])
forall a. a -> Maybe a
Just (a
a,[a]
rest)
_ -> Maybe (a, [a])
forall a. Maybe a
Nothing
findCommand :: String -> [CommandDescr]
findCommand :: String -> [CommandDescr]
findCommand str :: String
str = String -> CommandMap -> [CommandDescr]
forall a. String -> Trie a -> [a]
lookupTrie String
str CommandMap
commands
findCommandExact :: String -> [CommandDescr]
findCommandExact :: String -> [CommandDescr]
findCommandExact str :: 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 True str :: String
str = String -> CommandMap -> [CommandDescr]
forall a. String -> Trie a -> [a]
lookupTrieExact String
str CommandMap
nbCommands
findNbCommand False str :: 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 findCmd :: String -> [CommandDescr]
findCmd line :: String
line = do
(cmd :: String
cmd,args :: String
args) <- String -> Maybe (String, String)
splitCommand String
line
let args' :: String
args' = ShowS
sanitizeEnd String
args
case String -> [CommandDescr]
findCmd String
cmd of
[c :: CommandDescr
c] -> case CommandDescr -> CommandBody
cBody CommandDescr
c of
ExprArg body :: String -> REPL ()
body -> Command -> Maybe Command
forall a. a -> Maybe a
Just (REPL () -> Command
Command (String -> REPL ()
body String
args'))
DeclsArg body :: String -> REPL ()
body -> Command -> Maybe Command
forall a. a -> Maybe a
Just (REPL () -> Command
Command (String -> REPL ()
body String
args'))
ExprTypeArg body :: String -> REPL ()
body -> Command -> Maybe Command
forall a. a -> Maybe a
Just (REPL () -> Command
Command (String -> REPL ()
body String
args'))
ModNameArg body :: String -> REPL ()
body -> Command -> Maybe Command
forall a. a -> Maybe a
Just (REPL () -> Command
Command (String -> REPL ()
body String
args'))
FilenameArg body :: String -> REPL ()
body -> Command -> Maybe Command
forall a. a -> Maybe a
Just (REPL () -> Command
Command (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 body :: String -> REPL ()
body -> Command -> Maybe Command
forall a. a -> Maybe a
Just (REPL () -> Command
Command (String -> REPL ()
body String
args'))
ShellArg body :: String -> REPL ()
body -> Command -> Maybe Command
forall a. a -> Maybe a
Just (REPL () -> Command
Command (String -> REPL ()
body String
args'))
HelpArg body :: String -> REPL ()
body -> Command -> Maybe Command
forall a. a -> Maybe a
Just (REPL () -> Command
Command (String -> REPL ()
body String
args'))
NoArg body :: REPL ()
body -> Command -> Maybe Command
forall a. a -> Maybe a
Just (REPL () -> Command
Command REPL ()
body)
FileExprArg body :: String -> String -> REPL ()
body ->
case String -> Maybe (String, String)
extractFilePath String
args' of
Just (fp :: String
fp,expr :: String
expr) -> Command -> Maybe Command
forall a. a -> Maybe a
Just (REPL () -> Command
Command (String -> REPL String
expandHome String
fp REPL String -> (String -> REPL ()) -> REPL ()
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= (String -> String -> REPL ()) -> String -> String -> REPL ()
forall a b c. (a -> b -> c) -> b -> a -> c
flip String -> String -> REPL ()
body String
expr))
Nothing -> Maybe Command
forall a. Maybe a
Nothing
[] -> case String -> Maybe (Char, String)
forall a. [a] -> Maybe (a, [a])
uncons String
cmd of
Just (':',_) -> Command -> Maybe Command
forall a. a -> Maybe a
Just (String -> Command
Unknown String
cmd)
Just _ -> Command -> Maybe Command
forall a. a -> Maybe a
Just (REPL () -> Command
Command (String -> REPL ()
evalCmd String
line))
_ -> Maybe Command
forall a. Maybe a
Nothing
cs :: [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 path :: String
path =
case String
path of
'~' : c :: Char
c : more :: 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 (m :: * -> *) a. Monad m => a -> m a
return (String
dir String -> ShowS
</> String
more)
_ -> String -> REPL String
forall (m :: * -> *) a. Monad m => a -> m a
return String
path
extractFilePath :: String -> Maybe (String, String)
extractFilePath ipt :: String
ipt =
let quoted :: a -> [a] -> ([a], [a])
quoted q :: a
q = (\(a :: [a]
a,b :: [a]
b) -> ([a]
a, Int -> [a] -> [a]
forall a. Int -> [a] -> [a]
drop 1 [a]
b)) (([a], [a]) -> ([a], [a]))
-> ([a] -> ([a], [a])) -> [a] -> ([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
"" -> Maybe (String, String)
forall a. Maybe a
Nothing
'\'':rest :: String
rest -> (String, String) -> Maybe (String, String)
forall a. a -> Maybe a
Just ((String, String) -> Maybe (String, String))
-> (String, String) -> Maybe (String, String)
forall a b. (a -> b) -> a -> b
$ Char -> String -> (String, String)
forall a. Eq a => a -> [a] -> ([a], [a])
quoted '\'' String
rest
'"':rest :: String
rest -> (String, String) -> Maybe (String, String)
forall a. a -> Maybe a
Just ((String, String) -> Maybe (String, String))
-> (String, String) -> Maybe (String, String)
forall a b. (a -> b) -> a -> b
$ Char -> String -> (String, String)
forall a. Eq a => a -> [a] -> ([a], [a])
quoted '"' String
rest
_ -> (String, String) -> Maybe (String, String)
forall a. a -> Maybe a
Just ((String, String) -> Maybe (String, String))
-> (String, String) -> Maybe (String, String)
forall a b. (a -> b) -> a -> b
$ (Char -> Bool) -> String -> (String, String)
forall a. (a -> Bool) -> [a] -> ([a], [a])
break Char -> Bool
isSpace String
ipt