{-|
  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

import Control.Concurrent.Supply (splitSupply)
#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.IntSet as IntSet
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)
#else
import GHC.Hs.Utils (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)

-- 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 :: 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.
    (Term
_,InScopeSet
isCollected,[(Term, ([Term], CaseTree [Either Term Type]))]
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]))]
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 [(Term, ([Term], CaseTree [Either Term Type]))] -> Bool
forall (t :: Type -> Type) a. Foldable t => t a -> Bool
null [(Term, ([Term], CaseTree [Either Term Type]))]
disJoint
       then Term -> RewriteMonad NormalizeState Term
forall (m :: Type -> Type) a. Monad m => a -> m a
return Term
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.
         [(Term, [Term])]
lifted <- ((Term, ([Term], CaseTree [Either Term Type]))
 -> RewriteMonad NormalizeState (Term, [Term]))
-> [(Term, ([Term], CaseTree [Either Term Type]))]
-> RewriteMonad NormalizeState [(Term, [Term])]
forall (t :: Type -> Type) (m :: Type -> Type) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM (InScopeSet
-> (Term, ([Term], CaseTree [Either Term Type]))
-> RewriteMonad NormalizeState (Term, [Term])
mkDisjointGroup InScopeSet
isCtx) [(Term, ([Term], CaseTree [Either Term Type]))]
disJoint
         TyConMap
tcm    <- Getting TyConMap RewriteEnv TyConMap
-> RewriteMonad NormalizeState TyConMap
forall s (m :: Type -> Type) a.
MonadReader s m =>
Getting a s a -> m a
Lens.view Getting TyConMap RewriteEnv TyConMap
Getter RewriteEnv TyConMap
tcCache
         -- 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.
         (InScopeSet
_,[Id]
funOutIds) <- (InScopeSet
 -> ((Term, ([Term], CaseTree [Either Term Type])), (Term, [Term]))
 -> RewriteMonad NormalizeState (InScopeSet, Id))
-> InScopeSet
-> [((Term, ([Term], CaseTree [Either Term Type])),
     (Term, [Term]))]
-> RewriteMonad NormalizeState (InScopeSet, [Id])
forall (m :: Type -> Type) acc x y.
Monad m =>
(acc -> x -> m (acc, y)) -> acc -> [x] -> m (acc, [y])
List.mapAccumLM (TyConMap
-> InScopeSet
-> ((Term, ([Term], CaseTree [Either Term Type])), (Term, [Term]))
-> RewriteMonad NormalizeState (InScopeSet, Id)
forall (m :: Type -> Type) a b b.
(MonadUnique m, InferType a) =>
TyConMap -> InScopeSet -> ((Term, b), (a, b)) -> m (InScopeSet, Id)
mkFunOut TyConMap
tcm)
                                          InScopeSet
isCollected
                                          ([(Term, ([Term], CaseTree [Either Term Type]))]
-> [(Term, [Term])]
-> [((Term, ([Term], CaseTree [Either Term Type])),
     (Term, [Term]))]
forall a b. [a] -> [b] -> [(a, b)]
zip [(Term, ([Term], CaseTree [Either Term Type]))]
disJoint [(Term, [Term])]
lifted)
         -- Create "substitutions" of the form [f X Y := f_out]
         let substitution :: [(Term, Term)]
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
isCtx1 = InScopeSet -> [Id] -> InScopeSet
forall a. InScopeSet -> [Var a] -> InScopeSet
extendInScopeSetList InScopeSet
isCtx [Id]
funOutIds
         [Term]
lifted1 <- InScopeSet
-> [(Term, Term)]
-> [(Term, [Term])]
-> RewriteMonad NormalizeState [Term]
substLifted InScopeSet
isCtx1 [(Term, Term)]
substitution [(Term, [Term])]
lifted
         -- Do the same for the actual case expression
         (Term
e1,InScopeSet
_,[(Term, ([Term], CaseTree [Either Term Type]))]
_) <- InScopeSet
-> [(Term, Term)]
-> [Term]
-> Term
-> NormalizeSession
     (Term, InScopeSet, [(Term, ([Term], CaseTree [Either Term Type]))])
collectGlobals InScopeSet
isCtx1 [(Term, Term)]
substitution [] Term
e
         -- Let-bind all the lifted function
         let lb :: Term
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.
         Term
lb1 <- NormRewrite -> NormRewrite
forall (m :: Type -> Type). Monad m => Transform m -> Transform m
bottomupR HasCallStack => NormRewrite
NormRewrite
deadCode TransformContext
ctx Term
lb
         Term -> RewriteMonad NormalizeState Term
forall a extra. a -> RewriteMonad extra a
changed Term
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 :: OccName
nm  = Term -> OccName
decFunName Term
fun
          nm1 :: OccName
nm1 = OccName
nm OccName -> OccName -> OccName
`Text.append` OccName
"_out"
      Id
nm2 <- InScopeSet -> OccName -> Type -> m Id
forall (m :: Type -> Type).
MonadUnique m =>
InScopeSet -> OccName -> Type -> m Id
mkInternalVar InScopeSet
isN OccName
nm1 Type
ty
      (InScopeSet, Id) -> m (InScopeSet, Id)
forall (m :: Type -> Type) a. Monad m => a -> m a
return (InScopeSet -> Id -> InScopeSet
forall a. InScopeSet -> Var a -> InScopeSet
extendInScopeSet InScopeSet
isN Id
nm2,Id
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
      [(Term, InScopeSet,
  [(Term, ([Term], CaseTree [Either Term Type]))])]
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
      [Term] -> RewriteMonad NormalizeState [Term]
forall (m :: Type -> Type) a. Monad m => a -> m a
return (((Term, InScopeSet,
  [(Term, ([Term], CaseTree [Either Term Type]))])
 -> Term)
-> [(Term, InScopeSet,
     [(Term, ([Term], CaseTree [Either Term Type]))])]
-> [Term]
forall a b. (a -> b) -> [a] -> [b]
map ((Term, InScopeSet, [(Term, ([Term], CaseTree [Either Term Type]))])
-> Getting
     Term
     (Term, InScopeSet, [(Term, ([Term], CaseTree [Either Term Type]))])
     Term
-> Term
forall s a. s -> Getting a s a -> a
^. Getting
  Term
  (Term, InScopeSet, [(Term, ([Term], CaseTree [Either Term Type]))])
  Term
forall s t a b. Field1 s t a b => Lens s t a b
_1) [(Term, InScopeSet,
  [(Term, ([Term], CaseTree [Either Term Type]))])]
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 (m :: Type -> Type) a. Monad m => a -> m a
return Term
e
{-# SCC disjointExpressionConsolidation #-}

decFunName :: Term -> OccName
decFunName :: Term -> OccName
decFunName Term
fun = [OccName] -> OccName
forall a. [a] -> a
last ([OccName] -> OccName)
-> (OccName -> [OccName]) -> OccName -> OccName
forall b c a. (b -> c) -> (a -> b) -> a -> c
. OccName -> OccName -> [OccName]
Text.splitOn OccName
"." (OccName -> OccName) -> OccName -> OccName
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 -> OccName
forall a. Name a -> OccName
nameOcc (Id -> Name Term
forall a. Var a -> Name a
varName Id
v)
  (Prim PrimInfo
p, [Either Term Type]
_) -> PrimInfo -> OccName
primName PrimInfo
p
  (Term, [Either Term Type])
_ -> OccName
"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
/= :: CaseTree a -> CaseTree a -> Bool
$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
Eq,Int -> CaseTree a -> ShowS
[CaseTree a] -> ShowS
CaseTree a -> String
(Int -> CaseTree a -> ShowS)
-> (CaseTree a -> String)
-> ([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 -> String
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [CaseTree a] -> ShowS
$cshowList :: forall a. Show a => [CaseTree a] -> ShowS
show :: CaseTree a -> String
$cshow :: forall a. Show a => CaseTree a -> String
showsPrec :: Int -> CaseTree a -> ShowS
$cshowsPrec :: forall a. Show a => Int -> CaseTree a -> ShowS
Show,a -> CaseTree b -> CaseTree a
(a -> b) -> CaseTree a -> CaseTree b
(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
<$ :: a -> CaseTree b -> CaseTree a
$c<$ :: forall a b. a -> CaseTree b -> CaseTree a
fmap :: (a -> b) -> CaseTree a -> CaseTree b
$cfmap :: forall a b. (a -> b) -> CaseTree a -> CaseTree b
Functor,CaseTree a -> Bool
(a -> m) -> CaseTree a -> m
(a -> b -> b) -> b -> CaseTree a -> b
(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
product :: CaseTree a -> a
$cproduct :: forall a. Num a => CaseTree a -> a
sum :: CaseTree a -> a
$csum :: forall a. Num a => CaseTree a -> a
minimum :: CaseTree a -> a
$cminimum :: forall a. Ord a => CaseTree a -> a
maximum :: CaseTree a -> a
$cmaximum :: forall a. Ord a => CaseTree a -> a
elem :: a -> CaseTree a -> Bool
$celem :: forall a. Eq a => a -> CaseTree a -> Bool
length :: CaseTree a -> Int
$clength :: forall a. CaseTree a -> Int
null :: CaseTree a -> Bool
$cnull :: forall a. CaseTree a -> Bool
toList :: CaseTree a -> [a]
$ctoList :: forall a. CaseTree a -> [a]
foldl1 :: (a -> a -> a) -> CaseTree a -> a
$cfoldl1 :: forall a. (a -> a -> a) -> CaseTree a -> a
foldr1 :: (a -> a -> a) -> CaseTree a -> a
$cfoldr1 :: forall a. (a -> a -> a) -> CaseTree a -> a
foldl' :: (b -> a -> b) -> b -> CaseTree a -> b
$cfoldl' :: forall b a. (b -> a -> b) -> b -> CaseTree a -> b
foldl :: (b -> a -> b) -> b -> CaseTree a -> b
$cfoldl :: forall b a. (b -> a -> b) -> b -> CaseTree a -> b
foldr' :: (a -> b -> b) -> b -> CaseTree a -> b
$cfoldr' :: forall a b. (a -> b -> b) -> b -> CaseTree a -> b
foldr :: (a -> b -> b) -> b -> CaseTree a -> b
$cfoldr :: forall a b. (a -> b -> b) -> b -> CaseTree a -> b
foldMap' :: (a -> m) -> CaseTree a -> m
$cfoldMap' :: forall m a. Monoid m => (a -> m) -> CaseTree a -> m
foldMap :: (a -> m) -> CaseTree a -> m
$cfoldMap :: forall m a. Monoid m => (a -> m) -> CaseTree a -> m
fold :: CaseTree m -> m
$cfold :: forall m. Monoid m => CaseTree m -> m
Foldable)

instance Applicative CaseTree where
  pure :: a -> CaseTree a
pure = a -> CaseTree a
forall a. a -> CaseTree a
Leaf
  liftA2 :: (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 (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 (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
_ = String -> CaseTree c
forall a. HasCallStack => String -> a
error String
"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 (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 :: [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 ([Alt]
alts1, InScopeSet
isAlts, [(Term, ([Term], CaseTree [Either Term Type]))]
collectedAlts) <-
        InScopeSet
-> [(Term, Term)]
-> [Term]
-> Term
-> [Alt]
-> NormalizeSession
     ([Alt], InScopeSet,
      [(Term, ([Term], CaseTree [Either Term Type]))])
collectGlobalsAlts InScopeSet
is0 [(Term, Term)]
substitution [Term]
seen Term
scrut1 [Alt]
alts
      (Term
scrut1, InScopeSet
isScrut, [(Term, ([Term], CaseTree [Either Term Type]))]
collectedScrut) <-
        InScopeSet
-> [(Term, Term)]
-> [Term]
-> Term
-> NormalizeSession
     (Term, InScopeSet, [(Term, ([Term], CaseTree [Either Term Type]))])
collectGlobals InScopeSet
is0 [(Term, Term)]
substitution (((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]))]
collectedAlts [Term] -> [Term] -> [Term]
forall a. [a] -> [a] -> [a]
++ [Term]
seen) Term
scrut
  (Term, InScopeSet, [(Term, ([Term], CaseTree [Either Term Type]))])
-> NormalizeSession
     (Term, InScopeSet, [(Term, ([Term], CaseTree [Either Term Type]))])
forall (m :: Type -> Type) a. Monad m => a -> m a
return ( Term -> Type -> [Alt] -> Term
Case Term
scrut1 Type
ty [Alt]
alts1
         , InScopeSet -> InScopeSet -> InScopeSet
unionInScope InScopeSet
isAlts InScopeSet
isScrut
         , [(Term, ([Term], CaseTree [Either Term Type]))]
collectedAlts [(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]))]
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
    TyConMap
tcm <- Getting TyConMap RewriteEnv TyConMap
-> RewriteMonad NormalizeState TyConMap
forall s (m :: Type -> Type) a.
MonadReader s m =>
Getting a s a -> m a
Lens.view Getting TyConMap RewriteEnv TyConMap
Getter RewriteEnv TyConMap
tcCache
    BindingMap
bndrs <- Getting BindingMap (RewriteState NormalizeState) BindingMap
-> RewriteMonad NormalizeState BindingMap
forall s (m :: Type -> Type) a.
MonadState s m =>
Getting a s a -> m a
Lens.use Getting BindingMap (RewriteState NormalizeState) BindingMap
forall extra. Lens' (RewriteState extra) BindingMap
bindings
    Evaluator
evaluate <- Getting Evaluator RewriteEnv Evaluator
-> RewriteMonad NormalizeState Evaluator
forall s (m :: Type -> Type) a.
MonadReader s m =>
Getting a s a -> m a
Lens.view Getting Evaluator RewriteEnv Evaluator
Lens' RewriteEnv Evaluator
evaluator
    Supply
ids <- Getting Supply (RewriteState NormalizeState) Supply
-> RewriteMonad NormalizeState Supply
forall s (m :: Type -> Type) a.
MonadState s m =>
Getting a s a -> m a
Lens.use Getting Supply (RewriteState NormalizeState) Supply
forall extra. Lens' (RewriteState extra) Supply
uniqSupply
    let (Supply
ids1,Supply
ids2) = Supply -> (Supply, Supply)
splitSupply Supply
ids
    (Supply -> Identity Supply)
-> RewriteState NormalizeState
-> Identity (RewriteState NormalizeState)
forall extra. Lens' (RewriteState extra) Supply
uniqSupply ((Supply -> Identity Supply)
 -> RewriteState NormalizeState
 -> Identity (RewriteState NormalizeState))
-> Supply -> RewriteMonad NormalizeState ()
forall s (m :: Type -> Type) a b.
MonadState s m =>
ASetter s s a b -> b -> m ()
Lens..= Supply
ids2
    PrimHeap
gh <- Getting PrimHeap (RewriteState NormalizeState) PrimHeap
-> RewriteMonad NormalizeState PrimHeap
forall s (m :: Type -> Type) a.
MonadState s m =>
Getting a s a -> m a
Lens.use Getting PrimHeap (RewriteState NormalizeState) PrimHeap
forall extra. Lens' (RewriteState extra) PrimHeap
globalHeap
    let eval :: Term -> Term
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._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 :: Type
eTy  = TyConMap -> Term -> Type
forall a. InferType a => TyConMap -> a -> Type
inferCoreTypeOf TyConMap
tcm Term
e
    Bool
untran <- Bool -> Type -> RewriteMonad NormalizeState Bool
forall extra. Bool -> Type -> RewriteMonad extra Bool
isUntranslatableType Bool
False Type
eTy
    case Bool
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
        ([Either Term Type]
args1,InScopeSet
isArgs,[(Term, ([Term], CaseTree [Either Term Type]))]
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]
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 :: Maybe Term
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 Maybe Term
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 (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 (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 (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)
  (Term
body1,InScopeSet
isBody,[(Term, ([Term], CaseTree [Either Term Type]))]
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
  ([LetBinding]
lbs1,InScopeSet
isBndrs,[(Term, ([Term], CaseTree [Either Term Type]))]
collectedBndrs) <-
    InScopeSet
-> [(Term, Term)]
-> [Term]
-> [LetBinding]
-> NormalizeSession
     ([LetBinding], InScopeSet,
      [(Term, ([Term], CaseTree [Either Term Type]))])
collectGlobalsLbs InScopeSet
is1 [(Term, Term)]
substitution (((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]))]
collectedBody [Term] -> [Term] -> [Term]
forall a. [a] -> [a] -> [a]
++ [Term]
seen) [LetBinding]
lbs
  (Term, InScopeSet, [(Term, ([Term], CaseTree [Either Term Type]))])
-> NormalizeSession
     (Term, InScopeSet, [(Term, ([Term], CaseTree [Either Term Type]))])
forall (m :: Type -> Type) a. Monad m => a -> m a
return ( [LetBinding] -> Term -> Term
Letrec [LetBinding]
lbs1 Term
body1
         , InScopeSet -> InScopeSet -> InScopeSet
unionInScope InScopeSet
isBody InScopeSet
isBndrs
         , ((Term, ([Term], CaseTree [Either Term Type]))
 -> (Term, ([Term], CaseTree [Either Term Type])))
-> [(Term, ([Term], CaseTree [Either Term Type]))]
-> [(Term, ([Term], CaseTree [Either Term Type]))]
forall a b. (a -> b) -> [a] -> [b]
map ((([Term], CaseTree [Either Term Type])
 -> ([Term], CaseTree [Either Term Type]))
-> (Term, ([Term], CaseTree [Either Term Type]))
-> (Term, ([Term], CaseTree [Either Term Type]))
forall (p :: Type -> Type -> Type) b c a.
Bifunctor p =>
(b -> c) -> p a b -> p a c
second ((CaseTree [Either Term Type] -> CaseTree [Either Term Type])
-> ([Term], CaseTree [Either Term Type])
-> ([Term], CaseTree [Either Term Type])
forall (p :: Type -> Type -> Type) b c a.
Bifunctor p =>
(b -> c) -> p a b -> p a c
second ([LetBinding]
-> CaseTree [Either Term Type] -> CaseTree [Either Term Type]
forall a. [LetBinding] -> CaseTree a -> CaseTree a
LB [LetBinding]
lbs1))) ([(Term, ([Term], CaseTree [Either Term Type]))]
collectedBody [(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]))]
collectedBndrs)
         )

collectGlobals InScopeSet
is0 [(Term, Term)]
substitution [Term]
seen (Tick TickInfo
t Term
e) = do
  (Term
e1,InScopeSet
is1,[(Term, ([Term], CaseTree [Either Term Type]))]
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
  (Term, InScopeSet, [(Term, ([Term], CaseTree [Either Term Type]))])
-> NormalizeSession
     (Term, InScopeSet, [(Term, ([Term], CaseTree [Either Term Type]))])
forall (m :: Type -> Type) a. Monad m => a -> m a
return (TickInfo -> Term -> Term
Tick TickInfo
t Term
e1, InScopeSet
is1, [(Term, ([Term], CaseTree [Either Term Type]))]
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 (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
    ((InScopeSet
is1,[Term]
_),([Either Term Type]
args',[[(Term, ([Term], CaseTree [Either Term Type]))]]
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 (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
    ([Either Term Type], InScopeSet,
 [(Term, ([Term], CaseTree [Either Term Type]))])
-> NormalizeSession
     ([Either Term Type], InScopeSet,
      [(Term, ([Term], CaseTree [Either Term Type]))])
forall (m :: Type -> Type) a. Monad m => a -> m a
return ([Either Term Type]
args',InScopeSet
is1,[[(Term, ([Term], CaseTree [Either Term Type]))]]
-> [(Term, ([Term], CaseTree [Either Term Type]))]
forall (t :: Type -> Type) a. Foldable t => t [a] -> [a]
concat [[(Term, ([Term], CaseTree [Either Term Type]))]]
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
      (Term
tm',InScopeSet
isN1,[(Term, ([Term], CaseTree [Either Term Type]))]
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
      ((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 (m :: Type -> Type) a. Monad m => a -> m a
return ((InScopeSet
isN1,((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]))]
collected [Term] -> [Term] -> [Term]
forall a. [a] -> [a] -> [a]
++ [Term]
s),(Term -> Either Term b
forall a b. a -> Either a b
Left Term
tm',[(Term, ([Term], CaseTree [Either Term Type]))]
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 (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
    (InScopeSet
is1,([Alt]
alts',[[(Term, ([Term], (Pat, CaseTree [Either Term Type])))]]
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 (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 :: [Map Term ([Term], [(Pat, CaseTree [Either Term Type])])]
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 (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 (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 :: Map Term ([Term], [(Pat, CaseTree [Either Term Type])])
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], CaseTree [Either Term Type]))]
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 (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 (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)
    ([Alt], InScopeSet,
 [(Term, ([Term], CaseTree [Either Term Type]))])
-> NormalizeSession
     ([Alt], InScopeSet,
      [(Term, ([Term], CaseTree [Either Term Type]))])
forall (m :: Type -> Type) a. Monad m => a -> m a
return ([Alt]
alts',InScopeSet
is1,[(Term, ([Term], CaseTree [Either Term Type]))]
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))
      (Term
e',InScopeSet
isN2,[(Term, ([Term], CaseTree [Either Term Type]))]
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
      (InScopeSet,
 (Alt, [(Term, ([Term], (Pat, CaseTree [Either Term Type])))]))
-> RewriteMonad
     NormalizeState
     (InScopeSet,
      (Alt, [(Term, ([Term], (Pat, CaseTree [Either Term Type])))]))
forall (m :: Type -> Type) a. Monad m => a -> m a
return (InScopeSet
isN2,((Pat
p,Term
e'),((Term, ([Term], CaseTree [Either Term Type]))
 -> (Term, ([Term], (Pat, CaseTree [Either Term Type]))))
-> [(Term, ([Term], CaseTree [Either Term Type]))]
-> [(Term, ([Term], (Pat, CaseTree [Either Term Type])))]
forall a b. (a -> b) -> [a] -> [b]
map ((([Term], CaseTree [Either Term Type])
 -> ([Term], (Pat, CaseTree [Either Term Type])))
-> (Term, ([Term], CaseTree [Either Term Type]))
-> (Term, ([Term], (Pat, CaseTree [Either Term Type])))
forall (p :: Type -> Type -> Type) b c a.
Bifunctor p =>
(b -> c) -> p a b -> p a c
second ((CaseTree [Either Term Type] -> (Pat, CaseTree [Either Term Type]))
-> ([Term], CaseTree [Either Term Type])
-> ([Term], (Pat, CaseTree [Either Term Type]))
forall (p :: Type -> Type -> Type) b c a.
Bifunctor p =>
(b -> c) -> p a b -> p a c
second (Pat
p,))) [(Term, ([Term], CaseTree [Either Term Type]))]
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
    ((InScopeSet
is1,[Term]
_),([SCC LetBinding]
lbsSCCs1,[[(Term, ([Term], CaseTree [Either Term Type]))]]
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 (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
    ([LetBinding], InScopeSet,
 [(Term, ([Term], CaseTree [Either Term Type]))])
-> NormalizeSession
     ([LetBinding], InScopeSet,
      [(Term, ([Term], CaseTree [Either Term Type]))])
forall (m :: Type -> Type) a. Monad m => a -> m a
return ([SCC LetBinding] -> [LetBinding]
forall a. [SCC a] -> [a]
Graph.flattenSCCs [SCC LetBinding]
lbsSCCs1,InScopeSet
is1,[[(Term, ([Term], CaseTree [Either Term Type]))]]
-> [(Term, ([Term], CaseTree [Either Term Type]))]
forall (t :: Type -> Type) a. Foldable t => t [a] -> [a]
concat [[(Term, ([Term], CaseTree [Either Term Type]))]]
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
      (Term
e',InScopeSet
isN1,[(Term, ([Term], CaseTree [Either Term Type]))]
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
      ((InScopeSet, [Term]),
 (SCC LetBinding, [(Term, ([Term], CaseTree [Either Term Type]))]))
-> RewriteMonad
     NormalizeState
     ((InScopeSet, [Term]),
      (SCC LetBinding, [(Term, ([Term], CaseTree [Either Term Type]))]))
forall (m :: Type -> Type) a. Monad m => a -> m a
return ((InScopeSet
isN1,((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]))]
collected [Term] -> [Term] -> [Term]
forall a. [a] -> [a] -> [a]
++ [Term]
s),(LetBinding -> SCC LetBinding
forall vertex. vertex -> SCC vertex
Graph.AcyclicSCC (Id
id_,Term
e'),[(Term, ([Term], CaseTree [Either Term Type]))]
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 (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
    TyConMap
tcm <- Getting TyConMap RewriteEnv TyConMap
-> RewriteMonad NormalizeState TyConMap
forall s (m :: Type -> Type) a.
MonadReader s m =>
Getting a s a -> m a
Lens.view Getting TyConMap RewriteEnv TyConMap
Getter RewriteEnv TyConMap
tcCache
    let funName :: OccName
funName = Term -> OccName
decFunName Term
fun
        argLen :: Int
argLen = case CaseTree [Either Term Type] -> [[Either Term Type]]
forall (t :: Type -> Type) a. Foldable t => t a -> [a]
Foldable.toList CaseTree [Either Term Type]
cs of
                   [] -> String -> Int
forall a. HasCallStack => String -> a
error String
"mkDisjointGroup: no disjoint groups"
                   [Either Term Type]
l:[[Either Term Type]]
_ -> [Either Term Type] -> 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 :: [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 (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
fmap ([Either Term Type] -> Int -> Either Term Type
forall a. [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
    ([(Id, (Type, CaseTree Term))]
lbs,[Either Term Type]
newArgs) <- ([(Id, (Type, CaseTree Term))]
 -> (CaseTree (Either Term Type), Word)
 -> RewriteMonad
      NormalizeState ([(Id, (Type, CaseTree Term))], Either Term Type))
-> [(Id, (Type, CaseTree Term))]
-> [(CaseTree (Either Term Type), Word)]
-> RewriteMonad
     NormalizeState ([(Id, (Type, CaseTree Term))], [Either Term Type])
forall (m :: Type -> Type) acc x y.
Monad m =>
(acc -> x -> m (acc, y)) -> acc -> [x] -> m (acc, [y])
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 (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 (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
fmap ((Term -> Term) -> Either Term Type -> Either Term Type
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 (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) ->
          String
-> RewriteMonad
     NormalizeState ([(Id, (Type, CaseTree Term))], Either Term Type)
forall a. HasCallStack => String -> a
error (String
"mkDisjointGroup: non-equal type arguments: " String -> ShowS
forall a. Semigroup a => a -> a -> a
<>
                 [Type] -> String
forall p. PrettyPrec p => p -> String
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 (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 = String -> a
forall a. HasCallStack => String -> a
error (String
"mkDisjointGroup: mixed type and term arguments: " String -> ShowS
forall a. Semigroup a => a -> a -> a
<> [Either Term Type] -> String
forall a. Show a => a -> String
show [Either Term Type]
cL)
          (Maybe (Id, (Type, CaseTree Term))
lbM,Term
arg) <- InScopeSet
-> Type
-> CaseTree Term
-> OccName
-> 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) OccName
funName Word
pos
          case Maybe (Id, (Type, CaseTree Term))
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 (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 (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
_) ->
          String
-> RewriteMonad
     NormalizeState ([(Id, (Type, CaseTree Term))], Either Term Type)
forall a. HasCallStack => String -> a
error String
"mkDisjointGroup: no arguments"
      ) [] ([CaseTree (Either Term Type)]
-> [Word] -> [(CaseTree (Either Term Type), Word)]
forall a b. [a] -> [b] -> [(a, b)]
zip [CaseTree (Either Term Type)]
csT [Word
0..])
    let funApp :: Term
funApp = Term -> [Either Term Type] -> Term
mkApps Term
fun [Either Term Type]
newArgs
    IntMap TyConName
tupTcm <- Getting (IntMap TyConName) RewriteEnv (IntMap TyConName)
-> RewriteMonad NormalizeState (IntMap TyConName)
forall s (m :: Type -> Type) a.
MonadReader s m =>
Getting a s a -> m a
Lens.view Getting (IntMap TyConName) RewriteEnv (IntMap TyConName)
Getter RewriteEnv (IntMap TyConName)
tupleTcCache
    case [(Id, (Type, CaseTree Term))]
lbs of
      [] ->
        (Term, [Term]) -> RewriteMonad NormalizeState (Term, [Term])
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 (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 (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 (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 (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 (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 (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
fmap ((Term -> [Term] -> [Term])
-> CaseTree Term -> CaseTree ([Term] -> [Term])
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
        Id
tupIn <- InScopeSet -> OccName -> Type -> RewriteMonad NormalizeState Id
forall (m :: Type -> Type).
MonadUnique m =>
InScopeSet -> OccName -> Type -> m Id
mkInternalVar InScopeSet
inScope (OccName
funName OccName -> OccName -> OccName
forall a. Semigroup a => a -> a -> a
<> OccName
"_tupIn") Type
bigTupTy
        [LetBinding]
projections <-
          (Id -> Int -> RewriteMonad NormalizeState LetBinding)
-> [Id] -> [Int] -> RewriteMonad NormalizeState [LetBinding]
forall (m :: Type -> Type) a b c.
Applicative m =>
(a -> b -> m c) -> [a] -> [b] -> m [c]
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)
            [Id]
vs [Int
0..]
        (Term, [Term]) -> RewriteMonad NormalizeState (Term, [Term])
forall (m :: Type -> Type) a. Monad m => a -> m a
return ([LetBinding] -> Term -> Term
Letrec ((Id
tupIn,Term
ct)LetBinding -> [LetBinding] -> [LetBinding]
forall a. a -> [a] -> [a]
:[LetBinding]
projections) Term
funApp, [Term]
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
-> OccName
-> Word
-> NormalizeSession (Maybe (Id, (Type, CaseTree Term)), Term)
disJointSelProj InScopeSet
inScope Type
argTy CaseTree Term
cs OccName
funName Word
argN = do
    TyConMap
tcm <- Getting TyConMap RewriteEnv TyConMap
-> RewriteMonad NormalizeState TyConMap
forall s (m :: Type -> Type) a.
MonadReader s m =>
Getting a s a -> m a
Lens.view Getting TyConMap RewriteEnv TyConMap
Getter RewriteEnv TyConMap
tcCache
    IntMap TyConName
tupTcm <- Getting (IntMap TyConName) RewriteEnv (IntMap TyConName)
-> RewriteMonad NormalizeState (IntMap TyConName)
forall s (m :: Type -> Type) a.
MonadReader s m =>
Getting a s a -> m a
Lens.view Getting (IntMap TyConName) RewriteEnv (IntMap TyConName)
Getter RewriteEnv (IntMap TyConName)
tupleTcCache
    let sel :: Term
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 (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)
    Bool
untran <- Bool -> Type -> RewriteMonad NormalizeState Bool
forall extra. Bool -> Type -> RewriteMonad extra Bool
isUntranslatableType Bool
False Type
argTy
    case Bool
untran of
      Bool
True -> (Maybe (Id, (Type, CaseTree Term)), Term)
-> NormalizeSession (Maybe (Id, (Type, CaseTree Term)), Term)
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
        Id
argId <- InScopeSet -> OccName -> Type -> RewriteMonad NormalizeState Id
forall (m :: Type -> Type).
MonadUnique m =>
InScopeSet -> OccName -> Type -> m Id
mkInternalVar InScopeSet
inScope (OccName
funName OccName -> OccName -> OccName
forall a. Semigroup a => a -> a -> a
<> OccName
"_arg" OccName -> OccName -> OccName
forall a. Semigroup a => a -> a -> a
<> Word -> OccName
forall a. Show a => a -> OccName
showt Word
argN) Type
argTy
        (Maybe (Id, (Type, CaseTree Term)), Term)
-> NormalizeSession (Maybe (Id, (Type, CaseTree Term)), Term)
forall (m :: Type -> Type) a. Monad m => a -> m a
return ((Id, (Type, CaseTree Term)) -> Maybe (Id, (Type, CaseTree Term))
forall a. a -> Maybe a
Just (Id
argId,(Type
argTy,CaseTree Term
cs)), Id -> Term
Var Id
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 Any) -> (Var Any -> All) -> Type -> All
forall r s a. Getting r s a -> (a -> r) -> s -> r
Lens.foldMapOf ((forall b. Var b -> Bool) -> IntSet -> Getting All Type (Var Any)
forall (f :: Type -> Type) a.
(Contravariant f, Applicative f) =>
(forall b. Var b -> Bool)
-> IntSet -> (Var a -> f (Var a)) -> Type -> f Type
typeFreeVars' forall b. Var b -> Bool
isLocallyBound IntSet
IntSet.empty)
                                       (All -> Var Any -> 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 Any) -> (Var Any -> 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 Any)
forall (f :: Type -> Type) a.
(Contravariant f, Applicative f) =>
(forall b. Var b -> Bool) -> (Var a -> f (Var a)) -> Term -> f Term
termFreeVars' forall b. Var b -> Bool
isLocallyBound)
                                       (All -> Var Any -> 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 -> OccName
forall a. Name a -> OccName
nameOcc -> OccName
nm) [Type]
_ ->  OccName
nm OccName -> OccName -> Bool
forall a. Eq a => a -> a -> Bool
== Name -> OccName
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. HasCallStack => [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 Any]
coerce [TyVar]
ptvs [Var Any] -> [Var Any] -> [Var Any]
forall a. [a] -> [a] -> [a]
++ [Id] -> [Var Any]
coerce [Id]
pids) [Var Any] -> 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 (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 (String -> (TyConName, DataCon)
forall a. HasCallStack => String -> a
error (String
"Cannot build " String -> ShowS
forall a. Semigroup a => a -> a -> a
<> Int -> String
forall a. Show a => a -> String
show Int
n String -> ShowS
forall a. Semigroup a => a -> a -> a
<> String
"-tuble")) (Maybe (TyConName, DataCon) -> (TyConName, DataCon))
-> Maybe (TyConName, DataCon) -> (TyConName, DataCon)
forall a b. (a -> b) -> a -> b
$ do
    TyConName
tupTcNm <- Int -> IntMap TyConName -> Maybe TyConName
forall a. Int -> IntMap a -> Maybe a
IntMap.lookup Int
n IntMap TyConName
tupTcm
    TyCon
tupTc <- TyConName -> TyConMap -> Maybe TyCon
forall a b. Uniquable a => a -> UniqMap b -> Maybe b
UniqMap.lookup TyConName
tupTcNm TyConMap
tcm
    DataCon
tupDc <- [DataCon] -> Maybe DataCon
forall a. [a] -> Maybe a
Maybe.listToMaybe (TyCon -> [DataCon]
tyConDataCons TyCon
tupTc)
    (TyConName, DataCon) -> Maybe (TyConName, DataCon)
forall (m :: Type -> Type) a. Monad m => a -> m a
return (TyConName
tupTcNm,DataCon
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
_ [] = String -> (Type, Term)
forall a. HasCallStack => String -> a
error (String -> (Type, Term)) -> String -> (Type, Term)
forall a b. (a -> b) -> a -> b
$ String
$curLoc String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
"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 (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
_ [] = String -> Type
forall a. HasCallStack => String -> a
error (String -> Type) -> String -> Type
forall a b. (a -> b) -> a -> b
$ String
$curLoc String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
"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 (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 :: InScopeSet
-> TyConMap -> IntMap TyConName -> Term -> [Type] -> Int -> m Term
mkSmallTupSelector InScopeSet
_ TyConMap
_ IntMap TyConName
_ Term
scrut [Type
_] Int
0 = Term -> m Term
forall (m :: Type -> Type) a. Monad m => a -> m a
return Term
scrut
mkSmallTupSelector InScopeSet
_ TyConMap
_ IntMap TyConName
_ Term
_     [Type
_] Int
n = String -> m Term
forall a. HasCallStack => String -> a
error (String -> m Term) -> String -> m Term
forall a b. (a -> b) -> a -> b
$ String
$curLoc String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
"mkSmallTupSelector called with one type, but to select " String -> ShowS
forall a. [a] -> [a] -> [a]
++ Int -> String
forall a. Show a => a -> String
show Int
n
mkSmallTupSelector InScopeSet
inScope TyConMap
tcm IntMap TyConName
_ Term
scrut [Type]
_ Int
n = String -> InScopeSet -> TyConMap -> Term -> Int -> Int -> m Term
forall (m :: Type -> Type).
(HasCallStack, MonadUnique m) =>
String -> InScopeSet -> TyConMap -> Term -> Int -> Int -> m Term
mkSelectorCase (String
$curLoc String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
"mkSmallTupSelector") InScopeSet
inScope TyConMap
tcm Term
scrut Int
1 Int
n

mkBigTupSelector :: 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
      Term
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
      Term
inner <- 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
outer ([[Type]]
tyss [[Type]] -> Int -> [Type]
forall a. [a] -> Int -> a
List.!! Int
nOuter) Int
nInner
      Term -> m Term
forall (m :: Type -> Type) a. Monad m => a -> m a
return Term
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 OccName -> [(OccName, Bool)] -> Maybe Bool
forall a b. Eq a => a -> [(a, b)] -> Maybe b
List.lookup (PrimInfo -> OccName
primName PrimInfo
pInfo) [(OccName, 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 (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 :: [(OccName, Bool)]
interestingPrims = ((Name, Bool) -> (OccName, Bool))
-> [(Name, Bool)] -> [(OccName, Bool)]
forall a b. (a -> b) -> [a] -> [b]
map ((Name -> OccName) -> (Name, Bool) -> (OccName, Bool)
forall (p :: Type -> Type -> Type) a b c.
Bifunctor p =>
(a -> b) -> p a c -> p b c
first Name -> OccName
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,bothNotPow2)
      ,('GHC.Num.Integer.integerDiv,lastNotPow2)
      ,('GHC.Num.Integer.integerMod,lastNotPow2)
      ,('GHC.Num.Integer.integerQuot,lastNotPow2)
      ,('GHC.Num.Integer.integerRem,lastNotPow2)
#else
      ,('GHC.Integer.Type.timesInteger,Bool
bothNotPow2)
      ,('GHC.Integer.Type.divInteger,Bool
lastNotPow2)
      ,('GHC.Integer.Type.modInteger,Bool
lastNotPow2)
      ,('GHC.Integer.Type.quotInteger,Bool
lastNotPow2)
      ,('GHC.Integer.Type.remInteger,Bool
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. [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))])
          | OccName -> Bool
isFromInt (PrimInfo -> OccName
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 -> OccName
primName PrimInfo
p OccName -> OccName -> Bool
forall a. Eq a => a -> a -> Bool
== Name -> OccName
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 -> OccName
fromTHName = String -> OccName
Text.pack (String -> OccName) -> (Name -> String) -> Name -> OccName
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Name -> String
forall a. Show a => a -> String
show