{-# 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 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 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) = forall a. NFData a => a -> ()
rnf Term a
t

instance (SupportedPrim a) => Solvable a (Sym a) where
  con :: a -> Sym a
con = forall a. Term a -> Sym a
Sym forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall t.
(SupportedPrim t, Typeable t, Hashable t, Eq t, Show t) =>
t -> Term t
conTerm
  ssym :: String -> Sym a
ssym = forall a. Term a -> Sym a
Sym forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall t. (SupportedPrim t, Typeable t) => String -> Term t
ssymTerm
  isym :: String -> Int -> Sym a
isym String
str Int
i = forall a. Term a -> Sym a
Sym forall a b. (a -> b) -> a -> b
$ 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 = forall a. Term a -> Sym a
Sym forall a b. (a -> b) -> a -> b
$ 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 = forall a. Term a -> Sym a
Sym forall a b. (a -> b) -> a -> b
$ 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)) = forall a. a -> Maybe a
Just a
t
  conView Sym a
_ = forall a. Maybe a
Nothing

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

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

instance (SupportedPrim a) => ToSym a (Sym a) where
  toSym :: a -> Sym a
toSym = 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 = forall a. a -> Maybe a
Just

instance (SupportedPrim a) => ToCon (Sym a) a where
  toCon :: Sym a -> Maybe a
toCon = 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) = forall a. Term a -> Sym a
Sym forall a b. (a -> b) -> a -> b
$ 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 forall a b. (a -> b) -> a -> b
$ 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) = 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 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 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 = forall b. LogicalOp b => b -> b
nots Sym Bool
l forall b. LogicalOp b => b -> b -> b
||~ Sym Bool
r
  Sym Bool
l <~ :: Sym Bool -> Sym Bool -> Sym Bool
<~ Sym Bool
r = forall b. LogicalOp b => b -> b
nots Sym Bool
l 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 forall b. LogicalOp b => b -> b -> b
||~ 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 forall b. LogicalOp b => b -> b -> b
&&~ forall b. LogicalOp b => b -> b
nots Sym Bool
r
  symCompare :: Sym Bool -> Sym Bool -> UnionM Ordering
symCompare Sym Bool
l Sym Bool
r =
    forall (u :: * -> *) a.
(UnionLike u, Mergeable a) =>
Sym Bool -> u a -> u a -> u a
mrgIf
      (forall b. LogicalOp b => b -> b
nots Sym Bool
l forall b. LogicalOp b => b -> b -> b
&&~ Sym Bool
r)
      (forall (u :: * -> *) a. (MonadUnion u, Mergeable a) => a -> u a
mrgReturn Ordering
LT)
      (forall (u :: * -> *) a.
(UnionLike u, Mergeable a) =>
Sym Bool -> u a -> u a -> u a
mrgIf (Sym Bool
l forall a. SEq a => a -> a -> Sym Bool
==~ Sym Bool
r) (forall (u :: * -> *) a. (MonadUnion u, Mergeable a) => a -> u a
mrgReturn Ordering
EQ) (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) = forall a. Term a -> Sym a
Sym forall a b. (a -> b) -> a -> b
$ 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) = forall a. Term a -> Sym a
Sym forall a b. (a -> b) -> a -> b
$ 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) = forall a. Term a -> Sym a
Sym forall a b. (a -> b) -> a -> b
$ 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) = forall a. Term a -> Sym a
Sym forall a b. (a -> b) -> a -> b
$ forall a. (Num a, SupportedPrim a) => Term a -> Term a
pevalUMinusNumTerm Term Integer
v
  abs :: Sym Integer -> Sym Integer
abs (Sym Term Integer
v) = forall a. Term a -> Sym a
Sym forall a b. (a -> b) -> a -> b
$ forall a. (SupportedPrim a, Num a) => Term a -> Term a
pevalAbsNumTerm Term Integer
v
  signum :: Sym Integer -> Sym Integer
signum (Sym Term Integer
v) = forall a. Term a -> Sym a
Sym forall a b. (a -> b) -> a -> b
$ forall a. (Num a, SupportedPrim a) => Term a -> Term a
pevalSignumNumTerm Term Integer
v
  fromInteger :: Integer -> Sym Integer
fromInteger = 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) =
    forall (u :: * -> *) a.
(UnionLike u, Mergeable a) =>
Sym Bool -> u a -> u a -> u a
mrgIf
      (Sym Integer
rs forall a. SEq a => a -> a -> Sym Bool
==~ forall c t. Solvable c t => c -> t
con Integer
0)
      (forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError forall a b. (a -> b) -> a -> b
$ forall from to. TransformError from to => from -> to
transformError ArithException
DivideByZero)
      (forall (u :: * -> *) a. (MonadUnion u, Mergeable a) => a -> u a
mrgReturn forall a b. (a -> b) -> a -> b
$ forall a. Term a -> Sym a
Sym 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) =
    forall (u :: * -> *) a.
(UnionLike u, Mergeable a) =>
Sym Bool -> u a -> u a -> u a
mrgIf
      (Sym Integer
rs forall a. SEq a => a -> a -> Sym Bool
==~ forall c t. Solvable c t => c -> t
con Integer
0)
      (forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError forall a b. (a -> b) -> a -> b
$ forall from to. TransformError from to => from -> to
transformError ArithException
DivideByZero)
      (forall (u :: * -> *) a. (MonadUnion u, Mergeable a) => a -> u a
mrgReturn forall a b. (a -> b) -> a -> b
$ forall a. Term a -> Sym a
Sym 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) = forall a. Term a -> Sym a
Sym forall a b. (a -> b) -> a -> b
$ forall t (proxy :: * -> *) a.
SupportedPrim t =>
proxy t -> (PrimConstraint t => a) -> a
withPrim (forall {k} (t :: k). Proxy t
Proxy @(IntN n)) forall a b. (a -> b) -> a -> b
$ 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) = forall a. Term a -> Sym a
Sym forall a b. (a -> b) -> a -> b
$ forall t (proxy :: * -> *) a.
SupportedPrim t =>
proxy t -> (PrimConstraint t => a) -> a
withPrim (forall {k} (t :: k). Proxy t
Proxy @(IntN n)) forall a b. (a -> b) -> a -> b
$ 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) = forall a. Term a -> Sym a
Sym forall a b. (a -> b) -> a -> b
$ forall t (proxy :: * -> *) a.
SupportedPrim t =>
proxy t -> (PrimConstraint t => a) -> a
withPrim (forall {k} (t :: k). Proxy t
Proxy @(IntN n)) forall a b. (a -> b) -> a -> b
$ 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) = forall a. Term a -> Sym a
Sym forall a b. (a -> b) -> a -> b
$ forall t (proxy :: * -> *) a.
SupportedPrim t =>
proxy t -> (PrimConstraint t => a) -> a
withPrim (forall {k} (t :: k). Proxy t
Proxy @(IntN n)) forall a b. (a -> b) -> a -> b
$ 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) = forall a. Term a -> Sym a
Sym forall a b. (a -> b) -> a -> b
$ forall t (proxy :: * -> *) a.
SupportedPrim t =>
proxy t -> (PrimConstraint t => a) -> a
withPrim (forall {k} (t :: k). Proxy t
Proxy @(IntN n)) forall a b. (a -> b) -> a -> b
$ 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) = forall a. Term a -> Sym a
Sym forall a b. (a -> b) -> a -> b
$ forall t (proxy :: * -> *) a.
SupportedPrim t =>
proxy t -> (PrimConstraint t => a) -> a
withPrim (forall {k} (t :: k). Proxy t
Proxy @(IntN n)) forall a b. (a -> b) -> a -> b
$ forall a. (Num a, SupportedPrim a) => Term a -> Term a
pevalSignumNumTerm Term (IntN n)
v
  fromInteger :: Integer -> Sym (IntN n)
fromInteger Integer
i = forall t (proxy :: * -> *) a.
SupportedPrim t =>
proxy t -> (PrimConstraint t => a) -> a
withPrim (forall {k} (t :: k). Proxy t
Proxy @(IntN n)) forall a b. (a -> b) -> a -> b
$ forall c t. Solvable c t => c -> t
con forall a b. (a -> b) -> a -> b
$ 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 = forall a. Term a -> Sym a
Sym forall a b. (a -> b) -> a -> b
$ forall t (proxy :: * -> *) a.
SupportedPrim t =>
proxy t -> (PrimConstraint t => a) -> a
withPrim (forall {k} (t :: k). Proxy t
Proxy @(IntN n)) forall a b. (a -> b) -> a -> b
$ 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 = forall a. Term a -> Sym a
Sym forall a b. (a -> b) -> a -> b
$ forall t (proxy :: * -> *) a.
SupportedPrim t =>
proxy t -> (PrimConstraint t => a) -> a
withPrim (forall {k} (t :: k). Proxy t
Proxy @(IntN n)) forall a b. (a -> b) -> a -> b
$ 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 = forall a. Term a -> Sym a
Sym forall a b. (a -> b) -> a -> b
$ forall t (proxy :: * -> *) a.
SupportedPrim t =>
proxy t -> (PrimConstraint t => a) -> a
withPrim (forall {k} (t :: k). Proxy t
Proxy @(IntN n)) forall a b. (a -> b) -> a -> b
$ 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) = forall a. Term a -> Sym a
Sym forall a b. (a -> b) -> a -> b
$ forall t (proxy :: * -> *) a.
SupportedPrim t =>
proxy t -> (PrimConstraint t => a) -> a
withPrim (forall {k} (t :: k). Proxy t
Proxy @(IntN n)) forall a b. (a -> b) -> a -> b
$ 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 = forall a. Term a -> Sym a
Sym forall a b. (a -> b) -> a -> b
$ forall t (proxy :: * -> *) a.
SupportedPrim t =>
proxy t -> (PrimConstraint t => a) -> a
withPrim (forall {k} (t :: k). Proxy t
Proxy @(IntN n)) forall a b. (a -> b) -> a -> b
$ 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 = forall a. Term a -> Sym a
Sym forall a b. (a -> b) -> a -> b
$ forall t (proxy :: * -> *) a.
SupportedPrim t =>
proxy t -> (PrimConstraint t => a) -> a
withPrim (forall {k} (t :: k). Proxy t
Proxy @(IntN n)) forall a b. (a -> b) -> a -> b
$ 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)
_ = forall a. Num a => Integer -> a
fromInteger forall a b. (a -> b) -> a -> b
$ forall t (proxy :: * -> *) a.
SupportedPrim t =>
proxy t -> (PrimConstraint t => a) -> a
withPrim (forall {k} (t :: k). Proxy t
Proxy @(IntN n)) forall a b. (a -> b) -> a -> b
$ forall (n :: Nat) (proxy :: Nat -> *).
KnownNat n =>
proxy n -> Integer
natVal (forall {k} (t :: k). Proxy t
Proxy @n)
  bitSizeMaybe :: Sym (IntN n) -> Maybe Int
bitSizeMaybe Sym (IntN n)
_ = forall a. a -> Maybe a
Just forall a b. (a -> b) -> a -> b
$ forall a. Num a => Integer -> a
fromInteger forall a b. (a -> b) -> a -> b
$ forall t (proxy :: * -> *) a.
SupportedPrim t =>
proxy t -> (PrimConstraint t => a) -> a
withPrim (forall {k} (t :: k). Proxy t
Proxy @(IntN n)) forall a b. (a -> b) -> a -> b
$ forall (n :: Nat) (proxy :: Nat -> *).
KnownNat n =>
proxy n -> Integer
natVal (forall {k} (t :: k). 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) = forall t (proxy :: * -> *) a.
SupportedPrim t =>
proxy t -> (PrimConstraint t => a) -> a
withPrim (forall {k} (t :: k). Proxy t
Proxy @(IntN n)) forall a b. (a -> b) -> a -> b
$ forall a. Bits a => a -> Int -> Bool
testBit IntN n
n
  testBit Sym (IntN n)
_ = forall a. HasCallStack => String -> a
error String
"You cannot call testBit on symbolic variables"
  bit :: Int -> Sym (IntN n)
bit = forall t (proxy :: * -> *) a.
SupportedPrim t =>
proxy t -> (PrimConstraint t => a) -> a
withPrim (forall {k} (t :: k). Proxy t
Proxy @(IntN n)) forall a b. (a -> b) -> a -> b
$ forall c t. Solvable c t => c -> t
con forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. Bits a => Int -> a
bit
  popCount :: Sym (IntN n) -> Int
popCount (Con IntN n
n) = forall t (proxy :: * -> *) a.
SupportedPrim t =>
proxy t -> (PrimConstraint t => a) -> a
withPrim (forall {k} (t :: k). Proxy t
Proxy @(IntN n)) forall a b. (a -> b) -> a -> b
$ forall a. Bits a => a -> Int
popCount IntN n
n
  popCount Sym (IntN n)
_ = 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) = forall a. Term a -> Sym a
Sym (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) = forall a. Term a -> Sym a
Sym forall a b. (a -> b) -> a -> b
$ 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
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) = forall a. Term a -> Sym a
Sym forall a b. (a -> b) -> a -> b
$ 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
Proxy @w') Term (IntN w)
v
  bvextend :: forall (proxy :: Nat -> *).
proxy w' -> Sym (IntN w) -> Sym (IntN w')
bvextend = 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) = forall a. Term a -> Sym a
Sym forall a b. (a -> b) -> a -> b
$ 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) = forall a. Term a -> Sym a
Sym forall a b. (a -> b) -> a -> b
$ forall t (proxy :: * -> *) a.
SupportedPrim t =>
proxy t -> (PrimConstraint t => a) -> a
withPrim (forall {k} (t :: k). Proxy t
Proxy @(WordN n)) forall a b. (a -> b) -> a -> b
$ 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) = forall a. Term a -> Sym a
Sym forall a b. (a -> b) -> a -> b
$ forall t (proxy :: * -> *) a.
SupportedPrim t =>
proxy t -> (PrimConstraint t => a) -> a
withPrim (forall {k} (t :: k). Proxy t
Proxy @(WordN n)) forall a b. (a -> b) -> a -> b
$ 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) = forall a. Term a -> Sym a
Sym forall a b. (a -> b) -> a -> b
$ forall t (proxy :: * -> *) a.
SupportedPrim t =>
proxy t -> (PrimConstraint t => a) -> a
withPrim (forall {k} (t :: k). Proxy t
Proxy @(WordN n)) forall a b. (a -> b) -> a -> b
$ 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) = forall a. Term a -> Sym a
Sym forall a b. (a -> b) -> a -> b
$ forall t (proxy :: * -> *) a.
SupportedPrim t =>
proxy t -> (PrimConstraint t => a) -> a
withPrim (forall {k} (t :: k). Proxy t
Proxy @(WordN n)) forall a b. (a -> b) -> a -> b
$ 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) = forall a. Term a -> Sym a
Sym forall a b. (a -> b) -> a -> b
$ forall t (proxy :: * -> *) a.
SupportedPrim t =>
proxy t -> (PrimConstraint t => a) -> a
withPrim (forall {k} (t :: k). Proxy t
Proxy @(WordN n)) forall a b. (a -> b) -> a -> b
$ 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) = forall a. Term a -> Sym a
Sym forall a b. (a -> b) -> a -> b
$ forall t (proxy :: * -> *) a.
SupportedPrim t =>
proxy t -> (PrimConstraint t => a) -> a
withPrim (forall {k} (t :: k). Proxy t
Proxy @(WordN n)) forall a b. (a -> b) -> a -> b
$ forall a. (Num a, SupportedPrim a) => Term a -> Term a
pevalSignumNumTerm Term (WordN n)
v
  fromInteger :: Integer -> Sym (WordN n)
fromInteger Integer
i = forall t (proxy :: * -> *) a.
SupportedPrim t =>
proxy t -> (PrimConstraint t => a) -> a
withPrim (forall {k} (t :: k). Proxy t
Proxy @(WordN n)) forall a b. (a -> b) -> a -> b
$ forall c t. Solvable c t => c -> t
con forall a b. (a -> b) -> a -> b
$ 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) = forall a. Term a -> Sym a
Sym (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) = forall a. Term a -> Sym a
Sym forall a b. (a -> b) -> a -> b
$ 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
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) = forall a. Term a -> Sym a
Sym forall a b. (a -> b) -> a -> b
$ 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
Proxy @w') Term (WordN w)
v
  bvextend :: forall (proxy :: Nat -> *).
proxy w' -> Sym (WordN w) -> Sym (WordN w')
bvextend = 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) = forall a. Term a -> Sym a
Sym forall a b. (a -> b) -> a -> b
$ 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 = forall a. Term a -> Sym a
Sym forall a b. (a -> b) -> a -> b
$ forall t (proxy :: * -> *) a.
SupportedPrim t =>
proxy t -> (PrimConstraint t => a) -> a
withPrim (forall {k} (t :: k). Proxy t
Proxy @(WordN n)) forall a b. (a -> b) -> a -> b
$ 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 = forall a. Term a -> Sym a
Sym forall a b. (a -> b) -> a -> b
$ forall t (proxy :: * -> *) a.
SupportedPrim t =>
proxy t -> (PrimConstraint t => a) -> a
withPrim (forall {k} (t :: k). Proxy t
Proxy @(WordN n)) forall a b. (a -> b) -> a -> b
$ 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 = forall a. Term a -> Sym a
Sym forall a b. (a -> b) -> a -> b
$ forall t (proxy :: * -> *) a.
SupportedPrim t =>
proxy t -> (PrimConstraint t => a) -> a
withPrim (forall {k} (t :: k). Proxy t
Proxy @(WordN n)) forall a b. (a -> b) -> a -> b
$ 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) = forall a. Term a -> Sym a
Sym forall a b. (a -> b) -> a -> b
$ forall t (proxy :: * -> *) a.
SupportedPrim t =>
proxy t -> (PrimConstraint t => a) -> a
withPrim (forall {k} (t :: k). Proxy t
Proxy @(WordN n)) forall a b. (a -> b) -> a -> b
$ 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 = forall a. Term a -> Sym a
Sym forall a b. (a -> b) -> a -> b
$ forall t (proxy :: * -> *) a.
SupportedPrim t =>
proxy t -> (PrimConstraint t => a) -> a
withPrim (forall {k} (t :: k). Proxy t
Proxy @(WordN n)) forall a b. (a -> b) -> a -> b
$ 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 = forall a. Term a -> Sym a
Sym forall a b. (a -> b) -> a -> b
$ forall t (proxy :: * -> *) a.
SupportedPrim t =>
proxy t -> (PrimConstraint t => a) -> a
withPrim (forall {k} (t :: k). Proxy t
Proxy @(WordN n)) forall a b. (a -> b) -> a -> b
$ 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)
_ = forall a. Num a => Integer -> a
fromInteger forall a b. (a -> b) -> a -> b
$ forall t (proxy :: * -> *) a.
SupportedPrim t =>
proxy t -> (PrimConstraint t => a) -> a
withPrim (forall {k} (t :: k). Proxy t
Proxy @(WordN n)) forall a b. (a -> b) -> a -> b
$ forall (n :: Nat) (proxy :: Nat -> *).
KnownNat n =>
proxy n -> Integer
natVal (forall {k} (t :: k). Proxy t
Proxy @n)
  bitSizeMaybe :: Sym (WordN n) -> Maybe Int
bitSizeMaybe Sym (WordN n)
_ = forall a. a -> Maybe a
Just forall a b. (a -> b) -> a -> b
$ forall a. Num a => Integer -> a
fromInteger forall a b. (a -> b) -> a -> b
$ forall t (proxy :: * -> *) a.
SupportedPrim t =>
proxy t -> (PrimConstraint t => a) -> a
withPrim (forall {k} (t :: k). Proxy t
Proxy @(WordN n)) forall a b. (a -> b) -> a -> b
$ forall (n :: Nat) (proxy :: Nat -> *).
KnownNat n =>
proxy n -> Integer
natVal (forall {k} (t :: k). 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) = forall t (proxy :: * -> *) a.
SupportedPrim t =>
proxy t -> (PrimConstraint t => a) -> a
withPrim (forall {k} (t :: k). Proxy t
Proxy @(WordN n)) forall a b. (a -> b) -> a -> b
$ forall a. Bits a => a -> Int -> Bool
testBit WordN n
n
  testBit Sym (WordN n)
_ = forall a. HasCallStack => String -> a
error String
"You cannot call testBit on symbolic variables"
  bit :: Int -> Sym (WordN n)
bit = forall t (proxy :: * -> *) a.
SupportedPrim t =>
proxy t -> (PrimConstraint t => a) -> a
withPrim (forall {k} (t :: k). Proxy t
Proxy @(WordN n)) forall a b. (a -> b) -> a -> b
$ forall c t. Solvable c t => c -> t
con forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. Bits a => Int -> a
bit
  popCount :: Sym (WordN n) -> Int
popCount (Con WordN n
n) = forall t (proxy :: * -> *) a.
SupportedPrim t =>
proxy t -> (PrimConstraint t => a) -> a
withPrim (forall {k} (t :: k). Proxy t
Proxy @(WordN n)) forall a b. (a -> b) -> a -> b
$ forall a. Bits a => a -> Int
popCount WordN n
n
  popCount Sym (WordN n)
_ = 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) = forall a. Term a -> Sym a
Sym forall a b. (a -> b) -> a -> 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) = forall a. Term a -> Sym a
Sym forall a b. (a -> b) -> a -> 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 = forall a. [Term a] -> Int
termsSize forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap 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 = forall a. Term a -> Int
termSize forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. Sym a -> Term a
underlyingTerm

data ModelSymPair t = (Sym t) := t deriving (Int -> ModelSymPair t -> ShowS
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) = forall model symbolSet (typedSymbol :: * -> *) t.
ModelOps model symbolSet typedSymbol =>
typedSymbol t -> t -> model -> model
insertValue TypedSymbol t
sym t
val forall model symbolSet (typedSymbol :: * -> *).
ModelOps model symbolSet typedSymbol =>
model
emptyModel
  buildModel ModelSymPair t
_ = 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
      ) =
      forall model symbolSet (typedSymbol :: * -> *) t.
ModelOps model symbolSet typedSymbol =>
typedSymbol t -> t -> model -> model
insertValue TypedSymbol a
sym1 a
val1
        forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall model symbolSet (typedSymbol :: * -> *) t.
ModelOps model symbolSet typedSymbol =>
typedSymbol t -> t -> model -> model
insertValue TypedSymbol b
sym2 b
val2
        forall a b. (a -> b) -> a -> b
$ forall model symbolSet (typedSymbol :: * -> *).
ModelOps model symbolSet typedSymbol =>
model
emptyModel
  buildModel (ModelSymPair a, ModelSymPair b)
_ = 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
      ) =
      forall model symbolSet (typedSymbol :: * -> *) t.
ModelOps model symbolSet typedSymbol =>
typedSymbol t -> t -> model -> model
insertValue TypedSymbol a
sym1 a
val1
        forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall model symbolSet (typedSymbol :: * -> *) t.
ModelOps model symbolSet typedSymbol =>
typedSymbol t -> t -> model -> model
insertValue TypedSymbol b
sym2 b
val2
        forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall model symbolSet (typedSymbol :: * -> *) t.
ModelOps model symbolSet typedSymbol =>
typedSymbol t -> t -> model -> model
insertValue TypedSymbol c
sym3 c
val3
        forall a b. (a -> b) -> a -> b
$ forall model symbolSet (typedSymbol :: * -> *).
ModelOps model symbolSet typedSymbol =>
model
emptyModel
  buildModel (ModelSymPair a, ModelSymPair b, ModelSymPair c)
_ = 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
      ) =
      forall model symbolSet (typedSymbol :: * -> *) t.
ModelOps model symbolSet typedSymbol =>
typedSymbol t -> t -> model -> model
insertValue TypedSymbol a
sym1 a
val1
        forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall model symbolSet (typedSymbol :: * -> *) t.
ModelOps model symbolSet typedSymbol =>
typedSymbol t -> t -> model -> model
insertValue TypedSymbol b
sym2 b
val2
        forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall model symbolSet (typedSymbol :: * -> *) t.
ModelOps model symbolSet typedSymbol =>
typedSymbol t -> t -> model -> model
insertValue TypedSymbol c
sym3 c
val3
        forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall model symbolSet (typedSymbol :: * -> *) t.
ModelOps model symbolSet typedSymbol =>
typedSymbol t -> t -> model -> model
insertValue TypedSymbol d
sym4 d
val4
        forall a b. (a -> b) -> a -> b
$ forall model symbolSet (typedSymbol :: * -> *).
ModelOps model symbolSet typedSymbol =>
model
emptyModel
  buildModel (ModelSymPair a, ModelSymPair b, ModelSymPair c, ModelSymPair d)
_ = 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
      ) =
      forall model symbolSet (typedSymbol :: * -> *) t.
ModelOps model symbolSet typedSymbol =>
typedSymbol t -> t -> model -> model
insertValue TypedSymbol a
sym1 a
val1
        forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall model symbolSet (typedSymbol :: * -> *) t.
ModelOps model symbolSet typedSymbol =>
typedSymbol t -> t -> model -> model
insertValue TypedSymbol b
sym2 b
val2
        forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall model symbolSet (typedSymbol :: * -> *) t.
ModelOps model symbolSet typedSymbol =>
typedSymbol t -> t -> model -> model
insertValue TypedSymbol c
sym3 c
val3
        forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall model symbolSet (typedSymbol :: * -> *) t.
ModelOps model symbolSet typedSymbol =>
typedSymbol t -> t -> model -> model
insertValue TypedSymbol d
sym4 d
val4
        forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall model symbolSet (typedSymbol :: * -> *) t.
ModelOps model symbolSet typedSymbol =>
typedSymbol t -> t -> model -> model
insertValue TypedSymbol e
sym5 e
val5
        forall a b. (a -> b) -> a -> b
$ forall model symbolSet (typedSymbol :: * -> *).
ModelOps model symbolSet typedSymbol =>
model
emptyModel
  buildModel (ModelSymPair a, ModelSymPair b, ModelSymPair c, ModelSymPair d,
 ModelSymPair e)
_ = 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
      ) =
      forall model symbolSet (typedSymbol :: * -> *) t.
ModelOps model symbolSet typedSymbol =>
typedSymbol t -> t -> model -> model
insertValue TypedSymbol a
sym1 a
val1
        forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall model symbolSet (typedSymbol :: * -> *) t.
ModelOps model symbolSet typedSymbol =>
typedSymbol t -> t -> model -> model
insertValue TypedSymbol b
sym2 b
val2
        forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall model symbolSet (typedSymbol :: * -> *) t.
ModelOps model symbolSet typedSymbol =>
typedSymbol t -> t -> model -> model
insertValue TypedSymbol c
sym3 c
val3
        forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall model symbolSet (typedSymbol :: * -> *) t.
ModelOps model symbolSet typedSymbol =>
typedSymbol t -> t -> model -> model
insertValue TypedSymbol d
sym4 d
val4
        forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall model symbolSet (typedSymbol :: * -> *) t.
ModelOps model symbolSet typedSymbol =>
typedSymbol t -> t -> model -> model
insertValue TypedSymbol e
sym5 e
val5
        forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall model symbolSet (typedSymbol :: * -> *) t.
ModelOps model symbolSet typedSymbol =>
typedSymbol t -> t -> model -> model
insertValue TypedSymbol f
sym6 f
val6
        forall a b. (a -> b) -> a -> b
$ forall model symbolSet (typedSymbol :: * -> *).
ModelOps model symbolSet typedSymbol =>
model
emptyModel
  buildModel (ModelSymPair a, ModelSymPair b, ModelSymPair c, ModelSymPair d,
 ModelSymPair e, ModelSymPair f)
_ = 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
      ) =
      forall model symbolSet (typedSymbol :: * -> *) t.
ModelOps model symbolSet typedSymbol =>
typedSymbol t -> t -> model -> model
insertValue TypedSymbol a
sym1 a
val1
        forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall model symbolSet (typedSymbol :: * -> *) t.
ModelOps model symbolSet typedSymbol =>
typedSymbol t -> t -> model -> model
insertValue TypedSymbol b
sym2 b
val2
        forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall model symbolSet (typedSymbol :: * -> *) t.
ModelOps model symbolSet typedSymbol =>
typedSymbol t -> t -> model -> model
insertValue TypedSymbol c
sym3 c
val3
        forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall model symbolSet (typedSymbol :: * -> *) t.
ModelOps model symbolSet typedSymbol =>
typedSymbol t -> t -> model -> model
insertValue TypedSymbol d
sym4 d
val4
        forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall model symbolSet (typedSymbol :: * -> *) t.
ModelOps model symbolSet typedSymbol =>
typedSymbol t -> t -> model -> model
insertValue TypedSymbol e
sym5 e
val5
        forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall model symbolSet (typedSymbol :: * -> *) t.
ModelOps model symbolSet typedSymbol =>
typedSymbol t -> t -> model -> model
insertValue TypedSymbol f
sym6 f
val6
        forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall model symbolSet (typedSymbol :: * -> *) t.
ModelOps model symbolSet typedSymbol =>
typedSymbol t -> t -> model -> model
insertValue TypedSymbol g
sym7 g
val7
        forall a b. (a -> b) -> a -> b
$ 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)
_ = 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
      ) =
      forall model symbolSet (typedSymbol :: * -> *) t.
ModelOps model symbolSet typedSymbol =>
typedSymbol t -> t -> model -> model
insertValue TypedSymbol a
sym1 a
val1
        forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall model symbolSet (typedSymbol :: * -> *) t.
ModelOps model symbolSet typedSymbol =>
typedSymbol t -> t -> model -> model
insertValue TypedSymbol b
sym2 b
val2
        forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall model symbolSet (typedSymbol :: * -> *) t.
ModelOps model symbolSet typedSymbol =>
typedSymbol t -> t -> model -> model
insertValue TypedSymbol c
sym3 c
val3
        forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall model symbolSet (typedSymbol :: * -> *) t.
ModelOps model symbolSet typedSymbol =>
typedSymbol t -> t -> model -> model
insertValue TypedSymbol d
sym4 d
val4
        forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall model symbolSet (typedSymbol :: * -> *) t.
ModelOps model symbolSet typedSymbol =>
typedSymbol t -> t -> model -> model
insertValue TypedSymbol e
sym5 e
val5
        forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall model symbolSet (typedSymbol :: * -> *) t.
ModelOps model symbolSet typedSymbol =>
typedSymbol t -> t -> model -> model
insertValue TypedSymbol f
sym6 f
val6
        forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall model symbolSet (typedSymbol :: * -> *) t.
ModelOps model symbolSet typedSymbol =>
typedSymbol t -> t -> model -> model
insertValue TypedSymbol g
sym7 g
val7
        forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall model symbolSet (typedSymbol :: * -> *) t.
ModelOps model symbolSet typedSymbol =>
typedSymbol t -> t -> model -> model
insertValue TypedSymbol h
sym8 h
val8
        forall a b. (a -> b) -> a -> b
$ 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)
_ = 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) = forall a. Term a -> Sym a
Sym forall a b. (a -> b) -> a -> 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) = forall a b.
(SupportedPrim a, SupportedPrim b) =>
TypedSymbol a -> Term b -> a --> b
GeneralFun TypedSymbol a
arg Term b
v