{-# 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.GhcTcPluginAPI
import Data.Record.Anon.Internal.Plugin.TC.NameResolution
import Data.Record.Anon.Internal.Plugin.TC.Parsing
import Data.Record.Anon.Internal.Plugin.TC.Row.KnownField (KnownField(..))
import Data.Record.Anon.Internal.Plugin.TC.Row.KnownRow (Source(..), Target (..), KnownRowField(..))
import Data.Record.Anon.Internal.Plugin.TC.Row.ParsedRow (Fields)
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
  -> [(Target (KnownField Type), Source (KnownRowField Type))]
  -> TcPluginM 'Solve EvTerm
evidenceSubRow :: ResolvedNames
-> CSubRow
-> [(Target (KnownField Type), Source (KnownRowField Type))]
-> 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
..} [(Target (KnownField Type), Source (KnownRowField Type))]
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]
indices ]
            ]
        ]
  where
    typeArgsEvidence :: [Type]
    typeArgsEvidence :: [Type]
typeArgsEvidence = [
          Type
subrowTypeKind
        , Type
subrowTypeLHS
        , Type
subrowTypeRHS
        ]

    -- Indices into the source array, in the order of the target array
    indices :: [Int]
    indices :: [Int]
indices = forall a b. (a -> b) -> [a] -> [b]
map (forall a. KnownRowField a -> Int
knownRowFieldIndex forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. Source a -> a
getSource forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b. (a, b) -> b
snd) [(Target (KnownField Type), Source (KnownRowField Type))]
fields

{-------------------------------------------------------------------------------
  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 KnownRow Type
rhs forall a b.
KnownRow a
-> KnownRow b
-> Either
     NotSubRow [(Target (KnownField a), Source (KnownRowField b))]
`KnownRow.isSubRowOf` KnownRow Type
lhs of
          Right [(Target (KnownField Type), Source (KnownRowField Type))]
inBoth -> do
            [CtEvidence]
eqs <- forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
t a -> (a -> m b) -> m (t b)
forM [(Target (KnownField Type), Source (KnownRowField Type))]
inBoth forall a b. (a -> b) -> a -> b
$ \(Target KnownField Type
r, Source KnownRowField Type
l) -> 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
                       (forall a. KnownRowField a -> a
knownRowFieldInfo KnownRowField Type
l)
                       (forall a. KnownField a -> a
knownFieldInfo KnownField Type
r)
            EvTerm
ev  <- ResolvedNames
-> CSubRow
-> [(Target (KnownField Type), Source (KnownRowField Type))]
-> TcPluginM 'Solve EvTerm
evidenceSubRow ResolvedNames
rn CSubRow
proj [(Target (KnownField Type), Source (KnownRowField 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, [])