go back to polimorphism in several util functions

LICENSE-APACHE

@@ -188,7 +188,7 @@ APPENDIX: How to apply the Apache License to your work.
    same "printed page" as the copyright notice for easier
    identification within third-party archives.
 
-Copyright [yyyy] [name of copyright owner]
+Copyright [2023] [Alfredo Garcia]
 
 Licensed under the Apache License, Version 2.0 (the "License");
 you may not use this file except in compliance with the License.

src/Columnround.hs

@@ -39,22 +39,22 @@ import Keelung hiding (input, eq)
 {-@ columnroundCompute :: { i:[Word32] | (len i) == 16 } -> { o:[Word32] | (len o) == 16 }  @-}
 columnroundCompute :: [Word32] -> [Word32]
 columnroundCompute input
-    | length input == 16 = transposev1 $ rowroundCompute $ transposev1 input
+    | length input == 16 = transpose $ rowroundCompute $ transpose input
     | otherwise = error "input to `columnroundCompute` must be a list of 16 `Word32` numbers"
 
 -- |The columnround expression as a string.
 {-@ columnroundDisplay :: { i:[String] | (len i) == 16 } -> { o:[String] | (len o) == 16 }  @-}
 columnroundDisplay :: [String] -> [String]
 columnroundDisplay input
-    | length input == 16 = transposev2 $ rowroundDisplay $ transposev2 input
+    | length input == 16 = transpose $ rowroundDisplay $ transpose input
     | otherwise = error "input to `columnroundDisplay` must be a list of 16 `String` strings"
 
 -- |The Keelung columnround expression.
 {-@ columnroundKeelung :: { i:[_] | (len i) == 16 } -> Comp { o:[_] | (len o) == 16 }  @-}
 columnroundKeelung :: [UInt 32] -> Comp [UInt 32]
 columnroundKeelung input
     | length input == 16 = do
-        let new_input = transposev3 input
+        let new_input = transpose input
         k <- rowroundKeelung new_input
-        return $ transposev3 k
+        return $ transpose k
     | otherwise = error "input to `columnroundKeelung` must be a list of 16 `UInt 32` numbers"

src/LittleEndian.hs

@@ -108,17 +108,17 @@ extractBytes4Keelung w = [ Keelung.shiftR w (8 * 0) Keelung..&. 0xff,
 -- | Reduce a matrix of 64 elements to a matrix of 16 elements by using `littleendian` encoding.
 {-@ reduce :: { i:[Word32] | (len i) == 64 } -> { o:[Word32] | (len o) == 16 } @-}
 reduce :: [Word32] -> [Word32]
-reduce input = Prelude.map littleendian (chunksof4v1 input)
+reduce input = Prelude.map littleendian (chunksof4 input)
 
 -- | Reduce a matrix of 64 elements to a matrix of 16 elements by using `littleendianDisplay` encoding.
 {-@ reduceDisplay :: { i:[String] | (len i) == 64 } -> { o:[String] | (len o) == 16 } @-}
 reduceDisplay :: [String] -> [String]
-reduceDisplay input = Prelude.map littleendianDisplay (chunksof4v2 input)
+reduceDisplay input = Prelude.map littleendianDisplay (chunksof4 input)
 
 -- |Reduce a matrix of 64 elements to a matrix of 16 elements by using `littleendianKeelung` encoding.
 {-@ reduceKeelung :: { i:[_] | (len i) == 64 } -> { o:[_] | (len o) == 16 } @-}
 reduceKeelung :: [UInt 32] -> [UInt 32]
-reduceKeelung input = Prelude.map littleendianKeelung (chunksof4v3 input)
+reduceKeelung input = Prelude.map littleendianKeelung (chunksof4 input)
 
 -- | Aument a matrix of 16 elements to one of 64 elements by using `extractBytes`.
 {-@ aument :: { i:[Word32] | (len i) == 16 } -> { o:[Word32] | (len o) == 64 } @-}

src/Utils.hs

@@ -14,10 +14,10 @@ This module provides general utility functions used in the creation of the Salsa
 
 module Utils
     (
-        modMatrix, numberListToStringList, transposev1, transposev2, transposev3, modMatrixDisplay, modMatrixKeelung,
+        modMatrix, numberListToStringList, transpose, modMatrixDisplay, modMatrixKeelung,
         eitherListToNumberList, eitherListToStringList,
         elts, concat64,
-        chunksof4v1, chunksof4v2, chunksof4v3,
+        chunksof4,
     )
 where
 
@@ -32,9 +32,9 @@ import Data.Set as Set
 import Operators()
 
 -- | Get chunks of 4 elements from a list of 64 elements.
-{-@ chunksof4v1 :: { i:[Word32] | (len i) == 64 } -> { o:[{ inner_o:[Word32] | (len inner_o) == 4}] | (len o) == 16 } @-}
-chunksof4v1 :: [Word32] -> [[Word32]]
-chunksof4v1 input
+{-@ chunksof4 :: { i:[a] | (len i) == 64 } -> { o:[{ inner_o:[a] | (len inner_o) == 4}] | (len o) == 16 } @-}
+chunksof4 :: [a] -> [[a]]
+chunksof4 input
     | length input == 64 = [
         Prelude.take 4 input,
         Prelude.take 4 (Prelude.drop 4 input),
@@ -54,105 +54,33 @@ chunksof4v1 input
         Prelude.take 4 (Prelude.drop 60 input)]
     | otherwise = error "input to `chunksof4` must be a list of 64 elements"
 
--- | Get chunks of 4 elements from a list of 64 elements.
-{-@ chunksof4v2 :: { i:[String] | (len i) == 64 } -> { o:[{ inner_o:[String] | (len inner_o) == 4}] | (len o) == 16 } @-}
-chunksof4v2 :: [String] -> [[String]]
-chunksof4v2 input
-    | length input == 64 = [
-        Prelude.take 4 input,
-        Prelude.take 4 (Prelude.drop 4 input),
-        Prelude.take 4 (Prelude.drop 8 input),
-        Prelude.take 4 (Prelude.drop 12 input),
-        Prelude.take 4 (Prelude.drop 16 input),
-        Prelude.take 4 (Prelude.drop 20 input),
-        Prelude.take 4 (Prelude.drop 24 input),
-        Prelude.take 4 (Prelude.drop 28 input),
-        Prelude.take 4 (Prelude.drop 32 input),
-        Prelude.take 4 (Prelude.drop 36 input),
-        Prelude.take 4 (Prelude.drop 40 input),
-        Prelude.take 4 (Prelude.drop 44 input),
-        Prelude.take 4 (Prelude.drop 48 input),
-        Prelude.take 4 (Prelude.drop 52 input),
-        Prelude.take 4 (Prelude.drop 56 input),
-        Prelude.take 4 (Prelude.drop 60 input)]
-    | otherwise = error "input to `chunksof4` must be a list of 64 elements"
-
--- | Get chunks of 4 elements from a list of 64 elements.
-{-@ chunksof4v3 :: { i:[_] | (len i) == 64 } -> { o:[{ inner_o:[_] | (len inner_o) == 4}] | (len o) == 16 } @-}
-chunksof4v3 :: [UInt 32] -> [[UInt 32]]
-chunksof4v3 input
-    | length input == 64 = [
-        Prelude.take 4 input,
-        Prelude.take 4 (Prelude.drop 4 input),
-        Prelude.take 4 (Prelude.drop 8 input),
-        Prelude.take 4 (Prelude.drop 12 input),
-        Prelude.take 4 (Prelude.drop 16 input),
-        Prelude.take 4 (Prelude.drop 20 input),
-        Prelude.take 4 (Prelude.drop 24 input),
-        Prelude.take 4 (Prelude.drop 28 input),
-        Prelude.take 4 (Prelude.drop 32 input),
-        Prelude.take 4 (Prelude.drop 36 input),
-        Prelude.take 4 (Prelude.drop 40 input),
-        Prelude.take 4 (Prelude.drop 44 input),
-        Prelude.take 4 (Prelude.drop 48 input),
-        Prelude.take 4 (Prelude.drop 52 input),
-        Prelude.take 4 (Prelude.drop 56 input),
-        Prelude.take 4 (Prelude.drop 60 input)]
-    | otherwise = error "input to `chunksof4` must be a list of 64 elements"
-
--- |Monomorphic `Word32` version of `zipWith` that works with refinements.
-zipWithv1 :: (Word32 -> Word32 -> Word32) -> [Word32] -> [Word32] -> [Word32]
-zipWithv1 _ [] _ = []
-zipWithv1 _ _ [] = []
-zipWithv1 f (x:xs) (y:ys) = f x y : zipWithv1 f xs ys
-
--- |Monomorphic `String` version of `zipWith` that works with refinements.
-zipWithv2 :: (String -> String -> String) -> [String] -> [String] -> [String]
-zipWithv2 _ [] _ = []
-zipWithv2 _ _ [] = []
-zipWithv2 f (x:xs) (y:ys) = f x y : zipWithv2 f xs ys
-
--- |Monomorphic `UInt 32` version of `zipWith` that works with refinements.
-zipWithv3 :: (UInt 32 -> UInt 32 -> UInt 32) -> [UInt 32] -> [UInt 32] -> [UInt 32]
-zipWithv3 _ [] _ = []
-zipWithv3 _ _ [] = []
-zipWithv3 f (x:xs) (y:ys) = f x y : zipWithv3 f xs ys
+-- |Polymorphic version of `zipWith` that works with refinements.
+zipWith :: (a -> a -> a) -> [a] -> [a] -> [a]
+zipWith _ [] _ = []
+zipWith _ _ [] = []
+zipWith f (x:xs) (y:ys) = f x y : Utils.zipWith f xs ys
 
 -- |Given two matrices, do modulo addition on each of the elements.
 {-@ modMatrix :: { i:[Word32] | (len i) == 16 } -> { i:[Word32] | (len i) == 16 } -> { o:[Word32] | (len o) == 16 } @-}
 modMatrix :: [Word32] -> [Word32] -> [Word32]
-modMatrix = zipWithv1 (+)
+modMatrix = Utils.zipWith (+)
 
 -- |Given two matrices, display the modulo addition on each of the elements.
 {-@ modMatrixDisplay :: { i:[String] | (len i) == 16 } -> { i:[String] | (len i) == 16 } -> { o:[String] | (len o) == 16 } @-}
 modMatrixDisplay :: [String] -> [String] -> [String]
-modMatrixDisplay = zipWithv2 (printf "%s + %s")
+modMatrixDisplay = Utils.zipWith (printf "%s + %s")
 
 -- |Given two matrices, do modulo addition on each of the elements using Keelung types.
 {-@ modMatrixKeelung :: { a:[_] | (len a) == 16 } -> { b:[_] | (len b) == 16 } -> { o:[_] | (len o) == 16 } @-}
 modMatrixKeelung :: [UInt 32] -> [UInt 32] -> [UInt 32]
-modMatrixKeelung = zipWithv3 Keelung.AddU
-
--- |Transpose a 4x4 matrix type.
-{-@ transposev1 :: {i:[Word32] | len i == 16} -> {o:[Word32] | len o == 16 && (elts i == elts o) } @-}
-transposev1 :: [Word32] -> [Word32]
-transposev1 [y0, y1, y2, y3, y4, y5, y6, y7, y8, y9, y10, y11, y12, y13, y14, y15] =
-    [y0, y4, y8, y12, y1, y5, y9, y13, y2, y6, y10, y14, y3, y7, y11, y15]
-transposev1 _ = error "input to `transpose` must be a list of 16 objects"
-
--- |Transpose a 4x4 matrix type.
-{-@ transposev2 :: {i:[String] | len i == 16} -> {o:[String] | len o == 16 && (elts i == elts o) } @-}
-transposev2 :: [String] -> [String]
-transposev2 [y0, y1, y2, y3, y4, y5, y6, y7, y8, y9, y10, y11, y12, y13, y14, y15] =
-    [y0, y4, y8, y12, y1, y5, y9, y13, y2, y6, y10, y14, y3, y7, y11, y15]
-transposev2 _ = error "input to `transpose` must be a list of 16 objects"
+modMatrixKeelung = Utils.zipWith Keelung.AddU
 
 -- |Transpose a 4x4 matrix type.
-{-@ transposev3 :: {i:[_] | len i == 16} -> {o:[_] | len o == 16 && (elts i == elts o) } @-}
-transposev3 :: [UInt 32] -> [UInt 32]
-transposev3 [y0, y1, y2, y3, y4, y5, y6, y7, y8, y9, y10, y11, y12, y13, y14, y15] =
+{-@ transpose :: {i:[a] | len i == 16} -> {o:[a] | len o == 16 && (elts i == elts o) } @-}
+transpose :: [a] -> [a]
+transpose [y0, y1, y2, y3, y4, y5, y6, y7, y8, y9, y10, y11, y12, y13, y14, y15] =
     [y0, y4, y8, y12, y1, y5, y9, y13, y2, y6, y10, y14, y3, y7, y11, y15]
-transposev3 _ = error "input to `transpose` must be a list of 16 objects"
+transpose _ = error "input to `transpose` must be a list of 16 objects"
 
 -- |Convert a list of numbers to a list of strings. This is always possible. 
 {-@ numberListToStringList :: { i:[Word32] | (len i) == 4 } -> { o:[String] | (len o) == 4 }  @-}