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

  Transformations for compile-time reduction of expressions / primitives.
-}

{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE OverloadedStrings #-}

module Clash.Normalize.Transformations.Reduce
  ( reduceBinders
  , reduceConst
  , reduceNonRepPrim
  ) where

import qualified Control.Lens as Lens
import Control.Monad.Trans.Except (runExcept)
import qualified Data.Either as Either
import qualified Data.List as List
import qualified Data.List.Extra as List
import qualified Data.Maybe as Maybe
import Data.Maybe (fromMaybe, listToMaybe)
import GHC.Stack (HasCallStack)

import Clash.Core.FreeVars (typeFreeVars)
import Clash.Core.HasType
import Clash.Core.Name (nameOcc)
import Clash.Core.Pretty (showPpr)
import Clash.Core.Subst (Subst, extendIdSubst, substTm)
import Clash.Core.Term
  ( CoreContext(..), LetBinding, PrimInfo(..), Term(..), TickInfo(..), collectArgs
  , collectArgsTicks, mkApps, mkTicks, mkTmApps)
import Clash.Core.TyCon (tyConDataCons)
import Clash.Core.Type (Type, TypeView(..), mkTyConApp, splitFunForallTy, tyView)
import Clash.Core.Util (mkVec, shouldSplit, tyNatSize, mkInternalVar)
import Clash.Core.VarEnv (extendInScopeSet)
import qualified Clash.Data.UniqMap as UniqMap
import Clash.Normalize.PrimitiveReductions
import Clash.Normalize.Primitives (removedArg)
import Clash.Normalize.Types (NormRewrite, NormalizeSession)
import Clash.Normalize.Util (shouldReduce)
import Clash.Rewrite.Types (TransformContext(..), tcCache, normalizeUltra)
import Clash.Rewrite.Util (changed, isUntranslatableType, setChanged, whnfRW)

-- | XXX: is given inverse topologically sorted binders, but returns
-- topologically sorted binders
--
-- TODO: check further speed improvements:
--
-- 1. Store the processed binders in a `Map Expr LetBinding`:
--    * Trades O(1) `cons` and O(n)*aeqTerm `find` for:
--    * O(log n)*aeqTerm `insert` and O(log n)*aeqTerm `lookup`
-- 2. Store the processed binders in a `AEQTrie Expr LetBinding`
--    * Trades O(1) `cons` and O(n)*aeqTerm `find` for:
--    * O(e) `insert` and O(e) `lookup`
reduceBinders
  :: Subst
  -> [LetBinding]
  -> [LetBinding]
  -> NormalizeSession (Subst, [LetBinding])
reduceBinders :: Subst
-> [LetBinding]
-> [LetBinding]
-> NormalizeSession (Subst, [LetBinding])
reduceBinders !Subst
subst [LetBinding]
processed [] = (Subst, [LetBinding]) -> NormalizeSession (Subst, [LetBinding])
forall a. a -> RewriteMonad NormalizeState a
forall (m :: Type -> Type) a. Monad m => a -> m a
return (Subst
subst,[LetBinding]
processed)
reduceBinders !Subst
subst [LetBinding]
processed ((Id
i,HasCallStack => Doc () -> Subst -> Term -> Term
Doc () -> Subst -> Term -> Term
substTm Doc ()
"reduceBinders" Subst
subst -> Term
e):[LetBinding]
rest)
  | (Term
_,[Either Term Type]
_,[TickInfo]
ticks) <- Term -> (Term, [Either Term Type], [TickInfo])
collectArgsTicks Term
e
  , TickInfo
NoDeDup TickInfo -> [TickInfo] -> Bool
forall (t :: Type -> Type) a.
(Foldable t, Eq a) =>
a -> t a -> Bool
`notElem` [TickInfo]
ticks
  , Just (Id
i1,Term
_) <- (LetBinding -> Bool) -> [LetBinding] -> Maybe LetBinding
forall (t :: Type -> Type) a.
Foldable t =>
(a -> Bool) -> t a -> Maybe a
List.find ((Term -> Term -> Bool
forall a. Eq a => a -> a -> Bool
== Term
e) (Term -> Bool) -> (LetBinding -> Term) -> LetBinding -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. LetBinding -> Term
forall a b. (a, b) -> b
snd) [LetBinding]
processed
  = do
    let subst1 :: Subst
subst1 = Subst -> Id -> Term -> Subst
extendIdSubst Subst
subst Id
i (Id -> Term
Var Id
i1)
    RewriteMonad NormalizeState ()
forall extra. RewriteMonad extra ()
setChanged
    Subst
-> [LetBinding]
-> [LetBinding]
-> NormalizeSession (Subst, [LetBinding])
reduceBinders Subst
subst1 [LetBinding]
processed [LetBinding]
rest
  | Bool
otherwise
  = Subst
-> [LetBinding]
-> [LetBinding]
-> NormalizeSession (Subst, [LetBinding])
reduceBinders Subst
subst ((Id
i,Term
e)LetBinding -> [LetBinding] -> [LetBinding]
forall a. a -> [a] -> [a]
:[LetBinding]
processed) [LetBinding]
rest
{-# SCC reduceBinders #-}

reduceConst :: HasCallStack => NormRewrite
reduceConst :: HasCallStack => NormRewrite
reduceConst TransformContext
ctx e :: Term
e@(App Term
_ Term
_)
  | (Prim PrimInfo
p0, [Either Term Type]
_) <- Term -> (Term, [Either Term Type])
collectArgs Term
e
  = Bool
-> TransformContext
-> Term
-> NormRewrite
-> RewriteMonad NormalizeState Term
forall extra.
Bool
-> TransformContext
-> Term
-> Rewrite extra
-> RewriteMonad extra Term
whnfRW Bool
False TransformContext
ctx Term
e (NormRewrite -> RewriteMonad NormalizeState Term)
-> NormRewrite -> RewriteMonad NormalizeState Term
forall a b. (a -> b) -> a -> b
$ \TransformContext
_ctx1 Term
e1 -> case Term
e1 of
      (Term -> (Term, [Either Term Type])
collectArgs -> (Prim PrimInfo
p1, [Either Term Type]
_)) | PrimInfo -> Text
primName PrimInfo
p0 Text -> Text -> Bool
forall a. Eq a => a -> a -> Bool
== PrimInfo -> Text
primName PrimInfo
p1 -> Term -> RewriteMonad NormalizeState Term
forall a. a -> RewriteMonad NormalizeState a
forall (m :: Type -> Type) a. Monad m => a -> m a
return Term
e
      Term
_ -> Term -> RewriteMonad NormalizeState Term
forall a extra. a -> RewriteMonad extra a
changed Term
e1

reduceConst TransformContext
_ Term
e = Term -> RewriteMonad NormalizeState Term
forall a. a -> RewriteMonad NormalizeState a
forall (m :: Type -> Type) a. Monad m => a -> m a
return Term
e
{-# SCC reduceConst #-}

-- | Replace primitives by their "definition" if they would lead to let-bindings
-- with a non-representable type when a function is in ANF. This happens for
-- example when Clash.Size.Vector.map consumes or produces a vector of
-- non-representable elements.
--
-- Basically what this transformation does is replace a primitive the completely
-- unrolled recursive definition that it represents. e.g.
--
-- > zipWith ($) (xs :: Vec 2 (Int -> Int)) (ys :: Vec 2 Int)
--
-- is replaced by:
--
-- > let (x0  :: (Int -> Int))       = case xs  of (:>) _ x xr -> x
-- >     (xr0 :: Vec 1 (Int -> Int)) = case xs  of (:>) _ x xr -> xr
-- >     (x1  :: (Int -> Int)(       = case xr0 of (:>) _ x xr -> x
-- >     (y0  :: Int)                = case ys  of (:>) _ y yr -> y
-- >     (yr0 :: Vec 1 Int)          = case ys  of (:>) _ y yr -> xr
-- >     (y1  :: Int                 = case yr0 of (:>) _ y yr -> y
-- > in  (($) x0 y0 :> ($) x1 y1 :> Nil)
--
-- Currently, it only handles the following functions:
--
-- * Clash.Sized.Vector.zipWith
-- * Clash.Sized.Vector.map
-- * Clash.Sized.Vector.traverse#
-- * Clash.Sized.Vector.fold
-- * Clash.Sized.Vector.foldr
-- * Clash.Sized.Vector.dfold
-- * Clash.Sized.Vector.(++)
-- * Clash.Sized.Vector.head
-- * Clash.Sized.Vector.tail
-- * Clash.Sized.Vector.last
-- * Clash.Sized.Vector.init
-- * Clash.Sized.Vector.unconcat
-- * Clash.Sized.Vector.transpose
-- * Clash.Sized.Vector.replicate
-- * Clash.Sized.Vector.replace_int
-- * Clash.Sized.Vector.imap
-- * Clash.Sized.Vector.dtfold
-- * Clash.Sized.RTree.tdfold
-- * Clash.Sized.RTree.treplicate
-- * Clash.Sized.Internal.BitVector.split#
-- * Clash.Sized.Internal.BitVector.eq#
--
-- Note [Unroll shouldSplit types]
-- 1. Certain higher-order functions over Vec, such as map, have specialized
-- code-paths to turn them into generate-for loops in HDL, instead of having to
-- having to unroll/inline their recursive definitions, e.g. Clash.Sized.Vector.map
--
-- 2. Clash, in general, translates Haskell product types to VHDL records. This
-- mostly works out fine, there is however one exception: certain synthesis
-- tools, and some HDL simulation tools (like verilator), do not like it when
-- the clock (and certain other global control signals) is contained in a
-- record type; they want them to be separate inputs to the entity/module.
-- And Clash actually does some transformations to try to ensure that values of
-- type Clock do not end up in a VHDL record type.
--
-- The problem is that the transformations in 2. never took into account the
-- specialized code-paths in 1. Making the code-paths in 1. aware of the
-- transformations in 2. is really not worth the effort for such a niche case.
-- It's easier to just unroll the recursive definitions.
--
-- See https://github.com/clash-lang/clash-compiler/issues/1606
reduceNonRepPrim :: HasCallStack => NormRewrite
reduceNonRepPrim :: HasCallStack => NormRewrite
reduceNonRepPrim c :: TransformContext
c@(TransformContext InScopeSet
_ Context
ctx) e :: Term
e@(App Term
_ Term
_) | (Prim PrimInfo
p, [Either Term Type]
args, [TickInfo]
ticks) <- Term -> (Term, [Either Term Type], [TickInfo])
collectArgsTicks Term
e = do
  tcm <- Getting TyConMap RewriteEnv TyConMap
-> RewriteMonad NormalizeState TyConMap
forall s (m :: Type -> Type) a.
MonadReader s m =>
Getting a s a -> m a
Lens.view Getting TyConMap RewriteEnv TyConMap
Getter RewriteEnv TyConMap
tcCache
  ultra <- Lens.view normalizeUltra
  let eTy = TyConMap -> Term -> Type
forall a. InferType a => TyConMap -> a -> Type
inferCoreTypeOf TyConMap
tcm Term
e
  let resTy = ([Either TyVar Type], Type) -> Type
forall a b. (a, b) -> b
snd (Type -> ([Either TyVar Type], Type)
splitFunForallTy Type
eTy)
  case tyView resTy of
    (TyConApp vecTcNm :: TyConName
vecTcNm@(TyConName -> Text
forall a. Name a -> Text
nameOcc -> Text
"Clash.Sized.Vector.Vec")
              [Except String Integer -> Either String Integer
forall e a. Except e a -> Either e a
runExcept (Except String Integer -> Either String Integer)
-> (Type -> Except String Integer) -> Type -> Either String Integer
forall b c a. (b -> c) -> (a -> b) -> a -> c
. TyConMap -> Type -> Except String Integer
tyNatSize TyConMap
tcm -> Right Integer
0, Type
aTy]) -> do
      let nilE :: Term
nilE = Term -> Maybe Term -> Term
forall a. a -> Maybe a -> a
fromMaybe (String -> Term
forall a. HasCallStack => String -> a
error String
"reduceNonRepPrim: unable to create Vec DCs") (Maybe Term -> Term) -> Maybe Term -> Term
forall a b. (a -> b) -> a -> b
$ do
            vecTc <- TyConName -> TyConMap -> Maybe TyCon
forall a b. Uniquable a => a -> UniqMap b -> Maybe b
UniqMap.lookup TyConName
vecTcNm TyConMap
tcm
            [nilCon,consCon] <- pure (tyConDataCons vecTc)
            return (mkVec nilCon consCon aTy 0 [])
      Term -> RewriteMonad NormalizeState Term
forall a extra. a -> RewriteMonad extra a
changed (Term -> [TickInfo] -> Term
mkTicks Term
nilE [TickInfo]
ticks)
    TypeView
tv -> let argLen :: Int
argLen = [Either Term Type] -> Int
forall a. [a] -> Int
forall (t :: Type -> Type) a. Foldable t => t a -> Int
length [Either Term Type]
args in case PrimInfo -> Text
primName PrimInfo
p of
      Text
"Clash.Sized.Vector.zipWith"
        | ([Term]
tmArgs,[Type
lhsElTy,Type
rhsElty,Type
resElTy,Type
nTy]) <- [Either Term Type] -> ([Term], [Type])
forall a b. [Either a b] -> ([a], [b])
Either.partitionEithers [Either Term Type]
args
        , TyConApp TyConName
vecTcNm [Type]
_ <- TypeView
tv
        , let lhsTy :: Type
lhsTy = TyConName -> [Type] -> Type
mkTyConApp TyConName
vecTcNm [Type
nTy,Type
lhsElTy]
        , let rhsTy :: Type
rhsTy = TyConName -> [Type] -> Type
mkTyConApp TyConName
vecTcNm [Type
nTy,Type
rhsElty]
        -> 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
n -> do
            shouldReduce1 <- [RewriteMonad NormalizeState Bool]
-> RewriteMonad NormalizeState Bool
forall (m :: Type -> Type). Monad m => [m Bool] -> m Bool
List.orM [ Bool -> RewriteMonad NormalizeState Bool
forall a. a -> RewriteMonad NormalizeState a
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure (Bool
ultra Bool -> Bool -> Bool
|| Integer
n Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
< Integer
2)
                                 , Context -> RewriteMonad NormalizeState Bool
shouldReduce Context
ctx
                                 , (Type -> RewriteMonad NormalizeState Bool)
-> [Type] -> RewriteMonad NormalizeState Bool
forall (m :: Type -> Type) a.
Monad m =>
(a -> m Bool) -> [a] -> m Bool
List.anyM Type -> RewriteMonad NormalizeState Bool
forall {extra}. Type -> RewriteMonad extra Bool
isUntranslatableType_not_poly
                                        [Type
lhsElTy,Type
rhsElty,Type
resElTy]
                                 -- Note [Unroll shouldSplit types]
                                 , Bool -> RewriteMonad NormalizeState Bool
forall a. a -> RewriteMonad NormalizeState a
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure ((Type -> Bool) -> [Type] -> Bool
forall (t :: Type -> Type) a.
Foldable t =>
(a -> Bool) -> t a -> Bool
any (Maybe ([Term] -> Term, Projections, [Type]) -> Bool
forall a. Maybe a -> Bool
Maybe.isJust (Maybe ([Term] -> Term, Projections, [Type]) -> Bool)
-> (Type -> Maybe ([Term] -> Term, Projections, [Type]))
-> Type
-> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. TyConMap -> Type -> Maybe ([Term] -> Term, Projections, [Type])
shouldSplit TyConMap
tcm)
                                             [Type
lhsTy,Type
rhsTy,Type
resTy]) ]
            if shouldReduce1
               then abstractOverMissingArgs ticks tmArgs eTy c
                      (reduceZipWith p n lhsElTy rhsElty resElTy)
               else return e
          Either String Integer
_ -> Term -> RewriteMonad NormalizeState Term
forall a. a -> RewriteMonad NormalizeState a
forall (m :: Type -> Type) a. Monad m => a -> m a
return Term
e
        | Int
argLen Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
>= Int
4
        -> String -> RewriteMonad NormalizeState Term
forall a. HasCallStack => String -> a
error (String
"reduceNonRepPrim: zipWith bad args" String -> String -> String
forall a. Semigroup a => a -> a -> a
<> Term -> String
forall p. PrettyPrec p => p -> String
showPpr Term
e)

      Text
"Clash.Sized.Vector.map"
        | ([Term]
tmArgs,[Type
argElTy,Type
resElTy,Type
nTy]) <- [Either Term Type] -> ([Term], [Type])
forall a b. [Either a b] -> ([a], [b])
Either.partitionEithers [Either Term Type]
args
        , TyConApp TyConName
vecTcNm [Type]
_ <- TypeView
tv
        , let argTy :: Type
argTy = TyConName -> [Type] -> Type
mkTyConApp TyConName
vecTcNm [Type
nTy,Type
argElTy]
        -> 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
n -> do
            shouldReduce1 <- [RewriteMonad NormalizeState Bool]
-> RewriteMonad NormalizeState Bool
forall (m :: Type -> Type). Monad m => [m Bool] -> m Bool
List.orM [ Bool -> RewriteMonad NormalizeState Bool
forall a. a -> RewriteMonad NormalizeState a
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure (Bool
ultra Bool -> Bool -> Bool
|| Integer
n Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
< Integer
2 )
                                 , Context -> RewriteMonad NormalizeState Bool
shouldReduce Context
ctx
                                 , (Type -> RewriteMonad NormalizeState Bool)
-> [Type] -> RewriteMonad NormalizeState Bool
forall (m :: Type -> Type) a.
Monad m =>
(a -> m Bool) -> [a] -> m Bool
List.anyM Type -> RewriteMonad NormalizeState Bool
forall {extra}. Type -> RewriteMonad extra Bool
isUntranslatableType_not_poly
                                        [Type
argElTy,Type
resElTy]
                                 -- Note [Unroll shouldSplit types]
                                 , Bool -> RewriteMonad NormalizeState Bool
forall a. a -> RewriteMonad NormalizeState a
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure ((Type -> Bool) -> [Type] -> Bool
forall (t :: Type -> Type) a.
Foldable t =>
(a -> Bool) -> t a -> Bool
any (Maybe ([Term] -> Term, Projections, [Type]) -> Bool
forall a. Maybe a -> Bool
Maybe.isJust (Maybe ([Term] -> Term, Projections, [Type]) -> Bool)
-> (Type -> Maybe ([Term] -> Term, Projections, [Type]))
-> Type
-> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. TyConMap -> Type -> Maybe ([Term] -> Term, Projections, [Type])
shouldSplit TyConMap
tcm)
                                             [Type
argTy,Type
resTy]) ]
            if shouldReduce1
               then abstractOverMissingArgs ticks tmArgs eTy c
                      (reduceMap p n argElTy resElTy)
               else return e
          Either String Integer
_ -> Term -> RewriteMonad NormalizeState Term
forall a. a -> RewriteMonad NormalizeState a
forall (m :: Type -> Type) a. Monad m => a -> m a
return Term
e
        | Int
argLen Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
>= Int
3
        -> String -> RewriteMonad NormalizeState Term
forall a. HasCallStack => String -> a
error (String
"reduceNonRepPrim: map bad args" String -> String -> String
forall a. Semigroup a => a -> a -> a
<> Term -> String
forall p. PrettyPrec p => p -> String
showPpr Term
e)

      Text
"Clash.Sized.Vector.traverse#"
        | ([Term]
tmArgs,[Type
aTy,Type
fTy,Type
bTy,Type
nTy]) <- [Either Term Type] -> ([Term], [Type])
forall a b. [Either a b] -> ([a], [b])
Either.partitionEithers [Either Term Type]
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
n -> [TickInfo]
-> [Term]
-> Type
-> TransformContext
-> (Term
    -> Term
    -> Term
    -> TransformContext
    -> RewriteMonad NormalizeState Term)
-> RewriteMonad NormalizeState Term
forall a.
(AbstractOverMissingArgs a, HasCallStack) =>
[TickInfo]
-> [Term]
-> Type
-> TransformContext
-> a
-> RewriteMonad NormalizeState Term
abstractOverMissingArgs [TickInfo]
ticks [Term]
tmArgs Type
eTy TransformContext
c (Integer
-> Type
-> Type
-> Type
-> Term
-> Term
-> Term
-> TransformContext
-> RewriteMonad NormalizeState Term
reduceTraverse Integer
n Type
aTy Type
fTy Type
bTy)
          Either String Integer
_ -> Term -> RewriteMonad NormalizeState Term
forall a. a -> RewriteMonad NormalizeState a
forall (m :: Type -> Type) a. Monad m => a -> m a
return Term
e
        | Int
argLen Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
>= Int
4
        -> String -> RewriteMonad NormalizeState Term
forall a. HasCallStack => String -> a
error (String
"reduceNonRepPrim: traverse# bad args" String -> String -> String
forall a. Semigroup a => a -> a -> a
<> Term -> String
forall p. PrettyPrec p => p -> String
showPpr Term
e)

      Text
"Clash.Sized.Vector.fold"
        | ([Term]
tmArgs,[Type
nTy,Type
aTy]) <- [Either Term Type] -> ([Term], [Type])
forall a b. [Either a b] -> ([a], [b])
Either.partitionEithers [Either Term Type]
args
        , (Either TyVar Type
_:Right Type
argTy:[Either TyVar Type]
_) <- ([Either TyVar Type], Type) -> [Either TyVar Type]
forall a b. (a, b) -> a
fst (Type -> ([Either TyVar Type], Type)
splitFunForallTy (HasCallStack => TyConMap -> Type -> [Type] -> Type
TyConMap -> Type -> [Type] -> Type
piResultTys TyConMap
tcm (PrimInfo -> Type
primType PrimInfo
p) [Type
nTy,Type
aTy]))
        -> 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
n -> do
            shouldReduce1 <- [RewriteMonad NormalizeState Bool]
-> RewriteMonad NormalizeState Bool
forall (m :: Type -> Type). Monad m => [m Bool] -> m Bool
List.orM [ Bool -> RewriteMonad NormalizeState Bool
forall a. a -> RewriteMonad NormalizeState a
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure (Bool
ultra Bool -> Bool -> Bool
|| Integer
n Integer -> Integer -> Bool
forall a. Eq a => a -> a -> Bool
== Integer
0)
                                 , Context -> RewriteMonad NormalizeState Bool
shouldReduce Context
ctx
                                 , Type -> RewriteMonad NormalizeState Bool
forall {extra}. Type -> RewriteMonad extra Bool
isUntranslatableType_not_poly Type
aTy
                                 -- Note [Unroll shouldSplit types]
                                 , Bool -> RewriteMonad NormalizeState Bool
forall a. a -> RewriteMonad NormalizeState a
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure (Maybe ([Term] -> Term, Projections, [Type]) -> Bool
forall a. Maybe a -> Bool
Maybe.isJust (TyConMap -> Type -> Maybe ([Term] -> Term, Projections, [Type])
shouldSplit TyConMap
tcm Type
argTy))]
            if shouldReduce1 then
              abstractOverMissingArgs ticks tmArgs eTy c (reduceFold (n + 1) aTy)
            else return e
          Either String Integer
_ -> Term -> RewriteMonad NormalizeState Term
forall a. a -> RewriteMonad NormalizeState a
forall (m :: Type -> Type) a. Monad m => a -> m a
return Term
e
        | Int
argLen Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
>= Int
2
        -> String -> RewriteMonad NormalizeState Term
forall a. HasCallStack => String -> a
error (String
"reduceNonRepPrim: fold bad args" String -> String -> String
forall a. Semigroup a => a -> a -> a
<> Term -> String
forall p. PrettyPrec p => p -> String
showPpr Term
e)

      Text
"Clash.Sized.Vector.foldr"
        | ([Term]
tmArgs,[Type
aTy,Type
bTy,Type
nTy]) <- [Either Term Type] -> ([Term], [Type])
forall a b. [Either a b] -> ([a], [b])
Either.partitionEithers [Either Term Type]
args
        , (Either TyVar Type
_:Either TyVar Type
_:Right Type
argTy:[Either TyVar Type]
_) <- ([Either TyVar Type], Type) -> [Either TyVar Type]
forall a b. (a, b) -> a
fst (Type -> ([Either TyVar Type], Type)
splitFunForallTy (HasCallStack => TyConMap -> Type -> [Type] -> Type
TyConMap -> Type -> [Type] -> Type
piResultTys TyConMap
tcm (PrimInfo -> Type
primType PrimInfo
p) [Type
aTy,Type
bTy,Type
nTy]))
        -> 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
n -> do
            shouldReduce1 <- [RewriteMonad NormalizeState Bool]
-> RewriteMonad NormalizeState Bool
forall (m :: Type -> Type). Monad m => [m Bool] -> m Bool
List.orM [ Bool -> RewriteMonad NormalizeState Bool
forall a. a -> RewriteMonad NormalizeState a
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure Bool
ultra
                                 , Context -> RewriteMonad NormalizeState Bool
shouldReduce Context
ctx
                                 , (Type -> RewriteMonad NormalizeState Bool)
-> [Type] -> RewriteMonad NormalizeState Bool
forall (m :: Type -> Type) a.
Monad m =>
(a -> m Bool) -> [a] -> m Bool
List.anyM Type -> RewriteMonad NormalizeState Bool
forall {extra}. Type -> RewriteMonad extra Bool
isUntranslatableType_not_poly [Type
aTy,Type
bTy]
                                 -- Note [Unroll shouldSplit types]
                                 , Bool -> RewriteMonad NormalizeState Bool
forall a. a -> RewriteMonad NormalizeState a
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure (Maybe ([Term] -> Term, Projections, [Type]) -> Bool
forall a. Maybe a -> Bool
Maybe.isJust (TyConMap -> Type -> Maybe ([Term] -> Term, Projections, [Type])
shouldSplit TyConMap
tcm Type
argTy)) ]
            if shouldReduce1
              then abstractOverMissingArgs ticks tmArgs eTy c (reduceFoldr p n aTy)
              else return e
          Either String Integer
_ -> Term -> RewriteMonad NormalizeState Term
forall a. a -> RewriteMonad NormalizeState a
forall (m :: Type -> Type) a. Monad m => a -> m a
return Term
e
        | Int
argLen Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
>= Int
3
        -> String -> RewriteMonad NormalizeState Term
forall a. HasCallStack => String -> a
error (String
"reduceNonRepPrim: foldr bad args" String -> String -> String
forall a. Semigroup a => a -> a -> a
<> Term -> String
forall p. PrettyPrec p => p -> String
showPpr Term
e)

      Text
"Clash.Sized.Vector.dfold"
        | ([Term]
tmArgs,[Type
_mTy,Type
nTy,Type
aTy]) <- [Either Term Type] -> ([Term], [Type])
forall a b. [Either a b] -> ([a], [b])
Either.partitionEithers [Either Term Type]
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
n -> [TickInfo]
-> [Term]
-> Type
-> TransformContext
-> (Term
    -> Term
    -> Term
    -> Term
    -> Term
    -> TransformContext
    -> RewriteMonad NormalizeState Term)
-> RewriteMonad NormalizeState Term
forall a.
(AbstractOverMissingArgs a, HasCallStack) =>
[TickInfo]
-> [Term]
-> Type
-> TransformContext
-> a
-> RewriteMonad NormalizeState Term
abstractOverMissingArgs [TickInfo]
ticks [Term]
tmArgs Type
eTy TransformContext
c (Integer
-> Type
-> Term
-> Term
-> Term
-> Term
-> Term
-> TransformContext
-> RewriteMonad NormalizeState Term
reduceDFold Integer
n Type
aTy)
          Either String Integer
_ -> Term -> RewriteMonad NormalizeState Term
forall a. a -> RewriteMonad NormalizeState a
forall (m :: Type -> Type) a. Monad m => a -> m a
return Term
e
        | Int
argLen Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
>= Int
3
        -> String -> RewriteMonad NormalizeState Term
forall a. HasCallStack => String -> a
error (String
"reduceNonRepPrim: dfold bad args" String -> String -> String
forall a. Semigroup a => a -> a -> a
<> Term -> String
forall p. PrettyPrec p => p -> String
showPpr Term
e)

      Text
"Clash.Sized.Vector.++"
        | ([Term]
tmArgs,[Type
nTy,Type
aTy,Type
mTy]) <- [Either Term Type] -> ([Term], [Type])
forall a b. [Either a b] -> ([a], [b])
Either.partitionEithers [Either Term Type]
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), 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)) of
              (Right Integer
n, Right Integer
m) -> do
                    shouldReduce1 <- [RewriteMonad NormalizeState Bool]
-> RewriteMonad NormalizeState Bool
forall (m :: Type -> Type). Monad m => [m Bool] -> m Bool
List.orM [ Bool -> RewriteMonad NormalizeState Bool
forall a. a -> RewriteMonad NormalizeState a
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure (Integer
nInteger -> Integer -> Bool
forall a. Eq a => a -> a -> Bool
==Integer
0)
                                         , Bool -> RewriteMonad NormalizeState Bool
forall a. a -> RewriteMonad NormalizeState a
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure (Integer
mInteger -> Integer -> Bool
forall a. Eq a => a -> a -> Bool
==Integer
0)
                                         , Context -> RewriteMonad NormalizeState Bool
shouldReduce Context
ctx
                                         , Type -> RewriteMonad NormalizeState Bool
forall {extra}. Type -> RewriteMonad extra Bool
isUntranslatableType_not_poly Type
aTy
                                         -- Note [Unroll shouldSplit types]
                                         , Bool -> RewriteMonad NormalizeState Bool
forall a. a -> RewriteMonad NormalizeState a
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure (Maybe ([Term] -> Term, Projections, [Type]) -> Bool
forall a. Maybe a -> Bool
Maybe.isJust (TyConMap -> Type -> Maybe ([Term] -> Term, Projections, [Type])
shouldSplit TyConMap
tcm Type
resTy)) ]
                    if shouldReduce1
                       then abstractOverMissingArgs ticks tmArgs eTy c (reduceAppend n m aTy)
                       else return e
              (Either String Integer, Either String Integer)
_ -> Term -> RewriteMonad NormalizeState Term
forall a. a -> RewriteMonad NormalizeState a
forall (m :: Type -> Type) a. Monad m => a -> m a
return Term
e
        | Int
argLen Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
>= Int
3
        -> String -> RewriteMonad NormalizeState Term
forall a. HasCallStack => String -> a
error (String
"reduceNonRepPrim: ++ bad args" String -> String -> String
forall a. Semigroup a => a -> a -> a
<> Term -> String
forall p. PrettyPrec p => p -> String
showPpr Term
e)

      Text
"Clash.Sized.Vector.head"
        | ([Term]
tmArgs,[Type
nTy,Type
aTy]) <- [Either Term Type] -> ([Term], [Type])
forall a b. [Either a b] -> ([a], [b])
Either.partitionEithers [Either Term Type]
args
        , (Right Type
argTy:[Either TyVar Type]
_) <- ([Either TyVar Type], Type) -> [Either TyVar Type]
forall a b. (a, b) -> a
fst (Type -> ([Either TyVar Type], Type)
splitFunForallTy (HasCallStack => TyConMap -> Type -> [Type] -> Type
TyConMap -> Type -> [Type] -> Type
piResultTys TyConMap
tcm (PrimInfo -> Type
primType PrimInfo
p) [Type
nTy,Type
aTy]))
        -> 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
n -> do
            shouldReduce1 <- [RewriteMonad NormalizeState Bool]
-> RewriteMonad NormalizeState Bool
forall (m :: Type -> Type). Monad m => [m Bool] -> m Bool
List.orM [ Context -> RewriteMonad NormalizeState Bool
shouldReduce Context
ctx
                                 , Type -> RewriteMonad NormalizeState Bool
forall {extra}. Type -> RewriteMonad extra Bool
isUntranslatableType_not_poly Type
aTy
                                 -- Note [Unroll shouldSplit types]
                                 , Bool -> RewriteMonad NormalizeState Bool
forall a. a -> RewriteMonad NormalizeState a
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure (Maybe ([Term] -> Term, Projections, [Type]) -> Bool
forall a. Maybe a -> Bool
Maybe.isJust (TyConMap -> Type -> Maybe ([Term] -> Term, Projections, [Type])
shouldSplit TyConMap
tcm Type
argTy)) ]
            if shouldReduce1
               then abstractOverMissingArgs ticks tmArgs eTy c (reduceHead (n+1) aTy)
               else return e
          Either String Integer
_ -> Term -> RewriteMonad NormalizeState Term
forall a. a -> RewriteMonad NormalizeState a
forall (m :: Type -> Type) a. Monad m => a -> m a
return Term
e
        | Int
argLen Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
>= Int
2
        -> String -> RewriteMonad NormalizeState Term
forall a. HasCallStack => String -> a
error (String
"reduceNonRepPrim: head bad args" String -> String -> String
forall a. Semigroup a => a -> a -> a
<> Term -> String
forall p. PrettyPrec p => p -> String
showPpr Term
e)

      Text
"Clash.Sized.Vector.tail"
        | ([Term]
tmArgs,[Type
nTy,Type
aTy]) <- [Either Term Type] -> ([Term], [Type])
forall a b. [Either a b] -> ([a], [b])
Either.partitionEithers [Either Term Type]
args
        , (Right Type
argTy:[Either TyVar Type]
_) <- ([Either TyVar Type], Type) -> [Either TyVar Type]
forall a b. (a, b) -> a
fst (Type -> ([Either TyVar Type], Type)
splitFunForallTy (HasCallStack => TyConMap -> Type -> [Type] -> Type
TyConMap -> Type -> [Type] -> Type
piResultTys TyConMap
tcm (PrimInfo -> Type
primType PrimInfo
p) [Type
nTy,Type
aTy]))
        -> 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
n -> do
            shouldReduce1 <- [RewriteMonad NormalizeState Bool]
-> RewriteMonad NormalizeState Bool
forall (m :: Type -> Type). Monad m => [m Bool] -> m Bool
List.orM [ Context -> RewriteMonad NormalizeState Bool
shouldReduce Context
ctx
                                 , Type -> RewriteMonad NormalizeState Bool
forall {extra}. Type -> RewriteMonad extra Bool
isUntranslatableType_not_poly Type
aTy
                                 -- Note [Unroll shouldSplit types]
                                 , Bool -> RewriteMonad NormalizeState Bool
forall a. a -> RewriteMonad NormalizeState a
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure (Maybe ([Term] -> Term, Projections, [Type]) -> Bool
forall a. Maybe a -> Bool
Maybe.isJust (TyConMap -> Type -> Maybe ([Term] -> Term, Projections, [Type])
shouldSplit TyConMap
tcm Type
argTy)) ]
            if shouldReduce1
               then abstractOverMissingArgs ticks tmArgs eTy c (reduceTail (n+1) aTy)
               else return e
          Either String Integer
_ -> Term -> RewriteMonad NormalizeState Term
forall a. a -> RewriteMonad NormalizeState a
forall (m :: Type -> Type) a. Monad m => a -> m a
return Term
e
        | Int
argLen Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
>= Int
2
        -> String -> RewriteMonad NormalizeState Term
forall a. HasCallStack => String -> a
error (String
"reduceNonRepPrim: tail bad args" String -> String -> String
forall a. Semigroup a => a -> a -> a
<> Term -> String
forall p. PrettyPrec p => p -> String
showPpr Term
e)

      Text
"Clash.Sized.Vector.last"
        | ([Term]
tmArgs,[Type
nTy,Type
aTy]) <- [Either Term Type] -> ([Term], [Type])
forall a b. [Either a b] -> ([a], [b])
Either.partitionEithers [Either Term Type]
args
        , (Right Type
argTy:[Either TyVar Type]
_) <- ([Either TyVar Type], Type) -> [Either TyVar Type]
forall a b. (a, b) -> a
fst (Type -> ([Either TyVar Type], Type)
splitFunForallTy (HasCallStack => TyConMap -> Type -> [Type] -> Type
TyConMap -> Type -> [Type] -> Type
piResultTys TyConMap
tcm (PrimInfo -> Type
primType PrimInfo
p) [Type
nTy,Type
aTy]))
        -> 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
n -> do
            shouldReduce1 <- [RewriteMonad NormalizeState Bool]
-> RewriteMonad NormalizeState Bool
forall (m :: Type -> Type). Monad m => [m Bool] -> m Bool
List.orM [ Context -> RewriteMonad NormalizeState Bool
shouldReduce Context
ctx
                                 , Type -> RewriteMonad NormalizeState Bool
forall {extra}. Type -> RewriteMonad extra Bool
isUntranslatableType_not_poly Type
aTy
                                 -- Note [Unroll shouldSplit types]
                                 , Bool -> RewriteMonad NormalizeState Bool
forall a. a -> RewriteMonad NormalizeState a
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure (Maybe ([Term] -> Term, Projections, [Type]) -> Bool
forall a. Maybe a -> Bool
Maybe.isJust (TyConMap -> Type -> Maybe ([Term] -> Term, Projections, [Type])
shouldSplit TyConMap
tcm Type
argTy))
                                 ]
            if shouldReduce1
               then abstractOverMissingArgs ticks tmArgs eTy c (reduceLast (n+1) aTy)
               else return e
          Either String Integer
_ -> Term -> RewriteMonad NormalizeState Term
forall a. a -> RewriteMonad NormalizeState a
forall (m :: Type -> Type) a. Monad m => a -> m a
return Term
e
        | Int
argLen Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
>= Int
2
        -> String -> RewriteMonad NormalizeState Term
forall a. HasCallStack => String -> a
error (String
"reduceNonRepPrim: last bad args" String -> String -> String
forall a. Semigroup a => a -> a -> a
<> Term -> String
forall p. PrettyPrec p => p -> String
showPpr Term
e)

      Text
"Clash.Sized.Vector.init"
        | ([Term]
tmArgs,[Type
nTy,Type
aTy]) <- [Either Term Type] -> ([Term], [Type])
forall a b. [Either a b] -> ([a], [b])
Either.partitionEithers [Either Term Type]
args
        , (Right Type
argTy:[Either TyVar Type]
_) <- ([Either TyVar Type], Type) -> [Either TyVar Type]
forall a b. (a, b) -> a
fst (Type -> ([Either TyVar Type], Type)
splitFunForallTy (HasCallStack => TyConMap -> Type -> [Type] -> Type
TyConMap -> Type -> [Type] -> Type
piResultTys TyConMap
tcm (PrimInfo -> Type
primType PrimInfo
p) [Type
nTy,Type
aTy]))
        -> 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
n -> do
            shouldReduce1 <- [RewriteMonad NormalizeState Bool]
-> RewriteMonad NormalizeState Bool
forall (m :: Type -> Type). Monad m => [m Bool] -> m Bool
List.orM [ Context -> RewriteMonad NormalizeState Bool
shouldReduce Context
ctx
                                 , Type -> RewriteMonad NormalizeState Bool
forall {extra}. Type -> RewriteMonad extra Bool
isUntranslatableType_not_poly Type
aTy
                                 -- Note [Unroll shouldSplit types]
                                 , Bool -> RewriteMonad NormalizeState Bool
forall a. a -> RewriteMonad NormalizeState a
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure (Maybe ([Term] -> Term, Projections, [Type]) -> Bool
forall a. Maybe a -> Bool
Maybe.isJust (TyConMap -> Type -> Maybe ([Term] -> Term, Projections, [Type])
shouldSplit TyConMap
tcm Type
argTy)) ]
            if shouldReduce1
               then abstractOverMissingArgs ticks tmArgs eTy c (reduceInit p n aTy)
               else return e
          Either String Integer
_ -> Term -> RewriteMonad NormalizeState Term
forall a. a -> RewriteMonad NormalizeState a
forall (m :: Type -> Type) a. Monad m => a -> m a
return Term
e
        | Int
argLen Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
>= Int
2
        -> String -> RewriteMonad NormalizeState Term
forall a. HasCallStack => String -> a
error (String
"reduceNonRepPrim: init bad args" String -> String -> String
forall a. Semigroup a => a -> a -> a
<> Term -> String
forall p. PrettyPrec p => p -> String
showPpr Term
e)

      Text
"Clash.Sized.Vector.unconcat"
        | ([Term]
tmArgs,[Type
nTy,Type
mTy,Type
aTy]) <- [Either Term Type] -> ([Term], [Type])
forall a b. [Either a b] -> ([a], [b])
Either.partitionEithers [Either Term Type]
args
        , (Either TyVar Type
_:Either TyVar Type
_:Right Type
argTy:[Either TyVar Type]
_) <- ([Either TyVar Type], Type) -> [Either TyVar Type]
forall a b. (a, b) -> a
fst (Type -> ([Either TyVar Type], Type)
splitFunForallTy (HasCallStack => TyConMap -> Type -> [Type] -> Type
TyConMap -> Type -> [Type] -> Type
piResultTys TyConMap
tcm (PrimInfo -> Type
primType PrimInfo
p) [Type
nTy,Type
mTy,Type
aTy]))
        -> 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), 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)) of
          (Right Integer
n, Right Integer
m) -> do
            shouldReduce1 <- [RewriteMonad NormalizeState Bool]
-> RewriteMonad NormalizeState Bool
forall (m :: Type -> Type). Monad m => [m Bool] -> m Bool
List.orM [ Bool -> RewriteMonad NormalizeState Bool
forall a. a -> RewriteMonad NormalizeState a
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure (Integer
mInteger -> Integer -> Bool
forall a. Eq a => a -> a -> Bool
==Integer
0)
                                      , Context -> RewriteMonad NormalizeState Bool
shouldReduce Context
ctx
                                      , Type -> RewriteMonad NormalizeState Bool
forall {extra}. Type -> RewriteMonad extra Bool
isUntranslatableType_not_poly Type
aTy
                                      --  Note [Unroll shouldSplit types]
                                      , Bool -> RewriteMonad NormalizeState Bool
forall a. a -> RewriteMonad NormalizeState a
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure (Maybe ([Term] -> Term, Projections, [Type]) -> Bool
forall a. Maybe a -> Bool
Maybe.isJust (TyConMap -> Type -> Maybe ([Term] -> Term, Projections, [Type])
shouldSplit TyConMap
tcm Type
argTy))
                                      ]
            if shouldReduce1 then
              abstractOverMissingArgs ticks tmArgs eTy c (reduceUnconcat p n m aTy)
            else
              return e
          (Either String Integer, Either String Integer)
_ -> Term -> RewriteMonad NormalizeState Term
forall a. a -> RewriteMonad NormalizeState a
forall (m :: Type -> Type) a. Monad m => a -> m a
return Term
e
        | Int
argLen Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
>= Int
3
        -> String -> RewriteMonad NormalizeState Term
forall a. HasCallStack => String -> a
error (String
"reduceNonRepPrim: unconcat bad args" String -> String -> String
forall a. Semigroup a => a -> a -> a
<> Term -> String
forall p. PrettyPrec p => p -> String
showPpr Term
e)

      Text
"Clash.Sized.Vector.transpose"
        | ([Term]
tmArgs,[Type
mTy,Type
nTy,Type
aTy]) <- [Either Term Type] -> ([Term], [Type])
forall a b. [Either a b] -> ([a], [b])
Either.partitionEithers [Either Term Type]
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), 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)) of
          (Right Integer
n, Right Integer
0) -> [TickInfo]
-> [Term]
-> Type
-> TransformContext
-> (Term
    -> Term -> TransformContext -> RewriteMonad NormalizeState Term)
-> RewriteMonad NormalizeState Term
forall a.
(AbstractOverMissingArgs a, HasCallStack) =>
[TickInfo]
-> [Term]
-> Type
-> TransformContext
-> a
-> RewriteMonad NormalizeState Term
abstractOverMissingArgs [TickInfo]
ticks [Term]
tmArgs Type
eTy TransformContext
c (Integer
-> Integer
-> Type
-> Term
-> Term
-> TransformContext
-> RewriteMonad NormalizeState Term
reduceTranspose Integer
n Integer
0 Type
aTy)
          (Either String Integer, Either String Integer)
_ -> Term -> RewriteMonad NormalizeState Term
forall a. a -> RewriteMonad NormalizeState a
forall (m :: Type -> Type) a. Monad m => a -> m a
return Term
e
        | Int
argLen Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
>= Int
3
        -> String -> RewriteMonad NormalizeState Term
forall a. HasCallStack => String -> a
error (String
"reduceNonRepPrim: transpose bad args" String -> String -> String
forall a. Semigroup a => a -> a -> a
<> Term -> String
forall p. PrettyPrec p => p -> String
showPpr Term
e)

      Text
"Clash.Sized.Vector.replicate"
        | ([Term]
tmArgs,[Type
nTy,Type
aTy]) <- [Either Term Type] -> ([Term], [Type])
forall a b. [Either a b] -> ([a], [b])
Either.partitionEithers [Either Term Type]
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
n -> do
            shouldReduce1 <- [RewriteMonad NormalizeState Bool]
-> RewriteMonad NormalizeState Bool
forall (m :: Type -> Type). Monad m => [m Bool] -> m Bool
List.orM [ Context -> RewriteMonad NormalizeState Bool
shouldReduce Context
ctx
                                 , Type -> RewriteMonad NormalizeState Bool
forall {extra}. Type -> RewriteMonad extra Bool
isUntranslatableType_not_poly Type
aTy
                                 -- Note [Unroll shouldSplit types]
                                 , Bool -> RewriteMonad NormalizeState Bool
forall a. a -> RewriteMonad NormalizeState a
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure (Maybe ([Term] -> Term, Projections, [Type]) -> Bool
forall a. Maybe a -> Bool
Maybe.isJust (TyConMap -> Type -> Maybe ([Term] -> Term, Projections, [Type])
shouldSplit TyConMap
tcm Type
resTy))
                                 ]
            if shouldReduce1
               then abstractOverMissingArgs ticks tmArgs eTy c (reduceReplicate n aTy resTy)
               else return e
          Either String Integer
_ -> Term -> RewriteMonad NormalizeState Term
forall a. a -> RewriteMonad NormalizeState a
forall (m :: Type -> Type) a. Monad m => a -> m a
return Term
e
        | Int
argLen Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
>= Int
2
        -> String -> RewriteMonad NormalizeState Term
forall a. HasCallStack => String -> a
error (String
"reduceNonRepPrim: replicate bad args" String -> String -> String
forall a. Semigroup a => a -> a -> a
<> Term -> String
forall p. PrettyPrec p => p -> String
showPpr Term
e)

       -- replace_int :: KnownNat n => Vec n a -> Int -> a -> Vec n a
      Text
"Clash.Sized.Vector.replace_int"
        | ([Term]
tmArgs,[Type
nTy,Type
aTy]) <- [Either Term Type] -> ([Term], [Type])
forall a b. [Either a b] -> ([a], [b])
Either.partitionEithers [Either Term Type]
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
n -> do
            shouldReduce1 <- [RewriteMonad NormalizeState Bool]
-> RewriteMonad NormalizeState Bool
forall (m :: Type -> Type). Monad m => [m Bool] -> m Bool
List.orM [ Bool -> RewriteMonad NormalizeState Bool
forall a. a -> RewriteMonad NormalizeState a
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure Bool
ultra
                                 , Context -> RewriteMonad NormalizeState Bool
shouldReduce Context
ctx
                                 , Type -> RewriteMonad NormalizeState Bool
forall {extra}. Type -> RewriteMonad extra Bool
isUntranslatableType_not_poly Type
aTy
                                 -- Note [Unroll shouldSplit types]
                                 , Bool -> RewriteMonad NormalizeState Bool
forall a. a -> RewriteMonad NormalizeState a
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure (Maybe ([Term] -> Term, Projections, [Type]) -> Bool
forall a. Maybe a -> Bool
Maybe.isJust (TyConMap -> Type -> Maybe ([Term] -> Term, Projections, [Type])
shouldSplit TyConMap
tcm Type
resTy))
                                 ]
            if shouldReduce1
               then abstractOverMissingArgs ticks tmArgs eTy c (reduceReplace_int n aTy resTy)
               else return e
          Either String Integer
_ -> Term -> RewriteMonad NormalizeState Term
forall a. a -> RewriteMonad NormalizeState a
forall (m :: Type -> Type) a. Monad m => a -> m a
return Term
e
        | Int
argLen Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
>= Int
2
        -> String -> RewriteMonad NormalizeState Term
forall a. HasCallStack => String -> a
error (String
"reduceNonRepPrim: replace_int bad args" String -> String -> String
forall a. Semigroup a => a -> a -> a
<> Term -> String
forall p. PrettyPrec p => p -> String
showPpr Term
e)

      Text
"Clash.Sized.Vector.index_int"
        | ([Term]
tmArgs,[Type
nTy,Type
aTy]) <- [Either Term Type] -> ([Term], [Type])
forall a b. [Either a b] -> ([a], [b])
Either.partitionEithers [Either Term Type]
args
        , (Either TyVar Type
_:Right Type
argTy:[Either TyVar Type]
_) <- ([Either TyVar Type], Type) -> [Either TyVar Type]
forall a b. (a, b) -> a
fst (Type -> ([Either TyVar Type], Type)
splitFunForallTy (HasCallStack => TyConMap -> Type -> [Type] -> Type
TyConMap -> Type -> [Type] -> Type
piResultTys TyConMap
tcm (PrimInfo -> Type
primType PrimInfo
p) [Type
nTy,Type
aTy]))
        -> 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
n -> do
            shouldReduce1 <- [RewriteMonad NormalizeState Bool]
-> RewriteMonad NormalizeState Bool
forall (m :: Type -> Type). Monad m => [m Bool] -> m Bool
List.orM [ Bool -> RewriteMonad NormalizeState Bool
forall a. a -> RewriteMonad NormalizeState a
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure Bool
ultra
                                 , Context -> RewriteMonad NormalizeState Bool
shouldReduce Context
ctx
                                 , Type -> RewriteMonad NormalizeState Bool
forall {extra}. Type -> RewriteMonad extra Bool
isUntranslatableType_not_poly Type
aTy
                                 -- Note [Unroll shouldSplit types]
                                 , Bool -> RewriteMonad NormalizeState Bool
forall a. a -> RewriteMonad NormalizeState a
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure (Maybe ([Term] -> Term, Projections, [Type]) -> Bool
forall a. Maybe a -> Bool
Maybe.isJust (TyConMap -> Type -> Maybe ([Term] -> Term, Projections, [Type])
shouldSplit TyConMap
tcm Type
argTy)) ]
            if shouldReduce1
               then abstractOverMissingArgs ticks tmArgs eTy c (reduceIndex_int n aTy)
               else return e
          Either String Integer
_ -> Term -> RewriteMonad NormalizeState Term
forall a. a -> RewriteMonad NormalizeState a
forall (m :: Type -> Type) a. Monad m => a -> m a
return Term
e
        | Int
argLen Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
>= Int
2
        -> String -> RewriteMonad NormalizeState Term
forall a. HasCallStack => String -> a
error (String
"reduceNonRepPrim: index_int bad args" String -> String -> String
forall a. Semigroup a => a -> a -> a
<> Term -> String
forall p. PrettyPrec p => p -> String
showPpr Term
e)

      Text
"Clash.Sized.Vector.imap"
        | ([Term]
tmArgs,[Type
nTy,Type
argElTy,Type
resElTy]) <- [Either Term Type] -> ([Term], [Type])
forall a b. [Either a b] -> ([a], [b])
Either.partitionEithers [Either Term Type]
args
        , TyConApp TyConName
vecTcNm [Type]
_ <- TypeView
tv
        , let argTy :: Type
argTy = TyConName -> [Type] -> Type
mkTyConApp TyConName
vecTcNm [Type
nTy,Type
argElTy]
        -> 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
n -> do
            shouldReduce1 <- [RewriteMonad NormalizeState Bool]
-> RewriteMonad NormalizeState Bool
forall (m :: Type -> Type). Monad m => [m Bool] -> m Bool
List.orM [ Bool -> RewriteMonad NormalizeState Bool
forall a. a -> RewriteMonad NormalizeState a
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure (Bool
ultra Bool -> Bool -> Bool
|| Integer
n Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
< Integer
2)
                                 , Context -> RewriteMonad NormalizeState Bool
shouldReduce Context
ctx
                                 , (Type -> RewriteMonad NormalizeState Bool)
-> [Type] -> RewriteMonad NormalizeState Bool
forall (m :: Type -> Type) a.
Monad m =>
(a -> m Bool) -> [a] -> m Bool
List.anyM Type -> RewriteMonad NormalizeState Bool
forall {extra}. Type -> RewriteMonad extra Bool
isUntranslatableType_not_poly [Type
argElTy,Type
resElTy]
                                 -- Note [Unroll shouldSplit types]
                                 , Bool -> RewriteMonad NormalizeState Bool
forall a. a -> RewriteMonad NormalizeState a
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure ((Type -> Bool) -> [Type] -> Bool
forall (t :: Type -> Type) a.
Foldable t =>
(a -> Bool) -> t a -> Bool
any (Maybe ([Term] -> Term, Projections, [Type]) -> Bool
forall a. Maybe a -> Bool
Maybe.isJust (Maybe ([Term] -> Term, Projections, [Type]) -> Bool)
-> (Type -> Maybe ([Term] -> Term, Projections, [Type]))
-> Type
-> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. TyConMap -> Type -> Maybe ([Term] -> Term, Projections, [Type])
shouldSplit TyConMap
tcm)
                                             [Type
argTy,Type
resTy]) ]
            if shouldReduce1
               then abstractOverMissingArgs ticks tmArgs eTy c (reduceImap n argElTy resElTy)
               else return e
          Either String Integer
_ -> Term -> RewriteMonad NormalizeState Term
forall a. a -> RewriteMonad NormalizeState a
forall (m :: Type -> Type) a. Monad m => a -> m a
return Term
e
        | Int
argLen Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
>= Int
3
        -> String -> RewriteMonad NormalizeState Term
forall a. HasCallStack => String -> a
error (String
"reduceNonRepPrim: imap bad args" String -> String -> String
forall a. Semigroup a => a -> a -> a
<> Term -> String
forall p. PrettyPrec p => p -> String
showPpr Term
e)

      Text
"Clash.Sized.Vector.iterateI"
        | ([Term]
tmArgs,[Type
nTy,Type
aTy]) <- [Either Term Type] -> ([Term], [Type])
forall a b. [Either a b] -> ([a], [b])
Either.partitionEithers [Either Term Type]
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
n -> do
            shouldReduce1 <- [RewriteMonad NormalizeState Bool]
-> RewriteMonad NormalizeState Bool
forall (m :: Type -> Type). Monad m => [m Bool] -> m Bool
List.orM
              [ Bool -> RewriteMonad NormalizeState Bool
forall a. a -> RewriteMonad NormalizeState a
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure (Bool
ultra Bool -> Bool -> Bool
|| Integer
n Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
< Integer
2)
              , Context -> RewriteMonad NormalizeState Bool
shouldReduce Context
ctx
              , Type -> RewriteMonad NormalizeState Bool
forall {extra}. Type -> RewriteMonad extra Bool
isUntranslatableType_not_poly Type
aTy
              -- Note [Unroll shouldSplit types]
              , Bool -> RewriteMonad NormalizeState Bool
forall a. a -> RewriteMonad NormalizeState a
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure (Maybe ([Term] -> Term, Projections, [Type]) -> Bool
forall a. Maybe a -> Bool
Maybe.isJust (TyConMap -> Type -> Maybe ([Term] -> Term, Projections, [Type])
shouldSplit TyConMap
tcm Type
resTy)) ]

            if shouldReduce1 then
              abstractOverMissingArgs ticks tmArgs eTy c (reduceIterateI n aTy resTy)
            else
              return e
          Either String Integer
_ -> Term -> RewriteMonad NormalizeState Term
forall a. a -> RewriteMonad NormalizeState a
forall (m :: Type -> Type) a. Monad m => a -> m a
return Term
e
        | Int
argLen Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
>= Int
2
        -> String -> RewriteMonad NormalizeState Term
forall a. HasCallStack => String -> a
error (String
"reduceNonRepPrim: iterateI bad args" String -> String -> String
forall a. Semigroup a => a -> a -> a
<> Term -> String
forall p. PrettyPrec p => p -> String
showPpr Term
e)

      Text
"Clash.Sized.Vector.dtfold"
        | ([Term]
tmArgs,[Type
_mTy,Type
nTy,Type
aTy]) <- [Either Term Type] -> ([Term], [Type])
forall a b. [Either a b] -> ([a], [b])
Either.partitionEithers [Either Term Type]
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
n -> [TickInfo]
-> [Term]
-> Type
-> TransformContext
-> (Term
    -> Term
    -> Term
    -> Term
    -> Term
    -> TransformContext
    -> RewriteMonad NormalizeState Term)
-> RewriteMonad NormalizeState Term
forall a.
(AbstractOverMissingArgs a, HasCallStack) =>
[TickInfo]
-> [Term]
-> Type
-> TransformContext
-> a
-> RewriteMonad NormalizeState Term
abstractOverMissingArgs [TickInfo]
ticks [Term]
tmArgs Type
eTy TransformContext
c (Integer
-> Type
-> Term
-> Term
-> Term
-> Term
-> Term
-> TransformContext
-> RewriteMonad NormalizeState Term
reduceDTFold Integer
n Type
aTy)
          Either String Integer
_ -> Term -> RewriteMonad NormalizeState Term
forall a. a -> RewriteMonad NormalizeState a
forall (m :: Type -> Type) a. Monad m => a -> m a
return Term
e
        | Int
argLen Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
>= Int
3
        -> String -> RewriteMonad NormalizeState Term
forall a. HasCallStack => String -> a
error (String
"reduceNonRepPrim: dtfold bad args" String -> String -> String
forall a. Semigroup a => a -> a -> a
<> Term -> String
forall p. PrettyPrec p => p -> String
showPpr Term
e)

      Text
"Clash.Sized.Vector.reverse"
        | Bool
ultra
        , ([Term]
tmArgs,[Type
nTy,Type
aTy]) <- [Either Term Type] -> ([Term], [Type])
forall a b. [Either a b] -> ([a], [b])
Either.partitionEithers [Either Term Type]
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)
        -> [TickInfo]
-> [Term]
-> Type
-> TransformContext
-> (Term -> TransformContext -> RewriteMonad NormalizeState Term)
-> RewriteMonad NormalizeState Term
forall a.
(AbstractOverMissingArgs a, HasCallStack) =>
[TickInfo]
-> [Term]
-> Type
-> TransformContext
-> a
-> RewriteMonad NormalizeState Term
abstractOverMissingArgs [TickInfo]
ticks [Term]
tmArgs Type
eTy TransformContext
c (Integer
-> Type
-> Term
-> TransformContext
-> RewriteMonad NormalizeState Term
reduceReverse Integer
n Type
aTy)

      Text
"Clash.Sized.RTree.tdfold"
        | ([Term]
tmArgs,[Type
_mTy,Type
nTy,Type
aTy]) <- [Either Term Type] -> ([Term], [Type])
forall a b. [Either a b] -> ([a], [b])
Either.partitionEithers [Either Term Type]
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
n -> [TickInfo]
-> [Term]
-> Type
-> TransformContext
-> (Term
    -> Term
    -> Term
    -> Term
    -> Term
    -> TransformContext
    -> RewriteMonad NormalizeState Term)
-> RewriteMonad NormalizeState Term
forall a.
(AbstractOverMissingArgs a, HasCallStack) =>
[TickInfo]
-> [Term]
-> Type
-> TransformContext
-> a
-> RewriteMonad NormalizeState Term
abstractOverMissingArgs [TickInfo]
ticks [Term]
tmArgs Type
eTy TransformContext
c (Integer
-> Type
-> Term
-> Term
-> Term
-> Term
-> Term
-> TransformContext
-> RewriteMonad NormalizeState Term
reduceTFold Integer
n Type
aTy)
          Either String Integer
_ -> Term -> RewriteMonad NormalizeState Term
forall a. a -> RewriteMonad NormalizeState a
forall (m :: Type -> Type) a. Monad m => a -> m a
return Term
e
        | Int
argLen Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
>= Int
3
        -> String -> RewriteMonad NormalizeState Term
forall a. HasCallStack => String -> a
error (String
"reduceNonRepPrim: tdfold bad args" String -> String -> String
forall a. Semigroup a => a -> a -> a
<> Term -> String
forall p. PrettyPrec p => p -> String
showPpr Term
e)
      Text
"Clash.Sized.RTree.treplicate"
        | ([Term]
tmArgs,[Type
nTy,Type
aTy]) <- [Either Term Type] -> ([Term], [Type])
forall a b. [Either a b] -> ([a], [b])
Either.partitionEithers [Either Term Type]
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
n -> do
            shouldReduce1 <- [RewriteMonad NormalizeState Bool]
-> RewriteMonad NormalizeState Bool
forall (m :: Type -> Type). Monad m => [m Bool] -> m Bool
List.orM [ Context -> RewriteMonad NormalizeState Bool
shouldReduce Context
ctx
                                 , Bool -> Type -> RewriteMonad NormalizeState Bool
forall extra. Bool -> Type -> RewriteMonad extra Bool
isUntranslatableType Bool
False Type
aTy ]
            if shouldReduce1
               then abstractOverMissingArgs ticks tmArgs eTy c (reduceTReplicate n aTy resTy)
               else return e
          Either String Integer
_ -> Term -> RewriteMonad NormalizeState Term
forall a. a -> RewriteMonad NormalizeState a
forall (m :: Type -> Type) a. Monad m => a -> m a
return Term
e
        | Int
argLen Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
>= Int
2
        -> String -> RewriteMonad NormalizeState Term
forall a. HasCallStack => String -> a
error (String
"reduceNonRepPrim: treplicate bad args" String -> String -> String
forall a. Semigroup a => a -> a -> a
<> Term -> String
forall p. PrettyPrec p => p -> String
showPpr Term
e)
      Text
"Clash.Sized.Internal.BitVector.split#"
        | ([Term]
tmArgs,[Type
nTy,Type
mTy]) <- [Either Term Type] -> ([Term], [Type])
forall a b. [Either a b] -> ([a], [b])
Either.partitionEithers [Either Term Type]
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), 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), TypeView
tv) of
          (Right Integer
n, Right Integer
m, TyConApp TyConName
tupTcNm [Type
lTy,Type
rTy])
            | Integer
n Integer -> Integer -> Bool
forall a. Eq a => a -> a -> Bool
== Integer
0 -> [TickInfo]
-> [Term]
-> Type
-> TransformContext
-> (Term
    -> Term -> TransformContext -> RewriteMonad NormalizeState Term)
-> RewriteMonad NormalizeState Term
forall a.
(AbstractOverMissingArgs a, HasCallStack) =>
[TickInfo]
-> [Term]
-> Type
-> TransformContext
-> a
-> RewriteMonad NormalizeState Term
abstractOverMissingArgs [TickInfo]
ticks [Term]
tmArgs Type
eTy TransformContext
c ((Term
  -> Term -> TransformContext -> RewriteMonad NormalizeState Term)
 -> RewriteMonad NormalizeState Term)
-> (Term
    -> Term -> TransformContext -> RewriteMonad NormalizeState Term)
-> RewriteMonad NormalizeState Term
forall a b. (a -> b) -> a -> b
$ \(Term
_kn :: Term) Term
bvArg (TransformContext
_ctx :: TransformContext) -> do
              let tup :: Term
tup = Term -> [Either Term Type] -> Term
mkApps (DataCon -> Term
Data DataCon
tupDc)
                           [Type -> Either Term Type
forall a b. b -> Either a b
Right Type
lTy
                           ,Type -> Either Term Type
forall a b. b -> Either a b
Right Type
rTy
                           ,Term -> Either Term Type
forall a b. a -> Either a b
Left  Term
bvArg
                           ,Term -> Either Term Type
forall a b. a -> Either a b
Left  (Term -> Type -> Term
TyApp (PrimInfo -> Term
Prim PrimInfo
removedArg) Type
rTy)
                           ]

              (Term -> RewriteMonad NormalizeState Term
forall a extra. a -> RewriteMonad extra a
changed (Term -> [TickInfo] -> Term
mkTicks Term
tup [TickInfo]
ticks) :: NormalizeSession Term)
            | Integer
m Integer -> Integer -> Bool
forall a. Eq a => a -> a -> Bool
== Integer
0 -> [TickInfo]
-> [Term]
-> Type
-> TransformContext
-> (Term
    -> Term -> TransformContext -> RewriteMonad NormalizeState Term)
-> RewriteMonad NormalizeState Term
forall a.
(AbstractOverMissingArgs a, HasCallStack) =>
[TickInfo]
-> [Term]
-> Type
-> TransformContext
-> a
-> RewriteMonad NormalizeState Term
abstractOverMissingArgs [TickInfo]
ticks [Term]
tmArgs Type
eTy TransformContext
c ((Term
  -> Term -> TransformContext -> RewriteMonad NormalizeState Term)
 -> RewriteMonad NormalizeState Term)
-> (Term
    -> Term -> TransformContext -> RewriteMonad NormalizeState Term)
-> RewriteMonad NormalizeState Term
forall a b. (a -> b) -> a -> b
$ \(Term
_kn :: Term) Term
bvArg (TransformContext
_ctx :: TransformContext) -> do
              let tup :: Term
tup = Term -> [Either Term Type] -> Term
mkApps (DataCon -> Term
Data DataCon
tupDc)
                           [Type -> Either Term Type
forall a b. b -> Either a b
Right Type
lTy
                           ,Type -> Either Term Type
forall a b. b -> Either a b
Right Type
rTy
                           ,Term -> Either Term Type
forall a b. a -> Either a b
Left  (Term -> Type -> Term
TyApp (PrimInfo -> Term
Prim PrimInfo
removedArg) Type
lTy)
                           ,Term -> Either Term Type
forall a b. a -> Either a b
Left  Term
bvArg
                           ]

              (Term -> RewriteMonad NormalizeState Term
forall a extra. a -> RewriteMonad extra a
changed (Term -> [TickInfo] -> Term
mkTicks Term
tup [TickInfo]
ticks) :: NormalizeSession Term)
           where
            tupDc :: DataCon
tupDc = DataCon -> Maybe DataCon -> DataCon
forall a. a -> Maybe a -> a
fromMaybe (String -> DataCon
forall a. HasCallStack => String -> a
error String
"reduceNonRepPrim: faield to create tup DC") (Maybe DataCon -> DataCon) -> Maybe DataCon -> DataCon
forall a b. (a -> b) -> a -> b
$ do
                    tupTc <- TyConName -> TyConMap -> Maybe TyCon
forall a b. Uniquable a => a -> UniqMap b -> Maybe b
UniqMap.lookup TyConName
tupTcNm TyConMap
tcm
                    listToMaybe (tyConDataCons tupTc)
          (Either String Integer, Either String Integer, TypeView)
_ -> Term -> RewriteMonad NormalizeState Term
forall a. a -> RewriteMonad NormalizeState a
forall (m :: Type -> Type) a. Monad m => a -> m a
return Term
e
        | Int
argLen Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
>= Int
3
        -> String -> RewriteMonad NormalizeState Term
forall a. HasCallStack => String -> a
error (String
"reduceNonRepPrim: split# bad args" String -> String -> String
forall a. Semigroup a => a -> a -> a
<> Term -> String
forall p. PrettyPrec p => p -> String
showPpr Term
e)
      Text
"Clash.Sized.Internal.BitVector.eq#"
        | ([Term]
tmArgs,[Type
nTy]) <- [Either Term Type] -> ([Term], [Type])
forall a b. [Either a b] -> ([a], [b])
Either.partitionEithers [Either Term Type]
args
        , Right Integer
0 <- Except String Integer -> Either String Integer
forall e a. Except e a -> Either e a
runExcept (TyConMap -> Type -> Except String Integer
tyNatSize TyConMap
tcm Type
nTy)
        , TyConApp TyConName
boolTcNm [] <- TypeView
tv
        -> [TickInfo]
-> [Term]
-> Type
-> TransformContext
-> (Term
    -> Term
    -> Term
    -> TransformContext
    -> RewriteMonad NormalizeState Term)
-> RewriteMonad NormalizeState Term
forall a.
(AbstractOverMissingArgs a, HasCallStack) =>
[TickInfo]
-> [Term]
-> Type
-> TransformContext
-> a
-> RewriteMonad NormalizeState Term
abstractOverMissingArgs [TickInfo]
ticks [Term]
tmArgs Type
eTy TransformContext
c ((Term
  -> Term
  -> Term
  -> TransformContext
  -> RewriteMonad NormalizeState Term)
 -> RewriteMonad NormalizeState Term)
-> (Term
    -> Term
    -> Term
    -> TransformContext
    -> RewriteMonad NormalizeState Term)
-> RewriteMonad NormalizeState Term
forall a b. (a -> b) -> a -> b
$ \(Term
_kn :: Term) (Term
_l :: Term) (Term
_r :: Term) (TransformContext
_ctx :: TransformContext) -> do
           let trueDc :: DataCon
trueDc = DataCon -> Maybe DataCon -> DataCon
forall a. a -> Maybe a -> a
fromMaybe (String -> DataCon
forall a. HasCallStack => String -> a
error String
"reduceNonRepPrim: failed to create True DC") (Maybe DataCon -> DataCon) -> Maybe DataCon -> DataCon
forall a b. (a -> b) -> a -> b
$ do
                  boolTc <- TyConName -> TyConMap -> Maybe TyCon
forall a b. Uniquable a => a -> UniqMap b -> Maybe b
UniqMap.lookup TyConName
boolTcNm TyConMap
tcm
                  [_falseDc,dc] <- pure (tyConDataCons boolTc)
                  return dc
            in (Term -> RewriteMonad NormalizeState Term
forall a extra. a -> RewriteMonad extra a
changed (DataCon -> Term
Data DataCon
trueDc) :: NormalizeSession Term)
      Text
_ -> Term -> RewriteMonad NormalizeState Term
forall a. a -> RewriteMonad NormalizeState a
forall (m :: Type -> Type) a. Monad m => a -> m a
return Term
e
  where
    isUntranslatableType_not_poly :: Type -> RewriteMonad extra Bool
isUntranslatableType_not_poly Type
t = do
      u <- Bool -> Type -> RewriteMonad extra Bool
forall extra. Bool -> Type -> RewriteMonad extra Bool
isUntranslatableType Bool
False Type
t
      if u
         then return (null $ Lens.toListOf typeFreeVars t)
         else return False

reduceNonRepPrim TransformContext
_ Term
e = Term -> RewriteMonad NormalizeState Term
forall a. a -> RewriteMonad NormalizeState a
forall (m :: Type -> Type) a. Monad m => a -> m a
return Term
e
{-# SCC reduceNonRepPrim #-}

class AbstractOverMissingArgs a where
  -- | Abstract over a primitive until it is saturated
  abstractOverMissingArgs ::
    HasCallStack =>
    -- | Ticks originally tagged to the applied primitive
    [TickInfo] ->
    -- | Available arguments
    [Term] ->
    -- | The type of the expression containing the applied primitive
    Type ->
    -- | The context in which reduceNonRepPrim was called
    TransformContext ->
    a ->
    NormalizeSession Term

instance AbstractOverMissingArgs (TransformContext -> NormalizeSession Term) where
  abstractOverMissingArgs :: HasCallStack =>
[TickInfo]
-> [Term]
-> Type
-> TransformContext
-> (TransformContext -> RewriteMonad NormalizeState Term)
-> RewriteMonad NormalizeState Term
abstractOverMissingArgs [TickInfo]
ticks [Term]
args Type
_ TransformContext
is TransformContext -> RewriteMonad NormalizeState Term
f = (Term -> [Term] -> Term
`mkTmApps` [Term]
args) (Term -> Term) -> (Term -> Term) -> Term -> Term
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> (Term -> [TickInfo] -> Term
`mkTicks` [TickInfo]
ticks) (Term -> Term)
-> RewriteMonad NormalizeState Term
-> RewriteMonad NormalizeState Term
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> TransformContext -> RewriteMonad NormalizeState Term
f TransformContext
is

instance AbstractOverMissingArgs a => AbstractOverMissingArgs (Term -> a) where
  abstractOverMissingArgs :: HasCallStack =>
[TickInfo]
-> [Term]
-> Type
-> TransformContext
-> (Term -> a)
-> RewriteMonad NormalizeState Term
abstractOverMissingArgs [TickInfo]
ticks (Term
t:[Term]
ts) Type
ty TransformContext
ctx Term -> a
f = [TickInfo]
-> [Term]
-> Type
-> TransformContext
-> a
-> RewriteMonad NormalizeState Term
forall a.
(AbstractOverMissingArgs a, HasCallStack) =>
[TickInfo]
-> [Term]
-> Type
-> TransformContext
-> a
-> RewriteMonad NormalizeState Term
abstractOverMissingArgs [TickInfo]
ticks [Term]
ts Type
ty TransformContext
ctx (Term -> a
f Term
t)
  abstractOverMissingArgs [TickInfo]
ticks []     (Type -> TypeView
tyView -> FunTy Type
argTy Type
resTy) (TransformContext InScopeSet
is0 Context
ctx) Term -> a
f = do
     newId <- InScopeSet -> Text -> Type -> RewriteMonad NormalizeState Id
forall (m :: Type -> Type).
MonadUnique m =>
InScopeSet -> Text -> Type -> m Id
mkInternalVar InScopeSet
is0 Text
"arg" Type
argTy
     let ctx1 = InScopeSet -> Context -> TransformContext
TransformContext (InScopeSet -> Id -> InScopeSet
forall a. InScopeSet -> Var a -> InScopeSet
extendInScopeSet InScopeSet
is0 Id
newId) (Id -> CoreContext
LamBody Id
newId CoreContext -> Context -> Context
forall a. a -> [a] -> [a]
: Context
ctx)
     Lam newId <$> abstractOverMissingArgs ticks [] resTy ctx1 (f (Var newId))
  abstractOverMissingArgs [TickInfo]
_ [Term]
_ Type
ty TransformContext
_ Term -> a
_ = String -> RewriteMonad NormalizeState Term
forall a. HasCallStack => String -> a
error (String
"not a funty: " String -> String -> String
forall a. Semigroup a => a -> a -> a
<> Type -> String
forall p. PrettyPrec p => p -> String
showPpr Type
ty)