{-# 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)))
-- 1. [c1 c2] -> c1c2
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'
-- 2. [c1 (c2 ?)] -> (c1c2 ?)
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)
-- 3. [c1 (s c2)] -> (c1 (s c2))
doPevalDefaultBVConcatTerm (ConTerm {}) (BVConcatTerm Id
_ Term (bv l)
_ ConTerm {}) = Maybe (Term (bv (l + r)))
forall a. Maybe a
Nothing
-- 4. [(c s) ?) -> (c [s ?])
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
-- 5. [? (c1 (s2 c2))] -> (([? c1] s2) c2)
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
-- 6. [(s1 c1) c2] -> (s1 c1c2)
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
-- 7. [(s1 c1) (c2 s2)] -> (s1 (c1c2 s2))
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
-- 8. [?notc (s2 c)] -> ((s1 s2) c)
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