{-# LANGUAGE DataKinds #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# 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
  ( pevalBVConcatTerm,
    pevalBVSelectTerm,
    pevalBVExtendTerm,
    pevalBVZeroExtendTerm,
    pevalBVSignExtendTerm,
  )
where

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.PartialEval.Unfold

-- select
pevalBVSelectTerm ::
  forall bv a ix w proxy.
  ( SupportedPrim (bv a),
    SupportedPrim (bv w),
    KnownNat a,
    KnownNat w,
    KnownNat ix,
    BVSelect (bv a) ix w (bv w)
  ) =>
  proxy ix ->
  proxy w ->
  Term (bv a) ->
  Term (bv w)
pevalBVSelectTerm :: forall (bv :: Nat -> *) (a :: Nat) (ix :: Nat) (w :: Nat)
       (proxy :: Nat -> *).
(SupportedPrim (bv a), SupportedPrim (bv w), KnownNat a,
 KnownNat w, KnownNat ix, BVSelect (bv a) ix w (bv w)) =>
proxy ix -> proxy w -> Term (bv a) -> Term (bv w)
pevalBVSelectTerm proxy ix
ix proxy w
w = PartialRuleUnary (bv a) (bv w)
-> TotalRuleUnary (bv a) (bv w) -> TotalRuleUnary (bv a) (bv w)
forall a b.
(Typeable a, SupportedPrim b) =>
PartialRuleUnary a b -> TotalRuleUnary a b -> TotalRuleUnary a b
unaryUnfoldOnce (proxy ix -> proxy w -> PartialRuleUnary (bv a) (bv w)
forall (bv :: Nat -> *) (a :: Nat) (ix :: Nat) (w :: Nat)
       (proxy :: Nat -> *).
(SupportedPrim (bv a), SupportedPrim (bv w), KnownNat a,
 KnownNat w, KnownNat ix, BVSelect (bv a) ix w (bv w)) =>
proxy ix -> proxy w -> Term (bv a) -> Maybe (Term (bv w))
doPevalBVSelectTerm proxy ix
ix proxy w
w) (proxy ix -> proxy w -> TotalRuleUnary (bv a) (bv w)
forall (bv :: Nat -> *) (a :: Nat) (ix :: Nat) (w :: Nat)
       (proxy :: Nat -> *).
(SupportedPrim (bv a), SupportedPrim (bv w), KnownNat a,
 KnownNat w, KnownNat ix, BVSelect (bv a) ix w (bv w)) =>
proxy ix -> proxy w -> Term (bv a) -> Term (bv w)
bvselectTerm proxy ix
ix proxy w
w)

doPevalBVSelectTerm ::
  forall bv a ix w proxy.
  ( SupportedPrim (bv a),
    SupportedPrim (bv w),
    KnownNat a,
    KnownNat w,
    KnownNat ix,
    BVSelect (bv a) ix w (bv w)
  ) =>
  proxy ix ->
  proxy w ->
  Term (bv a) ->
  Maybe (Term (bv w))
doPevalBVSelectTerm :: forall (bv :: Nat -> *) (a :: Nat) (ix :: Nat) (w :: Nat)
       (proxy :: Nat -> *).
(SupportedPrim (bv a), SupportedPrim (bv w), KnownNat a,
 KnownNat w, KnownNat ix, BVSelect (bv a) ix w (bv w)) =>
proxy ix -> proxy w -> Term (bv a) -> Maybe (Term (bv w))
doPevalBVSelectTerm proxy ix
ix proxy w
w (ConTerm Id
_ bv a
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
$ proxy ix -> proxy w -> bv a -> bv w
forall bv1 (ix :: Nat) (w :: Nat) bv2 (proxy :: Nat -> *).
BVSelect bv1 ix w bv2 =>
proxy ix -> proxy w -> bv1 -> bv2
bvselect proxy ix
ix proxy w
w bv a
b
doPevalBVSelectTerm proxy ix
_ proxy w
_ Term (bv a)
_ = Maybe (Term (bv w))
forall a. Maybe a
Nothing

-- ext
pevalBVZeroExtendTerm ::
  forall proxy a n b bv.
  ( KnownNat a,
    KnownNat b,
    KnownNat n,
    BVExtend (bv a) n (bv b),
    SupportedPrim (bv a),
    SupportedPrim (bv b)
  ) =>
  proxy n ->
  Term (bv a) ->
  Term (bv b)
pevalBVZeroExtendTerm :: forall (proxy :: Nat -> *) (a :: Nat) (n :: Nat) (b :: Nat)
       (bv :: Nat -> *).
(KnownNat a, KnownNat b, KnownNat n, BVExtend (bv a) n (bv b),
 SupportedPrim (bv a), SupportedPrim (bv b)) =>
proxy n -> Term (bv a) -> Term (bv b)
pevalBVZeroExtendTerm = Bool -> proxy n -> Term (bv a) -> Term (bv b)
forall (proxy :: Nat -> *) (a :: Nat) (n :: Nat) (b :: Nat)
       (bv :: Nat -> *).
(KnownNat a, KnownNat b, KnownNat n, BVExtend (bv a) n (bv b),
 SupportedPrim (bv a), SupportedPrim (bv b)) =>
Bool -> proxy n -> Term (bv a) -> Term (bv b)
pevalBVExtendTerm Bool
False

pevalBVSignExtendTerm ::
  forall proxy a n b bv.
  ( KnownNat a,
    KnownNat b,
    KnownNat n,
    BVExtend (bv a) n (bv b),
    SupportedPrim (bv a),
    SupportedPrim (bv b)
  ) =>
  proxy n ->
  Term (bv a) ->
  Term (bv b)
pevalBVSignExtendTerm :: forall (proxy :: Nat -> *) (a :: Nat) (n :: Nat) (b :: Nat)
       (bv :: Nat -> *).
(KnownNat a, KnownNat b, KnownNat n, BVExtend (bv a) n (bv b),
 SupportedPrim (bv a), SupportedPrim (bv b)) =>
proxy n -> Term (bv a) -> Term (bv b)
pevalBVSignExtendTerm = Bool -> proxy n -> Term (bv a) -> Term (bv b)
forall (proxy :: Nat -> *) (a :: Nat) (n :: Nat) (b :: Nat)
       (bv :: Nat -> *).
(KnownNat a, KnownNat b, KnownNat n, BVExtend (bv a) n (bv b),
 SupportedPrim (bv a), SupportedPrim (bv b)) =>
Bool -> proxy n -> Term (bv a) -> Term (bv b)
pevalBVExtendTerm Bool
True

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

doPevalBVExtendTerm ::
  forall proxy a n b bv.
  ( KnownNat a,
    KnownNat b,
    KnownNat n,
    BVExtend (bv a) n (bv b),
    SupportedPrim (bv a),
    SupportedPrim (bv b)
  ) =>
  Bool ->
  proxy n ->
  Term (bv a) ->
  Maybe (Term (bv b))
doPevalBVExtendTerm :: forall (proxy :: Nat -> *) (a :: Nat) (n :: Nat) (b :: Nat)
       (bv :: Nat -> *).
(KnownNat a, KnownNat b, KnownNat n, BVExtend (bv a) n (bv b),
 SupportedPrim (bv a), SupportedPrim (bv b)) =>
Bool -> proxy n -> Term (bv a) -> Maybe (Term (bv b))
doPevalBVExtendTerm Bool
signed proxy n
p (ConTerm Id
_ bv a
b) = Term (bv b) -> Maybe (Term (bv b))
forall a. a -> Maybe a
Just (Term (bv b) -> Maybe (Term (bv b)))
-> Term (bv b) -> Maybe (Term (bv b))
forall a b. (a -> b) -> a -> b
$ bv b -> Term (bv b)
forall t.
(SupportedPrim t, Typeable t, Hashable t, Eq t, Show t) =>
t -> Term t
conTerm (bv b -> Term (bv b)) -> bv b -> Term (bv b)
forall a b. (a -> b) -> a -> b
$ if Bool
signed then proxy n -> bv a -> bv b
forall bv1 (n :: Nat) bv2 (proxy :: Nat -> *).
BVExtend bv1 n bv2 =>
proxy n -> bv1 -> bv2
bvsignExtend proxy n
p bv a
b else proxy n -> bv a -> bv b
forall bv1 (n :: Nat) bv2 (proxy :: Nat -> *).
BVExtend bv1 n bv2 =>
proxy n -> bv1 -> bv2
bvzeroExtend proxy n
p bv a
b
doPevalBVExtendTerm Bool
_ proxy n
_ Term (bv a)
_ = Maybe (Term (bv b))
forall a. Maybe a
Nothing

pevalBVConcatTerm ::
  ( SupportedPrim (s w),
    SupportedPrim (s w'),
    SupportedPrim (s w''),
    KnownNat w,
    KnownNat w',
    KnownNat w'',
    BVConcat (s w) (s w') (s w'')
  ) =>
  Term (s w) ->
  Term (s w') ->
  Term (s w'')
pevalBVConcatTerm :: forall (s :: Nat -> *) (w :: Nat) (w' :: Nat) (w'' :: Nat).
(SupportedPrim (s w), SupportedPrim (s w'), SupportedPrim (s w''),
 KnownNat w, KnownNat w', KnownNat w'',
 BVConcat (s w) (s w') (s w'')) =>
Term (s w) -> Term (s w') -> Term (s w'')
pevalBVConcatTerm = PartialRuleBinary (s w) (s w') (s w'')
-> TotalRuleBinary (s w) (s w') (s w'')
-> TotalRuleBinary (s w) (s w') (s w'')
forall a b c.
(Typeable a, Typeable b, SupportedPrim c) =>
PartialRuleBinary a b c
-> TotalRuleBinary a b c -> TotalRuleBinary a b c
binaryUnfoldOnce PartialRuleBinary (s w) (s w') (s w'')
forall (s :: Nat -> *) (w :: Nat) (w' :: Nat) (w'' :: Nat).
(SupportedPrim (s w), SupportedPrim (s w'), SupportedPrim (s w''),
 KnownNat w, KnownNat w', KnownNat w'',
 BVConcat (s w) (s w') (s w'')) =>
Term (s w) -> Term (s w') -> Maybe (Term (s w''))
doPevalBVConcatTerm TotalRuleBinary (s w) (s w') (s w'')
forall (s :: Nat -> *) (w :: Nat) (w' :: Nat) (w'' :: Nat).
(SupportedPrim (s w), SupportedPrim (s w'), SupportedPrim (s w''),
 KnownNat w, KnownNat w', KnownNat w'',
 BVConcat (s w) (s w') (s w'')) =>
Term (s w) -> Term (s w') -> Term (s w'')
bvconcatTerm

doPevalBVConcatTerm ::
  ( SupportedPrim (s w),
    SupportedPrim (s w'),
    SupportedPrim (s w''),
    KnownNat w,
    KnownNat w',
    KnownNat w'',
    BVConcat (s w) (s w') (s w'')
  ) =>
  Term (s w) ->
  Term (s w') ->
  Maybe (Term (s w''))
doPevalBVConcatTerm :: forall (s :: Nat -> *) (w :: Nat) (w' :: Nat) (w'' :: Nat).
(SupportedPrim (s w), SupportedPrim (s w'), SupportedPrim (s w''),
 KnownNat w, KnownNat w', KnownNat w'',
 BVConcat (s w) (s w') (s w'')) =>
Term (s w) -> Term (s w') -> Maybe (Term (s w''))
doPevalBVConcatTerm (ConTerm Id
_ s w
v) (ConTerm Id
_ s w'
v') = Term (s w'') -> Maybe (Term (s w''))
forall a. a -> Maybe a
Just (Term (s w'') -> Maybe (Term (s w'')))
-> Term (s w'') -> Maybe (Term (s w''))
forall a b. (a -> b) -> a -> b
$ s w'' -> Term (s w'')
forall t.
(SupportedPrim t, Typeable t, Hashable t, Eq t, Show t) =>
t -> Term t
conTerm (s w'' -> Term (s w'')) -> s w'' -> Term (s w'')
forall a b. (a -> b) -> a -> b
$ s w -> s w' -> s w''
forall bv1 bv2 bv3. BVConcat bv1 bv2 bv3 => bv1 -> bv2 -> bv3
bvconcat s w
v s w'
v'
doPevalBVConcatTerm Term (s w)
_ Term (s w')
_ = Maybe (Term (s w''))
forall a. Maybe a
Nothing