{-|
This defines a data type `App` for representing operations that can be
applied to a range of values.  We call it an `App` because it
represents an application of an operation.  In mathematics, we would
probably call it a signature.
-}
{-# LANGUAGE AllowAmbiguousTypes #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE OverloadedStrings #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TemplateHaskell #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE TypeOperators #-}
module Data.Macaw.CFG.App
  ( -- * App
    App(..)
  , ppApp
  , ppAppA
    -- ** Rendering
  , AppRender(..)
  , AppRenderArg(..)
  , rendApp
    -- * Casting proof objects.
  , WidthEqProof(..)
  , widthEqProofEq
  , widthEqProofCompare
  , widthEqSource
  , widthEqTarget
  , widthEqSym
  ) where

import           Control.Monad.Identity
import qualified Data.Kind as Kind
import           Data.Parameterized.Classes
import qualified Data.Parameterized.List as P
import           Data.Parameterized.NatRepr
import           Data.Parameterized.TH.GADT
import Data.Parameterized.TraversableFC
    ( TraversableFC(..),
      FoldableFC(toListFC, foldMapFC, foldlFC'),
      FunctorFC(..),
      fmapFCDefault,
      foldMapFCDefault )
import           Data.Text (Text)
import qualified Data.Text as Text
import Numeric.Natural ( Natural )
import           Prettyprinter

import           Data.Macaw.Types
import           Data.Macaw.Utils.Pretty

-----------------------------------------------------------------------
-- App

-- | Data type to represent that two types use the same number of
-- bits, and thus can be bitcast.
--
-- Note. This datatype needs to balance several competing
-- requirements.  It needs to support all bitcasts needed by
-- architectures, represent bitcasts compactly, allow bitcasts to be
-- removed during optimization, and allow bitcasts to be symbolically
-- simulated.
--
-- Due to these requirements, we have a fairly limited set of proof
-- rules.  New rules can be added, but need to be balanced against the
-- above set of goals.  By design we do not have transitivity or
-- equality, as those can be obtained by respectively chaining
-- bitcasts or eliminating them.
data WidthEqProof (in_tp :: Type) (out_tp :: Type) where
  PackBits :: (1 <= n, 2 <= n, 1 <= w)
           => !(NatRepr n)
           -> !(NatRepr w)
           -> WidthEqProof (VecType n (BVType w)) (BVType (n * w))
  UnpackBits :: (1 <= n, 2 <= n, 1 <= w)
             => !(NatRepr n)
             -> !(NatRepr w)
             -> WidthEqProof (BVType (n * w)) (VecType n (BVType w))
  FromFloat :: !(FloatInfoRepr ftp)
            -> WidthEqProof (FloatType ftp) (BVType (FloatInfoBits ftp))
  ToFloat :: !(FloatInfoRepr ftp)
          -> WidthEqProof (BVType (FloatInfoBits ftp)) (FloatType ftp)

  -- | Convert between vector types that are equivalent.
  VecEqCongruence :: !(NatRepr n)
                  -> !(WidthEqProof i o)
                  -> WidthEqProof (VecType n i) (VecType n o)

  -- | Type is equal to itself.
  WidthEqRefl  :: !(TypeRepr tp) -> WidthEqProof tp tp

  -- | Allows transitivity composing proofs.
  WidthEqTrans :: !(WidthEqProof x y) -> !(WidthEqProof y z) -> WidthEqProof x z

-- | Apply symmetry to a width equality proof.
widthEqSym :: WidthEqProof x y -> WidthEqProof y x
widthEqSym :: forall (x :: Type) (y :: Type).
WidthEqProof x y -> WidthEqProof y x
widthEqSym (PackBits NatRepr n
n NatRepr w
w) = NatRepr n
-> NatRepr w
-> WidthEqProof ('BVType (n * w)) ('VecType n (BVType w))
forall (tp :: Natural) (tp :: Natural).
(1 <= tp, 2 <= tp, 1 <= tp) =>
NatRepr tp
-> NatRepr tp
-> WidthEqProof (BVType (tp * tp)) (VecType tp (BVType tp))
UnpackBits NatRepr n
n NatRepr w
w
widthEqSym (UnpackBits NatRepr n
n NatRepr w
w) = NatRepr n
-> NatRepr w
-> WidthEqProof ('VecType n (BVType w)) ('BVType (n * w))
forall (tp :: Natural) (tp :: Natural).
(1 <= tp, 2 <= tp, 1 <= tp) =>
NatRepr tp
-> NatRepr tp
-> WidthEqProof (VecType tp (BVType tp)) (BVType (tp * tp))
PackBits NatRepr n
n NatRepr w
w
widthEqSym (FromFloat FloatInfoRepr ftp
r) = FloatInfoRepr ftp
-> WidthEqProof ('BVType (FloatInfoBits ftp)) ('FloatType ftp)
forall (tp :: FloatInfo).
FloatInfoRepr tp
-> WidthEqProof (BVType (FloatInfoBits tp)) (FloatType tp)
ToFloat FloatInfoRepr ftp
r
widthEqSym (ToFloat FloatInfoRepr ftp
r) = FloatInfoRepr ftp
-> WidthEqProof ('FloatType ftp) ('BVType (FloatInfoBits ftp))
forall (tp :: FloatInfo).
FloatInfoRepr tp
-> WidthEqProof (FloatType tp) (BVType (FloatInfoBits tp))
FromFloat FloatInfoRepr ftp
r
widthEqSym (VecEqCongruence NatRepr n
n WidthEqProof i o
p) = NatRepr n
-> WidthEqProof o i -> WidthEqProof ('VecType n o) ('VecType n i)
forall (tp :: Natural) (tp :: Type) (o :: Type).
NatRepr tp
-> WidthEqProof tp o -> WidthEqProof (VecType tp tp) (VecType tp o)
VecEqCongruence NatRepr n
n (WidthEqProof i o -> WidthEqProof o i
forall (x :: Type) (y :: Type).
WidthEqProof x y -> WidthEqProof y x
widthEqSym WidthEqProof i o
p)
widthEqSym (WidthEqRefl TypeRepr x
tp) = TypeRepr y -> WidthEqProof y y
forall (tp :: Type). TypeRepr tp -> WidthEqProof tp tp
WidthEqRefl TypeRepr x
TypeRepr y
tp
widthEqSym (WidthEqTrans WidthEqProof x y
x WidthEqProof y y
y) = WidthEqProof y y -> WidthEqProof y x -> WidthEqProof y x
forall (x :: Type) (tp :: Type) (z :: Type).
WidthEqProof x tp -> WidthEqProof tp z -> WidthEqProof x z
WidthEqTrans (WidthEqProof y y -> WidthEqProof y y
forall (x :: Type) (y :: Type).
WidthEqProof x y -> WidthEqProof y x
widthEqSym WidthEqProof y y
y) (WidthEqProof x y -> WidthEqProof y x
forall (x :: Type) (y :: Type).
WidthEqProof x y -> WidthEqProof y x
widthEqSym WidthEqProof x y
x)

-- | Return the input type of the width equality proof
widthEqSource :: WidthEqProof i o -> TypeRepr i
widthEqSource :: forall (i :: Type) (o :: Type). WidthEqProof i o -> TypeRepr i
widthEqSource (PackBits NatRepr n
n NatRepr w
w) = NatRepr n
-> TypeRepr (BVType w) -> TypeRepr ('VecType n (BVType w))
forall (n :: Natural) (tp1 :: Type).
NatRepr n -> TypeRepr tp1 -> TypeRepr ('VecType n tp1)
VecTypeRepr NatRepr n
n (NatRepr w -> TypeRepr (BVType w)
forall (n :: Natural).
(1 <= n) =>
NatRepr n -> TypeRepr ('BVType n)
BVTypeRepr NatRepr w
w)
widthEqSource (UnpackBits NatRepr n
n NatRepr w
w) =
  case NatRepr n -> NatRepr w -> LeqProof 1 (n * w)
forall (p :: Natural -> Type) (q :: Natural -> Type) (x :: Natural)
       (y :: Natural).
(1 <= x, 1 <= y) =>
p x -> q y -> LeqProof 1 (x * y)
leqMulPos NatRepr n
n NatRepr w
w of
    LeqProof 1 (n * w)
LeqProof -> NatRepr (n * w) -> TypeRepr ('BVType (n * w))
forall (n :: Natural).
(1 <= n) =>
NatRepr n -> TypeRepr ('BVType n)
BVTypeRepr (NatRepr n -> NatRepr w -> NatRepr (n * w)
forall (n :: Natural) (m :: Natural).
NatRepr n -> NatRepr m -> NatRepr (n * m)
natMultiply NatRepr n
n NatRepr w
w)
widthEqSource (FromFloat FloatInfoRepr ftp
f) = FloatInfoRepr ftp -> TypeRepr ('FloatType ftp)
forall (fi :: FloatInfo).
FloatInfoRepr fi -> TypeRepr ('FloatType fi)
FloatTypeRepr FloatInfoRepr ftp
f
widthEqSource (ToFloat FloatInfoRepr ftp
f) =
  case FloatInfoRepr ftp -> LeqProof 1 (FloatInfoBits ftp)
forall (fi :: FloatInfo).
FloatInfoRepr fi -> LeqProof 1 (FloatInfoBits fi)
floatInfoBitsIsPos FloatInfoRepr ftp
f of
    LeqProof 1 (FloatInfoBits ftp)
LeqProof -> NatRepr (FloatInfoBits ftp)
-> TypeRepr ('BVType (FloatInfoBits ftp))
forall (n :: Natural).
(1 <= n) =>
NatRepr n -> TypeRepr ('BVType n)
BVTypeRepr (FloatInfoRepr ftp -> NatRepr (FloatInfoBits ftp)
forall (fi :: FloatInfo).
FloatInfoRepr fi -> NatRepr (FloatInfoBits fi)
floatInfoBits FloatInfoRepr ftp
f)
widthEqSource (VecEqCongruence NatRepr n
n WidthEqProof i o
r) = NatRepr n -> TypeRepr i -> TypeRepr ('VecType n i)
forall (n :: Natural) (tp1 :: Type).
NatRepr n -> TypeRepr tp1 -> TypeRepr ('VecType n tp1)
VecTypeRepr NatRepr n
n (WidthEqProof i o -> TypeRepr i
forall (i :: Type) (o :: Type). WidthEqProof i o -> TypeRepr i
widthEqSource WidthEqProof i o
r)
widthEqSource (WidthEqRefl TypeRepr i
x) = TypeRepr i
x
widthEqSource (WidthEqTrans WidthEqProof i y
x WidthEqProof y o
_) = WidthEqProof i y -> TypeRepr i
forall (i :: Type) (o :: Type). WidthEqProof i o -> TypeRepr i
widthEqSource WidthEqProof i y
x

-- | Return the result type of the width equality proof
widthEqTarget :: WidthEqProof i o -> TypeRepr o
widthEqTarget :: forall (i :: Type) (o :: Type). WidthEqProof i o -> TypeRepr o
widthEqTarget (PackBits NatRepr n
n NatRepr w
w) =
  case NatRepr n -> NatRepr w -> LeqProof 1 (n * w)
forall (p :: Natural -> Type) (q :: Natural -> Type) (x :: Natural)
       (y :: Natural).
(1 <= x, 1 <= y) =>
p x -> q y -> LeqProof 1 (x * y)
leqMulPos NatRepr n
n NatRepr w
w of
    LeqProof 1 (n * w)
LeqProof -> NatRepr (n * w) -> TypeRepr ('BVType (n * w))
forall (n :: Natural).
(1 <= n) =>
NatRepr n -> TypeRepr ('BVType n)
BVTypeRepr (NatRepr n -> NatRepr w -> NatRepr (n * w)
forall (n :: Natural) (m :: Natural).
NatRepr n -> NatRepr m -> NatRepr (n * m)
natMultiply NatRepr n
n NatRepr w
w)
widthEqTarget (UnpackBits NatRepr n
n NatRepr w
w) = NatRepr n
-> TypeRepr (BVType w) -> TypeRepr ('VecType n (BVType w))
forall (n :: Natural) (tp1 :: Type).
NatRepr n -> TypeRepr tp1 -> TypeRepr ('VecType n tp1)
VecTypeRepr NatRepr n
n (NatRepr w -> TypeRepr (BVType w)
forall (n :: Natural).
(1 <= n) =>
NatRepr n -> TypeRepr ('BVType n)
BVTypeRepr NatRepr w
w)
widthEqTarget (FromFloat FloatInfoRepr ftp
f) =
  case FloatInfoRepr ftp -> LeqProof 1 (FloatInfoBits ftp)
forall (fi :: FloatInfo).
FloatInfoRepr fi -> LeqProof 1 (FloatInfoBits fi)
floatInfoBitsIsPos FloatInfoRepr ftp
f of
    LeqProof 1 (FloatInfoBits ftp)
LeqProof -> NatRepr (FloatInfoBits ftp)
-> TypeRepr ('BVType (FloatInfoBits ftp))
forall (n :: Natural).
(1 <= n) =>
NatRepr n -> TypeRepr ('BVType n)
BVTypeRepr (FloatInfoRepr ftp -> NatRepr (FloatInfoBits ftp)
forall (fi :: FloatInfo).
FloatInfoRepr fi -> NatRepr (FloatInfoBits fi)
floatInfoBits FloatInfoRepr ftp
f)
widthEqTarget (ToFloat FloatInfoRepr ftp
f) = FloatInfoRepr ftp -> TypeRepr ('FloatType ftp)
forall (fi :: FloatInfo).
FloatInfoRepr fi -> TypeRepr ('FloatType fi)
FloatTypeRepr FloatInfoRepr ftp
f
widthEqTarget (VecEqCongruence NatRepr n
n WidthEqProof i o
r) = NatRepr n -> TypeRepr o -> TypeRepr ('VecType n o)
forall (n :: Natural) (tp1 :: Type).
NatRepr n -> TypeRepr tp1 -> TypeRepr ('VecType n tp1)
VecTypeRepr NatRepr n
n (WidthEqProof i o -> TypeRepr o
forall (i :: Type) (o :: Type). WidthEqProof i o -> TypeRepr o
widthEqTarget WidthEqProof i o
r)
widthEqTarget (WidthEqRefl TypeRepr i
x) = TypeRepr i
TypeRepr o
x
widthEqTarget (WidthEqTrans WidthEqProof i y
_ WidthEqProof y o
y) = WidthEqProof y o -> TypeRepr o
forall (i :: Type) (o :: Type). WidthEqProof i o -> TypeRepr o
widthEqTarget WidthEqProof y o
y

-- Force app to be in template-haskell context.
$(pure [])

-- | Compare two proofs, and return truei if the input/output types
-- are the same.
widthEqProofEq :: WidthEqProof xi xo
               -> WidthEqProof yi yo
               -> Maybe (WidthEqProof xi xo :~: WidthEqProof yi yo)
widthEqProofEq :: forall (xi :: Type) (xo :: Type) (yi :: Type) (yo :: Type).
WidthEqProof xi xo
-> WidthEqProof yi yo
-> Maybe (WidthEqProof xi xo :~: WidthEqProof yi yo)
widthEqProofEq WidthEqProof xi xo
p WidthEqProof yi yo
q = do
  xi :~: yi
Refl <- TypeRepr xi -> TypeRepr yi -> Maybe (xi :~: yi)
forall {k} (f :: k -> Type) (a :: k) (b :: k).
TestEquality f =>
f a -> f b -> Maybe (a :~: b)
forall (a :: Type) (b :: Type).
TypeRepr a -> TypeRepr b -> Maybe (a :~: b)
testEquality (WidthEqProof xi xo -> TypeRepr xi
forall (i :: Type) (o :: Type). WidthEqProof i o -> TypeRepr i
widthEqSource WidthEqProof xi xo
p) (WidthEqProof yi yo -> TypeRepr yi
forall (i :: Type) (o :: Type). WidthEqProof i o -> TypeRepr i
widthEqSource WidthEqProof yi yo
q)
  xo :~: yo
Refl <- TypeRepr xo -> TypeRepr yo -> Maybe (xo :~: yo)
forall {k} (f :: k -> Type) (a :: k) (b :: k).
TestEquality f =>
f a -> f b -> Maybe (a :~: b)
forall (a :: Type) (b :: Type).
TypeRepr a -> TypeRepr b -> Maybe (a :~: b)
testEquality (WidthEqProof xi xo -> TypeRepr xo
forall (i :: Type) (o :: Type). WidthEqProof i o -> TypeRepr o
widthEqTarget WidthEqProof xi xo
p) (WidthEqProof yi yo -> TypeRepr yo
forall (i :: Type) (o :: Type). WidthEqProof i o -> TypeRepr o
widthEqTarget WidthEqProof yi yo
q)
  (WidthEqProof xi xo :~: WidthEqProof yi yo)
-> Maybe (WidthEqProof xi xo :~: WidthEqProof yi yo)
forall a. a -> Maybe a
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure WidthEqProof xi xo :~: WidthEqProof xi xo
WidthEqProof xi xo :~: WidthEqProof yi yo
forall {k} (a :: k). a :~: a
Refl

-- | Compare proofs based on ordering of source and target.
widthEqProofCompare :: WidthEqProof xi xo
                    -> WidthEqProof yi yo
                    -> OrderingF (WidthEqProof xi xo) (WidthEqProof yi yo)
widthEqProofCompare :: forall (xi :: Type) (xo :: Type) (yi :: Type) (yo :: Type).
WidthEqProof xi xo
-> WidthEqProof yi yo
-> OrderingF (WidthEqProof xi xo) (WidthEqProof yi yo)
widthEqProofCompare WidthEqProof xi xo
p WidthEqProof yi yo
q =
  OrderingF xi yi
-> ((xi ~ yi) =>
    OrderingF (WidthEqProof xi xo) (WidthEqProof yi yo))
-> OrderingF (WidthEqProof xi xo) (WidthEqProof yi yo)
forall j k (a :: j) (b :: j) (c :: k) (d :: k).
OrderingF a b -> ((a ~ b) => OrderingF c d) -> OrderingF c d
joinOrderingF (TypeRepr xi -> TypeRepr yi -> OrderingF xi yi
forall k (ktp :: k -> Type) (x :: k) (y :: k).
OrdF ktp =>
ktp x -> ktp y -> OrderingF x y
forall (x :: Type) (y :: Type).
TypeRepr x -> TypeRepr y -> OrderingF x y
compareF (WidthEqProof xi xo -> TypeRepr xi
forall (i :: Type) (o :: Type). WidthEqProof i o -> TypeRepr i
widthEqSource WidthEqProof xi xo
p) (WidthEqProof yi yo -> TypeRepr yi
forall (i :: Type) (o :: Type). WidthEqProof i o -> TypeRepr i
widthEqSource WidthEqProof yi yo
q)) (((xi ~ yi) => OrderingF (WidthEqProof xi xo) (WidthEqProof yi yo))
 -> OrderingF (WidthEqProof xi xo) (WidthEqProof yi yo))
-> ((xi ~ yi) =>
    OrderingF (WidthEqProof xi xo) (WidthEqProof yi yo))
-> OrderingF (WidthEqProof xi xo) (WidthEqProof yi yo)
forall a b. (a -> b) -> a -> b
$
    OrderingF xo yo
-> ((xo ~ yo) =>
    OrderingF (WidthEqProof xi xo) (WidthEqProof yi yo))
-> OrderingF (WidthEqProof xi xo) (WidthEqProof yi yo)
forall j k (a :: j) (b :: j) (c :: k) (d :: k).
OrderingF a b -> ((a ~ b) => OrderingF c d) -> OrderingF c d
joinOrderingF (TypeRepr xo -> TypeRepr yo -> OrderingF xo yo
forall k (ktp :: k -> Type) (x :: k) (y :: k).
OrdF ktp =>
ktp x -> ktp y -> OrderingF x y
forall (x :: Type) (y :: Type).
TypeRepr x -> TypeRepr y -> OrderingF x y
compareF (WidthEqProof xi xo -> TypeRepr xo
forall (i :: Type) (o :: Type). WidthEqProof i o -> TypeRepr o
widthEqTarget WidthEqProof xi xo
p) (WidthEqProof yi yo -> TypeRepr yo
forall (i :: Type) (o :: Type). WidthEqProof i o -> TypeRepr o
widthEqTarget WidthEqProof yi yo
q))
      OrderingF (WidthEqProof xi xo) (WidthEqProof xi xo)
OrderingF (WidthEqProof xi xo) (WidthEqProof yi yo)
(xo ~ yo) => OrderingF (WidthEqProof xi xo) (WidthEqProof yi yo)
forall {k} (x :: k). OrderingF x x
EQF

-- | This datatype defines operations used on multiple architectures.
--
-- These operations are all total functions.  Different architecture tend to have
-- different ways of raising signals or exceptions, and so partial functions are
-- all architecture specific.
data App (f :: Type -> Kind.Type) (tp :: Type) where

  -- | Compare for equality.
  Eq :: !(f tp) -> !(f tp) -> App f BoolType

  Mux :: !(TypeRepr tp) -> !(f BoolType) -> !(f tp) -> !(f tp) -> App f tp

  ----------------------------------------------------------------------
  -- Boolean operations

  AndApp :: !(f BoolType) -> !(f BoolType) -> App f BoolType
  OrApp  :: !(f BoolType) -> !(f BoolType) -> App f BoolType
  NotApp :: !(f BoolType) -> App f BoolType
  XorApp  :: !(f BoolType) -> !(f BoolType) -> App f BoolType

  ----------------------------------------------------------------------
  -- Tuples

  -- | Create a tuple from a list of fields
  MkTuple :: !(P.List TypeRepr flds)
          -> !(P.List f flds)
          -> App f (TupleType flds)

  -- | Extract the value out of a tuple.
  TupleField :: !(P.List TypeRepr l) -> !(f (TupleType l)) -> !(P.Index l r) -> App f r

  ----------------------------------------------------------------------
  -- Vector

  -- | Extracts an element at given constant index from vector
  ExtractElement :: !(TypeRepr tp) -> !(f (VecType n tp)) -> !Int -> App f tp

  -- | Sets an element at given constant in vector.
  InsertElement :: !(TypeRepr (VecType n tp))
                -> !(f (VecType n tp)) -> !Int -> !(f tp) -> App f (VecType n tp)

  ----------------------------------------------------------------------
  -- Operations related to concatenating and extending bitvectors.

  -- | Given a @m@-bit bitvector and a natural number @n@ less than @m@, this returns
  -- the bitvector with the @n@ least significant bits.
  Trunc :: (1 <= n, n+1 <= m)
        => !(f (BVType m)) -> !(NatRepr n) -> App f (BVType n)

  -- | Given a @m@-bit bitvector @x@ and a natural number @n@ greater
  -- than @m@, this returns the bitvector with the same @m@ least
  -- signficant bits, and where the new bits are the same as the most
  -- significant bit in @x@.
  SExt :: (1 <= m, m+1 <= n, 1 <= n)
       => !(f (BVType m)) -> !(NatRepr n) -> App f (BVType n)
  -- | Given a @m@-bit bitvector @x@ and a natural number @n@ greater
  -- than @m@, this returns the bitvector with the same @m@ least
  -- signficant bits, and where the new bits are all @false@.
  UExt :: (1 <= m, m+1 <= n, 1 <= n)
       => !(f (BVType m))
       -> !(NatRepr n)
       -> App f (BVType n)

  -- | This casts an expression from one type to another that should
  -- use the same number of bytes in memory.
  Bitcast :: !(f tp) -> !(WidthEqProof tp out) -> App f out

  ----------------------------------------------------------------------
  -- Bitvector operations

  -- | @BVAdd w x y@ denotes @x + y@.
  BVAdd :: (1 <= n)
        => !(NatRepr n)
        -> !(f (BVType n))
        -> !(f (BVType n))
        -> App f (BVType n)

  -- | @BVAdc w x y c@ denotes @x + y + (c ? 1 : 0)@.
  BVAdc :: (1 <= n)
        => !(NatRepr n)
        -> !(f (BVType n))
        -> !(f (BVType n))
        -> !(f BoolType)
        -> App f (BVType n)

  -- | @BVSub w x y@ denotes @x - y@.
  BVSub :: (1 <= n)
        => !(NatRepr n)
        -> !(f (BVType n))
        -> !(f (BVType n))
        -> App f (BVType n)

  -- | @BVSbb w x y b@ denotes @(x - y) - (b ? 1 : 0)@.
  BVSbb :: (1 <= n)
        => !(NatRepr n)
        -> !(f (BVType n))
        -> !(f (BVType n))
        -> !(f BoolType)
        -> App f (BVType n)

  -- Multiply two numbers
  BVMul :: (1 <= n)
        => !(NatRepr n)
        -> !(f (BVType n))
        -> !(f (BVType n))
        -> App f (BVType n)

  -- Unsigned less than or equal.
  BVUnsignedLe :: (1 <= n) => !(f (BVType n)) -> !(f (BVType n)) -> App f BoolType

  -- Unsigned less than.
  BVUnsignedLt :: (1 <= n) => !(f (BVType n)) -> !(f (BVType n)) -> App f BoolType

  -- Signed less than or equal.
  BVSignedLe :: (1 <= n) => !(f (BVType n)) -> !(f (BVType n)) -> App f BoolType

  -- Signed less than
  BVSignedLt :: (1 <= n) => !(f (BVType n)) -> !(f (BVType n)) -> App f BoolType

  -- @BVTestBit x i@ returns true iff bit @i@ of @x@ is true.
  -- 0 is the index of the least-significant bit.
  --
  -- If the value is larger than the width of n, then the result is false.
  BVTestBit :: (1 <= n) => !(f (BVType n)) -> !(f (BVType n)) -> App f BoolType

  -- Bitwise complement
  BVComplement :: (1 <= n) => !(NatRepr n) -> !(f (BVType n)) -> App f (BVType n)
  -- Bitwise and
  BVAnd :: (1 <= n) => !(NatRepr n) -> !(f (BVType n)) -> !(f (BVType n)) -> App f (BVType n)
  -- Bitwise or
  BVOr  :: (1 <= n) => !(NatRepr n) -> !(f (BVType n)) -> !(f (BVType n)) -> App f (BVType n)
  -- Exclusive or
  BVXor :: (1 <= n) => !(NatRepr n) -> !(f (BVType n)) -> !(f (BVType n)) -> App f (BVType n)

  -- | Left shift (e.g. `BVShl x y` denotes `fromUnsigned (toUnsigned x * 2 ^ toUnsigned y)`
  BVShl :: (1 <= n) => !(NatRepr n) -> !(f (BVType n)) -> !(f (BVType n)) -> App f (BVType n)
  -- | Unsigned right shift (e.g. `BVShr x y` denotes `fromUnsigned (toUnsigned x / 2 ^ toUnsigned y)`
  BVShr :: (1 <= n) => !(NatRepr n) -> !(f (BVType n)) -> !(f (BVType n)) -> App f (BVType n)
  -- | Arithmetic right shift (e.g. `BVSar x y` denotes `fromUnsigned (toSigned x / 2 ^ toUnsigned y)`
  BVSar :: (1 <= n) => !(NatRepr n) -> !(f (BVType n)) -> !(f (BVType n)) -> App f (BVType n)

  -- | Add two values and a carry bit to determine if they have an
  -- unsigned overflow.
  --
  -- This is the sum of three three values cannot be represented as an
  -- unsigned number.
  UadcOverflows :: (1 <= n)
                => !(f (BVType n))
                -> !(f (BVType n))
                -> !(f BoolType)
                -> App f BoolType

  -- | Add two values and a carry bit to determine if they have a
  -- signed overflow.
  --
  -- @SadcOverflows  w x y c@ should be true iff the result
  -- @toNat x + toNat y + (c ? 1 : 0)@ is greater than @2^w-1@.
  SadcOverflows :: (1 <= n)
                => !(f (BVType n))
                -> !(f (BVType n))
                -> !(f BoolType)
                -> App f BoolType

  -- | Unsigned subtract with borrow overflow
  --
  -- @UsbbOverflows w x y c@ should be true iff the result
  -- @(toNat x - toNat y) - (c ? 1 : 0)@ is non-negative.
  -- Since everything is
  -- unsigned, this is equivalent to @x unsignedLt (y + (c ? 1 : 0)@.
  UsbbOverflows :: (1 <= n)
                => !(f (BVType n))
                -> !(f (BVType n))
                -> !(f BoolType)
                -> App f BoolType

  -- | Signed subtract with borrow overflow.
  --
  -- @SsbbOverflows w x y c@ should be true iff the result
  -- @(toInt x - toInt y) - (c ? 1 : 0)@ is not between @-2^(w-1)@ and @2^(w-1)-1@.
  -- An equivalent way to express this is that x and y should have opposite signs and
  -- the sign of the result should differ from the sign of x.
  SsbbOverflows :: (1 <= n)
                => !(f (BVType n))
                -> !(f (BVType n))
                -> !(f BoolType)
                -> App f BoolType

  -- | This returns the number of true bits in the input.
  PopCount :: (1 <= n) => !(NatRepr n) -> !(f (BVType n)) -> App f (BVType n)

  -- | Reverse the bytes in a bitvector expression.
  ReverseBytes :: (1 <= n) => !(NatRepr n) -> !(f (BVType (8*n))) -> App f (BVType (8*n))

  -- | bsf "bit scan forward" returns the index of the
  -- least-significant bit that is 1.  An equivalent way of stating
  -- this is that it returns the number zero-bits starting from the
  -- least significant bit.  This returns n if the value is zero.
  Bsf :: (1 <= n) => !(NatRepr n) -> !(f (BVType n)) -> App f (BVType n)

  -- | bsr "bit scan reverse" returns the index of the
  -- most-significant bit that is 1.  An equivalent way of stating
  -- this is that it returns the number zero-bits starting from
  -- the most-significant bit location.  This returns n if the
  -- value is zero.
  Bsr :: (1 <= n) => !(NatRepr n) -> !(f (BVType n)) -> App f (BVType n)

-----------------------------------------------------------------------
-- App utilities

-- Force app to be in template-haskell context.
$(pure [])

instance TestEquality f => Eq (App f tp) where
  App f tp
x == :: App f tp -> App f tp -> Bool
== App f tp
y = Maybe (tp :~: tp) -> Bool
forall a. Maybe a -> Bool
isJust (App f tp -> App f tp -> Maybe (tp :~: tp)
forall {k} (f :: k -> Type) (a :: k) (b :: k).
TestEquality f =>
f a -> f b -> Maybe (a :~: b)
forall (a :: Type) (b :: Type).
App f a -> App f b -> Maybe (a :~: b)
testEquality App f tp
x App f tp
y)

instance TestEquality f => TestEquality (App f) where
  testEquality :: forall (a :: Type) (b :: Type).
App f a -> App f b -> Maybe (a :~: b)
testEquality = $(structuralTypeEquality [t|App|]
                   [ (DataArg 0                  `TypeApp` AnyType, [|testEquality|])
                   , (ConType [t|NatRepr|]       `TypeApp` AnyType, [|testEquality|])
                   , (ConType [t|FloatInfoRepr|] `TypeApp` AnyType, [|testEquality|])
                   , (ConType [t|TypeRepr|]      `TypeApp` AnyType, [|testEquality|])
                   , (ConType [t|P.List|] `TypeApp` AnyType `TypeApp` AnyType,
                      [|testEquality|])
                   , (ConType [t|P.Index|] `TypeApp` AnyType `TypeApp` AnyType,
                      [|testEquality|])
                   , (ConType [t|WidthEqProof|] `TypeApp` AnyType `TypeApp` AnyType,
                      [|widthEqProofEq|])
                   ]
                  )

instance (HashableF f, TestEquality f) => Hashable (App f tp) where
  hashWithSalt :: Int -> App f tp -> Int
hashWithSalt = $(structuralHashWithSalt [t|App|]
                     [ (DataArg 0 `TypeApp` AnyType, [|hashWithSaltF|])
                     , (ConType [t|TypeRepr|] `TypeApp` AnyType, [|\s _c -> s|])
                     , (ConType [t|P.List|] `TypeApp` ConType [t|TypeRepr|] `TypeApp` AnyType
                       , [|\s _c -> s|])
                     , (ConType [t|P.List|] `TypeApp` DataArg 0 `TypeApp` AnyType
                       , [|foldlFC' hashWithSaltF|])
                     , (ConType [t|WidthEqProof|] `TypeApp` AnyType `TypeApp` AnyType
                       , [|\s _c -> s|])
                     ]
                  )

instance (HashableF f, TestEquality f) => HashableF (App f) where
  hashWithSaltF :: forall (tp :: Type). Int -> App f tp -> Int
hashWithSaltF = Int -> App f tp -> Int
forall a. Hashable a => Int -> a -> Int
hashWithSalt

instance OrdF f => OrdF (App f) where
  compareF :: forall (x :: Type) (y :: Type). App f x -> App f y -> OrderingF x y
compareF = $(structuralTypeOrd [t|App|]
                   [ (DataArg 0                  `TypeApp` AnyType, [|compareF|])
                   , (ConType [t|NatRepr|]       `TypeApp` AnyType, [|compareF|])
                   , (ConType [t|FloatInfoRepr|] `TypeApp` AnyType, [|compareF|])
                   , (ConType [t|TypeRepr|]      `TypeApp` AnyType, [|compareF|])
                   , (ConType [t|P.List|] `TypeApp` ConType [t|TypeRepr|] `TypeApp` AnyType,
                      [|compareF|])
                  , (ConType [t|P.List|] `TypeApp` DataArg 0 `TypeApp` AnyType,
                      [|compareF|])
                   , (ConType [t|P.Index|] `TypeApp` AnyType `TypeApp` AnyType,
                      [|compareF|])
                   , (ConType [t|WidthEqProof|] `TypeApp` AnyType `TypeApp` AnyType,
                      [|widthEqProofCompare|])
                   ]
              )

instance OrdF f => Ord (App f tp) where
  compare :: App f tp -> App f tp -> Ordering
compare App f tp
a App f tp
b =
    case App f tp -> App f tp -> OrderingF tp tp
forall k (ktp :: k -> Type) (x :: k) (y :: k).
OrdF ktp =>
ktp x -> ktp y -> OrderingF x y
forall (x :: Type) (y :: Type). App f x -> App f y -> OrderingF x y
compareF App f tp
a App f tp
b of
      OrderingF tp tp
LTF -> Ordering
LT
      OrderingF tp tp
EQF -> Ordering
EQ
      OrderingF tp tp
GTF -> Ordering
GT

instance FunctorFC App where
  fmapFC :: forall (f :: Type -> Type) (g :: Type -> Type).
(forall (x :: Type). f x -> g x)
-> forall (x :: Type). App f x -> App g x
fmapFC = (forall (x :: Type). f x -> g x) -> App f x -> App g x
(forall (x :: Type). f x -> g x)
-> forall (x :: Type). App f x -> App g x
forall {k} {l} (t :: (k -> Type) -> l -> Type) (f :: k -> Type)
       (g :: k -> Type).
TraversableFC t =>
(forall (x :: k). f x -> g x) -> forall (x :: l). t f x -> t g x
forall (f :: Type -> Type) (g :: Type -> Type).
(forall (x :: Type). f x -> g x)
-> forall (x :: Type). App f x -> App g x
fmapFCDefault

instance FoldableFC App where
  foldMapFC :: forall (f :: Type -> Type) m.
Monoid m =>
(forall (x :: Type). f x -> m) -> forall (x :: Type). App f x -> m
foldMapFC = (forall (x :: Type). f x -> m) -> App f x -> m
(forall (x :: Type). f x -> m) -> forall (x :: Type). App f x -> m
forall {k} {l} (t :: (k -> Type) -> l -> Type) m (f :: k -> Type).
(TraversableFC t, Monoid m) =>
(forall (x :: k). f x -> m) -> forall (x :: l). t f x -> m
foldMapFCDefault

instance TraversableFC App where
  traverseFC :: forall (f :: Type -> Type) (g :: Type -> Type) (m :: Type -> Type).
Applicative m =>
(forall (x :: Type). f x -> m (g x))
-> forall (x :: Type). App f x -> m (App g x)
traverseFC =
    $(structuralTraversal [t|App|]
      [ (ConType [t|P.List|] `TypeApp` DataArg 0 `TypeApp` AnyType
        , [|traverseFC|]
        )
      ])

------------------------------------------------------------------------
-- App pretty printing

data AppRenderArg (f :: Type -> Kind.Type) where
  Val :: f tp -> AppRenderArg f
  -- Type argument (for bitcast)
  Type :: !(TypeRepr tp) -> AppRenderArg f
  -- Index into vector or tuple (must be valid for type)
  Index :: Natural -> AppRenderArg f
  -- Width argument passed to extension (must be positive)
  Width :: Natural -> AppRenderArg f

data AppRender (f :: Type -> Kind.Type) = AppRender Text [AppRenderArg f]

-- | Pretty print an 'App' as an expression using the given function
-- for printing arguments.
rendApp :: App f tp -> AppRender f
rendApp :: forall (f :: Type -> Type) (tp :: Type). App f tp -> AppRender f
rendApp App f tp
a0 = do
  let app :: Text -> [AppRenderArg f] -> AppRender f
app = Text -> [AppRenderArg f] -> AppRender f
forall (f :: Type -> Type). Text -> [AppRenderArg f] -> AppRender f
AppRender
  case App f tp
a0 of
    Eq f tp
x f tp
y       -> Text -> [AppRenderArg f] -> AppRender f
forall (f :: Type -> Type). Text -> [AppRenderArg f] -> AppRender f
app Text
"eq" [ f tp -> AppRenderArg f
forall (f :: Type -> Type) (tp :: Type). f tp -> AppRenderArg f
Val f tp
x, f tp -> AppRenderArg f
forall (f :: Type -> Type) (tp :: Type). f tp -> AppRenderArg f
Val f tp
y ]
    Mux   TypeRepr tp
_ f BoolType
c f tp
x f tp
y -> Text -> [AppRenderArg f] -> AppRender f
forall (f :: Type -> Type). Text -> [AppRenderArg f] -> AppRender f
app Text
"mux" [ f BoolType -> AppRenderArg f
forall (f :: Type -> Type) (tp :: Type). f tp -> AppRenderArg f
Val f BoolType
c, f tp -> AppRenderArg f
forall (f :: Type -> Type) (tp :: Type). f tp -> AppRenderArg f
Val f tp
x, f tp -> AppRenderArg f
forall (f :: Type -> Type) (tp :: Type). f tp -> AppRenderArg f
Val f tp
y ]
    AndApp f BoolType
x f BoolType
y -> Text -> [AppRenderArg f] -> AppRender f
forall (f :: Type -> Type). Text -> [AppRenderArg f] -> AppRender f
app Text
"and" [ f BoolType -> AppRenderArg f
forall (f :: Type -> Type) (tp :: Type). f tp -> AppRenderArg f
Val f BoolType
x, f BoolType -> AppRenderArg f
forall (f :: Type -> Type) (tp :: Type). f tp -> AppRenderArg f
Val f BoolType
y ]
    OrApp  f BoolType
x f BoolType
y -> Text -> [AppRenderArg f] -> AppRender f
forall (f :: Type -> Type). Text -> [AppRenderArg f] -> AppRender f
app Text
"or"  [ f BoolType -> AppRenderArg f
forall (f :: Type -> Type) (tp :: Type). f tp -> AppRenderArg f
Val f BoolType
x, f BoolType -> AppRenderArg f
forall (f :: Type -> Type) (tp :: Type). f tp -> AppRenderArg f
Val f BoolType
y ]
    NotApp f BoolType
x   -> Text -> [AppRenderArg f] -> AppRender f
forall (f :: Type -> Type). Text -> [AppRenderArg f] -> AppRender f
app Text
"not" [ f BoolType -> AppRenderArg f
forall (f :: Type -> Type) (tp :: Type). f tp -> AppRenderArg f
Val f BoolType
x ]
    XorApp  f BoolType
x f BoolType
y -> Text -> [AppRenderArg f] -> AppRender f
forall (f :: Type -> Type). Text -> [AppRenderArg f] -> AppRender f
app Text
"xor"  [ f BoolType -> AppRenderArg f
forall (f :: Type -> Type) (tp :: Type). f tp -> AppRenderArg f
Val f BoolType
x, f BoolType -> AppRenderArg f
forall (f :: Type -> Type) (tp :: Type). f tp -> AppRenderArg f
Val f BoolType
y ]
    MkTuple List TypeRepr flds
_ List f flds
flds -> Text -> [AppRenderArg f] -> AppRender f
forall (f :: Type -> Type). Text -> [AppRenderArg f] -> AppRender f
app Text
"tuple" ((forall (x :: Type). f x -> AppRenderArg f)
-> forall (x :: [Type]). List f x -> [AppRenderArg f]
forall k l (t :: (k -> Type) -> l -> Type) (f :: k -> Type) a.
FoldableFC t =>
(forall (x :: k). f x -> a) -> forall (x :: l). t f x -> [a]
forall (f :: Type -> Type) a.
(forall (x :: Type). f x -> a)
-> forall (x :: [Type]). List f x -> [a]
toListFC f x -> AppRenderArg f
forall (x :: Type). f x -> AppRenderArg f
forall (f :: Type -> Type) (tp :: Type). f tp -> AppRenderArg f
Val List f flds
flds)
    TupleField List TypeRepr l
_ f (TupleType l)
x Index l tp
i -> Text -> [AppRenderArg f] -> AppRender f
forall (f :: Type -> Type). Text -> [AppRenderArg f] -> AppRender f
app Text
"tuple_field" [ f (TupleType l) -> AppRenderArg f
forall (f :: Type -> Type) (tp :: Type). f tp -> AppRenderArg f
Val f (TupleType l)
x, Natural -> AppRenderArg f
forall (f :: Type -> Type). Natural -> AppRenderArg f
Index (Integer -> Natural
forall a. Num a => Integer -> a
fromInteger (Index l tp -> Integer
forall {k} (l :: [k]) (tp :: k). Index l tp -> Integer
P.indexValue Index l tp
i)) ]
    ExtractElement TypeRepr tp
_ f (VecType n tp)
v Int
i -> Text -> [AppRenderArg f] -> AppRender f
forall (f :: Type -> Type). Text -> [AppRenderArg f] -> AppRender f
app Text
"extract_element" [ f (VecType n tp) -> AppRenderArg f
forall (f :: Type -> Type) (tp :: Type). f tp -> AppRenderArg f
Val f (VecType n tp)
v, Natural -> AppRenderArg f
forall (f :: Type -> Type). Natural -> AppRenderArg f
Index (Int -> Natural
forall a b. (Integral a, Num b) => a -> b
fromIntegral Int
i) ]
    InsertElement TypeRepr ('VecType n tp)
_ f ('VecType n tp)
s Int
i f tp
v -> Text -> [AppRenderArg f] -> AppRender f
forall (f :: Type -> Type). Text -> [AppRenderArg f] -> AppRender f
app Text
"insert_element" [ f ('VecType n tp) -> AppRenderArg f
forall (f :: Type -> Type) (tp :: Type). f tp -> AppRenderArg f
Val f ('VecType n tp)
s, Natural -> AppRenderArg f
forall (f :: Type -> Type). Natural -> AppRenderArg f
Index (Int -> Natural
forall a b. (Integral a, Num b) => a -> b
fromIntegral Int
i), f tp -> AppRenderArg f
forall (f :: Type -> Type) (tp :: Type). f tp -> AppRenderArg f
Val f tp
v ]
    Trunc f (BVType m)
x NatRepr n
w -> Text -> [AppRenderArg f] -> AppRender f
forall (f :: Type -> Type). Text -> [AppRenderArg f] -> AppRender f
app Text
"trunc" [ f (BVType m) -> AppRenderArg f
forall (f :: Type -> Type) (tp :: Type). f tp -> AppRenderArg f
Val f (BVType m)
x, Natural -> AppRenderArg f
forall (f :: Type -> Type). Natural -> AppRenderArg f
Width (NatRepr n -> Natural
forall (n :: Natural). NatRepr n -> Natural
natValue NatRepr n
w) ]
    SExt f (BVType m)
x NatRepr n
w -> Text -> [AppRenderArg f] -> AppRender f
forall (f :: Type -> Type). Text -> [AppRenderArg f] -> AppRender f
app Text
"sext" [ f (BVType m) -> AppRenderArg f
forall (f :: Type -> Type) (tp :: Type). f tp -> AppRenderArg f
Val f (BVType m)
x, Natural -> AppRenderArg f
forall (f :: Type -> Type). Natural -> AppRenderArg f
Width (NatRepr n -> Natural
forall (n :: Natural). NatRepr n -> Natural
natValue NatRepr n
w) ]
    UExt f (BVType m)
x NatRepr n
w -> Text -> [AppRenderArg f] -> AppRender f
forall (f :: Type -> Type). Text -> [AppRenderArg f] -> AppRender f
app Text
"uext" [ f (BVType m) -> AppRenderArg f
forall (f :: Type -> Type) (tp :: Type). f tp -> AppRenderArg f
Val f (BVType m)
x, Natural -> AppRenderArg f
forall (f :: Type -> Type). Natural -> AppRenderArg f
Width (NatRepr n -> Natural
forall (n :: Natural). NatRepr n -> Natural
natValue NatRepr n
w) ]
    Bitcast f tp
x WidthEqProof tp tp
tp -> Text -> [AppRenderArg f] -> AppRender f
forall (f :: Type -> Type). Text -> [AppRenderArg f] -> AppRender f
app Text
"bitcast" [ f tp -> AppRenderArg f
forall (f :: Type -> Type) (tp :: Type). f tp -> AppRenderArg f
Val f tp
x, TypeRepr tp -> AppRenderArg f
forall (tp :: Type) (f :: Type -> Type).
TypeRepr tp -> AppRenderArg f
Type (WidthEqProof tp tp -> TypeRepr tp
forall (i :: Type) (o :: Type). WidthEqProof i o -> TypeRepr o
widthEqTarget WidthEqProof tp tp
tp) ]
    BVAdd NatRepr n
_ f ('BVType n)
x f ('BVType n)
y   -> Text -> [AppRenderArg f] -> AppRender f
forall (f :: Type -> Type). Text -> [AppRenderArg f] -> AppRender f
app Text
"bv_add" [ f ('BVType n) -> AppRenderArg f
forall (f :: Type -> Type) (tp :: Type). f tp -> AppRenderArg f
Val f ('BVType n)
x, f ('BVType n) -> AppRenderArg f
forall (f :: Type -> Type) (tp :: Type). f tp -> AppRenderArg f
Val f ('BVType n)
y ]
    BVAdc NatRepr n
_ f ('BVType n)
x f ('BVType n)
y f BoolType
c -> Text -> [AppRenderArg f] -> AppRender f
forall (f :: Type -> Type). Text -> [AppRenderArg f] -> AppRender f
app Text
"bv_adc" [ f ('BVType n) -> AppRenderArg f
forall (f :: Type -> Type) (tp :: Type). f tp -> AppRenderArg f
Val f ('BVType n)
x, f ('BVType n) -> AppRenderArg f
forall (f :: Type -> Type) (tp :: Type). f tp -> AppRenderArg f
Val f ('BVType n)
y, f BoolType -> AppRenderArg f
forall (f :: Type -> Type) (tp :: Type). f tp -> AppRenderArg f
Val f BoolType
c ]
    BVSub NatRepr n
_ f ('BVType n)
x f ('BVType n)
y -> Text -> [AppRenderArg f] -> AppRender f
forall (f :: Type -> Type). Text -> [AppRenderArg f] -> AppRender f
app Text
"bv_sub" [ f ('BVType n) -> AppRenderArg f
forall (f :: Type -> Type) (tp :: Type). f tp -> AppRenderArg f
Val f ('BVType n)
x, f ('BVType n) -> AppRenderArg f
forall (f :: Type -> Type) (tp :: Type). f tp -> AppRenderArg f
Val f ('BVType n)
y ]
    BVSbb NatRepr n
_ f ('BVType n)
x f ('BVType n)
y f BoolType
b -> Text -> [AppRenderArg f] -> AppRender f
forall (f :: Type -> Type). Text -> [AppRenderArg f] -> AppRender f
app Text
"bv_sbb" [ f ('BVType n) -> AppRenderArg f
forall (f :: Type -> Type) (tp :: Type). f tp -> AppRenderArg f
Val f ('BVType n)
x, f ('BVType n) -> AppRenderArg f
forall (f :: Type -> Type) (tp :: Type). f tp -> AppRenderArg f
Val f ('BVType n)
y, f BoolType -> AppRenderArg f
forall (f :: Type -> Type) (tp :: Type). f tp -> AppRenderArg f
Val f BoolType
b ]
    BVMul NatRepr n
_ f ('BVType n)
x f ('BVType n)
y -> Text -> [AppRenderArg f] -> AppRender f
forall (f :: Type -> Type). Text -> [AppRenderArg f] -> AppRender f
app Text
"bv_mul" [ f ('BVType n) -> AppRenderArg f
forall (f :: Type -> Type) (tp :: Type). f tp -> AppRenderArg f
Val f ('BVType n)
x, f ('BVType n) -> AppRenderArg f
forall (f :: Type -> Type) (tp :: Type). f tp -> AppRenderArg f
Val f ('BVType n)
y ]
    BVUnsignedLt f (BVType n)
x f (BVType n)
y  -> Text -> [AppRenderArg f] -> AppRender f
forall (f :: Type -> Type). Text -> [AppRenderArg f] -> AppRender f
app Text
"bv_ult"  [ f (BVType n) -> AppRenderArg f
forall (f :: Type -> Type) (tp :: Type). f tp -> AppRenderArg f
Val f (BVType n)
x, f (BVType n) -> AppRenderArg f
forall (f :: Type -> Type) (tp :: Type). f tp -> AppRenderArg f
Val f (BVType n)
y ]
    BVUnsignedLe f (BVType n)
x f (BVType n)
y  -> Text -> [AppRenderArg f] -> AppRender f
forall (f :: Type -> Type). Text -> [AppRenderArg f] -> AppRender f
app Text
"bv_ule"  [ f (BVType n) -> AppRenderArg f
forall (f :: Type -> Type) (tp :: Type). f tp -> AppRenderArg f
Val f (BVType n)
x, f (BVType n) -> AppRenderArg f
forall (f :: Type -> Type) (tp :: Type). f tp -> AppRenderArg f
Val f (BVType n)
y ]
    BVSignedLt f (BVType n)
x f (BVType n)
y    -> Text -> [AppRenderArg f] -> AppRender f
forall (f :: Type -> Type). Text -> [AppRenderArg f] -> AppRender f
app Text
"bv_slt"  [ f (BVType n) -> AppRenderArg f
forall (f :: Type -> Type) (tp :: Type). f tp -> AppRenderArg f
Val f (BVType n)
x, f (BVType n) -> AppRenderArg f
forall (f :: Type -> Type) (tp :: Type). f tp -> AppRenderArg f
Val f (BVType n)
y ]
    BVSignedLe f (BVType n)
x f (BVType n)
y    -> Text -> [AppRenderArg f] -> AppRender f
forall (f :: Type -> Type). Text -> [AppRenderArg f] -> AppRender f
app Text
"bv_sle"  [ f (BVType n) -> AppRenderArg f
forall (f :: Type -> Type) (tp :: Type). f tp -> AppRenderArg f
Val f (BVType n)
x, f (BVType n) -> AppRenderArg f
forall (f :: Type -> Type) (tp :: Type). f tp -> AppRenderArg f
Val f (BVType n)
y ]
    BVTestBit f (BVType n)
x f (BVType n)
i -> Text -> [AppRenderArg f] -> AppRender f
forall (f :: Type -> Type). Text -> [AppRenderArg f] -> AppRender f
app Text
"bv_testbit" [ f (BVType n) -> AppRenderArg f
forall (f :: Type -> Type) (tp :: Type). f tp -> AppRenderArg f
Val f (BVType n)
x, f (BVType n) -> AppRenderArg f
forall (f :: Type -> Type) (tp :: Type). f tp -> AppRenderArg f
Val f (BVType n)
i]
    BVComplement NatRepr n
_ f ('BVType n)
x -> Text -> [AppRenderArg f] -> AppRender f
forall (f :: Type -> Type). Text -> [AppRenderArg f] -> AppRender f
app Text
"bv_complement" [ f ('BVType n) -> AppRenderArg f
forall (f :: Type -> Type) (tp :: Type). f tp -> AppRenderArg f
Val f ('BVType n)
x ]
    BVAnd NatRepr n
_ f ('BVType n)
x f ('BVType n)
y -> Text -> [AppRenderArg f] -> AppRender f
forall (f :: Type -> Type). Text -> [AppRenderArg f] -> AppRender f
app Text
"bv_and" [ f ('BVType n) -> AppRenderArg f
forall (f :: Type -> Type) (tp :: Type). f tp -> AppRenderArg f
Val f ('BVType n)
x, f ('BVType n) -> AppRenderArg f
forall (f :: Type -> Type) (tp :: Type). f tp -> AppRenderArg f
Val f ('BVType n)
y ]
    BVOr  NatRepr n
_ f ('BVType n)
x f ('BVType n)
y -> Text -> [AppRenderArg f] -> AppRender f
forall (f :: Type -> Type). Text -> [AppRenderArg f] -> AppRender f
app Text
"bv_or"  [ f ('BVType n) -> AppRenderArg f
forall (f :: Type -> Type) (tp :: Type). f tp -> AppRenderArg f
Val f ('BVType n)
x, f ('BVType n) -> AppRenderArg f
forall (f :: Type -> Type) (tp :: Type). f tp -> AppRenderArg f
Val f ('BVType n)
y ]
    BVXor NatRepr n
_ f ('BVType n)
x f ('BVType n)
y -> Text -> [AppRenderArg f] -> AppRender f
forall (f :: Type -> Type). Text -> [AppRenderArg f] -> AppRender f
app Text
"bv_xor" [ f ('BVType n) -> AppRenderArg f
forall (f :: Type -> Type) (tp :: Type). f tp -> AppRenderArg f
Val f ('BVType n)
x, f ('BVType n) -> AppRenderArg f
forall (f :: Type -> Type) (tp :: Type). f tp -> AppRenderArg f
Val f ('BVType n)
y ]
    BVShl NatRepr n
_ f ('BVType n)
x f ('BVType n)
y -> Text -> [AppRenderArg f] -> AppRender f
forall (f :: Type -> Type). Text -> [AppRenderArg f] -> AppRender f
app Text
"bv_shl" [ f ('BVType n) -> AppRenderArg f
forall (f :: Type -> Type) (tp :: Type). f tp -> AppRenderArg f
Val f ('BVType n)
x, f ('BVType n) -> AppRenderArg f
forall (f :: Type -> Type) (tp :: Type). f tp -> AppRenderArg f
Val f ('BVType n)
y ]
    BVShr NatRepr n
_ f ('BVType n)
x f ('BVType n)
y -> Text -> [AppRenderArg f] -> AppRender f
forall (f :: Type -> Type). Text -> [AppRenderArg f] -> AppRender f
app Text
"bv_shr" [ f ('BVType n) -> AppRenderArg f
forall (f :: Type -> Type) (tp :: Type). f tp -> AppRenderArg f
Val f ('BVType n)
x, f ('BVType n) -> AppRenderArg f
forall (f :: Type -> Type) (tp :: Type). f tp -> AppRenderArg f
Val f ('BVType n)
y ]
    BVSar NatRepr n
_ f ('BVType n)
x f ('BVType n)
y -> Text -> [AppRenderArg f] -> AppRender f
forall (f :: Type -> Type). Text -> [AppRenderArg f] -> AppRender f
app Text
"bv_sar" [ f ('BVType n) -> AppRenderArg f
forall (f :: Type -> Type) (tp :: Type). f tp -> AppRenderArg f
Val f ('BVType n)
x, f ('BVType n) -> AppRenderArg f
forall (f :: Type -> Type) (tp :: Type). f tp -> AppRenderArg f
Val f ('BVType n)
y ]
    PopCount NatRepr n
_ f ('BVType n)
x -> Text -> [AppRenderArg f] -> AppRender f
forall (f :: Type -> Type). Text -> [AppRenderArg f] -> AppRender f
app Text
"popcount" [ f ('BVType n) -> AppRenderArg f
forall (f :: Type -> Type) (tp :: Type). f tp -> AppRenderArg f
Val f ('BVType n)
x ]
    ReverseBytes NatRepr n
_ f ('BVType (8 * n))
x -> Text -> [AppRenderArg f] -> AppRender f
forall (f :: Type -> Type). Text -> [AppRenderArg f] -> AppRender f
app Text
"reverse_bytes" [ f ('BVType (8 * n)) -> AppRenderArg f
forall (f :: Type -> Type) (tp :: Type). f tp -> AppRenderArg f
Val f ('BVType (8 * n))
x ]
    UadcOverflows f (BVType n)
x f (BVType n)
y f BoolType
c -> Text -> [AppRenderArg f] -> AppRender f
forall (f :: Type -> Type). Text -> [AppRenderArg f] -> AppRender f
app Text
"uadc_overflows" [ f (BVType n) -> AppRenderArg f
forall (f :: Type -> Type) (tp :: Type). f tp -> AppRenderArg f
Val f (BVType n)
x, f (BVType n) -> AppRenderArg f
forall (f :: Type -> Type) (tp :: Type). f tp -> AppRenderArg f
Val f (BVType n)
y, f BoolType -> AppRenderArg f
forall (f :: Type -> Type) (tp :: Type). f tp -> AppRenderArg f
Val f BoolType
c ]
    SadcOverflows f (BVType n)
x f (BVType n)
y f BoolType
c -> Text -> [AppRenderArg f] -> AppRender f
forall (f :: Type -> Type). Text -> [AppRenderArg f] -> AppRender f
app Text
"sadc_overflows" [ f (BVType n) -> AppRenderArg f
forall (f :: Type -> Type) (tp :: Type). f tp -> AppRenderArg f
Val f (BVType n)
x, f (BVType n) -> AppRenderArg f
forall (f :: Type -> Type) (tp :: Type). f tp -> AppRenderArg f
Val f (BVType n)
y, f BoolType -> AppRenderArg f
forall (f :: Type -> Type) (tp :: Type). f tp -> AppRenderArg f
Val f BoolType
c ]
    UsbbOverflows f (BVType n)
x f (BVType n)
y f BoolType
c -> Text -> [AppRenderArg f] -> AppRender f
forall (f :: Type -> Type). Text -> [AppRenderArg f] -> AppRender f
app Text
"usbb_overflows" [ f (BVType n) -> AppRenderArg f
forall (f :: Type -> Type) (tp :: Type). f tp -> AppRenderArg f
Val f (BVType n)
x, f (BVType n) -> AppRenderArg f
forall (f :: Type -> Type) (tp :: Type). f tp -> AppRenderArg f
Val f (BVType n)
y, f BoolType -> AppRenderArg f
forall (f :: Type -> Type) (tp :: Type). f tp -> AppRenderArg f
Val f BoolType
c ]
    SsbbOverflows f (BVType n)
x f (BVType n)
y f BoolType
c -> Text -> [AppRenderArg f] -> AppRender f
forall (f :: Type -> Type). Text -> [AppRenderArg f] -> AppRender f
app Text
"ssbb_overflows" [ f (BVType n) -> AppRenderArg f
forall (f :: Type -> Type) (tp :: Type). f tp -> AppRenderArg f
Val f (BVType n)
x, f (BVType n) -> AppRenderArg f
forall (f :: Type -> Type) (tp :: Type). f tp -> AppRenderArg f
Val f (BVType n)
y, f BoolType -> AppRenderArg f
forall (f :: Type -> Type) (tp :: Type). f tp -> AppRenderArg f
Val f BoolType
c ]
    Bsf NatRepr n
_ f ('BVType n)
x -> Text -> [AppRenderArg f] -> AppRender f
forall (f :: Type -> Type). Text -> [AppRenderArg f] -> AppRender f
app Text
"bsf" [ f ('BVType n) -> AppRenderArg f
forall (f :: Type -> Type) (tp :: Type). f tp -> AppRenderArg f
Val f ('BVType n)
x ]
    Bsr NatRepr n
_ f ('BVType n)
x -> Text -> [AppRenderArg f] -> AppRender f
forall (f :: Type -> Type). Text -> [AppRenderArg f] -> AppRender f
app Text
"bsr" [ f ('BVType n) -> AppRenderArg f
forall (f :: Type -> Type) (tp :: Type). f tp -> AppRenderArg f
Val f ('BVType n)
x ]

-- | Pretty print an 'App' as an expression using the given function
-- for printing arguments.
ppAppA :: forall m f tp ann
       . Applicative m
       => (forall u . f u -> m (Doc ann))
       -> App f tp
       -> m (Doc ann)
ppAppA :: forall (m :: Type -> Type) (f :: Type -> Type) (tp :: Type) ann.
Applicative m =>
(forall (u :: Type). f u -> m (Doc ann)) -> App f tp -> m (Doc ann)
ppAppA forall (u :: Type). f u -> m (Doc ann)
pp App f tp
a0 =
  case App f tp -> AppRender f
forall (f :: Type -> Type) (tp :: Type). App f tp -> AppRender f
rendApp App f tp
a0 of
    AppRender Text
nm [AppRenderArg f]
args -> do
      let rendArg :: AppRenderArg f -> m (Doc ann)
          rendArg :: AppRenderArg f -> m (Doc ann)
rendArg (Val f tp
v) = f tp -> m (Doc ann)
forall (u :: Type). f u -> m (Doc ann)
pp f tp
v
          rendArg (Type TypeRepr tp
tp) = Doc ann -> m (Doc ann)
forall a. a -> m a
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure (TypeRepr tp -> Doc ann
forall a ann. Show a => a -> Doc ann
viaShow TypeRepr tp
tp)
          rendArg (Index Natural
i) = Doc ann -> m (Doc ann)
forall a. a -> m a
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure (Natural -> Doc ann
forall a ann. Show a => a -> Doc ann
viaShow Natural
i)
          rendArg (Width Natural
i) = Doc ann -> m (Doc ann)
forall a. a -> m a
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure (Natural -> Doc ann
forall a ann. Show a => a -> Doc ann
viaShow Natural
i)
      String -> [Doc ann] -> Doc ann
forall ann. String -> [Doc ann] -> Doc ann
sexpr (Text -> String
Text.unpack Text
nm) ([Doc ann] -> Doc ann) -> m [Doc ann] -> m (Doc ann)
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> (AppRenderArg f -> m (Doc ann)) -> [AppRenderArg f] -> m [Doc ann]
forall (t :: Type -> Type) (f :: Type -> Type) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
forall (f :: Type -> Type) a b.
Applicative f =>
(a -> f b) -> [a] -> f [b]
traverse AppRenderArg f -> m (Doc ann)
rendArg [AppRenderArg f]
args

ppApp :: (forall u . f u -> Doc ann)
      -> App f tp
      -> Doc ann
ppApp :: forall (f :: Type -> Type) ann (tp :: Type).
(forall (u :: Type). f u -> Doc ann) -> App f tp -> Doc ann
ppApp forall (u :: Type). f u -> Doc ann
pp App f tp
a0 = Identity (Doc ann) -> Doc ann
forall a. Identity a -> a
runIdentity (Identity (Doc ann) -> Doc ann) -> Identity (Doc ann) -> Doc ann
forall a b. (a -> b) -> a -> b
$ (forall (u :: Type). f u -> Identity (Doc ann))
-> App f tp -> Identity (Doc ann)
forall (m :: Type -> Type) (f :: Type -> Type) (tp :: Type) ann.
Applicative m =>
(forall (u :: Type). f u -> m (Doc ann)) -> App f tp -> m (Doc ann)
ppAppA (Doc ann -> Identity (Doc ann)
forall a. a -> Identity a
Identity (Doc ann -> Identity (Doc ann))
-> (f u -> Doc ann) -> f u -> Identity (Doc ann)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. f u -> Doc ann
forall (u :: Type). f u -> Doc ann
pp) App f tp
a0

------------------------------------------------------------------------
-- appType

instance HasRepr (App f) TypeRepr where
  typeRepr :: forall (tp :: Type). App f tp -> TypeRepr tp
typeRepr App f tp
a =
    case App f tp
a of
      Eq f tp
_ f tp
_       -> TypeRepr tp
forall k (f :: k -> Type) (ctx :: k). KnownRepr f ctx => f ctx
knownRepr
      Mux TypeRepr tp
tp f BoolType
_ f tp
_ f tp
_ -> TypeRepr tp
tp

      AndApp{} -> TypeRepr tp
forall k (f :: k -> Type) (ctx :: k). KnownRepr f ctx => f ctx
knownRepr
      OrApp{}  -> TypeRepr tp
forall k (f :: k -> Type) (ctx :: k). KnownRepr f ctx => f ctx
knownRepr
      NotApp{} -> TypeRepr tp
forall k (f :: k -> Type) (ctx :: k). KnownRepr f ctx => f ctx
knownRepr
      XorApp{} -> TypeRepr tp
forall k (f :: k -> Type) (ctx :: k). KnownRepr f ctx => f ctx
knownRepr

      MkTuple List TypeRepr flds
fieldTypes List f flds
_ -> List TypeRepr flds -> TypeRepr ('TupleType flds)
forall (ctx :: [Type]).
List TypeRepr ctx -> TypeRepr ('TupleType ctx)
TupleTypeRepr List TypeRepr flds
fieldTypes
      TupleField List TypeRepr l
f f (TupleType l)
_ Index l tp
i -> List TypeRepr l
f List TypeRepr l -> Index l tp -> TypeRepr tp
forall {k} (f :: k -> Type) (l :: [k]) (x :: k).
List f l -> Index l x -> f x
P.!! Index l tp
i

      ExtractElement TypeRepr tp
tp f (VecType n tp)
_ Int
_ -> TypeRepr tp
tp
      InsertElement TypeRepr ('VecType n tp)
tp f ('VecType n tp)
_ Int
_ f tp
_ -> TypeRepr tp
TypeRepr ('VecType n tp)
tp

      Trunc f (BVType m)
_ NatRepr n
w -> NatRepr n -> TypeRepr ('BVType n)
forall (n :: Natural).
(1 <= n) =>
NatRepr n -> TypeRepr ('BVType n)
BVTypeRepr NatRepr n
w
      SExt  f (BVType m)
_ NatRepr n
w -> NatRepr n -> TypeRepr ('BVType n)
forall (n :: Natural).
(1 <= n) =>
NatRepr n -> TypeRepr ('BVType n)
BVTypeRepr NatRepr n
w
      UExt  f (BVType m)
_ NatRepr n
w -> NatRepr n -> TypeRepr ('BVType n)
forall (n :: Natural).
(1 <= n) =>
NatRepr n -> TypeRepr ('BVType n)
BVTypeRepr NatRepr n
w
      Bitcast f tp
_ WidthEqProof tp tp
p -> WidthEqProof tp tp -> TypeRepr tp
forall (i :: Type) (o :: Type). WidthEqProof i o -> TypeRepr o
widthEqTarget WidthEqProof tp tp
p

      BVAdd NatRepr n
w f ('BVType n)
_ f ('BVType n)
_   -> NatRepr n -> TypeRepr ('BVType n)
forall (n :: Natural).
(1 <= n) =>
NatRepr n -> TypeRepr ('BVType n)
BVTypeRepr NatRepr n
w
      BVAdc NatRepr n
w f ('BVType n)
_ f ('BVType n)
_ f BoolType
_ -> NatRepr n -> TypeRepr ('BVType n)
forall (n :: Natural).
(1 <= n) =>
NatRepr n -> TypeRepr ('BVType n)
BVTypeRepr NatRepr n
w
      BVSub NatRepr n
w f ('BVType n)
_ f ('BVType n)
_   -> NatRepr n -> TypeRepr ('BVType n)
forall (n :: Natural).
(1 <= n) =>
NatRepr n -> TypeRepr ('BVType n)
BVTypeRepr NatRepr n
w
      BVSbb NatRepr n
w f ('BVType n)
_ f ('BVType n)
_ f BoolType
_ -> NatRepr n -> TypeRepr ('BVType n)
forall (n :: Natural).
(1 <= n) =>
NatRepr n -> TypeRepr ('BVType n)
BVTypeRepr NatRepr n
w
      BVMul NatRepr n
w f ('BVType n)
_ f ('BVType n)
_ -> NatRepr n -> TypeRepr ('BVType n)
forall (n :: Natural).
(1 <= n) =>
NatRepr n -> TypeRepr ('BVType n)
BVTypeRepr NatRepr n
w

      BVUnsignedLt{} -> TypeRepr tp
forall k (f :: k -> Type) (ctx :: k). KnownRepr f ctx => f ctx
knownRepr
      BVUnsignedLe{} -> TypeRepr tp
forall k (f :: k -> Type) (ctx :: k). KnownRepr f ctx => f ctx
knownRepr
      BVSignedLt{} -> TypeRepr tp
forall k (f :: k -> Type) (ctx :: k). KnownRepr f ctx => f ctx
knownRepr
      BVSignedLe{} -> TypeRepr tp
forall k (f :: k -> Type) (ctx :: k). KnownRepr f ctx => f ctx
knownRepr
      BVTestBit{} -> TypeRepr tp
forall k (f :: k -> Type) (ctx :: k). KnownRepr f ctx => f ctx
knownRepr

      BVComplement NatRepr n
w f ('BVType n)
_ -> NatRepr n -> TypeRepr ('BVType n)
forall (n :: Natural).
(1 <= n) =>
NatRepr n -> TypeRepr ('BVType n)
BVTypeRepr NatRepr n
w
      BVAnd NatRepr n
w f ('BVType n)
_ f ('BVType n)
_ -> NatRepr n -> TypeRepr ('BVType n)
forall (n :: Natural).
(1 <= n) =>
NatRepr n -> TypeRepr ('BVType n)
BVTypeRepr NatRepr n
w
      BVOr  NatRepr n
w f ('BVType n)
_ f ('BVType n)
_ -> NatRepr n -> TypeRepr ('BVType n)
forall (n :: Natural).
(1 <= n) =>
NatRepr n -> TypeRepr ('BVType n)
BVTypeRepr NatRepr n
w
      BVXor NatRepr n
w f ('BVType n)
_ f ('BVType n)
_ -> NatRepr n -> TypeRepr ('BVType n)
forall (n :: Natural).
(1 <= n) =>
NatRepr n -> TypeRepr ('BVType n)
BVTypeRepr NatRepr n
w
      BVShl NatRepr n
w f ('BVType n)
_ f ('BVType n)
_ -> NatRepr n -> TypeRepr ('BVType n)
forall (n :: Natural).
(1 <= n) =>
NatRepr n -> TypeRepr ('BVType n)
BVTypeRepr NatRepr n
w
      BVShr NatRepr n
w f ('BVType n)
_ f ('BVType n)
_ -> NatRepr n -> TypeRepr ('BVType n)
forall (n :: Natural).
(1 <= n) =>
NatRepr n -> TypeRepr ('BVType n)
BVTypeRepr NatRepr n
w
      BVSar NatRepr n
w f ('BVType n)
_ f ('BVType n)
_ -> NatRepr n -> TypeRepr ('BVType n)
forall (n :: Natural).
(1 <= n) =>
NatRepr n -> TypeRepr ('BVType n)
BVTypeRepr NatRepr n
w

      UadcOverflows{} -> TypeRepr tp
forall k (f :: k -> Type) (ctx :: k). KnownRepr f ctx => f ctx
knownRepr
      SadcOverflows{} -> TypeRepr tp
forall k (f :: k -> Type) (ctx :: k). KnownRepr f ctx => f ctx
knownRepr
      UsbbOverflows{} -> TypeRepr tp
forall k (f :: k -> Type) (ctx :: k). KnownRepr f ctx => f ctx
knownRepr
      SsbbOverflows{} -> TypeRepr tp
forall k (f :: k -> Type) (ctx :: k). KnownRepr f ctx => f ctx
knownRepr

      PopCount NatRepr n
w f ('BVType n)
_ -> NatRepr n -> TypeRepr ('BVType n)
forall (n :: Natural).
(1 <= n) =>
NatRepr n -> TypeRepr ('BVType n)
BVTypeRepr NatRepr n
w
      ReverseBytes NatRepr n
w f ('BVType (8 * n))
_ ->
        case LeqProof 1 8 -> LeqProof 1 n -> LeqProof (1 * 1) (8 * n)
forall (a :: Natural) (x :: Natural) (b :: Natural) (y :: Natural).
LeqProof a x -> LeqProof b y -> LeqProof (a * b) (x * y)
leqMulCongr (LeqProof 1 8
forall (m :: Natural) (n :: Natural). (m <= n) => LeqProof m n
LeqProof :: LeqProof 1 8) (NatRepr 1 -> NatRepr n -> LeqProof 1 n
forall (m :: Natural) (n :: Natural) (f :: Natural -> Type)
       (g :: Natural -> Type).
(m <= n) =>
f m -> g n -> LeqProof m n
leqProof (NatRepr 1
forall (n :: Natural). KnownNat n => NatRepr n
knownNat :: NatRepr 1) NatRepr n
w) of
          LeqProof (1 * 1) (8 * n)
LeqProof -> NatRepr (8 * n) -> TypeRepr ('BVType (8 * n))
forall (n :: Natural).
(1 <= n) =>
NatRepr n -> TypeRepr ('BVType n)
BVTypeRepr (NatRepr 8 -> NatRepr n -> NatRepr (8 * n)
forall (n :: Natural) (m :: Natural).
NatRepr n -> NatRepr m -> NatRepr (n * m)
natMultiply (NatRepr 8
forall (n :: Natural). KnownNat n => NatRepr n
knownNat :: NatRepr 8) NatRepr n
w)
      Bsf NatRepr n
w f ('BVType n)
_ -> NatRepr n -> TypeRepr ('BVType n)
forall (n :: Natural).
(1 <= n) =>
NatRepr n -> TypeRepr ('BVType n)
BVTypeRepr NatRepr n
w
      Bsr NatRepr n
w f ('BVType n)
_ -> NatRepr n -> TypeRepr ('BVType n)
forall (n :: Natural).
(1 <= n) =>
NatRepr n -> TypeRepr ('BVType n)
BVTypeRepr NatRepr n
w