{-# 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
-- Copyright   :   (c) Sirui Lu 2021-2023
-- License     :   BSD-3-Clause (see the LICENSE file)
--
-- Maintainer  :   siruilu@cs.washington.edu
-- Stability   :   Experimental
-- Portability :   GHC only
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 Natural
nVal) KnownNat n => r
v =
  case Natural -> SomeNat
someNatVal Natural
nVal of
    SomeNat (Proxy n
Proxy :: Proxy n') ->
      case n :~: n
forall {k} (a :: k) (b :: k). a :~: b
unsafeAxiom :: n :~: n' of
        n :~: n
Refl -> r
KnownNat n => r
v

data LeqProof (m :: Nat) (n :: Nat) where
  LeqProof :: m <= n => LeqProof m n

-- | Assert a proof of equality between two types.
-- This is unsafe if used improperly, so use this with caution!
unsafeAxiom :: forall a b. a :~: b
unsafeAxiom :: forall {k} (a :: k) (b :: k). a :~: b
unsafeAxiom = (a :~: a) -> a :~: b
forall a b. a -> b
unsafeCoerce (forall {a :: k}. a :~: a
forall {k} (a :: k). a :~: a
Refl @a)
{-# NOINLINE unsafeAxiom #-} -- Note [Mark unsafe axioms as NOINLINE]

unsafeLeqProof :: forall m n. LeqProof m n
unsafeLeqProof :: forall (m :: Nat) (n :: Nat). LeqProof m n
unsafeLeqProof = LeqProof 0 0 -> LeqProof m n
forall a b. a -> b
unsafeCoerce (forall (m :: Nat) (n :: Nat). (m <= n) => LeqProof m n
LeqProof @0 @0)
{-# NOINLINE unsafeLeqProof #-} -- Note [Mark unsafe axioms as NOINLINE]

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 = (SymBiMap -> Maybe (TermTy integerBitWidth a))
-> StateT SymBiMap Identity (Maybe (TermTy integerBitWidth a))
forall s (m :: * -> *) a. MonadState s m => (s -> a) -> m a
gets ((SymBiMap -> Maybe (TermTy integerBitWidth a))
 -> StateT SymBiMap Identity (Maybe (TermTy integerBitWidth a)))
-> (SymBiMap -> Maybe (TermTy integerBitWidth a))
-> StateT SymBiMap Identity (Maybe (TermTy integerBitWidth a))
forall a b. (a -> b) -> a -> b
$ \SymBiMap
m -> do
  Dynamic
d <- HasCallStack => SomeTerm -> SymBiMap -> Maybe Dynamic
SomeTerm -> SymBiMap -> Maybe Dynamic
lookupTerm (Term a -> SomeTerm
forall a. SupportedPrim a => Term a -> SomeTerm
SomeTerm Term a
t) SymBiMap
m
  TermTy integerBitWidth a -> Maybe (TermTy integerBitWidth a)
forall a. a -> Maybe a
Just (TermTy integerBitWidth a -> Maybe (TermTy integerBitWidth a))
-> TermTy integerBitWidth a -> Maybe (TermTy integerBitWidth a)
forall a b. (a -> b) -> a -> b
$ Dynamic -> TermTy integerBitWidth a -> TermTy integerBitWidth a
forall a. Typeable a => Dynamic -> a -> a
fromDyn Dynamic
d TermTy integerBitWidth a
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 = (SymBiMap -> SymBiMap) -> State SymBiMap ()
forall s (m :: * -> *). MonadState s m => (s -> s) -> m ()
modify ((SymBiMap -> SymBiMap) -> State SymBiMap ())
-> (SymBiMap -> SymBiMap) -> State SymBiMap ()
forall a b. (a -> b) -> a -> b
$ HasCallStack => SomeTerm -> Dynamic -> SymBiMap -> SymBiMap
SomeTerm -> Dynamic -> SymBiMap -> SymBiMap
addBiMapIntermediate (Term a -> SomeTerm
forall a. SupportedPrim a => Term a -> SomeTerm
SomeTerm Term a
tm) (TermTy integerBitWidth a -> Dynamic
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 = State SymBiMap (TermTy integerBitWidth a)
-> SymBiMap -> (TermTy integerBitWidth a, SymBiMap)
forall s a. State s a -> s -> (a, s)
runState (GrisetteSMTConfig integerBitWidth
-> Term a -> State SymBiMap (TermTy integerBitWidth a)
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 = Term a
-> (SupportedPrim a => State SymBiMap (TermTy integerBitWidth a))
-> State SymBiMap (TermTy integerBitWidth a)
forall t a. Term t -> (SupportedPrim t => a) -> a
introSupportedPrimConstraint Term a
t ((SupportedPrim a => State SymBiMap (TermTy integerBitWidth a))
 -> State SymBiMap (TermTy integerBitWidth a))
-> (SupportedPrim a => State SymBiMap (TermTy integerBitWidth a))
-> State SymBiMap (TermTy integerBitWidth a)
forall a b. (a -> b) -> a -> b
$
  case (GrisetteSMTConfig integerBitWidth
config, forall a. Typeable a => TypeRep a
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 -> s' -> StateT SymBiMap Identity s'
forall (m :: * -> *) a. Monad m => a -> m a
return s'
v
        Maybe s'
_ -> GrisetteSMTConfig integerBitWidth
-> Term a -> State SymBiMap (TermTy integerBitWidth a)
forall (integerBitWidth :: Nat) a.
GrisetteSMTConfig integerBitWidth
-> Term a -> State SymBiMap (TermTy integerBitWidth a)
lowerSinglePrimImpl' GrisetteSMTConfig integerBitWidth
config Term a
t
    (GrisetteSMTConfig integerBitWidth, TypeRep a)
_ -> TypeRep a -> State SymBiMap (TermTy integerBitWidth a)
forall {k} (a :: k) b. HasCallStack => TypeRep a -> b
translateTypeError (forall a. Typeable a => TypeRep a
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 <- GrisetteSMTConfig integerBitWidth
-> Term a -> State SymBiMap (TermTy integerBitWidth a)
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
TermTy integerBitWidth x
g
  x1 -> StateT SymBiMap Identity x1
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 <- GrisetteSMTConfig integerBitWidth
-> Term a -> State SymBiMap (TermTy integerBitWidth a)
forall (integerBitWidth :: Nat) a.
GrisetteSMTConfig integerBitWidth
-> Term a -> State SymBiMap (TermTy integerBitWidth a)
lowerSinglePrimCached' GrisetteSMTConfig integerBitWidth
config Term a
t1
  b1
l2 <- GrisetteSMTConfig integerBitWidth
-> Term b -> State SymBiMap (TermTy integerBitWidth b)
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
  TermTy integerBitWidth x
-> State SymBiMap (TermTy integerBitWidth x)
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 a. Typeable a => TypeRep a
forall {k} (a :: k). Typeable a => TypeRep a
R.typeRep @a of
    TypeRep a
BoolType -> SBool -> StateT SymBiMap Identity SBool
forall (m :: * -> *) a. Monad m => a -> m a
return (SBool -> StateT SymBiMap Identity SBool)
-> SBool -> StateT SymBiMap Identity SBool
forall a b. (a -> b) -> a -> b
$ if a
Bool
v then SBool
SBV.sTrue else SBool
SBV.sFalse
    TypeRep a
IntegerType -> SBV s -> StateT SymBiMap Identity (SBV s)
forall (m :: * -> *) a. Monad m => a -> m a
return (SBV s -> StateT SymBiMap Identity (SBV s))
-> SBV s -> StateT SymBiMap Identity (SBV s)
forall a b. (a -> b) -> a -> b
$ Integer -> SBV s
forall a. Num a => Integer -> a
fromInteger a
Integer
v
    SignedBVType Proxy n
_ -> case a
v of
      IntN Integer
x -> SBV (IntN n) -> StateT SymBiMap Identity (SBV (IntN n))
forall (m :: * -> *) a. Monad m => a -> m a
return (SBV (IntN n) -> StateT SymBiMap Identity (SBV (IntN n)))
-> SBV (IntN n) -> StateT SymBiMap Identity (SBV (IntN n))
forall a b. (a -> b) -> a -> b
$ Integer -> SBV (IntN n)
forall a. Num a => Integer -> a
fromInteger Integer
x
    UnsignedBVType Proxy n
_ -> case a
v of
      WordN Integer
x -> SBV (WordN n) -> StateT SymBiMap Identity (SBV (WordN n))
forall (m :: * -> *) a. Monad m => a -> m a
return (SBV (WordN n) -> StateT SymBiMap Identity (SBV (WordN n)))
-> SBV (WordN n) -> StateT SymBiMap Identity (SBV (WordN n))
forall a b. (a -> b) -> a -> b
$ Integer -> SBV (WordN n)
forall a. Num a => Integer -> a
fromInteger Integer
x
    TypeRep a
_ -> TypeRep a -> State SymBiMap (TermTy integerBitWidth a)
forall {k} (a :: k) b. HasCallStack => TypeRep a -> b
translateTypeError (forall a. Typeable a => TypeRep a
forall {k} (a :: k). Typeable a => TypeRep a
R.typeRep @a)
lowerSinglePrimImpl' GrisetteSMTConfig integerBitWidth
_ t :: Term a
t@SymTerm {} =
  [Char] -> State SymBiMap (TermTy integerBitWidth a)
forall a. HasCallStack => [Char] -> a
error ([Char] -> State SymBiMap (TermTy integerBitWidth a))
-> [Char] -> State SymBiMap (TermTy integerBitWidth a)
forall a b. (a -> b) -> a -> b
$
    [Char]
"The symbolic term should have already been lowered "
      [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ Term a -> [Char]
forall a. Show a => a -> [Char]
show Term a
t
      [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Char]
" to SMT with collectedPrims.\n"
      [Char] -> [Char] -> [Char]
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)) = State SymBiMap (TermTy integerBitWidth a)
forall t1. t1
errorMsg
  where
    errorMsg :: forall t1. t1
    errorMsg :: forall t1. t1
errorMsg = [Char] -> TypeRep arg -> TypeRep a -> t1
forall {k} {k} (a :: k) (b :: k) c.
HasCallStack =>
[Char] -> TypeRep a -> TypeRep b -> c
translateUnaryError (tag -> [Char]
forall a. Show a => a -> [Char]
show tag
op) (forall a. Typeable a => TypeRep a
forall {k} (a :: k). Typeable a => TypeRep a
R.typeRep @x) (forall a. Typeable a => TypeRep a
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)) = State SymBiMap (TermTy integerBitWidth a)
forall t1. t1
errorMsg
  where
    errorMsg :: forall t1. t1
    errorMsg :: forall t1. t1
errorMsg = [Char] -> TypeRep arg1 -> TypeRep arg2 -> TypeRep a -> t1
forall {k} {k} {k} (a :: k) (b :: k) (c :: k) d.
HasCallStack =>
[Char] -> TypeRep a -> TypeRep b -> TypeRep c -> d
translateBinaryError (tag -> [Char]
forall a. Show a => a -> [Char]
show tag
op) (forall a. Typeable a => TypeRep a
forall {k} (a :: k). Typeable a => TypeRep a
R.typeRep @x) (forall a. Typeable a => TypeRep a
forall {k} (a :: k). Typeable a => TypeRep a
R.typeRep @y) (forall a. Typeable a => TypeRep a
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)) = State SymBiMap (TermTy integerBitWidth a)
forall t1. t1
errorMsg
  where
    errorMsg :: forall t1. t1
    errorMsg :: forall t1. t1
errorMsg = [Char]
-> TypeRep arg1 -> TypeRep arg2 -> TypeRep arg3 -> TypeRep a -> t1
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 (tag -> [Char]
forall a. Show a => a -> [Char]
show tag
op) (forall a. Typeable a => TypeRep a
forall {k} (a :: k). Typeable a => TypeRep a
R.typeRep @x) (forall a. Typeable a => TypeRep a
forall {k} (a :: k). Typeable a => TypeRep a
R.typeRep @y) (forall a. Typeable a => TypeRep a
forall {k} (a :: k). Typeable a => TypeRep a
R.typeRep @z) (forall a. Typeable a => TypeRep a
forall {k} (a :: k). Typeable a => TypeRep a
R.typeRep @a)
lowerSinglePrimImpl' GrisetteSMTConfig integerBitWidth
config t :: Term a
t@(NotTerm Id
_ Term Bool
arg) = GrisetteSMTConfig integerBitWidth
-> Term a
-> Term Bool
-> (SBool -> SBool)
-> State SymBiMap (TermTy integerBitWidth a)
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) = GrisetteSMTConfig integerBitWidth
-> Term a
-> Term Bool
-> Term Bool
-> (SBool -> SBool -> TermTy integerBitWidth a)
-> State SymBiMap (TermTy integerBitWidth a)
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
SBool -> SBool -> TermTy integerBitWidth a
(SBV..||)
lowerSinglePrimImpl' GrisetteSMTConfig integerBitWidth
config t :: Term a
t@(AndTerm Id
_ Term Bool
arg1 Term Bool
arg2) = GrisetteSMTConfig integerBitWidth
-> Term a
-> Term Bool
-> Term Bool
-> (SBool -> SBool -> TermTy integerBitWidth a)
-> State SymBiMap (TermTy integerBitWidth a)
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
SBool -> SBool -> TermTy integerBitWidth a
(SBV..&&)
lowerSinglePrimImpl' GrisetteSMTConfig integerBitWidth
config t :: Term a
t@(EqvTerm Id
_ (Term t1
arg1 :: Term x) Term t1
arg2) =
  case (GrisetteSMTConfig integerBitWidth
config, forall a. Typeable a => TypeRep a
forall {k} (a :: k). Typeable a => TypeRep a
R.typeRep @x) of
    (GrisetteSMTConfig integerBitWidth, TypeRep t1)
ResolvedSimpleType -> GrisetteSMTConfig integerBitWidth
-> Term a
-> Term t1
-> Term t1
-> (SBV s' -> SBV s' -> TermTy integerBitWidth a)
-> State SymBiMap (TermTy integerBitWidth a)
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 SBV s' -> SBV s' -> TermTy integerBitWidth a
forall a. EqSymbolic a => a -> a -> SBool
(SBV..==)
    (GrisetteSMTConfig integerBitWidth, TypeRep t1)
_ -> [Char]
-> TypeRep t1
-> TypeRep t1
-> TypeRep a
-> StateT SymBiMap Identity SBool
forall {k} {k} {k} (a :: k) (b :: k) (c :: k) d.
HasCallStack =>
[Char] -> TypeRep a -> TypeRep b -> TypeRep c -> d
translateBinaryError [Char]
"(==)" (forall a. Typeable a => TypeRep a
forall {k} (a :: k). Typeable a => TypeRep a
R.typeRep @x) (forall a. Typeable a => TypeRep a
forall {k} (a :: k). Typeable a => TypeRep a
R.typeRep @x) (forall a. Typeable a => TypeRep a
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 a. Typeable a => TypeRep a
forall {k} (a :: k). Typeable a => TypeRep a
R.typeRep @a) of
    (GrisetteSMTConfig integerBitWidth, TypeRep a)
ResolvedSimpleType -> do
      SBool
l1 <- GrisetteSMTConfig integerBitWidth
-> Term Bool -> State SymBiMap (TermTy integerBitWidth Bool)
forall (integerBitWidth :: Nat) a.
GrisetteSMTConfig integerBitWidth
-> Term a -> State SymBiMap (TermTy integerBitWidth a)
lowerSinglePrimCached' GrisetteSMTConfig integerBitWidth
config Term Bool
cond
      SBV s'
l2 <- GrisetteSMTConfig integerBitWidth
-> Term a -> State SymBiMap (TermTy integerBitWidth a)
forall (integerBitWidth :: Nat) a.
GrisetteSMTConfig integerBitWidth
-> Term a -> State SymBiMap (TermTy integerBitWidth a)
lowerSinglePrimCached' GrisetteSMTConfig integerBitWidth
config Term a
arg1
      SBV s'
l3 <- GrisetteSMTConfig integerBitWidth
-> Term a -> State SymBiMap (TermTy integerBitWidth a)
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 = SBool -> SBV s' -> SBV s' -> SBV s'
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'
TermTy integerBitWidth a
g
      SBV s' -> StateT SymBiMap Identity (SBV s')
forall (m :: * -> *) a. Monad m => a -> m a
return SBV s'
g
    (GrisetteSMTConfig integerBitWidth, TypeRep a)
_ -> [Char]
-> TypeRep Bool
-> TypeRep a
-> TypeRep a
-> TypeRep a
-> State SymBiMap (TermTy integerBitWidth 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 a. Typeable a => TypeRep a
forall {k} (a :: k). Typeable a => TypeRep a
R.typeRep @Bool) (forall a. Typeable a => TypeRep a
forall {k} (a :: k). Typeable a => TypeRep a
R.typeRep @a) (forall a. Typeable a => TypeRep a
forall {k} (a :: k). Typeable a => TypeRep a
R.typeRep @a) (forall a. Typeable a => 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 a. Typeable a => TypeRep a
forall {k} (a :: k). Typeable a => TypeRep a
R.typeRep @a) of
    (GrisetteSMTConfig integerBitWidth, TypeRep a)
ResolvedNumType -> GrisetteSMTConfig integerBitWidth
-> Term a
-> Term a
-> Term a
-> (SBV s' -> SBV s' -> TermTy integerBitWidth a)
-> State SymBiMap (TermTy integerBitWidth a)
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 SBV s' -> SBV s' -> TermTy integerBitWidth a
forall a. Num a => a -> a -> a
(+)
    (GrisetteSMTConfig integerBitWidth, TypeRep a)
_ -> [Char]
-> TypeRep a
-> TypeRep a
-> TypeRep a
-> State SymBiMap (TermTy integerBitWidth a)
forall {k} {k} {k} (a :: k) (b :: k) (c :: k) d.
HasCallStack =>
[Char] -> TypeRep a -> TypeRep b -> TypeRep c -> d
translateBinaryError [Char]
"(+)" (forall a. Typeable a => TypeRep a
forall {k} (a :: k). Typeable a => TypeRep a
R.typeRep @a) (forall a. Typeable a => TypeRep a
forall {k} (a :: k). Typeable a => TypeRep a
R.typeRep @a) (forall a. Typeable a => 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 a. Typeable a => TypeRep a
forall {k} (a :: k). Typeable a => TypeRep a
R.typeRep @a) of
    (GrisetteSMTConfig integerBitWidth, TypeRep a)
ResolvedNumType -> GrisetteSMTConfig integerBitWidth
-> Term a
-> Term a
-> (SBV s' -> SBV s')
-> State SymBiMap (TermTy integerBitWidth a)
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 SBV s' -> SBV s'
forall a. Num a => a -> a
negate
    (GrisetteSMTConfig integerBitWidth, TypeRep a)
_ -> [Char]
-> TypeRep a
-> TypeRep a
-> State SymBiMap (TermTy integerBitWidth a)
forall {k} {k} (a :: k) (b :: k) c.
HasCallStack =>
[Char] -> TypeRep a -> TypeRep b -> c
translateUnaryError [Char]
"negate" (forall a. Typeable a => TypeRep a
forall {k} (a :: k). Typeable a => TypeRep a
R.typeRep @a) (forall a. Typeable a => 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 a. Typeable a => TypeRep a
forall {k} (a :: k). Typeable a => TypeRep a
R.typeRep @a) of
    (GrisetteSMTConfig integerBitWidth, TypeRep a)
ResolvedNumType -> GrisetteSMTConfig integerBitWidth
-> Term a
-> Term a
-> Term a
-> (SBV s' -> SBV s' -> TermTy integerBitWidth a)
-> State SymBiMap (TermTy integerBitWidth a)
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 SBV s' -> SBV s' -> TermTy integerBitWidth a
forall a. Num a => a -> a -> a
(*)
    (GrisetteSMTConfig integerBitWidth, TypeRep a)
_ -> [Char]
-> TypeRep a
-> TypeRep a
-> TypeRep a
-> State SymBiMap (TermTy integerBitWidth a)
forall {k} {k} {k} (a :: k) (b :: k) (c :: k) d.
HasCallStack =>
[Char] -> TypeRep a -> TypeRep b -> TypeRep c -> d
translateBinaryError [Char]
"(*)" (forall a. Typeable a => TypeRep a
forall {k} (a :: k). Typeable a => TypeRep a
R.typeRep @a) (forall a. Typeable a => TypeRep a
forall {k} (a :: k). Typeable a => TypeRep a
R.typeRep @a) (forall a. Typeable a => 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 a. Typeable a => TypeRep a
forall {k} (a :: k). Typeable a => TypeRep a
R.typeRep @a) of
    (GrisetteSMTConfig integerBitWidth, TypeRep a)
ResolvedNumType -> GrisetteSMTConfig integerBitWidth
-> Term a
-> Term a
-> (SBV s' -> SBV s')
-> State SymBiMap (TermTy integerBitWidth a)
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 SBV s' -> SBV s'
forall a. Num a => a -> a
abs
    (GrisetteSMTConfig integerBitWidth, TypeRep a)
_ -> [Char]
-> TypeRep a
-> TypeRep a
-> State SymBiMap (TermTy integerBitWidth a)
forall {k} {k} (a :: k) (b :: k) c.
HasCallStack =>
[Char] -> TypeRep a -> TypeRep b -> c
translateUnaryError [Char]
"abs" (forall a. Typeable a => TypeRep a
forall {k} (a :: k). Typeable a => TypeRep a
R.typeRep @a) (forall a. Typeable a => 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 a. Typeable a => TypeRep a
forall {k} (a :: k). Typeable a => TypeRep a
R.typeRep @a) of
    (GrisetteSMTConfig integerBitWidth, TypeRep a)
ResolvedNumType -> GrisetteSMTConfig integerBitWidth
-> Term a
-> Term a
-> (SBV s' -> SBV s')
-> State SymBiMap (TermTy integerBitWidth a)
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 SBV s' -> SBV s'
forall a. Num a => a -> a
signum
    (GrisetteSMTConfig integerBitWidth, TypeRep a)
_ -> [Char]
-> TypeRep a
-> TypeRep a
-> State SymBiMap (TermTy integerBitWidth a)
forall {k} {k} (a :: k) (b :: k) c.
HasCallStack =>
[Char] -> TypeRep a -> TypeRep b -> c
translateUnaryError [Char]
"signum" (forall a. Typeable a => TypeRep a
forall {k} (a :: k). Typeable a => TypeRep a
R.typeRep @a) (forall a. Typeable a => 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 a. Typeable a => TypeRep a
forall {k} (a :: k). Typeable a => TypeRep a
R.typeRep @arg) of
    (GrisetteSMTConfig integerBitWidth, TypeRep t1)
ResolvedNumOrdType -> GrisetteSMTConfig integerBitWidth
-> Term a
-> Term t1
-> Term t1
-> (SBV s' -> SBV s' -> TermTy integerBitWidth a)
-> State SymBiMap (TermTy integerBitWidth a)
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 SBV s' -> SBV s' -> TermTy integerBitWidth a
forall a. OrdSymbolic a => a -> a -> SBool
(SBV..<)
    (GrisetteSMTConfig integerBitWidth, TypeRep t1)
_ -> [Char]
-> TypeRep t1
-> TypeRep t1
-> TypeRep Bool
-> StateT SymBiMap Identity SBool
forall {k} {k} {k} (a :: k) (b :: k) (c :: k) d.
HasCallStack =>
[Char] -> TypeRep a -> TypeRep b -> TypeRep c -> d
translateBinaryError [Char]
"(<)" (forall a. Typeable a => TypeRep a
forall {k} (a :: k). Typeable a => TypeRep a
R.typeRep @arg) (forall a. Typeable a => TypeRep a
forall {k} (a :: k). Typeable a => TypeRep a
R.typeRep @arg) (forall a. Typeable a => 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) =
  case (GrisetteSMTConfig integerBitWidth
config, forall a. Typeable a => TypeRep a
forall {k} (a :: k). Typeable a => TypeRep a
R.typeRep @arg) of
    (GrisetteSMTConfig integerBitWidth, TypeRep t1)
ResolvedNumOrdType -> GrisetteSMTConfig integerBitWidth
-> Term a
-> Term t1
-> Term t1
-> (SBV s' -> SBV s' -> TermTy integerBitWidth a)
-> State SymBiMap (TermTy integerBitWidth a)
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 SBV s' -> SBV s' -> TermTy integerBitWidth a
forall a. OrdSymbolic a => a -> a -> SBool
(SBV..<=)
    (GrisetteSMTConfig integerBitWidth, TypeRep t1)
_ -> [Char]
-> TypeRep t1
-> TypeRep t1
-> TypeRep Bool
-> StateT SymBiMap Identity SBool
forall {k} {k} {k} (a :: k) (b :: k) (c :: k) d.
HasCallStack =>
[Char] -> TypeRep a -> TypeRep b -> TypeRep c -> d
translateBinaryError [Char]
"(<=)" (forall a. Typeable a => TypeRep a
forall {k} (a :: k). Typeable a => TypeRep a
R.typeRep @arg) (forall a. Typeable a => TypeRep a
forall {k} (a :: k). Typeable a => TypeRep a
R.typeRep @arg) (forall a. Typeable a => 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) =
  case (GrisetteSMTConfig integerBitWidth
config, forall a. Typeable a => TypeRep a
forall {k} (a :: k). Typeable a => TypeRep a
R.typeRep @a) of
    (GrisetteSMTConfig integerBitWidth, TypeRep a)
ResolvedBitsType -> GrisetteSMTConfig integerBitWidth
-> Term a
-> Term a
-> Term a
-> (SBV s' -> SBV s' -> TermTy integerBitWidth a)
-> State SymBiMap (TermTy integerBitWidth a)
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 SBV s' -> SBV s' -> TermTy integerBitWidth a
forall a. Bits a => a -> a -> a
(.&.)
    (GrisetteSMTConfig integerBitWidth, TypeRep a)
_ -> [Char]
-> TypeRep a
-> TypeRep a
-> TypeRep a
-> State SymBiMap (TermTy integerBitWidth a)
forall {k} {k} {k} (a :: k) (b :: k) (c :: k) d.
HasCallStack =>
[Char] -> TypeRep a -> TypeRep b -> TypeRep c -> d
translateBinaryError [Char]
"(.&.)" (forall a. Typeable a => TypeRep a
forall {k} (a :: k). Typeable a => TypeRep a
R.typeRep @a) (forall a. Typeable a => TypeRep a
forall {k} (a :: k). Typeable a => TypeRep a
R.typeRep @a) (forall a. Typeable a => 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 a. Typeable a => TypeRep a
forall {k} (a :: k). Typeable a => TypeRep a
R.typeRep @a) of
    (GrisetteSMTConfig integerBitWidth, TypeRep a)
ResolvedBitsType -> GrisetteSMTConfig integerBitWidth
-> Term a
-> Term a
-> Term a
-> (SBV s' -> SBV s' -> TermTy integerBitWidth a)
-> State SymBiMap (TermTy integerBitWidth a)
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 SBV s' -> SBV s' -> TermTy integerBitWidth a
forall a. Bits a => a -> a -> a
(.|.)
    (GrisetteSMTConfig integerBitWidth, TypeRep a)
_ -> [Char]
-> TypeRep a
-> TypeRep a
-> TypeRep a
-> State SymBiMap (TermTy integerBitWidth a)
forall {k} {k} {k} (a :: k) (b :: k) (c :: k) d.
HasCallStack =>
[Char] -> TypeRep a -> TypeRep b -> TypeRep c -> d
translateBinaryError [Char]
"(.|.)" (forall a. Typeable a => TypeRep a
forall {k} (a :: k). Typeable a => TypeRep a
R.typeRep @a) (forall a. Typeable a => TypeRep a
forall {k} (a :: k). Typeable a => TypeRep a
R.typeRep @a) (forall a. Typeable a => 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 a. Typeable a => TypeRep a
forall {k} (a :: k). Typeable a => TypeRep a
R.typeRep @a) of
    (GrisetteSMTConfig integerBitWidth, TypeRep a)
ResolvedBitsType -> GrisetteSMTConfig integerBitWidth
-> Term a
-> Term a
-> Term a
-> (SBV s' -> SBV s' -> TermTy integerBitWidth a)
-> State SymBiMap (TermTy integerBitWidth a)
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 SBV s' -> SBV s' -> TermTy integerBitWidth a
forall a. Bits a => a -> a -> a
xor
    (GrisetteSMTConfig integerBitWidth, TypeRep a)
_ -> [Char]
-> TypeRep a
-> TypeRep a
-> TypeRep a
-> State SymBiMap (TermTy integerBitWidth 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 a. Typeable a => TypeRep a
forall {k} (a :: k). Typeable a => TypeRep a
R.typeRep @a) (forall a. Typeable a => TypeRep a
forall {k} (a :: k). Typeable a => TypeRep a
R.typeRep @a) (forall a. Typeable a => 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 a. Typeable a => TypeRep a
forall {k} (a :: k). Typeable a => TypeRep a
R.typeRep @a) of
    (GrisetteSMTConfig integerBitWidth, TypeRep a)
ResolvedBitsType -> GrisetteSMTConfig integerBitWidth
-> Term a
-> Term a
-> (SBV s' -> SBV s')
-> State SymBiMap (TermTy integerBitWidth a)
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 SBV s' -> SBV s'
forall a. Bits a => a -> a
complement
    (GrisetteSMTConfig integerBitWidth, TypeRep a)
_ -> [Char]
-> TypeRep a
-> TypeRep a
-> State SymBiMap (TermTy integerBitWidth a)
forall {k} {k} (a :: k) (b :: k) c.
HasCallStack =>
[Char] -> TypeRep a -> TypeRep b -> c
translateUnaryError [Char]
"complement" (forall a. Typeable a => TypeRep a
forall {k} (a :: k). Typeable a => TypeRep a
R.typeRep @a) (forall a. Typeable a => 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 a. Typeable a => TypeRep a
forall {k} (a :: k). Typeable a => TypeRep a
R.typeRep @a) of
    (GrisetteSMTConfig integerBitWidth, TypeRep a)
ResolvedBitsType -> GrisetteSMTConfig integerBitWidth
-> Term a
-> Term a
-> (SBV s' -> SBV s')
-> State SymBiMap (TermTy integerBitWidth a)
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 (SBV s' -> Id -> SBV s'
forall a. Bits a => a -> Id -> a
`shift` Id
n)
    (GrisetteSMTConfig integerBitWidth, TypeRep a)
_ -> [Char]
-> TypeRep a
-> TypeRep Id
-> TypeRep a
-> State SymBiMap (TermTy integerBitWidth 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 a. Typeable a => TypeRep a
forall {k} (a :: k). Typeable a => TypeRep a
R.typeRep @a) (forall a. Typeable a => TypeRep a
forall {k} (a :: k). Typeable a => TypeRep a
R.typeRep @Int) (forall a. Typeable a => TypeRep a
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 a. Typeable a => TypeRep a
forall {k} (a :: k). Typeable a => TypeRep a
R.typeRep @a) of
    (GrisetteSMTConfig integerBitWidth, TypeRep a)
ResolvedBitsType -> GrisetteSMTConfig integerBitWidth
-> Term a
-> Term a
-> (SBV s' -> SBV s')
-> State SymBiMap (TermTy integerBitWidth a)
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 (SBV s' -> Id -> SBV s'
forall a. Bits a => a -> Id -> a
`rotate` Id
n)
    (GrisetteSMTConfig integerBitWidth, TypeRep a)
_ -> [Char]
-> TypeRep a
-> TypeRep Id
-> TypeRep a
-> State SymBiMap (TermTy integerBitWidth 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 a. Typeable a => TypeRep a
forall {k} (a :: k). Typeable a => TypeRep a
R.typeRep @a) (forall a. Typeable a => TypeRep a
forall {k} (a :: k). Typeable a => TypeRep a
R.typeRep @Int) (forall a. Typeable a => TypeRep a
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 a. Typeable a => TypeRep a
forall {k} (a :: k). Typeable a => TypeRep a
R.typeRep @a, forall a. Typeable a => TypeRep a
forall {k} (a :: k). Typeable a => TypeRep a
R.typeRep @x, forall a. Typeable a => TypeRep a
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
forall (a :: Nat) (b :: Nat). a :~: b
unsafeAxiom @(nx + ny) @na) of
        (n + n) :~: n
Refl -> GrisetteSMTConfig integerBitWidth
-> Term a
-> Term (bv a)
-> Term (bv b)
-> (SBV (WordN a) -> SBV (WordN b) -> TermTy integerBitWidth a)
-> State SymBiMap (TermTy integerBitWidth a)
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 SBV (WordN a) -> SBV (WordN b) -> TermTy integerBitWidth a
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
forall (a :: Nat) (b :: Nat). a :~: b
unsafeAxiom @(nx + ny) @na) of
        (n + n) :~: n
Refl ->
          GrisetteSMTConfig integerBitWidth
-> Term a
-> Term (bv a)
-> Term (bv b)
-> (SInt a -> SInt b -> TermTy integerBitWidth a)
-> State SymBiMap (TermTy integerBitWidth a)
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) ->
                SBV (WordN c) -> SBV (IntN c)
forall a b.
(Integral a, HasKind a, Num a, SymVal a, HasKind b, Num b,
 SymVal b) =>
SBV a -> SBV b
SBV.sFromIntegral (SBV (WordN c) -> SBV (IntN c)) -> SBV (WordN c) -> SBV (IntN c)
forall a b. (a -> b) -> a -> b
$
                  (SInt a -> SBV (WordN a)
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) SBV (WordN a) -> SBV (WordN b) -> SBV (WordN (a + b))
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.# (SInt b -> SBV (WordN 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 b
y :: SBV.SWord yn)
            )
    (TypeRep a, TypeRep (bv a), TypeRep (bv b))
_ -> [Char]
-> TypeRep (bv a)
-> TypeRep (bv b)
-> TypeRep a
-> State SymBiMap (TermTy integerBitWidth (bv c))
forall {k} {k} {k} (a :: k) (b :: k) (c :: k) d.
HasCallStack =>
[Char] -> TypeRep a -> TypeRep b -> TypeRep c -> d
translateBinaryError [Char]
"bvconcat" (forall a. Typeable a => TypeRep a
forall {k} (a :: k). Typeable a => TypeRep a
R.typeRep @x) (forall a. Typeable a => TypeRep a
forall {k} (a :: k). Typeable a => TypeRep a
R.typeRep @y) (forall a. Typeable a => TypeRep a
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 a. Typeable a => TypeRep a
forall {k} (a :: k). Typeable a => TypeRep a
R.typeRep @a, forall a. Typeable a => TypeRep a
forall {k} (a :: k). Typeable a => TypeRep a
R.typeRep @x) of
    (UnsignedBVType (Proxy n
_ :: Proxy na), UnsignedBVType (Proxy n
_ :: Proxy xn)) ->
      NatRepr ((w + ix) - 1)
-> (KnownNat ((w + ix) - 1) => State SymBiMap (SBV (WordN w)))
-> State SymBiMap (SBV (WordN w))
forall (n :: Nat) r. NatRepr n -> (KnownNat n => r) -> r
withKnownNat NatRepr ((w + ix) - 1)
NatRepr ((n + ix) - 1)
n1 ((KnownNat ((w + ix) - 1) => State SymBiMap (SBV (WordN w)))
 -> State SymBiMap (SBV (WordN w)))
-> (KnownNat ((w + ix) - 1) => State SymBiMap (SBV (WordN w)))
-> State SymBiMap (SBV (WordN w))
forall a b. (a -> b) -> a -> b
$
        case ( forall {k} (a :: k) (b :: k). a :~: b
forall (a :: Nat) (b :: Nat). 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) ->
            GrisetteSMTConfig integerBitWidth
-> Term a
-> Term (bv a)
-> (SBV (WordN a) -> SBV (WordN w))
-> State SymBiMap (TermTy integerBitWidth a)
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 (Proxy ((w + ix) - 1)
-> Proxy ix
-> SBV (WordN a)
-> SBV (WordN ((((w + ix) - 1) - ix) + 1))
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
forall {t :: Nat}. Proxy t
Proxy @(na + ix - 1)) (forall {k} (t :: k). Proxy t
forall {t :: Nat}. Proxy t
Proxy @ix))
      where
        n1 :: NatRepr (na + ix - 1)
        n1 :: NatRepr ((n + ix) - 1)
n1 = Natural -> NatRepr ((w + ix) - 1)
forall (n :: Nat). Natural -> NatRepr n
NatRepr (Proxy n -> Natural
forall (n :: Nat) (proxy :: Nat -> *).
KnownNat n =>
proxy n -> Natural
natVal (forall {k} (t :: k). Proxy t
forall {t :: Nat}. Proxy t
Proxy @na) Natural -> Natural -> Natural
forall a. Num a => a -> a -> a
+ Proxy ix -> Natural
forall (n :: Nat) (proxy :: Nat -> *).
KnownNat n =>
proxy n -> Natural
natVal (forall {k} (t :: k). Proxy t
forall {t :: Nat}. Proxy t
Proxy @ix) Natural -> Natural -> Natural
forall a. Num a => a -> a -> a
- Natural
1)
    (SignedBVType (Proxy n
_ :: Proxy na), SignedBVType (Proxy n
_ :: Proxy xn)) ->
      NatRepr ((w + ix) - 1)
-> (KnownNat ((w + ix) - 1) => State SymBiMap (SBV (IntN w)))
-> State SymBiMap (SBV (IntN w))
forall (n :: Nat) r. NatRepr n -> (KnownNat n => r) -> r
withKnownNat NatRepr ((w + ix) - 1)
NatRepr ((n + ix) - 1)
n1 ((KnownNat ((w + ix) - 1) => State SymBiMap (SBV (IntN w)))
 -> State SymBiMap (SBV (IntN w)))
-> (KnownNat ((w + ix) - 1) => State SymBiMap (SBV (IntN w)))
-> State SymBiMap (SBV (IntN w))
forall a b. (a -> b) -> a -> b
$
        case ( forall {k} (a :: k) (b :: k). a :~: b
forall (a :: Nat) (b :: Nat). 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) ->
            GrisetteSMTConfig integerBitWidth
-> Term a
-> Term (bv a)
-> (SBV (IntN a) -> SBV (IntN w))
-> State SymBiMap (TermTy integerBitWidth a)
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 (Proxy ((w + ix) - 1)
-> Proxy ix
-> SBV (IntN a)
-> SBV (IntN ((((w + ix) - 1) - ix) + 1))
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
forall {t :: Nat}. Proxy t
Proxy @(na + ix - 1)) (forall {k} (t :: k). Proxy t
forall {t :: Nat}. Proxy t
Proxy @ix))
      where
        n1 :: NatRepr (na + ix - 1)
        n1 :: NatRepr ((n + ix) - 1)
n1 = Natural -> NatRepr ((w + ix) - 1)
forall (n :: Nat). Natural -> NatRepr n
NatRepr (Proxy n -> Natural
forall (n :: Nat) (proxy :: Nat -> *).
KnownNat n =>
proxy n -> Natural
natVal (forall {k} (t :: k). Proxy t
forall {t :: Nat}. Proxy t
Proxy @na) Natural -> Natural -> Natural
forall a. Num a => a -> a -> a
+ Proxy ix -> Natural
forall (n :: Nat) (proxy :: Nat -> *).
KnownNat n =>
proxy n -> Natural
natVal (forall {k} (t :: k). Proxy t
forall {t :: Nat}. Proxy t
Proxy @ix) Natural -> Natural -> Natural
forall a. Num a => a -> a -> a
- Natural
1)
    (TypeRep a, TypeRep (bv a))
_ -> [Char]
-> TypeRep ix
-> TypeRep w
-> TypeRep (bv a)
-> TypeRep a
-> State SymBiMap (TermTy integerBitWidth (bv w))
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 a. Typeable a => TypeRep a
forall {k} (a :: k). Typeable a => TypeRep a
R.typeRep @x) (forall a. Typeable a => TypeRep a
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 a. Typeable a => TypeRep a
forall {k} (a :: k). Typeable a => TypeRep a
R.typeRep @a, forall a. Typeable a => TypeRep a
forall {k} (a :: k). Typeable a => TypeRep a
R.typeRep @x) of
    (UnsignedBVType (Proxy n
_ :: Proxy na), UnsignedBVType (Proxy n
_ :: Proxy nx)) ->
      NatRepr (b - a)
-> (KnownNat (b - a) => State SymBiMap (SBV (WordN b)))
-> State SymBiMap (SBV (WordN b))
forall (n :: Nat) r. NatRepr n -> (KnownNat n => r) -> r
withKnownNat (Natural -> NatRepr (b - a)
forall (n :: Nat). Natural -> NatRepr n
NatRepr (Proxy n -> Natural
forall (n :: Nat) (proxy :: Nat -> *).
KnownNat n =>
proxy n -> Natural
natVal (forall {k} (t :: k). Proxy t
forall {t :: Nat}. Proxy t
Proxy @na) Natural -> Natural -> Natural
forall a. Num a => a -> a -> a
- Proxy n -> Natural
forall (n :: Nat) (proxy :: Nat -> *).
KnownNat n =>
proxy n -> Natural
natVal (forall {k} (t :: k). Proxy t
forall {t :: Nat}. Proxy t
Proxy @nx)) :: NatRepr (na - nx)) ((KnownNat (b - a) => State SymBiMap (SBV (WordN b)))
 -> State SymBiMap (SBV (WordN b)))
-> (KnownNat (b - a) => State SymBiMap (SBV (WordN b)))
-> State SymBiMap (SBV (WordN b))
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) ((BVIsNonZero (n - n) => State SymBiMap (SBV (WordN b)))
 -> State SymBiMap (SBV (WordN b)))
-> (BVIsNonZero (n - n) => State SymBiMap (SBV (WordN b)))
-> State SymBiMap (SBV (WordN b))
forall a b. (a -> b) -> a -> b
$
              GrisetteSMTConfig integerBitWidth
-> Term a
-> Term (bv a)
-> (SBV (WordN a) -> SBV (WordN b))
-> State SymBiMap (TermTy integerBitWidth a)
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 SBV (WordN a) -> SBV (WordN b)
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 (WordN a) -> SBV (WordN b)
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)) ->
      NatRepr (b - a)
-> (KnownNat (b - a) => State SymBiMap (SBV (IntN b)))
-> State SymBiMap (SBV (IntN b))
forall (n :: Nat) r. NatRepr n -> (KnownNat n => r) -> r
withKnownNat (Natural -> NatRepr (b - a)
forall (n :: Nat). Natural -> NatRepr n
NatRepr (Proxy n -> Natural
forall (n :: Nat) (proxy :: Nat -> *).
KnownNat n =>
proxy n -> Natural
natVal (forall {k} (t :: k). Proxy t
forall {t :: Nat}. Proxy t
Proxy @na) Natural -> Natural -> Natural
forall a. Num a => a -> a -> a
- Proxy n -> Natural
forall (n :: Nat) (proxy :: Nat -> *).
KnownNat n =>
proxy n -> Natural
natVal (forall {k} (t :: k). Proxy t
forall {t :: Nat}. Proxy t
Proxy @nx)) :: NatRepr (na - nx)) ((KnownNat (b - a) => State SymBiMap (SBV (IntN b)))
 -> State SymBiMap (SBV (IntN b)))
-> (KnownNat (b - a) => State SymBiMap (SBV (IntN b)))
-> State SymBiMap (SBV (IntN b))
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) ((BVIsNonZero (n - n) => State SymBiMap (SBV (IntN b)))
 -> State SymBiMap (SBV (IntN b)))
-> (BVIsNonZero (n - n) => State SymBiMap (SBV (IntN b)))
-> State SymBiMap (SBV (IntN b))
forall a b. (a -> b) -> a -> b
$
              GrisetteSMTConfig integerBitWidth
-> Term a
-> Term (bv a)
-> (SBV (IntN a) -> SBV (IntN b))
-> State SymBiMap (TermTy integerBitWidth a)
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 SBV (IntN a) -> SBV (IntN b)
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 ->
                      SBV (WordN n) -> SBV (IntN b)
forall a b.
(Integral a, HasKind a, Num a, SymVal a, HasKind b, Num b,
 SymVal b) =>
SBV a -> SBV b
SBV.sFromIntegral
                        (SBV (WordN n) -> SBV (WordN n)
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 (SBV (IntN a) -> SBV (WordN n)
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))
_ -> [Char]
-> TypeRep Bool
-> TypeRep n
-> TypeRep (bv a)
-> TypeRep a
-> State SymBiMap (TermTy integerBitWidth (bv b))
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 a. Typeable a => TypeRep a
forall {k} (a :: k). Typeable a => TypeRep a
R.typeRep @Bool) TypeRep n
n (forall a. Typeable a => TypeRep a
forall {k} (a :: k). Typeable a => TypeRep a
R.typeRep @x) (forall a. Typeable a => TypeRep a
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 a. Typeable a => TypeRep a
forall {k} (a :: k). Typeable a => TypeRep a
R.typeRep @a) of
    (GrisetteSMTConfig integerBitWidth, TypeRep a)
ResolvedDeepType -> do
      TermTy integerBitWidth a -> s'
l1 <- GrisetteSMTConfig integerBitWidth
-> Term (a =-> a)
-> State SymBiMap (TermTy integerBitWidth (a =-> a))
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 <- GrisetteSMTConfig integerBitWidth
-> Term a -> State SymBiMap (TermTy integerBitWidth a)
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'
TermTy integerBitWidth a
g
      s' -> StateT SymBiMap Identity s'
forall (m :: * -> *) a. Monad m => a -> m a
return s'
g
    (GrisetteSMTConfig integerBitWidth, TypeRep a)
_ -> [Char]
-> TypeRep (a =-> a)
-> TypeRep a
-> TypeRep a
-> State SymBiMap (TermTy integerBitWidth 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 a. Typeable a => TypeRep a
forall {k} (a :: k). Typeable a => TypeRep a
R.typeRep @(b =-> a)) (forall a. Typeable a => TypeRep a
forall {k} (a :: k). Typeable a => TypeRep a
R.typeRep @b) (forall a. Typeable a => TypeRep a
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 a. Typeable a => TypeRep a
forall {k} (a :: k). Typeable a => TypeRep a
R.typeRep @a) of
    (GrisetteSMTConfig integerBitWidth, TypeRep a)
ResolvedDeepType -> do
      TermTy integerBitWidth a -> s'
l1 <- GrisetteSMTConfig integerBitWidth
-> Term (a --> a)
-> State SymBiMap (TermTy integerBitWidth (a --> a))
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 <- GrisetteSMTConfig integerBitWidth
-> Term a -> State SymBiMap (TermTy integerBitWidth a)
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'
TermTy integerBitWidth a
g
      s' -> StateT SymBiMap Identity s'
forall (m :: * -> *) a. Monad m => a -> m a
return s'
g
    (GrisetteSMTConfig integerBitWidth, TypeRep a)
_ -> [Char]
-> TypeRep (a --> a)
-> TypeRep a
-> TypeRep a
-> State SymBiMap (TermTy integerBitWidth 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 a. Typeable a => TypeRep a
forall {k} (a :: k). Typeable a => TypeRep a
R.typeRep @(b --> a)) (forall a. Typeable a => TypeRep a
forall {k} (a :: k). Typeable a => TypeRep a
R.typeRep @b) (forall a. Typeable a => TypeRep a
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 a. Typeable a => TypeRep a
forall {k} (a :: k). Typeable a => TypeRep a
R.typeRep @a) of
    (ResolvedConfig {}, TypeRep a
IntegerType) -> GrisetteSMTConfig integerBitWidth
-> Term a
-> Term Integer
-> Term Integer
-> (SBV s -> SBV s -> TermTy integerBitWidth a)
-> State SymBiMap (TermTy integerBitWidth a)
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 SBV s -> SBV s -> TermTy integerBitWidth a
forall a. SDivisible a => a -> a -> a
SBV.sDiv
    (GrisetteSMTConfig integerBitWidth, TypeRep a)
_ -> [Char]
-> TypeRep a
-> TypeRep a
-> TypeRep a
-> State SymBiMap (Aux (IsZero integerBitWidth) integerBitWidth)
forall {k} {k} {k} (a :: k) (b :: k) (c :: k) d.
HasCallStack =>
[Char] -> TypeRep a -> TypeRep b -> TypeRep c -> d
translateBinaryError [Char]
"div" (forall a. Typeable a => TypeRep a
forall {k} (a :: k). Typeable a => TypeRep a
R.typeRep @a) (forall a. Typeable a => TypeRep a
forall {k} (a :: k). Typeable a => TypeRep a
R.typeRep @a) (forall a. Typeable a => 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 a. Typeable a => TypeRep a
forall {k} (a :: k). Typeable a => TypeRep a
R.typeRep @a) of
    (ResolvedConfig {}, TypeRep a
IntegerType) -> GrisetteSMTConfig integerBitWidth
-> Term a
-> Term Integer
-> Term Integer
-> (SBV s -> SBV s -> TermTy integerBitWidth a)
-> State SymBiMap (TermTy integerBitWidth a)
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 SBV s -> SBV s -> TermTy integerBitWidth a
forall a. SDivisible a => a -> a -> a
SBV.sMod
    (GrisetteSMTConfig integerBitWidth, TypeRep a)
_ -> [Char]
-> TypeRep a
-> TypeRep a
-> TypeRep a
-> State SymBiMap (Aux (IsZero integerBitWidth) integerBitWidth)
forall {k} {k} {k} (a :: k) (b :: k) (c :: k) d.
HasCallStack =>
[Char] -> TypeRep a -> TypeRep b -> TypeRep c -> d
translateBinaryError [Char]
"mod" (forall a. Typeable a => TypeRep a
forall {k} (a :: k). Typeable a => TypeRep a
R.typeRep @a) (forall a. Typeable a => TypeRep a
forall {k} (a :: k). Typeable a => TypeRep a
R.typeRep @a) (forall a. Typeable a => TypeRep a
forall {k} (a :: k). Typeable a => TypeRep a
R.typeRep @a)
lowerSinglePrimImpl' GrisetteSMTConfig integerBitWidth
_ Term a
_ = State SymBiMap (TermTy integerBitWidth 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_" [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ Id -> [Char]
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 SymbolicT IO (SymBiMap, SBV s' -> SBV s')
-> Maybe (SymbolicT IO (SymBiMap, SBV s' -> SBV s'))
forall a. a -> Maybe a
Just (SymbolicT IO (SymBiMap, SBV s' -> SBV s')
 -> Maybe (SymbolicT IO (SymBiMap, SBV s' -> SBV s')))
-> SymbolicT IO (SymBiMap, SBV s' -> SBV s')
-> Maybe (SymbolicT IO (SymBiMap, SBV s' -> SBV s'))
forall a b. (a -> b) -> a -> b
$ (SymBiMap, SBV s' -> SBV s')
-> SymbolicT IO (SymBiMap, SBV s' -> SBV s')
forall (m :: * -> *) a. Monad m => a -> m a
return (HasCallStack =>
SomeTerm
-> Dynamic -> [Char] -> SomeTypedSymbol -> SymBiMap -> SymBiMap
SomeTerm
-> Dynamic -> [Char] -> SomeTypedSymbol -> SymBiMap -> SymBiMap
addBiMap (Term a -> SomeTerm
forall a. SupportedPrim a => Term a -> SomeTerm
SomeTerm Term a
term) ((SBV s' -> SBV s') -> Dynamic
forall a. Typeable a => a -> Dynamic
toDyn SBV s' -> SBV s'
TermTy integerBitWidth s1 -> TermTy integerBitWidth s2
f) [Char]
name (TypedSymbol a -> SomeTypedSymbol
forall t. TypedSymbol t -> SomeTypedSymbol
someTypedSymbol TypedSymbol a
ts) SymBiMap
m, SBV s' -> SBV s'
TermTy integerBitWidth s1 -> TermTy integerBitWidth s2
f)
  ((GrisetteSMTConfig integerBitWidth, TypeRep s1),
 (GrisetteSMTConfig integerBitWidth, TypeRep s2))
_ -> Maybe (Symbolic (SymBiMap, TermTy integerBitWidth (s1 =-> s2)))
forall a. Maybe a
Nothing
buildUTFun11 GrisetteSMTConfig integerBitWidth
_ TypeRep s1
_ TypeRep s2
_ Term a
_ SymBiMap
_ = [Char]
-> Maybe
     (Symbolic
        (SymBiMap, TermTy integerBitWidth s1 -> TermTy integerBitWidth s2))
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_" [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ Id -> [Char]
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 SymbolicT IO (SymBiMap, SBV s' -> SBV s' -> SBV s')
-> Maybe (SymbolicT IO (SymBiMap, SBV s' -> SBV s' -> SBV s'))
forall a. a -> Maybe a
Just (SymbolicT IO (SymBiMap, SBV s' -> SBV s' -> SBV s')
 -> Maybe (SymbolicT IO (SymBiMap, SBV s' -> SBV s' -> SBV s')))
-> SymbolicT IO (SymBiMap, SBV s' -> SBV s' -> SBV s')
-> Maybe (SymbolicT IO (SymBiMap, SBV s' -> SBV s' -> SBV s'))
forall a b. (a -> b) -> a -> b
$ (SymBiMap, SBV s' -> SBV s' -> SBV s')
-> SymbolicT IO (SymBiMap, SBV s' -> SBV s' -> SBV s')
forall (m :: * -> *) a. Monad m => a -> m a
return (HasCallStack =>
SomeTerm
-> Dynamic -> [Char] -> SomeTypedSymbol -> SymBiMap -> SymBiMap
SomeTerm
-> Dynamic -> [Char] -> SomeTypedSymbol -> SymBiMap -> SymBiMap
addBiMap (Term a -> SomeTerm
forall a. SupportedPrim a => Term a -> SomeTerm
SomeTerm Term a
term) ((SBV s' -> SBV s' -> SBV s') -> Dynamic
forall a. Typeable a => a -> Dynamic
toDyn SBV s' -> SBV s' -> SBV s'
TermTy integerBitWidth s1
-> TermTy integerBitWidth s2 -> TermTy integerBitWidth s3
f) [Char]
name (TypedSymbol a -> SomeTypedSymbol
forall t. TypedSymbol t -> SomeTypedSymbol
someTypedSymbol TypedSymbol a
ts) SymBiMap
m, SBV s' -> SBV s' -> SBV s'
TermTy integerBitWidth s1
-> TermTy integerBitWidth s2 -> TermTy integerBitWidth s3
f)
  ((GrisetteSMTConfig integerBitWidth, TypeRep s1),
 (GrisetteSMTConfig integerBitWidth, TypeRep s2),
 (GrisetteSMTConfig integerBitWidth, TypeRep s3))
_ -> Maybe
  (Symbolic (SymBiMap, TermTy integerBitWidth (s1 =-> (s2 =-> s3))))
forall a. Maybe a
Nothing
buildUTFun111 GrisetteSMTConfig integerBitWidth
_ TypeRep s1
_ TypeRep s2
_ TypeRep s3
_ Term a
_ SymBiMap
_ = [Char]
-> Maybe
     (Symbolic
        (SymBiMap,
         TermTy integerBitWidth s1
         -> TermTy integerBitWidth s2 -> TermTy integerBitWidth s3))
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_" [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ Id -> [Char]
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 SymbolicT IO (SymBiMap, SBV s' -> SBV s')
-> Maybe (SymbolicT IO (SymBiMap, SBV s' -> SBV s'))
forall a. a -> Maybe a
Just (SymbolicT IO (SymBiMap, SBV s' -> SBV s')
 -> Maybe (SymbolicT IO (SymBiMap, SBV s' -> SBV s')))
-> SymbolicT IO (SymBiMap, SBV s' -> SBV s')
-> Maybe (SymbolicT IO (SymBiMap, SBV s' -> SBV s'))
forall a b. (a -> b) -> a -> b
$ (SymBiMap, SBV s' -> SBV s')
-> SymbolicT IO (SymBiMap, SBV s' -> SBV s')
forall (m :: * -> *) a. Monad m => a -> m a
return (HasCallStack =>
SomeTerm
-> Dynamic -> [Char] -> SomeTypedSymbol -> SymBiMap -> SymBiMap
SomeTerm
-> Dynamic -> [Char] -> SomeTypedSymbol -> SymBiMap -> SymBiMap
addBiMap (Term a -> SomeTerm
forall a. SupportedPrim a => Term a -> SomeTerm
SomeTerm Term a
term) ((SBV s' -> SBV s') -> Dynamic
forall a. Typeable a => a -> Dynamic
toDyn SBV s' -> SBV s'
TermTy integerBitWidth s1 -> TermTy integerBitWidth s2
f) [Char]
name (TypedSymbol a -> SomeTypedSymbol
forall t. TypedSymbol t -> SomeTypedSymbol
someTypedSymbol TypedSymbol a
ts) SymBiMap
m, SBV s' -> SBV s'
TermTy integerBitWidth s1 -> TermTy integerBitWidth s2
f)
  ((GrisetteSMTConfig integerBitWidth, TypeRep s1),
 (GrisetteSMTConfig integerBitWidth, TypeRep s2))
_ -> Maybe (Symbolic (SymBiMap, TermTy integerBitWidth (s1 --> s2)))
forall a. Maybe a
Nothing
buildUGFun11 GrisetteSMTConfig integerBitWidth
_ TypeRep s1
_ TypeRep s2
_ Term a
_ SymBiMap
_ = [Char]
-> Maybe
     (Symbolic
        (SymBiMap, TermTy integerBitWidth s1 -> TermTy integerBitWidth s2))
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_" [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ Id -> [Char]
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 SymbolicT IO (SymBiMap, SBV s' -> SBV s' -> SBV s')
-> Maybe (SymbolicT IO (SymBiMap, SBV s' -> SBV s' -> SBV s'))
forall a. a -> Maybe a
Just (SymbolicT IO (SymBiMap, SBV s' -> SBV s' -> SBV s')
 -> Maybe (SymbolicT IO (SymBiMap, SBV s' -> SBV s' -> SBV s')))
-> SymbolicT IO (SymBiMap, SBV s' -> SBV s' -> SBV s')
-> Maybe (SymbolicT IO (SymBiMap, SBV s' -> SBV s' -> SBV s'))
forall a b. (a -> b) -> a -> b
$ (SymBiMap, SBV s' -> SBV s' -> SBV s')
-> SymbolicT IO (SymBiMap, SBV s' -> SBV s' -> SBV s')
forall (m :: * -> *) a. Monad m => a -> m a
return (HasCallStack =>
SomeTerm
-> Dynamic -> [Char] -> SomeTypedSymbol -> SymBiMap -> SymBiMap
SomeTerm
-> Dynamic -> [Char] -> SomeTypedSymbol -> SymBiMap -> SymBiMap
addBiMap (Term a -> SomeTerm
forall a. SupportedPrim a => Term a -> SomeTerm
SomeTerm Term a
term) ((SBV s' -> SBV s' -> SBV s') -> Dynamic
forall a. Typeable a => a -> Dynamic
toDyn SBV s' -> SBV s' -> SBV s'
TermTy integerBitWidth s1
-> TermTy integerBitWidth s2 -> TermTy integerBitWidth s3
f) [Char]
name (TypedSymbol a -> SomeTypedSymbol
forall t. TypedSymbol t -> SomeTypedSymbol
someTypedSymbol TypedSymbol a
ts) SymBiMap
m, SBV s' -> SBV s' -> SBV s'
TermTy integerBitWidth s1
-> TermTy integerBitWidth s2 -> TermTy integerBitWidth s3
f)
  ((GrisetteSMTConfig integerBitWidth, TypeRep s1),
 (GrisetteSMTConfig integerBitWidth, TypeRep s2),
 (GrisetteSMTConfig integerBitWidth, TypeRep s3))
_ -> Maybe
  (Symbolic (SymBiMap, TermTy integerBitWidth (s1 --> (s2 --> s3))))
forall a. Maybe a
Nothing
buildUGFun111 GrisetteSMTConfig integerBitWidth
_ TypeRep s1
_ TypeRep s2
_ TypeRep s3
_ Term a
_ SymBiMap
_ = [Char]
-> Maybe
     (Symbolic
        (SymBiMap,
         TermTy integerBitWidth s1
         -> TermTy integerBitWidth s2 -> TermTy integerBitWidth s3))
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 a. Typeable a => TypeRep a
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) -> GrisetteSMTConfig integerBitWidth
-> TypeRep a
-> TypeRep b
-> TypeRep c
-> Term a
-> SymBiMap
-> Maybe
     (Symbolic (SymBiMap, TermTy integerBitWidth (a =-> (b =-> c))))
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) -> GrisetteSMTConfig integerBitWidth
-> TypeRep a
-> TypeRep b
-> Term a
-> SymBiMap
-> Maybe (Symbolic (SymBiMap, TermTy integerBitWidth (a =-> b)))
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) -> GrisetteSMTConfig integerBitWidth
-> TypeRep a
-> TypeRep b
-> TypeRep c
-> Term a
-> SymBiMap
-> Maybe
     (Symbolic (SymBiMap, TermTy integerBitWidth (a --> (b --> c))))
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) -> GrisetteSMTConfig integerBitWidth
-> TypeRep a
-> TypeRep b
-> Term a
-> SymBiMap
-> Maybe (Symbolic (SymBiMap, TermTy integerBitWidth (a --> b)))
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
_ -> Maybe (Symbolic (SymBiMap, TermTy integerBitWidth a))
forall a. Maybe a
Nothing
lowerSinglePrimUFun GrisetteSMTConfig integerBitWidth
_ Term a
_ SymBiMap
_ = [Char] -> Maybe (Symbolic (SymBiMap, TermTy integerBitWidth a))
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) <- GrisetteSMTConfig integerBitWidth
-> Term a
-> SymBiMap
-> Symbolic (SymBiMap, TermTy integerBitWidth a)
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
  (SymBiMap, x1) -> Symbolic (SymBiMap, x1)
forall (m :: * -> *) a. Monad m => a -> m a
return (HasCallStack => SomeTerm -> Dynamic -> SymBiMap -> SymBiMap
SomeTerm -> Dynamic -> SymBiMap -> SymBiMap
addBiMapIntermediate (Term x -> SomeTerm
forall a. SupportedPrim a => Term a -> SomeTerm
SomeTerm Term x
orig) (x1 -> Dynamic
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) <- GrisetteSMTConfig integerBitWidth
-> Term a
-> SymBiMap
-> Symbolic (SymBiMap, TermTy integerBitWidth a)
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) <- GrisetteSMTConfig integerBitWidth
-> Term b
-> SymBiMap
-> Symbolic (SymBiMap, TermTy integerBitWidth b)
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
  (SymBiMap, x1) -> Symbolic (SymBiMap, x1)
forall (m :: * -> *) a. Monad m => a -> m a
return (HasCallStack => SomeTerm -> Dynamic -> SymBiMap -> SymBiMap
SomeTerm -> Dynamic -> SymBiMap -> SymBiMap
addBiMapIntermediate (Term x -> SomeTerm
forall a. SupportedPrim a => Term a -> SomeTerm
SomeTerm Term x
orig) (x1 -> Dynamic
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 =
  Term a
-> (SupportedPrim a =>
    Symbolic (SymBiMap, TermTy integerBitWidth a))
-> Symbolic (SymBiMap, TermTy integerBitWidth a)
forall t a. Term t -> (SupportedPrim t => a) -> a
introSupportedPrimConstraint Term a
t ((SupportedPrim a => Symbolic (SymBiMap, TermTy integerBitWidth a))
 -> Symbolic (SymBiMap, TermTy integerBitWidth a))
-> (SupportedPrim a =>
    Symbolic (SymBiMap, TermTy integerBitWidth a))
-> Symbolic (SymBiMap, TermTy integerBitWidth a)
forall a b. (a -> b) -> a -> b
$
    case (GrisetteSMTConfig integerBitWidth
config, forall a. Typeable a => TypeRep a
forall {k} (a :: k). Typeable a => TypeRep a
R.typeRep @a) of
      (GrisetteSMTConfig integerBitWidth, TypeRep a)
ResolvedDeepType ->
        case HasCallStack => SomeTerm -> SymBiMap -> Maybe Dynamic
SomeTerm -> SymBiMap -> Maybe Dynamic
lookupTerm (Term a -> SomeTerm
forall a. SupportedPrim a => Term a -> SomeTerm
SomeTerm Term a
t) SymBiMap
m of
          Just Dynamic
x -> (SymBiMap, s') -> SymbolicT IO (SymBiMap, s')
forall (m :: * -> *) a. Monad m => a -> m a
return (SymBiMap
m, Dynamic -> s' -> s'
forall a. Typeable a => Dynamic -> a -> a
fromDyn Dynamic
x s'
forall a. HasCallStack => a
undefined)
          Maybe Dynamic
Nothing -> GrisetteSMTConfig integerBitWidth
-> Term a
-> SymBiMap
-> Symbolic (SymBiMap, TermTy integerBitWidth a)
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)
_ -> TypeRep a -> Symbolic (SymBiMap, TermTy integerBitWidth a)
forall {k} (a :: k) b. HasCallStack => TypeRep a -> b
translateTypeError (forall a. Typeable a => TypeRep a
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 = GrisetteSMTConfig integerBitWidth
-> Term a
-> SymBiMap
-> Symbolic (SymBiMap, TermTy integerBitWidth a)
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 =
  [Char] -> b
forall a. HasCallStack => [Char] -> a
error ([Char] -> b) -> [Char] -> b
forall a b. (a -> b) -> a -> b
$
    [Char]
"Don't know how to translate the type " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ TypeRep a -> [Char]
forall a. Show a => a -> [Char]
show TypeRep a
ta [Char] -> [Char] -> [Char]
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 =
  [Char] -> c
forall a. HasCallStack => [Char] -> a
error ([Char] -> c) -> [Char] -> c
forall a b. (a -> b) -> a -> b
$
    [Char]
"Don't know how to translate the op "
      [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Char] -> [Char]
forall a. Show a => a -> [Char]
show [Char]
op
      [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Char]
" :: "
      [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ TypeRep a -> [Char]
forall a. Show a => a -> [Char]
show TypeRep a
ta
      [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Char]
" -> "
      [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ TypeRep b -> [Char]
forall a. Show a => a -> [Char]
show TypeRep b
tb
      [Char] -> [Char] -> [Char]
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 =
  [Char] -> d
forall a. HasCallStack => [Char] -> a
error ([Char] -> d) -> [Char] -> d
forall a b. (a -> b) -> a -> b
$
    [Char]
"Don't know how to translate the op "
      [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Char] -> [Char]
forall a. Show a => a -> [Char]
show [Char]
op
      [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Char]
" :: "
      [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ TypeRep a -> [Char]
forall a. Show a => a -> [Char]
show TypeRep a
ta
      [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Char]
" -> "
      [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ TypeRep b -> [Char]
forall a. Show a => a -> [Char]
show TypeRep b
tb
      [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Char]
" -> "
      [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ TypeRep c -> [Char]
forall a. Show a => a -> [Char]
show TypeRep c
tc
      [Char] -> [Char] -> [Char]
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 =
  [Char] -> e
forall a. HasCallStack => [Char] -> a
error ([Char] -> e) -> [Char] -> e
forall a b. (a -> b) -> a -> b
$
    [Char]
"Don't know how to translate the op "
      [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Char] -> [Char]
forall a. Show a => a -> [Char]
show [Char]
op
      [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Char]
" :: "
      [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ TypeRep a -> [Char]
forall a. Show a => a -> [Char]
show TypeRep a
ta
      [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Char]
" -> "
      [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ TypeRep b -> [Char]
forall a. Show a => a -> [Char]
show TypeRep b
tb
      [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Char]
" -> "
      [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ TypeRep c -> [Char]
forall a. Show a => a -> [Char]
show TypeRep c
tc
      [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Char]
" -> "
      [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ TypeRep d -> [Char]
forall a. Show a => a -> [Char]
show TypeRep d
td
      [Char] -> [Char] -> [Char]
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 a. Typeable a => TypeRep a
forall {k} (a :: k). Typeable a => TypeRep a
R.typeRep @a of
    TypeRep a
BoolType -> (SymBiMap, SBool) -> SymbolicT IO (SymBiMap, SBool)
forall (m :: * -> *) a. Monad m => a -> m a
return (SymBiMap
m, if a
Bool
v then SBool
SBV.sTrue else SBool
SBV.sFalse)
    TypeRep a
IntegerType -> (SymBiMap, SBV s) -> SymbolicT IO (SymBiMap, SBV s)
forall (m :: * -> *) a. Monad m => a -> m a
return (SymBiMap
m, Integer -> SBV s
forall a. Num a => Integer -> a
fromInteger a
Integer
v)
    SignedBVType Proxy n
_ -> case a
v of
      IntN Integer
x -> (SymBiMap, SBV (IntN n)) -> SymbolicT IO (SymBiMap, SBV (IntN n))
forall (m :: * -> *) a. Monad m => a -> m a
return (SymBiMap
m, Integer -> SBV (IntN n)
forall a. Num a => Integer -> a
fromInteger Integer
x)
    UnsignedBVType Proxy n
_ -> case a
v of
      WordN Integer
x -> (SymBiMap, SBV (WordN n)) -> SymbolicT IO (SymBiMap, SBV (WordN n))
forall (m :: * -> *) a. Monad m => a -> m a
return (SymBiMap
m, Integer -> SBV (WordN n)
forall a. Num a => Integer -> a
fromInteger Integer
x)
    TypeRep a
_ -> TypeRep a -> Symbolic (SymBiMap, TermTy integerBitWidth a)
forall {k} (a :: k) b. HasCallStack => TypeRep a -> b
translateTypeError (forall a. Typeable a => TypeRep a
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 =
  Symbolic (SymBiMap, TermTy integerBitWidth a)
-> Maybe (Symbolic (SymBiMap, TermTy integerBitWidth a))
-> Symbolic (SymBiMap, TermTy integerBitWidth a)
forall a. a -> Maybe a -> a
fromMaybe Symbolic (SymBiMap, TermTy integerBitWidth a)
forall t1. t1
errorMsg (Maybe (Symbolic (SymBiMap, TermTy integerBitWidth a))
 -> Symbolic (SymBiMap, TermTy integerBitWidth a))
-> Maybe (Symbolic (SymBiMap, TermTy integerBitWidth a))
-> Symbolic (SymBiMap, TermTy integerBitWidth a)
forall a b. (a -> b) -> a -> b
$ [Maybe (Symbolic (SymBiMap, TermTy integerBitWidth a))]
-> Maybe (Symbolic (SymBiMap, TermTy integerBitWidth a))
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 = TypeRep a -> x
forall {k} (a :: k) b. HasCallStack => TypeRep a -> b
translateTypeError (forall a. Typeable a => TypeRep a
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 a. Typeable a => TypeRep a
forall {k} (a :: k). Typeable a => TypeRep a
R.typeRep @a) of
      (GrisetteSMTConfig integerBitWidth, TypeRep a)
ResolvedSimpleType -> SymbolicT IO (SymBiMap, SBV s')
-> Maybe (SymbolicT IO (SymBiMap, SBV s'))
forall a. a -> Maybe a
Just (SymbolicT IO (SymBiMap, SBV s')
 -> Maybe (SymbolicT IO (SymBiMap, SBV s')))
-> SymbolicT IO (SymBiMap, SBV s')
-> Maybe (SymbolicT IO (SymBiMap, SBV s'))
forall a b. (a -> b) -> a -> b
$ do
        let name :: [Char]
name = TypedSymbol a -> [Char]
forall a. Show a => a -> [Char]
show TypedSymbol a
ts
        (TermTy integerBitWidth a
g :: TermTy integerBitWidth a) <- [Char] -> Symbolic (SBV s')
forall a. SymVal a => [Char] -> Symbolic (SBV a)
SBV.free [Char]
name
        (SymBiMap, SBV s') -> SymbolicT IO (SymBiMap, SBV s')
forall (m :: * -> *) a. Monad m => a -> m a
return (HasCallStack =>
SomeTerm
-> Dynamic -> [Char] -> SomeTypedSymbol -> SymBiMap -> SymBiMap
SomeTerm
-> Dynamic -> [Char] -> SomeTypedSymbol -> SymBiMap -> SymBiMap
addBiMap (Term a -> SomeTerm
forall a. SupportedPrim a => Term a -> SomeTerm
SomeTerm Term a
t) (SBV s' -> Dynamic
forall a. Typeable a => a -> Dynamic
toDyn SBV s'
TermTy integerBitWidth a
g) [Char]
name (TypedSymbol a -> SomeTypedSymbol
forall t. TypedSymbol t -> SomeTypedSymbol
someTypedSymbol TypedSymbol a
ts) SymBiMap
m, SBV s'
TermTy integerBitWidth a
g)
      (GrisetteSMTConfig integerBitWidth, TypeRep a)
_ -> Maybe (Symbolic (SymBiMap, TermTy integerBitWidth a))
forall a. Maybe a
Nothing
    ufunc :: (Maybe (SBV.Symbolic (SymBiMap, TermTy integerBitWidth a)))
    ufunc :: Maybe (Symbolic (SymBiMap, TermTy integerBitWidth a))
ufunc = GrisetteSMTConfig integerBitWidth
-> Term a
-> SymBiMap
-> Maybe (Symbolic (SymBiMap, TermTy integerBitWidth a))
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
_ = Symbolic (SymBiMap, TermTy integerBitWidth a)
forall t1. t1
errorMsg
  where
    errorMsg :: forall t1. t1
    errorMsg :: forall t1. t1
errorMsg = [Char] -> TypeRep arg -> TypeRep a -> t1
forall {k} {k} (a :: k) (b :: k) c.
HasCallStack =>
[Char] -> TypeRep a -> TypeRep b -> c
translateUnaryError (tag -> [Char]
forall a. Show a => a -> [Char]
show tag
op) (forall a. Typeable a => TypeRep a
forall {k} (a :: k). Typeable a => TypeRep a
R.typeRep @x) (forall a. Typeable a => TypeRep a
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
_ = Symbolic (SymBiMap, TermTy integerBitWidth a)
forall t1. t1
errorMsg
  where
    errorMsg :: forall t1. t1
    errorMsg :: forall t1. t1
errorMsg = [Char] -> TypeRep arg1 -> TypeRep arg2 -> TypeRep a -> t1
forall {k} {k} {k} (a :: k) (b :: k) (c :: k) d.
HasCallStack =>
[Char] -> TypeRep a -> TypeRep b -> TypeRep c -> d
translateBinaryError (tag -> [Char]
forall a. Show a => a -> [Char]
show tag
op) (forall a. Typeable a => TypeRep a
forall {k} (a :: k). Typeable a => TypeRep a
R.typeRep @x) (forall a. Typeable a => TypeRep a
forall {k} (a :: k). Typeable a => TypeRep a
R.typeRep @y) (forall a. Typeable a => TypeRep a
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
_ = Symbolic (SymBiMap, TermTy integerBitWidth a)
forall t1. t1
errorMsg
  where
    errorMsg :: forall t1. t1
    errorMsg :: forall t1. t1
errorMsg = [Char]
-> TypeRep arg1 -> TypeRep arg2 -> TypeRep arg3 -> TypeRep a -> t1
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 (tag -> [Char]
forall a. Show a => a -> [Char]
show tag
op) (forall a. Typeable a => TypeRep a
forall {k} (a :: k). Typeable a => TypeRep a
R.typeRep @x) (forall a. Typeable a => TypeRep a
forall {k} (a :: k). Typeable a => TypeRep a
R.typeRep @y) (forall a. Typeable a => TypeRep a
forall {k} (a :: k). Typeable a => TypeRep a
R.typeRep @z) (forall a. Typeable a => TypeRep a
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 = GrisetteSMTConfig integerBitWidth
-> Term a
-> Term Bool
-> (SBool -> SBool)
-> SymBiMap
-> SymbolicT IO (SymBiMap, SBool)
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 = GrisetteSMTConfig integerBitWidth
-> Term a
-> Term Bool
-> Term Bool
-> (SBool -> SBool -> SBool)
-> SymBiMap
-> SymbolicT IO (SymBiMap, SBool)
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 = GrisetteSMTConfig integerBitWidth
-> Term a
-> Term Bool
-> Term Bool
-> (SBool -> SBool -> SBool)
-> SymBiMap
-> SymbolicT IO (SymBiMap, SBool)
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 a. Typeable a => TypeRep a
forall {k} (a :: k). Typeable a => TypeRep a
R.typeRep @x) of
    (GrisetteSMTConfig integerBitWidth, TypeRep t1)
ResolvedSimpleType -> GrisetteSMTConfig integerBitWidth
-> Term a
-> Term t1
-> Term t1
-> (SBV s' -> SBV s' -> SBool)
-> SymBiMap
-> SymbolicT IO (SymBiMap, SBool)
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 SBV s' -> SBV s' -> SBool
forall a. EqSymbolic a => a -> a -> SBool
(SBV..==) SymBiMap
m
    (GrisetteSMTConfig integerBitWidth, TypeRep t1)
_ -> [Char]
-> TypeRep t1
-> TypeRep t1
-> TypeRep a
-> SymbolicT IO (SymBiMap, SBool)
forall {k} {k} {k} (a :: k) (b :: k) (c :: k) d.
HasCallStack =>
[Char] -> TypeRep a -> TypeRep b -> TypeRep c -> d
translateBinaryError [Char]
"(==)" (forall a. Typeable a => TypeRep a
forall {k} (a :: k). Typeable a => TypeRep a
R.typeRep @x) (forall a. Typeable a => TypeRep a
forall {k} (a :: k). Typeable a => TypeRep a
R.typeRep @x) (forall a. Typeable a => TypeRep a
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 a. Typeable a => TypeRep a
forall {k} (a :: k). Typeable a => TypeRep a
R.typeRep @a) of
    (GrisetteSMTConfig integerBitWidth, TypeRep a)
ResolvedSimpleType -> do
      (SymBiMap
m1, SBool
l1) <- GrisetteSMTConfig integerBitWidth
-> Term Bool
-> SymBiMap
-> Symbolic (SymBiMap, TermTy integerBitWidth Bool)
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) <- GrisetteSMTConfig integerBitWidth
-> Term a
-> SymBiMap
-> Symbolic (SymBiMap, TermTy integerBitWidth a)
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) <- GrisetteSMTConfig integerBitWidth
-> Term a
-> SymBiMap
-> Symbolic (SymBiMap, TermTy integerBitWidth a)
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 = SBool -> SBV s' -> SBV s' -> SBV s'
forall a. Mergeable a => SBool -> a -> a -> a
SBV.ite SBool
l1 SBV s'
l2 SBV s'
l3
      (SymBiMap, SBV s') -> SymbolicT IO (SymBiMap, SBV s')
forall (m :: * -> *) a. Monad m => a -> m a
return (HasCallStack => SomeTerm -> Dynamic -> SymBiMap -> SymBiMap
SomeTerm -> Dynamic -> SymBiMap -> SymBiMap
addBiMapIntermediate (Term a -> SomeTerm
forall a. SupportedPrim a => Term a -> SomeTerm
SomeTerm Term a
t) (SBV s' -> Dynamic
forall a. Typeable a => a -> Dynamic
toDyn SBV s'
g) SymBiMap
m3, SBV s'
g)
    (GrisetteSMTConfig integerBitWidth, TypeRep a)
_ -> [Char]
-> TypeRep Bool
-> TypeRep a
-> TypeRep a
-> TypeRep a
-> Symbolic (SymBiMap, TermTy integerBitWidth 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 a. Typeable a => TypeRep a
forall {k} (a :: k). Typeable a => TypeRep a
R.typeRep @Bool) (forall a. Typeable a => TypeRep a
forall {k} (a :: k). Typeable a => TypeRep a
R.typeRep @a) (forall a. Typeable a => TypeRep a
forall {k} (a :: k). Typeable a => TypeRep a
R.typeRep @a) (forall a. Typeable a => 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 a. Typeable a => TypeRep a
forall {k} (a :: k). Typeable a => TypeRep a
R.typeRep @a) of
    (GrisetteSMTConfig integerBitWidth, TypeRep a)
ResolvedNumType -> GrisetteSMTConfig integerBitWidth
-> Term a
-> Term a
-> Term a
-> (SBV s' -> SBV s' -> SBV s')
-> SymBiMap
-> Symbolic (SymBiMap, SBV s')
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 SBV s' -> SBV s' -> SBV s'
forall a. Num a => a -> a -> a
(+) SymBiMap
m
    (GrisetteSMTConfig integerBitWidth, TypeRep a)
_ -> [Char]
-> TypeRep a
-> TypeRep a
-> TypeRep a
-> Symbolic (SymBiMap, TermTy integerBitWidth a)
forall {k} {k} {k} (a :: k) (b :: k) (c :: k) d.
HasCallStack =>
[Char] -> TypeRep a -> TypeRep b -> TypeRep c -> d
translateBinaryError [Char]
"(+)" (forall a. Typeable a => TypeRep a
forall {k} (a :: k). Typeable a => TypeRep a
R.typeRep @a) (forall a. Typeable a => TypeRep a
forall {k} (a :: k). Typeable a => TypeRep a
R.typeRep @a) (forall a. Typeable a => 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 a. Typeable a => TypeRep a
forall {k} (a :: k). Typeable a => TypeRep a
R.typeRep @a) of
    (GrisetteSMTConfig integerBitWidth, TypeRep a)
ResolvedNumType -> GrisetteSMTConfig integerBitWidth
-> Term a
-> Term a
-> (SBV s' -> SBV s')
-> SymBiMap
-> Symbolic (SymBiMap, SBV s')
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 SBV s' -> SBV s'
forall a. Num a => a -> a
negate SymBiMap
m
    (GrisetteSMTConfig integerBitWidth, TypeRep a)
_ -> [Char]
-> TypeRep a
-> TypeRep a
-> Symbolic (SymBiMap, TermTy integerBitWidth a)
forall {k} {k} (a :: k) (b :: k) c.
HasCallStack =>
[Char] -> TypeRep a -> TypeRep b -> c
translateUnaryError [Char]
"negate" (forall a. Typeable a => TypeRep a
forall {k} (a :: k). Typeable a => TypeRep a
R.typeRep @a) (forall a. Typeable a => 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 a. Typeable a => TypeRep a
forall {k} (a :: k). Typeable a => TypeRep a
R.typeRep @a) of
    (GrisetteSMTConfig integerBitWidth, TypeRep a)
ResolvedNumType -> GrisetteSMTConfig integerBitWidth
-> Term a
-> Term a
-> Term a
-> (SBV s' -> SBV s' -> SBV s')
-> SymBiMap
-> Symbolic (SymBiMap, SBV s')
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 SBV s' -> SBV s' -> SBV s'
forall a. Num a => a -> a -> a
(*) SymBiMap
m
    (GrisetteSMTConfig integerBitWidth, TypeRep a)
_ -> [Char]
-> TypeRep a
-> TypeRep a
-> TypeRep a
-> Symbolic (SymBiMap, TermTy integerBitWidth a)
forall {k} {k} {k} (a :: k) (b :: k) (c :: k) d.
HasCallStack =>
[Char] -> TypeRep a -> TypeRep b -> TypeRep c -> d
translateBinaryError [Char]
"(*)" (forall a. Typeable a => TypeRep a
forall {k} (a :: k). Typeable a => TypeRep a
R.typeRep @a) (forall a. Typeable a => TypeRep a
forall {k} (a :: k). Typeable a => TypeRep a
R.typeRep @a) (forall a. Typeable a => 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 a. Typeable a => TypeRep a
forall {k} (a :: k). Typeable a => TypeRep a
R.typeRep @a) of
    (GrisetteSMTConfig integerBitWidth, TypeRep a)
ResolvedNumType -> GrisetteSMTConfig integerBitWidth
-> Term a
-> Term a
-> (SBV s' -> SBV s')
-> SymBiMap
-> Symbolic (SymBiMap, SBV s')
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 SBV s' -> SBV s'
forall a. Num a => a -> a
abs SymBiMap
m
    (GrisetteSMTConfig integerBitWidth, TypeRep a)
_ -> [Char]
-> TypeRep a
-> TypeRep a
-> Symbolic (SymBiMap, TermTy integerBitWidth a)
forall {k} {k} (a :: k) (b :: k) c.
HasCallStack =>
[Char] -> TypeRep a -> TypeRep b -> c
translateUnaryError [Char]
"abs" (forall a. Typeable a => TypeRep a
forall {k} (a :: k). Typeable a => TypeRep a
R.typeRep @a) (forall a. Typeable a => 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 a. Typeable a => TypeRep a
forall {k} (a :: k). Typeable a => TypeRep a
R.typeRep @a) of
    (GrisetteSMTConfig integerBitWidth, TypeRep a)
ResolvedNumType -> GrisetteSMTConfig integerBitWidth
-> Term a
-> Term a
-> (SBV s' -> SBV s')
-> SymBiMap
-> Symbolic (SymBiMap, SBV s')
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 SBV s' -> SBV s'
forall a. Num a => a -> a
signum SymBiMap
m
    (GrisetteSMTConfig integerBitWidth, TypeRep a)
_ -> [Char]
-> TypeRep a
-> TypeRep a
-> Symbolic (SymBiMap, TermTy integerBitWidth a)
forall {k} {k} (a :: k) (b :: k) c.
HasCallStack =>
[Char] -> TypeRep a -> TypeRep b -> c
translateUnaryError [Char]
"signum" (forall a. Typeable a => TypeRep a
forall {k} (a :: k). Typeable a => TypeRep a
R.typeRep @a) (forall a. Typeable a => 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 a. Typeable a => TypeRep a
forall {k} (a :: k). Typeable a => TypeRep a
R.typeRep @arg) of
    (GrisetteSMTConfig integerBitWidth, TypeRep t1)
ResolvedNumOrdType -> GrisetteSMTConfig integerBitWidth
-> Term a
-> Term t1
-> Term t1
-> (SBV s' -> SBV s' -> SBool)
-> SymBiMap
-> SymbolicT IO (SymBiMap, SBool)
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 SBV s' -> SBV s' -> SBool
forall a. OrdSymbolic a => a -> a -> SBool
(SBV..<) SymBiMap
m
    (GrisetteSMTConfig integerBitWidth, TypeRep t1)
_ -> [Char]
-> TypeRep a
-> TypeRep a
-> TypeRep Bool
-> SymbolicT IO (SymBiMap, SBool)
forall {k} {k} {k} (a :: k) (b :: k) (c :: k) d.
HasCallStack =>
[Char] -> TypeRep a -> TypeRep b -> TypeRep c -> d
translateBinaryError [Char]
"(<)" (forall a. Typeable a => TypeRep a
forall {k} (a :: k). Typeable a => TypeRep a
R.typeRep @a) (forall a. Typeable a => TypeRep a
forall {k} (a :: k). Typeable a => TypeRep a
R.typeRep @a) (forall a. Typeable a => 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 a. Typeable a => TypeRep a
forall {k} (a :: k). Typeable a => TypeRep a
R.typeRep @arg) of
    (GrisetteSMTConfig integerBitWidth, TypeRep t1)
ResolvedNumOrdType -> GrisetteSMTConfig integerBitWidth
-> Term a
-> Term t1
-> Term t1
-> (SBV s' -> SBV s' -> SBool)
-> SymBiMap
-> SymbolicT IO (SymBiMap, SBool)
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 SBV s' -> SBV s' -> SBool
forall a. OrdSymbolic a => a -> a -> SBool
(SBV..<=) SymBiMap
m
    (GrisetteSMTConfig integerBitWidth, TypeRep t1)
_ -> [Char]
-> TypeRep a
-> TypeRep a
-> TypeRep Bool
-> SymbolicT IO (SymBiMap, SBool)
forall {k} {k} {k} (a :: k) (b :: k) (c :: k) d.
HasCallStack =>
[Char] -> TypeRep a -> TypeRep b -> TypeRep c -> d
translateBinaryError [Char]
"(<=)" (forall a. Typeable a => TypeRep a
forall {k} (a :: k). Typeable a => TypeRep a
R.typeRep @a) (forall a. Typeable a => TypeRep a
forall {k} (a :: k). Typeable a => TypeRep a
R.typeRep @a) (forall a. Typeable a => 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 a. Typeable a => TypeRep a
forall {k} (a :: k). Typeable a => TypeRep a
R.typeRep @a) of
    (GrisetteSMTConfig integerBitWidth, TypeRep a)
ResolvedBitsType -> GrisetteSMTConfig integerBitWidth
-> Term a
-> Term a
-> Term a
-> (SBV s' -> SBV s' -> SBV s')
-> SymBiMap
-> Symbolic (SymBiMap, SBV s')
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 SBV s' -> SBV s' -> SBV s'
forall a. Bits a => a -> a -> a
(.&.) SymBiMap
m
    (GrisetteSMTConfig integerBitWidth, TypeRep a)
_ -> [Char]
-> TypeRep a
-> TypeRep a
-> TypeRep a
-> Symbolic (SymBiMap, TermTy integerBitWidth a)
forall {k} {k} {k} (a :: k) (b :: k) (c :: k) d.
HasCallStack =>
[Char] -> TypeRep a -> TypeRep b -> TypeRep c -> d
translateBinaryError [Char]
"(.&.)" (forall a. Typeable a => TypeRep a
forall {k} (a :: k). Typeable a => TypeRep a
R.typeRep @a) (forall a. Typeable a => TypeRep a
forall {k} (a :: k). Typeable a => TypeRep a
R.typeRep @a) (forall a. Typeable a => 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 a. Typeable a => TypeRep a
forall {k} (a :: k). Typeable a => TypeRep a
R.typeRep @a) of
    (GrisetteSMTConfig integerBitWidth, TypeRep a)
ResolvedBitsType -> GrisetteSMTConfig integerBitWidth
-> Term a
-> Term a
-> Term a
-> (SBV s' -> SBV s' -> SBV s')
-> SymBiMap
-> Symbolic (SymBiMap, SBV s')
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 SBV s' -> SBV s' -> SBV s'
forall a. Bits a => a -> a -> a
(.|.) SymBiMap
m
    (GrisetteSMTConfig integerBitWidth, TypeRep a)
_ -> [Char]
-> TypeRep a
-> TypeRep a
-> TypeRep a
-> Symbolic (SymBiMap, TermTy integerBitWidth a)
forall {k} {k} {k} (a :: k) (b :: k) (c :: k) d.
HasCallStack =>
[Char] -> TypeRep a -> TypeRep b -> TypeRep c -> d
translateBinaryError [Char]
"(.|.)" (forall a. Typeable a => TypeRep a
forall {k} (a :: k). Typeable a => TypeRep a
R.typeRep @a) (forall a. Typeable a => TypeRep a
forall {k} (a :: k). Typeable a => TypeRep a
R.typeRep @a) (forall a. Typeable a => 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 a. Typeable a => TypeRep a
forall {k} (a :: k). Typeable a => TypeRep a
R.typeRep @a) of
    (GrisetteSMTConfig integerBitWidth, TypeRep a)
ResolvedBitsType -> GrisetteSMTConfig integerBitWidth
-> Term a
-> Term a
-> Term a
-> (SBV s' -> SBV s' -> SBV s')
-> SymBiMap
-> Symbolic (SymBiMap, SBV s')
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 SBV s' -> SBV s' -> SBV s'
forall a. Bits a => a -> a -> a
xor SymBiMap
m
    (GrisetteSMTConfig integerBitWidth, TypeRep a)
_ -> [Char]
-> TypeRep a
-> TypeRep a
-> TypeRep a
-> Symbolic (SymBiMap, TermTy integerBitWidth 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 a. Typeable a => TypeRep a
forall {k} (a :: k). Typeable a => TypeRep a
R.typeRep @a) (forall a. Typeable a => TypeRep a
forall {k} (a :: k). Typeable a => TypeRep a
R.typeRep @a) (forall a. Typeable a => 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 a. Typeable a => TypeRep a
forall {k} (a :: k). Typeable a => TypeRep a
R.typeRep @a) of
    (GrisetteSMTConfig integerBitWidth, TypeRep a)
ResolvedBitsType -> GrisetteSMTConfig integerBitWidth
-> Term a
-> Term a
-> (SBV s' -> SBV s')
-> SymBiMap
-> Symbolic (SymBiMap, SBV s')
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 SBV s' -> SBV s'
forall a. Bits a => a -> a
complement SymBiMap
m
    (GrisetteSMTConfig integerBitWidth, TypeRep a)
_ -> [Char]
-> TypeRep a
-> TypeRep a
-> Symbolic (SymBiMap, TermTy integerBitWidth a)
forall {k} {k} (a :: k) (b :: k) c.
HasCallStack =>
[Char] -> TypeRep a -> TypeRep b -> c
translateUnaryError [Char]
"complement" (forall a. Typeable a => TypeRep a
forall {k} (a :: k). Typeable a => TypeRep a
R.typeRep @a) (forall a. Typeable a => 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 a. Typeable a => TypeRep a
forall {k} (a :: k). Typeable a => TypeRep a
R.typeRep @a) of
    (GrisetteSMTConfig integerBitWidth, TypeRep a)
ResolvedBitsType -> GrisetteSMTConfig integerBitWidth
-> Term a
-> Term a
-> (SBV s' -> SBV s')
-> SymBiMap
-> Symbolic (SymBiMap, SBV s')
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 (SBV s' -> Id -> SBV s'
forall a. Bits a => a -> Id -> a
`shift` Id
n) SymBiMap
m
    (GrisetteSMTConfig integerBitWidth, TypeRep a)
_ -> [Char]
-> TypeRep a
-> TypeRep Id
-> TypeRep a
-> Symbolic (SymBiMap, TermTy integerBitWidth 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 a. Typeable a => TypeRep a
forall {k} (a :: k). Typeable a => TypeRep a
R.typeRep @a) (forall a. Typeable a => TypeRep a
forall {k} (a :: k). Typeable a => TypeRep a
R.typeRep @Int) (forall a. Typeable a => TypeRep a
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 a. Typeable a => TypeRep a
forall {k} (a :: k). Typeable a => TypeRep a
R.typeRep @a) of
    (GrisetteSMTConfig integerBitWidth, TypeRep a)
ResolvedBitsType -> GrisetteSMTConfig integerBitWidth
-> Term a
-> Term a
-> (SBV s' -> SBV s')
-> SymBiMap
-> Symbolic (SymBiMap, SBV s')
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 (SBV s' -> Id -> SBV s'
forall a. Bits a => a -> Id -> a
`rotate` Id
n) SymBiMap
m
    (GrisetteSMTConfig integerBitWidth, TypeRep a)
_ -> [Char]
-> TypeRep a
-> TypeRep Id
-> TypeRep a
-> Symbolic (SymBiMap, TermTy integerBitWidth 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 a. Typeable a => TypeRep a
forall {k} (a :: k). Typeable a => TypeRep a
R.typeRep @a) (forall a. Typeable a => TypeRep a
forall {k} (a :: k). Typeable a => TypeRep a
R.typeRep @Int) (forall a. Typeable a => TypeRep a
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 a. Typeable a => TypeRep a
forall {k} (a :: k). Typeable a => TypeRep a
R.typeRep @a, forall a. Typeable a => TypeRep a
forall {k} (a :: k). Typeable a => TypeRep a
R.typeRep @x, forall a. Typeable a => TypeRep a
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
forall (a :: Nat) (b :: Nat). a :~: b
unsafeAxiom @(nx + ny) @na) of
        (n + n) :~: n
Refl -> GrisetteSMTConfig integerBitWidth
-> Term a
-> Term (bv a)
-> Term (bv b)
-> (SBV (WordN a) -> SBV (WordN b) -> SBV (WordN c))
-> SymBiMap
-> Symbolic (SymBiMap, SBV (WordN c))
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 SBV (WordN a) -> SBV (WordN b) -> SBV (WordN c)
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
forall (a :: Nat) (b :: Nat). a :~: b
unsafeAxiom @(nx + ny) @na) of
        (n + n) :~: n
Refl ->
          GrisetteSMTConfig integerBitWidth
-> Term a
-> Term (bv a)
-> Term (bv b)
-> (SInt a -> SInt b -> SBV (IntN c))
-> SymBiMap
-> Symbolic (SymBiMap, SBV (IntN c))
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) ->
                SBV (WordN c) -> SBV (IntN c)
forall a b.
(Integral a, HasKind a, Num a, SymVal a, HasKind b, Num b,
 SymVal b) =>
SBV a -> SBV b
SBV.sFromIntegral (SBV (WordN c) -> SBV (IntN c)) -> SBV (WordN c) -> SBV (IntN c)
forall a b. (a -> b) -> a -> b
$
                  (SInt a -> SBV (WordN a)
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) SBV (WordN a) -> SBV (WordN b) -> SBV (WordN (a + b))
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.# (SInt b -> SBV (WordN 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 b
y :: SBV.SWord yn)
            )
            SymBiMap
m
    (TypeRep a, TypeRep (bv a), TypeRep (bv b))
_ -> [Char]
-> TypeRep (bv a)
-> TypeRep (bv b)
-> TypeRep a
-> Symbolic (SymBiMap, TermTy integerBitWidth (bv c))
forall {k} {k} {k} (a :: k) (b :: k) (c :: k) d.
HasCallStack =>
[Char] -> TypeRep a -> TypeRep b -> TypeRep c -> d
translateBinaryError [Char]
"bvconcat" (forall a. Typeable a => TypeRep a
forall {k} (a :: k). Typeable a => TypeRep a
R.typeRep @x) (forall a. Typeable a => TypeRep a
forall {k} (a :: k). Typeable a => TypeRep a
R.typeRep @y) (forall a. Typeable a => TypeRep a
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 a. Typeable a => TypeRep a
forall {k} (a :: k). Typeable a => TypeRep a
R.typeRep @a, forall a. Typeable a => TypeRep a
forall {k} (a :: k). Typeable a => TypeRep a
R.typeRep @x) of
    (UnsignedBVType (Proxy n
_ :: Proxy na), UnsignedBVType (Proxy n
_ :: Proxy xn)) ->
      NatRepr ((w + ix) - 1)
-> (KnownNat ((w + ix) - 1) => Symbolic (SymBiMap, SBV (WordN w)))
-> Symbolic (SymBiMap, SBV (WordN w))
forall (n :: Nat) r. NatRepr n -> (KnownNat n => r) -> r
withKnownNat NatRepr ((w + ix) - 1)
NatRepr ((n + ix) - 1)
n1 ((KnownNat ((w + ix) - 1) => Symbolic (SymBiMap, SBV (WordN w)))
 -> Symbolic (SymBiMap, SBV (WordN w)))
-> (KnownNat ((w + ix) - 1) => Symbolic (SymBiMap, SBV (WordN w)))
-> Symbolic (SymBiMap, SBV (WordN w))
forall a b. (a -> b) -> a -> b
$
        case ( forall {k} (a :: k) (b :: k). a :~: b
forall (a :: Nat) (b :: Nat). 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) ->
            GrisetteSMTConfig integerBitWidth
-> Term a
-> Term (bv a)
-> (SBV (WordN a) -> SBV (WordN ((((w + ix) - 1) - ix) + 1)))
-> SymBiMap
-> Symbolic (SymBiMap, SBV (WordN ((((w + ix) - 1) - ix) + 1)))
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 (Proxy ((w + ix) - 1)
-> Proxy ix
-> SBV (WordN a)
-> SBV (WordN ((((w + ix) - 1) - ix) + 1))
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
forall {t :: Nat}. Proxy t
Proxy @(na + ix - 1)) (forall {k} (t :: k). Proxy t
forall {t :: Nat}. Proxy t
Proxy @ix)) SymBiMap
m
      where
        n1 :: NatRepr (na + ix - 1)
        n1 :: NatRepr ((n + ix) - 1)
n1 = Natural -> NatRepr ((w + ix) - 1)
forall (n :: Nat). Natural -> NatRepr n
NatRepr (Proxy n -> Natural
forall (n :: Nat) (proxy :: Nat -> *).
KnownNat n =>
proxy n -> Natural
natVal (forall {k} (t :: k). Proxy t
forall {t :: Nat}. Proxy t
Proxy @na) Natural -> Natural -> Natural
forall a. Num a => a -> a -> a
+ Proxy ix -> Natural
forall (n :: Nat) (proxy :: Nat -> *).
KnownNat n =>
proxy n -> Natural
natVal (forall {k} (t :: k). Proxy t
forall {t :: Nat}. Proxy t
Proxy @ix) Natural -> Natural -> Natural
forall a. Num a => a -> a -> a
- Natural
1)
    (SignedBVType (Proxy n
_ :: Proxy na), SignedBVType (Proxy n
_ :: Proxy xn)) ->
      NatRepr ((w + ix) - 1)
-> (KnownNat ((w + ix) - 1) => Symbolic (SymBiMap, SBV (IntN w)))
-> Symbolic (SymBiMap, SBV (IntN w))
forall (n :: Nat) r. NatRepr n -> (KnownNat n => r) -> r
withKnownNat NatRepr ((w + ix) - 1)
NatRepr ((n + ix) - 1)
n1 ((KnownNat ((w + ix) - 1) => Symbolic (SymBiMap, SBV (IntN w)))
 -> Symbolic (SymBiMap, SBV (IntN w)))
-> (KnownNat ((w + ix) - 1) => Symbolic (SymBiMap, SBV (IntN w)))
-> Symbolic (SymBiMap, SBV (IntN w))
forall a b. (a -> b) -> a -> b
$
        case ( forall {k} (a :: k) (b :: k). a :~: b
forall (a :: Nat) (b :: Nat). 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) ->
            GrisetteSMTConfig integerBitWidth
-> Term a
-> Term (bv a)
-> (SBV (IntN a) -> SBV (IntN ((((w + ix) - 1) - ix) + 1)))
-> SymBiMap
-> Symbolic (SymBiMap, SBV (IntN ((((w + ix) - 1) - ix) + 1)))
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 (Proxy ((w + ix) - 1)
-> Proxy ix
-> SBV (IntN a)
-> SBV (IntN ((((w + ix) - 1) - ix) + 1))
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
forall {t :: Nat}. Proxy t
Proxy @(na + ix - 1)) (forall {k} (t :: k). Proxy t
forall {t :: Nat}. Proxy t
Proxy @ix)) SymBiMap
m
      where
        n1 :: NatRepr (na + ix - 1)
        n1 :: NatRepr ((n + ix) - 1)
n1 = Natural -> NatRepr ((w + ix) - 1)
forall (n :: Nat). Natural -> NatRepr n
NatRepr (Proxy n -> Natural
forall (n :: Nat) (proxy :: Nat -> *).
KnownNat n =>
proxy n -> Natural
natVal (forall {k} (t :: k). Proxy t
forall {t :: Nat}. Proxy t
Proxy @na) Natural -> Natural -> Natural
forall a. Num a => a -> a -> a
+ Proxy ix -> Natural
forall (n :: Nat) (proxy :: Nat -> *).
KnownNat n =>
proxy n -> Natural
natVal (forall {k} (t :: k). Proxy t
forall {t :: Nat}. Proxy t
Proxy @ix) Natural -> Natural -> Natural
forall a. Num a => a -> a -> a
- Natural
1)
    (TypeRep a, TypeRep (bv a))
_ -> [Char]
-> TypeRep ix
-> TypeRep w
-> TypeRep (bv a)
-> TypeRep a
-> Symbolic (SymBiMap, TermTy integerBitWidth (bv w))
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 a. Typeable a => TypeRep a
forall {k} (a :: k). Typeable a => TypeRep a
R.typeRep @x) (forall a. Typeable a => TypeRep a
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 a. Typeable a => TypeRep a
forall {k} (a :: k). Typeable a => TypeRep a
R.typeRep @a, forall a. Typeable a => TypeRep a
forall {k} (a :: k). Typeable a => TypeRep a
R.typeRep @x) of
    (UnsignedBVType (Proxy n
_ :: Proxy na), UnsignedBVType (Proxy n
_ :: Proxy nx)) ->
      NatRepr (b - a)
-> (KnownNat (b - a) => Symbolic (SymBiMap, SBV (WordN b)))
-> Symbolic (SymBiMap, SBV (WordN b))
forall (n :: Nat) r. NatRepr n -> (KnownNat n => r) -> r
withKnownNat (Natural -> NatRepr (b - a)
forall (n :: Nat). Natural -> NatRepr n
NatRepr (Proxy n -> Natural
forall (n :: Nat) (proxy :: Nat -> *).
KnownNat n =>
proxy n -> Natural
natVal (forall {k} (t :: k). Proxy t
forall {t :: Nat}. Proxy t
Proxy @na) Natural -> Natural -> Natural
forall a. Num a => a -> a -> a
- Proxy n -> Natural
forall (n :: Nat) (proxy :: Nat -> *).
KnownNat n =>
proxy n -> Natural
natVal (forall {k} (t :: k). Proxy t
forall {t :: Nat}. Proxy t
Proxy @nx)) :: NatRepr (na - nx)) ((KnownNat (b - a) => Symbolic (SymBiMap, SBV (WordN b)))
 -> Symbolic (SymBiMap, SBV (WordN b)))
-> (KnownNat (b - a) => Symbolic (SymBiMap, SBV (WordN b)))
-> Symbolic (SymBiMap, SBV (WordN b))
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) ((BVIsNonZero (n - n) => Symbolic (SymBiMap, SBV (WordN b)))
 -> Symbolic (SymBiMap, SBV (WordN b)))
-> (BVIsNonZero (n - n) => Symbolic (SymBiMap, SBV (WordN b)))
-> Symbolic (SymBiMap, SBV (WordN b))
forall a b. (a -> b) -> a -> b
$
              GrisetteSMTConfig integerBitWidth
-> Term a
-> Term (bv a)
-> (SBV (WordN a) -> SBV (WordN b))
-> SymBiMap
-> Symbolic (SymBiMap, SBV (WordN 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 SBV (WordN a) -> SBV (WordN b)
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 (WordN a) -> SBV (WordN b)
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)) ->
      NatRepr (b - a)
-> (KnownNat (b - a) => Symbolic (SymBiMap, SBV (IntN b)))
-> Symbolic (SymBiMap, SBV (IntN b))
forall (n :: Nat) r. NatRepr n -> (KnownNat n => r) -> r
withKnownNat (Natural -> NatRepr (b - a)
forall (n :: Nat). Natural -> NatRepr n
NatRepr (Proxy n -> Natural
forall (n :: Nat) (proxy :: Nat -> *).
KnownNat n =>
proxy n -> Natural
natVal (forall {k} (t :: k). Proxy t
forall {t :: Nat}. Proxy t
Proxy @na) Natural -> Natural -> Natural
forall a. Num a => a -> a -> a
- Proxy n -> Natural
forall (n :: Nat) (proxy :: Nat -> *).
KnownNat n =>
proxy n -> Natural
natVal (forall {k} (t :: k). Proxy t
forall {t :: Nat}. Proxy t
Proxy @nx)) :: NatRepr (na - nx)) ((KnownNat (b - a) => Symbolic (SymBiMap, SBV (IntN b)))
 -> Symbolic (SymBiMap, SBV (IntN b)))
-> (KnownNat (b - a) => Symbolic (SymBiMap, SBV (IntN b)))
-> Symbolic (SymBiMap, SBV (IntN b))
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) ((BVIsNonZero (n - n) => Symbolic (SymBiMap, SBV (IntN b)))
 -> Symbolic (SymBiMap, SBV (IntN b)))
-> (BVIsNonZero (n - n) => Symbolic (SymBiMap, SBV (IntN b)))
-> Symbolic (SymBiMap, SBV (IntN b))
forall a b. (a -> b) -> a -> b
$
              GrisetteSMTConfig integerBitWidth
-> Term a
-> Term (bv a)
-> (SBV (IntN a) -> SBV (IntN b))
-> SymBiMap
-> Symbolic (SymBiMap, SBV (IntN 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 SBV (IntN a) -> SBV (IntN b)
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 ->
                      SBV (WordN n) -> SBV (IntN b)
forall a b.
(Integral a, HasKind a, Num a, SymVal a, HasKind b, Num b,
 SymVal b) =>
SBV a -> SBV b
SBV.sFromIntegral
                        (SBV (WordN n) -> SBV (WordN n)
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 (SBV (IntN a) -> SBV (WordN n)
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))
_ -> [Char]
-> TypeRep Bool
-> TypeRep n
-> TypeRep (bv a)
-> TypeRep a
-> Symbolic (SymBiMap, TermTy integerBitWidth (bv b))
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 a. Typeable a => TypeRep a
forall {k} (a :: k). Typeable a => TypeRep a
R.typeRep @Bool) TypeRep n
n (forall a. Typeable a => TypeRep a
forall {k} (a :: k). Typeable a => TypeRep a
R.typeRep @x) (forall a. Typeable a => TypeRep a
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 a. Typeable a => TypeRep a
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) <- GrisetteSMTConfig integerBitWidth
-> Term (a =-> a)
-> SymBiMap
-> Symbolic (SymBiMap, TermTy integerBitWidth (a =-> a))
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) <- GrisetteSMTConfig integerBitWidth
-> Term a
-> SymBiMap
-> Symbolic (SymBiMap, TermTy integerBitWidth a)
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
      (SymBiMap, s') -> SymbolicT IO (SymBiMap, s')
forall (m :: * -> *) a. Monad m => a -> m a
return (HasCallStack => SomeTerm -> Dynamic -> SymBiMap -> SymBiMap
SomeTerm -> Dynamic -> SymBiMap -> SymBiMap
addBiMapIntermediate (Term a -> SomeTerm
forall a. SupportedPrim a => Term a -> SomeTerm
SomeTerm Term a
t) (s' -> Dynamic
forall a. Typeable a => a -> Dynamic
toDyn s'
g) SymBiMap
m2, s'
g)
    (GrisetteSMTConfig integerBitWidth, TypeRep a)
_ -> [Char]
-> TypeRep (a =-> a)
-> TypeRep a
-> TypeRep a
-> Symbolic (SymBiMap, TermTy integerBitWidth 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 a. Typeable a => TypeRep a
forall {k} (a :: k). Typeable a => TypeRep a
R.typeRep @(b =-> a)) (forall a. Typeable a => TypeRep a
forall {k} (a :: k). Typeable a => TypeRep a
R.typeRep @b) (forall a. Typeable a => TypeRep a
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 a. Typeable a => TypeRep a
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) <- GrisetteSMTConfig integerBitWidth
-> Term (a --> a)
-> SymBiMap
-> Symbolic (SymBiMap, TermTy integerBitWidth (a --> a))
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) <- GrisetteSMTConfig integerBitWidth
-> Term a
-> SymBiMap
-> Symbolic (SymBiMap, TermTy integerBitWidth a)
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
      (SymBiMap, s') -> SymbolicT IO (SymBiMap, s')
forall (m :: * -> *) a. Monad m => a -> m a
return (HasCallStack => SomeTerm -> Dynamic -> SymBiMap -> SymBiMap
SomeTerm -> Dynamic -> SymBiMap -> SymBiMap
addBiMapIntermediate (Term a -> SomeTerm
forall a. SupportedPrim a => Term a -> SomeTerm
SomeTerm Term a
t) (s' -> Dynamic
forall a. Typeable a => a -> Dynamic
toDyn s'
g) SymBiMap
m2, s'
g)
    (GrisetteSMTConfig integerBitWidth, TypeRep a)
_ -> [Char]
-> TypeRep (a --> a)
-> TypeRep a
-> TypeRep a
-> Symbolic (SymBiMap, TermTy integerBitWidth 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 a. Typeable a => TypeRep a
forall {k} (a :: k). Typeable a => TypeRep a
R.typeRep @(b --> a)) (forall a. Typeable a => TypeRep a
forall {k} (a :: k). Typeable a => TypeRep a
R.typeRep @b) (forall a. Typeable a => TypeRep a
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 a. Typeable a => TypeRep a
forall {k} (a :: k). Typeable a => TypeRep a
R.typeRep @a) of
    (ResolvedConfig {}, TypeRep a
IntegerType) -> GrisetteSMTConfig integerBitWidth
-> Term a
-> Term Integer
-> Term Integer
-> (SBV s -> SBV s -> SBV s)
-> SymBiMap
-> Symbolic (SymBiMap, SBV s)
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 SBV s -> SBV s -> SBV s
forall a. SDivisible a => a -> a -> a
SBV.sDiv SymBiMap
m
    (GrisetteSMTConfig integerBitWidth, TypeRep a)
_ -> [Char]
-> TypeRep a
-> TypeRep a
-> TypeRep a
-> Symbolic
     (SymBiMap, Aux (IsZero integerBitWidth) integerBitWidth)
forall {k} {k} {k} (a :: k) (b :: k) (c :: k) d.
HasCallStack =>
[Char] -> TypeRep a -> TypeRep b -> TypeRep c -> d
translateBinaryError [Char]
"div" (forall a. Typeable a => TypeRep a
forall {k} (a :: k). Typeable a => TypeRep a
R.typeRep @a) (forall a. Typeable a => TypeRep a
forall {k} (a :: k). Typeable a => TypeRep a
R.typeRep @a) (forall a. Typeable a => 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 a. Typeable a => TypeRep a
forall {k} (a :: k). Typeable a => TypeRep a
R.typeRep @a) of
    (ResolvedConfig {}, TypeRep a
IntegerType) -> GrisetteSMTConfig integerBitWidth
-> Term a
-> Term Integer
-> Term Integer
-> (SBV s -> SBV s -> SBV s)
-> SymBiMap
-> Symbolic (SymBiMap, SBV s)
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 SBV s -> SBV s -> SBV s
forall a. SDivisible a => a -> a -> a
SBV.sMod SymBiMap
m
    (GrisetteSMTConfig integerBitWidth, TypeRep a)
_ -> [Char]
-> TypeRep a
-> TypeRep a
-> TypeRep a
-> Symbolic
     (SymBiMap, Aux (IsZero integerBitWidth) integerBitWidth)
forall {k} {k} {k} (a :: k) (b :: k) (c :: k) d.
HasCallStack =>
[Char] -> TypeRep a -> TypeRep b -> TypeRep c -> d
translateBinaryError [Char]
"mod" (forall a. Typeable a => TypeRep a
forall {k} (a :: k). Typeable a => TypeRep a
R.typeRep @a) (forall a. Typeable a => TypeRep a
forall {k} (a :: k). Typeable a => TypeRep a
R.typeRep @a) (forall a. Typeable a => TypeRep a
forall {k} (a :: k). Typeable a => TypeRep a
R.typeRep @a)
lowerSinglePrimImpl GrisetteSMTConfig integerBitWidth
_ Term a
_ SymBiMap
_ = [Char] -> Symbolic (SymBiMap, TermTy integerBitWidth a)
forall a. HasCallStack => [Char] -> a
error [Char]
"Should never happen"

unsafeMkNatRepr :: Int -> NatRepr w
unsafeMkNatRepr :: forall (w :: Nat). Id -> NatRepr w
unsafeMkNatRepr Id
x = Natural -> NatRepr w
forall (n :: Nat). Natural -> NatRepr n
NatRepr (Integer -> Natural
forall a. Num a => Integer -> a
fromInteger (Integer -> Natural) -> Integer -> Natural
forall a b. (a -> b) -> a -> b
$ Id -> Integer
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 Id -> Id -> Bool
forall a. Ord a => a -> a -> Bool
<= Id
0 = [Char] -> r
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 (Id -> NatRepr w
forall (w :: Nat). Id -> NatRepr w
unsafeMkNatRepr Id
i) ((KnownNat w => r) -> r) -> (KnownNat w => r) -> r
forall a b. (a -> b) -> a -> b
$ ((1 <= w) => r) -> r
unsafeBVIsNonZero (KnownNat w, 1 <= w) => r
(1 <= w) => r
r
  where
    unsafeBVIsNonZero :: ((1 <= w) => r) -> r
    unsafeBVIsNonZero :: ((1 <= w) => r) -> r
unsafeBVIsNonZero (1 <= w) => r
r1 = case w :~: 1
forall {k} (a :: k) (b :: k). a :~: b
unsafeAxiom :: w :~: 1 of
      w :~: 1
Refl -> r
(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 w :~: 1
forall {k} (a :: k) (b :: k). a :~: b
unsafeAxiom :: w :~: 1 of
  w :~: 1
Refl -> r
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 = (([Char], (SBVType, ([([CV], CV)], CV))) -> Model -> Model)
-> Model -> [([Char], (SBVType, ([([CV], CV)], CV)))] -> Model
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr ([Char], (SBVType, ([([CV], CV)], CV))) -> Model -> Model
gouifuncs ((([Char], CV) -> Model -> Model)
-> Model -> [([Char], CV)] -> Model
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr ([Char], CV) -> Model -> Model
goassoc Model
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) ->
        TypedSymbol t -> t -> Model -> Model
forall model symbolSet (typedSymbol :: * -> *) t.
ModelOps model symbolSet typedSymbol =>
typedSymbol t -> t -> model -> model
insertValue TypedSymbol t
s (TypeRep t -> CV -> t
forall a. TypeRep a -> CV -> a
resolveSingle TypeRep t
tr CV
cv) Model
m
      Maybe SomeTypedSymbol
Nothing -> [Char] -> Model
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 TypeRep a -> TypeRep Bool -> Maybe (a :~~: Bool)
forall k1 k2 (a :: k1) (b :: k2).
TypeRep a -> TypeRep b -> Maybe (a :~~: b)
R.eqTypeRep TypeRep a
t (forall a. Typeable a => TypeRep a
forall {k} (a :: k). Typeable a => TypeRep a
R.typeRep @Bool) of
        Just a :~~: Bool
R.HRefl -> Integer
n Integer -> Integer -> Bool
forall a. Eq a => a -> a -> Bool
/= Integer
0
        Maybe (a :~~: Bool)
Nothing -> [Char] -> a
forall a. HasCallStack => [Char] -> a
error [Char]
"Bad type"
    resolveSingle TypeRep a
t (SBVI.CV Kind
SBVI.KUnbounded (SBVI.CInteger Integer
i)) =
      case TypeRep a -> TypeRep Integer -> Maybe (a :~~: Integer)
forall k1 k2 (a :: k1) (b :: k2).
TypeRep a -> TypeRep b -> Maybe (a :~~: b)
R.eqTypeRep TypeRep a
t (forall a. Typeable a => TypeRep a
forall {k} (a :: k). Typeable a => TypeRep a
R.typeRep @Integer) of
        Just a :~~: Integer
R.HRefl -> a
Integer
i
        Maybe (a :~~: Integer)
Nothing -> [Char] -> a
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 TypeRep a -> TypeRep Integer -> Maybe (a :~~: Integer)
forall k1 k2 (a :: k1) (b :: k2).
TypeRep a -> TypeRep b -> Maybe (a :~~: b)
R.eqTypeRep TypeRep a
t (forall a. Typeable a => TypeRep a
forall {k} (a :: k). Typeable a => TypeRep a
R.typeRep @Integer) of
        Just a :~~: Integer
R.HRefl -> a
Integer
i
        Maybe (a :~~: Integer)
_ -> case TypeRep a
t of
          R.App TypeRep a
a (TypeRep b
n :: R.TypeRep w) ->
            case TypeRep k1 -> TypeRep Nat -> Maybe (k1 :~~: Nat)
forall k1 k2 (a :: k1) (b :: k2).
TypeRep a -> TypeRep b -> Maybe (a :~~: b)
R.eqTypeRep (TypeRep b -> TypeRep k1
forall k (a :: k). TypeRep a -> TypeRep k
R.typeRepKind TypeRep b
n) (forall a. Typeable a => TypeRep a
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 (((KnownNat b, 1 <= b) => a) -> a)
-> ((KnownNat b, 1 <= b) => a) -> a
forall a b. (a -> b) -> a -> b
$
                  case (TypeRep a -> TypeRep IntN -> Maybe (a :~~: 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
forall (a :: Nat -> *). Typeable a => TypeRep a
R.typeRep @IntN), TypeRep a -> TypeRep WordN -> Maybe (a :~~: WordN)
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
forall (a :: Nat -> *). Typeable a => TypeRep a
R.typeRep @WordN)) of
                    (Just a :~~: IntN
R.HRefl, Maybe (a :~~: WordN)
_) ->
                      Integer -> a
forall a. Num a => Integer -> a
fromInteger Integer
i
                    (Maybe (a :~~: IntN)
_, Just a :~~: WordN
R.HRefl) -> Integer -> a
forall a. Num a => Integer -> a
fromInteger Integer
i
                    (Maybe (a :~~: IntN), Maybe (a :~~: WordN))
_ -> [Char] -> a
forall a. HasCallStack => [Char] -> a
error [Char]
"Bad type"
              Maybe (k1 :~~: Nat)
_ -> [Char] -> a
forall a. HasCallStack => [Char] -> a
error [Char]
"Bad type"
          TypeRep a
_ -> [Char] -> a
forall a. HasCallStack => [Char] -> a
error [Char]
"Bad type"
    resolveSingle TypeRep a
_ CV
_ = [Char] -> a
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) -> [(a, a =-> b)] -> (a =-> b) -> a =-> (a =-> b)
forall a b. [(a, b)] -> b -> a =-> b
TabularFun [] ((a =-> b) -> a =-> (a =-> b)) -> (a =-> b) -> a =-> (a =-> b)
forall a b. (a -> b) -> a -> b
$ TypeRep a -> TypeRep b -> CV -> 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
_ -> [(a, r)] -> r -> a =-> r
forall a b. [(a, b)] -> b -> a =-> b
TabularFun [] (r -> a =-> r) -> r -> a =-> r
forall a b. (a -> b) -> a -> b
$ TypeRep r -> CV -> r
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) ->
          [(a, a =-> b)] -> (a =-> b) -> a =-> (a =-> b)
forall a b. [(a, b)] -> b -> a =-> b
TabularFun
            (([([CV], CV)] -> a =-> b) -> (a, [([CV], CV)]) -> (a, a =-> b)
forall (p :: * -> * -> *) b c a.
Bifunctor p =>
(b -> c) -> p a b -> p a c
second (\[([CV], CV)]
r -> TypeRep a -> TypeRep b -> ([([CV], CV)], CV) -> a =-> b
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)) ((a, [([CV], CV)]) -> (a, a =-> b))
-> [(a, [([CV], CV)])] -> [(a, a =-> b)]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> TypeRep a -> [([CV], CV)] -> [(a, [([CV], CV)])]
forall a. TypeRep a -> [([CV], CV)] -> [(a, [([CV], CV)])]
partition TypeRep a
ta1 [([CV], CV)]
l)
            (TypeRep a -> TypeRep b -> CV -> a =-> b
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
_ ->
          [(a, r)] -> r -> a =-> r
forall a b. [(a, b)] -> b -> a =-> b
TabularFun
            (([CV] -> a) -> (CV -> r) -> ([CV], CV) -> (a, r)
forall (p :: * -> * -> *) a b c d.
Bifunctor p =>
(a -> b) -> (c -> d) -> p a c -> p b d
bimap (TypeRep a -> CV -> a
forall a. TypeRep a -> CV -> a
resolveSingle TypeRep a
ta1 (CV -> a) -> ([CV] -> CV) -> [CV] -> a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [CV] -> CV
forall a. [a] -> a
head) (TypeRep r -> CV -> r
forall a. TypeRep a -> CV -> a
resolveSingle TypeRep r
ta2) (([CV], CV) -> (a, r)) -> [([CV], CV)] -> [(a, r)]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [([CV], CV)]
l)
            (TypeRep r -> CV -> r
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 = TypedSymbol a -> FunArg -> TypedSymbol a
forall t a.
(SupportedPrim t, Typeable a, Ord a, Lift a, NFData a, Show a,
 Hashable a) =>
TypedSymbol t -> a -> TypedSymbol t
WithInfo ([Char] -> Id -> TypedSymbol a
forall t. SupportedPrim t => [Char] -> Id -> TypedSymbol t
IndexedSymbol [Char]
"arg" Id
idx) FunArg
FunArg
              funs :: [(a, a --> b)]
funs = ([([CV], CV)] -> a --> b) -> (a, [([CV], CV)]) -> (a, a --> b)
forall (p :: * -> * -> *) b c a.
Bifunctor p =>
(b -> c) -> p a b -> p a c
second (\[([CV], CV)]
r -> Id -> TypeRep a -> TypeRep b -> ([([CV], CV)], CV) -> a --> b
forall a r.
(SupportedPrim a, SupportedPrim r) =>
Id -> TypeRep a -> TypeRep r -> ([([CV], CV)], CV) -> a --> r
gougfuncResolve (Id
idx Id -> Id -> Id
forall a. Num a => a -> a -> a
+ Id
1) TypeRep a
ta2' TypeRep b
tr2' ([([CV], CV)]
r, CV
s)) ((a, [([CV], CV)]) -> (a, a --> b))
-> [(a, [([CV], CV)])] -> [(a, a --> b)]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> TypeRep a -> [([CV], CV)] -> [(a, [([CV], CV)])]
forall a. TypeRep a -> [([CV], CV)] -> [(a, [([CV], CV)])]
partition TypeRep a
ta1 [([CV], CV)]
l
              def :: a --> b
def = Id -> TypeRep a -> TypeRep b -> ([([CV], CV)], CV) -> a --> b
forall a r.
(SupportedPrim a, SupportedPrim r) =>
Id -> TypeRep a -> TypeRep r -> ([([CV], CV)], CV) -> a --> r
gougfuncResolve (Id
idx Id -> Id -> Id
forall a. Num a => a -> a -> a
+ Id
1) TypeRep a
ta2' TypeRep b
tr2' ([], CV
s)
              body :: Term (a --> b)
body =
                (Term (a --> b) -> (a, a --> b) -> Term (a --> b))
-> Term (a --> b) -> [(a, a --> b)] -> Term (a --> b)
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl'
                  ( \Term (a --> b)
acc (a
v, a --> b
f) ->
                      Term Bool -> Term (a --> b) -> Term (a --> b) -> Term (a --> b)
forall a.
SupportedPrim a =>
Term Bool -> Term a -> Term a -> Term a
pevalITETerm
                        (Term a -> Term a -> Term Bool
forall a. SupportedPrim a => Term a -> Term a -> Term Bool
pevalEqvTerm ([Char] -> Id -> FunArg -> Term a
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) (a -> Term a
forall t.
(SupportedPrim t, Typeable t, Hashable t, Eq t, Show t) =>
t -> Term t
conTerm a
v))
                        ((a --> b) -> Term (a --> b)
forall t.
(SupportedPrim t, Typeable t, Hashable t, Eq t, Show t) =>
t -> Term t
conTerm a --> b
f)
                        Term (a --> b)
acc
                  )
                  ((a --> b) -> Term (a --> b)
forall t.
(SupportedPrim t, Typeable t, Hashable t, Eq t, Show t) =>
t -> Term t
conTerm a --> b
def)
                  [(a, a --> b)]
funs
           in TypedSymbol a -> Term (a --> b) -> a --> (a --> b)
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 = TypedSymbol a -> FunArg -> TypedSymbol a
forall t a.
(SupportedPrim t, Typeable a, Ord a, Lift a, NFData a, Show a,
 Hashable a) =>
TypedSymbol t -> a -> TypedSymbol t
WithInfo ([Char] -> Id -> TypedSymbol a
forall t. SupportedPrim t => [Char] -> Id -> TypedSymbol t
IndexedSymbol [Char]
"arg" Id
idx) FunArg
FunArg
              vs :: [(a, r)]
vs = ([CV] -> a) -> (CV -> r) -> ([CV], CV) -> (a, r)
forall (p :: * -> * -> *) a b c d.
Bifunctor p =>
(a -> b) -> (c -> d) -> p a c -> p b d
bimap (TypeRep a -> CV -> a
forall a. TypeRep a -> CV -> a
resolveSingle TypeRep a
ta1 (CV -> a) -> ([CV] -> CV) -> [CV] -> a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [CV] -> CV
forall a. [a] -> a
head) (TypeRep r -> CV -> r
forall a. TypeRep a -> CV -> a
resolveSingle TypeRep r
ta2) (([CV], CV) -> (a, r)) -> [([CV], CV)] -> [(a, r)]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [([CV], CV)]
l
              def :: r
def = TypeRep r -> CV -> r
forall a. TypeRep a -> CV -> a
resolveSingle TypeRep r
ta2 CV
s
              body :: Term r
body =
                (Term r -> (a, r) -> Term r) -> Term r -> [(a, r)] -> Term r
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl'
                  ( \Term r
acc (a
v, r
a) ->
                      Term Bool -> Term r -> Term r -> Term r
forall a.
SupportedPrim a =>
Term Bool -> Term a -> Term a -> Term a
pevalITETerm
                        (Term a -> Term a -> Term Bool
forall a. SupportedPrim a => Term a -> Term a -> Term Bool
pevalEqvTerm ([Char] -> Id -> FunArg -> Term a
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) (a -> Term a
forall t.
(SupportedPrim t, Typeable t, Hashable t, Eq t, Show t) =>
t -> Term t
conTerm a
v))
                        (r -> Term r
forall t.
(SupportedPrim t, Typeable t, Hashable t, Eq t, Show t) =>
t -> Term t
conTerm r
a)
                        Term r
acc
                  )
                  (r -> Term r
forall t.
(SupportedPrim t, Typeable t, Hashable t, Eq t, Show t) =>
t -> Term t
conTerm r
def)
                  [(a, r)]
vs
           in TypedSymbol a -> Term r -> a --> r
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 (TypeRep a -> TypeRep Bool -> Maybe (a :~~: Bool)
forall k1 k2 (a :: k1) (b :: k2).
TypeRep a -> TypeRep b -> Maybe (a :~~: b)
R.eqTypeRep TypeRep a
t (forall a. Typeable a => TypeRep a
forall {k} (a :: k). Typeable a => TypeRep a
R.typeRep @Bool), TypeRep a -> TypeRep Integer -> Maybe (a :~~: Integer)
forall k1 k2 (a :: k1) (b :: k2).
TypeRep a -> TypeRep b -> Maybe (a :~~: b)
R.eqTypeRep TypeRep a
t (forall a. Typeable a => TypeRep a
forall {k} (a :: k). Typeable a => TypeRep a
R.typeRep @Integer)) of
      (Just a :~~: Bool
R.HRefl, Maybe (a :~~: Integer)
_) -> [(a, [([CV], CV)])] -> [(a, [([CV], CV)])]
forall a. Ord a => [(a, [([CV], CV)])] -> [(a, [([CV], CV)])]
partitionWithOrd ([(a, [([CV], CV)])] -> [(a, [([CV], CV)])])
-> ([([CV], CV)] -> [(a, [([CV], CV)])])
-> [([CV], CV)]
-> [(a, [([CV], CV)])]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. TypeRep a -> [([CV], CV)] -> [(a, [([CV], CV)])]
forall a. TypeRep a -> [([CV], CV)] -> [(a, [([CV], CV)])]
resolveFirst TypeRep a
t
      (Maybe (a :~~: Bool)
_, Just a :~~: Integer
R.HRefl) -> [(a, [([CV], CV)])] -> [(a, [([CV], CV)])]
forall a. Ord a => [(a, [([CV], CV)])] -> [(a, [([CV], CV)])]
partitionWithOrd ([(a, [([CV], CV)])] -> [(a, [([CV], CV)])])
-> ([([CV], CV)] -> [(a, [([CV], CV)])])
-> [([CV], CV)]
-> [(a, [([CV], CV)])]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. TypeRep a -> [([CV], CV)] -> [(a, [([CV], CV)])]
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 (TypeRep a -> TypeRep IntN -> Maybe (a :~~: 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
forall (a :: Nat -> *). Typeable a => TypeRep a
R.typeRep @IntN), TypeRep a -> TypeRep WordN -> Maybe (a :~~: WordN)
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
forall (a :: Nat -> *). Typeable a => TypeRep a
R.typeRep @WordN)) of
          (Just a :~~: IntN
R.HRefl, Maybe (a :~~: WordN)
_) -> ((Integer, [([CV], CV)]) -> (IntN b, [([CV], CV)]))
-> [(Integer, [([CV], CV)])] -> [(IntN b, [([CV], CV)])]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap ((Integer -> IntN b)
-> (Integer, [([CV], CV)]) -> (IntN b, [([CV], CV)])
forall (p :: * -> * -> *) a b c.
Bifunctor p =>
(a -> b) -> p a c -> p b c
first Integer -> IntN b
forall (n :: Nat). Integer -> IntN n
IntN) ([(Integer, [([CV], CV)])] -> [(IntN b, [([CV], CV)])])
-> ([([CV], CV)] -> [(Integer, [([CV], CV)])])
-> [([CV], CV)]
-> [(IntN b, [([CV], CV)])]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [(Integer, [([CV], CV)])] -> [(Integer, [([CV], CV)])]
forall a. Ord a => [(a, [([CV], CV)])] -> [(a, [([CV], CV)])]
partitionWithOrd ([(Integer, [([CV], CV)])] -> [(Integer, [([CV], CV)])])
-> ([([CV], CV)] -> [(Integer, [([CV], CV)])])
-> [([CV], CV)]
-> [(Integer, [([CV], CV)])]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ((IntN b, [([CV], CV)]) -> (Integer, [([CV], CV)]))
-> [(IntN b, [([CV], CV)])] -> [(Integer, [([CV], CV)])]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap ((IntN b -> Integer)
-> (IntN b, [([CV], CV)]) -> (Integer, [([CV], CV)])
forall (p :: * -> * -> *) a b c.
Bifunctor p =>
(a -> b) -> p a c -> p b c
first IntN b -> Integer
forall (n :: Nat). IntN n -> Integer
unIntN) ([(IntN b, [([CV], CV)])] -> [(Integer, [([CV], CV)])])
-> ([([CV], CV)] -> [(IntN b, [([CV], CV)])])
-> [([CV], CV)]
-> [(Integer, [([CV], CV)])]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. TypeRep a -> [([CV], CV)] -> [(a, [([CV], CV)])]
forall a. TypeRep a -> [([CV], CV)] -> [(a, [([CV], CV)])]
resolveFirst TypeRep a
t
          (Maybe (a :~~: IntN)
_, Just a :~~: WordN
R.HRefl) -> [(a, [([CV], CV)])] -> [(a, [([CV], CV)])]
forall a. Ord a => [(a, [([CV], CV)])] -> [(a, [([CV], CV)])]
partitionWithOrd ([(a, [([CV], CV)])] -> [(a, [([CV], CV)])])
-> ([([CV], CV)] -> [(a, [([CV], CV)])])
-> [([CV], CV)]
-> [(a, [([CV], CV)])]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. TypeRep a -> [([CV], CV)] -> [(a, [([CV], CV)])]
forall a. TypeRep a -> [([CV], CV)] -> [(a, [([CV], CV)])]
resolveFirst TypeRep a
t
          (Maybe (a :~~: IntN), Maybe (a :~~: WordN))
_ -> [Char] -> [([CV], CV)] -> [(a, [([CV], CV)])]
forall a. HasCallStack => [Char] -> a
error [Char]
"Unknown type"
        TypeRep a
_ -> [Char] -> [([CV], CV)] -> [(a, [([CV], CV)])]
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 = (([CV], CV) -> (a, [([CV], CV)]))
-> [([CV], CV)] -> [(a, [([CV], CV)])]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (\case (CV
x : [CV]
xs, CV
v) -> (TypeRep a -> CV -> a
forall a. TypeRep a -> CV -> a
resolveSingle TypeRep a
tf CV
x, [([CV]
xs, CV
v)]); ([CV], CV)
_ -> [Char] -> (a, [([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 = [(a, [([CV], CV)])] -> [(a, [([CV], CV)])]
forall {a} {a}. Eq a => [(a, [a])] -> [(a, [a])]
go [(a, [([CV], CV)])]
sorted
      where
        sorted :: [(a, [([CV], CV)])]
sorted = ((a, [([CV], CV)]) -> a)
-> [(a, [([CV], CV)])] -> [(a, [([CV], CV)])]
forall b a. Ord b => (a -> b) -> [a] -> [a]
sortWith (a, [([CV], CV)]) -> a
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 (a, [a]) -> a
forall a b. (a, b) -> a
fst (a, [a])
x a -> a -> Bool
forall a. Eq a => a -> a -> Bool
== (a, [a]) -> a
forall a b. (a, b) -> a
fst (a, [a])
x1
            then [(a, [a])] -> [(a, [a])]
go ([(a, [a])] -> [(a, [a])]) -> [(a, [a])] -> [(a, [a])]
forall a b. (a -> b) -> a -> b
$ ((a, [a]) -> a
forall a b. (a, b) -> a
fst (a, [a])
x, (a, [a]) -> [a]
forall a b. (a, b) -> b
snd (a, [a])
x [a] -> [a] -> [a]
forall a. [a] -> [a] -> [a]
++ (a, [a]) -> [a]
forall a b. (a, b) -> b
snd (a, [a])
x1) (a, [a]) -> [(a, [a])] -> [(a, [a])]
forall a. a -> [a] -> [a]
: [(a, [a])]
xs
            else (a, [a])
x (a, [a]) -> [(a, [a])] -> [(a, [a])]
forall a. a -> [a] -> [a]
: [(a, [a])] -> [(a, [a])]
go ((a, [a])
x1 (a, [a]) -> [(a, [a])] -> [(a, [a])]
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) -> TypedSymbol t -> (SupportedPrim t => Model) -> Model
forall t a. TypedSymbol t -> (SupportedPrim t => a) -> a
withSymbolSupported TypedSymbol t
s ((SupportedPrim t => Model) -> Model)
-> (SupportedPrim t => Model) -> Model
forall a b. (a -> b) -> a -> b
$ case TypeRep t
tr of
        t :: TypeRep t
t@(TFunType TypeRep a
a TypeRep b
r) -> TypeRep t -> (Typeable t => Model) -> Model
forall k (a :: k) r. TypeRep a -> (Typeable a => r) -> r
R.withTypeable TypeRep t
t ((Typeable t => Model) -> Model) -> (Typeable t => Model) -> Model
forall a b. (a -> b) -> a -> b
$ TypedSymbol t -> t -> Model -> Model
forall model symbolSet (typedSymbol :: * -> *) t.
ModelOps model symbolSet typedSymbol =>
typedSymbol t -> t -> model -> model
insertValue TypedSymbol t
s (TypeRep a -> TypeRep b -> ([([CV], CV)], CV) -> a =-> b
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) -> TypeRep t -> (Typeable t => Model) -> Model
forall k (a :: k) r. TypeRep a -> (Typeable a => r) -> r
R.withTypeable TypeRep t
t ((Typeable t => Model) -> Model) -> (Typeable t => Model) -> Model
forall a b. (a -> b) -> a -> b
$ TypedSymbol t -> t -> Model -> Model
forall model symbolSet (typedSymbol :: * -> *) t.
ModelOps model symbolSet typedSymbol =>
typedSymbol t -> t -> model -> model
insertValue TypedSymbol t
s (Id -> TypeRep a -> TypeRep b -> ([([CV], CV)], CV) -> a --> b
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
_ -> [Char] -> Model
forall a. HasCallStack => [Char] -> a
error [Char]
"Bad"
      Maybe SomeTypedSymbol
Nothing -> [Char] -> Model
forall a. HasCallStack => [Char] -> a
error [Char]
"Bad"

-- helpers

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 (TypeRep a -> TypeRep IntN -> Maybe (a :~~: IntN)
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
forall (a :: Nat -> *). Typeable a => TypeRep a
R.typeRep @IntN), TypeRep k1 -> TypeRep Nat -> Maybe (k1 :~~: Nat)
forall k1 k2 (a :: k1) (b :: k2).
TypeRep a -> TypeRep b -> Maybe (a :~~: b)
R.eqTypeRep (TypeRep b -> TypeRep k1
forall k (a :: k). TypeRep a -> TypeRep k
R.typeRepKind TypeRep b
n) (forall a. Typeable a => TypeRep a
forall {k} (a :: k). Typeable a => TypeRep a
R.typeRep @Nat)) of
      (Just a :~~: IntN
R.HRefl, Just k1 :~~: Nat
R.HRefl) ->
        BVTypeContainer IntN t -> Maybe (BVTypeContainer IntN t)
forall a. a -> Maybe a
Just (BVTypeContainer IntN t -> Maybe (BVTypeContainer IntN t))
-> BVTypeContainer IntN t -> Maybe (BVTypeContainer IntN t)
forall a b. (a -> b) -> a -> b
$ forall (w :: Nat) r. (BVIsNonZero w => r) -> r
unsafeBVIsNonZero @w ((BVIsNonZero b => BVTypeContainer IntN t)
 -> BVTypeContainer IntN t)
-> (BVIsNonZero b => BVTypeContainer IntN t)
-> BVTypeContainer IntN t
forall a b. (a -> b) -> a -> b
$ Proxy t
-> (PrimConstraint t => BVTypeContainer IntN t)
-> BVTypeContainer IntN t
forall t (proxy :: * -> *) a.
SupportedPrim t =>
proxy t -> (PrimConstraint t => a) -> a
withPrim (forall {t}. Proxy t
forall {k} (t :: k). Proxy t
Proxy @t) (Proxy b -> BVTypeContainer IntN (IntN b)
forall {k} (s' :: Nat) (k :: k) (bv :: Nat -> k).
(BVIsNonZero s', KnownNat s', 1 <= s', k ~ bv s') =>
Proxy s' -> BVTypeContainer bv k
BVTypeContainer Proxy b
forall {k} (t :: k). Proxy t
Proxy)
      (Maybe (a :~~: IntN), Maybe (k1 :~~: Nat))
_ -> Maybe (BVTypeContainer IntN t)
forall a. Maybe a
Nothing
  TypeRep t
_ -> Maybe (BVTypeContainer IntN 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 w :~: 1
forall {k} (a :: k) (b :: k). a :~: b
unsafeAxiom :: w :~: 1 of
      w :~: 1
Refl -> r
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)
-> (Void# -> 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 (TypeRep a -> TypeRep WordN -> Maybe (a :~~: WordN)
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
forall (a :: Nat -> *). Typeable a => TypeRep a
R.typeRep @WordN), TypeRep k1 -> TypeRep Nat -> Maybe (k1 :~~: Nat)
forall k1 k2 (a :: k1) (b :: k2).
TypeRep a -> TypeRep b -> Maybe (a :~~: b)
R.eqTypeRep (TypeRep b -> TypeRep k1
forall k (a :: k). TypeRep a -> TypeRep k
R.typeRepKind TypeRep b
n) (forall a. Typeable a => TypeRep a
forall {k} (a :: k). Typeable a => TypeRep a
R.typeRep @Nat)) of
      (Just a :~~: WordN
R.HRefl, Just k1 :~~: Nat
R.HRefl) ->
        BVTypeContainer WordN t -> Maybe (BVTypeContainer WordN t)
forall a. a -> Maybe a
Just (BVTypeContainer WordN t -> Maybe (BVTypeContainer WordN t))
-> BVTypeContainer WordN t -> Maybe (BVTypeContainer WordN t)
forall a b. (a -> b) -> a -> b
$ forall (w :: Nat) r. (BVIsNonZero w => r) -> r
unsafeBVIsNonZero @w ((BVIsNonZero b => BVTypeContainer WordN t)
 -> BVTypeContainer WordN t)
-> (BVIsNonZero b => BVTypeContainer WordN t)
-> BVTypeContainer WordN t
forall a b. (a -> b) -> a -> b
$ Proxy t
-> (PrimConstraint t => BVTypeContainer WordN t)
-> BVTypeContainer WordN t
forall t (proxy :: * -> *) a.
SupportedPrim t =>
proxy t -> (PrimConstraint t => a) -> a
withPrim (forall {t}. Proxy t
forall {k} (t :: k). Proxy t
Proxy @t) (Proxy b -> BVTypeContainer WordN (WordN b)
forall {k} (s' :: Nat) (k :: k) (bv :: Nat -> k).
(BVIsNonZero s', KnownNat s', 1 <= s', k ~ bv s') =>
Proxy s' -> BVTypeContainer bv k
BVTypeContainer Proxy b
forall {k} (t :: k). Proxy t
Proxy)
      (Maybe (a :~~: WordN), Maybe (k1 :~~: Nat))
_ -> Maybe (BVTypeContainer WordN t)
forall a. Maybe a
Nothing
  TypeRep t
_ -> Maybe (BVTypeContainer WordN 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 w :~: 1
forall {k} (a :: k) (b :: k). a :~: b
unsafeAxiom :: w :~: 1 of
      w :~: 1
Refl -> r
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)
-> (Void# -> 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 TypeRep a -> TypeRep (=->) -> Maybe (a :~~: (=->))
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
forall (a :: * -> * -> *). Typeable a => TypeRep a
R.typeRep @(=->)) of
      Just a :~~: (=->)
R.HRefl -> TFunTypeContainer t -> Maybe (TFunTypeContainer t)
forall a. a -> Maybe a
Just (TFunTypeContainer t -> Maybe (TFunTypeContainer t))
-> TFunTypeContainer t -> Maybe (TFunTypeContainer t)
forall a b. (a -> b) -> a -> b
$ Proxy t
-> (PrimConstraint t => TFunTypeContainer t) -> TFunTypeContainer t
forall t (proxy :: * -> *) a.
SupportedPrim t =>
proxy t -> (PrimConstraint t => a) -> a
withPrim (forall {t}. Proxy t
forall {k} (t :: k). Proxy t
Proxy @t) ((PrimConstraint t => TFunTypeContainer t) -> TFunTypeContainer t)
-> (PrimConstraint t => TFunTypeContainer t) -> TFunTypeContainer t
forall a b. (a -> b) -> a -> b
$ TypeRep b -> TypeRep b -> TFunTypeContainer (b =-> b)
forall s' b.
(SupportedPrim s', SupportedPrim b) =>
TypeRep s' -> TypeRep b -> TFunTypeContainer (s' =-> b)
TFunTypeContainer TypeRep b
TypeRep b
ta2' TypeRep b
TypeRep b
tr2'
      Maybe (a :~~: (=->))
Nothing -> Maybe (TFunTypeContainer t)
forall a. Maybe a
Nothing
  TypeRep t
_ -> Maybe (TFunTypeContainer 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)
-> (Void# -> r)
-> r
TFunType a b <-
  (tFunTypeView -> Just (TFunTypeContainer a b))
  where
    TFunType TypeRep a
a TypeRep b
b = TypeRep ((=->) a) -> TypeRep b -> TypeRep t
forall k2 (t :: k2) k1 (a :: k1 -> k2) (b :: k1).
(t ~ a b) =>
TypeRep a -> TypeRep b -> TypeRep t
R.App (TypeRep (=->) -> TypeRep a -> TypeRep ((=->) a)
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
forall (a :: * -> * -> *). 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)
-> (Void# -> 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 TypeRep a -> TypeRep (-->) -> Maybe (a :~~: (-->))
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
forall (a :: * -> * -> *). Typeable a => TypeRep a
R.typeRep @(-->)) of
      Just a :~~: (-->)
R.HRefl -> GFunTypeContainer t -> Maybe (GFunTypeContainer t)
forall a. a -> Maybe a
Just (GFunTypeContainer t -> Maybe (GFunTypeContainer t))
-> GFunTypeContainer t -> Maybe (GFunTypeContainer t)
forall a b. (a -> b) -> a -> b
$ Proxy t
-> (PrimConstraint t => GFunTypeContainer t) -> GFunTypeContainer t
forall t (proxy :: * -> *) a.
SupportedPrim t =>
proxy t -> (PrimConstraint t => a) -> a
withPrim (forall {t}. Proxy t
forall {k} (t :: k). Proxy t
Proxy @t) ((PrimConstraint t => GFunTypeContainer t) -> GFunTypeContainer t)
-> (PrimConstraint t => GFunTypeContainer t) -> GFunTypeContainer t
forall a b. (a -> b) -> a -> b
$ TypeRep b -> TypeRep b -> GFunTypeContainer (b --> b)
forall s' b.
(SupportedPrim s', SupportedPrim b) =>
TypeRep s' -> TypeRep b -> GFunTypeContainer (s' --> b)
GFunTypeContainer TypeRep b
TypeRep b
ta2' TypeRep b
TypeRep b
tr2'
      Maybe (a :~~: (-->))
Nothing -> Maybe (GFunTypeContainer t)
forall a. Maybe a
Nothing
  TypeRep t
_ -> Maybe (GFunTypeContainer 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)
-> (Void# -> r)
-> r
GFunType a b <-
  (gFunTypeView -> Just (GFunTypeContainer a b))
  where
    GFunType TypeRep a
a TypeRep b
b = TypeRep ((-->) a) -> TypeRep b -> TypeRep t
forall k2 (t :: k2) k1 (a :: k1 -> k2) (b :: k1).
(t ~ a b) =>
TypeRep a -> TypeRep b -> TypeRep t
R.App (TypeRep (-->) -> TypeRep a -> TypeRep ((-->) a)
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
forall (a :: * -> * -> *). 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)
-> (Void# -> 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) -> (Void# -> 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) -> (Void# -> 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 -> SMTConfig -> DictConfig integerBitWidth
forall s' (integerBitWidth :: Nat).
ConfigConstraint integerBitWidth s' =>
SMTConfig -> DictConfig integerBitWidth
DictConfig SMTConfig
c
  BoundedReasoning SMTConfig
c -> SMTConfig -> DictConfig integerBitWidth
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)
-> (Void# -> 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)

-- has to declare this because GHC does not support impredicative polymorphism
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 -> DictSimpleType integerBitWidth s
-> Maybe (DictSimpleType integerBitWidth s)
forall a. a -> Maybe a
Just DictSimpleType integerBitWidth s
forall (integerBitWidth :: Nat) s s'.
SimpleTypeConstraint integerBitWidth s s' =>
DictSimpleType integerBitWidth s
DictSimpleType
  TypeRep s
IntegerType -> DictSimpleType integerBitWidth s
-> Maybe (DictSimpleType integerBitWidth s)
forall a. a -> Maybe a
Just DictSimpleType integerBitWidth s
forall (integerBitWidth :: Nat) s s'.
SimpleTypeConstraint integerBitWidth s s' =>
DictSimpleType integerBitWidth s
DictSimpleType
  SignedBVType Proxy n
_ -> DictSimpleType integerBitWidth s
-> Maybe (DictSimpleType integerBitWidth s)
forall a. a -> Maybe a
Just DictSimpleType integerBitWidth s
forall (integerBitWidth :: Nat) s s'.
SimpleTypeConstraint integerBitWidth s s' =>
DictSimpleType integerBitWidth s
DictSimpleType
  UnsignedBVType Proxy n
_ -> DictSimpleType integerBitWidth s
-> Maybe (DictSimpleType integerBitWidth s)
forall a. a -> Maybe a
Just DictSimpleType integerBitWidth s
forall (integerBitWidth :: Nat) s s'.
SimpleTypeConstraint integerBitWidth s s' =>
DictSimpleType integerBitWidth s
DictSimpleType
  TypeRep s
_ -> Maybe (DictSimpleType integerBitWidth s)
forall a. Maybe a
Nothing
resolveSimpleTypeView (GrisetteSMTConfig integerBitWidth, TypeRep s)
_ = [Char] -> Maybe (DictSimpleType integerBitWidth 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)
-> (Void# -> 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 -> DictDeepType integerBitWidth s
-> Maybe (DictDeepType integerBitWidth s)
forall a. a -> Maybe a
Just DictDeepType integerBitWidth s
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 ((GrisetteSMTConfig integerBitWidth, TypeRep a)
-> Maybe (DictDeepType integerBitWidth a)
TypeResolver DictDeepType
resolveDeepTypeView (GrisetteSMTConfig integerBitWidth
config, TypeRep a
ta), (GrisetteSMTConfig integerBitWidth, TypeRep b)
-> Maybe (DictDeepType integerBitWidth b)
TypeResolver DictDeepType
resolveDeepTypeView (GrisetteSMTConfig integerBitWidth
config, TypeRep b
tb)) of
      (Just DictDeepType integerBitWidth a
DictDeepType, Just DictDeepType integerBitWidth b
DictDeepType) -> DictDeepType integerBitWidth s
-> Maybe (DictDeepType integerBitWidth s)
forall a. a -> Maybe a
Just DictDeepType integerBitWidth s
forall (integerBitWidth :: Nat) s s'.
DeepTypeConstraint integerBitWidth s s' =>
DictDeepType integerBitWidth s
DictDeepType
      (Maybe (DictDeepType integerBitWidth a),
 Maybe (DictDeepType integerBitWidth b))
_ -> Maybe (DictDeepType integerBitWidth s)
forall a. Maybe a
Nothing
  (GrisetteSMTConfig integerBitWidth
config, GFunType (TypeRep a
ta :: R.TypeRep a) (TypeRep b
tb :: R.TypeRep b)) ->
    case ((GrisetteSMTConfig integerBitWidth, TypeRep a)
-> Maybe (DictDeepType integerBitWidth a)
TypeResolver DictDeepType
resolveDeepTypeView (GrisetteSMTConfig integerBitWidth
config, TypeRep a
ta), (GrisetteSMTConfig integerBitWidth, TypeRep b)
-> Maybe (DictDeepType integerBitWidth b)
TypeResolver DictDeepType
resolveDeepTypeView (GrisetteSMTConfig integerBitWidth
config, TypeRep b
tb)) of
      (Just DictDeepType integerBitWidth a
DictDeepType, Just DictDeepType integerBitWidth b
DictDeepType) -> DictDeepType integerBitWidth s
-> Maybe (DictDeepType integerBitWidth s)
forall a. a -> Maybe a
Just DictDeepType integerBitWidth s
forall (integerBitWidth :: Nat) s s'.
DeepTypeConstraint integerBitWidth s s' =>
DictDeepType integerBitWidth s
DictDeepType
      (Maybe (DictDeepType integerBitWidth a),
 Maybe (DictDeepType integerBitWidth b))
_ -> Maybe (DictDeepType integerBitWidth s)
forall a. Maybe a
Nothing
  (GrisetteSMTConfig integerBitWidth, TypeRep s)
_ -> Maybe (DictDeepType integerBitWidth 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)
-> (Void# -> 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 -> DictNumType integerBitWidth s
-> Maybe (DictNumType integerBitWidth s)
forall a. a -> Maybe a
Just DictNumType integerBitWidth s
forall (integerBitWidth :: Nat) s s'.
NumTypeConstraint integerBitWidth s s' =>
DictNumType integerBitWidth s
DictNumType
  SignedBVType Proxy n
_ -> DictNumType integerBitWidth s
-> Maybe (DictNumType integerBitWidth s)
forall a. a -> Maybe a
Just DictNumType integerBitWidth s
forall (integerBitWidth :: Nat) s s'.
NumTypeConstraint integerBitWidth s s' =>
DictNumType integerBitWidth s
DictNumType
  UnsignedBVType Proxy n
_ -> DictNumType integerBitWidth s
-> Maybe (DictNumType integerBitWidth s)
forall a. a -> Maybe a
Just DictNumType integerBitWidth s
forall (integerBitWidth :: Nat) s s'.
NumTypeConstraint integerBitWidth s s' =>
DictNumType integerBitWidth s
DictNumType
  TypeRep s
_ -> Maybe (DictNumType integerBitWidth s)
forall a. Maybe a
Nothing
resolveNumTypeView (GrisetteSMTConfig integerBitWidth, TypeRep s)
_ = [Char] -> Maybe (DictNumType integerBitWidth 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)
-> (Void# -> 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 -> DictNumOrdType integerBitWidth s
-> Maybe (DictNumOrdType integerBitWidth s)
forall a. a -> Maybe a
Just DictNumOrdType integerBitWidth s
forall (integerBitWidth :: Nat) s s'.
NumOrdTypeConstraint integerBitWidth s s' =>
DictNumOrdType integerBitWidth s
DictNumOrdType
  SignedBVType Proxy n
_ -> DictNumOrdType integerBitWidth s
-> Maybe (DictNumOrdType integerBitWidth s)
forall a. a -> Maybe a
Just DictNumOrdType integerBitWidth s
forall (integerBitWidth :: Nat) s s'.
NumOrdTypeConstraint integerBitWidth s s' =>
DictNumOrdType integerBitWidth s
DictNumOrdType
  UnsignedBVType Proxy n
_ -> DictNumOrdType integerBitWidth s
-> Maybe (DictNumOrdType integerBitWidth s)
forall a. a -> Maybe a
Just DictNumOrdType integerBitWidth s
forall (integerBitWidth :: Nat) s s'.
NumOrdTypeConstraint integerBitWidth s s' =>
DictNumOrdType integerBitWidth s
DictNumOrdType
  TypeRep s
_ -> Maybe (DictNumOrdType integerBitWidth s)
forall a. Maybe a
Nothing
resolveNumOrdTypeView (GrisetteSMTConfig integerBitWidth, TypeRep s)
_ = [Char] -> Maybe (DictNumOrdType integerBitWidth 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)
-> (Void# -> 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
_ -> DictBitsType integerBitWidth s
-> Maybe (DictBitsType integerBitWidth s)
forall a. a -> Maybe a
Just DictBitsType integerBitWidth s
forall (integerBitWidth :: Nat) s s'.
BitsTypeConstraint integerBitWidth s s' =>
DictBitsType integerBitWidth s
DictBitsType
  UnsignedBVType Proxy n
_ -> DictBitsType integerBitWidth s
-> Maybe (DictBitsType integerBitWidth s)
forall a. a -> Maybe a
Just DictBitsType integerBitWidth s
forall (integerBitWidth :: Nat) s s'.
BitsTypeConstraint integerBitWidth s s' =>
DictBitsType integerBitWidth s
DictBitsType
  TypeRep s
_ -> Maybe (DictBitsType integerBitWidth s)
forall a. Maybe a
Nothing
resolveBitsTypeView (GrisetteSMTConfig integerBitWidth, TypeRep s)
_ = [Char] -> Maybe (DictBitsType integerBitWidth 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)
-> (Void# -> r)
-> r
ResolvedBitsType <- (resolveBitsTypeView -> Just DictBitsType)