--------------------------------------------------------------------------
-- |
-- Module      :  Data.SBV.Plugin.Env
-- Copyright   :  (c) Levent Erkok
-- License     :  BSD3
-- Maintainer  :  erkokl@gmail.com
-- Stability   :  experimental
--
-- The environment for mapping concrete functions/types to symbolic ones.
-----------------------------------------------------------------------------

{-# LANGUAGE MagicHash             #-}
{-# LANGUAGE NamedFieldPuns        #-}
{-# LANGUAGE TemplateHaskellQuotes #-}

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

-- | What tuple-sizes we support? We go upto 15, but would be easy to change if necessary
supportTupleSizes :: [Int]
supportTupleSizes :: [Int]
supportTupleSizes = [Int
2 .. Int
15]

-- | Build the initial environment containing types
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)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [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)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [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 a. a -> CoreM a
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)
forall (m :: * -> *) a b. 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 a. a -> CoreM a
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) ]

-- | Build the initial environment containing functions
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 a b. (a -> b) -> CoreM a -> CoreM b
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)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [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)

-- | Basic conversions, only on one kind
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 a. a -> ReaderT Env Symbolic a
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 a. a -> ReaderT Env Symbolic a
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 a. a -> ReaderT Env Symbolic a
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 a. a -> ReaderT Env Symbolic a
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)
                 ]

-- | Symbolic functions supported by the plugin; those from a class.
symFuncs :: Int -> [(TH.Name, SKind, Val)]
symFuncs :: Int -> [(Name, SKind, Val)]
symFuncs Int
wsz =  -- equality is for all kinds
          [(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)]]

          -- arithmetic
       [(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]

          -- literal conversions from Integer
       [(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)]]

          -- comparisons
       [(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 ]

          -- integer div/rem
      [(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)]]

         -- bit-vector
      [(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]

         -- constructing "fixed-size" lists
      [(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
       -- Bit-vectors
       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]]

       -- Those that are "integral"ish
       integralKinds :: [Kind]
integralKinds = Kind
S.KUnbounded Kind -> [Kind] -> [Kind]
forall a. a -> [a] -> [a]
: [Kind]
bvKinds

       -- Those that can be converted from an Integer
       integerKinds :: [Kind]
integerKinds = Kind
S.KReal Kind -> [Kind] -> [Kind]
forall a. a -> [a] -> [a]
: [Kind]
integralKinds

       -- Float kinds
       floatKinds :: [Kind]
floatKinds = [Kind
S.KFloat, Kind
S.KDouble]

       -- All arithmetic kinds
       arithKinds :: [Kind]
arithKinds = [Kind]
floatKinds [Kind] -> [Kind] -> [Kind]
forall a. [a] -> [a] -> [a]
++ [Kind]
integerKinds

       -- Everything
       allKinds :: [Kind]
allKinds   = Kind
S.KBool Kind -> [Kind] -> [Kind]
forall a. a -> [a] -> [a]
: [Kind]
arithKinds

       -- Unary arithmetic ops
       unaryOps :: [(Name, SVal -> SVal)]
unaryOps   = [ ('abs,        SVal -> SVal
S.svAbs)
                    , ('negate,     SVal -> SVal
S.svUNeg)
                    , ('complement, SVal -> SVal
S.svNot)
                    ]

       -- Binary arithmetic ops
       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)
                    ]

       -- Comparisons
       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)
                 ]

       -- Binary bit-vector ops
       bvBinOps :: [(Name, SVal -> SVal -> SVal)]
bvBinOps = [ ('(.&.),   SVal -> SVal -> SVal
S.svAnd)
                  , ('(.|.),   SVal -> SVal -> SVal
S.svOr)
                  , ('xor,     SVal -> SVal -> SVal
S.svXOr)
                  ]

       -- Shift/rotates, where second argument is an int
       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)
                     ]


-- | Destructors
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)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [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)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [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 a. a -> CoreM a
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 a. [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 a. a -> CoreM a
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 a. [a] -> 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 a. [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 a. a -> CoreM a
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 a. a -> CoreM 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 a. a -> CoreM a
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)

-- | These types show up during uninterpretation, but are not really "interesting" as they
-- are singly inhabited.
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 a b. (a -> b) -> CoreM a -> CoreM b
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)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [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#]

-- | Certain things are just too special, as they uniformly apply to uninterpreted types.
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 a. a -> CoreM a
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 a. a -> ReaderT Env Symbolic a
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 a. a -> ReaderT Env Symbolic a
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 a. a -> ReaderT Env Symbolic a
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)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [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 a. a -> CoreM a
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 a. a -> ReaderT Env Symbolic a
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 a. a -> ReaderT Env Symbolic a
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 a. a -> m a
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 a. a -> CoreM a
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 a. a -> CoreM a
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
                                  }

-- | Lift a binary type, with result bool
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))

-- | Lift a unary type
tlift1 :: SKind -> SKind
tlift1 :: SKind -> SKind
tlift1 SKind
k = SKind -> SKind -> SKind
KFun SKind
k SKind
k

-- | Lift a binary type
tlift2 :: SKind -> SKind
tlift2 :: SKind -> SKind
tlift2 SKind
k = SKind -> SKind -> SKind
KFun SKind
k (SKind -> SKind
tlift1 SKind
k)

-- | Lift a binary type, where second argument is Int
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)

-- | Type of enumFromTo: [x .. y]
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))

-- | Type of enumFromThenTo: [x .. y]
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)))

-- | Lift a unary SBV function that via kind/integer
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 a. a -> m a
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!"

-- | Lift a unary SBV function to the plugin value space
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 a. a -> m a
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 a. a -> m a
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)

-- | Lift a two argument SBV function to our the plugin value space
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 a. a -> m a
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 a. a -> m a
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 a. a -> m a
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)

-- | Lifting an equality is special; since it acts uniformly over tuples.
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 a. a -> ReaderT Env Symbolic a
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 a. a -> ReaderT Env Symbolic a
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 a. a -> ReaderT Env Symbolic a
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

-- | Lifting enumFromTo: [x .. y]
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 a. a -> ReaderT Env Symbolic a
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 a. a -> ReaderT Env Symbolic a
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))

-- | Lifting sEnumFromThenTo: [x, y .. z]
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 a. a -> ReaderT Env Symbolic a
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 a. a -> ReaderT Env Symbolic a
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))

-- | Implement [x .. y] or [x, y .. z]; provided the inputs are concrete
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 a. a -> ReaderT Env Symbolic a
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 :: 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 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 a. a -> CoreM a
forall (m :: * -> *) a. Monad m => a -> m a
return ((Id
f, a
k), b
sfn)

-- TODO: Starting with GHC 8.6, we no longer get the names available unless the
-- user code explicitly imports them. See: https://ghc.haskell.org/trac/ghc/ticket/16104
-- I was able to get the workaround it as in below, but it seems really fragile and
-- it also requires me to export the splittable class from the plugin. Surely there
-- must be a better way.
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
           env :: HscEnv
env@HscEnv{NameCache
hsc_NC :: NameCache
hsc_NC :: HscEnv -> NameCache
hsc_NC} <- CoreM HscEnv
getHscEnv
           IO Name -> CoreM Name
forall a. IO a -> CoreM a
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 -> PkgQual -> IO FindResult
findImportedModule HscEnv
env (String -> ModuleName
mkModuleName String
inModule) PkgQual
NoPkgQual
                       case FindResult
r of
                         Found ModLocation
_ Module
mdl -> NameCache -> Module -> OccName -> IO Name
lookupNameCache NameCache
hsc_NC 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