Safe Haskell	Safe-Inferred
Language	Haskell2010

Data.SBV.Program.Types

Synopsis

module Data.Biapplicative
module Data.Bifoldable
module Data.Bitraversable
type Location = Word64
type SLocation = SWord64
class SynthSpec s a where
- specArity :: s a -> Word
- specFunc :: s a -> [SBV a] -> SBV a -> SBool
class SynthSpec spec a => SynthComponent comp spec a | comp -> spec where
- compName :: comp a -> String
- compSpec :: comp a -> spec a
- extraLocConstrs :: comp a -> [[SLocation] -> SLocation -> SBool]
- getConstValue :: comp a -> a
- putConstValue :: comp a -> a -> comp a
data SimpleSpec a = SimpleSpec {
- simpleArity :: Word
- simpleFunc :: [SBV a] -> SBV a -> SBool
}
data SimpleComponent a = SimpleComponent {
- simpleName :: String
- simpleSpec :: SimpleSpec a
- simpleVal :: a
}
mkSimpleComp :: String -> SimpleSpec a -> SimpleComponent a
data SynthesisError
data IOs l = IOs {
- _ins :: [l]
- _out :: l
}
data Instruction l a = Instruction {
- instructionIOs :: IOs l
- instructionComponent :: a
}
data Program l a = Program {
- programIOs :: IOs l
- programInstructions :: [Instruction l a]
}
toIOsList :: Program l a -> [l]
sortInstructions :: Ord l => Program l a -> Program l a
data ProgramTree a
- = InstructionNode a [ProgramTree a]
- | InputLeaf Location
buildProgramTree :: Program Location a -> ProgramTree a
buildForestResult :: Program Location a -> [ProgramTree a]

Documentation

module Data.Biapplicative

module Data.Bifoldable

module Data.Bitraversable

type Location = Word64 Source #

Type used to represent a value from the set of location variables $l_x \in L$.

type SLocation = SWord64 Source #

Symbolic Location.

class SynthSpec s a where Source #

Class for a program or a component specification $φ(\vec I, O)$. Type variable a stands for function's domain type.

Methods

specArity :: s a -> Word Source #

Number of inputs the specification function takes.

specFunc Source #

Arguments

:: s a
-> [SBV a]	Input variables. The list should be of `specArity` size.
-> SBV a	Output variable.
-> SBool

An equation that relates input variables to the output one. The equation is build up either using (.==) or in a "tabular" way using multiple (.=>) expressions. See definitions from the Data.SBV.Program.SimpleLibrary module for examples.

Instances

Instances details

SynthSpec SimpleSpec a Source #
Instance details Defined in Data.SBV.Program.Types Methods specArity :: SimpleSpec a -> Word Source # specFunc :: SimpleSpec a -> [SBV a] -> SBV a -> SBool Source #

class SynthSpec spec a => SynthComponent comp spec a | comp -> spec where Source #

A class for a library component.

Minimal complete definition

compSpec

Methods

compName :: comp a -> String Source #

Component name (optional). Used for naming SBV variables and when rendering the resulting program.

compSpec :: comp a -> spec a Source #

Component's specification.

extraLocConstrs :: comp a -> [[SLocation] -> SLocation -> SBool] Source #

Optional constraints to set on location variables $l_x \in L$.

getConstValue :: comp a -> a Source #

Method used to get the value of a constant component. It doesn't require an implementation if you don't use constant components.

putConstValue :: comp a -> a -> comp a Source #

Method used to by the synthesis procedure to set the value of a constant component. It doesn't require an implementation if you don't use constant components.

Instances

Instances details

SynthComponent SimpleComponent SimpleSpec a Source #
Instance details Defined in Data.SBV.Program.Types Methods compName :: SimpleComponent a -> String Source # compSpec :: SimpleComponent a -> SimpleSpec a Source # extraLocConstrs :: SimpleComponent a -> [[SLocation] -> SLocation -> SBool] Source # getConstValue :: SimpleComponent a -> a Source # putConstValue :: SimpleComponent a -> a -> SimpleComponent a Source #

data SimpleSpec a Source #

A simplest specification datatype possible. Type variable a stands for function's domain type.

Constructors

SimpleSpec
Fields simpleArity :: Word simpleFunc :: [SBV a] -> SBV a -> SBool

Instances

Instances details

SynthSpec SimpleSpec a Source #
Instance details Defined in Data.SBV.Program.Types Methods specArity :: SimpleSpec a -> Word Source # specFunc :: SimpleSpec a -> [SBV a] -> SBV a -> SBool Source #
SynthComponent SimpleComponent SimpleSpec a Source #
Instance details Defined in Data.SBV.Program.Types Methods compName :: SimpleComponent a -> String Source # compSpec :: SimpleComponent a -> SimpleSpec a Source # extraLocConstrs :: SimpleComponent a -> [[SLocation] -> SLocation -> SBool] Source # getConstValue :: SimpleComponent a -> a Source # putConstValue :: SimpleComponent a -> a -> SimpleComponent a Source #

data SimpleComponent a Source #

A simplest library component datatype possible.

Constructors

SimpleComponent
Fields simpleName :: String simpleSpec :: SimpleSpec a simpleVal :: a

Instances

Instances details

SynthComponent SimpleComponent SimpleSpec a Source #
Instance details Defined in Data.SBV.Program.Types Methods compName :: SimpleComponent a -> String Source # compSpec :: SimpleComponent a -> SimpleSpec a Source # extraLocConstrs :: SimpleComponent a -> [[SLocation] -> SLocation -> SBool] Source # getConstValue :: SimpleComponent a -> a Source # putConstValue :: SimpleComponent a -> a -> SimpleComponent a Source #
Show (SimpleComponent spec) Source #
Instance details Defined in Data.SBV.Program.Types Methods showsPrec :: Int -> SimpleComponent spec -> ShowS # show :: SimpleComponent spec -> String # showList :: [SimpleComponent spec] -> ShowS #

mkSimpleComp :: String -> SimpleSpec a -> SimpleComponent a Source #

data SynthesisError Source #

Possible failure reasons during synthesis operation.

Constructors

ErrorUnsat
ErrorUnknown String
ErrorZeroResultsRequested
ErrorSeedingFailed

Instances

Instances details

Show SynthesisError Source #
Instance details Defined in Data.SBV.Program.Types Methods showsPrec :: Int -> SynthesisError -> ShowS # show :: SynthesisError -> String # showList :: [SynthesisError] -> ShowS #

data IOs l Source #

A datatype holding inputs and output of something. Usual types for l are Location and SLocation.

Constructors

IOs
Fields _ins :: [l] _out :: l

Instances

Instances details

Foldable IOs Source #
Instance details Defined in Data.SBV.Program.Types Methods fold :: Monoid m => IOs m -> m # foldMap :: Monoid m => (a -> m) -> IOs a -> m # foldMap' :: Monoid m => (a -> m) -> IOs a -> m # foldr :: (a -> b -> b) -> b -> IOs a -> b # foldr' :: (a -> b -> b) -> b -> IOs a -> b # foldl :: (b -> a -> b) -> b -> IOs a -> b # foldl' :: (b -> a -> b) -> b -> IOs a -> b # foldr1 :: (a -> a -> a) -> IOs a -> a # foldl1 :: (a -> a -> a) -> IOs a -> a # toList :: IOs a -> [a] # null :: IOs a -> Bool # length :: IOs a -> Int # elem :: Eq a => a -> IOs a -> Bool # maximum :: Ord a => IOs a -> a # minimum :: Ord a => IOs a -> a # sum :: Num a => IOs a -> a # product :: Num a => IOs a -> a #
Traversable IOs Source #
Instance details Defined in Data.SBV.Program.Types Methods traverse :: Applicative f => (a -> f b) -> IOs a -> f (IOs b) # sequenceA :: Applicative f => IOs (f a) -> f (IOs a) # mapM :: Monad m => (a -> m b) -> IOs a -> m (IOs b) # sequence :: Monad m => IOs (m a) -> m (IOs a) #
Functor IOs Source #
Instance details Defined in Data.SBV.Program.Types Methods fmap :: (a -> b) -> IOs a -> IOs b # (<$) :: a -> IOs b -> IOs a #
Show l => Show (IOs l) Source #
Instance details Defined in Data.SBV.Program.Types Methods showsPrec :: Int -> IOs l -> ShowS # show :: IOs l -> String # showList :: [IOs l] -> ShowS #
Eq l => Eq (IOs l) Source #
Instance details Defined in Data.SBV.Program.Types Methods (==) :: IOs l -> IOs l -> Bool # (/=) :: IOs l -> IOs l -> Bool #
Ord l => Ord (IOs l) Source #
Instance details Defined in Data.SBV.Program.Types Methods compare :: IOs l -> IOs l -> Ordering # (<) :: IOs l -> IOs l -> Bool # (<=) :: IOs l -> IOs l -> Bool # (>) :: IOs l -> IOs l -> Bool # (>=) :: IOs l -> IOs l -> Bool # max :: IOs l -> IOs l -> IOs l # min :: IOs l -> IOs l -> IOs l #
EqSymbolic l => EqSymbolic (IOs l) Source #
Instance details Defined in Data.SBV.Program.Types Methods (.==) :: IOs l -> IOs l -> SBool # (./=) :: IOs l -> IOs l -> SBool # (.===) :: IOs l -> IOs l -> SBool # (./==) :: IOs l -> IOs l -> SBool # distinct :: [IOs l] -> SBool # distinctExcept :: [IOs l] -> [IOs l] -> SBool # allEqual :: [IOs l] -> SBool # sElem :: IOs l -> [IOs l] -> SBool # sNotElem :: IOs l -> [IOs l] -> SBool #

data Instruction l a Source #

A datatype that holds a SynthComponent with inputs and output locations.

Constructors

Instruction
Fields instructionIOs :: IOs l instructionComponent :: a

Instances

Instances details

Bifoldable Instruction Source #
Instance details Defined in Data.SBV.Program.Types Methods bifold :: Monoid m => Instruction m m -> m # bifoldMap :: Monoid m => (a -> m) -> (b -> m) -> Instruction a b -> m # bifoldr :: (a -> c -> c) -> (b -> c -> c) -> c -> Instruction a b -> c # bifoldl :: (c -> a -> c) -> (c -> b -> c) -> c -> Instruction a b -> c #
Bifunctor Instruction Source #
Instance details Defined in Data.SBV.Program.Types Methods bimap :: (a -> b) -> (c -> d) -> Instruction a c -> Instruction b d # first :: (a -> b) -> Instruction a c -> Instruction b c # second :: (b -> c) -> Instruction a b -> Instruction a c #
Bitraversable Instruction Source #
Instance details Defined in Data.SBV.Program.Types Methods bitraverse :: Applicative f => (a -> f c) -> (b -> f d) -> Instruction a b -> f (Instruction c d) #
(Show l, Show a) => Show (Instruction l a) Source #
Instance details Defined in Data.SBV.Program.Types Methods showsPrec :: Int -> Instruction l a -> ShowS # show :: Instruction l a -> String # showList :: [Instruction l a] -> ShowS #
(Eq l, Eq a) => Eq (Instruction l a) Source #
Instance details Defined in Data.SBV.Program.Types Methods (==) :: Instruction l a -> Instruction l a -> Bool # (/=) :: Instruction l a -> Instruction l a -> Bool #
(Ord l, Ord a) => Ord (Instruction l a) Source #
Instance details Defined in Data.SBV.Program.Types Methods compare :: Instruction l a -> Instruction l a -> Ordering # (<) :: Instruction l a -> Instruction l a -> Bool # (<=) :: Instruction l a -> Instruction l a -> Bool # (>) :: Instruction l a -> Instruction l a -> Bool # (>=) :: Instruction l a -> Instruction l a -> Bool # max :: Instruction l a -> Instruction l a -> Instruction l a # min :: Instruction l a -> Instruction l a -> Instruction l a #

data Program l a Source #

A datatype that unites program instructions with IOs of the program itself.

Constructors

Program
Fields programIOs :: IOs l programInstructions :: [Instruction l a]

Instances

Instances details

Bifoldable Program Source #
Instance details Defined in Data.SBV.Program.Types Methods bifold :: Monoid m => Program m m -> m # bifoldMap :: Monoid m => (a -> m) -> (b -> m) -> Program a b -> m # bifoldr :: (a -> c -> c) -> (b -> c -> c) -> c -> Program a b -> c # bifoldl :: (c -> a -> c) -> (c -> b -> c) -> c -> Program a b -> c #
Bifunctor Program Source #
Instance details Defined in Data.SBV.Program.Types Methods bimap :: (a -> b) -> (c -> d) -> Program a c -> Program b d # first :: (a -> b) -> Program a c -> Program b c # second :: (b -> c) -> Program a b -> Program a c #
Bitraversable Program Source #
Instance details Defined in Data.SBV.Program.Types Methods bitraverse :: Applicative f => (a -> f c) -> (b -> f d) -> Program a b -> f (Program c d) #
(Show l, Show a) => Show (Program l a) Source #
Instance details Defined in Data.SBV.Program.Types Methods showsPrec :: Int -> Program l a -> ShowS # show :: Program l a -> String # showList :: [Program l a] -> ShowS #
(Eq l, Eq a) => Eq (Program l a) Source #
Instance details Defined in Data.SBV.Program.Types Methods (==) :: Program l a -> Program l a -> Bool # (/=) :: Program l a -> Program l a -> Bool #
(Ord l, Ord a) => Ord (Program l a) Source #
Instance details Defined in Data.SBV.Program.Types Methods compare :: Program l a -> Program l a -> Ordering # (<) :: Program l a -> Program l a -> Bool # (<=) :: Program l a -> Program l a -> Bool # (>) :: Program l a -> Program l a -> Bool # (>=) :: Program l a -> Program l a -> Bool # max :: Program l a -> Program l a -> Program l a # min :: Program l a -> Program l a -> Program l a #

toIOsList :: Program l a -> [l] Source #

Extract all locations from the program as a list, including locations of instructions.

sortInstructions :: Ord l => Program l a -> Program l a Source #

Sorts program's instructions by their output location.

data ProgramTree a Source #

A Program converted into a tree-like structure.

Constructors

InstructionNode a [ProgramTree a]
InputLeaf Location

Instances

Instances details

Foldable ProgramTree Source #
Instance details Defined in Data.SBV.Program.Types Methods fold :: Monoid m => ProgramTree m -> m # foldMap :: Monoid m => (a -> m) -> ProgramTree a -> m # foldMap' :: Monoid m => (a -> m) -> ProgramTree a -> m # foldr :: (a -> b -> b) -> b -> ProgramTree a -> b # foldr' :: (a -> b -> b) -> b -> ProgramTree a -> b # foldl :: (b -> a -> b) -> b -> ProgramTree a -> b # foldl' :: (b -> a -> b) -> b -> ProgramTree a -> b # foldr1 :: (a -> a -> a) -> ProgramTree a -> a # foldl1 :: (a -> a -> a) -> ProgramTree a -> a # toList :: ProgramTree a -> [a] # null :: ProgramTree a -> Bool # length :: ProgramTree a -> Int # elem :: Eq a => a -> ProgramTree a -> Bool # maximum :: Ord a => ProgramTree a -> a # minimum :: Ord a => ProgramTree a -> a # sum :: Num a => ProgramTree a -> a # product :: Num a => ProgramTree a -> a #
Functor ProgramTree Source #
Instance details Defined in Data.SBV.Program.Types Methods fmap :: (a -> b) -> ProgramTree a -> ProgramTree b # (<$) :: a -> ProgramTree b -> ProgramTree a #
Show a => Show (ProgramTree a) Source #
Instance details Defined in Data.SBV.Program.Types Methods showsPrec :: Int -> ProgramTree a -> ShowS # show :: ProgramTree a -> String # showList :: [ProgramTree a] -> ShowS #
Eq a => Eq (ProgramTree a) Source #
Instance details Defined in Data.SBV.Program.Types Methods (==) :: ProgramTree a -> ProgramTree a -> Bool # (/=) :: ProgramTree a -> ProgramTree a -> Bool #
Ord a => Ord (ProgramTree a) Source #
Instance details Defined in Data.SBV.Program.Types Methods compare :: ProgramTree a -> ProgramTree a -> Ordering # (<) :: ProgramTree a -> ProgramTree a -> Bool # (<=) :: ProgramTree a -> ProgramTree a -> Bool # (>) :: ProgramTree a -> ProgramTree a -> Bool # (>=) :: ProgramTree a -> ProgramTree a -> Bool # max :: ProgramTree a -> ProgramTree a -> ProgramTree a # min :: ProgramTree a -> ProgramTree a -> ProgramTree a #

buildProgramTree :: Program Location a -> ProgramTree a Source #

Create a ProgramTree for a given Program by resolving its Locations. This function effectively performs dead code elimination.

buildForestResult :: Program Location a -> [ProgramTree a] Source #

Create a ProgramTree for each unused output in the Program