commit 80195ffb832639764c04b60940804c2390d74655 Author: Gabriel Gonzalez Date: Fri Jan 20 20:33:49 2017 -0800 Initial commit diff --git a/dhall-nix/LICENSE b/dhall-nix/LICENSE new file mode 100644 index 0000000..f821e29 --- /dev/null +++ b/dhall-nix/LICENSE @@ -0,0 +1,24 @@ +Copyright (c) 2017 Gabriel Gonzalez +All rights reserved. + +Redistribution and use in source and binary forms, with or without modification, +are permitted provided that the following conditions are met: + * Redistributions of source code must retain the above copyright notice, + this list of conditions and the following disclaimer. + * Redistributions in binary form must reproduce the above copyright notice, + this list of conditions and the following disclaimer in the documentation + and/or other materials provided with the distribution. + * Neither the name of Gabriel Gonzalez nor the names of other contributors + may be used to endorse or promote products derived from this software + without specific prior written permission. + +THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS "AS IS" AND +ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE IMPLIED +WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE ARE +DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT OWNER OR CONTRIBUTORS BE LIABLE FOR +ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES +(INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; +LOSS OF USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON +ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT +(INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE OF THIS +SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE. diff --git a/dhall-nix/Setup.hs b/dhall-nix/Setup.hs new file mode 100644 index 0000000..9a994af --- /dev/null +++ b/dhall-nix/Setup.hs @@ -0,0 +1,2 @@ +import Distribution.Simple +main = defaultMain diff --git a/dhall-nix/default.nix b/dhall-nix/default.nix new file mode 100644 index 0000000..c3ff554 --- /dev/null +++ b/dhall-nix/default.nix @@ -0,0 +1,18 @@ +{ mkDerivation, base, containers, data-fix, dhall, hnix +, optparse-generic, stdenv, text, trifecta, vector +}: +mkDerivation { + pname = "dhall-nix"; + version = "1.0.0"; + src = ./.; + isLibrary = true; + isExecutable = true; + libraryHaskellDepends = [ + base containers data-fix dhall hnix text vector + ]; + executableHaskellDepends = [ + base dhall hnix optparse-generic text trifecta + ]; + description = "A configuration language guaranteed to terminate"; + license = stdenv.lib.licenses.bsd3; +} diff --git a/dhall-nix/dhall-nix.cabal b/dhall-nix/dhall-nix.cabal new file mode 100644 index 0000000..40e8631 --- /dev/null +++ b/dhall-nix/dhall-nix.cabal @@ -0,0 +1,43 @@ +Name: dhall-nix +Version: 1.0.0 +Cabal-Version: >=1.8.0.2 +Build-Type: Simple +License: BSD3 +License-File: LICENSE +Copyright: 2017 Gabriel Gonzalez +Author: Gabriel Gonzalez +Maintainer: Gabriel439@gmail.com +Bug-Reports: https://github.com/Gabriel439/Haskell-Dhall-Nix-Library/issues +Synopsis: A configuration language guaranteed to terminate +Description: TODO +Category: Compiler +Source-Repository head + Type: git + Location: https://github.com/Gabriel439/Haskell-Dhall-Nix-Library + +Library + Hs-Source-Dirs: src + Build-Depends: + base >= 4.8.0.0 && < 5, + containers, + data-fix, + dhall, + hnix, + text, + vector + Exposed-Modules: + Dhall.Nix + GHC-Options: -Wall + +Executable dhall-to-nix + Hs-Source-Dirs: exec + Main-Is: Main.hs + Build-Depends: + base >= 4 && < 5 , + dhall , + dhall-nix , + hnix , + optparse-generic >= 1.1.1 && < 1.2, + text , + trifecta + GHC-Options: -Wall diff --git a/dhall-nix/exec/Main.hs b/dhall-nix/exec/Main.hs new file mode 100644 index 0000000..3e10f94 --- /dev/null +++ b/dhall-nix/exec/Main.hs @@ -0,0 +1,44 @@ +{-# LANGUAGE DataKinds #-} +{-# LANGUAGE DeriveGeneric #-} +{-# LANGUAGE OverloadedStrings #-} +{-# LANGUAGE TypeOperators #-} + +module Main where + +import Options.Generic (Generic, ParseRecord, type ()) +import Text.Trifecta.Delta (Delta(..)) + +import qualified Control.Exception +import qualified Data.Text.Lazy.IO +import qualified Dhall.Import +import qualified Dhall.Nix +import qualified Dhall.Parser +import qualified Dhall.TypeCheck +import qualified Nix.Pretty +import qualified Options.Generic + +data Options = Options + { explain :: Bool "Explain error messages in more detail" + } deriving (Generic) + +instance ParseRecord Options + +main :: IO () +main = do +-- options <- Options.Generic.getRecord "Compile Dhall to Nix" + + inText <- Data.Text.Lazy.IO.getContents + + expr <- case Dhall.Parser.exprFromText (Directed "(stdin)" 0 0 0 0) inText of + Left err -> Control.Exception.throwIO err + Right expr -> return expr + + expr' <- Dhall.Import.load expr + case Dhall.TypeCheck.typeOf expr' of + Left err -> Control.Exception.throwIO err + Right _ -> return () + + nix <- case Dhall.Nix.dhallToNix expr' of + Left err -> Control.Exception.throwIO err + Right nix -> return nix + print (Nix.Pretty.prettyNix nix) diff --git a/dhall-nix/release.nix b/dhall-nix/release.nix new file mode 100644 index 0000000..55d8e19 --- /dev/null +++ b/dhall-nix/release.nix @@ -0,0 +1,27 @@ +# You can build this repository using Nix by running: +# +# $ nix-build -A dhall-nix release.nix +# +# You can also open up this repository inside of a Nix shell by running: +# +# $ nix-shell -A dhall-nix.env release.nix +# +# ... and then Nix will supply the correct Haskell development environment for +# you +let + config = { + packageOverrides = pkgs: { + haskellPackages = pkgs.haskellPackages.override { + overrides = haskellPackagesNew: haskellPackagesOld: { + dhall-nix = haskellPackagesNew.callPackage ./default.nix { }; + }; + }; + }; + }; + + pkgs = + import { inherit config; }; + +in + { dhall-nix = pkgs.haskellPackages.dhall-nix; + } diff --git a/dhall-nix/src/Dhall/Nix.hs b/dhall-nix/src/Dhall/Nix.hs new file mode 100644 index 0000000..3ad172b --- /dev/null +++ b/dhall-nix/src/Dhall/Nix.hs @@ -0,0 +1,300 @@ +{-# LANGUAGE DeriveDataTypeable #-} +{-# LANGUAGE OverloadedStrings #-} + +module Dhall.Nix where + +import Control.Exception (Exception) +import Data.Foldable (toList) +import Data.Fix (Fix(..)) +import Data.Typeable (Typeable) +import Dhall.Core (Expr(..), Var(..)) +import Dhall.TypeCheck (X(..)) +import Nix.Atoms (NAtom(..)) +import Nix.Expr + ( Antiquoted(..) + , Binding(..) + , NBinaryOp(..) + , NExprF(..) + , NKeyName(..) + , NString(..) + , Params(..) + , ParamSet(..) + ) + +import qualified Data.Map +import qualified Data.Text.Lazy +import qualified Data.Text.Lazy.Builder +import qualified Data.Vector +import qualified Dhall.Core + +data CompileError + = CannotReferenceShadowedVariable + | NoDoubles + deriving (Show, Typeable) + +instance Exception CompileError + +dhallToNix :: Expr s X -> Either CompileError (Fix NExprF) +dhallToNix e = loop (Dhall.Core.normalize e) + where + loop (Const _) = return (Fix (NSet [])) + loop (Var (V a 0)) = return (Fix (NSym (Data.Text.Lazy.toStrict a))) + loop (Var (V _ _)) = Left CannotReferenceShadowedVariable + loop (Lam a _ c) = do + let a' = Data.Text.Lazy.toStrict a + c' <- loop c + return (Fix (NAbs (Param a') c')) + loop (Pi _ _ _) = return (Fix (NSet [])) + loop (App a b) = do + a' <- loop a + b' <- loop b + return (Fix (NApp a' b')) + loop (Let a _ c d) = do + let a' = Data.Text.Lazy.toStrict a + c' <- loop c + d' <- loop d + return (Fix (NLet [NamedVar [StaticKey a'] c'] d')) + loop (Annot a _) = loop a + loop Bool = return (Fix (NSet [])) + 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 (Fix (NSet [])) + loop (NaturalLit n) = return (Fix (NConstant (NInt (fromIntegral n)))) + loop NaturalFold = do + -- n - 1 + let e0 = Fix (NBinary NMinus "n" (Fix (NConstant (NInt 1)))) + -- naturalFold e0 succ + let e1 = Fix (NApp (Fix (NApp "naturalFold" e0)) "succ") + -- succ (e1 zero) + let e2 = Fix (NApp "succ" (Fix (NApp e1 "zero"))) + -- n == 0 + let e3 = Fix (NBinary NLte "n" (Fix (NConstant (NInt 0)))) + -- succ : zero : if e3 then zero else e2 + let e4 = Fix (NAbs "succ" (Fix (NAbs "zero" (Fix (NIf e3 "zero" e2))))) + -- n : t : e4 + let e5 = Fix (NAbs "n" (Fix (NAbs "t" e4))) + -- let naturalFold = e5 in naturalFold + return (Fix (NLet [NamedVar [StaticKey "naturalFold"] e5] "naturalFold")) + loop NaturalBuild = do + -- n + 1 + let e0 = Fix (NBinary NPlus "n" (Fix (NConstant (NInt 1)))) + -- k {} (n : e0) + let e1 = Fix (NApp (Fix (NApp "k" (Fix (NSet [])))) (Fix (NAbs "n" e0))) + -- k : e1 0 + return (Fix (NAbs "k" (Fix (NApp e1 (Fix (NConstant (NInt 0))))))) + loop NaturalIsZero = do + -- n == 0 + let e0 = Fix (NBinary NEq "n" (Fix (NConstant (NInt 0)))) + -- n : e0 + return (Fix (NAbs "n" e0)) + loop NaturalEven = do + -- n - 2 + let e0 = Fix (NBinary NMinus "n" (Fix (NConstant (NInt 2)))) + -- naturalEven e0 + let e1 = Fix (NApp "naturalEven" e0) + -- n != 1 + let e2 = Fix (NBinary NNEq "n" (Fix (NConstant (NInt 1)))) + -- n == 0 + let e3 = Fix (NBinary NEq "n" (Fix (NConstant (NInt 0)))) + -- e3 || (e2 && e1) + let e4 = Fix (NBinary NOr e3 (Fix (NBinary NAnd e2 e1))) + -- naturalEvent = n : e4 + let e5 = NamedVar [StaticKey "naturalEven"] (Fix (NAbs "n" e4)) + -- 0 - n + let e6 = Fix (NBinary NMinus (Fix (NConstant (NInt 0))) "n") + -- n <= 0 + let e7 = Fix (NBinary NLte "n" (Fix (NConstant (NInt 0)))) + -- n : naturalEven (if e7 then e6 else n) + let e8 = Fix (NAbs "n" (Fix (NApp "naturalEven" (Fix (NIf e7 e6 "n"))))) + -- let e5 in e8 + return (Fix (NLet [e5] e8)) + loop NaturalOdd = do + -- n - 2 + let e0 = Fix (NBinary NMinus "n" (Fix (NConstant (NInt 2)))) + -- naturalOdd e0 + let e1 = Fix (NApp "naturalOdd" e0) + -- n != 0 + let e2 = Fix (NBinary NNEq "n" (Fix (NConstant (NInt 0)))) + -- n == 1 + let e3 = Fix (NBinary NEq "n" (Fix (NConstant (NInt 1)))) + -- e3 || (e2 && e1) + let e4 = Fix (NBinary NOr e3 (Fix (NBinary NAnd e2 e1))) + -- naturalOddt = n : e4 + let e5 = NamedVar [StaticKey "naturalOdd"] (Fix (NAbs "n" e4)) + -- 0 - n + let e6 = Fix (NBinary NMinus (Fix (NConstant (NInt 0))) "n") + -- n <= 0 + let e7 = Fix (NBinary NLte "n" (Fix (NConstant (NInt 0)))) + -- n : naturalOdd (if e7 then e6 else n) + let e8 = Fix (NAbs "n" (Fix (NApp "naturalOdd" (Fix (NIf e7 e6 "n"))))) + -- let e5 in e8 + return (Fix (NLet [e5] e8)) + 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 (Fix (NSet [])) + loop (IntegerLit n) = return (Fix (NConstant (NInt (fromIntegral n)))) + loop Double = return (Fix (NSet [])) + loop (DoubleLit _) = Left NoDoubles + loop Text = return (Fix (NSet [])) + loop (TextLit a) = do + let a' = Data.Text.Lazy.toStrict (Data.Text.Lazy.Builder.toLazyText a) + return (Fix (NStr (DoubleQuoted [Plain a']))) + loop (TextAppend a b) = do + a' <- loop a + b' <- loop b + return (Fix (NBinary NPlus a' b')) + loop List = return (Fix (NAbs "t" (Fix (NSet [])))) + loop (ListLit _ bs) = do + bs' <- mapM loop (toList bs) + return (Fix (NList bs')) + loop ListBuild = do + -- k {} + let e0 = Fix (NApp "k" (Fix (NSet []))) + -- [x] ++ xs + let e1 = Fix (NBinary NConcat (Fix (NList ["x"])) "xs") + -- e0 (x : xs : e1) + let e2 = Fix (NApp e0 (Fix (NAbs "x" (Fix (NAbs "xs" e1))))) + -- k : e2 [] + let e3 = Fix (NAbs "k" (Fix (NApp e2 (Fix (NList []))))) + -- t : e3 + return (Fix (NAbs "t" e3)) + loop ListFold = do + -- f (cons y ys) + let e0 = Fix (NApp "f" (Fix (NApp (Fix (NApp "cons" "y")) "ys"))) + -- f : y : ys : e0 + let e1 = Fix (NAbs "f" (Fix (NAbs "y" (Fix (NAbs "ys" e0))))) + -- "builtins.foldl" e1 + let e2 = Fix (NApp "builtins.foldl'" e1) + -- e2 (ys : ys) xs + let e3 = Fix (NApp (Fix (NApp e2 (Fix (NAbs "ys" "ys")))) "xs") + -- xs : t : cons : e3 + let e4 = Fix (NAbs "xs" (Fix (NAbs "t" (Fix (NAbs "cons" e3))))) + -- t : e4 + return (Fix (NAbs "t" e4)) + loop ListLength = return (Fix (NAbs "t" "builtins.length")) + loop ListHead = do + -- builtins.head xs + let e0 = Fix (NApp "builtins.head" "xs") + -- xs == [] + let e1 = Fix (NBinary NEq "xs" (Fix (NList []))) + -- xs : if e1 then null else e0 + let e2 = Fix (NAbs "xs" (Fix (NIf e1 (Fix (NConstant NNull)) e0))) + -- t : e2 + return (Fix (NAbs "t" e2)) + loop ListLast = do + -- builtins.length xs + let e0 = Fix (NApp "builtins.length" "xs") + -- e0 - 1 + let e1 = Fix (NBinary NMinus e0 (Fix (NConstant (NInt 1)))) + -- builtins.elemAt xs e1 + let e2 = Fix (NApp (Fix (NApp "builtins.elemAt" "xs")) e1) + -- x == [] + let e3 = Fix (NBinary NEq "xs" (Fix (NList []))) + -- xs : if e3 then null else e2 + let e4 = Fix (NAbs "xs" (Fix (NIf e3 (Fix (NConstant NNull)) e2))) + -- t : e4 + return (Fix (NAbs "t" e4)) + loop ListIndexed = do + -- builtins.length xs + let e0 = Fix (NApp "builtins.length" "xs") + -- builtins.elemAt xs i + let e1 = Fix (NApp (Fix (NApp "builtins.elemAt" "xs")) "i") + -- { index = i; value = e1; } + let e2 = + [ NamedVar [StaticKey "index"] "i" + , NamedVar [StaticKey "value"] e1 + ] + -- builtins.genList (i : e2) + let e3 = Fix (NApp "builtins.genList" (Fix (NAbs "i" (Fix (NSet e2))))) + -- t : xs : e3 + return (Fix (NAbs "t" (Fix (NAbs "xs" (Fix (NApp e3 e0)))))) + loop ListReverse = do + -- n - i + let e0 = Fix (NBinary NMinus "n" "i") + -- n - 1 + let e1 = Fix (NBinary NMinus e0 (Fix (NConstant (NInt 1)))) + -- builtins.elemAt xs e1 + let e2 = Fix (NApp (Fix (NApp "builtins.elemAt" "xs")) e1) + -- builtins.genList (i : e2) + let e3 = Fix (NApp "builtins.genList" (Fix (NAbs "i" e2))) + -- e3 n + let e4 = Fix (NApp e3 "n") + -- builtins.length xs + let e5 = Fix (NApp "builtins.length" "xs") + -- xs : let n = e5 in e4 + let e6 = Fix (NAbs "xs" (Fix (NLet [NamedVar [StaticKey "n"] e5] e4))) + -- t : e6 + return (Fix (NAbs "t" e6)) + loop Optional = return (Fix (NAbs "t" (Fix (NSet [])))) + loop (OptionalLit _ b) = + if Data.Vector.null b + then return (Fix (NConstant NNull)) + else dhallToNix (Data.Vector.head b) + loop OptionalFold = do + -- x == null + let e0 = Fix (NBinary NEq "x" (Fix (NConstant NNull))) + -- if e0 then nothing else just x + let e1 = Fix (NIf e0 "nothing" (Fix (NApp "just" "x"))) + -- t : just : nothing : e1 + let e2 = Fix (NAbs "t" (Fix (NAbs "just" (Fix (NAbs "nothing" e1))))) + -- t : x : e2 + return (Fix (NAbs "t" (Fix (NAbs "x" e2)))) + loop (Record _) = return (Fix (NSet [])) + loop (RecordLit a) = do + a' <- traverse dhallToNix a + let a'' = do + (k, v) <- Data.Map.toAscList a' + let k' = Data.Text.Lazy.toStrict k + return (NamedVar [StaticKey k'] v) + return (Fix (NSet a'')) + loop (Union _) = return (Fix (NSet [])) + loop (UnionLit k v kts) = do + v' <- dhallToNix v + let k' = Data.Text.Lazy.toStrict k + let e0 = do + k'' <- k : toList (Data.Map.keysSet kts) + return (Data.Text.Lazy.toStrict k'', Nothing) + let e1 = Data.Map.fromAscList e0 + let e2 = Fix (NApp (Fix (NSym k')) v') + return (Fix (NAbs (ParamSet (FixedParamSet e1) Nothing) e2)) + loop (Combine a b) = do + a' <- dhallToNix a + b' <- dhallToNix b + -- TODO: Do recursive update + return (Fix (NBinary NUpdate a' b')) + loop (Merge a b _) = do + a' <- dhallToNix a + b' <- dhallToNix b + return (Fix (NApp b' a')) + loop (Field a b) = do + a' <- dhallToNix a + let b' = Data.Text.Lazy.toStrict b + return (Fix (NSelect a' [StaticKey b'] Nothing)) + loop (Note _ b) = loop b + loop (Embed (X x)) = x