dhall-1.42.3: src/Dhall.hs

{-# LANGUAGE ApplicativeDo         #-}
{-# LANGUAGE ConstraintKinds       #-}
{-# LANGUAGE FlexibleContexts      #-}
{-# LANGUAGE FlexibleInstances     #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE OverloadedStrings     #-}
{-# LANGUAGE PolyKinds             #-}
{-# LANGUAGE RankNTypes            #-}
{-# LANGUAGE RecordWildCards       #-}
{-# LANGUAGE ScopedTypeVariables   #-}
{-# LANGUAGE TypeFamilies          #-}
{-# LANGUAGE UndecidableInstances  #-}

{-| Please read the "Dhall.Tutorial" module, which contains a tutorial explaining
    how to use the language, the compiler, and this library
-}

module Dhall
    (
    -- * Input
      input
    , inputWithSettings
    , inputFile
    , inputFileWithSettings
    , inputExpr
    , inputExprWithSettings
    , interpretExpr
    , interpretExprWithSettings
    , fromExpr
    , fromExprWithSettings
    , rootDirectory
    , sourceName
    , startingContext
    , substitutions
    , normalizer
    , newManager
    , defaultInputSettings
    , InputSettings
    , defaultEvaluateSettings
    , EvaluateSettings
    , HasEvaluateSettings(..)
    , detailed

    -- * Decoders
    , module Dhall.Marshal.Decode

    -- * Encoders
    , module Dhall.Marshal.Encode

    -- * Individual phases
    , parseWithSettings
    , resolveWithSettings
    , resolveAndStatusWithSettings
    , typecheckWithSettings
    , checkWithSettings
    , expectWithSettings
    , normalizeWithSettings

    -- * Miscellaneous
    , rawInput
    ) where

import Control.Applicative    (Alternative, empty)
import Control.Monad.Catch    (MonadThrow, throwM)
import Data.Either.Validation (Validation (..))
import Data.Void              (Void)
import Dhall.Import           (Imported (..), Status)
import Dhall.Parser           (Src (..))
import Dhall.Syntax           (Expr (..), Import)
import Dhall.TypeCheck        (DetailedTypeError (..), TypeError)
import GHC.Generics
import Lens.Micro             (Lens', lens)
import Lens.Micro.Extras      (view)
import Prelude                hiding (maybe, sequence)
import System.FilePath        (takeDirectory)

import qualified Control.Exception
import qualified Control.Monad.Trans.State.Strict as State
import qualified Data.Text.IO
import qualified Dhall.Context
import qualified Dhall.Core                       as Core
import qualified Dhall.Import
import qualified Dhall.Parser
import qualified Dhall.Pretty.Internal
import qualified Dhall.Substitution
import qualified Dhall.TypeCheck
import qualified Lens.Micro                       as Lens

import Dhall.Marshal.Decode
import Dhall.Marshal.Encode

-- | @since 1.16
data InputSettings = InputSettings
  { _rootDirectory :: FilePath
  , _sourceName :: FilePath
  , _evaluateSettings :: EvaluateSettings
  }

-- | Default input settings: resolves imports relative to @.@ (the
-- current working directory), report errors as coming from @(input)@,
-- and default evaluation settings from 'defaultEvaluateSettings'.
--
-- @since 1.16
defaultInputSettings :: InputSettings
defaultInputSettings = InputSettings
  { _rootDirectory = "."
  , _sourceName = "(input)"
  , _evaluateSettings = defaultEvaluateSettings
  }


-- | Access the directory to resolve imports relative to.
--
-- @since 1.16
rootDirectory :: Lens' InputSettings FilePath
rootDirectory = lens _rootDirectory (\s x -> s { _rootDirectory = x })

-- | Access the name of the source to report locations from; this is
-- only used in error messages, so it's okay if this is a best guess
-- or something symbolic.
--
-- @since 1.16
sourceName :: Lens' InputSettings FilePath
sourceName = lens _sourceName (\s x -> s { _sourceName = x})

-- | @since 1.16
data EvaluateSettings = EvaluateSettings
  { _substitutions   :: Dhall.Substitution.Substitutions Src Void
  , _startingContext :: Dhall.Context.Context (Expr Src Void)
  , _normalizer      :: Maybe (Core.ReifiedNormalizer Void)
  , _newManager      :: IO Dhall.Import.Manager
  }

-- | Default evaluation settings: no extra entries in the initial
-- context, and no special normalizer behaviour.
--
-- @since 1.16
defaultEvaluateSettings :: EvaluateSettings
defaultEvaluateSettings = EvaluateSettings
  { _substitutions   = Dhall.Substitution.empty
  , _startingContext = Dhall.Context.empty
  , _normalizer      = Nothing
  , _newManager      = Dhall.Import.defaultNewManager
  }

-- | Access the starting context used for evaluation and type-checking.
--
-- @since 1.16
startingContext
  :: (HasEvaluateSettings s)
  => Lens' s (Dhall.Context.Context (Expr Src Void))
startingContext =
    evaluateSettings
        . lens _startingContext (\s x -> s { _startingContext = x})

-- | Access the custom substitutions.
--
-- @since 1.30
substitutions
  :: (HasEvaluateSettings s)
  => Lens' s (Dhall.Substitution.Substitutions Src Void)
substitutions =
    evaluateSettings
        . lens _substitutions (\s x -> s { _substitutions = x })

-- | Access the custom normalizer.
--
-- @since 1.16
normalizer
  :: (HasEvaluateSettings s)
  => Lens' s (Maybe (Core.ReifiedNormalizer Void))
normalizer =
    evaluateSettings
        . lens _normalizer (\s x -> s { _normalizer = x })

-- | Access the HTTP manager initializer.
--
-- @since 1.36
newManager
  :: (HasEvaluateSettings s)
  => Lens' s (IO Dhall.Import.Manager)
newManager =
    evaluateSettings
        . lens _newManager (\s x -> s { _newManager = x })

-- | @since 1.16
class HasEvaluateSettings s where
  evaluateSettings :: Lens' s EvaluateSettings

instance HasEvaluateSettings InputSettings where
  evaluateSettings =
    lens _evaluateSettings (\s x -> s { _evaluateSettings = x })

instance HasEvaluateSettings EvaluateSettings where
  evaluateSettings = id

-- | Parse an expression, using the supplied `InputSettings`
parseWithSettings :: MonadThrow m => InputSettings -> Text -> m (Expr Src Import)
parseWithSettings settings text =
    either throwM return (Dhall.Parser.exprFromText (view sourceName settings) text)

-- | Type-check an expression, using the supplied `InputSettings`
typecheckWithSettings :: MonadThrow m => InputSettings -> Expr Src Void -> m ()
typecheckWithSettings settings expression =
    either throwM (return . const ()) (Dhall.TypeCheck.typeWith (view startingContext settings) expression)

{-| Type-check an expression against a type provided as a Dhall expreession,
    using the supplied `InputSettings`
-}
checkWithSettings ::
    MonadThrow m =>
    -- | The input settings
    InputSettings ->
    -- | The expected type of the expression
    Expr Src Void ->
    -- | The expression to check
    Expr Src Void ->
    m ()
checkWithSettings settings type_ expression = do
    let suffix = Dhall.Pretty.Internal.prettyToStrictText type_

    let annotated = case expression of
            Note (Src begin end bytes) _ ->
                Note (Src begin end bytes') (Annot expression type_)
              where
                bytes' = bytes <> " : " <> suffix
            _ ->
                Annot expression type_

    typecheckWithSettings settings annotated

{-| Type-check an expression against a `Decoder`'s expected type, using the
    supplied `InputSettings`.
    This is equivalent of using the 'expected' type of a @Decoder@ as the second
    argument to 'checkWithSettings'.
-}
expectWithSettings :: MonadThrow m => InputSettings -> Decoder a -> Expr Src Void -> m ()
expectWithSettings settings Decoder{..} expression = do
    expected' <- case expected of
        Success x -> return x
        Failure e -> throwM e

    checkWithSettings settings expected' expression

{-| Resolve an expression, using the supplied `InputSettings`

    Note that this also applies any substitutions specified in the
    `InputSettings`
-}
resolveWithSettings :: InputSettings -> Expr Src Import -> IO (Expr Src Void)
resolveWithSettings settings expression =
    fst <$> resolveAndStatusWithSettings settings expression

-- | A version of 'resolveWithSettings' that also returns the import 'Status'
-- together with the resolved expression.
resolveAndStatusWithSettings
    :: InputSettings
    -> Expr Src Import
    -> IO (Expr Src Void, Status)
resolveAndStatusWithSettings settings expression = do
    let InputSettings{..} = settings

    let EvaluateSettings{..} = _evaluateSettings

    let transform =
               Lens.set Dhall.Import.substitutions   _substitutions
            .  Lens.set Dhall.Import.normalizer      _normalizer
            .  Lens.set Dhall.Import.startingContext _startingContext

    let status = transform (Dhall.Import.emptyStatusWithManager _newManager _rootDirectory)

    (resolved, status') <- State.runStateT (Dhall.Import.loadWith expression) status

    let substituted = Dhall.Substitution.substitute resolved (view substitutions settings)

    pure (substituted, status')

-- | Normalize an expression, using the supplied `InputSettings`
normalizeWithSettings :: InputSettings -> Expr Src Void -> Expr Src Void
normalizeWithSettings settings =
    Core.normalizeWith (view normalizer settings)

{-| Type-check and evaluate a Dhall program, decoding the result into Haskell

    The first argument determines the type of value that you decode:

>>> input integer "+2"
2
>>> input (vector double) "[1.0, 2.0]"
[1.0,2.0]

    Use `auto` to automatically select which type to decode based on the
    inferred return type:

>>> input auto "True" :: IO Bool
True

    This uses the settings from 'defaultInputSettings'.
-}
input
    :: Decoder a
    -- ^ The decoder for the Dhall value
    -> Text
    -- ^ The Dhall program
    -> IO a
    -- ^ The decoded value in Haskell
input =
  inputWithSettings defaultInputSettings

{-| Extend 'input' with a root directory to resolve imports relative
    to, a file to mention in errors as the source, a custom typing
    context, and a custom normalization process.

@since 1.16
-}
inputWithSettings
    :: InputSettings
    -> Decoder a
    -- ^ The decoder for the Dhall value
    -> Text
    -- ^ The Dhall program
    -> IO a
    -- ^ The decoded value in Haskell
inputWithSettings settings decoder@Decoder{..} text = do
    parsed <- parseWithSettings settings text

    resolved <- resolveWithSettings settings parsed

    expectWithSettings settings decoder resolved

    let normalized = normalizeWithSettings settings resolved

    case extract normalized of
        Success x -> return x
        Failure e -> Control.Exception.throwIO e

{-| Type-check and evaluate a Dhall program that is read from the
    file-system.

    This uses the settings from 'defaultEvaluateSettings'.

    @since 1.16
-}
inputFile
  :: Decoder a
  -- ^ The decoder for the Dhall value
  -> FilePath
  -- ^ The path to the Dhall program.
  -> IO a
  -- ^ The decoded value in Haskell.
inputFile =
  inputFileWithSettings defaultEvaluateSettings

{-| Extend 'inputFile' with a custom typing context and a custom
    normalization process.

@since 1.16
-}
inputFileWithSettings
  :: EvaluateSettings
  -> Decoder a
  -- ^ The decoder for the Dhall value
  -> FilePath
  -- ^ The path to the Dhall program.
  -> IO a
  -- ^ The decoded value in Haskell.
inputFileWithSettings settings ty path = do
  text <- Data.Text.IO.readFile path
  let inputSettings = InputSettings
        { _rootDirectory = takeDirectory path
        , _sourceName = path
        , _evaluateSettings = settings
        }
  inputWithSettings inputSettings ty text

{-| Similar to `input`, but without interpreting the Dhall `Expr` into a Haskell
    type.

    Uses the settings from 'defaultInputSettings'.
-}
inputExpr
    :: Text
    -- ^ The Dhall program
    -> IO (Expr Src Void)
    -- ^ The fully normalized AST
inputExpr =
  inputExprWithSettings defaultInputSettings

{-| Extend 'inputExpr' with a root directory to resolve imports relative
    to, a file to mention in errors as the source, a custom typing
    context, and a custom normalization process.

@since 1.16
-}
inputExprWithSettings
    :: InputSettings
    -> Text
    -- ^ The Dhall program
    -> IO (Expr Src Void)
    -- ^ The fully normalized AST
inputExprWithSettings settings text = do
    parsed <- parseWithSettings settings text

    resolved <- resolveWithSettings settings parsed

    _ <- typecheckWithSettings settings resolved

    pure (Core.normalizeWith (view normalizer settings) resolved)

{-| Interpret a Dhall Expression

    This takes care of import resolution, type-checking, and normalization
-}
interpretExpr :: Expr Src Import -> IO (Expr Src Void)
interpretExpr = interpretExprWithSettings defaultInputSettings

-- | Like `interpretExpr`, but customizable using `InputSettings`
interpretExprWithSettings
    :: InputSettings -> Expr Src Import -> IO (Expr Src Void)
interpretExprWithSettings settings parsed = do
    resolved <- resolveWithSettings settings parsed

    typecheckWithSettings settings resolved

    pure (Core.normalizeWith (view normalizer settings) resolved)

{- | Decode a Dhall expression

    This takes care of import resolution, type-checking and normalization
-}
fromExpr :: Decoder a -> Expr Src Import -> IO a
fromExpr = fromExprWithSettings defaultInputSettings

-- | Like `fromExpr`, but customizable using `InputSettings`
fromExprWithSettings :: InputSettings -> Decoder a -> Expr Src Import -> IO a
fromExprWithSettings settings decoder@Decoder{..} expression = do
    resolved <- resolveWithSettings settings expression

    expectWithSettings settings decoder resolved

    let normalized = Core.normalizeWith (view normalizer settings) resolved

    case extract normalized of
        Success x -> return x
        Failure e -> Control.Exception.throwIO e

-- | Use this function to extract Haskell values directly from Dhall AST.
--   The intended use case is to allow easy extraction of Dhall values for
--   making the function `Core.normalizeWith` easier to use.
--
--   For other use cases, use `input` from "Dhall" module. It will give you
--   a much better user experience.
rawInput
    :: Alternative f
    => Decoder a
    -- ^ The decoder for the Dhall value
    -> Expr s Void
    -- ^ a closed form Dhall program, which evaluates to the expected type
    -> f a
    -- ^ The decoded value in Haskell
rawInput (Decoder {..}) expr =
    case extract (Core.normalize expr) of
        Success x  -> pure x
        Failure _e -> empty

{-| Use this to provide more detailed error messages

>> input auto "True" :: IO Integer
> *** Exception: Error: Expression doesn't match annotation
>
> True : Integer
>
> (input):1:1

>> detailed (input auto "True") :: IO Integer
> *** Exception: Error: Expression doesn't match annotation
>
> Explanation: You can annotate an expression with its type or kind using the
> ❰:❱ symbol, like this:
>
>
>     ┌───────┐
>     │ x : t │  ❰x❱ is an expression and ❰t❱ is the annotated type or kind of ❰x❱
>     └───────┘
>
> The type checker verifies that the expression's type or kind matches the
> provided annotation
>
> For example, all of the following are valid annotations that the type checker
> accepts:
>
>
>     ┌─────────────┐
>     │ 1 : Natural │  ❰1❱ is an expression that has type ❰Natural❱, so the type
>     └─────────────┘  checker accepts the annotation
>
>
>     ┌───────────────────────┐
>     │ Natural/even 2 : Bool │  ❰Natural/even 2❱ has type ❰Bool❱, so the type
>     └───────────────────────┘  checker accepts the annotation
>
>
>     ┌────────────────────┐
>     │ List : Type → Type │  ❰List❱ is an expression that has kind ❰Type → Type❱,
>     └────────────────────┘  so the type checker accepts the annotation
>
>
>     ┌──────────────────┐
>     │ List Text : Type │  ❰List Text❱ is an expression that has kind ❰Type❱, so
>     └──────────────────┘  the type checker accepts the annotation
>
>
> However, the following annotations are not valid and the type checker will
> reject them:
>
>
>     ┌──────────┐
>     │ 1 : Text │  The type checker rejects this because ❰1❱ does not have type
>     └──────────┘  ❰Text❱
>
>
>     ┌─────────────┐
>     │ List : Type │  ❰List❱ does not have kind ❰Type❱
>     └─────────────┘
>
>
> You or the interpreter annotated this expression:
>
> ↳ True
>
> ... with this type or kind:
>
> ↳ Integer
>
> ... but the inferred type or kind of the expression is actually:
>
> ↳ Bool
>
> Some common reasons why you might get this error:
>
> ● The Haskell Dhall interpreter implicitly inserts a top-level annotation
>   matching the expected type
>
>   For example, if you run the following Haskell code:
>
>
>     ┌───────────────────────────────┐
>     │ >>> input auto "1" :: IO Text │
>     └───────────────────────────────┘
>
>
>   ... then the interpreter will actually type check the following annotated
>   expression:
>
>
>     ┌──────────┐
>     │ 1 : Text │
>     └──────────┘
>
>
>   ... and then type-checking will fail
>
> ────────────────────────────────────────────────────────────────────────────────
>
> True : Integer
>
> (input):1:1

-}
detailed :: IO a -> IO a
detailed =
    Control.Exception.handle handler1 . Control.Exception.handle handler0
  where
    handler0 :: Imported (TypeError Src Void) -> IO a
    handler0 (Imported ps e) =
        Control.Exception.throwIO (Imported ps (DetailedTypeError e))

    handler1 :: TypeError Src Void -> IO a
    handler1 e = Control.Exception.throwIO (DetailedTypeError e)