Bitwise Operations in Dhall

Bitwise.dhall

let P =
      { List =
          https://raw.githubusercontent.com/dhall-lang/dhall-lang/v23.0.0/Prelude/List/package.dhall
      , Natural =
          https://raw.githubusercontent.com/dhall-lang/dhall-lang/v23.0.0/Prelude/Natural/package.dhall
      }

let modulo
    : Natural → Natural → Natural
    = λ(divisor : Natural) →
      λ(n : Natural) →
        P.Natural.fold
          n
          Natural
          ( λ(x : Natural) →
              if    P.Natural.greaterThanEqual x divisor
              then  P.Natural.subtract divisor x
              else  x
          )
          n

let moduleExamples =
      { _2_1 = assert : modulo 2 1 ≡ 1
      , _2_2 = assert : modulo 2 2 ≡ 0
      , _2_3 = assert : modulo 2 3 ≡ 1
      }

let pow
    : Natural → Natural → Natural
    = λ(exponent : Natural) →
      λ(n : Natural) →
        if    P.Natural.equal exponent 0
        then  1
        else  P.Natural.fold
                (P.Natural.subtract 1 exponent)
                Natural
                (λ(x : Natural) → n * x)
                n

let powExamples =
      { _2_0 = assert : pow 2 0 ≡ 0
      , _0_2 = assert : pow 0 2 ≡ 1
      , _1_2 = assert : pow 1 2 ≡ 2
      , _2_2 = assert : pow 2 2 ≡ 4
      , _3_3 = assert : pow 3 3 ≡ 27
      }

let toBits
    : Natural → Natural → List Bool
    = λ(size : Natural) →
      λ(n : Natural) →
        let State
            : Type
            = { bits : List Bool, remaining : Natural }

        let initial
            : State
            = { bits = [] : List Bool, remaining = modulo (pow size 2) n }

        let compute
            : State → State
            = λ(state : State) →
                let bit
                    : Natural
                    = P.Natural.subtract (1 + List/length Bool state.bits) size

                let bitValue
                    : Natural
                    = pow bit 2

                in  if    P.Natural.greaterThanEqual state.remaining bitValue
                    then  { bits = state.bits # [ True ]
                          , remaining =
                              P.Natural.subtract bitValue state.remaining
                          }
                    else  { bits = state.bits # [ False ]
                          , remaining = state.remaining
                          }

        let result
            : State
            = P.Natural.fold size State compute initial

        in  result.bits

let toBitsExamples =
      { _1_0 = assert : toBits 1 0 ≡ [ False ]
      , _1_1 = assert : toBits 1 1 ≡ [ True ]
      , _2_2 = assert : toBits 2 2 ≡ [ True, False ]
      , _2_3 = assert : toBits 2 3 ≡ [ True, True ]
      , _8_0 =
            assert
          :   toBits 8 0
            ≡ [ False, False, False, False, False, False, False, False ]
      , _8_1 =
            assert
          :   toBits 8 1
            ≡ [ False, False, False, False, False, False, False, True ]
      , _8_2 =
            assert
          :   toBits 8 2
            ≡ [ False, False, False, False, False, False, True, False ]
      , _8_3 =
            assert
          :   toBits 8 3
            ≡ [ False, False, False, False, False, False, True, True ]
      , _3_4 = assert : toBits 3 4 ≡ [ True, False, False ]
      , _3_6 = assert : toBits 3 6 ≡ [ True, True, False ]
      , _overflow = assert : toBits 3 8 ≡ toBits 3 0
      }

let fromBits
    : List Bool → Natural
    = λ(bits : List Bool) →
        let State
            : Type
            = { n : Natural, remaining : List Bool }

        let Indexed
            : Type
            = { index : Natural, value : Bool }

        let fold
            : Indexed → Natural → Natural
            = λ(bit : Indexed) →
              λ(value : Natural) →
                value + (if bit.value then pow bit.index 2 else 0)

        let result
            : Natural
            = List/fold
                Indexed
                (List/indexed Bool (List/reverse Bool bits))
                Natural
                fold
                0

        in  result

let fromBitsExamples =
      { _1_0 = assert : 0 ≡ fromBits [ False ]
      , _1_1 = assert : 1 ≡ fromBits [ True ]
      , _2_2 = assert : 2 ≡ fromBits [ True, False ]
      , _2_3 = assert : 3 ≡ fromBits [ True, True ]
      , _8_0 =
            assert
          :   0
            ≡ fromBits
                [ False, False, False, False, False, False, False, False ]
      , _8_1 =
            assert
          :   1
            ≡ fromBits [ False, False, False, False, False, False, False, True ]
      , _8_2 =
            assert
          :   2
            ≡ fromBits [ False, False, False, False, False, False, True, False ]
      , _8_3 =
            assert
          :   3
            ≡ fromBits [ False, False, False, False, False, False, True, True ]
      }

let bitwiseCompare
    : Natural → (Bool → Bool → Bool) → Natural → Natural → Natural
    = λ(size : Natural) →
      λ(compare : Bool → Bool → Bool) →
      λ(a : Natural) →
      λ(b : Natural) →
        let zipped = P.List.zip Bool (toBits size a) Bool (toBits size b)

        let compared =
              P.List.map
                { _1 : Bool, _2 : Bool }
                Bool
                ( λ(tuple : { _1 : Bool, _2 : Bool }) →
                    compare tuple._1 tuple._2
                )
                zipped

        in  fromBits compared

let or
    : Natural → Natural → Natural → Natural
    = λ(size : Natural) →
        bitwiseCompare size (λ(a : Bool) → λ(b : Bool) → a || b)

let orExample = assert : or 8 4 6 ≡ 6

let xor
    : Natural → Natural → Natural → Natural
    = λ(size : Natural) →
        bitwiseCompare size (λ(a : Bool) → λ(b : Bool) → a != b)

let xorExample = assert : xor 8 4 6 ≡ 2

let and
    : Natural → Natural → Natural → Natural
    = λ(size : Natural) →
        bitwiseCompare size (λ(a : Bool) → λ(b : Bool) → a && b)

let andExample = assert : and 8 4 6 ≡ 4

let shiftLeft
    : Natural → Natural → Natural → Natural
    = λ(size : Natural) →
      λ(shift : Natural) →
      λ(n : Natural) →
        let bits
            : List Bool
            = toBits size n

        let shifted =
              P.List.drop shift Bool bits # P.List.replicate shift Bool False

        in  fromBits shifted

let shiftLeftExample = assert : shiftLeft 3 2 5 ≡ 4

let shiftRight
    : Natural → Natural → Natural → Natural
    = λ(size : Natural) →
      λ(shift : Natural) →
      λ(n : Natural) →
        let bits
            : List Bool
            = toBits size n

        let shifted =
              List/reverse
                Bool
                (P.List.drop shift Bool (List/reverse Bool bits))

        in  fromBits shifted

let shiftRightExample = assert : shiftRight 3 2 7 ≡ 1

in  { and, or, shiftLeft, shiftRight, xor }