Add support for +/-Infinity and NaN of type Double. Encode Doubles us…

…ing IEEE 754 (#263)

standard/binary.md

@@ -98,9 +98,11 @@ e =   n              ; Unsigned integer    (Section 2.1, Major type = 0)
   /  False           ; False               (Section 2.3, Value = 20)
   /  True            ; True                (Section 2.3, Value = 21)
   /  null            ; Null                (Section 2.3, Value = 22)
+  /  n.n_h           ; Half float          (Section 2.3, Value = 25)
+  /  n.n_s           ; Single float        (Section 2.3, Value = 26)
+  /  n.n             ; Double float        (Section 2.3, Value = 27)
   /  nn              ; Unsigned bignum     (Section 2.4, Tag = 2)
   / -nn              ; Negative bignum     (Section 2.4, Tag = 3)
-  /  n.n             ; Decimal fraction    (Section 2.4, Tag = 4)
 ```
 
 ## Encoding judgment
@@ -590,14 +592,33 @@ Encode `Integer` literals using the smallest available numeric representation:
 
 ### `Double`
 
-Encode `Double`s as CBOR decimal fractions in order to avoid loss of precision
-when converting to and from their textual representation:
+Encode `Double` literals using the smallest available numeric representation.
+CBOR has 16-bit, 32-bit, and 64-bit IEEE 754 floating point representations.
 
 
-    ─────────────────────────────
-    encode(n.n) = [ 17, n.n ]
+    ─────────────────────────────  ; isNaN(n.n)
+    encode(n.n) = n.n_h(0x7e00)
+
+
+    ─────────────────────────────  ; toDouble(toSingle(n.n)) ≠ n.n AND NOT isNaN(n.n)
+    encode(n.n) = n.n
+
+
+    ─────────────────────────────  ; toDouble(toHalf(n.n)) ≠ n.n AND toDouble(toSingle(n.n)) = n.n AND NOT isNaN(n.n)
+    encode(n.n) = n.n_s
+
+
+    ─────────────────────────────  ; toDouble(toHalf(n.n)) = n.n AND NOT isNaN(n.n)
+    encode(n.n) = n.n_h
 
 
+In other words: If n.n is a NaN, encode as a half (16-bit) float with the value 0x7e00.
+This ensures identical semantic hashes on different platforms. For all other values,
+convert to `Single` and back to `Double` and check for equality with the original.
+If they are the same, then there is no loss of precision using the smaller representation.
+Also convert to `Half` and back and check for equality with the original. Use the smallest
+of the three representations (Half, Single, Double) possible without losing precision.
+
 ### `Text`
 
 Encode `Text` literals as an alternation between their text chunks and any
@@ -1209,15 +1230,20 @@ representation.
 
 ### `Double`
 
-Decode a CBOR array beginning with a `17` as an `Double` literal:
+Decode a CBOR double, single, or half and convert to a `Double` literal:
+
+
+    ─────────────────────────────
+    decode(n.n) = n.n
 
 
     ─────────────────────────────
-    decode([ 17, n.n ]) = n.n
+    decode(n.n_s) = n.n
+
 
+    ─────────────────────────────
+    decode(n.n_h) = n.n
 
-A decoder MUST accept a decimal fraction that is not encoded using the most
-compact representation.
 
 ### `Text`
 

standard/dhall.abnf

@@ -266,6 +266,8 @@ Text-raw              = %x54.65.78.74
 List-raw              = %x4c.69.73.74
 True-raw              = %x54.72.75.65
 False-raw             = %x46.61.6c.73.65
+NaN-raw               = %x4e.61.4e
+Infinity-raw          = %x49.6e.66.69.6e.69.74.79
 Type-raw              = %x54.79.70.65
 Kind-raw              = %x4b.69.6e.64
 Sort-raw              = %x53.6f.72.74
@@ -281,6 +283,8 @@ reserved-raw =
   / List-raw
   / True-raw
   / False-raw
+  / NaN-raw
+  / Infinity-raw
   / Type-raw
   / Kind-raw
   / Sort-raw
@@ -665,6 +669,9 @@ primitive-expression =
     ; "+2"
     / integer-literal
 
+    ; "-Infinity"
+    / "-" Infinity-raw
+
     ; '"ABC"'
     / text-literal
 

standard/semantics.md

@@ -2850,10 +2850,15 @@ An `Integer` literal is in normal form:
 `Integer/toDouble` transforms an `Integer` into the corresponding `Double`:
 
 
-    f ⇥ Natural/toDouble   a ⇥ ±n
+    f ⇥ Integer/toDouble   a ⇥ ±n
     ─────────────────────────────
     f a ⇥ ±n.0
 
+Note that if the magnitude of `a` is greater than 2^53, `Integer/toDouble a`
+may result in loss of precision. A `Double` will be selected by rounding `a` to
+the nearest `Double`. Ties go to the `Double` with an even least significant
+bit. When the magnitude of `a` is greater than or equal to `c`, the magnitude
+will round to `Infinity`, where `c = 2^1024 - 2^970 ≈ 1.8e308`.
 
 `Integer/show` transforms an `Integer` into a `Text` literal representing valid
 Dhall code for representing that `Integer` number:
@@ -2912,6 +2917,19 @@ The `Double/show` function is in normal form:
     Double/show ⇥ Double/show
 
 
+The following 2 properties must hold for `Double/show`:
+
+```
+show (read (show (X : Double))) = show X
+
+read (show (read (Y : Text))) = read Y
+```
+
+where `show : Double → Text` is shorthand for `Double/show` and `read : Text →
+Double` is the function in the implementation of Dhall which takes a correctly
+formated text representation of a `Double` as input and outputs a `Double`.
+
+
 ### Functions
 
 Normalizing a function type normalizes the types of the input and output: