Clarify JSON.asString in coercions section

examples/Examples/Classes.lean

@@ -1232,43 +1232,92 @@ book declaration {{{ JSON }}}
     | number : Float → JSON
     | object : List (String × JSON) → JSON
     | array : List JSON → JSON
+  deriving Repr
+stop book declaration
+
+
+
+expect info {{{ fiveZeros }}}
+  #eval (5 : Float).toString
+message
+"\"5.000000\""
+end expect
+
+
+book declaration {{{ Stringseparate }}}
+  def String.separate (sep : String) (strings : List String) : String :=
+    match strings with
+    | [] => ""
+    | x :: xs => String.join (x :: xs.map (sep ++ ·))
 stop book declaration
 
 
-def escapeChar : Char → List Char
-  | '\\' => ['\\', '\\']
-  | '"' => ['\\', '"']
-  | '\r' => ['\\', 'r']
-  | '\n' => ['\\', 'n']
-  | '/' => ['\\', '/']
-  | '\t' => ['\\', 't']
-  | c => [c]
 
-def escape (str : String) : String := ⟨ str.data.bind escapeChar ⟩
+expect info {{{ sep2ex }}}
+  #eval ", ".separate ["1", "2"]
+message
+"\"1, 2\""
+end expect
+
+
+expect info {{{ sep1ex }}}
+  #eval ", ".separate ["1"]
+message
+"\"1\""
+end expect
+
+
+expect info {{{ sep0ex }}}
+  #eval ", ".separate []
+message
+"\"\""
+end expect
+
+book declaration {{{ dropDecimals }}}
+  def dropDecimals (numString : String) : String :=
+    if numString.contains '.' then
+      let noTrailingZeros := numString.dropRightWhile (· == '0')
+      noTrailingZeros.dropRightWhile (· == '.')
+    else numString
+stop book declaration
 
 
-def mapCombineWith (f : α → β) (combine : β → β → β) (default : β) (xs : List α) : β :=
-  let rec go (acc : β) : List α → β
-       | [] => acc
-       | y :: ys => go (combine acc (f y)) ys
-  match xs with
-  | [] => default
-  | [x] => f x
-  | x :: x' :: xs => go (f x) (x' :: xs)
+expect info {{{ dropDecimalExample }}}
+  #eval dropDecimals (5 : Float).toString
+message
+"\"5\""
+end expect
+
+expect info {{{ dropDecimalExample2 }}}
+  #eval dropDecimals (5.2 : Float).toString
+message
+"\"5.2\""
+end expect
+
 
 
-partial def JSON.asString : JSON → String
-  | true => "true"
-  | false => "false"
-  | null => "null"
-  | string s => "\"" ++ escape s ++ "\""
-  | number n => n.toString.dropRightWhile (· == '0') |>.dropRightWhile (· == '.')
-  | object members =>
-    "{" ++ mapCombineWith (fun mem => "\"" ++ escape mem.fst ++ "\": " ++ asString mem.snd) (· ++ ", " ++ ·) "" members ++ "}"
-  | array elements =>
-    "[" ++ mapCombineWith asString (· ++ ", " ++ ·) "" elements ++ "]"
+expect info {{{ escapeQuotes }}}
+  #eval Lean.Json.escape "\"Hello!\""
+message
+"\"\\\\\\\"Hello!\\\\\\\"\""
+end expect
 
 
+book declaration {{{ JSONasString }}}
+  partial def JSON.asString (val : JSON) : String :=
+    match val with
+    | true => "true"
+    | false => "false"
+    | null => "null"
+    | string s => "\"" ++ Lean.Json.escape s ++ "\""
+    | number n => dropDecimals n.toString
+    | object members =>
+      let memberToString mem :=
+        "\"" ++ Lean.Json.escape mem.fst ++ "\": " ++ asString mem.snd
+      "{" ++ ", ".separate (members.map memberToString) ++ "}"
+    | array elements =>
+      "[" ++ ", ".separate (elements.map asString) ++ "]"
+stop book declaration
 
 book declaration {{{ Monoid }}}
   structure Monoid where
@@ -1395,6 +1444,18 @@ book declaration {{{ buildResponse }}}
 stop book declaration
 
 
+
+expect info {{{ buildResponseOut }}}
+  #eval buildResponse "Functional Programming in Lean" Str "Programming is fun!"
+message
+"JSON.object
+  [(\"title\", JSON.string \"Functional Programming in Lean\"),
+   (\"status\", JSON.number 200.000000),
+   (\"record\", JSON.string \"Programming is fun!\")]"
+end expect
+
+
+
 expect info {{{ buildResponseStr }}}
   #eval (buildResponse "Functional Programming in Lean" Str "Programming is fun!").asString
 message
@@ -1414,7 +1475,7 @@ argument
 has type
   NonEmptyList String : Type
 but is expected to have type
-  List ?m.32982 : Type ?u.32980"
+  List ?m.32938 : Type ?u.32936"
 end expect
 
 expect error {{{ lastSpiderC }}}

functional-programming-lean/src/title.md

@@ -9,7 +9,7 @@ This version of the text is written for Lean 4 release `{{#lean_version}}`.
 ## Release history
 
 ### November, 2022
-This release adds a chapter on programming with monads.
+This release adds a chapter on programming with monads. Additionally, the example of using JSON in the coercions section has been updated to include the complete code.
 
 ### October, 2022
 

functional-programming-lean/src/type-classes/coercion.md

@@ -218,12 +218,56 @@ Given this instance, a serializer can be applied directly to an argument:
 ```
 The serializer can be passed directly to `buildResponse`:
 ```lean
+{{#example_in Examples/Classes.lean buildResponseOut}}
+```
+```output info
+{{#example_out Examples/Classes.lean buildResponseOut}}
+```
+
+### Aside: JSON as a String
+
+It can be a bit difficult to understand JSON when encoded as Lean objects.
+To help make sure that the serialized response was what was expected, it can be convenient to write a simple converter from `JSON` to `String`.
+The first step is to simplify the display of numbers.
+`JSON` doesn't distinguish between integers and floating point numbers, and the type `Float` is used to represent both.
+In Lean, `Float.toString` includes a number of trailing zeros:
+```lean
+{{#example_in Examples/Classes.lean fiveZeros}}
+```
+```output info
+{{#example_out Examples/Classes.lean fiveZeros}}
+```
+The solution is to write a little function that cleans up the presentation by dropping all trailing zeros, followed by a trailing decimal point:
+```lean
+{{#example_decl Examples/Classes.lean dropDecimals}}
+```
+With this definition, `{{#example_in Examples/Classes.lean dropDecimalExample}}` yields `{{#example_out Examples/Classes.lean dropDecimalExample}}`, and `{{#example_in Examples/Classes.lean dropDecimalExample2}}` yields `{{#example_out Examples/Classes.lean dropDecimalExample2}}`.
+
+The next step is to define a helper function to append a list of strings with a separator in between them:
+```lean
+{{#example_decl Examples/Classes.lean Stringseparate}}
+```
+This function is useful to account for comma-separated elements in JSON arrays and objects.
+`{{#example_in Examples/Classes.lean sep2ex}}` yields `{{#example_out Examples/Classes.lean sep2ex}}`, `{{#example_in Examples/Classes.lean sep1ex}}` yields `{{#example_out Examples/Classes.lean sep1ex}}`, and `{{#example_in Examples/Classes.lean sep0ex}}` yields `{{#example_out Examples/Classes.lean sep0ex}}`.
+
+Finally, a string escaping procedure is needed for JSON strings, so that the Lean string containing `"Hello!"` can be output as `"\"Hello!\""`.
+Happily, Lean contains a function for escaping JSON strings already, called `Lean.Json.escape`.
+
+The function that emits a string from a `JSON` value is declared `partial` because Lean cannot see that it terminates.
+This is because recursive calls to `asString` occur in functions that are being applied by `List.map`, and this pattern of recursion is complicated enough that Lean cannot see that the recursive calls are actually being performed on smaller values.
+In an application that just needs to produce JSON strings and doesn't need to mathematically reason about the process, having the function be `partial` is not likely to cause problems.
+```lean
+{{#example_decl Examples/Classes.lean JSONasString}}
+```
+With this definition, the output of serialization is easier to read:
+```lean
 {{#example_in Examples/Classes.lean buildResponseStr}}
 ```
 ```output info
 {{#example_out Examples/Classes.lean buildResponseStr}}
 ```
 
+
 ## Messages You May Meet
 
 Natural number literals are overloaded with the `OfNat` type class.