{-# LANGUAGE ExistentialQuantification #-}
module TcHoleFitTypes (
  TypedHole (..), HoleFit (..), HoleFitCandidate (..),
  CandPlugin, FitPlugin, HoleFitPlugin (..), HoleFitPluginR (..),
  hfIsLcl, pprHoleFitCand
  ) where

import GhcPrelude

import TcRnTypes
import Constraint
import TcType

import RdrName

import GHC.Hs.Doc
import Id

import Outputable
import Name

import Data.Function ( on )

data TypedHole = TyH { TypedHole -> Cts
tyHRelevantCts :: Cts
                       -- ^ Any relevant Cts to the hole
                     , TypedHole -> [Implication]
tyHImplics :: [Implication]
                       -- ^ The nested implications of the hole with the
                       --   innermost implication first.
                     , TypedHole -> Maybe Ct
tyHCt :: Maybe Ct
                       -- ^ The hole constraint itself, if available.
                     }

instance Outputable TypedHole where
  ppr :: TypedHole -> SDoc
ppr (TyH Cts
rels [Implication]
implics Maybe Ct
ct)
    = SDoc -> Int -> SDoc -> SDoc
hang (String -> SDoc
text String
"TypedHole") Int
2
        (Cts -> SDoc
forall a. Outputable a => a -> SDoc
ppr Cts
rels SDoc -> SDoc -> SDoc
$+$ [Implication] -> SDoc
forall a. Outputable a => a -> SDoc
ppr [Implication]
implics SDoc -> SDoc -> SDoc
$+$ Maybe Ct -> SDoc
forall a. Outputable a => a -> SDoc
ppr Maybe Ct
ct)


-- | HoleFitCandidates are passed to hole fit plugins and then
-- checked whether they fit a given typed-hole.
data HoleFitCandidate = IdHFCand Id             -- An id, like locals.
                      | NameHFCand Name         -- A name, like built-in syntax.
                      | GreHFCand GlobalRdrElt  -- A global, like imported ids.
                      deriving (HoleFitCandidate -> HoleFitCandidate -> Bool
(HoleFitCandidate -> HoleFitCandidate -> Bool)
-> (HoleFitCandidate -> HoleFitCandidate -> Bool)
-> Eq HoleFitCandidate
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: HoleFitCandidate -> HoleFitCandidate -> Bool
$c/= :: HoleFitCandidate -> HoleFitCandidate -> Bool
== :: HoleFitCandidate -> HoleFitCandidate -> Bool
$c== :: HoleFitCandidate -> HoleFitCandidate -> Bool
Eq)

instance Outputable HoleFitCandidate where
  ppr :: HoleFitCandidate -> SDoc
ppr = HoleFitCandidate -> SDoc
pprHoleFitCand

pprHoleFitCand :: HoleFitCandidate -> SDoc
pprHoleFitCand :: HoleFitCandidate -> SDoc
pprHoleFitCand (IdHFCand Id
cid) = String -> SDoc
text String
"Id HFC: " SDoc -> SDoc -> SDoc
<> Id -> SDoc
forall a. Outputable a => a -> SDoc
ppr Id
cid
pprHoleFitCand (NameHFCand Name
cname) = String -> SDoc
text String
"Name HFC: " SDoc -> SDoc -> SDoc
<> Name -> SDoc
forall a. Outputable a => a -> SDoc
ppr Name
cname
pprHoleFitCand (GreHFCand GlobalRdrElt
cgre) = String -> SDoc
text String
"Gre HFC: " SDoc -> SDoc -> SDoc
<> GlobalRdrElt -> SDoc
forall a. Outputable a => a -> SDoc
ppr GlobalRdrElt
cgre




instance NamedThing HoleFitCandidate where
  getName :: HoleFitCandidate -> Name
getName HoleFitCandidate
hfc = case HoleFitCandidate
hfc of
                     IdHFCand Id
cid -> Id -> Name
idName Id
cid
                     NameHFCand Name
cname -> Name
cname
                     GreHFCand GlobalRdrElt
cgre -> GlobalRdrElt -> Name
gre_name GlobalRdrElt
cgre
  getOccName :: HoleFitCandidate -> OccName
getOccName HoleFitCandidate
hfc = case HoleFitCandidate
hfc of
                     IdHFCand Id
cid -> Id -> OccName
forall name. HasOccName name => name -> OccName
occName Id
cid
                     NameHFCand Name
cname -> Name -> OccName
forall name. HasOccName name => name -> OccName
occName Name
cname
                     GreHFCand GlobalRdrElt
cgre -> Name -> OccName
forall name. HasOccName name => name -> OccName
occName (GlobalRdrElt -> Name
gre_name GlobalRdrElt
cgre)

instance HasOccName HoleFitCandidate where
  occName :: HoleFitCandidate -> OccName
occName = HoleFitCandidate -> OccName
forall a. NamedThing a => a -> OccName
getOccName

instance Ord HoleFitCandidate where
  compare :: HoleFitCandidate -> HoleFitCandidate -> Ordering
compare = Name -> Name -> Ordering
forall a. Ord a => a -> a -> Ordering
compare (Name -> Name -> Ordering)
-> (HoleFitCandidate -> Name)
-> HoleFitCandidate
-> HoleFitCandidate
-> Ordering
forall b c a. (b -> b -> c) -> (a -> b) -> a -> a -> c
`on` HoleFitCandidate -> Name
forall a. NamedThing a => a -> Name
getName

-- | HoleFit is the type we use for valid hole fits. It contains the
-- element that was checked, the Id of that element as found by `tcLookup`,
-- and the refinement level of the fit, which is the number of extra argument
-- holes that this fit uses (e.g. if hfRefLvl is 2, the fit is for `Id _ _`).
data HoleFit =
  HoleFit { HoleFit -> Id
hfId   :: Id       -- ^ The elements id in the TcM
          , HoleFit -> HoleFitCandidate
hfCand :: HoleFitCandidate  -- ^ The candidate that was checked.
          , HoleFit -> TcType
hfType :: TcType -- ^ The type of the id, possibly zonked.
          , HoleFit -> Int
hfRefLvl :: Int  -- ^ The number of holes in this fit.
          , HoleFit -> [TcType]
hfWrap :: [TcType] -- ^ The wrapper for the match.
          , HoleFit -> [TcType]
hfMatches :: [TcType]
          -- ^ What the refinement variables got matched with, if anything
          , HoleFit -> Maybe HsDocString
hfDoc :: Maybe HsDocString
          -- ^ Documentation of this HoleFit, if available.
          }
 | RawHoleFit SDoc
 -- ^ A fit that is just displayed as is. Here so thatHoleFitPlugins
 --   can inject any fit they want.

-- We define an Eq and Ord instance to be able to build a graph.
instance Eq HoleFit where
   == :: HoleFit -> HoleFit -> Bool
(==) = Id -> Id -> Bool
forall a. Eq a => a -> a -> Bool
(==) (Id -> Id -> Bool) -> (HoleFit -> Id) -> HoleFit -> HoleFit -> Bool
forall b c a. (b -> b -> c) -> (a -> b) -> a -> a -> c
`on` HoleFit -> Id
hfId

instance Outputable HoleFit where
  ppr :: HoleFit -> SDoc
ppr (RawHoleFit SDoc
sd) = SDoc
sd
  ppr (HoleFit Id
_ HoleFitCandidate
cand TcType
ty Int
_ [TcType]
_ [TcType]
mtchs Maybe HsDocString
_) =
    SDoc -> Int -> SDoc -> SDoc
hang (SDoc
name SDoc -> SDoc -> SDoc
<+> SDoc
holes) Int
2 (String -> SDoc
text String
"where" SDoc -> SDoc -> SDoc
<+> SDoc
name SDoc -> SDoc -> SDoc
<+> SDoc
dcolon SDoc -> SDoc -> SDoc
<+> (TcType -> SDoc
forall a. Outputable a => a -> SDoc
ppr TcType
ty))
    where name :: SDoc
name = Name -> SDoc
forall a. Outputable a => a -> SDoc
ppr (Name -> SDoc) -> Name -> SDoc
forall a b. (a -> b) -> a -> b
$ HoleFitCandidate -> Name
forall a. NamedThing a => a -> Name
getName HoleFitCandidate
cand
          holes :: SDoc
holes = [SDoc] -> SDoc
sep ([SDoc] -> SDoc) -> [SDoc] -> SDoc
forall a b. (a -> b) -> a -> b
$ (TcType -> SDoc) -> [TcType] -> [SDoc]
forall a b. (a -> b) -> [a] -> [b]
map (SDoc -> SDoc
parens (SDoc -> SDoc) -> (TcType -> SDoc) -> TcType -> SDoc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (String -> SDoc
text String
"_" SDoc -> SDoc -> SDoc
<+> SDoc
dcolon SDoc -> SDoc -> SDoc
<+>) (SDoc -> SDoc) -> (TcType -> SDoc) -> TcType -> SDoc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. TcType -> SDoc
forall a. Outputable a => a -> SDoc
ppr) [TcType]
mtchs

-- We compare HoleFits by their name instead of their Id, since we don't
-- want our tests to be affected by the non-determinism of `nonDetCmpVar`,
-- which is used to compare Ids. When comparing, we want HoleFits with a lower
-- refinement level to come first.
instance Ord HoleFit where
  compare :: HoleFit -> HoleFit -> Ordering
compare (RawHoleFit SDoc
_) (RawHoleFit SDoc
_) = Ordering
EQ
  compare (RawHoleFit SDoc
_) HoleFit
_ = Ordering
LT
  compare HoleFit
_ (RawHoleFit SDoc
_) = Ordering
GT
  compare a :: HoleFit
a@(HoleFit {}) b :: HoleFit
b@(HoleFit {}) = HoleFit -> HoleFit -> Ordering
cmp HoleFit
a HoleFit
b
    where cmp :: HoleFit -> HoleFit -> Ordering
cmp  = if HoleFit -> Int
hfRefLvl HoleFit
a Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== HoleFit -> Int
hfRefLvl HoleFit
b
                 then Name -> Name -> Ordering
forall a. Ord a => a -> a -> Ordering
compare (Name -> Name -> Ordering)
-> (HoleFit -> Name) -> HoleFit -> HoleFit -> Ordering
forall b c a. (b -> b -> c) -> (a -> b) -> a -> a -> c
`on` (HoleFitCandidate -> Name
forall a. NamedThing a => a -> Name
getName (HoleFitCandidate -> Name)
-> (HoleFit -> HoleFitCandidate) -> HoleFit -> Name
forall b c a. (b -> c) -> (a -> b) -> a -> c
. HoleFit -> HoleFitCandidate
hfCand)
                 else Int -> Int -> Ordering
forall a. Ord a => a -> a -> Ordering
compare (Int -> Int -> Ordering)
-> (HoleFit -> Int) -> HoleFit -> HoleFit -> Ordering
forall b c a. (b -> b -> c) -> (a -> b) -> a -> a -> c
`on` HoleFit -> Int
hfRefLvl

hfIsLcl :: HoleFit -> Bool
hfIsLcl :: HoleFit -> Bool
hfIsLcl hf :: HoleFit
hf@(HoleFit {}) = case HoleFit -> HoleFitCandidate
hfCand HoleFit
hf of
                            IdHFCand Id
_    -> Bool
True
                            NameHFCand Name
_  -> Bool
False
                            GreHFCand GlobalRdrElt
gre -> GlobalRdrElt -> Bool
gre_lcl GlobalRdrElt
gre
hfIsLcl HoleFit
_ = Bool
False


-- | A plugin for modifying the candidate hole fits *before* they're checked.
type CandPlugin = TypedHole -> [HoleFitCandidate] -> TcM [HoleFitCandidate]

-- | A plugin for modifying hole fits  *after* they've been found.
type FitPlugin =  TypedHole -> [HoleFit] -> TcM [HoleFit]

-- | A HoleFitPlugin is a pair of candidate and fit plugins.
data HoleFitPlugin = HoleFitPlugin
  { HoleFitPlugin -> CandPlugin
candPlugin :: CandPlugin
  , HoleFitPlugin -> FitPlugin
fitPlugin :: FitPlugin }

-- | HoleFitPluginR adds a TcRef to hole fit plugins so that plugins can
-- track internal state. Note the existential quantification, ensuring that
-- the state cannot be modified from outside the plugin.
data HoleFitPluginR = forall s. HoleFitPluginR
  { ()
hfPluginInit :: TcM (TcRef s)
    -- ^ Initializes the TcRef to be passed to the plugin
  , ()
hfPluginRun :: TcRef s -> HoleFitPlugin
    -- ^ The function defining the plugin itself
  , ()
hfPluginStop :: TcRef s -> TcM ()
    -- ^ Cleanup of state, guaranteed to be called even on error
  }