Add a special case to the translation of cryptol comprehensions

when we can easily tell that the length of the branches are the
same.  This avoids unneccessary coercions.

Fixes #1507

Author: robdockins

cryptol-saw-core/saw/Cryptol.sawcore

@@ -403,6 +403,16 @@ seqZip a b m n =
        n)
     m;
 
+zipSame : (a b : isort 0) -> (n : Nat) -> Vec n a -> Vec n b -> Vec n (a * b);
+zipSame a b n x y = gen n (a*b) (\ (i : Nat) -> (at n a x i, at n b y i));
+
+seqZipSame : (a b : isort 0) -> (n : Num) -> seq n a -> seq n b -> seq n (a * b);
+seqZipSame a b n =
+  Num#rec
+    (\ (n : Num) -> seq n a -> seq n b -> seq n (a * b))
+    (\ (n : Nat) -> zipSame a b n)
+    (streamMap2 a b (a*b) (\ (x:a) -> \ (y:b) -> (x,y)))
+    n;
 
 --------------------------------------------------------------------------------
 -- Ring and Logic functions

cryptol-saw-core/src/Verifier/SAW/Cryptol.hs

@@ -1483,10 +1483,14 @@ importComp sc env lenT elemT expr mss =
               m <- importType sc env len
               a <- importType sc env ty
               (ys, n, b, argss, len') <- zipAll branches
-              zs <- scGlobalApply sc "Cryptol.seqZip" [a, b, m, n, xs, ys]
-              mn <- scGlobalApply sc "Cryptol.tcMin" [m, n]
               ab <- scTupleType sc [a, b]
-              return (zs, mn, ab, args : argss, C.tMin len len')
+              if len == len' then
+                do zs <- scGlobalApply sc "Cryptol.seqZipSame" [a, b, m, xs, ys]
+                   return (zs, m, ab, args : argss, len)
+              else
+                do zs <- scGlobalApply sc "Cryptol.seqZip" [a, b, m, n, xs, ys]
+                   mn <- scGlobalApply sc "Cryptol.tcMin" [m, n]
+                   return (zs, mn, ab, args : argss, C.tMin len len')
      (xs, n, a, argss, lenT') <- zipAll mss
      f <- lambdaTuples sc env elemT expr argss
      b <- importType sc env elemT

saw-core-coq/coq/generated/CryptolToCoq/CryptolPrimitivesForSAWCore.v

@@ -182,6 +182,12 @@ Definition mlet : forall (a : Type), forall {Inh_a : SAWCoreScaffolding.Inhabite
 Definition seqZip : forall (a : Type), forall {Inh_a : SAWCoreScaffolding.Inhabited a}, forall (b : Type), forall {Inh_b : SAWCoreScaffolding.Inhabited b}, forall (m : Num), forall (n : Num), seq m a -> seq n b -> seq (tcMin m n) (prod a b) :=
   fun (a : Type) {Inh_a : SAWCoreScaffolding.Inhabited a} (b : Type) {Inh_b : SAWCoreScaffolding.Inhabited b} (m : Num) (n : Num) => CryptolPrimitivesForSAWCore.Num_rect (fun (m1 : Num) => seq m1 a -> seq n b -> seq (tcMin m1 n) (prod a b)) (fun (m1 : SAWCoreScaffolding.Nat) => CryptolPrimitivesForSAWCore.Num_rect (fun (n1 : Num) => SAWCoreVectorsAsCoqVectors.Vec m1 a -> seq n1 b -> seq (tcMin (TCNum m1) n1) (prod a b)) (fun (n1 : SAWCoreScaffolding.Nat) => SAWCorePrelude.zip a b m1 n1) (fun (xs : SAWCoreVectorsAsCoqVectors.Vec m1 a) (ys : SAWCorePrelude.Stream b) => SAWCoreVectorsAsCoqVectors.gen m1 (prod a b) (fun (i : SAWCoreScaffolding.Nat) => pair (SAWCorePrelude.sawAt m1 a xs i) (SAWCorePrelude.streamGet b ys i))) n) (CryptolPrimitivesForSAWCore.Num_rect (fun (n1 : Num) => SAWCorePrelude.Stream a -> seq n1 b -> seq (tcMin TCInf n1) (prod a b)) (fun (n1 : SAWCoreScaffolding.Nat) (xs : SAWCorePrelude.Stream a) (ys : SAWCoreVectorsAsCoqVectors.Vec n1 b) => SAWCoreVectorsAsCoqVectors.gen n1 (prod a b) (fun (i : SAWCoreScaffolding.Nat) => pair (SAWCorePrelude.streamGet a xs i) (SAWCorePrelude.sawAt n1 b ys i))) (SAWCorePrelude.streamMap2 a b (prod a b) (fun (x : a) (y : b) => pair x y)) n) m.
 
+Definition zipSame : forall (a : Type), forall {Inh_a : SAWCoreScaffolding.Inhabited a}, forall (b : Type), forall {Inh_b : SAWCoreScaffolding.Inhabited b}, forall (n : SAWCoreScaffolding.Nat), SAWCoreVectorsAsCoqVectors.Vec n a -> SAWCoreVectorsAsCoqVectors.Vec n b -> SAWCoreVectorsAsCoqVectors.Vec n (prod a b) :=
+  fun (a : Type) {Inh_a : SAWCoreScaffolding.Inhabited a} (b : Type) {Inh_b : SAWCoreScaffolding.Inhabited b} (n : SAWCoreScaffolding.Nat) (x : SAWCoreVectorsAsCoqVectors.Vec n a) (y : SAWCoreVectorsAsCoqVectors.Vec n b) => SAWCoreVectorsAsCoqVectors.gen n (prod a b) (fun (i : SAWCoreScaffolding.Nat) => pair (SAWCorePrelude.sawAt n a x i) (SAWCorePrelude.sawAt n b y i)).
+
+Definition seqZipSame : forall (a : Type), forall {Inh_a : SAWCoreScaffolding.Inhabited a}, forall (b : Type), forall {Inh_b : SAWCoreScaffolding.Inhabited b}, forall (n : Num), seq n a -> seq n b -> seq n (prod a b) :=
+  fun (a : Type) {Inh_a : SAWCoreScaffolding.Inhabited a} (b : Type) {Inh_b : SAWCoreScaffolding.Inhabited b} (n : Num) => CryptolPrimitivesForSAWCore.Num_rect (fun (n1 : Num) => seq n1 a -> seq n1 b -> seq n1 (prod a b)) (fun (n1 : SAWCoreScaffolding.Nat) => zipSame a b n1) (SAWCorePrelude.streamMap2 a b (prod a b) (fun (x : a) (y : b) => pair x y)) n.
+
 Definition seqBinary : forall (n : Num), forall (a : Type), forall {Inh_a : SAWCoreScaffolding.Inhabited a}, (a -> a -> a) -> seq n a -> seq n a -> seq n a :=
   fun (num : Num) (a : Type) {Inh_a : SAWCoreScaffolding.Inhabited a} (f : a -> a -> a) => CryptolPrimitivesForSAWCore.Num_rect (fun (n : Num) => seq n a -> seq n a -> seq n a) (fun (n : SAWCoreScaffolding.Nat) => SAWCorePrelude.zipWith a a a f n) (SAWCorePrelude.streamMap2 a a a f) num.