特定位宽的Haskell二进制数据类型

atmip9wb 于 2023-10-19 发布在其他

关注(0)|答案(2)|浏览(127)

我想创建一个数据类型表示一个特定位宽的二进制数。
所以类型bin3--> 0bXXX，bin7--> 0bXXXXXXX
有人知道怎么做吗？我试过安装像bv-sized这样的软件包，但是它们不能正确地构建。我不需要太多的功能，所以我想我可以实现我自己的。
我在尝试安装bv-sized时遇到的错误是

$ cabal install bv-sized
Resolving dependencies...
Configuring parameterized-utils-2.1.2.0...
Building parameterized-utils-2.1.2.0...
Failed to install parameterized-utils-2.1.2.0
Build log ( /home/.../.cabal/logs/ghc-8.2.2/parameterized-utils-2.1.2.0-4VdYssETRDcLceu2pgYcjQ.log ):
cabal: Entering directory '/tmp/cabal-tmp-99266/parameterized-utils-2.1.2.0'
Configuring parameterized-utils-2.1.2.0...
Preprocessing library for parameterized-utils-2.1.2.0..
Building library for parameterized-utils-2.1.2.0..
[ 1 of 32] Compiling Data.Parameterized.Compose ( src/Data/Parameterized/Compose.hs, dist/build/Data/Parameterized/Compose.o )

src/Data/Parameterized/Compose.hs:30:45: error:
    Type variable ‘k’ used in a kind.
    Did you mean to use TypeInType?
    the type signature for ‘testEqualityComposeBare’
   |
30 | testEqualityComposeBare :: forall k l (f :: k -> *) (g :: l -> k) x y.
   |                                             ^

src/Data/Parameterized/Compose.hs:30:59: error:
    Type variable ‘l’ used in a kind.
    Did you mean to use TypeInType?
    the type signature for ‘testEqualityComposeBare’
   |
30 | testEqualityComposeBare :: forall k l (f :: k -> *) (g :: l -> k) x y.
   |                                                           ^

src/Data/Parameterized/Compose.hs:30:64: error:
    Type variable ‘k’ used in a kind.
    Did you mean to use TypeInType?
    the type signature for ‘testEqualityComposeBare’
   |
30 | testEqualityComposeBare :: forall k l (f :: k -> *) (g :: l -> k) x y.
   |                                                                ^
cabal: Leaving directory '/tmp/cabal-tmp-99266/parameterized-utils-2.1.2.0'
cabal: Error: some packages failed to install:
bv-sized-1.0.3-Ip13iwUWQ7u421I8e2amlq depends on bv-sized-1.0.3 which failed
to install.
parameterized-utils-2.1.2.0-4VdYssETRDcLceu2pgYcjQ failed during the building
phase. The exception was:
ExitFailure 1

GHC 8.2.2

haskell

来源：https://stackoverflow.com/questions/77287141/haskell-binary-datatype-of-specific-bitwidth

2条答案

按热度按时间

koaltpgm1#

假设最多有64位，我们可以很容易地将其编码为64位字。这将意味着我们可以与：

{-# LANGUAGE DataKinds, KindSignatures #-}

import Data.Word(Word64)
import GHC.TypeNats (KnownNat, natVal)
import Numeric.Natural (Natural)
import Text.Printf (printf)

newtype Bin (n :: Natural) = Bin Word64 deriving (Eq, Ord, Read)

_sz :: KnownNat n => Bin n -> Int
_sz = fromIntegral . natVal

instance KnownNat n => Show (Bin n) where
  showsPrec d g@(Bin v) = showParen (d > 0) (("0b" ++ printf ("%0" ++ (show (_sz g)) ++ "b") v) ++)

因此，_sz与Bin n一起工作，并将n的值作为Int返回，无论Bin n对象是什么，这甚至可以是未定义的。因此，我们使用它来显示位数，例如：

ghci> Bin 3 :: Bin 3
0b011
ghci> Bin 3 :: Bin 5
0b00011

当然这只是一个最小的例子。例如，它没有智能构造函数。但是我们可以完成这一点，例如构造函数，以及Num，Bits等的额外示例。

赞(0）回复(0）举报 2023-10-19

jw5wzhpr2#

对于您的目的来说，这可能是一个过度的要求，但是SBV支持任意大小的位向量，包括有符号和无符号的：

Prelude Data.SBV> :set -XDataKinds
Prelude Data.SBV> (3 :: SWord 2) + 1
0 :: SWord 2
Prelude Data.SBV> (3 :: SInt 7) * 91
17 :: SInt 7

它们也具有象征性的特性：

Prelude Data.SBV> sat $ \(x :: SWord 4) y -> x + y .== 3
Satisfiable. Model:
  s0 = 14 :: WordN 4
  s1 =  5 :: WordN 4

只要你坚持使用常量值，所有的东西都应该是常量折叠的。

赞(0）回复(0）举报 2023-10-19

我来回答

特定位宽的Haskell二进制数据类型

2条答案

相关问题

热门标签

最新问答