idris-lang/Idris2
1
1
Fork 0
mirror of https://github.com/idris-lang/Idris2.git synced 2024-09-21 10:18:23 +03:00
Code Issues Projects Releases Wiki Activity

Make Prelude.unpack tail-recursive

Browse Source
This commit is contained in:
Johann Rudloff 2020-06-12 15:46:26 +02:00
parent 176f2516da
commit 7128f127e8
1 changed files with 6 additions and 6 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

12
libs/prelude/Prelude.idr
View File

@ -1139,13 +1139,13 @@ fastPack xs
||| ```
public export
unpack : String -> List Char
unpack str = unpack' 0 (prim__cast_IntegerInt (natToInteger (length str))) str
unpack str = unpack' (prim__cast_IntegerInt (natToInteger (length str)) - 1) str []
where
unpack' : Int -> Int -> String -> List Char
unpack' pos len str
= if pos >= len
then []
else assert_total (prim__strIndex str pos) :: assert_total (unpack' (pos + 1) len str)
unpack' : Int -> String -> List Char -> List Char
unpack' pos str acc
= if pos < 0
then acc
else assert_total $ unpack' (pos - 1) str (assert_total (prim__strIndex str pos)::acc)
public export
Semigroup String where