Skip to content

Commit

Permalink
Respect VWord/VSeq invariants in parmap implementation
Browse files Browse the repository at this point in the history
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.
  • Loading branch information
RyanGlScott committed Oct 9, 2023
1 parent 8bc638e commit 850eb00
Show file tree
Hide file tree
Showing 4 changed files with 19 additions and 11 deletions.
2 changes: 2 additions & 0 deletions CHANGES.md
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down
23 changes: 12 additions & 11 deletions src/Cryptol/Eval/Generic.hs
Original file line number Diff line number Diff line change
Expand Up @@ -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 ::
Expand Down
2 changes: 2 additions & 0 deletions tests/issues/T1578.icry
Original file line number Diff line number Diff line change
@@ -0,0 +1,2 @@
parmap (\_ -> True) [0, 1] > 0b00
parmap (\_ -> ()) 0b00 == [(), ()]
3 changes: 3 additions & 0 deletions tests/issues/T1578.icry.stdout
Original file line number Diff line number Diff line change
@@ -0,0 +1,3 @@
Loading module Cryptol
True
True

0 comments on commit 850eb00

Please sign in to comment.