dt.hs

{-# LANGUAGE OverloadedStrings   #-}
{-# LANGUAGE DeriveDataTypeable  #-}
{-# LANGUAGE DeriveAnyClass      #-}
{-# LANGUAGE ScopedTypeVariables #-}

import Data.SBV
import Data.SBV.Char
import Data.SBV.Tuple
import Data.SBV.Control
import Data.Generics
import Data.SBV.Either

import qualified Data.SBV.List as L

-- Term type; the deriving clause is just so SBV can treat it
-- as a symbolic value; there is no other meaning to it.
-- Note that Tm cannot really be recursive.
data Tm = TmSLF  String [Float]
        | TmInt  Integer
        | TmBool Bool
        deriving (Show, HasKind, Read, SymVal, Data, SMTValue)

-- The underlying symbolic representation as an SMTLib level symbolic value
type STm = SEither (String, [Float])
                   (Either Integer Bool)

-- Extract a symbolic value in a more recognizable form
queryTm :: STm -> Query Tm
queryTm v = do sv <- getValue v
               case sv of
                 Left (s, fs)      -> return $ TmSLF s fs
                 (Right (Left i))  -> return $ TmInt i
                 (Right (Right b)) -> return $ TmBool b


-- Since we don't have case splits, we have to define recognizers ourselves.
isTmSLF :: STm -> SBool
isTmSLF = isLeft

tmSLF :: STm -> STuple String [Float]
tmSLF = fromLeft

-- Same as above
isTmTFloat :: STm -> SBool
isTmTFloat x = isRight x .&& isLeft (fromRight x)

tmInt :: STm -> SInteger
tmInt = fromLeft . fromRight

-- Same as above
isTmBool :: STm -> SBool
isTmBool x = isRight x .&& isRight (fromRight x)

tmBool :: STm -> SBool
tmBool = fromRight . fromRight

-- A very simple example
ex :: Symbolic Tm
ex = do x :: STm <- free "x"

        -- enforce a certain shape
        constrain $ isTmSLF x
        constrain $ L.length ((tmSLF x)^._2) .> 2

        -- make sure the first element in the list is a float that is at least 10
        -- and the string is hello world..
        let elts :: SList Float
            elts = (tmSLF x)^._2
            telt :: SFloat
            telt = elts L..!! 0

        -- We have to say that there are at least 1 elements, the first is an integer, and it's > 10
        -- This is clunky, but is the only way without pattern matching
        constrain $ (tmSLF x)^._1 .== "hello world"
        constrain $ L.length elts .>= 1
        constrain $ telt .>= 10

        -- grab the result
        query $ do ensureSat
                   queryTm x

-- *Main> test
-- TmSLF "hello world" [24.001955,NaN,1.469368e-39]
test :: IO Tm
test = runSMT ex