diff --git a/dhall-nix/src/Dhall/Nix.hs b/dhall-nix/src/Dhall/Nix.hs index a803b1f69..80e98148a 100644 --- a/dhall-nix/src/Dhall/Nix.hs +++ b/dhall-nix/src/Dhall/Nix.hs @@ -3,6 +3,7 @@ {-# LANGUAGE OverloadedStrings #-} {-# LANGUAGE QuasiQuotes #-} {-# LANGUAGE RecordWildCards #-} +{-# LANGUAGE TemplateHaskell #-} {-# LANGUAGE TypeFamilies #-} {-# LANGUAGE ViewPatterns #-} @@ -93,24 +94,30 @@ module Dhall.Nix ( ) where import Control.Exception (Exception) -import Data.Fix (Fix (..)) -import Data.Foldable (toList) -import Data.Text (Text) -import Data.Traversable (for) -import Data.Typeable (Typeable) -import Data.Void (Void, absurd) +import Data.Fix (Fix (..)) +import Data.Foldable (toList) +import Data.List.NonEmpty (NonEmpty(..)) +import Data.Text (Text) +import Data.Traversable (for) +import Data.Typeable (Typeable) +import Data.Void (Void, absurd) +import Lens.Family (toListOf) +import Nix.Atoms (NAtom (..)) +import Nix (($//), ($==)) + import Dhall.Core ( Binding (..) , Chunks (..) , DhallDouble (..) , Expr (..) + , FieldSelection (..) , FunctionBinding (..) , MultiLet (..) , PreferAnnotation (..) , Var (..) + , WithComponent (..) ) -import Lens.Family (toListOf) -import Nix.Atoms (NAtom (..)) + import Nix.Expr ( Antiquoted (..) , Binding (..) @@ -670,8 +677,24 @@ dhallToNix e = return untranslatable loop (Equivalent _ _ _) = return untranslatable - loop a@With{} = - loop (Dhall.Core.desugarWith a) + loop (With a (WithLabel k :| []) b) = do + a' <- loop a + b' <- loop b + + return (a' $// Nix.attrsE [(k, b')]) + loop (With a (WithLabel k :| k' : ks) b) = do + a' <- loop a + b' <- loop (With (Field "_" (FieldSelection Nothing k Nothing)) (k' :| ks) (Dhall.Core.shift 1 "_" b)) + + return (Nix.letE "_" a' ("_" $// Nix.attrsE [(k, b')])) + loop (With a (WithQuestion :| []) b) = do + a' <- loop a + b' <- loop b + return (Nix.mkIf (a' $== Nix.mkNull) Nix.mkNull b') + loop (With a (WithQuestion :| k : ks) b) = do + a' <- loop a + b' <- loop (With "_" (k :| ks) (Dhall.Core.shift 1 "_" b)) + return (Nix.letE "_" a' (Nix.mkIf (a' $== Nix.mkNull) Nix.mkNull b')) loop (ImportAlt a _) = loop a loop (Note _ b) = loop b loop (Embed x) = absurd x diff --git a/dhall/src/Dhall/Binary.hs b/dhall/src/Dhall/Binary.hs index 4cbbb18e6..d9698fa57 100644 --- a/dhall/src/Dhall/Binary.hs +++ b/dhall/src/Dhall/Binary.hs @@ -47,6 +47,7 @@ import Dhall.Syntax , Scheme (..) , URL (..) , Var (..) + , WithComponent (..) ) import Data.Foldable (toList) @@ -559,7 +560,18 @@ decodeExpressionInternal decodeEmbed = go n <- Decoding.decodeListLen - ks₀ <- replicateDecoder n Decoding.decodeString + let decodeWithComponent = do + tokenType₂ <- Decoding.peekTokenType + case tokenType₂ of + TypeString -> do + fmap WithLabel Decoding.decodeString + _ -> do + m <- Decoding.decodeInt + + case m of + 0 -> return WithQuestion + _ -> die ("Unexpected integer encoding a with expression: " <> show n) + ks₀ <- replicateDecoder n decodeWithComponent ks₁ <- case NonEmpty.nonEmpty ks₀ of Nothing -> @@ -1017,8 +1029,11 @@ encodeExpressionInternal encodeEmbed = go encodeList4 (Encoding.encodeInt 29) (go l) - (encodeList (fmap Encoding.encodeString ks)) + (encodeList (fmap encodeWithComponent ks)) (go r) + where + encodeWithComponent WithQuestion = Encoding.encodeInt 0 + encodeWithComponent (WithLabel k ) = Encoding.encodeString k DateLiteral day -> encodeList4 diff --git a/dhall/src/Dhall/Core.hs b/dhall/src/Dhall/Core.hs index 744cad134..1d52884bf 100644 --- a/dhall/src/Dhall/Core.hs +++ b/dhall/src/Dhall/Core.hs @@ -31,6 +31,7 @@ module Dhall.Core ( , makeFunctionBinding , FieldSelection (..) , makeFieldSelection + , WithComponent (..) , Expr(..) -- * Normalization @@ -76,7 +77,6 @@ module Dhall.Core ( , Eval.textShow , censorExpression , censorText - , Syntax.desugarWith ) where import Control.Exception (Exception) @@ -92,8 +92,7 @@ import Prettyprinter (Pretty) import qualified Control.Exception import qualified Data.Text -import qualified Dhall.Eval as Eval -import qualified Dhall.Syntax as Syntax +import qualified Dhall.Eval as Eval -- | Pretty-print a value pretty :: Pretty a => a -> Text diff --git a/dhall/src/Dhall/Diff.hs b/dhall/src/Dhall/Diff.hs index 87ca78c71..06fe15aee 100644 --- a/dhall/src/Dhall/Diff.hs +++ b/dhall/src/Dhall/Diff.hs @@ -35,6 +35,7 @@ import Dhall.Syntax , FunctionBinding (..) , RecordField (..) , Var (..) + , WithComponent (..) ) import Numeric.Natural (Natural) import Prettyprinter (Doc, Pretty) @@ -1067,12 +1068,15 @@ diffWithExpression (With eL ksL vL) (With eR ksR vR) = ( format " " (diffImportExpression eL eR) <> "with " <> align - ( format " " (diffPath ksL ksR) + ( format " " (diffPath (fmap toText ksL) (fmap toText ksR)) <> "= " <> diffOperatorExpression vL vR ) ) where + toText WithQuestion = "?" + toText (WithLabel k ) = k + diffPath (kL :| []) (kR :| []) = diffLabel kL kR diffPath (kL₀ :| kL₁ : ksL') (kR₀ :| kR₁ : ksR') = diff --git a/dhall/src/Dhall/Eval.hs b/dhall/src/Dhall/Eval.hs index 7764bce4d..d082e9d00 100644 --- a/dhall/src/Dhall/Eval.hs +++ b/dhall/src/Dhall/Eval.hs @@ -69,6 +69,7 @@ import Dhall.Syntax , PreferAnnotation (..) , RecordField (..) , Var (..) + , WithComponent (..) ) import qualified Data.Char @@ -234,7 +235,7 @@ data Val a | VProject !(Val a) !(Either (Set Text) (Val a)) | VAssert !(Val a) | VEquivalent !(Val a) !(Val a) - | VWith !(Val a) (NonEmpty Text) !(Val a) + | VWith !(Val a) (NonEmpty WithComponent) !(Val a) | VEmbed a -- | For use with "Text.Show.Functions". @@ -417,9 +418,9 @@ vProjectByFields env t ks = t' -> VProject t' (Left ks) -vWith :: Val a -> NonEmpty Text -> Val a -> Val a -vWith (VRecordLit kvs) (k :| [] ) v = VRecordLit (Map.insert k v kvs) -vWith (VRecordLit kvs) (k₀ :| k₁ : ks) v = VRecordLit (Map.insert k₀ e₂ kvs) +vWith :: Val a -> NonEmpty WithComponent -> Val a -> Val a +vWith (VRecordLit kvs) (WithLabel k :| [] ) v = VRecordLit (Map.insert k v kvs) +vWith (VRecordLit kvs) (WithLabel k₀ :| k₁ : ks) v = VRecordLit (Map.insert k₀ e₂ kvs) where e₁ = case Map.lookup k₀ kvs of @@ -427,6 +428,9 @@ vWith (VRecordLit kvs) (k₀ :| k₁ : ks) v = VRecordLit (Map.insert k₀ e₂ Just e₁' -> e₁' e₂ = vWith e₁ (k₁ :| ks) v +vWith (VNone _T) (WithQuestion :| _ ) _ = VNone _T +vWith (VSome _) (WithQuestion :| [] ) v = VSome v +vWith (VSome t) (WithQuestion :| k₁ : ks) v = VSome (vWith t (k₁ :| ks) v) vWith e₀ ks v₀ = VWith e₀ ks v₀ eval :: forall a. Eq a => Environment a -> Expr Void a -> Val a diff --git a/dhall/src/Dhall/Normalize.hs b/dhall/src/Dhall/Normalize.hs index 2518f8707..60a4c2499 100644 --- a/dhall/src/Dhall/Normalize.hs +++ b/dhall/src/Dhall/Normalize.hs @@ -38,6 +38,7 @@ import Dhall.Syntax , FunctionBinding (..) , PreferAnnotation (..) , RecordField (..) + , WithComponent (..) , Var (..) ) @@ -698,9 +699,9 @@ normalizeWithM ctx e0 = loop (Syntax.denote e0) case e' of RecordLit kvs -> case ks of - k :| [] -> + WithLabel k :| [] -> return (RecordLit (Dhall.Map.insert k (Syntax.makeRecordField v') kvs)) - k₀ :| k₁ : ks' -> do + WithLabel k₀ :| k₁ : ks' -> do let e₁ = case Dhall.Map.lookup k₀ kvs of Nothing -> RecordLit mempty @@ -709,6 +710,23 @@ normalizeWithM ctx e0 = loop (Syntax.denote e0) e₂ <- loop (With e₁ (k₁ :| ks') v') return (RecordLit (Dhall.Map.insert k₀ (Syntax.makeRecordField e₂) kvs)) + WithQuestion :| _ -> do + return (With e' ks v') + Some t -> + case ks of + WithQuestion :| [] -> do + return (Some v') + WithQuestion :| k : ks' -> do + w <- loop (With t (k :| ks') v) + return (Some w) + WithLabel _ :| _ -> + return (With e' ks v') + App None _T -> + case ks of + WithQuestion :| _ -> + return (App None _T) + WithLabel _ :| _ -> + return (With e' ks v') _ -> return (With e' ks v') Note _ e' -> loop e' diff --git a/dhall/src/Dhall/Parser/Expression.hs b/dhall/src/Dhall/Parser/Expression.hs index 66165bd60..321d3d65b 100644 --- a/dhall/src/Dhall/Parser/Expression.hs +++ b/dhall/src/Dhall/Parser/Expression.hs @@ -388,7 +388,11 @@ parsers embedded = Parsers{..} bs <- some (do try (nonemptyWhitespace *> _with *> nonemptyWhitespace) - keys <- Combinators.NonEmpty.sepBy1 anyLabelOrSome (try (whitespace *> _dot) *> whitespace) + let withComponent = + fmap WithLabel anyLabelOrSome + <|> fmap (\_ -> WithQuestion) (text "?") + + keys <- Combinators.NonEmpty.sepBy1 withComponent (try (whitespace *> _dot) *> whitespace) whitespace diff --git a/dhall/src/Dhall/Pretty/Internal.hs b/dhall/src/Dhall/Pretty/Internal.hs index c0d12a936..5783ac9fe 100644 --- a/dhall/src/Dhall/Pretty/Internal.hs +++ b/dhall/src/Dhall/Pretty/Internal.hs @@ -513,7 +513,7 @@ escapeLabel :: Bool -> Text -> Text escapeLabel allowReserved l = case Text.uncons l of Just (h, t) - | headCharacter h && Text.all tailCharacter t && (notReservedIdentifier || (allowReserved && someOrNotLanguageKeyword)) + | headCharacter h && Text.all tailCharacter t && (notReservedIdentifier || (allowReserved && someOrNotLanguageKeyword)) && l /= "?" -> l _ -> "`" <> l <> "`" where @@ -829,7 +829,11 @@ prettyPrinters characterSet = <> Pretty.align (keyword "with" <> " " <> update) (update, _) = - prettyKeyValue prettyOperatorExpression equals (makeKeyValue b c) + prettyKeyValue prettyOperatorExpression equals + (makeKeyValue (fmap toText b) c) + + toText WithQuestion = "?" + toText (WithLabel k ) = k prettyExpression (Assert a) = Pretty.group (Pretty.flatAlt long short) where diff --git a/dhall/src/Dhall/Syntax.hs b/dhall/src/Dhall/Syntax.hs index 16d5541d0..83ca37907 100644 --- a/dhall/src/Dhall/Syntax.hs +++ b/dhall/src/Dhall/Syntax.hs @@ -37,6 +37,7 @@ module Dhall.Syntax ( , makeFunctionBinding , FieldSelection(..) , makeFieldSelection + , WithComponent(..) -- ** 'Let'-blocks , MultiLet(..) @@ -79,9 +80,6 @@ module Dhall.Syntax ( , linesLiteral , unlinesLiteral - -- * Desugaring - , desugarWith - -- * Utilities , internalError -- `shift` should really be in `Dhall.Normalize`, but it's here to avoid a @@ -118,7 +116,6 @@ import qualified Data.List.NonEmpty as NonEmpty import qualified Data.Text import qualified Data.Time as Time import qualified Dhall.Crypto -import qualified Dhall.Optics as Optics import qualified Lens.Family as Lens import qualified Network.URI as URI import qualified Prettyprinter as Pretty @@ -429,6 +426,10 @@ data FieldSelection s = FieldSelection makeFieldSelection :: Text -> FieldSelection s makeFieldSelection t = FieldSelection Nothing t Nothing +-- | A path component for a @with@ expression +data WithComponent = WithLabel Text | WithQuestion + deriving (Data, Eq, Generic, Lift, NFData, Ord, Show) + {-| Syntax tree for expressions The @s@ type parameter is used to track the presence or absence of `Src` @@ -644,7 +645,7 @@ data Expr s a -- | > Equivalent _ x y ~ x ≡ y | Equivalent (Maybe CharacterSet) (Expr s a) (Expr s a) -- | > With x y e ~ x with y = e - | With (Expr s a) (NonEmpty Text) (Expr s a) + | With (Expr s a) (NonEmpty WithComponent) (Expr s a) -- | > Note s x ~ e | Note s (Expr s a) -- | > ImportAlt ~ e1 ? e2 @@ -1464,30 +1465,6 @@ shift d (V x n) (Let (Binding src0 f src1 mt src2 r) e) = r' = shift d (V x n) r shift d v expression = Lens.over subExpressions (shift d v) expression --- | Desugar all @with@ expressions -desugarWith :: Expr s a -> Expr s a -desugarWith = Optics.rewriteOf subExpressions rewrite - where - rewrite e@(With record (key :| []) value) = - Just - (Prefer - mempty - (PreferFromWith e) - record - (RecordLit [ (key, makeRecordField value) ]) - ) - rewrite e@(With record (key0 :| key1 : keys) value) = - Just - (Let - (makeBinding "_" record) - (Prefer mempty (PreferFromWith e) "_" - (RecordLit - [ (key0, makeRecordField $ With (Field "_" (FieldSelection Nothing key0 Nothing)) (key1 :| keys) (shift 1 "_" value)) ] - ) - ) - ) - rewrite _ = Nothing - _ERROR :: String _ERROR = "\ESC[1;31mError\ESC[0m" diff --git a/dhall/src/Dhall/TypeCheck.hs b/dhall/src/Dhall/TypeCheck.hs index 7eb205833..0bd76b378 100644 --- a/dhall/src/Dhall/TypeCheck.hs +++ b/dhall/src/Dhall/TypeCheck.hs @@ -61,6 +61,7 @@ import Dhall.Syntax , PreferAnnotation (..) , RecordField (..) , Var (..) + , WithComponent (..) ) import qualified Data.Foldable as Foldable @@ -1283,25 +1284,41 @@ infer typer = loop -- The purpose of this inner loop is to ensure that we only need to -- typecheck the record once - let with tE' ks v = do - kTs' <- case tE' of - VRecord kTs' -> return kTs' - _ -> die (NotWithARecord e₀ (quote names tE')) + let with tE' ks v = case tE' of + VRecord kTs' -> case ks of - k :| [] -> do - tV' <- loop ctx v + WithLabel k :| [] -> do + tV' <- loop ctx v - return (VRecord (Dhall.Map.insert k tV' kTs')) - k₀ :| k₁ : ks' -> do - let _T = - case Dhall.Map.lookup k₀ kTs' of - Just _T' -> _T' - Nothing -> VRecord mempty + return (VRecord (Dhall.Map.insert k tV' kTs')) + WithLabel k₀ :| k₁ : ks' -> do + let _T = + case Dhall.Map.lookup k₀ kTs' of + Just _T' -> _T' + Nothing -> VRecord mempty - tV' <- with _T (k₁ :| ks') v + tV' <- with _T (k₁ :| ks') v - return (VRecord (Dhall.Map.insert k₀ tV' kTs')) + return (VRecord (Dhall.Map.insert k₀ tV' kTs')) + WithQuestion :| _ -> do + die NotALabelPath + + VOptional _O' -> do + case ks of + WithQuestion :| [] -> do + tV' <- loop ctx v + if Eval.conv values _O' tV' + then return (VOptional _O') + else die OptionalWithTypeMismatch + + WithQuestion :| k₁ : ks' -> do + tV' <- with _O' (k₁ :| ks') v + return (VOptional tV') + + WithLabel k :| _ -> die (NotAQuestionPath k) + + _ -> die (NotWithARecord e₀ (quote names tE')) -- TODO: NotWithARecordOrOptional with tE₀' ks₀ v₀ @@ -1404,6 +1421,9 @@ data TypeMessage s a | CantListAppend (Expr s a) (Expr s a) | CantAdd (Expr s a) (Expr s a) | CantMultiply (Expr s a) (Expr s a) + | OptionalWithTypeMismatch + | NotALabelPath + | NotAQuestionPath Text | ShowConstructorNotOnUnion deriving (Show) @@ -4559,6 +4579,120 @@ prettyTypeMessage (CantAdd expr0 expr1) = prettyTypeMessage (CantMultiply expr0 expr1) = buildNaturalOperator "*" expr0 expr1 +prettyTypeMessage OptionalWithTypeMismatch = ErrorMessages {..} + where + short = "❰with❱ cannot change the type of an ❰Optional❱ value" + hints = [] + long = + "Explanation: The ❰with❱ keyword cannot change the type of a value stored inside \n\ + \of a ❰Some❱ constructor \n\ + \ \n\ + \For example, this is a valid use of ❰with❱: \n\ + \ \n\ + \ \n\ + \ The old value has type ❰Natural❱ \n\ + \ ⇩ \n\ + \ ┌───────────────────┐ \n\ + \ │ Some 1 with ? = 2 │ \n\ + \ └───────────────────┘ \n\ + \ ⇧ \n\ + \ ... which matches the type of the new value, which is also\n\ + \ ❰Natural❱ \n\ + \ \n\ + \ \n\ + \... but the following example is not valid: \n\ + \ \n\ + \ \n\ + \ The old value has type ❰Natural❱ \n\ + \ ⇩ \n\ + \ ┌──────────────────────┐ \n\ + \ │ Some 1 with ? = True │ \n\ + \ └──────────────────────┘ \n\ + \ ⇧ \n\ + \ ... but the new value has type ❰Bool❱, which does not \n\ + \ match \n" + +prettyTypeMessage NotALabelPath = ErrorMessages {..} + where + short = "Use a label to update a record" + hints = [] + long = + "Explanation: The ❰with❱ keyword supports updating records by naming the field(s)\n\ + \to update, but you provided a path component of ❰?❱, which only works on \n\ + \❰Optional❱ values and not records. \n\ + \ \n\ + \For example, these are valid uses of ❰with❱ to update a record: \n\ + \ \n\ + \ \n\ + \ ┌──────────────────────┐ \n\ + \ │ { x = 1 } with x = 2 │ \n\ + \ └──────────────────────┘ \n\ + \ \n\ + \ \n\ + \ ┌────────────────────────────────┐ \n\ + \ │ { x = { y = 1 } } with x.y = 2 │ \n\ + \ └────────────────────────────────┘ \n\ + \ \n\ + \ \n\ + \... but the following example is not valid: \n\ + \ \n\ + \ \n\ + \ ┌──────────────────────┐ \n\ + \ │ { x = 1 } with ? = 2 │ \n\ + \ └──────────────────────┘ \n\ + \ ⇧ \n\ + \ This path component is reserved for updating ❰Optional❱ \n\ + \ values and not records \n\ + \ \n\ + \Note that you can update a field named ❰?❱ if you escape the path component, \n\ + \though: \n\ + \ \n\ + \ \n\ + \ ┌────────────────────────┐ \n\ + \ │ { ? = 1 } with `?` = 2 │ \n\ + \ └────────────────────────┘ \n" + +prettyTypeMessage (NotAQuestionPath k) = ErrorMessages {..} + where + short = "Use ❰?❱ to update an ❰Optional❱ value" + hints = [] + long = + "Explanation: The ❰with❱ keyword supports updating ❰Optional❱ values using a path\n\ + \component of ❰?❱, but you provided a path component other than ❰?❱. \n\ + \ \n\ + \For example, these are valid uses of ❰with❱ to update an ❰Optional❱ value: \n\ + \ \n\ + \ \n\ + \ ┌───────────────────┐ \n\ + \ │ Some 1 with ? = 2 │ \n\ + \ └───────────────────┘ \n\ + \ \n\ + \ \n\ + \ ┌─────────────────────────────┐ \n\ + \ │ { x = Some 1 } with x.? = 2 │ \n\ + \ └─────────────────────────────┘ \n\ + \ \n\ + \ \n\ + \... but the following example is not valid: \n\ + \ \n\ + \ \n\ + \ ┌──────────────────────┐ \n\ + \ │ Some 1 with x = True │ \n\ + \ └──────────────────────┘ \n\ + \ ⇧ \n\ + \ This path component should have been ❰?❱ \n\ + \ \n\ + \ \n\ + \────────────────────────────────────────────────────────────────────────────────\n\ + \ \n\ + \You provided this path component: \n\ + \ \n\ + \" <> txt0 <> "\n\ + \ \n\ + \... which perhaps should have been ❰?❱. \n" + where + txt0 = insert k + prettyTypeMessage ShowConstructorNotOnUnion = ErrorMessages {..} where short = "ShowConstructorNotOnUnion" @@ -4846,6 +4980,12 @@ messageExpressions f m = case m of CantAdd <$> f a <*> f b CantMultiply a b -> CantMultiply <$> f a <*> f b + OptionalWithTypeMismatch -> + pure OptionalWithTypeMismatch + NotALabelPath -> + pure NotALabelPath + NotAQuestionPath k -> + pure (NotAQuestionPath k) ShowConstructorNotOnUnion -> pure ShowConstructorNotOnUnion diff --git a/dhall/tests/Dhall/Test/QuickCheck.hs b/dhall/tests/Dhall/Test/QuickCheck.hs index 27a39b39c..cc4aeacfc 100644 --- a/dhall/tests/Dhall/Test/QuickCheck.hs +++ b/dhall/tests/Dhall/Test/QuickCheck.hs @@ -52,6 +52,7 @@ import Dhall.Core , Scheme (..) , URL (..) , Var (..) + , WithComponent (..) ) import Dhall.Map (Map) @@ -298,6 +299,10 @@ instance Arbitrary s => Arbitrary (FieldSelection s) where arbitrary = FieldSelection <$> pure Nothing <*> label <*> pure Nothing shrink = genericShrink +instance Arbitrary WithComponent where + arbitrary = + Test.QuickCheck.oneof [ pure WithQuestion, WithLabel <$> arbitrary ] + instance (Arbitrary s, Arbitrary a) => Arbitrary (Expr s a) where arbitrary = Test.QuickCheck.suchThat