{-# 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
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 :: 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 :: 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
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"
[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
S.ProofError{} -> Bool
False
S.SatExtField{} -> Bool
False
S.DeltaSat{} -> Bool
False
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
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
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)
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)
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
[(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))
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)
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
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
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
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
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)
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)
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" []
walk (Alt AltCon
p [Var]
bs CoreExpr
rhs : [Alt Var]
rest) =
do
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
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
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
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 :: Scaled a -> a
unScale :: forall a. Scaled a -> a
unScale (Scaled Type
_ a
a) = a
a
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)
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
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
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
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
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
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) #-}