From 757cb26264af0876ffa29ee3b292072c9e5c9c4b Mon Sep 17 00:00:00 2001
From: Brian Huffman <huffman@galois.com>
Date: Tue, 13 Aug 2019 11:56:31 -0700
Subject: [PATCH] Implement ecTranspose for infinite sizes.

This is a fix for GaloisInc/saw-script#534.
---
 saw/Cryptol.sawcore | 32 ++++++++++++++++++++++++++------
 1 file changed, 26 insertions(+), 6 deletions(-)

diff --git a/saw/Cryptol.sawcore b/saw/Cryptol.sawcore
index caf5147..c6af113 100644
--- a/saw/Cryptol.sawcore
+++ b/saw/Cryptol.sawcore
@@ -1065,12 +1065,32 @@ ecReverse =
 
 ecTranspose : (m n : Num) -> (a : sort 0) -> seq m (seq n a) ->
                seq n (seq m a);
-ecTranspose =
-  finNumRec2
-    (\ (m:Num) -> \ (n:Num) -> (a:sort 0) -> seq m (seq n a) ->
-       seq n (seq m a))
-    transpose;
-
+ecTranspose m n a =
+  Num#rec
+    (\ (m : Num) -> seq m (seq n a) -> seq n (seq m a))
+    (\ (m : Nat) ->
+      Num#rec
+        (\ (n : Num) -> Vec m (seq n a) -> seq n (Vec m a))
+        (\ (n : Nat) -> transpose m n a)
+        (\ (xss : Vec m (Stream a)) ->
+          MkStream (Vec m a) (\ (i : Nat) ->
+            gen m a (\ (j : Nat) ->
+              streamGet a (at m (Stream a) xss j) i)))
+        n
+    )
+    ( Num#rec
+        (\ (n : Num) -> Stream (seq n a) -> seq n (Stream a))
+        (\ (n : Nat) -> \ (xss : Stream (Vec n a)) ->
+          gen n (Stream a) (\ (i : Nat) ->
+            MkStream a (\ (j : Nat) ->
+              at n a (streamGet (Vec n a) xss j) i)))
+        (\ (xss : Stream (Stream a)) ->
+          MkStream (Stream a) (\ (i : Nat) ->
+            MkStream a (\ (j : Nat) ->
+              streamGet a (streamGet (Stream a) xss j) i)))
+        n
+    )
+    m;
 
 ecAt : (n : Num) -> (a : sort 0) -> (i : Num) -> seq n a -> seq i Bool -> a;
 ecAt n a i =