{-# LANGUAGE AllowAmbiguousTypes #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE KindSignatures #-}
{-# HLINT ignore "Eta reduce" #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE PatternSynonyms #-}
{-# LANGUAGE QuantifiedConstraints #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE UndecidableInstances #-}
{-# OPTIONS_GHC -Wno-unrecognised-pragmas #-}

-- |
-- Module      :   Grisette.Internal.SymPrim.Prim.Internal.Instances.BVPEval
-- Copyright   :   (c) Sirui Lu 2024
-- License     :   BSD-3-Clause (see the LICENSE file)
--
-- Maintainer  :   siruilu@cs.washington.edu
-- Stability   :   Experimental
-- Portability :   GHC only
module Grisette.Internal.SymPrim.Prim.Internal.Instances.BVPEval () where

import Data.Kind (Type)
import Data.Maybe (isJust)
import Data.Proxy (Proxy (Proxy))
import qualified Data.SBV as SBV
import Data.Typeable (Typeable, type (:~:) (Refl))
import GHC.TypeNats (KnownNat, Nat, natVal, sameNat, type (+), type (-), type (<=))
import Grisette.Internal.Core.Data.Class.BitVector
  ( SizedBV
      ( sizedBVConcat,
        sizedBVFromIntegral,
        sizedBVSelect,
        sizedBVSext,
        sizedBVZext
      ),
  )
import Grisette.Internal.SymPrim.BV (IntN, WordN)
import Grisette.Internal.SymPrim.Prim.Internal.Instances.PEvalBitCastTerm (doPevalBitCast)
import Grisette.Internal.SymPrim.Prim.Internal.Instances.SupportedPrim
  ( bvIsNonZeroFromGEq1,
  )
import Grisette.Internal.SymPrim.Prim.Internal.Term
  ( PEvalBVTerm
      ( pevalBVConcatTerm,
        pevalBVExtendTerm,
        pevalBVSelectTerm,
        sbvBVConcatTerm,
        sbvBVExtendTerm,
        sbvBVSelectTerm
      ),
    PEvalBitCastTerm (pevalBitCastTerm, sbvBitCast),
    SupportedPrim,
    Term,
    bitCastTerm,
    bvConcatTerm,
    bvExtendTerm,
    bvSelectTerm,
    conTerm,
    pattern BVConcatTerm,
    pattern BVExtendTerm,
    pattern BVSelectTerm,
    pattern BitCastTerm,
    pattern ConTerm,
    pattern DynTerm,
  )
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,
  )

pevalDefaultBVSelectTerm ::
  forall (bv2 :: Nat -> Type) bv n ix w p q.
  ( KnownNat n,
    KnownNat ix,
    KnownNat w,
    1 <= n,
    1 <= w,
    ix + w <= n,
    PEvalBVTerm bv,
    forall x. (KnownNat x, 1 <= x) => PEvalBitCastTerm (bv2 x) (bv x),
    PEvalBVTerm bv2,
    Typeable bv,
    SupportedPrim (bv w),
    SupportedPrim (bv2 n)
  ) =>
  p ix ->
  q w ->
  Term (bv n) ->
  Term (bv w)
pevalDefaultBVSelectTerm :: forall (bv2 :: Nat -> *) (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,
 forall (x :: Nat).
 (KnownNat x, 1 <= x) =>
 PEvalBitCastTerm (bv2 x) (bv x),
 PEvalBVTerm bv2, Typeable bv, SupportedPrim (bv w),
 SupportedPrim (bv2 n)) =>
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 (forall (bv2 :: Nat -> *) (bv :: Nat -> *) (n :: Nat) (ix :: Nat)
       (w :: Nat) (p :: Nat -> *) (q :: Nat -> *).
(KnownNat n, KnownNat ix, KnownNat w,
 forall (x :: Nat).
 (KnownNat x, 1 <= x) =>
 PEvalBitCastTerm (bv2 x) (bv x),
 1 <= n, 1 <= w, (ix + w) <= n, PEvalBVTerm bv, PEvalBVTerm bv2,
 Typeable bv, SupportedPrim (bv w), SupportedPrim (bv2 n)) =>
p ix -> q w -> Term (bv n) -> Maybe (Term (bv w))
doPevalDefaultBVSelectTerm @bv2 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, SupportedPrim (bv w)) =>
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 (bv2 :: Nat -> Type) bv n ix w p q.
  ( KnownNat n,
    KnownNat ix,
    KnownNat w,
    forall x. (KnownNat x, 1 <= x) => PEvalBitCastTerm (bv2 x) (bv x),
    1 <= n,
    1 <= w,
    ix + w <= n,
    PEvalBVTerm bv,
    PEvalBVTerm bv2,
    Typeable bv,
    SupportedPrim (bv w),
    SupportedPrim (bv2 n)
  ) =>
  p ix ->
  q w ->
  Term (bv n) ->
  Maybe (Term (bv w))
doPevalDefaultBVSelectTerm :: forall (bv2 :: Nat -> *) (bv :: Nat -> *) (n :: Nat) (ix :: Nat)
       (w :: Nat) (p :: Nat -> *) (q :: Nat -> *).
(KnownNat n, KnownNat ix, KnownNat w,
 forall (x :: Nat).
 (KnownNat x, 1 <= x) =>
 PEvalBitCastTerm (bv2 x) (bv x),
 1 <= n, 1 <= w, (ix + w) <= n, PEvalBVTerm bv, PEvalBVTerm bv2,
 Typeable bv, SupportedPrim (bv w), SupportedPrim (bv2 n)) =>
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 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 => 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 (BitCastTerm (DynTerm (Term (bv2 n)
b :: Term (bv2 n)))) =
  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 (bv2 w) -> Term (bv w)
forall a b. PEvalBitCastTerm a b => Term a -> Term b
pevalBitCastTerm (Term (bv2 w) -> Term (bv w)) -> Term (bv2 w) -> Term (bv w)
forall a b. (a -> b) -> a -> b
$ p ix -> q w -> Term (bv2 n) -> Term (bv2 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 (bv2 n) -> Term (bv2 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 (bv2 n)
b
doPevalDefaultBVSelectTerm
  p ix
pix
  q w
pw
  (BVConcatTerm (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 (Proxy ix
_ :: proxy ix1) Proxy 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 Bool
signed Proxy 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,
    Typeable bv,
    forall n. (KnownNat n, 1 <= n) => SupportedPrim (bv n)
  ) =>
  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,
 Typeable bv,
 forall (n :: Nat). (KnownNat n, 1 <= n) => SupportedPrim (bv n)) =>
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,
 Typeable bv,
 forall (n :: Nat). (KnownNat n, 1 <= n) => SupportedPrim (bv n)) =>
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,
 SupportedPrim (bv 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,
    Typeable bv,
    forall n. (KnownNat n, 1 <= n) => SupportedPrim (bv n)
  ) =>
  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,
 Typeable bv,
 forall (n :: Nat). (KnownNat n, 1 <= n) => SupportedPrim (bv n)) =>
Bool -> proxy r -> Term (bv l) -> Maybe (Term (bv r))
doPevalDefaultBVExtendTerm Bool
signed proxy r
p (ConTerm 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 => 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 => 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 Bool
True Proxy 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,
    forall n. (KnownNat n, 1 <= n) => SupportedPrim (bv n)
  ) =>
  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,
 forall (n :: Nat). (KnownNat n, 1 <= n) => SupportedPrim (bv n)) =>
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.
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, KnownNat (l + r), 1 <= l, 1 <= r,
 1 <= (l + r), PEvalBVTerm bv,
 forall (n :: Nat). (KnownNat n, 1 <= n) => SupportedPrim (bv n)) =>
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), SupportedPrim (bv (l + r))) =>
Term (bv l) -> Term (bv r) -> Term (bv (l + r))
bvConcatTerm

unsafeBVConcatTerm ::
  forall bv n1 n2 r.
  (PEvalBVTerm bv, forall n. (KnownNat n, 1 <= n) => SupportedPrim (bv n)) =>
  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,
 forall (n :: Nat). (KnownNat n, 1 <= n) => SupportedPrim (bv n)) =>
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), SupportedPrim (bv (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,
    KnownNat (l + r),
    1 <= l,
    1 <= r,
    1 <= (l + r),
    PEvalBVTerm bv,
    forall n. (KnownNat n, 1 <= n) => SupportedPrim (bv n)
  ) =>
  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, KnownNat (l + r), 1 <= l, 1 <= r,
 1 <= (l + r), PEvalBVTerm bv,
 forall (n :: Nat). (KnownNat n, 1 <= n) => SupportedPrim (bv n)) =>
Term (bv l) -> Term (bv r) -> Maybe (Term (bv (l + r)))
doPevalDefaultBVConcatTerm (ConTerm bv l
v) (ConTerm 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 => 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 bv l
vl)
  (BVConcatTerm (ConTerm (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,
 forall (n :: Nat). (KnownNat n, 1 <= n) => SupportedPrim (bv n)) =>
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 => 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 Term (bv l)
_ ConTerm {}) = Maybe (Term (bv (l + r)))
forall a. Maybe a
Nothing
-- 4. [(c s) ?) -> (c [s ?])
doPevalDefaultBVConcatTerm
  (BVConcatTerm (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,
 forall (n :: Nat). (KnownNat n, 1 <= n) => SupportedPrim (bv n)) =>
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
      (rl :: Term (bv l)
rl@ConTerm {} :: Term (bv rl))
      (BVConcatTerm (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,
 forall (n :: Nat). (KnownNat n, 1 <= n) => SupportedPrim (bv n)) =>
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,
 forall (n :: Nat). (KnownNat n, 1 <= n) => SupportedPrim (bv n)) =>
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 (Term (bv l)
ll :: Term (bv ll)) ((ConTerm bv r
vlr) :: Term (bv lr)))
  (ConTerm 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,
 forall (n :: Nat). (KnownNat n, 1 <= n) => SupportedPrim (bv n)) =>
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 => 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 (Term (bv l)
ll :: Term (bv ll)) ((ConTerm bv r
vlr) :: Term (bv lr)))
  (BVConcatTerm ((ConTerm 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,
 forall (n :: Nat). (KnownNat n, 1 <= n) => SupportedPrim (bv n)) =>
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 => 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,
 forall (n :: Nat). (KnownNat n, 1 <= n) => SupportedPrim (bv n)) =>
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 (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,
 forall (n :: Nat). (KnownNat n, 1 <= n) => SupportedPrim (bv n)) =>
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,
 forall (n :: Nat). (KnownNat n, 1 <= n) => SupportedPrim (bv n)) =>
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 = forall (bv2 :: Nat -> *) (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,
 forall (x :: Nat).
 (KnownNat x, 1 <= x) =>
 PEvalBitCastTerm (bv2 x) (bv x),
 PEvalBVTerm bv2, Typeable bv, SupportedPrim (bv w),
 SupportedPrim (bv2 n)) =>
p ix -> q w -> Term (bv n) -> Term (bv w)
pevalDefaultBVSelectTerm @IntN
  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,
 forall (n :: Nat). (KnownNat n, 1 <= n) => SupportedPrim (bv n)) =>
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,
 Typeable bv,
 forall (n :: Nat). (KnownNat n, 1 <= n) => SupportedPrim (bv n)) =>
Bool -> proxy r -> Term (bv l) -> Term (bv r)
pevalDefaultBVExtendTerm
  sbvBVConcatTerm :: forall (l :: Nat) (r :: Nat) (p1 :: Nat -> *) (p2 :: Nat -> *).
(KnownNat l, KnownNat r, 1 <= l, 1 <= r) =>
p1 l
-> p2 r
-> SBVType (WordN l)
-> SBVType (WordN r)
-> SBVType (WordN (l + r))
sbvBVConcatTerm p1 l
pl p2 r
pr SBVType (WordN l)
l SBVType (WordN r)
r =
    p1 l
-> (BVIsNonZero l => SBVType (WordN (l + r)))
-> SBVType (WordN (l + r))
forall (w :: Nat) r (proxy :: Nat -> *).
(1 <= w) =>
proxy w -> (BVIsNonZero w => r) -> r
bvIsNonZeroFromGEq1 p1 l
pl ((BVIsNonZero l => SBVType (WordN (l + r)))
 -> SBVType (WordN (l + r)))
-> (BVIsNonZero l => SBVType (WordN (l + r)))
-> SBVType (WordN (l + r))
forall a b. (a -> b) -> a -> b
$
      p2 r
-> (BVIsNonZero r => SBVType (WordN (l + r)))
-> SBVType (WordN (l + r))
forall (w :: Nat) r (proxy :: Nat -> *).
(1 <= w) =>
proxy w -> (BVIsNonZero w => r) -> r
bvIsNonZeroFromGEq1 p2 r
pr ((BVIsNonZero r => SBVType (WordN (l + r)))
 -> SBVType (WordN (l + r)))
-> (BVIsNonZero r => SBVType (WordN (l + r)))
-> SBVType (WordN (l + r))
forall a b. (a -> b) -> a -> b
$
        SBV (WordN l)
SBVType (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 (WordN r)
r
  sbvBVSelectTerm :: forall (ix :: Nat) (w :: Nat) (n :: Nat) (p1 :: Nat -> *)
       (p2 :: Nat -> *) (p3 :: Nat -> *).
(KnownNat ix, KnownNat w, KnownNat n, 1 <= n, 1 <= w,
 (ix + w) <= n) =>
p1 ix -> p2 w -> p3 n -> SBVType (WordN n) -> SBVType (WordN w)
sbvBVSelectTerm (p1 ix
pix :: p0 ix) (p2 w
pw :: p1 w) (p3 n
pn :: p2 n) SBVType (WordN n)
bv =
    Proxy n
-> (BVIsNonZero n => SBVType (WordN w)) -> SBVType (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 (WordN w)) -> SBVType (WordN w))
-> (BVIsNonZero n => SBVType (WordN w)) -> SBVType (WordN w)
forall a b. (a -> b) -> a -> b
$
      Proxy w
-> (BVIsNonZero w => SBVType (WordN w)) -> SBVType (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 (WordN w)) -> SBVType (WordN w))
-> (BVIsNonZero w => SBVType (WordN w)) -> SBVType (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 (WordN n)
bv
  sbvBVExtendTerm :: forall (l :: Nat) (r :: Nat) (p1 :: Nat -> *) (p2 :: Nat -> *).
(KnownNat l, KnownNat r, 1 <= l, 1 <= r, l <= r) =>
p1 l -> p2 r -> Bool -> SBVType (WordN l) -> SBVType (WordN r)
sbvBVExtendTerm (p1 l
_ :: p0 l) (p2 r
_ :: p1 r) Bool
signed SBVType (WordN l)
bv =
    KnownProof (r - l)
-> (KnownNat (r - l) => SBVType (WordN r)) -> SBVType (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 (WordN r)) -> SBVType (WordN r))
-> (KnownNat (r - l) => SBVType (WordN r)) -> SBVType (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 (WordN r)) -> SBVType (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 (WordN r)) -> SBVType (WordN r))
-> (BVIsNonZero r => SBVType (WordN r)) -> SBVType (WordN r)
forall a b. (a -> b) -> a -> b
$
            Proxy l
-> (BVIsNonZero l => SBVType (WordN r)) -> SBVType (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 (WordN r)) -> SBVType (WordN r))
-> (BVIsNonZero l => SBVType (WordN r)) -> SBVType (WordN r)
forall a b. (a -> b) -> a -> b
$
              Proxy (r - l)
-> (BVIsNonZero (r - l) => SBVType (WordN r)) -> SBVType (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 (WordN r)) -> SBVType (WordN r))
-> (BVIsNonZero (r - l) => SBVType (WordN r)) -> SBVType (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 (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 (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 = forall (bv2 :: Nat -> *) (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,
 forall (x :: Nat).
 (KnownNat x, 1 <= x) =>
 PEvalBitCastTerm (bv2 x) (bv x),
 PEvalBVTerm bv2, Typeable bv, SupportedPrim (bv w),
 SupportedPrim (bv2 n)) =>
p ix -> q w -> Term (bv n) -> Term (bv w)
pevalDefaultBVSelectTerm @WordN
  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,
 forall (n :: Nat). (KnownNat n, 1 <= n) => SupportedPrim (bv n)) =>
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,
 Typeable bv,
 forall (n :: Nat). (KnownNat n, 1 <= n) => SupportedPrim (bv n)) =>
Bool -> proxy r -> Term (bv l) -> Term (bv r)
pevalDefaultBVExtendTerm
  sbvBVConcatTerm :: forall (l :: Nat) (r :: Nat) (p1 :: Nat -> *) (p2 :: Nat -> *).
(KnownNat l, KnownNat r, 1 <= l, 1 <= r) =>
p1 l
-> p2 r
-> SBVType (IntN l)
-> SBVType (IntN r)
-> SBVType (IntN (l + r))
sbvBVConcatTerm (p1 l
pl :: p l) (p2 r
pr :: q r) SBVType (IntN l)
l SBVType (IntN r)
r =
    p1 l
-> (BVIsNonZero l => SBVType (IntN (l + r)))
-> SBVType (IntN (l + r))
forall (w :: Nat) r (proxy :: Nat -> *).
(1 <= w) =>
proxy w -> (BVIsNonZero w => r) -> r
bvIsNonZeroFromGEq1 p1 l
pl ((BVIsNonZero l => SBVType (IntN (l + r)))
 -> SBVType (IntN (l + r)))
-> (BVIsNonZero l => SBVType (IntN (l + r)))
-> SBVType (IntN (l + r))
forall a b. (a -> b) -> a -> b
$
      p2 r
-> (BVIsNonZero r => SBVType (IntN (l + r)))
-> SBVType (IntN (l + r))
forall (w :: Nat) r (proxy :: Nat -> *).
(1 <= w) =>
proxy w -> (BVIsNonZero w => r) -> r
bvIsNonZeroFromGEq1 p2 r
pr ((BVIsNonZero r => SBVType (IntN (l + r)))
 -> SBVType (IntN (l + r)))
-> (BVIsNonZero r => SBVType (IntN (l + r)))
-> SBVType (IntN (l + r))
forall a b. (a -> b) -> a -> b
$
        NatRepr (l + r)
-> (KnownNat (l + r) => SBVType (IntN (l + r)))
-> SBVType (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 (IntN (l + r)))
 -> SBVType (IntN (l + r)))
-> (KnownNat (l + r) => SBVType (IntN (l + r)))
-> SBVType (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 (IntN (l + r)))
-> SBVType (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 (IntN (l + r)))
 -> SBVType (IntN (l + r)))
-> (BVIsNonZero (l + r) => SBVType (IntN (l + r)))
-> SBVType (IntN (l + r))
forall a b. (a -> b) -> a -> b
$
                forall a b. PEvalBitCastTerm a b => SBVType a -> SBVType b
sbvBitCast @(WordN (l + r)) @(IntN (l + r)) (SBVType (WordN (l + r)) -> SBVType (IntN (l + r)))
-> SBVType (WordN (l + r)) -> SBVType (IntN (l + r))
forall a b. (a -> b) -> a -> b
$
                  (forall a b. PEvalBitCastTerm a b => SBVType a -> SBVType b
sbvBitCast @(IntN l) @(WordN l) SBVType (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.# (forall a b. PEvalBitCastTerm a b => SBVType a -> SBVType b
sbvBitCast @(IntN r) @(WordN r) SBVType (IntN r)
r)
  sbvBVSelectTerm :: forall (ix :: Nat) (w :: Nat) (n :: Nat) (p1 :: Nat -> *)
       (p2 :: Nat -> *) (p3 :: Nat -> *).
(KnownNat ix, KnownNat w, KnownNat n, 1 <= n, 1 <= w,
 (ix + w) <= n) =>
p1 ix -> p2 w -> p3 n -> SBVType (IntN n) -> SBVType (IntN w)
sbvBVSelectTerm (p1 ix
pix :: p0 ix) (p2 w
pw :: p1 w) (p3 n
pn :: p2 n) SBVType (IntN n)
bv =
    Proxy n -> (BVIsNonZero n => SBVType (IntN w)) -> SBVType (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 (IntN w)) -> SBVType (IntN w))
-> (BVIsNonZero n => SBVType (IntN w)) -> SBVType (IntN w)
forall a b. (a -> b) -> a -> b
$
      Proxy w -> (BVIsNonZero w => SBVType (IntN w)) -> SBVType (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 (IntN w)) -> SBVType (IntN w))
-> (BVIsNonZero w => SBVType (IntN w)) -> SBVType (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 (IntN n)
bv
  sbvBVExtendTerm :: forall (l :: Nat) (r :: Nat) (p1 :: Nat -> *) (p2 :: Nat -> *).
(KnownNat l, KnownNat r, 1 <= l, 1 <= r, l <= r) =>
p1 l -> p2 r -> Bool -> SBVType (IntN l) -> SBVType (IntN r)
sbvBVExtendTerm (p1 l
_ :: p0 l) (p2 r
_ :: p1 r) Bool
signed SBVType (IntN l)
bv =
    KnownProof (r - l)
-> (KnownNat (r - l) => SBVType (IntN r)) -> SBVType (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 (IntN r)) -> SBVType (IntN r))
-> (KnownNat (r - l) => SBVType (IntN r)) -> SBVType (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 (IntN r)) -> SBVType (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 (IntN r)) -> SBVType (IntN r))
-> (BVIsNonZero r => SBVType (IntN r)) -> SBVType (IntN r)
forall a b. (a -> b) -> a -> b
$
            Proxy l -> (BVIsNonZero l => SBVType (IntN r)) -> SBVType (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 (IntN r)) -> SBVType (IntN r))
-> (BVIsNonZero l => SBVType (IntN r)) -> SBVType (IntN r)
forall a b. (a -> b) -> a -> b
$
              Proxy (r - l)
-> (BVIsNonZero (r - l) => SBVType (IntN r)) -> SBVType (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 (IntN r)) -> SBVType (IntN r))
-> (BVIsNonZero (r - l) => SBVType (IntN r)) -> SBVType (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 (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 (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

instance (KnownNat n, 1 <= n) => PEvalBitCastTerm (WordN n) (IntN n) where
  pevalBitCastTerm :: Term (WordN n) -> Term (IntN n)
pevalBitCastTerm = PartialRuleUnary (WordN n) (IntN n)
-> (Term (WordN n) -> Term (IntN n))
-> Term (WordN n)
-> Term (IntN n)
forall a b.
SupportedPrim b =>
PartialRuleUnary a b -> TotalRuleUnary a b -> TotalRuleUnary a b
unaryUnfoldOnce PartialRuleUnary (WordN n) (IntN n)
doPevalBitCastBV Term (WordN n) -> Term (IntN n)
forall a b.
(PEvalBitCastTerm a b, SupportedPrim b) =>
Term a -> Term b
bitCastTerm
    where
      doPevalBitCastBV :: Term (WordN n) -> Maybe (Term (IntN n))
      doPevalBitCastBV :: PartialRuleUnary (WordN n) (IntN n)
doPevalBitCastBV
        (BVConcatTerm (Term (WordN l)
l :: Term (WordN l)) (Term (WordN r)
r :: Term (WordN r))) =
          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
              (forall a b. PEvalBitCastTerm a b => Term a -> Term b
pevalBitCastTerm @(WordN l) @(IntN l) Term (WordN l)
l)
              (forall a b. PEvalBitCastTerm a b => Term a -> Term b
pevalBitCastTerm @(WordN r) @(IntN r) Term (WordN r)
r)
      doPevalBitCastBV (BVExtendTerm Bool
signed Proxy r
pr (Term (WordN l)
b :: Term (WordN l))) =
        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 -> Proxy 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 Proxy n
Proxy r
pr (Term (IntN l) -> Term (IntN n)) -> Term (IntN l) -> Term (IntN n)
forall a b. (a -> b) -> a -> b
$
            forall a b. PEvalBitCastTerm a b => Term a -> Term b
pevalBitCastTerm @(WordN l) @(IntN l) Term (WordN l)
b
      doPevalBitCastBV Term (WordN n)
v = PartialRuleUnary (WordN n) (IntN n)
forall a b.
(PEvalBitCastTerm a b, SupportedPrim b) =>
Term a -> Maybe (Term b)
doPevalBitCast Term (WordN n)
v
  sbvBitCast :: SBVType (WordN n) -> SBVType (IntN n)
sbvBitCast = Proxy n
-> (BVIsNonZero n => SBV (WordN n) -> SBV (IntN n))
-> SBV (WordN n)
-> SBV (IntN n)
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 (WordN n) -> SBV (IntN n)
SBV (WordN n) -> SBV (IntN n)
forall a b.
(Integral a, HasKind a, Num a, SymVal a, HasKind b, Num b,
 SymVal b) =>
SBV a -> SBV b
SBV.sFromIntegral

instance (KnownNat n, 1 <= n) => PEvalBitCastTerm (IntN n) (WordN n) where
  pevalBitCastTerm :: Term (IntN n) -> Term (WordN n)
pevalBitCastTerm = PartialRuleUnary (IntN n) (WordN n)
-> (Term (IntN n) -> Term (WordN n))
-> Term (IntN n)
-> Term (WordN n)
forall a b.
SupportedPrim b =>
PartialRuleUnary a b -> TotalRuleUnary a b -> TotalRuleUnary a b
unaryUnfoldOnce PartialRuleUnary (IntN n) (WordN n)
doPevalBitCastBV Term (IntN n) -> Term (WordN n)
forall a b.
(PEvalBitCastTerm a b, SupportedPrim b) =>
Term a -> Term b
bitCastTerm
    where
      doPevalBitCastBV :: Term (IntN n) -> Maybe (Term (WordN n))
      doPevalBitCastBV :: PartialRuleUnary (IntN n) (WordN n)
doPevalBitCastBV
        (BVConcatTerm (Term (IntN l)
l :: Term (IntN l)) (Term (IntN r)
r :: Term (IntN r))) =
          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
              (forall a b. PEvalBitCastTerm a b => Term a -> Term b
pevalBitCastTerm @(IntN l) @(WordN l) Term (IntN l)
l)
              (forall a b. PEvalBitCastTerm a b => Term a -> Term b
pevalBitCastTerm @(IntN r) @(WordN r) Term (IntN r)
r)
      doPevalBitCastBV (BVExtendTerm Bool
signed Proxy r
pr (Term (IntN l)
b :: Term (IntN l))) =
        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 -> Proxy 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 Proxy n
Proxy r
pr (Term (WordN l) -> Term (WordN n))
-> Term (WordN l) -> Term (WordN n)
forall a b. (a -> b) -> a -> b
$
            forall a b. PEvalBitCastTerm a b => Term a -> Term b
pevalBitCastTerm @(IntN l) @(WordN l) Term (IntN l)
b
      doPevalBitCastBV Term (IntN n)
v = PartialRuleUnary (IntN n) (WordN n)
forall a b.
(PEvalBitCastTerm a b, SupportedPrim b) =>
Term a -> Maybe (Term b)
doPevalBitCast Term (IntN n)
v
  sbvBitCast :: SBVType (IntN n) -> SBVType (WordN n)
sbvBitCast = Proxy n
-> (BVIsNonZero n => SBV (IntN n) -> SBV (WordN n))
-> SBV (IntN n)
-> SBV (WordN n)
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 (IntN n) -> SBV (WordN n)
SBV (IntN n) -> SBV (WordN n)
forall a b.
(Integral a, HasKind a, Num a, SymVal a, HasKind b, Num b,
 SymVal b) =>
SBV a -> SBV b
SBV.sFromIntegral