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

    {-# LANGUAGE CPP               #-}
    {-# LANGUAGE FlexibleContexts  #-}
    {-# LANGUAGE LambdaCase        #-}
    {-# LANGUAGE NamedFieldPuns    #-}
    {-# LANGUAGE OverloadedStrings #-}
    {-# LANGUAGE RecordWildCards   #-}
    {-# LANGUAGE ViewPatterns      #-}

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

    import Control.Exception
        ( SomeException (SomeException)
        , displayException
        , throwIO
        )
    import Control.Monad     (forM_)
    #if !(MIN_VERSION_base(4,13,0))
    import Control.Monad.Fail (MonadFail)
    #endif
    import Control.Monad.IO.Class              (MonadIO, liftIO)
    import Control.Monad.State.Class           (MonadState, get, modify)
    import Control.Monad.State.Strict          (evalStateT)
    import Data.Char                           (isSpace)
    import Data.List
        ( dropWhileEnd
        , groupBy
        , isPrefixOf
        , nub
        )
    import Data.Maybe                          (mapMaybe)
    import Data.Text                           (Text)
    import Data.Void                           (Void)
    import Dhall.Context                       (Context)
    import Dhall.Import                        (hashExpressionToCode)
    import Dhall.Parser                        (Parser (..))
    import Dhall.Pretty                        (CharacterSet (..))
    import Dhall.Src                           (Src)
    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 Dhall
    import qualified Dhall.Context
    import qualified Dhall.Core
    import qualified Dhall.Core                          as Dhall
        ( Expr
        , Var (V)
        , normalize
        )
    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.Parser.Expression             as Parser.Expression
    import qualified Dhall.Pretty
    import qualified Dhall.Pretty.Internal
    import qualified Dhall.Syntax                        as Syntax
    import qualified Dhall.TypeCheck                     as Dhall
    import qualified Dhall.Version                       as Meta
    import qualified Prettyprinter                       as Pretty
    import qualified Prettyprinter.Render.Terminal       as Pretty (renderIO)
    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 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
            ( (MultiLine -> HaskelineT (StateT Env IO) String)
    -> Command (HaskelineT (StateT Env IO))
    -> Options (HaskelineT (StateT Env IO))
    -> Maybe Char
    -> Maybe String
    -> CompleterStyle (StateT Env IO)
    -> HaskelineT (StateT Env IO) ()
    -> HaskelineT (StateT Env IO) ExitDecision
    -> StateT Env IO ()
    forall (m :: * -> *) a.
    (MonadMask m, MonadIO m) =>
    (MultiLine -> HaskelineT m String)
    -> Command (HaskelineT m)
    -> Options (HaskelineT m)
    -> Maybe Char
    -> Maybe String
    -> CompleterStyle m
    -> HaskelineT m a
    -> HaskelineT m ExitDecision
    -> m ()
    Repline.evalRepl
                MultiLine -> HaskelineT (StateT Env IO) String
    banner
                ( 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 )
                ( String -> Maybe String
    forall a. a -> Maybe a
    Just String
    "paste" )
                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
                HaskelineT (StateT Env IO) ExitDecision
    forall (m :: * -> *). MonadIO m => m ExitDecision
    finaliser
            )
            (Env
    emptyEnv { CharacterSet
    characterSet :: CharacterSet
    characterSet :: CharacterSet
    characterSet, Bool
    explain :: Bool
    explain :: Bool
    explain })

        banner :: MultiLine -> HaskelineT (StateT Env IO) String
    banner = String -> HaskelineT (StateT Env IO) String
    forall a. a -> HaskelineT (StateT Env IO) a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure (String -> HaskelineT (StateT Env IO) String)
    -> (MultiLine -> String)
    -> MultiLine
    -> HaskelineT (StateT Env IO) String
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . \case
          MultiLine
    Repline.SingleLine -> String
    turnstile String -> String -> String
    forall a. Semigroup a => a -> a -> a
    <> String
    " "
          MultiLine
    Repline.MultiLine  -> String
    "| "

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

    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
        { 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 :: Env -> Context Binding
    envBindings :: Context Binding
    envBindings, Maybe Binding
    envIt :: Env -> Maybe Binding
    envIt :: Maybe Binding
    envIt } =
      case Maybe Binding
    envIt of
        Maybe Binding
    Nothing ->
          Context Binding
    envBindings

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

    parseAndLoad
      :: MonadIO m => String -> m ( Dhall.Expr Dhall.Src Void)
    parseAndLoad :: forall (m :: * -> *). MonadIO m => String -> m (Expr Src Void)
    parseAndLoad String
    src = do
      Expr Src Import
    parsed <-
        case String -> Text -> Either ParseError (Expr Src Import)
    Dhall.exprFromText String
    "(input)" (String -> Text
    Text.pack String
    src Text -> Text -> Text
    forall a. Semigroup a => a -> a -> a
    <> Text
    "\n") of
          Left ParseError
    e ->
            IO (Expr Src Import) -> m (Expr Src Import)
    forall a. IO a -> m a
    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 Expr Src Import
    a ->
            Expr Src Import -> m (Expr Src Import)
    forall a. a -> m a
    forall (m :: * -> *) a. Monad m => a -> m a
    return Expr Src Import
    a

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

      IO (Expr Src Void) -> m (Expr Src Void)
    forall a. IO a -> m a
    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 :: forall (m :: * -> *).
    (MonadIO m, MonadState Env m) =>
    String -> m ()
    eval 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 ( \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 :: forall (m :: * -> *).
    (MonadFail m, MonadIO m, MonadState Env m) =>
    String -> m ()
    typeOf 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 -> 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 Binding
    context 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 (Text
    variable, Binding Expr Src Void
    expr Expr Src Void
    _) =
            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 a b. (a -> b) -> [a] -> [b]
    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 :: forall (m :: * -> *) t.
    MonadState Env m =>
    Expr Src Void -> m (Expr t Void)
    normalize 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 a. a -> m a
    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 :: forall (m :: * -> *).
    (MonadIO m, MonadState Env m) =>
    Expr Src Void -> m (Expr Src Void)
    typeCheck 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  TypeError Src Void
    e -> IO (Expr Src Void) -> m (Expr Src Void)
    forall a. IO a -> m a
    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 Expr Src Void
    a -> Expr Src Void -> m (Expr Src Void)
    forall a. a -> m a
    forall (m :: * -> *) a. Monad m => a -> m a
    return Expr Src Void
    a

    -- Split on the first '=' if there is any
    parseAssignment :: String -> Either String (String, String)
    parseAssignment :: String -> Either String (String, String)
    parseAssignment String
    str
      | (String
    var, Char
    '=' : String
    expr) <- (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
      = (String, String) -> Either String (String, String)
    forall a b. b -> Either a b
    Right (String -> String
    trim String
    var, String
    expr)
      | Bool
    otherwise
      = String -> Either String (String, String)
    forall a b. a -> Either a b
    Left (String -> String
    trim String
    str)

    addBinding :: ( MonadFail m, MonadIO m, MonadState Env m ) => String -> m ()
    addBinding :: forall (m :: * -> *).
    (MonadFail m, MonadIO m, MonadState Env m) =>
    String -> m ()
    addBinding String
    string = do
      let parseBinding :: Parser (Binding Src Import)
    parseBinding =
              Parsers Import -> Parser (Binding Src Import)
    forall a. Parsers a -> Parser (Binding Src a)
    Parser.Expression.letBinding
                  (Parser Import -> Parsers Import
    forall a. Parser a -> Parsers a
    Parser.Expression.parsers
                      (Parser Import -> Parser Import
    forall a. Parser a -> Parser a
    forall e s (m :: * -> *) a. MonadParsec e s m => m a -> m a
    Megaparsec.try Parser Import
    Parser.Expression.import_)
                  )

      let input :: Text
    input = Text
    "let " Text -> Text -> Text
    forall a. Semigroup a => a -> a -> a
    <> String -> Text
    Text.pack String
    string

      Syntax.Binding{ Text
    variable :: Text
    variable :: forall s a. Binding s a -> Text
    variable, Maybe (Maybe Src, Expr Src Import)
    annotation :: Maybe (Maybe Src, Expr Src Import)
    annotation :: forall s a. Binding s a -> Maybe (Maybe s, Expr s a)
    annotation, Expr Src Import
    value :: Expr Src Import
    value :: forall s a. Binding s a -> Expr s a
    value } <- case Parsec Void Text (Binding Src Import)
    -> String
    -> Text
    -> Either (ParseErrorBundle Text Void) (Binding Src Import)
    forall e s a.
    Parsec e s a -> String -> s -> Either (ParseErrorBundle s e) a
    Megaparsec.parse (Parser (Binding Src Import)
    -> Parsec Void Text (Binding Src Import)
    forall a. Parser a -> Parsec Void Text a
    unParser Parser (Binding Src Import)
    parseBinding) String
    "(input)" Text
    input of
          Left  ParseErrorBundle Text Void
    _       -> String -> m (Binding Src Import)
    forall a. String -> m a
    forall (m :: * -> *) a. MonadFail m => String -> m a
    Fail.fail String
    ":let should be of the form `:let x [: T] = y`"
          Right Binding Src Import
    binding -> Binding Src Import -> m (Binding Src Import)
    forall a. a -> m a
    forall (m :: * -> *) a. Monad m => a -> m a
    return Binding Src Import
    binding

      (Expr Src Void
    resolved, Expr Src Void
    bindingType) <- case Maybe (Maybe Src, Expr Src Import)
    annotation of
          Just (Maybe Src
    _, Expr Src Import
    unresolvedType) -> do
              let annotated :: Expr Src Import
    annotated = Expr Src Import -> Expr Src Import -> Expr Src Import
    forall s a. Expr s a -> Expr s a -> Expr s a
    Syntax.Annot Expr Src Import
    value Expr Src Import
    unresolvedType

              Expr Src Void
    resolved <- IO (Expr Src Void) -> m (Expr Src Void)
    forall a. IO a -> m a
    forall (m :: * -> *) a. MonadIO m => IO a -> m a
    liftIO (Expr Src Import -> IO (Expr Src Void)
    Dhall.load Expr Src Import
    annotated)

              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
    resolved

              Expr Src Void
    bindingType <- IO (Expr Src Void) -> m (Expr Src Void)
    forall a. IO a -> m a
    forall (m :: * -> *) a. MonadIO m => IO a -> m a
    liftIO (Expr Src Import -> IO (Expr Src Void)
    Dhall.load Expr Src Import
    unresolvedType)

              (Expr Src Void, Expr Src Void) -> m (Expr Src Void, Expr Src Void)
    forall a. a -> m a
    forall (m :: * -> *) a. Monad m => a -> m a
    return (Expr Src Void
    resolved, Expr Src Void
    bindingType)
          Maybe (Maybe Src, Expr Src Import)
    _ -> do
              Expr Src Void
    resolved <- IO (Expr Src Void) -> m (Expr Src Void)
    forall a. IO a -> m a
    forall (m :: * -> *) a. MonadIO m => IO a -> m a
    liftIO (Expr Src Import -> IO (Expr Src Void)
    Dhall.load Expr Src Import
    value)

              Expr Src Void
    bindingType <- 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
    resolved

              (Expr Src Void, Expr Src Void) -> m (Expr Src Void, Expr Src Void)
    forall a. a -> m a
    forall (m :: * -> *) a. Monad m => a -> m a
    return (Expr Src Void
    resolved, Expr Src Void
    bindingType)

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

      (Env -> Env) -> m ()
    forall s (m :: * -> *). MonadState s m => (s -> s) -> m ()
    modify
        ( \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
    variable
                    Binding{ Expr Src Void
    bindingType :: Expr Src Void
    bindingType :: Expr Src Void
    bindingType, Expr Src Void
    bindingExpr :: Expr Src Void
    bindingExpr :: Expr Src Void
    bindingExpr }
                    ( 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
    variable Int
    0)) Expr Src Void
    bindingType)

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

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

      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
        (Expr Void Void -> Text
    hashExpressionToCode (Expr Void Void -> Expr Void Void
    forall s a. Expr s a -> Expr s a
    Dhall.Core.alphaNormalize Expr Void Void
    normalizedExpression))

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

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

      let parseIndex :: String -> Maybe a
    parseIndex String
    file
            | String
    saveFilePrefix String -> String -> Bool
    forall a. Eq a => [a] -> [a] -> Bool
    `isPrefixOf` String
    file
            , Char
    '-':String
    index <- Int -> String -> String
    forall a. Int -> [a] -> [a]
    drop (String -> Int
    forall a. [a] -> Int
    forall (t :: * -> *) a. Foldable t => t a -> Int
    length String
    saveFilePrefix) String
    file
            , [(a
    x, String
    "")] <- 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 a. a -> m a
    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
        [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 a. Ord a => [a] -> a
    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 :: forall (m :: * -> *). MonadIO m => m (Maybe String)
    currentSaveFile =
      ((Maybe Int -> Maybe String) -> m (Maybe Int) -> m (Maybe String)
    forall a b. (a -> b) -> m a -> m b
    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 a b. (a -> b) -> Maybe a -> Maybe b
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    fmap) (\Int
    i -> String
    saveFilePrefix String -> String -> String
    forall a. Semigroup a => a -> a -> a
    <> String
    "-" 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 :: forall (m :: * -> *). MonadIO m => 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 Int
    0 Int -> Int
    forall a. Enum a => a -> a
    succ Maybe Int
    mIndex

      String -> m String
    forall a. a -> m a
    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 -> String
    forall a. Semigroup a => a -> a -> a
    <> Int -> String
    forall a. Show a => a -> String
    show Int
    nextIndex

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

      case Maybe String
    mFile of
        Just String
    file -> Command (HaskelineT (StateT Env IO))
    loadBinding String
    file
        Maybe String
    Nothing   ->
          Command (HaskelineT (StateT Env IO))
    forall a. String -> HaskelineT (StateT Env IO) a
    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
    $ String
    ":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
    <> String
    "-*` files"

    loadBinding String
    file = do
      -- Read commands from the save file
      -- Some commands can span multiple lines, only the first line will start with
      -- the optionsPrefix
      [String]
    loadedLines <- 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 a. IO a -> HaskelineT (StateT Env IO) a
    forall (m :: * -> *) a. MonadIO m => IO a -> m a
    liftIO (String -> IO String
    readFile String
    file)

      let -- Group lines that belong to the same command
          commands :: [[String]]
    commands = ((String -> String -> Bool) -> [String] -> [[String]])
    -> [String] -> (String -> String -> Bool) -> [[String]]
    forall a b c. (a -> b -> c) -> b -> a -> c
    flip (String -> String -> Bool) -> [String] -> [[String]]
    forall a. (a -> a -> Bool) -> [a] -> [[a]]
    groupBy [String]
    loadedLines ((String -> String -> Bool) -> [[String]])
    -> (String -> String -> Bool) -> [[String]]
    forall a b. (a -> b) -> a -> b
    $ \String
    _prev String
    next ->
            Bool -> Bool
    not (Bool -> Bool) -> Bool -> Bool
    forall a b. (a -> b) -> a -> b
    $ [Char
    optionsPrefix] String -> String -> Bool
    forall a. Eq a => [a] -> [a] -> Bool
    `isPrefixOf` String
    next

          runCommand :: Command (HaskelineT (StateT Env IO))
    runCommand line :: String
    line@(String -> [String]
    words -> (Char
    c:String
    cmd):[String]
    _)
            | Char
    c Char -> Char -> Bool
    forall a. Eq a => a -> a -> Bool
    == Char
    optionsPrefix
            = case String
    -> Options (HaskelineT (StateT Env IO))
    -> Maybe (Command (HaskelineT (StateT Env IO)))
    forall a b. Eq a => a -> [(a, b)] -> Maybe b
    lookup String
    cmd Options (HaskelineT (StateT Env IO))
    options of
                Just Command (HaskelineT (StateT Env IO))
    action -> Command (HaskelineT (StateT Env IO))
    action (Int -> String -> String
    forall a. Int -> [a] -> [a]
    drop (Int
    1 Int -> 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
    cmd Int -> Int -> Int
    forall a. Num a => a -> a -> a
    + Int
    1) String
    line)
                Maybe (Command (HaskelineT (StateT Env IO)))
    Nothing -> Command (HaskelineT (StateT Env IO))
    forall a. String -> HaskelineT (StateT Env IO) a
    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
    $
                  String
    ":load unexpected command `" String -> String -> String
    forall a. Semigroup a => a -> a -> a
    <> String
    cmd String -> String -> String
    forall a. Semigroup a => a -> a -> a
    <> String
    "` in file `" String -> String -> String
    forall a. Semigroup a => a -> a -> a
    <> String
    file String -> String -> String
    forall a. Semigroup a => a -> a -> a
    <> String
    "`"
          runCommand String
    _ = Command (HaskelineT (StateT Env IO))
    forall a. String -> HaskelineT (StateT Env IO) a
    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
    $
            String
    ":load expects `" String -> String -> String
    forall a. Semigroup a => a -> a -> a
    <> String
    file String -> String -> String
    forall a. Semigroup a => a -> a -> a
    <> String
    "` to contain a command"

      -- Keep current handle in scope
      Env { Maybe Handle
    outputHandle :: Env -> Maybe Handle
    outputHandle :: 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 (\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]]
    commands (Command (HaskelineT (StateT Env IO))
    runCommand Command (HaskelineT (StateT Env IO))
    -> ([String] -> String)
    -> [String]
    -> HaskelineT (StateT Env IO) ()
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . [String] -> String
    unlines)

      -- Restore the previous handle
      (Env -> Env) -> HaskelineT (StateT Env IO) ()
    forall s (m :: * -> *). MonadState s m => (s -> s) -> m ()
    modify (\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
    $ Text
    "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
    <> Text
    "`\n"

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

      Either String (String, String) -> m ()
    forall (m :: * -> *).
    (MonadFail m, MonadIO m, MonadState Env m) =>
    Either String (String, String) -> m ()
    saveBinding (String -> Either String (String, String)
    forall a b. a -> Either a b
    Left String
    file)

    -- Save all the bindings into `file`
    saveBinding (Left 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 a b. (a -> b) -> [a] -> [b]
    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 a b. (a -> b) -> (Text, a) -> (Text, b)
    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 =
              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
    $ \(Text
    name, 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 a. IO a -> StateT Env m a
    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
    $ String
    ":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
    <> String
    " = ")
                  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 a. IO a -> m a
    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
    $ Text
    "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
    <> Text
    "`\n"

    -- Save a single expression to `file`
    saveBinding (Right (String
    file, String
    src)) = do
      Expr Src Void
    loadedExpression <- String -> m (Expr Src Void)
    forall (m :: * -> *). MonadIO m => String -> m (Expr Src Void)
    parseAndLoad String
    src

      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 =
              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 a. IO a -> m a
    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
    $ Text
    "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
    <> Text
    "`\n"

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

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

    quitMessage :: String
    quitMessage :: String
    quitMessage = String
    "Goodbye."

    cmdQuit :: ( MonadIO m, MonadState Env m ) => String -> m ()
    cmdQuit :: forall (m :: * -> *).
    (MonadIO m, MonadState Env m) =>
    String -> m ()
    cmdQuit String
    _ = do
      IO () -> m ()
    forall a. IO a -> m a
    forall (m :: * -> *) a. MonadIO m => IO a -> m a
    liftIO (String -> IO ()
    putStrLn String
    quitMessage)
      IO () -> m ()
    forall a. IO a -> m a
    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 :: forall (m :: * -> *).
    (MonadFail m, MonadIO m, MonadState Env m) =>
    HelpOptions m -> String -> m ()
    help HelpOptions m
    hs String
    _ = do
      IO () -> m ()
    forall a. IO a -> m a
    forall (m :: * -> *) a. MonadIO m => IO a -> m a
    liftIO (String -> IO ()
    putStrLn String
    "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
    $ \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 a. IO a -> m a
    forall (m :: * -> *) a. MonadIO m => IO a -> m a
    liftIO (String -> IO ()
    putStrLn (String
    ":" 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 -> String
    forall a. Semigroup a => a -> a -> a
    <> String
    syntax))
        IO () -> m ()
    forall a. IO a -> m a
    forall (m :: * -> *) a. MonadIO m => IO a -> m a
    liftIO (String -> IO ()
    putStrLn (String
    "    " String -> String -> String
    forall a. Semigroup a => a -> a -> a
    <> String
    doc))

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

    trim :: String -> String
    trim :: String -> String
    trim = (Char -> Bool) -> String -> String
    forall a. (a -> Bool) -> [a] -> [a]
    dropWhile Char -> Bool
    isSpace (String -> String) -> (String -> String) -> String -> String
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . (Char -> Bool) -> String -> String
    forall a. (a -> Bool) -> [a] -> [a]
    dropWhileEnd Char -> Bool
    isSpace

    data HelpOption m = HelpOption
      { forall (m :: * -> *). HelpOption m -> String
    helpOptionName :: String
      , forall (m :: * -> *). HelpOption m -> String
    helpOptionSyntax :: String
      , forall (m :: * -> *). HelpOption m -> String
    helpOptionDoc :: String
      , forall (m :: * -> *). 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
    -> Command (HaskelineT (StateT Env IO))
    -> HelpOption (HaskelineT (StateT Env IO))
    forall (m :: * -> *).
    String -> String -> String -> Cmd m -> HelpOption m
    HelpOption
          String
    "help"
          String
    ""
          String
    "Print help text and describe options"
          (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
    . HelpOptions (HaskelineT (StateT Env IO))
    -> Command (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
    -> Command (HaskelineT (StateT Env IO))
    -> HelpOption (HaskelineT (StateT Env IO))
    forall (m :: * -> *).
    String -> String -> String -> Cmd m -> HelpOption m
    HelpOption
          String
    "paste"
          String
    ""
          String
    "Start a multi-line input. Submit with <Ctrl-D>"
          (String -> Command (HaskelineT (StateT Env IO))
    forall a. HasCallStack => String -> a
    error String
    "Dhall.Repl.helpOptions: Unreachable")
      , String
    -> String
    -> String
    -> Command (HaskelineT (StateT Env IO))
    -> HelpOption (HaskelineT (StateT Env IO))
    forall (m :: * -> *).
    String -> String -> String -> Cmd m -> HelpOption m
    HelpOption
          String
    "type"
          String
    "EXPRESSION"
          String
    "Infer the type of an expression"
          (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 :: * -> *).
    (MonadFail m, MonadIO m, MonadState Env m) =>
    String -> m ()
    typeOf)
      , String
    -> String
    -> String
    -> Command (HaskelineT (StateT Env IO))
    -> HelpOption (HaskelineT (StateT Env IO))
    forall (m :: * -> *).
    String -> String -> String -> Cmd m -> HelpOption m
    HelpOption
          String
    "hash"
          String
    "EXPRESSION"
          String
    "Hash the normalized value of an expression"
          (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 :: * -> *).
    (MonadFail m, MonadIO m, MonadState Env m) =>
    String -> m ()
    hashBinding)
      , String
    -> String
    -> String
    -> Command (HaskelineT (StateT Env IO))
    -> HelpOption (HaskelineT (StateT Env IO))
    forall (m :: * -> *).
    String -> String -> String -> Cmd m -> HelpOption m
    HelpOption
          String
    "let"
          String
    "IDENTIFIER = EXPRESSION"
          String
    "Assign an expression to a variable"
          (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 :: * -> *).
    (MonadFail m, MonadIO m, MonadState Env m) =>
    String -> m ()
    addBinding)
      , String
    -> String
    -> String
    -> Command (HaskelineT (StateT Env IO))
    -> HelpOption (HaskelineT (StateT Env IO))
    forall (m :: * -> *).
    String -> String -> String -> Cmd m -> HelpOption m
    HelpOption
          String
    "clear"
          String
    ""
          String
    "Clear all bound variables"
          (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 :: * -> *).
    (MonadFail m, MonadState Env m) =>
    String -> m ()
    clearBindings)
      , String
    -> String
    -> String
    -> Command (HaskelineT (StateT Env IO))
    -> HelpOption (HaskelineT (StateT Env IO))
    forall (m :: * -> *).
    String -> String -> String -> Cmd m -> HelpOption m
    HelpOption
          String
    "load"
          String
    "[FILENAME]"
          String
    "Load bound variables from a file"
          (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))
    loadBinding Command (HaskelineT (StateT Env IO))
    -> (String -> String) -> Command (HaskelineT (StateT Env IO))
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . String -> String
    trim)
      , String
    -> String
    -> String
    -> Command (HaskelineT (StateT Env IO))
    -> HelpOption (HaskelineT (StateT Env IO))
    forall (m :: * -> *).
    String -> String -> String -> Cmd m -> HelpOption m
    HelpOption
          String
    "save"
          String
    "[FILENAME | FILENAME = EXPRESSION]"
          String
    "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) ())
    -> Command (HaskelineT (StateT Env IO))
    -> Command (HaskelineT (StateT Env IO))
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Either String (String, String) -> HaskelineT (StateT Env IO) ()
    forall (m :: * -> *).
    (MonadFail m, MonadIO m, MonadState Env m) =>
    Either String (String, String) -> m ()
    saveBinding (Either String (String, String) -> HaskelineT (StateT Env IO) ())
    -> (String -> Either String (String, String))
    -> Command (HaskelineT (StateT Env IO))
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . String -> Either String (String, String)
    parseAssignment)
      , String
    -> String
    -> String
    -> Command (HaskelineT (StateT Env IO))
    -> HelpOption (HaskelineT (StateT Env IO))
    forall (m :: * -> *).
    String -> String -> String -> Cmd m -> HelpOption m
    HelpOption
          String
    "set"
          String
    "OPTION"
          String
    "Set an option. Currently supported: --explain"
          (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 ()
    setOption Command (HaskelineT (StateT Env IO))
    -> (String -> String) -> Command (HaskelineT (StateT Env IO))
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . String -> String
    trim)
      , String
    -> String
    -> String
    -> Command (HaskelineT (StateT Env IO))
    -> HelpOption (HaskelineT (StateT Env IO))
    forall (m :: * -> *).
    String -> String -> String -> Cmd m -> HelpOption m
    HelpOption
          String
    "unset"
          String
    "OPTION"
          String
    "Unset an option"
          (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 ()
    unsetOption Command (HaskelineT (StateT Env IO))
    -> (String -> String) -> Command (HaskelineT (StateT Env IO))
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . String -> String
    trim)
      , String
    -> String
    -> String
    -> Command (HaskelineT (StateT Env IO))
    -> HelpOption (HaskelineT (StateT Env IO))
    forall (m :: * -> *).
    String -> String -> String -> Cmd m -> HelpOption m
    HelpOption
          String
    "quit"
          String
    ""
          String
    "Exit the REPL"
          Command (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 = (\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))
    -> Command (HaskelineT (StateT Env IO))
    forall (m :: * -> *). HelpOption m -> Cmd m
    helpOptionFunction HelpOption (HaskelineT (StateT Env IO))
    h)) (HelpOption (HaskelineT (StateT Env IO))
     -> (String, Command (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 :: forall (m :: * -> *).
    (Monad m, MonadFail m, MonadIO m, MonadState Env m) =>
    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 Char
    '\\') 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 = String
    " \t[(,=+*&|}#?>:"

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

      -- Complete commands
      | String
    reversedPrev String -> String -> Bool
    forall a. Eq a => a -> a -> Bool
    == String
    ":"
      = [Completion] -> m [Completion]
    forall a. a -> m a
    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, Command (HaskelineT (StateT Env IO))) -> String
    forall a b. (a, b) -> a
    fst ((String, Command (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 String
    ":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
    "/", String
    "./", String
    "../", String
    "~/" ]
      = String -> m [Completion]
    forall (m :: * -> *). MonadIO m => String -> m [Completion]
    Haskeline.listFiles String
    word

      -- Complete environment variables
      | String -> String
    forall a. [a] -> [a]
    reverse String
    "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 a b. (a -> b) -> [a] -> [b]
    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 a. IO a -> m a
    forall (m :: * -> *) a. MonadIO m => IO a -> m a
    liftIO IO [(String, String)]
    getEnvironment

      -- Complete record fields and union alternatives
      | Text
    var : [Text]
    subFields <- (Char -> Bool) -> Text -> [Text]
    Text.split (Char -> Char -> Bool
    forall a. Eq a => a -> a -> Bool
    == Char
    '.') (String -> Text
    Text.pack String
    word)
      , Bool -> Bool
    not (Bool -> Bool) -> Bool -> Bool
    forall a b. (a -> b) -> a -> b
    $ [Text] -> Bool
    forall a. [a] -> Bool
    forall (t :: * -> *) a. Foldable t => t a -> Bool
    null [Text]
    subFields
      = do
        Env { Context Binding
    envBindings :: Env -> Context Binding
    envBindings :: 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 Int
    0 Context Binding
    envBindings of

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

          Just 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 a. a -> m a
    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 :: Env -> Context Binding
    envBindings :: 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 a. a -> m a
    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 [Text]
    subFields Expr Src Void
    expr =
          let keys :: Map Text v -> [Text]
    keys = (Text -> Text) -> [Text] -> [Text]
    forall a b. (a -> b) -> [a] -> [b]
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    fmap (Text
    "." 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 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)
                      [Text
    _] -> Map Text (Maybe (Expr Src Void)) -> [Text]
    forall {v}. Map Text v -> [Text]
    keys Map Text (Maybe (Expr Src Void))
    m
                      Text
    f:[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
                              Maybe (Maybe (Expr Src Void))
    Nothing ->
                                  []
                              Just Maybe (Expr Src Void)
    Nothing ->
                                  Map Text (Maybe (Expr Src Void)) -> [Text]
    forall {v}. Map Text v -> [Text]
    keys Map Text (Maybe (Expr Src Void))
    m
                              Just (Just Expr Src Void
    e) ->
                                  (Text -> Text) -> [Text] -> [Text]
    forall a b. (a -> b) -> [a] -> [b]
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    fmap ((Text
    "." 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    Map Text (RecordField Src Void)
    m -> Map Text (Maybe (Expr Src Void)) -> [Text]
    withMap ((RecordField Src Void -> Maybe (Expr Src Void))
    -> Map Text (RecordField Src Void)
    -> Map Text (Maybe (Expr Src Void))
    forall a b. (a -> b) -> Map Text a -> Map Text b
    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 (Expr Src Void -> Maybe (Expr Src Void))
    -> (RecordField Src Void -> Expr Src Void)
    -> RecordField Src Void
    -> Maybe (Expr Src Void)
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . RecordField Src Void -> Expr Src Void
    forall s a. RecordField s a -> Expr s a
    Dhall.Core.recordFieldValue) Map Text (RecordField Src Void)
    m)
                Dhall.Core.Union        Map Text (Maybe (Expr Src Void))
    m -> Map Text (Maybe (Expr Src Void)) -> [Text]
    withMap Map Text (Maybe (Expr Src Void))
    m
                Expr Src Void
    _                         -> []

    greeter :: MonadIO m => m ()
    greeter :: forall (m :: * -> *). MonadIO m => m ()
    greeter =
      let version :: String
    version = String
    Meta.dhallVersionString
          message :: String
    message = String
    "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
    <> String
    " REPL! Type :help for more information."
      in IO () -> m ()
    forall a. IO a -> m a
    forall (m :: * -> *) a. MonadIO m => IO a -> m a
    liftIO (String -> IO ()
    putStrLn String
    message)

    finaliser :: MonadIO m => m Repline.ExitDecision
    finaliser :: forall (m :: * -> *). MonadIO m => m ExitDecision
    finaliser = do
      IO () -> m ()
    forall a. IO a -> m a
    forall (m :: * -> *) a. MonadIO m => IO a -> m a
    liftIO (String -> IO ()
    putStrLn String
    quitMessage)
      ExitDecision -> m ExitDecision
    forall a. a -> m a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure ExitDecision
    Repline.Exit

    dontCrash :: Repl () -> Repl ()
    dontCrash :: HaskelineT (StateT Env IO) () -> HaskelineT (StateT Env IO) ()
    dontCrash HaskelineT (StateT Env IO) ()
    m =
    #if MIN_VERSION_haskeline(0,8,0)
      HaskelineT (StateT Env IO) ()
    -> (SomeException -> HaskelineT (StateT Env IO) ())
    -> HaskelineT (StateT Env IO) ()
    forall e a.
    Exception e =>
    HaskelineT (StateT Env IO) a
    -> (e -> HaskelineT (StateT Env IO) a)
    -> HaskelineT (StateT Env IO) a
    forall (m :: * -> *) e a.
    (MonadCatch m, Exception e) =>
    m a -> (e -> m a) -> m a
    Control.Monad.Catch.catch
    #else
      System.Console.Haskeline.MonadException.catch
    #endif
        HaskelineT (StateT Env IO) ()
    m
        ( \ e :: SomeException
    e@SomeException{} -> IO () -> HaskelineT (StateT Env IO) ()
    forall a. IO a -> HaskelineT (StateT Env IO) a
    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 :: forall (m :: * -> *). (MonadIO m, MonadState Env m) => Text -> m ()
    writeOutputHandle Text
    txt = do
      Env { Maybe Handle
    outputHandle :: Env -> Maybe Handle
    outputHandle :: Maybe Handle
    outputHandle } <- m Env
    forall s (m :: * -> *). MonadState s m => m s
    get

      case Maybe Handle
    outputHandle of
        Just Handle
    handle -> 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
    $ Handle -> Text -> IO ()
    Text.IO.hPutStrLn Handle
    handle Text
    txt
        Maybe Handle
    Nothing     -> () -> m ()
    forall a. a -> m a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure ()

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

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

      case Maybe Handle
    outputHandle of
        Maybe Handle
    Nothing     -> () -> m ()
    forall a. a -> m a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure ()
        Just 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 a. IO a -> m a
    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 a b. (a -> b) -> SimpleDocStream a -> SimpleDocStream b
    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 a. IO a -> m a
    forall (m :: * -> *) a. MonadIO m => IO a -> m a
    liftIO (Handle -> SimpleDocStream AnsiStyle -> IO ()
    Pretty.renderIO Handle
    handle SimpleDocStream AnsiStyle
    ansiStream)
          IO () -> m ()
    forall a. IO a -> m a
    forall (m :: * -> *) a. MonadIO m => IO a -> m a
    liftIO (Handle -> String -> IO ()
    System.IO.hPutStrLn Handle
    handle String
    "") -- Pretty printing doesn't end with a new line