Refactor string functions, rewrite tests

[dignissimus]

Resolves #2172

[Z-snails]

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

[mattpolzin]

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]

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: https://github.com/idris-lang/Idris2/pull/2230).

[mattpolzin]

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.

[ProofOfKeags]

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

[andrevidela]

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)