{-# 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
  ( pevalToSignedTerm,
    pevalToUnsignedTerm,
    pevalBVConcatTerm,
    pevalBVSelectTerm,
    pevalBVExtendTerm,
    pevalBVZeroExtendTerm,
    pevalBVSignExtendTerm,
  )
where

import Data.Typeable (Typeable)
import GHC.TypeNats (KnownNat, type (+), type (<=))
import Grisette.Core.Data.Class.BitVector
  ( SizedBV (sizedBVConcat, sizedBVSelect, sizedBVSext, sizedBVZext),
  )
import Grisette.Core.Data.Class.SignConversion (SignConversion (toSigned, toUnsigned))
import Grisette.IR.SymPrim.Data.Prim.InternedTerm.InternedCtors
  ( bvconcatTerm,
    bvextendTerm,
    bvselectTerm,
    conTerm,
    toSignedTerm,
    toUnsignedTerm,
  )
import Grisette.IR.SymPrim.Data.Prim.InternedTerm.Term
  ( SupportedPrim,
    Term (ConTerm, ToSignedTerm, ToUnsignedTerm),
  )
import Grisette.IR.SymPrim.Data.Prim.InternedTerm.TermUtils
  ( castTerm,
  )
import Grisette.IR.SymPrim.Data.Prim.PartialEval.Unfold
  ( binaryUnfoldOnce,
    unaryUnfoldOnce,
  )

-- ToSigned
pevalToSignedTerm ::
  ( SupportedPrim u,
    SupportedPrim s,
    SignConversion u s
  ) =>
  Term u ->
  Term s
pevalToSignedTerm :: forall u s.
(SupportedPrim u, SupportedPrim s, SignConversion u s) =>
Term u -> Term s
pevalToSignedTerm = PartialRuleUnary u s -> TotalRuleUnary u s -> TotalRuleUnary u s
forall a b.
(Typeable a, SupportedPrim b) =>
PartialRuleUnary a b -> TotalRuleUnary a b -> TotalRuleUnary a b
unaryUnfoldOnce PartialRuleUnary u s
forall u s.
(SupportedPrim u, SupportedPrim s, SignConversion u s) =>
Term u -> Maybe (Term s)
doPevalToSignedTerm TotalRuleUnary u s
forall u s.
(SupportedPrim u, SupportedPrim s, SignConversion u s) =>
Term u -> Term s
toSignedTerm

doPevalToSignedTerm ::
  ( SupportedPrim u,
    SupportedPrim s,
    SignConversion u s
  ) =>
  Term u ->
  Maybe (Term s)
doPevalToSignedTerm :: forall u s.
(SupportedPrim u, SupportedPrim s, SignConversion u s) =>
Term u -> Maybe (Term s)
doPevalToSignedTerm (ConTerm Id
_ u
b) = Term s -> Maybe (Term s)
forall a. a -> Maybe a
Just (Term s -> Maybe (Term s)) -> Term s -> Maybe (Term s)
forall a b. (a -> b) -> a -> b
$ s -> Term s
forall t.
(SupportedPrim t, Typeable t, Hashable t, Eq t, Show t) =>
t -> Term t
conTerm (s -> Term s) -> s -> Term s
forall a b. (a -> b) -> a -> b
$ u -> s
forall ubv sbv. SignConversion ubv sbv => ubv -> sbv
toSigned u
b
doPevalToSignedTerm (ToUnsignedTerm Id
_ Term s
b) = Term s -> Maybe (Term s)
forall a. a -> Maybe a
Just Term s
b Maybe (Term s) -> (Term s -> Maybe (Term s)) -> Maybe (Term s)
forall a b. Maybe a -> (a -> Maybe b) -> Maybe b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= Term s -> Maybe (Term s)
forall a b. Typeable b => Term a -> Maybe (Term b)
castTerm
doPevalToSignedTerm Term u
_ = Maybe (Term s)
forall a. Maybe a
Nothing

-- ToUnsigned
pevalToUnsignedTerm ::
  ( SupportedPrim u,
    SupportedPrim s,
    SignConversion u s
  ) =>
  Term s ->
  Term u
pevalToUnsignedTerm :: forall u s.
(SupportedPrim u, SupportedPrim s, SignConversion u s) =>
Term s -> Term u
pevalToUnsignedTerm = PartialRuleUnary s u -> TotalRuleUnary s u -> TotalRuleUnary s u
forall a b.
(Typeable a, SupportedPrim b) =>
PartialRuleUnary a b -> TotalRuleUnary a b -> TotalRuleUnary a b
unaryUnfoldOnce PartialRuleUnary s u
forall u s.
(SupportedPrim u, SupportedPrim s, SignConversion u s) =>
Term s -> Maybe (Term u)
doPevalToUnsignedTerm TotalRuleUnary s u
forall u s.
(SupportedPrim u, SupportedPrim s, SignConversion u s) =>
Term s -> Term u
toUnsignedTerm

doPevalToUnsignedTerm ::
  ( SupportedPrim u,
    SupportedPrim s,
    SignConversion u s
  ) =>
  Term s ->
  Maybe (Term u)
doPevalToUnsignedTerm :: forall u s.
(SupportedPrim u, SupportedPrim s, SignConversion u s) =>
Term s -> Maybe (Term u)
doPevalToUnsignedTerm (ConTerm Id
_ s
b) = Term u -> Maybe (Term u)
forall a. a -> Maybe a
Just (Term u -> Maybe (Term u)) -> Term u -> Maybe (Term u)
forall a b. (a -> b) -> a -> b
$ u -> Term u
forall t.
(SupportedPrim t, Typeable t, Hashable t, Eq t, Show t) =>
t -> Term t
conTerm (u -> Term u) -> u -> Term u
forall a b. (a -> b) -> a -> b
$ s -> u
forall ubv sbv. SignConversion ubv sbv => sbv -> ubv
toUnsigned s
b
doPevalToUnsignedTerm (ToSignedTerm Id
_ Term u
b) = Term u -> Maybe (Term u)
forall a. a -> Maybe a
Just Term u
b Maybe (Term u) -> (Term u -> Maybe (Term u)) -> Maybe (Term u)
forall a b. Maybe a -> (a -> Maybe b) -> Maybe b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= Term u -> Maybe (Term u)
forall a b. Typeable b => Term a -> Maybe (Term b)
castTerm
doPevalToUnsignedTerm Term s
_ = Maybe (Term u)
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 = PartialRuleUnary (bv n) (bv w)
-> TotalRuleUnary (bv n) (bv w) -> TotalRuleUnary (bv n) (bv w)
forall a b.
(Typeable a, SupportedPrim b) =>
PartialRuleUnary a b -> TotalRuleUnary a b -> TotalRuleUnary a b
unaryUnfoldOnce (p ix -> q w -> PartialRuleUnary (bv n) (bv w)
forall (bv :: Nat -> *) (n :: Nat) (ix :: Nat) (w :: Nat)
       (p :: Nat -> *) (q :: Nat -> *).
(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) (p ix -> q w -> TotalRuleUnary (bv n) (bv 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) = Term (bv w) -> Maybe (Term (bv w))
forall a. a -> Maybe a
Just (Term (bv w) -> Maybe (Term (bv w)))
-> Term (bv w) -> Maybe (Term (bv w))
forall a b. (a -> b) -> a -> b
$ bv w -> Term (bv w)
forall t.
(SupportedPrim t, Typeable t, Hashable t, Eq t, Show t) =>
t -> Term t
conTerm (bv w -> Term (bv w)) -> bv w -> Term (bv w)
forall a b. (a -> b) -> a -> b
$ p ix -> q w -> bv n -> bv w
forall (n :: Nat) (ix :: Nat) (w :: Nat) (p :: Nat -> *)
       (q :: Nat -> *).
(KnownNat n, KnownNat ix, KnownNat w, 1 <= n, 1 <= w,
 (ix + w) <= n) =>
p ix -> q w -> bv n -> bv w
forall (bv :: Nat -> *) (n :: Nat) (ix :: Nat) (w :: Nat)
       (p :: Nat -> *) (q :: Nat -> *).
(SizedBV bv, KnownNat n, KnownNat ix, KnownNat w, 1 <= n, 1 <= w,
 (ix + w) <= n) =>
p ix -> q w -> bv n -> bv w
sizedBVSelect p ix
ix q w
w bv n
b
doPevalBVSelectTerm p ix
_ q w
_ Term (bv n)
_ = Maybe (Term (bv w))
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 = Bool -> proxy r -> Term (bv l) -> Term (bv r)
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 = Bool -> proxy r -> Term (bv l) -> Term (bv r)
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 = PartialRuleUnary (bv l) (bv r)
-> TotalRuleUnary (bv l) (bv r) -> TotalRuleUnary (bv l) (bv r)
forall a b.
(Typeable a, 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 -> *).
(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) (Bool -> proxy r -> TotalRuleUnary (bv l) (bv r)
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) = Term (bv r) -> Maybe (Term (bv r))
forall a. a -> Maybe a
Just (Term (bv r) -> Maybe (Term (bv r)))
-> Term (bv r) -> Maybe (Term (bv r))
forall a b. (a -> b) -> a -> b
$ bv r -> Term (bv r)
forall t.
(SupportedPrim t, Typeable t, Hashable t, Eq t, Show t) =>
t -> Term t
conTerm (bv r -> Term (bv r)) -> bv r -> Term (bv r)
forall a b. (a -> b) -> a -> b
$ if Bool
signed then proxy r -> bv l -> bv r
forall (l :: Nat) (r :: Nat) (proxy :: Nat -> *).
(KnownNat l, KnownNat r, 1 <= l, KnownNat r, l <= r) =>
proxy r -> bv l -> bv r
forall (bv :: Nat -> *) (l :: Nat) (r :: Nat) (proxy :: Nat -> *).
(SizedBV bv, KnownNat l, KnownNat r, 1 <= l, KnownNat r, l <= r) =>
proxy r -> bv l -> bv r
sizedBVSext proxy r
p bv l
b else proxy r -> bv l -> bv r
forall (l :: Nat) (r :: Nat) (proxy :: Nat -> *).
(KnownNat l, KnownNat r, 1 <= l, KnownNat r, l <= r) =>
proxy r -> bv l -> bv r
forall (bv :: Nat -> *) (l :: Nat) (r :: Nat) (proxy :: Nat -> *).
(SizedBV bv, KnownNat l, KnownNat r, 1 <= l, KnownNat r, l <= r) =>
proxy r -> bv l -> bv r
sizedBVZext proxy r
p bv l
b
doPevalBVExtendTerm Bool
_ proxy r
_ Term (bv l)
_ = Maybe (Term (bv r))
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 = PartialRuleBinary (bv a) (bv b) (bv (a + b))
-> (Term (bv a) -> Term (bv b) -> Term (bv (a + b)))
-> Term (bv a)
-> Term (bv b)
-> Term (bv (a + b))
forall a b c.
(Typeable a, Typeable b, SupportedPrim c) =>
PartialRuleBinary a b c
-> TotalRuleBinary a b c -> TotalRuleBinary a b c
binaryUnfoldOnce PartialRuleBinary (bv a) (bv b) (bv (a + b))
forall (bv :: Nat -> *) (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 Term (bv a) -> Term (bv b) -> Term (bv (a + b))
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') = Term (bv (a + b)) -> Maybe (Term (bv (a + b)))
forall a. a -> Maybe a
Just (Term (bv (a + b)) -> Maybe (Term (bv (a + b))))
-> Term (bv (a + b)) -> Maybe (Term (bv (a + b)))
forall a b. (a -> b) -> a -> b
$ bv (a + b) -> Term (bv (a + b))
forall t.
(SupportedPrim t, Typeable t, Hashable t, Eq t, Show t) =>
t -> Term t
conTerm (bv (a + b) -> Term (bv (a + b)))
-> bv (a + b) -> Term (bv (a + b))
forall a b. (a -> b) -> a -> b
$ bv a -> bv b -> bv (a + b)
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 a
v bv b
v'
doPevalBVConcatTerm Term (bv a)
_ Term (bv b)
_ = Maybe (Term (bv (a + b)))
forall a. Maybe a
Nothing