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

-- | This module contains functions for "resugaring" low-level GHC `CoreExpr`
--   into high-level patterns, that can receive special case handling in
--   different phases (e.g. ANF, Constraint Generation, etc.)

module Language.Haskell.Liquid.GHC.Resugar (
  -- * High-level Source Patterns
    Pattern (..)

  -- * Lift a CoreExpr into a Pattern
  , lift

  -- * Lower a pattern back into a CoreExpr
  , lower
  ) where

import qualified Data.List as L
import           Liquid.GHC.API  as Ghc
import qualified Language.Haskell.Liquid.GHC.Misc as GM
import qualified Language.Fixpoint.Types          as F
import qualified Text.PrettyPrint.HughesPJ        as PJ
-- import           Debug.Trace

--------------------------------------------------------------------------------
-- | Data type for high-level patterns -----------------------------------------
--------------------------------------------------------------------------------

data Pattern
  = PatBind
      { Pattern -> Expr Var
patE1  :: !CoreExpr
      , Pattern -> Var
patX   :: !Var
      , Pattern -> Expr Var
patE2  :: !CoreExpr
      , Pattern -> Type
patM   :: !Type
      , Pattern -> Expr Var
patDct :: !CoreExpr
      , Pattern -> Type
patTyA :: !Type
      , Pattern -> Type
patTyB :: !Type
      , Pattern -> Var
patFF  :: !Var
      }                      -- ^ e1 >>= \x -> e2

  | PatReturn                -- return @ m @ t @ $dT @ e
     { Pattern -> Expr Var
patE    :: !CoreExpr  -- ^ e
     , patM    :: !Type      -- ^ m
     , patDct  :: !CoreExpr  -- ^ $dT
     , Pattern -> Type
patTy   :: !Type      -- ^ t
     , Pattern -> Var
patRet  :: !Var       -- ^ "return"
     }

  | PatProject               -- (case xe as x of C [x1,...,xn] -> xi) : ty
    { Pattern -> Var
patXE    :: !Var       -- ^ xe
    , patX     :: !Var       -- ^ x
    , patTy    :: !Type      -- ^ ty
    , Pattern -> DataCon
patCtor  :: !DataCon   -- ^ C
    , Pattern -> [Var]
patBinds :: ![Var]     -- ^ [x1,...,xn]
    , Pattern -> Int
patIdx   :: !Int       -- ^ i :: NatLT {len patBinds}
    }

  | PatSelfBind              -- let x = e in x
    { patX     :: !Var       -- ^ x
    , patE     :: !CoreExpr  -- ^ e
    }

  | PatSelfRecBind           -- letrec x = e in x
    { patX     :: !Var       -- ^ x
    , patE     :: !CoreExpr  -- ^ e
    }

instance F.PPrint Pattern where
  pprintTidy :: Tidy -> Pattern -> Doc
pprintTidy  = Tidy -> Pattern -> Doc
ppPat

ppPat :: F.Tidy -> Pattern -> PJ.Doc
ppPat :: Tidy -> Pattern -> Doc
ppPat Tidy
k (PatReturn Expr Var
e Type
m Expr Var
d Type
t Var
rv) =
  Doc
"PatReturn: "
  Doc -> Doc -> Doc
PJ.$+$
  Tidy -> [(Doc, Doc)] -> Doc
forall k v. (PPrint k, PPrint v) => Tidy -> [(k, v)] -> Doc
F.pprintKVs Tidy
k
    [ (Doc
"rv" :: PJ.Doc, Var -> Doc
forall a. Outputable a => a -> Doc
GM.pprDoc Var
rv)
    , (Doc
"e " :: PJ.Doc, Expr Var -> Doc
forall a. Outputable a => a -> Doc
GM.pprDoc Expr Var
e)
    , (Doc
"m " :: PJ.Doc, Type -> Doc
forall a. Outputable a => a -> Doc
GM.pprDoc Type
m)
    , (Doc
"$d" :: PJ.Doc, Expr Var -> Doc
forall a. Outputable a => a -> Doc
GM.pprDoc Expr Var
d)
    , (Doc
"t " :: PJ.Doc, Type -> Doc
forall a. Outputable a => a -> Doc
GM.pprDoc Type
t)
    ]
ppPat Tidy
_ Pattern
_  = Doc
"TODO: PATTERN"


_mbId :: CoreExpr -> Maybe Var
_mbId :: Expr Var -> Maybe Var
_mbId (Var Var
x)    = Var -> Maybe Var
forall a. a -> Maybe a
Just Var
x
_mbId (Tick CoreTickish
_ Expr Var
e) = Expr Var -> Maybe Var
_mbId Expr Var
e
_mbId Expr Var
_          = Maybe Var
forall a. Maybe a
Nothing

--------------------------------------------------------------------------------
-- | Lift expressions into High-level patterns ---------------------------------
--------------------------------------------------------------------------------
lift :: CoreExpr -> Maybe Pattern
--------------------------------------------------------------------------------
lift :: Expr Var -> Maybe Pattern
lift Expr Var
e = Expr Var -> (Expr Var, [Expr Var]) -> Maybe Pattern
exprArgs Expr Var
e (Expr Var -> (Expr Var, [Expr Var])
forall b. Expr b -> (Expr b, [Expr b])
collectArgs Expr Var
e)

exprArgs :: CoreExpr -> (CoreExpr, [CoreExpr]) -> Maybe Pattern
exprArgs :: Expr Var -> (Expr Var, [Expr Var]) -> Maybe Pattern
exprArgs Expr Var
_e (Var Var
op, [Type Type
m, Expr Var
d, Type Type
a, Type Type
b, Expr Var
e1, Lam Var
x Expr Var
e2])
  | Var
op Var -> Name -> Bool
`is` Name
Ghc.bindMName
  = Pattern -> Maybe Pattern
forall a. a -> Maybe a
Just (Expr Var
-> Var
-> Expr Var
-> Type
-> Expr Var
-> Type
-> Type
-> Var
-> Pattern
PatBind Expr Var
e1 Var
x Expr Var
e2 Type
m Expr Var
d Type
a Type
b Var
op)

exprArgs (Case (Var Var
xe) Var
x Type
t [Alt (DataAlt DataCon
c) [Var]
ys (Var Var
y)]) (Expr Var, [Expr Var])
_
  | Just Int
i <- Var
y Var -> [Var] -> Maybe Int
forall a. Eq a => a -> [a] -> Maybe Int
`L.elemIndex` [Var]
ys
  = Pattern -> Maybe Pattern
forall a. a -> Maybe a
Just (Var -> Var -> Type -> DataCon -> [Var] -> Int -> Pattern
PatProject Var
xe Var
x Type
t DataCon
c [Var]
ys Int
i)


{- TEMPORARILY DISABLED: TODO-REBARE; in reality it hasn't been working AT ALL
   since at least the GHC 8.2.1 port (?) because the TICKs get in the way
   of recognizing the pattern? Anyways, messes up

     tests/pattern/pos/Return00.hs

   because we treat _all_ types of the form `m a` as "invariant" in the parameter `a`.
   Looks like the above tests only pass in earlier LH versions because this pattern
   was NOT getting tickled!

exprArgs _e (Var op, [Type m, d, Type t, e])
  | op `is` PN.returnMName
  = Just (PatReturn e m d t op)
-}

{- TEMPORARILY DISBLED

exprArgs (Let (NonRec x e) e') _
  | Just y <- _mbId e', x == y
  = Just (PatSelfBind x e)

exprArgs (Let (Rec [(x, e)]) e') _
  | Just y <- _mbId e', x == y
  = Just (PatSelfRecBind x e)

-}
exprArgs Expr Var
_ (Expr Var, [Expr Var])
_
  = Maybe Pattern
forall a. Maybe a
Nothing

is :: Var -> Name -> Bool
is :: Var -> Name -> Bool
is Var
v Name
n = Name
n Name -> Name -> Bool
forall a. Eq a => a -> a -> Bool
== Var -> Name
forall a. NamedThing a => a -> Name
getName Var
v

--------------------------------------------------------------------------------
-- | Lower patterns back into expressions --------------------------------------
--------------------------------------------------------------------------------
lower :: Pattern -> CoreExpr
--------------------------------------------------------------------------------
lower :: Pattern -> Expr Var
lower (PatBind Expr Var
e1 Var
x Expr Var
e2 Type
m Expr Var
d Type
a Type
b Var
op)
  = Expr Var -> [Expr Var] -> Expr Var
Ghc.mkCoreApps (Var -> Expr Var
forall b. Var -> Expr b
Var Var
op) [Type -> Expr Var
forall b. Type -> Expr b
Type Type
m, Expr Var
d, Type -> Expr Var
forall b. Type -> Expr b
Type Type
a, Type -> Expr Var
forall b. Type -> Expr b
Type Type
b, Expr Var
e1, Var -> Expr Var -> Expr Var
forall b. b -> Expr b -> Expr b
Lam Var
x Expr Var
e2]

lower (PatReturn Expr Var
e Type
m Expr Var
d Type
t Var
op)
  = Expr Var -> [Expr Var] -> Expr Var
Ghc.mkCoreApps (Var -> Expr Var
forall b. Var -> Expr b
Var Var
op) [Type -> Expr Var
forall b. Type -> Expr b
Type Type
m, Expr Var
d, Type -> Expr Var
forall b. Type -> Expr b
Type Type
t, Expr Var
e]

lower (PatProject Var
xe Var
x Type
t DataCon
c [Var]
ys Int
i)
  = Expr Var -> Var -> Type -> [Alt Var] -> Expr Var
forall b. Expr b -> b -> Type -> [Alt b] -> Expr b
Case (Var -> Expr Var
forall b. Var -> Expr b
Var Var
xe) Var
x Type
t [AltCon -> [Var] -> Expr Var -> Alt Var
forall b. AltCon -> [b] -> Expr b -> Alt b
Alt (DataCon -> AltCon
DataAlt DataCon
c) [Var]
ys (Var -> Expr Var
forall b. Var -> Expr b
Var Var
yi)] where yi :: Var
yi = [Var]
ys [Var] -> Int -> Var
forall a. HasCallStack => [a] -> Int -> a
!! Int
i

lower (PatSelfBind Var
x Expr Var
e)
  = Bind Var -> Expr Var -> Expr Var
forall b. Bind b -> Expr b -> Expr b
Let (Var -> Expr Var -> Bind Var
forall b. b -> Expr b -> Bind b
NonRec Var
x Expr Var
e) (Var -> Expr Var
forall b. Var -> Expr b
Var Var
x)

lower (PatSelfRecBind Var
x Expr Var
e)
  = Bind Var -> Expr Var -> Expr Var
forall b. Bind b -> Expr b -> Expr b
Let ([(Var, Expr Var)] -> Bind Var
forall b. [(b, Expr b)] -> Bind b
Rec [(Var
x, Expr Var
e)]) (Var -> Expr Var
forall b. Var -> Expr b
Var Var
x)