Skip to content
Permalink
Browse files

Add `Text/show` built-in (#365)

There are two motivations for adding this built-in:

* For consistency with `Natural/show`, `Integer/show`, etc.

* To enable the implementation of a Dhall-to-JSON conversion in pure Dhall

  ... as described in:

  #336 (comment)

Carefully note that dollar signs are escaped as `\u0024` because that is the
only representation that is both JSON-compatible (since JSON does not
support the `\$` escape sequence) and Dhall-compatible (since failure to
escape `$` may accidentally generate an unintended string interpolation).
  • Loading branch information...
Gabriel439 committed Feb 13, 2019
1 parent 471037f commit 4085530bc37477f86ab24f99dbdc80988639d583
@@ -6,4 +6,6 @@
./concatMapSep
, concatSep =
./concatSep
, show =
./show
}
@@ -0,0 +1,13 @@
{-
Render a `Text` literal as its own representation as Dhall source code (i.e. a
double-quoted string literal)

Examples:

```
./show "ABC" = "\"ABC\""

./show "\u0000 \$ \\ \n \u263a" = "\"\\u0000 \\u0024 \\\\ \\n ☺\""
```
-}
let show : Text → Text = Text/show in show
@@ -259,6 +259,10 @@ string matching their identifier.
encode(Optional/build) = "Optional/build"
───────────────────────────────
encode(Text/show) = "Text/show"
─────────────────────────
encode(Bool) = "Bool"
@@ -880,6 +884,10 @@ identifier if it matches any of the following strings:
decode("Optional/build") = Optional/build
───────────────────────────────
decode("Text/show") = Text/show
─────────────────────────
decode("Bool") = Bool
@@ -177,6 +177,7 @@ HEXDIG = DIGIT / "A" / "B" / "C" / "D" / "E" / "F"
; * List/reverse
; * Optional/fold
; * Optional/build
; * Text/show
; * if
; * then
; * else
@@ -315,6 +316,7 @@ List-indexed-raw = %x4c.69.73.74.2f.69.6e.64.65.78.65.64
List-reverse-raw = %x4c.69.73.74.2f.72.65.76.65.72.73.65
Optional-fold-raw = %x4f.70.74.69.6f.6e.61.6c.2f.66.6f.6c.64
Optional-build-raw = %x4f.70.74.69.6f.6e.61.6c.2f.62.75.69.6c.64
Text-show-raw = %x54.65.78.74.2f.73.68.6f.77
Bool-raw = %x42.6f.6f.6c
Optional-raw = %x4f.70.74.69.6f.6e.61.6c
None-raw = %x4e.6f.6e.65
@@ -368,6 +370,7 @@ reserved-namespaced-raw =
/ List-reverse-raw
/ Optional-fold-raw
/ Optional-build-raw
/ Text-show-raw

reserved = reserved-raw whitespace
reserved-namespaced = reserved-namespaced-raw whitespace
@@ -183,10 +183,10 @@ a, b, f, l, r, e, t, u, A, B, E, T, U, c, i, o
/ Natural/even ; Test if even
/ Natural/odd ; Test if odd
/ Natural/toInteger ; Convert Natural to Integer
/ Natural/show ; Convert Natural to Text
/ Natural/show ; Convert Natural to Text representation
/ Integer/toDouble ; Convert Integer to Double
/ Integer/show ; Convert Integer to Text
/ Double/show ; Convert Double to Text
/ Integer/show ; Convert Integer to Text representation
/ Double/show ; Convert Double to Text representation
/ List/build ; List introduction
/ List/fold ; List elimination
/ List/length ; Length of list
@@ -196,6 +196,7 @@ a, b, f, l, r, e, t, u, A, B, E, T, U, c, i, o
/ List/reverse ; Reverse list
/ Optional/fold ; Optional introduction
/ Optional/build ; Optional elimination
/ Text/show ; Convert Text to its own representation
/ Bool ; Bool type
/ Optional ; Optional type
/ Natural ; Natural type
@@ -831,6 +832,10 @@ The remaining rules are:
↑(d, x, m, Optional/build) = Optional/build


─────────────────────────────────
↑(d, x, m, Text/show) = Text/show


───────────────────────
↑(d, x, m, Bool) = Bool

@@ -1381,6 +1386,10 @@ The remaining rules are:
Optional/build[x@n ≔ e] = Optional/build


──────────────────────────────
Text/show[x@n ≔ e] = Text/show


────────────────────
Bool[x@n ≔ e] = Bool

@@ -1854,6 +1863,10 @@ sub-expressions for the remaining rules:
Optional/build ↦ Optional/build
─────────────────────
Text/show ↦ Text/show
───────────
Bool ↦ Bool
@@ -2434,6 +2447,57 @@ any interpolated expression that normalize to `Text` literals:
"s₀${t₀}ss₀…" ⇥ "s₀${t₁}ss₁…"


The `Text/show` function replaces a `Text` literal with another `Text` literal
representing valid Dhall source code for the original literal. In particular,
this function both quotes and escapes the original literal so that if you were
to render the escaped `Text` value the result would appear to be the original
`Text` input to the function:

-- Rendering the right-hand side gives the original argument: "abc\ndef"
Text/show "abc\ndef" = "\"abc\\ndef\""

Escaping is done in such a way that the rendered result is not only valid
Dhall source code but also valid JSON when the `Text` does not contain any
Unicode code points above `\uFFFF`. This comes in handy if you want to use
Dhall to generate Dhall code or to generate JSON.

The body of the `Text` literal escapes the following characters according to
these rules:

* `"``\"`
* `$``\u0024`
* `\``\\`
* `\b``\\b`
* `\f``\\f`
* `\n``\\n`
* `\r``\\r`
* `\t``\\t`

Carefully note that `$` is not escaped as `\$` since that is not a valid JSON
escape sequence.

`Text/show` also escapes any non-printable characters as their Unicode escape
sequences:

* `\u0000`-`\u001F``\\u0000`-`\\u001F`

... since that is the only valid way to represent them within the Dhall grammar.

Or in other words:


f ⇥ Text/show a ⇥ "…\n\$\\\"\u0000…"
──────────────────────────────────────────
f a ⇥ "\"\\n…\\u0024…\\\\\\\"\\u0000…\""


Otherwise, in isolation `Text/show` is in normal form:


─────────────────────
Text/show ⇥ Text/show


Use machine concatenation to simplify the "text concatenation" operator if both
arguments normalize to uninterpolated `Text` literals:

@@ -3574,6 +3638,13 @@ The built-in functions on `Natural` numbers have the following types:
Γ ⊢ "s${t}ss…" : Text


The `Text` show function has the following type:


───────────────────────────
Γ ⊢ Text/show : Text → Text


The `Text` concatenation operator takes arguments of type `Text` and returns a
result of type `Text`:

@@ -0,0 +1 @@
(../../../../../../Prelude/package.dhall).`Text`.show "ABC"
@@ -0,0 +1 @@
(../../../../../../Prelude/package.dhall).`Text`.show "\u0000 \$ \\ \n \u263a"
@@ -0,0 +1 @@
"\"\\u0000 \\u0024 \\\\ \\n ☺\""

0 comments on commit 4085530

Please sign in to comment.
You can’t perform that action at this time.