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

module Data.Record.Anon.Internal.Plugin.TC.Constraints.SubRow (
    CSubRow(..)
  , parseSubRow
  , solveSubRow
  ) where

import Control.Monad (forM)
import Data.Void

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

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

-- | Parsed form of @SubRow@
--
-- > SubRow (r :: [(Symbol, k)]) (r' :: [(Symbol, k)])
data CSubRow = CSubRow {
      -- | Fields on the LHS
      CSubRow -> Fields
subrowParsedLHS :: Fields

      -- | Fields on the RHS
    , CSubRow -> Fields
subrowParsedRHS :: Fields

      -- | Left-hand side (@r@)
    , CSubRow -> Type
subrowTypeLHS :: Type

      -- | Right-hand side (@r'@)
    , CSubRow -> Type
subrowTypeRHS :: Type

      -- | Functor argument kind (@k@)
    , CSubRow -> Type
subrowTypeKind :: Type
    }

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

instance Outputable CSubRow where
  ppr :: CSubRow -> SDoc
ppr (CSubRow Fields
parsedLHS Fields
parsedRHS Type
typeLHS Type
typeRHS Type
typeKind) = SDoc -> SDoc
parens forall a b. (a -> b) -> a -> b
$
      String -> SDoc
text String
"CSubRow" SDoc -> SDoc -> SDoc
<+> SDoc -> SDoc
braces ([SDoc] -> SDoc
vcat [
          String -> SDoc
text String
"subrowParsedLHS"   SDoc -> SDoc -> SDoc
<+> String -> SDoc
text String
"=" SDoc -> SDoc -> SDoc
<+> forall a. Outputable a => a -> SDoc
ppr Fields
parsedLHS
        , String -> SDoc
text String
"subrowParsedRHS"   SDoc -> SDoc -> SDoc
<+> String -> SDoc
text String
"=" SDoc -> SDoc -> SDoc
<+> forall a. Outputable a => a -> SDoc
ppr Fields
parsedRHS
        , String -> SDoc
text String
"subrowTypeLHS"     SDoc -> SDoc -> SDoc
<+> String -> SDoc
text String
"=" SDoc -> SDoc -> SDoc
<+> forall a. Outputable a => a -> SDoc
ppr Type
typeLHS
        , String -> SDoc
text String
"subrowTypeRHS"     SDoc -> SDoc -> SDoc
<+> String -> SDoc
text String
"=" SDoc -> SDoc -> SDoc
<+> forall a. Outputable a => a -> SDoc
ppr Type
typeRHS
        , String -> SDoc
text String
"subrowTypeKind"    SDoc -> SDoc -> SDoc
<+> String -> SDoc
text String
"=" SDoc -> SDoc -> SDoc
<+> forall a. Outputable a => a -> SDoc
ppr Type
typeKind
        ])

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

parseSubRow ::
     TyConSubst
  -> ResolvedNames
  -> Ct
  -> ParseResult Void (GenLocated CtLoc CSubRow)
parseSubRow :: TyConSubst
-> ResolvedNames
-> Ct
-> ParseResult Void (GenLocated CtLoc CSubRow)
parseSubRow 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
clsSubRow forall a b. (a -> b) -> a -> b
$ \ [Type]
args ->
      case [Type]
args of
        [Type
typeKind, Type
typeLHS, Type
typeRHS] -> do
          Fields
fieldsLHS <- TyConSubst -> ResolvedNames -> Type -> Maybe Fields
ParsedRow.parseFields TyConSubst
tcs ResolvedNames
rn Type
typeLHS
          Fields
fieldsRHS <- TyConSubst -> ResolvedNames -> Type -> Maybe Fields
ParsedRow.parseFields TyConSubst
tcs ResolvedNames
rn Type
typeRHS
          forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ CSubRow {
                subrowParsedLHS :: Fields
subrowParsedLHS = Fields
fieldsLHS
              , subrowParsedRHS :: Fields
subrowParsedRHS = Fields
fieldsRHS
              , subrowTypeLHS :: Type
subrowTypeLHS   = Type
typeLHS
              , subrowTypeRHS :: Type
subrowTypeRHS   = Type
typeRHS
              , subrowTypeKind :: Type
subrowTypeKind  = Type
typeKind
              }
        [Type]
_ -> forall a. HasCallStack => String -> SDoc -> a
pprPanic String
"parseSubRow: expected 3 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
-------------------------------------------------------------------------------}

evidenceSubRow ::
     ResolvedNames
  -> CSubRow
  -> [Int]
  -> TcPluginM 'Solve EvTerm
evidenceSubRow :: ResolvedNames -> CSubRow -> [Int] -> TcPluginM 'Solve EvTerm
evidenceSubRow 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
..} CSubRow{Type
Fields
subrowTypeKind :: Type
subrowTypeRHS :: Type
subrowTypeLHS :: Type
subrowParsedRHS :: Fields
subrowParsedLHS :: Fields
subrowTypeKind :: CSubRow -> Type
subrowTypeRHS :: CSubRow -> Type
subrowTypeLHS :: CSubRow -> Type
subrowParsedRHS :: CSubRow -> Fields
subrowParsedLHS :: CSubRow -> Fields
..} [Int]
fields = 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
clsSubRow)
        [Type]
typeArgsEvidence
        [ EvExpr -> [EvExpr] -> EvExpr
mkCoreApps (forall b. Id -> Expr b
Var Id
idEvidenceSubRow) 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 -> [EvExpr] -> EvExpr
mkListExpr Type
intTy forall a b. (a -> b) -> a -> b
$
                  forall a b. (a -> b) -> [a] -> [b]
map (Integer -> EvExpr
mkUncheckedIntExpr forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b. (Integral a, Num b) => a -> b
fromIntegral) [Int]
fields ]
            ]
        ]
  where
    typeArgsEvidence :: [Type]
    typeArgsEvidence :: [Type]
typeArgsEvidence = [
          Type
subrowTypeKind
        , Type
subrowTypeLHS
        , Type
subrowTypeRHS
        ]

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

solveSubRow ::
     ResolvedNames
  -> Ct
  -> GenLocated CtLoc CSubRow
  -> TcPluginM 'Solve (Maybe (EvTerm, Ct), [Ct])
solveSubRow :: ResolvedNames
-> Ct
-> GenLocated CtLoc CSubRow
-> TcPluginM 'Solve (Maybe (EvTerm, Ct), [Ct])
solveSubRow ResolvedNames
rn Ct
orig (L CtLoc
loc proj :: CSubRow
proj@CSubRow{Type
Fields
subrowTypeKind :: Type
subrowTypeRHS :: Type
subrowTypeLHS :: Type
subrowParsedRHS :: Fields
subrowParsedLHS :: Fields
subrowTypeKind :: CSubRow -> Type
subrowTypeRHS :: CSubRow -> Type
subrowTypeLHS :: CSubRow -> Type
subrowParsedRHS :: CSubRow -> Fields
subrowParsedLHS :: CSubRow -> Fields
..}) =
    case ( Fields -> Maybe (KnownRow Type)
ParsedRow.allKnown Fields
subrowParsedLHS
         , Fields -> Maybe (KnownRow Type)
ParsedRow.allKnown Fields
subrowParsedRHS
         ) of
      (Just KnownRow Type
lhs, Just KnownRow Type
rhs) ->
        case forall a b.
KnownRow a -> KnownRow b -> Either NotSubRow [(Int, (a, b))]
KnownRow.isSubRow KnownRow Type
lhs KnownRow Type
rhs of
          Right [(Int, (Type, Type))]
inBoth -> do
            [CtEvidence]
eqs <- forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
t a -> (a -> m b) -> m (t b)
forM [(Int, (Type, Type))]
inBoth forall a b. (a -> b) -> a -> b
$ \(Int
_i, (Type
l, Type
r)) ->
                     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
l Type
r
            EvTerm
ev  <- ResolvedNames -> CSubRow -> [Int] -> TcPluginM 'Solve EvTerm
evidenceSubRow ResolvedNames
rn CSubRow
proj (forall a b. (a -> b) -> [a] -> [b]
map forall a b. (a, b) -> a
fst [(Int, (Type, Type))]
inBoth)
            forall (m :: * -> *) a. Monad m => a -> m a
return (forall a. a -> Maybe a
Just (EvTerm
ev, Ct
orig), forall a b. (a -> b) -> [a] -> [b]
map CtEvidence -> Ct
mkNonCanonical [CtEvidence]
eqs)
          Left NotSubRow
_err ->
            -- TODO: Return a custom error message
            forall (m :: * -> *) a. Monad m => a -> m a
return (forall a. Maybe a
Nothing, [])
      (Maybe (KnownRow Type), Maybe (KnownRow Type))
_otherwise ->
        forall (m :: * -> *) a. Monad m => a -> m a
return (forall a. Maybe a
Nothing, [])