{-# LANGUAGE CPP #-}
{-# LANGUAGE ConstraintKinds #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE DeriveGeneric #-}
{-# LANGUAGE DeriveLift #-}
{-# LANGUAGE DerivingVia #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE GeneralizedNewtypeDeriving #-}
{-# LANGUAGE InstanceSigs #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE PatternSynonyms #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE StandaloneDeriving #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE UndecidableInstances #-}

-- |
-- Module      :   Grisette.IR.SymPrim.Data.SymPrim
-- 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.IR.SymPrim.Data.SymPrim
  ( SymBool (..),
    SymInteger (..),
    SymWordN (..),
    SymIntN (..),
    SomeSymWordN (..),
    SomeSymIntN (..),
    type (=~>) (..),
    type (-~>) (..),
    (-->),
    ModelSymPair (..),
    symSize,
    symsSize,
    SomeSym (..),
    AllSyms (..),
    allSymsSize,
    unarySomeSymIntN,
    unarySomeSymIntNR1,
    binSomeSymIntN,
    binSomeSymIntNR1,
    binSomeSymIntNR2,
    unarySomeSymWordN,
    unarySomeSymWordNR1,
    binSomeSymWordN,
    binSomeSymWordNR1,
    binSomeSymWordNR2,
  )
where

import Control.DeepSeq (NFData (rnf))
import Control.Monad.Except (ExceptT (ExceptT))
import Control.Monad.Identity
  ( Identity (Identity),
    IdentityT (IdentityT),
  )
import Control.Monad.Trans.Maybe (MaybeT (MaybeT))
import qualified Control.Monad.Writer.Lazy as WriterLazy
import qualified Control.Monad.Writer.Strict as WriterStrict
import Data.Bits
  ( Bits
      ( bit,
        bitSize,
        bitSizeMaybe,
        clearBit,
        complement,
        complementBit,
        isSigned,
        popCount,
        rotate,
        rotateL,
        rotateR,
        setBit,
        shift,
        shiftL,
        shiftR,
        testBit,
        unsafeShiftL,
        unsafeShiftR,
        xor,
        zeroBits,
        (.&.),
        (.|.)
      ),
    FiniteBits (finiteBitSize),
  )
import qualified Data.ByteString as B
import Data.Functor.Sum (Sum)
import Data.Hashable (Hashable (hashWithSalt))
import Data.Int (Int16, Int32, Int64, Int8)
import Data.Proxy (Proxy (Proxy))
import Data.String (IsString (fromString))
import qualified Data.Text as T
import Data.Typeable (typeRep, type (:~:) (Refl))
import Data.Word (Word16, Word32, Word64, Word8)
import GHC.Generics
  ( Generic (Rep, from),
    K1 (K1),
    M1 (M1),
    U1,
    type (:*:) ((:*:)),
    type (:+:) (L1, R1),
  )
import GHC.TypeNats
  ( KnownNat,
    Nat,
    natVal,
    sameNat,
    type (+),
    type (<=),
  )
import Generics.Deriving (Default (Default, unDefault))
import Grisette.Core.Control.Exception
  ( AssertionError,
    VerificationConditions,
  )
import Grisette.Core.Data.BV
  ( IntN,
    WordN,
  )
import Grisette.Core.Data.Class.BitVector
  ( BV (bvConcat, bvExt, bvSelect, bvSext, bvZext),
    SizedBV (sizedBVConcat, sizedBVExt, sizedBVSelect, sizedBVSext, sizedBVZext),
  )
import Grisette.Core.Data.Class.Function (Apply (FunType, apply), Function (Arg, Ret, (#)))
import Grisette.Core.Data.Class.ModelOps
  ( ModelOps (emptyModel, insertValue),
    ModelRep (buildModel),
  )
import Grisette.Core.Data.Class.SignConversion (SignConversion (toSigned, toUnsigned))
import Grisette.Core.Data.Class.Solvable
  ( Solvable (con, conView, iinfosym, isym, sinfosym, ssym),
    pattern Con,
  )
import Grisette.Core.Data.Class.SymRotate (SymRotate (symRotate))
import Grisette.Core.Data.Class.SymShift (SymShift (symShift))
import Grisette.IR.SymPrim.Data.Prim.InternedTerm.InternedCtors (conTerm, iinfosymTerm, isymTerm, sinfosymTerm, ssymTerm, symTerm)
import Grisette.IR.SymPrim.Data.Prim.InternedTerm.SomeTerm
  ( SomeTerm (SomeTerm),
  )
import Grisette.IR.SymPrim.Data.Prim.InternedTerm.Term
  ( ConRep (ConType),
    LinkedRep (underlyingTerm, wrapTerm),
    SupportedPrim,
    SymRep (SymType),
    Term (ConTerm, SymTerm),
    TypedSymbol (WithInfo),
    type (-->) (GeneralFun),
  )
import Grisette.IR.SymPrim.Data.Prim.InternedTerm.TermSubstitution
  ( substTerm,
  )
import Grisette.IR.SymPrim.Data.Prim.InternedTerm.TermUtils
  ( pformat,
    someTermsSize,
    termSize,
    termsSize,
  )
import Grisette.IR.SymPrim.Data.Prim.Model
  ( Model,
  )
import Grisette.IR.SymPrim.Data.Prim.PartialEval.BV
  ( pevalBVConcatTerm,
    pevalBVExtendTerm,
    pevalBVSelectTerm,
    pevalToSignedTerm,
    pevalToUnsignedTerm,
  )
import Grisette.IR.SymPrim.Data.Prim.PartialEval.Bits
  ( pevalAndBitsTerm,
    pevalComplementBitsTerm,
    pevalOrBitsTerm,
    pevalRotateLeftTerm,
    pevalRotateRightTerm,
    pevalShiftLeftTerm,
    pevalShiftRightTerm,
    pevalXorBitsTerm,
  )
import Grisette.IR.SymPrim.Data.Prim.PartialEval.Bool
  ( pevalEqvTerm,
    pevalITETerm,
    pevalOrTerm,
  )
import Grisette.IR.SymPrim.Data.Prim.PartialEval.GeneralFun
  ( pevalGeneralFunApplyTerm,
  )
import Grisette.IR.SymPrim.Data.Prim.PartialEval.Integral (pevalModBoundedIntegralTerm)
import Grisette.IR.SymPrim.Data.Prim.PartialEval.Num
  ( pevalAbsNumTerm,
    pevalAddNumTerm,
    pevalGeNumTerm,
    pevalLeNumTerm,
    pevalMinusNumTerm,
    pevalSignumNumTerm,
    pevalTimesNumTerm,
    pevalUMinusNumTerm,
  )
import Grisette.IR.SymPrim.Data.Prim.PartialEval.TabularFun
  ( pevalTabularFunApplyTerm,
  )
import Grisette.IR.SymPrim.Data.TabularFun (type (=->))
import Grisette.Utils.Parameterized
  ( KnownProof (KnownProof),
    LeqProof (LeqProof),
    knownAdd,
    leqAddPos,
    leqTrans,
    unsafeKnownProof,
    unsafeLeqProof,
  )
import Language.Haskell.TH.Syntax (Lift)

-- $setup
-- >>> import Grisette.Core
-- >>> import Grisette.IR.SymPrim
-- >>> import Grisette.Backend.SBV
-- >>> import Data.Proxy

-- | Symbolic Boolean type.
--
-- >>> :set -XOverloadedStrings
-- >>> "a" :: SymBool
-- a
-- >>> "a" .&& "b" :: SymBool
-- (&& a b)
--
-- More symbolic operations are available. Please refer to the documentation
-- for the type class instances.
newtype SymBool = SymBool {SymBool -> Term Bool
underlyingBoolTerm :: Term Bool}
  deriving ((forall (m :: * -> *). Quote m => SymBool -> m Exp)
-> (forall (m :: * -> *). Quote m => SymBool -> Code m SymBool)
-> Lift SymBool
forall t.
(forall (m :: * -> *). Quote m => t -> m Exp)
-> (forall (m :: * -> *). Quote m => t -> Code m t) -> Lift t
forall (m :: * -> *). Quote m => SymBool -> m Exp
forall (m :: * -> *). Quote m => SymBool -> Code m SymBool
$clift :: forall (m :: * -> *). Quote m => SymBool -> m Exp
lift :: forall (m :: * -> *). Quote m => SymBool -> m Exp
$cliftTyped :: forall (m :: * -> *). Quote m => SymBool -> Code m SymBool
liftTyped :: forall (m :: * -> *). Quote m => SymBool -> Code m SymBool
Lift, SymBool -> ()
(SymBool -> ()) -> NFData SymBool
forall a. (a -> ()) -> NFData a
$crnf :: SymBool -> ()
rnf :: SymBool -> ()
NFData, (forall x. SymBool -> Rep SymBool x)
-> (forall x. Rep SymBool x -> SymBool) -> Generic SymBool
forall x. Rep SymBool x -> SymBool
forall x. SymBool -> Rep SymBool x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cfrom :: forall x. SymBool -> Rep SymBool x
from :: forall x. SymBool -> Rep SymBool x
$cto :: forall x. Rep SymBool x -> SymBool
to :: forall x. Rep SymBool x -> SymBool
Generic)

-- | Symbolic (unbounded, mathematical) integer type.
--
-- >>> "a" + 1 :: SymInteger
-- (+ 1 a)
--
-- More symbolic operations are available. Please refer to the documentation
-- for the type class instances.
newtype SymInteger = SymInteger {SymInteger -> Term Integer
underlyingIntegerTerm :: Term Integer}
  deriving ((forall (m :: * -> *). Quote m => SymInteger -> m Exp)
-> (forall (m :: * -> *).
    Quote m =>
    SymInteger -> Code m SymInteger)
-> Lift SymInteger
forall t.
(forall (m :: * -> *). Quote m => t -> m Exp)
-> (forall (m :: * -> *). Quote m => t -> Code m t) -> Lift t
forall (m :: * -> *). Quote m => SymInteger -> m Exp
forall (m :: * -> *). Quote m => SymInteger -> Code m SymInteger
$clift :: forall (m :: * -> *). Quote m => SymInteger -> m Exp
lift :: forall (m :: * -> *). Quote m => SymInteger -> m Exp
$cliftTyped :: forall (m :: * -> *). Quote m => SymInteger -> Code m SymInteger
liftTyped :: forall (m :: * -> *). Quote m => SymInteger -> Code m SymInteger
Lift, SymInteger -> ()
(SymInteger -> ()) -> NFData SymInteger
forall a. (a -> ()) -> NFData a
$crnf :: SymInteger -> ()
rnf :: SymInteger -> ()
NFData, (forall x. SymInteger -> Rep SymInteger x)
-> (forall x. Rep SymInteger x -> SymInteger) -> Generic SymInteger
forall x. Rep SymInteger x -> SymInteger
forall x. SymInteger -> Rep SymInteger x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cfrom :: forall x. SymInteger -> Rep SymInteger x
from :: forall x. SymInteger -> Rep SymInteger x
$cto :: forall x. Rep SymInteger x -> SymInteger
to :: forall x. Rep SymInteger x -> SymInteger
Generic)

#define QUOTE() '
#define QID(a) a
#define QRIGHT(a) QID(a)'

-- | Symbolic signed bit vector type. Indexed with the bit width.
-- Signedness affects the semantics of the operations, including
-- comparison/extension, etc.
--
-- >>> :set -XOverloadedStrings -XDataKinds -XBinaryLiterals
-- >>> "a" + 5 :: SymIntN 5
-- (+ 0b00101 a)
-- >>> sizedBVConcat (con 0b101 :: SymIntN 3) (con 0b110 :: SymIntN 3)
-- 0b101110
-- >>> sizedBVExt (Proxy @6) (con 0b101 :: SymIntN 3)
-- 0b111101
-- >>> (8 :: SymIntN 4) .< (7 :: SymIntN 4)
-- true
--
-- More symbolic operations are available. Please refer to the documentation
-- for the type class instances.
newtype SymIntN (n :: Nat) = SymIntN {forall (n :: Nat). SymIntN n -> Term (IntN n)
underlyingIntNTerm :: Term (IntN n)}
  deriving ((forall (m :: * -> *). Quote m => SymIntN n -> m Exp)
-> (forall (m :: * -> *).
    Quote m =>
    SymIntN n -> Code m (SymIntN n))
-> Lift (SymIntN n)
forall (n :: Nat) (m :: * -> *). Quote m => SymIntN n -> m Exp
forall (n :: Nat) (m :: * -> *).
Quote m =>
SymIntN n -> Code m (SymIntN n)
forall t.
(forall (m :: * -> *). Quote m => t -> m Exp)
-> (forall (m :: * -> *). Quote m => t -> Code m t) -> Lift t
forall (m :: * -> *). Quote m => SymIntN n -> m Exp
forall (m :: * -> *). Quote m => SymIntN n -> Code m (SymIntN n)
$clift :: forall (n :: Nat) (m :: * -> *). Quote m => SymIntN n -> m Exp
lift :: forall (m :: * -> *). Quote m => SymIntN n -> m Exp
$cliftTyped :: forall (n :: Nat) (m :: * -> *).
Quote m =>
SymIntN n -> Code m (SymIntN n)
liftTyped :: forall (m :: * -> *). Quote m => SymIntN n -> Code m (SymIntN n)
Lift, SymIntN n -> ()
(SymIntN n -> ()) -> NFData (SymIntN n)
forall (n :: Nat). SymIntN n -> ()
forall a. (a -> ()) -> NFData a
$crnf :: forall (n :: Nat). SymIntN n -> ()
rnf :: SymIntN n -> ()
NFData, (forall x. SymIntN n -> Rep (SymIntN n) x)
-> (forall x. Rep (SymIntN n) x -> SymIntN n)
-> Generic (SymIntN n)
forall (n :: Nat) x. Rep (SymIntN n) x -> SymIntN n
forall (n :: Nat) x. SymIntN n -> Rep (SymIntN n) x
forall x. Rep (SymIntN n) x -> SymIntN n
forall x. SymIntN n -> Rep (SymIntN n) x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cfrom :: forall (n :: Nat) x. SymIntN n -> Rep (SymIntN n) x
from :: forall x. SymIntN n -> Rep (SymIntN n) x
$cto :: forall (n :: Nat) x. Rep (SymIntN n) x -> SymIntN n
to :: forall x. Rep (SymIntN n) x -> SymIntN n
Generic)

-- | Symbolic signed bit vector type. Not indexed, but the bit width is
-- fixed at the creation time.
--
-- A 'SomeSymIntN' must be created by wrapping a 'SymIntN' with the
-- 'SomeSymIntN' constructor to fix the bit width:
--
-- >>> (SomeSymIntN ("a" :: SymIntN 5))
-- a
--
-- >>> :set -XOverloadedStrings -XDataKinds -XBinaryLiterals
-- >>> (SomeSymIntN ("a" :: SymIntN 5)) + (SomeSymIntN (5 :: SymIntN 5))
-- (+ 0b00101 a)
-- >>> bvConcat (SomeSymIntN (con 0b101 :: SymIntN 3)) (SomeSymIntN (con 0b110 :: SymIntN 3))
-- 0b101110
--
-- More symbolic operations are available. Please refer to the documentation
-- for the type class instances.
data SomeSymIntN where
  SomeSymIntN :: (KnownNat n, 1 <= n) => SymIntN n -> SomeSymIntN

unarySomeSymIntN :: (forall n. (KnownNat n, 1 <= n) => SymIntN n -> r) -> String -> SomeSymIntN -> r
unarySomeSymIntN :: forall r.
(forall (n :: Nat). (KnownNat n, 1 <= n) => SymIntN n -> r)
-> String -> SomeSymIntN -> r
unarySomeSymIntN forall (n :: Nat). (KnownNat n, 1 <= n) => SymIntN n -> r
op String
_ (SomeSymIntN (SymIntN n
w :: SymIntN w)) = SymIntN n -> r
forall (n :: Nat). (KnownNat n, 1 <= n) => SymIntN n -> r
op SymIntN n
w
{-# INLINE unarySomeSymIntN #-}

unarySomeSymIntNR1 :: (forall n. (KnownNat n, 1 <= n) => SymIntN n -> SymIntN n) -> String -> SomeSymIntN -> SomeSymIntN
unarySomeSymIntNR1 :: (forall (n :: Nat). (KnownNat n, 1 <= n) => SymIntN n -> SymIntN n)
-> String -> SomeSymIntN -> SomeSymIntN
unarySomeSymIntNR1 forall (n :: Nat). (KnownNat n, 1 <= n) => SymIntN n -> SymIntN n
op String
_ (SomeSymIntN (SymIntN n
w :: SymIntN w)) = SymIntN n -> SomeSymIntN
forall (con :: Nat).
(KnownNat con, 1 <= con) =>
SymIntN con -> SomeSymIntN
SomeSymIntN (SymIntN n -> SomeSymIntN) -> SymIntN n -> SomeSymIntN
forall a b. (a -> b) -> a -> b
$ SymIntN n -> SymIntN n
forall (n :: Nat). (KnownNat n, 1 <= n) => SymIntN n -> SymIntN n
op SymIntN n
w
{-# INLINE unarySomeSymIntNR1 #-}

binSomeSymIntN :: (forall n. (KnownNat n, 1 <= n) => SymIntN n -> SymIntN n -> r) -> String -> SomeSymIntN -> SomeSymIntN -> r
binSomeSymIntN :: forall r.
(forall (n :: Nat).
 (KnownNat n, 1 <= n) =>
 SymIntN n -> SymIntN n -> r)
-> String -> SomeSymIntN -> SomeSymIntN -> r
binSomeSymIntN forall (n :: Nat).
(KnownNat n, 1 <= n) =>
SymIntN n -> SymIntN n -> r
op String
str (SomeSymIntN (SymIntN n
l :: SymIntN l)) (SomeSymIntN (SymIntN n
r :: SymIntN r)) =
  case Proxy n -> Proxy n -> Maybe (n :~: n)
forall (a :: Nat) (b :: Nat) (proxy1 :: Nat -> *)
       (proxy2 :: Nat -> *).
(KnownNat a, KnownNat b) =>
proxy1 a -> proxy2 b -> Maybe (a :~: b)
sameNat (forall (t :: Nat). Proxy t
forall {k} (t :: k). Proxy t
Proxy @l) (forall (t :: Nat). Proxy t
forall {k} (t :: k). Proxy t
Proxy @r) of
    Just n :~: n
Refl -> SymIntN n -> SymIntN n -> r
forall (n :: Nat).
(KnownNat n, 1 <= n) =>
SymIntN n -> SymIntN n -> r
op SymIntN n
l SymIntN n
SymIntN n
r
    Maybe (n :~: n)
Nothing -> String -> r
forall a. HasCallStack => String -> a
error (String -> r) -> String -> r
forall a b. (a -> b) -> a -> b
$ String
"Operation " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
str String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
" on SymIntN with different bitwidth"
{-# INLINE binSomeSymIntN #-}

binSomeSymIntNR1 :: (forall n. (KnownNat n, 1 <= n) => SymIntN n -> SymIntN n -> SymIntN n) -> String -> SomeSymIntN -> SomeSymIntN -> SomeSymIntN
binSomeSymIntNR1 :: (forall (n :: Nat).
 (KnownNat n, 1 <= n) =>
 SymIntN n -> SymIntN n -> SymIntN n)
-> String -> SomeSymIntN -> SomeSymIntN -> SomeSymIntN
binSomeSymIntNR1 forall (n :: Nat).
(KnownNat n, 1 <= n) =>
SymIntN n -> SymIntN n -> SymIntN n
op String
str (SomeSymIntN (SymIntN n
l :: SymIntN l)) (SomeSymIntN (SymIntN n
r :: SymIntN r)) =
  case Proxy n -> Proxy n -> Maybe (n :~: n)
forall (a :: Nat) (b :: Nat) (proxy1 :: Nat -> *)
       (proxy2 :: Nat -> *).
(KnownNat a, KnownNat b) =>
proxy1 a -> proxy2 b -> Maybe (a :~: b)
sameNat (forall (t :: Nat). Proxy t
forall {k} (t :: k). Proxy t
Proxy @l) (forall (t :: Nat). Proxy t
forall {k} (t :: k). Proxy t
Proxy @r) of
    Just n :~: n
Refl -> SymIntN n -> SomeSymIntN
forall (con :: Nat).
(KnownNat con, 1 <= con) =>
SymIntN con -> SomeSymIntN
SomeSymIntN (SymIntN n -> SomeSymIntN) -> SymIntN n -> SomeSymIntN
forall a b. (a -> b) -> a -> b
$ SymIntN n -> SymIntN n -> SymIntN n
forall (n :: Nat).
(KnownNat n, 1 <= n) =>
SymIntN n -> SymIntN n -> SymIntN n
op SymIntN n
l SymIntN n
SymIntN n
r
    Maybe (n :~: n)
Nothing -> String -> SomeSymIntN
forall a. HasCallStack => String -> a
error (String -> SomeSymIntN) -> String -> SomeSymIntN
forall a b. (a -> b) -> a -> b
$ String
"Operation " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
str String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
" on SymIntN with different bitwidth"
{-# INLINE binSomeSymIntNR1 #-}

binSomeSymIntNR2 :: (forall n. (KnownNat n, 1 <= n) => SymIntN n -> SymIntN n -> (SymIntN n, SymIntN n)) -> String -> SomeSymIntN -> SomeSymIntN -> (SomeSymIntN, SomeSymIntN)
binSomeSymIntNR2 :: (forall (n :: Nat).
 (KnownNat n, 1 <= n) =>
 SymIntN n -> SymIntN n -> (SymIntN n, SymIntN n))
-> String
-> SomeSymIntN
-> SomeSymIntN
-> (SomeSymIntN, SomeSymIntN)
binSomeSymIntNR2 forall (n :: Nat).
(KnownNat n, 1 <= n) =>
SymIntN n -> SymIntN n -> (SymIntN n, SymIntN n)
op String
str (SomeSymIntN (SymIntN n
l :: SymIntN l)) (SomeSymIntN (SymIntN n
r :: SymIntN r)) =
  case Proxy n -> Proxy n -> Maybe (n :~: n)
forall (a :: Nat) (b :: Nat) (proxy1 :: Nat -> *)
       (proxy2 :: Nat -> *).
(KnownNat a, KnownNat b) =>
proxy1 a -> proxy2 b -> Maybe (a :~: b)
sameNat (forall (t :: Nat). Proxy t
forall {k} (t :: k). Proxy t
Proxy @l) (forall (t :: Nat). Proxy t
forall {k} (t :: k). Proxy t
Proxy @r) of
    Just n :~: n
Refl ->
      case SymIntN n -> SymIntN n -> (SymIntN n, SymIntN n)
forall (n :: Nat).
(KnownNat n, 1 <= n) =>
SymIntN n -> SymIntN n -> (SymIntN n, SymIntN n)
op SymIntN n
l SymIntN n
SymIntN n
r of
        (SymIntN n
a, SymIntN n
b) -> (SymIntN n -> SomeSymIntN
forall (con :: Nat).
(KnownNat con, 1 <= con) =>
SymIntN con -> SomeSymIntN
SomeSymIntN SymIntN n
a, SymIntN n -> SomeSymIntN
forall (con :: Nat).
(KnownNat con, 1 <= con) =>
SymIntN con -> SomeSymIntN
SomeSymIntN SymIntN n
b)
    Maybe (n :~: n)
Nothing -> String -> (SomeSymIntN, SomeSymIntN)
forall a. HasCallStack => String -> a
error (String -> (SomeSymIntN, SomeSymIntN))
-> String -> (SomeSymIntN, SomeSymIntN)
forall a b. (a -> b) -> a -> b
$ String
"Operation " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
str String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
" on SymIntN with different bitwidth"
{-# INLINE binSomeSymIntNR2 #-}

-- | Symbolic unsigned bit vector type. Indexed with the bit width.
-- Signedness affects the semantics of the operations, including
-- comparison/extension, etc.
--
-- >>> :set -XOverloadedStrings -XDataKinds -XBinaryLiterals
-- >>> "a" + 5 :: SymWordN 5
-- (+ 0b00101 a)
-- >>> sizedBVConcat (con 0b101 :: SymWordN 3) (con 0b110 :: SymWordN 3)
-- 0b101110
-- >>> sizedBVExt (Proxy @6) (con 0b101 :: SymWordN 3)
-- 0b000101
-- >>> (8 :: SymWordN 4) .< (7 :: SymWordN 4)
-- false
--
-- More symbolic operations are available. Please refer to the documentation
-- for the type class instances.
newtype SymWordN (n :: Nat) = SymWordN {forall (n :: Nat). SymWordN n -> Term (WordN n)
underlyingWordNTerm :: Term (WordN n)}
  deriving ((forall (m :: * -> *). Quote m => SymWordN n -> m Exp)
-> (forall (m :: * -> *).
    Quote m =>
    SymWordN n -> Code m (SymWordN n))
-> Lift (SymWordN n)
forall (n :: Nat) (m :: * -> *). Quote m => SymWordN n -> m Exp
forall (n :: Nat) (m :: * -> *).
Quote m =>
SymWordN n -> Code m (SymWordN n)
forall t.
(forall (m :: * -> *). Quote m => t -> m Exp)
-> (forall (m :: * -> *). Quote m => t -> Code m t) -> Lift t
forall (m :: * -> *). Quote m => SymWordN n -> m Exp
forall (m :: * -> *). Quote m => SymWordN n -> Code m (SymWordN n)
$clift :: forall (n :: Nat) (m :: * -> *). Quote m => SymWordN n -> m Exp
lift :: forall (m :: * -> *). Quote m => SymWordN n -> m Exp
$cliftTyped :: forall (n :: Nat) (m :: * -> *).
Quote m =>
SymWordN n -> Code m (SymWordN n)
liftTyped :: forall (m :: * -> *). Quote m => SymWordN n -> Code m (SymWordN n)
Lift, SymWordN n -> ()
(SymWordN n -> ()) -> NFData (SymWordN n)
forall (n :: Nat). SymWordN n -> ()
forall a. (a -> ()) -> NFData a
$crnf :: forall (n :: Nat). SymWordN n -> ()
rnf :: SymWordN n -> ()
NFData, (forall x. SymWordN n -> Rep (SymWordN n) x)
-> (forall x. Rep (SymWordN n) x -> SymWordN n)
-> Generic (SymWordN n)
forall (n :: Nat) x. Rep (SymWordN n) x -> SymWordN n
forall (n :: Nat) x. SymWordN n -> Rep (SymWordN n) x
forall x. Rep (SymWordN n) x -> SymWordN n
forall x. SymWordN n -> Rep (SymWordN n) x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cfrom :: forall (n :: Nat) x. SymWordN n -> Rep (SymWordN n) x
from :: forall x. SymWordN n -> Rep (SymWordN n) x
$cto :: forall (n :: Nat) x. Rep (SymWordN n) x -> SymWordN n
to :: forall x. Rep (SymWordN n) x -> SymWordN n
Generic)

-- | Symbolic unsigned bit vector type. Not indexed, but the bit width is
-- fixed at the creation time.
--
-- A 'SomeSymWordN' must be created by wrapping a 'SymWordN' with the
-- 'SomeSymWordN' constructor to fix the bit width:
--
-- >>> (SomeSymWordN ("a" :: SymWordN 5))
-- a
--
-- >>> :set -XOverloadedStrings -XDataKinds -XBinaryLiterals
-- >>> (SomeSymWordN ("a" :: SymWordN 5)) + (SomeSymWordN (5 :: SymWordN 5))
-- (+ 0b00101 a)
-- >>> bvConcat (SomeSymWordN (con 0b101 :: SymWordN 3)) (SomeSymWordN (con 0b110 :: SymWordN 3))
-- 0b101110
--
-- More symbolic operations are available. Please refer to the documentation
-- for the type class instances.
data SomeSymWordN where
  SomeSymWordN :: (KnownNat n, 1 <= n) => SymWordN n -> SomeSymWordN

unarySomeSymWordN :: (forall n. (KnownNat n, 1 <= n) => SymWordN n -> r) -> String -> SomeSymWordN -> r
unarySomeSymWordN :: forall r.
(forall (n :: Nat). (KnownNat n, 1 <= n) => SymWordN n -> r)
-> String -> SomeSymWordN -> r
unarySomeSymWordN forall (n :: Nat). (KnownNat n, 1 <= n) => SymWordN n -> r
op String
_ (SomeSymWordN (SymWordN n
w :: SymWordN w)) = SymWordN n -> r
forall (n :: Nat). (KnownNat n, 1 <= n) => SymWordN n -> r
op SymWordN n
w
{-# INLINE unarySomeSymWordN #-}

unarySomeSymWordNR1 :: (forall n. (KnownNat n, 1 <= n) => SymWordN n -> SymWordN n) -> String -> SomeSymWordN -> SomeSymWordN
unarySomeSymWordNR1 :: (forall (n :: Nat).
 (KnownNat n, 1 <= n) =>
 SymWordN n -> SymWordN n)
-> String -> SomeSymWordN -> SomeSymWordN
unarySomeSymWordNR1 forall (n :: Nat). (KnownNat n, 1 <= n) => SymWordN n -> SymWordN n
op String
_ (SomeSymWordN (SymWordN n
w :: SymWordN w)) = SymWordN n -> SomeSymWordN
forall (con :: Nat).
(KnownNat con, 1 <= con) =>
SymWordN con -> SomeSymWordN
SomeSymWordN (SymWordN n -> SomeSymWordN) -> SymWordN n -> SomeSymWordN
forall a b. (a -> b) -> a -> b
$ SymWordN n -> SymWordN n
forall (n :: Nat). (KnownNat n, 1 <= n) => SymWordN n -> SymWordN n
op SymWordN n
w
{-# INLINE unarySomeSymWordNR1 #-}

binSomeSymWordN :: (forall n. (KnownNat n, 1 <= n) => SymWordN n -> SymWordN n -> r) -> String -> SomeSymWordN -> SomeSymWordN -> r
binSomeSymWordN :: forall r.
(forall (n :: Nat).
 (KnownNat n, 1 <= n) =>
 SymWordN n -> SymWordN n -> r)
-> String -> SomeSymWordN -> SomeSymWordN -> r
binSomeSymWordN forall (n :: Nat).
(KnownNat n, 1 <= n) =>
SymWordN n -> SymWordN n -> r
op String
str (SomeSymWordN (SymWordN n
l :: SymWordN l)) (SomeSymWordN (SymWordN n
r :: SymWordN r)) =
  case Proxy n -> Proxy n -> Maybe (n :~: n)
forall (a :: Nat) (b :: Nat) (proxy1 :: Nat -> *)
       (proxy2 :: Nat -> *).
(KnownNat a, KnownNat b) =>
proxy1 a -> proxy2 b -> Maybe (a :~: b)
sameNat (forall (t :: Nat). Proxy t
forall {k} (t :: k). Proxy t
Proxy @l) (forall (t :: Nat). Proxy t
forall {k} (t :: k). Proxy t
Proxy @r) of
    Just n :~: n
Refl -> SymWordN n -> SymWordN n -> r
forall (n :: Nat).
(KnownNat n, 1 <= n) =>
SymWordN n -> SymWordN n -> r
op SymWordN n
l SymWordN n
SymWordN n
r
    Maybe (n :~: n)
Nothing -> String -> r
forall a. HasCallStack => String -> a
error (String -> r) -> String -> r
forall a b. (a -> b) -> a -> b
$ String
"Operation " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
str String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
" on SymWordN with different bitwidth"
{-# INLINE binSomeSymWordN #-}

binSomeSymWordNR1 :: (forall n. (KnownNat n, 1 <= n) => SymWordN n -> SymWordN n -> SymWordN n) -> String -> SomeSymWordN -> SomeSymWordN -> SomeSymWordN
binSomeSymWordNR1 :: (forall (n :: Nat).
 (KnownNat n, 1 <= n) =>
 SymWordN n -> SymWordN n -> SymWordN n)
-> String -> SomeSymWordN -> SomeSymWordN -> SomeSymWordN
binSomeSymWordNR1 forall (n :: Nat).
(KnownNat n, 1 <= n) =>
SymWordN n -> SymWordN n -> SymWordN n
op String
str (SomeSymWordN (SymWordN n
l :: SymWordN l)) (SomeSymWordN (SymWordN n
r :: SymWordN r)) =
  case Proxy n -> Proxy n -> Maybe (n :~: n)
forall (a :: Nat) (b :: Nat) (proxy1 :: Nat -> *)
       (proxy2 :: Nat -> *).
(KnownNat a, KnownNat b) =>
proxy1 a -> proxy2 b -> Maybe (a :~: b)
sameNat (forall (t :: Nat). Proxy t
forall {k} (t :: k). Proxy t
Proxy @l) (forall (t :: Nat). Proxy t
forall {k} (t :: k). Proxy t
Proxy @r) of
    Just n :~: n
Refl -> SymWordN n -> SomeSymWordN
forall (con :: Nat).
(KnownNat con, 1 <= con) =>
SymWordN con -> SomeSymWordN
SomeSymWordN (SymWordN n -> SomeSymWordN) -> SymWordN n -> SomeSymWordN
forall a b. (a -> b) -> a -> b
$ SymWordN n -> SymWordN n -> SymWordN n
forall (n :: Nat).
(KnownNat n, 1 <= n) =>
SymWordN n -> SymWordN n -> SymWordN n
op SymWordN n
l SymWordN n
SymWordN n
r
    Maybe (n :~: n)
Nothing -> String -> SomeSymWordN
forall a. HasCallStack => String -> a
error (String -> SomeSymWordN) -> String -> SomeSymWordN
forall a b. (a -> b) -> a -> b
$ String
"Operation " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
str String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
" on SymWordN with different bitwidth"
{-# INLINE binSomeSymWordNR1 #-}

binSomeSymWordNR2 :: (forall n. (KnownNat n, 1 <= n) => SymWordN n -> SymWordN n -> (SymWordN n, SymWordN n)) -> String -> SomeSymWordN -> SomeSymWordN -> (SomeSymWordN, SomeSymWordN)
binSomeSymWordNR2 :: (forall (n :: Nat).
 (KnownNat n, 1 <= n) =>
 SymWordN n -> SymWordN n -> (SymWordN n, SymWordN n))
-> String
-> SomeSymWordN
-> SomeSymWordN
-> (SomeSymWordN, SomeSymWordN)
binSomeSymWordNR2 forall (n :: Nat).
(KnownNat n, 1 <= n) =>
SymWordN n -> SymWordN n -> (SymWordN n, SymWordN n)
op String
str (SomeSymWordN (SymWordN n
l :: SymWordN l)) (SomeSymWordN (SymWordN n
r :: SymWordN r)) =
  case Proxy n -> Proxy n -> Maybe (n :~: n)
forall (a :: Nat) (b :: Nat) (proxy1 :: Nat -> *)
       (proxy2 :: Nat -> *).
(KnownNat a, KnownNat b) =>
proxy1 a -> proxy2 b -> Maybe (a :~: b)
sameNat (forall (t :: Nat). Proxy t
forall {k} (t :: k). Proxy t
Proxy @l) (forall (t :: Nat). Proxy t
forall {k} (t :: k). Proxy t
Proxy @r) of
    Just n :~: n
Refl ->
      case SymWordN n -> SymWordN n -> (SymWordN n, SymWordN n)
forall (n :: Nat).
(KnownNat n, 1 <= n) =>
SymWordN n -> SymWordN n -> (SymWordN n, SymWordN n)
op SymWordN n
l SymWordN n
SymWordN n
r of
        (SymWordN n
a, SymWordN n
b) -> (SymWordN n -> SomeSymWordN
forall (con :: Nat).
(KnownNat con, 1 <= con) =>
SymWordN con -> SomeSymWordN
SomeSymWordN SymWordN n
a, SymWordN n -> SomeSymWordN
forall (con :: Nat).
(KnownNat con, 1 <= con) =>
SymWordN con -> SomeSymWordN
SomeSymWordN SymWordN n
b)
    Maybe (n :~: n)
Nothing -> String -> (SomeSymWordN, SomeSymWordN)
forall a. HasCallStack => String -> a
error (String -> (SomeSymWordN, SomeSymWordN))
-> String -> (SomeSymWordN, SomeSymWordN)
forall a b. (a -> b) -> a -> b
$ String
"Operation " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
str String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
" on SymWordN with different bitwidth"
{-# INLINE binSomeSymWordNR2 #-}

instance ConRep SymBool where
  type ConType SymBool = Bool

instance SymRep Bool where
  type SymType Bool = SymBool

instance LinkedRep Bool SymBool where
  underlyingTerm :: SymBool -> Term Bool
underlyingTerm (SymBool Term Bool
a) = Term Bool
a
  wrapTerm :: Term Bool -> SymBool
wrapTerm = Term Bool -> SymBool
SymBool

instance ConRep SymInteger where
  type ConType SymInteger = Integer

instance SymRep Integer where
  type SymType Integer = SymInteger

instance LinkedRep Integer SymInteger where
  underlyingTerm :: SymInteger -> Term Integer
underlyingTerm (SymInteger Term Integer
a) = Term Integer
a
  wrapTerm :: Term Integer -> SymInteger
wrapTerm = Term Integer -> SymInteger
SymInteger

instance (KnownNat n, 1 <= n) => ConRep (SymIntN n) where
  type ConType (SymIntN n) = IntN n

instance (KnownNat n, 1 <= n) => SymRep (IntN n) where
  type SymType (IntN n) = SymIntN n

instance (KnownNat n, 1 <= n) => LinkedRep (IntN n) (SymIntN n) where
  underlyingTerm :: SymIntN n -> Term (IntN n)
underlyingTerm (SymIntN Term (IntN n)
a) = Term (IntN n)
a
  wrapTerm :: Term (IntN n) -> SymIntN n
wrapTerm = Term (IntN n) -> SymIntN n
forall (n :: Nat). Term (IntN n) -> SymIntN n
SymIntN

instance (KnownNat n, 1 <= n) => ConRep (SymWordN n) where
  type ConType (SymWordN n) = WordN n

instance (KnownNat n, 1 <= n) => SymRep (WordN n) where
  type SymType (WordN n) = SymWordN n

instance (KnownNat n, 1 <= n) => LinkedRep (WordN n) (SymWordN n) where
  underlyingTerm :: SymWordN n -> Term (WordN n)
underlyingTerm (SymWordN Term (WordN n)
a) = Term (WordN n)
a
  wrapTerm :: Term (WordN n) -> SymWordN n
wrapTerm = Term (WordN n) -> SymWordN n
forall (n :: Nat). Term (WordN n) -> SymWordN n
SymWordN

-- | Symbolic tabular function type.
--
-- >>> :set -XTypeOperators -XOverloadedStrings
-- >>> f' = "f" :: SymInteger =~> SymInteger
-- >>> f = (f' #)
-- >>> f 1
-- (apply f 1)
--
-- >>> f' = con (TabularFun [(1, 2), (2, 3)] 4) :: SymInteger =~> SymInteger
-- >>> f = (f' #)
-- >>> f 1
-- 2
-- >>> f 2
-- 3
-- >>> f 3
-- 4
-- >>> f "b"
-- (ite (= b 1) 2 (ite (= b 2) 3 4))
data sa =~> sb where
  SymTabularFun :: (LinkedRep ca sa, LinkedRep cb sb) => Term (ca =-> cb) -> sa =~> sb

infixr 0 =~>

instance (ConRep a, ConRep b) => ConRep (a =~> b) where
  type ConType (a =~> b) = ConType a =-> ConType b

instance (SymRep a, SymRep b) => SymRep (a =-> b) where
  type SymType (a =-> b) = SymType a =~> SymType b

instance (LinkedRep ca sa, LinkedRep cb sb) => LinkedRep (ca =-> cb) (sa =~> sb) where
  underlyingTerm :: (sa =~> sb) -> Term (ca =-> cb)
underlyingTerm (SymTabularFun Term (ca =-> cb)
a) = Term (ca =-> cb)
Term (ca =-> cb)
a
  wrapTerm :: Term (ca =-> cb) -> sa =~> sb
wrapTerm = Term (ca =-> cb) -> sa =~> sb
forall ca sa cb sb.
(LinkedRep ca sa, LinkedRep cb sb) =>
Term (ca =-> cb) -> sa =~> sb
SymTabularFun

instance (SupportedPrim ca, SupportedPrim cb, LinkedRep ca sa, LinkedRep cb sb) => Function (sa =~> sb) where
  type Arg (sa =~> sb) = sa
  type Ret (sa =~> sb) = sb
  (SymTabularFun Term (ca =-> cb)
f) # :: (sa =~> sb) -> Arg (sa =~> sb) -> Ret (sa =~> sb)
# Arg (sa =~> sb)
t = Term cb -> Ret (sa =~> sb)
forall con sym. LinkedRep con sym => Term con -> sym
wrapTerm (Term cb -> Ret (sa =~> sb)) -> Term cb -> Ret (sa =~> sb)
forall a b. (a -> b) -> a -> b
$ Term (ca =-> cb) -> Term ca -> Term cb
forall a b.
(SupportedPrim a, SupportedPrim b) =>
Term (a =-> b) -> Term a -> Term b
pevalTabularFunApplyTerm Term (ca =-> cb)
f (sa -> Term ca
forall con sym. LinkedRep con sym => sym -> Term con
underlyingTerm sa
Arg (sa =~> sb)
t)

instance (LinkedRep ca sa, LinkedRep ct st, Apply st) => Apply (sa =~> st) where
  type FunType (sa =~> st) = sa -> FunType st
  apply :: (sa =~> st) -> FunType (sa =~> st)
apply sa =~> st
uf sa
a = st -> FunType st
forall uf. Apply uf => uf -> FunType uf
apply (sa =~> st
uf (sa =~> st) -> Arg (sa =~> st) -> Ret (sa =~> st)
forall f. Function f => f -> Arg f -> Ret f
# sa
Arg (sa =~> st)
a)

-- |
-- Symbolic general function type.
--
-- >>> :set -XTypeOperators -XOverloadedStrings
-- >>> f' = "f" :: SymInteger -~> SymInteger
-- >>> f = (f' #)
-- >>> f 1
-- (apply f 1)
--
-- >>> f' = con ("a" --> "a" + 1) :: SymInteger -~> SymInteger
-- >>> f'
-- \(a:ARG :: Integer) -> (+ 1 a:ARG)
-- >>> f = (f' #)
-- >>> f 1
-- 2
-- >>> f 2
-- 3
-- >>> f 3
-- 4
-- >>> f "b"
-- (+ 1 b)
data sa -~> sb where
  SymGeneralFun :: (LinkedRep ca sa, LinkedRep cb sb) => Term (ca --> cb) -> sa -~> sb

infixr 0 -~>

instance (ConRep a, ConRep b) => ConRep (a -~> b) where
  type ConType (a -~> b) = ConType a --> ConType b

instance (SymRep ca, SymRep cb) => SymRep (ca --> cb) where
  type SymType (ca --> cb) = SymType ca -~> SymType cb

instance (LinkedRep ca sa, LinkedRep cb sb) => LinkedRep (ca --> cb) (sa -~> sb) where
  underlyingTerm :: (sa -~> sb) -> Term (ca --> cb)
underlyingTerm (SymGeneralFun Term (ca --> cb)
a) = Term (ca --> cb)
Term (ca --> cb)
a
  wrapTerm :: Term (ca --> cb) -> sa -~> sb
wrapTerm = Term (ca --> cb) -> sa -~> sb
forall ca sa cb sb.
(LinkedRep ca sa, LinkedRep cb sb) =>
Term (ca --> cb) -> sa -~> sb
SymGeneralFun

instance (SupportedPrim ca, SupportedPrim cb, LinkedRep ca sa, LinkedRep cb sb) => Function (sa -~> sb) where
  type Arg (sa -~> sb) = sa
  type Ret (sa -~> sb) = sb
  (SymGeneralFun Term (ca --> cb)
f) # :: (sa -~> sb) -> Arg (sa -~> sb) -> Ret (sa -~> sb)
# Arg (sa -~> sb)
t = Term cb -> Ret (sa -~> sb)
forall con sym. LinkedRep con sym => Term con -> sym
wrapTerm (Term cb -> Ret (sa -~> sb)) -> Term cb -> Ret (sa -~> sb)
forall a b. (a -> b) -> a -> b
$ Term (ca --> cb) -> Term ca -> Term cb
forall a b.
(SupportedPrim a, SupportedPrim b) =>
Term (a --> b) -> Term a -> Term b
pevalGeneralFunApplyTerm Term (ca --> cb)
f (sa -> Term ca
forall con sym. LinkedRep con sym => sym -> Term con
underlyingTerm sa
Arg (sa -~> sb)
t)

instance (LinkedRep ca sa, LinkedRep ct st, Apply st) => Apply (sa -~> st) where
  type FunType (sa -~> st) = sa -> FunType st
  apply :: (sa -~> st) -> FunType (sa -~> st)
apply sa -~> st
uf sa
a = st -> FunType st
forall uf. Apply uf => uf -> FunType uf
apply (sa -~> st
uf (sa -~> st) -> Arg (sa -~> st) -> Ret (sa -~> st)
forall f. Function f => f -> Arg f -> Ret f
# sa
Arg (sa -~> st)
a)

-- | Construction of general symbolic functions.
--
-- >>> f = "a" --> "a" + 1 :: Integer --> Integer
-- >>> f
-- \(a:ARG :: Integer) -> (+ 1 a:ARG)
--
-- This general symbolic function needs to be applied to symbolic values:
-- >>> f # ("a" :: SymInteger)
-- (+ 1 a)
(-->) :: (SupportedPrim ca, SupportedPrim cb, LinkedRep cb sb) => TypedSymbol ca -> sb -> ca --> cb
--> :: forall ca cb sb.
(SupportedPrim ca, SupportedPrim cb, LinkedRep cb sb) =>
TypedSymbol ca -> sb -> ca --> cb
(-->) TypedSymbol ca
arg sb
v = TypedSymbol ca -> Term cb -> ca --> cb
forall a b.
(SupportedPrim a, SupportedPrim b) =>
TypedSymbol a -> Term b -> a --> b
GeneralFun TypedSymbol ca
newarg (TypedSymbol ca -> Term ca -> Term cb -> Term cb
forall a b.
(SupportedPrim a, SupportedPrim b) =>
TypedSymbol a -> Term a -> Term b -> Term b
substTerm TypedSymbol ca
arg (TypedSymbol ca -> Term ca
forall t. (SupportedPrim t, Typeable t) => TypedSymbol t -> Term t
symTerm TypedSymbol ca
newarg) (sb -> Term cb
forall con sym. LinkedRep con sym => sym -> Term con
underlyingTerm sb
v))
  where
    newarg :: TypedSymbol ca
newarg = TypedSymbol ca -> ARG -> TypedSymbol ca
forall t a.
(SupportedPrim t, Typeable a, Ord a, Lift a, NFData a, Show a,
 Hashable a) =>
TypedSymbol t -> a -> TypedSymbol t
WithInfo TypedSymbol ca
arg ARG
ARG

infixr 0 -->

data ARG = ARG
  deriving (ARG -> ARG -> Bool
(ARG -> ARG -> Bool) -> (ARG -> ARG -> Bool) -> Eq ARG
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: ARG -> ARG -> Bool
== :: ARG -> ARG -> Bool
$c/= :: ARG -> ARG -> Bool
/= :: ARG -> ARG -> Bool
Eq, Eq ARG
Eq ARG =>
(ARG -> ARG -> Ordering)
-> (ARG -> ARG -> Bool)
-> (ARG -> ARG -> Bool)
-> (ARG -> ARG -> Bool)
-> (ARG -> ARG -> Bool)
-> (ARG -> ARG -> ARG)
-> (ARG -> ARG -> ARG)
-> Ord ARG
ARG -> ARG -> Bool
ARG -> ARG -> Ordering
ARG -> ARG -> ARG
forall a.
Eq a =>
(a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
$ccompare :: ARG -> ARG -> Ordering
compare :: ARG -> ARG -> Ordering
$c< :: ARG -> ARG -> Bool
< :: ARG -> ARG -> Bool
$c<= :: ARG -> ARG -> Bool
<= :: ARG -> ARG -> Bool
$c> :: ARG -> ARG -> Bool
> :: ARG -> ARG -> Bool
$c>= :: ARG -> ARG -> Bool
>= :: ARG -> ARG -> Bool
$cmax :: ARG -> ARG -> ARG
max :: ARG -> ARG -> ARG
$cmin :: ARG -> ARG -> ARG
min :: ARG -> ARG -> ARG
Ord, (forall (m :: * -> *). Quote m => ARG -> m Exp)
-> (forall (m :: * -> *). Quote m => ARG -> Code m ARG) -> Lift ARG
forall t.
(forall (m :: * -> *). Quote m => t -> m Exp)
-> (forall (m :: * -> *). Quote m => t -> Code m t) -> Lift t
forall (m :: * -> *). Quote m => ARG -> m Exp
forall (m :: * -> *). Quote m => ARG -> Code m ARG
$clift :: forall (m :: * -> *). Quote m => ARG -> m Exp
lift :: forall (m :: * -> *). Quote m => ARG -> m Exp
$cliftTyped :: forall (m :: * -> *). Quote m => ARG -> Code m ARG
liftTyped :: forall (m :: * -> *). Quote m => ARG -> Code m ARG
Lift, Int -> ARG -> String -> String
[ARG] -> String -> String
ARG -> String
(Int -> ARG -> String -> String)
-> (ARG -> String) -> ([ARG] -> String -> String) -> Show ARG
forall a.
(Int -> a -> String -> String)
-> (a -> String) -> ([a] -> String -> String) -> Show a
$cshowsPrec :: Int -> ARG -> String -> String
showsPrec :: Int -> ARG -> String -> String
$cshow :: ARG -> String
show :: ARG -> String
$cshowList :: [ARG] -> String -> String
showList :: [ARG] -> String -> String
Show, (forall x. ARG -> Rep ARG x)
-> (forall x. Rep ARG x -> ARG) -> Generic ARG
forall x. Rep ARG x -> ARG
forall x. ARG -> Rep ARG x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cfrom :: forall x. ARG -> Rep ARG x
from :: forall x. ARG -> Rep ARG x
$cto :: forall x. Rep ARG x -> ARG
to :: forall x. Rep ARG x -> ARG
Generic)

instance NFData ARG where
  rnf :: ARG -> ()
rnf ARG
ARG = ()

instance Hashable ARG where
  hashWithSalt :: Int -> ARG -> Int
hashWithSalt Int
s ARG
ARG = Int
s Int -> Int -> Int
forall a. Hashable a => Int -> a -> Int
`hashWithSalt` (Int
0 :: Int)

-- Aggregate instances

instance Apply SymBool where
  type FunType SymBool = SymBool
  apply :: SymBool -> FunType SymBool
apply = SymBool -> FunType SymBool
SymBool -> SymBool
forall a. a -> a
id

instance Apply SymInteger where
  type FunType SymInteger = SymInteger
  apply :: SymInteger -> FunType SymInteger
apply = SymInteger -> FunType SymInteger
SymInteger -> SymInteger
forall a. a -> a
id

instance (KnownNat n, 1 <= n) => Apply (SymIntN n) where
  type FunType (SymIntN n) = SymIntN n
  apply :: SymIntN n -> FunType (SymIntN n)
apply = SymIntN n -> FunType (SymIntN n)
SymIntN n -> SymIntN n
forall a. a -> a
id

instance (KnownNat n, 1 <= n) => Apply (SymWordN n) where
  type FunType (SymWordN n) = SymWordN n
  apply :: SymWordN n -> FunType (SymWordN n)
apply = SymWordN n -> FunType (SymWordN n)
SymWordN n -> SymWordN n
forall a. a -> a
id

#define SOLVABLE_SIMPLE(contype, symtype) \
instance Solvable contype symtype where \
  con = symtype . conTerm; \
  ssym = symtype . ssymTerm; \
  isym str i = symtype $ isymTerm str i; \
  sinfosym str info = symtype $ sinfosymTerm str info; \
  iinfosym str i info = symtype $ iinfosymTerm str i info; \
  conView (symtype (ConTerm _ t)) = Just t; \
  conView _ = Nothing

#define SOLVABLE_BV(contype, symtype) \
instance (KnownNat n, 1 <= n) => Solvable (contype n) (symtype n) where \
  con = symtype . conTerm; \
  ssym = symtype . ssymTerm; \
  isym str i = symtype $ isymTerm str i; \
  sinfosym str info = symtype $ sinfosymTerm str info; \
  iinfosym str i info = symtype $ iinfosymTerm str i info; \
  conView (symtype (ConTerm _ t)) = Just t; \
  conView _ = Nothing

#define SOLVABLE_FUN(symop, conop, symcons) \
instance \
  (SupportedPrim ca, SupportedPrim cb, LinkedRep ca sa, LinkedRep cb sb) => \
  Solvable (conop ca cb) (symop sa sb) where \
  con = symcons . conTerm; \
  ssym = symcons . ssymTerm; \
  isym str i = symcons $ isymTerm str i; \
  sinfosym str info = symcons $ sinfosymTerm str info; \
  iinfosym str i info = symcons $ iinfosymTerm str i info; \
  conView (symcons (ConTerm _ t)) = Just t; \
  conView _ = Nothing

#if 1
SOLVABLE_SIMPLE(Bool, SymBool)
SOLVABLE_SIMPLE(Integer, SymInteger)
SOLVABLE_BV(IntN, SymIntN)
SOLVABLE_BV(WordN, SymWordN)
SOLVABLE_FUN((=~>), (=->), SymTabularFun)
SOLVABLE_FUN((-~>), (-->), SymGeneralFun)
#endif

-- Num

#define NUM_BV(symtype) \
instance (KnownNat n, 1 <= n) => Num (symtype n) where \
  (symtype l) + (symtype r) = symtype $ pevalAddNumTerm l r; \
  (symtype l) - (symtype r) = symtype $ pevalMinusNumTerm l r; \
  (symtype l) * (symtype r) = symtype $ pevalTimesNumTerm l r; \
  negate (symtype v) = symtype $ pevalUMinusNumTerm v; \
  abs (symtype v) = symtype $ pevalAbsNumTerm v; \
  signum (symtype v) = symtype $ pevalSignumNumTerm v; \
  fromInteger i = con $ fromInteger i

#define NUM_SOME_BV(somety, br1, ur1) \
instance Num somety where \
  (+) = br1 (+) "+"; \
  {-# INLINE (+) #-}; \
  (-) = br1 (-) "-"; \
  {-# INLINE (-) #-}; \
  (*) = br1 (*) "*"; \
  {-# INLINE (*) #-}; \
  negate = ur1 negate "negate"; \
  {-# INLINE negate #-}; \
  abs = ur1 abs "abs"; \
  {-# INLINE abs #-}; \
  signum = ur1 signum "signum"; \
  {-# INLINE signum #-}; \
  fromInteger = error "fromInteger is not defined for SomeSymWordN as no bitwidth is known"; \
  {-# INLINE fromInteger #-}

#if 1
NUM_BV(SymIntN)
NUM_BV(SymWordN)
NUM_SOME_BV(SomeSymWordN, binSomeSymWordNR1, unarySomeSymWordNR1)
NUM_SOME_BV(SomeSymIntN, binSomeSymIntNR1, unarySomeSymIntNR1)
#endif

instance Num SymInteger where
  (SymInteger Term Integer
l) + :: SymInteger -> SymInteger -> SymInteger
+ (SymInteger Term Integer
r) = Term Integer -> SymInteger
SymInteger (Term Integer -> SymInteger) -> Term Integer -> SymInteger
forall a b. (a -> b) -> a -> b
$ Term Integer -> Term Integer -> Term Integer
forall a. (Num a, SupportedPrim a) => Term a -> Term a -> Term a
pevalAddNumTerm Term Integer
l Term Integer
r
  (SymInteger Term Integer
l) - :: SymInteger -> SymInteger -> SymInteger
- (SymInteger Term Integer
r) = Term Integer -> SymInteger
SymInteger (Term Integer -> SymInteger) -> Term Integer -> SymInteger
forall a b. (a -> b) -> a -> b
$ Term Integer -> Term Integer -> Term Integer
forall a. (Num a, SupportedPrim a) => Term a -> Term a -> Term a
pevalMinusNumTerm Term Integer
l Term Integer
r
  (SymInteger Term Integer
l) * :: SymInteger -> SymInteger -> SymInteger
* (SymInteger Term Integer
r) = Term Integer -> SymInteger
SymInteger (Term Integer -> SymInteger) -> Term Integer -> SymInteger
forall a b. (a -> b) -> a -> b
$ Term Integer -> Term Integer -> Term Integer
forall a. (Num a, SupportedPrim a) => Term a -> Term a -> Term a
pevalTimesNumTerm Term Integer
l Term Integer
r
  negate :: SymInteger -> SymInteger
negate (SymInteger Term Integer
v) = Term Integer -> SymInteger
SymInteger (Term Integer -> SymInteger) -> Term Integer -> SymInteger
forall a b. (a -> b) -> a -> b
$ Term Integer -> Term Integer
forall a. (Num a, SupportedPrim a) => Term a -> Term a
pevalUMinusNumTerm Term Integer
v
  abs :: SymInteger -> SymInteger
abs (SymInteger Term Integer
v) = Term Integer -> SymInteger
SymInteger (Term Integer -> SymInteger) -> Term Integer -> SymInteger
forall a b. (a -> b) -> a -> b
$ Term Integer -> Term Integer
forall a. (SupportedPrim a, Num a) => Term a -> Term a
pevalAbsNumTerm Term Integer
v
  signum :: SymInteger -> SymInteger
signum (SymInteger Term Integer
v) = Term Integer -> SymInteger
SymInteger (Term Integer -> SymInteger) -> Term Integer -> SymInteger
forall a b. (a -> b) -> a -> b
$ Term Integer -> Term Integer
forall a. (Num a, SupportedPrim a) => Term a -> Term a
pevalSignumNumTerm Term Integer
v
  fromInteger :: Integer -> SymInteger
fromInteger = Integer -> SymInteger
forall c t. Solvable c t => c -> t
con

-- Bits

#define BITS_BV(symtype, signed) \
instance (KnownNat n, 1 <= n) => Bits (symtype n) where \
  symtype l .&. symtype r = symtype $ pevalAndBitsTerm l r; \
  {-# INLINE (.&.) #-}; \
  symtype l .|. symtype r = symtype $ pevalOrBitsTerm l r; \
  {-# INLINE (.|.) #-}; \
  symtype l `xor` symtype r = symtype $ pevalXorBitsTerm l r; \
  {-# INLINE xor #-}; \
  complement (symtype n) = symtype $ pevalComplementBitsTerm n; \
  {-# INLINE complement #-}; \
  shift (symtype n) i | i > 0 = symtype $ pevalShiftLeftTerm n (conTerm $ fromIntegral i); \
  shift (symtype n) i | i < 0 = symtype $ pevalShiftRightTerm n (conTerm $ fromIntegral (-i)); \
  shift (symtype n) _ = symtype n; \
  {-# INLINE shift #-}; \
  rotate (symtype n) i | i > 0 = symtype $ pevalRotateLeftTerm n (conTerm $ fromIntegral i); \
  rotate (symtype n) i | i < 0 = symtype $ pevalRotateRightTerm n (conTerm $ fromIntegral (-i)); \
  rotate (symtype n) _ = symtype n; \
  {-# INLINE rotate #-}; \
  bitSize = finiteBitSize; \
  {-# INLINE bitSize #-}; \
  bitSizeMaybe = Just . finiteBitSize; \
  {-# INLINE bitSizeMaybe #-}; \
  isSigned _ = signed; \
  {-# INLINE isSigned #-}; \
  testBit (Con n) =  testBit n; \
  testBit _ = error "You cannot call testBit on symbolic variables"; \
  {-# INLINE testBit #-}; \
  bit = con . bit; \
  {-# INLINE bit #-}; \
  popCount (Con n) = popCount n; \
  popCount _ = error "You cannot call popCount on symbolic variables"; \
  {-# INLINE popCount #-}

#define BITS_BV_SOME(somety, origty, br1, uf, ur1) \
instance Bits somety where \
  (.&.) = br1 (.&.) ".&."; \
  {-# INLINE (.&.) #-}; \
  (.|.) = br1 (.|.) ".|."; \
  {-# INLINE (.|.) #-}; \
  xor = br1 xor "xor"; \
  {-# INLINE xor #-}; \
  complement = ur1 complement "complement"; \
  {-# INLINE complement #-}; \
  shift s i = ur1 (`shift` i) "shift" s; \
  {-# INLINE shift #-}; \
  rotate s i = ur1 (`rotate` i) "rotate" s; \
  {-# INLINE rotate #-}; \
  zeroBits = error ("zeroBits is not defined for " ++ show (typeRep (Proxy @somety)) ++ " as no bitwidth is known"); \
  {-# INLINE zeroBits #-}; \
  bit = error ("bit is not defined for " ++ show (typeRep (Proxy @somety)) ++ " as no bitwidth is known"); \
  {-# INLINE bit #-}; \
  setBit s i = ur1 (`setBit` i) "setBit" s; \
  {-# INLINE setBit #-}; \
  clearBit s i = ur1 (`clearBit` i) "clearBit" s; \
  {-# INLINE clearBit #-}; \
  complementBit s i = ur1 (`complementBit` i) "complementBit" s; \
  {-# INLINE complementBit #-}; \
  testBit s i = uf (`testBit` i) "testBit" s; \
  {-# INLINE testBit #-}; \
  bitSizeMaybe = Just . finiteBitSize; \
  {-# INLINE bitSizeMaybe #-}; \
  bitSize = finiteBitSize; \
  {-# INLINE bitSize #-}; \
  isSigned _ = False; \
  {-# INLINE isSigned #-}; \
  shiftL s i = ur1 (`shiftL` i) "shiftL" s; \
  {-# INLINE shiftL #-}; \
  unsafeShiftL s i = ur1 (`unsafeShiftL` i) "unsafeShiftL" s; \
  {-# INLINE unsafeShiftL #-}; \
  shiftR s i = ur1 (`shiftR` i) "shiftR" s; \
  {-# INLINE shiftR #-}; \
  unsafeShiftR s i = ur1 (`unsafeShiftR` i) "unsafeShiftR" s; \
  {-# INLINE unsafeShiftR #-}; \
  rotateL s i = ur1 (`rotateL` i) "rotateL" s; \
  {-# INLINE rotateL #-}; \
  rotateR s i = ur1 (`rotateR` i) "rotateR" s; \
  {-# INLINE rotateR #-}; \
  popCount = uf popCount "popCount"; \
  {-# INLINE popCount #-}

#if 1
BITS_BV(SymIntN, True)
BITS_BV(SymWordN, False)
BITS_BV_SOME(SomeSymIntN, SymIntN, binSomeSymIntNR1, unarySomeSymIntN, unarySomeSymIntNR1)
BITS_BV_SOME(SomeSymWordN, SymWordN, binSomeSymWordNR1, unarySomeSymWordN, unarySomeSymWordNR1)
#endif

-- FiniteBits

#define FINITE_BITS_BV(symtype) \
instance (KnownNat n, 1 <= n) => FiniteBits (symtype n) where \
  finiteBitSize _ = fromIntegral $ natVal (Proxy @n); \
  {-# INLINE finiteBitSize #-}; \

#define FINITE_BITS_BV_SOME(somety, origty) \
instance FiniteBits somety where \
  finiteBitSize (somety (n :: origty n)) = fromIntegral $ natVal n; \
  {-# INLINE finiteBitSize #-}

#if 1
FINITE_BITS_BV(SymIntN)
FINITE_BITS_BV(SymWordN)
FINITE_BITS_BV_SOME(SomeSymIntN, SymIntN)
FINITE_BITS_BV_SOME(SomeSymWordN, SymWordN)
#endif

-- Show

#define SHOW_SIMPLE(symtype) \
instance Show symtype where \
  show (symtype t) = pformat t

#define SHOW_BV(symtype) \
instance (KnownNat n, 1 <= n) => Show (symtype n) where \
  show (symtype t) = pformat t

#define SHOW_FUN(op, cons) \
instance (SupportedPrim ca, SupportedPrim cb, LinkedRep ca sa, LinkedRep cb sb) => Show (sa op sb) where \
  show (cons t) = pformat t

#define SHOW_BV_SOME(somety) \
instance Show somety where \
  show (somety t) = show t

#if 1
SHOW_SIMPLE(SymBool)
SHOW_SIMPLE(SymInteger)
SHOW_BV(SymIntN)
SHOW_BV(SymWordN)
SHOW_FUN(=~>, SymTabularFun)
SHOW_FUN(-~>, SymGeneralFun)
SHOW_BV_SOME(SomeSymIntN)
SHOW_BV_SOME(SomeSymWordN)
#endif

-- Hashable

#define HASHABLE_SIMPLE(symtype) \
instance Hashable symtype where \
  hashWithSalt s (symtype v) = s `hashWithSalt` v

#define HASHABLE_BV(symtype) \
instance (KnownNat n, 1 <= n) => Hashable (symtype n) where \
  hashWithSalt s (symtype v) = s `hashWithSalt` v

#define HASHABLE_FUN(op, cons) \
instance (SupportedPrim ca, SupportedPrim cb, LinkedRep ca sa, LinkedRep cb sb) => Hashable (sa op sb) where \
  hashWithSalt s (cons v) = s `hashWithSalt` v

#define HASHABLE_BV_SOME(somety, origty) \
instance Hashable somety where \
  s `hashWithSalt` (somety (w :: origty n)) = s `hashWithSalt` natVal (Proxy @n) `hashWithSalt` w

#if 1
HASHABLE_SIMPLE(SymBool)
HASHABLE_SIMPLE(SymInteger)
HASHABLE_BV(SymIntN)
HASHABLE_BV(SymWordN)
HASHABLE_FUN(=~>, SymTabularFun)
HASHABLE_FUN(-~>, SymGeneralFun)
HASHABLE_BV_SOME(SomeSymIntN, SymIntN)
HASHABLE_BV_SOME(SomeSymWordN, SymWordNInt
)
#endif

-- Eq

#define EQ_SIMPLE(symtype) \
instance Eq symtype where \
  (symtype l) == (symtype r) = l == r

#define EQ_BV(symtype) \
instance (KnownNat n, 1 <= n) => Eq (symtype n) where \
  (symtype l) == (symtype r) = l == r

#define EQ_BV_SOME(symtype, bf) \
instance Eq symtype where; \
  (==) = bf (==) "=="; \
  {-# INLINE (==) #-}; \
  (/=) = bf (/=) "/="; \
  {-# INLINE (/=) #-}

#define EQ_FUN(op, cons) \
instance (SupportedPrim ca, SupportedPrim cb, LinkedRep ca sa, LinkedRep cb sb) => Eq (sa op sb) where \
  (cons l) == (cons r) = l == r

#if 1
EQ_SIMPLE(SymBool)
EQ_SIMPLE(SymInteger)
EQ_BV(SymIntN)
EQ_BV(SymWordN)
EQ_FUN(=~>, SymTabularFun)
EQ_FUN(-~>, SymGeneralFun)
EQ_BV_SOME(SomeSymIntN, binSomeSymIntN)
EQ_BV_SOME(SomeSymWordN, binSomeSymWordN)
#endif

-- IsString

#define IS_STRING_SIMPLE(symtype) \
instance IsString symtype where \
  fromString = ssym . fromString

#define IS_STRING_BV(symtype) \
instance (KnownNat n, 1 <= n) => IsString (symtype n) where \
  fromString = ssym . fromString

#define IS_STRING_FUN(op, cons) \
instance (SupportedPrim ca, SupportedPrim cb, LinkedRep ca sa, LinkedRep cb sb) => IsString (sa op sb) where \
  fromString = ssym . fromString

#if 1
IS_STRING_SIMPLE(SymBool)
IS_STRING_SIMPLE(SymInteger)
IS_STRING_BV(SymIntN)
IS_STRING_BV(SymWordN)
IS_STRING_FUN(=~>, SymTabularFunc)
IS_STRING_FUN(-~>, SymGeneralFun)
#endif

-- SizedBV

#define BVCONCAT_SIZED(symtype) \
sizedBVConcat :: forall l r. (KnownNat l, KnownNat r, 1 <= l, 1 <= r) => symtype l -> symtype r -> symtype (l + r); \
sizedBVConcat (symtype l) (symtype r) = \
  case (leqAddPos pl pr, knownAdd (KnownProof @l) (KnownProof @r)) of \
    (LeqProof, KnownProof) -> \
      symtype (pevalBVConcatTerm l r); \
  where; \
    pl = Proxy :: Proxy l; \
    pr = Proxy :: Proxy r

#define BVZEXT_SIZED(symtype) \
sizedBVZext :: forall l r proxy. (KnownNat l, KnownNat r, 1 <= l, KnownNat r, l <= r) => proxy r -> symtype l -> symtype r; \
sizedBVZext _ (symtype v) = \
  case leqTrans (LeqProof @1 @l) (LeqProof @l @r) of \
    LeqProof -> symtype $ pevalBVExtendTerm False (Proxy @r) v

#define BVSEXT_SIZED(symtype) \
sizedBVSext :: forall l r proxy. (KnownNat l, KnownNat r, 1 <= l, KnownNat r, l <= r) => proxy r -> symtype l -> symtype r; \
sizedBVSext _ (symtype v) = \
  case leqTrans (LeqProof @1 @l) (LeqProof @l @r) of \
    LeqProof -> symtype $ pevalBVExtendTerm True (Proxy @r) v

#define BVSELECT_SIZED(symtype) \
sizedBVSelect :: forall n ix w p q. (KnownNat n, KnownNat ix, KnownNat w, 1 <= n, 1 <= w, ix + w <= n) => \
  p ix -> q w -> symtype n -> symtype w; \
sizedBVSelect pix pw (symtype v) = symtype $ pevalBVSelectTerm pix pw v

#if 1
instance SizedBV SymIntN where
  BVCONCAT_SIZED(SymIntN)
  BVZEXT_SIZED(SymIntN)
  BVSEXT_SIZED(SymIntN)
  sizedBVExt :: forall (l :: Nat) (r :: Nat) (proxy :: Nat -> *).
(KnownNat l, KnownNat r, 1 <= l, KnownNat r, l <= r) =>
proxy r -> SymIntN l -> SymIntN r
sizedBVExt = proxy r -> SymIntN l -> SymIntN r
forall (l :: Nat) (r :: Nat) (proxy :: Nat -> *).
(KnownNat l, KnownNat r, 1 <= l, KnownNat r, l <= r) =>
proxy r -> SymIntN l -> SymIntN r
forall (bv :: Nat -> *) (l :: Nat) (r :: Nat) (proxy :: Nat -> *).
(SizedBV bv, KnownNat l, KnownNat r, 1 <= l, KnownNat r, l <= r) =>
proxy r -> bv l -> bv r
sizedBVSext
  BVSELECT_SIZED(SymIntN)

instance SizedBV SymWordN where
  BVCONCAT_SIZED(SymWordN)
  BVZEXT_SIZED(SymWordN)
  BVSEXT_SIZED(SymWordN)
  sizedBVExt :: forall (l :: Nat) (r :: Nat) (proxy :: Nat -> *).
(KnownNat l, KnownNat r, 1 <= l, KnownNat r, l <= r) =>
proxy r -> SymWordN l -> SymWordN r
sizedBVExt = proxy r -> SymWordN l -> SymWordN r
forall (l :: Nat) (r :: Nat) (proxy :: Nat -> *).
(KnownNat l, KnownNat r, 1 <= l, KnownNat r, l <= r) =>
proxy r -> SymWordN l -> SymWordN r
forall (bv :: Nat -> *) (l :: Nat) (r :: Nat) (proxy :: Nat -> *).
(SizedBV bv, KnownNat l, KnownNat r, 1 <= l, KnownNat r, l <= r) =>
proxy r -> bv l -> bv r
sizedBVZext
  BVSELECT_SIZED(SymWordN)
#endif

-- BV

#define BVCONCAT(somety, origty) \
bvConcat (somety (a :: origty l)) (somety (b :: origty r)) = \
  case (leqAddPos (Proxy @l) (Proxy @r), knownAdd @l @r KnownProof KnownProof) of \
    (LeqProof, KnownProof) -> \
      somety $ sizedBVConcat a b

#define BVZEXT(somety, origty) \
bvZext l (somety (a :: origty n)) \
  | l < n = error "bvZext: trying to zero extend a value to a smaller size" \
  | otherwise = res (Proxy @n) \
  where \
    n = fromIntegral $ natVal (Proxy @n); \
    res :: forall (l :: Nat). Proxy l -> somety; \
    res p = \
      case (unsafeKnownProof @l (fromIntegral l), unsafeLeqProof @1 @l, unsafeLeqProof @n @l) of \
        (KnownProof, LeqProof, LeqProof) -> somety $ sizedBVZext p a

#define BVSEXT(somety, origty) \
bvSext l (somety (a :: origty n)) \
  | l < n = error "bvZext: trying to zero extend a value to a smaller size" \
  | otherwise = res (Proxy @n) \
  where \
    n = fromIntegral $ natVal (Proxy @n); \
    res :: forall (l :: Nat). Proxy l -> somety; \
    res p = \
      case (unsafeKnownProof @l (fromIntegral l), unsafeLeqProof @1 @l, unsafeLeqProof @n @l) of \
        (KnownProof, LeqProof, LeqProof) -> somety $ sizedBVSext p a

#define BVSELECT(somety, origty) \
bvSelect ix w (somety (a :: origty n)) \
    | ix + w > n = error "bvSelect: trying to select a bitvector outside the bounds of the input" \
    | w == 0 = error "bvSelect: trying to select a bitvector of size 0" \
    | otherwise = res (Proxy @n) (Proxy @n) \
    where \
      n = fromIntegral $ natVal (Proxy @n); \
      res :: forall (w :: Nat) (ix :: Nat). Proxy w -> Proxy ix -> somety; \
      res _ _ = \
        case ( unsafeKnownProof @ix (fromIntegral ix), \
               unsafeKnownProof @w (fromIntegral w), \
               unsafeLeqProof @1 @w, \
               unsafeLeqProof @(ix + w) @n \
             ) of \
          (KnownProof, KnownProof, LeqProof, LeqProof) -> \
            somety $ sizedBVSelect (Proxy @ix) (Proxy @w) a

#if 1
instance BV SomeSymIntN where
  bvConcat :: SomeSymIntN -> SomeSymIntN -> SomeSymIntN
BVCONCAT(SomeSymIntN, SymIntN)
  {-# INLINE bvConcat #-}
  bvZext :: Int -> SomeSymIntN -> SomeSymIntN
BVZEXT(SomeSymIntN, SymIntN)
  {-# INLINE bvZext #-}
  bvSext :: Int -> SomeSymIntN -> SomeSymIntN
BVSEXT(SomeSymIntN, SymIntN)
  {-# INLINE bvSext #-}
  bvExt :: Int -> SomeSymIntN -> SomeSymIntN
bvExt = Int -> SomeSymIntN -> SomeSymIntN
forall bv. BV bv => Int -> bv -> bv
bvSext
  {-# INLINE bvExt #-}
  bvSelect :: Int -> Int -> SomeSymIntN -> SomeSymIntN
BVSELECT(SomeSymIntN, SymIntN)
  {-# INLINE bvSelect #-}

instance BV SomeSymWordN where
  bvConcat :: SomeSymWordN -> SomeSymWordN -> SomeSymWordN
BVCONCAT(SomeSymWordN, SymWordN)
  {-# INLINE bvConcat #-}
  bvZext :: Int -> SomeSymWordN -> SomeSymWordN
BVZEXT(SomeSymWordN, SymWordN)
  {-# INLINE bvZext #-}
  bvSext :: Int -> SomeSymWordN -> SomeSymWordN
BVSEXT(SomeSymWordN, SymWordN)
  {-# INLINE bvSext #-}
  bvExt :: Int -> SomeSymWordN -> SomeSymWordN
bvExt = Int -> SomeSymWordN -> SomeSymWordN
forall bv. BV bv => Int -> bv -> bv
bvZext
  {-# INLINE bvExt #-}
  bvSelect :: Int -> Int -> SomeSymWordN -> SomeSymWordN
BVSELECT(SomeSymWordN, SymWordN)
  {-# INLINE bvSelect #-}
#endif

-- BVSignConversion

instance (KnownNat n, 1 <= n) => SignConversion (SymWordN n) (SymIntN n) where
  toSigned :: SymWordN n -> SymIntN n
toSigned (SymWordN Term (WordN n)
n) = Term (IntN n) -> SymIntN n
forall (n :: Nat). Term (IntN n) -> SymIntN n
SymIntN (Term (IntN n) -> SymIntN n) -> Term (IntN n) -> SymIntN n
forall a b. (a -> b) -> a -> b
$ Term (WordN n) -> Term (IntN n)
forall u s.
(SupportedPrim u, SupportedPrim s, SignConversion u s) =>
Term u -> Term s
pevalToSignedTerm Term (WordN n)
n
  toUnsigned :: SymIntN n -> SymWordN n
toUnsigned (SymIntN Term (IntN n)
n) = Term (WordN n) -> SymWordN n
forall (n :: Nat). Term (WordN n) -> SymWordN n
SymWordN (Term (WordN n) -> SymWordN n) -> Term (WordN n) -> SymWordN n
forall a b. (a -> b) -> a -> b
$ Term (IntN n) -> Term (WordN n)
forall u s.
(SupportedPrim u, SupportedPrim s, SignConversion u s) =>
Term s -> Term u
pevalToUnsignedTerm Term (IntN n)
n

instance SignConversion SomeSymWordN SomeSymIntN where
  toSigned :: SomeSymWordN -> SomeSymIntN
toSigned (SomeSymWordN SymWordN n
n) = SymIntN n -> SomeSymIntN
forall (con :: Nat).
(KnownNat con, 1 <= con) =>
SymIntN con -> SomeSymIntN
SomeSymIntN (SymIntN n -> SomeSymIntN) -> SymIntN n -> SomeSymIntN
forall a b. (a -> b) -> a -> b
$ SymWordN n -> SymIntN n
forall ubv sbv. SignConversion ubv sbv => ubv -> sbv
toSigned SymWordN n
n
  toUnsigned :: SomeSymIntN -> SomeSymWordN
toUnsigned (SomeSymIntN SymIntN n
n) = SymWordN n -> SomeSymWordN
forall (con :: Nat).
(KnownNat con, 1 <= con) =>
SymWordN con -> SomeSymWordN
SomeSymWordN (SymWordN n -> SomeSymWordN) -> SymWordN n -> SomeSymWordN
forall a b. (a -> b) -> a -> b
$ SymIntN n -> SymWordN n
forall ubv sbv. SignConversion ubv sbv => sbv -> ubv
toUnsigned SymIntN n
n

-- SymShift
instance (KnownNat n, 1 <= n) => SymShift (SymWordN n) where
  symShift :: SymWordN n -> SymWordN n -> SymWordN n
symShift (SymWordN Term (WordN n)
a) (SymWordN Term (WordN n)
s) = Term (WordN n) -> SymWordN n
forall (n :: Nat). Term (WordN n) -> SymWordN n
SymWordN (Term (WordN n) -> SymWordN n) -> Term (WordN n) -> SymWordN n
forall a b. (a -> b) -> a -> b
$ Term (WordN n) -> Term (WordN n) -> Term (WordN n)
forall a.
(Integral a, SymShift a, FiniteBits a, SupportedPrim a) =>
Term a -> Term a -> Term a
pevalShiftLeftTerm Term (WordN n)
a Term (WordN n)
s

instance (KnownNat n, 1 <= n) => SymShift (SymIntN n) where
  symShift :: SymIntN n -> SymIntN n -> SymIntN n
symShift SymIntN n
a SymIntN n
_ | SymIntN n -> Int
forall b. FiniteBits b => b -> Int
finiteBitSize SymIntN n
a Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
1 = SymIntN n
a
  symShift as :: SymIntN n
as@(SymIntN Term (IntN n)
a) (SymIntN Term (IntN n)
s)
    | SymIntN n -> Int
forall b. FiniteBits b => b -> Int
finiteBitSize SymIntN n
as Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
2 =
        Term (IntN n) -> SymIntN n
forall (n :: Nat). Term (IntN n) -> SymIntN n
SymIntN (Term (IntN n) -> SymIntN n) -> Term (IntN n) -> SymIntN n
forall a b. (a -> b) -> a -> b
$
          Term Bool -> Term (IntN n) -> Term (IntN n) -> Term (IntN n)
forall a.
SupportedPrim a =>
Term Bool -> Term a -> Term a -> Term a
pevalITETerm
            (Term (IntN n) -> Term (IntN n) -> Term Bool
forall a.
(Num a, Ord a, SupportedPrim a) =>
Term a -> Term a -> Term Bool
pevalGeNumTerm Term (IntN n)
s (IntN n -> Term (IntN n)
forall t.
(SupportedPrim t, Typeable t, Hashable t, Eq t, Show t) =>
t -> Term t
conTerm IntN n
0))
            (Term (IntN n) -> Term (IntN n) -> Term (IntN n)
forall a.
(Integral a, SymShift a, FiniteBits a, SupportedPrim a) =>
Term a -> Term a -> Term a
pevalShiftLeftTerm Term (IntN n)
a Term (IntN n)
s)
            ( Term Bool -> Term (IntN n) -> Term (IntN n) -> Term (IntN n)
forall a.
SupportedPrim a =>
Term Bool -> Term a -> Term a -> Term a
pevalITETerm
                (Term (IntN n) -> Term (IntN n) -> Term Bool
forall a. SupportedPrim a => Term a -> Term a -> Term Bool
pevalEqvTerm Term (IntN n)
s (IntN n -> Term (IntN n)
forall t.
(SupportedPrim t, Typeable t, Hashable t, Eq t, Show t) =>
t -> Term t
conTerm (-IntN n
2)))
                ( Term Bool -> Term (IntN n) -> Term (IntN n) -> Term (IntN n)
forall a.
SupportedPrim a =>
Term Bool -> Term a -> Term a -> Term a
pevalITETerm
                    (Term (IntN n) -> Term (IntN n) -> Term Bool
forall a.
(Num a, Ord a, SupportedPrim a) =>
Term a -> Term a -> Term Bool
pevalGeNumTerm Term (IntN n)
a (IntN n -> Term (IntN n)
forall t.
(SupportedPrim t, Typeable t, Hashable t, Eq t, Show t) =>
t -> Term t
conTerm IntN n
0))
                    (IntN n -> Term (IntN n)
forall t.
(SupportedPrim t, Typeable t, Hashable t, Eq t, Show t) =>
t -> Term t
conTerm IntN n
0)
                    (IntN n -> Term (IntN n)
forall t.
(SupportedPrim t, Typeable t, Hashable t, Eq t, Show t) =>
t -> Term t
conTerm (-IntN n
1))
                )
                (Term (IntN n) -> Term (IntN n) -> Term (IntN n)
forall a.
(Integral a, SymShift a, FiniteBits a, SupportedPrim a) =>
Term a -> Term a -> Term a
pevalShiftRightTerm Term (IntN n)
a (Term (IntN n) -> Term (IntN n)
forall a. (Num a, SupportedPrim a) => Term a -> Term a
pevalUMinusNumTerm Term (IntN n)
s))
            )
  symShift (SymIntN Term (IntN n)
a) (SymIntN Term (IntN n)
s) =
    Term (IntN n) -> SymIntN n
forall (n :: Nat). Term (IntN n) -> SymIntN n
SymIntN (Term (IntN n) -> SymIntN n) -> Term (IntN n) -> SymIntN n
forall a b. (a -> b) -> a -> b
$
      Term Bool -> Term (IntN n) -> Term (IntN n) -> Term (IntN n)
forall a.
SupportedPrim a =>
Term Bool -> Term a -> Term a -> Term a
pevalITETerm
        (Term (IntN n) -> Term (IntN n) -> Term Bool
forall a.
(Num a, Ord a, SupportedPrim a) =>
Term a -> Term a -> Term Bool
pevalGeNumTerm Term (IntN n)
s (IntN n -> Term (IntN n)
forall t.
(SupportedPrim t, Typeable t, Hashable t, Eq t, Show t) =>
t -> Term t
conTerm IntN n
0))
        (Term (IntN n) -> Term (IntN n) -> Term (IntN n)
forall a.
(Integral a, SymShift a, FiniteBits a, SupportedPrim a) =>
Term a -> Term a -> Term a
pevalShiftLeftTerm Term (IntN n)
a Term (IntN n)
s)
        ( Term Bool -> Term (IntN n) -> Term (IntN n) -> Term (IntN n)
forall a.
SupportedPrim a =>
Term Bool -> Term a -> Term a -> Term a
pevalITETerm
            (Term (IntN n) -> Term (IntN n) -> Term Bool
forall a.
(Num a, Ord a, SupportedPrim a) =>
Term a -> Term a -> Term Bool
pevalLeNumTerm Term (IntN n)
s (IntN n -> Term (IntN n)
forall t.
(SupportedPrim t, Typeable t, Hashable t, Eq t, Show t) =>
t -> Term t
conTerm (-IntN n
bs)))
            (Term (IntN n) -> Term (IntN n) -> Term (IntN n)
forall a.
(Integral a, SymShift a, FiniteBits a, SupportedPrim a) =>
Term a -> Term a -> Term a
pevalShiftRightTerm Term (IntN n)
a (IntN n -> Term (IntN n)
forall t.
(SupportedPrim t, Typeable t, Hashable t, Eq t, Show t) =>
t -> Term t
conTerm IntN n
bs))
            (Term (IntN n) -> Term (IntN n) -> Term (IntN n)
forall a.
(Integral a, SymShift a, FiniteBits a, SupportedPrim a) =>
Term a -> Term a -> Term a
pevalShiftRightTerm Term (IntN n)
a (Term (IntN n) -> Term (IntN n)
forall a. (Num a, SupportedPrim a) => Term a -> Term a
pevalUMinusNumTerm Term (IntN n)
s))
        )
    where
      bs :: IntN n
bs = Int -> IntN n
forall a b. (Integral a, Num b) => a -> b
fromIntegral (IntN n -> Int
forall b. FiniteBits b => b -> Int
finiteBitSize (IntN n
0 :: IntN n)) :: IntN n

-- SymRotate
instance (KnownNat n, 1 <= n) => SymRotate (SymWordN n) where
  symRotate :: SymWordN n -> SymWordN n -> SymWordN n
symRotate (SymWordN Term (WordN n)
a) (SymWordN Term (WordN n)
s) = Term (WordN n) -> SymWordN n
forall (n :: Nat). Term (WordN n) -> SymWordN n
SymWordN (Term (WordN n) -> Term (WordN n) -> Term (WordN n)
forall a.
(Integral a, SymRotate a, FiniteBits a, SupportedPrim a) =>
Term a -> Term a -> Term a
pevalRotateLeftTerm Term (WordN n)
a Term (WordN n)
s)

instance (KnownNat n, 1 <= n) => SymRotate (SymIntN n) where
  symRotate :: SymIntN n -> SymIntN n -> SymIntN n
symRotate SymIntN n
a SymIntN n
_ | SymIntN n -> Int
forall b. FiniteBits b => b -> Int
finiteBitSize SymIntN n
a Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
1 = SymIntN n
a
  symRotate as :: SymIntN n
as@(SymIntN Term (IntN n)
a) (SymIntN Term (IntN n)
s)
    | SymIntN n -> Int
forall b. FiniteBits b => b -> Int
finiteBitSize SymIntN n
as Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
2 =
        Term (IntN n) -> SymIntN n
forall (n :: Nat). Term (IntN n) -> SymIntN n
SymIntN (Term (IntN n) -> SymIntN n) -> Term (IntN n) -> SymIntN n
forall a b. (a -> b) -> a -> b
$
          Term Bool -> Term (IntN n) -> Term (IntN n) -> Term (IntN n)
forall a.
SupportedPrim a =>
Term Bool -> Term a -> Term a -> Term a
pevalITETerm
            ( Term Bool -> Term Bool -> Term Bool
pevalOrTerm
                (Term (IntN n) -> Term (IntN n) -> Term Bool
forall a. SupportedPrim a => Term a -> Term a -> Term Bool
pevalEqvTerm Term (IntN n)
s (IntN n -> Term (IntN n)
forall t.
(SupportedPrim t, Typeable t, Hashable t, Eq t, Show t) =>
t -> Term t
conTerm IntN n
0))
                (Term (IntN n) -> Term (IntN n) -> Term Bool
forall a. SupportedPrim a => Term a -> Term a -> Term Bool
pevalEqvTerm Term (IntN n)
s (IntN n -> Term (IntN n)
forall t.
(SupportedPrim t, Typeable t, Hashable t, Eq t, Show t) =>
t -> Term t
conTerm (-IntN n
2)))
            )
            Term (IntN n)
a
            (Term (IntN n) -> Term (IntN n) -> Term (IntN n)
forall a.
(Integral a, SymRotate a, FiniteBits a, SupportedPrim a) =>
Term a -> Term a -> Term a
pevalRotateLeftTerm Term (IntN n)
a (IntN n -> Term (IntN n)
forall t.
(SupportedPrim t, Typeable t, Hashable t, Eq t, Show t) =>
t -> Term t
conTerm IntN n
1))
  symRotate as :: SymIntN n
as@(SymIntN Term (IntN n)
a) (SymIntN Term (IntN n)
s) =
    Term (IntN n) -> SymIntN n
forall (n :: Nat). Term (IntN n) -> SymIntN n
SymIntN (Term (IntN n) -> SymIntN n) -> Term (IntN n) -> SymIntN n
forall a b. (a -> b) -> a -> b
$
      Term (IntN n) -> Term (IntN n) -> Term (IntN n)
forall a.
(Integral a, SymRotate a, FiniteBits a, SupportedPrim a) =>
Term a -> Term a -> Term a
pevalRotateLeftTerm
        Term (IntN n)
a
        ( Term (IntN n) -> Term (IntN n) -> Term (IntN n)
forall a.
(SupportedPrim a, Integral a) =>
Term a -> Term a -> Term a
pevalModBoundedIntegralTerm
            Term (IntN n)
s
            (IntN n -> Term (IntN n)
forall t.
(SupportedPrim t, Typeable t, Hashable t, Eq t, Show t) =>
t -> Term t
conTerm (Int -> IntN n
forall a b. (Integral a, Num b) => a -> b
fromIntegral (Int -> IntN n) -> Int -> IntN n
forall a b. (a -> b) -> a -> b
$ SymIntN n -> Int
forall b. FiniteBits b => b -> Int
finiteBitSize SymIntN n
as))
        )

-- ModelRep

-- | A pair of a symbolic constant and its value.
-- This is used to build a model from a list of symbolic constants and their values.
--
-- >>> buildModel ("a" := (1 :: Integer), "b" := True) :: Model
-- Model {a -> 1 :: Integer, b -> True :: Bool}
data ModelSymPair ct st where
  (:=) :: (LinkedRep ct st) => st -> ct -> ModelSymPair ct st

instance ModelRep (ModelSymPair ct st) Model where
  buildModel :: ModelSymPair ct st -> Model
buildModel (st
sym := ct
val) =
    case st -> Term ct
forall con sym. LinkedRep con sym => sym -> Term con
underlyingTerm st
sym of
      SymTerm Int
_ TypedSymbol ct
symbol -> TypedSymbol ct -> ct -> Model -> Model
forall t. TypedSymbol t -> t -> Model -> Model
forall model symbolSet (typedSymbol :: * -> *) t.
ModelOps model symbolSet typedSymbol =>
typedSymbol t -> t -> model -> model
insertValue TypedSymbol ct
symbol ct
val Model
forall model symbolSet (typedSymbol :: * -> *).
ModelOps model symbolSet typedSymbol =>
model
emptyModel
      Term ct
_ -> String -> Model
forall a. HasCallStack => String -> a
error String
"buildModel: should only use symbolic constants"

-- | Get the sum of the sizes of a list of symbolic terms.
-- Duplicate sub-terms are counted for only once.
--
-- >>> symsSize [1, "a" :: SymInteger, "a" + 1 :: SymInteger]
-- 3
symsSize :: forall con sym. (LinkedRep con sym) => [sym] -> Int
symsSize :: forall con sym. LinkedRep con sym => [sym] -> Int
symsSize = [Term con] -> Int
forall a. [Term a] -> Int
termsSize ([Term con] -> Int) -> ([sym] -> [Term con]) -> [sym] -> Int
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (sym -> Term con) -> [sym] -> [Term con]
forall a b. (a -> b) -> [a] -> [b]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (forall con sym. LinkedRep con sym => sym -> Term con
underlyingTerm @con)
{-# INLINE symsSize #-}

-- | Get the size of a symbolic term.
-- Duplicate sub-terms are counted for only once.
--
-- >>> symSize (1 :: SymInteger)
-- 1
-- >>> symSize ("a" :: SymInteger)
-- 1
-- >>> symSize ("a" + 1 :: SymInteger)
-- 3
-- >>> symSize (("a" + 1) * ("a" + 1) :: SymInteger)
-- 4
symSize :: forall con sym. (LinkedRep con sym) => sym -> Int
symSize :: forall con sym. LinkedRep con sym => sym -> Int
symSize = Term con -> Int
forall a. Term a -> Int
termSize (Term con -> Int) -> (sym -> Term con) -> sym -> Int
forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall con sym. LinkedRep con sym => sym -> Term con
underlyingTerm @con
{-# INLINE symSize #-}

-- | Some symbolic value with 'LinkedRep' constraint.
data SomeSym where
  SomeSym :: (LinkedRep con sym) => sym -> SomeSym

someUnderlyingTerm :: SomeSym -> SomeTerm
someUnderlyingTerm :: SomeSym -> SomeTerm
someUnderlyingTerm (SomeSym sym
s) = Term con -> SomeTerm
forall a. SupportedPrim a => Term a -> SomeTerm
SomeTerm (Term con -> SomeTerm) -> Term con -> SomeTerm
forall a b. (a -> b) -> a -> b
$ sym -> Term con
forall con sym. LinkedRep con sym => sym -> Term con
underlyingTerm sym
s

someSymsSize :: [SomeSym] -> Int
someSymsSize :: [SomeSym] -> Int
someSymsSize = [SomeTerm] -> Int
someTermsSize ([SomeTerm] -> Int)
-> ([SomeSym] -> [SomeTerm]) -> [SomeSym] -> Int
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (SomeSym -> SomeTerm) -> [SomeSym] -> [SomeTerm]
forall a b. (a -> b) -> [a] -> [b]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap SomeSym -> SomeTerm
someUnderlyingTerm
{-# INLINE someSymsSize #-}

-- | Extract all symbolic primitive values that are represented as SMT terms.
--
-- __Note:__ This type class can be derived for algebraic data types. You may
-- need the @DerivingVia@ and @DerivingStrategies@ extenstions.
--
-- > data X = ... deriving Generic deriving AllSyms via (Default X)
class AllSyms a where
  -- | Convert a value to a list of symbolic primitive values. It should
  -- prepend to an existing list of symbolic primitive values.
  allSymsS :: a -> [SomeSym] -> [SomeSym]
  allSymsS a
a [SomeSym]
l = a -> [SomeSym]
forall a. AllSyms a => a -> [SomeSym]
allSyms a
a [SomeSym] -> [SomeSym] -> [SomeSym]
forall a. [a] -> [a] -> [a]
++ [SomeSym]
l

  -- | Specialized 'allSymsS' that prepends to an empty list.
  allSyms :: a -> [SomeSym]
  allSyms a
a = a -> [SomeSym] -> [SomeSym]
forall a. AllSyms a => a -> [SomeSym] -> [SomeSym]
allSymsS a
a []

  {-# MINIMAL allSymsS | allSyms #-}

-- | Get the total size of symbolic terms in a value.
-- Duplicate sub-terms are counted for only once.
--
-- >>> allSymsSize ("a" :: SymInteger, "a" + "b" :: SymInteger, ("a" + "b") * "c" :: SymInteger)
-- 5
allSymsSize :: (AllSyms a) => a -> Int
allSymsSize :: forall a. AllSyms a => a -> Int
allSymsSize = [SomeSym] -> Int
someSymsSize ([SomeSym] -> Int) -> (a -> [SomeSym]) -> a -> Int
forall b c a. (b -> c) -> (a -> b) -> a -> c
. a -> [SomeSym]
forall a. AllSyms a => a -> [SomeSym]
allSyms

class AllSyms' a where
  allSymsS' :: a c -> [SomeSym] -> [SomeSym]

instance (Generic a, AllSyms' (Rep a)) => AllSyms (Default a) where
  allSymsS :: Default a -> [SomeSym] -> [SomeSym]
allSymsS = Rep a Any -> [SomeSym] -> [SomeSym]
forall c. Rep a c -> [SomeSym] -> [SomeSym]
forall (a :: * -> *) c. AllSyms' a => a c -> [SomeSym] -> [SomeSym]
allSymsS' (Rep a Any -> [SomeSym] -> [SomeSym])
-> (Default a -> Rep a Any) -> Default a -> [SomeSym] -> [SomeSym]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. a -> Rep a Any
forall x. a -> Rep a x
forall a x. Generic a => a -> Rep a x
from (a -> Rep a Any) -> (Default a -> a) -> Default a -> Rep a Any
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Default a -> a
forall a. Default a -> a
unDefault

instance AllSyms' U1 where
  allSymsS' :: forall c. U1 c -> [SomeSym] -> [SomeSym]
allSymsS' U1 c
_ = [SomeSym] -> [SomeSym]
forall a. a -> a
id

instance (AllSyms c) => AllSyms' (K1 i c) where
  allSymsS' :: forall c. K1 i c c -> [SomeSym] -> [SomeSym]
allSymsS' (K1 c
v) = c -> [SomeSym] -> [SomeSym]
forall a. AllSyms a => a -> [SomeSym] -> [SomeSym]
allSymsS c
v

instance (AllSyms' a) => AllSyms' (M1 i c a) where
  allSymsS' :: forall c. M1 i c a c -> [SomeSym] -> [SomeSym]
allSymsS' (M1 a c
v) = a c -> [SomeSym] -> [SomeSym]
forall c. a c -> [SomeSym] -> [SomeSym]
forall (a :: * -> *) c. AllSyms' a => a c -> [SomeSym] -> [SomeSym]
allSymsS' a c
v

instance (AllSyms' a, AllSyms' b) => AllSyms' (a :+: b) where
  allSymsS' :: forall c. (:+:) a b c -> [SomeSym] -> [SomeSym]
allSymsS' (L1 a c
l) = a c -> [SomeSym] -> [SomeSym]
forall c. a c -> [SomeSym] -> [SomeSym]
forall (a :: * -> *) c. AllSyms' a => a c -> [SomeSym] -> [SomeSym]
allSymsS' a c
l
  allSymsS' (R1 b c
r) = b c -> [SomeSym] -> [SomeSym]
forall c. b c -> [SomeSym] -> [SomeSym]
forall (a :: * -> *) c. AllSyms' a => a c -> [SomeSym] -> [SomeSym]
allSymsS' b c
r

instance (AllSyms' a, AllSyms' b) => AllSyms' (a :*: b) where
  allSymsS' :: forall c. (:*:) a b c -> [SomeSym] -> [SomeSym]
allSymsS' (a c
a :*: b c
b) = a c -> [SomeSym] -> [SomeSym]
forall c. a c -> [SomeSym] -> [SomeSym]
forall (a :: * -> *) c. AllSyms' a => a c -> [SomeSym] -> [SomeSym]
allSymsS' a c
a ([SomeSym] -> [SomeSym])
-> ([SomeSym] -> [SomeSym]) -> [SomeSym] -> [SomeSym]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. b c -> [SomeSym] -> [SomeSym]
forall c. b c -> [SomeSym] -> [SomeSym]
forall (a :: * -> *) c. AllSyms' a => a c -> [SomeSym] -> [SomeSym]
allSymsS' b c
b

#define CONCRETE_ALLSYMS(type) \
instance AllSyms type where \
  allSymsS _ = id

#define ALLSYMS_SIMPLE(t) \
instance AllSyms t where \
  allSymsS v = (SomeSym v :)

#define ALLSYMS_BV(t) \
instance (KnownNat n, 1 <= n) => AllSyms (t n) where \
  allSymsS v = (SomeSym v :)

#define ALLSYMS_SOME_BV(t) \
instance AllSyms t where \
  allSymsS (t v) = (SomeSym v :)

#define ALLSYMS_FUN(op) \
instance (SupportedPrim ca, SupportedPrim cb, LinkedRep ca sa, LinkedRep cb sb) => AllSyms (sa op sb) where \
  allSymsS v = (SomeSym v :)

#if 1
CONCRETE_ALLSYMS(Bool)
CONCRETE_ALLSYMS(Integer)
CONCRETE_ALLSYMS(Char)
CONCRETE_ALLSYMS(Int)
CONCRETE_ALLSYMS(Int8)
CONCRETE_ALLSYMS(Int16)
CONCRETE_ALLSYMS(Int32)
CONCRETE_ALLSYMS(Int64)
CONCRETE_ALLSYMS(Word)
CONCRETE_ALLSYMS(Word8)
CONCRETE_ALLSYMS(Word16)
CONCRETE_ALLSYMS(Word32)
CONCRETE_ALLSYMS(Word64)
CONCRETE_ALLSYMS(B.ByteString)
CONCRETE_ALLSYMS(T.Text)
ALLSYMS_SIMPLE(SymBool)
ALLSYMS_SIMPLE(SymInteger)
ALLSYMS_BV(SymIntN)
ALLSYMS_BV(SymWordN)
ALLSYMS_SOME_BV(SomeSymIntN)
ALLSYMS_SOME_BV(SomeSymWordN)
ALLSYMS_FUN(=~>)
ALLSYMS_FUN(-~>)
#endif

instance AllSyms () where
  allSymsS :: () -> [SomeSym] -> [SomeSym]
allSymsS ()
_ = [SomeSym] -> [SomeSym]
forall a. a -> a
id

-- Either
deriving via
  (Default (Either a b))
  instance
    ( AllSyms a,
      AllSyms b
    ) =>
    AllSyms (Either a b)

-- Maybe
deriving via (Default (Maybe a)) instance (AllSyms a) => AllSyms (Maybe a)

-- List
deriving via (Default [a]) instance (AllSyms a) => AllSyms [a]

-- (,)
deriving via
  (Default (a, b))
  instance
    (AllSyms a, AllSyms b) =>
    AllSyms (a, b)

-- (,,)
deriving via
  (Default (a, b, c))
  instance
    ( AllSyms a,
      AllSyms b,
      AllSyms c
    ) =>
    AllSyms (a, b, c)

-- (,,,)
deriving via
  (Default (a, b, c, d))
  instance
    ( AllSyms a,
      AllSyms b,
      AllSyms c,
      AllSyms d
    ) =>
    AllSyms (a, b, c, d)

-- (,,,,)
deriving via
  (Default (a, b, c, d, e))
  instance
    ( AllSyms a,
      AllSyms b,
      AllSyms c,
      AllSyms d,
      AllSyms e
    ) =>
    AllSyms (a, b, c, d, e)

-- (,,,,,)
deriving via
  (Default (a, b, c, d, e, f))
  instance
    ( AllSyms a,
      AllSyms b,
      AllSyms c,
      AllSyms d,
      AllSyms e,
      AllSyms f
    ) =>
    AllSyms (a, b, c, d, e, f)

-- (,,,,,,)
deriving via
  (Default (a, b, c, d, e, f, g))
  instance
    ( AllSyms a,
      AllSyms b,
      AllSyms c,
      AllSyms d,
      AllSyms e,
      AllSyms f,
      AllSyms g
    ) =>
    AllSyms (a, b, c, d, e, f, g)

-- (,,,,,,,)
deriving via
  (Default (a, b, c, d, e, f, g, h))
  instance
    ( AllSyms a,
      AllSyms b,
      AllSyms c,
      AllSyms d,
      AllSyms e,
      AllSyms f,
      AllSyms g,
      AllSyms h
    ) =>
    AllSyms ((,,,,,,,) a b c d e f g h)

-- MaybeT
instance
  (AllSyms (m (Maybe a))) =>
  AllSyms (MaybeT m a)
  where
  allSymsS :: MaybeT m a -> [SomeSym] -> [SomeSym]
allSymsS (MaybeT m (Maybe a)
v) = m (Maybe a) -> [SomeSym] -> [SomeSym]
forall a. AllSyms a => a -> [SomeSym] -> [SomeSym]
allSymsS m (Maybe a)
v

-- ExceptT
instance
  (AllSyms (m (Either e a))) =>
  AllSyms (ExceptT e m a)
  where
  allSymsS :: ExceptT e m a -> [SomeSym] -> [SomeSym]
allSymsS (ExceptT m (Either e a)
v) = m (Either e a) -> [SomeSym] -> [SomeSym]
forall a. AllSyms a => a -> [SomeSym] -> [SomeSym]
allSymsS m (Either e a)
v

-- Sum
deriving via
  (Default (Sum f g a))
  instance
    (AllSyms (f a), AllSyms (g a)) =>
    AllSyms (Sum f g a)

-- WriterT
instance
  (AllSyms (m (a, s))) =>
  AllSyms (WriterLazy.WriterT s m a)
  where
  allSymsS :: WriterT s m a -> [SomeSym] -> [SomeSym]
allSymsS (WriterLazy.WriterT m (a, s)
v) = m (a, s) -> [SomeSym] -> [SomeSym]
forall a. AllSyms a => a -> [SomeSym] -> [SomeSym]
allSymsS m (a, s)
v

instance
  (AllSyms (m (a, s))) =>
  AllSyms (WriterStrict.WriterT s m a)
  where
  allSymsS :: WriterT s m a -> [SomeSym] -> [SomeSym]
allSymsS (WriterStrict.WriterT m (a, s)
v) = m (a, s) -> [SomeSym] -> [SomeSym]
forall a. AllSyms a => a -> [SomeSym] -> [SomeSym]
allSymsS m (a, s)
v

-- Identity
instance (AllSyms a) => AllSyms (Identity a) where
  allSymsS :: Identity a -> [SomeSym] -> [SomeSym]
allSymsS (Identity a
a) = a -> [SomeSym] -> [SomeSym]
forall a. AllSyms a => a -> [SomeSym] -> [SomeSym]
allSymsS a
a

-- IdentityT
instance (AllSyms (m a)) => AllSyms (IdentityT m a) where
  allSymsS :: IdentityT m a -> [SomeSym] -> [SomeSym]
allSymsS (IdentityT m a
a) = m a -> [SomeSym] -> [SomeSym]
forall a. AllSyms a => a -> [SomeSym] -> [SomeSym]
allSymsS m a
a

-- VerificationConditions
deriving via (Default VerificationConditions) instance AllSyms VerificationConditions

-- AssertionError
deriving via (Default AssertionError) instance AllSyms AssertionError