{-# LANGUAGE ExistentialQuantification #-}
module GHC.Tc.Errors.Hole.FitTypes (
  TypedHole (..), HoleFit (..), HoleFitCandidate (..),
  CandPlugin, FitPlugin, HoleFitPlugin (..), HoleFitPluginR (..),
  hfIsLcl, pprHoleFitCand
  ) where

import GHC.Prelude

import GHC.Tc.Types
import GHC.Tc.Types.Constraint
import GHC.Tc.Utils.TcType

import GHC.Types.Name.Reader

import GHC.Hs.Doc
import GHC.Types.Id

import GHC.Utils.Outputable
import GHC.Types.Name

import Data.Function ( on )

data TypedHole = TypedHole { TypedHole -> Cts
th_relevant_cts :: Cts
                           -- ^ Any relevant Cts to the hole
                           , TypedHole -> [Implication]
th_implics :: [Implication]
                           -- ^ The nested implications of the hole with the
                           --   innermost implication first.
                           , TypedHole -> Maybe Hole
th_hole :: Maybe Hole
                           -- ^ The hole itself, if available. Only for debugging.
                           }

instance Outputable TypedHole where
  ppr :: TypedHole -> SDoc
ppr (TypedHole { th_relevant_cts :: TypedHole -> Cts
th_relevant_cts = Cts
rels
                 , th_implics :: TypedHole -> [Implication]
th_implics      = [Implication]
implics
                 , th_hole :: TypedHole -> Maybe Hole
th_hole         = Maybe Hole
hole })
    = SDoc -> Int -> SDoc -> SDoc
hang (String -> SDoc
text String
"TypedHole") Int
2
        (Cts -> SDoc
forall a. Outputable a => a -> SDoc
External instance of the constraint type forall a. Outputable a => Outputable (Bag a)
External instance of the constraint type Outputable Ct
ppr Cts
rels SDoc -> SDoc -> SDoc
$+$ [Implication] -> SDoc
forall a. Outputable a => a -> SDoc
External instance of the constraint type forall a. Outputable a => Outputable [a]
External instance of the constraint type Outputable Implication
ppr [Implication]
implics SDoc -> SDoc -> SDoc
$+$ Maybe Hole -> SDoc
forall a. Outputable a => a -> SDoc
External instance of the constraint type forall a. Outputable a => Outputable (Maybe a)
External instance of the constraint type Outputable Hole
ppr Maybe Hole
hole)

-- | 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
External instance of the constraint type Eq GlobalRdrElt
External instance of the constraint type Eq Name
External instance of the constraint type Eq Id
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
External instance of the constraint type Outputable Id
ppr Id
cid
pprHoleFitCand (NameHFCand Name
cname) = String -> SDoc
text String
"Name HFC: " SDoc -> SDoc -> SDoc
<> Name -> SDoc
forall a. Outputable a => a -> SDoc
External instance of the constraint type Outputable Name
ppr Name
cname
pprHoleFitCand (GreHFCand GlobalRdrElt
cgre) = String -> SDoc
text String
"Gre HFC: " SDoc -> SDoc -> SDoc
<> GlobalRdrElt -> SDoc
forall a. Outputable a => a -> SDoc
External instance of the constraint type Outputable GlobalRdrElt
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
External instance of the constraint type HasOccName Id
occName Id
cid
                     NameHFCand Name
cname -> Name -> OccName
forall name. HasOccName name => name -> OccName
External instance of the constraint type HasOccName Name
occName Name
cname
                     GreHFCand GlobalRdrElt
cgre -> Name -> OccName
forall name. HasOccName name => name -> OccName
External instance of the constraint type HasOccName Name
occName (GlobalRdrElt -> Name
gre_name GlobalRdrElt
cgre)

instance HasOccName HoleFitCandidate where
  occName :: HoleFitCandidate -> OccName
occName = HoleFitCandidate -> OccName
forall a. NamedThing a => a -> OccName
Instance of class: NamedThing of the constraint type NamedThing HoleFitCandidate
getOccName

instance Ord HoleFitCandidate where
  compare :: HoleFitCandidate -> HoleFitCandidate -> Ordering
compare = Name -> Name -> Ordering
forall a. Ord a => a -> a -> Ordering
External instance of the constraint type Ord Name
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
Instance of class: NamedThing of the constraint type NamedThing HoleFitCandidate
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
External instance of the constraint type Eq Id
(==) (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
External instance of the constraint type Outputable TcType
ppr TcType
ty))
    where name :: SDoc
name = Name -> SDoc
forall a. Outputable a => a -> SDoc
External instance of the constraint type Outputable Name
ppr (Name -> SDoc) -> Name -> SDoc
forall a b. (a -> b) -> a -> b
$ HoleFitCandidate -> Name
forall a. NamedThing a => a -> Name
Instance of class: NamedThing of the constraint type NamedThing HoleFitCandidate
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
External instance of the constraint type Outputable TcType
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
External instance of the constraint type Eq Int
== HoleFit -> Int
hfRefLvl HoleFit
b
                 then Name -> Name -> Ordering
forall a. Ord a => a -> a -> Ordering
External instance of the constraint type Ord Name
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
Instance of class: NamedThing of the constraint type NamedThing HoleFitCandidate
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
External instance of the constraint type Ord Int
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
  }