dhall-lang · alexhumphreys · Oct 10, 2020 · Sep 6, 2020 · Sep 7, 2020 · Sep 7, 2020
diff --git a/Prelude/Text/replace.dhall b/Prelude/Text/replace.dhall
@@ -0,0 +1,14 @@
+{-
+Replace a section of `Text` with another inside a `Text` literal.
+-}
+let replace
+    : ∀(needle : Text) → ∀(replacement : Text) → ∀(haystack : Text) → Text
+    = Text/replace
+
+let example0 = assert : replace "-" "_" "foo-bar" ≡ "foo_bar"
+
+let example1 = assert : replace "💣" "💥" "💣💣💣" ≡ "💥💥💥"
+
+let example2 = assert : replace "👨" "👩" "👨‍👩‍👧‍👦" ≡ "👩‍👩‍👧‍👦"
+
+in  replace
diff --git a/docs/howtos/Cheatsheet.md b/docs/howtos/Cheatsheet.md
@@ -112,6 +112,8 @@
     "ABC" ++ "DEF" = "ABCDEF"
 
     Text/show "Hello, world!" = "\"Hello, world!\""
+
+    Text/replace "-" "_" "foo-bar" = "foo_bar"
     ```
 
 ## Complex types

diff --git a/docs/references/Built-in-types.md b/docs/references/Built-in-types.md
@@ -815,6 +815,23 @@ string:
 "\"\\n🎉\""
 ```
 
+### Function `Text/replace`
+
+The `Text/replace` built-in function modifies a substring of a given `Text` literal. It takes 3 arguments, the `Text` literal substring to match, the `Text` literal replacement, and the `Text` literal in which to replace all matches:
+
+```dhall
+⊢ Text/replace "foo" "bar" "foobar"
+
+"barbar"
+```
+
+#### Type
+
+```
+──────────────────────────────────────
+Γ ⊢ Text/replace : ∀(needle : Text) → ∀(replacement : Text) → ∀(haystack : Text) → Text
+```
+
 #### Type
 
 ```

diff --git a/docs/tutorials/Language-Tour.md b/docs/tutorials/Language-Tour.md
@@ -910,6 +910,34 @@ You can concatenate `Text` literals using the `++` operator:
 "123456"
 ```
 
+It is also possible to replace substrings inside a Text literal. Say you have
+a name where you need to replace dashes with underscores. That can be achieved
+with the following:
+
+```dhall
+⊢ Text/replace "-" "_" "foo-bar-baz"
+
+"foo_bar_baz"
+```
+
+You can also replace larger sections of text:
+
+```dhall
+⊢ Text/replace "Hey" "Hello" "Hey, world!"
+
+"Hello, world!"
+```
+
+Here's how you would strip newlines from a multiline string:
+
+```dhall
+Text/replace "\n" " " ''
+  This now behaves like a YAML
+  "folded" multi-line string literal where
+  newlines are replaced with spaces
+''
+```
+
 Other than that, `Text` literals are essentially opaque.  You currently cannot
 parse `Text` literals nor can you compare them for equality.  This is because
 the language promotes using more precise types (like enums) instead of `Text`

diff --git a/standard/README.md b/standard/README.md
@@ -169,6 +169,7 @@ a, b, f, l, r, e, t, u, A, B, E, T, U, c, i, o
   / List/indexed                      ; Tag elements with index
   / List/reverse                      ; Reverse list
   / Text/show                         ; Convert Text to its own representation
+  / Text/replace                      ; Replace a section of a Text literal
   / Bool                              ; Bool type
   / Optional                          ; Optional type
   / Natural                           ; Natural type

diff --git a/standard/alpha-normalization.md b/standard/alpha-normalization.md
@@ -422,6 +422,10 @@ sub-expressions for the remaining rules:
     Text/show ↦ Text/show
 
 
+    ───────────────────────────
+    Text/replace ↦ Text/replace
+
+
     ───────────
     Bool ↦ Bool
 

diff --git a/standard/beta-normalization.md b/standard/beta-normalization.md
@@ -661,13 +661,54 @@ Or in other words:
     f a ⇥ "\"…\\n…\\u0024…\\\\…\\\"…\\u0000…\""
 
 
-Otherwise, in isolation `Text/show` is in normal form:
+`Text/replace` modifies a substring of a given `Text` literal. It takes 3
+arguments, the `Text` literal substring to match, the `Text` literal replacement,
+and the `Text` literal in which to replace all matches. In the case that the
+substring to replace is empty (`""`), then no replacement is performed:
+
+
+    f ⇥ Text/replace "" replacement   a ⇥ "foo"   ; No replacement performed if
+    ────────────────────────────────────────────  ; the search string is empty,
+    f a ⇥ "foo"                                   ; to avoid an infinite loop.
+
+
+    f ⇥ Text/replace "NEEDLE" replacement  ; If the "NEEDLE" is not found within
+    a ⇥ "other"                            ; the string, then perform no
+    ─────────────────────────────────────  ; replacement.
+    f a ⇥ "other"
+
+
+    f ⇥ Text/replace "NEEDLE" replacement  ; If the "NEEDLE" is found within
+    a ⇥ "beforeNEEDLEafter"                ; the string, then replace.
+    "before${replacement}" ++ Text/replace "NEEDLE" replacement "after" → e
+    ───────────────────────────────────────────────────────────────────────
+    f a ⇥ e
+
+
+    f ⇥ Text/replace "NEEDLE" replacement  ; The string has interpolation, but
+    a ⇥ "other${x}remainder…"              ; the prefix does not match.
+    "other${x}" ++ Text/replace "NEEDLE" "remainder…" → e
+    ─────────────────────────────────────────────────────
+    f a ⇥ e
+
+
+    f ⇥ Text/replace "NEEDLE" replacement  ; The string has interpolation, and
+    a ⇥ "beforeNEEDLEafter${x}remainder…"  ; the prefix matches.
+    "before${replacement}" ++ Text/replace "NEEDLE" "after${x}remainder…" → e
+    ─────────────────────────────────────────────────────────────────────────
+    f a ⇥ e
+
+
+All of the built-in functions on `Text` are in normal form:
 
 
     ─────────────────────
     Text/show ⇥ Text/show
 
-
+    ───────────────────────────
+    Text/replace ⇥ Text/replace
+
+
 ## `List`
 
 The `List` type-level function is in normal form:

diff --git a/standard/binary.md b/standard/binary.md
@@ -267,6 +267,10 @@ matching their identifier.
     encode(Text/show) = "Text/show"
 
 
+    ─────────────────────────────────────
+    encode(Text/replace) = "Text/replace"
+
+
     ─────────────────────────
     encode(Bool) = "Bool"
 
@@ -987,6 +991,10 @@ a built-in identifier if it matches any of the following strings:
     decode("List/reverse") = List/reverse
 
 
+    ─────────────────────────────────────
+    decode("Text/replace") = Text/replace
+
+
     ───────────────────────────────
     decode("Text/show") = Text/show
 

diff --git a/standard/dhall.abnf b/standard/dhall.abnf
@@ -412,6 +412,7 @@ builtin =
     / List-indexed
     / List-reverse
     / Text-show
+    / Text-replace
     / Bool
     / True
     / False
@@ -464,6 +465,7 @@ List-last         = %x4c.69.73.74.2f.6c.61.73.74
 List-indexed      = %x4c.69.73.74.2f.69.6e.64.65.78.65.64
 List-reverse      = %x4c.69.73.74.2f.72.65.76.65.72.73.65
 Text-show         = %x54.65.78.74.2f.73.68.6f.77
+Text-replace      = %x54.65.78.74.2f.72.65.70.6c.61.63.65
 
 ; Operators
 combine       = %x2227 / "/\"

diff --git a/standard/shift.md b/standard/shift.md
@@ -489,6 +489,10 @@ The remaining rules are:
     ↑(d, x, m, Text/show) = Text/show
 
 
+    ───────────────────────────────────────
+    ↑(d, x, m, Text/replace) = Text/replace
+
+
     ───────────────────────
     ↑(d, x, m, Bool) = Bool
 

diff --git a/standard/substitution.md b/standard/substitution.md
@@ -470,6 +470,10 @@ The remaining rules are:
     Text/show[x@n ≔ e] = Text/show
 
 
+    ────────────────────────────────────
+    Text/replace[x@n ≔ e] = Text/replace
+
+
     ────────────────────
     Bool[x@n ≔ e] = Bool
 

diff --git a/standard/type-inference.md b/standard/type-inference.md
@@ -275,6 +275,13 @@ The `Text` show function has the following type:
     Γ ⊢ Text/show : Text → Text
 
 
+The `Text/replace` function has the following type:
+
+
+    ───────────────────────────────────────────────────────────────────────────────────────
+    Γ ⊢ Text/replace : ∀(needle : Text) → ∀(replacement : Text) → ∀(haystack : Text) → Text
+
+
 The `Text` concatenation operator takes arguments of type `Text` and returns a
 result of type `Text`:
 

diff --git a/tests/normalization/success/unit/TextReplaceAbstractA.dhall b/tests/normalization/success/unit/TextReplaceAbstractA.dhall
@@ -0,0 +1,4 @@
+{- This test verifies that an implementation correctly permits both the
+   "replacement" and the "haystack" to be abstract.
+-}
+λ(x : Text) → λ(y : Text) → Text/replace "a" "-${x}-" "_a_${y}_a_"
diff --git a/tests/normalization/success/unit/TextReplaceAbstractB.dhall b/tests/normalization/success/unit/TextReplaceAbstractB.dhall
@@ -0,0 +1 @@
+λ(x : Text) → λ(y : Text) → "_-${x}-_${y}_-${x}-_"
diff --git a/tests/normalization/success/unit/TextReplaceEmptyA.dhall b/tests/normalization/success/unit/TextReplaceEmptyA.dhall
@@ -0,0 +1 @@
+Text/replace "" "bar" "foo"
diff --git a/tests/normalization/success/unit/TextReplaceEmptyB.dhall b/tests/normalization/success/unit/TextReplaceEmptyB.dhall
@@ -0,0 +1 @@
+"foo"
diff --git a/tests/normalization/success/unit/TextReplaceMultipleA.dhall b/tests/normalization/success/unit/TextReplaceMultipleA.dhall
@@ -0,0 +1 @@
+Text/replace "foo" "bar" "foobazfoo"
diff --git a/tests/normalization/success/unit/TextReplaceMultipleB.dhall b/tests/normalization/success/unit/TextReplaceMultipleB.dhall
@@ -0,0 +1 @@
+"barbazbar"
diff --git a/tests/normalization/success/unit/TextReplaceNFCUnicodeA.dhall b/tests/normalization/success/unit/TextReplaceNFCUnicodeA.dhall
@@ -0,0 +1 @@
+Text/replace "👨" "👩" "👨‍👩‍👧‍👦"
diff --git a/tests/normalization/success/unit/TextReplaceNFCUnicodeB.dhall b/tests/normalization/success/unit/TextReplaceNFCUnicodeB.dhall
@@ -0,0 +1 @@
+"👩‍👩‍👧‍👦"
diff --git a/tests/normalization/success/unit/TextReplaceNormalizationA.dhall b/tests/normalization/success/unit/TextReplaceNormalizationA.dhall
@@ -0,0 +1,3 @@
+-- This test verifies that implementations do not perform Unicode normalization
+-- before substitution.
+Text/replace "a\u{0301}" "b" "\u{00e1}c"
diff --git a/tests/normalization/success/unit/TextReplaceNormalizationB.dhall b/tests/normalization/success/unit/TextReplaceNormalizationB.dhall
@@ -0,0 +1 @@
+"ác"
diff --git a/tests/normalization/success/unit/TextReplaceSimpleA.dhall b/tests/normalization/success/unit/TextReplaceSimpleA.dhall
@@ -0,0 +1 @@
+Text/replace "foo" "bar" "foo"
diff --git a/tests/normalization/success/unit/TextReplaceSimpleB.dhall b/tests/normalization/success/unit/TextReplaceSimpleB.dhall
@@ -0,0 +1 @@
+"bar"
diff --git a/tests/normalization/success/unit/TextReplaceUnicodeA.dhall b/tests/normalization/success/unit/TextReplaceUnicodeA.dhall
@@ -0,0 +1 @@
+Text/replace "💣" "💥" "💣💣💣"
diff --git a/tests/normalization/success/unit/TextReplaceUnicodeB.dhall b/tests/normalization/success/unit/TextReplaceUnicodeB.dhall
@@ -0,0 +1 @@
+"💥💥💥"
diff --git a/tests/parser/success/builtinsA.dhall b/tests/parser/success/builtinsA.dhall
@@ -19,6 +19,7 @@
 , List/indexed
 , List/reverse
 , Text/show
+, Text/replace
 , Bool
 , True
 , False

diff --git a/tests/parser/success/builtinsB.dhallb b/tests/parser/success/builtinsB.dhallb
@@ -1 +1 @@
-�$�lNatural/foldmNatural/buildnNatural/isZerolNatural/evenkNatural/oddqNatural/toIntegerlNatural/showpInteger/toDoublelInteger/shownInteger/negatemInteger/clamppNatural/subtractkDouble/showjList/buildiList/foldkList/lengthiList/headiList/lastlList/indexedlList/reverseiText/showdBool��hOptionaldNonegNaturalgIntegerfDoubledTextdListdTypedKinddSort
+�%�lNatural/foldmNatural/buildnNatural/isZerolNatural/evenkNatural/oddqNatural/toIntegerlNatural/showpInteger/toDoublelInteger/shownInteger/negatemInteger/clamppNatural/subtractkDouble/showjList/buildiList/foldkList/lengthiList/headiList/lastlList/indexedlList/reverseiText/showlText/replacedBool��hOptionaldNonegNaturalgIntegerfDoubledTextdListdTypedKinddSort
diff --git a/tests/parser/success/builtinsB.diag b/tests/parser/success/builtinsB.diag
@@ -1 +1 @@
-[4, null, "Natural/fold", "Natural/build", "Natural/isZero", "Natural/even", "Natural/odd", "Natural/toInteger", "Natural/show", "Integer/toDouble", "Integer/show", "Integer/negate", "Integer/clamp", "Natural/subtract", "Double/show", "List/build", "List/fold", "List/length", "List/head", "List/last", "List/indexed", "List/reverse", "Text/show", "Bool", true, false, "Optional", "None", "Natural", "Integer", "Double", "Text", "List", "Type", "Kind", "Sort"]
+[4, null, "Natural/fold", "Natural/build", "Natural/isZero", "Natural/even", "Natural/odd", "Natural/toInteger", "Natural/show", "Integer/toDouble", "Integer/show", "Integer/negate", "Integer/clamp", "Natural/subtract", "Double/show", "List/build", "List/fold", "List/length", "List/head", "List/last", "List/indexed", "List/reverse", "Text/show", "Text/replace", "Bool", true, false, "Optional", "None", "Natural", "Integer", "Double", "Text", "List", "Type", "Kind", "Sort"]
diff --git a/tests/type-inference/success/unit/TextReplaceA.dhall b/tests/type-inference/success/unit/TextReplaceA.dhall
@@ -0,0 +1 @@
+Text/replace
diff --git a/tests/type-inference/success/unit/TextReplaceB.dhall b/tests/type-inference/success/unit/TextReplaceB.dhall
@@ -0,0 +1 @@
+∀(needle : Text) → ∀(replacement : Text) → ∀(haystack : Text) → Text