Alternative Imports (#473)

This implements dhall-lang/dhall-lang#172, by adding "alternative imports", as detailed in dhall-lang/dhall-lang#163. We add: - a `?` operator for specifying alternatives for Imports that fail to resolve - a `missing` keyword for impossible imports (identity for the above operator) Also adds tests for all of the above.
2018-06-28 19:00:00 +03:00 · 2018-06-28 19:00:00 +03:00 · 5416269d5f
commit 5416269d5f
parent dba035e220
17 changed files with 267 additions and 20 deletions
--- a/dhall.cabal
+++ b/dhall.cabal
@ -152,6 +152,7 @@ Extra-Source-Files:
    tests/tutorial/*.dhall
    tests/typecheck/*.dhall
    tests/typecheck/examples/Monoid/*.dhall
+    tests/import/*.dhall
    benchmark/examples/*.dhall
    benchmark/deep-nested-large-record/*.dhall

@ -248,6 +249,7 @@ Test-Suite tasty
    GHC-Options: -Wall
    Other-Modules:
        Format
+        Import
        Normalization
        Parser
        Regression
--- a/src/Dhall/Core.hs
+++ b/src/Dhall/Core.hs
@ -163,6 +163,7 @@ data ImportType
    -- ^ URL of remote resource and optional headers stored in an import
    | Env  Text
    -- ^ Environment variable
+    | Missing
    deriving (Eq, Ord, Show)

 instance Semigroup ImportType where
@ -188,6 +189,8 @@ instance Pretty ImportType where

    pretty (Env env) = "env:" <> Pretty.pretty env

+    pretty Missing = "missing"
+
 -- | How to interpret the import's contents (i.e. as Dhall code or raw text)
 data ImportMode = Code | RawText deriving (Eq, Ord, Show)

@ -401,6 +404,8 @@ data Expr s a
    | Project (Expr s a) (Set Text)
    -- | > Note s x                                 ~  e
    | Note s (Expr s a)
+    -- | > ImportAlt                                ~  e1 ? e2
+    | ImportAlt (Expr s a) (Expr s a)
    -- | > Embed import                             ~  import
    | Embed a
    deriving (Functor, Foldable, Traversable, Show, Eq, Data)
@ -474,6 +479,7 @@ instance Monad (Expr s) where
    Field a b            >>= k = Field (a >>= k) b
    Project a b          >>= k = Project (a >>= k) b
    Note a b             >>= k = Note a (b >>= k)
+    ImportAlt a b        >>= k = ImportAlt (a >>= k) (b >>= k)
    Embed a              >>= k = k a

 instance Bifunctor Expr where
@ -538,6 +544,7 @@ instance Bifunctor Expr where
    first k (Field a b           ) = Field (first k a) b
    first k (Project a b         ) = Project (first k a) b
    first k (Note a b            ) = Note (k a) (first k b)
+    first k (ImportAlt a b       ) = ImportAlt (first k a) (first k b)
    first _ (Embed a             ) = Embed a

    second = fmap
@ -794,6 +801,10 @@ shift d v (Project a b) = Project a' b
 shift d v (Note a b) = Note a b'
  where
    b' = shift d v b
+shift d v (ImportAlt a b) = ImportAlt a' b'
+  where
+    a' = shift d v a
+    b' = shift d v b
 -- The Dhall compiler enforces that all embedded values are closed expressions
 -- and `shift` does nothing to a closed expression
 shift _ _ (Embed p) = Embed p
@ -942,6 +953,10 @@ subst x e (Project a b) = Project a' b
 subst x e (Note a b) = Note a b'
  where
    b' = subst x e b
+subst x e (ImportAlt a b) = ImportAlt a' b'
+  where
+    a' = subst x e a
+    b' = subst x e b
 -- The Dhall compiler enforces that all embedded values are closed expressions
 -- and `subst` does nothing to a closed expression
 subst _ _ (Embed p) = Embed p
@ -1207,6 +1222,11 @@ alphaNormalize (Note s e₀) =
    Note s e₁
  where
    e₁ = alphaNormalize e₀
+alphaNormalize (ImportAlt l₀ r₀) =
+    ImportAlt l₁ r₁
+  where
+    l₁ = alphaNormalize l₀
+    r₁ = alphaNormalize r₀
 alphaNormalize (Embed a) =
    Embed a

@ -1307,6 +1327,7 @@ denote (Merge a b c         ) = Merge (denote a) (denote b) (fmap denote c)
 denote (Constructors a      ) = Constructors (denote a)
 denote (Field a b           ) = Field (denote a) b
 denote (Project a b         ) = Project (denote a) b
+denote (ImportAlt a b       ) = ImportAlt (denote a) (denote b)
 denote (Embed a             ) = Embed a

 {-| Reduce an expression to its normal form, performing beta reduction and applying
@ -1677,6 +1698,7 @@ normalizeWith ctx e0 = loop (denote e0)
                    return (x, v)
            r' -> Project r' xs
    Note _ e' -> loop e'
+    ImportAlt l _r -> loop l
    Embed a -> Embed a

 {-| Returns `True` if two expressions are α-equivalent and β-equivalent and
@ -1890,6 +1912,7 @@ isNormalized e = case denote e of
                    else True
            _ -> True
    Note _ e' -> isNormalized e'
+    ImportAlt l _r -> isNormalized l
    Embed _ -> True

 {-| Detect if the given variable is free within the given expression
--- a/src/Dhall/Import.hs
+++ b/src/Dhall/Import.hs
@ -113,12 +113,12 @@ module Dhall.Import (
    , PrettyHttpException(..)
    , MissingFile(..)
    , MissingEnvironmentVariable(..)
+    , MissingImports(..)
    ) where

 import Control.Applicative (empty)
-import Control.Exception (Exception, SomeException, throwIO)
-import Control.Monad (join)
-import Control.Monad.Catch (throwM, MonadCatch(catch))
+import Control.Exception (Exception, SomeException, throwIO, toException)
+import Control.Monad.Catch (throwM, MonadCatch(catch), catches, Handler(..))
 import Control.Monad.IO.Class (MonadIO(..))
 import Control.Monad.Trans.State.Strict (StateT)
 import Crypto.Hash (SHA256)
@ -269,6 +269,28 @@ instance Show MissingEnvironmentVariable where
        <>  "\n"
        <>  "↳ " <> Text.unpack name

+-- | List of Exceptions we encounter while resolving Import Alternatives
+newtype MissingImports = MissingImports [SomeException]
+
+instance Exception MissingImports
+
+instance Show MissingImports where
+    show (MissingImports []) =
+            "\n"
+        <>  "\ESC[1;31mError\ESC[0m: No valid imports"
+        <>  "\n"
+    show (MissingImports [e]) = show e
+    show (MissingImports es) =
+            "\n"
+        <>  "\ESC[1;31mError\ESC[0m: Failed to resolve imports. Error list:"
+        <>  "\n"
+        <>  concatMap (\e -> "\n" <> show e <> "\n") es
+        <>  "\n"
+
+throwMissingImport :: (MonadCatch m, Exception e) => e -> m a
+throwMissingImport e = throwM (MissingImports [(toException e)])
+
+
 -- | Exception thrown when a HTTP url is imported but dhall was built without
 -- the @with-http@ Cabal flag.
 data CannotImportHTTPURL =
@ -336,6 +358,9 @@ instance Canonicalize ImportType where
    canonicalize (Env name) =
        Env name

+    canonicalize Missing =
+        Missing
+
 instance Canonicalize ImportHashed where
    canonicalize (ImportHashed hash importType) =
        ImportHashed hash (canonicalize importType)
@ -429,7 +454,7 @@ exprFromImport (Import {..}) = do

            if exists
                then return ()
-                else throwIO (MissingFile path)
+                else throwMissingImport (MissingFile path)

            text <- Data.Text.IO.readFile path

@ -487,7 +512,10 @@ exprFromImport (Import {..}) = do
            x <- System.Environment.lookupEnv (Text.unpack env)
            case x of
                Just string -> return (Text.unpack env, Text.pack string)
-                Nothing     -> throwIO (MissingEnvironmentVariable env)
+                Nothing     -> throwMissingImport (MissingEnvironmentVariable env)
+
+        Missing -> liftIO $ do
+            throwM (MissingImports [])

    case importMode of
        Code -> do
@ -537,39 +565,61 @@ loadStaticWith
    -> Dhall.Core.Normalizer X
    -> Expr Src Import
    -> StateT Status m (Expr Src X)
-loadStaticWith from_import ctx n (Embed import_) = do
+loadStaticWith from_import ctx n expr₀ = case expr₀ of
+  Embed import_ -> do
    imports <- zoom stack State.get

-    let local (Import (ImportHashed _ (URL   {})) _) = False
-        local (Import (ImportHashed _ (Local {})) _) = True
-        local (Import (ImportHashed _ (Env   {})) _) = True
+    let local (Import (ImportHashed _ (URL     {})) _) = False
+        local (Import (ImportHashed _ (Local   {})) _) = True
+        local (Import (ImportHashed _ (Env     {})) _) = True
+        local (Import (ImportHashed _ (Missing {})) _) = True

    let parent = canonicalizeImport imports
    let here   = canonicalizeImport (import_:imports)

    if local here && not (local parent)
-        then throwM (Imported imports (ReferentiallyOpaque import_))
+        then throwMissingImport (Imported imports (ReferentiallyOpaque import_))
        else return ()

    expr <- if here `elem` canonicalizeAll imports
-        then throwM (Imported imports (Cycle import_))
+        then throwMissingImport (Imported imports (Cycle import_))
        else do
            m <- zoom cache State.get
            case Map.lookup here m of
                Just expr -> return expr
                Nothing   -> do
-                    let handler
-                            :: MonadCatch m
+                    -- Here we have to match and unwrap the @MissingImports@
+                    -- in a separate handler, otherwise we'd have it wrapped
+                    -- in another @Imported@ when parsing a @missing@, because
+                    -- we are representing it with an empty exception list
+                    -- (which would not be empty if this would happen).
+                    -- TODO: restructure the Exception hierarchy to prevent
+                    -- this nesting from happening in the first place.
+                    let handler₀
+                            :: (MonadCatch m)
+                            => MissingImports
+                            -> StateT Status m (Expr Src Import)
+                        handler₀ e@(MissingImports []) = throwM e
+                        handler₀ (MissingImports [e]) =
+                          throwMissingImport (Imported (import_:imports) e)
+                        handler₀ (MissingImports es) = throwM
+                          (MissingImports
+                           (fmap
+                             (\e -> (toException (Imported (import_:imports) e)))
+                             es))
+                        handler₁
+                            :: (MonadCatch m)
                            => SomeException
                            -> StateT Status m (Expr Src Import)
-                        handler e = throwM (Imported (import_:imports) e)
+                        handler₁ e =
+                          throwMissingImport (Imported (import_:imports) e)

                    -- This loads a \"dynamic\" expression (i.e. an expression
                    -- that might still contain imports)
                    let loadDynamic =
                            from_import (canonicalizeImport (import_:imports))

-                    expr' <- loadDynamic `catch` handler
+                    expr' <- loadDynamic `catches` [ Handler handler₀, Handler handler₁ ]

                    let imports' = import_:imports
                    zoom stack (State.put imports')
@ -599,12 +649,80 @@ loadStaticWith from_import ctx n (Embed import_) = do
            let actualHash = hashExpression expr
            if expectedHash == actualHash
                then return ()
-                else throwM (Imported (import_:imports) (HashMismatch {..}))
+                else throwMissingImport (Imported (import_:imports) (HashMismatch {..}))

    return expr
-loadStaticWith from_import ctx n expr = fmap join (traverse process expr)
+  ImportAlt a b -> loop a `catch` handler₀
+    where
+      handler₀ (MissingImports es₀) =
+        loop b `catch` handler₁
+        where
+          handler₁ (MissingImports es₁) =
+            throwM (MissingImports (es₀ ++ es₁))
+  Const a              -> pure (Const a)
+  Var a                -> pure (Var a)
+  Lam a b c            -> Lam <$> pure a <*> loop b <*> loop c
+  Pi a b c             -> Pi <$> pure a <*> loop b <*> loop c
+  App a b              -> App <$> loop a <*> loop b
+  Let a b c d          -> Let <$> pure a <*> mapM loop b <*> loop c <*> loop d
+  Annot a b            -> Annot <$> loop a <*> loop b
+  Bool                 -> pure Bool
+  BoolLit a            -> pure (BoolLit a)
+  BoolAnd a b          -> BoolAnd <$> loop a <*> loop b
+  BoolOr a b           -> BoolOr <$> loop a <*> loop b
+  BoolEQ a b           -> BoolEQ <$> loop a <*> loop b
+  BoolNE a b           -> BoolNE <$> loop a <*> loop b
+  BoolIf a b c         -> BoolIf <$> loop a <*> loop b <*> loop c
+  Natural              -> pure Natural
+  NaturalLit a         -> pure (NaturalLit a)
+  NaturalFold          -> pure NaturalFold
+  NaturalBuild         -> pure NaturalBuild
+  NaturalIsZero        -> pure NaturalIsZero
+  NaturalEven          -> pure NaturalEven
+  NaturalOdd           -> pure NaturalOdd
+  NaturalToInteger     -> pure NaturalToInteger
+  NaturalShow          -> pure NaturalShow
+  NaturalPlus a b      -> NaturalPlus <$> loop a <*> loop b
+  NaturalTimes a b     -> NaturalTimes <$> loop a <*> loop b
+  Integer              -> pure Integer
+  IntegerLit a         -> pure (IntegerLit a)
+  IntegerShow          -> pure IntegerShow
+  IntegerToDouble      -> pure IntegerToDouble
+  Double               -> pure Double
+  DoubleLit a          -> pure (DoubleLit a)
+  DoubleShow           -> pure DoubleShow
+  Text                 -> pure Text
+  TextLit (Chunks a b) -> fmap TextLit (Chunks <$> mapM (mapM loop) a <*> pure b)
+  TextAppend a b       -> TextAppend <$> loop a <*> loop b
+  List                 -> pure List
+  ListLit a b          -> ListLit <$> mapM loop a <*> mapM loop b
+  ListAppend a b       -> ListAppend <$> loop a <*> loop b
+  ListBuild            -> pure ListBuild
+  ListFold             -> pure ListFold
+  ListLength           -> pure ListLength
+  ListHead             -> pure ListHead
+  ListLast             -> pure ListLast
+  ListIndexed          -> pure ListIndexed
+  ListReverse          -> pure ListReverse
+  Optional             -> pure Optional
+  OptionalLit a b      -> OptionalLit <$> loop a <*> mapM loop b
+  OptionalFold         -> pure OptionalFold
+  OptionalBuild        -> pure OptionalBuild
+  Record a             -> Record <$> mapM loop a
+  RecordLit a          -> RecordLit <$> mapM loop a
+  Union a              -> Union <$> mapM loop a
+  UnionLit a b c       -> UnionLit <$> pure a <*> loop b <*> mapM loop c
+  Combine a b          -> Combine <$> loop a <*> loop b
+  CombineTypes a b     -> CombineTypes <$> loop a <*> loop b
+  Prefer a b           -> Prefer <$> loop a <*> loop b
+  Merge a b c          -> Merge <$> loop a <*> loop b <*> mapM loop c
+  Constructors a       -> Constructors <$> loop a
+  Field a b            -> Field <$> loop a <*> pure b
+  Project a b          -> Project <$> loop a <*> pure b
+  Note a b             -> Note <$> pure a <*> loop b
  where
-    process import_ = loadStaticWith from_import ctx n (Embed import_)
+    loop = loadStaticWith from_import ctx n
+

 -- | Resolve all imports within an expression
 load :: Expr Src Import -> IO (Expr Src X)
--- a/src/Dhall/Lint.hs
+++ b/src/Dhall/Lint.hs
@ -213,5 +213,10 @@ lint expression = loop (Dhall.Core.denote expression)
        a' = loop a
    loop (Note a _) =
        absurd a
+    loop (ImportAlt a b) =
+        ImportAlt a' b'
+      where
+        a' = loop a
+        b' = loop b
    loop (Embed a) =
        Embed a
--- a/src/Dhall/Parser/Expression.hs
+++ b/src/Dhall/Parser/Expression.hs
@ -157,7 +157,7 @@ nonEmptyOptional embedded = do
    return (OptionalLit b (pure a))

 operatorExpression :: Parser a -> Parser (Expr Src a)
-operatorExpression = orExpression
+operatorExpression = importAltExpression

 makeOperatorExpression
    :: (Parser a -> Parser (Expr Src a))
@ -171,6 +171,10 @@ makeOperatorExpression subExpression operatorParser operator embedded =
        b <- many (do operatorParser; subExpression embedded)
        return (foldr1 operator (a:b)) )

+importAltExpression :: Parser a -> Parser (Expr Src a)
+importAltExpression =
+    makeOperatorExpression orExpression _importAlt ImportAlt
+
 orExpression :: Parser a -> Parser (Expr Src a)
 orExpression =
    makeOperatorExpression plusExpression _or BoolOr
@ -760,8 +764,13 @@ http = do
        (importHashed_ <|> (_openParens *> importHashed_ <* _closeParens)) )
    return (URL prefix path suffix headers)

+missing :: Parser ImportType
+missing = do
+  _missing
+  return Missing
+
 importType_ :: Parser ImportType
-importType_ = choice [ local, http, env ]
+importType_ = choice [ local, http, env, missing ]

 importHashed_ :: Parser ImportHashed
 importHashed_ = do
--- a/src/Dhall/Parser/Token.hs
+++ b/src/Dhall/Parser/Token.hs
@ -575,6 +575,12 @@ _colon = reserved ":"
 _at :: Parser ()
 _at = reserved "@"

+_missing :: Parser ()
+_missing = reserved "missing"
+
+_importAlt :: Parser ()
+_importAlt = reserved "?"
+
 _combine :: Parser ()
 _combine = do
    void (Text.Parser.Char.char '∧' <?> "\"∧\"") <|> void (Text.Parser.Char.text "/\\")
--- a/src/Dhall/TypeCheck.hs
+++ b/src/Dhall/TypeCheck.hs
@ -752,6 +752,8 @@ typeWithA tpa = loop
        Left (TypeError ctx' (Note s' e'') m) -> Left (TypeError ctx' (Note s' e'') m)
        Left (TypeError ctx'          e''  m) -> Left (TypeError ctx' (Note s  e'') m)
        Right r                               -> Right r
+    loop ctx   (ImportAlt l _r  ) =
+       fmap Dhall.Core.normalize (loop ctx l)
    loop _     (Embed p         ) = Right $ tpa p

 {-| `typeOf` is the same as `typeWith` with an empty context, meaning that the
--- a/tests/Import.hs
+++ b/tests/Import.hs
@ -0,0 +1,70 @@
+{-# LANGUAGE OverloadedStrings #-}
+
+module Import where
+
+import Data.Text (Text)
+import Test.Tasty (TestTree)
+import Dhall.Import (MissingImports(..))
+import Control.Exception (catch, throwIO)
+import Data.Monoid ((<>))
+
+import qualified Data.Text
+import qualified Data.Text.IO
+import qualified Dhall.Parser
+import qualified Dhall.Import
+import qualified Test.Tasty
+import qualified Test.Tasty.HUnit
+
+importTests :: TestTree
+importTests =
+    Test.Tasty.testGroup "import tests"
+        [ Test.Tasty.testGroup "import alternatives"
+            [ shouldFail
+                3
+                "alternative of several unset env variables"
+                "./tests/import/alternativeEnv.dhall"
+            , shouldFail
+                1
+                "alternative of env variable and missing"
+                "./tests/import/alternativeEnvMissing.dhall"
+            , shouldFail
+                0
+                "just missing"
+                "./tests/import/missing.dhall"
+            , shouldNotFail
+                "alternative of env variable, missing, and a Natural"
+                "./tests/import/alternativeEnvNatural.dhall"
+            , shouldNotFail
+                "alternative of env variable and a Natural"
+                "./tests/import/alternativeEnvSimple.dhall"
+            , shouldNotFail
+                "alternative of a Natural and missing"
+                "./tests/import/alternativeNatural.dhall"
+            ]
+        ]
+
+shouldNotFail :: Text -> FilePath -> TestTree
+shouldNotFail name path = Test.Tasty.HUnit.testCase (Data.Text.unpack name) (do
+    text <- Data.Text.IO.readFile path
+    actualExpr <- case Dhall.Parser.exprFromText mempty text of
+                     Left  err  -> throwIO err
+                     Right expr -> return expr
+    _ <- Dhall.Import.load actualExpr
+    return ())
+
+shouldFail :: Int -> Text -> FilePath -> TestTree
+shouldFail failures name path = Test.Tasty.HUnit.testCase (Data.Text.unpack name) (do
+    text <- Data.Text.IO.readFile path
+    actualExpr <- case Dhall.Parser.exprFromText mempty text of
+                     Left  err  -> throwIO err
+                     Right expr -> return expr
+    catch
+      (do
+          _ <- Dhall.Import.load actualExpr
+          fail "Import should have failed, but it succeeds")
+      (\(MissingImports es) -> case length es == failures of
+                                True -> pure ()
+                                False -> fail ("Should have failed "
+                                               <> show failures
+                                               <> " times, but failed with: \n"
+                                               <> show es)) )
--- a/tests/Parser.hs
+++ b/tests/Parser.hs
@ -124,6 +124,9 @@ parserTests =
            , shouldParse
                "builtins"
                "./tests/parser/builtins.dhall"
+            , shouldParse
+                "import alternatives"
+                "./tests/parser/importAlt.dhall"
            , shouldParse
                "large expression"
                "./tests/parser/largeExpression.dhall"
--- a/tests/Tests.hs
+++ b/tests/Tests.hs
@ -6,6 +6,7 @@ import Regression (regressionTests)
 import Tutorial (tutorialTests)
 import TypeCheck (typecheckTests)
 import Format (formatTests)
+import Import (importTests)
 import Test.Tasty

 allTests :: TestTree
@ -17,6 +18,7 @@ allTests =
        , tutorialTests
        , formatTests
        , typecheckTests
+        , importTests
        ]

 main :: IO ()
--- a/tests/import/alternativeEnv.dhall
+++ b/tests/import/alternativeEnv.dhall
@ -0,0 +1 @@
+env:UNSET1 as Text ? env:UNSET2 ? missing ? env:UNSET3
--- a/tests/import/alternativeEnvMissing.dhall
+++ b/tests/import/alternativeEnvMissing.dhall
@ -0,0 +1 @@
+env:UNSET ? missing
--- a/tests/import/alternativeEnvNatural.dhall
+++ b/tests/import/alternativeEnvNatural.dhall
@ -0,0 +1 @@
+env:UNSET1 as Text ? env:UNSET2 ? missing ? env:UNSET3 ? 2
--- a/tests/import/alternativeEnvSimple.dhall
+++ b/tests/import/alternativeEnvSimple.dhall
@ -0,0 +1 @@
+env:UNSET ? 3
--- a/tests/import/alternativeNatural.dhall
+++ b/tests/import/alternativeNatural.dhall
@ -0,0 +1 @@
+4 ? missing
--- a/tests/import/missing.dhall
+++ b/tests/import/missing.dhall
@ -0,0 +1 @@
+missing
--- a/tests/parser/importAlt.dhall
+++ b/tests/parser/importAlt.dhall
@ -0,0 +1 @@
+env:UNSET1 as Text ? env:UNSET2 ? missing ? env:UNSET3 ? 2
				`@ -0,0 +1 @@`
				`env:UNSET1 as Text ? env:UNSET2 ? missing ? env:UNSET3`