Add a `pkgs.dhallToNix` utility #22193

Merged
merged 1 commit into from Jan 27, 2017

Projects

None yet

3 participants

@Gabriel439

This adds a dhallToNix utility which compiles expressions from the Dhall
configuration language to Nix using Nix's support for "import from derivation".

Motivation for this change

The main motivation of this utility is to allow users to carve out small typed
subsets of Nix projects. Everything in the Dhall language (except Doubles)
can be translated to Nix in this way, including functions.

Things done
  • Tested using sandboxing
    (nix.useSandbox on NixOS,
    or option build-use-sandbox in nix.conf
    on non-NixOS)
  • Built on platform(s)
    • NixOS
    • macOS
    • Linux
  • Tested compilation of all pkgs that depend on this change using nix-shell -p nox --run "nox-review wip"
  • Tested execution of all binary files (usually in ./result/bin/)
  • Fits CONTRIBUTING.md.

I also tested by running nix-build on the following file:

let
  pkgs = import ../nixpkgs { };

  inherit (pkgs) dhallToNix;

  testConst = dhallToNix "Type";
  testLam = dhallToNix "λ(x : Bool) → x";
  testPi = dhallToNix "Bool → Bool";
  testApp = dhallToNix "λ(f : Bool → Bool) → λ(x : Bool) → f x";
  testLet = dhallToNix "λ(b : Bool) → let x = b in x";
  testAnnot = dhallToNix "True : Bool";
  testBool = dhallToNix "Bool";
  testBoolLit = dhallToNix "True";
  testBoolAnd = dhallToNix "λ(l : Bool) → λ(r : Bool) → l && r";
  testBoolOr = dhallToNix "λ(l : Bool) → λ(r : Bool) → l || r";
  testBoolEQ = dhallToNix "λ(l : Bool) → λ(r : Bool) → l == r";
  testBoolNE = dhallToNix "λ(l : Bool) → λ(r : Bool) → l != r";
  testBoolIf = dhallToNix "λ(x : Bool) → if x then True else False";
  testNatural = dhallToNix "Natural";
  testNaturalLit = dhallToNix "+123";
  testNaturalFold = dhallToNix ''
      λ(x : Natural)
    → Natural/fold x Natural (λ(n : Natural) → +2 + n) +0
  '';
  testNaturalBuild = dhallToNix ''
      λ(b : Bool)
    → Natural/build
      ( λ(natural : Type)
      → λ(succ : natural → natural)
      → λ(zero : natural)
      → if b then succ zero else zero
      )
  '';
  testNaturalIsZero = dhallToNix "Natural/isZero";
  testNaturalEven = dhallToNix "Natural/even";
  testNaturalOdd = dhallToNix "Natural/odd";
  testNaturalPlus = dhallToNix "λ(x : Natural) → λ(y : Natural) → x + y";
  testNaturalTimes = dhallToNix "λ(x : Natural) → λ(y : Natural) → x * y";
  testInteger = dhallToNix "Integer";
  testIntegerLit = dhallToNix "123";
  testDouble = dhallToNix "Double";
  testTextLit = dhallToNix ''"ABC"'';
  testTextAppend = dhallToNix "λ(x : Text) → λ(y : Text) → x ++ y";
  testList = dhallToNix "List Integer";
  testListLit = dhallToNix "[1, 2, 3] : List Integer";
  testListBuild = dhallToNix ''
      λ(b : Bool)
    → List/build
      Integer
      ( λ(list : Type)
      → λ(cons : Integer → list → list)
      → λ(nil : list)
      → if b then cons 1 (cons 2 (cons 3 nil)) else nil
      )
  '';
  testListFold = dhallToNix ''
      List/fold
      Natural
      ([+1, +2, +3] : List Natural)
      Natural
  '';
  testListLength = dhallToNix "List/length Integer";
  testListHead = dhallToNix "List/head Integer";
  testListLast = dhallToNix "List/last Integer";
  testListIndexed = dhallToNix "List/indexed Integer";
  testListReverse = dhallToNix "List/reverse Integer";
  testOptional = dhallToNix "Optional";
  testOptionalLit = dhallToNix ''
      λ(b : Bool)
    → if b
      then ([0] : Optional Integer)
      else ([]  : Optional Integer)
  '';
  testOptionalFold = dhallToNix ''
    Optional/fold
    Integer
    ([1] : Optional Integer)
    Integer
  '';
  testRecord = dhallToNix "{}";
  testRecordLit = dhallToNix "{ foo = 1, bar = True}";
  testUnion = dhallToNix "< Left : Natural | Right : Bool >";
  testUnionLit = dhallToNix "< Left = +2 | Right : Bool >";
  testCombine = dhallToNix ''
      λ(x : { foo : { bar : Text } })
    → λ(y : { foo : { baz : Bool } })
    → x ∧ y
  '';
  testMerge = dhallToNix ''
      λ(r : < Left : Natural | Right : Bool >)
    → merge
      { Left = Natural/isZero, Right = λ(b : Bool) → b }
      r : Bool
  '';
  testField = dhallToNix "λ(r : { foo : Bool, bar : Text }) → r.foo";

in
  assert (testConst == {});
  assert (testLam true == true);
  assert (testPi == {});
  assert (testApp (b : b) true == true);
  assert (testLet true == true);
  assert (testAnnot == true);
  assert (testBool == {});
  assert (testBoolLit == true);
  assert (testBoolAnd true false == false);
  assert (testBoolOr true false == true);
  assert (testBoolEQ true false == false);
  assert (testBoolNE true false == true);
  assert (testBoolIf true == true);
  assert (testNatural == {});
  assert (testNaturalLit == 123);
  assert (testNaturalFold 123 == 246);
  assert (testNaturalBuild true == 1);
  assert (testNaturalBuild false == 0);
  assert (testNaturalIsZero 0 == true);
  assert (testNaturalIsZero 3 == false);
  assert (testNaturalEven 2 == true);
  assert (testNaturalEven 3 == false);
  assert (testNaturalOdd 2 == false);
  assert (testNaturalOdd 3 == true);
  assert (testNaturalPlus 2 3 == 5);
  assert (testNaturalTimes 2 3 == 6);
  assert (testInteger == {});
  assert (testIntegerLit == 123);
  assert (testDouble == {});
  assert (testTextLit == "ABC");
  assert (testTextAppend "ABC" "DEF" == "ABCDEF");
  assert (testList == {});
  assert (testListLit == [1 2 3]);
  assert (testListBuild true == [1 2 3]);
  assert (testListFold (x : y: x + y) 0 == 6);
  assert (testListLength [1 2 3] == 3);
  assert (testListLength [] == 0);
  assert (testListHead [1 2 3] == 1);
  assert (testListHead [] == null);
  assert (testListLast [1 2 3] == 3);
  assert (testListLast [] == null);
  assert (testListIndexed [2 3 5] == [
    { index = 0; value = 2; }
    { index = 1; value = 3; }
    { index = 2; value = 5; }
  ]);
  assert (testListReverse [1 2 3] == [3 2 1]);
  assert (testOptional {} == {});
  assert (testOptionalLit true == 0);
  assert (testOptionalLit false == null);
  assert (testOptionalFold (n : n) 0 == 1);
  assert (testRecord == {});
  assert (testRecordLit == { foo = 1; bar = true; });
  assert (testUnion == {});
  assert (testUnionLit { Left = n : n == 0; Right = b : b; } == false);
  assert ((testCombine { foo.baz = true; } { foo.bar = "ABC"; }) == {
    foo = {
      baz = true;
      bar = "ABC";
    };
  });
  assert (testMerge ({ Left, Right }: Left 2) == false);
  assert (testField { foo = true; bar = "ABC"; } == true);
  pkgs.stdenv.mkDerivation {
    name = "tests-pass";

    buildCommand = "touch $out";
  }

Gabriel Gonzalez Add a `pkgs.dhallToNix` utility
This adds a `dhallToNix` utility which compiles expression from the Dhall
configuration language to Nix using Nix's support for "import from derivation".
The main motivation of this compiler is to allow users to carve out small typed
subsets of Nix projects.  Everything in the Dhall language (except `Double`s)
can be translated to Nix in this way, including functions.
c791c0f
@joachifm joachifm merged commit da1cd49 into NixOS:master Jan 27, 2017

1 check failed

continuous-integration/travis-ci/pr The Travis CI build could not complete due to an error
Details
@Gabriel439 Gabriel439 referenced this pull request in Gabriel439/Haskell-Dhall-Library Jan 29, 2017
Closed

Try to write a Dhall-to-Nix compiler #4

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment