2019-07-01 19:30:32 +02:00
|
|
|
module Dhall.LSP.Backend.Dhall (
|
|
|
|
FileIdentifier,
|
|
|
|
fileIdentifierFromFilePath,
|
|
|
|
fileIdentifierFromURI,
|
2019-07-19 19:24:11 +02:00
|
|
|
hashNormalToCode,
|
2019-07-01 19:30:32 +02:00
|
|
|
WellTyped,
|
|
|
|
fromWellTyped,
|
|
|
|
Normal,
|
|
|
|
fromNormal,
|
|
|
|
Cache,
|
|
|
|
emptyCache,
|
|
|
|
invalidate,
|
|
|
|
DhallError(..),
|
|
|
|
parse,
|
|
|
|
parseWithHeader,
|
|
|
|
load,
|
|
|
|
typecheck,
|
|
|
|
normalize
|
|
|
|
) where
|
2019-06-13 16:23:48 +02:00
|
|
|
|
2019-07-01 19:30:32 +02:00
|
|
|
import Dhall.Parser (Src)
|
2019-06-13 16:23:48 +02:00
|
|
|
import Dhall.Core (Expr)
|
|
|
|
|
2019-07-01 19:30:32 +02:00
|
|
|
import qualified Dhall.Core as Dhall
|
|
|
|
import qualified Dhall.Import as Dhall
|
|
|
|
import qualified Dhall.Parser as Dhall
|
|
|
|
import qualified Dhall.TypeCheck as Dhall
|
|
|
|
|
2019-07-08 12:55:15 +02:00
|
|
|
import qualified Data.Graph as Graph
|
2019-07-01 19:30:32 +02:00
|
|
|
import qualified Data.Map.Strict as Map
|
2019-07-08 12:55:15 +02:00
|
|
|
import qualified Data.Set as Set
|
2019-07-01 19:30:32 +02:00
|
|
|
import qualified Network.URI as URI
|
|
|
|
import qualified Language.Haskell.LSP.Types as LSP.Types
|
|
|
|
import qualified Data.Text as Text
|
|
|
|
|
|
|
|
import Data.List.NonEmpty (NonEmpty((:|)))
|
2019-06-13 16:23:48 +02:00
|
|
|
import Data.Text (Text)
|
2019-10-14 07:22:39 +02:00
|
|
|
import Data.Void (Void)
|
2019-07-01 19:30:32 +02:00
|
|
|
import System.FilePath (splitDirectories, takeFileName, takeDirectory)
|
|
|
|
import Lens.Family (view, set)
|
|
|
|
import Control.Exception (SomeException, catch)
|
|
|
|
import Control.Monad.Trans.State.Strict (runStateT)
|
|
|
|
import Network.URI (URI)
|
|
|
|
import Data.Bifunctor (first)
|
|
|
|
|
|
|
|
-- | A @FileIdentifier@ represents either a local file or a remote url.
|
2019-07-17 17:20:48 +02:00
|
|
|
newtype FileIdentifier = FileIdentifier Dhall.Chained
|
2019-07-01 19:30:32 +02:00
|
|
|
|
|
|
|
-- | Construct a FileIdentifier from a local file path.
|
|
|
|
fileIdentifierFromFilePath :: FilePath -> FileIdentifier
|
|
|
|
fileIdentifierFromFilePath path =
|
|
|
|
let filename = Text.pack $ takeFileName path
|
|
|
|
directory = takeDirectory path
|
|
|
|
components = map Text.pack . reverse . splitDirectories $ directory
|
2019-07-17 17:20:48 +02:00
|
|
|
file = Dhall.File (Dhall.Directory components) filename
|
|
|
|
in FileIdentifier $ Dhall.chainedFromLocalHere Dhall.Absolute file Dhall.Code
|
2019-07-01 19:30:32 +02:00
|
|
|
|
2019-07-17 17:20:48 +02:00
|
|
|
-- | Construct a FileIdentifier from a given URI. Supports only "file:" URIs.
|
2019-07-01 19:30:32 +02:00
|
|
|
fileIdentifierFromURI :: URI -> Maybe FileIdentifier
|
|
|
|
fileIdentifierFromURI uri
|
|
|
|
| URI.uriScheme uri == "file:" = do
|
|
|
|
path <- LSP.Types.uriToFilePath . LSP.Types.Uri . Text.pack
|
|
|
|
$ URI.uriToString id uri ""
|
|
|
|
return $ fileIdentifierFromFilePath path
|
2019-07-17 17:20:48 +02:00
|
|
|
fileIdentifierFromURI _ = Nothing
|
2019-07-01 19:30:32 +02:00
|
|
|
|
|
|
|
-- | A well-typed expression.
|
2019-10-14 07:22:39 +02:00
|
|
|
newtype WellTyped = WellTyped {fromWellTyped :: Expr Src Void}
|
2019-07-01 19:30:32 +02:00
|
|
|
|
|
|
|
-- | A fully normalised expression.
|
2019-10-14 07:22:39 +02:00
|
|
|
newtype Normal = Normal {fromNormal :: Expr Src Void}
|
2019-07-01 19:30:32 +02:00
|
|
|
|
2019-07-08 12:55:15 +02:00
|
|
|
-- An import graph, represented by list of import dependencies.
|
|
|
|
type ImportGraph = [Dhall.Depends]
|
|
|
|
|
2019-07-01 19:30:32 +02:00
|
|
|
-- | A cache maps Dhall imports to fully normalised expressions. By reusing
|
|
|
|
-- caches we can speeds up diagnostics etc. significantly!
|
2019-07-23 18:11:33 +02:00
|
|
|
data Cache = Cache ImportGraph (Map.Map Dhall.Chained Dhall.ImportSemantics)
|
2019-07-01 19:30:32 +02:00
|
|
|
|
|
|
|
-- | The initial cache.
|
|
|
|
emptyCache :: Cache
|
2019-07-08 12:55:15 +02:00
|
|
|
emptyCache = Cache [] Map.empty
|
2019-06-13 16:23:48 +02:00
|
|
|
|
2019-07-01 19:30:32 +02:00
|
|
|
-- | 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.
|
2019-07-08 12:55:15 +02:00
|
|
|
-- Transitively invalidates any imports depending on the changed file.
|
2019-07-01 19:30:32 +02:00
|
|
|
invalidate :: FileIdentifier -> Cache -> Cache
|
2019-07-17 17:20:48 +02:00
|
|
|
invalidate (FileIdentifier chained) (Cache dependencies cache) =
|
2019-07-08 12:55:15 +02:00
|
|
|
Cache dependencies' $ Map.withoutKeys cache invalidImports
|
2019-06-13 16:23:48 +02:00
|
|
|
where
|
2019-07-08 12:55:15 +02:00
|
|
|
imports = map Dhall.parent dependencies ++ map Dhall.child dependencies
|
|
|
|
|
|
|
|
adjacencyLists = foldr
|
|
|
|
-- add reversed edges to adjacency lists
|
|
|
|
(\(Dhall.Depends parent child) -> Map.adjust (parent :) child)
|
|
|
|
-- starting from the discrete graph
|
|
|
|
(Map.fromList [ (i,[]) | i <- imports])
|
|
|
|
dependencies
|
|
|
|
|
|
|
|
(graph, importFromVertex, vertexFromImport) = Graph.graphFromEdges
|
|
|
|
[(node, node, neighbours) | (node, neighbours) <- Map.assocs adjacencyLists]
|
|
|
|
|
|
|
|
-- compute the reverse dependencies, i.e. the imports reachable in the transposed graph
|
|
|
|
reachableImports import_ =
|
|
|
|
map (\(i,_,_) -> i) . map importFromVertex . concat $
|
|
|
|
do vertex <- vertexFromImport import_
|
|
|
|
return (Graph.reachable graph vertex)
|
|
|
|
|
2019-07-17 17:20:48 +02:00
|
|
|
codeImport = Dhall.chainedChangeMode Dhall.Code chained
|
|
|
|
textImport = Dhall.chainedChangeMode Dhall.RawText chained
|
2019-07-08 12:55:15 +02:00
|
|
|
invalidImports = Set.fromList $ codeImport : reachableImports codeImport
|
|
|
|
++ textImport : reachableImports textImport
|
|
|
|
|
|
|
|
dependencies' = filter (\(Dhall.Depends parent child) -> Set.notMember parent invalidImports
|
|
|
|
&& Set.notMember child invalidImports) dependencies
|
2019-07-01 19:30:32 +02:00
|
|
|
|
|
|
|
-- | A Dhall error. Covers parsing, resolving of imports, typechecking and
|
|
|
|
-- normalisation.
|
|
|
|
data DhallError = ErrorInternal SomeException
|
|
|
|
| ErrorImportSourced (Dhall.SourcedException Dhall.MissingImports)
|
2019-10-14 07:22:39 +02:00
|
|
|
| ErrorTypecheck (Dhall.TypeError Src Void)
|
2019-07-01 19:30:32 +02:00
|
|
|
| ErrorParse Dhall.ParseError
|
|
|
|
|
|
|
|
-- | Parse a Dhall expression.
|
|
|
|
parse :: Text -> Either DhallError (Expr Src Dhall.Import)
|
|
|
|
parse = fmap snd . parseWithHeader
|
|
|
|
|
|
|
|
-- | Parse a Dhall expression along with its "header", i.e. whitespace and
|
|
|
|
-- comments prefixing the actual code.
|
2019-10-22 19:45:08 +02:00
|
|
|
parseWithHeader :: Text -> Either DhallError (Dhall.Header, Expr Src Dhall.Import)
|
2019-07-01 19:30:32 +02:00
|
|
|
parseWithHeader = first ErrorParse . Dhall.exprAndHeaderFromText ""
|
|
|
|
|
|
|
|
-- | Resolve all imports in an expression.
|
|
|
|
load :: FileIdentifier -> Expr Src Dhall.Import -> Cache ->
|
2019-10-14 07:22:39 +02:00
|
|
|
IO (Either DhallError (Cache, Expr Src Void))
|
2019-07-17 17:20:48 +02:00
|
|
|
load (FileIdentifier chained) expr (Cache graph cache) = do
|
2019-07-01 19:30:32 +02:00
|
|
|
let emptyStatus = Dhall.emptyStatus ""
|
2019-07-08 12:55:15 +02:00
|
|
|
status = -- reuse cache and import graph
|
2019-07-01 19:30:32 +02:00
|
|
|
set Dhall.cache cache .
|
2019-07-08 12:55:15 +02:00
|
|
|
set Dhall.graph graph .
|
2019-07-01 19:30:32 +02:00
|
|
|
-- set "root import"
|
2019-07-17 17:20:48 +02:00
|
|
|
set Dhall.stack (chained :| [])
|
2019-07-01 19:30:32 +02:00
|
|
|
$ emptyStatus
|
|
|
|
(do (expr', status') <- runStateT (Dhall.loadWith expr) status
|
2019-07-08 12:55:15 +02:00
|
|
|
let cache' = view Dhall.cache status'
|
|
|
|
graph' = view Dhall.graph status'
|
|
|
|
return . Right $ (Cache graph' cache', expr'))
|
2019-07-01 19:30:32 +02:00
|
|
|
`catch` (\e -> return . Left $ ErrorImportSourced e)
|
|
|
|
`catch` (\e -> return . Left $ ErrorInternal e)
|
|
|
|
|
|
|
|
-- | Typecheck a fully resolved expression. Returns a certification that the
|
|
|
|
-- input was well-typed along with its (well-typed) type.
|
2019-10-14 07:22:39 +02:00
|
|
|
typecheck :: Expr Src Void -> Either DhallError (WellTyped, WellTyped)
|
2019-07-01 19:30:32 +02:00
|
|
|
typecheck expr = case Dhall.typeOf expr of
|
|
|
|
Left err -> Left $ ErrorTypecheck err
|
|
|
|
Right typ -> Right (WellTyped expr, WellTyped typ)
|
|
|
|
|
|
|
|
-- | Normalise a well-typed expression.
|
|
|
|
normalize :: WellTyped -> Normal
|
|
|
|
normalize (WellTyped expr) = Normal $ Dhall.normalize expr
|
2019-07-19 19:24:11 +02:00
|
|
|
|
|
|
|
-- | 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 expr) =
|
2019-11-01 04:05:22 +01:00
|
|
|
Dhall.hashExpressionToCode (Dhall.denote alphaNormal)
|
2019-07-19 19:24:11 +02:00
|
|
|
where alphaNormal = Dhall.alphaNormalize expr
|