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

  The 'disjointExpressionConsolidation' transformation lifts applications of
  global binders out of alternatives of case-statements.

  e.g. It converts:

  > case x of
  >   A -> f 3 y
  >   B -> f x x
  >   C -> h x

  into:

  > let f_arg0 = case x of {A -> 3; B -> x}
  >     f_arg1 = case x of {A -> y; B -> x}
  >     f_out  = f f_arg0 f_arg1
  > in  case x of
  >       A -> f_out
  >       B -> f_out
  >       C -> h x
-}

{-# LANGUAGE CPP #-}
{-# LANGUAGE OverloadedStrings #-}
{-# LANGUAGE RecursiveDo #-}
{-# LANGUAGE ViewPatterns #-}
{-# LANGUAGE TemplateHaskell #-}
{-# LANGUAGE MagicHash #-}

module Clash.Normalize.Transformations.DEC
  ( disjointExpressionConsolidation
  ) where

#if !MIN_VERSION_base(4,18,0)
import Control.Applicative (liftA2)
#endif
import Control.Lens ((^.), _1)
import qualified Control.Lens as Lens
import qualified Control.Monad as Monad
import Data.Bifunctor (first, second)
import Data.Bits ((.&.), complement)
import Data.Coerce (coerce)
import qualified Data.Either as Either
import qualified Data.Foldable as Foldable
import qualified Data.Graph as Graph
import Data.IntMap.Strict (IntMap)
import qualified Data.IntMap.Strict as IntMap
import qualified Data.List as List
import qualified Data.List.Extra as List
import qualified Data.Map.Strict as Map
import qualified Data.Maybe as Maybe
import Data.Monoid (All(..))
import qualified Data.Text as Text
import Data.Text.Extra (showt)
import GHC.Stack (HasCallStack)
import qualified Language.Haskell.TH as TH

#if MIN_VERSION_ghc(9,6,0)
import GHC.Core.Make (chunkify, mkChunkified)
#elif MIN_VERSION_ghc(8,10,0)
import GHC.Hs.Utils (chunkify, mkChunkified)
#else
import HsUtils (chunkify, mkChunkified)
#endif

#if MIN_VERSION_ghc(9,0,0)
import GHC.Settings.Constants (mAX_TUPLE_SIZE)
#else
import Constants (mAX_TUPLE_SIZE)
#endif

-- internal
import Clash.Core.DataCon (DataCon)
import Clash.Core.Evaluator.Types  (whnf')
import Clash.Core.FreeVars
  (termFreeVars', typeFreeVars', localVarsDoNotOccurIn)
import Clash.Core.HasType
import Clash.Core.Literal (Literal(..))
import Clash.Core.Name (OccName, nameOcc)
import Clash.Core.Pretty (showPpr)
import Clash.Core.Term
  ( Alt, LetBinding, Pat(..), PrimInfo(..), Term(..), TickInfo(..)
  , collectArgs, collectArgsTicks, mkApps, mkTicks, patIds, stripTicks)
import Clash.Core.TyCon (TyConMap, TyConName, tyConDataCons)
import Clash.Core.Type
  (Type, TypeView (..), isPolyFunTy, mkTyConApp, splitFunForallTy, tyView)
import Clash.Core.Util (mkInternalVar, mkSelectorCase, sccLetBindings)
import Clash.Core.Var (Id, isGlobalId, isLocalId, varName)
import Clash.Core.VarEnv
  ( InScopeSet, elemInScopeSet, extendInScopeSet, extendInScopeSetList
  , notElemInScopeSet, unionInScope)
import qualified Clash.Data.UniqMap as UniqMap
import Clash.Normalize.Transformations.Letrec (deadCode)
import Clash.Normalize.Types (NormRewrite, NormalizeSession)
import Clash.Rewrite.Combinators (bottomupR)
import Clash.Rewrite.Types
import Clash.Rewrite.Util (changed, isFromInt, isUntranslatableType)
import Clash.Rewrite.WorkFree (isConstant)
import Clash.Util (MonadUnique, curLoc)
import Clash.Util.Supply (splitSupply)

-- primitives
import qualified Clash.Sized.Internal.BitVector
import qualified Clash.Sized.Internal.Index
import qualified Clash.Sized.Internal.Signed
import qualified Clash.Sized.Internal.Unsigned
import qualified GHC.Base
import qualified GHC.Classes
#if MIN_VERSION_base(4,15,0)
import qualified GHC.Num.Integer
#else
-- interger-gmp primitives are defined in the hidden module GHC.Integer.Type,
-- but exported from GHC.Integer
import qualified GHC.Integer as GHC.Integer.Type
#endif
import qualified GHC.Prim

-- | This transformation lifts applications of global binders out of
-- alternatives of case-statements.
--
-- e.g. It converts:
--
-- @
-- case x of
--   A -> f 3 y
--   B -> f x x
--   C -> h x
-- @
--
-- into:
--
-- @
-- let f_arg0 = case x of {A -> 3; B -> x}
--     f_arg1 = case x of {A -> y; B -> x}
--     f_out  = f f_arg0 f_arg1
-- in  case x of
--       A -> f_out
--       B -> f_out
--       C -> h x
-- @
--
-- Though that's a lie. It actually converts it into:
--
-- @
-- let f_tupIn = case x of {A -> (3,y); B -> (x,x)}
--     f_arg0  = case f_tupIn of (l,_) -> l
--     f_arg1  = case f_tupIn of (_,r) -> r
--     f_out   = f f_arg0 f_arg1
-- in  case x of
--       A -> f_out
--       B -> f_out
--       C -> h x
-- @
--
-- In order to share the expression that's in the subject of the case expression,
-- and to share the /decoder/ circuit that logic synthesis will create to map the
-- bits of the subject expression to the bits needed to make the selection in the
-- multiplexer.
disjointExpressionConsolidation :: HasCallStack => NormRewrite
disjointExpressionConsolidation :: HasCallStack => NormRewrite
disjointExpressionConsolidation ctx :: TransformContext
ctx@(TransformContext InScopeSet
isCtx Context
_) e :: Term
e@(Case Term
_scrut Type
_ty _alts :: [Alt]
_alts@(Alt
_:Alt
_:[Alt]
_)) = do
    -- Collect all (the applications of) global binders (and certain primitives)
    -- that would be interesting to share out of the case-alternatives.
    (_,isCollected,collected) <- InScopeSet
-> [(Term, Term)]
-> [Term]
-> Term
-> NormalizeSession
     (Term, InScopeSet, [(Term, ([Term], CaseTree [Either Term Type]))])
collectGlobals InScopeSet
isCtx [] [] Term
e
    -- Filter those that are used at most once in every (nested) branch.
    let disJoint = ((Term, ([Term], CaseTree [Either Term Type])) -> Bool)
-> [(Term, ([Term], CaseTree [Either Term Type]))]
-> [(Term, ([Term], CaseTree [Either Term Type]))]
forall a. (a -> Bool) -> [a] -> [a]
filter (CaseTree [Either Term Type] -> Bool
isDisjoint (CaseTree [Either Term Type] -> Bool)
-> ((Term, ([Term], CaseTree [Either Term Type]))
    -> CaseTree [Either Term Type])
-> (Term, ([Term], CaseTree [Either Term Type]))
-> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ([Term], CaseTree [Either Term Type])
-> CaseTree [Either Term Type]
forall a b. (a, b) -> b
snd (([Term], CaseTree [Either Term Type])
 -> CaseTree [Either Term Type])
-> ((Term, ([Term], CaseTree [Either Term Type]))
    -> ([Term], CaseTree [Either Term Type]))
-> (Term, ([Term], CaseTree [Either Term Type]))
-> CaseTree [Either Term Type]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Term, ([Term], CaseTree [Either Term Type]))
-> ([Term], CaseTree [Either Term Type])
forall a b. (a, b) -> b
snd) [(Term, ([Term], CaseTree [Either Term Type]))]
collected
    if null disJoint
       then return e
       else do
         -- For every to-lift expression create (the generalization of):
         --
         -- let f_tupIn = case x of {A -> (3,y); B -> (x,x)}
         --     f_arg0  = case f_tupIn of (l,_) -> l
         --     f_arg1  = case f_tupIn of (_,r) -> r
         -- in  f f_arg0 f_arg0
         --
         -- if an argument is non-representable, the case-expression is inlined,
         -- and no let-binding will be created for it.
         --
         -- NB: mkDisJointGroup needs the context InScopeSet, isCtx, to determine
         -- whether expressions reference variables from the context, or
         -- variables inside a let-expression inside one of the alternatives.
         lifted <- mapM (mkDisjointGroup isCtx) disJoint
         tcm    <- Lens.view tcCache
         -- Create let-binders for all of the lifted expressions
         --
         -- NB: Because we will be substituting under binders we use the collected
         -- inScopeSet, isCollected, which also contains all the binders
         -- created inside all of the alternatives. With this inScopeSet, we
         -- ensure that the let-bindings we create here won't be accidentally
         -- captured by binders inside the case-alternatives.
         (_,funOutIds) <- List.mapAccumLM (mkFunOut tcm)
                                          isCollected
                                          (zip disJoint lifted)
         -- Create "substitutions" of the form [f X Y := f_out]
         let substitution = [Term] -> [Term] -> [(Term, Term)]
forall a b. [a] -> [b] -> [(a, b)]
zip (((Term, ([Term], CaseTree [Either Term Type])) -> Term)
-> [(Term, ([Term], CaseTree [Either Term Type]))] -> [Term]
forall a b. (a -> b) -> [a] -> [b]
map (Term, ([Term], CaseTree [Either Term Type])) -> Term
forall a b. (a, b) -> a
fst [(Term, ([Term], CaseTree [Either Term Type]))]
disJoint) ((Id -> Term) -> [Id] -> [Term]
forall a b. (a -> b) -> [a] -> [b]
map Id -> Term
Var [Id]
funOutIds)
         -- For all of the lifted expression: substitute occurrences of the
         -- disjoint expressions (f X Y) by a variable reference to the lifted
         -- expression (f_out)
         let isCtx1 = InScopeSet -> [Id] -> InScopeSet
forall a. InScopeSet -> [Var a] -> InScopeSet
extendInScopeSetList InScopeSet
isCtx [Id]
funOutIds
         lifted1 <- substLifted isCtx1 substitution lifted
         -- Do the same for the actual case expression
         (e1,_,_) <- collectGlobals isCtx1 substitution [] e
         -- Let-bind all the lifted function
         let lb = [LetBinding] -> Term -> Term
Letrec ([Id] -> [Term] -> [LetBinding]
forall a b. [a] -> [b] -> [(a, b)]
zip [Id]
funOutIds [Term]
lifted1) Term
e1
         -- Do an initial dead-code elimination pass, as `mkDisJoint` doesn't
         -- clean-up unused let-binders.
         lb1 <- bottomupR deadCode ctx lb
         changed lb1
  where
    -- Make the let-binder for the lifted expressions
    mkFunOut :: TyConMap -> InScopeSet -> ((Term, b), (a, b)) -> m (InScopeSet, Id)
mkFunOut TyConMap
tcm InScopeSet
isN ((Term
fun,b
_),(a
eLifted,b
_)) = do
      let ty :: Type
ty  = TyConMap -> a -> Type
forall a. InferType a => TyConMap -> a -> Type
inferCoreTypeOf TyConMap
tcm a
eLifted
          nm :: Text
nm  = Term -> Text
decFunName Term
fun
          nm1 :: Text
nm1 = Text
nm Text -> Text -> Text
`Text.append` Text
"_out"
      nm2 <- InScopeSet -> Text -> Type -> m Id
forall (m :: Type -> Type).
MonadUnique m =>
InScopeSet -> Text -> Type -> m Id
mkInternalVar InScopeSet
isN Text
nm1 Type
ty
      return (extendInScopeSet isN nm2,nm2)

    -- Substitute inside the lifted expressions
    --
    -- In case you are wondering why this function isn't simply
    --
    -- > mapM (\s (eL,seen) -> collectGlobal isN s seen eL) substitution lifted
    --
    -- then that's because we have e.g. the list of "substitutions":
    --
    -- [foo _ _ := foo_out; bar _ _ := bar_out]
    --
    -- and if we were to apply that to a lifted expression, which is going
    -- to be of the form `foo (case ...) (case ...)` then we would end up
    -- with let-bindings that are simply:
    --
    -- > let foo_out = foo_out ; bar_out = bar_out
    --
    -- instead of the desired
    --
    -- > let foo_out = foo ((case ...)[foo _ _ := foo_out; bar _ _ := bar_out])
    -- >                   ((case ...)[foo _ _ := foo_out; bar _ _ := bar_out])
    -- >     bar_out = bar ((case ...)[foo _ _ := foo_out; bar _ _ := bar_out])
    -- >                   ((case ...)[foo _ _ := foo_out; bar _ _ := bar_out])
    --
    -- So what we do is that for every lifted-expression we make sure that the
    -- 'substitution' never contains the self-substitution, so we end up with:
    --
    -- > let foo_out = (foo (case ...) (case ...))[bar _ _ := bar_out]
    --       bar_out = (bar (case ...) (case ...))[foo _ _ := foo_out]
    --
    -- We used to have a different approach, see commit
    -- 73d237017c4a5fff0c49bb72c9c4d5f6c68faf69
    --
    -- But that lead to the generation of combinational loops. Now that we no
    -- longer traverse into recursive groups of let-bindings, the issue #1316
    -- that the above commit tried to solve, no longer shows up.
    substLifted :: InScopeSet
-> [(Term, Term)]
-> [(Term, [Term])]
-> RewriteMonad NormalizeState [Term]
substLifted InScopeSet
isN [(Term, Term)]
substitution [(Term, [Term])]
lifted = do
      -- remove the self-substitutions for the respective lifted expressions
      let subsMatrix :: [[(Term, Term)]]
subsMatrix = [(Term, Term)] -> [[(Term, Term)]]
forall {a}. [a] -> [[a]]
l2m [(Term, Term)]
substitution
      lifted1 <- ([(Term, Term)]
 -> (Term, [Term])
 -> NormalizeSession
      (Term, InScopeSet,
       [(Term, ([Term], CaseTree [Either Term Type]))]))
-> [[(Term, Term)]]
-> [(Term, [Term])]
-> RewriteMonad
     NormalizeState
     [(Term, InScopeSet,
       [(Term, ([Term], CaseTree [Either Term Type]))])]
forall (m :: Type -> Type) a b c.
Applicative m =>
(a -> b -> m c) -> [a] -> [b] -> m [c]
Monad.zipWithM (\[(Term, Term)]
s (Term
eL,[Term]
seen) -> InScopeSet
-> [(Term, Term)]
-> [Term]
-> Term
-> NormalizeSession
     (Term, InScopeSet, [(Term, ([Term], CaseTree [Either Term Type]))])
collectGlobals InScopeSet
isN [(Term, Term)]
s [Term]
seen Term
eL)
                                 [[(Term, Term)]]
subsMatrix
                                 [(Term, [Term])]
lifted
      return (map (^. _1) lifted1)

    l2m :: [a] -> [[a]]
l2m = [a] -> [a] -> [[a]]
forall {a}. [a] -> [a] -> [[a]]
go []
     where
      go :: [a] -> [a] -> [[a]]
go [a]
_  []     = []
      go [a]
xs (a
y:[a]
ys) = ([a]
xs [a] -> [a] -> [a]
forall a. [a] -> [a] -> [a]
++ [a]
ys) [a] -> [[a]] -> [[a]]
forall a. a -> [a] -> [a]
: [a] -> [a] -> [[a]]
go ([a]
xs [a] -> [a] -> [a]
forall a. [a] -> [a] -> [a]
++ [a
y]) [a]
ys

disjointExpressionConsolidation 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 disjointExpressionConsolidation #-}

decFunName :: Term -> OccName
decFunName :: Term -> Text
decFunName Term
fun = [Text] -> Text
forall a. HasCallStack => [a] -> a
last ([Text] -> Text) -> (Text -> [Text]) -> Text -> Text
forall b c a. (b -> c) -> (a -> b) -> a -> c
. HasCallStack => Text -> Text -> [Text]
Text -> Text -> [Text]
Text.splitOn Text
"." (Text -> Text) -> Text -> Text
forall a b. (a -> b) -> a -> b
$ case Term -> (Term, [Either Term Type])
collectArgs Term
fun of
  (Var Id
v, [Either Term Type]
_) -> Name Term -> Text
forall a. Name a -> Text
nameOcc (Id -> Name Term
forall a. Var a -> Name a
varName Id
v)
  (Prim PrimInfo
p, [Either Term Type]
_) -> PrimInfo -> Text
primName PrimInfo
p
  (Term, [Either Term Type])
_ -> Text
"complex_expression"

data CaseTree a
  = Leaf a
  | LB [LetBinding] (CaseTree a)
  | Branch Term [(Pat,CaseTree a)]
  deriving (CaseTree a -> CaseTree a -> Bool
(CaseTree a -> CaseTree a -> Bool)
-> (CaseTree a -> CaseTree a -> Bool) -> Eq (CaseTree a)
forall a. Eq a => CaseTree a -> CaseTree a -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: forall a. Eq a => CaseTree a -> CaseTree a -> Bool
== :: CaseTree a -> CaseTree a -> Bool
$c/= :: forall a. Eq a => CaseTree a -> CaseTree a -> Bool
/= :: CaseTree a -> CaseTree a -> Bool
Eq,Int -> CaseTree a -> ShowS
[CaseTree a] -> ShowS
CaseTree a -> [Char]
(Int -> CaseTree a -> ShowS)
-> (CaseTree a -> [Char])
-> ([CaseTree a] -> ShowS)
-> Show (CaseTree a)
forall a. Show a => Int -> CaseTree a -> ShowS
forall a. Show a => [CaseTree a] -> ShowS
forall a. Show a => CaseTree a -> [Char]
forall a.
(Int -> a -> ShowS) -> (a -> [Char]) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: forall a. Show a => Int -> CaseTree a -> ShowS
showsPrec :: Int -> CaseTree a -> ShowS
$cshow :: forall a. Show a => CaseTree a -> [Char]
show :: CaseTree a -> [Char]
$cshowList :: forall a. Show a => [CaseTree a] -> ShowS
showList :: [CaseTree a] -> ShowS
Show,(forall a b. (a -> b) -> CaseTree a -> CaseTree b)
-> (forall a b. a -> CaseTree b -> CaseTree a) -> Functor CaseTree
forall a b. a -> CaseTree b -> CaseTree a
forall a b. (a -> b) -> CaseTree a -> CaseTree b
forall (f :: Type -> Type).
(forall a b. (a -> b) -> f a -> f b)
-> (forall a b. a -> f b -> f a) -> Functor f
$cfmap :: forall a b. (a -> b) -> CaseTree a -> CaseTree b
fmap :: forall a b. (a -> b) -> CaseTree a -> CaseTree b
$c<$ :: forall a b. a -> CaseTree b -> CaseTree a
<$ :: forall a b. a -> CaseTree b -> CaseTree a
Functor,(forall m. Monoid m => CaseTree m -> m)
-> (forall m a. Monoid m => (a -> m) -> CaseTree a -> m)
-> (forall m a. Monoid m => (a -> m) -> CaseTree a -> m)
-> (forall a b. (a -> b -> b) -> b -> CaseTree a -> b)
-> (forall a b. (a -> b -> b) -> b -> CaseTree a -> b)
-> (forall b a. (b -> a -> b) -> b -> CaseTree a -> b)
-> (forall b a. (b -> a -> b) -> b -> CaseTree a -> b)
-> (forall a. (a -> a -> a) -> CaseTree a -> a)
-> (forall a. (a -> a -> a) -> CaseTree a -> a)
-> (forall a. CaseTree a -> [a])
-> (forall a. CaseTree a -> Bool)
-> (forall a. CaseTree a -> Int)
-> (forall a. Eq a => a -> CaseTree a -> Bool)
-> (forall a. Ord a => CaseTree a -> a)
-> (forall a. Ord a => CaseTree a -> a)
-> (forall a. Num a => CaseTree a -> a)
-> (forall a. Num a => CaseTree a -> a)
-> Foldable CaseTree
forall a. Eq a => a -> CaseTree a -> Bool
forall a. Num a => CaseTree a -> a
forall a. Ord a => CaseTree a -> a
forall m. Monoid m => CaseTree m -> m
forall a. CaseTree a -> Bool
forall a. CaseTree a -> Int
forall a. CaseTree a -> [a]
forall a. (a -> a -> a) -> CaseTree a -> a
forall m a. Monoid m => (a -> m) -> CaseTree a -> m
forall b a. (b -> a -> b) -> b -> CaseTree a -> b
forall a b. (a -> b -> b) -> b -> CaseTree a -> b
forall (t :: Type -> Type).
(forall m. Monoid m => t m -> m)
-> (forall m a. Monoid m => (a -> m) -> t a -> m)
-> (forall m a. Monoid m => (a -> m) -> t a -> m)
-> (forall a b. (a -> b -> b) -> b -> t a -> b)
-> (forall a b. (a -> b -> b) -> b -> t a -> b)
-> (forall b a. (b -> a -> b) -> b -> t a -> b)
-> (forall b a. (b -> a -> b) -> b -> t a -> b)
-> (forall a. (a -> a -> a) -> t a -> a)
-> (forall a. (a -> a -> a) -> t a -> a)
-> (forall a. t a -> [a])
-> (forall a. t a -> Bool)
-> (forall a. t a -> Int)
-> (forall a. Eq a => a -> t a -> Bool)
-> (forall a. Ord a => t a -> a)
-> (forall a. Ord a => t a -> a)
-> (forall a. Num a => t a -> a)
-> (forall a. Num a => t a -> a)
-> Foldable t
$cfold :: forall m. Monoid m => CaseTree m -> m
fold :: forall m. Monoid m => CaseTree m -> m
$cfoldMap :: forall m a. Monoid m => (a -> m) -> CaseTree a -> m
foldMap :: forall m a. Monoid m => (a -> m) -> CaseTree a -> m
$cfoldMap' :: forall m a. Monoid m => (a -> m) -> CaseTree a -> m
foldMap' :: forall m a. Monoid m => (a -> m) -> CaseTree a -> m
$cfoldr :: forall a b. (a -> b -> b) -> b -> CaseTree a -> b
foldr :: forall a b. (a -> b -> b) -> b -> CaseTree a -> b
$cfoldr' :: forall a b. (a -> b -> b) -> b -> CaseTree a -> b
foldr' :: forall a b. (a -> b -> b) -> b -> CaseTree a -> b
$cfoldl :: forall b a. (b -> a -> b) -> b -> CaseTree a -> b
foldl :: forall b a. (b -> a -> b) -> b -> CaseTree a -> b
$cfoldl' :: forall b a. (b -> a -> b) -> b -> CaseTree a -> b
foldl' :: forall b a. (b -> a -> b) -> b -> CaseTree a -> b
$cfoldr1 :: forall a. (a -> a -> a) -> CaseTree a -> a
foldr1 :: forall a. (a -> a -> a) -> CaseTree a -> a
$cfoldl1 :: forall a. (a -> a -> a) -> CaseTree a -> a
foldl1 :: forall a. (a -> a -> a) -> CaseTree a -> a
$ctoList :: forall a. CaseTree a -> [a]
toList :: forall a. CaseTree a -> [a]
$cnull :: forall a. CaseTree a -> Bool
null :: forall a. CaseTree a -> Bool
$clength :: forall a. CaseTree a -> Int
length :: forall a. CaseTree a -> Int
$celem :: forall a. Eq a => a -> CaseTree a -> Bool
elem :: forall a. Eq a => a -> CaseTree a -> Bool
$cmaximum :: forall a. Ord a => CaseTree a -> a
maximum :: forall a. Ord a => CaseTree a -> a
$cminimum :: forall a. Ord a => CaseTree a -> a
minimum :: forall a. Ord a => CaseTree a -> a
$csum :: forall a. Num a => CaseTree a -> a
sum :: forall a. Num a => CaseTree a -> a
$cproduct :: forall a. Num a => CaseTree a -> a
product :: forall a. Num a => CaseTree a -> a
Foldable)

instance Applicative CaseTree where
  pure :: forall a. a -> CaseTree a
pure = a -> CaseTree a
forall a. a -> CaseTree a
Leaf
  liftA2 :: forall a b c.
(a -> b -> c) -> CaseTree a -> CaseTree b -> CaseTree c
liftA2 a -> b -> c
f (Leaf a
a) (Leaf b
b) = c -> CaseTree c
forall a. a -> CaseTree a
Leaf (a -> b -> c
f a
a b
b)
  liftA2 a -> b -> c
f (LB [LetBinding]
lb CaseTree a
c1) (LB [LetBinding]
_ CaseTree b
c2) = [LetBinding] -> CaseTree c -> CaseTree c
forall a. [LetBinding] -> CaseTree a -> CaseTree a
LB [LetBinding]
lb ((a -> b -> c) -> CaseTree a -> CaseTree b -> CaseTree c
forall a b c.
(a -> b -> c) -> CaseTree a -> CaseTree b -> CaseTree c
forall (f :: Type -> Type) a b c.
Applicative f =>
(a -> b -> c) -> f a -> f b -> f c
liftA2 a -> b -> c
f CaseTree a
c1 CaseTree b
c2)
  liftA2 a -> b -> c
f (Branch Term
scrut [(Pat, CaseTree a)]
alts1) (Branch Term
_ [(Pat, CaseTree b)]
alts2) =
    Term -> [(Pat, CaseTree c)] -> CaseTree c
forall a. Term -> [(Pat, CaseTree a)] -> CaseTree a
Branch Term
scrut (((Pat, CaseTree a) -> (Pat, CaseTree b) -> (Pat, CaseTree c))
-> [(Pat, CaseTree a)]
-> [(Pat, CaseTree b)]
-> [(Pat, CaseTree c)]
forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
zipWith (\(Pat
p1,CaseTree a
a1) (Pat
_,CaseTree b
a2) -> (Pat
p1,(a -> b -> c) -> CaseTree a -> CaseTree b -> CaseTree c
forall a b c.
(a -> b -> c) -> CaseTree a -> CaseTree b -> CaseTree c
forall (f :: Type -> Type) a b c.
Applicative f =>
(a -> b -> c) -> f a -> f b -> f c
liftA2 a -> b -> c
f CaseTree a
a1 CaseTree b
a2)) [(Pat, CaseTree a)]
alts1 [(Pat, CaseTree b)]
alts2)
  liftA2 a -> b -> c
_ CaseTree a
_ CaseTree b
_ = [Char] -> CaseTree c
forall a. HasCallStack => [Char] -> a
error [Char]
"CaseTree.liftA2: internal error, this should not happen."

-- | Test if a 'CaseTree' collected from an expression indicates that
-- application of a global binder is disjoint: occur in separate branches of a
-- case-expression.
isDisjoint :: CaseTree ([Either Term Type])
           -> Bool
isDisjoint :: CaseTree [Either Term Type] -> Bool
isDisjoint (Branch Term
_ [(Pat, CaseTree [Either Term Type])
_]) = Bool
False
isDisjoint CaseTree [Either Term Type]
ct = CaseTree [Either Term Type] -> Bool
forall {b} {a}. Eq b => CaseTree [Either a b] -> Bool
go CaseTree [Either Term Type]
ct
  where
    go :: CaseTree [Either a b] -> Bool
go (Leaf [Either a b]
_)             = Bool
False
    go (LB [LetBinding]
_ CaseTree [Either a b]
ct')           = CaseTree [Either a b] -> Bool
go CaseTree [Either a b]
ct'
    go (Branch Term
_ [])        = Bool
False
    go (Branch Term
_ [(Pat
_,CaseTree [Either a b]
x)])   = CaseTree [Either a b] -> Bool
go CaseTree [Either a b]
x
    go b :: CaseTree [Either a b]
b@(Branch Term
_ ((Pat, CaseTree [Either a b])
_:(Pat, CaseTree [Either a b])
_:[(Pat, CaseTree [Either a b])]
_)) = [[b]] -> Bool
forall a. Eq a => [a] -> Bool
allEqual (([Either a b] -> [b]) -> [[Either a b]] -> [[b]]
forall a b. (a -> b) -> [a] -> [b]
map [Either a b] -> [b]
forall a b. [Either a b] -> [b]
Either.rights (CaseTree [Either a b] -> [[Either a b]]
forall a. CaseTree a -> [a]
forall (t :: Type -> Type) a. Foldable t => t a -> [a]
Foldable.toList CaseTree [Either a b]
b))

-- | Test if all elements in a list are equal to each other.
allEqual :: Eq a => [a] -> Bool
allEqual :: forall a. Eq a => [a] -> Bool
allEqual []     = Bool
True
allEqual (a
x:[a]
xs) = (a -> Bool) -> [a] -> Bool
forall (t :: Type -> Type) a.
Foldable t =>
(a -> Bool) -> t a -> Bool
all (a -> a -> Bool
forall a. Eq a => a -> a -> Bool
== a
x) [a]
xs

-- | Collect 'CaseTree's for (potentially) disjoint applications of globals out
-- of an expression. Also substitute truly disjoint applications of globals by a
-- reference to a lifted out application.
collectGlobals
  :: InScopeSet
  -> [(Term,Term)]
  -- ^ Substitution of (applications of) a global binder by a reference to a
  -- lifted term.
  -> [Term]
  -- ^ List of already seen global binders
  -> Term
  -- ^ The expression
  -> NormalizeSession (Term, InScopeSet, [(Term, ([Term], CaseTree [Either Term Type]))])
collectGlobals :: InScopeSet
-> [(Term, Term)]
-> [Term]
-> Term
-> NormalizeSession
     (Term, InScopeSet, [(Term, ([Term], CaseTree [Either Term Type]))])
collectGlobals InScopeSet
is0 [(Term, Term)]
substitution [Term]
seen (Case Term
scrut Type
ty [Alt]
alts) = do
  rec (alts1, isAlts, collectedAlts) <-
        collectGlobalsAlts is0 substitution seen scrut1 alts
      (scrut1, isScrut, collectedScrut) <-
        collectGlobals is0 substitution (map fst collectedAlts ++ seen) scrut
  return ( Case scrut1 ty alts1
         , unionInScope isAlts isScrut
         , collectedAlts ++ collectedScrut )

collectGlobals InScopeSet
is0 [(Term, Term)]
substitution [Term]
seen e :: Term
e@(Term -> (Term, [Either Term Type], [TickInfo])
collectArgsTicks -> (Term
fun, args :: [Either Term Type]
args@(Either Term Type
_:[Either Term Type]
_), [TickInfo]
ticks))
  | Bool -> Bool
not (Term -> Bool
isConstant 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
    bndrs <- Lens.use bindings
    evaluate <- Lens.view evaluator
    ids <- Lens.use uniqSupply
    let (ids1,ids2) = splitSupply ids
    uniqSupply Lens..= ids2
    gh <- Lens.use globalHeap
    let eval = (Getting Term (PrimHeap, PureHeap, Term) Term
-> (PrimHeap, PureHeap, Term) -> Term
forall s (m :: Type -> Type) a.
MonadReader s m =>
Getting a s a -> m a
Lens.view Getting Term (PrimHeap, PureHeap, Term) Term
forall s t a b. Field3 s t a b => Lens s t a b
Lens
  (PrimHeap, PureHeap, Term) (PrimHeap, PureHeap, Term) Term Term
Lens._3) ((PrimHeap, PureHeap, Term) -> Term)
-> (Term -> (PrimHeap, PureHeap, Term)) -> Term -> Term
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Evaluator
-> BindingMap
-> PureHeap
-> TyConMap
-> PrimHeap
-> Supply
-> InScopeSet
-> Bool
-> Term
-> (PrimHeap, PureHeap, Term)
whnf' Evaluator
evaluate BindingMap
bndrs PureHeap
forall a. Monoid a => a
mempty TyConMap
tcm PrimHeap
gh Supply
ids1 InScopeSet
is0 Bool
False
    let eTy  = TyConMap -> Term -> Type
forall a. InferType a => TyConMap -> a -> Type
inferCoreTypeOf TyConMap
tcm Term
e
    untran <- isUntranslatableType False eTy
    case untran of
      -- Don't lift out non-representable values, because they cannot be let-bound
      -- in our desired normal form.
      Bool
False -> do
        -- Look for, and substitute by, disjoint applications of globals in
        -- the arguments first before considering the current term in function
        -- position. Doing it in the other order (this term in function position
        -- first, followed by arguments) resulted in issue #1322
        (args1,isArgs,collectedArgs) <-
          InScopeSet
-> [(Term, Term)]
-> [Term]
-> [Either Term Type]
-> NormalizeSession
     ([Either Term Type], InScopeSet,
      [(Term, ([Term], CaseTree [Either Term Type]))])
collectGlobalsArgs InScopeSet
is0 [(Term, Term)]
substitution [Term]
seen [Either Term Type]
args
        let seenInArgs = ((Term, ([Term], CaseTree [Either Term Type])) -> Term)
-> [(Term, ([Term], CaseTree [Either Term Type]))] -> [Term]
forall a b. (a -> b) -> [a] -> [b]
map (Term, ([Term], CaseTree [Either Term Type])) -> Term
forall a b. (a, b) -> a
fst [(Term, ([Term], CaseTree [Either Term Type]))]
collectedArgs [Term] -> [Term] -> [Term]
forall a. [a] -> [a] -> [a]
++ [Term]
seen
            isInteresting = InScopeSet
-> (Term -> Term)
-> Term
-> [Either Term Type]
-> [TickInfo]
-> Maybe Term
interestingToLift InScopeSet
is0 Term -> Term
eval Term
fun [Either Term Type]
args [TickInfo]
ticks
        case isInteresting of
          Just Term
fun1 | Term
fun1 Term -> [Term] -> Bool
forall (t :: Type -> Type) a.
(Foldable t, Eq a) =>
a -> t a -> Bool
`notElem` [Term]
seenInArgs -> do
            let e1 :: Term
e1 = Term -> Maybe Term -> Term
forall a. a -> Maybe a -> a
Maybe.fromMaybe (Term -> [Either Term Type] -> Term
mkApps (Term -> [TickInfo] -> Term
mkTicks Term
fun1 [TickInfo]
ticks) [Either Term Type]
args1) (Term -> [(Term, Term)] -> Maybe Term
forall a b. Eq a => a -> [(a, b)] -> Maybe b
List.lookup Term
fun1 [(Term, Term)]
substitution)
            -- This function is lifted out an environment with the currently 'seen'
            -- binders. When we later apply substitution, we need to start with this
            -- environment, otherwise we perform incorrect substitutions in the
            -- arguments.
            (Term, InScopeSet, [(Term, ([Term], CaseTree [Either Term Type]))])
-> NormalizeSession
     (Term, InScopeSet, [(Term, ([Term], CaseTree [Either Term Type]))])
forall a. a -> RewriteMonad NormalizeState a
forall (m :: Type -> Type) a. Monad m => a -> m a
return (Term
e1,InScopeSet
isArgs,(Term
fun1,([Term]
seen,[Either Term Type] -> CaseTree [Either Term Type]
forall a. a -> CaseTree a
Leaf [Either Term Type]
args1))(Term, ([Term], CaseTree [Either Term Type]))
-> [(Term, ([Term], CaseTree [Either Term Type]))]
-> [(Term, ([Term], CaseTree [Either Term Type]))]
forall a. a -> [a] -> [a]
:[(Term, ([Term], CaseTree [Either Term Type]))]
collectedArgs)
          Maybe Term
_ -> (Term, InScopeSet, [(Term, ([Term], CaseTree [Either Term Type]))])
-> NormalizeSession
     (Term, InScopeSet, [(Term, ([Term], CaseTree [Either Term Type]))])
forall a. a -> RewriteMonad NormalizeState a
forall (m :: Type -> Type) a. Monad m => a -> m a
return (Term -> [Either Term Type] -> Term
mkApps (Term -> [TickInfo] -> Term
mkTicks Term
fun [TickInfo]
ticks) [Either Term Type]
args1, InScopeSet
isArgs, [(Term, ([Term], CaseTree [Either Term Type]))]
collectedArgs)
      Bool
_ -> (Term, InScopeSet, [(Term, ([Term], CaseTree [Either Term Type]))])
-> NormalizeSession
     (Term, InScopeSet, [(Term, ([Term], CaseTree [Either Term Type]))])
forall a. a -> RewriteMonad NormalizeState a
forall (m :: Type -> Type) a. Monad m => a -> m a
return (Term
e,InScopeSet
is0,[])

-- FIXME: This duplicates A LOT of let-bindings, where I just pray that after
-- the ANF, CSE, and DeadCodeRemoval pass all duplicates are removed.
--
-- I think we should be able to do better, but perhaps we cannot fix it here.
collectGlobals InScopeSet
is0 [(Term, Term)]
substitution [Term]
seen (Letrec [LetBinding]
lbs Term
body) = do
  let is1 :: InScopeSet
is1 = InScopeSet -> [Id] -> InScopeSet
forall a. InScopeSet -> [Var a] -> InScopeSet
extendInScopeSetList InScopeSet
is0 ((LetBinding -> Id) -> [LetBinding] -> [Id]
forall a b. (a -> b) -> [a] -> [b]
map LetBinding -> Id
forall a b. (a, b) -> a
fst [LetBinding]
lbs)
  (body1,isBody,collectedBody) <-
    InScopeSet
-> [(Term, Term)]
-> [Term]
-> Term
-> NormalizeSession
     (Term, InScopeSet, [(Term, ([Term], CaseTree [Either Term Type]))])
collectGlobals InScopeSet
is1 [(Term, Term)]
substitution [Term]
seen Term
body
  (lbs1,isBndrs,collectedBndrs) <-
    collectGlobalsLbs is1 substitution (map fst collectedBody ++ seen) lbs
  return ( Letrec lbs1 body1
         , unionInScope isBody isBndrs
         , map (second (second (LB lbs1))) (collectedBody ++ collectedBndrs)
         )

collectGlobals InScopeSet
is0 [(Term, Term)]
substitution [Term]
seen (Tick TickInfo
t Term
e) = do
  (e1,is1,collected) <- InScopeSet
-> [(Term, Term)]
-> [Term]
-> Term
-> NormalizeSession
     (Term, InScopeSet, [(Term, ([Term], CaseTree [Either Term Type]))])
collectGlobals InScopeSet
is0 [(Term, Term)]
substitution [Term]
seen Term
e
  return (Tick t e1, is1, collected)

collectGlobals InScopeSet
is0 [(Term, Term)]
_ [Term]
_ Term
e = (Term, InScopeSet, [(Term, ([Term], CaseTree [Either Term Type]))])
-> NormalizeSession
     (Term, InScopeSet, [(Term, ([Term], CaseTree [Either Term Type]))])
forall a. a -> RewriteMonad NormalizeState a
forall (m :: Type -> Type) a. Monad m => a -> m a
return (Term
e,InScopeSet
is0,[])

-- | Collect 'CaseTree's for (potentially) disjoint applications of globals out
-- of a list of application arguments. Also substitute truly disjoint
-- applications of globals by a reference to a lifted out application.
collectGlobalsArgs
  :: InScopeSet
  -> [(Term,Term)] -- ^ Substitution of (applications of) a global
                   -- binder by a reference to a lifted term.
  -> [Term] -- ^ List of already seen global binders
  -> [Either Term Type] -- ^ The list of arguments
  -> NormalizeSession
       ( [Either Term Type]
       , InScopeSet
       , [(Term, ([Term], CaseTree [(Either Term Type)]))]
       )
collectGlobalsArgs :: InScopeSet
-> [(Term, Term)]
-> [Term]
-> [Either Term Type]
-> NormalizeSession
     ([Either Term Type], InScopeSet,
      [(Term, ([Term], CaseTree [Either Term Type]))])
collectGlobalsArgs InScopeSet
is0 [(Term, Term)]
substitution [Term]
seen [Either Term Type]
args = do
    ((is1,_),(args',collected)) <- ([(Either Term Type,
   [(Term, ([Term], CaseTree [Either Term Type]))])]
 -> ([Either Term Type],
     [[(Term, ([Term], CaseTree [Either Term Type]))]]))
-> ((InScopeSet, [Term]),
    [(Either Term Type,
      [(Term, ([Term], CaseTree [Either Term Type]))])])
-> ((InScopeSet, [Term]),
    ([Either Term Type],
     [[(Term, ([Term], CaseTree [Either Term Type]))]]))
forall b c a. (b -> c) -> (a, b) -> (a, c)
forall (p :: Type -> Type -> Type) b c a.
Bifunctor p =>
(b -> c) -> p a b -> p a c
second [(Either Term Type,
  [(Term, ([Term], CaseTree [Either Term Type]))])]
-> ([Either Term Type],
    [[(Term, ([Term], CaseTree [Either Term Type]))]])
forall a b. [(a, b)] -> ([a], [b])
unzip (((InScopeSet, [Term]),
  [(Either Term Type,
    [(Term, ([Term], CaseTree [Either Term Type]))])])
 -> ((InScopeSet, [Term]),
     ([Either Term Type],
      [[(Term, ([Term], CaseTree [Either Term Type]))]])))
-> RewriteMonad
     NormalizeState
     ((InScopeSet, [Term]),
      [(Either Term Type,
        [(Term, ([Term], CaseTree [Either Term Type]))])])
-> RewriteMonad
     NormalizeState
     ((InScopeSet, [Term]),
      ([Either Term Type],
       [[(Term, ([Term], CaseTree [Either Term Type]))]]))
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> ((InScopeSet, [Term])
 -> Either Term Type
 -> RewriteMonad
      NormalizeState
      ((InScopeSet, [Term]),
       (Either Term Type,
        [(Term, ([Term], CaseTree [Either Term Type]))])))
-> (InScopeSet, [Term])
-> [Either Term Type]
-> RewriteMonad
     NormalizeState
     ((InScopeSet, [Term]),
      [(Either Term Type,
        [(Term, ([Term], CaseTree [Either Term Type]))])])
forall (m :: Type -> Type) acc x y.
Monad m =>
(acc -> x -> m (acc, y)) -> acc -> [x] -> m (acc, [y])
List.mapAccumLM (InScopeSet, [Term])
-> Either Term Type
-> RewriteMonad
     NormalizeState
     ((InScopeSet, [Term]),
      (Either Term Type,
       [(Term, ([Term], CaseTree [Either Term Type]))]))
forall {b}.
(InScopeSet, [Term])
-> Either Term b
-> RewriteMonad
     NormalizeState
     ((InScopeSet, [Term]),
      (Either Term b, [(Term, ([Term], CaseTree [Either Term Type]))]))
go (InScopeSet
is0,[Term]
seen) [Either Term Type]
args
    return (args',is1,concat collected)
  where
    go :: (InScopeSet, [Term])
-> Either Term b
-> RewriteMonad
     NormalizeState
     ((InScopeSet, [Term]),
      (Either Term b, [(Term, ([Term], CaseTree [Either Term Type]))]))
go (InScopeSet
isN0,[Term]
s) (Left Term
tm) = do
      (tm',isN1,collected) <- InScopeSet
-> [(Term, Term)]
-> [Term]
-> Term
-> NormalizeSession
     (Term, InScopeSet, [(Term, ([Term], CaseTree [Either Term Type]))])
collectGlobals InScopeSet
isN0 [(Term, Term)]
substitution [Term]
s Term
tm
      return ((isN1,map fst collected ++ s),(Left tm',collected))
    go (InScopeSet
isN,[Term]
s) (Right b
ty) = ((InScopeSet, [Term]),
 (Either Term b, [(Term, ([Term], CaseTree [Either Term Type]))]))
-> RewriteMonad
     NormalizeState
     ((InScopeSet, [Term]),
      (Either Term b, [(Term, ([Term], CaseTree [Either Term Type]))]))
forall a. a -> RewriteMonad NormalizeState a
forall (m :: Type -> Type) a. Monad m => a -> m a
return ((InScopeSet
isN,[Term]
s),(b -> Either Term b
forall a b. b -> Either a b
Right b
ty,[]))

-- | Collect 'CaseTree's for (potentially) disjoint applications of globals out
-- of a list of alternatives. Also substitute truly disjoint applications of
-- globals by a reference to a lifted out application.
collectGlobalsAlts ::
     InScopeSet
  -> [(Term,Term)] -- ^ Substitution of (applications of) a global
                   -- binder by a reference to a lifted term.
  -> [Term] -- ^ List of already seen global binders
  -> Term -- ^ The subject term
  -> [Alt] -- ^ The list of alternatives
  -> NormalizeSession
       ( [Alt]
       , InScopeSet
       , [(Term, ([Term], CaseTree [(Either Term Type)]))]
       )
collectGlobalsAlts :: InScopeSet
-> [(Term, Term)]
-> [Term]
-> Term
-> [Alt]
-> NormalizeSession
     ([Alt], InScopeSet,
      [(Term, ([Term], CaseTree [Either Term Type]))])
collectGlobalsAlts InScopeSet
is0 [(Term, Term)]
substitution [Term]
seen Term
scrut [Alt]
alts = do
    (is1,(alts',collected)) <- ([(Alt, [(Term, ([Term], (Pat, CaseTree [Either Term Type])))])]
 -> ([Alt],
     [[(Term, ([Term], (Pat, CaseTree [Either Term Type])))]]))
-> (InScopeSet,
    [(Alt, [(Term, ([Term], (Pat, CaseTree [Either Term Type])))])])
-> (InScopeSet,
    ([Alt], [[(Term, ([Term], (Pat, CaseTree [Either Term Type])))]]))
forall b c a. (b -> c) -> (a, b) -> (a, c)
forall (p :: Type -> Type -> Type) b c a.
Bifunctor p =>
(b -> c) -> p a b -> p a c
second [(Alt, [(Term, ([Term], (Pat, CaseTree [Either Term Type])))])]
-> ([Alt],
    [[(Term, ([Term], (Pat, CaseTree [Either Term Type])))]])
forall a b. [(a, b)] -> ([a], [b])
unzip ((InScopeSet,
  [(Alt, [(Term, ([Term], (Pat, CaseTree [Either Term Type])))])])
 -> (InScopeSet,
     ([Alt], [[(Term, ([Term], (Pat, CaseTree [Either Term Type])))]])))
-> RewriteMonad
     NormalizeState
     (InScopeSet,
      [(Alt, [(Term, ([Term], (Pat, CaseTree [Either Term Type])))])])
-> RewriteMonad
     NormalizeState
     (InScopeSet,
      ([Alt], [[(Term, ([Term], (Pat, CaseTree [Either Term Type])))]]))
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> (InScopeSet
 -> Alt
 -> RewriteMonad
      NormalizeState
      (InScopeSet,
       (Alt, [(Term, ([Term], (Pat, CaseTree [Either Term Type])))])))
-> InScopeSet
-> [Alt]
-> RewriteMonad
     NormalizeState
     (InScopeSet,
      [(Alt, [(Term, ([Term], (Pat, CaseTree [Either Term Type])))])])
forall (m :: Type -> Type) acc x y.
Monad m =>
(acc -> x -> m (acc, y)) -> acc -> [x] -> m (acc, [y])
List.mapAccumLM InScopeSet
-> Alt
-> RewriteMonad
     NormalizeState
     (InScopeSet,
      (Alt, [(Term, ([Term], (Pat, CaseTree [Either Term Type])))]))
go InScopeSet
is0 [Alt]
alts
    let collectedM  = ([(Term, ([Term], (Pat, CaseTree [Either Term Type])))]
 -> Map Term ([Term], [(Pat, CaseTree [Either Term Type])]))
-> [[(Term, ([Term], (Pat, CaseTree [Either Term Type])))]]
-> [Map Term ([Term], [(Pat, CaseTree [Either Term Type])])]
forall a b. (a -> b) -> [a] -> [b]
map ([(Term, ([Term], [(Pat, CaseTree [Either Term Type])]))]
-> Map Term ([Term], [(Pat, CaseTree [Either Term Type])])
forall k a. Ord k => [(k, a)] -> Map k a
Map.fromList ([(Term, ([Term], [(Pat, CaseTree [Either Term Type])]))]
 -> Map Term ([Term], [(Pat, CaseTree [Either Term Type])]))
-> ([(Term, ([Term], (Pat, CaseTree [Either Term Type])))]
    -> [(Term, ([Term], [(Pat, CaseTree [Either Term Type])]))])
-> [(Term, ([Term], (Pat, CaseTree [Either Term Type])))]
-> Map Term ([Term], [(Pat, CaseTree [Either Term Type])])
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ((Term, ([Term], (Pat, CaseTree [Either Term Type])))
 -> (Term, ([Term], [(Pat, CaseTree [Either Term Type])])))
-> [(Term, ([Term], (Pat, CaseTree [Either Term Type])))]
-> [(Term, ([Term], [(Pat, CaseTree [Either Term Type])]))]
forall a b. (a -> b) -> [a] -> [b]
map ((([Term], (Pat, CaseTree [Either Term Type]))
 -> ([Term], [(Pat, CaseTree [Either Term Type])]))
-> (Term, ([Term], (Pat, CaseTree [Either Term Type])))
-> (Term, ([Term], [(Pat, CaseTree [Either Term Type])]))
forall b c a. (b -> c) -> (a, b) -> (a, c)
forall (p :: Type -> Type -> Type) b c a.
Bifunctor p =>
(b -> c) -> p a b -> p a c
second (((Pat, CaseTree [Either Term Type])
 -> [(Pat, CaseTree [Either Term Type])])
-> ([Term], (Pat, CaseTree [Either Term Type]))
-> ([Term], [(Pat, CaseTree [Either Term Type])])
forall b c a. (b -> c) -> (a, b) -> (a, c)
forall (p :: Type -> Type -> Type) b c a.
Bifunctor p =>
(b -> c) -> p a b -> p a c
second ((Pat, CaseTree [Either Term Type])
-> [(Pat, CaseTree [Either Term Type])]
-> [(Pat, CaseTree [Either Term Type])]
forall a. a -> [a] -> [a]
:[])))) [[(Term, ([Term], (Pat, CaseTree [Either Term Type])))]]
collected
        collectedUN = (([Term], [(Pat, CaseTree [Either Term Type])])
 -> ([Term], [(Pat, CaseTree [Either Term Type])])
 -> ([Term], [(Pat, CaseTree [Either Term Type])]))
-> [Map Term ([Term], [(Pat, CaseTree [Either Term Type])])]
-> Map Term ([Term], [(Pat, CaseTree [Either Term Type])])
forall (f :: Type -> Type) k a.
(Foldable f, Ord k) =>
(a -> a -> a) -> f (Map k a) -> Map k a
Map.unionsWith (\([Term]
l1,[(Pat, CaseTree [Either Term Type])]
r1) ([Term]
l2,[(Pat, CaseTree [Either Term Type])]
r2) -> ([Term] -> [Term]
forall a. Eq a => [a] -> [a]
List.nub ([Term]
l1 [Term] -> [Term] -> [Term]
forall a. [a] -> [a] -> [a]
++ [Term]
l2),[(Pat, CaseTree [Either Term Type])]
r1 [(Pat, CaseTree [Either Term Type])]
-> [(Pat, CaseTree [Either Term Type])]
-> [(Pat, CaseTree [Either Term Type])]
forall a. [a] -> [a] -> [a]
++ [(Pat, CaseTree [Either Term Type])]
r2)) [Map Term ([Term], [(Pat, CaseTree [Either Term Type])])]
collectedM
        collected'  = ((Term, ([Term], [(Pat, CaseTree [Either Term Type])]))
 -> (Term, ([Term], CaseTree [Either Term Type])))
-> [(Term, ([Term], [(Pat, CaseTree [Either Term Type])]))]
-> [(Term, ([Term], CaseTree [Either Term Type]))]
forall a b. (a -> b) -> [a] -> [b]
map ((([Term], [(Pat, CaseTree [Either Term Type])])
 -> ([Term], CaseTree [Either Term Type]))
-> (Term, ([Term], [(Pat, CaseTree [Either Term Type])]))
-> (Term, ([Term], CaseTree [Either Term Type]))
forall b c a. (b -> c) -> (a, b) -> (a, c)
forall (p :: Type -> Type -> Type) b c a.
Bifunctor p =>
(b -> c) -> p a b -> p a c
second (([(Pat, CaseTree [Either Term Type])]
 -> CaseTree [Either Term Type])
-> ([Term], [(Pat, CaseTree [Either Term Type])])
-> ([Term], CaseTree [Either Term Type])
forall b c a. (b -> c) -> (a, b) -> (a, c)
forall (p :: Type -> Type -> Type) b c a.
Bifunctor p =>
(b -> c) -> p a b -> p a c
second (Term
-> [(Pat, CaseTree [Either Term Type])]
-> CaseTree [Either Term Type]
forall a. Term -> [(Pat, CaseTree a)] -> CaseTree a
Branch Term
scrut))) (Map Term ([Term], [(Pat, CaseTree [Either Term Type])])
-> [(Term, ([Term], [(Pat, CaseTree [Either Term Type])]))]
forall k a. Map k a -> [(k, a)]
Map.toList Map Term ([Term], [(Pat, CaseTree [Either Term Type])])
collectedUN)
    return (alts',is1,collected')
  where
    go :: InScopeSet
-> Alt
-> RewriteMonad
     NormalizeState
     (InScopeSet,
      (Alt, [(Term, ([Term], (Pat, CaseTree [Either Term Type])))]))
go InScopeSet
isN0 (Pat
p,Term
e) = do
      let isN1 :: InScopeSet
isN1 = InScopeSet -> [Id] -> InScopeSet
forall a. InScopeSet -> [Var a] -> InScopeSet
extendInScopeSetList InScopeSet
isN0 (([TyVar], [Id]) -> [Id]
forall a b. (a, b) -> b
snd (Pat -> ([TyVar], [Id])
patIds Pat
p))
      (e',isN2,collected) <- InScopeSet
-> [(Term, Term)]
-> [Term]
-> Term
-> NormalizeSession
     (Term, InScopeSet, [(Term, ([Term], CaseTree [Either Term Type]))])
collectGlobals InScopeSet
isN1 [(Term, Term)]
substitution [Term]
seen Term
e
      return (isN2,((p,e'),map (second (second (p,))) collected))

-- | Collect 'CaseTree's for (potentially) disjoint applications of globals out
-- of a list of let-bindings. Also substitute truly disjoint applications of
-- globals by a reference to a lifted out application.
collectGlobalsLbs ::
     InScopeSet
  -> [(Term,Term)] -- ^ Substitution of (applications of) a global
                   -- binder by a reference to a lifted term.
  -> [Term] -- ^ List of already seen global binders
  -> [LetBinding] -- ^ The list let-bindings
  -> NormalizeSession
       ( [LetBinding]
       , InScopeSet
       , [(Term, ([Term], CaseTree [(Either Term Type)]))]
       )
collectGlobalsLbs :: InScopeSet
-> [(Term, Term)]
-> [Term]
-> [LetBinding]
-> NormalizeSession
     ([LetBinding], InScopeSet,
      [(Term, ([Term], CaseTree [Either Term Type]))])
collectGlobalsLbs InScopeSet
is0 [(Term, Term)]
substitution [Term]
seen [LetBinding]
lbs = do
    let lbsSCCs :: [SCC LetBinding]
lbsSCCs = HasCallStack => [LetBinding] -> [SCC LetBinding]
[LetBinding] -> [SCC LetBinding]
sccLetBindings [LetBinding]
lbs
    ((is1,_),(lbsSCCs1,collected)) <-
      ([(SCC LetBinding,
   [(Term, ([Term], CaseTree [Either Term Type]))])]
 -> ([SCC LetBinding],
     [[(Term, ([Term], CaseTree [Either Term Type]))]]))
-> ((InScopeSet, [Term]),
    [(SCC LetBinding,
      [(Term, ([Term], CaseTree [Either Term Type]))])])
-> ((InScopeSet, [Term]),
    ([SCC LetBinding],
     [[(Term, ([Term], CaseTree [Either Term Type]))]]))
forall b c a. (b -> c) -> (a, b) -> (a, c)
forall (p :: Type -> Type -> Type) b c a.
Bifunctor p =>
(b -> c) -> p a b -> p a c
second [(SCC LetBinding, [(Term, ([Term], CaseTree [Either Term Type]))])]
-> ([SCC LetBinding],
    [[(Term, ([Term], CaseTree [Either Term Type]))]])
forall a b. [(a, b)] -> ([a], [b])
unzip (((InScopeSet, [Term]),
  [(SCC LetBinding,
    [(Term, ([Term], CaseTree [Either Term Type]))])])
 -> ((InScopeSet, [Term]),
     ([SCC LetBinding],
      [[(Term, ([Term], CaseTree [Either Term Type]))]])))
-> RewriteMonad
     NormalizeState
     ((InScopeSet, [Term]),
      [(SCC LetBinding,
        [(Term, ([Term], CaseTree [Either Term Type]))])])
-> RewriteMonad
     NormalizeState
     ((InScopeSet, [Term]),
      ([SCC LetBinding],
       [[(Term, ([Term], CaseTree [Either Term Type]))]]))
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> ((InScopeSet, [Term])
 -> SCC LetBinding
 -> RewriteMonad
      NormalizeState
      ((InScopeSet, [Term]),
       (SCC LetBinding, [(Term, ([Term], CaseTree [Either Term Type]))])))
-> (InScopeSet, [Term])
-> [SCC LetBinding]
-> RewriteMonad
     NormalizeState
     ((InScopeSet, [Term]),
      [(SCC LetBinding,
        [(Term, ([Term], CaseTree [Either Term Type]))])])
forall (m :: Type -> Type) acc x y.
Monad m =>
(acc -> x -> m (acc, y)) -> acc -> [x] -> m (acc, [y])
List.mapAccumLM (InScopeSet, [Term])
-> SCC LetBinding
-> RewriteMonad
     NormalizeState
     ((InScopeSet, [Term]),
      (SCC LetBinding, [(Term, ([Term], CaseTree [Either Term Type]))]))
go (InScopeSet
is0,[Term]
seen) [SCC LetBinding]
lbsSCCs
    return (Graph.flattenSCCs lbsSCCs1,is1,concat collected)
  where
    go :: (InScopeSet,[Term]) -> Graph.SCC LetBinding
       -> NormalizeSession
            ( (InScopeSet, [Term])
            , ( Graph.SCC LetBinding
              , [(Term, ([Term], CaseTree [(Either Term Type)]))]
              )
            )
    go :: (InScopeSet, [Term])
-> SCC LetBinding
-> RewriteMonad
     NormalizeState
     ((InScopeSet, [Term]),
      (SCC LetBinding, [(Term, ([Term], CaseTree [Either Term Type]))]))
go (InScopeSet
isN0,[Term]
s) (Graph.AcyclicSCC (Id
id_, Term
e)) = do
      (e',isN1,collected) <- InScopeSet
-> [(Term, Term)]
-> [Term]
-> Term
-> NormalizeSession
     (Term, InScopeSet, [(Term, ([Term], CaseTree [Either Term Type]))])
collectGlobals InScopeSet
isN0 [(Term, Term)]
substitution [Term]
s Term
e
      return ((isN1,map fst collected ++ s),(Graph.AcyclicSCC (id_,e'),collected))
    -- TODO: This completely skips recursive let-bindings in the collection of
    -- potentially disjoint applications of globals; and skips substituting truly
    -- disjoint applications of globals by a reference to a lifted out application.
    --
    -- This is to prevent the creation of combinational loops that have occurred
    -- "in the wild", but for which we have not been able to a create small
    -- unit test that triggers this creation-of-combinational-loops bug.
    -- Completely skipping recursive let-bindings is taking the hammer to
    -- solving this bug, without knowing whether a scalpel even existed and what
    -- it might look like. We should at some point think hard how traversing
    -- recursive let-bindings can introduce combinational loops, and whether
    -- there exists a solution that can traverse recursive let-bindings,
    -- finding more opportunities for DEC, while not introducing combinational
    -- loops.
    go (InScopeSet, [Term])
acc scc :: SCC LetBinding
scc@(Graph.CyclicSCC {}) = ((InScopeSet, [Term]),
 (SCC LetBinding, [(Term, ([Term], CaseTree [Either Term Type]))]))
-> RewriteMonad
     NormalizeState
     ((InScopeSet, [Term]),
      (SCC LetBinding, [(Term, ([Term], CaseTree [Either Term Type]))]))
forall a. a -> RewriteMonad NormalizeState a
forall (m :: Type -> Type) a. Monad m => a -> m a
return ((InScopeSet, [Term])
acc,(SCC LetBinding
scc,[]))

-- | Given a case-tree corresponding to a disjoint interesting \"term-in-a-
-- function-position\", return a let-expression: where the let-binding holds
-- a case-expression selecting between the distinct arguments of the case-tree,
-- and the body is an application of the term applied to the shared arguments of
-- the case tree, and variable references to the created let-bindings.
--
-- case-expressions whose type would be non-representable are not let-bound,
-- but occur directly in the argument position of the application in the body
-- of the let-expression.
mkDisjointGroup
  :: InScopeSet
  -- ^ Variables in scope at the very top of the case-tree, i.e., the original
  -- expression
  -> (Term,([Term],CaseTree [Either Term Type]))
  -- ^ Case-tree of arguments belonging to the applied term.
  -> NormalizeSession (Term,[Term])
mkDisjointGroup :: InScopeSet
-> (Term, ([Term], CaseTree [Either Term Type]))
-> RewriteMonad NormalizeState (Term, [Term])
mkDisjointGroup InScopeSet
inScope (Term
fun,([Term]
seen,CaseTree [Either Term Type]
cs)) = 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
    let funName = Term -> Text
decFunName Term
fun
        argLen = case CaseTree [Either Term Type] -> [[Either Term Type]]
forall a. CaseTree a -> [a]
forall (t :: Type -> Type) a. Foldable t => t a -> [a]
Foldable.toList CaseTree [Either Term Type]
cs of
                   [] -> [Char] -> Int
forall a. HasCallStack => [Char] -> a
error [Char]
"mkDisjointGroup: no disjoint groups"
                   [Either Term Type]
l:[[Either Term Type]]
_ -> [Either Term Type] -> Int
forall a. [a] -> Int
forall (t :: Type -> Type) a. Foldable t => t a -> Int
length [Either Term Type]
l
        csT :: [CaseTree (Either Term Type)] -- "Transposed" 'CaseTree [Either Term Type]'
        csT = (Int -> CaseTree (Either Term Type))
-> [Int] -> [CaseTree (Either Term Type)]
forall a b. (a -> b) -> [a] -> [b]
map (\Int
i -> ([Either Term Type] -> Either Term Type)
-> CaseTree [Either Term Type] -> CaseTree (Either Term Type)
forall a b. (a -> b) -> CaseTree a -> CaseTree b
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
fmap ([Either Term Type] -> Int -> Either Term Type
forall a. HasCallStack => [a] -> Int -> a
!!Int
i) CaseTree [Either Term Type]
cs) [Int
0..(Int
argLenInt -> Int -> Int
forall a. Num a => a -> a -> a
-Int
1)] -- sequenceA does the wrong thing
    (lbs,newArgs) <- List.mapAccumRM (\[(Id, (Type, CaseTree Term))]
lbs (CaseTree (Either Term Type)
c,Word
pos) -> do
      let cL :: [Either Term Type]
cL = CaseTree (Either Term Type) -> [Either Term Type]
forall a. CaseTree a -> [a]
forall (t :: Type -> Type) a. Foldable t => t a -> [a]
Foldable.toList CaseTree (Either Term Type)
c
      case ([Either Term Type]
cL, TyConMap -> InScopeSet -> [Either Term Type] -> Bool
areShared TyConMap
tcm InScopeSet
inScope ((Either Term Type -> Either Term Type)
-> [Either Term Type] -> [Either Term Type]
forall a b. (a -> b) -> [a] -> [b]
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
fmap ((Term -> Term) -> Either Term Type -> Either Term Type
forall a b c. (a -> b) -> Either a c -> Either b c
forall (p :: Type -> Type -> Type) a b c.
Bifunctor p =>
(a -> b) -> p a c -> p b c
first Term -> Term
stripTicks) [Either Term Type]
cL)) of
        (Right Type
ty:[Either Term Type]
_, Bool
True) ->
          ([(Id, (Type, CaseTree Term))], Either Term Type)
-> RewriteMonad
     NormalizeState ([(Id, (Type, CaseTree Term))], Either Term Type)
forall a. a -> RewriteMonad NormalizeState a
forall (m :: Type -> Type) a. Monad m => a -> m a
return ([(Id, (Type, CaseTree Term))]
lbs,Type -> Either Term Type
forall a b. b -> Either a b
Right Type
ty)
        (Right Type
_:[Either Term Type]
_, Bool
False) ->
          [Char]
-> RewriteMonad
     NormalizeState ([(Id, (Type, CaseTree Term))], Either Term Type)
forall a. HasCallStack => [Char] -> a
error ([Char]
"mkDisjointGroup: non-equal type arguments: " [Char] -> ShowS
forall a. Semigroup a => a -> a -> a
<>
                 [Type] -> [Char]
forall p. PrettyPrec p => p -> [Char]
showPpr ([Either Term Type] -> [Type]
forall a b. [Either a b] -> [b]
Either.rights [Either Term Type]
cL))
        (Left Term
tm:[Either Term Type]
_, Bool
True) ->
          ([(Id, (Type, CaseTree Term))], Either Term Type)
-> RewriteMonad
     NormalizeState ([(Id, (Type, CaseTree Term))], Either Term Type)
forall a. a -> RewriteMonad NormalizeState a
forall (m :: Type -> Type) a. Monad m => a -> m a
return ([(Id, (Type, CaseTree Term))]
lbs,Term -> Either Term Type
forall a b. a -> Either a b
Left Term
tm)
        (Left Term
tm:[Either Term Type]
_, Bool
False) -> do
          let ty :: Type
ty = TyConMap -> Term -> Type
forall a. InferType a => TyConMap -> a -> Type
inferCoreTypeOf TyConMap
tcm Term
tm
          let err :: a
err = [Char] -> a
forall a. HasCallStack => [Char] -> a
error ([Char]
"mkDisjointGroup: mixed type and term arguments: " [Char] -> ShowS
forall a. Semigroup a => a -> a -> a
<> [Either Term Type] -> [Char]
forall a. Show a => a -> [Char]
show [Either Term Type]
cL)
          (lbM,arg) <- InScopeSet
-> Type
-> CaseTree Term
-> Text
-> Word
-> NormalizeSession (Maybe (Id, (Type, CaseTree Term)), Term)
disJointSelProj InScopeSet
inScope Type
ty (Term -> Either Term Type -> Term
forall a b. a -> Either a b -> a
Either.fromLeft Term
forall {a}. a
err (Either Term Type -> Term)
-> CaseTree (Either Term Type) -> CaseTree Term
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> CaseTree (Either Term Type)
c) Text
funName Word
pos
          case lbM of
            Just (Id, (Type, CaseTree Term))
lb -> ([(Id, (Type, CaseTree Term))], Either Term Type)
-> RewriteMonad
     NormalizeState ([(Id, (Type, CaseTree Term))], Either Term Type)
forall a. a -> RewriteMonad NormalizeState a
forall (m :: Type -> Type) a. Monad m => a -> m a
return ((Id, (Type, CaseTree Term))
lb(Id, (Type, CaseTree Term))
-> [(Id, (Type, CaseTree Term))] -> [(Id, (Type, CaseTree Term))]
forall a. a -> [a] -> [a]
:[(Id, (Type, CaseTree Term))]
lbs, Term -> Either Term Type
forall a b. a -> Either a b
Left Term
arg)
            Maybe (Id, (Type, CaseTree Term))
_ -> ([(Id, (Type, CaseTree Term))], Either Term Type)
-> RewriteMonad
     NormalizeState ([(Id, (Type, CaseTree Term))], Either Term Type)
forall a. a -> RewriteMonad NormalizeState a
forall (m :: Type -> Type) a. Monad m => a -> m a
return ([(Id, (Type, CaseTree Term))]
lbs, Term -> Either Term Type
forall a b. a -> Either a b
Left Term
arg)
        ([], Bool
_) ->
          [Char]
-> RewriteMonad
     NormalizeState ([(Id, (Type, CaseTree Term))], Either Term Type)
forall a. HasCallStack => [Char] -> a
error [Char]
"mkDisjointGroup: no arguments"
      ) [] (zip csT [0..])
    let funApp = Term -> [Either Term Type] -> Term
mkApps Term
fun [Either Term Type]
newArgs
    tupTcm <- Lens.view tupleTcCache
    case lbs of
      [] ->
        (Term, [Term]) -> RewriteMonad NormalizeState (Term, [Term])
forall a. a -> RewriteMonad NormalizeState a
forall (m :: Type -> Type) a. Monad m => a -> m a
return (Term
funApp, [Term]
seen)
      [(Id
v,(Type
ty,CaseTree Term
ct))] -> do
        let e :: Term
e = TyConMap
-> IntMap TyConName -> Type -> [Type] -> CaseTree [Term] -> Term
genCase TyConMap
tcm IntMap TyConName
tupTcm Type
ty [Type
ty] ((Term -> [Term]) -> CaseTree Term -> CaseTree [Term]
forall a b. (a -> b) -> CaseTree a -> CaseTree b
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
fmap (Term -> [Term] -> [Term]
forall a. a -> [a] -> [a]
:[]) CaseTree Term
ct)
        (Term, [Term]) -> RewriteMonad NormalizeState (Term, [Term])
forall a. a -> RewriteMonad NormalizeState a
forall (m :: Type -> Type) a. Monad m => a -> m a
return ([LetBinding] -> Term -> Term
Letrec [(Id
v,Term
e)] Term
funApp, [Term]
seen)
      [(Id, (Type, CaseTree Term))]
_ -> do
        let ([Id]
vs,[(Type, CaseTree Term)]
zs) = [(Id, (Type, CaseTree Term))] -> ([Id], [(Type, CaseTree Term)])
forall a b. [(a, b)] -> ([a], [b])
unzip [(Id, (Type, CaseTree Term))]
lbs
            csL :: [CaseTree Term]
            ([Type]
tys,[CaseTree Term]
csL) = [(Type, CaseTree Term)] -> ([Type], [CaseTree Term])
forall a b. [(a, b)] -> ([a], [b])
unzip [(Type, CaseTree Term)]
zs
            csLT :: CaseTree [Term]
            csLT :: CaseTree [Term]
csLT = (([Term] -> [Term]) -> [Term])
-> CaseTree ([Term] -> [Term]) -> CaseTree [Term]
forall a b. (a -> b) -> CaseTree a -> CaseTree b
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
fmap (([Term] -> [Term]) -> [Term] -> [Term]
forall a b. (a -> b) -> a -> b
$ []) ((CaseTree ([Term] -> [Term])
 -> CaseTree ([Term] -> [Term]) -> CaseTree ([Term] -> [Term]))
-> [CaseTree ([Term] -> [Term])] -> CaseTree ([Term] -> [Term])
forall a. (a -> a -> a) -> [a] -> a
forall (t :: Type -> Type) a.
Foldable t =>
(a -> a -> a) -> t a -> a
foldr1 ((([Term] -> [Term]) -> ([Term] -> [Term]) -> [Term] -> [Term])
-> CaseTree ([Term] -> [Term])
-> CaseTree ([Term] -> [Term])
-> CaseTree ([Term] -> [Term])
forall a b c.
(a -> b -> c) -> CaseTree a -> CaseTree b -> CaseTree c
forall (f :: Type -> Type) a b c.
Applicative f =>
(a -> b -> c) -> f a -> f b -> f c
liftA2 ([Term] -> [Term]) -> ([Term] -> [Term]) -> [Term] -> [Term]
forall b c a. (b -> c) -> (a -> b) -> a -> c
(.)) ((CaseTree Term -> CaseTree ([Term] -> [Term]))
-> [CaseTree Term] -> [CaseTree ([Term] -> [Term])]
forall a b. (a -> b) -> [a] -> [b]
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
fmap ((Term -> [Term] -> [Term])
-> CaseTree Term -> CaseTree ([Term] -> [Term])
forall a b. (a -> b) -> CaseTree a -> CaseTree b
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
fmap (:)) [CaseTree Term]
csL))
            bigTupTy :: Type
bigTupTy = TyConMap -> IntMap TyConName -> [Type] -> Type
mkBigTupTy TyConMap
tcm IntMap TyConName
tupTcm [Type]
tys
            ct :: Term
ct = TyConMap
-> IntMap TyConName -> Type -> [Type] -> CaseTree [Term] -> Term
genCase TyConMap
tcm IntMap TyConName
tupTcm Type
bigTupTy [Type]
tys CaseTree [Term]
csLT
        tupIn <- InScopeSet -> Text -> Type -> RewriteMonad NormalizeState Id
forall (m :: Type -> Type).
MonadUnique m =>
InScopeSet -> Text -> Type -> m Id
mkInternalVar InScopeSet
inScope (Text
funName Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Text
"_tupIn") Type
bigTupTy
        projections <-
          Monad.zipWithM (\Id
v Int
n ->
            (Id
v,) (Term -> LetBinding)
-> RewriteMonad NormalizeState Term
-> RewriteMonad NormalizeState LetBinding
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> InScopeSet
-> TyConMap
-> IntMap TyConName
-> Term
-> [Type]
-> Int
-> RewriteMonad NormalizeState Term
forall (m :: Type -> Type).
MonadUnique m =>
InScopeSet
-> TyConMap -> IntMap TyConName -> Term -> [Type] -> Int -> m Term
mkBigTupSelector InScopeSet
inScope TyConMap
tcm IntMap TyConName
tupTcm (Id -> Term
Var Id
tupIn) [Type]
tys Int
n)
            vs [0..]
        return (Letrec ((tupIn,ct):projections) funApp, seen)

-- | Create a selector for the case-tree of the argument. If the argument is
-- representable create a let-binding for the created selector, and return
-- a variable reference to this let-binding. If the argument is not representable
-- return the selector directly.
disJointSelProj
  :: InScopeSet
  -> Type
  -- ^ Types of the argument
  -> CaseTree Term
  -- ^ The case-tree of argument
  -> OccName
  -- ^ Name of the lifted function
  -> Word
  -- ^ Position of the argument
  -> NormalizeSession (Maybe (Id, (Type, CaseTree Term)),Term)
disJointSelProj :: InScopeSet
-> Type
-> CaseTree Term
-> Text
-> Word
-> NormalizeSession (Maybe (Id, (Type, CaseTree Term)), Term)
disJointSelProj InScopeSet
inScope Type
argTy CaseTree Term
cs Text
funName Word
argN = 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
    tupTcm <- Lens.view tupleTcCache
    let sel = TyConMap
-> IntMap TyConName -> Type -> [Type] -> CaseTree [Term] -> Term
genCase TyConMap
tcm IntMap TyConName
tupTcm Type
argTy [Type
argTy] ((Term -> [Term]) -> CaseTree Term -> CaseTree [Term]
forall a b. (a -> b) -> CaseTree a -> CaseTree b
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
fmap (Term -> [Term] -> [Term]
forall a. a -> [a] -> [a]
:[]) CaseTree Term
cs)
    untran <- isUntranslatableType False argTy
    case untran of
      Bool
True -> (Maybe (Id, (Type, CaseTree Term)), Term)
-> NormalizeSession (Maybe (Id, (Type, CaseTree Term)), Term)
forall a. a -> RewriteMonad NormalizeState a
forall (m :: Type -> Type) a. Monad m => a -> m a
return (Maybe (Id, (Type, CaseTree Term))
forall a. Maybe a
Nothing, Term
sel)
      Bool
False -> do
        argId <- InScopeSet -> Text -> Type -> RewriteMonad NormalizeState Id
forall (m :: Type -> Type).
MonadUnique m =>
InScopeSet -> Text -> Type -> m Id
mkInternalVar InScopeSet
inScope (Text
funName Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Text
"_arg" Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Word -> Text
forall a. Show a => a -> Text
showt Word
argN) Type
argTy
        return (Just (argId,(argTy,cs)), Var argId)

-- | Arguments are shared between invocations if:
--
-- * They contain _no_ references to locally-bound variables
-- * Are either:
--     1. All equal
--     2. A proof of an equality: we don't care about the shape of a proof.
--
--        Whether we have `Refl : True ~ True` or `SomeAxiom : (1 <=? 2) ~ True`
--        it doesn't matter, since when we normalize both sides we always end
--        up with a proof of `True ~ True`.
--        Since DEC only fires for applications where all the type arguments
--        are equal, we can deduce that all equality arguments witness the same
--        equality, hence we don't have to care about the shape of the proof.
areShared :: TyConMap -> InScopeSet -> [Either Term Type] -> Bool
areShared :: TyConMap -> InScopeSet -> [Either Term Type] -> Bool
areShared TyConMap
_   InScopeSet
_       []       = Bool
True
areShared TyConMap
tcm InScopeSet
inScope xs :: [Either Term Type]
xs@(Either Term Type
x:[Either Term Type]
_) = Bool
noFV1 Bool -> Bool -> Bool
&& (Either Term Type -> Bool
forall {a} {b}. InferType a => Either a b -> Bool
isProof Either Term Type
x Bool -> Bool -> Bool
|| [Either Term Type] -> Bool
forall a. Eq a => [a] -> Bool
allEqual [Either Term Type]
xs)
 where
  noFV1 :: Bool
noFV1 = case Either Term Type
x of
    Right Type
ty -> All -> Bool
getAll (Getting All Type (Var (ZonkAny 1))
-> (Var (ZonkAny 1) -> All) -> Type -> All
forall r s a. Getting r s a -> (a -> r) -> s -> r
Lens.foldMapOf ((forall b. Var b -> Bool)
-> Word64Set -> Getting All Type (Var (ZonkAny 1))
forall (f :: Type -> Type) a.
(Contravariant f, Applicative f) =>
(forall b. Var b -> Bool)
-> Word64Set -> (Var a -> f (Var a)) -> Type -> f Type
typeFreeVars' Var b -> Bool
forall b. Var b -> Bool
isLocallyBound Word64Set
forall a. Monoid a => a
mempty)
                                       (All -> Var (ZonkAny 1) -> All
forall a b. a -> b -> a
const (Bool -> All
All Bool
False)) Type
ty)
    Left Term
tm  -> All -> Bool
getAll (Getting All Term (Var (ZonkAny 2))
-> (Var (ZonkAny 2) -> All) -> Term -> All
forall r s a. Getting r s a -> (a -> r) -> s -> r
Lens.foldMapOf ((forall b. Var b -> Bool) -> Getting All Term (Var (ZonkAny 2))
forall (f :: Type -> Type) a.
(Contravariant f, Applicative f) =>
(forall b. Var b -> Bool) -> (Var a -> f (Var a)) -> Term -> f Term
termFreeVars' Var b -> Bool
forall b. Var b -> Bool
isLocallyBound)
                                       (All -> Var (ZonkAny 2) -> All
forall a b. a -> b -> a
const (Bool -> All
All Bool
False)) Term
tm)

  isLocallyBound :: Var a -> Bool
isLocallyBound Var a
v = Var a -> Bool
forall b. Var b -> Bool
isLocalId Var a
v Bool -> Bool -> Bool
&& Var a
v Var a -> InScopeSet -> Bool
forall a. Var a -> InScopeSet -> Bool
`notElemInScopeSet` InScopeSet
inScope

  isProof :: Either a b -> Bool
isProof (Left a
co) = case Type -> TypeView
tyView (TyConMap -> a -> Type
forall a. InferType a => TyConMap -> a -> Type
inferCoreTypeOf TyConMap
tcm a
co) of
    TyConApp (TyConName -> Text
forall a. Name a -> Text
nameOcc -> Text
nm) [Type]
_ ->  Text
nm Text -> Text -> Bool
forall a. Eq a => a -> a -> Bool
== Name -> Text
fromTHName ''(~)
    TypeView
_ -> Bool
False
  isProof Either a b
_ = Bool
False

-- | Create a case-expression that selects between the distinct arguments given
-- a case-tree
genCase :: TyConMap
        -> IntMap TyConName
        -> Type -- ^ Type of the alternatives
        -> [Type] -- ^ Types of the arguments
        -> CaseTree [Term] -- ^ CaseTree of arguments
        -> Term
genCase :: TyConMap
-> IntMap TyConName -> Type -> [Type] -> CaseTree [Term] -> Term
genCase TyConMap
tcm IntMap TyConName
tupTcm Type
ty [Type]
argTys = CaseTree [Term] -> Term
go
  where
    go :: CaseTree [Term] -> Term
go (Leaf [Term]
tms) =
      TyConMap -> IntMap TyConName -> [(Type, Term)] -> Term
mkBigTupTm TyConMap
tcm IntMap TyConName
tupTcm ([Type] -> [Term] -> [(Type, Term)]
forall a b. [a] -> [b] -> [(a, b)]
List.zipEqual [Type]
argTys [Term]
tms)

    go (LB [LetBinding]
lb CaseTree [Term]
ct) =
      [LetBinding] -> Term -> Term
Letrec [LetBinding]
lb (CaseTree [Term] -> Term
go CaseTree [Term]
ct)

    go (Branch Term
scrut [(Pat
p,CaseTree [Term]
ct)]) =
      let ct' :: Term
ct' = CaseTree [Term] -> Term
go CaseTree [Term]
ct
          ([TyVar]
ptvs,[Id]
pids) = Pat -> ([TyVar], [Id])
patIds Pat
p
      in  if ([TyVar] -> [Var (ZonkAny 0)]
forall a b. Coercible a b => a -> b
coerce [TyVar]
ptvs [Var (ZonkAny 0)] -> [Var (ZonkAny 0)] -> [Var (ZonkAny 0)]
forall a. [a] -> [a] -> [a]
++ [Id] -> [Var (ZonkAny 0)]
forall a b. Coercible a b => a -> b
coerce [Id]
pids) [Var (ZonkAny 0)] -> Term -> Bool
forall a. [Var a] -> Term -> Bool
`localVarsDoNotOccurIn` Term
ct'
             then Term
ct'
             else Term -> Type -> [Alt] -> Term
Case Term
scrut Type
ty [(Pat
p,Term
ct')]

    go (Branch Term
scrut [(Pat, CaseTree [Term])]
pats) =
      Term -> Type -> [Alt] -> Term
Case Term
scrut Type
ty (((Pat, CaseTree [Term]) -> Alt)
-> [(Pat, CaseTree [Term])] -> [Alt]
forall a b. (a -> b) -> [a] -> [b]
map ((CaseTree [Term] -> Term) -> (Pat, CaseTree [Term]) -> Alt
forall b c a. (b -> c) -> (a, b) -> (a, c)
forall (p :: Type -> Type -> Type) b c a.
Bifunctor p =>
(b -> c) -> p a b -> p a c
second CaseTree [Term] -> Term
go) [(Pat, CaseTree [Term])]
pats)

-- | Lookup the TyConName and DataCon for a tuple of size n
findTup :: TyConMap -> IntMap TyConName -> Int -> (TyConName,DataCon)
findTup :: TyConMap -> IntMap TyConName -> Int -> (TyConName, DataCon)
findTup TyConMap
tcm IntMap TyConName
tupTcm Int
n =
  (TyConName, DataCon)
-> Maybe (TyConName, DataCon) -> (TyConName, DataCon)
forall a. a -> Maybe a -> a
Maybe.fromMaybe ([Char] -> (TyConName, DataCon)
forall a. HasCallStack => [Char] -> a
error ([Char]
"Cannot build " [Char] -> ShowS
forall a. Semigroup a => a -> a -> a
<> Int -> [Char]
forall a. Show a => a -> [Char]
show Int
n [Char] -> ShowS
forall a. Semigroup a => a -> a -> a
<> [Char]
"-tuble")) (Maybe (TyConName, DataCon) -> (TyConName, DataCon))
-> Maybe (TyConName, DataCon) -> (TyConName, DataCon)
forall a b. (a -> b) -> a -> b
$ do
    tupTcNm <- Int -> IntMap TyConName -> Maybe TyConName
forall a. Int -> IntMap a -> Maybe a
IntMap.lookup Int
n IntMap TyConName
tupTcm
    tupTc <- UniqMap.lookup tupTcNm tcm
    tupDc <- Maybe.listToMaybe (tyConDataCons tupTc)
    return (tupTcNm,tupDc)

mkBigTupTm :: TyConMap -> IntMap TyConName -> [(Type,Term)] -> Term
mkBigTupTm :: TyConMap -> IntMap TyConName -> [(Type, Term)] -> Term
mkBigTupTm TyConMap
tcm IntMap TyConName
tupTcm [(Type, Term)]
args = (Type, Term) -> Term
forall a b. (a, b) -> b
snd ((Type, Term) -> Term) -> (Type, Term) -> Term
forall a b. (a -> b) -> a -> b
$ TyConMap -> IntMap TyConName -> [(Type, Term)] -> (Type, Term)
mkBigTup TyConMap
tcm IntMap TyConName
tupTcm [(Type, Term)]
args

mkSmallTup,mkBigTup :: TyConMap -> IntMap TyConName -> [(Type,Term)] -> (Type,Term)
mkSmallTup :: TyConMap -> IntMap TyConName -> [(Type, Term)] -> (Type, Term)
mkSmallTup TyConMap
_ IntMap TyConName
_ [] = [Char] -> (Type, Term)
forall a. HasCallStack => [Char] -> a
error ([Char] -> (Type, Term)) -> [Char] -> (Type, Term)
forall a b. (a -> b) -> a -> b
$ $[Char]
curLoc [Char] -> ShowS
forall a. [a] -> [a] -> [a]
++ [Char]
"mkSmallTup: Can't create 0-tuple"
mkSmallTup TyConMap
_ IntMap TyConName
_ [(Type
ty,Term
tm)] = (Type
ty,Term
tm)
mkSmallTup TyConMap
tcm IntMap TyConName
tupTcm [(Type, Term)]
args = (Type
ty,Term
tm)
  where
    ([Type]
argTys,[Term]
tms) = [(Type, Term)] -> ([Type], [Term])
forall a b. [(a, b)] -> ([a], [b])
unzip [(Type, Term)]
args
    (TyConName
tupTcNm,DataCon
tupDc) = TyConMap -> IntMap TyConName -> Int -> (TyConName, DataCon)
findTup TyConMap
tcm IntMap TyConName
tupTcm ([(Type, Term)] -> Int
forall a. [a] -> Int
forall (t :: Type -> Type) a. Foldable t => t a -> Int
length [(Type, Term)]
args)
    tm :: Term
tm = Term -> [Either Term Type] -> Term
mkApps (DataCon -> Term
Data DataCon
tupDc) ((Type -> Either Term Type) -> [Type] -> [Either Term Type]
forall a b. (a -> b) -> [a] -> [b]
map Type -> Either Term Type
forall a b. b -> Either a b
Right [Type]
argTys [Either Term Type] -> [Either Term Type] -> [Either Term Type]
forall a. [a] -> [a] -> [a]
++ (Term -> Either Term Type) -> [Term] -> [Either Term Type]
forall a b. (a -> b) -> [a] -> [b]
map Term -> Either Term Type
forall a b. a -> Either a b
Left [Term]
tms)
    ty :: Type
ty = TyConName -> [Type] -> Type
mkTyConApp TyConName
tupTcNm [Type]
argTys

mkBigTup :: TyConMap -> IntMap TyConName -> [(Type, Term)] -> (Type, Term)
mkBigTup TyConMap
tcm IntMap TyConName
tupTcm = ([(Type, Term)] -> (Type, Term)) -> [(Type, Term)] -> (Type, Term)
forall a. ([a] -> a) -> [a] -> a
mkChunkified (TyConMap -> IntMap TyConName -> [(Type, Term)] -> (Type, Term)
mkSmallTup TyConMap
tcm IntMap TyConName
tupTcm)

mkSmallTupTy,mkBigTupTy
  :: TyConMap
  -> IntMap TyConName
  -> [Type]
  -> Type
mkSmallTupTy :: TyConMap -> IntMap TyConName -> [Type] -> Type
mkSmallTupTy TyConMap
_ IntMap TyConName
_ [] = [Char] -> Type
forall a. HasCallStack => [Char] -> a
error ([Char] -> Type) -> [Char] -> Type
forall a b. (a -> b) -> a -> b
$ $[Char]
curLoc [Char] -> ShowS
forall a. [a] -> [a] -> [a]
++ [Char]
"mkSmallTupTy: Can't create 0-tuple"
mkSmallTupTy TyConMap
_ IntMap TyConName
_ [Type
ty] = Type
ty
mkSmallTupTy TyConMap
tcm IntMap TyConName
tupTcm [Type]
tys = TyConName -> [Type] -> Type
mkTyConApp TyConName
tupTcNm [Type]
tys
  where
    m :: Int
m = [Type] -> Int
forall a. [a] -> Int
forall (t :: Type -> Type) a. Foldable t => t a -> Int
length [Type]
tys
    (TyConName
tupTcNm,DataCon
_) = TyConMap -> IntMap TyConName -> Int -> (TyConName, DataCon)
findTup TyConMap
tcm IntMap TyConName
tupTcm Int
m

mkBigTupTy :: TyConMap -> IntMap TyConName -> [Type] -> Type
mkBigTupTy TyConMap
tcm IntMap TyConName
tupTcm = ([Type] -> Type) -> [Type] -> Type
forall a. ([a] -> a) -> [a] -> a
mkChunkified (TyConMap -> IntMap TyConName -> [Type] -> Type
mkSmallTupTy TyConMap
tcm IntMap TyConName
tupTcm)

mkSmallTupSelector,mkBigTupSelector
  :: MonadUnique m
  => InScopeSet
  -> TyConMap
  -> IntMap TyConName
  -> Term
  -> [Type]
  -> Int
  -> m Term
mkSmallTupSelector :: forall (m :: Type -> Type).
MonadUnique m =>
InScopeSet
-> TyConMap -> IntMap TyConName -> Term -> [Type] -> Int -> m Term
mkSmallTupSelector InScopeSet
_ TyConMap
_ IntMap TyConName
_ Term
scrut [Type
_] Int
0 = Term -> m Term
forall a. a -> m a
forall (m :: Type -> Type) a. Monad m => a -> m a
return Term
scrut
mkSmallTupSelector InScopeSet
_ TyConMap
_ IntMap TyConName
_ Term
_     [Type
_] Int
n = [Char] -> m Term
forall a. HasCallStack => [Char] -> a
error ([Char] -> m Term) -> [Char] -> m Term
forall a b. (a -> b) -> a -> b
$ $[Char]
curLoc [Char] -> ShowS
forall a. [a] -> [a] -> [a]
++ [Char]
"mkSmallTupSelector called with one type, but to select " [Char] -> ShowS
forall a. [a] -> [a] -> [a]
++ Int -> [Char]
forall a. Show a => a -> [Char]
show Int
n
mkSmallTupSelector InScopeSet
inScope TyConMap
tcm IntMap TyConName
_ Term
scrut [Type]
_ Int
n = [Char] -> InScopeSet -> TyConMap -> Term -> Int -> Int -> m Term
forall (m :: Type -> Type).
(HasCallStack, MonadUnique m) =>
[Char] -> InScopeSet -> TyConMap -> Term -> Int -> Int -> m Term
mkSelectorCase ($[Char]
curLoc [Char] -> ShowS
forall a. [a] -> [a] -> [a]
++ [Char]
"mkSmallTupSelector") InScopeSet
inScope TyConMap
tcm Term
scrut Int
1 Int
n

mkBigTupSelector :: forall (m :: Type -> Type).
MonadUnique m =>
InScopeSet
-> TyConMap -> IntMap TyConName -> Term -> [Type] -> Int -> m Term
mkBigTupSelector InScopeSet
inScope TyConMap
tcm IntMap TyConName
tupTcm Term
scrut [Type]
tys Int
n = [[Type]] -> m Term
forall {m :: Type -> Type}. MonadUnique m => [[Type]] -> m Term
go ([Type] -> [[Type]]
forall {a}. [a] -> [[a]]
chunkify [Type]
tys)
  where
    go :: [[Type]] -> m Term
go [[Type]
_] = InScopeSet
-> TyConMap -> IntMap TyConName -> Term -> [Type] -> Int -> m Term
forall (m :: Type -> Type).
MonadUnique m =>
InScopeSet
-> TyConMap -> IntMap TyConName -> Term -> [Type] -> Int -> m Term
mkSmallTupSelector InScopeSet
inScope TyConMap
tcm IntMap TyConName
tupTcm Term
scrut [Type]
tys Int
n
    go [[Type]]
tyss = do
      let (Int
nOuter,Int
nInner) = Int -> Int -> (Int, Int)
forall a. Integral a => a -> a -> (a, a)
divMod Int
n Int
mAX_TUPLE_SIZE
          tyss' :: [Type]
tyss' = ([Type] -> Type) -> [[Type]] -> [Type]
forall a b. (a -> b) -> [a] -> [b]
map (TyConMap -> IntMap TyConName -> [Type] -> Type
mkSmallTupTy TyConMap
tcm IntMap TyConName
tupTcm) [[Type]]
tyss
      outer <- InScopeSet
-> TyConMap -> IntMap TyConName -> Term -> [Type] -> Int -> m Term
forall (m :: Type -> Type).
MonadUnique m =>
InScopeSet
-> TyConMap -> IntMap TyConName -> Term -> [Type] -> Int -> m Term
mkSmallTupSelector InScopeSet
inScope TyConMap
tcm IntMap TyConName
tupTcm Term
scrut [Type]
tyss' Int
nOuter
      inner <- mkSmallTupSelector inScope tcm tupTcm outer (tyss List.!! nOuter) nInner
      return inner


-- | Determine if a term in a function position is interesting to lift out of
-- of a case-expression.
--
-- This holds for all global functions, and certain primitives. Currently those
-- primitives are:
--
-- * All non-cheap multiplications
-- * All division-like operations with a non-cheap divisor
--
-- Multiplying/dividing by zero or powers of two are considered cheap and
-- isn't lifted out.
interestingToLift
  :: InScopeSet
  -- ^ in scope
  -> (Term -> Term)
  -- ^ Evaluator
  -> Term
  -- ^ Term in function position
  -> [Either Term Type]
  -- ^ Arguments
  -> [TickInfo]
  -- ^ Tick annoations
  -> Maybe Term
interestingToLift :: InScopeSet
-> (Term -> Term)
-> Term
-> [Either Term Type]
-> [TickInfo]
-> Maybe Term
interestingToLift InScopeSet
inScope Term -> Term
_ e :: Term
e@(Var Id
v) [Either Term Type]
_ [TickInfo]
ticks =
  if TickInfo
NoDeDup TickInfo -> [TickInfo] -> Bool
forall (t :: Type -> Type) a.
(Foldable t, Eq a) =>
a -> t a -> Bool
`notElem` [TickInfo]
ticks Bool -> Bool -> Bool
&& (Id -> Bool
forall b. Var b -> Bool
isGlobalId Id
v Bool -> Bool -> Bool
||  Id
v Id -> InScopeSet -> Bool
forall a. Var a -> InScopeSet -> Bool
`elemInScopeSet` InScopeSet
inScope)
     then (Term -> Maybe Term
forall a. a -> Maybe a
Just Term
e)
     else Maybe Term
forall a. Maybe a
Nothing
interestingToLift InScopeSet
inScope Term -> Term
eval e :: Term
e@(Prim PrimInfo
pInfo) [Either Term Type]
args [TickInfo]
ticks
  | TickInfo
NoDeDup TickInfo -> [TickInfo] -> Bool
forall (t :: Type -> Type) a.
(Foldable t, Eq a) =>
a -> t a -> Bool
`notElem` [TickInfo]
ticks = do
  let anyArgNotConstant :: Bool
anyArgNotConstant = (Term -> Bool) -> [Term] -> Bool
forall (t :: Type -> Type) a.
Foldable t =>
(a -> Bool) -> t a -> Bool
any (Bool -> Bool
not (Bool -> Bool) -> (Term -> Bool) -> Term -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Term -> Bool
isConstant) [Term]
lArgs
  case Text -> [(Text, Bool)] -> Maybe Bool
forall a b. Eq a => a -> [(a, b)] -> Maybe b
List.lookup (PrimInfo -> Text
primName PrimInfo
pInfo) [(Text, Bool)]
interestingPrims of
    Just Bool
t | Bool
t Bool -> Bool -> Bool
|| Bool
anyArgNotConstant -> (Term -> Maybe Term
forall a. a -> Maybe a
Just Term
e)
    Maybe Bool
_ | TickInfo
DeDup TickInfo -> [TickInfo] -> Bool
forall a. Eq a => a -> [a] -> Bool
forall (t :: Type -> Type) a.
(Foldable t, Eq a) =>
a -> t a -> Bool
`elem` [TickInfo]
ticks -> (Term -> Maybe Term
forall a. a -> Maybe a
Just Term
e)
    Maybe Bool
_ ->
      if Type -> Bool
isHOTy (PrimInfo -> Type
forall a. HasType a => a -> Type
coreTypeOf PrimInfo
pInfo) then do
        let anyInteresting :: Bool
anyInteresting = (Term -> Bool) -> [Term] -> Bool
forall (t :: Type -> Type) a.
Foldable t =>
(a -> Bool) -> t a -> Bool
List.any (Maybe Term -> Bool
forall a. Maybe a -> Bool
Maybe.isJust (Maybe Term -> Bool) -> (Term -> Maybe Term) -> Term -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Term -> Maybe Term
isInteresting) [Term]
lArgs
        if Bool
anyInteresting then Term -> Maybe Term
forall a. a -> Maybe a
Just Term
e else Maybe Term
forall a. Maybe a
Nothing
      else
        Maybe Term
forall a. Maybe a
Nothing

  where
    isInteresting :: Term -> Maybe Term
isInteresting = (\(Term
x, [Either Term Type]
y, [TickInfo]
z) -> InScopeSet
-> (Term -> Term)
-> Term
-> [Either Term Type]
-> [TickInfo]
-> Maybe Term
interestingToLift InScopeSet
inScope Term -> Term
eval Term
x [Either Term Type]
y [TickInfo]
z) ((Term, [Either Term Type], [TickInfo]) -> Maybe Term)
-> (Term -> (Term, [Either Term Type], [TickInfo]))
-> Term
-> Maybe Term
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Term -> (Term, [Either Term Type], [TickInfo])
collectArgsTicks
    interestingPrims :: [(Text, Bool)]
interestingPrims = ((Name, Bool) -> (Text, Bool)) -> [(Name, Bool)] -> [(Text, Bool)]
forall a b. (a -> b) -> [a] -> [b]
map ((Name -> Text) -> (Name, Bool) -> (Text, Bool)
forall a b c. (a -> b) -> (a, c) -> (b, c)
forall (p :: Type -> Type -> Type) a b c.
Bifunctor p =>
(a -> b) -> p a c -> p b c
first Name -> Text
fromTHName)
      [('(Clash.Sized.Internal.BitVector.*#),Bool
bothNotPow2)
      ,('Clash.Sized.Internal.BitVector.times#,Bool
bothNotPow2)
      ,('Clash.Sized.Internal.BitVector.quot#,Bool
lastNotPow2)
      ,('Clash.Sized.Internal.BitVector.rem#,Bool
lastNotPow2)
      ,('(Clash.Sized.Internal.Index.*#),Bool
bothNotPow2)
      ,('Clash.Sized.Internal.Index.times#,Bool
bothNotPow2)
      ,('Clash.Sized.Internal.Index.quot#,Bool
lastNotPow2)
      ,('Clash.Sized.Internal.Index.rem#,Bool
lastNotPow2)
      ,('(Clash.Sized.Internal.Signed.*#),Bool
bothNotPow2)
      ,('Clash.Sized.Internal.Signed.times#,Bool
bothNotPow2)
      ,('Clash.Sized.Internal.Signed.rem#,Bool
lastNotPow2)
      ,('Clash.Sized.Internal.Signed.quot#,Bool
lastNotPow2)
      ,('Clash.Sized.Internal.Signed.div#,Bool
lastNotPow2)
      ,('Clash.Sized.Internal.Signed.mod#,Bool
lastNotPow2)
      ,('(Clash.Sized.Internal.Unsigned.*#),Bool
bothNotPow2)
      ,('Clash.Sized.Internal.Unsigned.times#,Bool
bothNotPow2)
      ,('Clash.Sized.Internal.Unsigned.quot#,Bool
lastNotPow2)
      ,('Clash.Sized.Internal.Unsigned.rem#,Bool
lastNotPow2)
      ,('GHC.Base.quotInt,Bool
lastNotPow2)
      ,('GHC.Base.remInt,Bool
lastNotPow2)
      ,('GHC.Base.divInt,Bool
lastNotPow2)
      ,('GHC.Base.modInt,Bool
lastNotPow2)
      ,('GHC.Classes.divInt#,Bool
lastNotPow2)
      ,('GHC.Classes.modInt#,Bool
lastNotPow2)
#if MIN_VERSION_base(4,15,0)
      ,('GHC.Num.Integer.integerMul,Bool
bothNotPow2)
      ,('GHC.Num.Integer.integerDiv,Bool
lastNotPow2)
      ,('GHC.Num.Integer.integerMod,Bool
lastNotPow2)
      ,('GHC.Num.Integer.integerQuot,Bool
lastNotPow2)
      ,('GHC.Num.Integer.integerRem,Bool
lastNotPow2)
#else
      ,('GHC.Integer.Type.timesInteger,bothNotPow2)
      ,('GHC.Integer.Type.divInteger,lastNotPow2)
      ,('GHC.Integer.Type.modInteger,lastNotPow2)
      ,('GHC.Integer.Type.quotInteger,lastNotPow2)
      ,('GHC.Integer.Type.remInteger,lastNotPow2)
#endif
      ,('(GHC.Prim.*#),Bool
bothNotPow2)
      ,('GHC.Prim.quotInt#,Bool
lastNotPow2)
      ,('GHC.Prim.remInt#,Bool
lastNotPow2)
      ]

    lArgs :: [Term]
lArgs       = [Either Term Type] -> [Term]
forall a b. [Either a b] -> [a]
Either.lefts [Either Term Type]
args

    lastNotPow2 :: Bool
lastNotPow2 = case [Term]
lArgs of
                    [] -> Bool
True
                    [Term]
_  -> Bool -> Bool
not (Term -> Bool
termIsPow2 ([Term] -> Term
forall a. HasCallStack => [a] -> a
last [Term]
lArgs))
    -- | This only looks at the last two arguments, skipping over any constraints if they exist
    bothNotPow2 :: Bool
bothNotPow2 = [Term] -> Bool
go [Term]
lArgs
     where
      go :: [Term] -> Bool
go [Term]
xs = case [Term]
xs of
                [] -> Bool
True
                [Term
a] -> Bool -> Bool
not (Term -> Bool
termIsPow2 Term
a)
                [Term
a,Term
b] -> Bool -> Bool
not (Term -> Bool
termIsPow2 Term
a) Bool -> Bool -> Bool
&& Bool -> Bool
not (Term -> Bool
termIsPow2 Term
b)
                (Term
_:[Term]
rest) -> [Term] -> Bool
go [Term]
rest

    termIsPow2 :: Term -> Bool
termIsPow2 Term
e' = case Term -> Term
eval Term
e' of
      Literal (IntegerLiteral Integer
n) -> Integer -> Bool
forall {a}. (Bits a, Num a) => a -> Bool
isPow2 Integer
n
      Term
a -> case Term -> (Term, [Either Term Type])
collectArgs Term
a of
        (Prim PrimInfo
p,[Right Type
_,Left Term
_,       Left (Literal (IntegerLiteral Integer
n))])
          | Text -> Bool
isFromInt (PrimInfo -> Text
primName PrimInfo
p) -> Integer -> Bool
forall {a}. (Bits a, Num a) => a -> Bool
isPow2 Integer
n
        (Prim PrimInfo
p,[Right Type
_,Left Term
_,Left Term
_,Left (Literal (IntegerLiteral Integer
n))])
          | PrimInfo -> Text
primName PrimInfo
p Text -> Text -> Bool
forall a. Eq a => a -> a -> Bool
== Name -> Text
fromTHName 'Clash.Sized.Internal.BitVector.fromInteger#  -> Integer -> Bool
forall {a}. (Bits a, Num a) => a -> Bool
isPow2 Integer
n
        (Term, [Either Term Type])
_ -> Bool
False

    -- This used to contain (x /= 0), but multiplying by zero is free
    isPow2 :: a -> Bool
isPow2 a
x = (a
x a -> a -> a
forall a. Bits a => a -> a -> a
.&. (a -> a
forall a. Bits a => a -> a
complement a
x a -> a -> a
forall a. Num a => a -> a -> a
+ a
1)) a -> a -> Bool
forall a. Eq a => a -> a -> Bool
== a
x

    isHOTy :: Type -> Bool
isHOTy Type
t = case Type -> ([Either TyVar Type], Type)
splitFunForallTy Type
t of
      ([Either TyVar Type]
args',Type
_) -> (Type -> Bool) -> [Type] -> Bool
forall (t :: Type -> Type) a.
Foldable t =>
(a -> Bool) -> t a -> Bool
any Type -> Bool
isPolyFunTy ([Either TyVar Type] -> [Type]
forall a b. [Either a b] -> [b]
Either.rights [Either TyVar Type]
args')

interestingToLift InScopeSet
_ Term -> Term
_ Term
_ [Either Term Type]
_ [TickInfo]
_ = Maybe Term
forall a. Maybe a
Nothing

fromTHName :: TH.Name -> Text.Text
fromTHName :: Name -> Text
fromTHName = [Char] -> Text
Text.pack ([Char] -> Text) -> (Name -> [Char]) -> Name -> Text
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Name -> [Char]
forall a. Show a => a -> [Char]
show