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.Haskell.LSP.Types as LSP.Types
import qualified Network.URI as URI
newtype FileIdentifier = FileIdentifier Dhall.Chained
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
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
newtype WellTyped = WellTyped {WellTyped -> Expr Src Void
fromWellTyped :: Expr Src Void}
newtype Normal = Normal {Normal -> Expr Src Void
fromNormal :: Expr Src Void}
type ImportGraph = [Dhall.Depends]
data Cache = Cache ImportGraph (Dhall.Map.Map Dhall.Chained Dhall.ImportSemantics)
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 :: 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
(\(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)
([(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]
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
data DhallError = ErrorInternal SomeException
| ErrorImportSourced (Dhall.SourcedException Dhall.MissingImports)
| ErrorTypecheck (Dhall.TypeError Src Void)
| ErrorParse Dhall.ParseError
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
parseWithHeader :: Text -> Either DhallError (Dhall.Header, Expr Src Dhall.Import)
= (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
""
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 =
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
.
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 :: 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)
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
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