{-# 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 -> CoreExpr
patE1  :: !CoreExpr
      , Pattern -> Var
patX   :: !Var
      , Pattern -> CoreExpr
patE2  :: !CoreExpr
      , Pattern -> Type
patM   :: !Type
      , Pattern -> CoreExpr
patDct :: !CoreExpr
      , Pattern -> Type
patTyA :: !Type
      , Pattern -> Type
patTyB :: !Type
      , Pattern -> Var
patFF  :: !Var
      }                      -- ^ e1 >>= \x -> e2

  | PatReturn                -- return @ m @ t @ $dT @ e
     { Pattern -> CoreExpr
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 CoreExpr
e Type
m CoreExpr
d Type
t Var
rv) = 
  Doc
"PatReturn: " 
  Doc -> Doc -> Doc
PJ.$+$ 
  forall k v. (PPrint k, PPrint v) => Tidy -> [(k, v)] -> Doc
F.pprintKVs Tidy
k
    [ (Doc
"rv" :: PJ.Doc, forall a. Outputable a => a -> Doc
GM.pprDoc Var
rv) 
    , (Doc
"e " :: PJ.Doc, forall a. Outputable a => a -> Doc
GM.pprDoc CoreExpr
e) 
    , (Doc
"m " :: PJ.Doc, forall a. Outputable a => a -> Doc
GM.pprDoc Type
m) 
    , (Doc
"$d" :: PJ.Doc, forall a. Outputable a => a -> Doc
GM.pprDoc CoreExpr
d) 
    , (Doc
"t " :: PJ.Doc, forall a. Outputable a => a -> Doc
GM.pprDoc Type
t) 
    ] 
ppPat Tidy
_ Pattern
_  = Doc
"TODO: PATTERN" 
    

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

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

exprArgs :: CoreExpr -> (CoreExpr, [CoreExpr]) -> Maybe Pattern
exprArgs :: CoreExpr -> (CoreExpr, [CoreExpr]) -> Maybe Pattern
exprArgs CoreExpr
_e (Var Var
op, [Type Type
m, CoreExpr
d, Type Type
a, Type Type
b, CoreExpr
e1, Lam Var
x CoreExpr
e2])
  | Var
op Var -> Name -> Bool
`is` Name
Ghc.bindMName
  = forall a. a -> Maybe a
Just (CoreExpr
-> Var
-> CoreExpr
-> Type
-> CoreExpr
-> Type
-> Type
-> Var
-> Pattern
PatBind CoreExpr
e1 Var
x CoreExpr
e2 Type
m CoreExpr
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)]) (CoreExpr, [CoreExpr])
_
  | Just Int
i <- Var
y forall a. Eq a => a -> [a] -> Maybe Int
`L.elemIndex` [Var]
ys
  = 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 CoreExpr
_ (CoreExpr, [CoreExpr])
_
  = forall a. Maybe a
Nothing

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

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

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

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

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

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