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