    -- | This module contains the implementation of the @dhall repl@ subcommand

    {-# language CPP               #-}
    {-# language FlexibleContexts  #-}
    {-# language NamedFieldPuns    #-}
    {-# language OverloadedStrings #-}
    {-# language RecordWildCards   #-}

    module Dhall.Repl
        ( -- * Repl
          repl
        ) where

    import Control.Exception ( SomeException(SomeException), displayException, throwIO )
    import Control.Monad ( forM_ )
    import Control.Monad.Fail ( MonadFail )
    import Control.Monad.IO.Class ( MonadIO, liftIO )
    import Control.Monad.State.Class ( MonadState, get, modify )
    import Control.Monad.State.Strict ( evalStateT )
    -- For the MonadFail instance for StateT.
    import Control.Monad.Trans.Instances ()
    import Data.List ( isPrefixOf, nub )
    import Data.Maybe ( mapMaybe )
    import Data.Semigroup ((<>))
    import Data.Text ( Text )
    import Data.Void (Void)
    import Dhall.Context (Context)
    import Dhall.Import (hashExpressionToCode)
    import Dhall.Parser (Parser(..))
    import Dhall.Src (Src)
    import Dhall.Pretty (CharacterSet(..))
    import System.Console.Haskeline (Interrupt(..))
    import System.Console.Haskeline.Completion ( Completion, simpleCompletion )
    import System.Directory ( getDirectoryContents )
    import System.Environment ( getEnvironment )

    import qualified Control.Monad.Fail as Fail
    import qualified Control.Monad.Trans.State.Strict as State
    import qualified Data.HashSet
    import qualified Data.Text as Text
    import qualified Data.Text.IO as Text.IO
    import qualified Data.Text.Prettyprint.Doc as Pretty
    import qualified Data.Text.Prettyprint.Doc.Render.Terminal as Pretty ( renderIO )
    import qualified Dhall
    import qualified Dhall.Context
    import qualified Dhall.Core
    import qualified Dhall.Core as Dhall ( Var(V), Expr, normalize )
    import qualified Dhall.Parser.Token                      as Parser.Token
    import qualified Dhall.Pretty
    import qualified Dhall.Pretty.Internal
    import qualified Dhall.Core as Expr ( Expr(..) )
    import qualified Dhall.Import                            as Dhall
    import qualified Dhall.Map                               as Map
    import qualified Dhall.Parser                            as Dhall
    import qualified Dhall.TypeCheck                         as Dhall
    import qualified Dhall.Version                           as Meta
    import qualified System.Console.ANSI
    import qualified System.Console.Haskeline.Completion     as Haskeline
    import qualified System.Console.Repline                  as Repline
    import qualified System.IO
    import qualified Text.Megaparsec                         as Megaparsec

    #if MIN_VERSION_haskeline(0,8,0)
    import qualified Control.Monad.Catch
    #else
    import qualified System.Console.Haskeline.MonadException
    #endif

    type Repl = Repline.HaskelineT (State.StateT Env IO)

    -- | Implementation of the @dhall repl@ subcommand
    repl :: CharacterSet -> Bool -> IO ()
    repl :: CharacterSet -> Bool -> IO ()
    repl characterSet :: CharacterSet
    characterSet explain :: Bool
    explain =
        if Bool
    explain then IO () -> IO ()
    forall a. IO a -> IO a
    Dhall.detailed IO ()
    io else IO ()
    io
      where
        io :: IO ()
    io =
          StateT Env IO () -> Env -> IO ()
    forall (m :: * -> *) s a. Monad m => StateT s m a -> s -> m a
    evalStateT
            ( HaskelineT (StateT Env IO) String
    -> Command (HaskelineT (StateT Env IO))
    -> Options (HaskelineT (StateT Env IO))
    -> Maybe Char
    -> CompleterStyle (StateT Env IO)
    -> HaskelineT (StateT Env IO) ()
    -> StateT Env IO ()
    forall (m :: * -> *) a.
    (Functor m, MonadException m) =>
    HaskelineT m String
    -> Command (HaskelineT m)
    -> Options (HaskelineT m)
    -> Maybe Char
    -> CompleterStyle m
    -> HaskelineT m a
    -> m ()
    Repline.evalRepl
                ( String -> HaskelineT (StateT Env IO) String
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure (String -> HaskelineT (StateT Env IO) String)
    -> String -> HaskelineT (StateT Env IO) String
    forall a b. (a -> b) -> a -> b
    $ String
    turnstile String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ " " )
                ( HaskelineT (StateT Env IO) () -> HaskelineT (StateT Env IO) ()
    dontCrash (HaskelineT (StateT Env IO) () -> HaskelineT (StateT Env IO) ())
    -> Command (HaskelineT (StateT Env IO))
    -> Command (HaskelineT (StateT Env IO))
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Command (HaskelineT (StateT Env IO))
    forall (m :: * -> *).
    (MonadIO m, MonadState Env m) =>
    String -> m ()
    eval )
                Options (HaskelineT (StateT Env IO))
    options
                ( Char -> Maybe Char
    forall a. a -> Maybe a
    Just Char
    optionsPrefix )
                CompleterStyle (StateT Env IO)
    forall (m :: * -> *).
    (Monad m, MonadFail m, MonadIO m, MonadState Env m) =>
    CompleterStyle m
    completer
                HaskelineT (StateT Env IO) ()
    forall (m :: * -> *). MonadIO m => m ()
    greeter
            )
            (Env
    emptyEnv { CharacterSet
    characterSet :: CharacterSet
    characterSet :: CharacterSet
    characterSet, Bool
    explain :: Bool
    explain :: Bool
    explain })

        turnstile :: String
    turnstile =
          case CharacterSet
    characterSet of
            Unicode -> "⊢"
            ASCII   -> "|-"

    data Env = Env
      { Env -> Context Binding
    envBindings      :: Dhall.Context.Context Binding
      , Env -> Maybe Binding
    envIt            :: Maybe Binding
      , Env -> Bool
    explain          :: Bool
      , Env -> CharacterSet
    characterSet     :: CharacterSet
      , Env -> Maybe Handle
    outputHandle     :: Maybe System.IO.Handle
      }

    emptyEnv :: Env
    emptyEnv :: Env
    emptyEnv =
      Env :: Context Binding
    -> Maybe Binding -> Bool -> CharacterSet -> Maybe Handle -> Env
    Env
        { envBindings :: Context Binding
    envBindings = Context Binding
    forall a. Context a
    Dhall.Context.empty
        , envIt :: Maybe Binding
    envIt = Maybe Binding
    forall a. Maybe a
    Nothing
        , explain :: Bool
    explain = Bool
    False
        , characterSet :: CharacterSet
    characterSet = CharacterSet
    Unicode
        , outputHandle :: Maybe Handle
    outputHandle = Handle -> Maybe Handle
    forall a. a -> Maybe a
    Just Handle
    System.IO.stdout
        }

    data Binding = Binding
      { Binding -> Expr Src Void
    bindingExpr :: Dhall.Expr Dhall.Src Void
      , Binding -> Expr Src Void
    bindingType :: Dhall.Expr Dhall.Src Void
      }

    envToContext :: Env -> Dhall.Context.Context Binding
    envToContext :: Env -> Context Binding
    envToContext Env{ Context Binding
    envBindings :: Context Binding
    envBindings :: Env -> Context Binding
    envBindings, Maybe Binding
    envIt :: Maybe Binding
    envIt :: Env -> Maybe Binding
    envIt } =
      case Maybe Binding
    envIt of
        Nothing ->
          Context Binding
    envBindings

        Just it :: Binding
    it ->
          Text -> Binding -> Context Binding -> Context Binding
    forall a. Text -> a -> Context a -> Context a
    Dhall.Context.insert "it" Binding
    it Context Binding
    envBindings

    parseAndLoad
      :: MonadIO m => String -> m ( Dhall.Expr Dhall.Src Void)
    parseAndLoad :: String -> m (Expr Src Void)
    parseAndLoad src :: String
    src = do
      Expr Src Import
    parsed <-
        case String -> Text -> Either ParseError (Expr Src Import)
    Dhall.exprFromText "(input)" (String -> Text
    Text.pack String
    src Text -> Text -> Text
    forall a. Semigroup a => a -> a -> a
    <> "\n") of
          Left e :: ParseError
    e ->
            IO (Expr Src Import) -> m (Expr Src Import)
    forall (m :: * -> *) a. MonadIO m => IO a -> m a
    liftIO ( ParseError -> IO (Expr Src Import)
    forall e a. Exception e => e -> IO a
    throwIO ParseError
    e )

          Right a :: Expr Src Import
    a ->
            Expr Src Import -> m (Expr Src Import)
    forall (m :: * -> *) a. Monad m => a -> m a
    return Expr Src Import
    a

      let status :: Status
    status = String -> Status
    Dhall.emptyStatus "."

      IO (Expr Src Void) -> m (Expr Src Void)
    forall (m :: * -> *) a. MonadIO m => IO a -> m a
    liftIO ( StateT Status IO (Expr Src Void) -> Status -> IO (Expr Src Void)
    forall (m :: * -> *) s a. Monad m => StateT s m a -> s -> m a
    State.evalStateT (Expr Src Import -> StateT Status IO (Expr Src Void)
    Dhall.loadWith Expr Src Import
    parsed) Status
    status )

    eval :: ( MonadIO m, MonadState Env m ) => String -> m ()
    eval :: String -> m ()
    eval src :: String
    src = do
      Expr Src Void
    loaded <-
        String -> m (Expr Src Void)
    forall (m :: * -> *). MonadIO m => String -> m (Expr Src Void)
    parseAndLoad String
    src

      Expr Src Void
    exprType <-
        Expr Src Void -> m (Expr Src Void)
    forall (m :: * -> *).
    (MonadIO m, MonadState Env m) =>
    Expr Src Void -> m (Expr Src Void)
    typeCheck Expr Src Void
    loaded

      Expr Src Void
    expr <-
        Expr Src Void -> m (Expr Src Void)
    forall (m :: * -> *) t.
    MonadState Env m =>
    Expr Src Void -> m (Expr t Void)
    normalize Expr Src Void
    loaded

      (Env -> Env) -> m ()
    forall s (m :: * -> *). MonadState s m => (s -> s) -> m ()
    modify ( \e :: Env
    e -> Env
    e { envIt :: Maybe Binding
    envIt = Binding -> Maybe Binding
    forall a. a -> Maybe a
    Just ( Expr Src Void -> Expr Src Void -> Binding
    Binding Expr Src Void
    expr Expr Src Void
    exprType ) } )

      Expr Src Void -> m ()
    forall a (m :: * -> *).
    (Pretty a, MonadState Env m, MonadIO m) =>
    Expr Src a -> m ()
    output Expr Src Void
    expr

    typeOf :: ( MonadFail m, MonadIO m, MonadState Env m ) => [String] -> m ()
    typeOf :: [String] -> m ()
    typeOf [] = String -> m ()
    forall (m :: * -> *) a. MonadFail m => String -> m a
    Fail.fail ":type requires an argument to check the type of"

    typeOf srcs :: [String]
    srcs = do
      Expr Src Void
    loaded <-
        String -> m (Expr Src Void)
    forall (m :: * -> *). MonadIO m => String -> m (Expr Src Void)
    parseAndLoad ( [String] -> String
    unwords [String]
    srcs )

      Expr Src Void
    exprType <-
        Expr Src Void -> m (Expr Src Void)
    forall (m :: * -> *).
    (MonadIO m, MonadState Env m) =>
    Expr Src Void -> m (Expr Src Void)
    typeCheck Expr Src Void
    loaded

      Expr Src Void -> m ()
    forall a (m :: * -> *).
    (Pretty a, MonadState Env m, MonadIO m) =>
    Expr Src a -> m ()
    output Expr Src Void
    exprType

    applyContext
        :: Context Binding
        -> Dhall.Expr Dhall.Src Void
        -> Dhall.Expr Dhall.Src Void
    applyContext :: Context Binding -> Expr Src Void -> Expr Src Void
    applyContext context :: Context Binding
    context expression :: Expr Src Void
    expression =
        [Binding Src Void] -> Expr Src Void -> Expr Src Void
    forall (f :: * -> *) s a.
    Foldable f =>
    f (Binding s a) -> Expr s a -> Expr s a
    Dhall.Core.wrapInLets [Binding Src Void]
    bindings Expr Src Void
    expression
      where
        definitions :: [(Text, Binding)]
    definitions = [(Text, Binding)] -> [(Text, Binding)]
    forall a. [a] -> [a]
    reverse ([(Text, Binding)] -> [(Text, Binding)])
    -> [(Text, Binding)] -> [(Text, Binding)]
    forall a b. (a -> b) -> a -> b
    $ Context Binding -> [(Text, Binding)]
    forall a. Context a -> [(Text, a)]
    Dhall.Context.toList Context Binding
    context

        convertBinding :: (Text, Binding) -> Binding Src Void
    convertBinding (variable :: Text
    variable, Binding expr :: Expr Src Void
    expr _) =
            Maybe Src
    -> Text
    -> Maybe Src
    -> Maybe (Maybe Src, Expr Src Void)
    -> Maybe Src
    -> Expr Src Void
    -> Binding Src Void
    forall s a.
    Maybe s
    -> Text
    -> Maybe s
    -> Maybe (Maybe s, Expr s a)
    -> Maybe s
    -> Expr s a
    -> Binding s a
    Dhall.Core.Binding Maybe Src
    forall a. Maybe a
    Nothing Text
    variable Maybe Src
    forall a. Maybe a
    Nothing Maybe (Maybe Src, Expr Src Void)
    forall a. Maybe a
    Nothing Maybe Src
    forall a. Maybe a
    Nothing Expr Src Void
    expr

        bindings :: [Binding Src Void]
    bindings = ((Text, Binding) -> Binding Src Void)
    -> [(Text, Binding)] -> [Binding Src Void]
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    fmap (Text, Binding) -> Binding Src Void
    convertBinding [(Text, Binding)]
    definitions

    normalize
      :: MonadState Env m
      => Dhall.Expr Dhall.Src Void -> m ( Dhall.Expr t Void )
    normalize :: Expr Src Void -> m (Expr t Void)
    normalize e :: Expr Src Void
    e = do
      Env
    env <- m Env
    forall s (m :: * -> *). MonadState s m => m s
    get

      Expr t Void -> m (Expr t Void)
    forall (m :: * -> *) a. Monad m => a -> m a
    return (Expr Src Void -> Expr t Void
    forall a s t. Eq a => Expr s a -> Expr t a
    Dhall.normalize (Context Binding -> Expr Src Void -> Expr Src Void
    applyContext (Env -> Context Binding
    envToContext Env
    env) Expr Src Void
    e))

    typeCheck
      :: ( MonadIO m, MonadState Env m )
      => Dhall.Expr Dhall.Src Void -> m ( Dhall.Expr Dhall.Src Void )
    typeCheck :: Expr Src Void -> m (Expr Src Void)
    typeCheck expression :: Expr Src Void
    expression = do
      Env
    env <- m Env
    forall s (m :: * -> *). MonadState s m => m s
    get

      let wrap :: IO a -> IO a
    wrap = if Env -> Bool
    explain Env
    env then IO a -> IO a
    forall a. IO a -> IO a
    Dhall.detailed else IO a -> IO a
    forall a. a -> a
    id

      case Expr Src Void -> Either (TypeError Src Void) (Expr Src Void)
    forall s. Expr s Void -> Either (TypeError s Void) (Expr s Void)
    Dhall.typeOf (Context Binding -> Expr Src Void -> Expr Src Void
    applyContext (Env -> Context Binding
    envToContext Env
    env) Expr Src Void
    expression) of
        Left  e :: TypeError Src Void
    e -> IO (Expr Src Void) -> m (Expr Src Void)
    forall (m :: * -> *) a. MonadIO m => IO a -> m a
    liftIO ( IO (Expr Src Void) -> IO (Expr Src Void)
    forall a. IO a -> IO a
    wrap (TypeError Src Void -> IO (Expr Src Void)
    forall e a. Exception e => e -> IO a
    throwIO TypeError Src Void
    e) )
        Right a :: Expr Src Void
    a -> Expr Src Void -> m (Expr Src Void)
    forall (m :: * -> *) a. Monad m => a -> m a
    return Expr Src Void
    a

    -- Separate the equal sign to be its own word in order to simplify parsing
    -- This is intended to be used with the options that require assignment
    separateEqual :: [String] -> [String]
    separateEqual :: [String] -> [String]
    separateEqual [] =
        []
    separateEqual (str₀ :: String
    str₀ : ('=' : str₁ :: String
    str₁) : strs :: [String]
    strs) =
        String
    str₀ String -> [String] -> [String]
    forall a. a -> [a] -> [a]
    : "=" String -> [String] -> [String]
    forall a. a -> [a] -> [a]
    : String
    str₁ String -> [String] -> [String]
    forall a. a -> [a] -> [a]
    : [String]
    strs
    separateEqual (str :: String
    str : strs :: [String]
    strs)
        | (str₀ :: String
    str₀, '=' : str₁ :: String
    str₁) <- (Char -> Bool) -> String -> (String, String)
    forall a. (a -> Bool) -> [a] -> ([a], [a])
    break (Char -> Char -> Bool
    forall a. Eq a => a -> a -> Bool
    == '=') String
    str =
            String
    str₀ String -> [String] -> [String]
    forall a. a -> [a] -> [a]
    : "=" String -> [String] -> [String]
    forall a. a -> [a] -> [a]
    : String
    str₁ String -> [String] -> [String]
    forall a. a -> [a] -> [a]
    : [String]
    strs
        | Bool
    otherwise =
            String
    str String -> [String] -> [String]
    forall a. a -> [a] -> [a]
    : [String]
    strs

    addBinding :: ( MonadFail m, MonadIO m, MonadState Env m ) => [String] -> m ()
    addBinding :: [String] -> m ()
    addBinding (k :: String
    k : "=" : srcs :: [String]
    srcs) = do
      Text
    varName <- case Parsec Void Text Text
    -> String -> Text -> Either (ParseErrorBundle Text Void) Text
    forall e s a.
    Parsec e s a -> String -> s -> Either (ParseErrorBundle s e) a
    Megaparsec.parse (Parser Text -> Parsec Void Text Text
    forall a. Parser a -> Parsec Void Text a
    unParser Parser Text
    Parser.Token.label) "(input)" (String -> Text
    Text.pack String
    k) of
          Left   _      -> String -> m Text
    forall (m :: * -> *) a. MonadFail m => String -> m a
    Fail.fail "Invalid variable name"
          Right varName :: Text
    varName -> Text -> m Text
    forall (m :: * -> *) a. Monad m => a -> m a
    return Text
    varName

      Expr Src Void
    loaded <- String -> m (Expr Src Void)
    forall (m :: * -> *). MonadIO m => String -> m (Expr Src Void)
    parseAndLoad ( [String] -> String
    unwords [String]
    srcs )

      Expr Src Void
    t <- Expr Src Void -> m (Expr Src Void)
    forall (m :: * -> *).
    (MonadIO m, MonadState Env m) =>
    Expr Src Void -> m (Expr Src Void)
    typeCheck Expr Src Void
    loaded

      Expr Src Void
    expr <- Expr Src Void -> m (Expr Src Void)
    forall (m :: * -> *) t.
    MonadState Env m =>
    Expr Src Void -> m (Expr t Void)
    normalize Expr Src Void
    loaded

      (Env -> Env) -> m ()
    forall s (m :: * -> *). MonadState s m => (s -> s) -> m ()
    modify
        ( \e :: Env
    e ->
            Env
    e { envBindings :: Context Binding
    envBindings =
                  Text -> Binding -> Context Binding -> Context Binding
    forall a. Text -> a -> Context a -> Context a
    Dhall.Context.insert
                    Text
    varName
                    Binding :: Expr Src Void -> Expr Src Void -> Binding
    Binding { bindingType :: Expr Src Void
    bindingType = Expr Src Void
    t, bindingExpr :: Expr Src Void
    bindingExpr = Expr Src Void
    expr }
                    ( Env -> Context Binding
    envBindings Env
    e )
              }
        )

      Expr Src Void -> m ()
    forall a (m :: * -> *).
    (Pretty a, MonadState Env m, MonadIO m) =>
    Expr Src a -> m ()
    output ( Expr Src Void -> Expr Src Void -> Expr Src Void
    forall s a. Expr s a -> Expr s a -> Expr s a
    Expr.Annot ( Var -> Expr Src Void
    forall s a. Var -> Expr s a
    Expr.Var ( Text -> Int -> Var
    Dhall.V Text
    varName 0 ) ) Expr Src Void
    t )

    addBinding _ = String -> m ()
    forall (m :: * -> *) a. MonadFail m => String -> m a
    Fail.fail ":let should be of the form `:let x = y`"

    clearBindings :: (MonadFail m, MonadState Env m) => [String] -> m ()
    clearBindings :: [String] -> m ()
    clearBindings [] = (Env -> Env) -> m ()
    forall s (m :: * -> *). MonadState s m => (s -> s) -> m ()
    modify Env -> Env
    adapt
      where
        adapt :: Env -> Env
    adapt (Env {..}) = Env :: Context Binding
    -> Maybe Binding -> Bool -> CharacterSet -> Maybe Handle -> Env
    Env { envBindings :: Context Binding
    envBindings = Context Binding
    forall a. Context a
    Dhall.Context.empty, ..}

    clearBindings _ = String -> m ()
    forall (m :: * -> *) a. MonadFail m => String -> m a
    Fail.fail ":clear takes no arguments"

    hashBinding :: ( MonadFail m, MonadIO m, MonadState Env m ) => [String] -> m ()
    hashBinding :: [String] -> m ()
    hashBinding [] = String -> m ()
    forall (m :: * -> *) a. MonadFail m => String -> m a
    Fail.fail ":hash should be of the form `:hash expr"
    hashBinding tokens :: [String]
    tokens = do
      Expr Src Void
    loadedExpression <- String -> m (Expr Src Void)
    forall (m :: * -> *). MonadIO m => String -> m (Expr Src Void)
    parseAndLoad ([String] -> String
    unwords [String]
    tokens)

      Expr Src Void
    _ <- Expr Src Void -> m (Expr Src Void)
    forall (m :: * -> *).
    (MonadIO m, MonadState Env m) =>
    Expr Src Void -> m (Expr Src Void)
    typeCheck Expr Src Void
    loadedExpression

      Expr Void Void
    normalizedExpression <- Expr Src Void -> m (Expr Void Void)
    forall (m :: * -> *) t.
    MonadState Env m =>
    Expr Src Void -> m (Expr t Void)
    normalize Expr Src Void
    loadedExpression

      Text -> m ()
    forall (m :: * -> *). (MonadIO m, MonadState Env m) => Text -> m ()
    writeOutputHandle (Text -> m ()) -> Text -> m ()
    forall a b. (a -> b) -> a -> b
    $ Expr Void Void -> Text
    hashExpressionToCode Expr Void Void
    normalizedExpression

    saveFilePrefix :: FilePath
    saveFilePrefix :: String
    saveFilePrefix = ".dhall-repl"

    -- | Find the index for the current _active_ dhall save file
    currentSaveFileIndex :: MonadIO m => m (Maybe Int)
    currentSaveFileIndex :: m (Maybe Int)
    currentSaveFileIndex = do
      [String]
    files <- IO [String] -> m [String]
    forall (m :: * -> *) a. MonadIO m => IO a -> m a
    liftIO (IO [String] -> m [String]) -> IO [String] -> m [String]
    forall a b. (a -> b) -> a -> b
    $ String -> IO [String]
    getDirectoryContents "."

      let parseIndex :: String -> Maybe a
    parseIndex file :: String
    file
            | String
    saveFilePrefix String -> String -> Bool
    forall a. Eq a => [a] -> [a] -> Bool
    `isPrefixOf` String
    file
            , '-':index :: String
    index <- Int -> String -> String
    forall a. Int -> [a] -> [a]
    drop (String -> Int
    forall (t :: * -> *) a. Foldable t => t a -> Int
    length String
    saveFilePrefix) String
    file
            , [(x :: a
    x, "")] <- ReadS a
    forall a. Read a => ReadS a
    reads String
    index -- safe version of read
            = a -> Maybe a
    forall a. a -> Maybe a
    Just a
    x

            | Bool
    otherwise
            = Maybe a
    forall a. Maybe a
    Nothing

      Maybe Int -> m (Maybe Int)
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure (Maybe Int -> m (Maybe Int)) -> Maybe Int -> m (Maybe Int)
    forall a b. (a -> b) -> a -> b
    $ case (String -> Maybe Int) -> [String] -> [Int]
    forall a b. (a -> Maybe b) -> [a] -> [b]
    mapMaybe String -> Maybe Int
    forall a. Read a => String -> Maybe a
    parseIndex [String]
    files of
        [] -> Maybe Int
    forall a. Maybe a
    Nothing
        xs :: [Int]
    xs -> Int -> Maybe Int
    forall a. a -> Maybe a
    Just (Int -> Maybe Int) -> Int -> Maybe Int
    forall a b. (a -> b) -> a -> b
    $ [Int] -> Int
    forall (t :: * -> *) a. (Foldable t, Ord a) => t a -> a
    maximum [Int]
    xs

    -- | Find the name for the current _active_ dhall save file
    currentSaveFile :: MonadIO m => m (Maybe FilePath)
    currentSaveFile :: m (Maybe String)
    currentSaveFile =
      ((Maybe Int -> Maybe String) -> m (Maybe Int) -> m (Maybe String)
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    fmap ((Maybe Int -> Maybe String) -> m (Maybe Int) -> m (Maybe String))
    -> ((Int -> String) -> Maybe Int -> Maybe String)
    -> (Int -> String)
    -> m (Maybe Int)
    -> m (Maybe String)
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . (Int -> String) -> Maybe Int -> Maybe String
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    fmap) (\i :: Int
    i -> String
    saveFilePrefix String -> String -> String
    forall a. Semigroup a => a -> a -> a
    <> "-" String -> String -> String
    forall a. Semigroup a => a -> a -> a
    <> Int -> String
    forall a. Show a => a -> String
    show Int
    i) m (Maybe Int)
    forall (m :: * -> *). MonadIO m => m (Maybe Int)
    currentSaveFileIndex

    -- | Find the name for the next dhall save file
    nextSaveFile :: MonadIO m => m FilePath
    nextSaveFile :: m String
    nextSaveFile = do
      Maybe Int
    mIndex <- m (Maybe Int)
    forall (m :: * -> *). MonadIO m => m (Maybe Int)
    currentSaveFileIndex

      let nextIndex :: Int
    nextIndex = Int -> (Int -> Int) -> Maybe Int -> Int
    forall b a. b -> (a -> b) -> Maybe a -> b
    maybe 0 Int -> Int
    forall a. Enum a => a -> a
    succ Maybe Int
    mIndex

      String -> m String
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure (String -> m String) -> String -> m String
    forall a b. (a -> b) -> a -> b
    $ String
    saveFilePrefix String -> String -> String
    forall a. Semigroup a => a -> a -> a
    <> "-" String -> String -> String
    forall a. Semigroup a => a -> a -> a
    <> Int -> String
    forall a. Show a => a -> String
    show Int
    nextIndex

    loadBinding :: [String] -> Repl ()
    loadBinding :: [String] -> HaskelineT (StateT Env IO) ()
    loadBinding [] = do
      Maybe String
    mFile <- HaskelineT (StateT Env IO) (Maybe String)
    forall (m :: * -> *). MonadIO m => m (Maybe String)
    currentSaveFile

      case Maybe String
    mFile of
        Just file :: String
    file -> [String] -> HaskelineT (StateT Env IO) ()
    loadBinding [String
    file]
        Nothing   ->
          Command (HaskelineT (StateT Env IO))
    forall (m :: * -> *) a. MonadFail m => String -> m a
    Fail.fail Command (HaskelineT (StateT Env IO))
    -> Command (HaskelineT (StateT Env IO))
    forall a b. (a -> b) -> a -> b
    $ ":load couldn't find any `" String -> String -> String
    forall a. Semigroup a => a -> a -> a
    <> String
    saveFilePrefix String -> String -> String
    forall a. Semigroup a => a -> a -> a
    <> "-*` files"

    loadBinding [file :: String
    file] = do
      -- Read commands from the save file
      [[String]]
    replLines <- (String -> [String]) -> [String] -> [[String]]
    forall a b. (a -> b) -> [a] -> [b]
    map String -> [String]
    words ([String] -> [[String]])
    -> (String -> [String]) -> String -> [[String]]
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . String -> [String]
    lines (String -> [[String]])
    -> HaskelineT (StateT Env IO) String
    -> HaskelineT (StateT Env IO) [[String]]
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> IO String -> HaskelineT (StateT Env IO) String
    forall (m :: * -> *) a. MonadIO m => IO a -> m a
    liftIO (String -> IO String
    readFile String
    file)

      let runCommand :: [String] -> HaskelineT (StateT Env IO) ()
    runCommand ((c :: Char
    c:cmd :: String
    cmd):opts :: [String]
    opts)
            | Char
    c Char -> Char -> Bool
    forall a. Eq a => a -> a -> Bool
    == Char
    optionsPrefix
            , Just action :: [String] -> HaskelineT (StateT Env IO) ()
    action <- String
    -> Options (HaskelineT (StateT Env IO))
    -> Maybe ([String] -> HaskelineT (StateT Env IO) ())
    forall a b. Eq a => a -> [(a, b)] -> Maybe b
    lookup String
    cmd Options (HaskelineT (StateT Env IO))
    options
            = [String] -> HaskelineT (StateT Env IO) ()
    action [String]
    opts
          runCommand _ = Command (HaskelineT (StateT Env IO))
    forall (m :: * -> *) a. MonadFail m => String -> m a
    Fail.fail Command (HaskelineT (StateT Env IO))
    -> Command (HaskelineT (StateT Env IO))
    forall a b. (a -> b) -> a -> b
    $
            ":load expects `" String -> String -> String
    forall a. Semigroup a => a -> a -> a
    <> String
    file String -> String -> String
    forall a. Semigroup a => a -> a -> a
    <> "` to contain one command per line"

      -- Keep current handle in scope
      Env { Maybe Handle
    outputHandle :: Maybe Handle
    outputHandle :: Env -> Maybe Handle
    outputHandle } <- HaskelineT (StateT Env IO) Env
    forall s (m :: * -> *). MonadState s m => m s
    get

      -- Discard output
      (Env -> Env) -> HaskelineT (StateT Env IO) ()
    forall s (m :: * -> *). MonadState s m => (s -> s) -> m ()
    modify (\e :: Env
    e -> Env
    e { outputHandle :: Maybe Handle
    outputHandle = Maybe Handle
    forall a. Maybe a
    Nothing })

      -- Run all the commands
      [[String]]
    -> ([String] -> HaskelineT (StateT Env IO) ())
    -> HaskelineT (StateT Env IO) ()
    forall (t :: * -> *) (m :: * -> *) a b.
    (Foldable t, Monad m) =>
    t a -> (a -> m b) -> m ()
    forM_ [[String]]
    replLines [String] -> HaskelineT (StateT Env IO) ()
    runCommand

      -- Restore the previous handle
      (Env -> Env) -> HaskelineT (StateT Env IO) ()
    forall s (m :: * -> *). MonadState s m => (s -> s) -> m ()
    modify (\e :: Env
    e -> Env
    e { outputHandle :: Maybe Handle
    outputHandle = Maybe Handle
    outputHandle })

      Text -> HaskelineT (StateT Env IO) ()
    forall (m :: * -> *). (MonadIO m, MonadState Env m) => Text -> m ()
    writeOutputHandle (Text -> HaskelineT (StateT Env IO) ())
    -> Text -> HaskelineT (StateT Env IO) ()
    forall a b. (a -> b) -> a -> b
    $ "Loaded `" Text -> Text -> Text
    forall a. Semigroup a => a -> a -> a
    <> String -> Text
    Text.pack String
    file Text -> Text -> Text
    forall a. Semigroup a => a -> a -> a
    <> "`\n"

    loadBinding _ = Command (HaskelineT (StateT Env IO))
    forall (m :: * -> *) a. MonadFail m => String -> m a
    Fail.fail ":load should be of the form `:load` or `:load file`"

    saveBinding :: ( MonadFail m, MonadIO m, MonadState Env m ) => [String] -> m ()
    -- Save all the bindings into a context save file
    saveBinding :: [String] -> m ()
    saveBinding [] = do
      String
    file <- m String
    forall (m :: * -> *). MonadIO m => m String
    nextSaveFile

      [String] -> m ()
    forall (m :: * -> *).
    (MonadFail m, MonadIO m, MonadState Env m) =>
    [String] -> m ()
    saveBinding [String
    file]

    -- Save all the bindings into `file`
    saveBinding [file :: String
    file] = do
      Env
    env <- m Env
    forall s (m :: * -> *). MonadState s m => m s
    get

      let bindings :: [(Text, Expr Src Void)]
    bindings
            = [(Text, Expr Src Void)] -> [(Text, Expr Src Void)]
    forall a. [a] -> [a]
    reverse
            ([(Text, Expr Src Void)] -> [(Text, Expr Src Void)])
    -> (Context Binding -> [(Text, Expr Src Void)])
    -> Context Binding
    -> [(Text, Expr Src Void)]
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . (((Text, Binding) -> (Text, Expr Src Void))
    -> [(Text, Binding)] -> [(Text, Expr Src Void)]
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    fmap (((Text, Binding) -> (Text, Expr Src Void))
     -> [(Text, Binding)] -> [(Text, Expr Src Void)])
    -> ((Binding -> Expr Src Void)
        -> (Text, Binding) -> (Text, Expr Src Void))
    -> (Binding -> Expr Src Void)
    -> [(Text, Binding)]
    -> [(Text, Expr Src Void)]
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . (Binding -> Expr Src Void)
    -> (Text, Binding) -> (Text, Expr Src Void)
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    fmap) Binding -> Expr Src Void
    bindingExpr
            ([(Text, Binding)] -> [(Text, Expr Src Void)])
    -> (Context Binding -> [(Text, Binding)])
    -> Context Binding
    -> [(Text, Expr Src Void)]
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Context Binding -> [(Text, Binding)]
    forall a. Context a -> [(Text, a)]
    Dhall.Context.toList
            (Context Binding -> [(Text, Expr Src Void)])
    -> Context Binding -> [(Text, Expr Src Void)]
    forall a b. (a -> b) -> a -> b
    $ Env -> Context Binding
    envBindings Env
    env

          handler :: Handle -> m ()
    handler handle :: Handle
    handle =
              StateT Env m () -> Env -> m ()
    forall (m :: * -> *) s a. Monad m => StateT s m a -> s -> m a
    State.evalStateT
                ([(Text, Expr Src Void)]
    -> ((Text, Expr Src Void) -> StateT Env m ()) -> StateT Env m ()
    forall (t :: * -> *) (m :: * -> *) a b.
    (Foldable t, Monad m) =>
    t a -> (a -> m b) -> m ()
    forM_ [(Text, Expr Src Void)]
    bindings (((Text, Expr Src Void) -> StateT Env m ()) -> StateT Env m ())
    -> ((Text, Expr Src Void) -> StateT Env m ()) -> StateT Env m ()
    forall a b. (a -> b) -> a -> b
    $ \(name :: Text
    name, expr :: Expr Src Void
    expr) -> do
                  let doc :: Doc Ann
    doc = Text -> Doc Ann
    Dhall.Pretty.Internal.prettyLabel Text
    name

                  let label :: Text
    label = Doc Ann -> Text
    forall ann. Doc ann -> Text
    Dhall.Pretty.Internal.docToStrictText Doc Ann
    doc

                  IO () -> StateT Env m ()
    forall (m :: * -> *) a. MonadIO m => IO a -> m a
    liftIO (Handle -> String -> IO ()
    System.IO.hPutStr Handle
    handle (String -> IO ()) -> String -> IO ()
    forall a b. (a -> b) -> a -> b
    $ ":let " String -> String -> String
    forall a. Semigroup a => a -> a -> a
    <> Text -> String
    Text.unpack Text
    label String -> String -> String
    forall a. Semigroup a => a -> a -> a
    <> " = ")
                  Expr Src Void -> StateT Env m ()
    forall a (m :: * -> *).
    (Pretty a, MonadState Env m, MonadIO m) =>
    Expr Src a -> m ()
    outputWithoutSpacing Expr Src Void
    expr)
                (Env
    env { outputHandle :: Maybe Handle
    outputHandle = Handle -> Maybe Handle
    forall a. a -> Maybe a
    Just Handle
    handle })

      IO () -> m ()
    forall (m :: * -> *) a. MonadIO m => IO a -> m a
    liftIO (String -> IOMode -> (Handle -> IO ()) -> IO ()
    forall r. String -> IOMode -> (Handle -> IO r) -> IO r
    System.IO.withFile String
    file IOMode
    System.IO.WriteMode Handle -> IO ()
    forall (m :: * -> *). MonadIO m => Handle -> m ()
    handler)

      Text -> m ()
    forall (m :: * -> *). (MonadIO m, MonadState Env m) => Text -> m ()
    writeOutputHandle (Text -> m ()) -> Text -> m ()
    forall a b. (a -> b) -> a -> b
    $ "Context saved to `" Text -> Text -> Text
    forall a. Semigroup a => a -> a -> a
    <> String -> Text
    Text.pack String
    file Text -> Text -> Text
    forall a. Semigroup a => a -> a -> a
    <> "`\n"

    -- Save a single expression to `file`
    saveBinding (file :: String
    file : "=" : tokens :: [String]
    tokens) = do
      Expr Src Void
    loadedExpression <- String -> m (Expr Src Void)
    forall (m :: * -> *). MonadIO m => String -> m (Expr Src Void)
    parseAndLoad ([String] -> String
    unwords [String]
    tokens)

      Expr Src Void
    _ <- Expr Src Void -> m (Expr Src Void)
    forall (m :: * -> *).
    (MonadIO m, MonadState Env m) =>
    Expr Src Void -> m (Expr Src Void)
    typeCheck Expr Src Void
    loadedExpression

      Expr Src Void
    normalizedExpression <- Expr Src Void -> m (Expr Src Void)
    forall (m :: * -> *) t.
    MonadState Env m =>
    Expr Src Void -> m (Expr t Void)
    normalize Expr Src Void
    loadedExpression

      Env
    env <- m Env
    forall s (m :: * -> *). MonadState s m => m s
    get

      let handler :: Handle -> m ()
    handler handle :: Handle
    handle =
              StateT Env m () -> Env -> m ()
    forall (m :: * -> *) s a. Monad m => StateT s m a -> s -> m a
    State.evalStateT
                (Expr Src Void -> StateT Env m ()
    forall a (m :: * -> *).
    (Pretty a, MonadState Env m, MonadIO m) =>
    Expr Src a -> m ()
    output Expr Src Void
    normalizedExpression)
                (Env
    env { outputHandle :: Maybe Handle
    outputHandle = Handle -> Maybe Handle
    forall a. a -> Maybe a
    Just Handle
    handle })

      IO () -> m ()
    forall (m :: * -> *) a. MonadIO m => IO a -> m a
    liftIO (String -> IOMode -> (Handle -> IO ()) -> IO ()
    forall r. String -> IOMode -> (Handle -> IO r) -> IO r
    System.IO.withFile String
    file IOMode
    System.IO.WriteMode Handle -> IO ()
    forall (m :: * -> *). MonadIO m => Handle -> m ()
    handler)

      Text -> m ()
    forall (m :: * -> *). (MonadIO m, MonadState Env m) => Text -> m ()
    writeOutputHandle (Text -> m ()) -> Text -> m ()
    forall a b. (a -> b) -> a -> b
    $ "Expression saved to `" Text -> Text -> Text
    forall a. Semigroup a => a -> a -> a
    <> String -> Text
    Text.pack String
    file Text -> Text -> Text
    forall a. Semigroup a => a -> a -> a
    <> "`\n"

    saveBinding _ = String -> m ()
    forall (m :: * -> *) a. MonadFail m => String -> m a
    Fail.fail ":save should be of the form `:save`, `:save file`, or `:save file = expr`"

    setOption :: ( MonadIO m, MonadState Env m ) => [String] -> m ()
    setOption :: [String] -> m ()
    setOption [ "--explain" ] = do
      (Env -> Env) -> m ()
    forall s (m :: * -> *). MonadState s m => (s -> s) -> m ()
    modify (\e :: Env
    e -> Env
    e { explain :: Bool
    explain = Bool
    True })
    setOption _ = do
      Text -> m ()
    forall (m :: * -> *). (MonadIO m, MonadState Env m) => Text -> m ()
    writeOutputHandle ":set should be of the form `:set <command line option>`"

    unsetOption :: ( MonadIO m, MonadState Env m ) => [String] -> m ()
    unsetOption :: [String] -> m ()
    unsetOption [ "--explain" ] = do
      (Env -> Env) -> m ()
    forall s (m :: * -> *). MonadState s m => (s -> s) -> m ()
    modify (\e :: Env
    e -> Env
    e { explain :: Bool
    explain = Bool
    False })
    unsetOption _ = do
      Text -> m ()
    forall (m :: * -> *). (MonadIO m, MonadState Env m) => Text -> m ()
    writeOutputHandle ":unset should be of the form `:unset <command line option>`"

    cmdQuit :: ( MonadIO m, MonadState Env m ) => [String] -> m ()
    cmdQuit :: [String] -> m ()
    cmdQuit _ = do
      IO () -> m ()
    forall (m :: * -> *) a. MonadIO m => IO a -> m a
    liftIO (String -> IO ()
    putStrLn "Goodbye.")
      IO () -> m ()
    forall (m :: * -> *) a. MonadIO m => IO a -> m a
    liftIO (Interrupt -> IO ()
    forall e a. Exception e => e -> IO a
    throwIO Interrupt
    Interrupt)

    help
      :: ( MonadFail m, MonadIO m, MonadState Env m )
      => HelpOptions m -> [String] -> m ()
    help :: HelpOptions m -> [String] -> m ()
    help hs :: HelpOptions m
    hs _ = do
      IO () -> m ()
    forall (m :: * -> *) a. MonadIO m => IO a -> m a
    liftIO (String -> IO ()
    putStrLn "Type any expression to normalize it or use one of the following commands:")
      HelpOptions m -> (HelpOption m -> m ()) -> m ()
    forall (t :: * -> *) (m :: * -> *) a b.
    (Foldable t, Monad m) =>
    t a -> (a -> m b) -> m ()
    forM_ HelpOptions m
    hs ((HelpOption m -> m ()) -> m ()) -> (HelpOption m -> m ()) -> m ()
    forall a b. (a -> b) -> a -> b
    $ \h :: HelpOption m
    h -> do
        let name :: String
    name = HelpOption m -> String
    forall (m :: * -> *). HelpOption m -> String
    helpOptionName HelpOption m
    h
            syntax :: String
    syntax = HelpOption m -> String
    forall (m :: * -> *). HelpOption m -> String
    helpOptionSyntax HelpOption m
    h
            doc :: String
    doc = HelpOption m -> String
    forall (m :: * -> *). HelpOption m -> String
    helpOptionDoc HelpOption m
    h
        IO () -> m ()
    forall (m :: * -> *) a. MonadIO m => IO a -> m a
    liftIO (String -> IO ()
    putStrLn (":" String -> String -> String
    forall a. Semigroup a => a -> a -> a
    <> String
    name String -> String -> String
    forall a. Semigroup a => a -> a -> a
    <> " " String -> String -> String
    forall a. Semigroup a => a -> a -> a
    <> String
    syntax))
        IO () -> m ()
    forall (m :: * -> *) a. MonadIO m => IO a -> m a
    liftIO (String -> IO ()
    putStrLn ("    " String -> String -> String
    forall a. Semigroup a => a -> a -> a
    <> String
    doc))

    optionsPrefix :: Char
    optionsPrefix :: Char
    optionsPrefix = ':'

    data HelpOption m = HelpOption
      { HelpOption m -> String
    helpOptionName :: String
      , HelpOption m -> String
    helpOptionSyntax :: String
      , HelpOption m -> String
    helpOptionDoc :: String
      , HelpOption m -> Cmd m
    helpOptionFunction :: Repline.Cmd m
      }

    type HelpOptions m = [HelpOption m]

    helpOptions :: HelpOptions Repl
    helpOptions :: HelpOptions (HaskelineT (StateT Env IO))
    helpOptions =
      [ String
    -> String
    -> String
    -> ([String] -> HaskelineT (StateT Env IO) ())
    -> HelpOption (HaskelineT (StateT Env IO))
    forall (m :: * -> *).
    String -> String -> String -> Cmd m -> HelpOption m
    HelpOption
          "help"
          ""
          "Print help text and describe options"
          (HaskelineT (StateT Env IO) () -> HaskelineT (StateT Env IO) ()
    dontCrash (HaskelineT (StateT Env IO) () -> HaskelineT (StateT Env IO) ())
    -> ([String] -> HaskelineT (StateT Env IO) ())
    -> [String]
    -> HaskelineT (StateT Env IO) ()
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . HelpOptions (HaskelineT (StateT Env IO))
    -> [String] -> HaskelineT (StateT Env IO) ()
    forall (m :: * -> *).
    (MonadFail m, MonadIO m, MonadState Env m) =>
    HelpOptions m -> [String] -> m ()
    help HelpOptions (HaskelineT (StateT Env IO))
    helpOptions)
      , String
    -> String
    -> String
    -> ([String] -> HaskelineT (StateT Env IO) ())
    -> HelpOption (HaskelineT (StateT Env IO))
    forall (m :: * -> *).
    String -> String -> String -> Cmd m -> HelpOption m
    HelpOption
          "type"
          "EXPRESSION"
          "Infer the type of an expression"
          (HaskelineT (StateT Env IO) () -> HaskelineT (StateT Env IO) ()
    dontCrash (HaskelineT (StateT Env IO) () -> HaskelineT (StateT Env IO) ())
    -> ([String] -> HaskelineT (StateT Env IO) ())
    -> [String]
    -> HaskelineT (StateT Env IO) ()
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . [String] -> HaskelineT (StateT Env IO) ()
    forall (m :: * -> *).
    (MonadFail m, MonadIO m, MonadState Env m) =>
    [String] -> m ()
    typeOf)
      , String
    -> String
    -> String
    -> ([String] -> HaskelineT (StateT Env IO) ())
    -> HelpOption (HaskelineT (StateT Env IO))
    forall (m :: * -> *).
    String -> String -> String -> Cmd m -> HelpOption m
    HelpOption
          "hash"
          "EXPRESSION"
          "Hash the normalized value of an expression"
          (HaskelineT (StateT Env IO) () -> HaskelineT (StateT Env IO) ()
    dontCrash (HaskelineT (StateT Env IO) () -> HaskelineT (StateT Env IO) ())
    -> ([String] -> HaskelineT (StateT Env IO) ())
    -> [String]
    -> HaskelineT (StateT Env IO) ()
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . [String] -> HaskelineT (StateT Env IO) ()
    forall (m :: * -> *).
    (MonadFail m, MonadIO m, MonadState Env m) =>
    [String] -> m ()
    hashBinding)
      , String
    -> String
    -> String
    -> ([String] -> HaskelineT (StateT Env IO) ())
    -> HelpOption (HaskelineT (StateT Env IO))
    forall (m :: * -> *).
    String -> String -> String -> Cmd m -> HelpOption m
    HelpOption
          "let"
          "IDENTIFIER = EXPRESSION"
          "Assign an expression to a variable"
          (HaskelineT (StateT Env IO) () -> HaskelineT (StateT Env IO) ()
    dontCrash (HaskelineT (StateT Env IO) () -> HaskelineT (StateT Env IO) ())
    -> ([String] -> HaskelineT (StateT Env IO) ())
    -> [String]
    -> HaskelineT (StateT Env IO) ()
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . [String] -> HaskelineT (StateT Env IO) ()
    forall (m :: * -> *).
    (MonadFail m, MonadIO m, MonadState Env m) =>
    [String] -> m ()
    addBinding ([String] -> HaskelineT (StateT Env IO) ())
    -> ([String] -> [String])
    -> [String]
    -> HaskelineT (StateT Env IO) ()
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . [String] -> [String]
    separateEqual)
      , String
    -> String
    -> String
    -> ([String] -> HaskelineT (StateT Env IO) ())
    -> HelpOption (HaskelineT (StateT Env IO))
    forall (m :: * -> *).
    String -> String -> String -> Cmd m -> HelpOption m
    HelpOption
          "clear"
          ""
          "Clear all bound variables"
          (HaskelineT (StateT Env IO) () -> HaskelineT (StateT Env IO) ()
    dontCrash (HaskelineT (StateT Env IO) () -> HaskelineT (StateT Env IO) ())
    -> ([String] -> HaskelineT (StateT Env IO) ())
    -> [String]
    -> HaskelineT (StateT Env IO) ()
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . [String] -> HaskelineT (StateT Env IO) ()
    forall (m :: * -> *).
    (MonadFail m, MonadState Env m) =>
    [String] -> m ()
    clearBindings)
      , String
    -> String
    -> String
    -> ([String] -> HaskelineT (StateT Env IO) ())
    -> HelpOption (HaskelineT (StateT Env IO))
    forall (m :: * -> *).
    String -> String -> String -> Cmd m -> HelpOption m
    HelpOption
          "load"
          "[FILENAME]"
          "Load bound variables from a file"
          (HaskelineT (StateT Env IO) () -> HaskelineT (StateT Env IO) ()
    dontCrash (HaskelineT (StateT Env IO) () -> HaskelineT (StateT Env IO) ())
    -> ([String] -> HaskelineT (StateT Env IO) ())
    -> [String]
    -> HaskelineT (StateT Env IO) ()
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . [String] -> HaskelineT (StateT Env IO) ()
    loadBinding)
      , String
    -> String
    -> String
    -> ([String] -> HaskelineT (StateT Env IO) ())
    -> HelpOption (HaskelineT (StateT Env IO))
    forall (m :: * -> *).
    String -> String -> String -> Cmd m -> HelpOption m
    HelpOption
          "save"
          "[FILENAME | FILENAME = EXPRESSION]"
          "Save bound variables or a given expression to a file"
          (HaskelineT (StateT Env IO) () -> HaskelineT (StateT Env IO) ()
    dontCrash (HaskelineT (StateT Env IO) () -> HaskelineT (StateT Env IO) ())
    -> ([String] -> HaskelineT (StateT Env IO) ())
    -> [String]
    -> HaskelineT (StateT Env IO) ()
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . [String] -> HaskelineT (StateT Env IO) ()
    forall (m :: * -> *).
    (MonadFail m, MonadIO m, MonadState Env m) =>
    [String] -> m ()
    saveBinding ([String] -> HaskelineT (StateT Env IO) ())
    -> ([String] -> [String])
    -> [String]
    -> HaskelineT (StateT Env IO) ()
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . [String] -> [String]
    separateEqual)
      , String
    -> String
    -> String
    -> ([String] -> HaskelineT (StateT Env IO) ())
    -> HelpOption (HaskelineT (StateT Env IO))
    forall (m :: * -> *).
    String -> String -> String -> Cmd m -> HelpOption m
    HelpOption
          "set"
          "OPTION"
          "Set an option. Currently supported: --explain"
          (HaskelineT (StateT Env IO) () -> HaskelineT (StateT Env IO) ()
    dontCrash (HaskelineT (StateT Env IO) () -> HaskelineT (StateT Env IO) ())
    -> ([String] -> HaskelineT (StateT Env IO) ())
    -> [String]
    -> HaskelineT (StateT Env IO) ()
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . [String] -> HaskelineT (StateT Env IO) ()
    forall (m :: * -> *).
    (MonadIO m, MonadState Env m) =>
    [String] -> m ()
    setOption)
      , String
    -> String
    -> String
    -> ([String] -> HaskelineT (StateT Env IO) ())
    -> HelpOption (HaskelineT (StateT Env IO))
    forall (m :: * -> *).
    String -> String -> String -> Cmd m -> HelpOption m
    HelpOption
          "unset"
          "OPTION"
          "Unset an option"
          (HaskelineT (StateT Env IO) () -> HaskelineT (StateT Env IO) ()
    dontCrash (HaskelineT (StateT Env IO) () -> HaskelineT (StateT Env IO) ())
    -> ([String] -> HaskelineT (StateT Env IO) ())
    -> [String]
    -> HaskelineT (StateT Env IO) ()
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . [String] -> HaskelineT (StateT Env IO) ()
    forall (m :: * -> *).
    (MonadIO m, MonadState Env m) =>
    [String] -> m ()
    unsetOption)
      , String
    -> String
    -> String
    -> ([String] -> HaskelineT (StateT Env IO) ())
    -> HelpOption (HaskelineT (StateT Env IO))
    forall (m :: * -> *).
    String -> String -> String -> Cmd m -> HelpOption m
    HelpOption
          "quit"
          ""
          "Exit the REPL"
          [String] -> HaskelineT (StateT Env IO) ()
    forall (m :: * -> *).
    (MonadIO m, MonadState Env m) =>
    [String] -> m ()
    cmdQuit
      ]

    options :: Repline.Options Repl
    options :: Options (HaskelineT (StateT Env IO))
    options = (\h :: HelpOption (HaskelineT (StateT Env IO))
    h -> (HelpOption (HaskelineT (StateT Env IO)) -> String
    forall (m :: * -> *). HelpOption m -> String
    helpOptionName HelpOption (HaskelineT (StateT Env IO))
    h, HelpOption (HaskelineT (StateT Env IO))
    -> [String] -> HaskelineT (StateT Env IO) ()
    forall (m :: * -> *). HelpOption m -> Cmd m
    helpOptionFunction HelpOption (HaskelineT (StateT Env IO))
    h)) (HelpOption (HaskelineT (StateT Env IO))
     -> (String, [String] -> HaskelineT (StateT Env IO) ()))
    -> HelpOptions (HaskelineT (StateT Env IO))
    -> Options (HaskelineT (StateT Env IO))
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> HelpOptions (HaskelineT (StateT Env IO))
    helpOptions

    completer
      :: (Monad m, MonadFail m, MonadIO m, MonadState Env m)
      => Repline.CompleterStyle m
    completer :: CompleterStyle m
    completer =
      CompletionFunc m
    -> [(String, CompletionFunc m)] -> CompleterStyle m
    forall (m :: * -> *).
    CompletionFunc m
    -> [(String, CompletionFunc m)] -> CompleterStyle m
    Repline.Prefix
        (Maybe Char
    -> String
    -> (String -> String -> m [Completion])
    -> CompletionFunc m
    forall (m :: * -> *).
    Monad m =>
    Maybe Char
    -> String
    -> (String -> String -> m [Completion])
    -> CompletionFunc m
    Haskeline.completeWordWithPrev (Char -> Maybe Char
    forall a. a -> Maybe a
    Just '\\') String
    separators String -> String -> m [Completion]
    forall (m :: * -> *).
    (Monad m, MonadFail m, MonadIO m, MonadState Env m) =>
    String -> String -> m [Completion]
    completeFunc)
        []
      where
        -- Separators that can be found on the left of something we want to
        -- autocomplete
        separators :: String
        separators :: String
    separators = " \t[(,=+*&|}#?>:"

    completeFunc
      :: (Monad m, MonadFail m, MonadIO m, MonadState Env m)
      => String -> String -> m [Completion]
    completeFunc :: String -> String -> m [Completion]
    completeFunc reversedPrev :: String
    reversedPrev word :: String
    word

      -- Complete commands
      | String
    reversedPrev String -> String -> Bool
    forall a. Eq a => a -> a -> Bool
    == ":"
      = [Completion] -> m [Completion]
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure ([Completion] -> m [Completion])
    -> ([String] -> [Completion]) -> [String] -> m [Completion]
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . [String] -> [Completion]
    listCompletion ([String] -> m [Completion]) -> [String] -> m [Completion]
    forall a b. (a -> b) -> a -> b
    $ (String, [String] -> HaskelineT (StateT Env IO) ()) -> String
    forall a b. (a, b) -> a
    fst ((String, [String] -> HaskelineT (StateT Env IO) ()) -> String)
    -> Options (HaskelineT (StateT Env IO)) -> [String]
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> (Options (HaskelineT (StateT Env IO))
    options :: Repline.Options Repl)

      -- Complete load command
      | String
    reversedPrev String -> String -> Bool
    forall a. Eq a => a -> a -> Bool
    == String -> String
    forall a. [a] -> [a]
    reverse ":load "
      = String -> m [Completion]
    forall (m :: * -> *). MonadIO m => String -> m [Completion]
    Haskeline.listFiles String
    word

      -- Complete file paths
      | (String -> Bool) -> [String] -> Bool
    forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
    any (String -> String -> Bool
    forall a. Eq a => [a] -> [a] -> Bool
    `isPrefixOf` String
    word) [ "/", "./", "../", "~/" ]
      = String -> m [Completion]
    forall (m :: * -> *). MonadIO m => String -> m [Completion]
    Haskeline.listFiles String
    word

      -- Complete environment variables
      | String -> String
    forall a. [a] -> [a]
    reverse "env:" String -> String -> Bool
    forall a. Eq a => [a] -> [a] -> Bool
    `isPrefixOf` String
    reversedPrev
      = [String] -> [Completion]
    listCompletion ([String] -> [Completion])
    -> ([(String, String)] -> [String])
    -> [(String, String)]
    -> [Completion]
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . ((String, String) -> String) -> [(String, String)] -> [String]
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    fmap (String, String) -> String
    forall a b. (a, b) -> a
    fst ([(String, String)] -> [Completion])
    -> m [(String, String)] -> m [Completion]
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> IO [(String, String)] -> m [(String, String)]
    forall (m :: * -> *) a. MonadIO m => IO a -> m a
    liftIO IO [(String, String)]
    getEnvironment

      -- Complete record fields and union alternatives
      | var :: Text
    var : subFields :: [Text]
    subFields <- (Char -> Bool) -> Text -> [Text]
    Text.split (Char -> Char -> Bool
    forall a. Eq a => a -> a -> Bool
    == '.') (String -> Text
    Text.pack String
    word)
      , Bool -> Bool
    not (Bool -> Bool) -> Bool -> Bool
    forall a b. (a -> b) -> a -> b
    $ [Text] -> Bool
    forall (t :: * -> *) a. Foldable t => t a -> Bool
    null [Text]
    subFields
      = do
        Env { Context Binding
    envBindings :: Context Binding
    envBindings :: Env -> Context Binding
    envBindings } <- m Env
    forall s (m :: * -> *). MonadState s m => m s
    get

        case Text -> Int -> Context Binding -> Maybe Binding
    forall a. Text -> Int -> Context a -> Maybe a
    Dhall.Context.lookup Text
    var 0 Context Binding
    envBindings of

          Nothing -> [Completion] -> m [Completion]
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure []

          Just binding :: Binding
    binding -> do
            let candidates :: [Text]
    candidates = [Text] -> Expr Src Void -> [Text]
    algebraicComplete [Text]
    subFields (Binding -> Expr Src Void
    bindingExpr Binding
    binding)
            [Completion] -> m [Completion]
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure ([Completion] -> m [Completion]) -> [Completion] -> m [Completion]
    forall a b. (a -> b) -> a -> b
    $ [String] -> [Completion]
    listCompletion (Text -> String
    Text.unpack (Text -> String) -> (Text -> Text) -> Text -> String
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . (Text
    var Text -> Text -> Text
    forall a. Semigroup a => a -> a -> a
    <>) (Text -> String) -> [Text] -> [String]
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> [Text]
    candidates)

      -- Complete variables in scope and all reserved identifiers
      | Bool
    otherwise
      = do
        Env { Context Binding
    envBindings :: Context Binding
    envBindings :: Env -> Context Binding
    envBindings } <- m Env
    forall s (m :: * -> *). MonadState s m => m s
    get

        let vars :: [Text]
    vars     = ((Text, Binding) -> Text) -> [(Text, Binding)] -> [Text]
    forall a b. (a -> b) -> [a] -> [b]
    map (Text, Binding) -> Text
    forall a b. (a, b) -> a
    fst ([(Text, Binding)] -> [Text]) -> [(Text, Binding)] -> [Text]
    forall a b. (a -> b) -> a -> b
    $ Context Binding -> [(Text, Binding)]
    forall a. Context a -> [(Text, a)]
    Dhall.Context.toList Context Binding
    envBindings
            reserved :: [Text]
    reserved = HashSet Text -> [Text]
    forall a. HashSet a -> [a]
    Data.HashSet.toList HashSet Text
    Dhall.Core.reservedIdentifiers

        [Completion] -> m [Completion]
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure ([Completion] -> m [Completion])
    -> ([Text] -> [Completion]) -> [Text] -> m [Completion]
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . [String] -> [Completion]
    listCompletion ([String] -> [Completion])
    -> ([Text] -> [String]) -> [Text] -> [Completion]
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . (Text -> String) -> [Text] -> [String]
    forall a b. (a -> b) -> [a] -> [b]
    map Text -> String
    Text.unpack ([Text] -> [String]) -> ([Text] -> [Text]) -> [Text] -> [String]
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . [Text] -> [Text]
    forall a. Eq a => [a] -> [a]
    nub ([Text] -> m [Completion]) -> [Text] -> m [Completion]
    forall a b. (a -> b) -> a -> b
    $ [Text]
    vars [Text] -> [Text] -> [Text]
    forall a. [a] -> [a] -> [a]
    ++ [Text]
    reserved

      where
        listCompletion :: [String] -> [Completion]
    listCompletion = (String -> Completion) -> [String] -> [Completion]
    forall a b. (a -> b) -> [a] -> [b]
    map String -> Completion
    simpleCompletion ([String] -> [Completion])
    -> ([String] -> [String]) -> [String] -> [Completion]
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . (String -> Bool) -> [String] -> [String]
    forall a. (a -> Bool) -> [a] -> [a]
    filter (String
    word String -> String -> Bool
    forall a. Eq a => [a] -> [a] -> Bool
    `isPrefixOf`)

        algebraicComplete
            :: [Text.Text] -> Dhall.Expr Dhall.Src Void -> [Text.Text]
        algebraicComplete :: [Text] -> Expr Src Void -> [Text]
    algebraicComplete subFields :: [Text]
    subFields expr :: Expr Src Void
    expr =
          let keys :: Map Text v -> [Text]
    keys = (Text -> Text) -> [Text] -> [Text]
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    fmap ("." Text -> Text -> Text
    forall a. Semigroup a => a -> a -> a
    <>) ([Text] -> [Text])
    -> (Map Text v -> [Text]) -> Map Text v -> [Text]
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Map Text v -> [Text]
    forall k v. Map k v -> [k]
    Map.keys

              withMap :: Map Text (Maybe (Expr Src Void)) -> [Text]
    withMap m :: Map Text (Maybe (Expr Src Void))
    m =
                  case [Text]
    subFields of
                      [] -> Map Text (Maybe (Expr Src Void)) -> [Text]
    forall v. Map Text v -> [Text]
    keys Map Text (Maybe (Expr Src Void))
    m
                      -- Stop on last subField (we care about the keys at this level)
                      [_] -> Map Text (Maybe (Expr Src Void)) -> [Text]
    forall v. Map Text v -> [Text]
    keys Map Text (Maybe (Expr Src Void))
    m
                      f :: Text
    f:fs :: [Text]
    fs ->
                          case Text
    -> Map Text (Maybe (Expr Src Void))
    -> Maybe (Maybe (Expr Src Void))
    forall k v. Ord k => k -> Map k v -> Maybe v
    Map.lookup Text
    f Map Text (Maybe (Expr Src Void))
    m of
                              Nothing ->
                                  []
                              Just Nothing ->
                                  Map Text (Maybe (Expr Src Void)) -> [Text]
    forall v. Map Text v -> [Text]
    keys Map Text (Maybe (Expr Src Void))
    m
                              Just (Just e :: Expr Src Void
    e) ->
                                  (Text -> Text) -> [Text] -> [Text]
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    fmap (("." Text -> Text -> Text
    forall a. Semigroup a => a -> a -> a
    <> Text
    f) Text -> Text -> Text
    forall a. Semigroup a => a -> a -> a
    <>) ([Text] -> Expr Src Void -> [Text]
    algebraicComplete [Text]
    fs Expr Src Void
    e)

          in  case Expr Src Void
    expr of
                Dhall.Core.RecordLit    m :: Map Text (Expr Src Void)
    m -> Map Text (Maybe (Expr Src Void)) -> [Text]
    withMap ((Expr Src Void -> Maybe (Expr Src Void))
    -> Map Text (Expr Src Void) -> Map Text (Maybe (Expr Src Void))
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    fmap Expr Src Void -> Maybe (Expr Src Void)
    forall a. a -> Maybe a
    Just Map Text (Expr Src Void)
    m)
                Dhall.Core.Union        m :: Map Text (Maybe (Expr Src Void))
    m -> Map Text (Maybe (Expr Src Void)) -> [Text]
    withMap Map Text (Maybe (Expr Src Void))
    m
                _                         -> []

    greeter :: MonadIO m => m ()
    greeter :: m ()
    greeter =
      let version :: String
    version = String
    Meta.dhallVersionString
          message :: String
    message = "Welcome to the Dhall v" String -> String -> String
    forall a. Semigroup a => a -> a -> a
    <> String
    version String -> String -> String
    forall a. Semigroup a => a -> a -> a
    <> " REPL! Type :help for more information."
      in IO () -> m ()
    forall (m :: * -> *) a. MonadIO m => IO a -> m a
    liftIO (String -> IO ()
    putStrLn String
    message)

    dontCrash :: Repl () -> Repl ()
    dontCrash :: HaskelineT (StateT Env IO) () -> HaskelineT (StateT Env IO) ()
    dontCrash m :: HaskelineT (StateT Env IO) ()
    m =
    #if MIN_VERSION_haskeline(0,8,0)
      Control.Monad.Catch.catch
    #else
      HaskelineT (StateT Env IO) ()
    -> (SomeException -> HaskelineT (StateT Env IO) ())
    -> HaskelineT (StateT Env IO) ()
    forall (m :: * -> *) e a.
    (MonadException m, Exception e) =>
    m a -> (e -> m a) -> m a
    System.Console.Haskeline.MonadException.catch
    #endif
        HaskelineT (StateT Env IO) ()
    m
        ( \ e :: SomeException
    e@SomeException{} -> IO () -> HaskelineT (StateT Env IO) ()
    forall (m :: * -> *) a. MonadIO m => IO a -> m a
    liftIO ( String -> IO ()
    putStrLn ( SomeException -> String
    forall e. Exception e => e -> String
    displayException SomeException
    e ) ) )

    writeOutputHandle :: (MonadIO m, MonadState Env m) => Text -> m ()
    writeOutputHandle :: Text -> m ()
    writeOutputHandle txt :: Text
    txt = do
      Env { Maybe Handle
    outputHandle :: Maybe Handle
    outputHandle :: Env -> Maybe Handle
    outputHandle } <- m Env
    forall s (m :: * -> *). MonadState s m => m s
    get

      case Maybe Handle
    outputHandle of
        Just handle :: Handle
    handle -> IO () -> m ()
    forall (m :: * -> *) a. MonadIO m => IO a -> m a
    liftIO (IO () -> m ()) -> IO () -> m ()
    forall a b. (a -> b) -> a -> b
    $ Handle -> Text -> IO ()
    Text.IO.hPutStrLn Handle
    handle Text
    txt
        Nothing     -> () -> m ()
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure ()

    output
      :: (Pretty.Pretty a, MonadState Env m, MonadIO m)
      => Dhall.Expr Src a -> m ()
    output :: Expr Src a -> m ()
    output expr :: Expr Src a
    expr = do
      Text -> m ()
    forall (m :: * -> *). (MonadIO m, MonadState Env m) => Text -> m ()
    writeOutputHandle "" -- Visual spacing

      Expr Src a -> m ()
    forall a (m :: * -> *).
    (Pretty a, MonadState Env m, MonadIO m) =>
    Expr Src a -> m ()
    outputWithoutSpacing Expr Src a
    expr

      Text -> m ()
    forall (m :: * -> *). (MonadIO m, MonadState Env m) => Text -> m ()
    writeOutputHandle "" -- Visual spacing

    outputWithoutSpacing
      :: (Pretty.Pretty a, MonadState Env m, MonadIO m)
      => Dhall.Expr Src a -> m ()
    outputWithoutSpacing :: Expr Src a -> m ()
    outputWithoutSpacing expr :: Expr Src a
    expr = do
      Env { CharacterSet
    characterSet :: CharacterSet
    characterSet :: Env -> CharacterSet
    characterSet, Maybe Handle
    outputHandle :: Maybe Handle
    outputHandle :: Env -> Maybe Handle
    outputHandle } <- m Env
    forall s (m :: * -> *). MonadState s m => m s
    get

      case Maybe Handle
    outputHandle of
        Nothing     -> () -> m ()
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure ()
        Just handle :: Handle
    handle -> do
          let stream :: SimpleDocStream Ann
    stream = Doc Ann -> SimpleDocStream Ann
    forall ann. Doc ann -> SimpleDocStream ann
    Dhall.Pretty.layout (CharacterSet -> Expr Src a -> Doc Ann
    forall a. Pretty a => CharacterSet -> Expr Src a -> Doc Ann
    Dhall.Pretty.prettyCharacterSet CharacterSet
    characterSet Expr Src a
    expr)

          Bool
    supportsANSI <- IO Bool -> m Bool
    forall (m :: * -> *) a. MonadIO m => IO a -> m a
    liftIO (Handle -> IO Bool
    System.Console.ANSI.hSupportsANSI Handle
    handle)
          let ansiStream :: SimpleDocStream AnsiStyle
    ansiStream =
                  if Bool
    supportsANSI
                  then (Ann -> AnsiStyle)
    -> SimpleDocStream Ann -> SimpleDocStream AnsiStyle
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    fmap Ann -> AnsiStyle
    Dhall.Pretty.annToAnsiStyle SimpleDocStream Ann
    stream
                  else SimpleDocStream Ann -> SimpleDocStream AnsiStyle
    forall ann xxx. SimpleDocStream ann -> SimpleDocStream xxx
    Pretty.unAnnotateS SimpleDocStream Ann
    stream

          IO () -> m ()
    forall (m :: * -> *) a. MonadIO m => IO a -> m a
    liftIO (Handle -> SimpleDocStream AnsiStyle -> IO ()
    Pretty.renderIO Handle
    handle SimpleDocStream AnsiStyle
    ansiStream)
          IO () -> m ()
    forall (m :: * -> *) a. MonadIO m => IO a -> m a
    liftIO (Handle -> String -> IO ()
    System.IO.hPutStrLn Handle
    handle "") -- Pretty printing doesn't end with a new line