{-|
  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 GeneralizedNewtypeDeriving #-}
{-# LANGUAGE LambdaCase #-}
{-# LANGUAGE MagicHash #-}
{-# LANGUAGE OverloadedStrings #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE RecordWildCards #-}
{-# LANGUAGE TemplateHaskell #-}
{-# LANGUAGE UnboxedTuples #-}

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

module Clash.GHC.Evaluator.Primitive.Util where

import           Control.DeepSeq            (force)
import           Control.Exception          (ArithException(..), ErrorCall, Exception, tryJust, evaluate)
import           Control.Monad.State.Strict (State, MonadState)
import qualified Control.Monad.State.Strict as State
import           Control.Monad.Trans.Except (runExcept)
import           Data.Bits
import qualified Data.Either         as Either
import           Data.Maybe (fromMaybe, mapMaybe)
import qualified Data.Primitive.ByteArray as BA
import           Data.Proxy          (Proxy)
import           Data.Text           (Text)
import qualified Data.Text           as Text
import           Data.Text.Extra     (showt)
import           GHC.Float
import           GHC.Int
import GHC.Num.Integer (Integer (..))
import           GHC.Natural
import           GHC.Prim
import           GHC.TypeLits        (KnownNat)
import           GHC.Types           (IO (..))
import           GHC.Word
import           System.IO.Unsafe    (unsafeDupablePerformIO)

import           GHC.Types.Basic     (Boxity (..))
import           GHC.Types.Name      (getSrcSpan, nameOccName, occNameString)
import           GHC.Builtin.Names   (trueDataConKey, falseDataConKey)
import qualified GHC.Core.TyCon      as TyCon
import           GHC.Builtin.Types   (tupleTyCon)

import           Clash.Core.DataCon  (DataCon (..))
import           Clash.Core.Evaluator.Types
import Clash.Core.HasType (piResultTys)
import           Clash.Core.Literal  (Literal (..))
import           Clash.Core.Name
  (Name (..), NameSort (..), mkUnsafeSystemName)
import           Clash.Core.Pretty   (showPpr)
import Clash.Core.Term
  (IsMultiPrim (..),
   PrimInfo (..),
   Term (..),
   WorkInfo (..),
   mkApps,
   PrimUnfolding(..))
import Clash.Core.Type
  (Type (..),
   LitTy (..),
   TypeView (..),
   mkFunTy,
   mkTyConApp,
   splitFunForallTy,
   tyView)
import           Clash.Core.TyCon
  (TyConMap, TyConName, tyConDataCons)
import           Clash.Core.TysPrim
import Clash.Core.Util (tyNatSize)
import Clash.Core.Var (mkTyVar)
import qualified Clash.Data.UniqMap as UniqMap
import           Clash.Debug
import           Clash.GHC.GHC2Core  (modNameM)
import           Clash.Unique        (fromGhcUnique)
import Clash.Util (MonadUnique (..), curLoc)
import           Clash.Util.Supply   (Supply,freshId)
import Clash.Normalize.PrimitiveReductions (typeNatAdd)

import qualified Clash.Normalize.Primitives as NP
import Clash.Sized.Internal.BitVector(BitVector(..), Bit(..))
import Clash.Sized.Internal.Signed   (Signed   (..))
import Clash.Sized.Internal.Unsigned (Unsigned (..))
import Clash.XException (isX)

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

import qualified Clash.Sized.Internal.BitVector
import qualified Clash.Sized.Internal.Index
import qualified Clash.Sized.Internal.Signed
import qualified Clash.Sized.Internal.Unsigned
import qualified Clash.Sized.Vector

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

newtype PrimEvalMonad a = PEM (State Supply a)
  deriving ((forall a b. (a -> b) -> PrimEvalMonad a -> PrimEvalMonad b)
-> (forall a b. a -> PrimEvalMonad b -> PrimEvalMonad a)
-> Functor PrimEvalMonad
forall a b. a -> PrimEvalMonad b -> PrimEvalMonad a
forall a b. (a -> b) -> PrimEvalMonad a -> PrimEvalMonad b
forall (f :: Type -> Type).
(forall a b. (a -> b) -> f a -> f b)
-> (forall a b. a -> f b -> f a) -> Functor f
$cfmap :: forall a b. (a -> b) -> PrimEvalMonad a -> PrimEvalMonad b
fmap :: forall a b. (a -> b) -> PrimEvalMonad a -> PrimEvalMonad b
$c<$ :: forall a b. a -> PrimEvalMonad b -> PrimEvalMonad a
<$ :: forall a b. a -> PrimEvalMonad b -> PrimEvalMonad a
Functor, Functor PrimEvalMonad
Functor PrimEvalMonad =>
(forall a. a -> PrimEvalMonad a)
-> (forall a b.
    PrimEvalMonad (a -> b) -> PrimEvalMonad a -> PrimEvalMonad b)
-> (forall a b c.
    (a -> b -> c)
    -> PrimEvalMonad a -> PrimEvalMonad b -> PrimEvalMonad c)
-> (forall a b.
    PrimEvalMonad a -> PrimEvalMonad b -> PrimEvalMonad b)
-> (forall a b.
    PrimEvalMonad a -> PrimEvalMonad b -> PrimEvalMonad a)
-> Applicative PrimEvalMonad
forall a. a -> PrimEvalMonad a
forall a b. PrimEvalMonad a -> PrimEvalMonad b -> PrimEvalMonad a
forall a b. PrimEvalMonad a -> PrimEvalMonad b -> PrimEvalMonad b
forall a b.
PrimEvalMonad (a -> b) -> PrimEvalMonad a -> PrimEvalMonad b
forall a b c.
(a -> b -> c)
-> PrimEvalMonad a -> PrimEvalMonad b -> PrimEvalMonad c
forall (f :: Type -> Type).
Functor f =>
(forall a. a -> f a)
-> (forall a b. f (a -> b) -> f a -> f b)
-> (forall a b c. (a -> b -> c) -> f a -> f b -> f c)
-> (forall a b. f a -> f b -> f b)
-> (forall a b. f a -> f b -> f a)
-> Applicative f
$cpure :: forall a. a -> PrimEvalMonad a
pure :: forall a. a -> PrimEvalMonad a
$c<*> :: forall a b.
PrimEvalMonad (a -> b) -> PrimEvalMonad a -> PrimEvalMonad b
<*> :: forall a b.
PrimEvalMonad (a -> b) -> PrimEvalMonad a -> PrimEvalMonad b
$cliftA2 :: forall a b c.
(a -> b -> c)
-> PrimEvalMonad a -> PrimEvalMonad b -> PrimEvalMonad c
liftA2 :: forall a b c.
(a -> b -> c)
-> PrimEvalMonad a -> PrimEvalMonad b -> PrimEvalMonad c
$c*> :: forall a b. PrimEvalMonad a -> PrimEvalMonad b -> PrimEvalMonad b
*> :: forall a b. PrimEvalMonad a -> PrimEvalMonad b -> PrimEvalMonad b
$c<* :: forall a b. PrimEvalMonad a -> PrimEvalMonad b -> PrimEvalMonad a
<* :: forall a b. PrimEvalMonad a -> PrimEvalMonad b -> PrimEvalMonad a
Applicative, Applicative PrimEvalMonad
Applicative PrimEvalMonad =>
(forall a b.
 PrimEvalMonad a -> (a -> PrimEvalMonad b) -> PrimEvalMonad b)
-> (forall a b.
    PrimEvalMonad a -> PrimEvalMonad b -> PrimEvalMonad b)
-> (forall a. a -> PrimEvalMonad a)
-> Monad PrimEvalMonad
forall a. a -> PrimEvalMonad a
forall a b. PrimEvalMonad a -> PrimEvalMonad b -> PrimEvalMonad b
forall a b.
PrimEvalMonad a -> (a -> PrimEvalMonad b) -> PrimEvalMonad b
forall (m :: Type -> Type).
Applicative m =>
(forall a b. m a -> (a -> m b) -> m b)
-> (forall a b. m a -> m b -> m b)
-> (forall a. a -> m a)
-> Monad m
$c>>= :: forall a b.
PrimEvalMonad a -> (a -> PrimEvalMonad b) -> PrimEvalMonad b
>>= :: forall a b.
PrimEvalMonad a -> (a -> PrimEvalMonad b) -> PrimEvalMonad b
$c>> :: forall a b. PrimEvalMonad a -> PrimEvalMonad b -> PrimEvalMonad b
>> :: forall a b. PrimEvalMonad a -> PrimEvalMonad b -> PrimEvalMonad b
$creturn :: forall a. a -> PrimEvalMonad a
return :: forall a. a -> PrimEvalMonad a
Monad, MonadState Supply)

instance MonadUnique PrimEvalMonad where
  getUniqueM :: PrimEvalMonad Unique
getUniqueM = State Supply Unique -> PrimEvalMonad Unique
forall a. State Supply a -> PrimEvalMonad a
PEM (State Supply Unique -> PrimEvalMonad Unique)
-> State Supply Unique -> PrimEvalMonad Unique
forall a b. (a -> b) -> a -> b
$ (Supply -> (Unique, Supply)) -> State Supply Unique
forall a. (Supply -> (a, Supply)) -> StateT Supply Identity a
forall s (m :: Type -> Type) a.
MonadState s m =>
(s -> (a, s)) -> m a
State.state (\Supply
s -> case Supply -> (Unique, Supply)
freshId Supply
s of (!Unique
i,!Supply
s') -> (Unique
i,Supply
s'))

runPEM :: PrimEvalMonad a -> Supply -> (a, Supply)
runPEM :: forall a. PrimEvalMonad a -> Supply -> (a, Supply)
runPEM (PEM State Supply a
m) = State Supply a -> Supply -> (a, Supply)
forall s a. State s a -> s -> (a, s)
State.runState State Supply a
m

-- | Arguments and shared helpers available to primitive implementations.
-- 'primStepEntry' constructs this context after a successful name lookup,
-- keeping the evaluator calling convention out of each individual entry.
data PrimStepContext = PrimStepContext
  { PrimStepContext -> TyConMap
tcm :: TyConMap
  , PrimStepContext -> Bool
isSubj :: Bool
  , PrimStepContext -> PrimInfo
pInfo :: PrimInfo
  , PrimStepContext -> [Type]
tys :: [Type]
  , PrimStepContext -> [Value]
args :: [Value]
  , PrimStepContext -> Machine
mach :: Machine
  , PrimStepContext -> Type
ty :: Type
  , PrimStepContext -> Type -> Integer -> (Natural -> Natural) -> Term
checkNaturalRange1 :: Type -> Integer -> (Natural -> Natural) -> Term
  , PrimStepContext
-> Type
-> Integer
-> Integer
-> (Natural -> Natural -> Natural)
-> Term
checkNaturalRange2 :: Type -> Integer -> Integer -> (Natural -> Natural -> Natural) -> Term
  , PrimStepContext -> Type -> [Integer] -> ([Natural] -> Term) -> Term
checkNaturalRange :: Type -> [Integer] -> ([Natural] -> Term) -> Term
  , PrimStepContext -> Term -> Maybe Machine
reduce :: Term -> Maybe Machine
  , PrimStepContext -> Machine -> Term -> Maybe Machine
reduceWith :: Machine -> Term -> Maybe Machine
  , PrimStepContext -> Term -> Maybe Machine
reduceWHNF :: Term -> Maybe Machine
  , PrimStepContext -> Machine -> Term -> Maybe Machine
reduceWHNF' :: Machine -> Term -> Maybe Machine
  , PrimStepContext -> Term -> Term
catchDivByZero :: Term -> Term
  , PrimStepContext -> Term -> Term
catchErrorCall :: Term -> Term
  }

mkPrimStepContext :: TyConMap -> Bool -> PrimInfo -> [Type] -> [Value] -> Machine
 -> PrimStepContext
mkPrimStepContext :: TyConMap
-> Bool
-> PrimInfo
-> [Type]
-> [Value]
-> Machine
-> PrimStepContext
mkPrimStepContext TyConMap
tcm Bool
isSubj PrimInfo
pInfo [Type]
tys [Value]
args Machine
mach = 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 :: 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
..}
  where
    ty :: Type
ty = PrimInfo -> Type
primType PrimInfo
pInfo

    checkNaturalRange1 :: Type -> Integer -> (Natural -> Natural) -> Term
checkNaturalRange1 Type
nTy Integer
i Natural -> Natural
f =
      Type -> [Integer] -> ([Natural] -> Term) -> Term
checkNaturalRange Type
nTy [Integer
i]
        (\[Natural
i'] -> Natural -> Term
naturalToNaturalLiteral (Natural -> Natural
f Natural
i'))

    checkNaturalRange2 :: Type
-> Integer -> Integer -> (Natural -> Natural -> Natural) -> Term
checkNaturalRange2 Type
nTy Integer
i Integer
j Natural -> Natural -> Natural
f =
      Type -> [Integer] -> ([Natural] -> Term) -> Term
checkNaturalRange Type
nTy [Integer
i, Integer
j]
        (\[Natural
i', Natural
j'] -> Natural -> Term
naturalToNaturalLiteral (Natural -> Natural -> Natural
f Natural
i' Natural
j'))

    -- Check given integer's range. If any of them are less than zero, give up
    -- and return an undefined type.
    checkNaturalRange
      :: Type
      -- Type of GHC.Natural.Natural ^
      -> [Integer]
      -> ([Natural] -> Term)
      -> Term
    checkNaturalRange :: Type -> [Integer] -> ([Natural] -> Term) -> Term
checkNaturalRange Type
nTy [Integer]
natsAsInts [Natural] -> Term
f =
      if (Integer -> Bool) -> [Integer] -> Bool
forall (t :: Type -> Type) a.
Foldable t =>
(a -> Bool) -> t a -> Bool
any (Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
<Integer
0) [Integer]
natsAsInts then
        Term -> Type -> Term
TyApp (PrimInfo -> Term
Prim PrimInfo
NP.undefined) Type
nTy
      else
        [Natural] -> Term
f ((Integer -> Natural) -> [Integer] -> [Natural]
forall a b. (a -> b) -> [a] -> [b]
map Integer -> Natural
forall a. Num a => Integer -> a
fromInteger [Integer]
natsAsInts)

    reduce :: Term -> Maybe Machine
    reduce :: Term -> Maybe Machine
reduce = Machine -> Term -> Maybe Machine
reduceWith Machine
mach

    -- Like 'reduceWith, but reduces in (the heap of) an explicitly given machine
    -- rather than the captured 'mach'. Use this when the reduced term refers to
    -- bindings freshly allocated with 'newLetBinding'.
    reduceWith :: Machine -> Term -> Maybe Machine
    reduceWith :: Machine -> Term -> Maybe Machine
reduceWith Machine
mach0 Term
e = case Term -> Either [Char] Term
forall a. a -> Either [Char] a
isX Term
e of
      Left [Char]
msg ->
        let resTy :: Type
resTy = TyConMap -> Type -> [Type] -> Type
getResultTy TyConMap
tcm Type
ty [Type]
tys
            warning :: [Char]
warning = [[Char]] -> [Char]
unlines
              [ [Char]
"Warning: caught XException: \"" [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Char]
msg [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Char]
"\" while trying to evaluate: "
              , Term -> [Char]
forall p. PrettyPrec p => p -> [Char]
showPpr (Term -> [Either Term Type] -> Term
mkApps (PrimInfo -> Term
Prim PrimInfo
pInfo) ((Value -> Either Term Type) -> [Value] -> [Either Term Type]
forall a b. (a -> b) -> [a] -> [b]
map (Term -> Either Term Type
forall a b. a -> Either a b
Left (Term -> Either Term Type)
-> (Value -> Term) -> Value -> Either Term Type
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Value -> Term
valToTerm) [Value]
args))
              ]
        in [Char] -> Maybe Machine -> Maybe Machine
forall a. [Char] -> a -> a
trace [Char]
warning (Machine -> Maybe Machine
forall a. a -> Maybe a
Just (Term -> Machine -> Machine
setTerm (Term -> Type -> Term
TyApp (PrimInfo -> Term
Prim PrimInfo
NP.undefined) Type
resTy) Machine
mach0))
      Right Term
e' -> Machine -> Maybe Machine
forall a. a -> Maybe a
Just (Term -> Machine -> Machine
setTerm Term
e' Machine
mach0)

    reduceWHNF :: Term -> Maybe Machine
reduceWHNF Term
e =
      let eval :: Evaluator
eval = Step -> Unwind -> PrimStep -> PrimUnwind -> Evaluator
Evaluator Step
ghcStep Unwind
ghcUnwind PrimStep
ghcPrimStep PrimUnwind
ghcPrimUnwind
          mach1 :: Machine
mach1@Machine{mStack :: Machine -> Stack
mStack=[]} = Evaluator -> TyConMap -> Bool -> Machine -> Machine
whnf Evaluator
eval TyConMap
tcm Bool
isSubj (Term -> Machine -> Machine
setTerm Term
e (Machine -> Machine) -> Machine -> Machine
forall a b. (a -> b) -> a -> b
$ Machine -> Machine
stackClear Machine
mach)
      in 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 }

    reduceWHNF' :: Machine -> Term -> Maybe Machine
reduceWHNF' Machine
mach1 Term
e =
      let eval :: Evaluator
eval = Step -> Unwind -> PrimStep -> PrimUnwind -> Evaluator
Evaluator Step
ghcStep Unwind
ghcUnwind PrimStep
ghcPrimStep PrimUnwind
ghcPrimUnwind
          mach2 :: Machine
mach2@Machine{mStack :: Machine -> Stack
mStack=[]} = Evaluator -> TyConMap -> Bool -> Machine -> Machine
whnf Evaluator
eval TyConMap
tcm Bool
isSubj (Term -> Machine -> Machine
setTerm Term
e (Machine -> Machine) -> Machine -> Machine
forall a b. (a -> b) -> a -> b
$ Machine -> Machine
stackClear Machine
mach1)
       in Machine -> Maybe Machine
forall a. a -> Maybe a
Just (Machine -> Maybe Machine) -> Machine -> Maybe Machine
forall a b. (a -> b) -> a -> b
$ Machine
mach2 { mStack = mStack mach }

    makeUndefinedIf :: Exception e => (e -> Bool) -> Term -> Term
    makeUndefinedIf :: forall e. Exception e => (e -> Bool) -> Term -> Term
makeUndefinedIf e -> Bool
wantToHandle Term
tm =
      case IO (Either e Term) -> Either e Term
forall a. IO a -> a
unsafeDupablePerformIO (IO (Either e Term) -> Either e Term)
-> IO (Either e Term) -> Either e Term
forall a b. (a -> b) -> a -> b
$ (e -> Maybe e) -> IO Term -> IO (Either e Term)
forall e b a.
Exception e =>
(e -> Maybe b) -> IO a -> IO (Either b a)
tryJust e -> Maybe e
selectException (Term -> IO Term
forall a. a -> IO a
evaluate (Term -> IO Term) -> Term -> IO Term
forall a b. (a -> b) -> a -> b
$ Term -> Term
forall a. NFData a => a -> a
force Term
tm) of
        Right Term
b -> Term
b
        Left e
e -> [Char] -> Term -> Term
forall a. [Char] -> a -> a
trace (e -> [Char]
forall {a}. Show a => a -> [Char]
msg e
e) (Term -> Type -> Term
TyApp (PrimInfo -> Term
Prim PrimInfo
NP.undefined) Type
resTy)
      where
        resTy :: Type
resTy = TyConMap -> Type -> [Type] -> Type
getResultTy TyConMap
tcm Type
ty [Type]
tys
        selectException :: e -> Maybe e
selectException e
e | e -> Bool
wantToHandle e
e = e -> Maybe e
forall a. a -> Maybe a
Just e
e
                          | Bool
otherwise = Maybe e
forall a. Maybe a
Nothing
        msg :: a -> [Char]
msg a
e = [[Char]] -> [Char]
unlines [[Char]
"Warning: caught exception: \"" [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ a -> [Char]
forall {a}. Show a => a -> [Char]
show a
e [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Char]
"\" while trying to evaluate: "
                        , Term -> [Char]
forall p. PrettyPrec p => p -> [Char]
showPpr (Term -> [Either Term Type] -> Term
mkApps (PrimInfo -> Term
Prim PrimInfo
pInfo) ((Value -> Either Term Type) -> [Value] -> [Either Term Type]
forall a b. (a -> b) -> [a] -> [b]
map (Term -> Either Term Type
forall a b. a -> Either a b
Left (Term -> Either Term Type)
-> (Value -> Term) -> Value -> Either Term Type
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Value -> Term
valToTerm) [Value]
args))
                        ]

    catchDivByZero :: Term -> Term
catchDivByZero = (ArithException -> Bool) -> Term -> Term
forall e. Exception e => (e -> Bool) -> Term -> Term
makeUndefinedIf (ArithException -> ArithException -> Bool
forall a. Eq a => a -> a -> Bool
==ArithException
DivideByZero)

    catchErrorCall :: Term -> Term
catchErrorCall = (ErrorCall -> Bool) -> Term -> Term
forall e. Exception e => (e -> Bool) -> Term -> Term
makeUndefinedIf (Bool -> ErrorCall -> Bool
forall a b. a -> b -> a
const Bool
True :: ErrorCall -> Bool)

-- | Associate a primitive name with an implementation. The adapter from the
-- evaluator's calling convention to 'PrimStepContext' lives here so individual
-- primitive implementations do not have to repeat it.
primStepEntry :: Text -> (PrimStepContext -> Maybe Machine) -> (Text, PrimStep)
primStepEntry :: Text -> (PrimStepContext -> Maybe Machine) -> (Text, PrimStep)
primStepEntry Text
name PrimStepContext -> Maybe Machine
impl =
  (Text
name, \TyConMap
tcm Bool
isSubj PrimInfo
pInfo [Type]
tys [Value]
args Machine
mach ->
    PrimStepContext -> Maybe Machine
impl (TyConMap
-> Bool
-> PrimInfo
-> [Type]
-> [Value]
-> Machine
-> PrimStepContext
mkPrimStepContext TyConMap
tcm Bool
isSubj PrimInfo
pInfo [Type]
tys [Value]
args Machine
mach))
{-# INLINE primStepEntry #-}

-- Helper functions for literals

pairOf :: (Value -> Maybe a) -> [Value] -> Maybe (a, a)
pairOf :: forall a. (Value -> Maybe a) -> [Value] -> Maybe (a, a)
pairOf Value -> Maybe a
f [Value
x, Value
y] = (,) (a -> a -> (a, a)) -> Maybe a -> Maybe (a -> (a, a))
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> Value -> Maybe a
f Value
x Maybe (a -> (a, a)) -> Maybe a -> Maybe (a, a)
forall a b. Maybe (a -> b) -> Maybe a -> Maybe b
forall (f :: Type -> Type) a b.
Applicative f =>
f (a -> b) -> f a -> f b
<*> Value -> Maybe a
f Value
y
pairOf Value -> Maybe a
_ [Value]
_ = Maybe (a, a)
forall a. Maybe a
Nothing

listOf :: (Value -> Maybe a) -> [Value] -> [a]
listOf :: forall a. (Value -> Maybe a) -> [Value] -> [a]
listOf = (Value -> Maybe a) -> [Value] -> [a]
forall a b. (a -> Maybe b) -> [a] -> [b]
mapMaybe

wrapUnsigned :: Integer -> Integer -> Integer
wrapUnsigned :: Integer -> Integer -> Integer
wrapUnsigned Integer
n Integer
i = Integer
i Integer -> Integer -> Integer
forall a. Integral a => a -> a -> a
`mod` Integer
sz
 where
  sz :: Integer
sz = Integer
1 Integer -> Int -> Integer
forall a. Bits a => a -> Int -> a
`shiftL` Integer -> Int
forall a. Num a => Integer -> a
fromInteger Integer
n

wrapSigned :: Integer -> Integer -> Integer
wrapSigned :: Integer -> Integer -> Integer
wrapSigned Integer
n Integer
i = if Integer
n Integer -> Integer -> Bool
forall a. Eq a => a -> a -> Bool
== Integer
0 then Integer
0 else Integer
res
 where
  mask :: Integer
mask = Integer
1 Integer -> Int -> Integer
forall a. Bits a => a -> Int -> a
`shiftL` Integer -> Int
forall a. Num a => Integer -> a
fromInteger (Integer
n Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
- Integer
1)
  res :: Integer
res  = case Integer -> Integer -> (Integer, Integer)
forall a. Integral a => a -> a -> (a, a)
divMod Integer
i Integer
mask of
           (Integer
s,Integer
i1) | Integer -> Bool
forall a. Integral a => a -> Bool
even Integer
s    -> Integer
i1
                  | Bool
otherwise -> Integer
i1 Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
- Integer
mask

doubleLiterals' :: [Value] -> [Word64]
doubleLiterals' :: [Value] -> [Unique]
doubleLiterals' = (Value -> Maybe Unique) -> [Value] -> [Unique]
forall a. (Value -> Maybe a) -> [Value] -> [a]
listOf Value -> Maybe Unique
doubleLiteral

doubleLiteral :: Value -> Maybe Word64
doubleLiteral :: Value -> Maybe Unique
doubleLiteral Value
v = case Value
v of
  Lit (DoubleLiteral Unique
i) -> Unique -> Maybe Unique
forall a. a -> Maybe a
Just Unique
i
  Value
_ -> Maybe Unique
forall a. Maybe a
Nothing

floatLiterals' :: [Value] -> [Word32]
floatLiterals' :: [Value] -> [Word32]
floatLiterals' = (Value -> Maybe Word32) -> [Value] -> [Word32]
forall a. (Value -> Maybe a) -> [Value] -> [a]
listOf Value -> Maybe Word32
floatLiteral

floatLiteral :: Value -> Maybe Word32
floatLiteral :: Value -> Maybe Word32
floatLiteral Value
v = case Value
v of
  Lit (FloatLiteral Word32
i) -> Word32 -> Maybe Word32
forall a. a -> Maybe a
Just Word32
i
  Value
_ -> Maybe Word32
forall a. Maybe a
Nothing

integerLiterals :: [Value] -> Maybe (Integer, Integer)
integerLiterals :: [Value] -> Maybe (Integer, Integer)
integerLiterals = (Value -> Maybe Integer) -> [Value] -> Maybe (Integer, Integer)
forall a. (Value -> Maybe a) -> [Value] -> Maybe (a, a)
pairOf Value -> Maybe Integer
integerLiteral

integerLiteral :: Value -> Maybe Integer
integerLiteral :: Value -> Maybe Integer
integerLiteral Value
v =
  case Value
v of
    Lit (IntegerLiteral Integer
i) -> Integer -> Maybe Integer
forall a. a -> Maybe a
Just Integer
i
    DC DataCon
dc [Left (Literal (IntLiteral Integer
i))]
      | DataCon -> Int
dcTag DataCon
dc Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
1
      -> Integer -> Maybe Integer
forall a. a -> Maybe a
Just Integer
i
    DC DataCon
dc [Left (Literal (ByteArrayLiteral (BA.ByteArray ByteArray#
ba)))]
      | DataCon -> Int
dcTag DataCon
dc Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
2
      -> Integer -> Maybe Integer
forall a. a -> Maybe a
Just (ByteArray# -> Integer
IP ByteArray#
ba)
      | DataCon -> Int
dcTag DataCon
dc Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
3
      -> Integer -> Maybe Integer
forall a. a -> Maybe a
Just (ByteArray# -> Integer
IN ByteArray#
ba)
    Value
_ -> Maybe Integer
forall a. Maybe a
Nothing

naturalLiterals :: [Value] -> Maybe (Integer, Integer)
naturalLiterals :: [Value] -> Maybe (Integer, Integer)
naturalLiterals = (Value -> Maybe Integer) -> [Value] -> Maybe (Integer, Integer)
forall a. (Value -> Maybe a) -> [Value] -> Maybe (a, a)
pairOf Value -> Maybe Integer
naturalLiteral

naturalLiteral :: Value -> Maybe Integer
naturalLiteral :: Value -> Maybe Integer
naturalLiteral Value
v =
  case Value
v of
    Lit (NaturalLiteral Integer
i) -> Integer -> Maybe Integer
forall a. a -> Maybe a
Just Integer
i
    DC DataCon
dc [Left (Literal (WordLiteral Integer
i))]
      | DataCon -> Int
dcTag DataCon
dc Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
1
      -> Integer -> Maybe Integer
forall a. a -> Maybe a
Just Integer
i
    DC DataCon
dc [Left (Literal (ByteArrayLiteral (BA.ByteArray ByteArray#
ba)))]
      | DataCon -> Int
dcTag DataCon
dc Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
2
      -> Integer -> Maybe Integer
forall a. a -> Maybe a
Just (ByteArray# -> Integer
IP ByteArray#
ba)
    Value
_ -> Maybe Integer
forall a. Maybe a
Nothing

integerLiterals' :: [Value] -> [Integer]
integerLiterals' :: [Value] -> [Integer]
integerLiterals' = (Value -> Maybe Integer) -> [Value] -> [Integer]
forall a. (Value -> Maybe a) -> [Value] -> [a]
listOf Value -> Maybe Integer
integerLiteral

naturalLiterals' :: [Value] -> [Integer]
naturalLiterals' :: [Value] -> [Integer]
naturalLiterals' = (Value -> Maybe Integer) -> [Value] -> [Integer]
forall a. (Value -> Maybe a) -> [Value] -> [a]
listOf Value -> Maybe Integer
naturalLiteral

intLiterals :: [Value] -> Maybe (Integer,Integer)
intLiterals :: [Value] -> Maybe (Integer, Integer)
intLiterals = (Value -> Maybe Integer) -> [Value] -> Maybe (Integer, Integer)
forall a. (Value -> Maybe a) -> [Value] -> Maybe (a, a)
pairOf Value -> Maybe Integer
intLiteral

intLiterals' :: [Value] -> [Integer]
intLiterals' :: [Value] -> [Integer]
intLiterals' = (Value -> Maybe Integer) -> [Value] -> [Integer]
forall a. (Value -> Maybe a) -> [Value] -> [a]
listOf Value -> Maybe Integer
intLiteral

intCLiterals' :: [Value] -> [Integer]
intCLiterals' :: [Value] -> [Integer]
intCLiterals' = (Value -> Maybe Integer) -> [Value] -> [Integer]
forall a. (Value -> Maybe a) -> [Value] -> [a]
listOf Value -> Maybe Integer
intCLiteral

intLiteral :: Value -> Maybe Integer
intLiteral :: Value -> Maybe Integer
intLiteral Value
x = case Value
x of
  Lit (IntLiteral Integer
i) -> Integer -> Maybe Integer
forall a. a -> Maybe a
Just Integer
i
  Value
_ -> Maybe Integer
forall a. Maybe a
Nothing

int8Literals' :: [Value] -> [Integer]
int8Literals' :: [Value] -> [Integer]
int8Literals' = (Value -> Maybe Integer) -> [Value] -> [Integer]
forall a. (Value -> Maybe a) -> [Value] -> [a]
listOf Value -> Maybe Integer
int8Literal

int8Literal :: Value -> Maybe Integer
int8Literal :: Value -> Maybe Integer
int8Literal Value
x = case Value
x of
  Lit (Int8Literal Integer
i) -> Integer -> Maybe Integer
forall a. a -> Maybe a
Just Integer
i
  Value
_ -> Maybe Integer
forall a. Maybe a
Nothing

int16Literals' :: [Value] -> [Integer]
int16Literals' :: [Value] -> [Integer]
int16Literals' = (Value -> Maybe Integer) -> [Value] -> [Integer]
forall a. (Value -> Maybe a) -> [Value] -> [a]
listOf Value -> Maybe Integer
int16Literal

int16Literal :: Value -> Maybe Integer
int16Literal :: Value -> Maybe Integer
int16Literal Value
x = case Value
x of
  Lit (Int16Literal Integer
i) -> Integer -> Maybe Integer
forall a. a -> Maybe a
Just Integer
i
  Value
_ -> Maybe Integer
forall a. Maybe a
Nothing

int32Literals' :: [Value] -> [Integer]
int32Literals' :: [Value] -> [Integer]
int32Literals' = (Value -> Maybe Integer) -> [Value] -> [Integer]
forall a. (Value -> Maybe a) -> [Value] -> [a]
listOf Value -> Maybe Integer
int32Literal

int32Literal :: Value -> Maybe Integer
int32Literal :: Value -> Maybe Integer
int32Literal Value
x = case Value
x of
  Lit (Int32Literal Integer
i) -> Integer -> Maybe Integer
forall a. a -> Maybe a
Just Integer
i
  Value
_ -> Maybe Integer
forall a. Maybe a
Nothing

int64Literals' :: [Value] -> [Integer]
int64Literals' :: [Value] -> [Integer]
int64Literals' = (Value -> Maybe Integer) -> [Value] -> [Integer]
forall a. (Value -> Maybe a) -> [Value] -> [a]
listOf Value -> Maybe Integer
int64Literal

int64Literal :: Value -> Maybe Integer
int64Literal :: Value -> Maybe Integer
int64Literal Value
x = case Value
x of
  Lit (Int64Literal Integer
i) -> Integer -> Maybe Integer
forall a. a -> Maybe a
Just Integer
i
  Value
_ -> Maybe Integer
forall a. Maybe a
Nothing

intCLiteral :: Value -> Maybe Integer
intCLiteral :: Value -> Maybe Integer
intCLiteral Value
v = case Value
v of
  (DC DataCon
_ [Left (Literal (IntLiteral Integer
i))]) -> Integer -> Maybe Integer
forall a. a -> Maybe a
Just Integer
i
  Value
_ -> Maybe Integer
forall a. Maybe a
Nothing

intCLiterals :: [Value] -> Maybe (Integer, Integer)
intCLiterals :: [Value] -> Maybe (Integer, Integer)
intCLiterals = (Value -> Maybe Integer) -> [Value] -> Maybe (Integer, Integer)
forall a. (Value -> Maybe a) -> [Value] -> Maybe (a, a)
pairOf Value -> Maybe Integer
intCLiteral

wordLiterals :: [Value] -> Maybe (Integer,Integer)
wordLiterals :: [Value] -> Maybe (Integer, Integer)
wordLiterals = (Value -> Maybe Integer) -> [Value] -> Maybe (Integer, Integer)
forall a. (Value -> Maybe a) -> [Value] -> Maybe (a, a)
pairOf Value -> Maybe Integer
wordLiteral

wordLiterals' :: [Value] -> [Integer]
wordLiterals' :: [Value] -> [Integer]
wordLiterals' = (Value -> Maybe Integer) -> [Value] -> [Integer]
forall a. (Value -> Maybe a) -> [Value] -> [a]
listOf Value -> Maybe Integer
wordLiteral

wordLiteral :: Value -> Maybe Integer
wordLiteral :: Value -> Maybe Integer
wordLiteral Value
x = case Value
x of
  Lit (WordLiteral Integer
i) -> Integer -> Maybe Integer
forall a. a -> Maybe a
Just Integer
i
  Value
_ -> Maybe Integer
forall a. Maybe a
Nothing

word8Literals' :: [Value] -> [Integer]
word8Literals' :: [Value] -> [Integer]
word8Literals' = (Value -> Maybe Integer) -> [Value] -> [Integer]
forall a. (Value -> Maybe a) -> [Value] -> [a]
listOf Value -> Maybe Integer
word8Literal

word8Literal :: Value -> Maybe Integer
word8Literal :: Value -> Maybe Integer
word8Literal Value
x = case Value
x of
  Lit (Word8Literal Integer
i) -> Integer -> Maybe Integer
forall a. a -> Maybe a
Just Integer
i
  Value
_ -> Maybe Integer
forall a. Maybe a
Nothing

word16Literals' :: [Value] -> [Integer]
word16Literals' :: [Value] -> [Integer]
word16Literals' = (Value -> Maybe Integer) -> [Value] -> [Integer]
forall a. (Value -> Maybe a) -> [Value] -> [a]
listOf Value -> Maybe Integer
word16Literal

word16Literal :: Value -> Maybe Integer
word16Literal :: Value -> Maybe Integer
word16Literal Value
x = case Value
x of
  Lit (Word16Literal Integer
i) -> Integer -> Maybe Integer
forall a. a -> Maybe a
Just Integer
i
  Value
_ -> Maybe Integer
forall a. Maybe a
Nothing

word32Literals' :: [Value] -> [Integer]
word32Literals' :: [Value] -> [Integer]
word32Literals' = (Value -> Maybe Integer) -> [Value] -> [Integer]
forall a. (Value -> Maybe a) -> [Value] -> [a]
listOf Value -> Maybe Integer
word32Literal

word32Literal :: Value -> Maybe Integer
word32Literal :: Value -> Maybe Integer
word32Literal Value
x = case Value
x of
  Lit (Word32Literal Integer
i) -> Integer -> Maybe Integer
forall a. a -> Maybe a
Just Integer
i
  Value
_ -> Maybe Integer
forall a. Maybe a
Nothing

word64Literals' :: [Value] -> [Integer]
word64Literals' :: [Value] -> [Integer]
word64Literals' = (Value -> Maybe Integer) -> [Value] -> [Integer]
forall a. (Value -> Maybe a) -> [Value] -> [a]
listOf Value -> Maybe Integer
word64Literal

word64Literal :: Value -> Maybe Integer
word64Literal :: Value -> Maybe Integer
word64Literal Value
x = case Value
x of
  Lit (Word64Literal Integer
i) -> Integer -> Maybe Integer
forall a. a -> Maybe a
Just Integer
i
  Value
_ -> Maybe Integer
forall a. Maybe a
Nothing

charLiterals :: [Value] -> Maybe (Char,Char)
charLiterals :: [Value] -> Maybe (Char, Char)
charLiterals = (Value -> Maybe Char) -> [Value] -> Maybe (Char, Char)
forall a. (Value -> Maybe a) -> [Value] -> Maybe (a, a)
pairOf Value -> Maybe Char
charLiteral

charLiterals' :: [Value] -> [Char]
charLiterals' :: [Value] -> [Char]
charLiterals' = (Value -> Maybe Char) -> [Value] -> [Char]
forall a. (Value -> Maybe a) -> [Value] -> [a]
listOf Value -> Maybe Char
charLiteral

charLiteral :: Value -> Maybe Char
charLiteral :: Value -> Maybe Char
charLiteral Value
x = case Value
x of
  Lit (CharLiteral Char
c) -> Char -> Maybe Char
forall a. a -> Maybe a
Just Char
c
  Value
_ -> Maybe Char
forall a. Maybe a
Nothing

sizedLiterals :: Text -> [Value] -> Maybe (Integer,Integer)
sizedLiterals :: Text -> [Value] -> Maybe (Integer, Integer)
sizedLiterals Text
szCon = (Value -> Maybe Integer) -> [Value] -> Maybe (Integer, Integer)
forall a. (Value -> Maybe a) -> [Value] -> Maybe (a, a)
pairOf (Text -> Value -> Maybe Integer
sizedLiteral Text
szCon)

sizedLiterals' :: Text -> [Value] -> [Integer]
sizedLiterals' :: Text -> [Value] -> [Integer]
sizedLiterals' Text
szCon = (Value -> Maybe Integer) -> [Value] -> [Integer]
forall a. (Value -> Maybe a) -> [Value] -> [a]
listOf (Text -> Value -> Maybe Integer
sizedLiteral Text
szCon)

sizedLiteral :: Text -> Value -> Maybe Integer
sizedLiteral :: Text -> Value -> Maybe Integer
sizedLiteral Text
szCon Value
val = case Value
val of
  PrimVal PrimInfo
p [Type]
_ [Value
_, Lit (IntegerLiteral Integer
i)]
    | PrimInfo -> Text
primName PrimInfo
p Text -> Text -> Bool
forall a. Eq a => a -> a -> Bool
== Text
szCon -> Integer -> Maybe Integer
forall a. a -> Maybe a
Just Integer
i
  Value
_ -> Maybe Integer
forall a. Maybe a
Nothing

bitLiterals
  :: [Value]
  -> [(Integer,Integer)]
bitLiterals :: [Value] -> [(Integer, Integer)]
bitLiterals = ((Integer, Integer) -> (Integer, Integer))
-> [(Integer, Integer)] -> [(Integer, Integer)]
forall a b. (a -> b) -> [a] -> [b]
map (Integer, Integer) -> (Integer, Integer)
forall {a} {b}. (Bits a, Bits b, Num a, Num b) => (a, b) -> (a, b)
normalizeBit ([(Integer, Integer)] -> [(Integer, Integer)])
-> ([Value] -> [(Integer, Integer)])
-> [Value]
-> [(Integer, Integer)]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Value -> Maybe (Integer, Integer))
-> [Value] -> [(Integer, Integer)]
forall a b. (a -> Maybe b) -> [a] -> [b]
mapMaybe Value -> Maybe (Integer, Integer)
go
 where
  normalizeBit :: (a, b) -> (a, b)
normalizeBit (a
msk,b
v) = (a
msk a -> a -> a
forall a. Bits a => a -> a -> a
.&. a
1, b
v b -> b -> b
forall a. Bits a => a -> a -> a
.&. b
1)
  go :: Value -> Maybe (Integer, Integer)
go Value
val = case Value
val of
    PrimVal PrimInfo
p [Type]
_ [Lit (WordLiteral Integer
m), Lit (IntegerLiteral Integer
i)]
      | PrimInfo -> Text
primName PrimInfo
p Text -> Text -> Bool
forall a. Eq a => a -> a -> Bool
== Name -> Text
forall a. Show a => a -> Text
showt 'Clash.Sized.Internal.BitVector.fromInteger##
      -> (Integer, Integer) -> Maybe (Integer, Integer)
forall a. a -> Maybe a
Just (Integer
m,Integer
i)
    Value
_ -> Maybe (Integer, Integer)
forall a. Maybe a
Nothing

indexLiterals, signedLiterals, unsignedLiterals
  :: [Value] -> Maybe (Integer,Integer)
indexLiterals :: [Value] -> Maybe (Integer, Integer)
indexLiterals     = Text -> [Value] -> Maybe (Integer, Integer)
sizedLiterals (Name -> Text
forall a. Show a => a -> Text
showt 'Clash.Sized.Internal.Index.fromInteger#)
signedLiterals :: [Value] -> Maybe (Integer, Integer)
signedLiterals    = Text -> [Value] -> Maybe (Integer, Integer)
sizedLiterals (Name -> Text
forall a. Show a => a -> Text
showt 'Clash.Sized.Internal.Signed.fromInteger#)
unsignedLiterals :: [Value] -> Maybe (Integer, Integer)
unsignedLiterals  = Text -> [Value] -> Maybe (Integer, Integer)
sizedLiterals (Name -> Text
forall a. Show a => a -> Text
showt 'Clash.Sized.Internal.Unsigned.fromInteger#)

indexLiterals', signedLiterals', unsignedLiterals'
  :: [Value] -> [Integer]
indexLiterals' :: [Value] -> [Integer]
indexLiterals'     = Text -> [Value] -> [Integer]
sizedLiterals' (Name -> Text
forall a. Show a => a -> Text
showt 'Clash.Sized.Internal.Index.fromInteger#)
signedLiterals' :: [Value] -> [Integer]
signedLiterals'    = Text -> [Value] -> [Integer]
sizedLiterals' (Name -> Text
forall a. Show a => a -> Text
showt 'Clash.Sized.Internal.Signed.fromInteger#)
unsignedLiterals' :: [Value] -> [Integer]
unsignedLiterals'  = Text -> [Value] -> [Integer]
sizedLiterals' (Name -> Text
forall a. Show a => a -> Text
showt 'Clash.Sized.Internal.Unsigned.fromInteger#)

bitVectorLiterals'
  :: [Value] -> [(Integer,Integer)]
bitVectorLiterals' :: [Value] -> [(Integer, Integer)]
bitVectorLiterals' = (Value -> Maybe (Integer, Integer))
-> [Value] -> [(Integer, Integer)]
forall a. (Value -> Maybe a) -> [Value] -> [a]
listOf Value -> Maybe (Integer, Integer)
bitVectorLiteral

bitVectorLiteral :: Value -> Maybe (Integer, Integer)
bitVectorLiteral :: Value -> Maybe (Integer, Integer)
bitVectorLiteral Value
val = case Value
val of
  (PrimVal PrimInfo
p [Type]
_ [Value
_, Lit (NaturalLiteral Integer
m), Lit (IntegerLiteral Integer
i)])
    | PrimInfo -> Text
primName PrimInfo
p Text -> Text -> Bool
forall a. Eq a => a -> a -> Bool
== Name -> Text
forall a. Show a => a -> Text
showt 'Clash.Sized.Internal.BitVector.fromInteger# -> (Integer, Integer) -> Maybe (Integer, Integer)
forall a. a -> Maybe a
Just (Integer
m, Integer
i)
  Value
_ -> Maybe (Integer, Integer)
forall a. Maybe a
Nothing

toBV :: (Integer,Integer) -> BitVector n
toBV :: forall (n :: Natural). (Integer, Integer) -> BitVector n
toBV (Integer
mask,Integer
val) = Natural -> Natural -> BitVector n
forall (n :: Natural). Natural -> Natural -> BitVector n
BV (Integer -> Natural
forall a. Num a => Integer -> a
fromInteger Integer
mask) (Integer -> Natural
forall a. Num a => Integer -> a
fromInteger Integer
val)

splitBV :: BitVector n -> (Integer,Integer)
splitBV :: forall (n :: Natural). BitVector n -> (Integer, Integer)
splitBV (BV Natural
msk Natural
val) = (Natural -> Integer
forall a. Integral a => a -> Integer
toInteger Natural
msk, Natural -> Integer
forall a. Integral a => a -> Integer
toInteger Natural
val)

toBit :: (Integer,Integer) -> Bit
toBit :: (Integer, Integer) -> Bit
toBit (Integer
mask,Integer
val) = Word -> Word -> Bit
Bit (Integer -> Word
forall a. Num a => Integer -> a
fromInteger Integer
mask) (Integer -> Word
forall a. Num a => Integer -> a
fromInteger Integer
val)

valArgs
  :: Value
  -> Maybe [Term]
valArgs :: Value -> Maybe [Term]
valArgs Value
v =
  case Value
v of
    PrimVal PrimInfo
_ [Type]
_ [Value]
vs -> [Term] -> Maybe [Term]
forall a. a -> Maybe a
Just ((Value -> Term) -> [Value] -> [Term]
forall a b. (a -> b) -> [a] -> [b]
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
fmap Value -> Term
valToTerm [Value]
vs)
    DC DataCon
_ [Either Term Type]
args -> [Term] -> Maybe [Term]
forall a. a -> Maybe a
Just ([Either Term Type] -> [Term]
forall a b. [Either a b] -> [a]
Either.lefts [Either Term Type]
args)
    Value
_ -> Maybe [Term]
forall a. Maybe a
Nothing

-- Tries to match literal arguments to a function like
--   (Unsigned.shiftL#  :: forall n. KnownNat n => Unsigned n -> Int -> Unsigned n)
sizedLitIntLit
  :: Text -> TyConMap -> [Type] -> [Value]
  -> Maybe (Type,Integer,Integer,Integer)
sizedLitIntLit :: Text
-> TyConMap
-> [Type]
-> [Value]
-> Maybe (Type, Integer, Integer, Integer)
sizedLitIntLit Text
szCon TyConMap
tcm [Type]
tys [Value]
args
  | Just (Type
nTy,Integer
kn) <- TyConMap -> [Type] -> Maybe (Type, Integer)
extractKnownNat TyConMap
tcm [Type]
tys
  , [Value
_
    ,PrimVal PrimInfo
p [Type]
_ [Value
_,Lit (IntegerLiteral Integer
i)]
    ,Value -> Maybe [Term]
valArgs -> Just [Literal (IntLiteral Integer
j)]
    ] <- [Value]
args
  , PrimInfo -> Text
primName PrimInfo
p Text -> Text -> Bool
forall a. Eq a => a -> a -> Bool
== Text
szCon
  = (Type, Integer, Integer, Integer)
-> Maybe (Type, Integer, Integer, Integer)
forall a. a -> Maybe a
Just (Type
nTy,Integer
kn,Integer
i,Integer
j)
  | Bool
otherwise
  = Maybe (Type, Integer, Integer, Integer)
forall a. Maybe a
Nothing

signedLitIntLit, unsignedLitIntLit
  :: TyConMap -> [Type] -> [Value]
  -> Maybe (Type,Integer,Integer,Integer)
signedLitIntLit :: TyConMap
-> [Type] -> [Value] -> Maybe (Type, Integer, Integer, Integer)
signedLitIntLit    = Text
-> TyConMap
-> [Type]
-> [Value]
-> Maybe (Type, Integer, Integer, Integer)
sizedLitIntLit (Name -> Text
forall a. Show a => a -> Text
showt 'Clash.Sized.Internal.Signed.fromInteger#)
unsignedLitIntLit :: TyConMap
-> [Type] -> [Value] -> Maybe (Type, Integer, Integer, Integer)
unsignedLitIntLit  = Text
-> TyConMap
-> [Type]
-> [Value]
-> Maybe (Type, Integer, Integer, Integer)
sizedLitIntLit (Name -> Text
forall a. Show a => a -> Text
showt 'Clash.Sized.Internal.Unsigned.fromInteger#)

bitVectorLitIntLit
  :: TyConMap -> [Type] -> [Value]
  -> Maybe (Type,Integer,(Integer,Integer),Integer)
bitVectorLitIntLit :: TyConMap
-> [Type]
-> [Value]
-> Maybe (Type, Integer, (Integer, Integer), Integer)
bitVectorLitIntLit TyConMap
tcm [Type]
tys [Value]
args
  | Just (Type
nTy,Integer
kn) <- TyConMap -> [Type] -> Maybe (Type, Integer)
extractKnownNat TyConMap
tcm [Type]
tys
  , [Value
_
    ,PrimVal PrimInfo
p [Type]
_ [Value
_,Lit (NaturalLiteral Integer
m),Lit (IntegerLiteral Integer
i)]
    ,Value -> Maybe [Term]
valArgs -> Just [Literal (IntLiteral Integer
j)]
    ] <- [Value]
args
  , PrimInfo -> Text
primName PrimInfo
p Text -> Text -> Bool
forall a. Eq a => a -> a -> Bool
== Name -> Text
forall a. Show a => a -> Text
showt 'Clash.Sized.Internal.BitVector.fromInteger#
  = (Type, Integer, (Integer, Integer), Integer)
-> Maybe (Type, Integer, (Integer, Integer), Integer)
forall a. a -> Maybe a
Just (Type
nTy,Integer
kn,(Integer
m,Integer
i),Integer
j)
  | Bool
otherwise
  = Maybe (Type, Integer, (Integer, Integer), Integer)
forall a. Maybe a
Nothing

mkIntCLit :: TyConMap -> (Integer -> Literal) -> Integer -> Type -> Term
mkIntCLit :: TyConMap -> (Integer -> Literal) -> Integer -> Type -> Term
mkIntCLit TyConMap
tcm Integer -> Literal
proj Integer
lit Type
resTy =
  Term -> Term -> Term
App (DataCon -> Term
Data DataCon
intDc) (Literal -> Term
Literal (Integer -> Literal
proj Integer
lit))
 where
  ([Either TyVar Type]
_, Type -> TypeView
tyView -> TyConApp TyConName
intTcNm []) = Type -> ([Either TyVar Type], Type)
splitFunForallTy Type
resTy
  Just TyCon
intTc = TyConName -> TyConMap -> Maybe TyCon
forall a b. Uniquable a => a -> UniqMap b -> Maybe b
UniqMap.lookup TyConName
intTcNm TyConMap
tcm
  [DataCon
intDc] = TyCon -> [DataCon]
tyConDataCons TyCon
intTc

mkFloatCLit :: TyConMap -> Word32 -> Type -> Term
mkFloatCLit :: TyConMap -> Word32 -> Type -> Term
mkFloatCLit TyConMap
tcm Word32
lit Type
resTy =
  Term -> Term -> Term
App (DataCon -> Term
Data DataCon
floatDc) (Literal -> Term
Literal (Word32 -> Literal
FloatLiteral Word32
lit))
 where
  ([Either TyVar Type]
_, Type -> TypeView
tyView -> TyConApp TyConName
floatTcNm []) = Type -> ([Either TyVar Type], Type)
splitFunForallTy Type
resTy
  (Just TyCon
floatTc) = TyConName -> TyConMap -> Maybe TyCon
forall a b. Uniquable a => a -> UniqMap b -> Maybe b
UniqMap.lookup TyConName
floatTcNm TyConMap
tcm
  [DataCon
floatDc] = TyCon -> [DataCon]
tyConDataCons TyCon
floatTc

mkDoubleCLit :: TyConMap -> Word64 -> Type -> Term
mkDoubleCLit :: TyConMap -> Unique -> Type -> Term
mkDoubleCLit TyConMap
tcm Unique
lit Type
resTy =
  Term -> Term -> Term
App (DataCon -> Term
Data DataCon
doubleDc) (Literal -> Term
Literal (Unique -> Literal
DoubleLiteral Unique
lit))
 where
  ([Either TyVar Type]
_, Type -> TypeView
tyView -> TyConApp TyConName
doubleTcNm []) = Type -> ([Either TyVar Type], Type)
splitFunForallTy Type
resTy
  (Just TyCon
doubleTc) = TyConName -> TyConMap -> Maybe TyCon
forall a b. Uniquable a => a -> UniqMap b -> Maybe b
UniqMap.lookup TyConName
doubleTcNm TyConMap
tcm
  [DataCon
doubleDc] = TyCon -> [DataCon]
tyConDataCons TyCon
doubleTc

mkSomeNat :: TyConMap -> Integer -> Type -> Term
mkSomeNat :: TyConMap -> Integer -> Type -> Term
mkSomeNat TyConMap
tcm Integer
lit Type
resTy =
  Term -> [Either Term Type] -> Term
mkApps (DataCon -> Term
Data DataCon
someNatDc)
         [ Type -> Either Term Type
forall a b. b -> Either a b
Right (LitTy -> Type
LitTy (Integer -> LitTy
NumTy Integer
lit))
         , Term -> Either Term Type
forall a b. a -> Either a b
Left (Literal -> Term
Literal (Integer -> Literal
NaturalLiteral Integer
lit))
         , Term -> Either Term Type
forall a b. a -> Either a b
Left Term
proxy
         ]
 where
  -- Get the SomeNat data constructor
  TyConApp TyConName
someNatTcNm [] = Type -> TypeView
tyView Type
resTy
  (Just TyCon
someNatTc) = TyConName -> TyConMap -> Maybe TyCon
forall a b. Uniquable a => a -> UniqMap b -> Maybe b
UniqMap.lookup TyConName
someNatTcNm TyConMap
tcm
  [DataCon
someNatDc] = TyCon -> [DataCon]
tyConDataCons TyCon
someNatTc

  -- Get the Proxy data constructor
  (Either TyVar Type
_:Either TyVar Type
_:Right (Type -> TypeView
tyView -> TyConApp TyConName
proxyTcNm [Type
natTy,Type
_]):[Either TyVar Type]
_,Type
_) =
    Type -> ([Either TyVar Type], Type)
splitFunForallTy (DataCon -> Type
dcType DataCon
someNatDc)
  (Just TyCon
proxyTc) = TyConName -> TyConMap -> Maybe TyCon
forall a b. Uniquable a => a -> UniqMap b -> Maybe b
UniqMap.lookup TyConName
proxyTcNm TyConMap
tcm
  [DataCon
proxyDc] = TyCon -> [DataCon]
tyConDataCons TyCon
proxyTc

  -- Build the Proxy argument
  proxy :: Term
proxy = Term -> [Either Term Type] -> Term
mkApps (DataCon -> Term
Data DataCon
proxyDc)
                 [ Type -> Either Term Type
forall a b. b -> Either a b
Right Type
natTy
                 , Type -> Either Term Type
forall a b. b -> Either a b
Right (LitTy -> Type
LitTy (Integer -> LitTy
NumTy Integer
lit))
                 ]

-- From an argument list to function of type
--   forall n. KnownNat n => ...
-- extract (nTy,nInt)
-- where nTy is the Type of n
-- and   nInt is its value as an Integer
extractKnownNat :: TyConMap -> [Type] -> Maybe (Type, Integer)
extractKnownNat :: TyConMap -> [Type] -> Maybe (Type, Integer)
extractKnownNat TyConMap
tcm [Type]
tys = case [Type]
tys of
  Type
nTy : [Type]
_ | Right Integer
nInt <- Except [Char] Integer -> Either [Char] Integer
forall e a. Except e a -> Either e a
runExcept (TyConMap -> Type -> Except [Char] Integer
tyNatSize TyConMap
tcm Type
nTy)
    -> (Type, Integer) -> Maybe (Type, Integer)
forall a. a -> Maybe a
Just (Type
nTy, Integer
nInt)
  [Type]
_ -> Maybe (Type, Integer)
forall a. Maybe a
Nothing

-- From an argument list to function of type
--   forall n m o .. . (KnownNat n, KnownNat m, KnownNat o, ..) => ...
-- extract [(nTy,nInt), (mTy,mInt), (oTy,oInt)]
-- where nTy is the Type of n
-- and   nInt is its value as an Integer
extractKnownNats :: TyConMap -> [Type] -> [(Type, Integer)]
extractKnownNats :: TyConMap -> [Type] -> [(Type, Integer)]
extractKnownNats TyConMap
tcm =
  (Type -> Maybe (Type, Integer)) -> [Type] -> [(Type, Integer)]
forall a b. (a -> Maybe b) -> [a] -> [b]
mapMaybe (TyConMap -> [Type] -> Maybe (Type, Integer)
extractKnownNat TyConMap
tcm ([Type] -> Maybe (Type, Integer))
-> (Type -> [Type]) -> Type -> Maybe (Type, Integer)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Type -> [Type]
forall a. a -> [a]
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure)

-- Construct a constant term of a sized type
mkSizedLit
  :: (Type -> Term)
  -- ^ Type constructor?
  -> Type
  -- ^ Result type
  -> Type
  -- ^ forall n.
  -> Integer
  -- ^ KnownNat n
  -> Integer
  -- ^ Value to construct
  -> Term
mkSizedLit :: (Type -> Term) -> Type -> Type -> Integer -> Integer -> Term
mkSizedLit Type -> Term
conPrim Type
ty Type
nTy Integer
kn Integer
val =
  Term -> [Either Term Type] -> Term
mkApps
    (Type -> Term
conPrim Type
sTy)
    [ Type -> Either Term Type
forall a b. b -> Either a b
Right Type
nTy
    , Term -> Either Term Type
forall a b. a -> Either a b
Left (Literal -> Term
Literal (Integer -> Literal
NaturalLiteral Integer
kn))
    , Term -> Either Term Type
forall a b. a -> Either a b
Left (Literal -> Term
Literal (Integer -> Literal
IntegerLiteral Integer
val)) ]
 where
    ([Either TyVar Type]
_,Type
sTy) = Type -> ([Either TyVar Type], Type)
splitFunForallTy Type
ty

mkBitLit
  :: Type
  -- ^ Result type
  -> Integer
  -- ^ Mask
  -> Integer
  -- ^ Value
  -> Term
mkBitLit :: Type -> Integer -> Integer -> Term
mkBitLit Type
ty Integer
msk Integer
val =
  Term -> [Either Term Type] -> Term
mkApps (Type -> Term
bConPrim Type
sTy) [ Term -> Either Term Type
forall a b. a -> Either a b
Left (Literal -> Term
Literal (Integer -> Literal
WordLiteral (Integer
msk Integer -> Integer -> Integer
forall a. Bits a => a -> a -> a
.&. Integer
1)))
                        , Term -> Either Term Type
forall a b. a -> Either a b
Left (Literal -> Term
Literal (Integer -> Literal
IntegerLiteral (Integer
val Integer -> Integer -> Integer
forall a. Bits a => a -> a -> a
.&. Integer
1)))]
  where
    ([Either TyVar Type]
_,Type
sTy) = Type -> ([Either TyVar Type], Type)
splitFunForallTy Type
ty

mkSignedLit, mkUnsignedLit
  :: Type
  -- Result type
  -> Type
  -- forall n.
  -> Integer
  -- KnownNat n
  -> Integer
  -- Value
  -> Term
mkSignedLit :: Type -> Type -> Integer -> Integer -> Term
mkSignedLit    = (Type -> Term) -> Type -> Type -> Integer -> Integer -> Term
mkSizedLit Type -> Term
signedConPrim
mkUnsignedLit :: Type -> Type -> Integer -> Integer -> Term
mkUnsignedLit  = (Type -> Term) -> Type -> Type -> Integer -> Integer -> Term
mkSizedLit Type -> Term
unsignedConPrim

mkBitVectorLit
  :: Type
  -- ^ Result type
  -> Type
  -- ^ forall n.
  -> Integer
  -- ^ KnownNat n
  -> Integer
  -- ^ mask
  -> Integer
  -- ^ Value to construct
  -> Term
mkBitVectorLit :: Type -> Type -> Integer -> Integer -> Integer -> Term
mkBitVectorLit Type
ty Type
nTy Integer
kn Integer
mask Integer
val
  = Term -> [Either Term Type] -> Term
mkApps (Type -> Term
bvConPrim Type
sTy)
           [Type -> Either Term Type
forall a b. b -> Either a b
Right Type
nTy
           ,Term -> Either Term Type
forall a b. a -> Either a b
Left (Literal -> Term
Literal (Integer -> Literal
NaturalLiteral Integer
kn))
           ,Term -> Either Term Type
forall a b. a -> Either a b
Left (Literal -> Term
Literal (Integer -> Literal
NaturalLiteral Integer
mask))
           ,Term -> Either Term Type
forall a b. a -> Either a b
Left (Literal -> Term
Literal (Integer -> Literal
IntegerLiteral Integer
val))]
  where
    ([Either TyVar Type]
_,Type
sTy) = Type -> ([Either TyVar Type], Type)
splitFunForallTy Type
ty

mkIndexLitE
  :: Type
  -- ^ Result type
  -> Type
  -- ^ forall n.
  -> Integer
  -- ^ KnownNat n
  -> Integer
  -- ^ Value to construct
  -> Either Term Term
  -- ^ Either undefined (if given value is out of bounds of given type) or term
  -- representing literal
mkIndexLitE :: Type -> Type -> Integer -> Integer -> Either Term Term
mkIndexLitE Type
rTy Type
nTy Integer
kn Integer
val
  | Integer
val Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
>= Integer
0
  , Integer
val Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
< Integer
kn
  = Term -> Either Term Term
forall a b. b -> Either a b
Right ((Type -> Term) -> Type -> Type -> Integer -> Integer -> Term
mkSizedLit Type -> Term
indexConPrim Type
rTy Type
nTy Integer
kn Integer
val)
  | Bool
otherwise
  = Term -> Either Term Term
forall a b. a -> Either a b
Left (Term -> Type -> Term
TyApp (PrimInfo -> Term
Prim PrimInfo
NP.undefined) (TyConName -> [Type] -> Type
mkTyConApp TyConName
indexTcNm [Type
nTy]))
  where
    TyConApp TyConName
indexTcNm [Type]
_ = Type -> TypeView
tyView (([Either TyVar Type], Type) -> Type
forall a b. (a, b) -> b
snd (Type -> ([Either TyVar Type], Type)
splitFunForallTy Type
rTy))

mkIndexLit
  :: Type
  -- ^ Result type
  -> Type
  -- ^ forall n.
  -> Integer
  -- ^ KnownNat n
  -> Integer
  -- ^ Value to construct
  -> Term
mkIndexLit :: Type -> Type -> Integer -> Integer -> Term
mkIndexLit Type
rTy Type
nTy Integer
kn Integer
val =
  (Term -> Term) -> (Term -> Term) -> Either Term Term -> Term
forall a c b. (a -> c) -> (b -> c) -> Either a b -> c
either Term -> Term
forall a. a -> a
id Term -> Term
forall a. a -> a
id (Type -> Type -> Integer -> Integer -> Either Term Term
mkIndexLitE Type
rTy Type
nTy Integer
kn Integer
val)

mkBitVectorLit'
  :: (Type, Type, Integer)
  -- ^ (result type, forall n., KnownNat n)
  -> Integer
  -- ^ Mask
  -> Integer
  -- ^ Value
  -> Term
mkBitVectorLit' :: (Type, Type, Integer) -> Integer -> Integer -> Term
mkBitVectorLit' (Type
ty,Type
nTy,Integer
kn) = Type -> Type -> Integer -> Integer -> Integer -> Term
mkBitVectorLit Type
ty Type
nTy Integer
kn

mkIndexLit'
  :: (Type, Type, Integer)
  -- ^ (result type, forall n., KnownNat n)
  -> Integer
  -- ^ value
  -> Term
mkIndexLit' :: (Type, Type, Integer) -> Integer -> Term
mkIndexLit' (Type
rTy,Type
nTy,Integer
kn) = Type -> Type -> Integer -> Integer -> Term
mkIndexLit Type
rTy Type
nTy Integer
kn

boolToIntLiteral :: Bool -> Term
boolToIntLiteral :: Bool -> Term
boolToIntLiteral Bool
b = if Bool
b then Literal -> Term
Literal (Integer -> Literal
IntLiteral Integer
1) else Literal -> Term
Literal (Integer -> Literal
IntLiteral Integer
0)

boolToBoolLiteral :: TyConMap -> Type -> Bool -> Term
boolToBoolLiteral :: TyConMap -> Type -> Bool -> Term
boolToBoolLiteral TyConMap
tcm Type
ty Bool
b =
 let ([Either TyVar Type]
_,Type -> TypeView
tyView -> TyConApp TyConName
boolTcNm []) = Type -> ([Either TyVar Type], Type)
splitFunForallTy Type
ty
     (Just TyCon
boolTc) = TyConName -> TyConMap -> Maybe TyCon
forall a b. Uniquable a => a -> UniqMap b -> Maybe b
UniqMap.lookup TyConName
boolTcNm TyConMap
tcm
     [DataCon
falseDc,DataCon
trueDc] = TyCon -> [DataCon]
tyConDataCons TyCon
boolTc
     retDc :: DataCon
retDc = if Bool
b then DataCon
trueDc else DataCon
falseDc
 in  DataCon -> Term
Data DataCon
retDc

charToCharLiteral :: Char -> Term
charToCharLiteral :: Char -> Term
charToCharLiteral = Literal -> Term
Literal (Literal -> Term) -> (Char -> Literal) -> Char -> Term
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Char -> Literal
CharLiteral

integerToIntLiteral :: Integer -> Term
integerToIntLiteral :: Integer -> Term
integerToIntLiteral = Literal -> Term
Literal (Literal -> Term) -> (Integer -> Literal) -> Integer -> Term
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Integer -> Literal
IntLiteral (Integer -> Literal) -> (Integer -> Integer) -> Integer -> Literal
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Int -> Integer
forall a. Integral a => a -> Integer
toInteger (Int -> Integer) -> (Integer -> Int) -> Integer -> Integer
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Integer -> Int
forall a. Num a => Integer -> a
fromInteger :: Integer -> Int) -- for overflow behavior

integerToWordLiteral :: Integer -> Term
integerToWordLiteral :: Integer -> Term
integerToWordLiteral = Literal -> Term
Literal (Literal -> Term) -> (Integer -> Literal) -> Integer -> Term
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Integer -> Literal
WordLiteral (Integer -> Literal) -> (Integer -> Integer) -> Integer -> Literal
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Word -> Integer
forall a. Integral a => a -> Integer
toInteger (Word -> Integer) -> (Integer -> Word) -> Integer -> Integer
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Integer -> Word
forall a. Num a => Integer -> a
fromInteger :: Integer -> Word) -- for overflow behavior

integerToInt64Literal :: Integer -> Term
integerToInt64Literal :: Integer -> Term
integerToInt64Literal = Literal -> Term
Literal (Literal -> Term) -> (Integer -> Literal) -> Integer -> Term
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Integer -> Literal
Int64Literal (Integer -> Literal) -> (Integer -> Integer) -> Integer -> Literal
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Int64 -> Integer
forall a. Integral a => a -> Integer
toInteger (Int64 -> Integer) -> (Integer -> Int64) -> Integer -> Integer
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Integer -> Int64
forall a. Num a => Integer -> a
fromInteger :: Integer -> Int64) -- for overflow behavior

integerToWord64Literal :: Integer -> Term
integerToWord64Literal :: Integer -> Term
integerToWord64Literal = Literal -> Term
Literal (Literal -> Term) -> (Integer -> Literal) -> Integer -> Term
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Integer -> Literal
Word64Literal (Integer -> Literal) -> (Integer -> Integer) -> Integer -> Literal
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Unique -> Integer
forall a. Integral a => a -> Integer
toInteger (Unique -> Integer) -> (Integer -> Unique) -> Integer -> Integer
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Integer -> Unique
forall a. Num a => Integer -> a
fromInteger :: Integer -> Word64) -- for overflow behavior

integerToIntegerLiteral :: Integer -> Term
integerToIntegerLiteral :: Integer -> Term
integerToIntegerLiteral = Literal -> Term
Literal (Literal -> Term) -> (Integer -> Literal) -> Integer -> Term
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Integer -> Literal
IntegerLiteral

-- | Implementation shared by every worker of GHC's @powImpl@, i.e. the
-- internal function behind '(^)'.
--
-- GHC's powImpl workers come in five flavors and get renumbered across
-- versions: the (numeric-suffix -> signature) mapping changes between 9.10,
-- 9.12 and 9.14, and may shift again. Rather than hard-code a fragile
-- name->signature table, we register this single implementation under every
-- worker name and dispatch by argument shape: the worker name is known, but
-- which specialization it implements is inferred from the arg literals.
--
-- Shapes:
--   [Int#, Integer]      -> Integer  (small-exponent path, IS exp#)
--   [Int#, Int#]         -> Int#     (Int -> Int -> Int spec, $w$*)
--   [Integer, Int#]      -> Integer  (Integer -> Int -> Integer spec, $w$*)
--   [ByteArray#, Integer]-> Integer  (large-exponent path, IP/IN)
--
-- For the ByteArray# variant we reconstruct the exponent as a positive
-- bignum (IP ba). The negative-bignum (IN) arm is in practice dead: (^)
-- errors on negative exponents before recursing, so reducing IN positively
-- only affects DCE-able code.
powImplWorker :: PrimStepContext -> Maybe Machine
powImplWorker :: PrimStepContext -> Maybe Machine
powImplWorker = \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
..}
    | [Value -> Maybe Integer
intLiteral -> Just Integer
j, Value -> Maybe Integer
integerLiteral -> Just Integer
i] <- [Value]
args
    -> Term -> Maybe Machine
reduce (Term -> Term
catchErrorCall (Integer -> Term
integerToIntegerLiteral (Integer -> Term) -> Integer -> Term
forall a b. (a -> b) -> a -> b
$ Integer
i Integer -> Integer -> Integer
forall a b. (Num a, Integral b) => a -> b -> a
^ Integer
j))
    | [Value -> Maybe Integer
integerLiteral -> Just Integer
i, Value -> Maybe Integer
intLiteral -> Just Integer
j] <- [Value]
args
    -> Term -> Maybe Machine
reduce (Term -> Term
catchErrorCall (Integer -> Term
integerToIntegerLiteral (Integer -> Term) -> Integer -> Term
forall a b. (a -> b) -> a -> b
$ Integer
i Integer -> Integer -> Integer
forall a b. (Num a, Integral b) => a -> b -> a
^ Integer
j))
    | [Value -> Maybe Integer
intLiteral -> Just Integer
i, Value -> Maybe Integer
intLiteral -> Just Integer
j] <- [Value]
args
    -> Term -> Maybe Machine
reduce (Term -> Term
catchErrorCall (Integer -> Term
integerToIntLiteral (Integer -> Term) -> Integer -> Term
forall a b. (a -> b) -> a -> b
$ Integer
i Integer -> Integer -> Integer
forall a b. (Num a, Integral b) => a -> b -> a
^ Integer
j))
    | [Lit (ByteArrayLiteral (BA.ByteArray ByteArray#
ba)), Value -> Maybe Integer
integerLiteral -> Just Integer
i] <- [Value]
args
    -> Term -> Maybe Machine
reduce (Term -> Term
catchErrorCall (Integer -> Term
integerToIntegerLiteral (Integer -> Term) -> Integer -> Term
forall a b. (a -> b) -> a -> b
$ Integer
i Integer -> Integer -> Integer
forall a b. (Num a, Integral b) => a -> b -> a
^ ByteArray# -> Integer
IP ByteArray#
ba))
  PrimStepContext
_ -> Maybe Machine
forall a. Maybe a
Nothing

naturalToNaturalLiteral :: Natural -> Term
naturalToNaturalLiteral :: Natural -> Term
naturalToNaturalLiteral = Literal -> Term
Literal (Literal -> Term) -> (Natural -> Literal) -> Natural -> Term
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Integer -> Literal
NaturalLiteral (Integer -> Literal) -> (Natural -> Integer) -> Natural -> Literal
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Natural -> Integer
forall a. Integral a => a -> Integer
toInteger

bConPrim :: Type -> Term
bConPrim :: Type -> Term
bConPrim (Type -> TypeView
tyView -> TyConApp TyConName
bTcNm [Type]
_)
  = PrimInfo -> Term
Prim (Text
-> Type -> WorkInfo -> IsMultiPrim -> PrimUnfolding -> PrimInfo
PrimInfo (Name -> Text
forall a. Show a => a -> Text
showt 'Clash.Sized.Internal.BitVector.fromInteger##) Type
funTy WorkInfo
WorkNever IsMultiPrim
SingleResult PrimUnfolding
NoUnfolding)
  where
    funTy :: Type
funTy      = (Type -> Type -> Type) -> [Type] -> Type
forall a. (a -> a -> a) -> [a] -> a
forall (t :: Type -> Type) a.
Foldable t =>
(a -> a -> a) -> t a -> a
foldr1 Type -> Type -> Type
mkFunTy [Type
wordPrimTy,Type
integerPrimTy,TyConName -> [Type] -> Type
mkTyConApp TyConName
bTcNm []]
bConPrim Type
_ = [Char] -> Term
forall a. HasCallStack => [Char] -> a
error ([Char] -> Term) -> [Char] -> Term
forall a b. (a -> b) -> a -> b
$ $(curLoc) [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Char]
"called with incorrect type"

bvConPrim :: Type -> Term
bvConPrim :: Type -> Term
bvConPrim (Type -> TypeView
tyView -> TyConApp TyConName
bvTcNm [Type]
_)
  = PrimInfo -> Term
Prim (Text
-> Type -> WorkInfo -> IsMultiPrim -> PrimUnfolding -> PrimInfo
PrimInfo (Name -> Text
forall a. Show a => a -> Text
showt 'Clash.Sized.Internal.BitVector.fromInteger#) (TyVar -> Type -> Type
ForAllTy TyVar
nTV Type
funTy) WorkInfo
WorkNever IsMultiPrim
SingleResult PrimUnfolding
NoUnfolding)
  where
    funTy :: Type
funTy = (Type -> Type -> Type) -> [Type] -> Type
forall a. (a -> a -> a) -> [a] -> a
forall (t :: Type -> Type) a.
Foldable t =>
(a -> a -> a) -> t a -> a
foldr1 Type -> Type -> Type
mkFunTy [Type
naturalPrimTy,Type
naturalPrimTy,Type
integerPrimTy,TyConName -> [Type] -> Type
mkTyConApp TyConName
bvTcNm [Type
nVar]]
    nName :: Name a
nName = Text -> Unique -> Name a
forall a. Text -> Unique -> Name a
mkUnsafeSystemName Text
"n" Unique
0
    nVar :: Type
nVar  = TyVar -> Type
VarTy TyVar
nTV
    nTV :: TyVar
nTV   = Type -> TyName -> TyVar
mkTyVar Type
typeNatKind TyName
forall {a}. Name a
nName
bvConPrim Type
_ = [Char] -> Term
forall a. HasCallStack => [Char] -> a
error ([Char] -> Term) -> [Char] -> Term
forall a b. (a -> b) -> a -> b
$ $(curLoc) [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Char]
"called with incorrect type"

indexConPrim :: Type -> Term
indexConPrim :: Type -> Term
indexConPrim (Type -> TypeView
tyView -> TyConApp TyConName
indexTcNm [Type]
_)
  = PrimInfo -> Term
Prim (Text
-> Type -> WorkInfo -> IsMultiPrim -> PrimUnfolding -> PrimInfo
PrimInfo (Name -> Text
forall a. Show a => a -> Text
showt 'Clash.Sized.Internal.Index.fromInteger#) (TyVar -> Type -> Type
ForAllTy TyVar
nTV Type
funTy) WorkInfo
WorkNever IsMultiPrim
SingleResult PrimUnfolding
NoUnfolding)
  where
    funTy :: Type
funTy        = (Type -> Type -> Type) -> [Type] -> Type
forall a. (a -> a -> a) -> [a] -> a
forall (t :: Type -> Type) a.
Foldable t =>
(a -> a -> a) -> t a -> a
foldr1 Type -> Type -> Type
mkFunTy [Type
naturalPrimTy,Type
integerPrimTy,TyConName -> [Type] -> Type
mkTyConApp TyConName
indexTcNm [Type
nVar]]
    nName :: Name a
nName      = Text -> Unique -> Name a
forall a. Text -> Unique -> Name a
mkUnsafeSystemName Text
"n" Unique
0
    nVar :: Type
nVar       = TyVar -> Type
VarTy TyVar
nTV
    nTV :: TyVar
nTV        = Type -> TyName -> TyVar
mkTyVar Type
typeNatKind TyName
forall {a}. Name a
nName
indexConPrim Type
_ = [Char] -> Term
forall a. HasCallStack => [Char] -> a
error ([Char] -> Term) -> [Char] -> Term
forall a b. (a -> b) -> a -> b
$ $(curLoc) [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Char]
"called with incorrect type"

signedConPrim :: Type -> Term
signedConPrim :: Type -> Term
signedConPrim (Type -> TypeView
tyView -> TyConApp TyConName
signedTcNm [Type]
_)
  = PrimInfo -> Term
Prim (Text
-> Type -> WorkInfo -> IsMultiPrim -> PrimUnfolding -> PrimInfo
PrimInfo (Name -> Text
forall a. Show a => a -> Text
showt 'Clash.Sized.Internal.Signed.fromInteger#) (TyVar -> Type -> Type
ForAllTy TyVar
nTV Type
funTy) WorkInfo
WorkNever IsMultiPrim
SingleResult PrimUnfolding
NoUnfolding)
  where
    funTy :: Type
funTy        = (Type -> Type -> Type) -> [Type] -> Type
forall a. (a -> a -> a) -> [a] -> a
forall (t :: Type -> Type) a.
Foldable t =>
(a -> a -> a) -> t a -> a
foldr1 Type -> Type -> Type
mkFunTy [Type
naturalPrimTy,Type
integerPrimTy,TyConName -> [Type] -> Type
mkTyConApp TyConName
signedTcNm [Type
nVar]]
    nName :: Name a
nName      = Text -> Unique -> Name a
forall a. Text -> Unique -> Name a
mkUnsafeSystemName Text
"n" Unique
0
    nVar :: Type
nVar       = TyVar -> Type
VarTy TyVar
nTV
    nTV :: TyVar
nTV        = Type -> TyName -> TyVar
mkTyVar Type
typeNatKind TyName
forall {a}. Name a
nName
signedConPrim Type
_ = [Char] -> Term
forall a. HasCallStack => [Char] -> a
error ([Char] -> Term) -> [Char] -> Term
forall a b. (a -> b) -> a -> b
$ $(curLoc) [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Char]
"called with incorrect type"

unsignedConPrim :: Type -> Term
unsignedConPrim :: Type -> Term
unsignedConPrim (Type -> TypeView
tyView -> TyConApp TyConName
unsignedTcNm [Type]
_)
  = PrimInfo -> Term
Prim (Text
-> Type -> WorkInfo -> IsMultiPrim -> PrimUnfolding -> PrimInfo
PrimInfo (Name -> Text
forall a. Show a => a -> Text
showt 'Clash.Sized.Internal.Unsigned.fromInteger#) (TyVar -> Type -> Type
ForAllTy TyVar
nTV Type
funTy) WorkInfo
WorkNever IsMultiPrim
SingleResult PrimUnfolding
NoUnfolding)
  where
    funTy :: Type
funTy        = (Type -> Type -> Type) -> [Type] -> Type
forall a. (a -> a -> a) -> [a] -> a
forall (t :: Type -> Type) a.
Foldable t =>
(a -> a -> a) -> t a -> a
foldr1 Type -> Type -> Type
mkFunTy [Type
naturalPrimTy,Type
integerPrimTy,TyConName -> [Type] -> Type
mkTyConApp TyConName
unsignedTcNm [Type
nVar]]
    nName :: Name a
nName        = Text -> Unique -> Name a
forall a. Text -> Unique -> Name a
mkUnsafeSystemName Text
"n" Unique
0
    nVar :: Type
nVar         = TyVar -> Type
VarTy TyVar
nTV
    nTV :: TyVar
nTV          = Type -> TyName -> TyVar
mkTyVar Type
typeNatKind TyName
forall {a}. Name a
nName
unsignedConPrim Type
_ = [Char] -> Term
forall a. HasCallStack => [Char] -> a
error ([Char] -> Term) -> [Char] -> Term
forall a b. (a -> b) -> a -> b
$ $(curLoc) [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Char]
"called with incorrect type"


-- |  Lift a binary function over 'Unsigned' values to be used as literal Evaluator
--
--
liftUnsigned2 :: KnownNat n
              => (Unsigned n -> Unsigned n -> Unsigned n)
              -> Type
              -> TyConMap
              -> [Type]
              -> [Value]
              -> (Proxy n -> Maybe Term)
liftUnsigned2 :: forall (n :: Natural).
KnownNat n =>
(Unsigned n -> Unsigned n -> Unsigned n)
-> Type -> TyConMap -> [Type] -> [Value] -> Proxy n -> Maybe Term
liftUnsigned2 = ([Value] -> [Integer])
-> (Type -> Type -> Integer -> Integer -> Term)
-> (Unsigned n -> Unsigned n -> Unsigned n)
-> Type
-> TyConMap
-> [Type]
-> [Value]
-> Proxy n
-> Maybe Term
forall (n :: Natural) (sized :: Natural -> Type).
(KnownNat n, Integral (sized n)) =>
([Value] -> [Integer])
-> (Type -> Type -> Integer -> Integer -> Term)
-> (sized n -> sized n -> sized n)
-> Type
-> TyConMap
-> [Type]
-> [Value]
-> Proxy n
-> Maybe Term
liftSized2 [Value] -> [Integer]
unsignedLiterals' Type -> Type -> Integer -> Integer -> Term
mkUnsignedLit

liftSigned2 :: KnownNat n
              => (Signed n -> Signed n -> Signed n)
              -> Type
              -> TyConMap
              -> [Type]
              -> [Value]
              -> (Proxy n -> Maybe Term)
liftSigned2 :: forall (n :: Natural).
KnownNat n =>
(Signed n -> Signed n -> Signed n)
-> Type -> TyConMap -> [Type] -> [Value] -> Proxy n -> Maybe Term
liftSigned2 = ([Value] -> [Integer])
-> (Type -> Type -> Integer -> Integer -> Term)
-> (Signed n -> Signed n -> Signed n)
-> Type
-> TyConMap
-> [Type]
-> [Value]
-> Proxy n
-> Maybe Term
forall (n :: Natural) (sized :: Natural -> Type).
(KnownNat n, Integral (sized n)) =>
([Value] -> [Integer])
-> (Type -> Type -> Integer -> Integer -> Term)
-> (sized n -> sized n -> sized n)
-> Type
-> TyConMap
-> [Type]
-> [Value]
-> Proxy n
-> Maybe Term
liftSized2 [Value] -> [Integer]
signedLiterals' Type -> Type -> Integer -> Integer -> Term
mkSignedLit

liftBitVector2 :: KnownNat n
              => (BitVector n -> BitVector n -> BitVector n)
              -> Type
              -> TyConMap
              -> [Type]
              -> [Value]
              -> (Proxy n -> Maybe Term)
liftBitVector2 :: 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
f Type
ty TyConMap
tcm [Type]
tys [Value]
args Proxy n
_p
  | Just (Type
nTy, Integer
kn) <- TyConMap -> [Type] -> Maybe (Type, Integer)
extractKnownNat TyConMap
tcm [Type]
tys
  , [(Integer, Integer)
i,(Integer, Integer)
j] <- [Value] -> [(Integer, Integer)]
bitVectorLiterals' [Value]
args
  = let BV Natural
mask Natural
val = BitVector n -> BitVector n -> BitVector n
f ((Integer, Integer) -> BitVector n
forall (n :: Natural). (Integer, Integer) -> BitVector n
toBV (Integer, Integer)
i) ((Integer, Integer) -> BitVector n
forall (n :: Natural). (Integer, Integer) -> BitVector n
toBV (Integer, Integer)
j)
    in Term -> Maybe Term
forall a. a -> Maybe a
Just (Term -> Maybe Term) -> Term -> Maybe Term
forall a b. (a -> b) -> a -> b
$ Type -> Type -> Integer -> Integer -> Integer -> Term
mkBitVectorLit Type
ty Type
nTy Integer
kn (Natural -> Integer
forall a. Integral a => a -> Integer
toInteger Natural
mask) (Natural -> Integer
forall a. Integral a => a -> Integer
toInteger Natural
val)
  | Bool
otherwise = Maybe Term
forall a. Maybe a
Nothing

liftBitVector2Bool :: KnownNat n
              => (BitVector n -> BitVector n -> Bool)
              -> Type
              -> TyConMap
              -> [Value]
              -> (Proxy n -> Maybe Term)
liftBitVector2Bool :: forall (n :: Natural).
KnownNat n =>
(BitVector n -> BitVector n -> Bool)
-> Type -> TyConMap -> [Value] -> Proxy n -> Maybe Term
liftBitVector2Bool  BitVector n -> BitVector n -> Bool
f Type
ty TyConMap
tcm [Value]
args Proxy n
_p
  | [(Integer, Integer)
i,(Integer, Integer)
j] <- [Value] -> [(Integer, Integer)]
bitVectorLiterals' [Value]
args
  = let val :: Bool
val = BitVector n -> BitVector n -> Bool
f ((Integer, Integer) -> BitVector n
forall (n :: Natural). (Integer, Integer) -> BitVector n
toBV (Integer, Integer)
i) ((Integer, Integer) -> BitVector n
forall (n :: Natural). (Integer, Integer) -> BitVector n
toBV (Integer, Integer)
j)
    in Term -> Maybe Term
forall a. a -> Maybe a
Just (Term -> Maybe Term) -> Term -> Maybe Term
forall a b. (a -> b) -> a -> b
$ TyConMap -> Type -> Bool -> Term
boolToBoolLiteral TyConMap
tcm Type
ty Bool
val
  | Bool
otherwise = Maybe Term
forall a. Maybe a
Nothing

liftInteger2BitVector
  :: KnownNat n
  => (Integer -> BitVector n)
  -> (Type, Type, Integer)
  -> [Value]
  -> (Proxy n -> Maybe Term)
liftInteger2BitVector :: forall (n :: Natural).
KnownNat n =>
(Integer -> BitVector n)
-> (Type, Type, Integer) -> [Value] -> Proxy n -> Maybe Term
liftInteger2BitVector Integer -> BitVector n
f (Type, Type, Integer)
resTyInfo [Value]
args Proxy n
_p
  | [Integer
i] <- [Value] -> [Integer]
intCLiterals' [Value]
args
  = let BV Natural
msk Natural
val = Integer -> BitVector n
f Integer
i
     in Term -> Maybe Term
forall a. a -> Maybe a
Just ((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))

  | Bool
otherwise
  = Maybe Term
forall a. Maybe a
Nothing

liftBitVector2CInt
  :: KnownNat n
  => TyConMap
  -> Type
  -> (BitVector n -> Integer)
  -> [Value]
  -> (Proxy n -> Maybe Term)
liftBitVector2CInt :: forall (n :: Natural).
KnownNat n =>
TyConMap
-> Type
-> (BitVector n -> Integer)
-> [Value]
-> Proxy n
-> Maybe Term
liftBitVector2CInt TyConMap
tcm Type
resTy BitVector n -> Integer
f [Value]
args Proxy n
_p
  | [(Integer, Integer)
i] <- [Value] -> [(Integer, Integer)]
bitVectorLiterals' [Value]
args
  = let val :: Integer
val = BitVector n -> Integer
f ((Integer, Integer) -> BitVector n
forall (n :: Natural). (Integer, Integer) -> BitVector n
toBV (Integer, Integer)
i)
     in Term -> Maybe Term
forall a. a -> Maybe a
Just (Term -> Maybe Term) -> Term -> Maybe Term
forall a b. (a -> b) -> a -> b
$ TyConMap -> (Integer -> Literal) -> Integer -> Type -> Term
mkIntCLit TyConMap
tcm Integer -> Literal
IntLiteral Integer
val Type
resTy
  | Bool
otherwise
  = Maybe Term
forall a. Maybe a
Nothing

liftSized2 :: (KnownNat n, Integral (sized n))
           => ([Value] -> [Integer])
              -- ^ literal argument extraction function
           -> (Type -> Type -> Integer -> Integer -> Term)
              -- ^ literal contruction function
           -> (sized n -> sized n -> sized n)
           -> Type
           -> TyConMap
           -> [Type]
           -> [Value]
           -> (Proxy n -> Maybe Term)
liftSized2 :: forall (n :: Natural) (sized :: Natural -> Type).
(KnownNat n, Integral (sized n)) =>
([Value] -> [Integer])
-> (Type -> Type -> Integer -> Integer -> Term)
-> (sized n -> sized n -> sized n)
-> Type
-> TyConMap
-> [Type]
-> [Value]
-> Proxy n
-> Maybe Term
liftSized2 [Value] -> [Integer]
extractLitArgs Type -> Type -> Integer -> Integer -> Term
mkLit sized n -> sized n -> sized n
f Type
ty TyConMap
tcm [Type]
tys [Value]
args Proxy n
p
  | Just (Type
nTy, Integer
kn) <- TyConMap -> [Type] -> Maybe (Type, Integer)
extractKnownNat TyConMap
tcm [Type]
tys
  , [Integer
i,Integer
j] <- [Value] -> [Integer]
extractLitArgs [Value]
args
  = let val :: Integer
val = (sized n -> sized n -> sized 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 sized n -> sized n -> sized n
f Integer
i Integer
j Proxy n
p
    in Term -> Maybe Term
forall a. a -> Maybe a
Just (Term -> Maybe Term) -> Term -> Maybe Term
forall a b. (a -> b) -> a -> b
$ Type -> Type -> Integer -> Integer -> Term
mkLit Type
ty Type
nTy Integer
kn Integer
val
  | Bool
otherwise = Maybe Term
forall a. Maybe a
Nothing

-- | Helper to run a function over sized types on integers
--
-- This only works on function of type (sized n -> sized n -> sized n)
-- The resulting function must be executed with reifyNat
runSizedF
  :: (KnownNat n, Integral (sized n))
  => (sized n -> sized n -> sized n)
  -- ^ function to run
  -> Integer
  -- ^ first  argument
  -> Integer
  -- ^ second argument
  -> (Proxy n -> Integer)
runSizedF :: forall (n :: Natural) (sized :: Natural -> Type).
(KnownNat n, Integral (sized n)) =>
(sized n -> sized n -> sized n)
-> Integer -> Integer -> Proxy n -> Integer
runSizedF sized n -> sized n -> sized n
f Integer
i Integer
j Proxy n
_ = sized n -> Integer
forall a. Integral a => a -> Integer
toInteger (sized n -> Integer) -> sized n -> Integer
forall a b. (a -> b) -> a -> b
$ sized n -> sized n -> sized n
f (Integer -> sized n
forall a. Num a => Integer -> a
fromInteger Integer
i) (Integer -> sized n
forall a. Num a => Integer -> a
fromInteger Integer
j)

extractTySizeInfo :: TyConMap -> Type -> [Type] -> (Type, Type, Integer)
extractTySizeInfo :: TyConMap -> Type -> [Type] -> (Type, Type, Integer)
extractTySizeInfo TyConMap
tcm Type
ty [Type]
tys = (Type
resTy,Type
resSizeTy,Integer
resSize)
  where
    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
resSize = Except [Char] Integer -> Either [Char] Integer
forall e a. Except e a -> Either e a
runExcept (TyConMap -> Type -> Except [Char] Integer
tyNatSize TyConMap
tcm Type
resSizeTy)

getResultTy
  :: TyConMap
  -> Type
  -> [Type]
  -> Type
getResultTy :: TyConMap -> Type -> [Type] -> Type
getResultTy TyConMap
tcm Type
ty [Type]
tys = Type
resTy
 where
  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'

liftDDI :: (Double# -> Double# -> Int#) -> [Value] -> Maybe Term
liftDDI :: (Double# -> Double# -> Int#) -> [Value] -> Maybe Term
liftDDI Double# -> Double# -> Int#
f [Value]
args = case [Value] -> [Unique]
doubleLiterals' [Value]
args of
  [Unique
i,Unique
j] -> Term -> Maybe Term
forall a. a -> Maybe a
Just (Term -> Maybe Term) -> Term -> Maybe Term
forall a b. (a -> b) -> a -> b
$ (Double# -> Double# -> Int#) -> Unique -> Unique -> Term
runDDI Double# -> Double# -> Int#
f Unique
i Unique
j
  [Unique]
_     -> Maybe Term
forall a. Maybe a
Nothing
liftDDD :: (Double# -> Double# -> Double#) -> [Value] -> Maybe Term
liftDDD :: (Double# -> Double# -> Double#) -> [Value] -> Maybe Term
liftDDD Double# -> Double# -> Double#
f [Value]
args = case [Value] -> [Unique]
doubleLiterals' [Value]
args of
  [Unique
i,Unique
j] -> Term -> Maybe Term
forall a. a -> Maybe a
Just (Term -> Maybe Term) -> Term -> Maybe Term
forall a b. (a -> b) -> a -> b
$ (Double# -> Double# -> Double#) -> Unique -> Unique -> Term
runDDD Double# -> Double# -> Double#
f Unique
i Unique
j
  [Unique]
_     -> Maybe Term
forall a. Maybe a
Nothing
liftDD  :: (Double# -> Double#) -> [Value] -> Maybe Term
liftDD :: (Double# -> Double#) -> [Value] -> Maybe Term
liftDD  Double# -> Double#
f [Value]
args = case [Value] -> [Unique]
doubleLiterals' [Value]
args of
  [Unique
i]   -> Term -> Maybe Term
forall a. a -> Maybe a
Just (Term -> Maybe Term) -> Term -> Maybe Term
forall a b. (a -> b) -> a -> b
$ (Double# -> Double#) -> Unique -> Term
runDD Double# -> Double#
f Unique
i
  [Unique]
_     -> Maybe Term
forall a. Maybe a
Nothing
runDDI :: (Double# -> Double# -> Int#) -> Word64 -> Word64 -> Term
runDDI :: (Double# -> Double# -> Int#) -> Unique -> Unique -> Term
runDDI Double# -> Double# -> Int#
f Unique
i Unique
j
  = let !(D# Double#
a) = Unique -> Double
castWord64ToDouble Unique
i
        !(D# Double#
b) = Unique -> Double
castWord64ToDouble Unique
j
        r :: Int#
r = Double# -> Double# -> Int#
f Double#
a Double#
b
    in  Literal -> Term
Literal (Literal -> Term) -> (Int -> Literal) -> Int -> Term
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Integer -> Literal
IntLiteral (Integer -> Literal) -> (Int -> Integer) -> Int -> Literal
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Int -> Integer
forall a. Integral a => a -> Integer
toInteger (Int -> Term) -> Int -> Term
forall a b. (a -> b) -> a -> b
$ Int# -> Int
I# Int#
r
runDDD :: (Double# -> Double# -> Double#) -> Word64 -> Word64 -> Term
runDDD :: (Double# -> Double# -> Double#) -> Unique -> Unique -> Term
runDDD Double# -> Double# -> Double#
f Unique
i Unique
j
  = let !(D# Double#
a) = Unique -> Double
castWord64ToDouble Unique
i
        !(D# Double#
b) = Unique -> Double
castWord64ToDouble Unique
j
        r :: Double#
r = Double# -> Double# -> Double#
f Double#
a Double#
b
    in  Literal -> Term
Literal (Literal -> Term) -> (Double -> Literal) -> Double -> Term
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Unique -> Literal
DoubleLiteral (Unique -> Literal) -> (Double -> Unique) -> Double -> Literal
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Double -> Unique
castDoubleToWord64 (Double -> Term) -> Double -> Term
forall a b. (a -> b) -> a -> b
$ Double# -> Double
D# Double#
r
runDD :: (Double# -> Double#) -> Word64 -> Term
runDD :: (Double# -> Double#) -> Unique -> Term
runDD Double# -> Double#
f Unique
i
  = let !(D# Double#
a) = Unique -> Double
castWord64ToDouble Unique
i
        r :: Double#
r = Double# -> Double#
f Double#
a
    in  Literal -> Term
Literal (Literal -> Term) -> (Double -> Literal) -> Double -> Term
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Unique -> Literal
DoubleLiteral (Unique -> Literal) -> (Double -> Unique) -> Double -> Literal
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Double -> Unique
castDoubleToWord64 (Double -> Term) -> Double -> Term
forall a b. (a -> b) -> a -> b
$ Double# -> Double
D# Double#
r

liftFFI :: (Float# -> Float# -> Int#) -> [Value] -> Maybe Term
liftFFI :: (Float# -> Float# -> Int#) -> [Value] -> Maybe Term
liftFFI Float# -> Float# -> Int#
f [Value]
args = case [Value] -> [Word32]
floatLiterals' [Value]
args of
  [Word32
i,Word32
j] -> Term -> Maybe Term
forall a. a -> Maybe a
Just (Term -> Maybe Term) -> Term -> Maybe Term
forall a b. (a -> b) -> a -> b
$ (Float# -> Float# -> Int#) -> Word32 -> Word32 -> Term
runFFI Float# -> Float# -> Int#
f Word32
i Word32
j
  [Word32]
_     -> Maybe Term
forall a. Maybe a
Nothing
liftFFF :: (Float# -> Float# -> Float#) -> [Value] -> Maybe Term
liftFFF :: (Float# -> Float# -> Float#) -> [Value] -> Maybe Term
liftFFF Float# -> Float# -> Float#
f [Value]
args = case [Value] -> [Word32]
floatLiterals' [Value]
args of
  [Word32
i,Word32
j] -> Term -> Maybe Term
forall a. a -> Maybe a
Just (Term -> Maybe Term) -> Term -> Maybe Term
forall a b. (a -> b) -> a -> b
$ (Float# -> Float# -> Float#) -> Word32 -> Word32 -> Term
runFFF Float# -> Float# -> Float#
f Word32
i Word32
j
  [Word32]
_     -> Maybe Term
forall a. Maybe a
Nothing
liftFF  :: (Float# -> Float#) -> [Value] -> Maybe Term
liftFF :: (Float# -> Float#) -> [Value] -> Maybe Term
liftFF  Float# -> Float#
f [Value]
args = case [Value] -> [Word32]
floatLiterals' [Value]
args of
  [Word32
i]   -> Term -> Maybe Term
forall a. a -> Maybe a
Just (Term -> Maybe Term) -> Term -> Maybe Term
forall a b. (a -> b) -> a -> b
$ (Float# -> Float#) -> Word32 -> Term
runFF Float# -> Float#
f Word32
i
  [Word32]
_     -> Maybe Term
forall a. Maybe a
Nothing
runFFI :: (Float# -> Float# -> Int#) -> Word32 -> Word32 -> Term
runFFI :: (Float# -> Float# -> Int#) -> Word32 -> Word32 -> Term
runFFI Float# -> Float# -> Int#
f Word32
i Word32
j
  = let !(F# Float#
a) = Word32 -> Float
castWord32ToFloat Word32
i
        !(F# Float#
b) = Word32 -> Float
castWord32ToFloat Word32
j
        r :: Int#
r = Float# -> Float# -> Int#
f Float#
a Float#
b
    in  Literal -> Term
Literal (Literal -> Term) -> (Int -> Literal) -> Int -> Term
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Integer -> Literal
IntLiteral (Integer -> Literal) -> (Int -> Integer) -> Int -> Literal
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Int -> Integer
forall a. Integral a => a -> Integer
toInteger (Int -> Term) -> Int -> Term
forall a b. (a -> b) -> a -> b
$ Int# -> Int
I# Int#
r
runFFF :: (Float# -> Float# -> Float#) -> Word32 -> Word32 -> Term
runFFF :: (Float# -> Float# -> Float#) -> Word32 -> Word32 -> Term
runFFF Float# -> Float# -> Float#
f Word32
i Word32
j
  = let !(F# Float#
a) = Word32 -> Float
castWord32ToFloat Word32
i
        !(F# Float#
b) = Word32 -> Float
castWord32ToFloat Word32
j
        r :: Float#
r = Float# -> Float# -> Float#
f Float#
a Float#
b
    in  Literal -> Term
Literal (Literal -> Term) -> (Float -> Literal) -> Float -> Term
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Word32 -> Literal
FloatLiteral (Word32 -> Literal) -> (Float -> Word32) -> Float -> Literal
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Float -> Word32
castFloatToWord32 (Float -> Term) -> Float -> Term
forall a b. (a -> b) -> a -> b
$ Float# -> Float
F# Float#
r
runFF :: (Float# -> Float#) -> Word32 -> Term
runFF :: (Float# -> Float#) -> Word32 -> Term
runFF Float# -> Float#
f Word32
i
  = let !(F# Float#
a) = Word32 -> Float
castWord32ToFloat Word32
i
        r :: Float#
r = Float# -> Float#
f Float#
a
    in  Literal -> Term
Literal (Literal -> Term) -> (Float -> Literal) -> Float -> Term
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Word32 -> Literal
FloatLiteral (Word32 -> Literal) -> (Float -> Word32) -> Float -> Literal
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Float -> Word32
castFloatToWord32 (Float -> Term) -> Float -> Term
forall a b. (a -> b) -> a -> b
$ Float# -> Float
F# Float#
r

liftI8 :: (Int8# -> Int8# -> Int8#) -> [Value] -> Maybe Term
liftI8 :: (Int8# -> Int8# -> Int8#) -> [Value] -> Maybe Term
liftI8 Int8# -> Int8# -> Int8#
f [Value]
args = case [Value] -> [Integer]
int8Literals' [Value]
args of
  [Integer
i,Integer
j] ->
    let !(I8# Int8#
a) = Integer -> Int8
forall a. Num a => Integer -> a
fromInteger Integer
i
        !(I8# Int8#
b) = Integer -> Int8
forall a. Num a => Integer -> a
fromInteger Integer
j
     in Term -> Maybe Term
forall a. a -> Maybe a
Just (Literal -> Term
Literal (Integer -> Literal
Int8Literal (Int8 -> Integer
forall a. Integral a => a -> Integer
toInteger (Int8# -> Int8
I8# (Int8# -> Int8# -> Int8#
f Int8#
a Int8#
b)))))
  [Integer]
_ -> Maybe Term
forall a. Maybe a
Nothing

liftI8I :: (Int8# -> Int# -> Int8#) -> [Value] -> Maybe Term
liftI8I :: (Int8# -> Int# -> Int8#) -> [Value] -> Maybe Term
liftI8I Int8# -> Int# -> Int8#
f [Value]
args = case [Value]
args of
  [Lit (Int8Literal Integer
i),Lit (IntLiteral Integer
j)] ->
    let !(I8# Int8#
a) = Integer -> Int8
forall a. Num a => Integer -> a
fromInteger Integer
i
        !(I# Int#
b) = Integer -> Int
forall a. Num a => Integer -> a
fromInteger Integer
j
     in Term -> Maybe Term
forall a. a -> Maybe a
Just (Literal -> Term
Literal (Integer -> Literal
Int8Literal (Int8 -> Integer
forall a. Integral a => a -> Integer
toInteger (Int8# -> Int8
I8# (Int8# -> Int# -> Int8#
f Int8#
a Int#
b)))))
  [Value]
_ -> Maybe Term
forall a. Maybe a
Nothing

liftI8RI :: (Int8# -> Int8# -> Int#) -> [Value] -> Maybe Term
liftI8RI :: (Int8# -> Int8# -> Int#) -> [Value] -> Maybe Term
liftI8RI Int8# -> Int8# -> Int#
f [Value]
args = case [Value] -> [Integer]
int8Literals' [Value]
args of
  [Integer
i,Integer
j] ->
    let !(I8# Int8#
a) = Integer -> Int8
forall a. Num a => Integer -> a
fromInteger Integer
i
        !(I8# Int8#
b) = Integer -> Int8
forall a. Num a => Integer -> a
fromInteger Integer
j
     in Term -> Maybe Term
forall a. a -> Maybe a
Just (Literal -> Term
Literal (Integer -> Literal
IntLiteral (Int -> Integer
forall a. Integral a => a -> Integer
toInteger (Int# -> Int
I# (Int8# -> Int8# -> Int#
f Int8#
a Int8#
b)))))
  [Integer]
_ -> Maybe Term
forall a. Maybe a
Nothing

liftI16 :: (Int16# -> Int16# -> Int16#) -> [Value] -> Maybe Term
liftI16 :: (Int16# -> Int16# -> Int16#) -> [Value] -> Maybe Term
liftI16 Int16# -> Int16# -> Int16#
f [Value]
args = case [Value] -> [Integer]
int16Literals' [Value]
args of
  [Integer
i,Integer
j] ->
    let !(I16# Int16#
a) = Integer -> Int16
forall a. Num a => Integer -> a
fromInteger Integer
i
        !(I16# Int16#
b) = Integer -> Int16
forall a. Num a => Integer -> a
fromInteger Integer
j
     in Term -> Maybe Term
forall a. a -> Maybe a
Just (Literal -> Term
Literal (Integer -> Literal
Int16Literal (Int16 -> Integer
forall a. Integral a => a -> Integer
toInteger (Int16# -> Int16
I16# (Int16# -> Int16# -> Int16#
f Int16#
a Int16#
b)))))
  [Integer]
_ -> Maybe Term
forall a. Maybe a
Nothing

liftI16I :: (Int16# -> Int# -> Int16#) -> [Value] -> Maybe Term
liftI16I :: (Int16# -> Int# -> Int16#) -> [Value] -> Maybe Term
liftI16I Int16# -> Int# -> Int16#
f [Value]
args = case [Value]
args of
  [Lit (Int16Literal Integer
i),Lit (IntLiteral Integer
j)] ->
    let !(I16# Int16#
a) = Integer -> Int16
forall a. Num a => Integer -> a
fromInteger Integer
i
        !(I# Int#
b) = Integer -> Int
forall a. Num a => Integer -> a
fromInteger Integer
j
     in Term -> Maybe Term
forall a. a -> Maybe a
Just (Literal -> Term
Literal (Integer -> Literal
Int16Literal (Int16 -> Integer
forall a. Integral a => a -> Integer
toInteger (Int16# -> Int16
I16# (Int16# -> Int# -> Int16#
f Int16#
a Int#
b)))))
  [Value]
_ -> Maybe Term
forall a. Maybe a
Nothing

liftI16RI :: (Int16# -> Int16# -> Int#) -> [Value] -> Maybe Term
liftI16RI :: (Int16# -> Int16# -> Int#) -> [Value] -> Maybe Term
liftI16RI Int16# -> Int16# -> Int#
f [Value]
args = case [Value] -> [Integer]
int16Literals' [Value]
args of
  [Integer
i,Integer
j] ->
    let !(I16# Int16#
a) = Integer -> Int16
forall a. Num a => Integer -> a
fromInteger Integer
i
        !(I16# Int16#
b) = Integer -> Int16
forall a. Num a => Integer -> a
fromInteger Integer
j
     in Term -> Maybe Term
forall a. a -> Maybe a
Just (Literal -> Term
Literal (Integer -> Literal
IntLiteral (Int -> Integer
forall a. Integral a => a -> Integer
toInteger (Int# -> Int
I# (Int16# -> Int16# -> Int#
f Int16#
a Int16#
b)))))
  [Integer]
_ -> Maybe Term
forall a. Maybe a
Nothing

liftI32 :: (Int32# -> Int32# -> Int32#) -> [Value] -> Maybe Term
liftI32 :: (Int32# -> Int32# -> Int32#) -> [Value] -> Maybe Term
liftI32 Int32# -> Int32# -> Int32#
f [Value]
args = case [Value] -> [Integer]
int32Literals' [Value]
args of
  [Integer
i,Integer
j] ->
    let !(I32# Int32#
a) = Integer -> Int32
forall a. Num a => Integer -> a
fromInteger Integer
i
        !(I32# Int32#
b) = Integer -> Int32
forall a. Num a => Integer -> a
fromInteger Integer
j
     in Term -> Maybe Term
forall a. a -> Maybe a
Just (Literal -> Term
Literal (Integer -> Literal
Int32Literal (Int32 -> Integer
forall a. Integral a => a -> Integer
toInteger (Int32# -> Int32
I32# (Int32# -> Int32# -> Int32#
f Int32#
a Int32#
b)))))
  [Integer]
_ -> Maybe Term
forall a. Maybe a
Nothing

liftI32I :: (Int32# -> Int# -> Int32#) -> [Value] -> Maybe Term
liftI32I :: (Int32# -> Int# -> Int32#) -> [Value] -> Maybe Term
liftI32I Int32# -> Int# -> Int32#
f [Value]
args = case [Value]
args of
  [Lit (Int32Literal Integer
i),Lit (IntLiteral Integer
j)] ->
    let !(I32# Int32#
a) = Integer -> Int32
forall a. Num a => Integer -> a
fromInteger Integer
i
        !(I# Int#
b) = Integer -> Int
forall a. Num a => Integer -> a
fromInteger Integer
j
     in Term -> Maybe Term
forall a. a -> Maybe a
Just (Literal -> Term
Literal (Integer -> Literal
Int32Literal (Int32 -> Integer
forall a. Integral a => a -> Integer
toInteger (Int32# -> Int32
I32# (Int32# -> Int# -> Int32#
f Int32#
a Int#
b)))))
  [Value]
_ -> Maybe Term
forall a. Maybe a
Nothing

liftI32RI :: (Int32# -> Int32# -> Int#) -> [Value] -> Maybe Term
liftI32RI :: (Int32# -> Int32# -> Int#) -> [Value] -> Maybe Term
liftI32RI Int32# -> Int32# -> Int#
f [Value]
args = case [Value] -> [Integer]
int32Literals' [Value]
args of
  [Integer
i,Integer
j] ->
    let !(I32# Int32#
a) = Integer -> Int32
forall a. Num a => Integer -> a
fromInteger Integer
i
        !(I32# Int32#
b) = Integer -> Int32
forall a. Num a => Integer -> a
fromInteger Integer
j
     in Term -> Maybe Term
forall a. a -> Maybe a
Just (Literal -> Term
Literal (Integer -> Literal
IntLiteral (Int -> Integer
forall a. Integral a => a -> Integer
toInteger (Int# -> Int
I# (Int32# -> Int32# -> Int#
f Int32#
a Int32#
b)))))
  [Integer]
_ -> Maybe Term
forall a. Maybe a
Nothing

liftI64 :: (Int64# -> Int64# -> Int64#) -> [Value] -> Maybe Term
liftI64 :: (Int64# -> Int64# -> Int64#) -> [Value] -> Maybe Term
liftI64 Int64# -> Int64# -> Int64#
f [Value]
args = case [Value] -> [Integer]
int64Literals' [Value]
args of
  [Integer
i,Integer
j] ->
    let !(I64# Int64#
a) = Integer -> Int64
forall a. Num a => Integer -> a
fromInteger Integer
i
        !(I64# Int64#
b) = Integer -> Int64
forall a. Num a => Integer -> a
fromInteger Integer
j
     in Term -> Maybe Term
forall a. a -> Maybe a
Just (Literal -> Term
Literal (Integer -> Literal
Int64Literal (Int64 -> Integer
forall a. Integral a => a -> Integer
toInteger (Int64# -> Int64
I64# (Int64# -> Int64# -> Int64#
f Int64#
a Int64#
b)))))
  [Integer]
_ -> Maybe Term
forall a. Maybe a
Nothing

liftI64I :: (Int64# -> Int# -> Int64#) -> [Value] -> Maybe Term
liftI64I :: (Int64# -> Int# -> Int64#) -> [Value] -> Maybe Term
liftI64I Int64# -> Int# -> Int64#
f [Value]
args = case [Value]
args of
  [Lit (Int64Literal Integer
i),Lit (IntLiteral Integer
j)] ->
    let !(I64# Int64#
a) = Integer -> Int64
forall a. Num a => Integer -> a
fromInteger Integer
i
        !(I# Int#
b) = Integer -> Int
forall a. Num a => Integer -> a
fromInteger Integer
j
     in Term -> Maybe Term
forall a. a -> Maybe a
Just (Literal -> Term
Literal (Integer -> Literal
Int64Literal (Int64 -> Integer
forall a. Integral a => a -> Integer
toInteger (Int64# -> Int64
I64# (Int64# -> Int# -> Int64#
f Int64#
a Int#
b)))))
  [Value]
_ -> Maybe Term
forall a. Maybe a
Nothing

liftI64RI :: (Int64# -> Int64# -> Int#) -> [Value] -> Maybe Term
liftI64RI :: (Int64# -> Int64# -> Int#) -> [Value] -> Maybe Term
liftI64RI Int64# -> Int64# -> Int#
f [Value]
args = case [Value] -> [Integer]
int64Literals' [Value]
args of
  [Integer
i,Integer
j] ->
    let !(I64# Int64#
a) = Integer -> Int64
forall a. Num a => Integer -> a
fromInteger Integer
i
        !(I64# Int64#
b) = Integer -> Int64
forall a. Num a => Integer -> a
fromInteger Integer
j
     in Term -> Maybe Term
forall a. a -> Maybe a
Just (Literal -> Term
Literal (Integer -> Literal
IntLiteral (Int -> Integer
forall a. Integral a => a -> Integer
toInteger (Int# -> Int
I# (Int64# -> Int64# -> Int#
f Int64#
a Int64#
b)))))
  [Integer]
_ -> Maybe Term
forall a. Maybe a
Nothing

liftW8 :: (Word8# -> Word8# -> Word8#) -> [Value] -> Maybe Term
liftW8 :: (Word8# -> Word8# -> Word8#) -> [Value] -> Maybe Term
liftW8 Word8# -> Word8# -> Word8#
f [Value]
args = case [Value] -> [Integer]
word8Literals' [Value]
args of
  [Integer
i,Integer
j] ->
    let !(W8# Word8#
a) = Integer -> Word8
forall a. Num a => Integer -> a
fromInteger Integer
i
        !(W8# Word8#
b) = Integer -> Word8
forall a. Num a => Integer -> a
fromInteger Integer
j
     in Term -> Maybe Term
forall a. a -> Maybe a
Just (Literal -> Term
Literal (Integer -> Literal
Word8Literal (Word8 -> Integer
forall a. Integral a => a -> Integer
toInteger (Word8# -> Word8
W8# (Word8# -> Word8# -> Word8#
f Word8#
a Word8#
b)))))
  [Integer]
_ -> Maybe Term
forall a. Maybe a
Nothing

liftW8I :: (Word8# -> Int# -> Word8#) -> [Value] -> Maybe Term
liftW8I :: (Word8# -> Int# -> Word8#) -> [Value] -> Maybe Term
liftW8I Word8# -> Int# -> Word8#
f [Value]
args = case [Value]
args of
  [Lit (Word8Literal Integer
i),Lit (IntLiteral Integer
j)] ->
    let !(W8# Word8#
a) = Integer -> Word8
forall a. Num a => Integer -> a
fromInteger Integer
i
        !(I# Int#
b) = Integer -> Int
forall a. Num a => Integer -> a
fromInteger Integer
j
     in Term -> Maybe Term
forall a. a -> Maybe a
Just (Literal -> Term
Literal (Integer -> Literal
Word8Literal (Word8 -> Integer
forall a. Integral a => a -> Integer
toInteger (Word8# -> Word8
W8# (Word8# -> Int# -> Word8#
f Word8#
a Int#
b)))))
  [Value]
_ -> Maybe Term
forall a. Maybe a
Nothing

liftW8RI :: (Word8# -> Word8# -> Int#) -> [Value] -> Maybe Term
liftW8RI :: (Word8# -> Word8# -> Int#) -> [Value] -> Maybe Term
liftW8RI Word8# -> Word8# -> Int#
f [Value]
args = case [Value] -> [Integer]
word8Literals' [Value]
args of
  [Integer
i,Integer
j] ->
    let !(W8# Word8#
a) = Integer -> Word8
forall a. Num a => Integer -> a
fromInteger Integer
i
        !(W8# Word8#
b) = Integer -> Word8
forall a. Num a => Integer -> a
fromInteger Integer
j
     in Term -> Maybe Term
forall a. a -> Maybe a
Just (Literal -> Term
Literal (Integer -> Literal
IntLiteral (Int -> Integer
forall a. Integral a => a -> Integer
toInteger (Int# -> Int
I# (Word8# -> Word8# -> Int#
f Word8#
a Word8#
b)))))
  [Integer]
_ -> Maybe Term
forall a. Maybe a
Nothing

liftW16 :: (Word16# -> Word16# -> Word16#) -> [Value] -> Maybe Term
liftW16 :: (Word16# -> Word16# -> Word16#) -> [Value] -> Maybe Term
liftW16 Word16# -> Word16# -> Word16#
f [Value]
args = case [Value] -> [Integer]
word16Literals' [Value]
args of
  [Integer
i,Integer
j] -> let !(W16# Word16#
a) = Integer -> Word16
forall a. Num a => Integer -> a
fromInteger Integer
i
               !(W16# Word16#
b) = Integer -> Word16
forall a. Num a => Integer -> a
fromInteger Integer
j
            in Term -> Maybe Term
forall a. a -> Maybe a
Just (Literal -> Term
Literal (Integer -> Literal
Word16Literal (Word16 -> Integer
forall a. Integral a => a -> Integer
toInteger (Word16# -> Word16
W16# (Word16# -> Word16# -> Word16#
f Word16#
a Word16#
b)))))
  [Integer]
_ -> Maybe Term
forall a. Maybe a
Nothing

liftW16I :: (Word16# -> Int# -> Word16#) -> [Value] -> Maybe Term
liftW16I :: (Word16# -> Int# -> Word16#) -> [Value] -> Maybe Term
liftW16I Word16# -> Int# -> Word16#
f [Value]
args = case [Value]
args of
  [Lit (Word16Literal Integer
i),Lit (IntLiteral Integer
j)] ->
    let !(W16# Word16#
a) = Integer -> Word16
forall a. Num a => Integer -> a
fromInteger Integer
i
        !(I# Int#
b) = Integer -> Int
forall a. Num a => Integer -> a
fromInteger Integer
j
     in Term -> Maybe Term
forall a. a -> Maybe a
Just (Literal -> Term
Literal (Integer -> Literal
Word16Literal (Word16 -> Integer
forall a. Integral a => a -> Integer
toInteger (Word16# -> Word16
W16# (Word16# -> Int# -> Word16#
f Word16#
a Int#
b)))))
  [Value]
_ -> Maybe Term
forall a. Maybe a
Nothing

liftW16RI :: (Word16# -> Word16# -> Int#) -> [Value] -> Maybe Term
liftW16RI :: (Word16# -> Word16# -> Int#) -> [Value] -> Maybe Term
liftW16RI Word16# -> Word16# -> Int#
f [Value]
args = case [Value] -> [Integer]
word16Literals' [Value]
args of
  [Integer
i,Integer
j] ->
    let !(W16# Word16#
a) = Integer -> Word16
forall a. Num a => Integer -> a
fromInteger Integer
i
        !(W16# Word16#
b) = Integer -> Word16
forall a. Num a => Integer -> a
fromInteger Integer
j
     in Term -> Maybe Term
forall a. a -> Maybe a
Just (Literal -> Term
Literal (Integer -> Literal
IntLiteral (Int -> Integer
forall a. Integral a => a -> Integer
toInteger (Int# -> Int
I# (Word16# -> Word16# -> Int#
f Word16#
a Word16#
b)))))
  [Integer]
_ -> Maybe Term
forall a. Maybe a
Nothing

liftW32 :: (Word32# -> Word32# -> Word32#) -> [Value] -> Maybe Term
liftW32 :: (Word32# -> Word32# -> Word32#) -> [Value] -> Maybe Term
liftW32 Word32# -> Word32# -> Word32#
f [Value]
args = case [Value] -> [Integer]
word32Literals' [Value]
args of
  [Integer
i,Integer
j] -> let !(W32# Word32#
a) = Integer -> Word32
forall a. Num a => Integer -> a
fromInteger Integer
i
               !(W32# Word32#
b) = Integer -> Word32
forall a. Num a => Integer -> a
fromInteger Integer
j
            in Term -> Maybe Term
forall a. a -> Maybe a
Just (Literal -> Term
Literal (Integer -> Literal
Word32Literal (Word32 -> Integer
forall a. Integral a => a -> Integer
toInteger (Word32# -> Word32
W32# (Word32# -> Word32# -> Word32#
f Word32#
a Word32#
b)))))
  [Integer]
_ -> Maybe Term
forall a. Maybe a
Nothing

liftW32I :: (Word32# -> Int# -> Word32#) -> [Value] -> Maybe Term
liftW32I :: (Word32# -> Int# -> Word32#) -> [Value] -> Maybe Term
liftW32I Word32# -> Int# -> Word32#
f [Value]
args = case [Value]
args of
  [Lit (Word32Literal Integer
i),Lit (IntLiteral Integer
j)] ->
    let !(W32# Word32#
a) = Integer -> Word32
forall a. Num a => Integer -> a
fromInteger Integer
i
        !(I# Int#
b) = Integer -> Int
forall a. Num a => Integer -> a
fromInteger Integer
j
     in Term -> Maybe Term
forall a. a -> Maybe a
Just (Literal -> Term
Literal (Integer -> Literal
Word32Literal (Word32 -> Integer
forall a. Integral a => a -> Integer
toInteger (Word32# -> Word32
W32# (Word32# -> Int# -> Word32#
f Word32#
a Int#
b)))))
  [Value]
_ -> Maybe Term
forall a. Maybe a
Nothing

liftW32RI :: (Word32# -> Word32# -> Int#) -> [Value] -> Maybe Term
liftW32RI :: (Word32# -> Word32# -> Int#) -> [Value] -> Maybe Term
liftW32RI Word32# -> Word32# -> Int#
f [Value]
args = case [Value] -> [Integer]
word32Literals' [Value]
args of
  [Integer
i,Integer
j] ->
    let !(W32# Word32#
a) = Integer -> Word32
forall a. Num a => Integer -> a
fromInteger Integer
i
        !(W32# Word32#
b) = Integer -> Word32
forall a. Num a => Integer -> a
fromInteger Integer
j
     in Term -> Maybe Term
forall a. a -> Maybe a
Just (Literal -> Term
Literal (Integer -> Literal
IntLiteral (Int -> Integer
forall a. Integral a => a -> Integer
toInteger (Int# -> Int
I# (Word32# -> Word32# -> Int#
f Word32#
a Word32#
b)))))
  [Integer]
_ -> Maybe Term
forall a. Maybe a
Nothing

liftW64 :: (Word64# -> Word64# -> Word64#) -> [Value] -> Maybe Term
liftW64 :: (Word64# -> Word64# -> Word64#) -> [Value] -> Maybe Term
liftW64 Word64# -> Word64# -> Word64#
f [Value]
args = case [Value] -> [Integer]
word64Literals' [Value]
args of
  [Integer
i,Integer
j] -> let !(W64# Word64#
a) = Integer -> Unique
forall a. Num a => Integer -> a
fromInteger Integer
i
               !(W64# Word64#
b) = Integer -> Unique
forall a. Num a => Integer -> a
fromInteger Integer
j
            in Term -> Maybe Term
forall a. a -> Maybe a
Just (Literal -> Term
Literal (Integer -> Literal
Word64Literal (Unique -> Integer
forall a. Integral a => a -> Integer
toInteger (Word64# -> Unique
W64# (Word64# -> Word64# -> Word64#
f Word64#
a Word64#
b)))))
  [Integer]
_ -> Maybe Term
forall a. Maybe a
Nothing

liftW64I :: (Word64# -> Int# -> Word64#) -> [Value] -> Maybe Term
liftW64I :: (Word64# -> Int# -> Word64#) -> [Value] -> Maybe Term
liftW64I Word64# -> Int# -> Word64#
f [Value]
args = case [Value]
args of
  [Lit (Word64Literal Integer
i),Lit (IntLiteral Integer
j)] ->
    let !(W64# Word64#
a) = Integer -> Unique
forall a. Num a => Integer -> a
fromInteger Integer
i
        !(I# Int#
b) = Integer -> Int
forall a. Num a => Integer -> a
fromInteger Integer
j
     in Term -> Maybe Term
forall a. a -> Maybe a
Just (Literal -> Term
Literal (Integer -> Literal
Word64Literal (Unique -> Integer
forall a. Integral a => a -> Integer
toInteger (Word64# -> Unique
W64# (Word64# -> Int# -> Word64#
f Word64#
a Int#
b)))))
  [Value]
_ -> Maybe Term
forall a. Maybe a
Nothing

liftW64RI :: (Word64# -> Word64# -> Int#) -> [Value] -> Maybe Term
liftW64RI :: (Word64# -> Word64# -> Int#) -> [Value] -> Maybe Term
liftW64RI Word64# -> Word64# -> Int#
f [Value]
args = case [Value] -> [Integer]
word64Literals' [Value]
args of
  [Integer
i,Integer
j] ->
    let !(W64# Word64#
a) = Integer -> Unique
forall a. Num a => Integer -> a
fromInteger Integer
i
        !(W64# Word64#
b) = Integer -> Unique
forall a. Num a => Integer -> a
fromInteger Integer
j
     in Term -> Maybe Term
forall a. a -> Maybe a
Just (Literal -> Term
Literal (Integer -> Literal
IntLiteral (Int -> Integer
forall a. Integral a => a -> Integer
toInteger (Int# -> Int
I# (Word64# -> Word64# -> Int#
f Word64#
a Word64#
b)))))
  [Integer]
_ -> Maybe Term
forall a. Maybe a
Nothing

splitAtPrim
  :: TyConName
  -- ^ SNat TyCon name
  -> TyConName
  -- ^ Vec TyCon name
  -> Term
splitAtPrim :: TyConName -> TyConName -> Term
splitAtPrim TyConName
snatTcNm TyConName
vecTcNm =
  PrimInfo -> Term
Prim (Text
-> Type -> WorkInfo -> IsMultiPrim -> PrimUnfolding -> PrimInfo
PrimInfo (Name -> Text
forall a. Show a => a -> Text
showt 'Clash.Sized.Vector.splitAt) (TyConName -> TyConName -> Type
splitAtTy TyConName
snatTcNm TyConName
vecTcNm) WorkInfo
WorkNever IsMultiPrim
SingleResult PrimUnfolding
NoUnfolding)

splitAtTy
  :: TyConName
  -- ^ SNat TyCon name
  -> TyConName
  -- ^ Vec TyCon name
  -> Type
splitAtTy :: TyConName -> TyConName -> Type
splitAtTy TyConName
snatNm TyConName
vecNm =
  TyVar -> Type -> Type
ForAllTy TyVar
mTV (
  TyVar -> Type -> Type
ForAllTy TyVar
nTV (
  TyVar -> Type -> Type
ForAllTy TyVar
aTV (
  Type -> Type -> Type
mkFunTy
    (TyConName -> [Type] -> Type
mkTyConApp TyConName
snatNm [TyVar -> Type
VarTy TyVar
mTV])
    (Type -> Type -> Type
mkFunTy
      (TyConName -> [Type] -> Type
mkTyConApp TyConName
vecNm
                  [TyConName -> [Type] -> Type
mkTyConApp TyConName
typeNatAdd
                    [TyVar -> Type
VarTy TyVar
mTV
                    ,TyVar -> Type
VarTy TyVar
nTV]
                  ,TyVar -> Type
VarTy TyVar
aTV])
      (TyConName -> [Type] -> Type
mkTyConApp TyConName
tupNm
                  [TyConName -> [Type] -> Type
mkTyConApp TyConName
vecNm
                              [TyVar -> Type
VarTy TyVar
mTV
                              ,TyVar -> Type
VarTy TyVar
aTV]
                  ,TyConName -> [Type] -> Type
mkTyConApp TyConName
vecNm
                              [TyVar -> Type
VarTy TyVar
nTV
                              ,TyVar -> Type
VarTy TyVar
aTV]])))))
  where
    mTV :: TyVar
mTV   = Type -> TyName -> TyVar
mkTyVar Type
typeNatKind (Text -> Unique -> TyName
forall a. Text -> Unique -> Name a
mkUnsafeSystemName Text
"m" Unique
0)
    nTV :: TyVar
nTV   = Type -> TyName -> TyVar
mkTyVar Type
typeNatKind (Text -> Unique -> TyName
forall a. Text -> Unique -> Name a
mkUnsafeSystemName Text
"n" Unique
1)
    aTV :: TyVar
aTV   = Type -> TyName -> TyVar
mkTyVar Type
liftedTypeKind (Text -> Unique -> TyName
forall a. Text -> Unique -> Name a
mkUnsafeSystemName Text
"a" Unique
2)
    tupNm :: TyConName
tupNm = TyCon -> TyConName
ghcTyconToTyConName (Boxity -> Int -> TyCon
tupleTyCon Boxity
Boxed Int
2)

foldSplitAtTy
  :: TyConName
  -- ^ Vec TyCon name
  -> Type
foldSplitAtTy :: TyConName -> Type
foldSplitAtTy TyConName
vecNm =
  TyVar -> Type -> Type
ForAllTy TyVar
mTV (
  TyVar -> Type -> Type
ForAllTy TyVar
nTV (
  TyVar -> Type -> Type
ForAllTy TyVar
aTV (
  Type -> Type -> Type
mkFunTy
    Type
naturalPrimTy
    (Type -> Type -> Type
mkFunTy
      (TyConName -> [Type] -> Type
mkTyConApp TyConName
vecNm
                  [TyConName -> [Type] -> Type
mkTyConApp TyConName
typeNatAdd
                    [TyVar -> Type
VarTy TyVar
mTV
                    ,TyVar -> Type
VarTy TyVar
nTV]
                  ,TyVar -> Type
VarTy TyVar
aTV])
      (TyConName -> [Type] -> Type
mkTyConApp TyConName
tupNm
                  [TyConName -> [Type] -> Type
mkTyConApp TyConName
vecNm
                              [TyVar -> Type
VarTy TyVar
mTV
                              ,TyVar -> Type
VarTy TyVar
aTV]
                  ,TyConName -> [Type] -> Type
mkTyConApp TyConName
vecNm
                              [TyVar -> Type
VarTy TyVar
nTV
                              ,TyVar -> Type
VarTy TyVar
aTV]])))))
  where
    mTV :: TyVar
mTV   = Type -> TyName -> TyVar
mkTyVar Type
typeNatKind (Text -> Unique -> TyName
forall a. Text -> Unique -> Name a
mkUnsafeSystemName Text
"m" Unique
0)
    nTV :: TyVar
nTV   = Type -> TyName -> TyVar
mkTyVar Type
typeNatKind (Text -> Unique -> TyName
forall a. Text -> Unique -> Name a
mkUnsafeSystemName Text
"n" Unique
1)
    aTV :: TyVar
aTV   = Type -> TyName -> TyVar
mkTyVar Type
liftedTypeKind (Text -> Unique -> TyName
forall a. Text -> Unique -> Name a
mkUnsafeSystemName Text
"a" Unique
2)
    tupNm :: TyConName
tupNm = TyCon -> TyConName
ghcTyconToTyConName (Boxity -> Int -> TyCon
tupleTyCon Boxity
Boxed Int
2)

vecAppendPrim
  :: TyConName
  -- ^ Vec TyCon name
  -> Term
vecAppendPrim :: TyConName -> Term
vecAppendPrim TyConName
vecNm =
  PrimInfo -> Term
Prim (Text
-> Type -> WorkInfo -> IsMultiPrim -> PrimUnfolding -> PrimInfo
PrimInfo (Name -> Text
forall a. Show a => a -> Text
showt '(Clash.Sized.Vector.++)) (TyConName -> Type
vecAppendTy TyConName
vecNm) WorkInfo
WorkNever IsMultiPrim
SingleResult PrimUnfolding
NoUnfolding)

vecAppendTy
  :: TyConName
  -- ^ Vec TyCon name
  -> Type
vecAppendTy :: TyConName -> Type
vecAppendTy TyConName
vecNm =
    TyVar -> Type -> Type
ForAllTy TyVar
nTV (
    TyVar -> Type -> Type
ForAllTy TyVar
aTV (
    TyVar -> Type -> Type
ForAllTy TyVar
mTV (
    Type -> Type -> Type
mkFunTy
      (TyConName -> [Type] -> Type
mkTyConApp TyConName
vecNm [TyVar -> Type
VarTy TyVar
nTV
                        ,TyVar -> Type
VarTy TyVar
aTV
                        ])
      (Type -> Type -> Type
mkFunTy
         (TyConName -> [Type] -> Type
mkTyConApp TyConName
vecNm [TyVar -> Type
VarTy TyVar
mTV
                           ,TyVar -> Type
VarTy TyVar
aTV
                           ])
         (TyConName -> [Type] -> Type
mkTyConApp TyConName
vecNm [TyConName -> [Type] -> Type
mkTyConApp TyConName
typeNatAdd
                              [TyVar -> Type
VarTy TyVar
nTV
                              ,TyVar -> Type
VarTy TyVar
mTV]
                           ,TyVar -> Type
VarTy TyVar
aTV
                           ])))))
  where
    nTV :: TyVar
nTV = Type -> TyName -> TyVar
mkTyVar Type
typeNatKind (Text -> Unique -> TyName
forall a. Text -> Unique -> Name a
mkUnsafeSystemName Text
"n" Unique
0)
    aTV :: TyVar
aTV = Type -> TyName -> TyVar
mkTyVar Type
liftedTypeKind (Text -> Unique -> TyName
forall a. Text -> Unique -> Name a
mkUnsafeSystemName Text
"a" Unique
1)
    mTV :: TyVar
mTV = Type -> TyName -> TyVar
mkTyVar Type
typeNatKind (Text -> Unique -> TyName
forall a. Text -> Unique -> Name a
mkUnsafeSystemName Text
"m" Unique
2)

vecZipWithPrim
  :: TyConName
  -- ^ Vec TyCon name
  -> Term
vecZipWithPrim :: TyConName -> Term
vecZipWithPrim TyConName
vecNm =
  PrimInfo -> Term
Prim (Text
-> Type -> WorkInfo -> IsMultiPrim -> PrimUnfolding -> PrimInfo
PrimInfo (Name -> Text
forall a. Show a => a -> Text
showt 'Clash.Sized.Vector.zipWith) (TyConName -> Type
vecZipWithTy TyConName
vecNm) WorkInfo
WorkNever IsMultiPrim
SingleResult PrimUnfolding
NoUnfolding)

vecZipWithTy
  :: TyConName
  -- ^ Vec TyCon name
  -> Type
vecZipWithTy :: TyConName -> Type
vecZipWithTy TyConName
vecNm =
  TyVar -> Type -> Type
ForAllTy TyVar
aTV (
  TyVar -> Type -> Type
ForAllTy TyVar
bTV (
  TyVar -> Type -> Type
ForAllTy TyVar
cTV (
  TyVar -> Type -> Type
ForAllTy TyVar
nTV (
  Type -> Type -> Type
mkFunTy
    (Type -> Type -> Type
mkFunTy Type
aTy (Type -> Type -> Type
mkFunTy Type
bTy Type
cTy))
    (Type -> Type -> Type
mkFunTy
      (TyConName -> [Type] -> Type
mkTyConApp TyConName
vecNm [Type
nTy,Type
aTy])
      (Type -> Type -> Type
mkFunTy
        (TyConName -> [Type] -> Type
mkTyConApp TyConName
vecNm [Type
nTy,Type
bTy])
        (TyConName -> [Type] -> Type
mkTyConApp TyConName
vecNm [Type
nTy,Type
cTy])))))))
  where
    aTV :: TyVar
aTV = Type -> TyName -> TyVar
mkTyVar Type
liftedTypeKind (Text -> Unique -> TyName
forall a. Text -> Unique -> Name a
mkUnsafeSystemName Text
"a" Unique
0)
    bTV :: TyVar
bTV = Type -> TyName -> TyVar
mkTyVar Type
liftedTypeKind (Text -> Unique -> TyName
forall a. Text -> Unique -> Name a
mkUnsafeSystemName Text
"b" Unique
1)
    cTV :: TyVar
cTV = Type -> TyName -> TyVar
mkTyVar Type
liftedTypeKind (Text -> Unique -> TyName
forall a. Text -> Unique -> Name a
mkUnsafeSystemName Text
"c" Unique
2)
    nTV :: TyVar
nTV = Type -> TyName -> TyVar
mkTyVar Type
typeNatKind (Text -> Unique -> TyName
forall a. Text -> Unique -> Name a
mkUnsafeSystemName Text
"n" Unique
3)
    aTy :: Type
aTy = TyVar -> Type
VarTy TyVar
aTV
    bTy :: Type
bTy = TyVar -> Type
VarTy TyVar
bTV
    cTy :: Type
cTy = TyVar -> Type
VarTy TyVar
cTV
    nTy :: Type
nTy = TyVar -> Type
VarTy TyVar
nTV

vecImapGoTy
  :: TyConName
  -- ^ Vec TyCon name
  -> TyConName
  -- ^ Index TyCon name
  -> Type
vecImapGoTy :: TyConName -> TyConName -> Type
vecImapGoTy TyConName
vecTcNm TyConName
indexTcNm =
  TyVar -> Type -> Type
ForAllTy TyVar
nTV (
  TyVar -> Type -> Type
ForAllTy TyVar
mTV (
  TyVar -> Type -> Type
ForAllTy TyVar
aTV (
  TyVar -> Type -> Type
ForAllTy TyVar
bTV (
  Type -> Type -> Type
mkFunTy Type
fTy
       (Type -> Type -> Type
mkFunTy Type
vecATy (Type -> Type -> Type
mkFunTy Type
indexTy Type
vecBTy))))))
  where
    nTV :: TyVar
nTV = Type -> TyName -> TyVar
mkTyVar Type
typeNatKind (Text -> Unique -> TyName
forall a. Text -> Unique -> Name a
mkUnsafeSystemName Text
"n" Unique
0)
    mTV :: TyVar
mTV = Type -> TyName -> TyVar
mkTyVar Type
typeNatKind (Text -> Unique -> TyName
forall a. Text -> Unique -> Name a
mkUnsafeSystemName Text
"m" Unique
1)
    aTV :: TyVar
aTV = Type -> TyName -> TyVar
mkTyVar Type
liftedTypeKind (Text -> Unique -> TyName
forall a. Text -> Unique -> Name a
mkUnsafeSystemName Text
"a" Unique
2)
    bTV :: TyVar
bTV = Type -> TyName -> TyVar
mkTyVar Type
liftedTypeKind (Text -> Unique -> TyName
forall a. Text -> Unique -> Name a
mkUnsafeSystemName Text
"b" Unique
3)
    indexTy :: Type
indexTy = TyConName -> [Type] -> Type
mkTyConApp TyConName
indexTcNm [Type
nTy]
    nTy :: Type
nTy = TyVar -> Type
VarTy TyVar
nTV
    mTy :: Type
mTy = TyVar -> Type
VarTy TyVar
mTV
    fTy :: Type
fTy = Type -> Type -> Type
mkFunTy Type
indexTy (Type -> Type -> Type
mkFunTy Type
aTy Type
bTy)
    aTy :: Type
aTy = TyVar -> Type
VarTy TyVar
aTV
    bTy :: Type
bTy = TyVar -> Type
VarTy TyVar
bTV
    vecATy :: Type
vecATy = TyConName -> [Type] -> Type
mkTyConApp TyConName
vecTcNm [Type
mTy,Type
aTy]
    vecBTy :: Type
vecBTy = TyConName -> [Type] -> Type
mkTyConApp TyConName
vecTcNm [Type
mTy,Type
bTy]

indexAddTy
  :: TyConName
  -- ^ Index TyCon name
  -> Type
indexAddTy :: TyConName -> Type
indexAddTy TyConName
indexTcNm =
  TyVar -> Type -> Type
ForAllTy TyVar
nTV (
  Type -> Type -> Type
mkFunTy Type
naturalPrimTy (Type -> Type -> Type
mkFunTy Type
indexTy (Type -> Type -> Type
mkFunTy Type
indexTy Type
indexTy)))
  where
    nTV :: TyVar
nTV     = Type -> TyName -> TyVar
mkTyVar Type
typeNatKind (Text -> Unique -> TyName
forall a. Text -> Unique -> Name a
mkUnsafeSystemName Text
"n" Unique
0)
    indexTy :: Type
indexTy = TyConName -> [Type] -> Type
mkTyConApp TyConName
indexTcNm [TyVar -> Type
VarTy TyVar
nTV]

bvAppendPrim
  :: TyConName
  -- ^ BitVector TyCon Name
  -> Term
bvAppendPrim :: TyConName -> Term
bvAppendPrim TyConName
bvTcNm =
  PrimInfo -> Term
Prim (Text
-> Type -> WorkInfo -> IsMultiPrim -> PrimUnfolding -> PrimInfo
PrimInfo (Name -> Text
forall a. Show a => a -> Text
showt '(Clash.Sized.Internal.BitVector.++#)) (TyConName -> Type
bvAppendTy TyConName
bvTcNm) WorkInfo
WorkNever IsMultiPrim
SingleResult PrimUnfolding
NoUnfolding)

bvAppendTy
  :: TyConName
  -- ^ BitVector TyCon Name
  -> Type
bvAppendTy :: TyConName -> Type
bvAppendTy TyConName
bvNm =
  TyVar -> Type -> Type
ForAllTy TyVar
mTV (
  TyVar -> Type -> Type
ForAllTy TyVar
nTV (
  Type -> Type -> Type
mkFunTy Type
naturalPrimTy (Type -> Type -> Type
mkFunTy
    (TyConName -> [Type] -> Type
mkTyConApp TyConName
bvNm [TyVar -> Type
VarTy TyVar
nTV])
    (Type -> Type -> Type
mkFunTy
      (TyConName -> [Type] -> Type
mkTyConApp TyConName
bvNm [TyVar -> Type
VarTy TyVar
mTV])
      (TyConName -> [Type] -> Type
mkTyConApp TyConName
bvNm [TyConName -> [Type] -> Type
mkTyConApp TyConName
typeNatAdd
                          [TyVar -> Type
VarTy TyVar
nTV
                          ,TyVar -> Type
VarTy TyVar
mTV]])))))
  where
    mTV :: TyVar
mTV = Type -> TyName -> TyVar
mkTyVar Type
typeNatKind (Text -> Unique -> TyName
forall a. Text -> Unique -> Name a
mkUnsafeSystemName Text
"m" Unique
0)
    nTV :: TyVar
nTV = Type -> TyName -> TyVar
mkTyVar Type
typeNatKind (Text -> Unique -> TyName
forall a. Text -> Unique -> Name a
mkUnsafeSystemName Text
"n" Unique
1)

bvSplitPrim
  :: TyConName
  -- ^ BitVector TyCon Name
  -> Term
bvSplitPrim :: TyConName -> Term
bvSplitPrim TyConName
bvTcNm =
  PrimInfo -> Term
Prim (Text
-> Type -> WorkInfo -> IsMultiPrim -> PrimUnfolding -> PrimInfo
PrimInfo (Name -> Text
forall a. Show a => a -> Text
showt 'Clash.Sized.Internal.BitVector.split#) (TyConName -> Type
bvSplitTy TyConName
bvTcNm) WorkInfo
WorkNever IsMultiPrim
SingleResult PrimUnfolding
NoUnfolding)

bvSplitTy
  :: TyConName
  -- ^ BitVector TyCon Name
  -> Type
bvSplitTy :: TyConName -> Type
bvSplitTy TyConName
bvNm =
  TyVar -> Type -> Type
ForAllTy TyVar
nTV (
  TyVar -> Type -> Type
ForAllTy TyVar
mTV (
  Type -> Type -> Type
mkFunTy Type
naturalPrimTy (Type -> Type -> Type
mkFunTy
    (TyConName -> [Type] -> Type
mkTyConApp TyConName
bvNm [TyConName -> [Type] -> Type
mkTyConApp TyConName
typeNatAdd
                                 [TyVar -> Type
VarTy TyVar
mTV
                                 ,TyVar -> Type
VarTy TyVar
nTV]])
    (TyConName -> [Type] -> Type
mkTyConApp TyConName
tupNm [TyConName -> [Type] -> Type
mkTyConApp TyConName
bvNm [TyVar -> Type
VarTy TyVar
mTV]
                      ,TyConName -> [Type] -> Type
mkTyConApp TyConName
bvNm [TyVar -> Type
VarTy TyVar
nTV]]))))
  where
    nTV :: TyVar
nTV   = Type -> TyName -> TyVar
mkTyVar Type
typeNatKind (Text -> Unique -> TyName
forall a. Text -> Unique -> Name a
mkUnsafeSystemName Text
"n" Unique
0)
    mTV :: TyVar
mTV   = Type -> TyName -> TyVar
mkTyVar Type
typeNatKind (Text -> Unique -> TyName
forall a. Text -> Unique -> Name a
mkUnsafeSystemName Text
"m" Unique
1)
    tupNm :: TyConName
tupNm = TyCon -> TyConName
ghcTyconToTyConName (Boxity -> Int -> TyCon
tupleTyCon Boxity
Boxed Int
2)

ghcTyconToTyConName
  :: TyCon.TyCon
  -> TyConName
ghcTyconToTyConName :: TyCon -> TyConName
ghcTyconToTyConName TyCon
tc =
    NameSort -> Text -> Unique -> SrcSpan -> TyConName
forall a. NameSort -> Text -> Unique -> SrcSpan -> Name a
Name NameSort
User Text
n' (Unique -> Unique
fromGhcUnique (TyCon -> Unique
TyCon.tyConUnique TyCon
tc)) (Name -> SrcSpan
forall a. NamedThing a => a -> SrcSpan
getSrcSpan Name
n)
  where
    n' :: Text
n'      = Text -> Maybe Text -> Text
forall a. a -> Maybe a -> a
fromMaybe Text
"_INTERNAL_" (Name -> Maybe Text
modNameM Name
n) Text -> Text -> Text
`Text.append`
              (Char
'.' Char -> Text -> Text
`Text.cons` [Char] -> Text
Text.pack [Char]
occName)
    occName :: [Char]
occName = OccName -> [Char]
occNameString (OccName -> [Char]) -> OccName -> [Char]
forall a b. (a -> b) -> a -> b
$ Name -> OccName
nameOccName Name
n
    n :: Name
n       = TyCon -> Name
TyCon.tyConName TyCon
tc

svoid :: (State# RealWorld -> State# RealWorld) -> IO ()
svoid :: (State# RealWorld -> State# RealWorld) -> IO ()
svoid State# RealWorld -> State# RealWorld
m0 = (State# RealWorld -> (# State# RealWorld, () #)) -> IO ()
forall a. (State# RealWorld -> (# State# RealWorld, a #)) -> IO a
IO (\State# RealWorld
s -> case State# RealWorld -> State# RealWorld
m0 State# RealWorld
s of State# RealWorld
s' -> (# State# RealWorld
s', () #))

isTrueDC,isFalseDC :: DataCon -> Bool
isTrueDC :: DataCon -> Bool
isTrueDC DataCon
dc  = DataCon -> Unique
dcUniq DataCon
dc Unique -> Unique -> Bool
forall a. Eq a => a -> a -> Bool
== Unique -> Unique
fromGhcUnique Unique
trueDataConKey
isFalseDC :: DataCon -> Bool
isFalseDC DataCon
dc = DataCon -> Unique
dcUniq DataCon
dc Unique -> Unique -> Bool
forall a. Eq a => a -> a -> Bool
== Unique -> Unique
fromGhcUnique Unique
falseDataConKey