{-# LANGUAGE DataKinds #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE PolyKinds #-}
{-# 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
  ( 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 n ix w proxy.
  ( SupportedPrim (bv n),
    SupportedPrim (bv w),
    KnownNat n,
    KnownNat ix,
    KnownNat w,
    1 <= n,
    1 <= w,
    ix + w <= n,
    SizedBV bv
  ) =>
  proxy ix ->
  proxy w ->
  Term (bv n) ->
  Term (bv w)
pevalBVSelectTerm :: forall (bv :: Nat -> *) (n :: Nat) (ix :: Nat) (w :: Nat)
       (proxy :: Nat -> *).
(SupportedPrim (bv n), SupportedPrim (bv w), KnownNat n,
 KnownNat ix, KnownNat w, 1 <= n, 1 <= w, (ix + w) <= n,
 SizedBV bv) =>
proxy ix -> proxy w -> Term (bv n) -> Term (bv w)
pevalBVSelectTerm proxy ix
ix proxy 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)
       (proxy :: Nat -> *).
(SupportedPrim (bv n), SupportedPrim (bv w), KnownNat n,
 KnownNat ix, KnownNat w, 1 <= n, 1 <= w, (ix + w) <= n,
 SizedBV bv) =>
proxy ix -> proxy w -> Term (bv n) -> Maybe (Term (bv w))
doPevalBVSelectTerm proxy ix
ix proxy w
w) (forall (bv :: Nat -> *) (n :: Nat) (ix :: Nat) (w :: Nat)
       (proxy :: Nat -> *).
(SupportedPrim (bv n), SupportedPrim (bv w), KnownNat n,
 KnownNat ix, KnownNat w, 1 <= n, 1 <= w, (ix + w) <= n,
 SizedBV bv) =>
proxy ix -> proxy w -> Term (bv n) -> Term (bv w)
bvselectTerm proxy ix
ix proxy w
w)

doPevalBVSelectTerm ::
  forall bv n ix w proxy.
  ( SupportedPrim (bv n),
    SupportedPrim (bv w),
    KnownNat n,
    KnownNat ix,
    KnownNat w,
    1 <= n,
    1 <= w,
    ix + w <= n,
    SizedBV bv
  ) =>
  proxy ix ->
  proxy w ->
  Term (bv n) ->
  Maybe (Term (bv w))
doPevalBVSelectTerm :: forall (bv :: Nat -> *) (n :: Nat) (ix :: Nat) (w :: Nat)
       (proxy :: Nat -> *).
(SupportedPrim (bv n), SupportedPrim (bv w), KnownNat n,
 KnownNat ix, KnownNat w, 1 <= n, 1 <= w, (ix + w) <= n,
 SizedBV bv) =>
proxy ix -> proxy w -> Term (bv n) -> Maybe (Term (bv w))
doPevalBVSelectTerm proxy ix
ix proxy 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)
       (proxy :: Nat -> *).
(SizedBV bv, KnownNat n, KnownNat ix, KnownNat w, 1 <= n, 1 <= w,
 (ix + w) <= n) =>
proxy ix -> proxy w -> bv n -> bv w
sizedBVSelect proxy ix
ix proxy w
w bv n
b
doPevalBVSelectTerm proxy ix
_ proxy w
_ Term (bv n)
_ = forall a. Maybe a
Nothing

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

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

pevalBVExtendTerm ::
  forall proxy l r bv.
  ( KnownNat l,
    KnownNat r,
    1 <= l,
    l <= r,
    SupportedPrim (bv l),
    SupportedPrim (bv r),
    SizedBV bv
  ) =>
  Bool ->
  proxy r ->
  Term (bv l) ->
  Term (bv r)
pevalBVExtendTerm :: forall (proxy :: Nat -> *) (l :: Nat) (r :: Nat) (bv :: Nat -> *).
(KnownNat l, KnownNat r, 1 <= l, l <= r, SupportedPrim (bv l),
 SupportedPrim (bv 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 -> *).
(KnownNat l, KnownNat r, 1 <= l, l <= r, SupportedPrim (bv l),
 SupportedPrim (bv 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 -> *).
(SupportedPrim (bv l), SupportedPrim (bv r), KnownNat l,
 KnownNat r, 1 <= l, 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.
  ( KnownNat l,
    KnownNat r,
    1 <= l,
    l <= r,
    SupportedPrim (bv l),
    SupportedPrim (bv r),
    SizedBV bv
  ) =>
  Bool ->
  proxy r ->
  Term (bv l) ->
  Maybe (Term (bv r))
doPevalBVExtendTerm :: forall (proxy :: Nat -> *) (l :: Nat) (r :: Nat) (bv :: Nat -> *).
(KnownNat l, KnownNat r, 1 <= l, l <= r, SupportedPrim (bv l),
 SupportedPrim (bv 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 ::
  ( SupportedPrim (bv a),
    SupportedPrim (bv b),
    SupportedPrim (bv (a + b)),
    KnownNat a,
    KnownNat b,
    1 <= a,
    1 <= b,
    SizedBV bv
  ) =>
  Term (bv a) ->
  Term (bv b) ->
  Term (bv (a + b))
pevalBVConcatTerm :: forall (bv :: Nat -> *) (a :: Nat) (b :: Nat).
(SupportedPrim (bv a), SupportedPrim (bv b),
 SupportedPrim (bv (a + b)), KnownNat a, KnownNat b, 1 <= a, 1 <= 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).
(SupportedPrim (bv a), SupportedPrim (bv b),
 SupportedPrim (bv (a + b)), KnownNat a, KnownNat b, 1 <= a, 1 <= b,
 SizedBV bv) =>
Term (bv a) -> Term (bv b) -> Maybe (Term (bv (a + b)))
doPevalBVConcatTerm forall (bv :: Nat -> *) (a :: Nat) (b :: Nat).
(SupportedPrim (bv a), SupportedPrim (bv b),
 SupportedPrim (bv (a + b)), KnownNat a, KnownNat b, 1 <= a, 1 <= b,
 SizedBV bv) =>
Term (bv a) -> Term (bv b) -> Term (bv (a + b))
bvconcatTerm

doPevalBVConcatTerm ::
  ( SupportedPrim (bv a),
    SupportedPrim (bv b),
    SupportedPrim (bv (a + b)),
    KnownNat a,
    KnownNat b,
    1 <= a,
    1 <= b,
    SizedBV bv
  ) =>
  Term (bv a) ->
  Term (bv b) ->
  Maybe (Term (bv (a + b)))
doPevalBVConcatTerm :: forall (bv :: Nat -> *) (a :: Nat) (b :: Nat).
(SupportedPrim (bv a), SupportedPrim (bv b),
 SupportedPrim (bv (a + b)), KnownNat a, KnownNat b, 1 <= a, 1 <= 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