sbv-program-1.0.0.0: Component-based program synthesis using SBV
Safe HaskellSafe-Inferred
LanguageHaskell2010

Data.SBV.Program.Types

Synopsis

Documentation

type Location = Word64 Source #

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

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\).

data SimpleSpec a Source #

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

Constructors

SimpleSpec 

Fields

data SimpleComponent a Source #

A simplest library component datatype possible.

Constructors

SimpleComponent 

data SynthesisError Source #

Possible failure reasons during synthesis operation.

Instances

Instances details
Show SynthesisError Source # 
Instance details

Defined in Data.SBV.Program.Types

data IOs l Source #

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

Constructors

IOs 

Fields

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 

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 

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.

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

Eq a => Eq (ProgramTree a) Source # 
Instance details

Defined in Data.SBV.Program.Types

Ord a => Ord (ProgramTree a) Source # 
Instance details

Defined in Data.SBV.Program.Types

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