Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

Add support for List/{drop,take} #2430

Open
wants to merge 1 commit into
base: main
Choose a base branch
from
Open

Add support for List/{drop,take} #2430

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
1 commit
Select commit
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
2 changes: 2 additions & 0 deletions dhall-bash/src/Dhall/Bash.hs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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)
Expand Down
6 changes: 6 additions & 0 deletions dhall-json/src/Dhall/JSON.hs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -966,6 +966,9 @@ convertToHomogeneousMaps (Conversion {..}) e0 = loop (Core.normalize e0)
Core.ListBuild ->
Core.ListBuild

Core.ListDrop ->
Core.ListDrop

Core.ListFold ->
Core.ListFold

Expand All @@ -984,6 +987,9 @@ convertToHomogeneousMaps (Conversion {..}) e0 = loop (Core.normalize e0)
Core.ListReverse ->
Core.ListReverse

Core.ListTake ->
Core.ListTake

Core.Optional ->
Core.Optional

Expand Down
28 changes: 28 additions & 0 deletions dhall-nix/src/Dhall/Nix.hs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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"
Expand Down Expand Up @@ -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)
Expand Down
2 changes: 1 addition & 1 deletion dhall/dhall-lang
Open in desktop
Submodule dhall-lang updated 112 files
10 changes: 9 additions & 1 deletion dhall/src/Dhall/Binary.hs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down Expand Up @@ -716,6 +718,9 @@ encodeExpressionInternal encodeEmbed = go
ListBuild ->
Encoding.encodeUtf8ByteArray "List/build"

ListDrop ->
Encoding.encodeUtf8ByteArray "List/drop"

ListFold ->
Encoding.encodeUtf8ByteArray "List/fold"

Expand All @@ -734,6 +739,9 @@ encodeExpressionInternal encodeEmbed = go
ListReverse ->
Encoding.encodeUtf8ByteArray "List/reverse"

ListTake ->
Encoding.encodeUtf8ByteArray "List/take"

Bool ->
Encoding.encodeUtf8ByteArray "Bool"

Expand Down
12 changes: 12 additions & 0 deletions dhall/src/Dhall/Diff.hs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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 =
Expand Down Expand Up @@ -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 =
Expand Down
61 changes: 60 additions & 1 deletion dhall/src/Dhall/Eval.hs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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)
Expand Down Expand Up @@ -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 ->
Expand Down Expand Up @@ -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 ->
Expand Down Expand Up @@ -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') ->
Expand Down Expand Up @@ -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 ->
Expand All @@ -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 ->
Expand Down Expand Up @@ -1423,6 +1478,8 @@ alphaNormalize = goEnv EmptyNames
ListAppend (go t) (go u)
ListBuild ->
ListBuild
ListDrop ->
ListDrop
ListFold ->
ListFold
ListLength ->
Expand All @@ -1435,6 +1492,8 @@ alphaNormalize = goEnv EmptyNames
ListIndexed
ListReverse ->
ListReverse
ListTake ->
ListTake
Optional ->
Optional
Some t ->
Expand Down
42 changes: 42 additions & 0 deletions dhall/src/Dhall/Normalize.hs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down Expand Up @@ -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
Expand Down Expand Up @@ -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
Expand Down Expand Up @@ -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 [] ""))) _) _ ->
Expand Down Expand Up @@ -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
Expand Down
2 changes: 2 additions & 0 deletions dhall/src/Dhall/Parser/Expression.hs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down
Loading