{-# LANGUAGE DeriveDataTypeable #-}
{-# LANGUAGE OverloadedStrings #-}
{-# LANGUAGE OverloadedLists #-}
{-# LANGUAGE RecordWildCards #-}
{-# LANGUAGE QuasiQuotes #-}
{-# LANGUAGE TypeFamilies #-}
module Dhall.Nix (
dhallToNix
, CompileError(..)
) where
import Control.Exception (Exception)
import Data.Foldable (toList)
import Data.Fix (Fix(..))
import Data.Text (Text)
import Data.Traversable (for)
import Data.Typeable (Typeable)
import Data.Void (Void, absurd)
import Dhall.Core
( Binding(..)
, Chunks(..)
, DhallDouble(..)
, Expr(..)
, MultiLet(..)
, PreferAnnotation(..)
, Var(..)
)
import Lens.Family (toListOf)
import Nix.Atoms (NAtom(..))
import Nix.Expr
( Antiquoted(..)
, Binding(..)
, NBinaryOp(..)
, NExprF(..)
, NKeyName(..)
, NRecordType(..)
, NString(..)
, Params(..)
, (@@)
, (==>)
, ($+)
)
import qualified Data.Text
import qualified Dhall.Core
import qualified Dhall.Map
import qualified Dhall.Optics
import qualified NeatInterpolation
import qualified Nix
data CompileError
= CannotReferenceShadowedVariable Var
| CannotProjectByType
deriving (Typeable)
instance Show CompileError where
show (CannotReferenceShadowedVariable v) =
Data.Text.unpack [NeatInterpolation.text|
$_ERROR: Cannot reference shadowed variable
Explanation: Whenever you introduce two variables of the same name, the latter
variable takes precedence:
This ❰x❱ ...
⇩
┌───────────────────────────────┐
│ λ(x : Text) → λ(x : Text) → x │
└───────────────────────────────┘
⇧
... refers to this ❰x❱
The former variable is "shadowed":
┌───────────────────────────────┐
│ λ(x : Text) → λ(x : Text) → x │
└───────────────────────────────┘
⇧
This ❰x❱ is shadowed
... and Dhall lets you reference shadowed variables using the ❰@❱ notation:
This ❰x❱ ...
⇩
┌─────────────────────────────────┐
│ λ(x : Text) → λ(x : Text) → x@1 │
└─────────────────────────────────┘
⇧
... now refers to this ❰x❱
However, the Nix language does not let you reference shadowed variables and
there is nothing analogous to ❰@❱ in Nix
Your code contains the following expression:
↳ $txt
... which references a shadowed variable and therefore cannot be translated to
Nix
|]
where
txt = Dhall.Core.pretty v
show CannotProjectByType =
Data.Text.unpack [NeatInterpolation.text|
$_ERROR: Cannot project by type
The ❰dhall-to-nix❱ compiler does not support projecting out a subset of a record
by the expected type (i.e. ❰someRecord.(someType)❱
|]
_ERROR :: Data.Text.Text
_ERROR = "\ESC[1;31mError\ESC[0m"
instance Exception CompileError
dhallToNix :: Expr s Void -> Either CompileError (Fix NExprF)
dhallToNix e =
loop (rewriteShadowed (Dhall.Core.normalize e))
where
untranslatable = Fix (NSet NNonRecursive [])
maximumDepth :: Var -> Expr s Void -> Maybe Int
maximumDepth v@(V x n) (Lam x' a b)
| x == x' =
max (maximumDepth v a) (fmap (+ 1) (maximumDepth (V x (n + 1)) b))
maximumDepth v@(V x n) (Pi x' a b)
| x == x' =
max (maximumDepth v a) (fmap (+ 1) (maximumDepth (V x (n + 1)) b))
maximumDepth (V x n) (Let (Binding { variable = x' }) a)
| x == x' = fmap (+ 1) (maximumDepth (V x (n + 1)) a)
maximumDepth v (Var v')
| v == v' = Just 0
maximumDepth v expression =
foldr max Nothing
(map
(maximumDepth v)
(toListOf Dhall.Core.subExpressions expression)
)
rename :: (Text, Expr s Void) -> Maybe (Text, Expr s Void)
rename (x, expression) =
case maximumDepth (V x 0) expression of
Nothing ->
Nothing
Just 0 ->
Nothing
Just n ->
Just
( x'
, Dhall.Core.subst (V x 0) (Var (V x' 0)) (Dhall.Core.shift 1 (V x' 0) expression)
)
where
x' = x <> Data.Text.pack (show n)
renameShadowed :: Expr s Void -> Maybe (Expr s Void)
renameShadowed (Lam x a b) = do
(x', b') <- rename (x, b)
return (Lam x' a b')
renameShadowed (Pi x a b) = do
(x', b') <- rename (x, b)
return (Pi x' a b')
renameShadowed (Let Binding{ variable = x, .. } a) = do
(x' , a') <- rename (x, a)
return (Let Binding{ variable = x', .. } a')
renameShadowed _ = do
Nothing
rewriteShadowed =
Dhall.Optics.rewriteOf Dhall.Core.subExpressions renameShadowed
loop (Const _) = return untranslatable
loop (Var (V a 0)) = return (Fix (NSym a))
loop (Var a ) = Left (CannotReferenceShadowedVariable a)
loop (Lam a _ c) = do
c' <- loop c
return (Fix (NAbs (Param a) c'))
loop (Pi _ _ _) = return untranslatable
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
return (Fix (NBinary NApp a' b'))
loop (Let a0 b0) = do
let MultiLet as b = Dhall.Core.multiLet a0 b0
as' <- for as $ \a -> do
val <- loop $ Dhall.Core.value a
pure $ NamedVar [StaticKey $ Dhall.Core.variable a] val Nix.nullPos
b' <- loop b
return (Fix (NLet (toList as') b'))
loop (Annot a _) = loop a
loop Bool = return untranslatable
loop (BoolLit b) = return (Fix (NConstant (NBool b)))
loop (BoolAnd a b) = do
a' <- loop a
b' <- loop b
return (Fix (NBinary NAnd a' b'))
loop (BoolOr a b) = do
a' <- loop a
b' <- loop b
return (Fix (NBinary NOr a' b'))
loop (BoolEQ a b) = do
a' <- loop a
b' <- loop b
return (Fix (NBinary NEq a' b'))
loop (BoolNE a b) = do
a' <- loop a
b' <- loop b
return (Fix (NBinary NNEq a' b'))
loop (BoolIf a b c) = do
a' <- loop a
b' <- loop b
c' <- loop c
return (Fix (NIf a' b' c'))
loop Natural = return untranslatable
loop (NaturalLit n) = return (Fix (NConstant (NInt (fromIntegral n))))
loop NaturalFold = do
let e0 = Fix (NBinary NMinus "n" (Fix (NConstant (NInt 1))))
let e1 = Fix (NBinary NApp (Fix (NBinary NApp (Fix (NBinary NApp "naturalFold" e0)) "t")) "succ")
let e2 = Fix (NBinary NApp "succ" (Fix (NBinary NApp e1 "zero")))
let e3 = Fix (NBinary NLte "n" (Fix (NConstant (NInt 0))))
let e4 = Fix (NAbs "succ" (Fix (NAbs "zero" (Fix (NIf e3 "zero" e2)))))
let e5 = Fix (NAbs "n" (Fix (NAbs "t" e4)))
return (Fix (NLet [NamedVar ["naturalFold"] e5 Nix.nullPos] "naturalFold"))
loop NaturalBuild = do
let e0 = Fix (NBinary NPlus "n" (Fix (NConstant (NInt 1))))
let e1 = Fix (NBinary NApp (Fix (NBinary NApp "k" untranslatable)) (Fix (NAbs "n" e0)))
return (Fix (NAbs "k" (Fix (NBinary NApp e1 (Fix (NConstant (NInt 0)))))))
loop NaturalIsZero = do
let e0 = Fix (NBinary NEq "n" (Fix (NConstant (NInt 0))))
return (Fix (NAbs "n" e0))
loop NaturalEven = do
let e0 = Fix (NBinary NMinus "n" (Fix (NConstant (NInt 2))))
let e1 = Fix (NBinary NApp "naturalEven" e0)
let e2 = Fix (NBinary NNEq "n" (Fix (NConstant (NInt 1))))
let e3 = Fix (NBinary NEq "n" (Fix (NConstant (NInt 0))))
let e4 = Fix (NBinary NOr e3 (Fix (NBinary NAnd e2 e1)))
let e5 = NamedVar ["naturalEven"] (Fix (NAbs "n" e4)) Nix.nullPos
let e6 = Fix (NBinary NMinus (Fix (NConstant (NInt 0))) "n")
let e7 = Fix (NBinary NLte "n" (Fix (NConstant (NInt 0))))
let e8 = Fix (NAbs "n" (Fix (NBinary NApp "naturalEven" (Fix (NIf e7 e6 "n")))))
return (Fix (NLet [e5] e8))
loop NaturalOdd = do
let e0 = Fix (NBinary NMinus "n" (Fix (NConstant (NInt 2))))
let e1 = Fix (NBinary NApp "naturalOdd" e0)
let e2 = Fix (NBinary NNEq "n" (Fix (NConstant (NInt 0))))
let e3 = Fix (NBinary NEq "n" (Fix (NConstant (NInt 1))))
let e4 = Fix (NBinary NOr e3 (Fix (NBinary NAnd e2 e1)))
let e5 = NamedVar ["naturalOdd"] (Fix (NAbs "n" e4)) Nix.nullPos
let e6 = Fix (NBinary NMinus (Fix (NConstant (NInt 0))) "n")
let e7 = Fix (NBinary NLte "n" (Fix (NConstant (NInt 0))))
let e8 = Fix (NAbs "n" (Fix (NBinary NApp "naturalOdd" (Fix (NIf e7 e6 "n")))))
return (Fix (NLet [e5] e8))
loop NaturalShow = do
return "toString"
loop NaturalSubtract = do
let e0 = NamedVar ["z"] (Fix (NBinary NMinus "y" "x")) Nix.nullPos
let e1 = Fix (NBinary NLt "z" (Fix (NConstant (NInt 0))))
let e2 = Fix (NConstant (NInt 0))
let e3 = "z"
let e4 = Fix (NIf e1 e2 e3)
let e5 = Fix (NLet [e0] e4)
return (Fix (NAbs "x" (Fix (NAbs "y" e5))))
loop NaturalToInteger = do
return (Fix (NAbs "n" "n"))
loop (NaturalPlus a b) = do
a' <- loop a
b' <- loop b
return (Fix (NBinary NPlus a' b'))
loop (NaturalTimes a b) = do
a' <- loop a
b' <- loop b
return (Fix (NBinary NMult a' b'))
loop Integer = return untranslatable
loop (IntegerLit n) = return (Fix (NConstant (NInt (fromIntegral n))))
loop IntegerClamp = do
let e0 = Fix (NConstant (NInt 0))
let e1 = Fix (NBinary NLte (Fix (NConstant (NInt 0))) "x")
let e2 = Fix (NAbs "x" (Fix (NIf e1 "x" e0)))
return e2
loop IntegerNegate = do
let e0 = Fix (NBinary NMinus (Fix (NConstant (NInt 0))) "x")
let e1 = Fix (NAbs "x" e0)
return e1
loop IntegerShow = do
let e0 = Fix (NBinary NApp "toString" "x")
let e1 = Fix (NBinary NPlus (Fix (NStr "+")) e0)
let e2 = Fix (NBinary NLte (Fix (NConstant (NInt 0))) "x")
let e3 = Fix (NAbs "x" (Fix (NIf e2 e1 e0)))
return e3
loop IntegerToDouble = do
return (Fix (NAbs "x" "x"))
loop Double = return untranslatable
loop (DoubleLit (DhallDouble n)) = return (Fix (NConstant (NFloat (realToFrac n))))
loop DoubleShow = do
return "toString"
loop Text = return untranslatable
loop (TextLit (Chunks abs_ c)) = do
let process (a, b) = do
b' <- loop b
return [Plain a, Antiquoted b']
abs' <- mapM process abs_
let chunks = concat abs' ++ [Plain c]
return (Fix (NStr (DoubleQuoted chunks)))
loop (TextAppend a b) = do
a' <- loop a
b' <- loop b
return (Fix (NBinary NPlus a' b'))
loop TextShow = do
let from =
Nix.mkList
[ Nix.mkStr "\""
, Nix.mkStr "$"
, Nix.mkStr "\\"
, Nix.mkStr "\n"
, Nix.mkStr "\r"
, Nix.mkStr "\t"
]
let to =
Nix.mkList
[ Nix.mkStr "\\\""
, Nix.mkStr "\\u0024"
, Nix.mkStr "\\\\"
, Nix.mkStr "\\n"
, Nix.mkStr "\\r"
, Nix.mkStr "\\t"
]
let replaced = "builtins.replaceStrings" @@ from @@ to @@ "t"
let quoted = Nix.mkStr "\"" $+ replaced $+ Nix.mkStr "\""
return ("t" ==> quoted)
loop List = return (Fix (NAbs "t" untranslatable))
loop (ListAppend a b) = do
a' <- loop a
b' <- loop b
return (Fix (NBinary NConcat a' b'))
loop (ListLit _ bs) = do
bs' <- mapM loop (toList bs)
return (Fix (NList bs'))
loop ListBuild = do
let e0 = Fix (NBinary NApp "k" untranslatable)
let e1 = Fix (NBinary NConcat (Fix (NList ["x"])) "xs")
let e2 = Fix (NBinary NApp e0 (Fix (NAbs "x" (Fix (NAbs "xs" e1)))))
let e3 = Fix (NAbs "k" (Fix (NBinary NApp e2 (Fix (NList [])))))
return (Fix (NAbs "t" e3))
loop ListFold = do
let e0 = Fix (NBinary NApp "f" (Fix (NBinary NApp (Fix (NBinary NApp "cons" "y")) "ys")))
let e1 = Fix (NAbs "f" (Fix (NAbs "y" (Fix (NAbs "ys" e0)))))
let e2 = Fix (NBinary NApp "builtins.foldl'" e1)
let e3 = Fix (NBinary NApp (Fix (NBinary NApp e2 (Fix (NAbs "ys" "ys")))) "xs")
let e4 = Fix (NAbs "xs" (Fix (NAbs "t" (Fix (NAbs "cons" e3)))))
return (Fix (NAbs "t" e4))
loop ListLength = return (Fix (NAbs "t" "builtins.length"))
loop ListHead = do
let e0 = Fix (NBinary NApp "builtins.head" "xs")
let e1 = Fix (NBinary NEq "xs" (Fix (NList [])))
let e2 = Fix (NAbs "xs" (Fix (NIf e1 (Fix (NConstant NNull)) e0)))
return (Fix (NAbs "t" e2))
loop ListLast = do
let e0 = Fix (NBinary NApp "builtins.length" "xs")
let e1 = Fix (NBinary NMinus e0 (Fix (NConstant (NInt 1))))
let e2 = Fix (NBinary NApp (Fix (NBinary NApp "builtins.elemAt" "xs")) e1)
let e3 = Fix (NBinary NEq "xs" (Fix (NList [])))
let e4 = Fix (NAbs "xs" (Fix (NIf e3 (Fix (NConstant NNull)) e2)))
return (Fix (NAbs "t" e4))
loop ListIndexed = do
let e0 = Fix (NBinary NApp "builtins.length" "xs")
let e1 = Fix (NBinary NApp (Fix (NBinary NApp "builtins.elemAt" "xs")) "i")
let e2 =
[ NamedVar ["index"] "i" Nix.nullPos
, NamedVar ["value"] e1 Nix.nullPos
]
let e3 = Fix (NBinary NApp "builtins.genList" (Fix (NAbs "i" (Fix (NSet NNonRecursive e2)))))
return (Fix (NAbs "t" (Fix (NAbs "xs" (Fix (NBinary NApp e3 e0))))))
loop ListReverse = do
let e0 = Fix (NBinary NMinus "n" "i")
let e1 = Fix (NBinary NMinus e0 (Fix (NConstant (NInt 1))))
let e2 = Fix (NBinary NApp (Fix (NBinary NApp "builtins.elemAt" "xs")) e1)
let e3 = Fix (NBinary NApp "builtins.genList" (Fix (NAbs "i" e2)))
let e4 = Fix (NBinary NApp e3 "n")
let e5 = Fix (NBinary NApp "builtins.length" "xs")
let e6 = Fix (NAbs "xs" (Fix (NLet [NamedVar ["n"] e5 Nix.nullPos] e4)))
return (Fix (NAbs "t" e6))
loop Optional = return (Fix (NAbs "t" untranslatable))
loop (Some a) = loop a
loop None = return (Fix (NConstant NNull))
loop (Record _) = return untranslatable
loop (RecordLit a) = do
a' <- traverse loop a
let a'' = do
(k, v) <- Dhall.Map.toList a'
return (NamedVar [StaticKey k] v Nix.nullPos)
return (Fix (NSet NNonRecursive a''))
loop (Union _) = return untranslatable
loop (Combine _ a b) = do
a' <- loop a
b' <- loop b
let e0 = Fix (NBinary NApp (Fix (NBinary NApp "map" "toKeyVals")) "ks")
let e1 = Fix (NBinary NApp "builtins.concatLists" e0)
let e2 = Fix (NBinary NApp "builtins.listToAttrs" e1)
let defL = Fix (NBinary NApp (Fix (NBinary NApp "builtins.hasAttr" "k")) "kvsL")
let defR = Fix (NBinary NApp (Fix (NBinary NApp "builtins.hasAttr" "k")) "kvsR")
let valL = Fix (NBinary NApp (Fix (NBinary NApp "builtins.getAttr" "k")) "kvsL")
let valR = Fix (NBinary NApp (Fix (NBinary NApp "builtins.getAttr" "k")) "kvsR")
let empty_ = Fix (NList [])
let toNameValue v =
let bindings =
[ NamedVar ["name" ] "k" Nix.nullPos
, NamedVar ["value"] v Nix.nullPos
]
in Fix (NList [Fix (NSet NNonRecursive bindings)])
let e3 = Fix (NBinary NApp (Fix (NBinary NApp "combine" valL)) valR)
let e4 = Fix (NBinary NApp "builtins.isAttrs" valL)
let e5 = Fix (NBinary NApp "builtins.isAttrs" valR)
let e6 = Fix (NBinary NAnd e4 e5)
let e7 = Fix (NIf e6 (toNameValue e3) (toNameValue valR))
let e8 = Fix (NIf defR e7 (toNameValue valL))
let e9 = Fix (NIf defR (toNameValue valR) empty_)
let toKeyVals = Fix (NAbs "k" (Fix (NIf defL e8 e9)))
let ksL = Fix (NBinary NApp "builtins.attrNames" "kvsL")
let ksR = Fix (NBinary NApp "builtins.attrNames" "kvsR")
let ks = Fix (NBinary NConcat ksL ksR)
let e10 =
[ NamedVar ["ks" ] ks Nix.nullPos
, NamedVar ["toKeyVals"] toKeyVals Nix.nullPos
]
let combine = Fix (NAbs "kvsL" (Fix (NAbs "kvsR" (Fix (NLet e10 e2)))))
let e11 = Fix (NBinary NApp (Fix (NBinary NApp "combine" a')) b')
return (Fix (NLet [NamedVar ["combine"] combine Nix.nullPos] e11))
loop (CombineTypes _ _) = return untranslatable
loop (Merge a b _) = do
a' <- loop a
b' <- loop b
return (Fix (NBinary NApp b' a'))
loop (ToMap a _) = do
a' <- loop a
let ks = Fix (NBinary NApp "builtins.attrNames" "kvs")
let v = Fix (NBinary NApp (Fix (NBinary NApp "builtins.getAttr" "k")) "kvs")
let setBindings =
[ NamedVar [StaticKey "mapKey"] "k" Nix.nullPos
, NamedVar [StaticKey "mapValue"] v Nix.nullPos
]
let map_ = Fix (NBinary NApp "map" (Fix (NAbs "k" (Fix (NSet NNonRecursive setBindings)))))
let toMap = Fix (NAbs "kvs" (Fix (NBinary NApp map_ ks)))
return (Fix (NBinary NApp toMap a'))
loop (Prefer _ b c) = do
b' <- loop b
c' <- loop c
return (Fix (NBinary NUpdate b' c'))
loop (RecordCompletion a b) = do
loop (Annot (Prefer PreferFromCompletion (Field a "default") b) (Field a "Type"))
loop (Field (Union kts) k) =
case Dhall.Map.lookup k kts of
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))
loop (Project a (Left b)) = do
a' <- loop a
let b' = fmap StaticKey (toList b)
return (Fix (NSet NNonRecursive [Inherit (Just a') b' Nix.nullPos]))
loop (Project _ (Right _)) = do
Left CannotProjectByType
loop (Assert _) = do
return untranslatable
loop (Equivalent _ _) = do
return untranslatable
loop a@With{} = do
loop (Dhall.Core.desugarWith a)
loop (ImportAlt a _) = loop a
loop (Note _ b) = loop b
loop (Embed x) = absurd x