Add Show instances for Int32, Int64, and Float64.

Use portable format constants from `<cinttypes>` and `<cfloat>`.
Change FFI calls to explicitly used fixed-width Int32 instead of Int.
Add prettyprinter-1.6.2 to stack-macos.yaml for consistency with stack.yaml.
Add show-tests.dx and register it as a test in makefile.

examples/show-tests.dx

@@ -0,0 +1,89 @@
+'# `Show` instances
+
+-- Int32
+
+:p show (1234: Int32)
+> (AsList 4 ['1', '2', '3', '4'])
+
+:p show (-1234: Int32)
+> (AsList 5 ['-', '1', '2', '3', '4'])
+
+:p show ((FToI (-(pow 2. 31.))): Int32)
+> (AsList 11 ['-', '2', '1', '4', '7', '4', '8', '3', '6', '4', '8'])
+
+-- Int64
+
+:p show (IToI64 1234: Int64)
+> (AsList 4 ['1', '2', '3', '4'])
+
+-- FIXME(https://github.com/google-research/dex-lang/issues/317):
+-- Unexpected zext from type conversion of negative Int32 to Int64.
+:p show (IToI64 (-1234): Int64)
+> (AsList 10 ['4', '2', '9', '4', '9', '6', '6', '0', '6', '2'])
+
+-- Float32
+
+:p show (123.456789: Float32)
+> (AsList 10 ['1', '2', '3', '.', '4', '5', '6', '7', '8', '7'])
+
+:p show ((pow 2. 16.): Float32)
+> (AsList 5 ['6', '5', '5', '3', '6'])
+
+-- FIXME(https://github.com/google-research/dex-lang/issues/316):
+-- Unparenthesized expression with type ascription does not parse.
+-- :p show (nan: Float32)
+
+:p show ((nan): Float32)
+> (AsList 3 ['n', 'a', 'n'])
+
+-- Note: `show nan` (Dex runtime dtoa implementation) appears different from
+-- `:p nan` (Dex interpreter implementation).
+:p nan
+> NaN
+
+:p show ((infinity): Float32)
+> (AsList 3 ['i', 'n', 'f'])
+
+-- Note: `show infinity` (Dex runtime dtoa implementation) appears different from
+-- `:p nan` (Dex interpreter implementation).
+:p infinity
+> Infinity
+
+-- Float64
+
+:p show (FToF64 123.456789: Float64)
+> (AsList 16 [ '1'
+>            , '2'
+>            , '3'
+>            , '.'
+>            , '4'
+>            , '5'
+>            , '6'
+>            , '7'
+>            , '8'
+>            , '7'
+>            , '1'
+>            , '0'
+>            , '9'
+>            , '3'
+>            , '7'
+>            , '5' ])
+
+:p show (FToF64 (pow 2. 16.): Float64)
+> (AsList 5 ['6', '5', '5', '3', '6'])
+
+:p show ((FToF64 nan): Float64)
+> (AsList 3 ['n', 'a', 'n'])
+
+-- Note: `show nan` (Dex runtime dtoa implementation) appears different from
+-- `:p nan` (Dex interpreter implementation).
+:p (FToF64 nan)
+> NaN
+
+:p show ((FToF64 infinity): Float64)
+> (AsList 3 ['i', 'n', 'f'])
+
+-- Note: `show infinity` (Dex runtime dtoa implementation) appears different from
+-- `:p nan` (Dex interpreter implementation).
+:p (FToF64 infinity)
+> Infinity

makefile

@@ -74,7 +74,7 @@ build-python: build
 # --- running tests ---
 
 # TODO: re-enable linear-tests ad-tests include-test chol
-example-names = uexpr-tests adt-tests type-tests eval-tests \
+example-names = uexpr-tests adt-tests type-tests eval-tests show-tests \
                 shadow-tests monad-tests \
                 ad-tests mandelbrot pi sierpinsky \
                 regression brownian_motion particle-swarm-optimizer \

prelude.dx

@@ -801,24 +801,39 @@ String : Type = List Char
 
 CharPtr : Type = %CharPtr
 
-interface Show a:Type where
-  show : a -> String
-
 -- TODO. This is ASCII code point. It really should be Int32 for Unicode codepoint 
 def codepoint (c:Char) : Int8 = %codePoint c
 
 @instance charEq  : Eq Char  = MkEq \x y. codepoint x == codepoint y
 @instance charOrd : Ord Char = (MkOrd charEq (\x y. codepoint x > codepoint y)
                                              (\x y. codepoint x < codepoint y))
 
+interface Show a:Type where
+  show : a -> String
 
-def showFloat' (x:Float) : String =
-  (n, ptr) = %ffi showFloat (Int & CharPtr) x
-  AsList n $ for i:(Fin n).
-    MkChar $ %ptrLoad (%ptrOffset ptr (ordinal i))
-
-instance showFloat : Show Float where
-  show = showFloat'
+instance showInt32 : Show Int32 where
+  show = \x: Int32.
+    (n, ptr) = %ffi showInt32 (Int32 & CharPtr) x
+    AsList n $ for i:(Fin n).
+      MkChar $ %ptrLoad (%ptrOffset ptr (ordinal i))
+
+instance showInt64 : Show Int64 where
+  show = \x: Int64.
+    (n, ptr) = %ffi showInt64 (Int32 & CharPtr) x
+    AsList n $ for i:(Fin n).
+      MkChar $ %ptrLoad (%ptrOffset ptr (ordinal i))
+
+instance showFloat32 : Show Float32 where
+  show = \x: Float32.
+    (n, ptr) = %ffi showFloat32 (Int32 & CharPtr) x
+    AsList n $ for i:(Fin n).
+      MkChar $ %ptrLoad (%ptrOffset ptr (ordinal i))
+
+instance showFloat64 : Show Float64 where
+  show = \x: Float64.
+    (n, ptr) = %ffi showFloat64 (Int32 & CharPtr) x
+    AsList n $ for i:(Fin n).
+      MkChar $ %ptrLoad (%ptrOffset ptr (ordinal i))
 
 '## Floating point helper functions
 

src/lib/dexrt.cpp

@@ -4,6 +4,8 @@
 // license that can be found in the LICENSE file or at
 // https://developers.google.com/open-source/licenses/bsd
 
+#include <cfloat>
+#include <cinttypes>
 #include <cstdio>
 #include <cstdint>
 #include <cstdlib>
@@ -13,7 +15,7 @@
 
 #ifdef DEX_CUDA
 #include <cuda.h>
-#endif
+#endif // DEX_CUDA
 
 extern "C" {
 
@@ -138,15 +140,48 @@ double randunif(uint64_t keypair) {
   return out - 1;
 }
 
-void showFloat(char **resultPtr, float x) {
-  auto p = reinterpret_cast<char*>(malloc_dex(100));
-  auto n = sprintf(p, "%.4f", x);
-  auto result1Ptr = reinterpret_cast<int32_t*>(resultPtr[0]);
-  auto result2Ptr = reinterpret_cast<char**>(  resultPtr[1]);
-  *result1Ptr = n;
-  *result2Ptr = p;
+// The string buffer size used for converting integer and floating-point types.
+static constexpr int showStringBufferSize = 32;
+
+void showInt32(char **resultPtr, int32_t x) {
+  auto buffer = reinterpret_cast<char *>(malloc_dex(showStringBufferSize));
+  auto length = snprintf(buffer, showStringBufferSize, "%" PRId32, x);
+  auto result1Ptr = reinterpret_cast<int32_t *>(resultPtr[0]);
+  auto result2Ptr = reinterpret_cast<char **>(resultPtr[1]);
+  *result1Ptr = length;
+  *result2Ptr = buffer;
+}
+
+void showInt64(char **resultPtr, int64_t x) {
+  auto buffer = reinterpret_cast<char *>(malloc_dex(showStringBufferSize));
+  auto length = snprintf(buffer, showStringBufferSize, "%" PRId64, x);
+  auto result1Ptr = reinterpret_cast<int32_t *>(resultPtr[0]);
+  auto result2Ptr = reinterpret_cast<char **>(resultPtr[1]);
+  *result1Ptr = length;
+  *result2Ptr = buffer;
+}
+
+void showFloat32(char **resultPtr, float x) {
+  auto buffer = reinterpret_cast<char *>(malloc_dex(showStringBufferSize));
+  auto length =
+      snprintf(buffer, showStringBufferSize, "%.*g", __FLT_DECIMAL_DIG__, x);
+  auto result1Ptr = reinterpret_cast<int32_t *>(resultPtr[0]);
+  auto result2Ptr = reinterpret_cast<char **>(resultPtr[1]);
+  *result1Ptr = length;
+  *result2Ptr = buffer;
+}
+
+void showFloat64(char **resultPtr, double x) {
+  auto buffer = reinterpret_cast<char *>(malloc_dex(showStringBufferSize));
+  auto length =
+      snprintf(buffer, showStringBufferSize, "%.*g", __DBL_DECIMAL_DIG__, x);
+  auto result1Ptr = reinterpret_cast<int32_t *>(resultPtr[0]);
+  auto result2Ptr = reinterpret_cast<char **>(resultPtr[1]);
+  *result1Ptr = length;
+  *result2Ptr = buffer;
 }
 
+
 #ifdef DEX_CUDA
 
 } // extern "C"
@@ -258,7 +293,7 @@ void dex_ensure_has_cuda_context() {
 
 #undef CHECK
 
-#endif
+#endif // DEX_CUDA
 
 int32_t dex_queryParallelismMC(int64_t iters) {
   int32_t nthreads = std::thread::hardware_concurrency();

stack-macos.yaml

@@ -13,6 +13,7 @@ extra-deps:
   - llvm-hs-9.0.1
   - llvm-hs-pure-9.0.0
   - megaparsec-8.0.0
+  - prettyprinter-1.6.2
 
 flags:
   llvm-hs: