{-# LANGUAGE OverloadedStrings #-}

module Funcons.Operations.Bits where

import Funcons.Operations.Booleans (tobool,frombool)
import Funcons.Operations.Internal
import Control.Monad (join)

import qualified Data.BitVector as BV

library :: (HasValues t, Ord t) => Library t
library :: Library t
library = [(OP, ValueOp t)] -> Library t
forall t. [(OP, ValueOp t)] -> Library t
libFromList [
        (OP
"bit-vector-not", UnaryExpr t -> ValueOp t
forall t. UnaryExpr t -> ValueOp t
UnaryExpr UnaryExpr t
forall t. HasValues t => OpExpr t -> OpExpr t
bit_vector_not)
    ,   (OP
"bit-vector-and", BinaryExpr t -> ValueOp t
forall t. BinaryExpr t -> ValueOp t
BinaryExpr BinaryExpr t
forall t. HasValues t => OpExpr t -> OpExpr t -> OpExpr t
bit_vector_and)
    ,   (OP
"bit-vector-or", BinaryExpr t -> ValueOp t
forall t. BinaryExpr t -> ValueOp t
BinaryExpr BinaryExpr t
forall t. HasValues t => OpExpr t -> OpExpr t -> OpExpr t
bit_vector_or)
    ,   (OP
"bit-vector-xor", BinaryExpr t -> ValueOp t
forall t. BinaryExpr t -> ValueOp t
BinaryExpr BinaryExpr t
forall t. HasValues t => OpExpr t -> OpExpr t -> OpExpr t
bit_vector_xor)
    ,   (OP
"bit-vector-shift-left", BinaryExpr t -> ValueOp t
forall t. BinaryExpr t -> ValueOp t
BinaryExpr BinaryExpr t
forall t. HasValues t => OpExpr t -> OpExpr t -> OpExpr t
bit_vector_shift_left)
    ,   (OP
"bit-vector-logical-shift-right", BinaryExpr t -> ValueOp t
forall t. BinaryExpr t -> ValueOp t
BinaryExpr BinaryExpr t
forall t. HasValues t => OpExpr t -> OpExpr t -> OpExpr t
bit_vector_logical_shift_right)
    ,   (OP
"bit-vector-arithmetic-shift-right", BinaryExpr t -> ValueOp t
forall t. BinaryExpr t -> ValueOp t
BinaryExpr BinaryExpr t
forall t. HasValues t => OpExpr t -> OpExpr t -> OpExpr t
bit_vector_arithmetical_shift_right)
    ,   (OP
"integer-to-bit-vector", BinaryExpr t -> ValueOp t
forall t. BinaryExpr t -> ValueOp t
BinaryExpr BinaryExpr t
forall t. HasValues t => OpExpr t -> OpExpr t -> OpExpr t
integer_to_bit_vector)
    ,   (OP
"bit-vector-to-integer", UnaryExpr t -> ValueOp t
forall t. UnaryExpr t -> ValueOp t
UnaryExpr UnaryExpr t
forall t. HasValues t => OpExpr t -> OpExpr t
bit_vector_to_integer)
    ,   (OP
"bit-vector-to-natural", UnaryExpr t -> ValueOp t
forall t. UnaryExpr t -> ValueOp t
UnaryExpr UnaryExpr t
forall t. HasValues t => OpExpr t -> OpExpr t
bit_vector_to_natural)
    ]

bit_vector_not_ :: HasValues t => [OpExpr t] -> OpExpr t
bit_vector_not_ :: [OpExpr t] -> OpExpr t
bit_vector_not_ = UnaryExpr t -> [OpExpr t] -> OpExpr t
forall t. UnaryExpr t -> [OpExpr t] -> OpExpr t
unaryOp UnaryExpr t
forall t. HasValues t => OpExpr t -> OpExpr t
bit_vector_not 
bit_vector_not :: HasValues t => OpExpr t -> OpExpr t
bit_vector_not :: OpExpr t -> OpExpr t
bit_vector_not = OP -> UnaryVOp t -> OpExpr t -> OpExpr t
forall t. HasValues t => OP -> UnaryVOp t -> OpExpr t -> OpExpr t
vUnaryOp OP
"bit-vector-not" UnaryVOp t
forall t. HasValues t => Values t -> Result t
op
  where op :: Values t -> Result t
op (ADTVal Name
"bit-vector" [t]
vals) | Just [t]
bv <- (BV -> BV) -> [t] -> Maybe [t]
forall t. HasValues t => (BV -> BV) -> [t] -> Maybe [t]
apply_to_vec BV -> BV
BV.not [t]
vals = 
          t -> Result t
forall t. t -> Result t
Normal (t -> Result t) -> t -> Result t
forall a b. (a -> b) -> a -> b
$ Values t -> t
forall t. HasValues t => Values t -> t
inject (Values t -> t) -> Values t -> t
forall a b. (a -> b) -> a -> b
$ Name -> [t] -> Values t
forall t. Name -> [t] -> Values t
ADTVal Name
"bit-vector" [t]
bv
        op Values t
_ = OP -> Result t
forall t. OP -> Result t
SortErr OP
"bit-vector-not applied to a bit-vector" 

bit_vector_and_ :: HasValues t => [OpExpr t] -> OpExpr t
bit_vector_and_ :: [OpExpr t] -> OpExpr t
bit_vector_and_ = BinaryExpr t -> [OpExpr t] -> OpExpr t
forall t. BinaryExpr t -> [OpExpr t] -> OpExpr t
binaryOp BinaryExpr t
forall t. HasValues t => OpExpr t -> OpExpr t -> OpExpr t
bit_vector_and 
bit_vector_and :: HasValues t => OpExpr t -> OpExpr t -> OpExpr t
bit_vector_and :: OpExpr t -> OpExpr t -> OpExpr t
bit_vector_and = OP -> BinaryVOp t -> OpExpr t -> OpExpr t -> OpExpr t
forall t.
HasValues t =>
OP -> BinaryVOp t -> OpExpr t -> OpExpr t -> OpExpr t
vBinaryOp OP
"bit-vector-and" BinaryVOp t
forall t t.
(HasValues t, HasValues t) =>
Values t -> Values t -> Result t
op
  where op :: Values t -> Values t -> Result t
op (ADTVal Name
"bit-vector" [t]
vals1) (ADTVal Name
"bit-vector" [t]
vals2) = 
          case [t] -> Maybe [Bool]
forall t. HasValues t => [t] -> Maybe [Bool]
args_to_bools [t]
vals1 of 
            Just [Bool]
bv1 -> case (BV -> BV) -> [t] -> Maybe [t]
forall t. HasValues t => (BV -> BV) -> [t] -> Maybe [t]
apply_to_vec (\BV
bv2 -> [BV] -> BV
BV.and [[Bool] -> BV
BV.fromBits [Bool]
bv1,BV
bv2]) [t]
vals2 of
                          Just [t]
bv2 -> t -> Result t
forall t. t -> Result t
Normal (t -> Result t) -> t -> Result t
forall a b. (a -> b) -> a -> b
$ Values t -> t
forall t. HasValues t => Values t -> t
inject (Values t -> t) -> Values t -> t
forall a b. (a -> b) -> a -> b
$ Name -> [t] -> Values t
forall t. Name -> [t] -> Values t
ADTVal Name
"bit-vector" [t]
bv2
                          Maybe [t]
Nothing -> OP -> Result t
forall t. OP -> Result t
SortErr OP
"second argument of bit-vector-and not a bit-vector"
            Maybe [Bool]
Nothing -> OP -> Result t
forall t. OP -> Result t
SortErr OP
"first argument of bit-vector-and not a bit-vector"
        op Values t
_ Values t
_ = OP -> Result t
forall t. OP -> Result t
SortErr OP
"bit-vector-and not applied to two bit-vectors" 

bit_vector_or_ :: HasValues t => [OpExpr t] -> OpExpr t
bit_vector_or_ :: [OpExpr t] -> OpExpr t
bit_vector_or_ = BinaryExpr t -> [OpExpr t] -> OpExpr t
forall t. BinaryExpr t -> [OpExpr t] -> OpExpr t
binaryOp BinaryExpr t
forall t. HasValues t => OpExpr t -> OpExpr t -> OpExpr t
bit_vector_or 
bit_vector_or :: HasValues t => OpExpr t -> OpExpr t -> OpExpr t
bit_vector_or :: OpExpr t -> OpExpr t -> OpExpr t
bit_vector_or = OP -> BinaryVOp t -> OpExpr t -> OpExpr t -> OpExpr t
forall t.
HasValues t =>
OP -> BinaryVOp t -> OpExpr t -> OpExpr t -> OpExpr t
vBinaryOp OP
"bit-vector-or" BinaryVOp t
forall t t.
(HasValues t, HasValues t) =>
Values t -> Values t -> Result t
op
  where op :: Values t -> Values t -> Result t
op (ADTVal Name
"bit-vector" [t]
vals1) (ADTVal Name
"bit-vector" [t]
vals2) = 
          case [t] -> Maybe [Bool]
forall t. HasValues t => [t] -> Maybe [Bool]
args_to_bools [t]
vals1 of 
            Just [Bool]
bv1 -> case (BV -> BV) -> [t] -> Maybe [t]
forall t. HasValues t => (BV -> BV) -> [t] -> Maybe [t]
apply_to_vec (\BV
bv2 -> [BV] -> BV
BV.or [[Bool] -> BV
BV.fromBits [Bool]
bv1,BV
bv2]) [t]
vals2 of
                          Just [t]
bv2 -> t -> Result t
forall t. t -> Result t
Normal (t -> Result t) -> t -> Result t
forall a b. (a -> b) -> a -> b
$ Values t -> t
forall t. HasValues t => Values t -> t
inject (Values t -> t) -> Values t -> t
forall a b. (a -> b) -> a -> b
$ Name -> [t] -> Values t
forall t. Name -> [t] -> Values t
ADTVal Name
"bit-vector" [t]
bv2
                          Maybe [t]
Nothing -> OP -> Result t
forall t. OP -> Result t
SortErr OP
"second argument of bit-vector-or not a bit-vector"
            Maybe [Bool]
Nothing -> OP -> Result t
forall t. OP -> Result t
SortErr OP
"first argument of bit-vector-or not a bit-vector"
        op Values t
_ Values t
_ = OP -> Result t
forall t. OP -> Result t
SortErr OP
"bit-vector-or not applied to two bit-vectors" 

bit_vector_xor_ :: HasValues t => [OpExpr t] -> OpExpr t
bit_vector_xor_ :: [OpExpr t] -> OpExpr t
bit_vector_xor_ = BinaryExpr t -> [OpExpr t] -> OpExpr t
forall t. BinaryExpr t -> [OpExpr t] -> OpExpr t
binaryOp BinaryExpr t
forall t. HasValues t => OpExpr t -> OpExpr t -> OpExpr t
bit_vector_xor 
bit_vector_xor :: HasValues t => OpExpr t -> OpExpr t -> OpExpr t
bit_vector_xor :: OpExpr t -> OpExpr t -> OpExpr t
bit_vector_xor = OP -> BinaryVOp t -> OpExpr t -> OpExpr t -> OpExpr t
forall t.
HasValues t =>
OP -> BinaryVOp t -> OpExpr t -> OpExpr t -> OpExpr t
vBinaryOp OP
"bit-vector-xor" (OP -> (BV -> BV -> BV) -> BinaryVOp t
forall t t.
(HasValues t, HasValues t) =>
OP -> (BV -> BV -> BV) -> Values t -> Values t -> Result t
binary_bit_op OP
"bit-vector-xor" BV -> BV -> BV
forall a. Bits a => a -> a -> a
BV.xor)

bit_vector_shift_left_ :: HasValues t => [OpExpr t] -> OpExpr t
bit_vector_shift_left_ :: [OpExpr t] -> OpExpr t
bit_vector_shift_left_ = BinaryExpr t -> [OpExpr t] -> OpExpr t
forall t. BinaryExpr t -> [OpExpr t] -> OpExpr t
binaryOp BinaryExpr t
forall t. HasValues t => OpExpr t -> OpExpr t -> OpExpr t
bit_vector_shift_left 
bit_vector_shift_left :: HasValues t => OpExpr t -> OpExpr t -> OpExpr t
bit_vector_shift_left :: OpExpr t -> OpExpr t -> OpExpr t
bit_vector_shift_left = OP -> BinaryVOp t -> OpExpr t -> OpExpr t -> OpExpr t
forall t.
HasValues t =>
OP -> BinaryVOp t -> OpExpr t -> OpExpr t -> OpExpr t
vBinaryOp OP
"bit-vector-shift-left" (OP -> (BV -> BV -> BV) -> BinaryVOp t
forall t b t.
(HasValues t, Num b) =>
OP -> (BV -> b -> BV) -> Values t -> Values t -> Result t
bit_nat_op OP
"bit-vector-shift-left" BV -> BV -> BV
BV.shl)

bit_vector_logical_shift_right_ :: HasValues t => [OpExpr t] -> OpExpr t
bit_vector_logical_shift_right_ :: [OpExpr t] -> OpExpr t
bit_vector_logical_shift_right_ = BinaryExpr t -> [OpExpr t] -> OpExpr t
forall t. BinaryExpr t -> [OpExpr t] -> OpExpr t
binaryOp BinaryExpr t
forall t. HasValues t => OpExpr t -> OpExpr t -> OpExpr t
bit_vector_logical_shift_right 
bit_vector_logical_shift_right :: HasValues t => OpExpr t -> OpExpr t -> OpExpr t
bit_vector_logical_shift_right :: OpExpr t -> OpExpr t -> OpExpr t
bit_vector_logical_shift_right = OP -> BinaryVOp t -> OpExpr t -> OpExpr t -> OpExpr t
forall t.
HasValues t =>
OP -> BinaryVOp t -> OpExpr t -> OpExpr t -> OpExpr t
vBinaryOp OP
"bit-vector-logical-shift-right" (OP -> (BV -> BV -> BV) -> BinaryVOp t
forall t b t.
(HasValues t, Num b) =>
OP -> (BV -> b -> BV) -> Values t -> Values t -> Result t
bit_nat_op OP
"bit-vector-logical-shift-right" BV -> BV -> BV
BV.shr)

bit_vector_arithmetical_shift_right_ :: HasValues t => [OpExpr t] -> OpExpr t
bit_vector_arithmetical_shift_right_ :: [OpExpr t] -> OpExpr t
bit_vector_arithmetical_shift_right_ = BinaryExpr t -> [OpExpr t] -> OpExpr t
forall t. BinaryExpr t -> [OpExpr t] -> OpExpr t
binaryOp BinaryExpr t
forall t. HasValues t => OpExpr t -> OpExpr t -> OpExpr t
bit_vector_arithmetical_shift_right 
bit_vector_arithmetical_shift_right :: HasValues t => OpExpr t -> OpExpr t -> OpExpr t
bit_vector_arithmetical_shift_right :: OpExpr t -> OpExpr t -> OpExpr t
bit_vector_arithmetical_shift_right = OP -> BinaryVOp t -> OpExpr t -> OpExpr t -> OpExpr t
forall t.
HasValues t =>
OP -> BinaryVOp t -> OpExpr t -> OpExpr t -> OpExpr t
vBinaryOp OP
"bit-vector-arithmetical-shift-right" (OP -> (BV -> BV -> BV) -> BinaryVOp t
forall t b t.
(HasValues t, Num b) =>
OP -> (BV -> b -> BV) -> Values t -> Values t -> Result t
bit_nat_op OP
"bit-vector-arithmetical-shift-right" BV -> BV -> BV
BV.ashr)

bit_vector_to_integer_ :: HasValues t => [OpExpr t] -> OpExpr t
bit_vector_to_integer_ :: [OpExpr t] -> OpExpr t
bit_vector_to_integer_ = UnaryExpr t -> [OpExpr t] -> OpExpr t
forall t. UnaryExpr t -> [OpExpr t] -> OpExpr t
unaryOp UnaryExpr t
forall t. HasValues t => OpExpr t -> OpExpr t
bit_vector_to_integer
bit_vector_to_integer :: HasValues t => OpExpr t -> OpExpr t
bit_vector_to_integer :: OpExpr t -> OpExpr t
bit_vector_to_integer = OP -> UnaryVOp t -> OpExpr t -> OpExpr t
forall t. HasValues t => OP -> UnaryVOp t -> OpExpr t -> OpExpr t
vUnaryOp OP
"bit-vector-to-integer" UnaryVOp t
forall t t. (HasValues t, HasValues t) => Values t -> Result t
op
  where op :: Values t -> Result t
op (ADTVal Name
"bit-vector" [t]
vals) | Just [Bool]
bits <- [t] -> Maybe [Bool]
forall t. HasValues t => [t] -> Maybe [Bool]
args_to_bools [t]
vals 
          = t -> Result t
forall t. t -> Result t
Normal (t -> Result t) -> t -> Result t
forall a b. (a -> b) -> a -> b
$ Values t -> t
forall t. HasValues t => Values t -> t
inject (Values t -> t) -> Values t -> t
forall a b. (a -> b) -> a -> b
$ Integer -> Values t
forall t. Integer -> Values t
Int (Integer -> Values t) -> Integer -> Values t
forall a b. (a -> b) -> a -> b
$ BV -> Integer
BV.int ([Bool] -> BV
BV.fromBits [Bool]
bits)
        op Values t
_ = OP -> Result t
forall t. OP -> Result t
SortErr OP
"bit-vector-to-integer not applied to a bit-vector"  

bit_vector_to_natural_ :: HasValues t => [OpExpr t] -> OpExpr t
bit_vector_to_natural_ :: [OpExpr t] -> OpExpr t
bit_vector_to_natural_ = UnaryExpr t -> [OpExpr t] -> OpExpr t
forall t. UnaryExpr t -> [OpExpr t] -> OpExpr t
unaryOp UnaryExpr t
forall t. HasValues t => OpExpr t -> OpExpr t
bit_vector_to_natural
bit_vector_to_natural :: HasValues t => OpExpr t -> OpExpr t
bit_vector_to_natural :: OpExpr t -> OpExpr t
bit_vector_to_natural = OP -> UnaryVOp t -> OpExpr t -> OpExpr t
forall t. HasValues t => OP -> UnaryVOp t -> OpExpr t -> OpExpr t
vUnaryOp OP
"bit-vector-to-natural" UnaryVOp t
forall t t. (HasValues t, HasValues t) => Values t -> Result t
op
  where op :: Values t -> Result t
op (ADTVal Name
"bit-vector" [t]
vals) | Just [Bool]
bits <- [t] -> Maybe [Bool]
forall t. HasValues t => [t] -> Maybe [Bool]
args_to_bools [t]
vals 
          = t -> Result t
forall t. t -> Result t
Normal (t -> Result t) -> t -> Result t
forall a b. (a -> b) -> a -> b
$ Values t -> t
forall t. HasValues t => Values t -> t
inject (Values t -> t) -> Values t -> t
forall a b. (a -> b) -> a -> b
$ Integer -> Values t
forall t. Integer -> Values t
Nat (Integer -> Values t) -> Integer -> Values t
forall a b. (a -> b) -> a -> b
$ BV -> Integer
BV.nat ([Bool] -> BV
BV.fromBits [Bool]
bits)
        op Values t
_ = OP -> Result t
forall t. OP -> Result t
SortErr OP
"bit-vector-to-natural not applied to a bit-vector"  

integer_to_bit_vector_ :: HasValues t => [OpExpr t] -> OpExpr t
integer_to_bit_vector_ :: [OpExpr t] -> OpExpr t
integer_to_bit_vector_ = BinaryExpr t -> [OpExpr t] -> OpExpr t
forall t. BinaryExpr t -> [OpExpr t] -> OpExpr t
binaryOp BinaryExpr t
forall t. HasValues t => OpExpr t -> OpExpr t -> OpExpr t
integer_to_bit_vector
integer_to_bit_vector :: HasValues t => OpExpr t -> OpExpr t -> OpExpr t
integer_to_bit_vector :: OpExpr t -> OpExpr t -> OpExpr t
integer_to_bit_vector = OP -> BinaryVOp t -> OpExpr t -> OpExpr t -> OpExpr t
forall t.
HasValues t =>
OP -> BinaryVOp t -> OpExpr t -> OpExpr t -> OpExpr t
vBinaryOp OP
"integer-to-bit-vector" BinaryVOp t
forall t t t. HasValues t => Values t -> Values t -> Result t
op
  where op :: Values t -> Values t -> Result t
op Values t
mi Values t
mn | Int Integer
i <- Values t -> Values t
forall t. Values t -> Values t
upcastIntegers Values t
mi, Nat Integer
n <- Values t -> Values t
forall t. Values t -> Values t
upcastNaturals Values t
mn 
                 = t -> Result t
forall t. t -> Result t
Normal (t -> Result t) -> t -> Result t
forall a b. (a -> b) -> a -> b
$ Values t -> t
forall t. HasValues t => Values t -> t
inject (Values t -> t) -> Values t -> t
forall a b. (a -> b) -> a -> b
$ Name -> [t] -> Values t
forall t. Name -> [t] -> Values t
ADTVal Name
"bit-vector" ([t] -> Values t) -> [t] -> Values t
forall a b. (a -> b) -> a -> b
$ (Bool -> t) -> [Bool] -> [t]
forall a b. (a -> b) -> [a] -> [b]
map (Values t -> t
forall t. HasValues t => Values t -> t
inject (Values t -> t) -> (Bool -> Values t) -> Bool -> t
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Bool -> Values t
forall t. Bool -> Values t
tobool) ([Bool] -> [t]) -> [Bool] -> [t]
forall a b. (a -> b) -> a -> b
$
                    BV -> [Bool]
BV.toBits (Int -> Integer -> BV
forall a. Integral a => Int -> a -> BV
BV.bitVec (Integer -> Int
forall a. Num a => Integer -> a
fromInteger Integer
n) (Integer
i Integer -> Integer -> Integer
forall a. Integral a => a -> a -> a
`mod` (Integer
2 Integer -> Integer -> Integer
forall a b. (Num a, Integral b) => a -> b -> a
^ Integer
n)))
        op Values t
_ Values t
_ = OP -> Result t
forall t. OP -> Result t
SortErr OP
"integer-to-bit-vector not applied to an integer and a natural"  
--- lib

apply_to_vec :: HasValues t => (BV.BV -> BV.BV) -> [t] -> Maybe [t]
apply_to_vec :: (BV -> BV) -> [t] -> Maybe [t]
apply_to_vec BV -> BV
app =
  ([Bool] -> [t]) -> Maybe [Bool] -> Maybe [t]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap ((Bool -> t) -> [Bool] -> [t]
forall a b. (a -> b) -> [a] -> [b]
map (Values t -> t
forall t. HasValues t => Values t -> t
inject (Values t -> t) -> (Bool -> Values t) -> Bool -> t
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Bool -> Values t
forall t. Bool -> Values t
tobool) ([Bool] -> [t]) -> ([Bool] -> [Bool]) -> [Bool] -> [t]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. BV -> [Bool]
BV.toBits (BV -> [Bool]) -> ([Bool] -> BV) -> [Bool] -> [Bool]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. BV -> BV
app (BV -> BV) -> ([Bool] -> BV) -> [Bool] -> BV
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [Bool] -> BV
BV.fromBits) (Maybe [Bool] -> Maybe [t])
-> ([t] -> Maybe [Bool]) -> [t] -> Maybe [t]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [t] -> Maybe [Bool]
forall t. HasValues t => [t] -> Maybe [Bool]
args_to_bools

args_to_bools :: HasValues t => [t] -> Maybe [Bool]
args_to_bools :: [t] -> Maybe [Bool]
args_to_bools = [Maybe Bool] -> Maybe [Bool]
forall (t :: * -> *) (m :: * -> *) a.
(Traversable t, Monad m) =>
t (m a) -> m (t a)
sequence ([Maybe Bool] -> Maybe [Bool])
-> ([t] -> [Maybe Bool]) -> [t] -> Maybe [Bool]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (t -> Maybe Bool) -> [t] -> [Maybe Bool]
forall a b. (a -> b) -> [a] -> [b]
map (Maybe (Maybe Bool) -> Maybe Bool
forall (m :: * -> *) a. Monad m => m (m a) -> m a
join (Maybe (Maybe Bool) -> Maybe Bool)
-> (t -> Maybe (Maybe Bool)) -> t -> Maybe Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Values t -> Maybe Bool) -> Maybe (Values t) -> Maybe (Maybe Bool)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Values t -> Maybe Bool
forall t. Values t -> Maybe Bool
frombool (Maybe (Values t) -> Maybe (Maybe Bool))
-> (t -> Maybe (Values t)) -> t -> Maybe (Maybe Bool)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. t -> Maybe (Values t)
forall t. HasValues t => t -> Maybe (Values t)
project)

binary_bit_op :: OP -> (BV -> BV -> BV) -> Values t -> Values t -> Result t
binary_bit_op OP
fc BV -> BV -> BV
app (ADTVal Name
"bit-vector" [t]
vals1) (ADTVal Name
"bit-vector" [t]
vals2) = 
          case [t] -> Maybe [Bool]
forall t. HasValues t => [t] -> Maybe [Bool]
args_to_bools [t]
vals1 of 
            Just [Bool]
bv1 -> case (BV -> BV) -> [t] -> Maybe [t]
forall t. HasValues t => (BV -> BV) -> [t] -> Maybe [t]
apply_to_vec (BV -> BV -> BV
app ([Bool] -> BV
BV.fromBits [Bool]
bv1)) [t]
vals2 of
                          Just [t]
bv2 -> t -> Result t
forall t. t -> Result t
Normal (t -> Result t) -> t -> Result t
forall a b. (a -> b) -> a -> b
$ Values t -> t
forall t. HasValues t => Values t -> t
inject (Values t -> t) -> Values t -> t
forall a b. (a -> b) -> a -> b
$ Name -> [t] -> Values t
forall t. Name -> [t] -> Values t
ADTVal Name
"bit-vector" [t]
bv2
                          Maybe [t]
Nothing -> OP -> Result t
forall t. OP -> Result t
SortErr (OP
"second argument of " OP -> OP -> OP
forall a. [a] -> [a] -> [a]
++ OP
fc OP -> OP -> OP
forall a. [a] -> [a] -> [a]
++ OP
" not a bit-vector")
            Maybe [Bool]
Nothing -> OP -> Result t
forall t. OP -> Result t
SortErr (OP
"first argument of " OP -> OP -> OP
forall a. [a] -> [a] -> [a]
++ OP
fc OP -> OP -> OP
forall a. [a] -> [a] -> [a]
++ OP
" not a bit-vector")
binary_bit_op OP
fc BV -> BV -> BV
_ Values t
_ Values t
_ = OP -> Result t
forall t. OP -> Result t
SortErr (OP
fc OP -> OP -> OP
forall a. [a] -> [a] -> [a]
++ OP
" not applied to two bit-vectors")

bit_nat_op :: OP -> (BV -> b -> BV) -> Values t -> Values t -> Result t
bit_nat_op OP
fc BV -> b -> BV
app (ADTVal Name
"bit-vector" [t]
vals1) Values t
v2 | Nat Integer
n <- Values t -> Values t
forall t. Values t -> Values t
upcastNaturals Values t
v2 = 
          case (BV -> BV) -> [t] -> Maybe [t]
forall t. HasValues t => (BV -> BV) -> [t] -> Maybe [t]
apply_to_vec ((BV -> b -> BV) -> b -> BV -> BV
forall a b c. (a -> b -> c) -> b -> a -> c
flip BV -> b -> BV
app (Integer -> b
forall a. Num a => Integer -> a
fromInteger Integer
n)) [t]
vals1 of
            Just [t]
bv2 -> t -> Result t
forall t. t -> Result t
Normal (t -> Result t) -> t -> Result t
forall a b. (a -> b) -> a -> b
$ Values t -> t
forall t. HasValues t => Values t -> t
inject (Values t -> t) -> Values t -> t
forall a b. (a -> b) -> a -> b
$ Name -> [t] -> Values t
forall t. Name -> [t] -> Values t
ADTVal Name
"bit-vector" [t]
bv2
            Maybe [t]
Nothing -> OP -> Result t
forall t. OP -> Result t
SortErr (OP
"first argument of " OP -> OP -> OP
forall a. [a] -> [a] -> [a]
++ OP
fc OP -> OP -> OP
forall a. [a] -> [a] -> [a]
++ OP
" not a bit-vector")
bit_nat_op OP
fc BV -> b -> BV
_ Values t
_ Values t
_ = OP -> Result t
forall t. OP -> Result t
SortErr (OP
fc OP -> OP -> OP
forall a. [a] -> [a] -> [a]
++ OP
" not applied to a bit-vector and a natural")