{-# LANGUAGE DataKinds #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE QuantifiedConstraints #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE UndecidableInstances #-}

-- |
-- Module      :   Grisette.IR.SymPrim.Data.Prim.PartialEval.BV
-- Copyright   :   (c) Sirui Lu 2021-2023
-- License     :   BSD-3-Clause (see the LICENSE file)
--
-- Maintainer  :   siruilu@cs.washington.edu
-- Stability   :   Experimental
-- Portability :   GHC only
module Grisette.IR.SymPrim.Data.Prim.PartialEval.BV
  ( pevalBVToSignedTerm,
    pevalBVToUnsignedTerm,
    pevalBVConcatTerm,
    pevalBVSelectTerm,
    pevalBVExtendTerm,
    pevalBVZeroExtendTerm,
    pevalBVSignExtendTerm,
  )
where

import Data.Typeable
import GHC.TypeNats
import Grisette.Core.Data.Class.BitVector
import Grisette.IR.SymPrim.Data.Prim.InternedTerm.InternedCtors
import Grisette.IR.SymPrim.Data.Prim.InternedTerm.Term
import Grisette.IR.SymPrim.Data.Prim.InternedTerm.TermUtils
import Grisette.IR.SymPrim.Data.Prim.PartialEval.Unfold

-- ToSigned
pevalBVToSignedTerm ::
  ( forall n. (KnownNat n, 1 <= n) => SupportedPrim (ubv n),
    forall n. (KnownNat n, 1 <= n) => SupportedPrim (sbv n),
    Typeable ubv,
    Typeable sbv,
    KnownNat n,
    1 <= n,
    BVSignConversion (ubv n) (sbv n)
  ) =>
  Term (ubv n) ->
  Term (sbv n)
pevalBVToSignedTerm :: forall (ubv :: Nat -> *) (sbv :: Nat -> *) (n :: Nat).
(forall (n :: Nat). (KnownNat n, 1 <= n) => SupportedPrim (ubv n),
 forall (n :: Nat). (KnownNat n, 1 <= n) => SupportedPrim (sbv n),
 Typeable ubv, Typeable sbv, KnownNat n, 1 <= n,
 BVSignConversion (ubv n) (sbv n)) =>
Term (ubv n) -> Term (sbv n)
pevalBVToSignedTerm = forall a b.
(Typeable a, SupportedPrim b) =>
PartialRuleUnary a b -> TotalRuleUnary a b -> TotalRuleUnary a b
unaryUnfoldOnce forall (ubv :: Nat -> *) (sbv :: Nat -> *) (n :: Nat).
(forall (n :: Nat). (KnownNat n, 1 <= n) => SupportedPrim (ubv n),
 forall (n :: Nat). (KnownNat n, 1 <= n) => SupportedPrim (sbv n),
 Typeable ubv, Typeable sbv, KnownNat n, 1 <= n,
 BVSignConversion (ubv n) (sbv n)) =>
Term (ubv n) -> Maybe (Term (sbv n))
doPevalBVToSignedTerm forall (ubv :: Nat -> *) (sbv :: Nat -> *) (n :: Nat).
(forall (n :: Nat). (KnownNat n, 1 <= n) => SupportedPrim (ubv n),
 forall (n :: Nat). (KnownNat n, 1 <= n) => SupportedPrim (sbv n),
 Typeable ubv, Typeable sbv, KnownNat n, 1 <= n,
 BVSignConversion (ubv n) (sbv n)) =>
Term (ubv n) -> Term (sbv n)
bvToSignedTerm

doPevalBVToSignedTerm ::
  ( forall n. (KnownNat n, 1 <= n) => SupportedPrim (ubv n),
    forall n. (KnownNat n, 1 <= n) => SupportedPrim (sbv n),
    Typeable ubv,
    Typeable sbv,
    KnownNat n,
    1 <= n,
    BVSignConversion (ubv n) (sbv n)
  ) =>
  Term (ubv n) ->
  Maybe (Term (sbv n))
doPevalBVToSignedTerm :: forall (ubv :: Nat -> *) (sbv :: Nat -> *) (n :: Nat).
(forall (n :: Nat). (KnownNat n, 1 <= n) => SupportedPrim (ubv n),
 forall (n :: Nat). (KnownNat n, 1 <= n) => SupportedPrim (sbv n),
 Typeable ubv, Typeable sbv, KnownNat n, 1 <= n,
 BVSignConversion (ubv n) (sbv n)) =>
Term (ubv n) -> Maybe (Term (sbv n))
doPevalBVToSignedTerm (ConTerm Id
_ ubv n
b) = forall a. a -> Maybe a
Just forall a b. (a -> b) -> a -> b
$ forall t.
(SupportedPrim t, Typeable t, Hashable t, Eq t, Show t) =>
t -> Term t
conTerm forall a b. (a -> b) -> a -> b
$ forall ubv sbv. BVSignConversion ubv sbv => ubv -> sbv
toSigned ubv n
b
doPevalBVToSignedTerm (BVToUnsignedTerm Id
_ Term (sbv n)
b) = forall a. a -> Maybe a
Just Term (sbv n)
b forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= forall a b. Typeable b => Term a -> Maybe (Term b)
castTerm
doPevalBVToSignedTerm Term (ubv n)
_ = forall a. Maybe a
Nothing

-- ToUnsigned
{-
bvToUnsignedTerm ::
  ( forall n. (KnownNat n, 1 <= n) => SupportedPrim (sbv n),
    forall n. (KnownNat n, 1 <= n) => SupportedPrim (ubv n),
    Typeable sbv,
    Typeable ubv,
    KnownNat n,
    1 <= n,
    BVToUnsigned (sbv n) (ubv n)
  ) =>
  Term (sbv n) ->
  Term (ubv n)
bvToUnsignedTerm = internTerm . UBVToUnsignedTerm
-}
pevalBVToUnsignedTerm ::
  ( forall n. (KnownNat n, 1 <= n) => SupportedPrim (ubv n),
    forall n. (KnownNat n, 1 <= n) => SupportedPrim (sbv n),
    Typeable ubv,
    Typeable sbv,
    KnownNat n,
    1 <= n,
    BVSignConversion (ubv n) (sbv n)
  ) =>
  Term (sbv n) ->
  Term (ubv n)
pevalBVToUnsignedTerm :: forall (ubv :: Nat -> *) (sbv :: Nat -> *) (n :: Nat).
(forall (n :: Nat). (KnownNat n, 1 <= n) => SupportedPrim (ubv n),
 forall (n :: Nat). (KnownNat n, 1 <= n) => SupportedPrim (sbv n),
 Typeable ubv, Typeable sbv, KnownNat n, 1 <= n,
 BVSignConversion (ubv n) (sbv n)) =>
Term (sbv n) -> Term (ubv n)
pevalBVToUnsignedTerm = forall a b.
(Typeable a, SupportedPrim b) =>
PartialRuleUnary a b -> TotalRuleUnary a b -> TotalRuleUnary a b
unaryUnfoldOnce forall (ubv :: Nat -> *) (sbv :: Nat -> *) (n :: Nat).
(forall (n :: Nat). (KnownNat n, 1 <= n) => SupportedPrim (ubv n),
 forall (n :: Nat). (KnownNat n, 1 <= n) => SupportedPrim (sbv n),
 Typeable ubv, Typeable sbv, KnownNat n, 1 <= n,
 BVSignConversion (ubv n) (sbv n)) =>
Term (sbv n) -> Maybe (Term (ubv n))
doPevalBVToUnsignedTerm forall (ubv :: Nat -> *) (sbv :: Nat -> *) (n :: Nat).
(forall (n :: Nat). (KnownNat n, 1 <= n) => SupportedPrim (ubv n),
 forall (n :: Nat). (KnownNat n, 1 <= n) => SupportedPrim (sbv n),
 Typeable ubv, Typeable sbv, KnownNat n, 1 <= n,
 BVSignConversion (ubv n) (sbv n)) =>
Term (sbv n) -> Term (ubv n)
bvToUnsignedTerm

doPevalBVToUnsignedTerm ::
  ( forall n. (KnownNat n, 1 <= n) => SupportedPrim (ubv n),
    forall n. (KnownNat n, 1 <= n) => SupportedPrim (sbv n),
    Typeable ubv,
    Typeable sbv,
    KnownNat n,
    1 <= n,
    BVSignConversion (ubv n) (sbv n)
  ) =>
  Term (sbv n) ->
  Maybe (Term (ubv n))
doPevalBVToUnsignedTerm :: forall (ubv :: Nat -> *) (sbv :: Nat -> *) (n :: Nat).
(forall (n :: Nat). (KnownNat n, 1 <= n) => SupportedPrim (ubv n),
 forall (n :: Nat). (KnownNat n, 1 <= n) => SupportedPrim (sbv n),
 Typeable ubv, Typeable sbv, KnownNat n, 1 <= n,
 BVSignConversion (ubv n) (sbv n)) =>
Term (sbv n) -> Maybe (Term (ubv n))
doPevalBVToUnsignedTerm (ConTerm Id
_ sbv n
b) = forall a. a -> Maybe a
Just forall a b. (a -> b) -> a -> b
$ forall t.
(SupportedPrim t, Typeable t, Hashable t, Eq t, Show t) =>
t -> Term t
conTerm forall a b. (a -> b) -> a -> b
$ forall ubv sbv. BVSignConversion ubv sbv => sbv -> ubv
toUnsigned sbv n
b
doPevalBVToUnsignedTerm (BVToSignedTerm Id
_ Term (ubv n)
b) = forall a. a -> Maybe a
Just Term (ubv n)
b forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= forall a b. Typeable b => Term a -> Maybe (Term b)
castTerm
doPevalBVToUnsignedTerm Term (sbv n)
_ = forall a. Maybe a
Nothing

-- select
pevalBVSelectTerm ::
  forall bv n ix w p q.
  ( forall n. (KnownNat n, 1 <= n) => SupportedPrim (bv n),
    Typeable bv,
    KnownNat n,
    KnownNat ix,
    KnownNat w,
    1 <= n,
    1 <= w,
    ix + w <= n,
    SizedBV bv
  ) =>
  p ix ->
  q w ->
  Term (bv n) ->
  Term (bv w)
pevalBVSelectTerm :: forall (bv :: Nat -> *) (n :: Nat) (ix :: Nat) (w :: Nat)
       (p :: Nat -> *) (q :: Nat -> *).
(forall (n :: Nat). (KnownNat n, 1 <= n) => SupportedPrim (bv n),
 Typeable bv, KnownNat n, KnownNat ix, KnownNat w, 1 <= n, 1 <= w,
 (ix + w) <= n, SizedBV bv) =>
p ix -> q w -> Term (bv n) -> Term (bv w)
pevalBVSelectTerm p ix
ix q w
w = forall a b.
(Typeable a, SupportedPrim b) =>
PartialRuleUnary a b -> TotalRuleUnary a b -> TotalRuleUnary a b
unaryUnfoldOnce (forall (bv :: Nat -> *) (n :: Nat) (ix :: Nat) (w :: Nat)
       (p :: Nat -> *) (q :: Nat -> *).
(forall (n :: Nat). (KnownNat n, 1 <= n) => SupportedPrim (bv n),
 Typeable bv, KnownNat n, KnownNat ix, KnownNat w, 1 <= n, 1 <= w,
 (ix + w) <= n, SizedBV bv) =>
p ix -> q w -> Term (bv n) -> Maybe (Term (bv w))
doPevalBVSelectTerm p ix
ix q w
w) (forall (bv :: Nat -> *) (n :: Nat) (ix :: Nat) (w :: Nat)
       (p :: Nat -> *) (q :: Nat -> *).
(forall (n :: Nat). (KnownNat n, 1 <= n) => SupportedPrim (bv n),
 Typeable bv, KnownNat n, KnownNat ix, KnownNat w, 1 <= n, 1 <= w,
 (ix + w) <= n, SizedBV bv) =>
p ix -> q w -> Term (bv n) -> Term (bv w)
bvselectTerm p ix
ix q w
w)

doPevalBVSelectTerm ::
  forall bv n ix w p q.
  ( forall n. (KnownNat n, 1 <= n) => SupportedPrim (bv n),
    Typeable bv,
    KnownNat n,
    KnownNat ix,
    KnownNat w,
    1 <= n,
    1 <= w,
    ix + w <= n,
    SizedBV bv
  ) =>
  p ix ->
  q w ->
  Term (bv n) ->
  Maybe (Term (bv w))
doPevalBVSelectTerm :: forall (bv :: Nat -> *) (n :: Nat) (ix :: Nat) (w :: Nat)
       (p :: Nat -> *) (q :: Nat -> *).
(forall (n :: Nat). (KnownNat n, 1 <= n) => SupportedPrim (bv n),
 Typeable bv, KnownNat n, KnownNat ix, KnownNat w, 1 <= n, 1 <= w,
 (ix + w) <= n, SizedBV bv) =>
p ix -> q w -> Term (bv n) -> Maybe (Term (bv w))
doPevalBVSelectTerm p ix
ix q w
w (ConTerm Id
_ bv n
b) = forall a. a -> Maybe a
Just forall a b. (a -> b) -> a -> b
$ forall t.
(SupportedPrim t, Typeable t, Hashable t, Eq t, Show t) =>
t -> Term t
conTerm forall a b. (a -> b) -> a -> b
$ 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
doPevalBVSelectTerm p ix
_ q w
_ Term (bv n)
_ = forall a. Maybe a
Nothing

-- ext
pevalBVZeroExtendTerm ::
  forall proxy l r bv.
  ( forall n. (KnownNat n, 1 <= n) => SupportedPrim (bv n),
    Typeable bv,
    KnownNat l,
    KnownNat r,
    1 <= l,
    1 <= r,
    l <= r,
    SizedBV bv
  ) =>
  proxy r ->
  Term (bv l) ->
  Term (bv r)
pevalBVZeroExtendTerm :: forall (proxy :: Nat -> *) (l :: Nat) (r :: Nat) (bv :: Nat -> *).
(forall (n :: Nat). (KnownNat n, 1 <= n) => SupportedPrim (bv n),
 Typeable bv, KnownNat l, KnownNat r, 1 <= l, 1 <= r, l <= r,
 SizedBV bv) =>
proxy r -> Term (bv l) -> Term (bv r)
pevalBVZeroExtendTerm = forall (proxy :: Nat -> *) (l :: Nat) (r :: Nat) (bv :: Nat -> *).
(forall (n :: Nat). (KnownNat n, 1 <= n) => SupportedPrim (bv n),
 Typeable bv, KnownNat l, KnownNat r, 1 <= l, 1 <= r, l <= r,
 SizedBV bv) =>
Bool -> proxy r -> Term (bv l) -> Term (bv r)
pevalBVExtendTerm Bool
False

pevalBVSignExtendTerm ::
  forall proxy l r bv.
  ( forall n. (KnownNat n, 1 <= n) => SupportedPrim (bv n),
    Typeable bv,
    KnownNat l,
    KnownNat r,
    1 <= l,
    1 <= r,
    l <= r,
    SizedBV bv
  ) =>
  proxy r ->
  Term (bv l) ->
  Term (bv r)
pevalBVSignExtendTerm :: forall (proxy :: Nat -> *) (l :: Nat) (r :: Nat) (bv :: Nat -> *).
(forall (n :: Nat). (KnownNat n, 1 <= n) => SupportedPrim (bv n),
 Typeable bv, KnownNat l, KnownNat r, 1 <= l, 1 <= r, l <= r,
 SizedBV bv) =>
proxy r -> Term (bv l) -> Term (bv r)
pevalBVSignExtendTerm = forall (proxy :: Nat -> *) (l :: Nat) (r :: Nat) (bv :: Nat -> *).
(forall (n :: Nat). (KnownNat n, 1 <= n) => SupportedPrim (bv n),
 Typeable bv, KnownNat l, KnownNat r, 1 <= l, 1 <= r, l <= r,
 SizedBV bv) =>
Bool -> proxy r -> Term (bv l) -> Term (bv r)
pevalBVExtendTerm Bool
True

pevalBVExtendTerm ::
  forall proxy l r bv.
  ( forall n. (KnownNat n, 1 <= n) => SupportedPrim (bv n),
    Typeable bv,
    KnownNat l,
    KnownNat r,
    1 <= l,
    1 <= r,
    l <= r,
    SizedBV bv
  ) =>
  Bool ->
  proxy r ->
  Term (bv l) ->
  Term (bv r)
pevalBVExtendTerm :: forall (proxy :: Nat -> *) (l :: Nat) (r :: Nat) (bv :: Nat -> *).
(forall (n :: Nat). (KnownNat n, 1 <= n) => SupportedPrim (bv n),
 Typeable bv, KnownNat l, KnownNat r, 1 <= l, 1 <= r, l <= r,
 SizedBV bv) =>
Bool -> proxy r -> Term (bv l) -> Term (bv r)
pevalBVExtendTerm Bool
signed proxy r
p = forall a b.
(Typeable a, SupportedPrim b) =>
PartialRuleUnary a b -> TotalRuleUnary a b -> TotalRuleUnary a b
unaryUnfoldOnce (forall (proxy :: Nat -> *) (l :: Nat) (r :: Nat) (bv :: Nat -> *).
(forall (n :: Nat). (KnownNat n, 1 <= n) => SupportedPrim (bv n),
 Typeable bv, KnownNat l, KnownNat r, 1 <= l, 1 <= r, l <= r,
 SizedBV bv) =>
Bool -> proxy r -> Term (bv l) -> Maybe (Term (bv r))
doPevalBVExtendTerm Bool
signed proxy r
p) (forall (bv :: Nat -> *) (l :: Nat) (r :: Nat) (proxy :: Nat -> *).
(forall (n :: Nat). (KnownNat n, 1 <= n) => SupportedPrim (bv n),
 Typeable bv, KnownNat l, KnownNat r, 1 <= l, 1 <= r, l <= r,
 SizedBV bv) =>
Bool -> proxy r -> Term (bv l) -> Term (bv r)
bvextendTerm Bool
signed proxy r
p)

doPevalBVExtendTerm ::
  forall proxy l r bv.
  ( forall n. (KnownNat n, 1 <= n) => SupportedPrim (bv n),
    Typeable bv,
    KnownNat l,
    KnownNat r,
    1 <= l,
    1 <= r,
    l <= r,
    SizedBV bv
  ) =>
  Bool ->
  proxy r ->
  Term (bv l) ->
  Maybe (Term (bv r))
doPevalBVExtendTerm :: forall (proxy :: Nat -> *) (l :: Nat) (r :: Nat) (bv :: Nat -> *).
(forall (n :: Nat). (KnownNat n, 1 <= n) => SupportedPrim (bv n),
 Typeable bv, KnownNat l, KnownNat r, 1 <= l, 1 <= r, l <= r,
 SizedBV bv) =>
Bool -> proxy r -> Term (bv l) -> Maybe (Term (bv r))
doPevalBVExtendTerm Bool
signed proxy r
p (ConTerm Id
_ bv l
b) = forall a. a -> Maybe a
Just forall a b. (a -> b) -> a -> b
$ forall t.
(SupportedPrim t, Typeable t, Hashable t, Eq t, Show t) =>
t -> Term t
conTerm forall a b. (a -> b) -> a -> b
$ if Bool
signed then 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 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
doPevalBVExtendTerm Bool
_ proxy r
_ Term (bv l)
_ = forall a. Maybe a
Nothing

pevalBVConcatTerm ::
  ( forall n. (KnownNat n, 1 <= n) => SupportedPrim (bv n),
    Typeable bv,
    KnownNat a,
    KnownNat b,
    KnownNat (a + b),
    1 <= a,
    1 <= b,
    1 <= a + b,
    SizedBV bv
  ) =>
  Term (bv a) ->
  Term (bv b) ->
  Term (bv (a + b))
pevalBVConcatTerm :: forall (bv :: Nat -> *) (a :: Nat) (b :: Nat).
(forall (n :: Nat). (KnownNat n, 1 <= n) => SupportedPrim (bv n),
 Typeable bv, KnownNat a, KnownNat b, KnownNat (a + b), 1 <= a,
 1 <= b, 1 <= (a + b), SizedBV bv) =>
Term (bv a) -> Term (bv b) -> Term (bv (a + b))
pevalBVConcatTerm = forall a b c.
(Typeable a, Typeable b, SupportedPrim c) =>
PartialRuleBinary a b c
-> TotalRuleBinary a b c -> TotalRuleBinary a b c
binaryUnfoldOnce forall (bv :: Nat -> *) (a :: Nat) (b :: Nat).
(forall (n :: Nat). (KnownNat n, 1 <= n) => SupportedPrim (bv n),
 Typeable bv, KnownNat a, KnownNat b, KnownNat (a + b), 1 <= a,
 1 <= b, 1 <= (a + b), SizedBV bv) =>
Term (bv a) -> Term (bv b) -> Maybe (Term (bv (a + b)))
doPevalBVConcatTerm forall (bv :: Nat -> *) (a :: Nat) (b :: Nat).
(forall (n :: Nat). (KnownNat n, 1 <= n) => SupportedPrim (bv n),
 Typeable bv, KnownNat a, KnownNat b, KnownNat (a + b), 1 <= a,
 1 <= b, 1 <= (a + b), SizedBV bv) =>
Term (bv a) -> Term (bv b) -> Term (bv (a + b))
bvconcatTerm

doPevalBVConcatTerm ::
  ( forall n. (KnownNat n, 1 <= n) => SupportedPrim (bv n),
    Typeable bv,
    KnownNat a,
    KnownNat b,
    KnownNat (a + b),
    1 <= a,
    1 <= b,
    1 <= (a + b),
    SizedBV bv
  ) =>
  Term (bv a) ->
  Term (bv b) ->
  Maybe (Term (bv (a + b)))
doPevalBVConcatTerm :: forall (bv :: Nat -> *) (a :: Nat) (b :: Nat).
(forall (n :: Nat). (KnownNat n, 1 <= n) => SupportedPrim (bv n),
 Typeable bv, KnownNat a, KnownNat b, KnownNat (a + b), 1 <= a,
 1 <= b, 1 <= (a + b), SizedBV bv) =>
Term (bv a) -> Term (bv b) -> Maybe (Term (bv (a + b)))
doPevalBVConcatTerm (ConTerm Id
_ bv a
v) (ConTerm Id
_ bv b
v') = forall a. a -> Maybe a
Just forall a b. (a -> b) -> a -> b
$ forall t.
(SupportedPrim t, Typeable t, Hashable t, Eq t, Show t) =>
t -> Term t
conTerm forall a b. (a -> b) -> a -> b
$ 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 a
v bv b
v'
doPevalBVConcatTerm Term (bv a)
_ Term (bv b)
_ = forall a. Maybe a
Nothing