Skip to content

Commit

Permalink
Refactor code in splitV for improved readability
Browse files Browse the repository at this point in the history
I found the code in `splitV` hard to read, so this commit performs some mild
refactoring to improve things somewhat:

1. There are multiple cases where `parts` can be either `Nat` or `Inf`, but the
   two `Nat` cases were far away from each other visually (and similarly for the
   two `Inf` cases).
2. The code was pattern-matching on `each` for no good reason, as every case
   treated `each` as a bare variable. I've removed this match.

There is no change in behavior, just refactoring.
  • Loading branch information
RyanGlScott committed Sep 18, 2024
1 parent 1b94a6f commit 49428ec
Showing 1 changed file with 25 additions and 22 deletions.
47 changes: 25 additions & 22 deletions src/Cryptol/Eval/Generic.hs
Original file line number Diff line number Diff line change
Expand Up @@ -1065,31 +1065,34 @@ splitV :: Backend sym =>
SEval sym (GenValue sym) ->
SEval sym (GenValue sym)
splitV sym parts each a val =
case (parts, each) of
(Nat p, e) | isTBit a -> do
val' <- sDelay sym (fromWordVal "splitV" <$> val)
case parts of
Nat p
| isTBit a ->
do val' <- sDelay sym (fromWordVal "splitV" <$> val)
return $ VSeq p $ indexSeqMap $ \i ->
VWord <$> (extractWordVal sym e ((p-i-1)*e) =<< val')
(Inf, e) | isTBit a -> do
val' <- sDelay sym (fromSeq "splitV" =<< val)
return $ VStream $ indexSeqMap $ \i ->
VWord <$> bitmapWordVal sym e (indexSeqMap $ \j ->
let idx = i*e + toInteger j
in idx `seq` do
xs <- val'
fromVBit <$> lookupSeqMap xs idx)
(Nat p, e) -> do
val' <- sDelay sym (fromSeq "splitV" =<< val)
VWord <$> (extractWordVal sym each ((p-i-1)*each) =<< val')
| otherwise ->
do val' <- sDelay sym (fromSeq "splitV" =<< val)
return $ VSeq p $ indexSeqMap $ \i ->
return $ VSeq e $ indexSeqMap $ \j -> do
return $ VSeq each $ indexSeqMap $ \j -> do
xs <- val'
lookupSeqMap xs (e * i + j)
(Inf , e) -> do
val' <- sDelay sym (fromSeq "splitV" =<< val)
return $ VStream $ indexSeqMap $ \i ->
return $ VSeq e $ indexSeqMap $ \j -> do
xs <- val'
lookupSeqMap xs (e * i + j)
lookupSeqMap xs (each * i + j)

Inf
| isTBit a ->
do val' <- sDelay sym (fromSeq "splitV" =<< val)
return $ VStream $ indexSeqMap $ \i ->
VWord <$> bitmapWordVal sym each (indexSeqMap $ \j ->
let idx = i*each + toInteger j
in idx `seq` do
xs <- val'
fromVBit <$> lookupSeqMap xs idx)
| otherwise ->
do val' <- sDelay sym (fromSeq "splitV" =<< val)
return $ VStream $ indexSeqMap $ \i ->
return $ VSeq each $ indexSeqMap $ \j -> do
xs <- val'
lookupSeqMap xs (each * i + j)


{-# INLINE reverseV #-}
Expand Down

0 comments on commit 49428ec

Please sign in to comment.