Initial commit

Any/Type.dhall

@@ -0,0 +1 @@
+{ __any : Text }

Any/add.dhall

@@ -0,0 +1,12 @@
+λ(nix : ../NixPrelude.dhall) →
+  let Any = ./Type.dhall
+
+  let Number = ../Number/Type.dhall
+
+  let Any/toTypeUnchecked = ./toTypeUnchecked.dhall nix
+
+  in  λ(e1 : Any) →
+      λ(e2 : Any) →
+        nix.builtins.add
+          (Any/toTypeUnchecked Number e1)
+          (Any/toTypeUnchecked Number e2)

Any/apply.dhall

@@ -0,0 +1,6 @@
+λ(nix : ../NixPrelude.dhall) →
+  let Any = ./Type.dhall
+
+  let Any/toTypeUnchecked = ./toTypeUnchecked.dhall nix
+
+  in  λ(e : Any) → Any/toTypeUnchecked (Any → Any) e

Any/div.dhall

@@ -0,0 +1,12 @@
+λ(nix : ../NixPrelude.dhall) →
+  let Any = ./Type.dhall
+
+  let Number = ../Number/Type.dhall
+
+  let Any/toTypeUnchecked = ./toTypeUnchecked.dhall nix
+
+  in  λ(e1 : Any) →
+      λ(e2 : Any) →
+        nix.builtins.div
+          (Any/toTypeUnchecked Number e1)
+          (Any/toTypeUnchecked Number e2)

Any/eq.dhall

@@ -0,0 +1,8 @@
+λ(nix : ../NixPrelude.dhall) →
+  let Any = ./Type.dhall
+
+  let Any/toTypeUnchecked = ./toTypeUnchecked.dhall nix
+
+  let eqFile = nix.builtins.toFile "eq.nix" "a: b: a == b"
+
+  in  Any/toTypeUnchecked (Any → Any → Bool) (nix.builtins.import eqFile)

Any/gt.dhall

@@ -0,0 +1,6 @@
+λ(nix : ../NixPrelude.dhall) →
+  let Any = ./Type.dhall
+
+  let Any/lte = ./lte.dhall nix
+
+  in  λ(e1 : Any) → λ(e2 : Any) → Any/lte e1 e2 == False

Any/gte.dhall

@@ -0,0 +1,6 @@
+λ(nix : ../NixPrelude.dhall) →
+  let Any = ./Type.dhall
+
+  let Any/lt = ./lt.dhall nix
+
+  in  λ(e1 : Any) → λ(e2 : Any) → Any/lt e1 e2 == False

Any/hasAttr.dhall

@@ -0,0 +1,10 @@
+λ(nix : ../NixPrelude.dhall) →
+  let Any = ./Type.dhall
+
+  let Set = ../Set/Type.dhall
+
+  let Any/toTypeUnchecked = ./toTypeUnchecked.dhall nix
+
+  in  λ(e : Any) →
+      λ(attr : Text) →
+        nix.builtins.hasAttr attr (Any/toTypeUnchecked Set e)

Any/impl.dhall

@@ -0,0 +1,10 @@
+λ(nix : ../NixPrelude.dhall) →
+  let Any = ./Type.dhall
+
+  let Any/not = ./not.dhall nix
+
+  let Any/lor = ./lor.dhall nix
+
+  let Any/toAny = ./toAny.dhall nix
+
+  in  λ(e1 : Any) → λ(e2 : Any) → Any/lor (Any/toAny Bool (Any/not e1)) e2

Any/land.dhall

@@ -0,0 +1,8 @@
+λ(nix : ../NixPrelude.dhall) →
+  let Any = ./Type.dhall
+
+  let Any/toTypeUnchecked = ./toTypeUnchecked.dhall nix
+
+  in  λ(e1 : Any) →
+      λ(e2 : Any) →
+        Any/toTypeUnchecked Bool e1 && Any/toTypeUnchecked Bool e2

Any/listConcat.dhall

@@ -0,0 +1,11 @@
+λ(nix : ../NixPrelude.dhall) →
+  let Any = ./Type.dhall
+
+  let Any/toTypeUnchecked = ./toTypeUnchecked.dhall nix
+
+  in  λ(e1 : Any) →
+      λ(e2 : Any) →
+        nix.builtins.concatLists
+          [ Any/toTypeUnchecked (List Any) e1
+          , Any/toTypeUnchecked (List Any) e2
+          ]

Any/lor.dhall

@@ -0,0 +1,8 @@
+λ(nix : ../NixPrelude.dhall) →
+  let Any = ./Type.dhall
+
+  let Any/toTypeUnchecked = ./toTypeUnchecked.dhall nix
+
+  in  λ(e1 : Any) →
+      λ(e2 : Any) →
+        Any/toTypeUnchecked Bool e1 || Any/toTypeUnchecked Bool e2

Any/lt.dhall

@@ -0,0 +1,12 @@
+λ(nix : ../NixPrelude.dhall) →
+  let Any = ./Type.dhall
+
+  let Number = ../Number/Type.dhall
+
+  let Any/toTypeUnchecked = ./toTypeUnchecked.dhall nix
+
+  in  λ(e1 : Any) →
+      λ(e2 : Any) →
+        nix.builtins.lessThan
+          (Any/toTypeUnchecked Number e1)
+          (Any/toTypeUnchecked Number e2)

Any/lte.dhall

@@ -0,0 +1,8 @@
+λ(nix : ../NixPrelude.dhall) →
+  let Any = ./Type.dhall
+
+  let Any/lt = ./lt.dhall nix
+
+  let Any/eq = ./eq.dhall nix
+
+  in  λ(e1 : Any) → λ(e2 : Any) → Any/lt e1 e2 || Any/eq e1 e2

Any/mul.dhall

@@ -0,0 +1,12 @@
+λ(nix : ../NixPrelude.dhall) →
+  let Any = ./Type.dhall
+
+  let Number = ../Number/Type.dhall
+
+  let Any/toTypeUnchecked = ./toTypeUnchecked.dhall nix
+
+  in  λ(e1 : Any) →
+      λ(e2 : Any) →
+        nix.builtins.mul
+          (Any/toTypeUnchecked Number e1)
+          (Any/toTypeUnchecked Number e2)

Any/negate.dhall

@@ -0,0 +1,8 @@
+λ(nix : ../NixPrelude.dhall) →
+  let Any = ./Type.dhall
+
+  let Any/toAny = ./toAny.dhall nix
+
+  let Any/sub = ./sub.dhall nix
+
+  in  λ(e : Any) → Any/sub (Any/toAny Natural 0) e

Any/neq.dhall

@@ -0,0 +1,6 @@
+λ(nix : ../NixPrelude.dhall) →
+  let Any = ./Type.dhall
+
+  let Any/eq = ./eq.dhall nix
+
+  in  λ(e1 : Any) → λ(e2 : Any) → Any/eq e1 e2 == False

Any/not.dhall

@@ -0,0 +1,6 @@
+λ(nix : ../NixPrelude.dhall) →
+  let Any = ./Type.dhall
+
+  let Any/toTypeUnchecked = ./toTypeUnchecked.dhall nix
+
+  in  λ(e : Any) → Any/toTypeUnchecked Bool e == False

Any/package.dhall

@@ -0,0 +1,27 @@
+λ(nix : ../NixPrelude.dhall) →
+  { Type = ./Type.dhall
+  , toAny = ./toAny.dhall nix
+  , toTypeUnchecked = ./toTypeUnchecked.dhall nix
+  , select = ./select.dhall nix
+  , selectOptional = ./selectOptional.dhall nix
+  , apply = ./apply.dhall nix
+  , negate = ./negate.dhall nix
+  , hasAttr = ./hasAttr.dhall nix
+  , listConcat = ./listConcat.dhall nix
+  , mul = ./mul.dhall nix
+  , div = ./div.dhall nix
+  , add = ./add.dhall nix
+  , sub = ./sub.dhall nix
+  , stringConcat = ./stringConcat.dhall nix
+  , not = ./not.dhall nix
+  , update = ./update.dhall nix
+  , lt = ./lt.dhall nix
+  , lte = ./lte.dhall nix
+  , gt = ./gt.dhall nix
+  , gte = ./gt.dhall nix
+  , eq = ./eq.dhall nix
+  , neq = ./neq.dhall nix
+  , land = ./land.dhall nix
+  , lor = ./lor.dhall nix
+  , impl = ./impl.dhall nix
+  }

Any/select.dhall

@@ -0,0 +1,10 @@
+λ(nix : ../NixPrelude.dhall) →
+  let Any = ./Type.dhall
+
+  let Set = ../Set/Type.dhall
+
+  let Any/toTypeUnchecked = ./toTypeUnchecked.dhall nix
+
+  in  λ(e : Any) →
+      λ(attrpath : Text) →
+        nix.builtins.getAttr attrpath (Any/toTypeUnchecked Set e)

Any/selectOptional.dhall

@@ -0,0 +1,10 @@
+λ(nix : ../NixPrelude.dhall) →
+  let Any = ./Type.dhall
+
+  let Any/select = ./select.dhall nix
+
+  let Any/hasAttr = ./hasAttr.dhall nix
+
+  in  λ(e : Any) →
+      λ(attr : Text) →
+        if Any/hasAttr e attr then Some (Any/select e attr) else None Any

Any/stringConcat.dhall

@@ -0,0 +1,10 @@
+λ(nix : ../NixPrelude.dhall) →
+  let Any = ./Type.dhall
+
+  let Any/toTypeUnchecked = ./toTypeUnchecked.dhall nix
+
+  in  λ(e1 : Any) →
+      λ(e2 : Any) →
+        nix.builtins.concatStringsSep
+          ""
+          [ Any/toTypeUnchecked Text e1, Any/toTypeUnchecked Text e2 ]

Any/sub.dhall

@@ -0,0 +1,12 @@
+λ(nix : ../NixPrelude.dhall) →
+  let Any = ./Type.dhall
+
+  let Number = ../Number/Type.dhall
+
+  let Any/toTypeUnchecked = ./toTypeUnchecked.dhall nix
+
+  in  λ(e1 : Any) →
+      λ(e2 : Any) →
+        nix.builtins.sub
+          (Any/toTypeUnchecked Number e1)
+          (Any/toTypeUnchecked Number e2)

Any/toAny.dhall

@@ -0,0 +1 @@
+λ(nix : ../NixPrelude.dhall) → nix.primops.toAny

Any/toTypeUnchecked.dhall

@@ -0,0 +1 @@
+λ(nix : ../NixPrelude.dhall) → nix.primops.toTypeUnchecked

Any/update.dhall

@@ -0,0 +1,33 @@
+λ(nix : ../NixPrelude.dhall) →
+  let Any = ./Type.dhall
+
+  let Set = ../Set/Type.dhall
+
+  let Number = ../Number/Type.dhall
+
+  let Any/toTypeUnchecked = ./toTypeUnchecked.dhall nix
+
+  let Any/sub = ./sub.dhall nix
+
+  let Any/toAny = ./toAny.dhall nix
+
+  let lastElem =
+        λ(x : List Any) →
+          nix.builtins.elemAt
+            x
+            ( Any/toTypeUnchecked
+                Natural
+                ( Any/toAny
+                    Number
+                    ( Any/sub
+                        (Any/toAny Natural (nix.builtins.length x))
+                        (Any/toAny Natural 1)
+                    )
+                )
+            )
+
+  in  λ(e1 : Any) →
+      λ(e2 : Any) →
+        nix.builtins.zipAttrsWith
+          (λ(name : Text) → λ(values : List Any) → lastElem values)
+          [ Any/toTypeUnchecked Set e1, Any/toTypeUnchecked Set e2 ]

NixPrelude.dhall

@@ -0,0 +1 @@
+{ primops : ./primops.dhall, builtins : ./builtins.dhall }

Number/Type.dhall

@@ -0,0 +1 @@
+{ __number : Text }

Number/package.dhall

@@ -0,0 +1 @@
+λ(nix : ../NixPrelude.dhall) → { Type = ./Type.dhall }

Path/Type.dhall

@@ -0,0 +1 @@
+{ __path : Text }

Path/package.dhall

@@ -0,0 +1 @@
+λ(nix : ../NixPrelude.dhall) → { Type = ./Type.dhall }

Set/Type.dhall

@@ -0,0 +1 @@
+{ __set : Text }

Set/package.dhall

@@ -0,0 +1 @@
+λ(nix : ../NixPrelude.dhall) → { Type = ./Type.dhall }

builtins.dhall

@@ -0,0 +1,115 @@
+let Any = ./Any/Type.dhall
+
+let Number = ./Number/Type.dhall
+
+let Set = ./Set/Type.dhall
+
+let Path = ./Path/Type.dhall
+
+in  { derivation : ∀(attrs : Set) → Path
+    , abort : ∀(s : Text) → Any
+    , add : ∀(e1 : Number) → ∀(e2 : Number) → Number
+    , all : ∀(pred : ∀(e : Any) → Bool) → ∀(list : List Any) → Bool
+    , any : ∀(pred : ∀(e : Any) → Bool) → ∀(list : List Any) → Bool
+    , attrNames : ∀(set : Set) → List Text
+    , attrValues : ∀(set : Set) → List Any
+    , baseNameOf : ∀(s : Path) → Text
+    , bitAnd : ∀(e1 : Natural) → ∀(e2 : Natural) → Natural
+    , bitOr : ∀(e1 : Natural) → ∀(e2 : Natural) → Natural
+    , bitXor : ∀(e1 : Natural) → ∀(e2 : Natural) → Natural
+    , break : ∀(v : Any) → Any
+    , catAttrs : ∀(attr : Text) → ∀(list : List Set) → Set
+    , ceil : ∀(double : Number) → Number
+    , compareVersions : ∀(s1 : Text) → ∀(s2 : Text) → Integer
+    , concatLists : ∀(lists : List (List Any)) → List Any
+    , concatMap :
+        ∀(f : ∀(e : Any) → Any) → ∀(lists : List (List Any)) → List Any
+    , concatStringsSep : ∀(separator : Text) → ∀(list : List Text) → Text
+    , deepSeq : ∀(e1 : Any) → ∀(e2 : Any) → Any
+    , dirOf : ∀(s : Path) → Path
+    , div : ∀(e1 : Number) → ∀(e2 : Number) → Number
+    , elem : ∀(x : Any) → ∀(xs : List Any) → Bool
+    , elemAt : ∀(xs : List Any) → ∀(n : Natural) → Any
+    , fetchClosure : ∀(args : Set) → Path
+    , fetchGit : ∀(args : Set) → Path
+    , fetchTarball : ∀(args : Set) → Path
+    , fetchurl : ∀(url : Text) → Path
+    , filter : ∀(f : ∀(e : Any) → Bool) → ∀(list : List Any) → List Any
+    , filterSource :
+        ∀(e1 : ∀(path : Path) → ∀(type : Text) → Bool) → ∀(e2 : Path) → Set
+    , floor : ∀(double : Number) → Number
+    , `foldl'` :
+        ∀(op : ∀(e1 : Any) → ∀(e2 : Any) → Any) →
+        ∀(nul : Any) →
+        ∀(list : List Any) →
+          Any
+    , fromJSON : ∀(e : Text) → Any
+    , functionArgs : ∀(e : Any) → Set
+    , genList :
+        ∀(generator : ∀(e : Natural) → Any) → ∀(length : Natural) → List Any
+    , genericClosure :
+        ∀(attrset : { startSet : List Set, operator : ∀(item : Set) → Set }) →
+          Set
+    , getAttr : ∀(s : Text) → ∀(set : Set) → Any
+    , getFlake : ∀(args : Text) → Set
+    , groupBy : ∀(f : ∀(e : Any) → Text) → ∀(list : List Any) → Set
+    , hasAttr : ∀(s : Text) → ∀(set : Set) → Bool
+    , hashFile : ∀(type : Text) → ∀(p : Path) → Text
+    , hashString : ∀(type : Text) → ∀(p : Text) → Text
+    , head : ∀(type : List Any) → Any
+    , import : ∀(path : Path) → Any
+    , insersectAttrs : ∀(e1 : Set) → ∀(e2 : Set) → Set
+    , isAttrs : ∀(e : Any) → Bool
+    , isBool : ∀(e : Any) → Bool
+    , isFloat : ∀(e : Any) → Bool
+    , isFunction : ∀(e : Any) → Bool
+    , isInt : ∀(e : Any) → Bool
+    , isList : ∀(e : Any) → Bool
+    , isPath : ∀(e : Any) → Bool
+    , isString : ∀(e : Any) → Bool
+    , length : ∀(e : List Any) → Natural
+    , lessThan : ∀(e1 : Number) → ∀(e2 : Number) → Bool
+    , listToAttrs : ∀(e : List { name : Text, value : Any }) → Set
+    , map : ∀(f : ∀(e : Any) → Any) → ∀(list : List Any) → List Any
+    , mapAttrs :
+        ∀(f : ∀(e1 : Text) → ∀(e2 : Any) → Any) → ∀(attrset : Set) → Set
+    , match : ∀(regex : Text) → ∀(str : Text) → Optional (List Any)
+    , mul : ∀(e1 : Number) → ∀(e2 : Number) → Number
+    , parseDrvName : ∀(s : Text) → { name : Text, version : Text }
+    , partition :
+        ∀(pred : ∀(e : Any) → Bool) →
+        ∀(list : List Any) →
+          { right : List Any, wrong : List Any }
+    , path : ∀(args : Set) → Path
+    , pathExists : ∀(path : Path) → Bool
+    , placeholder : ∀(output : Text) → Text
+    , readDir : ∀(path : Path) → Set
+    , readFile : ∀(path : Path) → Text
+    , removeAttrs : ∀(set : Set) → ∀(list : List Text) → Set
+    , replaceStrings :
+        ∀(from : List Text) → ∀(to : List Text) → ∀(s : Text) → Text
+    , seq : ∀(e1 : Any) → ∀(e2 : Any) → Any
+    , sort :
+        ∀(comparator : ∀(e1 : Any) → ∀(e2 : Any) → Bool) →
+        ∀(list : List Any) →
+          List Any
+    , split : ∀(regex : Text) → ∀(string : Text) → List Any
+    , splitVersion : ∀(version : Text) → List Text
+    , stringLength : ∀(string : Text) → Natural
+    , sub : ∀(e1 : Number) → ∀(e2 : Number) → Number
+    , substring : ∀(start : Natural) → ∀(len : Natural) → ∀(s : Text) → Text
+    , tail : ∀(list : List Any) → List Any
+    , throw : ∀(s : Text) → Any
+    , toFile : ∀(name : Text) → ∀(s : Text) → Path
+    , toJSON : ∀(e : Any) → Text
+    , toString : ∀(e : Any) → Text
+    , toXML : ∀(e : Any) → Text
+    , trace : ∀(e1 : Any) → ∀(e2 : Any) → Any
+    , traceVerbose : ∀(e1 : Any) → ∀(e2 : Any) → Any
+    , tryEval : ∀(e : Any) → { success : Bool, value : Any }
+    , typeOf : ∀(e : Any) → Text
+    , zipAttrsWith :
+        ∀(f : ∀(name : Text) → ∀(values : List Any) → Any) →
+        ∀(list : List Set) →
+          Set
+    }

dhallToNix.nix

@@ -0,0 +1,15 @@
+{ pkgs ? import <nixpkgs> {} }: code:
+let
+  codeString = builtins.toString code;
+  file = if builtins.isPath code then code else builtins.toFile "dhall-expr" codeString;
+  drv = pkgs.stdenvNoCC.mkDerivation {
+    name = "dhall-expr-as-nix";
+    src = ./.;
+    buildCommand = ''
+      cd $src
+      dhall-to-nix < ${file} > $out
+    '';
+
+    nativeBuildInputs = [ pkgs.dhall-nix ];
+  };
+in import "${drv}"

package.dhall

@@ -0,0 +1,6 @@
+λ(nix : ./NixPrelude.dhall) →
+  { Any = ./Any/package.dhall nix
+  , Number = ./Number/package.dhall nix
+  , Path = ./Path/package.dhall nix
+  , Set = ./Set/package.dhall nix
+  }

primops.dhall

@@ -0,0 +1,5 @@
+let Any = ./Any/Type.dhall
+
+in  { toAny : ∀(t : Type) → ∀(v : t) → Any
+    , toTypeUnchecked : ∀(t : Type) → ∀(v : Any) → t
+    }