{-# LANGUAGE DataKinds       #-}
{-# LANGUAGE LambdaCase      #-}
{-# LANGUAGE RecordWildCards #-}

module Data.Record.Anon.Internal.Plugin.TC.Constraints.RowHasField (
    CRowHasField(..)
  , parseRowHasField
  , solveRowHasField
  ) where

import Data.Void
import GHC.Stack

import Data.Record.Anon.Internal.Plugin.TC.Row.ParsedRow (Fields, FieldLabel(..))
import Data.Record.Anon.Internal.Plugin.TC.GhcTcPluginAPI
import Data.Record.Anon.Internal.Plugin.TC.NameResolution
import Data.Record.Anon.Internal.Plugin.TC.Parsing
import Data.Record.Anon.Internal.Plugin.TC.TyConSubst

import qualified Data.Record.Anon.Internal.Plugin.TC.Row.ParsedRow as ParsedRow

{-------------------------------------------------------------------------------
  Definition
-------------------------------------------------------------------------------}

-- | Parsed form of a @RowHasField n r@ with @r :: Row k@ constraint
data CRowHasField = CRowHasField {
      -- | Label we're looking for (@n@)
      CRowHasField -> FieldLabel
hasFieldLabel :: FieldLabel

      -- | Fields of the record (parsed form of @r@)
      --
      -- These may be fully or partially known, or completely unknown.
    , CRowHasField -> Fields
hasFieldRecord :: Fields

      -- | Row kind (@k@)
    , CRowHasField -> Type
hasFieldTypeKind :: Type

      -- | Record field (@n@)
    , CRowHasField -> Type
hasFieldTypeLabel :: Type

      -- | Row (@r@)
    , CRowHasField -> Type
hasFieldTypeRow :: Type

      -- | Type of the record field we're looking for (@a@)
      --
      -- Although @a@ will be of the form @f a'@ for some @a'@, we do not
      -- enforce that here (but instead generate a new wanted equality
      -- constraint to enforce this).
    , CRowHasField -> Type
hasFieldTypeField :: Type
    }

{-------------------------------------------------------------------------------
  Outputable
-------------------------------------------------------------------------------}

instance Outputable CRowHasField where
  ppr :: CRowHasField -> SDoc
ppr (CRowHasField FieldLabel
label Fields
record Type
typeKind Type
typeLabel Type
typeRow Type
typeField) = SDoc -> SDoc
parens forall a b. (a -> b) -> a -> b
$
      String -> SDoc
text String
"CRowHasField" SDoc -> SDoc -> SDoc
<+> SDoc -> SDoc
braces ([SDoc] -> SDoc
vcat [
          String -> SDoc
text String
"hasFieldLabel"     SDoc -> SDoc -> SDoc
<+> String -> SDoc
text String
"=" SDoc -> SDoc -> SDoc
<+> forall a. Outputable a => a -> SDoc
ppr FieldLabel
label
        , String -> SDoc
text String
"hasFieldRecord"    SDoc -> SDoc -> SDoc
<+> String -> SDoc
text String
"=" SDoc -> SDoc -> SDoc
<+> forall a. Outputable a => a -> SDoc
ppr Fields
record
        , String -> SDoc
text String
"hasFieldTypeKind"  SDoc -> SDoc -> SDoc
<+> String -> SDoc
text String
"=" SDoc -> SDoc -> SDoc
<+> forall a. Outputable a => a -> SDoc
ppr Type
typeKind
        , String -> SDoc
text String
"hasFieldTypeLabel" SDoc -> SDoc -> SDoc
<+> String -> SDoc
text String
"=" SDoc -> SDoc -> SDoc
<+> forall a. Outputable a => a -> SDoc
ppr Type
typeLabel
        , String -> SDoc
text String
"hasFieldTypeRow"   SDoc -> SDoc -> SDoc
<+> String -> SDoc
text String
"=" SDoc -> SDoc -> SDoc
<+> forall a. Outputable a => a -> SDoc
ppr Type
typeRow
        , String -> SDoc
text String
"hasFieldTypeField" SDoc -> SDoc -> SDoc
<+> String -> SDoc
text String
"=" SDoc -> SDoc -> SDoc
<+> forall a. Outputable a => a -> SDoc
ppr Type
typeField
        ])

{-------------------------------------------------------------------------------
  Parser
-------------------------------------------------------------------------------}

parseRowHasField ::
     HasCallStack
  => TyConSubst
  -> ResolvedNames
  -> Ct
  -> ParseResult Void (GenLocated CtLoc CRowHasField)
parseRowHasField :: HasCallStack =>
TyConSubst
-> ResolvedNames
-> Ct
-> ParseResult Void (GenLocated CtLoc CRowHasField)
parseRowHasField TyConSubst
tcs rn :: ResolvedNames
rn@ResolvedNames{Class
DataCon
TyCon
Id
tyConSimpleFieldTypes :: ResolvedNames -> TyCon
tyConPair :: ResolvedNames -> TyCon
tyConFieldTypes :: ResolvedNames -> TyCon
tyConMerge :: ResolvedNames -> TyCon
tyConDictAny :: ResolvedNames -> TyCon
idUnsafeCoerce :: ResolvedNames -> Id
idEvidenceSubRow :: ResolvedNames -> Id
idEvidenceRowHasField :: ResolvedNames -> Id
idEvidenceKnownHash :: ResolvedNames -> Id
idEvidenceKnownFields :: ResolvedNames -> Id
idEvidenceAllFields :: ResolvedNames -> Id
dataConDictAny :: ResolvedNames -> DataCon
clsSubRow :: ResolvedNames -> Class
clsRowHasField :: ResolvedNames -> Class
clsKnownHash :: ResolvedNames -> Class
clsKnownFields :: ResolvedNames -> Class
clsAllFields :: ResolvedNames -> Class
tyConSimpleFieldTypes :: TyCon
tyConPair :: TyCon
tyConFieldTypes :: TyCon
tyConMerge :: TyCon
tyConDictAny :: TyCon
idUnsafeCoerce :: Id
idEvidenceSubRow :: Id
idEvidenceRowHasField :: Id
idEvidenceKnownHash :: Id
idEvidenceKnownFields :: Id
idEvidenceAllFields :: Id
dataConDictAny :: DataCon
clsSubRow :: Class
clsRowHasField :: Class
clsKnownHash :: Class
clsKnownFields :: Class
clsAllFields :: Class
..} =
    forall a e.
HasCallStack =>
Class
-> ([Type] -> Maybe a) -> Ct -> ParseResult e (GenLocated CtLoc a)
parseConstraint' Class
clsRowHasField forall a b. (a -> b) -> a -> b
$ \ [Type]
args ->
      case [Type]
args of
        [Type
k, Type
n, Type
r, Type
a] -> do
          FieldLabel
label  <- Type -> Maybe FieldLabel
ParsedRow.parseFieldLabel Type
n
          Fields
fields <- TyConSubst -> ResolvedNames -> Type -> Maybe Fields
ParsedRow.parseFields TyConSubst
tcs ResolvedNames
rn Type
r
          forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ CRowHasField {
              hasFieldLabel :: FieldLabel
hasFieldLabel     = FieldLabel
label
            , hasFieldRecord :: Fields
hasFieldRecord    = Fields
fields
            , hasFieldTypeKind :: Type
hasFieldTypeKind  = Type
k
            , hasFieldTypeLabel :: Type
hasFieldTypeLabel = Type
n
            , hasFieldTypeRow :: Type
hasFieldTypeRow   = Type
r
            , hasFieldTypeField :: Type
hasFieldTypeField = Type
a
            }
        [Type]
_ -> forall a. HasCallStack => String -> SDoc -> a
pprPanic String
"parseRowHasField: expected 4 arguments" forall a b. (a -> b) -> a -> b
$
               ( String -> SDoc
text String
"args:" SDoc -> SDoc -> SDoc
<+> forall a. Outputable a => a -> SDoc
ppr [Type]
args )

{-------------------------------------------------------------------------------
  Evidence
-------------------------------------------------------------------------------}

evidenceHasField ::
     ResolvedNames
  -> CRowHasField
  -> Int        -- ^ Field index
  -> TcPluginM 'Solve EvTerm
evidenceHasField :: ResolvedNames -> CRowHasField -> Int -> TcPluginM 'Solve EvTerm
evidenceHasField ResolvedNames{Class
DataCon
TyCon
Id
tyConSimpleFieldTypes :: TyCon
tyConPair :: TyCon
tyConFieldTypes :: TyCon
tyConMerge :: TyCon
tyConDictAny :: TyCon
idUnsafeCoerce :: Id
idEvidenceSubRow :: Id
idEvidenceRowHasField :: Id
idEvidenceKnownHash :: Id
idEvidenceKnownFields :: Id
idEvidenceAllFields :: Id
dataConDictAny :: DataCon
clsSubRow :: Class
clsRowHasField :: Class
clsKnownHash :: Class
clsKnownFields :: Class
clsAllFields :: Class
tyConSimpleFieldTypes :: ResolvedNames -> TyCon
tyConPair :: ResolvedNames -> TyCon
tyConFieldTypes :: ResolvedNames -> TyCon
tyConMerge :: ResolvedNames -> TyCon
tyConDictAny :: ResolvedNames -> TyCon
idUnsafeCoerce :: ResolvedNames -> Id
idEvidenceSubRow :: ResolvedNames -> Id
idEvidenceRowHasField :: ResolvedNames -> Id
idEvidenceKnownHash :: ResolvedNames -> Id
idEvidenceKnownFields :: ResolvedNames -> Id
idEvidenceAllFields :: ResolvedNames -> Id
dataConDictAny :: ResolvedNames -> DataCon
clsSubRow :: ResolvedNames -> Class
clsRowHasField :: ResolvedNames -> Class
clsKnownHash :: ResolvedNames -> Class
clsKnownFields :: ResolvedNames -> Class
clsAllFields :: ResolvedNames -> Class
..} CRowHasField{Type
FieldLabel
Fields
hasFieldTypeField :: Type
hasFieldTypeRow :: Type
hasFieldTypeLabel :: Type
hasFieldTypeKind :: Type
hasFieldRecord :: Fields
hasFieldLabel :: FieldLabel
hasFieldTypeField :: CRowHasField -> Type
hasFieldTypeRow :: CRowHasField -> Type
hasFieldTypeLabel :: CRowHasField -> Type
hasFieldTypeKind :: CRowHasField -> Type
hasFieldRecord :: CRowHasField -> Fields
hasFieldLabel :: CRowHasField -> FieldLabel
..} Int
i = do
    forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$
      DataCon -> [Type] -> [EvExpr] -> EvTerm
evDataConApp
        (Class -> DataCon
classDataCon Class
clsRowHasField)
        [Type]
typeArgsEvidence
        [ EvExpr -> [EvExpr] -> EvExpr
mkCoreApps (forall b. Id -> Expr b
Var Id
idEvidenceRowHasField) forall a b. (a -> b) -> a -> b
$ forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat [
              forall a b. (a -> b) -> [a] -> [b]
map forall b. Type -> Expr b
Type [Type]
typeArgsEvidence
            , [Integer -> EvExpr
mkUncheckedIntExpr forall a b. (a -> b) -> a -> b
$ forall a b. (Integral a, Num b) => a -> b
fromIntegral Int
i]
            ]
        ]
  where
    typeArgsEvidence :: [Type]
    typeArgsEvidence :: [Type]
typeArgsEvidence = [
          Type
hasFieldTypeKind
        , Type
hasFieldTypeLabel
        , Type
hasFieldTypeRow
        , Type
hasFieldTypeField
        ]

{-------------------------------------------------------------------------------
  Solver
-------------------------------------------------------------------------------}

solveRowHasField ::
     ResolvedNames
  -> Ct
  -> GenLocated CtLoc CRowHasField
  -> TcPluginM 'Solve (Maybe (EvTerm, Ct), [Ct])
solveRowHasField :: ResolvedNames
-> Ct
-> GenLocated CtLoc CRowHasField
-> TcPluginM 'Solve (Maybe (EvTerm, Ct), [Ct])
solveRowHasField ResolvedNames
_ Ct
_ (L CtLoc
_ CRowHasField{hasFieldLabel :: CRowHasField -> FieldLabel
hasFieldLabel = FieldVar Id
_}) =
    forall (m :: * -> *) a. Monad m => a -> m a
return (forall a. Maybe a
Nothing, [])
solveRowHasField ResolvedNames
rn Ct
orig (L CtLoc
loc hf :: CRowHasField
hf@CRowHasField{hasFieldLabel :: CRowHasField -> FieldLabel
hasFieldLabel = FieldKnown FieldName
name, Type
Fields
hasFieldTypeField :: Type
hasFieldTypeRow :: Type
hasFieldTypeLabel :: Type
hasFieldTypeKind :: Type
hasFieldRecord :: Fields
hasFieldTypeField :: CRowHasField -> Type
hasFieldTypeRow :: CRowHasField -> Type
hasFieldTypeLabel :: CRowHasField -> Type
hasFieldTypeKind :: CRowHasField -> Type
hasFieldRecord :: CRowHasField -> Fields
..}) =
    case FieldName -> Fields -> Maybe (Int, Type)
ParsedRow.lookup FieldName
name Fields
hasFieldRecord of
      Maybe (Int, Type)
Nothing ->
        -- TODO: If the record is fully known, we should issue a custom type
        -- error here rather than leaving the constraint unsolved
        forall (m :: * -> *) a. Monad m => a -> m a
return (forall a. Maybe a
Nothing, [])
      Just (Int
i, Type
typ) -> do
        CtEvidence
eq <- forall (m :: * -> *).
MonadTcPluginWork m =>
CtLoc -> Type -> m CtEvidence
newWanted CtLoc
loc forall a b. (a -> b) -> a -> b
$
                Role -> Type -> Type -> Type
mkPrimEqPredRole Role
Nominal
                  Type
hasFieldTypeField
                  Type
typ
        EvTerm
ev <- ResolvedNames -> CRowHasField -> Int -> TcPluginM 'Solve EvTerm
evidenceHasField ResolvedNames
rn CRowHasField
hf Int
i
        forall (m :: * -> *) a. Monad m => a -> m a
return (forall a. a -> Maybe a
Just (EvTerm
ev, Ct
orig), [CtEvidence -> Ct
mkNonCanonical CtEvidence
eq])