Pretty-print n => Char tables as string literals.

Make `prettyVal` print `n => Char` tables as string literals.

Add `make update-all` command for updating all test files.
Update tests.

examples/eval-tests.dx

@@ -764,12 +764,12 @@ hard = [(-1000.0), 1000.0, 1000.0, 0.1, 0.0]
 str = ['x', 'y']
 
 :p str
-> ['x', 'y']
+> "xy"
 
 s1 = "hello world"
 
 :p s1
-> ['h', 'e', 'l', 'l', 'o', ' ', 'w', 'o', 'r', 'l', 'd']
+> "hello world"
 
 :p codepoint 'a'
 > 97

examples/serialize-tests.dx

@@ -19,13 +19,17 @@
 :p ()
 > ()
 
+x = "ab"
+:p for i,j. [x.i, x.j]
+> ["aa", "ab", "ba", "bb"]@(Fin 2 & Fin 2)
+
 'Records and variants
 
 :p {a=1, b=2}
 > {a = 1, b = 2}
 
 :p {a="1234", b=[1, 2, 3]}
-> {a = ['1', '2', '3', '4'], b = [1, 2, 3]}
+> {a = "1234", b = [1, 2, 3]}
 
 :p [{| a=1 |}, {| b=2.0 |}] : (Fin 2) => {a:Int | b:Float}
 > [{| a = 1 |}, {| b = 2.0 |}]

examples/show-tests.dx

@@ -3,46 +3,46 @@
 -- Int32
 
 :p show (1234: Int32)
-> (AsList 4 ['1', '2', '3', '4'])
+> (AsList 4 "1234")
 
 :p show (-1234: Int32)
-> (AsList 5 ['-', '1', '2', '3', '4'])
+> (AsList 5 "-1234")
 
 :p show ((FToI (-(pow 2. 31.))): Int32)
-> (AsList 11 ['-', '2', '1', '4', '7', '4', '8', '3', '6', '4', '8'])
+> (AsList 11 "-2147483648")
 
 -- Int64
 
 :p show (IToI64 1234: Int64)
-> (AsList 4 ['1', '2', '3', '4'])
+> (AsList 4 "1234")
 
 -- 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'])
+> (AsList 10 "4294966062")
 
 -- Float32
 
 :p show (123.456789: Float32)
-> (AsList 10 ['1', '2', '3', '.', '4', '5', '6', '7', '8', '7'])
+> (AsList 10 "123.456787")
 
 :p show ((pow 2. 16.): Float32)
-> (AsList 5 ['6', '5', '5', '3', '6'])
+> (AsList 5 "65536")
 
 -- 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'])
+> (AsList 3 "nan")
 
 -- 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'])
+> (AsList 3 "inf")
 
 -- Note: `show infinity` (Dex runtime dtoa implementation) appears different from
 -- `:p nan` (Dex interpreter implementation).
@@ -52,36 +52,21 @@
 -- Float64
 
 :p show (FToF64 123.456789: Float64)
-> (AsList 16 [ '1'
->            , '2'
->            , '3'
->            , '.'
->            , '4'
->            , '5'
->            , '6'
->            , '7'
->            , '8'
->            , '7'
->            , '1'
->            , '0'
->            , '9'
->            , '3'
->            , '7'
->            , '5' ])
+> (AsList 16 "123.456787109375")
 
 :p show (FToF64 (pow 2. 16.): Float64)
-> (AsList 5 ['6', '5', '5', '3', '6'])
+> (AsList 5 "65536")
 
 :p show ((FToF64 nan): Float64)
-> (AsList 3 ['n', 'a', 'n'])
+> (AsList 3 "nan")
 
 -- 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'])
+> (AsList 3 "inf")
 
 -- Note: `show infinity` (Dex runtime dtoa implementation) appears different from
 -- `:p nan` (Dex interpreter implementation).

makefile

@@ -85,6 +85,8 @@ example-names = uexpr-tests adt-tests type-tests eval-tests show-tests \
 
 quine-test-targets = $(example-names:%=run-%)
 
+update-targets = $(example-names:%=update-%)
+
 doc-names = $(example-names:%=doc/%.html)
 
 tests: quine-tests repl-test export-tests
@@ -101,6 +103,8 @@ run-%: examples/%.dx build
 prop-tests: cbits/libdex.so
 	$(STACK) test $(PROF)
 
+update-all: $(update-targets)
+
 update-%: export DEX_ALLOW_CONTRACTIONS=0
 update-%: examples/%.dx build
 	$(dex) script --allow-errors $< > $<.tmp

src/lib/Serialize.hs

@@ -36,19 +36,30 @@ getDexString (DataCon _ _ 0 [_, xs]) = do
     return $ toEnum $ fromIntegral c
 getDexString x = error $ "Not a string: " ++ pprint x
 
+-- Pretty-print values, e.g. for displaying in the REPL.
 -- This doesn't handle parentheses well. TODO: treat it more like PrettyPrec
 prettyVal :: Val -> IO (Doc ann)
 prettyVal val = case val of
-  Lam abs@(Abs b (TabArrow, _)) -> do
+  -- Pretty-print tables.
+  Lam abs@(Abs b (TabArrow, body)) -> do
+    -- Pretty-print index set.
     let idxSet = binderType b
+    let idxSetDoc = case idxSet of
+          Fin _ -> mempty               -- (Fin n) is not shown
+          _     -> "@" <> pretty idxSet -- Otherwise, show index set
+    -- Pretty-print elements.
     idxs <- indices idxSet
     elems <- forM idxs $ \idx -> do
-      ans <- evalBlock mempty $ snd $ applyAbs abs idx
-      asStr <$> prettyVal ans
-    let idxSetStr = case idxSet of
-                      FixedIntRange l _ | l == 0 -> mempty
-                      _                          -> "@" <> pretty idxSet
-    return $ pretty elems <> idxSetStr
+      atom <- evalBlock mempty $ snd $ applyAbs abs idx
+      case atom of
+        CharLit c -> return $ showChar (toEnum @Char $ fromIntegral c) ""
+        _         -> pprintVal atom
+    let bodyType = getType body
+    let elemsDoc = case bodyType of
+          -- Print table of characters as a string literal.
+          CharTy -> pretty ('"': concat elems ++ "\"")
+          _      -> pretty elems
+    return $ elemsDoc <> idxSetDoc
   DataCon (DataDef _ _ dataCons) _ con args ->
     case args of
       [] -> return $ pretty conName