Add isSubstr to Util

This commit is contained in:
Nathan McCarty 2025-01-07 11:46:49 -05:00
parent adc6b0a4a6
commit 9301eb303c

View file

@ -6,6 +6,7 @@ This module contains functions that extend the functionality of standard data ty
module Util
import Data.SortedSet
import Data.String
%default total
```
@ -66,3 +67,34 @@ Count the number of elements in a sorted set
length : SortedSet k -> Nat
length x = foldl (\acc, e => acc + 1) 0 x
```
## String
Extend `Data.String`
<!-- idris
namespace String
-->
### isSubstr
Returns `True` if `needle` is a substring of `haystack`
We first check to see if the needle is a prefix of the top level haystack, before calling into a tail recursive helper function that peels one character off of the string at a time, checking if the needle is a prefix at each step.
```idris
export
isSubstr : (needle, haystack : String) -> Bool
isSubstr needle haystack =
if needle `isPrefixOf` haystack
then True
else isSubstr' haystack
where
isSubstr' : String -> Bool
isSubstr' str with (asList str)
isSubstr' "" | [] = False
isSubstr' (strCons c str) | (c :: x) =
if needle `isPrefixOf` str
then True
else isSubstr' str | x
```