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

Data.SBV.Program.Utils

Synopsis

Documentation

sampleSpec :: forall a comp spec. (SymVal a, SynthSpec spec a) => spec a -> IO (Maybe (IOs a)) Source #

Given a SynthSpec tries to generate a set of input/output values that satisfy the specification. Uses solver under the hood.

mkVarName Source #

Arguments

:: String

Base name, which can be an empty string, in which case "UnnamedComponent" value will be used.

-> Bool

Setting isLocation to True will append "Loc" to the name.

-> Bool

If isOutput is False the value of i is also appended to the name.

-> Word

Number of an input. Can be undefined for an output.

-> String 

Creates sanitized variable name suitable for SBV.

mkInputLocName :: String -> Word -> String Source #

Shortcut for the more general mkVarName function.

mkOutputLocName :: String -> String Source #

Shortcut for the more general mkVarName function.

mkInputVarName :: String -> Word -> String Source #

Shortcut for the more general mkVarName function.

mkOutputVarName :: String -> String Source #

Shortcut for the more general mkVarName function.

writePseudocode :: SynthComponent comp spec a => Program Location (comp a) -> String Source #

Renders the solution in SSA style.