Text/replace on interpolated text#1084
Conversation
This change to the beta normalization rules ensures that the normalization stays consistent.
The current haskell implementation currently has this weird behaviour:
```
➜ dhall repl
Welcome to the Dhall v1.35.0 REPL! Type :help for more information.
⊢ :let f = \(x : Text) -> Text/replace "a" "b" "a ${x} a"
f : ∀(x : Text) → Text
⊢ f "a"
"b a b"
⊢ let g = \(x : Text) -> Text/replace "a" "b" "a ${x} a" in g "a"
"b b b"
```
|
I believe that "require the haystack to be non-abstract before further reduction can occur" is the only sensible rule here. For example in |
|
Good point, I didn't think about this case. 😅 I will edit the changes to the spec to reflect this tomorrow! |
|
There is one slightly different rule possible. If the needle is empty, then the haystack does not need to be fully evaluated. So: Text/replace ""Could be normalized to: \(_replacement : Text) \(haystack : Text) -> haystackBut that goes against "builtins are fully saturated". So maybe just this: Text/replace "" replacement haystackIs normalized to: haystackRegardless of whether Is this something we might want? |
|
This special case feels like pretty low value, I’d rather stick with the general rule for all cases. |
|
While you're at it, could you also add a test for |
Gabriella439
left a comment
There was a problem hiding this comment.
Thank you for doing this! 🙂
|
As per the rules, I believe you can now merge this, since there are no objections |
|
Alright great! I've updated the branch. I don't think I have write access in this repo though, so someone else will have to merge this PR. 😄 |
|
@basile-henry: I just added you to the repository |
|
Great, thanks! 😄 |
|
You're welcome! 🙂 |
Previously, `Text/replace "foo" "bar${x}baz" "foofoo"` did not work as
expected. This fixes it by extracting the code from eval.go that
deals with evaluating Text into a textValBuilder struct, and then
reusing that textValBuilder in the Text/replace implementation.
This pins us to a dhall-lang commit just after
dhall-lang/dhall-lang#1084 was merged; this is
the same as verison 19.0.0 with a fix for
TestNormalization/unit/TextReplaceAbstractA.
This change to the beta normalization rules ensures that the normalization stays consistent.
The current haskell implementation has this weird behaviour:
As @Gabriel439 suggested in #1065 an alternative rule could be:
That would definitely be simpler to implement, but maybe not as strongly normalising as it could be.
Is there anything else I need to change? Should this change be documented somehow?
EDIT:
As @Nadrieril pointed out, Gabriel's suggestion really is the only rule possible here. I changed this PR to implement this suggestion instead! 😄