haskellsbvsymbolic-execution

Symbolic `show` for `SInt16`

I am looking for a way to turn an SInt16 into an SString. For my use case, it is enough that it does the right thing for concrete values, i.e. I will only be looking at the SString result for concrete SInt16s.

I noticed there is a Show instance for SInt16, which (of course) returns a String. It is almost good enough for my needs: for symbolic values, it returns "<symbolic> :: SInt16" and for concrete values e.g. 42, it returns "42 :: SInt16". So if not for that pesky type tag, I could use literal . show @SInt16 as my SInt16 -> SString function.

Is there a better way than editing the return value of show to cut out the type tag?

Solution

  • Something like this should do the trick:

    import Data.SBV
import Data.SBV.String

toString :: (SymVal a, Show a) => SBV a -> SString
toString = literal . maybe "<symbolic>" show . unliteral

    I get:

    *Main> toString (2 :: SInt16)
"2" :: SString
*Main> toString (uninterpret "n" :: SInt16)
"<symbolic>" :: SString