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

module Data.Record.Anon.Internal.Plugin.TC.Solver (
    solve
  ) where

import Data.Bifunctor
import Data.Maybe (catMaybes)
import Data.Traversable (forM)

import Data.Record.Anon.Internal.Plugin.TC.Constraints.AllFields
import Data.Record.Anon.Internal.Plugin.TC.Constraints.KnownFields
import Data.Record.Anon.Internal.Plugin.TC.Constraints.KnownHash
import Data.Record.Anon.Internal.Plugin.TC.Constraints.RowHasField
import Data.Record.Anon.Internal.Plugin.TC.Constraints.SubRow
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

{-------------------------------------------------------------------------------
  Top-level solver
-------------------------------------------------------------------------------}

solve :: ResolvedNames -> TcPluginSolver
solve :: ResolvedNames -> TcPluginSolver
solve ResolvedNames
rn [Ct]
given [Ct]
wanted =
--  trace _debugInput  $
--  trace _debugParsed $
    do ([(EvTerm, Ct)]
solved, [Ct]
new) <- forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (forall (p :: * -> * -> *) a b c d.
Bifunctor p =>
(a -> b) -> (c -> d) -> p a c -> p b d
bimap forall a. [Maybe a] -> [a]
catMaybes forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b. [(a, b)] -> ([a], [b])
unzip) forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) a. Applicative m => [m [a]] -> m [a]
concatM [
           forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
t a -> (a -> m b) -> m (t b)
forM [(Ct, GenLocated CtLoc CAllFields)]
parsedAllFields   forall a b. (a -> b) -> a -> b
$ forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry (ResolvedNames
-> Ct
-> GenLocated CtLoc CAllFields
-> TcPluginM 'Solve (Maybe (EvTerm, Ct), [Ct])
solveAllFields   ResolvedNames
rn)
         , forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
t a -> (a -> m b) -> m (t b)
forM [(Ct, GenLocated CtLoc CKnownFields)]
parsedKnownFields forall a b. (a -> b) -> a -> b
$ forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry (ResolvedNames
-> Ct
-> GenLocated CtLoc CKnownFields
-> TcPluginM 'Solve (Maybe (EvTerm, Ct), [Ct])
solveKnownFields ResolvedNames
rn)
         , forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
t a -> (a -> m b) -> m (t b)
forM [(Ct, GenLocated CtLoc CKnownHash)]
parsedKnownHash   forall a b. (a -> b) -> a -> b
$ forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry (ResolvedNames
-> Ct
-> GenLocated CtLoc CKnownHash
-> TcPluginM 'Solve (Maybe (EvTerm, Ct), [Ct])
solveKnownHash   ResolvedNames
rn)
         , forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
t a -> (a -> m b) -> m (t b)
forM [(Ct, GenLocated CtLoc CRowHasField)]
parsedRowHasField forall a b. (a -> b) -> a -> b
$ forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry (ResolvedNames
-> Ct
-> GenLocated CtLoc CRowHasField
-> TcPluginM 'Solve (Maybe (EvTerm, Ct), [Ct])
solveRowHasField ResolvedNames
rn)
         , forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
t a -> (a -> m b) -> m (t b)
forM [(Ct, GenLocated CtLoc CSubRow)]
parsedSubRow      forall a b. (a -> b) -> a -> b
$ forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry (ResolvedNames
-> Ct
-> GenLocated CtLoc CSubRow
-> TcPluginM 'Solve (Maybe (EvTerm, Ct), [Ct])
solveSubRow      ResolvedNames
rn)
         ]
       forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ [(EvTerm, Ct)] -> [Ct] -> TcPluginSolveResult
TcPluginOk [(EvTerm, Ct)]
solved [Ct]
new
  where
    tcs :: TyConSubst
    tcs :: TyConSubst
tcs = [Ct] -> TyConSubst
mkTyConSubst [Ct]
given

    parsedAllFields   :: [(Ct, GenLocated CtLoc CAllFields)]
    parsedKnownFields :: [(Ct, GenLocated CtLoc CKnownFields)]
    parsedKnownHash   :: [(Ct, GenLocated CtLoc CKnownHash)]
    parsedRowHasField :: [(Ct, GenLocated CtLoc CRowHasField)]
    parsedSubRow      :: [(Ct, GenLocated CtLoc CSubRow)]

    parsedAllFields :: [(Ct, GenLocated CtLoc CAllFields)]
parsedAllFields   = forall a b. (a -> ParseResult Void b) -> [a] -> [b]
parseAll' (forall a e b. (a -> ParseResult e b) -> a -> ParseResult e (a, b)
withOrig (TyConSubst
-> ResolvedNames
-> Ct
-> ParseResult Void (GenLocated CtLoc CAllFields)
parseAllFields   TyConSubst
tcs ResolvedNames
rn)) [Ct]
wanted
    parsedKnownFields :: [(Ct, GenLocated CtLoc CKnownFields)]
parsedKnownFields = forall a b. (a -> ParseResult Void b) -> [a] -> [b]
parseAll' (forall a e b. (a -> ParseResult e b) -> a -> ParseResult e (a, b)
withOrig (TyConSubst
-> ResolvedNames
-> Ct
-> ParseResult Void (GenLocated CtLoc CKnownFields)
parseKnownFields TyConSubst
tcs ResolvedNames
rn)) [Ct]
wanted
    parsedKnownHash :: [(Ct, GenLocated CtLoc CKnownHash)]
parsedKnownHash   = forall a b. (a -> ParseResult Void b) -> [a] -> [b]
parseAll' (forall a e b. (a -> ParseResult e b) -> a -> ParseResult e (a, b)
withOrig (TyConSubst
-> ResolvedNames
-> Ct
-> ParseResult Void (GenLocated CtLoc CKnownHash)
parseKnownHash   TyConSubst
tcs ResolvedNames
rn)) [Ct]
wanted
    parsedRowHasField :: [(Ct, GenLocated CtLoc CRowHasField)]
parsedRowHasField = forall a b. (a -> ParseResult Void b) -> [a] -> [b]
parseAll' (forall a e b. (a -> ParseResult e b) -> a -> ParseResult e (a, b)
withOrig (HasCallStack =>
TyConSubst
-> ResolvedNames
-> Ct
-> ParseResult Void (GenLocated CtLoc CRowHasField)
parseRowHasField TyConSubst
tcs ResolvedNames
rn)) [Ct]
wanted
    parsedSubRow :: [(Ct, GenLocated CtLoc CSubRow)]
parsedSubRow      = forall a b. (a -> ParseResult Void b) -> [a] -> [b]
parseAll' (forall a e b. (a -> ParseResult e b) -> a -> ParseResult e (a, b)
withOrig (TyConSubst
-> ResolvedNames
-> Ct
-> ParseResult Void (GenLocated CtLoc CSubRow)
parseSubRow      TyConSubst
tcs ResolvedNames
rn)) [Ct]
wanted

    _debugInput :: String
    _debugInput :: String
_debugInput = [String] -> String
unlines [
          String
"*** input"
        , forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat [
              String
"given:"
            , SDoc -> String
showSDocUnsafe (forall a. Outputable a => a -> SDoc
ppr [Ct]
given)
            ]
        , forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat [
              String
"wanted: "
            , SDoc -> String
showSDocUnsafe (forall a. Outputable a => a -> SDoc
ppr [Ct]
wanted)
            ]
        ]

    _debugParsed :: String
    _debugParsed :: String
_debugParsed = [String] -> String
unlines [
          String
"*** parsed"
        , forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat [String
"parsedAllFields:   ", SDoc -> String
showSDocUnsafe forall a b. (a -> b) -> a -> b
$ forall a. Outputable a => a -> SDoc
ppr [(Ct, GenLocated CtLoc CAllFields)]
parsedAllFields]
        , forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat [String
"parsedKnownFields: ", SDoc -> String
showSDocUnsafe forall a b. (a -> b) -> a -> b
$ forall a. Outputable a => a -> SDoc
ppr [(Ct, GenLocated CtLoc CKnownFields)]
parsedKnownFields]
        , forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat [String
"parsedKnownHash:   ", SDoc -> String
showSDocUnsafe forall a b. (a -> b) -> a -> b
$ forall a. Outputable a => a -> SDoc
ppr [(Ct, GenLocated CtLoc CKnownFields)]
parsedKnownFields]
        , forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat [String
"parsedRowHasField: ", SDoc -> String
showSDocUnsafe forall a b. (a -> b) -> a -> b
$ forall a. Outputable a => a -> SDoc
ppr [(Ct, GenLocated CtLoc CRowHasField)]
parsedRowHasField]
        , forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat [String
"parsedSubRow:      ", SDoc -> String
showSDocUnsafe forall a b. (a -> b) -> a -> b
$ forall a. Outputable a => a -> SDoc
ppr [(Ct, GenLocated CtLoc CSubRow)]
parsedSubRow]
        , forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat [String
"tcs (TyConSubst):  ", SDoc -> String
showSDocUnsafe forall a b. (a -> b) -> a -> b
$ forall a. Outputable a => a -> SDoc
ppr TyConSubst
tcs]
        ]

{-------------------------------------------------------------------------------
  Auxiliary
-------------------------------------------------------------------------------}

concatM :: Applicative m => [m [a]] -> m [a]
concatM :: forall (m :: * -> *) a. Applicative m => [m [a]] -> m [a]
concatM = forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (t :: * -> *) (f :: * -> *) a.
(Traversable t, Applicative f) =>
t (f a) -> f (t a)
sequenceA