ehmry/dhall-haskell
ehmry/dhall-haskell
1
0
Fork 0
Code Issues Pull Requests Releases Wiki Activity

dhall-nix: Fix field-based union access (#907)

Browse Source 
Fixes #906.

This adds new translation rules:

* <Foo : {} | Bar>.Foo => x: { Bar, Foo }: Foo x

* <Foo : {} | Bar>.Foo {=} => { Bar, Foo }: Foo {}

* <Foo : {} | Bar>.Bar => { Bar, Foo }: Bar
This commit is contained in:
Ollie Charles 2019-04-27 11:17:01 +01:00 committed by GitHub
parent 21da6f2b7f
commit d3d7baf3e5
No known key found for this signature in database
GPG Key ID: 4AEE18F83AFDEB23
1 changed files with 27 additions and 0 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

27
dhall-nix/src/Dhall/Nix.hs
View File

@ -208,6 +208,13 @@ dhallToNix e = loop (Dhall.Core.normalize e)
-- None needs a type to convert to an Optional
loop (App None _) = do
return (Fix (NConstant NNull))
loop (App (Field (Union kts) k) v) = do
v' <- loop v
let e0 = do
k' <- Dhall.Map.keys kts
return (k', Nothing)
let e2 = Fix (NBinary NApp (Fix (NSym k)) v')
return (Fix (NAbs (ParamSet e0 False Nothing) e2))
loop (App a b) = do
a' <- loop a
b' <- loop b
@ -488,6 +495,26 @@ dhallToNix e = loop (Dhall.Core.normalize e)
a' <- loop a
b' <- loop b
return (Fix (NBinary NUpdate a' b'))
loop (Field (Union kts) k) =
case Dhall.Map.lookup k kts of
-- If the selected alternative has an associated payload, then we
-- need introduce the partial application through an extra abstraction
-- (here "x").
--
-- This translates `< Foo : T >.Foo` to `x: { Foo }: Foo x`
Just ( Just _ ) -> do
let e0 = do
k' <- Dhall.Map.keys kts
return (k', Nothing)
let e2 = Fix (NBinary NApp (Fix (NSym k)) (Fix (NSym "x")))
return (Fix (NAbs (Param "x") (Fix (NAbs (ParamSet e0 False Nothing) e2))))
_ -> do
let e0 = do
k' <- Dhall.Map.keys kts
return (k', Nothing)
let e2 = Fix (NSym k)
return (Fix (NAbs (ParamSet e0 False Nothing) e2))
loop (Field a b) = do
a' <- loop a
return (Fix (NSelect a' [StaticKey b] Nothing))