ekmett / ersatz

A monad for interfacing with external SAT solvers
Other
62 stars 15 forks source link

add Num instances for Bit{3..} #49

Open jwaldmann opened 3 years ago

jwaldmann commented 3 years ago

I was surprised that Bit3 (and later) has no Num instance.

Easiest way is to go via Bits, as in

instance Num Bit3 where
  fromInteger = fromBits . fromInteger
  x + y = fromBits $ bits x + bits y
  negate (Bit3 x2 x1 x0) = Bit3 (not x2) (not x1) (not x0) + 1
  x * y = fromBits $ bits x * bits y

Implementation: this just throws away higher-order bits (that is, half of the work in multiplication), I hope that's still fine by lazy evaluation.

Semantics: this is inconsistent with type Decoded Bits3 = Word8 (the decoded type is mod 2^8 while the encoded type is mod 2^3) but this already happens for Bit1, Bit2.