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

module Data.Record.Anon.Internal.Plugin.TC.Constraints.KnownFields (
    CKnownFields(..)
  , parseKnownFields
  , solveKnownFields
  ) where

import Data.Void

import Data.Record.Anon.Internal.Plugin.TC.Row.KnownRow (KnownRow)
import Data.Record.Anon.Internal.Plugin.TC.Row.ParsedRow (Fields)
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.KnownField as KnownField
import qualified Data.Record.Anon.Internal.Plugin.TC.Row.KnownRow   as KnownRow
import qualified Data.Record.Anon.Internal.Plugin.TC.Row.ParsedRow  as ParsedRow

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

-- | Parsed form of a @KnownFields (r :: [(Symbol, Kind)]) @ constraint
data CKnownFields = CKnownFields {
      -- | Fields of the record
      CKnownFields -> Fields
knownFieldsParsedFields :: Fields

      -- | Type of the record fields (@r@)
    , CKnownFields -> Type
knownFieldsTypeRecord :: Type

      -- | Kind of the type information (@k@)
    , CKnownFields -> Type
knownFieldsTypeKind :: Type
    }

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

instance Outputable CKnownFields where
  ppr :: CKnownFields -> SDoc
ppr (CKnownFields Fields
parsedFields Type
typeRecord Type
typeKind) = SDoc -> SDoc
parens forall a b. (a -> b) -> a -> b
$
      String -> SDoc
text String
"CKnownFields" SDoc -> SDoc -> SDoc
<+> SDoc -> SDoc
braces ([SDoc] -> SDoc
vcat [
          String -> SDoc
text String
"knownFieldsParsedFields" SDoc -> SDoc -> SDoc
<+> String -> SDoc
text String
"=" SDoc -> SDoc -> SDoc
<+> forall a. Outputable a => a -> SDoc
ppr Fields
parsedFields
        , String -> SDoc
text String
"knownFieldsTypeRecord"   SDoc -> SDoc -> SDoc
<+> String -> SDoc
text String
"=" SDoc -> SDoc -> SDoc
<+> forall a. Outputable a => a -> SDoc
ppr Type
typeRecord
        , String -> SDoc
text String
"knownFieldsTypeKind"     SDoc -> SDoc -> SDoc
<+> String -> SDoc
text String
"=" SDoc -> SDoc -> SDoc
<+> forall a. Outputable a => a -> SDoc
ppr Type
typeKind
        ])

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

parseKnownFields ::
     TyConSubst
  -> ResolvedNames
  -> Ct
  -> ParseResult Void (GenLocated CtLoc CKnownFields)
parseKnownFields :: TyConSubst
-> ResolvedNames
-> Ct
-> ParseResult Void (GenLocated CtLoc CKnownFields)
parseKnownFields 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
clsKnownFields forall a b. (a -> b) -> a -> b
$ \case
      [Type
k, Type
r] -> do
        Fields
fields <- TyConSubst -> ResolvedNames -> Type -> Maybe Fields
ParsedRow.parseFields TyConSubst
tcs ResolvedNames
rn Type
r
        forall (m :: * -> *) a. Monad m => a -> m a
return CKnownFields {
            knownFieldsParsedFields :: Fields
knownFieldsParsedFields = Fields
fields
          , knownFieldsTypeRecord :: Type
knownFieldsTypeRecord   = Type
r
          , knownFieldsTypeKind :: Type
knownFieldsTypeKind     = Type
k
          }
      [Type]
_invalidNumArgs ->
        forall a. Maybe a
Nothing

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

-- | Construct evidence
--
-- For each field we need an evidence variable corresponding to the evidence
-- that that field name satisfies KnownSymbol.
evidenceKnownFields ::
     ResolvedNames
  -> CKnownFields
  -> KnownRow a
  -> TcPluginM 'Solve EvTerm
evidenceKnownFields :: forall a.
ResolvedNames
-> CKnownFields -> KnownRow a -> TcPluginM 'Solve EvTerm
evidenceKnownFields 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
..} CKnownFields{Type
Fields
knownFieldsTypeKind :: Type
knownFieldsTypeRecord :: Type
knownFieldsParsedFields :: Fields
knownFieldsTypeKind :: CKnownFields -> Type
knownFieldsTypeRecord :: CKnownFields -> Type
knownFieldsParsedFields :: CKnownFields -> Fields
..} KnownRow a
r = do
    [CoreExpr]
fields <- forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM forall a. KnownField a -> TcPluginM 'Solve CoreExpr
KnownField.toExpr (forall a. KnownRow a -> [KnownField a]
KnownRow.toList KnownRow a
r)
    forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$
      DataCon -> [Type] -> [CoreExpr] -> EvTerm
evDataConApp
        (Class -> DataCon
classDataCon Class
clsKnownFields)
        [Type]
typeArgsEvidence
        [ CoreExpr -> [CoreExpr] -> CoreExpr
mkCoreApps (forall b. Id -> Expr b
Var Id
idEvidenceKnownFields) 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
            , [ Type -> [CoreExpr] -> CoreExpr
mkListExpr Type
stringTy [CoreExpr]
fields ]
            ]
        ]
  where
    typeArgsEvidence :: [Type]
    typeArgsEvidence :: [Type]
typeArgsEvidence = [
          Type
knownFieldsTypeKind
        , Type
knownFieldsTypeRecord
        ]

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

solveKnownFields ::
     ResolvedNames
  -> Ct
  -> GenLocated CtLoc CKnownFields
  -> TcPluginM 'Solve (Maybe (EvTerm, Ct), [Ct])
solveKnownFields :: ResolvedNames
-> Ct
-> GenLocated CtLoc CKnownFields
-> TcPluginM 'Solve (Maybe (EvTerm, Ct), [Ct])
solveKnownFields ResolvedNames
rn Ct
orig (L CtLoc
_ cm :: CKnownFields
cm@CKnownFields{Type
Fields
knownFieldsTypeKind :: Type
knownFieldsTypeRecord :: Type
knownFieldsParsedFields :: Fields
knownFieldsTypeKind :: CKnownFields -> Type
knownFieldsTypeRecord :: CKnownFields -> Type
knownFieldsParsedFields :: CKnownFields -> Fields
..}) = do
    -- See 'solveRecordConstraints' for a discussion of 'allFieldsKnown'
    case Fields -> Maybe (KnownRow Type)
ParsedRow.allKnown Fields
knownFieldsParsedFields of
      Maybe (KnownRow Type)
Nothing ->
        forall (m :: * -> *) a. Monad m => a -> m a
return (forall a. Maybe a
Nothing, [])
      Just KnownRow Type
fields -> do
        EvTerm
ev <- forall a.
ResolvedNames
-> CKnownFields -> KnownRow a -> TcPluginM 'Solve EvTerm
evidenceKnownFields ResolvedNames
rn CKnownFields
cm KnownRow Type
fields
        forall (m :: * -> *) a. Monad m => a -> m a
return (forall a. a -> Maybe a
Just (EvTerm
ev, Ct
orig), [])