From b628a57c79c7a94ca5b9de88f9f12e7d98bb3e8c Mon Sep 17 00:00:00 2001 From: Gabriella Gonzalez Date: Mon, 27 Jun 2022 20:31:33 -0700 Subject: [PATCH] Add support for `List/{drop,take}` MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit … as standardized in https://github.com/dhall-lang/dhall-lang/pull/1287 --- dhall-bash/src/Dhall/Bash.hs | 2 + dhall-json/src/Dhall/JSON.hs | 6 +++ dhall-nix/src/Dhall/Nix.hs | 28 +++++++++++++ dhall/dhall-lang | 2 +- dhall/src/Dhall/Binary.hs | 10 ++++- dhall/src/Dhall/Diff.hs | 12 ++++++ dhall/src/Dhall/Eval.hs | 61 +++++++++++++++++++++++++++- dhall/src/Dhall/Normalize.hs | 42 +++++++++++++++++++ dhall/src/Dhall/Parser/Expression.hs | 2 + dhall/src/Dhall/Parser/Token.hs | 16 ++++++++ dhall/src/Dhall/Pretty/Internal.hs | 4 ++ dhall/src/Dhall/Syntax.hs | 8 ++++ dhall/src/Dhall/TypeCheck.hs | 8 ++++ dhall/tests/Dhall/Test/QuickCheck.hs | 2 + nix/shared.nix | 2 +- 15 files changed, 201 insertions(+), 4 deletions(-) diff --git a/dhall-bash/src/Dhall/Bash.hs b/dhall-bash/src/Dhall/Bash.hs index 855045d1d..56e463a8e 100644 --- a/dhall-bash/src/Dhall/Bash.hs +++ b/dhall-bash/src/Dhall/Bash.hs @@ -324,12 +324,14 @@ dhallToStatement expr0 var0 = go (Dhall.Core.normalize expr0) go e@(List ) = Left (UnsupportedStatement e) go e@(ListAppend {}) = Left (UnsupportedStatement e) go e@(ListBuild ) = Left (UnsupportedStatement e) + go e@(ListDrop ) = Left (UnsupportedStatement e) go e@(ListFold ) = Left (UnsupportedStatement e) go e@(ListLength ) = Left (UnsupportedStatement e) go e@(ListHead ) = Left (UnsupportedStatement e) go e@(ListLast ) = Left (UnsupportedStatement e) go e@(ListIndexed ) = Left (UnsupportedStatement e) go e@(ListReverse ) = Left (UnsupportedStatement e) + go e@(ListTake ) = Left (UnsupportedStatement e) go e@(Optional ) = Left (UnsupportedStatement e) go e@(None ) = Left (UnsupportedStatement e) go e@(Record {}) = Left (UnsupportedStatement e) diff --git a/dhall-json/src/Dhall/JSON.hs b/dhall-json/src/Dhall/JSON.hs index 4e579d7dd..f967a8773 100644 --- a/dhall-json/src/Dhall/JSON.hs +++ b/dhall-json/src/Dhall/JSON.hs @@ -966,6 +966,9 @@ convertToHomogeneousMaps (Conversion {..}) e0 = loop (Core.normalize e0) Core.ListBuild -> Core.ListBuild + Core.ListDrop -> + Core.ListDrop + Core.ListFold -> Core.ListFold @@ -984,6 +987,9 @@ convertToHomogeneousMaps (Conversion {..}) e0 = loop (Core.normalize e0) Core.ListReverse -> Core.ListReverse + Core.ListTake -> + Core.ListTake + Core.Optional -> Core.Optional diff --git a/dhall-nix/src/Dhall/Nix.hs b/dhall-nix/src/Dhall/Nix.hs index 956694450..00eeb3e5a 100644 --- a/dhall-nix/src/Dhall/Nix.hs +++ b/dhall-nix/src/Dhall/Nix.hs @@ -519,6 +519,20 @@ dhallToNix e = @@ Nix.mkList [] ) ) + loop ListDrop = do + return + ( "n" + ==> "a" + ==> "as" + ==> Nix.letsE + [ ("maxLength", ("builtins.length" @@ "as") $- "n") + , ("newLength", Nix.mkIf (Nix.mkInt 0 $<= "newLength") "newLength" (Nix.mkInt 0)) + ] + ( "builtins.genList" + @@ ("i" ==> ("builtins.elemAt" @@ "as" @@ ("n" $+ "i"))) + @@ "newLength" + ) + ) loop ListFold = do return ( "t" @@ -584,6 +598,20 @@ dhallToNix e = @@ "n" ) ) + loop ListTake = do + return + ( "n" + ==> "a" + ==> "as" + ==> Nix.letsE + [ ("oldLength", "builtins.length" @@ "as") + , ("newLength", Nix.mkIf ("n" $<= "oldLength") "n" "oldLength") + ] + ( "builtins.genList" + @@ ("builtins.elemAt" @@ "as") + @@ "newLength" + ) + ) loop Optional = return ("t" ==> untranslatable) loop (Some a) = loop a loop None = return ("t" ==> Nix.mkNull) diff --git a/dhall/dhall-lang b/dhall/dhall-lang index 149cc55e7..ff10b8215 160000 --- a/dhall/dhall-lang +++ b/dhall/dhall-lang @@ -1 +1 @@ -Subproject commit 149cc55e7170db15e2196a82a56ea05e935b80f5 +Subproject commit ff10b8215a5108362ca35845769a6fcb59500cc9 diff --git a/dhall/src/Dhall/Binary.hs b/dhall/src/Dhall/Binary.hs index d9698fa57..6a6ca51c1 100644 --- a/dhall/src/Dhall/Binary.hs +++ b/dhall/src/Dhall/Binary.hs @@ -149,10 +149,12 @@ decodeExpressionInternal decodeEmbed = go | sb == "Natural" -> return Natural 8 | sb == "Optional" -> return Optional | sb == "TimeZone" -> return TimeZone - 9 | sb == "List/fold" -> return ListFold + 9 | sb == "List/drop" -> return ListDrop + | sb == "List/fold" -> return ListFold | sb == "List/head" -> return ListHead | sb == "List/last" -> return ListLast | sb == "Text/show" -> return TextShow + | sb == "List/take" -> return ListTake 10 | sb == "List/build" -> return ListBuild 11 | sb == "Double/show" -> return DoubleShow | sb == "List/length" -> return ListLength @@ -716,6 +718,9 @@ encodeExpressionInternal encodeEmbed = go ListBuild -> Encoding.encodeUtf8ByteArray "List/build" + ListDrop -> + Encoding.encodeUtf8ByteArray "List/drop" + ListFold -> Encoding.encodeUtf8ByteArray "List/fold" @@ -734,6 +739,9 @@ encodeExpressionInternal encodeEmbed = go ListReverse -> Encoding.encodeUtf8ByteArray "List/reverse" + ListTake -> + Encoding.encodeUtf8ByteArray "List/take" + Bool -> Encoding.encodeUtf8ByteArray "Bool" diff --git a/dhall/src/Dhall/Diff.hs b/dhall/src/Dhall/Diff.hs index 06fe15aee..2eeaa6a25 100644 --- a/dhall/src/Dhall/Diff.hs +++ b/dhall/src/Dhall/Diff.hs @@ -1316,6 +1316,12 @@ diffPrimitiveExpression l@ListBuild r = mismatch l r diffPrimitiveExpression l r@ListBuild = mismatch l r +diffPrimitiveExpression ListDrop ListDrop = + "…" +diffPrimitiveExpression l@ListDrop r = + mismatch l r +diffPrimitiveExpression l r@ListDrop = + mismatch l r diffPrimitiveExpression ListFold ListFold = "…" diffPrimitiveExpression l@ListFold r = @@ -1352,6 +1358,12 @@ diffPrimitiveExpression l@ListReverse r = mismatch l r diffPrimitiveExpression l r@ListReverse = mismatch l r +diffPrimitiveExpression ListTake ListTake = + "…" +diffPrimitiveExpression l@ListTake r = + mismatch l r +diffPrimitiveExpression l r@ListTake = + mismatch l r diffPrimitiveExpression Optional Optional = "…" diffPrimitiveExpression l@Optional r = diff --git a/dhall/src/Dhall/Eval.hs b/dhall/src/Dhall/Eval.hs index d082e9d00..1bda0e114 100644 --- a/dhall/src/Dhall/Eval.hs +++ b/dhall/src/Dhall/Eval.hs @@ -211,12 +211,14 @@ data Val a | VListLit !(Maybe (Val a)) !(Seq (Val a)) | VListAppend !(Val a) !(Val a) | VListBuild (Val a) !(Val a) + | VListDrop !(Val a) (Val a) !(Val a) | VListFold (Val a) !(Val a) !(Val a) !(Val a) !(Val a) | VListLength (Val a) !(Val a) | VListHead (Val a) !(Val a) | VListLast (Val a) !(Val a) | VListIndexed (Val a) !(Val a) | VListReverse (Val a) !(Val a) + | VListTake !(Val a) (Val a) !(Val a) | VOptional (Val a) | VSome (Val a) @@ -684,7 +686,30 @@ eval !env t0 = VHLam (Typed "as" (VList a)) (\as -> vListAppend (VListLit Nothing (pure x)) as)) `vApp` VListLit (Just (VList a)) mempty - + ListDrop -> + VPrim $ \n -> + VPrim $ \a -> + VPrim $ \list -> + let inert = VListDrop n a list + in case n of + VPrimVar -> inert + _ -> case a of + VPrimVar -> inert + _ -> case list of + VPrimVar -> inert + _ | VListLit _ as <- list + , Sequence.null as -> + list + | VNaturalLit 0 <- n -> + list + | VListLit _ as <- list + , VNaturalLit m <- n -> + let as' = Sequence.drop (fromIntegral m) as + in if Sequence.null as' + then VListLit (Just a) as' + else VListLit Nothing as' + | otherwise -> + VListDrop n a list ListFold -> VPrim $ \a -> VPrim $ \as -> @@ -759,6 +784,28 @@ eval !env t0 = VListLit Nothing (Sequence.reverse as) t -> VListReverse a t + ListTake -> + VPrim $ \n -> + VPrim $ \a -> + VPrim $ \list -> + let inert = VListTake n a list + in case n of + VPrimVar -> inert + _ -> case a of + VPrimVar -> inert + _ -> case list of + VPrimVar -> inert + _ | VListLit _ as <- list + , Sequence.null as -> + list + | VNaturalLit 0 <- n -> + VListLit (Just a) Sequence.empty + | VListLit _ as <- list + , VNaturalLit m <- n -> + let as' = Sequence.take (fromIntegral m) as + in VListLit Nothing as' + | otherwise -> + VListTake n a list Optional -> VPrim VOptional Some t -> @@ -1022,6 +1069,10 @@ conv !env t0 t0' = conv env t t' (VListReverse _ t, VListReverse _ t') -> conv env t t' + (VListDrop n a as, VListDrop n' a' as') -> + conv env n n' && conv env a a' && conv env a a' && conv env as as' + (VListTake n a as, VListTake n' a' as') -> + conv env n n' && conv env a a' && conv env a a' && conv env as as' (VListFold a l _ t u, VListFold a' l' _ t' u') -> conv env a a' && conv env l l' && conv env t t' && conv env u u' (VOptional a, VOptional a') -> @@ -1224,6 +1275,8 @@ quote !env !t0 = ListAppend (quote env t) (quote env u) VListBuild a t -> ListBuild `qApp` a `qApp` t + VListDrop n a as -> + ListDrop `qApp` n `qApp` a `qApp` as VListFold a l t u v -> ListFold `qApp` a `qApp` l `qApp` t `qApp` u `qApp` v VListLength a t -> @@ -1236,6 +1289,8 @@ quote !env !t0 = ListIndexed `qApp` a `qApp` t VListReverse a t -> ListReverse `qApp` a `qApp` t + VListTake n a as -> + ListTake `qApp` n `qApp` a `qApp` as VOptional a -> Optional `qApp` a VSome t -> @@ -1423,6 +1478,8 @@ alphaNormalize = goEnv EmptyNames ListAppend (go t) (go u) ListBuild -> ListBuild + ListDrop -> + ListDrop ListFold -> ListFold ListLength -> @@ -1435,6 +1492,8 @@ alphaNormalize = goEnv EmptyNames ListIndexed ListReverse -> ListReverse + ListTake -> + ListTake Optional -> Optional Some t -> diff --git a/dhall/src/Dhall/Normalize.hs b/dhall/src/Dhall/Normalize.hs index 7e5b91b96..7a388b84d 100644 --- a/dhall/src/Dhall/Normalize.hs +++ b/dhall/src/Dhall/Normalize.hs @@ -269,6 +269,20 @@ normalizeWithM ctx e0 = loop (Syntax.denote e0) ) nil = ListLit (Just (App List _A₀)) empty + App (App (App ListDrop n) a_) as + | ListLit _ as' <- as + , Data.Sequence.null as' -> + return as + | NaturalLit 0 <- n -> + return as + | ListLit _ as' <- as + , NaturalLit m <- n -> do + let as'' = Data.Sequence.drop (fromIntegral m) as' + if Data.Sequence.null as'' + then return (ListLit (Just a_) as') + else return (ListLit Nothing as') + | otherwise -> + return (App (App (App ListDrop n) a_) as) App (App (App (App (App ListFold _) (ListLit _ xs)) t) cons) nil -> do t' <- loop t if boundedType t' then strict else lazy @@ -315,6 +329,18 @@ normalizeWithM ctx e0 = loop (Syntax.denote e0) ] App (App ListReverse _) (ListLit t xs) -> loop (ListLit t (Data.Sequence.reverse xs)) + App (App (App ListTake n) a_) as + | ListLit _ as' <- as + , Data.Sequence.null as' -> + return as + | NaturalLit 0 <- n -> + return as + | ListLit _ as' <- as + , NaturalLit m <- n -> do + let as'' = Data.Sequence.take (fromIntegral m) as' + return (ListLit Nothing as'') + | otherwise -> + return (App (App (App ListTake n) a_) as) App TextShow (TextLit (Chunks [] oldText)) -> loop (TextLit (Chunks [] newText)) where @@ -501,12 +527,14 @@ normalizeWithM ctx e0 = loop (Syntax.denote e0) decide (ListLit t m) (ListLit _ n) = ListLit t (m <> n) decide l r = ListAppend l r ListBuild -> pure ListBuild + ListDrop -> pure ListDrop ListFold -> pure ListFold ListLength -> pure ListLength ListHead -> pure ListHead ListLast -> pure ListLast ListIndexed -> pure ListIndexed ListReverse -> pure ListReverse + ListTake -> pure ListTake Optional -> pure Optional Some a -> Some <$> a' where @@ -794,12 +822,24 @@ isNormalized e0 = loop (Syntax.denote e0) App IntegerToDouble (IntegerLit _) -> False App DoubleShow (DoubleLit _) -> False App (App ListBuild _) _ -> False + App (App (App ListDrop n) _) as + | NaturalLit 0 <- n -> False + | ListLit _ as' <- as + , Data.Sequence.null as' -> False + | NaturalLit _ <- n + , ListLit _ _ <- as -> False App (App (App (App (App (App ListFold _) (ListLit _ _)) _) _) _) _ -> False App (App ListLength _) (ListLit _ _) -> False App (App ListHead _) (ListLit _ _) -> False App (App ListLast _) (ListLit _ _) -> False App (App ListIndexed _) (ListLit _ _) -> False App (App ListReverse _) (ListLit _ _) -> False + App (App (App ListTake n) _) as + | NaturalLit 0 <- n -> False + | ListLit _ as' <- as + , Data.Sequence.null as' -> False + | NaturalLit _ <- n + , ListLit _ _ <- as -> False App TextShow (TextLit (Chunks [] _)) -> False App (App (App TextReplace (TextLit (Chunks [] ""))) _) _ -> @@ -895,12 +935,14 @@ isNormalized e0 = loop (Syntax.denote e0) decide (ListLit _ _) (ListLit _ _) = False decide _ _ = True ListBuild -> True + ListDrop -> True ListFold -> True ListLength -> True ListHead -> True ListLast -> True ListIndexed -> True ListReverse -> True + ListTake -> True Optional -> True Some a -> loop a None -> True diff --git a/dhall/src/Dhall/Parser/Expression.hs b/dhall/src/Dhall/Parser/Expression.hs index 321d3d65b..541e86f41 100644 --- a/dhall/src/Dhall/Parser/Expression.hs +++ b/dhall/src/Dhall/Parser/Expression.hs @@ -727,12 +727,14 @@ parsers embedded = Parsers{..} 'L' -> choice [ ListBuild <$ _ListBuild + , ListDrop <$ _ListDrop , ListFold <$ _ListFold , ListLength <$ _ListLength , ListHead <$ _ListHead , ListLast <$ _ListLast , ListIndexed <$ _ListIndexed , ListReverse <$ _ListReverse + , ListTake <$ _ListTake , List <$ _List ] 'O' -> Optional <$ _Optional diff --git a/dhall/src/Dhall/Parser/Token.hs b/dhall/src/Dhall/Parser/Token.hs index 7292561a6..2118d4b6d 100644 --- a/dhall/src/Dhall/Parser/Token.hs +++ b/dhall/src/Dhall/Parser/Token.hs @@ -65,12 +65,14 @@ module Dhall.Parser.Token ( _IntegerToDouble, _DoubleShow, _ListBuild, + _ListDrop, _ListFold, _ListLength, _ListHead, _ListLast, _ListIndexed, _ListReverse, + _ListTake, _Bool, _Natural, _Integer, @@ -1083,6 +1085,13 @@ _DoubleShow = builtin "Double/show" _ListBuild :: Parser () _ListBuild = builtin "List/build" +{-| Parse the @List/drop@ built-in + + This corresponds to the @List-drop@ rule from the official grammar +-} +_ListDrop :: Parser () +_ListDrop = builtin "List/drop" + {-| Parse the @List/fold@ built-in This corresponds to the @List-fold@ rule from the official grammar @@ -1125,6 +1134,13 @@ _ListIndexed = builtin "List/indexed" _ListReverse :: Parser () _ListReverse = builtin "List/reverse" +{-| Parse the @List/take@ built-in + + This corresponds to the @List-take@ rule from the official grammar +-} +_ListTake :: Parser () +_ListTake = builtin "List/take" + {-| Parse the @Bool@ built-in This corresponds to the @Bool@ rule from the official grammar diff --git a/dhall/src/Dhall/Pretty/Internal.hs b/dhall/src/Dhall/Pretty/Internal.hs index 3b45ffb8a..54b1ca825 100644 --- a/dhall/src/Dhall/Pretty/Internal.hs +++ b/dhall/src/Dhall/Pretty/Internal.hs @@ -1368,6 +1368,8 @@ prettyPrinters characterSet = builtin "List" prettyPrimitiveExpression ListBuild = builtin "List/build" + prettyPrimitiveExpression ListDrop = + builtin "List/drop" prettyPrimitiveExpression ListFold = builtin "List/fold" prettyPrimitiveExpression ListLength = @@ -1380,6 +1382,8 @@ prettyPrinters characterSet = builtin "List/indexed" prettyPrimitiveExpression ListReverse = builtin "List/reverse" + prettyPrimitiveExpression ListTake = + builtin "List/take" prettyPrimitiveExpression Optional = builtin "Optional" prettyPrimitiveExpression None = diff --git a/dhall/src/Dhall/Syntax.hs b/dhall/src/Dhall/Syntax.hs index 83ca37907..2a289141b 100644 --- a/dhall/src/Dhall/Syntax.hs +++ b/dhall/src/Dhall/Syntax.hs @@ -579,6 +579,8 @@ data Expr s a | ListAppend (Expr s a) (Expr s a) -- | > ListBuild ~ List/build | ListBuild + -- | > ListDrop ~ List/drop + | ListDrop -- | > ListFold ~ List/fold | ListFold -- | > ListLength ~ List/length @@ -591,6 +593,8 @@ data Expr s a | ListIndexed -- | > ListReverse ~ List/reverse | ListReverse + -- | > ListTake ~ List/take + | ListTake -- | > Optional ~ Optional | Optional -- | > Some e ~ Some e @@ -861,12 +865,14 @@ unsafeSubExpressions _ List = pure List unsafeSubExpressions f (ListLit a b) = ListLit <$> traverse f a <*> traverse f b unsafeSubExpressions f (ListAppend a b) = ListAppend <$> f a <*> f b unsafeSubExpressions _ ListBuild = pure ListBuild +unsafeSubExpressions _ ListDrop = pure ListDrop unsafeSubExpressions _ ListFold = pure ListFold unsafeSubExpressions _ ListLength = pure ListLength unsafeSubExpressions _ ListHead = pure ListHead unsafeSubExpressions _ ListLast = pure ListLast unsafeSubExpressions _ ListIndexed = pure ListIndexed unsafeSubExpressions _ ListReverse = pure ListReverse +unsafeSubExpressions _ ListTake = pure ListTake unsafeSubExpressions _ Optional = pure Optional unsafeSubExpressions f (Some a) = Some <$> f a unsafeSubExpressions _ None = pure None @@ -1260,12 +1266,14 @@ reservedIdentifiers = reservedKeywords <> , "Natural/subtract" , "Double/show" , "List/build" + , "List/drop" , "List/fold" , "List/length" , "List/head" , "List/last" , "List/indexed" , "List/reverse" + , "List/take" , "Text/replace" , "Text/show" , "Bool" diff --git a/dhall/src/Dhall/TypeCheck.hs b/dhall/src/Dhall/TypeCheck.hs index 82667d1bf..cf25834b5 100644 --- a/dhall/src/Dhall/TypeCheck.hs +++ b/dhall/src/Dhall/TypeCheck.hs @@ -686,6 +686,10 @@ infer typer = loop ) ) + ListDrop -> + return + (VNatural ~> VHPi "a" (VConst Type) (\a -> VList a ~> VList a)) + ListFold -> return ( VHPi "a" (VConst Type) (\a -> @@ -724,6 +728,10 @@ infer typer = loop ListReverse -> return (VHPi "a" (VConst Type) (\a -> VList a ~> VList a)) + ListTake -> + return + (VNatural ~> VHPi "a" (VConst Type) (\a -> VList a ~> VList a)) + Optional -> return (VConst Type ~> VConst Type) diff --git a/dhall/tests/Dhall/Test/QuickCheck.hs b/dhall/tests/Dhall/Test/QuickCheck.hs index cc4aeacfc..792593d41 100644 --- a/dhall/tests/Dhall/Test/QuickCheck.hs +++ b/dhall/tests/Dhall/Test/QuickCheck.hs @@ -394,12 +394,14 @@ instance (Arbitrary s, Arbitrary a) => Arbitrary (Expr s a) where % (1 :: W "ListLit") % (1 :: W "ListAppend") % (1 :: W "ListBuild") + % (1 :: W "ListDrop") % (1 :: W "ListFold") % (1 :: W "ListLength") % (1 :: W "ListHead") % (1 :: W "ListLast") % (1 :: W "ListIndexed") % (1 :: W "ListReverse") + % (1 :: W "ListTake") % (1 :: W "Optional") % (7 :: W "Some") % (1 :: W "None") diff --git a/nix/shared.nix b/nix/shared.nix index 3c95c8578..fcad55501 100644 --- a/nix/shared.nix +++ b/nix/shared.nix @@ -236,7 +236,7 @@ let [ (pkgsNew.haskell.lib.packagesFromDirectory { directory = ./packages; }) extension doCheckExtension - doBenchmarkExtension + # doBenchmarkExtension failOnAllWarningsExtension failOnMissingHaddocksExtension ];