{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeApplications #-}

module Data.SBV.Program.Utils (
  sampleSpec,

  mkVarName,
  mkInputLocName,
  mkOutputLocName,
  mkInputVarName,
  mkOutputVarName,

  writePseudocode,
  )
where

import Data.List (intercalate)
import Data.SBV
import Data.SBV.Control
import Data.SBV.Program.Types


-- | Given a 'SynthSpec' tries to generate a set of input/output values that satisfy the specification.
-- Uses solver under the hood.
sampleSpec :: forall a comp spec . (SymVal a, SynthSpec spec a) => spec a -> IO (Maybe (IOs a))
sampleSpec :: forall a comp (spec :: * -> *).
(SymVal a, SynthSpec spec a) =>
spec a -> IO (Maybe (IOs a))
sampleSpec spec a
spec = forall a. Symbolic a -> IO a
runSMT forall a b. (a -> b) -> a -> b
$ do
    -- use solver to create initial values for I
    [SBV a]
ins <- forall a. SymVal a => Int -> Symbolic [SBV a]
mkExistVars @a forall a b. (a -> b) -> a -> b
$ forall a b. (Integral a, Num b) => a -> b
fromIntegral forall a b. (a -> b) -> a -> b
$ forall (s :: * -> *) a. SynthSpec s a => s a -> Word
specArity spec a
spec
    SBV a
out <- forall a. SymVal a => Symbolic (SBV a)
sbvExists_
    forall (m :: * -> *). SolverContext m => SBool -> m ()
constrain forall a b. (a -> b) -> a -> b
$ forall (s :: * -> *) a.
SynthSpec s a =>
s a -> [SBV a] -> SBV a -> SBool
specFunc spec a
spec [SBV a]
ins SBV a
out
    forall a. Query a -> Symbolic a
query forall a b. (a -> b) -> a -> b
$ do
      CheckSatResult
r <- Query CheckSatResult
checkSat
      case CheckSatResult
r of
        CheckSatResult
Sat -> forall a. a -> Maybe a
Just forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (forall l. [l] -> l -> IOs l
IOs forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM forall a. SymVal a => SBV a -> Query a
getValue [SBV a]
ins forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> forall a. SymVal a => SBV a -> Query a
getValue SBV a
out)
        CheckSatResult
_ -> forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a. Maybe a
Nothing


-- | Creates sanitized variable name suitable for SBV.
mkVarName :: 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
mkVarName :: String -> Bool -> Bool -> Word -> String
mkVarName String
compName Bool
isLocation Bool
isOutput Word
i = String
name1 forall a. [a] -> [a] -> [a]
++ String
name2 forall a. [a] -> [a] -> [a]
++ if Bool -> Bool
not Bool
isOutput then forall a. Show a => a -> String
show Word
i else String
""
  where
    name1 :: String
name1 = if forall (t :: * -> *) a. Foldable t => t a -> Bool
null String
compName then String
"UnnamedComponent" else String
compName
    name2 :: String
name2 = (if Bool
isOutput then String
"Output" else String
"Input") forall a. [a] -> [a] -> [a]
++ if Bool
isLocation then String
"Loc" else String
""

-- | Shortcut for the more general 'mkVarName' function.
mkInputLocName :: String -> Word -> String
mkInputLocName String
compName = String -> Bool -> Bool -> Word -> String
mkVarName String
compName Bool
True Bool
False
-- | Shortcut for the more general 'mkVarName' function.
mkOutputLocName :: String -> String
mkOutputLocName String
compName = String -> Bool -> Bool -> Word -> String
mkVarName String
compName Bool
True Bool
True forall a. HasCallStack => a
undefined
-- | Shortcut for the more general 'mkVarName' function.
mkInputVarName :: String -> Word -> String
mkInputVarName String
compName = String -> Bool -> Bool -> Word -> String
mkVarName String
compName Bool
False Bool
False
-- | Shortcut for the more general 'mkVarName' function.
mkOutputVarName :: String -> String
mkOutputVarName String
compName = String -> Bool -> Bool -> Word -> String
mkVarName String
compName Bool
False Bool
True forall a. HasCallStack => a
undefined


-- | Renders the solution in SSA style.
writePseudocode :: SynthComponent comp spec a => Program Location (comp a) -> String
writePseudocode :: forall (comp :: * -> *) (spec :: * -> *) a.
SynthComponent comp spec a =>
Program Location (comp a) -> String
writePseudocode Program Location (comp a)
prog = [String] -> String
unlines (String
header forall a. a -> [a] -> [a]
: [String]
body forall a. [a] -> [a] -> [a]
++ [String]
ret)
  where
    prog' :: Program Location (comp a)
prog' = forall l a. Ord l => Program l a -> Program l a
sortInstructions Program Location (comp a)
prog
    header :: String
header = forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat [
          String
"function(",
          forall a. [a] -> [[a]] -> [a]
intercalate String
", " forall a b. (a -> b) -> a -> b
$ forall a b. (a -> b) -> [a] -> [b]
map forall a. Show a => a -> String
writeArg (forall l. IOs l -> [l]
_ins forall a b. (a -> b) -> a -> b
$ forall l a. Program l a -> IOs l
programIOs Program Location (comp a)
prog'),
          String
"):"
        ]
    body :: [String]
body = forall a b c. (a -> b -> c) -> b -> a -> c
flip forall a b. (a -> b) -> [a] -> [b]
map (forall l a. Program l a -> [Instruction l a]
programInstructions Program Location (comp a)
prog') forall a b. (a -> b) -> a -> b
$ \(Instruction (IOs {[Location]
Location
_out :: forall l. IOs l -> l
_out :: Location
_ins :: [Location]
_ins :: forall l. IOs l -> [l]
..}) comp a
comp) -> forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat [
        String
"\t%",
        forall a. Show a => a -> String
show Location
_out,
        String
" = ",
        forall (comp :: * -> *) (spec :: * -> *) a.
SynthComponent comp spec a =>
comp a -> String
compName comp a
comp,
        String
" ",
        forall a. [a] -> [[a]] -> [a]
intercalate String
", " forall a b. (a -> b) -> a -> b
$ forall a b. (a -> b) -> [a] -> [b]
map forall a. Show a => a -> String
writeArg [Location]
_ins
        ]
    ret :: [String]
ret = [String
"\treturn " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
writeArg (forall l. IOs l -> l
_out forall a b. (a -> b) -> a -> b
$ forall l a. Program l a -> IOs l
programIOs Program Location (comp a)
prog')]
    writeArg :: a -> String
writeArg a
loc = Char
'%' forall a. a -> [a] -> [a]
: forall a. Show a => a -> String
show a
loc