module Data.SBV.Program.SimpleLibrary(
    Data.SBV.Program.SimpleLibrary.const,

    -- * 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,
    bNand,
    bEquiv
  )
where

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


const :: SimpleComponent a
const = forall {a}. String -> SimpleSpec a -> SimpleComponent a
mkSimpleComp String
"const" forall a b. (a -> b) -> a -> b
$ forall a. Word -> ([SBV a] -> SBV a -> SBV Bool) -> SimpleSpec a
SimpleSpec Word
0 forall a b. (a -> b) -> a -> b
$ \[] SBV a
o -> SBV Bool
sTrue


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
mkSimpleComp String
"inc" forall a b. (a -> b) -> a -> b
$ forall a. Word -> ([SBV a] -> SBV a -> SBV Bool) -> 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 -> SBV Bool
.== (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
mkSimpleComp String
"dec" forall a b. (a -> b) -> a -> b
$ forall a. Word -> ([SBV a] -> SBV a -> SBV Bool) -> 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 -> SBV Bool
.== (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
mkSimpleComp String
"add" forall a b. (a -> b) -> a -> b
$ forall a. Word -> ([SBV a] -> SBV a -> SBV Bool) -> 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 -> SBV Bool
.== (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
mkSimpleComp String
"sub" forall a b. (a -> b) -> a -> b
$ forall a. Word -> ([SBV a] -> SBV a -> SBV Bool) -> 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 -> SBV Bool
.== (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
mkSimpleComp String
"mul" forall a b. (a -> b) -> a -> b
$ forall a. Word -> ([SBV a] -> SBV a -> SBV Bool) -> 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 -> SBV Bool
.== (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
mkSimpleComp String
"and" forall a b. (a -> b) -> a -> b
$ forall a. Word -> ([SBV a] -> SBV a -> SBV Bool) -> 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 -> SBV Bool
.== (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
mkSimpleComp String
"or" forall a b. (a -> b) -> a -> b
$ forall a. Word -> ([SBV a] -> SBV a -> SBV Bool) -> 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 -> SBV Bool
.== (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
mkSimpleComp String
"not" forall a b. (a -> b) -> a -> b
$ forall a. Word -> ([SBV a] -> SBV a -> SBV Bool) -> 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 -> SBV Bool
.== forall a. Bits a => a -> a
complement SBV a
i1


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

bNand :: SimpleComponent Bool
bNand :: SimpleComponent Bool
bNand = forall {a}. String -> SimpleSpec a -> SimpleComponent a
mkSimpleComp String
"bNand" forall a b. (a -> b) -> a -> b
$ forall a. Word -> ([SBV a] -> SBV a -> SBV Bool) -> SimpleSpec a
SimpleSpec Word
2 forall a b. (a -> b) -> a -> b
$ \[SBV Bool
i1,SBV Bool
i2] SBV Bool
o -> SBV Bool
o forall a. EqSymbolic a => a -> a -> SBV Bool
.== SBV Bool -> SBV Bool
sNot (SBV Bool
i1 SBV Bool -> SBV Bool -> SBV Bool
.&& SBV Bool
i2)

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