---------------------------------------------------------------------------
-- |
-- 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 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

-- | Dispatch the analyzer over bindings
analyzeBind :: Config -> CoreBind -> CoreM ()
analyzeBind :: Config -> CoreBind -> CoreM ()
analyzeBind cfg :: Config
cfg@Config{Var -> [SBVAnnotation]
sbvAnnotation :: Config -> Var -> [SBVAnnotation]
sbvAnnotation :: Var -> [SBVAnnotation]
sbvAnnotation, Env
cfgEnv :: Config -> Env
cfgEnv :: 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 (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 (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 (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 (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 (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [SBVOption]
opts
                   = () -> m ()
forall (m :: * -> *) a. Monad m => a -> m a
return ()
                   | Bool
True
                   = IO () -> m ()
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 :: Config -> Bool
isGHCi :: Bool
isGHCi} [SBVOption]
opts Var
b CoreExpr
e = do
        Bool
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
        Bool -> IO () -> IO ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless (Bool
success Bool -> Bool -> Bool
|| Bool
isGHCi Bool -> Bool -> Bool
|| SBVOption
IgnoreFailure SBVOption -> [SBVOption] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [SBVOption]
opts) (IO () -> IO ()) -> IO () -> IO ()
forall a b. (a -> b) -> a -> b
$ do
            String -> IO ()
putStrLn (String -> IO ()) -> String -> IO ()
forall a b. (a -> b) -> a -> b
$ String
"[SBV] Failed. (Use option '" String -> String -> String
forall a. [a] -> [a] -> [a]
++ SBVOption -> String
forall a. Show a => a -> String
show SBVOption
IgnoreFailure String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
"' to continue.)"
            IO ()
forall a. IO a
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 (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 :: Env
cfgEnv :: Config -> Env
cfgEnv, Var -> [SBVAnnotation]
sbvAnnotation :: Var -> [SBVAnnotation]
sbvAnnotation :: Config -> Var -> [SBVAnnotation]
sbvAnnotation} [SBVOption]
opts Var
topBind CoreExpr
topExpr = do
        [SMTConfig]
solverConfigs <- [SBVOption] -> IO [SMTConfig]
pickSolvers [SBVOption]
opts
        let verbose :: Bool
verbose = SBVOption
Verbose    SBVOption -> [SBVOption] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [SBVOption]
opts
            qCheck :: Bool
qCheck  = SBVOption
QuickCheck SBVOption -> [SBVOption] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [SBVOption]
opts
            runProver :: Symbolic SVal
-> IO (Either Bool (Solver, NominalDiffTime, ThmResult))
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 (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 (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
`fmap` [SMTConfig]
-> Symbolic SVal -> IO (Solver, NominalDiffTime, ThmResult)
S.proveWithAny [SMTConfig
s{verbose :: Bool
S.verbose = Bool
verbose} | SMTConfig
s <- [SMTConfig]
solverConfigs] Symbolic SVal
prop
            topLoc :: SrcSpan
topLoc = Var -> SrcSpan
varSpan Var
topBind
            loc :: String
loc = String
"[SBV] " String -> String -> String
forall a. [a] -> [a] -> [a]
++ DynFlags -> SrcSpan -> String
showSpan (Env -> DynFlags
flags Env
cfgEnv) SrcSpan
topLoc
            slvrTag :: String
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. [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. [a] -> a
last [Solver]
xs)
        String -> IO ()
putStrLn (String -> IO ()) -> String -> IO ()
forall a b. (a -> b) -> a -> b
$ String
"\n" String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
loc String -> String -> String
forall a. [a] -> [a] -> [a]
++ (if Bool
qCheck then String
" QuickChecking " else String
" Proving ") String -> String -> String
forall a. [a] -> [a] -> [a]
++ String -> String
forall a. Show a => a -> String
show (Var -> String
forall {a}. Outputable a => a -> String
sh Var
topBind) String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
slvrTag
        (Either Bool (Solver, NominalDiffTime, ThmResult)
finalResult, [((Var, Type), (Bool, String, Val))]
finalUninterps) <- do
                        Either Bool (Solver, NominalDiffTime, ThmResult)
finalResult    <- Symbolic SVal
-> IO (Either Bool (Solver, NominalDiffTime, ThmResult))
runProver (Env -> SrcSpan -> Symbolic SVal
res Env
cfgEnv SrcSpan
topLoc)
                        [((Var, Type), (Bool, String, Val))]
finalUninterps <- IORef [((Var, Type), (Bool, String, Val))]
-> IO [((Var, Type), (Bool, String, Val))]
forall a. IORef a -> IO a
readIORef (Env -> IORef [((Var, Type), (Bool, String, Val))]
rUninterpreted Env
cfgEnv)
                        (Either Bool (Solver, NominalDiffTime, ThmResult),
 [((Var, Type), (Bool, String, Val))])
-> IO
     (Either Bool (Solver, NominalDiffTime, ThmResult),
      [((Var, Type), (Bool, String, Val))])
forall (m :: * -> *) a. Monad m => a -> m a
return (Either Bool (Solver, NominalDiffTime, ThmResult)
finalResult, [((Var, Type), (Bool, String, Val))]
finalUninterps)
        case Either Bool (Solver, NominalDiffTime, ThmResult)
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 (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 (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 (t :: * -> *) a. (Foldable t, Ord a) => t a -> a
maximum (Int
0 Int -> [Int] -> [Int]
forall a. a -> [a] -> [a]
: [String -> 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 (t :: * -> *) a. (Foldable t, Ord a) => t a -> a
maximum (Int
0 Int -> [Int] -> [Int]
forall a. a -> [a] -> [a]
: [String -> 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 (m :: * -> *) a. Monad m => a -> m a
return Bool
success
          Left Bool
success -> Bool -> IO Bool
forall (m :: * -> *) a. Monad m => a -> m a
return Bool
success

  where debug :: Bool
debug = SBVOption
Debug SBVOption -> [SBVOption] -> 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{DynFlags
flags :: DynFlags
flags :: Env -> DynFlags
flags, [SrcSpan]
curLoc :: Env -> [SrcSpan]
curLoc :: [SrcSpan]
curLoc} <- ReaderT Env Symbolic Env
forall r (m :: * -> *). MonadReader r m => m r
ask
                             let marker :: String
marker = String
"[SBV] " String -> String -> String
forall a. [a] -> [a] -> [a]
++ DynFlags -> SrcSpan -> String
showSpan DynFlags
flags ([SrcSpan] -> SrcSpan
pickSpan [SrcSpan]
curLoc)
                                 tag :: String -> String
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 -> String
tab String
s = Int -> Char -> String
forall a. Int -> a -> [a]
replicate (String -> 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
                                 msg :: String
msg   = (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)
                             String -> Eval a
forall a. String -> a
errorWithoutStackTrace String
msg
#else
                             error msg
#endif

        res :: Env -> SrcSpan -> Symbolic SVal
res Env
initEnv SrcSpan
topLoc = do
               Val
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 :: [SrcSpan]
curLoc     = [SrcSpan
topLoc]
                                                         , mbListSize :: Maybe Int
mbListSize = [Int] -> Maybe Int
forall a. [a] -> Maybe a
listToMaybe [Int
n | ListSize Int
n <- [SBVOption]
opts]
                                                         , bailOut :: forall a. String -> [String] -> Eval a
bailOut    = forall a. String -> [String] -> Eval a
cantHandle
                                                         }
               case Val
v of
                 Base SVal
r -> SVal -> Symbolic SVal
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{forall a. String -> [String] -> Eval a
bailOut :: forall a. String -> [String] -> Eval a
bailOut :: Env -> forall a. String -> [String] -> Eval a
bailOut} <- ReaderT Env Symbolic Env
forall r (m :: * -> *). MonadReader r m => m r
ask
                      String -> [String] -> ReaderT Env Symbolic Val
forall a. String -> [String] -> Eval a
bailOut String
w [String]
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
curEnv@Env{forall a. String -> [String] -> Eval a
bailOut :: forall a. String -> [String] -> Eval a
bailOut :: Env -> forall a. String -> [String] -> Eval a
bailOut} <- ReaderT Env Symbolic Env
forall r (m :: * -> *). MonadReader r m => m r
ask
                       SKind
bodyType <- SrcSpan -> Type -> Eval SKind
getType ([SrcSpan] -> SrcSpan
pickSpan (Env -> [SrcSpan]
curLoc Env
curEnv)) (CoreExpr -> Type
exprType CoreExpr
body)

                       -- Figure out if there were some unmentioned variables; happens if the top
                       -- level wasn't fully saturated.
                       let ([SKind]
extraArgs, SKind
finalType) = SKind -> [SKind] -> ([SKind], SKind)
walk SKind
bodyType []
                                where walk :: SKind -> [SKind] -> ([SKind], SKind)
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 SKind
finalType of
                         KBase Kind
S.KBool -> do -- First collect the named arguments:
                                             [(Var, SKind)]
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)
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 (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \SKind
bt -> (Var, SKind) -> ReaderT Env Symbolic (Var, SKind)
forall (m :: * -> *) a. Monad m => a -> m a
return (Var
b, SKind
bt)) [Var]
bs
                                             let mkVar :: ((Var, SKind), Maybe String)
-> ReaderT Env Symbolic ((Var, SKind), Val)
mkVar ((Var
b, SKind
k), Maybe String
mbN) = do Val
sv <- (Env -> Env)
-> ReaderT Env Symbolic Val -> ReaderT Env Symbolic Val
forall r (m :: * -> *) a. MonadReader r m => (r -> r) -> m a -> m a
local (\Env
env -> Env
env{curLoc :: [SrcSpan]
curLoc = Var -> SrcSpan
varSpan Var
b SrcSpan -> [SrcSpan] -> [SrcSpan]
forall a. a -> [a] -> [a]
: Env -> [SrcSpan]
curLoc Env
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 (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))
                                                                          ((Var, SKind), Val) -> ReaderT Env Symbolic ((Var, SKind), Val)
forall (m :: * -> *) a. Monad m => a -> m a
return ((Var
b, SKind
k), Val
sv)
                                             [((Var, SKind), Val)]
bArgs <- (((Var, SKind), Maybe String)
 -> ReaderT Env Symbolic ((Var, SKind), Val))
-> [((Var, SKind), Maybe String)]
-> ReaderT Env Symbolic [((Var, SKind), Val)]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM ((Var, SKind), Maybe String)
-> ReaderT Env Symbolic ((Var, SKind), Val)
mkVar ([(Var, SKind)] -> [Maybe String] -> [((Var, SKind), Maybe String)]
forall a b. [a] -> [b] -> [(a, b)]
zip [(Var, SKind)]
argKs ([[Maybe String]] -> [Maybe String]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat [(String -> Maybe String) -> [String] -> [Maybe String]
forall a b. (a -> b) -> [a] -> [b]
map String -> Maybe String
forall a. a -> Maybe a
Just [String]
ns | Names [String]
ns <- [SBVOption]
opts] [Maybe String] -> [Maybe String] -> [Maybe String]
forall a. [a] -> [a] -> [a]
++ Maybe String -> [Maybe String]
forall a. a -> [a]
repeat Maybe String
forall a. Maybe a
Nothing))

                                             -- Go ahead and run the body symbolically; on bArgs
                                             Val
bRes <- (Env -> Env)
-> ReaderT Env Symbolic Val -> ReaderT Env Symbolic Val
forall r (m :: * -> *) a. MonadReader r m => (r -> r) -> m a -> m a
local (\Env
env -> Env
env{envMap :: Map (Var, SKind) Val
envMap = (((Var, SKind), Val)
 -> Map (Var, SKind) Val -> Map (Var, SKind) Val)
-> Map (Var, SKind) Val
-> [((Var, SKind), Val)]
-> Map (Var, SKind) Val
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr (((Var, SKind)
 -> Val -> Map (Var, SKind) Val -> Map (Var, SKind) Val)
-> ((Var, SKind), Val)
-> Map (Var, SKind) Val
-> Map (Var, SKind) Val
forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry (Var, SKind) -> Val -> Map (Var, SKind) Val -> Map (Var, SKind) Val
forall k a. Ord k => k -> a -> Map k a -> Map k a
M.insert) (Env -> Map (Var, SKind) Val
envMap Env
env) [((Var, SKind), Val)]
bArgs}) (CoreExpr -> ReaderT Env Symbolic Val
go CoreExpr
body)

                                             -- If there are extraArgs; then create symbolics and apply to the result:
                                             let feed :: [SKind] -> Val -> ReaderT Env Symbolic Val
feed []     Val
sres       = Val -> ReaderT Env Symbolic Val
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 Val
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
                                                                             Val -> ReaderT Env Symbolic Val
f Val
sv ReaderT Env Symbolic Val
-> (Val -> ReaderT Env Symbolic Val) -> ReaderT Env Symbolic Val
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= [SKind] -> Val -> ReaderT Env Symbolic Val
feed [SKind]
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)

                                             [SKind] -> Val -> ReaderT Env Symbolic Val
feed [SKind]
extraArgs Val
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 (CoreExpr -> Type
exprType CoreExpr
e)]
                                                                                             , [String
"Returning: " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Type -> String
forall {a}. Outputable a => a -> String
sh (CoreExpr -> Type
exprType CoreExpr
body) | Bool -> Bool
not ([Var] -> 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 (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 (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 r (m :: * -> *) a. MonadReader r m => (r -> r) -> m a -> m a
local (\Env
envMap -> Env
envMap{curLoc :: [SrcSpan]
curLoc = CoreTickish -> SrcSpan
forall (t :: TickishPass). GenTickish t -> SrcSpan
tickSpan CoreTickish
t SrcSpan -> [SrcSpan] -> [SrcSpan]
forall a. a -> [a] -> [a]
: Env -> [SrcSpan]
curLoc Env
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 (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{Map (Var, SKind) Val
envMap :: Map (Var, SKind) Val
envMap :: Env -> Map (Var, SKind) Val
envMap, Map Var (SrcSpan, CoreExpr)
coreMap :: Env -> Map Var (SrcSpan, CoreExpr)
coreMap :: Map Var (SrcSpan, CoreExpr)
coreMap} <- ReaderT Env Symbolic Env
forall r (m :: * -> *). MonadReader r m => m r
ask
                           SKind
k <- SrcSpan -> Type -> Eval SKind
getType (Var -> SrcSpan
forall a. NamedThing a => a -> SrcSpan
getSrcSpan Var
v) Type
t
                           case (Var
v, SKind
k) (Var, SKind) -> Map (Var, SKind) Val -> Maybe Val
forall k a. Ord k => k -> Map k a -> Maybe a
`M.lookup` Map (Var, SKind) Val
envMap of
                             Just Val
b  -> Val -> ReaderT Env Symbolic Val
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 r (m :: * -> *) a. MonadReader r m => (r -> r) -> m a -> m a
local (\Env
env -> Env
env{curLoc :: [SrcSpan]
curLoc = SrcSpan
l SrcSpan -> [SrcSpan] -> [SrcSpan]
forall a. a -> [a] -> [a]
: Env -> [SrcSpan]
curLoc Env
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
t e :: CoreExpr
e@(Lit Literal
l) = do Env{Int
machWordSize :: Env -> Int
machWordSize :: Int
machWordSize} <- ReaderT Env Symbolic Env
forall r (m :: * -> *). MonadReader r m => m r
ask
                             case Literal
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 (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 (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
LitNumInteger -> Val -> ReaderT Env Symbolic Val
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                    Integer
i
                                                   LitNumType
LitNumInt     -> Val -> ReaderT Env Symbolic Val
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 (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 (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 (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 (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 (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 (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 (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 (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 (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
                                                   LitNumType
LitNumNatural -> ReaderT Env Symbolic Val
unint

                  where unint :: ReaderT Env Symbolic Val
unint = do Env{DynFlags
flags :: DynFlags
flags :: Env -> DynFlags
flags} <- ReaderT Env Symbolic Env
forall r (m :: * -> *). MonadReader r m => m r
ask
                                   SKind
k  <- SrcSpan -> Type -> Eval SKind
getType SrcSpan
noSrcSpan Type
t
                                   String
nm <- String -> Eval String
mkValidName (DynFlags -> SDoc -> String
showSDoc DynFlags
flags (CoreExpr -> SDoc
forall a. Outputable a => a -> SDoc
ppr CoreExpr
e))
                                   case SKind
k of
                                     KBase Kind
b -> Val -> ReaderT Env Symbolic Val
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 -> Maybe [String] -> [SVal] -> SVal
S.svUninterpreted Kind
b String
nm Maybe [String]
forall a. Maybe a
Nothing []
                                     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
             CoreExpr
reduced <- CoreExpr -> Eval CoreExpr
betaReduce CoreExpr
orig

             Env{Specials
specials :: Env -> Specials
specials :: Specials
specials} <- ReaderT Env Symbolic Env
forall r (m :: * -> *). MonadReader r m => m r
ask

             -- handle specials: Equality, tuples, and lists
             let getVar :: Expr b -> Maybe Var
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 :: CoreExpr -> Maybe Val
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 :: Expr b -> Maybe Val
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 :: Expr b -> Maybe Val
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 -> Maybe Val
isSpecial CoreExpr
e = CoreExpr -> Maybe Val
isEq CoreExpr
e Maybe Val -> Maybe Val -> Maybe Val
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 (m :: * -> *) a. MonadPlus m => m a -> m a -> m a
`mplus` CoreExpr -> Maybe Val
forall {b}. Expr b -> Maybe Val
isLst CoreExpr
e

             case CoreExpr -> Maybe Val
isSpecial CoreExpr
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 (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{Map (Var, SKind) Val
envMap :: Map (Var, SKind) Val
envMap :: Env -> Map (Var, SKind) Val
envMap} <- ReaderT Env Symbolic Env
forall r (m :: * -> *). MonadReader r m => m r
ask
                                let vSpan :: SrcSpan
vSpan = Var -> SrcSpan
forall a. NamedThing a => a -> SrcSpan
getSrcSpan Var
v
                                SKind
k1 <- SrcSpan -> Type -> Eval SKind
getType SrcSpan
vSpan Type
t1
                                SKind
k2 <- SrcSpan -> Type -> Eval SKind
getType SrcSpan
vSpan Type
t2
                                let kExp :: SKind
kExp  = SKind -> SKind -> SKind
KFun SKind
k1 (SKind -> SKind -> SKind
KFun SKind
k1 SKind
k2)
                                case (Var
v, SKind
kExp) (Var, SKind) -> Map (Var, SKind) Val -> Maybe Val
forall k a. Ord k => k -> Map k a -> Maybe a
`M.lookup` Map (Var, SKind) Val
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 (m :: * -> *) a. Monad m => a -> m a
return Val
b
                                  Maybe Val
_      -> do Env{Map Var (SrcSpan, CoreExpr)
coreMap :: Map Var (SrcSpan, CoreExpr)
coreMap :: Env -> Map Var (SrcSpan, CoreExpr)
coreMap} <- ReaderT Env Symbolic Env
forall r (m :: * -> *). MonadReader r m => m r
ask
                                               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
e) -> (Env -> Env)
-> ReaderT Env Symbolic Val -> ReaderT Env Symbolic Val
forall r (m :: * -> *) a. MonadReader r m => (r -> r) -> m a -> m a
local (\Env
env -> Env
env{curLoc :: [SrcSpan]
curLoc = SrcSpan
l SrcSpan -> [SrcSpan] -> [SrcSpan]
forall a. a -> [a] -> [a]
: Env -> [SrcSpan]
curLoc Env
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{Map (Var, SKind) Val
envMap :: Map (Var, SKind) Val
envMap :: Env -> Map (Var, SKind) Val
envMap} <- ReaderT Env Symbolic Env
forall r (m :: * -> *). MonadReader r m => m r
ask
                                let vSpan :: SrcSpan
vSpan = Var -> SrcSpan
forall a. NamedThing a => a -> SrcSpan
getSrcSpan Var
v
                                SKind
k1 <- SrcSpan -> Type -> Eval SKind
getType SrcSpan
vSpan Type
t1
                                SKind
k2 <- SrcSpan -> Type -> Eval SKind
getType SrcSpan
vSpan Type
t2
                                let kSplit :: SKind
kSplit = SKind -> SKind -> SKind
KFun SKind
k1 ([SKind] -> SKind
KTup [SKind
k2, SKind
k2])
                                    kJoin :: SKind
kJoin  = SKind -> SKind -> SKind
KFun SKind
k1 (SKind -> SKind -> SKind
KFun SKind
k1 SKind
k2)
                                case ((Var
v, SKind
kSplit) (Var, SKind) -> Map (Var, SKind) Val -> Maybe Val
forall k a. Ord k => k -> Map k a -> Maybe a
`M.lookup` Map (Var, SKind) Val
envMap, (Var
v, SKind
kJoin) (Var, SKind) -> Map (Var, SKind) Val -> Maybe Val
forall k a. Ord k => k -> Map k a -> Maybe a
`M.lookup` Map (Var, SKind) Val
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 (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 (m :: * -> *) a. Monad m => a -> m a
return Val
b
                                  (Maybe Val, Maybe Val)
_           -> do Env{Map Var (SrcSpan, CoreExpr)
coreMap :: Map Var (SrcSpan, CoreExpr)
coreMap :: Env -> Map Var (SrcSpan, CoreExpr)
coreMap} <- ReaderT Env Symbolic Env
forall r (m :: * -> *). MonadReader r m => m r
ask
                                                    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
e) -> (Env -> Env)
-> ReaderT Env Symbolic Val -> ReaderT Env Symbolic Val
forall r (m :: * -> *) a. MonadReader r m => (r -> r) -> m a -> m a
local (\Env
env -> Env
env{curLoc :: [SrcSpan]
curLoc = SrcSpan
l SrcSpan -> [SrcSpan] -> [SrcSpan]
forall a. a -> [a] -> [a]
: Env -> [SrcSpan]
curLoc Env
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{Map (Var, SKind) Val
envMap :: Map (Var, SKind) Val
envMap :: Env -> Map (Var, SKind) Val
envMap} <- ReaderT Env Symbolic Env
forall r (m :: * -> *). MonadReader r m => m r
ask
                                SKind
k <- SrcSpan -> Type -> Eval SKind
getType (Var -> SrcSpan
forall a. NamedThing a => a -> SrcSpan
getSrcSpan Var
v) Type
t
                                case (Var
v, SKind
k) (Var, SKind) -> Map (Var, SKind) Val -> Maybe Val
forall k a. Ord k => k -> Map k a -> Maybe a
`M.lookup` Map (Var, SKind) Val
envMap of
                                  Just Val
b  -> Val -> ReaderT Env Symbolic Val
forall (m :: * -> *) a. Monad m => a -> m a
return Val
b
                                  Maybe Val
Nothing -> do Env{Map Var (SrcSpan, CoreExpr)
coreMap :: Map Var (SrcSpan, CoreExpr)
coreMap :: Env -> Map Var (SrcSpan, CoreExpr)
coreMap} <- ReaderT Env Symbolic Env
forall r (m :: * -> *). MonadReader r m => m r
ask
                                                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
e) -> (Env -> Env)
-> ReaderT Env Symbolic Val -> ReaderT Env Symbolic Val
forall r (m :: * -> *) a. MonadReader r m => (r -> r) -> m a -> m a
local (\Env
env -> Env
env{curLoc :: [SrcSpan]
curLoc = SrcSpan
l SrcSpan -> [SrcSpan] -> [SrcSpan]
forall a. a -> [a] -> [a]
: Env -> [SrcSpan]
curLoc Env
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{Map Var (SrcSpan, CoreExpr)
coreMap :: Map Var (SrcSpan, CoreExpr)
coreMap :: Env -> Map Var (SrcSpan, CoreExpr)
coreMap} <- ReaderT Env Symbolic Env
forall r (m :: * -> *). MonadReader r m => m r
ask
                                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
e) -> (Env -> Env)
-> ReaderT Env Symbolic Val -> ReaderT Env Symbolic Val
forall r (m :: * -> *) a. MonadReader r m => (r -> r) -> m a -> m a
local (\Env
env -> Env
env{curLoc :: [SrcSpan]
curLoc = SrcSpan
l SrcSpan -> [SrcSpan] -> [SrcSpan]
forall a. a -> [a] -> [a]
: Env -> [SrcSpan]
curLoc Env
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
                                Val
func <- CoreExpr -> ReaderT Env Symbolic Val
go CoreExpr
f
                                Val
arg  <- CoreExpr -> ReaderT Env Symbolic Val
go CoreExpr
e
                                case (Val
func, Val
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
                SKind
k <- SrcSpan -> Type -> Eval SKind
getType (Var -> SrcSpan
forall a. NamedThing a => a -> SrcSpan
getSrcSpan Var
b) (Var -> Type
varType Var
b)
                Env{Map (Var, SKind) Val
envMap :: Map (Var, SKind) Val
envMap :: Env -> Map (Var, SKind) Val
envMap} <- ReaderT Env Symbolic Env
forall r (m :: * -> *). MonadReader r m => m r
ask
                Val -> ReaderT Env Symbolic Val
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 (String -> Maybe String
forall a. a -> Maybe a
Just (Var -> String
forall {a}. Outputable a => a -> String
sh Var
b)) ((Val -> ReaderT Env Symbolic Val) -> Val)
-> (Val -> ReaderT Env Symbolic Val) -> Val
forall a b. (a -> b) -> a -> b
$ \Val
s -> (Env -> Env)
-> ReaderT Env Symbolic Val -> ReaderT Env Symbolic Val
forall r (m :: * -> *) a. MonadReader r m => (r -> r) -> m a -> m a
local (\Env
env -> Env
env{envMap :: Map (Var, SKind) Val
envMap = (Var, SKind) -> Val -> Map (Var, SKind) Val -> Map (Var, SKind) Val
forall k a. Ord k => k -> a -> Map k a -> Map k a
M.insert (Var
b, SKind
k) Val
s Map (Var, SKind) Val
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 r (m :: * -> *) a. MonadReader r m => (r -> r) -> m a -> m a
local (\Env
env -> Env
env{coreMap :: Map Var (SrcSpan, CoreExpr)
coreMap = 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) (Env -> Map Var (SrcSpan, CoreExpr)
coreMap Env
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 r (m :: * -> *) a. MonadReader r m => (r -> r) -> m a -> m a
local (\Env
env -> Env
env{coreMap :: Map Var (SrcSpan, CoreExpr)
coreMap = ((Var, CoreExpr)
 -> Map Var (SrcSpan, CoreExpr) -> Map Var (SrcSpan, CoreExpr))
-> Map Var (SrcSpan, CoreExpr)
-> [(Var, CoreExpr)]
-> Map Var (SrcSpan, CoreExpr)
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
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) (Env -> Map Var (SrcSpan, CoreExpr)
coreMap Env
env) [(Var, CoreExpr)]
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 Val
sce <- CoreExpr -> ReaderT Env Symbolic Val
go CoreExpr
ce
                let caseTooComplicated :: String -> [String] -> ReaderT Env Symbolic Val
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 b -> Bool
isDefault (Alt AltCon
DEFAULT [b]
_ Expr b
_) = Bool
True
                    isDefault Alt b
_                 = Bool
False

                    ([Alt Var]
defs, [Alt Var]
nonDefs)           = (Alt Var -> Bool) -> [Alt Var] -> ([Alt Var], [Alt Var])
forall a. (a -> Bool) -> [a] -> ([a], [a])
partition Alt Var -> Bool
forall {b}. Alt b -> Bool
isDefault [Alt Var]
alts

                    walk :: [Alt Var] -> ReaderT Env Symbolic Val
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
                            Maybe (SVal, [((Var, SKind), Val)])
mr <- SrcSpan
-> Val
-> AltCon
-> [Var]
-> Eval (Maybe (SVal, [((Var, SKind), Val)]))
match SrcSpan
eLoc Val
sce AltCon
p [Var]
bs
                            case Maybe (SVal, [((Var, SKind), Val)])
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 r (m :: * -> *) a. MonadReader r m => (r -> r) -> m a -> m a
local (\Env
env -> Env
env{curLoc :: [SrcSpan]
curLoc = SrcSpan
eLoc SrcSpan -> [SrcSpan] -> [SrcSpan]
forall a. a -> [a] -> [a]
: Env -> [SrcSpan]
curLoc Env
env, envMap :: Map (Var, SKind) Val
envMap = (((Var, SKind), Val)
 -> Map (Var, SKind) Val -> Map (Var, SKind) Val)
-> Map (Var, SKind) Val
-> [((Var, SKind), Val)]
-> Map (Var, SKind) Val
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr (((Var, SKind)
 -> Val -> Map (Var, SKind) Val -> Map (Var, SKind) Val)
-> ((Var, SKind), Val)
-> Map (Var, SKind) Val
-> Map (Var, SKind) Val
forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry (Var, SKind) -> Val -> Map (Var, SKind) Val -> Map (Var, SKind) Val
forall k a. Ord k => k -> a -> Map k a -> Map k a
M.insert) (Env -> Map (Var, SKind) Val
envMap Env
env) [((Var, SKind), Val)]
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 (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]

                SKind
k <- SrcSpan -> Type -> Eval SKind
getType (Var -> SrcSpan
forall a. NamedThing a => a -> SrcSpan
getSrcSpan Var
cBinder) Type
caseType
                (Env -> Env)
-> ReaderT Env Symbolic Val -> ReaderT Env Symbolic Val
forall r (m :: * -> *) a. MonadReader r m => (r -> r) -> m a -> m a
local (\Env
env -> Env
env{envMap :: Map (Var, SKind) Val
envMap = (Var, SKind) -> Val -> Map (Var, SKind) Val -> Map (Var, SKind) Val
forall k a. Ord k => k -> a -> Map k a -> Map k a
M.insert (Var
cBinder, SKind
k) Val
sce (Env -> Map (Var, SKind) Val
envMap Env
env)}) (ReaderT Env Symbolic Val -> ReaderT Env Symbolic Val)
-> ReaderT Env Symbolic Val -> ReaderT Env Symbolic Val
forall a b. (a -> b) -> a -> b
$ [Alt Var] -> ReaderT Env Symbolic Val
walk ([Alt Var]
nonDefs [Alt Var] -> [Alt Var] -> [Alt Var]
forall a. [a] -> [a] -> [a]
++ [Alt Var]
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 Val
stb <- ReaderT Env Symbolic Val
tb
                                                             Val
sfb <- ReaderT Env Symbolic Val
fb
                                                             ([String] -> ReaderT Env Symbolic Val)
-> SVal -> Val -> Val -> ReaderT Env Symbolic Val
iteVal [String] -> ReaderT Env Symbolic Val
bailOut SVal
t Val
stb Val
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 (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 Val
b <- CoreExpr -> ReaderT Env Symbolic Val
go (Literal -> CoreExpr
forall b. Literal -> Expr b
Lit Literal
l)
                                                      Maybe (SVal, [((Var, SKind), Val)])
-> Eval (Maybe (SVal, [((Var, SKind), Val)]))
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` Val
b, [])
                                     DataAlt DataCon
dc -> do Env{Map (Var, SKind) Val
envMap :: Map (Var, SKind) Val
envMap :: Env -> Map (Var, SKind) Val
envMap, Map Var (Val -> [(Var, SKind)] -> (SVal, [((Var, SKind), Val)]))
destMap :: Env
-> Map Var (Val -> [(Var, SKind)] -> (SVal, [((Var, SKind), Val)]))
destMap :: Map Var (Val -> [(Var, SKind)] -> (SVal, [((Var, SKind), Val)]))
destMap} <- ReaderT Env Symbolic Env
forall r (m :: * -> *). MonadReader r m => m r
ask
                                                      SKind
k <- SrcSpan -> Type -> Eval SKind
getType SrcSpan
sp (DataCon -> Type
dataConRepType DataCon
dc)
                                                      let wid :: Var
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 (Var
wid, SKind
k) (Var, SKind) -> Map (Var, SKind) Val -> Maybe Val
forall k a. Ord k => k -> Map k a -> Maybe a
`M.lookup` Map (Var, SKind) Val
envMap of
                                                        Just (Base SVal
b) -> Maybe (SVal, [((Var, SKind), Val)])
-> Eval (Maybe (SVal, [((Var, SKind), Val)]))
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 (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 [(Var, SKind)]
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)
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 (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \SKind
bt -> (Var, SKind) -> ReaderT Env Symbolic (Var, SKind)
forall (m :: * -> *) a. Monad m => a -> m a
return (Var
b, SKind
bt)) [Var]
bs
                                                                                         Maybe (SVal, [((Var, SKind), Val)])
-> Eval (Maybe (SVal, [((Var, SKind), Val)]))
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 -> [(Var, SKind)] -> (SVal, [((Var, SKind), Val)])
f Val
a [(Var, SKind)]
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 r (m :: * -> *) a. MonadReader r m => (r -> r) -> m a -> m a
local (\Env
envMap -> Env
envMap{curLoc :: [SrcSpan]
curLoc = CoreTickish -> SrcSpan
forall (t :: TickishPass). GenTickish t -> SrcSpan
tickSpan CoreTickish
t SrcSpan -> [SrcSpan] -> [SrcSpan]
forall a. a -> [a] -> [a]
: Env -> [SrcSpan]
curLoc Env
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{[SrcSpan]
curLoc :: [SrcSpan]
curLoc :: Env -> [SrcSpan]
curLoc} <- ReaderT Env Symbolic Env
forall r (m :: * -> *). MonadReader r m => m r
ask
                SKind
k <- SrcSpan -> Type -> Eval SKind
getType ([SrcSpan] -> SrcSpan
pickSpan [SrcSpan]
curLoc) Type
t
                Val -> ReaderT Env Symbolic Val
forall (m :: * -> *) a. Monad m => a -> m a
return (SKind -> Val
Typ SKind
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
                CoreExpr
rf <- CoreExpr -> Eval CoreExpr
betaReduce CoreExpr
f
                if Bool -> Bool
not (CoreExpr -> Bool
isBetaReducable CoreExpr
a)
                   then CoreExpr -> Eval CoreExpr
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)
                   else do let chaseVars :: CoreExpr -> Eval CoreExpr
                               chaseVars :: CoreExpr -> Eval CoreExpr
chaseVars (Var Var
x)    = do Env{Map Var (SrcSpan, CoreExpr)
coreMap :: Map Var (SrcSpan, CoreExpr)
coreMap :: Env -> Map Var (SrcSpan, CoreExpr)
coreMap} <- ReaderT Env Symbolic Env
forall r (m :: * -> *). MonadReader r m => m r
ask
                                                         case Var
x 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
                                                           Maybe (SrcSpan, CoreExpr)
Nothing     -> CoreExpr -> Eval CoreExpr
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 (m :: * -> *) a. Monad m => a -> m a
return CoreExpr
x
                           CoreExpr
func <- CoreExpr -> Eval CoreExpr
chaseVars CoreExpr
rf
                           case CoreExpr
func of
                             Lam Var
x CoreExpr
b -> do CoreExpr
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
                                           () <- String -> ReaderT Env Symbolic () -> ReaderT Env Symbolic ()
forall a. String -> a -> a
debugTrace (String
"Beta reduce:\n" String -> String -> String
forall a. [a] -> [a] -> [a]
++ (CoreExpr, CoreExpr) -> String
forall {a}. Outputable a => a -> String
sh (CoreExpr
orig, CoreExpr
reduced)) (ReaderT Env Symbolic () -> ReaderT Env Symbolic ())
-> ReaderT Env Symbolic () -> ReaderT Env Symbolic ()
forall a b. (a -> b) -> a -> b
$ () -> ReaderT Env Symbolic ()
forall (m :: * -> *) a. Monad m => a -> m a
return ()
                                           CoreExpr -> Eval CoreExpr
forall (m :: * -> *) a. Monad m => a -> m a
return CoreExpr
reduced
                             CoreExpr
_       -> CoreExpr -> Eval CoreExpr
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 (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 :: Env
cfgEnv :: Config -> 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 SVal
v <- Symbolic SVal -> ReaderT Env Symbolic SVal
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 (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= IO SVal -> Symbolic SVal
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
                              Val -> ReaderT Env Symbolic Val
forall (m :: * -> *) a. Monad m => a -> m a
return (SVal -> Val
Base SVal
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 (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
`fmap` Maybe String
nm) [Int
1 .. [SKind] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [SKind]
ks]
                             [Val]
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
                             Val -> ReaderT Env Symbolic Val
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]
vs

       sym (KLst SKind
ks) Maybe String
nm = do Env{Maybe Int
mbListSize :: Maybe Int
mbListSize :: Env -> Maybe Int
mbListSize, forall a. String -> [String] -> Eval a
bailOut :: forall a. String -> [String] -> Eval a
bailOut :: Env -> forall a. String -> [String] -> Eval a
bailOut} <- ReaderT Env Symbolic Env
forall r (m :: * -> *). MonadReader r m => m r
ask
                             Int
ls <- case Maybe Int
mbListSize of
                                     Just Int
i  -> Int -> ReaderT Env Symbolic Int
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 :: [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 (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
`fmap` Maybe String
nm) [Int
1 .. Int
ls]
                             [Val]
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 (Int -> SKind -> [SKind]
forall a. Int -> a -> [a]
replicate Int
ls SKind
ks) [Maybe String]
ns
                             Val -> ReaderT Env Symbolic Val
forall (m :: * -> *) a. Monad m => a -> m a
return ([Val] -> Val
Lst [Val]
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{forall a. String -> [String] -> Eval a
bailOut :: forall a. String -> [String] -> Eval a
bailOut :: Env -> forall a. String -> [String] -> Eval a
bailOut} <- ReaderT Env Symbolic Env
forall r (m :: * -> *). MonadReader r m => m r
ask
                                         String -> [String] -> ReaderT Env Symbolic Val
forall a. String -> [String] -> Eval a
bailOut String
"Unsupported unnamed higher-order symbolic input"
                                                 [ 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
k
                                                 , String
"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{IORef [((Var, Type), (Bool, String, Val))]
rUninterpreted :: IORef [((Var, Type), (Bool, String, Val))]
rUninterpreted :: Env -> IORef [((Var, Type), (Bool, String, Val))]
rUninterpreted, DynFlags
flags :: DynFlags
flags :: Env -> DynFlags
flags} <- ReaderT Env Symbolic Env
forall r (m :: * -> *). MonadReader r m => m r
ask
          [((Var, Type), (Bool, String, Val))]
prevUninterpreted <- IO [((Var, Type), (Bool, String, Val))]
-> ReaderT Env Symbolic [((Var, Type), (Bool, String, Val))]
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (IO [((Var, Type), (Bool, String, Val))]
 -> ReaderT Env Symbolic [((Var, Type), (Bool, String, Val))])
-> IO [((Var, Type), (Bool, String, Val))]
-> ReaderT Env Symbolic [((Var, Type), (Bool, String, Val))]
forall a b. (a -> b) -> a -> b
$ IORef [((Var, Type), (Bool, String, Val))]
-> IO [((Var, Type), (Bool, String, Val))]
forall a. IORef a -> IO a
readIORef IORef [((Var, Type), (Bool, String, Val))]
rUninterpreted
          case [(Bool, String, Val)
r | ((Var
v, Type
t'), (Bool, String, Val)
r) <- [((Var, Type), (Bool, String, Val))]
prevUninterpreted, Var
var Var -> Var -> Bool
forall a. Eq a => a -> a -> Bool
== Var
v Bool -> Bool -> Bool
&& Type
t Type -> Type -> Bool
`eqType` Type
t'] of
             (Bool
_, String
_, Val
val):[(Bool, String, Val)]
_ -> Val -> ReaderT Env Symbolic Val
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
                                 [SKind]
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)
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
                                 SKind
resK  <- SrcSpan -> Type -> Eval SKind
getType SrcSpan
sp Type
res
                                 String
nm    <- String -> Eval String
mkValidName (String -> Eval String) -> String -> Eval String
forall a b. (a -> b) -> a -> b
$ DynFlags -> SDoc -> String
showSDoc DynFlags
flags (Var -> SDoc
forall a. Outputable a => a -> SDoc
ppr Var
var)
                                 Val
body  <- [SKind] -> (String, SKind) -> [Val] -> ReaderT Env Symbolic Val
walk [SKind]
argKs (String
nm, SKind
resK) []
                                 let fVal :: Val
fVal = [Var] -> Val -> Val
forall {a}. [a] -> Val -> Val
wrap [Var]
tvs Val
body
                                 IO () -> ReaderT Env Symbolic ()
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (IO () -> ReaderT Env Symbolic ())
-> IO () -> ReaderT Env Symbolic ()
forall a b. (a -> b) -> a -> b
$ IORef [((Var, Type), (Bool, String, Val))]
-> ([((Var, Type), (Bool, String, Val))]
    -> [((Var, Type), (Bool, String, Val))])
-> IO ()
forall a. IORef a -> (a -> a) -> IO ()
modifyIORef IORef [((Var, Type), (Bool, String, Val))]
rUninterpreted (((Var
var, Type
t), (Bool
isInput, String
nm, Val
fVal)) ((Var, Type), (Bool, String, Val))
-> [((Var, Type), (Bool, String, Val))]
-> [((Var, Type), (Bool, String, Val))]
forall a. a -> [a] -> [a]
:)
                                 Val -> ReaderT Env Symbolic Val
forall (m :: * -> *) a. Monad m => a -> m a
return Val
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{Maybe Int
mbListSize :: Maybe Int
mbListSize :: Env -> Maybe Int
mbListSize, forall a. String -> [String] -> Eval a
bailOut :: forall a. String -> [String] -> Eval a
bailOut :: Env -> forall a. String -> [String] -> Eval a
bailOut} <- ReaderT Env Symbolic Env
forall r (m :: * -> *). MonadReader r m => m r
ask

                                      let mkArg :: Val -> [S.SVal]
                                          mkArg :: Val -> [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 :: [SVal]
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 -> SKind -> Eval [SVal]
mkRes String
n (KBase Kind
b)  = [SVal] -> Eval [SVal]
forall (m :: * -> *) a. Monad m => a -> m a
return [Kind -> String -> Maybe [String] -> [SVal] -> SVal
S.svUninterpreted Kind
b String
n Maybe [String]
forall a. Maybe a
Nothing [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 (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 Int
ls <- case Maybe Int
mbListSize of
                                                                          Just Int
i  -> Int -> ReaderT Env Symbolic Int
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"]
                                                                  [[SVal]] -> [SVal]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat ([[SVal]] -> [SVal])
-> ReaderT Env Symbolic [[SVal]] -> Eval [SVal]
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) .. Int
ls]] (SKind -> [SKind]
forall a. a -> [a]
repeat SKind
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)
                                                                        ]

                                      [SVal]
res <- String -> SKind -> Eval [SVal]
mkRes String
nm SKind
k
                                      case (SVal -> Val) -> [SVal] -> [Val]
forall a b. (a -> b) -> [a] -> [b]
map SVal -> Val
Base [SVal]
res of
                                        [Val
x] -> Val -> ReaderT Env Symbolic Val
forall (m :: * -> *) a. Monad m => a -> m a
return Val
x
                                        [Val]
xs  -> Val -> ReaderT Env Symbolic Val
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 (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 (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{IORef [String]
rUsedNames :: Env -> IORef [String]
rUsedNames :: IORef [String]
rUsedNames} <- ReaderT Env Symbolic Env
forall r (m :: * -> *). MonadReader r m => m r
ask
           [String]
usedNames <- IO [String] -> ReaderT Env Symbolic [String]
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (IO [String] -> ReaderT Env Symbolic [String])
-> IO [String] -> ReaderT Env Symbolic [String]
forall a b. (a -> b) -> a -> b
$ IORef [String] -> IO [String]
forall a. IORef a -> IO a
readIORef IORef [String]
rUsedNames
           let unm :: String
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
           IO () -> ReaderT Env Symbolic ()
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (IO () -> ReaderT Env Symbolic ())
-> IO () -> ReaderT Env Symbolic ()
forall a b. (a -> b) -> a -> b
$ IORef [String] -> ([String] -> [String]) -> IO ()
forall a. IORef a -> (a -> a) -> IO ()
modifyIORef IORef [String]
rUsedNames (String
unm String -> [String] -> [String]
forall a. a -> [a] -> [a]
:)
           String -> Eval String
forall (m :: * -> *) a. Monad m => a -> m a
return (String -> Eval String) -> String -> Eval String
forall a b. (a -> b) -> a -> b
$ String -> String
escape String
unm
  where genSym :: t String -> String -> String
genSym t String
bad String
nm
          | String
nm String -> t String -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` t String
bad = [String] -> String
forall a. [a] -> a
head [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 (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [String]
S.smtLibReservedNames
          = if Bool -> Bool
not (String -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null String
nm) Bool -> Bool -> Bool
&& Char -> Bool
isUpper (String -> Char
forall a. [a] -> a
head 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 -> Char
forall a. [a] -> a
head 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
forall a. [a] -> [a]
tail 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

-- | 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'
                    [SKind]
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)
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
                    SKind
resK  <- Type -> Eval SKind
getComposite Type
res
                    SKind -> Eval SKind
forall (m :: * -> *) a. Monad m => a -> m a
return (SKind -> Eval SKind) -> SKind -> Eval SKind
forall a b. (a -> b) -> a -> b
$ [Var] -> SKind -> SKind
forall {t :: * -> *}. Foldable t => t Var -> SKind -> SKind
wrap [Var]
tvs (SKind -> SKind) -> SKind -> SKind
forall a b. (a -> b) -> a -> b
$ (SKind -> SKind -> SKind) -> SKind -> [SKind] -> SKind
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr SKind -> SKind -> SKind
KFun SKind
resK [SKind]
argKs
 where wrap :: t Var -> SKind -> SKind
wrap t Var
ts SKind
f         = (Var -> SKind -> SKind) -> SKind -> t Var -> SKind
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 (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)
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 (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 (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{Map TCKey Kind
tcMap :: Env -> Map TCKey Kind
tcMap :: Map TCKey Kind
tcMap} <- ReaderT Env Symbolic Env
forall r (m :: * -> *). MonadReader r m => m r
ask
               case Maybe (TyCon, [Type]) -> Maybe TCKey
grabTCs (HasDebugCallStack => Type -> Maybe (TyCon, [Type])
Type -> Maybe (TyCon, [Type])
splitTyConApp_maybe Type
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 (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 [TyCon]
as <- [Type] -> [TyCon] -> Maybe [TyCon]
walk [Type]
ts []
                                             TCKey -> Maybe TCKey
forall (m :: * -> *) a. Monad m => a -> m a
return (TCKey -> Maybe TCKey) -> TCKey -> Maybe TCKey
forall a b. (a -> b) -> a -> b
$ (TyCon, [TyCon]) -> TCKey
TCKey (TyCon
top, [TyCon]
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{DynFlags
flags :: DynFlags
flags :: Env -> DynFlags
flags, IORef [(Type, Kind)]
rUITypes :: Env -> IORef [(Type, Kind)]
rUITypes :: IORef [(Type, Kind)]
rUITypes} <- ReaderT Env Symbolic Env
forall r (m :: * -> *). MonadReader r m => m r
ask
                            [(Type, Kind)]
uiTypes <- IO [(Type, Kind)] -> ReaderT Env Symbolic [(Type, Kind)]
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (IO [(Type, Kind)] -> ReaderT Env Symbolic [(Type, Kind)])
-> IO [(Type, Kind)] -> ReaderT Env Symbolic [(Type, Kind)]
forall a b. (a -> b) -> a -> b
$ IORef [(Type, Kind)] -> IO [(Type, Kind)]
forall a. IORef a -> IO a
readIORef IORef [(Type, Kind)]
rUITypes
                            case [Kind
k | (Type
bt', Kind
k) <- [(Type, Kind)]
uiTypes, Type
bt Type -> Type -> Bool
`eqType` Type
bt'] of
                              Kind
k:[Kind]
_ -> Kind -> ReaderT Env Symbolic Kind
forall (m :: * -> *) a. Monad m => a -> m a
return Kind
k
                              []  -> do String
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 :: Kind
k = String -> Maybe [String] -> Kind
S.KUserSort String
nm Maybe [String]
forall a. Maybe a
Nothing
                                        IO () -> ReaderT Env Symbolic ()
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (IO () -> ReaderT Env Symbolic ())
-> IO () -> ReaderT Env Symbolic ()
forall a b. (a -> b) -> a -> b
$ IORef [(Type, Kind)] -> ([(Type, Kind)] -> [(Type, Kind)]) -> IO ()
forall a. IORef a -> (a -> a) -> IO ()
modifyIORef IORef [(Type, Kind)]
rUITypes ((Type
bt, Kind
k) (Type, Kind) -> [(Type, Kind)] -> [(Type, Kind)]
forall a. a -> [a] -> [a]
:)
                                        Kind -> ReaderT Env Symbolic Kind
forall (m :: * -> *) a. Monad m => a -> m a
return Kind
k

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