{-# LANGUAGE DataKinds #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE GADTs #-}
{-# HLINT ignore "Eta reduce" #-}
{-# LANGUAGE InstanceSigs #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE UndecidableInstances #-}
{-# OPTIONS_GHC -Wno-unrecognised-pragmas #-}
module Grisette.Internal.SymPrim.Prim.Internal.Instances.BVPEval () where
import Data.Maybe (isJust)
import Data.Proxy (Proxy (Proxy))
import qualified Data.SBV as SBV
import Data.Typeable (type (:~:) (Refl))
import GHC.TypeNats (KnownNat, natVal, sameNat, type (+), type (-), type (<=))
import Grisette.Internal.Core.Data.Class.BitVector
( SizedBV
( sizedBVConcat,
sizedBVFromIntegral,
sizedBVSelect,
sizedBVSext,
sizedBVZext
),
)
import Grisette.Internal.Core.Data.Class.SignConversion
( SignConversion (toSigned, toUnsigned),
)
import Grisette.Internal.SymPrim.BV (IntN, WordN)
import Grisette.Internal.SymPrim.Prim.Internal.Instances.SupportedPrim
( bvIsNonZeroFromGEq1,
)
import Grisette.Internal.SymPrim.Prim.Internal.Term
( PEvalBVSignConversionTerm
( pevalBVToSignedTerm,
pevalBVToUnsignedTerm,
sbvToSigned,
sbvToUnsigned,
withSbvSignConversionTermConstraint
),
PEvalBVTerm
( pevalBVConcatTerm,
pevalBVExtendTerm,
pevalBVSelectTerm,
sbvBVConcatTerm,
sbvBVExtendTerm,
sbvBVSelectTerm
),
SupportedPrim (withPrim),
Term
( BVConcatTerm,
BVExtendTerm,
BVSelectTerm,
ConTerm,
ToSignedTerm,
ToUnsignedTerm
),
bvconcatTerm,
bvextendTerm,
bvselectTerm,
conTerm,
toSignedTerm,
toUnsignedTerm,
)
import Grisette.Internal.SymPrim.Prim.Internal.Unfold
( binaryUnfoldOnce,
unaryUnfoldOnce,
)
import Grisette.Internal.SymPrim.Prim.TermUtils (castTerm)
import Grisette.Internal.Utils.Parameterized
( LeqProof (LeqProof),
NatRepr,
SomeNatRepr (SomeNatRepr),
SomePositiveNatRepr (SomePositiveNatRepr),
addNat,
mkNatRepr,
mkPositiveNatRepr,
natRepr,
unsafeAxiom,
unsafeKnownProof,
unsafeLeqProof,
withKnownNat,
withKnownProof,
)
instance PEvalBVSignConversionTerm WordN IntN where
pevalBVToSignedTerm :: forall (n :: Nat).
(KnownNat n, 1 <= n) =>
Term (WordN n) -> Term (IntN n)
pevalBVToSignedTerm = PartialRuleUnary (WordN n) (IntN n)
-> TotalRuleUnary (WordN n) (IntN n)
-> TotalRuleUnary (WordN n) (IntN n)
forall a b.
SupportedPrim b =>
PartialRuleUnary a b -> TotalRuleUnary a b -> TotalRuleUnary a b
unaryUnfoldOnce PartialRuleUnary (WordN n) (IntN n)
forall (n :: Nat).
(KnownNat n, 1 <= n) =>
Term (WordN n) -> Maybe (Term (IntN n))
doPevalToSignedTerm TotalRuleUnary (WordN n) (IntN n)
forall (u :: Nat -> *) (s :: Nat -> *) (n :: Nat).
(PEvalBVSignConversionTerm u s, KnownNat n, 1 <= n) =>
Term (u n) -> Term (s n)
toSignedTerm
where
doPevalToSignedTerm ::
forall n.
(KnownNat n, 1 <= n) =>
Term (WordN n) ->
Maybe (Term (IntN n))
doPevalToSignedTerm :: forall (n :: Nat).
(KnownNat n, 1 <= n) =>
Term (WordN n) -> Maybe (Term (IntN n))
doPevalToSignedTerm (ConTerm Id
_ WordN n
b) = Term (IntN n) -> Maybe (Term (IntN n))
forall a. a -> Maybe a
Just (Term (IntN n) -> Maybe (Term (IntN n)))
-> Term (IntN n) -> Maybe (Term (IntN n))
forall a b. (a -> b) -> a -> b
$ IntN n -> Term (IntN n)
forall t.
(SupportedPrim t, Typeable t, Hashable t, Eq t, Show t) =>
t -> Term t
conTerm (IntN n -> Term (IntN n)) -> IntN n -> Term (IntN n)
forall a b. (a -> b) -> a -> b
$ WordN n -> IntN n
forall ubv sbv. SignConversion ubv sbv => ubv -> sbv
toSigned WordN n
b
doPevalToSignedTerm (ToUnsignedTerm Id
_ Term (s n)
b) = Term (s n) -> Maybe (Term (s n))
forall a. a -> Maybe a
Just Term (s n)
b Maybe (Term (s n))
-> (Term (s n) -> Maybe (Term (IntN n))) -> Maybe (Term (IntN n))
forall a b. Maybe a -> (a -> Maybe b) -> Maybe b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= Term (s n) -> Maybe (Term (IntN n))
forall a b. Typeable b => Term a -> Maybe (Term b)
castTerm
doPevalToSignedTerm (BVConcatTerm Id
_ Term (bv l)
b1 Term (bv r)
b2) =
Term (IntN n) -> Maybe (Term (IntN n))
forall a. a -> Maybe a
Just (Term (IntN n) -> Maybe (Term (IntN n)))
-> Term (IntN n) -> Maybe (Term (IntN n))
forall a b. (a -> b) -> a -> b
$
Term (IntN l) -> Term (IntN r) -> Term (IntN (l + r))
forall (l :: Nat) (r :: Nat).
(KnownNat l, KnownNat r, 1 <= l, 1 <= r) =>
Term (IntN l) -> Term (IntN r) -> Term (IntN (l + r))
forall (bv :: Nat -> *) (l :: Nat) (r :: Nat).
(PEvalBVTerm bv, KnownNat l, KnownNat r, 1 <= l, 1 <= r) =>
Term (bv l) -> Term (bv r) -> Term (bv (l + r))
pevalBVConcatTerm (Term (bv l) -> Term (IntN l)
forall (n :: Nat).
(KnownNat n, 1 <= n) =>
Term (bv n) -> Term (IntN n)
forall (u :: Nat -> *) (s :: Nat -> *) (n :: Nat).
(PEvalBVSignConversionTerm u s, KnownNat n, 1 <= n) =>
Term (u n) -> Term (s n)
pevalBVToSignedTerm Term (bv l)
b1) (Term (bv r) -> Term (IntN r)
forall (n :: Nat).
(KnownNat n, 1 <= n) =>
Term (bv n) -> Term (IntN n)
forall (u :: Nat -> *) (s :: Nat -> *) (n :: Nat).
(PEvalBVSignConversionTerm u s, KnownNat n, 1 <= n) =>
Term (u n) -> Term (s n)
pevalBVToSignedTerm Term (bv r)
b2)
doPevalToSignedTerm (BVExtendTerm Id
_ Bool
signed TypeRep r
pr Term (bv l)
b) =
Term (IntN n) -> Maybe (Term (IntN n))
forall a. a -> Maybe a
Just (Term (IntN n) -> Maybe (Term (IntN n)))
-> Term (IntN n) -> Maybe (Term (IntN n))
forall a b. (a -> b) -> a -> b
$ Bool -> TypeRep n -> Term (IntN l) -> Term (IntN n)
forall (l :: Nat) (r :: Nat) (proxy :: Nat -> *).
(KnownNat l, KnownNat r, 1 <= l, 1 <= r, l <= r) =>
Bool -> proxy r -> Term (IntN l) -> Term (IntN r)
forall (bv :: Nat -> *) (l :: Nat) (r :: Nat) (proxy :: Nat -> *).
(PEvalBVTerm bv, KnownNat l, KnownNat r, 1 <= l, 1 <= r, l <= r) =>
Bool -> proxy r -> Term (bv l) -> Term (bv r)
pevalBVExtendTerm Bool
signed TypeRep n
TypeRep r
pr (Term (IntN l) -> Term (IntN n)) -> Term (IntN l) -> Term (IntN n)
forall a b. (a -> b) -> a -> b
$ Term (bv l) -> Term (IntN l)
forall (n :: Nat).
(KnownNat n, 1 <= n) =>
Term (bv n) -> Term (IntN n)
forall (u :: Nat -> *) (s :: Nat -> *) (n :: Nat).
(PEvalBVSignConversionTerm u s, KnownNat n, 1 <= n) =>
Term (u n) -> Term (s n)
pevalBVToSignedTerm Term (bv l)
b
doPevalToSignedTerm Term (WordN n)
_ = Maybe (Term (IntN n))
forall a. Maybe a
Nothing
pevalBVToUnsignedTerm :: forall (n :: Nat).
(KnownNat n, 1 <= n) =>
Term (IntN n) -> Term (WordN n)
pevalBVToUnsignedTerm = PartialRuleUnary (IntN n) (WordN n)
-> TotalRuleUnary (IntN n) (WordN n)
-> TotalRuleUnary (IntN n) (WordN n)
forall a b.
SupportedPrim b =>
PartialRuleUnary a b -> TotalRuleUnary a b -> TotalRuleUnary a b
unaryUnfoldOnce PartialRuleUnary (IntN n) (WordN n)
forall (n :: Nat).
(KnownNat n, 1 <= n) =>
Term (IntN n) -> Maybe (Term (WordN n))
doPevalToUnsignedTerm TotalRuleUnary (IntN n) (WordN n)
forall (u :: Nat -> *) (s :: Nat -> *) (n :: Nat).
(PEvalBVSignConversionTerm u s, KnownNat n, 1 <= n) =>
Term (s n) -> Term (u n)
toUnsignedTerm
where
doPevalToUnsignedTerm ::
forall n.
(KnownNat n, 1 <= n) =>
Term (IntN n) ->
Maybe (Term (WordN n))
doPevalToUnsignedTerm :: forall (n :: Nat).
(KnownNat n, 1 <= n) =>
Term (IntN n) -> Maybe (Term (WordN n))
doPevalToUnsignedTerm (ConTerm Id
_ IntN n
b) = Term (WordN n) -> Maybe (Term (WordN n))
forall a. a -> Maybe a
Just (Term (WordN n) -> Maybe (Term (WordN n)))
-> Term (WordN n) -> Maybe (Term (WordN n))
forall a b. (a -> b) -> a -> b
$ WordN n -> Term (WordN n)
forall t.
(SupportedPrim t, Typeable t, Hashable t, Eq t, Show t) =>
t -> Term t
conTerm (WordN n -> Term (WordN n)) -> WordN n -> Term (WordN n)
forall a b. (a -> b) -> a -> b
$ IntN n -> WordN n
forall ubv sbv. SignConversion ubv sbv => sbv -> ubv
toUnsigned IntN n
b
doPevalToUnsignedTerm (ToSignedTerm Id
_ Term (u n)
b) = Term (u n) -> Maybe (Term (u n))
forall a. a -> Maybe a
Just Term (u n)
b Maybe (Term (u n))
-> (Term (u n) -> Maybe (Term (WordN n))) -> Maybe (Term (WordN n))
forall a b. Maybe a -> (a -> Maybe b) -> Maybe b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= Term (u n) -> Maybe (Term (WordN n))
forall a b. Typeable b => Term a -> Maybe (Term b)
castTerm
doPevalToUnsignedTerm (BVConcatTerm Id
_ Term (bv l)
b1 Term (bv r)
b2) =
Term (WordN n) -> Maybe (Term (WordN n))
forall a. a -> Maybe a
Just (Term (WordN n) -> Maybe (Term (WordN n)))
-> Term (WordN n) -> Maybe (Term (WordN n))
forall a b. (a -> b) -> a -> b
$
Term (WordN l) -> Term (WordN r) -> Term (WordN (l + r))
forall (l :: Nat) (r :: Nat).
(KnownNat l, KnownNat r, 1 <= l, 1 <= r) =>
Term (WordN l) -> Term (WordN r) -> Term (WordN (l + r))
forall (bv :: Nat -> *) (l :: Nat) (r :: Nat).
(PEvalBVTerm bv, KnownNat l, KnownNat r, 1 <= l, 1 <= r) =>
Term (bv l) -> Term (bv r) -> Term (bv (l + r))
pevalBVConcatTerm
(Term (bv l) -> Term (WordN l)
forall (n :: Nat).
(KnownNat n, 1 <= n) =>
Term (bv n) -> Term (WordN n)
forall (u :: Nat -> *) (s :: Nat -> *) (n :: Nat).
(PEvalBVSignConversionTerm u s, KnownNat n, 1 <= n) =>
Term (s n) -> Term (u n)
pevalBVToUnsignedTerm Term (bv l)
b1)
(Term (bv r) -> Term (WordN r)
forall (n :: Nat).
(KnownNat n, 1 <= n) =>
Term (bv n) -> Term (WordN n)
forall (u :: Nat -> *) (s :: Nat -> *) (n :: Nat).
(PEvalBVSignConversionTerm u s, KnownNat n, 1 <= n) =>
Term (s n) -> Term (u n)
pevalBVToUnsignedTerm Term (bv r)
b2)
doPevalToUnsignedTerm (BVExtendTerm Id
_ Bool
signed TypeRep r
pr Term (bv l)
b) =
Term (WordN n) -> Maybe (Term (WordN n))
forall a. a -> Maybe a
Just (Term (WordN n) -> Maybe (Term (WordN n)))
-> Term (WordN n) -> Maybe (Term (WordN n))
forall a b. (a -> b) -> a -> b
$ Bool -> TypeRep n -> Term (WordN l) -> Term (WordN n)
forall (l :: Nat) (r :: Nat) (proxy :: Nat -> *).
(KnownNat l, KnownNat r, 1 <= l, 1 <= r, l <= r) =>
Bool -> proxy r -> Term (WordN l) -> Term (WordN r)
forall (bv :: Nat -> *) (l :: Nat) (r :: Nat) (proxy :: Nat -> *).
(PEvalBVTerm bv, KnownNat l, KnownNat r, 1 <= l, 1 <= r, l <= r) =>
Bool -> proxy r -> Term (bv l) -> Term (bv r)
pevalBVExtendTerm Bool
signed TypeRep n
TypeRep r
pr (Term (WordN l) -> Term (WordN n))
-> Term (WordN l) -> Term (WordN n)
forall a b. (a -> b) -> a -> b
$ Term (bv l) -> Term (WordN l)
forall (n :: Nat).
(KnownNat n, 1 <= n) =>
Term (bv n) -> Term (WordN n)
forall (u :: Nat -> *) (s :: Nat -> *) (n :: Nat).
(PEvalBVSignConversionTerm u s, KnownNat n, 1 <= n) =>
Term (s n) -> Term (u n)
pevalBVToUnsignedTerm Term (bv l)
b
doPevalToUnsignedTerm Term (IntN n)
_ = Maybe (Term (WordN n))
forall a. Maybe a
Nothing
withSbvSignConversionTermConstraint :: forall (n :: Nat) (integerBitwidth :: Nat) (p :: Nat -> *)
(q :: Nat -> *) r.
(KnownIsZero integerBitwidth, KnownNat n, 1 <= n) =>
p n
-> q integerBitwidth
-> ((Integral (NonFuncSBVBaseType integerBitwidth (WordN n)),
Integral (NonFuncSBVBaseType integerBitwidth (IntN n))) =>
r)
-> r
withSbvSignConversionTermConstraint (p n
_ :: p n) q integerBitwidth
qint (Integral (NonFuncSBVBaseType integerBitwidth (WordN n)),
Integral (NonFuncSBVBaseType integerBitwidth (IntN n))) =>
r
r =
forall t (n :: Nat) (p :: Nat -> *) a.
(SupportedPrim t, KnownIsZero n) =>
p n
-> ((PrimConstraint n t, SMTDefinable (SBVType n t),
Mergeable (SBVType n t), Typeable (SBVType n t)) =>
a)
-> a
withPrim @(WordN n) q integerBitwidth
qint r
(Integral (NonFuncSBVBaseType integerBitwidth (WordN n)),
Integral (NonFuncSBVBaseType integerBitwidth (IntN n))) =>
r
(PrimConstraint integerBitwidth (WordN n),
SMTDefinable (SBVType integerBitwidth (WordN n)),
Mergeable (SBVType integerBitwidth (WordN n)),
Typeable (SBVType integerBitwidth (WordN n))) =>
r
r
pevalDefaultBVSelectTerm ::
forall bv n ix w p q.
( KnownNat n,
KnownNat ix,
KnownNat w,
1 <= n,
1 <= w,
ix + w <= n,
PEvalBVTerm bv
) =>
p ix ->
q w ->
Term (bv n) ->
Term (bv w)
pevalDefaultBVSelectTerm :: forall (bv :: Nat -> *) (n :: Nat) (ix :: Nat) (w :: Nat)
(p :: Nat -> *) (q :: Nat -> *).
(KnownNat n, KnownNat ix, KnownNat w, 1 <= n, 1 <= w,
(ix + w) <= n, PEvalBVTerm bv) =>
p ix -> q w -> Term (bv n) -> Term (bv w)
pevalDefaultBVSelectTerm p ix
ix q w
w =
PartialRuleUnary (bv n) (bv w)
-> TotalRuleUnary (bv n) (bv w) -> TotalRuleUnary (bv n) (bv w)
forall a b.
SupportedPrim b =>
PartialRuleUnary a b -> TotalRuleUnary a b -> TotalRuleUnary a b
unaryUnfoldOnce (p ix -> q w -> PartialRuleUnary (bv n) (bv w)
forall (bv :: Nat -> *) (n :: Nat) (ix :: Nat) (w :: Nat)
(p :: Nat -> *) (q :: Nat -> *).
(KnownNat n, KnownNat ix, KnownNat w, 1 <= n, 1 <= w,
(ix + w) <= n, PEvalBVTerm bv) =>
p ix -> q w -> Term (bv n) -> Maybe (Term (bv w))
doPevalDefaultBVSelectTerm p ix
ix q w
w) (p ix -> q w -> TotalRuleUnary (bv n) (bv w)
forall (bv :: Nat -> *) (n :: Nat) (ix :: Nat) (w :: Nat)
(p :: Nat -> *) (q :: Nat -> *).
(PEvalBVTerm bv, KnownNat n, KnownNat ix, KnownNat w, 1 <= n,
1 <= w, (ix + w) <= n) =>
p ix -> q w -> Term (bv n) -> Term (bv w)
bvselectTerm p ix
ix q w
w)
unsafePevalBVSelectTerm ::
forall bv n ix w.
(PEvalBVTerm bv) =>
NatRepr n ->
NatRepr ix ->
NatRepr w ->
Term (bv n) ->
Term (bv w)
unsafePevalBVSelectTerm :: forall (bv :: Nat -> *) (n :: Nat) (ix :: Nat) (w :: Nat).
PEvalBVTerm bv =>
NatRepr n -> NatRepr ix -> NatRepr w -> Term (bv n) -> Term (bv w)
unsafePevalBVSelectTerm NatRepr n
n NatRepr ix
ix NatRepr w
w Term (bv n)
term =
NatRepr n -> (KnownNat n => Term (bv w)) -> Term (bv w)
forall (n :: Nat) r. NatRepr n -> (KnownNat n => r) -> r
withKnownNat NatRepr n
n ((KnownNat n => Term (bv w)) -> Term (bv w))
-> (KnownNat n => Term (bv w)) -> Term (bv w)
forall a b. (a -> b) -> a -> b
$
NatRepr ix -> (KnownNat ix => Term (bv w)) -> Term (bv w)
forall (n :: Nat) r. NatRepr n -> (KnownNat n => r) -> r
withKnownNat NatRepr ix
ix ((KnownNat ix => Term (bv w)) -> Term (bv w))
-> (KnownNat ix => Term (bv w)) -> Term (bv w)
forall a b. (a -> b) -> a -> b
$
NatRepr w -> (KnownNat w => Term (bv w)) -> Term (bv w)
forall (n :: Nat) r. NatRepr n -> (KnownNat n => r) -> r
withKnownNat NatRepr w
w ((KnownNat w => Term (bv w)) -> Term (bv w))
-> (KnownNat w => Term (bv w)) -> Term (bv w)
forall a b. (a -> b) -> a -> b
$
case ( forall (m :: Nat) (n :: Nat). LeqProof m n
unsafeLeqProof @1 @n,
forall (m :: Nat) (n :: Nat). LeqProof m n
unsafeLeqProof @1 @w,
forall (m :: Nat) (n :: Nat). LeqProof m n
unsafeLeqProof @(ix + w) @n
) of
(LeqProof 1 n
LeqProof, LeqProof 1 w
LeqProof, LeqProof (ix + w) n
LeqProof) -> NatRepr ix -> NatRepr w -> Term (bv n) -> Term (bv w)
forall (n :: Nat) (ix :: Nat) (w :: Nat) (p :: Nat -> *)
(q :: Nat -> *).
(KnownNat n, KnownNat ix, KnownNat w, 1 <= n, 1 <= w,
(ix + w) <= n) =>
p ix -> q w -> Term (bv n) -> Term (bv w)
forall (bv :: Nat -> *) (n :: Nat) (ix :: Nat) (w :: Nat)
(p :: Nat -> *) (q :: Nat -> *).
(PEvalBVTerm bv, KnownNat n, KnownNat ix, KnownNat w, 1 <= n,
1 <= w, (ix + w) <= n) =>
p ix -> q w -> Term (bv n) -> Term (bv w)
pevalBVSelectTerm NatRepr ix
ix NatRepr w
w Term (bv n)
term
doPevalDefaultBVSelectTerm ::
forall bv n ix w p q.
( KnownNat n,
KnownNat ix,
KnownNat w,
1 <= n,
1 <= w,
ix + w <= n,
PEvalBVTerm bv
) =>
p ix ->
q w ->
Term (bv n) ->
Maybe (Term (bv w))
doPevalDefaultBVSelectTerm :: forall (bv :: Nat -> *) (n :: Nat) (ix :: Nat) (w :: Nat)
(p :: Nat -> *) (q :: Nat -> *).
(KnownNat n, KnownNat ix, KnownNat w, 1 <= n, 1 <= w,
(ix + w) <= n, PEvalBVTerm bv) =>
p ix -> q w -> Term (bv n) -> Maybe (Term (bv w))
doPevalDefaultBVSelectTerm p ix
_ q w
_ Term (bv n)
rhs
| Maybe (ix :~: 0) -> Bool
forall a. Maybe a -> Bool
isJust (Proxy ix -> Proxy 0 -> Maybe (ix :~: 0)
forall (a :: Nat) (b :: Nat) (proxy1 :: Nat -> *)
(proxy2 :: Nat -> *).
(KnownNat a, KnownNat b) =>
proxy1 a -> proxy2 b -> Maybe (a :~: b)
sameNat (forall (t :: Nat). Proxy t
forall {k} (t :: k). Proxy t
Proxy @ix) (forall (t :: Nat). Proxy t
forall {k} (t :: k). Proxy t
Proxy @0))
Bool -> Bool -> Bool
&& Maybe (w :~: n) -> Bool
forall a. Maybe a -> Bool
isJust (Proxy w -> Proxy n -> Maybe (w :~: n)
forall (a :: Nat) (b :: Nat) (proxy1 :: Nat -> *)
(proxy2 :: Nat -> *).
(KnownNat a, KnownNat b) =>
proxy1 a -> proxy2 b -> Maybe (a :~: b)
sameNat (forall (t :: Nat). Proxy t
forall {k} (t :: k). Proxy t
Proxy @w) (forall (t :: Nat). Proxy t
forall {k} (t :: k). Proxy t
Proxy @n)) =
Term (bv n) -> Maybe (Term (bv n))
forall a. a -> Maybe a
Just Term (bv n)
rhs Maybe (Term (bv n))
-> (Term (bv n) -> Maybe (Term (bv w))) -> Maybe (Term (bv w))
forall a b. Maybe a -> (a -> Maybe b) -> Maybe b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= Term (bv n) -> Maybe (Term (bv w))
forall a b. Typeable b => Term a -> Maybe (Term b)
castTerm
doPevalDefaultBVSelectTerm p ix
ix q w
w (ConTerm Id
_ bv n
b) =
Term (bv w) -> Maybe (Term (bv w))
forall a. a -> Maybe a
Just (Term (bv w) -> Maybe (Term (bv w)))
-> Term (bv w) -> Maybe (Term (bv w))
forall a b. (a -> b) -> a -> b
$ bv w -> Term (bv w)
forall t.
(SupportedPrim t, Typeable t, Hashable t, Eq t, Show t) =>
t -> Term t
conTerm (bv w -> Term (bv w)) -> bv w -> Term (bv w)
forall a b. (a -> b) -> a -> b
$ p ix -> q w -> bv n -> bv w
forall (n :: Nat) (ix :: Nat) (w :: Nat) (p :: Nat -> *)
(q :: Nat -> *).
(KnownNat n, KnownNat ix, KnownNat w, 1 <= n, 1 <= w,
(ix + w) <= n) =>
p ix -> q w -> bv n -> bv w
forall (bv :: Nat -> *) (n :: Nat) (ix :: Nat) (w :: Nat)
(p :: Nat -> *) (q :: Nat -> *).
(SizedBV bv, KnownNat n, KnownNat ix, KnownNat w, 1 <= n, 1 <= w,
(ix + w) <= n) =>
p ix -> q w -> bv n -> bv w
sizedBVSelect p ix
ix q w
w bv n
b
doPevalDefaultBVSelectTerm p ix
ix q w
w (ToSignedTerm Id
_ Term (u n)
b) =
Term (bv w) -> Maybe (Term (bv w))
forall a. a -> Maybe a
Just (Term (bv w) -> Maybe (Term (bv w)))
-> Term (bv w) -> Maybe (Term (bv w))
forall a b. (a -> b) -> a -> b
$ Term (u w) -> Term (bv w)
forall (n :: Nat).
(KnownNat n, 1 <= n) =>
Term (u n) -> Term (bv n)
forall (u :: Nat -> *) (s :: Nat -> *) (n :: Nat).
(PEvalBVSignConversionTerm u s, KnownNat n, 1 <= n) =>
Term (u n) -> Term (s n)
pevalBVToSignedTerm (Term (u w) -> Term (bv w)) -> Term (u w) -> Term (bv w)
forall a b. (a -> b) -> a -> b
$ p ix -> q w -> Term (u n) -> Term (u w)
forall (n :: Nat) (ix :: Nat) (w :: Nat) (p :: Nat -> *)
(q :: Nat -> *).
(KnownNat n, KnownNat ix, KnownNat w, 1 <= n, 1 <= w,
(ix + w) <= n) =>
p ix -> q w -> Term (u n) -> Term (u w)
forall (bv :: Nat -> *) (n :: Nat) (ix :: Nat) (w :: Nat)
(p :: Nat -> *) (q :: Nat -> *).
(PEvalBVTerm bv, KnownNat n, KnownNat ix, KnownNat w, 1 <= n,
1 <= w, (ix + w) <= n) =>
p ix -> q w -> Term (bv n) -> Term (bv w)
pevalBVSelectTerm p ix
ix q w
w Term (u n)
b
doPevalDefaultBVSelectTerm p ix
ix q w
w (ToUnsignedTerm Id
_ Term (s n)
b) =
Term (bv w) -> Maybe (Term (bv w))
forall a. a -> Maybe a
Just (Term (bv w) -> Maybe (Term (bv w)))
-> Term (bv w) -> Maybe (Term (bv w))
forall a b. (a -> b) -> a -> b
$ Term (s w) -> Term (bv w)
forall (n :: Nat).
(KnownNat n, 1 <= n) =>
Term (s n) -> Term (bv n)
forall (u :: Nat -> *) (s :: Nat -> *) (n :: Nat).
(PEvalBVSignConversionTerm u s, KnownNat n, 1 <= n) =>
Term (s n) -> Term (u n)
pevalBVToUnsignedTerm (Term (s w) -> Term (bv w)) -> Term (s w) -> Term (bv w)
forall a b. (a -> b) -> a -> b
$ p ix -> q w -> Term (s n) -> Term (s w)
forall (n :: Nat) (ix :: Nat) (w :: Nat) (p :: Nat -> *)
(q :: Nat -> *).
(KnownNat n, KnownNat ix, KnownNat w, 1 <= n, 1 <= w,
(ix + w) <= n) =>
p ix -> q w -> Term (s n) -> Term (s w)
forall (bv :: Nat -> *) (n :: Nat) (ix :: Nat) (w :: Nat)
(p :: Nat -> *) (q :: Nat -> *).
(PEvalBVTerm bv, KnownNat n, KnownNat ix, KnownNat w, 1 <= n,
1 <= w, (ix + w) <= n) =>
p ix -> q w -> Term (bv n) -> Term (bv w)
pevalBVSelectTerm p ix
ix q w
w Term (s n)
b
doPevalDefaultBVSelectTerm
p ix
pix
q w
pw
(BVConcatTerm Id
_ (Term (bv l)
b1 :: Term (bv n1)) (Term (bv r)
b2 :: Term (bv n2)))
| Nat
ix Nat -> Nat -> Nat
forall a. Num a => a -> a -> a
+ Nat
w Nat -> Nat -> Bool
forall a. Ord a => a -> a -> Bool
<= Nat
n2 = Term (bv w) -> Maybe (Term (bv w))
forall a. a -> Maybe a
Just (Term (bv w) -> Maybe (Term (bv w)))
-> Term (bv w) -> Maybe (Term (bv w))
forall a b. (a -> b) -> a -> b
$ NatRepr r -> NatRepr ix -> NatRepr w -> Term (bv r) -> Term (bv w)
forall (bv :: Nat -> *) (n :: Nat) (ix :: Nat) (w :: Nat).
PEvalBVTerm bv =>
NatRepr n -> NatRepr ix -> NatRepr w -> Term (bv n) -> Term (bv w)
unsafePevalBVSelectTerm NatRepr r
n2Repr NatRepr ix
ixRepr NatRepr w
wRepr Term (bv r)
b2
| Nat
ix Nat -> Nat -> Bool
forall a. Ord a => a -> a -> Bool
>= Nat
n2 =
case Nat -> SomeNatRepr
mkNatRepr (Nat
ix Nat -> Nat -> Nat
forall a. Num a => a -> a -> a
- Nat
n2) of
SomeNatRepr NatRepr n
ixpn2Repr ->
Term (bv w) -> Maybe (Term (bv w))
forall a. a -> Maybe a
Just (Term (bv w) -> Maybe (Term (bv w)))
-> Term (bv w) -> Maybe (Term (bv w))
forall a b. (a -> b) -> a -> b
$ NatRepr l -> NatRepr n -> NatRepr w -> Term (bv l) -> Term (bv w)
forall (bv :: Nat -> *) (n :: Nat) (ix :: Nat) (w :: Nat).
PEvalBVTerm bv =>
NatRepr n -> NatRepr ix -> NatRepr w -> Term (bv n) -> Term (bv w)
unsafePevalBVSelectTerm NatRepr l
n1Repr NatRepr n
ixpn2Repr NatRepr w
wRepr Term (bv l)
b1
| Bool
otherwise =
case (Nat -> SomeNatRepr
mkNatRepr (Nat
w Nat -> Nat -> Nat
forall a. Num a => a -> a -> a
+ Nat
ix Nat -> Nat -> Nat
forall a. Num a => a -> a -> a
- Nat
n2), Nat -> SomeNatRepr
mkNatRepr (Nat
n2 Nat -> Nat -> Nat
forall a. Num a => a -> a -> a
- Nat
ix)) of
(SomeNatRepr NatRepr n
wixpn2Repr, SomeNatRepr NatRepr n
n2pixRepr) ->
let b1Part :: Term (bv n)
b1Part =
NatRepr l -> NatRepr 0 -> NatRepr n -> Term (bv l) -> Term (bv n)
forall (bv :: Nat -> *) (n :: Nat) (ix :: Nat) (w :: Nat).
PEvalBVTerm bv =>
NatRepr n -> NatRepr ix -> NatRepr w -> Term (bv n) -> Term (bv w)
unsafePevalBVSelectTerm NatRepr l
n1Repr (forall (n :: Nat). KnownNat n => NatRepr n
natRepr @0) NatRepr n
wixpn2Repr Term (bv l)
b1
b2Part :: Term (bv n)
b2Part = NatRepr r -> NatRepr ix -> NatRepr n -> Term (bv r) -> Term (bv n)
forall (bv :: Nat -> *) (n :: Nat) (ix :: Nat) (w :: Nat).
PEvalBVTerm bv =>
NatRepr n -> NatRepr ix -> NatRepr w -> Term (bv n) -> Term (bv w)
unsafePevalBVSelectTerm NatRepr r
n2Repr NatRepr ix
ixRepr NatRepr n
n2pixRepr Term (bv r)
b2
in Term (bv w) -> Maybe (Term (bv w))
forall a. a -> Maybe a
Just (Term (bv w) -> Maybe (Term (bv w)))
-> Term (bv w) -> Maybe (Term (bv w))
forall a b. (a -> b) -> a -> b
$
NatRepr n
-> NatRepr n
-> NatRepr w
-> Term (bv n)
-> Term (bv n)
-> Term (bv w)
forall (bv :: Nat -> *) (n1 :: Nat) (n2 :: Nat) (r :: Nat).
PEvalBVTerm bv =>
NatRepr n1
-> NatRepr n2
-> NatRepr r
-> Term (bv n1)
-> Term (bv n2)
-> Term (bv r)
unsafePevalBVConcatTerm
NatRepr n
wixpn2Repr
NatRepr n
n2pixRepr
NatRepr w
wRepr
Term (bv n)
b1Part
Term (bv n)
b2Part
where
ixRepr :: NatRepr ix
ixRepr = forall (n :: Nat). KnownNat n => NatRepr n
natRepr @ix
wRepr :: NatRepr w
wRepr = forall (n :: Nat). KnownNat n => NatRepr n
natRepr @w
n1Repr :: NatRepr l
n1Repr = forall (n :: Nat). KnownNat n => NatRepr n
natRepr @n1
n2Repr :: NatRepr r
n2Repr = forall (n :: Nat). KnownNat n => NatRepr n
natRepr @n2
ix :: Nat
ix = forall (n :: Nat) (proxy :: Nat -> *). KnownNat n => proxy n -> Nat
natVal @ix p ix
pix
w :: Nat
w = forall (n :: Nat) (proxy :: Nat -> *). KnownNat n => proxy n -> Nat
natVal @w q w
pw
n2 :: Nat
n2 = forall (n :: Nat) (proxy :: Nat -> *). KnownNat n => proxy n -> Nat
natVal @n2 (forall (t :: Nat). Proxy t
forall {k} (t :: k). Proxy t
Proxy @n2)
doPevalDefaultBVSelectTerm
p ix
_
q w
_
(BVSelectTerm Id
_ (TypeRep ix
_ :: proxy ix1) TypeRep w
_ (Term (bv n)
b :: Term (bv n1))) =
Term (bv w) -> Maybe (Term (bv w))
forall a. a -> Maybe a
Just (Term (bv w) -> Maybe (Term (bv w)))
-> Term (bv w) -> Maybe (Term (bv w))
forall a b. (a -> b) -> a -> b
$
NatRepr n
-> NatRepr (ix + ix) -> NatRepr w -> Term (bv n) -> Term (bv w)
forall (bv :: Nat -> *) (n :: Nat) (ix :: Nat) (w :: Nat).
PEvalBVTerm bv =>
NatRepr n -> NatRepr ix -> NatRepr w -> Term (bv n) -> Term (bv w)
unsafePevalBVSelectTerm
(forall (n :: Nat). KnownNat n => NatRepr n
natRepr @n1)
(NatRepr ix -> NatRepr ix -> NatRepr (ix + ix)
forall (m :: Nat) (n :: Nat).
NatRepr m -> NatRepr n -> NatRepr (m + n)
addNat (forall (n :: Nat). KnownNat n => NatRepr n
natRepr @ix) (forall (n :: Nat). KnownNat n => NatRepr n
natRepr @ix1))
(forall (n :: Nat). KnownNat n => NatRepr n
natRepr @w)
Term (bv n)
b
doPevalDefaultBVSelectTerm
p ix
pix
q w
pw
(BVExtendTerm Id
_ Bool
signed TypeRep r
_ (Term (bv l)
b :: Term (bv n1)))
| Nat
ix Nat -> Nat -> Nat
forall a. Num a => a -> a -> a
+ Nat
w Nat -> Nat -> Bool
forall a. Ord a => a -> a -> Bool
<= Nat
n1 = Term (bv w) -> Maybe (Term (bv w))
forall a. a -> Maybe a
Just (Term (bv w) -> Maybe (Term (bv w)))
-> Term (bv w) -> Maybe (Term (bv w))
forall a b. (a -> b) -> a -> b
$ NatRepr l -> NatRepr ix -> NatRepr w -> Term (bv l) -> Term (bv w)
forall (bv :: Nat -> *) (n :: Nat) (ix :: Nat) (w :: Nat).
PEvalBVTerm bv =>
NatRepr n -> NatRepr ix -> NatRepr w -> Term (bv n) -> Term (bv w)
unsafePevalBVSelectTerm NatRepr l
n1Repr NatRepr ix
ixRepr NatRepr w
wRepr Term (bv l)
b
| Nat
ix Nat -> Nat -> Bool
forall a. Ord a => a -> a -> Bool
< Nat
n1 =
case Nat -> SomeNatRepr
mkNatRepr (Nat
n1 Nat -> Nat -> Nat
forall a. Num a => a -> a -> a
- Nat
ix) of
SomeNatRepr NatRepr n
n1pixRepr ->
let bPart :: Term (bv n)
bPart = NatRepr l -> NatRepr ix -> NatRepr n -> Term (bv l) -> Term (bv n)
forall (bv :: Nat -> *) (n :: Nat) (ix :: Nat) (w :: Nat).
PEvalBVTerm bv =>
NatRepr n -> NatRepr ix -> NatRepr w -> Term (bv n) -> Term (bv w)
unsafePevalBVSelectTerm NatRepr l
n1Repr NatRepr ix
ixRepr NatRepr n
n1pixRepr Term (bv l)
b
in Term (bv w) -> Maybe (Term (bv w))
forall a. a -> Maybe a
Just (Term (bv w) -> Maybe (Term (bv w)))
-> Term (bv w) -> Maybe (Term (bv w))
forall a b. (a -> b) -> a -> b
$ NatRepr n -> NatRepr w -> Bool -> Term (bv n) -> Term (bv w)
forall (bv :: Nat -> *) (l :: Nat) (r :: Nat).
PEvalBVTerm bv =>
NatRepr l -> NatRepr r -> Bool -> Term (bv l) -> Term (bv r)
unsafePevalBVExtendTerm NatRepr n
n1pixRepr NatRepr w
wRepr Bool
signed Term (bv n)
bPart
| Bool
otherwise = Maybe (Term (bv w))
forall a. Maybe a
Nothing
where
ixRepr :: NatRepr ix
ixRepr = forall (n :: Nat). KnownNat n => NatRepr n
natRepr @ix
wRepr :: NatRepr w
wRepr = forall (n :: Nat). KnownNat n => NatRepr n
natRepr @w
n1Repr :: NatRepr l
n1Repr = forall (n :: Nat). KnownNat n => NatRepr n
natRepr @n1
ix :: Nat
ix = forall (n :: Nat) (proxy :: Nat -> *). KnownNat n => proxy n -> Nat
natVal @ix p ix
pix
w :: Nat
w = forall (n :: Nat) (proxy :: Nat -> *). KnownNat n => proxy n -> Nat
natVal @w q w
pw
n1 :: Nat
n1 = forall (n :: Nat) (proxy :: Nat -> *). KnownNat n => proxy n -> Nat
natVal @n1 (forall (t :: Nat). Proxy t
forall {k} (t :: k). Proxy t
Proxy @n1)
doPevalDefaultBVSelectTerm p ix
_ q w
_ Term (bv n)
_ = Maybe (Term (bv w))
forall a. Maybe a
Nothing
pevalDefaultBVExtendTerm ::
forall proxy l r bv.
( PEvalBVTerm bv,
KnownNat l,
KnownNat r,
1 <= l,
1 <= r,
l <= r
) =>
Bool ->
proxy r ->
Term (bv l) ->
Term (bv r)
pevalDefaultBVExtendTerm :: forall (proxy :: Nat -> *) (l :: Nat) (r :: Nat) (bv :: Nat -> *).
(PEvalBVTerm bv, KnownNat l, KnownNat r, 1 <= l, 1 <= r, l <= r) =>
Bool -> proxy r -> Term (bv l) -> Term (bv r)
pevalDefaultBVExtendTerm Bool
signed proxy r
p =
PartialRuleUnary (bv l) (bv r)
-> TotalRuleUnary (bv l) (bv r) -> TotalRuleUnary (bv l) (bv r)
forall a b.
SupportedPrim b =>
PartialRuleUnary a b -> TotalRuleUnary a b -> TotalRuleUnary a b
unaryUnfoldOnce (Bool -> proxy r -> PartialRuleUnary (bv l) (bv r)
forall (proxy :: Nat -> *) (l :: Nat) (r :: Nat) (bv :: Nat -> *).
(PEvalBVTerm bv, KnownNat l, KnownNat r, 1 <= l, 1 <= r, l <= r) =>
Bool -> proxy r -> Term (bv l) -> Maybe (Term (bv r))
doPevalDefaultBVExtendTerm Bool
signed proxy r
p) (Bool -> proxy r -> TotalRuleUnary (bv l) (bv r)
forall (bv :: Nat -> *) (l :: Nat) (r :: Nat) (proxy :: Nat -> *).
(PEvalBVTerm bv, KnownNat l, KnownNat r, 1 <= l, 1 <= r, l <= r) =>
Bool -> proxy r -> Term (bv l) -> Term (bv r)
bvextendTerm Bool
signed proxy r
p)
unsafePevalBVExtendTerm ::
forall bv l r.
(PEvalBVTerm bv) =>
NatRepr l ->
NatRepr r ->
Bool ->
Term (bv l) ->
Term (bv r)
unsafePevalBVExtendTerm :: forall (bv :: Nat -> *) (l :: Nat) (r :: Nat).
PEvalBVTerm bv =>
NatRepr l -> NatRepr r -> Bool -> Term (bv l) -> Term (bv r)
unsafePevalBVExtendTerm NatRepr l
lRepr NatRepr r
rRepr Bool
signed Term (bv l)
v =
case (forall (m :: Nat) (n :: Nat). LeqProof m n
unsafeLeqProof @1 @l, forall (m :: Nat) (n :: Nat). LeqProof m n
unsafeLeqProof @1 @r, forall (m :: Nat) (n :: Nat). LeqProof m n
unsafeLeqProof @l @r) of
(LeqProof 1 l
LeqProof, LeqProof 1 r
LeqProof, LeqProof l r
LeqProof) ->
NatRepr l -> (KnownNat l => Term (bv r)) -> Term (bv r)
forall (n :: Nat) r. NatRepr n -> (KnownNat n => r) -> r
withKnownNat NatRepr l
lRepr ((KnownNat l => Term (bv r)) -> Term (bv r))
-> (KnownNat l => Term (bv r)) -> Term (bv r)
forall a b. (a -> b) -> a -> b
$
NatRepr r -> (KnownNat r => Term (bv r)) -> Term (bv r)
forall (n :: Nat) r. NatRepr n -> (KnownNat n => r) -> r
withKnownNat NatRepr r
rRepr ((KnownNat r => Term (bv r)) -> Term (bv r))
-> (KnownNat r => Term (bv r)) -> Term (bv r)
forall a b. (a -> b) -> a -> b
$
Bool -> Proxy r -> Term (bv l) -> Term (bv r)
forall (l :: Nat) (r :: Nat) (proxy :: Nat -> *).
(KnownNat l, KnownNat r, 1 <= l, 1 <= r, l <= r) =>
Bool -> proxy r -> Term (bv l) -> Term (bv r)
forall (bv :: Nat -> *) (l :: Nat) (r :: Nat) (proxy :: Nat -> *).
(PEvalBVTerm bv, KnownNat l, KnownNat r, 1 <= l, 1 <= r, l <= r) =>
Bool -> proxy r -> Term (bv l) -> Term (bv r)
pevalBVExtendTerm Bool
signed (forall (t :: Nat). Proxy t
forall {k} (t :: k). Proxy t
Proxy @r) Term (bv l)
v
doPevalDefaultBVExtendTerm ::
forall proxy l r bv.
( PEvalBVTerm bv,
KnownNat l,
KnownNat r,
1 <= l,
1 <= r,
l <= r
) =>
Bool ->
proxy r ->
Term (bv l) ->
Maybe (Term (bv r))
doPevalDefaultBVExtendTerm :: forall (proxy :: Nat -> *) (l :: Nat) (r :: Nat) (bv :: Nat -> *).
(PEvalBVTerm bv, KnownNat l, KnownNat r, 1 <= l, 1 <= r, l <= r) =>
Bool -> proxy r -> Term (bv l) -> Maybe (Term (bv r))
doPevalDefaultBVExtendTerm Bool
signed proxy r
p (ConTerm Id
_ bv l
b) =
Term (bv r) -> Maybe (Term (bv r))
forall a. a -> Maybe a
Just (Term (bv r) -> Maybe (Term (bv r)))
-> Term (bv r) -> Maybe (Term (bv r))
forall a b. (a -> b) -> a -> b
$ bv r -> Term (bv r)
forall t.
(SupportedPrim t, Typeable t, Hashable t, Eq t, Show t) =>
t -> Term t
conTerm (bv r -> Term (bv r)) -> bv r -> Term (bv r)
forall a b. (a -> b) -> a -> b
$ if Bool
signed then proxy r -> bv l -> bv r
forall (l :: Nat) (r :: Nat) (proxy :: Nat -> *).
(KnownNat l, KnownNat r, 1 <= l, KnownNat r, l <= r) =>
proxy r -> bv l -> bv r
forall (bv :: Nat -> *) (l :: Nat) (r :: Nat) (proxy :: Nat -> *).
(SizedBV bv, KnownNat l, KnownNat r, 1 <= l, KnownNat r, l <= r) =>
proxy r -> bv l -> bv r
sizedBVSext proxy r
p bv l
b else proxy r -> bv l -> bv r
forall (l :: Nat) (r :: Nat) (proxy :: Nat -> *).
(KnownNat l, KnownNat r, 1 <= l, KnownNat r, l <= r) =>
proxy r -> bv l -> bv r
forall (bv :: Nat -> *) (l :: Nat) (r :: Nat) (proxy :: Nat -> *).
(SizedBV bv, KnownNat l, KnownNat r, 1 <= l, KnownNat r, l <= r) =>
proxy r -> bv l -> bv r
sizedBVZext proxy r
p bv l
b
doPevalDefaultBVExtendTerm Bool
_ proxy r
_ Term (bv l)
b
| Maybe (l :~: r) -> Bool
forall a. Maybe a -> Bool
isJust (Maybe (l :~: r) -> Bool) -> Maybe (l :~: r) -> Bool
forall a b. (a -> b) -> a -> b
$ Proxy l -> Proxy r -> Maybe (l :~: r)
forall (a :: Nat) (b :: Nat) (proxy1 :: Nat -> *)
(proxy2 :: Nat -> *).
(KnownNat a, KnownNat b) =>
proxy1 a -> proxy2 b -> Maybe (a :~: b)
sameNat (forall (t :: Nat). Proxy t
forall {k} (t :: k). Proxy t
Proxy @l) (forall (t :: Nat). Proxy t
forall {k} (t :: k). Proxy t
Proxy @r) =
Term (bv l) -> Maybe (Term (bv l))
forall a. a -> Maybe a
Just Term (bv l)
b Maybe (Term (bv l))
-> (Term (bv l) -> Maybe (Term (bv r))) -> Maybe (Term (bv r))
forall a b. Maybe a -> (a -> Maybe b) -> Maybe b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= Term (bv l) -> Maybe (Term (bv r))
forall a b. Typeable b => Term a -> Maybe (Term b)
castTerm
doPevalDefaultBVExtendTerm Bool
False proxy r
pr Term (bv l)
b =
case (Nat -> SomePositiveNatRepr
mkPositiveNatRepr (Nat -> SomePositiveNatRepr) -> Nat -> SomePositiveNatRepr
forall a b. (a -> b) -> a -> b
$ Nat
r Nat -> Nat -> Nat
forall a. Num a => a -> a -> a
- Nat
l) of
SomePositiveNatRepr (NatRepr n
rplRepr :: NatRepr lpr) ->
Term (bv r) -> Maybe (Term (bv r))
forall a. a -> Maybe a
Just (Term (bv r) -> Maybe (Term (bv r)))
-> Term (bv r) -> Maybe (Term (bv r))
forall a b. (a -> b) -> a -> b
$
NatRepr n
-> NatRepr l
-> NatRepr r
-> Term (bv n)
-> Term (bv l)
-> Term (bv r)
forall (bv :: Nat -> *) (n1 :: Nat) (n2 :: Nat) (r :: Nat).
PEvalBVTerm bv =>
NatRepr n1
-> NatRepr n2
-> NatRepr r
-> Term (bv n1)
-> Term (bv n2)
-> Term (bv r)
unsafePevalBVConcatTerm
NatRepr n
rplRepr
NatRepr l
lRepr
NatRepr r
rRepr
(bv n -> Term (bv n)
forall t.
(SupportedPrim t, Typeable t, Hashable t, Eq t, Show t) =>
t -> Term t
conTerm (bv n -> Term (bv n)) -> bv n -> Term (bv n)
forall a b. (a -> b) -> a -> b
$ Integer -> bv n
forall a (n :: Nat). (Integral a, KnownNat n, 1 <= n) => a -> bv n
forall (bv :: Nat -> *) a (n :: Nat).
(SizedBV bv, Integral a, KnownNat n, 1 <= n) =>
a -> bv n
sizedBVFromIntegral Integer
0)
Term (bv l)
b
where
lRepr :: NatRepr l
lRepr = forall (n :: Nat). KnownNat n => NatRepr n
natRepr @l
rRepr :: NatRepr r
rRepr = forall (n :: Nat). KnownNat n => NatRepr n
natRepr @r
l :: Nat
l = forall (n :: Nat) (proxy :: Nat -> *). KnownNat n => proxy n -> Nat
natVal @l (forall (t :: Nat). Proxy t
forall {k} (t :: k). Proxy t
Proxy @l)
r :: Nat
r = forall (n :: Nat) (proxy :: Nat -> *). KnownNat n => proxy n -> Nat
natVal @r proxy r
pr
doPevalDefaultBVExtendTerm Bool
True proxy r
p (BVExtendTerm Id
_ Bool
True TypeRep r
_ (Term (bv l)
b :: Term (bv l1))) =
case forall (m :: Nat) (n :: Nat). LeqProof m n
unsafeLeqProof @l1 @r of
LeqProof l r
LeqProof -> Term (bv r) -> Maybe (Term (bv r))
forall a. a -> Maybe a
Just (Term (bv r) -> Maybe (Term (bv r)))
-> Term (bv r) -> Maybe (Term (bv r))
forall a b. (a -> b) -> a -> b
$ Bool -> proxy r -> Term (bv l) -> Term (bv r)
forall (l :: Nat) (r :: Nat) (proxy :: Nat -> *).
(KnownNat l, KnownNat r, 1 <= l, 1 <= r, l <= r) =>
Bool -> proxy r -> Term (bv l) -> Term (bv r)
forall (bv :: Nat -> *) (l :: Nat) (r :: Nat) (proxy :: Nat -> *).
(PEvalBVTerm bv, KnownNat l, KnownNat r, 1 <= l, 1 <= r, l <= r) =>
Bool -> proxy r -> Term (bv l) -> Term (bv r)
pevalBVExtendTerm Bool
True proxy r
p Term (bv l)
b
doPevalDefaultBVExtendTerm Bool
_ proxy r
_ Term (bv l)
_ = Maybe (Term (bv r))
forall a. Maybe a
Nothing
pevalDefaultBVConcatTerm ::
forall bv a b.
( KnownNat a,
KnownNat b,
1 <= a,
1 <= b,
PEvalBVTerm bv
) =>
Term (bv a) ->
Term (bv b) ->
Term (bv (a + b))
pevalDefaultBVConcatTerm :: forall (bv :: Nat -> *) (a :: Nat) (b :: Nat).
(KnownNat a, KnownNat b, 1 <= a, 1 <= b, PEvalBVTerm bv) =>
Term (bv a) -> Term (bv b) -> Term (bv (a + b))
pevalDefaultBVConcatTerm =
NatRepr (a + b)
-> (KnownNat (a + b) =>
Term (bv a) -> Term (bv b) -> Term (bv (a + b)))
-> Term (bv a)
-> Term (bv b)
-> Term (bv (a + b))
forall (n :: Nat) r. NatRepr n -> (KnownNat n => r) -> r
withKnownNat (NatRepr a -> NatRepr b -> NatRepr (a + b)
forall (m :: Nat) (n :: Nat).
NatRepr m -> NatRepr n -> NatRepr (m + n)
addNat (forall (n :: Nat). KnownNat n => NatRepr n
natRepr @a) (forall (n :: Nat). KnownNat n => NatRepr n
natRepr @b)) ((KnownNat (a + b) =>
Term (bv a) -> Term (bv b) -> Term (bv (a + b)))
-> Term (bv a) -> Term (bv b) -> Term (bv (a + b)))
-> (KnownNat (a + b) =>
Term (bv a) -> Term (bv b) -> Term (bv (a + b)))
-> Term (bv a)
-> Term (bv b)
-> Term (bv (a + b))
forall a b. (a -> b) -> a -> b
$
case (forall (m :: Nat) (n :: Nat). LeqProof m n
unsafeLeqProof @1 @(a + b)) of
LeqProof 1 (a + b)
LeqProof ->
PartialRuleBinary (bv a) (bv b) (bv (a + b))
-> (Term (bv a) -> Term (bv b) -> Term (bv (a + b)))
-> Term (bv a)
-> Term (bv b)
-> Term (bv (a + b))
forall a b c.
(Typeable a, Typeable b, SupportedPrim c) =>
PartialRuleBinary a b c
-> TotalRuleBinary a b c -> TotalRuleBinary a b c
binaryUnfoldOnce PartialRuleBinary (bv a) (bv b) (bv (a + b))
forall (bv :: Nat -> *) (l :: Nat) (r :: Nat).
(KnownNat l, KnownNat r, 1 <= l, 1 <= r, 1 <= (l + r),
PEvalBVTerm bv) =>
Term (bv l) -> Term (bv r) -> Maybe (Term (bv (l + r)))
doPevalDefaultBVConcatTerm Term (bv a) -> Term (bv b) -> Term (bv (a + b))
forall (bv :: Nat -> *) (l :: Nat) (r :: Nat).
(PEvalBVTerm bv, KnownNat l, KnownNat r, KnownNat (l + r), 1 <= l,
1 <= r, 1 <= (l + r)) =>
Term (bv l) -> Term (bv r) -> Term (bv (l + r))
bvconcatTerm
unsafeBVConcatTerm ::
forall bv n1 n2 r.
(PEvalBVTerm bv) =>
NatRepr n1 ->
NatRepr n2 ->
NatRepr r ->
Term (bv n1) ->
Term (bv n2) ->
Term (bv r)
unsafeBVConcatTerm :: forall (bv :: Nat -> *) (n1 :: Nat) (n2 :: Nat) (r :: Nat).
PEvalBVTerm bv =>
NatRepr n1
-> NatRepr n2
-> NatRepr r
-> Term (bv n1)
-> Term (bv n2)
-> Term (bv r)
unsafeBVConcatTerm NatRepr n1
n1Repr NatRepr n2
n2Repr NatRepr r
rRepr Term (bv n1)
lhs Term (bv n2)
rhs =
case ( (n1 + n2) :~: r
forall {k} (a :: k) (b :: k). a :~: b
unsafeAxiom :: (n1 + n2) :~: r,
forall (m :: Nat) (n :: Nat). LeqProof m n
unsafeLeqProof @1 @r,
forall (m :: Nat) (n :: Nat). LeqProof m n
unsafeLeqProof @1 @n1,
forall (m :: Nat) (n :: Nat). LeqProof m n
unsafeLeqProof @1 @n2
) of
((n1 + n2) :~: r
Refl, LeqProof 1 r
LeqProof, LeqProof 1 n1
LeqProof, LeqProof 1 n2
LeqProof) ->
NatRepr n1 -> (KnownNat n1 => Term (bv r)) -> Term (bv r)
forall (n :: Nat) r. NatRepr n -> (KnownNat n => r) -> r
withKnownNat NatRepr n1
n1Repr ((KnownNat n1 => Term (bv r)) -> Term (bv r))
-> (KnownNat n1 => Term (bv r)) -> Term (bv r)
forall a b. (a -> b) -> a -> b
$
NatRepr n2 -> (KnownNat n2 => Term (bv r)) -> Term (bv r)
forall (n :: Nat) r. NatRepr n -> (KnownNat n => r) -> r
withKnownNat NatRepr n2
n2Repr ((KnownNat n2 => Term (bv r)) -> Term (bv r))
-> (KnownNat n2 => Term (bv r)) -> Term (bv r)
forall a b. (a -> b) -> a -> b
$
NatRepr r -> (KnownNat r => Term (bv r)) -> Term (bv r)
forall (n :: Nat) r. NatRepr n -> (KnownNat n => r) -> r
withKnownNat NatRepr r
rRepr ((KnownNat r => Term (bv r)) -> Term (bv r))
-> (KnownNat r => Term (bv r)) -> Term (bv r)
forall a b. (a -> b) -> a -> b
$
Term (bv n1) -> Term (bv n2) -> Term (bv (n1 + n2))
forall (bv :: Nat -> *) (l :: Nat) (r :: Nat).
(PEvalBVTerm bv, KnownNat l, KnownNat r, KnownNat (l + r), 1 <= l,
1 <= r, 1 <= (l + r)) =>
Term (bv l) -> Term (bv r) -> Term (bv (l + r))
bvconcatTerm Term (bv n1)
lhs Term (bv n2)
rhs
unsafePevalBVConcatTerm ::
forall bv n1 n2 r.
(PEvalBVTerm bv) =>
NatRepr n1 ->
NatRepr n2 ->
NatRepr r ->
Term (bv n1) ->
Term (bv n2) ->
Term (bv r)
unsafePevalBVConcatTerm :: forall (bv :: Nat -> *) (n1 :: Nat) (n2 :: Nat) (r :: Nat).
PEvalBVTerm bv =>
NatRepr n1
-> NatRepr n2
-> NatRepr r
-> Term (bv n1)
-> Term (bv n2)
-> Term (bv r)
unsafePevalBVConcatTerm NatRepr n1
n1Repr NatRepr n2
n2Repr NatRepr r
rRepr Term (bv n1)
lhs Term (bv n2)
rhs =
case ( (n1 + n2) :~: r
forall {k} (a :: k) (b :: k). a :~: b
unsafeAxiom :: (n1 + n2) :~: r,
forall (m :: Nat) (n :: Nat). LeqProof m n
unsafeLeqProof @1 @r,
forall (m :: Nat) (n :: Nat). LeqProof m n
unsafeLeqProof @1 @n1,
forall (m :: Nat) (n :: Nat). LeqProof m n
unsafeLeqProof @1 @n2
) of
((n1 + n2) :~: r
Refl, LeqProof 1 r
LeqProof, LeqProof 1 n1
LeqProof, LeqProof 1 n2
LeqProof) ->
NatRepr n1 -> (KnownNat n1 => Term (bv r)) -> Term (bv r)
forall (n :: Nat) r. NatRepr n -> (KnownNat n => r) -> r
withKnownNat NatRepr n1
n1Repr ((KnownNat n1 => Term (bv r)) -> Term (bv r))
-> (KnownNat n1 => Term (bv r)) -> Term (bv r)
forall a b. (a -> b) -> a -> b
$
NatRepr n2 -> (KnownNat n2 => Term (bv r)) -> Term (bv r)
forall (n :: Nat) r. NatRepr n -> (KnownNat n => r) -> r
withKnownNat NatRepr n2
n2Repr ((KnownNat n2 => Term (bv r)) -> Term (bv r))
-> (KnownNat n2 => Term (bv r)) -> Term (bv r)
forall a b. (a -> b) -> a -> b
$
NatRepr r -> (KnownNat r => Term (bv r)) -> Term (bv r)
forall (n :: Nat) r. NatRepr n -> (KnownNat n => r) -> r
withKnownNat NatRepr r
rRepr ((KnownNat r => Term (bv r)) -> Term (bv r))
-> (KnownNat r => Term (bv r)) -> Term (bv r)
forall a b. (a -> b) -> a -> b
$
Term (bv n1) -> Term (bv n2) -> Term (bv (n1 + n2))
forall (l :: Nat) (r :: Nat).
(KnownNat l, KnownNat r, 1 <= l, 1 <= r) =>
Term (bv l) -> Term (bv r) -> Term (bv (l + r))
forall (bv :: Nat -> *) (l :: Nat) (r :: Nat).
(PEvalBVTerm bv, KnownNat l, KnownNat r, 1 <= l, 1 <= r) =>
Term (bv l) -> Term (bv r) -> Term (bv (l + r))
pevalBVConcatTerm Term (bv n1)
lhs Term (bv n2)
rhs
doPevalDefaultBVConcatTerm ::
forall bv l r.
( KnownNat l,
KnownNat r,
1 <= l,
1 <= r,
1 <= (l + r),
PEvalBVTerm bv
) =>
Term (bv l) ->
Term (bv r) ->
Maybe (Term (bv (l + r)))
doPevalDefaultBVConcatTerm :: forall (bv :: Nat -> *) (l :: Nat) (r :: Nat).
(KnownNat l, KnownNat r, 1 <= l, 1 <= r, 1 <= (l + r),
PEvalBVTerm bv) =>
Term (bv l) -> Term (bv r) -> Maybe (Term (bv (l + r)))
doPevalDefaultBVConcatTerm (ConTerm Id
_ bv l
v) (ConTerm Id
_ bv r
v') =
NatRepr (l + r)
-> (KnownNat (l + r) => Maybe (Term (bv (l + r))))
-> Maybe (Term (bv (l + r)))
forall (n :: Nat) r. NatRepr n -> (KnownNat n => r) -> r
withKnownNat (NatRepr l -> NatRepr r -> NatRepr (l + r)
forall (m :: Nat) (n :: Nat).
NatRepr m -> NatRepr n -> NatRepr (m + n)
addNat (forall (n :: Nat). KnownNat n => NatRepr n
natRepr @l) (forall (n :: Nat). KnownNat n => NatRepr n
natRepr @r)) ((KnownNat (l + r) => Maybe (Term (bv (l + r))))
-> Maybe (Term (bv (l + r))))
-> (KnownNat (l + r) => Maybe (Term (bv (l + r))))
-> Maybe (Term (bv (l + r)))
forall a b. (a -> b) -> a -> b
$
Term (bv (l + r)) -> Maybe (Term (bv (l + r)))
forall a. a -> Maybe a
Just (Term (bv (l + r)) -> Maybe (Term (bv (l + r))))
-> Term (bv (l + r)) -> Maybe (Term (bv (l + r)))
forall a b. (a -> b) -> a -> b
$
bv (l + r) -> Term (bv (l + r))
forall t.
(SupportedPrim t, Typeable t, Hashable t, Eq t, Show t) =>
t -> Term t
conTerm (bv (l + r) -> Term (bv (l + r)))
-> bv (l + r) -> Term (bv (l + r))
forall a b. (a -> b) -> a -> b
$
bv l -> bv r -> bv (l + r)
forall (l :: Nat) (r :: Nat).
(KnownNat l, KnownNat r, 1 <= l, 1 <= r) =>
bv l -> bv r -> bv (l + r)
forall (bv :: Nat -> *) (l :: Nat) (r :: Nat).
(SizedBV bv, KnownNat l, KnownNat r, 1 <= l, 1 <= r) =>
bv l -> bv r -> bv (l + r)
sizedBVConcat bv l
v bv r
v'
doPevalDefaultBVConcatTerm
(ConTerm Id
_ bv l
vl)
(BVConcatTerm Id
_ (ConTerm Id
_ (bv l
vrl :: bv rl)) (Term (bv r)
rr :: Term (bv rr))) =
case forall (m :: Nat) (n :: Nat). LeqProof m n
unsafeLeqProof @1 @(l + rl) of
LeqProof 1 (l + l)
LeqProof ->
Term (bv (l + r)) -> Maybe (Term (bv (l + r)))
forall a. a -> Maybe a
Just (Term (bv (l + r)) -> Maybe (Term (bv (l + r))))
-> Term (bv (l + r)) -> Maybe (Term (bv (l + r)))
forall a b. (a -> b) -> a -> b
$
NatRepr (l + l)
-> (KnownNat (l + l) => Term (bv (l + r))) -> Term (bv (l + r))
forall (n :: Nat) r. NatRepr n -> (KnownNat n => r) -> r
withKnownNat NatRepr (l + l)
lRlRepr ((KnownNat (l + l) => Term (bv (l + r))) -> Term (bv (l + r)))
-> (KnownNat (l + l) => Term (bv (l + r))) -> Term (bv (l + r))
forall a b. (a -> b) -> a -> b
$
NatRepr (l + l)
-> NatRepr r
-> NatRepr (l + r)
-> Term (bv (l + l))
-> Term (bv r)
-> Term (bv (l + r))
forall (bv :: Nat -> *) (n1 :: Nat) (n2 :: Nat) (r :: Nat).
PEvalBVTerm bv =>
NatRepr n1
-> NatRepr n2
-> NatRepr r
-> Term (bv n1)
-> Term (bv n2)
-> Term (bv r)
unsafeBVConcatTerm
NatRepr (l + l)
lRlRepr
(forall (n :: Nat). KnownNat n => NatRepr n
natRepr @rr)
(NatRepr l -> NatRepr r -> NatRepr (l + r)
forall (m :: Nat) (n :: Nat).
NatRepr m -> NatRepr n -> NatRepr (m + n)
addNat (forall (n :: Nat). KnownNat n => NatRepr n
natRepr @l) (forall (n :: Nat). KnownNat n => NatRepr n
natRepr @r))
(bv (l + l) -> Term (bv (l + l))
forall t.
(SupportedPrim t, Typeable t, Hashable t, Eq t, Show t) =>
t -> Term t
conTerm (bv (l + l) -> Term (bv (l + l)))
-> bv (l + l) -> Term (bv (l + l))
forall a b. (a -> b) -> a -> b
$ bv l -> bv l -> bv (l + l)
forall (l :: Nat) (r :: Nat).
(KnownNat l, KnownNat r, 1 <= l, 1 <= r) =>
bv l -> bv r -> bv (l + r)
forall (bv :: Nat -> *) (l :: Nat) (r :: Nat).
(SizedBV bv, KnownNat l, KnownNat r, 1 <= l, 1 <= r) =>
bv l -> bv r -> bv (l + r)
sizedBVConcat bv l
vl bv l
vrl)
Term (bv r)
rr
where
lRlRepr :: NatRepr (l + l)
lRlRepr = NatRepr l -> NatRepr l -> NatRepr (l + l)
forall (m :: Nat) (n :: Nat).
NatRepr m -> NatRepr n -> NatRepr (m + n)
addNat (forall (n :: Nat). KnownNat n => NatRepr n
natRepr @l) (forall (n :: Nat). KnownNat n => NatRepr n
natRepr @rl)
doPevalDefaultBVConcatTerm (ConTerm {}) (BVConcatTerm Id
_ Term (bv l)
_ ConTerm {}) = Maybe (Term (bv (l + r)))
forall a. Maybe a
Nothing
doPevalDefaultBVConcatTerm
(BVConcatTerm Id
_ (ll :: Term (bv l)
ll@ConTerm {} :: Term (bv ll)) (Term (bv r)
lr :: Term (bv lr)))
Term (bv r)
r =
Term (bv (l + r)) -> Maybe (Term (bv (l + r)))
forall a. a -> Maybe a
Just (Term (bv (l + r)) -> Maybe (Term (bv (l + r))))
-> Term (bv (l + r)) -> Maybe (Term (bv (l + r)))
forall a b. (a -> b) -> a -> b
$ NatRepr l
-> NatRepr (r + r)
-> NatRepr (l + r)
-> Term (bv l)
-> Term (bv (r + r))
-> Term (bv (l + r))
forall (bv :: Nat -> *) (n1 :: Nat) (n2 :: Nat) (r :: Nat).
PEvalBVTerm bv =>
NatRepr n1
-> NatRepr n2
-> NatRepr r
-> Term (bv n1)
-> Term (bv n2)
-> Term (bv r)
unsafeBVConcatTerm NatRepr l
llRepr NatRepr (r + r)
lrRRepr NatRepr (l + r)
lRRepr Term (bv l)
ll Term (bv (r + r))
rhs
where
llRepr :: NatRepr l
llRepr = forall (n :: Nat). KnownNat n => NatRepr n
natRepr @ll
lrRepr :: NatRepr r
lrRepr = forall (n :: Nat). KnownNat n => NatRepr n
natRepr @lr
lRepr :: NatRepr l
lRepr = forall (n :: Nat). KnownNat n => NatRepr n
natRepr @l
rRepr :: NatRepr r
rRepr = forall (n :: Nat). KnownNat n => NatRepr n
natRepr @r
lrRRepr :: NatRepr (r + r)
lrRRepr = NatRepr r -> NatRepr r -> NatRepr (r + r)
forall (m :: Nat) (n :: Nat).
NatRepr m -> NatRepr n -> NatRepr (m + n)
addNat NatRepr r
lrRepr NatRepr r
rRepr
lRRepr :: NatRepr (l + r)
lRRepr = NatRepr l -> NatRepr r -> NatRepr (l + r)
forall (m :: Nat) (n :: Nat).
NatRepr m -> NatRepr n -> NatRepr (m + n)
addNat NatRepr l
lRepr NatRepr r
rRepr
rhs :: Term (bv (lr + r))
rhs :: Term (bv (r + r))
rhs = NatRepr r
-> NatRepr r
-> NatRepr (r + r)
-> Term (bv r)
-> Term (bv r)
-> Term (bv (r + r))
forall (bv :: Nat -> *) (n1 :: Nat) (n2 :: Nat) (r :: Nat).
PEvalBVTerm bv =>
NatRepr n1
-> NatRepr n2
-> NatRepr r
-> Term (bv n1)
-> Term (bv n2)
-> Term (bv r)
unsafePevalBVConcatTerm NatRepr r
lrRepr NatRepr r
rRepr NatRepr (r + r)
lrRRepr Term (bv r)
lr Term (bv r)
r
doPevalDefaultBVConcatTerm
Term (bv l)
l
( BVConcatTerm
Id
_
(rl :: Term (bv l)
rl@ConTerm {} :: Term (bv rl))
(BVConcatTerm Id
_ (Term (bv l)
rrl :: Term (bv rrl)) (rrr :: Term (bv r)
rrr@ConTerm {} :: Term (bv rrr)))
) =
Term (bv (l + r)) -> Maybe (Term (bv (l + r)))
forall a. a -> Maybe a
Just (Term (bv (l + r)) -> Maybe (Term (bv (l + r))))
-> Term (bv (l + r)) -> Maybe (Term (bv (l + r)))
forall a b. (a -> b) -> a -> b
$ NatRepr ((l + l) + l)
-> NatRepr r
-> NatRepr (l + r)
-> Term (bv ((l + l) + l))
-> Term (bv r)
-> Term (bv (l + r))
forall (bv :: Nat -> *) (n1 :: Nat) (n2 :: Nat) (r :: Nat).
PEvalBVTerm bv =>
NatRepr n1
-> NatRepr n2
-> NatRepr r
-> Term (bv n1)
-> Term (bv n2)
-> Term (bv r)
unsafeBVConcatTerm NatRepr ((l + l) + l)
lRlRrlRepr NatRepr r
rrrRepr NatRepr (l + r)
lRRepr Term (bv ((l + l) + l))
lRlRrl Term (bv r)
rrr
where
lRepr :: NatRepr l
lRepr = forall (n :: Nat). KnownNat n => NatRepr n
natRepr @l
rlRepr :: NatRepr l
rlRepr = forall (n :: Nat). KnownNat n => NatRepr n
natRepr @rl
rrlRepr :: NatRepr l
rrlRepr = forall (n :: Nat). KnownNat n => NatRepr n
natRepr @rrl
rrrRepr :: NatRepr r
rrrRepr = forall (n :: Nat). KnownNat n => NatRepr n
natRepr @rrr
lRlRepr :: NatRepr (l + l)
lRlRepr = NatRepr l -> NatRepr l -> NatRepr (l + l)
forall (m :: Nat) (n :: Nat).
NatRepr m -> NatRepr n -> NatRepr (m + n)
addNat NatRepr l
lRepr NatRepr l
rlRepr
rRepr :: NatRepr r
rRepr = forall (n :: Nat). KnownNat n => NatRepr n
natRepr @r
lRRepr :: NatRepr (l + r)
lRRepr = NatRepr l -> NatRepr r -> NatRepr (l + r)
forall (m :: Nat) (n :: Nat).
NatRepr m -> NatRepr n -> NatRepr (m + n)
addNat NatRepr l
lRepr NatRepr r
rRepr
lRl :: Term (bv (l + l))
lRl = NatRepr l
-> NatRepr l
-> NatRepr (l + l)
-> Term (bv l)
-> Term (bv l)
-> Term (bv (l + l))
forall (bv :: Nat -> *) (n1 :: Nat) (n2 :: Nat) (r :: Nat).
PEvalBVTerm bv =>
NatRepr n1
-> NatRepr n2
-> NatRepr r
-> Term (bv n1)
-> Term (bv n2)
-> Term (bv r)
unsafePevalBVConcatTerm NatRepr l
lRepr NatRepr l
rlRepr NatRepr (l + l)
lRlRepr Term (bv l)
l Term (bv l)
rl
lRlRrlRepr :: NatRepr ((l + l) + l)
lRlRrlRepr = NatRepr (l + l) -> NatRepr l -> NatRepr ((l + l) + l)
forall (m :: Nat) (n :: Nat).
NatRepr m -> NatRepr n -> NatRepr (m + n)
addNat NatRepr (l + l)
lRlRepr NatRepr l
rrlRepr
lRlRrl :: Term (bv ((l + l) + l))
lRlRrl = NatRepr (l + l)
-> NatRepr l
-> NatRepr ((l + l) + l)
-> Term (bv (l + l))
-> Term (bv l)
-> Term (bv ((l + l) + l))
forall (bv :: Nat -> *) (n1 :: Nat) (n2 :: Nat) (r :: Nat).
PEvalBVTerm bv =>
NatRepr n1
-> NatRepr n2
-> NatRepr r
-> Term (bv n1)
-> Term (bv n2)
-> Term (bv r)
unsafeBVConcatTerm NatRepr (l + l)
lRlRepr NatRepr l
rrlRepr NatRepr ((l + l) + l)
lRlRrlRepr Term (bv (l + l))
lRl Term (bv l)
rrl
doPevalDefaultBVConcatTerm
(BVConcatTerm Id
_ (Term (bv l)
ll :: Term (bv ll)) ((ConTerm Id
_ bv r
vlr) :: Term (bv lr)))
(ConTerm Id
_ bv r
vr) =
Term (bv (l + r)) -> Maybe (Term (bv (l + r)))
forall a. a -> Maybe a
Just (Term (bv (l + r)) -> Maybe (Term (bv (l + r))))
-> Term (bv (l + r)) -> Maybe (Term (bv (l + r)))
forall a b. (a -> b) -> a -> b
$ NatRepr l
-> NatRepr (r + r)
-> NatRepr (l + r)
-> Term (bv l)
-> Term (bv (r + r))
-> Term (bv (l + r))
forall (bv :: Nat -> *) (n1 :: Nat) (n2 :: Nat) (r :: Nat).
PEvalBVTerm bv =>
NatRepr n1
-> NatRepr n2
-> NatRepr r
-> Term (bv n1)
-> Term (bv n2)
-> Term (bv r)
unsafeBVConcatTerm NatRepr l
llRepr NatRepr (r + r)
lrRRepr NatRepr (l + r)
lRRepr Term (bv l)
ll Term (bv (r + r))
rhs
where
llRepr :: NatRepr l
llRepr = forall (n :: Nat). KnownNat n => NatRepr n
natRepr @ll
lrRepr :: NatRepr r
lrRepr = forall (n :: Nat). KnownNat n => NatRepr n
natRepr @lr
lRepr :: NatRepr l
lRepr = forall (n :: Nat). KnownNat n => NatRepr n
natRepr @l
rRepr :: NatRepr r
rRepr = forall (n :: Nat). KnownNat n => NatRepr n
natRepr @r
lrRRepr :: NatRepr (r + r)
lrRRepr = NatRepr r -> NatRepr r -> NatRepr (r + r)
forall (m :: Nat) (n :: Nat).
NatRepr m -> NatRepr n -> NatRepr (m + n)
addNat NatRepr r
lrRepr NatRepr r
rRepr
lRRepr :: NatRepr (l + r)
lRRepr = NatRepr l -> NatRepr r -> NatRepr (l + r)
forall (m :: Nat) (n :: Nat).
NatRepr m -> NatRepr n -> NatRepr (m + n)
addNat NatRepr l
lRepr NatRepr r
rRepr
rhs :: Term (bv (lr + r))
rhs :: Term (bv (r + r))
rhs = case forall (m :: Nat) (n :: Nat). LeqProof m n
unsafeLeqProof @1 @(lr + r) of
LeqProof 1 (r + r)
LeqProof ->
NatRepr (r + r)
-> (KnownNat (r + r) => Term (bv (r + r))) -> Term (bv (r + r))
forall (n :: Nat) r. NatRepr n -> (KnownNat n => r) -> r
withKnownNat NatRepr (r + r)
lrRRepr ((KnownNat (r + r) => Term (bv (r + r))) -> Term (bv (r + r)))
-> (KnownNat (r + r) => Term (bv (r + r))) -> Term (bv (r + r))
forall a b. (a -> b) -> a -> b
$ bv (r + r) -> Term (bv (r + r))
forall t.
(SupportedPrim t, Typeable t, Hashable t, Eq t, Show t) =>
t -> Term t
conTerm (bv (r + r) -> Term (bv (r + r)))
-> bv (r + r) -> Term (bv (r + r))
forall a b. (a -> b) -> a -> b
$ bv r -> bv r -> bv (r + r)
forall (l :: Nat) (r :: Nat).
(KnownNat l, KnownNat r, 1 <= l, 1 <= r) =>
bv l -> bv r -> bv (l + r)
forall (bv :: Nat -> *) (l :: Nat) (r :: Nat).
(SizedBV bv, KnownNat l, KnownNat r, 1 <= l, 1 <= r) =>
bv l -> bv r -> bv (l + r)
sizedBVConcat bv r
vlr bv r
vr
doPevalDefaultBVConcatTerm
(BVConcatTerm Id
_ (Term (bv l)
ll :: Term (bv ll)) ((ConTerm Id
_ bv r
vlr) :: Term (bv lr)))
(BVConcatTerm Id
_ ((ConTerm Id
_ bv l
vrl) :: Term (bv rl)) (Term (bv r)
rr :: Term (bv rr))) =
Term (bv (l + r)) -> Maybe (Term (bv (l + r)))
forall a. a -> Maybe a
Just (Term (bv (l + r)) -> Maybe (Term (bv (l + r))))
-> Term (bv (l + r)) -> Maybe (Term (bv (l + r)))
forall a b. (a -> b) -> a -> b
$ NatRepr l
-> NatRepr ((r + l) + r)
-> NatRepr (l + r)
-> Term (bv l)
-> Term (bv ((r + l) + r))
-> Term (bv (l + r))
forall (bv :: Nat -> *) (n1 :: Nat) (n2 :: Nat) (r :: Nat).
PEvalBVTerm bv =>
NatRepr n1
-> NatRepr n2
-> NatRepr r
-> Term (bv n1)
-> Term (bv n2)
-> Term (bv r)
unsafeBVConcatTerm NatRepr l
llRepr NatRepr ((r + l) + r)
lrRlRrRepr NatRepr (l + r)
lRRepr Term (bv l)
ll Term (bv ((r + l) + r))
lrRlRR
where
lRepr :: NatRepr l
lRepr = forall (n :: Nat). KnownNat n => NatRepr n
natRepr @l
rRepr :: NatRepr r
rRepr = forall (n :: Nat). KnownNat n => NatRepr n
natRepr @r
llRepr :: NatRepr l
llRepr = forall (n :: Nat). KnownNat n => NatRepr n
natRepr @ll
lrRepr :: NatRepr r
lrRepr = forall (n :: Nat). KnownNat n => NatRepr n
natRepr @lr
rlRepr :: NatRepr l
rlRepr = forall (n :: Nat). KnownNat n => NatRepr n
natRepr @rl
rrRepr :: NatRepr r
rrRepr = forall (n :: Nat). KnownNat n => NatRepr n
natRepr @rr
lRRepr :: NatRepr (l + r)
lRRepr = NatRepr l -> NatRepr r -> NatRepr (l + r)
forall (m :: Nat) (n :: Nat).
NatRepr m -> NatRepr n -> NatRepr (m + n)
addNat NatRepr l
lRepr NatRepr r
rRepr
lrRlRepr :: NatRepr (lr + rl)
lrRlRepr :: NatRepr (r + l)
lrRlRepr = NatRepr r -> NatRepr l -> NatRepr (r + l)
forall (m :: Nat) (n :: Nat).
NatRepr m -> NatRepr n -> NatRepr (m + n)
addNat NatRepr r
lrRepr NatRepr l
rlRepr
lrRlRrRepr :: NatRepr ((lr + rl) + rr)
lrRlRrRepr :: NatRepr ((r + l) + r)
lrRlRrRepr = NatRepr (r + l) -> NatRepr r -> NatRepr ((r + l) + r)
forall (m :: Nat) (n :: Nat).
NatRepr m -> NatRepr n -> NatRepr (m + n)
addNat NatRepr (r + l)
lrRlRepr NatRepr r
rrRepr
lrRl :: Term (bv (lr + rl))
lrRl :: Term (bv (r + l))
lrRl = case forall (m :: Nat) (n :: Nat). LeqProof m n
unsafeLeqProof @1 @(lr + rl) of
LeqProof 1 (r + l)
LeqProof -> NatRepr (r + l)
-> (KnownNat (r + l) => Term (bv (r + l))) -> Term (bv (r + l))
forall (n :: Nat) r. NatRepr n -> (KnownNat n => r) -> r
withKnownNat NatRepr (r + l)
lrRlRepr ((KnownNat (r + l) => Term (bv (r + l))) -> Term (bv (r + l)))
-> (KnownNat (r + l) => Term (bv (r + l))) -> Term (bv (r + l))
forall a b. (a -> b) -> a -> b
$ bv (r + l) -> Term (bv (r + l))
forall t.
(SupportedPrim t, Typeable t, Hashable t, Eq t, Show t) =>
t -> Term t
conTerm (bv (r + l) -> Term (bv (r + l)))
-> bv (r + l) -> Term (bv (r + l))
forall a b. (a -> b) -> a -> b
$ bv r -> bv l -> bv (r + l)
forall (l :: Nat) (r :: Nat).
(KnownNat l, KnownNat r, 1 <= l, 1 <= r) =>
bv l -> bv r -> bv (l + r)
forall (bv :: Nat -> *) (l :: Nat) (r :: Nat).
(SizedBV bv, KnownNat l, KnownNat r, 1 <= l, 1 <= r) =>
bv l -> bv r -> bv (l + r)
sizedBVConcat bv r
vlr bv l
vrl
lrRlRR :: Term (bv ((lr + rl) + rr))
lrRlRR :: Term (bv ((r + l) + r))
lrRlRR = NatRepr (r + l)
-> NatRepr r
-> NatRepr ((r + l) + r)
-> Term (bv (r + l))
-> Term (bv r)
-> Term (bv ((r + l) + r))
forall (bv :: Nat -> *) (n1 :: Nat) (n2 :: Nat) (r :: Nat).
PEvalBVTerm bv =>
NatRepr n1
-> NatRepr n2
-> NatRepr r
-> Term (bv n1)
-> Term (bv n2)
-> Term (bv r)
unsafeBVConcatTerm NatRepr (r + l)
lrRlRepr NatRepr r
rrRepr NatRepr ((r + l) + r)
lrRlRrRepr Term (bv (r + l))
lrRl Term (bv r)
rr
doPevalDefaultBVConcatTerm
Term (bv l)
l
(BVConcatTerm Id
_ (Term (bv l)
rl :: Term (bv rl)) (rr :: Term (bv r)
rr@ConTerm {} :: Term (bv rr))) =
Term (bv (l + r)) -> Maybe (Term (bv (l + r)))
forall a. a -> Maybe a
Just (Term (bv (l + r)) -> Maybe (Term (bv (l + r))))
-> Term (bv (l + r)) -> Maybe (Term (bv (l + r)))
forall a b. (a -> b) -> a -> b
$
NatRepr (l + l)
-> NatRepr r
-> NatRepr (l + r)
-> Term (bv (l + l))
-> Term (bv r)
-> Term (bv (l + r))
forall (bv :: Nat -> *) (n1 :: Nat) (n2 :: Nat) (r :: Nat).
PEvalBVTerm bv =>
NatRepr n1
-> NatRepr n2
-> NatRepr r
-> Term (bv n1)
-> Term (bv n2)
-> Term (bv r)
unsafeBVConcatTerm
NatRepr (l + l)
lRlRepr
(forall (n :: Nat). KnownNat n => NatRepr n
natRepr @rr)
(NatRepr l -> NatRepr r -> NatRepr (l + r)
forall (m :: Nat) (n :: Nat).
NatRepr m -> NatRepr n -> NatRepr (m + n)
addNat (forall (n :: Nat). KnownNat n => NatRepr n
natRepr @l) (forall (n :: Nat). KnownNat n => NatRepr n
natRepr @r))
Term (bv (l + l))
lhs
Term (bv r)
rr
where
lRepr :: NatRepr l
lRepr = forall (n :: Nat). KnownNat n => NatRepr n
natRepr @l
rlRepr :: NatRepr l
rlRepr = forall (n :: Nat). KnownNat n => NatRepr n
natRepr @rl
lRlRepr :: NatRepr (l + l)
lRlRepr = NatRepr l -> NatRepr l -> NatRepr (l + l)
forall (m :: Nat) (n :: Nat).
NatRepr m -> NatRepr n -> NatRepr (m + n)
addNat NatRepr l
lRepr NatRepr l
rlRepr
lhs :: Term (bv (l + rl))
lhs :: Term (bv (l + l))
lhs = NatRepr l
-> NatRepr l
-> NatRepr (l + l)
-> Term (bv l)
-> Term (bv l)
-> Term (bv (l + l))
forall (bv :: Nat -> *) (n1 :: Nat) (n2 :: Nat) (r :: Nat).
PEvalBVTerm bv =>
NatRepr n1
-> NatRepr n2
-> NatRepr r
-> Term (bv n1)
-> Term (bv n2)
-> Term (bv r)
unsafeBVConcatTerm NatRepr l
lRepr NatRepr l
rlRepr NatRepr (l + l)
lRlRepr Term (bv l)
l Term (bv l)
rl
doPevalDefaultBVConcatTerm Term (bv l)
_ Term (bv r)
_ = Maybe (Term (bv (l + r)))
forall a. Maybe a
Nothing
instance PEvalBVTerm WordN where
pevalBVSelectTerm :: forall (n :: Nat) (ix :: Nat) (w :: Nat) (p :: Nat -> *)
(q :: Nat -> *).
(KnownNat n, KnownNat ix, KnownNat w, 1 <= n, 1 <= w,
(ix + w) <= n) =>
p ix -> q w -> Term (WordN n) -> Term (WordN w)
pevalBVSelectTerm = p ix -> q w -> Term (WordN n) -> Term (WordN w)
forall (bv :: Nat -> *) (n :: Nat) (ix :: Nat) (w :: Nat)
(p :: Nat -> *) (q :: Nat -> *).
(KnownNat n, KnownNat ix, KnownNat w, 1 <= n, 1 <= w,
(ix + w) <= n, PEvalBVTerm bv) =>
p ix -> q w -> Term (bv n) -> Term (bv w)
pevalDefaultBVSelectTerm
pevalBVConcatTerm :: forall (l :: Nat) (r :: Nat).
(KnownNat l, KnownNat r, 1 <= l, 1 <= r) =>
Term (WordN l) -> Term (WordN r) -> Term (WordN (l + r))
pevalBVConcatTerm = Term (WordN l) -> Term (WordN r) -> Term (WordN (l + r))
forall (bv :: Nat -> *) (a :: Nat) (b :: Nat).
(KnownNat a, KnownNat b, 1 <= a, 1 <= b, PEvalBVTerm bv) =>
Term (bv a) -> Term (bv b) -> Term (bv (a + b))
pevalDefaultBVConcatTerm
pevalBVExtendTerm :: forall (l :: Nat) (r :: Nat) (proxy :: Nat -> *).
(KnownNat l, KnownNat r, 1 <= l, 1 <= r, l <= r) =>
Bool -> proxy r -> Term (WordN l) -> Term (WordN r)
pevalBVExtendTerm = Bool -> proxy r -> Term (WordN l) -> Term (WordN r)
forall (proxy :: Nat -> *) (l :: Nat) (r :: Nat) (bv :: Nat -> *).
(PEvalBVTerm bv, KnownNat l, KnownNat r, 1 <= l, 1 <= r, l <= r) =>
Bool -> proxy r -> Term (bv l) -> Term (bv r)
pevalDefaultBVExtendTerm
sbvBVConcatTerm :: forall (n :: Nat) (l :: Nat) (r :: Nat) (p0 :: Nat -> *)
(p1 :: Nat -> *) (p2 :: Nat -> *).
(KnownIsZero n, KnownNat l, KnownNat r, 1 <= l, 1 <= r) =>
p0 n
-> p1 l
-> p2 r
-> SBVType n (WordN l)
-> SBVType n (WordN r)
-> SBVType n (WordN (l + r))
sbvBVConcatTerm p0 n
_ p1 l
pl p2 r
pr SBVType n (WordN l)
l SBVType n (WordN r)
r =
p1 l
-> (BVIsNonZero l => SBVType n (WordN (l + r)))
-> SBVType n (WordN (l + r))
forall (w :: Nat) r (proxy :: Nat -> *).
(1 <= w) =>
proxy w -> (BVIsNonZero w => r) -> r
bvIsNonZeroFromGEq1 p1 l
pl ((BVIsNonZero l => SBVType n (WordN (l + r)))
-> SBVType n (WordN (l + r)))
-> (BVIsNonZero l => SBVType n (WordN (l + r)))
-> SBVType n (WordN (l + r))
forall a b. (a -> b) -> a -> b
$
p2 r
-> (BVIsNonZero r => SBVType n (WordN (l + r)))
-> SBVType n (WordN (l + r))
forall (w :: Nat) r (proxy :: Nat -> *).
(1 <= w) =>
proxy w -> (BVIsNonZero w => r) -> r
bvIsNonZeroFromGEq1 p2 r
pr ((BVIsNonZero r => SBVType n (WordN (l + r)))
-> SBVType n (WordN (l + r)))
-> (BVIsNonZero r => SBVType n (WordN (l + r)))
-> SBVType n (WordN (l + r))
forall a b. (a -> b) -> a -> b
$
SBV (WordN l)
SBVType n (WordN l)
l SBV (WordN l) -> SBV (WordN r) -> SBV (WordN (l + r))
forall (n :: Nat) (bv :: Nat -> *) (m :: Nat).
(KnownNat n, BVIsNonZero n, SymVal (bv n), KnownNat m,
BVIsNonZero m, SymVal (bv m)) =>
SBV (bv n) -> SBV (bv m) -> SBV (bv (n + m))
SBV.# SBV (WordN r)
SBVType n (WordN r)
r
sbvBVSelectTerm :: forall (int :: Nat) (ix :: Nat) (w :: Nat) (n :: Nat)
(p0 :: Nat -> *) (p1 :: Nat -> *) (p2 :: Nat -> *)
(p3 :: Nat -> *).
(KnownIsZero int, KnownNat ix, KnownNat w, KnownNat n, 1 <= n,
1 <= w, (ix + w) <= n) =>
p0 int
-> p1 ix
-> p2 w
-> p3 n
-> SBVType int (WordN n)
-> SBVType int (WordN w)
sbvBVSelectTerm p0 int
_ (p1 ix
pix :: p0 ix) (p2 w
pw :: p1 w) (p3 n
pn :: p2 n) SBVType int (WordN n)
bv =
Proxy n
-> (BVIsNonZero n => SBVType int (WordN w))
-> SBVType int (WordN w)
forall (w :: Nat) r (proxy :: Nat -> *).
(1 <= w) =>
proxy w -> (BVIsNonZero w => r) -> r
bvIsNonZeroFromGEq1 (forall (t :: Nat). Proxy t
forall {k} (t :: k). Proxy t
Proxy @n) ((BVIsNonZero n => SBVType int (WordN w)) -> SBVType int (WordN w))
-> (BVIsNonZero n => SBVType int (WordN w))
-> SBVType int (WordN w)
forall a b. (a -> b) -> a -> b
$
Proxy w
-> (BVIsNonZero w => SBVType int (WordN w))
-> SBVType int (WordN w)
forall (w :: Nat) r (proxy :: Nat -> *).
(1 <= w) =>
proxy w -> (BVIsNonZero w => r) -> r
bvIsNonZeroFromGEq1 (forall (t :: Nat). Proxy t
forall {k} (t :: k). Proxy t
Proxy @w) ((BVIsNonZero w => SBVType int (WordN w)) -> SBVType int (WordN w))
-> (BVIsNonZero w => SBVType int (WordN w))
-> SBVType int (WordN w)
forall a b. (a -> b) -> a -> b
$
p1 ix -> p2 w -> p3 n -> SBV (WordN n) -> SBV (WordN w)
forall (ix :: Nat) (w :: Nat) (n :: Nat) (bv :: Nat -> *)
(p1 :: Nat -> *) (p2 :: Nat -> *) (p3 :: Nat -> *).
(KnownNat ix, KnownNat w, KnownNat n, 1 <= n, 1 <= w,
(ix + w) <= n, SymVal (bv n)) =>
p1 ix -> p2 w -> p3 n -> SBV (bv n) -> SBV (bv w)
sbvDefaultBVSelectTerm p1 ix
pix p2 w
pw p3 n
pn SBV (WordN n)
SBVType int (WordN n)
bv
sbvBVExtendTerm :: forall (n :: Nat) (l :: Nat) (r :: Nat) (p0 :: Nat -> *)
(p1 :: Nat -> *) (p2 :: Nat -> *).
(KnownIsZero n, KnownNat l, KnownNat r, 1 <= l, 1 <= r, l <= r) =>
p0 n
-> p1 l
-> p2 r
-> Bool
-> SBVType n (WordN l)
-> SBVType n (WordN r)
sbvBVExtendTerm p0 n
_ (p1 l
_ :: p0 l) (p2 r
_ :: p1 r) Bool
signed SBVType n (WordN l)
bv =
KnownProof (r - l)
-> (KnownNat (r - l) => SBVType n (WordN r)) -> SBVType n (WordN r)
forall (n :: Nat) r. KnownProof n -> (KnownNat n => r) -> r
withKnownProof
(forall (n :: Nat). Nat -> KnownProof n
unsafeKnownProof @(r - l) (Proxy r -> Nat
forall (n :: Nat) (proxy :: Nat -> *). KnownNat n => proxy n -> Nat
natVal (forall (t :: Nat). Proxy t
forall {k} (t :: k). Proxy t
Proxy @r) Nat -> Nat -> Nat
forall a. Num a => a -> a -> a
- Proxy l -> Nat
forall (n :: Nat) (proxy :: Nat -> *). KnownNat n => proxy n -> Nat
natVal (forall (t :: Nat). Proxy t
forall {k} (t :: k). Proxy t
Proxy @l)))
((KnownNat (r - l) => SBVType n (WordN r)) -> SBVType n (WordN r))
-> (KnownNat (r - l) => SBVType n (WordN r)) -> SBVType n (WordN r)
forall a b. (a -> b) -> a -> b
$ case (forall (m :: Nat) (n :: Nat). LeqProof m n
unsafeLeqProof @(l + 1) @r, forall (m :: Nat) (n :: Nat). LeqProof m n
unsafeLeqProof @1 @(r - l)) of
(LeqProof (l + 1) r
LeqProof, LeqProof 1 (r - l)
LeqProof) ->
Proxy r
-> (BVIsNonZero r => SBVType n (WordN r)) -> SBVType n (WordN r)
forall (w :: Nat) r (proxy :: Nat -> *).
(1 <= w) =>
proxy w -> (BVIsNonZero w => r) -> r
bvIsNonZeroFromGEq1 (forall (t :: Nat). Proxy t
forall {k} (t :: k). Proxy t
Proxy @r) ((BVIsNonZero r => SBVType n (WordN r)) -> SBVType n (WordN r))
-> (BVIsNonZero r => SBVType n (WordN r)) -> SBVType n (WordN r)
forall a b. (a -> b) -> a -> b
$
Proxy l
-> (BVIsNonZero l => SBVType n (WordN r)) -> SBVType n (WordN r)
forall (w :: Nat) r (proxy :: Nat -> *).
(1 <= w) =>
proxy w -> (BVIsNonZero w => r) -> r
bvIsNonZeroFromGEq1 (forall (t :: Nat). Proxy t
forall {k} (t :: k). Proxy t
Proxy @l) ((BVIsNonZero l => SBVType n (WordN r)) -> SBVType n (WordN r))
-> (BVIsNonZero l => SBVType n (WordN r)) -> SBVType n (WordN r)
forall a b. (a -> b) -> a -> b
$
Proxy (r - l)
-> (BVIsNonZero (r - l) => SBVType n (WordN r))
-> SBVType n (WordN r)
forall (w :: Nat) r (proxy :: Nat -> *).
(1 <= w) =>
proxy w -> (BVIsNonZero w => r) -> r
bvIsNonZeroFromGEq1 (forall (t :: Nat). Proxy t
forall {k} (t :: k). Proxy t
Proxy @(r - l)) ((BVIsNonZero (r - l) => SBVType n (WordN r))
-> SBVType n (WordN r))
-> (BVIsNonZero (r - l) => SBVType n (WordN r))
-> SBVType n (WordN r)
forall a b. (a -> b) -> a -> b
$
if Bool
signed then SBV (WordN l) -> SBV (WordN r)
forall (n :: Nat) (m :: Nat) (bv :: Nat -> *).
(KnownNat n, BVIsNonZero n, SymVal (bv n), KnownNat m,
BVIsNonZero m, SymVal (bv m), (n + 1) <= m, SFiniteBits (bv n),
SIntegral (bv (m - n)), BVIsNonZero (m - n)) =>
SBV (bv n) -> SBV (bv m)
SBV.signExtend SBV (WordN l)
SBVType n (WordN l)
bv else SBV (WordN l) -> SBV (WordN r)
forall (n :: Nat) (m :: Nat) (bv :: Nat -> *).
(KnownNat n, BVIsNonZero n, SymVal (bv n), KnownNat m,
BVIsNonZero m, SymVal (bv m), (n + 1) <= m, SIntegral (bv (m - n)),
BVIsNonZero (m - n)) =>
SBV (bv n) -> SBV (bv m)
SBV.zeroExtend SBV (WordN l)
SBVType n (WordN l)
bv
instance PEvalBVTerm IntN where
pevalBVSelectTerm :: forall (n :: Nat) (ix :: Nat) (w :: Nat) (p :: Nat -> *)
(q :: Nat -> *).
(KnownNat n, KnownNat ix, KnownNat w, 1 <= n, 1 <= w,
(ix + w) <= n) =>
p ix -> q w -> Term (IntN n) -> Term (IntN w)
pevalBVSelectTerm = p ix -> q w -> Term (IntN n) -> Term (IntN w)
forall (bv :: Nat -> *) (n :: Nat) (ix :: Nat) (w :: Nat)
(p :: Nat -> *) (q :: Nat -> *).
(KnownNat n, KnownNat ix, KnownNat w, 1 <= n, 1 <= w,
(ix + w) <= n, PEvalBVTerm bv) =>
p ix -> q w -> Term (bv n) -> Term (bv w)
pevalDefaultBVSelectTerm
pevalBVConcatTerm :: forall (l :: Nat) (r :: Nat).
(KnownNat l, KnownNat r, 1 <= l, 1 <= r) =>
Term (IntN l) -> Term (IntN r) -> Term (IntN (l + r))
pevalBVConcatTerm = Term (IntN l) -> Term (IntN r) -> Term (IntN (l + r))
forall (bv :: Nat -> *) (a :: Nat) (b :: Nat).
(KnownNat a, KnownNat b, 1 <= a, 1 <= b, PEvalBVTerm bv) =>
Term (bv a) -> Term (bv b) -> Term (bv (a + b))
pevalDefaultBVConcatTerm
pevalBVExtendTerm :: forall (l :: Nat) (r :: Nat) (proxy :: Nat -> *).
(KnownNat l, KnownNat r, 1 <= l, 1 <= r, l <= r) =>
Bool -> proxy r -> Term (IntN l) -> Term (IntN r)
pevalBVExtendTerm = Bool -> proxy r -> Term (IntN l) -> Term (IntN r)
forall (proxy :: Nat -> *) (l :: Nat) (r :: Nat) (bv :: Nat -> *).
(PEvalBVTerm bv, KnownNat l, KnownNat r, 1 <= l, 1 <= r, l <= r) =>
Bool -> proxy r -> Term (bv l) -> Term (bv r)
pevalDefaultBVExtendTerm
sbvBVConcatTerm :: forall (n :: Nat) (l :: Nat) (r :: Nat) (p0 :: Nat -> *)
(p1 :: Nat -> *) (p2 :: Nat -> *).
(KnownIsZero n, KnownNat l, KnownNat r, 1 <= l, 1 <= r) =>
p0 n
-> p1 l
-> p2 r
-> SBVType n (IntN l)
-> SBVType n (IntN r)
-> SBVType n (IntN (l + r))
sbvBVConcatTerm p0 n
pn (p1 l
pl :: p l) (p2 r
pr :: q r) SBVType n (IntN l)
l SBVType n (IntN r)
r =
p1 l
-> (BVIsNonZero l => SBVType n (IntN (l + r)))
-> SBVType n (IntN (l + r))
forall (w :: Nat) r (proxy :: Nat -> *).
(1 <= w) =>
proxy w -> (BVIsNonZero w => r) -> r
bvIsNonZeroFromGEq1 p1 l
pl ((BVIsNonZero l => SBVType n (IntN (l + r)))
-> SBVType n (IntN (l + r)))
-> (BVIsNonZero l => SBVType n (IntN (l + r)))
-> SBVType n (IntN (l + r))
forall a b. (a -> b) -> a -> b
$
p2 r
-> (BVIsNonZero r => SBVType n (IntN (l + r)))
-> SBVType n (IntN (l + r))
forall (w :: Nat) r (proxy :: Nat -> *).
(1 <= w) =>
proxy w -> (BVIsNonZero w => r) -> r
bvIsNonZeroFromGEq1 p2 r
pr ((BVIsNonZero r => SBVType n (IntN (l + r)))
-> SBVType n (IntN (l + r)))
-> (BVIsNonZero r => SBVType n (IntN (l + r)))
-> SBVType n (IntN (l + r))
forall a b. (a -> b) -> a -> b
$
NatRepr (l + r)
-> (KnownNat (l + r) => SBVType n (IntN (l + r)))
-> SBVType n (IntN (l + r))
forall (n :: Nat) r. NatRepr n -> (KnownNat n => r) -> r
withKnownNat (NatRepr l -> NatRepr r -> NatRepr (l + r)
forall (m :: Nat) (n :: Nat).
NatRepr m -> NatRepr n -> NatRepr (m + n)
addNat (forall (n :: Nat). KnownNat n => NatRepr n
natRepr @l) (forall (n :: Nat). KnownNat n => NatRepr n
natRepr @r)) ((KnownNat (l + r) => SBVType n (IntN (l + r)))
-> SBVType n (IntN (l + r)))
-> (KnownNat (l + r) => SBVType n (IntN (l + r)))
-> SBVType n (IntN (l + r))
forall a b. (a -> b) -> a -> b
$
case forall (m :: Nat) (n :: Nat). LeqProof m n
unsafeLeqProof @1 @(l + r) of
LeqProof 1 (l + r)
LeqProof ->
Proxy (l + r)
-> (BVIsNonZero (l + r) => SBVType n (IntN (l + r)))
-> SBVType n (IntN (l + r))
forall (w :: Nat) r (proxy :: Nat -> *).
(1 <= w) =>
proxy w -> (BVIsNonZero w => r) -> r
bvIsNonZeroFromGEq1 (forall (t :: Nat). Proxy t
forall {k} (t :: k). Proxy t
Proxy @(l + r)) ((BVIsNonZero (l + r) => SBVType n (IntN (l + r)))
-> SBVType n (IntN (l + r)))
-> (BVIsNonZero (l + r) => SBVType n (IntN (l + r)))
-> SBVType n (IntN (l + r))
forall a b. (a -> b) -> a -> b
$
Proxy WordN
-> Proxy (l + r)
-> p0 n
-> SBVType n (WordN (l + r))
-> SBVType n (IntN (l + r))
forall (n :: Nat) (integerBitwidth :: Nat) (o :: (Nat -> *) -> *)
(p :: Nat -> *) (q :: Nat -> *).
(KnownIsZero integerBitwidth, KnownNat n, 1 <= n) =>
o WordN
-> p n
-> q integerBitwidth
-> SBVType integerBitwidth (WordN n)
-> SBVType integerBitwidth (IntN n)
forall (u :: Nat -> *) (s :: Nat -> *) (n :: Nat)
(integerBitwidth :: Nat) (o :: (Nat -> *) -> *) (p :: Nat -> *)
(q :: Nat -> *).
(PEvalBVSignConversionTerm u s, KnownIsZero integerBitwidth,
KnownNat n, 1 <= n) =>
o u
-> p n
-> q integerBitwidth
-> SBVType integerBitwidth (u n)
-> SBVType integerBitwidth (s n)
sbvToSigned (forall {k} (t :: k). Proxy t
forall (t :: Nat -> *). Proxy t
Proxy @WordN) (forall (t :: Nat). Proxy t
forall {k} (t :: k). Proxy t
Proxy @(l + r)) p0 n
pn (SBVType n (WordN (l + r)) -> SBVType n (IntN (l + r)))
-> SBVType n (WordN (l + r)) -> SBVType n (IntN (l + r))
forall a b. (a -> b) -> a -> b
$
Proxy IntN
-> p1 l -> p0 n -> SBVType n (IntN l) -> SBVType n (WordN l)
forall (n :: Nat) (integerBitwidth :: Nat) (o :: (Nat -> *) -> *)
(p :: Nat -> *) (q :: Nat -> *).
(KnownIsZero integerBitwidth, KnownNat n, 1 <= n) =>
o IntN
-> p n
-> q integerBitwidth
-> SBVType integerBitwidth (IntN n)
-> SBVType integerBitwidth (WordN n)
forall (u :: Nat -> *) (s :: Nat -> *) (n :: Nat)
(integerBitwidth :: Nat) (o :: (Nat -> *) -> *) (p :: Nat -> *)
(q :: Nat -> *).
(PEvalBVSignConversionTerm u s, KnownIsZero integerBitwidth,
KnownNat n, 1 <= n) =>
o s
-> p n
-> q integerBitwidth
-> SBVType integerBitwidth (s n)
-> SBVType integerBitwidth (u n)
sbvToUnsigned (forall {k} (t :: k). Proxy t
forall (t :: Nat -> *). Proxy t
Proxy @IntN) p1 l
pl p0 n
pn SBVType n (IntN l)
l
SBV (WordN l) -> SBV (WordN r) -> SBV (WordN (l + r))
forall (n :: Nat) (bv :: Nat -> *) (m :: Nat).
(KnownNat n, BVIsNonZero n, SymVal (bv n), KnownNat m,
BVIsNonZero m, SymVal (bv m)) =>
SBV (bv n) -> SBV (bv m) -> SBV (bv (n + m))
SBV.# Proxy IntN
-> p2 r -> p0 n -> SBVType n (IntN r) -> SBVType n (WordN r)
forall (n :: Nat) (integerBitwidth :: Nat) (o :: (Nat -> *) -> *)
(p :: Nat -> *) (q :: Nat -> *).
(KnownIsZero integerBitwidth, KnownNat n, 1 <= n) =>
o IntN
-> p n
-> q integerBitwidth
-> SBVType integerBitwidth (IntN n)
-> SBVType integerBitwidth (WordN n)
forall (u :: Nat -> *) (s :: Nat -> *) (n :: Nat)
(integerBitwidth :: Nat) (o :: (Nat -> *) -> *) (p :: Nat -> *)
(q :: Nat -> *).
(PEvalBVSignConversionTerm u s, KnownIsZero integerBitwidth,
KnownNat n, 1 <= n) =>
o s
-> p n
-> q integerBitwidth
-> SBVType integerBitwidth (s n)
-> SBVType integerBitwidth (u n)
sbvToUnsigned (forall {k} (t :: k). Proxy t
forall (t :: Nat -> *). Proxy t
Proxy @IntN) p2 r
pr p0 n
pn SBVType n (IntN r)
r
sbvBVSelectTerm :: forall (int :: Nat) (ix :: Nat) (w :: Nat) (n :: Nat)
(p0 :: Nat -> *) (p1 :: Nat -> *) (p2 :: Nat -> *)
(p3 :: Nat -> *).
(KnownIsZero int, KnownNat ix, KnownNat w, KnownNat n, 1 <= n,
1 <= w, (ix + w) <= n) =>
p0 int
-> p1 ix
-> p2 w
-> p3 n
-> SBVType int (IntN n)
-> SBVType int (IntN w)
sbvBVSelectTerm p0 int
_ (p1 ix
pix :: p0 ix) (p2 w
pw :: p1 w) (p3 n
pn :: p2 n) SBVType int (IntN n)
bv =
Proxy n
-> (BVIsNonZero n => SBVType int (IntN w)) -> SBVType int (IntN w)
forall (w :: Nat) r (proxy :: Nat -> *).
(1 <= w) =>
proxy w -> (BVIsNonZero w => r) -> r
bvIsNonZeroFromGEq1 (forall (t :: Nat). Proxy t
forall {k} (t :: k). Proxy t
Proxy @n) ((BVIsNonZero n => SBVType int (IntN w)) -> SBVType int (IntN w))
-> (BVIsNonZero n => SBVType int (IntN w)) -> SBVType int (IntN w)
forall a b. (a -> b) -> a -> b
$
Proxy w
-> (BVIsNonZero w => SBVType int (IntN w)) -> SBVType int (IntN w)
forall (w :: Nat) r (proxy :: Nat -> *).
(1 <= w) =>
proxy w -> (BVIsNonZero w => r) -> r
bvIsNonZeroFromGEq1 (forall (t :: Nat). Proxy t
forall {k} (t :: k). Proxy t
Proxy @w) ((BVIsNonZero w => SBVType int (IntN w)) -> SBVType int (IntN w))
-> (BVIsNonZero w => SBVType int (IntN w)) -> SBVType int (IntN w)
forall a b. (a -> b) -> a -> b
$
p1 ix -> p2 w -> p3 n -> SBV (IntN n) -> SBV (IntN w)
forall (ix :: Nat) (w :: Nat) (n :: Nat) (bv :: Nat -> *)
(p1 :: Nat -> *) (p2 :: Nat -> *) (p3 :: Nat -> *).
(KnownNat ix, KnownNat w, KnownNat n, 1 <= n, 1 <= w,
(ix + w) <= n, SymVal (bv n)) =>
p1 ix -> p2 w -> p3 n -> SBV (bv n) -> SBV (bv w)
sbvDefaultBVSelectTerm p1 ix
pix p2 w
pw p3 n
pn SBV (IntN n)
SBVType int (IntN n)
bv
sbvBVExtendTerm :: forall (n :: Nat) (l :: Nat) (r :: Nat) (p0 :: Nat -> *)
(p1 :: Nat -> *) (p2 :: Nat -> *).
(KnownIsZero n, KnownNat l, KnownNat r, 1 <= l, 1 <= r, l <= r) =>
p0 n
-> p1 l -> p2 r -> Bool -> SBVType n (IntN l) -> SBVType n (IntN r)
sbvBVExtendTerm p0 n
_ (p1 l
_ :: p0 l) (p2 r
_ :: p1 r) Bool
signed SBVType n (IntN l)
bv =
KnownProof (r - l)
-> (KnownNat (r - l) => SBVType n (IntN r)) -> SBVType n (IntN r)
forall (n :: Nat) r. KnownProof n -> (KnownNat n => r) -> r
withKnownProof
(forall (n :: Nat). Nat -> KnownProof n
unsafeKnownProof @(r - l) (Proxy r -> Nat
forall (n :: Nat) (proxy :: Nat -> *). KnownNat n => proxy n -> Nat
natVal (forall (t :: Nat). Proxy t
forall {k} (t :: k). Proxy t
Proxy @r) Nat -> Nat -> Nat
forall a. Num a => a -> a -> a
- Proxy l -> Nat
forall (n :: Nat) (proxy :: Nat -> *). KnownNat n => proxy n -> Nat
natVal (forall (t :: Nat). Proxy t
forall {k} (t :: k). Proxy t
Proxy @l)))
((KnownNat (r - l) => SBVType n (IntN r)) -> SBVType n (IntN r))
-> (KnownNat (r - l) => SBVType n (IntN r)) -> SBVType n (IntN r)
forall a b. (a -> b) -> a -> b
$ case (forall (m :: Nat) (n :: Nat). LeqProof m n
unsafeLeqProof @(l + 1) @r, forall (m :: Nat) (n :: Nat). LeqProof m n
unsafeLeqProof @1 @(r - l)) of
(LeqProof (l + 1) r
LeqProof, LeqProof 1 (r - l)
LeqProof) ->
Proxy r
-> (BVIsNonZero r => SBVType n (IntN r)) -> SBVType n (IntN r)
forall (w :: Nat) r (proxy :: Nat -> *).
(1 <= w) =>
proxy w -> (BVIsNonZero w => r) -> r
bvIsNonZeroFromGEq1 (forall (t :: Nat). Proxy t
forall {k} (t :: k). Proxy t
Proxy @r) ((BVIsNonZero r => SBVType n (IntN r)) -> SBVType n (IntN r))
-> (BVIsNonZero r => SBVType n (IntN r)) -> SBVType n (IntN r)
forall a b. (a -> b) -> a -> b
$
Proxy l
-> (BVIsNonZero l => SBVType n (IntN r)) -> SBVType n (IntN r)
forall (w :: Nat) r (proxy :: Nat -> *).
(1 <= w) =>
proxy w -> (BVIsNonZero w => r) -> r
bvIsNonZeroFromGEq1 (forall (t :: Nat). Proxy t
forall {k} (t :: k). Proxy t
Proxy @l) ((BVIsNonZero l => SBVType n (IntN r)) -> SBVType n (IntN r))
-> (BVIsNonZero l => SBVType n (IntN r)) -> SBVType n (IntN r)
forall a b. (a -> b) -> a -> b
$
Proxy (r - l)
-> (BVIsNonZero (r - l) => SBVType n (IntN r))
-> SBVType n (IntN r)
forall (w :: Nat) r (proxy :: Nat -> *).
(1 <= w) =>
proxy w -> (BVIsNonZero w => r) -> r
bvIsNonZeroFromGEq1 (forall (t :: Nat). Proxy t
forall {k} (t :: k). Proxy t
Proxy @(r - l)) ((BVIsNonZero (r - l) => SBVType n (IntN r)) -> SBVType n (IntN r))
-> (BVIsNonZero (r - l) => SBVType n (IntN r))
-> SBVType n (IntN r)
forall a b. (a -> b) -> a -> b
$
if Bool
signed
then SBV (IntN l) -> SBV (IntN r)
forall (n :: Nat) (m :: Nat) (bv :: Nat -> *).
(KnownNat n, BVIsNonZero n, SymVal (bv n), KnownNat m,
BVIsNonZero m, SymVal (bv m), (n + 1) <= m, SFiniteBits (bv n),
SIntegral (bv (m - n)), BVIsNonZero (m - n)) =>
SBV (bv n) -> SBV (bv m)
SBV.signExtend SBV (IntN l)
SBVType n (IntN l)
bv
else
SBV (WordN r) -> SBV (IntN r)
forall a b.
(Integral a, HasKind a, Num a, SymVal a, HasKind b, Num b,
SymVal b) =>
SBV a -> SBV b
SBV.sFromIntegral
( SBV (WordN l) -> SBV (WordN r)
forall (n :: Nat) (m :: Nat) (bv :: Nat -> *).
(KnownNat n, BVIsNonZero n, SymVal (bv n), KnownNat m,
BVIsNonZero m, SymVal (bv m), (n + 1) <= m, SIntegral (bv (m - n)),
BVIsNonZero (m - n)) =>
SBV (bv n) -> SBV (bv m)
SBV.zeroExtend
(SBV (IntN l) -> SBV (WordN l)
forall a b.
(Integral a, HasKind a, Num a, SymVal a, HasKind b, Num b,
SymVal b) =>
SBV a -> SBV b
SBV.sFromIntegral SBV (IntN l)
SBVType n (IntN l)
bv :: SBV.SBV (SBV.WordN l)) ::
SBV.SBV (SBV.WordN r)
)
sbvDefaultBVSelectTerm ::
( KnownNat ix,
KnownNat w,
KnownNat n,
1 <= n,
1 <= w,
(ix + w) <= n,
SBV.SymVal (bv n)
) =>
p1 ix ->
p2 w ->
p3 n ->
SBV.SBV (bv n) ->
SBV.SBV (bv w)
sbvDefaultBVSelectTerm :: forall (ix :: Nat) (w :: Nat) (n :: Nat) (bv :: Nat -> *)
(p1 :: Nat -> *) (p2 :: Nat -> *) (p3 :: Nat -> *).
(KnownNat ix, KnownNat w, KnownNat n, 1 <= n, 1 <= w,
(ix + w) <= n, SymVal (bv n)) =>
p1 ix -> p2 w -> p3 n -> SBV (bv n) -> SBV (bv w)
sbvDefaultBVSelectTerm (p1 ix
_ :: p0 ix) (p2 w
_ :: p1 w) (p3 n
_ :: p2 n) SBV (bv n)
bv =
KnownProof ((w + ix) - 1)
-> (KnownNat ((w + ix) - 1) => SBV (bv w)) -> SBV (bv w)
forall (n :: Nat) r. KnownProof n -> (KnownNat n => r) -> r
withKnownProof
( forall (n :: Nat). Nat -> KnownProof n
unsafeKnownProof @(w + ix - 1)
(Proxy w -> Nat
forall (n :: Nat) (proxy :: Nat -> *). KnownNat n => proxy n -> Nat
natVal (forall (t :: Nat). Proxy t
forall {k} (t :: k). Proxy t
Proxy @w) Nat -> Nat -> Nat
forall a. Num a => a -> a -> a
+ Proxy ix -> Nat
forall (n :: Nat) (proxy :: Nat -> *). KnownNat n => proxy n -> Nat
natVal (forall (t :: Nat). Proxy t
forall {k} (t :: k). Proxy t
Proxy @ix) Nat -> Nat -> Nat
forall a. Num a => a -> a -> a
- Nat
1)
)
((KnownNat ((w + ix) - 1) => SBV (bv w)) -> SBV (bv w))
-> (KnownNat ((w + ix) - 1) => SBV (bv w)) -> SBV (bv w)
forall a b. (a -> b) -> a -> b
$ case ( forall (a :: Nat) (b :: Nat). a :~: b
forall {k} (a :: k) (b :: k). a :~: b
unsafeAxiom @(w + ix - 1 - ix + 1) @w,
forall (m :: Nat) (n :: Nat). LeqProof m n
unsafeLeqProof @(((w + ix) - 1) + 1) @n,
forall (m :: Nat) (n :: Nat). LeqProof m n
unsafeLeqProof @ix @(w + ix - 1)
) of
(((((w + ix) - 1) - ix) + 1) :~: w
Refl, LeqProof (((w + ix) - 1) + 1) n
LeqProof, LeqProof ix ((w + ix) - 1)
LeqProof) ->
Proxy n -> (BVIsNonZero n => SBV (bv w)) -> SBV (bv w)
forall (w :: Nat) r (proxy :: Nat -> *).
(1 <= w) =>
proxy w -> (BVIsNonZero w => r) -> r
bvIsNonZeroFromGEq1 (forall (t :: Nat). Proxy t
forall {k} (t :: k). Proxy t
Proxy @n) ((BVIsNonZero n => SBV (bv w)) -> SBV (bv w))
-> (BVIsNonZero n => SBV (bv w)) -> SBV (bv w)
forall a b. (a -> b) -> a -> b
$
Proxy w -> (BVIsNonZero w => SBV (bv w)) -> SBV (bv w)
forall (w :: Nat) r (proxy :: Nat -> *).
(1 <= w) =>
proxy w -> (BVIsNonZero w => r) -> r
bvIsNonZeroFromGEq1 (forall (t :: Nat). Proxy t
forall {k} (t :: k). Proxy t
Proxy @w) ((BVIsNonZero w => SBV (bv w)) -> SBV (bv w))
-> (BVIsNonZero w => SBV (bv w)) -> SBV (bv w)
forall a b. (a -> b) -> a -> b
$
Proxy ((w + ix) - 1)
-> Proxy ix -> SBV (bv n) -> SBV (bv ((((w + ix) - 1) - ix) + 1))
forall (i :: Nat) (j :: Nat) (n :: Nat) (bv :: Nat -> *)
(proxy :: Nat -> *).
(KnownNat n, BVIsNonZero n, SymVal (bv n), KnownNat i, KnownNat j,
(i + 1) <= n, j <= i, BVIsNonZero ((i - j) + 1)) =>
proxy i -> proxy j -> SBV (bv n) -> SBV (bv ((i - j) + 1))
SBV.bvExtract (forall (t :: Nat). Proxy t
forall {k} (t :: k). Proxy t
Proxy @(w + ix - 1)) (forall (t :: Nat). Proxy t
forall {k} (t :: k). Proxy t
Proxy @ix) SBV (bv n)
bv