---------------------------------------------------------------------------
-- |
-- Module      :  Data.SBV.Plugin.Analyze
-- Copyright   :  (c) Levent Erkok
-- License     :  BSD3
-- Maintainer  :  erkokl@gmail.com
-- Stability   :  experimental
--
-- Walk the GHC Core, proving theorems/checking safety as they are found
-----------------------------------------------------------------------------

{-# LANGUAGE CPP            #-}
{-# LANGUAGE NamedFieldPuns #-}

{-# OPTIONS_GHC -Wall -Werror #-}

module Data.SBV.Plugin.Analyze (analyzeBind) where

import GHC.Core.TyCo.Rep as TyCoRep
import GHC.Plugins
import GHC.Tc.Utils.TcType

import Control.Monad (unless, mplus, zipWithM)
import Control.Monad.Reader
import System.Exit

import Data.IORef

import Data.Char     (isAlpha, isAlphaNum, toLower, isUpper)
import Data.List     (intercalate, partition, nub, nubBy, sort, sortOn, isPrefixOf)
import Data.Maybe    (listToMaybe, fromMaybe)

import qualified Data.Map as M

import qualified Data.SBV           as S hiding (proveWithAny)
import qualified Data.SBV.Dynamic   as S
import qualified Data.SBV.Internals as S

import qualified Control.Exception as C

import Data.SBV.Plugin.Common
import Data.SBV.Plugin.Data

import Debug.Trace

-- | Dispatch the analyzer over bindings
analyzeBind :: Config -> CoreBind -> CoreM ()
analyzeBind :: Config -> CoreBind -> CoreM ()
analyzeBind cfg :: Config
cfg@Config{Var -> [SBVAnnotation]
sbvAnnotation :: Var -> [SBVAnnotation]
sbvAnnotation :: Config -> Var -> [SBVAnnotation]
sbvAnnotation, Env
cfgEnv :: Env
cfgEnv :: Config -> Env
cfgEnv} = CoreBind -> CoreM ()
forall {m :: * -> *}. MonadIO m => CoreBind -> m ()
go
  where go :: CoreBind -> m ()
go (NonRec Var
b CoreExpr
e) = (Var, CoreExpr) -> m ()
forall {m :: * -> *}. MonadIO m => (Var, CoreExpr) -> m ()
condProve (Var
b, CoreExpr
e)
        go (Rec [(Var, CoreExpr)]
binds)  = ((Var, CoreExpr) -> m ()) -> [(Var, CoreExpr)] -> m ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ (Var, CoreExpr) -> m ()
forall {m :: * -> *}. MonadIO m => (Var, CoreExpr) -> m ()
condProve [(Var, CoreExpr)]
binds

        condProve :: (Var, CoreExpr) -> m ()
condProve (Var
b, CoreExpr
e)
          | Bool -> Bool
not (Bool -> Bool) -> Bool -> Bool
forall a b. (a -> b) -> a -> b
$ [SBVAnnotation] -> Bool
forall a. [a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null (Var -> [SBVAnnotation]
sbvAnnotation Var
b)
          = (SBVAnnotation -> m ()) -> [SBVAnnotation] -> m ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ SBVAnnotation -> m ()
forall {m :: * -> *}. MonadIO m => SBVAnnotation -> m ()
workAnnotated (Var -> [SBVAnnotation]
sbvAnnotation Var
b)
          | TyCoRep.TyConApp TyCon
tc [Type]
_ <- Var -> Type
varType Var
b
          , Name -> String
forall a. NamedThing a => a -> String
getOccString (TyCon -> Name
tyConName TyCon
tc) String -> String -> Bool
forall a. Eq a => a -> a -> Bool
== String
"Proved"
          = IO () -> m ()
forall a. IO a -> m a
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (IO () -> m ()) -> IO () -> m ()
forall a b. (a -> b) -> a -> b
$ Config -> [SBVOption] -> Var -> CoreExpr -> IO ()
prove Config
cfg [] Var
b CoreExpr
e
          | Bool
True
          = () -> m ()
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return ()
          where workAnnotated :: SBVAnnotation -> m ()
workAnnotated (SBV [SBVOption]
opts)
                   | Just String
s <- [SBVOption] -> Maybe String
hasSkip [SBVOption]
opts
                   = IO () -> m ()
forall a. IO a -> m a
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (IO () -> m ()) -> IO () -> m ()
forall a b. (a -> b) -> a -> b
$ String -> IO ()
putStrLn (String -> IO ()) -> String -> IO ()
forall a b. (a -> b) -> a -> b
$ String
"[SBV] " String -> String -> String
forall a. [a] -> [a] -> [a]
++ DynFlags -> SrcSpan -> String
showSpan (Env -> DynFlags
flags Env
cfgEnv) ([SrcSpan] -> SrcSpan
pickSpan [Var -> SrcSpan
varSpan Var
b]) String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
" Skipping " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String -> String
forall a. Show a => a -> String
show (DynFlags -> SDoc -> String
showSDoc (Env -> DynFlags
flags Env
cfgEnv) (Var -> SDoc
forall a. Outputable a => a -> SDoc
ppr Var
b)) String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
": " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
s
                   | SBVOption
Uninterpret SBVOption -> [SBVOption] -> Bool
forall a. Eq a => a -> [a] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [SBVOption]
opts
                   = () -> m ()
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return ()
                   | Bool
True
                   = IO () -> m ()
forall a. IO a -> m a
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (IO () -> m ()) -> IO () -> m ()
forall a b. (a -> b) -> a -> b
$ Config -> [SBVOption] -> Var -> CoreExpr -> IO ()
prove Config
cfg [SBVOption]
opts Var
b CoreExpr
e
                hasSkip :: [SBVOption] -> Maybe String
hasSkip [SBVOption]
opts = [String] -> Maybe String
forall a. [a] -> Maybe a
listToMaybe [String
s | Skip String
s <- [SBVOption]
opts]

-- | Prove an SBVTheorem
prove :: Config -> [SBVOption] -> Var -> CoreExpr -> IO ()
prove :: Config -> [SBVOption] -> Var -> CoreExpr -> IO ()
prove cfg :: Config
cfg@Config{Bool
isGHCi :: Bool
isGHCi :: Config -> Bool
isGHCi} [SBVOption]
opts Var
b CoreExpr
e = do
        success <- IO Bool -> IO Bool
safely (IO Bool -> IO Bool) -> IO Bool -> IO Bool
forall a b. (a -> b) -> a -> b
$ Config -> [SBVOption] -> Var -> CoreExpr -> IO Bool
proveIt Config
cfg [SBVOption]
opts Var
b CoreExpr
e
        unless (success || isGHCi || IgnoreFailure `elem` opts) $ do
            putStrLn $ "[SBV] Failed. (Use option '" ++ show IgnoreFailure ++ "' to continue.)"
            exitFailure

-- | Safely execute an action, catching the exceptions, printing and returning False if something goes wrong
safely :: IO Bool -> IO Bool
safely :: IO Bool -> IO Bool
safely IO Bool
a = IO Bool
a IO Bool -> (SomeException -> IO Bool) -> IO Bool
forall e a. Exception e => IO a -> (e -> IO a) -> IO a
`C.catch` SomeException -> IO Bool
bad
  where bad :: C.SomeException -> IO Bool
        bad :: SomeException -> IO Bool
bad SomeException
e = do SomeException -> IO ()
forall a. Show a => a -> IO ()
print SomeException
e
                   Bool -> IO Bool
forall a. a -> IO a
forall (m :: * -> *) a. Monad m => a -> m a
return Bool
False

-- | Returns True if proof went thru
proveIt :: Config -> [SBVOption] -> Var -> CoreExpr -> IO Bool
proveIt :: Config -> [SBVOption] -> Var -> CoreExpr -> IO Bool
proveIt cfg :: Config
cfg@Config{Env
cfgEnv :: Config -> Env
cfgEnv :: Env
cfgEnv, Var -> [SBVAnnotation]
sbvAnnotation :: Config -> Var -> [SBVAnnotation]
sbvAnnotation :: Var -> [SBVAnnotation]
sbvAnnotation} [SBVOption]
opts Var
topBind CoreExpr
topExpr = do
        solverConfigs <- [SBVOption] -> IO [SMTConfig]
pickSolvers [SBVOption]
opts
        let verbose = SBVOption
Verbose    SBVOption -> [SBVOption] -> Bool
forall a. Eq a => a -> [a] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [SBVOption]
opts
            qCheck  = SBVOption
QuickCheck SBVOption -> [SBVOption] -> Bool
forall a. Eq a => a -> [a] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [SBVOption]
opts
            runProver Symbolic SVal
prop
              | Bool
qCheck = Bool -> Either Bool (Solver, NominalDiffTime, ThmResult)
forall a b. a -> Either a b
Left  (Bool -> Either Bool (Solver, NominalDiffTime, ThmResult))
-> IO Bool -> IO (Either Bool (Solver, NominalDiffTime, ThmResult))
forall a b. (a -> b) -> IO a -> IO b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
`fmap` Symbolic SVal -> IO Bool
S.svQuickCheck Symbolic SVal
prop
              | Bool
True   = (Solver, NominalDiffTime, ThmResult)
-> Either Bool (Solver, NominalDiffTime, ThmResult)
forall a b. b -> Either a b
Right ((Solver, NominalDiffTime, ThmResult)
 -> Either Bool (Solver, NominalDiffTime, ThmResult))
-> IO (Solver, NominalDiffTime, ThmResult)
-> IO (Either Bool (Solver, NominalDiffTime, ThmResult))
forall a b. (a -> b) -> IO a -> IO b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
`fmap` [SMTConfig]
-> Symbolic SVal -> IO (Solver, NominalDiffTime, ThmResult)
S.proveWithAny [SMTConfig
s{S.verbose = verbose} | SMTConfig
s <- [SMTConfig]
solverConfigs] Symbolic SVal
prop
            topLoc = Var -> SrcSpan
varSpan Var
topBind
            loc = String
"[SBV] " String -> String -> String
forall a. [a] -> [a] -> [a]
++ DynFlags -> SrcSpan -> String
showSpan (Env -> DynFlags
flags Env
cfgEnv) SrcSpan
topLoc
            slvrTag = String
", using " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
tag String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
"."
              where tag :: String
tag = case (SMTConfig -> Solver) -> [SMTConfig] -> [Solver]
forall a b. (a -> b) -> [a] -> [b]
map (SMTSolver -> Solver
S.name (SMTSolver -> Solver)
-> (SMTConfig -> SMTSolver) -> SMTConfig -> Solver
forall b c a. (b -> c) -> (a -> b) -> a -> c
. SMTConfig -> SMTSolver
S.solver) [SMTConfig]
solverConfigs of
                            []     -> String
"no solvers"  -- can't really happen
                            [Solver
x]    -> Solver -> String
forall a. Show a => a -> String
show Solver
x
                            [Solver
x, Solver
y] -> Solver -> String
forall a. Show a => a -> String
show Solver
x String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
" and " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Solver -> String
forall a. Show a => a -> String
show Solver
y
                            [Solver]
xs     -> String -> [String] -> String
forall a. [a] -> [[a]] -> [a]
intercalate String
", " ((Solver -> String) -> [Solver] -> [String]
forall a b. (a -> b) -> [a] -> [b]
map Solver -> String
forall a. Show a => a -> String
show ([Solver] -> [Solver]
forall a. HasCallStack => [a] -> [a]
init [Solver]
xs)) String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
", and " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Solver -> String
forall a. Show a => a -> String
show ([Solver] -> Solver
forall a. HasCallStack => [a] -> a
last [Solver]
xs)
        putStrLn $ "\n" ++ loc ++ (if qCheck then " QuickChecking " else " Proving ") ++ show (sh topBind) ++ slvrTag
        (finalResult, finalUninterps) <- do
                        finalResult    <- runProver (res cfgEnv topLoc)
                        finalUninterps <- readIORef (rUninterpreted cfgEnv)
                        return (finalResult, finalUninterps)
        case finalResult of
          Right (Solver
solver, NominalDiffTime
_, sres :: ThmResult
sres@(S.ThmResult SMTResult
smtRes)) -> do
                let success :: Bool
success = case SMTResult
smtRes of
                                S.Unsatisfiable{} -> Bool
True
                                S.Satisfiable{}   -> Bool
False
                                S.Unknown{}       -> Bool
False   -- conservative
                                S.ProofError{}    -> Bool
False   -- conservative
                                S.SatExtField{}   -> Bool
False   -- conservative
                                S.DeltaSat{}      -> Bool
False   -- conservative
                String -> IO ()
putStr (String -> IO ()) -> String -> IO ()
forall a b. (a -> b) -> a -> b
$ String
"[" String -> String -> String
forall a. [a] -> [a] -> [a]
++ Solver -> String
forall a. Show a => a -> String
show Solver
solver String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
"] "
                ThmResult -> IO ()
forall a. Show a => a -> IO ()
print ThmResult
sres

                -- If proof failed and there are uninterpreted non-input values, print a warning; except for "uninteresting" types
                let ok :: Type -> t Type -> Bool
ok  Type
t            = Bool -> Bool
not (Bool -> Bool) -> (t Type -> Bool) -> t Type -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Type -> Bool) -> t Type -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any (Type -> Type -> Bool
eqType Type
t)
                    eq :: (a, Type) -> (a, Type) -> Bool
eq (a
a, Type
b) (a
c, Type
d) = a
a a -> a -> Bool
forall a. Eq a => a -> a -> Bool
== a
c Bool -> Bool -> Bool
&& Type
b Type -> Type -> Bool
`eqType` Type
d
                    unintVals :: [(Var, Type)]
unintVals = ((Var, Type) -> Bool) -> [(Var, Type)] -> [(Var, Type)]
forall a. (a -> Bool) -> [a] -> [a]
filter ((Type -> [Type] -> Bool
forall {t :: * -> *}. Foldable t => Type -> t Type -> Bool
`ok` Env -> [Type]
uninteresting Env
cfgEnv) (Type -> Bool) -> ((Var, Type) -> Type) -> (Var, Type) -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Var, Type) -> Type
forall a b. (a, b) -> b
snd) ([(Var, Type)] -> [(Var, Type)]) -> [(Var, Type)] -> [(Var, Type)]
forall a b. (a -> b) -> a -> b
$ ((Var, Type) -> (Var, Type) -> Bool)
-> [(Var, Type)] -> [(Var, Type)]
forall a. (a -> a -> Bool) -> [a] -> [a]
nubBy (Var, Type) -> (Var, Type) -> Bool
forall {a}. Eq a => (a, Type) -> (a, Type) -> Bool
eq ([(Var, Type)] -> [(Var, Type)]) -> [(Var, Type)] -> [(Var, Type)]
forall a b. (a -> b) -> a -> b
$ ((Var, Type) -> Var) -> [(Var, Type)] -> [(Var, Type)]
forall b a. Ord b => (a -> b) -> [a] -> [a]
sortOn (Var, Type) -> Var
forall a b. (a, b) -> a
fst [(Var, Type)
vt | ((Var, Type)
vt, (Bool
False, String
_, Val
_)) <- [((Var, Type), (Bool, String, Val))]
finalUninterps]
                Bool -> IO () -> IO ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless (Bool
success Bool -> Bool -> Bool
|| [(Var, Type)] -> Bool
forall a. [a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [(Var, Type)]
unintVals) (IO () -> IO ()) -> IO () -> IO ()
forall a b. (a -> b) -> a -> b
$ do
                        let plu :: String
plu | [((Var, Type), (Bool, String, Val))] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [((Var, Type), (Bool, String, Val))]
finalUninterps Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
> Int
1 = String
"s:"
                                | Bool
True                      = String
":"
                            shUI :: (a, a) -> (String, String, String)
shUI (a
e, a
t) = (DynFlags -> SDoc -> String
showSDoc (Env -> DynFlags
flags Env
cfgEnv) (SrcSpan -> SDoc
forall a. Outputable a => a -> SDoc
ppr (a -> SrcSpan
forall a. NamedThing a => a -> SrcSpan
getSrcSpan a
e)), a -> String
forall {a}. Outputable a => a -> String
sh a
e, a -> String
forall {a}. Outputable a => a -> String
sh a
t)
                            ls :: [(String, String, String)]
ls   = ((Var, Type) -> (String, String, String))
-> [(Var, Type)] -> [(String, String, String)]
forall a b. (a -> b) -> [a] -> [b]
map (Var, Type) -> (String, String, String)
forall {a} {a}.
(NamedThing a, Outputable a, Outputable a) =>
(a, a) -> (String, String, String)
shUI [(Var, Type)]
unintVals
                            len1 :: Int
len1 = [Int] -> Int
forall a. Ord a => [a] -> a
forall (t :: * -> *) a. (Foldable t, Ord a) => t a -> a
maximum (Int
0 Int -> [Int] -> [Int]
forall a. a -> [a] -> [a]
: [String -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length String
s | (String
s, String
_, String
_) <- [(String, String, String)]
ls])
                            len2 :: Int
len2 = [Int] -> Int
forall a. Ord a => [a] -> a
forall (t :: * -> *) a. (Foldable t, Ord a) => t a -> a
maximum (Int
0 Int -> [Int] -> [Int]
forall a. a -> [a] -> [a]
: [String -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length String
s | (String
_, String
s, String
_) <- [(String, String, String)]
ls])
                            pad :: Int -> String -> String
pad Int
n String
s = Int -> String -> String
forall a. Int -> [a] -> [a]
take Int
n (String
s String -> String -> String
forall a. [a] -> [a] -> [a]
++ Char -> String
forall a. a -> [a]
repeat Char
' ')
                            put :: (String, String, String) -> IO ()
put (String
a, String
b, String
c) = String -> IO ()
putStrLn (String -> IO ()) -> String -> IO ()
forall a b. (a -> b) -> a -> b
$ String
"  [" String -> String -> String
forall a. [a] -> [a] -> [a]
++ Int -> String -> String
pad Int
len1 String
a String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
"] " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Int -> String -> String
pad Int
len2 String
b String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
" :: " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
c
                        String -> IO ()
putStrLn (String -> IO ()) -> String -> IO ()
forall a b. (a -> b) -> a -> b
$ String
"[SBV] Counter-example might be bogus due to uninterpreted constant" String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
plu
                        ((String, String, String) -> IO ())
-> [(String, String, String)] -> IO ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ (String, String, String) -> IO ()
put [(String, String, String)]
ls

                Bool -> IO Bool
forall a. a -> IO a
forall (m :: * -> *) a. Monad m => a -> m a
return Bool
success
          Left Bool
success -> Bool -> IO Bool
forall a. a -> IO a
forall (m :: * -> *) a. Monad m => a -> m a
return Bool
success

  where debug :: Bool
debug = SBVOption
Debug SBVOption -> [SBVOption] -> Bool
forall a. Eq a => a -> [a] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [SBVOption]
opts

        -- | Sometimes life is hard. Giving up is an option.
        cantHandle :: String -> [String] -> Eval a
        cantHandle :: forall a. String -> [String] -> Eval a
cantHandle String
w [String]
es = do Env{flags, curLoc} <- ReaderT Env Symbolic Env
forall r (m :: * -> *). MonadReader r m => m r
ask
                             let marker = String
"[SBV] " String -> String -> String
forall a. [a] -> [a] -> [a]
++ DynFlags -> SrcSpan -> String
showSpan DynFlags
flags ([SrcSpan] -> SrcSpan
pickSpan [SrcSpan]
curLoc)
                                 tag String
s = String
marker String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
" " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
s
                                 tab String
s = Int -> Char -> String
forall a. Int -> a -> [a]
replicate (String -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length String
marker) Char
' ' String -> String -> String
forall a. [a] -> [a] -> [a]
++  String
"    " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
s
                                 note  = (String -> String) -> [String] -> String
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap (String
"\n" String -> String -> String
forall a. [a] -> [a] -> [a]
++) ([String] -> String) -> [String] -> String
forall a b. (a -> b) -> a -> b
$ String -> String
tag (String
"Skipping proof. " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
w String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
":") String -> [String] -> [String]
forall a. a -> [a] -> [a]
: (String -> String) -> [String] -> [String]
forall a b. (a -> b) -> [a] -> [b]
map String -> String
tab [String]
es
#if MIN_VERSION_base(4,9,0)
                             errorWithoutStackTrace note
#else
                             error note
#endif

        res :: Env -> SrcSpan -> Symbolic SVal
res Env
initEnv SrcSpan
topLoc = do
               v <- ReaderT Env Symbolic Val -> Env -> Symbolic Val
forall r (m :: * -> *) a. ReaderT r m a -> r -> m a
runReaderT (CoreExpr -> ReaderT Env Symbolic Val
symEval CoreExpr
topExpr) Env
initEnv { curLoc     = [topLoc]
                                                         , mbListSize = listToMaybe [n | ListSize n <- opts]
                                                         , bailOut    = cantHandle
                                                         }
               case v of
                 Base SVal
r -> SVal -> Symbolic SVal
forall a. a -> Symbolic a
forall (m :: * -> *) a. Monad m => a -> m a
return SVal
r
                 Val
r      -> String -> Symbolic SVal
forall a. HasCallStack => String -> a
error (String -> Symbolic SVal) -> String -> Symbolic SVal
forall a b. (a -> b) -> a -> b
$ String
"Impossible happened. Final result reduced to a non-base value: " String -> String -> String
forall a. [a] -> [a] -> [a]
++ SDoc -> String
showSDocUnsafe (Val -> SDoc
forall a. Outputable a => a -> SDoc
ppr Val
r)

        tbd :: String -> [String] -> Eval Val
        tbd :: String -> [String] -> ReaderT Env Symbolic Val
tbd String
w [String]
ws = do Env{bailOut} <- ReaderT Env Symbolic Env
forall r (m :: * -> *). MonadReader r m => m r
ask
                      bailOut w ws

        sh :: a -> String
sh a
o = DynFlags -> SDoc -> String
showSDoc (Env -> DynFlags
flags Env
cfgEnv) (a -> SDoc
forall a. Outputable a => a -> SDoc
ppr a
o)

        -- Given an alleged theorem, first establish it has the right type, and
        -- then go ahead and evaluate it symbolicly after applying it to sufficient
        -- number of symbolic arguments
        symEval :: CoreExpr -> Eval Val
        symEval :: CoreExpr -> ReaderT Env Symbolic Val
symEval CoreExpr
e = do let ([Var]
bs, CoreExpr
body) = CoreExpr -> ([Var], CoreExpr)
forall b. Expr b -> ([b], Expr b)
collectBinders (CoreExpr -> CoreExpr
forall {b}. Expr b -> Expr b
pushLetLambda CoreExpr
e)
                       curEnv@Env{bailOut} <- ReaderT Env Symbolic Env
forall r (m :: * -> *). MonadReader r m => m r
ask
                       bodyType <- getType (pickSpan (curLoc curEnv)) (exprType body)

                       -- Figure out if there were some unmentioned variables; happens if the top
                       -- level wasn't fully saturated.
                       let (extraArgs, finalType) = walk bodyType []
                                where walk (KFun SKind
d SKind
c) [SKind]
sofar = SKind -> [SKind] -> ([SKind], SKind)
walk SKind
c (SKind
dSKind -> [SKind] -> [SKind]
forall a. a -> [a] -> [a]
:[SKind]
sofar)
                                      walk SKind
k          [SKind]
sofar = ([SKind] -> [SKind]
forall a. [a] -> [a]
reverse [SKind]
sofar, SKind
k)

                       case finalType of
                         KBase Kind
S.KBool -> do -- First collect the named arguments:
                                             argKs <- (Var -> ReaderT Env Symbolic (Var, SKind))
-> [Var] -> ReaderT Env Symbolic [(Var, SKind)]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [b]
mapM (\Var
b -> SrcSpan -> Type -> Eval SKind
getType (Var -> SrcSpan
forall a. NamedThing a => a -> SrcSpan
getSrcSpan Var
b) (Var -> Type
varType Var
b) Eval SKind
-> (SKind -> ReaderT Env Symbolic (Var, SKind))
-> ReaderT Env Symbolic (Var, SKind)
forall a b.
ReaderT Env Symbolic a
-> (a -> ReaderT Env Symbolic b) -> ReaderT Env Symbolic b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \SKind
bt -> (Var, SKind) -> ReaderT Env Symbolic (Var, SKind)
forall a. a -> ReaderT Env Symbolic a
forall (m :: * -> *) a. Monad m => a -> m a
return (Var
b, SKind
bt)) [Var]
bs
                                             let mkVar ((Var
b, SKind
k), Maybe String
mbN) = do sv <- (Env -> Env)
-> ReaderT Env Symbolic Val -> ReaderT Env Symbolic Val
forall a.
(Env -> Env) -> ReaderT Env Symbolic a -> ReaderT Env Symbolic a
forall r (m :: * -> *) a. MonadReader r m => (r -> r) -> m a -> m a
local (\Env
env -> Env
env{curLoc = varSpan b : curLoc env})
                                                                                    (ReaderT Env Symbolic Val -> ReaderT Env Symbolic Val)
-> ReaderT Env Symbolic Val -> ReaderT Env Symbolic Val
forall a b. (a -> b) -> a -> b
$ Config
-> Maybe Var
-> Maybe Type
-> SKind
-> Maybe String
-> ReaderT Env Symbolic Val
mkSym Config
cfg (Var -> Maybe Var
forall a. a -> Maybe a
Just Var
b) (Type -> Maybe Type
forall a. a -> Maybe a
Just (Var -> Type
idType Var
b)) SKind
k (Maybe String
mbN Maybe String -> Maybe String -> Maybe String
forall a. Maybe a -> Maybe a -> Maybe a
forall (m :: * -> *) a. MonadPlus m => m a -> m a -> m a
`mplus` String -> Maybe String
forall a. a -> Maybe a
Just (Var -> String
forall {a}. Outputable a => a -> String
sh Var
b))
                                                                          return ((b, k), sv)
                                             bArgs <- mapM mkVar (zip argKs (concat [map Just ns | Names ns <- opts] ++ repeat Nothing))

                                             -- Go ahead and run the body symbolically; on bArgs
                                             bRes <- local (\Env
env -> Env
env{envMap = foldr (uncurry M.insert) (envMap env) bArgs}) (go body)

                                             -- If there are extraArgs; then create symbolics and apply to the result:
                                             let feed []     Val
sres       = Val -> ReaderT Env Symbolic Val
forall a. a -> ReaderT Env Symbolic a
forall (m :: * -> *) a. Monad m => a -> m a
return Val
sres
                                                 feed (SKind
k:[SKind]
ks) (Func Maybe String
_ Val -> ReaderT Env Symbolic Val
f) = do sv <- Config
-> Maybe Var
-> Maybe Type
-> SKind
-> Maybe String
-> ReaderT Env Symbolic Val
mkSym Config
cfg Maybe Var
forall a. Maybe a
Nothing Maybe Type
forall a. Maybe a
Nothing SKind
k Maybe String
forall a. Maybe a
Nothing
                                                                             f sv >>= feed ks
                                                 feed [SKind]
ks     Val
v          = String -> ReaderT Env Symbolic Val
forall a. HasCallStack => String -> a
error (String -> ReaderT Env Symbolic Val)
-> String -> ReaderT Env Symbolic Val
forall a b. (a -> b) -> a -> b
$ String
"Impossible! Left with extra args to apply on a non-function: " String -> String -> String
forall a. [a] -> [a] -> [a]
++ ([SKind], Val) -> String
forall {a}. Outputable a => a -> String
sh ([SKind]
ks, Val
v)

                                             feed extraArgs bRes

                         SKind
_             -> String -> [String] -> ReaderT Env Symbolic Val
forall a. String -> [String] -> Eval a
bailOut String
"Non-boolean property declaration" ([[String]] -> [String]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat [ [String
"Found    : " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Type -> String
forall {a}. Outputable a => a -> String
sh (HasDebugCallStack => CoreExpr -> Type
CoreExpr -> Type
exprType CoreExpr
e)]
                                                                                             , [String
"Returning: " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Type -> String
forall {a}. Outputable a => a -> String
sh (HasDebugCallStack => CoreExpr -> Type
CoreExpr -> Type
exprType CoreExpr
body) | Bool -> Bool
not ([Var] -> Bool
forall a. [a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [Var]
bs)]
                                                                                             , [String
"Expected : Bool" String -> String -> String
forall a. [a] -> [a] -> [a]
++ if [Var] -> Bool
forall a. [a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [Var]
bs then String
"" else String
" result"]
                                                                                             ])
          where -- Sometimes the core has a wrapper let, floated out on top. Float that in.
                pushLetLambda :: Expr b -> Expr b
pushLetLambda (Let Bind b
b (Lam b
x Expr b
bd)) = b -> Expr b -> Expr b
forall b. b -> Expr b -> Expr b
Lam b
x (Expr b -> Expr b
pushLetLambda (Bind b -> Expr b -> Expr b
forall b. Bind b -> Expr b -> Expr b
Let Bind b
b Expr b
bd))
                pushLetLambda Expr b
o                  = Expr b
o

        isUninterpretedBinding :: Var -> Bool
        isUninterpretedBinding :: Var -> Bool
isUninterpretedBinding Var
v = ([SBVOption] -> Bool) -> [[SBVOption]] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any (SBVOption
Uninterpret SBVOption -> [SBVOption] -> Bool
forall a. Eq a => a -> [a] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem`) [[SBVOption]
opt | SBV [SBVOption]
opt <- Var -> [SBVAnnotation]
sbvAnnotation Var
v]

        go :: CoreExpr -> Eval Val
        go :: CoreExpr -> ReaderT Env Symbolic Val
go (Tick CoreTickish
t CoreExpr
e) = (Env -> Env)
-> ReaderT Env Symbolic Val -> ReaderT Env Symbolic Val
forall a.
(Env -> Env) -> ReaderT Env Symbolic a -> ReaderT Env Symbolic a
forall r (m :: * -> *) a. MonadReader r m => (r -> r) -> m a -> m a
local (\Env
envMap -> Env
envMap{curLoc = tickSpan t : curLoc envMap}) (ReaderT Env Symbolic Val -> ReaderT Env Symbolic Val)
-> ReaderT Env Symbolic Val -> ReaderT Env Symbolic Val
forall a b. (a -> b) -> a -> b
$ CoreExpr -> ReaderT Env Symbolic Val
go CoreExpr
e
        go CoreExpr
e          = Type -> CoreExpr -> ReaderT Env Symbolic Val
tgo (HasDebugCallStack => CoreExpr -> Type
CoreExpr -> Type
exprType CoreExpr
e) CoreExpr
e

        debugTrace :: String -> a -> a
debugTrace String
s a
w
          | Bool
debug = String -> a -> a
forall a. String -> a -> a
trace (String
"--> " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
s) a
w
          | Bool
True  = a
w

        -- Main symbolic evaluator:
        tgo :: Type -> CoreExpr -> Eval Val

        tgo :: Type -> CoreExpr -> ReaderT Env Symbolic Val
tgo Type
t CoreExpr
e | String -> Bool -> Bool
forall a. String -> a -> a
debugTrace ((CoreExpr, Type) -> String
forall {a}. Outputable a => a -> String
sh (CoreExpr
e, Type
t)) Bool
False = ReaderT Env Symbolic Val
forall a. HasCallStack => a
undefined

        tgo Type
t (Var Var
v) = do Env{envMap, coreMap} <- ReaderT Env Symbolic Env
forall r (m :: * -> *). MonadReader r m => m r
ask
                           k <- getType (getSrcSpan v) t
                           case (v, k) `M.lookup` envMap of
                             Just Val
b  -> Val -> ReaderT Env Symbolic Val
forall a. a -> ReaderT Env Symbolic a
forall (m :: * -> *) a. Monad m => a -> m a
return Val
b
                             Maybe Val
Nothing -> case Var
v Var -> Map Var (SrcSpan, CoreExpr) -> Maybe (SrcSpan, CoreExpr)
forall k a. Ord k => k -> Map k a -> Maybe a
`M.lookup` Map Var (SrcSpan, CoreExpr)
coreMap of
                                           Just (SrcSpan
l, CoreExpr
b)  -> if Var -> Bool
isUninterpretedBinding Var
v
                                                           then Bool -> Type -> Var -> ReaderT Env Symbolic Val
uninterpret Bool
False Type
t Var
v
                                                           else (Env -> Env)
-> ReaderT Env Symbolic Val -> ReaderT Env Symbolic Val
forall a.
(Env -> Env) -> ReaderT Env Symbolic a -> ReaderT Env Symbolic a
forall r (m :: * -> *) a. MonadReader r m => (r -> r) -> m a -> m a
local (\Env
env -> Env
env{curLoc = l : curLoc env}) (ReaderT Env Symbolic Val -> ReaderT Env Symbolic Val)
-> ReaderT Env Symbolic Val -> ReaderT Env Symbolic Val
forall a b. (a -> b) -> a -> b
$ CoreExpr -> ReaderT Env Symbolic Val
go CoreExpr
b
                                           Maybe (SrcSpan, CoreExpr)
Nothing      -> String -> ReaderT Env Symbolic Val -> ReaderT Env Symbolic Val
forall a. String -> a -> a
debugTrace (String
"Uninterpreting: " String -> String -> String
forall a. [a] -> [a] -> [a]
++ (Var, SKind, [Var]) -> String
forall {a}. Outputable a => a -> String
sh (Var
v, SKind
k, [Var] -> [Var]
forall a. Eq a => [a] -> [a]
nub ([Var] -> [Var]) -> [Var] -> [Var]
forall a b. (a -> b) -> a -> b
$ [Var] -> [Var]
forall a. Ord a => [a] -> [a]
sort ([Var] -> [Var]) -> [Var] -> [Var]
forall a b. (a -> b) -> a -> b
$ (((Var, SKind), Val) -> Var) -> [((Var, SKind), Val)] -> [Var]
forall a b. (a -> b) -> [a] -> [b]
map ((Var, SKind) -> Var
forall a b. (a, b) -> a
fst ((Var, SKind) -> Var)
-> (((Var, SKind), Val) -> (Var, SKind))
-> ((Var, SKind), Val)
-> Var
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ((Var, SKind), Val) -> (Var, SKind)
forall a b. (a, b) -> a
fst) (Map (Var, SKind) Val -> [((Var, SKind), Val)]
forall k a. Map k a -> [(k, a)]
M.toList Map (Var, SKind) Val
envMap)))
                                                                      (ReaderT Env Symbolic Val -> ReaderT Env Symbolic Val)
-> ReaderT Env Symbolic Val -> ReaderT Env Symbolic Val
forall a b. (a -> b) -> a -> b
$ Bool -> Type -> Var -> ReaderT Env Symbolic Val
uninterpret Bool
False Type
t Var
v

        tgo Type
_ (App (Var Var
dataCon) (Lit (LitNumber LitNumType
LitNumInt Integer
i)))
           | Just DataCon
con <- Var -> Maybe DataCon
isDataConWorkId_maybe Var
dataCon, DataCon
con DataCon -> [DataCon] -> Bool
forall a. Eq a => a -> [a] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [DataCon
integerISDataCon, DataCon
integerIPDataCon, DataCon
integerINDataCon]
           = Val -> ReaderT Env Symbolic Val
forall a. a -> ReaderT Env Symbolic a
forall (m :: * -> *) a. Monad m => a -> m a
return (Val -> ReaderT Env Symbolic Val)
-> Val -> ReaderT Env Symbolic Val
forall a b. (a -> b) -> a -> b
$ SVal -> Val
Base (SVal -> Val) -> SVal -> Val
forall a b. (a -> b) -> a -> b
$ Kind -> Integer -> SVal
S.svInteger Kind
S.KUnbounded (DataCon -> Integer
v DataCon
con)
           where v :: DataCon -> Integer
v DataCon
con | DataCon
con DataCon -> DataCon -> Bool
forall a. Eq a => a -> a -> Bool
== DataCon
integerINDataCon = -Integer
i
                       | Bool
True                    = Integer
i

        -- Other literals
        tgo Type
t e :: CoreExpr
e@(Lit Literal
l) = do Env{machWordSize} <- ReaderT Env Symbolic Env
forall r (m :: * -> *). MonadReader r m => m r
ask
                             case l of
                               LitChar{}      -> ReaderT Env Symbolic Val
unint
                               LitString{}    -> ReaderT Env Symbolic Val
unint
                               LitNullAddr{}  -> ReaderT Env Symbolic Val
unint
                               LitRubbish{}   -> ReaderT Env Symbolic Val
unint
                               LitLabel{}     -> ReaderT Env Symbolic Val
unint
                               LitFloat    Rational
f  -> Val -> ReaderT Env Symbolic Val
forall a. a -> ReaderT Env Symbolic a
forall (m :: * -> *) a. Monad m => a -> m a
return (Val -> ReaderT Env Symbolic Val)
-> Val -> ReaderT Env Symbolic Val
forall a b. (a -> b) -> a -> b
$ SVal -> Val
Base (SVal -> Val) -> SVal -> Val
forall a b. (a -> b) -> a -> b
$ Float -> SVal
S.svFloat   (Rational -> Float
forall a. Fractional a => Rational -> a
fromRational Rational
f)
                               LitDouble   Rational
d  -> Val -> ReaderT Env Symbolic Val
forall a. a -> ReaderT Env Symbolic a
forall (m :: * -> *) a. Monad m => a -> m a
return (Val -> ReaderT Env Symbolic Val)
-> Val -> ReaderT Env Symbolic Val
forall a b. (a -> b) -> a -> b
$ SVal -> Val
Base (SVal -> Val) -> SVal -> Val
forall a b. (a -> b) -> a -> b
$ Double -> SVal
S.svDouble  (Rational -> Double
forall a. Fractional a => Rational -> a
fromRational Rational
d)
                               LitNumber LitNumType
lt Integer
i -> case LitNumType
lt of
                                                   LitNumType
LitNumBigNat  -> ReaderT Env Symbolic Val
unint
                                                   LitNumType
LitNumInt     -> Val -> ReaderT Env Symbolic Val
forall a. a -> ReaderT Env Symbolic a
forall (m :: * -> *) a. Monad m => a -> m a
return (Val -> ReaderT Env Symbolic Val)
-> Val -> ReaderT Env Symbolic Val
forall a b. (a -> b) -> a -> b
$ SVal -> Val
Base (SVal -> Val) -> SVal -> Val
forall a b. (a -> b) -> a -> b
$ Kind -> Integer -> SVal
S.svInteger (Bool -> Int -> Kind
S.KBounded Bool
True  Int
machWordSize) Integer
i
                                                   LitNumType
LitNumInt8    -> Val -> ReaderT Env Symbolic Val
forall a. a -> ReaderT Env Symbolic a
forall (m :: * -> *) a. Monad m => a -> m a
return (Val -> ReaderT Env Symbolic Val)
-> Val -> ReaderT Env Symbolic Val
forall a b. (a -> b) -> a -> b
$ SVal -> Val
Base (SVal -> Val) -> SVal -> Val
forall a b. (a -> b) -> a -> b
$ Kind -> Integer -> SVal
S.svInteger (Bool -> Int -> Kind
S.KBounded Bool
True  Int
8           ) Integer
i
                                                   LitNumType
LitNumInt16   -> Val -> ReaderT Env Symbolic Val
forall a. a -> ReaderT Env Symbolic a
forall (m :: * -> *) a. Monad m => a -> m a
return (Val -> ReaderT Env Symbolic Val)
-> Val -> ReaderT Env Symbolic Val
forall a b. (a -> b) -> a -> b
$ SVal -> Val
Base (SVal -> Val) -> SVal -> Val
forall a b. (a -> b) -> a -> b
$ Kind -> Integer -> SVal
S.svInteger (Bool -> Int -> Kind
S.KBounded Bool
True  Int
16          ) Integer
i
                                                   LitNumType
LitNumInt32   -> Val -> ReaderT Env Symbolic Val
forall a. a -> ReaderT Env Symbolic a
forall (m :: * -> *) a. Monad m => a -> m a
return (Val -> ReaderT Env Symbolic Val)
-> Val -> ReaderT Env Symbolic Val
forall a b. (a -> b) -> a -> b
$ SVal -> Val
Base (SVal -> Val) -> SVal -> Val
forall a b. (a -> b) -> a -> b
$ Kind -> Integer -> SVal
S.svInteger (Bool -> Int -> Kind
S.KBounded Bool
True  Int
32          ) Integer
i
                                                   LitNumType
LitNumInt64   -> Val -> ReaderT Env Symbolic Val
forall a. a -> ReaderT Env Symbolic a
forall (m :: * -> *) a. Monad m => a -> m a
return (Val -> ReaderT Env Symbolic Val)
-> Val -> ReaderT Env Symbolic Val
forall a b. (a -> b) -> a -> b
$ SVal -> Val
Base (SVal -> Val) -> SVal -> Val
forall a b. (a -> b) -> a -> b
$ Kind -> Integer -> SVal
S.svInteger (Bool -> Int -> Kind
S.KBounded Bool
True  Int
64          ) Integer
i
                                                   LitNumType
LitNumWord    -> Val -> ReaderT Env Symbolic Val
forall a. a -> ReaderT Env Symbolic a
forall (m :: * -> *) a. Monad m => a -> m a
return (Val -> ReaderT Env Symbolic Val)
-> Val -> ReaderT Env Symbolic Val
forall a b. (a -> b) -> a -> b
$ SVal -> Val
Base (SVal -> Val) -> SVal -> Val
forall a b. (a -> b) -> a -> b
$ Kind -> Integer -> SVal
S.svInteger (Bool -> Int -> Kind
S.KBounded Bool
False Int
machWordSize) Integer
i
                                                   LitNumType
LitNumWord8   -> Val -> ReaderT Env Symbolic Val
forall a. a -> ReaderT Env Symbolic a
forall (m :: * -> *) a. Monad m => a -> m a
return (Val -> ReaderT Env Symbolic Val)
-> Val -> ReaderT Env Symbolic Val
forall a b. (a -> b) -> a -> b
$ SVal -> Val
Base (SVal -> Val) -> SVal -> Val
forall a b. (a -> b) -> a -> b
$ Kind -> Integer -> SVal
S.svInteger (Bool -> Int -> Kind
S.KBounded Bool
False Int
8           ) Integer
i
                                                   LitNumType
LitNumWord16  -> Val -> ReaderT Env Symbolic Val
forall a. a -> ReaderT Env Symbolic a
forall (m :: * -> *) a. Monad m => a -> m a
return (Val -> ReaderT Env Symbolic Val)
-> Val -> ReaderT Env Symbolic Val
forall a b. (a -> b) -> a -> b
$ SVal -> Val
Base (SVal -> Val) -> SVal -> Val
forall a b. (a -> b) -> a -> b
$ Kind -> Integer -> SVal
S.svInteger (Bool -> Int -> Kind
S.KBounded Bool
False Int
16          ) Integer
i
                                                   LitNumType
LitNumWord32  -> Val -> ReaderT Env Symbolic Val
forall a. a -> ReaderT Env Symbolic a
forall (m :: * -> *) a. Monad m => a -> m a
return (Val -> ReaderT Env Symbolic Val)
-> Val -> ReaderT Env Symbolic Val
forall a b. (a -> b) -> a -> b
$ SVal -> Val
Base (SVal -> Val) -> SVal -> Val
forall a b. (a -> b) -> a -> b
$ Kind -> Integer -> SVal
S.svInteger (Bool -> Int -> Kind
S.KBounded Bool
False Int
32          ) Integer
i
                                                   LitNumType
LitNumWord64  -> Val -> ReaderT Env Symbolic Val
forall a. a -> ReaderT Env Symbolic a
forall (m :: * -> *) a. Monad m => a -> m a
return (Val -> ReaderT Env Symbolic Val)
-> Val -> ReaderT Env Symbolic Val
forall a b. (a -> b) -> a -> b
$ SVal -> Val
Base (SVal -> Val) -> SVal -> Val
forall a b. (a -> b) -> a -> b
$ Kind -> Integer -> SVal
S.svInteger (Bool -> Int -> Kind
S.KBounded Bool
False Int
64          ) Integer
i

                  where unint :: ReaderT Env Symbolic Val
unint = do Env{flags} <- ReaderT Env Symbolic Env
forall r (m :: * -> *). MonadReader r m => m r
ask
                                   k  <- getType noSrcSpan t
                                   nm <- mkValidName (showSDoc flags (ppr e))
                                   case k of
                                     KBase Kind
b -> Val -> ReaderT Env Symbolic Val
forall a. a -> ReaderT Env Symbolic a
forall (m :: * -> *) a. Monad m => a -> m a
return (Val -> ReaderT Env Symbolic Val)
-> Val -> ReaderT Env Symbolic Val
forall a b. (a -> b) -> a -> b
$ SVal -> Val
Base (SVal -> Val) -> SVal -> Val
forall a b. (a -> b) -> a -> b
$ Kind -> String -> UICodeKind -> [SVal] -> SVal
S.svUninterpreted Kind
b String
nm (Bool -> UICodeKind
S.UINone Bool
True) []
                                     SKind
_       -> String -> ReaderT Env Symbolic Val
forall a. HasCallStack => String -> a
error (String -> ReaderT Env Symbolic Val)
-> String -> ReaderT Env Symbolic Val
forall a b. (a -> b) -> a -> b
$ String
"Impossible: The type for literal resulted in non base kind: " String -> String -> String
forall a. [a] -> [a] -> [a]
++ (CoreExpr, SKind) -> String
forall {a}. Outputable a => a -> String
sh (CoreExpr
e, SKind
k)

        tgo Type
tFun orig :: CoreExpr
orig@App{} = do
             reduced <- CoreExpr -> Eval CoreExpr
betaReduce CoreExpr
orig

             Env{specials} <- ask

             -- handle specials: Equality, tuples, and lists
             let getVar (Var Var
v)    = Var -> Maybe Var
forall a. a -> Maybe a
Just Var
v
                 getVar (Tick CoreTickish
_ Expr b
e) = Expr b -> Maybe Var
getVar Expr b
e
                 getVar Expr b
_          = Maybe Var
forall a. Maybe a
Nothing

                 isEq (App (App CoreExpr
ev (Type Type
_)) CoreExpr
dict) | Just Var
v <- CoreExpr -> Maybe Var
forall {b}. Expr b -> Maybe Var
getVar CoreExpr
ev, CoreExpr -> Bool
isReallyADictionary CoreExpr
dict, Just Val
f <- Specials -> Var -> Maybe Val
isEquality Specials
specials Var
v = Val -> Maybe Val
forall a. a -> Maybe a
Just Val
f
                 isEq CoreExpr
_                                                                                                             = Maybe Val
forall a. Maybe a
Nothing

                 isTup (Var Var
v)          = Specials -> Var -> Maybe Val
isTuple Specials
specials Var
v
                 isTup (App Expr b
f (Type Type
_)) = Expr b -> Maybe Val
isTup Expr b
f
                 isTup (Tick CoreTickish
_ Expr b
e)       = Expr b -> Maybe Val
isTup Expr b
e
                 isTup Expr b
_                = Maybe Val
forall a. Maybe a
Nothing

                 isLst (Var Var
v)          = Specials -> Var -> Maybe Val
isList Specials
specials Var
v
                 isLst (App Expr b
f (Type Type
_)) = Expr b -> Maybe Val
isLst Expr b
f
                 isLst (Tick CoreTickish
_ Expr b
e)       = Expr b -> Maybe Val
isLst Expr b
e
                 isLst Expr b
_                = Maybe Val
forall a. Maybe a
Nothing

                 isSpecial CoreExpr
e = CoreExpr -> Maybe Val
isEq CoreExpr
e Maybe Val -> Maybe Val -> Maybe Val
forall a. Maybe a -> Maybe a -> Maybe a
forall (m :: * -> *) a. MonadPlus m => m a -> m a -> m a
`mplus` CoreExpr -> Maybe Val
forall {b}. Expr b -> Maybe Val
isTup CoreExpr
e Maybe Val -> Maybe Val -> Maybe Val
forall a. Maybe a -> Maybe a -> Maybe a
forall (m :: * -> *) a. MonadPlus m => m a -> m a -> m a
`mplus` CoreExpr -> Maybe Val
forall {b}. Expr b -> Maybe Val
isLst CoreExpr
e

             case isSpecial reduced of
               Just Val
f  -> String -> ReaderT Env Symbolic Val -> ReaderT Env Symbolic Val
forall a. String -> a -> a
debugTrace (String
"Special located: " String -> String -> String
forall a. [a] -> [a] -> [a]
++ (CoreExpr, Val) -> String
forall {a}. Outputable a => a -> String
sh (CoreExpr
orig, Val
f)) (ReaderT Env Symbolic Val -> ReaderT Env Symbolic Val)
-> ReaderT Env Symbolic Val -> ReaderT Env Symbolic Val
forall a b. (a -> b) -> a -> b
$ Val -> ReaderT Env Symbolic Val
forall a. a -> ReaderT Env Symbolic a
forall (m :: * -> *) a. Monad m => a -> m a
return Val
f
               Maybe Val
Nothing -> case CoreExpr
reduced of

                            -- special case for exponentiation; there must be a better way to do this
                            App (App (App (App (Var Var
v) (Type Type
t1)) (Type Type
t2)) CoreExpr
dict1) CoreExpr
dict2 | CoreExpr -> Bool
isReallyADictionary CoreExpr
dict1 Bool -> Bool -> Bool
&& CoreExpr -> Bool
isReallyADictionary CoreExpr
dict2 -> do
                                Env{envMap} <- ReaderT Env Symbolic Env
forall r (m :: * -> *). MonadReader r m => m r
ask
                                let vSpan = Var -> SrcSpan
forall a. NamedThing a => a -> SrcSpan
getSrcSpan Var
v
                                k1 <- getType vSpan t1
                                k2 <- getType vSpan t2
                                let kExp  = SKind -> SKind -> SKind
KFun SKind
k1 (SKind -> SKind -> SKind
KFun SKind
k1 SKind
k2)
                                case (v, kExp) `M.lookup` envMap of
                                  Just Val
b -> String -> ReaderT Env Symbolic Val -> ReaderT Env Symbolic Val
forall a. String -> a -> a
debugTrace (String
"Located exp(^): " String -> String -> String
forall a. [a] -> [a] -> [a]
++ (CoreExpr, SKind) -> String
forall {a}. Outputable a => a -> String
sh (CoreExpr
reduced, SKind
kExp)) (ReaderT Env Symbolic Val -> ReaderT Env Symbolic Val)
-> ReaderT Env Symbolic Val -> ReaderT Env Symbolic Val
forall a b. (a -> b) -> a -> b
$ Val -> ReaderT Env Symbolic Val
forall a. a -> ReaderT Env Symbolic a
forall (m :: * -> *) a. Monad m => a -> m a
return Val
b
                                  Maybe Val
_      -> do Env{coreMap} <- ReaderT Env Symbolic Env
forall r (m :: * -> *). MonadReader r m => m r
ask
                                               case v `M.lookup` coreMap of
                                                 Just (SrcSpan
l, CoreExpr
e) -> (Env -> Env)
-> ReaderT Env Symbolic Val -> ReaderT Env Symbolic Val
forall a.
(Env -> Env) -> ReaderT Env Symbolic a -> ReaderT Env Symbolic a
forall r (m :: * -> *) a. MonadReader r m => (r -> r) -> m a -> m a
local (\Env
env -> Env
env{curLoc = l : curLoc env}) (ReaderT Env Symbolic Val -> ReaderT Env Symbolic Val)
-> ReaderT Env Symbolic Val -> ReaderT Env Symbolic Val
forall a b. (a -> b) -> a -> b
$ Type -> CoreExpr -> ReaderT Env Symbolic Val
tgo Type
tFun (CoreExpr -> CoreExpr -> CoreExpr
forall b. Expr b -> Expr b -> Expr b
App (CoreExpr -> CoreExpr -> CoreExpr
forall b. Expr b -> Expr b -> Expr b
App (CoreExpr -> CoreExpr -> CoreExpr
forall b. Expr b -> Expr b -> Expr b
App (CoreExpr -> CoreExpr -> CoreExpr
forall b. Expr b -> Expr b -> Expr b
App CoreExpr
e (Type -> CoreExpr
forall b. Type -> Expr b
Type Type
t1)) (Type -> CoreExpr
forall b. Type -> Expr b
Type Type
t2)) CoreExpr
dict1) CoreExpr
dict2)
                                                 Maybe (SrcSpan, CoreExpr)
Nothing     -> Type -> CoreExpr -> ReaderT Env Symbolic Val
tgo Type
tFun (Var -> CoreExpr
forall b. Var -> Expr b
Var Var
v)

                            -- special case for split and join; there must be a better way to do this
                            App (App (App (Var Var
v) (Type Type
t1)) (Type Type
t2)) CoreExpr
dict | CoreExpr -> Bool
isReallyADictionary CoreExpr
dict -> do
                                Env{envMap} <- ReaderT Env Symbolic Env
forall r (m :: * -> *). MonadReader r m => m r
ask
                                let vSpan = Var -> SrcSpan
forall a. NamedThing a => a -> SrcSpan
getSrcSpan Var
v
                                k1 <- getType vSpan t1
                                k2 <- getType vSpan t2
                                let kSplit = SKind -> SKind -> SKind
KFun SKind
k1 ([SKind] -> SKind
KTup [SKind
k2, SKind
k2])
                                    kJoin  = SKind -> SKind -> SKind
KFun SKind
k1 (SKind -> SKind -> SKind
KFun SKind
k1 SKind
k2)
                                case ((v, kSplit) `M.lookup` envMap, (v, kJoin) `M.lookup` envMap)  of
                                  (Just Val
b, Maybe Val
_) -> String -> ReaderT Env Symbolic Val -> ReaderT Env Symbolic Val
forall a. String -> a -> a
debugTrace (String
"Located split: " String -> String -> String
forall a. [a] -> [a] -> [a]
++ (CoreExpr, SKind) -> String
forall {a}. Outputable a => a -> String
sh (CoreExpr
reduced, SKind
kSplit)) (ReaderT Env Symbolic Val -> ReaderT Env Symbolic Val)
-> ReaderT Env Symbolic Val -> ReaderT Env Symbolic Val
forall a b. (a -> b) -> a -> b
$ Val -> ReaderT Env Symbolic Val
forall a. a -> ReaderT Env Symbolic a
forall (m :: * -> *) a. Monad m => a -> m a
return Val
b
                                  (Maybe Val
_, Just Val
b) -> String -> ReaderT Env Symbolic Val -> ReaderT Env Symbolic Val
forall a. String -> a -> a
debugTrace (String
"Located join: "  String -> String -> String
forall a. [a] -> [a] -> [a]
++ (CoreExpr, SKind) -> String
forall {a}. Outputable a => a -> String
sh (CoreExpr
reduced, SKind
kJoin))  (ReaderT Env Symbolic Val -> ReaderT Env Symbolic Val)
-> ReaderT Env Symbolic Val -> ReaderT Env Symbolic Val
forall a b. (a -> b) -> a -> b
$ Val -> ReaderT Env Symbolic Val
forall a. a -> ReaderT Env Symbolic a
forall (m :: * -> *) a. Monad m => a -> m a
return Val
b
                                  (Maybe Val, Maybe Val)
_           -> do Env{coreMap} <- ReaderT Env Symbolic Env
forall r (m :: * -> *). MonadReader r m => m r
ask
                                                    case v `M.lookup` coreMap of
                                                      Just (SrcSpan
l, CoreExpr
e) -> (Env -> Env)
-> ReaderT Env Symbolic Val -> ReaderT Env Symbolic Val
forall a.
(Env -> Env) -> ReaderT Env Symbolic a -> ReaderT Env Symbolic a
forall r (m :: * -> *) a. MonadReader r m => (r -> r) -> m a -> m a
local (\Env
env -> Env
env{curLoc = l : curLoc env}) (ReaderT Env Symbolic Val -> ReaderT Env Symbolic Val)
-> ReaderT Env Symbolic Val -> ReaderT Env Symbolic Val
forall a b. (a -> b) -> a -> b
$ Type -> CoreExpr -> ReaderT Env Symbolic Val
tgo Type
tFun (CoreExpr -> CoreExpr -> CoreExpr
forall b. Expr b -> Expr b -> Expr b
App (CoreExpr -> CoreExpr -> CoreExpr
forall b. Expr b -> Expr b -> Expr b
App (CoreExpr -> CoreExpr -> CoreExpr
forall b. Expr b -> Expr b -> Expr b
App CoreExpr
e (Type -> CoreExpr
forall b. Type -> Expr b
Type Type
t1)) (Type -> CoreExpr
forall b. Type -> Expr b
Type Type
t2)) CoreExpr
dict)
                                                      Maybe (SrcSpan, CoreExpr)
Nothing     -> Type -> CoreExpr -> ReaderT Env Symbolic Val
tgo Type
tFun (Var -> CoreExpr
forall b. Var -> Expr b
Var Var
v)

                            App (App (Var Var
v) (Type Type
t)) CoreExpr
dict | CoreExpr -> Bool
isReallyADictionary CoreExpr
dict -> do
                                Env{envMap} <- ReaderT Env Symbolic Env
forall r (m :: * -> *). MonadReader r m => m r
ask
                                k <- getType (getSrcSpan v) t
                                case (v, k) `M.lookup` envMap of
                                  Just Val
b  -> Val -> ReaderT Env Symbolic Val
forall a. a -> ReaderT Env Symbolic a
forall (m :: * -> *) a. Monad m => a -> m a
return Val
b
                                  Maybe Val
Nothing -> do Env{coreMap} <- ReaderT Env Symbolic Env
forall r (m :: * -> *). MonadReader r m => m r
ask
                                                case v `M.lookup` coreMap of
                                                  Just (SrcSpan
l, CoreExpr
e) -> (Env -> Env)
-> ReaderT Env Symbolic Val -> ReaderT Env Symbolic Val
forall a.
(Env -> Env) -> ReaderT Env Symbolic a -> ReaderT Env Symbolic a
forall r (m :: * -> *) a. MonadReader r m => (r -> r) -> m a -> m a
local (\Env
env -> Env
env{curLoc = l : curLoc env}) (ReaderT Env Symbolic Val -> ReaderT Env Symbolic Val)
-> ReaderT Env Symbolic Val -> ReaderT Env Symbolic Val
forall a b. (a -> b) -> a -> b
$ Type -> CoreExpr -> ReaderT Env Symbolic Val
tgo Type
tFun (CoreExpr -> CoreExpr -> CoreExpr
forall b. Expr b -> Expr b -> Expr b
App (CoreExpr -> CoreExpr -> CoreExpr
forall b. Expr b -> Expr b -> Expr b
App CoreExpr
e (Type -> CoreExpr
forall b. Type -> Expr b
Type Type
t)) CoreExpr
dict)
                                                  Maybe (SrcSpan, CoreExpr)
Nothing     -> Type -> CoreExpr -> ReaderT Env Symbolic Val
tgo Type
tFun (Var -> CoreExpr
forall b. Var -> Expr b
Var Var
v)

                            App (Var Var
v) (Type Type
t) -> do
                                Env{coreMap} <- ReaderT Env Symbolic Env
forall r (m :: * -> *). MonadReader r m => m r
ask
                                case v `M.lookup` coreMap of
                                  Just (SrcSpan
l, CoreExpr
e) -> (Env -> Env)
-> ReaderT Env Symbolic Val -> ReaderT Env Symbolic Val
forall a.
(Env -> Env) -> ReaderT Env Symbolic a -> ReaderT Env Symbolic a
forall r (m :: * -> *) a. MonadReader r m => (r -> r) -> m a -> m a
local (\Env
env -> Env
env{curLoc = l : curLoc env}) (ReaderT Env Symbolic Val -> ReaderT Env Symbolic Val)
-> ReaderT Env Symbolic Val -> ReaderT Env Symbolic Val
forall a b. (a -> b) -> a -> b
$ Type -> CoreExpr -> ReaderT Env Symbolic Val
tgo Type
tFun (CoreExpr -> CoreExpr -> CoreExpr
forall b. Expr b -> Expr b -> Expr b
App CoreExpr
e (Type -> CoreExpr
forall b. Type -> Expr b
Type Type
t))
                                  Maybe (SrcSpan, CoreExpr)
Nothing     -> Type -> CoreExpr -> ReaderT Env Symbolic Val
tgo Type
tFun (Var -> CoreExpr
forall b. Var -> Expr b
Var Var
v)

                            App (Let (Rec [(Var, CoreExpr)]
bs) CoreExpr
f) CoreExpr
a -> CoreExpr -> ReaderT Env Symbolic Val
go (CoreBind -> CoreExpr -> CoreExpr
forall b. Bind b -> Expr b -> Expr b
Let ([(Var, CoreExpr)] -> CoreBind
forall b. [(b, Expr b)] -> Bind b
Rec [(Var, CoreExpr)]
bs) (CoreExpr -> CoreExpr -> CoreExpr
forall b. Expr b -> Expr b -> Expr b
App CoreExpr
f CoreExpr
a))

                            App CoreExpr
f CoreExpr
e  -> do
                                func <- CoreExpr -> ReaderT Env Symbolic Val
go CoreExpr
f
                                arg  <- go e
                                case (func, arg) of
                                   (Func Maybe String
_ Val -> ReaderT Env Symbolic Val
sf, Val
sv) -> Val -> ReaderT Env Symbolic Val
sf Val
sv
                                   (Val, Val)
_               -> String -> ReaderT Env Symbolic Val
forall a. HasCallStack => String -> a
error (String -> ReaderT Env Symbolic Val)
-> String -> ReaderT Env Symbolic Val
forall a b. (a -> b) -> a -> b
$ String
"[SBV] Impossible happened. Got an application with mismatched types: " String -> String -> String
forall a. [a] -> [a] -> [a]
++ [(CoreExpr, Val)] -> String
forall {a}. Outputable a => a -> String
sh [(CoreExpr
f, Val
func), (CoreExpr
e, Val
arg)]

                            CoreExpr
e   -> CoreExpr -> ReaderT Env Symbolic Val
go CoreExpr
e

        tgo Type
_ (Lam Var
b CoreExpr
body) = do
                k <- SrcSpan -> Type -> Eval SKind
getType (Var -> SrcSpan
forall a. NamedThing a => a -> SrcSpan
getSrcSpan Var
b) (Var -> Type
varType Var
b)
                Env{envMap} <- ask
                return $ Func (Just (sh b)) $ \Val
s -> (Env -> Env)
-> ReaderT Env Symbolic Val -> ReaderT Env Symbolic Val
forall a.
(Env -> Env) -> ReaderT Env Symbolic a -> ReaderT Env Symbolic a
forall r (m :: * -> *) a. MonadReader r m => (r -> r) -> m a -> m a
local (\Env
env -> Env
env{envMap = M.insert (b, k) s envMap}) (CoreExpr -> ReaderT Env Symbolic Val
go CoreExpr
body)

        tgo Type
_ (Let (NonRec Var
b CoreExpr
e) CoreExpr
body) = (Env -> Env)
-> ReaderT Env Symbolic Val -> ReaderT Env Symbolic Val
forall a.
(Env -> Env) -> ReaderT Env Symbolic a -> ReaderT Env Symbolic a
forall r (m :: * -> *) a. MonadReader r m => (r -> r) -> m a -> m a
local (\Env
env -> Env
env{coreMap = M.insert b (varSpan b, e) (coreMap env)}) (CoreExpr -> ReaderT Env Symbolic Val
go CoreExpr
body)

        tgo Type
_ (Let (Rec [(Var, CoreExpr)]
bs) CoreExpr
body) = (Env -> Env)
-> ReaderT Env Symbolic Val -> ReaderT Env Symbolic Val
forall a.
(Env -> Env) -> ReaderT Env Symbolic a -> ReaderT Env Symbolic a
forall r (m :: * -> *) a. MonadReader r m => (r -> r) -> m a -> m a
local (\Env
env -> Env
env{coreMap = foldr (\(Var
b, CoreExpr
e) Map Var (SrcSpan, CoreExpr)
m -> Var
-> (SrcSpan, CoreExpr)
-> Map Var (SrcSpan, CoreExpr)
-> Map Var (SrcSpan, CoreExpr)
forall k a. Ord k => k -> a -> Map k a -> Map k a
M.insert Var
b (Var -> SrcSpan
varSpan Var
b, CoreExpr
e) Map Var (SrcSpan, CoreExpr)
m) (coreMap env) bs}) (CoreExpr -> ReaderT Env Symbolic Val
go CoreExpr
body)

        -- Case expressions. We take advantage of the core-invariant that each case alternative
        -- is exhaustive; and DEFAULT (if present) is the first alternative. We turn it into a
        -- simple if-then-else chain with the last element on the DEFAULT, or whatever comes last.
        tgo Type
_ e :: CoreExpr
e@(Case CoreExpr
ce Var
cBinder Type
caseType [Alt Var]
alts)
           = do sce <- CoreExpr -> ReaderT Env Symbolic Val
go CoreExpr
ce
                let caseTooComplicated String
w [] = String -> [String] -> ReaderT Env Symbolic Val
tbd (String
"Unsupported case-expression (" String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
w String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
")") [CoreExpr -> String
forall {a}. Outputable a => a -> String
sh CoreExpr
e]
                    caseTooComplicated String
w [String]
xs = String -> [String] -> ReaderT Env Symbolic Val
tbd (String
"Unsupported case-expression (" String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
w String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
")") ([String] -> ReaderT Env Symbolic Val)
-> [String] -> ReaderT Env Symbolic Val
forall a b. (a -> b) -> a -> b
$ [CoreExpr -> String
forall {a}. Outputable a => a -> String
sh CoreExpr
e, String
"While Analyzing:"] [String] -> [String] -> [String]
forall a. [a] -> [a] -> [a]
++ [String]
xs

                    isDefault (Alt AltCon
DEFAULT [b]
_ Expr b
_) = Bool
True
                    isDefault Alt b
_                 = Bool
False

                    (defs, nonDefs)           = partition isDefault alts

                    walk []                    = String -> [String] -> ReaderT Env Symbolic Val
caseTooComplicated String
"with-non-exhaustive-match" []  -- can't really happen
                    walk (Alt AltCon
p [Var]
bs CoreExpr
rhs : [Alt Var]
rest) =
                         do -- try to get a "good" location for this alternative, if possible:
                            let eLoc :: SrcSpan
eLoc = case (CoreExpr
rhs, [Var]
bs) of
                                        (Tick CoreTickish
t CoreExpr
_, [Var]
_  ) -> CoreTickish -> SrcSpan
forall (t :: TickishPass). GenTickish t -> SrcSpan
tickSpan CoreTickish
t
                                        (Var Var
v,    [Var]
_  ) -> Var -> SrcSpan
varSpan Var
v
                                        (CoreExpr
_,        Var
b:[Var]
_) -> Var -> SrcSpan
varSpan Var
b
                                        (CoreExpr, [Var])
_               -> Var -> SrcSpan
varSpan Var
cBinder
                            mr <- SrcSpan
-> Val
-> AltCon
-> [Var]
-> Eval (Maybe (SVal, [((Var, SKind), Val)]))
match SrcSpan
eLoc Val
sce AltCon
p [Var]
bs
                            case mr of
                              Just (SVal
m, [((Var, SKind), Val)]
bs') -> do let result :: ReaderT Env Symbolic Val
result = (Env -> Env)
-> ReaderT Env Symbolic Val -> ReaderT Env Symbolic Val
forall a.
(Env -> Env) -> ReaderT Env Symbolic a -> ReaderT Env Symbolic a
forall r (m :: * -> *) a. MonadReader r m => (r -> r) -> m a -> m a
local (\Env
env -> Env
env{curLoc = eLoc : curLoc env, envMap = foldr (uncurry M.insert) (envMap env) bs'}) (ReaderT Env Symbolic Val -> ReaderT Env Symbolic Val)
-> ReaderT Env Symbolic Val -> ReaderT Env Symbolic Val
forall a b. (a -> b) -> a -> b
$ CoreExpr -> ReaderT Env Symbolic Val
go CoreExpr
rhs
                                                  if [Alt Var] -> Bool
forall a. [a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [Alt Var]
rest
                                                     then ReaderT Env Symbolic Val
result
                                                     else ([String] -> ReaderT Env Symbolic Val)
-> SVal
-> ReaderT Env Symbolic Val
-> ReaderT Env Symbolic Val
-> ReaderT Env Symbolic Val
choose (String -> [String] -> ReaderT Env Symbolic Val
caseTooComplicated String
"with-complicated-alternatives-during-merging") SVal
m ReaderT Env Symbolic Val
result ([Alt Var] -> ReaderT Env Symbolic Val
walk [Alt Var]
rest)
                              Maybe (SVal, [((Var, SKind), Val)])
Nothing       -> String -> [String] -> ReaderT Env Symbolic Val
caseTooComplicated String
"with-complicated-match" [String
"MATCH " String -> String -> String
forall a. [a] -> [a] -> [a]
++ (CoreExpr, AltCon) -> String
forall {a}. Outputable a => a -> String
sh (CoreExpr
ce, AltCon
p), String
" --> " String -> String -> String
forall a. [a] -> [a] -> [a]
++ CoreExpr -> String
forall {a}. Outputable a => a -> String
sh CoreExpr
rhs]

                k <- getType (getSrcSpan cBinder) caseType
                local (\Env
env -> Env
env{envMap = M.insert (cBinder, k) sce (envMap env)}) $ walk (nonDefs ++ defs)

           where choose :: ([String] -> ReaderT Env Symbolic Val)
-> SVal
-> ReaderT Env Symbolic Val
-> ReaderT Env Symbolic Val
-> ReaderT Env Symbolic Val
choose [String] -> ReaderT Env Symbolic Val
bailOut SVal
t ReaderT Env Symbolic Val
tb ReaderT Env Symbolic Val
fb = case SVal -> Maybe Bool
S.svAsBool SVal
t of
                                            Maybe Bool
Nothing    -> do stb <- ReaderT Env Symbolic Val
tb
                                                             sfb <- fb
                                                             iteVal bailOut t stb sfb
                                            Just Bool
True  -> ReaderT Env Symbolic Val
tb
                                            Just Bool
False -> ReaderT Env Symbolic Val
fb
                 match :: SrcSpan -> Val -> AltCon -> [Var] -> Eval (Maybe (S.SVal, [((Var, SKind), Val)]))
                 match :: SrcSpan
-> Val
-> AltCon
-> [Var]
-> Eval (Maybe (SVal, [((Var, SKind), Val)]))
match SrcSpan
sp Val
a AltCon
c [Var]
bs = case AltCon
c of
                                     AltCon
DEFAULT    -> Maybe (SVal, [((Var, SKind), Val)])
-> Eval (Maybe (SVal, [((Var, SKind), Val)]))
forall a. a -> ReaderT Env Symbolic a
forall (m :: * -> *) a. Monad m => a -> m a
return (Maybe (SVal, [((Var, SKind), Val)])
 -> Eval (Maybe (SVal, [((Var, SKind), Val)])))
-> Maybe (SVal, [((Var, SKind), Val)])
-> Eval (Maybe (SVal, [((Var, SKind), Val)]))
forall a b. (a -> b) -> a -> b
$ (SVal, [((Var, SKind), Val)])
-> Maybe (SVal, [((Var, SKind), Val)])
forall a. a -> Maybe a
Just (SVal
S.svTrue, [])
                                     LitAlt  Literal
l  -> do b <- CoreExpr -> ReaderT Env Symbolic Val
go (Literal -> CoreExpr
forall b. Literal -> Expr b
Lit Literal
l)
                                                      return $ Just (a `eqVal` b, [])
                                     DataAlt DataCon
dc -> do Env{envMap, destMap} <- ReaderT Env Symbolic Env
forall r (m :: * -> *). MonadReader r m => m r
ask
                                                      k <- getType sp (dataConRepType dc)
                                                      let wid = DataCon -> Var
dataConWorkId DataCon
dc
                                                      -- The following lookup in env essentially gets True/False constructors (or other base-values if we add them)
                                                      case (wid, k) `M.lookup` envMap of
                                                        Just (Base SVal
b) -> Maybe (SVal, [((Var, SKind), Val)])
-> Eval (Maybe (SVal, [((Var, SKind), Val)]))
forall a. a -> ReaderT Env Symbolic a
forall (m :: * -> *) a. Monad m => a -> m a
return (Maybe (SVal, [((Var, SKind), Val)])
 -> Eval (Maybe (SVal, [((Var, SKind), Val)])))
-> Maybe (SVal, [((Var, SKind), Val)])
-> Eval (Maybe (SVal, [((Var, SKind), Val)]))
forall a b. (a -> b) -> a -> b
$ (SVal, [((Var, SKind), Val)])
-> Maybe (SVal, [((Var, SKind), Val)])
forall a. a -> Maybe a
Just (Val
a Val -> Val -> SVal
`eqVal` SVal -> Val
Base SVal
b, [])
                                                        Maybe Val
_             -> case Var
wid Var
-> Map Var (Val -> [(Var, SKind)] -> (SVal, [((Var, SKind), Val)]))
-> Maybe (Val -> [(Var, SKind)] -> (SVal, [((Var, SKind), Val)]))
forall k a. Ord k => k -> Map k a -> Maybe a
`M.lookup` Map Var (Val -> [(Var, SKind)] -> (SVal, [((Var, SKind), Val)]))
destMap of
                                                                           Maybe (Val -> [(Var, SKind)] -> (SVal, [((Var, SKind), Val)]))
Nothing -> Maybe (SVal, [((Var, SKind), Val)])
-> Eval (Maybe (SVal, [((Var, SKind), Val)]))
forall a. a -> ReaderT Env Symbolic a
forall (m :: * -> *) a. Monad m => a -> m a
return Maybe (SVal, [((Var, SKind), Val)])
forall a. Maybe a
Nothing
                                                                           Just Val -> [(Var, SKind)] -> (SVal, [((Var, SKind), Val)])
f  -> do bts <- (Var -> ReaderT Env Symbolic (Var, SKind))
-> [Var] -> ReaderT Env Symbolic [(Var, SKind)]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [b]
mapM (\Var
b -> SrcSpan -> Type -> Eval SKind
getType (Var -> SrcSpan
forall a. NamedThing a => a -> SrcSpan
getSrcSpan Var
b) (Var -> Type
varType Var
b) Eval SKind
-> (SKind -> ReaderT Env Symbolic (Var, SKind))
-> ReaderT Env Symbolic (Var, SKind)
forall a b.
ReaderT Env Symbolic a
-> (a -> ReaderT Env Symbolic b) -> ReaderT Env Symbolic b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \SKind
bt -> (Var, SKind) -> ReaderT Env Symbolic (Var, SKind)
forall a. a -> ReaderT Env Symbolic a
forall (m :: * -> *) a. Monad m => a -> m a
return (Var
b, SKind
bt)) [Var]
bs
                                                                                         return $ Just (f a bts)

        tgo Type
t (Cast CoreExpr
e CoercionR
c)
           = String -> ReaderT Env Symbolic Val -> ReaderT Env Symbolic Val
forall a. String -> a -> a
debugTrace (String
"Going thru a Cast: " String -> String -> String
forall a. [a] -> [a] -> [a]
++ CoercionR -> String
forall {a}. Outputable a => a -> String
sh CoercionR
c) (ReaderT Env Symbolic Val -> ReaderT Env Symbolic Val)
-> ReaderT Env Symbolic Val -> ReaderT Env Symbolic Val
forall a b. (a -> b) -> a -> b
$ Type -> CoreExpr -> ReaderT Env Symbolic Val
tgo Type
t CoreExpr
e

        tgo Type
_ (Tick CoreTickish
t CoreExpr
e) = (Env -> Env)
-> ReaderT Env Symbolic Val -> ReaderT Env Symbolic Val
forall a.
(Env -> Env) -> ReaderT Env Symbolic a -> ReaderT Env Symbolic a
forall r (m :: * -> *) a. MonadReader r m => (r -> r) -> m a -> m a
local (\Env
envMap -> Env
envMap{curLoc = tickSpan t : curLoc envMap}) (ReaderT Env Symbolic Val -> ReaderT Env Symbolic Val)
-> ReaderT Env Symbolic Val -> ReaderT Env Symbolic Val
forall a b. (a -> b) -> a -> b
$ CoreExpr -> ReaderT Env Symbolic Val
go CoreExpr
e

        tgo Type
_ (Type Type
t)
           = do Env{curLoc} <- ReaderT Env Symbolic Env
forall r (m :: * -> *). MonadReader r m => m r
ask
                k <- getType (pickSpan curLoc) t
                return (Typ k)

        tgo Type
_ e :: CoreExpr
e@Coercion{}
           = String -> [String] -> ReaderT Env Symbolic Val
tbd String
"Unsupported coercion-expression" [CoreExpr -> String
forall {a}. Outputable a => a -> String
sh CoreExpr
e]

        isBetaReducable :: CoreExpr -> Bool
isBetaReducable (Type Type
_) = Bool
True
        isBetaReducable CoreExpr
e        = CoreExpr -> Bool
isReallyADictionary CoreExpr
e

        betaReduce :: CoreExpr -> Eval CoreExpr
        betaReduce :: CoreExpr -> Eval CoreExpr
betaReduce orig :: CoreExpr
orig@(App CoreExpr
f CoreExpr
a) = do
                rf <- CoreExpr -> Eval CoreExpr
betaReduce CoreExpr
f
                if not (isBetaReducable a)
                   then return (App rf a)
                   else do let chaseVars :: CoreExpr -> Eval CoreExpr
                               chaseVars (Var Var
x)    = do Env{coreMap} <- ReaderT Env Symbolic Env
forall r (m :: * -> *). MonadReader r m => m r
ask
                                                         case x `M.lookup` coreMap of
                                                           Maybe (SrcSpan, CoreExpr)
Nothing     -> CoreExpr -> Eval CoreExpr
forall a. a -> ReaderT Env Symbolic a
forall (m :: * -> *) a. Monad m => a -> m a
return (Var -> CoreExpr
forall b. Var -> Expr b
Var Var
x)
                                                           Just (SrcSpan
_, CoreExpr
b) -> CoreExpr -> Eval CoreExpr
chaseVars CoreExpr
b
                               chaseVars (Tick CoreTickish
_ CoreExpr
x) = CoreExpr -> Eval CoreExpr
chaseVars CoreExpr
x
                               chaseVars CoreExpr
x          = CoreExpr -> Eval CoreExpr
forall a. a -> ReaderT Env Symbolic a
forall (m :: * -> *) a. Monad m => a -> m a
return CoreExpr
x
                           func <- chaseVars rf
                           case func of
                             Lam Var
x CoreExpr
b -> do reduced <- CoreExpr -> Eval CoreExpr
betaReduce (CoreExpr -> Eval CoreExpr) -> CoreExpr -> Eval CoreExpr
forall a b. (a -> b) -> a -> b
$ HasDebugCallStack => Subst -> CoreExpr -> CoreExpr
Subst -> CoreExpr -> CoreExpr
substExpr (Subst -> [(Var, CoreExpr)] -> Subst
extendSubstList Subst
emptySubst [(Var
x, CoreExpr
a)]) CoreExpr
b
                                           () <- debugTrace ("Beta reduce:\n" ++ sh (orig, reduced)) $ return ()
                                           return reduced
                             CoreExpr
_       -> CoreExpr -> Eval CoreExpr
forall a. a -> ReaderT Env Symbolic a
forall (m :: * -> *) a. Monad m => a -> m a
return (CoreExpr -> CoreExpr -> CoreExpr
forall b. Expr b -> Expr b -> Expr b
App CoreExpr
rf CoreExpr
a)
        betaReduce CoreExpr
e = CoreExpr -> Eval CoreExpr
forall a. a -> ReaderT Env Symbolic a
forall (m :: * -> *) a. Monad m => a -> m a
return CoreExpr
e

-- | Is this really a dictionary in disguise? This is a terrible hack, and the ice is thin here. But it seems to work.
-- TODO: Figure out if there's a better way of doing this. Note that this function really does get applications, when
-- those dictionaries are parameterized by others. Think of the case where "Eq [a]" dictionary depends on "Eq a", for
-- instance. In these cases, GHC to produces applications.
isReallyADictionary :: CoreExpr -> Bool
isReallyADictionary :: CoreExpr -> Bool
isReallyADictionary (App CoreExpr
f CoreExpr
_) = CoreExpr -> Bool
isReallyADictionary CoreExpr
f
isReallyADictionary (Var Var
v)   = String
"$" String -> String -> Bool
forall a. Eq a => [a] -> [a] -> Bool
`isPrefixOf` FastString -> String
unpackFS (OccName -> FastString
occNameFS (Name -> OccName
forall name. HasOccName name => name -> OccName
occName (Var -> Name
varName Var
v)))
isReallyADictionary CoreExpr
_         = Bool
False

-- Create a symbolic variable.
mkSym :: Config -> Maybe Var -> Maybe Type -> SKind -> Maybe String -> Eval Val
mkSym :: Config
-> Maybe Var
-> Maybe Type
-> SKind
-> Maybe String
-> ReaderT Env Symbolic Val
mkSym Config{Env
cfgEnv :: Config -> Env
cfgEnv :: Env
cfgEnv} Maybe Var
mbBind Maybe Type
mbBType = SKind -> Maybe String -> ReaderT Env Symbolic Val
sym
 where sh :: a -> String
sh a
o = DynFlags -> SDoc -> String
showSDoc (Env -> DynFlags
flags Env
cfgEnv) (a -> SDoc
forall a. Outputable a => a -> SDoc
ppr a
o)

       tinfo :: a -> String
tinfo a
k = case Maybe Type
mbBType of
                   Maybe Type
Nothing -> String
"Kind: " String -> String -> String
forall a. [a] -> [a] -> [a]
++ a -> String
forall {a}. Outputable a => a -> String
sh a
k
                   Just Type
t  -> String
"Type: " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Type -> String
forall {a}. Outputable a => a -> String
sh Type
t

       sym :: SKind -> Maybe String -> ReaderT Env Symbolic Val
sym (KBase Kind
k) Maybe String
nm  = do v <- Symbolic SVal -> ReaderT Env Symbolic SVal
forall (m :: * -> *) a. Monad m => m a -> ReaderT Env m a
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (Symbolic SVal -> ReaderT Env Symbolic SVal)
-> Symbolic SVal -> ReaderT Env Symbolic SVal
forall a b. (a -> b) -> a -> b
$ Symbolic State
forall (m :: * -> *). MonadSymbolic m => m State
S.symbolicEnv Symbolic State -> (State -> Symbolic SVal) -> Symbolic SVal
forall a b. Symbolic a -> (a -> Symbolic b) -> Symbolic b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= IO SVal -> Symbolic SVal
forall a. IO a -> Symbolic a
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (IO SVal -> Symbolic SVal)
-> (State -> IO SVal) -> State -> Symbolic SVal
forall b c a. (b -> c) -> (a -> b) -> a -> c
. VarContext -> Kind -> Maybe String -> State -> IO SVal
S.svMkSymVar (Maybe Quantifier -> VarContext
S.NonQueryVar Maybe Quantifier
forall a. Maybe a
Nothing) Kind
k Maybe String
nm
                              return (Base v)

       sym (KTup [SKind]
ks) Maybe String
nm = do let ns :: [Maybe String]
ns = (Int -> Maybe String) -> [Int] -> [Maybe String]
forall a b. (a -> b) -> [a] -> [b]
map (\Int
i -> (String -> String -> String
forall a. [a] -> [a] -> [a]
++ (String
"_" String -> String -> String
forall a. [a] -> [a] -> [a]
++ Int -> String
forall a. Show a => a -> String
show Int
i)) (String -> String) -> Maybe String -> Maybe String
forall a b. (a -> b) -> Maybe a -> Maybe b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
`fmap` Maybe String
nm) [Int
1 .. [SKind] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [SKind]
ks]
                             vs <- (SKind -> Maybe String -> ReaderT Env Symbolic Val)
-> [SKind] -> [Maybe String] -> ReaderT Env Symbolic [Val]
forall (m :: * -> *) a b c.
Applicative m =>
(a -> b -> m c) -> [a] -> [b] -> m [c]
zipWithM SKind -> Maybe String -> ReaderT Env Symbolic Val
sym [SKind]
ks [Maybe String]
ns
                             return $ Tup vs

       sym (KLst SKind
ks) Maybe String
nm = do Env{mbListSize, bailOut} <- ReaderT Env Symbolic Env
forall r (m :: * -> *). MonadReader r m => m r
ask
                             ls <- case mbListSize of
                                     Just Int
i  -> Int -> ReaderT Env Symbolic Int
forall a. a -> ReaderT Env Symbolic a
forall (m :: * -> *) a. Monad m => a -> m a
return Int
i
                                     Maybe Int
Nothing -> String -> [String] -> ReaderT Env Symbolic Int
forall a. String -> [String] -> Eval a
bailOut String
"List-argument found, with no size info"
                                                        [ String
"Name: " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String -> Maybe String -> String
forall a. a -> Maybe a -> a
fromMaybe String
"anonymous" Maybe String
nm
                                                        , SKind -> String
forall {a}. Outputable a => a -> String
tinfo (SKind -> SKind
KLst SKind
ks)
                                                        , String
"Hint: Use the \"ListSize\" annotation"
                                                        ]
                             let ns = (Int -> Maybe String) -> [Int] -> [Maybe String]
forall a b. (a -> b) -> [a] -> [b]
map (\Int
i -> (String -> String -> String
forall a. [a] -> [a] -> [a]
++ (String
"_" String -> String -> String
forall a. [a] -> [a] -> [a]
++ Int -> String
forall a. Show a => a -> String
show Int
i)) (String -> String) -> Maybe String -> Maybe String
forall a b. (a -> b) -> Maybe a -> Maybe b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
`fmap` Maybe String
nm) [Int
1 .. Int
ls]
                             vs <- zipWithM sym (replicate ls ks) ns
                             return (Lst vs)

       sym k :: SKind
k@KFun{}  Maybe String
nm = case Maybe Var
mbBind of
                            Just Var
v -> Bool -> Type -> Var -> ReaderT Env Symbolic Val
uninterpret Bool
True (Var -> Type
varType Var
v) Var
v
                            Maybe Var
_      -> do Env{bailOut} <- ReaderT Env Symbolic Env
forall r (m :: * -> *). MonadReader r m => m r
ask
                                         bailOut "Unsupported unnamed higher-order symbolic input"
                                                 [ "Name: " ++ fromMaybe "<anonymous>" nm
                                                 , tinfo k
                                                 , "Hint: Name all higher-order inputs explicitly"
                                                 ]


-- | Unscale a value. We don't really care about the scale itself, so far as SBV is concerned
unScale :: Scaled a -> a
unScale :: forall a. Scaled a -> a
unScale (Scaled Type
_ a
a) = a
a

-- | Uninterpret an expression
uninterpret :: Bool -> Type -> Var -> Eval Val
uninterpret :: Bool -> Type -> Var -> ReaderT Env Symbolic Val
uninterpret Bool
isInput Type
t Var
var = do
          Env{rUninterpreted, flags} <- ReaderT Env Symbolic Env
forall r (m :: * -> *). MonadReader r m => m r
ask
          prevUninterpreted <- liftIO $ readIORef rUninterpreted
          case [r | ((v, t'), r) <- prevUninterpreted, var == v && t `eqType` t'] of
             (Bool
_, String
_, Val
val):[(Bool, String, Val)]
_ -> Val -> ReaderT Env Symbolic Val
forall a. a -> ReaderT Env Symbolic a
forall (m :: * -> *) a. Monad m => a -> m a
return Val
val
             []            -> do let ([Var]
tvs,  Type
t')  = Type -> ([Var], Type)
splitForAllTyCoVars Type
t
                                     ([Scaled Type]
args, Type
res) = Type -> ([Scaled Type], Type)
splitFunTys Type
t'
                                     sp :: SrcSpan
sp          = Var -> SrcSpan
forall a. NamedThing a => a -> SrcSpan
getSrcSpan Var
var
                                 argKs <- (Scaled Type -> Eval SKind)
-> [Scaled Type] -> ReaderT Env Symbolic [SKind]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [b]
mapM (SrcSpan -> Type -> Eval SKind
getType SrcSpan
sp (Type -> Eval SKind)
-> (Scaled Type -> Type) -> Scaled Type -> Eval SKind
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Scaled Type -> Type
forall a. Scaled a -> a
unScale) [Scaled Type]
args
                                 resK  <- getType sp res
                                 nm    <- mkValidName $ showSDoc flags (ppr var)
                                 body  <- walk argKs (nm, resK) []
                                 let fVal = [Var] -> Val -> Val
forall {a}. [a] -> Val -> Val
wrap [Var]
tvs Val
body
                                 liftIO $ modifyIORef rUninterpreted (((var, t), (isInput, nm, fVal)) :)
                                 return fVal
  where walk :: [SKind] -> (String, SKind) -> [Val] -> Eval Val
        walk :: [SKind] -> (String, SKind) -> [Val] -> ReaderT Env Symbolic Val
walk []     (String
nm, SKind
k) [Val]
args = do Env{mbListSize, bailOut} <- ReaderT Env Symbolic Env
forall r (m :: * -> *). MonadReader r m => m r
ask

                                      let mkArg :: Val -> [S.SVal]
                                          mkArg (Base SVal
v)  = [SVal
v]
                                          mkArg (Tup  [Val]
vs) = (Val -> [SVal]) -> [Val] -> [SVal]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap Val -> [SVal]
mkArg [Val]
vs
                                          mkArg (Lst  [Val]
vs) = (Val -> [SVal]) -> [Val] -> [SVal]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap Val -> [SVal]
mkArg [Val]
vs
                                          mkArg Val
sk        = String -> [SVal]
forall a. HasCallStack => String -> a
error (String -> [SVal]) -> String -> [SVal]
forall a b. (a -> b) -> a -> b
$ String
"Not yet supported uninterpreted function with a higher-order argument: " String -> String -> String
forall a. [a] -> [a] -> [a]
++ SDoc -> String
showSDocUnsafe (Val -> SDoc
forall a. Outputable a => a -> SDoc
ppr Val
sk)

                                          bArgs = (Val -> [SVal]) -> [Val] -> [SVal]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap Val -> [SVal]
mkArg ([Val] -> [Val]
forall a. [a] -> [a]
reverse [Val]
args)

                                          mkRes :: String -> SKind -> Eval [S.SVal]
                                          mkRes String
n (KBase Kind
b)  = [SVal] -> Eval [SVal]
forall a. a -> ReaderT Env Symbolic a
forall (m :: * -> *) a. Monad m => a -> m a
return [Kind -> String -> UICodeKind -> [SVal] -> SVal
S.svUninterpreted Kind
b String
n (Bool -> UICodeKind
S.UINone Bool
True) [SVal]
bArgs]
                                          mkRes String
n (KTup  [SKind]
bs) = [[SVal]] -> [SVal]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat ([[SVal]] -> [SVal])
-> ReaderT Env Symbolic [[SVal]] -> Eval [SVal]
forall a b.
(a -> b) -> ReaderT Env Symbolic a -> ReaderT Env Symbolic b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
`fmap` (String -> SKind -> Eval [SVal])
-> [String] -> [SKind] -> ReaderT Env Symbolic [[SVal]]
forall (m :: * -> *) a b c.
Applicative m =>
(a -> b -> m c) -> [a] -> [b] -> m [c]
zipWithM String -> SKind -> Eval [SVal]
mkRes [String
n String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
"_" String -> String -> String
forall a. [a] -> [a] -> [a]
++ Int -> String
forall a. Show a => a -> String
show Int
i | Int
i <- [(Int
1 :: Int) ..   ]] [SKind]
bs
                                          mkRes String
n (KLst  SKind
b)  = do ls <- case Maybe Int
mbListSize of
                                                                          Just Int
i  -> Int -> ReaderT Env Symbolic Int
forall a. a -> ReaderT Env Symbolic a
forall (m :: * -> *) a. Monad m => a -> m a
return Int
i
                                                                          Maybe Int
Nothing -> String -> [String] -> ReaderT Env Symbolic Int
forall a. String -> [String] -> Eval a
bailOut String
"List-argument found in uninterpreted function, with no size info"
                                                                                             [String
"Hint: Use the \"ListSize\" annotation"]
                                                                  concat `fmap` zipWithM mkRes [n ++ "_" ++ show i | i <- [(1 :: Int) .. ls]] (repeat b)
                                          mkRes String
n sk :: SKind
sk@KFun{}   = String -> [String] -> Eval [SVal]
forall a. String -> [String] -> Eval a
bailOut String
"Not yet supported uninterpreted function with a higher-order result"
                                                                        [ String
"Name: " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
n
                                                                        , String
"Kind: " String -> String -> String
forall a. [a] -> [a] -> [a]
++ SDoc -> String
showSDocUnsafe (SKind -> SDoc
forall a. Outputable a => a -> SDoc
ppr SKind
sk)
                                                                        ]

                                      res <- mkRes nm k
                                      case map Base res of
                                        [Val
x] -> Val -> ReaderT Env Symbolic Val
forall a. a -> ReaderT Env Symbolic a
forall (m :: * -> *) a. Monad m => a -> m a
return Val
x
                                        [Val]
xs  -> Val -> ReaderT Env Symbolic Val
forall a. a -> ReaderT Env Symbolic a
forall (m :: * -> *) a. Monad m => a -> m a
return (Val -> ReaderT Env Symbolic Val)
-> Val -> ReaderT Env Symbolic Val
forall a b. (a -> b) -> a -> b
$ [Val] -> Val
Tup [Val]
xs

        walk (SKind
_:[SKind]
ks) (String, SKind)
nmk     [Val]
args = Val -> ReaderT Env Symbolic Val
forall a. a -> ReaderT Env Symbolic a
forall (m :: * -> *) a. Monad m => a -> m a
return (Val -> ReaderT Env Symbolic Val)
-> Val -> ReaderT Env Symbolic Val
forall a b. (a -> b) -> a -> b
$ Maybe String -> (Val -> ReaderT Env Symbolic Val) -> Val
Func Maybe String
forall a. Maybe a
Nothing ((Val -> ReaderT Env Symbolic Val) -> Val)
-> (Val -> ReaderT Env Symbolic Val) -> Val
forall a b. (a -> b) -> a -> b
$ \Val
a -> [SKind] -> (String, SKind) -> [Val] -> ReaderT Env Symbolic Val
walk [SKind]
ks (String, SKind)
nmk (Val
aVal -> [Val] -> [Val]
forall a. a -> [a] -> [a]
:[Val]
args)

        wrap :: [a] -> Val -> Val
wrap []     Val
f = Val
f
        wrap (a
_:[a]
ts) Val
f = Maybe String -> (Val -> ReaderT Env Symbolic Val) -> Val
Func Maybe String
forall a. Maybe a
Nothing ((Val -> ReaderT Env Symbolic Val) -> Val)
-> (Val -> ReaderT Env Symbolic Val) -> Val
forall a b. (a -> b) -> a -> b
$ \Val
_ -> Val -> ReaderT Env Symbolic Val
forall a. a -> ReaderT Env Symbolic a
forall (m :: * -> *) a. Monad m => a -> m a
return ([a] -> Val -> Val
wrap [a]
ts Val
f)

-- not every name is good, sigh
mkValidName :: String -> Eval String
mkValidName :: String -> Eval String
mkValidName String
name =
        do Env{rUsedNames} <- ReaderT Env Symbolic Env
forall r (m :: * -> *). MonadReader r m => m r
ask
           usedNames <- liftIO $ readIORef rUsedNames
           let unm = String -> String
unSMT (String -> String) -> String -> String
forall a b. (a -> b) -> a -> b
$ [String] -> String -> String
forall {t :: * -> *}. Foldable t => t String -> String -> String
genSym [String]
usedNames String
name
           liftIO $ modifyIORef rUsedNames (unm :)
           return $ escape unm
  where genSym :: t String -> String -> String
genSym t String
bad String
nm
          | String
nm String -> t String -> Bool
forall a. Eq a => a -> t a -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` t String
bad = String -> [String] -> String
forall a. String -> [a] -> a
hd (String
"genSym: " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
nm) [String
nm' | Int
i <- [(Int
0::Int) ..], let nm' :: String
nm' = String
nm String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
"_" String -> String -> String
forall a. [a] -> [a] -> [a]
++ Int -> String
forall a. Show a => a -> String
show Int
i, String
nm' String -> t String -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`notElem` t String
bad]
          | Bool
True          = String
nm

        unSMT :: String -> String
unSMT String
nm
          | (Char -> Char) -> String -> String
forall a b. (a -> b) -> [a] -> [b]
map Char -> Char
toLower String
nm String -> [String] -> Bool
forall a. Eq a => a -> [a] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [String]
S.smtLibReservedNames
          = if Bool -> Bool
not (String -> Bool
forall a. [a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null String
nm) Bool -> Bool -> Bool
&& Char -> Bool
isUpper (String -> String -> Char
forall a. String -> [a] -> a
hd String
"unSMT" String
nm)
            then String
"sbv"  String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
nm
            else String
"sbv_" String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
nm
          | Bool
True
          = String
nm

        escape :: String -> String
escape String
nm | Char -> Bool
isAlpha (String -> String -> Char
forall a. String -> [a] -> a
hd String
"escape" String
nm) Bool -> Bool -> Bool
&& (Char -> Bool) -> String -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all Char -> Bool
isGood (String -> String -> String
forall a. String -> [a] -> [a]
tl String
"escape" String
nm) = String
nm
                  | Bool
True                                                    = String
"|" String -> String -> String
forall a. [a] -> [a] -> [a]
++ (Char -> Char) -> String -> String
forall a b. (a -> b) -> [a] -> [b]
map Char -> Char
tr String
nm String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
"|"

        isGood :: Char -> Bool
isGood Char
c = Char -> Bool
isAlphaNum Char
c Bool -> Bool -> Bool
|| Char
c Char -> Char -> Bool
forall a. Eq a => a -> a -> Bool
== Char
'_'
        tr :: Char -> Char
tr Char
'|'   = Char
'_'
        tr Char
'\\'  = Char
'_'
        tr Char
c     = Char
c

hd :: String -> [a] -> a
hd :: forall a. String -> [a] -> a
hd String
_ (a
x:[a]
_) = a
x
hd String
n []    = String -> a
forall a. HasCallStack => String -> a
error (String -> a) -> String -> a
forall a b. (a -> b) -> a -> b
$ String
"Impossible happened: hd received empty list while running " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String -> String
forall a. Show a => a -> String
show String
n

tl :: String -> [a] -> [a]
tl :: forall a. String -> [a] -> [a]
tl String
_ (a
_:[a]
xs) = [a]
xs
tl String
n []     = String -> [a]
forall a. HasCallStack => String -> a
error (String -> [a]) -> String -> [a]
forall a b. (a -> b) -> a -> b
$ String
"Impossible happened: hd received empty list while running " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String -> String
forall a. Show a => a -> String
show String
n

-- | Convert a Core type to an SBV Type, retaining functions and tuples
getType :: SrcSpan -> Type -> Eval SKind
getType :: SrcSpan -> Type -> Eval SKind
getType SrcSpan
sp Type
typ = do let ([Var]
tvs, Type
typ') = Type -> ([Var], Type)
splitForAllTyCoVars Type
typ
                        ([Scaled Type]
args, Type
res) = Type -> ([Scaled Type], Type)
splitFunTys Type
typ'
                    argKs <- (Scaled Type -> Eval SKind)
-> [Scaled Type] -> ReaderT Env Symbolic [SKind]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [b]
mapM (SrcSpan -> Type -> Eval SKind
getType SrcSpan
sp (Type -> Eval SKind)
-> (Scaled Type -> Type) -> Scaled Type -> Eval SKind
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Scaled Type -> Type
forall a. Scaled a -> a
unScale) [Scaled Type]
args
                    resK  <- getComposite res
                    return $ wrap tvs $ foldr KFun resK argKs
 where wrap :: t Var -> SKind -> SKind
wrap t Var
ts SKind
f         = (Var -> SKind -> SKind) -> SKind -> t Var -> SKind
forall a b. (a -> b -> b) -> b -> t a -> b
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr (SKind -> SKind -> SKind
KFun (SKind -> SKind -> SKind)
-> (Var -> SKind) -> Var -> SKind -> SKind
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Var -> SKind
mkUninterpreted) SKind
f t Var
ts
       mkUninterpreted :: Var -> SKind
mkUninterpreted Var
v = Kind -> SKind
KBase (Kind -> SKind) -> Kind -> SKind
forall a b. (a -> b) -> a -> b
$ String -> Maybe [String] -> Kind
S.KUserSort (FastString -> String
forall a. Show a => a -> String
show (OccName -> FastString
occNameFS (Name -> OccName
forall name. HasOccName name => name -> OccName
occName (Var -> Name
varName Var
v)))) Maybe [String]
forall a. Maybe a
Nothing

       -- | Extract tuples, lists, or base kinds
       getComposite :: Type -> Eval SKind
       getComposite :: Type -> Eval SKind
getComposite Type
t = case HasDebugCallStack => Type -> Maybe (TyCon, [Type])
Type -> Maybe (TyCon, [Type])
splitTyConApp_maybe Type
t of
                          Just (TyCon
k, [Type]
ts)  | TyCon -> Bool
isTupleTyCon TyCon
k -> [SKind] -> SKind
KTup  ([SKind] -> SKind) -> ReaderT Env Symbolic [SKind] -> Eval SKind
forall a b.
(a -> b) -> ReaderT Env Symbolic a -> ReaderT Env Symbolic b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
`fmap` (Type -> Eval SKind) -> [Type] -> ReaderT Env Symbolic [SKind]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [b]
mapM (SrcSpan -> Type -> Eval SKind
getType SrcSpan
sp) [Type]
ts
                          Just (TyCon
k, [Type
a]) | TyCon
listTyCon TyCon -> TyCon -> Bool
forall a. Eq a => a -> a -> Bool
== TyCon
k -> SKind -> SKind
KLst  (SKind -> SKind) -> Eval SKind -> Eval SKind
forall a b.
(a -> b) -> ReaderT Env Symbolic a -> ReaderT Env Symbolic b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
`fmap` SrcSpan -> Type -> Eval SKind
getType SrcSpan
sp Type
a
                          Maybe (TyCon, [Type])
_                              -> Kind -> SKind
KBase (Kind -> SKind) -> ReaderT Env Symbolic Kind -> Eval SKind
forall a b.
(a -> b) -> ReaderT Env Symbolic a -> ReaderT Env Symbolic b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
`fmap` Type -> ReaderT Env Symbolic Kind
getBaseType Type
t

       -- | Convert a Core type to an SBV kind, if known
       -- Otherwise, create an uninterpreted kind, and return that.
       getBaseType :: Type -> Eval S.Kind
       getBaseType :: Type -> ReaderT Env Symbolic Kind
getBaseType Type
bt = do
               Env{tcMap} <- ReaderT Env Symbolic Env
forall r (m :: * -> *). MonadReader r m => m r
ask
               case grabTCs (splitTyConApp_maybe bt) of
                 Just TCKey
k -> ReaderT Env Symbolic Kind
-> (Kind -> ReaderT Env Symbolic Kind)
-> Maybe Kind
-> ReaderT Env Symbolic Kind
forall b a. b -> (a -> b) -> Maybe a -> b
maybe ReaderT Env Symbolic Kind
unknown Kind -> ReaderT Env Symbolic Kind
forall a. a -> ReaderT Env Symbolic a
forall (m :: * -> *) a. Monad m => a -> m a
return (TCKey
k TCKey -> Map TCKey Kind -> Maybe Kind
forall k a. Ord k => k -> Map k a -> Maybe a
`M.lookup` Map TCKey Kind
tcMap)
                 Maybe TCKey
_      -> ReaderT Env Symbolic Kind
unknown
         where -- allow one level of nesting, essentially to support Haskell's 'Ratio Integer' to map to 'SReal'
               grabTCs :: Maybe (TyCon, [Type]) -> Maybe TCKey
grabTCs Maybe (TyCon, [Type])
Nothing          = Maybe TCKey
forall a. Maybe a
Nothing
               grabTCs (Just (TyCon
top, [Type]
ts)) = do as <- [Type] -> [TyCon] -> Maybe [TyCon]
walk [Type]
ts []
                                             return $ TCKey (top, as)
               walk :: [Type] -> [TyCon] -> Maybe [TyCon]
walk []     [TyCon]
sofar = [TyCon] -> Maybe [TyCon]
forall a. a -> Maybe a
Just ([TyCon] -> Maybe [TyCon]) -> [TyCon] -> Maybe [TyCon]
forall a b. (a -> b) -> a -> b
$ [TyCon] -> [TyCon]
forall a. [a] -> [a]
reverse [TyCon]
sofar
               walk (Type
a:[Type]
as) [TyCon]
sofar = case HasDebugCallStack => Type -> Maybe (TyCon, [Type])
Type -> Maybe (TyCon, [Type])
splitTyConApp_maybe Type
a of
                                      Just (TyCon
ac, []) -> [Type] -> [TyCon] -> Maybe [TyCon]
walk [Type]
as (TyCon
acTyCon -> [TyCon] -> [TyCon]
forall a. a -> [a] -> [a]
:[TyCon]
sofar)
                                      Maybe (TyCon, [Type])
_             -> Maybe [TyCon]
forall a. Maybe a
Nothing
               -- Check if we uninterpreted this before; if so, return it, otherwise create a new one
               unknown :: ReaderT Env Symbolic Kind
unknown = do Env{flags, rUITypes} <- ReaderT Env Symbolic Env
forall r (m :: * -> *). MonadReader r m => m r
ask
                            uiTypes <- liftIO $ readIORef rUITypes
                            case [k | (bt', k) <- uiTypes, bt `eqType` bt'] of
                              Kind
k:[Kind]
_ -> Kind -> ReaderT Env Symbolic Kind
forall a. a -> ReaderT Env Symbolic a
forall (m :: * -> *) a. Monad m => a -> m a
return Kind
k
                              []  -> do nm <- String -> Eval String
mkValidName (String -> Eval String) -> String -> Eval String
forall a b. (a -> b) -> a -> b
$ DynFlags -> SDoc -> String
showSDoc DynFlags
flags (Type -> SDoc
forall a. Outputable a => a -> SDoc
ppr Type
bt)
                                        let k = String -> Maybe [String] -> Kind
S.KUserSort String
nm Maybe [String]
forall a. Maybe a
Nothing
                                        liftIO $ modifyIORef rUITypes ((bt, k) :)
                                        return k

{-# ANN module ("HLint: ignore Reduce duplication" :: String) #-}