Refactor string functions, rewrite tests #2235

dignissimus · 2021-12-31T08:37:26Z

Resolves #2172

Z-snails · 2021-12-31T09:34:23Z

You need to add the test to tests/Main.idr for it to actually run.
Edit: I would suggest adding a new TestPool, eg using testsInDir

buzden · 2021-12-31T10:29:25Z

libs/base/Data/String.idr

+unlines [""] = "\n"
+unlines = join "\n"


All patterns in pattern matching must have the same count of arguments they are matching at, so you'd better to have unlines ss = join "\n" ss for the second line.

Anyway, this implementation is not equivalent to the current unlines implementation. For example, unlines ["", ""] now gives "\n\n", your implementation gives "\n".

Just to further the point made in the above comment, here's a reference to when the semantics of lines/unlines were most recently changed: #1585

That is, the current semantics were intentional instead of accidental so we should honor them in the changes made in this PR. That might make the suggestion of using join less obvious of a win, at least for unlines, though I wish I'd thought to mention that on the open GitHub ticket in the first place.

Should unlines be written to use join? I ended up writing the following which doesn't include join so I'm considering reverting this specific change since it won't be any different to the original code.

Idris2/libs/base/Data/String.idr

Lines 147 to 149 in 5433275

unlines : List String -> String

unlines [] = ""

unlines (x::xs) = (x ++ "\n") ++ (unlines xs)

Since the function isn't publicly exported and it is transformed to fastUnlines at runtime, I suppose it's neither here nor there whether it unpacks and runs on characters or not. I think I slightly prefer your new approach personally.

buzden · 2021-12-31T10:29:29Z

libs/base/Data/String.idr

@@ -1,5 +1,6 @@
 module Data.String

+import Data.String.Extra


This looks like a dependency of base to contrib which should not be. I think it's better to move join function from contrib to base for that case.

Big +1 from me on moving join from contrib to base.

Idris2/libs/base/Data/String.idr

Lines 41 to 52 in 5433275

||| Remove the first `n` characters from a string. Returns the empty string if

||| the input string is too short.

public export

drop : (n : Nat) -> (input : String) -> String

drop n str = substr n (length str) str

||| Concatenate the strings from a `Foldable` containing strings, separated by

||| the given string.

public export

join : (sep : String) -> Foldable t => (xs : t String) -> String

join sep xs = drop (length sep)

(foldl (\acc, x => acc ++ sep ++ x) "" xs)

How's this?

mattpolzin · 2022-01-01T16:12:31Z

You've gone a different direction with your test file -- making a single file and name spacing it by folder in a way that reminds me of unit tests instead of sequentially increasing test folders.

Your approach to the rename both makes sense to me and at the same time makes me wonder if it forces an awkward middle ground between the golden testing we have today and the unit testing we would ideally want for a module in the base library but cannot have yet because our test harness only supports golden.

So, I'm on the fence about the file renames and relocation within the test folders, but aside from that (as noted above by @Z-snails) , you'll need to add the test to the Main file in the test harness for it to be picked up (it isn't running right now).

mattpolzin · 2022-01-02T17:43:07Z

Right now you've got some build failures in the compiler where you've added functions to Data.String that were previously added to the compiler's internal Libraries.Data.String.Extra.

We can't remove the definitions from Libraries.Data.String.Extra until after the next release because the compiler depends on base and needs to be able to build against the previous version of base (before you added those functions to base).

This is awkward, but not uncommon when working in the compiler codebase. You should be able to add %hide Data.String.join (and for drop) to the top of files that currently use those functions. You could also modify those files in the compiler to fully qualify their calls to the functions as Libraries.Data.String.Extra.join.

After the next release, that workaround can be removed (as is done in another currently open PR for a similar reason: #2230).

mattpolzin · 2022-01-02T17:45:39Z

I'm immediately thinking the circumstance is different here and the compiler should I think complain if you try to hide the version you're adding now before it's available in the previous version of base.

You'll probably need to use the second approach I mentioned of fully qualifying the calls to Libraries.Data.String.Extra.

mattpolzin · 2022-01-05T15:22:54Z

libs/contrib/Data/String/Extra.idr

@@ -63,19 +63,19 @@ drop n str = substr n (length str) str
 ||| the input string is too short.
 public export
 dropLast : (n : Nat) -> (input : String) -> String
-dropLast n str = reverse (drop n (reverse str))
+dropLast n str = reverse (Libraries.Data.String.Extra.drop n (reverse str))


Sorry my previous comment was unclear. This fully qualified call change is necessary inside the compiler codebase but in contrib (this file), there won't be ambiguity -- more importantly, the Libraries.Data.String.Extra module is not accessible from contrib.

In short, just revert the changes to this file.

ProofOfKeags · 2022-06-27T21:57:33Z

Is this dead? Should I revive the effort in a different PR?

andrevidela · 2023-06-14T11:15:06Z

Given that this has gone stale for quite a while I'm going to close this. If someone else wants to try again, feel free (@ProofOfKeags)

dignissimus added 2 commits December 31, 2021 08:33

Refactor string functions, rewrite tests

09dcc1f

Clean up code, to prepare future work

de55289

buzden reviewed Dec 31, 2021

View reviewed changes

dignissimus added 2 commits January 1, 2022 00:57

Move join, drop into base. Rewrite unlines

087ddd7

Include final part of previous commit

5433275

dignissimus added 2 commits January 1, 2022 18:01

Fix up proof, minor refactor

463f63e

Add test to Main.idr

ebfac45

dignissimus added 3 commits January 3, 2022 00:05

Re-add join, drop to contrib (partially revert 087ddd7)

8c98d00

Fully qualify calls to Data.String.Extra.join

1795a83

Fully qualify calls to Libraries.Data.String.Extra.drop from contrib

ff45eda

mattpolzin reviewed Jan 6, 2022

View reviewed changes

gallais force-pushed the main branch 2 times, most recently from 20718fd to 2c9bf24 Compare February 3, 2022 18:41

andrevidela closed this Jun 14, 2023

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

Uh oh!

Refactor string functions, rewrite tests #2235

Refactor string functions, rewrite tests #2235

Uh oh!

dignissimus commented Dec 31, 2021

Uh oh!

Z-snails commented Dec 31, 2021 •

edited

Loading

Uh oh!

buzden Dec 31, 2021

Uh oh!

mattpolzin Dec 31, 2021

Uh oh!

dignissimus Jan 1, 2022

Uh oh!

mattpolzin Jan 1, 2022

Uh oh!

buzden Dec 31, 2021

Uh oh!

mattpolzin Dec 31, 2021

Uh oh!

dignissimus Jan 1, 2022

Uh oh!

mattpolzin commented Jan 1, 2022

Uh oh!

mattpolzin commented Jan 2, 2022

Uh oh!

mattpolzin commented Jan 2, 2022

Uh oh!

mattpolzin Jan 5, 2022

Uh oh!

ProofOfKeags commented Jun 27, 2022

Uh oh!

andrevidela commented Jun 14, 2023

Uh oh!

Uh oh!

	unlines : List String -> String
	unlines [] = ""
	unlines (x::xs) = (x ++ "\n") ++ (unlines xs)

	\|\|\| Remove the first `n` characters from a string. Returns the empty string if
	\|\|\| the input string is too short.
	public export
	drop : (n : Nat) -> (input : String) -> String
	drop n str = substr n (length str) str

	\|\|\| Concatenate the strings from a `Foldable` containing strings, separated by
	\|\|\| the given string.
	public export
	join : (sep : String) -> Foldable t => (xs : t String) -> String
	join sep xs = drop (length sep)
	(foldl (\acc, x => acc ++ sep ++ x) "" xs)

Refactor string functions, rewrite tests #2235

Refactor string functions, rewrite tests #2235

Uh oh!

Conversation

dignissimus commented Dec 31, 2021

Uh oh!

Z-snails commented Dec 31, 2021 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

mattpolzin commented Jan 1, 2022

Uh oh!

mattpolzin commented Jan 2, 2022

Uh oh!

mattpolzin commented Jan 2, 2022

Uh oh!

Choose a reason for hiding this comment

Uh oh!

ProofOfKeags commented Jun 27, 2022

Uh oh!

andrevidela commented Jun 14, 2023

Uh oh!

Uh oh!

Z-snails commented Dec 31, 2021 •

edited

Loading