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

    {-# LANGUAGE FlexibleContexts #-}
    {-# LANGUAGE OverloadedStrings #-}
    {-# LANGUAGE PatternGuards #-}
    {-# LANGUAGE RecordWildCards #-}
    module Cryptol.REPL.Command (
        -- * Commands
        Command(..), CommandDescr(..), CommandBody(..), CommandExitCode(..)
      , parseCommand
      , runCommand
      , splitCommand
      , findCommand
      , findCommandExact
      , findNbCommand
      , commandList

      , moduleCmd, loadCmd, loadPrelude, setOptionCmd

        -- Parsing
      , interactiveConfig
      , replParseExpr

        -- Evaluation and Typechecking
      , replEvalExpr
      , replCheckExpr

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

        -- Misc utilities
      , handleCtrlC
      , sanitize

        -- To support Notebook interface (might need to refactor)
      , 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)

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

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

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

    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 -- XXX: More?

    -- | REPL command parsing.
    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

    -- | Notebook command parsing.
    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

    -- | A subset of commands safe for Notebook execution
    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)) ' '

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

    -- | Run a command.
    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

    -- Get the setting we should use for displaying values.
    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)

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

          String -> REPL ()
    rPutStrLn (Doc -> String
    forall a. Show a => a -> String
    show Doc
    valDoc)
        P.LetInput decl :: Decl PName
    decl -> do
          -- explicitly make this a top-level declaration, so that it will
          -- be generalized if mono-binds is enabled
          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 -- function application has precedence 3
         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)

    -- | Randomly test a property, or exhaustively check it if the number
    -- of values in the type under test is smaller than the @tests@
    -- environment variable, or we specify exhaustive testing.
    qcCmd :: QCMode -> String -> 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    -- 100%

      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"]

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

    -- | Console-specific version of 'proveSat'. Prints output to the
    -- console, and binds the @it@ variable to a record whose form depends
    -- on the expression given. See ticket #66 for a discussion of this
    -- design.
    cmdProveSat :: Bool -> String -> 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"

    -- | Make a type/expression pair that is suitable for binding to @it@
    -- after running @:sat@ or @:prove@
    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

      -- XXX need more warnings from the module system
      REPL () -> REPL ()
    whenDebug (String -> REPL ()
    rPutStrLn (Expr -> String
    forall a. PP (WithNames a) => a -> String
    dump Expr
    def))
      (_,_,_,names :: NameDisp
    names) <- REPL (IfaceParams, IfaceDecls, NamingEnv, NameDisp)
    getFocusedEnv
      -- type annotation ':' has precedence 2
      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 ()

      -- when `:load`, the edit and focused paths become the parameter
      | 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
            }
         -- after a successful load, the current module becomes the edit target
         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"

    -- XXX at the moment, this can only look at declarations.
    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

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

    -- XXX this should probably do something a bit more specific.
    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

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

    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

    -- | Lift a parsing action into the REPL monad.
    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"
      -- XXX: let's generalize this pattern
      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 ->
                      -- on error, the file with the error becomes the edit
                      -- target.  Note, however, that the focused module is not
                      -- changed.
                      do String -> REPL ()
    setEditPath String
    file
                         ModuleError -> REPL ModuleError
    forall (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

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

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

      let mkTop :: Decl name -> TopDecl name
    mkTop 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))

      -- extend the naming env
      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))
         -- add "it" to the namespace
         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

    -- | Creates a fresh binding of "it" to the expression given, and adds
    -- it to the current dynamic environment
    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' }

    -- | Extend the dynamic environment with a fresh binding for "it",
    -- as defined by the given value.  If we cannot determine the definition
    -- of the value, then we don't bind `it`.
    bindItVariableVal :: 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

    -- | Creates a fresh binding of "it" to a finite sequence of
    -- expressions of the same type, and adds that sequence to the current
    -- dynamic environment
    bindItVariables :: 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

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

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

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

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

    -- | Split at the first word boundary.
    splitCommand :: String -> Maybe (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 list.
    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

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

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

    -- | Lookup a string in the notebook-safe command list.
    findNbCommand :: Bool -> String -> [CommandDescr]
    findNbCommand :: Bool -> String -> [CommandDescr]
    findNbCommand 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

    -- | Parse a line as a command.
    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