module Data.SBV.Program.SimpleLibrary(
    -- * Arithmetic components
    inc,
    dec,
    add,
    sub,
    mul,

    -- * Bitwise logic components
    Data.SBV.Program.SimpleLibrary.and,
    Data.SBV.Program.SimpleLibrary.or,
    Data.SBV.Program.SimpleLibrary.not,

    -- * Logic components
    bXor,
    bEquiv
  )
where

import Data.SBV
import Data.SBV.Program.Types


inc :: (SymVal a, Ord a, Num a) => SimpleComponent a
inc :: forall a. (SymVal a, Ord a, Num a) => SimpleComponent a
inc = forall a. String -> SimpleSpec a -> SimpleComponent a
SimpleComponent String
"inc" forall a b. (a -> b) -> a -> b
$ forall a. Word -> ([SBV a] -> SBV a -> SBool) -> SimpleSpec a
SimpleSpec Word
1 forall a b. (a -> b) -> a -> b
$ \[SBV a
i] SBV a
o -> SBV a
o forall a. EqSymbolic a => a -> a -> SBool
.== (SBV a
iforall a. Num a => a -> a -> a
+SBV a
1)

dec :: (SymVal a, Ord a, Num a) => SimpleComponent a
dec :: forall a. (SymVal a, Ord a, Num a) => SimpleComponent a
dec = forall a. String -> SimpleSpec a -> SimpleComponent a
SimpleComponent String
"dec" forall a b. (a -> b) -> a -> b
$ forall a. Word -> ([SBV a] -> SBV a -> SBool) -> SimpleSpec a
SimpleSpec Word
1 forall a b. (a -> b) -> a -> b
$ \[SBV a
i] SBV a
o -> SBV a
o forall a. EqSymbolic a => a -> a -> SBool
.== (SBV a
iforall a. Num a => a -> a -> a
-SBV a
1)

add :: (SymVal a, Ord a, Num a) => SimpleComponent a
add :: forall a. (SymVal a, Ord a, Num a) => SimpleComponent a
add = forall a. String -> SimpleSpec a -> SimpleComponent a
SimpleComponent String
"add" forall a b. (a -> b) -> a -> b
$ forall a. Word -> ([SBV a] -> SBV a -> SBool) -> SimpleSpec a
SimpleSpec Word
2 forall a b. (a -> b) -> a -> b
$ \[SBV a
i1,SBV a
i2] SBV a
o -> SBV a
o forall a. EqSymbolic a => a -> a -> SBool
.== (SBV a
i1 forall a. Num a => a -> a -> a
+ SBV a
i2)

sub :: (SymVal a, Ord a, Num a) => SimpleComponent a
sub :: forall a. (SymVal a, Ord a, Num a) => SimpleComponent a
sub = forall a. String -> SimpleSpec a -> SimpleComponent a
SimpleComponent String
"sub" forall a b. (a -> b) -> a -> b
$ forall a. Word -> ([SBV a] -> SBV a -> SBool) -> SimpleSpec a
SimpleSpec Word
2 forall a b. (a -> b) -> a -> b
$ \[SBV a
i1,SBV a
i2] SBV a
o -> SBV a
o forall a. EqSymbolic a => a -> a -> SBool
.== (SBV a
i1 forall a. Num a => a -> a -> a
- SBV a
i2)

mul :: (SymVal a, Ord a, Num a) => SimpleComponent a
mul :: forall a. (SymVal a, Ord a, Num a) => SimpleComponent a
mul = forall a. String -> SimpleSpec a -> SimpleComponent a
SimpleComponent String
"mul" forall a b. (a -> b) -> a -> b
$ forall a. Word -> ([SBV a] -> SBV a -> SBool) -> SimpleSpec a
SimpleSpec Word
2 forall a b. (a -> b) -> a -> b
$ \[SBV a
i1,SBV a
i2] SBV a
o -> SBV a
o forall a. EqSymbolic a => a -> a -> SBool
.== (SBV a
i1 forall a. Num a => a -> a -> a
* SBV a
i2)


and :: (SymVal a, Ord a, Num a, Bits a) => SimpleComponent a
and :: forall a. (SymVal a, Ord a, Num a, Bits a) => SimpleComponent a
and = forall a. String -> SimpleSpec a -> SimpleComponent a
SimpleComponent String
"and" forall a b. (a -> b) -> a -> b
$ forall a. Word -> ([SBV a] -> SBV a -> SBool) -> SimpleSpec a
SimpleSpec Word
2 forall a b. (a -> b) -> a -> b
$ \[SBV a
i1,SBV a
i2] SBV a
o -> SBV a
o forall a. EqSymbolic a => a -> a -> SBool
.== (SBV a
i1 forall a. Bits a => a -> a -> a
.&. SBV a
i2)

or :: (SymVal a, Ord a, Num a, Bits a) => SimpleComponent a
or :: forall a. (SymVal a, Ord a, Num a, Bits a) => SimpleComponent a
or = forall a. String -> SimpleSpec a -> SimpleComponent a
SimpleComponent String
"or" forall a b. (a -> b) -> a -> b
$ forall a. Word -> ([SBV a] -> SBV a -> SBool) -> SimpleSpec a
SimpleSpec Word
2 forall a b. (a -> b) -> a -> b
$ \[SBV a
i1,SBV a
i2] SBV a
o -> SBV a
o forall a. EqSymbolic a => a -> a -> SBool
.== (SBV a
i1 forall a. Bits a => a -> a -> a
.|. SBV a
i2)

not :: (SymVal a, Ord a, Num a, Bits a) => SimpleComponent a
not :: forall a. (SymVal a, Ord a, Num a, Bits a) => SimpleComponent a
not = forall a. String -> SimpleSpec a -> SimpleComponent a
SimpleComponent String
"not" forall a b. (a -> b) -> a -> b
$ forall a. Word -> ([SBV a] -> SBV a -> SBool) -> SimpleSpec a
SimpleSpec Word
1 forall a b. (a -> b) -> a -> b
$ \[SBV a
i1] SBV a
o -> SBV a
o forall a. EqSymbolic a => a -> a -> SBool
.== forall a. Bits a => a -> a
complement SBV a
i1


bXor :: SimpleComponent Bool
bXor = forall a. String -> SimpleSpec a -> SimpleComponent a
SimpleComponent String
"bXor" forall a b. (a -> b) -> a -> b
$ forall a. Word -> ([SBV a] -> SBV a -> SBool) -> SimpleSpec a
SimpleSpec Word
2 forall a b. (a -> b) -> a -> b
$ \[SBool
i1,SBool
i2] SBool
o -> SBool
o forall a. EqSymbolic a => a -> a -> SBool
.== SBool
i1 SBool -> SBool -> SBool
.<+> SBool
i2

-- | Logical equivalence implemented in "tabular" style
bEquiv :: SimpleComponent Bool
bEquiv = forall a. String -> SimpleSpec a -> SimpleComponent a
SimpleComponent String
"bEquiv" forall a b. (a -> b) -> a -> b
$ forall a. Word -> ([SBV a] -> SBV a -> SBool) -> SimpleSpec a
SimpleSpec Word
2 forall a b. (a -> b) -> a -> b
$ \[SBool
i1,SBool
i2] SBool
o -> [SBool] -> SBool
sAnd [
    SBool -> SBool
sNot SBool
i1 SBool -> SBool -> SBool
.&& SBool -> SBool
sNot SBool
i2 SBool -> SBool -> SBool
.=> SBool
o,
    SBool
i1 SBool -> SBool -> SBool
.&& SBool -> SBool
sNot SBool
i2 SBool -> SBool -> SBool
.=> SBool -> SBool
sNot SBool
o,
    SBool -> SBool
sNot SBool
i1 SBool -> SBool -> SBool
.&& SBool
i2 SBool -> SBool -> SBool
.=> SBool -> SBool
sNot SBool
o,
    SBool
i1 SBool -> SBool -> SBool
.&& SBool
i2 SBool -> SBool -> SBool
.=> SBool
o
  ]