haskell: move countTrailingZeros to Data.Word_Lib

Signed-off-by: Gerwin Klein <gerwin.klein@proofcraft.systems>

spec/haskell/src/Data/WordLib.lhs

@@ -1,4 +1,5 @@
 %
+% Copyright 2023, Proofcraft Pty Ltd
 % Copyright 2020, Data61, CSIRO (ABN 41 687 119 230)
 %
 % SPDX-License-Identifier: GPL-2.0-only
@@ -17,6 +18,7 @@
 > -- * Bytes required to store a word
 > -- * Selecting one of two alternatives depending on the size of the machine word
 > --      (32 or 64 bits)
+> -- * Counting the number of trailing zeros in a word
 >
 > wordBits :: Int
 > wordBits = finiteBitSize (undefined::Word)
@@ -32,4 +34,7 @@
 >
 > wordRadix :: Int
 > wordRadix = wordSizeCase 5 6
-
+>
+> countTrailingZeros :: (Bits b, FiniteBits b) => b -> Int
+> countTrailingZeros w =
+>    length . takeWhile not . map (testBit w) $ [0 .. finiteBitSize w - 1]

spec/haskell/src/SEL4/Object/VCPU/AARCH64.hs

@@ -39,6 +39,7 @@ import {-# SOURCE #-} SEL4.Object.Interrupt
 
 import Data.Bits hiding (countTrailingZeros)
 import Data.Word(Word8, Word16, Word32, Word64)
+import Data.WordLib(countTrailingZeros)
 import Data.Array
 import Data.Maybe
 
@@ -493,11 +494,6 @@ vcpuSwitch (Just new) = do
 
 {- VGICMaintenance -}
 
--- FIXME AARCH64: try move this to a more generic location
-countTrailingZeros :: (Bits b, FiniteBits b) => b -> Int
-countTrailingZeros w =
-    length . takeWhile not . map (testBit w) $ [0 .. finiteBitSize w - 1]
-
 vgicMaintenance :: Kernel ()
 vgicMaintenance = do
     hsCurVCPU <- gets (armHSCurVCPU . ksArchState)

spec/haskell/src/SEL4/Object/VCPU/ARM.lhs

@@ -43,6 +43,7 @@ hypervisor extensions on ARM.
 
 > import Data.Bits hiding (countTrailingZeros)
 > import Data.Word(Word8, Word16, Word32, Word64)
+> import Data.WordLib(countTrailingZeros)
 > import Data.Array
 > import Data.Maybe
 
@@ -491,10 +492,6 @@ For initialisation, see makeVCPUObject.
 
 \subsection{VGICMaintenance}
 
-> countTrailingZeros :: (Bits b, FiniteBits b) => b -> Int
-> countTrailingZeros w =
->     length . takeWhile not . map (testBit w) $ [0 .. finiteBitSize w - 1]
-
 > vgicMaintenance :: Kernel ()
 > vgicMaintenance = do
 >     hsCurVCPU <- gets (armHSCurVCPU . ksArchState)