{-|
  Copyright   :  (C) 2013-2016, University of Twente,
                     2016-2017, Myrtle Software Ltd,
                     2017-2022, Google Inc.,
                     2017-2026, QBayLogic B.V.
  License     :  BSD2 (see the file LICENSE)
  Maintainer  :  QBayLogic B.V. <devops@qbaylogic.com>
-}

{-# LANGUAGE MagicHash #-}
{-# LANGUAGE LambdaCase #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE RecordWildCards #-}
{-# LANGUAGE TemplateHaskell #-}
{-# LANGUAGE UnboxedTuples #-}

{-# OPTIONS_GHC -Wno-incomplete-uni-patterns #-}

module Clash.GHC.Evaluator.Primitives.Clash.Sized.Internal.BitVector
  ( primitives
  ) where

import           Control.Monad.Trans.Except (runExcept)
import           Data.Bits
import           Data.Proxy          (Proxy)
import           Data.Reflection     (reifyNat)
import           Data.Text           (Text)
import           Data.Text.Extra     (showt)
import           GHC.TypeLits        (KnownNat)

import           Clash.Core.Evaluator.Types
import Clash.Core.HasType (piResultTys)
import           Clash.Core.Literal  (Literal (..))
import Clash.Core.Term (PrimInfo (..), Term (..), mkApps, collectArgs)
import Clash.Core.Type (TypeView (..), splitFunForallTy, tyView)
import Clash.Core.TyCon (tyConDataCons)
import Clash.Core.Util (tyNatSize, undefinedXPrims)
import qualified Clash.Data.UniqMap as UniqMap
import Clash.Util (textNameLit)

import Clash.Promoted.Nat.Unsafe (unsafeSNat)
import qualified Clash.Sized.Internal.BitVector as BitVector
import Clash.Sized.Internal.BitVector(BitVector(..), Bit(..))
import Clash.XException (isX)

import {-# SOURCE #-} Clash.GHC.Evaluator

import qualified Clash.Sized.Internal.BitVector

import {-# SOURCE #-} Clash.GHC.Evaluator.Primitive
import Clash.GHC.Evaluator.Primitive.Util

primitives :: [(Text, PrimStep)]
primitives :: [(Text, PrimStep)]
primitives =
  [ Text -> (PrimStepContext -> Maybe Machine) -> (Text, PrimStep)
primStepEntry $(textNameLit 'Clash.Sized.Internal.BitVector.xToBV) ((PrimStepContext -> Maybe Machine) -> (Text, PrimStep))
-> (PrimStepContext -> Maybe Machine) -> (Text, PrimStep)
forall a b. (a -> b) -> a -> b
$ \case
      PrimStepContext{Bool
[Type]
[Value]
Type
TyConMap
Machine
PrimInfo
Term -> Maybe Machine
Term -> Term
Type
-> Integer -> Integer -> (Natural -> Natural -> Natural) -> Term
Type -> Integer -> (Natural -> Natural) -> Term
Type -> [Integer] -> ([Natural] -> Term) -> Term
Machine -> Term -> Maybe Machine
tcm :: TyConMap
isSubj :: Bool
pInfo :: PrimInfo
tys :: [Type]
args :: [Value]
mach :: Machine
ty :: Type
checkNaturalRange1 :: Type -> Integer -> (Natural -> Natural) -> Term
checkNaturalRange2 :: Type
-> Integer -> Integer -> (Natural -> Natural -> Natural) -> Term
checkNaturalRange :: Type -> [Integer] -> ([Natural] -> Term) -> Term
reduce :: Term -> Maybe Machine
reduceWith :: Machine -> Term -> Maybe Machine
reduceWHNF :: Term -> Maybe Machine
reduceWHNF' :: Machine -> Term -> Maybe Machine
catchDivByZero :: Term -> Term
catchErrorCall :: Term -> Term
tcm :: PrimStepContext -> TyConMap
isSubj :: PrimStepContext -> Bool
pInfo :: PrimStepContext -> PrimInfo
tys :: PrimStepContext -> [Type]
args :: PrimStepContext -> [Value]
mach :: PrimStepContext -> Machine
ty :: PrimStepContext -> Type
checkNaturalRange1 :: PrimStepContext -> Type -> Integer -> (Natural -> Natural) -> Term
checkNaturalRange2 :: PrimStepContext
-> Type
-> Integer
-> Integer
-> (Natural -> Natural -> Natural)
-> Term
checkNaturalRange :: PrimStepContext -> Type -> [Integer] -> ([Natural] -> Term) -> Term
reduce :: PrimStepContext -> Term -> Maybe Machine
reduceWith :: PrimStepContext -> Machine -> Term -> Maybe Machine
reduceWHNF :: PrimStepContext -> Term -> Maybe Machine
reduceWHNF' :: PrimStepContext -> Machine -> Term -> Maybe Machine
catchDivByZero :: PrimStepContext -> Term -> Term
catchErrorCall :: PrimStepContext -> Term -> Term
..}
        | Bool
isSubj
        , Just (Type
nTy, Integer
kn) <- TyConMap -> [Type] -> Maybe (Type, Integer)
extractKnownNat TyConMap
tcm [Type]
tys
        -- The second argument to `xToBV` is always going to be suspended.
        -- See Note [Lazy primitives]
        , [ Value
_, (Suspend Term
arg) ] <- [Value]
args
        , Evaluator
eval <- Step -> Unwind -> PrimStep -> PrimUnwind -> Evaluator
Evaluator Step
ghcStep Unwind
ghcUnwind PrimStep
ghcPrimStep PrimUnwind
ghcPrimUnwind
        , mach1 :: Machine
mach1@Machine{mStack :: Machine -> Stack
mStack=[],mTerm :: Machine -> Term
mTerm=Term
argWHNF} <-
            Evaluator -> TyConMap -> Bool -> Machine -> Machine
whnf Evaluator
eval TyConMap
tcm Bool
True (Term -> Machine -> Machine
setTerm Term
arg (Machine -> Machine
stackClear Machine
mach))
        , let undefBitVector :: Maybe Machine
undefBitVector =
                Machine -> Maybe Machine
forall a. a -> Maybe a
Just (Machine -> Maybe Machine) -> Machine -> Maybe Machine
forall a b. (a -> b) -> a -> b
$ Machine
mach1
                     { mStack = mStack mach
                     , mTerm  = mkBitVectorLit ty nTy kn (bit (fromInteger kn)-1) 0
                     }
        -> case Term -> Either String Term
forall a. a -> Either String a
isX Term
argWHNF of
             Left String
_ -> Maybe Machine
undefBitVector
             Either String Term
_ -> case Term -> (Term, [Either Term Type])
collectArgs Term
argWHNF of
               (Prim PrimInfo
p,[Either Term Type]
_) | PrimInfo -> Text
primName PrimInfo
p Text -> [Text] -> Bool
forall a. Eq a => a -> [a] -> Bool
forall (t :: Type -> Type) a.
(Foldable t, Eq a) =>
a -> t a -> Bool
`elem` [Text]
undefinedXPrims -> Maybe Machine
undefBitVector
               (Term, [Either Term Type])
_ -> Machine -> Maybe Machine
forall a. a -> Maybe a
Just (Machine -> Maybe Machine) -> Machine -> Maybe Machine
forall a b. (a -> b) -> a -> b
$ Machine
mach1
                         { mStack = mStack mach
                         , mTerm  = argWHNF
                         }
      PrimStepContext
_ -> Maybe Machine
forall a. Maybe a
Nothing


------------
-- BitVector
------------
-- Constructor
  , Text -> (PrimStepContext -> Maybe Machine) -> (Text, PrimStep)
primStepEntry $(textNameLit 'Clash.Sized.Internal.BitVector.BV) ((PrimStepContext -> Maybe Machine) -> (Text, PrimStep))
-> (PrimStepContext -> Maybe Machine) -> (Text, PrimStep)
forall a b. (a -> b) -> a -> b
$ \case
      PrimStepContext{Bool
[Type]
[Value]
Type
TyConMap
Machine
PrimInfo
Term -> Maybe Machine
Term -> Term
Type
-> Integer -> Integer -> (Natural -> Natural -> Natural) -> Term
Type -> Integer -> (Natural -> Natural) -> Term
Type -> [Integer] -> ([Natural] -> Term) -> Term
Machine -> Term -> Maybe Machine
tcm :: PrimStepContext -> TyConMap
isSubj :: PrimStepContext -> Bool
pInfo :: PrimStepContext -> PrimInfo
tys :: PrimStepContext -> [Type]
args :: PrimStepContext -> [Value]
mach :: PrimStepContext -> Machine
ty :: PrimStepContext -> Type
checkNaturalRange1 :: PrimStepContext -> Type -> Integer -> (Natural -> Natural) -> Term
checkNaturalRange2 :: PrimStepContext
-> Type
-> Integer
-> Integer
-> (Natural -> Natural -> Natural)
-> Term
checkNaturalRange :: PrimStepContext -> Type -> [Integer] -> ([Natural] -> Term) -> Term
reduce :: PrimStepContext -> Term -> Maybe Machine
reduceWith :: PrimStepContext -> Machine -> Term -> Maybe Machine
reduceWHNF :: PrimStepContext -> Term -> Maybe Machine
reduceWHNF' :: PrimStepContext -> Machine -> Term -> Maybe Machine
catchDivByZero :: PrimStepContext -> Term -> Term
catchErrorCall :: PrimStepContext -> Term -> Term
tcm :: TyConMap
isSubj :: Bool
pInfo :: PrimInfo
tys :: [Type]
args :: [Value]
mach :: Machine
ty :: Type
checkNaturalRange1 :: Type -> Integer -> (Natural -> Natural) -> Term
checkNaturalRange2 :: Type
-> Integer -> Integer -> (Natural -> Natural -> Natural) -> Term
checkNaturalRange :: Type -> [Integer] -> ([Natural] -> Term) -> Term
reduce :: Term -> Maybe Machine
reduceWith :: Machine -> Term -> Maybe Machine
reduceWHNF :: Term -> Maybe Machine
reduceWHNF' :: Machine -> Term -> Maybe Machine
catchDivByZero :: Term -> Term
catchErrorCall :: Term -> Term
..}
        | [Right Integer
_] <- (Type -> Either String Integer)
-> [Type] -> [Either String Integer]
forall a b. (a -> b) -> [a] -> [b]
map (Except String Integer -> Either String Integer
forall e a. Except e a -> Either e a
runExcept (Except String Integer -> Either String Integer)
-> (Type -> Except String Integer) -> Type -> Either String Integer
forall b c a. (b -> c) -> (a -> b) -> a -> c
. TyConMap -> Type -> Except String Integer
tyNatSize TyConMap
tcm) [Type]
tys
        , Just (Integer
m,Integer
i) <- [Value] -> Maybe (Integer, Integer)
integerLiterals [Value]
args
        -> let resTyInfo :: (Type, Type, Integer)
resTyInfo = TyConMap -> Type -> [Type] -> (Type, Type, Integer)
extractTySizeInfo TyConMap
tcm Type
ty [Type]
tys
           in  Term -> Maybe Machine
reduce ((Type, Type, Integer) -> Integer -> Integer -> Term
mkBitVectorLit' (Type, Type, Integer)
resTyInfo Integer
m Integer
i)
      PrimStepContext
_ -> Maybe Machine
forall a. Maybe a
Nothing

  , Text -> (PrimStepContext -> Maybe Machine) -> (Text, PrimStep)
primStepEntry $(textNameLit 'Clash.Sized.Internal.BitVector.Bit) ((PrimStepContext -> Maybe Machine) -> (Text, PrimStep))
-> (PrimStepContext -> Maybe Machine) -> (Text, PrimStep)
forall a b. (a -> b) -> a -> b
$ \case
      PrimStepContext{Bool
[Type]
[Value]
Type
TyConMap
Machine
PrimInfo
Term -> Maybe Machine
Term -> Term
Type
-> Integer -> Integer -> (Natural -> Natural -> Natural) -> Term
Type -> Integer -> (Natural -> Natural) -> Term
Type -> [Integer] -> ([Natural] -> Term) -> Term
Machine -> Term -> Maybe Machine
tcm :: PrimStepContext -> TyConMap
isSubj :: PrimStepContext -> Bool
pInfo :: PrimStepContext -> PrimInfo
tys :: PrimStepContext -> [Type]
args :: PrimStepContext -> [Value]
mach :: PrimStepContext -> Machine
ty :: PrimStepContext -> Type
checkNaturalRange1 :: PrimStepContext -> Type -> Integer -> (Natural -> Natural) -> Term
checkNaturalRange2 :: PrimStepContext
-> Type
-> Integer
-> Integer
-> (Natural -> Natural -> Natural)
-> Term
checkNaturalRange :: PrimStepContext -> Type -> [Integer] -> ([Natural] -> Term) -> Term
reduce :: PrimStepContext -> Term -> Maybe Machine
reduceWith :: PrimStepContext -> Machine -> Term -> Maybe Machine
reduceWHNF :: PrimStepContext -> Term -> Maybe Machine
reduceWHNF' :: PrimStepContext -> Machine -> Term -> Maybe Machine
catchDivByZero :: PrimStepContext -> Term -> Term
catchErrorCall :: PrimStepContext -> Term -> Term
tcm :: TyConMap
isSubj :: Bool
pInfo :: PrimInfo
tys :: [Type]
args :: [Value]
mach :: Machine
ty :: Type
checkNaturalRange1 :: Type -> Integer -> (Natural -> Natural) -> Term
checkNaturalRange2 :: Type
-> Integer -> Integer -> (Natural -> Natural -> Natural) -> Term
checkNaturalRange :: Type -> [Integer] -> ([Natural] -> Term) -> Term
reduce :: Term -> Maybe Machine
reduceWith :: Machine -> Term -> Maybe Machine
reduceWHNF :: Term -> Maybe Machine
reduceWHNF' :: Machine -> Term -> Maybe Machine
catchDivByZero :: Term -> Term
catchErrorCall :: Term -> Term
..}
        | Just (Integer
m,Integer
i) <- [Value] -> Maybe (Integer, Integer)
integerLiterals [Value]
args
        -> Term -> Maybe Machine
reduce (Type -> Integer -> Integer -> Term
mkBitLit Type
ty Integer
m Integer
i)
      PrimStepContext
_ -> Maybe Machine
forall a. Maybe a
Nothing


-- Initialization
  , Text -> (PrimStepContext -> Maybe Machine) -> (Text, PrimStep)
primStepEntry $(textNameLit 'Clash.Sized.Internal.BitVector.size#) ((PrimStepContext -> Maybe Machine) -> (Text, PrimStep))
-> (PrimStepContext -> Maybe Machine) -> (Text, PrimStep)
forall a b. (a -> b) -> a -> b
$ \case
      PrimStepContext{Bool
[Type]
[Value]
Type
TyConMap
Machine
PrimInfo
Term -> Maybe Machine
Term -> Term
Type
-> Integer -> Integer -> (Natural -> Natural -> Natural) -> Term
Type -> Integer -> (Natural -> Natural) -> Term
Type -> [Integer] -> ([Natural] -> Term) -> Term
Machine -> Term -> Maybe Machine
tcm :: PrimStepContext -> TyConMap
isSubj :: PrimStepContext -> Bool
pInfo :: PrimStepContext -> PrimInfo
tys :: PrimStepContext -> [Type]
args :: PrimStepContext -> [Value]
mach :: PrimStepContext -> Machine
ty :: PrimStepContext -> Type
checkNaturalRange1 :: PrimStepContext -> Type -> Integer -> (Natural -> Natural) -> Term
checkNaturalRange2 :: PrimStepContext
-> Type
-> Integer
-> Integer
-> (Natural -> Natural -> Natural)
-> Term
checkNaturalRange :: PrimStepContext -> Type -> [Integer] -> ([Natural] -> Term) -> Term
reduce :: PrimStepContext -> Term -> Maybe Machine
reduceWith :: PrimStepContext -> Machine -> Term -> Maybe Machine
reduceWHNF :: PrimStepContext -> Term -> Maybe Machine
reduceWHNF' :: PrimStepContext -> Machine -> Term -> Maybe Machine
catchDivByZero :: PrimStepContext -> Term -> Term
catchErrorCall :: PrimStepContext -> Term -> Term
tcm :: TyConMap
isSubj :: Bool
pInfo :: PrimInfo
tys :: [Type]
args :: [Value]
mach :: Machine
ty :: Type
checkNaturalRange1 :: Type -> Integer -> (Natural -> Natural) -> Term
checkNaturalRange2 :: Type
-> Integer -> Integer -> (Natural -> Natural -> Natural) -> Term
checkNaturalRange :: Type -> [Integer] -> ([Natural] -> Term) -> Term
reduce :: Term -> Maybe Machine
reduceWith :: Machine -> Term -> Maybe Machine
reduceWHNF :: Term -> Maybe Machine
reduceWHNF' :: Machine -> Term -> Maybe Machine
catchDivByZero :: Term -> Term
catchErrorCall :: Term -> Term
..}
        | Just (Type
_, Integer
kn) <- TyConMap -> [Type] -> Maybe (Type, Integer)
extractKnownNat TyConMap
tcm [Type]
tys
        -> let ([Either TyVar Type]
_,Type -> TypeView
tyView -> TyConApp TyConName
intTcNm [Type]
_) = Type -> ([Either TyVar Type], Type)
splitFunForallTy Type
ty
               (Just TyCon
intTc) = TyConName -> TyConMap -> Maybe TyCon
forall a b. Uniquable a => a -> UniqMap b -> Maybe b
UniqMap.lookup TyConName
intTcNm TyConMap
tcm
               [DataCon
intCon] = TyCon -> [DataCon]
tyConDataCons TyCon
intTc
           in  Term -> Maybe Machine
reduce (Term -> [Either Term Type] -> Term
mkApps (DataCon -> Term
Data DataCon
intCon) [Term -> Either Term Type
forall a b. a -> Either a b
Left (Literal -> Term
Literal (Integer -> Literal
IntLiteral Integer
kn))])
      PrimStepContext
_ -> Maybe Machine
forall a. Maybe a
Nothing

  , Text -> (PrimStepContext -> Maybe Machine) -> (Text, PrimStep)
primStepEntry $(textNameLit 'Clash.Sized.Internal.BitVector.maxIndex#) ((PrimStepContext -> Maybe Machine) -> (Text, PrimStep))
-> (PrimStepContext -> Maybe Machine) -> (Text, PrimStep)
forall a b. (a -> b) -> a -> b
$ \case
      PrimStepContext{Bool
[Type]
[Value]
Type
TyConMap
Machine
PrimInfo
Term -> Maybe Machine
Term -> Term
Type
-> Integer -> Integer -> (Natural -> Natural -> Natural) -> Term
Type -> Integer -> (Natural -> Natural) -> Term
Type -> [Integer] -> ([Natural] -> Term) -> Term
Machine -> Term -> Maybe Machine
tcm :: PrimStepContext -> TyConMap
isSubj :: PrimStepContext -> Bool
pInfo :: PrimStepContext -> PrimInfo
tys :: PrimStepContext -> [Type]
args :: PrimStepContext -> [Value]
mach :: PrimStepContext -> Machine
ty :: PrimStepContext -> Type
checkNaturalRange1 :: PrimStepContext -> Type -> Integer -> (Natural -> Natural) -> Term
checkNaturalRange2 :: PrimStepContext
-> Type
-> Integer
-> Integer
-> (Natural -> Natural -> Natural)
-> Term
checkNaturalRange :: PrimStepContext -> Type -> [Integer] -> ([Natural] -> Term) -> Term
reduce :: PrimStepContext -> Term -> Maybe Machine
reduceWith :: PrimStepContext -> Machine -> Term -> Maybe Machine
reduceWHNF :: PrimStepContext -> Term -> Maybe Machine
reduceWHNF' :: PrimStepContext -> Machine -> Term -> Maybe Machine
catchDivByZero :: PrimStepContext -> Term -> Term
catchErrorCall :: PrimStepContext -> Term -> Term
tcm :: TyConMap
isSubj :: Bool
pInfo :: PrimInfo
tys :: [Type]
args :: [Value]
mach :: Machine
ty :: Type
checkNaturalRange1 :: Type -> Integer -> (Natural -> Natural) -> Term
checkNaturalRange2 :: Type
-> Integer -> Integer -> (Natural -> Natural -> Natural) -> Term
checkNaturalRange :: Type -> [Integer] -> ([Natural] -> Term) -> Term
reduce :: Term -> Maybe Machine
reduceWith :: Machine -> Term -> Maybe Machine
reduceWHNF :: Term -> Maybe Machine
reduceWHNF' :: Machine -> Term -> Maybe Machine
catchDivByZero :: Term -> Term
catchErrorCall :: Term -> Term
..}
        | Just (Type
_, Integer
kn) <- TyConMap -> [Type] -> Maybe (Type, Integer)
extractKnownNat TyConMap
tcm [Type]
tys
        -> let ([Either TyVar Type]
_,Type -> TypeView
tyView -> TyConApp TyConName
intTcNm [Type]
_) = Type -> ([Either TyVar Type], Type)
splitFunForallTy Type
ty
               (Just TyCon
intTc) = TyConName -> TyConMap -> Maybe TyCon
forall a b. Uniquable a => a -> UniqMap b -> Maybe b
UniqMap.lookup TyConName
intTcNm TyConMap
tcm
               [DataCon
intCon] = TyCon -> [DataCon]
tyConDataCons TyCon
intTc
           in  Term -> Maybe Machine
reduce (Term -> [Either Term Type] -> Term
mkApps (DataCon -> Term
Data DataCon
intCon) [Term -> Either Term Type
forall a b. a -> Either a b
Left (Literal -> Term
Literal (Integer -> Literal
IntLiteral (Integer
knInteger -> Integer -> Integer
forall a. Num a => a -> a -> a
-Integer
1)))])
      PrimStepContext
_ -> Maybe Machine
forall a. Maybe a
Nothing


-- Construction
  , Text -> (PrimStepContext -> Maybe Machine) -> (Text, PrimStep)
primStepEntry $(textNameLit 'Clash.Sized.Internal.BitVector.high) ((PrimStepContext -> Maybe Machine) -> (Text, PrimStep))
-> (PrimStepContext -> Maybe Machine) -> (Text, PrimStep)
forall a b. (a -> b) -> a -> b
$ \case
      PrimStepContext{Bool
[Type]
[Value]
Type
TyConMap
Machine
PrimInfo
Term -> Maybe Machine
Term -> Term
Type
-> Integer -> Integer -> (Natural -> Natural -> Natural) -> Term
Type -> Integer -> (Natural -> Natural) -> Term
Type -> [Integer] -> ([Natural] -> Term) -> Term
Machine -> Term -> Maybe Machine
tcm :: PrimStepContext -> TyConMap
isSubj :: PrimStepContext -> Bool
pInfo :: PrimStepContext -> PrimInfo
tys :: PrimStepContext -> [Type]
args :: PrimStepContext -> [Value]
mach :: PrimStepContext -> Machine
ty :: PrimStepContext -> Type
checkNaturalRange1 :: PrimStepContext -> Type -> Integer -> (Natural -> Natural) -> Term
checkNaturalRange2 :: PrimStepContext
-> Type
-> Integer
-> Integer
-> (Natural -> Natural -> Natural)
-> Term
checkNaturalRange :: PrimStepContext -> Type -> [Integer] -> ([Natural] -> Term) -> Term
reduce :: PrimStepContext -> Term -> Maybe Machine
reduceWith :: PrimStepContext -> Machine -> Term -> Maybe Machine
reduceWHNF :: PrimStepContext -> Term -> Maybe Machine
reduceWHNF' :: PrimStepContext -> Machine -> Term -> Maybe Machine
catchDivByZero :: PrimStepContext -> Term -> Term
catchErrorCall :: PrimStepContext -> Term -> Term
tcm :: TyConMap
isSubj :: Bool
pInfo :: PrimInfo
tys :: [Type]
args :: [Value]
mach :: Machine
ty :: Type
checkNaturalRange1 :: Type -> Integer -> (Natural -> Natural) -> Term
checkNaturalRange2 :: Type
-> Integer -> Integer -> (Natural -> Natural -> Natural) -> Term
checkNaturalRange :: Type -> [Integer] -> ([Natural] -> Term) -> Term
reduce :: Term -> Maybe Machine
reduceWith :: Machine -> Term -> Maybe Machine
reduceWHNF :: Term -> Maybe Machine
reduceWHNF' :: Machine -> Term -> Maybe Machine
catchDivByZero :: Term -> Term
catchErrorCall :: Term -> Term
..}
        -> Term -> Maybe Machine
reduce (Type -> Integer -> Integer -> Term
mkBitLit Type
ty Integer
0 Integer
1)

  , Text -> (PrimStepContext -> Maybe Machine) -> (Text, PrimStep)
primStepEntry $(textNameLit 'Clash.Sized.Internal.BitVector.low) ((PrimStepContext -> Maybe Machine) -> (Text, PrimStep))
-> (PrimStepContext -> Maybe Machine) -> (Text, PrimStep)
forall a b. (a -> b) -> a -> b
$ \case
      PrimStepContext{Bool
[Type]
[Value]
Type
TyConMap
Machine
PrimInfo
Term -> Maybe Machine
Term -> Term
Type
-> Integer -> Integer -> (Natural -> Natural -> Natural) -> Term
Type -> Integer -> (Natural -> Natural) -> Term
Type -> [Integer] -> ([Natural] -> Term) -> Term
Machine -> Term -> Maybe Machine
tcm :: PrimStepContext -> TyConMap
isSubj :: PrimStepContext -> Bool
pInfo :: PrimStepContext -> PrimInfo
tys :: PrimStepContext -> [Type]
args :: PrimStepContext -> [Value]
mach :: PrimStepContext -> Machine
ty :: PrimStepContext -> Type
checkNaturalRange1 :: PrimStepContext -> Type -> Integer -> (Natural -> Natural) -> Term
checkNaturalRange2 :: PrimStepContext
-> Type
-> Integer
-> Integer
-> (Natural -> Natural -> Natural)
-> Term
checkNaturalRange :: PrimStepContext -> Type -> [Integer] -> ([Natural] -> Term) -> Term
reduce :: PrimStepContext -> Term -> Maybe Machine
reduceWith :: PrimStepContext -> Machine -> Term -> Maybe Machine
reduceWHNF :: PrimStepContext -> Term -> Maybe Machine
reduceWHNF' :: PrimStepContext -> Machine -> Term -> Maybe Machine
catchDivByZero :: PrimStepContext -> Term -> Term
catchErrorCall :: PrimStepContext -> Term -> Term
tcm :: TyConMap
isSubj :: Bool
pInfo :: PrimInfo
tys :: [Type]
args :: [Value]
mach :: Machine
ty :: Type
checkNaturalRange1 :: Type -> Integer -> (Natural -> Natural) -> Term
checkNaturalRange2 :: Type
-> Integer -> Integer -> (Natural -> Natural -> Natural) -> Term
checkNaturalRange :: Type -> [Integer] -> ([Natural] -> Term) -> Term
reduce :: Term -> Maybe Machine
reduceWith :: Machine -> Term -> Maybe Machine
reduceWHNF :: Term -> Maybe Machine
reduceWHNF' :: Machine -> Term -> Maybe Machine
catchDivByZero :: Term -> Term
catchErrorCall :: Term -> Term
..}
        -> Term -> Maybe Machine
reduce (Type -> Integer -> Integer -> Term
mkBitLit Type
ty Integer
0 Integer
0)

  , Text -> (PrimStepContext -> Maybe Machine) -> (Text, PrimStep)
primStepEntry $(textNameLit 'Clash.Sized.Internal.BitVector.undefined##) ((PrimStepContext -> Maybe Machine) -> (Text, PrimStep))
-> (PrimStepContext -> Maybe Machine) -> (Text, PrimStep)
forall a b. (a -> b) -> a -> b
$ \case
      PrimStepContext{Bool
[Type]
[Value]
Type
TyConMap
Machine
PrimInfo
Term -> Maybe Machine
Term -> Term
Type
-> Integer -> Integer -> (Natural -> Natural -> Natural) -> Term
Type -> Integer -> (Natural -> Natural) -> Term
Type -> [Integer] -> ([Natural] -> Term) -> Term
Machine -> Term -> Maybe Machine
tcm :: PrimStepContext -> TyConMap
isSubj :: PrimStepContext -> Bool
pInfo :: PrimStepContext -> PrimInfo
tys :: PrimStepContext -> [Type]
args :: PrimStepContext -> [Value]
mach :: PrimStepContext -> Machine
ty :: PrimStepContext -> Type
checkNaturalRange1 :: PrimStepContext -> Type -> Integer -> (Natural -> Natural) -> Term
checkNaturalRange2 :: PrimStepContext
-> Type
-> Integer
-> Integer
-> (Natural -> Natural -> Natural)
-> Term
checkNaturalRange :: PrimStepContext -> Type -> [Integer] -> ([Natural] -> Term) -> Term
reduce :: PrimStepContext -> Term -> Maybe Machine
reduceWith :: PrimStepContext -> Machine -> Term -> Maybe Machine
reduceWHNF :: PrimStepContext -> Term -> Maybe Machine
reduceWHNF' :: PrimStepContext -> Machine -> Term -> Maybe Machine
catchDivByZero :: PrimStepContext -> Term -> Term
catchErrorCall :: PrimStepContext -> Term -> Term
tcm :: TyConMap
isSubj :: Bool
pInfo :: PrimInfo
tys :: [Type]
args :: [Value]
mach :: Machine
ty :: Type
checkNaturalRange1 :: Type -> Integer -> (Natural -> Natural) -> Term
checkNaturalRange2 :: Type
-> Integer -> Integer -> (Natural -> Natural -> Natural) -> Term
checkNaturalRange :: Type -> [Integer] -> ([Natural] -> Term) -> Term
reduce :: Term -> Maybe Machine
reduceWith :: Machine -> Term -> Maybe Machine
reduceWHNF :: Term -> Maybe Machine
reduceWHNF' :: Machine -> Term -> Maybe Machine
catchDivByZero :: Term -> Term
catchErrorCall :: Term -> Term
..}
        -> Term -> Maybe Machine
reduce (Type -> Integer -> Integer -> Term
mkBitLit Type
ty Integer
1 Integer
0)

  , Text -> (PrimStepContext -> Maybe Machine) -> (Text, PrimStep)
primStepEntry $(textNameLit 'Clash.Sized.Internal.BitVector.undefined#) ((PrimStepContext -> Maybe Machine) -> (Text, PrimStep))
-> (PrimStepContext -> Maybe Machine) -> (Text, PrimStep)
forall a b. (a -> b) -> a -> b
$ \case
      PrimStepContext{Bool
[Type]
[Value]
Type
TyConMap
Machine
PrimInfo
Term -> Maybe Machine
Term -> Term
Type
-> Integer -> Integer -> (Natural -> Natural -> Natural) -> Term
Type -> Integer -> (Natural -> Natural) -> Term
Type -> [Integer] -> ([Natural] -> Term) -> Term
Machine -> Term -> Maybe Machine
tcm :: PrimStepContext -> TyConMap
isSubj :: PrimStepContext -> Bool
pInfo :: PrimStepContext -> PrimInfo
tys :: PrimStepContext -> [Type]
args :: PrimStepContext -> [Value]
mach :: PrimStepContext -> Machine
ty :: PrimStepContext -> Type
checkNaturalRange1 :: PrimStepContext -> Type -> Integer -> (Natural -> Natural) -> Term
checkNaturalRange2 :: PrimStepContext
-> Type
-> Integer
-> Integer
-> (Natural -> Natural -> Natural)
-> Term
checkNaturalRange :: PrimStepContext -> Type -> [Integer] -> ([Natural] -> Term) -> Term
reduce :: PrimStepContext -> Term -> Maybe Machine
reduceWith :: PrimStepContext -> Machine -> Term -> Maybe Machine
reduceWHNF :: PrimStepContext -> Term -> Maybe Machine
reduceWHNF' :: PrimStepContext -> Machine -> Term -> Maybe Machine
catchDivByZero :: PrimStepContext -> Term -> Term
catchErrorCall :: PrimStepContext -> Term -> Term
tcm :: TyConMap
isSubj :: Bool
pInfo :: PrimInfo
tys :: [Type]
args :: [Value]
mach :: Machine
ty :: Type
checkNaturalRange1 :: Type -> Integer -> (Natural -> Natural) -> Term
checkNaturalRange2 :: Type
-> Integer -> Integer -> (Natural -> Natural -> Natural) -> Term
checkNaturalRange :: Type -> [Integer] -> ([Natural] -> Term) -> Term
reduce :: Term -> Maybe Machine
reduceWith :: Machine -> Term -> Maybe Machine
reduceWHNF :: Term -> Maybe Machine
reduceWHNF' :: Machine -> Term -> Maybe Machine
catchDivByZero :: Term -> Term
catchErrorCall :: Term -> Term
..}
        | Just (Type
_, Integer
kn) <- TyConMap -> [Type] -> Maybe (Type, Integer)
extractKnownNat TyConMap
tcm [Type]
tys
        -> let resTyInfo :: (Type, Type, Integer)
resTyInfo = TyConMap -> Type -> [Type] -> (Type, Type, Integer)
extractTySizeInfo TyConMap
tcm Type
ty [Type]
tys
               mask :: Integer
mask = Int -> Integer
forall a. Bits a => Int -> a
bit (Integer -> Int
forall a. Num a => Integer -> a
fromInteger Integer
kn) Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
- Integer
1
           in Term -> Maybe Machine
reduce ((Type, Type, Integer) -> Integer -> Integer -> Term
mkBitVectorLit' (Type, Type, Integer)
resTyInfo Integer
mask Integer
0)
      PrimStepContext
_ -> Maybe Machine
forall a. Maybe a
Nothing


-- Eq
  , Text -> (PrimStepContext -> Maybe Machine) -> (Text, PrimStep)
primStepEntry $(textNameLit 'Clash.Sized.Internal.BitVector.eq##) ((PrimStepContext -> Maybe Machine) -> (Text, PrimStep))
-> (PrimStepContext -> Maybe Machine) -> (Text, PrimStep)
forall a b. (a -> b) -> a -> b
$ \case
      PrimStepContext{Bool
[Type]
[Value]
Type
TyConMap
Machine
PrimInfo
Term -> Maybe Machine
Term -> Term
Type
-> Integer -> Integer -> (Natural -> Natural -> Natural) -> Term
Type -> Integer -> (Natural -> Natural) -> Term
Type -> [Integer] -> ([Natural] -> Term) -> Term
Machine -> Term -> Maybe Machine
tcm :: PrimStepContext -> TyConMap
isSubj :: PrimStepContext -> Bool
pInfo :: PrimStepContext -> PrimInfo
tys :: PrimStepContext -> [Type]
args :: PrimStepContext -> [Value]
mach :: PrimStepContext -> Machine
ty :: PrimStepContext -> Type
checkNaturalRange1 :: PrimStepContext -> Type -> Integer -> (Natural -> Natural) -> Term
checkNaturalRange2 :: PrimStepContext
-> Type
-> Integer
-> Integer
-> (Natural -> Natural -> Natural)
-> Term
checkNaturalRange :: PrimStepContext -> Type -> [Integer] -> ([Natural] -> Term) -> Term
reduce :: PrimStepContext -> Term -> Maybe Machine
reduceWith :: PrimStepContext -> Machine -> Term -> Maybe Machine
reduceWHNF :: PrimStepContext -> Term -> Maybe Machine
reduceWHNF' :: PrimStepContext -> Machine -> Term -> Maybe Machine
catchDivByZero :: PrimStepContext -> Term -> Term
catchErrorCall :: PrimStepContext -> Term -> Term
tcm :: TyConMap
isSubj :: Bool
pInfo :: PrimInfo
tys :: [Type]
args :: [Value]
mach :: Machine
ty :: Type
checkNaturalRange1 :: Type -> Integer -> (Natural -> Natural) -> Term
checkNaturalRange2 :: Type
-> Integer -> Integer -> (Natural -> Natural -> Natural) -> Term
checkNaturalRange :: Type -> [Integer] -> ([Natural] -> Term) -> Term
reduce :: Term -> Maybe Machine
reduceWith :: Machine -> Term -> Maybe Machine
reduceWHNF :: Term -> Maybe Machine
reduceWHNF' :: Machine -> Term -> Maybe Machine
catchDivByZero :: Term -> Term
catchErrorCall :: Term -> Term
..} | [(Integer
0,Integer
i),(Integer
0,Integer
j)] <- [Value] -> [(Integer, Integer)]
bitLiterals [Value]
args
        -> Term -> Maybe Machine
reduce (TyConMap -> Type -> Bool -> Term
boolToBoolLiteral TyConMap
tcm Type
ty (Integer
i Integer -> Integer -> Bool
forall a. Eq a => a -> a -> Bool
== Integer
j))
      PrimStepContext
_ -> Maybe Machine
forall a. Maybe a
Nothing

  , Text -> (PrimStepContext -> Maybe Machine) -> (Text, PrimStep)
primStepEntry $(textNameLit 'Clash.Sized.Internal.BitVector.neq##) ((PrimStepContext -> Maybe Machine) -> (Text, PrimStep))
-> (PrimStepContext -> Maybe Machine) -> (Text, PrimStep)
forall a b. (a -> b) -> a -> b
$ \case
      PrimStepContext{Bool
[Type]
[Value]
Type
TyConMap
Machine
PrimInfo
Term -> Maybe Machine
Term -> Term
Type
-> Integer -> Integer -> (Natural -> Natural -> Natural) -> Term
Type -> Integer -> (Natural -> Natural) -> Term
Type -> [Integer] -> ([Natural] -> Term) -> Term
Machine -> Term -> Maybe Machine
tcm :: PrimStepContext -> TyConMap
isSubj :: PrimStepContext -> Bool
pInfo :: PrimStepContext -> PrimInfo
tys :: PrimStepContext -> [Type]
args :: PrimStepContext -> [Value]
mach :: PrimStepContext -> Machine
ty :: PrimStepContext -> Type
checkNaturalRange1 :: PrimStepContext -> Type -> Integer -> (Natural -> Natural) -> Term
checkNaturalRange2 :: PrimStepContext
-> Type
-> Integer
-> Integer
-> (Natural -> Natural -> Natural)
-> Term
checkNaturalRange :: PrimStepContext -> Type -> [Integer] -> ([Natural] -> Term) -> Term
reduce :: PrimStepContext -> Term -> Maybe Machine
reduceWith :: PrimStepContext -> Machine -> Term -> Maybe Machine
reduceWHNF :: PrimStepContext -> Term -> Maybe Machine
reduceWHNF' :: PrimStepContext -> Machine -> Term -> Maybe Machine
catchDivByZero :: PrimStepContext -> Term -> Term
catchErrorCall :: PrimStepContext -> Term -> Term
tcm :: TyConMap
isSubj :: Bool
pInfo :: PrimInfo
tys :: [Type]
args :: [Value]
mach :: Machine
ty :: Type
checkNaturalRange1 :: Type -> Integer -> (Natural -> Natural) -> Term
checkNaturalRange2 :: Type
-> Integer -> Integer -> (Natural -> Natural -> Natural) -> Term
checkNaturalRange :: Type -> [Integer] -> ([Natural] -> Term) -> Term
reduce :: Term -> Maybe Machine
reduceWith :: Machine -> Term -> Maybe Machine
reduceWHNF :: Term -> Maybe Machine
reduceWHNF' :: Machine -> Term -> Maybe Machine
catchDivByZero :: Term -> Term
catchErrorCall :: Term -> Term
..} | [(Integer
0,Integer
i),(Integer
0,Integer
j)] <- [Value] -> [(Integer, Integer)]
bitLiterals [Value]
args
        -> Term -> Maybe Machine
reduce (TyConMap -> Type -> Bool -> Term
boolToBoolLiteral TyConMap
tcm Type
ty (Integer
i Integer -> Integer -> Bool
forall a. Eq a => a -> a -> Bool
/= Integer
j))
      PrimStepContext
_ -> Maybe Machine
forall a. Maybe a
Nothing


-- Ord
  , Text -> (PrimStepContext -> Maybe Machine) -> (Text, PrimStep)
primStepEntry $(textNameLit 'Clash.Sized.Internal.BitVector.lt##) ((PrimStepContext -> Maybe Machine) -> (Text, PrimStep))
-> (PrimStepContext -> Maybe Machine) -> (Text, PrimStep)
forall a b. (a -> b) -> a -> b
$ \case
      PrimStepContext{Bool
[Type]
[Value]
Type
TyConMap
Machine
PrimInfo
Term -> Maybe Machine
Term -> Term
Type
-> Integer -> Integer -> (Natural -> Natural -> Natural) -> Term
Type -> Integer -> (Natural -> Natural) -> Term
Type -> [Integer] -> ([Natural] -> Term) -> Term
Machine -> Term -> Maybe Machine
tcm :: PrimStepContext -> TyConMap
isSubj :: PrimStepContext -> Bool
pInfo :: PrimStepContext -> PrimInfo
tys :: PrimStepContext -> [Type]
args :: PrimStepContext -> [Value]
mach :: PrimStepContext -> Machine
ty :: PrimStepContext -> Type
checkNaturalRange1 :: PrimStepContext -> Type -> Integer -> (Natural -> Natural) -> Term
checkNaturalRange2 :: PrimStepContext
-> Type
-> Integer
-> Integer
-> (Natural -> Natural -> Natural)
-> Term
checkNaturalRange :: PrimStepContext -> Type -> [Integer] -> ([Natural] -> Term) -> Term
reduce :: PrimStepContext -> Term -> Maybe Machine
reduceWith :: PrimStepContext -> Machine -> Term -> Maybe Machine
reduceWHNF :: PrimStepContext -> Term -> Maybe Machine
reduceWHNF' :: PrimStepContext -> Machine -> Term -> Maybe Machine
catchDivByZero :: PrimStepContext -> Term -> Term
catchErrorCall :: PrimStepContext -> Term -> Term
tcm :: TyConMap
isSubj :: Bool
pInfo :: PrimInfo
tys :: [Type]
args :: [Value]
mach :: Machine
ty :: Type
checkNaturalRange1 :: Type -> Integer -> (Natural -> Natural) -> Term
checkNaturalRange2 :: Type
-> Integer -> Integer -> (Natural -> Natural -> Natural) -> Term
checkNaturalRange :: Type -> [Integer] -> ([Natural] -> Term) -> Term
reduce :: Term -> Maybe Machine
reduceWith :: Machine -> Term -> Maybe Machine
reduceWHNF :: Term -> Maybe Machine
reduceWHNF' :: Machine -> Term -> Maybe Machine
catchDivByZero :: Term -> Term
catchErrorCall :: Term -> Term
..} | [(Integer
0,Integer
i),(Integer
0,Integer
j)] <- [Value] -> [(Integer, Integer)]
bitLiterals [Value]
args
        -> Term -> Maybe Machine
reduce (TyConMap -> Type -> Bool -> Term
boolToBoolLiteral TyConMap
tcm Type
ty (Integer
i Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
<  Integer
j))
      PrimStepContext
_ -> Maybe Machine
forall a. Maybe a
Nothing

  , Text -> (PrimStepContext -> Maybe Machine) -> (Text, PrimStep)
primStepEntry $(textNameLit 'Clash.Sized.Internal.BitVector.ge##) ((PrimStepContext -> Maybe Machine) -> (Text, PrimStep))
-> (PrimStepContext -> Maybe Machine) -> (Text, PrimStep)
forall a b. (a -> b) -> a -> b
$ \case
      PrimStepContext{Bool
[Type]
[Value]
Type
TyConMap
Machine
PrimInfo
Term -> Maybe Machine
Term -> Term
Type
-> Integer -> Integer -> (Natural -> Natural -> Natural) -> Term
Type -> Integer -> (Natural -> Natural) -> Term
Type -> [Integer] -> ([Natural] -> Term) -> Term
Machine -> Term -> Maybe Machine
tcm :: PrimStepContext -> TyConMap
isSubj :: PrimStepContext -> Bool
pInfo :: PrimStepContext -> PrimInfo
tys :: PrimStepContext -> [Type]
args :: PrimStepContext -> [Value]
mach :: PrimStepContext -> Machine
ty :: PrimStepContext -> Type
checkNaturalRange1 :: PrimStepContext -> Type -> Integer -> (Natural -> Natural) -> Term
checkNaturalRange2 :: PrimStepContext
-> Type
-> Integer
-> Integer
-> (Natural -> Natural -> Natural)
-> Term
checkNaturalRange :: PrimStepContext -> Type -> [Integer] -> ([Natural] -> Term) -> Term
reduce :: PrimStepContext -> Term -> Maybe Machine
reduceWith :: PrimStepContext -> Machine -> Term -> Maybe Machine
reduceWHNF :: PrimStepContext -> Term -> Maybe Machine
reduceWHNF' :: PrimStepContext -> Machine -> Term -> Maybe Machine
catchDivByZero :: PrimStepContext -> Term -> Term
catchErrorCall :: PrimStepContext -> Term -> Term
tcm :: TyConMap
isSubj :: Bool
pInfo :: PrimInfo
tys :: [Type]
args :: [Value]
mach :: Machine
ty :: Type
checkNaturalRange1 :: Type -> Integer -> (Natural -> Natural) -> Term
checkNaturalRange2 :: Type
-> Integer -> Integer -> (Natural -> Natural -> Natural) -> Term
checkNaturalRange :: Type -> [Integer] -> ([Natural] -> Term) -> Term
reduce :: Term -> Maybe Machine
reduceWith :: Machine -> Term -> Maybe Machine
reduceWHNF :: Term -> Maybe Machine
reduceWHNF' :: Machine -> Term -> Maybe Machine
catchDivByZero :: Term -> Term
catchErrorCall :: Term -> Term
..} | [(Integer
0,Integer
i),(Integer
0,Integer
j)] <- [Value] -> [(Integer, Integer)]
bitLiterals [Value]
args
        -> Term -> Maybe Machine
reduce (TyConMap -> Type -> Bool -> Term
boolToBoolLiteral TyConMap
tcm Type
ty (Integer
i Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
>= Integer
j))
      PrimStepContext
_ -> Maybe Machine
forall a. Maybe a
Nothing

  , Text -> (PrimStepContext -> Maybe Machine) -> (Text, PrimStep)
primStepEntry $(textNameLit 'Clash.Sized.Internal.BitVector.gt##) ((PrimStepContext -> Maybe Machine) -> (Text, PrimStep))
-> (PrimStepContext -> Maybe Machine) -> (Text, PrimStep)
forall a b. (a -> b) -> a -> b
$ \case
      PrimStepContext{Bool
[Type]
[Value]
Type
TyConMap
Machine
PrimInfo
Term -> Maybe Machine
Term -> Term
Type
-> Integer -> Integer -> (Natural -> Natural -> Natural) -> Term
Type -> Integer -> (Natural -> Natural) -> Term
Type -> [Integer] -> ([Natural] -> Term) -> Term
Machine -> Term -> Maybe Machine
tcm :: PrimStepContext -> TyConMap
isSubj :: PrimStepContext -> Bool
pInfo :: PrimStepContext -> PrimInfo
tys :: PrimStepContext -> [Type]
args :: PrimStepContext -> [Value]
mach :: PrimStepContext -> Machine
ty :: PrimStepContext -> Type
checkNaturalRange1 :: PrimStepContext -> Type -> Integer -> (Natural -> Natural) -> Term
checkNaturalRange2 :: PrimStepContext
-> Type
-> Integer
-> Integer
-> (Natural -> Natural -> Natural)
-> Term
checkNaturalRange :: PrimStepContext -> Type -> [Integer] -> ([Natural] -> Term) -> Term
reduce :: PrimStepContext -> Term -> Maybe Machine
reduceWith :: PrimStepContext -> Machine -> Term -> Maybe Machine
reduceWHNF :: PrimStepContext -> Term -> Maybe Machine
reduceWHNF' :: PrimStepContext -> Machine -> Term -> Maybe Machine
catchDivByZero :: PrimStepContext -> Term -> Term
catchErrorCall :: PrimStepContext -> Term -> Term
tcm :: TyConMap
isSubj :: Bool
pInfo :: PrimInfo
tys :: [Type]
args :: [Value]
mach :: Machine
ty :: Type
checkNaturalRange1 :: Type -> Integer -> (Natural -> Natural) -> Term
checkNaturalRange2 :: Type
-> Integer -> Integer -> (Natural -> Natural -> Natural) -> Term
checkNaturalRange :: Type -> [Integer] -> ([Natural] -> Term) -> Term
reduce :: Term -> Maybe Machine
reduceWith :: Machine -> Term -> Maybe Machine
reduceWHNF :: Term -> Maybe Machine
reduceWHNF' :: Machine -> Term -> Maybe Machine
catchDivByZero :: Term -> Term
catchErrorCall :: Term -> Term
..} | [(Integer
0,Integer
i),(Integer
0,Integer
j)] <- [Value] -> [(Integer, Integer)]
bitLiterals [Value]
args
        -> Term -> Maybe Machine
reduce (TyConMap -> Type -> Bool -> Term
boolToBoolLiteral TyConMap
tcm Type
ty (Integer
i Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
>  Integer
j))
      PrimStepContext
_ -> Maybe Machine
forall a. Maybe a
Nothing

  , Text -> (PrimStepContext -> Maybe Machine) -> (Text, PrimStep)
primStepEntry $(textNameLit 'Clash.Sized.Internal.BitVector.le##) ((PrimStepContext -> Maybe Machine) -> (Text, PrimStep))
-> (PrimStepContext -> Maybe Machine) -> (Text, PrimStep)
forall a b. (a -> b) -> a -> b
$ \case
      PrimStepContext{Bool
[Type]
[Value]
Type
TyConMap
Machine
PrimInfo
Term -> Maybe Machine
Term -> Term
Type
-> Integer -> Integer -> (Natural -> Natural -> Natural) -> Term
Type -> Integer -> (Natural -> Natural) -> Term
Type -> [Integer] -> ([Natural] -> Term) -> Term
Machine -> Term -> Maybe Machine
tcm :: PrimStepContext -> TyConMap
isSubj :: PrimStepContext -> Bool
pInfo :: PrimStepContext -> PrimInfo
tys :: PrimStepContext -> [Type]
args :: PrimStepContext -> [Value]
mach :: PrimStepContext -> Machine
ty :: PrimStepContext -> Type
checkNaturalRange1 :: PrimStepContext -> Type -> Integer -> (Natural -> Natural) -> Term
checkNaturalRange2 :: PrimStepContext
-> Type
-> Integer
-> Integer
-> (Natural -> Natural -> Natural)
-> Term
checkNaturalRange :: PrimStepContext -> Type -> [Integer] -> ([Natural] -> Term) -> Term
reduce :: PrimStepContext -> Term -> Maybe Machine
reduceWith :: PrimStepContext -> Machine -> Term -> Maybe Machine
reduceWHNF :: PrimStepContext -> Term -> Maybe Machine
reduceWHNF' :: PrimStepContext -> Machine -> Term -> Maybe Machine
catchDivByZero :: PrimStepContext -> Term -> Term
catchErrorCall :: PrimStepContext -> Term -> Term
tcm :: TyConMap
isSubj :: Bool
pInfo :: PrimInfo
tys :: [Type]
args :: [Value]
mach :: Machine
ty :: Type
checkNaturalRange1 :: Type -> Integer -> (Natural -> Natural) -> Term
checkNaturalRange2 :: Type
-> Integer -> Integer -> (Natural -> Natural -> Natural) -> Term
checkNaturalRange :: Type -> [Integer] -> ([Natural] -> Term) -> Term
reduce :: Term -> Maybe Machine
reduceWith :: Machine -> Term -> Maybe Machine
reduceWHNF :: Term -> Maybe Machine
reduceWHNF' :: Machine -> Term -> Maybe Machine
catchDivByZero :: Term -> Term
catchErrorCall :: Term -> Term
..} | [(Integer
0,Integer
i),(Integer
0,Integer
j)] <- [Value] -> [(Integer, Integer)]
bitLiterals [Value]
args
        -> Term -> Maybe Machine
reduce (TyConMap -> Type -> Bool -> Term
boolToBoolLiteral TyConMap
tcm Type
ty (Integer
i Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
<= Integer
j))
      PrimStepContext
_ -> Maybe Machine
forall a. Maybe a
Nothing


-- Enum
  , Text -> (PrimStepContext -> Maybe Machine) -> (Text, PrimStep)
primStepEntry $(textNameLit 'Clash.Sized.Internal.BitVector.toEnum##) ((PrimStepContext -> Maybe Machine) -> (Text, PrimStep))
-> (PrimStepContext -> Maybe Machine) -> (Text, PrimStep)
forall a b. (a -> b) -> a -> b
$ \case
      PrimStepContext{Bool
[Type]
[Value]
Type
TyConMap
Machine
PrimInfo
Term -> Maybe Machine
Term -> Term
Type
-> Integer -> Integer -> (Natural -> Natural -> Natural) -> Term
Type -> Integer -> (Natural -> Natural) -> Term
Type -> [Integer] -> ([Natural] -> Term) -> Term
Machine -> Term -> Maybe Machine
tcm :: PrimStepContext -> TyConMap
isSubj :: PrimStepContext -> Bool
pInfo :: PrimStepContext -> PrimInfo
tys :: PrimStepContext -> [Type]
args :: PrimStepContext -> [Value]
mach :: PrimStepContext -> Machine
ty :: PrimStepContext -> Type
checkNaturalRange1 :: PrimStepContext -> Type -> Integer -> (Natural -> Natural) -> Term
checkNaturalRange2 :: PrimStepContext
-> Type
-> Integer
-> Integer
-> (Natural -> Natural -> Natural)
-> Term
checkNaturalRange :: PrimStepContext -> Type -> [Integer] -> ([Natural] -> Term) -> Term
reduce :: PrimStepContext -> Term -> Maybe Machine
reduceWith :: PrimStepContext -> Machine -> Term -> Maybe Machine
reduceWHNF :: PrimStepContext -> Term -> Maybe Machine
reduceWHNF' :: PrimStepContext -> Machine -> Term -> Maybe Machine
catchDivByZero :: PrimStepContext -> Term -> Term
catchErrorCall :: PrimStepContext -> Term -> Term
tcm :: TyConMap
isSubj :: Bool
pInfo :: PrimInfo
tys :: [Type]
args :: [Value]
mach :: Machine
ty :: Type
checkNaturalRange1 :: Type -> Integer -> (Natural -> Natural) -> Term
checkNaturalRange2 :: Type
-> Integer -> Integer -> (Natural -> Natural -> Natural) -> Term
checkNaturalRange :: Type -> [Integer] -> ([Natural] -> Term) -> Term
reduce :: Term -> Maybe Machine
reduceWith :: Machine -> Term -> Maybe Machine
reduceWHNF :: Term -> Maybe Machine
reduceWHNF' :: Machine -> Term -> Maybe Machine
catchDivByZero :: Term -> Term
catchErrorCall :: Term -> Term
..}
        | [Integer
i] <- [Value] -> [Integer]
intCLiterals' [Value]
args
        -> let Bit Word
msk Word
val = Int -> Bit
BitVector.toEnum## (Integer -> Int
forall a. Num a => Integer -> a
fromInteger Integer
i)
           in Term -> Maybe Machine
reduce (Type -> Integer -> Integer -> Term
mkBitLit Type
ty (Word -> Integer
forall a. Integral a => a -> Integer
toInteger Word
msk) (Word -> Integer
forall a. Integral a => a -> Integer
toInteger Word
val))
      PrimStepContext
_ -> Maybe Machine
forall a. Maybe a
Nothing


-- Bits
  , Text -> (PrimStepContext -> Maybe Machine) -> (Text, PrimStep)
primStepEntry $(textNameLit 'Clash.Sized.Internal.BitVector.and##) ((PrimStepContext -> Maybe Machine) -> (Text, PrimStep))
-> (PrimStepContext -> Maybe Machine) -> (Text, PrimStep)
forall a b. (a -> b) -> a -> b
$ \case
      PrimStepContext{Bool
[Type]
[Value]
Type
TyConMap
Machine
PrimInfo
Term -> Maybe Machine
Term -> Term
Type
-> Integer -> Integer -> (Natural -> Natural -> Natural) -> Term
Type -> Integer -> (Natural -> Natural) -> Term
Type -> [Integer] -> ([Natural] -> Term) -> Term
Machine -> Term -> Maybe Machine
tcm :: PrimStepContext -> TyConMap
isSubj :: PrimStepContext -> Bool
pInfo :: PrimStepContext -> PrimInfo
tys :: PrimStepContext -> [Type]
args :: PrimStepContext -> [Value]
mach :: PrimStepContext -> Machine
ty :: PrimStepContext -> Type
checkNaturalRange1 :: PrimStepContext -> Type -> Integer -> (Natural -> Natural) -> Term
checkNaturalRange2 :: PrimStepContext
-> Type
-> Integer
-> Integer
-> (Natural -> Natural -> Natural)
-> Term
checkNaturalRange :: PrimStepContext -> Type -> [Integer] -> ([Natural] -> Term) -> Term
reduce :: PrimStepContext -> Term -> Maybe Machine
reduceWith :: PrimStepContext -> Machine -> Term -> Maybe Machine
reduceWHNF :: PrimStepContext -> Term -> Maybe Machine
reduceWHNF' :: PrimStepContext -> Machine -> Term -> Maybe Machine
catchDivByZero :: PrimStepContext -> Term -> Term
catchErrorCall :: PrimStepContext -> Term -> Term
tcm :: TyConMap
isSubj :: Bool
pInfo :: PrimInfo
tys :: [Type]
args :: [Value]
mach :: Machine
ty :: Type
checkNaturalRange1 :: Type -> Integer -> (Natural -> Natural) -> Term
checkNaturalRange2 :: Type
-> Integer -> Integer -> (Natural -> Natural -> Natural) -> Term
checkNaturalRange :: Type -> [Integer] -> ([Natural] -> Term) -> Term
reduce :: Term -> Maybe Machine
reduceWith :: Machine -> Term -> Maybe Machine
reduceWHNF :: Term -> Maybe Machine
reduceWHNF' :: Machine -> Term -> Maybe Machine
catchDivByZero :: Term -> Term
catchErrorCall :: Term -> Term
..}
        | [(Integer, Integer)
i,(Integer, Integer)
j] <- [Value] -> [(Integer, Integer)]
bitLiterals [Value]
args
        -> let Bit Word
msk Word
val = Bit -> Bit -> Bit
BitVector.and## ((Integer, Integer) -> Bit
toBit (Integer, Integer)
i) ((Integer, Integer) -> Bit
toBit (Integer, Integer)
j)
           in Term -> Maybe Machine
reduce (Type -> Integer -> Integer -> Term
mkBitLit Type
ty (Word -> Integer
forall a. Integral a => a -> Integer
toInteger Word
msk) (Word -> Integer
forall a. Integral a => a -> Integer
toInteger Word
val))
      PrimStepContext
_ -> Maybe Machine
forall a. Maybe a
Nothing

  , Text -> (PrimStepContext -> Maybe Machine) -> (Text, PrimStep)
primStepEntry $(textNameLit 'Clash.Sized.Internal.BitVector.or##) ((PrimStepContext -> Maybe Machine) -> (Text, PrimStep))
-> (PrimStepContext -> Maybe Machine) -> (Text, PrimStep)
forall a b. (a -> b) -> a -> b
$ \case
      PrimStepContext{Bool
[Type]
[Value]
Type
TyConMap
Machine
PrimInfo
Term -> Maybe Machine
Term -> Term
Type
-> Integer -> Integer -> (Natural -> Natural -> Natural) -> Term
Type -> Integer -> (Natural -> Natural) -> Term
Type -> [Integer] -> ([Natural] -> Term) -> Term
Machine -> Term -> Maybe Machine
tcm :: PrimStepContext -> TyConMap
isSubj :: PrimStepContext -> Bool
pInfo :: PrimStepContext -> PrimInfo
tys :: PrimStepContext -> [Type]
args :: PrimStepContext -> [Value]
mach :: PrimStepContext -> Machine
ty :: PrimStepContext -> Type
checkNaturalRange1 :: PrimStepContext -> Type -> Integer -> (Natural -> Natural) -> Term
checkNaturalRange2 :: PrimStepContext
-> Type
-> Integer
-> Integer
-> (Natural -> Natural -> Natural)
-> Term
checkNaturalRange :: PrimStepContext -> Type -> [Integer] -> ([Natural] -> Term) -> Term
reduce :: PrimStepContext -> Term -> Maybe Machine
reduceWith :: PrimStepContext -> Machine -> Term -> Maybe Machine
reduceWHNF :: PrimStepContext -> Term -> Maybe Machine
reduceWHNF' :: PrimStepContext -> Machine -> Term -> Maybe Machine
catchDivByZero :: PrimStepContext -> Term -> Term
catchErrorCall :: PrimStepContext -> Term -> Term
tcm :: TyConMap
isSubj :: Bool
pInfo :: PrimInfo
tys :: [Type]
args :: [Value]
mach :: Machine
ty :: Type
checkNaturalRange1 :: Type -> Integer -> (Natural -> Natural) -> Term
checkNaturalRange2 :: Type
-> Integer -> Integer -> (Natural -> Natural -> Natural) -> Term
checkNaturalRange :: Type -> [Integer] -> ([Natural] -> Term) -> Term
reduce :: Term -> Maybe Machine
reduceWith :: Machine -> Term -> Maybe Machine
reduceWHNF :: Term -> Maybe Machine
reduceWHNF' :: Machine -> Term -> Maybe Machine
catchDivByZero :: Term -> Term
catchErrorCall :: Term -> Term
..}
        | [(Integer, Integer)
i,(Integer, Integer)
j] <- [Value] -> [(Integer, Integer)]
bitLiterals [Value]
args
        -> let Bit Word
msk Word
val = Bit -> Bit -> Bit
BitVector.or## ((Integer, Integer) -> Bit
toBit (Integer, Integer)
i) ((Integer, Integer) -> Bit
toBit (Integer, Integer)
j)
           in Term -> Maybe Machine
reduce (Type -> Integer -> Integer -> Term
mkBitLit Type
ty (Word -> Integer
forall a. Integral a => a -> Integer
toInteger Word
msk) (Word -> Integer
forall a. Integral a => a -> Integer
toInteger Word
val))
      PrimStepContext
_ -> Maybe Machine
forall a. Maybe a
Nothing

  , Text -> (PrimStepContext -> Maybe Machine) -> (Text, PrimStep)
primStepEntry $(textNameLit 'Clash.Sized.Internal.BitVector.xor##) ((PrimStepContext -> Maybe Machine) -> (Text, PrimStep))
-> (PrimStepContext -> Maybe Machine) -> (Text, PrimStep)
forall a b. (a -> b) -> a -> b
$ \case
      PrimStepContext{Bool
[Type]
[Value]
Type
TyConMap
Machine
PrimInfo
Term -> Maybe Machine
Term -> Term
Type
-> Integer -> Integer -> (Natural -> Natural -> Natural) -> Term
Type -> Integer -> (Natural -> Natural) -> Term
Type -> [Integer] -> ([Natural] -> Term) -> Term
Machine -> Term -> Maybe Machine
tcm :: PrimStepContext -> TyConMap
isSubj :: PrimStepContext -> Bool
pInfo :: PrimStepContext -> PrimInfo
tys :: PrimStepContext -> [Type]
args :: PrimStepContext -> [Value]
mach :: PrimStepContext -> Machine
ty :: PrimStepContext -> Type
checkNaturalRange1 :: PrimStepContext -> Type -> Integer -> (Natural -> Natural) -> Term
checkNaturalRange2 :: PrimStepContext
-> Type
-> Integer
-> Integer
-> (Natural -> Natural -> Natural)
-> Term
checkNaturalRange :: PrimStepContext -> Type -> [Integer] -> ([Natural] -> Term) -> Term
reduce :: PrimStepContext -> Term -> Maybe Machine
reduceWith :: PrimStepContext -> Machine -> Term -> Maybe Machine
reduceWHNF :: PrimStepContext -> Term -> Maybe Machine
reduceWHNF' :: PrimStepContext -> Machine -> Term -> Maybe Machine
catchDivByZero :: PrimStepContext -> Term -> Term
catchErrorCall :: PrimStepContext -> Term -> Term
tcm :: TyConMap
isSubj :: Bool
pInfo :: PrimInfo
tys :: [Type]
args :: [Value]
mach :: Machine
ty :: Type
checkNaturalRange1 :: Type -> Integer -> (Natural -> Natural) -> Term
checkNaturalRange2 :: Type
-> Integer -> Integer -> (Natural -> Natural -> Natural) -> Term
checkNaturalRange :: Type -> [Integer] -> ([Natural] -> Term) -> Term
reduce :: Term -> Maybe Machine
reduceWith :: Machine -> Term -> Maybe Machine
reduceWHNF :: Term -> Maybe Machine
reduceWHNF' :: Machine -> Term -> Maybe Machine
catchDivByZero :: Term -> Term
catchErrorCall :: Term -> Term
..}
        | [(Integer, Integer)
i,(Integer, Integer)
j] <- [Value] -> [(Integer, Integer)]
bitLiterals [Value]
args
        -> let Bit Word
msk Word
val = Bit -> Bit -> Bit
BitVector.xor## ((Integer, Integer) -> Bit
toBit (Integer, Integer)
i) ((Integer, Integer) -> Bit
toBit (Integer, Integer)
j)
           in Term -> Maybe Machine
reduce (Type -> Integer -> Integer -> Term
mkBitLit Type
ty (Word -> Integer
forall a. Integral a => a -> Integer
toInteger Word
msk) (Word -> Integer
forall a. Integral a => a -> Integer
toInteger Word
val))
      PrimStepContext
_ -> Maybe Machine
forall a. Maybe a
Nothing

  , Text -> (PrimStepContext -> Maybe Machine) -> (Text, PrimStep)
primStepEntry $(textNameLit 'Clash.Sized.Internal.BitVector.complement##) ((PrimStepContext -> Maybe Machine) -> (Text, PrimStep))
-> (PrimStepContext -> Maybe Machine) -> (Text, PrimStep)
forall a b. (a -> b) -> a -> b
$ \case
      PrimStepContext{Bool
[Type]
[Value]
Type
TyConMap
Machine
PrimInfo
Term -> Maybe Machine
Term -> Term
Type
-> Integer -> Integer -> (Natural -> Natural -> Natural) -> Term
Type -> Integer -> (Natural -> Natural) -> Term
Type -> [Integer] -> ([Natural] -> Term) -> Term
Machine -> Term -> Maybe Machine
tcm :: PrimStepContext -> TyConMap
isSubj :: PrimStepContext -> Bool
pInfo :: PrimStepContext -> PrimInfo
tys :: PrimStepContext -> [Type]
args :: PrimStepContext -> [Value]
mach :: PrimStepContext -> Machine
ty :: PrimStepContext -> Type
checkNaturalRange1 :: PrimStepContext -> Type -> Integer -> (Natural -> Natural) -> Term
checkNaturalRange2 :: PrimStepContext
-> Type
-> Integer
-> Integer
-> (Natural -> Natural -> Natural)
-> Term
checkNaturalRange :: PrimStepContext -> Type -> [Integer] -> ([Natural] -> Term) -> Term
reduce :: PrimStepContext -> Term -> Maybe Machine
reduceWith :: PrimStepContext -> Machine -> Term -> Maybe Machine
reduceWHNF :: PrimStepContext -> Term -> Maybe Machine
reduceWHNF' :: PrimStepContext -> Machine -> Term -> Maybe Machine
catchDivByZero :: PrimStepContext -> Term -> Term
catchErrorCall :: PrimStepContext -> Term -> Term
tcm :: TyConMap
isSubj :: Bool
pInfo :: PrimInfo
tys :: [Type]
args :: [Value]
mach :: Machine
ty :: Type
checkNaturalRange1 :: Type -> Integer -> (Natural -> Natural) -> Term
checkNaturalRange2 :: Type
-> Integer -> Integer -> (Natural -> Natural -> Natural) -> Term
checkNaturalRange :: Type -> [Integer] -> ([Natural] -> Term) -> Term
reduce :: Term -> Maybe Machine
reduceWith :: Machine -> Term -> Maybe Machine
reduceWHNF :: Term -> Maybe Machine
reduceWHNF' :: Machine -> Term -> Maybe Machine
catchDivByZero :: Term -> Term
catchErrorCall :: Term -> Term
..}
        | [(Integer, Integer)
i] <- [Value] -> [(Integer, Integer)]
bitLiterals [Value]
args
        -> let Bit Word
msk Word
val = Bit -> Bit
BitVector.complement## ((Integer, Integer) -> Bit
toBit (Integer, Integer)
i)
           in Term -> Maybe Machine
reduce (Type -> Integer -> Integer -> Term
mkBitLit Type
ty (Word -> Integer
forall a. Integral a => a -> Integer
toInteger Word
msk) (Word -> Integer
forall a. Integral a => a -> Integer
toInteger Word
val))
      PrimStepContext
_ -> Maybe Machine
forall a. Maybe a
Nothing


-- Pack
  , Text -> (PrimStepContext -> Maybe Machine) -> (Text, PrimStep)
primStepEntry $(textNameLit 'Clash.Sized.Internal.BitVector.pack#) ((PrimStepContext -> Maybe Machine) -> (Text, PrimStep))
-> (PrimStepContext -> Maybe Machine) -> (Text, PrimStep)
forall a b. (a -> b) -> a -> b
$ \case
      PrimStepContext{Bool
[Type]
[Value]
Type
TyConMap
Machine
PrimInfo
Term -> Maybe Machine
Term -> Term
Type
-> Integer -> Integer -> (Natural -> Natural -> Natural) -> Term
Type -> Integer -> (Natural -> Natural) -> Term
Type -> [Integer] -> ([Natural] -> Term) -> Term
Machine -> Term -> Maybe Machine
tcm :: PrimStepContext -> TyConMap
isSubj :: PrimStepContext -> Bool
pInfo :: PrimStepContext -> PrimInfo
tys :: PrimStepContext -> [Type]
args :: PrimStepContext -> [Value]
mach :: PrimStepContext -> Machine
ty :: PrimStepContext -> Type
checkNaturalRange1 :: PrimStepContext -> Type -> Integer -> (Natural -> Natural) -> Term
checkNaturalRange2 :: PrimStepContext
-> Type
-> Integer
-> Integer
-> (Natural -> Natural -> Natural)
-> Term
checkNaturalRange :: PrimStepContext -> Type -> [Integer] -> ([Natural] -> Term) -> Term
reduce :: PrimStepContext -> Term -> Maybe Machine
reduceWith :: PrimStepContext -> Machine -> Term -> Maybe Machine
reduceWHNF :: PrimStepContext -> Term -> Maybe Machine
reduceWHNF' :: PrimStepContext -> Machine -> Term -> Maybe Machine
catchDivByZero :: PrimStepContext -> Term -> Term
catchErrorCall :: PrimStepContext -> Term -> Term
tcm :: TyConMap
isSubj :: Bool
pInfo :: PrimInfo
tys :: [Type]
args :: [Value]
mach :: Machine
ty :: Type
checkNaturalRange1 :: Type -> Integer -> (Natural -> Natural) -> Term
checkNaturalRange2 :: Type
-> Integer -> Integer -> (Natural -> Natural -> Natural) -> Term
checkNaturalRange :: Type -> [Integer] -> ([Natural] -> Term) -> Term
reduce :: Term -> Maybe Machine
reduceWith :: Machine -> Term -> Maybe Machine
reduceWHNF :: Term -> Maybe Machine
reduceWHNF' :: Machine -> Term -> Maybe Machine
catchDivByZero :: Term -> Term
catchErrorCall :: Term -> Term
..}
        | [(Integer
msk,Integer
i)] <- [Value] -> [(Integer, Integer)]
bitLiterals [Value]
args
        -> let resTyInfo :: (Type, Type, Integer)
resTyInfo = TyConMap -> Type -> [Type] -> (Type, Type, Integer)
extractTySizeInfo TyConMap
tcm Type
ty [Type]
tys
           in  Term -> Maybe Machine
reduce ((Type, Type, Integer) -> Integer -> Integer -> Term
mkBitVectorLit' (Type, Type, Integer)
resTyInfo Integer
msk Integer
i)
      PrimStepContext
_ -> Maybe Machine
forall a. Maybe a
Nothing

  , Text -> (PrimStepContext -> Maybe Machine) -> (Text, PrimStep)
primStepEntry $(textNameLit 'Clash.Sized.Internal.BitVector.unpack#) ((PrimStepContext -> Maybe Machine) -> (Text, PrimStep))
-> (PrimStepContext -> Maybe Machine) -> (Text, PrimStep)
forall a b. (a -> b) -> a -> b
$ \case
      PrimStepContext{Bool
[Type]
[Value]
Type
TyConMap
Machine
PrimInfo
Term -> Maybe Machine
Term -> Term
Type
-> Integer -> Integer -> (Natural -> Natural -> Natural) -> Term
Type -> Integer -> (Natural -> Natural) -> Term
Type -> [Integer] -> ([Natural] -> Term) -> Term
Machine -> Term -> Maybe Machine
tcm :: PrimStepContext -> TyConMap
isSubj :: PrimStepContext -> Bool
pInfo :: PrimStepContext -> PrimInfo
tys :: PrimStepContext -> [Type]
args :: PrimStepContext -> [Value]
mach :: PrimStepContext -> Machine
ty :: PrimStepContext -> Type
checkNaturalRange1 :: PrimStepContext -> Type -> Integer -> (Natural -> Natural) -> Term
checkNaturalRange2 :: PrimStepContext
-> Type
-> Integer
-> Integer
-> (Natural -> Natural -> Natural)
-> Term
checkNaturalRange :: PrimStepContext -> Type -> [Integer] -> ([Natural] -> Term) -> Term
reduce :: PrimStepContext -> Term -> Maybe Machine
reduceWith :: PrimStepContext -> Machine -> Term -> Maybe Machine
reduceWHNF :: PrimStepContext -> Term -> Maybe Machine
reduceWHNF' :: PrimStepContext -> Machine -> Term -> Maybe Machine
catchDivByZero :: PrimStepContext -> Term -> Term
catchErrorCall :: PrimStepContext -> Term -> Term
tcm :: TyConMap
isSubj :: Bool
pInfo :: PrimInfo
tys :: [Type]
args :: [Value]
mach :: Machine
ty :: Type
checkNaturalRange1 :: Type -> Integer -> (Natural -> Natural) -> Term
checkNaturalRange2 :: Type
-> Integer -> Integer -> (Natural -> Natural -> Natural) -> Term
checkNaturalRange :: Type -> [Integer] -> ([Natural] -> Term) -> Term
reduce :: Term -> Maybe Machine
reduceWith :: Machine -> Term -> Maybe Machine
reduceWHNF :: Term -> Maybe Machine
reduceWHNF' :: Machine -> Term -> Maybe Machine
catchDivByZero :: Term -> Term
catchErrorCall :: Term -> Term
..}
        | [(Integer
msk,Integer
i)] <- [Value] -> [(Integer, Integer)]
bitVectorLiterals' [Value]
args
        -> Term -> Maybe Machine
reduce (Type -> Integer -> Integer -> Term
mkBitLit Type
ty Integer
msk Integer
i)
      PrimStepContext
_ -> Maybe Machine
forall a. Maybe a
Nothing


-- Concatenation
  , Text -> (PrimStepContext -> Maybe Machine) -> (Text, PrimStep)
primStepEntry $(textNameLit '(Clash.Sized.Internal.BitVector.++#)) ((PrimStepContext -> Maybe Machine) -> (Text, PrimStep))
-> (PrimStepContext -> Maybe Machine) -> (Text, PrimStep)
forall a b. (a -> b) -> a -> b
$ \case
      PrimStepContext{Bool
[Type]
[Value]
Type
TyConMap
Machine
PrimInfo
Term -> Maybe Machine
Term -> Term
Type
-> Integer -> Integer -> (Natural -> Natural -> Natural) -> Term
Type -> Integer -> (Natural -> Natural) -> Term
Type -> [Integer] -> ([Natural] -> Term) -> Term
Machine -> Term -> Maybe Machine
tcm :: PrimStepContext -> TyConMap
isSubj :: PrimStepContext -> Bool
pInfo :: PrimStepContext -> PrimInfo
tys :: PrimStepContext -> [Type]
args :: PrimStepContext -> [Value]
mach :: PrimStepContext -> Machine
ty :: PrimStepContext -> Type
checkNaturalRange1 :: PrimStepContext -> Type -> Integer -> (Natural -> Natural) -> Term
checkNaturalRange2 :: PrimStepContext
-> Type
-> Integer
-> Integer
-> (Natural -> Natural -> Natural)
-> Term
checkNaturalRange :: PrimStepContext -> Type -> [Integer] -> ([Natural] -> Term) -> Term
reduce :: PrimStepContext -> Term -> Maybe Machine
reduceWith :: PrimStepContext -> Machine -> Term -> Maybe Machine
reduceWHNF :: PrimStepContext -> Term -> Maybe Machine
reduceWHNF' :: PrimStepContext -> Machine -> Term -> Maybe Machine
catchDivByZero :: PrimStepContext -> Term -> Term
catchErrorCall :: PrimStepContext -> Term -> Term
tcm :: TyConMap
isSubj :: Bool
pInfo :: PrimInfo
tys :: [Type]
args :: [Value]
mach :: Machine
ty :: Type
checkNaturalRange1 :: Type -> Integer -> (Natural -> Natural) -> Term
checkNaturalRange2 :: Type
-> Integer -> Integer -> (Natural -> Natural -> Natural) -> Term
checkNaturalRange :: Type -> [Integer] -> ([Natural] -> Term) -> Term
reduce :: Term -> Maybe Machine
reduceWith :: Machine -> Term -> Maybe Machine
reduceWHNF :: Term -> Maybe Machine
reduceWHNF' :: Machine -> Term -> Maybe Machine
catchDivByZero :: Term -> Term
catchErrorCall :: Term -> Term
..} -- :: KnownNat m => BitVector n -> BitVector m -> BitVector (n + m)
        | Just (Type
_,Integer
m) <- TyConMap -> [Type] -> Maybe (Type, Integer)
extractKnownNat TyConMap
tcm [Type]
tys
        , [(Integer
mski,Integer
i),(Integer
mskj,Integer
j)] <- [Value] -> [(Integer, Integer)]
bitVectorLiterals' [Value]
args
        -> let val :: Integer
val = Integer
i Integer -> Int -> Integer
forall a. Bits a => a -> Int -> a
`shiftL` Integer -> Int
forall a. Num a => Integer -> a
fromInteger Integer
m Integer -> Integer -> Integer
forall a. Bits a => a -> a -> a
.|. Integer
j
               msk :: Integer
msk = Integer
mski Integer -> Int -> Integer
forall a. Bits a => a -> Int -> a
`shiftL` Integer -> Int
forall a. Num a => Integer -> a
fromInteger Integer
m Integer -> Integer -> Integer
forall a. Bits a => a -> a -> a
.|. Integer
mskj
               resTyInfo :: (Type, Type, Integer)
resTyInfo = TyConMap -> Type -> [Type] -> (Type, Type, Integer)
extractTySizeInfo TyConMap
tcm Type
ty [Type]
tys
           in Term -> Maybe Machine
reduce ((Type, Type, Integer) -> Integer -> Integer -> Term
mkBitVectorLit' (Type, Type, Integer)
resTyInfo Integer
msk Integer
val)
      PrimStepContext
_ -> Maybe Machine
forall a. Maybe a
Nothing


-- Reduction
  , Text -> (PrimStepContext -> Maybe Machine) -> (Text, PrimStep)
primStepEntry $(textNameLit 'Clash.Sized.Internal.BitVector.reduceAnd#) ((PrimStepContext -> Maybe Machine) -> (Text, PrimStep))
-> (PrimStepContext -> Maybe Machine) -> (Text, PrimStep)
forall a b. (a -> b) -> a -> b
$ \case
      PrimStepContext{Bool
[Type]
[Value]
Type
TyConMap
Machine
PrimInfo
Term -> Maybe Machine
Term -> Term
Type
-> Integer -> Integer -> (Natural -> Natural -> Natural) -> Term
Type -> Integer -> (Natural -> Natural) -> Term
Type -> [Integer] -> ([Natural] -> Term) -> Term
Machine -> Term -> Maybe Machine
tcm :: PrimStepContext -> TyConMap
isSubj :: PrimStepContext -> Bool
pInfo :: PrimStepContext -> PrimInfo
tys :: PrimStepContext -> [Type]
args :: PrimStepContext -> [Value]
mach :: PrimStepContext -> Machine
ty :: PrimStepContext -> Type
checkNaturalRange1 :: PrimStepContext -> Type -> Integer -> (Natural -> Natural) -> Term
checkNaturalRange2 :: PrimStepContext
-> Type
-> Integer
-> Integer
-> (Natural -> Natural -> Natural)
-> Term
checkNaturalRange :: PrimStepContext -> Type -> [Integer] -> ([Natural] -> Term) -> Term
reduce :: PrimStepContext -> Term -> Maybe Machine
reduceWith :: PrimStepContext -> Machine -> Term -> Maybe Machine
reduceWHNF :: PrimStepContext -> Term -> Maybe Machine
reduceWHNF' :: PrimStepContext -> Machine -> Term -> Maybe Machine
catchDivByZero :: PrimStepContext -> Term -> Term
catchErrorCall :: PrimStepContext -> Term -> Term
tcm :: TyConMap
isSubj :: Bool
pInfo :: PrimInfo
tys :: [Type]
args :: [Value]
mach :: Machine
ty :: Type
checkNaturalRange1 :: Type -> Integer -> (Natural -> Natural) -> Term
checkNaturalRange2 :: Type
-> Integer -> Integer -> (Natural -> Natural -> Natural) -> Term
checkNaturalRange :: Type -> [Integer] -> ([Natural] -> Term) -> Term
reduce :: Term -> Maybe Machine
reduceWith :: Machine -> Term -> Maybe Machine
reduceWHNF :: Term -> Maybe Machine
reduceWHNF' :: Machine -> Term -> Maybe Machine
catchDivByZero :: Term -> Term
catchErrorCall :: Term -> Term
..} -- :: KnownNat n => BitVector n -> Bit
        | [(Integer, Integer)
i] <- [Value] -> [(Integer, Integer)]
bitVectorLiterals' [Value]
args
        , Just (Type
_, Integer
kn) <- TyConMap -> [Type] -> Maybe (Type, Integer)
extractKnownNat TyConMap
tcm [Type]
tys
        -> let resTy :: Type
resTy = TyConMap -> Type -> [Type] -> Type
getResultTy TyConMap
tcm Type
ty [Type]
tys
               val :: Integer
val = Integer
-> (forall (n :: Natural). KnownNat n => Proxy n -> Integer)
-> Integer
forall r.
Integer -> (forall (n :: Natural). KnownNat n => Proxy n -> r) -> r
reifyNat Integer
kn (BitVector n -> Proxy n -> Integer
forall (n :: Natural).
KnownNat n =>
BitVector n -> Proxy n -> Integer
op ((Integer, Integer) -> BitVector n
forall (n :: Natural). (Integer, Integer) -> BitVector n
toBV (Integer, Integer)
i))
           in Term -> Maybe Machine
reduce (Type -> Integer -> Integer -> Term
mkBitLit Type
resTy Integer
0 Integer
val)
        where
          op :: KnownNat n => BitVector n -> Proxy n -> Integer
          op :: forall (n :: Natural).
KnownNat n =>
BitVector n -> Proxy n -> Integer
op BitVector n
u Proxy n
_ = Bit -> Integer
forall a. Integral a => a -> Integer
toInteger (BitVector n -> Bit
forall (n :: Natural). KnownNat n => BitVector n -> Bit
BitVector.reduceAnd# BitVector n
u)
      PrimStepContext
_ -> Maybe Machine
forall a. Maybe a
Nothing

  , Text -> (PrimStepContext -> Maybe Machine) -> (Text, PrimStep)
primStepEntry $(textNameLit 'Clash.Sized.Internal.BitVector.reduceOr#) ((PrimStepContext -> Maybe Machine) -> (Text, PrimStep))
-> (PrimStepContext -> Maybe Machine) -> (Text, PrimStep)
forall a b. (a -> b) -> a -> b
$ \case
      PrimStepContext{Bool
[Type]
[Value]
Type
TyConMap
Machine
PrimInfo
Term -> Maybe Machine
Term -> Term
Type
-> Integer -> Integer -> (Natural -> Natural -> Natural) -> Term
Type -> Integer -> (Natural -> Natural) -> Term
Type -> [Integer] -> ([Natural] -> Term) -> Term
Machine -> Term -> Maybe Machine
tcm :: PrimStepContext -> TyConMap
isSubj :: PrimStepContext -> Bool
pInfo :: PrimStepContext -> PrimInfo
tys :: PrimStepContext -> [Type]
args :: PrimStepContext -> [Value]
mach :: PrimStepContext -> Machine
ty :: PrimStepContext -> Type
checkNaturalRange1 :: PrimStepContext -> Type -> Integer -> (Natural -> Natural) -> Term
checkNaturalRange2 :: PrimStepContext
-> Type
-> Integer
-> Integer
-> (Natural -> Natural -> Natural)
-> Term
checkNaturalRange :: PrimStepContext -> Type -> [Integer] -> ([Natural] -> Term) -> Term
reduce :: PrimStepContext -> Term -> Maybe Machine
reduceWith :: PrimStepContext -> Machine -> Term -> Maybe Machine
reduceWHNF :: PrimStepContext -> Term -> Maybe Machine
reduceWHNF' :: PrimStepContext -> Machine -> Term -> Maybe Machine
catchDivByZero :: PrimStepContext -> Term -> Term
catchErrorCall :: PrimStepContext -> Term -> Term
tcm :: TyConMap
isSubj :: Bool
pInfo :: PrimInfo
tys :: [Type]
args :: [Value]
mach :: Machine
ty :: Type
checkNaturalRange1 :: Type -> Integer -> (Natural -> Natural) -> Term
checkNaturalRange2 :: Type
-> Integer -> Integer -> (Natural -> Natural -> Natural) -> Term
checkNaturalRange :: Type -> [Integer] -> ([Natural] -> Term) -> Term
reduce :: Term -> Maybe Machine
reduceWith :: Machine -> Term -> Maybe Machine
reduceWHNF :: Term -> Maybe Machine
reduceWHNF' :: Machine -> Term -> Maybe Machine
catchDivByZero :: Term -> Term
catchErrorCall :: Term -> Term
..} -- :: KnownNat n => BitVector n -> Bit
        | [(Integer, Integer)
i] <- [Value] -> [(Integer, Integer)]
bitVectorLiterals' [Value]
args
        , Just (Type
_, Integer
kn) <- TyConMap -> [Type] -> Maybe (Type, Integer)
extractKnownNat TyConMap
tcm [Type]
tys
        -> let resTy :: Type
resTy = TyConMap -> Type -> [Type] -> Type
getResultTy TyConMap
tcm Type
ty [Type]
tys
               val :: Integer
val = Integer
-> (forall (n :: Natural). KnownNat n => Proxy n -> Integer)
-> Integer
forall r.
Integer -> (forall (n :: Natural). KnownNat n => Proxy n -> r) -> r
reifyNat Integer
kn (BitVector n -> Proxy n -> Integer
forall (n :: Natural).
KnownNat n =>
BitVector n -> Proxy n -> Integer
op ((Integer, Integer) -> BitVector n
forall (n :: Natural). (Integer, Integer) -> BitVector n
toBV (Integer, Integer)
i))
           in Term -> Maybe Machine
reduce (Type -> Integer -> Integer -> Term
mkBitLit Type
resTy Integer
0 Integer
val)
        where
          op :: KnownNat n => BitVector n -> Proxy n -> Integer
          op :: forall (n :: Natural).
KnownNat n =>
BitVector n -> Proxy n -> Integer
op BitVector n
u Proxy n
_ = Bit -> Integer
forall a. Integral a => a -> Integer
toInteger (BitVector n -> Bit
forall (n :: Natural). KnownNat n => BitVector n -> Bit
BitVector.reduceOr# BitVector n
u)
      PrimStepContext
_ -> Maybe Machine
forall a. Maybe a
Nothing

  , Text -> (PrimStepContext -> Maybe Machine) -> (Text, PrimStep)
primStepEntry $(textNameLit 'Clash.Sized.Internal.BitVector.reduceXor#) ((PrimStepContext -> Maybe Machine) -> (Text, PrimStep))
-> (PrimStepContext -> Maybe Machine) -> (Text, PrimStep)
forall a b. (a -> b) -> a -> b
$ \case
      PrimStepContext{Bool
[Type]
[Value]
Type
TyConMap
Machine
PrimInfo
Term -> Maybe Machine
Term -> Term
Type
-> Integer -> Integer -> (Natural -> Natural -> Natural) -> Term
Type -> Integer -> (Natural -> Natural) -> Term
Type -> [Integer] -> ([Natural] -> Term) -> Term
Machine -> Term -> Maybe Machine
tcm :: PrimStepContext -> TyConMap
isSubj :: PrimStepContext -> Bool
pInfo :: PrimStepContext -> PrimInfo
tys :: PrimStepContext -> [Type]
args :: PrimStepContext -> [Value]
mach :: PrimStepContext -> Machine
ty :: PrimStepContext -> Type
checkNaturalRange1 :: PrimStepContext -> Type -> Integer -> (Natural -> Natural) -> Term
checkNaturalRange2 :: PrimStepContext
-> Type
-> Integer
-> Integer
-> (Natural -> Natural -> Natural)
-> Term
checkNaturalRange :: PrimStepContext -> Type -> [Integer] -> ([Natural] -> Term) -> Term
reduce :: PrimStepContext -> Term -> Maybe Machine
reduceWith :: PrimStepContext -> Machine -> Term -> Maybe Machine
reduceWHNF :: PrimStepContext -> Term -> Maybe Machine
reduceWHNF' :: PrimStepContext -> Machine -> Term -> Maybe Machine
catchDivByZero :: PrimStepContext -> Term -> Term
catchErrorCall :: PrimStepContext -> Term -> Term
tcm :: TyConMap
isSubj :: Bool
pInfo :: PrimInfo
tys :: [Type]
args :: [Value]
mach :: Machine
ty :: Type
checkNaturalRange1 :: Type -> Integer -> (Natural -> Natural) -> Term
checkNaturalRange2 :: Type
-> Integer -> Integer -> (Natural -> Natural -> Natural) -> Term
checkNaturalRange :: Type -> [Integer] -> ([Natural] -> Term) -> Term
reduce :: Term -> Maybe Machine
reduceWith :: Machine -> Term -> Maybe Machine
reduceWHNF :: Term -> Maybe Machine
reduceWHNF' :: Machine -> Term -> Maybe Machine
catchDivByZero :: Term -> Term
catchErrorCall :: Term -> Term
..} -- :: KnownNat n => BitVector n -> Bit
        | [(Integer, Integer)
i] <- [Value] -> [(Integer, Integer)]
bitVectorLiterals' [Value]
args
        , Just (Type
_, Integer
kn) <- TyConMap -> [Type] -> Maybe (Type, Integer)
extractKnownNat TyConMap
tcm [Type]
tys
        -> let resTy :: Type
resTy = TyConMap -> Type -> [Type] -> Type
getResultTy TyConMap
tcm Type
ty [Type]
tys
               val :: Integer
val = Integer
-> (forall (n :: Natural). KnownNat n => Proxy n -> Integer)
-> Integer
forall r.
Integer -> (forall (n :: Natural). KnownNat n => Proxy n -> r) -> r
reifyNat Integer
kn (BitVector n -> Proxy n -> Integer
forall (n :: Natural).
KnownNat n =>
BitVector n -> Proxy n -> Integer
op ((Integer, Integer) -> BitVector n
forall (n :: Natural). (Integer, Integer) -> BitVector n
toBV (Integer, Integer)
i))
           in Term -> Maybe Machine
reduce (Type -> Integer -> Integer -> Term
mkBitLit Type
resTy Integer
0 Integer
val)
        where
          op :: KnownNat n => BitVector n -> Proxy n -> Integer
          op :: forall (n :: Natural).
KnownNat n =>
BitVector n -> Proxy n -> Integer
op BitVector n
u Proxy n
_ = Bit -> Integer
forall a. Integral a => a -> Integer
toInteger (BitVector n -> Bit
forall (n :: Natural). KnownNat n => BitVector n -> Bit
BitVector.reduceXor# BitVector n
u)
      PrimStepContext
_ -> Maybe Machine
forall a. Maybe a
Nothing



-- Indexing
  , Text -> (PrimStepContext -> Maybe Machine) -> (Text, PrimStep)
primStepEntry $(textNameLit 'Clash.Sized.Internal.BitVector.index#) ((PrimStepContext -> Maybe Machine) -> (Text, PrimStep))
-> (PrimStepContext -> Maybe Machine) -> (Text, PrimStep)
forall a b. (a -> b) -> a -> b
$ \case
      PrimStepContext{Bool
[Type]
[Value]
Type
TyConMap
Machine
PrimInfo
Term -> Maybe Machine
Term -> Term
Type
-> Integer -> Integer -> (Natural -> Natural -> Natural) -> Term
Type -> Integer -> (Natural -> Natural) -> Term
Type -> [Integer] -> ([Natural] -> Term) -> Term
Machine -> Term -> Maybe Machine
tcm :: PrimStepContext -> TyConMap
isSubj :: PrimStepContext -> Bool
pInfo :: PrimStepContext -> PrimInfo
tys :: PrimStepContext -> [Type]
args :: PrimStepContext -> [Value]
mach :: PrimStepContext -> Machine
ty :: PrimStepContext -> Type
checkNaturalRange1 :: PrimStepContext -> Type -> Integer -> (Natural -> Natural) -> Term
checkNaturalRange2 :: PrimStepContext
-> Type
-> Integer
-> Integer
-> (Natural -> Natural -> Natural)
-> Term
checkNaturalRange :: PrimStepContext -> Type -> [Integer] -> ([Natural] -> Term) -> Term
reduce :: PrimStepContext -> Term -> Maybe Machine
reduceWith :: PrimStepContext -> Machine -> Term -> Maybe Machine
reduceWHNF :: PrimStepContext -> Term -> Maybe Machine
reduceWHNF' :: PrimStepContext -> Machine -> Term -> Maybe Machine
catchDivByZero :: PrimStepContext -> Term -> Term
catchErrorCall :: PrimStepContext -> Term -> Term
tcm :: TyConMap
isSubj :: Bool
pInfo :: PrimInfo
tys :: [Type]
args :: [Value]
mach :: Machine
ty :: Type
checkNaturalRange1 :: Type -> Integer -> (Natural -> Natural) -> Term
checkNaturalRange2 :: Type
-> Integer -> Integer -> (Natural -> Natural -> Natural) -> Term
checkNaturalRange :: Type -> [Integer] -> ([Natural] -> Term) -> Term
reduce :: Term -> Maybe Machine
reduceWith :: Machine -> Term -> Maybe Machine
reduceWHNF :: Term -> Maybe Machine
reduceWHNF' :: Machine -> Term -> Maybe Machine
catchDivByZero :: Term -> Term
catchErrorCall :: Term -> Term
..} -- :: KnownNat n => BitVector n -> Int -> Bit
        | Just (Type
_,Integer
kn,(Integer, Integer)
i,Integer
j) <- TyConMap
-> [Type]
-> [Value]
-> Maybe (Type, Integer, (Integer, Integer), Integer)
bitVectorLitIntLit TyConMap
tcm [Type]
tys [Value]
args
          -> let resTy :: Type
resTy = TyConMap -> Type -> [Type] -> Type
getResultTy TyConMap
tcm Type
ty [Type]
tys
                 (Integer
msk,Integer
val) = Integer
-> (forall (n :: Natural).
    KnownNat n =>
    Proxy n -> (Integer, Integer))
-> (Integer, Integer)
forall r.
Integer -> (forall (n :: Natural). KnownNat n => Proxy n -> r) -> r
reifyNat Integer
kn (BitVector n -> Int -> Proxy n -> (Integer, Integer)
forall (n :: Natural).
KnownNat n =>
BitVector n -> Int -> Proxy n -> (Integer, Integer)
op ((Integer, Integer) -> BitVector n
forall (n :: Natural). (Integer, Integer) -> BitVector n
toBV (Integer, Integer)
i) (Integer -> Int
forall a. Num a => Integer -> a
fromInteger Integer
j))
             in Term -> Maybe Machine
reduce (Type -> Integer -> Integer -> Term
mkBitLit Type
resTy Integer
msk Integer
val)
          where
            op :: KnownNat n => BitVector n -> Int -> Proxy n -> (Integer,Integer)
            op :: forall (n :: Natural).
KnownNat n =>
BitVector n -> Int -> Proxy n -> (Integer, Integer)
op BitVector n
u Int
i Proxy n
_ = (Word -> Integer
forall a. Integral a => a -> Integer
toInteger Word
m, Word -> Integer
forall a. Integral a => a -> Integer
toInteger Word
v)
              where Bit Word
m Word
v = (BitVector n -> Int -> Bit
forall (n :: Natural). KnownNat n => BitVector n -> Int -> Bit
BitVector.index# BitVector n
u Int
i)
      PrimStepContext
_ -> Maybe Machine
forall a. Maybe a
Nothing

  , Text -> (PrimStepContext -> Maybe Machine) -> (Text, PrimStep)
primStepEntry $(textNameLit 'Clash.Sized.Internal.BitVector.replaceBit#) ((PrimStepContext -> Maybe Machine) -> (Text, PrimStep))
-> (PrimStepContext -> Maybe Machine) -> (Text, PrimStep)
forall a b. (a -> b) -> a -> b
$ \case
      PrimStepContext{Bool
[Type]
[Value]
Type
TyConMap
Machine
PrimInfo
Term -> Maybe Machine
Term -> Term
Type
-> Integer -> Integer -> (Natural -> Natural -> Natural) -> Term
Type -> Integer -> (Natural -> Natural) -> Term
Type -> [Integer] -> ([Natural] -> Term) -> Term
Machine -> Term -> Maybe Machine
tcm :: PrimStepContext -> TyConMap
isSubj :: PrimStepContext -> Bool
pInfo :: PrimStepContext -> PrimInfo
tys :: PrimStepContext -> [Type]
args :: PrimStepContext -> [Value]
mach :: PrimStepContext -> Machine
ty :: PrimStepContext -> Type
checkNaturalRange1 :: PrimStepContext -> Type -> Integer -> (Natural -> Natural) -> Term
checkNaturalRange2 :: PrimStepContext
-> Type
-> Integer
-> Integer
-> (Natural -> Natural -> Natural)
-> Term
checkNaturalRange :: PrimStepContext -> Type -> [Integer] -> ([Natural] -> Term) -> Term
reduce :: PrimStepContext -> Term -> Maybe Machine
reduceWith :: PrimStepContext -> Machine -> Term -> Maybe Machine
reduceWHNF :: PrimStepContext -> Term -> Maybe Machine
reduceWHNF' :: PrimStepContext -> Machine -> Term -> Maybe Machine
catchDivByZero :: PrimStepContext -> Term -> Term
catchErrorCall :: PrimStepContext -> Term -> Term
tcm :: TyConMap
isSubj :: Bool
pInfo :: PrimInfo
tys :: [Type]
args :: [Value]
mach :: Machine
ty :: Type
checkNaturalRange1 :: Type -> Integer -> (Natural -> Natural) -> Term
checkNaturalRange2 :: Type
-> Integer -> Integer -> (Natural -> Natural -> Natural) -> Term
checkNaturalRange :: Type -> [Integer] -> ([Natural] -> Term) -> Term
reduce :: Term -> Maybe Machine
reduceWith :: Machine -> Term -> Maybe Machine
reduceWHNF :: Term -> Maybe Machine
reduceWHNF' :: Machine -> Term -> Maybe Machine
catchDivByZero :: Term -> Term
catchErrorCall :: Term -> Term
..} -- :: :: KnownNat n => BitVector n -> Int -> Bit -> BitVector n
        | Just (Type
_, Integer
n) <- TyConMap -> [Type] -> Maybe (Type, Integer)
extractKnownNat TyConMap
tcm [Type]
tys
        , [ Value
_
          , PrimVal PrimInfo
bvP [Type]
_ [Value
_, Lit (NaturalLiteral Integer
mskBv), Lit (IntegerLiteral Integer
bv)]
          , Value -> Maybe [Term]
valArgs -> Just [Literal (IntLiteral Integer
i)]
          , PrimVal PrimInfo
bP [Type]
_ [Lit (WordLiteral Integer
mskB), Lit (IntegerLiteral Integer
b)]
          ] <- [Value]
args
        , PrimInfo -> Text
primName PrimInfo
bvP Text -> Text -> Bool
forall a. Eq a => a -> a -> Bool
== Name -> Text
forall a. Show a => a -> Text
showt 'Clash.Sized.Internal.BitVector.fromInteger#
        , PrimInfo -> Text
primName PrimInfo
bP  Text -> Text -> Bool
forall a. Eq a => a -> a -> Bool
== Name -> Text
forall a. Show a => a -> Text
showt 'Clash.Sized.Internal.BitVector.fromInteger##
          -> let resTyInfo :: (Type, Type, Integer)
resTyInfo = TyConMap -> Type -> [Type] -> (Type, Type, Integer)
extractTySizeInfo TyConMap
tcm Type
ty [Type]
tys
                 (Integer
mskVal,Integer
val) = Integer
-> (forall (n :: Natural).
    KnownNat n =>
    Proxy n -> (Integer, Integer))
-> (Integer, Integer)
forall r.
Integer -> (forall (n :: Natural). KnownNat n => Proxy n -> r) -> r
reifyNat Integer
n (BitVector n -> Int -> Bit -> Proxy n -> (Integer, Integer)
forall (n :: Natural).
KnownNat n =>
BitVector n -> Int -> Bit -> Proxy n -> (Integer, Integer)
op (Natural -> Natural -> BitVector n
forall (n :: Natural). Natural -> Natural -> BitVector n
BV (Integer -> Natural
forall a. Num a => Integer -> a
fromInteger Integer
mskBv) (Integer -> Natural
forall a. Num a => Integer -> a
fromInteger Integer
bv))
                                               (Integer -> Int
forall a. Num a => Integer -> a
fromInteger Integer
i)
                                               (Word -> Word -> Bit
Bit (Integer -> Word
forall a. Num a => Integer -> a
fromInteger Integer
mskB) (Integer -> Word
forall a. Num a => Integer -> a
fromInteger Integer
b)))
          in Term -> Maybe Machine
reduce ((Type, Type, Integer) -> Integer -> Integer -> Term
mkBitVectorLit' (Type, Type, Integer)
resTyInfo Integer
mskVal Integer
val)
          where
            op :: KnownNat n => BitVector n -> Int -> Bit -> Proxy n -> (Integer,Integer)
            -- op bv i b _ = (BitVector.unsafeMask res, BitVector.unsafeToInteger res)
            op :: forall (n :: Natural).
KnownNat n =>
BitVector n -> Int -> Bit -> Proxy n -> (Integer, Integer)
op BitVector n
bv Int
i Bit
b Proxy n
_ = BitVector n -> (Integer, Integer)
forall (n :: Natural). BitVector n -> (Integer, Integer)
splitBV (BitVector n -> Int -> Bit -> BitVector n
forall (n :: Natural).
KnownNat n =>
BitVector n -> Int -> Bit -> BitVector n
BitVector.replaceBit# BitVector n
bv Int
i Bit
b)
      PrimStepContext
_ -> Maybe Machine
forall a. Maybe a
Nothing

  , Text -> (PrimStepContext -> Maybe Machine) -> (Text, PrimStep)
primStepEntry $(textNameLit 'Clash.Sized.Internal.BitVector.setSlice#) ((PrimStepContext -> Maybe Machine) -> (Text, PrimStep))
-> (PrimStepContext -> Maybe Machine) -> (Text, PrimStep)
forall a b. (a -> b) -> a -> b
$ \case
      PrimStepContext{Bool
[Type]
[Value]
Type
TyConMap
Machine
PrimInfo
Term -> Maybe Machine
Term -> Term
Type
-> Integer -> Integer -> (Natural -> Natural -> Natural) -> Term
Type -> Integer -> (Natural -> Natural) -> Term
Type -> [Integer] -> ([Natural] -> Term) -> Term
Machine -> Term -> Maybe Machine
tcm :: PrimStepContext -> TyConMap
isSubj :: PrimStepContext -> Bool
pInfo :: PrimStepContext -> PrimInfo
tys :: PrimStepContext -> [Type]
args :: PrimStepContext -> [Value]
mach :: PrimStepContext -> Machine
ty :: PrimStepContext -> Type
checkNaturalRange1 :: PrimStepContext -> Type -> Integer -> (Natural -> Natural) -> Term
checkNaturalRange2 :: PrimStepContext
-> Type
-> Integer
-> Integer
-> (Natural -> Natural -> Natural)
-> Term
checkNaturalRange :: PrimStepContext -> Type -> [Integer] -> ([Natural] -> Term) -> Term
reduce :: PrimStepContext -> Term -> Maybe Machine
reduceWith :: PrimStepContext -> Machine -> Term -> Maybe Machine
reduceWHNF :: PrimStepContext -> Term -> Maybe Machine
reduceWHNF' :: PrimStepContext -> Machine -> Term -> Maybe Machine
catchDivByZero :: PrimStepContext -> Term -> Term
catchErrorCall :: PrimStepContext -> Term -> Term
tcm :: TyConMap
isSubj :: Bool
pInfo :: PrimInfo
tys :: [Type]
args :: [Value]
mach :: Machine
ty :: Type
checkNaturalRange1 :: Type -> Integer -> (Natural -> Natural) -> Term
checkNaturalRange2 :: Type
-> Integer -> Integer -> (Natural -> Natural -> Natural) -> Term
checkNaturalRange :: Type -> [Integer] -> ([Natural] -> Term) -> Term
reduce :: Term -> Maybe Machine
reduceWith :: Machine -> Term -> Maybe Machine
reduceWHNF :: Term -> Maybe Machine
reduceWHNF' :: Machine -> Term -> Maybe Machine
catchDivByZero :: Term -> Term
catchErrorCall :: Term -> Term
..}
      -- :: SNat (m+1+i) -> BitVector (m + 1 + i) -> SNat m -> SNat n -> BitVector (m + 1 - n) -> BitVector (m + 1 + i)
        | Type
mTy : Type
iTy : Type
nTy : [Type]
_ <- [Type]
tys
        , Right Integer
m <- Except String Integer -> Either String Integer
forall e a. Except e a -> Either e a
runExcept (TyConMap -> Type -> Except String Integer
tyNatSize TyConMap
tcm Type
mTy)
        , Right Integer
iN <- Except String Integer -> Either String Integer
forall e a. Except e a -> Either e a
runExcept (TyConMap -> Type -> Except String Integer
tyNatSize TyConMap
tcm Type
iTy)
        , Right Integer
n <- Except String Integer -> Either String Integer
forall e a. Except e a -> Either e a
runExcept (TyConMap -> Type -> Except String Integer
tyNatSize TyConMap
tcm Type
nTy)
        , [(Integer, Integer)
i,(Integer, Integer)
j] <- [Value] -> [(Integer, Integer)]
bitVectorLiterals' [Value]
args
        -> let BV Natural
msk Natural
val = SNat ((Any + 1) + Any)
-> BitVector ((Any + 1) + Any)
-> SNat Any
-> SNat Any
-> BitVector ((Any + 1) - Any)
-> BitVector ((Any + 1) + Any)
forall (m :: Natural) (i :: Natural) (n :: Natural).
SNat ((m + 1) + i)
-> BitVector ((m + 1) + i)
-> SNat m
-> SNat n
-> BitVector ((m + 1) - n)
-> BitVector ((m + 1) + i)
BitVector.setSlice# (Integer -> SNat ((Any + 1) + Any)
forall (k :: Natural). Integer -> SNat k
unsafeSNat (Integer
mInteger -> Integer -> Integer
forall a. Num a => a -> a -> a
+Integer
1Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
+Integer
iN)) ((Integer, Integer) -> BitVector ((Any + 1) + Any)
forall (n :: Natural). (Integer, Integer) -> BitVector n
toBV (Integer, Integer)
i) (Integer -> SNat Any
forall (k :: Natural). Integer -> SNat k
unsafeSNat Integer
m) (Integer -> SNat Any
forall (k :: Natural). Integer -> SNat k
unsafeSNat Integer
n) ((Integer, Integer) -> BitVector ((Any + 1) - Any)
forall (n :: Natural). (Integer, Integer) -> BitVector n
toBV (Integer, Integer)
j)
               resTyInfo :: (Type, Type, Integer)
resTyInfo = TyConMap -> Type -> [Type] -> (Type, Type, Integer)
extractTySizeInfo TyConMap
tcm Type
ty [Type]
tys
           in  Term -> Maybe Machine
reduce ((Type, Type, Integer) -> Integer -> Integer -> Term
mkBitVectorLit' (Type, Type, Integer)
resTyInfo (Natural -> Integer
forall a. Integral a => a -> Integer
toInteger Natural
msk) (Natural -> Integer
forall a. Integral a => a -> Integer
toInteger Natural
val))
      PrimStepContext
_ -> Maybe Machine
forall a. Maybe a
Nothing

  , Text -> (PrimStepContext -> Maybe Machine) -> (Text, PrimStep)
primStepEntry $(textNameLit 'Clash.Sized.Internal.BitVector.slice#) ((PrimStepContext -> Maybe Machine) -> (Text, PrimStep))
-> (PrimStepContext -> Maybe Machine) -> (Text, PrimStep)
forall a b. (a -> b) -> a -> b
$ \case
      PrimStepContext{Bool
[Type]
[Value]
Type
TyConMap
Machine
PrimInfo
Term -> Maybe Machine
Term -> Term
Type
-> Integer -> Integer -> (Natural -> Natural -> Natural) -> Term
Type -> Integer -> (Natural -> Natural) -> Term
Type -> [Integer] -> ([Natural] -> Term) -> Term
Machine -> Term -> Maybe Machine
tcm :: PrimStepContext -> TyConMap
isSubj :: PrimStepContext -> Bool
pInfo :: PrimStepContext -> PrimInfo
tys :: PrimStepContext -> [Type]
args :: PrimStepContext -> [Value]
mach :: PrimStepContext -> Machine
ty :: PrimStepContext -> Type
checkNaturalRange1 :: PrimStepContext -> Type -> Integer -> (Natural -> Natural) -> Term
checkNaturalRange2 :: PrimStepContext
-> Type
-> Integer
-> Integer
-> (Natural -> Natural -> Natural)
-> Term
checkNaturalRange :: PrimStepContext -> Type -> [Integer] -> ([Natural] -> Term) -> Term
reduce :: PrimStepContext -> Term -> Maybe Machine
reduceWith :: PrimStepContext -> Machine -> Term -> Maybe Machine
reduceWHNF :: PrimStepContext -> Term -> Maybe Machine
reduceWHNF' :: PrimStepContext -> Machine -> Term -> Maybe Machine
catchDivByZero :: PrimStepContext -> Term -> Term
catchErrorCall :: PrimStepContext -> Term -> Term
tcm :: TyConMap
isSubj :: Bool
pInfo :: PrimInfo
tys :: [Type]
args :: [Value]
mach :: Machine
ty :: Type
checkNaturalRange1 :: Type -> Integer -> (Natural -> Natural) -> Term
checkNaturalRange2 :: Type
-> Integer -> Integer -> (Natural -> Natural -> Natural) -> Term
checkNaturalRange :: Type -> [Integer] -> ([Natural] -> Term) -> Term
reduce :: Term -> Maybe Machine
reduceWith :: Machine -> Term -> Maybe Machine
reduceWHNF :: Term -> Maybe Machine
reduceWHNF' :: Machine -> Term -> Maybe Machine
catchDivByZero :: Term -> Term
catchErrorCall :: Term -> Term
..}
      -- :: BitVector (m + 1 + i) -> SNat m -> SNat n -> BitVector (m + 1 - n)
        | Type
mTy : Type
_ : Type
nTy : [Type]
_ <- [Type]
tys
        , Right Integer
m <- Except String Integer -> Either String Integer
forall e a. Except e a -> Either e a
runExcept (TyConMap -> Type -> Except String Integer
tyNatSize TyConMap
tcm Type
mTy)
        , Right Integer
n <- Except String Integer -> Either String Integer
forall e a. Except e a -> Either e a
runExcept (TyConMap -> Type -> Except String Integer
tyNatSize TyConMap
tcm Type
nTy)
        , [(Integer, Integer)
i] <- [Value] -> [(Integer, Integer)]
bitVectorLiterals' [Value]
args
        -> let BV Natural
msk Natural
val = BitVector ((Any + 1) + Any)
-> SNat Any -> SNat Any -> BitVector ((Any + 1) - Any)
forall (m :: Natural) (i :: Natural) (n :: Natural).
BitVector ((m + 1) + i)
-> SNat m -> SNat n -> BitVector ((m + 1) - n)
BitVector.slice# ((Integer, Integer) -> BitVector ((Any + 1) + Any)
forall (n :: Natural). (Integer, Integer) -> BitVector n
toBV (Integer, Integer)
i) (Integer -> SNat Any
forall (k :: Natural). Integer -> SNat k
unsafeSNat Integer
m) (Integer -> SNat Any
forall (k :: Natural). Integer -> SNat k
unsafeSNat Integer
n)
               resTyInfo :: (Type, Type, Integer)
resTyInfo = TyConMap -> Type -> [Type] -> (Type, Type, Integer)
extractTySizeInfo TyConMap
tcm Type
ty [Type]
tys
           in  Term -> Maybe Machine
reduce ((Type, Type, Integer) -> Integer -> Integer -> Term
mkBitVectorLit' (Type, Type, Integer)
resTyInfo (Natural -> Integer
forall a. Integral a => a -> Integer
toInteger Natural
msk) (Natural -> Integer
forall a. Integral a => a -> Integer
toInteger Natural
val))
      PrimStepContext
_ -> Maybe Machine
forall a. Maybe a
Nothing

  , Text -> (PrimStepContext -> Maybe Machine) -> (Text, PrimStep)
primStepEntry $(textNameLit 'Clash.Sized.Internal.BitVector.split#) ((PrimStepContext -> Maybe Machine) -> (Text, PrimStep))
-> (PrimStepContext -> Maybe Machine) -> (Text, PrimStep)
forall a b. (a -> b) -> a -> b
$ \case
      PrimStepContext{Bool
[Type]
[Value]
Type
TyConMap
Machine
PrimInfo
Term -> Maybe Machine
Term -> Term
Type
-> Integer -> Integer -> (Natural -> Natural -> Natural) -> Term
Type -> Integer -> (Natural -> Natural) -> Term
Type -> [Integer] -> ([Natural] -> Term) -> Term
Machine -> Term -> Maybe Machine
tcm :: PrimStepContext -> TyConMap
isSubj :: PrimStepContext -> Bool
pInfo :: PrimStepContext -> PrimInfo
tys :: PrimStepContext -> [Type]
args :: PrimStepContext -> [Value]
mach :: PrimStepContext -> Machine
ty :: PrimStepContext -> Type
checkNaturalRange1 :: PrimStepContext -> Type -> Integer -> (Natural -> Natural) -> Term
checkNaturalRange2 :: PrimStepContext
-> Type
-> Integer
-> Integer
-> (Natural -> Natural -> Natural)
-> Term
checkNaturalRange :: PrimStepContext -> Type -> [Integer] -> ([Natural] -> Term) -> Term
reduce :: PrimStepContext -> Term -> Maybe Machine
reduceWith :: PrimStepContext -> Machine -> Term -> Maybe Machine
reduceWHNF :: PrimStepContext -> Term -> Maybe Machine
reduceWHNF' :: PrimStepContext -> Machine -> Term -> Maybe Machine
catchDivByZero :: PrimStepContext -> Term -> Term
catchErrorCall :: PrimStepContext -> Term -> Term
tcm :: TyConMap
isSubj :: Bool
pInfo :: PrimInfo
tys :: [Type]
args :: [Value]
mach :: Machine
ty :: Type
checkNaturalRange1 :: Type -> Integer -> (Natural -> Natural) -> Term
checkNaturalRange2 :: Type
-> Integer -> Integer -> (Natural -> Natural -> Natural) -> Term
checkNaturalRange :: Type -> [Integer] -> ([Natural] -> Term) -> Term
reduce :: Term -> Maybe Machine
reduceWith :: Machine -> Term -> Maybe Machine
reduceWHNF :: Term -> Maybe Machine
reduceWHNF' :: Machine -> Term -> Maybe Machine
catchDivByZero :: Term -> Term
catchErrorCall :: Term -> Term
..} -- :: forall n m. KnownNat n => BitVector (m + n) -> (BitVector m, BitVector n)
        | Type
nTy : Type
mTy : [Type]
_ <- [Type]
tys
        , Right Integer
n <-  Except String Integer -> Either String Integer
forall e a. Except e a -> Either e a
runExcept (TyConMap -> Type -> Except String Integer
tyNatSize TyConMap
tcm Type
nTy)
        , Right Integer
m <-  Except String Integer -> Either String Integer
forall e a. Except e a -> Either e a
runExcept (TyConMap -> Type -> Except String Integer
tyNatSize TyConMap
tcm Type
mTy)
        , [(Integer
mski,Integer
i)] <- [Value] -> [(Integer, Integer)]
bitVectorLiterals' [Value]
args
        -> let ty' :: Type
ty' = HasCallStack => TyConMap -> Type -> [Type] -> Type
TyConMap -> Type -> [Type] -> Type
piResultTys TyConMap
tcm Type
ty [Type]
tys
               ([Either TyVar Type]
_,Type -> TypeView
tyView -> TyConApp TyConName
tupTcNm [Type]
tyArgs) = Type -> ([Either TyVar Type], Type)
splitFunForallTy Type
ty'
               (Just TyCon
tupTc) = TyConName -> TyConMap -> Maybe TyCon
forall a b. Uniquable a => a -> UniqMap b -> Maybe b
UniqMap.lookup TyConName
tupTcNm TyConMap
tcm
               [DataCon
tupDc] = TyCon -> [DataCon]
tyConDataCons TyCon
tupTc
               Type
bvTy : [Type]
_ = [Type]
tyArgs
               valM :: Integer
valM = Integer
i Integer -> Int -> Integer
forall a. Bits a => a -> Int -> a
`shiftR` Integer -> Int
forall a. Num a => Integer -> a
fromInteger Integer
n
               mskM :: Integer
mskM = Integer
mski Integer -> Int -> Integer
forall a. Bits a => a -> Int -> a
`shiftR` Integer -> Int
forall a. Num a => Integer -> a
fromInteger Integer
n
               valN :: Integer
valN = Integer
i Integer -> Integer -> Integer
forall a. Bits a => a -> a -> a
.&. Integer
mask
               mskN :: Integer
mskN = Integer
mski Integer -> Integer -> Integer
forall a. Bits a => a -> a -> a
.&. Integer
mask
               mask :: Integer
mask = Int -> Integer
forall a. Bits a => Int -> a
bit (Integer -> Int
forall a. Num a => Integer -> a
fromInteger Integer
n) Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
- Integer
1
        in Term -> Maybe Machine
reduce (Term -> Maybe Machine) -> Term -> Maybe Machine
forall a b. (a -> b) -> a -> b
$
           Term -> [Either Term Type] -> Term
mkApps (DataCon -> Term
Data DataCon
tupDc) ((Type -> Either Term Type) -> [Type] -> [Either Term Type]
forall a b. (a -> b) -> [a] -> [b]
map Type -> Either Term Type
forall a b. b -> Either a b
Right [Type]
tyArgs [Either Term Type] -> [Either Term Type] -> [Either Term Type]
forall a. [a] -> [a] -> [a]
++
                    [ Term -> Either Term Type
forall a b. a -> Either a b
Left (Type -> Type -> Integer -> Integer -> Integer -> Term
mkBitVectorLit Type
bvTy Type
mTy Integer
m Integer
mskM Integer
valM)
                    , Term -> Either Term Type
forall a b. a -> Either a b
Left (Type -> Type -> Integer -> Integer -> Integer -> Term
mkBitVectorLit Type
bvTy Type
nTy Integer
n Integer
mskN Integer
valN)])
      PrimStepContext
_ -> Maybe Machine
forall a. Maybe a
Nothing

  , Text -> (PrimStepContext -> Maybe Machine) -> (Text, PrimStep)
primStepEntry $(textNameLit 'Clash.Sized.Internal.BitVector.msb#) ((PrimStepContext -> Maybe Machine) -> (Text, PrimStep))
-> (PrimStepContext -> Maybe Machine) -> (Text, PrimStep)
forall a b. (a -> b) -> a -> b
$ \case
      PrimStepContext{Bool
[Type]
[Value]
Type
TyConMap
Machine
PrimInfo
Term -> Maybe Machine
Term -> Term
Type
-> Integer -> Integer -> (Natural -> Natural -> Natural) -> Term
Type -> Integer -> (Natural -> Natural) -> Term
Type -> [Integer] -> ([Natural] -> Term) -> Term
Machine -> Term -> Maybe Machine
tcm :: PrimStepContext -> TyConMap
isSubj :: PrimStepContext -> Bool
pInfo :: PrimStepContext -> PrimInfo
tys :: PrimStepContext -> [Type]
args :: PrimStepContext -> [Value]
mach :: PrimStepContext -> Machine
ty :: PrimStepContext -> Type
checkNaturalRange1 :: PrimStepContext -> Type -> Integer -> (Natural -> Natural) -> Term
checkNaturalRange2 :: PrimStepContext
-> Type
-> Integer
-> Integer
-> (Natural -> Natural -> Natural)
-> Term
checkNaturalRange :: PrimStepContext -> Type -> [Integer] -> ([Natural] -> Term) -> Term
reduce :: PrimStepContext -> Term -> Maybe Machine
reduceWith :: PrimStepContext -> Machine -> Term -> Maybe Machine
reduceWHNF :: PrimStepContext -> Term -> Maybe Machine
reduceWHNF' :: PrimStepContext -> Machine -> Term -> Maybe Machine
catchDivByZero :: PrimStepContext -> Term -> Term
catchErrorCall :: PrimStepContext -> Term -> Term
tcm :: TyConMap
isSubj :: Bool
pInfo :: PrimInfo
tys :: [Type]
args :: [Value]
mach :: Machine
ty :: Type
checkNaturalRange1 :: Type -> Integer -> (Natural -> Natural) -> Term
checkNaturalRange2 :: Type
-> Integer -> Integer -> (Natural -> Natural -> Natural) -> Term
checkNaturalRange :: Type -> [Integer] -> ([Natural] -> Term) -> Term
reduce :: Term -> Maybe Machine
reduceWith :: Machine -> Term -> Maybe Machine
reduceWHNF :: Term -> Maybe Machine
reduceWHNF' :: Machine -> Term -> Maybe Machine
catchDivByZero :: Term -> Term
catchErrorCall :: Term -> Term
..} -- :: forall n. KnownNat n => BitVector n -> Bit
        | [(Integer, Integer)
i] <- [Value] -> [(Integer, Integer)]
bitVectorLiterals' [Value]
args
        , Just (Type
_, Integer
kn) <- TyConMap -> [Type] -> Maybe (Type, Integer)
extractKnownNat TyConMap
tcm [Type]
tys
        -> let resTy :: Type
resTy = TyConMap -> Type -> [Type] -> Type
getResultTy TyConMap
tcm Type
ty [Type]
tys
               (Word
msk,Word
val) = Integer
-> (forall (n :: Natural). KnownNat n => Proxy n -> (Word, Word))
-> (Word, Word)
forall r.
Integer -> (forall (n :: Natural). KnownNat n => Proxy n -> r) -> r
reifyNat Integer
kn (BitVector n -> Proxy n -> (Word, Word)
forall (n :: Natural).
KnownNat n =>
BitVector n -> Proxy n -> (Word, Word)
op ((Integer, Integer) -> BitVector n
forall (n :: Natural). (Integer, Integer) -> BitVector n
toBV (Integer, Integer)
i))
           in Term -> Maybe Machine
reduce (Type -> Integer -> Integer -> Term
mkBitLit Type
resTy (Word -> Integer
forall a. Integral a => a -> Integer
toInteger Word
msk) (Word -> Integer
forall a. Integral a => a -> Integer
toInteger Word
val))
        where
          op :: KnownNat n => BitVector n -> Proxy n -> (Word,Word)
          op :: forall (n :: Natural).
KnownNat n =>
BitVector n -> Proxy n -> (Word, Word)
op BitVector n
u Proxy n
_ = (Bit -> Word
unsafeMask# Bit
res, Bit -> Word
BitVector.unsafeToInteger# Bit
res)
            where
              res :: Bit
res = BitVector n -> Bit
forall (n :: Natural). KnownNat n => BitVector n -> Bit
BitVector.msb# BitVector n
u
      PrimStepContext
_ -> Maybe Machine
forall a. Maybe a
Nothing

  , Text -> (PrimStepContext -> Maybe Machine) -> (Text, PrimStep)
primStepEntry $(textNameLit 'Clash.Sized.Internal.BitVector.lsb#) ((PrimStepContext -> Maybe Machine) -> (Text, PrimStep))
-> (PrimStepContext -> Maybe Machine) -> (Text, PrimStep)
forall a b. (a -> b) -> a -> b
$ \case
      PrimStepContext{Bool
[Type]
[Value]
Type
TyConMap
Machine
PrimInfo
Term -> Maybe Machine
Term -> Term
Type
-> Integer -> Integer -> (Natural -> Natural -> Natural) -> Term
Type -> Integer -> (Natural -> Natural) -> Term
Type -> [Integer] -> ([Natural] -> Term) -> Term
Machine -> Term -> Maybe Machine
tcm :: PrimStepContext -> TyConMap
isSubj :: PrimStepContext -> Bool
pInfo :: PrimStepContext -> PrimInfo
tys :: PrimStepContext -> [Type]
args :: PrimStepContext -> [Value]
mach :: PrimStepContext -> Machine
ty :: PrimStepContext -> Type
checkNaturalRange1 :: PrimStepContext -> Type -> Integer -> (Natural -> Natural) -> Term
checkNaturalRange2 :: PrimStepContext
-> Type
-> Integer
-> Integer
-> (Natural -> Natural -> Natural)
-> Term
checkNaturalRange :: PrimStepContext -> Type -> [Integer] -> ([Natural] -> Term) -> Term
reduce :: PrimStepContext -> Term -> Maybe Machine
reduceWith :: PrimStepContext -> Machine -> Term -> Maybe Machine
reduceWHNF :: PrimStepContext -> Term -> Maybe Machine
reduceWHNF' :: PrimStepContext -> Machine -> Term -> Maybe Machine
catchDivByZero :: PrimStepContext -> Term -> Term
catchErrorCall :: PrimStepContext -> Term -> Term
tcm :: TyConMap
isSubj :: Bool
pInfo :: PrimInfo
tys :: [Type]
args :: [Value]
mach :: Machine
ty :: Type
checkNaturalRange1 :: Type -> Integer -> (Natural -> Natural) -> Term
checkNaturalRange2 :: Type
-> Integer -> Integer -> (Natural -> Natural -> Natural) -> Term
checkNaturalRange :: Type -> [Integer] -> ([Natural] -> Term) -> Term
reduce :: Term -> Maybe Machine
reduceWith :: Machine -> Term -> Maybe Machine
reduceWHNF :: Term -> Maybe Machine
reduceWHNF' :: Machine -> Term -> Maybe Machine
catchDivByZero :: Term -> Term
catchErrorCall :: Term -> Term
..} -- :: BitVector n -> Bit
        | [(Integer, Integer)
i] <- [Value] -> [(Integer, Integer)]
bitVectorLiterals' [Value]
args
        -> let resTy :: Type
resTy = TyConMap -> Type -> [Type] -> Type
getResultTy TyConMap
tcm Type
ty [Type]
tys
               Bit Word
msk Word
val = BitVector Any -> Bit
forall (n :: Natural). BitVector n -> Bit
BitVector.lsb# ((Integer, Integer) -> BitVector Any
forall (n :: Natural). (Integer, Integer) -> BitVector n
toBV (Integer, Integer)
i)
        in Term -> Maybe Machine
reduce (Type -> Integer -> Integer -> Term
mkBitLit Type
resTy (Word -> Integer
forall a. Integral a => a -> Integer
toInteger Word
msk) (Word -> Integer
forall a. Integral a => a -> Integer
toInteger Word
val))
      PrimStepContext
_ -> Maybe Machine
forall a. Maybe a
Nothing



-- Eq
  -- eq#, neq# :: KnownNat n => BitVector n -> BitVector n -> Bool
  , Text -> (PrimStepContext -> Maybe Machine) -> (Text, PrimStep)
primStepEntry $(textNameLit 'Clash.Sized.Internal.BitVector.eq#) ((PrimStepContext -> Maybe Machine) -> (Text, PrimStep))
-> (PrimStepContext -> Maybe Machine) -> (Text, PrimStep)
forall a b. (a -> b) -> a -> b
$ \case
      PrimStepContext{Bool
[Type]
[Value]
Type
TyConMap
Machine
PrimInfo
Term -> Maybe Machine
Term -> Term
Type
-> Integer -> Integer -> (Natural -> Natural -> Natural) -> Term
Type -> Integer -> (Natural -> Natural) -> Term
Type -> [Integer] -> ([Natural] -> Term) -> Term
Machine -> Term -> Maybe Machine
tcm :: PrimStepContext -> TyConMap
isSubj :: PrimStepContext -> Bool
pInfo :: PrimStepContext -> PrimInfo
tys :: PrimStepContext -> [Type]
args :: PrimStepContext -> [Value]
mach :: PrimStepContext -> Machine
ty :: PrimStepContext -> Type
checkNaturalRange1 :: PrimStepContext -> Type -> Integer -> (Natural -> Natural) -> Term
checkNaturalRange2 :: PrimStepContext
-> Type
-> Integer
-> Integer
-> (Natural -> Natural -> Natural)
-> Term
checkNaturalRange :: PrimStepContext -> Type -> [Integer] -> ([Natural] -> Term) -> Term
reduce :: PrimStepContext -> Term -> Maybe Machine
reduceWith :: PrimStepContext -> Machine -> Term -> Maybe Machine
reduceWHNF :: PrimStepContext -> Term -> Maybe Machine
reduceWHNF' :: PrimStepContext -> Machine -> Term -> Maybe Machine
catchDivByZero :: PrimStepContext -> Term -> Term
catchErrorCall :: PrimStepContext -> Term -> Term
tcm :: TyConMap
isSubj :: Bool
pInfo :: PrimInfo
tys :: [Type]
args :: [Value]
mach :: Machine
ty :: Type
checkNaturalRange1 :: Type -> Integer -> (Natural -> Natural) -> Term
checkNaturalRange2 :: Type
-> Integer -> Integer -> (Natural -> Natural -> Natural) -> Term
checkNaturalRange :: Type -> [Integer] -> ([Natural] -> Term) -> Term
reduce :: Term -> Maybe Machine
reduceWith :: Machine -> Term -> Maybe Machine
reduceWHNF :: Term -> Maybe Machine
reduceWHNF' :: Machine -> Term -> Maybe Machine
catchDivByZero :: Term -> Term
catchErrorCall :: Term -> Term
..}
        | Type
nTy : [Type]
_ <- [Type]
tys
        , Right Integer
0 <- Except String Integer -> Either String Integer
forall e a. Except e a -> Either e a
runExcept (TyConMap -> Type -> Except String Integer
tyNatSize TyConMap
tcm Type
nTy)
        -> Term -> Maybe Machine
reduce (TyConMap -> Type -> Bool -> Term
boolToBoolLiteral TyConMap
tcm Type
ty Bool
True)
        | Just (Type
_, Integer
kn) <- TyConMap -> [Type] -> Maybe (Type, Integer)
extractKnownNat TyConMap
tcm [Type]
tys
        , Just Term
val <- Integer
-> (forall (n :: Natural). KnownNat n => Proxy n -> Maybe Term)
-> Maybe Term
forall r.
Integer -> (forall (n :: Natural). KnownNat n => Proxy n -> r) -> r
reifyNat Integer
kn ((BitVector n -> BitVector n -> Bool)
-> Type -> TyConMap -> [Value] -> Proxy n -> Maybe Term
forall (n :: Natural).
KnownNat n =>
(BitVector n -> BitVector n -> Bool)
-> Type -> TyConMap -> [Value] -> Proxy n -> Maybe Term
liftBitVector2Bool BitVector n -> BitVector n -> Bool
forall (n :: Natural).
KnownNat n =>
BitVector n -> BitVector n -> Bool
BitVector.eq# Type
ty TyConMap
tcm [Value]
args)
        -> Term -> Maybe Machine
reduce Term
val
      PrimStepContext
_ -> Maybe Machine
forall a. Maybe a
Nothing

  , Text -> (PrimStepContext -> Maybe Machine) -> (Text, PrimStep)
primStepEntry $(textNameLit 'Clash.Sized.Internal.BitVector.neq#) ((PrimStepContext -> Maybe Machine) -> (Text, PrimStep))
-> (PrimStepContext -> Maybe Machine) -> (Text, PrimStep)
forall a b. (a -> b) -> a -> b
$ \case
      PrimStepContext{Bool
[Type]
[Value]
Type
TyConMap
Machine
PrimInfo
Term -> Maybe Machine
Term -> Term
Type
-> Integer -> Integer -> (Natural -> Natural -> Natural) -> Term
Type -> Integer -> (Natural -> Natural) -> Term
Type -> [Integer] -> ([Natural] -> Term) -> Term
Machine -> Term -> Maybe Machine
tcm :: PrimStepContext -> TyConMap
isSubj :: PrimStepContext -> Bool
pInfo :: PrimStepContext -> PrimInfo
tys :: PrimStepContext -> [Type]
args :: PrimStepContext -> [Value]
mach :: PrimStepContext -> Machine
ty :: PrimStepContext -> Type
checkNaturalRange1 :: PrimStepContext -> Type -> Integer -> (Natural -> Natural) -> Term
checkNaturalRange2 :: PrimStepContext
-> Type
-> Integer
-> Integer
-> (Natural -> Natural -> Natural)
-> Term
checkNaturalRange :: PrimStepContext -> Type -> [Integer] -> ([Natural] -> Term) -> Term
reduce :: PrimStepContext -> Term -> Maybe Machine
reduceWith :: PrimStepContext -> Machine -> Term -> Maybe Machine
reduceWHNF :: PrimStepContext -> Term -> Maybe Machine
reduceWHNF' :: PrimStepContext -> Machine -> Term -> Maybe Machine
catchDivByZero :: PrimStepContext -> Term -> Term
catchErrorCall :: PrimStepContext -> Term -> Term
tcm :: TyConMap
isSubj :: Bool
pInfo :: PrimInfo
tys :: [Type]
args :: [Value]
mach :: Machine
ty :: Type
checkNaturalRange1 :: Type -> Integer -> (Natural -> Natural) -> Term
checkNaturalRange2 :: Type
-> Integer -> Integer -> (Natural -> Natural -> Natural) -> Term
checkNaturalRange :: Type -> [Integer] -> ([Natural] -> Term) -> Term
reduce :: Term -> Maybe Machine
reduceWith :: Machine -> Term -> Maybe Machine
reduceWHNF :: Term -> Maybe Machine
reduceWHNF' :: Machine -> Term -> Maybe Machine
catchDivByZero :: Term -> Term
catchErrorCall :: Term -> Term
..}
        | Type
nTy : [Type]
_ <- [Type]
tys
        , Right Integer
0 <- Except String Integer -> Either String Integer
forall e a. Except e a -> Either e a
runExcept (TyConMap -> Type -> Except String Integer
tyNatSize TyConMap
tcm Type
nTy)
        -> Term -> Maybe Machine
reduce (TyConMap -> Type -> Bool -> Term
boolToBoolLiteral TyConMap
tcm Type
ty Bool
False)
        | Just (Type
_, Integer
kn) <- TyConMap -> [Type] -> Maybe (Type, Integer)
extractKnownNat TyConMap
tcm [Type]
tys
        , Just Term
val <- Integer
-> (forall (n :: Natural). KnownNat n => Proxy n -> Maybe Term)
-> Maybe Term
forall r.
Integer -> (forall (n :: Natural). KnownNat n => Proxy n -> r) -> r
reifyNat Integer
kn ((BitVector n -> BitVector n -> Bool)
-> Type -> TyConMap -> [Value] -> Proxy n -> Maybe Term
forall (n :: Natural).
KnownNat n =>
(BitVector n -> BitVector n -> Bool)
-> Type -> TyConMap -> [Value] -> Proxy n -> Maybe Term
liftBitVector2Bool BitVector n -> BitVector n -> Bool
forall (n :: Natural).
KnownNat n =>
BitVector n -> BitVector n -> Bool
BitVector.neq# Type
ty TyConMap
tcm [Value]
args)
        -> Term -> Maybe Machine
reduce Term
val
      PrimStepContext
_ -> Maybe Machine
forall a. Maybe a
Nothing


-- Ord
  -- lt#,ge#,gt#,le# :: KnownNat n => BitVector n -> BitVector n -> Bool
  , Text -> (PrimStepContext -> Maybe Machine) -> (Text, PrimStep)
primStepEntry $(textNameLit 'Clash.Sized.Internal.BitVector.lt#) ((PrimStepContext -> Maybe Machine) -> (Text, PrimStep))
-> (PrimStepContext -> Maybe Machine) -> (Text, PrimStep)
forall a b. (a -> b) -> a -> b
$ \case
      PrimStepContext{Bool
[Type]
[Value]
Type
TyConMap
Machine
PrimInfo
Term -> Maybe Machine
Term -> Term
Type
-> Integer -> Integer -> (Natural -> Natural -> Natural) -> Term
Type -> Integer -> (Natural -> Natural) -> Term
Type -> [Integer] -> ([Natural] -> Term) -> Term
Machine -> Term -> Maybe Machine
tcm :: PrimStepContext -> TyConMap
isSubj :: PrimStepContext -> Bool
pInfo :: PrimStepContext -> PrimInfo
tys :: PrimStepContext -> [Type]
args :: PrimStepContext -> [Value]
mach :: PrimStepContext -> Machine
ty :: PrimStepContext -> Type
checkNaturalRange1 :: PrimStepContext -> Type -> Integer -> (Natural -> Natural) -> Term
checkNaturalRange2 :: PrimStepContext
-> Type
-> Integer
-> Integer
-> (Natural -> Natural -> Natural)
-> Term
checkNaturalRange :: PrimStepContext -> Type -> [Integer] -> ([Natural] -> Term) -> Term
reduce :: PrimStepContext -> Term -> Maybe Machine
reduceWith :: PrimStepContext -> Machine -> Term -> Maybe Machine
reduceWHNF :: PrimStepContext -> Term -> Maybe Machine
reduceWHNF' :: PrimStepContext -> Machine -> Term -> Maybe Machine
catchDivByZero :: PrimStepContext -> Term -> Term
catchErrorCall :: PrimStepContext -> Term -> Term
tcm :: TyConMap
isSubj :: Bool
pInfo :: PrimInfo
tys :: [Type]
args :: [Value]
mach :: Machine
ty :: Type
checkNaturalRange1 :: Type -> Integer -> (Natural -> Natural) -> Term
checkNaturalRange2 :: Type
-> Integer -> Integer -> (Natural -> Natural -> Natural) -> Term
checkNaturalRange :: Type -> [Integer] -> ([Natural] -> Term) -> Term
reduce :: Term -> Maybe Machine
reduceWith :: Machine -> Term -> Maybe Machine
reduceWHNF :: Term -> Maybe Machine
reduceWHNF' :: Machine -> Term -> Maybe Machine
catchDivByZero :: Term -> Term
catchErrorCall :: Term -> Term
..}
        | Type
nTy : [Type]
_ <- [Type]
tys
        , Right Integer
0 <- Except String Integer -> Either String Integer
forall e a. Except e a -> Either e a
runExcept (TyConMap -> Type -> Except String Integer
tyNatSize TyConMap
tcm Type
nTy)
        -> Term -> Maybe Machine
reduce (TyConMap -> Type -> Bool -> Term
boolToBoolLiteral TyConMap
tcm Type
ty Bool
False)
        | Just (Type
_, Integer
kn) <- TyConMap -> [Type] -> Maybe (Type, Integer)
extractKnownNat TyConMap
tcm [Type]
tys
        , Just Term
val <- Integer
-> (forall (n :: Natural). KnownNat n => Proxy n -> Maybe Term)
-> Maybe Term
forall r.
Integer -> (forall (n :: Natural). KnownNat n => Proxy n -> r) -> r
reifyNat Integer
kn ((BitVector n -> BitVector n -> Bool)
-> Type -> TyConMap -> [Value] -> Proxy n -> Maybe Term
forall (n :: Natural).
KnownNat n =>
(BitVector n -> BitVector n -> Bool)
-> Type -> TyConMap -> [Value] -> Proxy n -> Maybe Term
liftBitVector2Bool BitVector n -> BitVector n -> Bool
forall (n :: Natural).
KnownNat n =>
BitVector n -> BitVector n -> Bool
BitVector.lt# Type
ty TyConMap
tcm [Value]
args)
        -> Term -> Maybe Machine
reduce Term
val
      PrimStepContext
_ -> Maybe Machine
forall a. Maybe a
Nothing

  , Text -> (PrimStepContext -> Maybe Machine) -> (Text, PrimStep)
primStepEntry $(textNameLit 'Clash.Sized.Internal.BitVector.ge#) ((PrimStepContext -> Maybe Machine) -> (Text, PrimStep))
-> (PrimStepContext -> Maybe Machine) -> (Text, PrimStep)
forall a b. (a -> b) -> a -> b
$ \case
      PrimStepContext{Bool
[Type]
[Value]
Type
TyConMap
Machine
PrimInfo
Term -> Maybe Machine
Term -> Term
Type
-> Integer -> Integer -> (Natural -> Natural -> Natural) -> Term
Type -> Integer -> (Natural -> Natural) -> Term
Type -> [Integer] -> ([Natural] -> Term) -> Term
Machine -> Term -> Maybe Machine
tcm :: PrimStepContext -> TyConMap
isSubj :: PrimStepContext -> Bool
pInfo :: PrimStepContext -> PrimInfo
tys :: PrimStepContext -> [Type]
args :: PrimStepContext -> [Value]
mach :: PrimStepContext -> Machine
ty :: PrimStepContext -> Type
checkNaturalRange1 :: PrimStepContext -> Type -> Integer -> (Natural -> Natural) -> Term
checkNaturalRange2 :: PrimStepContext
-> Type
-> Integer
-> Integer
-> (Natural -> Natural -> Natural)
-> Term
checkNaturalRange :: PrimStepContext -> Type -> [Integer] -> ([Natural] -> Term) -> Term
reduce :: PrimStepContext -> Term -> Maybe Machine
reduceWith :: PrimStepContext -> Machine -> Term -> Maybe Machine
reduceWHNF :: PrimStepContext -> Term -> Maybe Machine
reduceWHNF' :: PrimStepContext -> Machine -> Term -> Maybe Machine
catchDivByZero :: PrimStepContext -> Term -> Term
catchErrorCall :: PrimStepContext -> Term -> Term
tcm :: TyConMap
isSubj :: Bool
pInfo :: PrimInfo
tys :: [Type]
args :: [Value]
mach :: Machine
ty :: Type
checkNaturalRange1 :: Type -> Integer -> (Natural -> Natural) -> Term
checkNaturalRange2 :: Type
-> Integer -> Integer -> (Natural -> Natural -> Natural) -> Term
checkNaturalRange :: Type -> [Integer] -> ([Natural] -> Term) -> Term
reduce :: Term -> Maybe Machine
reduceWith :: Machine -> Term -> Maybe Machine
reduceWHNF :: Term -> Maybe Machine
reduceWHNF' :: Machine -> Term -> Maybe Machine
catchDivByZero :: Term -> Term
catchErrorCall :: Term -> Term
..}
        | Type
nTy : [Type]
_ <- [Type]
tys
        , Right Integer
0 <- Except String Integer -> Either String Integer
forall e a. Except e a -> Either e a
runExcept (TyConMap -> Type -> Except String Integer
tyNatSize TyConMap
tcm Type
nTy)
        -> Term -> Maybe Machine
reduce (TyConMap -> Type -> Bool -> Term
boolToBoolLiteral TyConMap
tcm Type
ty Bool
True)
        | Just (Type
_, Integer
kn) <- TyConMap -> [Type] -> Maybe (Type, Integer)
extractKnownNat TyConMap
tcm [Type]
tys
        , Just Term
val <- Integer
-> (forall (n :: Natural). KnownNat n => Proxy n -> Maybe Term)
-> Maybe Term
forall r.
Integer -> (forall (n :: Natural). KnownNat n => Proxy n -> r) -> r
reifyNat Integer
kn ((BitVector n -> BitVector n -> Bool)
-> Type -> TyConMap -> [Value] -> Proxy n -> Maybe Term
forall (n :: Natural).
KnownNat n =>
(BitVector n -> BitVector n -> Bool)
-> Type -> TyConMap -> [Value] -> Proxy n -> Maybe Term
liftBitVector2Bool BitVector n -> BitVector n -> Bool
forall (n :: Natural).
KnownNat n =>
BitVector n -> BitVector n -> Bool
BitVector.ge# Type
ty TyConMap
tcm [Value]
args)
        -> Term -> Maybe Machine
reduce Term
val
      PrimStepContext
_ -> Maybe Machine
forall a. Maybe a
Nothing

  , Text -> (PrimStepContext -> Maybe Machine) -> (Text, PrimStep)
primStepEntry $(textNameLit 'Clash.Sized.Internal.BitVector.gt#) ((PrimStepContext -> Maybe Machine) -> (Text, PrimStep))
-> (PrimStepContext -> Maybe Machine) -> (Text, PrimStep)
forall a b. (a -> b) -> a -> b
$ \case
      PrimStepContext{Bool
[Type]
[Value]
Type
TyConMap
Machine
PrimInfo
Term -> Maybe Machine
Term -> Term
Type
-> Integer -> Integer -> (Natural -> Natural -> Natural) -> Term
Type -> Integer -> (Natural -> Natural) -> Term
Type -> [Integer] -> ([Natural] -> Term) -> Term
Machine -> Term -> Maybe Machine
tcm :: PrimStepContext -> TyConMap
isSubj :: PrimStepContext -> Bool
pInfo :: PrimStepContext -> PrimInfo
tys :: PrimStepContext -> [Type]
args :: PrimStepContext -> [Value]
mach :: PrimStepContext -> Machine
ty :: PrimStepContext -> Type
checkNaturalRange1 :: PrimStepContext -> Type -> Integer -> (Natural -> Natural) -> Term
checkNaturalRange2 :: PrimStepContext
-> Type
-> Integer
-> Integer
-> (Natural -> Natural -> Natural)
-> Term
checkNaturalRange :: PrimStepContext -> Type -> [Integer] -> ([Natural] -> Term) -> Term
reduce :: PrimStepContext -> Term -> Maybe Machine
reduceWith :: PrimStepContext -> Machine -> Term -> Maybe Machine
reduceWHNF :: PrimStepContext -> Term -> Maybe Machine
reduceWHNF' :: PrimStepContext -> Machine -> Term -> Maybe Machine
catchDivByZero :: PrimStepContext -> Term -> Term
catchErrorCall :: PrimStepContext -> Term -> Term
tcm :: TyConMap
isSubj :: Bool
pInfo :: PrimInfo
tys :: [Type]
args :: [Value]
mach :: Machine
ty :: Type
checkNaturalRange1 :: Type -> Integer -> (Natural -> Natural) -> Term
checkNaturalRange2 :: Type
-> Integer -> Integer -> (Natural -> Natural -> Natural) -> Term
checkNaturalRange :: Type -> [Integer] -> ([Natural] -> Term) -> Term
reduce :: Term -> Maybe Machine
reduceWith :: Machine -> Term -> Maybe Machine
reduceWHNF :: Term -> Maybe Machine
reduceWHNF' :: Machine -> Term -> Maybe Machine
catchDivByZero :: Term -> Term
catchErrorCall :: Term -> Term
..}
        | Type
nTy : [Type]
_ <- [Type]
tys
        , Right Integer
0 <- Except String Integer -> Either String Integer
forall e a. Except e a -> Either e a
runExcept (TyConMap -> Type -> Except String Integer
tyNatSize TyConMap
tcm Type
nTy)
        -> Term -> Maybe Machine
reduce (TyConMap -> Type -> Bool -> Term
boolToBoolLiteral TyConMap
tcm Type
ty Bool
False)
        | Just (Type
_, Integer
kn) <- TyConMap -> [Type] -> Maybe (Type, Integer)
extractKnownNat TyConMap
tcm [Type]
tys
        , Just Term
val <- Integer
-> (forall (n :: Natural). KnownNat n => Proxy n -> Maybe Term)
-> Maybe Term
forall r.
Integer -> (forall (n :: Natural). KnownNat n => Proxy n -> r) -> r
reifyNat Integer
kn ((BitVector n -> BitVector n -> Bool)
-> Type -> TyConMap -> [Value] -> Proxy n -> Maybe Term
forall (n :: Natural).
KnownNat n =>
(BitVector n -> BitVector n -> Bool)
-> Type -> TyConMap -> [Value] -> Proxy n -> Maybe Term
liftBitVector2Bool BitVector n -> BitVector n -> Bool
forall (n :: Natural).
KnownNat n =>
BitVector n -> BitVector n -> Bool
BitVector.gt# Type
ty TyConMap
tcm [Value]
args)
        -> Term -> Maybe Machine
reduce Term
val
      PrimStepContext
_ -> Maybe Machine
forall a. Maybe a
Nothing

  , Text -> (PrimStepContext -> Maybe Machine) -> (Text, PrimStep)
primStepEntry $(textNameLit 'Clash.Sized.Internal.BitVector.le#) ((PrimStepContext -> Maybe Machine) -> (Text, PrimStep))
-> (PrimStepContext -> Maybe Machine) -> (Text, PrimStep)
forall a b. (a -> b) -> a -> b
$ \case
      PrimStepContext{Bool
[Type]
[Value]
Type
TyConMap
Machine
PrimInfo
Term -> Maybe Machine
Term -> Term
Type
-> Integer -> Integer -> (Natural -> Natural -> Natural) -> Term
Type -> Integer -> (Natural -> Natural) -> Term
Type -> [Integer] -> ([Natural] -> Term) -> Term
Machine -> Term -> Maybe Machine
tcm :: PrimStepContext -> TyConMap
isSubj :: PrimStepContext -> Bool
pInfo :: PrimStepContext -> PrimInfo
tys :: PrimStepContext -> [Type]
args :: PrimStepContext -> [Value]
mach :: PrimStepContext -> Machine
ty :: PrimStepContext -> Type
checkNaturalRange1 :: PrimStepContext -> Type -> Integer -> (Natural -> Natural) -> Term
checkNaturalRange2 :: PrimStepContext
-> Type
-> Integer
-> Integer
-> (Natural -> Natural -> Natural)
-> Term
checkNaturalRange :: PrimStepContext -> Type -> [Integer] -> ([Natural] -> Term) -> Term
reduce :: PrimStepContext -> Term -> Maybe Machine
reduceWith :: PrimStepContext -> Machine -> Term -> Maybe Machine
reduceWHNF :: PrimStepContext -> Term -> Maybe Machine
reduceWHNF' :: PrimStepContext -> Machine -> Term -> Maybe Machine
catchDivByZero :: PrimStepContext -> Term -> Term
catchErrorCall :: PrimStepContext -> Term -> Term
tcm :: TyConMap
isSubj :: Bool
pInfo :: PrimInfo
tys :: [Type]
args :: [Value]
mach :: Machine
ty :: Type
checkNaturalRange1 :: Type -> Integer -> (Natural -> Natural) -> Term
checkNaturalRange2 :: Type
-> Integer -> Integer -> (Natural -> Natural -> Natural) -> Term
checkNaturalRange :: Type -> [Integer] -> ([Natural] -> Term) -> Term
reduce :: Term -> Maybe Machine
reduceWith :: Machine -> Term -> Maybe Machine
reduceWHNF :: Term -> Maybe Machine
reduceWHNF' :: Machine -> Term -> Maybe Machine
catchDivByZero :: Term -> Term
catchErrorCall :: Term -> Term
..}
        | Type
nTy : [Type]
_ <- [Type]
tys
        , Right Integer
0 <- Except String Integer -> Either String Integer
forall e a. Except e a -> Either e a
runExcept (TyConMap -> Type -> Except String Integer
tyNatSize TyConMap
tcm Type
nTy)
        -> Term -> Maybe Machine
reduce (TyConMap -> Type -> Bool -> Term
boolToBoolLiteral TyConMap
tcm Type
ty Bool
True)
        | Just (Type
_, Integer
kn) <- TyConMap -> [Type] -> Maybe (Type, Integer)
extractKnownNat TyConMap
tcm [Type]
tys
        , Just Term
val <- Integer
-> (forall (n :: Natural). KnownNat n => Proxy n -> Maybe Term)
-> Maybe Term
forall r.
Integer -> (forall (n :: Natural). KnownNat n => Proxy n -> r) -> r
reifyNat Integer
kn ((BitVector n -> BitVector n -> Bool)
-> Type -> TyConMap -> [Value] -> Proxy n -> Maybe Term
forall (n :: Natural).
KnownNat n =>
(BitVector n -> BitVector n -> Bool)
-> Type -> TyConMap -> [Value] -> Proxy n -> Maybe Term
liftBitVector2Bool BitVector n -> BitVector n -> Bool
forall (n :: Natural).
KnownNat n =>
BitVector n -> BitVector n -> Bool
BitVector.le# Type
ty TyConMap
tcm [Value]
args)
        -> Term -> Maybe Machine
reduce Term
val
      PrimStepContext
_ -> Maybe Machine
forall a. Maybe a
Nothing


-- Enum

  , Text -> (PrimStepContext -> Maybe Machine) -> (Text, PrimStep)
primStepEntry $(textNameLit 'Clash.Sized.Internal.BitVector.toEnum#) ((PrimStepContext -> Maybe Machine) -> (Text, PrimStep))
-> (PrimStepContext -> Maybe Machine) -> (Text, PrimStep)
forall a b. (a -> b) -> a -> b
$ \case
      PrimStepContext{Bool
[Type]
[Value]
Type
TyConMap
Machine
PrimInfo
Term -> Maybe Machine
Term -> Term
Type
-> Integer -> Integer -> (Natural -> Natural -> Natural) -> Term
Type -> Integer -> (Natural -> Natural) -> Term
Type -> [Integer] -> ([Natural] -> Term) -> Term
Machine -> Term -> Maybe Machine
tcm :: PrimStepContext -> TyConMap
isSubj :: PrimStepContext -> Bool
pInfo :: PrimStepContext -> PrimInfo
tys :: PrimStepContext -> [Type]
args :: PrimStepContext -> [Value]
mach :: PrimStepContext -> Machine
ty :: PrimStepContext -> Type
checkNaturalRange1 :: PrimStepContext -> Type -> Integer -> (Natural -> Natural) -> Term
checkNaturalRange2 :: PrimStepContext
-> Type
-> Integer
-> Integer
-> (Natural -> Natural -> Natural)
-> Term
checkNaturalRange :: PrimStepContext -> Type -> [Integer] -> ([Natural] -> Term) -> Term
reduce :: PrimStepContext -> Term -> Maybe Machine
reduceWith :: PrimStepContext -> Machine -> Term -> Maybe Machine
reduceWHNF :: PrimStepContext -> Term -> Maybe Machine
reduceWHNF' :: PrimStepContext -> Machine -> Term -> Maybe Machine
catchDivByZero :: PrimStepContext -> Term -> Term
catchErrorCall :: PrimStepContext -> Term -> Term
tcm :: TyConMap
isSubj :: Bool
pInfo :: PrimInfo
tys :: [Type]
args :: [Value]
mach :: Machine
ty :: Type
checkNaturalRange1 :: Type -> Integer -> (Natural -> Natural) -> Term
checkNaturalRange2 :: Type
-> Integer -> Integer -> (Natural -> Natural -> Natural) -> Term
checkNaturalRange :: Type -> [Integer] -> ([Natural] -> Term) -> Term
reduce :: Term -> Maybe Machine
reduceWith :: Machine -> Term -> Maybe Machine
reduceWHNF :: Term -> Maybe Machine
reduceWHNF' :: Machine -> Term -> Maybe Machine
catchDivByZero :: Term -> Term
catchErrorCall :: Term -> Term
..}
        | let resTyInfo :: (Type, Type, Integer)
resTyInfo@(Type
_,Type
_,Integer
kn) = TyConMap -> Type -> [Type] -> (Type, Type, Integer)
extractTySizeInfo TyConMap
tcm Type
ty [Type]
tys
        , Just Term
val <- Integer
-> (forall (n :: Natural). KnownNat n => Proxy n -> Maybe Term)
-> Maybe Term
forall r.
Integer -> (forall (n :: Natural). KnownNat n => Proxy n -> r) -> r
reifyNat Integer
kn ((Integer -> BitVector n)
-> (Type, Type, Integer) -> [Value] -> Proxy n -> Maybe Term
forall (n :: Natural).
KnownNat n =>
(Integer -> BitVector n)
-> (Type, Type, Integer) -> [Value] -> Proxy n -> Maybe Term
liftInteger2BitVector (Int -> BitVector n
forall (n :: Natural). KnownNat n => Int -> BitVector n
BitVector.toEnum# (Int -> BitVector n) -> (Integer -> Int) -> Integer -> BitVector n
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Integer -> Int
forall a. Num a => Integer -> a
fromInteger) (Type, Type, Integer)
resTyInfo [Value]
args)
        -> Term -> Maybe Machine
reduce Term
val
      PrimStepContext
_ -> Maybe Machine
forall a. Maybe a
Nothing

  , Text -> (PrimStepContext -> Maybe Machine) -> (Text, PrimStep)
primStepEntry $(textNameLit 'Clash.Sized.Internal.BitVector.fromEnum#) ((PrimStepContext -> Maybe Machine) -> (Text, PrimStep))
-> (PrimStepContext -> Maybe Machine) -> (Text, PrimStep)
forall a b. (a -> b) -> a -> b
$ \case
      PrimStepContext{Bool
[Type]
[Value]
Type
TyConMap
Machine
PrimInfo
Term -> Maybe Machine
Term -> Term
Type
-> Integer -> Integer -> (Natural -> Natural -> Natural) -> Term
Type -> Integer -> (Natural -> Natural) -> Term
Type -> [Integer] -> ([Natural] -> Term) -> Term
Machine -> Term -> Maybe Machine
tcm :: PrimStepContext -> TyConMap
isSubj :: PrimStepContext -> Bool
pInfo :: PrimStepContext -> PrimInfo
tys :: PrimStepContext -> [Type]
args :: PrimStepContext -> [Value]
mach :: PrimStepContext -> Machine
ty :: PrimStepContext -> Type
checkNaturalRange1 :: PrimStepContext -> Type -> Integer -> (Natural -> Natural) -> Term
checkNaturalRange2 :: PrimStepContext
-> Type
-> Integer
-> Integer
-> (Natural -> Natural -> Natural)
-> Term
checkNaturalRange :: PrimStepContext -> Type -> [Integer] -> ([Natural] -> Term) -> Term
reduce :: PrimStepContext -> Term -> Maybe Machine
reduceWith :: PrimStepContext -> Machine -> Term -> Maybe Machine
reduceWHNF :: PrimStepContext -> Term -> Maybe Machine
reduceWHNF' :: PrimStepContext -> Machine -> Term -> Maybe Machine
catchDivByZero :: PrimStepContext -> Term -> Term
catchErrorCall :: PrimStepContext -> Term -> Term
tcm :: TyConMap
isSubj :: Bool
pInfo :: PrimInfo
tys :: [Type]
args :: [Value]
mach :: Machine
ty :: Type
checkNaturalRange1 :: Type -> Integer -> (Natural -> Natural) -> Term
checkNaturalRange2 :: Type
-> Integer -> Integer -> (Natural -> Natural -> Natural) -> Term
checkNaturalRange :: Type -> [Integer] -> ([Natural] -> Term) -> Term
reduce :: Term -> Maybe Machine
reduceWith :: Machine -> Term -> Maybe Machine
reduceWHNF :: Term -> Maybe Machine
reduceWHNF' :: Machine -> Term -> Maybe Machine
catchDivByZero :: Term -> Term
catchErrorCall :: Term -> Term
..}
        | Just (Type
_, Integer
kn) <- TyConMap -> [Type] -> Maybe (Type, Integer)
extractKnownNat TyConMap
tcm [Type]
tys
        , let resTy :: Type
resTy = TyConMap -> Type -> [Type] -> Type
getResultTy TyConMap
tcm Type
ty [Type]
tys
        , Just Term
val <- Integer
-> (forall (n :: Natural). KnownNat n => Proxy n -> Maybe Term)
-> Maybe Term
forall r.
Integer -> (forall (n :: Natural). KnownNat n => Proxy n -> r) -> r
reifyNat Integer
kn (TyConMap
-> Type
-> (BitVector n -> Integer)
-> [Value]
-> Proxy n
-> Maybe Term
forall (n :: Natural).
KnownNat n =>
TyConMap
-> Type
-> (BitVector n -> Integer)
-> [Value]
-> Proxy n
-> Maybe Term
liftBitVector2CInt TyConMap
tcm Type
resTy (Int -> Integer
forall a. Integral a => a -> Integer
toInteger (Int -> Integer) -> (BitVector n -> Int) -> BitVector n -> Integer
forall b c a. (b -> c) -> (a -> b) -> a -> c
. BitVector n -> Int
forall (n :: Natural). KnownNat n => BitVector n -> Int
BitVector.fromEnum#) [Value]
args)
        -> Term -> Maybe Machine
reduce Term
val
      PrimStepContext
_ -> Maybe Machine
forall a. Maybe a
Nothing


-- Bounded
  , Text -> (PrimStepContext -> Maybe Machine) -> (Text, PrimStep)
primStepEntry $(textNameLit 'Clash.Sized.Internal.BitVector.minBound#) ((PrimStepContext -> Maybe Machine) -> (Text, PrimStep))
-> (PrimStepContext -> Maybe Machine) -> (Text, PrimStep)
forall a b. (a -> b) -> a -> b
$ \case
      PrimStepContext{Bool
[Type]
[Value]
Type
TyConMap
Machine
PrimInfo
Term -> Maybe Machine
Term -> Term
Type
-> Integer -> Integer -> (Natural -> Natural -> Natural) -> Term
Type -> Integer -> (Natural -> Natural) -> Term
Type -> [Integer] -> ([Natural] -> Term) -> Term
Machine -> Term -> Maybe Machine
tcm :: PrimStepContext -> TyConMap
isSubj :: PrimStepContext -> Bool
pInfo :: PrimStepContext -> PrimInfo
tys :: PrimStepContext -> [Type]
args :: PrimStepContext -> [Value]
mach :: PrimStepContext -> Machine
ty :: PrimStepContext -> Type
checkNaturalRange1 :: PrimStepContext -> Type -> Integer -> (Natural -> Natural) -> Term
checkNaturalRange2 :: PrimStepContext
-> Type
-> Integer
-> Integer
-> (Natural -> Natural -> Natural)
-> Term
checkNaturalRange :: PrimStepContext -> Type -> [Integer] -> ([Natural] -> Term) -> Term
reduce :: PrimStepContext -> Term -> Maybe Machine
reduceWith :: PrimStepContext -> Machine -> Term -> Maybe Machine
reduceWHNF :: PrimStepContext -> Term -> Maybe Machine
reduceWHNF' :: PrimStepContext -> Machine -> Term -> Maybe Machine
catchDivByZero :: PrimStepContext -> Term -> Term
catchErrorCall :: PrimStepContext -> Term -> Term
tcm :: TyConMap
isSubj :: Bool
pInfo :: PrimInfo
tys :: [Type]
args :: [Value]
mach :: Machine
ty :: Type
checkNaturalRange1 :: Type -> Integer -> (Natural -> Natural) -> Term
checkNaturalRange2 :: Type
-> Integer -> Integer -> (Natural -> Natural -> Natural) -> Term
checkNaturalRange :: Type -> [Integer] -> ([Natural] -> Term) -> Term
reduce :: Term -> Maybe Machine
reduceWith :: Machine -> Term -> Maybe Machine
reduceWHNF :: Term -> Maybe Machine
reduceWHNF' :: Machine -> Term -> Maybe Machine
catchDivByZero :: Term -> Term
catchErrorCall :: Term -> Term
..}
        | Just (Type
nTy,Integer
len) <- TyConMap -> [Type] -> Maybe (Type, Integer)
extractKnownNat TyConMap
tcm [Type]
tys
        -> Term -> Maybe Machine
reduce (Type -> Type -> Integer -> Integer -> Integer -> Term
mkBitVectorLit Type
ty Type
nTy Integer
len Integer
0 Integer
0)
      PrimStepContext
_ -> Maybe Machine
forall a. Maybe a
Nothing

  , Text -> (PrimStepContext -> Maybe Machine) -> (Text, PrimStep)
primStepEntry $(textNameLit 'Clash.Sized.Internal.BitVector.maxBound#) ((PrimStepContext -> Maybe Machine) -> (Text, PrimStep))
-> (PrimStepContext -> Maybe Machine) -> (Text, PrimStep)
forall a b. (a -> b) -> a -> b
$ \case
      PrimStepContext{Bool
[Type]
[Value]
Type
TyConMap
Machine
PrimInfo
Term -> Maybe Machine
Term -> Term
Type
-> Integer -> Integer -> (Natural -> Natural -> Natural) -> Term
Type -> Integer -> (Natural -> Natural) -> Term
Type -> [Integer] -> ([Natural] -> Term) -> Term
Machine -> Term -> Maybe Machine
tcm :: PrimStepContext -> TyConMap
isSubj :: PrimStepContext -> Bool
pInfo :: PrimStepContext -> PrimInfo
tys :: PrimStepContext -> [Type]
args :: PrimStepContext -> [Value]
mach :: PrimStepContext -> Machine
ty :: PrimStepContext -> Type
checkNaturalRange1 :: PrimStepContext -> Type -> Integer -> (Natural -> Natural) -> Term
checkNaturalRange2 :: PrimStepContext
-> Type
-> Integer
-> Integer
-> (Natural -> Natural -> Natural)
-> Term
checkNaturalRange :: PrimStepContext -> Type -> [Integer] -> ([Natural] -> Term) -> Term
reduce :: PrimStepContext -> Term -> Maybe Machine
reduceWith :: PrimStepContext -> Machine -> Term -> Maybe Machine
reduceWHNF :: PrimStepContext -> Term -> Maybe Machine
reduceWHNF' :: PrimStepContext -> Machine -> Term -> Maybe Machine
catchDivByZero :: PrimStepContext -> Term -> Term
catchErrorCall :: PrimStepContext -> Term -> Term
tcm :: TyConMap
isSubj :: Bool
pInfo :: PrimInfo
tys :: [Type]
args :: [Value]
mach :: Machine
ty :: Type
checkNaturalRange1 :: Type -> Integer -> (Natural -> Natural) -> Term
checkNaturalRange2 :: Type
-> Integer -> Integer -> (Natural -> Natural -> Natural) -> Term
checkNaturalRange :: Type -> [Integer] -> ([Natural] -> Term) -> Term
reduce :: Term -> Maybe Machine
reduceWith :: Machine -> Term -> Maybe Machine
reduceWHNF :: Term -> Maybe Machine
reduceWHNF' :: Machine -> Term -> Maybe Machine
catchDivByZero :: Term -> Term
catchErrorCall :: Term -> Term
..}
        | Just (Type
litTy,Integer
mb) <- TyConMap -> [Type] -> Maybe (Type, Integer)
extractKnownNat TyConMap
tcm [Type]
tys
        -> let maxB :: Integer
maxB = (Integer
2 Integer -> Integer -> Integer
forall a b. (Num a, Integral b) => a -> b -> a
^ Integer
mb) Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
- Integer
1
           in  Term -> Maybe Machine
reduce (Type -> Type -> Integer -> Integer -> Integer -> Term
mkBitVectorLit Type
ty Type
litTy Integer
mb Integer
0 Integer
maxB)
      PrimStepContext
_ -> Maybe Machine
forall a. Maybe a
Nothing


-- Num
  , Text -> (PrimStepContext -> Maybe Machine) -> (Text, PrimStep)
primStepEntry $(textNameLit '(Clash.Sized.Internal.BitVector.+#)) ((PrimStepContext -> Maybe Machine) -> (Text, PrimStep))
-> (PrimStepContext -> Maybe Machine) -> (Text, PrimStep)
forall a b. (a -> b) -> a -> b
$ \case
      PrimStepContext{Bool
[Type]
[Value]
Type
TyConMap
Machine
PrimInfo
Term -> Maybe Machine
Term -> Term
Type
-> Integer -> Integer -> (Natural -> Natural -> Natural) -> Term
Type -> Integer -> (Natural -> Natural) -> Term
Type -> [Integer] -> ([Natural] -> Term) -> Term
Machine -> Term -> Maybe Machine
tcm :: PrimStepContext -> TyConMap
isSubj :: PrimStepContext -> Bool
pInfo :: PrimStepContext -> PrimInfo
tys :: PrimStepContext -> [Type]
args :: PrimStepContext -> [Value]
mach :: PrimStepContext -> Machine
ty :: PrimStepContext -> Type
checkNaturalRange1 :: PrimStepContext -> Type -> Integer -> (Natural -> Natural) -> Term
checkNaturalRange2 :: PrimStepContext
-> Type
-> Integer
-> Integer
-> (Natural -> Natural -> Natural)
-> Term
checkNaturalRange :: PrimStepContext -> Type -> [Integer] -> ([Natural] -> Term) -> Term
reduce :: PrimStepContext -> Term -> Maybe Machine
reduceWith :: PrimStepContext -> Machine -> Term -> Maybe Machine
reduceWHNF :: PrimStepContext -> Term -> Maybe Machine
reduceWHNF' :: PrimStepContext -> Machine -> Term -> Maybe Machine
catchDivByZero :: PrimStepContext -> Term -> Term
catchErrorCall :: PrimStepContext -> Term -> Term
tcm :: TyConMap
isSubj :: Bool
pInfo :: PrimInfo
tys :: [Type]
args :: [Value]
mach :: Machine
ty :: Type
checkNaturalRange1 :: Type -> Integer -> (Natural -> Natural) -> Term
checkNaturalRange2 :: Type
-> Integer -> Integer -> (Natural -> Natural -> Natural) -> Term
checkNaturalRange :: Type -> [Integer] -> ([Natural] -> Term) -> Term
reduce :: Term -> Maybe Machine
reduceWith :: Machine -> Term -> Maybe Machine
reduceWHNF :: Term -> Maybe Machine
reduceWHNF' :: Machine -> Term -> Maybe Machine
catchDivByZero :: Term -> Term
catchErrorCall :: Term -> Term
..}
        | Just (Type
_, Integer
kn) <- TyConMap -> [Type] -> Maybe (Type, Integer)
extractKnownNat TyConMap
tcm [Type]
tys
        , Just Term
val <- Integer
-> (forall (n :: Natural). KnownNat n => Proxy n -> Maybe Term)
-> Maybe Term
forall r.
Integer -> (forall (n :: Natural). KnownNat n => Proxy n -> r) -> r
reifyNat Integer
kn ((BitVector n -> BitVector n -> BitVector n)
-> Type -> TyConMap -> [Type] -> [Value] -> Proxy n -> Maybe Term
forall (n :: Natural).
KnownNat n =>
(BitVector n -> BitVector n -> BitVector n)
-> Type -> TyConMap -> [Type] -> [Value] -> Proxy n -> Maybe Term
liftBitVector2 BitVector n -> BitVector n -> BitVector n
forall (n :: Natural).
KnownNat n =>
BitVector n -> BitVector n -> BitVector n
(BitVector.+#) Type
ty TyConMap
tcm [Type]
tys [Value]
args)
        -> Term -> Maybe Machine
reduce Term
val
      PrimStepContext
_ -> Maybe Machine
forall a. Maybe a
Nothing

  , Text -> (PrimStepContext -> Maybe Machine) -> (Text, PrimStep)
primStepEntry $(textNameLit '(Clash.Sized.Internal.BitVector.-#)) ((PrimStepContext -> Maybe Machine) -> (Text, PrimStep))
-> (PrimStepContext -> Maybe Machine) -> (Text, PrimStep)
forall a b. (a -> b) -> a -> b
$ \case
      PrimStepContext{Bool
[Type]
[Value]
Type
TyConMap
Machine
PrimInfo
Term -> Maybe Machine
Term -> Term
Type
-> Integer -> Integer -> (Natural -> Natural -> Natural) -> Term
Type -> Integer -> (Natural -> Natural) -> Term
Type -> [Integer] -> ([Natural] -> Term) -> Term
Machine -> Term -> Maybe Machine
tcm :: PrimStepContext -> TyConMap
isSubj :: PrimStepContext -> Bool
pInfo :: PrimStepContext -> PrimInfo
tys :: PrimStepContext -> [Type]
args :: PrimStepContext -> [Value]
mach :: PrimStepContext -> Machine
ty :: PrimStepContext -> Type
checkNaturalRange1 :: PrimStepContext -> Type -> Integer -> (Natural -> Natural) -> Term
checkNaturalRange2 :: PrimStepContext
-> Type
-> Integer
-> Integer
-> (Natural -> Natural -> Natural)
-> Term
checkNaturalRange :: PrimStepContext -> Type -> [Integer] -> ([Natural] -> Term) -> Term
reduce :: PrimStepContext -> Term -> Maybe Machine
reduceWith :: PrimStepContext -> Machine -> Term -> Maybe Machine
reduceWHNF :: PrimStepContext -> Term -> Maybe Machine
reduceWHNF' :: PrimStepContext -> Machine -> Term -> Maybe Machine
catchDivByZero :: PrimStepContext -> Term -> Term
catchErrorCall :: PrimStepContext -> Term -> Term
tcm :: TyConMap
isSubj :: Bool
pInfo :: PrimInfo
tys :: [Type]
args :: [Value]
mach :: Machine
ty :: Type
checkNaturalRange1 :: Type -> Integer -> (Natural -> Natural) -> Term
checkNaturalRange2 :: Type
-> Integer -> Integer -> (Natural -> Natural -> Natural) -> Term
checkNaturalRange :: Type -> [Integer] -> ([Natural] -> Term) -> Term
reduce :: Term -> Maybe Machine
reduceWith :: Machine -> Term -> Maybe Machine
reduceWHNF :: Term -> Maybe Machine
reduceWHNF' :: Machine -> Term -> Maybe Machine
catchDivByZero :: Term -> Term
catchErrorCall :: Term -> Term
..}
        | Just (Type
_, Integer
kn) <- TyConMap -> [Type] -> Maybe (Type, Integer)
extractKnownNat TyConMap
tcm [Type]
tys
        , Just Term
val <- Integer
-> (forall (n :: Natural). KnownNat n => Proxy n -> Maybe Term)
-> Maybe Term
forall r.
Integer -> (forall (n :: Natural). KnownNat n => Proxy n -> r) -> r
reifyNat Integer
kn ((BitVector n -> BitVector n -> BitVector n)
-> Type -> TyConMap -> [Type] -> [Value] -> Proxy n -> Maybe Term
forall (n :: Natural).
KnownNat n =>
(BitVector n -> BitVector n -> BitVector n)
-> Type -> TyConMap -> [Type] -> [Value] -> Proxy n -> Maybe Term
liftBitVector2 BitVector n -> BitVector n -> BitVector n
forall (n :: Natural).
KnownNat n =>
BitVector n -> BitVector n -> BitVector n
(BitVector.-#) Type
ty TyConMap
tcm [Type]
tys [Value]
args)
        -> Term -> Maybe Machine
reduce Term
val
      PrimStepContext
_ -> Maybe Machine
forall a. Maybe a
Nothing

  , Text -> (PrimStepContext -> Maybe Machine) -> (Text, PrimStep)
primStepEntry $(textNameLit '(Clash.Sized.Internal.BitVector.*#)) ((PrimStepContext -> Maybe Machine) -> (Text, PrimStep))
-> (PrimStepContext -> Maybe Machine) -> (Text, PrimStep)
forall a b. (a -> b) -> a -> b
$ \case
      PrimStepContext{Bool
[Type]
[Value]
Type
TyConMap
Machine
PrimInfo
Term -> Maybe Machine
Term -> Term
Type
-> Integer -> Integer -> (Natural -> Natural -> Natural) -> Term
Type -> Integer -> (Natural -> Natural) -> Term
Type -> [Integer] -> ([Natural] -> Term) -> Term
Machine -> Term -> Maybe Machine
tcm :: PrimStepContext -> TyConMap
isSubj :: PrimStepContext -> Bool
pInfo :: PrimStepContext -> PrimInfo
tys :: PrimStepContext -> [Type]
args :: PrimStepContext -> [Value]
mach :: PrimStepContext -> Machine
ty :: PrimStepContext -> Type
checkNaturalRange1 :: PrimStepContext -> Type -> Integer -> (Natural -> Natural) -> Term
checkNaturalRange2 :: PrimStepContext
-> Type
-> Integer
-> Integer
-> (Natural -> Natural -> Natural)
-> Term
checkNaturalRange :: PrimStepContext -> Type -> [Integer] -> ([Natural] -> Term) -> Term
reduce :: PrimStepContext -> Term -> Maybe Machine
reduceWith :: PrimStepContext -> Machine -> Term -> Maybe Machine
reduceWHNF :: PrimStepContext -> Term -> Maybe Machine
reduceWHNF' :: PrimStepContext -> Machine -> Term -> Maybe Machine
catchDivByZero :: PrimStepContext -> Term -> Term
catchErrorCall :: PrimStepContext -> Term -> Term
tcm :: TyConMap
isSubj :: Bool
pInfo :: PrimInfo
tys :: [Type]
args :: [Value]
mach :: Machine
ty :: Type
checkNaturalRange1 :: Type -> Integer -> (Natural -> Natural) -> Term
checkNaturalRange2 :: Type
-> Integer -> Integer -> (Natural -> Natural -> Natural) -> Term
checkNaturalRange :: Type -> [Integer] -> ([Natural] -> Term) -> Term
reduce :: Term -> Maybe Machine
reduceWith :: Machine -> Term -> Maybe Machine
reduceWHNF :: Term -> Maybe Machine
reduceWHNF' :: Machine -> Term -> Maybe Machine
catchDivByZero :: Term -> Term
catchErrorCall :: Term -> Term
..}
        | Just (Type
_, Integer
kn) <- TyConMap -> [Type] -> Maybe (Type, Integer)
extractKnownNat TyConMap
tcm [Type]
tys
        , Just Term
val <- Integer
-> (forall (n :: Natural). KnownNat n => Proxy n -> Maybe Term)
-> Maybe Term
forall r.
Integer -> (forall (n :: Natural). KnownNat n => Proxy n -> r) -> r
reifyNat Integer
kn ((BitVector n -> BitVector n -> BitVector n)
-> Type -> TyConMap -> [Type] -> [Value] -> Proxy n -> Maybe Term
forall (n :: Natural).
KnownNat n =>
(BitVector n -> BitVector n -> BitVector n)
-> Type -> TyConMap -> [Type] -> [Value] -> Proxy n -> Maybe Term
liftBitVector2 BitVector n -> BitVector n -> BitVector n
forall (n :: Natural).
KnownNat n =>
BitVector n -> BitVector n -> BitVector n
(BitVector.*#) Type
ty TyConMap
tcm [Type]
tys [Value]
args)
        -> Term -> Maybe Machine
reduce Term
val
      PrimStepContext
_ -> Maybe Machine
forall a. Maybe a
Nothing

  , Text -> (PrimStepContext -> Maybe Machine) -> (Text, PrimStep)
primStepEntry $(textNameLit 'Clash.Sized.Internal.BitVector.negate#) ((PrimStepContext -> Maybe Machine) -> (Text, PrimStep))
-> (PrimStepContext -> Maybe Machine) -> (Text, PrimStep)
forall a b. (a -> b) -> a -> b
$ \case
      PrimStepContext{Bool
[Type]
[Value]
Type
TyConMap
Machine
PrimInfo
Term -> Maybe Machine
Term -> Term
Type
-> Integer -> Integer -> (Natural -> Natural -> Natural) -> Term
Type -> Integer -> (Natural -> Natural) -> Term
Type -> [Integer] -> ([Natural] -> Term) -> Term
Machine -> Term -> Maybe Machine
tcm :: PrimStepContext -> TyConMap
isSubj :: PrimStepContext -> Bool
pInfo :: PrimStepContext -> PrimInfo
tys :: PrimStepContext -> [Type]
args :: PrimStepContext -> [Value]
mach :: PrimStepContext -> Machine
ty :: PrimStepContext -> Type
checkNaturalRange1 :: PrimStepContext -> Type -> Integer -> (Natural -> Natural) -> Term
checkNaturalRange2 :: PrimStepContext
-> Type
-> Integer
-> Integer
-> (Natural -> Natural -> Natural)
-> Term
checkNaturalRange :: PrimStepContext -> Type -> [Integer] -> ([Natural] -> Term) -> Term
reduce :: PrimStepContext -> Term -> Maybe Machine
reduceWith :: PrimStepContext -> Machine -> Term -> Maybe Machine
reduceWHNF :: PrimStepContext -> Term -> Maybe Machine
reduceWHNF' :: PrimStepContext -> Machine -> Term -> Maybe Machine
catchDivByZero :: PrimStepContext -> Term -> Term
catchErrorCall :: PrimStepContext -> Term -> Term
tcm :: TyConMap
isSubj :: Bool
pInfo :: PrimInfo
tys :: [Type]
args :: [Value]
mach :: Machine
ty :: Type
checkNaturalRange1 :: Type -> Integer -> (Natural -> Natural) -> Term
checkNaturalRange2 :: Type
-> Integer -> Integer -> (Natural -> Natural -> Natural) -> Term
checkNaturalRange :: Type -> [Integer] -> ([Natural] -> Term) -> Term
reduce :: Term -> Maybe Machine
reduceWith :: Machine -> Term -> Maybe Machine
reduceWHNF :: Term -> Maybe Machine
reduceWHNF' :: Machine -> Term -> Maybe Machine
catchDivByZero :: Term -> Term
catchErrorCall :: Term -> Term
..}
        | Just (Type
nTy, Integer
kn) <- TyConMap -> [Type] -> Maybe (Type, Integer)
extractKnownNat TyConMap
tcm [Type]
tys
        , [(Integer, Integer)
i] <- [Value] -> [(Integer, Integer)]
bitVectorLiterals' [Value]
args
        -> let (Integer
msk,Integer
val) = Integer
-> (forall (n :: Natural).
    KnownNat n =>
    Proxy n -> (Integer, Integer))
-> (Integer, Integer)
forall r.
Integer -> (forall (n :: Natural). KnownNat n => Proxy n -> r) -> r
reifyNat Integer
kn (BitVector n -> Proxy n -> (Integer, Integer)
forall (n :: Natural).
KnownNat n =>
BitVector n -> Proxy n -> (Integer, Integer)
op ((Integer, Integer) -> BitVector n
forall (n :: Natural). (Integer, Integer) -> BitVector n
toBV (Integer, Integer)
i))
        in Term -> Maybe Machine
reduce (Type -> Type -> Integer -> Integer -> Integer -> Term
mkBitVectorLit Type
ty Type
nTy Integer
kn Integer
msk Integer
val)
        where
          op :: KnownNat n => BitVector n -> Proxy n -> (Integer,Integer)
          op :: forall (n :: Natural).
KnownNat n =>
BitVector n -> Proxy n -> (Integer, Integer)
op BitVector n
u Proxy n
_ = BitVector n -> (Integer, Integer)
forall (n :: Natural). BitVector n -> (Integer, Integer)
splitBV (BitVector n -> BitVector n
forall (n :: Natural). KnownNat n => BitVector n -> BitVector n
BitVector.negate# BitVector n
u)
      PrimStepContext
_ -> Maybe Machine
forall a. Maybe a
Nothing


-- ExtendingNum
  , Text -> (PrimStepContext -> Maybe Machine) -> (Text, PrimStep)
primStepEntry $(textNameLit 'Clash.Sized.Internal.BitVector.plus#) ((PrimStepContext -> Maybe Machine) -> (Text, PrimStep))
-> (PrimStepContext -> Maybe Machine) -> (Text, PrimStep)
forall a b. (a -> b) -> a -> b
$ \case
      PrimStepContext{Bool
[Type]
[Value]
Type
TyConMap
Machine
PrimInfo
Term -> Maybe Machine
Term -> Term
Type
-> Integer -> Integer -> (Natural -> Natural -> Natural) -> Term
Type -> Integer -> (Natural -> Natural) -> Term
Type -> [Integer] -> ([Natural] -> Term) -> Term
Machine -> Term -> Maybe Machine
tcm :: PrimStepContext -> TyConMap
isSubj :: PrimStepContext -> Bool
pInfo :: PrimStepContext -> PrimInfo
tys :: PrimStepContext -> [Type]
args :: PrimStepContext -> [Value]
mach :: PrimStepContext -> Machine
ty :: PrimStepContext -> Type
checkNaturalRange1 :: PrimStepContext -> Type -> Integer -> (Natural -> Natural) -> Term
checkNaturalRange2 :: PrimStepContext
-> Type
-> Integer
-> Integer
-> (Natural -> Natural -> Natural)
-> Term
checkNaturalRange :: PrimStepContext -> Type -> [Integer] -> ([Natural] -> Term) -> Term
reduce :: PrimStepContext -> Term -> Maybe Machine
reduceWith :: PrimStepContext -> Machine -> Term -> Maybe Machine
reduceWHNF :: PrimStepContext -> Term -> Maybe Machine
reduceWHNF' :: PrimStepContext -> Machine -> Term -> Maybe Machine
catchDivByZero :: PrimStepContext -> Term -> Term
catchErrorCall :: PrimStepContext -> Term -> Term
tcm :: TyConMap
isSubj :: Bool
pInfo :: PrimInfo
tys :: [Type]
args :: [Value]
mach :: Machine
ty :: Type
checkNaturalRange1 :: Type -> Integer -> (Natural -> Natural) -> Term
checkNaturalRange2 :: Type
-> Integer -> Integer -> (Natural -> Natural -> Natural) -> Term
checkNaturalRange :: Type -> [Integer] -> ([Natural] -> Term) -> Term
reduce :: Term -> Maybe Machine
reduceWith :: Machine -> Term -> Maybe Machine
reduceWHNF :: Term -> Maybe Machine
reduceWHNF' :: Machine -> Term -> Maybe Machine
catchDivByZero :: Term -> Term
catchErrorCall :: Term -> Term
..} -- :: (KnownNat n, KnownNat m) => BitVector m -> BitVector n -> BitVector (Max m n + 1)
        | [(Integer
0,Integer
i),(Integer
0,Integer
j)] <- [Value] -> [(Integer, Integer)]
bitVectorLiterals' [Value]
args
        -> let ty' :: Type
ty' = HasCallStack => TyConMap -> Type -> [Type] -> Type
TyConMap -> Type -> [Type] -> Type
piResultTys TyConMap
tcm Type
ty [Type]
tys
               ([Either TyVar Type]
_,Type
resTy) = Type -> ([Either TyVar Type], Type)
splitFunForallTy Type
ty'
               (TyConApp TyConName
_ [Type
resSizeTy]) = Type -> TypeView
tyView Type
resTy
               Right Integer
resSizeInt = Except String Integer -> Either String Integer
forall e a. Except e a -> Either e a
runExcept (TyConMap -> Type -> Except String Integer
tyNatSize TyConMap
tcm Type
resSizeTy)
           in  Term -> Maybe Machine
reduce (Type -> Type -> Integer -> Integer -> Integer -> Term
mkBitVectorLit Type
resTy Type
resSizeTy Integer
resSizeInt Integer
0 (Integer
iInteger -> Integer -> Integer
forall a. Num a => a -> a -> a
+Integer
j))
      PrimStepContext
_ -> Maybe Machine
forall a. Maybe a
Nothing

  , Text -> (PrimStepContext -> Maybe Machine) -> (Text, PrimStep)
primStepEntry $(textNameLit 'Clash.Sized.Internal.BitVector.minus#) ((PrimStepContext -> Maybe Machine) -> (Text, PrimStep))
-> (PrimStepContext -> Maybe Machine) -> (Text, PrimStep)
forall a b. (a -> b) -> a -> b
$ \case
      PrimStepContext{Bool
[Type]
[Value]
Type
TyConMap
Machine
PrimInfo
Term -> Maybe Machine
Term -> Term
Type
-> Integer -> Integer -> (Natural -> Natural -> Natural) -> Term
Type -> Integer -> (Natural -> Natural) -> Term
Type -> [Integer] -> ([Natural] -> Term) -> Term
Machine -> Term -> Maybe Machine
tcm :: PrimStepContext -> TyConMap
isSubj :: PrimStepContext -> Bool
pInfo :: PrimStepContext -> PrimInfo
tys :: PrimStepContext -> [Type]
args :: PrimStepContext -> [Value]
mach :: PrimStepContext -> Machine
ty :: PrimStepContext -> Type
checkNaturalRange1 :: PrimStepContext -> Type -> Integer -> (Natural -> Natural) -> Term
checkNaturalRange2 :: PrimStepContext
-> Type
-> Integer
-> Integer
-> (Natural -> Natural -> Natural)
-> Term
checkNaturalRange :: PrimStepContext -> Type -> [Integer] -> ([Natural] -> Term) -> Term
reduce :: PrimStepContext -> Term -> Maybe Machine
reduceWith :: PrimStepContext -> Machine -> Term -> Maybe Machine
reduceWHNF :: PrimStepContext -> Term -> Maybe Machine
reduceWHNF' :: PrimStepContext -> Machine -> Term -> Maybe Machine
catchDivByZero :: PrimStepContext -> Term -> Term
catchErrorCall :: PrimStepContext -> Term -> Term
tcm :: TyConMap
isSubj :: Bool
pInfo :: PrimInfo
tys :: [Type]
args :: [Value]
mach :: Machine
ty :: Type
checkNaturalRange1 :: Type -> Integer -> (Natural -> Natural) -> Term
checkNaturalRange2 :: Type
-> Integer -> Integer -> (Natural -> Natural -> Natural) -> Term
checkNaturalRange :: Type -> [Integer] -> ([Natural] -> Term) -> Term
reduce :: Term -> Maybe Machine
reduceWith :: Machine -> Term -> Maybe Machine
reduceWHNF :: Term -> Maybe Machine
reduceWHNF' :: Machine -> Term -> Maybe Machine
catchDivByZero :: Term -> Term
catchErrorCall :: Term -> Term
..}
        | [(Integer
0,Integer
i),(Integer
0,Integer
j)] <- [Value] -> [(Integer, Integer)]
bitVectorLiterals' [Value]
args
        -> let ty' :: Type
ty' = HasCallStack => TyConMap -> Type -> [Type] -> Type
TyConMap -> Type -> [Type] -> Type
piResultTys TyConMap
tcm Type
ty [Type]
tys
               ([Either TyVar Type]
_,Type
resTy) = Type -> ([Either TyVar Type], Type)
splitFunForallTy Type
ty'
               (TyConApp TyConName
_ [Type
resSizeTy]) = Type -> TypeView
tyView Type
resTy
               Right Integer
resSizeInt = Except String Integer -> Either String Integer
forall e a. Except e a -> Either e a
runExcept (TyConMap -> Type -> Except String Integer
tyNatSize TyConMap
tcm Type
resSizeTy)
               val :: Integer
val = Integer
-> (forall (n :: Natural). KnownNat n => Proxy n -> Integer)
-> Integer
forall r.
Integer -> (forall (n :: Natural). KnownNat n => Proxy n -> r) -> r
reifyNat Integer
resSizeInt ((BitVector n -> BitVector n -> BitVector n)
-> Integer -> Integer -> Proxy n -> Integer
forall (n :: Natural) (sized :: Natural -> Type).
(KnownNat n, Integral (sized n)) =>
(sized n -> sized n -> sized n)
-> Integer -> Integer -> Proxy n -> Integer
runSizedF BitVector n -> BitVector n -> BitVector n
forall (n :: Natural).
KnownNat n =>
BitVector n -> BitVector n -> BitVector n
(BitVector.-#) Integer
i Integer
j)
          in  Term -> Maybe Machine
reduce (Type -> Type -> Integer -> Integer -> Integer -> Term
mkBitVectorLit Type
resTy Type
resSizeTy Integer
resSizeInt Integer
0 Integer
val)
      PrimStepContext
_ -> Maybe Machine
forall a. Maybe a
Nothing

  , Text -> (PrimStepContext -> Maybe Machine) -> (Text, PrimStep)
primStepEntry $(textNameLit 'Clash.Sized.Internal.BitVector.times#) ((PrimStepContext -> Maybe Machine) -> (Text, PrimStep))
-> (PrimStepContext -> Maybe Machine) -> (Text, PrimStep)
forall a b. (a -> b) -> a -> b
$ \case
      PrimStepContext{Bool
[Type]
[Value]
Type
TyConMap
Machine
PrimInfo
Term -> Maybe Machine
Term -> Term
Type
-> Integer -> Integer -> (Natural -> Natural -> Natural) -> Term
Type -> Integer -> (Natural -> Natural) -> Term
Type -> [Integer] -> ([Natural] -> Term) -> Term
Machine -> Term -> Maybe Machine
tcm :: PrimStepContext -> TyConMap
isSubj :: PrimStepContext -> Bool
pInfo :: PrimStepContext -> PrimInfo
tys :: PrimStepContext -> [Type]
args :: PrimStepContext -> [Value]
mach :: PrimStepContext -> Machine
ty :: PrimStepContext -> Type
checkNaturalRange1 :: PrimStepContext -> Type -> Integer -> (Natural -> Natural) -> Term
checkNaturalRange2 :: PrimStepContext
-> Type
-> Integer
-> Integer
-> (Natural -> Natural -> Natural)
-> Term
checkNaturalRange :: PrimStepContext -> Type -> [Integer] -> ([Natural] -> Term) -> Term
reduce :: PrimStepContext -> Term -> Maybe Machine
reduceWith :: PrimStepContext -> Machine -> Term -> Maybe Machine
reduceWHNF :: PrimStepContext -> Term -> Maybe Machine
reduceWHNF' :: PrimStepContext -> Machine -> Term -> Maybe Machine
catchDivByZero :: PrimStepContext -> Term -> Term
catchErrorCall :: PrimStepContext -> Term -> Term
tcm :: TyConMap
isSubj :: Bool
pInfo :: PrimInfo
tys :: [Type]
args :: [Value]
mach :: Machine
ty :: Type
checkNaturalRange1 :: Type -> Integer -> (Natural -> Natural) -> Term
checkNaturalRange2 :: Type
-> Integer -> Integer -> (Natural -> Natural -> Natural) -> Term
checkNaturalRange :: Type -> [Integer] -> ([Natural] -> Term) -> Term
reduce :: Term -> Maybe Machine
reduceWith :: Machine -> Term -> Maybe Machine
reduceWHNF :: Term -> Maybe Machine
reduceWHNF' :: Machine -> Term -> Maybe Machine
catchDivByZero :: Term -> Term
catchErrorCall :: Term -> Term
..}
        | [(Integer
0,Integer
i),(Integer
0,Integer
j)] <- [Value] -> [(Integer, Integer)]
bitVectorLiterals' [Value]
args
        -> let ty' :: Type
ty' = HasCallStack => TyConMap -> Type -> [Type] -> Type
TyConMap -> Type -> [Type] -> Type
piResultTys TyConMap
tcm Type
ty [Type]
tys
               ([Either TyVar Type]
_,Type
resTy) = Type -> ([Either TyVar Type], Type)
splitFunForallTy Type
ty'
               (TyConApp TyConName
_ [Type
resSizeTy]) = Type -> TypeView
tyView Type
resTy
               Right Integer
resSizeInt = Except String Integer -> Either String Integer
forall e a. Except e a -> Either e a
runExcept (TyConMap -> Type -> Except String Integer
tyNatSize TyConMap
tcm Type
resSizeTy)
           in  Term -> Maybe Machine
reduce (Type -> Type -> Integer -> Integer -> Integer -> Term
mkBitVectorLit Type
resTy Type
resSizeTy Integer
resSizeInt Integer
0 (Integer
iInteger -> Integer -> Integer
forall a. Num a => a -> a -> a
*Integer
j))
      PrimStepContext
_ -> Maybe Machine
forall a. Maybe a
Nothing


-- Integral
  , Text -> (PrimStepContext -> Maybe Machine) -> (Text, PrimStep)
primStepEntry $(textNameLit 'Clash.Sized.Internal.BitVector.quot#) ((PrimStepContext -> Maybe Machine) -> (Text, PrimStep))
-> (PrimStepContext -> Maybe Machine) -> (Text, PrimStep)
forall a b. (a -> b) -> a -> b
$ \case
      PrimStepContext{Bool
[Type]
[Value]
Type
TyConMap
Machine
PrimInfo
Term -> Maybe Machine
Term -> Term
Type
-> Integer -> Integer -> (Natural -> Natural -> Natural) -> Term
Type -> Integer -> (Natural -> Natural) -> Term
Type -> [Integer] -> ([Natural] -> Term) -> Term
Machine -> Term -> Maybe Machine
tcm :: PrimStepContext -> TyConMap
isSubj :: PrimStepContext -> Bool
pInfo :: PrimStepContext -> PrimInfo
tys :: PrimStepContext -> [Type]
args :: PrimStepContext -> [Value]
mach :: PrimStepContext -> Machine
ty :: PrimStepContext -> Type
checkNaturalRange1 :: PrimStepContext -> Type -> Integer -> (Natural -> Natural) -> Term
checkNaturalRange2 :: PrimStepContext
-> Type
-> Integer
-> Integer
-> (Natural -> Natural -> Natural)
-> Term
checkNaturalRange :: PrimStepContext -> Type -> [Integer] -> ([Natural] -> Term) -> Term
reduce :: PrimStepContext -> Term -> Maybe Machine
reduceWith :: PrimStepContext -> Machine -> Term -> Maybe Machine
reduceWHNF :: PrimStepContext -> Term -> Maybe Machine
reduceWHNF' :: PrimStepContext -> Machine -> Term -> Maybe Machine
catchDivByZero :: PrimStepContext -> Term -> Term
catchErrorCall :: PrimStepContext -> Term -> Term
tcm :: TyConMap
isSubj :: Bool
pInfo :: PrimInfo
tys :: [Type]
args :: [Value]
mach :: Machine
ty :: Type
checkNaturalRange1 :: Type -> Integer -> (Natural -> Natural) -> Term
checkNaturalRange2 :: Type
-> Integer -> Integer -> (Natural -> Natural -> Natural) -> Term
checkNaturalRange :: Type -> [Integer] -> ([Natural] -> Term) -> Term
reduce :: Term -> Maybe Machine
reduceWith :: Machine -> Term -> Maybe Machine
reduceWHNF :: Term -> Maybe Machine
reduceWHNF' :: Machine -> Term -> Maybe Machine
catchDivByZero :: Term -> Term
catchErrorCall :: Term -> Term
..}
        | Just (Type
_, Integer
kn) <- TyConMap -> [Type] -> Maybe (Type, Integer)
extractKnownNat TyConMap
tcm [Type]
tys
        , Just Term
val <- Integer
-> (forall (n :: Natural). KnownNat n => Proxy n -> Maybe Term)
-> Maybe Term
forall r.
Integer -> (forall (n :: Natural). KnownNat n => Proxy n -> r) -> r
reifyNat Integer
kn ((BitVector n -> BitVector n -> BitVector n)
-> Type -> TyConMap -> [Type] -> [Value] -> Proxy n -> Maybe Term
forall (n :: Natural).
KnownNat n =>
(BitVector n -> BitVector n -> BitVector n)
-> Type -> TyConMap -> [Type] -> [Value] -> Proxy n -> Maybe Term
liftBitVector2 (BitVector n -> BitVector n -> BitVector n
forall (n :: Natural).
KnownNat n =>
BitVector n -> BitVector n -> BitVector n
BitVector.quot#) Type
ty TyConMap
tcm [Type]
tys [Value]
args)
        -> Term -> Maybe Machine
reduce (Term -> Maybe Machine) -> Term -> Maybe Machine
forall a b. (a -> b) -> a -> b
$ Term -> Term
catchDivByZero Term
val
      PrimStepContext
_ -> Maybe Machine
forall a. Maybe a
Nothing

  , Text -> (PrimStepContext -> Maybe Machine) -> (Text, PrimStep)
primStepEntry $(textNameLit 'Clash.Sized.Internal.BitVector.rem#) ((PrimStepContext -> Maybe Machine) -> (Text, PrimStep))
-> (PrimStepContext -> Maybe Machine) -> (Text, PrimStep)
forall a b. (a -> b) -> a -> b
$ \case
      PrimStepContext{Bool
[Type]
[Value]
Type
TyConMap
Machine
PrimInfo
Term -> Maybe Machine
Term -> Term
Type
-> Integer -> Integer -> (Natural -> Natural -> Natural) -> Term
Type -> Integer -> (Natural -> Natural) -> Term
Type -> [Integer] -> ([Natural] -> Term) -> Term
Machine -> Term -> Maybe Machine
tcm :: PrimStepContext -> TyConMap
isSubj :: PrimStepContext -> Bool
pInfo :: PrimStepContext -> PrimInfo
tys :: PrimStepContext -> [Type]
args :: PrimStepContext -> [Value]
mach :: PrimStepContext -> Machine
ty :: PrimStepContext -> Type
checkNaturalRange1 :: PrimStepContext -> Type -> Integer -> (Natural -> Natural) -> Term
checkNaturalRange2 :: PrimStepContext
-> Type
-> Integer
-> Integer
-> (Natural -> Natural -> Natural)
-> Term
checkNaturalRange :: PrimStepContext -> Type -> [Integer] -> ([Natural] -> Term) -> Term
reduce :: PrimStepContext -> Term -> Maybe Machine
reduceWith :: PrimStepContext -> Machine -> Term -> Maybe Machine
reduceWHNF :: PrimStepContext -> Term -> Maybe Machine
reduceWHNF' :: PrimStepContext -> Machine -> Term -> Maybe Machine
catchDivByZero :: PrimStepContext -> Term -> Term
catchErrorCall :: PrimStepContext -> Term -> Term
tcm :: TyConMap
isSubj :: Bool
pInfo :: PrimInfo
tys :: [Type]
args :: [Value]
mach :: Machine
ty :: Type
checkNaturalRange1 :: Type -> Integer -> (Natural -> Natural) -> Term
checkNaturalRange2 :: Type
-> Integer -> Integer -> (Natural -> Natural -> Natural) -> Term
checkNaturalRange :: Type -> [Integer] -> ([Natural] -> Term) -> Term
reduce :: Term -> Maybe Machine
reduceWith :: Machine -> Term -> Maybe Machine
reduceWHNF :: Term -> Maybe Machine
reduceWHNF' :: Machine -> Term -> Maybe Machine
catchDivByZero :: Term -> Term
catchErrorCall :: Term -> Term
..}
        | Just (Type
_, Integer
kn) <- TyConMap -> [Type] -> Maybe (Type, Integer)
extractKnownNat TyConMap
tcm [Type]
tys
        , Just Term
val <- Integer
-> (forall (n :: Natural). KnownNat n => Proxy n -> Maybe Term)
-> Maybe Term
forall r.
Integer -> (forall (n :: Natural). KnownNat n => Proxy n -> r) -> r
reifyNat Integer
kn ((BitVector n -> BitVector n -> BitVector n)
-> Type -> TyConMap -> [Type] -> [Value] -> Proxy n -> Maybe Term
forall (n :: Natural).
KnownNat n =>
(BitVector n -> BitVector n -> BitVector n)
-> Type -> TyConMap -> [Type] -> [Value] -> Proxy n -> Maybe Term
liftBitVector2 (BitVector n -> BitVector n -> BitVector n
forall (n :: Natural).
KnownNat n =>
BitVector n -> BitVector n -> BitVector n
BitVector.rem#) Type
ty TyConMap
tcm [Type]
tys [Value]
args)
        -> Term -> Maybe Machine
reduce (Term -> Maybe Machine) -> Term -> Maybe Machine
forall a b. (a -> b) -> a -> b
$ Term -> Term
catchDivByZero Term
val
      PrimStepContext
_ -> Maybe Machine
forall a. Maybe a
Nothing

  , Text -> (PrimStepContext -> Maybe Machine) -> (Text, PrimStep)
primStepEntry $(textNameLit 'Clash.Sized.Internal.BitVector.toInteger#) ((PrimStepContext -> Maybe Machine) -> (Text, PrimStep))
-> (PrimStepContext -> Maybe Machine) -> (Text, PrimStep)
forall a b. (a -> b) -> a -> b
$ \case
      PrimStepContext{Bool
[Type]
[Value]
Type
TyConMap
Machine
PrimInfo
Term -> Maybe Machine
Term -> Term
Type
-> Integer -> Integer -> (Natural -> Natural -> Natural) -> Term
Type -> Integer -> (Natural -> Natural) -> Term
Type -> [Integer] -> ([Natural] -> Term) -> Term
Machine -> Term -> Maybe Machine
tcm :: PrimStepContext -> TyConMap
isSubj :: PrimStepContext -> Bool
pInfo :: PrimStepContext -> PrimInfo
tys :: PrimStepContext -> [Type]
args :: PrimStepContext -> [Value]
mach :: PrimStepContext -> Machine
ty :: PrimStepContext -> Type
checkNaturalRange1 :: PrimStepContext -> Type -> Integer -> (Natural -> Natural) -> Term
checkNaturalRange2 :: PrimStepContext
-> Type
-> Integer
-> Integer
-> (Natural -> Natural -> Natural)
-> Term
checkNaturalRange :: PrimStepContext -> Type -> [Integer] -> ([Natural] -> Term) -> Term
reduce :: PrimStepContext -> Term -> Maybe Machine
reduceWith :: PrimStepContext -> Machine -> Term -> Maybe Machine
reduceWHNF :: PrimStepContext -> Term -> Maybe Machine
reduceWHNF' :: PrimStepContext -> Machine -> Term -> Maybe Machine
catchDivByZero :: PrimStepContext -> Term -> Term
catchErrorCall :: PrimStepContext -> Term -> Term
tcm :: TyConMap
isSubj :: Bool
pInfo :: PrimInfo
tys :: [Type]
args :: [Value]
mach :: Machine
ty :: Type
checkNaturalRange1 :: Type -> Integer -> (Natural -> Natural) -> Term
checkNaturalRange2 :: Type
-> Integer -> Integer -> (Natural -> Natural -> Natural) -> Term
checkNaturalRange :: Type -> [Integer] -> ([Natural] -> Term) -> Term
reduce :: Term -> Maybe Machine
reduceWith :: Machine -> Term -> Maybe Machine
reduceWHNF :: Term -> Maybe Machine
reduceWHNF' :: Machine -> Term -> Maybe Machine
catchDivByZero :: Term -> Term
catchErrorCall :: Term -> Term
..}
        | Just (Type
_, Integer
kn) <- TyConMap -> [Type] -> Maybe (Type, Integer)
extractKnownNat TyConMap
tcm [Type]
tys
        , [(Integer, Integer)
i] <- [Value] -> [(Integer, Integer)]
bitVectorLiterals' [Value]
args
        -> let val :: Integer
val = Integer
-> (forall (n :: Natural). KnownNat n => Proxy n -> Integer)
-> Integer
forall r.
Integer -> (forall (n :: Natural). KnownNat n => Proxy n -> r) -> r
reifyNat Integer
kn (BitVector n -> Proxy n -> Integer
forall (n :: Natural).
KnownNat n =>
BitVector n -> Proxy n -> Integer
op ((Integer, Integer) -> BitVector n
forall (n :: Natural). (Integer, Integer) -> BitVector n
toBV (Integer, Integer)
i))
        in Term -> Maybe Machine
reduce (Integer -> Term
integerToIntegerLiteral Integer
val)
        where
          op :: KnownNat n => BitVector n -> Proxy n -> Integer
          op :: forall (n :: Natural).
KnownNat n =>
BitVector n -> Proxy n -> Integer
op BitVector n
u Proxy n
_ = BitVector n -> Integer
forall (n :: Natural). KnownNat n => BitVector n -> Integer
BitVector.toInteger# BitVector n
u
      PrimStepContext
_ -> Maybe Machine
forall a. Maybe a
Nothing


-- Bits
  , Text -> (PrimStepContext -> Maybe Machine) -> (Text, PrimStep)
primStepEntry $(textNameLit 'Clash.Sized.Internal.BitVector.and#) ((PrimStepContext -> Maybe Machine) -> (Text, PrimStep))
-> (PrimStepContext -> Maybe Machine) -> (Text, PrimStep)
forall a b. (a -> b) -> a -> b
$ \case
      PrimStepContext{Bool
[Type]
[Value]
Type
TyConMap
Machine
PrimInfo
Term -> Maybe Machine
Term -> Term
Type
-> Integer -> Integer -> (Natural -> Natural -> Natural) -> Term
Type -> Integer -> (Natural -> Natural) -> Term
Type -> [Integer] -> ([Natural] -> Term) -> Term
Machine -> Term -> Maybe Machine
tcm :: PrimStepContext -> TyConMap
isSubj :: PrimStepContext -> Bool
pInfo :: PrimStepContext -> PrimInfo
tys :: PrimStepContext -> [Type]
args :: PrimStepContext -> [Value]
mach :: PrimStepContext -> Machine
ty :: PrimStepContext -> Type
checkNaturalRange1 :: PrimStepContext -> Type -> Integer -> (Natural -> Natural) -> Term
checkNaturalRange2 :: PrimStepContext
-> Type
-> Integer
-> Integer
-> (Natural -> Natural -> Natural)
-> Term
checkNaturalRange :: PrimStepContext -> Type -> [Integer] -> ([Natural] -> Term) -> Term
reduce :: PrimStepContext -> Term -> Maybe Machine
reduceWith :: PrimStepContext -> Machine -> Term -> Maybe Machine
reduceWHNF :: PrimStepContext -> Term -> Maybe Machine
reduceWHNF' :: PrimStepContext -> Machine -> Term -> Maybe Machine
catchDivByZero :: PrimStepContext -> Term -> Term
catchErrorCall :: PrimStepContext -> Term -> Term
tcm :: TyConMap
isSubj :: Bool
pInfo :: PrimInfo
tys :: [Type]
args :: [Value]
mach :: Machine
ty :: Type
checkNaturalRange1 :: Type -> Integer -> (Natural -> Natural) -> Term
checkNaturalRange2 :: Type
-> Integer -> Integer -> (Natural -> Natural -> Natural) -> Term
checkNaturalRange :: Type -> [Integer] -> ([Natural] -> Term) -> Term
reduce :: Term -> Maybe Machine
reduceWith :: Machine -> Term -> Maybe Machine
reduceWHNF :: Term -> Maybe Machine
reduceWHNF' :: Machine -> Term -> Maybe Machine
catchDivByZero :: Term -> Term
catchErrorCall :: Term -> Term
..}
        | Just (Type
_, Integer
kn) <- TyConMap -> [Type] -> Maybe (Type, Integer)
extractKnownNat TyConMap
tcm [Type]
tys
        , Just Term
val <- Integer
-> (forall (n :: Natural). KnownNat n => Proxy n -> Maybe Term)
-> Maybe Term
forall r.
Integer -> (forall (n :: Natural). KnownNat n => Proxy n -> r) -> r
reifyNat Integer
kn ((BitVector n -> BitVector n -> BitVector n)
-> Type -> TyConMap -> [Type] -> [Value] -> Proxy n -> Maybe Term
forall (n :: Natural).
KnownNat n =>
(BitVector n -> BitVector n -> BitVector n)
-> Type -> TyConMap -> [Type] -> [Value] -> Proxy n -> Maybe Term
liftBitVector2 (BitVector n -> BitVector n -> BitVector n
forall (n :: Natural).
KnownNat n =>
BitVector n -> BitVector n -> BitVector n
BitVector.and#) Type
ty TyConMap
tcm [Type]
tys [Value]
args)
        -> Term -> Maybe Machine
reduce Term
val
      PrimStepContext
_ -> Maybe Machine
forall a. Maybe a
Nothing

  , Text -> (PrimStepContext -> Maybe Machine) -> (Text, PrimStep)
primStepEntry $(textNameLit 'Clash.Sized.Internal.BitVector.or#) ((PrimStepContext -> Maybe Machine) -> (Text, PrimStep))
-> (PrimStepContext -> Maybe Machine) -> (Text, PrimStep)
forall a b. (a -> b) -> a -> b
$ \case
      PrimStepContext{Bool
[Type]
[Value]
Type
TyConMap
Machine
PrimInfo
Term -> Maybe Machine
Term -> Term
Type
-> Integer -> Integer -> (Natural -> Natural -> Natural) -> Term
Type -> Integer -> (Natural -> Natural) -> Term
Type -> [Integer] -> ([Natural] -> Term) -> Term
Machine -> Term -> Maybe Machine
tcm :: PrimStepContext -> TyConMap
isSubj :: PrimStepContext -> Bool
pInfo :: PrimStepContext -> PrimInfo
tys :: PrimStepContext -> [Type]
args :: PrimStepContext -> [Value]
mach :: PrimStepContext -> Machine
ty :: PrimStepContext -> Type
checkNaturalRange1 :: PrimStepContext -> Type -> Integer -> (Natural -> Natural) -> Term
checkNaturalRange2 :: PrimStepContext
-> Type
-> Integer
-> Integer
-> (Natural -> Natural -> Natural)
-> Term
checkNaturalRange :: PrimStepContext -> Type -> [Integer] -> ([Natural] -> Term) -> Term
reduce :: PrimStepContext -> Term -> Maybe Machine
reduceWith :: PrimStepContext -> Machine -> Term -> Maybe Machine
reduceWHNF :: PrimStepContext -> Term -> Maybe Machine
reduceWHNF' :: PrimStepContext -> Machine -> Term -> Maybe Machine
catchDivByZero :: PrimStepContext -> Term -> Term
catchErrorCall :: PrimStepContext -> Term -> Term
tcm :: TyConMap
isSubj :: Bool
pInfo :: PrimInfo
tys :: [Type]
args :: [Value]
mach :: Machine
ty :: Type
checkNaturalRange1 :: Type -> Integer -> (Natural -> Natural) -> Term
checkNaturalRange2 :: Type
-> Integer -> Integer -> (Natural -> Natural -> Natural) -> Term
checkNaturalRange :: Type -> [Integer] -> ([Natural] -> Term) -> Term
reduce :: Term -> Maybe Machine
reduceWith :: Machine -> Term -> Maybe Machine
reduceWHNF :: Term -> Maybe Machine
reduceWHNF' :: Machine -> Term -> Maybe Machine
catchDivByZero :: Term -> Term
catchErrorCall :: Term -> Term
..}
        | Just (Type
_, Integer
kn) <- TyConMap -> [Type] -> Maybe (Type, Integer)
extractKnownNat TyConMap
tcm [Type]
tys
        , Just Term
val <- Integer
-> (forall (n :: Natural). KnownNat n => Proxy n -> Maybe Term)
-> Maybe Term
forall r.
Integer -> (forall (n :: Natural). KnownNat n => Proxy n -> r) -> r
reifyNat Integer
kn ((BitVector n -> BitVector n -> BitVector n)
-> Type -> TyConMap -> [Type] -> [Value] -> Proxy n -> Maybe Term
forall (n :: Natural).
KnownNat n =>
(BitVector n -> BitVector n -> BitVector n)
-> Type -> TyConMap -> [Type] -> [Value] -> Proxy n -> Maybe Term
liftBitVector2 (BitVector n -> BitVector n -> BitVector n
forall (n :: Natural).
KnownNat n =>
BitVector n -> BitVector n -> BitVector n
BitVector.or#) Type
ty TyConMap
tcm [Type]
tys [Value]
args)
        -> Term -> Maybe Machine
reduce Term
val
      PrimStepContext
_ -> Maybe Machine
forall a. Maybe a
Nothing

  , Text -> (PrimStepContext -> Maybe Machine) -> (Text, PrimStep)
primStepEntry $(textNameLit 'Clash.Sized.Internal.BitVector.xor#) ((PrimStepContext -> Maybe Machine) -> (Text, PrimStep))
-> (PrimStepContext -> Maybe Machine) -> (Text, PrimStep)
forall a b. (a -> b) -> a -> b
$ \case
      PrimStepContext{Bool
[Type]
[Value]
Type
TyConMap
Machine
PrimInfo
Term -> Maybe Machine
Term -> Term
Type
-> Integer -> Integer -> (Natural -> Natural -> Natural) -> Term
Type -> Integer -> (Natural -> Natural) -> Term
Type -> [Integer] -> ([Natural] -> Term) -> Term
Machine -> Term -> Maybe Machine
tcm :: PrimStepContext -> TyConMap
isSubj :: PrimStepContext -> Bool
pInfo :: PrimStepContext -> PrimInfo
tys :: PrimStepContext -> [Type]
args :: PrimStepContext -> [Value]
mach :: PrimStepContext -> Machine
ty :: PrimStepContext -> Type
checkNaturalRange1 :: PrimStepContext -> Type -> Integer -> (Natural -> Natural) -> Term
checkNaturalRange2 :: PrimStepContext
-> Type
-> Integer
-> Integer
-> (Natural -> Natural -> Natural)
-> Term
checkNaturalRange :: PrimStepContext -> Type -> [Integer] -> ([Natural] -> Term) -> Term
reduce :: PrimStepContext -> Term -> Maybe Machine
reduceWith :: PrimStepContext -> Machine -> Term -> Maybe Machine
reduceWHNF :: PrimStepContext -> Term -> Maybe Machine
reduceWHNF' :: PrimStepContext -> Machine -> Term -> Maybe Machine
catchDivByZero :: PrimStepContext -> Term -> Term
catchErrorCall :: PrimStepContext -> Term -> Term
tcm :: TyConMap
isSubj :: Bool
pInfo :: PrimInfo
tys :: [Type]
args :: [Value]
mach :: Machine
ty :: Type
checkNaturalRange1 :: Type -> Integer -> (Natural -> Natural) -> Term
checkNaturalRange2 :: Type
-> Integer -> Integer -> (Natural -> Natural -> Natural) -> Term
checkNaturalRange :: Type -> [Integer] -> ([Natural] -> Term) -> Term
reduce :: Term -> Maybe Machine
reduceWith :: Machine -> Term -> Maybe Machine
reduceWHNF :: Term -> Maybe Machine
reduceWHNF' :: Machine -> Term -> Maybe Machine
catchDivByZero :: Term -> Term
catchErrorCall :: Term -> Term
..}
        | Just (Type
_, Integer
kn) <- TyConMap -> [Type] -> Maybe (Type, Integer)
extractKnownNat TyConMap
tcm [Type]
tys
        , Just Term
val <- Integer
-> (forall (n :: Natural). KnownNat n => Proxy n -> Maybe Term)
-> Maybe Term
forall r.
Integer -> (forall (n :: Natural). KnownNat n => Proxy n -> r) -> r
reifyNat Integer
kn ((BitVector n -> BitVector n -> BitVector n)
-> Type -> TyConMap -> [Type] -> [Value] -> Proxy n -> Maybe Term
forall (n :: Natural).
KnownNat n =>
(BitVector n -> BitVector n -> BitVector n)
-> Type -> TyConMap -> [Type] -> [Value] -> Proxy n -> Maybe Term
liftBitVector2 (BitVector n -> BitVector n -> BitVector n
forall (n :: Natural).
KnownNat n =>
BitVector n -> BitVector n -> BitVector n
BitVector.xor#) Type
ty TyConMap
tcm [Type]
tys [Value]
args)
        -> Term -> Maybe Machine
reduce Term
val
      PrimStepContext
_ -> Maybe Machine
forall a. Maybe a
Nothing

  , Text -> (PrimStepContext -> Maybe Machine) -> (Text, PrimStep)
primStepEntry $(textNameLit 'Clash.Sized.Internal.BitVector.complement#) ((PrimStepContext -> Maybe Machine) -> (Text, PrimStep))
-> (PrimStepContext -> Maybe Machine) -> (Text, PrimStep)
forall a b. (a -> b) -> a -> b
$ \case
      PrimStepContext{Bool
[Type]
[Value]
Type
TyConMap
Machine
PrimInfo
Term -> Maybe Machine
Term -> Term
Type
-> Integer -> Integer -> (Natural -> Natural -> Natural) -> Term
Type -> Integer -> (Natural -> Natural) -> Term
Type -> [Integer] -> ([Natural] -> Term) -> Term
Machine -> Term -> Maybe Machine
tcm :: PrimStepContext -> TyConMap
isSubj :: PrimStepContext -> Bool
pInfo :: PrimStepContext -> PrimInfo
tys :: PrimStepContext -> [Type]
args :: PrimStepContext -> [Value]
mach :: PrimStepContext -> Machine
ty :: PrimStepContext -> Type
checkNaturalRange1 :: PrimStepContext -> Type -> Integer -> (Natural -> Natural) -> Term
checkNaturalRange2 :: PrimStepContext
-> Type
-> Integer
-> Integer
-> (Natural -> Natural -> Natural)
-> Term
checkNaturalRange :: PrimStepContext -> Type -> [Integer] -> ([Natural] -> Term) -> Term
reduce :: PrimStepContext -> Term -> Maybe Machine
reduceWith :: PrimStepContext -> Machine -> Term -> Maybe Machine
reduceWHNF :: PrimStepContext -> Term -> Maybe Machine
reduceWHNF' :: PrimStepContext -> Machine -> Term -> Maybe Machine
catchDivByZero :: PrimStepContext -> Term -> Term
catchErrorCall :: PrimStepContext -> Term -> Term
tcm :: TyConMap
isSubj :: Bool
pInfo :: PrimInfo
tys :: [Type]
args :: [Value]
mach :: Machine
ty :: Type
checkNaturalRange1 :: Type -> Integer -> (Natural -> Natural) -> Term
checkNaturalRange2 :: Type
-> Integer -> Integer -> (Natural -> Natural -> Natural) -> Term
checkNaturalRange :: Type -> [Integer] -> ([Natural] -> Term) -> Term
reduce :: Term -> Maybe Machine
reduceWith :: Machine -> Term -> Maybe Machine
reduceWHNF :: Term -> Maybe Machine
reduceWHNF' :: Machine -> Term -> Maybe Machine
catchDivByZero :: Term -> Term
catchErrorCall :: Term -> Term
..}
        | [(Integer, Integer)
i] <- [Value] -> [(Integer, Integer)]
bitVectorLiterals' [Value]
args
        , Just (Type
nTy, Integer
kn) <- TyConMap -> [Type] -> Maybe (Type, Integer)
extractKnownNat TyConMap
tcm [Type]
tys
        -> let (Integer
msk,Integer
val) = Integer
-> (forall (n :: Natural).
    KnownNat n =>
    Proxy n -> (Integer, Integer))
-> (Integer, Integer)
forall r.
Integer -> (forall (n :: Natural). KnownNat n => Proxy n -> r) -> r
reifyNat Integer
kn (BitVector n -> Proxy n -> (Integer, Integer)
forall (n :: Natural).
KnownNat n =>
BitVector n -> Proxy n -> (Integer, Integer)
op ((Integer, Integer) -> BitVector n
forall (n :: Natural). (Integer, Integer) -> BitVector n
toBV (Integer, Integer)
i))
        in Term -> Maybe Machine
reduce (Type -> Type -> Integer -> Integer -> Integer -> Term
mkBitVectorLit Type
ty Type
nTy Integer
kn Integer
msk Integer
val)
        where
          op :: KnownNat n => BitVector n -> Proxy n -> (Integer,Integer)
          op :: forall (n :: Natural).
KnownNat n =>
BitVector n -> Proxy n -> (Integer, Integer)
op BitVector n
u Proxy n
_ = BitVector n -> (Integer, Integer)
forall (n :: Natural). BitVector n -> (Integer, Integer)
splitBV (BitVector n -> (Integer, Integer))
-> BitVector n -> (Integer, Integer)
forall a b. (a -> b) -> a -> b
$ BitVector n -> BitVector n
forall (n :: Natural). KnownNat n => BitVector n -> BitVector n
BitVector.complement# BitVector n
u
      PrimStepContext
_ -> Maybe Machine
forall a. Maybe a
Nothing

  , Text -> (PrimStepContext -> Maybe Machine) -> (Text, PrimStep)
primStepEntry $(textNameLit 'Clash.Sized.Internal.BitVector.shiftL#) ((PrimStepContext -> Maybe Machine) -> (Text, PrimStep))
-> (PrimStepContext -> Maybe Machine) -> (Text, PrimStep)
forall a b. (a -> b) -> a -> b
$ \case
      PrimStepContext{Bool
[Type]
[Value]
Type
TyConMap
Machine
PrimInfo
Term -> Maybe Machine
Term -> Term
Type
-> Integer -> Integer -> (Natural -> Natural -> Natural) -> Term
Type -> Integer -> (Natural -> Natural) -> Term
Type -> [Integer] -> ([Natural] -> Term) -> Term
Machine -> Term -> Maybe Machine
tcm :: PrimStepContext -> TyConMap
isSubj :: PrimStepContext -> Bool
pInfo :: PrimStepContext -> PrimInfo
tys :: PrimStepContext -> [Type]
args :: PrimStepContext -> [Value]
mach :: PrimStepContext -> Machine
ty :: PrimStepContext -> Type
checkNaturalRange1 :: PrimStepContext -> Type -> Integer -> (Natural -> Natural) -> Term
checkNaturalRange2 :: PrimStepContext
-> Type
-> Integer
-> Integer
-> (Natural -> Natural -> Natural)
-> Term
checkNaturalRange :: PrimStepContext -> Type -> [Integer] -> ([Natural] -> Term) -> Term
reduce :: PrimStepContext -> Term -> Maybe Machine
reduceWith :: PrimStepContext -> Machine -> Term -> Maybe Machine
reduceWHNF :: PrimStepContext -> Term -> Maybe Machine
reduceWHNF' :: PrimStepContext -> Machine -> Term -> Maybe Machine
catchDivByZero :: PrimStepContext -> Term -> Term
catchErrorCall :: PrimStepContext -> Term -> Term
tcm :: TyConMap
isSubj :: Bool
pInfo :: PrimInfo
tys :: [Type]
args :: [Value]
mach :: Machine
ty :: Type
checkNaturalRange1 :: Type -> Integer -> (Natural -> Natural) -> Term
checkNaturalRange2 :: Type
-> Integer -> Integer -> (Natural -> Natural -> Natural) -> Term
checkNaturalRange :: Type -> [Integer] -> ([Natural] -> Term) -> Term
reduce :: Term -> Maybe Machine
reduceWith :: Machine -> Term -> Maybe Machine
reduceWHNF :: Term -> Maybe Machine
reduceWHNF' :: Machine -> Term -> Maybe Machine
catchDivByZero :: Term -> Term
catchErrorCall :: Term -> Term
..}
        | Just (Type
nTy,Integer
kn,(Integer, Integer)
i,Integer
j) <- TyConMap
-> [Type]
-> [Value]
-> Maybe (Type, Integer, (Integer, Integer), Integer)
bitVectorLitIntLit TyConMap
tcm [Type]
tys [Value]
args
          -> let (Integer
msk,Integer
val) = Integer
-> (forall (n :: Natural).
    KnownNat n =>
    Proxy n -> (Integer, Integer))
-> (Integer, Integer)
forall r.
Integer -> (forall (n :: Natural). KnownNat n => Proxy n -> r) -> r
reifyNat Integer
kn (BitVector n -> Int -> Proxy n -> (Integer, Integer)
forall (n :: Natural).
KnownNat n =>
BitVector n -> Int -> Proxy n -> (Integer, Integer)
op ((Integer, Integer) -> BitVector n
forall (n :: Natural). (Integer, Integer) -> BitVector n
toBV (Integer, Integer)
i) (Integer -> Int
forall a. Num a => Integer -> a
fromInteger Integer
j))
          in Term -> Maybe Machine
reduce (Type -> Type -> Integer -> Integer -> Integer -> Term
mkBitVectorLit Type
ty Type
nTy Integer
kn Integer
msk Integer
val)
          where
            op :: KnownNat n => BitVector n -> Int -> Proxy n -> (Integer,Integer)
            op :: forall (n :: Natural).
KnownNat n =>
BitVector n -> Int -> Proxy n -> (Integer, Integer)
op BitVector n
u Int
i Proxy n
_ = BitVector n -> (Integer, Integer)
forall (n :: Natural). BitVector n -> (Integer, Integer)
splitBV (BitVector n -> Int -> BitVector n
forall (n :: Natural).
KnownNat n =>
BitVector n -> Int -> BitVector n
BitVector.shiftL# BitVector n
u Int
i)
      PrimStepContext
_ -> Maybe Machine
forall a. Maybe a
Nothing

  , Text -> (PrimStepContext -> Maybe Machine) -> (Text, PrimStep)
primStepEntry $(textNameLit 'Clash.Sized.Internal.BitVector.shiftR#) ((PrimStepContext -> Maybe Machine) -> (Text, PrimStep))
-> (PrimStepContext -> Maybe Machine) -> (Text, PrimStep)
forall a b. (a -> b) -> a -> b
$ \case
      PrimStepContext{Bool
[Type]
[Value]
Type
TyConMap
Machine
PrimInfo
Term -> Maybe Machine
Term -> Term
Type
-> Integer -> Integer -> (Natural -> Natural -> Natural) -> Term
Type -> Integer -> (Natural -> Natural) -> Term
Type -> [Integer] -> ([Natural] -> Term) -> Term
Machine -> Term -> Maybe Machine
tcm :: PrimStepContext -> TyConMap
isSubj :: PrimStepContext -> Bool
pInfo :: PrimStepContext -> PrimInfo
tys :: PrimStepContext -> [Type]
args :: PrimStepContext -> [Value]
mach :: PrimStepContext -> Machine
ty :: PrimStepContext -> Type
checkNaturalRange1 :: PrimStepContext -> Type -> Integer -> (Natural -> Natural) -> Term
checkNaturalRange2 :: PrimStepContext
-> Type
-> Integer
-> Integer
-> (Natural -> Natural -> Natural)
-> Term
checkNaturalRange :: PrimStepContext -> Type -> [Integer] -> ([Natural] -> Term) -> Term
reduce :: PrimStepContext -> Term -> Maybe Machine
reduceWith :: PrimStepContext -> Machine -> Term -> Maybe Machine
reduceWHNF :: PrimStepContext -> Term -> Maybe Machine
reduceWHNF' :: PrimStepContext -> Machine -> Term -> Maybe Machine
catchDivByZero :: PrimStepContext -> Term -> Term
catchErrorCall :: PrimStepContext -> Term -> Term
tcm :: TyConMap
isSubj :: Bool
pInfo :: PrimInfo
tys :: [Type]
args :: [Value]
mach :: Machine
ty :: Type
checkNaturalRange1 :: Type -> Integer -> (Natural -> Natural) -> Term
checkNaturalRange2 :: Type
-> Integer -> Integer -> (Natural -> Natural -> Natural) -> Term
checkNaturalRange :: Type -> [Integer] -> ([Natural] -> Term) -> Term
reduce :: Term -> Maybe Machine
reduceWith :: Machine -> Term -> Maybe Machine
reduceWHNF :: Term -> Maybe Machine
reduceWHNF' :: Machine -> Term -> Maybe Machine
catchDivByZero :: Term -> Term
catchErrorCall :: Term -> Term
..}
        | Just (Type
nTy,Integer
kn,(Integer, Integer)
i,Integer
j) <- TyConMap
-> [Type]
-> [Value]
-> Maybe (Type, Integer, (Integer, Integer), Integer)
bitVectorLitIntLit TyConMap
tcm [Type]
tys [Value]
args
          -> let (Integer
msk,Integer
val) = Integer
-> (forall (n :: Natural).
    KnownNat n =>
    Proxy n -> (Integer, Integer))
-> (Integer, Integer)
forall r.
Integer -> (forall (n :: Natural). KnownNat n => Proxy n -> r) -> r
reifyNat Integer
kn (BitVector n -> Int -> Proxy n -> (Integer, Integer)
forall (n :: Natural).
KnownNat n =>
BitVector n -> Int -> Proxy n -> (Integer, Integer)
op ((Integer, Integer) -> BitVector n
forall (n :: Natural). (Integer, Integer) -> BitVector n
toBV (Integer, Integer)
i) (Integer -> Int
forall a. Num a => Integer -> a
fromInteger Integer
j))
          in Term -> Maybe Machine
reduce (Type -> Type -> Integer -> Integer -> Integer -> Term
mkBitVectorLit Type
ty Type
nTy Integer
kn Integer
msk Integer
val)
          where
            op :: KnownNat n => BitVector n -> Int -> Proxy n -> (Integer,Integer)
            op :: forall (n :: Natural).
KnownNat n =>
BitVector n -> Int -> Proxy n -> (Integer, Integer)
op BitVector n
u Int
i Proxy n
_ = BitVector n -> (Integer, Integer)
forall (n :: Natural). BitVector n -> (Integer, Integer)
splitBV (BitVector n -> Int -> BitVector n
forall (n :: Natural).
KnownNat n =>
BitVector n -> Int -> BitVector n
BitVector.shiftR# BitVector n
u Int
i)
      PrimStepContext
_ -> Maybe Machine
forall a. Maybe a
Nothing

  , Text -> (PrimStepContext -> Maybe Machine) -> (Text, PrimStep)
primStepEntry $(textNameLit 'Clash.Sized.Internal.BitVector.rotateL#) ((PrimStepContext -> Maybe Machine) -> (Text, PrimStep))
-> (PrimStepContext -> Maybe Machine) -> (Text, PrimStep)
forall a b. (a -> b) -> a -> b
$ \case
      PrimStepContext{Bool
[Type]
[Value]
Type
TyConMap
Machine
PrimInfo
Term -> Maybe Machine
Term -> Term
Type
-> Integer -> Integer -> (Natural -> Natural -> Natural) -> Term
Type -> Integer -> (Natural -> Natural) -> Term
Type -> [Integer] -> ([Natural] -> Term) -> Term
Machine -> Term -> Maybe Machine
tcm :: PrimStepContext -> TyConMap
isSubj :: PrimStepContext -> Bool
pInfo :: PrimStepContext -> PrimInfo
tys :: PrimStepContext -> [Type]
args :: PrimStepContext -> [Value]
mach :: PrimStepContext -> Machine
ty :: PrimStepContext -> Type
checkNaturalRange1 :: PrimStepContext -> Type -> Integer -> (Natural -> Natural) -> Term
checkNaturalRange2 :: PrimStepContext
-> Type
-> Integer
-> Integer
-> (Natural -> Natural -> Natural)
-> Term
checkNaturalRange :: PrimStepContext -> Type -> [Integer] -> ([Natural] -> Term) -> Term
reduce :: PrimStepContext -> Term -> Maybe Machine
reduceWith :: PrimStepContext -> Machine -> Term -> Maybe Machine
reduceWHNF :: PrimStepContext -> Term -> Maybe Machine
reduceWHNF' :: PrimStepContext -> Machine -> Term -> Maybe Machine
catchDivByZero :: PrimStepContext -> Term -> Term
catchErrorCall :: PrimStepContext -> Term -> Term
tcm :: TyConMap
isSubj :: Bool
pInfo :: PrimInfo
tys :: [Type]
args :: [Value]
mach :: Machine
ty :: Type
checkNaturalRange1 :: Type -> Integer -> (Natural -> Natural) -> Term
checkNaturalRange2 :: Type
-> Integer -> Integer -> (Natural -> Natural -> Natural) -> Term
checkNaturalRange :: Type -> [Integer] -> ([Natural] -> Term) -> Term
reduce :: Term -> Maybe Machine
reduceWith :: Machine -> Term -> Maybe Machine
reduceWHNF :: Term -> Maybe Machine
reduceWHNF' :: Machine -> Term -> Maybe Machine
catchDivByZero :: Term -> Term
catchErrorCall :: Term -> Term
..}
        | Just (Type
nTy,Integer
kn,(Integer, Integer)
i,Integer
j) <- TyConMap
-> [Type]
-> [Value]
-> Maybe (Type, Integer, (Integer, Integer), Integer)
bitVectorLitIntLit TyConMap
tcm [Type]
tys [Value]
args
          -> let (Integer
msk,Integer
val) = Integer
-> (forall (n :: Natural).
    KnownNat n =>
    Proxy n -> (Integer, Integer))
-> (Integer, Integer)
forall r.
Integer -> (forall (n :: Natural). KnownNat n => Proxy n -> r) -> r
reifyNat Integer
kn (BitVector n -> Int -> Proxy n -> (Integer, Integer)
forall (n :: Natural).
KnownNat n =>
BitVector n -> Int -> Proxy n -> (Integer, Integer)
op ((Integer, Integer) -> BitVector n
forall (n :: Natural). (Integer, Integer) -> BitVector n
toBV (Integer, Integer)
i) (Integer -> Int
forall a. Num a => Integer -> a
fromInteger Integer
j))
          in Term -> Maybe Machine
reduce (Type -> Type -> Integer -> Integer -> Integer -> Term
mkBitVectorLit Type
ty Type
nTy Integer
kn Integer
msk Integer
val)
          where
            op :: KnownNat n => BitVector n -> Int -> Proxy n -> (Integer,Integer)
            op :: forall (n :: Natural).
KnownNat n =>
BitVector n -> Int -> Proxy n -> (Integer, Integer)
op BitVector n
u Int
i Proxy n
_ = BitVector n -> (Integer, Integer)
forall (n :: Natural). BitVector n -> (Integer, Integer)
splitBV (BitVector n -> Int -> BitVector n
forall (n :: Natural).
KnownNat n =>
BitVector n -> Int -> BitVector n
BitVector.rotateL# BitVector n
u Int
i)
      PrimStepContext
_ -> Maybe Machine
forall a. Maybe a
Nothing

  , Text -> (PrimStepContext -> Maybe Machine) -> (Text, PrimStep)
primStepEntry $(textNameLit 'Clash.Sized.Internal.BitVector.rotateR#) ((PrimStepContext -> Maybe Machine) -> (Text, PrimStep))
-> (PrimStepContext -> Maybe Machine) -> (Text, PrimStep)
forall a b. (a -> b) -> a -> b
$ \case
      PrimStepContext{Bool
[Type]
[Value]
Type
TyConMap
Machine
PrimInfo
Term -> Maybe Machine
Term -> Term
Type
-> Integer -> Integer -> (Natural -> Natural -> Natural) -> Term
Type -> Integer -> (Natural -> Natural) -> Term
Type -> [Integer] -> ([Natural] -> Term) -> Term
Machine -> Term -> Maybe Machine
tcm :: PrimStepContext -> TyConMap
isSubj :: PrimStepContext -> Bool
pInfo :: PrimStepContext -> PrimInfo
tys :: PrimStepContext -> [Type]
args :: PrimStepContext -> [Value]
mach :: PrimStepContext -> Machine
ty :: PrimStepContext -> Type
checkNaturalRange1 :: PrimStepContext -> Type -> Integer -> (Natural -> Natural) -> Term
checkNaturalRange2 :: PrimStepContext
-> Type
-> Integer
-> Integer
-> (Natural -> Natural -> Natural)
-> Term
checkNaturalRange :: PrimStepContext -> Type -> [Integer] -> ([Natural] -> Term) -> Term
reduce :: PrimStepContext -> Term -> Maybe Machine
reduceWith :: PrimStepContext -> Machine -> Term -> Maybe Machine
reduceWHNF :: PrimStepContext -> Term -> Maybe Machine
reduceWHNF' :: PrimStepContext -> Machine -> Term -> Maybe Machine
catchDivByZero :: PrimStepContext -> Term -> Term
catchErrorCall :: PrimStepContext -> Term -> Term
tcm :: TyConMap
isSubj :: Bool
pInfo :: PrimInfo
tys :: [Type]
args :: [Value]
mach :: Machine
ty :: Type
checkNaturalRange1 :: Type -> Integer -> (Natural -> Natural) -> Term
checkNaturalRange2 :: Type
-> Integer -> Integer -> (Natural -> Natural -> Natural) -> Term
checkNaturalRange :: Type -> [Integer] -> ([Natural] -> Term) -> Term
reduce :: Term -> Maybe Machine
reduceWith :: Machine -> Term -> Maybe Machine
reduceWHNF :: Term -> Maybe Machine
reduceWHNF' :: Machine -> Term -> Maybe Machine
catchDivByZero :: Term -> Term
catchErrorCall :: Term -> Term
..}
        | Just (Type
nTy,Integer
kn,(Integer, Integer)
i,Integer
j) <- TyConMap
-> [Type]
-> [Value]
-> Maybe (Type, Integer, (Integer, Integer), Integer)
bitVectorLitIntLit TyConMap
tcm [Type]
tys [Value]
args
          -> let (Integer
msk,Integer
val) = Integer
-> (forall (n :: Natural).
    KnownNat n =>
    Proxy n -> (Integer, Integer))
-> (Integer, Integer)
forall r.
Integer -> (forall (n :: Natural). KnownNat n => Proxy n -> r) -> r
reifyNat Integer
kn (BitVector n -> Int -> Proxy n -> (Integer, Integer)
forall (n :: Natural).
KnownNat n =>
BitVector n -> Int -> Proxy n -> (Integer, Integer)
op ((Integer, Integer) -> BitVector n
forall (n :: Natural). (Integer, Integer) -> BitVector n
toBV (Integer, Integer)
i) (Integer -> Int
forall a. Num a => Integer -> a
fromInteger Integer
j))
          in Term -> Maybe Machine
reduce (Type -> Type -> Integer -> Integer -> Integer -> Term
mkBitVectorLit Type
ty Type
nTy Integer
kn Integer
msk Integer
val)
          where
            op :: KnownNat n => BitVector n -> Int -> Proxy n -> (Integer,Integer)
            op :: forall (n :: Natural).
KnownNat n =>
BitVector n -> Int -> Proxy n -> (Integer, Integer)
op BitVector n
u Int
i Proxy n
_ = BitVector n -> (Integer, Integer)
forall (n :: Natural). BitVector n -> (Integer, Integer)
splitBV (BitVector n -> Int -> BitVector n
forall (n :: Natural).
KnownNat n =>
BitVector n -> Int -> BitVector n
BitVector.rotateR# BitVector n
u Int
i)
      PrimStepContext
_ -> Maybe Machine
forall a. Maybe a
Nothing


-- truncateB
  , Text -> (PrimStepContext -> Maybe Machine) -> (Text, PrimStep)
primStepEntry $(textNameLit 'Clash.Sized.Internal.BitVector.truncateB#) ((PrimStepContext -> Maybe Machine) -> (Text, PrimStep))
-> (PrimStepContext -> Maybe Machine) -> (Text, PrimStep)
forall a b. (a -> b) -> a -> b
$ \case
      PrimStepContext{Bool
[Type]
[Value]
Type
TyConMap
Machine
PrimInfo
Term -> Maybe Machine
Term -> Term
Type
-> Integer -> Integer -> (Natural -> Natural -> Natural) -> Term
Type -> Integer -> (Natural -> Natural) -> Term
Type -> [Integer] -> ([Natural] -> Term) -> Term
Machine -> Term -> Maybe Machine
tcm :: PrimStepContext -> TyConMap
isSubj :: PrimStepContext -> Bool
pInfo :: PrimStepContext -> PrimInfo
tys :: PrimStepContext -> [Type]
args :: PrimStepContext -> [Value]
mach :: PrimStepContext -> Machine
ty :: PrimStepContext -> Type
checkNaturalRange1 :: PrimStepContext -> Type -> Integer -> (Natural -> Natural) -> Term
checkNaturalRange2 :: PrimStepContext
-> Type
-> Integer
-> Integer
-> (Natural -> Natural -> Natural)
-> Term
checkNaturalRange :: PrimStepContext -> Type -> [Integer] -> ([Natural] -> Term) -> Term
reduce :: PrimStepContext -> Term -> Maybe Machine
reduceWith :: PrimStepContext -> Machine -> Term -> Maybe Machine
reduceWHNF :: PrimStepContext -> Term -> Maybe Machine
reduceWHNF' :: PrimStepContext -> Machine -> Term -> Maybe Machine
catchDivByZero :: PrimStepContext -> Term -> Term
catchErrorCall :: PrimStepContext -> Term -> Term
tcm :: TyConMap
isSubj :: Bool
pInfo :: PrimInfo
tys :: [Type]
args :: [Value]
mach :: Machine
ty :: Type
checkNaturalRange1 :: Type -> Integer -> (Natural -> Natural) -> Term
checkNaturalRange2 :: Type
-> Integer -> Integer -> (Natural -> Natural -> Natural) -> Term
checkNaturalRange :: Type -> [Integer] -> ([Natural] -> Term) -> Term
reduce :: Term -> Maybe Machine
reduceWith :: Machine -> Term -> Maybe Machine
reduceWHNF :: Term -> Maybe Machine
reduceWHNF' :: Machine -> Term -> Maybe Machine
catchDivByZero :: Term -> Term
catchErrorCall :: Term -> Term
..} -- forall a b . KnownNat a => BitVector (a + b) -> BitVector a
        | Type
aTy  : [Type]
_ <- [Type]
tys
        , Right Integer
ka <- Except String Integer -> Either String Integer
forall e a. Except e a -> Either e a
runExcept (TyConMap -> Type -> Except String Integer
tyNatSize TyConMap
tcm Type
aTy)
        , [(Integer
mski,Integer
i)] <- [Value] -> [(Integer, Integer)]
bitVectorLiterals' [Value]
args
        -> let bitsKeep :: Integer
bitsKeep = (Int -> Integer
forall a. Bits a => Int -> a
bit (Integer -> Int
forall a. Num a => Integer -> a
fromInteger Integer
ka)) Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
- Integer
1
               val :: Integer
val = Integer
i Integer -> Integer -> Integer
forall a. Bits a => a -> a -> a
.&. Integer
bitsKeep
               msk :: Integer
msk = Integer
mski Integer -> Integer -> Integer
forall a. Bits a => a -> a -> a
.&. Integer
bitsKeep
        in Term -> Maybe Machine
reduce (Type -> Type -> Integer -> Integer -> Integer -> Term
mkBitVectorLit Type
ty Type
aTy Integer
ka Integer
msk Integer
val)
      PrimStepContext
_ -> Maybe Machine
forall a. Maybe a
Nothing

  ]