-- Hoogle documentation, generated by Haddock
-- See Hoogle, http://www.haskell.org/hoogle/


-- | Hardware description EDSL
--   
--   For more info, see the tutorial:
--   <a>http://projects.haskell.org/chalmers-lava2000/Doc/tutorial.pdf</a>
@package chalmers-lava2000
@version 1.6.1

module Lava.Error
data Error
DelayEval :: Error
VarEval :: Error
CombinationalLoop :: Error
BadCombinationalLoop :: Error
UndefinedWire :: Error
IncompatibleStructures :: Error
NoEquality :: Error
NoArithmetic :: Error
EnumOnSymbols :: Error
Internal_OptionNotFound :: Error
wrong :: Error -> a
instance GHC.Show.Show Lava.Error.Error
instance GHC.Classes.Eq Lava.Error.Error

module Lava.IOBuffering
noBuffering :: IO ()

module Lava.LavaRandom
type Rnd = StdGen
newRnd :: IO StdGen
next :: RandomGen g => g -> (Int, g)
split :: RandomGen g => g -> (g, g)

module Lava.MyST
data ST s a
data STRef s a
newSTRef :: a -> ST s (STRef s a)
readSTRef :: STRef s a -> ST s a
writeSTRef :: STRef s a -> a -> ST s ()
runST :: (forall s. ST s a) -> a
fixST :: (a -> ST s a) -> ST s a
unsafePerformST :: ST s a -> a
unsafeInterleaveST :: ST s a -> ST s a
unsafeIOtoST :: IO a -> ST s a
instance GHC.Classes.Eq (Lava.MyST.STRef s a)
instance GHC.Base.Functor (Lava.MyST.ST s)
instance GHC.Base.Applicative (Lava.MyST.ST s)
instance GHC.Base.Monad (Lava.MyST.ST s)

module Lava.Ref
data Ref a
ref :: a -> Ref a
deref :: Ref a -> a
memoRef :: (Ref a -> b) -> Ref a -> b
data TableIO a b
tableIO :: IO (TableIO a b)
extendIO :: TableIO a b -> Ref a -> b -> IO ()
findIO :: TableIO a b -> Ref a -> IO (Maybe b)
memoRefIO :: (Ref a -> IO b) -> Ref a -> IO b
data TableST s a b
tableST :: ST s (TableST s a b)
extendST :: TableST s a b -> Ref a -> b -> ST s ()
findST :: TableST s a b -> Ref a -> ST s (Maybe b)
memoRefST :: (Ref a -> ST s b) -> Ref a -> ST s b
instance GHC.Classes.Eq (Lava.Ref.TableST s a b)
instance GHC.Classes.Eq (Lava.Ref.TableIO a b)
instance GHC.Classes.Eq (Lava.Ref.Ref a)
instance GHC.Show.Show a => GHC.Show.Show (Lava.Ref.Ref a)

module Lava.Sequent
class Functor s => Sequent s
sequent :: (Sequent s, Monad m) => s (m a) -> m (s a)
mmap :: (Monad m, Sequent s) => (a -> m b) -> s a -> m (s b)
instance Lava.Sequent.Sequent []

module Lava.Signal
newtype Signal a
Signal :: Symbol -> Signal a
newtype Symbol
Symbol :: Ref (S Symbol) -> Symbol
data S s
Bool :: Bool -> S s
Inv :: s -> S s
And :: [s] -> S s
Or :: [s] -> S s
Xor :: [s] -> S s
VarBool :: String -> S s
DelayBool :: s -> s -> S s
Int :: Int -> S s
Neg :: s -> S s
Div :: s -> s -> S s
Mod :: s -> s -> S s
Plus :: [s] -> S s
Times :: [s] -> S s
Gte :: s -> s -> S s
Equal :: [s] -> S s
If :: s -> s -> s -> S s
VarInt :: String -> S s
DelayInt :: s -> s -> S s
symbol :: S Symbol -> Symbol
unsymbol :: Symbol -> S Symbol
bool :: Bool -> Signal Bool
low :: Signal Bool
high :: Signal Bool
inv :: Signal Bool -> Signal Bool
andl :: [Signal Bool] -> Signal Bool
orl :: [Signal Bool] -> Signal Bool
xorl :: [Signal Bool] -> Signal Bool
equalBool :: Signal Bool -> Signal Bool -> Signal Bool
ifBool :: Signal Bool -> (Signal Bool, Signal Bool) -> Signal Bool
delayBool :: Signal Bool -> Signal Bool -> Signal Bool
varBool :: String -> Signal Bool
int :: Int -> Signal Int
neg :: Signal Int -> Signal Int
divide :: Signal Int -> Signal Int -> Signal Int
modulo :: Signal Int -> Signal Int -> Signal Int
plusl :: [Signal Int] -> Signal Int
timesl :: [Signal Int] -> Signal Int
equall :: [Signal Int] -> Signal Bool
gteInt :: Signal Int -> Signal Int -> Signal Bool
equalInt :: Signal Int -> Signal Int -> Signal Bool
ifInt :: Signal Bool -> (Signal Int, Signal Int) -> Signal a
delayInt :: Signal Int -> Signal Int -> Signal Int
varInt :: String -> Signal Int
lift0 :: S Symbol -> Signal a
lift1 :: (Symbol -> S Symbol) -> Signal a -> Signal b
lift2 :: (Symbol -> Symbol -> S Symbol) -> Signal a -> Signal b -> Signal c
lift3 :: (Symbol -> Symbol -> Symbol -> S Symbol) -> Signal a -> Signal b -> Signal c -> Signal d
liftl :: ([Symbol] -> S Symbol) -> [Signal a] -> Signal c
eval :: S (S a) -> S a
evalLazy :: S (Maybe (S a)) -> Maybe (S a)
arguments :: S a -> [a]
zips :: S [a] -> [S a]
instance GHC.Classes.Eq (Lava.Signal.Signal a)
instance GHC.Show.Show (Lava.Signal.Signal a)
instance GHC.Show.Show Lava.Signal.Symbol
instance GHC.Base.Functor Lava.Signal.S
instance Lava.Sequent.Sequent Lava.Signal.S
instance GHC.Show.Show a => GHC.Show.Show (Lava.Signal.S a)

module Lava.Generic
data Struct a
Compound :: [Struct a] -> Struct a
Object :: a -> Struct a
flatten :: Struct a -> [a]
transStruct :: Struct [a] -> [Struct a]
class Generic a
struct :: Generic a => a -> Struct Symbol
construct :: Generic a => Struct Symbol -> a
data Ops
Ops :: (Symbol -> Symbol -> Signal Bool) -> (Symbol -> Symbol -> Symbol) -> (Signal Bool -> (Symbol, Symbol) -> Symbol) -> (String -> Symbol) -> Symbol -> Ops
[equalSymbol] :: Ops -> Symbol -> Symbol -> Signal Bool
[delaySymbol] :: Ops -> Symbol -> Symbol -> Symbol
[ifSymbol] :: Ops -> Signal Bool -> (Symbol, Symbol) -> Symbol
[varSymbol] :: Ops -> String -> Symbol
[zeroSymbol] :: Ops -> Symbol
opsBool :: Ops
opsInt :: Ops
unSignal :: Signal a -> Symbol
ops :: Symbol -> Ops
equal :: Generic a => (a, a) -> Signal Bool
delay :: Generic a => a -> a -> a
zeroify :: Generic a => a -> a
symbolize :: Generic a => String -> a -> a
pickSymbol :: Generic a => String -> a -> Symbol
class ConstructiveSig a
zeroSig :: ConstructiveSig a => Signal a
varSig :: ConstructiveSig a => String -> Signal a
randomSig :: ConstructiveSig a => Rnd -> Signal a
class Generic a => Constructive a
zero :: Constructive a => a
var :: Constructive a => String -> a
random :: Constructive a => Rnd -> a
zeroList :: Constructive a => Int -> [a]
varList :: Constructive a => Int -> String -> [a]
randomList :: Constructive a => Int -> Rnd -> [a]
splitRndList :: Rnd -> [Rnd]
valRnd :: Rnd -> Int
class ConstructiveSig a => FiniteSig a
domainSig :: FiniteSig a => [Signal a]
class Constructive a => Finite a
domain :: Finite a => [a]
domainList :: Finite a => Int -> [[a]]
class Choice a
ifThenElse :: Choice a => Signal Bool -> (a, a) -> a
mux :: Choice a => (Signal Bool, (a, a)) -> a
strongZipWith :: (a -> b -> c) -> [a] -> [b] -> [c]
lazyZipWith :: (a -> b -> c) -> [a] -> [b] -> [c]
instance GHC.Show.Show a => GHC.Show.Show (Lava.Generic.Struct a)
instance GHC.Classes.Eq a => GHC.Classes.Eq (Lava.Generic.Struct a)
instance Lava.Generic.Choice Lava.Signal.Symbol
instance Lava.Generic.Choice (Lava.Signal.Signal a)
instance Lava.Generic.Choice ()
instance Lava.Generic.Choice a => Lava.Generic.Choice [a]
instance (Lava.Generic.Choice a, Lava.Generic.Choice b) => Lava.Generic.Choice (a, b)
instance (Lava.Generic.Choice a, Lava.Generic.Choice b, Lava.Generic.Choice c) => Lava.Generic.Choice (a, b, c)
instance (Lava.Generic.Choice a, Lava.Generic.Choice b, Lava.Generic.Choice c, Lava.Generic.Choice d) => Lava.Generic.Choice (a, b, c, d)
instance (Lava.Generic.Choice a, Lava.Generic.Choice b, Lava.Generic.Choice c, Lava.Generic.Choice d, Lava.Generic.Choice e) => Lava.Generic.Choice (a, b, c, d, e)
instance (Lava.Generic.Choice a, Lava.Generic.Choice b, Lava.Generic.Choice c, Lava.Generic.Choice d, Lava.Generic.Choice e, Lava.Generic.Choice f) => Lava.Generic.Choice (a, b, c, d, e, f)
instance (Lava.Generic.Choice a, Lava.Generic.Choice b, Lava.Generic.Choice c, Lava.Generic.Choice d, Lava.Generic.Choice e, Lava.Generic.Choice f, Lava.Generic.Choice g) => Lava.Generic.Choice (a, b, c, d, e, f, g)
instance Lava.Generic.Choice b => Lava.Generic.Choice (a -> b)
instance Lava.Generic.FiniteSig a => Lava.Generic.Finite (Lava.Signal.Signal a)
instance Lava.Generic.Finite ()
instance (Lava.Generic.Finite a, Lava.Generic.Finite b) => Lava.Generic.Finite (a, b)
instance (Lava.Generic.Finite a, Lava.Generic.Finite b, Lava.Generic.Finite c) => Lava.Generic.Finite (a, b, c)
instance (Lava.Generic.Finite a, Lava.Generic.Finite b, Lava.Generic.Finite c, Lava.Generic.Finite d) => Lava.Generic.Finite (a, b, c, d)
instance (Lava.Generic.Finite a, Lava.Generic.Finite b, Lava.Generic.Finite c, Lava.Generic.Finite d, Lava.Generic.Finite e) => Lava.Generic.Finite (a, b, c, d, e)
instance (Lava.Generic.Finite a, Lava.Generic.Finite b, Lava.Generic.Finite c, Lava.Generic.Finite d, Lava.Generic.Finite e, Lava.Generic.Finite f) => Lava.Generic.Finite (a, b, c, d, e, f)
instance (Lava.Generic.Finite a, Lava.Generic.Finite b, Lava.Generic.Finite c, Lava.Generic.Finite d, Lava.Generic.Finite e, Lava.Generic.Finite f, Lava.Generic.Finite g) => Lava.Generic.Finite (a, b, c, d, e, f, g)
instance Lava.Generic.FiniteSig GHC.Types.Bool
instance Lava.Generic.ConstructiveSig a => Lava.Generic.Constructive (Lava.Signal.Signal a)
instance Lava.Generic.Constructive ()
instance (Lava.Generic.Constructive a, Lava.Generic.Constructive b) => Lava.Generic.Constructive (a, b)
instance (Lava.Generic.Constructive a, Lava.Generic.Constructive b, Lava.Generic.Constructive c) => Lava.Generic.Constructive (a, b, c)
instance (Lava.Generic.Constructive a, Lava.Generic.Constructive b, Lava.Generic.Constructive c, Lava.Generic.Constructive d) => Lava.Generic.Constructive (a, b, c, d)
instance (Lava.Generic.Constructive a, Lava.Generic.Constructive b, Lava.Generic.Constructive c, Lava.Generic.Constructive d, Lava.Generic.Constructive e) => Lava.Generic.Constructive (a, b, c, d, e)
instance (Lava.Generic.Constructive a, Lava.Generic.Constructive b, Lava.Generic.Constructive c, Lava.Generic.Constructive d, Lava.Generic.Constructive e, Lava.Generic.Constructive f) => Lava.Generic.Constructive (a, b, c, d, e, f)
instance (Lava.Generic.Constructive a, Lava.Generic.Constructive b, Lava.Generic.Constructive c, Lava.Generic.Constructive d, Lava.Generic.Constructive e, Lava.Generic.Constructive f, Lava.Generic.Constructive g) => Lava.Generic.Constructive (a, b, c, d, e, f, g)
instance Lava.Generic.ConstructiveSig GHC.Types.Bool
instance Lava.Generic.ConstructiveSig GHC.Types.Int
instance Lava.Generic.Generic Lava.Signal.Symbol
instance Lava.Generic.Generic (Lava.Signal.Signal a)
instance Lava.Generic.Generic ()
instance Lava.Generic.Generic a => Lava.Generic.Generic [a]
instance (Lava.Generic.Generic a, Lava.Generic.Generic b) => Lava.Generic.Generic (a, b)
instance (Lava.Generic.Generic a, Lava.Generic.Generic b, Lava.Generic.Generic c) => Lava.Generic.Generic (a, b, c)
instance (Lava.Generic.Generic a, Lava.Generic.Generic b, Lava.Generic.Generic c, Lava.Generic.Generic d) => Lava.Generic.Generic (a, b, c, d)
instance (Lava.Generic.Generic a, Lava.Generic.Generic b, Lava.Generic.Generic c, Lava.Generic.Generic d, Lava.Generic.Generic e) => Lava.Generic.Generic (a, b, c, d, e)
instance (Lava.Generic.Generic a, Lava.Generic.Generic b, Lava.Generic.Generic c, Lava.Generic.Generic d, Lava.Generic.Generic e, Lava.Generic.Generic f) => Lava.Generic.Generic (a, b, c, d, e, f)
instance (Lava.Generic.Generic a, Lava.Generic.Generic b, Lava.Generic.Generic c, Lava.Generic.Generic d, Lava.Generic.Generic e, Lava.Generic.Generic f, Lava.Generic.Generic g) => Lava.Generic.Generic (a, b, c, d, e, f, g)
instance GHC.Base.Functor Lava.Generic.Struct
instance Lava.Sequent.Sequent Lava.Generic.Struct

module Lava.Property
data Gen a
generate :: Gen a -> IO a
class ChoiceWithSig a
class Fresh a
fresh :: Fresh a => Gen a
class CoFresh a
cofresh :: (CoFresh a, Choice b, Fresh b) => Gen b -> Gen (a -> b)
double :: Gen a -> Gen (a, a)
triple :: Gen a -> Gen (a, a, a)
list :: Fresh a => Int -> Gen [a]
listOf :: Int -> Gen a -> Gen [a]
results :: Int -> Gen (a -> b) -> Gen (a -> [b])
sequential :: (CoFresh a, Fresh b, Choice b) => Int -> Gen (a -> b)
forAll :: (ShowModel a, Checkable b) => Gen a -> (a -> b) -> Property
newtype Property
P :: Gen ([Signal Bool], Model -> [[String]]) -> Property
class Checkable a
property :: Checkable a => a -> Property
class ShowModel a
showModel :: ShowModel a => Model -> a -> [String]
type Model = [(String, [String])]
properties :: Checkable a => a -> IO ([Signal Bool], Model -> [[String]])
instance (Lava.Property.Fresh a, Lava.Property.ShowModel a, Lava.Property.Checkable b) => Lava.Property.Checkable (a -> b)
instance Lava.Property.ShowModel (Lava.Signal.Signal a)
instance Lava.Property.ShowModel ()
instance (Lava.Property.ShowModel a, Lava.Property.ShowModel b) => Lava.Property.ShowModel (a, b)
instance (Lava.Property.ShowModel a, Lava.Property.ShowModel b, Lava.Property.ShowModel c) => Lava.Property.ShowModel (a, b, c)
instance (Lava.Property.ShowModel a, Lava.Property.ShowModel b, Lava.Property.ShowModel c, Lava.Property.ShowModel d) => Lava.Property.ShowModel (a, b, c, d)
instance (Lava.Property.ShowModel a, Lava.Property.ShowModel b, Lava.Property.ShowModel c, Lava.Property.ShowModel d, Lava.Property.ShowModel e) => Lava.Property.ShowModel (a, b, c, d, e)
instance (Lava.Property.ShowModel a, Lava.Property.ShowModel b, Lava.Property.ShowModel c, Lava.Property.ShowModel d, Lava.Property.ShowModel e, Lava.Property.ShowModel f) => Lava.Property.ShowModel (a, b, c, d, e, f)
instance (Lava.Property.ShowModel a, Lava.Property.ShowModel b, Lava.Property.ShowModel c, Lava.Property.ShowModel d, Lava.Property.ShowModel e, Lava.Property.ShowModel f, Lava.Property.ShowModel g) => Lava.Property.ShowModel (a, b, c, d, e, f, g)
instance Lava.Property.ShowModel a => Lava.Property.ShowModel [a]
instance Lava.Property.ShowModel (a -> b)
instance Lava.Property.Checkable Lava.Property.Property
instance Lava.Property.Checkable GHC.Types.Bool
instance Lava.Property.Checkable a => Lava.Property.Checkable (Lava.Signal.Signal a)
instance Lava.Property.Checkable a => Lava.Property.Checkable [a]
instance Lava.Property.Checkable a => Lava.Property.Checkable (Lava.Property.Gen a)
instance Lava.Property.CoFresh ()
instance Lava.Property.ChoiceWithSig a => Lava.Property.CoFresh (Lava.Signal.Signal a)
instance (Lava.Property.CoFresh a, Lava.Property.CoFresh b) => Lava.Property.CoFresh (a, b)
instance (Lava.Property.CoFresh a, Lava.Property.CoFresh b, Lava.Property.CoFresh c) => Lava.Property.CoFresh (a, b, c)
instance (Lava.Property.CoFresh a, Lava.Property.CoFresh b, Lava.Property.CoFresh c, Lava.Property.CoFresh d) => Lava.Property.CoFresh (a, b, c, d)
instance (Lava.Property.CoFresh a, Lava.Property.CoFresh b, Lava.Property.CoFresh c, Lava.Property.CoFresh d, Lava.Property.CoFresh e) => Lava.Property.CoFresh (a, b, c, d, e)
instance (Lava.Property.CoFresh a, Lava.Property.CoFresh b, Lava.Property.CoFresh c, Lava.Property.CoFresh d, Lava.Property.CoFresh e, Lava.Property.CoFresh f) => Lava.Property.CoFresh (a, b, c, d, e, f)
instance (Lava.Property.CoFresh a, Lava.Property.CoFresh b, Lava.Property.CoFresh c, Lava.Property.CoFresh d, Lava.Property.CoFresh e, Lava.Property.CoFresh f, Lava.Property.CoFresh g) => Lava.Property.CoFresh (a, b, c, d, e, f, g)
instance (Lava.Property.CoFresh a, Lava.Generic.Choice b, Lava.Property.Fresh b) => Lava.Property.Fresh (a -> b)
instance Lava.Property.CoFresh a => Lava.Property.CoFresh [a]
instance (Lava.Generic.Finite a, Lava.Property.CoFresh b) => Lava.Property.CoFresh (a -> b)
instance Lava.Property.ChoiceWithSig GHC.Types.Bool
instance Lava.Property.Fresh ()
instance Lava.Generic.ConstructiveSig a => Lava.Property.Fresh (Lava.Signal.Signal a)
instance (Lava.Property.Fresh a, Lava.Property.Fresh b) => Lava.Property.Fresh (a, b)
instance (Lava.Property.Fresh a, Lava.Property.Fresh b, Lava.Property.Fresh c) => Lava.Property.Fresh (a, b, c)
instance (Lava.Property.Fresh a, Lava.Property.Fresh b, Lava.Property.Fresh c, Lava.Property.Fresh d) => Lava.Property.Fresh (a, b, c, d)
instance (Lava.Property.Fresh a, Lava.Property.Fresh b, Lava.Property.Fresh c, Lava.Property.Fresh d, Lava.Property.Fresh e) => Lava.Property.Fresh (a, b, c, d, e)
instance (Lava.Property.Fresh a, Lava.Property.Fresh b, Lava.Property.Fresh c, Lava.Property.Fresh d, Lava.Property.Fresh e, Lava.Property.Fresh f) => Lava.Property.Fresh (a, b, c, d, e, f)
instance (Lava.Property.Fresh a, Lava.Property.Fresh b, Lava.Property.Fresh c, Lava.Property.Fresh d, Lava.Property.Fresh e, Lava.Property.Fresh f, Lava.Property.Fresh g) => Lava.Property.Fresh (a, b, c, d, e, f, g)
instance GHC.Base.Functor Lava.Property.Gen
instance GHC.Base.Applicative Lava.Property.Gen
instance GHC.Base.Monad Lava.Property.Gen

module Lava.Operators
and2 :: (Signal Bool, Signal Bool) -> Signal Bool
or2 :: (Signal Bool, Signal Bool) -> Signal Bool
xor2 :: (Signal Bool, Signal Bool) -> Signal Bool
nand2 :: (Signal Bool, Signal Bool) -> Signal Bool
nor2 :: (Signal Bool, Signal Bool) -> Signal Bool
xnor2 :: (Signal Bool, Signal Bool) -> Signal Bool
equiv :: (Signal Bool, Signal Bool) -> Signal Bool
impl :: (Signal Bool, Signal Bool) -> Signal Bool
nandl :: [Signal Bool] -> Signal Bool
norl :: [Signal Bool] -> Signal Bool
plus :: (Signal Int, Signal Int) -> Signal Int
sub :: (Signal Int, Signal Int) -> Signal Int
times :: (Signal Int, Signal Int) -> Signal Int
imod :: (Signal Int, Signal Int) -> Signal Int
idiv :: (Signal Int, Signal Int) -> Signal Int
(|->) :: Generic a => a -> a -> a
infixr 1 |->
(<==>) :: Generic a => a -> a -> Signal Bool
infix 4 <==>
(<&>) :: Signal Bool -> Signal Bool -> Signal Bool
infixr 3 <&>
(<|>) :: Signal Bool -> Signal Bool -> Signal Bool
infixr 2 <|>
(<#>) :: Signal Bool -> Signal Bool -> Signal Bool
infixr 2 <#>
(<=>) :: Signal Bool -> Signal Bool -> Signal Bool
infixr 2 <=>
(==>) :: Signal Bool -> Signal Bool -> Signal Bool
infixr 2 ==>
(<==) :: Signal Bool -> Signal Bool -> Signal Bool
infixr 2 <==
(%%) :: Signal Int -> Signal Int -> Signal Int
gte :: (Signal Int, Signal Int) -> Signal Bool
(>>==) :: Signal Int -> Signal Int -> Signal Bool
imin :: (Signal Int, Signal Int) -> Signal Int
imax :: (Signal Int, Signal Int) -> Signal Int
class SignalInt a
toSignalInt :: SignalInt a => Signal a -> Signal Int
fromSignalInt :: SignalInt a => Signal Int -> Signal a
int2bit :: Signal Int -> Signal Bool
bit2int :: Signal Bool -> Signal Int
instance Lava.Operators.SignalInt GHC.Types.Int
instance Lava.Operators.SignalInt a => GHC.Num.Num (Lava.Signal.Signal a)
instance Lava.Operators.SignalInt a => GHC.Real.Fractional (Lava.Signal.Signal a)
instance Lava.Operators.SignalInt a => GHC.Enum.Enum (Lava.Signal.Signal a)
instance Lava.Operators.SignalInt a => GHC.Classes.Ord (Lava.Signal.Signal a)

module Lava.Netlist
netlist :: Functor f => (S a -> a) -> f Symbol -> f a
netlistIO :: Sequent f => IO v -> (v -> S v -> IO ()) -> f Symbol -> IO (f v)
netlistST :: Sequent f => ST s v -> (v -> S v -> ST s ()) -> f Symbol -> ST s (f v)

module Lava.SequentialConstructive
simulateCon :: (Generic a, Generic b) => (a -> b) -> [a] -> [b]

module Lava.Sequential
simulateSeq :: (Generic a, Generic b) => (a -> b) -> [a] -> [b]

module Lava.Retime
timeTransform :: (Generic a, Generic b) => (a -> b) -> [a] -> [b]

module Lava.ConstructiveAnalysis
constructive :: (Generic a, Generic b) => (a -> b) -> a -> Signal Bool

module Lava.Combinational
simulate :: Generic b => (a -> b) -> a -> b

module Lava.SignalTry
data Signal a
Value :: a -> Signal a
Symbol :: Ref (Symbol a) -> Signal a
data Symbol a
Function :: String -> ([x] -> [y] -> a) -> [Signal x] -> [Signal y] -> Symbol a
Delay :: Signal a -> Signal a -> Symbol a
Variable :: String -> Symbol a
and2 :: (Signal Bool, Signal Bool) -> Signal Bool

module Lava.Stable
stable :: Generic a => a -> Signal Bool

module Lava.Table
table :: Sequent f => f Symbol -> ([(Int, S Int)], f Int)
tableProp :: Checkable a => a -> IO ([(Int, S Int)], [Int])

module Lava.Test
test :: (Constructive a, Show b, Generic b) => (a -> b) -> IO [b]

module Lava.LavaDir
getLavaDir :: IO FilePath

module Lava.Vhdl
writeVhdl :: (Constructive a, Generic b) => String -> (a -> b) -> IO ()
writeVhdlInput :: (Generic a, Generic b) => String -> (a -> b) -> a -> IO ()
writeVhdlInputOutput :: (Generic a, Generic b) => String -> (a -> b) -> a -> b -> IO ()

module Lava.Verification
data Option
Name :: String -> Option
ShowTime :: Option
Sat :: Int -> Option
NoBacktracking :: Option
Depth :: Int -> Option
Increasing :: Option
RestrictStates :: Option
verify :: Checkable a => a -> IO ProofResult
verifyWith :: Checkable a => [Option] -> a -> IO ProofResult
data ProofResult
Valid :: ProofResult
Falsifiable :: ProofResult
Indeterminate :: ProofResult
verifyDir :: FilePath
checkVerifyDir :: IO ()
instance GHC.Show.Show Lava.Verification.ProofResult
instance GHC.Classes.Eq Lava.Verification.ProofResult
instance GHC.Show.Show Lava.Verification.Option
instance GHC.Classes.Eq Lava.Verification.Option
instance GHC.Show.Show Lava.Verification.Indexed
instance GHC.Show.Show Lava.Verification.Timed

module Lava.Zchaff
zchaff :: Checkable a => a -> IO ProofResult

module Lava.Vis
vis :: Checkable a => a -> IO ProofResult
writeVis :: (Constructive a, Generic b) => String -> (a -> b) -> IO ()
writeVisInput :: (Generic a, Generic b) => String -> (a -> b) -> a -> IO ()
writeVisInputOutput :: (Generic a, Generic b) => String -> (a -> b) -> a -> b -> IO ()
equivCheckVisInput :: (Generic a, Generic b1, Generic b2) => (a -> b1) -> (a -> b2) -> a -> IO ProofResult

module Lava.Smv
smv :: Checkable a => a -> IO ProofResult

module Lava.Satzoo
satzoo :: Checkable a => a -> IO ProofResult

module Lava.Satnik
satnik :: Checkable a => a -> IO ProofResult

module Lava.Modoc
modoc :: Checkable a => a -> IO ProofResult

module Lava.Minisat
minisat :: Checkable a => a -> IO ProofResult

module Lava.Limmat
limmat :: Checkable a => a -> IO ProofResult

module Lava.Isc
data IscMethod
StepMin :: IscMethod
StepMax :: IscMethod
Mixed :: IscMethod
Bmc :: IscMethod
isc :: Checkable a => a -> IO ProofResult
iscWith :: Checkable a => IscMethod -> Int -> a -> IO ProofResult
instance GHC.Read.Read a => GHC.Read.Read (Lava.Isc.Sign a)
instance GHC.Show.Show a => GHC.Show.Show (Lava.Isc.Sign a)
instance GHC.Base.Functor Lava.Isc.Sign

module Lava.HeerHugo
heerhugo :: Checkable a => a -> IO ProofResult

module Lava.Fixit
fixit :: Checkable a => a -> IO ProofResult

module Lava

module Lava.SequentialCircuits
edge :: Signal Bool -> Signal Bool
toggle :: Signal Bool -> Signal Bool
delayClk :: (Generic b, Choice b) => b -> (Signal Bool, b) -> b
delayN :: (Eq a, Num a, Generic t) => a -> t -> t -> t
always :: Signal Bool -> Signal Bool
constant :: Constructive a => a -> Signal Bool
puls :: (Eq a, Num a) => a -> () -> Signal Bool
outputList :: (Foldable t, Generic b) => t b -> () -> b
rowSeq :: Constructive a1 => ((a1, b) -> (a2, a1)) -> b -> a2
rowSeqReset :: (Constructive a1, Choice a1) => ((a1, b) -> (a2, a1)) -> (Signal Bool, b) -> a2
rowSeqPeriod :: (Eq a1, Num a1, Constructive a2, Choice a2) => a1 -> ((a2, b) -> (a3, a2)) -> b -> a3

module Lava.Patterns
swap :: (b, a) -> (a, b)
swapl :: [a] -> [a]
copy :: b -> (b, b)
riffle :: [a] -> [a]
unriffle :: [a] -> [a]
zipp :: ([a], [b]) -> [(a, b)]
unzipp :: [(a1, a2)] -> ([a1], [a2])
pair :: [b] -> [(b, b)]
unpair :: [(a, a)] -> [a]
halveList :: [a] -> ([a], [a])
append :: ([a], [a]) -> [a]
serial :: (a -> b) -> (b -> c) -> a -> c
(->-) :: (a -> b) -> (b -> c) -> a -> c
infixr 5 ->-
compose :: [b -> b] -> b -> b
composeN :: Int -> (b -> b) -> b -> b
par :: (t1 -> a) -> (t2 -> b) -> (t1, t2) -> (a, b)
(-|-) :: (t1 -> a) -> (t2 -> b) -> (t1, t2) -> (a, b)
infixr 4 -|-
parl :: ([a1] -> [a2]) -> ([a1] -> [a2]) -> [a1] -> [a2]
two :: ([a1] -> [a2]) -> [a1] -> [a2]
ilv :: ([a1] -> [a2]) -> [a1] -> [a2]
iter :: (Eq t1, Num t1) => t1 -> (t2 -> t2) -> t2 -> t2
twoN :: (Eq t, Num t) => t -> ([a1] -> [a2]) -> [a1] -> [a2]
ilvN :: (Eq t, Num t) => t -> ([a1] -> [a2]) -> [a1] -> [a2]
bfly :: (Eq t, Num t) => t -> ([a] -> [a]) -> [a] -> [a]
pmap :: ((b, b) -> (a, a)) -> [b] -> [a]
tri :: (b -> b) -> [b] -> [b]
mirror :: ((b1, a1) -> (b2, a2)) -> (a1, b1) -> (a2, b2)
row :: ((b, a1) -> (a2, b)) -> (b, [a1]) -> ([a2], b)
column :: ((b, a1) -> (a1, a2)) -> ([b], a1) -> (a1, [a2])
grid :: ((b, a) -> (a, b)) -> ([b], [a]) -> ([a], [b])

module Lava.Arithmetic
halfAdd :: (Signal Bool, Signal Bool) -> (Signal Bool, Signal Bool)
fullAdd :: (Signal Bool, (Signal Bool, Signal Bool)) -> (Signal Bool, Signal Bool)
bitAdder :: (Signal Bool, [Signal Bool]) -> ([Signal Bool], Signal Bool)
adder :: (Signal Bool, ([Signal Bool], [Signal Bool])) -> ([Signal Bool], Signal Bool)
binAdder :: ([Signal Bool], [Signal Bool]) -> [Signal Bool]
bitMulti :: (Signal Bool, [Signal Bool]) -> [Signal Bool]
multi :: ([Signal Bool], [Signal Bool]) -> [Signal Bool]
numBreak :: Signal Int -> (Signal Bool, Signal Int)
int2bin :: (Eq a, Num a) => a -> Signal Int -> [Signal Bool]
bin2int :: [Signal Bool] -> Signal Int

module Lava.Eprover
eprover :: Checkable a => a -> IO ProofResult

module Lava.Captain
captain :: Checkable a => a -> IO ProofResult
