{-# 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
forall doc. IsLine doc => doc -> doc
parens (SDoc -> SDoc) -> SDoc -> SDoc
forall a b. (a -> b) -> a -> b
$
      String -> SDoc
forall doc. IsLine doc => String -> doc
text String
"CSubRow" SDoc -> SDoc -> SDoc
forall doc. IsLine doc => doc -> doc -> doc
<+> SDoc -> SDoc
forall doc. IsLine doc => doc -> doc
braces ([SDoc] -> SDoc
forall doc. IsDoc doc => [doc] -> doc
vcat [
          String -> SDoc
forall doc. IsLine doc => String -> doc
text String
"subrowParsedLHS"   SDoc -> SDoc -> SDoc
forall doc. IsLine doc => doc -> doc -> doc
<+> String -> SDoc
forall doc. IsLine doc => String -> doc
text String
"=" SDoc -> SDoc -> SDoc
forall doc. IsLine doc => doc -> doc -> doc
<+> Fields -> SDoc
forall a. Outputable a => a -> SDoc
ppr Fields
parsedLHS
        , String -> SDoc
forall doc. IsLine doc => String -> doc
text String
"subrowParsedRHS"   SDoc -> SDoc -> SDoc
forall doc. IsLine doc => doc -> doc -> doc
<+> String -> SDoc
forall doc. IsLine doc => String -> doc
text String
"=" SDoc -> SDoc -> SDoc
forall doc. IsLine doc => doc -> doc -> doc
<+> Fields -> SDoc
forall a. Outputable a => a -> SDoc
ppr Fields
parsedRHS
        , String -> SDoc
forall doc. IsLine doc => String -> doc
text String
"subrowTypeLHS"     SDoc -> SDoc -> SDoc
forall doc. IsLine doc => doc -> doc -> doc
<+> String -> SDoc
forall doc. IsLine doc => String -> doc
text String
"=" SDoc -> SDoc -> SDoc
forall doc. IsLine doc => doc -> doc -> doc
<+> Type -> SDoc
forall a. Outputable a => a -> SDoc
ppr Type
typeLHS
        , String -> SDoc
forall doc. IsLine doc => String -> doc
text String
"subrowTypeRHS"     SDoc -> SDoc -> SDoc
forall doc. IsLine doc => doc -> doc -> doc
<+> String -> SDoc
forall doc. IsLine doc => String -> doc
text String
"=" SDoc -> SDoc -> SDoc
forall doc. IsLine doc => doc -> doc -> doc
<+> Type -> SDoc
forall a. Outputable a => a -> SDoc
ppr Type
typeRHS
        , String -> SDoc
forall doc. IsLine doc => String -> doc
text String
"subrowTypeKind"    SDoc -> SDoc -> SDoc
forall doc. IsLine doc => doc -> doc -> doc
<+> String -> SDoc
forall doc. IsLine doc => String -> doc
text String
"=" SDoc -> SDoc -> SDoc
forall doc. IsLine doc => doc -> doc -> doc
<+> Type -> 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{Id
TyCon
DataCon
Class
clsAllFields :: Class
clsKnownFields :: Class
clsKnownHash :: Class
clsRowHasField :: Class
clsSubRow :: Class
dataConDictAny :: DataCon
idEvidenceAllFields :: Id
idEvidenceKnownFields :: Id
idEvidenceKnownHash :: Id
idEvidenceRowHasField :: Id
idEvidenceSubRow :: Id
idMkDictAny :: Id
tyConDictAny :: TyCon
tyConMerge :: TyCon
tyConFieldTypes :: TyCon
tyConPair :: TyCon
tyConSimpleFieldTypes :: TyCon
clsAllFields :: ResolvedNames -> Class
clsKnownFields :: ResolvedNames -> Class
clsKnownHash :: ResolvedNames -> Class
clsRowHasField :: ResolvedNames -> Class
clsSubRow :: ResolvedNames -> Class
dataConDictAny :: ResolvedNames -> DataCon
idEvidenceAllFields :: ResolvedNames -> Id
idEvidenceKnownFields :: ResolvedNames -> Id
idEvidenceKnownHash :: ResolvedNames -> Id
idEvidenceRowHasField :: ResolvedNames -> Id
idEvidenceSubRow :: ResolvedNames -> Id
idMkDictAny :: ResolvedNames -> Id
tyConDictAny :: ResolvedNames -> TyCon
tyConMerge :: ResolvedNames -> TyCon
tyConFieldTypes :: ResolvedNames -> TyCon
tyConPair :: ResolvedNames -> TyCon
tyConSimpleFieldTypes :: ResolvedNames -> TyCon
..} =
    Class
-> ([Type] -> Maybe CSubRow)
-> Ct
-> ParseResult Void (GenLocated CtLoc CSubRow)
forall a e.
HasCallStack =>
Class
-> ([Type] -> Maybe a) -> Ct -> ParseResult e (GenLocated CtLoc a)
parseConstraint' Class
clsSubRow (([Type] -> Maybe CSubRow)
 -> Ct -> ParseResult Void (GenLocated CtLoc CSubRow))
-> ([Type] -> Maybe CSubRow)
-> Ct
-> ParseResult Void (GenLocated CtLoc CSubRow)
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
          CSubRow -> Maybe CSubRow
forall a. a -> Maybe a
forall (m :: * -> *) a. Monad m => a -> m a
return (CSubRow -> Maybe CSubRow) -> CSubRow -> Maybe CSubRow
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]
_ -> String -> SDoc -> Maybe CSubRow
forall a. HasCallStack => String -> SDoc -> a
pprPanic String
"parseSubRow: expected 3 arguments" (SDoc -> Maybe CSubRow) -> SDoc -> Maybe CSubRow
forall a b. (a -> b) -> a -> b
$
               String -> SDoc
forall doc. IsLine doc => String -> doc
text String
"args" SDoc -> SDoc -> SDoc
forall doc. IsLine doc => doc -> doc -> doc
<+> [Type] -> 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{Id
TyCon
DataCon
Class
clsAllFields :: ResolvedNames -> Class
clsKnownFields :: ResolvedNames -> Class
clsKnownHash :: ResolvedNames -> Class
clsRowHasField :: ResolvedNames -> Class
clsSubRow :: ResolvedNames -> Class
dataConDictAny :: ResolvedNames -> DataCon
idEvidenceAllFields :: ResolvedNames -> Id
idEvidenceKnownFields :: ResolvedNames -> Id
idEvidenceKnownHash :: ResolvedNames -> Id
idEvidenceRowHasField :: ResolvedNames -> Id
idEvidenceSubRow :: ResolvedNames -> Id
idMkDictAny :: ResolvedNames -> Id
tyConDictAny :: ResolvedNames -> TyCon
tyConMerge :: ResolvedNames -> TyCon
tyConFieldTypes :: ResolvedNames -> TyCon
tyConPair :: ResolvedNames -> TyCon
tyConSimpleFieldTypes :: ResolvedNames -> TyCon
clsAllFields :: Class
clsKnownFields :: Class
clsKnownHash :: Class
clsRowHasField :: Class
clsSubRow :: Class
dataConDictAny :: DataCon
idEvidenceAllFields :: Id
idEvidenceKnownFields :: Id
idEvidenceKnownHash :: Id
idEvidenceRowHasField :: Id
idEvidenceSubRow :: Id
idMkDictAny :: Id
tyConDictAny :: TyCon
tyConMerge :: TyCon
tyConFieldTypes :: TyCon
tyConPair :: TyCon
tyConSimpleFieldTypes :: TyCon
..} CSubRow{Type
Fields
subrowParsedLHS :: CSubRow -> Fields
subrowParsedRHS :: CSubRow -> Fields
subrowTypeLHS :: CSubRow -> Type
subrowTypeRHS :: CSubRow -> Type
subrowTypeKind :: CSubRow -> Type
subrowParsedLHS :: Fields
subrowParsedRHS :: Fields
subrowTypeLHS :: Type
subrowTypeRHS :: Type
subrowTypeKind :: Type
..} [(Target (KnownField Type), Source (KnownRowField Type))]
fields = do
    EvTerm -> TcPluginM 'Solve EvTerm
forall a. a -> TcPluginM 'Solve a
forall (m :: * -> *) a. Monad m => a -> m a
return (EvTerm -> TcPluginM 'Solve EvTerm)
-> EvTerm -> TcPluginM 'Solve EvTerm
forall a b. (a -> b) -> a -> b
$
      DataCon -> [Type] -> [EvExpr] -> EvTerm
evDataConApp
        (Class -> DataCon
classDataCon Class
clsSubRow)
        [Type]
typeArgsEvidence
        [ EvExpr -> [EvExpr] -> EvExpr
mkCoreApps (Id -> EvExpr
forall b. Id -> Expr b
Var Id
idEvidenceSubRow) ([EvExpr] -> EvExpr) -> [EvExpr] -> EvExpr
forall a b. (a -> b) -> a -> b
$ [[EvExpr]] -> [EvExpr]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat [
              (Type -> EvExpr) -> [Type] -> [EvExpr]
forall a b. (a -> b) -> [a] -> [b]
map Type -> EvExpr
forall b. Type -> Expr b
Type [Type]
typeArgsEvidence
            , [ Type -> [EvExpr] -> EvExpr
mkListExpr Type
intTy ([EvExpr] -> EvExpr) -> [EvExpr] -> EvExpr
forall a b. (a -> b) -> a -> b
$
                  (Int -> EvExpr) -> [Int] -> [EvExpr]
forall a b. (a -> b) -> [a] -> [b]
map (Integer -> EvExpr
mkUncheckedIntExpr (Integer -> EvExpr) -> (Int -> Integer) -> Int -> EvExpr
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Int -> Integer
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 = ((Target (KnownField Type), Source (KnownRowField Type)) -> Int)
-> [(Target (KnownField Type), Source (KnownRowField Type))]
-> [Int]
forall a b. (a -> b) -> [a] -> [b]
map (KnownRowField Type -> Int
forall a. KnownRowField a -> Int
knownRowFieldIndex (KnownRowField Type -> Int)
-> ((Target (KnownField Type), Source (KnownRowField Type))
    -> KnownRowField Type)
-> (Target (KnownField Type), Source (KnownRowField Type))
-> Int
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Source (KnownRowField Type) -> KnownRowField Type
forall a. Source a -> a
getSource (Source (KnownRowField Type) -> KnownRowField Type)
-> ((Target (KnownField Type), Source (KnownRowField Type))
    -> Source (KnownRowField Type))
-> (Target (KnownField Type), Source (KnownRowField Type))
-> KnownRowField Type
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Target (KnownField Type), Source (KnownRowField Type))
-> Source (KnownRowField Type)
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
subrowParsedLHS :: CSubRow -> Fields
subrowParsedRHS :: CSubRow -> Fields
subrowTypeLHS :: CSubRow -> Type
subrowTypeRHS :: CSubRow -> Type
subrowTypeKind :: CSubRow -> Type
subrowParsedLHS :: Fields
subrowParsedRHS :: Fields
subrowTypeLHS :: Type
subrowTypeRHS :: Type
subrowTypeKind :: Type
..}) =
    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 KnownRow Type
-> KnownRow Type
-> Either
     NotSubRow [(Target (KnownField Type), Source (KnownRowField Type))]
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 <- [(Target (KnownField Type), Source (KnownRowField Type))]
-> ((Target (KnownField Type), Source (KnownRowField Type))
    -> TcPluginM 'Solve CtEvidence)
-> TcPluginM 'Solve [CtEvidence]
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 (((Target (KnownField Type), Source (KnownRowField Type))
  -> TcPluginM 'Solve CtEvidence)
 -> TcPluginM 'Solve [CtEvidence])
-> ((Target (KnownField Type), Source (KnownRowField Type))
    -> TcPluginM 'Solve CtEvidence)
-> TcPluginM 'Solve [CtEvidence]
forall a b. (a -> b) -> a -> b
$ \(Target KnownField Type
r, Source KnownRowField Type
l) -> CtLoc -> Type -> TcPluginM 'Solve CtEvidence
forall (m :: * -> *).
MonadTcPluginWork m =>
CtLoc -> Type -> m CtEvidence
newWanted CtLoc
loc (Type -> TcPluginM 'Solve CtEvidence)
-> Type -> TcPluginM 'Solve CtEvidence
forall a b. (a -> b) -> a -> b
$
                     Role -> Type -> Type -> Type
mkPrimEqPredRole
                       Role
Nominal
                       (KnownRowField Type -> Type
forall a. KnownRowField a -> a
knownRowFieldInfo KnownRowField Type
l)
                       (KnownField Type -> Type
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
            (Maybe (EvTerm, Ct), [Ct])
-> TcPluginM 'Solve (Maybe (EvTerm, Ct), [Ct])
forall a. a -> TcPluginM 'Solve a
forall (m :: * -> *) a. Monad m => a -> m a
return ((EvTerm, Ct) -> Maybe (EvTerm, Ct)
forall a. a -> Maybe a
Just (EvTerm
ev, Ct
orig), (CtEvidence -> Ct) -> [CtEvidence] -> [Ct]
forall a b. (a -> b) -> [a] -> [b]
map CtEvidence -> Ct
mkNonCanonical [CtEvidence]
eqs)
          Left NotSubRow
_err ->
            -- TODO: Return a custom error message
            (Maybe (EvTerm, Ct), [Ct])
-> TcPluginM 'Solve (Maybe (EvTerm, Ct), [Ct])
forall a. a -> TcPluginM 'Solve a
forall (m :: * -> *) a. Monad m => a -> m a
return (Maybe (EvTerm, Ct)
forall a. Maybe a
Nothing, [])
      (Maybe (KnownRow Type), Maybe (KnownRow Type))
_otherwise ->
        (Maybe (EvTerm, Ct), [Ct])
-> TcPluginM 'Solve (Maybe (EvTerm, Ct), [Ct])
forall a. a -> TcPluginM 'Solve a
forall (m :: * -> *) a. Monad m => a -> m a
return (Maybe (EvTerm, Ct)
forall a. Maybe a
Nothing, [])