From 850eb003e7fe6c242e29b1c25e208b2124574dca Mon Sep 17 00:00:00 2001
From: Ryan Scott <rscott@galois.com>
Date: Mon, 9 Oct 2023 08:28:18 -0400
Subject: [PATCH] Respect VWord/VSeq invariants in parmap implementation

Previously, `parmap` could incorrectly return a `VWord` when the element type
was not `Bit`, and it could also return a `VSeq` when the element type was
`Bit`. This changes the implementation of `parmap` to use the `mkSeq` smart
constructor, which properly chooses what sort of `GenValue` to return depending
on the element type.

Fixes #1578.
---
 CHANGES.md                     |  2 ++
 src/Cryptol/Eval/Generic.hs    | 23 ++++++++++++-----------
 tests/issues/T1578.icry        |  2 ++
 tests/issues/T1578.icry.stdout |  3 +++
 4 files changed, 19 insertions(+), 11 deletions(-)
 create mode 100644 tests/issues/T1578.icry
 create mode 100644 tests/issues/T1578.icry.stdout

diff --git a/CHANGES.md b/CHANGES.md
index 88057caca..96de3227b 100644
--- a/CHANGES.md
+++ b/CHANGES.md
@@ -12,6 +12,8 @@
 * Fixed #1455, making anything in scope of the functor in scope at the REPL as
   well when an instantiation of the functor is loaded and focused,
   design choice (3) on the ticket.  In particular, the prelude will be in scope.
+* Fix #1578, which caused `parmap` to crash when evaluated on certain types of
+  sequences.
 
 
 # 3.0.0 -- 2023-06-26
diff --git a/src/Cryptol/Eval/Generic.hs b/src/Cryptol/Eval/Generic.hs
index 461c4bc22..7a01e76c3 100644
--- a/src/Cryptol/Eval/Generic.hs
+++ b/src/Cryptol/Eval/Generic.hs
@@ -1877,22 +1877,23 @@ randomV sym ty seed =
 parmapV :: Backend sym => sym -> Prim sym
 parmapV sym =
   PTyPoly \_a ->
-  PTyPoly \_b ->
-  PFinPoly \_n ->
+  PTyPoly \b ->
+  PFinPoly \n ->
   PFun \f ->
   PFun \xs ->
   PPrim
     do f' <- fromVFun sym <$> f
        xs' <- xs
-       case xs' of
-          VWord n w ->
-            do let m = asBitsMap sym w
-               m' <- sparkParMap sym (\x -> f' (VBit <$> x)) n m
-               VWord n <$> (bitmapWordVal sym n (fromVBit <$> m'))
-          VSeq n m ->
-            VSeq n <$> sparkParMap sym f' n m
-
-          _ -> panic "parmapV" ["expected sequence!"]
+       m <-
+         case xs' of
+           VWord _n w ->
+             let m = asBitsMap sym w in
+             sparkParMap sym (\x -> f' (VBit <$> x)) n m
+           VSeq _n m ->
+             sparkParMap sym f' n m
+
+           _ -> panic "parmapV" ["expected finite sequence!"]
+       mkSeq sym (Nat n) b m
 
 
 sparkParMap ::
diff --git a/tests/issues/T1578.icry b/tests/issues/T1578.icry
new file mode 100644
index 000000000..038e23742
--- /dev/null
+++ b/tests/issues/T1578.icry
@@ -0,0 +1,2 @@
+parmap (\_ -> True) [0, 1] > 0b00
+parmap (\_ -> ()) 0b00 == [(), ()]
diff --git a/tests/issues/T1578.icry.stdout b/tests/issues/T1578.icry.stdout
new file mode 100644
index 000000000..c80ef5e56
--- /dev/null
+++ b/tests/issues/T1578.icry.stdout
@@ -0,0 +1,3 @@
+Loading module Cryptol
+True
+True