{-# LANGUAGE MagicHash #-}
{-# LANGUAGE NamedFieldPuns #-}
{-# LANGUAGE TemplateHaskell #-}
{-# OPTIONS_GHC -Wall -Werror #-}
module Data.SBV.Plugin.Env (buildTCEnv, buildFunEnv, buildDests, buildSpecials, uninterestingTypes) where
import GHC.Plugins
import GHC.Prim
import GHC.Types hiding (Type, TyCon)
import GHC.Types.TyThing
import GHC.Unit.Finder
import GHC.Iface.Env
import qualified Data.Map as M
import qualified Language.Haskell.TH as TH
import Control.Monad.Reader
import Data.Int
import Data.Word
import Data.Bits
import Data.Maybe (fromMaybe, isJust)
import Data.Ratio
import qualified Data.SBV as S
import qualified Data.SBV.Dynamic as S
import Data.SBV.Plugin.Common
supportTupleSizes :: [Int]
supportTupleSizes :: [Int]
supportTupleSizes = [Int
2 .. Int
15]
buildTCEnv :: Int -> CoreM (M.Map TCKey S.Kind)
buildTCEnv :: Int -> CoreM (Map TCKey Kind)
buildTCEnv Int
wsz = do [((TyCon, [TyCon]), Kind)]
xs <- ((Name, Kind) -> CoreM ((TyCon, [TyCon]), Kind))
-> [(Name, Kind)] -> CoreM [((TyCon, [TyCon]), Kind)]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM (Name, Kind) -> CoreM ((TyCon, [TyCon]), Kind)
forall {b}. (Name, b) -> CoreM ((TyCon, [TyCon]), b)
grabTyCon [(Name, Kind)]
basics
[((TyCon, [TyCon]), Kind)]
ys <- ((Name, [Name], Kind) -> CoreM ((TyCon, [TyCon]), Kind))
-> [(Name, [Name], Kind)] -> CoreM [((TyCon, [TyCon]), Kind)]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM (Name, [Name], Kind) -> CoreM ((TyCon, [TyCon]), Kind)
forall {t :: * -> *} {b}.
Traversable t =>
(Name, t Name, b) -> CoreM ((TyCon, t TyCon), b)
grabTyApp [(Name, [Name], Kind)]
apps
Map TCKey Kind -> CoreM (Map TCKey Kind)
forall (m :: * -> *) a. Monad m => a -> m a
return (Map TCKey Kind -> CoreM (Map TCKey Kind))
-> Map TCKey Kind -> CoreM (Map TCKey Kind)
forall a b. (a -> b) -> a -> b
$ [(TCKey, Kind)] -> Map TCKey Kind
forall k a. Ord k => [(k, a)] -> Map k a
M.fromList [((TyCon, [TyCon]) -> TCKey
TCKey (TyCon, [TyCon])
k, Kind
v) | ((TyCon, [TyCon])
k, Kind
v) <- [((TyCon, [TyCon]), Kind)]
xs [((TyCon, [TyCon]), Kind)]
-> [((TyCon, [TyCon]), Kind)] -> [((TyCon, [TyCon]), Kind)]
forall a. [a] -> [a] -> [a]
++ [((TyCon, [TyCon]), Kind)]
ys]
where grab :: Name -> CoreM TyCon
grab = (Name -> CoreM TyCon) -> Name -> CoreM TyCon
forall b. (Name -> CoreM b) -> Name -> CoreM b
grabTH Name -> CoreM TyCon
forall (m :: * -> *). MonadThings m => Name -> m TyCon
lookupTyCon
grabTyCon :: (Name, b) -> CoreM ((TyCon, [TyCon]), b)
grabTyCon (Name
x, b
k) = (Name, [Name], b) -> CoreM ((TyCon, [TyCon]), b)
forall {t :: * -> *} {b}.
Traversable t =>
(Name, t Name, b) -> CoreM ((TyCon, t TyCon), b)
grabTyApp (Name
x, [], b
k)
grabTyApp :: (Name, t Name, b) -> CoreM ((TyCon, t TyCon), b)
grabTyApp (Name
x, t Name
as, b
k) = do TyCon
fn <- Name -> CoreM TyCon
grab Name
x
t TyCon
args <- (Name -> CoreM TyCon) -> t Name -> CoreM (t TyCon)
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM Name -> CoreM TyCon
grab t Name
as
((TyCon, t TyCon), b) -> CoreM ((TyCon, t TyCon), b)
forall (m :: * -> *) a. Monad m => a -> m a
return ((TyCon
fn, t TyCon
args), b
k)
basics :: [(Name, Kind)]
basics = [[(Name, Kind)]] -> [(Name, Kind)]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat [ [(Name
t, Kind
S.KBool) | Name
t <- [''Bool ]]
, [(Name
t, Kind
S.KUnbounded) | Name
t <- [''Integer ]]
, [(Name
t, Kind
S.KFloat) | Name
t <- [''Float, ''Float# ]]
, [(Name
t, Kind
S.KDouble) | Name
t <- [''Double, ''Double#]]
, [(Name
t, Bool -> Int -> Kind
S.KBounded Bool
True Int
wsz) | Name
t <- [''Int, ''Int# ]]
, [(Name
t, Bool -> Int -> Kind
S.KBounded Bool
True Int
8) | Name
t <- [''Int8 ]]
, [(Name
t, Bool -> Int -> Kind
S.KBounded Bool
True Int
16) | Name
t <- [''Int16 ]]
, [(Name
t, Bool -> Int -> Kind
S.KBounded Bool
True Int
32) | Name
t <- [''Int32, ''Int32# ]]
, [(Name
t, Bool -> Int -> Kind
S.KBounded Bool
True Int
64) | Name
t <- [''Int64, ''Int64# ]]
, [(Name
t, Bool -> Int -> Kind
S.KBounded Bool
False Int
wsz) | Name
t <- [''Word, ''Word# ]]
, [(Name
t, Bool -> Int -> Kind
S.KBounded Bool
False Int
8) | Name
t <- [''Word8 ]]
, [(Name
t, Bool -> Int -> Kind
S.KBounded Bool
False Int
16) | Name
t <- [''Word16 ]]
, [(Name
t, Bool -> Int -> Kind
S.KBounded Bool
False Int
32) | Name
t <- [''Word32, ''Word32#]]
, [(Name
t, Bool -> Int -> Kind
S.KBounded Bool
False Int
64) | Name
t <- [''Word64, ''Word64#]]
]
apps :: [(Name, [Name], Kind)]
apps = [ (''Ratio, [''Integer], Kind
S.KReal) ]
buildFunEnv :: Int -> CoreM (M.Map (Id, SKind) Val)
buildFunEnv :: Int -> CoreM (Map (Id, SKind) Val)
buildFunEnv Int
wsz = [((Id, SKind), Val)] -> Map (Id, SKind) Val
forall k a. Ord k => [(k, a)] -> Map k a
M.fromList ([((Id, SKind), Val)] -> Map (Id, SKind) Val)
-> CoreM [((Id, SKind), Val)] -> CoreM (Map (Id, SKind) Val)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
`fmap` ((Name, SKind, Val) -> CoreM ((Id, SKind), Val))
-> [(Name, SKind, Val)] -> CoreM [((Id, SKind), Val)]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM (Name, SKind, Val) -> CoreM ((Id, SKind), Val)
forall a b. (Name, a, b) -> CoreM ((Id, a), b)
thToGHC (Int -> [(Name, SKind, Val)]
basicFuncs Int
wsz [(Name, SKind, Val)]
-> [(Name, SKind, Val)] -> [(Name, SKind, Val)]
forall a. [a] -> [a] -> [a]
++ Int -> [(Name, SKind, Val)]
symFuncs Int
wsz)
basicFuncs :: Int -> [(TH.Name, SKind, Val)]
basicFuncs :: Int -> [(Name, SKind, Val)]
basicFuncs Int
wsz = [ ('F#, SKind -> SKind
tlift1 (Kind -> SKind
KBase Kind
S.KFloat), Maybe String -> (Val -> Eval Val) -> Val
Func Maybe String
forall a. Maybe a
Nothing Val -> Eval Val
forall (m :: * -> *) a. Monad m => a -> m a
return)
, ('D#, SKind -> SKind
tlift1 (Kind -> SKind
KBase Kind
S.KDouble), Maybe String -> (Val -> Eval Val) -> Val
Func Maybe String
forall a. Maybe a
Nothing Val -> Eval Val
forall (m :: * -> *) a. Monad m => a -> m a
return)
, ('I#, SKind -> SKind
tlift1 (Kind -> SKind
KBase (Bool -> Int -> Kind
S.KBounded Bool
True Int
wsz)), Maybe String -> (Val -> Eval Val) -> Val
Func Maybe String
forall a. Maybe a
Nothing Val -> Eval Val
forall (m :: * -> *) a. Monad m => a -> m a
return)
, ('W#, SKind -> SKind
tlift1 (Kind -> SKind
KBase (Bool -> Int -> Kind
S.KBounded Bool
False Int
wsz)), Maybe String -> (Val -> Eval Val) -> Val
Func Maybe String
forall a. Maybe a
Nothing Val -> Eval Val
forall (m :: * -> *) a. Monad m => a -> m a
return)
, ('True, Kind -> SKind
KBase Kind
S.KBool, SVal -> Val
Base SVal
S.svTrue)
, ('False, Kind -> SKind
KBase Kind
S.KBool, SVal -> Val
Base SVal
S.svFalse)
, ('(&&), SKind -> SKind
tlift2 (Kind -> SKind
KBase Kind
S.KBool), (SVal -> SVal -> SVal) -> Val
lift2 SVal -> SVal -> SVal
S.svAnd)
, ('(||), SKind -> SKind
tlift2 (Kind -> SKind
KBase Kind
S.KBool), (SVal -> SVal -> SVal) -> Val
lift2 SVal -> SVal -> SVal
S.svOr)
, ('not, SKind -> SKind
tlift1 (Kind -> SKind
KBase Kind
S.KBool), (SVal -> SVal) -> Val
lift1 SVal -> SVal
S.svNot)
]
symFuncs :: Int -> [(TH.Name, SKind, Val)]
symFuncs :: Int -> [(Name, SKind, Val)]
symFuncs Int
wsz =
[(Name
op, SKind -> SKind
tlift2Bool (Kind -> SKind
KBase Kind
k), (SVal -> SVal -> SVal) -> Val
lift2 SVal -> SVal -> SVal
sOp) | Kind
k <- [Kind]
allKinds, (Name
op, SVal -> SVal -> SVal
sOp) <- [('(==), SVal -> SVal -> SVal
S.svEqual), ('(/=), SVal -> SVal -> SVal
S.svNotEqual)]]
[(Name, SKind, Val)]
-> [(Name, SKind, Val)] -> [(Name, SKind, Val)]
forall a. [a] -> [a] -> [a]
++ [(Name
op, SKind -> SKind
tlift1 (Kind -> SKind
KBase Kind
k), (SVal -> SVal) -> Val
lift1 SVal -> SVal
sOp) | Kind
k <- [Kind]
arithKinds, (Name
op, SVal -> SVal
sOp) <- [(Name, SVal -> SVal)]
unaryOps]
[(Name, SKind, Val)]
-> [(Name, SKind, Val)] -> [(Name, SKind, Val)]
forall a. [a] -> [a] -> [a]
++ [(Name
op, SKind -> SKind
tlift2 (Kind -> SKind
KBase Kind
k), (SVal -> SVal -> SVal) -> Val
lift2 SVal -> SVal -> SVal
sOp) | Kind
k <- [Kind]
arithKinds, (Name
op, SVal -> SVal -> SVal
sOp) <- [(Name, SVal -> SVal -> SVal)]
binaryOps]
[(Name, SKind, Val)]
-> [(Name, SKind, Val)] -> [(Name, SKind, Val)]
forall a. [a] -> [a] -> [a]
++ [(Name
op, SKind -> SKind -> SKind
KFun (Kind -> SKind
KBase Kind
S.KUnbounded) (Kind -> SKind
KBase Kind
k), (Integer -> SVal) -> Val
lift1Int Integer -> SVal
sOp) | Kind
k <- [Kind]
integerKinds, (Name
op, Integer -> SVal
sOp) <- [('fromInteger, Kind -> Integer -> SVal
S.svInteger Kind
k)]]
[(Name, SKind, Val)]
-> [(Name, SKind, Val)] -> [(Name, SKind, Val)]
forall a. [a] -> [a] -> [a]
++ [(Name
op, SKind -> SKind
tlift2Bool (Kind -> SKind
KBase Kind
k), (SVal -> SVal -> SVal) -> Val
lift2 SVal -> SVal -> SVal
sOp) | Kind
k <- [Kind]
arithKinds, (Name
op, SVal -> SVal -> SVal
sOp) <- [(Name, SVal -> SVal -> SVal)]
compOps ]
[(Name, SKind, Val)]
-> [(Name, SKind, Val)] -> [(Name, SKind, Val)]
forall a. [a] -> [a] -> [a]
++ [(Name
op, SKind -> SKind
tlift2 (Kind -> SKind
KBase Kind
k), (SVal -> SVal -> SVal) -> Val
lift2 SVal -> SVal -> SVal
sOp) | Kind
k <- [Kind]
integralKinds, (Name
op, SVal -> SVal -> SVal
sOp) <- [('div, SVal -> SVal -> SVal
S.svDivide), ('quot, SVal -> SVal -> SVal
S.svQuot), ('rem, SVal -> SVal -> SVal
S.svRem)]]
[(Name, SKind, Val)]
-> [(Name, SKind, Val)] -> [(Name, SKind, Val)]
forall a. [a] -> [a] -> [a]
++ [ (Name
op, SKind -> SKind
tlift2 (Kind -> SKind
KBase Kind
k), (SVal -> SVal -> SVal) -> Val
lift2 SVal -> SVal -> SVal
sOp) | Kind
k <- [Kind]
bvKinds, (Name
op, SVal -> SVal -> SVal
sOp) <- [(Name, SVal -> SVal -> SVal)]
bvBinOps ]
[(Name, SKind, Val)]
-> [(Name, SKind, Val)] -> [(Name, SKind, Val)]
forall a. [a] -> [a] -> [a]
++ [ (Name
op, Int -> SKind -> SKind
tlift2ShRot Int
wsz (Kind -> SKind
KBase Kind
k), (SVal -> SVal -> SVal) -> Val
lift2 SVal -> SVal -> SVal
sOp) | Kind
k <- [Kind]
bvKinds, (Name
op, SVal -> SVal -> SVal
sOp) <- [(Name, SVal -> SVal -> SVal)]
bvShiftRots]
[(Name, SKind, Val)]
-> [(Name, SKind, Val)] -> [(Name, SKind, Val)]
forall a. [a] -> [a] -> [a]
++ [ ('enumFromTo, SKind -> SKind
tEnumFromTo (Kind -> SKind
KBase Kind
k), Val
sEnumFromTo) | Kind
k <- [Kind]
arithKinds ]
[(Name, SKind, Val)]
-> [(Name, SKind, Val)] -> [(Name, SKind, Val)]
forall a. [a] -> [a] -> [a]
++ [ ('enumFromThenTo, SKind -> SKind
tEnumFromThenTo (Kind -> SKind
KBase Kind
k), Val
sEnumFromThenTo) | Kind
k <- [Kind]
arithKinds ]
where
bvKinds :: [Kind]
bvKinds = [Bool -> Int -> Kind
S.KBounded Bool
s Int
sz | Bool
s <- [Bool
False, Bool
True], Int
sz <- [Int
8, Int
16, Int
32, Int
64]]
integralKinds :: [Kind]
integralKinds = Kind
S.KUnbounded Kind -> [Kind] -> [Kind]
forall a. a -> [a] -> [a]
: [Kind]
bvKinds
integerKinds :: [Kind]
integerKinds = Kind
S.KReal Kind -> [Kind] -> [Kind]
forall a. a -> [a] -> [a]
: [Kind]
integralKinds
floatKinds :: [Kind]
floatKinds = [Kind
S.KFloat, Kind
S.KDouble]
arithKinds :: [Kind]
arithKinds = [Kind]
floatKinds [Kind] -> [Kind] -> [Kind]
forall a. [a] -> [a] -> [a]
++ [Kind]
integerKinds
allKinds :: [Kind]
allKinds = Kind
S.KBool Kind -> [Kind] -> [Kind]
forall a. a -> [a] -> [a]
: [Kind]
arithKinds
unaryOps :: [(Name, SVal -> SVal)]
unaryOps = [ ('abs, SVal -> SVal
S.svAbs)
, ('negate, SVal -> SVal
S.svUNeg)
, ('complement, SVal -> SVal
S.svNot)
]
binaryOps :: [(Name, SVal -> SVal -> SVal)]
binaryOps = [ ('(+), SVal -> SVal -> SVal
S.svPlus)
, ('(-), SVal -> SVal -> SVal
S.svMinus)
, ('(*), SVal -> SVal -> SVal
S.svTimes)
, ('(/), SVal -> SVal -> SVal
S.svDivide)
, ('(^), SVal -> SVal -> SVal
S.svExp)
, ('quot, SVal -> SVal -> SVal
S.svQuot)
, ('rem, SVal -> SVal -> SVal
S.svRem)
]
compOps :: [(Name, SVal -> SVal -> SVal)]
compOps = [ ('(<), SVal -> SVal -> SVal
S.svLessThan)
, ('(>), SVal -> SVal -> SVal
S.svGreaterThan)
, ('(<=), SVal -> SVal -> SVal
S.svLessEq)
, ('(>=), SVal -> SVal -> SVal
S.svGreaterEq)
]
bvBinOps :: [(Name, SVal -> SVal -> SVal)]
bvBinOps = [ ('(.&.), SVal -> SVal -> SVal
S.svAnd)
, ('(.|.), SVal -> SVal -> SVal
S.svOr)
, ('xor, SVal -> SVal -> SVal
S.svXOr)
]
bvShiftRots :: [(Name, SVal -> SVal -> SVal)]
bvShiftRots = [ ('shiftL, SVal -> SVal -> SVal
S.svShiftLeft)
, ('shiftR, SVal -> SVal -> SVal
S.svShiftRight)
, ('rotateL, SVal -> SVal -> SVal
S.svRotateLeft)
, ('rotateR, SVal -> SVal -> SVal
S.svRotateRight)
]
buildDests :: CoreM (M.Map Var (Val -> [(Var, SKind)] -> (S.SVal, [((Var, SKind), Val)])))
buildDests :: CoreM
(Map Id (Val -> [(Id, SKind)] -> (SVal, [((Id, SKind), Val)])))
buildDests = do [(Id, Val -> [(Id, SKind)] -> (SVal, [((Id, SKind), Val)]))]
simple <- ((Name, Val -> [(Id, SKind)] -> (SVal, [((Id, SKind), Val)]))
-> CoreM
(Id, Val -> [(Id, SKind)] -> (SVal, [((Id, SKind), Val)])))
-> [(Name, Val -> [(Id, SKind)] -> (SVal, [((Id, SKind), Val)]))]
-> CoreM
[(Id, Val -> [(Id, SKind)] -> (SVal, [((Id, SKind), Val)]))]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM (Name, Val -> [(Id, SKind)] -> (SVal, [((Id, SKind), Val)]))
-> CoreM (Id, Val -> [(Id, SKind)] -> (SVal, [((Id, SKind), Val)]))
forall b. (Name, b) -> CoreM (Id, b)
mkSingle [(Name, Val -> [(Id, SKind)] -> (SVal, [((Id, SKind), Val)]))]
forall {a}. [(Name, Val -> [a] -> (SVal, [(a, Val)]))]
dests
[(Id, Val -> [(Id, SKind)] -> (SVal, [((Id, SKind), Val)]))]
tups <- (Int
-> CoreM
(Id, Val -> [(Id, SKind)] -> (SVal, [((Id, SKind), Val)])))
-> [Int]
-> CoreM
[(Id, Val -> [(Id, SKind)] -> (SVal, [((Id, SKind), Val)]))]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM Int
-> CoreM (Id, Val -> [(Id, SKind)] -> (SVal, [((Id, SKind), Val)]))
forall {a}.
Outputable a =>
Int -> CoreM (Id, Val -> [a] -> (SVal, [(a, Val)]))
mkTuple [Int]
supportTupleSizes
(Id, Val -> [(Id, SKind)] -> (SVal, [((Id, SKind), Val)]))
nil <- CoreM (Id, Val -> [(Id, SKind)] -> (SVal, [((Id, SKind), Val)]))
forall {a}. CoreM (Id, Val -> [(Id, SKind)] -> (SVal, [a]))
mkNil
(Id, Val -> [(Id, SKind)] -> (SVal, [((Id, SKind), Val)]))
cons <- CoreM (Id, Val -> [(Id, SKind)] -> (SVal, [((Id, SKind), Val)]))
mkCons
Map Id (Val -> [(Id, SKind)] -> (SVal, [((Id, SKind), Val)]))
-> CoreM
(Map Id (Val -> [(Id, SKind)] -> (SVal, [((Id, SKind), Val)])))
forall (m :: * -> *) a. Monad m => a -> m a
return (Map Id (Val -> [(Id, SKind)] -> (SVal, [((Id, SKind), Val)]))
-> CoreM
(Map Id (Val -> [(Id, SKind)] -> (SVal, [((Id, SKind), Val)]))))
-> Map Id (Val -> [(Id, SKind)] -> (SVal, [((Id, SKind), Val)]))
-> CoreM
(Map Id (Val -> [(Id, SKind)] -> (SVal, [((Id, SKind), Val)])))
forall a b. (a -> b) -> a -> b
$ [(Id, Val -> [(Id, SKind)] -> (SVal, [((Id, SKind), Val)]))]
-> Map Id (Val -> [(Id, SKind)] -> (SVal, [((Id, SKind), Val)]))
forall k a. Ord k => [(k, a)] -> Map k a
M.fromList ([(Id, Val -> [(Id, SKind)] -> (SVal, [((Id, SKind), Val)]))]
simple [(Id, Val -> [(Id, SKind)] -> (SVal, [((Id, SKind), Val)]))]
-> [(Id, Val -> [(Id, SKind)] -> (SVal, [((Id, SKind), Val)]))]
-> [(Id, Val -> [(Id, SKind)] -> (SVal, [((Id, SKind), Val)]))]
forall a. [a] -> [a] -> [a]
++ [(Id, Val -> [(Id, SKind)] -> (SVal, [((Id, SKind), Val)]))]
tups [(Id, Val -> [(Id, SKind)] -> (SVal, [((Id, SKind), Val)]))]
-> [(Id, Val -> [(Id, SKind)] -> (SVal, [((Id, SKind), Val)]))]
-> [(Id, Val -> [(Id, SKind)] -> (SVal, [((Id, SKind), Val)]))]
forall a. [a] -> [a] -> [a]
++ [(Id, Val -> [(Id, SKind)] -> (SVal, [((Id, SKind), Val)]))
nil, (Id, Val -> [(Id, SKind)] -> (SVal, [((Id, SKind), Val)]))
cons])
where
dests :: [(Name, Val -> [a] -> (SVal, [(a, Val)]))]
dests = [ ('W#, Val -> [a] -> (SVal, [(a, Val)])
forall {a} {a}. Outputable a => a -> [a] -> (SVal, [(a, a)])
dest1)
, ('I#, Val -> [a] -> (SVal, [(a, Val)])
forall {a} {a}. Outputable a => a -> [a] -> (SVal, [(a, a)])
dest1)
, ('F#, Val -> [a] -> (SVal, [(a, Val)])
forall {a} {a}. Outputable a => a -> [a] -> (SVal, [(a, a)])
dest1)
, ('D#, Val -> [a] -> (SVal, [(a, Val)])
forall {a} {a}. Outputable a => a -> [a] -> (SVal, [(a, a)])
dest1)
]
dest1 :: a -> [a] -> (SVal, [(a, a)])
dest1 a
a [a
bk] = (SVal
S.svTrue, [(a
bk, a
a)])
dest1 a
a [a]
bs = String -> (SVal, [(a, a)])
forall a. HasCallStack => String -> a
error (String -> (SVal, [(a, a)])) -> String -> (SVal, [(a, a)])
forall a b. (a -> b) -> a -> b
$ String
"Impossible happened: Mistmatched arity case-binder for: " String -> String -> String
forall a. [a] -> [a] -> [a]
++ SDoc -> String
showSDocUnsafe (a -> SDoc
forall a. Outputable a => a -> SDoc
ppr a
a) String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
". Expected 1, got: " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Int -> String
forall a. Show a => a -> String
show ([a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [a]
bs) String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
" arguments."
mkSingle :: (TH.Name, b) -> CoreM (Id, b)
mkSingle :: forall b. (Name, b) -> CoreM (Id, b)
mkSingle (Name
n, b
sfn) = do Id
f <- (Name -> CoreM Id) -> Name -> CoreM Id
forall b. (Name -> CoreM b) -> Name -> CoreM b
grabTH Name -> CoreM Id
forall (m :: * -> *). MonadThings m => Name -> m Id
lookupId Name
n
(Id, b) -> CoreM (Id, b)
forall (m :: * -> *) a. Monad m => a -> m a
return (Id
f, b
sfn)
mkTuple :: Int -> CoreM (Id, Val -> [a] -> (SVal, [(a, Val)]))
mkTuple Int
n = do Id
d <- (Name -> CoreM Id) -> Name -> CoreM Id
forall b. (Name -> CoreM b) -> Name -> CoreM b
grabTH Name -> CoreM Id
forall (m :: * -> *). MonadThings m => Name -> m Id
lookupId (Int -> Name
TH.tupleDataName Int
n)
let dest :: Val -> [a] -> (SVal, [(a, Val)])
dest (Tup [Val]
xs) [a]
bs
| [Val] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [Val]
xs Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
n Bool -> Bool -> Bool
&& [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [a]
bs Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
n
= (SVal
S.svTrue, [a] -> [Val] -> [(a, Val)]
forall a b. [a] -> [b] -> [(a, b)]
zip [a]
bs [Val]
xs)
dest Val
a [a]
b = String -> (SVal, [(a, Val)])
forall a. HasCallStack => String -> a
error (String -> (SVal, [(a, Val)])) -> String -> (SVal, [(a, Val)])
forall a b. (a -> b) -> a -> b
$ String
"Impossible: Tuple-case mismatch: " String -> String -> String
forall a. [a] -> [a] -> [a]
++ SDoc -> String
showSDocUnsafe ((Int, Val, [a]) -> SDoc
forall a. Outputable a => a -> SDoc
ppr (Int
n, Val
a, [a]
b))
(Id, Val -> [a] -> (SVal, [(a, Val)]))
-> CoreM (Id, Val -> [a] -> (SVal, [(a, Val)]))
forall (m :: * -> *) a. Monad m => a -> m a
return (Id
d, Val -> [a] -> (SVal, [(a, Val)])
forall {a}. Outputable a => Val -> [a] -> (SVal, [(a, Val)])
dest)
mkNil :: CoreM (Id, Val -> [(Id, SKind)] -> (SVal, [a]))
mkNil = do Id
d <- Name -> CoreM Id
forall (m :: * -> *). MonadThings m => Name -> m Id
lookupId Name
nilDataConName
let dest :: Val -> [a] -> (SVal, [a])
dest (Lst []) [] = (SVal
S.svTrue, [])
dest (Lst [Val]
_) [a]
_ = (SVal
S.svFalse, [])
dest Val
a [a]
b = String -> (SVal, [a])
forall a. HasCallStack => String -> a
error (String -> (SVal, [a])) -> String -> (SVal, [a])
forall a b. (a -> b) -> a -> b
$ String
"Impossible: []-case mismatch: " String -> String -> String
forall a. [a] -> [a] -> [a]
++ SDoc -> String
showSDocUnsafe ((Val, [a]) -> SDoc
forall a. Outputable a => a -> SDoc
ppr (Val
a, [a]
b))
(Id, Val -> [(Id, SKind)] -> (SVal, [a]))
-> CoreM (Id, Val -> [(Id, SKind)] -> (SVal, [a]))
forall (m :: * -> *) a. Monad m => a -> m a
return (Id
d, Val -> [(Id, SKind)] -> (SVal, [a])
forall {a} {a}. Outputable a => Val -> [a] -> (SVal, [a])
dest)
mkCons :: CoreM (Id, Val -> [(Id, SKind)] -> (SVal, [((Id, SKind), Val)]))
mkCons = do Id
d <- Name -> CoreM Id
forall (m :: * -> *). MonadThings m => Name -> m Id
lookupId Name
consDataConName
let dest :: Val -> [a] -> (SVal, [(a, Val)])
dest (Lst []) [a]
_ = (SVal
S.svFalse, [])
dest (Lst (Val
x:[Val]
xs)) [a
h, a
t] = (SVal
S.svTrue, [(a
h, Val
x), (a
t, [Val] -> Val
Lst [Val]
xs)])
dest Val
a [a]
b = String -> (SVal, [(a, Val)])
forall a. HasCallStack => String -> a
error (String -> (SVal, [(a, Val)])) -> String -> (SVal, [(a, Val)])
forall a b. (a -> b) -> a -> b
$ String
"Impossible: (:)-case mismatch: " String -> String -> String
forall a. [a] -> [a] -> [a]
++ SDoc -> String
showSDocUnsafe ((Val, [a]) -> SDoc
forall a. Outputable a => a -> SDoc
ppr (Val
a, [a]
b))
(Id, Val -> [(Id, SKind)] -> (SVal, [((Id, SKind), Val)]))
-> CoreM (Id, Val -> [(Id, SKind)] -> (SVal, [((Id, SKind), Val)]))
forall (m :: * -> *) a. Monad m => a -> m a
return (Id
d, Val -> [(Id, SKind)] -> (SVal, [((Id, SKind), Val)])
forall {a}. Outputable a => Val -> [a] -> (SVal, [(a, Val)])
dest)
uninterestingTypes :: CoreM [Type]
uninterestingTypes :: CoreM [Type]
uninterestingTypes = (Id -> Type) -> [Id] -> [Type]
forall a b. (a -> b) -> [a] -> [b]
map Id -> Type
varType ([Id] -> [Type]) -> CoreM [Id] -> CoreM [Type]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
`fmap` (Name -> CoreM Id) -> [Name] -> CoreM [Id]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM ((Name -> CoreM Id) -> Name -> CoreM Id
forall b. (Name -> CoreM b) -> Name -> CoreM b
grabTH Name -> CoreM Id
forall (m :: * -> *). MonadThings m => Name -> m Id
lookupId) ['void#]
buildSpecials :: CoreM Specials
buildSpecials :: CoreM Specials
buildSpecials = do Id -> Maybe Val
isEq <- do Id
eq <- (Name -> CoreM Id) -> Name -> CoreM Id
forall b. (Name -> CoreM b) -> Name -> CoreM b
grabTH Name -> CoreM Id
forall (m :: * -> *). MonadThings m => Name -> m Id
lookupId '(==)
Id
neq <- (Name -> CoreM Id) -> Name -> CoreM Id
forall b. (Name -> CoreM b) -> Name -> CoreM b
grabTH Name -> CoreM Id
forall (m :: * -> *). MonadThings m => Name -> m Id
lookupId '(/=)
let choose :: [(Id, Val)]
choose = [(Id
eq, (SVal -> SVal -> SVal) -> Val
liftEq SVal -> SVal -> SVal
S.svEqual), (Id
neq, (SVal -> SVal -> SVal) -> Val
liftEq SVal -> SVal -> SVal
S.svNotEqual)]
(Id -> Maybe Val) -> CoreM (Id -> Maybe Val)
forall (m :: * -> *) a. Monad m => a -> m a
return (Id -> [(Id, Val)] -> Maybe Val
forall a b. Eq a => a -> [(a, b)] -> Maybe b
`lookup` [(Id, Val)]
choose)
Id -> Maybe Val
isTup <- do let mkTup :: p -> Val
mkTup p
n = Maybe String -> (Val -> Eval Val) -> Val
Func Maybe String
forall a. Maybe a
Nothing Val -> Eval Val
g
where g :: Val -> Eval Val
g (Typ SKind
_) = Val -> Eval Val
forall (m :: * -> *) a. Monad m => a -> m a
return (Val -> Eval Val) -> Val -> Eval Val
forall a b. (a -> b) -> a -> b
$ Maybe String -> (Val -> Eval Val) -> Val
Func Maybe String
forall a. Maybe a
Nothing Val -> Eval Val
g
g Val
v = p -> [Val] -> Eval Val
forall {t}. (Eq t, Num t) => t -> [Val] -> Eval Val
h (p
np -> p -> p
forall a. Num a => a -> a -> a
-p
1) [Val
v]
h :: t -> [Val] -> Eval Val
h t
0 [Val]
sofar = Val -> Eval Val
forall (m :: * -> *) a. Monad m => a -> m a
return (Val -> Eval Val) -> Val -> Eval Val
forall a b. (a -> b) -> a -> b
$ [Val] -> Val
Tup ([Val] -> [Val]
forall a. [a] -> [a]
reverse [Val]
sofar)
h t
i [Val]
sofar = Val -> Eval Val
forall (m :: * -> *) a. Monad m => a -> m a
return (Val -> Eval Val) -> Val -> Eval Val
forall a b. (a -> b) -> a -> b
$ Maybe String -> (Val -> Eval Val) -> Val
Func Maybe String
forall a. Maybe a
Nothing ((Val -> Eval Val) -> Val) -> (Val -> Eval Val) -> Val
forall a b. (a -> b) -> a -> b
$ \Val
v -> t -> [Val] -> Eval Val
h (t
it -> t -> t
forall a. Num a => a -> a -> a
-t
1) (Val
vVal -> [Val] -> [Val]
forall a. a -> [a] -> [a]
:[Val]
sofar)
[Id]
ts <- (Int -> CoreM Id) -> [Int] -> CoreM [Id]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM ((Name -> CoreM Id) -> Name -> CoreM Id
forall b. (Name -> CoreM b) -> Name -> CoreM b
grabTH Name -> CoreM Id
forall (m :: * -> *). MonadThings m => Name -> m Id
lookupId (Name -> CoreM Id) -> (Int -> Name) -> Int -> CoreM Id
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Int -> Name
TH.tupleDataName) [Int]
supportTupleSizes
let choose :: [(Id, Val)]
choose = [Id] -> [Val] -> [(Id, Val)]
forall a b. [a] -> [b] -> [(a, b)]
zip [Id]
ts ((Int -> Val) -> [Int] -> [Val]
forall a b. (a -> b) -> [a] -> [b]
map Int -> Val
forall {p}. (Eq p, Num p) => p -> Val
mkTup [Int]
supportTupleSizes)
(Id -> Maybe Val) -> CoreM (Id -> Maybe Val)
forall (m :: * -> *) a. Monad m => a -> m a
return (Id -> [(Id, Val)] -> Maybe Val
forall a b. Eq a => a -> [(a, b)] -> Maybe b
`lookup` [(Id, Val)]
choose)
Id -> Maybe Val
isLst <- do Id
nil <- Name -> CoreM Id
forall (m :: * -> *). MonadThings m => Name -> m Id
lookupId Name
nilDataConName
Id
cons <- Name -> CoreM Id
forall (m :: * -> *). MonadThings m => Name -> m Id
lookupId Name
consDataConName
let snil :: Val
snil = [Val] -> Val
Lst []
scons :: Val
scons = Maybe String -> (Val -> Eval Val) -> Val
Func Maybe String
forall a. Maybe a
Nothing Val -> Eval Val
g
where g :: Val -> Eval Val
g (Typ SKind
_) = Val -> Eval Val
forall (m :: * -> *) a. Monad m => a -> m a
return (Val -> Eval Val) -> Val -> Eval Val
forall a b. (a -> b) -> a -> b
$ Maybe String -> (Val -> Eval Val) -> Val
Func Maybe String
forall a. Maybe a
Nothing Val -> Eval Val
g
g Val
v = Val -> Eval Val
forall (m :: * -> *) a. Monad m => a -> m a
return (Val -> Eval Val) -> Val -> Eval Val
forall a b. (a -> b) -> a -> b
$ Maybe String -> (Val -> Eval Val) -> Val
Func Maybe String
forall a. Maybe a
Nothing (Val -> Val -> Eval Val
forall {m :: * -> *}. Monad m => Val -> Val -> m Val
k Val
v)
k :: Val -> Val -> m Val
k Val
v (Lst [Val]
xs) = Val -> m Val
forall (m :: * -> *) a. Monad m => a -> m a
return ([Val] -> Val
Lst (Val
vVal -> [Val] -> [Val]
forall a. a -> [a] -> [a]
:[Val]
xs))
k Val
v Val
a = String -> m Val
forall a. HasCallStack => String -> a
error (String -> m Val) -> String -> m Val
forall a b. (a -> b) -> a -> b
$ String
"Impossible: (:) received incompatible arguments: " String -> String -> String
forall a. [a] -> [a] -> [a]
++ SDoc -> String
showSDocUnsafe ((Val, Val) -> SDoc
forall a. Outputable a => a -> SDoc
ppr (Val
v, Val
a))
choose :: [(Id, Val)]
choose = [(Id
nil, Val
snil), (Id
cons, Val
scons)]
(Id -> Maybe Val) -> CoreM (Id -> Maybe Val)
forall (m :: * -> *) a. Monad m => a -> m a
return (Id -> [(Id, Val)] -> Maybe Val
forall a b. Eq a => a -> [(a, b)] -> Maybe b
`lookup` [(Id, Val)]
choose)
Specials -> CoreM Specials
forall (m :: * -> *) a. Monad m => a -> m a
return Specials{ isEquality :: Id -> Maybe Val
isEquality = Id -> Maybe Val
isEq
, isTuple :: Id -> Maybe Val
isTuple = Id -> Maybe Val
isTup
, isList :: Id -> Maybe Val
isList = Id -> Maybe Val
isLst
}
tlift2Bool :: SKind -> SKind
tlift2Bool :: SKind -> SKind
tlift2Bool SKind
k = SKind -> SKind -> SKind
KFun SKind
k (SKind -> SKind -> SKind
KFun SKind
k (Kind -> SKind
KBase Kind
S.KBool))
tlift1 :: SKind -> SKind
tlift1 :: SKind -> SKind
tlift1 SKind
k = SKind -> SKind -> SKind
KFun SKind
k SKind
k
tlift2 :: SKind -> SKind
tlift2 :: SKind -> SKind
tlift2 SKind
k = SKind -> SKind -> SKind
KFun SKind
k (SKind -> SKind
tlift1 SKind
k)
tlift2ShRot :: Int -> SKind -> SKind
tlift2ShRot :: Int -> SKind -> SKind
tlift2ShRot Int
wsz SKind
k = SKind -> SKind -> SKind
KFun SKind
k (SKind -> SKind -> SKind
KFun (Kind -> SKind
KBase (Bool -> Int -> Kind
S.KBounded Bool
True Int
wsz)) SKind
k)
tEnumFromTo :: SKind -> SKind
tEnumFromTo :: SKind -> SKind
tEnumFromTo SKind
a = SKind -> SKind -> SKind
KFun SKind
a (SKind -> SKind -> SKind
KFun SKind
a (SKind -> SKind
KLst SKind
a))
tEnumFromThenTo :: SKind -> SKind
tEnumFromThenTo :: SKind -> SKind
tEnumFromThenTo SKind
a = SKind -> SKind -> SKind
KFun SKind
a (SKind -> SKind -> SKind
KFun SKind
a (SKind -> SKind -> SKind
KFun SKind
a (SKind -> SKind
KLst SKind
a)))
lift1Int :: (Integer -> S.SVal) -> Val
lift1Int :: (Integer -> SVal) -> Val
lift1Int Integer -> SVal
f = Maybe String -> (Val -> Eval Val) -> Val
Func Maybe String
forall a. Maybe a
Nothing Val -> Eval Val
forall {m :: * -> *}. Monad m => Val -> m Val
g
where g :: Val -> m Val
g (Base SVal
i) = Val -> m Val
forall (m :: * -> *) a. Monad m => a -> m a
return (Val -> m Val) -> Val -> m Val
forall a b. (a -> b) -> a -> b
$ SVal -> Val
Base (SVal -> Val) -> SVal -> Val
forall a b. (a -> b) -> a -> b
$ Integer -> SVal
f (Integer -> Maybe Integer -> Integer
forall a. a -> Maybe a -> a
fromMaybe (String -> Integer
forall a. HasCallStack => String -> a
error (String
"Cannot extract an integer from value: " String -> String -> String
forall a. [a] -> [a] -> [a]
++ SVal -> String
forall a. Show a => a -> String
show SVal
i)) (SVal -> Maybe Integer
S.svAsInteger SVal
i))
g Val
_ = String -> m Val
forall a. HasCallStack => String -> a
error String
"Impossible happened: lift1Int received non-base argument!"
lift1 :: (S.SVal -> S.SVal) -> Val
lift1 :: (SVal -> SVal) -> Val
lift1 SVal -> SVal
f = Maybe String -> (Val -> Eval Val) -> Val
Func Maybe String
forall a. Maybe a
Nothing Val -> Eval Val
forall {m :: * -> *}. Monad m => Val -> m Val
g
where g :: Val -> m Val
g (Typ SKind
_) = Val -> m Val
forall (m :: * -> *) a. Monad m => a -> m a
return (Val -> m Val) -> Val -> m Val
forall a b. (a -> b) -> a -> b
$ Maybe String -> (Val -> Eval Val) -> Val
Func Maybe String
forall a. Maybe a
Nothing Val -> Eval Val
forall {m :: * -> *}. Monad m => Val -> m Val
h
g Val
v = Val -> m Val
forall {m :: * -> *}. Monad m => Val -> m Val
h Val
v
h :: Val -> m Val
h (Base SVal
a) = Val -> m Val
forall (m :: * -> *) a. Monad m => a -> m a
return (Val -> m Val) -> Val -> m Val
forall a b. (a -> b) -> a -> b
$ SVal -> Val
Base (SVal -> Val) -> SVal -> Val
forall a b. (a -> b) -> a -> b
$ SVal -> SVal
f SVal
a
h Val
v = String -> m Val
forall a. HasCallStack => String -> a
error (String -> m Val) -> String -> m Val
forall a b. (a -> b) -> a -> b
$ String
"Impossible happened: lift1 received non-base argument: " String -> String -> String
forall a. [a] -> [a] -> [a]
++ SDoc -> String
showSDocUnsafe (Val -> SDoc
forall a. Outputable a => a -> SDoc
ppr Val
v)
lift2 :: (S.SVal -> S.SVal -> S.SVal) -> Val
lift2 :: (SVal -> SVal -> SVal) -> Val
lift2 SVal -> SVal -> SVal
f = Maybe String -> (Val -> Eval Val) -> Val
Func Maybe String
forall a. Maybe a
Nothing Val -> Eval Val
forall {m :: * -> *}. Monad m => Val -> m Val
g
where g :: Val -> m Val
g (Typ SKind
_) = Val -> m Val
forall (m :: * -> *) a. Monad m => a -> m a
return (Val -> m Val) -> Val -> m Val
forall a b. (a -> b) -> a -> b
$ Maybe String -> (Val -> Eval Val) -> Val
Func Maybe String
forall a. Maybe a
Nothing Val -> Eval Val
forall {m :: * -> *}. Monad m => Val -> m Val
h
g Val
v = Val -> m Val
forall {m :: * -> *}. Monad m => Val -> m Val
h Val
v
h :: Val -> m Val
h (Base SVal
a) = Val -> m Val
forall (m :: * -> *) a. Monad m => a -> m a
return (Val -> m Val) -> Val -> m Val
forall a b. (a -> b) -> a -> b
$ Maybe String -> (Val -> Eval Val) -> Val
Func Maybe String
forall a. Maybe a
Nothing (SVal -> Val -> Eval Val
forall {m :: * -> *}. Monad m => SVal -> Val -> m Val
k SVal
a)
h Val
v = String -> m Val
forall a. HasCallStack => String -> a
error (String -> m Val) -> String -> m Val
forall a b. (a -> b) -> a -> b
$ String
"Impossible happened: lift2 received non-base argument (h): " String -> String -> String
forall a. [a] -> [a] -> [a]
++ SDoc -> String
showSDocUnsafe (Val -> SDoc
forall a. Outputable a => a -> SDoc
ppr Val
v)
k :: SVal -> Val -> m Val
k SVal
a (Base SVal
b) = Val -> m Val
forall (m :: * -> *) a. Monad m => a -> m a
return (Val -> m Val) -> Val -> m Val
forall a b. (a -> b) -> a -> b
$ SVal -> Val
Base (SVal -> Val) -> SVal -> Val
forall a b. (a -> b) -> a -> b
$ SVal -> SVal -> SVal
f SVal
a SVal
b
k SVal
_ Val
v = String -> m Val
forall a. HasCallStack => String -> a
error (String -> m Val) -> String -> m Val
forall a b. (a -> b) -> a -> b
$ String
"Impossible happened: lift2 received non-base argument (k): " String -> String -> String
forall a. [a] -> [a] -> [a]
++ SDoc -> String
showSDocUnsafe (Val -> SDoc
forall a. Outputable a => a -> SDoc
ppr Val
v)
liftEq :: (S.SVal -> S.SVal -> S.SVal) -> Val
liftEq :: (SVal -> SVal -> SVal) -> Val
liftEq SVal -> SVal -> SVal
baseEq = Maybe String -> (Val -> Eval Val) -> Val
Func Maybe String
forall a. Maybe a
Nothing Val -> Eval Val
g
where g :: Val -> Eval Val
g (Typ SKind
_) = Val -> Eval Val
forall (m :: * -> *) a. Monad m => a -> m a
return (Val -> Eval Val) -> Val -> Eval Val
forall a b. (a -> b) -> a -> b
$ Maybe String -> (Val -> Eval Val) -> Val
Func Maybe String
forall a. Maybe a
Nothing Val -> Eval Val
g
g Val
v1 = Val -> Eval Val
forall (m :: * -> *) a. Monad m => a -> m a
return (Val -> Eval Val) -> Val -> Eval Val
forall a b. (a -> b) -> a -> b
$ Maybe String -> (Val -> Eval Val) -> Val
Func Maybe String
forall a. Maybe a
Nothing ((Val -> Eval Val) -> Val) -> (Val -> Eval Val) -> Val
forall a b. (a -> b) -> a -> b
$ \Val
v2 -> Val -> Eval Val
forall (m :: * -> *) a. Monad m => a -> m a
return (Val -> Eval Val) -> Val -> Eval Val
forall a b. (a -> b) -> a -> b
$ SVal -> Val
Base (SVal -> Val) -> SVal -> Val
forall a b. (a -> b) -> a -> b
$ (SVal -> SVal -> SVal) -> Val -> Val -> SVal
liftEqVal SVal -> SVal -> SVal
baseEq Val
v1 Val
v2
sEnumFromTo :: Val
sEnumFromTo :: Val
sEnumFromTo = Maybe String -> (Val -> Eval Val) -> Val
Func Maybe String
forall a. Maybe a
Nothing ([Val] -> Val -> Eval Val
g [])
where g :: [Val] -> Val -> Eval Val
g [Val
x] Val
y = Val -> Maybe Val -> Val -> Eval Val
enumList Val
x Maybe Val
forall a. Maybe a
Nothing Val
y
g [Val]
args (Typ SKind
_) = Val -> Eval Val
forall (m :: * -> *) a. Monad m => a -> m a
return (Val -> Eval Val) -> Val -> Eval Val
forall a b. (a -> b) -> a -> b
$ Maybe String -> (Val -> Eval Val) -> Val
Func Maybe String
forall a. Maybe a
Nothing ([Val] -> Val -> Eval Val
g [Val]
args)
g [Val]
args Val
v = Val -> Eval Val
forall (m :: * -> *) a. Monad m => a -> m a
return (Val -> Eval Val) -> Val -> Eval Val
forall a b. (a -> b) -> a -> b
$ Maybe String -> (Val -> Eval Val) -> Val
Func Maybe String
forall a. Maybe a
Nothing ([Val] -> Val -> Eval Val
g (Val
vVal -> [Val] -> [Val]
forall a. a -> [a] -> [a]
:[Val]
args))
sEnumFromThenTo :: Val
sEnumFromThenTo :: Val
sEnumFromThenTo = Maybe String -> (Val -> Eval Val) -> Val
Func Maybe String
forall a. Maybe a
Nothing ([Val] -> Val -> Eval Val
g [])
where g :: [Val] -> Val -> Eval Val
g [Val
x, Val
y] Val
z = Val -> Maybe Val -> Val -> Eval Val
enumList Val
y (Val -> Maybe Val
forall a. a -> Maybe a
Just Val
x) Val
z
g [Val]
args (Typ SKind
_) = Val -> Eval Val
forall (m :: * -> *) a. Monad m => a -> m a
return (Val -> Eval Val) -> Val -> Eval Val
forall a b. (a -> b) -> a -> b
$ Maybe String -> (Val -> Eval Val) -> Val
Func Maybe String
forall a. Maybe a
Nothing ([Val] -> Val -> Eval Val
g [Val]
args)
g [Val]
args Val
v = Val -> Eval Val
forall (m :: * -> *) a. Monad m => a -> m a
return (Val -> Eval Val) -> Val -> Eval Val
forall a b. (a -> b) -> a -> b
$ Maybe String -> (Val -> Eval Val) -> Val
Func Maybe String
forall a. Maybe a
Nothing ([Val] -> Val -> Eval Val
g (Val
vVal -> [Val] -> [Val]
forall a. a -> [a] -> [a]
:[Val]
args))
enumList :: Val -> Maybe Val -> Val -> Eval Val
enumList :: Val -> Maybe Val -> Val -> Eval Val
enumList Val
bf Maybe Val
mbs Val
bt
| Just Val
bs <- Maybe Val
mbs, Just SVal
f <- Val -> Maybe SVal
extract Val
bf, Just SVal
s <- Val -> Maybe SVal
extract Val
bs, Just SVal
t <- Val -> Maybe SVal
extract Val
bt = Maybe [SVal] -> Eval Val
mkLst (Maybe [SVal] -> Eval Val) -> Maybe [SVal] -> Eval Val
forall a b. (a -> b) -> a -> b
$ SVal -> Maybe SVal -> SVal -> Maybe [SVal]
S.svEnumFromThenTo SVal
f (SVal -> Maybe SVal
forall a. a -> Maybe a
Just SVal
s) SVal
t
| Just SVal
f <- Val -> Maybe SVal
extract Val
bf, Just SVal
t <- Val -> Maybe SVal
extract Val
bt = Maybe [SVal] -> Eval Val
mkLst (Maybe [SVal] -> Eval Val) -> Maybe [SVal] -> Eval Val
forall a b. (a -> b) -> a -> b
$ SVal -> Maybe SVal -> SVal -> Maybe [SVal]
S.svEnumFromThenTo SVal
f Maybe SVal
forall a. Maybe a
Nothing SVal
t
| Bool
True = Eval Val
forall {b}. ReaderT Env Symbolic b
cantHandle
where extract :: Val -> Maybe SVal
extract (Base SVal
b) = SVal -> Maybe SVal
forall a. a -> Maybe a
Just SVal
b
extract Val
_ = String -> Maybe SVal
forall a. HasCallStack => String -> a
error (String -> Maybe SVal) -> String -> Maybe SVal
forall a b. (a -> b) -> a -> b
$ String
"SBVPlugin.enumList: Impossible happened: " String -> String -> String
forall a. [a] -> [a] -> [a]
++ SDoc -> String
showSDocUnsafe ((Val, Maybe Val, Val) -> SDoc
forall a. Outputable a => a -> SDoc
ppr (Val
bf, Maybe Val
mbs, Val
bt))
mkLst :: Maybe [SVal] -> Eval Val
mkLst (Just [SVal]
xs) = Val -> Eval Val
forall (m :: * -> *) a. Monad m => a -> m a
return (Val -> Eval Val) -> Val -> Eval Val
forall a b. (a -> b) -> a -> b
$ [Val] -> Val
Lst ([Val] -> Val) -> [Val] -> Val
forall a b. (a -> b) -> a -> b
$ (SVal -> Val) -> [SVal] -> [Val]
forall a b. (a -> b) -> [a] -> [b]
map SVal -> Val
Base [SVal]
xs
mkLst Maybe [SVal]
_ = Eval Val
forall {b}. ReaderT Env Symbolic b
cantHandle
cantHandle :: ReaderT Env Symbolic b
cantHandle = do Env{forall a. String -> [String] -> Eval a
bailOut :: Env -> forall a. String -> [String] -> Eval a
bailOut :: 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 b
forall a. String -> [String] -> Eval a
bailOut String
"Found unsupported list comprehension expression"
([[String]] -> [String]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat [ [ String
"From: " String -> String -> String
forall a. [a] -> [a] -> [a]
++ SDoc -> String
showSDocUnsafe (Val -> SDoc
forall a. Outputable a => a -> SDoc
ppr Val
bf) ]
, [ String
"Then: " String -> String -> String
forall a. [a] -> [a] -> [a]
++ SDoc -> String
showSDocUnsafe (Val -> SDoc
forall a. Outputable a => a -> SDoc
ppr Val
bs) | Just Val
bs <- [Maybe Val
mbs]]
, [ String
"To : " String -> String -> String
forall a. [a] -> [a] -> [a]
++ SDoc -> String
showSDocUnsafe (Val -> SDoc
forall a. Outputable a => a -> SDoc
ppr Val
bt)
, String
"Kind: " String -> String -> String
forall a. [a] -> [a] -> [a]
++ (if Maybe Val -> Bool
forall a. Maybe a -> Bool
isJust Maybe Val
mbs then String
"[x, y .. z]" else String
"[x .. y]")
, String
"Hint: The plugin only allows finite comprehensions with concrete boundaries."
]
])
thToGHC :: (TH.Name, a, b) -> CoreM ((Id, a), b)
thToGHC :: forall a b. (Name, a, b) -> CoreM ((Id, a), b)
thToGHC (Name
n, a
k, b
sfn) = do Id
f <- (Name -> CoreM Id) -> Name -> CoreM Id
forall b. (Name -> CoreM b) -> Name -> CoreM b
grabTH Name -> CoreM Id
forall (m :: * -> *). MonadThings m => Name -> m Id
lookupId Name
n
((Id, a), b) -> CoreM ((Id, a), b)
forall (m :: * -> *) a. Monad m => a -> m a
return ((Id
f, a
k), b
sfn)
grabTH :: (Name -> CoreM b) -> TH.Name -> CoreM b
grabTH :: forall b. (Name -> CoreM b) -> Name -> CoreM b
grabTH Name -> CoreM b
f Name
n = do Maybe Name
mbN <- Name -> CoreM (Maybe Name)
thNameToGhcName Name
n
case Maybe Name
mbN of
Just Name
gn -> Name -> CoreM b
f Name
gn
Maybe Name
Nothing -> Name -> CoreM b
f (Name -> CoreM b) -> CoreM Name -> CoreM b
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< Maybe String -> String -> CoreM Name
lookInModule (Name -> Maybe String
TH.nameModule Name
n) (Name -> String
TH.nameBase Name
n)
where lookInModule :: Maybe String -> String -> CoreM Name
lookInModule Maybe String
Nothing String
_ = String -> CoreM Name
forall a. HasCallStack => String -> a
error (String -> CoreM Name) -> String -> CoreM Name
forall a b. (a -> b) -> a -> b
$ String
"[SBV] Impossible happened, while trying to locate GHC name for: " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Name -> String
forall a. Show a => a -> String
show Name
n
lookInModule (Just String
inModule) String
bn = do
HscEnv
env <- CoreM HscEnv
getHscEnv
IO Name -> CoreM Name
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (IO Name -> CoreM Name) -> IO Name -> CoreM Name
forall a b. (a -> b) -> a -> b
$ do FindResult
r <- HscEnv -> ModuleName -> Maybe FastString -> IO FindResult
findImportedModule HscEnv
env (String -> ModuleName
mkModuleName String
inModule) Maybe FastString
forall a. Maybe a
Nothing
case FindResult
r of
Found ModLocation
_ Module
mdl -> HscEnv -> Module -> OccName -> IO Name
lookupOrigIO HscEnv
env Module
mdl (String -> OccName
mkVarOcc String
bn)
FindResult
_ -> String -> IO Name
forall a. HasCallStack => String -> a
error (String -> IO Name) -> String -> IO Name
forall a b. (a -> b) -> a -> b
$ String
"[SBV] Impossible happened, can't find " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String -> String
forall a. Show a => a -> String
show String
bn String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
" in module " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String -> String
forall a. Show a => a -> String
show String
inModule