{-# LANGUAGE CPP #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE DeriveGeneric #-}
{-# LANGUAGE DeriveLift #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TemplateHaskell #-}
{-# 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
  ( Sym (..),
    SymBool,
    SymInteger,
    (-->),
    type (=~>),
    type (-~>),
    SymWordN,
    SymIntN,
    symSize,
    symsSize,
    ModelSymPair (..),
  )
where

import Control.DeepSeq
import Control.Monad.Except
import Data.Bits
import Data.Hashable
import Data.Int
import Data.Proxy
import Data.String
import Data.Word
import GHC.Generics
import GHC.TypeLits
import Grisette.Core.Data.Class.BitVector
import Grisette.Core.Data.Class.Bool
import Grisette.Core.Data.Class.Error
import Grisette.Core.Data.Class.Evaluate
import Grisette.Core.Data.Class.ExtractSymbolics
import Grisette.Core.Data.Class.Function
import Grisette.Core.Data.Class.GenSym
import Grisette.Core.Data.Class.Integer
import Grisette.Core.Data.Class.Mergeable
import Grisette.Core.Data.Class.ModelOps
import Grisette.Core.Data.Class.SOrd
import Grisette.Core.Data.Class.SimpleMergeable
import Grisette.Core.Data.Class.Solvable
import Grisette.Core.Data.Class.Substitute
import Grisette.Core.Data.Class.ToCon
import Grisette.Core.Data.Class.ToSym
import Grisette.IR.SymPrim.Data.BV
import Grisette.IR.SymPrim.Data.IntBitwidth
import Grisette.IR.SymPrim.Data.Prim.InternedTerm.InternedCtors
import Grisette.IR.SymPrim.Data.Prim.InternedTerm.Term
import Grisette.IR.SymPrim.Data.Prim.InternedTerm.TermSubstitution
import Grisette.IR.SymPrim.Data.Prim.InternedTerm.TermUtils
import Grisette.IR.SymPrim.Data.Prim.Model
import Grisette.IR.SymPrim.Data.Prim.PartialEval.BV
import Grisette.IR.SymPrim.Data.Prim.PartialEval.Bits
import Grisette.IR.SymPrim.Data.Prim.PartialEval.Bool
import Grisette.IR.SymPrim.Data.Prim.PartialEval.GeneralFun
import Grisette.IR.SymPrim.Data.Prim.PartialEval.Integer
import Grisette.IR.SymPrim.Data.Prim.PartialEval.Num
import Grisette.IR.SymPrim.Data.Prim.PartialEval.TabularFun
import Grisette.IR.SymPrim.Data.TabularFun
import Grisette.Lib.Control.Monad
import Language.Haskell.TH.Syntax

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

-- | Symbolic primitive type.
--
-- Symbolic Boolean, integer, and bit vector types are supported.
--
-- >>> :set -XOverloadedStrings
-- >>> "a" :: Sym Bool
-- a
-- >>> "a" &&~ "b" :: Sym Bool
-- (&& a b)
-- >>> "i" + 1 :: Sym Integer
-- (+ 1 i)
--
-- For more symbolic operations, please refer to the documentation of the
-- [grisette-core](https://hackage.haskell.org/package/grisette-core) package.
--
-- Grisette also supports uninterpreted functions. You can use the '-->'
-- (general function) or '=->' (tabular function) types to define uninterpreted
-- functions. The following code shows the examples
--
-- >>> :set -XTypeOperators
-- >>> let ftab = "ftab" :: Sym (Integer =-> Integer)
-- >>> ftab # "x"
-- (apply ftab x)
--
-- > >>> solve (UnboundedReasoning z3) (ftab # 1 ==~ 2 &&~ ftab # 2 ==~ 3 &&~ ftab # 3 ==~ 4)
-- > Right (Model {
-- >   ftab ->
-- >     TabularFun {funcTable = [(3,4),(2,3)], defaultFuncValue = 2}
-- >       :: (=->) Integer Integer
-- > }) -- possible result (reformatted)
--
-- >>> let fgen = "fgen" :: Sym (Integer --> Integer)
-- >>> fgen # "x"
-- (apply fgen x)
--
-- > >>> solve (UnboundedReasoning z3) (fgen # 1 ==~ 2 &&~ fgen # 2 ==~ 3 &&~ fgen # 3 ==~ 4)
-- > Right (Model {
-- >   fgen ->
-- >     \(arg@0:FuncArg :: Integer) ->
-- >       (ite (= arg@0:FuncArg 2) 3 (ite (= arg@0:FuncArg 3) 4 2))
-- >         :: (-->) Integer Integer
-- > }) -- possible result (reformatted)
newtype Sym a = Sym {forall a. Sym a -> Term a
underlyingTerm :: Term a} deriving ((forall (m :: * -> *). Quote m => Sym a -> m Exp)
-> (forall (m :: * -> *). Quote m => Sym a -> Code m (Sym a))
-> Lift (Sym a)
forall a (m :: * -> *). Quote m => Sym a -> m Exp
forall a (m :: * -> *). Quote m => Sym a -> Code m (Sym a)
forall t.
(forall (m :: * -> *). Quote m => t -> m Exp)
-> (forall (m :: * -> *). Quote m => t -> Code m t) -> Lift t
forall (m :: * -> *). Quote m => Sym a -> m Exp
forall (m :: * -> *). Quote m => Sym a -> Code m (Sym a)
liftTyped :: forall (m :: * -> *). Quote m => Sym a -> Code m (Sym a)
$cliftTyped :: forall a (m :: * -> *). Quote m => Sym a -> Code m (Sym a)
lift :: forall (m :: * -> *). Quote m => Sym a -> m Exp
$clift :: forall a (m :: * -> *). Quote m => Sym a -> m Exp
Lift, (forall x. Sym a -> Rep (Sym a) x)
-> (forall x. Rep (Sym a) x -> Sym a) -> Generic (Sym a)
forall x. Rep (Sym a) x -> Sym a
forall x. Sym a -> Rep (Sym a) x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
forall a x. Rep (Sym a) x -> Sym a
forall a x. Sym a -> Rep (Sym a) x
$cto :: forall a x. Rep (Sym a) x -> Sym a
$cfrom :: forall a x. Sym a -> Rep (Sym a) x
Generic)

instance NFData (Sym a) where
  rnf :: Sym a -> ()
rnf (Sym Term a
t) = Term a -> ()
forall a. NFData a => a -> ()
rnf Term a
t

instance (SupportedPrim a) => Solvable a (Sym a) where
  con :: a -> Sym a
con = Term a -> Sym a
forall a. Term a -> Sym a
Sym (Term a -> Sym a) -> (a -> Term a) -> a -> Sym a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. a -> Term a
forall t.
(SupportedPrim t, Typeable t, Hashable t, Eq t, Show t) =>
t -> Term t
conTerm
  ssym :: String -> Sym a
ssym = Term a -> Sym a
forall a. Term a -> Sym a
Sym (Term a -> Sym a) -> (String -> Term a) -> String -> Sym a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. String -> Term a
forall t. (SupportedPrim t, Typeable t) => String -> Term t
ssymTerm
  isym :: String -> Int -> Sym a
isym String
str Int
i = Term a -> Sym a
forall a. Term a -> Sym a
Sym (Term a -> Sym a) -> Term a -> Sym a
forall a b. (a -> b) -> a -> b
$ String -> Int -> Term a
forall t. (SupportedPrim t, Typeable t) => String -> Int -> Term t
isymTerm String
str Int
i
  sinfosym :: forall a.
(Typeable a, Ord a, Lift a, NFData a, Show a, Hashable a) =>
String -> a -> Sym a
sinfosym String
str a
info = Term a -> Sym a
forall a. Term a -> Sym a
Sym (Term a -> Sym a) -> Term a -> Sym a
forall a b. (a -> b) -> a -> b
$ String -> a -> Term a
forall t a.
(SupportedPrim t, Typeable t, Typeable a, Ord a, Lift a, NFData a,
 Show a, Hashable a) =>
String -> a -> Term t
sinfosymTerm String
str a
info
  iinfosym :: forall a.
(Typeable a, Ord a, Lift a, NFData a, Show a, Hashable a) =>
String -> Int -> a -> Sym a
iinfosym String
str Int
i a
info = Term a -> Sym a
forall a. Term a -> Sym a
Sym (Term a -> Sym a) -> Term a -> Sym a
forall a b. (a -> b) -> a -> b
$ String -> Int -> a -> Term a
forall t a.
(SupportedPrim t, Typeable t, Typeable a, Ord a, Lift a, NFData a,
 Show a, Hashable a) =>
String -> Int -> a -> Term t
iinfosymTerm String
str Int
i a
info
  conView :: Sym a -> Maybe a
conView (Sym (ConTerm Int
_ a
t)) = a -> Maybe a
forall a. a -> Maybe a
Just a
t
  conView Sym a
_ = Maybe a
forall a. Maybe a
Nothing

instance (SupportedPrim t) => IsString (Sym t) where
  fromString :: String -> Sym t
fromString = String -> Sym t
forall c t. Solvable c t => String -> t
ssym

instance (SupportedPrim a) => ToSym (Sym a) (Sym a) where
  toSym :: Sym a -> Sym a
toSym = Sym a -> Sym a
forall a. a -> a
id

instance (SupportedPrim a) => ToSym a (Sym a) where
  toSym :: a -> Sym a
toSym = a -> Sym a
forall c t. Solvable c t => c -> t
con

instance (SupportedPrim a) => ToCon (Sym a) (Sym a) where
  toCon :: Sym a -> Maybe (Sym a)
toCon = Sym a -> Maybe (Sym a)
forall a. a -> Maybe a
Just

instance (SupportedPrim a) => ToCon (Sym a) a where
  toCon :: Sym a -> Maybe a
toCon = Sym a -> Maybe a
forall c t. Solvable c t => t -> Maybe c
conView

instance (SupportedPrim a) => EvaluateSym (Sym a) where
  evaluateSym :: Bool -> Model -> Sym a -> Sym a
evaluateSym Bool
fillDefault Model
model (Sym Term a
t) = Term a -> Sym a
forall a. Term a -> Sym a
Sym (Term a -> Sym a) -> Term a -> Sym a
forall a b. (a -> b) -> a -> b
$ Bool -> Model -> Term a -> Term a
forall a. SupportedPrim a => Bool -> Model -> Term a -> Term a
evaluateTerm Bool
fillDefault Model
model Term a
t

instance (SupportedPrim a) => ExtractSymbolics (Sym a) where
  extractSymbolics :: Sym a -> SymbolSet
extractSymbolics (Sym Term a
t) = HashSet SomeTypedSymbol -> SymbolSet
SymbolSet (HashSet SomeTypedSymbol -> SymbolSet)
-> HashSet SomeTypedSymbol -> SymbolSet
forall a b. (a -> b) -> a -> b
$ Term a -> HashSet SomeTypedSymbol
forall a. SupportedPrim a => Term a -> HashSet SomeTypedSymbol
extractSymbolicsTerm Term a
t

instance (SupportedPrim a) => Show (Sym a) where
  show :: Sym a -> String
show (Sym Term a
t) = Term a -> String
forall t. SupportedPrim t => Term t -> String
pformat Term a
t

instance (SupportedPrim a) => Hashable (Sym a) where
  hashWithSalt :: Int -> Sym a -> Int
hashWithSalt Int
s (Sym Term a
v) = Int
s Int -> Term a -> Int
forall a. Hashable a => Int -> a -> Int
`hashWithSalt` Term a
v

instance (SupportedPrim a) => Eq (Sym a) where
  (Sym Term a
l) == :: Sym a -> Sym a -> Bool
== (Sym Term a
r) = Term a
l Term a -> Term a -> Bool
forall a. Eq a => a -> a -> Bool
== Term a
r

#define SEQ_SYM(type) \
instance (SupportedPrim type) => SEq (Sym type) where \
  (Sym l) ==~ (Sym r) = Sym $ pevalEqvTerm l r

#define SORD_SYM(type) \
instance (SupportedPrim type) => SOrd (Sym type) where \
  (Sym a) <=~ (Sym b) = Sym $ withPrim (Proxy @type) $ pevalLeNumTerm a b; \
  (Sym a) <~ (Sym b) = Sym $ withPrim (Proxy @type) $ pevalLtNumTerm a b; \
  (Sym a) >=~ (Sym b) = Sym $ withPrim (Proxy @type) $ pevalGeNumTerm a b; \
  (Sym a) >~ (Sym b) = Sym $ withPrim (Proxy @type) $ pevalGtNumTerm a b; \
  a `symCompare` b = \
    withPrim (Proxy @type) $ mrgIf \
      (a <~ b) \
      (mrgReturn LT) \
      (mrgIf (a ==~ b) (mrgReturn EQ) (mrgReturn GT))

#if 1
SEQ_SYM(Bool)
SEQ_SYM(Integer)
SEQ_SYM((IntN n))
SEQ_SYM((WordN n))
SORD_SYM(Integer)
SORD_SYM((IntN n))
SORD_SYM((WordN n))
#endif

-- | Symbolic Boolean type.
type SymBool = Sym Bool

instance SOrd (Sym Bool) where
  Sym Bool
l <=~ :: Sym Bool -> Sym Bool -> Sym Bool
<=~ Sym Bool
r = Sym Bool -> Sym Bool
forall b. LogicalOp b => b -> b
nots Sym Bool
l Sym Bool -> Sym Bool -> Sym Bool
forall b. LogicalOp b => b -> b -> b
||~ Sym Bool
r
  Sym Bool
l <~ :: Sym Bool -> Sym Bool -> Sym Bool
<~ Sym Bool
r = Sym Bool -> Sym Bool
forall b. LogicalOp b => b -> b
nots Sym Bool
l Sym Bool -> Sym Bool -> Sym Bool
forall b. LogicalOp b => b -> b -> b
&&~ Sym Bool
r
  Sym Bool
l >=~ :: Sym Bool -> Sym Bool -> Sym Bool
>=~ Sym Bool
r = Sym Bool
l Sym Bool -> Sym Bool -> Sym Bool
forall b. LogicalOp b => b -> b -> b
||~ Sym Bool -> Sym Bool
forall b. LogicalOp b => b -> b
nots Sym Bool
r
  Sym Bool
l >~ :: Sym Bool -> Sym Bool -> Sym Bool
>~ Sym Bool
r = Sym Bool
l Sym Bool -> Sym Bool -> Sym Bool
forall b. LogicalOp b => b -> b -> b
&&~ Sym Bool -> Sym Bool
forall b. LogicalOp b => b -> b
nots Sym Bool
r
  symCompare :: Sym Bool -> Sym Bool -> UnionM Ordering
symCompare Sym Bool
l Sym Bool
r =
    Sym Bool -> UnionM Ordering -> UnionM Ordering -> UnionM Ordering
forall (u :: * -> *) a.
(UnionLike u, Mergeable a) =>
Sym Bool -> u a -> u a -> u a
mrgIf
      (Sym Bool -> Sym Bool
forall b. LogicalOp b => b -> b
nots Sym Bool
l Sym Bool -> Sym Bool -> Sym Bool
forall b. LogicalOp b => b -> b -> b
&&~ Sym Bool
r)
      (Ordering -> UnionM Ordering
forall (u :: * -> *) a. (MonadUnion u, Mergeable a) => a -> u a
mrgReturn Ordering
LT)
      (Sym Bool -> UnionM Ordering -> UnionM Ordering -> UnionM Ordering
forall (u :: * -> *) a.
(UnionLike u, Mergeable a) =>
Sym Bool -> u a -> u a -> u a
mrgIf (Sym Bool
l Sym Bool -> Sym Bool -> Sym Bool
forall a. SEq a => a -> a -> Sym Bool
==~ Sym Bool
r) (Ordering -> UnionM Ordering
forall (u :: * -> *) a. (MonadUnion u, Mergeable a) => a -> u a
mrgReturn Ordering
EQ) (Ordering -> UnionM Ordering
forall (u :: * -> *) a. (MonadUnion u, Mergeable a) => a -> u a
mrgReturn Ordering
GT))

instance SymBoolOp (Sym Bool)

-- | Symbolic integer type (unbounded, mathematical integer).
type SymInteger = Sym Integer

instance Num (Sym Integer) where
  (Sym Term Integer
l) + :: Sym Integer -> Sym Integer -> Sym Integer
+ (Sym Term Integer
r) = Term Integer -> Sym Integer
forall a. Term a -> Sym a
Sym (Term Integer -> Sym Integer) -> Term Integer -> Sym Integer
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
  (Sym Term Integer
l) - :: Sym Integer -> Sym Integer -> Sym Integer
- (Sym Term Integer
r) = Term Integer -> Sym Integer
forall a. Term a -> Sym a
Sym (Term Integer -> Sym Integer) -> Term Integer -> Sym Integer
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
  (Sym Term Integer
l) * :: Sym Integer -> Sym Integer -> Sym Integer
* (Sym Term Integer
r) = Term Integer -> Sym Integer
forall a. Term a -> Sym a
Sym (Term Integer -> Sym Integer) -> Term Integer -> Sym Integer
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 :: Sym Integer -> Sym Integer
negate (Sym Term Integer
v) = Term Integer -> Sym Integer
forall a. Term a -> Sym a
Sym (Term Integer -> Sym Integer) -> Term Integer -> Sym Integer
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 :: Sym Integer -> Sym Integer
abs (Sym Term Integer
v) = Term Integer -> Sym Integer
forall a. Term a -> Sym a
Sym (Term Integer -> Sym Integer) -> Term Integer -> Sym Integer
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 :: Sym Integer -> Sym Integer
signum (Sym Term Integer
v) = Term Integer -> Sym Integer
forall a. Term a -> Sym a
Sym (Term Integer -> Sym Integer) -> Term Integer -> Sym Integer
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 -> Sym Integer
fromInteger = Integer -> Sym Integer
forall c t. Solvable c t => c -> t
con

instance SignedDivMod (Sym Integer) where
  divs :: forall e (uf :: * -> *).
(MonadError e uf, MonadUnion uf,
 TransformError ArithException e) =>
Sym Integer -> Sym Integer -> uf (Sym Integer)
divs (Sym Term Integer
l) rs :: Sym Integer
rs@(Sym Term Integer
r) =
    Sym Bool
-> uf (Sym Integer) -> uf (Sym Integer) -> uf (Sym Integer)
forall (u :: * -> *) a.
(UnionLike u, Mergeable a) =>
Sym Bool -> u a -> u a -> u a
mrgIf
      (Sym Integer
rs Sym Integer -> Sym Integer -> Sym Bool
forall a. SEq a => a -> a -> Sym Bool
==~ Integer -> Sym Integer
forall c t. Solvable c t => c -> t
con Integer
0)
      (e -> uf (Sym Integer)
forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError (e -> uf (Sym Integer)) -> e -> uf (Sym Integer)
forall a b. (a -> b) -> a -> b
$ ArithException -> e
forall from to. TransformError from to => from -> to
transformError ArithException
DivideByZero)
      (Sym Integer -> uf (Sym Integer)
forall (u :: * -> *) a. (MonadUnion u, Mergeable a) => a -> u a
mrgReturn (Sym Integer -> uf (Sym Integer))
-> Sym Integer -> uf (Sym Integer)
forall a b. (a -> b) -> a -> b
$ Term Integer -> Sym Integer
forall a. Term a -> Sym a
Sym (Term Integer -> Sym Integer) -> Term Integer -> Sym Integer
forall a b. (a -> b) -> a -> b
$ Term Integer -> Term Integer -> Term Integer
pevalDivIntegerTerm Term Integer
l Term Integer
r)
  mods :: forall e (uf :: * -> *).
(MonadError e uf, MonadUnion uf,
 TransformError ArithException e) =>
Sym Integer -> Sym Integer -> uf (Sym Integer)
mods (Sym Term Integer
l) rs :: Sym Integer
rs@(Sym Term Integer
r) =
    Sym Bool
-> uf (Sym Integer) -> uf (Sym Integer) -> uf (Sym Integer)
forall (u :: * -> *) a.
(UnionLike u, Mergeable a) =>
Sym Bool -> u a -> u a -> u a
mrgIf
      (Sym Integer
rs Sym Integer -> Sym Integer -> Sym Bool
forall a. SEq a => a -> a -> Sym Bool
==~ Integer -> Sym Integer
forall c t. Solvable c t => c -> t
con Integer
0)
      (e -> uf (Sym Integer)
forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError (e -> uf (Sym Integer)) -> e -> uf (Sym Integer)
forall a b. (a -> b) -> a -> b
$ ArithException -> e
forall from to. TransformError from to => from -> to
transformError ArithException
DivideByZero)
      (Sym Integer -> uf (Sym Integer)
forall (u :: * -> *) a. (MonadUnion u, Mergeable a) => a -> u a
mrgReturn (Sym Integer -> uf (Sym Integer))
-> Sym Integer -> uf (Sym Integer)
forall a b. (a -> b) -> a -> b
$ Term Integer -> Sym Integer
forall a. Term a -> Sym a
Sym (Term Integer -> Sym Integer) -> Term Integer -> Sym Integer
forall a b. (a -> b) -> a -> b
$ Term Integer -> Term Integer -> Term Integer
pevalModIntegerTerm Term Integer
l Term Integer
r)

instance SymIntegerOp (Sym Integer)

-- | Symbolic signed bit vector type.
type SymIntN n = Sym (IntN n)

instance (SupportedPrim (IntN n)) => Num (Sym (IntN n)) where
  (Sym Term (IntN n)
l) + :: Sym (IntN n) -> Sym (IntN n) -> Sym (IntN n)
+ (Sym Term (IntN n)
r) = Term (IntN n) -> Sym (IntN n)
forall a. Term a -> Sym a
Sym (Term (IntN n) -> Sym (IntN n)) -> Term (IntN n) -> Sym (IntN n)
forall a b. (a -> b) -> a -> b
$ Proxy (IntN n)
-> (PrimConstraint (IntN n) => Term (IntN n)) -> Term (IntN n)
forall t (proxy :: * -> *) a.
SupportedPrim t =>
proxy t -> (PrimConstraint t => a) -> a
withPrim (forall {t}. Proxy t
forall {k} (t :: k). Proxy t
Proxy @(IntN n)) ((PrimConstraint (IntN n) => Term (IntN n)) -> Term (IntN n))
-> (PrimConstraint (IntN n) => Term (IntN n)) -> Term (IntN n)
forall a b. (a -> b) -> a -> b
$ Term (IntN n) -> Term (IntN n) -> Term (IntN n)
forall a. (Num a, SupportedPrim a) => Term a -> Term a -> Term a
pevalAddNumTerm Term (IntN n)
l Term (IntN n)
r
  (Sym Term (IntN n)
l) - :: Sym (IntN n) -> Sym (IntN n) -> Sym (IntN n)
- (Sym Term (IntN n)
r) = Term (IntN n) -> Sym (IntN n)
forall a. Term a -> Sym a
Sym (Term (IntN n) -> Sym (IntN n)) -> Term (IntN n) -> Sym (IntN n)
forall a b. (a -> b) -> a -> b
$ Proxy (IntN n)
-> (PrimConstraint (IntN n) => Term (IntN n)) -> Term (IntN n)
forall t (proxy :: * -> *) a.
SupportedPrim t =>
proxy t -> (PrimConstraint t => a) -> a
withPrim (forall {t}. Proxy t
forall {k} (t :: k). Proxy t
Proxy @(IntN n)) ((PrimConstraint (IntN n) => Term (IntN n)) -> Term (IntN n))
-> (PrimConstraint (IntN n) => Term (IntN n)) -> Term (IntN n)
forall a b. (a -> b) -> a -> b
$ Term (IntN n) -> Term (IntN n) -> Term (IntN n)
forall a. (Num a, SupportedPrim a) => Term a -> Term a -> Term a
pevalMinusNumTerm Term (IntN n)
l Term (IntN n)
r
  (Sym Term (IntN n)
l) * :: Sym (IntN n) -> Sym (IntN n) -> Sym (IntN n)
* (Sym Term (IntN n)
r) = Term (IntN n) -> Sym (IntN n)
forall a. Term a -> Sym a
Sym (Term (IntN n) -> Sym (IntN n)) -> Term (IntN n) -> Sym (IntN n)
forall a b. (a -> b) -> a -> b
$ Proxy (IntN n)
-> (PrimConstraint (IntN n) => Term (IntN n)) -> Term (IntN n)
forall t (proxy :: * -> *) a.
SupportedPrim t =>
proxy t -> (PrimConstraint t => a) -> a
withPrim (forall {t}. Proxy t
forall {k} (t :: k). Proxy t
Proxy @(IntN n)) ((PrimConstraint (IntN n) => Term (IntN n)) -> Term (IntN n))
-> (PrimConstraint (IntN n) => Term (IntN n)) -> Term (IntN n)
forall a b. (a -> b) -> a -> b
$ Term (IntN n) -> Term (IntN n) -> Term (IntN n)
forall a. (Num a, SupportedPrim a) => Term a -> Term a -> Term a
pevalTimesNumTerm Term (IntN n)
l Term (IntN n)
r
  negate :: Sym (IntN n) -> Sym (IntN n)
negate (Sym Term (IntN n)
v) = Term (IntN n) -> Sym (IntN n)
forall a. Term a -> Sym a
Sym (Term (IntN n) -> Sym (IntN n)) -> Term (IntN n) -> Sym (IntN n)
forall a b. (a -> b) -> a -> b
$ Proxy (IntN n)
-> (PrimConstraint (IntN n) => Term (IntN n)) -> Term (IntN n)
forall t (proxy :: * -> *) a.
SupportedPrim t =>
proxy t -> (PrimConstraint t => a) -> a
withPrim (forall {t}. Proxy t
forall {k} (t :: k). Proxy t
Proxy @(IntN n)) ((PrimConstraint (IntN n) => Term (IntN n)) -> Term (IntN n))
-> (PrimConstraint (IntN n) => Term (IntN n)) -> Term (IntN n)
forall a b. (a -> b) -> a -> b
$ Term (IntN n) -> Term (IntN n)
forall a. (Num a, SupportedPrim a) => Term a -> Term a
pevalUMinusNumTerm Term (IntN n)
v
  abs :: Sym (IntN n) -> Sym (IntN n)
abs (Sym Term (IntN n)
v) = Term (IntN n) -> Sym (IntN n)
forall a. Term a -> Sym a
Sym (Term (IntN n) -> Sym (IntN n)) -> Term (IntN n) -> Sym (IntN n)
forall a b. (a -> b) -> a -> b
$ Proxy (IntN n)
-> (PrimConstraint (IntN n) => Term (IntN n)) -> Term (IntN n)
forall t (proxy :: * -> *) a.
SupportedPrim t =>
proxy t -> (PrimConstraint t => a) -> a
withPrim (forall {t}. Proxy t
forall {k} (t :: k). Proxy t
Proxy @(IntN n)) ((PrimConstraint (IntN n) => Term (IntN n)) -> Term (IntN n))
-> (PrimConstraint (IntN n) => Term (IntN n)) -> Term (IntN n)
forall a b. (a -> b) -> a -> b
$ Term (IntN n) -> Term (IntN n)
forall a. (SupportedPrim a, Num a) => Term a -> Term a
pevalAbsNumTerm Term (IntN n)
v
  signum :: Sym (IntN n) -> Sym (IntN n)
signum (Sym Term (IntN n)
v) = Term (IntN n) -> Sym (IntN n)
forall a. Term a -> Sym a
Sym (Term (IntN n) -> Sym (IntN n)) -> Term (IntN n) -> Sym (IntN n)
forall a b. (a -> b) -> a -> b
$ Proxy (IntN n)
-> (PrimConstraint (IntN n) => Term (IntN n)) -> Term (IntN n)
forall t (proxy :: * -> *) a.
SupportedPrim t =>
proxy t -> (PrimConstraint t => a) -> a
withPrim (forall {t}. Proxy t
forall {k} (t :: k). Proxy t
Proxy @(IntN n)) ((PrimConstraint (IntN n) => Term (IntN n)) -> Term (IntN n))
-> (PrimConstraint (IntN n) => Term (IntN n)) -> Term (IntN n)
forall a b. (a -> b) -> a -> b
$ Term (IntN n) -> Term (IntN n)
forall a. (Num a, SupportedPrim a) => Term a -> Term a
pevalSignumNumTerm Term (IntN n)
v
  fromInteger :: Integer -> Sym (IntN n)
fromInteger Integer
i = Proxy (IntN n)
-> (PrimConstraint (IntN n) => Sym (IntN n)) -> Sym (IntN n)
forall t (proxy :: * -> *) a.
SupportedPrim t =>
proxy t -> (PrimConstraint t => a) -> a
withPrim (forall {t}. Proxy t
forall {k} (t :: k). Proxy t
Proxy @(IntN n)) ((PrimConstraint (IntN n) => Sym (IntN n)) -> Sym (IntN n))
-> (PrimConstraint (IntN n) => Sym (IntN n)) -> Sym (IntN n)
forall a b. (a -> b) -> a -> b
$ IntN n -> Sym (IntN n)
forall c t. Solvable c t => c -> t
con (IntN n -> Sym (IntN n)) -> IntN n -> Sym (IntN n)
forall a b. (a -> b) -> a -> b
$ Integer -> IntN n
forall a. Num a => Integer -> a
fromInteger Integer
i

instance (SupportedPrim (IntN n)) => Bits (Sym (IntN n)) where
  Sym Term (IntN n)
l .&. :: Sym (IntN n) -> Sym (IntN n) -> Sym (IntN n)
.&. Sym Term (IntN n)
r = Term (IntN n) -> Sym (IntN n)
forall a. Term a -> Sym a
Sym (Term (IntN n) -> Sym (IntN n)) -> Term (IntN n) -> Sym (IntN n)
forall a b. (a -> b) -> a -> b
$ Proxy (IntN n)
-> (PrimConstraint (IntN n) => Term (IntN n)) -> Term (IntN n)
forall t (proxy :: * -> *) a.
SupportedPrim t =>
proxy t -> (PrimConstraint t => a) -> a
withPrim (forall {t}. Proxy t
forall {k} (t :: k). Proxy t
Proxy @(IntN n)) ((PrimConstraint (IntN n) => Term (IntN n)) -> Term (IntN n))
-> (PrimConstraint (IntN n) => Term (IntN n)) -> Term (IntN n)
forall a b. (a -> b) -> a -> b
$ Term (IntN n) -> Term (IntN n) -> Term (IntN n)
forall a. (Bits a, SupportedPrim a) => Term a -> Term a -> Term a
pevalAndBitsTerm Term (IntN n)
l Term (IntN n)
r
  Sym Term (IntN n)
l .|. :: Sym (IntN n) -> Sym (IntN n) -> Sym (IntN n)
.|. Sym Term (IntN n)
r = Term (IntN n) -> Sym (IntN n)
forall a. Term a -> Sym a
Sym (Term (IntN n) -> Sym (IntN n)) -> Term (IntN n) -> Sym (IntN n)
forall a b. (a -> b) -> a -> b
$ Proxy (IntN n)
-> (PrimConstraint (IntN n) => Term (IntN n)) -> Term (IntN n)
forall t (proxy :: * -> *) a.
SupportedPrim t =>
proxy t -> (PrimConstraint t => a) -> a
withPrim (forall {t}. Proxy t
forall {k} (t :: k). Proxy t
Proxy @(IntN n)) ((PrimConstraint (IntN n) => Term (IntN n)) -> Term (IntN n))
-> (PrimConstraint (IntN n) => Term (IntN n)) -> Term (IntN n)
forall a b. (a -> b) -> a -> b
$ Term (IntN n) -> Term (IntN n) -> Term (IntN n)
forall a. (Bits a, SupportedPrim a) => Term a -> Term a -> Term a
pevalOrBitsTerm Term (IntN n)
l Term (IntN n)
r
  Sym Term (IntN n)
l xor :: Sym (IntN n) -> Sym (IntN n) -> Sym (IntN n)
`xor` Sym Term (IntN n)
r = Term (IntN n) -> Sym (IntN n)
forall a. Term a -> Sym a
Sym (Term (IntN n) -> Sym (IntN n)) -> Term (IntN n) -> Sym (IntN n)
forall a b. (a -> b) -> a -> b
$ Proxy (IntN n)
-> (PrimConstraint (IntN n) => Term (IntN n)) -> Term (IntN n)
forall t (proxy :: * -> *) a.
SupportedPrim t =>
proxy t -> (PrimConstraint t => a) -> a
withPrim (forall {t}. Proxy t
forall {k} (t :: k). Proxy t
Proxy @(IntN n)) ((PrimConstraint (IntN n) => Term (IntN n)) -> Term (IntN n))
-> (PrimConstraint (IntN n) => Term (IntN n)) -> Term (IntN n)
forall a b. (a -> b) -> a -> b
$ Term (IntN n) -> Term (IntN n) -> Term (IntN n)
forall a. (Bits a, SupportedPrim a) => Term a -> Term a -> Term a
pevalXorBitsTerm Term (IntN n)
l Term (IntN n)
r
  complement :: Sym (IntN n) -> Sym (IntN n)
complement (Sym Term (IntN n)
n) = Term (IntN n) -> Sym (IntN n)
forall a. Term a -> Sym a
Sym (Term (IntN n) -> Sym (IntN n)) -> Term (IntN n) -> Sym (IntN n)
forall a b. (a -> b) -> a -> b
$ Proxy (IntN n)
-> (PrimConstraint (IntN n) => Term (IntN n)) -> Term (IntN n)
forall t (proxy :: * -> *) a.
SupportedPrim t =>
proxy t -> (PrimConstraint t => a) -> a
withPrim (forall {t}. Proxy t
forall {k} (t :: k). Proxy t
Proxy @(IntN n)) ((PrimConstraint (IntN n) => Term (IntN n)) -> Term (IntN n))
-> (PrimConstraint (IntN n) => Term (IntN n)) -> Term (IntN n)
forall a b. (a -> b) -> a -> b
$ Term (IntN n) -> Term (IntN n)
forall a. (Bits a, SupportedPrim a) => Term a -> Term a
pevalComplementBitsTerm Term (IntN n)
n
  shift :: Sym (IntN n) -> Int -> Sym (IntN n)
shift (Sym Term (IntN n)
n) Int
i = Term (IntN n) -> Sym (IntN n)
forall a. Term a -> Sym a
Sym (Term (IntN n) -> Sym (IntN n)) -> Term (IntN n) -> Sym (IntN n)
forall a b. (a -> b) -> a -> b
$ Proxy (IntN n)
-> (PrimConstraint (IntN n) => Term (IntN n)) -> Term (IntN n)
forall t (proxy :: * -> *) a.
SupportedPrim t =>
proxy t -> (PrimConstraint t => a) -> a
withPrim (forall {t}. Proxy t
forall {k} (t :: k). Proxy t
Proxy @(IntN n)) ((PrimConstraint (IntN n) => Term (IntN n)) -> Term (IntN n))
-> (PrimConstraint (IntN n) => Term (IntN n)) -> Term (IntN n)
forall a b. (a -> b) -> a -> b
$ Term (IntN n) -> Int -> Term (IntN n)
forall a. (Bits a, SupportedPrim a) => Term a -> Int -> Term a
pevalShiftBitsTerm Term (IntN n)
n Int
i
  rotate :: Sym (IntN n) -> Int -> Sym (IntN n)
rotate (Sym Term (IntN n)
n) Int
i = Term (IntN n) -> Sym (IntN n)
forall a. Term a -> Sym a
Sym (Term (IntN n) -> Sym (IntN n)) -> Term (IntN n) -> Sym (IntN n)
forall a b. (a -> b) -> a -> b
$ Proxy (IntN n)
-> (PrimConstraint (IntN n) => Term (IntN n)) -> Term (IntN n)
forall t (proxy :: * -> *) a.
SupportedPrim t =>
proxy t -> (PrimConstraint t => a) -> a
withPrim (forall {t}. Proxy t
forall {k} (t :: k). Proxy t
Proxy @(IntN n)) ((PrimConstraint (IntN n) => Term (IntN n)) -> Term (IntN n))
-> (PrimConstraint (IntN n) => Term (IntN n)) -> Term (IntN n)
forall a b. (a -> b) -> a -> b
$ Term (IntN n) -> Int -> Term (IntN n)
forall a. (Bits a, SupportedPrim a) => Term a -> Int -> Term a
pevalRotateBitsTerm Term (IntN n)
n Int
i
  bitSize :: Sym (IntN n) -> Int
bitSize Sym (IntN n)
_ = Integer -> Int
forall a. Num a => Integer -> a
fromInteger (Integer -> Int) -> Integer -> Int
forall a b. (a -> b) -> a -> b
$ Proxy (IntN n) -> (PrimConstraint (IntN n) => Integer) -> Integer
forall t (proxy :: * -> *) a.
SupportedPrim t =>
proxy t -> (PrimConstraint t => a) -> a
withPrim (forall {t}. Proxy t
forall {k} (t :: k). Proxy t
Proxy @(IntN n)) ((PrimConstraint (IntN n) => Integer) -> Integer)
-> (PrimConstraint (IntN n) => Integer) -> Integer
forall a b. (a -> b) -> a -> b
$ Proxy n -> Integer
forall (n :: Nat) (proxy :: Nat -> *).
KnownNat n =>
proxy n -> Integer
natVal (forall {k} (t :: k). Proxy t
forall {t :: Nat}. Proxy t
Proxy @n)
  bitSizeMaybe :: Sym (IntN n) -> Maybe Int
bitSizeMaybe Sym (IntN n)
_ = Int -> Maybe Int
forall a. a -> Maybe a
Just (Int -> Maybe Int) -> Int -> Maybe Int
forall a b. (a -> b) -> a -> b
$ Integer -> Int
forall a. Num a => Integer -> a
fromInteger (Integer -> Int) -> Integer -> Int
forall a b. (a -> b) -> a -> b
$ Proxy (IntN n) -> (PrimConstraint (IntN n) => Integer) -> Integer
forall t (proxy :: * -> *) a.
SupportedPrim t =>
proxy t -> (PrimConstraint t => a) -> a
withPrim (forall {t}. Proxy t
forall {k} (t :: k). Proxy t
Proxy @(IntN n)) ((PrimConstraint (IntN n) => Integer) -> Integer)
-> (PrimConstraint (IntN n) => Integer) -> Integer
forall a b. (a -> b) -> a -> b
$ Proxy n -> Integer
forall (n :: Nat) (proxy :: Nat -> *).
KnownNat n =>
proxy n -> Integer
natVal (forall {k} (t :: k). Proxy t
forall {t :: Nat}. Proxy t
Proxy @n)
  isSigned :: Sym (IntN n) -> Bool
isSigned Sym (IntN n)
_ = Bool
True
  testBit :: Sym (IntN n) -> Int -> Bool
testBit (Con IntN n
n) = Proxy (IntN n)
-> (PrimConstraint (IntN n) => Int -> Bool) -> Int -> Bool
forall t (proxy :: * -> *) a.
SupportedPrim t =>
proxy t -> (PrimConstraint t => a) -> a
withPrim (forall {t}. Proxy t
forall {k} (t :: k). Proxy t
Proxy @(IntN n)) ((PrimConstraint (IntN n) => Int -> Bool) -> Int -> Bool)
-> (PrimConstraint (IntN n) => Int -> Bool) -> Int -> Bool
forall a b. (a -> b) -> a -> b
$ IntN n -> Int -> Bool
forall a. Bits a => a -> Int -> Bool
testBit IntN n
n
  testBit Sym (IntN n)
_ = String -> Int -> Bool
forall a. HasCallStack => String -> a
error String
"You cannot call testBit on symbolic variables"
  bit :: Int -> Sym (IntN n)
bit = Proxy (IntN n)
-> (PrimConstraint (IntN n) => Int -> Sym (IntN n))
-> Int
-> Sym (IntN n)
forall t (proxy :: * -> *) a.
SupportedPrim t =>
proxy t -> (PrimConstraint t => a) -> a
withPrim (forall {t}. Proxy t
forall {k} (t :: k). Proxy t
Proxy @(IntN n)) ((PrimConstraint (IntN n) => Int -> Sym (IntN n))
 -> Int -> Sym (IntN n))
-> (PrimConstraint (IntN n) => Int -> Sym (IntN n))
-> Int
-> Sym (IntN n)
forall a b. (a -> b) -> a -> b
$ IntN n -> Sym (IntN n)
forall c t. Solvable c t => c -> t
con (IntN n -> Sym (IntN n)) -> (Int -> IntN n) -> Int -> Sym (IntN n)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Int -> IntN n
forall a. Bits a => Int -> a
bit
  popCount :: Sym (IntN n) -> Int
popCount (Con IntN n
n) = Proxy (IntN n) -> (PrimConstraint (IntN n) => Int) -> Int
forall t (proxy :: * -> *) a.
SupportedPrim t =>
proxy t -> (PrimConstraint t => a) -> a
withPrim (forall {t}. Proxy t
forall {k} (t :: k). Proxy t
Proxy @(IntN n)) ((PrimConstraint (IntN n) => Int) -> Int)
-> (PrimConstraint (IntN n) => Int) -> Int
forall a b. (a -> b) -> a -> b
$ IntN n -> Int
forall a. Bits a => a -> Int
popCount IntN n
n
  popCount Sym (IntN n)
_ = String -> Int
forall a. HasCallStack => String -> a
error String
"You cannot call popCount on symbolic variables"

instance
  (KnownNat w', KnownNat n, KnownNat w, w' ~ (n + w), 1 <= n, 1 <= w, 1 <= w') =>
  BVConcat (Sym (IntN n)) (Sym (IntN w)) (Sym (IntN w'))
  where
  bvconcat :: Sym (IntN n) -> Sym (IntN w) -> Sym (IntN w')
bvconcat (Sym Term (IntN n)
l) (Sym Term (IntN w)
r) = Term (IntN w') -> Sym (IntN w')
forall a. Term a -> Sym a
Sym (Term (IntN n) -> Term (IntN w) -> Term (IntN w')
forall (s :: Nat -> *) (w :: Nat) (w' :: Nat) (w'' :: Nat).
(SupportedPrim (s w), SupportedPrim (s w'), SupportedPrim (s w''),
 KnownNat w, KnownNat w', KnownNat w'',
 BVConcat (s w) (s w') (s w'')) =>
Term (s w) -> Term (s w') -> Term (s w'')
pevalBVConcatTerm Term (IntN n)
l Term (IntN w)
r)

instance
  ( KnownNat w,
    KnownNat w',
    1 <= w,
    1 <= w',
    w <= w',
    w + 1 <= w',
    1 <= w' - w,
    KnownNat (w' - w)
  ) =>
  BVExtend (Sym (IntN w)) w' (Sym (IntN w'))
  where
  bvzeroExtend :: forall (proxy :: Nat -> *).
proxy w' -> Sym (IntN w) -> Sym (IntN w')
bvzeroExtend proxy w'
_ (Sym Term (IntN w)
v) = Term (IntN w') -> Sym (IntN w')
forall a. Term a -> Sym a
Sym (Term (IntN w') -> Sym (IntN w'))
-> Term (IntN w') -> Sym (IntN w')
forall a b. (a -> b) -> a -> b
$ Bool -> Proxy w' -> Term (IntN w) -> Term (IntN w')
forall (proxy :: Nat -> *) (a :: Nat) (n :: Nat) (b :: Nat)
       (bv :: Nat -> *).
(KnownNat a, KnownNat b, KnownNat n, BVExtend (bv a) n (bv b),
 SupportedPrim (bv a), SupportedPrim (bv b)) =>
Bool -> proxy n -> Term (bv a) -> Term (bv b)
pevalBVExtendTerm Bool
False (forall {k} (t :: k). Proxy t
forall {t :: Nat}. Proxy t
Proxy @w') Term (IntN w)
v
  bvsignExtend :: forall (proxy :: Nat -> *).
proxy w' -> Sym (IntN w) -> Sym (IntN w')
bvsignExtend proxy w'
_ (Sym Term (IntN w)
v) = Term (IntN w') -> Sym (IntN w')
forall a. Term a -> Sym a
Sym (Term (IntN w') -> Sym (IntN w'))
-> Term (IntN w') -> Sym (IntN w')
forall a b. (a -> b) -> a -> b
$ Bool -> Proxy w' -> Term (IntN w) -> Term (IntN w')
forall (proxy :: Nat -> *) (a :: Nat) (n :: Nat) (b :: Nat)
       (bv :: Nat -> *).
(KnownNat a, KnownNat b, KnownNat n, BVExtend (bv a) n (bv b),
 SupportedPrim (bv a), SupportedPrim (bv b)) =>
Bool -> proxy n -> Term (bv a) -> Term (bv b)
pevalBVExtendTerm Bool
True (forall {k} (t :: k). Proxy t
forall {t :: Nat}. Proxy t
Proxy @w') Term (IntN w)
v
  bvextend :: forall (proxy :: Nat -> *).
proxy w' -> Sym (IntN w) -> Sym (IntN w')
bvextend = proxy w' -> Sym (IntN w) -> Sym (IntN w')
forall bv1 (n :: Nat) bv2 (proxy :: Nat -> *).
BVExtend bv1 n bv2 =>
proxy n -> bv1 -> bv2
bvsignExtend

instance
  ( KnownNat ix,
    KnownNat w,
    KnownNat ow,
    ix + w <= ow,
    1 <= ow,
    1 <= w
  ) =>
  BVSelect (Sym (IntN ow)) ix w (Sym (IntN w))
  where
  bvselect :: forall (proxy :: Nat -> *).
proxy ix -> proxy w -> Sym (IntN ow) -> Sym (IntN w)
bvselect proxy ix
pix proxy w
pw (Sym Term (IntN ow)
v) = Term (IntN w) -> Sym (IntN w)
forall a. Term a -> Sym a
Sym (Term (IntN w) -> Sym (IntN w)) -> Term (IntN w) -> Sym (IntN w)
forall a b. (a -> b) -> a -> b
$ proxy ix -> proxy w -> Term (IntN ow) -> Term (IntN w)
forall (bv :: Nat -> *) (a :: Nat) (ix :: Nat) (w :: Nat)
       (proxy :: Nat -> *).
(SupportedPrim (bv a), SupportedPrim (bv w), KnownNat a,
 KnownNat w, KnownNat ix, BVSelect (bv a) ix w (bv w)) =>
proxy ix -> proxy w -> Term (bv a) -> Term (bv w)
pevalBVSelectTerm proxy ix
pix proxy w
pw Term (IntN ow)
v

#define TOSYM_MACHINE_INTEGER(int, bv) \
instance ToSym int (Sym (bv)) where \
  toSym = fromIntegral

#define TOCON_MACHINE_INTEGER(bvw, n, int) \
instance ToCon (Sym (bvw n)) int where \
  toCon (Con (bvw v :: bvw n)) = Just $ fromIntegral v; \
  toCon _ = Nothing

#if 1
TOSYM_MACHINE_INTEGER(Int8, IntN 8)
TOSYM_MACHINE_INTEGER(Int16, IntN 16)
TOSYM_MACHINE_INTEGER(Int32, IntN 32)
TOSYM_MACHINE_INTEGER(Int64, IntN 64)
TOSYM_MACHINE_INTEGER(Word8, WordN 8)
TOSYM_MACHINE_INTEGER(Word16, WordN 16)
TOSYM_MACHINE_INTEGER(Word32, WordN 32)
TOSYM_MACHINE_INTEGER(Word64, WordN 64)
TOSYM_MACHINE_INTEGER(Int, IntN $intBitwidthQ)
TOSYM_MACHINE_INTEGER(Word, WordN $intBitwidthQ)

TOCON_MACHINE_INTEGER(IntN, 8, Int8)
TOCON_MACHINE_INTEGER(IntN, 16, Int16)
TOCON_MACHINE_INTEGER(IntN, 32, Int32)
TOCON_MACHINE_INTEGER(IntN, 64, Int64)
TOCON_MACHINE_INTEGER(WordN, 8, Word8)
TOCON_MACHINE_INTEGER(WordN, 16, Word16)
TOCON_MACHINE_INTEGER(WordN, 32, Word32)
TOCON_MACHINE_INTEGER(WordN, 64, Word64)
TOCON_MACHINE_INTEGER(IntN, $intBitwidthQ, Int)
TOCON_MACHINE_INTEGER(WordN, $intBitwidthQ, Word)
#endif

-- | Symbolic unsigned bit vector type.
type SymWordN n = Sym (WordN n)

instance (SupportedPrim (WordN n)) => Num (Sym (WordN n)) where
  (Sym Term (WordN n)
l) + :: Sym (WordN n) -> Sym (WordN n) -> Sym (WordN n)
+ (Sym Term (WordN n)
r) = Term (WordN n) -> Sym (WordN n)
forall a. Term a -> Sym a
Sym (Term (WordN n) -> Sym (WordN n))
-> Term (WordN n) -> Sym (WordN n)
forall a b. (a -> b) -> a -> b
$ Proxy (WordN n)
-> (PrimConstraint (WordN n) => Term (WordN n)) -> Term (WordN n)
forall t (proxy :: * -> *) a.
SupportedPrim t =>
proxy t -> (PrimConstraint t => a) -> a
withPrim (forall {t}. Proxy t
forall {k} (t :: k). Proxy t
Proxy @(WordN n)) ((PrimConstraint (WordN n) => Term (WordN n)) -> Term (WordN n))
-> (PrimConstraint (WordN n) => Term (WordN n)) -> Term (WordN n)
forall a b. (a -> b) -> a -> b
$ Term (WordN n) -> Term (WordN n) -> Term (WordN n)
forall a. (Num a, SupportedPrim a) => Term a -> Term a -> Term a
pevalAddNumTerm Term (WordN n)
l Term (WordN n)
r
  (Sym Term (WordN n)
l) - :: Sym (WordN n) -> Sym (WordN n) -> Sym (WordN n)
- (Sym Term (WordN n)
r) = Term (WordN n) -> Sym (WordN n)
forall a. Term a -> Sym a
Sym (Term (WordN n) -> Sym (WordN n))
-> Term (WordN n) -> Sym (WordN n)
forall a b. (a -> b) -> a -> b
$ Proxy (WordN n)
-> (PrimConstraint (WordN n) => Term (WordN n)) -> Term (WordN n)
forall t (proxy :: * -> *) a.
SupportedPrim t =>
proxy t -> (PrimConstraint t => a) -> a
withPrim (forall {t}. Proxy t
forall {k} (t :: k). Proxy t
Proxy @(WordN n)) ((PrimConstraint (WordN n) => Term (WordN n)) -> Term (WordN n))
-> (PrimConstraint (WordN n) => Term (WordN n)) -> Term (WordN n)
forall a b. (a -> b) -> a -> b
$ Term (WordN n) -> Term (WordN n) -> Term (WordN n)
forall a. (Num a, SupportedPrim a) => Term a -> Term a -> Term a
pevalMinusNumTerm Term (WordN n)
l Term (WordN n)
r
  (Sym Term (WordN n)
l) * :: Sym (WordN n) -> Sym (WordN n) -> Sym (WordN n)
* (Sym Term (WordN n)
r) = Term (WordN n) -> Sym (WordN n)
forall a. Term a -> Sym a
Sym (Term (WordN n) -> Sym (WordN n))
-> Term (WordN n) -> Sym (WordN n)
forall a b. (a -> b) -> a -> b
$ Proxy (WordN n)
-> (PrimConstraint (WordN n) => Term (WordN n)) -> Term (WordN n)
forall t (proxy :: * -> *) a.
SupportedPrim t =>
proxy t -> (PrimConstraint t => a) -> a
withPrim (forall {t}. Proxy t
forall {k} (t :: k). Proxy t
Proxy @(WordN n)) ((PrimConstraint (WordN n) => Term (WordN n)) -> Term (WordN n))
-> (PrimConstraint (WordN n) => Term (WordN n)) -> Term (WordN n)
forall a b. (a -> b) -> a -> b
$ Term (WordN n) -> Term (WordN n) -> Term (WordN n)
forall a. (Num a, SupportedPrim a) => Term a -> Term a -> Term a
pevalTimesNumTerm Term (WordN n)
l Term (WordN n)
r
  negate :: Sym (WordN n) -> Sym (WordN n)
negate (Sym Term (WordN n)
v) = Term (WordN n) -> Sym (WordN n)
forall a. Term a -> Sym a
Sym (Term (WordN n) -> Sym (WordN n))
-> Term (WordN n) -> Sym (WordN n)
forall a b. (a -> b) -> a -> b
$ Proxy (WordN n)
-> (PrimConstraint (WordN n) => Term (WordN n)) -> Term (WordN n)
forall t (proxy :: * -> *) a.
SupportedPrim t =>
proxy t -> (PrimConstraint t => a) -> a
withPrim (forall {t}. Proxy t
forall {k} (t :: k). Proxy t
Proxy @(WordN n)) ((PrimConstraint (WordN n) => Term (WordN n)) -> Term (WordN n))
-> (PrimConstraint (WordN n) => Term (WordN n)) -> Term (WordN n)
forall a b. (a -> b) -> a -> b
$ Term (WordN n) -> Term (WordN n)
forall a. (Num a, SupportedPrim a) => Term a -> Term a
pevalUMinusNumTerm Term (WordN n)
v
  abs :: Sym (WordN n) -> Sym (WordN n)
abs (Sym Term (WordN n)
v) = Term (WordN n) -> Sym (WordN n)
forall a. Term a -> Sym a
Sym (Term (WordN n) -> Sym (WordN n))
-> Term (WordN n) -> Sym (WordN n)
forall a b. (a -> b) -> a -> b
$ Proxy (WordN n)
-> (PrimConstraint (WordN n) => Term (WordN n)) -> Term (WordN n)
forall t (proxy :: * -> *) a.
SupportedPrim t =>
proxy t -> (PrimConstraint t => a) -> a
withPrim (forall {t}. Proxy t
forall {k} (t :: k). Proxy t
Proxy @(WordN n)) ((PrimConstraint (WordN n) => Term (WordN n)) -> Term (WordN n))
-> (PrimConstraint (WordN n) => Term (WordN n)) -> Term (WordN n)
forall a b. (a -> b) -> a -> b
$ Term (WordN n) -> Term (WordN n)
forall a. (SupportedPrim a, Num a) => Term a -> Term a
pevalAbsNumTerm Term (WordN n)
v
  signum :: Sym (WordN n) -> Sym (WordN n)
signum (Sym Term (WordN n)
v) = Term (WordN n) -> Sym (WordN n)
forall a. Term a -> Sym a
Sym (Term (WordN n) -> Sym (WordN n))
-> Term (WordN n) -> Sym (WordN n)
forall a b. (a -> b) -> a -> b
$ Proxy (WordN n)
-> (PrimConstraint (WordN n) => Term (WordN n)) -> Term (WordN n)
forall t (proxy :: * -> *) a.
SupportedPrim t =>
proxy t -> (PrimConstraint t => a) -> a
withPrim (forall {t}. Proxy t
forall {k} (t :: k). Proxy t
Proxy @(WordN n)) ((PrimConstraint (WordN n) => Term (WordN n)) -> Term (WordN n))
-> (PrimConstraint (WordN n) => Term (WordN n)) -> Term (WordN n)
forall a b. (a -> b) -> a -> b
$ Term (WordN n) -> Term (WordN n)
forall a. (Num a, SupportedPrim a) => Term a -> Term a
pevalSignumNumTerm Term (WordN n)
v
  fromInteger :: Integer -> Sym (WordN n)
fromInteger Integer
i = Proxy (WordN n)
-> (PrimConstraint (WordN n) => Sym (WordN n)) -> Sym (WordN n)
forall t (proxy :: * -> *) a.
SupportedPrim t =>
proxy t -> (PrimConstraint t => a) -> a
withPrim (forall {t}. Proxy t
forall {k} (t :: k). Proxy t
Proxy @(WordN n)) ((PrimConstraint (WordN n) => Sym (WordN n)) -> Sym (WordN n))
-> (PrimConstraint (WordN n) => Sym (WordN n)) -> Sym (WordN n)
forall a b. (a -> b) -> a -> b
$ WordN n -> Sym (WordN n)
forall c t. Solvable c t => c -> t
con (WordN n -> Sym (WordN n)) -> WordN n -> Sym (WordN n)
forall a b. (a -> b) -> a -> b
$ Integer -> WordN n
forall a. Num a => Integer -> a
fromInteger Integer
i

instance
  (KnownNat w', KnownNat n, KnownNat w, w' ~ (n + w), 1 <= n, 1 <= w, 1 <= w') =>
  BVConcat (Sym (WordN n)) (Sym (WordN w)) (Sym (WordN w'))
  where
  bvconcat :: Sym (WordN n) -> Sym (WordN w) -> Sym (WordN w')
bvconcat (Sym Term (WordN n)
l) (Sym Term (WordN w)
r) = Term (WordN w') -> Sym (WordN w')
forall a. Term a -> Sym a
Sym (Term (WordN n) -> Term (WordN w) -> Term (WordN w')
forall (s :: Nat -> *) (w :: Nat) (w' :: Nat) (w'' :: Nat).
(SupportedPrim (s w), SupportedPrim (s w'), SupportedPrim (s w''),
 KnownNat w, KnownNat w', KnownNat w'',
 BVConcat (s w) (s w') (s w'')) =>
Term (s w) -> Term (s w') -> Term (s w'')
pevalBVConcatTerm Term (WordN n)
l Term (WordN w)
r)

instance
  ( KnownNat w,
    KnownNat w',
    1 <= w,
    1 <= w',
    w + 1 <= w',
    w <= w',
    1 <= w' - w,
    KnownNat (w' - w)
  ) =>
  BVExtend (Sym (WordN w)) w' (Sym (WordN w'))
  where
  bvzeroExtend :: forall (proxy :: Nat -> *).
proxy w' -> Sym (WordN w) -> Sym (WordN w')
bvzeroExtend proxy w'
_ (Sym Term (WordN w)
v) = Term (WordN w') -> Sym (WordN w')
forall a. Term a -> Sym a
Sym (Term (WordN w') -> Sym (WordN w'))
-> Term (WordN w') -> Sym (WordN w')
forall a b. (a -> b) -> a -> b
$ Bool -> Proxy w' -> Term (WordN w) -> Term (WordN w')
forall (proxy :: Nat -> *) (a :: Nat) (n :: Nat) (b :: Nat)
       (bv :: Nat -> *).
(KnownNat a, KnownNat b, KnownNat n, BVExtend (bv a) n (bv b),
 SupportedPrim (bv a), SupportedPrim (bv b)) =>
Bool -> proxy n -> Term (bv a) -> Term (bv b)
pevalBVExtendTerm Bool
False (forall {k} (t :: k). Proxy t
forall {t :: Nat}. Proxy t
Proxy @w') Term (WordN w)
v
  bvsignExtend :: forall (proxy :: Nat -> *).
proxy w' -> Sym (WordN w) -> Sym (WordN w')
bvsignExtend proxy w'
_ (Sym Term (WordN w)
v) = Term (WordN w') -> Sym (WordN w')
forall a. Term a -> Sym a
Sym (Term (WordN w') -> Sym (WordN w'))
-> Term (WordN w') -> Sym (WordN w')
forall a b. (a -> b) -> a -> b
$ Bool -> Proxy w' -> Term (WordN w) -> Term (WordN w')
forall (proxy :: Nat -> *) (a :: Nat) (n :: Nat) (b :: Nat)
       (bv :: Nat -> *).
(KnownNat a, KnownNat b, KnownNat n, BVExtend (bv a) n (bv b),
 SupportedPrim (bv a), SupportedPrim (bv b)) =>
Bool -> proxy n -> Term (bv a) -> Term (bv b)
pevalBVExtendTerm Bool
True (forall {k} (t :: k). Proxy t
forall {t :: Nat}. Proxy t
Proxy @w') Term (WordN w)
v
  bvextend :: forall (proxy :: Nat -> *).
proxy w' -> Sym (WordN w) -> Sym (WordN w')
bvextend = proxy w' -> Sym (WordN w) -> Sym (WordN w')
forall bv1 (n :: Nat) bv2 (proxy :: Nat -> *).
BVExtend bv1 n bv2 =>
proxy n -> bv1 -> bv2
bvzeroExtend

instance
  ( KnownNat ix,
    KnownNat w,
    KnownNat ow,
    ix + w <= ow,
    1 <= ow,
    1 <= w
  ) =>
  BVSelect (Sym (WordN ow)) ix w (Sym (WordN w))
  where
  bvselect :: forall (proxy :: Nat -> *).
proxy ix -> proxy w -> Sym (WordN ow) -> Sym (WordN w)
bvselect proxy ix
pix proxy w
pw (Sym Term (WordN ow)
v) = Term (WordN w) -> Sym (WordN w)
forall a. Term a -> Sym a
Sym (Term (WordN w) -> Sym (WordN w))
-> Term (WordN w) -> Sym (WordN w)
forall a b. (a -> b) -> a -> b
$ proxy ix -> proxy w -> Term (WordN ow) -> Term (WordN w)
forall (bv :: Nat -> *) (a :: Nat) (ix :: Nat) (w :: Nat)
       (proxy :: Nat -> *).
(SupportedPrim (bv a), SupportedPrim (bv w), KnownNat a,
 KnownNat w, KnownNat ix, BVSelect (bv a) ix w (bv w)) =>
proxy ix -> proxy w -> Term (bv a) -> Term (bv w)
pevalBVSelectTerm proxy ix
pix proxy w
pw Term (WordN ow)
v

instance (SupportedPrim (WordN n)) => Bits (Sym (WordN n)) where
  Sym Term (WordN n)
l .&. :: Sym (WordN n) -> Sym (WordN n) -> Sym (WordN n)
.&. Sym Term (WordN n)
r = Term (WordN n) -> Sym (WordN n)
forall a. Term a -> Sym a
Sym (Term (WordN n) -> Sym (WordN n))
-> Term (WordN n) -> Sym (WordN n)
forall a b. (a -> b) -> a -> b
$ Proxy (WordN n)
-> (PrimConstraint (WordN n) => Term (WordN n)) -> Term (WordN n)
forall t (proxy :: * -> *) a.
SupportedPrim t =>
proxy t -> (PrimConstraint t => a) -> a
withPrim (forall {t}. Proxy t
forall {k} (t :: k). Proxy t
Proxy @(WordN n)) ((PrimConstraint (WordN n) => Term (WordN n)) -> Term (WordN n))
-> (PrimConstraint (WordN n) => Term (WordN n)) -> Term (WordN n)
forall a b. (a -> b) -> a -> b
$ Term (WordN n) -> Term (WordN n) -> Term (WordN n)
forall a. (Bits a, SupportedPrim a) => Term a -> Term a -> Term a
pevalAndBitsTerm Term (WordN n)
l Term (WordN n)
r
  Sym Term (WordN n)
l .|. :: Sym (WordN n) -> Sym (WordN n) -> Sym (WordN n)
.|. Sym Term (WordN n)
r = Term (WordN n) -> Sym (WordN n)
forall a. Term a -> Sym a
Sym (Term (WordN n) -> Sym (WordN n))
-> Term (WordN n) -> Sym (WordN n)
forall a b. (a -> b) -> a -> b
$ Proxy (WordN n)
-> (PrimConstraint (WordN n) => Term (WordN n)) -> Term (WordN n)
forall t (proxy :: * -> *) a.
SupportedPrim t =>
proxy t -> (PrimConstraint t => a) -> a
withPrim (forall {t}. Proxy t
forall {k} (t :: k). Proxy t
Proxy @(WordN n)) ((PrimConstraint (WordN n) => Term (WordN n)) -> Term (WordN n))
-> (PrimConstraint (WordN n) => Term (WordN n)) -> Term (WordN n)
forall a b. (a -> b) -> a -> b
$ Term (WordN n) -> Term (WordN n) -> Term (WordN n)
forall a. (Bits a, SupportedPrim a) => Term a -> Term a -> Term a
pevalOrBitsTerm Term (WordN n)
l Term (WordN n)
r
  Sym Term (WordN n)
l xor :: Sym (WordN n) -> Sym (WordN n) -> Sym (WordN n)
`xor` Sym Term (WordN n)
r = Term (WordN n) -> Sym (WordN n)
forall a. Term a -> Sym a
Sym (Term (WordN n) -> Sym (WordN n))
-> Term (WordN n) -> Sym (WordN n)
forall a b. (a -> b) -> a -> b
$ Proxy (WordN n)
-> (PrimConstraint (WordN n) => Term (WordN n)) -> Term (WordN n)
forall t (proxy :: * -> *) a.
SupportedPrim t =>
proxy t -> (PrimConstraint t => a) -> a
withPrim (forall {t}. Proxy t
forall {k} (t :: k). Proxy t
Proxy @(WordN n)) ((PrimConstraint (WordN n) => Term (WordN n)) -> Term (WordN n))
-> (PrimConstraint (WordN n) => Term (WordN n)) -> Term (WordN n)
forall a b. (a -> b) -> a -> b
$ Term (WordN n) -> Term (WordN n) -> Term (WordN n)
forall a. (Bits a, SupportedPrim a) => Term a -> Term a -> Term a
pevalXorBitsTerm Term (WordN n)
l Term (WordN n)
r
  complement :: Sym (WordN n) -> Sym (WordN n)
complement (Sym Term (WordN n)
n) = Term (WordN n) -> Sym (WordN n)
forall a. Term a -> Sym a
Sym (Term (WordN n) -> Sym (WordN n))
-> Term (WordN n) -> Sym (WordN n)
forall a b. (a -> b) -> a -> b
$ Proxy (WordN n)
-> (PrimConstraint (WordN n) => Term (WordN n)) -> Term (WordN n)
forall t (proxy :: * -> *) a.
SupportedPrim t =>
proxy t -> (PrimConstraint t => a) -> a
withPrim (forall {t}. Proxy t
forall {k} (t :: k). Proxy t
Proxy @(WordN n)) ((PrimConstraint (WordN n) => Term (WordN n)) -> Term (WordN n))
-> (PrimConstraint (WordN n) => Term (WordN n)) -> Term (WordN n)
forall a b. (a -> b) -> a -> b
$ Term (WordN n) -> Term (WordN n)
forall a. (Bits a, SupportedPrim a) => Term a -> Term a
pevalComplementBitsTerm Term (WordN n)
n
  shift :: Sym (WordN n) -> Int -> Sym (WordN n)
shift (Sym Term (WordN n)
n) Int
i = Term (WordN n) -> Sym (WordN n)
forall a. Term a -> Sym a
Sym (Term (WordN n) -> Sym (WordN n))
-> Term (WordN n) -> Sym (WordN n)
forall a b. (a -> b) -> a -> b
$ Proxy (WordN n)
-> (PrimConstraint (WordN n) => Term (WordN n)) -> Term (WordN n)
forall t (proxy :: * -> *) a.
SupportedPrim t =>
proxy t -> (PrimConstraint t => a) -> a
withPrim (forall {t}. Proxy t
forall {k} (t :: k). Proxy t
Proxy @(WordN n)) ((PrimConstraint (WordN n) => Term (WordN n)) -> Term (WordN n))
-> (PrimConstraint (WordN n) => Term (WordN n)) -> Term (WordN n)
forall a b. (a -> b) -> a -> b
$ Term (WordN n) -> Int -> Term (WordN n)
forall a. (Bits a, SupportedPrim a) => Term a -> Int -> Term a
pevalShiftBitsTerm Term (WordN n)
n Int
i
  rotate :: Sym (WordN n) -> Int -> Sym (WordN n)
rotate (Sym Term (WordN n)
n) Int
i = Term (WordN n) -> Sym (WordN n)
forall a. Term a -> Sym a
Sym (Term (WordN n) -> Sym (WordN n))
-> Term (WordN n) -> Sym (WordN n)
forall a b. (a -> b) -> a -> b
$ Proxy (WordN n)
-> (PrimConstraint (WordN n) => Term (WordN n)) -> Term (WordN n)
forall t (proxy :: * -> *) a.
SupportedPrim t =>
proxy t -> (PrimConstraint t => a) -> a
withPrim (forall {t}. Proxy t
forall {k} (t :: k). Proxy t
Proxy @(WordN n)) ((PrimConstraint (WordN n) => Term (WordN n)) -> Term (WordN n))
-> (PrimConstraint (WordN n) => Term (WordN n)) -> Term (WordN n)
forall a b. (a -> b) -> a -> b
$ Term (WordN n) -> Int -> Term (WordN n)
forall a. (Bits a, SupportedPrim a) => Term a -> Int -> Term a
pevalRotateBitsTerm Term (WordN n)
n Int
i
  bitSize :: Sym (WordN n) -> Int
bitSize Sym (WordN n)
_ = Integer -> Int
forall a. Num a => Integer -> a
fromInteger (Integer -> Int) -> Integer -> Int
forall a b. (a -> b) -> a -> b
$ Proxy (WordN n) -> (PrimConstraint (WordN n) => Integer) -> Integer
forall t (proxy :: * -> *) a.
SupportedPrim t =>
proxy t -> (PrimConstraint t => a) -> a
withPrim (forall {t}. Proxy t
forall {k} (t :: k). Proxy t
Proxy @(WordN n)) ((PrimConstraint (WordN n) => Integer) -> Integer)
-> (PrimConstraint (WordN n) => Integer) -> Integer
forall a b. (a -> b) -> a -> b
$ Proxy n -> Integer
forall (n :: Nat) (proxy :: Nat -> *).
KnownNat n =>
proxy n -> Integer
natVal (forall {k} (t :: k). Proxy t
forall {t :: Nat}. Proxy t
Proxy @n)
  bitSizeMaybe :: Sym (WordN n) -> Maybe Int
bitSizeMaybe Sym (WordN n)
_ = Int -> Maybe Int
forall a. a -> Maybe a
Just (Int -> Maybe Int) -> Int -> Maybe Int
forall a b. (a -> b) -> a -> b
$ Integer -> Int
forall a. Num a => Integer -> a
fromInteger (Integer -> Int) -> Integer -> Int
forall a b. (a -> b) -> a -> b
$ Proxy (WordN n) -> (PrimConstraint (WordN n) => Integer) -> Integer
forall t (proxy :: * -> *) a.
SupportedPrim t =>
proxy t -> (PrimConstraint t => a) -> a
withPrim (forall {t}. Proxy t
forall {k} (t :: k). Proxy t
Proxy @(WordN n)) ((PrimConstraint (WordN n) => Integer) -> Integer)
-> (PrimConstraint (WordN n) => Integer) -> Integer
forall a b. (a -> b) -> a -> b
$ Proxy n -> Integer
forall (n :: Nat) (proxy :: Nat -> *).
KnownNat n =>
proxy n -> Integer
natVal (forall {k} (t :: k). Proxy t
forall {t :: Nat}. Proxy t
Proxy @n)
  isSigned :: Sym (WordN n) -> Bool
isSigned Sym (WordN n)
_ = Bool
False
  testBit :: Sym (WordN n) -> Int -> Bool
testBit (Con WordN n
n) = Proxy (WordN n)
-> (PrimConstraint (WordN n) => Int -> Bool) -> Int -> Bool
forall t (proxy :: * -> *) a.
SupportedPrim t =>
proxy t -> (PrimConstraint t => a) -> a
withPrim (forall {t}. Proxy t
forall {k} (t :: k). Proxy t
Proxy @(WordN n)) ((PrimConstraint (WordN n) => Int -> Bool) -> Int -> Bool)
-> (PrimConstraint (WordN n) => Int -> Bool) -> Int -> Bool
forall a b. (a -> b) -> a -> b
$ WordN n -> Int -> Bool
forall a. Bits a => a -> Int -> Bool
testBit WordN n
n
  testBit Sym (WordN n)
_ = String -> Int -> Bool
forall a. HasCallStack => String -> a
error String
"You cannot call testBit on symbolic variables"
  bit :: Int -> Sym (WordN n)
bit = Proxy (WordN n)
-> (PrimConstraint (WordN n) => Int -> Sym (WordN n))
-> Int
-> Sym (WordN n)
forall t (proxy :: * -> *) a.
SupportedPrim t =>
proxy t -> (PrimConstraint t => a) -> a
withPrim (forall {t}. Proxy t
forall {k} (t :: k). Proxy t
Proxy @(WordN n)) ((PrimConstraint (WordN n) => Int -> Sym (WordN n))
 -> Int -> Sym (WordN n))
-> (PrimConstraint (WordN n) => Int -> Sym (WordN n))
-> Int
-> Sym (WordN n)
forall a b. (a -> b) -> a -> b
$ WordN n -> Sym (WordN n)
forall c t. Solvable c t => c -> t
con (WordN n -> Sym (WordN n))
-> (Int -> WordN n) -> Int -> Sym (WordN n)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Int -> WordN n
forall a. Bits a => Int -> a
bit
  popCount :: Sym (WordN n) -> Int
popCount (Con WordN n
n) = Proxy (WordN n) -> (PrimConstraint (WordN n) => Int) -> Int
forall t (proxy :: * -> *) a.
SupportedPrim t =>
proxy t -> (PrimConstraint t => a) -> a
withPrim (forall {t}. Proxy t
forall {k} (t :: k). Proxy t
Proxy @(WordN n)) ((PrimConstraint (WordN n) => Int) -> Int)
-> (PrimConstraint (WordN n) => Int) -> Int
forall a b. (a -> b) -> a -> b
$ WordN n -> Int
forall a. Bits a => a -> Int
popCount WordN n
n
  popCount Sym (WordN n)
_ = String -> Int
forall a. HasCallStack => String -> a
error String
"You cannot call popCount on symbolic variables"

-- |
-- Symbolic tabular function type.
type a =~> b = Sym (a =-> b)

infixr 0 =~>

instance (SupportedPrim a, SupportedPrim b) => Function (a =~> b) where
  type Arg (a =~> b) = Sym a
  type Ret (a =~> b) = Sym b
  (Sym Term (a =-> b)
f) # :: (a =~> b) -> Arg (a =~> b) -> Ret (a =~> b)
# (Sym Term a
t) = Term b -> Sym b
forall a. Term a -> Sym a
Sym (Term b -> Sym b) -> Term b -> Sym b
forall a b. (a -> b) -> a -> b
$ Term (a =-> b) -> Term a -> Term b
forall a b.
(SupportedPrim a, SupportedPrim b) =>
Term (a =-> b) -> Term a -> Term b
pevalTabularFunApplyTerm Term (a =-> b)
f Term a
t

-- |
-- Symbolic general function type.
type a -~> b = Sym (a --> b)

infixr 0 -~>

instance (SupportedPrim a, SupportedPrim b) => Function (a -~> b) where
  type Arg (a -~> b) = Sym a
  type Ret (a -~> b) = Sym b
  (Sym Term (a --> b)
f) # :: (a -~> b) -> Arg (a -~> b) -> Ret (a -~> b)
# (Sym Term a
t) = Term b -> Sym b
forall a. Term a -> Sym a
Sym (Term b -> Sym b) -> Term b -> Sym b
forall a b. (a -> b) -> a -> b
$ Term (a --> b) -> Term a -> Term b
forall a b.
(SupportedPrim a, SupportedPrim b) =>
Term (a --> b) -> Term a -> Term b
pevalGeneralFunApplyTerm Term (a --> b)
f Term a
t

-- | Get the sum of the sizes of a list of symbolic terms.
-- Duplicate sub-terms are counted for only once.
symsSize :: [Sym a] -> Int
symsSize :: forall a. [Sym a] -> Int
symsSize = [Term a] -> Int
forall a. [Term a] -> Int
termsSize ([Term a] -> Int) -> ([Sym a] -> [Term a]) -> [Sym a] -> Int
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Sym a -> Term a) -> [Sym a] -> [Term a]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Sym a -> Term a
forall a. Sym a -> Term a
underlyingTerm

-- | Get the size of a symbolic term.
-- Duplicate sub-terms are counted for only once.
symSize :: Sym a -> Int
symSize :: forall a. Sym a -> Int
symSize = Term a -> Int
forall a. Term a -> Int
termSize (Term a -> Int) -> (Sym a -> Term a) -> Sym a -> Int
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Sym a -> Term a
forall a. Sym a -> Term a
underlyingTerm

data ModelSymPair t = (Sym t) := t deriving (Int -> ModelSymPair t -> ShowS
[ModelSymPair t] -> ShowS
ModelSymPair t -> String
(Int -> ModelSymPair t -> ShowS)
-> (ModelSymPair t -> String)
-> ([ModelSymPair t] -> ShowS)
-> Show (ModelSymPair t)
forall t. SupportedPrim t => Int -> ModelSymPair t -> ShowS
forall t. SupportedPrim t => [ModelSymPair t] -> ShowS
forall t. SupportedPrim t => ModelSymPair t -> String
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [ModelSymPair t] -> ShowS
$cshowList :: forall t. SupportedPrim t => [ModelSymPair t] -> ShowS
show :: ModelSymPair t -> String
$cshow :: forall t. SupportedPrim t => ModelSymPair t -> String
showsPrec :: Int -> ModelSymPair t -> ShowS
$cshowsPrec :: forall t. SupportedPrim t => Int -> ModelSymPair t -> ShowS
Show)

instance ModelRep (ModelSymPair t) Model SymbolSet TypedSymbol where
  buildModel :: ModelSymPair t -> Model
buildModel (Sym (SymTerm Int
_ TypedSymbol t
sym) := t
val) = TypedSymbol t -> t -> Model -> Model
forall model symbolSet (typedSymbol :: * -> *) t.
ModelOps model symbolSet typedSymbol =>
typedSymbol t -> t -> model -> model
insertValue TypedSymbol t
sym t
val Model
forall model symbolSet (typedSymbol :: * -> *).
ModelOps model symbolSet typedSymbol =>
model
emptyModel
  buildModel ModelSymPair t
_ = String -> Model
forall a. HasCallStack => String -> a
error String
"buildModel: should only use symbolic constants"

instance
  ModelRep
    ( ModelSymPair a,
      ModelSymPair b
    )
    Model
    SymbolSet
    TypedSymbol
  where
  buildModel :: (ModelSymPair a, ModelSymPair b) -> Model
buildModel
    ( Sym (SymTerm Int
_ TypedSymbol a
sym1) := a
val1,
      Sym (SymTerm Int
_ TypedSymbol b
sym2) := b
val2
      ) =
      TypedSymbol a -> a -> Model -> Model
forall model symbolSet (typedSymbol :: * -> *) t.
ModelOps model symbolSet typedSymbol =>
typedSymbol t -> t -> model -> model
insertValue TypedSymbol a
sym1 a
val1
        (Model -> Model) -> (Model -> Model) -> Model -> Model
forall b c a. (b -> c) -> (a -> b) -> a -> c
. TypedSymbol b -> b -> Model -> Model
forall model symbolSet (typedSymbol :: * -> *) t.
ModelOps model symbolSet typedSymbol =>
typedSymbol t -> t -> model -> model
insertValue TypedSymbol b
sym2 b
val2
        (Model -> Model) -> Model -> Model
forall a b. (a -> b) -> a -> b
$ Model
forall model symbolSet (typedSymbol :: * -> *).
ModelOps model symbolSet typedSymbol =>
model
emptyModel
  buildModel (ModelSymPair a, ModelSymPair b)
_ = String -> Model
forall a. HasCallStack => String -> a
error String
"buildModel: should only use symbolic constants"

instance
  ModelRep
    ( ModelSymPair a,
      ModelSymPair b,
      ModelSymPair c
    )
    Model
    SymbolSet
    TypedSymbol
  where
  buildModel :: (ModelSymPair a, ModelSymPair b, ModelSymPair c) -> Model
buildModel
    ( Sym (SymTerm Int
_ TypedSymbol a
sym1) := a
val1,
      Sym (SymTerm Int
_ TypedSymbol b
sym2) := b
val2,
      Sym (SymTerm Int
_ TypedSymbol c
sym3) := c
val3
      ) =
      TypedSymbol a -> a -> Model -> Model
forall model symbolSet (typedSymbol :: * -> *) t.
ModelOps model symbolSet typedSymbol =>
typedSymbol t -> t -> model -> model
insertValue TypedSymbol a
sym1 a
val1
        (Model -> Model) -> (Model -> Model) -> Model -> Model
forall b c a. (b -> c) -> (a -> b) -> a -> c
. TypedSymbol b -> b -> Model -> Model
forall model symbolSet (typedSymbol :: * -> *) t.
ModelOps model symbolSet typedSymbol =>
typedSymbol t -> t -> model -> model
insertValue TypedSymbol b
sym2 b
val2
        (Model -> Model) -> (Model -> Model) -> Model -> Model
forall b c a. (b -> c) -> (a -> b) -> a -> c
. TypedSymbol c -> c -> Model -> Model
forall model symbolSet (typedSymbol :: * -> *) t.
ModelOps model symbolSet typedSymbol =>
typedSymbol t -> t -> model -> model
insertValue TypedSymbol c
sym3 c
val3
        (Model -> Model) -> Model -> Model
forall a b. (a -> b) -> a -> b
$ Model
forall model symbolSet (typedSymbol :: * -> *).
ModelOps model symbolSet typedSymbol =>
model
emptyModel
  buildModel (ModelSymPair a, ModelSymPair b, ModelSymPair c)
_ = String -> Model
forall a. HasCallStack => String -> a
error String
"buildModel: should only use symbolic constants"

instance
  ModelRep
    ( ModelSymPair a,
      ModelSymPair b,
      ModelSymPair c,
      ModelSymPair d
    )
    Model
    SymbolSet
    TypedSymbol
  where
  buildModel :: (ModelSymPair a, ModelSymPair b, ModelSymPair c, ModelSymPair d)
-> Model
buildModel
    ( Sym (SymTerm Int
_ TypedSymbol a
sym1) := a
val1,
      Sym (SymTerm Int
_ TypedSymbol b
sym2) := b
val2,
      Sym (SymTerm Int
_ TypedSymbol c
sym3) := c
val3,
      Sym (SymTerm Int
_ TypedSymbol d
sym4) := d
val4
      ) =
      TypedSymbol a -> a -> Model -> Model
forall model symbolSet (typedSymbol :: * -> *) t.
ModelOps model symbolSet typedSymbol =>
typedSymbol t -> t -> model -> model
insertValue TypedSymbol a
sym1 a
val1
        (Model -> Model) -> (Model -> Model) -> Model -> Model
forall b c a. (b -> c) -> (a -> b) -> a -> c
. TypedSymbol b -> b -> Model -> Model
forall model symbolSet (typedSymbol :: * -> *) t.
ModelOps model symbolSet typedSymbol =>
typedSymbol t -> t -> model -> model
insertValue TypedSymbol b
sym2 b
val2
        (Model -> Model) -> (Model -> Model) -> Model -> Model
forall b c a. (b -> c) -> (a -> b) -> a -> c
. TypedSymbol c -> c -> Model -> Model
forall model symbolSet (typedSymbol :: * -> *) t.
ModelOps model symbolSet typedSymbol =>
typedSymbol t -> t -> model -> model
insertValue TypedSymbol c
sym3 c
val3
        (Model -> Model) -> (Model -> Model) -> Model -> Model
forall b c a. (b -> c) -> (a -> b) -> a -> c
. TypedSymbol d -> d -> Model -> Model
forall model symbolSet (typedSymbol :: * -> *) t.
ModelOps model symbolSet typedSymbol =>
typedSymbol t -> t -> model -> model
insertValue TypedSymbol d
sym4 d
val4
        (Model -> Model) -> Model -> Model
forall a b. (a -> b) -> a -> b
$ Model
forall model symbolSet (typedSymbol :: * -> *).
ModelOps model symbolSet typedSymbol =>
model
emptyModel
  buildModel (ModelSymPair a, ModelSymPair b, ModelSymPair c, ModelSymPair d)
_ = String -> Model
forall a. HasCallStack => String -> a
error String
"buildModel: should only use symbolic constants"

instance
  ModelRep
    ( ModelSymPair a,
      ModelSymPair b,
      ModelSymPair c,
      ModelSymPair d,
      ModelSymPair e
    )
    Model
    SymbolSet
    TypedSymbol
  where
  buildModel :: (ModelSymPair a, ModelSymPair b, ModelSymPair c, ModelSymPair d,
 ModelSymPair e)
-> Model
buildModel
    ( Sym (SymTerm Int
_ TypedSymbol a
sym1) := a
val1,
      Sym (SymTerm Int
_ TypedSymbol b
sym2) := b
val2,
      Sym (SymTerm Int
_ TypedSymbol c
sym3) := c
val3,
      Sym (SymTerm Int
_ TypedSymbol d
sym4) := d
val4,
      Sym (SymTerm Int
_ TypedSymbol e
sym5) := e
val5
      ) =
      TypedSymbol a -> a -> Model -> Model
forall model symbolSet (typedSymbol :: * -> *) t.
ModelOps model symbolSet typedSymbol =>
typedSymbol t -> t -> model -> model
insertValue TypedSymbol a
sym1 a
val1
        (Model -> Model) -> (Model -> Model) -> Model -> Model
forall b c a. (b -> c) -> (a -> b) -> a -> c
. TypedSymbol b -> b -> Model -> Model
forall model symbolSet (typedSymbol :: * -> *) t.
ModelOps model symbolSet typedSymbol =>
typedSymbol t -> t -> model -> model
insertValue TypedSymbol b
sym2 b
val2
        (Model -> Model) -> (Model -> Model) -> Model -> Model
forall b c a. (b -> c) -> (a -> b) -> a -> c
. TypedSymbol c -> c -> Model -> Model
forall model symbolSet (typedSymbol :: * -> *) t.
ModelOps model symbolSet typedSymbol =>
typedSymbol t -> t -> model -> model
insertValue TypedSymbol c
sym3 c
val3
        (Model -> Model) -> (Model -> Model) -> Model -> Model
forall b c a. (b -> c) -> (a -> b) -> a -> c
. TypedSymbol d -> d -> Model -> Model
forall model symbolSet (typedSymbol :: * -> *) t.
ModelOps model symbolSet typedSymbol =>
typedSymbol t -> t -> model -> model
insertValue TypedSymbol d
sym4 d
val4
        (Model -> Model) -> (Model -> Model) -> Model -> Model
forall b c a. (b -> c) -> (a -> b) -> a -> c
. TypedSymbol e -> e -> Model -> Model
forall model symbolSet (typedSymbol :: * -> *) t.
ModelOps model symbolSet typedSymbol =>
typedSymbol t -> t -> model -> model
insertValue TypedSymbol e
sym5 e
val5
        (Model -> Model) -> Model -> Model
forall a b. (a -> b) -> a -> b
$ Model
forall model symbolSet (typedSymbol :: * -> *).
ModelOps model symbolSet typedSymbol =>
model
emptyModel
  buildModel (ModelSymPair a, ModelSymPair b, ModelSymPair c, ModelSymPair d,
 ModelSymPair e)
_ = String -> Model
forall a. HasCallStack => String -> a
error String
"buildModel: should only use symbolic constants"

instance
  ModelRep
    ( ModelSymPair a,
      ModelSymPair b,
      ModelSymPair c,
      ModelSymPair d,
      ModelSymPair e,
      ModelSymPair f
    )
    Model
    SymbolSet
    TypedSymbol
  where
  buildModel :: (ModelSymPair a, ModelSymPair b, ModelSymPair c, ModelSymPair d,
 ModelSymPair e, ModelSymPair f)
-> Model
buildModel
    ( Sym (SymTerm Int
_ TypedSymbol a
sym1) := a
val1,
      Sym (SymTerm Int
_ TypedSymbol b
sym2) := b
val2,
      Sym (SymTerm Int
_ TypedSymbol c
sym3) := c
val3,
      Sym (SymTerm Int
_ TypedSymbol d
sym4) := d
val4,
      Sym (SymTerm Int
_ TypedSymbol e
sym5) := e
val5,
      Sym (SymTerm Int
_ TypedSymbol f
sym6) := f
val6
      ) =
      TypedSymbol a -> a -> Model -> Model
forall model symbolSet (typedSymbol :: * -> *) t.
ModelOps model symbolSet typedSymbol =>
typedSymbol t -> t -> model -> model
insertValue TypedSymbol a
sym1 a
val1
        (Model -> Model) -> (Model -> Model) -> Model -> Model
forall b c a. (b -> c) -> (a -> b) -> a -> c
. TypedSymbol b -> b -> Model -> Model
forall model symbolSet (typedSymbol :: * -> *) t.
ModelOps model symbolSet typedSymbol =>
typedSymbol t -> t -> model -> model
insertValue TypedSymbol b
sym2 b
val2
        (Model -> Model) -> (Model -> Model) -> Model -> Model
forall b c a. (b -> c) -> (a -> b) -> a -> c
. TypedSymbol c -> c -> Model -> Model
forall model symbolSet (typedSymbol :: * -> *) t.
ModelOps model symbolSet typedSymbol =>
typedSymbol t -> t -> model -> model
insertValue TypedSymbol c
sym3 c
val3
        (Model -> Model) -> (Model -> Model) -> Model -> Model
forall b c a. (b -> c) -> (a -> b) -> a -> c
. TypedSymbol d -> d -> Model -> Model
forall model symbolSet (typedSymbol :: * -> *) t.
ModelOps model symbolSet typedSymbol =>
typedSymbol t -> t -> model -> model
insertValue TypedSymbol d
sym4 d
val4
        (Model -> Model) -> (Model -> Model) -> Model -> Model
forall b c a. (b -> c) -> (a -> b) -> a -> c
. TypedSymbol e -> e -> Model -> Model
forall model symbolSet (typedSymbol :: * -> *) t.
ModelOps model symbolSet typedSymbol =>
typedSymbol t -> t -> model -> model
insertValue TypedSymbol e
sym5 e
val5
        (Model -> Model) -> (Model -> Model) -> Model -> Model
forall b c a. (b -> c) -> (a -> b) -> a -> c
. TypedSymbol f -> f -> Model -> Model
forall model symbolSet (typedSymbol :: * -> *) t.
ModelOps model symbolSet typedSymbol =>
typedSymbol t -> t -> model -> model
insertValue TypedSymbol f
sym6 f
val6
        (Model -> Model) -> Model -> Model
forall a b. (a -> b) -> a -> b
$ Model
forall model symbolSet (typedSymbol :: * -> *).
ModelOps model symbolSet typedSymbol =>
model
emptyModel
  buildModel (ModelSymPair a, ModelSymPair b, ModelSymPair c, ModelSymPair d,
 ModelSymPair e, ModelSymPair f)
_ = String -> Model
forall a. HasCallStack => String -> a
error String
"buildModel: should only use symbolic constants"

instance
  ModelRep
    ( ModelSymPair a,
      ModelSymPair b,
      ModelSymPair c,
      ModelSymPair d,
      ModelSymPair e,
      ModelSymPair f,
      ModelSymPair g
    )
    Model
    SymbolSet
    TypedSymbol
  where
  buildModel :: (ModelSymPair a, ModelSymPair b, ModelSymPair c, ModelSymPair d,
 ModelSymPair e, ModelSymPair f, ModelSymPair g)
-> Model
buildModel
    ( Sym (SymTerm Int
_ TypedSymbol a
sym1) := a
val1,
      Sym (SymTerm Int
_ TypedSymbol b
sym2) := b
val2,
      Sym (SymTerm Int
_ TypedSymbol c
sym3) := c
val3,
      Sym (SymTerm Int
_ TypedSymbol d
sym4) := d
val4,
      Sym (SymTerm Int
_ TypedSymbol e
sym5) := e
val5,
      Sym (SymTerm Int
_ TypedSymbol f
sym6) := f
val6,
      Sym (SymTerm Int
_ TypedSymbol g
sym7) := g
val7
      ) =
      TypedSymbol a -> a -> Model -> Model
forall model symbolSet (typedSymbol :: * -> *) t.
ModelOps model symbolSet typedSymbol =>
typedSymbol t -> t -> model -> model
insertValue TypedSymbol a
sym1 a
val1
        (Model -> Model) -> (Model -> Model) -> Model -> Model
forall b c a. (b -> c) -> (a -> b) -> a -> c
. TypedSymbol b -> b -> Model -> Model
forall model symbolSet (typedSymbol :: * -> *) t.
ModelOps model symbolSet typedSymbol =>
typedSymbol t -> t -> model -> model
insertValue TypedSymbol b
sym2 b
val2
        (Model -> Model) -> (Model -> Model) -> Model -> Model
forall b c a. (b -> c) -> (a -> b) -> a -> c
. TypedSymbol c -> c -> Model -> Model
forall model symbolSet (typedSymbol :: * -> *) t.
ModelOps model symbolSet typedSymbol =>
typedSymbol t -> t -> model -> model
insertValue TypedSymbol c
sym3 c
val3
        (Model -> Model) -> (Model -> Model) -> Model -> Model
forall b c a. (b -> c) -> (a -> b) -> a -> c
. TypedSymbol d -> d -> Model -> Model
forall model symbolSet (typedSymbol :: * -> *) t.
ModelOps model symbolSet typedSymbol =>
typedSymbol t -> t -> model -> model
insertValue TypedSymbol d
sym4 d
val4
        (Model -> Model) -> (Model -> Model) -> Model -> Model
forall b c a. (b -> c) -> (a -> b) -> a -> c
. TypedSymbol e -> e -> Model -> Model
forall model symbolSet (typedSymbol :: * -> *) t.
ModelOps model symbolSet typedSymbol =>
typedSymbol t -> t -> model -> model
insertValue TypedSymbol e
sym5 e
val5
        (Model -> Model) -> (Model -> Model) -> Model -> Model
forall b c a. (b -> c) -> (a -> b) -> a -> c
. TypedSymbol f -> f -> Model -> Model
forall model symbolSet (typedSymbol :: * -> *) t.
ModelOps model symbolSet typedSymbol =>
typedSymbol t -> t -> model -> model
insertValue TypedSymbol f
sym6 f
val6
        (Model -> Model) -> (Model -> Model) -> Model -> Model
forall b c a. (b -> c) -> (a -> b) -> a -> c
. TypedSymbol g -> g -> Model -> Model
forall model symbolSet (typedSymbol :: * -> *) t.
ModelOps model symbolSet typedSymbol =>
typedSymbol t -> t -> model -> model
insertValue TypedSymbol g
sym7 g
val7
        (Model -> Model) -> Model -> Model
forall a b. (a -> b) -> a -> b
$ Model
forall model symbolSet (typedSymbol :: * -> *).
ModelOps model symbolSet typedSymbol =>
model
emptyModel
  buildModel (ModelSymPair a, ModelSymPair b, ModelSymPair c, ModelSymPair d,
 ModelSymPair e, ModelSymPair f, ModelSymPair g)
_ = String -> Model
forall a. HasCallStack => String -> a
error String
"buildModel: should only use symbolic constants"

instance
  ModelRep
    ( ModelSymPair a,
      ModelSymPair b,
      ModelSymPair c,
      ModelSymPair d,
      ModelSymPair e,
      ModelSymPair f,
      ModelSymPair g,
      ModelSymPair h
    )
    Model
    SymbolSet
    TypedSymbol
  where
  buildModel :: (ModelSymPair a, ModelSymPair b, ModelSymPair c, ModelSymPair d,
 ModelSymPair e, ModelSymPair f, ModelSymPair g, ModelSymPair h)
-> Model
buildModel
    ( Sym (SymTerm Int
_ TypedSymbol a
sym1) := a
val1,
      Sym (SymTerm Int
_ TypedSymbol b
sym2) := b
val2,
      Sym (SymTerm Int
_ TypedSymbol c
sym3) := c
val3,
      Sym (SymTerm Int
_ TypedSymbol d
sym4) := d
val4,
      Sym (SymTerm Int
_ TypedSymbol e
sym5) := e
val5,
      Sym (SymTerm Int
_ TypedSymbol f
sym6) := f
val6,
      Sym (SymTerm Int
_ TypedSymbol g
sym7) := g
val7,
      Sym (SymTerm Int
_ TypedSymbol h
sym8) := h
val8
      ) =
      TypedSymbol a -> a -> Model -> Model
forall model symbolSet (typedSymbol :: * -> *) t.
ModelOps model symbolSet typedSymbol =>
typedSymbol t -> t -> model -> model
insertValue TypedSymbol a
sym1 a
val1
        (Model -> Model) -> (Model -> Model) -> Model -> Model
forall b c a. (b -> c) -> (a -> b) -> a -> c
. TypedSymbol b -> b -> Model -> Model
forall model symbolSet (typedSymbol :: * -> *) t.
ModelOps model symbolSet typedSymbol =>
typedSymbol t -> t -> model -> model
insertValue TypedSymbol b
sym2 b
val2
        (Model -> Model) -> (Model -> Model) -> Model -> Model
forall b c a. (b -> c) -> (a -> b) -> a -> c
. TypedSymbol c -> c -> Model -> Model
forall model symbolSet (typedSymbol :: * -> *) t.
ModelOps model symbolSet typedSymbol =>
typedSymbol t -> t -> model -> model
insertValue TypedSymbol c
sym3 c
val3
        (Model -> Model) -> (Model -> Model) -> Model -> Model
forall b c a. (b -> c) -> (a -> b) -> a -> c
. TypedSymbol d -> d -> Model -> Model
forall model symbolSet (typedSymbol :: * -> *) t.
ModelOps model symbolSet typedSymbol =>
typedSymbol t -> t -> model -> model
insertValue TypedSymbol d
sym4 d
val4
        (Model -> Model) -> (Model -> Model) -> Model -> Model
forall b c a. (b -> c) -> (a -> b) -> a -> c
. TypedSymbol e -> e -> Model -> Model
forall model symbolSet (typedSymbol :: * -> *) t.
ModelOps model symbolSet typedSymbol =>
typedSymbol t -> t -> model -> model
insertValue TypedSymbol e
sym5 e
val5
        (Model -> Model) -> (Model -> Model) -> Model -> Model
forall b c a. (b -> c) -> (a -> b) -> a -> c
. TypedSymbol f -> f -> Model -> Model
forall model symbolSet (typedSymbol :: * -> *) t.
ModelOps model symbolSet typedSymbol =>
typedSymbol t -> t -> model -> model
insertValue TypedSymbol f
sym6 f
val6
        (Model -> Model) -> (Model -> Model) -> Model -> Model
forall b c a. (b -> c) -> (a -> b) -> a -> c
. TypedSymbol g -> g -> Model -> Model
forall model symbolSet (typedSymbol :: * -> *) t.
ModelOps model symbolSet typedSymbol =>
typedSymbol t -> t -> model -> model
insertValue TypedSymbol g
sym7 g
val7
        (Model -> Model) -> (Model -> Model) -> Model -> Model
forall b c a. (b -> c) -> (a -> b) -> a -> c
. TypedSymbol h -> h -> Model -> Model
forall model symbolSet (typedSymbol :: * -> *) t.
ModelOps model symbolSet typedSymbol =>
typedSymbol t -> t -> model -> model
insertValue TypedSymbol h
sym8 h
val8
        (Model -> Model) -> Model -> Model
forall a b. (a -> b) -> a -> b
$ Model
forall model symbolSet (typedSymbol :: * -> *).
ModelOps model symbolSet typedSymbol =>
model
emptyModel
  buildModel (ModelSymPair a, ModelSymPair b, ModelSymPair c, ModelSymPair d,
 ModelSymPair e, ModelSymPair f, ModelSymPair g, ModelSymPair h)
_ = String -> Model
forall a. HasCallStack => String -> a
error String
"buildModel: should only use symbolic constants"

instance (SupportedPrim a, SupportedPrim b) => Function (a --> b) where
  type Arg (a --> b) = Sym a
  type Ret (a --> b) = Sym b
  (GeneralFun TypedSymbol a
arg Term b
tm) # :: (a --> b) -> Arg (a --> b) -> Ret (a --> b)
# (Sym Term a
v) = Term b -> Sym b
forall a. Term a -> Sym a
Sym (Term b -> Sym b) -> Term b -> Sym b
forall a b. (a -> b) -> a -> b
$ TypedSymbol a -> Term a -> Term b -> Term b
forall a b.
(SupportedPrim a, SupportedPrim b) =>
TypedSymbol a -> Term a -> Term b -> Term b
substTerm TypedSymbol a
arg Term a
v Term b
tm

-- | Construction of general symbolic functions.
(-->) :: (SupportedPrim a, SupportedPrim b) => TypedSymbol a -> Sym b -> a --> b
--> :: forall a b.
(SupportedPrim a, SupportedPrim b) =>
TypedSymbol a -> Sym b -> a --> b
(-->) TypedSymbol a
arg (Sym Term b
v) = TypedSymbol a -> Term b -> a --> b
forall a b.
(SupportedPrim a, SupportedPrim b) =>
TypedSymbol a -> Term b -> a --> b
GeneralFun TypedSymbol a
arg Term b
v