-- | 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 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.
(MonadMask m, MonadIO 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]
++ String
" " )
            ( 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
        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 :: 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
    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 :: 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 (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 (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 (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 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 :: [String] -> m ()
typeOf [] = String -> m ()
forall (m :: * -> *) a. MonadFail m => String -> m a
Fail.fail String
":type requires an argument to check the type of"

typeOf [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 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 (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 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 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 (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 (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 (String
str₀ : (Char
'=' : String
str₁) : [String]
strs) =
    String
str₀ String -> [String] -> [String]
forall a. a -> [a] -> [a]
: String
"=" String -> [String] -> [String]
forall a. a -> [a] -> [a]
: String
str₁ String -> [String] -> [String]
forall a. a -> [a] -> [a]
: [String]
strs
separateEqual (String
str : [String]
strs)
    | (String
str₀, Char
'=' : 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
== Char
'=') String
str =
        String
str₀ String -> [String] -> [String]
forall a. a -> [a] -> [a]
: String
"=" 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 (String
k : String
"=" : [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) String
"(input)" (String -> Text
Text.pack String
k) of
      Left   ParseErrorBundle Text Void
_      -> String -> m Text
forall (m :: * -> *) a. MonadFail m => String -> m a
Fail.fail String
"Invalid variable name"
      Right 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
    ( \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 Int
0 ) ) Expr Src Void
t )

addBinding [String]
_ = String -> m ()
forall (m :: * -> *) a. MonadFail m => String -> m a
Fail.fail String
":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 {Bool
Maybe Handle
Maybe Binding
Context Binding
CharacterSet
outputHandle :: Maybe Handle
characterSet :: CharacterSet
explain :: Bool
envIt :: Maybe Binding
envBindings :: Context Binding
outputHandle :: Env -> Maybe Handle
envIt :: Env -> Maybe Binding
envBindings :: Env -> Context Binding
explain :: Env -> Bool
characterSet :: Env -> CharacterSet
..}) = Env :: Context Binding
-> Maybe Binding -> Bool -> CharacterSet -> Maybe Handle -> Env
Env { envBindings :: Context Binding
envBindings = Context Binding
forall a. Context a
Dhall.Context.empty, Bool
Maybe Handle
Maybe Binding
CharacterSet
outputHandle :: Maybe Handle
characterSet :: CharacterSet
explain :: Bool
envIt :: Maybe Binding
outputHandle :: Maybe Handle
envIt :: Maybe Binding
explain :: Bool
characterSet :: CharacterSet
..}

clearBindings [String]
_ = String -> m ()
forall (m :: * -> *) a. MonadFail m => String -> m a
Fail.fail String
":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 String
":hash should be of the form `:hash expr"
hashBinding [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 = String
".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 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 (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 (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 (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) (\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 :: 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 (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 :: [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 String
file -> [String] -> HaskelineT (StateT Env IO) ()
loadBinding [String
file]
    Maybe String
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
$ 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
  [[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 ((Char
c:String
cmd):[String]
opts)
        | Char
c Char -> Char -> Bool
forall a. Eq a => a -> a -> Bool
== Char
optionsPrefix
        , Just [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 [String]
_ = 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
$
        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 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 (\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 (\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"

loadBinding [String]
_ = Command (HaskelineT (StateT Env IO))
forall (m :: * -> *) a. MonadFail m => String -> m a
Fail.fail String
":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 [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 =
          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 (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 (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 (String
file : String
"=" : [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 =
          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
$ 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"

saveBinding [String]
_ = String -> m ()
forall (m :: * -> *) a. MonadFail m => String -> m a
Fail.fail String
":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 [ String
"--explain" ] = do
  (Env -> Env) -> m ()
forall s (m :: * -> *). MonadState s m => (s -> s) -> m ()
modify (\Env
e -> Env
e { explain :: Bool
explain = Bool
True })
setOption [String]
_ = do
  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 :: [String] -> m ()
unsetOption [ String
"--explain" ] = do
  (Env -> Env) -> m ()
forall s (m :: * -> *). MonadState s m => (s -> s) -> m ()
modify (\Env
e -> Env
e { explain :: Bool
explain = Bool
False })
unsetOption [String]
_ = do
  Text -> m ()
forall (m :: * -> *). (MonadIO m, MonadState Env m) => Text -> m ()
writeOutputHandle Text
":unset should be of the form `:unset <command line option>`"

cmdQuit :: ( MonadIO m, MonadState Env m ) => [String] -> m ()
cmdQuit :: [String] -> m ()
cmdQuit [String]
_ = do
  IO () -> m ()
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (String -> IO ()
putStrLn String
"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 HelpOptions m
hs [String]
_ = do
  IO () -> m ()
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 (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 (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
':'

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
      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) ())
-> ([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
      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) ())
-> ([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
      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) ())
-> ([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
      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) ())
-> ([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
      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) ())
-> ([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
      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) ())
-> ([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
      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) ())
-> ([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
      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) ())
-> ([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
      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) ())
-> ([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
      String
"quit"
      String
""
      String
"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 = (\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 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 :: 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 (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 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 (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
  | 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 (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 Int
0 Context Binding
envBindings of

      Maybe Binding
Nothing -> [Completion] -> m [Completion]
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 (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 [Text]
subFields 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 -> 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 (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 (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        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 :: 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 (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 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 (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 (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 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 -> 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
    Maybe Handle
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 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 :: Expr Src a -> m ()
outputWithoutSpacing 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
    Maybe Handle
Nothing     -> () -> m ()
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 (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 String
"") -- Pretty printing doesn't end with a new line