[ performance ] a faster implementation of unpack (#3281)

* [ performance ] a much faster implementation of unpack

* [ fix ] partiality error in Hangman test

* [ test ] add some documentation to the unpack test case

* [ test ] fix expected output of unpack test

libs/prelude/Prelude/Types.idr

@@ -867,13 +867,13 @@ fastPack : List Char -> String
 ||| ```
 public export
 unpack : String -> List Char
-unpack str = unpack' (prim__cast_IntegerInt (natToInteger (length str)) - 1) str []
+unpack str = go [] (length str)
   where
-    unpack' : Int -> String -> List Char -> List Char
-    unpack' pos str acc
-        = if pos < 0
-             then acc
-             else unpack' (assert_smaller pos (pos - 1)) str $ (assert_total $ prim__strIndex str pos) :: acc
+    go : List Char -> Nat -> List Char
+    go cs 0     = cs
+    go cs (S k) =
+      let ix := prim__cast_IntegerInt $ natToInteger k
+       in go (assert_total (prim__strIndex str ix) :: cs) k
 
 -- This function runs fast when compiled but won't compute at compile time.
 -- If you need to unpack strings at compile time, use Prelude.unpack.

tests/prelude/unpack/expected

@@ -0,0 +1,15 @@
+1/1: Building unpack (unpack.idr)
+Error: While processing right hand side of message. When unifying:
+    String -> InterpFormat (format [assert_total (prim__strIndex (fromString "My name is %s and I am %d years old") (prim__cast_IntegerInt (natToInteger (assert_total (integerToNat 13))))), assert_total (prim__strIndex (fromString "My name is %s and I am %d years old") (prim__cast_IntegerInt (natToInteger (assert_total (integerToNat 14))))), assert_total (prim__strIndex (fromString "My name is %s and I am %d years old") (prim__cast_IntegerInt (natToInteger (assert_total (integerToNat 15))))), assert_total (prim__strIndex (fromString "My name is %s and I am %d years old") (prim__cast_IntegerInt (natToInteger (assert_total (integerToNat 16))))), assert_total (prim__strIndex (fromString "My name is %s and I am %d years old") (prim__cast_IntegerInt (natToInteger (assert_total (integerToNat 17))))), assert_total (prim__strIndex (fromString "My name is %s and I am %d years old") (prim__cast_IntegerInt (natToInteger (assert_total (integerToNat 18))))), assert_total (prim__strIndex (fromString "My name is %s and I am %d years old") (prim__cast_IntegerInt (natToInteger (assert_total (integerToNat 19))))), assert_total (prim__strIndex (fromString "My name is %s and I am %d years old") (prim__cast_IntegerInt (natToInteger (assert_total (integerToNat 20))))), assert_total (prim__strIndex (fromString "My name is %s and I am %d years old") (prim__cast_IntegerInt (natToInteger (assert_total (integerToNat 21))))), assert_total (prim__strIndex (fromString "My name is %s and I am %d years old") (prim__cast_IntegerInt (natToInteger (assert_total (integerToNat 22))))), assert_total (prim__strIndex (fromString "My name is %s and I am %d years old") (prim__cast_IntegerInt (natToInteger (assert_total (integerToNat 23))))), assert_total (prim__strIndex (fromString "My name is %s and I am %d years old") (prim__cast_IntegerInt (natToInteger (assert_total (integerToNat 24))))), assert_total (prim__strIndex (fromString "My name is %s and I am %d years old") (prim__cast_IntegerInt (natToInteger (assert_total (integerToNat 25))))), assert_total (prim__strIndex (fromString "My name is %s and I am %d years old") (prim__cast_IntegerInt (natToInteger (assert_total (integerToNat 26))))), assert_total (prim__strIndex (fromString "My name is %s and I am %d years old") (prim__cast_IntegerInt (natToInteger (assert_total (integerToNat 27))))), assert_total (prim__strIndex (fromString "My name is %s and I am %d years old") (prim__cast_IntegerInt (natToInteger (assert_total (integerToNat 28))))), assert_total (prim__strIndex (fromString "My name is %s and I am %d years old") (prim__cast_IntegerInt (natToInteger (assert_total (integerToNat 29))))), assert_total (prim__strIndex (fromString "My name is %s and I am %d years old") (prim__cast_IntegerInt (natToInteger (assert_total (integerToNat 30))))), assert_total (prim__strIndex (fromString "My name is %s and I am %d years old") (prim__cast_IntegerInt (natToInteger (assert_total (integerToNat 31))))), assert_total (prim__strIndex (fromString "My name is %s and I am %d years old") (prim__cast_IntegerInt (natToInteger (assert_total (integerToNat 32))))), assert_total (prim__strIndex (fromString "My name is %s and I am %d years old") (prim__cast_IntegerInt (natToInteger (assert_total (integerToNat 33))))), assert_total (prim__strIndex (fromString "My name is %s and I am %d years old") (prim__cast_IntegerInt (natToInteger (assert_total (integerToNat 34)))))])
+and:
+    String
+Mismatch between: String -> InterpFormat (format [assert_total (prim__strIndex (fromString "My name is %s and I am %d years old") (prim__cast_IntegerInt (natToInteger (assert_total (integerToNat 13))))), assert_total (prim__strIndex (fromString "My name is %s and I am %d years old") (prim__cast_IntegerInt (natToInteger (assert_total (integerToNat 14))))), assert_total (prim__strIndex (fromString "My name is %s and I am %d years old") (prim__cast_IntegerInt (natToInteger (assert_total (integerToNat 15))))), assert_total (prim__strIndex (fromString "My name is %s and I am %d years old") (prim__cast_IntegerInt (natToInteger (assert_total (integerToNat 16))))), assert_total (prim__strIndex (fromString "My name is %s and I am %d years old") (prim__cast_IntegerInt (natToInteger (assert_total (integerToNat 17))))), assert_total (prim__strIndex (fromString "My name is %s and I am %d years old") (prim__cast_IntegerInt (natToInteger (assert_total (integerToNat 18))))), assert_total (prim__strIndex (fromString "My name is %s and I am %d years old") (prim__cast_IntegerInt (natToInteger (assert_total (integerToNat 19))))), assert_total (prim__strIndex (fromString "My name is %s and I am %d years old") (prim__cast_IntegerInt (natToInteger (assert_total (integerToNat 20))))), assert_total (prim__strIndex (fromString "My name is %s and I am %d years old") (prim__cast_IntegerInt (natToInteger (assert_total (integerToNat 21))))), assert_total (prim__strIndex (fromString "My name is %s and I am %d years old") (prim__cast_IntegerInt (natToInteger (assert_total (integerToNat 22))))), assert_total (prim__strIndex (fromString "My name is %s and I am %d years old") (prim__cast_IntegerInt (natToInteger (assert_total (integerToNat 23))))), assert_total (prim__strIndex (fromString "My name is %s and I am %d years old") (prim__cast_IntegerInt (natToInteger (assert_total (integerToNat 24))))), assert_total (prim__strIndex (fromString "My name is %s and I am %d years old") (prim__cast_IntegerInt (natToInteger (assert_total (integerToNat 25))))), assert_total (prim__strIndex (fromString "My name is %s and I am %d years old") (prim__cast_IntegerInt (natToInteger (assert_total (integerToNat 26))))), assert_total (prim__strIndex (fromString "My name is %s and I am %d years old") (prim__cast_IntegerInt (natToInteger (assert_total (integerToNat 27))))), assert_total (prim__strIndex (fromString "My name is %s and I am %d years old") (prim__cast_IntegerInt (natToInteger (assert_total (integerToNat 28))))), assert_total (prim__strIndex (fromString "My name is %s and I am %d years old") (prim__cast_IntegerInt (natToInteger (assert_total (integerToNat 29))))), assert_total (prim__strIndex (fromString "My name is %s and I am %d years old") (prim__cast_IntegerInt (natToInteger (assert_total (integerToNat 30))))), assert_total (prim__strIndex (fromString "My name is %s and I am %d years old") (prim__cast_IntegerInt (natToInteger (assert_total (integerToNat 31))))), assert_total (prim__strIndex (fromString "My name is %s and I am %d years old") (prim__cast_IntegerInt (natToInteger (assert_total (integerToNat 32))))), assert_total (prim__strIndex (fromString "My name is %s and I am %d years old") (prim__cast_IntegerInt (natToInteger (assert_total (integerToNat 33))))), assert_total (prim__strIndex (fromString "My name is %s and I am %d years old") (prim__cast_IntegerInt (natToInteger (assert_total (integerToNat 34)))))]) and String.
+
+unpack:39:11--39:55
+ 35 | printf : (s : String) -> InterpFormat (formatString s)
+ 36 | printf s = toFunction (formatString s) ""
+ 37 | 
+ 38 | message : String
+ 39 | message = printf "My name is %s and I am %d years old"
+                ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
+

tests/prelude/unpack/run

@@ -0,0 +1,3 @@
+. ../../testutils.sh
+
+check unpack.idr

tests/prelude/unpack/unpack.idr

@@ -0,0 +1,39 @@
+||| This tests that issue #3280 has been fixed. With the former
+||| implementation of `unpack`, the compiler would not produce
+||| an error in a reasonable amount of time.
+import Data.String
+
+%default total
+
+data Format = FInt Format        -- %d
+            | FString Format     -- %s
+            | FOther Char Format
+            | FEnd
+
+format : List Char -> Format
+format Nil = FEnd
+format ('%' :: 'd' :: xs) = FInt (format xs)
+format ('%' :: 's' :: xs) = FString (format xs)
+format (x :: xs) = FOther x (format xs)
+
+
+0 InterpFormat : Format -> Type
+InterpFormat (FInt f)     = Int    -> InterpFormat f
+InterpFormat (FString f)  = String -> InterpFormat f
+InterpFormat (FOther _ f) = InterpFormat f
+InterpFormat FEnd         = String
+
+formatString : String -> Format
+formatString s = format (unpack s)
+
+toFunction : (fmt : Format) -> String -> InterpFormat fmt
+toFunction (FInt x) str     = \y => toFunction x (str ++ show y)
+toFunction (FString x) str  = \y => toFunction x (str ++ y)
+toFunction (FOther c x) str = toFunction x (str ++ singleton c)
+toFunction FEnd str         = str
+
+printf : (s : String) -> InterpFormat (formatString s)
+printf s = toFunction (formatString s) ""
+
+message : String
+message = printf "My name is %s and I am %d years old"