{-|
  Copyright  :  (C) 2012-2016, University of Twente,
                (C) 2021-2026, QBayLogic B.V.
  License    :  BSD2 (see the file LICENSE)
  Maintainer :  QBayLogic B.V. <devops@qbaylogic.com>

  The normalization strategies, as pure "Clash.Rewrite.StrategyDSL" values.
  "Clash.Normalize.Strategy" compiles 'normalizationSpec' and
  'constantPropagationSpec' into the executable 'Clash.Normalize.Strategy.normalization'
  and 'Clash.Normalize.Strategy.constantPropagation'; "Clash.Normalize"
  compiles 'flattenSpec' into the flattening strategy of @flattenCallTree@.
-}

{-# LANGUAGE DisambiguateRecordFields #-}
{-# LANGUAGE DuplicateRecordFields #-}
{-# LANGUAGE NamedFieldPuns #-}
{-# LANGUAGE NoFieldSelectors #-}
{-# LANGUAGE OverloadedRecordDot #-}
{-# LANGUAGE TemplateHaskellQuotes #-}

module Clash.Normalize.Strategy.Spec
  ( normalizationSpec
  , constantPropagationSpec
  , flattenSpec
  ) where

import Language.Haskell.TH.Syntax (Name)

import Clash.Normalize.Transformations
import Clash.Rewrite.StrategyDSL

-- [Note: bottomup traversal reduceConst]
--
-- 2-May-2019: There is a bug in the evaluator where all data constructors are
-- considered lazy, even though their declaration says they have strict fields.
-- This causes some reductions to fail because the term under the constructor is
-- not in WHNF, which is what some of the evaluation rules for certain primitive
-- operations expect. Using a bottom-up traversal works around this bug by
-- ensuring that the values under the constructor are in WHNF.
--
-- Using a bottomup traversal ensures that constants are reduced to NF, even if
-- constructors are lazy, thus ensuring more sensible/smaller generated HDL.

-- | Normalisation transformation. The argument is the name of the compiled
-- 'Clash.Normalize.Strategy.constantPropagation' binding.
normalizationSpec :: Name -> Strat
normalizationSpec :: Name -> Strat
normalizationSpec Name
constantPropagationName =
  Strat
rmDeadcode Strat -> Strat -> Strat
forall a. Strategic a => a -> a -> a
>-> Strat
multPrim Strat -> Strat -> Strat
forall a. Strategic a => a -> a -> a
>-> Name -> Strat
callStrategy Name
constantPropagationName Strat -> Strat -> Strat
forall a. Strategic a => a -> a -> a
>->
  Strat
rmUnusedExpr Strat -> Strat -> Strat
>-!-> Strat
anf Strat -> Strat -> Strat
>-!-> Strat
rmDeadcode Strat -> Strat -> Strat
forall a. Strategic a => a -> a -> a
>->
  Strat
bindConst Strat -> Strat -> Strat
forall a. Strategic a => a -> a -> a
>-> Strat
letTL
  Strat -> Strat -> Strat
forall a. Strategic a => a -> a -> a
>-> Strat
evalConst
  Strat -> Strat -> Strat
>-!-> Strat
cse Strat -> Strat -> Strat
>-!-> Strat
cleanup Strat -> Strat -> Strat
forall a. Strategic a => a -> a -> a
>->
  Strat
elimCaseBigNum Strat -> Strat -> Strat
forall a. Strategic a => a -> a -> a
>->  -- see [Note] late elimCaseBigNum
  Strat
xOptim Strat -> Strat -> Strat
forall a. Strategic a => a -> a -> a
>-> Strat
rmDeadcode Strat -> Strat -> Strat
forall a. Strategic a => a -> a -> a
>->
  Strat
cleanup Strat -> Strat -> Strat
forall a. Strategic a => a -> a -> a
>-> Strat
bindSimIO Strat -> Strat -> Strat
forall a. Strategic a => a -> a -> a
>-> Strat
recLetRec Strat -> Strat -> Strat
forall a. Strategic a => a -> a -> a
>-> Strat
splitArgs
  where
    multPrim :: Strat
multPrim   = Transformation -> Strat
forall s. ToStep s => s -> Strat
topdown Transformation
setupMultiResultPrim
    anf :: Strat
anf        = Transformation -> Strat
forall s. ToStep s => s -> Strat
topdown Transformation
nonRepANF Strat -> Strat -> Strat
forall a. Strategic a => a -> a -> a
>-> String -> Name -> Strat
pass String
"ANF" 'makeANF Strat -> Strat -> Strat
forall a. Strategic a => a -> a -> a
>-> Transformation -> Strat
forall s. ToStep s => s -> Strat
topdown Transformation
caseCon
    letTL :: Strat
letTL      = Transformation -> Strat
forall s. ToStep s => s -> Strat
topdownSuc Transformation
topLet
    recLetRec :: Strat
recLetRec  = String -> Name -> Strat
pass String
"recToLetRec" 'recToLetRec
    rmUnusedExpr :: Strat
rmUnusedExpr = Transformation -> Strat
forall s. ToStep s => s -> Strat
bottomup Transformation
removeUnusedExpr
    rmDeadcode :: Strat
rmDeadcode = Transformation -> Strat
forall s. ToStep s => s -> Strat
bottomup (String -> Transformation -> Transformation
named String
"deadcode" Transformation
deadCode)
    bindConst :: Strat
bindConst  = Transformation -> Strat
forall s. ToStep s => s -> Strat
topdown Transformation
bindConstantVar
    -- See [Note] bottomup traversal reduceConst:
    evalConst :: Strat
evalConst  = Transformation -> Strat
forall s. ToStep s => s -> Strat
bottomup Transformation
reduceConst
    cse :: Strat
cse        = Transformation -> Strat
forall s. ToStep s => s -> Strat
topdown Transformation
simpleCSE
    elimCaseBigNum :: Strat
elimCaseBigNum = Transformation -> Strat
forall s. ToStep s => s -> Strat
topdown Transformation
elimCaseBigNumInternals
    xOptim :: Strat
xOptim     = Transformation -> Strat
forall s. ToStep s => s -> Strat
bottomup Transformation
xOptimize
    cleanup :: Strat
cleanup    = Transformation -> Strat
forall s. ToStep s => s -> Strat
topdown Transformation
etaExpandSyn Strat -> Strat -> Strat
forall a. Strategic a => a -> a -> a
>->
                 Transformation -> Strat
forall s. ToStep s => s -> Strat
topdownSuc Transformation
inlineCleanup Strat -> Strat -> Strat
forall a. Strategic a => a -> a -> a
!->
                 Step -> Strat
forall s. ToStep s => s -> Strat
innerMost ([Transformation] -> Step
chain [ Transformation
caseCon
                                  , Transformation
bindConstantVar
                                  , String -> Transformation -> Transformation
named String
"letFlat" Transformation
flattenLet
                                  ])
                 Strat -> Strat -> Strat
forall a. Strategic a => a -> a -> a
>-> Strat
rmDeadcode Strat -> Strat -> Strat
forall a. Strategic a => a -> a -> a
>-> Strat
letTL
    splitArgs :: Strat
splitArgs  = Transformation -> Strat
forall s. ToStep s => s -> Strat
topdown Transformation
separateArguments Strat -> Strat -> Strat
forall a. Strategic a => a -> a -> a
!->
                 Transformation -> Strat
forall s. ToStep s => s -> Strat
bottomup Transformation
caseCon
    bindSimIO :: Strat
bindSimIO  = Transformation -> Strat
forall s. ToStep s => s -> Strat
topdown Transformation
inlineSimIO


constantPropagationSpec :: Strat
constantPropagationSpec :: Strat
constantPropagationSpec =
  Strat
inlineAndPropagate Strat -> Strat -> Strat
forall a. Strategic a => a -> a -> a
>->
  Strat
caseFlattening Strat -> Strat -> Strat
forall a. Strategic a => a -> a -> a
>->
  Strat
etaTL Strat -> Strat -> Strat
forall a. Strategic a => a -> a -> a
>->
  Strat
dec Strat -> Strat -> Strat
forall a. Strategic a => a -> a -> a
>->
  Strat
spec Strat -> Strat -> Strat
forall a. Strategic a => a -> a -> a
>->
  Strat
dec Strat -> Strat -> Strat
forall a. Strategic a => a -> a -> a
>->
  Strat
conSpec
  where
    etaTL :: Strat
etaTL              = String -> Name -> Strat
pass String
"etaTL" 'etaExpansionTL Strat -> Strat -> Strat
forall a. Strategic a => a -> a -> a
!-> Transformation -> Strat
forall s. ToStep s => s -> Strat
topdown Transformation
appProp
    -- The outer repeatR is still needed: inlineNR is a full traversal whose
    -- results can only be processed by re-running the top-down chain from the
    -- new root.
    --
    -- NB: 'topdownFix' is deliberately _not_ used here, see
    -- Note [topdownFixR is not for inlining bundles].
    inlineAndPropagate :: Strat
inlineAndPropagate = Strat -> Strat
repeatR (Step -> Strat
forall s. ToStep s => s -> Strat
topdown Step
transPropagateAndInline Strat -> Strat -> Strat
forall a. Strategic a => a -> a -> a
>-> Strat
inlineNR)
    spec :: Strat
spec               = Step -> Strat
forall s. ToStep s => s -> Strat
bottomup Step
specTransformations
    caseFlattening :: Strat
caseFlattening     = Transformation -> Strat
forall s. ToStep s => s -> Strat
topdownFix Transformation
caseFlat
    dec :: Strat
dec                = Transformation -> Strat
forall s. ToStep s => s -> Strat
topdownFix Transformation
disjointExpressionConsolidation
    conSpec :: Strat
conSpec            = Step -> Strat
forall s. ToStep s => s -> Strat
bottomup ((Transformation -> Step
one (String -> Transformation -> Transformation
named String
"appPropCS" Transformation
appProp) Step -> Step -> Step
forall a. Strategic a => a -> a -> a
!->
                                    Strat -> Step
nested (Transformation -> Strat
forall s. ToStep s => s -> Strat
bottomup Transformation
constantSpec)) Step -> Step -> Step
forall a. Strategic a => a -> a -> a
>-!
                                   Transformation -> Step
one Transformation
constantSpec)

    transPropagateAndInline :: Step
    transPropagateAndInline :: Step
transPropagateAndInline = [Transformation] -> Step
chain
      [ Transformation
appProp
      , Transformation
bindConstantVar
      , Transformation
caseLet
      , Transformation
caseCase
      , Transformation
caseCon
      , Transformation
caseDataToTag
      , Transformation
elimExistentials
      , Transformation
caseEliminateNonReachable
      , Transformation
removeUnusedExpr
      -- These transformations can safely be applied in a top-down traversal as
      -- they themselves check whether the to-be-inlined binder is recursive or not.
      , Transformation
inlineWorkFree
      , Transformation
inlineSmall
      , Transformation
inlineOrLiftNonRep -- See: [Note] bindNonRep before liftNonRep
                           -- See: [Note] bottom-up traversal for liftNonRep
      , Transformation
reducePrim

      , Transformation
caseCast
      , Transformation
letCast
      , Transformation
splitCastWork
      , Transformation
argCastSpec
      , Transformation
inlineCast
      , Transformation
elimCastCast
      ]

    -- InlineNonRep cannot be applied in a top-down traversal, as the non-representable
    -- binder might be recursive. The idea is, is that if the recursive
    -- non-representable binder is inlined once, we can get rid of the recursive
    -- aspect using the case-of-known-constructor
    --
    -- Note that we first do a dead code removal pass, which makes sure that
    -- unused let-bindings get cleaned up. Only if no dead code is removed
    -- 'inlineNonRep' is executed. We do this for two reasons:
    --
    --   1. 'deadCode' is an expensive operation and is therefore left out of
    --      the hot loop 'transPropagateAndInline'.
    --
    --   2. In various situations 'transPropagateAndInline' can do more work
    --      after 'deadCode' was successful. This work in turn might remove a
    --      a construct 'inlineNonRep' would fire on - saving the compiler work.
    --
    inlineNR :: Strat
    inlineNR :: Strat
inlineNR =
          Transformation -> Strat
forall s. ToStep s => s -> Strat
bottomup Transformation
deadCode
      Strat -> Strat -> Strat
forall a. Strategic a => a -> a -> a
>-! String -> Name -> Strat
pass String
"inlineNonRep" 'inlineNonRep

    specTransformations :: Step
    specTransformations :: Step
specTransformations = [Transformation] -> Step
chain
      [ Transformation
typeSpec
      , Transformation
nonRepSpec
      , Transformation
zeroWidthSpec
        -- See Note [zeroWidthSpec enabling transformations]
      ]

{-
Note [flatten pass structure]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
Through experimentation we've learned the following:

1. The evaluator-backed rewrites ('reduceConst', 'reducePrim') must not
   sit inside the top-down propagation chain. 'topdownFix' settles that chain
   at each node until a fixpoint, so a chained 'reduceConst' is re-attempted -
   evaluator call and all - for every 'appProp' or 'caseCon' that fires there.
   On large designs we've measured that dominates; hoisting them out was worth
   ~30%. See #3338.

2. There should be exactly two traversals per round, and the bottom-up one has
   to come first.

   A traversal rebuilds every node it walks, so each extra traversal costs a
   full term rebuild per round even when nothing fires. Running 'flattenLet'
   and the evaluator-backed rewrites as one fused bottom-up pass instead of two
   consecutive ones is therefore free of charge (it does not change which
   rewrites fire, or in which order they fire relative to each other).

   Running that bottom-up pass _before_ the top-down one lets the constants it
   folds be consumed by 'caseCon' in the same round. With the passes the other
   way round the folded constants sit unused until the next round, so
   constant-heavy designs pay for an extra iteration of the whole loop:
   @tests/shouldwork/Basic/AES.hs@ did ~36k extra node visits per transformation
   that way.

If you touch code related to this, please make sure to run benchmarks.
-}

-- | The flattening strategy of 'Clash.Normalize.flattenCallTree'.
flattenSpec :: Strat
flattenSpec :: Strat
flattenSpec =
  -- See Note [flatten pass structure].
  Strat -> Strat
repeatR (Step -> Strat
forall s. ToStep s => s -> Strat
bottomup (Transformation -> Step
one Transformation
flattenLet Step -> Step -> Step
forall a. Strategic a => a -> a -> a
>->
                     (Transformation -> Step
one Transformation
reduceConst Step -> Step -> Step
forall a. Strategic a => a -> a -> a
!-> Transformation -> Step
one Transformation
deadCode) Step -> Step -> Step
forall a. Strategic a => a -> a -> a
>->
                     [Transformation] -> Step
chain [ Transformation
reducePrim
                           , Transformation
removeUnusedExpr
                           ]) Strat -> Strat -> Strat
forall a. Strategic a => a -> a -> a
>->
           Step -> Strat
forall s. ToStep s => s -> Strat
topdownFix ([Transformation] -> Step
chain [ String -> Transformation -> Transformation
named String
"appProp" Transformation
appProp
                             , Transformation
bindConstantVar
                             , Transformation
caseCon
                             ])) Strat -> Strat -> Strat
forall a. Strategic a => a -> a -> a
!->
  Transformation -> Strat
forall s. ToStep s => s -> Strat
bottomup Transformation
deadCode Strat -> Strat -> Strat
forall a. Strategic a => a -> a -> a
>-> -- See #3407
  Strat
letTL Strat -> Strat -> Strat
forall a. Strategic a => a -> a -> a
>->
  -- See [Note] relation `collapseRHSNoops` and `inlineCleanup`
  -- Note that we do this as the very last step, after all constant propagation
  -- has been done to avoid #3036.
  Transformation -> Strat
forall s. ToStep s => s -> Strat
topdownSuc Transformation
collapseRHSNoops Strat -> Strat -> Strat
forall a. Strategic a => a -> a -> a
>->
  Transformation -> Strat
forall s. ToStep s => s -> Strat
topdownSuc Transformation
inlineCleanup Strat -> Strat -> Strat
forall a. Strategic a => a -> a -> a
>->
  Transformation -> Strat
forall s. ToStep s => s -> Strat
bottomup Transformation
caseCon Strat -> Strat -> Strat
forall a. Strategic a => a -> a -> a
>-> -- https://github.com/clash-lang/clash-compiler/issues/3159 / #3204
  Transformation -> Strat
forall s. ToStep s => s -> Strat
bottomup Transformation
flattenLet Strat -> Strat -> Strat
forall a. Strategic a => a -> a -> a
>-> -- https://github.com/clash-lang/clash-compiler/issues/3185
  Transformation -> Strat
forall s. ToStep s => s -> Strat
bottomup Transformation
bindConstantVar Strat -> Strat -> Strat
forall a. Strategic a => a -> a -> a
>-> -- https://github.com/clash-lang/clash-compiler/issues/3041
  Strat
letTL
  where
    letTL :: Strat
letTL = Transformation -> Strat
forall s. ToStep s => s -> Strat
topdownSuc Transformation
topLet

{-
[Note] late elimCaseBigNum

elimCaseBigNum is placed fairly late in the pipeline, after any constant folding and after caseCon.
Because Naturals also hide inside SNat/Nat/KnownNats, and those can be bigger then 64bits.
But they're ultimately monomorphic and thus static and will be evaluated.
We just have to make sure that evaluation happens before we do elimCaseBigNum.

For an example of where this can happen see foldableSNat in tests/shouldwork/Issues/T3157_IntegerNaturalInternals.hs
-}

{-
Note [zeroWidthSpec enabling transformations]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
When zeroWidthSpec fires, it can lead to better results in normalization, but
this is somewhat incidental. The extra transformations which fire are typically
from

  * calls to transformations like caseCon which occur after constantPropagation
    (e.g. caseCon run after ANF conversion).

  * flattening / inlining which happens late in normalization (after regular
    normalization has occurred)

  * normalizing another function due to being marked NOINLINE

If we consider the following:

    data AB = A | B

    ab :: KnownNat n => Index n -> AB -> AB
    ab n A = if n >  0 then A else B
    ab n B = if n == 0 then B else A
    {-# NOINLINE ab #-}

    topEntity = ab @1
    {-# NOINLINE topEntity #-}

The zeroWidthSpec transformation fires on the topEntity, giving a
post-normalization topEntity of

    \(x :: Index 1) ->
      \(y :: AB) ->
        letrec result :: AB = ab' y in result

where

    ab' = ab (fromInteger# 0)

The extra transformations which fire happen later when ab' is normalized.
Removing the NOINLINE from ab gives the same result, but the extra
transformations fire in flattening instead.
-}

{- [Note] bottom-up traversal for liftNonRep
We used to say:

"The liftNonRep transformation must be applied in a topDown traversal because
of what Clash considers tail calls in its join-point analysis."

Consider:

> let fail = \x -> ...
> in  case ... of
>       A -> let fail1 = \y -> case ... of
>                                 X -> fail ...
>                                 Y -> ...
>            in case ... of
>                 P -> fail1 ...
>                 Q -> ...
>       B -> fail ...

under "normal" tail call rules, the local 'fail' functions is not a join-point
because it is used in a let-binding. However, we apply "special" tail call rules
in Clash. Because 'fail' is used in a TC position within 'fail1', and 'fail1' is
only used in a TC position, in Clash, we consider 'tail' also only to be used
in a TC position.

Now image we apply 'liftNonRep' in a bottom up traversal, we will end up with:

> fail1 = \fail y -> case ... of
>   X -> fail ...
>   Y -> ...

> let fail = \x -> ...
> in  case ... of
>       A -> case ... of
>                 P -> fail1 fail ...
>                 Q -> ...
>       B -> fail ...

Suddenly, 'fail' ends up in an argument position, because it occurred as a
_locally_ bound variable within 'fail1'. And because of that 'fail' stops being
a join-point.

However, when we apply 'liftNonRep' in a top down traversal we end up with:

> fail = \x -> ...
>
> fail1 = \y -> case ... of
>   X -> fail ...
>   Y -> ...
>
> let ...
> in  case ... of
>       A -> let
>            in case ... of
>                 P -> fail1 ...
>                 Q -> ...
>       B -> fail ...

and all is well with the world.

UPDATE:
We can now just perform liftNonRep in a bottom-up traversal again, because
liftNonRep no longer checks that if the binding that is lifted is a join-point.
However, for this to work, bindNonRep must always have been exhaustively applied
before liftNonRep. See also: [Note] bindNonRep before liftNonRep.
-}

{- [Note] bindNonRep before liftNonRep
The combination of liftNonRep and nonRepSpec can lead to non-termination in an
unchecked rewrite system (without termination measures in place) on the
following:

> main = f not
> f    = \a x -> (a x) && (f a x)

nonRepSpec will lead to:

> main = f'
> f    = \a x -> (a x) && (f a x)
> f'   = (\a x -> (a x) && (f a x)) not

then lamApp leads to:

> main = f'
> f    = \a x -> (a x) && (f a x)
> f'   = let a = not in (\x -> (a x) && (f a x))

then liftNonRep leads to:

> main = f'
> f    = \a x -> (a x) && (f a x)
> f'   = \x -> (g x) && (f g x)
> g    = not

and nonRepSepc leads to:

> main = f'
> f    = \a x -> (a x) && (f a x)
> f'   = \x -> (g x) && (f'' g x)
> g    = not
> f''  = (\a x -> (a x) && (f a x)) g

This cycle continues indefinitely, as liftNonRep creates a new global variable,
which is never alpha-equivalent to the previous global variable introduced by
liftNonRep.

That is why bindNonRep must always be applied before liftNonRep. When we end up
in the situation after lamApp:

> main = f'
> f    = \a x -> (a x) && (f a x)
> f'   = let a = not in (\x -> (a x) && (f a x))

bindNonRep will now lead to:

> main = f'
> f    = \a x -> (a x) && (f a x)
> f'   = \x -> (not x) && (f not x)

Because `f` has already been specialized on the alpha-equivalent-to-itself `not`
function, liftNonRep leads to:

> main = f'
> f    = \a x -> (a x) && (f a x)
> f'   = \x -> (not x) && (f' x)

And there is no non-terminating rewriting cycle.

That is why bindNonRep must always be exhaustively applied before we apply
liftNonRep.
-}