{-# 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 (msum)
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
  = (CoreBind -> CoreBind) -> [CoreBind] -> [CoreBind]
forall a b. (a -> b) -> [a] -> [b]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (CoreBind -> CoreBind
normalizeTuples 
       (CoreBind -> CoreBind)
-> (CoreBind -> CoreBind) -> CoreBind -> CoreBind
forall b c a. (b -> c) -> (a -> b) -> a -> c
. RewriteRule -> CoreBind -> CoreBind
rewriteBindWith RewriteRule
undollar 
       (CoreBind -> CoreBind)
-> (CoreBind -> CoreBind) -> CoreBind -> CoreBind
forall b c a. (b -> c) -> (a -> b) -> a -> c
. RewriteRule -> CoreBind -> CoreBind
rewriteBindWith RewriteRule
tidyTuples 
       (CoreBind -> CoreBind)
-> (CoreBind -> CoreBind) -> CoreBind -> CoreBind
forall b c a. (b -> c) -> (a -> b) -> a -> c
. RewriteRule -> CoreBind -> CoreBind
rewriteBindWith RewriteRule
simplifyPatTuple)
  | Bool
otherwise
  = [CoreBind] -> [CoreBind]
forall a. a -> a
id

simplifyCore :: Config -> Bool
simplifyCore :: Config -> Bool
simplifyCore = Bool -> Bool
not (Bool -> Bool) -> (Config -> Bool) -> Config -> Bool
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 Var -> Unique -> Bool
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
     = RewriteRule
forall a. a -> Maybe a
Just RewriteRule -> RewriteRule
forall a b. (a -> b) -> a -> b
$ CoreExpr -> CoreExpr -> CoreExpr
forall b. Expr b -> Expr b -> Expr b
App CoreExpr
f CoreExpr
a 
    go (Tick CoreTickish
t CoreExpr
e)
      = CoreTickish -> CoreExpr -> CoreExpr
forall b. CoreTickish -> Expr b -> Expr b
Tick CoreTickish
t (CoreExpr -> CoreExpr) -> Maybe CoreExpr -> Maybe CoreExpr
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
           RewriteRule
forall a. a -> Maybe a
forall (m :: * -> *) a. Monad m => a -> m a
return RewriteRule -> RewriteRule
forall a b. (a -> b) -> a -> b
$ CoreBind -> CoreExpr -> CoreExpr
forall b. Bind b -> Expr b -> Expr b
Let (Var -> CoreExpr -> CoreBind
forall b. b -> Expr b -> Bind b
NonRec Var
x CoreExpr
ex') CoreExpr
e'
    go (Let (Rec [(Var, CoreExpr)]
bes) CoreExpr
e)
      = CoreBind -> CoreExpr -> CoreExpr
forall b. Bind b -> Expr b -> Expr b
Let (CoreBind -> CoreExpr -> CoreExpr)
-> Maybe CoreBind -> Maybe (CoreExpr -> CoreExpr)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ([(Var, CoreExpr)] -> CoreBind
forall b. [(b, Expr b)] -> Bind b
Rec ([(Var, CoreExpr)] -> CoreBind)
-> Maybe [(Var, CoreExpr)] -> Maybe CoreBind
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ((Var, CoreExpr) -> Maybe (Var, CoreExpr))
-> [(Var, CoreExpr)] -> Maybe [(Var, CoreExpr)]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [b]
mapM (Var, CoreExpr) -> Maybe (Var, CoreExpr)
goRec [(Var, CoreExpr)]
bes) Maybe (CoreExpr -> CoreExpr) -> Maybe CoreExpr -> Maybe CoreExpr
forall a b. Maybe (a -> b) -> Maybe a -> Maybe b
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)
      = CoreExpr -> Var -> Type -> [Alt Var] -> CoreExpr
forall b. Expr b -> b -> Type -> [Alt b] -> Expr b
Case CoreExpr
e Var
x Type
t ([Alt Var] -> CoreExpr) -> Maybe [Alt Var] -> Maybe CoreExpr
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (Alt Var -> Maybe (Alt Var)) -> [Alt Var] -> Maybe [Alt Var]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [b]
mapM Alt Var -> Maybe (Alt Var)
goAlt [Alt Var]
alts
    go (App CoreExpr
e1 CoreExpr
e2)
      = CoreExpr -> CoreExpr -> CoreExpr
forall b. Expr b -> Expr b -> Expr b
App (CoreExpr -> CoreExpr -> CoreExpr)
-> Maybe CoreExpr -> Maybe (CoreExpr -> CoreExpr)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> RewriteRule
go CoreExpr
e1 Maybe (CoreExpr -> CoreExpr) -> Maybe CoreExpr -> Maybe CoreExpr
forall a b. Maybe (a -> b) -> Maybe a -> Maybe b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> RewriteRule
go CoreExpr
e2
    go (Lam Var
x CoreExpr
e)
      = Var -> CoreExpr -> CoreExpr
forall b. b -> Expr b -> Expr b
Lam Var
x (CoreExpr -> CoreExpr) -> Maybe CoreExpr -> Maybe CoreExpr
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> RewriteRule
go CoreExpr
e
    go (Cast CoreExpr
e CoercionR
c)
      = (CoreExpr -> CoercionR -> CoreExpr
forall b. Expr b -> CoercionR -> Expr b
`Cast` CoercionR
c) (CoreExpr -> CoreExpr) -> Maybe CoreExpr -> Maybe CoreExpr
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> RewriteRule
go CoreExpr
e
    go CoreExpr
e
      = RewriteRule
forall a. a -> Maybe a
forall (m :: * -> *) a. Monad m => a -> m a
return CoreExpr
e

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

    goRec :: (Var, CoreExpr) -> f (Var, CoreExpr)
goRec (Var
x, CoreExpr
e)
      = (Var
x,) (CoreExpr -> (Var, CoreExpr)) -> f CoreExpr -> f (Var, CoreExpr)
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)
      = AltCon -> [Var] -> CoreExpr -> Alt Var
forall b. AltCon -> [b] -> Expr b -> Alt b
Alt AltCon
c [Var]
bs (CoreExpr -> Alt Var) -> f CoreExpr -> f (Alt Var)
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 <- m [((AltCon, b), [Var])]
forall s (m :: * -> *). MonadState s m => m s
get
           case (AltCon, b) -> [((AltCon, b), [Var])] -> Maybe [Var]
forall a b. Eq a => a -> [(a, b)] -> Maybe b
L.lookup (AltCon
c,b
v) [((AltCon, b), [Var])]
m of
            Just [Var]
bs' -> Alt Var -> m (Alt Var)
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return (AltCon -> [Var] -> CoreExpr -> Alt Var
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 (Var -> Var) -> [Var] -> [Var]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [Var]
bs
                           ([((AltCon, b), [Var])] -> [((AltCon, b), [Var])]) -> m ()
forall s (m :: * -> *). MonadState s m => (s -> s) -> m ()
modify (((AltCon
c,b
v),[Var]
bs')((AltCon, b), [Var])
-> [((AltCon, b), [Var])] -> [((AltCon, b), [Var])]
forall a. a -> [a] -> [a]
:)
                           Alt Var -> m (Alt Var)
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return (AltCon -> [Var] -> CoreExpr -> Alt Var
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
  = Var -> CoreExpr -> CoreBind
forall b. b -> Expr b -> Bind b
NonRec Var
x (CoreExpr -> CoreBind) -> CoreExpr -> CoreBind
forall a b. (a -> b) -> a -> b
$ CoreExpr -> CoreExpr
go CoreExpr
e
  | Rec [(Var, CoreExpr)]
xes <- CoreBind
cb
  = let ([Var]
xs,[CoreExpr]
es) = [(Var, CoreExpr)] -> ([Var], [CoreExpr])
forall a b. [(a, b)] -> ([a], [b])
unzip [(Var, CoreExpr)]
xes in
    [(Var, CoreExpr)] -> CoreBind
forall b. [(b, Expr b)] -> Bind b
Rec ([(Var, CoreExpr)] -> CoreBind) -> [(Var, CoreExpr)] -> CoreBind
forall a b. (a -> b) -> a -> b
$ [Var] -> [CoreExpr] -> [(Var, CoreExpr)]
forall a b. [a] -> [b] -> [(a, b)]
zip [Var]
xs (CoreExpr -> CoreExpr
go (CoreExpr -> CoreExpr) -> [CoreExpr] -> [CoreExpr]
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 Var -> [Var] -> Bool
forall a. Eq a => a -> [a] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [Var]
vs
      = CoreBind -> CoreExpr -> CoreExpr
forall b. Bind b -> Expr b -> Expr b
Let (Var -> CoreExpr -> CoreBind
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)
      = CoreBind -> CoreExpr -> CoreExpr
forall b. Bind b -> Expr b -> Expr b
Let (Var -> CoreExpr -> CoreBind
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)
      = CoreBind -> CoreExpr -> CoreExpr
forall b. Bind b -> Expr b -> Expr b
Let ([(Var, CoreExpr)] -> CoreBind
forall b. [(b, Expr b)] -> Bind b
Rec ((CoreExpr -> CoreExpr) -> (Var, CoreExpr) -> (Var, CoreExpr)
forall b c a. (b -> c) -> (a, b) -> (a, c)
mapSnd CoreExpr -> CoreExpr
go ((Var, CoreExpr) -> (Var, CoreExpr))
-> [(Var, CoreExpr)] -> [(Var, CoreExpr)]
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)
      = CoreExpr -> CoreExpr -> CoreExpr
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)
      = Var -> CoreExpr -> CoreExpr
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)
      = CoreExpr -> Var -> Type -> [Alt Var] -> CoreExpr
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') -> AltCon -> [Var] -> CoreExpr -> Alt Var
forall b. AltCon -> [b] -> Expr b -> Alt b
Alt AltCon
c [Var]
bs (CoreExpr -> CoreExpr
go CoreExpr
e')) (Alt Var -> Alt Var) -> [Alt Var] -> [Alt Var]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [Alt Var]
alt)
    go (Cast CoreExpr
e CoercionR
c)
      = CoreExpr -> CoercionR -> CoreExpr
forall b. Expr b -> CoercionR -> Expr b
Cast (CoreExpr -> CoreExpr
go CoreExpr
e) CoercionR
c
    go (Tick CoreTickish
t CoreExpr
e)
      = CoreTickish -> CoreExpr -> CoreExpr
forall b. CoreTickish -> Expr b -> Expr b
Tick CoreTickish
t (CoreExpr -> CoreExpr
go CoreExpr
e)
    go (Type Type
t)
      = Type -> CoreExpr
forall b. Type -> Expr b
Type Type
t
    go (Coercion CoercionR
c)
      = CoercionR -> CoreExpr
forall b. CoercionR -> Expr b
Coercion CoercionR
c
    go (Lit Literal
l)
      = Literal -> CoreExpr
forall b. Literal -> Expr b
Lit Literal
l
    go (Var Var
x)
      = Var -> CoreExpr
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) = Var -> CoreExpr -> CoreBind
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)    = [(Var, CoreExpr)] -> CoreBind
forall b. [(b, Expr b)] -> Bind b
Rec    ((CoreExpr -> CoreExpr) -> (Var, CoreExpr) -> (Var, CoreExpr)
forall b c a. (b -> c) -> (a, b) -> (a, c)
mapSnd (RewriteRule -> CoreExpr -> CoreExpr
rewriteWith RewriteRule
r) ((Var, CoreExpr) -> (Var, CoreExpr))
-> [(Var, CoreExpr)] -> [(Var, CoreExpr)]
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 (CoreExpr -> CoreExpr)
-> (CoreExpr -> CoreExpr) -> CoreExpr -> CoreExpr
forall b c a. (b -> c) -> (a -> b) -> a -> c
. CoreExpr -> CoreExpr
step
    txTop :: CoreExpr -> CoreExpr
txTop CoreExpr
e              = CoreExpr -> Maybe CoreExpr -> CoreExpr
forall a. a -> Maybe a -> a
fromMaybe CoreExpr
e (RewriteRule
tx CoreExpr
e)
    goB :: CoreBind -> CoreBind
goB (Rec [(Var, CoreExpr)]
xes)        = [(Var, CoreExpr)] -> CoreBind
forall b. [(b, Expr b)] -> Bind b
Rec         ((CoreExpr -> CoreExpr) -> (Var, CoreExpr) -> (Var, CoreExpr)
forall b c a. (b -> c) -> (a, b) -> (a, c)
mapSnd CoreExpr -> CoreExpr
go ((Var, CoreExpr) -> (Var, CoreExpr))
-> [(Var, CoreExpr)] -> [(Var, CoreExpr)]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [(Var, CoreExpr)]
xes)
    goB (NonRec Var
x CoreExpr
e)     = Var -> CoreExpr -> CoreBind
forall b. b -> Expr b -> Bind b
NonRec Var
x    (CoreExpr -> CoreExpr
go CoreExpr
e)
    step :: CoreExpr -> CoreExpr
step (Let CoreBind
b CoreExpr
e)       = CoreBind -> CoreExpr -> CoreExpr
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')      = CoreExpr -> CoreExpr -> CoreExpr
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)       = Var -> CoreExpr -> CoreExpr
forall b. b -> Expr b -> Expr b
Lam Var
x       (CoreExpr -> CoreExpr
go CoreExpr
e)
    step (Cast CoreExpr
e CoercionR
c)      = CoreExpr -> CoercionR -> CoreExpr
forall b. Expr b -> CoercionR -> Expr b
Cast (CoreExpr -> CoreExpr
go CoreExpr
e) CoercionR
c
    step (Tick CoreTickish
t CoreExpr
e)      = CoreTickish -> CoreExpr -> CoreExpr
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) = CoreExpr -> Var -> Type -> [Alt Var] -> CoreExpr
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') -> AltCon -> [Var] -> CoreExpr -> Alt Var
forall b. AltCon -> [b] -> Expr b -> Alt b
Alt AltCon
c [Var]
bs (CoreExpr -> CoreExpr
go CoreExpr
e')) (Alt Var -> Alt Var) -> [Alt Var] -> [Alt Var]
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
  , (() :: Constraint) => CoreExpr -> Type
CoreExpr -> Type
Ghc.exprType CoreExpr
e' Type -> Type -> Bool
forall a. Eq a => a -> a -> Bool
== (() :: Constraint) => CoreExpr -> Type
CoreExpr -> Type
Ghc.exprType CoreExpr
e
  = RewriteRule
forall a. a -> Maybe a
Just CoreExpr
e'
  | Bool
otherwise
  = Maybe CoreExpr
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
  = RewriteRule
forall a. a -> Maybe a
Just RewriteRule -> RewriteRule
forall a b. (a -> b) -> a -> b
$ CoreBind -> CoreExpr -> CoreExpr
forall b. Bind b -> Expr b -> Expr b
Let (Var -> CoreExpr -> CoreBind
forall b. b -> Expr b -> Bind b
NonRec Var
cb CoreExpr
expr) (CoreExpr -> CoreExpr) -> CoreExpr -> CoreExpr
forall a b. (a -> b) -> a -> b
$ (CoreExpr -> (Var, CoreExpr) -> CoreExpr)
-> CoreExpr -> [(Var, CoreExpr)] -> CoreExpr
forall b a. (b -> a -> b) -> b -> [a] -> b
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl (\CoreExpr
e (Var
x, CoreExpr
ex) -> CoreBind -> CoreExpr -> CoreExpr
forall b. Bind b -> Expr b -> Expr b
Let (Var -> CoreExpr -> CoreBind
forall b. b -> Expr b -> Bind b
NonRec Var
x CoreExpr
ex) CoreExpr
e) CoreExpr
e' ([(Var, CoreExpr)] -> [(Var, CoreExpr)]
forall a. [a] -> [a]
reverse ([(Var, CoreExpr)] -> [(Var, CoreExpr)])
-> [(Var, CoreExpr)] -> [(Var, CoreExpr)]
forall a b. (a -> b) -> a -> b
$ [(Var, CoreExpr)] -> [(Var, CoreExpr)]
forall {a} {b}. [(a, Expr b)] -> [(a, Expr b)]
go ([(Var, CoreExpr)] -> [(Var, CoreExpr)])
-> [(Var, CoreExpr)] -> [(Var, CoreExpr)]
forall a b. (a -> b) -> a -> b
$ [(Var, CoreExpr)] -> [(Var, CoreExpr)]
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 = Expr b -> [b]
forall {a}. Expr a -> [a]
grapBinds Expr b
e in (Expr b -> Expr b) -> (a, Expr b) -> (a, Expr b)
forall b c a. (b -> c) -> (a, b) -> (a, c)
mapSnd ([b] -> Expr b -> Expr b
forall {b}. [b] -> Expr b -> Expr b
replaceBinds [b]
bs) ((a, Expr b) -> (a, Expr b)) -> [(a, Expr b)] -> [(a, Expr b)]
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) = Expr b -> b -> Type -> [Alt b] -> Expr b
forall b. Expr b -> b -> Type -> [Alt b] -> Expr b
Case Expr b
c b
x Type
t ([b] -> Alt b -> Alt b
forall {b}. [b] -> Alt b -> Alt b
replaceBindsAlt [b]
bs (Alt b -> Alt b) -> [Alt b] -> [Alt b]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [Alt b]
alt)
    replaceBinds [b]
bs (Tick CoreTickish
t Expr b
e)       = CoreTickish -> Expr b -> Expr b
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)     = AltCon -> [b] -> Expr b -> Alt b
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) = [Alt a] -> [a]
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 Int -> Int -> Bool
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          = (Var, CoreExpr) -> Var
forall a b. (a, b) -> a
fst ((Var, CoreExpr) -> Var) -> [(Var, CoreExpr)] -> [Var]
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
_
  = Maybe 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
  = (Int, [Type]) -> Maybe (Int, [Type])
forall a. a -> Maybe a
Just ([Type] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [Type]
ts, [Type]
ts)
  | Bool
otherwise
  = Maybe (Int, [Type])
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 Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
< Int
2     = Maybe ([(Var, CoreExpr)], CoreExpr)
forall a. Maybe a
Nothing
  | Bool
otherwise = {- mapFst reverse <$> -} Int -> CoreExpr -> Maybe ([(Var, CoreExpr)], CoreExpr)
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                      = ([(a, Expr a)], Expr a) -> Maybe ([(a, Expr a)], Expr a)
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
nt -> t -> t
forall a. Num a => a -> a -> a
-t
1) Expr a
e'
                                       ([(a, Expr a)], Expr a) -> Maybe ([(a, Expr a)], Expr a)
forall a. a -> Maybe a
Just ((a
x,Expr a
e) (a, Expr a) -> [(a, Expr a)] -> [(a, Expr a)]
forall a. a -> [a] -> [a]
: [(a, Expr a)]
xes, Expr a
e'')
      go t
_ Expr a
_                      = Maybe ([(a, Expr a)], 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 Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
tN
                  Bool -> Bool -> Bool
&& ((Type, Type) -> Bool) -> [(Type, Type)] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all ((Type -> Type -> Bool) -> (Type, Type) -> Bool
forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry Type -> Type -> Bool
eqType) (String -> [Type] -> [Type] -> [(Type, Type)]
forall t t1. String -> [t] -> [t1] -> [(t, t1)]
safeZipWithError String
forall {a}. IsString a => a
msg [Type]
xts [Type]
ts)
                  Bool -> Bool -> Bool
&& (CoreExpr -> Bool) -> [CoreExpr] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all CoreExpr -> Bool
isProjection [CoreExpr]
es
  where
    xN :: Int
xN            = [(Var, CoreExpr)] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [(Var, CoreExpr)]
xes
    tN :: Int
tN            = [Type] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [Type]
ts
    xts :: [Type]
xts           = Var -> Type
Ghc.varType (Var -> Type) -> [Var] -> [Type]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [Var]
xs
    ([Var]
xs, [CoreExpr]
es)      = [(Var, CoreExpr)] -> ([Var], [CoreExpr])
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 = [Var] -> Maybe [Var]
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
_)     = Maybe [Var]
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)          = [Maybe [Var]] -> Maybe [Var]
forall (t :: * -> *) (m :: * -> *) a.
(Foldable t, MonadPlus m) =>
t (m a) -> m a
msum (Alt Var -> Maybe [Var]
stepA (Alt Var -> Maybe [Var]) -> [Alt Var] -> [Maybe [Var]]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [Alt Var]
cs)
    go CoreExpr
_                        = Maybe [Var]
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'                          = (() :: Constraint) => CoreExpr -> Type
CoreExpr -> Type
Ghc.exprType CoreExpr
ce'
    stepE :: RewriteRule
stepE CoreExpr
e
     | Just [Var]
xs <- [Var] -> CoreExpr -> Maybe [Var]
isVarTup [Var]
ys CoreExpr
e = RewriteRule
forall a. a -> Maybe a
Just RewriteRule -> RewriteRule
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)  = Alt Var -> Maybe (Alt Var)
forall a. a -> Maybe a
Just (AltCon -> [Var] -> CoreExpr -> Alt Var
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)          = AltCon -> [Var] -> CoreExpr -> Alt Var
forall b. AltCon -> [b] -> Expr b -> Alt b
Alt AltCon
c [Var]
xs   (CoreExpr -> Alt Var) -> Maybe CoreExpr -> Maybe (Alt Var)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> RewriteRule
stepE CoreExpr
e
    go :: RewriteRule
go (Let CoreBind
b CoreExpr
e)                = CoreBind -> CoreExpr -> CoreExpr
forall b. Bind b -> Expr b -> Expr b
Let CoreBind
b      (CoreExpr -> CoreExpr) -> Maybe CoreExpr -> Maybe CoreExpr
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 ([Alt Var] -> CoreExpr) -> Maybe [Alt Var] -> Maybe CoreExpr
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (Alt Var -> Maybe (Alt Var)) -> [Alt Var] -> Maybe [Alt Var]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [b]
mapM Alt Var -> Maybe (Alt Var)
stepA [Alt Var]
cs
    go CoreExpr
_                        = Maybe 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 String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
" " String -> String -> 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 " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Var -> String
_showVar Var
x String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
" = " String -> String -> String
forall a. [a] -> [a] -> [a]
++ CoreExpr -> String
show' CoreExpr
ex String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
"\nIN " String -> String -> String
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 " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Var -> String
_showVar Var
x String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
" = " String -> String -> String
forall a. [a] -> [a] -> [a]
++ CoreExpr -> String
show' CoreExpr
e String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
" OF " String -> String -> String
forall a. [a] -> [a] -> [a]
++ [String] -> String
unlines (Alt Var -> String
showAlt' (Alt Var -> String) -> [Alt Var] -> [String]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [Alt Var]
alt)
    show' CoreExpr
e           = CoreExpr -> String
forall a. Outputable a => a -> String
showPpr CoreExpr
e

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

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

_errorSkip :: String -> a -> b
_errorSkip :: forall a b. String -> a -> b
_errorSkip String
x a
_ = String -> b
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' = CoreExpr -> Var -> Type -> [Alt Var] -> CoreExpr
forall b. Expr b -> b -> Type -> [Alt b] -> Expr b
Case CoreExpr
e Var
x Type
t' [Alt Var]
cs'
  where
    t' :: Type
t'            = (() :: Constraint) => CoreExpr -> Type
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
  = CoreExpr -> CoreExpr -> CoreExpr
forall b. Expr b -> Expr b -> Expr b
App (Var -> CoreExpr -> CoreExpr
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) <- CoreExpr -> (CoreExpr, [CoreExpr])
forall b. Expr b -> (Expr b, [Expr b])
collectArgs CoreExpr
e
  , Var -> Bool
isIrrefutErrorVar Var
x
  = RewriteRule
forall a. a -> Maybe a
Just (CoreExpr -> [CoreExpr] -> CoreExpr
Ghc.mkCoreApps (Var -> CoreExpr
forall b. Var -> Expr b
Var Var
x) (CoreExpr
rep CoreExpr -> [CoreExpr] -> [CoreExpr]
forall a. a -> [a] -> [a]
: Type -> CoreExpr
forall b. Type -> Expr b
Type Type
t CoreExpr -> [CoreExpr] -> [CoreExpr]
forall a. a -> [a] -> [a]
: [CoreExpr]
args))
  | Bool
otherwise
  = Maybe CoreExpr
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 Var -> Var -> Bool
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 ([(Var, Var)] -> HashMap Var Var
forall k v. (Eq k, Hashable k) => [(k, v)] -> HashMap k v
M.fromList ([(Var, Var)] -> HashMap Var Var)
-> [(Var, Var)] -> HashMap Var Var
forall a b. (a -> b) -> a -> b
$ [Var] -> [Var] -> [(Var, Var)]
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        = [Var] -> Maybe [Var]
forall a. a -> Maybe a
Just [Var]
ys
isVarTup [Var]
_ CoreExpr
_             = Maybe [Var]
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' [String] -> [String] -> Bool
forall a. Eq a => a -> a -> Bool
== [String]
ys'
  where
    xs' :: [String]
xs' = {- F.symbol -} Var -> String
forall a. Show a => a -> String
show (Var -> String) -> [Var] -> [String]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [Var]
xs
    ys' :: [String]
ys' = {- F.symbol -} Var -> String
forall a. Show a => a -> String
show (Var -> String) -> [Var] -> [String]
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) <- CoreExpr -> (CoreExpr, [CoreExpr])
forall b. Expr b -> (Expr b, [Expr b])
collectArgs CoreExpr
e
  , Var -> Bool
isTupleId Var
t
  , Just [Var]
xs     <- (CoreExpr -> Maybe Var) -> [CoreExpr] -> Maybe [Var]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [b]
mapM CoreExpr -> Maybe Var
isVar ([CoreExpr] -> [CoreExpr]
forall a. [a] -> [a]
secondHalf [CoreExpr]
es)
  = [Var] -> Maybe [Var]
forall a. a -> Maybe a
Just [Var]
xs
  | Bool
otherwise
  = Maybe [Var]
forall a. Maybe a
Nothing

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

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