{-# LANGUAGE CPP #-}
{-# LANGUAGE BlockArguments #-}
{-# LANGUAGE ViewPatterns #-}
{-# LANGUAGE DerivingVia #-}
{-# OPTIONS_GHC -Wno-x-partial -Wno-incomplete-uni-patterns -Wno-unused-imports #-}
-- | @Read@ synthesizer: builds @readPrec@ exactly as GHC's derived @Read@ does
-- (the @ReadPrec@ combinators via "Stock.Internal"'s 'buildReadPrecBody'), so
-- @readsPrec@ — from the class default — is byte-faithful, including the order
-- of ambiguous infix parses.
module Stock.Read where
-- Most names below (data-con/type builders, coercion builders, occ-name
-- helpers, …) are re-exported by 'GHC.Plugins', so we only import explicitly
-- the ones it does not provide.
import GHC.Plugins hiding (TcPlugin)
import GHC.Tc.Plugin
import GHC.Tc.Types
import GHC.Tc.Types.Constraint
#if MIN_VERSION_ghc(9,12,0)
import GHC.Tc.Types.CtLoc (CtLoc)
#else
import GHC.Tc.Types.Constraint (CtLoc)
#endif
import GHC.Tc.Types.Evidence
import GHC.Tc.Utils.Monad (addErrTc)
import GHC.Tc.Errors.Types (mkTcRnUnknownMessage)
import GHC.Types.Error (mkPlainError, noHints)
import GHC.Core.Class (Class, className, classMethods, classOpItems, classTyCon)
import GHC.Core.Predicate (classifyPredType, Pred(ClassPred), mkClassPred)
import GHC.Builtin.Types.Prim (intPrimTy)
import GHC.Builtin.PrimOps (PrimOp(TagToEnumOp))
import GHC.Builtin.PrimOps.Ids (primOpId)
import GHC.Builtin.Names ( eqClassName, ordClassName, appendName
                         , enumClassName, mapName, numClassName
                         , enumFromToName, enumFromThenToName
                         , eqStringName
                         , genClassName, repTyConName, u1TyConName, k1TyConName
                         , prodTyConName, sumTyConName
                         , monoidClassName, foldableClassName, functorClassName
                         , semigroupClassName, monadClassName )
import Stock.Compat ( gHC_INTERNAL_SHOW, gHC_INTERNAL_READ
                    , gHC_INTERNAL_LIST, gHC_INTERNAL_GENERICS
                    , tEXT_READPREC, tEXT_READ_LEX )
import GHC.Core.Reduction (mkReduction)
import GHC.Core.TyCo.Rep (UnivCoProvenance(PluginProv))
import GHC.Rename.Fixity (lookupFixityRn)
import GHC.Types.Fixity (Fixity(..), defaultFixity)
import GHC.Core.TyCo.Compare (eqType)
import GHC.Core.Multiplicity (scaledThing)
import GHC.Core.SimpleOpt (defaultSimpleOpts)
import GHC.Core.Unfold.Make (mkInlineUnfoldingWithArity)
import GHC.Core.InstEnv (classInstances, is_dfun, is_tys)
import GHC.Runtime.Loader (getValueSafely)
import Stock.Derive
import Data.Maybe (catMaybes, fromJust, isJust, fromMaybe)
import qualified Data.Monoid as Mon (Alt(..))  -- 'Alt' clashes with GHC.Core's case-alt 'Alt'
import Stock.Trans (MaybeT(..))
import Control.Monad (forM, zipWithM, unless, guard)
import Data.IORef (IORef, newIORef, readIORef, modifyIORef')
import Stock.Internal

synthRead :: Class -> CtLoc -> Type -> Type -> Coercion -> [(DataCon, [Coercion])]
          -> TcPluginM (EvTerm, [Ct])
synthRead :: Class
-> CtLoc
-> Type
-> Type
-> Coercion
-> [(DataCon, [Coercion])]
-> TcPluginM (EvTerm, [Ct])
synthRead Class
cls CtLoc
loc Type
wrappedTy Type
innerTy Coercion
co [(DataCon, [Coercion])]
dcons = do
  (ReadPrecEnv
env, Ct
monadCt) <- CtLoc -> TcPluginM (ReadPrecEnv, Ct)
lookupReadPrecEnv CtLoc
loc
  let readPrecSel :: Id
readPrecSel = String -> Class -> Id
classMethod String
"readPrec" Class
cls
      toWrapped :: Expr b -> Expr b
toWrapped Expr b
e = Expr b -> Coercion -> Expr b
forall b. Expr b -> Coercion -> Expr b
Cast Expr b
e (Coercion -> Coercion
mkSymCo Coercion
co)
  -- each field is read at its modifier type @ft@ (= coercionRKind of its
  -- coercion) via that type's own @readPrec@, then coerced back to the real
  -- field type when the constructor is built.
  ([(DataCon, [(Type, Expr Id)], [Coercion])]
cons, [[CtEvidence]]
evss) <- ([((DataCon, [(Type, Expr Id)], [Coercion]), [CtEvidence])]
 -> ([(DataCon, [(Type, Expr Id)], [Coercion])], [[CtEvidence]]))
-> TcPluginM
     [((DataCon, [(Type, Expr Id)], [Coercion]), [CtEvidence])]
-> TcPluginM
     ([(DataCon, [(Type, Expr Id)], [Coercion])], [[CtEvidence]])
forall a b. (a -> b) -> TcPluginM a -> TcPluginM b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap [((DataCon, [(Type, Expr Id)], [Coercion]), [CtEvidence])]
-> ([(DataCon, [(Type, Expr Id)], [Coercion])], [[CtEvidence]])
forall a b. [(a, b)] -> ([a], [b])
unzip (TcPluginM
   [((DataCon, [(Type, Expr Id)], [Coercion]), [CtEvidence])]
 -> TcPluginM
      ([(DataCon, [(Type, Expr Id)], [Coercion])], [[CtEvidence]]))
-> TcPluginM
     [((DataCon, [(Type, Expr Id)], [Coercion]), [CtEvidence])]
-> TcPluginM
     ([(DataCon, [(Type, Expr Id)], [Coercion])], [[CtEvidence]])
forall a b. (a -> b) -> a -> b
$ [(DataCon, [Coercion])]
-> ((DataCon, [Coercion])
    -> TcPluginM
         ((DataCon, [(Type, Expr Id)], [Coercion]), [CtEvidence]))
-> TcPluginM
     [((DataCon, [(Type, Expr Id)], [Coercion]), [CtEvidence])]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
t a -> (a -> m b) -> m (t b)
forM [(DataCon, [Coercion])]
dcons \(DataCon
dc, [Coercion]
cosI) -> do
    let fts :: [Type]
fts = (Coercion -> Type) -> [Coercion] -> [Type]
forall a b. (a -> b) -> [a] -> [b]
map Coercion -> Type
coercionRKind [Coercion]
cosI
    [CtEvidence]
fieldEvs <- (Type -> TcPluginM CtEvidence) -> [Type] -> TcPluginM [CtEvidence]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [b]
mapM (\Type
ft -> CtLoc -> Type -> TcPluginM CtEvidence
newWanted CtLoc
loc (Class -> [Type] -> Type
mkClassPred Class
cls [Type
ft])) [Type]
fts
    let readers :: [(Type, Expr Id)]
readers = [ (Type
ft, Expr Id -> [Expr Id] -> Expr Id
forall b. Expr b -> [Expr b] -> Expr b
mkApps (Id -> Expr Id
forall b. Id -> Expr b
Var Id
readPrecSel) [Type -> Expr Id
forall b. Type -> Expr b
Type Type
ft, HasDebugCallStack => CtEvidence -> Expr Id
CtEvidence -> Expr Id
ctEvExpr CtEvidence
ev])
                  | (Type
ft, CtEvidence
ev) <- [Type] -> [CtEvidence] -> [(Type, CtEvidence)]
forall a b. [a] -> [b] -> [(a, b)]
zip [Type]
fts [CtEvidence]
fieldEvs ]
    ((DataCon, [(Type, Expr Id)], [Coercion]), [CtEvidence])
-> TcPluginM
     ((DataCon, [(Type, Expr Id)], [Coercion]), [CtEvidence])
forall a. a -> TcPluginM a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ((DataCon
dc, [(Type, Expr Id)]
readers, [Coercion]
cosI), [CtEvidence]
fieldEvs)
  let cosMap :: [(Unique, [Coercion])]
cosMap = [ (DataCon -> Unique
forall a. Uniquable a => a -> Unique
getUnique DataCon
dc, [Coercion]
cosI) | (DataCon
dc, [(Type, Expr Id)]
_, [Coercion]
cosI) <- [(DataCon, [(Type, Expr Id)], [Coercion])]
cons ]
      mkConVal :: DataCon -> [Id] -> Expr Id
mkConVal DataCon
dc [Id]
argIds =
        let cosI :: [Coercion]
cosI = Maybe [Coercion] -> [Coercion]
forall a. HasCallStack => Maybe a -> a
fromJust (Unique -> [(Unique, [Coercion])] -> Maybe [Coercion]
forall a b. Eq a => a -> [(a, b)] -> Maybe b
lookup (DataCon -> Unique
forall a. Uniquable a => a -> Unique
getUnique DataCon
dc) [(Unique, [Coercion])]
cosMap)
        in Expr Id -> Expr Id
forall {b}. Expr b -> Expr b
toWrapped (Type -> DataCon -> [Expr Id] -> Expr Id
conAppAt Type
innerTy DataCon
dc
             ((Id -> Coercion -> Expr Id) -> [Id] -> [Coercion] -> [Expr Id]
forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
zipWith (\Id
a Coercion
c -> Expr Id -> Coercion -> Expr Id
castInto (Id -> Expr Id
forall b. Id -> Expr b
Var Id
a) (Coercion -> Coercion
mkSymCo Coercion
c)) [Id]
argIds [Coercion]
cosI))
  Expr Id
body <- ReadPrecEnv
-> Type
-> (DataCon -> [Id] -> Expr Id)
-> [(DataCon, [(Type, Expr Id)])]
-> TcPluginM (Expr Id)
buildReadPrecBody ReadPrecEnv
env Type
wrappedTy DataCon -> [Id] -> Expr Id
mkConVal [ (DataCon
dc, [(Type, Expr Id)]
rs) | (DataCon
dc, [(Type, Expr Id)]
rs, [Coercion]
_) <- [(DataCon, [(Type, Expr Id)], [Coercion])]
cons ]
  Expr Id
dict <- Class
-> Type -> [Expr Id] -> [(Int, Expr Id)] -> TcPluginM (Expr Id)
recDictWith Class
cls Type
wrappedTy [] [(Int
2, Expr Id
body)]
  (EvTerm, [Ct]) -> TcPluginM (EvTerm, [Ct])
forall a. a -> TcPluginM a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Expr Id -> EvTerm
EvExpr Expr Id
dict, Ct
monadCt Ct -> [Ct] -> [Ct]
forall a. a -> [a] -> [a]
: (CtEvidence -> Ct) -> [CtEvidence] -> [Ct]
forall a b. (a -> b) -> [a] -> [b]
map CtEvidence -> Ct
mkNonCanonical ([[CtEvidence]] -> [CtEvidence]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat [[CtEvidence]]
evss))

-- | Synthesize @Generic (Stock T)@ for any single-level ADT.  @Rep@ is a
-- balanced @:+:@ tree of constructors (one constructor ⇒ no @:+:@), each a
-- balanced @:*:@ tree of @Rec0 field@ (or @U1@ if no fields).  @from@ matches
-- the real constructor, builds its product value and injects it into the sum
-- with @L1@\/@R1@; @to@ projects through the @:+:@\/@:*:@ structure and
-- rebuilds.  All casts go through the same plugin coercion the rewriter
-- asserts.  @K1@\/@:+:@\/@:*:@ layers: @K1@ is a newtype (coercion), @:+:@ and
-- @:*:@ are real data (constructed/matched).