Add Integer/toDouble (#434)

... as standardized in https://github.com/dhall-lang/dhall-lang/pull/168

Prelude/Integer/toDouble

@@ -0,0 +1,12 @@
+{-
+Convert an `Integer` to the corresponding `Double`
+
+Examples:
+
+```
+./toDouble -3 = -3.0
+
+./toDouble +2 = 2.0
+```
+-}
+let toDouble : Integer → Double = Integer/toDouble in toDouble

Prelude/Natural/toDouble

@@ -0,0 +1,16 @@
+{-
+Convert a `Natural` number to the corresponding `Double`
+
+Examples:
+
+```
+./toDouble 3 = 3.0
+
+./toDouble 0 = 0.0
+```
+-}
+    let toDouble
+        : Natural → Double
+        = λ(n : Natural) → Integer/toDouble (Natural/toInteger n)
+
+in  toDouble

dhall.cabal

@@ -34,6 +34,7 @@ Extra-Source-Files:
     Prelude/Bool/show
     Prelude/Double/show
     Prelude/Integer/show
+    Prelude/Integer/toDouble
     Prelude/List/all
     Prelude/List/any
     Prelude/List/build
@@ -63,6 +64,7 @@ Extra-Source-Files:
     Prelude/Natural/product
     Prelude/Natural/show
     Prelude/Natural/sum
+    Prelude/Natural/toDouble
     Prelude/Natural/toInteger
     Prelude/Optional/all
     Prelude/Optional/any
@@ -95,6 +97,7 @@ Extra-Source-Files:
     tests/normalization/examples/Bool/show/*.dhall
     tests/normalization/examples/Double/show/*.dhall
     tests/normalization/examples/Integer/show/*.dhall
+    tests/normalization/examples/Integer/toDouble/*.dhall
     tests/normalization/examples/List/all/*.dhall
     tests/normalization/examples/List/any/*.dhall
     tests/normalization/examples/List/build/*.dhall
@@ -123,6 +126,7 @@ Extra-Source-Files:
     tests/normalization/examples/Natural/product/*.dhall
     tests/normalization/examples/Natural/show/*.dhall
     tests/normalization/examples/Natural/sum/*.dhall
+    tests/normalization/examples/Natural/toDouble/*.dhall
     tests/normalization/examples/Natural/toInteger/*.dhall
     tests/normalization/examples/Optional/all/*.dhall
     tests/normalization/examples/Optional/any/*.dhall

src/Dhall/Core.hs

@@ -331,6 +331,8 @@ data Expr s a
     | IntegerLit Integer
     -- | > IntegerShow                              ~  Integer/show
     | IntegerShow
+    -- | > IntegerToDouble                          ~  Integer/toDouble
+    | IntegerToDouble
     -- | > Double                                   ~  Double
     | Double
     -- | > DoubleLit n                              ~  n
@@ -438,6 +440,7 @@ instance Monad (Expr s) where
     Integer              >>= _ = Integer
     IntegerLit a         >>= _ = IntegerLit a
     IntegerShow          >>= _ = IntegerShow
+    IntegerToDouble      >>= _ = IntegerToDouble
     Double               >>= _ = Double
     DoubleLit a          >>= _ = DoubleLit a
     DoubleShow           >>= _ = DoubleShow
@@ -501,6 +504,7 @@ instance Bifunctor Expr where
     first _  Integer               = Integer
     first _ (IntegerLit a        ) = IntegerLit a
     first _  IntegerShow           = IntegerShow
+    first _  IntegerToDouble       = IntegerToDouble
     first _  Double                = Double
     first _ (DoubleLit a         ) = DoubleLit a
     first _  DoubleShow            = DoubleShow
@@ -712,6 +716,7 @@ shift d v (NaturalTimes a b) = NaturalTimes a' b'
 shift _ _ Integer = Integer
 shift _ _ (IntegerLit a) = IntegerLit a
 shift _ _ IntegerShow = IntegerShow
+shift _ _ IntegerToDouble = IntegerToDouble
 shift _ _ Double = Double
 shift _ _ (DoubleLit a) = DoubleLit a
 shift _ _ DoubleShow = DoubleShow
@@ -868,6 +873,7 @@ subst x e (NaturalTimes a b) = NaturalTimes a' b'
 subst _ _ Integer = Integer
 subst _ _ (IntegerLit a) = IntegerLit a
 subst _ _ IntegerShow = IntegerShow
+subst _ _ IntegerToDouble = IntegerToDouble
 subst _ _ Double = Double
 subst _ _ (DoubleLit a) = DoubleLit a
 subst _ _ DoubleShow = DoubleShow
@@ -1073,6 +1079,8 @@ alphaNormalize (IntegerLit n) =
     IntegerLit n
 alphaNormalize IntegerShow =
     IntegerShow
+alphaNormalize IntegerToDouble =
+    IntegerToDouble
 alphaNormalize Double =
     Double
 alphaNormalize (DoubleLit n) =
@@ -1266,6 +1274,7 @@ denote (NaturalTimes a b    ) = NaturalTimes (denote a) (denote b)
 denote  Integer               = Integer
 denote (IntegerLit a        ) = IntegerLit a
 denote  IntegerShow           = IntegerShow
+denote  IntegerToDouble       = IntegerToDouble
 denote  Double                = Double
 denote (DoubleLit a         ) = DoubleLit a
 denote  DoubleShow            = DoubleShow
@@ -1369,6 +1378,7 @@ normalizeWith ctx e0 = loop (denote e0)
             App IntegerShow (IntegerLit n)
                 | 0 <= n    -> TextLit (Chunks [] ("+" <> Data.Text.pack (show n)))
                 | otherwise -> TextLit (Chunks [] (Data.Text.pack (show n)))
+            App IntegerToDouble (IntegerLit n) -> DoubleLit (fromInteger n)
             App DoubleShow (DoubleLit n) ->
                 TextLit (Chunks [] (Data.Text.pack (show n)))
             App (App OptionalBuild _A₀) g ->
@@ -1524,6 +1534,7 @@ normalizeWith ctx e0 = loop (denote e0)
     Integer -> Integer
     IntegerLit n -> IntegerLit n
     IntegerShow -> IntegerShow
+    IntegerToDouble -> IntegerToDouble
     Double -> Double
     DoubleLit n -> DoubleLit n
     DoubleShow -> DoubleShow
@@ -1715,6 +1726,7 @@ isNormalized e = case denote e of
         App NaturalShow (NaturalLit _) -> False
         App NaturalToInteger (NaturalLit _) -> False
         App IntegerShow (IntegerLit _) -> False
+        App IntegerToDouble (IntegerLit _) -> False
         App DoubleShow (DoubleLit _) -> False
         App (App OptionalBuild _) _ -> False
         App (App ListBuild _) _ -> False
@@ -1789,6 +1801,7 @@ isNormalized e = case denote e of
     Integer -> True
     IntegerLit _ -> True
     IntegerShow -> True
+    IntegerToDouble -> True
     Double -> True
     DoubleLit _ -> True
     DoubleShow -> True
@@ -1930,6 +1943,7 @@ reservedIdentifiers =
         , "Natural/show"
         , "Integer"
         , "Integer/show"
+        , "Integer/toDouble"
         , "Double"
         , "Double/show"
         , "Text"

src/Dhall/Diff.hs

@@ -1084,6 +1084,12 @@ diffExprF l@IntegerShow r =
     mismatch l r
 diffExprF l r@IntegerShow =
     mismatch l r
+diffExprF IntegerToDouble IntegerToDouble =
+    "…"
+diffExprF l@IntegerToDouble r =
+    mismatch l r
+diffExprF l r@IntegerToDouble =
+    mismatch l r
 diffExprF Double Double =
     "…"
 diffExprF l@Double r =

src/Dhall/Parser/Expression.hs

@@ -267,6 +267,7 @@ primitiveExpression embedded =
                 , alternative13
                 , alternative14
                 , alternative15
+                , alternativeIntegerToDouble
                 , alternative16
                 , alternative17
                 , alternative18
@@ -353,6 +354,10 @@ primitiveExpression embedded =
         _IntegerShow
         return IntegerShow
 
+    alternativeIntegerToDouble = do
+        _IntegerToDouble
+        return IntegerToDouble
+
     alternative16 = do
         _DoubleShow
         return DoubleShow

src/Dhall/Parser/Token.hs

@@ -443,6 +443,9 @@ _NaturalShow = reserved "Natural/show"
 _IntegerShow :: Parser ()
 _IntegerShow = reserved "Integer/show"
 
+_IntegerToDouble :: Parser ()
+_IntegerToDouble = reserved "Integer/toDouble"
+
 _DoubleShow :: Parser ()
 _DoubleShow = reserved "Double/show"
 

src/Dhall/Pretty/Internal.hs

@@ -720,6 +720,8 @@ prettyExprF Integer =
     builtin "Integer"
 prettyExprF IntegerShow =
     builtin "Integer/show"
+prettyExprF IntegerToDouble =
+    builtin "Integer/toDouble"
 prettyExprF Double =
     builtin "Double"
 prettyExprF DoubleShow =

src/Dhall/TypeCheck.hs

@@ -321,6 +321,8 @@ typeWithA tpa = loop
         return Integer
     loop _      IntegerShow  = do
         return (Pi "_" Integer Text)
+    loop _      IntegerToDouble = do
+        return (Pi "_" Integer Double)
     loop _      Double            = do
         return (Const Type)
     loop _     (DoubleLit _     ) = do

tests/Normalization.hs

@@ -68,6 +68,8 @@ preludeExamples =
         , shouldNormalize "Double/show" "./examples/Double/show/1"
         , shouldNormalize "Integer/show" "./examples/Integer/show/0"
         , shouldNormalize "Integer/show" "./examples/Integer/show/1"
+        , shouldNormalize "Integer/toDouble" "./examples/Integer/toDouble/0"
+        , shouldNormalize "Integer/toDouble" "./examples/Integer/toDouble/1"
         , shouldNormalize "List/all" "./examples/List/all/0"
         , shouldNormalize "List/all" "./examples/List/all/1"
         , shouldNormalize "List/any" "./examples/List/any/0"
@@ -126,6 +128,8 @@ preludeExamples =
         , shouldNormalize "Natural/show" "./examples/Natural/show/1"
         , shouldNormalize "Natural/sum" "./examples/Natural/sum/0"
         , shouldNormalize "Natural/sum" "./examples/Natural/sum/1"
+        , shouldNormalize "Natural/toDouble" "./examples/Natural/toDouble/0"
+        , shouldNormalize "Natural/toDouble" "./examples/Natural/toDouble/1"
         , shouldNormalize "Natural/toInteger" "./examples/Natural/toInteger/0"
         , shouldNormalize "Natural/toInteger" "./examples/Natural/toInteger/1"
         , shouldNormalize "Optional/all" "./examples/Optional/all/0"

tests/normalization/examples/Integer/toDouble/0A.dhall

@@ -0,0 +1 @@
+../../../../../Prelude/Integer/toDouble -3

tests/normalization/examples/Integer/toDouble/0B.dhall

@@ -0,0 +1 @@
+-3.0

tests/normalization/examples/Integer/toDouble/1A.dhall

@@ -0,0 +1 @@
+../../../../../Prelude/Integer/toDouble +2

tests/normalization/examples/Integer/toDouble/1B.dhall

@@ -0,0 +1 @@
+2.0

tests/normalization/examples/Natural/toDouble/0A.dhall

@@ -0,0 +1 @@
+../../../../../Prelude/Natural/toDouble 3

tests/normalization/examples/Natural/toDouble/0B.dhall

@@ -0,0 +1 @@
+3.0

tests/normalization/examples/Natural/toDouble/1A.dhall

@@ -0,0 +1 @@
+../../../../../Prelude/Natural/toDouble 0

tests/normalization/examples/Natural/toDouble/1B.dhall

@@ -0,0 +1 @@
+0.0