Add new Some/None constructors (#559)

... as standardized in dhall-lang/dhall-lang#227

The legacy `Optional` syntax is still supported for now but the normal form for `Optional`
literals now prefers `Some`/`None`.

The `dhall lint` command will automatically migrate the old `Optional` literal syntax to the
new syntax.

Prelude/Bool/package.dhall

@@ -1,17 +1,17 @@
 { and =
-    ./and 
+    ./and
 , build =
-    ./build 
+    ./build
 , even =
-    ./even 
+    ./even
 , fold =
-    ./fold 
+    ./fold
 , not =
-    ./not 
+    ./not
 , odd =
-    ./odd 
+    ./odd
 , or =
-    ./or 
+    ./or
 , show =
-    ./show 
+    ./show
 }

Prelude/Double/package.dhall

@@ -1 +1 @@
-{ show = ./show  }
+{ show = ./show }

Prelude/Function/compose

@@ -0,0 +1,21 @@
+{-
+Compose two functions into one.
+
+Examples:
+
+```
+./compose Natural Natural Bool (λ(n : Natural) → n + n) ../Natural/even 3
+= True
+```
+-}
+    let compose
+        : ∀(a : Type) → ∀(b : Type) → ∀(c : Type) → (a → b) → (b → c) → a → c
+        =   λ(A : Type)
+          → λ(B : Type)
+          → λ(C : Type)
+          → λ(f : A → B)
+          → λ(g : B → C)
+          → λ(x : A)
+          → g (f x)
+
+in  compose

Prelude/Function/package.dhall

@@ -0,0 +1 @@
+{ compose = ./compose }

Prelude/Integer/package.dhall

@@ -1 +1 @@
-{ show = ./show  }
+{ show = ./show }

Prelude/JSON/Nesting

@@ -0,0 +1,32 @@
+{-
+This type is used as part of `dhall-json`'s support for preserving alternative
+names
+
+For example, this Dhall code:
+
+```
+    let Example = < Left : { foo : Natural } | Right : { bar : Bool } >
+
+in  let example = constructors Example
+
+in  let Nesting = < Inline : {} | Nested : Text >
+
+in  let nesting = constructors Nesting
+
+in  { field    = "name"
+    , nesting  = nesting.Inline {=}
+    , contents = example.Left { foo = 2 }
+    }
+```
+
+... generates this JSON:
+
+```
+{
+  "foo": 2,
+  "name": "Left"
+ }
+```
+
+-}
+let Nesting : Type = < Inline : {} | Nested : Text > in Nesting

Prelude/JSON/Tagged

@@ -0,0 +1,69 @@
+{-
+This is a convenient type-level function when using `dhall-to-json`'s support
+for preserving alternative names
+
+For example, this code:
+
+```
+    let map = ../List/map
+
+in  let Provisioner =
+          < shell :
+              { inline : List Text }
+          | file :
+              { source : Text, destination : Text }
+          >
+
+in  let provisioner = constructors Provisioner
+
+in  let Tagged = ./Tagged
+
+in  let nesting = constructors ./Nesting
+
+in  let wrap
+        : Provisioner → Tagged Provisioner
+        =   λ(x : Provisioner)
+          → { field = "type", nesting = nesting.Nested "params", contents = x }
+
+in  { provisioners =
+        map
+        Provisioner
+        (Tagged Provisioner)
+        wrap
+        [ provisioner.shell { inline = [ "echo foo" ] }
+        , provisioner.file
+          { source = "app.tar.gz", destination = "/tmp/app.tar.gz" }
+        ]
+    }
+```
+
+... produces this JSON:
+
+```
+{
+  "provisioners": [
+    {
+      "params": {
+        "inline": [
+          "echo foo"
+        ]
+      },
+      "type": "shell"
+    },
+    {
+      "params": {
+        "destination": "/tmp/app.tar.gz",
+        "source": "app.tar.gz"
+      },
+      "type": "file"
+    }
+  ]
+}
+```
+
+-}
+    let Tagged
+        : Type → Type
+        = λ(a : Type) → { field : Text, nesting : ./Nesting, contents : a }
+
+in  Tagged

Prelude/JSON/keyText

@@ -0,0 +1,17 @@
+{-
+Builds a key-value record such that a List of them will be converted to a
+homogeneous record by dhall-to-json and dhall-to-yaml.
+Both key and value are fixed to Text.
+Take a look at `Record/keyValue` for a polymorphic version.
+
+Example:
+
+```
+./keyText "foo" "bar" = { mapKey = "foo", mapValue = "bar" }
+```
+-}
+
+    let keyText =
+          λ(key : Text) → λ(value : Text) → { mapKey = key, mapValue = value }
+
+in  keyText

Prelude/JSON/keyValue

@@ -0,0 +1,20 @@
+{-
+Builds a key-value record such that a List of them will be converted to a
+homogeneous record by dhall-to-json and dhall-to-yaml.
+
+Examples:
+
+```
+./keyValue Natural "foo" 2 = { mapKey = "foo", mapValue = 2 }
+
+./keyValue Text "bar" "baz" = { mapKey = "bar", mapValue = "baz" }
+```
+-}
+
+    let keyValue =
+            λ(v : Type)
+          → λ(key : Text)
+          → λ(value : v)
+          → { mapKey = key, mapValue = value }
+
+in  keyValue

Prelude/JSON/package.dhall

@@ -0,0 +1 @@
+{ keyText = ./keyText, keyValue = ./keyValue }

Prelude/List/head

@@ -4,9 +4,9 @@ Retrieve the first element of the list
 Examples:
 
 ```
-./head Natural [ 0, 1, 2 ] = [ 0 ] : Optional Natural
+./head Natural [ 0, 1, 2 ] = Some 0
 
-./head Natural ([] : List Natural) = [] : Optional Natural
+./head Natural ([] : List Natural) = None Natural
 ```
 -}
 let head : ∀(a : Type) → List a → Optional a = List/head in head

Prelude/List/last

@@ -4,9 +4,9 @@ Retrieve the last element of the list
 Examples:
 
 ```
-./last Natural [ 0, 1, 2 ] = [ 2 ] : Optional Natural
+./last Natural [ 0, 1, 2 ] = Some 2
 
-./last Natural ([] : List Natural) = [] : Optional Natural
+./last Natural ([] : List Natural) = None Natural
 ```
 -}
 let last : ∀(a : Type) → List a → Optional a = List/last in last

Prelude/List/package.dhall

@@ -1,39 +1,39 @@
 { all =
-    ./all 
+    ./all
 , any =
-    ./any 
+    ./any
 , build =
-    ./build 
+    ./build
 , concat =
-    ./concat 
+    ./concat
 , concatMap =
-    ./concatMap 
+    ./concatMap
 , filter =
-    ./filter 
+    ./filter
 , fold =
-    ./fold 
+    ./fold
 , generate =
-    ./generate 
+    ./generate
 , head =
-    ./head 
+    ./head
 , indexed =
-    ./indexed 
+    ./indexed
 , iterate =
-    ./iterate 
+    ./iterate
 , last =
-    ./last 
+    ./last
 , length =
-    ./length 
+    ./length
 , map =
-    ./map 
+    ./map
 , null =
-    ./null 
+    ./null
 , replicate =
-    ./replicate 
+    ./replicate
 , reverse =
-    ./reverse 
+    ./reverse
 , shifted =
-    ./shifted 
+    ./shifted
 , unzip =
-    ./unzip 
+    ./unzip
 }

Prelude/List/shifted

@@ -58,8 +58,9 @@ Bool
                                         { index : Natural, value : a }
                                         kvs
 
-                              in  { count = y.count + length
-                                  , diff  =
+                              in  { count =
+                                      y.count + length
+                                  , diff =
                                         λ(n : Natural)
                                       → List/fold
                                         { index : Natural, value : a }
@@ -70,8 +71,10 @@ Bool
                                               )
                                           → λ(z : list)
                                           →     let kvNew =
-                                                      { index = kvOld.index + n
-                                                      , value = kvOld.value
+                                                      { index =
+                                                          kvOld.index + n
+                                                      , value =
+                                                          kvOld.value
                                                       }
 
                                             in  cons kvNew z

Prelude/Natural/package.dhall

@@ -1,21 +1,21 @@
 { build =
-    ./build 
+    ./build
 , enumerate =
-    ./enumerate 
+    ./enumerate
 , even =
-    ./even 
+    ./even
 , fold =
-    ./fold 
+    ./fold
 , isZero =
-    ./isZero 
+    ./isZero
 , odd =
-    ./odd 
+    ./odd
 , product =
-    ./product 
+    ./product
 , sum =
-    ./sum 
+    ./sum
 , show =
-    ./show 
+    ./show
 , toInteger =
-    ./toInteger 
+    ./toInteger
 }

Prelude/Optional/all

@@ -5,9 +5,9 @@ and `True` otherwise:
 Examples:
 
 ```
-./all Natural Natural/even ([ 3 ] : Optional Natural) = False
+./all Natural Natural/even (Some 3) = False
 
-./all Natural Natural/even ([] : Optional Natural) = True
+./all Natural Natural/even (None Natural) = True
 ```
 -}
     let all

Prelude/Optional/any

@@ -5,9 +5,9 @@ Returns `True` if the supplied function returns `True` for a present element and
 Examples:
 
 ```
-./any Natural Natural/even ([ 2 ] : Optional Natural) = True
+./any Natural Natural/even (Some 2) = True
 
-./any Natural Natural/even ([] : Optional Natural) = False
+./any Natural Natural/even (None Natural) = False
 ```
 -}
     let any