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

    {-# LANGUAGE BangPatterns #-}
    {-# LANGUAGE BlockArguments #-}
    {-# LANGUAGE FlexibleContexts #-}
    {-# LANGUAGE LambdaCase #-}
    {-# LANGUAGE MultiWayIf #-}
    {-# LANGUAGE OverloadedStrings #-}
    {-# LANGUAGE PatternGuards #-}
    {-# LANGUAGE RecordWildCards #-}
    -- See Note [-Wincomplete-uni-patterns and irrefutable patterns] in Cryptol.TypeCheck.TypePat
    {-# OPTIONS_GHC -Wno-incomplete-uni-patterns #-}
    module Cryptol.REPL.Command (
        -- * Commands
        Command(..), CommandDescr(..), CommandBody(..), CommandExitCode(..)
      , parseCommand
      , runCommand
      , splitCommand
      , findCommand
      , findCommandExact
      , findNbCommand
      , commandList

      , moduleCmd, loadCmd, loadPrelude, setOptionCmd

        -- Parsing
      , interactiveConfig
      , replParseExpr

        -- Evaluation and Typechecking
      , replEvalExpr
      , replCheckExpr

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

        -- Misc utilities
      , handleCtrlC
      , sanitize
      , withRWTempFile

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

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

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

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

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

    import GHC.Float (log1p, expm1)

    import Prelude ()
    import Prelude.Compat

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

    printCounterexample :: CounterExampleType -> Doc -> [Concrete.Value] -> REPL ()
    printCounterexample :: CounterExampleType -> Doc -> [Value] -> REPL ()
    printCounterexample CounterExampleType
    cexTy Doc
    exprDoc [Value]
    vs =
      do PPOpts
    ppOpts <- REPL PPOpts
    getPPValOpts
         [Doc]
    docs <- (Value -> REPL Doc) -> [Value] -> REPL [Doc]
    forall (t :: * -> *) (m :: * -> *) a b.
    (Traversable t, Monad m) =>
    (a -> m b) -> t a -> m (t b)
    forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [b]
    mapM (Eval Doc -> REPL Doc
    forall a. Eval a -> REPL a
    rEval (Eval Doc -> REPL Doc) -> (Value -> Eval Doc) -> Value -> REPL Doc
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Concrete -> PPOpts -> Value -> SEval Concrete Doc
    forall sym.
    Backend sym =>
    sym -> PPOpts -> GenValue sym -> SEval sym Doc
    E.ppValue Concrete
    Concrete PPOpts
    ppOpts) [Value]
    vs
         let cexRes :: [Doc]
    cexRes = case CounterExampleType
    cexTy of
               CounterExampleType
    SafetyViolation    -> [String -> Doc
    text String
    "~> ERROR"]
               CounterExampleType
    PredicateFalsified -> [String -> Doc
    text String
    "= False"]
         Doc -> REPL ()
    forall a. Show a => a -> REPL ()
    rPrint (Doc -> REPL ()) -> Doc -> REPL ()
    forall a b. (a -> b) -> a -> b
    $ Int -> Doc -> Doc
    nest Int
    2 ([Doc] -> Doc
    sep ([Doc
    exprDoc] [Doc] -> [Doc] -> [Doc]
    forall a. [a] -> [a] -> [a]
    ++ [Doc]
    docs [Doc] -> [Doc] -> [Doc]
    forall a. [a] -> [a] -> [a]
    ++ [Doc]
    cexRes))

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

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

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

    -- | Randomly test a property, or exhaustively check it if the number
    -- of values in the type under test is smaller than the @tests@
    -- environment variable, or we specify exhaustive testing.
    qcCmd :: QCMode -> String -> (Int,Int) -> Maybe FilePath -> REPL ()
    qcCmd :: QCMode -> String -> (Int, Int) -> Maybe String -> REPL ()
    qcCmd QCMode
    qcMode String
    "" (Int, Int)
    _pos Maybe String
    _fnm =
      do ([(Name, IfaceDecl)]
    xs,NameDisp
    disp) <- REPL ([(Name, IfaceDecl)], NameDisp)
    getPropertyNames
         let nameStr :: a -> String
    nameStr a
    x = Doc -> String
    forall a. Show a => a -> String
    show (NameDisp -> Doc -> Doc
    fixNameDisp NameDisp
    disp (a -> Doc
    forall a. PP a => a -> Doc
    pp a
    x))
         if [(Name, IfaceDecl)] -> Bool
    forall a. [a] -> Bool
    forall (t :: * -> *) a. Foldable t => t a -> Bool
    null [(Name, IfaceDecl)]
    xs
            then String -> REPL ()
    rPutStrLn String
    "There are no properties in scope."
            else [(Name, IfaceDecl)] -> ((Name, IfaceDecl) -> REPL ()) -> REPL ()
    forall (t :: * -> *) (m :: * -> *) a b.
    (Foldable t, Monad m) =>
    t a -> (a -> m b) -> m ()
    forM_ [(Name, IfaceDecl)]
    xs (((Name, IfaceDecl) -> REPL ()) -> REPL ())
    -> ((Name, IfaceDecl) -> REPL ()) -> REPL ()
    forall a b. (a -> b) -> a -> b
    $ \(Name
    x,IfaceDecl
    d) ->
                   do let str :: String
    str = Name -> String
    forall {a}. PP a => a -> String
    nameStr Name
    x
                      String -> REPL ()
    rPutStr (String -> REPL ()) -> String -> REPL ()
    forall a b. (a -> b) -> a -> b
    $ String
    "property " String -> ShowS
    forall a. [a] -> [a] -> [a]
    ++ String
    str String -> ShowS
    forall a. [a] -> [a] -> [a]
    ++ String
    " "
                      let texpr :: Expr
    texpr = Name -> Expr
    T.EVar Name
    x
                      let schema :: Schema
    schema = IfaceDecl -> Schema
    M.ifDeclSig IfaceDecl
    d
                      NameDisp
    nd <- ModContext -> NameDisp
    M.mctxNameDisp (ModContext -> NameDisp) -> REPL ModContext -> REPL NameDisp
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> REPL ModContext
    getFocusedEnv
                      let doc :: Doc
    doc = NameDisp -> Doc -> Doc
    fixNameDisp NameDisp
    nd (Expr -> Doc
    forall a. PP a => a -> Doc
    pp Expr
    texpr)
                      REPL TestReport -> REPL ()
    forall (f :: * -> *) a. Functor f => f a -> f ()
    void (QCMode -> Doc -> Expr -> Schema -> REPL TestReport
    qcExpr QCMode
    qcMode Doc
    doc Expr
    texpr Schema
    schema)

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

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

    qcExpr ::
      QCMode ->
      Doc ->
      T.Expr ->
      T.Schema ->
      REPL TestReport
    qcExpr :: QCMode -> Doc -> Expr -> Schema -> REPL TestReport
    qcExpr QCMode
    qcMode Doc
    exprDoc Expr
    texpr Schema
    schema =
      do (Value
    val,Type
    ty) <- Expr -> Schema -> REPL (Maybe (Value, Type))
    replEvalCheckedExpr Expr
    texpr Schema
    schema REPL (Maybe (Value, Type))
    -> (Maybe (Value, Type) -> REPL (Value, Type))
    -> REPL (Value, Type)
    forall a b. REPL a -> (a -> REPL b) -> REPL b
    forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
    >>= \Maybe (Value, Type)
    mb_res -> case Maybe (Value, Type)
    mb_res of
           Just (Value, Type)
    res -> (Value, Type) -> REPL (Value, Type)
    forall a. a -> REPL a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure (Value, Type)
    res
           -- If instance is not found, doesn't necessarily mean that there is no instance.
           -- And due to nondeterminism in result from the solver (for finding solution to
           -- numeric type constraints), `:check` can get to this exception sometimes, but
           -- successfully find an instance and test with it other times.
           Maybe (Value, Type)
    Nothing -> REPLException -> REPL (Value, Type)
    forall a. REPLException -> REPL a
    raise (Schema -> REPLException
    InstantiationsNotFound Schema
    schema)
         Integer
    testNum <- (Int -> Integer
    forall a. Integral a => a -> Integer
    toInteger :: Int -> Integer) (Int -> Integer) -> REPL Int -> REPL Integer
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> String -> REPL Int
    forall a. IsEnvVal a => String -> REPL a
    getKnownUser String
    "tests"
         TypeEnv
    tenv <- GenEvalEnv Concrete -> TypeEnv
    forall sym. GenEvalEnv sym -> TypeEnv
    E.envTypes (GenEvalEnv Concrete -> TypeEnv)
    -> (DynamicEnv -> GenEvalEnv Concrete) -> DynamicEnv -> TypeEnv
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . DynamicEnv -> GenEvalEnv Concrete
    M.deEnv (DynamicEnv -> TypeEnv) -> REPL DynamicEnv -> REPL TypeEnv
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> REPL DynamicEnv
    getDynEnv
         let tyv :: TValue
    tyv = TypeEnv -> Type -> TValue
    E.evalValType TypeEnv
    tenv Type
    ty
         -- tv has already had polymorphism instantiated
         IORef (Maybe String)
    percentRef <- IO (IORef (Maybe String)) -> REPL (IORef (Maybe String))
    forall a. IO a -> REPL a
    io (IO (IORef (Maybe String)) -> REPL (IORef (Maybe String)))
    -> IO (IORef (Maybe String)) -> REPL (IORef (Maybe String))
    forall a b. (a -> b) -> a -> b
    $ Maybe String -> IO (IORef (Maybe String))
    forall a. a -> IO (IORef a)
    newIORef Maybe String
    forall a. Maybe a
    Nothing
         IORef Integer
    testsRef <- IO (IORef Integer) -> REPL (IORef Integer)
    forall a. IO a -> REPL a
    io (IO (IORef Integer) -> REPL (IORef Integer))
    -> IO (IORef Integer) -> REPL (IORef Integer)
    forall a b. (a -> b) -> a -> b
    $ Integer -> IO (IORef Integer)
    forall a. a -> IO (IORef a)
    newIORef Integer
    0

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

    type CommandMap = Trie CommandDescr

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

           String -> REPL ()
    rPutStrLn String
    "}"