{-# LANGUAGE OverloadedStrings         #-}
{-# LANGUAGE FlexibleInstances         #-}
{-# LANGUAGE GADTs                     #-}
{-# LANGUAGE NoMonomorphismRestriction #-}
{-# LANGUAGE RankNTypes                #-}
{-# LANGUAGE TupleSections             #-}
{-# LANGUAGE UndecidableInstances      #-}
{-# LANGUAGE FlexibleContexts          #-}

{-# OPTIONS_GHC -Wno-incomplete-uni-patterns #-}

-- | This module contains functions for recursively "rewriting"
--   GHC core using "rules".

module Language.Haskell.Liquid.Transforms.Rewrite
  ( -- * Top level rewrite function
    rewriteBinds

  -- * Low-level Rewriting Function
  -- , rewriteWith

  -- * Rewrite Rule
  -- ,  RewriteRule

  ) where

import           Liquid.GHC.API as Ghc hiding (showPpr, substExpr)
import           Language.Haskell.Liquid.GHC.TypeRep ()
import           Data.Maybe     (fromMaybe)
import           Control.Monad.State hiding (lift)
import           Language.Fixpoint.Misc       ({- mapFst, -}  mapSnd)
import qualified          Language.Fixpoint.Types as F
import           Language.Haskell.Liquid.Misc (safeZipWithError, Nat)
import           Language.Haskell.Liquid.GHC.Play (substExpr)
import           Language.Haskell.Liquid.GHC.Resugar
import           Language.Haskell.Liquid.GHC.Misc (unTickExpr, isTupleId, showPpr, mkAlive) -- , showPpr, tracePpr)
import           Language.Haskell.Liquid.UX.Config  (Config, noSimplifyCore)
import qualified Data.List as L
import qualified Data.HashMap.Strict as M

--------------------------------------------------------------------------------
-- | Top-level rewriter --------------------------------------------------------
--------------------------------------------------------------------------------
rewriteBinds :: Config -> [CoreBind] -> [CoreBind]
rewriteBinds :: Config -> [CoreBind] -> [CoreBind]
rewriteBinds Config
cfg
  | Config -> Bool
simplifyCore Config
cfg
  = forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (CoreBind -> CoreBind
normalizeTuples 
       forall b c a. (b -> c) -> (a -> b) -> a -> c
. RewriteRule -> CoreBind -> CoreBind
rewriteBindWith RewriteRule
undollar 
       forall b c a. (b -> c) -> (a -> b) -> a -> c
. RewriteRule -> CoreBind -> CoreBind
rewriteBindWith RewriteRule
tidyTuples 
       forall b c a. (b -> c) -> (a -> b) -> a -> c
. RewriteRule -> CoreBind -> CoreBind
rewriteBindWith RewriteRule
simplifyPatTuple)
  | Bool
otherwise
  = forall a. a -> a
id

simplifyCore :: Config -> Bool
simplifyCore :: Config -> Bool
simplifyCore = Bool -> Bool
not forall b c a. (b -> c) -> (a -> b) -> a -> c
. Config -> Bool
noSimplifyCore

undollar :: RewriteRule
undollar :: RewriteRule
undollar = RewriteRule
go 
  where 
    go :: RewriteRule
go CoreExpr
e 
     -- matches `$ t1 t2 t3 f a`  
     | App CoreExpr
e1 CoreExpr
a  <- CoreExpr -> CoreExpr
untick CoreExpr
e
     , App CoreExpr
e2 CoreExpr
f  <- CoreExpr -> CoreExpr
untick CoreExpr
e1
     , App CoreExpr
e3 CoreExpr
t3 <- CoreExpr -> CoreExpr
untick CoreExpr
e2 
     , App CoreExpr
e4 CoreExpr
t2 <- CoreExpr -> CoreExpr
untick CoreExpr
e3 
     , App CoreExpr
d CoreExpr
t1  <- CoreExpr -> CoreExpr
untick CoreExpr
e4 
     , Var Var
v     <- CoreExpr -> CoreExpr
untick CoreExpr
d 
     , Var
v forall a. Uniquable a => a -> Unique -> Bool
`hasKey` Unique
dollarIdKey
     , Type Type
_    <- CoreExpr -> CoreExpr
untick CoreExpr
t1
     , Type Type
_    <- CoreExpr -> CoreExpr
untick CoreExpr
t2
     , Type Type
_    <- CoreExpr -> CoreExpr
untick CoreExpr
t3
     = forall a. a -> Maybe a
Just forall a b. (a -> b) -> a -> b
$ forall b. Expr b -> Expr b -> Expr b
App CoreExpr
f CoreExpr
a 
    go (Tick CoreTickish
t CoreExpr
e)
      = forall b. CoreTickish -> Expr b -> Expr b
Tick CoreTickish
t forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> RewriteRule
go CoreExpr
e
    go (Let (NonRec Var
x CoreExpr
ex) CoreExpr
e)
      = do CoreExpr
ex' <- RewriteRule
go CoreExpr
ex
           CoreExpr
e'  <- RewriteRule
go CoreExpr
e
           forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall b. Bind b -> Expr b -> Expr b
Let (forall b. b -> Expr b -> Bind b
NonRec Var
x CoreExpr
ex') CoreExpr
e'
    go (Let (Rec [(Var, CoreExpr)]
bes) CoreExpr
e)
      = forall b. Bind b -> Expr b -> Expr b
Let forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (forall b. [(b, Expr b)] -> Bind b
Rec forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM (Var, CoreExpr) -> Maybe (Var, CoreExpr)
goRec [(Var, CoreExpr)]
bes) forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> RewriteRule
go CoreExpr
e
    go (Case CoreExpr
e Var
x Type
t [Alt Var]
alts)
      = forall b. Expr b -> b -> Type -> [Alt b] -> Expr b
Case CoreExpr
e Var
x Type
t forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM Alt Var -> Maybe (Alt Var)
goAlt [Alt Var]
alts
    go (App CoreExpr
e1 CoreExpr
e2)
      = forall b. Expr b -> Expr b -> Expr b
App forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> RewriteRule
go CoreExpr
e1 forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> RewriteRule
go CoreExpr
e2
    go (Lam Var
x CoreExpr
e)
      = forall b. b -> Expr b -> Expr b
Lam Var
x forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> RewriteRule
go CoreExpr
e
    go (Cast CoreExpr
e CoercionR
c)
      = (forall b. Expr b -> CoercionR -> Expr b
`Cast` CoercionR
c) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> RewriteRule
go CoreExpr
e
    go CoreExpr
e
      = forall (m :: * -> *) a. Monad m => a -> m a
return CoreExpr
e

    goRec :: (Var, CoreExpr) -> Maybe (Var, CoreExpr)
goRec (Var
x, CoreExpr
e)
      = (Var
x,) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> RewriteRule
go CoreExpr
e

    goAlt :: Alt Var -> Maybe (Alt Var)
goAlt (Alt AltCon
c [Var]
bs CoreExpr
e)
      = forall b. AltCon -> [b] -> Expr b -> Alt b
Alt AltCon
c [Var]
bs forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> RewriteRule
go CoreExpr
e

  
 

untick :: CoreExpr -> CoreExpr 
untick :: CoreExpr -> CoreExpr
untick (Tick CoreTickish
_ CoreExpr
e) = CoreExpr -> CoreExpr
untick CoreExpr
e 
untick CoreExpr
e          = CoreExpr
e 

tidyTuples :: RewriteRule
tidyTuples :: RewriteRule
tidyTuples CoreExpr
ce = forall a. a -> Maybe a
Just forall a b. (a -> b) -> a -> b
$ forall s a. State s a -> s -> a
evalState (forall {f :: * -> *}.
MonadState [((AltCon, Var), [Var])] f =>
CoreExpr -> f CoreExpr
go CoreExpr
ce) []
  where
    go :: CoreExpr -> f CoreExpr
go (Tick CoreTickish
t CoreExpr
e)
      = forall b. CoreTickish -> Expr b -> Expr b
Tick CoreTickish
t forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> CoreExpr -> f CoreExpr
go CoreExpr
e
    go (Let (NonRec Var
x CoreExpr
ex) CoreExpr
e)
      = do CoreExpr
ex' <- CoreExpr -> f CoreExpr
go CoreExpr
ex
           CoreExpr
e'  <- CoreExpr -> f CoreExpr
go CoreExpr
e
           forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall b. Bind b -> Expr b -> Expr b
Let (forall b. b -> Expr b -> Bind b
NonRec Var
x CoreExpr
ex') CoreExpr
e'
    go (Let (Rec [(Var, CoreExpr)]
bes) CoreExpr
e)
      = forall b. Bind b -> Expr b -> Expr b
Let forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (forall b. [(b, Expr b)] -> Bind b
Rec forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM (Var, CoreExpr) -> f (Var, CoreExpr)
goRec [(Var, CoreExpr)]
bes) forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> CoreExpr -> f CoreExpr
go CoreExpr
e
    go (Case (Var Var
v) Var
x Type
t [Alt Var]
alts)
      = forall b. Expr b -> b -> Type -> [Alt b] -> Expr b
Case (forall b. Var -> Expr b
Var Var
v) Var
x Type
t forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM (forall {m :: * -> *} {b}.
(MonadState [((AltCon, b), [Var])] m, Eq b) =>
b -> Alt Var -> m (Alt Var)
goAltR Var
v) [Alt Var]
alts
    go (Case CoreExpr
e Var
x Type
t [Alt Var]
alts)
      = forall b. Expr b -> b -> Type -> [Alt b] -> Expr b
Case CoreExpr
e Var
x Type
t forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM Alt Var -> f (Alt Var)
goAlt [Alt Var]
alts
    go (App CoreExpr
e1 CoreExpr
e2)
      = forall b. Expr b -> Expr b -> Expr b
App forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> CoreExpr -> f CoreExpr
go CoreExpr
e1 forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> CoreExpr -> f CoreExpr
go CoreExpr
e2
    go (Lam Var
x CoreExpr
e)
      = forall b. b -> Expr b -> Expr b
Lam Var
x forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> CoreExpr -> f CoreExpr
go CoreExpr
e
    go (Cast CoreExpr
e CoercionR
c)
      = (forall b. Expr b -> CoercionR -> Expr b
`Cast` CoercionR
c) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> CoreExpr -> f CoreExpr
go CoreExpr
e
    go CoreExpr
e
      = forall (m :: * -> *) a. Monad m => a -> m a
return CoreExpr
e

    goRec :: (Var, CoreExpr) -> f (Var, CoreExpr)
goRec (Var
x, CoreExpr
e)
      = (Var
x,) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> CoreExpr -> f CoreExpr
go CoreExpr
e

    goAlt :: Alt Var -> f (Alt Var)
goAlt (Alt AltCon
c [Var]
bs CoreExpr
e)
      = forall b. AltCon -> [b] -> Expr b -> Alt b
Alt AltCon
c [Var]
bs forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> CoreExpr -> f CoreExpr
go CoreExpr
e

    goAltR :: b -> Alt Var -> m (Alt Var)
goAltR b
v (Alt AltCon
c [Var]
bs CoreExpr
e)
      = do [((AltCon, b), [Var])]
m <- forall s (m :: * -> *). MonadState s m => m s
get
           case forall a b. Eq a => a -> [(a, b)] -> Maybe b
L.lookup (AltCon
c,b
v) [((AltCon, b), [Var])]
m of
            Just [Var]
bs' -> forall (m :: * -> *) a. Monad m => a -> m a
return (forall b. AltCon -> [b] -> Expr b -> Alt b
Alt AltCon
c [Var]
bs' ([Var] -> [Var] -> CoreExpr -> CoreExpr
substTuple [Var]
bs' [Var]
bs CoreExpr
e))
            Maybe [Var]
Nothing  -> do let bs' :: [Var]
bs' = Var -> Var
mkAlive forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [Var]
bs
                           forall s (m :: * -> *). MonadState s m => (s -> s) -> m ()
modify (((AltCon
c,b
v),[Var]
bs')forall a. a -> [a] -> [a]
:)
                           forall (m :: * -> *) a. Monad m => a -> m a
return (forall b. AltCon -> [b] -> Expr b -> Alt b
Alt AltCon
c [Var]
bs' CoreExpr
e)



normalizeTuples :: CoreBind -> CoreBind
normalizeTuples :: CoreBind -> CoreBind
normalizeTuples CoreBind
cb
  | NonRec Var
x CoreExpr
e <- CoreBind
cb
  = forall b. b -> Expr b -> Bind b
NonRec Var
x forall a b. (a -> b) -> a -> b
$ CoreExpr -> CoreExpr
go CoreExpr
e
  | Rec [(Var, CoreExpr)]
xes <- CoreBind
cb
  = let ([Var]
xs,[CoreExpr]
es) = forall a b. [(a, b)] -> ([a], [b])
unzip [(Var, CoreExpr)]
xes in
    forall b. [(b, Expr b)] -> Bind b
Rec forall a b. (a -> b) -> a -> b
$ forall a b. [a] -> [b] -> [(a, b)]
zip [Var]
xs (CoreExpr -> CoreExpr
go forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [CoreExpr]
es)
  where
    go :: CoreExpr -> CoreExpr
go (Let (NonRec Var
x CoreExpr
ex) CoreExpr
e)
      | Case CoreExpr
_ Var
_ Type
_ [Alt Var]
alts  <- CoreExpr -> CoreExpr
unTickExpr CoreExpr
ex
      , [Alt AltCon
_ [Var]
vs (Var Var
z)] <- [Alt Var]
alts
      , Var
z forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [Var]
vs
      = forall b. Bind b -> Expr b -> Expr b
Let (forall b. b -> Expr b -> Bind b
NonRec Var
z (CoreExpr -> CoreExpr
go CoreExpr
ex)) ([Var] -> [Var] -> CoreExpr -> CoreExpr
substTuple [Var
z] [Var
x] (CoreExpr -> CoreExpr
go CoreExpr
e))
    go (Let (NonRec Var
x CoreExpr
ex) CoreExpr
e)
      = forall b. Bind b -> Expr b -> Expr b
Let (forall b. b -> Expr b -> Bind b
NonRec Var
x (CoreExpr -> CoreExpr
go CoreExpr
ex)) (CoreExpr -> CoreExpr
go CoreExpr
e)
    go (Let (Rec [(Var, CoreExpr)]
xes) CoreExpr
e)
      = forall b. Bind b -> Expr b -> Expr b
Let (forall b. [(b, Expr b)] -> Bind b
Rec (forall b c a. (b -> c) -> (a, b) -> (a, c)
mapSnd CoreExpr -> CoreExpr
go forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [(Var, CoreExpr)]
xes)) (CoreExpr -> CoreExpr
go CoreExpr
e)
    go (App CoreExpr
e1 CoreExpr
e2)
      = forall b. Expr b -> Expr b -> Expr b
App (CoreExpr -> CoreExpr
go CoreExpr
e1) (CoreExpr -> CoreExpr
go CoreExpr
e2)
    go (Lam Var
x CoreExpr
e)
      = forall b. b -> Expr b -> Expr b
Lam Var
x (CoreExpr -> CoreExpr
go CoreExpr
e)
    go (Case CoreExpr
e Var
b Type
t [Alt Var]
alt)
      = forall b. Expr b -> b -> Type -> [Alt b] -> Expr b
Case (CoreExpr -> CoreExpr
go CoreExpr
e) Var
b Type
t ((\(Alt AltCon
c [Var]
bs CoreExpr
e') -> forall b. AltCon -> [b] -> Expr b -> Alt b
Alt AltCon
c [Var]
bs (CoreExpr -> CoreExpr
go CoreExpr
e')) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [Alt Var]
alt)
    go (Cast CoreExpr
e CoercionR
c)
      = forall b. Expr b -> CoercionR -> Expr b
Cast (CoreExpr -> CoreExpr
go CoreExpr
e) CoercionR
c
    go (Tick CoreTickish
t CoreExpr
e)
      = forall b. CoreTickish -> Expr b -> Expr b
Tick CoreTickish
t (CoreExpr -> CoreExpr
go CoreExpr
e)
    go (Type Type
t)
      = forall b. Type -> Expr b
Type Type
t
    go (Coercion CoercionR
c)
      = forall b. CoercionR -> Expr b
Coercion CoercionR
c
    go (Lit Literal
l)
      = forall b. Literal -> Expr b
Lit Literal
l
    go (Var Var
x)
      = forall b. Var -> Expr b
Var Var
x


--------------------------------------------------------------------------------
-- | A @RewriteRule@ is a function that maps a CoreExpr to another
--------------------------------------------------------------------------------
type RewriteRule = CoreExpr -> Maybe CoreExpr
--------------------------------------------------------------------------------

--------------------------------------------------------------------------------
rewriteBindWith :: RewriteRule -> CoreBind -> CoreBind
--------------------------------------------------------------------------------
rewriteBindWith :: RewriteRule -> CoreBind -> CoreBind
rewriteBindWith RewriteRule
r (NonRec Var
x CoreExpr
e) = forall b. b -> Expr b -> Bind b
NonRec Var
x (RewriteRule -> CoreExpr -> CoreExpr
rewriteWith RewriteRule
r CoreExpr
e)
rewriteBindWith RewriteRule
r (Rec [(Var, CoreExpr)]
xes)    = forall b. [(b, Expr b)] -> Bind b
Rec    (forall b c a. (b -> c) -> (a, b) -> (a, c)
mapSnd (RewriteRule -> CoreExpr -> CoreExpr
rewriteWith RewriteRule
r) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [(Var, CoreExpr)]
xes)

--------------------------------------------------------------------------------
rewriteWith :: RewriteRule -> CoreExpr -> CoreExpr
--------------------------------------------------------------------------------
rewriteWith :: RewriteRule -> CoreExpr -> CoreExpr
rewriteWith RewriteRule
tx           = CoreExpr -> CoreExpr
go
  where
    go :: CoreExpr -> CoreExpr
go                   = CoreExpr -> CoreExpr
txTop forall b c a. (b -> c) -> (a -> b) -> a -> c
. CoreExpr -> CoreExpr
step
    txTop :: CoreExpr -> CoreExpr
txTop CoreExpr
e              = forall a. a -> Maybe a -> a
fromMaybe CoreExpr
e (RewriteRule
tx CoreExpr
e)
    goB :: CoreBind -> CoreBind
goB (Rec [(Var, CoreExpr)]
xes)        = forall b. [(b, Expr b)] -> Bind b
Rec         (forall b c a. (b -> c) -> (a, b) -> (a, c)
mapSnd CoreExpr -> CoreExpr
go forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [(Var, CoreExpr)]
xes)
    goB (NonRec Var
x CoreExpr
e)     = forall b. b -> Expr b -> Bind b
NonRec Var
x    (CoreExpr -> CoreExpr
go CoreExpr
e)
    step :: CoreExpr -> CoreExpr
step (Let CoreBind
b CoreExpr
e)       = forall b. Bind b -> Expr b -> Expr b
Let (CoreBind -> CoreBind
goB CoreBind
b) (CoreExpr -> CoreExpr
go CoreExpr
e)
    step (App CoreExpr
e CoreExpr
e')      = forall b. Expr b -> Expr b -> Expr b
App (CoreExpr -> CoreExpr
go CoreExpr
e)  (CoreExpr -> CoreExpr
go CoreExpr
e')
    step (Lam Var
x CoreExpr
e)       = forall b. b -> Expr b -> Expr b
Lam Var
x       (CoreExpr -> CoreExpr
go CoreExpr
e)
    step (Cast CoreExpr
e CoercionR
c)      = forall b. Expr b -> CoercionR -> Expr b
Cast (CoreExpr -> CoreExpr
go CoreExpr
e) CoercionR
c
    step (Tick CoreTickish
t CoreExpr
e)      = forall b. CoreTickish -> Expr b -> Expr b
Tick CoreTickish
t      (CoreExpr -> CoreExpr
go CoreExpr
e)
    step (Case CoreExpr
e Var
x Type
t [Alt Var]
cs) = forall b. Expr b -> b -> Type -> [Alt b] -> Expr b
Case (CoreExpr -> CoreExpr
go CoreExpr
e) Var
x Type
t ((\(Alt AltCon
c [Var]
bs CoreExpr
e') -> forall b. AltCon -> [b] -> Expr b -> Alt b
Alt AltCon
c [Var]
bs (CoreExpr -> CoreExpr
go CoreExpr
e')) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [Alt Var]
cs)
    step e :: CoreExpr
e@(Type Type
_)      = CoreExpr
e
    step e :: CoreExpr
e@(Lit Literal
_)       = CoreExpr
e
    step e :: CoreExpr
e@(Var Var
_)       = CoreExpr
e
    step e :: CoreExpr
e@(Coercion CoercionR
_)  = CoreExpr
e


--------------------------------------------------------------------------------
-- | Rewriting Pattern-Match-Tuples --------------------------------------------
--------------------------------------------------------------------------------

{-
    let CrazyPat x1 ... xn = e in e'

    let t : (t1,...,tn) = "CrazyPat e ... (y1, ..., yn)"
        xn = Proj t n
        ...
        x1 = Proj t 1
    in
        e'

    "crazy-pat"
 -}

{- [NOTE] The following is the structure of a @PatMatchTup@

      let x :: (t1,...,tn) = E[(x1,...,xn)]
          yn = case x of (..., yn) -> yn
          …
          y1 = case x of (y1, ...) -> y1
      in
          E'

  GOAL: simplify the above to:

      E [ (x1,...,xn) := E' [y1 := x1,...,yn := xn] ]

  TODO: several tests (e.g. tests/pos/zipper000.hs) fail because
  the above changes the "type" the expression `E` and in "other branches"
  the new type may be different than the old, e.g.

     let (x::y::_) = e in
     x + y

     let t = case e of
               h1::t1 -> case t1 of
                            (h2::t2) ->  (h1, h2)
                            DEFAULT  ->  error @ (Int, Int)
               DEFAULT   -> error @ (Int, Int)
         x = case t of (h1, _) -> h1
         y = case t of (_, h2) -> h2
     in
         x + y

  is rewritten to:

              h1::t1    -> case t1 of
                            (h2::t2) ->  h1 + h2
                            DEFAULT  ->  error @ (Int, Int)
              DEFAULT   -> error @ (Int, Int)

     case e of
       h1 :: h2 :: _ -> h1 + h2
       DEFAULT       -> error @ (Int, Int)

  which, alas, is ill formed.

-}

--------------------------------------------------------------------------------

-- simplifyPatTuple :: RewriteRule
-- simplifyPatTuple e =
--  case simplifyPatTuple' e of
--    Just e' -> if Ghc.exprType e == Ghc.exprType e'
--                 then Just e'
--                 else Just (tracePpr ("YIKES: RWR " ++ showPpr e) e')
--    Nothing -> Nothing


_safeSimplifyPatTuple :: RewriteRule
_safeSimplifyPatTuple :: RewriteRule
_safeSimplifyPatTuple CoreExpr
e
  | Just CoreExpr
e' <- RewriteRule
simplifyPatTuple CoreExpr
e
  , CoreExpr -> Type
Ghc.exprType CoreExpr
e' forall a. Eq a => a -> a -> Bool
== CoreExpr -> Type
Ghc.exprType CoreExpr
e
  = forall a. a -> Maybe a
Just CoreExpr
e'
  | Bool
otherwise
  = forall a. Maybe a
Nothing

--------------------------------------------------------------------------------
simplifyPatTuple :: RewriteRule
--------------------------------------------------------------------------------

_tidyAlt :: Int -> Maybe CoreExpr -> Maybe CoreExpr

_tidyAlt :: Int -> Maybe CoreExpr -> Maybe CoreExpr
_tidyAlt Int
n (Just (Let (NonRec Var
cb CoreExpr
expr) CoreExpr
rest))
  | Just ([(Var, CoreExpr)]
yes, CoreExpr
e') <- Int -> CoreExpr -> Maybe ([(Var, CoreExpr)], CoreExpr)
takeBinds Int
n CoreExpr
rest
  = forall a. a -> Maybe a
Just forall a b. (a -> b) -> a -> b
$ forall b. Bind b -> Expr b -> Expr b
Let (forall b. b -> Expr b -> Bind b
NonRec Var
cb CoreExpr
expr) forall a b. (a -> b) -> a -> b
$ forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl (\CoreExpr
e (Var
x, CoreExpr
ex) -> forall b. Bind b -> Expr b -> Expr b
Let (forall b. b -> Expr b -> Bind b
NonRec Var
x CoreExpr
ex) CoreExpr
e) CoreExpr
e' (forall a. [a] -> [a]
reverse forall a b. (a -> b) -> a -> b
$ forall {a} {b}. [(a, Expr b)] -> [(a, Expr b)]
go forall a b. (a -> b) -> a -> b
$ forall a. [a] -> [a]
reverse [(Var, CoreExpr)]
yes)

  where
    go :: [(a, Expr b)] -> [(a, Expr b)]
go xes :: [(a, Expr b)]
xes@((a
_, Expr b
e):[(a, Expr b)]
_) = let bs :: [b]
bs = forall {a}. Expr a -> [a]
grapBinds Expr b
e in forall b c a. (b -> c) -> (a, b) -> (a, c)
mapSnd (forall {b}. [b] -> Expr b -> Expr b
replaceBinds [b]
bs) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [(a, Expr b)]
xes
    go [] = []
    replaceBinds :: [b] -> Expr b -> Expr b
replaceBinds [b]
bs (Case Expr b
c b
x Type
t [Alt b]
alt) = forall b. Expr b -> b -> Type -> [Alt b] -> Expr b
Case Expr b
c b
x Type
t (forall {b}. [b] -> Alt b -> Alt b
replaceBindsAlt [b]
bs forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [Alt b]
alt)
    replaceBinds [b]
bs (Tick CoreTickish
t Expr b
e)       = forall b. CoreTickish -> Expr b -> Expr b
Tick CoreTickish
t ([b] -> Expr b -> Expr b
replaceBinds [b]
bs Expr b
e)
    replaceBinds [b]
_ Expr b
e                 = Expr b
e
    replaceBindsAlt :: [b] -> Alt b -> Alt b
replaceBindsAlt [b]
bs (Alt AltCon
c [b]
_ Expr b
e)     = forall b. AltCon -> [b] -> Expr b -> Alt b
Alt AltCon
c [b]
bs Expr b
e

    grapBinds :: Expr a -> [a]
grapBinds (Case Expr a
_ a
_ Type
_ [Alt a]
alt) = forall {a}. [Alt a] -> [a]
grapBinds' [Alt a]
alt
    grapBinds (Tick CoreTickish
_ Expr a
e) = Expr a -> [a]
grapBinds Expr a
e
    grapBinds Expr a
_ = []
    grapBinds' :: [Alt a] -> [a]
grapBinds' [] = []
    grapBinds' (Alt AltCon
_ [a]
bs Expr a
_ : [Alt a]
_) = [a]
bs

_tidyAlt Int
_ Maybe CoreExpr
e
  = Maybe CoreExpr
e

simplifyPatTuple :: RewriteRule
simplifyPatTuple (Let (NonRec Var
x CoreExpr
e) CoreExpr
rest)
  | Just (Int
n, [Type]
ts  ) <- Var -> Maybe (Int, [Type])
varTuple Var
x
  , Int
2 forall a. Ord a => a -> a -> Bool
<= Int
n
  , Just ([(Var, CoreExpr)]
yes, CoreExpr
e') <- Int -> CoreExpr -> Maybe ([(Var, CoreExpr)], CoreExpr)
takeBinds Int
n CoreExpr
rest
  , let ys :: [Var]
ys          = forall a b. (a, b) -> a
fst forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [(Var, CoreExpr)]
yes
  , Just [Var]
_         <- [Var] -> CoreExpr -> Maybe [Var]
hasTuple [Var]
ys CoreExpr
e
  , [(Var, CoreExpr)] -> [Type] -> Bool
matchTypes [(Var, CoreExpr)]
yes [Type]
ts
  = [Var] -> CoreExpr -> RewriteRule
replaceTuple [Var]
ys CoreExpr
e CoreExpr
e'

simplifyPatTuple CoreExpr
_
  = forall a. Maybe a
Nothing

varTuple :: Var -> Maybe (Int, [Type])
varTuple :: Var -> Maybe (Int, [Type])
varTuple Var
x
  | TyConApp TyCon
c [Type]
ts <- Var -> Type
Ghc.varType Var
x
  , TyCon -> Bool
isTupleTyCon TyCon
c
  = forall a. a -> Maybe a
Just (forall (t :: * -> *) a. Foldable t => t a -> Int
length [Type]
ts, [Type]
ts)
  | Bool
otherwise
  = forall a. Maybe a
Nothing

takeBinds  :: Nat -> CoreExpr -> Maybe ([(Var, CoreExpr)], CoreExpr)
takeBinds :: Int -> CoreExpr -> Maybe ([(Var, CoreExpr)], CoreExpr)
takeBinds Int
nat CoreExpr
ce
  | Int
nat forall a. Ord a => a -> a -> Bool
< Int
2     = forall a. Maybe a
Nothing
  | Bool
otherwise = {- mapFst reverse <$> -} forall {t} {a}.
(Eq t, Num t) =>
t -> Expr a -> Maybe ([(a, Expr a)], Expr a)
go Int
nat CoreExpr
ce
    where
      go :: t -> Expr a -> Maybe ([(a, Expr a)], Expr a)
go t
0 Expr a
e                      = forall a. a -> Maybe a
Just ([], Expr a
e)
      go t
n (Let (NonRec a
x Expr a
e) Expr a
e')  = do ([(a, Expr a)]
xes, Expr a
e'') <- t -> Expr a -> Maybe ([(a, Expr a)], Expr a)
go (t
nforall a. Num a => a -> a -> a
-t
1) Expr a
e'
                                       forall a. a -> Maybe a
Just ((a
x,Expr a
e) forall a. a -> [a] -> [a]
: [(a, Expr a)]
xes, Expr a
e'')
      go t
_ Expr a
_                      = forall a. Maybe a
Nothing

matchTypes :: [(Var, CoreExpr)] -> [Type] -> Bool
matchTypes :: [(Var, CoreExpr)] -> [Type] -> Bool
matchTypes [(Var, CoreExpr)]
xes [Type]
ts =  Int
xN forall a. Eq a => a -> a -> Bool
== Int
tN
                  Bool -> Bool -> Bool
&& forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all (forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry Type -> Type -> Bool
eqType) (forall t t1. String -> [t] -> [t1] -> [(t, t1)]
safeZipWithError forall {a}. IsString a => a
msg [Type]
xts [Type]
ts)
                  Bool -> Bool -> Bool
&& forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all CoreExpr -> Bool
isProjection [CoreExpr]
es
  where
    xN :: Int
xN            = forall (t :: * -> *) a. Foldable t => t a -> Int
length [(Var, CoreExpr)]
xes
    tN :: Int
tN            = forall (t :: * -> *) a. Foldable t => t a -> Int
length [Type]
ts
    xts :: [Type]
xts           = Var -> Type
Ghc.varType forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [Var]
xs
    ([Var]
xs, [CoreExpr]
es)      = forall a b. [(a, b)] -> ([a], [b])
unzip [(Var, CoreExpr)]
xes
    msg :: a
msg           = a
"RW:matchTypes"

isProjection :: CoreExpr -> Bool
isProjection :: CoreExpr -> Bool
isProjection CoreExpr
e = case CoreExpr -> Maybe Pattern
lift CoreExpr
e of
                   Just PatProject{} -> Bool
True
                   Maybe Pattern
_                 -> Bool
False

--------------------------------------------------------------------------------
-- | `hasTuple ys e` CHECKS if `e` contains a tuple that "looks like" (y1...yn)
--------------------------------------------------------------------------------
hasTuple :: [Var] -> CoreExpr -> Maybe [Var]
--------------------------------------------------------------------------------
hasTuple :: [Var] -> CoreExpr -> Maybe [Var]
hasTuple [Var]
ys = CoreExpr -> Maybe [Var]
stepE
  where
    stepE :: CoreExpr -> Maybe [Var]
stepE CoreExpr
e
     | Just [Var]
xs <- [Var] -> CoreExpr -> Maybe [Var]
isVarTup [Var]
ys CoreExpr
e = forall a. a -> Maybe a
Just [Var]
xs
     | Bool
otherwise                = CoreExpr -> Maybe [Var]
go CoreExpr
e
    stepA :: Alt Var -> Maybe [Var]
stepA (Alt AltCon
DEFAULT [Var]
_ CoreExpr
_)     = forall a. Maybe a
Nothing
    stepA (Alt AltCon
_ [Var]
_ CoreExpr
e)           = CoreExpr -> Maybe [Var]
stepE CoreExpr
e
    go :: CoreExpr -> Maybe [Var]
go (Let CoreBind
_ CoreExpr
e)                = CoreExpr -> Maybe [Var]
stepE CoreExpr
e
    go (Case CoreExpr
_ Var
_ Type
_ [Alt Var]
cs)          = forall (t :: * -> *) (m :: * -> *) a.
(Foldable t, MonadPlus m) =>
t (m a) -> m a
msum (Alt Var -> Maybe [Var]
stepA forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [Alt Var]
cs)
    go CoreExpr
_                        = forall a. Maybe a
Nothing

--------------------------------------------------------------------------------
-- | `replaceTuple ys e e'` REPLACES tuples that "looks like" (y1...yn) with e'
--------------------------------------------------------------------------------

replaceTuple :: [Var] -> CoreExpr -> CoreExpr -> Maybe CoreExpr
replaceTuple :: [Var] -> CoreExpr -> RewriteRule
replaceTuple [Var]
ys CoreExpr
ce CoreExpr
ce'           = RewriteRule
stepE CoreExpr
ce
  where
    t' :: Type
t'                          = CoreExpr -> Type
Ghc.exprType CoreExpr
ce'
    stepE :: RewriteRule
stepE CoreExpr
e
     | Just [Var]
xs <- [Var] -> CoreExpr -> Maybe [Var]
isVarTup [Var]
ys CoreExpr
e = forall a. a -> Maybe a
Just forall a b. (a -> b) -> a -> b
$ [Var] -> [Var] -> CoreExpr -> CoreExpr
substTuple [Var]
xs [Var]
ys CoreExpr
ce'
     | Bool
otherwise                = RewriteRule
go CoreExpr
e
    stepA :: Alt Var -> Maybe (Alt Var)
stepA (Alt AltCon
DEFAULT [Var]
xs CoreExpr
err)  = forall a. a -> Maybe a
Just (forall b. AltCon -> [b] -> Expr b -> Alt b
Alt AltCon
DEFAULT [Var]
xs (Type -> CoreExpr -> CoreExpr
replaceIrrefutPat Type
t' CoreExpr
err))
    stepA (Alt AltCon
c [Var]
xs CoreExpr
e)          = forall b. AltCon -> [b] -> Expr b -> Alt b
Alt AltCon
c [Var]
xs   forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> RewriteRule
stepE CoreExpr
e
    go :: RewriteRule
go (Let CoreBind
b CoreExpr
e)                = forall b. Bind b -> Expr b -> Expr b
Let CoreBind
b      forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> RewriteRule
stepE CoreExpr
e
    go (Case CoreExpr
e Var
x Type
t [Alt Var]
cs)          = CoreExpr -> Var -> Type -> [Alt Var] -> CoreExpr
fixCase CoreExpr
e Var
x Type
t forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM Alt Var -> Maybe (Alt Var)
stepA [Alt Var]
cs
    go CoreExpr
_                        = forall a. Maybe a
Nothing

_showExpr :: CoreExpr -> String
_showExpr :: CoreExpr -> String
_showExpr = CoreExpr -> String
show'
  where
    show' :: CoreExpr -> String
show' (App CoreExpr
e1 CoreExpr
e2) = CoreExpr -> String
show' CoreExpr
e1 forall a. [a] -> [a] -> [a]
++ String
" " forall a. [a] -> [a] -> [a]
++ CoreExpr -> String
show' CoreExpr
e2
    show' (Var Var
x)     = Var -> String
_showVar Var
x
    show' (Let (NonRec Var
x CoreExpr
ex) CoreExpr
e) = String
"Let " forall a. [a] -> [a] -> [a]
++ Var -> String
_showVar Var
x forall a. [a] -> [a] -> [a]
++ String
" = " forall a. [a] -> [a] -> [a]
++ CoreExpr -> String
show' CoreExpr
ex forall a. [a] -> [a] -> [a]
++ String
"\nIN " forall a. [a] -> [a] -> [a]
++ CoreExpr -> String
show' CoreExpr
e
    show' (Tick CoreTickish
_ CoreExpr
e) = CoreExpr -> String
show' CoreExpr
e
    show' (Case CoreExpr
e Var
x Type
_ [Alt Var]
alt) = String
"Case " forall a. [a] -> [a] -> [a]
++ Var -> String
_showVar Var
x forall a. [a] -> [a] -> [a]
++ String
" = " forall a. [a] -> [a] -> [a]
++ CoreExpr -> String
show' CoreExpr
e forall a. [a] -> [a] -> [a]
++ String
" OF " forall a. [a] -> [a] -> [a]
++ [String] -> String
unlines (Alt Var -> String
showAlt' forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [Alt Var]
alt)
    show' CoreExpr
e           = forall a. Outputable a => a -> String
showPpr CoreExpr
e

    showAlt' :: Alt Var -> String
showAlt' (Alt AltCon
c [Var]
bs CoreExpr
e) = forall a. Outputable a => a -> String
showPpr AltCon
c forall a. [a] -> [a] -> [a]
++ [String] -> String
unwords (Var -> String
_showVar forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [Var]
bs) forall a. [a] -> [a] -> [a]
++ String
" -> " forall a. [a] -> [a] -> [a]
++ CoreExpr -> String
show' CoreExpr
e

_showVar :: Var -> String
_showVar :: Var -> String
_showVar = forall a. Show a => a -> String
show forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. Symbolic a => a -> Symbol
F.symbol

_errorSkip :: String -> a -> b
_errorSkip :: forall a b. String -> a -> b
_errorSkip String
x a
_ = forall a. HasCallStack => String -> a
error String
x

-- replaceTuple :: [Var] -> CoreExpr -> CoreExpr -> Maybe CoreExpr
-- replaceTuple ys e e' = tracePpr msg (_replaceTuple ys e e')
--  where
--    msg = "replaceTuple: ys = " ++ showPpr ys ++
--                        " e = " ++ showPpr e  ++
--                        " e' =" ++ showPpr e'

-- | The substitution (`substTuple`) can change the type of the overall
--   case-expression, so we must update the type of each `Case` with its
--   new, possibly updated type. See:
--   https://github.com/ucsd-progsys/liquidhaskell/pull/752#issuecomment-228946210

fixCase :: CoreExpr -> Var -> Type -> ListNE (Alt Var) -> CoreExpr
fixCase :: CoreExpr -> Var -> Type -> [Alt Var] -> CoreExpr
fixCase CoreExpr
e Var
x Type
_t [Alt Var]
cs' = forall b. Expr b -> b -> Type -> [Alt b] -> Expr b
Case CoreExpr
e Var
x Type
t' [Alt Var]
cs'
  where
    t' :: Type
t'            = CoreExpr -> Type
Ghc.exprType CoreExpr
body
    Alt AltCon
_ [Var]
_ CoreExpr
body  = Alt Var
c
    Alt Var
c:[Alt Var]
_           = [Alt Var]
cs'

{-@  type ListNE a = {v:[a] | len v > 0} @-}
type ListNE a = [a]

replaceIrrefutPat :: Type -> CoreExpr -> CoreExpr
replaceIrrefutPat :: Type -> CoreExpr -> CoreExpr
replaceIrrefutPat Type
t (App (Lam Var
z CoreExpr
e) CoreExpr
eVoid)
  | Just CoreExpr
e' <- Type -> RewriteRule
replaceIrrefutPat' Type
t CoreExpr
e
  = forall b. Expr b -> Expr b -> Expr b
App (forall b. b -> Expr b -> Expr b
Lam Var
z CoreExpr
e') CoreExpr
eVoid

replaceIrrefutPat Type
t CoreExpr
e
  | Just CoreExpr
e' <- Type -> RewriteRule
replaceIrrefutPat' Type
t CoreExpr
e
  = CoreExpr
e'

replaceIrrefutPat Type
_ CoreExpr
e
  = CoreExpr
e

replaceIrrefutPat' :: Type -> CoreExpr -> Maybe CoreExpr
replaceIrrefutPat' :: Type -> RewriteRule
replaceIrrefutPat' Type
t CoreExpr
e
  | (Var Var
x, CoreExpr
rep:CoreExpr
_:[CoreExpr]
args) <- forall b. Expr b -> (Expr b, [Expr b])
collectArgs CoreExpr
e
  , Var -> Bool
isIrrefutErrorVar Var
x
  = forall a. a -> Maybe a
Just (CoreExpr -> [CoreExpr] -> CoreExpr
Ghc.mkCoreApps (forall b. Var -> Expr b
Var Var
x) (CoreExpr
rep forall a. a -> [a] -> [a]
: forall b. Type -> Expr b
Type Type
t forall a. a -> [a] -> [a]
: [CoreExpr]
args))
  | Bool
otherwise
  = forall a. Maybe a
Nothing

isIrrefutErrorVar :: Var -> Bool
-- isIrrefutErrorVar _x = False -- Ghc.iRREFUT_PAT_ERROR_ID == x -- TODO:GHC-863
isIrrefutErrorVar :: Var -> Bool
isIrrefutErrorVar Var
x = Var
x forall a. Eq a => a -> a -> Bool
== Var
Ghc.pAT_ERROR_ID

--------------------------------------------------------------------------------
-- | `substTuple xs ys e'` returns e' [y1 := x1,...,yn := xn]
--------------------------------------------------------------------------------
substTuple :: [Var] -> [Var] -> CoreExpr -> CoreExpr
substTuple :: [Var] -> [Var] -> CoreExpr -> CoreExpr
substTuple [Var]
xs [Var]
ys = HashMap Var Var -> CoreExpr -> CoreExpr
substExpr (forall k v. (Eq k, Hashable k) => [(k, v)] -> HashMap k v
M.fromList forall a b. (a -> b) -> a -> b
$ forall a b. [a] -> [b] -> [(a, b)]
zip [Var]
ys [Var]
xs)

--------------------------------------------------------------------------------
-- | `isVarTup xs e` returns `Just ys` if e == (y1, ... , yn) and xi ~ yi
--------------------------------------------------------------------------------

isVarTup :: [Var] -> CoreExpr -> Maybe [Var]
isVarTup :: [Var] -> CoreExpr -> Maybe [Var]
isVarTup [Var]
xs CoreExpr
e
  | Just [Var]
ys <- CoreExpr -> Maybe [Var]
isTuple CoreExpr
e
  , [Var] -> [Var] -> Bool
eqVars [Var]
xs [Var]
ys        = forall a. a -> Maybe a
Just [Var]
ys
isVarTup [Var]
_ CoreExpr
_             = forall a. Maybe a
Nothing

eqVars :: [Var] -> [Var] -> Bool
eqVars :: [Var] -> [Var] -> Bool
eqVars [Var]
xs [Var]
ys = {- F.tracepp ("eqVars: " ++ show xs' ++ show ys') -} [String]
xs' forall a. Eq a => a -> a -> Bool
== [String]
ys'
  where
    xs' :: [String]
xs' = {- F.symbol -} forall a. Show a => a -> String
show forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [Var]
xs
    ys' :: [String]
ys' = {- F.symbol -} forall a. Show a => a -> String
show forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [Var]
ys

isTuple :: CoreExpr -> Maybe [Var]
isTuple :: CoreExpr -> Maybe [Var]
isTuple CoreExpr
e
  | (Var Var
t, [CoreExpr]
es) <- forall b. Expr b -> (Expr b, [Expr b])
collectArgs CoreExpr
e
  , Var -> Bool
isTupleId Var
t
  , Just [Var]
xs     <- forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM CoreExpr -> Maybe Var
isVar (forall a. [a] -> [a]
secondHalf [CoreExpr]
es)
  = forall a. a -> Maybe a
Just [Var]
xs
  | Bool
otherwise
  = forall a. Maybe a
Nothing

isVar :: CoreExpr -> Maybe Var
isVar :: CoreExpr -> Maybe Var
isVar (Var Var
x) = forall a. a -> Maybe a
Just Var
x
isVar CoreExpr
_       = forall a. Maybe a
Nothing

secondHalf :: [a] -> [a]
secondHalf :: forall a. [a] -> [a]
secondHalf [a]
xs = forall a. Int -> [a] -> [a]
drop (Int
n forall a. Integral a => a -> a -> a
`div` Int
2) [a]
xs
  where
    n :: Int
n         = forall (t :: * -> *) a. Foldable t => t a -> Int
length [a]
xs