module Dhall.LSP.Backend.Dhall (
  FileIdentifier,
  fileIdentifierFromFilePath,
  fileIdentifierFromURI,
  hashNormalToCode,
  WellTyped,
  fromWellTyped,
  Normal,
  fromNormal,
  Cache,
  emptyCache,
  invalidate,
  DhallError(..),
  parse,
  parseWithHeader,
  load,
  typecheck,
  normalize
 ) where

import Dhall.Core   (Expr)
import Dhall.Parser (Src)

import Control.Exception                (SomeException, catch)
import Control.Lens                     (set, view)
import Control.Monad.Trans.State.Strict (runStateT)
import Data.Bifunctor                   (first)
import Data.List.NonEmpty               (NonEmpty ((:|)))
import Data.Text                        (Text)
import Data.Void                        (Void)
import Network.URI                      (URI)
import System.FilePath
    ( splitDirectories
    , takeDirectory
    , takeFileName
    )

import qualified Data.Graph         as Graph
import qualified Data.Map.Strict    as Map
import qualified Data.Set           as Set
import qualified Data.Text          as Text
import qualified Dhall.Core         as Dhall
import qualified Dhall.Import       as Dhall
import qualified Dhall.Map
import qualified Dhall.Parser       as Dhall
import qualified Dhall.TypeCheck    as Dhall
import qualified Language.LSP.Types as LSP.Types
import qualified Network.URI        as URI


-- | A @FileIdentifier@ represents either a local file or a remote url.
newtype FileIdentifier = FileIdentifier Dhall.Chained

-- | Construct a FileIdentifier from a local file path.
fileIdentifierFromFilePath :: FilePath -> FileIdentifier
fileIdentifierFromFilePath :: FilePath -> FileIdentifier
fileIdentifierFromFilePath FilePath
path =
  let filename :: Text
filename = FilePath -> Text
Text.pack (FilePath -> Text) -> FilePath -> Text
forall a b. (a -> b) -> a -> b
$ FilePath -> FilePath
takeFileName FilePath
path
      directory :: FilePath
directory = FilePath -> FilePath
takeDirectory FilePath
path
      components :: [Text]
components = (FilePath -> Text) -> [FilePath] -> [Text]
forall a b. (a -> b) -> [a] -> [b]
map FilePath -> Text
Text.pack ([FilePath] -> [Text])
-> (FilePath -> [FilePath]) -> FilePath -> [Text]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [FilePath] -> [FilePath]
forall a. [a] -> [a]
reverse ([FilePath] -> [FilePath])
-> (FilePath -> [FilePath]) -> FilePath -> [FilePath]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. FilePath -> [FilePath]
splitDirectories (FilePath -> [Text]) -> FilePath -> [Text]
forall a b. (a -> b) -> a -> b
$ FilePath
directory
      file :: File
file = Directory -> Text -> File
Dhall.File ([Text] -> Directory
Dhall.Directory [Text]
components) Text
filename
  in Chained -> FileIdentifier
FileIdentifier (Chained -> FileIdentifier) -> Chained -> FileIdentifier
forall a b. (a -> b) -> a -> b
$ FilePrefix -> File -> ImportMode -> Chained
Dhall.chainedFromLocalHere FilePrefix
Dhall.Absolute File
file ImportMode
Dhall.Code

-- | Construct a FileIdentifier from a given URI. Supports only "file:" URIs.
fileIdentifierFromURI :: URI -> Maybe FileIdentifier
fileIdentifierFromURI :: URI -> Maybe FileIdentifier
fileIdentifierFromURI URI
uri
  | URI -> FilePath
URI.uriScheme URI
uri FilePath -> FilePath -> Bool
forall a. Eq a => a -> a -> Bool
== FilePath
"file:" = do
    FilePath
path <- Uri -> Maybe FilePath
LSP.Types.uriToFilePath (Uri -> Maybe FilePath)
-> (FilePath -> Uri) -> FilePath -> Maybe FilePath
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Text -> Uri
LSP.Types.Uri (Text -> Uri) -> (FilePath -> Text) -> FilePath -> Uri
forall b c a. (b -> c) -> (a -> b) -> a -> c
. FilePath -> Text
Text.pack
                  (FilePath -> Maybe FilePath) -> FilePath -> Maybe FilePath
forall a b. (a -> b) -> a -> b
$ (FilePath -> FilePath) -> URI -> FilePath -> FilePath
URI.uriToString FilePath -> FilePath
forall a. a -> a
id URI
uri FilePath
""
    FileIdentifier -> Maybe FileIdentifier
forall (m :: * -> *) a. Monad m => a -> m a
return (FileIdentifier -> Maybe FileIdentifier)
-> FileIdentifier -> Maybe FileIdentifier
forall a b. (a -> b) -> a -> b
$ FilePath -> FileIdentifier
fileIdentifierFromFilePath FilePath
path
fileIdentifierFromURI URI
_ = Maybe FileIdentifier
forall a. Maybe a
Nothing

-- | A well-typed expression.
newtype WellTyped = WellTyped {WellTyped -> Expr Src Void
fromWellTyped :: Expr Src Void}

-- | A fully normalised expression.
newtype Normal = Normal {Normal -> Expr Src Void
fromNormal :: Expr Src Void}

-- An import graph, represented by list of import dependencies.
type ImportGraph = [Dhall.Depends]

-- | A cache maps Dhall imports to fully normalised expressions. By reusing
--   caches we can speeds up diagnostics etc. significantly!
data Cache = Cache ImportGraph (Dhall.Map.Map Dhall.Chained Dhall.ImportSemantics)

-- | The initial cache.
emptyCache :: Cache
emptyCache :: Cache
emptyCache = ImportGraph -> Map Chained ImportSemantics -> Cache
Cache [] Map Chained ImportSemantics
forall k v. Ord k => Map k v
Dhall.Map.empty

-- | Invalidate any _unhashed_ imports of the given file. Hashed imports are
--   kept around as per
--   https://github.com/dhall-lang/dhall-lang/blob/master/standard/imports.md.
--   Transitively invalidates any imports depending on the changed file.
invalidate :: FileIdentifier -> Cache -> Cache
invalidate :: FileIdentifier -> Cache -> Cache
invalidate (FileIdentifier Chained
chained) (Cache ImportGraph
dependencies Map Chained ImportSemantics
cache) =
  ImportGraph -> Map Chained ImportSemantics -> Cache
Cache ImportGraph
dependencies' (Map Chained ImportSemantics -> Cache)
-> Map Chained ImportSemantics -> Cache
forall a b. (a -> b) -> a -> b
$ Map Chained ImportSemantics
-> Set Chained -> Map Chained ImportSemantics
forall k a. Ord k => Map k a -> Set k -> Map k a
Dhall.Map.withoutKeys Map Chained ImportSemantics
cache Set Chained
invalidImports
  where
    imports :: [Chained]
imports = (Depends -> Chained) -> ImportGraph -> [Chained]
forall a b. (a -> b) -> [a] -> [b]
map Depends -> Chained
Dhall.parent ImportGraph
dependencies [Chained] -> [Chained] -> [Chained]
forall a. [a] -> [a] -> [a]
++ (Depends -> Chained) -> ImportGraph -> [Chained]
forall a b. (a -> b) -> [a] -> [b]
map Depends -> Chained
Dhall.child ImportGraph
dependencies

    adjacencyLists :: Map Chained [Chained]
adjacencyLists = (Depends -> Map Chained [Chained] -> Map Chained [Chained])
-> Map Chained [Chained] -> ImportGraph -> Map Chained [Chained]
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr
                       -- add reversed edges to adjacency lists
                       (\(Dhall.Depends Chained
parent Chained
child) -> ([Chained] -> [Chained])
-> Chained -> Map Chained [Chained] -> Map Chained [Chained]
forall k a. Ord k => (a -> a) -> k -> Map k a -> Map k a
Map.adjust (Chained
parent Chained -> [Chained] -> [Chained]
forall a. a -> [a] -> [a]
:) Chained
child)
                       -- starting from the discrete graph
                       ([(Chained, [Chained])] -> Map Chained [Chained]
forall k a. Ord k => [(k, a)] -> Map k a
Map.fromList [ (Chained
i,[]) | Chained
i <- [Chained]
imports])
                       ImportGraph
dependencies

    (Graph
graph, Vertex -> (Chained, Chained, [Chained])
importFromVertex, Chained -> Maybe Vertex
vertexFromImport) = [(Chained, Chained, [Chained])]
-> (Graph, Vertex -> (Chained, Chained, [Chained]),
    Chained -> Maybe Vertex)
forall key node.
Ord key =>
[(node, key, [key])]
-> (Graph, Vertex -> (node, key, [key]), key -> Maybe Vertex)
Graph.graphFromEdges
      [(Chained
node, Chained
node, [Chained]
neighbours) | (Chained
node, [Chained]
neighbours) <- Map Chained [Chained] -> [(Chained, [Chained])]
forall k a. Map k a -> [(k, a)]
Map.assocs Map Chained [Chained]
adjacencyLists]

    -- compute the reverse dependencies, i.e. the imports reachable in the transposed graph
    reachableImports :: Chained -> [Chained]
reachableImports Chained
import_ =
      ((Vertex -> Chained) -> [Vertex] -> [Chained]
forall a b. (a -> b) -> [a] -> [b]
map ((\ (Chained
i, Chained
_, [Chained]
_) -> Chained
i) ((Chained, Chained, [Chained]) -> Chained)
-> (Vertex -> (Chained, Chained, [Chained])) -> Vertex -> Chained
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Vertex -> (Chained, Chained, [Chained])
importFromVertex) ([Vertex] -> [Chained])
-> (Maybe [Vertex] -> [Vertex]) -> Maybe [Vertex] -> [Chained]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Maybe [Vertex] -> [Vertex]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat) (Maybe [Vertex] -> [Chained]) -> Maybe [Vertex] -> [Chained]
forall a b. (a -> b) -> a -> b
$
        do Vertex
vertex <- Chained -> Maybe Vertex
vertexFromImport Chained
import_
           [Vertex] -> Maybe [Vertex]
forall (m :: * -> *) a. Monad m => a -> m a
return (Graph -> Vertex -> [Vertex]
Graph.reachable Graph
graph Vertex
vertex)

    codeImport :: Chained
codeImport = ImportMode -> Chained -> Chained
Dhall.chainedChangeMode ImportMode
Dhall.Code Chained
chained
    textImport :: Chained
textImport = ImportMode -> Chained -> Chained
Dhall.chainedChangeMode ImportMode
Dhall.RawText Chained
chained
    invalidImports :: Set Chained
invalidImports = [Chained] -> Set Chained
forall a. Ord a => [a] -> Set a
Set.fromList ([Chained] -> Set Chained) -> [Chained] -> Set Chained
forall a b. (a -> b) -> a -> b
$ Chained
codeImport Chained -> [Chained] -> [Chained]
forall a. a -> [a] -> [a]
: Chained -> [Chained]
reachableImports Chained
codeImport
                                    [Chained] -> [Chained] -> [Chained]
forall a. [a] -> [a] -> [a]
++ Chained
textImport Chained -> [Chained] -> [Chained]
forall a. a -> [a] -> [a]
: Chained -> [Chained]
reachableImports Chained
textImport

    dependencies' :: ImportGraph
dependencies' = (Depends -> Bool) -> ImportGraph -> ImportGraph
forall a. (a -> Bool) -> [a] -> [a]
filter (\(Dhall.Depends Chained
parent Chained
child) -> Chained -> Set Chained -> Bool
forall a. Ord a => a -> Set a -> Bool
Set.notMember Chained
parent Set Chained
invalidImports
                                Bool -> Bool -> Bool
&& Chained -> Set Chained -> Bool
forall a. Ord a => a -> Set a -> Bool
Set.notMember Chained
child Set Chained
invalidImports) ImportGraph
dependencies

-- | A Dhall error. Covers parsing, resolving of imports, typechecking and
--   normalisation.
data DhallError = ErrorInternal SomeException
                | ErrorImportSourced (Dhall.SourcedException Dhall.MissingImports)
                | ErrorTypecheck (Dhall.TypeError Src Void)
                | ErrorParse Dhall.ParseError

-- | Parse a Dhall expression.
parse :: Text -> Either DhallError (Expr Src Dhall.Import)
parse :: Text -> Either DhallError (Expr Src Import)
parse = ((Header, Expr Src Import) -> Expr Src Import)
-> Either DhallError (Header, Expr Src Import)
-> Either DhallError (Expr Src Import)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (Header, Expr Src Import) -> Expr Src Import
forall a b. (a, b) -> b
snd (Either DhallError (Header, Expr Src Import)
 -> Either DhallError (Expr Src Import))
-> (Text -> Either DhallError (Header, Expr Src Import))
-> Text
-> Either DhallError (Expr Src Import)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Text -> Either DhallError (Header, Expr Src Import)
parseWithHeader

-- | Parse a Dhall expression along with its "header", i.e. whitespace and
--   comments prefixing the actual code.
parseWithHeader :: Text -> Either DhallError (Dhall.Header, Expr Src Dhall.Import)
parseWithHeader :: Text -> Either DhallError (Header, Expr Src Import)
parseWithHeader = (ParseError -> DhallError)
-> Either ParseError (Header, Expr Src Import)
-> Either DhallError (Header, Expr Src Import)
forall (p :: * -> * -> *) a b c.
Bifunctor p =>
(a -> b) -> p a c -> p b c
first ParseError -> DhallError
ErrorParse (Either ParseError (Header, Expr Src Import)
 -> Either DhallError (Header, Expr Src Import))
-> (Text -> Either ParseError (Header, Expr Src Import))
-> Text
-> Either DhallError (Header, Expr Src Import)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. FilePath -> Text -> Either ParseError (Header, Expr Src Import)
Dhall.exprAndHeaderFromText FilePath
""

-- | Resolve all imports in an expression.
load :: FileIdentifier -> Expr Src Dhall.Import -> Cache ->
  IO (Either DhallError (Cache, Expr Src Void))
load :: FileIdentifier
-> Expr Src Import
-> Cache
-> IO (Either DhallError (Cache, Expr Src Void))
load (FileIdentifier Chained
chained) Expr Src Import
expr (Cache ImportGraph
graph Map Chained ImportSemantics
cache) = do
  let emptyStatus :: Status
emptyStatus = FilePath -> Status
Dhall.emptyStatus FilePath
""
      status :: Status
status = -- reuse cache and import graph
               ASetter
  Status
  Status
  (Map Chained ImportSemantics)
  (Map Chained ImportSemantics)
-> Map Chained ImportSemantics -> Status -> Status
forall s t a b. ASetter s t a b -> b -> s -> t
set ASetter
  Status
  Status
  (Map Chained ImportSemantics)
  (Map Chained ImportSemantics)
forall (f :: * -> *).
Functor f =>
LensLike' f Status (Map Chained ImportSemantics)
Dhall.cache Map Chained ImportSemantics
cache (Status -> Status) -> (Status -> Status) -> Status -> Status
forall b c a. (b -> c) -> (a -> b) -> a -> c
.
               ASetter Status Status ImportGraph ImportGraph
-> ImportGraph -> Status -> Status
forall s t a b. ASetter s t a b -> b -> s -> t
set ASetter Status Status ImportGraph ImportGraph
forall (f :: * -> *). Functor f => LensLike' f Status ImportGraph
Dhall.graph ImportGraph
graph (Status -> Status) -> (Status -> Status) -> Status -> Status
forall b c a. (b -> c) -> (a -> b) -> a -> c
.
               -- set "root import"
               ASetter Status Status (NonEmpty Chained) (NonEmpty Chained)
-> NonEmpty Chained -> Status -> Status
forall s t a b. ASetter s t a b -> b -> s -> t
set ASetter Status Status (NonEmpty Chained) (NonEmpty Chained)
forall (f :: * -> *).
Functor f =>
LensLike' f Status (NonEmpty Chained)
Dhall.stack (Chained
chained Chained -> [Chained] -> NonEmpty Chained
forall a. a -> [a] -> NonEmpty a
:| [])
                 (Status -> Status) -> Status -> Status
forall a b. (a -> b) -> a -> b
$ Status
emptyStatus
  (do (Expr Src Void
expr', Status
status') <- StateT Status IO (Expr Src Void)
-> Status -> IO (Expr Src Void, Status)
forall s (m :: * -> *) a. StateT s m a -> s -> m (a, s)
runStateT (Expr Src Import -> StateT Status IO (Expr Src Void)
Dhall.loadWith Expr Src Import
expr) Status
status
      let cache' :: Map Chained ImportSemantics
cache' = Getting
  (Map Chained ImportSemantics) Status (Map Chained ImportSemantics)
-> Status -> Map Chained ImportSemantics
forall s (m :: * -> *) a. MonadReader s m => Getting a s a -> m a
view Getting
  (Map Chained ImportSemantics) Status (Map Chained ImportSemantics)
forall (f :: * -> *).
Functor f =>
LensLike' f Status (Map Chained ImportSemantics)
Dhall.cache Status
status'
          graph' :: ImportGraph
graph' = Getting ImportGraph Status ImportGraph -> Status -> ImportGraph
forall s (m :: * -> *) a. MonadReader s m => Getting a s a -> m a
view Getting ImportGraph Status ImportGraph
forall (f :: * -> *). Functor f => LensLike' f Status ImportGraph
Dhall.graph Status
status'
      Either DhallError (Cache, Expr Src Void)
-> IO (Either DhallError (Cache, Expr Src Void))
forall (m :: * -> *) a. Monad m => a -> m a
return (Either DhallError (Cache, Expr Src Void)
 -> IO (Either DhallError (Cache, Expr Src Void)))
-> ((Cache, Expr Src Void)
    -> Either DhallError (Cache, Expr Src Void))
-> (Cache, Expr Src Void)
-> IO (Either DhallError (Cache, Expr Src Void))
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Cache, Expr Src Void) -> Either DhallError (Cache, Expr Src Void)
forall a b. b -> Either a b
Right ((Cache, Expr Src Void)
 -> IO (Either DhallError (Cache, Expr Src Void)))
-> (Cache, Expr Src Void)
-> IO (Either DhallError (Cache, Expr Src Void))
forall a b. (a -> b) -> a -> b
$ (ImportGraph -> Map Chained ImportSemantics -> Cache
Cache ImportGraph
graph' Map Chained ImportSemantics
cache', Expr Src Void
expr'))
    IO (Either DhallError (Cache, Expr Src Void))
-> (SourcedException MissingImports
    -> IO (Either DhallError (Cache, Expr Src Void)))
-> IO (Either DhallError (Cache, Expr Src Void))
forall e a. Exception e => IO a -> (e -> IO a) -> IO a
`catch` (\SourcedException MissingImports
e -> Either DhallError (Cache, Expr Src Void)
-> IO (Either DhallError (Cache, Expr Src Void))
forall (m :: * -> *) a. Monad m => a -> m a
return (Either DhallError (Cache, Expr Src Void)
 -> IO (Either DhallError (Cache, Expr Src Void)))
-> (DhallError -> Either DhallError (Cache, Expr Src Void))
-> DhallError
-> IO (Either DhallError (Cache, Expr Src Void))
forall b c a. (b -> c) -> (a -> b) -> a -> c
. DhallError -> Either DhallError (Cache, Expr Src Void)
forall a b. a -> Either a b
Left (DhallError -> IO (Either DhallError (Cache, Expr Src Void)))
-> DhallError -> IO (Either DhallError (Cache, Expr Src Void))
forall a b. (a -> b) -> a -> b
$ SourcedException MissingImports -> DhallError
ErrorImportSourced SourcedException MissingImports
e)
    IO (Either DhallError (Cache, Expr Src Void))
-> (SomeException -> IO (Either DhallError (Cache, Expr Src Void)))
-> IO (Either DhallError (Cache, Expr Src Void))
forall e a. Exception e => IO a -> (e -> IO a) -> IO a
`catch` (\SomeException
e -> Either DhallError (Cache, Expr Src Void)
-> IO (Either DhallError (Cache, Expr Src Void))
forall (m :: * -> *) a. Monad m => a -> m a
return (Either DhallError (Cache, Expr Src Void)
 -> IO (Either DhallError (Cache, Expr Src Void)))
-> (DhallError -> Either DhallError (Cache, Expr Src Void))
-> DhallError
-> IO (Either DhallError (Cache, Expr Src Void))
forall b c a. (b -> c) -> (a -> b) -> a -> c
. DhallError -> Either DhallError (Cache, Expr Src Void)
forall a b. a -> Either a b
Left (DhallError -> IO (Either DhallError (Cache, Expr Src Void)))
-> DhallError -> IO (Either DhallError (Cache, Expr Src Void))
forall a b. (a -> b) -> a -> b
$ SomeException -> DhallError
ErrorInternal SomeException
e)

-- | Typecheck a fully resolved expression. Returns a certification that the
--   input was well-typed along with its (well-typed) type.
typecheck :: Expr Src Void -> Either DhallError (WellTyped, WellTyped)
typecheck :: Expr Src Void -> Either DhallError (WellTyped, WellTyped)
typecheck Expr Src Void
expr = 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 Expr Src Void
expr of
  Left TypeError Src Void
err -> DhallError -> Either DhallError (WellTyped, WellTyped)
forall a b. a -> Either a b
Left (DhallError -> Either DhallError (WellTyped, WellTyped))
-> DhallError -> Either DhallError (WellTyped, WellTyped)
forall a b. (a -> b) -> a -> b
$ TypeError Src Void -> DhallError
ErrorTypecheck TypeError Src Void
err
  Right Expr Src Void
typ -> (WellTyped, WellTyped) -> Either DhallError (WellTyped, WellTyped)
forall a b. b -> Either a b
Right (Expr Src Void -> WellTyped
WellTyped Expr Src Void
expr, Expr Src Void -> WellTyped
WellTyped Expr Src Void
typ)

-- | Normalise a well-typed expression.
normalize :: WellTyped -> Normal
normalize :: WellTyped -> Normal
normalize (WellTyped Expr Src Void
expr) = Expr Src Void -> Normal
Normal (Expr Src Void -> Normal) -> Expr Src Void -> Normal
forall a b. (a -> b) -> a -> b
$ Expr Src Void -> Expr Src Void
forall a s t. Eq a => Expr s a -> Expr t a
Dhall.normalize Expr Src Void
expr

-- | Given a normal expression compute the hash (using the default standard
--   version) of its alpha-normal form. Returns the hash in the format used in
--   Dhall's hash annotations (prefixed by "sha256:" and base-64 encoded).
hashNormalToCode :: Normal -> Text
hashNormalToCode :: Normal -> Text
hashNormalToCode (Normal Expr Src Void
expr) =
  Expr Void Void -> Text
Dhall.hashExpressionToCode (Expr Src Void -> Expr Void Void
forall s a t. Expr s a -> Expr t a
Dhall.denote Expr Src Void
alphaNormal)
  where alphaNormal :: Expr Src Void
alphaNormal = Expr Src Void -> Expr Src Void
forall s a. Expr s a -> Expr s a
Dhall.alphaNormalize Expr Src Void
expr