String Functions in Idris

import Data.String

-- We alias putStrLn to a shorter name as we'll use it a lot below.
p : String -> IO ()
p = putStrLn

main : IO ()
main = do
    -- Here's a sample of the functions available for string manipulation in Idris.
    -- Since these are functions from the Data.String module, not methods on the string object itself,
    -- we need to pass the string in question as an argument to the function.
    -- You can find more functions in the Data.String module documentation.

    p $ "Contains:  " ++ show (isInfixOf "es" "test")
    p $ "Count:     " ++ show (length $ filter (== 't') "test")
    p $ "HasPrefix: " ++ show (isPrefixOf "te" "test")
    p $ "HasSuffix: " ++ show (isSuffixOf "st" "test")
    p $ "Index:     " ++ show (findIndex (== 'e') "test")
    p $ "Join:      " ++ join "-" ["a", "b"]
    p $ "Repeat:    " ++ replicate 5 'a'
    p $ "Replace:   " ++ replace "o" "0" "foo"
    p $ "Replace:   " ++ replaceOnce "o" "0" "foo"
    p $ "Split:     " ++ show (split (\c -> c == '-') "a-b-c-d-e")
    p $ "ToLower:   " ++ toLower "TEST"
    p $ "ToUpper:   " ++ toUpper "test"

This Idris code demonstrates various string manipulation functions. Here’s a breakdown of the functions used:

1. isInfixOf: Checks if a string is a substring of another string.
2. filter and length: Used together to count occurrences of a character.
3. isPrefixOf: Checks if a string starts with a given prefix.
4. isSuffixOf: Checks if a string ends with a given suffix.
5. findIndex: Finds the index of the first occurrence of a character.
6. join: Joins a list of strings with a separator.
7. replicate: Repeats a character a given number of times.
8. replace: Replaces all occurrences of a substring.
9. replaceOnce: Replaces the first occurrence of a substring.
10. split: Splits a string into a list of substrings based on a predicate.
11. toLower: Converts a string to lowercase.
12. toUpper: Converts a string to uppercase.

Note that Idris doesn’t have a built-in strings package like Go. Instead, these functions are part of the Data.String module. The syntax and function names might differ slightly from Go, but the functionality is similar.

To run this program, save it as StringFunctions.idr and use the Idris compiler:

$ idris StringFunctions.idr -o StringFunctions
$ ./StringFunctions
Contains:  True
Count:     2
HasPrefix: True
HasSuffix: True
Index:     Just 1
Join:      a-b
Repeat:    aaaaa
Replace:   f00
Replace:   f0o
Split:     ["a", "b", "c", "d", "e"]
ToLower:   test
ToUpper:   TEST

This example demonstrates how to perform various string operations in Idris, providing a starting point for more complex string manipulations in your programs.