{-|
  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 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 GHC.Stack (HasCallStack)

import Clash.Core.FreeVars (typeFreeVars)
import Clash.Core.HasType
import Clash.Core.Name (nameOcc)
import Clash.Core.Subst (Subst, extendIdSubst, substTm)
import Clash.Core.Term
  ( LetBinding, PrimInfo(..), Term(..), TickInfo(..), collectArgs
  , collectArgsTicks, mkApps, mkTicks)
import Clash.Core.TyCon (tyConDataCons)
import Clash.Core.Type (TypeView(..), mkTyConApp, tyView)
import Clash.Core.Util (mkVec, shouldSplit, tyNatSize)
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)
import Clash.Unique (lookupUniqMap)

-- | 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 (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 :: 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 (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 (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 :: NormRewrite
reduceNonRepPrim c :: TransformContext
c@(TransformContext InScopeSet
is0 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
  TyConMap
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
  Bool
ultra <- Getting Bool RewriteEnv Bool -> RewriteMonad NormalizeState Bool
forall s (m :: Type -> Type) a.
MonadReader s m =>
Getting a s a -> m a
Lens.view Getting Bool RewriteEnv Bool
Getter RewriteEnv Bool
normalizeUltra
  let eTy :: Type
eTy = TyConMap -> Term -> Type
forall a. InferType a => TyConMap -> a -> Type
inferCoreTypeOf TyConMap
tcm Term
e
  case Type -> TypeView
tyView Type
eTy 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 (Just TyCon
vecTc) = TyConName -> TyConMap -> Maybe TyCon
forall a b. Uniquable a => a -> UniqMap b -> Maybe b
lookupUniqMap TyConName
vecTcNm TyConMap
tcm
          [DataCon
nilCon,DataCon
consCon] = TyCon -> [DataCon]
tyConDataCons TyCon
vecTc
          nilE :: Term
nilE = DataCon -> DataCon -> Type -> Integer -> [Term] -> Term
mkVec DataCon
nilCon DataCon
consCon Type
aTy Integer
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 (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" | Int
argLen Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
7 -> do
        let [Type
lhsElTy,Type
rhsElty,Type
resElTy,Type
nTy] = [Either Term Type] -> [Type]
forall a b. [Either a b] -> [b]
Either.rights [Either Term Type]
args
            TyConApp TyConName
vecTcNm [Type]
_ = TypeView
tv
            lhsTy :: Type
lhsTy = TyConName -> [Type] -> Type
mkTyConApp TyConName
vecTcNm [Type
nTy,Type
lhsElTy]
            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
            Bool
shouldReduce1 <- [RewriteMonad NormalizeState Bool]
-> RewriteMonad NormalizeState Bool
forall (m :: Type -> Type). Monad m => [m Bool] -> m Bool
List.orM [ Bool -> RewriteMonad NormalizeState Bool
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 (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
eTy]) ]
            if Bool
shouldReduce1
               then let [Term
fun,Term
lhsArg,Term
rhsArg] = [Either Term Type] -> [Term]
forall a b. [Either a b] -> [a]
Either.lefts [Either Term Type]
args
                    in  (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
-> PrimInfo
-> Integer
-> Type
-> Type
-> Type
-> Term
-> Term
-> Term
-> RewriteMonad NormalizeState Term
reduceZipWith TransformContext
c PrimInfo
p Integer
n Type
lhsElTy Type
rhsElty Type
resElTy Term
fun Term
lhsArg Term
rhsArg
               else Term -> RewriteMonad NormalizeState Term
forall (m :: Type -> Type) a. Monad m => a -> m a
return Term
e
          Either String Integer
_ -> Term -> RewriteMonad NormalizeState Term
forall (m :: Type -> Type) a. Monad m => a -> m a
return Term
e
      Text
"Clash.Sized.Vector.map" | Int
argLen Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
5 -> do
        let [Type
argElTy,Type
resElTy,Type
nTy] = [Either Term Type] -> [Type]
forall a b. [Either a b] -> [b]
Either.rights [Either Term Type]
args
            TyConApp TyConName
vecTcNm [Type]
_ = TypeView
tv
            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
            Bool
shouldReduce1 <- [RewriteMonad NormalizeState Bool]
-> RewriteMonad NormalizeState Bool
forall (m :: Type -> Type). Monad m => [m Bool] -> m Bool
List.orM [ Bool -> RewriteMonad NormalizeState Bool
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 (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
eTy]) ]
            if Bool
shouldReduce1
               then let [Term
fun,Term
arg] = [Either Term Type] -> [Term]
forall a b. [Either a b] -> [a]
Either.lefts [Either Term Type]
args
                    in  (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
-> PrimInfo
-> Integer
-> Type
-> Type
-> Term
-> Term
-> RewriteMonad NormalizeState Term
reduceMap TransformContext
c PrimInfo
p Integer
n Type
argElTy Type
resElTy Term
fun Term
arg
               else Term -> RewriteMonad NormalizeState Term
forall (m :: Type -> Type) a. Monad m => a -> m a
return Term
e
          Either String Integer
_ -> Term -> RewriteMonad NormalizeState Term
forall (m :: Type -> Type) a. Monad m => a -> m a
return Term
e
      Text
"Clash.Sized.Vector.traverse#" | Int
argLen Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
7 ->
        let [Type
aTy,Type
fTy,Type
bTy,Type
nTy] = [Either Term Type] -> [Type]
forall a b. [Either a b] -> [b]
Either.rights [Either Term Type]
args
        in  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 ->
            let [Term
dict,Term
fun,Term
arg] = [Either Term Type] -> [Term]
forall a b. [Either a b] -> [a]
Either.lefts [Either Term Type]
args
            in  (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
-> Integer
-> Type
-> Type
-> Type
-> Term
-> Term
-> Term
-> RewriteMonad NormalizeState Term
reduceTraverse TransformContext
c Integer
n Type
aTy Type
fTy Type
bTy Term
dict Term
fun Term
arg
          Either String Integer
_ -> Term -> RewriteMonad NormalizeState Term
forall (m :: Type -> Type) a. Monad m => a -> m a
return Term
e
      Text
"Clash.Sized.Vector.fold" | Int
argLen Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
4 -> do
        let ([Term
fun,Term
arg],[Type
nTy,Type
aTy]) = [Either Term Type] -> ([Term], [Type])
forall a b. [Either a b] -> ([a], [b])
Either.partitionEithers [Either Term Type]
args
            argTy :: Type
argTy = TyConMap -> Term -> Type
forall a. InferType a => TyConMap -> a -> Type
inferCoreTypeOf TyConMap
tcm Term
arg
        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
            Bool
shouldReduce1 <- [RewriteMonad NormalizeState Bool]
-> RewriteMonad NormalizeState Bool
forall (m :: Type -> Type). Monad m => [m Bool] -> m Bool
List.orM [ Bool -> RewriteMonad NormalizeState Bool
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 (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 Bool
shouldReduce1 then
              (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
-> Integer
-> Type
-> Term
-> Term
-> RewriteMonad NormalizeState Term
reduceFold TransformContext
c (Integer
n Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
+ Integer
1) Type
aTy Term
fun Term
arg
            else Term -> RewriteMonad NormalizeState Term
forall (m :: Type -> Type) a. Monad m => a -> m a
return Term
e
          Either String Integer
_ -> Term -> RewriteMonad NormalizeState Term
forall (m :: Type -> Type) a. Monad m => a -> m a
return Term
e
      Text
"Clash.Sized.Vector.foldr" | Int
argLen Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
6 ->
        let ([Term
fun,Term
start,Term
arg],[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
            argTy :: Type
argTy = TyConMap -> Term -> Type
forall a. InferType a => TyConMap -> a -> Type
inferCoreTypeOf TyConMap
tcm Term
arg
        in  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
            Bool
shouldReduce1 <- [RewriteMonad NormalizeState Bool]
-> RewriteMonad NormalizeState Bool
forall (m :: Type -> Type). Monad m => [m Bool] -> m Bool
List.orM [ Bool -> RewriteMonad NormalizeState Bool
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 (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 Bool
shouldReduce1
              then (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
-> PrimInfo
-> Integer
-> Type
-> Term
-> Term
-> Term
-> RewriteMonad NormalizeState Term
reduceFoldr TransformContext
c PrimInfo
p Integer
n Type
aTy Term
fun Term
start Term
arg
              else Term -> RewriteMonad NormalizeState Term
forall (m :: Type -> Type) a. Monad m => a -> m a
return Term
e
          Either String Integer
_ -> Term -> RewriteMonad NormalizeState Term
forall (m :: Type -> Type) a. Monad m => a -> m a
return Term
e
      Text
"Clash.Sized.Vector.dfold" | Int
argLen Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
8 ->
        let ([Term
_kn,Term
_motive,Term
fun,Term
start,Term
arg],[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
        in  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 -> (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
<$> InScopeSet
-> Integer
-> Type
-> Term
-> Term
-> Term
-> RewriteMonad NormalizeState Term
reduceDFold InScopeSet
is0 Integer
n Type
aTy Term
fun Term
start Term
arg
          Either String Integer
_ -> Term -> RewriteMonad NormalizeState Term
forall (m :: Type -> Type) a. Monad m => a -> m a
return Term
e
      Text
"Clash.Sized.Vector.++" | Int
argLen Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
5 ->
        let [Type
nTy,Type
aTy,Type
mTy] = [Either Term Type] -> [Type]
forall a b. [Either a b] -> [b]
Either.rights [Either Term Type]
args
            [Term
lArg,Term
rArg]   = [Either Term Type] -> [Term]
forall a b. [Either a b] -> [a]
Either.lefts [Either Term Type]
args
        in 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)
                | Integer
n Integer -> Integer -> Bool
forall a. Eq a => a -> a -> Bool
== Integer
0 -> Term -> RewriteMonad NormalizeState Term
forall a extra. a -> RewriteMonad extra a
changed Term
rArg
                | Integer
m Integer -> Integer -> Bool
forall a. Eq a => a -> a -> Bool
== Integer
0 -> Term -> RewriteMonad NormalizeState Term
forall a extra. a -> RewriteMonad extra a
changed Term
lArg
                | Bool
otherwise -> do
                    Bool
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 (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
eTy)) ]
                    if Bool
shouldReduce1
                       then (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
<$> InScopeSet
-> Integer
-> Integer
-> Type
-> Term
-> Term
-> RewriteMonad NormalizeState Term
reduceAppend InScopeSet
is0 Integer
n Integer
m Type
aTy Term
lArg Term
rArg
                       else Term -> RewriteMonad NormalizeState Term
forall (m :: Type -> Type) a. Monad m => a -> m a
return Term
e
              (Either String Integer, Either String Integer)
_ -> Term -> RewriteMonad NormalizeState Term
forall (m :: Type -> Type) a. Monad m => a -> m a
return Term
e
      Text
"Clash.Sized.Vector.head" | Int
argLen Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
3 -> do
        let [Type
nTy,Type
aTy] = [Either Term Type] -> [Type]
forall a b. [Either a b] -> [b]
Either.rights [Either Term Type]
args
            [Term
vArg]    = [Either Term Type] -> [Term]
forall a b. [Either a b] -> [a]
Either.lefts [Either Term Type]
args
            argTy :: Type
argTy     = TyConMap -> Term -> Type
forall a. InferType a => TyConMap -> a -> Type
inferCoreTypeOf TyConMap
tcm Term
vArg
        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
            Bool
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 (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 Bool
shouldReduce1
               then (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
<$> InScopeSet
-> Integer -> Type -> Term -> RewriteMonad NormalizeState Term
reduceHead InScopeSet
is0 (Integer
nInteger -> Integer -> Integer
forall a. Num a => a -> a -> a
+Integer
1) Type
aTy Term
vArg
               else Term -> RewriteMonad NormalizeState Term
forall (m :: Type -> Type) a. Monad m => a -> m a
return Term
e
          Either String Integer
_ -> Term -> RewriteMonad NormalizeState Term
forall (m :: Type -> Type) a. Monad m => a -> m a
return Term
e
      Text
"Clash.Sized.Vector.tail" | Int
argLen Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
3 -> do
        let [Type
nTy,Type
aTy] = [Either Term Type] -> [Type]
forall a b. [Either a b] -> [b]
Either.rights [Either Term Type]
args
            [Term
vArg]    = [Either Term Type] -> [Term]
forall a b. [Either a b] -> [a]
Either.lefts [Either Term Type]
args
            argTy :: Type
argTy     = TyConMap -> Term -> Type
forall a. InferType a => TyConMap -> a -> Type
inferCoreTypeOf TyConMap
tcm Term
vArg
        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
            Bool
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 (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 Bool
shouldReduce1
               then (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
<$> InScopeSet
-> Integer -> Type -> Term -> RewriteMonad NormalizeState Term
reduceTail InScopeSet
is0 (Integer
nInteger -> Integer -> Integer
forall a. Num a => a -> a -> a
+Integer
1) Type
aTy Term
vArg
               else Term -> RewriteMonad NormalizeState Term
forall (m :: Type -> Type) a. Monad m => a -> m a
return Term
e
          Either String Integer
_ -> Term -> RewriteMonad NormalizeState Term
forall (m :: Type -> Type) a. Monad m => a -> m a
return Term
e
      Text
"Clash.Sized.Vector.last" | Int
argLen Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
3 -> do
        let [Type
nTy,Type
aTy] = [Either Term Type] -> [Type]
forall a b. [Either a b] -> [b]
Either.rights [Either Term Type]
args
            [Term
vArg]    = [Either Term Type] -> [Term]
forall a b. [Either a b] -> [a]
Either.lefts [Either Term Type]
args
            argTy :: Type
argTy     = TyConMap -> Term -> Type
forall a. InferType a => TyConMap -> a -> Type
inferCoreTypeOf TyConMap
tcm Term
vArg
        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
            Bool
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 (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 Bool
shouldReduce1
               then (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
<$> InScopeSet
-> Integer -> Type -> Term -> RewriteMonad NormalizeState Term
reduceLast InScopeSet
is0 (Integer
nInteger -> Integer -> Integer
forall a. Num a => a -> a -> a
+Integer
1) Type
aTy Term
vArg
               else Term -> RewriteMonad NormalizeState Term
forall (m :: Type -> Type) a. Monad m => a -> m a
return Term
e
          Either String Integer
_ -> Term -> RewriteMonad NormalizeState Term
forall (m :: Type -> Type) a. Monad m => a -> m a
return Term
e
      Text
"Clash.Sized.Vector.init" | Int
argLen Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
3 -> do
        let [Type
nTy,Type
aTy] = [Either Term Type] -> [Type]
forall a b. [Either a b] -> [b]
Either.rights [Either Term Type]
args
            [Term
vArg]    = [Either Term Type] -> [Term]
forall a b. [Either a b] -> [a]
Either.lefts [Either Term Type]
args
            argTy :: Type
argTy     = TyConMap -> Term -> Type
forall a. InferType a => TyConMap -> a -> Type
inferCoreTypeOf TyConMap
tcm Term
vArg
        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
            Bool
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 (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 Bool
shouldReduce1
               then (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
<$> InScopeSet
-> PrimInfo
-> Integer
-> Type
-> Term
-> RewriteMonad NormalizeState Term
reduceInit InScopeSet
is0 PrimInfo
p Integer
n Type
aTy Term
vArg
               else Term -> RewriteMonad NormalizeState Term
forall (m :: Type -> Type) a. Monad m => a -> m a
return Term
e
          Either String Integer
_ -> Term -> RewriteMonad NormalizeState Term
forall (m :: Type -> Type) a. Monad m => a -> m a
return Term
e
      Text
"Clash.Sized.Vector.unconcat" | Int
argLen Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
6 -> do
        let ([Term
_knN,Term
sm,Term
arg],[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
            argTy :: Type
argTy = TyConMap -> Term -> Type
forall a. InferType a => TyConMap -> a -> Type
inferCoreTypeOf TyConMap
tcm Term
arg
        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
            Bool
shouldReduce1 <- [RewriteMonad NormalizeState Bool]
-> RewriteMonad NormalizeState Bool
forall (m :: Type -> Type). Monad m => [m Bool] -> m Bool
List.orM [ Bool -> RewriteMonad NormalizeState Bool
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 (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 Bool
shouldReduce1 then
              (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
<$> InScopeSet
-> PrimInfo
-> Integer
-> Integer
-> Type
-> Term
-> Term
-> RewriteMonad NormalizeState Term
reduceUnconcat InScopeSet
is0 PrimInfo
p Integer
n Integer
m Type
aTy Term
sm Term
arg
            else
              Term -> RewriteMonad NormalizeState Term
forall (m :: Type -> Type) a. Monad m => a -> m a
return Term
e
          (Either String Integer, Either String Integer)
_ -> Term -> RewriteMonad NormalizeState Term
forall (m :: Type -> Type) a. Monad m => a -> m a
return Term
e
      Text
"Clash.Sized.Vector.transpose" | Int
argLen Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
5 -> do
        let ([Term
_knN,Term
arg],[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) -> (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
<$> Integer
-> Integer -> Type -> Term -> RewriteMonad NormalizeState Term
reduceTranspose Integer
n Integer
0 Type
aTy Term
arg
          (Either String Integer, Either String Integer)
_ -> Term -> RewriteMonad NormalizeState Term
forall (m :: Type -> Type) a. Monad m => a -> m a
return Term
e
      Text
"Clash.Sized.Vector.replicate" | Int
argLen Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
4 -> do
        let ([Term
_sArg,Term
vArg],[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
            Bool
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 (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
eTy))
                                 ]
            if Bool
shouldReduce1
               then (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
<$> Integer -> Type -> Type -> Term -> RewriteMonad NormalizeState Term
reduceReplicate Integer
n Type
aTy Type
eTy Term
vArg
               else Term -> RewriteMonad NormalizeState Term
forall (m :: Type -> Type) a. Monad m => a -> m a
return Term
e
          Either String Integer
_ -> Term -> RewriteMonad NormalizeState Term
forall (m :: Type -> Type) a. Monad m => a -> m a
return Term
e
       -- replace_int :: KnownNat n => Vec n a -> Int -> a -> Vec n a
      Text
"Clash.Sized.Vector.replace_int" | Int
argLen Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
6 -> do
        let ([Term
_knArg,Term
vArg,Term
iArg,Term
aArg],[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
            Bool
shouldReduce1 <- [RewriteMonad NormalizeState Bool]
-> RewriteMonad NormalizeState Bool
forall (m :: Type -> Type). Monad m => [m Bool] -> m Bool
List.orM [ Bool -> RewriteMonad NormalizeState Bool
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 (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
eTy))
                                 ]
            if Bool
shouldReduce1
               then (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
<$> InScopeSet
-> Integer
-> Type
-> Type
-> Term
-> Term
-> Term
-> RewriteMonad NormalizeState Term
reduceReplace_int InScopeSet
is0 Integer
n Type
aTy Type
eTy Term
vArg Term
iArg Term
aArg
               else Term -> RewriteMonad NormalizeState Term
forall (m :: Type -> Type) a. Monad m => a -> m a
return Term
e
          Either String Integer
_ -> Term -> RewriteMonad NormalizeState Term
forall (m :: Type -> Type) a. Monad m => a -> m a
return Term
e

      Text
"Clash.Sized.Vector.index_int" | Int
argLen Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
5 -> do
        let ([Term
_knArg,Term
vArg,Term
iArg],[Type
nTy,Type
aTy]) = [Either Term Type] -> ([Term], [Type])
forall a b. [Either a b] -> ([a], [b])
Either.partitionEithers [Either Term Type]
args
            argTy :: Type
argTy = TyConMap -> Term -> Type
forall a. InferType a => TyConMap -> a -> Type
inferCoreTypeOf TyConMap
tcm Term
vArg
        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
            Bool
shouldReduce1 <- [RewriteMonad NormalizeState Bool]
-> RewriteMonad NormalizeState Bool
forall (m :: Type -> Type). Monad m => [m Bool] -> m Bool
List.orM [ Bool -> RewriteMonad NormalizeState Bool
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 (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 Bool
shouldReduce1
               then (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
<$> InScopeSet
-> Integer
-> Type
-> Term
-> Term
-> RewriteMonad NormalizeState Term
reduceIndex_int InScopeSet
is0 Integer
n Type
aTy Term
vArg Term
iArg
               else Term -> RewriteMonad NormalizeState Term
forall (m :: Type -> Type) a. Monad m => a -> m a
return Term
e
          Either String Integer
_ -> Term -> RewriteMonad NormalizeState Term
forall (m :: Type -> Type) a. Monad m => a -> m a
return Term
e

      Text
"Clash.Sized.Vector.imap" | Int
argLen Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
6 -> do
        let [Type
nTy,Type
argElTy,Type
resElTy] = [Either Term Type] -> [Type]
forall a b. [Either a b] -> [b]
Either.rights [Either Term Type]
args
            TyConApp TyConName
vecTcNm [Type]
_ = TypeView
tv
            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
            Bool
shouldReduce1 <- [RewriteMonad NormalizeState Bool]
-> RewriteMonad NormalizeState Bool
forall (m :: Type -> Type). Monad m => [m Bool] -> m Bool
List.orM [ Bool -> RewriteMonad NormalizeState Bool
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 (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
eTy]) ]
            if Bool
shouldReduce1
               then let [Term
_,Term
fun,Term
arg] = [Either Term Type] -> [Term]
forall a b. [Either a b] -> [a]
Either.lefts [Either Term Type]
args
                    in  (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
-> Integer
-> Type
-> Type
-> Term
-> Term
-> RewriteMonad NormalizeState Term
reduceImap TransformContext
c Integer
n Type
argElTy Type
resElTy Term
fun Term
arg
               else Term -> RewriteMonad NormalizeState Term
forall (m :: Type -> Type) a. Monad m => a -> m a
return Term
e
          Either String Integer
_ -> Term -> RewriteMonad NormalizeState Term
forall (m :: Type -> Type) a. Monad m => a -> m a
return Term
e
      Text
"Clash.Sized.Vector.iterateI" | Int
argLen Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
5 ->
        let ([Term
_kn,Term
f,Term
a],[Type
nTy,Type
aTy]) = [Either Term Type] -> ([Term], [Type])
forall a b. [Either a b] -> ([a], [b])
Either.partitionEithers [Either Term Type]
args in
        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
            Bool
shouldReduce1 <- [RewriteMonad NormalizeState Bool]
-> RewriteMonad NormalizeState Bool
forall (m :: Type -> Type). Monad m => [m Bool] -> m Bool
List.orM
              [ Bool -> RewriteMonad NormalizeState Bool
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 (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
eTy)) ]

            if Bool
shouldReduce1 then
              (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
-> Integer
-> Type
-> Type
-> Term
-> Term
-> RewriteMonad NormalizeState Term
reduceIterateI TransformContext
c Integer
n Type
aTy Type
eTy Term
f Term
a
            else
              Term -> RewriteMonad NormalizeState Term
forall (m :: Type -> Type) a. Monad m => a -> m a
return Term
e
          Either String Integer
_ -> Term -> RewriteMonad NormalizeState Term
forall (m :: Type -> Type) a. Monad m => a -> m a
return Term
e
      Text
"Clash.Sized.Vector.dtfold" | Int
argLen Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
8 ->
        let ([Term
_kn,Term
_motive,Term
lrFun,Term
brFun,Term
arg],[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
        in  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 -> (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
<$> InScopeSet
-> Integer
-> Type
-> Term
-> Term
-> Term
-> RewriteMonad NormalizeState Term
reduceDTFold InScopeSet
is0 Integer
n Type
aTy Term
lrFun Term
brFun Term
arg
          Either String Integer
_ -> Term -> RewriteMonad NormalizeState Term
forall (m :: Type -> Type) a. Monad m => a -> m a
return Term
e

      Text
"Clash.Sized.Vector.reverse"
        | Bool
ultra
        , ([Term
vArg],[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)
        -> (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
<$> InScopeSet
-> Integer -> Type -> Term -> RewriteMonad NormalizeState Term
reduceReverse InScopeSet
is0 Integer
n Type
aTy Term
vArg

      Text
"Clash.Sized.RTree.tdfold" | Int
argLen Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
8 ->
        let ([Term
_kn,Term
_motive,Term
lrFun,Term
brFun,Term
arg],[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
        in  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 -> (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
<$> InScopeSet
-> Integer
-> Type
-> Term
-> Term
-> Term
-> RewriteMonad NormalizeState Term
reduceTFold InScopeSet
is0 Integer
n Type
aTy Term
lrFun Term
brFun Term
arg
          Either String Integer
_ -> Term -> RewriteMonad NormalizeState Term
forall (m :: Type -> Type) a. Monad m => a -> m a
return Term
e
      Text
"Clash.Sized.RTree.treplicate" | Int
argLen Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
4 -> do
        let ([Term
_sArg,Term
vArg],[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
            Bool
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 Bool
shouldReduce1
               then (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
<$> Integer -> Type -> Type -> Term -> RewriteMonad NormalizeState Term
reduceTReplicate Integer
n Type
aTy Type
eTy Term
vArg
               else Term -> RewriteMonad NormalizeState Term
forall (m :: Type -> Type) a. Monad m => a -> m a
return Term
e
          Either String Integer
_ -> Term -> RewriteMonad NormalizeState Term
forall (m :: Type -> Type) a. Monad m => a -> m a
return Term
e
      Text
"Clash.Sized.Internal.BitVector.split#" | Int
argLen Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
4 -> do
        let ([Term
_knArg,Term
bvArg],[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 -> do
              let (Just TyCon
tupTc) = TyConName -> TyConMap -> Maybe TyCon
forall a b. Uniquable a => a -> UniqMap b -> Maybe b
lookupUniqMap TyConName
tupTcNm TyConMap
tcm
                  [DataCon
tupDc]      = TyCon -> [DataCon]
tyConDataCons TyCon
tupTc
                  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)
            | Integer
m Integer -> Integer -> Bool
forall a. Eq a => a -> a -> Bool
== Integer
0 -> do
              let (Just TyCon
tupTc) = TyConName -> TyConMap -> Maybe TyCon
forall a b. Uniquable a => a -> UniqMap b -> Maybe b
lookupUniqMap TyConName
tupTcNm TyConMap
tcm
                  [DataCon
tupDc]      = TyCon -> [DataCon]
tyConDataCons TyCon
tupTc
                  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)
          (Either String Integer, Either String Integer, TypeView)
_ -> Term -> RewriteMonad NormalizeState Term
forall (m :: Type -> Type) a. Monad m => a -> m a
return Term
e
      Text
"Clash.Sized.Internal.BitVector.eq#"
        | ([Term
_,Term
_],[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
        -> let (Just TyCon
boolTc) = TyConName -> TyConMap -> Maybe TyCon
forall a b. Uniquable a => a -> UniqMap b -> Maybe b
lookupUniqMap TyConName
boolTcNm TyConMap
tcm
               [DataCon
_falseDc,DataCon
trueDc] = TyCon -> [DataCon]
tyConDataCons TyCon
boolTc
           in  Term -> RewriteMonad NormalizeState Term
forall a extra. a -> RewriteMonad extra a
changed (Term -> [TickInfo] -> Term
mkTicks (DataCon -> Term
Data DataCon
trueDc) [TickInfo]
ticks)
      Text
_ -> Term -> RewriteMonad NormalizeState Term
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
      Bool
u <- Bool -> Type -> RewriteMonad extra Bool
forall extra. Bool -> Type -> RewriteMonad extra Bool
isUntranslatableType Bool
False Type
t
      if Bool
u
         then Bool -> RewriteMonad extra Bool
forall (m :: Type -> Type) a. Monad m => a -> m a
return ([TyVar] -> Bool
forall (t :: Type -> Type) a. Foldable t => t a -> Bool
null ([TyVar] -> Bool) -> [TyVar] -> Bool
forall a b. (a -> b) -> a -> b
$ 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
t)
         else Bool -> RewriteMonad extra Bool
forall (m :: Type -> Type) a. Monad m => a -> m a
return Bool
False

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