{-# LANGUAGE RankNTypes         #-}
{-# LANGUAGE RecordWildCards    #-}

{-| This module contains the core calculus for the Dhall language.

    Dhall is essentially a fork of the @morte@ compiler but with more built-in
    functionality, better error messages, and Haskell integration
-}

module Dhall.Core (
    -- * Syntax
      Const(..)
    , Directory(..)
    , File(..)
    , FilePrefix(..)
    , Import(..)
    , ImportHashed(..)
    , ImportMode(..)
    , ImportType(..)
    , URL(..)
    , Scheme(..)
    , DhallDouble(..)
    , Var(..)
    , Binding(..)
    , makeBinding
    , Chunks(..)
    , Expr(..)

    -- * Normalization
    , alphaNormalize
    , normalize
    , normalizeWith
    , normalizeWithM
    , Normalizer
    , NormalizerM
    , ReifiedNormalizer (..)
    , judgmentallyEqual
    , subst
    , shift
    , isNormalized
    , isNormalizedWith
    , denote
    , renote
    , shallowDenote
    , freeIn

    -- * Pretty-printing
    , pretty

    -- * Optics
    , subExpressions
    , chunkExprs
    , bindingExprs

    -- * Let-blocks
    , multiLet
    , wrapInLets
    , MultiLet(..)

    -- * Miscellaneous
    , internalError
    , reservedIdentifiers
    , escapeText
    , pathCharacter
    , throws
    , Eval.textShow
    , censorExpression
    , censorText
    ) where

import Control.Exception (Exception)
import Control.Monad.IO.Class (MonadIO(..))
import Data.Semigroup (Semigroup(..))
import Data.Text (Text)
import Data.Text.Prettyprint.Doc (Pretty)
import Dhall.Normalize
import Dhall.Src (Src(..))
import Dhall.Syntax
import Dhall.Pretty.Internal
import Instances.TH.Lift ()
import Lens.Family (over)
import Prelude hiding (succ)

import qualified Control.Exception
import qualified Dhall.Eval    as Eval
import qualified Data.Text

-- | Pretty-print a value
pretty :: Pretty a => a -> Text
pretty :: a -> Text
pretty = a -> Text
forall a. Pretty a => a -> Text
pretty_
{-# INLINE pretty #-}

_ERROR :: String
_ERROR :: String
_ERROR = "\ESC[1;31mError\ESC[0m"

{-| Utility function used to throw internal errors that should never happen
    (in theory) but that are not enforced by the type system
-}
internalError :: Data.Text.Text -> forall b . b
internalError :: Text -> forall b. b
internalError text :: Text
text = String -> b
forall a. HasCallStack => String -> a
error ([String] -> String
unlines
    [ String
_ERROR String -> String -> String
forall a. Semigroup a => a -> a -> a
<> ": Compiler bug                                                        "
    , "                                                                                "
    , "Explanation: This error message means that there is a bug in the Dhall compiler."
    , "You didn't do anything wrong, but if you would like to see this problem fixed   "
    , "then you should report the bug at:                                              "
    , "                                                                                "
    , "https://github.com/dhall-lang/dhall-haskell/issues                              "
    , "                                                                                "
    , "Please include the following text in your bug report:                           "
    , "                                                                                "
    , "```                                                                             "
    , Text -> String
Data.Text.unpack Text
text String -> String -> String
forall a. Semigroup a => a -> a -> a
<> "                                                       "
    , "```                                                                             "
    ] )

{-| Escape a `Text` literal using Dhall's escaping rules

    Note that the result does not include surrounding quotes
-}
escapeText :: Text -> Text
escapeText :: Text -> Text
escapeText = Text -> Text
escapeText_
{-# INLINE escapeText #-}


{-| Utility used to implement the @--censor@ flag, by:

    * Replacing all `Src` text with spaces
    * Replacing all `Text` literals inside type errors with spaces
-}
censorExpression :: Expr Src a -> Expr Src a
censorExpression :: Expr Src a -> Expr Src a
censorExpression (TextLit chunks :: Chunks Src a
chunks) = Chunks Src a -> Expr Src a
forall s a. Chunks s a -> Expr s a
TextLit (Chunks Src a -> Chunks Src a
forall a. Chunks Src a -> Chunks Src a
censorChunks Chunks Src a
chunks)
censorExpression (Note src :: Src
src     e :: Expr Src a
e) = Src -> Expr Src a -> Expr Src a
forall s a. s -> Expr s a -> Expr s a
Note (Src -> Src
censorSrc Src
src) (Expr Src a -> Expr Src a
forall a. Expr Src a -> Expr Src a
censorExpression Expr Src a
e)
censorExpression  e :: Expr Src a
e               = ASetter (Expr Src a) (Expr Src a) (Expr Src a) (Expr Src a)
-> (Expr Src a -> Expr Src a) -> Expr Src a -> Expr Src a
forall s t a b. ASetter s t a b -> (a -> b) -> s -> t
over ASetter (Expr Src a) (Expr Src a) (Expr Src a) (Expr Src a)
forall (f :: * -> *) s a.
Applicative f =>
(Expr s a -> f (Expr s a)) -> Expr s a -> f (Expr s a)
subExpressions Expr Src a -> Expr Src a
forall a. Expr Src a -> Expr Src a
censorExpression Expr Src a
e

censorChunks :: Chunks Src a -> Chunks Src a
censorChunks :: Chunks Src a -> Chunks Src a
censorChunks (Chunks xys :: [(Text, Expr Src a)]
xys z :: Text
z) = [(Text, Expr Src a)] -> Text -> Chunks Src a
forall s a. [(Text, Expr s a)] -> Text -> Chunks s a
Chunks [(Text, Expr Src a)]
xys' Text
z'
  where
    z' :: Text
z' = Text -> Text
censorText Text
z

    xys' :: [(Text, Expr Src a)]
xys' = [ (Text -> Text
censorText Text
x, Expr Src a -> Expr Src a
forall a. Expr Src a -> Expr Src a
censorExpression Expr Src a
y) | (x :: Text
x, y :: Expr Src a
y) <- [(Text, Expr Src a)]
xys ]

-- | Utility used to censor `Text` by replacing all characters with a space
censorText :: Text -> Text
censorText :: Text -> Text
censorText = (Char -> Char) -> Text -> Text
Data.Text.map (\_ -> ' ')

censorSrc :: Src -> Src
censorSrc :: Src -> Src
censorSrc (Src { srcText :: Src -> Text
srcText = Text
oldText, .. }) = $WSrc :: SourcePos -> SourcePos -> Text -> Src
Src { srcText :: Text
srcText = Text
newText, .. }
  where
    newText :: Text
newText = Text -> Text
censorText Text
oldText

{-| Convenience utility for converting `Either`-based exceptions to `IO`-based
    exceptions
-}
throws :: (Exception e, MonadIO io) => Either e a -> io a
throws :: Either e a -> io a
throws (Left  e :: e
e) = IO a -> io a
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (e -> IO a
forall e a. Exception e => e -> IO a
Control.Exception.throwIO e
e)
throws (Right r :: a
r) = a -> io a
forall (m :: * -> *) a. Monad m => a -> m a
return a
r

{- $setup
>>> import qualified Codec.Serialise
>>> import qualified Dhall.Binary
>>> import Data.SpecialValues
>>> import Test.QuickCheck (Arbitrary(..), oneof, elements)
>>> :{
  instance Arbitrary DhallDouble where
    arbitrary = fmap DhallDouble (oneof [ arbitrary, elements specialValues ])
:}
-}