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

-- | 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           CoreSyn
import           Language.Haskell.Liquid.GHC.API
import           Language.Haskell.Liquid.GHC.TypeRep ()
import qualified CoreUtils
import qualified Var
import qualified MkCore
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, mapThd3, 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 (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
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

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

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

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

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



normalizeTuples :: CoreBind -> CoreBind
normalizeTuples :: CoreBind -> CoreBind
normalizeTuples CoreBind
b 
  | NonRec Id
x CoreExpr
e <- CoreBind
b 
  = Id -> CoreExpr -> CoreBind
forall b. b -> Expr b -> Bind b
NonRec Id
x (CoreExpr -> CoreBind) -> CoreExpr -> CoreBind
forall a b. (a -> b) -> a -> b
$ CoreExpr -> CoreExpr
go CoreExpr
e 
  | Rec [(Id, CoreExpr)]
xes <- CoreBind
b 
  = let ([Id]
xs,[CoreExpr]
es) = [(Id, CoreExpr)] -> ([Id], [CoreExpr])
forall a b. [(a, b)] -> ([a], [b])
unzip [(Id, CoreExpr)]
xes in 
    [(Id, CoreExpr)] -> CoreBind
forall b. [(b, Expr b)] -> Bind b
Rec ([(Id, CoreExpr)] -> CoreBind) -> [(Id, CoreExpr)] -> CoreBind
forall a b. (a -> b) -> a -> b
$ [Id] -> [CoreExpr] -> [(Id, CoreExpr)]
forall a b. [a] -> [b] -> [(a, b)]
zip [Id]
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 Id
x CoreExpr
ex) CoreExpr
e)
      | Case CoreExpr
_ Id
_ Type
_ [Alt Id]
alts  <- CoreExpr -> CoreExpr
unTickExpr CoreExpr
ex 
      , [(AltCon
_, [Id]
vs, Var Id
z)] <- [Alt Id]
alts 
      , Id
z Id -> [Id] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [Id]
vs
      = CoreBind -> CoreExpr -> CoreExpr
forall b. Bind b -> Expr b -> Expr b
Let (Id -> CoreExpr -> CoreBind
forall b. b -> Expr b -> Bind b
NonRec Id
z (CoreExpr -> CoreExpr
go CoreExpr
ex)) ([Id] -> [Id] -> CoreExpr -> CoreExpr
substTuple [Id
z] [Id
x] (CoreExpr -> CoreExpr
go CoreExpr
e)) 
    go (Let (NonRec Id
x CoreExpr
ex) CoreExpr
e)
      = CoreBind -> CoreExpr -> CoreExpr
forall b. Bind b -> Expr b -> Expr b
Let (Id -> CoreExpr -> CoreBind
forall b. b -> Expr b -> Bind b
NonRec Id
x (CoreExpr -> CoreExpr
go CoreExpr
ex)) (CoreExpr -> CoreExpr
go CoreExpr
e)
    go (Let (Rec [(Id, CoreExpr)]
xes) CoreExpr
e)
      = CoreBind -> CoreExpr -> CoreExpr
forall b. Bind b -> Expr b -> Expr b
Let ([(Id, CoreExpr)] -> CoreBind
forall b. [(b, Expr b)] -> Bind b
Rec ((CoreExpr -> CoreExpr) -> (Id, CoreExpr) -> (Id, CoreExpr)
forall b c a. (b -> c) -> (a, b) -> (a, c)
mapSnd CoreExpr -> CoreExpr
go ((Id, CoreExpr) -> (Id, CoreExpr))
-> [(Id, CoreExpr)] -> [(Id, CoreExpr)]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [(Id, 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 Id
x CoreExpr
e)
      = Id -> CoreExpr -> CoreExpr
forall b. b -> Expr b -> Expr b
Lam Id
x (CoreExpr -> CoreExpr
go CoreExpr
e)
    go (Case CoreExpr
e Id
b Type
t [Alt Id]
alt)
      = CoreExpr -> Id -> Type -> [Alt Id] -> CoreExpr
forall b. Expr b -> b -> Type -> [Alt b] -> Expr b
Case (CoreExpr -> CoreExpr
go CoreExpr
e) Id
b Type
t ((CoreExpr -> CoreExpr) -> Alt Id -> Alt Id
forall t t3 t1 t2. (t -> t3) -> (t1, t2, t) -> (t1, t2, t3)
mapThd3 CoreExpr -> CoreExpr
go (Alt Id -> Alt Id) -> [Alt Id] -> [Alt Id]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [Alt Id]
alt)
    go (Cast CoreExpr
e Coercion
c)
      = CoreExpr -> Coercion -> CoreExpr
forall b. Expr b -> Coercion -> Expr b
Cast (CoreExpr -> CoreExpr
go CoreExpr
e) Coercion
c 
    go (Tick Tickish Id
t CoreExpr
e)
      = Tickish Id -> CoreExpr -> CoreExpr
forall b. Tickish Id -> Expr b -> Expr b
Tick Tickish Id
t (CoreExpr -> CoreExpr
go CoreExpr
e)
    go (Type Type
t)
      = Type -> CoreExpr
forall b. Type -> Expr b
Type Type
t 
    go (Coercion Coercion
c)
      = Coercion -> CoreExpr
forall b. Coercion -> Expr b
Coercion Coercion
c
    go (Lit Literal
l)
      = Literal -> CoreExpr
forall b. Literal -> Expr b
Lit Literal
l 
    go (Var Id
x)
      = Id -> CoreExpr
forall b. Id -> Expr b
Var Id
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 Id
x CoreExpr
e) = Id -> CoreExpr -> CoreBind
forall b. b -> Expr b -> Bind b
NonRec Id
x (RewriteRule -> CoreExpr -> CoreExpr
rewriteWith RewriteRule
r CoreExpr
e)
rewriteBindWith RewriteRule
r (Rec [(Id, CoreExpr)]
xes)    = [(Id, CoreExpr)] -> CoreBind
forall b. [(b, Expr b)] -> Bind b
Rec    ((CoreExpr -> CoreExpr) -> (Id, CoreExpr) -> (Id, CoreExpr)
forall b c a. (b -> c) -> (a, b) -> (a, c)
mapSnd (RewriteRule -> CoreExpr -> CoreExpr
rewriteWith RewriteRule
r) ((Id, CoreExpr) -> (Id, CoreExpr))
-> [(Id, CoreExpr)] -> [(Id, CoreExpr)]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [(Id, 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 [(Id, CoreExpr)]
xes)        = [(Id, CoreExpr)] -> CoreBind
forall b. [(b, Expr b)] -> Bind b
Rec         ((CoreExpr -> CoreExpr) -> (Id, CoreExpr) -> (Id, CoreExpr)
forall b c a. (b -> c) -> (a, b) -> (a, c)
mapSnd CoreExpr -> CoreExpr
go ((Id, CoreExpr) -> (Id, CoreExpr))
-> [(Id, CoreExpr)] -> [(Id, CoreExpr)]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [(Id, CoreExpr)]
xes)
    goB (NonRec Id
x CoreExpr
e)     = Id -> CoreExpr -> CoreBind
forall b. b -> Expr b -> Bind b
NonRec Id
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 Id
x CoreExpr
e)       = Id -> CoreExpr -> CoreExpr
forall b. b -> Expr b -> Expr b
Lam Id
x       (CoreExpr -> CoreExpr
go CoreExpr
e)
    step (Cast CoreExpr
e Coercion
c)      = CoreExpr -> Coercion -> CoreExpr
forall b. Expr b -> Coercion -> Expr b
Cast (CoreExpr -> CoreExpr
go CoreExpr
e) Coercion
c
    step (Tick Tickish Id
t CoreExpr
e)      = Tickish Id -> CoreExpr -> CoreExpr
forall b. Tickish Id -> Expr b -> Expr b
Tick Tickish Id
t      (CoreExpr -> CoreExpr
go CoreExpr
e)
    step (Case CoreExpr
e Id
x Type
t [Alt Id]
cs) = CoreExpr -> Id -> Type -> [Alt Id] -> CoreExpr
forall b. Expr b -> b -> Type -> [Alt b] -> Expr b
Case (CoreExpr -> CoreExpr
go CoreExpr
e) Id
x Type
t ((CoreExpr -> CoreExpr) -> Alt Id -> Alt Id
forall t t3 t1 t2. (t -> t3) -> (t1, t2, t) -> (t1, t2, t3)
mapThd3 CoreExpr -> CoreExpr
go (Alt Id -> Alt Id) -> [Alt Id] -> [Alt Id]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [Alt Id]
cs)
    step e :: CoreExpr
e@(Type Type
_)      = CoreExpr
e
    step e :: CoreExpr
e@(Lit Literal
_)       = CoreExpr
e
    step e :: CoreExpr
e@(Var Id
_)       = CoreExpr
e
    step e :: CoreExpr
e@(Coercion Coercion
_)  = 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 CoreUtils.exprType e == CoreUtils.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
CoreUtils.exprType CoreExpr
e' Type -> Type -> Bool
forall a. Eq a => a -> a -> Bool
== CoreExpr -> Type
CoreUtils.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 Id
x CoreExpr
e) CoreExpr
rest))
  | Just ([(Id, CoreExpr)]
yes, CoreExpr
e') <- Int -> CoreExpr -> Maybe ([(Id, 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 (Id -> CoreExpr -> CoreBind
forall b. b -> Expr b -> Bind b
NonRec Id
x CoreExpr
e) (CoreExpr -> CoreExpr) -> CoreExpr -> CoreExpr
forall a b. (a -> b) -> a -> b
$ (CoreExpr -> (Id, CoreExpr) -> CoreExpr)
-> CoreExpr -> [(Id, CoreExpr)] -> CoreExpr
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl (\CoreExpr
e (Id
x, CoreExpr
ex) -> CoreBind -> CoreExpr -> CoreExpr
forall b. Bind b -> Expr b -> Expr b
Let (Id -> CoreExpr -> CoreBind
forall b. b -> Expr b -> Bind b
NonRec Id
x CoreExpr
ex) CoreExpr
e) CoreExpr
e' (([(Id, CoreExpr)] -> [(Id, CoreExpr)]
forall a. [a] -> [a]
reverse ([(Id, CoreExpr)] -> [(Id, CoreExpr)])
-> [(Id, CoreExpr)] -> [(Id, CoreExpr)]
forall a b. (a -> b) -> a -> b
$ [(Id, CoreExpr)] -> [(Id, CoreExpr)]
forall a b. [(a, Expr b)] -> [(a, Expr b)]
go ([(Id, CoreExpr)] -> [(Id, CoreExpr)])
-> [(Id, CoreExpr)] -> [(Id, CoreExpr)]
forall a b. (a -> b) -> a -> b
$ [(Id, CoreExpr)] -> [(Id, CoreExpr)]
forall a. [a] -> [a]
reverse [(Id, 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 a b c. b -> (a, b, c) -> (a, b, c)
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 Tickish Id
t Expr b
e)       = Tickish Id -> Expr b -> Expr b
forall b. Tickish Id -> Expr b -> Expr b
Tick Tickish Id
t ([b] -> Expr b -> Expr b
replaceBinds [b]
bs Expr b
e)
    replaceBinds [b]
_ Expr b
e                 = Expr b
e
    replaceBindsAlt :: b -> (a, b, c) -> (a, b, c)
replaceBindsAlt b
bs (a
c, b
_, c
e)     = (a
c, b
bs, c
e)

    grapBinds :: Expr a -> [a]
grapBinds (Case Expr a
_ a
_ Type
_ [Alt a]
alt) = [Alt a] -> [a]
forall a a c. [(a, [a], c)] -> [a]
grapBinds' [Alt a]
alt
    grapBinds (Tick Tickish Id
_ Expr a
e) = Expr a -> [a]
grapBinds Expr a
e
    grapBinds Expr a
_ = []
    grapBinds' :: [(a, [a], c)] -> [a]
grapBinds' [] = []
    grapBinds' ((a
_,[a]
bs,c
_):[(a, [a], c)]
_) = [a]
bs

_tidyAlt Int
_ Maybe CoreExpr
e
  = Maybe CoreExpr
e

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

simplifyPatTuple CoreExpr
_
  = Maybe CoreExpr
forall a. Maybe a
Nothing

varTuple :: Var -> Maybe (Int, [Type])
varTuple :: Id -> Maybe (Int, [Type])
varTuple Id
x
  | TyConApp TyCon
c [Type]
ts <- Id -> Type
Var.varType Id
x
  , TyCon -> Bool
isTupleTyCon TyCon
c
  = (Int, [Type]) -> Maybe (Int, [Type])
forall a. a -> Maybe a
Just ([Type] -> 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 ([(Id, CoreExpr)], CoreExpr)
takeBinds Int
n CoreExpr
e
  | Int
n Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
< Int
2     = Maybe ([(Id, CoreExpr)], CoreExpr)
forall a. Maybe a
Nothing
  | Bool
otherwise = {- mapFst reverse <$> -} Int -> CoreExpr -> Maybe ([(Id, CoreExpr)], CoreExpr)
forall t a.
(Eq t, Num t) =>
t -> Expr a -> Maybe ([(a, Expr a)], Expr a)
go Int
n CoreExpr
e
    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 :: [(Id, CoreExpr)] -> [Type] -> Bool
matchTypes [(Id, 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 p. IsString p => p
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            = [(Id, CoreExpr)] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [(Id, CoreExpr)]
xes
    tN :: Int
tN            = [Type] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [Type]
ts
    xts :: [Type]
xts           = Id -> Type
Var.varType (Id -> Type) -> [Id] -> [Type]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [Id]
xs
    ([Id]
xs, [CoreExpr]
es)      = [(Id, CoreExpr)] -> ([Id], [CoreExpr])
forall a b. [(a, b)] -> ([a], [b])
unzip [(Id, CoreExpr)]
xes
    msg :: p
msg           = p
"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 :: [Id] -> CoreExpr -> Maybe [Id]
hasTuple [Id]
ys = CoreExpr -> Maybe [Id]
stepE
  where
    stepE :: CoreExpr -> Maybe [Id]
stepE CoreExpr
e
     | Just [Id]
xs <- [Id] -> CoreExpr -> Maybe [Id]
isVarTup [Id]
ys CoreExpr
e = [Id] -> Maybe [Id]
forall a. a -> Maybe a
Just [Id]
xs
     | Bool
otherwise                = CoreExpr -> Maybe [Id]
go CoreExpr
e
    stepA :: Alt Id -> Maybe [Id]
stepA (AltCon
DEFAULT,[Id]
_,CoreExpr
_)         = Maybe [Id]
forall a. Maybe a
Nothing
    stepA (AltCon
_, [Id]
_, CoreExpr
e)             = CoreExpr -> Maybe [Id]
stepE CoreExpr
e
    go :: CoreExpr -> Maybe [Id]
go (Let CoreBind
_ CoreExpr
e)                = CoreExpr -> Maybe [Id]
stepE CoreExpr
e
    go (Case CoreExpr
_ Id
_ Type
_ [Alt Id]
cs)          = [Maybe [Id]] -> Maybe [Id]
forall (t :: * -> *) (m :: * -> *) a.
(Foldable t, MonadPlus m) =>
t (m a) -> m a
msum (Alt Id -> Maybe [Id]
stepA (Alt Id -> Maybe [Id]) -> [Alt Id] -> [Maybe [Id]]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [Alt Id]
cs)
    go CoreExpr
_                        = Maybe [Id]
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 :: [Id] -> CoreExpr -> RewriteRule
replaceTuple [Id]
ys CoreExpr
e CoreExpr
e'           = RewriteRule
stepE CoreExpr
e
  where
    t' :: Type
t'                          = CoreExpr -> Type
CoreUtils.exprType CoreExpr
e'
    stepE :: RewriteRule
stepE CoreExpr
e
     | Just [Id]
xs <- [Id] -> CoreExpr -> Maybe [Id]
isVarTup [Id]
ys CoreExpr
e = RewriteRule
forall a. a -> Maybe a
Just RewriteRule -> RewriteRule
forall a b. (a -> b) -> a -> b
$ [Id] -> [Id] -> CoreExpr -> CoreExpr
substTuple [Id]
xs [Id]
ys CoreExpr
e'
     | Bool
otherwise                = RewriteRule
go CoreExpr
e
    stepA :: Alt Id -> Maybe (Alt Id)
stepA (AltCon
DEFAULT, [Id]
xs, CoreExpr
err)    = Alt Id -> Maybe (Alt Id)
forall a. a -> Maybe a
Just (AltCon
DEFAULT, [Id]
xs, Type -> CoreExpr -> CoreExpr
replaceIrrefutPat Type
t' CoreExpr
err)
    stepA (AltCon
c, [Id]
xs, CoreExpr
e)            = (AltCon
c, [Id]
xs,)   (CoreExpr -> Alt Id) -> Maybe CoreExpr -> Maybe (Alt Id)
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 Id
x Type
t [Alt Id]
cs)          = CoreExpr -> Id -> Type -> [Alt Id] -> CoreExpr
fixCase CoreExpr
e Id
x Type
t ([Alt Id] -> CoreExpr) -> Maybe [Alt Id] -> Maybe CoreExpr
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (Alt Id -> Maybe (Alt Id)) -> [Alt Id] -> Maybe [Alt Id]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM Alt Id -> Maybe (Alt Id)
stepA [Alt Id]
cs
    go CoreExpr
_                        = Maybe CoreExpr
forall a. Maybe a
Nothing

_showExpr :: CoreExpr -> String
_showExpr :: CoreExpr -> String
_showExpr CoreExpr
e = CoreExpr -> String
show' CoreExpr
e
  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 Id
x)     = Id -> String
_showVar Id
x
    show' (Let (NonRec Id
x CoreExpr
ex) CoreExpr
e) = String
"Let " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Id -> String
_showVar Id
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 Tickish Id
_ CoreExpr
e) = CoreExpr -> String
show' CoreExpr
e
    show' (Case CoreExpr
e Id
x Type
_ [Alt Id]
alt) = String
"Case " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Id -> String
_showVar Id
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 Id -> String
showAlt' (Alt Id -> String) -> [Alt Id] -> [String]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [Alt Id]
alt)
    show' CoreExpr
e           = CoreExpr -> String
forall a. Outputable a => a -> String
showPpr CoreExpr
e

    showAlt' :: Alt Id -> String
showAlt' (AltCon
c, [Id]
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 (Id -> String
_showVar (Id -> String) -> [Id] -> [String]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [Id]
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 :: Id -> String
_showVar = Symbol -> String
forall a. Show a => a -> String
show (Symbol -> String) -> (Id -> Symbol) -> Id -> String
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Id -> Symbol
forall a. Symbolic a => a -> Symbol
F.symbol

_errorSkip :: String -> a -> b
_errorSkip :: 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 -> Id -> Type -> [Alt Id] -> CoreExpr
fixCase CoreExpr
e Id
x Type
_t [Alt Id]
cs' = CoreExpr -> Id -> Type -> [Alt Id] -> CoreExpr
forall b. Expr b -> b -> Type -> [Alt b] -> Expr b
Case CoreExpr
e Id
x Type
t' [Alt Id]
cs'
  where
    t' :: Type
t'            = CoreExpr -> Type
CoreUtils.exprType CoreExpr
body
    (AltCon
_,[Id]
_,CoreExpr
body)    = Alt Id
c
    Alt Id
c:[Alt Id]
_           = [Alt Id]
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 Id
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 (Id -> CoreExpr -> CoreExpr
forall b. b -> Expr b -> Expr b
Lam Id
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 Id
x, CoreExpr
rep:CoreExpr
_:[CoreExpr]
args) <- CoreExpr -> (CoreExpr, [CoreExpr])
forall b. Expr b -> (Expr b, [Expr b])
collectArgs CoreExpr
e
  , Id -> Bool
isIrrefutErrorVar Id
x
  = RewriteRule
forall a. a -> Maybe a
Just (CoreExpr -> [CoreExpr] -> CoreExpr
MkCore.mkCoreApps (Id -> CoreExpr
forall b. Id -> Expr b
Var Id
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 -- MkCore.iRREFUT_PAT_ERROR_ID == x -- TODO:GHC-863
isIrrefutErrorVar :: Id -> Bool
isIrrefutErrorVar Id
x = Id
x Id -> Id -> Bool
forall a. Eq a => a -> a -> Bool
== Id
MkCore.pAT_ERROR_ID
 
--------------------------------------------------------------------------------
-- | `substTuple xs ys e'` returns e' [y1 := x1,...,yn := xn]
--------------------------------------------------------------------------------
substTuple :: [Var] -> [Var] -> CoreExpr -> CoreExpr
substTuple :: [Id] -> [Id] -> CoreExpr -> CoreExpr
substTuple [Id]
xs [Id]
ys = HashMap Id Id -> CoreExpr -> CoreExpr
substExpr ([(Id, Id)] -> HashMap Id Id
forall k v. (Eq k, Hashable k) => [(k, v)] -> HashMap k v
M.fromList ([(Id, Id)] -> HashMap Id Id) -> [(Id, Id)] -> HashMap Id Id
forall a b. (a -> b) -> a -> b
$ [Id] -> [Id] -> [(Id, Id)]
forall a b. [a] -> [b] -> [(a, b)]
zip [Id]
ys [Id]
xs)

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

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

eqVars :: [Var] -> [Var] -> Bool
eqVars :: [Id] -> [Id] -> Bool
eqVars [Id]
xs [Id]
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 -} Id -> String
forall a. Show a => a -> String
show (Id -> String) -> [Id] -> [String]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [Id]
xs
    ys' :: [String]
ys' = {- F.symbol -} Id -> String
forall a. Show a => a -> String
show (Id -> String) -> [Id] -> [String]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [Id]
ys

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

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

secondHalf :: [a] -> [a]
secondHalf :: [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 (t :: * -> *) a. Foldable t => t a -> Int
length [a]
xs