{-# LANGUAGE CPP #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE TemplateHaskellQuotes #-}

{-# OPTIONS_GHC -Wno-unused-matches #-}

module GHC.TypeLits.Extra.Solver.Compat where

import qualified Language.Haskell.TH as TH

import GHC.TcPlugin.API

import GHC.TypeLits.Normalise.Compat

import GHC.Builtin.Names
  ( eqPrimTyConKey, hasKey
  )
#if MIN_VERSION_ghc(9,1,0)
import GHC.Builtin.Types
  ( boolTy, promotedFalseDataCon, promotedTrueDataCon
  )
#endif
import GHC.Builtin.Types.Literals
  ( typeNatDivTyCon, typeNatModTyCon
  )
#if MIN_VERSION_ghc(9,8,0)
import GHC.Tc.Types.Constraint
  ( DictCt(..), EqCt(..), IrredCt(..)
  )
#endif
import GHC.Tc.Types.Constraint
  ( Ct (..), qci_ev
  )

import qualified GHC.TypeLits.Extra

data ExtraDefs = ExtraDefs
  { ExtraDefs -> TyCon
maxTyCon  :: TyCon
  , ExtraDefs -> TyCon
minTyCon  :: TyCon
  , ExtraDefs -> TyCon
divTyCon  :: TyCon
  , ExtraDefs -> TyCon
modTyCon  :: TyCon
  , ExtraDefs -> TyCon
flogTyCon :: TyCon
  , ExtraDefs -> TyCon
clogTyCon :: TyCon
  , ExtraDefs -> TyCon
logTyCon  :: TyCon
  , ExtraDefs -> TyCon
gcdTyCon  :: TyCon
  , ExtraDefs -> TyCon
lcmTyCon  :: TyCon
  , ExtraDefs -> LookedUpTyCons
ordTyCons :: LookedUpTyCons
  }

-- | Find the \"magic\" classes and instances in "GHC.TypeLits.KnownNat"
lookupExtraDefs :: TcPluginM 'Init ExtraDefs
lookupExtraDefs :: TcPluginM 'Init ExtraDefs
lookupExtraDefs = do
    TyCon
-> TyCon
-> TyCon
-> TyCon
-> TyCon
-> TyCon
-> TyCon
-> TyCon
-> TyCon
-> LookedUpTyCons
-> ExtraDefs
ExtraDefs (TyCon
 -> TyCon
 -> TyCon
 -> TyCon
 -> TyCon
 -> TyCon
 -> TyCon
 -> TyCon
 -> TyCon
 -> LookedUpTyCons
 -> ExtraDefs)
-> TcPluginM 'Init TyCon
-> TcPluginM
     'Init
     (TyCon
      -> TyCon
      -> TyCon
      -> TyCon
      -> TyCon
      -> TyCon
      -> TyCon
      -> TyCon
      -> LookedUpTyCons
      -> ExtraDefs)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Name -> TcPluginM 'Init TyCon
look ''GHC.TypeLits.Extra.Max
              TcPluginM
  'Init
  (TyCon
   -> TyCon
   -> TyCon
   -> TyCon
   -> TyCon
   -> TyCon
   -> TyCon
   -> TyCon
   -> LookedUpTyCons
   -> ExtraDefs)
-> TcPluginM 'Init TyCon
-> TcPluginM
     'Init
     (TyCon
      -> TyCon
      -> TyCon
      -> TyCon
      -> TyCon
      -> TyCon
      -> TyCon
      -> LookedUpTyCons
      -> ExtraDefs)
forall a b.
TcPluginM 'Init (a -> b) -> TcPluginM 'Init a -> TcPluginM 'Init b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Name -> TcPluginM 'Init TyCon
look ''GHC.TypeLits.Extra.Min
              TcPluginM
  'Init
  (TyCon
   -> TyCon
   -> TyCon
   -> TyCon
   -> TyCon
   -> TyCon
   -> TyCon
   -> LookedUpTyCons
   -> ExtraDefs)
-> TcPluginM 'Init TyCon
-> TcPluginM
     'Init
     (TyCon
      -> TyCon
      -> TyCon
      -> TyCon
      -> TyCon
      -> TyCon
      -> LookedUpTyCons
      -> ExtraDefs)
forall a b.
TcPluginM 'Init (a -> b) -> TcPluginM 'Init a -> TcPluginM 'Init b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> TyCon -> TcPluginM 'Init TyCon
forall a. a -> TcPluginM 'Init a
forall (f :: * -> *) a. Applicative f => a -> f a
pure TyCon
typeNatDivTyCon
              TcPluginM
  'Init
  (TyCon
   -> TyCon
   -> TyCon
   -> TyCon
   -> TyCon
   -> TyCon
   -> LookedUpTyCons
   -> ExtraDefs)
-> TcPluginM 'Init TyCon
-> TcPluginM
     'Init
     (TyCon
      -> TyCon -> TyCon -> TyCon -> TyCon -> LookedUpTyCons -> ExtraDefs)
forall a b.
TcPluginM 'Init (a -> b) -> TcPluginM 'Init a -> TcPluginM 'Init b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> TyCon -> TcPluginM 'Init TyCon
forall a. a -> TcPluginM 'Init a
forall (f :: * -> *) a. Applicative f => a -> f a
pure TyCon
typeNatModTyCon
              TcPluginM
  'Init
  (TyCon
   -> TyCon -> TyCon -> TyCon -> TyCon -> LookedUpTyCons -> ExtraDefs)
-> TcPluginM 'Init TyCon
-> TcPluginM
     'Init
     (TyCon -> TyCon -> TyCon -> TyCon -> LookedUpTyCons -> ExtraDefs)
forall a b.
TcPluginM 'Init (a -> b) -> TcPluginM 'Init a -> TcPluginM 'Init b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Name -> TcPluginM 'Init TyCon
look ''GHC.TypeLits.Extra.FLog
              TcPluginM
  'Init
  (TyCon -> TyCon -> TyCon -> TyCon -> LookedUpTyCons -> ExtraDefs)
-> TcPluginM 'Init TyCon
-> TcPluginM
     'Init (TyCon -> TyCon -> TyCon -> LookedUpTyCons -> ExtraDefs)
forall a b.
TcPluginM 'Init (a -> b) -> TcPluginM 'Init a -> TcPluginM 'Init b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Name -> TcPluginM 'Init TyCon
look ''GHC.TypeLits.Extra.CLog
              TcPluginM
  'Init (TyCon -> TyCon -> TyCon -> LookedUpTyCons -> ExtraDefs)
-> TcPluginM 'Init TyCon
-> TcPluginM 'Init (TyCon -> TyCon -> LookedUpTyCons -> ExtraDefs)
forall a b.
TcPluginM 'Init (a -> b) -> TcPluginM 'Init a -> TcPluginM 'Init b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Name -> TcPluginM 'Init TyCon
look ''GHC.TypeLits.Extra.Log
              TcPluginM 'Init (TyCon -> TyCon -> LookedUpTyCons -> ExtraDefs)
-> TcPluginM 'Init TyCon
-> TcPluginM 'Init (TyCon -> LookedUpTyCons -> ExtraDefs)
forall a b.
TcPluginM 'Init (a -> b) -> TcPluginM 'Init a -> TcPluginM 'Init b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Name -> TcPluginM 'Init TyCon
look ''GHC.TypeLits.Extra.GCD
              TcPluginM 'Init (TyCon -> LookedUpTyCons -> ExtraDefs)
-> TcPluginM 'Init TyCon
-> TcPluginM 'Init (LookedUpTyCons -> ExtraDefs)
forall a b.
TcPluginM 'Init (a -> b) -> TcPluginM 'Init a -> TcPluginM 'Init b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Name -> TcPluginM 'Init TyCon
look ''GHC.TypeLits.Extra.LCM
              TcPluginM 'Init (LookedUpTyCons -> ExtraDefs)
-> TcPluginM 'Init LookedUpTyCons -> TcPluginM 'Init ExtraDefs
forall a b.
TcPluginM 'Init (a -> b) -> TcPluginM 'Init a -> TcPluginM 'Init b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> TcPluginM 'Init LookedUpTyCons
lookupTyCons
  where
    look :: TH.Name -> TcPluginM 'Init TyCon
    look :: Name -> TcPluginM 'Init TyCon
look Name
nm = Name -> TcPluginM 'Init TyCon
forall (m :: * -> *). MonadTcPlugin m => Name -> m TyCon
tcLookupTyCon (Name -> TcPluginM 'Init TyCon)
-> TcPluginM 'Init Name -> TcPluginM 'Init TyCon
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< Name -> TcPluginM 'Init Name
forall (s :: TcPluginStage).
(Monad (TcPluginM s), MonadTcPlugin (TcPluginM s)) =>
Name -> TcPluginM s Name
lookupTHName Name
nm

setCtEv :: Ct -> CtEvidence -> Ct
setCtEv :: Ct -> CtEvidence -> Ct
setCtEv Ct
ct CtEvidence
ev = case Ct
ct of
  CQuantCan QCInst
qc -> QCInst -> Ct
CQuantCan (QCInst
qc { qci_ev = ev})
#if MIN_VERSION_ghc(9,8,0)
  CDictCan DictCt
di     -> DictCt -> Ct
CDictCan (DictCt
di { di_ev = ev})
  CIrredCan IrredCt
ir    -> IrredCt -> Ct
CIrredCan (IrredCt
ir { ir_ev = ev})
  CEqCan EqCt
eq       -> EqCt -> Ct
CEqCan (EqCt
eq { eq_ev = ev})
  CNonCanonical CtEvidence
_ -> CtEvidence -> Ct
CNonCanonical CtEvidence
ev
#else
  ctX             -> ctX { cc_ev = ev }
#endif

mkLeqQNat :: LookedUpTyCons -> Type -> Type -> Type
mkLeqQNat :: LookedUpTyCons -> Type -> Type -> Type
mkLeqQNat LookedUpTyCons
tcs Type
x Type
y =
#if MIN_VERSION_ghc(9,1,0)
  TyCon -> [Type] -> Type
mkTyConApp (LookedUpTyCons -> TyCon
ordCondTyCon LookedUpTyCons
tcs)
    [ Type
boolTy
    , TyCon -> [Type] -> Type
mkTyConApp (LookedUpTyCons -> TyCon
cmpNatTyCon LookedUpTyCons
tcs) [Type
x,Type
y]
    , TyCon -> [Type] -> Type
mkTyConApp TyCon
promotedTrueDataCon []
    , TyCon -> [Type] -> Type
mkTyConApp TyCon
promotedTrueDataCon []
    , TyCon -> [Type] -> Type
mkTyConApp TyCon
promotedFalseDataCon []
    ]
#else
  mkTyConApp (leqQNatTyCon tcs) [x, y]
#endif

toLeqPredType :: Monad m => LookedUpTyCons -> Ct -> Type -> Type -> m PredType
toLeqPredType :: forall (m :: * -> *).
Monad m =>
LookedUpTyCons -> Ct -> Type -> Type -> m Type
toLeqPredType LookedUpTyCons
defs Ct
ct Type
t1 Type
t2 = case HasDebugCallStack => Type -> Maybe (TyCon, [Type])
Type -> Maybe (TyCon, [Type])
splitTyConApp_maybe (Type -> Maybe (TyCon, [Type])) -> Type -> Maybe (TyCon, [Type])
forall a b. (a -> b) -> a -> b
$ CtEvidence -> Type
ctEvPred (CtEvidence -> Type) -> CtEvidence -> Type
forall a b. (a -> b) -> a -> b
$ Ct -> CtEvidence
ctEvidence Ct
ct of
  Just (TyCon
tc, [Type
a, Type
b, Type
_, Type
_]) | TyCon
tc TyCon -> Unique -> Bool
forall a. Uniquable a => a -> Unique -> Bool
`hasKey` Unique
eqPrimTyConKey -> Type -> m Type
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (TyCon -> [Type] -> Type
mkTyConApp TyCon
tc [Type
a, Type
b, Type
t1, Type
t2])
#if MIN_VERSION_ghc(9,3,0)
  Just (TyCon
tc, [Type
_, Type
b]) | TyCon
tc TyCon -> TyCon -> Bool
forall a. Eq a => a -> a -> Bool
== LookedUpTyCons -> TyCon
assertTyCon LookedUpTyCons
defs -> Type -> m Type
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (TyCon -> [Type] -> Type
mkTyConApp TyCon
tc [Type
t1,Type
b])
#endif
  Maybe (TyCon, [Type])
_ -> [Char] -> m Type
forall a. HasCallStack => [Char] -> a
error [Char]
"Impossible: neither (<=?) nor Assert"