{-# LANGUAGE CPP #-} {-# LANGUAGE DeriveDataTypeable #-} {-# LANGUAGE OverloadedStrings #-} {-# OPTIONS_GHC -Wall #-} {-| Morte lets you import external expressions located either in local files or hosted on network endpoints. To import a local file as an expression, just insert the path to the file, prepending a @./@ if the path is relative to the current directory. For example, suppose we had the following three local files: > -- id > \(a : *) -> \(x : a) -> x > -- Bool > forall (Bool : *) -> forall (True : Bool) -> forall (False : Bool) -> Bool > -- True > \(Bool : *) -> \(True : Bool) -> \(False : Bool) -> True You could then reference them within a Morte expression using this syntax: > ./id ./Bool ./True ... which would embed their expressions directly within the syntax tree: > -- ... expands out to: > (\(a : *) -> \(x : a) -> x) > (forall (Bool : *) -> forall (True : Bool) -> forall (False : Bool) -> True) > (\(Bool : *) -> \(True : Bool) -> \(False : Bool) -> True) ... and which normalizes to: > λ(Bool : *) → λ(True : Bool) → λ(False : Bool) → True Imported expressions may contain imports of their own, too, which will continue to be resolved. However, Morte will prevent cyclic imports. For example, if you had these two files: > -- foo > ./bar > -- bar > ./foo ... Morte would throw the following exception if you tried to import @foo@: > morte: > ⤷ ./foo > ⤷ ./bar > Cyclic import: ./foo You can also import expressions hosted on network endpoints. Just use the URL > http://host[:port]/path The compiler expects the downloaded expressions to be in the same format as local files, specifically UTF8-encoded source code text. For example, if our @id@ expression were hosted at @http://example.com/id@, then we would embed the expression within our code using: > http://example.com/id You can also reuse directory names as expressions. If you provide a path to a local or remote directory then the compiler will look for a file named @\@@ within that directory and use that file to represent the directory. -} module Morte.Import ( -- * Import load , Cycle(..) , ReferentiallyOpaque(..) , Imported(..) ) where import Control.Exception (Exception, IOException, catch, onException, throwIO) import Control.Monad (join) import Control.Monad.IO.Class (MonadIO(..)) import Control.Monad.Trans.State.Strict (StateT) import Data.Map.Strict (Map) import Data.Monoid ((<>)) import Data.Text.Lazy (Text) import Data.Text.Lazy.Builder (Builder) #if MIN_VERSION_base(4,8,0) #else import Data.Traversable (traverse) #endif import Data.Typeable (Typeable) import Filesystem.Path ((), FilePath) import Filesystem as Filesystem import Formatting.Buildable (build) import Lens.Micro (Lens') import Lens.Micro.Mtl (zoom) import Morte.Core (Expr, Path(..), X(..)) import Network.HTTP.Client (Manager) import Prelude hiding (FilePath) import qualified Control.Monad.Trans.State.Strict as State import qualified Data.Foldable as Foldable import qualified Data.List as List import qualified Data.Map.Strict as Map import qualified Data.Text.Lazy as Text import qualified Data.Text.Lazy.Builder as Builder import qualified Data.Text.Lazy.Encoding as Text import qualified Morte.Core as Morte import qualified Morte.Parser as Morte import qualified Network.HTTP.Client as HTTP import qualified Network.HTTP.Client.TLS as HTTP import qualified Filesystem.Path.CurrentOS as Filesystem builderToString :: Builder -> String builderToString = Text.unpack . Builder.toLazyText -- | An import failed because of a cycle in the import graph newtype Cycle = Cycle { cyclicImport :: Path -- ^ The offending cyclic import } deriving (Typeable) instance Exception Cycle instance Show Cycle where show (Cycle path) = "Cyclic import: " ++ builderToString (build path) {-| Morte tries to ensure that all expressions hosted on network endpoints are weakly referentially transparent, meaning roughly that any two clients will compile the exact same result given the same URL. To be precise, a strong interpretaton of referential transparency means that if you compiled a URL you could replace the expression hosted at that URL with the compiled result. Let's term this \"static linking\". Morte (very intentionally) does not satisfy this stronger interpretation of referential transparency since \"statically linking\" an expression (i.e. permanently resolving all imports) means that the expression will no longer update if its dependencies change. In general, either interpretation of referential transparency is not enforceable in a networked context since one can easily violate referential transparency with a custom DNS, but Morte can still try to guard against common unintentional violations. To do this, Morte enforces that a non-local import may not reference a local import. Local imports are defined as: * A file * A URL with a host of @localhost@ or @127.0.0.1@ All other imports are defined to be non-local -} newtype ReferentiallyOpaque = ReferentiallyOpaque { opaqueImport :: Path -- ^ The offending opaque import } deriving (Typeable) instance Exception ReferentiallyOpaque instance Show ReferentiallyOpaque where show (ReferentiallyOpaque path) = "Referentially opaque import: " ++ builderToString (build path) -- | Extend another exception with the current import stack data Imported e = Imported { importStack :: [Path] -- ^ Imports resolved so far, in reverse order , nested :: e -- ^ The nested exception } deriving (Typeable) instance Exception e => Exception (Imported e) instance Show e => Show (Imported e) where show (Imported paths e) = "\n" ++ unlines (map (\path -> "⤷ " ++ builderToString (build path)) paths') ++ show e where -- Canonicalize all paths paths' = drop 1 (reverse (canonicalizeAll paths)) data Status = Status { _stack :: [Path] , _cache :: Map Path (Expr X) , _manager :: Maybe Manager } canonicalizeAll :: [Path] -> [Path] canonicalizeAll = map canonicalize . List.tails stack :: Lens' Status [Path] stack k s = fmap (\x -> s { _stack = x }) (k (_stack s)) cache :: Lens' Status (Map Path (Expr X)) cache k s = fmap (\x -> s { _cache = x }) (k (_cache s)) manager :: Lens' Status (Maybe Manager) manager k s = fmap (\x -> s { _manager = x }) (k (_manager s)) needManager :: StateT Status IO Manager needManager = do x <- zoom manager State.get case x of Just m -> return m Nothing -> do let settings = HTTP.tlsManagerSettings { HTTP.managerResponseTimeout = HTTP.responseTimeoutMicro 1000000 } m <- liftIO (HTTP.newManager settings) zoom manager (State.put (Just m)) return m {-| This function computes the current path by taking the last absolute path (either an absolute `FilePath` or `URL`) and combining it with all following relative paths For example, if the file `./foo/bar` imports `./baz`, that will resolve to `./foo/baz`. Relative imports are relative to a file's parent directory. This also works for URLs, too. This code is full of all sorts of edge cases so it wouldn't surprise me at all if you find something broken in here. Most of the ugliness is due to: * Handling paths ending with @/\@@ by stripping the @/\@@ suffix if and only if you navigate to any downstream relative paths * Removing spurious @.@s and @..@s from the path Also, there are way too many `reverse`s in the URL-handling cod For now I don't mind, but if were to really do this correctly we'd store the URLs as `Text` for O(1) access to the end of the string. The only reason we use `String` at all is for consistency with the @http-client@ library. -} canonicalize :: [Path] -> Path canonicalize [] = File "." canonicalize (File file0:paths0) = if Filesystem.relative file0 then go file0 paths0 else File (clean file0) where go currPath [] = File (clean currPath) go currPath (URL url0:_ ) = combine prefix suffix where prefix = parentURL (removeAtFromURL url0) suffix = clean currPath -- `clean` will resolve internal @.@/@..@'s in @currPath@, but we still -- need to manually handle @.@/@..@'s at the beginning of the path combine url path = case Filesystem.stripPrefix ".." path of Just path' -> combine url' path' where url' = parentURL (removeAtFromURL url) Nothing -> case Filesystem.stripPrefix "." path of Just path' -> combine url path' Nothing -> -- This `last` is safe because the lexer constrains all -- URLs to be non-empty. I couldn't find a simple and safe -- equivalent in the `text` API case Text.last url of '/' -> URL (url <> path') _ -> URL (url <> "/" <> path') where path' = Text.fromStrict (case Filesystem.toText path of Left txt -> txt Right txt -> txt ) go currPath (File file:paths) = if Filesystem.relative file then go file' paths else File (clean file') where file' = Filesystem.parent (removeAtFromFile file) currPath canonicalize (URL path:_) = URL path parentURL :: Text -> Text parentURL = Text.dropWhileEnd (/= '/') removeAtFromURL:: Text -> Text removeAtFromURL url | Text.isSuffixOf "/@" url = Text.dropEnd 2 url | Text.isSuffixOf "/" url = Text.dropEnd 1 url | otherwise = url removeAtFromFile :: FilePath -> FilePath removeAtFromFile file = if Filesystem.filename file == "@" then Filesystem.parent file else file -- | Remove all @.@'s and @..@'s in the path clean :: FilePath -> FilePath clean = strip . Filesystem.collapse where strip p = case Filesystem.stripPrefix "." p of Nothing -> p Just p' -> p' {-| Load a `Path` as a \"dynamic\" expression (without resolving any imports) This also returns the true final path (i.e. explicit "/@" at the end for directories) -} loadDynamic :: Path -> StateT Status IO (Expr Path) loadDynamic p = do paths <- zoom stack State.get let readURL url = do request <- liftIO (HTTP.parseUrlThrow (Text.unpack url)) m <- needManager let httpLbs' = do HTTP.httpLbs request m `catch` (\e -> case e of HTTP.HttpExceptionRequest _ (HTTP.StatusCodeException _ _) -> do let request' = request { HTTP.path = HTTP.path request <> "/@" } -- If the fallback fails, reuse the original -- exception to avoid user confusion HTTP.httpLbs request' m `onException` throwIO (Imported paths e) _ -> throwIO (Imported paths e) ) response <- liftIO httpLbs' case Text.decodeUtf8' (HTTP.responseBody response) of Left err -> liftIO (throwIO (Imported paths err)) Right txt -> return txt let readFile' file = liftIO (do (do txt <- Filesystem.readTextFile file return (Text.fromStrict txt) ) `catch` (\e -> do -- Unfortunately, GHC throws an `InappropriateType` -- exception when trying to read a directory, but does not -- export the exception, so I must resort to a more -- heavy-handed `catch` let _ = e :: IOException -- If the fallback fails, reuse the original exception to -- avoid user confusion let file' = file "@" txt <- Filesystem.readTextFile file' `onException` throwIO (Imported paths e) return (Text.fromStrict txt) ) ) txt <- case canonicalize (p:paths) of File file -> readFile' file URL url -> readURL url let abort err = liftIO (throwIO (Imported (p:paths) err)) case Morte.exprFromText txt of Left err -> case canonicalize (p:paths) of URL url -> do -- Also try the fallback in case of a parse error, since the -- parse error might signify that this URL points to a directory -- list request <- liftIO (HTTP.parseUrlThrow (Text.unpack url)) let request' = request { HTTP.path = HTTP.path request <> "/@" } m <- needManager response <- liftIO (HTTP.httpLbs request' m `onException` abort err) case Text.decodeUtf8' (HTTP.responseBody response) of Left _ -> liftIO (abort err) Right txt' -> case Morte.exprFromText txt' of Left _ -> liftIO (abort err) Right expr -> return expr _ -> liftIO (abort err) Right expr -> return expr -- | Load a `Path` as a \"static\" expression (with all imports resolved) loadStatic :: Path -> StateT Status IO (Expr X) loadStatic path = do paths <- zoom stack State.get let local (URL url) = case HTTP.parseUrlThrow (Text.unpack url) of Nothing -> False Just request -> case HTTP.host request of "127.0.0.1" -> True "localhost" -> True _ -> False local (File _) = True let parent = canonicalize paths let here = canonicalize (path:paths) if local here && not (local parent) then liftIO (throwIO (Imported paths (ReferentiallyOpaque path))) else return () (expr, cached) <- if here `elem` canonicalizeAll paths then liftIO (throwIO (Imported paths (Cycle path))) else do m <- zoom cache State.get case Map.lookup here m of Just expr -> return (expr, True) Nothing -> do expr' <- loadDynamic path expr'' <- case traverse (\_ -> Nothing) expr' of -- No imports left Just expr -> do zoom cache (State.put $! Map.insert here expr m) return expr -- Some imports left, so recurse Nothing -> do let paths' = path:paths zoom stack (State.put paths') expr'' <- fmap join (traverse loadStatic expr') zoom stack (State.put paths) return expr'' return (expr'', False) -- Type-check expressions here for two separate reasons: -- -- * to verify that they are closed -- * to catch type errors as early in the import process as possible -- -- There is no need to check expressions that have been cached, since they -- have already been checked if cached then return () else case Morte.typeOf expr of Left err -> liftIO (throwIO (Imported (path:paths) err)) Right _ -> return () return expr {-| Resolve all imports within an expression By default the starting path is the current directory, but you can override the starting path with a file if you read in the expression from that file -} load :: Maybe Path -- ^ Starting path -> Expr Path -- ^ Expression to resolve -> IO (Expr X) load here expr = State.evalStateT (fmap join (traverse loadStatic expr)) status where status = Status (Foldable.toList here) Map.empty Nothing