{-# LANGUAGE AllowAmbiguousTypes #-}
{-# LANGUAGE ConstraintKinds #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE LambdaCase #-}
{-# LANGUAGE PatternSynonyms #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE QuantifiedConstraints #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE RoleAnnotations #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE ViewPatterns #-}
module Grisette.Backend.SBV.Data.SMT.Lowering
( lowerSinglePrim,
lowerSinglePrim',
parseModel,
SymBiMap,
)
where
import Control.Monad.State.Strict
import Data.Bifunctor
import Data.Bits
import Data.Dynamic
import Data.Foldable
import Data.Kind
import Data.Maybe
import qualified Data.SBV as SBV
import qualified Data.SBV.Internals as SBVI
import Data.Type.Equality (type (~~))
import Data.Typeable
import GHC.Exts (sortWith)
import GHC.Natural
import GHC.Stack
import GHC.TypeNats
import {-# SOURCE #-} Grisette.Backend.SBV.Data.SMT.Solving
import Grisette.Backend.SBV.Data.SMT.SymBiMap
import Grisette.Core.Data.Class.ModelOps
import Grisette.IR.SymPrim.Data.BV
import Grisette.IR.SymPrim.Data.Prim.InternedTerm.InternedCtors
import Grisette.IR.SymPrim.Data.Prim.InternedTerm.SomeTerm
import Grisette.IR.SymPrim.Data.Prim.InternedTerm.Term
import Grisette.IR.SymPrim.Data.Prim.InternedTerm.TermUtils
import Grisette.IR.SymPrim.Data.Prim.Model as PM
import Grisette.IR.SymPrim.Data.Prim.PartialEval.Bool
import Grisette.IR.SymPrim.Data.TabularFun
import qualified Type.Reflection as R
import Unsafe.Coerce
newtype NatRepr (n :: Nat) = NatRepr Natural
withKnownNat :: forall n r. NatRepr n -> (KnownNat n => r) -> r
withKnownNat :: forall (n :: Nat) r. NatRepr n -> (KnownNat n => r) -> r
withKnownNat (NatRepr Nat
nVal) KnownNat n => r
v =
case Nat -> SomeNat
someNatVal Nat
nVal of
SomeNat (Proxy n
Proxy :: Proxy n') ->
case forall {k} (a :: k) (b :: k). a :~: b
unsafeAxiom :: n :~: n' of
n :~: n
Refl -> KnownNat n => r
v
data LeqProof (m :: Nat) (n :: Nat) where
LeqProof :: m <= n => LeqProof m n
unsafeAxiom :: forall a b. a :~: b
unsafeAxiom :: forall {k} (a :: k) (b :: k). a :~: b
unsafeAxiom = forall a b. a -> b
unsafeCoerce (forall {k} (a :: k). a :~: a
Refl @a)
{-# NOINLINE unsafeAxiom #-}
unsafeLeqProof :: forall m n. LeqProof m n
unsafeLeqProof :: forall (m :: Nat) (n :: Nat). LeqProof m n
unsafeLeqProof = forall a b. a -> b
unsafeCoerce (forall (m :: Nat) (n :: Nat). (m <= n) => LeqProof m n
LeqProof @0 @0)
{-# NOINLINE unsafeLeqProof #-}
cachedResult ::
forall integerBitWidth a.
(SupportedPrim a, Typeable (TermTy integerBitWidth a)) =>
Term a ->
State SymBiMap (Maybe (TermTy integerBitWidth a))
cachedResult :: forall (integerBitWidth :: Nat) a.
(SupportedPrim a, Typeable (TermTy integerBitWidth a)) =>
Term a -> State SymBiMap (Maybe (TermTy integerBitWidth a))
cachedResult Term a
t = forall s (m :: * -> *) a. MonadState s m => (s -> a) -> m a
gets forall a b. (a -> b) -> a -> b
$ \SymBiMap
m -> do
Dynamic
d <- HasCallStack => SomeTerm -> SymBiMap -> Maybe Dynamic
lookupTerm (forall a. SupportedPrim a => Term a -> SomeTerm
SomeTerm Term a
t) SymBiMap
m
forall a. a -> Maybe a
Just forall a b. (a -> b) -> a -> b
$ forall a. Typeable a => Dynamic -> a -> a
fromDyn Dynamic
d forall a. HasCallStack => a
undefined
addResult ::
forall integerBitWidth a.
(SupportedPrim a, Typeable (TermTy integerBitWidth a)) =>
Term a ->
TermTy integerBitWidth a ->
State SymBiMap ()
addResult :: forall (integerBitWidth :: Nat) a.
(SupportedPrim a, Typeable (TermTy integerBitWidth a)) =>
Term a -> TermTy integerBitWidth a -> State SymBiMap ()
addResult Term a
tm TermTy integerBitWidth a
sbvtm = forall s (m :: * -> *). MonadState s m => (s -> s) -> m ()
modify forall a b. (a -> b) -> a -> b
$ HasCallStack => SomeTerm -> Dynamic -> SymBiMap -> SymBiMap
addBiMapIntermediate (forall a. SupportedPrim a => Term a -> SomeTerm
SomeTerm Term a
tm) (forall a. Typeable a => a -> Dynamic
toDyn TermTy integerBitWidth a
sbvtm)
lowerSinglePrim' ::
forall integerBitWidth a.
GrisetteSMTConfig integerBitWidth ->
Term a ->
SymBiMap ->
(TermTy integerBitWidth a, SymBiMap)
lowerSinglePrim' :: forall (integerBitWidth :: Nat) a.
GrisetteSMTConfig integerBitWidth
-> Term a -> SymBiMap -> (TermTy integerBitWidth a, SymBiMap)
lowerSinglePrim' GrisetteSMTConfig integerBitWidth
config Term a
t = forall s a. State s a -> s -> (a, s)
runState (forall (integerBitWidth :: Nat) a.
GrisetteSMTConfig integerBitWidth
-> Term a -> State SymBiMap (TermTy integerBitWidth a)
lowerSinglePrimCached' GrisetteSMTConfig integerBitWidth
config Term a
t)
lowerSinglePrimCached' ::
forall integerBitWidth a.
GrisetteSMTConfig integerBitWidth ->
Term a ->
State SymBiMap (TermTy integerBitWidth a)
lowerSinglePrimCached' :: forall (integerBitWidth :: Nat) a.
GrisetteSMTConfig integerBitWidth
-> Term a -> State SymBiMap (TermTy integerBitWidth a)
lowerSinglePrimCached' GrisetteSMTConfig integerBitWidth
config Term a
t = forall t a. Term t -> (SupportedPrim t => a) -> a
introSupportedPrimConstraint Term a
t forall a b. (a -> b) -> a -> b
$
case (GrisetteSMTConfig integerBitWidth
config, forall {k} (a :: k). Typeable a => TypeRep a
R.typeRep @a) of
(GrisetteSMTConfig integerBitWidth, TypeRep a)
ResolvedDeepType -> do
Maybe s'
r <- forall (integerBitWidth :: Nat) a.
(SupportedPrim a, Typeable (TermTy integerBitWidth a)) =>
Term a -> State SymBiMap (Maybe (TermTy integerBitWidth a))
cachedResult @integerBitWidth Term a
t
case Maybe s'
r of
Just s'
v -> forall (m :: * -> *) a. Monad m => a -> m a
return s'
v
Maybe s'
_ -> forall (integerBitWidth :: Nat) a.
GrisetteSMTConfig integerBitWidth
-> Term a -> State SymBiMap (TermTy integerBitWidth a)
lowerSinglePrimImpl' GrisetteSMTConfig integerBitWidth
config Term a
t
(GrisetteSMTConfig integerBitWidth, TypeRep a)
_ -> forall {k} (a :: k) b. HasCallStack => TypeRep a -> b
translateTypeError (forall {k} (a :: k). Typeable a => TypeRep a
R.typeRep @a)
lowerUnaryTerm' ::
forall integerBitWidth a a1 x x1.
(Typeable x1, a1 ~ TermTy integerBitWidth a, SupportedPrim x, x1 ~ TermTy integerBitWidth x) =>
GrisetteSMTConfig integerBitWidth ->
Term x ->
Term a ->
(a1 -> x1) ->
State SymBiMap (TermTy integerBitWidth x)
lowerUnaryTerm' :: forall (integerBitWidth :: Nat) a a1 x x1.
(Typeable x1, a1 ~ TermTy integerBitWidth a, SupportedPrim x,
x1 ~ TermTy integerBitWidth x) =>
GrisetteSMTConfig integerBitWidth
-> Term x
-> Term a
-> (a1 -> x1)
-> State SymBiMap (TermTy integerBitWidth x)
lowerUnaryTerm' GrisetteSMTConfig integerBitWidth
config Term x
orig Term a
t1 a1 -> x1
f = do
a1
l1 <- forall (integerBitWidth :: Nat) a.
GrisetteSMTConfig integerBitWidth
-> Term a -> State SymBiMap (TermTy integerBitWidth a)
lowerSinglePrimCached' GrisetteSMTConfig integerBitWidth
config Term a
t1
let g :: x1
g = a1 -> x1
f a1
l1
forall (integerBitWidth :: Nat) a.
(SupportedPrim a, Typeable (TermTy integerBitWidth a)) =>
Term a -> TermTy integerBitWidth a -> State SymBiMap ()
addResult @integerBitWidth Term x
orig x1
g
forall (m :: * -> *) a. Monad m => a -> m a
return x1
g
lowerBinaryTerm' ::
forall integerBitWidth a b a1 b1 x.
( Typeable (TermTy integerBitWidth x),
a1 ~ TermTy integerBitWidth a,
b1 ~ TermTy integerBitWidth b,
SupportedPrim x
) =>
GrisetteSMTConfig integerBitWidth ->
Term x ->
Term a ->
Term b ->
(a1 -> b1 -> TermTy integerBitWidth x) ->
State SymBiMap (TermTy integerBitWidth x)
lowerBinaryTerm' :: forall (integerBitWidth :: Nat) a b a1 b1 x.
(Typeable (TermTy integerBitWidth x),
a1 ~ TermTy integerBitWidth a, b1 ~ TermTy integerBitWidth b,
SupportedPrim x) =>
GrisetteSMTConfig integerBitWidth
-> Term x
-> Term a
-> Term b
-> (a1 -> b1 -> TermTy integerBitWidth x)
-> State SymBiMap (TermTy integerBitWidth x)
lowerBinaryTerm' GrisetteSMTConfig integerBitWidth
config Term x
orig Term a
t1 Term b
t2 a1 -> b1 -> TermTy integerBitWidth x
f = do
a1
l1 <- forall (integerBitWidth :: Nat) a.
GrisetteSMTConfig integerBitWidth
-> Term a -> State SymBiMap (TermTy integerBitWidth a)
lowerSinglePrimCached' GrisetteSMTConfig integerBitWidth
config Term a
t1
b1
l2 <- forall (integerBitWidth :: Nat) a.
GrisetteSMTConfig integerBitWidth
-> Term a -> State SymBiMap (TermTy integerBitWidth a)
lowerSinglePrimCached' GrisetteSMTConfig integerBitWidth
config Term b
t2
let g :: TermTy integerBitWidth x
g = a1 -> b1 -> TermTy integerBitWidth x
f a1
l1 b1
l2
forall (integerBitWidth :: Nat) a.
(SupportedPrim a, Typeable (TermTy integerBitWidth a)) =>
Term a -> TermTy integerBitWidth a -> State SymBiMap ()
addResult @integerBitWidth Term x
orig TermTy integerBitWidth x
g
forall (m :: * -> *) a. Monad m => a -> m a
return TermTy integerBitWidth x
g
lowerSinglePrimImpl' ::
forall integerBitWidth a.
GrisetteSMTConfig integerBitWidth ->
Term a ->
State SymBiMap (TermTy integerBitWidth a)
lowerSinglePrimImpl' :: forall (integerBitWidth :: Nat) a.
GrisetteSMTConfig integerBitWidth
-> Term a -> State SymBiMap (TermTy integerBitWidth a)
lowerSinglePrimImpl' ResolvedConfig {} (ConTerm Id
_ a
v) =
case forall {k} (a :: k). Typeable a => TypeRep a
R.typeRep @a of
TypeRep a
BoolType -> forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ if a
v then SBool
SBV.sTrue else SBool
SBV.sFalse
TypeRep a
IntegerType -> forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall a. Num a => Integer -> a
fromInteger a
v
SignedBVType Proxy n
_ -> case a
v of
IntN Integer
x -> forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall a. Num a => Integer -> a
fromInteger Integer
x
UnsignedBVType Proxy n
_ -> case a
v of
WordN Integer
x -> forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall a. Num a => Integer -> a
fromInteger Integer
x
TypeRep a
_ -> forall {k} (a :: k) b. HasCallStack => TypeRep a -> b
translateTypeError (forall {k} (a :: k). Typeable a => TypeRep a
R.typeRep @a)
lowerSinglePrimImpl' GrisetteSMTConfig integerBitWidth
_ t :: Term a
t@SymTerm {} =
forall a. HasCallStack => [Char] -> a
error forall a b. (a -> b) -> a -> b
$
[Char]
"The symbolic term should have already been lowered "
forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> [Char]
show Term a
t
forall a. [a] -> [a] -> [a]
++ [Char]
" to SMT with collectedPrims.\n"
forall a. [a] -> [a] -> [a]
++ [Char]
"We don't support adding new symbolics after collectedPrims with SBV backend"
lowerSinglePrimImpl' GrisetteSMTConfig integerBitWidth
_ (UnaryTerm Id
_ tag
op (Term arg
_ :: Term x)) = forall t1. t1
errorMsg
where
errorMsg :: forall t1. t1
errorMsg :: forall t1. t1
errorMsg = forall {k} {k} (a :: k) (b :: k) c.
HasCallStack =>
[Char] -> TypeRep a -> TypeRep b -> c
translateUnaryError (forall a. Show a => a -> [Char]
show tag
op) (forall {k} (a :: k). Typeable a => TypeRep a
R.typeRep @x) (forall {k} (a :: k). Typeable a => TypeRep a
R.typeRep @a)
lowerSinglePrimImpl' GrisetteSMTConfig integerBitWidth
_ (BinaryTerm Id
_ tag
op (Term arg1
_ :: Term x) (Term arg2
_ :: Term y)) = forall t1. t1
errorMsg
where
errorMsg :: forall t1. t1
errorMsg :: forall t1. t1
errorMsg = forall {k} {k} {k} (a :: k) (b :: k) (c :: k) d.
HasCallStack =>
[Char] -> TypeRep a -> TypeRep b -> TypeRep c -> d
translateBinaryError (forall a. Show a => a -> [Char]
show tag
op) (forall {k} (a :: k). Typeable a => TypeRep a
R.typeRep @x) (forall {k} (a :: k). Typeable a => TypeRep a
R.typeRep @y) (forall {k} (a :: k). Typeable a => TypeRep a
R.typeRep @a)
lowerSinglePrimImpl' ResolvedConfig {} (TernaryTerm Id
_ tag
op (Term arg1
_ :: Term x) (Term arg2
_ :: Term y) (Term arg3
_ :: Term z)) = forall t1. t1
errorMsg
where
errorMsg :: forall t1. t1
errorMsg :: forall t1. t1
errorMsg = forall {k} {k} {k} {k} (a :: k) (b :: k) (c :: k) (d :: k) e.
HasCallStack =>
[Char] -> TypeRep a -> TypeRep b -> TypeRep c -> TypeRep d -> e
translateTernaryError (forall a. Show a => a -> [Char]
show tag
op) (forall {k} (a :: k). Typeable a => TypeRep a
R.typeRep @x) (forall {k} (a :: k). Typeable a => TypeRep a
R.typeRep @y) (forall {k} (a :: k). Typeable a => TypeRep a
R.typeRep @z) (forall {k} (a :: k). Typeable a => TypeRep a
R.typeRep @a)
lowerSinglePrimImpl' GrisetteSMTConfig integerBitWidth
config t :: Term a
t@(NotTerm Id
_ Term Bool
arg) = forall (integerBitWidth :: Nat) a a1 x x1.
(Typeable x1, a1 ~ TermTy integerBitWidth a, SupportedPrim x,
x1 ~ TermTy integerBitWidth x) =>
GrisetteSMTConfig integerBitWidth
-> Term x
-> Term a
-> (a1 -> x1)
-> State SymBiMap (TermTy integerBitWidth x)
lowerUnaryTerm' GrisetteSMTConfig integerBitWidth
config Term a
t Term Bool
arg SBool -> SBool
SBV.sNot
lowerSinglePrimImpl' GrisetteSMTConfig integerBitWidth
config t :: Term a
t@(OrTerm Id
_ Term Bool
arg1 Term Bool
arg2) = forall (integerBitWidth :: Nat) a b a1 b1 x.
(Typeable (TermTy integerBitWidth x),
a1 ~ TermTy integerBitWidth a, b1 ~ TermTy integerBitWidth b,
SupportedPrim x) =>
GrisetteSMTConfig integerBitWidth
-> Term x
-> Term a
-> Term b
-> (a1 -> b1 -> TermTy integerBitWidth x)
-> State SymBiMap (TermTy integerBitWidth x)
lowerBinaryTerm' GrisetteSMTConfig integerBitWidth
config Term a
t Term Bool
arg1 Term Bool
arg2 SBool -> SBool -> SBool
(SBV..||)
lowerSinglePrimImpl' GrisetteSMTConfig integerBitWidth
config t :: Term a
t@(AndTerm Id
_ Term Bool
arg1 Term Bool
arg2) = forall (integerBitWidth :: Nat) a b a1 b1 x.
(Typeable (TermTy integerBitWidth x),
a1 ~ TermTy integerBitWidth a, b1 ~ TermTy integerBitWidth b,
SupportedPrim x) =>
GrisetteSMTConfig integerBitWidth
-> Term x
-> Term a
-> Term b
-> (a1 -> b1 -> TermTy integerBitWidth x)
-> State SymBiMap (TermTy integerBitWidth x)
lowerBinaryTerm' GrisetteSMTConfig integerBitWidth
config Term a
t Term Bool
arg1 Term Bool
arg2 SBool -> SBool -> SBool
(SBV..&&)
lowerSinglePrimImpl' GrisetteSMTConfig integerBitWidth
config t :: Term a
t@(EqvTerm Id
_ (Term t1
arg1 :: Term x) Term t1
arg2) =
case (GrisetteSMTConfig integerBitWidth
config, forall {k} (a :: k). Typeable a => TypeRep a
R.typeRep @x) of
(GrisetteSMTConfig integerBitWidth, TypeRep t1)
ResolvedSimpleType -> forall (integerBitWidth :: Nat) a b a1 b1 x.
(Typeable (TermTy integerBitWidth x),
a1 ~ TermTy integerBitWidth a, b1 ~ TermTy integerBitWidth b,
SupportedPrim x) =>
GrisetteSMTConfig integerBitWidth
-> Term x
-> Term a
-> Term b
-> (a1 -> b1 -> TermTy integerBitWidth x)
-> State SymBiMap (TermTy integerBitWidth x)
lowerBinaryTerm' GrisetteSMTConfig integerBitWidth
config Term a
t Term t1
arg1 Term t1
arg2 forall a. EqSymbolic a => a -> a -> SBool
(SBV..==)
(GrisetteSMTConfig integerBitWidth, TypeRep t1)
_ -> forall {k} {k} {k} (a :: k) (b :: k) (c :: k) d.
HasCallStack =>
[Char] -> TypeRep a -> TypeRep b -> TypeRep c -> d
translateBinaryError [Char]
"(==)" (forall {k} (a :: k). Typeable a => TypeRep a
R.typeRep @x) (forall {k} (a :: k). Typeable a => TypeRep a
R.typeRep @x) (forall {k} (a :: k). Typeable a => TypeRep a
R.typeRep @a)
lowerSinglePrimImpl' GrisetteSMTConfig integerBitWidth
config t :: Term a
t@(ITETerm Id
_ Term Bool
cond Term a
arg1 Term a
arg2) =
case (GrisetteSMTConfig integerBitWidth
config, forall {k} (a :: k). Typeable a => TypeRep a
R.typeRep @a) of
(GrisetteSMTConfig integerBitWidth, TypeRep a)
ResolvedSimpleType -> do
SBool
l1 <- forall (integerBitWidth :: Nat) a.
GrisetteSMTConfig integerBitWidth
-> Term a -> State SymBiMap (TermTy integerBitWidth a)
lowerSinglePrimCached' GrisetteSMTConfig integerBitWidth
config Term Bool
cond
SBV s'
l2 <- forall (integerBitWidth :: Nat) a.
GrisetteSMTConfig integerBitWidth
-> Term a -> State SymBiMap (TermTy integerBitWidth a)
lowerSinglePrimCached' GrisetteSMTConfig integerBitWidth
config Term a
arg1
SBV s'
l3 <- forall (integerBitWidth :: Nat) a.
GrisetteSMTConfig integerBitWidth
-> Term a -> State SymBiMap (TermTy integerBitWidth a)
lowerSinglePrimCached' GrisetteSMTConfig integerBitWidth
config Term a
arg2
let g :: SBV s'
g = forall a. Mergeable a => SBool -> a -> a -> a
SBV.ite SBool
l1 SBV s'
l2 SBV s'
l3
forall (integerBitWidth :: Nat) a.
(SupportedPrim a, Typeable (TermTy integerBitWidth a)) =>
Term a -> TermTy integerBitWidth a -> State SymBiMap ()
addResult @integerBitWidth Term a
t SBV s'
g
forall (m :: * -> *) a. Monad m => a -> m a
return SBV s'
g
(GrisetteSMTConfig integerBitWidth, TypeRep a)
_ -> forall {k} {k} {k} {k} (a :: k) (b :: k) (c :: k) (d :: k) e.
HasCallStack =>
[Char] -> TypeRep a -> TypeRep b -> TypeRep c -> TypeRep d -> e
translateTernaryError [Char]
"ite" (forall {k} (a :: k). Typeable a => TypeRep a
R.typeRep @Bool) (forall {k} (a :: k). Typeable a => TypeRep a
R.typeRep @a) (forall {k} (a :: k). Typeable a => TypeRep a
R.typeRep @a) (forall {k} (a :: k). Typeable a => TypeRep a
R.typeRep @a)
lowerSinglePrimImpl' GrisetteSMTConfig integerBitWidth
config t :: Term a
t@(AddNumTerm Id
_ Term a
arg1 Term a
arg2) =
case (GrisetteSMTConfig integerBitWidth
config, forall {k} (a :: k). Typeable a => TypeRep a
R.typeRep @a) of
(GrisetteSMTConfig integerBitWidth, TypeRep a)
ResolvedNumType -> forall (integerBitWidth :: Nat) a b a1 b1 x.
(Typeable (TermTy integerBitWidth x),
a1 ~ TermTy integerBitWidth a, b1 ~ TermTy integerBitWidth b,
SupportedPrim x) =>
GrisetteSMTConfig integerBitWidth
-> Term x
-> Term a
-> Term b
-> (a1 -> b1 -> TermTy integerBitWidth x)
-> State SymBiMap (TermTy integerBitWidth x)
lowerBinaryTerm' GrisetteSMTConfig integerBitWidth
config Term a
t Term a
arg1 Term a
arg2 forall a. Num a => a -> a -> a
(+)
(GrisetteSMTConfig integerBitWidth, TypeRep a)
_ -> forall {k} {k} {k} (a :: k) (b :: k) (c :: k) d.
HasCallStack =>
[Char] -> TypeRep a -> TypeRep b -> TypeRep c -> d
translateBinaryError [Char]
"(+)" (forall {k} (a :: k). Typeable a => TypeRep a
R.typeRep @a) (forall {k} (a :: k). Typeable a => TypeRep a
R.typeRep @a) (forall {k} (a :: k). Typeable a => TypeRep a
R.typeRep @a)
lowerSinglePrimImpl' GrisetteSMTConfig integerBitWidth
config t :: Term a
t@(UMinusNumTerm Id
_ Term a
arg) =
case (GrisetteSMTConfig integerBitWidth
config, forall {k} (a :: k). Typeable a => TypeRep a
R.typeRep @a) of
(GrisetteSMTConfig integerBitWidth, TypeRep a)
ResolvedNumType -> forall (integerBitWidth :: Nat) a a1 x x1.
(Typeable x1, a1 ~ TermTy integerBitWidth a, SupportedPrim x,
x1 ~ TermTy integerBitWidth x) =>
GrisetteSMTConfig integerBitWidth
-> Term x
-> Term a
-> (a1 -> x1)
-> State SymBiMap (TermTy integerBitWidth x)
lowerUnaryTerm' GrisetteSMTConfig integerBitWidth
config Term a
t Term a
arg forall a. Num a => a -> a
negate
(GrisetteSMTConfig integerBitWidth, TypeRep a)
_ -> forall {k} {k} (a :: k) (b :: k) c.
HasCallStack =>
[Char] -> TypeRep a -> TypeRep b -> c
translateUnaryError [Char]
"negate" (forall {k} (a :: k). Typeable a => TypeRep a
R.typeRep @a) (forall {k} (a :: k). Typeable a => TypeRep a
R.typeRep @a)
lowerSinglePrimImpl' GrisetteSMTConfig integerBitWidth
config t :: Term a
t@(TimesNumTerm Id
_ Term a
arg1 Term a
arg2) =
case (GrisetteSMTConfig integerBitWidth
config, forall {k} (a :: k). Typeable a => TypeRep a
R.typeRep @a) of
(GrisetteSMTConfig integerBitWidth, TypeRep a)
ResolvedNumType -> forall (integerBitWidth :: Nat) a b a1 b1 x.
(Typeable (TermTy integerBitWidth x),
a1 ~ TermTy integerBitWidth a, b1 ~ TermTy integerBitWidth b,
SupportedPrim x) =>
GrisetteSMTConfig integerBitWidth
-> Term x
-> Term a
-> Term b
-> (a1 -> b1 -> TermTy integerBitWidth x)
-> State SymBiMap (TermTy integerBitWidth x)
lowerBinaryTerm' GrisetteSMTConfig integerBitWidth
config Term a
t Term a
arg1 Term a
arg2 forall a. Num a => a -> a -> a
(*)
(GrisetteSMTConfig integerBitWidth, TypeRep a)
_ -> forall {k} {k} {k} (a :: k) (b :: k) (c :: k) d.
HasCallStack =>
[Char] -> TypeRep a -> TypeRep b -> TypeRep c -> d
translateBinaryError [Char]
"(*)" (forall {k} (a :: k). Typeable a => TypeRep a
R.typeRep @a) (forall {k} (a :: k). Typeable a => TypeRep a
R.typeRep @a) (forall {k} (a :: k). Typeable a => TypeRep a
R.typeRep @a)
lowerSinglePrimImpl' GrisetteSMTConfig integerBitWidth
config t :: Term a
t@(AbsNumTerm Id
_ Term a
arg) =
case (GrisetteSMTConfig integerBitWidth
config, forall {k} (a :: k). Typeable a => TypeRep a
R.typeRep @a) of
(GrisetteSMTConfig integerBitWidth, TypeRep a)
ResolvedNumType -> forall (integerBitWidth :: Nat) a a1 x x1.
(Typeable x1, a1 ~ TermTy integerBitWidth a, SupportedPrim x,
x1 ~ TermTy integerBitWidth x) =>
GrisetteSMTConfig integerBitWidth
-> Term x
-> Term a
-> (a1 -> x1)
-> State SymBiMap (TermTy integerBitWidth x)
lowerUnaryTerm' GrisetteSMTConfig integerBitWidth
config Term a
t Term a
arg forall a. Num a => a -> a
abs
(GrisetteSMTConfig integerBitWidth, TypeRep a)
_ -> forall {k} {k} (a :: k) (b :: k) c.
HasCallStack =>
[Char] -> TypeRep a -> TypeRep b -> c
translateUnaryError [Char]
"abs" (forall {k} (a :: k). Typeable a => TypeRep a
R.typeRep @a) (forall {k} (a :: k). Typeable a => TypeRep a
R.typeRep @a)
lowerSinglePrimImpl' GrisetteSMTConfig integerBitWidth
config t :: Term a
t@(SignumNumTerm Id
_ Term a
arg) =
case (GrisetteSMTConfig integerBitWidth
config, forall {k} (a :: k). Typeable a => TypeRep a
R.typeRep @a) of
(GrisetteSMTConfig integerBitWidth, TypeRep a)
ResolvedNumType -> forall (integerBitWidth :: Nat) a a1 x x1.
(Typeable x1, a1 ~ TermTy integerBitWidth a, SupportedPrim x,
x1 ~ TermTy integerBitWidth x) =>
GrisetteSMTConfig integerBitWidth
-> Term x
-> Term a
-> (a1 -> x1)
-> State SymBiMap (TermTy integerBitWidth x)
lowerUnaryTerm' GrisetteSMTConfig integerBitWidth
config Term a
t Term a
arg forall a. Num a => a -> a
signum
(GrisetteSMTConfig integerBitWidth, TypeRep a)
_ -> forall {k} {k} (a :: k) (b :: k) c.
HasCallStack =>
[Char] -> TypeRep a -> TypeRep b -> c
translateUnaryError [Char]
"signum" (forall {k} (a :: k). Typeable a => TypeRep a
R.typeRep @a) (forall {k} (a :: k). Typeable a => TypeRep a
R.typeRep @a)
lowerSinglePrimImpl' GrisetteSMTConfig integerBitWidth
config t :: Term a
t@(LTNumTerm Id
_ (Term t1
arg1 :: Term arg) Term t1
arg2) =
case (GrisetteSMTConfig integerBitWidth
config, forall {k} (a :: k). Typeable a => TypeRep a
R.typeRep @arg) of
(GrisetteSMTConfig integerBitWidth, TypeRep t1)
ResolvedNumOrdType -> forall (integerBitWidth :: Nat) a b a1 b1 x.
(Typeable (TermTy integerBitWidth x),
a1 ~ TermTy integerBitWidth a, b1 ~ TermTy integerBitWidth b,
SupportedPrim x) =>
GrisetteSMTConfig integerBitWidth
-> Term x
-> Term a
-> Term b
-> (a1 -> b1 -> TermTy integerBitWidth x)
-> State SymBiMap (TermTy integerBitWidth x)
lowerBinaryTerm' GrisetteSMTConfig integerBitWidth
config Term a
t Term t1
arg1 Term t1
arg2 forall a. OrdSymbolic a => a -> a -> SBool
(SBV..<)
(GrisetteSMTConfig integerBitWidth, TypeRep t1)
_ -> forall {k} {k} {k} (a :: k) (b :: k) (c :: k) d.
HasCallStack =>
[Char] -> TypeRep a -> TypeRep b -> TypeRep c -> d
translateBinaryError [Char]
"(<)" (forall {k} (a :: k). Typeable a => TypeRep a
R.typeRep @arg) (forall {k} (a :: k). Typeable a => TypeRep a
R.typeRep @arg) (forall {k} (a :: k). Typeable a => TypeRep a
R.typeRep @Bool)
lowerSinglePrimImpl' GrisetteSMTConfig integerBitWidth
config t :: Term a
t@(LENumTerm Id
_ (Term t1
arg1 :: Term arg) Term t1
arg2) =
case (GrisetteSMTConfig integerBitWidth
config, forall {k} (a :: k). Typeable a => TypeRep a
R.typeRep @arg) of
(GrisetteSMTConfig integerBitWidth, TypeRep t1)
ResolvedNumOrdType -> forall (integerBitWidth :: Nat) a b a1 b1 x.
(Typeable (TermTy integerBitWidth x),
a1 ~ TermTy integerBitWidth a, b1 ~ TermTy integerBitWidth b,
SupportedPrim x) =>
GrisetteSMTConfig integerBitWidth
-> Term x
-> Term a
-> Term b
-> (a1 -> b1 -> TermTy integerBitWidth x)
-> State SymBiMap (TermTy integerBitWidth x)
lowerBinaryTerm' GrisetteSMTConfig integerBitWidth
config Term a
t Term t1
arg1 Term t1
arg2 forall a. OrdSymbolic a => a -> a -> SBool
(SBV..<=)
(GrisetteSMTConfig integerBitWidth, TypeRep t1)
_ -> forall {k} {k} {k} (a :: k) (b :: k) (c :: k) d.
HasCallStack =>
[Char] -> TypeRep a -> TypeRep b -> TypeRep c -> d
translateBinaryError [Char]
"(<=)" (forall {k} (a :: k). Typeable a => TypeRep a
R.typeRep @arg) (forall {k} (a :: k). Typeable a => TypeRep a
R.typeRep @arg) (forall {k} (a :: k). Typeable a => TypeRep a
R.typeRep @Bool)
lowerSinglePrimImpl' GrisetteSMTConfig integerBitWidth
config t :: Term a
t@(AndBitsTerm Id
_ Term a
arg1 Term a
arg2) =
case (GrisetteSMTConfig integerBitWidth
config, forall {k} (a :: k). Typeable a => TypeRep a
R.typeRep @a) of
(GrisetteSMTConfig integerBitWidth, TypeRep a)
ResolvedBitsType -> forall (integerBitWidth :: Nat) a b a1 b1 x.
(Typeable (TermTy integerBitWidth x),
a1 ~ TermTy integerBitWidth a, b1 ~ TermTy integerBitWidth b,
SupportedPrim x) =>
GrisetteSMTConfig integerBitWidth
-> Term x
-> Term a
-> Term b
-> (a1 -> b1 -> TermTy integerBitWidth x)
-> State SymBiMap (TermTy integerBitWidth x)
lowerBinaryTerm' GrisetteSMTConfig integerBitWidth
config Term a
t Term a
arg1 Term a
arg2 forall a. Bits a => a -> a -> a
(.&.)
(GrisetteSMTConfig integerBitWidth, TypeRep a)
_ -> forall {k} {k} {k} (a :: k) (b :: k) (c :: k) d.
HasCallStack =>
[Char] -> TypeRep a -> TypeRep b -> TypeRep c -> d
translateBinaryError [Char]
"(.&.)" (forall {k} (a :: k). Typeable a => TypeRep a
R.typeRep @a) (forall {k} (a :: k). Typeable a => TypeRep a
R.typeRep @a) (forall {k} (a :: k). Typeable a => TypeRep a
R.typeRep @a)
lowerSinglePrimImpl' GrisetteSMTConfig integerBitWidth
config t :: Term a
t@(OrBitsTerm Id
_ Term a
arg1 Term a
arg2) =
case (GrisetteSMTConfig integerBitWidth
config, forall {k} (a :: k). Typeable a => TypeRep a
R.typeRep @a) of
(GrisetteSMTConfig integerBitWidth, TypeRep a)
ResolvedBitsType -> forall (integerBitWidth :: Nat) a b a1 b1 x.
(Typeable (TermTy integerBitWidth x),
a1 ~ TermTy integerBitWidth a, b1 ~ TermTy integerBitWidth b,
SupportedPrim x) =>
GrisetteSMTConfig integerBitWidth
-> Term x
-> Term a
-> Term b
-> (a1 -> b1 -> TermTy integerBitWidth x)
-> State SymBiMap (TermTy integerBitWidth x)
lowerBinaryTerm' GrisetteSMTConfig integerBitWidth
config Term a
t Term a
arg1 Term a
arg2 forall a. Bits a => a -> a -> a
(.|.)
(GrisetteSMTConfig integerBitWidth, TypeRep a)
_ -> forall {k} {k} {k} (a :: k) (b :: k) (c :: k) d.
HasCallStack =>
[Char] -> TypeRep a -> TypeRep b -> TypeRep c -> d
translateBinaryError [Char]
"(.|.)" (forall {k} (a :: k). Typeable a => TypeRep a
R.typeRep @a) (forall {k} (a :: k). Typeable a => TypeRep a
R.typeRep @a) (forall {k} (a :: k). Typeable a => TypeRep a
R.typeRep @a)
lowerSinglePrimImpl' GrisetteSMTConfig integerBitWidth
config t :: Term a
t@(XorBitsTerm Id
_ Term a
arg1 Term a
arg2) =
case (GrisetteSMTConfig integerBitWidth
config, forall {k} (a :: k). Typeable a => TypeRep a
R.typeRep @a) of
(GrisetteSMTConfig integerBitWidth, TypeRep a)
ResolvedBitsType -> forall (integerBitWidth :: Nat) a b a1 b1 x.
(Typeable (TermTy integerBitWidth x),
a1 ~ TermTy integerBitWidth a, b1 ~ TermTy integerBitWidth b,
SupportedPrim x) =>
GrisetteSMTConfig integerBitWidth
-> Term x
-> Term a
-> Term b
-> (a1 -> b1 -> TermTy integerBitWidth x)
-> State SymBiMap (TermTy integerBitWidth x)
lowerBinaryTerm' GrisetteSMTConfig integerBitWidth
config Term a
t Term a
arg1 Term a
arg2 forall a. Bits a => a -> a -> a
xor
(GrisetteSMTConfig integerBitWidth, TypeRep a)
_ -> forall {k} {k} {k} (a :: k) (b :: k) (c :: k) d.
HasCallStack =>
[Char] -> TypeRep a -> TypeRep b -> TypeRep c -> d
translateBinaryError [Char]
"xor" (forall {k} (a :: k). Typeable a => TypeRep a
R.typeRep @a) (forall {k} (a :: k). Typeable a => TypeRep a
R.typeRep @a) (forall {k} (a :: k). Typeable a => TypeRep a
R.typeRep @a)
lowerSinglePrimImpl' GrisetteSMTConfig integerBitWidth
config t :: Term a
t@(ComplementBitsTerm Id
_ Term a
arg) =
case (GrisetteSMTConfig integerBitWidth
config, forall {k} (a :: k). Typeable a => TypeRep a
R.typeRep @a) of
(GrisetteSMTConfig integerBitWidth, TypeRep a)
ResolvedBitsType -> forall (integerBitWidth :: Nat) a a1 x x1.
(Typeable x1, a1 ~ TermTy integerBitWidth a, SupportedPrim x,
x1 ~ TermTy integerBitWidth x) =>
GrisetteSMTConfig integerBitWidth
-> Term x
-> Term a
-> (a1 -> x1)
-> State SymBiMap (TermTy integerBitWidth x)
lowerUnaryTerm' GrisetteSMTConfig integerBitWidth
config Term a
t Term a
arg forall a. Bits a => a -> a
complement
(GrisetteSMTConfig integerBitWidth, TypeRep a)
_ -> forall {k} {k} (a :: k) (b :: k) c.
HasCallStack =>
[Char] -> TypeRep a -> TypeRep b -> c
translateUnaryError [Char]
"complement" (forall {k} (a :: k). Typeable a => TypeRep a
R.typeRep @a) (forall {k} (a :: k). Typeable a => TypeRep a
R.typeRep @a)
lowerSinglePrimImpl' GrisetteSMTConfig integerBitWidth
config t :: Term a
t@(ShiftBitsTerm Id
_ Term a
arg Id
n) =
case (GrisetteSMTConfig integerBitWidth
config, forall {k} (a :: k). Typeable a => TypeRep a
R.typeRep @a) of
(GrisetteSMTConfig integerBitWidth, TypeRep a)
ResolvedBitsType -> forall (integerBitWidth :: Nat) a a1 x x1.
(Typeable x1, a1 ~ TermTy integerBitWidth a, SupportedPrim x,
x1 ~ TermTy integerBitWidth x) =>
GrisetteSMTConfig integerBitWidth
-> Term x
-> Term a
-> (a1 -> x1)
-> State SymBiMap (TermTy integerBitWidth x)
lowerUnaryTerm' GrisetteSMTConfig integerBitWidth
config Term a
t Term a
arg (forall a. Bits a => a -> Id -> a
`shift` Id
n)
(GrisetteSMTConfig integerBitWidth, TypeRep a)
_ -> forall {k} {k} {k} (a :: k) (b :: k) (c :: k) d.
HasCallStack =>
[Char] -> TypeRep a -> TypeRep b -> TypeRep c -> d
translateBinaryError [Char]
"shift" (forall {k} (a :: k). Typeable a => TypeRep a
R.typeRep @a) (forall {k} (a :: k). Typeable a => TypeRep a
R.typeRep @Int) (forall {k} (a :: k). Typeable a => TypeRep a
R.typeRep @a)
lowerSinglePrimImpl' GrisetteSMTConfig integerBitWidth
config t :: Term a
t@(RotateBitsTerm Id
_ Term a
arg Id
n) =
case (GrisetteSMTConfig integerBitWidth
config, forall {k} (a :: k). Typeable a => TypeRep a
R.typeRep @a) of
(GrisetteSMTConfig integerBitWidth, TypeRep a)
ResolvedBitsType -> forall (integerBitWidth :: Nat) a a1 x x1.
(Typeable x1, a1 ~ TermTy integerBitWidth a, SupportedPrim x,
x1 ~ TermTy integerBitWidth x) =>
GrisetteSMTConfig integerBitWidth
-> Term x
-> Term a
-> (a1 -> x1)
-> State SymBiMap (TermTy integerBitWidth x)
lowerUnaryTerm' GrisetteSMTConfig integerBitWidth
config Term a
t Term a
arg (forall a. Bits a => a -> Id -> a
`rotate` Id
n)
(GrisetteSMTConfig integerBitWidth, TypeRep a)
_ -> forall {k} {k} {k} (a :: k) (b :: k) (c :: k) d.
HasCallStack =>
[Char] -> TypeRep a -> TypeRep b -> TypeRep c -> d
translateBinaryError [Char]
"rotate" (forall {k} (a :: k). Typeable a => TypeRep a
R.typeRep @a) (forall {k} (a :: k). Typeable a => TypeRep a
R.typeRep @Int) (forall {k} (a :: k). Typeable a => TypeRep a
R.typeRep @a)
lowerSinglePrimImpl' GrisetteSMTConfig integerBitWidth
config t :: Term a
t@(BVConcatTerm Id
_ (Term (bv a)
bv1 :: Term x) (Term (bv b)
bv2 :: Term y)) =
case (forall {k} (a :: k). Typeable a => TypeRep a
R.typeRep @a, forall {k} (a :: k). Typeable a => TypeRep a
R.typeRep @x, forall {k} (a :: k). Typeable a => TypeRep a
R.typeRep @y) of
(UnsignedBVType (Proxy n
_ :: Proxy na), UnsignedBVType (Proxy n
_ :: Proxy nx), UnsignedBVType (Proxy n
_ :: Proxy ny)) ->
case (forall {k} (a :: k) (b :: k). a :~: b
unsafeAxiom @(nx + ny) @na) of
(n + n) :~: n
Refl -> forall (integerBitWidth :: Nat) a b a1 b1 x.
(Typeable (TermTy integerBitWidth x),
a1 ~ TermTy integerBitWidth a, b1 ~ TermTy integerBitWidth b,
SupportedPrim x) =>
GrisetteSMTConfig integerBitWidth
-> Term x
-> Term a
-> Term b
-> (a1 -> b1 -> TermTy integerBitWidth x)
-> State SymBiMap (TermTy integerBitWidth x)
lowerBinaryTerm' GrisetteSMTConfig integerBitWidth
config Term a
t Term (bv a)
bv1 Term (bv b)
bv2 forall (n :: Nat) (bv :: Nat -> *) (m :: Nat).
(KnownNat n, BVIsNonZero n, SymVal (bv n), KnownNat m,
BVIsNonZero m, SymVal (bv m)) =>
SBV (bv n) -> SBV (bv m) -> SBV (bv (n + m))
(SBV.#)
(SignedBVType (Proxy n
_ :: Proxy na), SignedBVType (Proxy n
_ :: Proxy nx), SignedBVType (Proxy n
_ :: Proxy ny)) ->
case (forall {k} (a :: k) (b :: k). a :~: b
unsafeAxiom @(nx + ny) @na) of
(n + n) :~: n
Refl ->
forall (integerBitWidth :: Nat) a b a1 b1 x.
(Typeable (TermTy integerBitWidth x),
a1 ~ TermTy integerBitWidth a, b1 ~ TermTy integerBitWidth b,
SupportedPrim x) =>
GrisetteSMTConfig integerBitWidth
-> Term x
-> Term a
-> Term b
-> (a1 -> b1 -> TermTy integerBitWidth x)
-> State SymBiMap (TermTy integerBitWidth x)
lowerBinaryTerm'
GrisetteSMTConfig integerBitWidth
config
Term a
t
Term (bv a)
bv1
Term (bv b)
bv2
( \(SInt a
x :: SBV.SInt xn) (SInt b
y :: SBV.SInt yn) ->
forall a b.
(Integral a, HasKind a, Num a, SymVal a, HasKind b, Num b,
SymVal b) =>
SBV a -> SBV b
SBV.sFromIntegral forall a b. (a -> b) -> a -> b
$
(forall a b.
(Integral a, HasKind a, Num a, SymVal a, HasKind b, Num b,
SymVal b) =>
SBV a -> SBV b
SBV.sFromIntegral SInt a
x :: SBV.SWord xn) forall (n :: Nat) (bv :: Nat -> *) (m :: Nat).
(KnownNat n, BVIsNonZero n, SymVal (bv n), KnownNat m,
BVIsNonZero m, SymVal (bv m)) =>
SBV (bv n) -> SBV (bv m) -> SBV (bv (n + m))
SBV.# (forall a b.
(Integral a, HasKind a, Num a, SymVal a, HasKind b, Num b,
SymVal b) =>
SBV a -> SBV b
SBV.sFromIntegral SInt b
y :: SBV.SWord yn)
)
(TypeRep a, TypeRep (bv a), TypeRep (bv b))
_ -> forall {k} {k} {k} (a :: k) (b :: k) (c :: k) d.
HasCallStack =>
[Char] -> TypeRep a -> TypeRep b -> TypeRep c -> d
translateBinaryError [Char]
"bvconcat" (forall {k} (a :: k). Typeable a => TypeRep a
R.typeRep @x) (forall {k} (a :: k). Typeable a => TypeRep a
R.typeRep @y) (forall {k} (a :: k). Typeable a => TypeRep a
R.typeRep @a)
lowerSinglePrimImpl' GrisetteSMTConfig integerBitWidth
config t :: Term a
t@(BVSelectTerm Id
_ (TypeRep ix
ix :: R.TypeRep ix) TypeRep w
w (Term (bv a)
bv :: Term x)) =
case (forall {k} (a :: k). Typeable a => TypeRep a
R.typeRep @a, forall {k} (a :: k). Typeable a => TypeRep a
R.typeRep @x) of
(UnsignedBVType (Proxy n
_ :: Proxy na), UnsignedBVType (Proxy n
_ :: Proxy xn)) ->
forall (n :: Nat) r. NatRepr n -> (KnownNat n => r) -> r
withKnownNat NatRepr ((n + ix) - 1)
n1 forall a b. (a -> b) -> a -> b
$
case ( forall {k} (a :: k) (b :: k). a :~: b
unsafeAxiom @(na + ix - 1 - ix + 1) @na,
forall (m :: Nat) (n :: Nat). LeqProof m n
unsafeLeqProof @(na + ix - 1 + 1) @xn,
forall (m :: Nat) (n :: Nat). LeqProof m n
unsafeLeqProof @ix @(na + ix - 1)
) of
(((((w + ix) - 1) - ix) + 1) :~: w
Refl, LeqProof (((w + ix) - 1) + 1) a
LeqProof, LeqProof ix ((w + ix) - 1)
LeqProof) ->
forall (integerBitWidth :: Nat) a a1 x x1.
(Typeable x1, a1 ~ TermTy integerBitWidth a, SupportedPrim x,
x1 ~ TermTy integerBitWidth x) =>
GrisetteSMTConfig integerBitWidth
-> Term x
-> Term a
-> (a1 -> x1)
-> State SymBiMap (TermTy integerBitWidth x)
lowerUnaryTerm' GrisetteSMTConfig integerBitWidth
config Term a
t Term (bv a)
bv (forall (i :: Nat) (j :: Nat) (n :: Nat) (bv :: Nat -> *)
(proxy :: Nat -> *).
(KnownNat n, BVIsNonZero n, SymVal (bv n), KnownNat i, KnownNat j,
(i + 1) <= n, j <= i, BVIsNonZero ((i - j) + 1)) =>
proxy i -> proxy j -> SBV (bv n) -> SBV (bv ((i - j) + 1))
SBV.bvExtract (forall {k} (t :: k). Proxy t
Proxy @(na + ix - 1)) (forall {k} (t :: k). Proxy t
Proxy @ix))
where
n1 :: NatRepr (na + ix - 1)
n1 :: NatRepr ((n + ix) - 1)
n1 = forall (n :: Nat). Nat -> NatRepr n
NatRepr (forall (n :: Nat) (proxy :: Nat -> *). KnownNat n => proxy n -> Nat
natVal (forall {k} (t :: k). Proxy t
Proxy @na) forall a. Num a => a -> a -> a
+ forall (n :: Nat) (proxy :: Nat -> *). KnownNat n => proxy n -> Nat
natVal (forall {k} (t :: k). Proxy t
Proxy @ix) forall a. Num a => a -> a -> a
- Nat
1)
(SignedBVType (Proxy n
_ :: Proxy na), SignedBVType (Proxy n
_ :: Proxy xn)) ->
forall (n :: Nat) r. NatRepr n -> (KnownNat n => r) -> r
withKnownNat NatRepr ((n + ix) - 1)
n1 forall a b. (a -> b) -> a -> b
$
case ( forall {k} (a :: k) (b :: k). a :~: b
unsafeAxiom @(na + ix - 1 - ix + 1) @na,
forall (m :: Nat) (n :: Nat). LeqProof m n
unsafeLeqProof @(na + ix - 1 + 1) @xn,
forall (m :: Nat) (n :: Nat). LeqProof m n
unsafeLeqProof @ix @(na + ix - 1)
) of
(((((w + ix) - 1) - ix) + 1) :~: w
Refl, LeqProof (((w + ix) - 1) + 1) a
LeqProof, LeqProof ix ((w + ix) - 1)
LeqProof) ->
forall (integerBitWidth :: Nat) a a1 x x1.
(Typeable x1, a1 ~ TermTy integerBitWidth a, SupportedPrim x,
x1 ~ TermTy integerBitWidth x) =>
GrisetteSMTConfig integerBitWidth
-> Term x
-> Term a
-> (a1 -> x1)
-> State SymBiMap (TermTy integerBitWidth x)
lowerUnaryTerm' GrisetteSMTConfig integerBitWidth
config Term a
t Term (bv a)
bv (forall (i :: Nat) (j :: Nat) (n :: Nat) (bv :: Nat -> *)
(proxy :: Nat -> *).
(KnownNat n, BVIsNonZero n, SymVal (bv n), KnownNat i, KnownNat j,
(i + 1) <= n, j <= i, BVIsNonZero ((i - j) + 1)) =>
proxy i -> proxy j -> SBV (bv n) -> SBV (bv ((i - j) + 1))
SBV.bvExtract (forall {k} (t :: k). Proxy t
Proxy @(na + ix - 1)) (forall {k} (t :: k). Proxy t
Proxy @ix))
where
n1 :: NatRepr (na + ix - 1)
n1 :: NatRepr ((n + ix) - 1)
n1 = forall (n :: Nat). Nat -> NatRepr n
NatRepr (forall (n :: Nat) (proxy :: Nat -> *). KnownNat n => proxy n -> Nat
natVal (forall {k} (t :: k). Proxy t
Proxy @na) forall a. Num a => a -> a -> a
+ forall (n :: Nat) (proxy :: Nat -> *). KnownNat n => proxy n -> Nat
natVal (forall {k} (t :: k). Proxy t
Proxy @ix) forall a. Num a => a -> a -> a
- Nat
1)
(TypeRep a, TypeRep (bv a))
_ -> forall {k} {k} {k} {k} (a :: k) (b :: k) (c :: k) (d :: k) e.
HasCallStack =>
[Char] -> TypeRep a -> TypeRep b -> TypeRep c -> TypeRep d -> e
translateTernaryError [Char]
"bvselect" TypeRep ix
ix TypeRep w
w (forall {k} (a :: k). Typeable a => TypeRep a
R.typeRep @x) (forall {k} (a :: k). Typeable a => TypeRep a
R.typeRep @a)
lowerSinglePrimImpl' GrisetteSMTConfig integerBitWidth
config t :: Term a
t@(BVExtendTerm Id
_ Bool
signed (TypeRep n
n :: R.TypeRep n) (Term (bv a)
bv :: Term x)) =
case (forall {k} (a :: k). Typeable a => TypeRep a
R.typeRep @a, forall {k} (a :: k). Typeable a => TypeRep a
R.typeRep @x) of
(UnsignedBVType (Proxy n
_ :: Proxy na), UnsignedBVType (Proxy n
_ :: Proxy nx)) ->
forall (n :: Nat) r. NatRepr n -> (KnownNat n => r) -> r
withKnownNat (forall (n :: Nat). Nat -> NatRepr n
NatRepr (forall (n :: Nat) (proxy :: Nat -> *). KnownNat n => proxy n -> Nat
natVal (forall {k} (t :: k). Proxy t
Proxy @na) forall a. Num a => a -> a -> a
- forall (n :: Nat) (proxy :: Nat -> *). KnownNat n => proxy n -> Nat
natVal (forall {k} (t :: k). Proxy t
Proxy @nx)) :: NatRepr (na - nx)) forall a b. (a -> b) -> a -> b
$
case (forall (m :: Nat) (n :: Nat). LeqProof m n
unsafeLeqProof @(nx + 1) @na, forall (m :: Nat) (n :: Nat). LeqProof m n
unsafeLeqProof @1 @(na - nx)) of
(LeqProof (a + 1) b
LeqProof, LeqProof 1 (b - a)
LeqProof) ->
forall (w :: Nat) r. (1 <= w) => (BVIsNonZero w => r) -> r
bvIsNonZeroFromGEq1 @(na - nx) forall a b. (a -> b) -> a -> b
$
forall (integerBitWidth :: Nat) a a1 x x1.
(Typeable x1, a1 ~ TermTy integerBitWidth a, SupportedPrim x,
x1 ~ TermTy integerBitWidth x) =>
GrisetteSMTConfig integerBitWidth
-> Term x
-> Term a
-> (a1 -> x1)
-> State SymBiMap (TermTy integerBitWidth x)
lowerUnaryTerm' GrisetteSMTConfig integerBitWidth
config Term a
t Term (bv a)
bv (if Bool
signed then forall (n :: Nat) (m :: Nat) (bv :: Nat -> *).
(KnownNat n, BVIsNonZero n, SymVal (bv n), KnownNat m,
BVIsNonZero m, SymVal (bv m), (n + 1) <= m, SFiniteBits (bv n),
SIntegral (bv (m - n)), BVIsNonZero (m - n)) =>
SBV (bv n) -> SBV (bv m)
SBV.signExtend else forall (n :: Nat) (m :: Nat) (bv :: Nat -> *).
(KnownNat n, BVIsNonZero n, SymVal (bv n), KnownNat m,
BVIsNonZero m, SymVal (bv m), (n + 1) <= m, SIntegral (bv (m - n)),
BVIsNonZero (m - n)) =>
SBV (bv n) -> SBV (bv m)
SBV.zeroExtend)
(SignedBVType (Proxy n
_ :: Proxy na), SignedBVType (Proxy n
_ :: Proxy nx)) ->
forall (n :: Nat) r. NatRepr n -> (KnownNat n => r) -> r
withKnownNat (forall (n :: Nat). Nat -> NatRepr n
NatRepr (forall (n :: Nat) (proxy :: Nat -> *). KnownNat n => proxy n -> Nat
natVal (forall {k} (t :: k). Proxy t
Proxy @na) forall a. Num a => a -> a -> a
- forall (n :: Nat) (proxy :: Nat -> *). KnownNat n => proxy n -> Nat
natVal (forall {k} (t :: k). Proxy t
Proxy @nx)) :: NatRepr (na - nx)) forall a b. (a -> b) -> a -> b
$
case (forall (m :: Nat) (n :: Nat). LeqProof m n
unsafeLeqProof @(nx + 1) @na, forall (m :: Nat) (n :: Nat). LeqProof m n
unsafeLeqProof @1 @(na - nx)) of
(LeqProof (a + 1) b
LeqProof, LeqProof 1 (b - a)
LeqProof) ->
forall (w :: Nat) r. (1 <= w) => (BVIsNonZero w => r) -> r
bvIsNonZeroFromGEq1 @(na - nx) forall a b. (a -> b) -> a -> b
$
forall (integerBitWidth :: Nat) a a1 x x1.
(Typeable x1, a1 ~ TermTy integerBitWidth a, SupportedPrim x,
x1 ~ TermTy integerBitWidth x) =>
GrisetteSMTConfig integerBitWidth
-> Term x
-> Term a
-> (a1 -> x1)
-> State SymBiMap (TermTy integerBitWidth x)
lowerUnaryTerm'
GrisetteSMTConfig integerBitWidth
config
Term a
t
Term (bv a)
bv
( if Bool
signed
then forall (n :: Nat) (m :: Nat) (bv :: Nat -> *).
(KnownNat n, BVIsNonZero n, SymVal (bv n), KnownNat m,
BVIsNonZero m, SymVal (bv m), (n + 1) <= m, SFiniteBits (bv n),
SIntegral (bv (m - n)), BVIsNonZero (m - n)) =>
SBV (bv n) -> SBV (bv m)
SBV.signExtend
else \SBV (IntN a)
x ->
forall a b.
(Integral a, HasKind a, Num a, SymVal a, HasKind b, Num b,
SymVal b) =>
SBV a -> SBV b
SBV.sFromIntegral
(forall (n :: Nat) (m :: Nat) (bv :: Nat -> *).
(KnownNat n, BVIsNonZero n, SymVal (bv n), KnownNat m,
BVIsNonZero m, SymVal (bv m), (n + 1) <= m, SIntegral (bv (m - n)),
BVIsNonZero (m - n)) =>
SBV (bv n) -> SBV (bv m)
SBV.zeroExtend (forall a b.
(Integral a, HasKind a, Num a, SymVal a, HasKind b, Num b,
SymVal b) =>
SBV a -> SBV b
SBV.sFromIntegral SBV (IntN a)
x :: SBV.SBV (SBV.WordN nx)) :: SBV.SBV (SBV.WordN na))
)
(TypeRep a, TypeRep (bv a))
_ -> forall {k} {k} {k} {k} (a :: k) (b :: k) (c :: k) (d :: k) e.
HasCallStack =>
[Char] -> TypeRep a -> TypeRep b -> TypeRep c -> TypeRep d -> e
translateTernaryError [Char]
"bvextend" (forall {k} (a :: k). Typeable a => TypeRep a
R.typeRep @Bool) TypeRep n
n (forall {k} (a :: k). Typeable a => TypeRep a
R.typeRep @x) (forall {k} (a :: k). Typeable a => TypeRep a
R.typeRep @a)
lowerSinglePrimImpl' GrisetteSMTConfig integerBitWidth
config t :: Term a
t@(TabularFunApplyTerm Id
_ (Term (a =-> a)
f :: Term (b =-> a)) (Term a
arg :: Term b)) =
case (GrisetteSMTConfig integerBitWidth
config, forall {k} (a :: k). Typeable a => TypeRep a
R.typeRep @a) of
(GrisetteSMTConfig integerBitWidth, TypeRep a)
ResolvedDeepType -> do
TermTy integerBitWidth a -> s'
l1 <- forall (integerBitWidth :: Nat) a.
GrisetteSMTConfig integerBitWidth
-> Term a -> State SymBiMap (TermTy integerBitWidth a)
lowerSinglePrimCached' GrisetteSMTConfig integerBitWidth
config Term (a =-> a)
f
TermTy integerBitWidth a
l2 <- forall (integerBitWidth :: Nat) a.
GrisetteSMTConfig integerBitWidth
-> Term a -> State SymBiMap (TermTy integerBitWidth a)
lowerSinglePrimCached' GrisetteSMTConfig integerBitWidth
config Term a
arg
let g :: s'
g = TermTy integerBitWidth a -> s'
l1 TermTy integerBitWidth a
l2
forall (integerBitWidth :: Nat) a.
(SupportedPrim a, Typeable (TermTy integerBitWidth a)) =>
Term a -> TermTy integerBitWidth a -> State SymBiMap ()
addResult @integerBitWidth Term a
t s'
g
forall (m :: * -> *) a. Monad m => a -> m a
return s'
g
(GrisetteSMTConfig integerBitWidth, TypeRep a)
_ -> forall {k} {k} {k} (a :: k) (b :: k) (c :: k) d.
HasCallStack =>
[Char] -> TypeRep a -> TypeRep b -> TypeRep c -> d
translateBinaryError [Char]
"tabularApply" (forall {k} (a :: k). Typeable a => TypeRep a
R.typeRep @(b =-> a)) (forall {k} (a :: k). Typeable a => TypeRep a
R.typeRep @b) (forall {k} (a :: k). Typeable a => TypeRep a
R.typeRep @a)
lowerSinglePrimImpl' GrisetteSMTConfig integerBitWidth
config t :: Term a
t@(GeneralFunApplyTerm Id
_ (Term (a --> a)
f :: Term (b --> a)) (Term a
arg :: Term b)) =
case (GrisetteSMTConfig integerBitWidth
config, forall {k} (a :: k). Typeable a => TypeRep a
R.typeRep @a) of
(GrisetteSMTConfig integerBitWidth, TypeRep a)
ResolvedDeepType -> do
TermTy integerBitWidth a -> s'
l1 <- forall (integerBitWidth :: Nat) a.
GrisetteSMTConfig integerBitWidth
-> Term a -> State SymBiMap (TermTy integerBitWidth a)
lowerSinglePrimCached' GrisetteSMTConfig integerBitWidth
config Term (a --> a)
f
TermTy integerBitWidth a
l2 <- forall (integerBitWidth :: Nat) a.
GrisetteSMTConfig integerBitWidth
-> Term a -> State SymBiMap (TermTy integerBitWidth a)
lowerSinglePrimCached' GrisetteSMTConfig integerBitWidth
config Term a
arg
let g :: s'
g = TermTy integerBitWidth a -> s'
l1 TermTy integerBitWidth a
l2
forall (integerBitWidth :: Nat) a.
(SupportedPrim a, Typeable (TermTy integerBitWidth a)) =>
Term a -> TermTy integerBitWidth a -> State SymBiMap ()
addResult @integerBitWidth Term a
t s'
g
forall (m :: * -> *) a. Monad m => a -> m a
return s'
g
(GrisetteSMTConfig integerBitWidth, TypeRep a)
_ -> forall {k} {k} {k} (a :: k) (b :: k) (c :: k) d.
HasCallStack =>
[Char] -> TypeRep a -> TypeRep b -> TypeRep c -> d
translateBinaryError [Char]
"generalApply" (forall {k} (a :: k). Typeable a => TypeRep a
R.typeRep @(b --> a)) (forall {k} (a :: k). Typeable a => TypeRep a
R.typeRep @b) (forall {k} (a :: k). Typeable a => TypeRep a
R.typeRep @a)
lowerSinglePrimImpl' GrisetteSMTConfig integerBitWidth
config t :: Term a
t@(DivIntegerTerm Id
_ Term Integer
arg1 Term Integer
arg2) =
case (GrisetteSMTConfig integerBitWidth
config, forall {k} (a :: k). Typeable a => TypeRep a
R.typeRep @a) of
(ResolvedConfig {}, TypeRep a
IntegerType) -> forall (integerBitWidth :: Nat) a b a1 b1 x.
(Typeable (TermTy integerBitWidth x),
a1 ~ TermTy integerBitWidth a, b1 ~ TermTy integerBitWidth b,
SupportedPrim x) =>
GrisetteSMTConfig integerBitWidth
-> Term x
-> Term a
-> Term b
-> (a1 -> b1 -> TermTy integerBitWidth x)
-> State SymBiMap (TermTy integerBitWidth x)
lowerBinaryTerm' GrisetteSMTConfig integerBitWidth
config Term a
t Term Integer
arg1 Term Integer
arg2 forall a. SDivisible a => a -> a -> a
SBV.sDiv
(GrisetteSMTConfig integerBitWidth, TypeRep a)
_ -> forall {k} {k} {k} (a :: k) (b :: k) (c :: k) d.
HasCallStack =>
[Char] -> TypeRep a -> TypeRep b -> TypeRep c -> d
translateBinaryError [Char]
"div" (forall {k} (a :: k). Typeable a => TypeRep a
R.typeRep @a) (forall {k} (a :: k). Typeable a => TypeRep a
R.typeRep @a) (forall {k} (a :: k). Typeable a => TypeRep a
R.typeRep @a)
lowerSinglePrimImpl' GrisetteSMTConfig integerBitWidth
config t :: Term a
t@(ModIntegerTerm Id
_ Term Integer
arg1 Term Integer
arg2) =
case (GrisetteSMTConfig integerBitWidth
config, forall {k} (a :: k). Typeable a => TypeRep a
R.typeRep @a) of
(ResolvedConfig {}, TypeRep a
IntegerType) -> forall (integerBitWidth :: Nat) a b a1 b1 x.
(Typeable (TermTy integerBitWidth x),
a1 ~ TermTy integerBitWidth a, b1 ~ TermTy integerBitWidth b,
SupportedPrim x) =>
GrisetteSMTConfig integerBitWidth
-> Term x
-> Term a
-> Term b
-> (a1 -> b1 -> TermTy integerBitWidth x)
-> State SymBiMap (TermTy integerBitWidth x)
lowerBinaryTerm' GrisetteSMTConfig integerBitWidth
config Term a
t Term Integer
arg1 Term Integer
arg2 forall a. SDivisible a => a -> a -> a
SBV.sMod
(GrisetteSMTConfig integerBitWidth, TypeRep a)
_ -> forall {k} {k} {k} (a :: k) (b :: k) (c :: k) d.
HasCallStack =>
[Char] -> TypeRep a -> TypeRep b -> TypeRep c -> d
translateBinaryError [Char]
"mod" (forall {k} (a :: k). Typeable a => TypeRep a
R.typeRep @a) (forall {k} (a :: k). Typeable a => TypeRep a
R.typeRep @a) (forall {k} (a :: k). Typeable a => TypeRep a
R.typeRep @a)
lowerSinglePrimImpl' GrisetteSMTConfig integerBitWidth
_ Term a
_ = forall a. HasCallStack => a
undefined
buildUTFun11 ::
forall integerBitWidth s1 s2 a.
(SupportedPrim a, SupportedPrim s1, SupportedPrim s2) =>
GrisetteSMTConfig integerBitWidth ->
R.TypeRep s1 ->
R.TypeRep s2 ->
Term a ->
SymBiMap ->
Maybe (SBV.Symbolic (SymBiMap, TermTy integerBitWidth (s1 =-> s2)))
buildUTFun11 :: forall (integerBitWidth :: Nat) s1 s2 a.
(SupportedPrim a, SupportedPrim s1, SupportedPrim s2) =>
GrisetteSMTConfig integerBitWidth
-> TypeRep s1
-> TypeRep s2
-> Term a
-> SymBiMap
-> Maybe (Symbolic (SymBiMap, TermTy integerBitWidth (s1 =-> s2)))
buildUTFun11 GrisetteSMTConfig integerBitWidth
config TypeRep s1
ta TypeRep s2
tb term :: Term a
term@(SymTerm Id
_ TypedSymbol a
ts) SymBiMap
m = case ((GrisetteSMTConfig integerBitWidth
config, TypeRep s1
ta), (GrisetteSMTConfig integerBitWidth
config, TypeRep s2
tb)) of
((GrisetteSMTConfig integerBitWidth, TypeRep s1)
ResolvedSimpleType, (GrisetteSMTConfig integerBitWidth, TypeRep s2)
ResolvedSimpleType) ->
let name :: [Char]
name = [Char]
"ufunc_" forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> [Char]
show (SymBiMap -> Id
sizeBiMap SymBiMap
m)
f :: TermTy integerBitWidth s1 -> TermTy integerBitWidth s2
f = forall a. Uninterpreted a => [Char] -> a
SBV.uninterpret @(TermTy integerBitWidth s1 -> TermTy integerBitWidth s2) [Char]
name
in forall a. a -> Maybe a
Just forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) a. Monad m => a -> m a
return (HasCallStack =>
SomeTerm
-> Dynamic -> [Char] -> SomeTypedSymbol -> SymBiMap -> SymBiMap
addBiMap (forall a. SupportedPrim a => Term a -> SomeTerm
SomeTerm Term a
term) (forall a. Typeable a => a -> Dynamic
toDyn TermTy integerBitWidth s1 -> TermTy integerBitWidth s2
f) [Char]
name (forall t. TypedSymbol t -> SomeTypedSymbol
someTypedSymbol TypedSymbol a
ts) SymBiMap
m, TermTy integerBitWidth s1 -> TermTy integerBitWidth s2
f)
((GrisetteSMTConfig integerBitWidth, TypeRep s1),
(GrisetteSMTConfig integerBitWidth, TypeRep s2))
_ -> forall a. Maybe a
Nothing
buildUTFun11 GrisetteSMTConfig integerBitWidth
_ TypeRep s1
_ TypeRep s2
_ Term a
_ SymBiMap
_ = forall a. HasCallStack => [Char] -> a
error [Char]
"Should only be called on SymTerm"
buildUTFun111 ::
forall integerBitWidth s1 s2 s3 a.
(SupportedPrim a, SupportedPrim s1, SupportedPrim s2, SupportedPrim s3) =>
GrisetteSMTConfig integerBitWidth ->
R.TypeRep s1 ->
R.TypeRep s2 ->
R.TypeRep s3 ->
Term a ->
SymBiMap ->
Maybe (SBV.Symbolic (SymBiMap, TermTy integerBitWidth (s1 =-> s2 =-> s3)))
buildUTFun111 :: forall (integerBitWidth :: Nat) s1 s2 s3 a.
(SupportedPrim a, SupportedPrim s1, SupportedPrim s2,
SupportedPrim s3) =>
GrisetteSMTConfig integerBitWidth
-> TypeRep s1
-> TypeRep s2
-> TypeRep s3
-> Term a
-> SymBiMap
-> Maybe
(Symbolic (SymBiMap, TermTy integerBitWidth (s1 =-> (s2 =-> s3))))
buildUTFun111 GrisetteSMTConfig integerBitWidth
config TypeRep s1
ta TypeRep s2
tb TypeRep s3
tc term :: Term a
term@(SymTerm Id
_ TypedSymbol a
ts) SymBiMap
m = case ((GrisetteSMTConfig integerBitWidth
config, TypeRep s1
ta), (GrisetteSMTConfig integerBitWidth
config, TypeRep s2
tb), (GrisetteSMTConfig integerBitWidth
config, TypeRep s3
tc)) of
((GrisetteSMTConfig integerBitWidth, TypeRep s1)
ResolvedSimpleType, (GrisetteSMTConfig integerBitWidth, TypeRep s2)
ResolvedSimpleType, (GrisetteSMTConfig integerBitWidth, TypeRep s3)
ResolvedSimpleType) ->
let name :: [Char]
name = [Char]
"ufunc_" forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> [Char]
show (SymBiMap -> Id
sizeBiMap SymBiMap
m)
f :: TermTy integerBitWidth s1
-> TermTy integerBitWidth s2 -> TermTy integerBitWidth s3
f =
forall a. Uninterpreted a => [Char] -> a
SBV.uninterpret @(TermTy integerBitWidth s1 -> TermTy integerBitWidth s2 -> TermTy integerBitWidth s3)
[Char]
name
in forall a. a -> Maybe a
Just forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) a. Monad m => a -> m a
return (HasCallStack =>
SomeTerm
-> Dynamic -> [Char] -> SomeTypedSymbol -> SymBiMap -> SymBiMap
addBiMap (forall a. SupportedPrim a => Term a -> SomeTerm
SomeTerm Term a
term) (forall a. Typeable a => a -> Dynamic
toDyn TermTy integerBitWidth s1
-> TermTy integerBitWidth s2 -> TermTy integerBitWidth s3
f) [Char]
name (forall t. TypedSymbol t -> SomeTypedSymbol
someTypedSymbol TypedSymbol a
ts) SymBiMap
m, TermTy integerBitWidth s1
-> TermTy integerBitWidth s2 -> TermTy integerBitWidth s3
f)
((GrisetteSMTConfig integerBitWidth, TypeRep s1),
(GrisetteSMTConfig integerBitWidth, TypeRep s2),
(GrisetteSMTConfig integerBitWidth, TypeRep s3))
_ -> forall a. Maybe a
Nothing
buildUTFun111 GrisetteSMTConfig integerBitWidth
_ TypeRep s1
_ TypeRep s2
_ TypeRep s3
_ Term a
_ SymBiMap
_ = forall a. HasCallStack => [Char] -> a
error [Char]
"Should only be called on SymTerm"
buildUGFun11 ::
forall integerBitWidth s1 s2 a.
(SupportedPrim a, SupportedPrim s1, SupportedPrim s2) =>
GrisetteSMTConfig integerBitWidth ->
R.TypeRep s1 ->
R.TypeRep s2 ->
Term a ->
SymBiMap ->
Maybe (SBV.Symbolic (SymBiMap, TermTy integerBitWidth (s1 --> s2)))
buildUGFun11 :: forall (integerBitWidth :: Nat) s1 s2 a.
(SupportedPrim a, SupportedPrim s1, SupportedPrim s2) =>
GrisetteSMTConfig integerBitWidth
-> TypeRep s1
-> TypeRep s2
-> Term a
-> SymBiMap
-> Maybe (Symbolic (SymBiMap, TermTy integerBitWidth (s1 --> s2)))
buildUGFun11 GrisetteSMTConfig integerBitWidth
config TypeRep s1
ta TypeRep s2
tb term :: Term a
term@(SymTerm Id
_ TypedSymbol a
ts) SymBiMap
m = case ((GrisetteSMTConfig integerBitWidth
config, TypeRep s1
ta), (GrisetteSMTConfig integerBitWidth
config, TypeRep s2
tb)) of
((GrisetteSMTConfig integerBitWidth, TypeRep s1)
ResolvedSimpleType, (GrisetteSMTConfig integerBitWidth, TypeRep s2)
ResolvedSimpleType) ->
let name :: [Char]
name = [Char]
"ufunc_" forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> [Char]
show (SymBiMap -> Id
sizeBiMap SymBiMap
m)
f :: TermTy integerBitWidth s1 -> TermTy integerBitWidth s2
f = forall a. Uninterpreted a => [Char] -> a
SBV.uninterpret @(TermTy integerBitWidth s1 -> TermTy integerBitWidth s2) [Char]
name
in forall a. a -> Maybe a
Just forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) a. Monad m => a -> m a
return (HasCallStack =>
SomeTerm
-> Dynamic -> [Char] -> SomeTypedSymbol -> SymBiMap -> SymBiMap
addBiMap (forall a. SupportedPrim a => Term a -> SomeTerm
SomeTerm Term a
term) (forall a. Typeable a => a -> Dynamic
toDyn TermTy integerBitWidth s1 -> TermTy integerBitWidth s2
f) [Char]
name (forall t. TypedSymbol t -> SomeTypedSymbol
someTypedSymbol TypedSymbol a
ts) SymBiMap
m, TermTy integerBitWidth s1 -> TermTy integerBitWidth s2
f)
((GrisetteSMTConfig integerBitWidth, TypeRep s1),
(GrisetteSMTConfig integerBitWidth, TypeRep s2))
_ -> forall a. Maybe a
Nothing
buildUGFun11 GrisetteSMTConfig integerBitWidth
_ TypeRep s1
_ TypeRep s2
_ Term a
_ SymBiMap
_ = forall a. HasCallStack => [Char] -> a
error [Char]
"Should only be called on SymTerm"
buildUGFun111 ::
forall integerBitWidth s1 s2 s3 a.
(SupportedPrim a, SupportedPrim s1, SupportedPrim s2, SupportedPrim s3) =>
GrisetteSMTConfig integerBitWidth ->
R.TypeRep s1 ->
R.TypeRep s2 ->
R.TypeRep s3 ->
Term a ->
SymBiMap ->
Maybe (SBV.Symbolic (SymBiMap, TermTy integerBitWidth (s1 --> s2 --> s3)))
buildUGFun111 :: forall (integerBitWidth :: Nat) s1 s2 s3 a.
(SupportedPrim a, SupportedPrim s1, SupportedPrim s2,
SupportedPrim s3) =>
GrisetteSMTConfig integerBitWidth
-> TypeRep s1
-> TypeRep s2
-> TypeRep s3
-> Term a
-> SymBiMap
-> Maybe
(Symbolic (SymBiMap, TermTy integerBitWidth (s1 --> (s2 --> s3))))
buildUGFun111 GrisetteSMTConfig integerBitWidth
config TypeRep s1
ta TypeRep s2
tb TypeRep s3
tc term :: Term a
term@(SymTerm Id
_ TypedSymbol a
ts) SymBiMap
m = case ((GrisetteSMTConfig integerBitWidth
config, TypeRep s1
ta), (GrisetteSMTConfig integerBitWidth
config, TypeRep s2
tb), (GrisetteSMTConfig integerBitWidth
config, TypeRep s3
tc)) of
((GrisetteSMTConfig integerBitWidth, TypeRep s1)
ResolvedSimpleType, (GrisetteSMTConfig integerBitWidth, TypeRep s2)
ResolvedSimpleType, (GrisetteSMTConfig integerBitWidth, TypeRep s3)
ResolvedSimpleType) ->
let name :: [Char]
name = [Char]
"ufunc_" forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> [Char]
show (SymBiMap -> Id
sizeBiMap SymBiMap
m)
f :: TermTy integerBitWidth s1
-> TermTy integerBitWidth s2 -> TermTy integerBitWidth s3
f =
forall a. Uninterpreted a => [Char] -> a
SBV.uninterpret @(TermTy integerBitWidth s1 -> TermTy integerBitWidth s2 -> TermTy integerBitWidth s3)
[Char]
name
in forall a. a -> Maybe a
Just forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) a. Monad m => a -> m a
return (HasCallStack =>
SomeTerm
-> Dynamic -> [Char] -> SomeTypedSymbol -> SymBiMap -> SymBiMap
addBiMap (forall a. SupportedPrim a => Term a -> SomeTerm
SomeTerm Term a
term) (forall a. Typeable a => a -> Dynamic
toDyn TermTy integerBitWidth s1
-> TermTy integerBitWidth s2 -> TermTy integerBitWidth s3
f) [Char]
name (forall t. TypedSymbol t -> SomeTypedSymbol
someTypedSymbol TypedSymbol a
ts) SymBiMap
m, TermTy integerBitWidth s1
-> TermTy integerBitWidth s2 -> TermTy integerBitWidth s3
f)
((GrisetteSMTConfig integerBitWidth, TypeRep s1),
(GrisetteSMTConfig integerBitWidth, TypeRep s2),
(GrisetteSMTConfig integerBitWidth, TypeRep s3))
_ -> forall a. Maybe a
Nothing
buildUGFun111 GrisetteSMTConfig integerBitWidth
_ TypeRep s1
_ TypeRep s2
_ TypeRep s3
_ Term a
_ SymBiMap
_ = forall a. HasCallStack => [Char] -> a
error [Char]
"Should only be called on SymTerm"
lowerSinglePrimUFun ::
forall integerBitWidth a.
GrisetteSMTConfig integerBitWidth ->
Term a ->
SymBiMap ->
Maybe (SBV.Symbolic (SymBiMap, TermTy integerBitWidth a))
lowerSinglePrimUFun :: forall (integerBitWidth :: Nat) a.
GrisetteSMTConfig integerBitWidth
-> Term a
-> SymBiMap
-> Maybe (Symbolic (SymBiMap, TermTy integerBitWidth a))
lowerSinglePrimUFun GrisetteSMTConfig integerBitWidth
config t :: Term a
t@(SymTerm Id
_ TypedSymbol a
_) SymBiMap
m =
case forall {k} (a :: k). Typeable a => TypeRep a
R.typeRep @a of
TFun3Type (TypeRep a
t1 :: R.TypeRep a1) (TypeRep b
t2 :: R.TypeRep a2) (TypeRep c
t3 :: R.TypeRep a3) -> forall (integerBitWidth :: Nat) s1 s2 s3 a.
(SupportedPrim a, SupportedPrim s1, SupportedPrim s2,
SupportedPrim s3) =>
GrisetteSMTConfig integerBitWidth
-> TypeRep s1
-> TypeRep s2
-> TypeRep s3
-> Term a
-> SymBiMap
-> Maybe
(Symbolic (SymBiMap, TermTy integerBitWidth (s1 =-> (s2 =-> s3))))
buildUTFun111 GrisetteSMTConfig integerBitWidth
config TypeRep a
t1 TypeRep b
t2 TypeRep c
t3 Term a
t SymBiMap
m
TFunType (TypeRep a
ta :: R.TypeRep b) (TypeRep b
tb :: R.TypeRep b1) -> forall (integerBitWidth :: Nat) s1 s2 a.
(SupportedPrim a, SupportedPrim s1, SupportedPrim s2) =>
GrisetteSMTConfig integerBitWidth
-> TypeRep s1
-> TypeRep s2
-> Term a
-> SymBiMap
-> Maybe (Symbolic (SymBiMap, TermTy integerBitWidth (s1 =-> s2)))
buildUTFun11 GrisetteSMTConfig integerBitWidth
config TypeRep a
ta TypeRep b
tb Term a
t SymBiMap
m
GFun3Type (TypeRep a
t1 :: R.TypeRep a1) (TypeRep b
t2 :: R.TypeRep a2) (TypeRep c
t3 :: R.TypeRep a3) -> forall (integerBitWidth :: Nat) s1 s2 s3 a.
(SupportedPrim a, SupportedPrim s1, SupportedPrim s2,
SupportedPrim s3) =>
GrisetteSMTConfig integerBitWidth
-> TypeRep s1
-> TypeRep s2
-> TypeRep s3
-> Term a
-> SymBiMap
-> Maybe
(Symbolic (SymBiMap, TermTy integerBitWidth (s1 --> (s2 --> s3))))
buildUGFun111 GrisetteSMTConfig integerBitWidth
config TypeRep a
t1 TypeRep b
t2 TypeRep c
t3 Term a
t SymBiMap
m
GFunType (TypeRep a
ta :: R.TypeRep b) (TypeRep b
tb :: R.TypeRep b1) -> forall (integerBitWidth :: Nat) s1 s2 a.
(SupportedPrim a, SupportedPrim s1, SupportedPrim s2) =>
GrisetteSMTConfig integerBitWidth
-> TypeRep s1
-> TypeRep s2
-> Term a
-> SymBiMap
-> Maybe (Symbolic (SymBiMap, TermTy integerBitWidth (s1 --> s2)))
buildUGFun11 GrisetteSMTConfig integerBitWidth
config TypeRep a
ta TypeRep b
tb Term a
t SymBiMap
m
TypeRep a
_ -> forall a. Maybe a
Nothing
lowerSinglePrimUFun GrisetteSMTConfig integerBitWidth
_ Term a
_ SymBiMap
_ = forall a. HasCallStack => [Char] -> a
error [Char]
"Should not call this function"
lowerUnaryTerm ::
forall integerBitWidth a a1 x x1.
(Typeable x1, a1 ~ TermTy integerBitWidth a, SupportedPrim x, HasCallStack) =>
GrisetteSMTConfig integerBitWidth ->
Term x ->
Term a ->
(a1 -> x1) ->
SymBiMap ->
SBV.Symbolic (SymBiMap, x1)
lowerUnaryTerm :: forall (integerBitWidth :: Nat) a a1 x x1.
(Typeable x1, a1 ~ TermTy integerBitWidth a, SupportedPrim x,
HasCallStack) =>
GrisetteSMTConfig integerBitWidth
-> Term x
-> Term a
-> (a1 -> x1)
-> SymBiMap
-> Symbolic (SymBiMap, x1)
lowerUnaryTerm GrisetteSMTConfig integerBitWidth
config Term x
orig Term a
t1 a1 -> x1
f SymBiMap
m = do
(SymBiMap
m1, a1
l1) <- forall (integerBitWidth :: Nat) a.
HasCallStack =>
GrisetteSMTConfig integerBitWidth
-> Term a
-> SymBiMap
-> Symbolic (SymBiMap, TermTy integerBitWidth a)
lowerSinglePrimCached GrisetteSMTConfig integerBitWidth
config Term a
t1 SymBiMap
m
let g :: x1
g = a1 -> x1
f a1
l1
forall (m :: * -> *) a. Monad m => a -> m a
return (HasCallStack => SomeTerm -> Dynamic -> SymBiMap -> SymBiMap
addBiMapIntermediate (forall a. SupportedPrim a => Term a -> SomeTerm
SomeTerm Term x
orig) (forall a. Typeable a => a -> Dynamic
toDyn x1
g) SymBiMap
m1, x1
g)
lowerBinaryTerm ::
forall integerBitWidth a b a1 b1 x x1.
(Typeable x1, a1 ~ TermTy integerBitWidth a, b1 ~ TermTy integerBitWidth b, SupportedPrim x, HasCallStack) =>
GrisetteSMTConfig integerBitWidth ->
Term x ->
Term a ->
Term b ->
(a1 -> b1 -> x1) ->
SymBiMap ->
SBV.Symbolic (SymBiMap, x1)
lowerBinaryTerm :: forall (integerBitWidth :: Nat) a b a1 b1 x x1.
(Typeable x1, a1 ~ TermTy integerBitWidth a,
b1 ~ TermTy integerBitWidth b, SupportedPrim x, HasCallStack) =>
GrisetteSMTConfig integerBitWidth
-> Term x
-> Term a
-> Term b
-> (a1 -> b1 -> x1)
-> SymBiMap
-> Symbolic (SymBiMap, x1)
lowerBinaryTerm GrisetteSMTConfig integerBitWidth
config Term x
orig Term a
t1 Term b
t2 a1 -> b1 -> x1
f SymBiMap
m = do
(SymBiMap
m1, a1
l1) <- forall (integerBitWidth :: Nat) a.
HasCallStack =>
GrisetteSMTConfig integerBitWidth
-> Term a
-> SymBiMap
-> Symbolic (SymBiMap, TermTy integerBitWidth a)
lowerSinglePrimCached GrisetteSMTConfig integerBitWidth
config Term a
t1 SymBiMap
m
(SymBiMap
m2, b1
l2) <- forall (integerBitWidth :: Nat) a.
HasCallStack =>
GrisetteSMTConfig integerBitWidth
-> Term a
-> SymBiMap
-> Symbolic (SymBiMap, TermTy integerBitWidth a)
lowerSinglePrimCached GrisetteSMTConfig integerBitWidth
config Term b
t2 SymBiMap
m1
let g :: x1
g = a1 -> b1 -> x1
f a1
l1 b1
l2
forall (m :: * -> *) a. Monad m => a -> m a
return (HasCallStack => SomeTerm -> Dynamic -> SymBiMap -> SymBiMap
addBiMapIntermediate (forall a. SupportedPrim a => Term a -> SomeTerm
SomeTerm Term x
orig) (forall a. Typeable a => a -> Dynamic
toDyn x1
g) SymBiMap
m2, x1
g)
lowerSinglePrimCached ::
forall integerBitWidth a.
HasCallStack =>
GrisetteSMTConfig integerBitWidth ->
Term a ->
SymBiMap ->
SBV.Symbolic (SymBiMap, TermTy integerBitWidth a)
lowerSinglePrimCached :: forall (integerBitWidth :: Nat) a.
HasCallStack =>
GrisetteSMTConfig integerBitWidth
-> Term a
-> SymBiMap
-> Symbolic (SymBiMap, TermTy integerBitWidth a)
lowerSinglePrimCached GrisetteSMTConfig integerBitWidth
config Term a
t SymBiMap
m =
forall t a. Term t -> (SupportedPrim t => a) -> a
introSupportedPrimConstraint Term a
t forall a b. (a -> b) -> a -> b
$
case (GrisetteSMTConfig integerBitWidth
config, forall {k} (a :: k). Typeable a => TypeRep a
R.typeRep @a) of
(GrisetteSMTConfig integerBitWidth, TypeRep a)
ResolvedDeepType ->
case HasCallStack => SomeTerm -> SymBiMap -> Maybe Dynamic
lookupTerm (forall a. SupportedPrim a => Term a -> SomeTerm
SomeTerm Term a
t) SymBiMap
m of
Just Dynamic
x -> forall (m :: * -> *) a. Monad m => a -> m a
return (SymBiMap
m, forall a. Typeable a => Dynamic -> a -> a
fromDyn Dynamic
x forall a. HasCallStack => a
undefined)
Maybe Dynamic
Nothing -> forall (integerBitWidth :: Nat) a.
HasCallStack =>
GrisetteSMTConfig integerBitWidth
-> Term a
-> SymBiMap
-> Symbolic (SymBiMap, TermTy integerBitWidth a)
lowerSinglePrimImpl GrisetteSMTConfig integerBitWidth
config Term a
t SymBiMap
m
(GrisetteSMTConfig integerBitWidth, TypeRep a)
_ -> forall {k} (a :: k) b. HasCallStack => TypeRep a -> b
translateTypeError (forall {k} (a :: k). Typeable a => TypeRep a
R.typeRep @a)
lowerSinglePrim ::
forall integerBitWidth a.
HasCallStack =>
GrisetteSMTConfig integerBitWidth ->
Term a ->
SBV.Symbolic (SymBiMap, TermTy integerBitWidth a)
lowerSinglePrim :: forall (integerBitWidth :: Nat) a.
HasCallStack =>
GrisetteSMTConfig integerBitWidth
-> Term a -> Symbolic (SymBiMap, TermTy integerBitWidth a)
lowerSinglePrim GrisetteSMTConfig integerBitWidth
config Term a
t = forall (integerBitWidth :: Nat) a.
HasCallStack =>
GrisetteSMTConfig integerBitWidth
-> Term a
-> SymBiMap
-> Symbolic (SymBiMap, TermTy integerBitWidth a)
lowerSinglePrimCached GrisetteSMTConfig integerBitWidth
config Term a
t SymBiMap
emptySymBiMap
translateTypeError :: HasCallStack => R.TypeRep a -> b
translateTypeError :: forall {k} (a :: k) b. HasCallStack => TypeRep a -> b
translateTypeError TypeRep a
ta =
forall a. HasCallStack => [Char] -> a
error forall a b. (a -> b) -> a -> b
$
[Char]
"Don't know how to translate the type " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> [Char]
show TypeRep a
ta forall a. [a] -> [a] -> [a]
++ [Char]
" to SMT"
translateUnaryError :: HasCallStack => String -> R.TypeRep a -> R.TypeRep b -> c
translateUnaryError :: forall {k} {k} (a :: k) (b :: k) c.
HasCallStack =>
[Char] -> TypeRep a -> TypeRep b -> c
translateUnaryError [Char]
op TypeRep a
ta TypeRep b
tb =
forall a. HasCallStack => [Char] -> a
error forall a b. (a -> b) -> a -> b
$
[Char]
"Don't know how to translate the op "
forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> [Char]
show [Char]
op
forall a. [a] -> [a] -> [a]
++ [Char]
" :: "
forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> [Char]
show TypeRep a
ta
forall a. [a] -> [a] -> [a]
++ [Char]
" -> "
forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> [Char]
show TypeRep b
tb
forall a. [a] -> [a] -> [a]
++ [Char]
" to SMT"
translateBinaryError :: HasCallStack => String -> R.TypeRep a -> R.TypeRep b -> R.TypeRep c -> d
translateBinaryError :: forall {k} {k} {k} (a :: k) (b :: k) (c :: k) d.
HasCallStack =>
[Char] -> TypeRep a -> TypeRep b -> TypeRep c -> d
translateBinaryError [Char]
op TypeRep a
ta TypeRep b
tb TypeRep c
tc =
forall a. HasCallStack => [Char] -> a
error forall a b. (a -> b) -> a -> b
$
[Char]
"Don't know how to translate the op "
forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> [Char]
show [Char]
op
forall a. [a] -> [a] -> [a]
++ [Char]
" :: "
forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> [Char]
show TypeRep a
ta
forall a. [a] -> [a] -> [a]
++ [Char]
" -> "
forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> [Char]
show TypeRep b
tb
forall a. [a] -> [a] -> [a]
++ [Char]
" -> "
forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> [Char]
show TypeRep c
tc
forall a. [a] -> [a] -> [a]
++ [Char]
" to SMT"
translateTernaryError :: HasCallStack => String -> R.TypeRep a -> R.TypeRep b -> R.TypeRep c -> R.TypeRep d -> e
translateTernaryError :: forall {k} {k} {k} {k} (a :: k) (b :: k) (c :: k) (d :: k) e.
HasCallStack =>
[Char] -> TypeRep a -> TypeRep b -> TypeRep c -> TypeRep d -> e
translateTernaryError [Char]
op TypeRep a
ta TypeRep b
tb TypeRep c
tc TypeRep d
td =
forall a. HasCallStack => [Char] -> a
error forall a b. (a -> b) -> a -> b
$
[Char]
"Don't know how to translate the op "
forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> [Char]
show [Char]
op
forall a. [a] -> [a] -> [a]
++ [Char]
" :: "
forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> [Char]
show TypeRep a
ta
forall a. [a] -> [a] -> [a]
++ [Char]
" -> "
forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> [Char]
show TypeRep b
tb
forall a. [a] -> [a] -> [a]
++ [Char]
" -> "
forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> [Char]
show TypeRep c
tc
forall a. [a] -> [a] -> [a]
++ [Char]
" -> "
forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> [Char]
show TypeRep d
td
forall a. [a] -> [a] -> [a]
++ [Char]
" to SMT"
lowerSinglePrimImpl ::
forall integerBitWidth a.
HasCallStack =>
GrisetteSMTConfig integerBitWidth ->
Term a ->
SymBiMap ->
SBV.Symbolic (SymBiMap, TermTy integerBitWidth a)
lowerSinglePrimImpl :: forall (integerBitWidth :: Nat) a.
HasCallStack =>
GrisetteSMTConfig integerBitWidth
-> Term a
-> SymBiMap
-> Symbolic (SymBiMap, TermTy integerBitWidth a)
lowerSinglePrimImpl ResolvedConfig {} (ConTerm Id
_ a
v) SymBiMap
m =
case forall {k} (a :: k). Typeable a => TypeRep a
R.typeRep @a of
TypeRep a
BoolType -> forall (m :: * -> *) a. Monad m => a -> m a
return (SymBiMap
m, if a
v then SBool
SBV.sTrue else SBool
SBV.sFalse)
TypeRep a
IntegerType -> forall (m :: * -> *) a. Monad m => a -> m a
return (SymBiMap
m, forall a. Num a => Integer -> a
fromInteger a
v)
SignedBVType Proxy n
_ -> case a
v of
IntN Integer
x -> forall (m :: * -> *) a. Monad m => a -> m a
return (SymBiMap
m, forall a. Num a => Integer -> a
fromInteger Integer
x)
UnsignedBVType Proxy n
_ -> case a
v of
WordN Integer
x -> forall (m :: * -> *) a. Monad m => a -> m a
return (SymBiMap
m, forall a. Num a => Integer -> a
fromInteger Integer
x)
TypeRep a
_ -> forall {k} (a :: k) b. HasCallStack => TypeRep a -> b
translateTypeError (forall {k} (a :: k). Typeable a => TypeRep a
R.typeRep @a)
lowerSinglePrimImpl GrisetteSMTConfig integerBitWidth
config t :: Term a
t@(SymTerm Id
_ TypedSymbol a
ts) SymBiMap
m =
forall a. a -> Maybe a -> a
fromMaybe forall t1. t1
errorMsg forall a b. (a -> b) -> a -> b
$ forall (t :: * -> *) (f :: * -> *) a.
(Foldable t, Alternative f) =>
t (f a) -> f a
asum [Maybe (Symbolic (SymBiMap, TermTy integerBitWidth a))
simple, Maybe (Symbolic (SymBiMap, TermTy integerBitWidth a))
ufunc]
where
errorMsg :: forall x. x
errorMsg :: forall t1. t1
errorMsg = forall {k} (a :: k) b. HasCallStack => TypeRep a -> b
translateTypeError (forall {k} (a :: k). Typeable a => TypeRep a
R.typeRep @a)
simple :: Maybe (SBV.Symbolic (SymBiMap, TermTy integerBitWidth a))
simple :: Maybe (Symbolic (SymBiMap, TermTy integerBitWidth a))
simple = case (GrisetteSMTConfig integerBitWidth
config, forall {k} (a :: k). Typeable a => TypeRep a
R.typeRep @a) of
(GrisetteSMTConfig integerBitWidth, TypeRep a)
ResolvedSimpleType -> forall a. a -> Maybe a
Just forall a b. (a -> b) -> a -> b
$ do
let name :: [Char]
name = forall a. Show a => a -> [Char]
show TypedSymbol a
ts
(TermTy integerBitWidth a
g :: TermTy integerBitWidth a) <- forall a. SymVal a => [Char] -> Symbolic (SBV a)
SBV.free [Char]
name
forall (m :: * -> *) a. Monad m => a -> m a
return (HasCallStack =>
SomeTerm
-> Dynamic -> [Char] -> SomeTypedSymbol -> SymBiMap -> SymBiMap
addBiMap (forall a. SupportedPrim a => Term a -> SomeTerm
SomeTerm Term a
t) (forall a. Typeable a => a -> Dynamic
toDyn TermTy integerBitWidth a
g) [Char]
name (forall t. TypedSymbol t -> SomeTypedSymbol
someTypedSymbol TypedSymbol a
ts) SymBiMap
m, TermTy integerBitWidth a
g)
(GrisetteSMTConfig integerBitWidth, TypeRep a)
_ -> forall a. Maybe a
Nothing
ufunc :: (Maybe (SBV.Symbolic (SymBiMap, TermTy integerBitWidth a)))
ufunc :: Maybe (Symbolic (SymBiMap, TermTy integerBitWidth a))
ufunc = forall (integerBitWidth :: Nat) a.
GrisetteSMTConfig integerBitWidth
-> Term a
-> SymBiMap
-> Maybe (Symbolic (SymBiMap, TermTy integerBitWidth a))
lowerSinglePrimUFun GrisetteSMTConfig integerBitWidth
config Term a
t SymBiMap
m
lowerSinglePrimImpl GrisetteSMTConfig integerBitWidth
_ (UnaryTerm Id
_ tag
op (Term arg
_ :: Term x)) SymBiMap
_ = forall t1. t1
errorMsg
where
errorMsg :: forall t1. t1
errorMsg :: forall t1. t1
errorMsg = forall {k} {k} (a :: k) (b :: k) c.
HasCallStack =>
[Char] -> TypeRep a -> TypeRep b -> c
translateUnaryError (forall a. Show a => a -> [Char]
show tag
op) (forall {k} (a :: k). Typeable a => TypeRep a
R.typeRep @x) (forall {k} (a :: k). Typeable a => TypeRep a
R.typeRep @a)
lowerSinglePrimImpl GrisetteSMTConfig integerBitWidth
_ (BinaryTerm Id
_ tag
op (Term arg1
_ :: Term x) (Term arg2
_ :: Term y)) SymBiMap
_ = forall t1. t1
errorMsg
where
errorMsg :: forall t1. t1
errorMsg :: forall t1. t1
errorMsg = forall {k} {k} {k} (a :: k) (b :: k) (c :: k) d.
HasCallStack =>
[Char] -> TypeRep a -> TypeRep b -> TypeRep c -> d
translateBinaryError (forall a. Show a => a -> [Char]
show tag
op) (forall {k} (a :: k). Typeable a => TypeRep a
R.typeRep @x) (forall {k} (a :: k). Typeable a => TypeRep a
R.typeRep @y) (forall {k} (a :: k). Typeable a => TypeRep a
R.typeRep @a)
lowerSinglePrimImpl ResolvedConfig {} (TernaryTerm Id
_ tag
op (Term arg1
_ :: Term x) (Term arg2
_ :: Term y) (Term arg3
_ :: Term z)) SymBiMap
_ = forall t1. t1
errorMsg
where
errorMsg :: forall t1. t1
errorMsg :: forall t1. t1
errorMsg = forall {k} {k} {k} {k} (a :: k) (b :: k) (c :: k) (d :: k) e.
HasCallStack =>
[Char] -> TypeRep a -> TypeRep b -> TypeRep c -> TypeRep d -> e
translateTernaryError (forall a. Show a => a -> [Char]
show tag
op) (forall {k} (a :: k). Typeable a => TypeRep a
R.typeRep @x) (forall {k} (a :: k). Typeable a => TypeRep a
R.typeRep @y) (forall {k} (a :: k). Typeable a => TypeRep a
R.typeRep @z) (forall {k} (a :: k). Typeable a => TypeRep a
R.typeRep @a)
lowerSinglePrimImpl GrisetteSMTConfig integerBitWidth
config t :: Term a
t@(NotTerm Id
_ Term Bool
arg) SymBiMap
m = forall (integerBitWidth :: Nat) a a1 x x1.
(Typeable x1, a1 ~ TermTy integerBitWidth a, SupportedPrim x,
HasCallStack) =>
GrisetteSMTConfig integerBitWidth
-> Term x
-> Term a
-> (a1 -> x1)
-> SymBiMap
-> Symbolic (SymBiMap, x1)
lowerUnaryTerm GrisetteSMTConfig integerBitWidth
config Term a
t Term Bool
arg SBool -> SBool
SBV.sNot SymBiMap
m
lowerSinglePrimImpl GrisetteSMTConfig integerBitWidth
config t :: Term a
t@(OrTerm Id
_ Term Bool
arg1 Term Bool
arg2) SymBiMap
m = forall (integerBitWidth :: Nat) a b a1 b1 x x1.
(Typeable x1, a1 ~ TermTy integerBitWidth a,
b1 ~ TermTy integerBitWidth b, SupportedPrim x, HasCallStack) =>
GrisetteSMTConfig integerBitWidth
-> Term x
-> Term a
-> Term b
-> (a1 -> b1 -> x1)
-> SymBiMap
-> Symbolic (SymBiMap, x1)
lowerBinaryTerm GrisetteSMTConfig integerBitWidth
config Term a
t Term Bool
arg1 Term Bool
arg2 SBool -> SBool -> SBool
(SBV..||) SymBiMap
m
lowerSinglePrimImpl GrisetteSMTConfig integerBitWidth
config t :: Term a
t@(AndTerm Id
_ Term Bool
arg1 Term Bool
arg2) SymBiMap
m = forall (integerBitWidth :: Nat) a b a1 b1 x x1.
(Typeable x1, a1 ~ TermTy integerBitWidth a,
b1 ~ TermTy integerBitWidth b, SupportedPrim x, HasCallStack) =>
GrisetteSMTConfig integerBitWidth
-> Term x
-> Term a
-> Term b
-> (a1 -> b1 -> x1)
-> SymBiMap
-> Symbolic (SymBiMap, x1)
lowerBinaryTerm GrisetteSMTConfig integerBitWidth
config Term a
t Term Bool
arg1 Term Bool
arg2 SBool -> SBool -> SBool
(SBV..&&) SymBiMap
m
lowerSinglePrimImpl GrisetteSMTConfig integerBitWidth
config t :: Term a
t@(EqvTerm Id
_ (Term t1
arg1 :: Term x) Term t1
arg2) SymBiMap
m =
case (GrisetteSMTConfig integerBitWidth
config, forall {k} (a :: k). Typeable a => TypeRep a
R.typeRep @x) of
(GrisetteSMTConfig integerBitWidth, TypeRep t1)
ResolvedSimpleType -> forall (integerBitWidth :: Nat) a b a1 b1 x x1.
(Typeable x1, a1 ~ TermTy integerBitWidth a,
b1 ~ TermTy integerBitWidth b, SupportedPrim x, HasCallStack) =>
GrisetteSMTConfig integerBitWidth
-> Term x
-> Term a
-> Term b
-> (a1 -> b1 -> x1)
-> SymBiMap
-> Symbolic (SymBiMap, x1)
lowerBinaryTerm GrisetteSMTConfig integerBitWidth
config Term a
t Term t1
arg1 Term t1
arg2 forall a. EqSymbolic a => a -> a -> SBool
(SBV..==) SymBiMap
m
(GrisetteSMTConfig integerBitWidth, TypeRep t1)
_ -> forall {k} {k} {k} (a :: k) (b :: k) (c :: k) d.
HasCallStack =>
[Char] -> TypeRep a -> TypeRep b -> TypeRep c -> d
translateBinaryError [Char]
"(==)" (forall {k} (a :: k). Typeable a => TypeRep a
R.typeRep @x) (forall {k} (a :: k). Typeable a => TypeRep a
R.typeRep @x) (forall {k} (a :: k). Typeable a => TypeRep a
R.typeRep @a)
lowerSinglePrimImpl GrisetteSMTConfig integerBitWidth
config t :: Term a
t@(ITETerm Id
_ Term Bool
cond Term a
arg1 Term a
arg2) SymBiMap
m =
case (GrisetteSMTConfig integerBitWidth
config, forall {k} (a :: k). Typeable a => TypeRep a
R.typeRep @a) of
(GrisetteSMTConfig integerBitWidth, TypeRep a)
ResolvedSimpleType -> do
(SymBiMap
m1, SBool
l1) <- forall (integerBitWidth :: Nat) a.
HasCallStack =>
GrisetteSMTConfig integerBitWidth
-> Term a
-> SymBiMap
-> Symbolic (SymBiMap, TermTy integerBitWidth a)
lowerSinglePrimCached GrisetteSMTConfig integerBitWidth
config Term Bool
cond SymBiMap
m
(SymBiMap
m2, SBV s'
l2) <- forall (integerBitWidth :: Nat) a.
HasCallStack =>
GrisetteSMTConfig integerBitWidth
-> Term a
-> SymBiMap
-> Symbolic (SymBiMap, TermTy integerBitWidth a)
lowerSinglePrimCached GrisetteSMTConfig integerBitWidth
config Term a
arg1 SymBiMap
m1
(SymBiMap
m3, SBV s'
l3) <- forall (integerBitWidth :: Nat) a.
HasCallStack =>
GrisetteSMTConfig integerBitWidth
-> Term a
-> SymBiMap
-> Symbolic (SymBiMap, TermTy integerBitWidth a)
lowerSinglePrimCached GrisetteSMTConfig integerBitWidth
config Term a
arg2 SymBiMap
m2
let g :: SBV s'
g = forall a. Mergeable a => SBool -> a -> a -> a
SBV.ite SBool
l1 SBV s'
l2 SBV s'
l3
forall (m :: * -> *) a. Monad m => a -> m a
return (HasCallStack => SomeTerm -> Dynamic -> SymBiMap -> SymBiMap
addBiMapIntermediate (forall a. SupportedPrim a => Term a -> SomeTerm
SomeTerm Term a
t) (forall a. Typeable a => a -> Dynamic
toDyn SBV s'
g) SymBiMap
m3, SBV s'
g)
(GrisetteSMTConfig integerBitWidth, TypeRep a)
_ -> forall {k} {k} {k} (a :: k) (b :: k) (c :: k) d.
HasCallStack =>
[Char] -> TypeRep a -> TypeRep b -> TypeRep c -> d
translateBinaryError [Char]
"ite" (forall {k} (a :: k). Typeable a => TypeRep a
R.typeRep @Bool) (forall {k} (a :: k). Typeable a => TypeRep a
R.typeRep @a) (forall {k} (a :: k). Typeable a => TypeRep a
R.typeRep @a) (forall {k} (a :: k). Typeable a => TypeRep a
R.typeRep @a)
lowerSinglePrimImpl GrisetteSMTConfig integerBitWidth
config t :: Term a
t@(AddNumTerm Id
_ Term a
arg1 Term a
arg2) SymBiMap
m =
case (GrisetteSMTConfig integerBitWidth
config, forall {k} (a :: k). Typeable a => TypeRep a
R.typeRep @a) of
(GrisetteSMTConfig integerBitWidth, TypeRep a)
ResolvedNumType -> forall (integerBitWidth :: Nat) a b a1 b1 x x1.
(Typeable x1, a1 ~ TermTy integerBitWidth a,
b1 ~ TermTy integerBitWidth b, SupportedPrim x, HasCallStack) =>
GrisetteSMTConfig integerBitWidth
-> Term x
-> Term a
-> Term b
-> (a1 -> b1 -> x1)
-> SymBiMap
-> Symbolic (SymBiMap, x1)
lowerBinaryTerm GrisetteSMTConfig integerBitWidth
config Term a
t Term a
arg1 Term a
arg2 forall a. Num a => a -> a -> a
(+) SymBiMap
m
(GrisetteSMTConfig integerBitWidth, TypeRep a)
_ -> forall {k} {k} {k} (a :: k) (b :: k) (c :: k) d.
HasCallStack =>
[Char] -> TypeRep a -> TypeRep b -> TypeRep c -> d
translateBinaryError [Char]
"(+)" (forall {k} (a :: k). Typeable a => TypeRep a
R.typeRep @a) (forall {k} (a :: k). Typeable a => TypeRep a
R.typeRep @a) (forall {k} (a :: k). Typeable a => TypeRep a
R.typeRep @a)
lowerSinglePrimImpl GrisetteSMTConfig integerBitWidth
config t :: Term a
t@(UMinusNumTerm Id
_ Term a
arg) SymBiMap
m =
case (GrisetteSMTConfig integerBitWidth
config, forall {k} (a :: k). Typeable a => TypeRep a
R.typeRep @a) of
(GrisetteSMTConfig integerBitWidth, TypeRep a)
ResolvedNumType -> forall (integerBitWidth :: Nat) a a1 x x1.
(Typeable x1, a1 ~ TermTy integerBitWidth a, SupportedPrim x,
HasCallStack) =>
GrisetteSMTConfig integerBitWidth
-> Term x
-> Term a
-> (a1 -> x1)
-> SymBiMap
-> Symbolic (SymBiMap, x1)
lowerUnaryTerm GrisetteSMTConfig integerBitWidth
config Term a
t Term a
arg forall a. Num a => a -> a
negate SymBiMap
m
(GrisetteSMTConfig integerBitWidth, TypeRep a)
_ -> forall {k} {k} (a :: k) (b :: k) c.
HasCallStack =>
[Char] -> TypeRep a -> TypeRep b -> c
translateUnaryError [Char]
"negate" (forall {k} (a :: k). Typeable a => TypeRep a
R.typeRep @a) (forall {k} (a :: k). Typeable a => TypeRep a
R.typeRep @a)
lowerSinglePrimImpl GrisetteSMTConfig integerBitWidth
config t :: Term a
t@(TimesNumTerm Id
_ Term a
arg1 Term a
arg2) SymBiMap
m =
case (GrisetteSMTConfig integerBitWidth
config, forall {k} (a :: k). Typeable a => TypeRep a
R.typeRep @a) of
(GrisetteSMTConfig integerBitWidth, TypeRep a)
ResolvedNumType -> forall (integerBitWidth :: Nat) a b a1 b1 x x1.
(Typeable x1, a1 ~ TermTy integerBitWidth a,
b1 ~ TermTy integerBitWidth b, SupportedPrim x, HasCallStack) =>
GrisetteSMTConfig integerBitWidth
-> Term x
-> Term a
-> Term b
-> (a1 -> b1 -> x1)
-> SymBiMap
-> Symbolic (SymBiMap, x1)
lowerBinaryTerm GrisetteSMTConfig integerBitWidth
config Term a
t Term a
arg1 Term a
arg2 forall a. Num a => a -> a -> a
(*) SymBiMap
m
(GrisetteSMTConfig integerBitWidth, TypeRep a)
_ -> forall {k} {k} {k} (a :: k) (b :: k) (c :: k) d.
HasCallStack =>
[Char] -> TypeRep a -> TypeRep b -> TypeRep c -> d
translateBinaryError [Char]
"(*)" (forall {k} (a :: k). Typeable a => TypeRep a
R.typeRep @a) (forall {k} (a :: k). Typeable a => TypeRep a
R.typeRep @a) (forall {k} (a :: k). Typeable a => TypeRep a
R.typeRep @a)
lowerSinglePrimImpl GrisetteSMTConfig integerBitWidth
config t :: Term a
t@(AbsNumTerm Id
_ Term a
arg) SymBiMap
m =
case (GrisetteSMTConfig integerBitWidth
config, forall {k} (a :: k). Typeable a => TypeRep a
R.typeRep @a) of
(GrisetteSMTConfig integerBitWidth, TypeRep a)
ResolvedNumType -> forall (integerBitWidth :: Nat) a a1 x x1.
(Typeable x1, a1 ~ TermTy integerBitWidth a, SupportedPrim x,
HasCallStack) =>
GrisetteSMTConfig integerBitWidth
-> Term x
-> Term a
-> (a1 -> x1)
-> SymBiMap
-> Symbolic (SymBiMap, x1)
lowerUnaryTerm GrisetteSMTConfig integerBitWidth
config Term a
t Term a
arg forall a. Num a => a -> a
abs SymBiMap
m
(GrisetteSMTConfig integerBitWidth, TypeRep a)
_ -> forall {k} {k} (a :: k) (b :: k) c.
HasCallStack =>
[Char] -> TypeRep a -> TypeRep b -> c
translateUnaryError [Char]
"abs" (forall {k} (a :: k). Typeable a => TypeRep a
R.typeRep @a) (forall {k} (a :: k). Typeable a => TypeRep a
R.typeRep @a)
lowerSinglePrimImpl GrisetteSMTConfig integerBitWidth
config t :: Term a
t@(SignumNumTerm Id
_ Term a
arg) SymBiMap
m =
case (GrisetteSMTConfig integerBitWidth
config, forall {k} (a :: k). Typeable a => TypeRep a
R.typeRep @a) of
(GrisetteSMTConfig integerBitWidth, TypeRep a)
ResolvedNumType -> forall (integerBitWidth :: Nat) a a1 x x1.
(Typeable x1, a1 ~ TermTy integerBitWidth a, SupportedPrim x,
HasCallStack) =>
GrisetteSMTConfig integerBitWidth
-> Term x
-> Term a
-> (a1 -> x1)
-> SymBiMap
-> Symbolic (SymBiMap, x1)
lowerUnaryTerm GrisetteSMTConfig integerBitWidth
config Term a
t Term a
arg forall a. Num a => a -> a
signum SymBiMap
m
(GrisetteSMTConfig integerBitWidth, TypeRep a)
_ -> forall {k} {k} (a :: k) (b :: k) c.
HasCallStack =>
[Char] -> TypeRep a -> TypeRep b -> c
translateUnaryError [Char]
"signum" (forall {k} (a :: k). Typeable a => TypeRep a
R.typeRep @a) (forall {k} (a :: k). Typeable a => TypeRep a
R.typeRep @a)
lowerSinglePrimImpl GrisetteSMTConfig integerBitWidth
config t :: Term a
t@(LTNumTerm Id
_ (Term t1
arg1 :: Term arg) Term t1
arg2) SymBiMap
m =
case (GrisetteSMTConfig integerBitWidth
config, forall {k} (a :: k). Typeable a => TypeRep a
R.typeRep @arg) of
(GrisetteSMTConfig integerBitWidth, TypeRep t1)
ResolvedNumOrdType -> forall (integerBitWidth :: Nat) a b a1 b1 x x1.
(Typeable x1, a1 ~ TermTy integerBitWidth a,
b1 ~ TermTy integerBitWidth b, SupportedPrim x, HasCallStack) =>
GrisetteSMTConfig integerBitWidth
-> Term x
-> Term a
-> Term b
-> (a1 -> b1 -> x1)
-> SymBiMap
-> Symbolic (SymBiMap, x1)
lowerBinaryTerm GrisetteSMTConfig integerBitWidth
config Term a
t Term t1
arg1 Term t1
arg2 forall a. OrdSymbolic a => a -> a -> SBool
(SBV..<) SymBiMap
m
(GrisetteSMTConfig integerBitWidth, TypeRep t1)
_ -> forall {k} {k} {k} (a :: k) (b :: k) (c :: k) d.
HasCallStack =>
[Char] -> TypeRep a -> TypeRep b -> TypeRep c -> d
translateBinaryError [Char]
"(<)" (forall {k} (a :: k). Typeable a => TypeRep a
R.typeRep @a) (forall {k} (a :: k). Typeable a => TypeRep a
R.typeRep @a) (forall {k} (a :: k). Typeable a => TypeRep a
R.typeRep @Bool)
lowerSinglePrimImpl GrisetteSMTConfig integerBitWidth
config t :: Term a
t@(LENumTerm Id
_ (Term t1
arg1 :: Term arg) Term t1
arg2) SymBiMap
m =
case (GrisetteSMTConfig integerBitWidth
config, forall {k} (a :: k). Typeable a => TypeRep a
R.typeRep @arg) of
(GrisetteSMTConfig integerBitWidth, TypeRep t1)
ResolvedNumOrdType -> forall (integerBitWidth :: Nat) a b a1 b1 x x1.
(Typeable x1, a1 ~ TermTy integerBitWidth a,
b1 ~ TermTy integerBitWidth b, SupportedPrim x, HasCallStack) =>
GrisetteSMTConfig integerBitWidth
-> Term x
-> Term a
-> Term b
-> (a1 -> b1 -> x1)
-> SymBiMap
-> Symbolic (SymBiMap, x1)
lowerBinaryTerm GrisetteSMTConfig integerBitWidth
config Term a
t Term t1
arg1 Term t1
arg2 forall a. OrdSymbolic a => a -> a -> SBool
(SBV..<=) SymBiMap
m
(GrisetteSMTConfig integerBitWidth, TypeRep t1)
_ -> forall {k} {k} {k} (a :: k) (b :: k) (c :: k) d.
HasCallStack =>
[Char] -> TypeRep a -> TypeRep b -> TypeRep c -> d
translateBinaryError [Char]
"(<=)" (forall {k} (a :: k). Typeable a => TypeRep a
R.typeRep @a) (forall {k} (a :: k). Typeable a => TypeRep a
R.typeRep @a) (forall {k} (a :: k). Typeable a => TypeRep a
R.typeRep @Bool)
lowerSinglePrimImpl GrisetteSMTConfig integerBitWidth
config t :: Term a
t@(AndBitsTerm Id
_ Term a
arg1 Term a
arg2) SymBiMap
m =
case (GrisetteSMTConfig integerBitWidth
config, forall {k} (a :: k). Typeable a => TypeRep a
R.typeRep @a) of
(GrisetteSMTConfig integerBitWidth, TypeRep a)
ResolvedBitsType -> forall (integerBitWidth :: Nat) a b a1 b1 x x1.
(Typeable x1, a1 ~ TermTy integerBitWidth a,
b1 ~ TermTy integerBitWidth b, SupportedPrim x, HasCallStack) =>
GrisetteSMTConfig integerBitWidth
-> Term x
-> Term a
-> Term b
-> (a1 -> b1 -> x1)
-> SymBiMap
-> Symbolic (SymBiMap, x1)
lowerBinaryTerm GrisetteSMTConfig integerBitWidth
config Term a
t Term a
arg1 Term a
arg2 forall a. Bits a => a -> a -> a
(.&.) SymBiMap
m
(GrisetteSMTConfig integerBitWidth, TypeRep a)
_ -> forall {k} {k} {k} (a :: k) (b :: k) (c :: k) d.
HasCallStack =>
[Char] -> TypeRep a -> TypeRep b -> TypeRep c -> d
translateBinaryError [Char]
"(.&.)" (forall {k} (a :: k). Typeable a => TypeRep a
R.typeRep @a) (forall {k} (a :: k). Typeable a => TypeRep a
R.typeRep @a) (forall {k} (a :: k). Typeable a => TypeRep a
R.typeRep @a)
lowerSinglePrimImpl GrisetteSMTConfig integerBitWidth
config t :: Term a
t@(OrBitsTerm Id
_ Term a
arg1 Term a
arg2) SymBiMap
m =
case (GrisetteSMTConfig integerBitWidth
config, forall {k} (a :: k). Typeable a => TypeRep a
R.typeRep @a) of
(GrisetteSMTConfig integerBitWidth, TypeRep a)
ResolvedBitsType -> forall (integerBitWidth :: Nat) a b a1 b1 x x1.
(Typeable x1, a1 ~ TermTy integerBitWidth a,
b1 ~ TermTy integerBitWidth b, SupportedPrim x, HasCallStack) =>
GrisetteSMTConfig integerBitWidth
-> Term x
-> Term a
-> Term b
-> (a1 -> b1 -> x1)
-> SymBiMap
-> Symbolic (SymBiMap, x1)
lowerBinaryTerm GrisetteSMTConfig integerBitWidth
config Term a
t Term a
arg1 Term a
arg2 forall a. Bits a => a -> a -> a
(.|.) SymBiMap
m
(GrisetteSMTConfig integerBitWidth, TypeRep a)
_ -> forall {k} {k} {k} (a :: k) (b :: k) (c :: k) d.
HasCallStack =>
[Char] -> TypeRep a -> TypeRep b -> TypeRep c -> d
translateBinaryError [Char]
"(.|.)" (forall {k} (a :: k). Typeable a => TypeRep a
R.typeRep @a) (forall {k} (a :: k). Typeable a => TypeRep a
R.typeRep @a) (forall {k} (a :: k). Typeable a => TypeRep a
R.typeRep @a)
lowerSinglePrimImpl GrisetteSMTConfig integerBitWidth
config t :: Term a
t@(XorBitsTerm Id
_ Term a
arg1 Term a
arg2) SymBiMap
m =
case (GrisetteSMTConfig integerBitWidth
config, forall {k} (a :: k). Typeable a => TypeRep a
R.typeRep @a) of
(GrisetteSMTConfig integerBitWidth, TypeRep a)
ResolvedBitsType -> forall (integerBitWidth :: Nat) a b a1 b1 x x1.
(Typeable x1, a1 ~ TermTy integerBitWidth a,
b1 ~ TermTy integerBitWidth b, SupportedPrim x, HasCallStack) =>
GrisetteSMTConfig integerBitWidth
-> Term x
-> Term a
-> Term b
-> (a1 -> b1 -> x1)
-> SymBiMap
-> Symbolic (SymBiMap, x1)
lowerBinaryTerm GrisetteSMTConfig integerBitWidth
config Term a
t Term a
arg1 Term a
arg2 forall a. Bits a => a -> a -> a
xor SymBiMap
m
(GrisetteSMTConfig integerBitWidth, TypeRep a)
_ -> forall {k} {k} {k} (a :: k) (b :: k) (c :: k) d.
HasCallStack =>
[Char] -> TypeRep a -> TypeRep b -> TypeRep c -> d
translateBinaryError [Char]
"xor" (forall {k} (a :: k). Typeable a => TypeRep a
R.typeRep @a) (forall {k} (a :: k). Typeable a => TypeRep a
R.typeRep @a) (forall {k} (a :: k). Typeable a => TypeRep a
R.typeRep @a)
lowerSinglePrimImpl GrisetteSMTConfig integerBitWidth
config t :: Term a
t@(ComplementBitsTerm Id
_ Term a
arg) SymBiMap
m =
case (GrisetteSMTConfig integerBitWidth
config, forall {k} (a :: k). Typeable a => TypeRep a
R.typeRep @a) of
(GrisetteSMTConfig integerBitWidth, TypeRep a)
ResolvedBitsType -> forall (integerBitWidth :: Nat) a a1 x x1.
(Typeable x1, a1 ~ TermTy integerBitWidth a, SupportedPrim x,
HasCallStack) =>
GrisetteSMTConfig integerBitWidth
-> Term x
-> Term a
-> (a1 -> x1)
-> SymBiMap
-> Symbolic (SymBiMap, x1)
lowerUnaryTerm GrisetteSMTConfig integerBitWidth
config Term a
t Term a
arg forall a. Bits a => a -> a
complement SymBiMap
m
(GrisetteSMTConfig integerBitWidth, TypeRep a)
_ -> forall {k} {k} (a :: k) (b :: k) c.
HasCallStack =>
[Char] -> TypeRep a -> TypeRep b -> c
translateUnaryError [Char]
"complement" (forall {k} (a :: k). Typeable a => TypeRep a
R.typeRep @a) (forall {k} (a :: k). Typeable a => TypeRep a
R.typeRep @a)
lowerSinglePrimImpl GrisetteSMTConfig integerBitWidth
config t :: Term a
t@(ShiftBitsTerm Id
_ Term a
arg Id
n) SymBiMap
m =
case (GrisetteSMTConfig integerBitWidth
config, forall {k} (a :: k). Typeable a => TypeRep a
R.typeRep @a) of
(GrisetteSMTConfig integerBitWidth, TypeRep a)
ResolvedBitsType -> forall (integerBitWidth :: Nat) a a1 x x1.
(Typeable x1, a1 ~ TermTy integerBitWidth a, SupportedPrim x,
HasCallStack) =>
GrisetteSMTConfig integerBitWidth
-> Term x
-> Term a
-> (a1 -> x1)
-> SymBiMap
-> Symbolic (SymBiMap, x1)
lowerUnaryTerm GrisetteSMTConfig integerBitWidth
config Term a
t Term a
arg (forall a. Bits a => a -> Id -> a
`shift` Id
n) SymBiMap
m
(GrisetteSMTConfig integerBitWidth, TypeRep a)
_ -> forall {k} {k} {k} (a :: k) (b :: k) (c :: k) d.
HasCallStack =>
[Char] -> TypeRep a -> TypeRep b -> TypeRep c -> d
translateBinaryError [Char]
"shift" (forall {k} (a :: k). Typeable a => TypeRep a
R.typeRep @a) (forall {k} (a :: k). Typeable a => TypeRep a
R.typeRep @Int) (forall {k} (a :: k). Typeable a => TypeRep a
R.typeRep @a)
lowerSinglePrimImpl GrisetteSMTConfig integerBitWidth
config t :: Term a
t@(RotateBitsTerm Id
_ Term a
arg Id
n) SymBiMap
m =
case (GrisetteSMTConfig integerBitWidth
config, forall {k} (a :: k). Typeable a => TypeRep a
R.typeRep @a) of
(GrisetteSMTConfig integerBitWidth, TypeRep a)
ResolvedBitsType -> forall (integerBitWidth :: Nat) a a1 x x1.
(Typeable x1, a1 ~ TermTy integerBitWidth a, SupportedPrim x,
HasCallStack) =>
GrisetteSMTConfig integerBitWidth
-> Term x
-> Term a
-> (a1 -> x1)
-> SymBiMap
-> Symbolic (SymBiMap, x1)
lowerUnaryTerm GrisetteSMTConfig integerBitWidth
config Term a
t Term a
arg (forall a. Bits a => a -> Id -> a
`rotate` Id
n) SymBiMap
m
(GrisetteSMTConfig integerBitWidth, TypeRep a)
_ -> forall {k} {k} {k} (a :: k) (b :: k) (c :: k) d.
HasCallStack =>
[Char] -> TypeRep a -> TypeRep b -> TypeRep c -> d
translateBinaryError [Char]
"rotate" (forall {k} (a :: k). Typeable a => TypeRep a
R.typeRep @a) (forall {k} (a :: k). Typeable a => TypeRep a
R.typeRep @Int) (forall {k} (a :: k). Typeable a => TypeRep a
R.typeRep @a)
lowerSinglePrimImpl GrisetteSMTConfig integerBitWidth
config t :: Term a
t@(BVConcatTerm Id
_ (Term (bv a)
bv1 :: Term x) (Term (bv b)
bv2 :: Term y)) SymBiMap
m =
case (forall {k} (a :: k). Typeable a => TypeRep a
R.typeRep @a, forall {k} (a :: k). Typeable a => TypeRep a
R.typeRep @x, forall {k} (a :: k). Typeable a => TypeRep a
R.typeRep @y) of
(UnsignedBVType (Proxy n
_ :: Proxy na), UnsignedBVType (Proxy n
_ :: Proxy nx), UnsignedBVType (Proxy n
_ :: Proxy ny)) ->
case (forall {k} (a :: k) (b :: k). a :~: b
unsafeAxiom @(nx + ny) @na) of
(n + n) :~: n
Refl -> forall (integerBitWidth :: Nat) a b a1 b1 x x1.
(Typeable x1, a1 ~ TermTy integerBitWidth a,
b1 ~ TermTy integerBitWidth b, SupportedPrim x, HasCallStack) =>
GrisetteSMTConfig integerBitWidth
-> Term x
-> Term a
-> Term b
-> (a1 -> b1 -> x1)
-> SymBiMap
-> Symbolic (SymBiMap, x1)
lowerBinaryTerm GrisetteSMTConfig integerBitWidth
config Term a
t Term (bv a)
bv1 Term (bv b)
bv2 forall (n :: Nat) (bv :: Nat -> *) (m :: Nat).
(KnownNat n, BVIsNonZero n, SymVal (bv n), KnownNat m,
BVIsNonZero m, SymVal (bv m)) =>
SBV (bv n) -> SBV (bv m) -> SBV (bv (n + m))
(SBV.#) SymBiMap
m
(SignedBVType (Proxy n
_ :: Proxy na), SignedBVType (Proxy n
_ :: Proxy nx), SignedBVType (Proxy n
_ :: Proxy ny)) ->
case (forall {k} (a :: k) (b :: k). a :~: b
unsafeAxiom @(nx + ny) @na) of
(n + n) :~: n
Refl ->
forall (integerBitWidth :: Nat) a b a1 b1 x x1.
(Typeable x1, a1 ~ TermTy integerBitWidth a,
b1 ~ TermTy integerBitWidth b, SupportedPrim x, HasCallStack) =>
GrisetteSMTConfig integerBitWidth
-> Term x
-> Term a
-> Term b
-> (a1 -> b1 -> x1)
-> SymBiMap
-> Symbolic (SymBiMap, x1)
lowerBinaryTerm
GrisetteSMTConfig integerBitWidth
config
Term a
t
Term (bv a)
bv1
Term (bv b)
bv2
( \(SInt a
x :: SBV.SInt xn) (SInt b
y :: SBV.SInt yn) ->
forall a b.
(Integral a, HasKind a, Num a, SymVal a, HasKind b, Num b,
SymVal b) =>
SBV a -> SBV b
SBV.sFromIntegral forall a b. (a -> b) -> a -> b
$
(forall a b.
(Integral a, HasKind a, Num a, SymVal a, HasKind b, Num b,
SymVal b) =>
SBV a -> SBV b
SBV.sFromIntegral SInt a
x :: SBV.SWord xn) forall (n :: Nat) (bv :: Nat -> *) (m :: Nat).
(KnownNat n, BVIsNonZero n, SymVal (bv n), KnownNat m,
BVIsNonZero m, SymVal (bv m)) =>
SBV (bv n) -> SBV (bv m) -> SBV (bv (n + m))
SBV.# (forall a b.
(Integral a, HasKind a, Num a, SymVal a, HasKind b, Num b,
SymVal b) =>
SBV a -> SBV b
SBV.sFromIntegral SInt b
y :: SBV.SWord yn)
)
SymBiMap
m
(TypeRep a, TypeRep (bv a), TypeRep (bv b))
_ -> forall {k} {k} {k} (a :: k) (b :: k) (c :: k) d.
HasCallStack =>
[Char] -> TypeRep a -> TypeRep b -> TypeRep c -> d
translateBinaryError [Char]
"bvconcat" (forall {k} (a :: k). Typeable a => TypeRep a
R.typeRep @x) (forall {k} (a :: k). Typeable a => TypeRep a
R.typeRep @y) (forall {k} (a :: k). Typeable a => TypeRep a
R.typeRep @a)
lowerSinglePrimImpl GrisetteSMTConfig integerBitWidth
config t :: Term a
t@(BVSelectTerm Id
_ (TypeRep ix
ix :: R.TypeRep ix) TypeRep w
w (Term (bv a)
bv :: Term x)) SymBiMap
m =
case (forall {k} (a :: k). Typeable a => TypeRep a
R.typeRep @a, forall {k} (a :: k). Typeable a => TypeRep a
R.typeRep @x) of
(UnsignedBVType (Proxy n
_ :: Proxy na), UnsignedBVType (Proxy n
_ :: Proxy xn)) ->
forall (n :: Nat) r. NatRepr n -> (KnownNat n => r) -> r
withKnownNat NatRepr ((n + ix) - 1)
n1 forall a b. (a -> b) -> a -> b
$
case ( forall {k} (a :: k) (b :: k). a :~: b
unsafeAxiom @(na + ix - 1 - ix + 1) @na,
forall (m :: Nat) (n :: Nat). LeqProof m n
unsafeLeqProof @(na + ix - 1 + 1) @xn,
forall (m :: Nat) (n :: Nat). LeqProof m n
unsafeLeqProof @ix @(na + ix - 1)
) of
(((((w + ix) - 1) - ix) + 1) :~: w
Refl, LeqProof (((w + ix) - 1) + 1) a
LeqProof, LeqProof ix ((w + ix) - 1)
LeqProof) ->
forall (integerBitWidth :: Nat) a a1 x x1.
(Typeable x1, a1 ~ TermTy integerBitWidth a, SupportedPrim x,
HasCallStack) =>
GrisetteSMTConfig integerBitWidth
-> Term x
-> Term a
-> (a1 -> x1)
-> SymBiMap
-> Symbolic (SymBiMap, x1)
lowerUnaryTerm GrisetteSMTConfig integerBitWidth
config Term a
t Term (bv a)
bv (forall (i :: Nat) (j :: Nat) (n :: Nat) (bv :: Nat -> *)
(proxy :: Nat -> *).
(KnownNat n, BVIsNonZero n, SymVal (bv n), KnownNat i, KnownNat j,
(i + 1) <= n, j <= i, BVIsNonZero ((i - j) + 1)) =>
proxy i -> proxy j -> SBV (bv n) -> SBV (bv ((i - j) + 1))
SBV.bvExtract (forall {k} (t :: k). Proxy t
Proxy @(na + ix - 1)) (forall {k} (t :: k). Proxy t
Proxy @ix)) SymBiMap
m
where
n1 :: NatRepr (na + ix - 1)
n1 :: NatRepr ((n + ix) - 1)
n1 = forall (n :: Nat). Nat -> NatRepr n
NatRepr (forall (n :: Nat) (proxy :: Nat -> *). KnownNat n => proxy n -> Nat
natVal (forall {k} (t :: k). Proxy t
Proxy @na) forall a. Num a => a -> a -> a
+ forall (n :: Nat) (proxy :: Nat -> *). KnownNat n => proxy n -> Nat
natVal (forall {k} (t :: k). Proxy t
Proxy @ix) forall a. Num a => a -> a -> a
- Nat
1)
(SignedBVType (Proxy n
_ :: Proxy na), SignedBVType (Proxy n
_ :: Proxy xn)) ->
forall (n :: Nat) r. NatRepr n -> (KnownNat n => r) -> r
withKnownNat NatRepr ((n + ix) - 1)
n1 forall a b. (a -> b) -> a -> b
$
case ( forall {k} (a :: k) (b :: k). a :~: b
unsafeAxiom @(na + ix - 1 - ix + 1) @na,
forall (m :: Nat) (n :: Nat). LeqProof m n
unsafeLeqProof @(na + ix - 1 + 1) @xn,
forall (m :: Nat) (n :: Nat). LeqProof m n
unsafeLeqProof @ix @(na + ix - 1)
) of
(((((w + ix) - 1) - ix) + 1) :~: w
Refl, LeqProof (((w + ix) - 1) + 1) a
LeqProof, LeqProof ix ((w + ix) - 1)
LeqProof) ->
forall (integerBitWidth :: Nat) a a1 x x1.
(Typeable x1, a1 ~ TermTy integerBitWidth a, SupportedPrim x,
HasCallStack) =>
GrisetteSMTConfig integerBitWidth
-> Term x
-> Term a
-> (a1 -> x1)
-> SymBiMap
-> Symbolic (SymBiMap, x1)
lowerUnaryTerm GrisetteSMTConfig integerBitWidth
config Term a
t Term (bv a)
bv (forall (i :: Nat) (j :: Nat) (n :: Nat) (bv :: Nat -> *)
(proxy :: Nat -> *).
(KnownNat n, BVIsNonZero n, SymVal (bv n), KnownNat i, KnownNat j,
(i + 1) <= n, j <= i, BVIsNonZero ((i - j) + 1)) =>
proxy i -> proxy j -> SBV (bv n) -> SBV (bv ((i - j) + 1))
SBV.bvExtract (forall {k} (t :: k). Proxy t
Proxy @(na + ix - 1)) (forall {k} (t :: k). Proxy t
Proxy @ix)) SymBiMap
m
where
n1 :: NatRepr (na + ix - 1)
n1 :: NatRepr ((n + ix) - 1)
n1 = forall (n :: Nat). Nat -> NatRepr n
NatRepr (forall (n :: Nat) (proxy :: Nat -> *). KnownNat n => proxy n -> Nat
natVal (forall {k} (t :: k). Proxy t
Proxy @na) forall a. Num a => a -> a -> a
+ forall (n :: Nat) (proxy :: Nat -> *). KnownNat n => proxy n -> Nat
natVal (forall {k} (t :: k). Proxy t
Proxy @ix) forall a. Num a => a -> a -> a
- Nat
1)
(TypeRep a, TypeRep (bv a))
_ -> forall {k} {k} {k} {k} (a :: k) (b :: k) (c :: k) (d :: k) e.
HasCallStack =>
[Char] -> TypeRep a -> TypeRep b -> TypeRep c -> TypeRep d -> e
translateTernaryError [Char]
"bvselect" TypeRep ix
ix TypeRep w
w (forall {k} (a :: k). Typeable a => TypeRep a
R.typeRep @x) (forall {k} (a :: k). Typeable a => TypeRep a
R.typeRep @a)
lowerSinglePrimImpl GrisetteSMTConfig integerBitWidth
config t :: Term a
t@(BVExtendTerm Id
_ Bool
signed (TypeRep n
n :: R.TypeRep n) (Term (bv a)
bv :: Term x)) SymBiMap
m =
case (forall {k} (a :: k). Typeable a => TypeRep a
R.typeRep @a, forall {k} (a :: k). Typeable a => TypeRep a
R.typeRep @x) of
(UnsignedBVType (Proxy n
_ :: Proxy na), UnsignedBVType (Proxy n
_ :: Proxy nx)) ->
forall (n :: Nat) r. NatRepr n -> (KnownNat n => r) -> r
withKnownNat (forall (n :: Nat). Nat -> NatRepr n
NatRepr (forall (n :: Nat) (proxy :: Nat -> *). KnownNat n => proxy n -> Nat
natVal (forall {k} (t :: k). Proxy t
Proxy @na) forall a. Num a => a -> a -> a
- forall (n :: Nat) (proxy :: Nat -> *). KnownNat n => proxy n -> Nat
natVal (forall {k} (t :: k). Proxy t
Proxy @nx)) :: NatRepr (na - nx)) forall a b. (a -> b) -> a -> b
$
case (forall (m :: Nat) (n :: Nat). LeqProof m n
unsafeLeqProof @(nx + 1) @na, forall (m :: Nat) (n :: Nat). LeqProof m n
unsafeLeqProof @1 @(na - nx)) of
(LeqProof (a + 1) b
LeqProof, LeqProof 1 (b - a)
LeqProof) ->
forall (w :: Nat) r. (1 <= w) => (BVIsNonZero w => r) -> r
bvIsNonZeroFromGEq1 @(na - nx) forall a b. (a -> b) -> a -> b
$
forall (integerBitWidth :: Nat) a a1 x x1.
(Typeable x1, a1 ~ TermTy integerBitWidth a, SupportedPrim x,
HasCallStack) =>
GrisetteSMTConfig integerBitWidth
-> Term x
-> Term a
-> (a1 -> x1)
-> SymBiMap
-> Symbolic (SymBiMap, x1)
lowerUnaryTerm GrisetteSMTConfig integerBitWidth
config Term a
t Term (bv a)
bv (if Bool
signed then forall (n :: Nat) (m :: Nat) (bv :: Nat -> *).
(KnownNat n, BVIsNonZero n, SymVal (bv n), KnownNat m,
BVIsNonZero m, SymVal (bv m), (n + 1) <= m, SFiniteBits (bv n),
SIntegral (bv (m - n)), BVIsNonZero (m - n)) =>
SBV (bv n) -> SBV (bv m)
SBV.signExtend else forall (n :: Nat) (m :: Nat) (bv :: Nat -> *).
(KnownNat n, BVIsNonZero n, SymVal (bv n), KnownNat m,
BVIsNonZero m, SymVal (bv m), (n + 1) <= m, SIntegral (bv (m - n)),
BVIsNonZero (m - n)) =>
SBV (bv n) -> SBV (bv m)
SBV.zeroExtend) SymBiMap
m
(SignedBVType (Proxy n
_ :: Proxy na), SignedBVType (Proxy n
_ :: Proxy nx)) ->
forall (n :: Nat) r. NatRepr n -> (KnownNat n => r) -> r
withKnownNat (forall (n :: Nat). Nat -> NatRepr n
NatRepr (forall (n :: Nat) (proxy :: Nat -> *). KnownNat n => proxy n -> Nat
natVal (forall {k} (t :: k). Proxy t
Proxy @na) forall a. Num a => a -> a -> a
- forall (n :: Nat) (proxy :: Nat -> *). KnownNat n => proxy n -> Nat
natVal (forall {k} (t :: k). Proxy t
Proxy @nx)) :: NatRepr (na - nx)) forall a b. (a -> b) -> a -> b
$
case (forall (m :: Nat) (n :: Nat). LeqProof m n
unsafeLeqProof @(nx + 1) @na, forall (m :: Nat) (n :: Nat). LeqProof m n
unsafeLeqProof @1 @(na - nx)) of
(LeqProof (a + 1) b
LeqProof, LeqProof 1 (b - a)
LeqProof) ->
forall (w :: Nat) r. (1 <= w) => (BVIsNonZero w => r) -> r
bvIsNonZeroFromGEq1 @(na - nx) forall a b. (a -> b) -> a -> b
$
forall (integerBitWidth :: Nat) a a1 x x1.
(Typeable x1, a1 ~ TermTy integerBitWidth a, SupportedPrim x,
HasCallStack) =>
GrisetteSMTConfig integerBitWidth
-> Term x
-> Term a
-> (a1 -> x1)
-> SymBiMap
-> Symbolic (SymBiMap, x1)
lowerUnaryTerm
GrisetteSMTConfig integerBitWidth
config
Term a
t
Term (bv a)
bv
( if Bool
signed
then forall (n :: Nat) (m :: Nat) (bv :: Nat -> *).
(KnownNat n, BVIsNonZero n, SymVal (bv n), KnownNat m,
BVIsNonZero m, SymVal (bv m), (n + 1) <= m, SFiniteBits (bv n),
SIntegral (bv (m - n)), BVIsNonZero (m - n)) =>
SBV (bv n) -> SBV (bv m)
SBV.signExtend
else \SBV (IntN a)
x ->
forall a b.
(Integral a, HasKind a, Num a, SymVal a, HasKind b, Num b,
SymVal b) =>
SBV a -> SBV b
SBV.sFromIntegral
(forall (n :: Nat) (m :: Nat) (bv :: Nat -> *).
(KnownNat n, BVIsNonZero n, SymVal (bv n), KnownNat m,
BVIsNonZero m, SymVal (bv m), (n + 1) <= m, SIntegral (bv (m - n)),
BVIsNonZero (m - n)) =>
SBV (bv n) -> SBV (bv m)
SBV.zeroExtend (forall a b.
(Integral a, HasKind a, Num a, SymVal a, HasKind b, Num b,
SymVal b) =>
SBV a -> SBV b
SBV.sFromIntegral SBV (IntN a)
x :: SBV.SBV (SBV.WordN nx)) :: SBV.SBV (SBV.WordN na))
)
SymBiMap
m
(TypeRep a, TypeRep (bv a))
_ -> forall {k} {k} {k} {k} (a :: k) (b :: k) (c :: k) (d :: k) e.
HasCallStack =>
[Char] -> TypeRep a -> TypeRep b -> TypeRep c -> TypeRep d -> e
translateTernaryError [Char]
"bvextend" (forall {k} (a :: k). Typeable a => TypeRep a
R.typeRep @Bool) TypeRep n
n (forall {k} (a :: k). Typeable a => TypeRep a
R.typeRep @x) (forall {k} (a :: k). Typeable a => TypeRep a
R.typeRep @a)
lowerSinglePrimImpl GrisetteSMTConfig integerBitWidth
config t :: Term a
t@(TabularFunApplyTerm Id
_ (Term (a =-> a)
f :: Term (b =-> a)) (Term a
arg :: Term b)) SymBiMap
m =
case (GrisetteSMTConfig integerBitWidth
config, forall {k} (a :: k). Typeable a => TypeRep a
R.typeRep @a) of
(GrisetteSMTConfig integerBitWidth, TypeRep a)
ResolvedDeepType -> do
(SymBiMap
m1, TermTy integerBitWidth a -> s'
l1) <- forall (integerBitWidth :: Nat) a.
HasCallStack =>
GrisetteSMTConfig integerBitWidth
-> Term a
-> SymBiMap
-> Symbolic (SymBiMap, TermTy integerBitWidth a)
lowerSinglePrimCached GrisetteSMTConfig integerBitWidth
config Term (a =-> a)
f SymBiMap
m
(SymBiMap
m2, TermTy integerBitWidth a
l2) <- forall (integerBitWidth :: Nat) a.
HasCallStack =>
GrisetteSMTConfig integerBitWidth
-> Term a
-> SymBiMap
-> Symbolic (SymBiMap, TermTy integerBitWidth a)
lowerSinglePrimCached GrisetteSMTConfig integerBitWidth
config Term a
arg SymBiMap
m1
let g :: s'
g = TermTy integerBitWidth a -> s'
l1 TermTy integerBitWidth a
l2
forall (m :: * -> *) a. Monad m => a -> m a
return (HasCallStack => SomeTerm -> Dynamic -> SymBiMap -> SymBiMap
addBiMapIntermediate (forall a. SupportedPrim a => Term a -> SomeTerm
SomeTerm Term a
t) (forall a. Typeable a => a -> Dynamic
toDyn s'
g) SymBiMap
m2, s'
g)
(GrisetteSMTConfig integerBitWidth, TypeRep a)
_ -> forall {k} {k} {k} (a :: k) (b :: k) (c :: k) d.
HasCallStack =>
[Char] -> TypeRep a -> TypeRep b -> TypeRep c -> d
translateBinaryError [Char]
"tabularApply" (forall {k} (a :: k). Typeable a => TypeRep a
R.typeRep @(b =-> a)) (forall {k} (a :: k). Typeable a => TypeRep a
R.typeRep @b) (forall {k} (a :: k). Typeable a => TypeRep a
R.typeRep @a)
lowerSinglePrimImpl GrisetteSMTConfig integerBitWidth
config t :: Term a
t@(GeneralFunApplyTerm Id
_ (Term (a --> a)
f :: Term (b --> a)) (Term a
arg :: Term b)) SymBiMap
m =
case (GrisetteSMTConfig integerBitWidth
config, forall {k} (a :: k). Typeable a => TypeRep a
R.typeRep @a) of
(GrisetteSMTConfig integerBitWidth, TypeRep a)
ResolvedDeepType -> do
(SymBiMap
m1, TermTy integerBitWidth a -> s'
l1) <- forall (integerBitWidth :: Nat) a.
HasCallStack =>
GrisetteSMTConfig integerBitWidth
-> Term a
-> SymBiMap
-> Symbolic (SymBiMap, TermTy integerBitWidth a)
lowerSinglePrimCached GrisetteSMTConfig integerBitWidth
config Term (a --> a)
f SymBiMap
m
(SymBiMap
m2, TermTy integerBitWidth a
l2) <- forall (integerBitWidth :: Nat) a.
HasCallStack =>
GrisetteSMTConfig integerBitWidth
-> Term a
-> SymBiMap
-> Symbolic (SymBiMap, TermTy integerBitWidth a)
lowerSinglePrimCached GrisetteSMTConfig integerBitWidth
config Term a
arg SymBiMap
m1
let g :: s'
g = TermTy integerBitWidth a -> s'
l1 TermTy integerBitWidth a
l2
forall (m :: * -> *) a. Monad m => a -> m a
return (HasCallStack => SomeTerm -> Dynamic -> SymBiMap -> SymBiMap
addBiMapIntermediate (forall a. SupportedPrim a => Term a -> SomeTerm
SomeTerm Term a
t) (forall a. Typeable a => a -> Dynamic
toDyn s'
g) SymBiMap
m2, s'
g)
(GrisetteSMTConfig integerBitWidth, TypeRep a)
_ -> forall {k} {k} {k} (a :: k) (b :: k) (c :: k) d.
HasCallStack =>
[Char] -> TypeRep a -> TypeRep b -> TypeRep c -> d
translateBinaryError [Char]
"generalApply" (forall {k} (a :: k). Typeable a => TypeRep a
R.typeRep @(b --> a)) (forall {k} (a :: k). Typeable a => TypeRep a
R.typeRep @b) (forall {k} (a :: k). Typeable a => TypeRep a
R.typeRep @a)
lowerSinglePrimImpl GrisetteSMTConfig integerBitWidth
config t :: Term a
t@(DivIntegerTerm Id
_ Term Integer
arg1 Term Integer
arg2) SymBiMap
m =
case (GrisetteSMTConfig integerBitWidth
config, forall {k} (a :: k). Typeable a => TypeRep a
R.typeRep @a) of
(ResolvedConfig {}, TypeRep a
IntegerType) -> forall (integerBitWidth :: Nat) a b a1 b1 x x1.
(Typeable x1, a1 ~ TermTy integerBitWidth a,
b1 ~ TermTy integerBitWidth b, SupportedPrim x, HasCallStack) =>
GrisetteSMTConfig integerBitWidth
-> Term x
-> Term a
-> Term b
-> (a1 -> b1 -> x1)
-> SymBiMap
-> Symbolic (SymBiMap, x1)
lowerBinaryTerm GrisetteSMTConfig integerBitWidth
config Term a
t Term Integer
arg1 Term Integer
arg2 forall a. SDivisible a => a -> a -> a
SBV.sDiv SymBiMap
m
(GrisetteSMTConfig integerBitWidth, TypeRep a)
_ -> forall {k} {k} {k} (a :: k) (b :: k) (c :: k) d.
HasCallStack =>
[Char] -> TypeRep a -> TypeRep b -> TypeRep c -> d
translateBinaryError [Char]
"div" (forall {k} (a :: k). Typeable a => TypeRep a
R.typeRep @a) (forall {k} (a :: k). Typeable a => TypeRep a
R.typeRep @a) (forall {k} (a :: k). Typeable a => TypeRep a
R.typeRep @a)
lowerSinglePrimImpl GrisetteSMTConfig integerBitWidth
config t :: Term a
t@(ModIntegerTerm Id
_ Term Integer
arg1 Term Integer
arg2) SymBiMap
m =
case (GrisetteSMTConfig integerBitWidth
config, forall {k} (a :: k). Typeable a => TypeRep a
R.typeRep @a) of
(ResolvedConfig {}, TypeRep a
IntegerType) -> forall (integerBitWidth :: Nat) a b a1 b1 x x1.
(Typeable x1, a1 ~ TermTy integerBitWidth a,
b1 ~ TermTy integerBitWidth b, SupportedPrim x, HasCallStack) =>
GrisetteSMTConfig integerBitWidth
-> Term x
-> Term a
-> Term b
-> (a1 -> b1 -> x1)
-> SymBiMap
-> Symbolic (SymBiMap, x1)
lowerBinaryTerm GrisetteSMTConfig integerBitWidth
config Term a
t Term Integer
arg1 Term Integer
arg2 forall a. SDivisible a => a -> a -> a
SBV.sMod SymBiMap
m
(GrisetteSMTConfig integerBitWidth, TypeRep a)
_ -> forall {k} {k} {k} (a :: k) (b :: k) (c :: k) d.
HasCallStack =>
[Char] -> TypeRep a -> TypeRep b -> TypeRep c -> d
translateBinaryError [Char]
"mod" (forall {k} (a :: k). Typeable a => TypeRep a
R.typeRep @a) (forall {k} (a :: k). Typeable a => TypeRep a
R.typeRep @a) (forall {k} (a :: k). Typeable a => TypeRep a
R.typeRep @a)
lowerSinglePrimImpl GrisetteSMTConfig integerBitWidth
_ Term a
_ SymBiMap
_ = forall a. HasCallStack => [Char] -> a
error [Char]
"Should never happen"
unsafeMkNatRepr :: Int -> NatRepr w
unsafeMkNatRepr :: forall (w :: Nat). Id -> NatRepr w
unsafeMkNatRepr Id
x = forall (n :: Nat). Nat -> NatRepr n
NatRepr (forall a. Num a => Integer -> a
fromInteger forall a b. (a -> b) -> a -> b
$ forall a. Integral a => a -> Integer
toInteger Id
x)
unsafeWithNonZeroKnownNat :: forall w r. Int -> ((KnownNat w, 1 <= w) => r) -> r
unsafeWithNonZeroKnownNat :: forall (w :: Nat) r. Id -> ((KnownNat w, 1 <= w) => r) -> r
unsafeWithNonZeroKnownNat Id
i (KnownNat w, 1 <= w) => r
r
| Id
i forall a. Ord a => a -> a -> Bool
<= Id
0 = forall a. HasCallStack => [Char] -> a
error [Char]
"Not an nonzero natural number"
| Bool
otherwise = forall (n :: Nat) r. NatRepr n -> (KnownNat n => r) -> r
withKnownNat @w (forall (w :: Nat). Id -> NatRepr w
unsafeMkNatRepr Id
i) forall a b. (a -> b) -> a -> b
$ ((1 <= w) => r) -> r
unsafeBVIsNonZero (KnownNat w, 1 <= w) => r
r
where
unsafeBVIsNonZero :: ((1 <= w) => r) -> r
unsafeBVIsNonZero :: ((1 <= w) => r) -> r
unsafeBVIsNonZero (1 <= w) => r
r1 = case forall {k} (a :: k) (b :: k). a :~: b
unsafeAxiom :: w :~: 1 of
w :~: 1
Refl -> (1 <= w) => r
r1
bvIsNonZeroFromGEq1 :: forall w r. (1 <= w) => ((SBV.BVIsNonZero w) => r) -> r
bvIsNonZeroFromGEq1 :: forall (w :: Nat) r. (1 <= w) => (BVIsNonZero w => r) -> r
bvIsNonZeroFromGEq1 BVIsNonZero w => r
r1 = case forall {k} (a :: k) (b :: k). a :~: b
unsafeAxiom :: w :~: 1 of
w :~: 1
Refl -> BVIsNonZero w => r
r1
parseModel :: forall integerBitWidth. GrisetteSMTConfig integerBitWidth -> SBVI.SMTModel -> SymBiMap -> PM.Model
parseModel :: forall (integerBitWidth :: Nat).
GrisetteSMTConfig integerBitWidth -> SMTModel -> SymBiMap -> Model
parseModel GrisetteSMTConfig integerBitWidth
_ (SBVI.SMTModel [([Char], GeneralizedCV)]
_ Maybe [((Quantifier, NamedSymVar), Maybe CV)]
_ [([Char], CV)]
assoc [([Char], (SBVType, ([([CV], CV)], CV)))]
uifuncs) SymBiMap
mp = forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr ([Char], (SBVType, ([([CV], CV)], CV))) -> Model -> Model
gouifuncs (forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr ([Char], CV) -> Model -> Model
goassoc forall model symbolSet (typedSymbol :: * -> *).
ModelOps model symbolSet typedSymbol =>
model
emptyModel [([Char], CV)]
assoc) [([Char], (SBVType, ([([CV], CV)], CV)))]
uifuncs
where
goassoc :: (String, SBVI.CV) -> PM.Model -> PM.Model
goassoc :: ([Char], CV) -> Model -> Model
goassoc ([Char]
name, CV
cv) Model
m = case [Char] -> SymBiMap -> Maybe SomeTypedSymbol
findStringToSymbol [Char]
name SymBiMap
mp of
Just (SomeTypedSymbol TypeRep t
tr TypedSymbol t
s) ->
forall model symbolSet (typedSymbol :: * -> *) t.
ModelOps model symbolSet typedSymbol =>
typedSymbol t -> t -> model -> model
insertValue TypedSymbol t
s (forall a. TypeRep a -> CV -> a
resolveSingle TypeRep t
tr CV
cv) Model
m
Maybe SomeTypedSymbol
Nothing -> forall a. HasCallStack => [Char] -> a
error [Char]
"Bad"
resolveSingle :: R.TypeRep a -> SBVI.CV -> a
resolveSingle :: forall a. TypeRep a -> CV -> a
resolveSingle TypeRep a
t (SBVI.CV Kind
SBVI.KBool (SBVI.CInteger Integer
n)) =
case forall k1 k2 (a :: k1) (b :: k2).
TypeRep a -> TypeRep b -> Maybe (a :~~: b)
R.eqTypeRep TypeRep a
t (forall {k} (a :: k). Typeable a => TypeRep a
R.typeRep @Bool) of
Just a :~~: Bool
R.HRefl -> Integer
n forall a. Eq a => a -> a -> Bool
/= Integer
0
Maybe (a :~~: Bool)
Nothing -> forall a. HasCallStack => [Char] -> a
error [Char]
"Bad type"
resolveSingle TypeRep a
t (SBVI.CV Kind
SBVI.KUnbounded (SBVI.CInteger Integer
i)) =
case forall k1 k2 (a :: k1) (b :: k2).
TypeRep a -> TypeRep b -> Maybe (a :~~: b)
R.eqTypeRep TypeRep a
t (forall {k} (a :: k). Typeable a => TypeRep a
R.typeRep @Integer) of
Just a :~~: Integer
R.HRefl -> Integer
i
Maybe (a :~~: Integer)
Nothing -> forall a. HasCallStack => [Char] -> a
error [Char]
"Bad type"
resolveSingle TypeRep a
t (SBVI.CV (SBVI.KBounded Bool
_ Id
bitWidth) (SBVI.CInteger Integer
i)) =
case forall k1 k2 (a :: k1) (b :: k2).
TypeRep a -> TypeRep b -> Maybe (a :~~: b)
R.eqTypeRep TypeRep a
t (forall {k} (a :: k). Typeable a => TypeRep a
R.typeRep @Integer) of
Just a :~~: Integer
R.HRefl -> Integer
i
Maybe (a :~~: Integer)
_ -> case TypeRep a
t of
R.App TypeRep a
a (TypeRep b
n :: R.TypeRep w) ->
case forall k1 k2 (a :: k1) (b :: k2).
TypeRep a -> TypeRep b -> Maybe (a :~~: b)
R.eqTypeRep (forall k (a :: k). TypeRep a -> TypeRep k
R.typeRepKind TypeRep b
n) (forall {k} (a :: k). Typeable a => TypeRep a
R.typeRep @Nat) of
Just k1 :~~: Nat
R.HRefl ->
forall (w :: Nat) r. Id -> ((KnownNat w, 1 <= w) => r) -> r
unsafeWithNonZeroKnownNat @w Id
bitWidth forall a b. (a -> b) -> a -> b
$
case (forall k1 k2 (a :: k1) (b :: k2).
TypeRep a -> TypeRep b -> Maybe (a :~~: b)
R.eqTypeRep TypeRep a
a (forall {k} (a :: k). Typeable a => TypeRep a
R.typeRep @IntN), forall k1 k2 (a :: k1) (b :: k2).
TypeRep a -> TypeRep b -> Maybe (a :~~: b)
R.eqTypeRep TypeRep a
a (forall {k} (a :: k). Typeable a => TypeRep a
R.typeRep @WordN)) of
(Just a :~~: IntN
R.HRefl, Maybe (a :~~: WordN)
_) ->
forall a. Num a => Integer -> a
fromInteger Integer
i
(Maybe (a :~~: IntN)
_, Just a :~~: WordN
R.HRefl) -> forall a. Num a => Integer -> a
fromInteger Integer
i
(Maybe (a :~~: IntN), Maybe (a :~~: WordN))
_ -> forall a. HasCallStack => [Char] -> a
error [Char]
"Bad type"
Maybe (k1 :~~: Nat)
_ -> forall a. HasCallStack => [Char] -> a
error [Char]
"Bad type"
TypeRep a
_ -> forall a. HasCallStack => [Char] -> a
error [Char]
"Bad type"
resolveSingle TypeRep a
_ CV
_ = forall a. HasCallStack => [Char] -> a
error [Char]
"Unknown cv"
buildConstFun :: (SupportedPrim a, SupportedPrim r) => R.TypeRep a -> R.TypeRep r -> SBVI.CV -> a =-> r
buildConstFun :: forall a r.
(SupportedPrim a, SupportedPrim r) =>
TypeRep a -> TypeRep r -> CV -> a =-> r
buildConstFun TypeRep a
_ TypeRep r
tr CV
v = case TypeRep r
tr of
TFunType (TypeRep a
ta2' :: R.TypeRep a2) (TypeRep b
tr2' :: R.TypeRep r2) -> forall a b. [(a, b)] -> b -> a =-> b
TabularFun [] forall a b. (a -> b) -> a -> b
$ forall a r.
(SupportedPrim a, SupportedPrim r) =>
TypeRep a -> TypeRep r -> CV -> a =-> r
buildConstFun TypeRep a
ta2' TypeRep b
tr2' CV
v
TypeRep r
_ -> forall a b. [(a, b)] -> b -> a =-> b
TabularFun [] forall a b. (a -> b) -> a -> b
$ forall a. TypeRep a -> CV -> a
resolveSingle TypeRep r
tr CV
v
goutfuncResolve ::
forall a r.
(SupportedPrim a, SupportedPrim r) =>
R.TypeRep a ->
R.TypeRep r ->
([([SBVI.CV], SBVI.CV)], SBVI.CV) ->
(a =-> r)
goutfuncResolve :: forall a r.
(SupportedPrim a, SupportedPrim r) =>
TypeRep a -> TypeRep r -> ([([CV], CV)], CV) -> a =-> r
goutfuncResolve TypeRep a
ta1 TypeRep r
ta2 ([([CV], CV)]
l, CV
s) =
case TypeRep r
ta2 of
TFunType (TypeRep a
ta2' :: R.TypeRep a2) (TypeRep b
tr2' :: R.TypeRep r2) ->
forall a b. [(a, b)] -> b -> a =-> b
TabularFun
(forall (p :: * -> * -> *) b c a.
Bifunctor p =>
(b -> c) -> p a b -> p a c
second (\[([CV], CV)]
r -> forall a r.
(SupportedPrim a, SupportedPrim r) =>
TypeRep a -> TypeRep r -> ([([CV], CV)], CV) -> a =-> r
goutfuncResolve TypeRep a
ta2' TypeRep b
tr2' ([([CV], CV)]
r, CV
s)) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall a. TypeRep a -> [([CV], CV)] -> [(a, [([CV], CV)])]
partition TypeRep a
ta1 [([CV], CV)]
l)
(forall a r.
(SupportedPrim a, SupportedPrim r) =>
TypeRep a -> TypeRep r -> CV -> a =-> r
buildConstFun TypeRep a
ta2' TypeRep b
tr2' CV
s)
TypeRep r
_ ->
forall a b. [(a, b)] -> b -> a =-> b
TabularFun
(forall (p :: * -> * -> *) a b c d.
Bifunctor p =>
(a -> b) -> (c -> d) -> p a c -> p b d
bimap (forall a. TypeRep a -> CV -> a
resolveSingle TypeRep a
ta1 forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. [a] -> a
head) (forall a. TypeRep a -> CV -> a
resolveSingle TypeRep r
ta2) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [([CV], CV)]
l)
(forall a. TypeRep a -> CV -> a
resolveSingle TypeRep r
ta2 CV
s)
gougfuncResolve ::
forall a r.
(SupportedPrim a, SupportedPrim r) =>
Int ->
R.TypeRep a ->
R.TypeRep r ->
([([SBVI.CV], SBVI.CV)], SBVI.CV) ->
(a --> r)
gougfuncResolve :: forall a r.
(SupportedPrim a, SupportedPrim r) =>
Id -> TypeRep a -> TypeRep r -> ([([CV], CV)], CV) -> a --> r
gougfuncResolve Id
idx TypeRep a
ta1 TypeRep r
ta2 ([([CV], CV)]
l, CV
s) =
case TypeRep r
ta2 of
GFunType (TypeRep a
ta2' :: R.TypeRep a2) (TypeRep b
tr2' :: R.TypeRep r2) ->
let sym :: TypedSymbol a
sym = forall t a.
(SupportedPrim t, Typeable a, Ord a, Lift a, NFData a, Show a,
Hashable a) =>
TypedSymbol t -> a -> TypedSymbol t
WithInfo (forall t. SupportedPrim t => [Char] -> Id -> TypedSymbol t
IndexedSymbol [Char]
"arg" Id
idx) FunArg
FunArg
funs :: [(a, a --> b)]
funs = forall (p :: * -> * -> *) b c a.
Bifunctor p =>
(b -> c) -> p a b -> p a c
second (\[([CV], CV)]
r -> forall a r.
(SupportedPrim a, SupportedPrim r) =>
Id -> TypeRep a -> TypeRep r -> ([([CV], CV)], CV) -> a --> r
gougfuncResolve (Id
idx forall a. Num a => a -> a -> a
+ Id
1) TypeRep a
ta2' TypeRep b
tr2' ([([CV], CV)]
r, CV
s)) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall a. TypeRep a -> [([CV], CV)] -> [(a, [([CV], CV)])]
partition TypeRep a
ta1 [([CV], CV)]
l
def :: a --> b
def = forall a r.
(SupportedPrim a, SupportedPrim r) =>
Id -> TypeRep a -> TypeRep r -> ([([CV], CV)], CV) -> a --> r
gougfuncResolve (Id
idx forall a. Num a => a -> a -> a
+ Id
1) TypeRep a
ta2' TypeRep b
tr2' ([], CV
s)
body :: Term (a --> b)
body =
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl'
( \Term (a --> b)
acc (a
v, a --> b
f) ->
forall a.
SupportedPrim a =>
Term Bool -> Term a -> Term a -> Term a
pevalITETerm
(forall a. SupportedPrim a => Term a -> Term a -> Term Bool
pevalEqvTerm (forall t a.
(SupportedPrim t, Typeable t, Typeable a, Ord a, Lift a, NFData a,
Show a, Hashable a) =>
[Char] -> Id -> a -> Term t
iinfosymTerm [Char]
"arg" Id
idx FunArg
FunArg) (forall t.
(SupportedPrim t, Typeable t, Hashable t, Eq t, Show t) =>
t -> Term t
conTerm a
v))
(forall t.
(SupportedPrim t, Typeable t, Hashable t, Eq t, Show t) =>
t -> Term t
conTerm a --> b
f)
Term (a --> b)
acc
)
(forall t.
(SupportedPrim t, Typeable t, Hashable t, Eq t, Show t) =>
t -> Term t
conTerm a --> b
def)
[(a, a --> b)]
funs
in forall a b.
(SupportedPrim a, SupportedPrim b) =>
TypedSymbol a -> Term b -> a --> b
GeneralFun TypedSymbol a
sym Term (a --> b)
body
TypeRep r
_ ->
let sym :: TypedSymbol a
sym = forall t a.
(SupportedPrim t, Typeable a, Ord a, Lift a, NFData a, Show a,
Hashable a) =>
TypedSymbol t -> a -> TypedSymbol t
WithInfo (forall t. SupportedPrim t => [Char] -> Id -> TypedSymbol t
IndexedSymbol [Char]
"arg" Id
idx) FunArg
FunArg
vs :: [(a, r)]
vs = forall (p :: * -> * -> *) a b c d.
Bifunctor p =>
(a -> b) -> (c -> d) -> p a c -> p b d
bimap (forall a. TypeRep a -> CV -> a
resolveSingle TypeRep a
ta1 forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. [a] -> a
head) (forall a. TypeRep a -> CV -> a
resolveSingle TypeRep r
ta2) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [([CV], CV)]
l
def :: r
def = forall a. TypeRep a -> CV -> a
resolveSingle TypeRep r
ta2 CV
s
body :: Term r
body =
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl'
( \Term r
acc (a
v, r
a) ->
forall a.
SupportedPrim a =>
Term Bool -> Term a -> Term a -> Term a
pevalITETerm
(forall a. SupportedPrim a => Term a -> Term a -> Term Bool
pevalEqvTerm (forall t a.
(SupportedPrim t, Typeable t, Typeable a, Ord a, Lift a, NFData a,
Show a, Hashable a) =>
[Char] -> Id -> a -> Term t
iinfosymTerm [Char]
"arg" Id
idx FunArg
FunArg) (forall t.
(SupportedPrim t, Typeable t, Hashable t, Eq t, Show t) =>
t -> Term t
conTerm a
v))
(forall t.
(SupportedPrim t, Typeable t, Hashable t, Eq t, Show t) =>
t -> Term t
conTerm r
a)
Term r
acc
)
(forall t.
(SupportedPrim t, Typeable t, Hashable t, Eq t, Show t) =>
t -> Term t
conTerm r
def)
[(a, r)]
vs
in forall a b.
(SupportedPrim a, SupportedPrim b) =>
TypedSymbol a -> Term b -> a --> b
GeneralFun TypedSymbol a
sym Term r
body
partition :: R.TypeRep a -> [([SBVI.CV], SBVI.CV)] -> [(a, [([SBVI.CV], SBVI.CV)])]
partition :: forall a. TypeRep a -> [([CV], CV)] -> [(a, [([CV], CV)])]
partition TypeRep a
t = case (forall k1 k2 (a :: k1) (b :: k2).
TypeRep a -> TypeRep b -> Maybe (a :~~: b)
R.eqTypeRep TypeRep a
t (forall {k} (a :: k). Typeable a => TypeRep a
R.typeRep @Bool), forall k1 k2 (a :: k1) (b :: k2).
TypeRep a -> TypeRep b -> Maybe (a :~~: b)
R.eqTypeRep TypeRep a
t (forall {k} (a :: k). Typeable a => TypeRep a
R.typeRep @Integer)) of
(Just a :~~: Bool
R.HRefl, Maybe (a :~~: Integer)
_) -> forall a. Ord a => [(a, [([CV], CV)])] -> [(a, [([CV], CV)])]
partitionWithOrd forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. TypeRep a -> [([CV], CV)] -> [(a, [([CV], CV)])]
resolveFirst TypeRep a
t
(Maybe (a :~~: Bool)
_, Just a :~~: Integer
R.HRefl) -> forall a. Ord a => [(a, [([CV], CV)])] -> [(a, [([CV], CV)])]
partitionWithOrd forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. TypeRep a -> [([CV], CV)] -> [(a, [([CV], CV)])]
resolveFirst TypeRep a
t
(Maybe (a :~~: Bool), Maybe (a :~~: Integer))
_ -> case TypeRep a
t of
R.App TypeRep a
bv TypeRep b
_ -> case (forall k1 k2 (a :: k1) (b :: k2).
TypeRep a -> TypeRep b -> Maybe (a :~~: b)
R.eqTypeRep TypeRep a
bv (forall {k} (a :: k). Typeable a => TypeRep a
R.typeRep @IntN), forall k1 k2 (a :: k1) (b :: k2).
TypeRep a -> TypeRep b -> Maybe (a :~~: b)
R.eqTypeRep TypeRep a
bv (forall {k} (a :: k). Typeable a => TypeRep a
R.typeRep @WordN)) of
(Just a :~~: IntN
R.HRefl, Maybe (a :~~: WordN)
_) -> forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (forall (p :: * -> * -> *) a b c.
Bifunctor p =>
(a -> b) -> p a c -> p b c
first forall (n :: Nat). Integer -> IntN n
IntN) forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. Ord a => [(a, [([CV], CV)])] -> [(a, [([CV], CV)])]
partitionWithOrd forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (forall (p :: * -> * -> *) a b c.
Bifunctor p =>
(a -> b) -> p a c -> p b c
first forall (n :: Nat). IntN n -> Integer
unIntN) forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. TypeRep a -> [([CV], CV)] -> [(a, [([CV], CV)])]
resolveFirst TypeRep a
t
(Maybe (a :~~: IntN)
_, Just a :~~: WordN
R.HRefl) -> forall a. Ord a => [(a, [([CV], CV)])] -> [(a, [([CV], CV)])]
partitionWithOrd forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. TypeRep a -> [([CV], CV)] -> [(a, [([CV], CV)])]
resolveFirst TypeRep a
t
(Maybe (a :~~: IntN), Maybe (a :~~: WordN))
_ -> forall a. HasCallStack => [Char] -> a
error [Char]
"Unknown type"
TypeRep a
_ -> forall a. HasCallStack => [Char] -> a
error [Char]
"Unknown type"
resolveFirst :: R.TypeRep a -> [([SBVI.CV], SBVI.CV)] -> [(a, [([SBVI.CV], SBVI.CV)])]
resolveFirst :: forall a. TypeRep a -> [([CV], CV)] -> [(a, [([CV], CV)])]
resolveFirst TypeRep a
tf = forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (\case (CV
x : [CV]
xs, CV
v) -> (forall a. TypeRep a -> CV -> a
resolveSingle TypeRep a
tf CV
x, [([CV]
xs, CV
v)]); ([CV], CV)
_ -> forall a. HasCallStack => [Char] -> a
error [Char]
"impossible")
partitionWithOrd :: forall a. Ord a => [(a, [([SBVI.CV], SBVI.CV)])] -> [(a, [([SBVI.CV], SBVI.CV)])]
partitionWithOrd :: forall a. Ord a => [(a, [([CV], CV)])] -> [(a, [([CV], CV)])]
partitionWithOrd [(a, [([CV], CV)])]
v = forall {a} {a}. Eq a => [(a, [a])] -> [(a, [a])]
go [(a, [([CV], CV)])]
sorted
where
sorted :: [(a, [([CV], CV)])]
sorted = forall b a. Ord b => (a -> b) -> [a] -> [a]
sortWith forall a b. (a, b) -> a
fst [(a, [([CV], CV)])]
v
go :: [(a, [a])] -> [(a, [a])]
go ((a, [a])
x : (a, [a])
x1 : [(a, [a])]
xs) =
if forall a b. (a, b) -> a
fst (a, [a])
x forall a. Eq a => a -> a -> Bool
== forall a b. (a, b) -> a
fst (a, [a])
x1
then [(a, [a])] -> [(a, [a])]
go forall a b. (a -> b) -> a -> b
$ (forall a b. (a, b) -> a
fst (a, [a])
x, forall a b. (a, b) -> b
snd (a, [a])
x forall a. [a] -> [a] -> [a]
++ forall a b. (a, b) -> b
snd (a, [a])
x1) forall a. a -> [a] -> [a]
: [(a, [a])]
xs
else (a, [a])
x forall a. a -> [a] -> [a]
: [(a, [a])] -> [(a, [a])]
go ((a, [a])
x1 forall a. a -> [a] -> [a]
: [(a, [a])]
xs)
go [(a, [a])]
x = [(a, [a])]
x
gouifuncs :: (String, (SBVI.SBVType, ([([SBVI.CV], SBVI.CV)], SBVI.CV))) -> PM.Model -> PM.Model
gouifuncs :: ([Char], (SBVType, ([([CV], CV)], CV))) -> Model -> Model
gouifuncs ([Char]
name, (SBVI.SBVType [Kind]
_, ([([CV], CV)], CV)
l)) Model
m = case [Char] -> SymBiMap -> Maybe SomeTypedSymbol
findStringToSymbol [Char]
name SymBiMap
mp of
Just (SomeTypedSymbol TypeRep t
tr TypedSymbol t
s) -> forall t a. TypedSymbol t -> (SupportedPrim t => a) -> a
withSymbolSupported TypedSymbol t
s forall a b. (a -> b) -> a -> b
$ case TypeRep t
tr of
t :: TypeRep t
t@(TFunType TypeRep a
a TypeRep b
r) -> forall k (a :: k) r. TypeRep a -> (Typeable a => r) -> r
R.withTypeable TypeRep t
t forall a b. (a -> b) -> a -> b
$ forall model symbolSet (typedSymbol :: * -> *) t.
ModelOps model symbolSet typedSymbol =>
typedSymbol t -> t -> model -> model
insertValue TypedSymbol t
s (forall a r.
(SupportedPrim a, SupportedPrim r) =>
TypeRep a -> TypeRep r -> ([([CV], CV)], CV) -> a =-> r
goutfuncResolve TypeRep a
a TypeRep b
r ([([CV], CV)], CV)
l) Model
m
t :: TypeRep t
t@(GFunType TypeRep a
a TypeRep b
r) -> forall k (a :: k) r. TypeRep a -> (Typeable a => r) -> r
R.withTypeable TypeRep t
t forall a b. (a -> b) -> a -> b
$ forall model symbolSet (typedSymbol :: * -> *) t.
ModelOps model symbolSet typedSymbol =>
typedSymbol t -> t -> model -> model
insertValue TypedSymbol t
s (forall a r.
(SupportedPrim a, SupportedPrim r) =>
Id -> TypeRep a -> TypeRep r -> ([([CV], CV)], CV) -> a --> r
gougfuncResolve Id
0 TypeRep a
a TypeRep b
r ([([CV], CV)], CV)
l) Model
m
TypeRep t
_ -> forall a. HasCallStack => [Char] -> a
error [Char]
"Bad"
Maybe SomeTypedSymbol
Nothing -> forall a. HasCallStack => [Char] -> a
error [Char]
"Bad"
data BVTypeContainer bv k where
BVTypeContainer :: (SBV.BVIsNonZero n, KnownNat n, 1 <= n, k ~ bv n) => Proxy n -> BVTypeContainer bv k
signedBVTypeView :: forall t. (SupportedPrim t) => R.TypeRep t -> Maybe (BVTypeContainer IntN t)
signedBVTypeView :: forall t.
SupportedPrim t =>
TypeRep t -> Maybe (BVTypeContainer IntN t)
signedBVTypeView TypeRep t
t = case TypeRep t
t of
R.App TypeRep a
s (TypeRep b
n :: R.TypeRep w) ->
case (forall k1 k2 (a :: k1) (b :: k2).
TypeRep a -> TypeRep b -> Maybe (a :~~: b)
R.eqTypeRep TypeRep a
s (forall {k} (a :: k). Typeable a => TypeRep a
R.typeRep @IntN), forall k1 k2 (a :: k1) (b :: k2).
TypeRep a -> TypeRep b -> Maybe (a :~~: b)
R.eqTypeRep (forall k (a :: k). TypeRep a -> TypeRep k
R.typeRepKind TypeRep b
n) (forall {k} (a :: k). Typeable a => TypeRep a
R.typeRep @Nat)) of
(Just a :~~: IntN
R.HRefl, Just k1 :~~: Nat
R.HRefl) ->
forall a. a -> Maybe a
Just forall a b. (a -> b) -> a -> b
$ forall (w :: Nat) r. (BVIsNonZero w => r) -> r
unsafeBVIsNonZero @w forall a b. (a -> b) -> a -> b
$ forall t (proxy :: * -> *) a.
SupportedPrim t =>
proxy t -> (PrimConstraint t => a) -> a
withPrim (forall {k} (t :: k). Proxy t
Proxy @t) (forall {k} (s' :: Nat) (k :: k) (bv :: Nat -> k).
(BVIsNonZero s', KnownNat s', 1 <= s', k ~ bv s') =>
Proxy s' -> BVTypeContainer bv k
BVTypeContainer forall {k} (t :: k). Proxy t
Proxy)
(Maybe (a :~~: IntN), Maybe (k1 :~~: Nat))
_ -> forall a. Maybe a
Nothing
TypeRep t
_ -> forall a. Maybe a
Nothing
where
unsafeBVIsNonZero :: forall w r. ((SBV.BVIsNonZero w) => r) -> r
unsafeBVIsNonZero :: forall (w :: Nat) r. (BVIsNonZero w => r) -> r
unsafeBVIsNonZero BVIsNonZero w => r
r1 = case forall {k} (a :: k) (b :: k). a :~: b
unsafeAxiom :: w :~: 1 of
w :~: 1
Refl -> BVIsNonZero w => r
r1
pattern SignedBVType ::
forall t.
(SupportedPrim t) =>
forall (n :: Nat).
(t ~~ IntN n, KnownNat n, 1 <= n, SBV.BVIsNonZero n) =>
Proxy n ->
R.TypeRep t
pattern $mSignedBVType :: forall {r} {t}.
SupportedPrim t =>
TypeRep t
-> (forall {n :: Nat}.
(t ~~ IntN n, KnownNat n, 1 <= n, BVIsNonZero n) =>
Proxy n -> r)
-> ((# #) -> r)
-> r
SignedBVType p <- (signedBVTypeView @t -> Just (BVTypeContainer p))
unsignedBVTypeView :: forall t. (SupportedPrim t) => R.TypeRep t -> Maybe (BVTypeContainer WordN t)
unsignedBVTypeView :: forall t.
SupportedPrim t =>
TypeRep t -> Maybe (BVTypeContainer WordN t)
unsignedBVTypeView TypeRep t
t = case TypeRep t
t of
R.App TypeRep a
s (TypeRep b
n :: R.TypeRep w) ->
case (forall k1 k2 (a :: k1) (b :: k2).
TypeRep a -> TypeRep b -> Maybe (a :~~: b)
R.eqTypeRep TypeRep a
s (forall {k} (a :: k). Typeable a => TypeRep a
R.typeRep @WordN), forall k1 k2 (a :: k1) (b :: k2).
TypeRep a -> TypeRep b -> Maybe (a :~~: b)
R.eqTypeRep (forall k (a :: k). TypeRep a -> TypeRep k
R.typeRepKind TypeRep b
n) (forall {k} (a :: k). Typeable a => TypeRep a
R.typeRep @Nat)) of
(Just a :~~: WordN
R.HRefl, Just k1 :~~: Nat
R.HRefl) ->
forall a. a -> Maybe a
Just forall a b. (a -> b) -> a -> b
$ forall (w :: Nat) r. (BVIsNonZero w => r) -> r
unsafeBVIsNonZero @w forall a b. (a -> b) -> a -> b
$ forall t (proxy :: * -> *) a.
SupportedPrim t =>
proxy t -> (PrimConstraint t => a) -> a
withPrim (forall {k} (t :: k). Proxy t
Proxy @t) (forall {k} (s' :: Nat) (k :: k) (bv :: Nat -> k).
(BVIsNonZero s', KnownNat s', 1 <= s', k ~ bv s') =>
Proxy s' -> BVTypeContainer bv k
BVTypeContainer forall {k} (t :: k). Proxy t
Proxy)
(Maybe (a :~~: WordN), Maybe (k1 :~~: Nat))
_ -> forall a. Maybe a
Nothing
TypeRep t
_ -> forall a. Maybe a
Nothing
where
unsafeBVIsNonZero :: forall w r. ((SBV.BVIsNonZero w) => r) -> r
unsafeBVIsNonZero :: forall (w :: Nat) r. (BVIsNonZero w => r) -> r
unsafeBVIsNonZero BVIsNonZero w => r
r1 = case forall {k} (a :: k) (b :: k). a :~: b
unsafeAxiom :: w :~: 1 of
w :~: 1
Refl -> BVIsNonZero w => r
r1
pattern UnsignedBVType ::
forall t.
(SupportedPrim t) =>
forall (n :: Nat).
(t ~~ WordN n, KnownNat n, 1 <= n, SBV.BVIsNonZero n) =>
Proxy n ->
R.TypeRep t
pattern $mUnsignedBVType :: forall {r} {t}.
SupportedPrim t =>
TypeRep t
-> (forall {n :: Nat}.
(t ~~ WordN n, KnownNat n, 1 <= n, BVIsNonZero n) =>
Proxy n -> r)
-> ((# #) -> r)
-> r
UnsignedBVType p <- (unsignedBVTypeView @t -> Just (BVTypeContainer p))
data TFunTypeContainer :: forall k. k -> Type where
TFunTypeContainer :: (SupportedPrim a, SupportedPrim b) => R.TypeRep a -> R.TypeRep b -> TFunTypeContainer (a =-> b)
tFunTypeView :: forall t. (SupportedPrim t) => R.TypeRep t -> Maybe (TFunTypeContainer t)
tFunTypeView :: forall t.
SupportedPrim t =>
TypeRep t -> Maybe (TFunTypeContainer t)
tFunTypeView TypeRep t
t = case TypeRep t
t of
R.App (R.App TypeRep a
arr (TypeRep b
ta2' :: R.TypeRep a2)) (TypeRep b
tr2' :: R.TypeRep r2) ->
case forall k1 k2 (a :: k1) (b :: k2).
TypeRep a -> TypeRep b -> Maybe (a :~~: b)
R.eqTypeRep TypeRep a
arr (forall {k} (a :: k). Typeable a => TypeRep a
R.typeRep @(=->)) of
Just a :~~: (=->)
R.HRefl -> forall a. a -> Maybe a
Just forall a b. (a -> b) -> a -> b
$ forall t (proxy :: * -> *) a.
SupportedPrim t =>
proxy t -> (PrimConstraint t => a) -> a
withPrim (forall {k} (t :: k). Proxy t
Proxy @t) forall a b. (a -> b) -> a -> b
$ forall s' b.
(SupportedPrim s', SupportedPrim b) =>
TypeRep s' -> TypeRep b -> TFunTypeContainer (s' =-> b)
TFunTypeContainer TypeRep b
ta2' TypeRep b
tr2'
Maybe (a :~~: (=->))
Nothing -> forall a. Maybe a
Nothing
TypeRep t
_ -> forall a. Maybe a
Nothing
pattern TFunType ::
forall t.
(SupportedPrim t) =>
forall (a :: Type) (b :: Type).
(t ~~ (a =-> b), SupportedPrim a, SupportedPrim b) =>
R.TypeRep a ->
R.TypeRep b ->
R.TypeRep t
pattern $bTFunType :: forall t a b.
(SupportedPrim t, t ~~ (a =-> b), SupportedPrim a,
SupportedPrim b) =>
TypeRep a -> TypeRep b -> TypeRep t
$mTFunType :: forall {r} {t}.
SupportedPrim t =>
TypeRep t
-> (forall {a} {b}.
(t ~~ (a =-> b), SupportedPrim a, SupportedPrim b) =>
TypeRep a -> TypeRep b -> r)
-> ((# #) -> r)
-> r
TFunType a b <-
(tFunTypeView -> Just (TFunTypeContainer a b))
where
TFunType TypeRep a
a TypeRep b
b = forall k2 (t :: k2) k1 (a :: k1 -> k2) (b :: k1).
(t ~ a b) =>
TypeRep a -> TypeRep b -> TypeRep t
R.App (forall k2 (t :: k2) k1 (a :: k1 -> k2) (b :: k1).
(t ~ a b) =>
TypeRep a -> TypeRep b -> TypeRep t
R.App (forall {k} (a :: k). Typeable a => TypeRep a
R.typeRep @(=->)) TypeRep a
a) TypeRep b
b
pattern TFun3Type ::
forall t.
(SupportedPrim t) =>
forall (a :: Type) (b :: Type) (c :: Type).
(t ~~ (a =-> b =-> c), SupportedPrim a, SupportedPrim b, SupportedPrim c) =>
R.TypeRep a ->
R.TypeRep b ->
R.TypeRep c ->
R.TypeRep t
pattern $bTFun3Type :: forall t a b c.
(SupportedPrim t, t ~~ (a =-> (b =-> c)), SupportedPrim a,
SupportedPrim b, SupportedPrim c) =>
TypeRep a -> TypeRep b -> TypeRep c -> TypeRep t
$mTFun3Type :: forall {r} {t}.
SupportedPrim t =>
TypeRep t
-> (forall {a} {b} {c}.
(t ~~ (a =-> (b =-> c)), SupportedPrim a, SupportedPrim b,
SupportedPrim c) =>
TypeRep a -> TypeRep b -> TypeRep c -> r)
-> ((# #) -> r)
-> r
TFun3Type a b c = TFunType a (TFunType b c)
data GFunTypeContainer :: forall k. k -> Type where
GFunTypeContainer :: (SupportedPrim a, SupportedPrim b) => R.TypeRep a -> R.TypeRep b -> GFunTypeContainer (a --> b)
gFunTypeView :: forall t. (SupportedPrim t) => R.TypeRep t -> Maybe (GFunTypeContainer t)
gFunTypeView :: forall t.
SupportedPrim t =>
TypeRep t -> Maybe (GFunTypeContainer t)
gFunTypeView TypeRep t
t = case TypeRep t
t of
R.App (R.App TypeRep a
arr (TypeRep b
ta2' :: R.TypeRep a2)) (TypeRep b
tr2' :: R.TypeRep r2) ->
case forall k1 k2 (a :: k1) (b :: k2).
TypeRep a -> TypeRep b -> Maybe (a :~~: b)
R.eqTypeRep TypeRep a
arr (forall {k} (a :: k). Typeable a => TypeRep a
R.typeRep @(-->)) of
Just a :~~: (-->)
R.HRefl -> forall a. a -> Maybe a
Just forall a b. (a -> b) -> a -> b
$ forall t (proxy :: * -> *) a.
SupportedPrim t =>
proxy t -> (PrimConstraint t => a) -> a
withPrim (forall {k} (t :: k). Proxy t
Proxy @t) forall a b. (a -> b) -> a -> b
$ forall s' b.
(SupportedPrim s', SupportedPrim b) =>
TypeRep s' -> TypeRep b -> GFunTypeContainer (s' --> b)
GFunTypeContainer TypeRep b
ta2' TypeRep b
tr2'
Maybe (a :~~: (-->))
Nothing -> forall a. Maybe a
Nothing
TypeRep t
_ -> forall a. Maybe a
Nothing
pattern GFunType ::
forall t.
(SupportedPrim t) =>
forall (a :: Type) (b :: Type).
(t ~~ (a --> b), SupportedPrim a, SupportedPrim b) =>
R.TypeRep a ->
R.TypeRep b ->
R.TypeRep t
pattern $bGFunType :: forall t a b.
(SupportedPrim t, t ~~ (a --> b), SupportedPrim a,
SupportedPrim b) =>
TypeRep a -> TypeRep b -> TypeRep t
$mGFunType :: forall {r} {t}.
SupportedPrim t =>
TypeRep t
-> (forall {a} {b}.
(t ~~ (a --> b), SupportedPrim a, SupportedPrim b) =>
TypeRep a -> TypeRep b -> r)
-> ((# #) -> r)
-> r
GFunType a b <-
(gFunTypeView -> Just (GFunTypeContainer a b))
where
GFunType TypeRep a
a TypeRep b
b = forall k2 (t :: k2) k1 (a :: k1 -> k2) (b :: k1).
(t ~ a b) =>
TypeRep a -> TypeRep b -> TypeRep t
R.App (forall k2 (t :: k2) k1 (a :: k1 -> k2) (b :: k1).
(t ~ a b) =>
TypeRep a -> TypeRep b -> TypeRep t
R.App (forall {k} (a :: k). Typeable a => TypeRep a
R.typeRep @(-->)) TypeRep a
a) TypeRep b
b
pattern GFun3Type ::
forall t.
(SupportedPrim t) =>
forall (a :: Type) (b :: Type) (c :: Type).
(t ~~ (a --> b --> c), SupportedPrim a, SupportedPrim b, SupportedPrim c) =>
R.TypeRep a ->
R.TypeRep b ->
R.TypeRep c ->
R.TypeRep t
pattern $bGFun3Type :: forall t a b c.
(SupportedPrim t, t ~~ (a --> (b --> c)), SupportedPrim a,
SupportedPrim b, SupportedPrim c) =>
TypeRep a -> TypeRep b -> TypeRep c -> TypeRep t
$mGFun3Type :: forall {r} {t}.
SupportedPrim t =>
TypeRep t
-> (forall {a} {b} {c}.
(t ~~ (a --> (b --> c)), SupportedPrim a, SupportedPrim b,
SupportedPrim c) =>
TypeRep a -> TypeRep b -> TypeRep c -> r)
-> ((# #) -> r)
-> r
GFun3Type a b c = GFunType a (GFunType b c)
pattern BoolType ::
forall t.
() =>
(t ~~ Bool) =>
R.TypeRep t
pattern $mBoolType :: forall {r} {k} {t :: k}.
TypeRep t -> ((t ~~ Bool) => r) -> ((# #) -> r) -> r
BoolType <- (R.eqTypeRep (R.typeRep @Bool) -> Just R.HRefl)
pattern IntegerType ::
forall t.
() =>
(t ~~ Integer) =>
R.TypeRep t
pattern $mIntegerType :: forall {r} {k} {t :: k}.
TypeRep t -> ((t ~~ Integer) => r) -> ((# #) -> r) -> r
IntegerType <- (R.eqTypeRep (R.typeRep @Integer) -> Just R.HRefl)
type ConfigConstraint integerBitWidth s =
( SBV.SBV s ~ TermTy integerBitWidth Integer,
SBV.SymVal s,
SBV.HasKind s,
Typeable s,
Num (SBV.SBV s),
Num s,
SBV.OrdSymbolic (SBV.SBV s),
Ord s,
SBV.SDivisible (SBV.SBV s),
SBV.OrdSymbolic (SBV.SBV s),
SBV.Mergeable (SBV.SBV s)
)
data DictConfig integerBitWidth where
DictConfig ::
forall s integerBitWidth.
(ConfigConstraint integerBitWidth s) =>
SBV.SMTConfig ->
DictConfig integerBitWidth
resolveConfigView ::
forall integerBitWidth.
GrisetteSMTConfig integerBitWidth ->
DictConfig integerBitWidth
resolveConfigView :: forall (integerBitWidth :: Nat).
GrisetteSMTConfig integerBitWidth -> DictConfig integerBitWidth
resolveConfigView GrisetteSMTConfig integerBitWidth
config = case GrisetteSMTConfig integerBitWidth
config of
UnboundedReasoning SMTConfig
c -> forall s' (integerBitWidth :: Nat).
ConfigConstraint integerBitWidth s' =>
SMTConfig -> DictConfig integerBitWidth
DictConfig SMTConfig
c
BoundedReasoning SMTConfig
c -> forall s' (integerBitWidth :: Nat).
ConfigConstraint integerBitWidth s' =>
SMTConfig -> DictConfig integerBitWidth
DictConfig SMTConfig
c
pattern ResolvedConfig ::
forall integerBitWidth.
() =>
forall s.
ConfigConstraint integerBitWidth s =>
SBV.SMTConfig ->
GrisetteSMTConfig integerBitWidth
pattern $mResolvedConfig :: forall {r} {integerBitWidth :: Nat}.
GrisetteSMTConfig integerBitWidth
-> (forall {s}.
ConfigConstraint integerBitWidth s =>
SMTConfig -> r)
-> ((# #) -> r)
-> r
ResolvedConfig c <- (resolveConfigView -> DictConfig c)
type SimpleTypeConstraint integerBitWidth s s' =
( SBV.SBV s' ~ TermTy integerBitWidth s,
SBV.SymVal s',
SBV.HasKind s',
Typeable s',
SBV.OrdSymbolic (SBV.SBV s'),
SBV.Mergeable (SBV.SBV s')
)
type TypeResolver dictType =
forall integerBitWidth s.
(SupportedPrim s) =>
(GrisetteSMTConfig integerBitWidth, R.TypeRep s) ->
Maybe (dictType integerBitWidth s)
data DictSimpleType integerBitWidth s where
DictSimpleType ::
forall integerBitWidth s s'.
(SimpleTypeConstraint integerBitWidth s s') =>
DictSimpleType integerBitWidth s
resolveSimpleTypeView :: TypeResolver DictSimpleType
resolveSimpleTypeView :: TypeResolver DictSimpleType
resolveSimpleTypeView (ResolvedConfig {}, TypeRep s
s) = case TypeRep s
s of
TypeRep s
BoolType -> forall a. a -> Maybe a
Just forall (integerBitWidth :: Nat) s s'.
SimpleTypeConstraint integerBitWidth s s' =>
DictSimpleType integerBitWidth s
DictSimpleType
TypeRep s
IntegerType -> forall a. a -> Maybe a
Just forall (integerBitWidth :: Nat) s s'.
SimpleTypeConstraint integerBitWidth s s' =>
DictSimpleType integerBitWidth s
DictSimpleType
SignedBVType Proxy n
_ -> forall a. a -> Maybe a
Just forall (integerBitWidth :: Nat) s s'.
SimpleTypeConstraint integerBitWidth s s' =>
DictSimpleType integerBitWidth s
DictSimpleType
UnsignedBVType Proxy n
_ -> forall a. a -> Maybe a
Just forall (integerBitWidth :: Nat) s s'.
SimpleTypeConstraint integerBitWidth s s' =>
DictSimpleType integerBitWidth s
DictSimpleType
TypeRep s
_ -> forall a. Maybe a
Nothing
resolveSimpleTypeView (GrisetteSMTConfig integerBitWidth, TypeRep s)
_ = forall a. HasCallStack => [Char] -> a
error [Char]
"Should never happen, make compiler happy"
pattern ResolvedSimpleType ::
forall integerBitWidth s.
(SupportedPrim s) =>
forall s'.
SimpleTypeConstraint integerBitWidth s s' =>
(GrisetteSMTConfig integerBitWidth, R.TypeRep s)
pattern $mResolvedSimpleType :: forall {r} {integerBitWidth :: Nat} {s}.
SupportedPrim s =>
(GrisetteSMTConfig integerBitWidth, TypeRep s)
-> (forall {s'}. SimpleTypeConstraint integerBitWidth s s' => r)
-> ((# #) -> r)
-> r
ResolvedSimpleType <- (resolveSimpleTypeView -> Just DictSimpleType)
type DeepTypeConstraint integerBitWidth s s' =
( s' ~ TermTy integerBitWidth s,
Typeable s',
SBV.Mergeable s'
)
data DictDeepType integerBitWidth s where
DictDeepType ::
forall integerBitWidth s s'.
(DeepTypeConstraint integerBitWidth s s') =>
DictDeepType integerBitWidth s
resolveDeepTypeView :: TypeResolver DictDeepType
resolveDeepTypeView :: TypeResolver DictDeepType
resolveDeepTypeView (GrisetteSMTConfig integerBitWidth, TypeRep s)
r = case (GrisetteSMTConfig integerBitWidth, TypeRep s)
r of
(GrisetteSMTConfig integerBitWidth, TypeRep s)
ResolvedSimpleType -> forall a. a -> Maybe a
Just forall (integerBitWidth :: Nat) s s'.
DeepTypeConstraint integerBitWidth s s' =>
DictDeepType integerBitWidth s
DictDeepType
(GrisetteSMTConfig integerBitWidth
config, TFunType (TypeRep a
ta :: R.TypeRep a) (TypeRep b
tb :: R.TypeRep b)) ->
case (TypeResolver DictDeepType
resolveDeepTypeView (GrisetteSMTConfig integerBitWidth
config, TypeRep a
ta), TypeResolver DictDeepType
resolveDeepTypeView (GrisetteSMTConfig integerBitWidth
config, TypeRep b
tb)) of
(Just DictDeepType integerBitWidth a
DictDeepType, Just DictDeepType integerBitWidth b
DictDeepType) -> forall a. a -> Maybe a
Just forall (integerBitWidth :: Nat) s s'.
DeepTypeConstraint integerBitWidth s s' =>
DictDeepType integerBitWidth s
DictDeepType
(Maybe (DictDeepType integerBitWidth a),
Maybe (DictDeepType integerBitWidth b))
_ -> forall a. Maybe a
Nothing
(GrisetteSMTConfig integerBitWidth
config, GFunType (TypeRep a
ta :: R.TypeRep a) (TypeRep b
tb :: R.TypeRep b)) ->
case (TypeResolver DictDeepType
resolveDeepTypeView (GrisetteSMTConfig integerBitWidth
config, TypeRep a
ta), TypeResolver DictDeepType
resolveDeepTypeView (GrisetteSMTConfig integerBitWidth
config, TypeRep b
tb)) of
(Just DictDeepType integerBitWidth a
DictDeepType, Just DictDeepType integerBitWidth b
DictDeepType) -> forall a. a -> Maybe a
Just forall (integerBitWidth :: Nat) s s'.
DeepTypeConstraint integerBitWidth s s' =>
DictDeepType integerBitWidth s
DictDeepType
(Maybe (DictDeepType integerBitWidth a),
Maybe (DictDeepType integerBitWidth b))
_ -> forall a. Maybe a
Nothing
(GrisetteSMTConfig integerBitWidth, TypeRep s)
_ -> forall a. Maybe a
Nothing
pattern ResolvedDeepType ::
forall integerBitWidth s.
(SupportedPrim s) =>
forall s'.
DeepTypeConstraint integerBitWidth s s' =>
(GrisetteSMTConfig integerBitWidth, R.TypeRep s)
pattern $mResolvedDeepType :: forall {r} {integerBitWidth :: Nat} {s}.
SupportedPrim s =>
(GrisetteSMTConfig integerBitWidth, TypeRep s)
-> (forall {s'}. DeepTypeConstraint integerBitWidth s s' => r)
-> ((# #) -> r)
-> r
ResolvedDeepType <- (resolveDeepTypeView -> Just DictDeepType)
type NumTypeConstraint integerBitWidth s s' =
( SimpleTypeConstraint integerBitWidth s s',
Num (SBV.SBV s'),
Num s',
Num s
)
data DictNumType integerBitWidth s where
DictNumType ::
forall integerBitWidth s s'.
(NumTypeConstraint integerBitWidth s s') =>
DictNumType integerBitWidth s
resolveNumTypeView :: TypeResolver DictNumType
resolveNumTypeView :: TypeResolver DictNumType
resolveNumTypeView (ResolvedConfig {}, TypeRep s
s) = case TypeRep s
s of
TypeRep s
IntegerType -> forall a. a -> Maybe a
Just forall (integerBitWidth :: Nat) s s'.
NumTypeConstraint integerBitWidth s s' =>
DictNumType integerBitWidth s
DictNumType
SignedBVType Proxy n
_ -> forall a. a -> Maybe a
Just forall (integerBitWidth :: Nat) s s'.
NumTypeConstraint integerBitWidth s s' =>
DictNumType integerBitWidth s
DictNumType
UnsignedBVType Proxy n
_ -> forall a. a -> Maybe a
Just forall (integerBitWidth :: Nat) s s'.
NumTypeConstraint integerBitWidth s s' =>
DictNumType integerBitWidth s
DictNumType
TypeRep s
_ -> forall a. Maybe a
Nothing
resolveNumTypeView (GrisetteSMTConfig integerBitWidth, TypeRep s)
_ = forall a. HasCallStack => [Char] -> a
error [Char]
"Should never happen, make compiler happy"
pattern ResolvedNumType ::
forall integerBitWidth s.
(SupportedPrim s) =>
forall s'.
NumTypeConstraint integerBitWidth s s' =>
(GrisetteSMTConfig integerBitWidth, R.TypeRep s)
pattern $mResolvedNumType :: forall {r} {integerBitWidth :: Nat} {s}.
SupportedPrim s =>
(GrisetteSMTConfig integerBitWidth, TypeRep s)
-> (forall {s'}. NumTypeConstraint integerBitWidth s s' => r)
-> ((# #) -> r)
-> r
ResolvedNumType <- (resolveNumTypeView -> Just DictNumType)
type NumOrdTypeConstraint integerBitWidth s s' =
( NumTypeConstraint integerBitWidth s s',
SBV.OrdSymbolic (SBV.SBV s'),
Ord s',
Ord s
)
data DictNumOrdType integerBitWidth s where
DictNumOrdType ::
forall integerBitWidth s s'.
(NumOrdTypeConstraint integerBitWidth s s') =>
DictNumOrdType integerBitWidth s
resolveNumOrdTypeView :: TypeResolver DictNumOrdType
resolveNumOrdTypeView :: TypeResolver DictNumOrdType
resolveNumOrdTypeView (ResolvedConfig {}, TypeRep s
s) = case TypeRep s
s of
TypeRep s
IntegerType -> forall a. a -> Maybe a
Just forall (integerBitWidth :: Nat) s s'.
NumOrdTypeConstraint integerBitWidth s s' =>
DictNumOrdType integerBitWidth s
DictNumOrdType
SignedBVType Proxy n
_ -> forall a. a -> Maybe a
Just forall (integerBitWidth :: Nat) s s'.
NumOrdTypeConstraint integerBitWidth s s' =>
DictNumOrdType integerBitWidth s
DictNumOrdType
UnsignedBVType Proxy n
_ -> forall a. a -> Maybe a
Just forall (integerBitWidth :: Nat) s s'.
NumOrdTypeConstraint integerBitWidth s s' =>
DictNumOrdType integerBitWidth s
DictNumOrdType
TypeRep s
_ -> forall a. Maybe a
Nothing
resolveNumOrdTypeView (GrisetteSMTConfig integerBitWidth, TypeRep s)
_ = forall a. HasCallStack => [Char] -> a
error [Char]
"Should never happen, make compiler happy"
pattern ResolvedNumOrdType ::
forall integerBitWidth s.
(SupportedPrim s) =>
forall s'.
NumOrdTypeConstraint integerBitWidth s s' =>
(GrisetteSMTConfig integerBitWidth, R.TypeRep s)
pattern $mResolvedNumOrdType :: forall {r} {integerBitWidth :: Nat} {s}.
SupportedPrim s =>
(GrisetteSMTConfig integerBitWidth, TypeRep s)
-> (forall {s'}. NumOrdTypeConstraint integerBitWidth s s' => r)
-> ((# #) -> r)
-> r
ResolvedNumOrdType <- (resolveNumOrdTypeView -> Just DictNumOrdType)
type BitsTypeConstraint integerBitWidth s s' =
( SimpleTypeConstraint integerBitWidth s s',
Bits (SBV.SBV s'),
Bits s',
Bits s
)
data DictBitsType integerBitWidth s where
DictBitsType ::
forall integerBitWidth s s'.
(BitsTypeConstraint integerBitWidth s s') =>
DictBitsType integerBitWidth s
resolveBitsTypeView :: TypeResolver DictBitsType
resolveBitsTypeView :: TypeResolver DictBitsType
resolveBitsTypeView (ResolvedConfig {}, TypeRep s
s) = case TypeRep s
s of
SignedBVType Proxy n
_ -> forall a. a -> Maybe a
Just forall (integerBitWidth :: Nat) s s'.
BitsTypeConstraint integerBitWidth s s' =>
DictBitsType integerBitWidth s
DictBitsType
UnsignedBVType Proxy n
_ -> forall a. a -> Maybe a
Just forall (integerBitWidth :: Nat) s s'.
BitsTypeConstraint integerBitWidth s s' =>
DictBitsType integerBitWidth s
DictBitsType
TypeRep s
_ -> forall a. Maybe a
Nothing
resolveBitsTypeView (GrisetteSMTConfig integerBitWidth, TypeRep s)
_ = forall a. HasCallStack => [Char] -> a
error [Char]
"Should never happen, make compiler happy"
pattern ResolvedBitsType ::
forall integerBitWidth s.
(SupportedPrim s) =>
forall s'.
BitsTypeConstraint integerBitWidth s s' =>
(GrisetteSMTConfig integerBitWidth, R.TypeRep s)
pattern $mResolvedBitsType :: forall {r} {integerBitWidth :: Nat} {s}.
SupportedPrim s =>
(GrisetteSMTConfig integerBitWidth, TypeRep s)
-> (forall {s'}. BitsTypeConstraint integerBitWidth s s' => r)
-> ((# #) -> r)
-> r
ResolvedBitsType <- (resolveBitsTypeView -> Just DictBitsType)