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

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

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

module Clash.GHC.Evaluator.Primitives.Clash.Sized.Vector
  ( primitives
  ) where

import qualified Control.Lens               as Lens
import           Control.Monad.Trans.Except (runExcept)
import           Data.Bits
import qualified Data.Either         as Either
import qualified Data.List           as List
import           Data.Text           (Text)
import           Data.Text.Extra     (showt)

import           GHC.Types.Basic     (Boxity (..))
import           GHC.Builtin.Types   (tupleTyCon)

import           Clash.Core.Evaluator.Types
import           Clash.Core.FreeVars (typeFreeVars)
import Clash.Core.HasType (piResultTys)
import           Clash.Core.Literal  (Literal (..))
import Clash.Core.Name (mkUnsafeSystemName)
import           Clash.Core.Subst    (extendTvSubst, mkSubst, substTy)
import Clash.Core.Term
  (IsMultiPrim (..),
   Pat (..),
   PrimInfo (..),
   Term (..),
   WorkInfo (..),
   mkApps,
   PrimUnfolding(..))
import Clash.Core.Type
  (Type (..),
   LitTy (..),
   TypeView (..),
   mkFunTy,
   mkTyConApp,
   normalizeType,
   splitFunForallTy,
   tyView)
import Clash.Core.TyCon (tyConDataCons)
import Clash.Core.Util (mkVec, tyNatSize, dataConInstArgTys, primCo, mkSelectorCase)
import Clash.Core.Var (mkLocalId)
import qualified Clash.Data.UniqMap as UniqMap
import Clash.Util (curLoc, textNameLit)
import Clash.Normalize.PrimitiveReductions
  (typeNatMul,
   typeNatSub,
   vecLastPrim,
   vecInitPrim,
   vecHeadPrim,
   vecTailPrim,
   mkVecCons,
   mkVecNil)

import qualified Clash.Normalize.Primitives as NP

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

import qualified Clash.Sized.Internal.Index
import qualified Clash.Sized.Vector

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

primitives :: [(Text, PrimStep)]
primitives :: [(Text, PrimStep)]
primitives =
---------
-- Vector
---------
  [ Text -> (PrimStepContext -> Maybe Machine) -> (Text, PrimStep)
primStepEntry $(textNameLit 'Clash.Sized.Vector.length) ((PrimStepContext -> Maybe Machine) -> (Text, PrimStep))
-> (PrimStepContext -> Maybe Machine) -> (Text, PrimStep)
forall a b. (a -> b) -> a -> b
$ \case
      PrimStepContext{Bool
[Type]
[Value]
Type
TyConMap
Machine
PrimInfo
Term -> Maybe Machine
Term -> Term
Type
-> Integer -> Integer -> (Natural -> Natural -> Natural) -> Term
Type -> Integer -> (Natural -> Natural) -> Term
Type -> [Integer] -> ([Natural] -> Term) -> Term
Machine -> Term -> Maybe Machine
tcm :: TyConMap
isSubj :: Bool
pInfo :: PrimInfo
tys :: [Type]
args :: [Value]
mach :: Machine
ty :: Type
checkNaturalRange1 :: Type -> Integer -> (Natural -> Natural) -> Term
checkNaturalRange2 :: Type
-> Integer -> Integer -> (Natural -> Natural -> Natural) -> Term
checkNaturalRange :: Type -> [Integer] -> ([Natural] -> Term) -> Term
reduce :: Term -> Maybe Machine
reduceWith :: Machine -> Term -> Maybe Machine
reduceWHNF :: Term -> Maybe Machine
reduceWHNF' :: Machine -> Term -> Maybe Machine
catchDivByZero :: Term -> Term
catchErrorCall :: Term -> Term
tcm :: PrimStepContext -> TyConMap
isSubj :: PrimStepContext -> Bool
pInfo :: PrimStepContext -> PrimInfo
tys :: PrimStepContext -> [Type]
args :: PrimStepContext -> [Value]
mach :: PrimStepContext -> Machine
ty :: PrimStepContext -> Type
checkNaturalRange1 :: PrimStepContext -> Type -> Integer -> (Natural -> Natural) -> Term
checkNaturalRange2 :: PrimStepContext
-> Type
-> Integer
-> Integer
-> (Natural -> Natural -> Natural)
-> Term
checkNaturalRange :: PrimStepContext -> Type -> [Integer] -> ([Natural] -> Term) -> Term
reduce :: PrimStepContext -> Term -> Maybe Machine
reduceWith :: PrimStepContext -> Machine -> Term -> Maybe Machine
reduceWHNF :: PrimStepContext -> Term -> Maybe Machine
reduceWHNF' :: PrimStepContext -> Machine -> Term -> Maybe Machine
catchDivByZero :: PrimStepContext -> Term -> Term
catchErrorCall :: PrimStepContext -> Term -> Term
..} -- :: KnownNat n => Vec n a -> Int
        | Bool
isSubj
        , [Type
nTy, Type
_] <- [Type]
tys
        , Right Integer
n <-Except String Integer -> Either String Integer
forall e a. Except e a -> Either e a
runExcept (TyConMap -> Type -> Except String Integer
tyNatSize TyConMap
tcm Type
nTy)
        -> let ([Either TyVar Type]
_, Type -> TypeView
tyView -> TyConApp TyConName
intTcNm [Type]
_) = Type -> ([Either TyVar Type], Type)
splitFunForallTy Type
ty
               (Just TyCon
intTc) = TyConName -> TyConMap -> Maybe TyCon
forall a b. Uniquable a => a -> UniqMap b -> Maybe b
UniqMap.lookup TyConName
intTcNm TyConMap
tcm
               [DataCon
intCon] = TyCon -> [DataCon]
tyConDataCons TyCon
intTc
           in  Term -> Maybe Machine
reduce (Term -> [Either Term Type] -> Term
mkApps (DataCon -> Term
Data DataCon
intCon) [Term -> Either Term Type
forall a b. a -> Either a b
Left (Literal -> Term
Literal (Integer -> Literal
IntLiteral (Integer -> Integer
forall a. Integral a => a -> Integer
toInteger Integer
n)))])
      PrimStepContext
_ -> Maybe Machine
forall a. Maybe a
Nothing


  -- XXX: Not a thing anymore?
  , Text -> (PrimStepContext -> Maybe Machine) -> (Text, PrimStep)
primStepEntry Text
"Clash.Sized.Vector.maxIndex" ((PrimStepContext -> Maybe Machine) -> (Text, PrimStep))
-> (PrimStepContext -> Maybe Machine) -> (Text, PrimStep)
forall a b. (a -> b) -> a -> b
$ \case
      PrimStepContext{Bool
[Type]
[Value]
Type
TyConMap
Machine
PrimInfo
Term -> Maybe Machine
Term -> Term
Type
-> Integer -> Integer -> (Natural -> Natural -> Natural) -> Term
Type -> Integer -> (Natural -> Natural) -> Term
Type -> [Integer] -> ([Natural] -> Term) -> Term
Machine -> Term -> Maybe Machine
tcm :: PrimStepContext -> TyConMap
isSubj :: PrimStepContext -> Bool
pInfo :: PrimStepContext -> PrimInfo
tys :: PrimStepContext -> [Type]
args :: PrimStepContext -> [Value]
mach :: PrimStepContext -> Machine
ty :: PrimStepContext -> Type
checkNaturalRange1 :: PrimStepContext -> Type -> Integer -> (Natural -> Natural) -> Term
checkNaturalRange2 :: PrimStepContext
-> Type
-> Integer
-> Integer
-> (Natural -> Natural -> Natural)
-> Term
checkNaturalRange :: PrimStepContext -> Type -> [Integer] -> ([Natural] -> Term) -> Term
reduce :: PrimStepContext -> Term -> Maybe Machine
reduceWith :: PrimStepContext -> Machine -> Term -> Maybe Machine
reduceWHNF :: PrimStepContext -> Term -> Maybe Machine
reduceWHNF' :: PrimStepContext -> Machine -> Term -> Maybe Machine
catchDivByZero :: PrimStepContext -> Term -> Term
catchErrorCall :: PrimStepContext -> Term -> Term
tcm :: TyConMap
isSubj :: Bool
pInfo :: PrimInfo
tys :: [Type]
args :: [Value]
mach :: Machine
ty :: Type
checkNaturalRange1 :: Type -> Integer -> (Natural -> Natural) -> Term
checkNaturalRange2 :: Type
-> Integer -> Integer -> (Natural -> Natural -> Natural) -> Term
checkNaturalRange :: Type -> [Integer] -> ([Natural] -> Term) -> Term
reduce :: Term -> Maybe Machine
reduceWith :: Machine -> Term -> Maybe Machine
reduceWHNF :: Term -> Maybe Machine
reduceWHNF' :: Machine -> Term -> Maybe Machine
catchDivByZero :: Term -> Term
catchErrorCall :: Term -> Term
..}
        | Bool
isSubj
        , [Type
nTy, Type
_] <- [Type]
tys
        , Right Integer
n <- Except String Integer -> Either String Integer
forall e a. Except e a -> Either e a
runExcept (TyConMap -> Type -> Except String Integer
tyNatSize TyConMap
tcm Type
nTy)
        -> let ([Either TyVar Type]
_, Type -> TypeView
tyView -> TyConApp TyConName
intTcNm [Type]
_) = Type -> ([Either TyVar Type], Type)
splitFunForallTy Type
ty
               (Just TyCon
intTc) = TyConName -> TyConMap -> Maybe TyCon
forall a b. Uniquable a => a -> UniqMap b -> Maybe b
UniqMap.lookup TyConName
intTcNm TyConMap
tcm
               [DataCon
intCon] = TyCon -> [DataCon]
tyConDataCons TyCon
intTc
           in  Term -> Maybe Machine
reduce (Term -> [Either Term Type] -> Term
mkApps (DataCon -> Term
Data DataCon
intCon) [Term -> Either Term Type
forall a b. a -> Either a b
Left (Literal -> Term
Literal (Integer -> Literal
IntLiteral (Integer -> Integer
forall a. Integral a => a -> Integer
toInteger (Integer
n Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
- Integer
1))))])
      PrimStepContext
_ -> Maybe Machine
forall a. Maybe a
Nothing


-- Indexing
  -- XXX: Not exported
  , Text -> (PrimStepContext -> Maybe Machine) -> (Text, PrimStep)
primStepEntry Text
"Clash.Sized.Vector.index_int" ((PrimStepContext -> Maybe Machine) -> (Text, PrimStep))
-> (PrimStepContext -> Maybe Machine) -> (Text, PrimStep)
forall a b. (a -> b) -> a -> b
$ \case
      PrimStepContext{Bool
[Type]
[Value]
Type
TyConMap
Machine
PrimInfo
Term -> Maybe Machine
Term -> Term
Type
-> Integer -> Integer -> (Natural -> Natural -> Natural) -> Term
Type -> Integer -> (Natural -> Natural) -> Term
Type -> [Integer] -> ([Natural] -> Term) -> Term
Machine -> Term -> Maybe Machine
tcm :: PrimStepContext -> TyConMap
isSubj :: PrimStepContext -> Bool
pInfo :: PrimStepContext -> PrimInfo
tys :: PrimStepContext -> [Type]
args :: PrimStepContext -> [Value]
mach :: PrimStepContext -> Machine
ty :: PrimStepContext -> Type
checkNaturalRange1 :: PrimStepContext -> Type -> Integer -> (Natural -> Natural) -> Term
checkNaturalRange2 :: PrimStepContext
-> Type
-> Integer
-> Integer
-> (Natural -> Natural -> Natural)
-> Term
checkNaturalRange :: PrimStepContext -> Type -> [Integer] -> ([Natural] -> Term) -> Term
reduce :: PrimStepContext -> Term -> Maybe Machine
reduceWith :: PrimStepContext -> Machine -> Term -> Maybe Machine
reduceWHNF :: PrimStepContext -> Term -> Maybe Machine
reduceWHNF' :: PrimStepContext -> Machine -> Term -> Maybe Machine
catchDivByZero :: PrimStepContext -> Term -> Term
catchErrorCall :: PrimStepContext -> Term -> Term
tcm :: TyConMap
isSubj :: Bool
pInfo :: PrimInfo
tys :: [Type]
args :: [Value]
mach :: Machine
ty :: Type
checkNaturalRange1 :: Type -> Integer -> (Natural -> Natural) -> Term
checkNaturalRange2 :: Type
-> Integer -> Integer -> (Natural -> Natural -> Natural) -> Term
checkNaturalRange :: Type -> [Integer] -> ([Natural] -> Term) -> Term
reduce :: Term -> Maybe Machine
reduceWith :: Machine -> Term -> Maybe Machine
reduceWHNF :: Term -> Maybe Machine
reduceWHNF' :: Machine -> Term -> Maybe Machine
catchDivByZero :: Term -> Term
catchErrorCall :: Term -> Term
..} -- :: KnownNat n => Vec n a -> Int
        | Type
nTy : Type
aTy : [Type]
_  <- [Type]
tys
        , Value
_ : Value
xs : Value
i : [Value]
_ <- [Value]
args
        , DC DataCon
intDc [Left (Literal (IntLiteral Integer
i'))] <- Value
i
        -> if Integer
i' Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
< Integer
0
              then Maybe Machine
forall a. Maybe a
Nothing
              else case Value
xs of
                     DC DataCon
_ [Either Term Type]
vArgs  -> case Except String Integer -> Either String Integer
forall e a. Except e a -> Either e a
runExcept (TyConMap -> Type -> Except String Integer
tyNatSize TyConMap
tcm Type
nTy) of
                        Right Integer
0  -> Maybe Machine
forall a. Maybe a
Nothing
                        Right Integer
n' ->
                          if Integer
i' Integer -> Integer -> Bool
forall a. Eq a => a -> a -> Bool
== Integer
0
                             then Term -> Maybe Machine
reduceWHNF ([Either Term Type] -> [Term]
forall a b. [Either a b] -> [a]
Either.lefts [Either Term Type]
vArgs [Term] -> Int -> Term
forall a. HasCallStack => [a] -> Int -> a
!! Int
1)
                             else Term -> Maybe Machine
reduceWHNF (Term -> Maybe Machine) -> Term -> Maybe Machine
forall a b. (a -> b) -> a -> b
$
                                  Term -> [Either Term Type] -> Term
mkApps (PrimInfo -> Term
Prim PrimInfo
pInfo)
                                         [Type -> Either Term Type
forall a b. b -> Either a b
Right (LitTy -> Type
LitTy (Integer -> LitTy
NumTy (Integer
n'Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
-Integer
1)))
                                         ,Type -> Either Term Type
forall a b. b -> Either a b
Right Type
aTy
                                         ,Term -> Either Term Type
forall a b. a -> Either a b
Left (Literal -> Term
Literal (Integer -> Literal
NaturalLiteral (Integer
n'Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
-Integer
1)))
                                         ,Term -> Either Term Type
forall a b. a -> Either a b
Left ([Either Term Type] -> [Term]
forall a b. [Either a b] -> [a]
Either.lefts [Either Term Type]
vArgs [Term] -> Int -> Term
forall a. HasCallStack => [a] -> Int -> a
!! Int
2)
                                         ,Term -> Either Term Type
forall a b. a -> Either a b
Left (Term -> [Either Term Type] -> Term
mkApps (DataCon -> Term
Data DataCon
intDc)
                                                       [Term -> Either Term Type
forall a b. a -> Either a b
Left (Literal -> Term
Literal (Integer -> Literal
IntLiteral (Integer
i'Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
-Integer
1)))])
                                         ]
                        Either String Integer
_ -> Maybe Machine
forall a. Maybe a
Nothing
                     Value
_ -> Maybe Machine
forall a. Maybe a
Nothing
      PrimStepContext
_ -> Maybe Machine
forall a. Maybe a
Nothing

  , Text -> (PrimStepContext -> Maybe Machine) -> (Text, PrimStep)
primStepEntry $(textNameLit 'Clash.Sized.Vector.head) ((PrimStepContext -> Maybe Machine) -> (Text, PrimStep))
-> (PrimStepContext -> Maybe Machine) -> (Text, PrimStep)
forall a b. (a -> b) -> a -> b
$ \case
      PrimStepContext{Bool
[Type]
[Value]
Type
TyConMap
Machine
PrimInfo
Term -> Maybe Machine
Term -> Term
Type
-> Integer -> Integer -> (Natural -> Natural -> Natural) -> Term
Type -> Integer -> (Natural -> Natural) -> Term
Type -> [Integer] -> ([Natural] -> Term) -> Term
Machine -> Term -> Maybe Machine
tcm :: PrimStepContext -> TyConMap
isSubj :: PrimStepContext -> Bool
pInfo :: PrimStepContext -> PrimInfo
tys :: PrimStepContext -> [Type]
args :: PrimStepContext -> [Value]
mach :: PrimStepContext -> Machine
ty :: PrimStepContext -> Type
checkNaturalRange1 :: PrimStepContext -> Type -> Integer -> (Natural -> Natural) -> Term
checkNaturalRange2 :: PrimStepContext
-> Type
-> Integer
-> Integer
-> (Natural -> Natural -> Natural)
-> Term
checkNaturalRange :: PrimStepContext -> Type -> [Integer] -> ([Natural] -> Term) -> Term
reduce :: PrimStepContext -> Term -> Maybe Machine
reduceWith :: PrimStepContext -> Machine -> Term -> Maybe Machine
reduceWHNF :: PrimStepContext -> Term -> Maybe Machine
reduceWHNF' :: PrimStepContext -> Machine -> Term -> Maybe Machine
catchDivByZero :: PrimStepContext -> Term -> Term
catchErrorCall :: PrimStepContext -> Term -> Term
tcm :: TyConMap
isSubj :: Bool
pInfo :: PrimInfo
tys :: [Type]
args :: [Value]
mach :: Machine
ty :: Type
checkNaturalRange1 :: Type -> Integer -> (Natural -> Natural) -> Term
checkNaturalRange2 :: Type
-> Integer -> Integer -> (Natural -> Natural -> Natural) -> Term
checkNaturalRange :: Type -> [Integer] -> ([Natural] -> Term) -> Term
reduce :: Term -> Maybe Machine
reduceWith :: Machine -> Term -> Maybe Machine
reduceWHNF :: Term -> Maybe Machine
reduceWHNF' :: Machine -> Term -> Maybe Machine
catchDivByZero :: Term -> Term
catchErrorCall :: Term -> Term
..} -- :: Vec (n+1) a -> a
        | Bool
isSubj
        , [DC DataCon
_ [Either Term Type]
vArgs] <- [Value]
args
        -> Term -> Maybe Machine
reduceWHNF ([Either Term Type] -> [Term]
forall a b. [Either a b] -> [a]
Either.lefts [Either Term Type]
vArgs [Term] -> Int -> Term
forall a. HasCallStack => [a] -> Int -> a
!! Int
1)
      PrimStepContext
_ -> Maybe Machine
forall a. Maybe a
Nothing

  , Text -> (PrimStepContext -> Maybe Machine) -> (Text, PrimStep)
primStepEntry $(textNameLit 'Clash.Sized.Vector.last) ((PrimStepContext -> Maybe Machine) -> (Text, PrimStep))
-> (PrimStepContext -> Maybe Machine) -> (Text, PrimStep)
forall a b. (a -> b) -> a -> b
$ \case
      PrimStepContext{Bool
[Type]
[Value]
Type
TyConMap
Machine
PrimInfo
Term -> Maybe Machine
Term -> Term
Type
-> Integer -> Integer -> (Natural -> Natural -> Natural) -> Term
Type -> Integer -> (Natural -> Natural) -> Term
Type -> [Integer] -> ([Natural] -> Term) -> Term
Machine -> Term -> Maybe Machine
tcm :: PrimStepContext -> TyConMap
isSubj :: PrimStepContext -> Bool
pInfo :: PrimStepContext -> PrimInfo
tys :: PrimStepContext -> [Type]
args :: PrimStepContext -> [Value]
mach :: PrimStepContext -> Machine
ty :: PrimStepContext -> Type
checkNaturalRange1 :: PrimStepContext -> Type -> Integer -> (Natural -> Natural) -> Term
checkNaturalRange2 :: PrimStepContext
-> Type
-> Integer
-> Integer
-> (Natural -> Natural -> Natural)
-> Term
checkNaturalRange :: PrimStepContext -> Type -> [Integer] -> ([Natural] -> Term) -> Term
reduce :: PrimStepContext -> Term -> Maybe Machine
reduceWith :: PrimStepContext -> Machine -> Term -> Maybe Machine
reduceWHNF :: PrimStepContext -> Term -> Maybe Machine
reduceWHNF' :: PrimStepContext -> Machine -> Term -> Maybe Machine
catchDivByZero :: PrimStepContext -> Term -> Term
catchErrorCall :: PrimStepContext -> Term -> Term
tcm :: TyConMap
isSubj :: Bool
pInfo :: PrimInfo
tys :: [Type]
args :: [Value]
mach :: Machine
ty :: Type
checkNaturalRange1 :: Type -> Integer -> (Natural -> Natural) -> Term
checkNaturalRange2 :: Type
-> Integer -> Integer -> (Natural -> Natural -> Natural) -> Term
checkNaturalRange :: Type -> [Integer] -> ([Natural] -> Term) -> Term
reduce :: Term -> Maybe Machine
reduceWith :: Machine -> Term -> Maybe Machine
reduceWHNF :: Term -> Maybe Machine
reduceWHNF' :: Machine -> Term -> Maybe Machine
catchDivByZero :: Term -> Term
catchErrorCall :: Term -> Term
..} -- :: Vec (n+1) a -> a
        | Bool
isSubj
        , [DC DataCon
_ [Either Term Type]
vArgs] <- [Value]
args
        , (Right Type
_ : Right Type
aTy : Right Type
nTy : [Either Term Type]
_) <- [Either Term Type]
vArgs
        , Right Integer
n <- Except String Integer -> Either String Integer
forall e a. Except e a -> Either e a
runExcept (TyConMap -> Type -> Except String Integer
tyNatSize TyConMap
tcm Type
nTy)
        -> if Integer
n Integer -> Integer -> Bool
forall a. Eq a => a -> a -> Bool
== Integer
0
              then Term -> Maybe Machine
reduceWHNF ([Either Term Type] -> [Term]
forall a b. [Either a b] -> [a]
Either.lefts [Either Term Type]
vArgs [Term] -> Int -> Term
forall a. HasCallStack => [a] -> Int -> a
!! Int
1)
              else Term -> Maybe Machine
reduceWHNF
                    (Term -> [Either Term Type] -> Term
mkApps (PrimInfo -> Term
Prim PrimInfo
pInfo)
                                         [Type -> Either Term Type
forall a b. b -> Either a b
Right (LitTy -> Type
LitTy (Integer -> LitTy
NumTy (Integer
nInteger -> Integer -> Integer
forall a. Num a => a -> a -> a
-Integer
1)))
                                         ,Type -> Either Term Type
forall a b. b -> Either a b
Right Type
aTy
                                         ,Term -> Either Term Type
forall a b. a -> Either a b
Left ([Either Term Type] -> [Term]
forall a b. [Either a b] -> [a]
Either.lefts [Either Term Type]
vArgs [Term] -> Int -> Term
forall a. HasCallStack => [a] -> Int -> a
!! Int
2)
                                         ])
      PrimStepContext
_ -> Maybe Machine
forall a. Maybe a
Nothing

-- - Sub-vectors
  , Text -> (PrimStepContext -> Maybe Machine) -> (Text, PrimStep)
primStepEntry $(textNameLit 'Clash.Sized.Vector.tail) ((PrimStepContext -> Maybe Machine) -> (Text, PrimStep))
-> (PrimStepContext -> Maybe Machine) -> (Text, PrimStep)
forall a b. (a -> b) -> a -> b
$ \case
      PrimStepContext{Bool
[Type]
[Value]
Type
TyConMap
Machine
PrimInfo
Term -> Maybe Machine
Term -> Term
Type
-> Integer -> Integer -> (Natural -> Natural -> Natural) -> Term
Type -> Integer -> (Natural -> Natural) -> Term
Type -> [Integer] -> ([Natural] -> Term) -> Term
Machine -> Term -> Maybe Machine
tcm :: PrimStepContext -> TyConMap
isSubj :: PrimStepContext -> Bool
pInfo :: PrimStepContext -> PrimInfo
tys :: PrimStepContext -> [Type]
args :: PrimStepContext -> [Value]
mach :: PrimStepContext -> Machine
ty :: PrimStepContext -> Type
checkNaturalRange1 :: PrimStepContext -> Type -> Integer -> (Natural -> Natural) -> Term
checkNaturalRange2 :: PrimStepContext
-> Type
-> Integer
-> Integer
-> (Natural -> Natural -> Natural)
-> Term
checkNaturalRange :: PrimStepContext -> Type -> [Integer] -> ([Natural] -> Term) -> Term
reduce :: PrimStepContext -> Term -> Maybe Machine
reduceWith :: PrimStepContext -> Machine -> Term -> Maybe Machine
reduceWHNF :: PrimStepContext -> Term -> Maybe Machine
reduceWHNF' :: PrimStepContext -> Machine -> Term -> Maybe Machine
catchDivByZero :: PrimStepContext -> Term -> Term
catchErrorCall :: PrimStepContext -> Term -> Term
tcm :: TyConMap
isSubj :: Bool
pInfo :: PrimInfo
tys :: [Type]
args :: [Value]
mach :: Machine
ty :: Type
checkNaturalRange1 :: Type -> Integer -> (Natural -> Natural) -> Term
checkNaturalRange2 :: Type
-> Integer -> Integer -> (Natural -> Natural -> Natural) -> Term
checkNaturalRange :: Type -> [Integer] -> ([Natural] -> Term) -> Term
reduce :: Term -> Maybe Machine
reduceWith :: Machine -> Term -> Maybe Machine
reduceWHNF :: Term -> Maybe Machine
reduceWHNF' :: Machine -> Term -> Maybe Machine
catchDivByZero :: Term -> Term
catchErrorCall :: Term -> Term
..} -- :: Vec (n+1) a -> Vec n a
        | Bool
isSubj
        , [DC DataCon
_ [Either Term Type]
vArgs] <- [Value]
args
        -> Term -> Maybe Machine
reduceWHNF ([Either Term Type] -> [Term]
forall a b. [Either a b] -> [a]
Either.lefts [Either Term Type]
vArgs [Term] -> Int -> Term
forall a. HasCallStack => [a] -> Int -> a
!! Int
2)
      PrimStepContext
_ -> Maybe Machine
forall a. Maybe a
Nothing

  , Text -> (PrimStepContext -> Maybe Machine) -> (Text, PrimStep)
primStepEntry $(textNameLit 'Clash.Sized.Vector.init) ((PrimStepContext -> Maybe Machine) -> (Text, PrimStep))
-> (PrimStepContext -> Maybe Machine) -> (Text, PrimStep)
forall a b. (a -> b) -> a -> b
$ \case
      PrimStepContext{Bool
[Type]
[Value]
Type
TyConMap
Machine
PrimInfo
Term -> Maybe Machine
Term -> Term
Type
-> Integer -> Integer -> (Natural -> Natural -> Natural) -> Term
Type -> Integer -> (Natural -> Natural) -> Term
Type -> [Integer] -> ([Natural] -> Term) -> Term
Machine -> Term -> Maybe Machine
tcm :: PrimStepContext -> TyConMap
isSubj :: PrimStepContext -> Bool
pInfo :: PrimStepContext -> PrimInfo
tys :: PrimStepContext -> [Type]
args :: PrimStepContext -> [Value]
mach :: PrimStepContext -> Machine
ty :: PrimStepContext -> Type
checkNaturalRange1 :: PrimStepContext -> Type -> Integer -> (Natural -> Natural) -> Term
checkNaturalRange2 :: PrimStepContext
-> Type
-> Integer
-> Integer
-> (Natural -> Natural -> Natural)
-> Term
checkNaturalRange :: PrimStepContext -> Type -> [Integer] -> ([Natural] -> Term) -> Term
reduce :: PrimStepContext -> Term -> Maybe Machine
reduceWith :: PrimStepContext -> Machine -> Term -> Maybe Machine
reduceWHNF :: PrimStepContext -> Term -> Maybe Machine
reduceWHNF' :: PrimStepContext -> Machine -> Term -> Maybe Machine
catchDivByZero :: PrimStepContext -> Term -> Term
catchErrorCall :: PrimStepContext -> Term -> Term
tcm :: TyConMap
isSubj :: Bool
pInfo :: PrimInfo
tys :: [Type]
args :: [Value]
mach :: Machine
ty :: Type
checkNaturalRange1 :: Type -> Integer -> (Natural -> Natural) -> Term
checkNaturalRange2 :: Type
-> Integer -> Integer -> (Natural -> Natural -> Natural) -> Term
checkNaturalRange :: Type -> [Integer] -> ([Natural] -> Term) -> Term
reduce :: Term -> Maybe Machine
reduceWith :: Machine -> Term -> Maybe Machine
reduceWHNF :: Term -> Maybe Machine
reduceWHNF' :: Machine -> Term -> Maybe Machine
catchDivByZero :: Term -> Term
catchErrorCall :: Term -> Term
..} -- :: Vec (n+1) a -> Vec n a
        | Bool
isSubj
        , [DC DataCon
consCon [Either Term Type]
vArgs] <- [Value]
args
        , (Right Type
_ : Right Type
aTy : Right Type
nTy : [Either Term Type]
_) <- [Either Term Type]
vArgs
        , Right Integer
n <- Except String Integer -> Either String Integer
forall e a. Except e a -> Either e a
runExcept (TyConMap -> Type -> Except String Integer
tyNatSize TyConMap
tcm Type
nTy)
        -> if Integer
n Integer -> Integer -> Bool
forall a. Eq a => a -> a -> Bool
== Integer
0
              then Term -> Maybe Machine
reduceWHNF ([Either Term Type] -> [Term]
forall a b. [Either a b] -> [a]
Either.lefts [Either Term Type]
vArgs [Term] -> Int -> Term
forall a. HasCallStack => [a] -> Int -> a
!! Int
2)
              else Term -> Maybe Machine
reduce (Term -> Maybe Machine) -> Term -> Maybe Machine
forall a b. (a -> b) -> a -> b
$
                   HasCallStack => DataCon -> Type -> Integer -> Term -> Term -> Term
DataCon -> Type -> Integer -> Term -> Term -> Term
mkVecCons DataCon
consCon Type
aTy Integer
n
                      ([Either Term Type] -> [Term]
forall a b. [Either a b] -> [a]
Either.lefts [Either Term Type]
vArgs [Term] -> Int -> Term
forall a. HasCallStack => [a] -> Int -> a
!! Int
1)
                      (Term -> [Either Term Type] -> Term
mkApps (PrimInfo -> Term
Prim PrimInfo
pInfo)
                                           [Type -> Either Term Type
forall a b. b -> Either a b
Right (LitTy -> Type
LitTy (Integer -> LitTy
NumTy (Integer
nInteger -> Integer -> Integer
forall a. Num a => a -> a -> a
-Integer
1)))
                                           ,Type -> Either Term Type
forall a b. b -> Either a b
Right Type
aTy
                                           ,Term -> Either Term Type
forall a b. a -> Either a b
Left ([Either Term Type] -> [Term]
forall a b. [Either a b] -> [a]
Either.lefts [Either Term Type]
vArgs [Term] -> Int -> Term
forall a. HasCallStack => [a] -> Int -> a
!! Int
2)])
      PrimStepContext
_ -> Maybe Machine
forall a. Maybe a
Nothing

  , Text -> (PrimStepContext -> Maybe Machine) -> (Text, PrimStep)
primStepEntry $(textNameLit 'Clash.Sized.Vector.select) ((PrimStepContext -> Maybe Machine) -> (Text, PrimStep))
-> (PrimStepContext -> Maybe Machine) -> (Text, PrimStep)
forall a b. (a -> b) -> a -> b
$ \case
      PrimStepContext{Bool
[Type]
[Value]
Type
TyConMap
Machine
PrimInfo
Term -> Maybe Machine
Term -> Term
Type
-> Integer -> Integer -> (Natural -> Natural -> Natural) -> Term
Type -> Integer -> (Natural -> Natural) -> Term
Type -> [Integer] -> ([Natural] -> Term) -> Term
Machine -> Term -> Maybe Machine
tcm :: PrimStepContext -> TyConMap
isSubj :: PrimStepContext -> Bool
pInfo :: PrimStepContext -> PrimInfo
tys :: PrimStepContext -> [Type]
args :: PrimStepContext -> [Value]
mach :: PrimStepContext -> Machine
ty :: PrimStepContext -> Type
checkNaturalRange1 :: PrimStepContext -> Type -> Integer -> (Natural -> Natural) -> Term
checkNaturalRange2 :: PrimStepContext
-> Type
-> Integer
-> Integer
-> (Natural -> Natural -> Natural)
-> Term
checkNaturalRange :: PrimStepContext -> Type -> [Integer] -> ([Natural] -> Term) -> Term
reduce :: PrimStepContext -> Term -> Maybe Machine
reduceWith :: PrimStepContext -> Machine -> Term -> Maybe Machine
reduceWHNF :: PrimStepContext -> Term -> Maybe Machine
reduceWHNF' :: PrimStepContext -> Machine -> Term -> Maybe Machine
catchDivByZero :: PrimStepContext -> Term -> Term
catchErrorCall :: PrimStepContext -> Term -> Term
tcm :: TyConMap
isSubj :: Bool
pInfo :: PrimInfo
tys :: [Type]
args :: [Value]
mach :: Machine
ty :: Type
checkNaturalRange1 :: Type -> Integer -> (Natural -> Natural) -> Term
checkNaturalRange2 :: Type
-> Integer -> Integer -> (Natural -> Natural -> Natural) -> Term
checkNaturalRange :: Type -> [Integer] -> ([Natural] -> Term) -> Term
reduce :: Term -> Maybe Machine
reduceWith :: Machine -> Term -> Maybe Machine
reduceWHNF :: Term -> Maybe Machine
reduceWHNF' :: Machine -> Term -> Maybe Machine
catchDivByZero :: Term -> Term
catchErrorCall :: Term -> Term
..} -- :: (CmpNat (i+s) (s*n) ~ GT) => SNat f -> SNat s -> SNat n -> Vec (f + i) a -> Vec n a
        | Bool
isSubj
        , Type
iTy : Type
sTy : Type
nTy : Type
fTy : Type
aTy : [Type]
_ <- [Type]
tys
        , Value
eq : Value
f : Value
s : Value
n : Value
xs : [Value]
_ <- [Value]
args
        , Right Integer
n' <- Except String Integer -> Either String Integer
forall e a. Except e a -> Either e a
runExcept (TyConMap -> Type -> Except String Integer
tyNatSize TyConMap
tcm Type
nTy)
        , Right Integer
f' <- Except String Integer -> Either String Integer
forall e a. Except e a -> Either e a
runExcept (TyConMap -> Type -> Except String Integer
tyNatSize TyConMap
tcm Type
fTy)
        , Right Integer
i' <- Except String Integer -> Either String Integer
forall e a. Except e a -> Either e a
runExcept (TyConMap -> Type -> Except String Integer
tyNatSize TyConMap
tcm Type
iTy)
        , Right Integer
s' <- Except String Integer -> Either String Integer
forall e a. Except e a -> Either e a
runExcept (TyConMap -> Type -> Except String Integer
tyNatSize TyConMap
tcm Type
sTy)
        , DC DataCon
_ [Either Term Type]
vArgs <- Value
xs
        -> case Integer
n' of
             Integer
0 -> Term -> Maybe Machine
reduce (DataCon -> Type -> Term
mkVecNil DataCon
nilCon Type
aTy)
             Integer
_ -> case Integer
f' of
              Integer
0 -> let splitAtCall :: Term
splitAtCall =
                        Term -> [Either Term Type] -> Term
mkApps (TyConName -> TyConName -> Term
splitAtPrim TyConName
snatTcNm TyConName
vecTcNm)
                               [Type -> Either Term Type
forall a b. b -> Either a b
Right Type
sTy
                               ,Type -> Either Term Type
forall a b. b -> Either a b
Right (LitTy -> Type
LitTy (Integer -> LitTy
NumTy (Integer
i'Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
-Integer
s')))
                               ,Type -> Either Term Type
forall a b. b -> Either a b
Right Type
aTy
                               ,Term -> Either Term Type
forall a b. a -> Either a b
Left (Value -> Term
valToTerm Value
s)
                               ,Term -> Either Term Type
forall a b. a -> Either a b
Left (Value -> Term
valToTerm Value
xs)
                               ]
                       fVecTy :: Type
fVecTy = TyConName -> [Type] -> Type
mkTyConApp TyConName
vecTcNm [Type
sTy,Type
aTy]
                       iVecTy :: Type
iVecTy = TyConName -> [Type] -> Type
mkTyConApp TyConName
vecTcNm [LitTy -> Type
LitTy (Integer -> LitTy
NumTy (Integer
i'Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
-Integer
s')),Type
aTy]
                       -- Guaranteed no capture, so okay to use unsafe name generation
                       fNm :: Name a
fNm    = Text -> Unique -> Name a
forall a. Text -> Unique -> Name a
mkUnsafeSystemName Text
"fxs" Unique
0
                       iNm :: Name a
iNm    = Text -> Unique -> Name a
forall a. Text -> Unique -> Name a
mkUnsafeSystemName Text
"ixs" Unique
1
                       fId :: Id
fId    = Type -> TmName -> Id
mkLocalId Type
fVecTy TmName
forall {a}. Name a
fNm
                       iId :: Id
iId    = Type -> TmName -> Id
mkLocalId Type
iVecTy TmName
forall {a}. Name a
iNm
                       tupPat :: Pat
tupPat = DataCon -> [TyVar] -> [Id] -> Pat
DataPat DataCon
tupDc [] [Id
fId,Id
iId]
                       iAlt :: (Pat, Term)
iAlt   = (Pat
tupPat, (Id -> Term
Var Id
iId))
                   in  Term -> Maybe Machine
reduce (Term -> Maybe Machine) -> Term -> Maybe Machine
forall a b. (a -> b) -> a -> b
$
                       HasCallStack => DataCon -> Type -> Integer -> Term -> Term -> Term
DataCon -> Type -> Integer -> Term -> Term -> Term
mkVecCons DataCon
consCon Type
aTy Integer
n' ([Either Term Type] -> [Term]
forall a b. [Either a b] -> [a]
Either.lefts [Either Term Type]
vArgs [Term] -> Int -> Term
forall a. HasCallStack => [a] -> Int -> a
!! Int
1) (Term -> Term) -> Term -> Term
forall a b. (a -> b) -> a -> b
$
                       Term -> [Either Term Type] -> Term
mkApps (PrimInfo -> Term
Prim PrimInfo
pInfo)
                              [Type -> Either Term Type
forall a b. b -> Either a b
Right (LitTy -> Type
LitTy (Integer -> LitTy
NumTy (Integer
i'Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
-Integer
s')))
                              ,Type -> Either Term Type
forall a b. b -> Either a b
Right Type
sTy
                              ,Type -> Either Term Type
forall a b. b -> Either a b
Right (LitTy -> Type
LitTy (Integer -> LitTy
NumTy (Integer
n'Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
-Integer
1)))
                              ,Type -> Either Term Type
forall a b. b -> Either a b
Right (LitTy -> Type
LitTy (Integer -> LitTy
NumTy Integer
0))
                              ,Type -> Either Term Type
forall a b. b -> Either a b
Right Type
aTy
                              ,Term -> Either Term Type
forall a b. a -> Either a b
Left (Value -> Term
valToTerm Value
eq)
                              ,Term -> Either Term Type
forall a b. a -> Either a b
Left (Literal -> Term
Literal (Integer -> Literal
NaturalLiteral Integer
0))
                              ,Term -> Either Term Type
forall a b. a -> Either a b
Left (Value -> Term
valToTerm Value
s)
                              ,Term -> Either Term Type
forall a b. a -> Either a b
Left (Literal -> Term
Literal (Integer -> Literal
NaturalLiteral (Integer
n'Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
-Integer
1)))
                              ,Term -> Either Term Type
forall a b. a -> Either a b
Left (Term -> Type -> [(Pat, Term)] -> Term
Case Term
splitAtCall Type
iVecTy [(Pat, Term)
iAlt])
                              ]
              Integer
_ -> let splitAtCall :: Term
splitAtCall =
                        Term -> [Either Term Type] -> Term
mkApps (TyConName -> TyConName -> Term
splitAtPrim TyConName
snatTcNm TyConName
vecTcNm)
                               [Type -> Either Term Type
forall a b. b -> Either a b
Right Type
fTy
                               ,Type -> Either Term Type
forall a b. b -> Either a b
Right Type
iTy
                               ,Type -> Either Term Type
forall a b. b -> Either a b
Right Type
aTy
                               ,Term -> Either Term Type
forall a b. a -> Either a b
Left (Value -> Term
valToTerm Value
f)
                               ,Term -> Either Term Type
forall a b. a -> Either a b
Left (Value -> Term
valToTerm Value
xs)
                               ]
                       fVecTy :: Type
fVecTy = TyConName -> [Type] -> Type
mkTyConApp TyConName
vecTcNm [Type
fTy,Type
aTy]
                       iVecTy :: Type
iVecTy = TyConName -> [Type] -> Type
mkTyConApp TyConName
vecTcNm [Type
iTy,Type
aTy]
                       -- Guaranteed no capture, so okay to use unsafe name generation
                       fNm :: Name a
fNm    = Text -> Unique -> Name a
forall a. Text -> Unique -> Name a
mkUnsafeSystemName Text
"fxs" Unique
0
                       iNm :: Name a
iNm    = Text -> Unique -> Name a
forall a. Text -> Unique -> Name a
mkUnsafeSystemName Text
"ixs" Unique
1
                       fId :: Id
fId    = Type -> TmName -> Id
mkLocalId Type
fVecTy TmName
forall {a}. Name a
fNm
                       iId :: Id
iId    = Type -> TmName -> Id
mkLocalId Type
iVecTy TmName
forall {a}. Name a
iNm
                       tupPat :: Pat
tupPat = DataCon -> [TyVar] -> [Id] -> Pat
DataPat DataCon
tupDc [] [Id
fId,Id
iId]
                       iAlt :: (Pat, Term)
iAlt   = (Pat
tupPat, (Id -> Term
Var Id
iId))
                   in  Term -> Maybe Machine
reduceWHNF (Term -> Maybe Machine) -> Term -> Maybe Machine
forall a b. (a -> b) -> a -> b
$
                       Term -> [Either Term Type] -> Term
mkApps (PrimInfo -> Term
Prim PrimInfo
pInfo)
                         [Type -> Either Term Type
forall a b. b -> Either a b
Right Type
iTy
                         ,Type -> Either Term Type
forall a b. b -> Either a b
Right Type
sTy
                         ,Type -> Either Term Type
forall a b. b -> Either a b
Right Type
nTy
                         ,Type -> Either Term Type
forall a b. b -> Either a b
Right (LitTy -> Type
LitTy (Integer -> LitTy
NumTy Integer
0))
                         ,Type -> Either Term Type
forall a b. b -> Either a b
Right Type
aTy
                         ,Term -> Either Term Type
forall a b. a -> Either a b
Left (Value -> Term
valToTerm Value
eq)
                         ,Term -> Either Term Type
forall a b. a -> Either a b
Left (Literal -> Term
Literal (Integer -> Literal
NaturalLiteral Integer
0))
                         ,Term -> Either Term Type
forall a b. a -> Either a b
Left (Value -> Term
valToTerm Value
s)
                         ,Term -> Either Term Type
forall a b. a -> Either a b
Left (Value -> Term
valToTerm Value
n)
                         ,Term -> Either Term Type
forall a b. a -> Either a b
Left (Term -> Type -> [(Pat, Term)] -> Term
Case Term
splitAtCall Type
iVecTy [(Pat, Term)
iAlt])
                         ]
        where
          ([Either TyVar Type]
tyArgs,Type -> TypeView
tyView -> TyConApp TyConName
vecTcNm [Type]
_) = Type -> ([Either TyVar Type], Type)
splitFunForallTy Type
ty
          Just TyCon
vecTc          = TyConName -> TyConMap -> Maybe TyCon
forall a b. Uniquable a => a -> UniqMap b -> Maybe b
UniqMap.lookup TyConName
vecTcNm TyConMap
tcm
          [DataCon
nilCon,DataCon
consCon]    = TyCon -> [DataCon]
tyConDataCons TyCon
vecTc
          TyConApp TyConName
snatTcNm [Type]
_ = Type -> TypeView
tyView ([Either TyVar Type] -> [Type]
forall a b. [Either a b] -> [b]
Either.rights [Either TyVar Type]
tyArgs [Type] -> Int -> Type
forall a. HasCallStack => [a] -> Int -> a
!! Int
1)
          tupTcNm :: TyConName
tupTcNm            = TyCon -> TyConName
ghcTyconToTyConName (Boxity -> Int -> TyCon
tupleTyCon Boxity
Boxed Int
2)
          (Just TyCon
tupTc)       = TyConName -> TyConMap -> Maybe TyCon
forall a b. Uniquable a => a -> UniqMap b -> Maybe b
UniqMap.lookup TyConName
tupTcNm TyConMap
tcm
          [DataCon
tupDc]            = TyCon -> [DataCon]
tyConDataCons TyCon
tupTc
      PrimStepContext
_ -> Maybe Machine
forall a. Maybe a
Nothing

-- - Splitting
  , Text -> (PrimStepContext -> Maybe Machine) -> (Text, PrimStep)
primStepEntry $(textNameLit 'Clash.Sized.Vector.splitAt) ((PrimStepContext -> Maybe Machine) -> (Text, PrimStep))
-> (PrimStepContext -> Maybe Machine) -> (Text, PrimStep)
forall a b. (a -> b) -> a -> b
$ \case
      PrimStepContext{Bool
[Type]
[Value]
Type
TyConMap
Machine
PrimInfo
Term -> Maybe Machine
Term -> Term
Type
-> Integer -> Integer -> (Natural -> Natural -> Natural) -> Term
Type -> Integer -> (Natural -> Natural) -> Term
Type -> [Integer] -> ([Natural] -> Term) -> Term
Machine -> Term -> Maybe Machine
tcm :: PrimStepContext -> TyConMap
isSubj :: PrimStepContext -> Bool
pInfo :: PrimStepContext -> PrimInfo
tys :: PrimStepContext -> [Type]
args :: PrimStepContext -> [Value]
mach :: PrimStepContext -> Machine
ty :: PrimStepContext -> Type
checkNaturalRange1 :: PrimStepContext -> Type -> Integer -> (Natural -> Natural) -> Term
checkNaturalRange2 :: PrimStepContext
-> Type
-> Integer
-> Integer
-> (Natural -> Natural -> Natural)
-> Term
checkNaturalRange :: PrimStepContext -> Type -> [Integer] -> ([Natural] -> Term) -> Term
reduce :: PrimStepContext -> Term -> Maybe Machine
reduceWith :: PrimStepContext -> Machine -> Term -> Maybe Machine
reduceWHNF :: PrimStepContext -> Term -> Maybe Machine
reduceWHNF' :: PrimStepContext -> Machine -> Term -> Maybe Machine
catchDivByZero :: PrimStepContext -> Term -> Term
catchErrorCall :: PrimStepContext -> Term -> Term
tcm :: TyConMap
isSubj :: Bool
pInfo :: PrimInfo
tys :: [Type]
args :: [Value]
mach :: Machine
ty :: Type
checkNaturalRange1 :: Type -> Integer -> (Natural -> Natural) -> Term
checkNaturalRange2 :: Type
-> Integer -> Integer -> (Natural -> Natural -> Natural) -> Term
checkNaturalRange :: Type -> [Integer] -> ([Natural] -> Term) -> Term
reduce :: Term -> Maybe Machine
reduceWith :: Machine -> Term -> Maybe Machine
reduceWHNF :: Term -> Maybe Machine
reduceWHNF' :: Machine -> Term -> Maybe Machine
catchDivByZero :: Term -> Term
catchErrorCall :: Term -> Term
..} -- :: SNat m -> Vec (m + n) a -> (Vec m a, Vec n a)
        | Bool
isSubj
        , (DC DataCon
snatDc (Right Type
mTy:[Either Term Type]
_)):[Value]
_ <- [Value]
args
        , Right Integer
m <- Except String Integer -> Either String Integer
forall e a. Except e a -> Either e a
runExcept (TyConMap -> Type -> Except String Integer
tyNatSize TyConMap
tcm Type
mTy)
        -> let Type
_:Type
nTy:Type
aTy:[Type]
_ = [Type]
tys
               -- Get the tuple data-constructor
               ty1 :: Type
ty1 = HasCallStack => TyConMap -> Type -> [Type] -> Type
TyConMap -> Type -> [Type] -> Type
piResultTys TyConMap
tcm Type
ty [Type]
tys
               ([Either TyVar Type]
_,Type -> TypeView
tyView -> TyConApp TyConName
tupTcNm tyArgs :: [Type]
tyArgs@(Type
tyArg:[Type]
_)) = Type -> ([Either TyVar Type], Type)
splitFunForallTy Type
ty1
               (Just TyCon
tupTc)       = TyConName -> TyConMap -> Maybe TyCon
forall a b. Uniquable a => a -> UniqMap b -> Maybe b
UniqMap.lookup TyConName
tupTcNm TyConMap
tcm
               [DataCon
tupDc]            = TyCon -> [DataCon]
tyConDataCons TyCon
tupTc
               -- Get the vector data-constructors
               TyConApp TyConName
vecTcNm [Type]
_ = Type -> TypeView
tyView Type
tyArg
               Just TyCon
vecTc         = TyConName -> TyConMap -> Maybe TyCon
forall a b. Uniquable a => a -> UniqMap b -> Maybe b
UniqMap.lookup TyConName
vecTcNm TyConMap
tcm
               [DataCon
nilCon,DataCon
consCon]   = TyCon -> [DataCon]
tyConDataCons TyCon
vecTc
               -- Recursive call to @splitAt@
               splitAtRec :: Term -> Term
splitAtRec Term
v =
                Term -> [Either Term Type] -> Term
mkApps (PrimInfo -> Term
Prim PrimInfo
pInfo)
                       [Type -> Either Term Type
forall a b. b -> Either a b
Right (LitTy -> Type
LitTy (Integer -> LitTy
NumTy (Integer
mInteger -> Integer -> Integer
forall a. Num a => a -> a -> a
-Integer
1)))
                       ,Type -> Either Term Type
forall a b. b -> Either a b
Right Type
nTy
                       ,Type -> Either Term Type
forall a b. b -> Either a b
Right Type
aTy
                       ,Term -> Either Term Type
forall a b. a -> Either a b
Left (Term -> [Either Term Type] -> Term
mkApps (DataCon -> Term
Data DataCon
snatDc)
                                     [ Type -> Either Term Type
forall a b. b -> Either a b
Right (LitTy -> Type
LitTy (Integer -> LitTy
NumTy (Integer
mInteger -> Integer -> Integer
forall a. Num a => a -> a -> a
-Integer
1)))
                                     , Term -> Either Term Type
forall a b. a -> Either a b
Left  (Literal -> Term
Literal (Integer -> Literal
NaturalLiteral (Integer
mInteger -> Integer -> Integer
forall a. Num a => a -> a -> a
-Integer
1)))])
                       ,Term -> Either Term Type
forall a b. a -> Either a b
Left Term
v
                       ]
               m1VecTy :: Type
m1VecTy = TyConName -> [Type] -> Type
mkTyConApp TyConName
vecTcNm [LitTy -> Type
LitTy (Integer -> LitTy
NumTy (Integer
mInteger -> Integer -> Integer
forall a. Num a => a -> a -> a
-Integer
1)),Type
aTy]
               nVecTy :: Type
nVecTy  = TyConName -> [Type] -> Type
mkTyConApp TyConName
vecTcNm [Type
nTy,Type
aTy]
               -- Guaranteed no capture, so okay to use unsafe name generation
               lNm :: Name a
lNm     = Text -> Unique -> Name a
forall a. Text -> Unique -> Name a
mkUnsafeSystemName Text
"l" Unique
0
               rNm :: Name a
rNm     = Text -> Unique -> Name a
forall a. Text -> Unique -> Name a
mkUnsafeSystemName Text
"r" Unique
1
               lId :: Id
lId     = Type -> TmName -> Id
mkLocalId Type
m1VecTy TmName
forall {a}. Name a
lNm
               rId :: Id
rId     = Type -> TmName -> Id
mkLocalId Type
nVecTy TmName
forall {a}. Name a
rNm
               tupPat :: Pat
tupPat  = DataCon -> [TyVar] -> [Id] -> Pat
DataPat DataCon
tupDc [] [Id
lId,Id
rId]
               lAlt :: (Pat, Term)
lAlt    = (Pat
tupPat, (Id -> Term
Var Id
lId))
               rAlt :: (Pat, Term)
rAlt    = (Pat
tupPat, (Id -> Term
Var Id
rId))

           in case Integer
m of
             -- (Nil,v)
             Integer
0 -> Term -> Maybe Machine
reduce (Term -> Maybe Machine) -> Term -> Maybe Machine
forall a b. (a -> b) -> a -> b
$
                  Term -> [Either Term Type] -> Term
mkApps (DataCon -> Term
Data DataCon
tupDc) ([Either Term Type] -> Term) -> [Either Term Type] -> Term
forall a b. (a -> b) -> a -> b
$ ((Type -> Either Term Type) -> [Type] -> [Either Term Type]
forall a b. (a -> b) -> [a] -> [b]
map Type -> Either Term Type
forall a b. b -> Either a b
Right [Type]
tyArgs) [Either Term Type] -> [Either Term Type] -> [Either Term Type]
forall a. [a] -> [a] -> [a]
++
                    [ Term -> Either Term Type
forall a b. a -> Either a b
Left (DataCon -> Type -> Term
mkVecNil DataCon
nilCon Type
aTy)
                    , Term -> Either Term Type
forall a b. a -> Either a b
Left (Value -> Term
valToTerm ([Value] -> Value
forall a. HasCallStack => [a] -> a
last [Value]
args))
                    ]
             -- (x:xs) <- v
             Integer
m' | DC DataCon
_ [Either Term Type]
vArgs <- [Value] -> Value
forall a. HasCallStack => [a] -> a
last [Value]
args
                -- (x:fst (splitAt (m-1) xs),snd (splitAt (m-1) xs))
                -> case [Either Term Type] -> [Term]
forall a b. [Either a b] -> [a]
Either.lefts [Either Term Type]
vArgs of
                    (Term
_ : Term
x : Term
xs : [Term]
_) ->
                      let (Machine
mach1, Id
recId) = TyConMap -> Machine -> Term -> (Machine, Id)
newLetBinding TyConMap
tcm Machine
mach (Term -> Term
splitAtRec Term
xs)
                      in Machine -> Term -> Maybe Machine
reduceWith Machine
mach1 (Term -> Maybe Machine) -> Term -> Maybe Machine
forall a b. (a -> b) -> a -> b
$
                        Term -> [Either Term Type] -> Term
mkApps (DataCon -> Term
Data DataCon
tupDc) ([Either Term Type] -> Term) -> [Either Term Type] -> Term
forall a b. (a -> b) -> a -> b
$ ((Type -> Either Term Type) -> [Type] -> [Either Term Type]
forall a b. (a -> b) -> [a] -> [b]
map Type -> Either Term Type
forall a b. b -> Either a b
Right [Type]
tyArgs) [Either Term Type] -> [Either Term Type] -> [Either Term Type]
forall a. [a] -> [a] -> [a]
++
                          [ Term -> Either Term Type
forall a b. a -> Either a b
Left (HasCallStack => DataCon -> Type -> Integer -> Term -> Term -> Term
DataCon -> Type -> Integer -> Term -> Term -> Term
mkVecCons DataCon
consCon Type
aTy Integer
m' Term
x
                                    (Term -> Type -> [(Pat, Term)] -> Term
Case (Id -> Term
Var Id
recId) Type
m1VecTy [(Pat, Term)
lAlt]))
                          , Term -> Either Term Type
forall a b. a -> Either a b
Left (Term -> Type -> [(Pat, Term)] -> Term
Case (Id -> Term
Var Id
recId) Type
nVecTy [(Pat, Term)
rAlt])
                          ]
                    [Term]
_ ->
                      -- v actually reduces to Nil and not Cons, this only happens
                      -- when 'n' would reduce to a negative number; the complement
                      -- of 'm'.
                      --
                      -- See Clash issue: https://github.com/clash-lang/clash-compiler/issues/2831
                      let resTy :: Type
resTy = TyConMap -> Type -> [Type] -> Type
getResultTy TyConMap
tcm Type
ty [Type]
tys
                       in Term -> Maybe Machine
reduce (Term -> Type -> Term
TyApp (PrimInfo -> Term
Prim PrimInfo
NP.undefined) Type
resTy)

             -- v doesn't reduce to a data-constructor
             Integer
_  -> Maybe Machine
forall a. Maybe a
Nothing
      PrimStepContext
_ -> Maybe Machine
forall a. Maybe a
Nothing

  , Text -> (PrimStepContext -> Maybe Machine) -> (Text, PrimStep)
primStepEntry $(textNameLit 'Clash.Sized.Vector.unconcat) ((PrimStepContext -> Maybe Machine) -> (Text, PrimStep))
-> (PrimStepContext -> Maybe Machine) -> (Text, PrimStep)
forall a b. (a -> b) -> a -> b
$ \case
      PrimStepContext{Bool
[Type]
[Value]
Type
TyConMap
Machine
PrimInfo
Term -> Maybe Machine
Term -> Term
Type
-> Integer -> Integer -> (Natural -> Natural -> Natural) -> Term
Type -> Integer -> (Natural -> Natural) -> Term
Type -> [Integer] -> ([Natural] -> Term) -> Term
Machine -> Term -> Maybe Machine
tcm :: PrimStepContext -> TyConMap
isSubj :: PrimStepContext -> Bool
pInfo :: PrimStepContext -> PrimInfo
tys :: PrimStepContext -> [Type]
args :: PrimStepContext -> [Value]
mach :: PrimStepContext -> Machine
ty :: PrimStepContext -> Type
checkNaturalRange1 :: PrimStepContext -> Type -> Integer -> (Natural -> Natural) -> Term
checkNaturalRange2 :: PrimStepContext
-> Type
-> Integer
-> Integer
-> (Natural -> Natural -> Natural)
-> Term
checkNaturalRange :: PrimStepContext -> Type -> [Integer] -> ([Natural] -> Term) -> Term
reduce :: PrimStepContext -> Term -> Maybe Machine
reduceWith :: PrimStepContext -> Machine -> Term -> Maybe Machine
reduceWHNF :: PrimStepContext -> Term -> Maybe Machine
reduceWHNF' :: PrimStepContext -> Machine -> Term -> Maybe Machine
catchDivByZero :: PrimStepContext -> Term -> Term
catchErrorCall :: PrimStepContext -> Term -> Term
tcm :: TyConMap
isSubj :: Bool
pInfo :: PrimInfo
tys :: [Type]
args :: [Value]
mach :: Machine
ty :: Type
checkNaturalRange1 :: Type -> Integer -> (Natural -> Natural) -> Term
checkNaturalRange2 :: Type
-> Integer -> Integer -> (Natural -> Natural -> Natural) -> Term
checkNaturalRange :: Type -> [Integer] -> ([Natural] -> Term) -> Term
reduce :: Term -> Maybe Machine
reduceWith :: Machine -> Term -> Maybe Machine
reduceWHNF :: Term -> Maybe Machine
reduceWHNF' :: Machine -> Term -> Maybe Machine
catchDivByZero :: Term -> Term
catchErrorCall :: Term -> Term
..} -- :: KnownNat n => SNamt m -> Vec (n * m) a -> Vec n (Vec m a)
        | Bool
isSubj
        , Value
kn : Value
snat : Value
v : [Value]
_  <- [Value]
args
        , Type
nTy : Type
mTy : Type
aTy :[Type]
_ <- [Type]
tys
        , Lit (NaturalLiteral Integer
n) <- Value
kn
        -> let ( [Either TyVar Type] -> [Type]
forall a b. [Either a b] -> [b]
Either.rights -> [Type]
argTys, Type -> TypeView
tyView -> TyConApp TyConName
vecTcNm [Type]
_) =
                  Type -> ([Either TyVar Type], Type)
splitFunForallTy Type
ty
               Just TyCon
vecTc = TyConName -> TyConMap -> Maybe TyCon
forall a b. Uniquable a => a -> UniqMap b -> Maybe b
UniqMap.lookup TyConName
vecTcNm TyConMap
tcm
               [DataCon
nilCon,DataCon
consCon]   = TyCon -> [DataCon]
tyConDataCons TyCon
vecTc
               tupTcNm :: TyConName
tupTcNm            = TyCon -> TyConName
ghcTyconToTyConName (Boxity -> Int -> TyCon
tupleTyCon Boxity
Boxed Int
2)
               (Just TyCon
tupTc)       = TyConName -> TyConMap -> Maybe TyCon
forall a b. Uniquable a => a -> UniqMap b -> Maybe b
UniqMap.lookup TyConName
tupTcNm TyConMap
tcm
               [DataCon
tupDc]            = TyCon -> [DataCon]
tyConDataCons TyCon
tupTc
               TyConApp TyConName
snatTcNm [Type]
_ = Type -> TypeView
tyView ([Type]
argTys [Type] -> Int -> Type
forall a. HasCallStack => [a] -> Int -> a
!! Int
1)
               n1mTy :: Type
n1mTy  = TyConName -> [Type] -> Type
mkTyConApp TyConName
typeNatMul
                            [TyConName -> [Type] -> Type
mkTyConApp TyConName
typeNatSub [Type
nTy,LitTy -> Type
LitTy (Integer -> LitTy
NumTy Integer
1)]
                            ,Type
mTy]
               splitAtCall :: Term
splitAtCall =
                Term -> [Either Term Type] -> Term
mkApps (TyConName -> TyConName -> Term
splitAtPrim TyConName
snatTcNm TyConName
vecTcNm)
                       [Type -> Either Term Type
forall a b. b -> Either a b
Right Type
mTy
                       ,Type -> Either Term Type
forall a b. b -> Either a b
Right Type
n1mTy
                       ,Type -> Either Term Type
forall a b. b -> Either a b
Right Type
aTy
                       ,Term -> Either Term Type
forall a b. a -> Either a b
Left (Value -> Term
valToTerm Value
snat)
                       ,Term -> Either Term Type
forall a b. a -> Either a b
Left (Value -> Term
valToTerm Value
v)
                       ]
               mVecTy :: Type
mVecTy   = TyConName -> [Type] -> Type
mkTyConApp TyConName
vecTcNm [Type
mTy,Type
aTy]
               n1mVecTy :: Type
n1mVecTy = TyConName -> [Type] -> Type
mkTyConApp TyConName
vecTcNm [Type
n1mTy,Type
aTy]
               -- Guaranteed no capture, so okay to use unsafe name generation
               asNm :: Name a
asNm     = Text -> Unique -> Name a
forall a. Text -> Unique -> Name a
mkUnsafeSystemName Text
"as" Unique
0
               bsNm :: Name a
bsNm     = Text -> Unique -> Name a
forall a. Text -> Unique -> Name a
mkUnsafeSystemName Text
"bs" Unique
1
               asId :: Id
asId     = Type -> TmName -> Id
mkLocalId Type
mVecTy TmName
forall {a}. Name a
asNm
               bsId :: Id
bsId     = Type -> TmName -> Id
mkLocalId Type
n1mVecTy TmName
forall {a}. Name a
bsNm
               tupPat :: Pat
tupPat   = DataCon -> [TyVar] -> [Id] -> Pat
DataPat DataCon
tupDc [] [Id
asId,Id
bsId]
               asAlt :: (Pat, Term)
asAlt    = (Pat
tupPat, (Id -> Term
Var Id
asId))
               bsAlt :: (Pat, Term)
bsAlt    = (Pat
tupPat, (Id -> Term
Var Id
bsId))

           in  case Integer
n of
             Integer
0 -> Term -> Maybe Machine
reduce (DataCon -> Type -> Term
mkVecNil DataCon
nilCon Type
mVecTy)
             Integer
_ -> Term -> Maybe Machine
reduce (Term -> Maybe Machine) -> Term -> Maybe Machine
forall a b. (a -> b) -> a -> b
$
                  HasCallStack => DataCon -> Type -> Integer -> Term -> Term -> Term
DataCon -> Type -> Integer -> Term -> Term -> Term
mkVecCons DataCon
consCon Type
mVecTy Integer
n
                    (Term -> Type -> [(Pat, Term)] -> Term
Case Term
splitAtCall Type
mVecTy [(Pat, Term)
asAlt])
                    (Term -> [Either Term Type] -> Term
mkApps (PrimInfo -> Term
Prim PrimInfo
pInfo)
                        [Type -> Either Term Type
forall a b. b -> Either a b
Right (LitTy -> Type
LitTy (Integer -> LitTy
NumTy (Integer
nInteger -> Integer -> Integer
forall a. Num a => a -> a -> a
-Integer
1)))
                        ,Type -> Either Term Type
forall a b. b -> Either a b
Right Type
mTy
                        ,Type -> Either Term Type
forall a b. b -> Either a b
Right Type
aTy
                        ,Term -> Either Term Type
forall a b. a -> Either a b
Left (Literal -> Term
Literal (Integer -> Literal
NaturalLiteral (Integer
nInteger -> Integer -> Integer
forall a. Num a => a -> a -> a
-Integer
1)))
                        ,Term -> Either Term Type
forall a b. a -> Either a b
Left (Value -> Term
valToTerm Value
snat)
                        ,Term -> Either Term Type
forall a b. a -> Either a b
Left (Term -> Type -> [(Pat, Term)] -> Term
Case Term
splitAtCall Type
n1mVecTy [(Pat, Term)
bsAlt])])
      PrimStepContext
_ -> Maybe Machine
forall a. Maybe a
Nothing

-- Construction
-- - initialisation
  , Text -> (PrimStepContext -> Maybe Machine) -> (Text, PrimStep)
primStepEntry $(textNameLit 'Clash.Sized.Vector.replicate) ((PrimStepContext -> Maybe Machine) -> (Text, PrimStep))
-> (PrimStepContext -> Maybe Machine) -> (Text, PrimStep)
forall a b. (a -> b) -> a -> b
$ \case
      PrimStepContext{Bool
[Type]
[Value]
Type
TyConMap
Machine
PrimInfo
Term -> Maybe Machine
Term -> Term
Type
-> Integer -> Integer -> (Natural -> Natural -> Natural) -> Term
Type -> Integer -> (Natural -> Natural) -> Term
Type -> [Integer] -> ([Natural] -> Term) -> Term
Machine -> Term -> Maybe Machine
tcm :: PrimStepContext -> TyConMap
isSubj :: PrimStepContext -> Bool
pInfo :: PrimStepContext -> PrimInfo
tys :: PrimStepContext -> [Type]
args :: PrimStepContext -> [Value]
mach :: PrimStepContext -> Machine
ty :: PrimStepContext -> Type
checkNaturalRange1 :: PrimStepContext -> Type -> Integer -> (Natural -> Natural) -> Term
checkNaturalRange2 :: PrimStepContext
-> Type
-> Integer
-> Integer
-> (Natural -> Natural -> Natural)
-> Term
checkNaturalRange :: PrimStepContext -> Type -> [Integer] -> ([Natural] -> Term) -> Term
reduce :: PrimStepContext -> Term -> Maybe Machine
reduceWith :: PrimStepContext -> Machine -> Term -> Maybe Machine
reduceWHNF :: PrimStepContext -> Term -> Maybe Machine
reduceWHNF' :: PrimStepContext -> Machine -> Term -> Maybe Machine
catchDivByZero :: PrimStepContext -> Term -> Term
catchErrorCall :: PrimStepContext -> Term -> Term
tcm :: TyConMap
isSubj :: Bool
pInfo :: PrimInfo
tys :: [Type]
args :: [Value]
mach :: Machine
ty :: Type
checkNaturalRange1 :: Type -> Integer -> (Natural -> Natural) -> Term
checkNaturalRange2 :: Type
-> Integer -> Integer -> (Natural -> Natural -> Natural) -> Term
checkNaturalRange :: Type -> [Integer] -> ([Natural] -> Term) -> Term
reduce :: Term -> Maybe Machine
reduceWith :: Machine -> Term -> Maybe Machine
reduceWHNF :: Term -> Maybe Machine
reduceWHNF' :: Machine -> Term -> Maybe Machine
catchDivByZero :: Term -> Term
catchErrorCall :: Term -> Term
..} -- :: SNat n -> a -> Vec n a
        | Bool
isSubj
        , let ty' :: Type
ty' = HasCallStack => TyConMap -> Type -> [Type] -> Type
TyConMap -> Type -> [Type] -> Type
piResultTys TyConMap
tcm Type
ty [Type]
tys
        , let ([Either TyVar Type]
_,Type
resTy) = Type -> ([Either TyVar Type], Type)
splitFunForallTy Type
ty'
        , (TyConApp TyConName
vecTcNm [Type
lenTy,Type
argTy]) <- Type -> TypeView
tyView Type
resTy
        , Right Integer
len <- Except String Integer -> Either String Integer
forall e a. Except e a -> Either e a
runExcept (TyConMap -> Type -> Except String Integer
tyNatSize TyConMap
tcm Type
lenTy)
        -> let (Just TyCon
vecTc) = TyConName -> TyConMap -> Maybe TyCon
forall a b. Uniquable a => a -> UniqMap b -> Maybe b
UniqMap.lookup TyConName
vecTcNm TyConMap
tcm
               [DataCon
nilCon,DataCon
consCon] = TyCon -> [DataCon]
tyConDataCons TyCon
vecTc
           in  Term -> Maybe Machine
reduce (Term -> Maybe Machine) -> Term -> Maybe Machine
forall a b. (a -> b) -> a -> b
$
               DataCon -> DataCon -> Type -> Integer -> [Term] -> Term
mkVec DataCon
nilCon DataCon
consCon Type
argTy Integer
len
                     (Int -> Term -> [Term]
forall a. Int -> a -> [a]
replicate (Integer -> Int
forall a. Num a => Integer -> a
fromInteger Integer
len) (Value -> Term
valToTerm ([Value] -> Value
forall a. HasCallStack => [a] -> a
last [Value]
args)))
      PrimStepContext
_ -> Maybe Machine
forall a. Maybe a
Nothing

-- - Concatenation
  , Text -> (PrimStepContext -> Maybe Machine) -> (Text, PrimStep)
primStepEntry $(textNameLit '(Clash.Sized.Vector.++)) ((PrimStepContext -> Maybe Machine) -> (Text, PrimStep))
-> (PrimStepContext -> Maybe Machine) -> (Text, PrimStep)
forall a b. (a -> b) -> a -> b
$ \case
      PrimStepContext{Bool
[Type]
[Value]
Type
TyConMap
Machine
PrimInfo
Term -> Maybe Machine
Term -> Term
Type
-> Integer -> Integer -> (Natural -> Natural -> Natural) -> Term
Type -> Integer -> (Natural -> Natural) -> Term
Type -> [Integer] -> ([Natural] -> Term) -> Term
Machine -> Term -> Maybe Machine
tcm :: PrimStepContext -> TyConMap
isSubj :: PrimStepContext -> Bool
pInfo :: PrimStepContext -> PrimInfo
tys :: PrimStepContext -> [Type]
args :: PrimStepContext -> [Value]
mach :: PrimStepContext -> Machine
ty :: PrimStepContext -> Type
checkNaturalRange1 :: PrimStepContext -> Type -> Integer -> (Natural -> Natural) -> Term
checkNaturalRange2 :: PrimStepContext
-> Type
-> Integer
-> Integer
-> (Natural -> Natural -> Natural)
-> Term
checkNaturalRange :: PrimStepContext -> Type -> [Integer] -> ([Natural] -> Term) -> Term
reduce :: PrimStepContext -> Term -> Maybe Machine
reduceWith :: PrimStepContext -> Machine -> Term -> Maybe Machine
reduceWHNF :: PrimStepContext -> Term -> Maybe Machine
reduceWHNF' :: PrimStepContext -> Machine -> Term -> Maybe Machine
catchDivByZero :: PrimStepContext -> Term -> Term
catchErrorCall :: PrimStepContext -> Term -> Term
tcm :: TyConMap
isSubj :: Bool
pInfo :: PrimInfo
tys :: [Type]
args :: [Value]
mach :: Machine
ty :: Type
checkNaturalRange1 :: Type -> Integer -> (Natural -> Natural) -> Term
checkNaturalRange2 :: Type
-> Integer -> Integer -> (Natural -> Natural -> Natural) -> Term
checkNaturalRange :: Type -> [Integer] -> ([Natural] -> Term) -> Term
reduce :: Term -> Maybe Machine
reduceWith :: Machine -> Term -> Maybe Machine
reduceWHNF :: Term -> Maybe Machine
reduceWHNF' :: Machine -> Term -> Maybe Machine
catchDivByZero :: Term -> Term
catchErrorCall :: Term -> Term
..} -- :: Vec n a -> Vec m a -> Vec (n + m) a
        | Bool
isSubj
        , (DC DataCon
dc [Either Term Type]
vArgs):[Value]
_ <- [Value]
args
        , Right Type
nTy : Right Type
aTy : [Either Term Type]
_ <- [Either Term Type]
vArgs
        , Right Integer
n <- Except String Integer -> Either String Integer
forall e a. Except e a -> Either e a
runExcept (TyConMap -> Type -> Except String Integer
tyNatSize TyConMap
tcm Type
nTy)
        -> case Integer
n of
             Integer
0  -> Term -> Maybe Machine
reduce (Value -> Term
valToTerm ([Value] -> Value
forall a. HasCallStack => [a] -> a
last [Value]
args))
             Integer
n' | (Type
_ : Type
_ : Type
mTy : [Type]
_) <- [Type]
tys
                , Right Integer
m <- Except String Integer -> Either String Integer
forall e a. Except e a -> Either e a
runExcept (TyConMap -> Type -> Except String Integer
tyNatSize TyConMap
tcm Type
mTy)
                -> -- x : (xs ++ ys)
                   Term -> Maybe Machine
reduce (Term -> Maybe Machine) -> Term -> Maybe Machine
forall a b. (a -> b) -> a -> b
$
                   HasCallStack => DataCon -> Type -> Integer -> Term -> Term -> Term
DataCon -> Type -> Integer -> Term -> Term -> Term
mkVecCons DataCon
dc Type
aTy (Integer
n' Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
+ Integer
m) ([Either Term Type] -> [Term]
forall a b. [Either a b] -> [a]
Either.lefts [Either Term Type]
vArgs [Term] -> Int -> Term
forall a. HasCallStack => [a] -> Int -> a
!! Int
1)
                     (Term -> [Either Term Type] -> Term
mkApps (PrimInfo -> Term
Prim PrimInfo
pInfo)
                                          [Type -> Either Term Type
forall a b. b -> Either a b
Right (LitTy -> Type
LitTy (Integer -> LitTy
NumTy (Integer
n'Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
-Integer
1)))
                                          ,Type -> Either Term Type
forall a b. b -> Either a b
Right Type
aTy
                                          ,Type -> Either Term Type
forall a b. b -> Either a b
Right Type
mTy
                                          ,Term -> Either Term Type
forall a b. a -> Either a b
Left ([Either Term Type] -> [Term]
forall a b. [Either a b] -> [a]
Either.lefts [Either Term Type]
vArgs [Term] -> Int -> Term
forall a. HasCallStack => [a] -> Int -> a
!! Int
2)
                                          ,Term -> Either Term Type
forall a b. a -> Either a b
Left (Value -> Term
valToTerm ([Value] -> Value
forall a. HasCallStack => [a] -> a
last [Value]
args))
                                          ])
             Integer
_ -> Maybe Machine
forall a. Maybe a
Nothing
      PrimStepContext
_ -> Maybe Machine
forall a. Maybe a
Nothing

  , Text -> (PrimStepContext -> Maybe Machine) -> (Text, PrimStep)
primStepEntry $(textNameLit 'Clash.Sized.Vector.concat) ((PrimStepContext -> Maybe Machine) -> (Text, PrimStep))
-> (PrimStepContext -> Maybe Machine) -> (Text, PrimStep)
forall a b. (a -> b) -> a -> b
$ \case
      PrimStepContext{Bool
[Type]
[Value]
Type
TyConMap
Machine
PrimInfo
Term -> Maybe Machine
Term -> Term
Type
-> Integer -> Integer -> (Natural -> Natural -> Natural) -> Term
Type -> Integer -> (Natural -> Natural) -> Term
Type -> [Integer] -> ([Natural] -> Term) -> Term
Machine -> Term -> Maybe Machine
tcm :: PrimStepContext -> TyConMap
isSubj :: PrimStepContext -> Bool
pInfo :: PrimStepContext -> PrimInfo
tys :: PrimStepContext -> [Type]
args :: PrimStepContext -> [Value]
mach :: PrimStepContext -> Machine
ty :: PrimStepContext -> Type
checkNaturalRange1 :: PrimStepContext -> Type -> Integer -> (Natural -> Natural) -> Term
checkNaturalRange2 :: PrimStepContext
-> Type
-> Integer
-> Integer
-> (Natural -> Natural -> Natural)
-> Term
checkNaturalRange :: PrimStepContext -> Type -> [Integer] -> ([Natural] -> Term) -> Term
reduce :: PrimStepContext -> Term -> Maybe Machine
reduceWith :: PrimStepContext -> Machine -> Term -> Maybe Machine
reduceWHNF :: PrimStepContext -> Term -> Maybe Machine
reduceWHNF' :: PrimStepContext -> Machine -> Term -> Maybe Machine
catchDivByZero :: PrimStepContext -> Term -> Term
catchErrorCall :: PrimStepContext -> Term -> Term
tcm :: TyConMap
isSubj :: Bool
pInfo :: PrimInfo
tys :: [Type]
args :: [Value]
mach :: Machine
ty :: Type
checkNaturalRange1 :: Type -> Integer -> (Natural -> Natural) -> Term
checkNaturalRange2 :: Type
-> Integer -> Integer -> (Natural -> Natural -> Natural) -> Term
checkNaturalRange :: Type -> [Integer] -> ([Natural] -> Term) -> Term
reduce :: Term -> Maybe Machine
reduceWith :: Machine -> Term -> Maybe Machine
reduceWHNF :: Term -> Maybe Machine
reduceWHNF' :: Machine -> Term -> Maybe Machine
catchDivByZero :: Term -> Term
catchErrorCall :: Term -> Term
..} -- :: Vec n (Vec m a) -> Vec (n * m) a
        | Bool
isSubj
        , (Type
nTy : Type
mTy : Type
aTy : [Type]
_)  <- [Type]
tys
        , (Value
xs : [Value]
_)               <- [Value]
args
        , DC DataCon
dc [Either Term Type]
vArgs <- Value
xs
        , Right Integer
n <- Except String Integer -> Either String Integer
forall e a. Except e a -> Either e a
runExcept (TyConMap -> Type -> Except String Integer
tyNatSize TyConMap
tcm Type
nTy)
        -> case Integer
n of
            Integer
0 -> Term -> Maybe Machine
reduce (DataCon -> Type -> Term
mkVecNil DataCon
dc Type
aTy)
            Integer
_ | Term
_ : Term
h' : Term
t : [Term]
_ <- [Either Term Type] -> [Term]
forall a b. [Either a b] -> [a]
Either.lefts  [Either Term Type]
vArgs
              , ([Either TyVar Type]
_,Type -> TypeView
tyView -> TyConApp TyConName
vecTcNm [Type]
_) <- Type -> ([Either TyVar Type], Type)
splitFunForallTy Type
ty
              -> Term -> Maybe Machine
reduceWHNF (Term -> Maybe Machine) -> Term -> Maybe Machine
forall a b. (a -> b) -> a -> b
$
                 Term -> [Either Term Type] -> Term
mkApps (TyConName -> Term
vecAppendPrim TyConName
vecTcNm)
                        [Type -> Either Term Type
forall a b. b -> Either a b
Right Type
mTy
                        ,Type -> Either Term Type
forall a b. b -> Either a b
Right Type
aTy
                        ,Type -> Either Term Type
forall a b. b -> Either a b
Right (Type -> Either Term Type) -> Type -> Either Term Type
forall a b. (a -> b) -> a -> b
$ TyConName -> [Type] -> Type
mkTyConApp TyConName
typeNatMul
                          [TyConName -> [Type] -> Type
mkTyConApp TyConName
typeNatSub [Type
nTy,LitTy -> Type
LitTy (Integer -> LitTy
NumTy Integer
1)], Type
mTy]
                        ,Term -> Either Term Type
forall a b. a -> Either a b
Left Term
h'
                        ,Term -> Either Term Type
forall a b. a -> Either a b
Left (Term -> Either Term Type) -> Term -> Either Term Type
forall a b. (a -> b) -> a -> b
$ Term -> [Either Term Type] -> Term
mkApps (PrimInfo -> Term
Prim PrimInfo
pInfo)
                          [ Type -> Either Term Type
forall a b. b -> Either a b
Right (LitTy -> Type
LitTy (Integer -> LitTy
NumTy (Integer
nInteger -> Integer -> Integer
forall a. Num a => a -> a -> a
-Integer
1)))
                          , Type -> Either Term Type
forall a b. b -> Either a b
Right Type
mTy
                          , Type -> Either Term Type
forall a b. b -> Either a b
Right Type
aTy
                          , Term -> Either Term Type
forall a b. a -> Either a b
Left Term
t
                          ]
                        ]
            Integer
_ -> Maybe Machine
forall a. Maybe a
Nothing
      PrimStepContext
_ -> Maybe Machine
forall a. Maybe a
Nothing


-- Modifying vectors
  , Text -> (PrimStepContext -> Maybe Machine) -> (Text, PrimStep)
primStepEntry Text
"Clash.Sized.Vector.replace_int" ((PrimStepContext -> Maybe Machine) -> (Text, PrimStep))
-> (PrimStepContext -> Maybe Machine) -> (Text, PrimStep)
forall a b. (a -> b) -> a -> b
$ \case
      PrimStepContext{Bool
[Type]
[Value]
Type
TyConMap
Machine
PrimInfo
Term -> Maybe Machine
Term -> Term
Type
-> Integer -> Integer -> (Natural -> Natural -> Natural) -> Term
Type -> Integer -> (Natural -> Natural) -> Term
Type -> [Integer] -> ([Natural] -> Term) -> Term
Machine -> Term -> Maybe Machine
tcm :: PrimStepContext -> TyConMap
isSubj :: PrimStepContext -> Bool
pInfo :: PrimStepContext -> PrimInfo
tys :: PrimStepContext -> [Type]
args :: PrimStepContext -> [Value]
mach :: PrimStepContext -> Machine
ty :: PrimStepContext -> Type
checkNaturalRange1 :: PrimStepContext -> Type -> Integer -> (Natural -> Natural) -> Term
checkNaturalRange2 :: PrimStepContext
-> Type
-> Integer
-> Integer
-> (Natural -> Natural -> Natural)
-> Term
checkNaturalRange :: PrimStepContext -> Type -> [Integer] -> ([Natural] -> Term) -> Term
reduce :: PrimStepContext -> Term -> Maybe Machine
reduceWith :: PrimStepContext -> Machine -> Term -> Maybe Machine
reduceWHNF :: PrimStepContext -> Term -> Maybe Machine
reduceWHNF' :: PrimStepContext -> Machine -> Term -> Maybe Machine
catchDivByZero :: PrimStepContext -> Term -> Term
catchErrorCall :: PrimStepContext -> Term -> Term
tcm :: TyConMap
isSubj :: Bool
pInfo :: PrimInfo
tys :: [Type]
args :: [Value]
mach :: Machine
ty :: Type
checkNaturalRange1 :: Type -> Integer -> (Natural -> Natural) -> Term
checkNaturalRange2 :: Type
-> Integer -> Integer -> (Natural -> Natural -> Natural) -> Term
checkNaturalRange :: Type -> [Integer] -> ([Natural] -> Term) -> Term
reduce :: Term -> Maybe Machine
reduceWith :: Machine -> Term -> Maybe Machine
reduceWHNF :: Term -> Maybe Machine
reduceWHNF' :: Machine -> Term -> Maybe Machine
catchDivByZero :: Term -> Term
catchErrorCall :: Term -> Term
..} -- :: KnownNat n => Vec n a -> Int -> a -> Vec n a
        | Type
nTy : Type
aTy : [Type]
_  <- [Type]
tys
        , Value
_ : Value
xs : Value
i : Value
a : [Value]
_ <- [Value]
args
        , DC DataCon
intDc [Left (Literal (IntLiteral Integer
i'))] <- Value
i
        -> if Integer
i' Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
< Integer
0
              then Maybe Machine
forall a. Maybe a
Nothing
              else case Value
xs of
                     DC DataCon
vecTcNm [Either Term Type]
vArgs -> case Except String Integer -> Either String Integer
forall e a. Except e a -> Either e a
runExcept (TyConMap -> Type -> Except String Integer
tyNatSize TyConMap
tcm Type
nTy) of
                        Right Integer
0  -> Maybe Machine
forall a. Maybe a
Nothing
                        Right Integer
n' ->
                          if Integer
i' Integer -> Integer -> Bool
forall a. Eq a => a -> a -> Bool
== Integer
0
                             then Term -> Maybe Machine
reduce (HasCallStack => DataCon -> Type -> Integer -> Term -> Term -> Term
DataCon -> Type -> Integer -> Term -> Term -> Term
mkVecCons DataCon
vecTcNm Type
aTy Integer
n' (Value -> Term
valToTerm Value
a) ([Either Term Type] -> [Term]
forall a b. [Either a b] -> [a]
Either.lefts [Either Term Type]
vArgs [Term] -> Int -> Term
forall a. HasCallStack => [a] -> Int -> a
!! Int
2))
                             else Term -> Maybe Machine
reduce (Term -> Maybe Machine) -> Term -> Maybe Machine
forall a b. (a -> b) -> a -> b
$
                                  HasCallStack => DataCon -> Type -> Integer -> Term -> Term -> Term
DataCon -> Type -> Integer -> Term -> Term -> Term
mkVecCons DataCon
vecTcNm Type
aTy Integer
n' ([Either Term Type] -> [Term]
forall a b. [Either a b] -> [a]
Either.lefts [Either Term Type]
vArgs [Term] -> Int -> Term
forall a. HasCallStack => [a] -> Int -> a
!! Int
1)
                                    (Term -> [Either Term Type] -> Term
mkApps (PrimInfo -> Term
Prim PrimInfo
pInfo)
                                            [Type -> Either Term Type
forall a b. b -> Either a b
Right (LitTy -> Type
LitTy (Integer -> LitTy
NumTy (Integer
n'Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
-Integer
1)))
                                            ,Type -> Either Term Type
forall a b. b -> Either a b
Right Type
aTy
                                            ,Term -> Either Term Type
forall a b. a -> Either a b
Left (Literal -> Term
Literal (Integer -> Literal
NaturalLiteral (Integer
n'Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
-Integer
1)))
                                            ,Term -> Either Term Type
forall a b. a -> Either a b
Left ([Either Term Type] -> [Term]
forall a b. [Either a b] -> [a]
Either.lefts [Either Term Type]
vArgs [Term] -> Int -> Term
forall a. HasCallStack => [a] -> Int -> a
!! Int
2)
                                            ,Term -> Either Term Type
forall a b. a -> Either a b
Left (Term -> [Either Term Type] -> Term
mkApps (DataCon -> Term
Data DataCon
intDc)
                                                          [Term -> Either Term Type
forall a b. a -> Either a b
Left (Literal -> Term
Literal (Integer -> Literal
IntLiteral (Integer
i'Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
-Integer
1)))])
                                            ,Term -> Either Term Type
forall a b. a -> Either a b
Left (Value -> Term
valToTerm Value
a)
                                            ])
                        Either String Integer
_ -> Maybe Machine
forall a. Maybe a
Nothing
                     Value
_ -> Maybe Machine
forall a. Maybe a
Nothing
      PrimStepContext
_ -> Maybe Machine
forall a. Maybe a
Nothing


-- - specialized permutations
  , Text -> (PrimStepContext -> Maybe Machine) -> (Text, PrimStep)
primStepEntry $(textNameLit 'Clash.Sized.Vector.reverse) ((PrimStepContext -> Maybe Machine) -> (Text, PrimStep))
-> (PrimStepContext -> Maybe Machine) -> (Text, PrimStep)
forall a b. (a -> b) -> a -> b
$ \case
      PrimStepContext{Bool
[Type]
[Value]
Type
TyConMap
Machine
PrimInfo
Term -> Maybe Machine
Term -> Term
Type
-> Integer -> Integer -> (Natural -> Natural -> Natural) -> Term
Type -> Integer -> (Natural -> Natural) -> Term
Type -> [Integer] -> ([Natural] -> Term) -> Term
Machine -> Term -> Maybe Machine
tcm :: PrimStepContext -> TyConMap
isSubj :: PrimStepContext -> Bool
pInfo :: PrimStepContext -> PrimInfo
tys :: PrimStepContext -> [Type]
args :: PrimStepContext -> [Value]
mach :: PrimStepContext -> Machine
ty :: PrimStepContext -> Type
checkNaturalRange1 :: PrimStepContext -> Type -> Integer -> (Natural -> Natural) -> Term
checkNaturalRange2 :: PrimStepContext
-> Type
-> Integer
-> Integer
-> (Natural -> Natural -> Natural)
-> Term
checkNaturalRange :: PrimStepContext -> Type -> [Integer] -> ([Natural] -> Term) -> Term
reduce :: PrimStepContext -> Term -> Maybe Machine
reduceWith :: PrimStepContext -> Machine -> Term -> Maybe Machine
reduceWHNF :: PrimStepContext -> Term -> Maybe Machine
reduceWHNF' :: PrimStepContext -> Machine -> Term -> Maybe Machine
catchDivByZero :: PrimStepContext -> Term -> Term
catchErrorCall :: PrimStepContext -> Term -> Term
tcm :: TyConMap
isSubj :: Bool
pInfo :: PrimInfo
tys :: [Type]
args :: [Value]
mach :: Machine
ty :: Type
checkNaturalRange1 :: Type -> Integer -> (Natural -> Natural) -> Term
checkNaturalRange2 :: Type
-> Integer -> Integer -> (Natural -> Natural -> Natural) -> Term
checkNaturalRange :: Type -> [Integer] -> ([Natural] -> Term) -> Term
reduce :: Term -> Maybe Machine
reduceWith :: Machine -> Term -> Maybe Machine
reduceWHNF :: Term -> Maybe Machine
reduceWHNF' :: Machine -> Term -> Maybe Machine
catchDivByZero :: Term -> Term
catchErrorCall :: Term -> Term
..} -- :: Vec n a -> Vec n a
        | Bool
isSubj
        , Type
nTy : Type
aTy : [Type]
_  <- [Type]
tys
        , [DC DataCon
vecDc [Either Term Type]
vArgs] <- [Value]
args
        -> case Except String Integer -> Either String Integer
forall e a. Except e a -> Either e a
runExcept (TyConMap -> Type -> Except String Integer
tyNatSize TyConMap
tcm Type
nTy) of
             Right Integer
0 -> Term -> Maybe Machine
reduce (DataCon -> Type -> Term
mkVecNil DataCon
vecDc Type
aTy)
             Right Integer
n
               | ([Either TyVar Type]
_,Type -> TypeView
tyView -> TyConApp TyConName
vecTcNm [Type]
_) <- Type -> ([Either TyVar Type], Type)
splitFunForallTy Type
ty
               , let (Just TyCon
vecTc) = TyConName -> TyConMap -> Maybe TyCon
forall a b. Uniquable a => a -> UniqMap b -> Maybe b
UniqMap.lookup TyConName
vecTcNm TyConMap
tcm
               , let [DataCon
nilCon,DataCon
consCon] = TyCon -> [DataCon]
tyConDataCons TyCon
vecTc
               -> Term -> Maybe Machine
reduceWHNF (Term -> Maybe Machine) -> Term -> Maybe Machine
forall a b. (a -> b) -> a -> b
$
                  Term -> [Either Term Type] -> Term
mkApps (TyConName -> Term
vecAppendPrim TyConName
vecTcNm)
                    [Type -> Either Term Type
forall a b. b -> Either a b
Right (LitTy -> Type
LitTy (Integer -> LitTy
NumTy (Integer
nInteger -> Integer -> Integer
forall a. Num a => a -> a -> a
-Integer
1)))
                    ,Type -> Either Term Type
forall a b. b -> Either a b
Right Type
aTy
                    ,Type -> Either Term Type
forall a b. b -> Either a b
Right (LitTy -> Type
LitTy (Integer -> LitTy
NumTy Integer
1))
                    ,Term -> Either Term Type
forall a b. a -> Either a b
Left (Term -> [Either Term Type] -> Term
mkApps (PrimInfo -> Term
Prim PrimInfo
pInfo)
                                  [Type -> Either Term Type
forall a b. b -> Either a b
Right (LitTy -> Type
LitTy (Integer -> LitTy
NumTy (Integer
nInteger -> Integer -> Integer
forall a. Num a => a -> a -> a
-Integer
1)))
                                  ,Type -> Either Term Type
forall a b. b -> Either a b
Right Type
aTy
                                  ,Term -> Either Term Type
forall a b. a -> Either a b
Left ([Either Term Type] -> [Term]
forall a b. [Either a b] -> [a]
Either.lefts [Either Term Type]
vArgs [Term] -> Int -> Term
forall a. HasCallStack => [a] -> Int -> a
!! Int
2)
                                  ])
                    ,Term -> Either Term Type
forall a b. a -> Either a b
Left (DataCon -> DataCon -> Type -> Integer -> [Term] -> Term
mkVec DataCon
nilCon DataCon
consCon Type
aTy Integer
1 [[Either Term Type] -> [Term]
forall a b. [Either a b] -> [a]
Either.lefts [Either Term Type]
vArgs [Term] -> Int -> Term
forall a. HasCallStack => [a] -> Int -> a
!! Int
1])
                    ]
             Either String Integer
_ -> Maybe Machine
forall a. Maybe a
Nothing
      PrimStepContext
_ -> Maybe Machine
forall a. Maybe a
Nothing

  , Text -> (PrimStepContext -> Maybe Machine) -> (Text, PrimStep)
primStepEntry $(textNameLit 'Clash.Sized.Vector.transpose) ((PrimStepContext -> Maybe Machine) -> (Text, PrimStep))
-> (PrimStepContext -> Maybe Machine) -> (Text, PrimStep)
forall a b. (a -> b) -> a -> b
$ \case
      PrimStepContext{Bool
[Type]
[Value]
Type
TyConMap
Machine
PrimInfo
Term -> Maybe Machine
Term -> Term
Type
-> Integer -> Integer -> (Natural -> Natural -> Natural) -> Term
Type -> Integer -> (Natural -> Natural) -> Term
Type -> [Integer] -> ([Natural] -> Term) -> Term
Machine -> Term -> Maybe Machine
tcm :: PrimStepContext -> TyConMap
isSubj :: PrimStepContext -> Bool
pInfo :: PrimStepContext -> PrimInfo
tys :: PrimStepContext -> [Type]
args :: PrimStepContext -> [Value]
mach :: PrimStepContext -> Machine
ty :: PrimStepContext -> Type
checkNaturalRange1 :: PrimStepContext -> Type -> Integer -> (Natural -> Natural) -> Term
checkNaturalRange2 :: PrimStepContext
-> Type
-> Integer
-> Integer
-> (Natural -> Natural -> Natural)
-> Term
checkNaturalRange :: PrimStepContext -> Type -> [Integer] -> ([Natural] -> Term) -> Term
reduce :: PrimStepContext -> Term -> Maybe Machine
reduceWith :: PrimStepContext -> Machine -> Term -> Maybe Machine
reduceWHNF :: PrimStepContext -> Term -> Maybe Machine
reduceWHNF' :: PrimStepContext -> Machine -> Term -> Maybe Machine
catchDivByZero :: PrimStepContext -> Term -> Term
catchErrorCall :: PrimStepContext -> Term -> Term
tcm :: TyConMap
isSubj :: Bool
pInfo :: PrimInfo
tys :: [Type]
args :: [Value]
mach :: Machine
ty :: Type
checkNaturalRange1 :: Type -> Integer -> (Natural -> Natural) -> Term
checkNaturalRange2 :: Type
-> Integer -> Integer -> (Natural -> Natural -> Natural) -> Term
checkNaturalRange :: Type -> [Integer] -> ([Natural] -> Term) -> Term
reduce :: Term -> Maybe Machine
reduceWith :: Machine -> Term -> Maybe Machine
reduceWHNF :: Term -> Maybe Machine
reduceWHNF' :: Machine -> Term -> Maybe Machine
catchDivByZero :: Term -> Term
catchErrorCall :: Term -> Term
..} -- :: KnownNat n => Vec m (Vec n a) -> Vec n (Vec m a)
        | Bool
isSubj
        , Type
nTy : Type
mTy : Type
aTy : [Type]
_ <- [Type]
tys
        , Value
kn : Value
xss : [Value]
_ <- [Value]
args
        , ([Either TyVar Type]
_,Type -> TypeView
tyView -> TyConApp TyConName
vecTcNm [Type]
_) <- Type -> ([Either TyVar Type], Type)
splitFunForallTy Type
ty
        , DC DataCon
_ [Either Term Type]
vArgs <- Value
xss
        , Right Integer
n <- Except String Integer -> Either String Integer
forall e a. Except e a -> Either e a
runExcept (TyConMap -> Type -> Except String Integer
tyNatSize TyConMap
tcm Type
nTy)
        , Right Integer
m <- Except String Integer -> Either String Integer
forall e a. Except e a -> Either e a
runExcept (TyConMap -> Type -> Except String Integer
tyNatSize TyConMap
tcm Type
mTy)
        -> case Integer
m of
          Integer
0 -> let (Just TyCon
vecTc)     = TyConName -> TyConMap -> Maybe TyCon
forall a b. Uniquable a => a -> UniqMap b -> Maybe b
UniqMap.lookup TyConName
vecTcNm TyConMap
tcm
                   [DataCon
nilCon,DataCon
consCon] = TyCon -> [DataCon]
tyConDataCons TyCon
vecTc
               in  Term -> Maybe Machine
reduce (Term -> Maybe Machine) -> Term -> Maybe Machine
forall a b. (a -> b) -> a -> b
$
                   DataCon -> DataCon -> Type -> Integer -> [Term] -> Term
mkVec DataCon
nilCon DataCon
consCon (TyConName -> [Type] -> Type
mkTyConApp TyConName
vecTcNm [Type
mTy,Type
aTy]) Integer
n
                    (Int -> Term -> [Term]
forall a. Int -> a -> [a]
replicate (Integer -> Int
forall a. Num a => Integer -> a
fromInteger Integer
n) (DataCon -> DataCon -> Type -> Integer -> [Term] -> Term
mkVec DataCon
nilCon DataCon
consCon Type
aTy Integer
0 []))
          Integer
m' -> let (Just TyCon
vecTc)     = TyConName -> TyConMap -> Maybe TyCon
forall a b. Uniquable a => a -> UniqMap b -> Maybe b
UniqMap.lookup TyConName
vecTcNm TyConMap
tcm
                    [DataCon
_,DataCon
consCon] = TyCon -> [DataCon]
tyConDataCons TyCon
vecTc
                    Just (Type
consCoTy : [Type]
_) = DataCon -> [Type] -> Maybe [Type]
dataConInstArgTys DataCon
consCon
                                            [Type
mTy,Type
aTy,LitTy -> Type
LitTy (Integer -> LitTy
NumTy (Integer
m'Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
-Integer
1))]
                in  Term -> Maybe Machine
reduceWHNF (Term -> Maybe Machine) -> Term -> Maybe Machine
forall a b. (a -> b) -> a -> b
$
                    Term -> [Either Term Type] -> Term
mkApps (TyConName -> Term
vecZipWithPrim TyConName
vecTcNm)
                           [ Type -> Either Term Type
forall a b. b -> Either a b
Right Type
aTy
                           , Type -> Either Term Type
forall a b. b -> Either a b
Right (TyConName -> [Type] -> Type
mkTyConApp TyConName
vecTcNm [LitTy -> Type
LitTy (Integer -> LitTy
NumTy (Integer
m'Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
-Integer
1)),Type
aTy])
                           , Type -> Either Term Type
forall a b. b -> Either a b
Right (TyConName -> [Type] -> Type
mkTyConApp TyConName
vecTcNm [Type
mTy,Type
aTy])
                           , 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  (Term -> [Either Term Type] -> Term
mkApps (DataCon -> Term
Data DataCon
consCon)
                                           [Type -> Either Term Type
forall a b. b -> Either a b
Right Type
mTy
                                           ,Type -> Either Term Type
forall a b. b -> Either a b
Right Type
aTy
                                           ,Type -> Either Term Type
forall a b. b -> Either a b
Right (LitTy -> Type
LitTy (Integer -> LitTy
NumTy (Integer
m'Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
-Integer
1)))
                                           ,Term -> Either Term Type
forall a b. a -> Either a b
Left (Type -> Term
primCo Type
consCoTy)
                                           ])
                           , Term -> Either Term Type
forall a b. a -> Either a b
Left  ([Either Term Type] -> [Term]
forall a b. [Either a b] -> [a]
Either.lefts [Either Term Type]
vArgs [Term] -> Int -> Term
forall a. HasCallStack => [a] -> Int -> a
!! Int
1)
                           , Term -> Either Term Type
forall a b. a -> Either a b
Left  (Term -> [Either Term Type] -> Term
mkApps (PrimInfo -> Term
Prim PrimInfo
pInfo)
                                           [ Type -> Either Term Type
forall a b. b -> Either a b
Right Type
nTy
                                           , Type -> Either Term Type
forall a b. b -> Either a b
Right (LitTy -> Type
LitTy (Integer -> LitTy
NumTy (Integer
m'Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
-Integer
1)))
                                           , Type -> Either Term Type
forall a b. b -> Either a b
Right Type
aTy
                                           , Term -> Either Term Type
forall a b. a -> Either a b
Left  (Value -> Term
valToTerm Value
kn)
                                           , Term -> Either Term Type
forall a b. a -> Either a b
Left  ([Either Term Type] -> [Term]
forall a b. [Either a b] -> [a]
Either.lefts [Either Term Type]
vArgs [Term] -> Int -> Term
forall a. HasCallStack => [a] -> Int -> a
!! Int
2)
                                           ])
                           ]
      PrimStepContext
_ -> Maybe Machine
forall a. Maybe a
Nothing

  , Text -> (PrimStepContext -> Maybe Machine) -> (Text, PrimStep)
primStepEntry $(textNameLit 'Clash.Sized.Vector.rotateLeftS) ((PrimStepContext -> Maybe Machine) -> (Text, PrimStep))
-> (PrimStepContext -> Maybe Machine) -> (Text, PrimStep)
forall a b. (a -> b) -> a -> b
$ \case
      PrimStepContext{Bool
[Type]
[Value]
Type
TyConMap
Machine
PrimInfo
Term -> Maybe Machine
Term -> Term
Type
-> Integer -> Integer -> (Natural -> Natural -> Natural) -> Term
Type -> Integer -> (Natural -> Natural) -> Term
Type -> [Integer] -> ([Natural] -> Term) -> Term
Machine -> Term -> Maybe Machine
tcm :: PrimStepContext -> TyConMap
isSubj :: PrimStepContext -> Bool
pInfo :: PrimStepContext -> PrimInfo
tys :: PrimStepContext -> [Type]
args :: PrimStepContext -> [Value]
mach :: PrimStepContext -> Machine
ty :: PrimStepContext -> Type
checkNaturalRange1 :: PrimStepContext -> Type -> Integer -> (Natural -> Natural) -> Term
checkNaturalRange2 :: PrimStepContext
-> Type
-> Integer
-> Integer
-> (Natural -> Natural -> Natural)
-> Term
checkNaturalRange :: PrimStepContext -> Type -> [Integer] -> ([Natural] -> Term) -> Term
reduce :: PrimStepContext -> Term -> Maybe Machine
reduceWith :: PrimStepContext -> Machine -> Term -> Maybe Machine
reduceWHNF :: PrimStepContext -> Term -> Maybe Machine
reduceWHNF' :: PrimStepContext -> Machine -> Term -> Maybe Machine
catchDivByZero :: PrimStepContext -> Term -> Term
catchErrorCall :: PrimStepContext -> Term -> Term
tcm :: TyConMap
isSubj :: Bool
pInfo :: PrimInfo
tys :: [Type]
args :: [Value]
mach :: Machine
ty :: Type
checkNaturalRange1 :: Type -> Integer -> (Natural -> Natural) -> Term
checkNaturalRange2 :: Type
-> Integer -> Integer -> (Natural -> Natural -> Natural) -> Term
checkNaturalRange :: Type -> [Integer] -> ([Natural] -> Term) -> Term
reduce :: Term -> Maybe Machine
reduceWith :: Machine -> Term -> Maybe Machine
reduceWHNF :: Term -> Maybe Machine
reduceWHNF' :: Machine -> Term -> Maybe Machine
catchDivByZero :: Term -> Term
catchErrorCall :: Term -> Term
..} -- :: KnownNat n => Vec n a -> SNat d -> Vec n a
        | Type
nTy : Type
aTy : Type
_ : [Type]
_ <- [Type]
tys
        , Value
kn : Value
xs : Value
d : [Value]
_ <- [Value]
args
        , DC DataCon
dc [Either Term Type]
vArgs <- Value
xs
        , Right Integer
n <- Except String Integer -> Either String Integer
forall e a. Except e a -> Either e a
runExcept (TyConMap -> Type -> Except String Integer
tyNatSize TyConMap
tcm Type
nTy)
        -> case Integer
n of
             Integer
0  -> Term -> Maybe Machine
reduce (DataCon -> Type -> Term
mkVecNil DataCon
dc Type
aTy)
             Integer
n' | DC DataCon
snatDc [Either Term Type
_,Left Term
d'] <- Value
d
                , Evaluator
eval <- Step -> Unwind -> PrimStep -> PrimUnwind -> Evaluator
Evaluator Step
ghcStep Unwind
ghcUnwind PrimStep
ghcPrimStep PrimUnwind
ghcPrimUnwind
                , mach2 :: Machine
mach2@Machine{mStack :: Machine -> Stack
mStack=[],mTerm :: Machine -> Term
mTerm=Literal (NaturalLiteral Integer
d2)} <- Evaluator -> TyConMap -> Bool -> Machine -> Machine
whnf Evaluator
eval TyConMap
tcm Bool
isSubj (Term -> Machine -> Machine
setTerm Term
d' (Machine -> Machine) -> Machine -> Machine
forall a b. (a -> b) -> a -> b
$ Machine -> Machine
stackClear Machine
mach)
                -> case (Integer
d2 Integer -> Integer -> Integer
forall a. Integral a => a -> a -> a
`mod` Integer
n) of
                     Integer
0  -> Term -> Maybe Machine
reduce (Value -> Term
valToTerm Value
xs)
                     Integer
d3 -> let ([Either TyVar Type]
_,Type -> TypeView
tyView -> TyConApp TyConName
vecTcNm [Type]
_) = Type -> ([Either TyVar Type], Type)
splitFunForallTy Type
ty
                               (Just TyCon
vecTc)     = TyConName -> TyConMap -> Maybe TyCon
forall a b. Uniquable a => a -> UniqMap b -> Maybe b
UniqMap.lookup TyConName
vecTcNm TyConMap
tcm
                               [DataCon
nilCon,DataCon
consCon] = TyCon -> [DataCon]
tyConDataCons TyCon
vecTc
                           in  Machine -> Term -> Maybe Machine
reduceWHNF' Machine
mach2 (Term -> Maybe Machine) -> Term -> Maybe Machine
forall a b. (a -> b) -> a -> b
$
                               Term -> [Either Term Type] -> Term
mkApps (PrimInfo -> Term
Prim PrimInfo
pInfo)
                                      [Type -> Either Term Type
forall a b. b -> Either a b
Right Type
nTy
                                      ,Type -> Either Term Type
forall a b. b -> Either a b
Right Type
aTy
                                      ,Type -> Either Term Type
forall a b. b -> Either a b
Right (LitTy -> Type
LitTy (Integer -> LitTy
NumTy (Integer
d3Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
-Integer
1)))
                                      ,Term -> Either Term Type
forall a b. a -> Either a b
Left (Value -> Term
valToTerm Value
kn)
                                      ,Term -> Either Term Type
forall a b. a -> Either a b
Left (Term -> [Either Term Type] -> Term
mkApps (TyConName -> Term
vecAppendPrim TyConName
vecTcNm)
                                                    [Type -> Either Term Type
forall a b. b -> Either a b
Right (LitTy -> Type
LitTy (Integer -> LitTy
NumTy (Integer
n'Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
-Integer
1)))
                                                    ,Type -> Either Term Type
forall a b. b -> Either a b
Right Type
aTy
                                                    ,Type -> Either Term Type
forall a b. b -> Either a b
Right (LitTy -> Type
LitTy (Integer -> LitTy
NumTy Integer
1))
                                                    ,Term -> Either Term Type
forall a b. a -> Either a b
Left  ([Either Term Type] -> [Term]
forall a b. [Either a b] -> [a]
Either.lefts [Either Term Type]
vArgs [Term] -> Int -> Term
forall a. HasCallStack => [a] -> Int -> a
!! Int
2)
                                                    ,Term -> Either Term Type
forall a b. a -> Either a b
Left  (DataCon -> DataCon -> Type -> Integer -> [Term] -> Term
mkVec DataCon
nilCon DataCon
consCon Type
aTy Integer
1 [[Either Term Type] -> [Term]
forall a b. [Either a b] -> [a]
Either.lefts [Either Term Type]
vArgs [Term] -> Int -> Term
forall a. HasCallStack => [a] -> Int -> a
!! Int
1])])
                                      ,Term -> Either Term Type
forall a b. a -> Either a b
Left (Term -> [Either Term Type] -> Term
mkApps (DataCon -> Term
Data DataCon
snatDc)
                                                    [Type -> Either Term Type
forall a b. b -> Either a b
Right (LitTy -> Type
LitTy (Integer -> LitTy
NumTy (Integer
d3Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
-Integer
1)))
                                                    ,Term -> Either Term Type
forall a b. a -> Either a b
Left  (Literal -> Term
Literal (Integer -> Literal
NaturalLiteral (Integer
d3Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
-Integer
1)))])
                                      ]
             Integer
_  -> Maybe Machine
forall a. Maybe a
Nothing
      PrimStepContext
_ -> Maybe Machine
forall a. Maybe a
Nothing

  , Text -> (PrimStepContext -> Maybe Machine) -> (Text, PrimStep)
primStepEntry $(textNameLit 'Clash.Sized.Vector.rotateRightS) ((PrimStepContext -> Maybe Machine) -> (Text, PrimStep))
-> (PrimStepContext -> Maybe Machine) -> (Text, PrimStep)
forall a b. (a -> b) -> a -> b
$ \case
      PrimStepContext{Bool
[Type]
[Value]
Type
TyConMap
Machine
PrimInfo
Term -> Maybe Machine
Term -> Term
Type
-> Integer -> Integer -> (Natural -> Natural -> Natural) -> Term
Type -> Integer -> (Natural -> Natural) -> Term
Type -> [Integer] -> ([Natural] -> Term) -> Term
Machine -> Term -> Maybe Machine
tcm :: PrimStepContext -> TyConMap
isSubj :: PrimStepContext -> Bool
pInfo :: PrimStepContext -> PrimInfo
tys :: PrimStepContext -> [Type]
args :: PrimStepContext -> [Value]
mach :: PrimStepContext -> Machine
ty :: PrimStepContext -> Type
checkNaturalRange1 :: PrimStepContext -> Type -> Integer -> (Natural -> Natural) -> Term
checkNaturalRange2 :: PrimStepContext
-> Type
-> Integer
-> Integer
-> (Natural -> Natural -> Natural)
-> Term
checkNaturalRange :: PrimStepContext -> Type -> [Integer] -> ([Natural] -> Term) -> Term
reduce :: PrimStepContext -> Term -> Maybe Machine
reduceWith :: PrimStepContext -> Machine -> Term -> Maybe Machine
reduceWHNF :: PrimStepContext -> Term -> Maybe Machine
reduceWHNF' :: PrimStepContext -> Machine -> Term -> Maybe Machine
catchDivByZero :: PrimStepContext -> Term -> Term
catchErrorCall :: PrimStepContext -> Term -> Term
tcm :: TyConMap
isSubj :: Bool
pInfo :: PrimInfo
tys :: [Type]
args :: [Value]
mach :: Machine
ty :: Type
checkNaturalRange1 :: Type -> Integer -> (Natural -> Natural) -> Term
checkNaturalRange2 :: Type
-> Integer -> Integer -> (Natural -> Natural -> Natural) -> Term
checkNaturalRange :: Type -> [Integer] -> ([Natural] -> Term) -> Term
reduce :: Term -> Maybe Machine
reduceWith :: Machine -> Term -> Maybe Machine
reduceWHNF :: Term -> Maybe Machine
reduceWHNF' :: Machine -> Term -> Maybe Machine
catchDivByZero :: Term -> Term
catchErrorCall :: Term -> Term
..} -- :: KnownNat n => Vec n a -> SNat d -> Vec n a
        | Bool
isSubj
        , Type
nTy : Type
aTy : Type
_ : [Type]
_ <- [Type]
tys
        , Value
kn : Value
xs : Value
d : [Value]
_ <- [Value]
args
        , DC DataCon
dc [Either Term Type]
_ <- Value
xs
        , Right Integer
n <- Except String Integer -> Either String Integer
forall e a. Except e a -> Either e a
runExcept (TyConMap -> Type -> Except String Integer
tyNatSize TyConMap
tcm Type
nTy)
        -> case Integer
n of
             Integer
0  -> Term -> Maybe Machine
reduce (DataCon -> Type -> Term
mkVecNil DataCon
dc Type
aTy)
             Integer
n' | DC DataCon
snatDc [Either Term Type
_,Left Term
d'] <- Value
d
                , Evaluator
eval <- Step -> Unwind -> PrimStep -> PrimUnwind -> Evaluator
Evaluator Step
ghcStep Unwind
ghcUnwind PrimStep
ghcPrimStep PrimUnwind
ghcPrimUnwind
                , mach2 :: Machine
mach2@Machine{mStack :: Machine -> Stack
mStack=[],mTerm :: Machine -> Term
mTerm=Literal (NaturalLiteral Integer
d2)} <- Evaluator -> TyConMap -> Bool -> Machine -> Machine
whnf Evaluator
eval TyConMap
tcm Bool
isSubj (Term -> Machine -> Machine
setTerm Term
d' (Machine -> Machine) -> Machine -> Machine
forall a b. (a -> b) -> a -> b
$ Machine -> Machine
stackClear Machine
mach)
                -> case (Integer
d2 Integer -> Integer -> Integer
forall a. Integral a => a -> a -> a
`mod` Integer
n) of
                     Integer
0  -> Term -> Maybe Machine
reduce (Value -> Term
valToTerm Value
xs)
                     Integer
d3 -> let ([Either TyVar Type]
_,Type -> TypeView
tyView -> TyConApp TyConName
vecTcNm [Type]
_) = Type -> ([Either TyVar Type], Type)
splitFunForallTy Type
ty
                           in  Machine -> Term -> Maybe Machine
reduceWHNF' Machine
mach2 (Term -> Maybe Machine) -> Term -> Maybe Machine
forall a b. (a -> b) -> a -> b
$
                               Term -> [Either Term Type] -> Term
mkApps (PrimInfo -> Term
Prim PrimInfo
pInfo)
                                      [Type -> Either Term Type
forall a b. b -> Either a b
Right Type
nTy
                                      ,Type -> Either Term Type
forall a b. b -> Either a b
Right Type
aTy
                                      ,Type -> Either Term Type
forall a b. b -> Either a b
Right (LitTy -> Type
LitTy (Integer -> LitTy
NumTy (Integer
d3Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
-Integer
1)))
                                      ,Term -> Either Term Type
forall a b. a -> Either a b
Left (Value -> Term
valToTerm Value
kn)
                                      ,Term -> Either Term Type
forall a b. a -> Either a b
Left (HasCallStack => DataCon -> Type -> Integer -> Term -> Term -> Term
DataCon -> Type -> Integer -> Term -> Term -> Term
mkVecCons DataCon
dc Type
aTy Integer
n
                                              (Term -> [Either Term Type] -> Term
mkApps (TyConName -> Term
vecLastPrim TyConName
vecTcNm)
                                                      [Type -> Either Term Type
forall a b. b -> Either a b
Right (LitTy -> Type
LitTy (Integer -> LitTy
NumTy (Integer
n'Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
-Integer
1)))
                                                      ,Type -> Either Term Type
forall a b. b -> Either a b
Right Type
aTy
                                                      ,Term -> Either Term Type
forall a b. a -> Either a b
Left  (Value -> Term
valToTerm Value
xs)])
                                              (Term -> [Either Term Type] -> Term
mkApps (TyConName -> Term
vecInitPrim TyConName
vecTcNm)
                                                      [Type -> Either Term Type
forall a b. b -> Either a b
Right (LitTy -> Type
LitTy (Integer -> LitTy
NumTy (Integer
n'Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
-Integer
1)))
                                                      ,Type -> Either Term Type
forall a b. b -> Either a b
Right Type
aTy
                                                      ,Term -> Either Term Type
forall a b. a -> Either a b
Left (Value -> Term
valToTerm Value
xs)]))
                                      ,Term -> Either Term Type
forall a b. a -> Either a b
Left (Term -> [Either Term Type] -> Term
mkApps (DataCon -> Term
Data DataCon
snatDc)
                                                    [Type -> Either Term Type
forall a b. b -> Either a b
Right (LitTy -> Type
LitTy (Integer -> LitTy
NumTy (Integer
d3Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
-Integer
1)))
                                                    ,Term -> Either Term Type
forall a b. a -> Either a b
Left  (Literal -> Term
Literal (Integer -> Literal
NaturalLiteral (Integer
d3Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
-Integer
1)))])
                                      ]
             Integer
_  -> Maybe Machine
forall a. Maybe a
Nothing
      PrimStepContext
_ -> Maybe Machine
forall a. Maybe a
Nothing

-- Element-wise operations
-- - mapping
  , Text -> (PrimStepContext -> Maybe Machine) -> (Text, PrimStep)
primStepEntry $(textNameLit 'Clash.Sized.Vector.map) ((PrimStepContext -> Maybe Machine) -> (Text, PrimStep))
-> (PrimStepContext -> Maybe Machine) -> (Text, PrimStep)
forall a b. (a -> b) -> a -> b
$ \case
      PrimStepContext{Bool
[Type]
[Value]
Type
TyConMap
Machine
PrimInfo
Term -> Maybe Machine
Term -> Term
Type
-> Integer -> Integer -> (Natural -> Natural -> Natural) -> Term
Type -> Integer -> (Natural -> Natural) -> Term
Type -> [Integer] -> ([Natural] -> Term) -> Term
Machine -> Term -> Maybe Machine
tcm :: PrimStepContext -> TyConMap
isSubj :: PrimStepContext -> Bool
pInfo :: PrimStepContext -> PrimInfo
tys :: PrimStepContext -> [Type]
args :: PrimStepContext -> [Value]
mach :: PrimStepContext -> Machine
ty :: PrimStepContext -> Type
checkNaturalRange1 :: PrimStepContext -> Type -> Integer -> (Natural -> Natural) -> Term
checkNaturalRange2 :: PrimStepContext
-> Type
-> Integer
-> Integer
-> (Natural -> Natural -> Natural)
-> Term
checkNaturalRange :: PrimStepContext -> Type -> [Integer] -> ([Natural] -> Term) -> Term
reduce :: PrimStepContext -> Term -> Maybe Machine
reduceWith :: PrimStepContext -> Machine -> Term -> Maybe Machine
reduceWHNF :: PrimStepContext -> Term -> Maybe Machine
reduceWHNF' :: PrimStepContext -> Machine -> Term -> Maybe Machine
catchDivByZero :: PrimStepContext -> Term -> Term
catchErrorCall :: PrimStepContext -> Term -> Term
tcm :: TyConMap
isSubj :: Bool
pInfo :: PrimInfo
tys :: [Type]
args :: [Value]
mach :: Machine
ty :: Type
checkNaturalRange1 :: Type -> Integer -> (Natural -> Natural) -> Term
checkNaturalRange2 :: Type
-> Integer -> Integer -> (Natural -> Natural -> Natural) -> Term
checkNaturalRange :: Type -> [Integer] -> ([Natural] -> Term) -> Term
reduce :: Term -> Maybe Machine
reduceWith :: Machine -> Term -> Maybe Machine
reduceWHNF :: Term -> Maybe Machine
reduceWHNF' :: Machine -> Term -> Maybe Machine
catchDivByZero :: Term -> Term
catchErrorCall :: Term -> Term
..} -- :: (a -> b) -> Vec n a -> Vec n b
        | Bool
isSubj
        , DC DataCon
dc [Either Term Type]
vArgs <- [Value]
args [Value] -> Int -> Value
forall a. HasCallStack => [a] -> Int -> a
!! Int
1
        , Type
aTy : Type
bTy : Type
nTy : [Type]
_ <- [Type]
tys
        , Right Integer
n <- Except String Integer -> Either String Integer
forall e a. Except e a -> Either e a
runExcept (TyConMap -> Type -> Except String Integer
tyNatSize TyConMap
tcm Type
nTy)
        -> case Integer
n of
             Integer
0  -> Term -> Maybe Machine
reduce (DataCon -> Type -> Term
mkVecNil DataCon
dc Type
bTy)
             Integer
n' -> Term -> Maybe Machine
reduce (Term -> Maybe Machine) -> Term -> Maybe Machine
forall a b. (a -> b) -> a -> b
$
                   HasCallStack => DataCon -> Type -> Integer -> Term -> Term -> Term
DataCon -> Type -> Integer -> Term -> Term -> Term
mkVecCons DataCon
dc Type
bTy Integer
n'
                     (Term -> [Either Term Type] -> Term
mkApps (Value -> Term
valToTerm ([Value]
args [Value] -> Int -> Value
forall a. HasCallStack => [a] -> Int -> a
!! Int
0)) [Term -> Either Term Type
forall a b. a -> Either a b
Left ([Either Term Type] -> [Term]
forall a b. [Either a b] -> [a]
Either.lefts [Either Term Type]
vArgs [Term] -> Int -> Term
forall a. HasCallStack => [a] -> Int -> a
!! Int
1)])
                     (Term -> [Either Term Type] -> Term
mkApps (PrimInfo -> Term
Prim PrimInfo
pInfo)
                                          [Type -> Either Term Type
forall a b. b -> Either a b
Right Type
aTy
                                          ,Type -> Either Term Type
forall a b. b -> Either a b
Right Type
bTy
                                          ,Type -> Either Term Type
forall a b. b -> Either a b
Right (LitTy -> Type
LitTy (Integer -> LitTy
NumTy (Integer
n' Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
- Integer
1)))
                                          ,Term -> Either Term Type
forall a b. a -> Either a b
Left (Value -> Term
valToTerm ([Value]
args [Value] -> Int -> Value
forall a. HasCallStack => [a] -> Int -> a
!! Int
0))
                                          ,Term -> Either Term Type
forall a b. a -> Either a b
Left ([Either Term Type] -> [Term]
forall a b. [Either a b] -> [a]
Either.lefts [Either Term Type]
vArgs [Term] -> Int -> Term
forall a. HasCallStack => [a] -> Int -> a
!! Int
2)])
      PrimStepContext
_ -> Maybe Machine
forall a. Maybe a
Nothing

  , Text -> (PrimStepContext -> Maybe Machine) -> (Text, PrimStep)
primStepEntry $(textNameLit 'Clash.Sized.Vector.imap) ((PrimStepContext -> Maybe Machine) -> (Text, PrimStep))
-> (PrimStepContext -> Maybe Machine) -> (Text, PrimStep)
forall a b. (a -> b) -> a -> b
$ \case
      PrimStepContext{Bool
[Type]
[Value]
Type
TyConMap
Machine
PrimInfo
Term -> Maybe Machine
Term -> Term
Type
-> Integer -> Integer -> (Natural -> Natural -> Natural) -> Term
Type -> Integer -> (Natural -> Natural) -> Term
Type -> [Integer] -> ([Natural] -> Term) -> Term
Machine -> Term -> Maybe Machine
tcm :: PrimStepContext -> TyConMap
isSubj :: PrimStepContext -> Bool
pInfo :: PrimStepContext -> PrimInfo
tys :: PrimStepContext -> [Type]
args :: PrimStepContext -> [Value]
mach :: PrimStepContext -> Machine
ty :: PrimStepContext -> Type
checkNaturalRange1 :: PrimStepContext -> Type -> Integer -> (Natural -> Natural) -> Term
checkNaturalRange2 :: PrimStepContext
-> Type
-> Integer
-> Integer
-> (Natural -> Natural -> Natural)
-> Term
checkNaturalRange :: PrimStepContext -> Type -> [Integer] -> ([Natural] -> Term) -> Term
reduce :: PrimStepContext -> Term -> Maybe Machine
reduceWith :: PrimStepContext -> Machine -> Term -> Maybe Machine
reduceWHNF :: PrimStepContext -> Term -> Maybe Machine
reduceWHNF' :: PrimStepContext -> Machine -> Term -> Maybe Machine
catchDivByZero :: PrimStepContext -> Term -> Term
catchErrorCall :: PrimStepContext -> Term -> Term
tcm :: TyConMap
isSubj :: Bool
pInfo :: PrimInfo
tys :: [Type]
args :: [Value]
mach :: Machine
ty :: Type
checkNaturalRange1 :: Type -> Integer -> (Natural -> Natural) -> Term
checkNaturalRange2 :: Type
-> Integer -> Integer -> (Natural -> Natural -> Natural) -> Term
checkNaturalRange :: Type -> [Integer] -> ([Natural] -> Term) -> Term
reduce :: Term -> Maybe Machine
reduceWith :: Machine -> Term -> Maybe Machine
reduceWHNF :: Term -> Maybe Machine
reduceWHNF' :: Machine -> Term -> Maybe Machine
catchDivByZero :: Term -> Term
catchErrorCall :: Term -> Term
..} -- :: forall n a b . KnownNat n => (Index n -> a -> b) -> Vec n a -> Vec n b
        | Bool
isSubj
        , Type
nTy : Type
aTy : Type
bTy : [Type]
_ <- [Type]
tys
        , ([Either TyVar Type]
tyArgs,Type -> TypeView
tyView -> TyConApp TyConName
vecTcNm [Type]
_) <- Type -> ([Either TyVar Type], Type)
splitFunForallTy Type
ty
        , let ([Either TyVar Type]
tyArgs',Type
_) = Type -> ([Either TyVar Type], Type)
splitFunForallTy ([Either TyVar Type] -> [Type]
forall a b. [Either a b] -> [b]
Either.rights [Either TyVar Type]
tyArgs [Type] -> Int -> Type
forall a. HasCallStack => [a] -> Int -> a
!! Int
1)
        , TyConApp TyConName
indexTcNm [Type]
_ <- Type -> TypeView
tyView ([Either TyVar Type] -> [Type]
forall a b. [Either a b] -> [b]
Either.rights [Either TyVar Type]
tyArgs' [Type] -> Int -> Type
forall a. HasCallStack => [a] -> Int -> a
!! Int
0)
        , Right Integer
n <- Except String Integer -> Either String Integer
forall e a. Except e a -> Either e a
runExcept (TyConMap -> Type -> Except String Integer
tyNatSize TyConMap
tcm Type
nTy)
        , let iLit :: Term
iLit = Type -> Type -> Integer -> Integer -> Term
mkIndexLit ([Either TyVar Type] -> [Type]
forall a b. [Either a b] -> [b]
Either.rights [Either TyVar Type]
tyArgs' [Type] -> Int -> Type
forall a. HasCallStack => [a] -> Int -> a
!! Int
0) Type
nTy Integer
n Integer
0
        -> Term -> Maybe Machine
reduceWHNF (Term -> Maybe Machine) -> Term -> Maybe Machine
forall a b. (a -> b) -> a -> b
$
           Term -> [Either Term Type] -> Term
mkApps (PrimInfo -> Term
Prim (Text
-> Type -> WorkInfo -> IsMultiPrim -> PrimUnfolding -> PrimInfo
PrimInfo Text
"Clash.Sized.Vector.imap_go" (TyConName -> TyConName -> Type
vecImapGoTy TyConName
vecTcNm TyConName
indexTcNm) WorkInfo
WorkNever IsMultiPrim
SingleResult PrimUnfolding
NoUnfolding))
                  [Type -> Either Term Type
forall a b. b -> Either a b
Right Type
nTy
                  ,Type -> Either Term Type
forall a b. b -> Either a b
Right Type
nTy
                  ,Type -> Either Term Type
forall a b. b -> Either a b
Right Type
aTy
                  ,Type -> Either Term Type
forall a b. b -> Either a b
Right Type
bTy
                  ,Term -> Either Term Type
forall a b. a -> Either a b
Left (Value -> Term
valToTerm ([Value]
args [Value] -> Int -> Value
forall a. HasCallStack => [a] -> Int -> a
!! Int
1))
                  ,Term -> Either Term Type
forall a b. a -> Either a b
Left (Value -> Term
valToTerm ([Value]
args [Value] -> Int -> Value
forall a. HasCallStack => [a] -> Int -> a
!! Int
2))
                  ,Term -> Either Term Type
forall a b. a -> Either a b
Left Term
iLit
                  ]
      PrimStepContext
_ -> Maybe Machine
forall a. Maybe a
Nothing

  , Text -> (PrimStepContext -> Maybe Machine) -> (Text, PrimStep)
primStepEntry Text
"Clash.Sized.Vector.imap_go" ((PrimStepContext -> Maybe Machine) -> (Text, PrimStep))
-> (PrimStepContext -> Maybe Machine) -> (Text, PrimStep)
forall a b. (a -> b) -> a -> b
$ \case
      PrimStepContext{Bool
[Type]
[Value]
Type
TyConMap
Machine
PrimInfo
Term -> Maybe Machine
Term -> Term
Type
-> Integer -> Integer -> (Natural -> Natural -> Natural) -> Term
Type -> Integer -> (Natural -> Natural) -> Term
Type -> [Integer] -> ([Natural] -> Term) -> Term
Machine -> Term -> Maybe Machine
tcm :: PrimStepContext -> TyConMap
isSubj :: PrimStepContext -> Bool
pInfo :: PrimStepContext -> PrimInfo
tys :: PrimStepContext -> [Type]
args :: PrimStepContext -> [Value]
mach :: PrimStepContext -> Machine
ty :: PrimStepContext -> Type
checkNaturalRange1 :: PrimStepContext -> Type -> Integer -> (Natural -> Natural) -> Term
checkNaturalRange2 :: PrimStepContext
-> Type
-> Integer
-> Integer
-> (Natural -> Natural -> Natural)
-> Term
checkNaturalRange :: PrimStepContext -> Type -> [Integer] -> ([Natural] -> Term) -> Term
reduce :: PrimStepContext -> Term -> Maybe Machine
reduceWith :: PrimStepContext -> Machine -> Term -> Maybe Machine
reduceWHNF :: PrimStepContext -> Term -> Maybe Machine
reduceWHNF' :: PrimStepContext -> Machine -> Term -> Maybe Machine
catchDivByZero :: PrimStepContext -> Term -> Term
catchErrorCall :: PrimStepContext -> Term -> Term
tcm :: TyConMap
isSubj :: Bool
pInfo :: PrimInfo
tys :: [Type]
args :: [Value]
mach :: Machine
ty :: Type
checkNaturalRange1 :: Type -> Integer -> (Natural -> Natural) -> Term
checkNaturalRange2 :: Type
-> Integer -> Integer -> (Natural -> Natural -> Natural) -> Term
checkNaturalRange :: Type -> [Integer] -> ([Natural] -> Term) -> Term
reduce :: Term -> Maybe Machine
reduceWith :: Machine -> Term -> Maybe Machine
reduceWHNF :: Term -> Maybe Machine
reduceWHNF' :: Machine -> Term -> Maybe Machine
catchDivByZero :: Term -> Term
catchErrorCall :: Term -> Term
..}
        | Bool
isSubj
        , Type
nTy : Type
mTy : Type
aTy : Type
bTy : [Type]
_ <- [Type]
tys
        , Value
f : Value
xs : (Suspend Term
nArg) : [Value]
_ <- [Value]
args
        , DC DataCon
dc [Either Term Type]
vArgs <- Value
xs
        , Right Integer
n' <- Except String Integer -> Either String Integer
forall e a. Except e a -> Either e a
runExcept (TyConMap -> Type -> Except String Integer
tyNatSize TyConMap
tcm Type
nTy)
        , Right Integer
m <- Except String Integer -> Either String Integer
forall e a. Except e a -> Either e a
runExcept (TyConMap -> Type -> Except String Integer
tyNatSize TyConMap
tcm Type
mTy)
        -> case Integer
m of
             Integer
0  -> Term -> Maybe Machine
reduce (DataCon -> Type -> Term
mkVecNil DataCon
dc Type
bTy)
             Integer
m'
              | Evaluator
eval <- Step -> Unwind -> PrimStep -> PrimUnwind -> Evaluator
Evaluator Step
ghcStep Unwind
ghcUnwind PrimStep
ghcPrimStep PrimUnwind
ghcPrimUnwind
              , mach1 :: Machine
mach1@Machine{mStack :: Machine -> Stack
mStack=[],mTerm :: Machine -> Term
mTerm=Term
n} <-
                  Evaluator -> TyConMap -> Bool -> Machine -> Machine
whnf Evaluator
eval TyConMap
tcm Bool
True (Term -> Machine -> Machine
setTerm Term
nArg (Machine -> Machine
stackClear Machine
mach))
              ->  let ([Either TyVar Type]
tyArgs,Type
_) = Type -> ([Either TyVar Type], Type)
splitFunForallTy Type
ty
                      TyConApp TyConName
indexTcNm [Type]
_ = Type -> TypeView
tyView ([Either TyVar Type] -> [Type]
forall a b. [Either a b] -> [b]
Either.rights [Either TyVar Type]
tyArgs [Type] -> Int -> Type
forall a. HasCallStack => [a] -> Int -> a
!! Int
2)
                      iLit :: Term
iLit = Type -> Type -> Integer -> Integer -> Term
mkIndexLit ([Either TyVar Type] -> [Type]
forall a b. [Either a b] -> [b]
Either.rights [Either TyVar Type]
tyArgs [Type] -> Int -> Type
forall a. HasCallStack => [a] -> Int -> a
!! Int
2) Type
nTy Integer
n' Integer
1
                   in Machine -> Maybe Machine
forall a. a -> Maybe a
Just (Machine -> Maybe Machine) -> Machine -> Maybe Machine
forall a b. (a -> b) -> a -> b
$ (Term -> Machine -> Machine) -> Machine -> Term -> Machine
forall a b c. (a -> b -> c) -> b -> a -> c
flip Term -> Machine -> Machine
setTerm (Machine
mach1 {mStack = mStack mach}) (Term -> Machine) -> Term -> Machine
forall a b. (a -> b) -> a -> b
$ HasCallStack => DataCon -> Type -> Integer -> Term -> Term -> Term
DataCon -> Type -> Integer -> Term -> Term -> Term
mkVecCons DataCon
dc Type
bTy Integer
m'
                     (Term -> [Either Term Type] -> Term
mkApps (Value -> Term
valToTerm Value
f) [Term -> Either Term Type
forall a b. a -> Either a b
Left Term
n,Term -> Either Term Type
forall a b. a -> Either a b
Left ([Either Term Type] -> [Term]
forall a b. [Either a b] -> [a]
Either.lefts [Either Term Type]
vArgs [Term] -> Int -> Term
forall a. HasCallStack => [a] -> Int -> a
!! Int
1)])
                     (Term -> [Either Term Type] -> Term
mkApps (PrimInfo -> Term
Prim PrimInfo
pInfo)
                             [Type -> Either Term Type
forall a b. b -> Either a b
Right Type
nTy
                             ,Type -> Either Term Type
forall a b. b -> Either a b
Right (LitTy -> Type
LitTy (Integer -> LitTy
NumTy (Integer
m'Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
-Integer
1)))
                             ,Type -> Either Term Type
forall a b. b -> Either a b
Right Type
aTy
                             ,Type -> Either Term Type
forall a b. b -> Either a b
Right Type
bTy
                             ,Term -> Either Term Type
forall a b. a -> Either a b
Left (Value -> Term
valToTerm Value
f)
                             ,Term -> Either Term Type
forall a b. a -> Either a b
Left ([Either Term Type] -> [Term]
forall a b. [Either a b] -> [a]
Either.lefts [Either Term Type]
vArgs [Term] -> Int -> Term
forall a. HasCallStack => [a] -> Int -> a
!! Int
2)
                             ,Term -> Either Term Type
forall a b. a -> Either a b
Left (Term -> [Either Term Type] -> Term
mkApps (PrimInfo -> Term
Prim (Text
-> Type -> WorkInfo -> IsMultiPrim -> PrimUnfolding -> PrimInfo
PrimInfo (Name -> Text
forall a. Show a => a -> Text
showt '(Clash.Sized.Internal.Index.+#)) (TyConName -> Type
indexAddTy TyConName
indexTcNm) WorkInfo
WorkVariable IsMultiPrim
SingleResult PrimUnfolding
NoUnfolding))
                                           [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
n'))
                                           ,Term -> Either Term Type
forall a b. a -> Either a b
Left Term
n
                                           ,Term -> Either Term Type
forall a b. a -> Either a b
Left Term
iLit
                                           ])
                             ])
              | Bool
otherwise
              -> Maybe Machine
forall a. Maybe a
Nothing
      PrimStepContext
_ -> Maybe Machine
forall a. Maybe a
Nothing


  -- :: forall n a. KnownNat n => (a -> a) -> a -> Vec n a
  , Text -> (PrimStepContext -> Maybe Machine) -> (Text, PrimStep)
primStepEntry $(textNameLit 'Clash.Sized.Vector.iterateI) ((PrimStepContext -> Maybe Machine) -> (Text, PrimStep))
-> (PrimStepContext -> Maybe Machine) -> (Text, PrimStep)
forall a b. (a -> b) -> a -> b
$ \case
      PrimStepContext{Bool
[Type]
[Value]
Type
TyConMap
Machine
PrimInfo
Term -> Maybe Machine
Term -> Term
Type
-> Integer -> Integer -> (Natural -> Natural -> Natural) -> Term
Type -> Integer -> (Natural -> Natural) -> Term
Type -> [Integer] -> ([Natural] -> Term) -> Term
Machine -> Term -> Maybe Machine
tcm :: PrimStepContext -> TyConMap
isSubj :: PrimStepContext -> Bool
pInfo :: PrimStepContext -> PrimInfo
tys :: PrimStepContext -> [Type]
args :: PrimStepContext -> [Value]
mach :: PrimStepContext -> Machine
ty :: PrimStepContext -> Type
checkNaturalRange1 :: PrimStepContext -> Type -> Integer -> (Natural -> Natural) -> Term
checkNaturalRange2 :: PrimStepContext
-> Type
-> Integer
-> Integer
-> (Natural -> Natural -> Natural)
-> Term
checkNaturalRange :: PrimStepContext -> Type -> [Integer] -> ([Natural] -> Term) -> Term
reduce :: PrimStepContext -> Term -> Maybe Machine
reduceWith :: PrimStepContext -> Machine -> Term -> Maybe Machine
reduceWHNF :: PrimStepContext -> Term -> Maybe Machine
reduceWHNF' :: PrimStepContext -> Machine -> Term -> Maybe Machine
catchDivByZero :: PrimStepContext -> Term -> Term
catchErrorCall :: PrimStepContext -> Term -> Term
tcm :: TyConMap
isSubj :: Bool
pInfo :: PrimInfo
tys :: [Type]
args :: [Value]
mach :: Machine
ty :: Type
checkNaturalRange1 :: Type -> Integer -> (Natural -> Natural) -> Term
checkNaturalRange2 :: Type
-> Integer -> Integer -> (Natural -> Natural -> Natural) -> Term
checkNaturalRange :: Type -> [Integer] -> ([Natural] -> Term) -> Term
reduce :: Term -> Maybe Machine
reduceWith :: Machine -> Term -> Maybe Machine
reduceWHNF :: Term -> Maybe Machine
reduceWHNF' :: Machine -> Term -> Maybe Machine
catchDivByZero :: Term -> Term
catchErrorCall :: Term -> Term
..}
        | Bool
isSubj
        , [Type
nTy, Type
aTy] <- [Type]
tys
        , [Value
_n, Value
f, Value
a] <- [Value]
args
        , Right Integer
n <- Except String Integer -> Either String Integer
forall e a. Except e a -> Either e a
runExcept (TyConMap -> Type -> Except String Integer
tyNatSize TyConMap
tcm Type
nTy)
        ->
          let
            TyConApp TyConName
vecTcNm [Type]
_ = Type -> TypeView
tyView (TyConMap -> Type -> [Type] -> Type
getResultTy TyConMap
tcm Type
ty [Type]
tys)
            Just TyCon
vecTc = TyConName -> TyConMap -> Maybe TyCon
forall a b. Uniquable a => a -> UniqMap b -> Maybe b
UniqMap.lookup TyConName
vecTcNm TyConMap
tcm
            [DataCon
nilCon, DataCon
consCon] = TyCon -> [DataCon]
tyConDataCons TyCon
vecTc
          in case Integer
n of
             Integer
0 -> Term -> Maybe Machine
reduce (DataCon -> Type -> Term
mkVecNil DataCon
nilCon Type
aTy)
             Integer
_ -> Term -> Maybe Machine
reduce (Term -> Maybe Machine) -> Term -> Maybe Machine
forall a b. (a -> b) -> a -> b
$
              HasCallStack => DataCon -> Type -> Integer -> Term -> Term -> Term
DataCon -> Type -> Integer -> Term -> Term -> Term
mkVecCons DataCon
consCon Type
aTy Integer
n
                (Value -> Term
valToTerm Value
a)
                (Term -> [Either Term Type] -> Term
mkApps
                  (PrimInfo -> Term
Prim PrimInfo
pInfo)
                  [ Type -> Either Term Type
forall a b. b -> Either a b
Right (LitTy -> Type
LitTy (Integer -> LitTy
NumTy (Integer
n Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
- Integer
1)))
                  , Type -> Either Term Type
forall a b. b -> Either a b
Right Type
aTy
                  , Term -> Either Term Type
forall a b. a -> Either a b
Left (Value -> Term
valToTerm (Literal -> Value
Lit (Integer -> Literal
NaturalLiteral (Integer
n Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
- Integer
1))))
                  , Term -> Either Term Type
forall a b. a -> Either a b
Left (Value -> Term
valToTerm Value
f)
                  , Term -> Either Term Type
forall a b. a -> Either a b
Left (Term -> [Either Term Type] -> Term
mkApps (Value -> Term
valToTerm Value
f) [Term -> Either Term Type
forall a b. a -> Either a b
Left (Value -> Term
valToTerm Value
a)])
                  ])
      PrimStepContext
_ -> Maybe Machine
forall a. Maybe a
Nothing


-- - Zipping
  , Text -> (PrimStepContext -> Maybe Machine) -> (Text, PrimStep)
primStepEntry $(textNameLit 'Clash.Sized.Vector.zipWith) ((PrimStepContext -> Maybe Machine) -> (Text, PrimStep))
-> (PrimStepContext -> Maybe Machine) -> (Text, PrimStep)
forall a b. (a -> b) -> a -> b
$ \case
      PrimStepContext{Bool
[Type]
[Value]
Type
TyConMap
Machine
PrimInfo
Term -> Maybe Machine
Term -> Term
Type
-> Integer -> Integer -> (Natural -> Natural -> Natural) -> Term
Type -> Integer -> (Natural -> Natural) -> Term
Type -> [Integer] -> ([Natural] -> Term) -> Term
Machine -> Term -> Maybe Machine
tcm :: PrimStepContext -> TyConMap
isSubj :: PrimStepContext -> Bool
pInfo :: PrimStepContext -> PrimInfo
tys :: PrimStepContext -> [Type]
args :: PrimStepContext -> [Value]
mach :: PrimStepContext -> Machine
ty :: PrimStepContext -> Type
checkNaturalRange1 :: PrimStepContext -> Type -> Integer -> (Natural -> Natural) -> Term
checkNaturalRange2 :: PrimStepContext
-> Type
-> Integer
-> Integer
-> (Natural -> Natural -> Natural)
-> Term
checkNaturalRange :: PrimStepContext -> Type -> [Integer] -> ([Natural] -> Term) -> Term
reduce :: PrimStepContext -> Term -> Maybe Machine
reduceWith :: PrimStepContext -> Machine -> Term -> Maybe Machine
reduceWHNF :: PrimStepContext -> Term -> Maybe Machine
reduceWHNF' :: PrimStepContext -> Machine -> Term -> Maybe Machine
catchDivByZero :: PrimStepContext -> Term -> Term
catchErrorCall :: PrimStepContext -> Term -> Term
tcm :: TyConMap
isSubj :: Bool
pInfo :: PrimInfo
tys :: [Type]
args :: [Value]
mach :: Machine
ty :: Type
checkNaturalRange1 :: Type -> Integer -> (Natural -> Natural) -> Term
checkNaturalRange2 :: Type
-> Integer -> Integer -> (Natural -> Natural -> Natural) -> Term
checkNaturalRange :: Type -> [Integer] -> ([Natural] -> Term) -> Term
reduce :: Term -> Maybe Machine
reduceWith :: Machine -> Term -> Maybe Machine
reduceWHNF :: Term -> Maybe Machine
reduceWHNF' :: Machine -> Term -> Maybe Machine
catchDivByZero :: Term -> Term
catchErrorCall :: Term -> Term
..} -- :: (a -> b -> c) -> Vec n a -> Vec n b -> Vec n c
        | Bool
isSubj
        , Type
aTy : Type
bTy : Type
cTy : Type
nTy : [Type]
_ <- [Type]
tys
        , Value
f : Value
xs : Value
ys : [Value]
_   <- [Value]
args
        , DC DataCon
dc [Either Term Type]
vArgs <- Value
xs
        , ([Either TyVar Type]
_,Type -> TypeView
tyView -> TyConApp TyConName
vecTcNm [Type]
_) <- Type -> ([Either TyVar Type], Type)
splitFunForallTy Type
ty
        , Right Integer
n <- Except String Integer -> Either String Integer
forall e a. Except e a -> Either e a
runExcept (TyConMap -> Type -> Except String Integer
tyNatSize TyConMap
tcm Type
nTy)
        -> case Integer
n of
             Integer
0  -> Term -> Maybe Machine
reduce (DataCon -> Type -> Term
mkVecNil DataCon
dc Type
cTy)
             -- We share the function 'f' and the second vector 'ys' via heap
             -- let-bindings instead of inlining 'valToTerm f' / 'valToTerm ys'
             -- twice. See #3308.
             Integer
n' ->
               let (Machine
mach1, Id
fId)  = TyConMap -> Machine -> Term -> (Machine, Id)
newLetBinding TyConMap
tcm Machine
mach  (Value -> Term
valToTerm Value
f)
                   (Machine
mach2, Id
ysId) = TyConMap -> Machine -> Term -> (Machine, Id)
newLetBinding TyConMap
tcm Machine
mach1 (Value -> Term
valToTerm Value
ys)
               in Machine -> Term -> Maybe Machine
reduceWith Machine
mach2 (Term -> Maybe Machine) -> Term -> Maybe Machine
forall a b. (a -> b) -> a -> b
$ HasCallStack => DataCon -> Type -> Integer -> Term -> Term -> Term
DataCon -> Type -> Integer -> Term -> Term -> Term
mkVecCons DataCon
dc Type
cTy Integer
n'
                     (Term -> [Either Term Type] -> Term
mkApps (Id -> Term
Var Id
fId)
                                [Term -> Either Term Type
forall a b. a -> Either a b
Left ([Either Term Type] -> [Term]
forall a b. [Either a b] -> [a]
Either.lefts [Either Term Type]
vArgs [Term] -> Int -> Term
forall a. HasCallStack => [a] -> Int -> a
!! Int
1)
                                ,Term -> Either Term Type
forall a b. a -> Either a b
Left (Term -> [Either Term Type] -> Term
mkApps (TyConName -> Term
vecHeadPrim TyConName
vecTcNm)
                                        [Type -> Either Term Type
forall a b. b -> Either a b
Right (LitTy -> Type
LitTy (Integer -> LitTy
NumTy (Integer
n'Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
-Integer
1)))
                                        ,Type -> Either Term Type
forall a b. b -> Either a b
Right Type
bTy
                                        ,Term -> Either Term Type
forall a b. a -> Either a b
Left  (Id -> Term
Var Id
ysId)
                                        ])
                                ])
                     (Term -> [Either Term Type] -> Term
mkApps (PrimInfo -> Term
Prim PrimInfo
pInfo)
                                          [Type -> Either Term Type
forall a b. b -> Either a b
Right Type
aTy
                                          ,Type -> Either Term Type
forall a b. b -> Either a b
Right Type
bTy
                                          ,Type -> Either Term Type
forall a b. b -> Either a b
Right Type
cTy
                                          ,Type -> Either Term Type
forall a b. b -> Either a b
Right (LitTy -> Type
LitTy (Integer -> LitTy
NumTy (Integer
n' Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
- Integer
1)))
                                          ,Term -> Either Term Type
forall a b. a -> Either a b
Left (Id -> Term
Var Id
fId)
                                          ,Term -> Either Term Type
forall a b. a -> Either a b
Left ([Either Term Type] -> [Term]
forall a b. [Either a b] -> [a]
Either.lefts [Either Term Type]
vArgs [Term] -> Int -> Term
forall a. HasCallStack => [a] -> Int -> a
!! Int
2)
                                          ,Term -> Either Term Type
forall a b. a -> Either a b
Left (Term -> [Either Term Type] -> Term
mkApps (TyConName -> Term
vecTailPrim TyConName
vecTcNm)
                                                        [Type -> Either Term Type
forall a b. b -> Either a b
Right (LitTy -> Type
LitTy (Integer -> LitTy
NumTy (Integer
n'Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
-Integer
1)))
                                                        ,Type -> Either Term Type
forall a b. b -> Either a b
Right Type
bTy
                                                        ,Term -> Either Term Type
forall a b. a -> Either a b
Left (Id -> Term
Var Id
ysId)
                                                        ])])
      PrimStepContext
_ -> Maybe Machine
forall a. Maybe a
Nothing


-- Folding
  , Text -> (PrimStepContext -> Maybe Machine) -> (Text, PrimStep)
primStepEntry $(textNameLit 'Clash.Sized.Vector.foldr) ((PrimStepContext -> Maybe Machine) -> (Text, PrimStep))
-> (PrimStepContext -> Maybe Machine) -> (Text, PrimStep)
forall a b. (a -> b) -> a -> b
$ \case
      PrimStepContext{Bool
[Type]
[Value]
Type
TyConMap
Machine
PrimInfo
Term -> Maybe Machine
Term -> Term
Type
-> Integer -> Integer -> (Natural -> Natural -> Natural) -> Term
Type -> Integer -> (Natural -> Natural) -> Term
Type -> [Integer] -> ([Natural] -> Term) -> Term
Machine -> Term -> Maybe Machine
tcm :: PrimStepContext -> TyConMap
isSubj :: PrimStepContext -> Bool
pInfo :: PrimStepContext -> PrimInfo
tys :: PrimStepContext -> [Type]
args :: PrimStepContext -> [Value]
mach :: PrimStepContext -> Machine
ty :: PrimStepContext -> Type
checkNaturalRange1 :: PrimStepContext -> Type -> Integer -> (Natural -> Natural) -> Term
checkNaturalRange2 :: PrimStepContext
-> Type
-> Integer
-> Integer
-> (Natural -> Natural -> Natural)
-> Term
checkNaturalRange :: PrimStepContext -> Type -> [Integer] -> ([Natural] -> Term) -> Term
reduce :: PrimStepContext -> Term -> Maybe Machine
reduceWith :: PrimStepContext -> Machine -> Term -> Maybe Machine
reduceWHNF :: PrimStepContext -> Term -> Maybe Machine
reduceWHNF' :: PrimStepContext -> Machine -> Term -> Maybe Machine
catchDivByZero :: PrimStepContext -> Term -> Term
catchErrorCall :: PrimStepContext -> Term -> Term
tcm :: TyConMap
isSubj :: Bool
pInfo :: PrimInfo
tys :: [Type]
args :: [Value]
mach :: Machine
ty :: Type
checkNaturalRange1 :: Type -> Integer -> (Natural -> Natural) -> Term
checkNaturalRange2 :: Type
-> Integer -> Integer -> (Natural -> Natural -> Natural) -> Term
checkNaturalRange :: Type -> [Integer] -> ([Natural] -> Term) -> Term
reduce :: Term -> Maybe Machine
reduceWith :: Machine -> Term -> Maybe Machine
reduceWHNF :: Term -> Maybe Machine
reduceWHNF' :: Machine -> Term -> Maybe Machine
catchDivByZero :: Term -> Term
catchErrorCall :: Term -> Term
..} -- :: (a -> b -> b) -> b -> Vec n a -> b
        | Bool
isSubj
        , Type
aTy : Type
bTy : Type
nTy : [Type]
_ <- [Type]
tys
        , Value
f : Value
z : Value
xs : [Value]
_ <- [Value]
args
        , DC DataCon
_ [Either Term Type]
vArgs <- Value
xs
        , Right Integer
n <- Except String Integer -> Either String Integer
forall e a. Except e a -> Either e a
runExcept (TyConMap -> Type -> Except String Integer
tyNatSize TyConMap
tcm Type
nTy)
        -> case Integer
n of
             Integer
0 -> Term -> Maybe Machine
reduce (Value -> Term
valToTerm Value
z)
             Integer
_ -> Term -> Maybe Machine
reduceWHNF (Term -> Maybe Machine) -> Term -> Maybe Machine
forall a b. (a -> b) -> a -> b
$
                  Term -> [Either Term Type] -> Term
mkApps (Value -> Term
valToTerm Value
f)
                         [Term -> Either Term Type
forall a b. a -> Either a b
Left ([Either Term Type] -> [Term]
forall a b. [Either a b] -> [a]
Either.lefts [Either Term Type]
vArgs [Term] -> Int -> Term
forall a. HasCallStack => [a] -> Int -> a
!! Int
1)
                         ,Term -> Either Term Type
forall a b. a -> Either a b
Left (Term -> [Either Term Type] -> Term
mkApps (PrimInfo -> Term
Prim PrimInfo
pInfo)
                                       [Type -> Either Term Type
forall a b. b -> Either a b
Right Type
aTy
                                       ,Type -> Either Term Type
forall a b. b -> Either a b
Right Type
bTy
                                       ,Type -> Either Term Type
forall a b. b -> Either a b
Right (LitTy -> Type
LitTy (Integer -> LitTy
NumTy (Integer
nInteger -> Integer -> Integer
forall a. Num a => a -> a -> a
-Integer
1)))
                                       ,Term -> Either Term Type
forall a b. a -> Either a b
Left  (Value -> Term
valToTerm Value
f)
                                       ,Term -> Either Term Type
forall a b. a -> Either a b
Left  (Value -> Term
valToTerm Value
z)
                                       ,Term -> Either Term Type
forall a b. a -> Either a b
Left  ([Either Term Type] -> [Term]
forall a b. [Either a b] -> [a]
Either.lefts [Either Term Type]
vArgs [Term] -> Int -> Term
forall a. HasCallStack => [a] -> Int -> a
!! Int
2)
                                       ])
                         ]
      PrimStepContext
_ -> Maybe Machine
forall a. Maybe a
Nothing

  , Text -> (PrimStepContext -> Maybe Machine) -> (Text, PrimStep)
primStepEntry $(textNameLit 'Clash.Sized.Vector.fold) ((PrimStepContext -> Maybe Machine) -> (Text, PrimStep))
-> (PrimStepContext -> Maybe Machine) -> (Text, PrimStep)
forall a b. (a -> b) -> a -> b
$ \case
      PrimStepContext{Bool
[Type]
[Value]
Type
TyConMap
Machine
PrimInfo
Term -> Maybe Machine
Term -> Term
Type
-> Integer -> Integer -> (Natural -> Natural -> Natural) -> Term
Type -> Integer -> (Natural -> Natural) -> Term
Type -> [Integer] -> ([Natural] -> Term) -> Term
Machine -> Term -> Maybe Machine
tcm :: PrimStepContext -> TyConMap
isSubj :: PrimStepContext -> Bool
pInfo :: PrimStepContext -> PrimInfo
tys :: PrimStepContext -> [Type]
args :: PrimStepContext -> [Value]
mach :: PrimStepContext -> Machine
ty :: PrimStepContext -> Type
checkNaturalRange1 :: PrimStepContext -> Type -> Integer -> (Natural -> Natural) -> Term
checkNaturalRange2 :: PrimStepContext
-> Type
-> Integer
-> Integer
-> (Natural -> Natural -> Natural)
-> Term
checkNaturalRange :: PrimStepContext -> Type -> [Integer] -> ([Natural] -> Term) -> Term
reduce :: PrimStepContext -> Term -> Maybe Machine
reduceWith :: PrimStepContext -> Machine -> Term -> Maybe Machine
reduceWHNF :: PrimStepContext -> Term -> Maybe Machine
reduceWHNF' :: PrimStepContext -> Machine -> Term -> Maybe Machine
catchDivByZero :: PrimStepContext -> Term -> Term
catchErrorCall :: PrimStepContext -> Term -> Term
tcm :: TyConMap
isSubj :: Bool
pInfo :: PrimInfo
tys :: [Type]
args :: [Value]
mach :: Machine
ty :: Type
checkNaturalRange1 :: Type -> Integer -> (Natural -> Natural) -> Term
checkNaturalRange2 :: Type
-> Integer -> Integer -> (Natural -> Natural -> Natural) -> Term
checkNaturalRange :: Type -> [Integer] -> ([Natural] -> Term) -> Term
reduce :: Term -> Maybe Machine
reduceWith :: Machine -> Term -> Maybe Machine
reduceWHNF :: Term -> Maybe Machine
reduceWHNF' :: Machine -> Term -> Maybe Machine
catchDivByZero :: Term -> Term
catchErrorCall :: Term -> Term
..} -- :: (a -> a -> a) -> Vec (n + 1) a -> a
        | Bool
isSubj
        , Type
nTy : Type
aTy :  [Type]
_ <- [Type]
tys
        , Value
f : Value
vs : [Value]
_ <- [Value]
args
        , DC DataCon
_ [Either Term Type]
vArgs <- Value
vs
        , Right Integer
n <- Except String Integer -> Either String Integer
forall e a. Except e a -> Either e a
runExcept (TyConMap -> Type -> Except String Integer
tyNatSize TyConMap
tcm Type
nTy)
        -> case Integer
n of
             Integer
0 -> Term -> Maybe Machine
reduceWHNF ([Either Term Type] -> [Term]
forall a b. [Either a b] -> [a]
Either.lefts [Either Term Type]
vArgs [Term] -> Int -> Term
forall a. HasCallStack => [a] -> Int -> a
!! Int
1)
             Integer
_ -> let ([Either TyVar Type]
tyArgs,Type
_)         = Type -> ([Either TyVar Type], Type)
splitFunForallTy Type
ty
                      TyConApp TyConName
vecTcNm [Type]
_ = Type -> TypeView
tyView ([Either TyVar Type] -> [Type]
forall a b. [Either a b] -> [b]
Either.rights [Either TyVar Type]
tyArgs [Type] -> Int -> Type
forall a. HasCallStack => [a] -> Int -> a
!! Int
1)
                      tupTcNm :: TyConName
tupTcNm      = TyCon -> TyConName
ghcTyconToTyConName (Boxity -> Int -> TyCon
tupleTyCon Boxity
Boxed Int
2)
                      (Just TyCon
tupTc) = TyConName -> TyConMap -> Maybe TyCon
forall a b. Uniquable a => a -> UniqMap b -> Maybe b
UniqMap.lookup TyConName
tupTcNm TyConMap
tcm
                      [DataCon
tupDc]      = TyCon -> [DataCon]
tyConDataCons TyCon
tupTc
                      n' :: Integer
n'     = Integer
nInteger -> Integer -> Integer
forall a. Num a => a -> a -> a
+Integer
1
                      m :: Integer
m      = Integer
n' Integer -> Integer -> Integer
forall a. Integral a => a -> a -> a
`div` Integer
2
                      n1 :: Integer
n1     = Integer
n' Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
- Integer
m
                      mTy :: Type
mTy    = LitTy -> Type
LitTy (Integer -> LitTy
NumTy Integer
m)
                      m'ty :: Type
m'ty   = LitTy -> Type
LitTy (Integer -> LitTy
NumTy (Integer
mInteger -> Integer -> Integer
forall a. Num a => a -> a -> a
-Integer
1))
                      n1mTy :: Type
n1mTy  = LitTy -> Type
LitTy (Integer -> LitTy
NumTy Integer
n1)
                      n1m'ty :: Type
n1m'ty = LitTy -> Type
LitTy (Integer -> LitTy
NumTy (Integer
n1Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
-Integer
1))
                      splitAtCall :: Term
splitAtCall =
                       Term -> [Either Term Type] -> Term
mkApps (PrimInfo -> Term
Prim (Text
-> Type -> WorkInfo -> IsMultiPrim -> PrimUnfolding -> PrimInfo
PrimInfo Text
"Clash.Sized.Vector.fold_split" (TyConName -> Type
foldSplitAtTy TyConName
vecTcNm) WorkInfo
WorkNever IsMultiPrim
SingleResult PrimUnfolding
NoUnfolding))
                              [Type -> Either Term Type
forall a b. b -> Either a b
Right Type
mTy
                              ,Type -> Either Term Type
forall a b. b -> Either a b
Right Type
n1mTy
                              ,Type -> Either Term Type
forall a b. b -> Either a b
Right Type
aTy
                              ,Term -> Either Term Type
forall a b. a -> Either a b
Left (Literal -> Term
Literal (Integer -> Literal
NaturalLiteral Integer
m))
                              ,Term -> Either Term Type
forall a b. a -> Either a b
Left (Value -> Term
valToTerm Value
vs)
                              ]
                      mVecTy :: Type
mVecTy   = TyConName -> [Type] -> Type
mkTyConApp TyConName
vecTcNm [Type
mTy,Type
aTy]
                      n1mVecTy :: Type
n1mVecTy = TyConName -> [Type] -> Type
mkTyConApp TyConName
vecTcNm [Type
n1mTy,Type
aTy]
                      -- Guaranteed no capture, so okay to use unsafe name generation
                      asNm :: Name a
asNm     = Text -> Unique -> Name a
forall a. Text -> Unique -> Name a
mkUnsafeSystemName Text
"as" Unique
0
                      bsNm :: Name a
bsNm     = Text -> Unique -> Name a
forall a. Text -> Unique -> Name a
mkUnsafeSystemName Text
"bs" Unique
1
                      asId :: Id
asId     = Type -> TmName -> Id
mkLocalId Type
mVecTy TmName
forall {a}. Name a
asNm
                      bsId :: Id
bsId     = Type -> TmName -> Id
mkLocalId Type
n1mVecTy TmName
forall {a}. Name a
bsNm
                      tupPat :: Pat
tupPat   = DataCon -> [TyVar] -> [Id] -> Pat
DataPat DataCon
tupDc [] [Id
asId,Id
bsId]
                      asAlt :: (Pat, Term)
asAlt    = (Pat
tupPat, (Id -> Term
Var Id
asId))
                      bsAlt :: (Pat, Term)
bsAlt    = (Pat
tupPat, (Id -> Term
Var Id
bsId))
                  in  Term -> Maybe Machine
reduceWHNF (Term -> Maybe Machine) -> Term -> Maybe Machine
forall a b. (a -> b) -> a -> b
$
                      Term -> [Either Term Type] -> Term
mkApps (Value -> Term
valToTerm Value
f)
                             [Term -> Either Term Type
forall a b. a -> Either a b
Left (Term -> [Either Term Type] -> Term
mkApps (PrimInfo -> Term
Prim PrimInfo
pInfo)
                                           [Type -> Either Term Type
forall a b. b -> Either a b
Right Type
m'ty
                                           ,Type -> Either Term Type
forall a b. b -> Either a b
Right Type
aTy
                                           ,Term -> Either Term Type
forall a b. a -> Either a b
Left (Value -> Term
valToTerm Value
f)
                                           ,Term -> Either Term Type
forall a b. a -> Either a b
Left (Term -> Type -> [(Pat, Term)] -> Term
Case Term
splitAtCall Type
mVecTy [(Pat, Term)
asAlt])
                                           ])
                             ,Term -> Either Term Type
forall a b. a -> Either a b
Left (Term -> [Either Term Type] -> Term
mkApps (PrimInfo -> Term
Prim PrimInfo
pInfo)
                                           [Type -> Either Term Type
forall a b. b -> Either a b
Right Type
n1m'ty
                                           ,Type -> Either Term Type
forall a b. b -> Either a b
Right Type
aTy
                                           ,Term -> Either Term Type
forall a b. a -> Either a b
Left  (Value -> Term
valToTerm Value
f)
                                           ,Term -> Either Term Type
forall a b. a -> Either a b
Left  (Term -> Type -> [(Pat, Term)] -> Term
Case Term
splitAtCall Type
n1mVecTy [(Pat, Term)
bsAlt])
                                           ])
                             ]
      PrimStepContext
_ -> Maybe Machine
forall a. Maybe a
Nothing


  , Text -> (PrimStepContext -> Maybe Machine) -> (Text, PrimStep)
primStepEntry Text
"Clash.Sized.Vector.fold_split" ((PrimStepContext -> Maybe Machine) -> (Text, PrimStep))
-> (PrimStepContext -> Maybe Machine) -> (Text, PrimStep)
forall a b. (a -> b) -> a -> b
$ \case
      PrimStepContext{Bool
[Type]
[Value]
Type
TyConMap
Machine
PrimInfo
Term -> Maybe Machine
Term -> Term
Type
-> Integer -> Integer -> (Natural -> Natural -> Natural) -> Term
Type -> Integer -> (Natural -> Natural) -> Term
Type -> [Integer] -> ([Natural] -> Term) -> Term
Machine -> Term -> Maybe Machine
tcm :: PrimStepContext -> TyConMap
isSubj :: PrimStepContext -> Bool
pInfo :: PrimStepContext -> PrimInfo
tys :: PrimStepContext -> [Type]
args :: PrimStepContext -> [Value]
mach :: PrimStepContext -> Machine
ty :: PrimStepContext -> Type
checkNaturalRange1 :: PrimStepContext -> Type -> Integer -> (Natural -> Natural) -> Term
checkNaturalRange2 :: PrimStepContext
-> Type
-> Integer
-> Integer
-> (Natural -> Natural -> Natural)
-> Term
checkNaturalRange :: PrimStepContext -> Type -> [Integer] -> ([Natural] -> Term) -> Term
reduce :: PrimStepContext -> Term -> Maybe Machine
reduceWith :: PrimStepContext -> Machine -> Term -> Maybe Machine
reduceWHNF :: PrimStepContext -> Term -> Maybe Machine
reduceWHNF' :: PrimStepContext -> Machine -> Term -> Maybe Machine
catchDivByZero :: PrimStepContext -> Term -> Term
catchErrorCall :: PrimStepContext -> Term -> Term
tcm :: TyConMap
isSubj :: Bool
pInfo :: PrimInfo
tys :: [Type]
args :: [Value]
mach :: Machine
ty :: Type
checkNaturalRange1 :: Type -> Integer -> (Natural -> Natural) -> Term
checkNaturalRange2 :: Type
-> Integer -> Integer -> (Natural -> Natural -> Natural) -> Term
checkNaturalRange :: Type -> [Integer] -> ([Natural] -> Term) -> Term
reduce :: Term -> Maybe Machine
reduceWith :: Machine -> Term -> Maybe Machine
reduceWHNF :: Term -> Maybe Machine
reduceWHNF' :: Machine -> Term -> Maybe Machine
catchDivByZero :: Term -> Term
catchErrorCall :: Term -> Term
..} -- :: Natural -> Vec (m + n) a -> (Vec m a, Vec n a)
        | Bool
isSubj
        , Type
mTy : Type
nTy : Type
aTy : [Type]
_ <- [Type]
tys
        , Right Integer
m <- Except String Integer -> Either String Integer
forall e a. Except e a -> Either e a
runExcept (TyConMap -> Type -> Except String Integer
tyNatSize TyConMap
tcm Type
mTy)
        -> let -- Get the tuple data-constructor
               ty1 :: Type
ty1 = HasCallStack => TyConMap -> Type -> [Type] -> Type
TyConMap -> Type -> [Type] -> Type
piResultTys TyConMap
tcm Type
ty [Type]
tys
               ([Either TyVar Type]
_,Type -> TypeView
tyView -> TyConApp TyConName
tupTcNm tyArgs :: [Type]
tyArgs@(Type
tyArg:[Type]
_)) = Type -> ([Either TyVar Type], Type)
splitFunForallTy Type
ty1
               (Just TyCon
tupTc)       = TyConName -> TyConMap -> Maybe TyCon
forall a b. Uniquable a => a -> UniqMap b -> Maybe b
UniqMap.lookup TyConName
tupTcNm TyConMap
tcm
               [DataCon
tupDc]            = TyCon -> [DataCon]
tyConDataCons TyCon
tupTc
               -- Get the vector data-constructors
               TyConApp TyConName
vecTcNm [Type]
_ = Type -> TypeView
tyView Type
tyArg
               Just TyCon
vecTc         = TyConName -> TyConMap -> Maybe TyCon
forall a b. Uniquable a => a -> UniqMap b -> Maybe b
UniqMap.lookup TyConName
vecTcNm TyConMap
tcm
               [DataCon
nilCon,DataCon
consCon]   = TyCon -> [DataCon]
tyConDataCons TyCon
vecTc
               -- Recursive call to @splitAt@
               splitAtRec :: Term -> Term
splitAtRec Term
v =
                Term -> [Either Term Type] -> Term
mkApps (PrimInfo -> Term
Prim PrimInfo
pInfo)
                       [Type -> Either Term Type
forall a b. b -> Either a b
Right (LitTy -> Type
LitTy (Integer -> LitTy
NumTy (Integer
mInteger -> Integer -> Integer
forall a. Num a => a -> a -> a
-Integer
1)))
                       ,Type -> Either Term Type
forall a b. b -> Either a b
Right Type
nTy
                       ,Type -> Either Term Type
forall a b. b -> Either a b
Right Type
aTy
                       ,Term -> Either Term Type
forall a b. a -> Either a b
Left (Literal -> Term
Literal (Integer -> Literal
NaturalLiteral (Integer
mInteger -> Integer -> Integer
forall a. Num a => a -> a -> a
-Integer
1)))
                       ,Term -> Either Term Type
forall a b. a -> Either a b
Left Term
v
                       ]
               -- Projection either the first or second field of the recursive
               -- call to @splitAt@
               splitAtSelR :: Term -> Type -> [(Pat, Term)] -> Term
splitAtSelR Term
v = Term -> Type -> [(Pat, Term)] -> Term
Case (Term -> Term
splitAtRec Term
v)
               m1VecTy :: Type
m1VecTy = TyConName -> [Type] -> Type
mkTyConApp TyConName
vecTcNm [LitTy -> Type
LitTy (Integer -> LitTy
NumTy (Integer
mInteger -> Integer -> Integer
forall a. Num a => a -> a -> a
-Integer
1)),Type
aTy]
               nVecTy :: Type
nVecTy  = TyConName -> [Type] -> Type
mkTyConApp TyConName
vecTcNm [Type
nTy,Type
aTy]
               -- Guaranteed no capture, so okay to use unsafe name generation
               lNm :: Name a
lNm     = Text -> Unique -> Name a
forall a. Text -> Unique -> Name a
mkUnsafeSystemName Text
"l" Unique
0
               rNm :: Name a
rNm     = Text -> Unique -> Name a
forall a. Text -> Unique -> Name a
mkUnsafeSystemName Text
"r" Unique
1
               lId :: Id
lId     = Type -> TmName -> Id
mkLocalId Type
m1VecTy TmName
forall {a}. Name a
lNm
               rId :: Id
rId     = Type -> TmName -> Id
mkLocalId Type
nVecTy TmName
forall {a}. Name a
rNm
               tupPat :: Pat
tupPat  = DataCon -> [TyVar] -> [Id] -> Pat
DataPat DataCon
tupDc [] [Id
lId,Id
rId]
               lAlt :: (Pat, Term)
lAlt    = (Pat
tupPat, (Id -> Term
Var Id
lId))
               rAlt :: (Pat, Term)
rAlt    = (Pat
tupPat, (Id -> Term
Var Id
rId))
           in case Integer
m of
             -- (Nil,v)
             Integer
0 -> Term -> Maybe Machine
reduce (Term -> Maybe Machine) -> Term -> Maybe Machine
forall a b. (a -> b) -> a -> b
$
                  Term -> [Either Term Type] -> Term
mkApps (DataCon -> Term
Data DataCon
tupDc) ([Either Term Type] -> Term) -> [Either Term Type] -> Term
forall a b. (a -> b) -> a -> b
$ ((Type -> Either Term Type) -> [Type] -> [Either Term Type]
forall a b. (a -> b) -> [a] -> [b]
map Type -> Either Term Type
forall a b. b -> Either a b
Right [Type]
tyArgs) [Either Term Type] -> [Either Term Type] -> [Either Term Type]
forall a. [a] -> [a] -> [a]
++
                    [ Term -> Either Term Type
forall a b. a -> Either a b
Left (DataCon -> Type -> Term
mkVecNil DataCon
nilCon Type
aTy)
                    , Term -> Either Term Type
forall a b. a -> Either a b
Left (Value -> Term
valToTerm ([Value] -> Value
forall a. HasCallStack => [a] -> a
last [Value]
args))
                    ]
             -- (x:xs) <- v
             Integer
m' | DC DataCon
_ [Either Term Type]
vArgs <- [Value] -> Value
forall a. HasCallStack => [a] -> a
last [Value]
args
                -- (x:fst (splitAt (m-1) xs),snd (splitAt (m-1) xs))
                -> Term -> Maybe Machine
reduce (Term -> Maybe Machine) -> Term -> Maybe Machine
forall a b. (a -> b) -> a -> b
$
                   Term -> [Either Term Type] -> Term
mkApps (DataCon -> Term
Data DataCon
tupDc) ([Either Term Type] -> Term) -> [Either Term Type] -> Term
forall a b. (a -> b) -> a -> b
$ ((Type -> Either Term Type) -> [Type] -> [Either Term Type]
forall a b. (a -> b) -> [a] -> [b]
map Type -> Either Term Type
forall a b. b -> Either a b
Right [Type]
tyArgs) [Either Term Type] -> [Either Term Type] -> [Either Term Type]
forall a. [a] -> [a] -> [a]
++
                     [ Term -> Either Term Type
forall a b. a -> Either a b
Left (HasCallStack => DataCon -> Type -> Integer -> Term -> Term -> Term
DataCon -> Type -> Integer -> Term -> Term -> Term
mkVecCons DataCon
consCon Type
aTy Integer
m' ([Either Term Type] -> [Term]
forall a b. [Either a b] -> [a]
Either.lefts [Either Term Type]
vArgs [Term] -> Int -> Term
forall a. HasCallStack => [a] -> Int -> a
!! Int
1)
                               (Term -> Type -> [(Pat, Term)] -> Term
splitAtSelR ([Either Term Type] -> [Term]
forall a b. [Either a b] -> [a]
Either.lefts [Either Term Type]
vArgs [Term] -> Int -> Term
forall a. HasCallStack => [a] -> Int -> a
!! Int
2) Type
m1VecTy [(Pat, Term)
lAlt]))
                     , Term -> Either Term Type
forall a b. a -> Either a b
Left (Term -> Type -> [(Pat, Term)] -> Term
splitAtSelR ([Either Term Type] -> [Term]
forall a b. [Either a b] -> [a]
Either.lefts [Either Term Type]
vArgs [Term] -> Int -> Term
forall a. HasCallStack => [a] -> Int -> a
!! Int
2) Type
nVecTy [(Pat, Term)
rAlt])
                     ]
             -- v doesn't reduce to a data-constructor
             Integer
_  -> Maybe Machine
forall a. Maybe a
Nothing
      PrimStepContext
_ -> Maybe Machine
forall a. Maybe a
Nothing

-- - Specialised folds
  , Text -> (PrimStepContext -> Maybe Machine) -> (Text, PrimStep)
primStepEntry $(textNameLit 'Clash.Sized.Vector.dfold) ((PrimStepContext -> Maybe Machine) -> (Text, PrimStep))
-> (PrimStepContext -> Maybe Machine) -> (Text, PrimStep)
forall a b. (a -> b) -> a -> b
$ \case
      PrimStepContext{Bool
[Type]
[Value]
Type
TyConMap
Machine
PrimInfo
Term -> Maybe Machine
Term -> Term
Type
-> Integer -> Integer -> (Natural -> Natural -> Natural) -> Term
Type -> Integer -> (Natural -> Natural) -> Term
Type -> [Integer] -> ([Natural] -> Term) -> Term
Machine -> Term -> Maybe Machine
tcm :: PrimStepContext -> TyConMap
isSubj :: PrimStepContext -> Bool
pInfo :: PrimStepContext -> PrimInfo
tys :: PrimStepContext -> [Type]
args :: PrimStepContext -> [Value]
mach :: PrimStepContext -> Machine
ty :: PrimStepContext -> Type
checkNaturalRange1 :: PrimStepContext -> Type -> Integer -> (Natural -> Natural) -> Term
checkNaturalRange2 :: PrimStepContext
-> Type
-> Integer
-> Integer
-> (Natural -> Natural -> Natural)
-> Term
checkNaturalRange :: PrimStepContext -> Type -> [Integer] -> ([Natural] -> Term) -> Term
reduce :: PrimStepContext -> Term -> Maybe Machine
reduceWith :: PrimStepContext -> Machine -> Term -> Maybe Machine
reduceWHNF :: PrimStepContext -> Term -> Maybe Machine
reduceWHNF' :: PrimStepContext -> Machine -> Term -> Maybe Machine
catchDivByZero :: PrimStepContext -> Term -> Term
catchErrorCall :: PrimStepContext -> Term -> Term
tcm :: TyConMap
isSubj :: Bool
pInfo :: PrimInfo
tys :: [Type]
args :: [Value]
mach :: Machine
ty :: Type
checkNaturalRange1 :: Type -> Integer -> (Natural -> Natural) -> Term
checkNaturalRange2 :: Type
-> Integer -> Integer -> (Natural -> Natural -> Natural) -> Term
checkNaturalRange :: Type -> [Integer] -> ([Natural] -> Term) -> Term
reduce :: Term -> Maybe Machine
reduceWith :: Machine -> Term -> Maybe Machine
reduceWHNF :: Term -> Maybe Machine
reduceWHNF' :: Machine -> Term -> Maybe Machine
catchDivByZero :: Term -> Term
catchErrorCall :: Term -> Term
..}
        | Bool
isSubj
        , Type
pTy : Type
kTy : Type
aTy : [Type]
_ <- [Type]
tys
        , Value
_ : Value
p : Value
f : Value
z : Value
xs : [Value]
_ <- [Value]
args
        , DC DataCon
_ [Either Term Type]
vArgs <- Value
xs
        , Right Integer
k' <- Except String Integer -> Either String Integer
forall e a. Except e a -> Either e a
runExcept (TyConMap -> Type -> Except String Integer
tyNatSize TyConMap
tcm Type
kTy)
        -> case Integer
k'  of
             Integer
0 -> Term -> Maybe Machine
reduce (Value -> Term
valToTerm Value
z)
             Integer
_ -> let ([Either TyVar Type]
tyArgs,Type
_)  = Type -> ([Either TyVar Type], Type)
splitFunForallTy Type
ty
                      ([Either TyVar Type]
tyArgs',Type
_) = Type -> ([Either TyVar Type], Type)
splitFunForallTy ([Either TyVar Type] -> [Type]
forall a b. [Either a b] -> [b]
Either.rights [Either TyVar Type]
tyArgs [Type] -> Int -> Type
forall a. HasCallStack => [a] -> Int -> a
!! Int
2)
                      Just (TyVar
tvN, [TyVar]
_) = [TyVar] -> Maybe (TyVar, [TyVar])
forall a. [a] -> Maybe (a, [a])
List.uncons ([TyVar] -> Maybe (TyVar, [TyVar]))
-> [TyVar] -> Maybe (TyVar, [TyVar])
forall a b. (a -> b) -> a -> b
$ [Either TyVar Type] -> [TyVar]
forall a b. [Either a b] -> [a]
Either.lefts [Either TyVar Type]
tyArgs'
                      ubpT :: Type
ubpT = [Either TyVar Type] -> [Type]
forall a b. [Either a b] -> [b]
Either.rights [Either TyVar Type]
tyArgs' [Type] -> Int -> Type
forall a. HasCallStack => [a] -> Int -> a
!! Int
0
                      fTVs :: [TyVar]
fTVs = Getting (Endo [TyVar]) Type TyVar -> Type -> [TyVar]
forall a s. Getting (Endo [a]) s a -> s -> [a]
Lens.toListOf Getting (Endo [TyVar]) Type TyVar
Fold Type TyVar
typeFreeVars Type
ubpT
                      Just TyVar
tvK = (TyVar -> Bool) -> [TyVar] -> Maybe TyVar
forall (t :: Type -> Type) a.
Foldable t =>
(a -> Bool) -> t a -> Maybe a
List.find (TyVar -> TyVar -> Bool
forall a. Eq a => a -> a -> Bool
/= TyVar
tvN) [TyVar]
fTVs
                      subst0 :: Subst
subst0 = Subst -> TyVar -> Type -> Subst
extendTvSubst (InScopeSet -> Subst
mkSubst InScopeSet
is0) TyVar
tvN Type
k'ty
                      subst1 :: Subst
subst1 = Subst -> TyVar -> Type -> Subst
extendTvSubst Subst
subst0 TyVar
tvK (LitTy -> Type
LitTy (Integer -> LitTy
NumTy Integer
k'))
                      witness :: Type
witness = TyConMap -> Type -> Type
normalizeType TyConMap
tcm (HasCallStack => Subst -> Type -> Type
Subst -> Type -> Type
substTy Subst
subst1 Type
ubpT)
                      TyConApp TyConName
tupTcNm [Type]
_ = Type -> TypeView
tyView Type
witness
                      Just TyCon
witnessTc = TyConName -> TyConMap -> Maybe TyCon
forall a b. Uniquable a => a -> UniqMap b -> Maybe b
UniqMap.lookup TyConName
tupTcNm TyConMap
tcm
                      DataCon
ubp : [DataCon]
_ = TyCon -> [DataCon]
tyConDataCons TyCon
witnessTc
                      TyConApp TyConName
snatTcNm [Type]
_ = Type -> TypeView
tyView ([Either TyVar Type] -> [Type]
forall a b. [Either a b] -> [b]
Either.rights [Either TyVar Type]
tyArgs' [Type] -> Int -> Type
forall a. HasCallStack => [a] -> Int -> a
!! Int
1)
                      Just TyCon
snatTc = TyConName -> TyConMap -> Maybe TyCon
forall a b. Uniquable a => a -> UniqMap b -> Maybe b
UniqMap.lookup TyConName
snatTcNm TyConMap
tcm
                      [DataCon
snatDc]    = TyCon -> [DataCon]
tyConDataCons TyCon
snatTc
                      k'ty :: Type
k'ty        = LitTy -> Type
LitTy (Integer -> LitTy
NumTy (Integer
k'Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
-Integer
1))
                  in  Term -> Maybe Machine
reduceWHNF (Term -> Maybe Machine) -> Term -> Maybe Machine
forall a b. (a -> b) -> a -> b
$
                      Term -> [Either Term Type] -> Term
mkApps (Value -> Term
valToTerm Value
f)
                             [Type -> Either Term Type
forall a b. b -> Either a b
Right Type
k'ty
                             ,Term -> Either Term Type
forall a b. a -> Either a b
Left (DataCon -> Term
Data DataCon
ubp)
                             ,Term -> Either Term Type
forall a b. a -> Either a b
Left (Term -> [Either Term Type] -> Term
mkApps (DataCon -> Term
Data DataCon
snatDc)
                                           [Type -> Either Term Type
forall a b. b -> Either a b
Right Type
k'ty
                                           ,Term -> Either Term Type
forall a b. a -> Either a b
Left (Literal -> Term
Literal (Integer -> Literal
NaturalLiteral (Integer
k'Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
-Integer
1)))])
                             ,Term -> Either Term Type
forall a b. a -> Either a b
Left ([Either Term Type] -> [Term]
forall a b. [Either a b] -> [a]
Either.lefts [Either Term Type]
vArgs [Term] -> Int -> Term
forall a. HasCallStack => [a] -> Int -> a
!! Int
1)
                             ,Term -> Either Term Type
forall a b. a -> Either a b
Left (Term -> [Either Term Type] -> Term
mkApps (PrimInfo -> Term
Prim PrimInfo
pInfo)
                                           [Type -> Either Term Type
forall a b. b -> Either a b
Right Type
pTy
                                           ,Type -> Either Term Type
forall a b. b -> Either a b
Right Type
k'ty
                                           ,Type -> Either Term Type
forall a b. b -> Either a b
Right Type
aTy
                                           ,Term -> Either Term Type
forall a b. a -> Either a b
Left (Literal -> Term
Literal (Integer -> Literal
NaturalLiteral (Integer
k'Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
-Integer
1)))
                                           ,Term -> Either Term Type
forall a b. a -> Either a b
Left (Value -> Term
valToTerm Value
p)
                                           ,Term -> Either Term Type
forall a b. a -> Either a b
Left (Value -> Term
valToTerm Value
f)
                                           ,Term -> Either Term Type
forall a b. a -> Either a b
Left (Value -> Term
valToTerm Value
z)
                                           ,Term -> Either Term Type
forall a b. a -> Either a b
Left ([Either Term Type] -> [Term]
forall a b. [Either a b] -> [a]
Either.lefts [Either Term Type]
vArgs [Term] -> Int -> Term
forall a. HasCallStack => [a] -> Int -> a
!! Int
2)
                                           ])
                             ]
        where
          is0 :: InScopeSet
is0 = Machine -> InScopeSet
mScopeNames Machine
mach
      PrimStepContext
_ -> Maybe Machine
forall a. Maybe a
Nothing

  , Text -> (PrimStepContext -> Maybe Machine) -> (Text, PrimStep)
primStepEntry $(textNameLit 'Clash.Sized.Vector.dtfold) ((PrimStepContext -> Maybe Machine) -> (Text, PrimStep))
-> (PrimStepContext -> Maybe Machine) -> (Text, PrimStep)
forall a b. (a -> b) -> a -> b
$ \case
      PrimStepContext{Bool
[Type]
[Value]
Type
TyConMap
Machine
PrimInfo
Term -> Maybe Machine
Term -> Term
Type
-> Integer -> Integer -> (Natural -> Natural -> Natural) -> Term
Type -> Integer -> (Natural -> Natural) -> Term
Type -> [Integer] -> ([Natural] -> Term) -> Term
Machine -> Term -> Maybe Machine
tcm :: PrimStepContext -> TyConMap
isSubj :: PrimStepContext -> Bool
pInfo :: PrimStepContext -> PrimInfo
tys :: PrimStepContext -> [Type]
args :: PrimStepContext -> [Value]
mach :: PrimStepContext -> Machine
ty :: PrimStepContext -> Type
checkNaturalRange1 :: PrimStepContext -> Type -> Integer -> (Natural -> Natural) -> Term
checkNaturalRange2 :: PrimStepContext
-> Type
-> Integer
-> Integer
-> (Natural -> Natural -> Natural)
-> Term
checkNaturalRange :: PrimStepContext -> Type -> [Integer] -> ([Natural] -> Term) -> Term
reduce :: PrimStepContext -> Term -> Maybe Machine
reduceWith :: PrimStepContext -> Machine -> Term -> Maybe Machine
reduceWHNF :: PrimStepContext -> Term -> Maybe Machine
reduceWHNF' :: PrimStepContext -> Machine -> Term -> Maybe Machine
catchDivByZero :: PrimStepContext -> Term -> Term
catchErrorCall :: PrimStepContext -> Term -> Term
tcm :: TyConMap
isSubj :: Bool
pInfo :: PrimInfo
tys :: [Type]
args :: [Value]
mach :: Machine
ty :: Type
checkNaturalRange1 :: Type -> Integer -> (Natural -> Natural) -> Term
checkNaturalRange2 :: Type
-> Integer -> Integer -> (Natural -> Natural -> Natural) -> Term
checkNaturalRange :: Type -> [Integer] -> ([Natural] -> Term) -> Term
reduce :: Term -> Maybe Machine
reduceWith :: Machine -> Term -> Maybe Machine
reduceWHNF :: Term -> Maybe Machine
reduceWHNF' :: Machine -> Term -> Maybe Machine
catchDivByZero :: Term -> Term
catchErrorCall :: Term -> Term
..}
        | Bool
isSubj
        , Type
pTy : Type
kTy : Type
aTy : [Type]
_ <- [Type]
tys
        , Value
_ : Value
p : Value
f : Value
g : Value
xs : [Value]
_ <- [Value]
args
        , DC DataCon
_ [Either Term Type]
vArgs <- Value
xs
        , Right Integer
k' <- Except String Integer -> Either String Integer
forall e a. Except e a -> Either e a
runExcept (TyConMap -> Type -> Except String Integer
tyNatSize TyConMap
tcm Type
kTy)
        -> case Integer
k' of
             Integer
0 -> Term -> Maybe Machine
reduceWHNF (Term -> [Either Term Type] -> Term
mkApps (Value -> Term
valToTerm Value
f) [Term -> Either Term Type
forall a b. a -> Either a b
Left ([Either Term Type] -> [Term]
forall a b. [Either a b] -> [a]
Either.lefts [Either Term Type]
vArgs [Term] -> Int -> Term
forall a. HasCallStack => [a] -> Int -> a
!! Int
1)])
             Integer
_ -> let ([Either TyVar Type]
tyArgs,Type
_)  = Type -> ([Either TyVar Type], Type)
splitFunForallTy Type
ty
                      TyConApp TyConName
vecTcNm [Type]
_ = Type -> TypeView
tyView ([Either TyVar Type] -> [Type]
forall a b. [Either a b] -> [b]
Either.rights [Either TyVar Type]
tyArgs [Type] -> Int -> Type
forall a. HasCallStack => [a] -> Int -> a
!! Int
4)
                      ([Either TyVar Type]
tyArgs',Type
_) = Type -> ([Either TyVar Type], Type)
splitFunForallTy ([Either TyVar Type] -> [Type]
forall a b. [Either a b] -> [b]
Either.rights [Either TyVar Type]
tyArgs [Type] -> Int -> Type
forall a. HasCallStack => [a] -> Int -> a
!! Int
3)
                      TyConApp TyConName
snatTcNm [Type]
_ = Type -> TypeView
tyView ([Either TyVar Type] -> [Type]
forall a b. [Either a b] -> [b]
Either.rights [Either TyVar Type]
tyArgs' [Type] -> Int -> Type
forall a. HasCallStack => [a] -> Int -> a
!! Int
0)
                      Just TyCon
snatTc = TyConName -> TyConMap -> Maybe TyCon
forall a b. Uniquable a => a -> UniqMap b -> Maybe b
UniqMap.lookup TyConName
snatTcNm TyConMap
tcm
                      [DataCon
snatDc]    = TyCon -> [DataCon]
tyConDataCons TyCon
snatTc
                      tupTcNm :: TyConName
tupTcNm     = TyCon -> TyConName
ghcTyconToTyConName (Boxity -> Int -> TyCon
tupleTyCon Boxity
Boxed Int
2)
                      (Just TyCon
tupTc) = TyConName -> TyConMap -> Maybe TyCon
forall a b. Uniquable a => a -> UniqMap b -> Maybe b
UniqMap.lookup TyConName
tupTcNm TyConMap
tcm
                      [DataCon
tupDc]     = TyCon -> [DataCon]
tyConDataCons TyCon
tupTc
                      k'ty :: Type
k'ty        = LitTy -> Type
LitTy (Integer -> LitTy
NumTy (Integer
k'Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
-Integer
1))
                      k2ty :: Type
k2ty        = LitTy -> Type
LitTy (Integer -> LitTy
NumTy (Integer
2Integer -> Integer -> Integer
forall a b. (Num a, Integral b) => a -> b -> a
^(Integer
k'Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
-Integer
1)))
                      splitAtCall :: Term
splitAtCall =
                       Term -> [Either Term Type] -> Term
mkApps (TyConName -> TyConName -> Term
splitAtPrim TyConName
snatTcNm TyConName
vecTcNm)
                              [Type -> Either Term Type
forall a b. b -> Either a b
Right Type
k2ty
                              ,Type -> Either Term Type
forall a b. b -> Either a b
Right Type
k2ty
                              ,Type -> Either Term Type
forall a b. b -> Either a b
Right Type
aTy
                              ,Term -> Either Term Type
forall a b. a -> Either a b
Left (Term -> [Either Term Type] -> Term
mkApps (DataCon -> Term
Data DataCon
snatDc)
                                            [Type -> Either Term Type
forall a b. b -> Either a b
Right Type
k2ty
                                            ,Term -> Either Term Type
forall a b. a -> Either a b
Left (Literal -> Term
Literal (Integer -> Literal
NaturalLiteral (Integer
2Integer -> Integer -> Integer
forall a b. (Num a, Integral b) => a -> b -> a
^(Integer
k'Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
-Integer
1))))])
                              ,Term -> Either Term Type
forall a b. a -> Either a b
Left (Value -> Term
valToTerm Value
xs)
                              ]
                      xsSVecTy :: Type
xsSVecTy = TyConName -> [Type] -> Type
mkTyConApp TyConName
vecTcNm [Type
k2ty,Type
aTy]
                      -- Guaranteed no capture, so okay to use unsafe name generation
                      xsLNm :: Name a
xsLNm    = Text -> Unique -> Name a
forall a. Text -> Unique -> Name a
mkUnsafeSystemName Text
"xsL" Unique
0
                      xsRNm :: Name a
xsRNm    = Text -> Unique -> Name a
forall a. Text -> Unique -> Name a
mkUnsafeSystemName Text
"xsR" Unique
1
                      xsLId :: Id
xsLId    = Type -> TmName -> Id
mkLocalId Type
k2ty TmName
forall {a}. Name a
xsLNm
                      xsRId :: Id
xsRId    = Type -> TmName -> Id
mkLocalId Type
k2ty TmName
forall {a}. Name a
xsRNm
                      tupPat :: Pat
tupPat   = DataCon -> [TyVar] -> [Id] -> Pat
DataPat DataCon
tupDc [] [Id
xsLId,Id
xsRId]
                      asAlt :: (Pat, Term)
asAlt    = (Pat
tupPat, (Id -> Term
Var Id
xsLId))
                      bsAlt :: (Pat, Term)
bsAlt    = (Pat
tupPat, (Id -> Term
Var Id
xsRId))
                  in  Term -> Maybe Machine
reduceWHNF (Term -> Maybe Machine) -> Term -> Maybe Machine
forall a b. (a -> b) -> a -> b
$
                      Term -> [Either Term Type] -> Term
mkApps (Value -> Term
valToTerm Value
g)
                             [Type -> Either Term Type
forall a b. b -> Either a b
Right Type
k'ty
                             ,Term -> Either Term Type
forall a b. a -> Either a b
Left (Term -> [Either Term Type] -> Term
mkApps (DataCon -> Term
Data DataCon
snatDc)
                                           [Type -> Either Term Type
forall a b. b -> Either a b
Right Type
k'ty
                                           ,Term -> Either Term Type
forall a b. a -> Either a b
Left (Literal -> Term
Literal (Integer -> Literal
NaturalLiteral (Integer
k'Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
-Integer
1)))])
                             ,Term -> Either Term Type
forall a b. a -> Either a b
Left (Term -> [Either Term Type] -> Term
mkApps (PrimInfo -> Term
Prim PrimInfo
pInfo)
                                           [Type -> Either Term Type
forall a b. b -> Either a b
Right Type
pTy
                                           ,Type -> Either Term Type
forall a b. b -> Either a b
Right Type
k'ty
                                           ,Type -> Either Term Type
forall a b. b -> Either a b
Right Type
aTy
                                           ,Term -> Either Term Type
forall a b. a -> Either a b
Left (Literal -> Term
Literal (Integer -> Literal
NaturalLiteral (Integer
k'Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
-Integer
1)))
                                           ,Term -> Either Term Type
forall a b. a -> Either a b
Left (Value -> Term
valToTerm Value
p)
                                           ,Term -> Either Term Type
forall a b. a -> Either a b
Left (Value -> Term
valToTerm Value
f)
                                           ,Term -> Either Term Type
forall a b. a -> Either a b
Left (Value -> Term
valToTerm Value
g)
                                           ,Term -> Either Term Type
forall a b. a -> Either a b
Left (Term -> Type -> [(Pat, Term)] -> Term
Case Term
splitAtCall Type
xsSVecTy [(Pat, Term)
asAlt])])
                             ,Term -> Either Term Type
forall a b. a -> Either a b
Left (Term -> [Either Term Type] -> Term
mkApps (PrimInfo -> Term
Prim PrimInfo
pInfo)
                                           [Type -> Either Term Type
forall a b. b -> Either a b
Right Type
pTy
                                           ,Type -> Either Term Type
forall a b. b -> Either a b
Right Type
k'ty
                                           ,Type -> Either Term Type
forall a b. b -> Either a b
Right Type
aTy
                                           ,Term -> Either Term Type
forall a b. a -> Either a b
Left (Literal -> Term
Literal (Integer -> Literal
NaturalLiteral (Integer
k'Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
-Integer
1)))
                                           ,Term -> Either Term Type
forall a b. a -> Either a b
Left (Value -> Term
valToTerm Value
p)
                                           ,Term -> Either Term Type
forall a b. a -> Either a b
Left (Value -> Term
valToTerm Value
f)
                                           ,Term -> Either Term Type
forall a b. a -> Either a b
Left (Value -> Term
valToTerm Value
g)
                                           ,Term -> Either Term Type
forall a b. a -> Either a b
Left (Term -> Type -> [(Pat, Term)] -> Term
Case Term
splitAtCall Type
xsSVecTy [(Pat, Term)
bsAlt])])
                             ]
      PrimStepContext
_ -> Maybe Machine
forall a. Maybe a
Nothing

-- Misc
  , Text -> (PrimStepContext -> Maybe Machine) -> (Text, PrimStep)
primStepEntry $(textNameLit 'Clash.Sized.Vector.lazyV) ((PrimStepContext -> Maybe Machine) -> (Text, PrimStep))
-> (PrimStepContext -> Maybe Machine) -> (Text, PrimStep)
forall a b. (a -> b) -> a -> b
$ \case
      PrimStepContext{Bool
[Type]
[Value]
Type
TyConMap
Machine
PrimInfo
Term -> Maybe Machine
Term -> Term
Type
-> Integer -> Integer -> (Natural -> Natural -> Natural) -> Term
Type -> Integer -> (Natural -> Natural) -> Term
Type -> [Integer] -> ([Natural] -> Term) -> Term
Machine -> Term -> Maybe Machine
tcm :: PrimStepContext -> TyConMap
isSubj :: PrimStepContext -> Bool
pInfo :: PrimStepContext -> PrimInfo
tys :: PrimStepContext -> [Type]
args :: PrimStepContext -> [Value]
mach :: PrimStepContext -> Machine
ty :: PrimStepContext -> Type
checkNaturalRange1 :: PrimStepContext -> Type -> Integer -> (Natural -> Natural) -> Term
checkNaturalRange2 :: PrimStepContext
-> Type
-> Integer
-> Integer
-> (Natural -> Natural -> Natural)
-> Term
checkNaturalRange :: PrimStepContext -> Type -> [Integer] -> ([Natural] -> Term) -> Term
reduce :: PrimStepContext -> Term -> Maybe Machine
reduceWith :: PrimStepContext -> Machine -> Term -> Maybe Machine
reduceWHNF :: PrimStepContext -> Term -> Maybe Machine
reduceWHNF' :: PrimStepContext -> Machine -> Term -> Maybe Machine
catchDivByZero :: PrimStepContext -> Term -> Term
catchErrorCall :: PrimStepContext -> Term -> Term
tcm :: TyConMap
isSubj :: Bool
pInfo :: PrimInfo
tys :: [Type]
args :: [Value]
mach :: Machine
ty :: Type
checkNaturalRange1 :: Type -> Integer -> (Natural -> Natural) -> Term
checkNaturalRange2 :: Type
-> Integer -> Integer -> (Natural -> Natural -> Natural) -> Term
checkNaturalRange :: Type -> [Integer] -> ([Natural] -> Term) -> Term
reduce :: Term -> Maybe Machine
reduceWith :: Machine -> Term -> Maybe Machine
reduceWHNF :: Term -> Maybe Machine
reduceWHNF' :: Machine -> Term -> Maybe Machine
catchDivByZero :: Term -> Term
catchErrorCall :: Term -> Term
..}
        | Bool
isSubj
        , Type
nTy : Type
aTy : [Type]
_ <- [Type]
tys
        , Value
_ : Value
xs : [Value]
_ <- [Value]
args
        , ([Either TyVar Type]
_,Type -> TypeView
tyView -> TyConApp TyConName
vecTcNm [Type]
_) <- Type -> ([Either TyVar Type], Type)
splitFunForallTy Type
ty
        , Right Integer
n <- Except String Integer -> Either String Integer
forall e a. Except e a -> Either e a
runExcept (TyConMap -> Type -> Except String Integer
tyNatSize TyConMap
tcm Type
nTy)
        -> case Integer
n of
             Integer
0  -> let (Just TyCon
vecTc) = TyConName -> TyConMap -> Maybe TyCon
forall a b. Uniquable a => a -> UniqMap b -> Maybe b
UniqMap.lookup TyConName
vecTcNm TyConMap
tcm
                       [DataCon
nilCon,DataCon
_]   = TyCon -> [DataCon]
tyConDataCons TyCon
vecTc
                   in  Term -> Maybe Machine
reduce (DataCon -> Type -> Term
mkVecNil DataCon
nilCon Type
aTy)
             Integer
n' -> let (Just TyCon
vecTc) = TyConName -> TyConMap -> Maybe TyCon
forall a b. Uniquable a => a -> UniqMap b -> Maybe b
UniqMap.lookup TyConName
vecTcNm TyConMap
tcm
                       [DataCon
_,DataCon
consCon]  = TyCon -> [DataCon]
tyConDataCons TyCon
vecTc
                   in  Term -> Maybe Machine
reduce (Term -> Maybe Machine) -> Term -> Maybe Machine
forall a b. (a -> b) -> a -> b
$ HasCallStack => DataCon -> Type -> Integer -> Term -> Term -> Term
DataCon -> Type -> Integer -> Term -> Term -> Term
mkVecCons DataCon
consCon Type
aTy Integer
n'
                         (Term -> [Either Term Type] -> Term
mkApps (TyConName -> Term
vecHeadPrim TyConName
vecTcNm)
                                 [ Type -> Either Term Type
forall a b. b -> Either a b
Right (LitTy -> Type
LitTy (Integer -> LitTy
NumTy (Integer
n' Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
- Integer
1)))
                                 , Type -> Either Term Type
forall a b. b -> Either a b
Right Type
aTy
                                 , Term -> Either Term Type
forall a b. a -> Either a b
Left  (Value -> Term
valToTerm Value
xs)
                                 ])
                         (Term -> [Either Term Type] -> Term
mkApps (PrimInfo -> Term
Prim PrimInfo
pInfo)
                                 [ Type -> Either Term Type
forall a b. b -> Either a b
Right (LitTy -> Type
LitTy (Integer -> LitTy
NumTy (Integer
n' Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
- Integer
1)))
                                 , Type -> Either Term Type
forall a b. b -> Either a b
Right Type
aTy
                                 , Term -> Either Term Type
forall a b. a -> Either a b
Left  (Literal -> Term
Literal (Integer -> Literal
NaturalLiteral (Integer
n'Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
-Integer
1)))
                                 , Term -> Either Term Type
forall a b. a -> Either a b
Left  (Term -> [Either Term Type] -> Term
mkApps (TyConName -> Term
vecTailPrim TyConName
vecTcNm)
                                                 [ Type -> Either Term Type
forall a b. b -> Either a b
Right (LitTy -> Type
LitTy (Integer -> LitTy
NumTy (Integer
n'Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
-Integer
1)))
                                                 , Type -> Either Term Type
forall a b. b -> Either a b
Right Type
aTy
                                                 , Term -> Either Term Type
forall a b. a -> Either a b
Left  (Value -> Term
valToTerm Value
xs)
                                                 ])
                                 ])
      PrimStepContext
_ -> Maybe Machine
forall a. Maybe a
Nothing

-- Traversable
  , Text -> (PrimStepContext -> Maybe Machine) -> (Text, PrimStep)
primStepEntry $(textNameLit 'Clash.Sized.Vector.traverse#) ((PrimStepContext -> Maybe Machine) -> (Text, PrimStep))
-> (PrimStepContext -> Maybe Machine) -> (Text, PrimStep)
forall a b. (a -> b) -> a -> b
$ \case
      PrimStepContext{Bool
[Type]
[Value]
Type
TyConMap
Machine
PrimInfo
Term -> Maybe Machine
Term -> Term
Type
-> Integer -> Integer -> (Natural -> Natural -> Natural) -> Term
Type -> Integer -> (Natural -> Natural) -> Term
Type -> [Integer] -> ([Natural] -> Term) -> Term
Machine -> Term -> Maybe Machine
tcm :: PrimStepContext -> TyConMap
isSubj :: PrimStepContext -> Bool
pInfo :: PrimStepContext -> PrimInfo
tys :: PrimStepContext -> [Type]
args :: PrimStepContext -> [Value]
mach :: PrimStepContext -> Machine
ty :: PrimStepContext -> Type
checkNaturalRange1 :: PrimStepContext -> Type -> Integer -> (Natural -> Natural) -> Term
checkNaturalRange2 :: PrimStepContext
-> Type
-> Integer
-> Integer
-> (Natural -> Natural -> Natural)
-> Term
checkNaturalRange :: PrimStepContext -> Type -> [Integer] -> ([Natural] -> Term) -> Term
reduce :: PrimStepContext -> Term -> Maybe Machine
reduceWith :: PrimStepContext -> Machine -> Term -> Maybe Machine
reduceWHNF :: PrimStepContext -> Term -> Maybe Machine
reduceWHNF' :: PrimStepContext -> Machine -> Term -> Maybe Machine
catchDivByZero :: PrimStepContext -> Term -> Term
catchErrorCall :: PrimStepContext -> Term -> Term
tcm :: TyConMap
isSubj :: Bool
pInfo :: PrimInfo
tys :: [Type]
args :: [Value]
mach :: Machine
ty :: Type
checkNaturalRange1 :: Type -> Integer -> (Natural -> Natural) -> Term
checkNaturalRange2 :: Type
-> Integer -> Integer -> (Natural -> Natural -> Natural) -> Term
checkNaturalRange :: Type -> [Integer] -> ([Natural] -> Term) -> Term
reduce :: Term -> Maybe Machine
reduceWith :: Machine -> Term -> Maybe Machine
reduceWHNF :: Term -> Maybe Machine
reduceWHNF' :: Machine -> Term -> Maybe Machine
catchDivByZero :: Term -> Term
catchErrorCall :: Term -> Term
..}
        | Bool
isSubj
        , Type
aTy : Type
fTy : Type
bTy : Type
nTy : [Type]
_ <- [Type]
tys
        , Value
apDict : Value
f : Value
xs : [Value]
_ <- [Value]
args
        , DC DataCon
dc [Either Term Type]
vArgs <- Value
xs
        , Right Integer
n <- Except String Integer -> Either String Integer
forall e a. Except e a -> Either e a
runExcept (TyConMap -> Type -> Except String Integer
tyNatSize TyConMap
tcm Type
nTy)
        -> case Integer
n of
             Integer
0 -> let (Term
pureF,Supply
ids') = PrimEvalMonad Term -> Supply -> (Term, Supply)
forall a. PrimEvalMonad a -> Supply -> (a, Supply)
runPEM (String
-> InScopeSet
-> TyConMap
-> Term
-> Int
-> Int
-> PrimEvalMonad Term
forall (m :: Type -> Type).
(HasCallStack, MonadUnique m) =>
String -> InScopeSet -> TyConMap -> Term -> Int -> Int -> m Term
mkSelectorCase $(curLoc) InScopeSet
is0 TyConMap
tcm (Value -> Term
valToTerm Value
apDict) Int
1 Int
1) Supply
ids
                  in  Machine -> Term -> Maybe Machine
reduceWHNF' (Machine
mach { mSupply = ids' }) (Term -> Maybe Machine) -> Term -> Maybe Machine
forall a b. (a -> b) -> a -> b
$
                      Term -> [Either Term Type] -> Term
mkApps Term
pureF
                             [Type -> Either Term Type
forall a b. b -> Either a b
Right (TyConName -> [Type] -> Type
mkTyConApp (TyConName
vecTcNm) [Type
nTy,Type
bTy])
                             ,Term -> Either Term Type
forall a b. a -> Either a b
Left  (DataCon -> Type -> Term
mkVecNil DataCon
dc Type
bTy)]
             Integer
_ -> let ((Term
fmapF,Term
apF),Supply
ids') = (PrimEvalMonad (Term, Term) -> Supply -> ((Term, Term), Supply))
-> Supply -> PrimEvalMonad (Term, Term) -> ((Term, Term), Supply)
forall a b c. (a -> b -> c) -> b -> a -> c
flip PrimEvalMonad (Term, Term) -> Supply -> ((Term, Term), Supply)
forall a. PrimEvalMonad a -> Supply -> (a, Supply)
runPEM Supply
ids (PrimEvalMonad (Term, Term) -> ((Term, Term), Supply))
-> PrimEvalMonad (Term, Term) -> ((Term, Term), Supply)
forall a b. (a -> b) -> a -> b
$ do
                        Term
fDict  <- String
-> InScopeSet
-> TyConMap
-> Term
-> Int
-> Int
-> PrimEvalMonad Term
forall (m :: Type -> Type).
(HasCallStack, MonadUnique m) =>
String -> InScopeSet -> TyConMap -> Term -> Int -> Int -> m Term
mkSelectorCase $(curLoc) InScopeSet
is0 TyConMap
tcm (Value -> Term
valToTerm Value
apDict) Int
1 Int
0
                        Term
fmapF' <- String
-> InScopeSet
-> TyConMap
-> Term
-> Int
-> Int
-> PrimEvalMonad Term
forall (m :: Type -> Type).
(HasCallStack, MonadUnique m) =>
String -> InScopeSet -> TyConMap -> Term -> Int -> Int -> m Term
mkSelectorCase $(curLoc) InScopeSet
is0 TyConMap
tcm Term
fDict Int
1 Int
0
                        Term
apF'   <- String
-> InScopeSet
-> TyConMap
-> Term
-> Int
-> Int
-> PrimEvalMonad Term
forall (m :: Type -> Type).
(HasCallStack, MonadUnique m) =>
String -> InScopeSet -> TyConMap -> Term -> Int -> Int -> m Term
mkSelectorCase $(curLoc) InScopeSet
is0 TyConMap
tcm (Value -> Term
valToTerm Value
apDict) Int
1 Int
2
                        (Term, Term) -> PrimEvalMonad (Term, Term)
forall a. a -> PrimEvalMonad a
forall (m :: Type -> Type) a. Monad m => a -> m a
return (Term
fmapF',Term
apF')
                      n'ty :: Type
n'ty = LitTy -> Type
LitTy (Integer -> LitTy
NumTy (Integer
nInteger -> Integer -> Integer
forall a. Num a => a -> a -> a
-Integer
1))
                      Just (Type
consCoTy : [Type]
_) = DataCon -> [Type] -> Maybe [Type]
dataConInstArgTys DataCon
dc [Type
nTy,Type
bTy,Type
n'ty]
                  in  Machine -> Term -> Maybe Machine
reduceWHNF' (Machine
mach { mSupply = ids' }) (Term -> Maybe Machine) -> Term -> Maybe Machine
forall a b. (a -> b) -> a -> b
$
                      Term -> [Either Term Type] -> Term
mkApps Term
apF
                             [Type -> Either Term Type
forall a b. b -> Either a b
Right (TyConName -> [Type] -> Type
mkTyConApp TyConName
vecTcNm [Type
n'ty,Type
bTy])
                             ,Type -> Either Term Type
forall a b. b -> Either a b
Right (TyConName -> [Type] -> Type
mkTyConApp TyConName
vecTcNm [Type
nTy,Type
bTy])
                             ,Term -> Either Term Type
forall a b. a -> Either a b
Left (Term -> [Either Term Type] -> Term
mkApps Term
fmapF
                                           [Type -> Either Term Type
forall a b. b -> Either a b
Right Type
bTy
                                           ,Type -> Either Term Type
forall a b. b -> Either a b
Right (Type -> Type -> Type
mkFunTy (TyConName -> [Type] -> Type
mkTyConApp TyConName
vecTcNm [Type
n'ty,Type
bTy])
                                                           (TyConName -> [Type] -> Type
mkTyConApp TyConName
vecTcNm [Type
nTy,Type
bTy]))
                                           ,Term -> Either Term Type
forall a b. a -> Either a b
Left (Term -> [Either Term Type] -> Term
mkApps (DataCon -> Term
Data DataCon
dc)
                                                         [Type -> Either Term Type
forall a b. b -> Either a b
Right Type
nTy
                                                         ,Type -> Either Term Type
forall a b. b -> Either a b
Right Type
bTy
                                                         ,Type -> Either Term Type
forall a b. b -> Either a b
Right Type
n'ty
                                                         ,Term -> Either Term Type
forall a b. a -> Either a b
Left (Type -> Term
primCo Type
consCoTy)])
                                           ,Term -> Either Term Type
forall a b. a -> Either a b
Left (Term -> [Either Term Type] -> Term
mkApps (Value -> Term
valToTerm Value
f)
                                                         [Term -> Either Term Type
forall a b. a -> Either a b
Left ([Either Term Type] -> [Term]
forall a b. [Either a b] -> [a]
Either.lefts [Either Term Type]
vArgs [Term] -> Int -> Term
forall a. HasCallStack => [a] -> Int -> a
!! Int
1)])
                                           ])
                             ,Term -> Either Term Type
forall a b. a -> Either a b
Left (Term -> [Either Term Type] -> Term
mkApps (PrimInfo -> Term
Prim PrimInfo
pInfo)
                                           [Type -> Either Term Type
forall a b. b -> Either a b
Right Type
aTy
                                           ,Type -> Either Term Type
forall a b. b -> Either a b
Right Type
fTy
                                           ,Type -> Either Term Type
forall a b. b -> Either a b
Right Type
bTy
                                           ,Type -> Either Term Type
forall a b. b -> Either a b
Right Type
n'ty
                                           ,Term -> Either Term Type
forall a b. a -> Either a b
Left (Value -> Term
valToTerm Value
apDict)
                                           ,Term -> Either Term Type
forall a b. a -> Either a b
Left (Value -> Term
valToTerm Value
f)
                                           ,Term -> Either Term Type
forall a b. a -> Either a b
Left ([Either Term Type] -> [Term]
forall a b. [Either a b] -> [a]
Either.lefts [Either Term Type]
vArgs [Term] -> Int -> Term
forall a. HasCallStack => [a] -> Int -> a
!! Int
2)
                                           ])
                             ]
        where
          ([Either TyVar Type]
tyArgs,Type
_)         = Type -> ([Either TyVar Type], Type)
splitFunForallTy Type
ty
          TyConApp TyConName
vecTcNm [Type]
_ = Type -> TypeView
tyView ([Either TyVar Type] -> [Type]
forall a b. [Either a b] -> [b]
Either.rights [Either TyVar Type]
tyArgs [Type] -> Int -> Type
forall a. HasCallStack => [a] -> Int -> a
!! Int
2)
          (Supply
ids, InScopeSet
is0) = (Machine -> Supply
mSupply Machine
mach, Machine -> InScopeSet
mScopeNames Machine
mach)
      PrimStepContext
_ -> Maybe Machine
forall a. Maybe a
Nothing


-- BitPack
  , Text -> (PrimStepContext -> Maybe Machine) -> (Text, PrimStep)
primStepEntry $(textNameLit 'Clash.Sized.Vector.concatBitVector#) ((PrimStepContext -> Maybe Machine) -> (Text, PrimStep))
-> (PrimStepContext -> Maybe Machine) -> (Text, PrimStep)
forall a b. (a -> b) -> a -> b
$ \case
      PrimStepContext{Bool
[Type]
[Value]
Type
TyConMap
Machine
PrimInfo
Term -> Maybe Machine
Term -> Term
Type
-> Integer -> Integer -> (Natural -> Natural -> Natural) -> Term
Type -> Integer -> (Natural -> Natural) -> Term
Type -> [Integer] -> ([Natural] -> Term) -> Term
Machine -> Term -> Maybe Machine
tcm :: PrimStepContext -> TyConMap
isSubj :: PrimStepContext -> Bool
pInfo :: PrimStepContext -> PrimInfo
tys :: PrimStepContext -> [Type]
args :: PrimStepContext -> [Value]
mach :: PrimStepContext -> Machine
ty :: PrimStepContext -> Type
checkNaturalRange1 :: PrimStepContext -> Type -> Integer -> (Natural -> Natural) -> Term
checkNaturalRange2 :: PrimStepContext
-> Type
-> Integer
-> Integer
-> (Natural -> Natural -> Natural)
-> Term
checkNaturalRange :: PrimStepContext -> Type -> [Integer] -> ([Natural] -> Term) -> Term
reduce :: PrimStepContext -> Term -> Maybe Machine
reduceWith :: PrimStepContext -> Machine -> Term -> Maybe Machine
reduceWHNF :: PrimStepContext -> Term -> Maybe Machine
reduceWHNF' :: PrimStepContext -> Machine -> Term -> Maybe Machine
catchDivByZero :: PrimStepContext -> Term -> Term
catchErrorCall :: PrimStepContext -> Term -> Term
tcm :: TyConMap
isSubj :: Bool
pInfo :: PrimInfo
tys :: [Type]
args :: [Value]
mach :: Machine
ty :: Type
checkNaturalRange1 :: Type -> Integer -> (Natural -> Natural) -> Term
checkNaturalRange2 :: Type
-> Integer -> Integer -> (Natural -> Natural -> Natural) -> Term
checkNaturalRange :: Type -> [Integer] -> ([Natural] -> Term) -> Term
reduce :: Term -> Maybe Machine
reduceWith :: Machine -> Term -> Maybe Machine
reduceWHNF :: Term -> Maybe Machine
reduceWHNF' :: Machine -> Term -> Maybe Machine
catchDivByZero :: Term -> Term
catchErrorCall :: Term -> Term
..}
        | Bool
isSubj
        , Type
nTy : Type
mTy : [Type]
_ <- [Type]
tys
        , Value
_  : Value
km  : Value
v : [Value]
_ <- [Value]
args
        , DC DataCon
_ [Either Term Type]
vArgs <- Value
v
        , Right Integer
n <- Except String Integer -> Either String Integer
forall e a. Except e a -> Either e a
runExcept (TyConMap -> Type -> Except String Integer
tyNatSize TyConMap
tcm Type
nTy)
        -> case Integer
n of
             Integer
0  -> let resTyInfo :: (Type, Type, Integer)
resTyInfo = TyConMap -> Type -> [Type] -> (Type, Type, Integer)
extractTySizeInfo TyConMap
tcm Type
ty [Type]
tys
                   in  Term -> Maybe Machine
reduce ((Type, Type, Integer) -> Integer -> Integer -> Term
mkBitVectorLit' (Type, Type, Integer)
resTyInfo Integer
0 Integer
0)
             Integer
n' | Right Integer
m <- Except String Integer -> Either String Integer
forall e a. Except e a -> Either e a
runExcept (TyConMap -> Type -> Except String Integer
tyNatSize TyConMap
tcm Type
mTy)
                , ([Either TyVar Type]
_,Type -> TypeView
tyView -> TyConApp TyConName
bvTcNm [Type]
_) <- Type -> ([Either TyVar Type], Type)
splitFunForallTy Type
ty
                -> Term -> Maybe Machine
reduceWHNF (Term -> Maybe Machine) -> Term -> Maybe Machine
forall a b. (a -> b) -> a -> b
$
                   Term -> [Either Term Type] -> Term
mkApps (TyConName -> Term
bvAppendPrim TyConName
bvTcNm)
                     [ Type -> Either Term Type
forall a b. b -> Either a b
Right (TyConName -> [Type] -> Type
mkTyConApp TyConName
typeNatMul [LitTy -> Type
LitTy (Integer -> LitTy
NumTy (Integer
n'Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
-Integer
1)),Type
mTy])
                     , Type -> Either Term Type
forall a b. b -> Either a b
Right Type
mTy
                     , Term -> Either Term Type
forall a b. a -> Either a b
Left (Literal -> Term
Literal (Integer -> Literal
NaturalLiteral ((Integer
n'Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
-Integer
1)Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
*Integer
m)))
                     , Term -> Either Term Type
forall a b. a -> Either a b
Left ([Either Term Type] -> [Term]
forall a b. [Either a b] -> [a]
Either.lefts [Either Term Type]
vArgs [Term] -> Int -> Term
forall a. HasCallStack => [a] -> Int -> a
!! Int
1)
                     , Term -> Either Term Type
forall a b. a -> Either a b
Left (Term -> [Either Term Type] -> Term
mkApps (PrimInfo -> Term
Prim PrimInfo
pInfo)
                                    [ Type -> Either Term Type
forall a b. b -> Either a b
Right (LitTy -> Type
LitTy (Integer -> LitTy
NumTy (Integer
n'Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
-Integer
1)))
                                    , Type -> Either Term Type
forall a b. b -> Either a b
Right Type
mTy
                                    , Term -> Either Term Type
forall a b. a -> Either a b
Left (Literal -> Term
Literal (Integer -> Literal
NaturalLiteral (Integer
n'Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
-Integer
1)))
                                    , Term -> Either Term Type
forall a b. a -> Either a b
Left (Value -> Term
valToTerm Value
km)
                                    , Term -> Either Term Type
forall a b. a -> Either a b
Left ([Either Term Type] -> [Term]
forall a b. [Either a b] -> [a]
Either.lefts [Either Term Type]
vArgs [Term] -> Int -> Term
forall a. HasCallStack => [a] -> Int -> a
!! Int
2)
                                    ])
                     ]
             Integer
_ -> Maybe Machine
forall a. Maybe a
Nothing
      PrimStepContext
_ -> Maybe Machine
forall a. Maybe a
Nothing

  , Text -> (PrimStepContext -> Maybe Machine) -> (Text, PrimStep)
primStepEntry $(textNameLit 'Clash.Sized.Vector.unconcatBitVector#) ((PrimStepContext -> Maybe Machine) -> (Text, PrimStep))
-> (PrimStepContext -> Maybe Machine) -> (Text, PrimStep)
forall a b. (a -> b) -> a -> b
$ \case
      PrimStepContext{Bool
[Type]
[Value]
Type
TyConMap
Machine
PrimInfo
Term -> Maybe Machine
Term -> Term
Type
-> Integer -> Integer -> (Natural -> Natural -> Natural) -> Term
Type -> Integer -> (Natural -> Natural) -> Term
Type -> [Integer] -> ([Natural] -> Term) -> Term
Machine -> Term -> Maybe Machine
tcm :: PrimStepContext -> TyConMap
isSubj :: PrimStepContext -> Bool
pInfo :: PrimStepContext -> PrimInfo
tys :: PrimStepContext -> [Type]
args :: PrimStepContext -> [Value]
mach :: PrimStepContext -> Machine
ty :: PrimStepContext -> Type
checkNaturalRange1 :: PrimStepContext -> Type -> Integer -> (Natural -> Natural) -> Term
checkNaturalRange2 :: PrimStepContext
-> Type
-> Integer
-> Integer
-> (Natural -> Natural -> Natural)
-> Term
checkNaturalRange :: PrimStepContext -> Type -> [Integer] -> ([Natural] -> Term) -> Term
reduce :: PrimStepContext -> Term -> Maybe Machine
reduceWith :: PrimStepContext -> Machine -> Term -> Maybe Machine
reduceWHNF :: PrimStepContext -> Term -> Maybe Machine
reduceWHNF' :: PrimStepContext -> Machine -> Term -> Maybe Machine
catchDivByZero :: PrimStepContext -> Term -> Term
catchErrorCall :: PrimStepContext -> Term -> Term
tcm :: TyConMap
isSubj :: Bool
pInfo :: PrimInfo
tys :: [Type]
args :: [Value]
mach :: Machine
ty :: Type
checkNaturalRange1 :: Type -> Integer -> (Natural -> Natural) -> Term
checkNaturalRange2 :: Type
-> Integer -> Integer -> (Natural -> Natural -> Natural) -> Term
checkNaturalRange :: Type -> [Integer] -> ([Natural] -> Term) -> Term
reduce :: Term -> Maybe Machine
reduceWith :: Machine -> Term -> Maybe Machine
reduceWHNF :: Term -> Maybe Machine
reduceWHNF' :: Machine -> Term -> Maybe Machine
catchDivByZero :: Term -> Term
catchErrorCall :: Term -> Term
..}
        | Bool
isSubj
        , Type
nTy : Type
mTy : [Type]
_  <- [Type]
tys
        , Value
_  : Value
km  : Value
bv : [Value]
_ <- [Value]
args
        , ([Either TyVar Type]
_,Type -> TypeView
tyView -> TyConApp TyConName
vecTcNm [Type
_,Type
bvMTy]) <- Type -> ([Either TyVar Type], Type)
splitFunForallTy Type
ty
        , TyConApp TyConName
bvTcNm [Type]
_ <- Type -> TypeView
tyView Type
bvMTy
        , Right Integer
n <- Except String Integer -> Either String Integer
forall e a. Except e a -> Either e a
runExcept (TyConMap -> Type -> Except String Integer
tyNatSize TyConMap
tcm Type
nTy)
        -> case Integer
n of
             Integer
0 ->
              let (Just TyCon
vecTc) = TyConName -> TyConMap -> Maybe TyCon
forall a b. Uniquable a => a -> UniqMap b -> Maybe b
UniqMap.lookup TyConName
vecTcNm TyConMap
tcm
                  [DataCon
nilCon,DataCon
_] = TyCon -> [DataCon]
tyConDataCons TyCon
vecTc
              in  Term -> Maybe Machine
reduce (DataCon -> Type -> Term
mkVecNil DataCon
nilCon (TyConName -> [Type] -> Type
mkTyConApp TyConName
bvTcNm [Type
mTy]))
             Integer
n' | Right Integer
m <- Except String Integer -> Either String Integer
forall e a. Except e a -> Either e a
runExcept (TyConMap -> Type -> Except String Integer
tyNatSize TyConMap
tcm Type
mTy) ->
              let Just TyCon
vecTc  = TyConName -> TyConMap -> Maybe TyCon
forall a b. Uniquable a => a -> UniqMap b -> Maybe b
UniqMap.lookup TyConName
vecTcNm TyConMap
tcm
                  [DataCon
_,DataCon
consCon] = TyCon -> [DataCon]
tyConDataCons TyCon
vecTc
                  mBVTy :: Type
mBVTy       = TyConName -> [Type] -> Type
mkTyConApp TyConName
bvTcNm [Type
mTy]
                  n1MTy :: Type
n1MTy       = TyConName -> [Type] -> Type
mkTyConApp TyConName
typeNatMul [LitTy -> Type
LitTy (Integer -> LitTy
NumTy (Integer
n'Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
-Integer
1)),Type
mTy]
                  n1BVTy :: Type
n1BVTy      = TyConName -> [Type] -> Type
mkTyConApp TyConName
bvTcNm [Type
n1MTy]

                  (Term
hd, Term
tl) = case Value -> Maybe (Integer, Integer)
bitVectorLiteral Value
bv of
                    -- Fast path for literals
                    Just (Integer
mski, Integer
i) ->
                      let sh :: Int
sh     = Integer -> Int
forall a. Num a => Integer -> a
fromInteger ((Integer
n'Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
-Integer
1) Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
* Integer
m)
                          loMask :: Integer
loMask = Int -> Integer
forall a. Bits a => Int -> a
bit Int
sh Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
- Integer
1
                      in  ( Type -> Type -> Integer -> Integer -> Integer -> Term
mkBitVectorLit Type
mBVTy Type
mTy Integer
m
                              (Integer
mski Integer -> Int -> Integer
forall a. Bits a => a -> Int -> a
`shiftR` Int
sh) (Integer
i Integer -> Int -> Integer
forall a. Bits a => a -> Int -> a
`shiftR` Int
sh)
                          , Type -> Type -> Integer -> Integer -> Integer -> Term
mkBitVectorLit Type
n1BVTy Type
n1MTy ((Integer
n'Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
-Integer
1)Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
*Integer
m)
                              (Integer
mski Integer -> Integer -> Integer
forall a. Bits a => a -> a -> a
.&. Integer
loMask) (Integer
i Integer -> Integer -> Integer
forall a. Bits a => a -> a -> a
.&. Integer
loMask)
                          )
                    Maybe (Integer, Integer)
Nothing ->
                      let tupTcNm :: TyConName
tupTcNm     = TyCon -> TyConName
ghcTyconToTyConName (Boxity -> Int -> TyCon
tupleTyCon Boxity
Boxed Int
2)
                          Just TyCon
tupTc  = TyConName -> TyConMap -> Maybe TyCon
forall a b. Uniquable a => a -> UniqMap b -> Maybe b
UniqMap.lookup TyConName
tupTcNm TyConMap
tcm
                          [DataCon
tupDc]     = TyCon -> [DataCon]
tyConDataCons TyCon
tupTc
                          splitCall :: Term
splitCall   =
                            Term -> [Either Term Type] -> Term
mkApps (TyConName -> Term
bvSplitPrim TyConName
bvTcNm)
                                   [ Type -> Either Term Type
forall a b. b -> Either a b
Right Type
n1MTy
                                   , Type -> Either Term Type
forall a b. b -> Either a b
Right Type
mTy
                                   , Term -> Either Term Type
forall a b. a -> Either a b
Left (Literal -> Term
Literal (Integer -> Literal
NaturalLiteral ((Integer
n'Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
-Integer
1)Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
*Integer
m)))
                                   , Term -> Either Term Type
forall a b. a -> Either a b
Left (Value -> Term
valToTerm Value
bv)
                                   ]
                          -- Guaranteed no capture, so okay to use unsafe name
                          -- generation
                          xNm :: Name a
xNm         = Text -> Unique -> Name a
forall a. Text -> Unique -> Name a
mkUnsafeSystemName Text
"x" Unique
0
                          bvNm :: Name a
bvNm        = Text -> Unique -> Name a
forall a. Text -> Unique -> Name a
mkUnsafeSystemName Text
"bv'" Unique
1
                          xId :: Id
xId         = Type -> TmName -> Id
mkLocalId Type
mBVTy TmName
forall {a}. Name a
xNm
                          bvId :: Id
bvId        = Type -> TmName -> Id
mkLocalId Type
n1BVTy TmName
forall {a}. Name a
bvNm
                          tupPat :: Pat
tupPat      = DataCon -> [TyVar] -> [Id] -> Pat
DataPat DataCon
tupDc [] [Id
xId,Id
bvId]
                          xAlt :: (Pat, Term)
xAlt        = (Pat
tupPat, (Id -> Term
Var Id
xId))
                          bvAlt :: (Pat, Term)
bvAlt       = (Pat
tupPat, (Id -> Term
Var Id
bvId))
                      in  ( Term -> Type -> [(Pat, Term)] -> Term
Case Term
splitCall Type
mBVTy [(Pat, Term)
xAlt]
                          , Term -> Type -> [(Pat, Term)] -> Term
Case Term
splitCall Type
n1BVTy [(Pat, Term)
bvAlt]
                          )

              in  Term -> Maybe Machine
reduce (Term -> Maybe Machine) -> Term -> Maybe Machine
forall a b. (a -> b) -> a -> b
$ HasCallStack => DataCon -> Type -> Integer -> Term -> Term -> Term
DataCon -> Type -> Integer -> Term -> Term -> Term
mkVecCons DataCon
consCon Type
mBVTy Integer
n' Term
hd
                    (Term -> [Either Term Type] -> Term
mkApps (PrimInfo -> Term
Prim PrimInfo
pInfo)
                            [ Type -> Either Term Type
forall a b. b -> Either a b
Right (LitTy -> Type
LitTy (Integer -> LitTy
NumTy (Integer
n'Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
-Integer
1)))
                            , Type -> Either Term Type
forall a b. b -> Either a b
Right Type
mTy
                            , Term -> Either Term Type
forall a b. a -> Either a b
Left (Literal -> Term
Literal (Integer -> Literal
NaturalLiteral (Integer
n'Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
-Integer
1)))
                            , Term -> Either Term Type
forall a b. a -> Either a b
Left (Value -> Term
valToTerm Value
km)
                            , Term -> Either Term Type
forall a b. a -> Either a b
Left Term
tl
                            ])
             Integer
_ -> Maybe Machine
forall a. Maybe a
Nothing
      PrimStepContext
_ -> Maybe Machine
forall a. Maybe a
Nothing

  ]