BitsBuiltin.hs

{-# LANGUAGE OverloadedStrings #-}

module Funcons.Core.Values.Primitive.BitsBuiltin where

import Funcons.EDSL
import Funcons.Types

import qualified Data.BitVector as BV

library = libFromList [
        ("bits-to-integer", ValueOp stepBits_To_Integer)
    ,   ("integer-to-bits", ValueOp stepInteger_To_Bits)
    ,   ("bits-not", ValueOp stepBits_Not)
    ,   ("bits-or", ValueOp stepBits_Or)
    ,   ("bits-and", ValueOp stepBits_And)
    ,   ("bits-xor", ValueOp stepBits_Xor)
    ,   ("bits-shift-left", ValueOp stepBits_Shift_Left)
    ,   ("bits-logical-shift-right", ValueOp stepBits_Logical_Shift_Right)
    ,   ("bits-arithmetic-shift-right", ValueOp stepBits_Arithmetic_Shift_Right)
    ,   ("bits-to-integer", ValueOp stepBits_To_Integer)
    ,   ("bits-to-natural", ValueOp stepBits_To_Natural)
    ,   ("integer-to-bits", ValueOp stepInteger_To_Bits)
    ]

stepBits_Not [Bit bv] = rewriteTo $ FValue $ Bit $ BV.not bv
stepBits_Not vs        = sortErr (applyFuncon "bits-not" (fvalues vs)) "bits-not not applied to bits"
stepBits_And [Bit bv1, Bit bv2] = rewriteTo $ FValue $ Bit (bv1 BV..&. bv2)
stepBits_And vs = sortErr (applyFuncon "bits-and" (fvalues vs)) "bits-and not applied to bits"

bits_or = applyFuncon "bits-or"
stepBits_Or [Bit bv1, Bit bv2] = rewriteTo $ FValue $ Bit (bv1 BV..|. bv2)
stepBits_Or vs = sortErr (bits_or (fvalues vs)) "bits-or not applied to bits"

bits_xor = applyFuncon "bits-xor"
stepBits_Xor [Bit bv1, Bit bv2] = rewriteTo $ FValue $ Bit (bv1 `BV.xor` bv2)
stepBits_Xor vs = sortErr (bits_xor (fvalues vs)) "bits-xor not applied to bits"

bits_shift_left = applyFuncon "bits-shift-left"
stepBits_Shift_Left [Bit bv1, vn]
    | Nat n <- upcastNaturals vn = rewriteTo $ FValue $ Bit (bv1 `BV.shl` (fromInteger n))
stepBits_Shift_Left vs = sortErr (bits_shift_left (fvalues vs)) "bits-shift not applied to bits"

bits_arithmetic_shift_right = applyFuncon "bits-arithmetic-shift_right"
stepBits_Arithmetic_Shift_Right [Bit bv1, vn]
    | Nat n <- upcastNaturals vn = rewriteTo $ FValue $ Bit (bv1 `BV.ashr` (fromInteger n))
stepBits_Arithmetic_Shift_Right vs = 
    sortErr (bits_arithmetic_shift_right (fvalues vs)) 
        "bits-arithmetic-shift-right not applied to bits"

bits_logical_shift_right = applyFuncon "bits-logical-shift-right"
stepBits_Logical_Shift_Right [Bit bv1, vn]
   | Nat n <- upcastNaturals vn = rewriteTo $ FValue $ Bit (bv1 `BV.shr` (fromInteger n))
stepBits_Logical_Shift_Right vs = 
    sortErr (bits_logical_shift_right (fvalues vs)) "bits-logical-shift-right"

bits_to_integer = applyFuncon "bits-to-integer"
stepBits_To_Integer [Bit bv] = rewriteTo $ int_ $ fromInteger $ (BV.int bv)
stepBits_To_Integer vs = sortErr (bits_to_integer (fvalues vs)) 
    "bits-to-integer not applied to bits"

bits_to_natural = applyFuncon "bits-to-natural"
stepBits_To_Natural [Bit bv] = rewriteTo $ FValue $ mk_naturals (BV.nat bv)
stepBits_To_Natural vs = sortErr (bits_to_natural (fvalues vs)) "bits-to-natural not applied to bits"
integer_to_bits = applyFuncon "integer-to-bits"
stepInteger_To_Bits [vn,vi]
    | (Nat n, Int i) <- (upcastNaturals vn, upcastIntegers vi)
            = rewriteTo $ FValue $ Bit (BV.bitVec (fromInteger n) (i `mod` (2 ^ n)))
stepInteger_To_Bits vs = sortErr (applyFuncon "integer-to-bits" (fvalues vs)) 
    "sort check: integer-to-bits(_:naturals,_:integers)"